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 f4360af0f2..8af9a4dbc1 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,7 @@ constructor( private val bmcEnabled: () -> Boolean = { bmcSolver != null }, private val lfPathOnly: () -> Boolean = { true }, private val itpSolver: ItpSolver? = null, - private val imcFpSolver: Solver? = 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 }, @@ -90,6 +90,7 @@ 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> { @@ -190,7 +191,7 @@ constructor( private fun itp(): SafetyResult>? { val itpSolver = this.itpSolver!! - val imcFpSolver = this.imcFpSolver!! + val imcFpSolver = this.imcFpSolver!! logger.write(Logger.Level.MAINSTEP, "\tStarting IMC\n") itpSolver.push(); @@ -204,9 +205,9 @@ constructor( itpSolver.add(a, exprs[0]) itpSolver.add(b, exprs.subList(1, exprs.size)) - itpSolver.push(); + itpSolver.push(); - itpSolver.add(a, unfoldedInitExpr) + itpSolver.add(a, unfoldedInitExpr) if (lfPathOnly()) { // indices contains currIndex as last() itpSolver.push() @@ -223,22 +224,22 @@ constructor( } if (itpSolver.check().isUnsat) { - itpSolver.popAll(); + 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.pop() itpSolver.add(b, Not(unfoldedPropExpr(indices.last()))) - itpSolver.push() - itpSolver.add(a, unfoldedInitExpr) + itpSolver.push() + itpSolver.add(a, unfoldedInitExpr) 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.popAll() + itpSolver.popAll() return SafetyResult.unsafe(trace, EmptyProof.getInstance(), BoundedStatistics(iteration)) } @@ -247,26 +248,26 @@ constructor( val interpolant = itpSolver.getInterpolant(pattern) val itpFormula = PathUtils.unfold(PathUtils.foldin(interpolant.eval(a), indices[1]), indices[0]) - - imcFpSolver.push() - imcFpSolver.add(itpFormula) - imcFpSolver.add(Not(img)) - if (imcFpSolver.check().isUnsat) { - logger.write(Logger.Level.MAINSTEP, "Safety proven in IMC step\n") - imcFpSolver.popAll() - itpSolver.popAll() - return SafetyResult.safe(EmptyProof.getInstance(), BoundedStatistics(iteration)) - } - imcFpSolver.popAll() + + imcFpSolver.push() + imcFpSolver.add(itpFormula) + imcFpSolver.add(Not(img)) + if (imcFpSolver.check().isUnsat) { + logger.write(Logger.Level.MAINSTEP, "Safety proven in IMC step\n") + imcFpSolver.popAll() + itpSolver.popAll() + return SafetyResult.safe(EmptyProof.getInstance(), BoundedStatistics(iteration)) + } + imcFpSolver.popAll() img = Or(img, itpFormula) - - itpSolver.pop(); - itpSolver.push(); - itpSolver.add(a, itpFormula) + + itpSolver.pop(); + itpSolver.push(); + itpSolver.add(a, itpFormula) } - - itpSolver.popAll() + + 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 456047a207..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,7 +40,7 @@ fun buildBMC( bmcEnabled, lfPathOnly, null, - null, + null, { false }, null, { false }, @@ -70,7 +70,7 @@ fun buildKIND( bmcEnabled, lfPathOnly, null, - null, + null, { false }, indSolver, kindEnabled, @@ -85,7 +85,7 @@ fun buildIMC( monolithicExpr: MonolithicExpr, bmcSolver: Solver, itpSolver: ItpSolver, - imcFpSolver: Solver, + imcFpSolver: Solver, valToState: (Valuation) -> S, biValToAction: (Valuation, Valuation) -> A, logger: Logger, @@ -101,7 +101,7 @@ fun buildIMC( bmcEnabled, lfPathOnly, itpSolver, - imcFpSolver, + 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 1f3fd4a179..ea4e37f936 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,13 +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 fpSolver = Z3LegacySolverFactory.getInstance().createSolver() val checker: BoundedChecker<*, *> = BoundedChecker( monolithicExpr = unsafeMonolithicExpr!!, bmcSolver = solver, itpSolver = itpSolver, - imcFpSolver = fpSolver, + imcFpSolver = fpSolver, indSolver = indSolver, valToState = valToState, biValToAction = biValToAction, @@ -90,13 +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 fpSolver = Z3LegacySolverFactory.getInstance().createSolver() val checker: BoundedChecker<*, *> = BoundedChecker( monolithicExpr = safeMonolithicExpr!!, bmcSolver = solver, itpSolver = itpSolver, - imcFpSolver = fpSolver, + 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 3ced7f6dc5..cf9e567e4e 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 @@ -57,8 +57,8 @@ final class JavaSMTItpSolver implements ItpSolver, Solver { private final JavaSMTTermTransformer termTransformer; private final SolverContext context; - - private int expCnt = 0; + + private int expCnt = 0; public JavaSMTItpSolver( final JavaSMTSymbolTable symbolTable, @@ -195,7 +195,7 @@ public SolverStatus check() { @Override public void push() { - expCnt++; + expCnt++; markers.push(); termMap.push(); for (final JavaSMTItpMarker marker : markers) { @@ -209,7 +209,7 @@ public void push() { @Override public void pop(final int n) { - expCnt-=n; + expCnt-=n; markers.pop(n); termMap.pop(n); for (final JavaSMTItpMarker marker : markers) { @@ -221,15 +221,15 @@ public void pop(final int n) { .collect(Collectors.toMap(Tuple2::get1, Tuple2::get2)); } - @Override - public void popAll() { - pop(expCnt); - } + @Override + public void popAll() { + pop(expCnt); + } @Override public void reset() { solver.reset(); - expCnt = 0; + 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 697d1c36e2..5f86b2b07e 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,7 +69,7 @@ final class JavaSMTSolver implements UCSolver, Solver { private final Map> assumptions; private SolverStatus status; - private int expCnt = 0; + private int expCnt = 0; public JavaSMTSolver( final JavaSMTSymbolTable symbolTable, @@ -156,7 +156,7 @@ public SolverStatus check() { @Override public void push() { - expCnt++; + expCnt++; assertions.push(); try { solver.push(); @@ -167,18 +167,18 @@ public void push() { @Override public void pop(final int n) { - expCnt-=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 popAll() { + pop(expCnt); + } @Override public void reset() { 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 96558aa6c5..759bc332e7 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,7 +74,7 @@ final class Z3ItpSolver implements ItpSolver, Solver { private final SmtLibTransformationManager smtLibTransformationManager; private final SmtLibTermTransformer smtLibTermTransformer; - private int expCnt = 0; + private int expCnt = 0; public Z3ItpSolver( final Z3SymbolTable symbolTable, @@ -233,7 +233,7 @@ public SolverStatus check() { @Override public void push() { - expCnt++; + expCnt++; markers.push(); for (final Z3ItpMarker marker : markers) { marker.push(); @@ -244,7 +244,7 @@ public void push() { @Override public void pop(final int n) { - expCnt += n; + expCnt += n; markers.pop(n); for (final Z3ItpMarker marker : markers) { marker.pop(n); @@ -253,14 +253,14 @@ public void pop(final int n) { solver.pop(n); } - @Override - public void popAll() { - pop(expCnt); - } + @Override + public void popAll() { + pop(expCnt); + } @Override public void reset() { - expCnt = 0; + 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 8591b138b5..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,7 +69,7 @@ class Z3Solver implements UCSolver, Solver { protected Collection> unsatCore; protected SolverStatus status; - private int expCnt = 0; + private int expCnt = 0; public Z3Solver( final Z3SymbolTable symbolTable, @@ -140,27 +140,27 @@ private SolverStatus transformStatus(final Status z3Status) { @Override public void push() { - expCnt++; + expCnt++; assertions.push(); z3Solver.push(); } @Override public void pop(final int n) { - expCnt -= n; + expCnt -= n; assertions.pop(n); z3Solver.pop(n); clearState(); } - @Override - public void popAll() { - pop(expCnt); - } + @Override + public void popAll() { + pop(expCnt); + } @Override public void reset() { - expCnt = 0; + 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 bff145624b..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 @@ -49,7 +49,7 @@ default void pop() { } /** Remove all expressions added. */ - void popAll(); + 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 48cdc4dad2..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 @@ -54,12 +54,12 @@ public void push() { public void pop(final int n) { throw new UnsupportedOperationException(); } - - @Override - public void popAll() { + + @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 28a6557a31..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,10 +86,10 @@ public void pop(int n) { solver.pop(); } - @Override - public void popAll() { - solver.pop(); - } + @Override + public void popAll() { + solver.pop(); + } @Override public void 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 8480c3959d..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,10 +62,10 @@ public void pop(int n) { solver.pop(); } - @Override - public void popAll() { - solver.pop(); - } + @Override + public void popAll() { + solver.pop(); + } @Override public void 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 e86eb2ba41..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,10 +57,10 @@ public void pop(int n) { solver.pop(); } - @Override - public void popAll() { - solver.pop(); - } + @Override + public void popAll() { + solver.pop(); + } @Override public void 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 447073244c..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,10 +48,10 @@ public void pop(final int n) { nPush -= n; } - @Override - public void popAll() { - pop(nPush); - } + @Override + public void popAll() { + pop(nPush); + } @Override public void reset() { 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 80152e0539..10f6162a58 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,7 +61,7 @@ fun getBoundedChecker( itpSolver = tryGetSolver(boundedConfig.itpConfig.itpSolver, boundedConfig.itpConfig.validateItpSolver) ?.createItpSolver(), - imcFpSolver = + imcFpSolver = tryGetSolver(boundedConfig.itpConfig.itpSolver, boundedConfig.itpConfig.validateItpSolver) ?.createSolver(), imcEnabled = { !boundedConfig.itpConfig.disable },