, CfaAction, CfaPrec> getRefiner(BuilderStrategy builderStrategy) {
- return SingleExprTraceRefiner.create(ExprTraceFwBinItpChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createItpSolver()), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+ public
+ ArgRefiner, CfaAction, CfaPrec> getRefiner(
+ BuilderStrategy builderStrategy) {
+ return SingleExprTraceRefiner.create(
+ ExprTraceFwBinItpChecker.create(
+ True(),
+ True(),
+ builderStrategy.getRefinementSolverFactory().createItpSolver()),
+ builderStrategy
+ .getPrecGranularity()
+ .createRefiner(builderStrategy.getItpRefToPrec()),
+ builderStrategy.getPruneStrategy(),
+ builderStrategy.getLogger());
}
- }, BW_BIN_ITP {
+ },
+ BW_BIN_ITP {
@Override
- public Refiner, CfaAction, CfaPrec> getRefiner(BuilderStrategy builderStrategy) {
- return SingleExprTraceRefiner.create(ExprTraceBwBinItpChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createItpSolver()), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+ public
+ ArgRefiner, CfaAction, CfaPrec> getRefiner(
+ BuilderStrategy builderStrategy) {
+ return SingleExprTraceRefiner.create(
+ ExprTraceBwBinItpChecker.create(
+ True(),
+ True(),
+ builderStrategy.getRefinementSolverFactory().createItpSolver()),
+ builderStrategy
+ .getPrecGranularity()
+ .createRefiner(builderStrategy.getItpRefToPrec()),
+ builderStrategy.getPruneStrategy(),
+ builderStrategy.getLogger());
}
- }, SEQ_ITP {
+ },
+ SEQ_ITP {
@Override
- public Refiner, CfaAction, CfaPrec> getRefiner(BuilderStrategy builderStrategy) {
- return SingleExprTraceRefiner.create(ExprTraceSeqItpChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createItpSolver()), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+ public
+ ArgRefiner, CfaAction, CfaPrec> getRefiner(
+ BuilderStrategy builderStrategy) {
+ return SingleExprTraceRefiner.create(
+ ExprTraceSeqItpChecker.create(
+ True(),
+ True(),
+ builderStrategy.getRefinementSolverFactory().createItpSolver()),
+ builderStrategy
+ .getPrecGranularity()
+ .createRefiner(builderStrategy.getItpRefToPrec()),
+ builderStrategy.getPruneStrategy(),
+ builderStrategy.getLogger());
}
},
MULTI_SEQ {
@@ -187,60 +225,229 @@ public StopCriterion getStopCriterion() {
}
@Override
- public Refiner, CfaAction, CfaPrec> getRefiner(BuilderStrategy builderStrategy) {
- return MultiExprTraceRefiner.create(ExprTraceSeqItpChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createItpSolver()), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+ public
+ ArgRefiner, CfaAction, CfaPrec> getRefiner(
+ BuilderStrategy builderStrategy) {
+ return MultiExprTraceRefiner.create(
+ ExprTraceSeqItpChecker.create(
+ True(),
+ True(),
+ builderStrategy.getRefinementSolverFactory().createItpSolver()),
+ builderStrategy
+ .getPrecGranularity()
+ .createRefiner(builderStrategy.getItpRefToPrec()),
+ builderStrategy.getPruneStrategy(),
+ builderStrategy.getLogger());
}
},
UNSAT_CORE {
@Override
- public Refiner, CfaAction, CfaPrec> getRefiner(BuilderStrategy builderStrategy) {
- return SingleExprTraceRefiner.create(ExprTraceUnsatCoreChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getVarsRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+ public
+ ArgRefiner, CfaAction, CfaPrec> getRefiner(
+ BuilderStrategy builderStrategy) {
+ return SingleExprTraceRefiner.create(
+ ExprTraceUnsatCoreChecker.create(
+ True(),
+ True(),
+ builderStrategy.getRefinementSolverFactory().createUCSolver()),
+ builderStrategy
+ .getPrecGranularity()
+ .createRefiner(builderStrategy.getVarsRefToPrec()),
+ builderStrategy.getPruneStrategy(),
+ builderStrategy.getLogger());
}
- }, UCB {
+ },
+ UCB {
@Override
- public Refiner, CfaAction, CfaPrec> getRefiner(BuilderStrategy builderStrategy) {
- return SingleExprTraceRefiner.create(ExprTraceUCBChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+ public
+ ArgRefiner, CfaAction, CfaPrec> getRefiner(
+ BuilderStrategy builderStrategy) {
+ return SingleExprTraceRefiner.create(
+ ExprTraceUCBChecker.create(
+ True(),
+ True(),
+ builderStrategy.getRefinementSolverFactory().createUCSolver()),
+ builderStrategy
+ .getPrecGranularity()
+ .createRefiner(builderStrategy.getItpRefToPrec()),
+ builderStrategy.getPruneStrategy(),
+ builderStrategy.getLogger());
}
},
NWT_WP {
@Override
- public Refiner, CfaAction, CfaPrec> getRefiner(BuilderStrategy builderStrategy) {
- return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withoutIT().withSP().withoutLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+ public
+ ArgRefiner, CfaAction, CfaPrec> getRefiner(
+ BuilderStrategy builderStrategy) {
+ return SingleExprTraceRefiner.create(
+ ExprTraceNewtonChecker.create(
+ True(),
+ True(),
+ builderStrategy
+ .getRefinementSolverFactory()
+ .createUCSolver())
+ .withoutIT()
+ .withSP()
+ .withoutLV(),
+ builderStrategy
+ .getPrecGranularity()
+ .createRefiner(builderStrategy.getItpRefToPrec()),
+ builderStrategy.getPruneStrategy(),
+ builderStrategy.getLogger());
}
- }, NWT_SP {
+ },
+ NWT_SP {
@Override
- public Refiner, CfaAction, CfaPrec> getRefiner(BuilderStrategy builderStrategy) {
- return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withoutIT().withWP().withoutLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+ public
+ ArgRefiner, CfaAction, CfaPrec> getRefiner(
+ BuilderStrategy builderStrategy) {
+ return SingleExprTraceRefiner.create(
+ ExprTraceNewtonChecker.create(
+ True(),
+ True(),
+ builderStrategy
+ .getRefinementSolverFactory()
+ .createUCSolver())
+ .withoutIT()
+ .withWP()
+ .withoutLV(),
+ builderStrategy
+ .getPrecGranularity()
+ .createRefiner(builderStrategy.getItpRefToPrec()),
+ builderStrategy.getPruneStrategy(),
+ builderStrategy.getLogger());
}
- }, NWT_WP_LV {
+ },
+ NWT_WP_LV {
@Override
- public Refiner, CfaAction, CfaPrec> getRefiner(BuilderStrategy builderStrategy) {
- return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withoutIT().withWP().withLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+ public
+ ArgRefiner, CfaAction, CfaPrec> getRefiner(
+ BuilderStrategy builderStrategy) {
+ return SingleExprTraceRefiner.create(
+ ExprTraceNewtonChecker.create(
+ True(),
+ True(),
+ builderStrategy
+ .getRefinementSolverFactory()
+ .createUCSolver())
+ .withoutIT()
+ .withWP()
+ .withLV(),
+ builderStrategy
+ .getPrecGranularity()
+ .createRefiner(builderStrategy.getItpRefToPrec()),
+ builderStrategy.getPruneStrategy(),
+ builderStrategy.getLogger());
}
- }, NWT_SP_LV {
+ },
+ NWT_SP_LV {
@Override
- public Refiner, CfaAction, CfaPrec> getRefiner(BuilderStrategy builderStrategy) {
- return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withoutIT().withSP().withLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+ public
+ ArgRefiner, CfaAction, CfaPrec> getRefiner(
+ BuilderStrategy builderStrategy) {
+ return SingleExprTraceRefiner.create(
+ ExprTraceNewtonChecker.create(
+ True(),
+ True(),
+ builderStrategy
+ .getRefinementSolverFactory()
+ .createUCSolver())
+ .withoutIT()
+ .withSP()
+ .withLV(),
+ builderStrategy
+ .getPrecGranularity()
+ .createRefiner(builderStrategy.getItpRefToPrec()),
+ builderStrategy.getPruneStrategy(),
+ builderStrategy.getLogger());
}
- }, NWT_IT_WP {
+ },
+ NWT_IT_WP {
@Override
- public Refiner, CfaAction, CfaPrec> getRefiner(BuilderStrategy builderStrategy) {
- return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withIT().withWP().withoutLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+ public
+ ArgRefiner, CfaAction, CfaPrec> getRefiner(
+ BuilderStrategy builderStrategy) {
+ return SingleExprTraceRefiner.create(
+ ExprTraceNewtonChecker.create(
+ True(),
+ True(),
+ builderStrategy
+ .getRefinementSolverFactory()
+ .createUCSolver())
+ .withIT()
+ .withWP()
+ .withoutLV(),
+ builderStrategy
+ .getPrecGranularity()
+ .createRefiner(builderStrategy.getItpRefToPrec()),
+ builderStrategy.getPruneStrategy(),
+ builderStrategy.getLogger());
}
- }, NWT_IT_SP {
+ },
+ NWT_IT_SP {
@Override
- public Refiner, CfaAction, CfaPrec> getRefiner(BuilderStrategy builderStrategy) {
- return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withIT().withSP().withoutLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+ public
+ ArgRefiner, CfaAction, CfaPrec> getRefiner(
+ BuilderStrategy builderStrategy) {
+ return SingleExprTraceRefiner.create(
+ ExprTraceNewtonChecker.create(
+ True(),
+ True(),
+ builderStrategy
+ .getRefinementSolverFactory()
+ .createUCSolver())
+ .withIT()
+ .withSP()
+ .withoutLV(),
+ builderStrategy
+ .getPrecGranularity()
+ .createRefiner(builderStrategy.getItpRefToPrec()),
+ builderStrategy.getPruneStrategy(),
+ builderStrategy.getLogger());
}
- }, NWT_IT_WP_LV {
+ },
+ NWT_IT_WP_LV {
@Override
- public Refiner, CfaAction, CfaPrec> getRefiner(BuilderStrategy builderStrategy) {
- return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withIT().withWP().withLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+ public
+ ArgRefiner, CfaAction, CfaPrec> getRefiner(
+ BuilderStrategy builderStrategy) {
+ return SingleExprTraceRefiner.create(
+ ExprTraceNewtonChecker.create(
+ True(),
+ True(),
+ builderStrategy
+ .getRefinementSolverFactory()
+ .createUCSolver())
+ .withIT()
+ .withWP()
+ .withLV(),
+ builderStrategy
+ .getPrecGranularity()
+ .createRefiner(builderStrategy.getItpRefToPrec()),
+ builderStrategy.getPruneStrategy(),
+ builderStrategy.getLogger());
}
- }, NWT_IT_SP_LV {
+ },
+ NWT_IT_SP_LV {
@Override
- public Refiner, CfaAction, CfaPrec> getRefiner(BuilderStrategy builderStrategy) {
- return SingleExprTraceRefiner.create(ExprTraceNewtonChecker.create(True(), True(), builderStrategy.getRefinementSolverFactory().createUCSolver()).withIT().withSP().withLV(), builderStrategy.getPrecGranularity().createRefiner(builderStrategy.getItpRefToPrec()), builderStrategy.getPruneStrategy(), builderStrategy.getLogger());
+ public
+ ArgRefiner, CfaAction, CfaPrec> getRefiner(
+ BuilderStrategy builderStrategy) {
+ return SingleExprTraceRefiner.create(
+ ExprTraceNewtonChecker.create(
+ True(),
+ True(),
+ builderStrategy
+ .getRefinementSolverFactory()
+ .createUCSolver())
+ .withIT()
+ .withSP()
+ .withLV(),
+ builderStrategy
+ .getPrecGranularity()
+ .createRefiner(builderStrategy.getItpRefToPrec()),
+ builderStrategy.getPruneStrategy(),
+ builderStrategy.getLogger());
}
};
@@ -248,24 +455,25 @@ public StopCriterion getStopCriterion() {
return StopCriterions.firstCex();
}
- public abstract Refiner, CfaAction, CfaPrec> getRefiner(BuilderStrategy builderStrategy);
-
+ public abstract
+ ArgRefiner, CfaAction, CfaPrec> getRefiner(
+ BuilderStrategy builderStrategy);
}
public enum Search {
BFS {
@Override
public ArgNodeComparator getComp(final CFA cfa, final CFA.Loc errLoc) {
- return ArgNodeComparators.combine(ArgNodeComparators.targetFirst(),
- ArgNodeComparators.bfs());
+ return ArgNodeComparators.combine(
+ ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs());
}
},
DFS {
@Override
public ArgNodeComparator getComp(final CFA cfa, final CFA.Loc errLoc) {
- return ArgNodeComparators.combine(ArgNodeComparators.targetFirst(),
- ArgNodeComparators.dfs());
+ return ArgNodeComparators.combine(
+ ArgNodeComparators.targetFirst(), ArgNodeComparators.dfs());
}
},
@@ -277,7 +485,6 @@ public ArgNodeComparator getComp(final CFA cfa, final CFA.Loc errLoc) {
};
public abstract ArgNodeComparator getComp(CFA cfa, CFA.Loc errLoc);
-
}
public enum PredSplit {
@@ -302,8 +509,9 @@ public CfaPrec
createPrec(final P innerPrec) {
}
@Override
- public PrecRefiner, A, CfaPrec, R> createRefiner(
- final RefutationToPrec refToPrec) {
+ public
+ PrecRefiner, A, CfaPrec, R> createRefiner(
+ final RefutationToPrec refToPrec) {
return GlobalCfaPrecRefiner.create(refToPrec);
}
@@ -320,8 +528,9 @@ public CfaPrec
createPrec(final P innerPrec) {
}
@Override
- public PrecRefiner, A, CfaPrec, R> createRefiner(
- final RefutationToPrec refToPrec) {
+ public
+ PrecRefiner, A, CfaPrec, R> createRefiner(
+ final RefutationToPrec refToPrec) {
return LocalCfaPrecRefiner.create(refToPrec);
}
@@ -333,8 +542,10 @@ public CfaPrec assumePrecs(CFA cfa) {
public abstract CfaPrec
createPrec(P innerPrec);
- public abstract PrecRefiner, A, CfaPrec, R> createRefiner(
- RefutationToPrec refToPrec);
+ public abstract <
+ S extends ExprState, A extends Action, P extends Prec, R extends Refutation>
+ PrecRefiner, A, CfaPrec, R> createRefiner(
+ RefutationToPrec refToPrec);
public abstract CfaPrec assumePrecs(CFA cfa);
}
@@ -358,19 +569,37 @@ public CfaLts getLts(CFA.Loc errorLoc) {
}
public enum InitPrec {
- EMPTY, ALLVARS, ALLASSUMES
+ EMPTY,
+ ALLVARS,
+ ALLASSUMES
}
public abstract class BuilderStrategy {
- protected static final String UNSUPPORTED_CONFIG_VALUE = "Builder strategy %s does not support configuration value %s as %s";
+ protected static final String UNSUPPORTED_CONFIG_VALUE =
+ "Builder strategy %s does not support configuration value %s as %s";
protected final CFA cfa;
@SuppressWarnings("java:S1699")
protected BuilderStrategy(CFA cfa) {
- checkState(getSupportedDomains().contains(domain), UNSUPPORTED_CONFIG_VALUE, getClass().getSimpleName(), domain, "domain");
- checkState(getSupportedRefinements().contains(refinement), UNSUPPORTED_CONFIG_VALUE, getClass().getSimpleName(), refinement, "refinement");
- checkState(getSupportedInitPrecs().contains(initPrec), UNSUPPORTED_CONFIG_VALUE, getClass().getSimpleName(), initPrec, "initial precision");
+ checkState(
+ getSupportedDomains().contains(domain),
+ UNSUPPORTED_CONFIG_VALUE,
+ getClass().getSimpleName(),
+ domain,
+ "domain");
+ checkState(
+ getSupportedRefinements().contains(refinement),
+ UNSUPPORTED_CONFIG_VALUE,
+ getClass().getSimpleName(),
+ refinement,
+ "refinement");
+ checkState(
+ getSupportedInitPrecs().contains(initPrec),
+ UNSUPPORTED_CONFIG_VALUE,
+ getClass().getSimpleName(),
+ initPrec,
+ "initial precision");
this.cfa = cfa;
}
@@ -389,7 +618,10 @@ public CfaAnalysis getAnalysis() {
public abstract RefutationToPrec getItpRefToPrec();
public RefutationToPrec getVarsRefToPrec() {
- throw new UnsupportedOperationException(String.format("Builder strategy %s can not provide Vars refutation to precision", getClass().getSimpleName()));
+ throw new UnsupportedOperationException(
+ String.format(
+ "Builder strategy %s can not provide Vars refutation to precision",
+ getClass().getSimpleName()));
}
protected SolverFactory getRefinementSolverFactory() {
@@ -421,22 +653,30 @@ public CfaLts getLts() {
public CfaConfig, CfaAction, CfaPrec> buildConfig(CFA.Loc errLoc) {
final Predicate> target = new CfaErrorlocPredicate<>(errLoc);
final Analysis, CfaAction, CfaPrec> analysis = getAnalysis();
- final ArgBuilder, CfaAction, CfaPrec> argBuilder = ArgBuilder.create(
- getLts(errLoc), analysis, target,
- true);
- final Abstractor, CfaAction, CfaPrec> abstractor = BasicAbstractor.builder(
- argBuilder)
- .waitlist(PriorityWaitlist.create(search.getComp(cfa, errLoc)))
- .stopCriterion(refinement.getStopCriterion())
- .logger(logger).build();
- final Refiner, CfaAction, CfaPrec> refiner = refinement.getRefiner(this);
- final SafetyChecker, CfaAction>, Trace, CfaAction>, CfaPrec> checker = CegarChecker.create(
- abstractor, refiner,
- logger);
+ final ArgBuilder, CfaAction, CfaPrec> argBuilder =
+ ArgBuilder.create(getLts(errLoc), analysis, target, true);
+ final ArgAbstractor, CfaAction, CfaPrec> abstractor =
+ BasicArgAbstractor.builder(argBuilder)
+ .waitlist(PriorityWaitlist.create(search.getComp(cfa, errLoc)))
+ .stopCriterion(refinement.getStopCriterion())
+ .logger(logger)
+ .build();
+ final ArgRefiner, CfaAction, CfaPrec> refiner =
+ refinement.getRefiner(this);
+ final SafetyChecker<
+ ARG, CfaAction>, Trace, CfaAction>, CfaPrec>
+ checker = ArgCegarChecker.create(abstractor, refiner, logger);
return CfaConfig.create(checker, createInitPrec());
}
- public MultiAnalysisSide, S, CfaState, CfaAction, CfaPrec, CfaPrec> getMultiSide() {
+ public MultiAnalysisSide<
+ CfaState,
+ S,
+ CfaState,
+ CfaAction,
+ CfaPrec,
+ CfaPrec>
+ getMultiSide() {
return new MultiAnalysisSide<>(
getAnalysis(),
CfaControlInitFuncKt.cfaControlInitFunc(cfa.getInitLoc()),
@@ -470,7 +710,8 @@ public Set getSupportedInitPrecs() {
@Override
public Analysis getDataAnalysis() {
- return ExplStmtAnalysis.create(abstractionSolverFactory.createSolver(), True(), maxEnum);
+ return ExplStmtAnalysis.create(
+ abstractionSolverFactory.createSolver(), True(), maxEnum);
}
@Override
@@ -489,7 +730,12 @@ public CfaPrec createInitPrec() {
case EMPTY -> precGranularity.createPrec(ExplPrec.empty());
case ALLVARS -> precGranularity.createPrec(ExplPrec.of(cfa.getVars()));
default ->
- throw new UnsupportedOperationException(String.format(UNSUPPORTED_CONFIG_VALUE, getClass().getSimpleName(), initPrec, "initial precision"));
+ throw new UnsupportedOperationException(
+ String.format(
+ UNSUPPORTED_CONFIG_VALUE,
+ getClass().getSimpleName(),
+ initPrec,
+ "initial precision"));
};
}
}
@@ -520,8 +766,7 @@ public Set getSupportedRefinements() {
Refinement.NWT_IT_SP,
Refinement.NWT_IT_WP,
Refinement.NWT_IT_SP_LV,
- Refinement.NWT_IT_WP_LV
- );
+ Refinement.NWT_IT_WP_LV);
}
@Override
@@ -546,9 +791,13 @@ public CfaPrec createInitPrec() {
case EMPTY -> precGranularity.createPrec(PredPrec.of());
case ALLASSUMES -> precGranularity.assumePrecs(cfa);
default ->
- throw new UnsupportedOperationException(String.format(UNSUPPORTED_CONFIG_VALUE, getClass().getSimpleName(), initPrec, "initial precision"));
+ throw new UnsupportedOperationException(
+ String.format(
+ UNSUPPORTED_CONFIG_VALUE,
+ getClass().getSimpleName(),
+ initPrec,
+ "initial precision"));
};
}
}
-
}
diff --git a/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java b/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java
index 4204a3785d..111600967f 100644
--- a/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java
+++ b/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java
@@ -17,60 +17,65 @@
import static org.junit.Assert.assertTrue;
-import java.io.FileInputStream;
-import java.io.FileNotFoundException;
-import java.io.IOException;
-
import hu.bme.mit.theta.analysis.Trace;
import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
-import hu.bme.mit.theta.analysis.pred.PredState;
-import hu.bme.mit.theta.cfa.analysis.CfaAction;
-import hu.bme.mit.theta.cfa.analysis.CfaState;
-import hu.bme.mit.theta.solver.Solver;
-import org.junit.Test;
-
import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
import hu.bme.mit.theta.analysis.algorithm.arg.ArgChecker;
import hu.bme.mit.theta.analysis.expr.ExprAction;
import hu.bme.mit.theta.analysis.expr.ExprState;
+import hu.bme.mit.theta.analysis.pred.PredState;
import hu.bme.mit.theta.analysis.unit.UnitPrec;
import hu.bme.mit.theta.analysis.utils.ArgVisualizer;
import hu.bme.mit.theta.cfa.CFA;
+import hu.bme.mit.theta.cfa.analysis.CfaAction;
+import hu.bme.mit.theta.cfa.analysis.CfaState;
import hu.bme.mit.theta.cfa.analysis.lts.CfaLbeLts;
import hu.bme.mit.theta.cfa.dsl.CfaDslManager;
import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter;
import hu.bme.mit.theta.solver.ItpSolver;
+import hu.bme.mit.theta.solver.Solver;
import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory;
+import java.io.FileInputStream;
+import java.io.FileNotFoundException;
+import java.io.IOException;
+import org.junit.Test;
public final class CfaPredImpactCheckerTest {
@Test
public void test() throws FileNotFoundException, IOException {
// Arrange
- final CFA cfa = CfaDslManager.createCfa(
- new FileInputStream("src/test/resources/counter5_true.cfa"));
+ final CFA cfa =
+ CfaDslManager.createCfa(
+ new FileInputStream("src/test/resources/counter5_true.cfa"));
final Solver abstractionSolver = Z3LegacySolverFactory.getInstance().createSolver();
final ItpSolver refinementSolver = Z3LegacySolverFactory.getInstance().createItpSolver();
- final PredImpactChecker checker = PredImpactChecker.create(
- CfaLbeLts.of(cfa.getErrorLoc().get()), cfa.getInitLoc(),
- l -> l.equals(cfa.getErrorLoc().get()), abstractionSolver, refinementSolver);
+ final PredImpactChecker checker =
+ PredImpactChecker.create(
+ CfaLbeLts.of(cfa.getErrorLoc().get()),
+ cfa.getInitLoc(),
+ l -> l.equals(cfa.getErrorLoc().get()),
+ abstractionSolver,
+ refinementSolver);
// Act
- final SafetyResult, CfaAction>, Trace, CfaAction>> status = checker.check(
- UnitPrec.getInstance());
+ final SafetyResult<
+ ARG, CfaAction>, Trace, CfaAction>>
+ status = checker.check(UnitPrec.getInstance());
// Assert
assertTrue(status.isSafe());
- final ARG arg = status.getWitness();
+ final ARG arg = status.getProof();
arg.minimize();
final ArgChecker argChecker = ArgChecker.create(abstractionSolver);
assertTrue(argChecker.isWellLabeled(arg));
System.out.println(
- GraphvizWriter.getInstance().writeString(ArgVisualizer.getDefault().visualize(arg)));
+ GraphvizWriter.getInstance()
+ .writeString(ArgVisualizer.getDefault().visualize(arg)));
}
-}
\ No newline at end of file
+}
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 024911743e..eda6c15702 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
@@ -15,6 +15,8 @@
*/
package hu.bme.mit.theta.cfa.cli;
+import static com.google.common.base.Preconditions.checkNotNull;
+
import com.beust.jcommander.JCommander;
import com.beust.jcommander.Parameter;
import com.beust.jcommander.ParameterException;
@@ -27,8 +29,6 @@
import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr;
import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics;
import hu.bme.mit.theta.analysis.expl.ExplState;
-import hu.bme.mit.theta.analysis.expr.ExprAction;
-import hu.bme.mit.theta.analysis.expr.ExprState;
import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy;
import hu.bme.mit.theta.cfa.CFA;
import hu.bme.mit.theta.cfa.analysis.CfaAction;
@@ -37,14 +37,7 @@
import hu.bme.mit.theta.cfa.analysis.CfaTraceConcretizer;
import hu.bme.mit.theta.cfa.analysis.config.CfaConfig;
import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder;
-import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Algorithm;
-import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Domain;
-import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Encoding;
-import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.InitPrec;
-import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.PrecGranularity;
-import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.PredSplit;
-import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Refinement;
-import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Search;
+import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.*;
import hu.bme.mit.theta.cfa.analysis.utils.CfaVisualizer;
import hu.bme.mit.theta.cfa.dsl.CfaDslManager;
import hu.bme.mit.theta.common.CliUtils;
@@ -62,28 +55,21 @@
import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager;
import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory;
import hu.bme.mit.theta.solver.z3legacy.Z3SolverManager;
-
-import java.io.File;
-import java.io.FileInputStream;
-import java.io.FileNotFoundException;
-import java.io.InputStream;
-import java.io.PrintWriter;
-import java.io.StringWriter;
+import java.io.*;
import java.nio.file.Path;
import java.util.concurrent.TimeUnit;
import java.util.stream.Stream;
-import static com.google.common.base.Preconditions.checkNotNull;
-
-/**
- * A command line interface for running a CEGAR configuration on a CFA.
- */
+/** A command line interface for running a CEGAR configuration on a CFA. */
public class CfaCli {
private static final String JAR_NAME = "theta-cfa-cli.jar";
private final String[] args;
private final TableWriter writer;
- @Parameter(names = {"--algorithm"}, description = "Algorithm")
+
+ @Parameter(
+ names = {"--algorithm"},
+ description = "Algorithm")
Algorithm algorithm = Algorithm.CEGAR;
@Parameter(names = "--domain", description = "Abstract domain")
@@ -95,16 +81,34 @@ public class CfaCli {
@Parameter(names = "--search", description = "Search strategy")
Search search = Search.BFS;
- @Parameter(names = "--predsplit", description = "Predicate splitting (for predicate abstraction)")
+ @Parameter(
+ names = "--predsplit",
+ description = "Predicate splitting (for predicate abstraction)")
PredSplit predSplit = PredSplit.WHOLE;
- @Parameter(names = "--solver", description = "Sets the underlying SMT solver to use for both the abstraction and the refinement process. Enter in format :, see theta-smtlib-cli.jar for more details. Enter \"Z3\" to use the legacy z3 solver.")
+ @Parameter(
+ names = "--solver",
+ description =
+ "Sets the underlying SMT solver to use for both the abstraction and the"
+ + " refinement process. Enter in format :, see"
+ + " theta-smtlib-cli.jar for more details. Enter \"Z3\" to use the legacy"
+ + " z3 solver.")
String solver = "Z3";
- @Parameter(names = "--abstraction-solver", description = "Sets the underlying SMT solver to use for the abstraction process. Enter in format :, see theta-smtlib-cli.jar for more details. Enter \"Z3\" to use the legacy z3 solver.")
+ @Parameter(
+ names = "--abstraction-solver",
+ description =
+ "Sets the underlying SMT solver to use for the abstraction process. Enter in"
+ + " format :, see theta-smtlib-cli.jar for"
+ + " more details. Enter \"Z3\" to use the legacy z3 solver.")
String abstractionSolver;
- @Parameter(names = "--refinement-solver", description = "Sets the underlying SMT solver to use for the refinement process. Enter in format :, see theta-smtlib-cli.jar for more details. Enter \"Z3\" to use the legacy z3 solver.")
+ @Parameter(
+ names = "--refinement-solver",
+ description =
+ "Sets the underlying SMT solver to use for the refinement process. Enter in"
+ + " format :, see theta-smtlib-cli.jar for"
+ + " more details. Enter \"Z3\" to use the legacy z3 solver.")
String refinementSolver;
@Parameter(names = "--home", description = "The path of the solver registry")
@@ -122,13 +126,17 @@ public class CfaCli {
@Parameter(names = "--encoding", description = "Block encoding")
Encoding encoding = Encoding.LBE;
- @Parameter(names = "--maxenum", description = "Maximal number of explicitly enumerated successors (0: unlimited)")
+ @Parameter(
+ names = "--maxenum",
+ description = "Maximal number of explicitly enumerated successors (0: unlimited)")
Integer maxEnum = 10;
@Parameter(names = "--initprec", description = "Initial precision of abstraction")
InitPrec initPrec = InitPrec.EMPTY;
- @Parameter(names = "--prunestrategy", description = "Strategy for pruning the ARG after refinement")
+ @Parameter(
+ names = "--prunestrategy",
+ description = "Strategy for pruning the ARG after refinement")
PruneStrategy pruneStrategy = PruneStrategy.LAZY;
@Parameter(names = "--loglevel", description = "Detailedness of logging")
@@ -140,13 +148,20 @@ public class CfaCli {
@Parameter(names = "--cex", description = "Write concrete counterexample to a file")
String cexfile = null;
- @Parameter(names = "--header", description = "Print only a header (for benchmarks)", help = true)
+ @Parameter(
+ names = "--header",
+ description = "Print only a header (for benchmarks)",
+ help = true)
boolean headerOnly = false;
- @Parameter(names = "--visualize", description = "Visualize CFA to this file without running the algorithm")
+ @Parameter(
+ names = "--visualize",
+ description = "Visualize CFA to this file without running the algorithm")
String visualize = null;
- @Parameter(names = "--metrics", description = "Print metrics about the CFA without running the algorithm")
+ @Parameter(
+ names = "--metrics",
+ description = "Print metrics about the CFA without running the algorithm")
boolean metrics = false;
@Parameter(names = "--stacktrace", description = "Print full stack trace in case of exception")
@@ -241,13 +256,19 @@ private void run() {
final SafetyResult> status;
if (algorithm == Algorithm.CEGAR) {
- final CfaConfig configuration = buildConfiguration(cfa, errLoc, abstractionSolverFactory, refinementSolverFactory);
+ final CfaConfig configuration =
+ buildConfiguration(
+ cfa, errLoc, abstractionSolverFactory, refinementSolverFactory);
status = check(configuration);
- } else if (algorithm == Algorithm.BMC || algorithm == Algorithm.KINDUCTION || algorithm == Algorithm.IMC) {
- final BoundedChecker checker = buildBoundedChecker(cfa, abstractionSolverFactory);
+ } else if (algorithm == Algorithm.BMC
+ || algorithm == Algorithm.KINDUCTION
+ || algorithm == Algorithm.IMC) {
+ final BoundedChecker checker =
+ buildBoundedChecker(cfa, abstractionSolverFactory);
status = checker.check(null);
} else {
- throw new UnsupportedOperationException("Algorithm " + algorithm + " not supported");
+ throw new UnsupportedOperationException(
+ "Algorithm " + algorithm + " not supported");
}
sw.stop();
@@ -262,8 +283,18 @@ private void run() {
}
private void printHeader() {
- Stream.of("Result", "TimeMs", "AlgoTimeMs", "AbsTimeMs", "RefTimeMs", "Iterations",
- "ArgSize", "ArgDepth", "ArgMeanBranchFactor", "CexLen").forEach(writer::cell);
+ Stream.of(
+ "Result",
+ "TimeMs",
+ "AlgoTimeMs",
+ "AbsTimeMs",
+ "RefTimeMs",
+ "Iterations",
+ "ArgSize",
+ "ArgDepth",
+ "ArgMeanBranchFactor",
+ "CexLen")
+ .forEach(writer::cell);
writer.newRow();
}
@@ -277,67 +308,89 @@ private CFA loadModel() throws Exception {
}
}
- private CfaConfig buildConfiguration(final CFA cfa, final CFA.Loc errLoc,
- final SolverFactory abstractionSolverFactory, final SolverFactory refinementSolverFactory)
+ private CfaConfig buildConfiguration(
+ final CFA cfa,
+ final CFA.Loc errLoc,
+ final SolverFactory abstractionSolverFactory,
+ final SolverFactory refinementSolverFactory)
throws Exception {
try {
- return new CfaConfigBuilder(domain, refinement, abstractionSolverFactory,
- refinementSolverFactory)
- .precGranularity(precGranularity).search(search)
- .predSplit(predSplit).encoding(encoding).maxEnum(maxEnum).initPrec(initPrec)
- .pruneStrategy(pruneStrategy).logger(logger).build(cfa, errLoc);
+ return new CfaConfigBuilder(
+ domain, refinement, abstractionSolverFactory, refinementSolverFactory)
+ .precGranularity(precGranularity)
+ .search(search)
+ .predSplit(predSplit)
+ .encoding(encoding)
+ .maxEnum(maxEnum)
+ .initPrec(initPrec)
+ .pruneStrategy(pruneStrategy)
+ .logger(logger)
+ .build(cfa, errLoc);
} catch (final Exception ex) {
throw new Exception("Could not create configuration: " + ex.getMessage(), ex);
}
}
- private BoundedChecker buildBoundedChecker(final CFA cfa, final SolverFactory abstractionSolverFactory) {
+ private BoundedChecker buildBoundedChecker(
+ final CFA cfa, final SolverFactory abstractionSolverFactory) {
final MonolithicExpr monolithicExpr = CfaToMonolithicExprKt.toMonolithicExpr(cfa);
final BoundedChecker checker;
switch (algorithm) {
- case BMC -> checker = BoundedCheckerBuilderKt.buildBMC(
- monolithicExpr,
- abstractionSolverFactory.createSolver(),
- val -> CfaToMonolithicExprKt.valToState(cfa, val),
- (val1, val2) -> CfaToMonolithicExprKt.valToAction(cfa, val1, val2),
- logger
- );
- case KINDUCTION -> checker = BoundedCheckerBuilderKt.buildKIND(
- monolithicExpr,
- abstractionSolverFactory.createSolver(),
- abstractionSolverFactory.createSolver(),
- val -> CfaToMonolithicExprKt.valToState(cfa, val),
- (val1, val2) -> CfaToMonolithicExprKt.valToAction(cfa, val1, val2),
- logger
- );
- case IMC -> checker = BoundedCheckerBuilderKt.buildIMC(
- monolithicExpr,
- abstractionSolverFactory.createSolver(),
- abstractionSolverFactory.createItpSolver(),
- val -> CfaToMonolithicExprKt.valToState(cfa, val),
- (val1, val2) -> CfaToMonolithicExprKt.valToAction(cfa, val1, val2),
- logger
- );
+ case BMC ->
+ checker =
+ BoundedCheckerBuilderKt.buildBMC(
+ monolithicExpr,
+ abstractionSolverFactory.createSolver(),
+ val -> CfaToMonolithicExprKt.valToState(cfa, val),
+ (val1, val2) ->
+ CfaToMonolithicExprKt.valToAction(cfa, val1, val2),
+ logger);
+ case KINDUCTION ->
+ checker =
+ BoundedCheckerBuilderKt.buildKIND(
+ monolithicExpr,
+ abstractionSolverFactory.createSolver(),
+ abstractionSolverFactory.createSolver(),
+ val -> CfaToMonolithicExprKt.valToState(cfa, val),
+ (val1, val2) ->
+ CfaToMonolithicExprKt.valToAction(cfa, val1, val2),
+ logger);
+ case IMC ->
+ checker =
+ BoundedCheckerBuilderKt.buildIMC(
+ monolithicExpr,
+ abstractionSolverFactory.createSolver(),
+ abstractionSolverFactory.createItpSolver(),
+ val -> CfaToMonolithicExprKt.valToState(cfa, val),
+ (val1, val2) ->
+ CfaToMonolithicExprKt.valToAction(cfa, val1, val2),
+ logger);
default ->
- throw new UnsupportedOperationException("Algorithm " + algorithm + " not supported");
+ throw new UnsupportedOperationException(
+ "Algorithm " + algorithm + " not supported");
}
return checker;
}
- private SafetyResult, ? extends Trace> check(CfaConfig configuration) throws Exception {
+ private SafetyResult, ? extends Trace> check(
+ CfaConfig configuration) throws Exception {
try {
return configuration.check();
} catch (final Exception ex) {
String message = ex.getMessage() == null ? "(no message)" : ex.getMessage();
throw new Exception(
- "Error while running algorithm: " + ex.getClass().getSimpleName() + " " + message,
+ "Error while running algorithm: "
+ + ex.getClass().getSimpleName()
+ + " "
+ + message,
ex);
}
}
- private void printResult(final SafetyResult> status, final long totalTimeMs) {
- final CegarStatistics stats = (CegarStatistics)
- status.getStats().orElse(new CegarStatistics(0, 0, 0, 0));
+ private void printResult(
+ final SafetyResult> status, final long totalTimeMs) {
+ final CegarStatistics stats =
+ (CegarStatistics) status.getStats().orElse(new CegarStatistics(0, 0, 0, 0));
if (benchmarkMode) {
writer.cell(status.isSafe());
writer.cell(totalTimeMs);
@@ -345,7 +398,7 @@ private void printResult(final SafetyResult> status, fi
writer.cell(stats.getAbstractorTimeMs());
writer.cell(stats.getRefinerTimeMs());
writer.cell(stats.getIterations());
- if (status.getWitness() instanceof ARG arg) {
+ if (status.getProof() instanceof ARG arg) {
writer.cell(arg.size());
writer.cell(arg.getDepth());
writer.cell(arg.getMeanBranchingFactor());
@@ -369,7 +422,10 @@ private void printError(final Throwable ex) {
writer.cell("[EX] " + ex.getClass().getSimpleName() + ": " + message);
writer.newRow();
} else {
- logger.write(Level.RESULT, "%s occurred, message: %s%n", ex.getClass().getSimpleName(),
+ logger.write(
+ Level.RESULT,
+ "%s occurred, message: %s%n",
+ ex.getClass().getSimpleName(),
message);
if (stacktrace) {
final StringWriter errors = new StringWriter();
@@ -382,9 +438,10 @@ private void printError(final Throwable ex) {
}
private void writeCex(final SafetyResult.Unsafe status) throws FileNotFoundException {
- @SuppressWarnings("unchecked") final Trace, CfaAction> trace = (Trace, CfaAction>) status.getCex();
- final Trace, CfaAction> concrTrace = CfaTraceConcretizer.concretize(
- trace, Z3LegacySolverFactory.getInstance());
+ @SuppressWarnings("unchecked")
+ final Trace, CfaAction> trace = (Trace, CfaAction>) status.getCex();
+ final Trace, CfaAction> concrTrace =
+ CfaTraceConcretizer.concretize(trace, Z3LegacySolverFactory.getInstance());
final File file = new File(cexfile);
PrintWriter printWriter = null;
try {
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Checker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Checker.java
index e1a86bee69..afed36eab9 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Checker.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Checker.java
@@ -15,8 +15,7 @@
*/
package hu.bme.mit.theta.analysis.algorithm;
-public interface Checker {
-
- Result check(I input);
+public interface Checker {
+ Result check(I input);
}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/EmptyWitness.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/EmptyProof.java
similarity index 78%
rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/EmptyWitness.java
rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/EmptyProof.java
index 49794dd84e..1c8d976149 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/EmptyWitness.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/EmptyProof.java
@@ -15,15 +15,13 @@
*/
package hu.bme.mit.theta.analysis.algorithm;
-public class EmptyWitness implements Witness {
+public class EmptyProof implements Proof {
- private final static EmptyWitness empty = new EmptyWitness();
+ private static final EmptyProof empty = new EmptyProof();
- private EmptyWitness() {
- }
+ private EmptyProof() {}
- public static EmptyWitness getInstance() {
+ public static EmptyProof getInstance() {
return empty;
}
-
}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Witness.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Proof.java
similarity index 95%
rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Witness.java
rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Proof.java
index ff6157e1e3..3668ab6315 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Witness.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Proof.java
@@ -15,5 +15,4 @@
*/
package hu.bme.mit.theta.analysis.algorithm;
-public interface Witness {
-}
+public interface Proof {}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Result.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Result.java
index 0c81bf5836..438edde295 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Result.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/Result.java
@@ -17,10 +17,9 @@
import java.util.Optional;
-public interface Result {
+public interface Result {
- W getWitness();
+ Pr getProof();
Optional getStats();
-
}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyChecker.java
index 4f13fac64c..c716c1dc24 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyChecker.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyChecker.java
@@ -15,19 +15,15 @@
*/
package hu.bme.mit.theta.analysis.algorithm;
-import hu.bme.mit.theta.analysis.*;
-import hu.bme.mit.theta.analysis.algorithm.Checker;
-import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
-import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
+import hu.bme.mit.theta.analysis.Cex;
@FunctionalInterface
-public interface SafetyChecker extends Checker {
+public interface SafetyChecker extends Checker {
@Override
- SafetyResult check(final I input);
+ SafetyResult check(final I input);
- default SafetyResult check() {
+ default SafetyResult check() {
return check(null);
}
-
}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java
index 6ee1284600..7e3af4eb5d 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java
@@ -14,33 +14,28 @@
* limitations under the License.
*/
package hu.bme.mit.theta.analysis.algorithm;
-
-import hu.bme.mit.theta.analysis.Action;
import hu.bme.mit.theta.analysis.Cex;
-import hu.bme.mit.theta.analysis.State;
import hu.bme.mit.theta.common.Utils;
-
import java.util.Optional;
-
import static com.google.common.base.Preconditions.checkNotNull;
-public abstract class SafetyResult implements Result {
- private final W witness;
+public abstract class SafetyResult implements Result {
+ private final Pr proof;
private final Optional stats;
- private SafetyResult(final W witness, final Optional stats) {
- this.witness = checkNotNull(witness);
+ private SafetyResult(final Pr proof, final Optional stats) {
+ this.proof = checkNotNull(proof);
this.stats = checkNotNull(stats);
}
private SafetyResult() {
- this.witness = null;
+ this.proof = null;
this.stats = Optional.empty();
}
@Override
- public W getWitness() {
- return witness;
+ public Pr getProof() {
+ return proof;
}
@Override
@@ -48,28 +43,30 @@ public Optional getStats() {
return stats;
}
- public static Safe safe(final W witness) {
+ public static Safe safe(final Pr witness) {
return new Safe<>(witness, Optional.empty());
}
- public static Unsafe unsafe(final C cex, final W witness) {
+ public static Unsafe unsafe(
+ final C cex, final Pr witness) {
return new Unsafe<>(cex, witness, Optional.empty());
}
- public static Unknown unknown() {
+ public static Unknown unknown() {
return new Unknown<>();
}
- public static Safe safe(final W witness, final Statistics stats) {
+ public static Safe safe(
+ final Pr witness, final Statistics stats) {
return new Safe<>(witness, Optional.of(stats));
}
- public static Unsafe
## About
diff --git a/build.gradle.kts b/build.gradle.kts
index 741094252d..06036a38d7 100644
--- a/build.gradle.kts
+++ b/build.gradle.kts
@@ -13,6 +13,7 @@
* See the License for the specific language governing permissions and
* limitations under the License.
*/
+
plugins {
base
id("jacoco-common")
@@ -28,7 +29,7 @@ buildscript {
allprojects {
group = "hu.bme.mit.theta"
- version = "6.5.1"
+ version = "6.6.4"
apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
}
diff --git a/buildSrc/build.gradle.kts b/buildSrc/build.gradle.kts
index 093b423f12..7b1e3380f6 100644
--- a/buildSrc/build.gradle.kts
+++ b/buildSrc/build.gradle.kts
@@ -30,6 +30,7 @@ apply(from = rootDir.resolve("../gradle/shared-with-buildSrc/mirrors.gradle.kts"
val kotlinVersion: String by project
val shadowVersion: String by project
+val spotlessVersion: String by project
// https://github.com/gradle/kotlin-dsl/issues/430#issuecomment-414768887
fun gradlePlugin(id: String, version: String): String = "$id:$id.gradle.plugin:$version"
@@ -38,6 +39,7 @@ dependencies {
compileOnly(gradleKotlinDsl())
implementation(kotlin("gradle-plugin", kotlinVersion))
implementation(gradlePlugin("com.github.johnrengelman.shadow", shadowVersion))
+ implementation(gradlePlugin("com.diffplug.spotless", spotlessVersion))
}
// Force the embeddable Kotlin compiler version to be the selected kotlinVersion.
@@ -103,4 +105,4 @@ tasks {
named("compileKotlin", KotlinCompile::class) {
dependsOn(generateVersions)
}
-}
+}
\ No newline at end of file
diff --git a/buildSrc/gradle.properties b/buildSrc/gradle.properties
index e9c71bc25e..77da25281b 100644
--- a/buildSrc/gradle.properties
+++ b/buildSrc/gradle.properties
@@ -39,4 +39,5 @@ deltaCollectionsVersion=0.0.1
gsonVersion=2.9.1
javasmtVersion=4.1.1
sosylabVersion=0.3000-569-g89796f98
-cliktVersion=4.4.0
\ No newline at end of file
+cliktVersion=4.4.0
+spotlessVersion=6.25.0
\ No newline at end of file
diff --git a/buildSrc/src/main/kotlin/java-common.gradle.kts b/buildSrc/src/main/kotlin/java-common.gradle.kts
index 96ffbd8ec6..838b4d4f41 100644
--- a/buildSrc/src/main/kotlin/java-common.gradle.kts
+++ b/buildSrc/src/main/kotlin/java-common.gradle.kts
@@ -17,6 +17,7 @@ plugins {
java
id("jacoco-common")
id("maven-artifact")
+ id("com.diffplug.spotless")
}
dependencies {
@@ -65,3 +66,46 @@ tasks {
jvmArgs("-Xss5m", "-Xms512m", "-Xmx1g")
}
}
+
+spotless {
+ ratchetFrom("origin/master")
+
+ isEnforceCheck = false
+
+ val year = "\$YEAR" // you can't escape $ in raw strings..
+ val licenseHeader = """ /*
+ * Copyright $year Budapest University of Technology and Economics
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */""".trimIndent()
+
+
+ java {
+ importOrder("java|javax", "hu.bme.", "")
+ removeUnusedImports()
+ googleJavaFormat("1.24.0").aosp().reflowLongStrings()
+ formatAnnotations()
+
+ licenseHeader(licenseHeader)
+ }
+ kotlin {
+ ktfmt("0.51").googleStyle()
+
+ licenseHeader(licenseHeader)
+ }
+ kotlinGradle {
+ target("*.gradle.kts") // default target for kotlinGradle
+
+ ktlint()
+ }
+}
\ No newline at end of file
diff --git a/doc/theta-logo.svg b/doc/theta-logo.svg
new file mode 100644
index 0000000000..8705b0a3b4
--- /dev/null
+++ b/doc/theta-logo.svg
@@ -0,0 +1,50 @@
+
+
+
+
diff --git a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java
index 7427f38b20..37c30260ea 100644
--- a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java
+++ b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java
@@ -15,16 +15,19 @@
*/
package hu.bme.mit.theta.cfa.analysis.config;
+import static com.google.common.base.Preconditions.checkState;
+import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True;
+
import hu.bme.mit.theta.analysis.*;
+import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder;
import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators;
import hu.bme.mit.theta.analysis.algorithm.arg.ArgNodeComparators.ArgNodeComparator;
-import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
-import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor;
-import hu.bme.mit.theta.analysis.algorithm.cegar.BasicAbstractor;
-import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker;
-import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner;
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor;
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgCegarChecker;
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgRefiner;
+import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor;
import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterion;
import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterions;
import hu.bme.mit.theta.analysis.expl.*;
@@ -52,14 +55,10 @@
import hu.bme.mit.theta.common.logging.NullLogger;
import hu.bme.mit.theta.solver.Solver;
import hu.bme.mit.theta.solver.SolverFactory;
-
import java.util.Set;
import java.util.function.Function;
import java.util.function.Predicate;
-import static com.google.common.base.Preconditions.checkState;
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True;
-
public class CfaConfigBuilder {
private final SolverFactory abstractionSolverFactory;
@@ -75,16 +74,19 @@ public class CfaConfigBuilder {
private InitPrec initPrec = InitPrec.EMPTY;
private PruneStrategy pruneStrategy = PruneStrategy.LAZY;
- public CfaConfigBuilder(final Domain domain, final Refinement refinement,
- final SolverFactory solverFactory) {
+ public CfaConfigBuilder(
+ final Domain domain, final Refinement refinement, final SolverFactory solverFactory) {
this.domain = domain;
this.refinement = refinement;
this.abstractionSolverFactory = solverFactory;
this.refinementSolverFactory = solverFactory;
}
- public CfaConfigBuilder(final Domain domain, final Refinement refinement,
- final SolverFactory abstractionSolverFactory, final SolverFactory refinementSolverFactory) {
+ public CfaConfigBuilder(
+ final Domain domain,
+ final Refinement refinement,
+ final SolverFactory abstractionSolverFactory,
+ final SolverFactory refinementSolverFactory) {
this.domain = domain;
this.refinement = refinement;
this.abstractionSolverFactory = abstractionSolverFactory;
@@ -131,12 +133,13 @@ public CfaConfigBuilder pruneStrategy(final PruneStrategy pruneStrategy) {
return this;
}
- public CfaConfig build(final CFA cfa,
- final CFA.Loc errLoc) {
+ public CfaConfig build(
+ final CFA cfa, final CFA.Loc errLoc) {
if (domain == Domain.EXPL) {
return (new ExplStrategy(cfa)).buildConfig(errLoc);
}
- if (domain == Domain.PRED_BOOL || domain == Domain.PRED_CART
+ if (domain == Domain.PRED_BOOL
+ || domain == Domain.PRED_CART
|| domain == Domain.PRED_SPLIT) {
return (new PredStrategy(cfa)).buildConfig(errLoc);
}
@@ -166,18 +169,53 @@ public enum Domain {
public enum Refinement {
FW_BIN_ITP {
@Override
- public