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.

9 files changed, 36 insertions, 4 deletions

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 4868db6f5..032788806 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -55,6 +55,10 @@ void BVMinisatSatSolver::addClause(SatClause& clause, bool removable) {
   d_minisat->addClause(minisat_clause);
 }
 
+SatValue BVMinisatSatSolver::propagate() {
+  return toSatLiteralValue(d_minisat->propagateAssumptions());
+}
+
 void BVMinisatSatSolver::addMarkerLiteral(SatLiteral lit) {
   d_minisat->addMarkerLiteral(BVMinisat::var(toMinisatLit(lit)));
 }
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 60cdd1c28..d337ff4e6 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -72,6 +72,8 @@ public:
 
   void addClause(SatClause& clause, bool removable);
 
+  SatValue propagate();
+
   SatVariable newVar(bool theoryAtom = false);
 
   SatVariable trueVar() { return d_minisat->trueVar(); }
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 2eadbdf22..94f3a6b74 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -522,6 +522,12 @@ void Solver::popAssumption() {
     cancelUntil(assumptions.size());
 }
 
+lbool Solver::propagateAssumptions() {
+  only_bcp = true;
+  ccmin_mode = 0;
+  return search(-1);
+}
+
 lbool Solver::assertAssumption(Lit p, bool propagate) {
   
   // assert(marker[var(p)] == 1);
@@ -953,7 +959,7 @@ void Solver::explain(Lit p, std::vector<Lit>& explanation) {
 
   Debug("bvminisat::explain") << OUTPUT_TAG << "starting explain of " << p << std::endl;
 
-      __gnu_cxx::hash_set<Var> visited;
+   __gnu_cxx::hash_set<Var> visited;
   visited.insert(var(p));
   
   while(queue.size() > 0) {
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index ea8e98c4c..b50ab632e 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -105,7 +105,8 @@ public:
     bool    solve        (Lit p, Lit q, Lit r);     // Search for a model that respects three assumptions.
     bool    okay         () const;                  // FALSE means solver is in a conflicting state
     lbool   assertAssumption(Lit p, bool propagate);  // Assert a new assumption, start BCP if propagate = true
-    void    popAssumption();                        // Pop an assumption
+    lbool   propagateAssumptions();                   // Do BCP over asserted assumptions
+    void    popAssumption();                          // Pop an assumption
 
     void    toDimacs     (FILE* f, const vec<Lit>& assumps);            // Write CNF to file in DIMACS-format.
     void    toDimacs     (const char *file, const vec<Lit>& assumps);
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 79e54cac2..102f8051b 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -95,7 +95,7 @@ public:
      * Notify about a learnt clause.
      */
     virtual void notify(SatClause& clause) = 0;
-};
+  };
 
   virtual void setNotify(Notify* notify) = 0; 
   
@@ -105,6 +105,8 @@ public:
 
   virtual void addMarkerLiteral(SatLiteral lit) = 0; 
 
+  virtual SatValue propagate() = 0;
+
   virtual void explain(SatLiteral lit, std::vector<SatLiteral>& explanation) = 0;
 
   virtual SatValue assertAssumption(SatLiteral lit, bool propagate = false) = 0; 
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);
   }