Attempted "quick-fix" for QF_UF performance regression since Boolean terms added.

Sharing is turned on only when Boolean terms are detected during preprocessing.  QF_UF problems (and others)
that don't use any Boolean terms won't have BV turned on.

(this commit was certified error- and warning-free by the test-and-commit script.)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1b031f645c2fc56a851e8a02c8eec7603e69b813..7df98ef089ae0a24b9182ead2c443cabc6e1e5c3 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -961,15 +961,6 @@ void SmtEngine::setLogicInternal() throw() {
       setOption("check-models", SExpr("false"));
     }
   }
-
-  // may need to force BV on to handle Boolean terms
-  // except in pure arith and QF_SAT
-  if(!d_logic.isPure(theory::THEORY_ARITH) &&
-     !d_logic.isPure(theory::THEORY_BOOL)) {
-    d_logic = d_logic.getUnlockedCopy();
-    d_logic.enableTheory(theory::THEORY_BV);
-    d_logic.lock();
-  }
 }
 
 void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
@@ -2087,8 +2078,13 @@ void SmtEnginePrivate::processAssertions() {
     Chat() << "rewriting Boolean terms..." << endl;
     TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime);
     for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) {
-      d_assertionsToPreprocess[i] =
-        d_booleanTermConverter.rewriteBooleanTerms(d_assertionsToPreprocess[i]);
+      Node n = d_booleanTermConverter.rewriteBooleanTerms(d_assertionsToPreprocess[i]);
+      if(n != d_assertionsToPreprocess[i] && !d_smt.d_logic.isTheoryEnabled(theory::THEORY_BV)) {
+        d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+        d_smt.d_logic.enableTheory(theory::THEORY_BV);
+        d_smt.d_logic.lock();
+      }
+      d_assertionsToPreprocess[i] = n;
     }
   }
   dumpAssertions("post-boolean-terms", d_assertionsToPreprocess);