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, 15 insertions, 2 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);