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 4b0876abb0e04b073ec0076703cc1e4903b0e097..876f475ff80bd65090e6a9a5a8f277bf4ccef375 100644 (file)
--- 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 69d19a1d8fc65d30cb35b8360a20884f0f4d3023..e77537d957436c7a76b254d30c80dd4d0f6b6d83 100644 (file)
--- 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 1c71a1ef85db14454b005c8a14eb1f489663b13d..100cf099ac7ae9d360c92b5e334221f4108a086a 100644 (file)
--- 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 e6de541fc316aa625b541fc460bf53d3d68f95e6..3885eebb0ce7c950580fcf7d40a8308e512c93f6 100644 (file)
--- 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 5823b35005f4e32a20626555cdb9754a507a0f59..c9c743baf435ae34b1fe2f6d6da3a5438e60b431 100755 (executable)
--- 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 5267e0f53f5b713eb0534108bf8c2ca11984cbf7..19aa94eccbefd188d33cfa0bd7f6565cd161ed94 100644 (file)
--- 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 e38839530d06cd32a7861b31dee6e1bd09158070..a99f07d06cb9831c828c9be7eab9ce40bcc590c3 100644 (file)
--- 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<THEORY>::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 3f25eefcd0778be7a7f2df57d6df5a01bbe38e67..13e3785850c62978a91d8cc38fe89b1fd73c8af0 100644 (file)
--- 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();