Override default methods in BasicProverEnvironment for all delegates

scripts/traceToSmtlib.py

@@ -1532,6 +1532,9 @@ def conv(arg):
             arg1 = stmt.value[-1].args[0]
             log(toExpr('get-value', toExpr('', arg1)))
 
+        elif stmt.getCalls()[-1] == "getEvaluator":
+            pass
+
         elif stmt.getCalls()[-1] == "getModel":
             log(toConst('(get-model)'))
 
@@ -1578,6 +1581,9 @@ def conv(arg):
 
         elif stmt.getCalls()[-1] == "push":
             log(toExpr('push', toConst('1')))
+            if len(stmt.value[-1].args) > 0:
+                arg1 = stmt.value[-1].args[0]
+                log(toExpr('assert', arg1))
 
         else:
             raise Exception(f'Unsupported call: {stmt.getCalls()}')

scripts/tracingTest.sh

@@ -28,7 +28,7 @@ source .venv/bin/activate
 pip install -r requirements.txt
 
 echo -e "\nConverting JavaTraces to Smtlib"
-find ../traces -name *.java -exec ./traceToSmtlib.py --save {} ';' | tee solver.log
+find ../output/traces -name *.java -exec ./traceToSmtlib.py --save {} ';' | tee solver.log
 
 echo -e "\nRunning the solver on the generated Smtlib files"
 find ../traces -name *.smt2 -exec echo "path: {}" ';' -exec timeout 20s $* {} ';' 2>&1 | grep -E "error|path" | tee -a solver.log

src/org/sosy_lab/java_smt/basicimpl/InterpolatingProverDelegate.java

@@ -13,14 +13,18 @@
 import static com.google.common.base.Preconditions.checkArgument;
 import static com.google.common.base.Preconditions.checkNotNull;
 
+import com.google.common.collect.ImmutableList;
+import com.google.common.collect.ImmutableMap;
 import java.util.Collection;
 import java.util.List;
 import java.util.Optional;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.Evaluator;
 import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment;
 import org.sosy_lab.java_smt.api.Model;
 import org.sosy_lab.java_smt.api.SolverException;
+import org.sosy_lab.java_smt.api.UserPropagator;
 
 /**
  * This delegate enables common implementations for methods in {@link
@@ -68,6 +72,11 @@ public List<BooleanFormula> getTreeInterpolants(
 
   /* ########################## Delegate methods of ProverEnvironment ########################## */
 
