Also avoid Collections.singleton*

The same arguments as for Collections.emptyList apply,
but additionally, the Immutable* classes forbid null.
There were actually some cases of Collections.singleton where forbidden
nulls are good because they will make us catch unexpected nulls earlier.
Furthermore, the name of Collections.singleton() does not mention that
it returns a set, so there were some callers where a list would better
fit (because they assigned lists to a variable on some code paths and a
singleton set on other paths).

Author: PhilippWendler

src/org/sosy_lab/java_smt/api/InterpolatingProverEnvironment.java

@@ -20,9 +20,9 @@
 package org.sosy_lab.java_smt.api;
 
 import com.google.common.base.Preconditions;
+import com.google.common.collect.ImmutableSet;
 import com.google.common.collect.Lists;
 import java.util.Collection;
-import java.util.Collections;
 import java.util.List;
 
 /**
@@ -77,7 +77,7 @@ default List<BooleanFormula> getSeqInterpolants(List<? extends Collection<T>> pa
 
   default List<BooleanFormula> getSeqInterpolants0(List<T> formulas)
       throws SolverException, InterruptedException {
-    return getSeqInterpolants(Lists.transform(formulas, Collections::singleton));
+    return getSeqInterpolants(Lists.transform(formulas, ImmutableSet::of));
   }
 
   /**
@@ -120,7 +120,7 @@ List<BooleanFormula> getTreeInterpolants(
 
   default List<BooleanFormula> getTreeInterpolants0(List<T> formulas, int[] startOfSubTree)
       throws SolverException, InterruptedException {
-    return getTreeInterpolants(Lists.transform(formulas, Collections::singleton), startOfSubTree);
+    return getTreeInterpolants(Lists.transform(formulas, ImmutableSet::of), startOfSubTree);
   }
 
   /** Checks for a valid subtree-structure. This code is taken from SMTinterpol. */

src/org/sosy_lab/java_smt/api/QuantifiedFormulaManager.java

@@ -19,7 +19,7 @@
  */
 package org.sosy_lab.java_smt.api;
 
