From ed21776f3fdf079ebedaee6882cf6d86c9159dd1 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 3 Sep 2020 23:46:43 -0700 Subject: Remove unused postsolve infrastructure The theory property `postsolve` was not used by any of the theories. This commit removes the property and associated infrastructure. --- src/smt/smt_engine.cpp | 7 ------- src/smt/smt_engine.h | 5 ----- src/smt/smt_engine_state.cpp | 6 +----- src/smt/smt_engine_state.h | 4 ++-- src/theory/builtin/kinds | 1 - src/theory/mktheorytraits | 6 +----- src/theory/theory.h | 12 ------------ src/theory/theory_engine.cpp | 28 ---------------------------- src/theory/theory_engine.h | 5 ----- 9 files changed, 4 insertions(+), 70 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 81d4f594d..bec193f58 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -910,13 +910,6 @@ void SmtEngine::notifyPostSolvePre() pe->resetTrail(); } -void SmtEngine::notifyPostSolvePost() -{ - TheoryEngine* te = getTheoryEngine(); - Assert(te != nullptr); - te->postsolve(); -} - Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore) { Dump("benchmark") << CheckSatCommand(assumption); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 5aa2ba987..372d98970 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -989,11 +989,6 @@ class CVC4_PUBLIC SmtEngine * doPendingPops. */ void notifyPostSolvePre(); - /** - * Same as above, but after contexts are popped. This calls the postsolve - * method of the underlying TheoryEngine. - */ - void notifyPostSolvePost(); // --------------------------------------- end callbacks from the state /** diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp index 07f1d3321..1a8569b10 100644 --- a/src/smt/smt_engine_state.cpp +++ b/src/smt/smt_engine_state.cpp @@ -287,11 +287,7 @@ void SmtEngineState::doPendingPops() --d_pendingPops; // no need for pop post (for now) } - if (d_needPostsolve) - { - d_smt.notifyPostSolvePost(); - d_needPostsolve = false; - } + d_needPostsolve = false; } } // namespace smt diff --git a/src/smt/smt_engine_state.h b/src/smt/smt_engine_state.h index efb86ca88..e58cf235e 100644 --- a/src/smt/smt_engine_state.h +++ b/src/smt/smt_engine_state.h @@ -222,8 +222,8 @@ class SmtEngineState /** * Internal status flag to indicate whether we have been issued a - * notifyCheckSat call and have yet to process the "postsolve" methods of - * SmtEngine via SmtEngine::notifyPostSolvePre/notifyPostSolvePost. + * notifyCheckSat call and have yet to process the + * SmtEngine::notifyPostSolvePre method of SmtEngine. */ bool d_needPostsolve; diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index a11354b1a..f5cd89983 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -39,7 +39,6 @@ # ppStaticLearn the theory supports ppStaticLearn() # notifyRestart the theory supports notifyRestart() # presolve the theory supports presolve() -# postsolve the theory supports postsolve() # # In the case of the "theory-supports-function" properties, you # need to declare these for your theory or the functions will not diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index 1b1350abe..7ef30e818 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -50,7 +50,6 @@ theory_has_propagate="false" theory_has_ppStaticLearn="false" theory_has_notifyRestart="false" theory_has_presolve="false" -theory_has_postsolve="false" theory_stable_infinite="false" theory_finite="false" @@ -165,14 +164,13 @@ struct TheoryTraits<${theory_id}> { static const bool hasPpStaticLearn = ${theory_has_ppStaticLearn}; 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 ppStaticLearn notifyRestart presolve postsolve; do + for function in check propagate ppStaticLearn notifyRestart presolve; 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 @@ -190,7 +188,6 @@ struct TheoryTraits<${theory_id}> { theory_has_ppStaticLearn="false" theory_has_notifyRestart="false" theory_has_presolve="false" - theory_has_postsolve="false" theory_stable_infinite="false" theory_finite="false" @@ -267,7 +264,6 @@ function properties { propagate) theory_has_propagate="true";; ppStaticLearn) theory_has_ppStaticLearn="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 77652f874..91af5d8fa 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -759,18 +759,6 @@ class Theory { */ 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 ac06d266d..a834ca300 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -749,34 +749,6 @@ bool TheoryEngine::presolve() { return false; }/* TheoryEngine::presolve() */ -void TheoryEngine::postsolve() { - // no longer in SAT mode - d_inSatMode = false; - // Reset the interrupt flag - d_interrupted = false; - bool CVC4_UNUSED wasInConflict = d_inConflict; - - 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) \ - { \ - theoryOf(THEORY)->postsolve(); \ - Assert(!d_inConflict || wasInConflict) \ - << "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() { // Reset the interrupt flag d_interrupted = false; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 30b5d9fbb..2f1245aa8 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -525,11 +525,6 @@ class TheoryEngine { */ bool presolve(); - /** - * Calls postsolve() on all theories. - */ - void postsolve(); - /** * Calls notifyRestart() on all active theories. */ -- cgit v1.2.3