From 34850fae4405bc1e139f0733e0c2e2ea6c32de10 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 3 Sep 2025 09:25:18 +0200 Subject: [PATCH 1/4] replace all usages of "List.of" with more readable "ImmutableList.of/copyOf" to directly show the immutability. This might optimise internal operations, e.g., avoid copies from List to other Lists, if all are ImmutableLists. --- .../java_smt/api/BitvectorFormulaManager.java | 3 ++- .../sosy_lab/java_smt/api/BooleanFormulaManager.java | 6 +++--- src/org/sosy_lab/java_smt/api/UFManager.java | 7 ++++--- .../delegate/debugging/DebuggingAssertions.java | 4 ++-- src/org/sosy_lab/java_smt/example/Binoxxo.java | 11 ++++++----- src/org/sosy_lab/java_smt/example/Sudoku.java | 2 +- .../java_smt/test/BitvectorFormulaManagerTest.java | 7 ++++--- src/org/sosy_lab/java_smt/test/DebugModeTest.java | 2 +- .../java_smt/test/InterpolatingProverTest.java | 2 +- .../sosy_lab/java_smt/test/MixedArithmeticsTest.java | 7 +++---- .../java_smt/test/SolverThreadLocalityTest.java | 3 +-- src/org/sosy_lab/java_smt/test/SolverVisitorTest.java | 4 ++-- .../java_smt/test/StringFormulaManagerTest.java | 4 ++-- 13 files changed, 32 insertions(+), 30 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/api/BitvectorFormulaManager.java index 5d81bb8625..ccef8aaae3 100644 --- a/src/org/sosy_lab/java_smt/api/BitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/BitvectorFormulaManager.java @@ -8,6 +8,7 @@ package org.sosy_lab.java_smt.api; +import com.google.common.collect.ImmutableList; import java.math.BigInteger; import java.util.List; import org.sosy_lab.java_smt.api.FormulaType.BitvectorType; @@ -415,6 +416,6 @@ default BitvectorFormula extract(BitvectorFormula number, int msb, int lsb, bool BooleanFormula distinct(List pBits); default BooleanFormula distinct(BitvectorFormula... pBits) { - return distinct(List.of(pBits)); + return distinct(ImmutableList.copyOf(pBits)); } } diff --git a/src/org/sosy_lab/java_smt/api/BooleanFormulaManager.java b/src/org/sosy_lab/java_smt/api/BooleanFormulaManager.java index a97bf6d780..3777fee198 100644 --- a/src/org/sosy_lab/java_smt/api/BooleanFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/BooleanFormulaManager.java @@ -8,9 +8,9 @@ package org.sosy_lab.java_smt.api; +import com.google.common.collect.ImmutableList; import com.google.errorprone.annotations.CanIgnoreReturnValue; import java.util.Collection; -import java.util.List; import java.util.Set; import java.util.stream.Collector; import org.sosy_lab.java_smt.api.visitors.BooleanFormulaTransformationVisitor; @@ -113,7 +113,7 @@ default BooleanFormula makeBoolean(boolean value) { * @see #and(BooleanFormula, BooleanFormula) */ default BooleanFormula and(BooleanFormula... bits) { - return and(List.of(bits)); + return and(ImmutableList.copyOf(bits)); } /** Return a stream {@link Collector} that creates a conjunction of all elements in the stream. */ @@ -137,7 +137,7 @@ default BooleanFormula and(BooleanFormula... bits) { * @see #or(BooleanFormula, BooleanFormula) */ default BooleanFormula or(BooleanFormula... bits) { - return or(List.of(bits)); + return or(ImmutableList.copyOf(bits)); } /** Return a stream {@link Collector} that creates a disjunction of all elements in the stream. */ diff --git a/src/org/sosy_lab/java_smt/api/UFManager.java b/src/org/sosy_lab/java_smt/api/UFManager.java index ae5d8e3c13..ab11223fc4 100644 --- a/src/org/sosy_lab/java_smt/api/UFManager.java +++ b/src/org/sosy_lab/java_smt/api/UFManager.java @@ -8,6 +8,7 @@ package org.sosy_lab.java_smt.api; +import com.google.common.collect.ImmutableList; import java.util.List; /** Manager for dealing with uninterpreted functions (UFs). */ @@ -20,7 +21,7 @@ FunctionDeclaration declareUF( /** Declare an uninterpreted function. */ default FunctionDeclaration declareUF( String name, FormulaType returnType, FormulaType... args) { - return declareUF(name, returnType, List.of(args)); + return declareUF(name, returnType, ImmutableList.copyOf(args)); } /** @@ -38,7 +39,7 @@ default FunctionDeclaration declareUF( * @see #callUF(FunctionDeclaration, List) */ default T callUF(FunctionDeclaration funcType, Formula... args) { - return callUF(funcType, List.of(args)); + return callUF(funcType, ImmutableList.copyOf(args)); } /** @@ -58,6 +59,6 @@ T declareAndCallUF( */ default T declareAndCallUF( String name, FormulaType pReturnType, Formula... pArgs) { - return declareAndCallUF(name, pReturnType, List.of(pArgs)); + return declareAndCallUF(name, pReturnType, ImmutableList.copyOf(pArgs)); } } diff --git a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingAssertions.java b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingAssertions.java index dd2b35bd8b..f527f30235 100644 --- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingAssertions.java +++ b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingAssertions.java @@ -9,7 +9,7 @@ package org.sosy_lab.java_smt.delegate.debugging; import com.google.common.base.Preconditions; -import java.util.List; +import com.google.common.collect.ImmutableList; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; @@ -54,7 +54,7 @@ public void addFunctionDeclaration(FunctionDeclaration pFunctionDeclaration) /** Assert that the function declaration belongs to this context. */ public void assertDeclarationInContext(FunctionDeclaration pFunctionDeclaration) { - if (List.of(FunctionDeclarationKind.VAR, FunctionDeclarationKind.UF) + if (ImmutableList.of(FunctionDeclarationKind.VAR, FunctionDeclarationKind.UF) .contains(pFunctionDeclaration.getKind())) { Preconditions.checkArgument( debugInfo.getDeclaredFunctions().contains(pFunctionDeclaration), diff --git a/src/org/sosy_lab/java_smt/example/Binoxxo.java b/src/org/sosy_lab/java_smt/example/Binoxxo.java index 2fac732adc..228b9081bd 100644 --- a/src/org/sosy_lab/java_smt/example/Binoxxo.java +++ b/src/org/sosy_lab/java_smt/example/Binoxxo.java @@ -9,6 +9,7 @@ package org.sosy_lab.java_smt.example; import com.google.common.base.Preconditions; +import com.google.common.collect.ImmutableList; import java.io.IOException; import java.math.BigInteger; import java.nio.charset.Charset; @@ -95,7 +96,7 @@ public static void main(String... args) SolverContextFactory.createSolverContext(config, logger, notifier, solver)) { for (BinoxxoSolver binoxxo : - List.of( + ImmutableList.of( new IntegerBasedBinoxxoSolver(context), new BooleanBasedBinoxxoSolver(context))) { long start = System.currentTimeMillis(); @@ -300,7 +301,7 @@ List getRules(IntegerFormula[][] symbols) { for (int row = 0; row < size; row++) { for (int col = 0; col < size - 2; col++) { List lst = - List.of(symbols[row][col], symbols[row][col + 1], symbols[row][col + 2]); + ImmutableList.of(symbols[row][col], symbols[row][col + 1], symbols[row][col + 2]); IntegerFormula sum = imgr.sum(lst); rules.add(bmgr.or(imgr.equal(one, sum), imgr.equal(two, sum))); } @@ -310,7 +311,7 @@ List getRules(IntegerFormula[][] symbols) { for (int col = 0; col < size; col++) { for (int row = 0; row < size - 2; row++) { List lst = - List.of(symbols[row][col], symbols[row + 1][col], symbols[row + 2][col]); + ImmutableList.of(symbols[row][col], symbols[row + 1][col], symbols[row + 2][col]); IntegerFormula sum = imgr.sum(lst); rules.add(bmgr.or(imgr.equal(one, sum), imgr.equal(two, sum))); } @@ -398,7 +399,7 @@ List getRules(BooleanFormula[][] symbols) { for (int row = 0; row < size; row++) { for (int col = 0; col < size - 2; col++) { List lst = - List.of(symbols[row][col], symbols[row][col + 1], symbols[row][col + 2]); + ImmutableList.of(symbols[row][col], symbols[row][col + 1], symbols[row][col + 2]); rules.add(bmgr.not(bmgr.and(lst))); rules.add(bmgr.or(lst)); } @@ -408,7 +409,7 @@ List getRules(BooleanFormula[][] symbols) { for (int col = 0; col < size; col++) { for (int row = 0; row < size - 2; row++) { List lst = - List.of(symbols[row][col], symbols[row + 1][col], symbols[row + 2][col]); + ImmutableList.of(symbols[row][col], symbols[row + 1][col], symbols[row + 2][col]); rules.add(bmgr.not(bmgr.and(lst))); rules.add(bmgr.or(lst)); } diff --git a/src/org/sosy_lab/java_smt/example/Sudoku.java b/src/org/sosy_lab/java_smt/example/Sudoku.java index 9311a7ebfe..99b3cbd872 100644 --- a/src/org/sosy_lab/java_smt/example/Sudoku.java +++ b/src/org/sosy_lab/java_smt/example/Sudoku.java @@ -108,7 +108,7 @@ public static void main(String... args) SolverContextFactory.createSolverContext(config, logger, notifier, solver)) { for (SudokuSolver sudoku : - List.of( + ImmutableList.of( new IntegerBasedSudokuSolver(context), new EnumerationBasedSudokuSolver(context), new BooleanBasedSudokuSolver(context))) { diff --git a/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java index 84888140af..e70e051ada 100644 --- a/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java @@ -14,6 +14,7 @@ import static org.junit.Assert.assertThrows; import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat; +import com.google.common.collect.ImmutableList; import java.math.BigInteger; import java.util.ArrayList; import java.util.LinkedHashMap; @@ -392,9 +393,9 @@ public void bvVarDistinct() throws SolverException, InterruptedException { BitvectorFormula a = bvmgr.makeVariable(4, "a"); BitvectorFormula num3 = bvmgr.makeBitvector(4, 3); - assertThatFormula(bvmgr.distinct(List.of(a, num3))).isSatisfiable(); - assertThatFormula(bvmgr.distinct(List.of(a, a))).isUnsatisfiable(); - assertThatFormula(bvmgr.distinct(List.of(num3, num3))).isUnsatisfiable(); + assertThatFormula(bvmgr.distinct(ImmutableList.of(a, num3))).isSatisfiable(); + assertThatFormula(bvmgr.distinct(ImmutableList.of(a, a))).isUnsatisfiable(); + assertThatFormula(bvmgr.distinct(ImmutableList.of(num3, num3))).isUnsatisfiable(); } @Test diff --git a/src/org/sosy_lab/java_smt/test/DebugModeTest.java b/src/org/sosy_lab/java_smt/test/DebugModeTest.java index 201c7bf606..dbfe92732b 100644 --- a/src/org/sosy_lab/java_smt/test/DebugModeTest.java +++ b/src/org/sosy_lab/java_smt/test/DebugModeTest.java @@ -149,7 +149,7 @@ public void noSharedFormulasTest() BooleanFormula formula = hardProblem.generate(DEFAULT_PROBLEM_SIZE); // We expect debug mode to throw an exception for all solvers, except CVC4, CVC5 and Yices - if (!List.of(Solvers.CVC4, Solvers.YICES2).contains(solverToUse())) { + if (!ImmutableList.of(Solvers.CVC4, Solvers.YICES2).contains(solverToUse())) { assertThrows(IllegalArgumentException.class, () -> checkFormulaInDebugContext(formula)); } else { checkFormulaInDebugContext(formula); diff --git a/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java b/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java index 21f8a8f6f6..4cc7cae699 100644 --- a/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java +++ b/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java @@ -344,7 +344,7 @@ public void sequentialInterpolationIsNotRepeatedIndividualInterpolation() // sequential interpolation should always work as expected checkItpSequence(ImmutableList.of(A, B, C), itpSeq); - checkItpSequence(ImmutableList.of(A, B, C), List.of(itp1, itp2)); + checkItpSequence(ImmutableList.of(A, B, C), ImmutableList.of(itp1, itp2)); } @Test diff --git a/src/org/sosy_lab/java_smt/test/MixedArithmeticsTest.java b/src/org/sosy_lab/java_smt/test/MixedArithmeticsTest.java index 2a6610c98f..8cae55c855 100644 --- a/src/org/sosy_lab/java_smt/test/MixedArithmeticsTest.java +++ b/src/org/sosy_lab/java_smt/test/MixedArithmeticsTest.java @@ -16,7 +16,6 @@ import com.google.common.collect.ImmutableList; import java.math.BigDecimal; import java.math.BigInteger; -import java.util.List; import java.util.function.BiFunction; import java.util.function.Function; import org.junit.Before; @@ -69,7 +68,7 @@ private void testIntegerOperation( public void createIntegerNumberTest() throws SolverException, InterruptedException { IntegerFormula num1 = imgr.makeNumber(1.0); for (IntegerFormula num2 : - List.of( + ImmutableList.of( imgr.makeNumber(1.0), imgr.makeNumber("1"), imgr.makeNumber(1), @@ -86,7 +85,7 @@ public void createIntegerNumberTest() throws SolverException, InterruptedExcepti public void createRationalNumberTest() throws SolverException, InterruptedException { RationalFormula num1 = rmgr.makeNumber(1.0); for (RationalFormula num2 : - List.of( + ImmutableList.of( rmgr.makeNumber(1.0), rmgr.makeNumber("1"), rmgr.makeNumber(1), @@ -103,7 +102,7 @@ public void createRationalNumberTest() throws SolverException, InterruptedExcept public void createRational2NumberTest() throws SolverException, InterruptedException { RationalFormula num1 = rmgr.makeNumber(1.5); for (RationalFormula num2 : - List.of( + ImmutableList.of( rmgr.makeNumber(1.5), rmgr.makeNumber("1.5"), rmgr.makeNumber(BigDecimal.valueOf(1.5)), diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java index a08232a24a..5718007828 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java @@ -15,7 +15,6 @@ import com.google.common.collect.ImmutableList; import com.google.common.truth.Truth; import java.util.Collection; -import java.util.List; import java.util.concurrent.ExecutionException; import java.util.concurrent.ExecutorService; import java.util.concurrent.Executors; @@ -385,7 +384,7 @@ public void wrongContextTest() // Boolector and Bitwuzla do not support integers, so we have to use two different versions // for this test. BooleanFormula formula = - List.of(Solvers.BOOLECTOR, Solvers.BITWUZLA).contains(solverToUse()) + ImmutableList.of(Solvers.BOOLECTOR, Solvers.BITWUZLA).contains(solverToUse()) ? bmgr.makeFalse() : hardProblem.generate(DEFAULT_PROBLEM_SIZE); diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java index 56b0200874..9ecc665d8e 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java @@ -556,7 +556,7 @@ public void floatMoreVisit() { checkKind(fpmgr.max(x, y), FunctionDeclarationKind.FP_MAX); checkKind(fpmgr.min(x, y), FunctionDeclarationKind.FP_MIN); checkKind(fpmgr.sqrt(x), FunctionDeclarationKind.FP_SQRT); - if (!List.of(Solvers.CVC4, Solvers.CVC5, Solvers.BITWUZLA) + if (!ImmutableList.of(Solvers.CVC4, Solvers.CVC5, Solvers.BITWUZLA) .contains(solverToUse())) { // CVC4/CVC5 and bitwuzla do not support this operation // On Bitwuzla we replaces "fp_to_bv(fpTerm)" with "newVar" and the adds the assertion // "fpTerm = bv_to_fp(newVar)" as a side condition. Unfortunately this workaround will not @@ -589,7 +589,7 @@ protected Void visitDefault(Formula f) { } }; - for (int num : List.of(0, 1, 4, 16, 256, 1024)) { + for (int num : ImmutableList.of(0, 1, 4, 16, 256, 1024)) { Formula bv2fp = fpmgr.fromIeeeBitvector(bvmgr.makeBitvector(16, num), fpType); mgr.visit(bv2fp, visitor); Formula fp2bv = fpmgr.toIeeeBitvector(fpmgr.makeNumber(num, fpType)); diff --git a/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java index c64161aec5..29fe5d89b0 100644 --- a/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java @@ -99,7 +99,7 @@ private void assertEqual(IntegerFormula num1, IntegerFormula num2) private void assertDistinct(IntegerFormula num1, IntegerFormula num2) throws SolverException, InterruptedException { - assertThatFormula(imgr.distinct(List.of(num1, num2))).isTautological(); + assertThatFormula(imgr.distinct(ImmutableList.of(num1, num2))).isTautological(); } private void assertEqual(StringFormula str1, StringFormula str2) @@ -1041,7 +1041,7 @@ public void testUnicodeEscaping() throws SolverException, InterruptedException { if (solverToUse() == Solvers.PRINCESS) { for (String invalidStr : - List.of( + ImmutableList.of( "\\u{10000}", Character.toString(0x10000), "\\u{2FFFF}", From 9246c13bc246007cb6bf470507bd472235641dd8 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 3 Sep 2025 09:59:13 +0200 Subject: [PATCH 2/4] replace all usages of "Arrays.asList" with "ImmutableList.copyOf" to directly show the immutability. This might cause one additional copy of the array-content in some cases, however, we iterate over the content again in the next step, so this is just a very small overhead, and it brings the benefit of immutability. --- src/org/sosy_lab/java_smt/api/StringFormulaManager.java | 6 +++--- .../sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java | 4 ++-- src/org/sosy_lab/java_smt/basicimpl/AbstractUFManager.java | 4 ++-- .../sosy_lab/java_smt/solvers/cvc4/CVC4NativeAPITest.java | 4 ++-- .../sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java | 4 ++-- .../java_smt/solvers/princess/PrincessEnvironment.java | 3 +-- src/org/sosy_lab/java_smt/test/NonLinearArithmeticTest.java | 5 ++--- .../java_smt/test/NonLinearArithmeticWithModuloTest.java | 6 +++--- src/org/sosy_lab/java_smt/test/TranslateFormulaTest.java | 4 ++-- 9 files changed, 19 insertions(+), 21 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/StringFormulaManager.java b/src/org/sosy_lab/java_smt/api/StringFormulaManager.java index a028e3ced1..8dd013d21a 100644 --- a/src/org/sosy_lab/java_smt/api/StringFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/StringFormulaManager.java @@ -8,7 +8,7 @@ package org.sosy_lab.java_smt.api; -import java.util.Arrays; +import com.google.common.collect.ImmutableList; import java.util.List; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager; @@ -104,7 +104,7 @@ public interface StringFormulaManager { IntegerFormula length(StringFormula str); default StringFormula concat(StringFormula... parts) { - return concat(Arrays.asList(parts)); + return concat(ImmutableList.copyOf(parts)); } StringFormula concat(List parts); @@ -165,7 +165,7 @@ default RegexFormula range(char start, char end) { * @return formula denoting the concatenation */ default RegexFormula concat(RegexFormula... parts) { - return concatRegex(Arrays.asList(parts)); + return concatRegex(ImmutableList.copyOf(parts)); } /** diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java index 49c2b5ae82..d9c3f691f6 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java @@ -15,11 +15,11 @@ import com.google.common.base.CharMatcher; import com.google.common.base.Preconditions; import com.google.common.collect.ImmutableBiMap; +import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableMap; import com.google.common.collect.ImmutableSet; import com.google.common.collect.Iterables; import java.io.IOException; -import java.util.Arrays; import java.util.List; import java.util.Map; import org.checkerframework.checker.nullness.qual.Nullable; @@ -542,7 +542,7 @@ public T makeApplication( @Override public T makeApplication( FunctionDeclaration declaration, Formula... args) { - return makeApplication(declaration, Arrays.asList(args)); + return makeApplication(declaration, ImmutableList.copyOf(args)); } @Override diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractUFManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractUFManager.java index 5ead7c1d03..88f0378431 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractUFManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractUFManager.java @@ -10,8 +10,8 @@ import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.checkVariableName; +import com.google.common.collect.ImmutableList; import com.google.common.collect.Lists; -import java.util.Arrays; import java.util.List; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; @@ -68,6 +68,6 @@ public T declareAndCallUF( public T declareAndCallUF( String name, FormulaType pReturnType, Formula... pArgs) { checkVariableName(name); - return declareAndCallUF(name, pReturnType, Arrays.asList(pArgs)); + return declareAndCallUF(name, pReturnType, ImmutableList.copyOf(pArgs)); } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NativeAPITest.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NativeAPITest.java index 1fd728b9c0..c3b15f3137 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NativeAPITest.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NativeAPITest.java @@ -11,6 +11,7 @@ import static com.google.common.truth.Truth.assertThat; import static org.junit.Assert.assertThrows; +import com.google.common.collect.ImmutableList; import edu.stanford.CVC4.ArrayType; import edu.stanford.CVC4.BitVector; import edu.stanford.CVC4.BitVectorType; @@ -31,7 +32,6 @@ import edu.stanford.CVC4.vectorExpr; import java.io.FileNotFoundException; import java.io.UnsupportedEncodingException; -import java.util.Arrays; import org.junit.After; import org.junit.AssumptionViolatedException; import org.junit.Before; @@ -766,7 +766,7 @@ public void checkUnsatCore() { // UnsatCores are iterable for (Expr e : unsatCore) { - assertThat(e.toString()).isIn(Arrays.asList("(not (or a b))", "(and a b)")); + assertThat(e.toString()).isIn(ImmutableList.of("(not (or a b))", "(and a b)")); } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java index b500598435..3181dc3f47 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java @@ -12,6 +12,7 @@ import static org.junit.Assert.assertThrows; import com.google.common.base.Preconditions; +import com.google.common.collect.ImmutableList; import io.github.cvc5.CVC5ApiException; import io.github.cvc5.Kind; import io.github.cvc5.Op; @@ -24,7 +25,6 @@ import io.github.cvc5.Term; import io.github.cvc5.TermManager; import java.util.ArrayList; -import java.util.Arrays; import java.util.HashMap; import java.util.List; import java.util.Map; @@ -1031,7 +1031,7 @@ public void checkUnsatCore() { // UnsatCores are iterable for (Term e : unsatCore) { - assertThat(e.toString()).isIn(Arrays.asList("(not (or a b))", "(and a b)")); + assertThat(e.toString()).isIn(ImmutableList.of("(not (or a b))", "(and a b)")); } } diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java index 61a42339c3..f3f933793e 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java @@ -58,7 +58,6 @@ import java.nio.file.Path; import java.util.ArrayDeque; import java.util.ArrayList; -import java.util.Arrays; import java.util.Deque; import java.util.HashMap; import java.util.HashSet; @@ -764,7 +763,7 @@ static Seq toITermSeq(List exprs) { } static Seq toITermSeq(IExpression... exprs) { - return toITermSeq(Arrays.asList(exprs)); + return toITermSeq(ImmutableList.copyOf(exprs)); } IExpression simplify(IExpression f) { diff --git a/src/org/sosy_lab/java_smt/test/NonLinearArithmeticTest.java b/src/org/sosy_lab/java_smt/test/NonLinearArithmeticTest.java index 74e9fec1b9..875f4a5b85 100644 --- a/src/org/sosy_lab/java_smt/test/NonLinearArithmeticTest.java +++ b/src/org/sosy_lab/java_smt/test/NonLinearArithmeticTest.java @@ -14,7 +14,6 @@ import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableSet; import com.google.common.collect.Lists; -import java.util.Arrays; import java.util.List; import java.util.function.Supplier; import org.junit.AssumptionViolatedException; @@ -52,9 +51,9 @@ public class NonLinearArithmeticTest extends SolverBas @Parameters(name = "{0} {1} {2}") public static Iterable getAllSolversAndTheories() { return Lists.cartesianProduct( - Arrays.asList(ParameterizedSolverBasedTest0.getAllSolvers()), + ImmutableList.copyOf(ParameterizedSolverBasedTest0.getAllSolvers()), ImmutableList.of(FormulaType.IntegerType, FormulaType.RationalType), - Arrays.asList(NonLinearArithmetic.values())) + ImmutableList.copyOf(NonLinearArithmetic.values())) .stream() .map(List::toArray) .collect(toImmutableList()); diff --git a/src/org/sosy_lab/java_smt/test/NonLinearArithmeticWithModuloTest.java b/src/org/sosy_lab/java_smt/test/NonLinearArithmeticWithModuloTest.java index c4b595d93d..3b80ce644e 100644 --- a/src/org/sosy_lab/java_smt/test/NonLinearArithmeticWithModuloTest.java +++ b/src/org/sosy_lab/java_smt/test/NonLinearArithmeticWithModuloTest.java @@ -10,9 +10,9 @@ import static com.google.common.collect.ImmutableList.toImmutableList; +import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableSet; import com.google.common.collect.Lists; -import java.util.Arrays; import java.util.List; import java.util.function.Supplier; import org.junit.AssumptionViolatedException; @@ -34,8 +34,8 @@ public class NonLinearArithmeticWithModuloTest extends SolverBasedTest0 { @Parameters(name = "{0} {1}") public static Iterable getAllSolversAndTheories() { return Lists.cartesianProduct( - Arrays.asList(ParameterizedSolverBasedTest0.getAllSolvers()), - Arrays.asList(NonLinearArithmetic.values())) + ImmutableList.copyOf(ParameterizedSolverBasedTest0.getAllSolvers()), + ImmutableList.copyOf(NonLinearArithmetic.values())) .stream() .map(List::toArray) .collect(toImmutableList()); diff --git a/src/org/sosy_lab/java_smt/test/TranslateFormulaTest.java b/src/org/sosy_lab/java_smt/test/TranslateFormulaTest.java index f789912019..365f97261b 100644 --- a/src/org/sosy_lab/java_smt/test/TranslateFormulaTest.java +++ b/src/org/sosy_lab/java_smt/test/TranslateFormulaTest.java @@ -11,8 +11,8 @@ import static com.google.common.truth.TruthJUnit.assume; import static org.sosy_lab.java_smt.test.BooleanFormulaSubject.assertUsing; +import com.google.common.collect.ImmutableList; import com.google.common.collect.Lists; -import java.util.Arrays; import java.util.List; import org.junit.After; import org.junit.Before; @@ -54,7 +54,7 @@ public class TranslateFormulaTest { @Parameters(name = "{index}: {0} --> {1}") public static List getSolverCombinations() { - List solvers = Arrays.asList(Solvers.values()); + List solvers = ImmutableList.copyOf(Solvers.values()); return Lists.transform(Lists.cartesianProduct(solvers, solvers), List::toArray); } From cfbe23f677d3b9d0f49290dc5c53cef01c5897f3 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 3 Sep 2025 10:06:19 +0200 Subject: [PATCH 3/4] replace all usages of "Sets.newHashSet" with "ImmutableSet.of". --- .../java_smt/test/EnumerationFormulaManagerTest.java | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/EnumerationFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/EnumerationFormulaManagerTest.java index 0413e9adb3..06dde29925 100644 --- a/src/org/sosy_lab/java_smt/test/EnumerationFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/EnumerationFormulaManagerTest.java @@ -12,8 +12,8 @@ import static junit.framework.TestCase.assertEquals; import static org.junit.Assert.assertThrows; +import com.google.common.collect.ImmutableSet; import com.google.common.collect.Lists; -import com.google.common.collect.Sets; import java.util.HashSet; import java.util.List; import java.util.Set; @@ -39,12 +39,12 @@ public void init() { @Test public void testEnumerationDeclaration() { - Set colors = Sets.newHashSet("Blue", "White"); + Set colors = ImmutableSet.of("Blue", "White"); EnumerationFormulaType colorType = emgr.declareEnumeration("Color", "Blue", "White"); assertEquals("Color", colorType.getName()); assertEquals(colors, colorType.getElements()); - Set shapes = Sets.newHashSet("Circle", "Square", "Triangle"); + Set shapes = ImmutableSet.of("Circle", "Square", "Triangle"); EnumerationFormulaType shapeType = emgr.declareEnumeration("Shape", shapes); assertEquals("Shape", shapeType.getName()); assertEquals(shapes, shapeType.getElements()); @@ -64,8 +64,8 @@ public void testType() { @Test public void testRepeatedEnumerationDeclaration() { - Set colors = Sets.newHashSet("Blue", "White"); - Set otherColors = Sets.newHashSet("Blue", "White", "Red"); + Set colors = ImmutableSet.of("Blue", "White"); + Set otherColors = ImmutableSet.of("Blue", "White", "Red"); EnumerationFormulaType colorType = emgr.declareEnumeration("Color", colors); // same type again is allowed From 6c7ccb3b8e4bd3dcce835e0a431471c45e014596 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 3 Sep 2025 13:32:25 +0200 Subject: [PATCH 4/4] simplify tests and avoid some unneeded construction of lists. --- src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NativeAPITest.java | 3 +-- src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java | 3 +-- src/org/sosy_lab/java_smt/test/ModelTest.java | 2 +- 3 files changed, 3 insertions(+), 5 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NativeAPITest.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NativeAPITest.java index c3b15f3137..ee96f54adf 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NativeAPITest.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NativeAPITest.java @@ -11,7 +11,6 @@ import static com.google.common.truth.Truth.assertThat; import static org.junit.Assert.assertThrows; -import com.google.common.collect.ImmutableList; import edu.stanford.CVC4.ArrayType; import edu.stanford.CVC4.BitVector; import edu.stanford.CVC4.BitVectorType; @@ -766,7 +765,7 @@ public void checkUnsatCore() { // UnsatCores are iterable for (Expr e : unsatCore) { - assertThat(e.toString()).isIn(ImmutableList.of("(not (or a b))", "(and a b)")); + assertThat(e.toString()).isAnyOf("(not (or a b))", "(and a b)"); } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java index 3181dc3f47..40216f4614 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java @@ -12,7 +12,6 @@ import static org.junit.Assert.assertThrows; import com.google.common.base.Preconditions; -import com.google.common.collect.ImmutableList; import io.github.cvc5.CVC5ApiException; import io.github.cvc5.Kind; import io.github.cvc5.Op; @@ -1031,7 +1030,7 @@ public void checkUnsatCore() { // UnsatCores are iterable for (Term e : unsatCore) { - assertThat(e.toString()).isIn(ImmutableList.of("(not (or a b))", "(and a b)")); + assertThat(e.toString()).isAnyOf("(not (or a b))", "(and a b)"); } } diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index d2e86f68e4..431a20e921 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -856,7 +856,7 @@ public void testPartialModelsUF() throws SolverException, InterruptedException { assume() .withMessage("As of now, only Z3 supports partial model evaluation") .that(solver) - .isIn(ImmutableList.of(Solvers.Z3)); + .isEqualTo(Solvers.Z3); try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { IntegerFormula x = imgr.makeVariable("x"); IntegerFormula f = fmgr.declareAndCallUF("f", IntegerType, x);