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

1 files changed, 23 insertions, 1 deletions

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() {