fixing the problems with the bvminisat. there was a case when things would get bitblasted, it would restart to add the clauses, and loose propagation information.

4 files changed, 18 insertions, 1 deletions

diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index a9c6d2676..60a98e6e5 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -173,6 +173,10 @@ void Bitblaster::explain(TNode atom, std::vector<TNode>& explanation) {
  * 
  */
  
+bool Bitblaster::propagate() {
+  return d_satSolver->propagate() == prop::SAT_VALUE_TRUE;
+}
+
 bool Bitblaster::assertToSat(TNode lit, bool propagate) {
   // strip the not
   TNode atom; 
diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h
index b27415e0b..16c50be22 100644
--- a/src/theory/bv/bitblaster.h
+++ b/src/theory/bv/bitblaster.h
@@ -129,6 +129,7 @@ public:
   Bitblaster(context::Context* c, bv::TheoryBV* bv); 
   ~Bitblaster();
   bool assertToSat(TNode node, bool propagate = true);
+  bool propagate();
   bool solve(bool quick_solve = false);
   void getConflict(std::vector<TNode>& conflict); 
   void explain(TNode atom, std::vector<TNode>& explanation);
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 334a704e9..a5a9b9a7e 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -93,6 +93,17 @@ bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory:
     }
   }
 
+  // We need to ensure we are fully propagated, so propagate now
+  if (d_useSatPropagation) {
+    bool ok = d_bitblaster->propagate();
+    if (!ok) {
+      std::vector<TNode> conflictAtoms;
+      d_bitblaster->getConflict(conflictAtoms);
+      d_bv->setConflict(mkConjunction(conflictAtoms));
+      return false;
+    }
+  }
+
   // solving
   if (e == Theory::EFFORT_FULL || Options::current()->bitvectorEagerFullcheck) {
     Assert(!d_bv->inConflict());
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 557acae95..d85d8915b 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1131,6 +1131,8 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable
 
 void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
 
+  Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << ")" << std::endl;
+
   // Mark that we are in conflict
   d_inConflict = true;
 
@@ -1152,7 +1154,6 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
     lemma(fullConflict, true, true);
   } else {
     // When only one theory, the conflict should need no processing
-    Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << ")" << std::endl;
     Assert(properConflict(conflict));
     lemma(conflict, true, true);
   }