Merge pull request #542 from sosy-lab/add_mathsat5_extended_parsing

Allow Mathsat to use its extended dumping method (allowing let-expressions and quantifier dumping) with new options

Author: baierd

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaManager.java

@@ -13,6 +13,7 @@
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_copy_from;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_simplify;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_to_smtlib2;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_to_smtlib2_ext;
 
 import com.google.common.collect.Collections2;
 import com.google.common.primitives.Longs;
@@ -26,6 +27,9 @@
 
 final class Mathsat5FormulaManager extends AbstractFormulaManager<Long, Long, Long, Long> {
 
+  private final boolean dumpExtendedOutput;
+  private final boolean dumpLetExpressions;
+
   @SuppressWarnings("checkstyle:parameternumber")
   Mathsat5FormulaManager(
       Mathsat5FormulaCreator creator,
@@ -36,7 +40,9 @@ final class Mathsat5FormulaManager extends AbstractFormulaManager<Long, Long, Lo
       Mathsat5BitvectorFormulaManager pBitpreciseManager,
       Mathsat5FloatingPointFormulaManager pFloatingPointManager,
       Mathsat5ArrayFormulaManager pArrayManager,
-      Mathsat5EnumerationFormulaManager pEnumerationManager) {
+      Mathsat5EnumerationFormulaManager pEnumerationManager,
+      boolean pDumpExtendedOutput,
+      boolean pDumpLetExpressions) {
     super(
         creator,
         pFunctionManager,
@@ -50,6 +56,8 @@ final class Mathsat5FormulaManager extends AbstractFormulaManager<Long, Long, Lo
         null,
         null,
         pEnumerationManager);
+    dumpLetExpressions = pDumpLetExpressions;
+    dumpExtendedOutput = pDumpExtendedOutput;
   }
 
   static long getMsatTerm(Formula pT) {
@@ -69,7 +77,16 @@ public Long parseImpl(String pS) throws IllegalArgumentException {
   public String dumpFormulaImpl(final Long f) {
     assert getFormulaCreator().getFormulaType(f) == FormulaType.BooleanType
         : "Only BooleanFormulas may be dumped";
-    return msat_to_smtlib2(getEnvironment(), f);
+
+    if (dumpExtendedOutput) {
+      // msat_to_smtlib2_ext() can export quantified formulas created in MathSAT5 (which it can't
+      // solve). Can generate let-expressions instead of define-fun bindings.
+      return msat_to_smtlib2_ext(getFormulaCreator().getEnv(), f, "", dumpLetExpressions ? 0 : 1);
+    } else {
+      // msat_to_smtlib2() generates `.def_...` expressions, which are disliked by some solvers
+      // (due to the . being a SMTLIB2 reserved symbol at the beginning of definitions)
+      return msat_to_smtlib2(getEnvironment(), f);
+    }
   }
 
   @Override

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java

@@ -60,6 +60,26 @@ private static final class Mathsat5Settings {
                 + "Format is 'key1=value1,key2=value2'")
     private String furtherOptions = "";
 
+    @Option(
+        secure = true,
+        description =
+            "If enabled, SMTLIB2 output of MathSAT5 will be generated using the extended dumping "
+                + "function msat_to_smtlib2_ext(), instead of the regular dumping "
+                + "function msat_to_smtlib2(). This extended dump might allow the exporting of "
+                + "features to SMTLIB2 that can't be solved using MathSAT5, e.g. quantified "
+                + "formulas. "
+                + "The output will contain define-fun based bindings instead of "
+                + "let-expressions per default. If you want to use let bindings, enable option "
+                + "solver.mathsat5.dumpSMTLIB2LetExpressions as well.")
+    private boolean useExtendedSMTLIB2Output = false;
+
+    @Option(
+        secure = true,
+        description =
+            "If used together with solver.mathsat5.useExtendedSMTLIB2Output, SMTLIB2 output will "
+                + "contain let-bindings instead of define-fun based bindings.")
+    private boolean dumpSMTLIB2LetExpressions = false;
+
     @Option(secure = true, description = "Load less stable optimizing version of mathsat5 solver.")
     boolean loadOptimathsat5 = false;
 
@@ -206,7 +226,9 @@ public static Mathsat5SolverContext create(
             bitvectorTheory,
             floatingPointTheory,
             arrayTheory,
-            enumerationTheory);
+            enumerationTheory,
+            settings.useExtendedSMTLIB2Output,
+            settings.dumpSMTLIB2LetExpressions);
     return new Mathsat5SolverContext(
         logger, msatConf, settings, randomSeed, pShutdownNotifier, manager, creator);
   }