Set same options for proofs as for unsat cores (#1957)

In SmtEngine::setDefaults() we were setting options such as
--simplifciation=none for unsat cores but not proofs. Producing unsat
cores relies on the same infrastructure as proofs and should be a subset
of the same work in most cases. Thus, this commit changes
SmtEngine::setDefaults() to set the same options for proofs as we
previously only did for unsat cores. Additionally, it changes the
function to only set the simplificationMode to SIMPLIFICATION_MODE_BATCH
if proofs and unsat cores are not enabled. Fixes issue #1953.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e96393f1197401faa2e45c6cd6714c5fa7042414..1145273348d273a8430e8beee04f872a0584ae08 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1419,90 +1419,153 @@ void SmtEngine::setDefaults() {
       setOption("produce-assertions", SExpr("true"));
     }
 
-  if(options::unsatCores()) {
-    if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE) {
-      if(options::simplificationMode.wasSetByUser()) {
-        throw OptionException("simplification not supported with unsat cores");
+    if (options::unsatCores() || options::proof())
+    {
+      if (options::simplificationMode() != SIMPLIFICATION_MODE_NONE)
+      {
+        if (options::simplificationMode.wasSetByUser())
+        {
+          throw OptionException(
+              "simplification not supported with unsat cores/proofs");
+        }
+        Notice() << "SmtEngine: turning off simplification to support unsat "
+                    "cores/proofs"
+                 << endl;
+        options::simplificationMode.set(SIMPLIFICATION_MODE_NONE);
       }
-      Notice() << "SmtEngine: turning off simplification to support unsat-cores"
-               << endl;
-      options::simplificationMode.set(SIMPLIFICATION_MODE_NONE);
-    }
 
-    if(options::unconstrainedSimp()) {
-      if(options::unconstrainedSimp.wasSetByUser()) {
-        throw OptionException("unconstrained simplification not supported with unsat cores");
+      if (options::unconstrainedSimp())
+      {
+        if (options::unconstrainedSimp.wasSetByUser())
+        {
+          throw OptionException(
+              "unconstrained simplification not supported with unsat "
+              "cores/proofs");
+        }
+        Notice() << "SmtEngine: turning off unconstrained simplification to "
+                    "support unsat cores/proofs"
+                 << endl;
+        options::unconstrainedSimp.set(false);
       }
-      Notice() << "SmtEngine: turning off unconstrained simplification to support unsat-cores" << endl;
-      options::unconstrainedSimp.set(false);
-    }
 
-    if(options::pbRewrites()) {
-      if(options::pbRewrites.wasSetByUser()) {
-        throw OptionException("pseudoboolean rewrites not supported with unsat cores");
+      if (options::pbRewrites())
+      {
+        if (options::pbRewrites.wasSetByUser())
+        {
+          throw OptionException(
+              "pseudoboolean rewrites not supported with unsat cores/proofs");
+        }
+        Notice() << "SmtEngine: turning off pseudoboolean rewrites to support "
+                    "unsat cores/proofs"
+                 << endl;
+        setOption("pb-rewrites", false);
       }
-      Notice() << "SmtEngine: turning off pseudoboolean rewrites to support unsat-cores" << endl;
-      setOption("pb-rewrites", false);
-    }
 
-    if(options::sortInference()) {
-      if(options::sortInference.wasSetByUser()) {
-        throw OptionException("sort inference not supported with unsat cores");
+      if (options::sortInference())
+      {
+        if (options::sortInference.wasSetByUser())
+        {
+          throw OptionException(
+              "sort inference not supported with unsat cores/proofs");
+        }
+        Notice() << "SmtEngine: turning off sort inference to support unsat "
+                    "cores/proofs"
+                 << endl;
+        options::sortInference.set(false);
       }
-      Notice() << "SmtEngine: turning off sort inference to support unsat-cores" << endl;
-      options::sortInference.set(false);
-    }
 
-    if(options::preSkolemQuant()) {
-      if(options::preSkolemQuant.wasSetByUser()) {
-        throw OptionException("pre-skolemization not supported with unsat cores");
+      if (options::preSkolemQuant())
+      {
+        if (options::preSkolemQuant.wasSetByUser())
+        {
+          throw OptionException(
+              "pre-skolemization not supported with unsat cores/proofs");
+        }
+        Notice() << "SmtEngine: turning off pre-skolemization to support unsat "
+                    "cores/proofs"
+                 << endl;
+        options::preSkolemQuant.set(false);
       }
-      Notice() << "SmtEngine: turning off pre-skolemization to support unsat-cores" << endl;
-      options::preSkolemQuant.set(false);
-    }
 
-    if(options::bitvectorToBool()) {
-      if(options::bitvectorToBool.wasSetByUser()) {
-        throw OptionException("bv-to-bool not supported with unsat cores");
+      if (options::bitvectorToBool())
+      {
+        if (options::bitvectorToBool.wasSetByUser())
+        {
+          throw OptionException(
+              "bv-to-bool not supported with unsat cores/proofs");
+        }
+        Notice() << "SmtEngine: turning off bitvector-to-bool to support unsat "
+                    "cores/proofs"
+                 << endl;
+        options::bitvectorToBool.set(false);
       }
-      Notice() << "SmtEngine: turning off bitvector-to-bool to support unsat-cores" << endl;
-      options::bitvectorToBool.set(false);
-    }
 
-    if(options::boolToBitvector()) {
-      if(options::boolToBitvector.wasSetByUser()) {
-        throw OptionException("bool-to-bv not supported with unsat cores");
+      if (options::boolToBitvector())
+      {
+        if (options::boolToBitvector.wasSetByUser())
+        {
+          throw OptionException(
+              "bool-to-bv not supported with unsat cores/proofs");
+        }
+        Notice() << "SmtEngine: turning off bool-to-bitvector to support unsat "
+                    "cores/proofs"
+                 << endl;
+        options::boolToBitvector.set(false);
       }
-      Notice() << "SmtEngine: turning off bool-to-bitvector to support unsat-cores" << endl;
-      options::boolToBitvector.set(false);
-    }
 
-    if(options::bvIntroducePow2()) {
-      if(options::bvIntroducePow2.wasSetByUser()) {
-        throw OptionException("bv-intro-pow2 not supported with unsat cores");
+      if (options::bvIntroducePow2())
+      {
+        if (options::bvIntroducePow2.wasSetByUser())
+        {
+          throw OptionException(
+              "bv-intro-pow2 not supported with unsat cores/proofs");
+        }
+        Notice() << "SmtEngine: turning off bv-intro-pow2 to support "
+                    "unsat-cores/proofs"
+                 << endl;
+        setOption("bv-intro-pow2", false);
       }
-      Notice() << "SmtEngine: turning off bv-intro-pow2 to support unsat-cores" << endl;
-      setOption("bv-intro-pow2", false);
-    }
 
-    if(options::repeatSimp()) {
-      if(options::repeatSimp.wasSetByUser()) {
-        throw OptionException("repeat-simp not supported with unsat cores");
+      if (options::repeatSimp())
+      {
+        if (options::repeatSimp.wasSetByUser())
+        {
+          throw OptionException(
+              "repeat-simp not supported with unsat cores/proofs");
+        }
+        Notice() << "SmtEngine: turning off repeat-simp to support unsat "
+                    "cores/proofs"
+                 << endl;
+        setOption("repeat-simp", false);
       }
-      Notice() << "SmtEngine: turning off repeat-simp to support unsat-cores" << endl;
-      setOption("repeat-simp", false);
-    }
 
-    if (options::globalNegate())
-    {
-      if (options::globalNegate.wasSetByUser())
+      if (options::globalNegate())
       {
-        throw OptionException("global-negate not supported with unsat cores");
+        if (options::globalNegate.wasSetByUser())
+        {
+          throw OptionException(
+              "global-negate not supported with unsat cores/proofs");
+        }
+        Notice() << "SmtEngine: turning off global-negate to support unsat "
+                    "cores/proofs"
+                 << endl;
+        setOption("global-negate", false);
       }
-      Notice() << "SmtEngine: turning off global-negate to support unsat-cores"
-               << endl;
-      setOption("global-negate", false);
     }
+    else
+    {
+      // by default, nonclausal simplification is off for QF_SAT
+      if (!options::simplificationMode.wasSetByUser())
+      {
+        bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
+        Trace("smt") << "setting simplification mode to <"
+                     << d_logic.getLogicString() << "> " << (!qf_sat) << endl;
+        // simplification=none works better for SMT LIB benchmarks with
+        // quantifiers, not others options::simplificationMode.set(qf_sat ||
+        // quantifiers ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
+        options::simplificationMode.set(qf_sat ? SIMPLIFICATION_MODE_NONE
+                                               : SIMPLIFICATION_MODE_BATCH);
+      }
   }
 
   if (options::cbqiBv() && d_logic.isQuantified())
@@ -1570,14 +1633,6 @@ void SmtEngine::setDefaults() {
     Trace("smt") << "setting uf symmetry breaker to " << qf_uf << endl;
     options::ufSymmetryBreaker.set(qf_uf);
   }
-  // by default, nonclausal simplification is off for QF_SAT
-  if(! options::simplificationMode.wasSetByUser()) {
-    bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
-    Trace("smt") << "setting simplification mode to <" << d_logic.getLogicString() << "> " << (!qf_sat) << endl;
-    //simplification=none works better for SMT LIB benchmarks with quantifiers, not others
-    //options::simplificationMode.set(qf_sat || quantifiers ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
-    options::simplificationMode.set(qf_sat ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
-  }
 
   // If in arrays, set the UF handler to arrays
   if(d_logic.isTheoryEnabled(THEORY_ARRAYS) && ( !d_logic.isQuantified() ||

diff --git a/test/regress/regress0/arith/bug569.smt2 b/test/regress/regress0/arith/bug569.smt2
index e1ca49ac5d65d9f312c997e03b6824b9801a2ced..1a63f265b71237f3e3d67036153aaa18517a3627 100644 (file)
--- a/test/regress/regress0/arith/bug569.smt2
+++ b/test/regress/regress0/arith/bug569.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-unsat-cores
+; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
 ; EXPECT: unsat
 (set-logic QF_AUFLIRA)
 (set-info :smt-lib-version 2.0)

diff --git a/test/regress/regress0/quantifiers/lra-triv-gn.smt2 b/test/regress/regress0/quantifiers/lra-triv-gn.smt2
index ccd31c46371596052b8263132d5a81c487ab7b8c..1598f7097eb42d67ff92d5ce05ceb0d9ea7e6313 100644 (file)
--- a/test/regress/regress0/quantifiers/lra-triv-gn.smt2
+++ b/test/regress/regress0/quantifiers/lra-triv-gn.smt2
@@ -1,7 +1,7 @@
-; COMMAND-LINE: --global-negate --no-check-unsat-cores
+; COMMAND-LINE: --global-negate --no-check-unsat-cores --no-check-proofs
 ; EXPECT: unsat
 (set-logic LRA)
 (set-info :status unsat)
 (assert (not (exists ((?X Real)) (>= (/ (- 13) 4) ?X))))
 (check-sat)
-(exit)
\ No newline at end of file
+(exit)