+  @Override
+  public @Nullable T push(BooleanFormula f) throws InterruptedException {
+    return itpProver.push(f);
+  }
+
   @Override
   public void pop() {
     itpProver.pop();
@@ -104,6 +113,16 @@ public Model getModel() throws SolverException {
     return itpProver.getModel();
   }
 
+  @Override
+  public Evaluator getEvaluator() throws SolverException {
+    return itpProver.getEvaluator();
+  }
+
+  @Override
+  public ImmutableList<Model.ValueAssignment> getModelAssignments() throws SolverException {
+    return itpProver.getModelAssignments();
+  }
+
   @Override
   public List<BooleanFormula> getUnsatCore() {
     return itpProver.getUnsatCore();
@@ -115,6 +134,11 @@ public Optional<List<BooleanFormula>> unsatCoreOverAssumptions(
     return itpProver.unsatCoreOverAssumptions(assumptions);
   }
 
+  @Override
+  public ImmutableMap<String, String> getStatistics() {
+    return itpProver.getStatistics();
+  }
+
   @Override
   public void close() {
     itpProver.close();
@@ -126,6 +150,11 @@ public <R> R allSat(AllSatCallback<R> callback, List<BooleanFormula> important)
     return itpProver.allSat(callback, important);
   }
 
+  @Override
+  public boolean registerUserPropagator(UserPropagator propagator) {
+    return itpProver.registerUserPropagator(propagator);
+  }
+
   /* ############################### Utility methods ############################### */
   @SuppressWarnings("unchecked")
   private AbstractProver<T> getDelegateAsAbstractProver() {

src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java

@@ -13,16 +13,20 @@
 import static com.google.common.base.Preconditions.checkArgument;
 import static com.google.common.base.Preconditions.checkNotNull;
 
+import com.google.common.collect.ImmutableList;
+import com.google.common.collect.ImmutableMap;
 import java.util.Collection;
 import java.util.List;
 import java.util.Optional;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.common.rationals.Rational;
 import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.Evaluator;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.Model;
 import org.sosy_lab.java_smt.api.OptimizationProverEnvironment;
 import org.sosy_lab.java_smt.api.SolverException;
+import org.sosy_lab.java_smt.api.UserPropagator;
 
 /**
  * This delegate enables common implementations for methods in {@link OptimizationProverEnvironment}
@@ -80,6 +84,21 @@ public Model getModel() throws SolverException {
     return optimizationProver.getModel();
   }
 
+  @Override
+  public Evaluator getEvaluator() throws SolverException {
+    return optimizationProver.getEvaluator();
+  }
+
+  @Override
+  public ImmutableList<Model.ValueAssignment> getModelAssignments() throws SolverException {
+    return optimizationProver.getModelAssignments();
+  }
+
+  @Override
+  public @Nullable Void push(BooleanFormula f) throws InterruptedException {
+    return optimizationProver.push(f);
+  }
+
   @Override
   public void pop() {
     optimizationProver.pop();
@@ -122,6 +141,11 @@ public Optional<List<BooleanFormula>> unsatCoreOverAssumptions(
     return optimizationProver.unsatCoreOverAssumptions(assumptions);
   }
 
+  @Override
+  public ImmutableMap<String, String> getStatistics() {
+    return optimizationProver.getStatistics();
+  }
+
   @Override
   public void close() {
     optimizationProver.close();
@@ -133,6 +157,11 @@ public <R> R allSat(AllSatCallback<R> callback, List<BooleanFormula> important)
     return optimizationProver.allSat(callback, important);
   }
 
+  @Override
+  public boolean registerUserPropagator(UserPropagator propagator) {
+    return optimizationProver.registerUserPropagator(propagator);
+  }
+
   /* ############################### Utility methods ############################### */
   @SuppressWarnings("unchecked")
   private AbstractProver<?> getDelegateAsAbstractProver() {

src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java

@@ -14,10 +14,13 @@
 import java.util.Collection;
 import java.util.List;
 import java.util.Optional;
+import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
 import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.Evaluator;
 import org.sosy_lab.java_smt.api.Model;
 import org.sosy_lab.java_smt.api.SolverException;
+import org.sosy_lab.java_smt.api.UserPropagator;
 
 class BasicProverWithAssumptionsWrapper<T, P extends BasicProverEnvironment<T>>
     implements BasicProverEnvironment<T> {
@@ -36,6 +39,12 @@ protected void clearAssumptions() {
     solverAssumptionsAsFormula.clear();
   }
 
+  @Override
+  public @Nullable T push(BooleanFormula f) throws InterruptedException {
+    clearAssumptions();
+    return delegate.push(f);
+  }
+
   @Override
   public void pop() {
     clearAssumptions();
@@ -86,6 +95,11 @@ public Model getModel() throws SolverException {
     return delegate.getModel();
   }
 
+  @Override
+  public Evaluator getEvaluator() throws SolverException {
+    return delegate.getEvaluator();
+  }
+
   @Override
   public ImmutableList<Model.ValueAssignment> getModelAssignments() throws SolverException {
     return delegate.getModelAssignments();
@@ -130,4 +144,9 @@ public <R> R allSat(AllSatCallback<R> pCallback, List<BooleanFormula> pImportant
     clearAssumptions();
     return delegate.allSat(pCallback, pImportant);
   }
+
+  @Override
+  public boolean registerUserPropagator(UserPropagator propagator) {
+    return delegate.registerUserPropagator(propagator);
+  }
 }

src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java

@@ -10,14 +10,18 @@
 
 import static com.google.common.base.Preconditions.checkNotNull;
 
+import com.google.common.collect.ImmutableList;
+import com.google.common.collect.ImmutableMap;
 import java.util.Collection;
 import java.util.List;
 import java.util.Optional;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
 import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.Evaluator;
 import org.sosy_lab.java_smt.api.Model;
 import org.sosy_lab.java_smt.api.SolverException;
+import org.sosy_lab.java_smt.api.UserPropagator;
 
 class DebuggingBasicProverEnvironment<T> implements BasicProverEnvironment<T> {
   private final BasicProverEnvironment<T> delegate;
@@ -29,6 +33,13 @@ class DebuggingBasicProverEnvironment<T> implements BasicProverEnvironment<T> {
     debugging = pDebugging;
   }
 
+  @Override
+  public @Nullable T push(BooleanFormula f) throws InterruptedException {
+    debugging.assertThreadLocal();
+    debugging.assertFormulaInContext(f);
+    return delegate.push(f);
+  }
+
   @Override
   public void pop() {
     debugging.assertThreadLocal();
@@ -77,6 +88,27 @@ public Model getModel() throws SolverException {
     return new DebuggingModel(delegate.getModel(), debugging);
   }
 
+  @SuppressWarnings("resource")
+  @Override
+  public Evaluator getEvaluator() throws SolverException {
+    debugging.assertThreadLocal();
+    return new DebuggingEvaluator(delegate.getEvaluator(), debugging);
+  }
+
+  @Override
+  public ImmutableList<Model.ValueAssignment> getModelAssignments() throws SolverException {
+    debugging.assertThreadLocal();
+    ImmutableList<Model.ValueAssignment> result = delegate.getModelAssignments();
+    for (Model.ValueAssignment v : result) {
+      // Both lines are needed as assignments like "a == false" may have been simplified to
+      // "not(a)" by the solver. This then leads to errors as the term "false" is not defined in
+      // the context.
+      debugging.addFormulaTerm(v.getValueAsFormula());
+      debugging.addFormulaTerm(v.getAssignmentAsFormula());
+    }
+    return result;
+  }
+
   @Override
   public List<BooleanFormula> getUnsatCore() {
     debugging.assertThreadLocal();
@@ -93,6 +125,12 @@ public Optional<List<BooleanFormula>> unsatCoreOverAssumptions(
     return delegate.unsatCoreOverAssumptions(assumptions);
   }
 
+  @Override
+  public ImmutableMap<String, String> getStatistics() {
+    debugging.assertThreadLocal();
+    return delegate.getStatistics();
+  }
+
   @Override
   public void close() {
     debugging.assertThreadLocal();
@@ -108,4 +146,9 @@ public <R> R allSat(AllSatCallback<R> callback, List<BooleanFormula> important)
     }
     return delegate.allSat(callback, important);
   }
+
+  @Override
+  public boolean registerUserPropagator(UserPropagator propagator) {
+    throw new UnsupportedOperationException();
+  }
 }