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

4 files changed, 45 insertions, 2 deletions

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
@@ -535,6 +535,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
    * 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 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<THEORY>::hasPostsolve) { \
+      reinterpret_cast<theory::TheoryTraits<THEORY>::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.
    */