diff options
Diffstat (limited to 'src/prop/bvminisat')
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 533 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.h | 31 | ||||
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.cc | 222 | ||||
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.h | 85 |
4 files changed, 490 insertions, 381 deletions
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 25b6a3da2..84ab62fd8 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -86,70 +86,92 @@ CRef Solver::TCRef_Lazy = CRef_Undef - 1; // no real lazy ref here //================================================================================================= // Constructor/Destructor: - -Solver::Solver(CVC4::context::Context* c) : - - // Parameters (user settable): - // - d_notify(nullptr) - , c(c) - , verbosity (0) - , var_decay (opt_var_decay) - , clause_decay (opt_clause_decay) - , random_var_freq (opt_random_var_freq) - , random_seed (opt_random_seed) - , luby_restart (opt_luby_restart) - , ccmin_mode (opt_ccmin_mode) - , phase_saving (opt_phase_saving) - , rnd_pol (false) - , rnd_init_act (opt_rnd_init_act) - , garbage_frac (opt_garbage_frac) - , restart_first (opt_restart_first) - , restart_inc (opt_restart_inc) - - // Parameters (the rest): - // - , learntsize_factor((double)1/(double)3), learntsize_inc(1.5) - - // Parameters (experimental): - // - , learntsize_adjust_start_confl (100) - , learntsize_adjust_inc (1.5) - - // Statistics: (formerly in 'SolverStats') - // - , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0) - , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) - - , need_to_propagate(false) - , only_bcp(false) - , clause_added(false) - , ok (true) - , cla_inc (1) - , var_inc (1) - , watches (WatcherDeleted(ca)) - , qhead (0) - , simpDB_assigns (-1) - , simpDB_props (0) - , order_heap (VarOrderLt(activity)) - , progress_estimate (0) - , remove_satisfied (true) - - , ca () - - // even though these are temporaries and technically should be set - // before calling, lets initialize them. this will reduces chances of - // non-determinism in portfolio (parallel) solver if variables are - // being (incorrectly) used without initialization. - , seen(), analyze_stack(), analyze_toclear(), add_tmp() - , max_learnts(0.0), learntsize_adjust_confl(0.0), learntsize_adjust_cnt(0) - - // Resource constraints: - // - , conflict_budget (-1) - , propagation_budget (-1) - , asynch_interrupt (false) - , d_bvp (NULL) +Solver::Solver(CVC4::context::Context* context) + : + + // Parameters (user settable): + // + d_notify(nullptr), + c(context), + verbosity(0), + var_decay(opt_var_decay), + clause_decay(opt_clause_decay), + random_var_freq(opt_random_var_freq), + random_seed(opt_random_seed), + luby_restart(opt_luby_restart), + ccmin_mode(opt_ccmin_mode), + phase_saving(opt_phase_saving), + rnd_pol(false), + rnd_init_act(opt_rnd_init_act), + garbage_frac(opt_garbage_frac), + restart_first(opt_restart_first), + restart_inc(opt_restart_inc) + + // Parameters (the rest): + // + , + learntsize_factor((double)1 / (double)3), + learntsize_inc(1.5) + + // Parameters (experimental): + // + , + learntsize_adjust_start_confl(100), + learntsize_adjust_inc(1.5) + + // Statistics: (formerly in 'SolverStats') + // + , + solves(0), + starts(0), + decisions(0), + rnd_decisions(0), + propagations(0), + conflicts(0), + dec_vars(0), + clauses_literals(0), + learnts_literals(0), + max_literals(0), + tot_literals(0) + + , + need_to_propagate(false), + only_bcp(false), + clause_added(false), + ok(true), + cla_inc(1), + var_inc(1), + watches(WatcherDeleted(ca)), + qhead(0), + simpDB_assigns(-1), + simpDB_props(0), + order_heap(VarOrderLt(activity)), + progress_estimate(0), + remove_satisfied(true) + + , + ca() + + // even though these are temporaries and technically should be set + // before calling, lets initialize them. this will reduces chances of + // non-determinism in portfolio (parallel) solver if variables are + // being (incorrectly) used without initialization. + , + seen(), + analyze_stack(), + analyze_toclear(), + add_tmp(), + max_learnts(0.0), + learntsize_adjust_confl(0.0), + learntsize_adjust_cnt(0) + + // Resource constraints: + // + , + conflict_budget(-1), + propagation_budget(-1), + asynch_interrupt(false), + d_bvp(NULL) { // Create the constant variables varTrue = newVar(true, false); @@ -304,65 +326,73 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseId& id) } void Solver::attachClause(CRef cr) { - const Clause& c = ca[cr]; - assert(c.size() > 1); - watches[~c[0]].push(Watcher(cr, c[1])); - watches[~c[1]].push(Watcher(cr, c[0])); - if (c.learnt()) learnts_literals += c.size(); - else clauses_literals += c.size(); } - + const Clause& clause = ca[cr]; + assert(clause.size() > 1); + watches[~clause[0]].push(Watcher(cr, clause[1])); + watches[~clause[1]].push(Watcher(cr, clause[0])); + if (clause.learnt()) + learnts_literals += clause.size(); + else + clauses_literals += clause.size(); +} void Solver::detachClause(CRef cr, bool strict) { - const Clause& c = ca[cr]; - if(d_bvp){ d_bvp->getSatProof()->markDeleted(cr); } - - assert(c.size() > 1); - - if (strict){ - remove(watches[~c[0]], Watcher(cr, c[1])); - remove(watches[~c[1]], Watcher(cr, c[0])); + const Clause& clause = ca[cr]; + if (d_bvp) + { + d_bvp->getSatProof()->markDeleted(cr); } + + assert(clause.size() > 1); + + if (strict) + { + remove(watches[~clause[0]], Watcher(cr, clause[1])); + remove(watches[~clause[1]], Watcher(cr, clause[0])); }else{ // Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause) - watches.smudge(~c[0]); - watches.smudge(~c[1]); + watches.smudge(~clause[0]); + watches.smudge(~clause[1]); } - if (c.learnt()) learnts_literals -= c.size(); - else clauses_literals -= c.size(); } - + if (clause.learnt()) + learnts_literals -= clause.size(); + else + clauses_literals -= clause.size(); +} void Solver::removeClause(CRef cr) { - Clause& c = ca[cr]; - detachClause(cr); - // Don't leave pointers to free'd memory! - if (locked(c)) vardata[var(c[0])].reason = CRef_Undef; - c.mark(1); - ca.free(cr); + Clause& clause = ca[cr]; + detachClause(cr); + // Don't leave pointers to free'd memory! + if (locked(clause)) vardata[var(clause[0])].reason = CRef_Undef; + clause.mark(1); + ca.free(cr); } - -bool Solver::satisfied(const Clause& c) const { - for (int i = 0; i < c.size(); i++) - if (value(c[i]) == l_True) - return true; - return false; } - +bool Solver::satisfied(const Clause& clause) const +{ + for (int i = 0; i < clause.size(); i++) + if (value(clause[i]) == l_True) return true; + return false; +} // Revert to the state at given level (keeping all assignment at 'level' but not beyond). // void Solver::cancelUntil(int level) { if (decisionLevel() > level){ Debug("bvminisat::explain") << OUTPUT_TAG << " backtracking to " << level << std::endl; - for (int c = trail.size()-1; c >= trail_lim[level]; c--){ - Var x = var(trail[c]); - assigns [x] = l_Undef; - if (marker[x] == 2) marker[x] = 1; - if (phase_saving > 1 - || ((phase_saving == 1) && c > trail_lim.last())) - { - polarity[x] = sign(trail[c]); - } - insertVarOrder(x); } + for (int clause = trail.size() - 1; clause >= trail_lim[level]; clause--) + { + Var x = var(trail[clause]); + assigns[x] = l_Undef; + if (marker[x] == 2) marker[x] = 1; + if (phase_saving > 1 + || ((phase_saving == 1) && clause > trail_lim.last())) + { + polarity[x] = sign(trail[clause]); + } + insertVarOrder(x); + } qhead = trail_lim[level]; trail.shrink(trail.size() - trail_lim[level]); trail_lim.shrink(trail_lim.size() - level); @@ -429,28 +459,33 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip do{ assert(confl != CRef_Undef); // (otherwise should be UIP) - Clause& c = ca[confl]; - - if (c.learnt()) - claBumpActivity(c); - - for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){ - Lit q = c[j]; + Clause& clause = ca[confl]; + + if (clause.learnt()) claBumpActivity(clause); + + for (int j = (p == lit_Undef) ? 0 : 1; j < clause.size(); j++) + { + Lit q = clause[j]; + + if (!seen[var(q)] && level(var(q)) > 0) + { + varBumpActivity(var(q)); + seen[var(q)] = 1; + if (level(var(q)) >= decisionLevel()) + pathC++; + else + out_learnt.push(q); + } - if (!seen[var(q)] && level(var(q)) > 0) { - varBumpActivity(var(q)); - seen[var(q)] = 1; - if (level(var(q)) >= decisionLevel()) - pathC++; - else - out_learnt.push(q); - } - - if (level(var(q)) == 0) { - if(d_bvp){ d_bvp->getSatProof()->resolveOutUnit(q); } + if (level(var(q)) == 0) + { + if (d_bvp) + { + d_bvp->getSatProof()->resolveOutUnit(q); } + } } - + // Select next clause to look at: while (!seen[var(trail[index--])]); p = trail[index+1]; @@ -478,51 +513,68 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip // Simplify conflict clause: // - int i, j; + int i1, j; out_learnt.copyTo(analyze_toclear); if (ccmin_mode == 2){ uint32_t abstract_level = 0; - for (i = 1; i < out_learnt.size(); i++) - abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict) - - for (i = j = 1; i < out_learnt.size(); i++) { - if (reason(var(out_learnt[i])) == CRef_Undef) { - out_learnt[j++] = out_learnt[i]; - } else { - // Check if the literal is redundant - if (!litRedundant(out_learnt[i], abstract_level)) { - // Literal is not redundant - out_learnt[j++] = out_learnt[i]; - } else { - if(d_bvp){ d_bvp->getSatProof()->storeLitRedundant(out_learnt[i]); } + for (i1 = 1; i1 < out_learnt.size(); i1++) + abstract_level |= abstractLevel( + var(out_learnt[i1])); // (maintain an abstraction of levels + // involved in conflict) + + for (i1 = j = 1; i1 < out_learnt.size(); i1++) + { + if (reason(var(out_learnt[i1])) == CRef_Undef) + { + out_learnt[j++] = out_learnt[i1]; + } + else + { + // Check if the literal is redundant + if (!litRedundant(out_learnt[i1], abstract_level)) + { + // Literal is not redundant + out_learnt[j++] = out_learnt[i1]; + } + else + { + if (d_bvp) + { + d_bvp->getSatProof()->storeLitRedundant(out_learnt[i1]); } } + } } - }else if (ccmin_mode == 1){ Unreachable(); - for (i = j = 1; i < out_learnt.size(); i++){ - Var x = var(out_learnt[i]); - - if (reason(x) == CRef_Undef) - out_learnt[j++] = out_learnt[i]; - else{ - Clause& c = ca[reason(var(out_learnt[i]))]; - for (int k = 1; k < c.size(); k++) - if (!seen[var(c[k])] && level(var(c[k])) > 0){ - out_learnt[j++] = out_learnt[i]; - break; } - } + for (i1 = j = 1; i1 < out_learnt.size(); i1++) + { + Var x = var(out_learnt[i1]); + + if (reason(x) == CRef_Undef) + out_learnt[j++] = out_learnt[i1]; + else + { + Clause& clause = ca[reason(var(out_learnt[i1]))]; + for (int k = 1; k < clause.size(); k++) + if (!seen[var(clause[k])] && level(var(clause[k])) > 0) + { + out_learnt[j++] = out_learnt[i1]; + break; + } + } } }else - i = j = out_learnt.size(); + i1 = j = out_learnt.size(); max_literals += out_learnt.size(); - out_learnt.shrink(i - j); + out_learnt.shrink(i1 - j); tot_literals += out_learnt.size(); - for (int i = 0; i < out_learnt.size(); ++ i) { - if (marker[var(out_learnt[i])] == 0) { + for (int i2 = 0; i2 < out_learnt.size(); ++i2) + { + if (marker[var(out_learnt[i2])] == 0) + { break; } } @@ -535,17 +587,18 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip else{ int max_i = 1; // Find the first literal assigned at the next-highest level: - for (int i = 2; i < out_learnt.size(); i++) - if (level(var(out_learnt[i])) > level(var(out_learnt[max_i]))) - max_i = i; - // Swap-in this literal at index 1: - Lit p = out_learnt[max_i]; + for (int i3 = 2; i3 < out_learnt.size(); i3++) + if (level(var(out_learnt[i3])) > level(var(out_learnt[max_i]))) + max_i = i3; + // Swap-in this literal at i1 1: + Lit p2 = out_learnt[max_i]; out_learnt[max_i] = out_learnt[1]; - out_learnt[1] = p; - out_btlevel = level(var(p)); + out_learnt[1] = p2; + out_btlevel = level(var(p2)); } - for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared) + for (int j2 = 0; j2 < analyze_toclear.size(); j2++) + seen[var(analyze_toclear[j2])] = 0; // ('seen[]' is now cleared) } @@ -558,24 +611,29 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels) while (analyze_stack.size() > 0){ CRef c_reason = reason(var(analyze_stack.last())); assert(c_reason != CRef_Undef); - Clause& c = ca[c_reason]; - int c_size = c.size(); + Clause& clause = ca[c_reason]; + int c_size = clause.size(); analyze_stack.pop(); for (int i = 1; i < c_size; i++){ - Lit p = c[i]; - if (!seen[var(p)] && level(var(p)) > 0){ - if (reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0){ - seen[var(p)] = 1; - analyze_stack.push(p); - analyze_toclear.push(p); - }else{ - for (int j = top; j < analyze_toclear.size(); j++) - seen[var(analyze_toclear[j])] = 0; - analyze_toclear.shrink(analyze_toclear.size() - top); - return false; - } + Lit p2 = clause[i]; + if (!seen[var(p2)] && level(var(p2)) > 0) + { + if (reason(var(p2)) != CRef_Undef + && (abstractLevel(var(p2)) & abstract_levels) != 0) + { + seen[var(p2)] = 1; + analyze_stack.push(p2); + analyze_toclear.push(p2); + } + else + { + for (int j = top; j < analyze_toclear.size(); j++) + seen[var(analyze_toclear[j])] = 0; + analyze_toclear.shrink(analyze_toclear.size() - top); + return false; } + } } } @@ -619,16 +677,18 @@ void Solver::analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict) { if(d_bvp){d_bvp->getSatProof()->resolveOutUnit(~p);} } } else { - Clause& c = ca[reason(x)]; + Clause& clause = ca[reason(x)]; if(d_bvp){d_bvp->getSatProof()->addResolutionStep(trail[i],reason(x), sign(trail[i]));} - for (int j = 1; j < c.size(); j++) { - if (level(var(c[j])) > 0) - seen[var(c[j])] = 1; + for (int j = 1; j < clause.size(); j++) + { + if (level(var(clause[j])) > 0) seen[var(clause[j])] = 1; if(d_bvp){ - if (level(var(c[j])) == 0) { - d_bvp->getSatProof()->resolveOutUnit(c[j]); - seen[var(c[j])] = 0; // we don't need to resolve it out again + if (level(var(clause[j])) == 0) + { + d_bvp->getSatProof()->resolveOutUnit(clause[j]); + seen[var(clause[j])] = + 0; // we don't need to resolve it out again } } } @@ -683,7 +743,7 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) out_conflict.push(~trail[i]); } } else { - Clause& c = ca[reason(x)]; + Clause& clause = ca[reason(x)]; if(d_bvp){ if (d_bvp->isAssumptionConflict() && trail[i] == p) { @@ -692,13 +752,16 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) d_bvp->getSatProof()->addResolutionStep(trail[i], reason(x), sign(trail[i])); } } - for (int j = 1; j < c.size(); j++) { - if (level(var(c[j])) > 0) { - seen[var(c[j])] = 1; + for (int j = 1; j < clause.size(); j++) + { + if (level(var(clause[j])) > 0) + { + seen[var(clause[j])] = 1; } if(d_bvp){ - if (level(var(c[j])) == 0) { - d_bvp->getSatProof()->resolveOutUnit(c[j]); + if (level(var(clause[j])) == 0) + { + d_bvp->getSatProof()->resolveOutUnit(clause[j]); } } } @@ -813,25 +876,28 @@ CRef Solver::propagate() // Make sure the false literal is data[1]: CRef cr = i->cref; - Clause& c = ca[cr]; + Clause& clause = ca[cr]; Lit false_lit = ~p; - if (c[0] == false_lit) - c[0] = c[1], c[1] = false_lit; - assert(c[1] == false_lit); + if (clause[0] == false_lit) + clause[0] = clause[1], clause[1] = false_lit; + assert(clause[1] == false_lit); i++; // If 0th watch is true, then clause is already satisfied. - Lit first = c[0]; + Lit first = clause[0]; Watcher w = Watcher(cr, first); if (first != blocker && value(first) == l_True){ *j++ = w; continue; } // Look for new watch: - for (int k = 2; k < c.size(); k++) - if (value(c[k]) != l_False){ - c[1] = c[k]; c[k] = false_lit; - watches[~c[1]].push(w); - goto NextClause; } + for (int k = 2; k < clause.size(); k++) + if (value(clause[k]) != l_False) + { + clause[1] = clause[k]; + clause[k] = false_lit; + watches[~clause[1]].push(w); + goto NextClause; + } // Did not find watch -- clause is unit under assignment: *j++ = w; @@ -878,11 +944,12 @@ void Solver::reduceDB() // Don't delete binary or locked clauses. From the rest, delete clauses from the first half // and clauses with activity smaller than 'extra_lim': for (i = j = 0; i < learnts.size(); i++){ - Clause& c = ca[learnts[i]]; - if (c.size() > 2 && !locked(c) && (i < learnts.size() / 2 || c.activity() < extra_lim)) - removeClause(learnts[i]); - else - learnts[j++] = learnts[i]; + Clause& clause = ca[learnts[i]]; + if (clause.size() > 2 && !locked(clause) + && (i < learnts.size() / 2 || clause.activity() < extra_lim)) + removeClause(learnts[i]); + else + learnts[j++] = learnts[i]; } learnts.shrink(i - j); checkGarbage(); @@ -893,14 +960,19 @@ void Solver::removeSatisfied(vec<CRef>& cs) { int i, j; for (i = j = 0; i < cs.size(); i++){ - Clause& c = ca[cs[i]]; - if (satisfied(c)) { - if (locked(c)) { - // store a resolution of the literal c propagated - if(d_bvp){ d_bvp->getSatProof()->storeUnitResolution(c[0]); } + Clause& clause = ca[cs[i]]; + if (satisfied(clause)) + { + if (locked(clause)) + { + // store a resolution of the literal clause propagated + if (d_bvp) + { + d_bvp->getSatProof()->storeUnitResolution(clause[0]); } - removeClause(cs[i]); } + removeClause(cs[i]); + } else cs[j++] = cs[i]; } @@ -1290,7 +1362,7 @@ void Solver::explain(Lit p, std::vector<Lit>& explanation) { } } else { - Clause& c = ca[reason(x)]; + Clause& clause = ca[reason(x)]; if(d_bvp){ if (p == trail[i]) { d_bvp->startBVConflict(reason(var(p))); @@ -1298,9 +1370,11 @@ void Solver::explain(Lit p, std::vector<Lit>& explanation) { d_bvp->getSatProof()->addResolutionStep(trail[i], reason(x), sign(trail[i])); } } - for (int j = 1; j < c.size(); j++) { - if (level(var(c[j])) > 0 || options::proof()) { - seen[var(c[j])] = 1; + for (int j = 1; j < clause.size(); j++) + { + if (level(var(clause[j])) > 0 || options::proof()) + { + seen[var(clause[j])] = 1; } } } @@ -1341,15 +1415,17 @@ static Var mapVar(Var x, vec<Var>& map, Var& max) return map[x]; } - -void Solver::toDimacs(FILE* f, Clause& c, vec<Var>& map, Var& max) +void Solver::toDimacs(FILE* f, Clause& clause, vec<Var>& map, Var& max) { - if (satisfied(c)) return; - - for (int i = 0; i < c.size(); i++) - if (value(c[i]) != l_False) - fprintf(f, "%s%d ", sign(c[i]) ? "-" : "", mapVar(var(c[i]), map, max)+1); - fprintf(f, "0\n"); + if (satisfied(clause)) return; + + for (int i = 0; i < clause.size(); i++) + if (value(clause[i]) != l_False) + fprintf(f, + "%s%d ", + sign(clause[i]) ? "-" : "", + mapVar(var(clause[i]), map, max) + 1); + fprintf(f, "0\n"); } @@ -1381,10 +1457,9 @@ void Solver::toDimacs(FILE* f, const vec<Lit>& assumps) for (int i = 0; i < clauses.size(); i++) if (!satisfied(ca[clauses[i]])){ - Clause& c = ca[clauses[i]]; - for (int j = 0; j < c.size(); j++) - if (value(c[j]) != l_False) - mapVar(var(c[j]), map, max); + Clause& clause = ca[clauses[i]]; + for (int j = 0; j < clause.size(); j++) + if (value(clause[j]) != l_False) mapVar(var(clause[j]), map, max); } // Assumptions are added as unit clauses: diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index 2197d030f..7fad72d6d 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -365,11 +365,11 @@ public: // Less than for literals in an added clause when proofs are on. struct assign_lt { - Solver& solver; - assign_lt(Solver& solver) : solver(solver) {} + Solver& d_solver; + assign_lt(Solver& solver) : d_solver(solver) {} bool operator () (Lit x, Lit y) { - lbool x_value = solver.value(x); - lbool y_value = solver.value(y); + lbool x_value = d_solver.value(x); + lbool y_value = d_solver.value(y); // Two unassigned literals are sorted arbitrarily if (x_value == l_Undef && y_value == l_Undef) { return x < y; @@ -379,7 +379,7 @@ public: if (y_value == l_Undef) return false; // Literals of the same value are sorted by decreasing levels if (x_value == y_value) { - return solver.level(var(x)) > solver.level(var(y)); + return d_solver.level(var(x)) > d_solver.level(var(y)); } else { // True literals go up front if (x_value == l_True) { @@ -417,12 +417,15 @@ inline void Solver::varBumpActivity(Var v, double inc) { order_heap.decrease(v); } inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); } -inline void Solver::claBumpActivity (Clause& c) { - if ( (c.activity() += cla_inc) > 1e20 ) { - // Rescale: - for (int i = 0; i < learnts.size(); i++) - ca[learnts[i]].activity() *= 1e-20; - cla_inc *= 1e-20; } } +inline void Solver::claBumpActivity(Clause& clause) +{ + if ((clause.activity() += cla_inc) > 1e20) + { + // Rescale: + for (int i = 0; i < learnts.size(); i++) ca[learnts[i]].activity() *= 1e-20; + cla_inc *= 1e-20; + } +} inline void Solver::checkGarbage(void){ return checkGarbage(garbage_frac); } inline void Solver::checkGarbage(double gf){ @@ -436,7 +439,11 @@ inline bool Solver::addEmptyClause () { add_tmp.clear( inline bool Solver::addClause (Lit p, ClauseId& id) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, id); } inline bool Solver::addClause (Lit p, Lit q, ClauseId& id) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, id); } inline bool Solver::addClause (Lit p, Lit q, Lit r, ClauseId& id) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, id); } -inline bool Solver::locked (const Clause& c) const { return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; } +inline bool Solver::locked(const Clause& clause) const +{ + return value(clause[0]) == l_True && reason(var(clause[0])) != CRef_Undef + && ca.lea(reason(var(clause[0]))) == &clause; +} inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } inline int Solver::decisionLevel () const { return trail_lim.size(); } diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc index 9e50433ef..b003342c6 100644 --- a/src/prop/bvminisat/simp/SimpSolver.cc +++ b/src/prop/bvminisat/simp/SimpSolver.cc @@ -48,8 +48,8 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of //================================================================================================= // Constructor/Destructor: -SimpSolver::SimpSolver(CVC4::context::Context* c) - : Solver(c), +SimpSolver::SimpSolver(CVC4::context::Context* context) + : Solver(context), grow(opt_grow), clause_lim(opt_clause_lim), subsumption_lim(opt_subsumption_lim), @@ -181,7 +181,7 @@ bool SimpSolver::addClause_(vec<Lit>& ps, ClauseId& id) if (use_simplification && clauses.size() == nclauses + 1){ CRef cr = clauses.last(); - const Clause& c = ca[cr]; + const Clause& clause = ca[cr]; // NOTE: the clause is added to the queue immediately and then // again during 'gatherTouchedClauses()'. If nothing happens @@ -190,13 +190,14 @@ bool SimpSolver::addClause_(vec<Lit>& ps, ClauseId& id) // consequence of how backward subsumption is used to mimic // forward subsumption. subsumption_queue.insert(cr); - for (int i = 0; i < c.size(); i++){ - occurs[var(c[i])].push(cr); - n_occ[toInt(c[i])]++; - touched[var(c[i])] = 1; - n_touched++; - if (elim_heap.inHeap(var(c[i]))) - elim_heap.increase(var(c[i])); + for (int i = 0; i < clause.size(); i++) + { + occurs[var(clause[i])].push(cr); + n_occ[toInt(clause[i])]++; + touched[var(clause[i])] = 1; + n_touched++; + if (elim_heap.inHeap(var(clause[i]))) + elim_heap.increase(var(clause[i])); } } @@ -206,14 +207,15 @@ bool SimpSolver::addClause_(vec<Lit>& ps, ClauseId& id) void SimpSolver::removeClause(CRef cr) { - const Clause& c = ca[cr]; + const Clause& clause = ca[cr]; - if (use_simplification) - for (int i = 0; i < c.size(); i++){ - n_occ[toInt(c[i])]--; - updateElimHeap(var(c[i])); - occurs.smudge(var(c[i])); - } + if (use_simplification) + for (int i = 0; i < clause.size(); i++) + { + n_occ[toInt(clause[i])]--; + updateElimHeap(var(clause[i])); + occurs.smudge(var(clause[i])); + } Solver::removeClause(cr); } @@ -221,27 +223,31 @@ void SimpSolver::removeClause(CRef cr) bool SimpSolver::strengthenClause(CRef cr, Lit l) { - Clause& c = ca[cr]; - assert(decisionLevel() == 0); - assert(use_simplification); - - // FIX: this is too inefficient but would be nice to have (properly implemented) - // if (!find(subsumption_queue, &c)) - subsumption_queue.insert(cr); - - if (c.size() == 2){ - removeClause(cr); - c.strengthen(l); - }else{ - detachClause(cr, true); - c.strengthen(l); - attachClause(cr); - remove(occurs[var(l)], cr); - n_occ[toInt(l)]--; - updateElimHeap(var(l)); - } - - return c.size() == 1 ? enqueue(c[0]) && propagate() == CRef_Undef : true; + Clause& clause = ca[cr]; + assert(decisionLevel() == 0); + assert(use_simplification); + + // FIX: this is too inefficient but would be nice to have (properly + // implemented) if (!find(subsumption_queue, &clause)) + subsumption_queue.insert(cr); + + if (clause.size() == 2) + { + removeClause(cr); + clause.strengthen(l); + } + else + { + detachClause(cr, true); + clause.strengthen(l); + attachClause(cr); + remove(occurs[var(l)], cr); + n_occ[toInt(l)]--; + updateElimHeap(var(l)); + } + + return clause.size() == 1 ? enqueue(clause[0]) && propagate() == CRef_Undef + : true; } @@ -345,20 +351,22 @@ void SimpSolver::gatherTouchedClauses() n_touched = 0; } - -bool SimpSolver::implied(const vec<Lit>& c) +bool SimpSolver::implied(const vec<Lit>& clause) { assert(decisionLevel() == 0); trail_lim.push(trail.size()); - for (int i = 0; i < c.size(); i++) - if (value(c[i]) == l_True){ - cancelUntil(0); - return false; - }else if (value(c[i]) != l_False){ - assert(value(c[i]) == l_Undef); - uncheckedEnqueue(~c[i]); - } + for (int i = 0; i < clause.size(); i++) + if (value(clause[i]) == l_True) + { + cancelUntil(0); + return false; + } + else if (value(clause[i]) != l_False) + { + assert(value(clause[i]) == l_Undef); + uncheckedEnqueue(~clause[i]); + } bool result = propagate() != CRef_Undef; cancelUntil(0); @@ -390,44 +398,49 @@ bool SimpSolver::backwardSubsumptionCheck(bool verbose) subsumption_queue.insert(bwdsub_tmpunit); } CRef cr = subsumption_queue.peek(); subsumption_queue.pop(); - Clause& c = ca[cr]; + Clause& clause = ca[cr]; - if (c.mark()) continue; + if (clause.mark()) continue; if (verbose && verbosity >= 2 && cnt++ % 1000 == 0) printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals); - assert(c.size() > 1 || value(c[0]) == l_True); // Unit-clauses should have been propagated before this point. + assert(clause.size() > 1 + || value(clause[0]) == l_True); // Unit-clauses should have been + // propagated before this point. // Find best variable to scan: - Var best = var(c[0]); - for (int i = 1; i < c.size(); i++) - if (occurs[var(c[i])].size() < occurs[best].size()) - best = var(c[i]); + Var best = var(clause[0]); + for (int i = 1; i < clause.size(); i++) + if (occurs[var(clause[i])].size() < occurs[best].size()) + best = var(clause[i]); // Search all candidates: vec<CRef>& _cs = occurs.lookup(best); CRef* cs = (CRef*)_cs; for (int j = 0; j < _cs.size(); j++) - if (c.mark()) - break; - else if (!ca[cs[j]].mark() && cs[j] != cr && (subsumption_lim == -1 || ca[cs[j]].size() < subsumption_lim)){ - Lit l = c.subsumes(ca[cs[j]]); - - if (l == lit_Undef) - subsumed++, removeClause(cs[j]); - else if (l != lit_Error){ - deleted_literals++; - - if (!strengthenClause(cs[j], ~l)) - return false; - - // Did current candidate get deleted from cs? Then check candidate at index j again: - if (var(l) == best) - j--; - } + if (clause.mark()) + break; + else if (!ca[cs[j]].mark() && cs[j] != cr + && (subsumption_lim == -1 + || ca[cs[j]].size() < subsumption_lim)) + { + Lit l = clause.subsumes(ca[cs[j]]); + + if (l == lit_Undef) + subsumed++, removeClause(cs[j]); + else if (l != lit_Error) + { + deleted_literals++; + + if (!strengthenClause(cs[j], ~l)) return false; + + // Did current candidate get deleted from cs? Then check candidate + // at index j again: + if (var(l) == best) j--; } + } } return true; @@ -436,28 +449,29 @@ bool SimpSolver::backwardSubsumptionCheck(bool verbose) bool SimpSolver::asymm(Var v, CRef cr) { - Clause& c = ca[cr]; - assert(decisionLevel() == 0); + Clause& clause = ca[cr]; + assert(decisionLevel() == 0); - if (c.mark() || satisfied(c)) return true; + if (clause.mark() || satisfied(clause)) return true; - trail_lim.push(trail.size()); - Lit l = lit_Undef; - for (int i = 0; i < c.size(); i++) - if (var(c[i]) != v && value(c[i]) != l_False) - uncheckedEnqueue(~c[i]); - else - l = c[i]; - - if (propagate() != CRef_Undef){ - cancelUntil(0); - asymm_lits++; - if (!strengthenClause(cr, l)) - return false; - }else - cancelUntil(0); + trail_lim.push(trail.size()); + Lit l = lit_Undef; + for (int i = 0; i < clause.size(); i++) + if (var(clause[i]) != v && value(clause[i]) != l_False) + uncheckedEnqueue(~clause[i]); + else + l = clause[i]; - return true; + if (propagate() != CRef_Undef) + { + cancelUntil(0); + asymm_lits++; + if (!strengthenClause(cr, l)) return false; + } + else + cancelUntil(0); + + return true; } @@ -484,18 +498,17 @@ static void mkElimClause(vec<uint32_t>& elimclauses, Lit x) elimclauses.push(1); } - -static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& c) +static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& clause) { int first = elimclauses.size(); int v_pos = -1; // Copy clause to elimclauses-vector. Remember position where the // variable 'v' occurs: - for (int i = 0; i < c.size(); i++){ - elimclauses.push(toInt(c[i])); - if (var(c[i]) == v) - v_pos = i + first; + for (int i = 0; i < clause.size(); i++) + { + elimclauses.push(toInt(clause[i])); + if (var(clause[i]) == v) v_pos = i + first; } assert(v_pos != -1); @@ -506,7 +519,7 @@ static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& c) elimclauses[first] = tmp; // Store the length of the clause last: - elimclauses.push(c.size()); + elimclauses.push(clause.size()); } @@ -590,13 +603,14 @@ bool SimpSolver::substitute(Var v, Lit x) vec<Lit>& subst_clause = add_tmp; for (int i = 0; i < cls.size(); i++){ - Clause& c = ca[cls[i]]; + Clause& clause = ca[cls[i]]; - subst_clause.clear(); - for (int j = 0; j < c.size(); j++){ - Lit p = c[j]; - subst_clause.push(var(p) == v ? x ^ sign(p) : p); - } + subst_clause.clear(); + for (int j = 0; j < clause.size(); j++) + { + Lit p = clause[j]; + subst_clause.push(var(p) == v ? x ^ sign(p) : p); + } removeClause(cls[i]); ClauseId id; diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index 246bb7152..9d3a51c02 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -37,42 +37,55 @@ class SimpSolver : public Solver { public: // Constructor/Destructor: // - SimpSolver(CVC4::context::Context* c); - ~SimpSolver(); - - // Problem specification: - // - Var newVar (bool polarity = true, bool dvar = true, bool freeze = false); - bool addClause (const vec<Lit>& ps, ClauseId& id); - bool addEmptyClause(); // Add the empty clause to the solver. - bool addClause (Lit p, ClauseId& id); // Add a unit clause to the solver. - bool addClause (Lit p, Lit q, ClauseId& id); // Add a binary clause to the solver. - bool addClause (Lit p, Lit q, Lit r, ClauseId& id); // Add a ternary clause to the solver. - bool addClause_( vec<Lit>& ps, ClauseId& id); - bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction). - - // Variable mode: - // - void setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated. - bool isEliminated(Var v) const; - - // Solving: - // - lbool solve (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false); - lbool solveLimited(const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false); - lbool solveLimited(bool do_simp = true, bool turn_off_simp = false); - lbool solve ( bool do_simp = true, bool turn_off_simp = false); - lbool solve (Lit p , bool do_simp = true, bool turn_off_simp = false); - lbool solve (Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false); - lbool solve (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false); - bool eliminate (bool turn_off_elim = false); // Perform variable elimination based simplification. - - // Memory managment: - // - void garbageCollect() override; - - // Generate a (possibly simplified) DIMACS file: - // + SimpSolver(CVC4::context::Context* context); + ~SimpSolver(); + + // Problem specification: + // + Var newVar(bool polarity = true, bool dvar = true, bool freeze = false); + bool addClause(const vec<Lit>& ps, ClauseId& id); + bool addEmptyClause(); // Add the empty clause to the solver. + bool addClause(Lit p, ClauseId& id); // Add a unit clause to the solver. + bool addClause(Lit p, + Lit q, + ClauseId& id); // Add a binary clause to the solver. + bool addClause(Lit p, + Lit q, + Lit r, + ClauseId& id); // Add a ternary clause to the solver. + bool addClause_(vec<Lit>& ps, ClauseId& id); + bool substitute(Var v, Lit x); // Replace all occurences of v with x (may + // cause a contradiction). + + // Variable mode: + // + void setFrozen(Var v, + bool b); // If a variable is frozen it will not be eliminated. + bool isEliminated(Var v) const; + + // Solving: + // + lbool solve(const vec<Lit>& assumps, + bool do_simp = true, + bool turn_off_simp = false); + lbool solveLimited(const vec<Lit>& assumps, + bool do_simp = true, + bool turn_off_simp = false); + lbool solveLimited(bool do_simp = true, bool turn_off_simp = false); + lbool solve(bool do_simp = true, bool turn_off_simp = false); + lbool solve(Lit p, bool do_simp = true, bool turn_off_simp = false); + lbool solve(Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false); + lbool solve( + Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false); + bool eliminate(bool turn_off_elim = false); // Perform variable elimination + // based simplification. + + // Memory managment: + // + void garbageCollect() override; + + // Generate a (possibly simplified) DIMACS file: + // #if 0 void toDimacs (const char* file, const vec<Lit>& assumps); void toDimacs (const char* file); |