CVC5: fix repeated usage of non-incremental mode in solver, i.e., just create a new solver whenever needed.

The previous mode either crashed when using a CVC5-solver again or kept the previous assertions when solving new asertions.
The issue only affects SL, other theories use the CVC5-solver in incremental mode, which works as expected.
SL was never properly tested here.

Author: kfriedberger

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

@@ -26,7 +26,6 @@
 import io.github.cvc5.Solver;
 import io.github.cvc5.Sort;
 import io.github.cvc5.Term;
-import io.github.cvc5.TermManager;
 import io.github.cvc5.UnknownExplanation;
 import java.util.ArrayDeque;
 import java.util.ArrayList;
@@ -55,75 +54,81 @@ abstract class CVC5AbstractProver<T> extends AbstractProverWithAllSat<T> {
 
   private final FormulaManager mgr;
   protected final CVC5FormulaCreator creator;
-  protected final Solver solver;
+  private final int randomSeed;
+  private final ImmutableSet<ProverOptions> options;
+  private final ImmutableMap<String, String> furtherOptionsMap;
+  protected Solver solver; // final in incremental mode, non-final in non-incremental mode
   private boolean changedSinceLastSatQuery = false;
   protected final Deque<PersistentMap<String, Term>> assertedTerms = new ArrayDeque<>();
 
   // TODO: does CVC5 support separation logic in incremental mode?
-  //  --> No, CVC5 aborts on addConstraint.
+  //  --> No. In incremental mode, CVC5 aborts when calling addConstraint(...).
+  //  This means, we have to use non-incremental mode when SL is enabled.
+  //  This also means, that push/pop are not supported when SL is enabled and we implement
+  //  our own stack for asserted terms, and use a different solver instance for each sat check.
   protected final boolean incremental;
 
-  // Separation Logic supports only one heap with one sort. Let's store them here.
-  private Sort heapSort = null;
-  private Sort elementSort = null;
-
   protected CVC5AbstractProver(
       CVC5FormulaCreator pFormulaCreator,
       ShutdownNotifier pShutdownNotifier,
-      @SuppressWarnings("unused") int randomSeed,
-      Set<ProverOptions> pOptions,
+      int pRandomSeed,
+      ImmutableSet<ProverOptions> pOptions,
       FormulaManager pMgr,
       ImmutableMap<String, String> pFurtherOptionsMap) {
     super(pOptions, pMgr.getBooleanFormulaManager(), pShutdownNotifier);
 
     mgr = pMgr;
     creator = pFormulaCreator;
+    options = ImmutableSet.copyOf(pOptions);
+    furtherOptionsMap = pFurtherOptionsMap;
+    randomSeed = pRandomSeed;
     incremental = !enableSL;
     assertedTerms.add(PathCopyingPersistentTreeMap.of());
 
-    TermManager termManager = creator.getEnv();
-    solver = new Solver(termManager);
-
-    setSolverOptions(randomSeed, pOptions, pFurtherOptionsMap, solver);
+    if (incremental) {
+      solver = getNewSolver(randomSeed, options, furtherOptionsMap);
+    }
   }
 
-  protected void setSolverOptions(
+  protected Solver getNewSolver(
       int randomSeed,
       Set<ProverOptions> pOptions,
-      ImmutableMap<String, String> pFurtherOptionsMap,
-      Solver pSolver) {
+      ImmutableMap<String, String> pFurtherOptionsMap) {
+    Solver newSolver = new Solver(creator.getEnv());
     try {
-      CVC5SolverContext.setSolverOptions(pSolver, randomSeed, pFurtherOptionsMap);
+      CVC5SolverContext.setSolverOptions(newSolver, randomSeed, pFurtherOptionsMap);
     } catch (CVC5ApiRecoverableException e) {
       // We've already used these options in CVC5SolverContext, so there should be no exception
       throw new AssertionError("Unexpected exception", e);
     }
 
-    pSolver.setOption("incremental", incremental ? "true" : "false");
-    pSolver.setOption("produce-models", generateModels ? "true" : "false");
-    pSolver.setOption("produce-unsat-cores", generateUnsatCores ? "true" : "false");
+    newSolver.setOption("incremental", incremental ? "true" : "false");
+    newSolver.setOption("produce-models", generateModels ? "true" : "false");
+    newSolver.setOption("produce-unsat-cores", generateUnsatCores ? "true" : "false");
 
-    pSolver.setOption("produce-assertions", "true");
-    pSolver.setOption("dump-models", "true");
+    newSolver.setOption("produce-assertions", "true");
+    newSolver.setOption("dump-models", "true");
 
     // Set Strings option to enable all String features (such as lessOrEquals)
-    pSolver.setOption("strings-exp", "true");
+    newSolver.setOption("strings-exp", "true");
 
     // Enable experimental array features
     // Needed when array constants (= with default element) are used
-    pSolver.setOption("arrays-exp", "true");
+    newSolver.setOption("arrays-exp", "true");
 
     // Enable more complete quantifier solving (for more info see CVC5QuantifiedFormulaManager)
-    pSolver.setOption("full-saturate-quant", "true");
+    newSolver.setOption("full-saturate-quant", "true");
 
     // if no logic is set in CVC5, select the broadest logic available: "ALL"
-    if (!solver.isLogicSet()) {
+    if (!newSolver.isLogicSet()) {
       try {
-        solver.setLogic("ALL");
+        newSolver.setLogic("ALL");
       } catch (CVC5ApiException e) {
         throw new AssertionError("Unexpected exception", e);
       }
     }
+
+    return newSolver;
   }
 
   @Override
@@ -217,6 +222,12 @@ public boolean isUnsat() throws InterruptedException, SolverException {
     closeAllEvaluators();
     changedSinceLastSatQuery = false;
     if (!incremental) {
+      // in non-incremental mode, we need to create a new solver instance for each sat check
+      if (solver != null) {
+        solver.deletePointer(); // cleanup
+      }
+      solver = getNewSolver(randomSeed, options, furtherOptionsMap);
+
       ImmutableSet<BooleanFormula> assertedFormulas = getAssertedFormulas();
       if (enableSL) {
         declareHeap(assertedFormulas);
@@ -261,33 +272,10 @@ private void declareHeap(ImmutableSet<BooleanFormula> pAssertedFormulas) throws
               + heapSorts);
     }
 
-    // get the (only) heap sort
-    final Sort newHeapSort = checkNotNull(Iterables.getOnlyElement(heapSorts.keySet()));
-    final Sort newElementSort = checkNotNull(Iterables.getOnlyElement(heapSorts.get(newHeapSort)));
-
-    // if we already have a heap, check that the sorts are the same
-    if (heapSort != null) {
-      checkState(elementSort != null, "Heap sort and element sort must both be defined.");
-      if (!heapSort.equals(newHeapSort) || !elementSort.equals(newElementSort)) {
-        throw new SolverException(
-            "CVC5 SL support is limited to one heap with one sort. Already declared heap with"
-                + " sorts: "
-                + heapSort
-                + "->"
-                + elementSort
-                + ", but found heap with sorts: "
-                + newHeapSort
-                + "->"
-                + newElementSort);
-      }
-    } else {
-      checkState(elementSort == null, "Heap sort and element sort must both be undefined.");
-      heapSort = newHeapSort;
-      elementSort = newElementSort;
-
-      // then declare the heap in the solver, once before the first sat check
-      solver.declareSepHeap(heapSort, elementSort);
-    }
+    // get the (only) heap sort, and declare it in the solver, once before the first sat check
+    final Sort heapSort = checkNotNull(Iterables.getOnlyElement(heapSorts.keySet()));
+    final Sort elementSort = checkNotNull(Iterables.getOnlyElement(heapSorts.get(heapSort)));
+    solver.declareSepHeap(heapSort, elementSort);
   }
 
   @Nonnull

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

@@ -48,7 +48,7 @@ public class CVC5InterpolatingProver extends CVC5AbstractProver<String>
       CVC5FormulaCreator pFormulaCreator,
       ShutdownNotifier pShutdownNotifier,
       int randomSeed,
-      Set<ProverOptions> pOptions,
+      ImmutableSet<ProverOptions> pOptions,
       FormulaManager pMgr,
       ImmutableMap<String, String> pFurtherOptionsMap,
       boolean pValidateInterpolants) {
@@ -66,13 +66,13 @@ public class CVC5InterpolatingProver extends CVC5AbstractProver<String>
    * produce-interpolants which is set here. From CVC5AbstractProver Line 66
    */
   @Override
-  protected void setSolverOptions(
+  protected Solver getNewSolver(
       int randomSeed,
       Set<ProverOptions> pOptions,
-      ImmutableMap<String, String> pFurtherOptionsMap,
-      Solver pSolver) {
-    super.setSolverOptions(randomSeed, pOptions, pFurtherOptionsMap, pSolver);
-    pSolver.setOption("produce-interpolants", "true");
+      ImmutableMap<String, String> pFurtherOptionsMap) {
+    Solver newSolver = super.getNewSolver(randomSeed, pOptions, pFurtherOptionsMap);
+    newSolver.setOption("produce-interpolants", "true");
+    return newSolver;
   }
 
   @Override
@@ -184,8 +184,7 @@ private Term getCVC5Interpolation(Collection<Term> formulasA, Collection<Term> f
     Term phiMinus = bmgr.andImpl(formulasB);
 
     // Uses a separate Solver instance to leave the original solver-context unmodified
-    Solver itpSolver = new Solver(termManager);
-    setSolverOptions(seed, solverOptions, furtherOptionsMap, itpSolver);
+    Solver itpSolver = getNewSolver(seed, solverOptions, furtherOptionsMap);
 
     Term interpolant;
     try {
@@ -225,9 +224,8 @@ private void checkInterpolationCriteria(Term interpolant, Term phiPlus, Term phi
         Sets.difference(interpolantSymbols, intersection));
 
     // build and check both Craig interpolation formulas with the generated interpolant.
-    Solver validationSolver = new Solver(termManager);
     // interpolation option is not required for validation
-    super.setSolverOptions(seed, solverOptions, furtherOptionsMap, validationSolver);
+    Solver validationSolver = getNewSolver(seed, solverOptions, furtherOptionsMap);
     try {
       validationSolver.push();
       validationSolver.assertFormula(termManager.mkTerm(Kind.IMPLIES, phiPlus, interpolant));

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

@@ -14,6 +14,7 @@
 import com.google.common.base.Splitter.MapSplitter;
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableMap;
+import com.google.common.collect.ImmutableSet;
 import io.github.cvc5.CVC5ApiRecoverableException;
 import io.github.cvc5.Solver;
 import io.github.cvc5.TermManager;
@@ -221,7 +222,7 @@ public ProverEnvironment newProverEnvironment0(Set<ProverOptions> pOptions) {
         creator,
         shutdownNotifier,
         randomSeed,
-        pOptions,
+        ImmutableSet.copyOf(pOptions),
         getFormulaManager(),
         settings.furtherOptionsMap);
   }
@@ -239,7 +240,7 @@ protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolatio
         creator,
         shutdownNotifier,
         randomSeed,
-        pOptions,
+        ImmutableSet.copyOf(pOptions),
         getFormulaManager(),
         settings.furtherOptionsMap,
         settings.validateInterpolants);

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

@@ -9,7 +9,7 @@
 package org.sosy_lab.java_smt.solvers.cvc5;
 
 import com.google.common.collect.ImmutableMap;
-import java.util.Set;
+import com.google.common.collect.ImmutableSet;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
@@ -24,8 +24,8 @@ class CVC5TheoremProver extends CVC5AbstractProver<Void>
   protected CVC5TheoremProver(
       CVC5FormulaCreator pFormulaCreator,
       ShutdownNotifier pShutdownNotifier,
-      @SuppressWarnings("unused") int randomSeed,
-      Set<ProverOptions> pOptions,
+      int randomSeed,
+      ImmutableSet<ProverOptions> pOptions,
       FormulaManager pMgr,
       ImmutableMap<String, String> pFurtherOptionsMap) {
     super(pFormulaCreator, pShutdownNotifier, randomSeed, pOptions, pMgr, pFurtherOptionsMap);