Optimize IMC with Dedicated Solvers for Reachability and Fixed-Point

subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java

@@ -361,6 +361,7 @@ private CFA loadModel() throws Exception {
                                     monolithicExpr,
                                     abstractionSolverFactory.createSolver(),
                                     abstractionSolverFactory.createItpSolver(),
+                                    abstractionSolverFactory.createSolver(),
                                     val -> CfaToMonolithicExprKt.valToState(cfa, val),
                                     (val1, val2) ->
                                             CfaToMonolithicExprKt.valToAction(cfa, val1, val2),

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt

@@ -68,7 +68,8 @@ constructor(
   private val bmcEnabled: () -> Boolean = { bmcSolver != null },
   private val lfPathOnly: () -> Boolean = { true },
   private val itpSolver: ItpSolver? = null,
-  private val imcEnabled: (Int) -> Boolean = { itpSolver != null },
+  private val imcFpSolver: Solver? = null,
+  private val imcEnabled: (Int) -> Boolean = { itpSolver != null && imcFpSolver != null },
   private val indSolver: Solver? = null,
   private val kindEnabled: (Int) -> Boolean = { indSolver != null },
   private val valToState: (Valuation) -> S,
@@ -89,6 +90,9 @@ constructor(
     check(bmcSolver != itpSolver || bmcSolver == null) { "Use distinct solvers for BMC and IMC!" }
     check(bmcSolver != indSolver || bmcSolver == null) { "Use distinct solvers for BMC and KInd!" }
     check(itpSolver != indSolver || itpSolver == null) { "Use distinct solvers for IMC and KInd!" }
+    check((itpSolver == null) == (imcFpSolver == null)) {
+      "Both itpSolver and imcFpSolver must be either null or non-null!"
+    }
   }
 
   override fun check(prec: UnitPrec?): SafetyResult<EmptyProof, Trace<S, A>> {
@@ -189,6 +193,7 @@ constructor(
 
   private fun itp(): SafetyResult<EmptyProof, Trace<S, A>>? {
     val itpSolver = this.itpSolver!!
+    val imcFpSolver = this.imcFpSolver!!
     logger.write(Logger.Level.MAINSTEP, "\tStarting IMC\n")
 
     itpSolver.push()
@@ -199,10 +204,13 @@ constructor(
 
     itpSolver.push()
 
-    itpSolver.add(a, unfoldedInitExpr)
     itpSolver.add(a, exprs[0])
     itpSolver.add(b, exprs.subList(1, exprs.size))
 
+    itpSolver.push()
+
+    itpSolver.add(a, unfoldedInitExpr)
+
     if (lfPathOnly()) { // indices contains currIndex as last()
       itpSolver.push()
       for (indexing in indices) {
@@ -218,23 +226,22 @@ constructor(
       }
 
       if (itpSolver.check().isUnsat) {
-        itpSolver.pop()
-        itpSolver.pop()
+        itpSolver.popAll()
         logger.write(Logger.Level.MAINSTEP, "Safety proven in IMC/BMC step\n")
         return SafetyResult.safe(EmptyProof.getInstance(), BoundedStatistics(iteration))
       }
       itpSolver.pop()
     }
 
+    itpSolver.pop()
     itpSolver.add(b, Not(unfoldedPropExpr(indices.last())))
+    itpSolver.push()
+    itpSolver.add(a, unfoldedInitExpr)
 
-    val status = itpSolver.check()
-
-    if (status.isSat) {
+    if (itpSolver.check().isSat) {
       val trace = getTrace(itpSolver.model)
       logger.write(Logger.Level.MAINSTEP, "CeX found in IMC/BMC step (length ${trace.length()})\n")
-      itpSolver.pop()
-      itpSolver.pop()
+      itpSolver.popAll()
       return SafetyResult.unsafe(trace, EmptyProof.getInstance(), BoundedStatistics(iteration))
     }
 
@@ -243,30 +250,26 @@ constructor(
       val interpolant = itpSolver.getInterpolant(pattern)
       val itpFormula =
         PathUtils.unfold(PathUtils.foldin(interpolant.eval(a), indices[1]), indices[0])
-      itpSolver.pop()
 
-      itpSolver.push()
-      itpSolver.add(a, itpFormula)
-      itpSolver.add(a, Not(img))
-      val itpStatus = itpSolver.check()
-      if (itpStatus.isUnsat) {
+      imcFpSolver.push()
+      imcFpSolver.add(itpFormula)
+      imcFpSolver.add(Not(img))
+      if (imcFpSolver.check().isUnsat) {
         logger.write(Logger.Level.MAINSTEP, "Safety proven in IMC step\n")
-        itpSolver.pop()
-        itpSolver.pop()
+        imcFpSolver.popAll()
+        itpSolver.popAll()
         return SafetyResult.safe(EmptyProof.getInstance(), BoundedStatistics(iteration))
       }
-      itpSolver.pop()
+      imcFpSolver.popAll()
+
       img = Or(img, itpFormula)
 
+      itpSolver.pop()
       itpSolver.push()
       itpSolver.add(a, itpFormula)
-      itpSolver.add(a, exprs[0])
-      itpSolver.add(b, exprs.subList(1, exprs.size))
-      itpSolver.add(b, Not(unfoldedPropExpr(indices.last())))
     }
 
-    itpSolver.pop()
-    itpSolver.pop()
+    itpSolver.popAll()
     return null
   }
 

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt

@@ -40,6 +40,7 @@ fun <S : ExprState, A : ExprAction> buildBMC(
     bmcEnabled,
     lfPathOnly,
     null,
+    null,
     { false },
     null,
     { false },
@@ -69,6 +70,7 @@ fun <S : ExprState, A : ExprAction> buildKIND(
     bmcEnabled,
     lfPathOnly,
     null,
+    null,
     { false },
     indSolver,
     kindEnabled,
@@ -83,6 +85,7 @@ fun <S : ExprState, A : ExprAction> buildIMC(
   monolithicExpr: MonolithicExpr,
   bmcSolver: Solver,
   itpSolver: ItpSolver,
+  imcFpSolver: Solver,
   valToState: (Valuation) -> S,
   biValToAction: (Valuation, Valuation) -> A,
   logger: Logger,
@@ -98,6 +101,7 @@ fun <S : ExprState, A : ExprAction> buildIMC(
     bmcEnabled,
     lfPathOnly,
     itpSolver,
+    imcFpSolver,
     imcEnabled,
     null,
     { false },

subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt

@@ -69,11 +69,13 @@ class BoundedTest {
     val solver = Z3LegacySolverFactory.getInstance().createSolver()
     val itpSolver = Z3LegacySolverFactory.getInstance().createItpSolver()
     val indSolver = Z3LegacySolverFactory.getInstance().createSolver()
+    val fpSolver = Z3LegacySolverFactory.getInstance().createSolver()
     val checker: BoundedChecker<*, *> =
       BoundedChecker(
         monolithicExpr = unsafeMonolithicExpr!!,
         bmcSolver = solver,
         itpSolver = itpSolver,
+        imcFpSolver = fpSolver,
         indSolver = indSolver,
         valToState = valToState,
         biValToAction = biValToAction,
@@ -88,11 +90,13 @@ class BoundedTest {
     val solver = Z3LegacySolverFactory.getInstance().createSolver()
     val itpSolver = Z3LegacySolverFactory.getInstance().createItpSolver()
     val indSolver = Z3LegacySolverFactory.getInstance().createSolver()
+    val fpSolver = Z3LegacySolverFactory.getInstance().createSolver()
     val checker: BoundedChecker<*, *> =
       BoundedChecker(
         monolithicExpr = safeMonolithicExpr!!,
         bmcSolver = solver,
         itpSolver = itpSolver,
+        imcFpSolver = fpSolver,
         indSolver = indSolver,
         valToState = valToState,
         biValToAction = biValToAction,

subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolver.java

@@ -58,6 +58,8 @@ final class JavaSMTItpSolver implements ItpSolver, Solver {
     private final JavaSMTTermTransformer termTransformer;
     private final SolverContext context;
 
+    private int expCnt = 0;
+
     public JavaSMTItpSolver(
             final JavaSMTSymbolTable symbolTable,
             final JavaSMTTransformationManager transformationManager,
@@ -193,6 +195,7 @@ public SolverStatus check() {
 
     @Override
     public void push() {
+        expCnt++;
         markers.push();
         termMap.push();
         for (final JavaSMTItpMarker marker : markers) {
@@ -206,6 +209,7 @@ public void push() {
 
     @Override
     public void pop(final int n) {
+        expCnt -= n;
         markers.pop(n);
         termMap.pop(n);
         for (final JavaSMTItpMarker marker : markers) {
@@ -217,9 +221,15 @@ public void pop(final int n) {
                         .collect(Collectors.toMap(Tuple2::get1, Tuple2::get2));
     }
 
+    @Override
+    public void popAll() {
+        pop(expCnt);
+    }
+
     @Override
     public void reset() {
         solver.reset();
+        expCnt = 0;
         combinedTermMap = Map.of();
     }
 

subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java

@@ -69,6 +69,8 @@ final class JavaSMTSolver implements UCSolver, Solver {
     private final Map<String, Expr<BoolType>> assumptions;
     private SolverStatus status;
 
+    private int expCnt = 0;
+
     public JavaSMTSolver(
             final JavaSMTSymbolTable symbolTable,
             final JavaSMTTransformationManager transformationManager,
@@ -154,6 +156,7 @@ public SolverStatus check() {
 
     @Override
     public void push() {
+        expCnt++;
         assertions.push();
         try {
             solver.push();
@@ -164,13 +167,19 @@ public void push() {
 
     @Override
     public void pop(final int n) {
+        expCnt -= n;
         assertions.pop(n);
         for (int i = 0; i < n; i++) {
             solver.pop();
         }
         clearState();
     }
 
+    @Override
+    public void popAll() {
+        pop(expCnt);
+    }
+
     @Override
     public void reset() {
         throw new JavaSMTSolverException("Cannot reset JavaSMT right now.");

subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericHornSolver.java

@@ -154,6 +154,11 @@ public void pop(int n) {
         throw new UnsupportedOperationException("Pop is not supported.");
     }
 
+    @Override
+    public void popAll() {
+        throw new UnsupportedOperationException("PopAll is not supported.");
+    }
+
     @Override
     public Collection<Expr<BoolType>> getUnsatCore() {
         throw new UnsupportedOperationException("This solver cannot return unsat cores");

subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibItpSolver.java

@@ -61,6 +61,8 @@ public abstract class SmtLibItpSolver<T extends SmtLibItpMarker> implements ItpS
     private Valuation model;
     private SolverStatus status;
 
+    private int expCnt = 0;
+
     public SmtLibItpSolver(
             final SmtLibSymbolTable symbolTable,
             final SmtLibTransformationManager transformationManager,
@@ -172,6 +174,7 @@ public SolverStatus check() {
 
     @Override
     public void push() {
+        expCnt++;
         markers.push();
         for (final var marker : markers) {
             marker.push();
@@ -184,6 +187,7 @@ public void push() {
 
     @Override
     public void pop(final int n) {
+        expCnt -= n;
         markers.pop(n);
         for (final var marker : markers) {
             marker.pop(n);
@@ -195,8 +199,14 @@ public void pop(final int n) {
         clearState();
     }
 
+    @Override
+    public void popAll() {
+        pop(expCnt);
+    }
+
     @Override
     public void reset() {
+        expCnt = 0;
         issueGeneralCommand("(reset)");
         clearState();
         init();

subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java

@@ -72,6 +72,8 @@ public class SmtLibSolver implements UCSolver, Solver {
     protected Collection<Expr<BoolType>> unsatCore;
     protected SolverStatus status;
 
+    private int expCnt = 0;
+
     public SmtLibSolver(
             final SmtLibSymbolTable symbolTable,
             final SmtLibTransformationManager transformationManager,
@@ -219,6 +221,7 @@ public SolverStatus check() {
 
     @Override
     public void push() {
+        expCnt++;
         assertions.push();
         declarationStack.push();
         typeStack.push();
@@ -227,15 +230,22 @@ public void push() {
 
     @Override
     public void pop(int n) {
+        expCnt -= n;
         assertions.pop(n);
         declarationStack.pop(n);
         typeStack.pop(n);
         issueGeneralCommand("(pop 1)");
         clearState();
     }
 
+    @Override
+    public void popAll() {
+        pop(expCnt);
+    }
+
     @Override
     public void reset() {
+        expCnt = 0;
         issueGeneralCommand("(reset)");
         clearState();
         init();

subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3ItpSolver.java

@@ -49,6 +49,8 @@ final class Z3ItpSolver implements ItpSolver, Solver {
 
     private final Stack<Z3ItpMarker> markers;
 
+    private int expCnt = 0;
+
     public Z3ItpSolver(
             final Z3SymbolTable symbolTable,
             final Z3TransformationManager transformationManager,
@@ -172,6 +174,7 @@ public SolverStatus check() {
 
     @Override
     public void push() {
+        expCnt++;
         markers.push();
         for (final Z3ItpMarker marker : markers) {
             marker.push();
@@ -181,15 +184,22 @@ public void push() {
 
     @Override
     public void pop(final int n) {
+        expCnt -= n;
         markers.pop(n);
         for (final Z3ItpMarker marker : markers) {
             marker.pop(n);
         }
         solver.pop(n);
     }
 
+    @Override
+    public void popAll() {
+        pop(expCnt);
+    }
+
     @Override
     public void reset() {
+        expCnt = 0;
         solver.reset();
     }