diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-03-22 21:45:31 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-03-22 21:45:31 +0000 |
commit | c0324db3ac7e5984c632f46690f58c333b9a42b2 (patch) | |
tree | 7a9a83b7dc1f929d4eb3de06b59ed6ff7b7f43bd /src/prop/bvminisat | |
parent | 8c4495b18e40a406be35baceaf473878bcc375f1 (diff) |
Merged updated version of the bitvector theory:
* added simplification rewrites
Diffstat (limited to 'src/prop/bvminisat')
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 5 |
1 files changed, 4 insertions, 1 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", |