diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-12 20:35:07 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-12 20:35:07 +0000 |
commit | 43a09137c2abd4902ce622afa445a9cb59e2352d (patch) | |
tree | 3086a6af95a29af036a7b28a08fb3fd56d60a051 | |
parent | e31f8ec3eeacff9b7818287eaa9b58ebc9cd3958 (diff) |
Moved some things around in the preprocessor. Now theory preprocessing gets
called before ite simplification unless arithrewriteequality is on
-rw-r--r-- | src/smt/smt_engine.cpp | 78 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 5 |
2 files changed, 50 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 diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 0873aea96..11f3bdcb9 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -163,6 +163,11 @@ class CVC4_PUBLIC SmtEngine { */ bool d_needPostsolve; + /* + * Whether to call theory preprocessing during simplification - on by default* but gets turned off if arithRewriteEq is on + */ + bool d_earlyTheoryPP; + /** A user-imposed cumulative time budget, in milliseconds. 0 = no limit. */ unsigned long d_timeBudgetCumulative; /** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */ |