Remove unused postsolve infrastructurermPostsolve

The theory property `postsolve` was not used by any of the theories.
This commit removes the property and associated infrastructure.

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
@@ -760,18 +760,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
    * assume you're at DL 0 for the purposes of Contexts.  This function
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<THEORY>::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.
    */