Partial merge from kind-backend branch, including Minisat and CNF work to

support incrementality.

Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.

Expected performance change negligible; slightly better on memory:
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!

1 files changed, 19 insertions, 1 deletions

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 4f83888fc..91b9a61e6 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -242,6 +242,12 @@ public:
   void pop();
 
   /**
+   * Return true if we are currently searching (either in this or
+   * another thread).
+   */
+  bool isRunning() const;
+
+  /**
    * Check the current time budget.
    */
   void checkTime();
@@ -258,11 +264,23 @@ public:
    */
   void spendResource() throw();
 
+  /**
+   * For debugging.  Return true if "expl" is a well-formed
+   * explanation for "node," meaning:
+   *
+   * 1. expl is either a SAT literal or an AND of SAT literals
+   *    currently assigned true;
+   * 2. node is assigned true;
+   * 3. node does not appear in expl; and
+   * 4. node was assigned after all of the literals in expl
+   */
+  bool properExplanation(TNode node, TNode expl) const;
+
 };/* class PropEngine */
 
 
 inline void SatTimer::check() {
-  if(expired()) {
+  if(d_propEngine.isRunning() && expired()) {
     Trace("limit") << "SatTimer::check(): interrupt!" << std::endl;
     d_propEngine.interrupt();
   }