diff options
Diffstat (limited to 'src/prop/minisat/simp/SimpSolver.cc')
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 96 |
1 files changed, 54 insertions, 42 deletions
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 23f97b5d5..0ec8981ca 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -21,8 +21,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/simp/SimpSolver.h" #include "options/prop_options.h" +#include "options/smt_options.h" #include "proof/clause_id.h" -#include "proof/proof.h" #include "prop/minisat/mtl/Sort.h" #include "prop/minisat/utils/System.h" @@ -47,25 +47,30 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of //================================================================================================= // Constructor/Destructor: - -SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, bool enableIncremental) : - Solver(proxy, context, enableIncremental) - , grow (opt_grow) - , clause_lim (opt_clause_lim) - , subsumption_lim (opt_subsumption_lim) - , simp_garbage_frac (opt_simp_garbage_frac) - , use_asymm (opt_use_asymm) - , use_rcheck (opt_use_rcheck) - , use_elim (options::minisatUseElim() && !enableIncremental) - , merges (0) - , asymm_lits (0) - , eliminated_vars (0) - , elimorder (1) - , use_simplification (!enableIncremental && !PROOF_ON()) // TODO: turn off simplifications if proofs are on initially - , occurs (ClauseDeleted(ca)) - , elim_heap (ElimLt(n_occ)) - , bwdsub_assigns (0) - , n_touched (0) +SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy, + CVC4::context::Context* context, + bool enableIncremental) + : Solver(proxy, context, enableIncremental), + grow(opt_grow), + clause_lim(opt_clause_lim), + subsumption_lim(opt_subsumption_lim), + simp_garbage_frac(opt_simp_garbage_frac), + use_asymm(opt_use_asymm), + use_rcheck(opt_use_rcheck), + use_elim(options::minisatUseElim() && !enableIncremental), + merges(0), + asymm_lits(0), + eliminated_vars(0), + elimorder(1), + use_simplification( + !enableIncremental + && !options::unsatCores()) // TODO: turn off simplifications if + // proofs are on initially + , + occurs(ClauseDeleted(ca)), + elim_heap(ElimLt(n_occ)), + bwdsub_assigns(0), + n_touched(0) { if(options::minisatUseElim() && options::minisatUseElim.wasSetByUser() && @@ -117,8 +122,8 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) { if (options::minisatDumpDimacs()) { - toDimacs(); - return l_Undef; + toDimacs(); + return l_Undef; } assert(decisionLevel() == 0); @@ -533,9 +538,10 @@ bool SimpSolver::eliminateVar(Var v) for (int i = 0; i < pos.size(); i++) for (int j = 0; j < neg.size(); j++) - if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) && - (++cnt > cls.size() + grow || (clause_lim != -1 && clause_size > clause_lim))) - return true; + if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) + && (++cnt > cls.size() + grow + || (clause_lim != -1 && clause_size > clause_lim))) + return true; // Delete and store old clauses: eliminated[v] = true; @@ -552,10 +558,9 @@ bool SimpSolver::eliminateVar(Var v) mkElimClause(elimclauses, ~mkLit(v)); } - for (int i = 0; i < cls.size(); i++) - removeClause(cls[i]); + for (int i = 0; i < cls.size(); i++) removeClause(cls[i]); - ClauseId id = ClauseIdUndef; + ClauseId id = ClauseIdUndef; // Produce clauses in cross product: vec<Lit>& resolvent = add_tmp; for (int i = 0; i < pos.size(); i++) @@ -569,7 +574,7 @@ bool SimpSolver::eliminateVar(Var v) // Free occurs list for this variable: occurs[v].clear(true); - + // Free watchers lists for this variable, if possible: if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true); if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true); @@ -589,7 +594,7 @@ bool SimpSolver::substitute(Var v, Lit x) eliminated[v] = true; setDecisionVar(v, false); const vec<CRef>& cls = occurs.lookup(v); - + vec<Lit>& subst_clause = add_tmp; for (int i = 0; i < cls.size(); i++){ Clause& c = ca[cls[i]]; @@ -641,9 +646,12 @@ bool SimpSolver::eliminate(bool turn_off_elim) gatherTouchedClauses(); // printf(" ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns); - if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) && - !backwardSubsumptionCheck(true)){ - ok = false; goto cleanup; } + if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) + && !backwardSubsumptionCheck(true)) + { + ok = false; + goto cleanup; + } // Empty elim_heap and return immediately on user-interrupt: if (asynch_interrupt){ @@ -656,7 +664,7 @@ bool SimpSolver::eliminate(bool turn_off_elim) // printf(" ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size()); for (int cnt = 0; !elim_heap.empty(); cnt++){ Var elim = elim_heap.removeMin(); - + if (asynch_interrupt) break; if (isEliminated(elim) || value(elim) != l_Undef) continue; @@ -706,8 +714,10 @@ bool SimpSolver::eliminate(bool turn_off_elim) } if (verbosity >= 1 && elimclauses.size() > 0) - printf("| Eliminated clauses: %10.2f Mb |\n", - double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024)); + printf( + "| Eliminated clauses: %10.2f Mb " + " |\n", + double(elimclauses.size() * sizeof(uint32_t)) / (1024 * 1024)); return ok; } @@ -744,11 +754,11 @@ void SimpSolver::relocAll(ClauseAllocator& to) // for (int i = 0; i < subsumption_queue.size(); i++) ca.reloc(subsumption_queue[i], to); - // TODO reloc now takes the proof form the core solver + // TODO reloc now takes the proof form the core solver // Temporary clause: // ca.reloc(bwdsub_tmpunit, to); - // TODO reloc now takes the proof form the core solver + // TODO reloc now takes the proof form the core solver } @@ -756,15 +766,17 @@ void SimpSolver::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()); + ClauseAllocator to(ca.size() - ca.wasted()); cleanUpClauses(); to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields. relocAll(to); Solver::relocAll(to); if (verbosity >= 2) - printf("| Garbage collection: %12d bytes => %12d bytes |\n", - ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size); + printf( + "| Garbage collection: %12d bytes => %12d bytes |\n", + ca.size() * ClauseAllocator::Unit_Size, + to.size() * ClauseAllocator::Unit_Size); to.moveTo(ca); - // TODO: proof.finalizeUpdateId(); + // TODO: proof.finalizeUpdateId(); } |