From a426d4b7795a173d6a50418a38a3b41bbfaf880d Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 20 Feb 2012 14:48:22 +0000 Subject: [PATCH] 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 --- src/smt/smt_engine.cpp | 36 ++++++++++++++++++++++++++++++++++++ src/smt/smt_engine.h | 6 ++++++ src/theory/mktheorytraits | 6 +++++- src/theory/theory.h | 12 ++++++++++++ src/theory/theory_engine.cpp | 24 +++++++++++++++++++++++- 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 @@ -534,6 +534,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 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::hasPostsolve) { \ + reinterpret_cast::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. */ -- 2.30.2