CVC4: improve implementation of SL.

Author: kfriedberger

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

@@ -73,7 +73,7 @@ private ImmutableList<ValueAssignment> generateModel() {
 
   // TODO this method is highly recursive and should be rewritten with a proper visitor
   private void recursiveAssignmentFinder(ImmutableSet.Builder<ValueAssignment> builder, Expr expr) {
-    if (expr.isConst() || expr.isNull()) {
+    if (expr.getKind() == Kind.SEP_NIL || expr.isConst() || expr.isNull()) {
       // We don't care about consts.
       return;
     } else if (expr.isVariable() && expr.getKind() == Kind.BOUND_VARIABLE) {

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

@@ -45,14 +45,6 @@ protected Expr makeEmptyHeap(Type pT1, Type pT2) {
 
   @Override
   protected Expr makeNilElement(Type pType) {
-    // TODO CVC4 bindings for Java do not support creation of SEP_NIL via mkTerm.
-    //  It is unclear whether this method ever worked.
-    //  CVC4 is deprecated and we will not investigate here.
-    //
-    // Executing this method will cause the following exception:
-    //     Illegal argument detected: CVC4::Expr CVC4::ExprManager::mkExpr(CVC4::Kind, CVC4::Expr)
-    //     `kind' is a bad argument; ... Only operator-style expressions are made with mkExpr();
-    //     to make variables and constants, see mkVar(), mkBoundVar(), and mkConst().
-    return exprManager.mkExpr(Kind.SEP_NIL, pType.mkGroundTerm());
+    return exprManager.mkNullaryOperator(pType, Kind.SEP_NIL);
   }
 }

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

@@ -40,6 +40,7 @@ class CVC4TheoremProver extends AbstractProverWithAllSat<Void>
     implements ProverEnvironment, BasicProverEnvironment<Void> {
 
   private final CVC4FormulaCreator creator;
+  private final int randomSeed;
   SmtEngine smtEngine; // final except for SL theory
   private boolean changedSinceLastSatQuery = false;
 
@@ -50,37 +51,45 @@ class CVC4TheoremProver extends AbstractProverWithAllSat<Void>
    * <p>TODO If the overhead of importing/exporting the expressions is too expensive, we can disable
    * this behavior. This change would cost us the flexibility of setting options per Prover.
    */
-  private final ExprManager exprManager = new ExprManager();
+  private ExprManager exprManager; // final except for SL theory
 
   /** We copy expression between different ExprManagers. The map serves as cache. */
-  private final ExprManagerMapCollection exportMapping = new ExprManagerMapCollection();
+  private ExprManagerMapCollection exportMapping; // final except for SL theory
 
   // CVC4 does not support separation logic in incremental mode.
   private final boolean incremental;
 
   protected CVC4TheoremProver(
       CVC4FormulaCreator pFormulaCreator,
       ShutdownNotifier pShutdownNotifier,
-      int randomSeed,
+      int pRandomSeed,
       Set<ProverOptions> pOptions,
       BooleanFormulaManager pBmgr) {
     super(pOptions, pBmgr, pShutdownNotifier);
 
     creator = pFormulaCreator;
-    smtEngine = new SmtEngine(exprManager);
+    randomSeed = pRandomSeed;
     incremental = !enableSL;
 
-    setOptions(randomSeed, pOptions);
+    createNewEngine();
   }
 
-  private void setOptions(int randomSeed, Set<ProverOptions> pOptions) {
-    smtEngine.setOption("incremental", new SExpr(incremental));
-    if (pOptions.contains(ProverOptions.GENERATE_MODELS)) {
-      smtEngine.setOption("produce-models", new SExpr(true));
+  private void createNewEngine() {
+    if (smtEngine != null) {
+      smtEngine.delete(); // cleanup
+    }
+    if (exportMapping != null) {
+      exportMapping.delete();
     }
-    if (pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE)) {
-      smtEngine.setOption("produce-unsat-cores", new SExpr(true));
+    if (exprManager != null) {
+      exprManager.delete(); // cleanup
     }
+    exprManager = new ExprManager();
+    smtEngine = new SmtEngine(exprManager);
+    exportMapping = new ExprManagerMapCollection();
+    smtEngine.setOption("incremental", new SExpr(incremental));
+    smtEngine.setOption("produce-models", new SExpr(generateModels));
+    smtEngine.setOption("produce-unsat-cores", new SExpr(generateUnsatCores));
     smtEngine.setOption("produce-assertions", new SExpr(true));
     smtEngine.setOption("dump-models", new SExpr(true));
     // smtEngine.setOption("produce-unsat-cores", new SExpr(true));
@@ -93,10 +102,6 @@ private void setOptions(int randomSeed, Set<ProverOptions> pOptions) {
     smtEngine.setOption("full-saturate-quant", new SExpr(true));
   }
 
-  protected void setOptionForIncremental() {
-    smtEngine.setOption("incremental", new SExpr(true));
-  }
-
   /** import an expression from global context into this prover's context. */
   protected Expr importExpr(Expr expr) {
     return expr.exportTo(exprManager, exportMapping);
@@ -172,13 +177,9 @@ protected Evaluator getEvaluatorWithoutChecks() {
   }
 
   private void setChanged() {
-    closeAllEvaluators();
     if (!changedSinceLastSatQuery) {
       changedSinceLastSatQuery = true;
-      if (!incremental) {
-        // create a new clean smtEngine
-        smtEngine = new SmtEngine(exprManager);
-      }
+      closeAllEvaluators();
     }
   }
 
@@ -196,17 +197,20 @@ public boolean isUnsat() throws InterruptedException, SolverException {
     closeAllEvaluators();
     changedSinceLastSatQuery = false;
     if (!incremental) {
-      for (BooleanFormula f : getAssertedFormulas()) {
-        assertFormula(f);
-      }
+      // in non-incremental mode, we need to create a new solver instance for each sat check
+      createNewEngine();
+      getAssertedFormulas().forEach(this::assertFormula);
     }
 
     Result result;
     try (ShutdownHook hook = new ShutdownHook(shutdownNotifier, smtEngine::interrupt)) {
       shutdownNotifier.shutdownIfNecessary();
       result = smtEngine.checkSat();
+    } catch (Exception e) {
+      throw new SolverException("CVC4 failed during satisfiability check", e);
+    } finally {
+      shutdownNotifier.shutdownIfNecessary();
     }
-    shutdownNotifier.shutdownIfNecessary();
     return convertSatResult(result);
   }
 

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

@@ -9,7 +9,7 @@
 package org.sosy_lab.java_smt.test;
 
 import static com.google.common.truth.Truth.assertThat;
-import static com.google.common.truth.TruthJUnit.assume;
+import static org.junit.Assert.assertThrows;
 
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableSet;
@@ -34,21 +34,6 @@ private BooleanFormula makeStarAll(List<BooleanFormula> formulas) {
     return formulas.stream().reduce(slmgr::makeStar).orElse(bmgr.makeTrue());
   }
 
-  protected void requireSepNil() {
-    assume()
-        .withMessage("Java bindings for solver %s do not support SEP_NIL", solverToUse())
-        .that(solverToUse())
-        .isNotEqualTo(Solvers.CVC4);
-  }
-
-  protected void requireMultipleHeapSorts() {
-    assume()
-        .withMessage(
-            "Java bindings for solver %s do not support multiple heap sorts", solverToUse())
-        .that(solverToUse())
-        .isNotEqualTo(Solvers.CVC4);
-  }
-
   @Before
   public void setup() {
     requireSeparationLogic();
@@ -70,24 +55,52 @@ public void testMakeEmp() throws InterruptedException, SolverException {
   }
 
   @Test
-  public void testMakeEmptoP2() throws InterruptedException, SolverException {
-    requireMultipleHeapSorts();
+  public void testMakeEmpWithMultipleSorts() throws InterruptedException, SolverException {
     // Actually, no solver supports multiple heap sorts. However, our bindings for CVC5
-    // apply non-incremental mode for SL and use distinct solver instances for distinct queries.
+    // can not detect the heap sort for EMP, so we use a dummy sort (Int->Int) instead.
 
     BooleanFormula emptyHeapInt =
         slmgr.makeEmptyHeap(FormulaType.RationalType, FormulaType.BooleanType);
     BooleanFormula emptyHeapRat =
         slmgr.makeEmptyHeap(FormulaType.IntegerType, FormulaType.IntegerType);
     BooleanFormula query = bmgr.and(emptyHeapInt, emptyHeapRat);
 
-    assertThatFormula(query).isSatisfiable(ProverOptions.ENABLE_SEPARATION_LOGIC);
+    try (ProverEnvironment prover =
+        context.newProverEnvironment(ProverOptions.ENABLE_SEPARATION_LOGIC)) {
+      prover.push(query);
+      if (solverToUse() == Solvers.CVC5) {
+        assertThatEnvironment(prover).isSatisfiable();
+      } else {
+        assertThrows(Exception.class, () -> prover.isUnsat());
+      }
+      prover.pop();
+    }
   }
 
   @Test
-  public void testNotNilPtoNil() throws InterruptedException, SolverException {
-    requireSepNil();
+  public void testMakeEmpWithMultipleSortsInDistinctQueries()
+      throws InterruptedException, SolverException {
+    // Actually, no solver supports multiple heap sorts. However, our bindings for CVC5
+    // apply non-incremental mode for SL and use distinct solver instances for distinct queries.
+
+    BooleanFormula emptyHeapInt =
+        slmgr.makeEmptyHeap(FormulaType.RationalType, FormulaType.BooleanType);
+    BooleanFormula emptyHeapRat =
+        slmgr.makeEmptyHeap(FormulaType.IntegerType, FormulaType.IntegerType);
+
+    try (ProverEnvironment prover =
+        context.newProverEnvironment(ProverOptions.ENABLE_SEPARATION_LOGIC)) {
+      prover.push(emptyHeapInt);
+      assertThatEnvironment(prover).isSatisfiable();
+      prover.pop();
+      prover.push(emptyHeapRat);
+      assertThatEnvironment(prover).isSatisfiable();
+      prover.pop();
+    }
+  }
 
+  @Test
+  public void testNotNilPtoNil() throws InterruptedException, SolverException {
     IntegerFormula nil = slmgr.makeNilElement(FormulaType.IntegerType);
     BooleanFormula nilPtoNil = slmgr.makePointsTo(nil, nil);
 
@@ -96,8 +109,6 @@ public void testNotNilPtoNil() throws InterruptedException, SolverException {
 
   @Test
   public void testNilPtoValue() throws InterruptedException, SolverException {
-    requireSepNil();
-
     IntegerFormula nil = slmgr.makeNilElement(FormulaType.IntegerType);
     IntegerFormula value = imgr.makeNumber(42);
     BooleanFormula nilPtoValue = slmgr.makePointsTo(nil, value);
@@ -107,8 +118,6 @@ public void testNilPtoValue() throws InterruptedException, SolverException {
 
   @Test
   public void testXPtoNil() throws InterruptedException, SolverException {
-    requireSepNil();
-
     IntegerFormula ptr = imgr.makeVariable("p");
     IntegerFormula nil = slmgr.makeNilElement(FormulaType.IntegerType);
     BooleanFormula ptoNil = slmgr.makePointsTo(ptr, nil);
@@ -127,8 +136,6 @@ public void testXPtoValue() throws InterruptedException, SolverException {
 
   @Test
   public void testPPtoNilThenPPtoNil() throws SolverException, InterruptedException {
-    requireSepNil();
-
     IntegerFormula ptr = imgr.makeVariable("p");
     IntegerFormula nil = slmgr.makeNilElement(FormulaType.IntegerType);
     BooleanFormula ptoNil = slmgr.makePointsTo(ptr, nil);
@@ -141,14 +148,14 @@ public void testPPtoNilThenPPtoNil() throws SolverException, InterruptedExceptio
       prover.push(ptoNil);
       assertThatEnvironment(prover).isSatisfiable();
       assertThatEnvironment(prover).isSatisfiable();
+      assertThatEnvironment(prover).isSatisfiable();
+      assertThatEnvironment(prover).isSatisfiable();
       prover.pop();
     }
   }
 
   @Test
   public void testPtoNilThenPPto42() throws SolverException, InterruptedException {
-    requireSepNil();
-
     IntegerFormula ptr = imgr.makeVariable("p");
     IntegerFormula nil = slmgr.makeNilElement(FormulaType.IntegerType);
     IntegerFormula value = imgr.makeNumber(42);
@@ -210,8 +217,6 @@ public void testStar() throws InterruptedException, SolverException {
 
   @Test
   public void testSimpleTreeValid() throws InterruptedException, SolverException {
-    requireSepNil();
-
     // lets build a tree:
     // - each node consists of two integers: left and right
     // - each node pointer points to the left integer, the right integer is at pointer+1
@@ -250,8 +255,6 @@ public void testSimpleTreeValid() throws InterruptedException, SolverException {
 
   @Test
   public void testSimpleTreeInvalid() throws InterruptedException, SolverException {
-    requireSepNil();
-
     IntegerFormula nil = slmgr.makeNilElement(FormulaType.IntegerType);
     IntegerFormula root = imgr.makeVariable("root");
     IntegerFormula left = imgr.makeVariable("left");
@@ -271,8 +274,6 @@ public void testSimpleTreeInvalid() throws InterruptedException, SolverException
 
   @Test
   public void testListValid() throws InterruptedException, SolverException {
-    requireSepNil();
-
     IntegerFormula nil = slmgr.makeNilElement(FormulaType.IntegerType);
     List<IntegerFormula> nodes = new ArrayList<>();
     for (int i = 0; i <= 10; i++) {