diff --git a/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java b/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java index 2438e93338..75be1081d4 100644 --- a/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java +++ b/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), diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt index 160c414f39..727f08a1b3 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt +++ b/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> { @@ -189,6 +193,7 @@ constructor( private fun itp(): SafetyResult>? { 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 } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt index 461dc22e37..c6083682aa 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt @@ -40,6 +40,7 @@ fun buildBMC( bmcEnabled, lfPathOnly, null, + null, { false }, null, { false }, @@ -69,6 +70,7 @@ fun buildKIND( bmcEnabled, lfPathOnly, null, + null, { false }, indSolver, kindEnabled, @@ -83,6 +85,7 @@ fun buildIMC( monolithicExpr: MonolithicExpr, bmcSolver: Solver, itpSolver: ItpSolver, + imcFpSolver: Solver, valToState: (Valuation) -> S, biValToAction: (Valuation, Valuation) -> A, logger: Logger, @@ -98,6 +101,7 @@ fun buildIMC( bmcEnabled, lfPathOnly, itpSolver, + imcFpSolver, imcEnabled, null, { false }, diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt index 4820edd81a..0634269e1c 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt +++ b/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, diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolver.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolver.java index fade4d1266..e79e3e6043 100644 --- a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolver.java +++ b/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(); } diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java index 032aeb7e51..e403c30310 100644 --- a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java +++ b/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> 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,6 +167,7 @@ public void push() { @Override public void pop(final int n) { + expCnt -= n; assertions.pop(n); for (int i = 0; i < n; i++) { solver.pop(); @@ -171,6 +175,11 @@ public void pop(final int n) { clearState(); } + @Override + public void popAll() { + pop(expCnt); + } + @Override public void reset() { throw new JavaSMTSolverException("Cannot reset JavaSMT right now."); diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericHornSolver.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericHornSolver.java index a4b43ec7aa..fe52673ad4 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericHornSolver.java +++ b/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> getUnsatCore() { throw new UnsupportedOperationException("This solver cannot return unsat cores"); diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibItpSolver.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibItpSolver.java index 5cc6d9f4ef..f657d3fcc8 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibItpSolver.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibItpSolver.java @@ -61,6 +61,8 @@ public abstract class SmtLibItpSolver 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(); diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java index d4fba45d1f..98797800ed 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java +++ b/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> 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,6 +230,7 @@ public void push() { @Override public void pop(int n) { + expCnt -= n; assertions.pop(n); declarationStack.pop(n); typeStack.pop(n); @@ -234,8 +238,14 @@ public void pop(int n) { clearState(); } + @Override + public void popAll() { + pop(expCnt); + } + @Override public void reset() { + expCnt = 0; issueGeneralCommand("(reset)"); clearState(); init(); diff --git a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3ItpSolver.java b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3ItpSolver.java index b13fa21281..bab40caa7a 100644 --- a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3ItpSolver.java +++ b/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 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,6 +184,7 @@ public void push() { @Override public void pop(final int n) { + expCnt -= n; markers.pop(n); for (final Z3ItpMarker marker : markers) { marker.pop(n); @@ -188,8 +192,14 @@ public void pop(final int n) { solver.pop(n); } + @Override + public void popAll() { + pop(expCnt); + } + @Override public void reset() { + expCnt = 0; solver.reset(); } diff --git a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3Solver.java b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3Solver.java index 49e5dc4ab9..b1dc795649 100644 --- a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3Solver.java +++ b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3Solver.java @@ -59,6 +59,8 @@ final class Z3Solver implements UCSolver, Solver { private Collection> unsatCore; private SolverStatus status; + private int expCnt = 0; + public Z3Solver( final Z3SymbolTable symbolTable, final Z3TransformationManager transformationManager, @@ -128,19 +130,27 @@ private SolverStatus transformStatus(final Status z3Status) { @Override public void push() { + expCnt++; assertions.push(); z3Solver.push(); } @Override public void pop(final int n) { + expCnt -= n; assertions.pop(n); z3Solver.pop(n); clearState(); } + @Override + public void popAll() { + pop(expCnt); + } + @Override public void reset() { + expCnt = 0; z3Solver.reset(); assertions.clear(); assumptions.clear(); diff --git a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java index 349fd5dfa9..1c2ee0083b 100644 --- a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java +++ b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java @@ -74,6 +74,8 @@ final class Z3ItpSolver implements ItpSolver, Solver { private final SmtLibTransformationManager smtLibTransformationManager; private final SmtLibTermTransformer smtLibTermTransformer; + private int expCnt = 0; + public Z3ItpSolver( final Z3SymbolTable symbolTable, final Z3TransformationManager transformationManager, @@ -231,6 +233,7 @@ public SolverStatus check() { @Override public void push() { + expCnt++; markers.push(); for (final Z3ItpMarker marker : markers) { marker.push(); @@ -241,6 +244,7 @@ public void push() { @Override public void pop(final int n) { + expCnt -= n; markers.pop(n); for (final Z3ItpMarker marker : markers) { marker.pop(n); @@ -249,8 +253,14 @@ public void pop(final int n) { solver.pop(n); } + @Override + public void popAll() { + pop(expCnt); + } + @Override public void reset() { + expCnt = 0; solver.reset(); } diff --git a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3Solver.java b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3Solver.java index 6fbf4fac56..95bf9867de 100644 --- a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3Solver.java +++ b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3Solver.java @@ -69,6 +69,8 @@ class Z3Solver implements UCSolver, Solver { protected Collection> unsatCore; protected SolverStatus status; + private int expCnt = 0; + public Z3Solver( final Z3SymbolTable symbolTable, final Z3TransformationManager transformationManager, @@ -138,19 +140,27 @@ private SolverStatus transformStatus(final Status z3Status) { @Override public void push() { + expCnt++; assertions.push(); z3Solver.push(); } @Override public void pop(final int n) { + expCnt -= n; assertions.pop(n); z3Solver.pop(n); clearState(); } + @Override + public void popAll() { + pop(expCnt); + } + @Override public void reset() { + expCnt = 0; z3Solver.reset(); assertions.clear(); assumptions.clear(); diff --git a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/SolverBase.java b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/SolverBase.java index f7a0b6dc55..3414d5091d 100644 --- a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/SolverBase.java +++ b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/SolverBase.java @@ -48,6 +48,9 @@ default void pop() { pop(1); } + /** Remove all expressions added. */ + void popAll(); + /** Reset the solver state. */ void reset(); diff --git a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/impl/NullSolver.java b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/impl/NullSolver.java index 805974bc7d..f19a1493b8 100644 --- a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/impl/NullSolver.java +++ b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/impl/NullSolver.java @@ -55,6 +55,11 @@ public void pop(final int n) { throw new UnsupportedOperationException(); } + @Override + public void popAll() { + throw new UnsupportedOperationException(); + } + @Override public void reset() { throw new UnsupportedOperationException(); diff --git a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/ItpSolverValidatorWrapper.java b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/ItpSolverValidatorWrapper.java index 10298f693c..50c5c1d5d1 100644 --- a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/ItpSolverValidatorWrapper.java +++ b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/ItpSolverValidatorWrapper.java @@ -86,6 +86,11 @@ public void pop(int n) { solver.pop(); } + @Override + public void popAll() { + solver.pop(); + } + @Override public void reset() { solver.reset(); diff --git a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/SolverValidatorWrapper.java b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/SolverValidatorWrapper.java index 682f6b6b84..48f1d54567 100644 --- a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/SolverValidatorWrapper.java +++ b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/SolverValidatorWrapper.java @@ -62,6 +62,11 @@ public void pop(int n) { solver.pop(); } + @Override + public void popAll() { + solver.pop(); + } + @Override public void reset() { solver.reset(); diff --git a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/UCSolverValidatorWrapper.java b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/UCSolverValidatorWrapper.java index 7fb63cd158..e45d4c0199 100644 --- a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/UCSolverValidatorWrapper.java +++ b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/validator/UCSolverValidatorWrapper.java @@ -57,6 +57,11 @@ public void pop(int n) { solver.pop(); } + @Override + public void popAll() { + solver.pop(); + } + @Override public void reset() { solver.reset(); diff --git a/subprojects/solver/solver/src/test/java/hu/bme/mit/theta/solver/SolverStub.java b/subprojects/solver/solver/src/test/java/hu/bme/mit/theta/solver/SolverStub.java index 059afa235e..4e364fa434 100644 --- a/subprojects/solver/solver/src/test/java/hu/bme/mit/theta/solver/SolverStub.java +++ b/subprojects/solver/solver/src/test/java/hu/bme/mit/theta/solver/SolverStub.java @@ -48,6 +48,11 @@ public void pop(final int n) { nPush -= n; } + @Override + public void popAll() { + pop(nPush); + } + @Override public void reset() { // Stub diff --git a/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java b/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java index 90c898bc99..5a13dc8909 100644 --- a/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java +++ b/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java @@ -299,6 +299,7 @@ private STS loadModel() throws Exception { monolithicExpr, abstractionSolverFactory.createSolver(), abstractionSolverFactory.createItpSolver(), + abstractionSolverFactory.createSolver(), val -> StsToMonolithicExprKt.valToState(sts, val), (val1, val2) -> StsToMonolithicExprKt.valToAction(sts, val1, val2), diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt index a0b6f37165..b427868ea0 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt @@ -61,6 +61,9 @@ fun getBoundedChecker( itpSolver = tryGetSolver(boundedConfig.itpConfig.itpSolver, boundedConfig.itpConfig.validateItpSolver) ?.createItpSolver(), + imcFpSolver = + tryGetSolver(boundedConfig.itpConfig.itpSolver, boundedConfig.itpConfig.validateItpSolver) + ?.createSolver(), imcEnabled = { !boundedConfig.itpConfig.disable }, indSolver = tryGetSolver(boundedConfig.indConfig.indSolver, boundedConfig.indConfig.validateIndSolver) diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBounded.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBounded.kt index b6ee960a00..34ba3eeae3 100644 --- a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBounded.kt +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBounded.kt @@ -88,6 +88,7 @@ class XstsCliBounded : monolithicExpr, solverFactory.createSolver(), solverFactory.createItpSolver(), + solverFactory.createSolver(), valToState, biValToAction, logger,