Add TaskSolver as abstraction layer over ModelChecker

dartagnan/pom.xml

@@ -253,6 +253,8 @@
                         </buildArgs>
                         <initializeAtBuildTime>
                             <!-- Every class should also be registered in OptionsInfo and reflect-config.json -->
+                            <className>com.dat3m.dartagnan.witness.graphviz.ExecutionGraphVisualizer</className>
+                            <className>com.dat3m.dartagnan.verification.TaskSolver</className>
                             <className>com.dat3m.dartagnan.wmm.RelationNameRepository</className>
                             <className>com.dat3m.dartagnan.configuration.OptionNames</className>
                             <className>com.dat3m.dartagnan.wmm.axiom.Acyclicity</className>

dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionInfo.java

@@ -9,8 +9,10 @@
 import com.dat3m.dartagnan.solver.caat4wmm.coreReasoning.CoreReasoner;
 import com.dat3m.dartagnan.utils.options.BaseOptions;
 import com.dat3m.dartagnan.utils.printer.Printer;
+import com.dat3m.dartagnan.verification.TaskSolver;
 import com.dat3m.dartagnan.verification.solving.ModelChecker;
 import com.dat3m.dartagnan.verification.solving.RefinementSolver;
+import com.dat3m.dartagnan.witness.graphviz.ExecutionGraphVisualizer;
 import com.dat3m.dartagnan.wmm.RelationNameRepository;
 import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis;
 import com.dat3m.dartagnan.wmm.analysis.WmmAnalysis;
@@ -31,16 +33,13 @@
 
 public final class OptionInfo implements Comparable<OptionInfo> {
 
-    public static void collectOptions() {
-        stream().sorted().forEach(System.out::print);
-    }
-
     public static Stream<OptionInfo> stream() {
         return classes().flatMap(OptionInfo::collectOptions);
     }
 
     private static Stream<Class<?>> classes() {
         return Stream.of(
+                TaskSolver.class,
                 RelationNameRepository.class,
                 OptionNames.class,
                 Acyclicity.class,
@@ -71,7 +70,8 @@ private static Stream<Class<?>> classes() {
                 RefinementSolver.class,
                 RelationAnalysis.Config.class,
                 WmmAnalysis.class,
-                WmmProcessingManager.class
+                WmmProcessingManager.class,
+                ExecutionGraphVisualizer.class
         );
     }
 

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/ProgramParser.java

@@ -2,12 +2,14 @@
 
 import com.dat3m.dartagnan.exception.ParsingException;
 import com.dat3m.dartagnan.program.Program;
+import com.google.common.io.Files;
 import org.antlr.v4.runtime.CharStream;
 import org.antlr.v4.runtime.CharStreams;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
 import java.io.*;
+import java.nio.file.Path;
 import java.util.List;
 
 import static com.dat3m.dartagnan.parsers.program.utils.Compilation.compileWithClang;
@@ -34,6 +36,11 @@ public class ProgramParser {
     public static final List<String> SUPPORTED_EXTENSIONS = List.of(
             EXTENSION_C, EXTENSION_I, EXTENSION_LL, EXTENSION_LITMUS, EXTENSION_SPV_DIS, EXTENSION_SPVASM);
 
+    public static boolean isSupported(Path filePath) {
+        final String extension = "." + Files.getFileExtension(filePath.getFileName().toString());
+        return SUPPORTED_EXTENSIONS.contains(extension);
+    }
+
     public Program parse(File file) throws Exception {
         if (needsClang(file)) {
             file = compileWithClang(file, "");

dartagnan/src/main/java/com/dat3m/dartagnan/utils/GitInfo.java

@@ -1,7 +1,6 @@
 package com.dat3m.dartagnan.utils;
 
 import com.dat3m.dartagnan.Dartagnan;
-
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
@@ -13,7 +12,7 @@ public class GitInfo {
 
     private static final Logger logger = LoggerFactory.getLogger(GitInfo.class);
 
-    static Properties properties = new Properties();
+    private final static Properties properties = new Properties();
 
     public static void initGitInfo() throws IOException {
         try (InputStream is = Dartagnan.class.getClassLoader()

dartagnan/src/main/java/com/dat3m/dartagnan/utils/printer/OutputLogger.java

@@ -26,18 +26,22 @@ public void addResult(ResultSummary result) {
         results.add(result);
     }
 
-    public void toStdOut(boolean batchMode) {
-        if (batchMode) {
+    public void toStdOut() {
+        if (results.isEmpty()) {
+            return;
+        }
+
+        if (results.size() == 1) {
+            System.out.println(results.get(0));
+        } else {
             System.out.println("================ Configuration ==================");
             System.out.println("cat = " + modelFile);
             System.out.print(config.asPropertiesString()); // it already contains its own \n
             System.out.println("=================================================");
-        }
-        for (ResultSummary r : results) {
-            if (batchMode) {
+            for (ResultSummary r : results) {
                 System.out.println();
+                System.out.println(r);
             }
-            System.out.println(r);
         }
     }