From: Tim King <taking@cs.nyu.edu>
Date: Mon, 1 Apr 2013 15:26:14 +0000 (-0400)
Subject: Adding demand restart.
X-Git-Tag: cvc5-1.0.0~7350
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3740d285d939b85af47804871abbf545ddda01af;p=cvc5.git

Adding demand restart.
---

diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index ca22f29b6..1bb6b5a9c 100644
--- 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 a8fe52498..f72b824cd 100644
--- 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("