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

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f8667fb71830d454e8fadb6455e4721b5ba42afd..f9539a1a46474810c31b408cac039bb76abc59f0 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -194,6 +194,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_logic(""),
   d_problemExtended(false),
   d_queryMade(false),
+  d_needPostsolve(false),
   d_timeBudgetCumulative(0),
   d_timeBudgetPerCall(0),
   d_resourceBudgetCumulative(0),
@@ -253,6 +254,13 @@ void SmtEngine::shutdown() {
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << QuitCommand() << endl;
   }
+
+  // check to see if a postsolve() is pending
+  if(d_needPostsolve) {
+    d_theoryEngine->postsolve();
+    d_needPostsolve = false;
+  }
+
   d_propEngine->shutdown();
   d_theoryEngine->shutdown();
 }
@@ -863,6 +871,12 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
     ensureBoolean(e);
   }
 
+  // check to see if a postsolve() is pending
+  if(d_needPostsolve) {
+    d_theoryEngine->postsolve();
+    d_needPostsolve = false;
+  }
+
   // Push the context
   internalPush();
 
@@ -877,6 +891,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
 
   // Run the check
   Result r = check().asSatisfiabilityResult();
+  d_needPostsolve = true;
 
   // Dump the query if requested
   if(Dump.isOn("benchmark")) {
@@ -915,6 +930,12 @@ Result SmtEngine::query(const BoolExpr& e) {
   // Ensure that the expression is type-checked at this point, and Boolean
   ensureBoolean(e);
 
+  // check to see if a postsolve() is pending
+  if(d_needPostsolve) {
+    d_theoryEngine->postsolve();
+    d_needPostsolve = false;
+  }
+
   // Push the context
   internalPush();
 
@@ -927,6 +948,7 @@ Result SmtEngine::query(const BoolExpr& e) {
 
   // Run the check
   Result r = check().asValidityResult();
+  d_needPostsolve = true;
 
   // Dump the query if requested
   if(Dump.isOn("benchmark")) {
@@ -1157,6 +1179,13 @@ void SmtEngine::push() {
   if(!Options::current()->incrementalSolving) {
     throw ModalException("Cannot push when not solving incrementally (use --incremental)");
   }
+
+  // check to see if a postsolve() is pending
+  if(d_needPostsolve) {
+    d_theoryEngine->postsolve();
+    d_needPostsolve = false;
+  }
+
   d_userLevels.push_back(d_userContext->getLevel());
   internalPush();
   Trace("userpushpop") << "SmtEngine: pushed to level "
@@ -1175,6 +1204,13 @@ void SmtEngine::pop() {
   if(d_userContext->getLevel() == 0) {
     throw ModalException("Cannot pop beyond the first user frame");
   }
+
+  // check to see if a postsolve() is pending
+  if(d_needPostsolve) {
+    d_theoryEngine->postsolve();
+    d_needPostsolve = false;
+  }
+
   AlwaysAssert(d_userLevels.size() > 0 && d_userLevels.back() < d_userContext->getLevel());
   while (d_userLevels.back() < d_userContext->getLevel()) {
     internalPop();

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 90593569b10cc1c1ff7a739bc26a10671970b6e6..a8f2d570013294e5319eab9f4741609baf5d3efc 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -145,6 +145,12 @@ class CVC4_PUBLIC SmtEngine {
    */
   bool d_queryMade;
 
+  /**
+   * Internal status flag to indicate whether we've sent a theory
+   * presolve() notification and need to match it with a postsolve().
+   */
+  bool d_needPostsolve;
+
   /** A user-imposed cumulative time budget, in milliseconds.  0 = no limit. */
   unsigned long d_timeBudgetCumulative;
   /** A user-imposed per-call time budget, in milliseconds.  0 = no limit. */

diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index 8e503f53e0f0940e2ce3326b6f5ae01356bd0c04..bccd520f9bbd64ab0b8e2d94fda6f147328cf6cb 100755 (executable)
--- 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 e6a2e2336f3b27b4c4c82e174a98f2ca9a96ac79..af891e3a35798af44025473f8459497b53d4e46e 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -534,6 +534,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

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f69fdddcbd917471bc3ab348cd09294dd8703e51..e21e8367108218320ce76a58c873844b783ee436 100644 (file)
--- 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 387468b144e5a10ee6bf08aefe110fde551469b5..147fb868e4e51895315009f785c3de274e611ff8 100644 (file)
--- 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.
    */