diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 78 |
1 files changed, 45 insertions, 33 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7cac970f8..4887ef540 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -248,6 +248,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_problemExtended(false), d_queryMade(false), d_needPostsolve(false), + d_earlyTheoryPP(true), d_timeBudgetCumulative(0), d_timeBudgetPerCall(0), d_resourceBudgetCumulative(0), @@ -489,6 +490,10 @@ void SmtEngine::setLogicInternal() throw(AssertionException) { Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << std::endl; NodeManager::currentNM()->getOptions()->arithRewriteEq = arithRewriteEq; } + // Turn off early theory preprocessing if arithRewriteEq is on + if (NodeManager::currentNM()->getOptions()->arithRewriteEq) { + d_earlyTheoryPP = false; + } } void SmtEngine::setInfo(const std::string& key, const SExpr& value) @@ -1149,19 +1154,6 @@ void SmtEnginePrivate::simplifyAssertions() Trace("simplify") << "SmtEnginePrivate::simplify()" << endl; - if(!Options::current()->lazyDefinitionExpansion) { - Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl; - TimerStat::CodeTimer codeTimer(d_smt.d_definitionExpansionTime); - hash_map<TNode, Node, TNodeHashFunction> cache; - for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { - d_assertionsToPreprocess[i] = - expandDefinitions(d_assertionsToPreprocess[i], cache); - } - } - - Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; - Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; - if(Options::current()->simplificationMode != Options::SIMPLIFICATION_MODE_NONE) { // Perform non-clausal simplification Trace("simplify") << "SmtEnginePrivate::simplify(): " @@ -1178,11 +1170,22 @@ void SmtEnginePrivate::simplifyAssertions() Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + // Theory preprocessing + if (d_smt.d_earlyTheoryPP) { + TimerStat::CodeTimer codeTimer(d_smt.d_theoryPreprocessTime); + // Call the theory preprocessors + d_smt.d_theoryEngine->preprocessStart(); + for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { + d_assertionsToCheck[i] = d_smt.d_theoryEngine->preprocess(d_assertionsToCheck[i]); + } + } + + // ITE simplification if(Options::current()->doITESimp) { - // ite simplification simpITE(); } + // Unconstrained simplification if(Options::current()->unconstrainedSimp) { unconstrainedSimp(); } @@ -1197,16 +1200,6 @@ void SmtEnginePrivate::simplifyAssertions() d_smt.d_userContext->pop(); } - Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; - Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; - - if(Options::current()->doStaticLearning) { - // Perform static learning - Trace("simplify") << "SmtEnginePrivate::simplify(): " - << "performing static learning" << endl; - staticLearning(); - } - } catch(TypeCheckingExceptionPrivate& tcep) { // Calls to this function should have already weeded out any // typechecking exceptions via (e.g.) ensureBoolean(). But a @@ -1292,9 +1285,25 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; - // Simplify the assertions + if(!Options::current()->lazyDefinitionExpansion) { + Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl; + TimerStat::CodeTimer codeTimer(d_smt.d_definitionExpansionTime); + hash_map<TNode, Node, TNodeHashFunction> cache; + for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { + d_assertionsToPreprocess[i] = + expandDefinitions(d_assertionsToPreprocess[i], cache); + } + } + simplifyAssertions(); + if(Options::current()->doStaticLearning) { + // Perform static learning + Trace("simplify") << "SmtEnginePrivate::simplify(): " + << "performing static learning" << endl; + staticLearning(); + } + // any assertions beyond realAssertionsEnd _must_ be introduced by // removeITEs(). int realAssertionsEnd = d_assertionsToCheck.size(); @@ -1313,6 +1322,9 @@ void SmtEnginePrivate::processAssertions() { removeITEs(); } + Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; + Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + // begin: INVARIANT to maintain: no reordering of assertions or // introducing new ones #ifdef CVC4_ASSERTIONS @@ -1323,14 +1335,6 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; - if(Dump.isOn("assertions")) { - // Push the simplified assertions to the dump output stream - for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { - Dump("assertions") - << AssertCommand(BoolExpr(d_assertionsToCheck[i].toExpr())); - } - } - { TimerStat::CodeTimer codeTimer(d_smt.d_theoryPreprocessTime); // Call the theory preprocessors @@ -1340,6 +1344,14 @@ void SmtEnginePrivate::processAssertions() { } } + if(Dump.isOn("assertions")) { + // Push the simplified assertions to the dump output stream + for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { + Dump("assertions") + << AssertCommand(BoolExpr(d_assertionsToCheck[i].toExpr())); + } + } + // Push the formula to decision engine Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size()); d_smt.d_decisionEngine->addAssertions |