From a426d4b7795a173d6a50418a38a3b41bbfaf880d Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 20 Feb 2012 14:48:22 +0000 Subject: 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/theory/mktheorytraits | 6 +++++- src/theory/theory.h | 12 ++++++++++++ src/theory/theory_engine.cpp | 24 +++++++++++++++++++++++- src/theory/theory_engine.h | 5 +++++ 4 files changed, 45 insertions(+), 2 deletions(-) (limited to 'src/theory') 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. */ -- cgit v1.2.3