Adding demand restart.

diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index ca22f29b6b4235d26ad09b9851bc4c8f7073ef1e..1bb6b5a9cb6bba1786bf2919986d486642544444 100644 (file)
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -216,6 +216,13 @@ public:
    */
   virtual void handleUserAttribute(const char* attr, Theory* t) {}
 
+
+  /** Demands that the search restart from sat search level 0.
+   * Using this leads to non-termination issues.
+   * It is appropraite for prototyping for theories.
+   */
+  virtual void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException) {}
+
 };/* class OutputChannel */
 
 }/* CVC4::theory namespace */

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index a8fe52498384b6f2f28297d20b3a41496ede07d8..f72b824cdaa38d32f1acebd908f472c539fad3d0 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -208,20 +208,22 @@ class TheoryEngine {
 
   public:
 
-    IntStat conflicts, propagations, lemmas, requirePhase, flipDecision;
+    IntStat conflicts, propagations, lemmas, requirePhase, flipDecision, restartDemands;
 
     Statistics(theory::TheoryId theory):
       conflicts(mkName("theory<", theory, ">::conflicts"), 0),
       propagations(mkName("theory<", theory, ">::propagations"), 0),
       lemmas(mkName("theory<", theory, ">::lemmas"), 0),
       requirePhase(mkName("theory<", theory, ">::requirePhase"), 0),
-      flipDecision(mkName("theory<", theory, ">::flipDecision"), 0)
+      flipDecision(mkName("theory<", theory, ">::flipDecision"), 0),
+      restartDemands(mkName("theory<", theory, ">::restartDemands"), 0)
     {
       StatisticsRegistry::registerStat(&conflicts);
       StatisticsRegistry::registerStat(&propagations);
       StatisticsRegistry::registerStat(&lemmas);
       StatisticsRegistry::registerStat(&requirePhase);
       StatisticsRegistry::registerStat(&flipDecision);
+      StatisticsRegistry::registerStat(&restartDemands);
     }
 
     ~Statistics() {
@@ -230,6 +232,7 @@ class TheoryEngine {
       StatisticsRegistry::unregisterStat(&lemmas);
       StatisticsRegistry::unregisterStat(&requirePhase);
       StatisticsRegistry::unregisterStat(&flipDecision);
+      StatisticsRegistry::unregisterStat(&restartDemands);
     }
   };/* class TheoryEngine::Statistics */
 
@@ -292,6 +295,16 @@ class TheoryEngine {
       return d_engine->lemma(lemma, false, removable);
     }
 
+    void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException) {
+      NodeManager* curr = NodeManager::currentNM();
+      Node restartVar =  curr->mkSkolem("restartVar",
+                                        curr->booleanType(),
+                                        "A boolean variable assrted to be true to force a restart");
+      Trace("theory::restart") << "EngineOutputChannel<" << d_theory << ">::restart(" << restartVar << ")" << std::endl;
+      ++ d_statistics.restartDemands;
+      lemma(restartVar, true);
+    }
+
     void requirePhase(TNode n, bool phase)
       throw(theory::Interrupted, AssertionException) {
       Debug("theory") << "EngineOutputChannel::requirePhase("