diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-02-20 14:48:22 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-02-20 14:48:22 +0000 |
commit | a426d4b7795a173d6a50418a38a3b41bbfaf880d (patch) | |
tree | 0687d074dd73c5b474538814e1c5f29207f48ab1 | |
parent | 96240c3cbc2a25e2d9ab14d1048ffda82a83ded2 (diff) |
Added Theory::postsolve() infrastructure as Clark requested.
(Though currently unused.)
For theories that request presolve and postsolve (in their kinds file),
they will get a presolve() notification before the first check(). After
the final check during the current search, they get a postsolve().
presolve() and postsolve() notifications always come in pairs, bracketing
all check()/propagate()/getValue() calls related to a single query. In
the case of incremental benchmarks, theories may get additional
presolve()/postsolve() pairs, but again, they always come in pairs.
Expected performance impact: none (for theories that don't use it)
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3598&reference_id=3581&p=5
-rw-r--r-- | src/smt/smt_engine.cpp | 36 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 6 | ||||
-rwxr-xr-x | src/theory/mktheorytraits | 6 | ||||
-rw-r--r-- | src/theory/theory.h | 12 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 24 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 5 |
6 files changed, 87 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f8667fb71..f9539a1a4 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -194,6 +194,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_logic(""), d_problemExtended(false), d_queryMade(false), + d_needPostsolve(false), d_timeBudgetCumulative(0), d_timeBudgetPerCall(0), d_resourceBudgetCumulative(0), @@ -253,6 +254,13 @@ void SmtEngine::shutdown() { if(Dump.isOn("benchmark")) { Dump("benchmark") << QuitCommand() << endl; } + + // check to see if a postsolve() is pending + if(d_needPostsolve) { + d_theoryEngine->postsolve(); + d_needPostsolve = false; + } + d_propEngine->shutdown(); d_theoryEngine->shutdown(); } @@ -863,6 +871,12 @@ Result SmtEngine::checkSat(const BoolExpr& e) { ensureBoolean(e); } + // check to see if a postsolve() is pending + if(d_needPostsolve) { + d_theoryEngine->postsolve(); + d_needPostsolve = false; + } + // Push the context internalPush(); @@ -877,6 +891,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) { // Run the check Result r = check().asSatisfiabilityResult(); + d_needPostsolve = true; // Dump the query if requested if(Dump.isOn("benchmark")) { @@ -915,6 +930,12 @@ Result SmtEngine::query(const BoolExpr& e) { // Ensure that the expression is type-checked at this point, and Boolean ensureBoolean(e); + // check to see if a postsolve() is pending + if(d_needPostsolve) { + d_theoryEngine->postsolve(); + d_needPostsolve = false; + } + // Push the context internalPush(); @@ -927,6 +948,7 @@ Result SmtEngine::query(const BoolExpr& e) { // Run the check Result r = check().asValidityResult(); + d_needPostsolve = true; // Dump the query if requested if(Dump.isOn("benchmark")) { @@ -1157,6 +1179,13 @@ void SmtEngine::push() { if(!Options::current()->incrementalSolving) { throw ModalException("Cannot push when not solving incrementally (use --incremental)"); } + + // check to see if a postsolve() is pending + if(d_needPostsolve) { + d_theoryEngine->postsolve(); + d_needPostsolve = false; + } + d_userLevels.push_back(d_userContext->getLevel()); internalPush(); Trace("userpushpop") << "SmtEngine: pushed to level " @@ -1175,6 +1204,13 @@ void SmtEngine::pop() { if(d_userContext->getLevel() == 0) { throw ModalException("Cannot pop beyond the first user frame"); } + + // check to see if a postsolve() is pending + if(d_needPostsolve) { + d_theoryEngine->postsolve(); + d_needPostsolve = false; + } + AlwaysAssert(d_userLevels.size() > 0 && d_userLevels.back() < d_userContext->getLevel()); while (d_userLevels.back() < d_userContext->getLevel()) { internalPop(); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 90593569b..a8f2d5700 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -145,6 +145,12 @@ class CVC4_PUBLIC SmtEngine { */ bool d_queryMade; + /** + * Internal status flag to indicate whether we've sent a theory + * presolve() notification and need to match it with a postsolve(). + */ + bool d_needPostsolve; + /** 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. */ diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index 8e503f53e..bccd520f9 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -45,6 +45,7 @@ theory_has_propagate="false" theory_has_staticLearning="false" theory_has_notifyRestart="false" theory_has_presolve="false" +theory_has_postsolve="false" theory_stable_infinite="false" theory_finite="false" @@ -133,13 +134,14 @@ struct TheoryTraits<${theory_id}> { static const bool hasStaticLearning = ${theory_has_staticLearning}; static const bool hasNotifyRestart = ${theory_has_notifyRestart}; static const bool hasPresolve = ${theory_has_presolve}; + static const bool hasPostsolve = ${theory_has_postsolve}; };/* struct TheoryTraits<${theory_id}> */ " # warnings about theory content and properties dir="$(dirname "$kf")/../../" if [ -e "$dir/$theory_header" ]; then - for function in check propagate staticLearning notifyRestart presolve; do + for function in check propagate staticLearning notifyRestart presolve postsolve; do if eval "\$theory_has_$function"; then grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' || echo "$kf: warning: $theory_class has property \"$function\" in its kinds file but doesn't appear to declare the function" >&2 @@ -157,6 +159,7 @@ struct TheoryTraits<${theory_id}> { theory_has_staticLearning="false" theory_has_notifyRestart="false" theory_has_presolve="false" + theory_has_postsolve="false" theory_stable_infinite="false" theory_finite="false" @@ -200,6 +203,7 @@ function properties { propagate) theory_has_propagate="true";; staticLearning) theory_has_staticLearning="true";; presolve) theory_has_presolve="true";; + postsolve) theory_has_postsolve="true";; notifyRestart) theory_has_notifyRestart="true";; *) echo "$kf:$lineno: error: unknown theory property \"$property\"" >&2; exit 1;; esac diff --git a/src/theory/theory.h b/src/theory/theory.h index e6a2e2336..af891e3a3 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -535,6 +535,18 @@ public: virtual void presolve() { } /** + * A Theory is called with postsolve exactly one time per user + * check-sat. postsolve() is called after the query has completed + * (regardless of whether sat, unsat, or unknown), and after any + * model-querying related to the query has been performed. + * After this call, the theory will not get another check() or + * propagate() call until presolve() is called again. A Theory + * cannot raise conflicts, add lemmas, or propagate literals during + * postsolve(). + */ + virtual void postsolve() { } + + /** * Notification sent to the theory wheneven the search restarts. * Serves as a good time to do some clean-up work, and you can * assume you're at DL 0 for the purposes of Contexts. This function diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index f69fdddcb..e21e83671 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -381,7 +381,29 @@ bool TheoryEngine::presolve() { } // return whether we have a conflict return false; -} +}/* TheoryEngine::presolve() */ + +void TheoryEngine::postsolve() { + // NOTE that we don't look at d_theoryIsActive[] here (for symmetry + // with presolve()). + + try { + // Definition of the statement that is to be run by every theory +#ifdef CVC4_FOR_EACH_THEORY_STATEMENT +#undef CVC4_FOR_EACH_THEORY_STATEMENT +#endif +#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits<THEORY>::hasPostsolve) { \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->postsolve(); \ + Assert(! d_inConflict, "conflict raised during postsolve()"); \ + } + + // Postsolve for each theory using the statement above + CVC4_FOR_EACH_THEORY; + } catch(const theory::Interrupted&) { + Trace("theory") << "TheoryEngine::postsolve() => interrupted" << endl; + } +}/* TheoryEngine::postsolve() */ void TheoryEngine::notifyRestart() { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 387468b14..147fb868e 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -519,6 +519,11 @@ public: */ bool presolve(); + /** + * Calls postsolve() on all active theories. + */ + void postsolve(); + /** * Calls notifyRestart() on all active theories. */ |