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.

Author: kfriedberger

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

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

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/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<T extends NumeralFormula> extends SolverBas
   @Parameters(name = "{0} {1} {2}")
   public static Iterable<Object[]> 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());

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<Object[]> 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());

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<Object[]> getSolverCombinations() {
-    List<Solvers> solvers = Arrays.asList(Solvers.values());
+    List<Solvers> solvers = ImmutableList.copyOf(Solvers.values());
     return Lists.transform(Lists.cartesianProduct(solvers, solvers), List::toArray);
   }