From: Andres Noetzli Date: Thu, 30 Jun 2022 23:18:06 +0000 (-0700) Subject: Remove `Theory::postsolve()` (#8924) X-Git-Tag: cvc5-1.0.1~21 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9480126b2c18d634b83b29e595e9bb54df72c1e0;p=cvc5.git Remove `Theory::postsolve()` (#8924) The feature was not used. This commit also uses the removal to simplify `SolverEngine` a bit. --- diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 4b0876abb..876f475ff 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -726,15 +726,12 @@ void SolverEngine::notifyPopPre() pe->pop(); } -void SolverEngine::notifyPostSolvePre() +void SolverEngine::notifyPostSolve() { PropEngine* pe = getPropEngine(); Assert(pe != nullptr); pe->resetTrail(); -} -void SolverEngine::notifyPostSolvePost() -{ TheoryEngine* te = getTheoryEngine(); Assert(te != nullptr); te->postsolve(); diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index 69d19a1d8..e77537d95 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -984,17 +984,11 @@ class CVC5_EXPORT SolverEngine */ void notifyPopPre(); /** - * Notify post solve pre, which is called once per check-sat query. It - * is triggered when the first d_state.doPendingPops() is issued after the - * check-sat. This method is called before the contexts pop in the method - * doPendingPops. + * Notify post solve, which is called once per check-sat query. It is + * triggered when the first d_state.doPendingPops() is issued after the + * check-sat. This calls the postsolve method of the underlying TheoryEngine. */ - void notifyPostSolvePre(); - /** - * Same as above, but after contexts are popped. This calls the postsolve - * method of the underlying TheoryEngine. - */ - void notifyPostSolvePost(); + void notifyPostSolve(); // --------------------------------------- end callbacks from the state /** diff --git a/src/smt/solver_engine_state.cpp b/src/smt/solver_engine_state.cpp index 1c71a1ef8..100cf099a 100644 --- a/src/smt/solver_engine_state.cpp +++ b/src/smt/solver_engine_state.cpp @@ -303,7 +303,8 @@ void SolverEngineState::doPendingPops() // check to see if a postsolve() is pending if (d_needPostsolve) { - d_slv.notifyPostSolvePre(); + d_slv.notifyPostSolve(); + d_needPostsolve = false; } while (d_pendingPops > 0) { @@ -314,11 +315,6 @@ void SolverEngineState::doPendingPops() --d_pendingPops; // no need for pop post (for now) } - if (d_needPostsolve) - { - d_slv.notifyPostSolvePost(); - d_needPostsolve = false; - } } } // namespace smt diff --git a/src/smt/solver_engine_state.h b/src/smt/solver_engine_state.h index e6de541fc..3885eebb0 100644 --- a/src/smt/solver_engine_state.h +++ b/src/smt/solver_engine_state.h @@ -230,7 +230,7 @@ class SolverEngineState : protected EnvObj /** * Internal status flag to indicate whether we have been issued a * notifyCheckSat call and have yet to process the "postsolve" methods of - * SolverEngine via SolverEngine::notifyPostSolvePre/notifyPostSolvePost. + * SolverEngine via SolverEngine::notifyPostSolve(). */ bool d_needPostsolve; diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index 5823b3500..c9c743baf 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -53,7 +53,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" @@ -168,14 +167,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 propagate ppStaticLearn notifyRestart presolve postsolve; do + for function in 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 @@ -193,7 +191,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" @@ -270,7 +267,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 5267e0f53..19aa94ecc 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -663,18 +663,6 @@ class Theory : protected EnvObj */ 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 e38839530..a99f07d06 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -686,28 +686,7 @@ void TheoryEngine::postsolve() { d_inSatMode = false; // Reset the interrupt flag d_interrupted = false; - CVC5_UNUSED bool wasInConflict = d_inConflict; - - try { - // Definition of the statement that is to be run by every theory -#ifdef CVC5_FOR_EACH_THEORY_STATEMENT -#undef CVC5_FOR_EACH_THEORY_STATEMENT -#endif -#define CVC5_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 - CVC5_FOR_EACH_THEORY; - } catch(const theory::Interrupted&) { - Trace("theory") << "TheoryEngine::postsolve() => interrupted" << endl; - } -}/* TheoryEngine::postsolve() */ - +} void TheoryEngine::notifyRestart() { // Reset the interrupt flag diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 3f25eefcd..13e378585 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -249,7 +249,7 @@ class TheoryEngine : protected EnvObj bool presolve(); /** - * Calls postsolve() on all theories. + * Resets the internal state. */ void postsolve();