From cce79b9667a4fd067e75d19926b22f0689756daa Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 28 Nov 2012 21:18:05 +0000 Subject: [PATCH] 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.) --- src/smt/smt_engine.cpp | 18 +++++++----------- 1 file changed, 7 insertions(+), 11 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1b031f645..7df98ef08 100644 --- 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); -- 2.30.2