replace all usages of "List.of" with more readable "ImmutableList.of/copyOf"

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<BitvectorFormula> pBits);
 
   default BooleanFormula distinct(BitvectorFormula... pBits) {
-    return distinct(List.of(pBits));
+    return distinct(ImmutableList.copyOf(pBits));
   }
 }

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. */

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<StringFormula> 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));
   }
 
   /**

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 @@ <T extends Formula> FunctionDeclaration<T> declareUF(
   /** Declare an uninterpreted function. */
   default <T extends Formula> FunctionDeclaration<T> declareUF(
       String name, FormulaType<T> returnType, FormulaType<?>... args) {
-    return declareUF(name, returnType, List.of(args));
+    return declareUF(name, returnType, ImmutableList.copyOf(args));
   }
 
   /**
@@ -38,7 +39,7 @@ default <T extends Formula> FunctionDeclaration<T> declareUF(
    * @see #callUF(FunctionDeclaration, List)
    */
   default <T extends Formula> T callUF(FunctionDeclaration<T> funcType, Formula... args) {
-    return callUF(funcType, List.of(args));
+    return callUF(funcType, ImmutableList.copyOf(args));
   }
 
   /**
@@ -58,6 +59,6 @@ <T extends Formula> T declareAndCallUF(
    */
   default <T extends Formula> T declareAndCallUF(
       String name, FormulaType<T> pReturnType, Formula... pArgs) {
-    return declareAndCallUF(name, pReturnType, List.of(pArgs));
+    return declareAndCallUF(name, pReturnType, ImmutableList.copyOf(pArgs));
   }
 }

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 extends Formula> T makeApplication(
   @Override
   public <T extends Formula> T makeApplication(
       FunctionDeclaration<T> declaration, Formula... args) {
-    return makeApplication(declaration, Arrays.asList(args));
+    return makeApplication(declaration, ImmutableList.copyOf(args));
   }
 
   @Override

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 extends Formula> T declareAndCallUF(
   public <T extends Formula> T declareAndCallUF(
       String name, FormulaType<T> pReturnType, Formula... pArgs) {
     checkVariableName(name);
-    return declareAndCallUF(name, pReturnType, Arrays.asList(pArgs));
+    return declareAndCallUF(name, pReturnType, ImmutableList.copyOf(pArgs));
   }
 }

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),

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<BooleanFormula> getRules(IntegerFormula[][] symbols) {
       for (int row = 0; row < size; row++) {
         for (int col = 0; col < size - 2; col++) {
           List<IntegerFormula> 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<BooleanFormula> getRules(IntegerFormula[][] symbols) {
       for (int col = 0; col < size; col++) {
         for (int row = 0; row < size - 2; row++) {
           List<IntegerFormula> 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<BooleanFormula> getRules(BooleanFormula[][] symbols) {
       for (int row = 0; row < size; row++) {
         for (int col = 0; col < size - 2; col++) {
           List<BooleanFormula> 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<BooleanFormula> getRules(BooleanFormula[][] symbols) {
       for (int col = 0; col < size; col++) {
         for (int row = 0; row < size - 2; row++) {
           List<BooleanFormula> 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));
         }

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))) {

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NativeAPITest.java

@@ -31,7 +31,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 +765,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()).isAnyOf("(not (or a b))", "(and a b)");
     }
   }
 

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java

@@ -24,7 +24,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 +1030,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()).isAnyOf("(not (or a b))", "(and a 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<ITerm> toITermSeq(List<IExpression> exprs) {
   }
 
   static Seq<ITerm> toITermSeq(IExpression... exprs) {
-    return toITermSeq(Arrays.asList(exprs));
+    return toITermSeq(ImmutableList.copyOf(exprs));
   }
 
   IExpression simplify(IExpression f) {

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

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);

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<String> colors = Sets.newHashSet("Blue", "White");
+    Set<String> colors = ImmutableSet.of("Blue", "White");
     EnumerationFormulaType colorType = emgr.declareEnumeration("Color", "Blue", "White");
     assertEquals("Color", colorType.getName());
     assertEquals(colors, colorType.getElements());
 
-    Set<String> shapes = Sets.newHashSet("Circle", "Square", "Triangle");
+    Set<String> 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<String> colors = Sets.newHashSet("Blue", "White");
-    Set<String> otherColors = Sets.newHashSet("Blue", "White", "Red");
+    Set<String> colors = ImmutableSet.of("Blue", "White");
+    Set<String> otherColors = ImmutableSet.of("Blue", "White", "Red");
     EnumerationFormulaType colorType = emgr.declareEnumeration("Color", colors);
 
     // same type again is allowed

src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java

@@ -344,7 +344,7 @@ public <T> 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

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)),

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);