Refactor and optimize the design

Signed-off-by: Tianrui Zheng <[email protected]>
hernanponcedeleon · Dec 4, 2024 · 8cf4620 · 8cf4620
1 parent eaf4a79
commit 8cf4620
Show file tree

Hide file tree

Showing 19 changed files with 854 additions and 977 deletions.
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java
@@ -22,8 +22,6 @@
 import com.dat3m.dartagnan.utils.options.BaseOptions;
 import com.dat3m.dartagnan.verification.VerificationTask;
 import com.dat3m.dartagnan.verification.VerificationTask.VerificationTaskBuilder;
-import com.dat3m.dartagnan.verification.model.ExecutionModelManager;
-import com.dat3m.dartagnan.verification.model.ExecutionModelNext;
 import com.dat3m.dartagnan.verification.solving.AssumeSolver;
 import com.dat3m.dartagnan.verification.solving.DataRaceSolver;
 import com.dat3m.dartagnan.verification.solving.ModelChecker;
@@ -233,8 +231,6 @@ public static File generateExecutionGraphFile(VerificationTask task, ProverEnvir
 
         final EncodingContext encodingContext = modelChecker instanceof RefinementSolver refinementSolver ?
             refinementSolver.getContextWithFullWmm() : modelChecker.getEncodingContext();
-        final ExecutionModelManager manager = new ExecutionModelManager();
-        final ExecutionModelNext m = manager.buildExecutionModel(encodingContext, prover.getModel(), true);
         final SyntacticContextAnalysis synContext = newInstance(task.getProgram());
         final String progName = task.getProgram().getName();
         final int fileSuffixIndex = progName.lastIndexOf('.');
@@ -244,7 +240,7 @@ public static File generateExecutionGraphFile(VerificationTask task, ProverEnvir
         // we get some data flow information by observing the edge
         // FR edges only give ordering information which is known if the pair is also in PO
         // CO edges only give ordering information which is known if the pair is also in PO
-        return generateGraphvizFile(m, 1, (x, y) -> true, (x, y) -> !x.getThread().equals(y.getThread()),
+        return generateGraphvizFile(encodingContext, prover.getModel(), 1, (x, y) -> true, (x, y) -> !x.getThread().equals(y.getThread()),
                 (x, y) -> !x.getThread().equals(y.getThread()), getOrCreateOutputDirectory() + "/", name,
                 synContext, witnessType.convertToPng());
     }

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java
@@ -75,7 +75,7 @@ public class OptionNames {
 
     // Witness Options
     public static final String WITNESS_ORIGINAL_PROGRAM_PATH = "witness.originalProgramFilePath";
-    public static final String WITNESS_RELATIONS_TO_SHOW = "witness.relationsToShow";
+    public static final String WITNESS_SHOW = "witness.show";
 
     // SVCOMP Options
     public static final String PROPERTYPATH = "svcomp.property";

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/EventDomainNext.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/EventDomainNext.java
@@ -14,7 +14,7 @@ public class EventDomainNext implements Domain<EventModel> {
 
     public EventDomainNext(ExecutionModelNext executionModel) {
         this.executionModel = executionModel;
-        eventList = executionModel.getEventList();
+        eventList = executionModel.getEventModels();
     }
 
     @Override