added support for interrupting TheoryBV

diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index e13775ab2b6de662cb6d21ba203da36e7636530c..0dd208088b0b3df5b313fc592587e45e4424bafd 100644 (file)
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -46,6 +46,10 @@ private:
       toSatClause(clause, satClause);
       d_notify->notify(satClause);
     }
+
+    void safePoint() {
+      d_notify->safePoint(); 
+    }
   };
 
   BVMinisat::SimpSolver* d_minisat;

diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 293ddd6575e431c2301912c7b7c5dc873c2c36c3..978ac8d7b85d20c9ea9b392469088af94068473a 100644 (file)
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -27,9 +27,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "util/output.h"
 #include "util/utility.h"
-
+#include "util/exception.h"
 #include "theory/bv/options.h"
-
+#include "theory/interrupted.h"
 using namespace BVMinisat;
 
 namespace CVC4 {
@@ -794,13 +794,25 @@ lbool Solver::search(int nof_conflicts, UIP uip)
 
         }else{
             // NO CONFLICT
-            if (decisionLevel() > assumptions.size() && nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){
+            bool isWithinBudget;
+            try {
+              isWithinBudget = withinBudget(); 
+            }
+            catch (const CVC4::theory::Interrupted& e) {
+              // do some clean-up and rethrow 
+              cancelUntil(assumptions.size()); 
+              throw e; 
+            }
+            
+            if (decisionLevel() > assumptions.size() && nof_conflicts >= 0 && conflictC >= nof_conflicts ||
+                !isWithinBudget) {
                 // Reached bound on number of conflicts:
                 Debug("bvminisat::search") << OUTPUT_TAG << " restarting " << std::endl;
                 progress_estimate = progressEstimate();
                 cancelUntil(assumptions.size());
-                return l_Undef; }
-
+                return l_Undef;
+            }
+ 
             // Simplify the set of problem clauses:
             if (decisionLevel() == 0 && !simplify()) {
                 Debug("bvminisat::search") << OUTPUT_TAG << " base level conflict, we're unsat" << std::endl;

diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index b50ab632e6ddc6768672c4d24ca940cdef6a00c7..53d92ac39ac6890b6b8179392184c596c8426c25 100644 (file)
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -52,6 +52,7 @@ public:
    */
   virtual void notify(vec<Lit>& learnt) = 0;
 
+  virtual void safePoint() = 0;
 };
 
 //=================================================================================================
@@ -410,6 +411,8 @@ inline void     Solver::interrupt(){ asynch_interrupt = true; }
 inline void     Solver::clearInterrupt(){ asynch_interrupt = false; }
 inline void     Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }
 inline bool     Solver::withinBudget() const {
+    Assert (notify); 
+    notify->safePoint(); 
     return !asynch_interrupt &&
            (conflict_budget    < 0 || conflicts < (uint64_t)conflict_budget) &&
            (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index fe25caf29b9210807982661b290f37e8497295a1..973adc67f24fbe95d69119bc9a81979af79f1575 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -282,6 +282,7 @@ void PropEngine::interrupt() throw(ModalException) {
 
   d_interrupted = true;
   d_satSolver->interrupt();
+  d_theoryEngine->interrupt(); 
   Debug("prop") << "interrupt()" << endl;
 }
 

diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index a4fdd5b3aa7f9f5aaacba795e104725a543a44f5..7e3af69cfd67697acf25f0acbe4e96b4d1ad174f 100644 (file)
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -94,6 +94,8 @@ public:
      * Notify about a learnt clause.
      */
     virtual void notify(SatClause& clause) = 0;
+    virtual void safePoint() = 0;
+    
   };/* class BVSatSolverInterface::Notify */
 
   virtual void setNotify(Notify* notify) = 0;

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d3806199bf36c49e264be7437ef6115e24356862..878588d1572c8ea070d7b7c626b646bd63547e11 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2446,6 +2446,7 @@ void SmtEngine::interrupt() throw(ModalException) {
     return;
   }
   d_propEngine->interrupt();
+  d_theoryEngine->interrupt();
 }
 
 void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) {

diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 2c45fb603c7de1b284f3f6d59ac72b5e9fa64cf0..3beb7c2299033543b8df3cf1df6a45fe57682f30 100644 (file)
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -356,6 +356,10 @@ void Bitblaster::MinisatNotify::notify(prop::SatClause& clause) {
   }
 };
 
