Disable unconstrainedSimp pass when proofs enabled (#1976)

Currently, we may end up enabling the unconstrainedSimp pass when proofs
are enabled because the check that this pass is disabled happens before
a check for automatically enabling it. This lead to issues when running
for example on regress0/aufbv/bug00.smt with --check-proofs. This commit
moves the code for automatically enabling the pass to only be run if
proofs and unsat cores are disabled. Note: This commit is mostly a
simple code move but formatting in setDefaults was a bit off, so there
are a lot of formatting changes.

1 files changed, 143 insertions, 132 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 69cea8b06..1b5e88536 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1422,155 +1422,181 @@ void SmtEngine::setDefaults() {
       Notice() << "SmtEngine: turning on produce-assertions to support "
                << "check-models or check-synth-sol." << endl;
       setOption("produce-assertions", SExpr("true"));
-    }
+  }
 
-    if (options::unsatCores() || options::proof())
+  // Disable options incompatible with incremental solving, unsat cores, and
+  // proofs or output an error if enabled explicitly
+  if (options::incrementalSolving() || options::unsatCores()
+      || options::proof())
+  {
+    if (options::unconstrainedSimp())
     {
-      if (options::simplificationMode() != SIMPLIFICATION_MODE_NONE)
+      if (options::unconstrainedSimp.wasSetByUser())
       {
-        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);
+        throw OptionException(
+            "unconstrained simplification not supported with unsat "
+            "cores/proofs/incremental solving");
       }
-
-      if (options::unconstrainedSimp())
+      Notice() << "SmtEngine: turning off unconstrained simplification to "
+                  "support unsat cores/proofs/incremental solving"
+               << endl;
+      options::unconstrainedSimp.set(false);
+    }
+  }
+  else
+  {
+    // Turn on unconstrained simplification for QF_AUFBV
+    if (!options::unconstrainedSimp.wasSetByUser())
+    {
+      //    bool qf_sat = d_logic.isPure(THEORY_BOOL) &&
+      //    !d_logic.isQuantified(); bool uncSimp = false && !qf_sat &&
+      //    !options::incrementalSolving();
+      bool uncSimp = !d_logic.isQuantified() && !options::produceModels()
+                     && !options::produceAssignments()
+                     && !options::checkModels()
+                     && (d_logic.isTheoryEnabled(THEORY_ARRAYS)
+                         && d_logic.isTheoryEnabled(THEORY_BV));
+      Trace("smt") << "setting unconstrained simplification to " << uncSimp
+                   << endl;
+      options::unconstrainedSimp.set(uncSimp);
+    }
+  }
+
+  // Disable options incompatible with unsat cores and proofs or output an
+  // error if enabled explicitly
+  if (options::unsatCores() || options::proof())
+  {
+    if (options::simplificationMode() != SIMPLIFICATION_MODE_NONE)
+    {
+      if (options::simplificationMode.wasSetByUser())
       {
-        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);
+        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);
+    }
 
-      if (options::pbRewrites())
+    if (options::pbRewrites())
+    {
+      if (options::pbRewrites.wasSetByUser())
       {
-        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);
+        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);
+    }
 
-      if (options::sortInference())
+    if (options::sortInference())
+    {
+      if (options::sortInference.wasSetByUser())
       {
-        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);
+        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);
+    }
 
-      if (options::preSkolemQuant())
+    if (options::preSkolemQuant())
+    {
+      if (options::preSkolemQuant.wasSetByUser())
       {
-        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);
+        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);
+    }
 
-      if (options::bitvectorToBool())
+    if (options::bitvectorToBool())
+    {
+      if (options::bitvectorToBool.wasSetByUser())
       {
-        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);
+        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);
+    }
 
-      if (options::boolToBitvector())
+    if (options::boolToBitvector())
+    {
+      if (options::boolToBitvector.wasSetByUser())
       {
-        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);
+        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);
+    }
 
-      if (options::bvIntroducePow2())
+    if (options::bvIntroducePow2())
+    {
+      if (options::bvIntroducePow2.wasSetByUser())
       {
-        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);
+        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);
+    }
 
-      if (options::repeatSimp())
+    if (options::repeatSimp())
+    {
+      if (options::repeatSimp.wasSetByUser())
       {
-        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);
+        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);
+    }
 
-      if (options::globalNegate())
+    if (options::globalNegate())
+    {
+      if (options::globalNegate.wasSetByUser())
       {
-        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);
+        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);
     }
-    else
+  }
+  else
+  {
+    // by default, nonclausal simplification is off for QF_SAT
+    if (!options::simplificationMode.wasSetByUser())
     {
-      // 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);
-      }
+      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())
@@ -1717,21 +1743,6 @@ void SmtEngine::setDefaults() {
     Trace("smt") << "setting repeat simplification to " << repeatSimp << endl;
     options::repeatSimp.set(repeatSimp);
   }
-  // Turn on unconstrained simplification for QF_AUFBV
-  if(!options::unconstrainedSimp.wasSetByUser() ||
-      options::incrementalSolving()) {
-    //    bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
-    //    bool uncSimp = false && !qf_sat && !options::incrementalSolving();
-    bool uncSimp = !options::incrementalSolving() &&
-                   !d_logic.isQuantified() &&
-                   !options::produceModels() &&
-                   !options::produceAssignments() &&
-                   !options::checkModels() &&
-                   !options::unsatCores() &&
-                   (d_logic.isTheoryEnabled(THEORY_ARRAYS) && d_logic.isTheoryEnabled(THEORY_BV));
-    Trace("smt") << "setting unconstrained simplification to " << uncSimp << endl;
-    options::unconstrainedSimp.set(uncSimp);
-  }
   // Unconstrained simp currently does *not* support model generation
   if (options::unconstrainedSimp.wasSetByUser() && options::unconstrainedSimp()) {
     if (options::produceModels()) {