Merged updated version of the bitvector theory:

  * added simplification rewrites

2 files changed, 9 insertions, 3 deletions

diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index af342dbbc..7ff7b50db 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -23,6 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "mtl/Sort.h"
 #include "core/Solver.h"
 #include <iostream>
+#include "util/output.h"
 
 using namespace BVMinisat;
 
@@ -766,6 +767,8 @@ static double luby(double y, int x){
 // NOTE: assumptions passed in member-variable 'assumptions'.
 lbool Solver::solve_()
 {
+  Debug("bvminisat") <<"BVMinisat::Solving learned clauses " << learnts.size() <<"\n";
+  Debug("bvminisat") <<"BVMinisat::Solving assumptions " << assumptions.size() <<"\n"; 
     model.clear();
     conflict.clear();
     if (!ok) return l_False;
@@ -930,7 +933,7 @@ void Solver::garbageCollect()
     // Initialize the next region to a size corresponding to the estimated utilization degree. This
     // is not precise but should avoid some unnecessary reallocations for the new region:
     ClauseAllocator to(ca.size() - ca.wasted()); 
-
+    Debug("bvminisat") << " BVMinisat::Garbage collection \n"; 
     relocAll(to);
     if (verbosity >= 2)
         printf("|  Garbage collection:   %12d bytes => %12d bytes             |\n", 
diff --git a/src/prop/sat_module.cpp b/src/prop/sat_module.cpp
index db911f488..cda32a0e8 100644
--- a/src/prop/sat_module.cpp
+++ b/src/prop/sat_module.cpp
@@ -55,7 +55,10 @@ MinisatSatSolver::~MinisatSatSolver() {
 void MinisatSatSolver::addClause(SatClause& clause, bool removable) {
   Debug("sat::minisat") << "Add clause " << clause <<"\n"; 
   BVMinisat::vec<BVMinisat::Lit> minisat_clause;
-  toMinisatClause(clause, minisat_clause); 
+  toMinisatClause(clause, minisat_clause);
+  // for(unsigned i = 0; i < minisat_clause.size(); ++i) {
+  //   d_minisat->setFrozen(BVMinisat::var(minisat_clause[i]), true); 
+  // }
   d_minisat->addClause(minisat_clause);
 }
 
@@ -102,7 +105,7 @@ SatLiteralValue MinisatSatSolver::solve(const context::CDList<SatLiteral> & assu
   }
   Debug("sat::minisat") <<"\n";
   
- SatLiteralValue result = toSatLiteralValue(d_minisat->solve(assump)); 
+ SatLiteralValue result = toSatLiteralValue(d_minisat->solve(assump));
  return result;
 }