- Implemented support for Mathsat and Z3 in my Benchmark class

Author: DavidGalllob

src/org/sosy_lab/java_smt/utils/ParseGenerateAndReparse.java

@@ -31,12 +31,6 @@ private ParseGenerateAndReparse() {}
 
   public static void main(String[] args)
       throws InvalidConfigurationException, InterruptedException, SolverException {
-    String expectedResult =
-        "(declare-const a (_ FloatingPoint 8 24))\n"
-            + "(declare-const b (_ FloatingPoint 8 24))\n"
-            + "(declare-const min (_ FloatingPoint 8 24))\n"
-            + "(assert (fp.eq (fp.min a b) min))\n";
-    System.out.println(nativeZ3ParseAndIsUnsat(expectedResult));
     if (args.length < 3) {
       System.err.println("Usage: java ParseGenerateAndReparseTest <smt2-file> <solver> <mode>");
       System.exit(1);
@@ -84,15 +78,15 @@ public static void main(String[] args)
         Generator.assembleConstraint(formula);
         String regenerated = Generator.getSMTLIB2String();
         // NATIVE PARSE
-        checkResult(nativeZ3ParseAndIsUnsat(regenerated));
+        checkResult(checkNativeParseAndIsUnsat(solver, regenerated));
       } catch (Exception pE) {
         printError(pE);
       }
     }
     if (mode.equals("NATIVE")) {
       try {
         // NATIVE PARSE
-        checkResult(nativeZ3ParseAndIsUnsat(smt2FilePath));
+        checkResult(checkNativeParseAndIsUnsat(solver, smt2FilePath));
       } catch (Exception pE) {
         printError(pE);
       }
@@ -121,6 +115,14 @@ public static void checkResult(boolean isUnsat) {
     System.out.println("SUCCESS: isUnsat = " + isUnsat);
     System.exit(0);
   }
+  public static boolean checkNativeParseAndIsUnsat(Solvers solver, String smt2)
+      throws SolverException, InterruptedException, InvalidConfigurationException {
+    switch (solver){
+      case Z3: return nativeZ3ParseAndIsUnsat(smt2);
+      case MATHSAT5: return nativeMathSatParseAndIsUnsat(smt2);
+    }
+    throw new SolverException("Unsupported solver: " + solver);
+  }
 
   public static boolean nativeZ3ParseAndIsUnsat(String smt2) {
     try (Context ctx = new Context()) {
@@ -131,6 +133,14 @@ public static boolean nativeZ3ParseAndIsUnsat(String smt2) {
     }
   }
 
+  public static boolean nativeMathSatParseAndIsUnsat(String smt2)
+      throws InvalidConfigurationException, InterruptedException, SolverException {
+    SolverContext mathsat = SolverContextFactory.createSolverContext(Solvers.MATHSAT5);
+    ProverEnvironment prover = mathsat.newProverEnvironment(ProverOptions.GENERATE_MODELS);
+    prover.addConstraint(mathsat.getFormulaManager().parse(smt2));
+    return prover.isUnsat();
+  }
+
   public static void printError(Exception pE) {
     System.out.println("ERROR: ");
     pE.printStackTrace();