Guard operations

hernanponcedeleon · Sep 3, 2024 · 0de6d15 · 0de6d15
1 parent 02915db
commit 0de6d15
Showing 1 changed file with 41 additions and 37 deletions.
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java
@@ -38,35 +38,39 @@ private boolean dump() {
     }
 
     private void init() {
-        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)"
-        );
-        try {
-            Files.deleteIfExists(Paths.get(fileName));
-            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");
-        } catch (IOException e) {
-            e.printStackTrace();
+        if(dump()) {
+            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)"
+            );
+            try {
+                Files.deleteIfExists(Paths.get(fileName));
+                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");
+            } catch (IOException e) {
+                e.printStackTrace();
+            }
         }
     }
 
     @Override
     public void close() throws Exception {
-        removeDuplicatedDeclarations(fileName);
-        write("(exit)\n");
+        if(dump()) {
+            removeDuplicatedDeclarations(fileName);
+            write("(exit)\n");
+        }
         prover.close();
     }
 
@@ -81,13 +85,12 @@ public boolean isUnsatWithAssumptions(Collection<BooleanFormula> fs) throws Solv
         long start = System.currentTimeMillis();
         boolean result = prover.isUnsatWithAssumptions(fs);
         long end = System.currentTimeMillis();
-        String resultString = result ? "unsat" : "sat";
         if(dump()) {
             write("(push)\n");
             for(BooleanFormula f : fs) {
                 write(fmgr.dumpFormula(f).toString());
             }
-            write("(set-info :status " + resultString + ")\n");
+            write("(set-info :status " + (result ? "unsat" : "sat") + ")\n");
             write("(check-sat)\n");
             write("; Original solving time: " + (end - start) + " ms");
             write("(pop)\n");
@@ -99,9 +102,8 @@ public boolean isUnsat() throws SolverException, InterruptedException {
         long start = System.currentTimeMillis();
         boolean result = prover.isUnsat();
         long end = System.currentTimeMillis();
-        String resultString = result ? "unsat" : "sat";
         if(dump()) {
-            write("(set-info :status " + resultString + ")\n");
+            write("(set-info :status " + (result ? "unsat" : "sat") + ")\n");
             write("(check-sat)\n");
             write("; Original solving time: " + (end - start) + " ms");
         }
@@ -131,15 +133,17 @@ public void pop() {
     }
 
     public void write(String content) {
-        File file = new File(fileName);
-        FileWriter writer;
-        try {
-            writer = new FileWriter(file, true);
-            PrintWriter printer = new PrintWriter(writer);
-            printer.append(removeDuplicatedDeclarations(content));
-            printer.close();
-        } catch (IOException e) {
-            e.printStackTrace();
+        if(dump()) {
+            File file = new File(fileName);
+            FileWriter writer;
+            try {
+                writer = new FileWriter(file, true);
+                PrintWriter printer = new PrintWriter(writer);
+                printer.append(removeDuplicatedDeclarations(content));
+                printer.close();
+            } catch (IOException e) {
+                e.printStackTrace();
+            }
         }
     }