+void Bitblaster::MinisatNotify::safePoint() {
+  d_bv->d_out->safePoint(); 
+}
+
 EqualityStatus Bitblaster::getEqualityStatus(TNode a, TNode b) {
 
   // We don't want to bit-blast every possibly expensive term for the sake of equality checking

diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h
index 2ff12bbdf35b38c246f83643e6e55d61f405c02f..ada9802bd11468ba17d5496ff7846b0c3d5f2a96 100644 (file)
--- a/src/theory/bv/bitblaster.h
+++ b/src/theory/bv/bitblaster.h
@@ -78,6 +78,7 @@ class Bitblaster {
     {}
     bool notify(prop::SatLiteral lit);
     void notify(prop::SatClause& clause);
+    void safePoint();
   };
   
   typedef __gnu_cxx::hash_map <Node, Bits, TNodeHashFunction >              TermDefMap;

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 932f11f74e842869217156072daeffc2c3a935ad..0db71aba434fb73b1c3bac98cfd7f165d1e4f74d 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -71,6 +71,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_propagatedLiterals(context),
   d_propagatedLiteralsIndex(context, 0),
   d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
+  d_interrupted(false),
   d_inPreregister(false),
   d_factsAsserted(context, false),
   d_preRegistrationVisitor(this, context),
@@ -113,6 +114,10 @@ TheoryEngine::~TheoryEngine() {
   StatisticsRegistry::unregisterStat(&d_combineTheoriesTime);
 }
 
+void TheoryEngine::interrupt() throw(ModalException) {
+  d_interrupted = true;
+}
+
 void TheoryEngine::preRegister(TNode preprocessed) {
 
   if(Dump.isOn("missed-t-propagations")) {
@@ -282,6 +287,9 @@ void TheoryEngine::check(Theory::Effort effort) {
 
   d_propEngine->checkTime();
 
+  // Reset the interrupt flag
+  d_interrupted = false; 
+
 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 #endif
@@ -293,7 +301,6 @@ void TheoryEngine::check(Theory::Effort effort) {
        } \
     }
 
-
   // Do the checking
   try {
 
@@ -455,6 +462,9 @@ void TheoryEngine::combineTheories() {
 }
 
 void TheoryEngine::propagate(Theory::Effort effort) {
+  // Reset the interrupt flag
+  d_interrupted = false; 
+
   // Definition of the statement that is to be run by every theory
 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
@@ -464,6 +474,9 @@ void TheoryEngine::propagate(Theory::Effort effort) {
     theoryOf(THEORY)->propagate(effort); \
   }
 
+  // Reset the interrupt flag
+  d_interrupted = false; 
+
   // Propagate for each theory using the statement above
   CVC4_FOR_EACH_THEORY;
 
@@ -592,6 +605,8 @@ TheoryModel* TheoryEngine::getModel() {
 }
 
 bool TheoryEngine::presolve() {
+  // Reset the interrupt flag
+  d_interrupted = false; 
 
   try {
     // Definition of the statement that is to be run by every theory
@@ -599,7 +614,7 @@ bool TheoryEngine::presolve() {
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-    if (theory::TheoryTraits<THEORY>::hasPresolve) { \
+    if (theory::TheoryTraits<THEORY>::hasPresolve) {    \
       theoryOf(THEORY)->presolve(); \
       if(d_inConflict) { \
         return true; \
@@ -616,6 +631,8 @@ bool TheoryEngine::presolve() {
 }/* TheoryEngine::presolve() */
 
 void TheoryEngine::postsolve() {
+  // Reset the interrupt flag
+  d_interrupted = false; 
 
   try {
     // Definition of the statement that is to be run by every theory
@@ -637,6 +654,9 @@ void TheoryEngine::postsolve() {
 
 
 void TheoryEngine::notifyRestart() {
+  // Reset the interrupt flag
+  d_interrupted = false; 
+
   // Definition of the statement that is to be run by every theory
 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
@@ -651,6 +671,8 @@ void TheoryEngine::notifyRestart() {
 }
 
 void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
+  // Reset the interrupt flag
+  d_interrupted = false; 
 
   // Definition of the statement that is to be run by every theory
 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
@@ -683,6 +705,9 @@ void TheoryEngine::shutdown() {
 }
 
 theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) {
+  // Reset the interrupt flag
+  d_interrupted = false; 
+
   TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
   Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl;
 

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 5ec0d9776b18d3af33784d95d463461cc10871ba..8f534a62cc3c59e7514dc3dfa20a567fa7243c12 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -36,11 +36,13 @@
 #include "theory/shared_terms_database.h"
 #include "theory/term_registration_visitor.h"
 #include "theory/valuation.h"
+#include "theory/interrupted.h"
 #include "options/options.h"
 #include "smt/options.h"
 #include "util/statistics_registry.h"
 #include "util/hash.h"
 #include "util/cache.h"
+#include "util/cvc4_assert.h"
 #include "theory/ite_simplifier.h"
 #include "theory/unconstrained_simplifier.h"
 #include "theory/model.h"
@@ -230,6 +232,11 @@ class TheoryEngine {
     {
     }
 
+    void safePoint() throw(theory::Interrupted, AssertionException) {
+      if (d_engine->d_interrupted)
+        throw theory::Interrupted(); 
+   }
+
     void conflict(TNode conflictNode) throw(AssertionException) {
       Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl;
       ++ d_statistics.conflicts;
@@ -386,6 +393,9 @@ class TheoryEngine {
   Node d_true;
   Node d_false;
 
+  /** Whether we were just interrupted (or not) */
+  bool d_interrupted; 
+  
 public:
 
   /** Constructs a theory engine */
@@ -394,6 +404,8 @@ public:
   /** Destroys a theory engine */
   ~TheoryEngine();
 
+  void interrupt() throw(ModalException); 
+  
   /**
    * Adds a theory. Only one theory per TheoryId can be present, so if
    * there is another theory it will be deleted.