Merge pull request #336 from sosy-lab/310-cvc5-parallel-prover-instan…

…ces-cause-issues-found-in-cpachecker-benchmark

310 cvc5 parallel prover instances cause issues found in cpachecker benchmark

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

@@ -14,10 +14,12 @@
 import com.google.common.base.Preconditions;
 import com.google.common.base.Splitter;
 import com.google.common.collect.FluentIterable;
+import com.google.common.collect.HashBasedTable;
 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 com.google.common.collect.Table;
 import io.github.cvc5.CVC5ApiException;
 import io.github.cvc5.Datatype;
 import io.github.cvc5.DatatypeConstructor;
@@ -28,6 +30,7 @@
 import io.github.cvc5.Sort;
 import io.github.cvc5.Term;
 import io.github.cvc5.Triplet;
+import java.lang.reflect.Array;
 import java.math.BigDecimal;
 import java.math.BigInteger;
 import java.util.ArrayList;
@@ -71,7 +74,9 @@ public class CVC5FormulaCreator extends FormulaCreator<Term, Sort, Solver, Term>
   // private static final Pattern FLOATING_POINT_PATTERN = Pattern.compile("^\\(fp #b(?<sign>\\d)
   // #b(?<exp>\\d+) #b(?<mant>\\d+)$");
 
-  private final Map<String, Term> variablesCache = new HashMap<>();
+  // <Name, Sort.toString, Term> because CVC5 returns distinct pointers for types, while the
+  // String representation is equal (and they are equal)
+  private final Table<String, String, Term> variablesCache = HashBasedTable.create();
   private final Map<String, Term> functionsCache = new HashMap<>();
   private final Solver solver;
 
@@ -88,15 +93,32 @@ protected CVC5FormulaCreator(Solver pSolver) {
 
   @Override
   public Term makeVariable(Sort sort, String name) {
-    checkSymbol(name);
-    Term exp = variablesCache.computeIfAbsent(name, n -> solver.mkConst(sort, name));
-    Preconditions.checkArgument(
-        sort.equals(exp.getSort()),
-        "symbol name %s with sort %s already in use for different sort %s",
-        name,
-        sort,
-        exp.getSort());
-    return exp;
+    Term existingVar = variablesCache.get(name, sort.toString());
+    if (existingVar != null) {
+      return existingVar;
+    }
+    if (variablesCache.containsRow(name)) {
+      throw new IllegalArgumentException(
+          "Symbol "
+              + name
+              + " requested with type "
+              + sort
+              + ", but "
+              + "already "
+              + "used "
+              + "with "
+              + "type "
+              + variablesCache
+                  .rowMap()
+                  .get(name)
+                  .entrySet()
+                  .toArray((java.util.Map.Entry[]) Array.newInstance(java.util.Map.Entry.class, 0))[
+                  0]
+                  .getKey());
+    }
+    Term newVar = solver.mkConst(sort, name);
+    variablesCache.put(name, sort.toString(), newVar);
+    return newVar;
   }
 
   /**
@@ -391,7 +413,7 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, final Term f) {
         // BOUND vars are used for all vars that are bound to a quantifier in CVC5.
         // We resubstitute them back to the original free.
         // CVC5 doesn't give you the de-brujin index
-        Term originalVar = variablesCache.get(dequote(formula.toString()));
+        Term originalVar = accessVariablesCache(formula.toString(), sort);
         return visitor.visitBoundVariable(encapsulate(originalVar), 0);
 
       } else if (f.getKind() == Kind.FORALL || f.getKind() == Kind.EXISTS) {
@@ -401,7 +423,7 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, final Term f) {
         List<Formula> freeVars = new ArrayList<>();
         for (Term boundVar : f.getChild(0)) { // unpack grand-children of f.
           String name = getName(boundVar);
-          Term freeVar = Preconditions.checkNotNull(variablesCache.get(name));
+          Term freeVar = Preconditions.checkNotNull(accessVariablesCache(name, boundVar.getSort()));
           body = body.substitute(boundVar, freeVar);
           freeVars.add(encapsulate(freeVar));
         }
@@ -829,4 +851,28 @@ public Object convertValue(Term expForType, Term value) {
           e);
     }
   }
+
+  private Term accessVariablesCache(String name, Sort sort) {
+    Term existingVar = variablesCache.get(name, sort.toString());
+    if (existingVar == null) {
+      throw new IllegalArgumentException(
+          "Symbol "
+              + name
+              + " requested with type "
+              + sort
+              + ", but "
+              + "already "
+              + "used "
+              + "with "
+              + "type"
+              + variablesCache
+                  .rowMap()
+                  .get(name)
+                  .entrySet()
+                  .toArray((java.util.Map.Entry[]) Array.newInstance(java.util.Map.Entry.class, 0))[
+                  0]
+                  .getKey());
+    }
+    return existingVar;
+  }
 }

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

@@ -22,7 +22,9 @@
 import io.github.cvc5.Term;
 import java.util.ArrayList;
 import java.util.Arrays;
+import java.util.HashMap;
 import java.util.List;
+import java.util.Map;
 import org.junit.After;
 import org.junit.AssumptionViolatedException;
 import org.junit.Before;
@@ -1322,4 +1324,21 @@ public void testSimpleInterpolation() {
                 Kind.ADD, solver.mkInteger(1), solver.mkTerm(Kind.MULT, z, solver.mkInteger(2))));
     interpolateAndCheck(solver, f1, f2);
   }
+
+  @Test
+  public void testBitvectorSortinVariableCache() throws CVC5ApiException {
+    Map<String, Term> variablesCache = new HashMap<>();
+    String name = "__ADDRESS_OF_main::i@";
+    Sort sort = solver.mkBitVectorSort(32);
+    System.out.println(sort);
+    System.out.println("--------");
+    Term exp = variablesCache.computeIfAbsent(name, n -> solver.mkConst(sort, name));
+    Preconditions.checkArgument(
+        sort.equals(exp.getSort()),
+        "symbol name %s with sort %s already in use for different sort %s with value %s as String",
+        name,
+        sort,
+        exp.getSort(),
+        exp);
+  }
 }

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

@@ -1187,10 +1187,11 @@ public void bvITETest() {
           Solvers.SMTINTERPOL,
           Solvers.MATHSAT5,
           Solvers.CVC4,
+          Solvers.CVC5,
           Solvers.BOOLECTOR,
           Solvers.YICES2,
-          Solvers.CVC5,
           Solvers.OPENSMT);
+
   private static final ImmutableSet<Solvers> VAR_AND_UF_TRACKING_SOLVERS =
       ImmutableSet.of(
           Solvers.SMTINTERPOL,