Skip to content

Commit

Permalink
style: apply spotless code formatting
Browse files Browse the repository at this point in the history
  • Loading branch information
@KlevisImeri
KlevisImeri committed Jan 29, 2025
1 parent 83db5d0 commit ad4e437
Show file tree
Hide file tree
Showing 8 changed files with 38 additions and 36 deletions.
18 changes: 10 additions & 8 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 @@ -69,7 +69,7 @@ constructor(
private val lfPathOnly: () -> Boolean = { true },
private val itpSolver: ItpSolver? = null,
private val imcFpSolver: Solver? = null,
private val imcEnabled: (Int) -> Boolean = { itpSolver != null && imcFpSolver != 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,
Expand All @@ -90,7 +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!" }
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 @@ -194,18 +196,18 @@ constructor(
val imcFpSolver = this.imcFpSolver!!
logger.write(Logger.Level.MAINSTEP, "\tStarting IMC\n")

itpSolver.push();
itpSolver.push()

val a = itpSolver.createMarker()
val b = itpSolver.createMarker()
val pattern = itpSolver.createBinPattern(a, b)

itpSolver.push();
itpSolver.push()

itpSolver.add(a, exprs[0])
itpSolver.add(b, exprs.subList(1, exprs.size))

itpSolver.push();
itpSolver.push()

itpSolver.add(a, unfoldedInitExpr)

Expand All @@ -224,7 +226,7 @@ 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))
}
Expand Down Expand Up @@ -262,8 +264,8 @@ constructor(

img = Or(img, itpFormula)

itpSolver.pop();
itpSolver.push();
itpSolver.pop()
itpSolver.push()
itpSolver.add(a, itpFormula)
}

Expand Down
4 changes: 2 additions & 2 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,7 +69,7 @@ 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!!,
Expand All @@ -90,7 +90,7 @@ 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!!,
Expand Down
8 changes: 4 additions & 4 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 @@ -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,7 +221,7 @@ public void pop(final int n) {
.collect(Collectors.toMap(Tuple2::get1, Tuple2::get2));
}

@Override
@Override
public void popAll() {
pop(expCnt);
}
Expand Down
4 changes: 2 additions & 2 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 @@ -167,15 +167,15 @@ 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
@Override
public void popAll() {
pop(expCnt);
}
Expand Down
2 changes: 1 addition & 1 deletion ...olver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -237,7 +237,7 @@ public void pop(int n) {
issueGeneralCommand("(pop 1)");
clearState();
}

@Override
public void popAll() {
pop(expCnt);
Expand Down
20 changes: 10 additions & 10 deletions ...s/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3ItpSolver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,9 +48,9 @@ final class Z3ItpSolver implements ItpSolver, Solver {
private final Z3Solver solver;

private final Stack<Z3ItpMarker> markers;
private int expCnt = 0;

private int expCnt = 0;

public Z3ItpSolver(
final Z3SymbolTable symbolTable,
final Z3TransformationManager transformationManager,
Expand Down Expand Up @@ -174,7 +174,7 @@ public SolverStatus check() {

@Override
public void push() {
expCnt++;
expCnt++;
markers.push();
for (final Z3ItpMarker marker : markers) {
marker.push();
Expand All @@ -184,22 +184,22 @@ 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);
}
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 ...ects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3Solver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ final class Z3Solver implements UCSolver, Solver {
private Collection<Expr<BoolType>> unsatCore;
private SolverStatus status;

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

public Z3Solver(
final Z3SymbolTable symbolTable,
Expand Down Expand Up @@ -130,27 +130,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 .../xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,7 @@ fun getBoundedChecker(
?.createItpSolver(),
imcFpSolver =
tryGetSolver(boundedConfig.itpConfig.itpSolver, boundedConfig.itpConfig.validateItpSolver)
?.createSolver(),
?.createSolver(),
imcEnabled = { !boundedConfig.itpConfig.disable },
indSolver =
tryGetSolver(boundedConfig.indConfig.indSolver, boundedConfig.indConfig.validateIndSolver)
Expand Down

0 comments on commit ad4e437

Please sign in to comment.