-import java.util.Collections;
+import com.google.common.collect.ImmutableList;
 import java.util.List;
 
 /**
@@ -56,12 +56,12 @@ default BooleanFormula forall(List<? extends Formula> pVariables, BooleanFormula
 
   /** Syntax sugar, see {@link #forall(List, BooleanFormula)}. */
   default BooleanFormula forall(Formula quantifiedArg, BooleanFormula pBody) {
-    return forall(Collections.singletonList(quantifiedArg), pBody);
+    return forall(ImmutableList.of(quantifiedArg), pBody);
   }
 
   /** Syntax sugar, see {@link #exists(List, BooleanFormula)}. */
   default BooleanFormula exists(Formula quantifiedArg, BooleanFormula pBody) {
-    return exists(Collections.singletonList(quantifiedArg), pBody);
+    return exists(ImmutableList.of(quantifiedArg), pBody);
   }
 
   /**

src/org/sosy_lab/java_smt/example/Interpolation.java

@@ -2,8 +2,8 @@
 
 import com.google.common.base.Preconditions;
 import com.google.common.collect.ImmutableList;
+import com.google.common.collect.ImmutableSet;
 import java.util.ArrayList;
-import java.util.Collections;
 import java.util.HashSet;
 import java.util.List;
 import java.util.Set;
@@ -111,17 +111,17 @@ private static <T> void interpolateExample(
     {
       // example 1b :
       // alternative solution ... with more code and partitioned formulas.
-      Set<T> partition0 = Collections.singleton(ip0);
-      Set<T> partition1 = Collections.singleton(ip1);
-      Set<T> partition2 = Collections.singleton(ip2);
+      Set<T> partition0 = ImmutableSet.of(ip0);
+      Set<T> partition1 = ImmutableSet.of(ip1);
+      Set<T> partition2 = ImmutableSet.of(ip2);
       itps = prover.getSeqInterpolants(ImmutableList.of(partition0, partition1, partition2));
       logger.log(Level.INFO, "1b :: Interpolants for [{ip0},{ip1},{ip2}] are:", itps);
     }
 
     {
       // example 2a :
       // get a sequence of interpolants for two formulas: (get-interpolants IP_1 (and IP_0 IP_2)).
-      Set<T> partition3 = Collections.singleton(ip0);
+      Set<T> partition3 = ImmutableSet.of(ip0);
       Set<T> partition4 = new HashSet<>();
       partition4.add(ip1);
       partition4.add(ip2);

src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java

@@ -37,7 +37,6 @@
 import com.google.common.collect.ImmutableSet;
 import java.util.ArrayList;
 import java.util.Collection;
-import java.util.Collections;
 import java.util.HashMap;
 import java.util.Map;
 import org.checkerframework.checker.nullness.qual.Nullable;
@@ -135,7 +134,7 @@ private Map<IIntLit, ITerm> getArrayAddresses(
           }
           fKey = creator.getEnv().makeSelect(arrayF, arrayIndex);
           name = arrayF.toString();
-          argumentInterpretations = Collections.singleton(creator.convertValue(arrayIndex));
+          argumentInterpretations = ImmutableList.of(creator.convertValue(arrayIndex));
           break;
         case "store":
           // array-access, for explanation see #getArrayAddresses
@@ -152,7 +151,7 @@ private Map<IIntLit, ITerm> getArrayAddresses(
           fKey = creator.getEnv().makeSelect(arrayF2, arrayIndex2);
           fValue = arrayContent;
           name = arrayF2.toString();
-          argumentInterpretations = Collections.singleton(creator.convertValue(arrayIndex2));
+          argumentInterpretations = ImmutableList.of(creator.convertValue(arrayIndex2));
           break;
         default:
           // normal variable or UF

src/org/sosy_lab/java_smt/solvers/z3/Z3Model.java

@@ -28,7 +28,6 @@
 import com.microsoft.z3.enumerations.Z3_sort_kind;
 import java.util.ArrayList;
 import java.util.Collection;
-import java.util.Collections;
 import java.util.HashSet;
 import java.util.List;
 import java.util.Set;
@@ -111,7 +110,7 @@ private Collection<ValueAssignment> getConstAssignments(long keyDecl) {
     try {
       long symbol = Native.getDeclName(z3context, keyDecl);
       if (z3creator.isConstant(value)) {
-        return Collections.singletonList(
+        return ImmutableList.of(
             new ValueAssignment(
                 z3creator.encapsulateWithTypeOf(var),
                 z3creator.encapsulateWithTypeOf(value),

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

@@ -28,7 +28,6 @@
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableSet;
 import com.google.common.collect.Lists;
-import java.util.Collections;
 import java.util.List;
 import java.util.Set;
 import org.junit.Test;
@@ -87,7 +86,7 @@ public <T> void simpleInterpolation() throws SolverException, InterruptedExcepti
       T id2 = prover.push(f2);
       boolean check = prover.isUnsat();
       assertThat(check).named("formulas must be contradicting").isTrue();
-      prover.getInterpolant(Collections.singletonList(id2));
+      prover.getInterpolant(ImmutableList.of(id2));
       // we actually only check for a successful execution here, the result is irrelevant.
     }
   }
@@ -301,13 +300,13 @@ public <T> void sequentialInterpolation() throws SolverException, InterruptedExc
 
     List<BooleanFormula> itps4 =
         stack.getSeqInterpolants(
-            Lists.transform(ImmutableList.of(TA, TA, TA, TB, TC, TD, TD), Collections::singleton));
+            Lists.transform(ImmutableList.of(TA, TA, TA, TB, TC, TD, TD), ImmutableSet::of));
     List<BooleanFormula> itps5 =
         stack.getSeqInterpolants(
-            Lists.transform(ImmutableList.of(TA, TA, TB, TC, TD, TA, TD), Collections::singleton));
+            Lists.transform(ImmutableList.of(TA, TA, TB, TC, TD, TA, TD), ImmutableSet::of));
     List<BooleanFormula> itps6 =
         stack.getSeqInterpolants(
-            Lists.transform(ImmutableList.of(TB, TC, TD, TA, TA, TA, TD), Collections::singleton));
+            Lists.transform(ImmutableList.of(TB, TC, TD, TA, TA, TA, TD), ImmutableSet::of));
 
     stack.pop(); // clear stack, such that we can re-use the solver
     stack.pop();

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

@@ -27,7 +27,6 @@
 import com.google.common.collect.Lists;
 import java.math.BigDecimal;
 import java.util.ArrayList;
-import java.util.Collections;
 import java.util.List;
 import org.junit.Test;
 import org.junit.runner.RunWith;
@@ -112,13 +111,13 @@ public <T> void basicAssumptionsTest()
               env.isUnsatWithAssumptions(
                   ImmutableList.of(bmgr.not(suffix1), bmgr.not(suffix2), suffix3)))
           .isTrue();
-      assertThat(env.getInterpolant(Collections.singletonList(firstPartForInterpolant)).toString())
+      assertThat(env.getInterpolant(ImmutableList.of(firstPartForInterpolant)).toString())
           .doesNotContain("suffix");
       assertThat(
               env.isUnsatWithAssumptions(
                   ImmutableList.of(bmgr.not(suffix1), bmgr.not(suffix3), suffix2)))
           .isTrue();
-      assertThat(env.getInterpolant(Collections.singletonList(firstPartForInterpolant)).toString())
+      assertThat(env.getInterpolant(ImmutableList.of(firstPartForInterpolant)).toString())
           .doesNotContain("suffix");
     }
   }
@@ -160,7 +159,7 @@ public <T> void assumptionsTest()
             .isTrue();
 
         for (int j = 0; j < i; j++) {
-          BooleanFormula itp = env.getInterpolant(Collections.singletonList(ids.get(j)));
+          BooleanFormula itp = env.getInterpolant(ImmutableList.of(ids.get(j)));
           for (String var : mgr.extractVariables(itp).keySet()) {
             assertThat(var).doesNotContain("suffix");
           }