Skip to content

Commit

Permalink
Fixed indenting issues and added checking for itpSolver & imcFpSolver
Browse files Browse the repository at this point in the history
  • Loading branch information
@KlevisImeri
KlevisImeri committed Jan 28, 2025
1 parent 9a8aca4 commit 83db5d0
Show file tree
Hide file tree
Showing 14 changed files with 91 additions and 90 deletions.
53 changes: 27 additions & 26 deletions ...mmon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 },
Expand All @@ -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<EmptyProof, Trace<S, A>> {
Expand Down Expand Up @@ -190,7 +191,7 @@ constructor(

private fun itp(): SafetyResult<EmptyProof, Trace<S, A>>? {
val itpSolver = this.itpSolver!!
val imcFpSolver = this.imcFpSolver!!
val imcFpSolver = this.imcFpSolver!!
logger.write(Logger.Level.MAINSTEP, "\tStarting IMC\n")

itpSolver.push();
Expand All @@ -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()
Expand All @@ -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))
}

Expand All @@ -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
}

Expand Down
8 changes: 4 additions & 4 deletions ...alysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ fun <S : ExprState, A : ExprAction> buildBMC(
bmcEnabled,
lfPathOnly,
null,
null,
null,
{ false },
null,
{ false },
Expand Down Expand Up @@ -70,7 +70,7 @@ fun <S : ExprState, A : ExprAction> buildKIND(
bmcEnabled,
lfPathOnly,
null,
null,
null,
{ false },
indSolver,
kindEnabled,
Expand All @@ -85,7 +85,7 @@ fun <S : ExprState, A : ExprAction> buildIMC(
monolithicExpr: MonolithicExpr,
bmcSolver: Solver,
itpSolver: ItpSolver,
imcFpSolver: Solver,
imcFpSolver: Solver,
valToState: (Valuation) -> S,
biValToAction: (Valuation, Valuation) -> A,
logger: Logger,
Expand All @@ -101,7 +101,7 @@ fun <S : ExprState, A : ExprAction> buildIMC(
bmcEnabled,
lfPathOnly,
itpSolver,
imcFpSolver,
imcFpSolver,
imcEnabled,
null,
{ false },
Expand Down
8 changes: 4 additions & 4 deletions subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand All @@ -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,
Expand Down
18 changes: 9 additions & 9 deletions ...solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -195,7 +195,7 @@ public SolverStatus check() {

@Override
public void push() {
expCnt++;
expCnt++;
markers.push();
termMap.push();
for (final JavaSMTItpMarker marker : markers) {
Expand All @@ -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) {
Expand All @@ -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();
}

Expand Down
16 changes: 8 additions & 8 deletions ...ts/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,7 @@ final class JavaSMTSolver implements UCSolver, Solver {
private final Map<String, Expr<BoolType>> assumptions;
private SolverStatus status;

private int expCnt = 0;
private int expCnt = 0;

public JavaSMTSolver(
final JavaSMTSymbolTable symbolTable,
Expand Down Expand Up @@ -156,7 +156,7 @@ public SolverStatus check() {

@Override
public void push() {
expCnt++;
expCnt++;
assertions.push();
try {
solver.push();
Expand All @@ -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() {
Expand Down
16 changes: 8 additions & 8 deletions subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -233,7 +233,7 @@ public SolverStatus check() {

@Override
public void push() {
expCnt++;
expCnt++;
markers.push();
for (final Z3ItpMarker marker : markers) {
marker.push();
Expand All @@ -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);
Expand All @@ -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();
}

Expand Down
16 changes: 8 additions & 8 deletions subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3Solver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,7 @@ class Z3Solver implements UCSolver, Solver {
protected Collection<Expr<BoolType>> unsatCore;
protected SolverStatus status;

private int expCnt = 0;
private int expCnt = 0;

public Z3Solver(
final Z3SymbolTable symbolTable,
Expand Down Expand Up @@ -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();
Expand Down
2 changes: 1 addition & 1 deletion subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/SolverBase.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ default void pop() {
}

/** Remove all expressions added. */
void popAll();
void popAll();

/** Reset the solver state. */
void reset();
Expand Down
10 changes: 5 additions & 5 deletions subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/impl/NullSolver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down
Loading

0 comments on commit 83db5d0

Please sign in to comment.