From ad4e437a0aed1be2909c4ed12f7c45c40711c290 Mon Sep 17 00:00:00 2001 From: Klevis Imeri Date: Wed, 29 Jan 2025 23:43:56 +0100 Subject: [PATCH] style: apply spotless code formatting --- .../algorithm/bounded/BoundedChecker.kt | 18 +++++++++-------- .../theta/analysis/algorithm/BoundedTest.kt | 4 ++-- .../solver/javasmt/JavaSMTItpSolver.java | 8 ++++---- .../theta/solver/javasmt/JavaSMTSolver.java | 4 ++-- .../solver/smtlib/solver/SmtLibSolver.java | 2 +- .../theta/solver/z3legacy/Z3ItpSolver.java | 20 +++++++++---------- .../mit/theta/solver/z3legacy/Z3Solver.java | 16 +++++++-------- .../cli/checkers/ConfigToBoundedChecker.kt | 2 +- 8 files changed, 38 insertions(+), 36 deletions(-) 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 8af9a4dbc1..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 @@ -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, @@ -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> { @@ -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) @@ -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)) } @@ -262,8 +264,8 @@ constructor( img = Or(img, itpFormula) - itpSolver.pop(); - itpSolver.push(); + itpSolver.pop() + itpSolver.push() itpSolver.add(a, itpFormula) } 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 ea4e37f936..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,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!!, @@ -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!!, 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 cf9e567e4e..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 @@ -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, @@ -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,7 +221,7 @@ public void pop(final int n) { .collect(Collectors.toMap(Tuple2::get1, Tuple2::get2)); } - @Override + @Override public void popAll() { pop(expCnt); } 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 5f86b2b07e..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 @@ -167,7 +167,7 @@ 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(); @@ -175,7 +175,7 @@ public void pop(final int n) { clearState(); } - @Override + @Override public void popAll() { pop(expCnt); } 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 8256a24f06..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 @@ -237,7 +237,7 @@ public void pop(int n) { issueGeneralCommand("(pop 1)"); clearState(); } - + @Override public void popAll() { pop(expCnt); 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 6c73d9081e..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 @@ -48,9 +48,9 @@ final class Z3ItpSolver implements ItpSolver, Solver { private final Z3Solver solver; private final Stack markers; - - private int expCnt = 0; - + + private int expCnt = 0; + public Z3ItpSolver( final Z3SymbolTable symbolTable, final Z3TransformationManager transformationManager, @@ -174,7 +174,7 @@ public SolverStatus check() { @Override public void push() { - expCnt++; + expCnt++; markers.push(); for (final Z3ItpMarker marker : markers) { marker.push(); @@ -184,7 +184,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); @@ -192,14 +192,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-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 87dc92d851..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,7 +59,7 @@ final class Z3Solver implements UCSolver, Solver { private Collection> unsatCore; private SolverStatus status; - private int expCnt = 0; + private int expCnt = 0; public Z3Solver( final Z3SymbolTable symbolTable, @@ -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(); 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 10f6162a58..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 @@ -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)