Smtlib2

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) {

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";

dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java

@@ -0,0 +1,185 @@
+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<String> 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();
+    }
+
+    public Void addConstraint(BooleanFormula f) throws InterruptedException {
+        if(dump()) {
+            write(fmgr.dumpFormula(f).toString());
+        }
+        return prover.addConstraint(f);
+    }
+
+    public boolean isUnsatWithAssumptions(Collection<BooleanFormula> fs) throws SolverException, InterruptedException {
+        long start = System.currentTimeMillis();
+        boolean result = prover.isUnsatWithAssumptions(fs);
+        long end = System.currentTimeMillis();
+        if(dump()) {
+            write("(push)\n");
+            for(BooleanFormula f : fs) {
+                write(fmgr.dumpFormula(f).toString());
+            }
+            write("(set-info :status " + (result ? "unsat" : "sat") + ")\n");
+            write("(check-sat)\n");
+            write("; Original solving time: " + (end - start) + " ms");
+            write("(pop)\n");
+        }
+        return result;
+    }
+
+    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");
+            write("; Original solving time: " + (end - start) + " ms");
+        }
+        return result;
+    }
+
+    public ImmutableMap<String, String> getStatistics() {
+        return prover.getStatistics();
+    }
+
+    public Model getModel() throws SolverException {
+        return prover.getModel();
+    }
+
+    public void push() throws InterruptedException {
+        if(dump()) {
+            write("(push)\n");
+        }
+        prover.push();
+    }
+
+    public void pop() {
+        if(dump()) {
+            write("(pop)\n");
+        }
+        prover.pop();
+    }
+
+    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);
+    }
+
+    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;
+    }
+
+    @Override
+    public <R> R allSat(AllSatCallback<R> arg0, List<BooleanFormula> arg1) throws InterruptedException, SolverException {
+        return prover.allSat(arg0, arg1);
+    }
+
+    @Override
+    public List<BooleanFormula> getUnsatCore() {
+        return prover.getUnsatCore();
+    }
+
+    @Override
+    public int size() {
+        return prover.size();
+    }
+
+    @Override
+    public Optional<List<BooleanFormula>> unsatCoreOverAssumptions(Collection<BooleanFormula> arg0)
+            throws SolverException, InterruptedException {
+        return prover.unsatCoreOverAssumptions(arg0);
+    }
+}

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;

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; }
 }

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;