diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2012-04-04 02:02:06 +0000 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2012-04-04 02:02:06 +0000 |
| commit | 52d6dc20c61007a5c066590aa1fd0b95ed3c2527 (patch) | |
| tree | 040efec36cde7775b5c19eb43fcdd60cbeb61f9e /src/prop/bvminisat/simp/SimpSolver.cc | |
| parent | 4fa8c7d1a0654e7780fd485c51463c06b34379b5 (diff) | |
* added propagation as lemmas to TheoryBV:
* modified BVMinisat to work incrementally
* added more bv regressions
Diffstat (limited to 'src/prop/bvminisat/simp/SimpSolver.cc')
| -rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.cc | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc index 4af756456..903ffa270 100644 --- a/src/prop/bvminisat/simp/SimpSolver.cc +++ b/src/prop/bvminisat/simp/SimpSolver.cc @@ -43,8 +43,9 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of // Constructor/Destructor: -SimpSolver::SimpSolver() : - grow (opt_grow) +SimpSolver::SimpSolver(CVC4::context::Context* c) : + Solver(c) + , grow (opt_grow) , clause_lim (opt_clause_lim) , subsumption_lim (opt_subsumption_lim) , simp_garbage_frac (opt_simp_garbage_frac) @@ -99,7 +100,13 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool freeze) { lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) { + vec<Lit> atom_propagations_backup; + atom_propagations.moveTo(atom_propagations_backup); + vec<int> atom_propagations_lim_backup; + atom_propagations_lim.moveTo(atom_propagations_lim_backup); + only_bcp = false; + cancelUntil(0); vec<Var> extra_frozen; lbool result = l_True; @@ -128,8 +135,8 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) else if (verbosity >= 1) printf("===============================================================================\n"); - if (result == l_True) - extendModel(); + atom_propagations_backup.moveTo(atom_propagations); + atom_propagations_lim_backup.moveTo(atom_propagations_lim); if (do_simp) // Unfreeze the assumptions that were frozen: |