Implemented Feedback

hernanponcedeleon · Sep 13, 2024 · a2ec2c1 · a2ec2c1
1 parent 3b8c0df
commit a2ec2c1
Show file tree

Hide file tree

Showing 2 changed files with 64 additions and 40 deletions.
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java
@@ -64,7 +64,6 @@ public String toString() {
         this.wmm = new Wmm();
     }
 
-
     @Override
     public Object visitMcm(McmContext ctx) {
         super.visitMcm(ctx);

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
@@ -16,70 +16,95 @@
 public abstract class BaseOptions {
 
     @Option(
-        name=PROPERTY,
-        description="The property to check for: reachability (default), liveness, races.",
-        toUppercase=true)
-    private EnumSet<Property> property=Property.getDefault();
+            name = PROPERTY,
+            description = "The property to check for: reachability (default), liveness, races.",
+            toUppercase = true)
+    private EnumSet<Property> property = Property.getDefault();
 
-    public EnumSet<Property> getProperty() { return property; }
+    public EnumSet<Property> getProperty() {
+        return property;
+    }
 
     @Option(
-        name=VALIDATE,
-        description="Performs violation witness validation. Argument is the path to the witness file.")
+            name = VALIDATE,
+            description = "Performs violation witness validation. Argument is the path to the witness file.")
     private String witnessPath;
 
-    public boolean runValidator() { return witnessPath != null; }
-    public String getWitnessPath() { return witnessPath; }
+    public boolean runValidator() {
+        return witnessPath != null;
+    }
+
+    public String getWitnessPath() {
+        return witnessPath;
+    }
 
     @Option(
-        name=METHOD,
-        description="Solver method to be used.",
-        toUppercase=true)
-    private Method method=Method.getDefault();
+            name = METHOD,
+            description = "Solver method to be used.",
+            toUppercase = true)
+    private Method method = Method.getDefault();
 
-    public Method getMethod() { return method; }
+    public Method getMethod() {
+        return method;
+    }
 
     @Option(
-        name=SOLVER,
-        description="Uses the specified SMT solver as a backend.",
-        toUppercase=true)
-    private Solvers solver=Solvers.Z3;
+            name = SOLVER,
+            description = "Uses the specified SMT solver as a backend.",
+            toUppercase = true)
+    private Solvers solver = Solvers.Z3;
 
-    public Solvers getSolver() { return solver; }
+    public Solvers getSolver() {
+        return solver;
+    }
 
     @Option(
-        name=TIMEOUT,
-        description="Timeout (in secs) before interrupting the SMT solver.")
-    private int timeout=0;
+            name = TIMEOUT,
+            description = "Timeout (in secs) before interrupting the SMT solver.")
+    private int timeout = 0;
+
+    public boolean hasTimeout() {
+        return timeout > 0;
+    }
 
-    public boolean hasTimeout() { return timeout > 0; }
-    public int getTimeout() { return timeout; }
+    public int getTimeout() {
+        return timeout;
+    }
 
     @Option(
-        name=PHANTOM_REFERENCES,
-        description="Decrease references on Z3 formula objects once they are no longer referenced.")
-    private boolean phantomReferences=true;
+            name = PHANTOM_REFERENCES,
+            description = "Decrease references on Z3 formula objects once they are no longer referenced.")
+    private boolean phantomReferences = true;
 
-    public boolean usePhantomReferences() { return phantomReferences; }
+    public boolean usePhantomReferences() {
+        return phantomReferences;
+    }
 
     @Option(
-        name=WITNESS,
-        description="Type of the violation graph to generate in the output directory.")
-    private WitnessType witnessType=WitnessType.getDefault();
+            name = WITNESS,
+            description = "Type of the violation graph to generate in the output directory.")
+    private WitnessType witnessType = WitnessType.getDefault();
 
-    public WitnessType getWitnessType() { return witnessType; }
+    public WitnessType getWitnessType() {
+        return witnessType;
+    }
 
     @Option(
-        name=SMTLIB2,
-        description="Dump encoding to an SMTLIB2 file.")
-    private boolean smtlib=false;
+            name = SMTLIB2,
+            description = "Dump encoding to an SMTLIB2 file.")
+    private boolean smtlib = false;
 
-    public boolean getDumpSmtLib() { return smtlib; }
+    public boolean getDumpSmtLib() {
+        return smtlib;
+    }
 
     @Option(
-            name=CAT_INCLUDE,
-            description = "The directory used to resolve cat include statements. Defaults to Dartagnan's cat directory."
+            name = CAT_INCLUDE,
+            description = "The directory used to resolve cat include statements. Defaults to $DAT3M_HOME/cat."
     )
     private String catIncludePath = GlobalSettings.getCatDirectory();
-    public String getCatIncludePath() { return catIncludePath; }
+
+    public String getCatIncludePath() {
+        return catIncludePath;
+    }
 }