diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 3ccab85b38..161486f7cd 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -3,6 +3,7 @@ import com.dat3m.dartagnan.configuration.OptionNames; import com.dat3m.dartagnan.configuration.Property; import com.dat3m.dartagnan.encoding.EncodingContext; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.expression.ExpressionPrinter; import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.parsers.program.ProgramParser; @@ -163,7 +164,10 @@ public static void main(String[] args) throws Exception { BasicLogManager.create(solverConfig), sdm.getNotifier(), o.getSolver()); - ProverEnvironment prover = ctx.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + ProverWithTracker prover = new ProverWithTracker(ctx, + o.getDumpSmtLib() ? + System.getenv("DAT3M_OUTPUT") + String.format("/%s.smt2", p.getName()) : "", + ProverOptions.GENERATE_MODELS)) { ModelChecker modelChecker; if (properties.contains(DATARACEFREEDOM)) { if (properties.size() > 1) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java index 3cec00bf75..18a0ca89fc 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java @@ -12,6 +12,7 @@ public class OptionNames { public static final String VALIDATE = "validate"; public static final String COVERAGE = "coverage"; public static final String WITNESS = "witness"; + public static final String SMTLIB2 = "smtlib2"; // Modeling Options public static final String THREAD_CREATE_ALWAYS_SUCCEEDS = "modeling.threadCreateAlwaysSucceeds"; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java new file mode 100644 index 0000000000..24d6ad8be4 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java @@ -0,0 +1,200 @@ +package com.dat3m.dartagnan.encoding; + +import java.io.File; +import java.io.FileWriter; +import java.io.IOException; +import java.io.PrintWriter; +import java.nio.file.Files; +import java.nio.file.Paths; +import java.time.LocalDate; +import java.time.format.DateTimeFormatter; +import java.util.Collection; +import java.util.HashSet; +import java.util.List; +import java.util.Optional; +import java.util.Set; + +import org.sosy_lab.java_smt.api.*; +import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; + +import com.google.common.collect.ImmutableMap; + +public class ProverWithTracker implements ProverEnvironment { + + private final FormulaManager fmgr; + private final ProverEnvironment prover; + private final String fileName; + private final Set declarations; + + public ProverWithTracker(SolverContext ctx, String fileName, ProverOptions... options) { + this.fmgr = ctx.getFormulaManager(); + this.prover = ctx.newProverEnvironment(options); + this.fileName = fileName; + this.declarations = new HashSet<>(); + init(); + } + + // An empty filename means there is no need to dump the encoding + private boolean dump() { + return !fileName.isEmpty(); + } + + private void init() { + if(dump()) { + try { + Files.deleteIfExists(Paths.get(fileName)); + } catch (IOException e) { + e.printStackTrace(); + } + StringBuilder description = new StringBuilder(); + LocalDate currentDate = LocalDate.now(); + DateTimeFormatter formatter = DateTimeFormatter.ofPattern("YYYY-MM-DD"); + description.append("Generated on: " + currentDate.format(formatter) + "\n"); + description.append("Generator: Dartagnan\n"); + description.append("Application: Bounded model checking for weak memory models\n"); + description.append("Publications: \n" + + "- Hernán Ponce de León, Florian Furbach, Keijo Heljanko, " + + "Roland Meyer: Dartagnan: Bounded Model Checking for Weak Memory Models " + + "(Competition Contribution). TACAS (2) 2020: 378-382\n" + + "- Thomas Haas, Roland Meyer, Hernán Ponce de León: " + + "CAAT: consistency as a theory. Proc. ACM Program. Lang. 6(OOPSLA2): 114-144 (2022)" + ); + write("(set-info :smt-lib-version 2.6)\n"); + write("(set-logic ALL)\n"); + write("(set-info :category \"industrial\")\n"); + write("(set-info :source |\n" + description + "\n|)\n"); + write("(set-info :license \"https://creativecommons.org/licenses/by/4.0/\")\n"); + } + } + + @Override + public void close() { + if(dump()) { + removeDuplicatedDeclarations(fileName); + write("(exit)\n"); + } + prover.close(); + } + + @Override + public Void addConstraint(BooleanFormula f) throws InterruptedException { + if(dump()) { + write(fmgr.dumpFormula(f).toString()); + } + return prover.addConstraint(f); + } + + @Override + public boolean isUnsatWithAssumptions(Collection fs) throws SolverException, InterruptedException { + + if(dump()) { + write("(push)\n"); + for(BooleanFormula f : fs) { + write(fmgr.dumpFormula(f).toString()); + } + } + + long start = System.currentTimeMillis(); + boolean result = prover.isUnsatWithAssumptions(fs); + long end = System.currentTimeMillis(); + + if(dump()) { + write("(set-info :status " + (result ? "unsat" : "sat") + ")\n"); + write("(check-sat)\n"); + writeComment("Original solving time: " + (end - start) + " ms"); + write("(pop)\n"); + } + + return result; + } + + @Override + public boolean isUnsat() throws SolverException, InterruptedException { + long start = System.currentTimeMillis(); + boolean result = prover.isUnsat(); + long end = System.currentTimeMillis(); + if(dump()) { + write("(set-info :status " + (result ? "unsat" : "sat") + ")\n"); + write("(check-sat)\n"); + writeComment("Original solving time: " + (end - start) + " ms"); + } + return result; + } + + @Override + public ImmutableMap getStatistics() { + return prover.getStatistics(); + } + + @Override + public Model getModel() throws SolverException { + return prover.getModel(); + } + + @Override + public void push() throws InterruptedException { + if(dump()) { + write("(push)\n"); + } + prover.push(); + } + + @Override + public void pop() { + if(dump()) { + write("(pop)\n"); + } + prover.pop(); + } + + @Override + public R allSat(AllSatCallback arg0, List arg1) throws InterruptedException, SolverException { + return prover.allSat(arg0, arg1); + } + + @Override + public List getUnsatCore() { + return prover.getUnsatCore(); + } + + @Override + public int size() { + return prover.size(); + } + + @Override + public Optional> unsatCoreOverAssumptions(Collection arg0) + throws SolverException, InterruptedException { + return prover.unsatCoreOverAssumptions(arg0); + } + + private void write(String content) { + if (dump()) { + File file = new File(fileName); + try (FileWriter writer = new FileWriter(file, true); + PrintWriter printer = new PrintWriter(writer)) { + printer.append(removeDuplicatedDeclarations(content)); + printer.close(); + } catch (IOException e) { + e.printStackTrace(); + } + } + } + + public void writeComment(String content) { + write("; " + content); + } + + // FIXME: This is only correct as long as no declarations are popped and then + // later redeclared (which is currently guarenteed by the way we use the solver) + private StringBuilder removeDuplicatedDeclarations(String content) { + StringBuilder builder = new StringBuilder(); + for(String line : content.split("\n")) { + if(line.contains("declare-fun") && !declarations.add(line)) { + continue; + } + builder.append(line + "\n"); + } + return builder; + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java index b448471580..d858308a5f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java @@ -2,10 +2,8 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; -import com.dat3m.dartagnan.expression.Type; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.Program.SourceLanguage; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; import com.dat3m.dartagnan.program.event.Tag; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java index 32cfec175a..fd166a38e0 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java @@ -68,4 +68,11 @@ public abstract class BaseOptions { private WitnessType witnessType=WitnessType.getDefault(); public WitnessType getWitnessType() { return witnessType; } + + @Option( + name=SMTLIB2, + description="Dump encoding to an SMTLIB2 file.") + private boolean smtlib=false; + + public boolean getDumpSmtLib() { return smtlib; } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java index cc0200630b..a8108aa9f1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java @@ -21,16 +21,16 @@ public class AssumeSolver extends ModelChecker { private static final Logger logger = LogManager.getLogger(AssumeSolver.class); private final SolverContext ctx; - private final ProverEnvironment prover; + private final ProverWithTracker prover; private final VerificationTask task; - private AssumeSolver(SolverContext c, ProverEnvironment p, VerificationTask t) { + private AssumeSolver(SolverContext c, ProverWithTracker p, VerificationTask t) { ctx = c; prover = p; task = t; } - public static AssumeSolver run(SolverContext ctx, ProverEnvironment prover, VerificationTask task) + public static AssumeSolver run(SolverContext ctx, ProverWithTracker prover, VerificationTask task) throws InterruptedException, SolverException, InvalidConfigurationException { AssumeSolver s = new AssumeSolver(ctx, prover, task); s.run(); @@ -55,21 +55,27 @@ private void run() throws InterruptedException, SolverException, InvalidConfigur SymmetryEncoder symmetryEncoder = SymmetryEncoder.withContext(context); logger.info("Starting encoding using " + ctx.getVersion()); + prover.writeComment("Program encoding"); prover.addConstraint(programEncoder.encodeFullProgram()); + prover.writeComment("Memory model encoding"); prover.addConstraint(wmmEncoder.encodeFullMemoryModel()); // For validation this contains information. // For verification graph.encode() just returns ctx.mkTrue() + prover.writeComment("Witness encoding"); prover.addConstraint(task.getWitness().encode(context)); + prover.writeComment("Symmetry breaking encoding"); prover.addConstraint(symmetryEncoder.encodeFullSymmetryBreaking()); BooleanFormulaManager bmgr = ctx.getFormulaManager().getBooleanFormulaManager(); BooleanFormula assumptionLiteral = bmgr.makeVariable("DAT3M_spec_assumption"); BooleanFormula propertyEncoding = propertyEncoder.encodeProperties(task.getProperty()); BooleanFormula assumedSpec = bmgr.implication(assumptionLiteral, propertyEncoding); + prover.writeComment("Property encoding"); prover.addConstraint(assumedSpec); logger.info("Starting first solver.check()"); if(prover.isUnsatWithAssumptions(singletonList(assumptionLiteral))) { + prover.writeComment("Bound encoding"); prover.addConstraint(propertyEncoder.encodeBoundEventExec()); logger.info("Starting second solver.check()"); res = prover.isUnsat()? PASS : Result.UNKNOWN; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java index 5190ef5d4c..0941215cc3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java @@ -9,7 +9,7 @@ import org.apache.logging.log4j.Logger; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; -import org.sosy_lab.java_smt.api.ProverEnvironment; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverException; @@ -18,63 +18,67 @@ import static com.dat3m.dartagnan.utils.Result.*; public class DataRaceSolver extends ModelChecker { - - // This analysis assumes that CAT file defining the memory model has a happens-before - // relation named hb: it should contain the following axiom "acyclic hb" + + // This analysis assumes that CAT file defining the memory model has a happens-before + // relation named hb: it should contain the following axiom "acyclic hb" private static final Logger logger = LogManager.getLogger(DataRaceSolver.class); - private final SolverContext ctx; - private final ProverEnvironment prover; - private final VerificationTask task; + private final SolverContext ctx; + private final ProverWithTracker prover; + private final VerificationTask task; - private DataRaceSolver(SolverContext c, ProverEnvironment p, VerificationTask t) { - ctx = c; - prover = p; - task = t; - } + private DataRaceSolver(SolverContext c, ProverWithTracker p, VerificationTask t) { + ctx = c; + prover = p; + task = t; + } - public static DataRaceSolver run(SolverContext ctx, ProverEnvironment prover, VerificationTask task) - throws InterruptedException, SolverException, InvalidConfigurationException { - DataRaceSolver s = new DataRaceSolver(ctx, prover, task); - s.run(); - return s; - } + public static DataRaceSolver run(SolverContext ctx, ProverWithTracker prover, VerificationTask task) + throws InterruptedException, SolverException, InvalidConfigurationException { + DataRaceSolver s = new DataRaceSolver(ctx, prover, task); + s.run(); + return s; + } - private void run() throws InterruptedException, SolverException, InvalidConfigurationException { - Wmm memoryModel = task.getMemoryModel(); - Context analysisContext = Context.create(); - Configuration config = task.getConfig(); + private void run() throws InterruptedException, SolverException, InvalidConfigurationException { + Wmm memoryModel = task.getMemoryModel(); + Context analysisContext = Context.create(); + Configuration config = task.getConfig(); - memoryModel.configureAll(config); - preprocessProgram(task, config); - preprocessMemoryModel(task, config); - performStaticProgramAnalyses(task, analysisContext, config); - performStaticWmmAnalyses(task, analysisContext, config); + memoryModel.configureAll(config); + preprocessProgram(task, config); + preprocessMemoryModel(task, config); + performStaticProgramAnalyses(task, analysisContext, config); + performStaticWmmAnalyses(task, analysisContext, config); - context = EncodingContext.of(task, analysisContext, ctx.getFormulaManager()); - ProgramEncoder programEncoder = ProgramEncoder.withContext(context); - PropertyEncoder propertyEncoder = PropertyEncoder.withContext(context); - WmmEncoder wmmEncoder = WmmEncoder.withContext(context); - SymmetryEncoder symmetryEncoder = SymmetryEncoder.withContext(context); + context = EncodingContext.of(task, analysisContext, ctx.getFormulaManager()); + ProgramEncoder programEncoder = ProgramEncoder.withContext(context); + PropertyEncoder propertyEncoder = PropertyEncoder.withContext(context); + WmmEncoder wmmEncoder = WmmEncoder.withContext(context); + SymmetryEncoder symmetryEncoder = SymmetryEncoder.withContext(context); logger.info("Starting encoding using " + ctx.getVersion()); - prover.addConstraint(programEncoder.encodeFullProgram()); - prover.addConstraint(wmmEncoder.encodeFullMemoryModel()); - prover.addConstraint(symmetryEncoder.encodeFullSymmetryBreaking()); - prover.push(); - - prover.addConstraint(propertyEncoder.encodeProperties(EnumSet.of(Property.DATARACEFREEDOM))); + prover.writeComment("Program encoding"); + prover.addConstraint(programEncoder.encodeFullProgram()); + prover.writeComment("Memory model encoding"); + prover.addConstraint(wmmEncoder.encodeFullMemoryModel()); + prover.writeComment("Symmetry breaking encoding"); + prover.addConstraint(symmetryEncoder.encodeFullSymmetryBreaking()); + prover.push(); + prover.writeComment("Property encoding"); + prover.addConstraint(propertyEncoder.encodeProperties(EnumSet.of(Property.DATARACEFREEDOM))); - logger.info("Starting first solver.check()"); - if(prover.isUnsat()) { - prover.pop(); - prover.addConstraint(propertyEncoder.encodeBoundEventExec()); - logger.info("Starting second solver.check()"); - res = prover.isUnsat() ? PASS : UNKNOWN; - } else { - res = FAIL; - } + logger.info("Starting first solver.check()"); + if (prover.isUnsat()) { + prover.pop(); + prover.writeComment("Bound encoding"); + prover.addConstraint(propertyEncoder.encodeBoundEventExec()); + logger.info("Starting second solver.check()"); + res = prover.isUnsat() ? PASS : UNKNOWN; + } else { + res = FAIL; + } logger.info("Verification finished with result " + res); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java index f432c68d0f..bce614c3ba 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java @@ -162,7 +162,7 @@ private RefinementSolver() { //TODO: We do not yet use Witness information. The problem is that WitnessGraph.encode() generates // constraints on hb, which is not encoded in Refinement. //TODO (2): Add possibility for Refinement to handle CAT-properties (it ignores them for now). - public static RefinementSolver run(SolverContext ctx, ProverEnvironment prover, VerificationTask task) + public static RefinementSolver run(SolverContext ctx, ProverWithTracker prover, VerificationTask task) throws InterruptedException, SolverException, InvalidConfigurationException { RefinementSolver solver = new RefinementSolver(); task.getConfig().inject(solver); @@ -171,7 +171,7 @@ public static RefinementSolver run(SolverContext ctx, ProverEnvironment prover, return solver; } - private void runInternal(SolverContext ctx, ProverEnvironment prover, VerificationTask task) + private void runInternal(SolverContext ctx, ProverWithTracker prover, VerificationTask task) throws InterruptedException, SolverException, InvalidConfigurationException { final Program program = task.getProgram(); final Wmm memoryModel = task.getMemoryModel(); @@ -224,8 +224,11 @@ private void runInternal(SolverContext ctx, ProverEnvironment prover, Verificati final Property.Type propertyType = Property.getCombinedType(task.getProperty(), task); logger.info("Starting encoding using " + ctx.getVersion()); + prover.writeComment("Program encoding"); prover.addConstraint(programEncoder.encodeFullProgram()); + prover.writeComment("Memory model (baseline) encoding"); prover.addConstraint(baselineEncoder.encodeFullMemoryModel()); + prover.writeComment("Symmetry breaking encoding"); prover.addConstraint(symmetryEncoder.encodeFullSymmetryBreaking()); // ------------------------ Solving ------------------------ @@ -233,6 +236,7 @@ private void runInternal(SolverContext ctx, ProverEnvironment prover, Verificati logger.info("Checking target property."); prover.push(); + prover.writeComment("Property encoding"); prover.addConstraint(propertyEncoder.encodeProperties(task.getProperty())); final RefinementTrace propertyTrace = runRefinement(task, prover, solver, refiner); @@ -265,8 +269,10 @@ private void runInternal(SolverContext ctx, ProverEnvironment prover, Verificati logger.info("Checking unrolling bounds."); final long lastTime = System.currentTimeMillis(); prover.pop(); + prover.writeComment("Bound encoding"); prover.addConstraint(propertyEncoder.encodeBoundEventExec()); // Add back the refinement clauses we already found, hoping that this improves the performance. + prover.writeComment("Refinement encoding"); prover.addConstraint(bmgr.and(propertyTrace.getRefinementFormulas())); final RefinementTrace boundTrace = runRefinement(task, prover, solver, refiner); boundCheckTime = System.currentTimeMillis() - lastTime; @@ -358,7 +364,7 @@ private void analyzeInconclusiveness(VerificationTask task, Context analysisCont // Refinement core algorithm // TODO: We could expose the following method(s) to allow for more general application of refinement. - private RefinementTrace runRefinement(VerificationTask task, ProverEnvironment prover, WMMSolver solver, Refiner refiner) + private RefinementTrace runRefinement(VerificationTask task, ProverWithTracker prover, WMMSolver solver, Refiner refiner) throws SolverException, InterruptedException { final List trace = new ArrayList<>(); @@ -418,7 +424,7 @@ private boolean checkProgress(List trace) { return !last.inconsistencyReasons.equals(prev.inconsistencyReasons); } - private RefinementIteration doRefinementIteration(ProverEnvironment prover, WMMSolver solver, Refiner refiner) + private RefinementIteration doRefinementIteration(ProverWithTracker prover, WMMSolver solver, Refiner refiner) throws SolverException, InterruptedException { long nativeTime = 0; @@ -455,6 +461,7 @@ private RefinementIteration doRefinementIteration(ProverEnvironment prover, WMMS inconsistencyReasons = solverResult.getCoreReasons(); lastTime = System.currentTimeMillis(); refinementFormula = refiner.refine(inconsistencyReasons, context); + prover.writeComment("Refinement encoding"); prover.addConstraint(refinementFormula); refineTime = (System.currentTimeMillis() - lastTime); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Assumption.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Assumption.java index 2da9f984e9..788a3b8f09 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Assumption.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Assumption.java @@ -1,21 +1,15 @@ package com.dat3m.dartagnan.wmm; -import com.dat3m.dartagnan.verification.Context; -import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; import com.dat3m.dartagnan.wmm.utils.EventGraph; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; -import java.util.Map; import java.util.Set; -import static com.dat3m.dartagnan.wmm.utils.EventGraph.difference; import static com.google.common.base.Preconditions.checkNotNull; public final class Assumption implements Constraint { - private static final Logger logger = LogManager.getLogger(Assumption.class); - private final Relation rel; private final EventGraph may; private final EventGraph must; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java index 1a674d9626..4c5ef52794 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java @@ -3,7 +3,6 @@ import com.dat3m.dartagnan.encoding.EncodingContext; import com.dat3m.dartagnan.verification.Context; import com.dat3m.dartagnan.verification.VerificationTask; -import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; import com.dat3m.dartagnan.wmm.axiom.*; import com.dat3m.dartagnan.wmm.definition.*; import com.dat3m.dartagnan.wmm.utils.EventGraph; diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java index 8593902783..39d4ef879d 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java @@ -3,6 +3,7 @@ import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.configuration.OptionNames; import com.dat3m.dartagnan.configuration.Property; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.utils.rules.Provider; @@ -17,7 +18,6 @@ import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import java.util.EnumSet; @@ -84,7 +84,7 @@ protected Provider getConfigurationProvider() { protected final Provider configurationProvider = getConfigurationProvider(); protected final Provider taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, targetProvider, boundProvider, configurationProvider); protected final Provider contextProvider = Providers.createSolverContextFromManager(shutdownManagerProvider, solverProvider); - protected final Provider proverProvider = Providers.createProverWithFixedOptions(contextProvider, SolverContext.ProverOptions.GENERATE_MODELS); + protected final Provider proverProvider = Providers.createProverWithFixedOptions(contextProvider, SolverContext.ProverOptions.GENERATE_MODELS); // Special rules protected final Timeout timeout = Timeout.millis(getTimeout()); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java index b92e1209f5..f0d6f31d2a 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java @@ -2,6 +2,7 @@ import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.configuration.Property; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.Tag; @@ -19,7 +20,6 @@ import org.sosy_lab.common.ShutdownManager; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; @@ -99,8 +99,8 @@ protected Provider getConfigurationProvider() { protected final Provider task2Provider = Providers.createTask(program2Provider, wmm2Provider, propertyProvider, targetProvider, () -> 1, configProvider); protected final Provider context1Provider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3); protected final Provider context2Provider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3); - protected final Provider prover1Provider = Providers.createProverWithFixedOptions(context1Provider, ProverOptions.GENERATE_MODELS); - protected final Provider prover2Provider = Providers.createProverWithFixedOptions(context2Provider, ProverOptions.GENERATE_MODELS); + protected final Provider prover1Provider = Providers.createProverWithFixedOptions(context1Provider, ProverOptions.GENERATE_MODELS); + protected final Provider prover2Provider = Providers.createProverWithFixedOptions(context2Provider, ProverOptions.GENERATE_MODELS); private final Timeout timeout = Timeout.millis(getTimeout()); private final RequestShutdownOnError shutdownOnError = RequestShutdownOnError.create(shutdownManagerProvider); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java index 1e86058312..3316d114eb 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/litmus/AbstractLitmusTest.java @@ -2,6 +2,7 @@ import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.configuration.Property; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.utils.ResourceHelper; import com.dat3m.dartagnan.utils.Result; @@ -19,7 +20,6 @@ import org.sosy_lab.common.ShutdownManager; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; @@ -110,8 +110,8 @@ protected long getTimeout() { protected final Provider configProvider = getConfigurationProvider(); protected final Provider taskProvider = Providers.createTask(programProvider, wmmProvider, propertyProvider, targetProvider, boundProvider, configProvider); protected final Provider contextProvider = Providers.createSolverContextFromManager(shutdownManagerProvider, () -> Solvers.Z3); - protected final Provider proverProvider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS); - protected final Provider prover2Provider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS); + protected final Provider proverProvider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS); + protected final Provider prover2Provider = Providers.createProverWithFixedOptions(contextProvider, ProverOptions.GENERATE_MODELS); private final Timeout timeout = Timeout.millis(getTimeout()); private final RequestShutdownOnError shutdownOnError = RequestShutdownOnError.create(shutdownManagerProvider); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/ArrayValidTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/ArrayValidTest.java index fa2d573259..e8ba520d5c 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/ArrayValidTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/ArrayValidTest.java @@ -2,6 +2,7 @@ import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.configuration.Property; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.parsers.program.ProgramParser; import com.dat3m.dartagnan.program.Program; @@ -12,7 +13,6 @@ import org.junit.Test; import org.junit.runner.RunWith; import org.junit.runners.Parameterized; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; @@ -56,7 +56,7 @@ public ArrayValidTest(String path, Wmm wmm) { @Test public void test() { try (SolverContext ctx = TestHelper.createContext(); - ProverEnvironment prover = ctx.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + ProverWithTracker prover = new ProverWithTracker(ctx, "", ProverOptions.GENERATE_MODELS)) { Program program = new ProgramParser().parse(new File(path)); VerificationTask task = VerificationTask.builder() .withSolverTimeout(60) diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/BranchTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/BranchTest.java index 05d84eb465..588dc3cdb0 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/BranchTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/BranchTest.java @@ -2,6 +2,7 @@ import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.configuration.Property; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.parsers.program.ProgramParser; import com.dat3m.dartagnan.program.Program; @@ -14,7 +15,6 @@ import org.junit.Test; import org.junit.runner.RunWith; import org.junit.runners.Parameterized; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; @@ -95,7 +95,7 @@ public BranchTest(String path, Result expected, Wmm wmm) { @Test public void test() { try (SolverContext ctx = TestHelper.createContext(); - ProverEnvironment prover = ctx.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + ProverWithTracker prover = new ProverWithTracker(ctx, "", ProverOptions.GENERATE_MODELS)) { Program program = new ProgramParser().parse(new File(path)); VerificationTask task = VerificationTask.builder() .withSolverTimeout(60) diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java index e86077b009..24fa6af270 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java @@ -1,6 +1,7 @@ package com.dat3m.dartagnan.spirv.basic; import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.parsers.program.ProgramParser; import com.dat3m.dartagnan.program.Program; @@ -17,7 +18,6 @@ import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.log.BasicLogManager; import org.sosy_lab.java_smt.SolverContextFactory; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import java.io.File; @@ -113,10 +113,10 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { - assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { + assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); } - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } } @@ -130,8 +130,8 @@ private SolverContext mkCtx() throws InvalidConfigurationException { SolverContextFactory.Solvers.Z3); } - private ProverEnvironment mkProver(SolverContext ctx) { - return ctx.newProverEnvironment(SolverContext.ProverOptions.GENERATE_MODELS); + private ProverWithTracker mkProver(SolverContext ctx) { + return new ProverWithTracker(ctx, "", SolverContext.ProverOptions.GENERATE_MODELS); } private VerificationTask mkTask() throws Exception { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java index 9006c1b99f..6625246101 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java @@ -1,6 +1,7 @@ package com.dat3m.dartagnan.spirv.benchmarks; import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.parsers.program.ProgramParser; import com.dat3m.dartagnan.program.Program; @@ -17,7 +18,6 @@ import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.log.BasicLogManager; import org.sosy_lab.java_smt.SolverContextFactory; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import java.io.File; @@ -114,10 +114,10 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); } - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } } @@ -131,8 +131,8 @@ private SolverContext mkCtx() throws InvalidConfigurationException { SolverContextFactory.Solvers.Z3); } - private ProverEnvironment mkProver(SolverContext ctx) { - return ctx.newProverEnvironment(SolverContext.ProverOptions.GENERATE_MODELS); + private ProverWithTracker mkProver(SolverContext ctx) { + return new ProverWithTracker(ctx, "", SolverContext.ProverOptions.GENERATE_MODELS); } private VerificationTask mkTask() throws Exception { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java index c217abd6f7..0efe8060ed 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java @@ -1,6 +1,7 @@ package com.dat3m.dartagnan.spirv.benchmarks; import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.parsers.program.ProgramParser; import com.dat3m.dartagnan.program.Program; @@ -17,7 +18,6 @@ import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.log.BasicLogManager; import org.sosy_lab.java_smt.SolverContextFactory; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import java.io.File; @@ -118,10 +118,10 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { - assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { + assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); } - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } } @@ -135,8 +135,8 @@ private SolverContext mkCtx() throws InvalidConfigurationException { SolverContextFactory.Solvers.Z3); } - private ProverEnvironment mkProver(SolverContext ctx) { - return ctx.newProverEnvironment(SolverContext.ProverOptions.GENERATE_MODELS); + private ProverWithTracker mkProver(SolverContext ctx) { + return new ProverWithTracker(ctx, "", SolverContext.ProverOptions.GENERATE_MODELS); } private VerificationTask mkTask() throws Exception { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java index a5c88e5f77..b6ee1d618c 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java @@ -1,6 +1,7 @@ package com.dat3m.dartagnan.spirv.benchmarks; import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.parsers.program.ProgramParser; import com.dat3m.dartagnan.program.Program; @@ -17,7 +18,6 @@ import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.log.BasicLogManager; import org.sosy_lab.java_smt.SolverContextFactory; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import java.io.File; @@ -119,10 +119,10 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { - assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { + assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); } - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } } @@ -136,8 +136,8 @@ private SolverContext mkCtx() throws InvalidConfigurationException { SolverContextFactory.Solvers.Z3); } - private ProverEnvironment mkProver(SolverContext ctx) { - return ctx.newProverEnvironment(SolverContext.ProverOptions.GENERATE_MODELS); + private ProverWithTracker mkProver(SolverContext ctx) { + return new ProverWithTracker(ctx, "", SolverContext.ProverOptions.GENERATE_MODELS); } private VerificationTask mkTask() throws Exception { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java index b682b3505e..0cbb610e7d 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java @@ -1,6 +1,7 @@ package com.dat3m.dartagnan.spirv.gpuverify; import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.parsers.program.ProgramParser; import com.dat3m.dartagnan.program.Program; @@ -17,7 +18,6 @@ import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.log.BasicLogManager; import org.sosy_lab.java_smt.SolverContextFactory; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import java.io.File; @@ -346,10 +346,10 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { - assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { + assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); } - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } } @@ -363,8 +363,8 @@ private SolverContext mkCtx() throws InvalidConfigurationException { SolverContextFactory.Solvers.Z3); } - private ProverEnvironment mkProver(SolverContext ctx) { - return ctx.newProverEnvironment(SolverContext.ProverOptions.GENERATE_MODELS); + private ProverWithTracker mkProver(SolverContext ctx) { + return new ProverWithTracker(ctx, "", SolverContext.ProverOptions.GENERATE_MODELS); } private VerificationTask mkTask() throws Exception { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java index da21d9fb30..2493d31e92 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java @@ -1,6 +1,7 @@ package com.dat3m.dartagnan.spirv.gpuverify; import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.parsers.program.ProgramParser; import com.dat3m.dartagnan.program.Program; @@ -17,7 +18,6 @@ import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.log.BasicLogManager; import org.sosy_lab.java_smt.SolverContextFactory; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import java.io.File; @@ -346,10 +346,10 @@ public static Iterable data() throws IOException { @Test public void testAllSolvers() throws Exception { - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { - assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { + assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); } - try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) { + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); } } @@ -363,8 +363,8 @@ private SolverContext mkCtx() throws InvalidConfigurationException { SolverContextFactory.Solvers.Z3); } - private ProverEnvironment mkProver(SolverContext ctx) { - return ctx.newProverEnvironment(SolverContext.ProverOptions.GENERATE_MODELS); + private ProverWithTracker mkProver(SolverContext ctx) { + return new ProverWithTracker(ctx, "", SolverContext.ProverOptions.GENERATE_MODELS); } private VerificationTask mkTask() throws Exception { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/utils/rules/Providers.java b/dartagnan/src/test/java/com/dat3m/dartagnan/utils/rules/Providers.java index 0b8c06b449..f31db39a13 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/utils/rules/Providers.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/utils/rules/Providers.java @@ -8,12 +8,12 @@ import com.dat3m.dartagnan.wmm.Wmm; import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.configuration.Property; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import org.sosy_lab.common.ShutdownManager; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import java.io.File; @@ -81,11 +81,11 @@ public static Provider createSolverContextFromManager(Supplier TestHelper.createContextWithShutdownNotifier(shutdownManagerSupplier.get().getNotifier(), solverSupplier.get())); } - public static Provider createProver(Supplier contextSupplier, Supplier optionsSupplier) { - return Provider.fromSupplier(() -> contextSupplier.get().newProverEnvironment(optionsSupplier.get())); + public static Provider createProver(Supplier contextSupplier, Supplier optionsSupplier) { + return Provider.fromSupplier(() -> new ProverWithTracker(contextSupplier.get(), "", optionsSupplier.get())); } - public static Provider createProverWithFixedOptions(Supplier contextSupplier, SolverContext.ProverOptions... options) { + public static Provider createProverWithFixedOptions(Supplier contextSupplier, SolverContext.ProverOptions... options) { return createProver(contextSupplier, () -> options); } } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java index 98b1d7d9ee..7b4d135cb4 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java @@ -1,6 +1,7 @@ package com.dat3m.dartagnan.witness; import com.dat3m.dartagnan.configuration.Property; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.parsers.program.ProgramParser; import com.dat3m.dartagnan.program.Program; @@ -15,7 +16,6 @@ import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.BooleanFormulaManager; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; @@ -43,7 +43,7 @@ public void BuildWriteEncode() throws Exception { Wmm wmm = new ParserCat().parse(new File(getRootPath("cat/svcomp.cat"))); VerificationTask task = VerificationTask.builder().withConfig(config).build(p, wmm, Property.getDefault()); try (SolverContext ctx = TestHelper.createContext(); - ProverEnvironment prover = ctx.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + ProverWithTracker prover = new ProverWithTracker(ctx, "", ProverOptions.GENERATE_MODELS)) { AssumeSolver modelChecker = AssumeSolver.run(ctx, prover, task); Result res = modelChecker.getResult(); WitnessBuilder witnessBuilder = WitnessBuilder.of(modelChecker.getEncodingContext(), prover, res, "user assertion"); diff --git a/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java b/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java index 6f2f6e622b..890aa30d4b 100644 --- a/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java +++ b/ui/src/main/java/com/dat3m/ui/result/ReachabilityResult.java @@ -10,13 +10,13 @@ import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.witness.WitnessType; import com.dat3m.dartagnan.wmm.Wmm; +import com.dat3m.dartagnan.encoding.ProverWithTracker; import com.dat3m.ui.utils.UiOptions; import com.dat3m.ui.utils.Utils; import org.sosy_lab.common.ShutdownManager; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.log.BasicLogManager; import org.sosy_lab.java_smt.SolverContextFactory; -import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; @@ -92,7 +92,7 @@ private void run() { BasicLogManager.create(solverConfig), sdm.getNotifier(), options.solver()); - ProverEnvironment prover = ctx.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + ProverWithTracker prover = new ProverWithTracker(ctx, "", ProverOptions.GENERATE_MODELS)) { final ModelChecker modelChecker; modelChecker = switch (options.method()) { case EAGER -> AssumeSolver.run(ctx, prover, task);