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, 12 insertions, 0 deletions

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