From 825b72719ca60e978aef1137699744177199372f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 4 Nov 2013 11:57:29 -0800 Subject: [PATCH] fix https://z3.codeplex.com/workitem/62 Signed-off-by: Leonardo de Moura --- src/sat/sat_simplifier.cpp | 142 ++++++++++++------------ src/sat/sat_solver.cpp | 220 ++++++++++++++++++++----------------- 2 files changed, 189 insertions(+), 173 deletions(-) diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index ba0c67235..37d41a5fd 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -9,7 +9,7 @@ Abstract: SAT simplification procedures that use a "full" occurrence list: Subsumption, Blocked Clause Removal, Variable Elimination, ... - + Author: @@ -54,21 +54,21 @@ namespace sat { m_use_list[l2.index()].erase(c); } } - + simplifier::simplifier(solver & _s, params_ref const & p): s(_s), m_num_calls(0) { updt_params(p); reset_statistics(); } - + simplifier::~simplifier() { } inline watch_list & simplifier::get_wlist(literal l) { return s.get_wlist(l); } inline watch_list const & simplifier::get_wlist(literal l) const { return s.get_wlist(l); } - + inline bool simplifier::is_external(bool_var v) const { return s.is_external(v); } inline bool simplifier::was_eliminated(bool_var v) const { return s.was_eliminated(v); } @@ -78,7 +78,7 @@ namespace sat { lbool simplifier::value(literal l) const { return s.value(l); } inline void simplifier::checkpoint() { s.checkpoint(); } - + void simplifier::register_clauses(clause_vector & cs) { std::stable_sort(cs.begin(), cs.end(), size_lt()); clause_vector::iterator it = cs.begin(); @@ -117,7 +117,7 @@ namespace sat { SASSERT(s.get_wlist(~l1).contains(watched(l2, learned))); s.get_wlist(~l1).erase(watched(l2, learned)); } - + void simplifier::init_visited() { m_visited.reset(); m_visited.resize(2*s.num_vars(), false); @@ -155,7 +155,7 @@ namespace sat { if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls)) elim_blocked_clauses(); - + if (!learned) m_num_calls++; @@ -180,6 +180,7 @@ namespace sat { bool vars_eliminated = m_num_elim_vars > old_num_elim_vars; if (!m_need_cleanup) { + TRACE("after_simplifier", tout << "skipping cleanup...\n";); if (vars_eliminated) { // must remove learned clauses with eliminated variables cleanup_clauses(s.m_learned, true, true, learned_in_use_lists); @@ -189,6 +190,7 @@ namespace sat { free_memory(); return; } + TRACE("after_simplifier", tout << "cleanning watches...\n";); cleanup_watches(); cleanup_clauses(s.m_learned, true, vars_eliminated, learned_in_use_lists); cleanup_clauses(s.m_clauses, false, vars_eliminated, true); @@ -234,7 +236,7 @@ namespace sat { s.del_clause(c); continue; } - + if (learned && vars_eliminated) { unsigned sz = c.size(); unsigned i; @@ -293,7 +295,7 @@ namespace sat { mark_visited(c[i]); } } - + void simplifier::unmark_all(clause const & c) { unsigned sz = c.size(); for (unsigned i = 0; i < sz; i++) @@ -325,7 +327,7 @@ namespace sat { */ bool simplifier::subsumes1(clause const & c1, clause const & c2, literal & l) { unsigned sz2 = c2.size(); - for (unsigned i = 0; i < sz2; i++) + for (unsigned i = 0; i < sz2; i++) mark_visited(c2[i]); bool r = true; @@ -344,7 +346,7 @@ namespace sat { } } - for (unsigned i = 0; i < sz2; i++) + for (unsigned i = 0; i < sz2; i++) unmark_visited(c2[i]); return r; } @@ -353,7 +355,7 @@ namespace sat { \brief Return the clauses subsumed by c1 and the clauses that can be subsumed resolved using c1. The collections is populated using the use list of target. */ - void simplifier::collect_subsumed1_core(clause const & c1, clause_vector & out, literal_vector & out_lits, + void simplifier::collect_subsumed1_core(clause const & c1, clause_vector & out, literal_vector & out_lits, literal target) { clause_use_list const & cs = m_use_list.get(target); clause_use_list::iterator it = cs.mk_iterator(); @@ -362,7 +364,7 @@ namespace sat { CTRACE("resolution_bug", c2.was_removed(), tout << "clause has been removed:\n" << c2 << "\n";); SASSERT(!c2.was_removed()); if (&c2 != &c1 && - c1.size() <= c2.size() && + c1.size() <= c2.size() && approx_subset(c1.approx(), c2.approx())) { m_sub_counter -= c1.size() + c2.size(); literal l; @@ -373,7 +375,7 @@ namespace sat { } it.next(); } - } + } /** \brief Return the clauses subsumed by c1 and the clauses that can be subsumed resolved using c1. @@ -400,7 +402,7 @@ namespace sat { if (*l_it == null_literal) { // c2 was subsumed if (c1.is_learned() && !c2.is_learned()) - c1.unset_learned(); + c1.unset_learned(); TRACE("subsumption", tout << c1 << " subsumed " << c2 << "\n";); remove_clause(c2); m_num_subsumed++; @@ -447,9 +449,9 @@ namespace sat { */ bool simplifier::subsumes0(clause const & c1, clause const & c2) { unsigned sz2 = c2.size(); - for (unsigned i = 0; i < sz2; i++) + for (unsigned i = 0; i < sz2; i++) mark_visited(c2[i]); - + bool r = true; unsigned sz1 = c1.size(); for (unsigned i = 0; i < sz1; i++) { @@ -459,12 +461,12 @@ namespace sat { } } - for (unsigned i = 0; i < sz2; i++) + for (unsigned i = 0; i < sz2; i++) unmark_visited(c2[i]); - + return r; } - + /** \brief Collect the clauses subsumed by c1 (using the occurrence list of target). */ @@ -475,7 +477,7 @@ namespace sat { clause & c2 = it.curr(); SASSERT(!c2.was_removed()); if (&c2 != &c1 && - c1.size() <= c2.size() && + c1.size() <= c2.size() && approx_subset(c1.approx(), c2.approx())) { m_sub_counter -= c1.size() + c2.size(); if (subsumes0(c1, c2)) { @@ -485,7 +487,7 @@ namespace sat { it.next(); } } - + /** \brief Collect the clauses subsumed by c1 */ @@ -493,8 +495,8 @@ namespace sat { literal l = get_min_occ_var0(c1); collect_subsumed0_core(c1, out, l); } - - + + /** \brief Perform backward subsumption using c1. */ @@ -507,16 +509,16 @@ namespace sat { clause & c2 = *(*it); // c2 was subsumed if (c1.is_learned() && !c2.is_learned()) - c1.unset_learned(); + c1.unset_learned(); TRACE("subsumption", tout << c1 << " subsumed " << c2 << "\n";); remove_clause(c2); m_num_subsumed++; } } - + /** \brief Eliminate false literals from c, and update occurrence lists - + Return true if the clause is satisfied */ bool simplifier::cleanup_clause(clause & c, bool in_use_list) { @@ -666,7 +668,7 @@ namespace sat { back_subsumption1(c); if (w.is_learned() && !c.is_learned()) { SASSERT(wlist[j] == w); - TRACE("mark_not_learned_bug", + TRACE("mark_not_learned_bug", tout << "marking as not learned: " << l2 << " " << wlist[j].is_learned() << "\n";); wlist[j].mark_not_learned(); mark_as_not_learned_core(get_wlist(~l2), l); @@ -735,7 +737,7 @@ namespace sat { continue; } if (it2->get_literal() == last_lit) { - TRACE("subsumption", tout << "eliminating: " << ~to_literal(l_idx) + TRACE("subsumption", tout << "eliminating: " << ~to_literal(l_idx) << " " << it2->get_literal() << "\n";); elim++; } @@ -762,12 +764,12 @@ namespace sat { m_num_sub_res(s.m_num_sub_res) { m_watch.start(); } - + ~subsumption_report() { m_watch.stop(); - IF_VERBOSE(SAT_VB_LVL, + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << " (sat-subsumer :subsumed " - << (m_simplifier.m_num_subsumed - m_num_subsumed) + << (m_simplifier.m_num_subsumed - m_num_subsumed) << " :subsumption-resolution " << (m_simplifier.m_num_sub_res - m_num_sub_res) << " :threshold " << m_simplifier.m_sub_counter << mem_stat() @@ -847,12 +849,12 @@ namespace sat { vector const & m_watches; public: literal_lt(use_list const & l, vector const & ws):m_use_list(l), m_watches(ws) {} - + unsigned weight(unsigned l_idx) const { return 2*m_use_list.get(~to_literal(l_idx)).size() + m_watches[l_idx].size(); } - - bool operator()(unsigned l_idx1, unsigned l_idx2) const { + + bool operator()(unsigned l_idx1, unsigned l_idx2) const { return weight(l_idx1) < weight(l_idx2); } }; @@ -861,9 +863,9 @@ namespace sat { heap m_queue; public: queue(use_list const & l, vector const & ws):m_queue(128, literal_lt(l, ws)) {} - void insert(literal l) { + void insert(literal l) { unsigned idx = l.index(); - m_queue.reserve(idx + 1); + m_queue.reserve(idx + 1); SASSERT(!m_queue.contains(idx)); m_queue.insert(idx); } @@ -877,14 +879,14 @@ namespace sat { literal next() { SASSERT(!empty()); return to_literal(m_queue.erase_min()); } bool empty() const { return m_queue.empty(); } }; - + simplifier & s; int m_counter; model_converter & mc; queue m_queue; clause_vector m_to_remove; - blocked_clause_elim(simplifier & _s, unsigned limit, model_converter & _mc, use_list & l, + blocked_clause_elim(simplifier & _s, unsigned limit, model_converter & _mc, use_list & l, vector & wlist): s(_s), m_counter(limit), @@ -946,7 +948,7 @@ namespace sat { clause_vector::iterator it = m_to_remove.begin(); clause_vector::iterator end = m_to_remove.end(); for (; it != end; ++it) { - s.remove_clause(*(*it)); + s.remove_clause(*(*it)); } } { @@ -1025,12 +1027,12 @@ namespace sat { m_num_blocked_clauses(s.m_num_blocked_clauses) { m_watch.start(); } - + ~blocked_cls_report() { m_watch.stop(); - IF_VERBOSE(SAT_VB_LVL, + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << " (sat-blocked-clauses :elim-blocked-clauses " - << (m_simplifier.m_num_blocked_clauses - m_num_blocked_clauses) + << (m_simplifier.m_num_blocked_clauses - m_num_blocked_clauses) << mem_stat() << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";); } @@ -1062,8 +1064,8 @@ namespace sat { unsigned num_neg = m_use_list.get(neg_l).size(); unsigned num_bin_pos = get_num_non_learned_bin(pos_l); unsigned num_bin_neg = get_num_non_learned_bin(neg_l); - unsigned cost = 2 * num_pos * num_neg + num_pos * num_bin_neg + num_neg * num_bin_pos; - CTRACE("elim_vars_detail", cost == 0, tout << v << " num_pos: " << num_pos << " num_neg: " << num_neg << " num_bin_pos: " << num_bin_pos + unsigned cost = 2 * num_pos * num_neg + num_pos * num_bin_neg + num_neg * num_bin_pos; + CTRACE("elim_vars_detail", cost == 0, tout << v << " num_pos: " << num_pos << " num_neg: " << num_neg << " num_bin_pos: " << num_bin_pos << " num_bin_neg: " << num_bin_neg << " cost: " << cost << "\n";); return cost; } @@ -1071,7 +1073,7 @@ namespace sat { typedef std::pair bool_var_and_cost; struct bool_var_and_cost_lt { - bool operator()(bool_var_and_cost const & p1, bool_var_and_cost const & p2) const { return p1.second < p2.second; } + bool operator()(bool_var_and_cost const & p1, bool_var_and_cost const & p2) const { return p1.second < p2.second; } }; void simplifier::order_vars_for_elim(bool_var_vector & r) { @@ -1104,7 +1106,7 @@ namespace sat { r.push_back(it2->first); } } - + /** \brief Collect clauses and binary clauses containing l. */ @@ -1116,7 +1118,7 @@ namespace sat { SASSERT(r.back().size() == it.curr().size()); it.next(); } - + watch_list & wlist = get_wlist(~l); watch_list::iterator it2 = wlist.begin(); watch_list::iterator end2 = wlist.end(); @@ -1129,7 +1131,7 @@ namespace sat { } /** - \brief Resolve clauses c1 and c2. + \brief Resolve clauses c1 and c2. c1 must contain l. c2 must contain ~l. Store result in r. @@ -1149,7 +1151,7 @@ namespace sat { m_visited[l2.index()] = true; r.push_back(l2); } - + literal not_l = ~l; sz = c2.size(); m_elim_counter -= sz; @@ -1164,7 +1166,7 @@ namespace sat { if (!m_visited[l2.index()]) r.push_back(l2); } - + sz = c1.size(); for (unsigned i = 0; i < sz; i++) { literal l2 = c1[i]; @@ -1200,7 +1202,7 @@ namespace sat { break; } } - CTRACE("resolve_bug", it2 == end2, + CTRACE("resolve_bug", it2 == end2, tout << ~l1 << " -> "; display(tout, s.m_cls_allocator, wlist1); tout << "\n" << ~l2 << " -> "; display(tout, s.m_cls_allocator, wlist2); tout << "\n";); @@ -1262,7 +1264,7 @@ namespace sat { TRACE("resolution_bug", tout << "processing: " << v << "\n";); if (value(v) != l_undef) return false; - + literal pos_l(v, false); literal neg_l(v, true); unsigned num_bin_pos = get_num_non_learned_bin(pos_l); @@ -1274,12 +1276,12 @@ namespace sat { m_elim_counter -= num_pos + num_neg; TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << "\n";); - + if (num_pos >= m_res_occ_cutoff && num_neg >= m_res_occ_cutoff) return false; unsigned before_lits = num_bin_pos*2 + num_bin_neg*2; - + { clause_use_list::iterator it = pos_occs.mk_iterator(); while (!it.at_end()) { @@ -1287,7 +1289,7 @@ namespace sat { it.next(); } } - + { clause_use_list::iterator it2 = neg_occs.mk_iterator(); while (!it2.at_end()) { @@ -1297,23 +1299,23 @@ namespace sat { } TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << " before_lits: " << before_lits << "\n";); - + if (num_pos >= m_res_occ_cutoff3 && num_neg >= m_res_occ_cutoff3 && before_lits > m_res_lit_cutoff3 && s.m_clauses.size() > m_res_cls_cutoff2) return false; - if (num_pos >= m_res_occ_cutoff2 && num_neg >= m_res_occ_cutoff2 && before_lits > m_res_lit_cutoff2 && + if (num_pos >= m_res_occ_cutoff2 && num_neg >= m_res_occ_cutoff2 && before_lits > m_res_lit_cutoff2 && s.m_clauses.size() > m_res_cls_cutoff1 && s.m_clauses.size() <= m_res_cls_cutoff2) return false; - if (num_pos >= m_res_occ_cutoff1 && num_neg >= m_res_occ_cutoff1 && before_lits > m_res_lit_cutoff1 && + if (num_pos >= m_res_occ_cutoff1 && num_neg >= m_res_occ_cutoff1 && before_lits > m_res_lit_cutoff1 && s.m_clauses.size() <= m_res_cls_cutoff1) return false; - + m_pos_cls.reset(); m_neg_cls.reset(); collect_clauses(pos_l, m_pos_cls); collect_clauses(neg_l, m_neg_cls); - + m_elim_counter -= num_pos * num_neg + before_lits; - + TRACE("resolution_detail", tout << "collecting number of after_clauses\n";); unsigned before_clauses = num_pos + num_neg; unsigned after_clauses = 0; @@ -1350,7 +1352,7 @@ namespace sat { neg_occs.reset(); m_elim_counter -= num_pos * num_neg + before_lits; - + it1 = m_pos_cls.begin(); end1 = m_pos_cls.end(); for (; it1 != end1; ++it1) { @@ -1393,7 +1395,7 @@ namespace sat { return true; } } - + return true; } @@ -1406,10 +1408,10 @@ namespace sat { m_num_elim_vars(s.m_num_elim_vars) { m_watch.start(); } - + ~elim_var_report() { m_watch.stop(); - IF_VERBOSE(SAT_VB_LVL, + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << " (sat-resolution :elim-bool-vars " << (m_simplifier.m_num_elim_vars - m_num_elim_vars) << " :threshold " << m_simplifier.m_elim_counter @@ -1417,12 +1419,12 @@ namespace sat { << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";); } }; - + void simplifier::elim_vars() { elim_var_report rpt(*this); bool_var_vector vars; order_vars_for_elim(vars); - + bool_var_vector::iterator it = vars.begin(); bool_var_vector::iterator end = vars.end(); for (; it != end; ++it) { @@ -1463,7 +1465,7 @@ namespace sat { void simplifier::collect_param_descrs(param_descrs & r) { sat_simplifier_params::collect_param_descrs(r); } - + void simplifier::collect_statistics(statistics & st) { st.update("subsumed", m_num_subsumed); st.update("subsumption resolution", m_num_sub_res); @@ -1471,7 +1473,7 @@ namespace sat { st.update("elim bool vars", m_num_elim_vars); st.update("elim blocked clauses", m_num_blocked_clauses); } - + void simplifier::reset_statistics() { m_num_blocked_clauses = 0; m_num_subsumed = 0; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index d9e11724c..bb08ae5c3 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -27,7 +27,7 @@ Revision History: // define to create a copy of the solver before starting the search // useful for checking models // #define CLONE_BEFORE_SOLVING - + namespace sat { solver::solver(params_ref const & p, extension * ext): @@ -103,7 +103,7 @@ namespace sat { } } } - + // ----------------------- // // Variable & Clause creation @@ -312,7 +312,7 @@ namespace sat { /** \brief Select a watch literal starting the search at the given position. This method is only used for clauses created during the search. - + I use the following rules to select a watch literal. 1- select a literal l in idx >= starting_at such that value(l) = l_true, @@ -329,7 +329,7 @@ namespace sat { lvl(l) >= lvl(l') Without rule 3, boolean propagation is incomplete, that is, it may miss possible propagations. - + \remark The method select_lemma_watch_lit is used to select the watch literal for regular learned clauses. */ unsigned solver::select_watch_lit(clause const & cls, unsigned starting_at) const { @@ -443,7 +443,7 @@ namespace sat { erase_clause_watch(get_wlist(~c[0]), cls_off); erase_clause_watch(get_wlist(~c[1]), cls_off); } - + void solver::dettach_ter_clause(clause & c) { erase_ternary_watch(get_wlist(~c[0]), c[1], c[2]); erase_ternary_watch(get_wlist(~c[1]), c[0], c[2]); @@ -498,10 +498,10 @@ namespace sat { unsigned sz = c.size(); for (unsigned i = 0; i < sz; i++) { switch (value(c[i])) { - case l_true: + case l_true: return l_true; - case l_undef: - found_undef = true; + case l_undef: + found_undef = true; break; default: break; @@ -515,7 +515,7 @@ namespace sat { // Propagation // // ----------------------- - + bool solver::propagate_core(bool update) { if (m_inconsistent) return false; @@ -545,7 +545,7 @@ namespace sat { } for (; it != end; ++it) { switch (it->get_kind()) { - case watched::BINARY: + case watched::BINARY: l1 = it->get_literal(); switch (value(l1)) { case l_false: @@ -585,12 +585,26 @@ namespace sat { break; case watched::CLAUSE: { if (value(it->get_blocked_literal()) == l_true) { + TRACE("propagate_clause_bug", tout << "blocked literal " << it->get_blocked_literal() << "\n"; + clause_offset cls_off = it->get_clause_offset(); + clause & c = *(m_cls_allocator.get_clause(cls_off)); + tout << c << "\n";); *it2 = *it; it2++; break; } clause_offset cls_off = it->get_clause_offset(); clause & c = *(m_cls_allocator.get_clause(cls_off)); + TRACE("propagate_clause_bug", tout << "processing... " << c << "\nwas_removed: " << c.was_removed() << "\n";); + if (c.was_removed()) { + // Remark: this method may be invoked when the watch lists are not in a consistent state, + // and may contain dead/removed clauses. + // See: sat_simplifier.cpp + // So, we must check whether the clause was marked for deletion, and ignore it. + *it2 = *it; + it2++; + break; + } if (c[0] == not_l) std::swap(c[0], c[1]); CTRACE("propagate_bug", c[1] != not_l, tout << "l: " << l << " " << c << "\n";); @@ -693,7 +707,7 @@ namespace sat { m_conflicts_since_restart = 0; m_restart_threshold = m_config.m_restart_initial; } - + // iff3_finder(*this)(); simplify_problem(); @@ -704,10 +718,10 @@ namespace sat { IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"abort: max-conflicts = 0\"\n";); return l_undef; } - + while (true) { SASSERT(!inconsistent()); - + lbool r = bounded_search(); if (r != l_undef) return r; @@ -716,7 +730,7 @@ namespace sat { IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"abort: max-conflicts = " << m_conflicts << "\"\n";); return l_undef; } - + restart(); if (m_conflicts >= m_next_simplify) { simplify_problem(); @@ -734,7 +748,7 @@ namespace sat { bool_var solver::next_var() { bool_var next; - + if (m_rand() < static_cast(m_config.m_random_freq * random_gen::max_value())) { if (num_vars() == 0) return null_bool_var; @@ -743,16 +757,16 @@ namespace sat { if (value(next) == l_undef && !was_eliminated(next)) return next; } - + while (!m_case_split_queue.empty()) { next = m_case_split_queue.next_var(); if (value(next) == l_undef && !was_eliminated(next)) return next; } - + return null_bool_var; } - + bool solver::decide() { bool_var next = next_var(); if (next == null_bool_var) @@ -760,7 +774,7 @@ namespace sat { push(); m_stats.m_decision++; lbool phase = m_ext ? m_ext->get_phase(next) : l_undef; - + if (phase == l_undef) { switch (m_config.m_phase) { case PS_ALWAYS_TRUE: @@ -784,7 +798,7 @@ namespace sat { break; } } - + SASSERT(phase != l_undef); literal next_lit(next, phase == l_false); assign(next_lit, justification()); @@ -807,23 +821,23 @@ namespace sat { return l_undef; if (scope_lvl() == 0) { cleanup(); // cleaner may propagate frozen clauses - if (inconsistent()) + if (inconsistent()) return l_false; gc(); } } - + gc(); if (!decide()) { if (m_ext) { switch (m_ext->check()) { - case CR_DONE: + case CR_DONE: mk_model(); return l_true; - case CR_CONTINUE: + case CR_CONTINUE: break; - case CR_GIVEUP: + case CR_GIVEUP: throw abort_solver(); } } @@ -849,23 +863,23 @@ namespace sat { m_stopwatch.reset(); m_stopwatch.start(); } - + /** \brief Apply all simplifications. */ void solver::simplify_problem() { SASSERT(scope_lvl() == 0); - + m_cleaner(); CASSERT("sat_simplify_bug", check_invariant()); - + m_scc(); CASSERT("sat_simplify_bug", check_invariant()); - - m_simplifier(false); + + m_simplifier(false); CASSERT("sat_simplify_bug", check_invariant()); CASSERT("sat_missed_prop", check_missed_propagation()); - + if (!m_learned.empty()) { m_simplifier(true); CASSERT("sat_missed_prop", check_missed_propagation()); @@ -878,11 +892,11 @@ namespace sat { m_probing(); CASSERT("sat_missed_prop", check_missed_propagation()); CASSERT("sat_simplify_bug", check_invariant()); - + m_asymm_branch(); CASSERT("sat_missed_prop", check_missed_propagation()); CASSERT("sat_simplify_bug", check_invariant()); - + if (m_ext) { m_ext->clauses_modifed(); m_ext->simplify(); @@ -956,7 +970,7 @@ namespace sat { } } } - if (!m_mc.check_model(m)) + if (!m_mc.check_model(m)) ok = false; CTRACE("sat_model_bug", !ok, tout << m << "\n";); return ok; @@ -964,9 +978,9 @@ namespace sat { void solver::restart() { m_stats.m_restart++; - IF_VERBOSE(1, + IF_VERBOSE(1, verbose_stream() << "(sat-restart :conflicts " << m_stats.m_conflict << " :decisions " << m_stats.m_decision - << " :restarts " << m_stats.m_restart << mk_stat(*this) + << " :restarts " << m_stats.m_restart << mk_stat(*this) << " :time " << std::fixed << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";); IF_VERBOSE(30, display_status(verbose_stream());); pop(scope_lvl()); @@ -991,9 +1005,9 @@ namespace sat { // GC // // ----------------------- - + void solver::gc() { - if (m_conflicts_since_gc <= m_gc_threshold) + if (m_conflicts_since_gc <= m_gc_threshold) return; CASSERT("sat_gc_bug", check_invariant()); switch (m_config.m_gc_strategy) { @@ -1073,7 +1087,7 @@ namespace sat { std::stable_sort(m_learned.begin(), m_learned.end(), glue_lt()); gc_half("glue"); } - + void solver::gc_psm() { save_psm(); std::stable_sort(m_learned.begin(), m_learned.end(), psm_lt()); @@ -1134,8 +1148,8 @@ namespace sat { void solver::gc_dyn_psm() { // To do gc at scope_lvl() > 0, I will need to use the reinitialization stack, or live with the fact // that I may miss some propagations for reactivated clauses. - SASSERT(scope_lvl() == 0); - // compute + SASSERT(scope_lvl() == 0); + // compute // d_tk unsigned h = 0; unsigned V_tk = 0; @@ -1152,7 +1166,7 @@ namespace sat { double d_tk = V_tk == 0 ? static_cast(num_vars() + 1) : static_cast(h)/static_cast(V_tk); if (d_tk < m_min_d_tk) m_min_d_tk = d_tk; - TRACE("sat_frozen", tout << "m_min_d_tk: " << m_min_d_tk << "\n";); + TRACE("sat_frozen", tout << "m_min_d_tk: " << m_min_d_tk << "\n";); unsigned frozen = 0; unsigned deleted = 0; unsigned activated = 0; @@ -1218,15 +1232,15 @@ namespace sat { ++it2; } m_learned.set_end(it2); - IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :d_tk " << d_tk << " :min-d_tk " << m_min_d_tk << + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :d_tk " << d_tk << " :min-d_tk " << m_min_d_tk << " :frozen " << frozen << " :activated " << activated << " :deleted " << deleted << ")\n";); } - + // return true if should keep the clause, and false if we should delete it. - bool solver::activate_frozen_clause(clause & c) { + bool solver::activate_frozen_clause(clause & c) { TRACE("sat_gc", tout << "reactivating:\n" << c << "\n";); SASSERT(scope_lvl() == 0); - // do some cleanup + // do some cleanup unsigned sz = c.size(); unsigned j = 0; for (unsigned i = 0; i < sz; i++) { @@ -1292,7 +1306,7 @@ namespace sat { bool r = resolve_conflict_core(); CASSERT("sat_check_marks", check_marks()); // after pop, clauses are reinitialized, this may trigger another conflict. - if (!r) + if (!r) return false; if (!inconsistent()) return true; @@ -1311,7 +1325,7 @@ namespace sat { if (m_conflict_lvl == 0) return false; m_lemma.reset(); - + forget_phase_of_vars(m_conflict_lvl); unsigned idx = skip_literals_above_conflict_level(); @@ -1326,7 +1340,7 @@ namespace sat { literal consequent = m_not_l; justification js = m_conflict; - + do { TRACE("sat_conflict_detail", tout << "processing consequent: " << consequent << "\n"; tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << "\n";); @@ -1362,7 +1376,7 @@ namespace sat { fill_ext_antecedents(consequent, js); literal_vector::iterator it = m_ext_antecedents.begin(); literal_vector::iterator end = m_ext_antecedents.end(); - for (; it != end; ++it) + for (; it != end; ++it) process_antecedent(*it, num_marks); break; } @@ -1370,10 +1384,10 @@ namespace sat { UNREACHABLE(); break; } - + while (true) { literal l = m_trail[idx]; - if (is_marked(l.var())) + if (is_marked(l.var())) break; SASSERT(idx > 0); idx--; @@ -1386,9 +1400,9 @@ namespace sat { idx--; num_marks--; reset_mark(c_var); - } + } while (num_marks > 0); - + m_lemma[0] = ~consequent; TRACE("sat_lemma", tout << "new lemma size: " << m_lemma.size() << "\n" << m_lemma << "\n";); @@ -1401,7 +1415,7 @@ namespace sat { } else reset_lemma_var_marks(); - + literal_vector::iterator it = m_lemma.begin(); literal_vector::iterator end = m_lemma.end(); unsigned new_scope_lvl = 0; @@ -1432,10 +1446,10 @@ namespace sat { return 0; unsigned r = 0; - + if (consequent != null_literal) r = lvl(consequent); - + switch (js.get_kind()) { case justification::NONE: break; @@ -1468,7 +1482,7 @@ namespace sat { fill_ext_antecedents(consequent, js); literal_vector::iterator it = m_ext_antecedents.begin(); literal_vector::iterator end = m_ext_antecedents.end(); - for (; it != end; ++it) + for (; it != end; ++it) r = std::max(r, lvl(*it)); break; } @@ -1497,7 +1511,7 @@ namespace sat { } return idx; } - + void solver::process_antecedent(literal antecedent, unsigned & num_marks) { bool_var var = antecedent.var(); unsigned var_lvl = lvl(var); @@ -1511,7 +1525,7 @@ namespace sat { m_lemma.push_back(~antecedent); } } - + /** \brief js is an external justification. Collect its antecedents and store at m_ext_antecedents. */ @@ -1578,7 +1592,7 @@ namespace sat { unsigned var_lvl = lvl(var); if (!is_marked(var) && var_lvl > 0) { if (m_lvl_set.may_contain(var_lvl)) { - mark(var); + mark(var); m_unmark.push_back(var); m_lemma_min_stack.push_back(var); } @@ -1590,17 +1604,17 @@ namespace sat { } /** - \brief Return true if lit is implied by other marked literals - and/or literals assigned at the base level. - The set lvl_set is used as an optimization. + \brief Return true if lit is implied by other marked literals + and/or literals assigned at the base level. + The set lvl_set is used as an optimization. The idea is to stop the recursive search with a failure - as soon as we find a literal assigned in a level that is not in lvl_set. + as soon as we find a literal assigned in a level that is not in lvl_set. */ bool solver::implied_by_marked(literal lit) { m_lemma_min_stack.reset(); // avoid recursive function m_lemma_min_stack.push_back(lit.var()); unsigned old_size = m_unmark.size(); - + while (!m_lemma_min_stack.empty()) { bool_var var = m_lemma_min_stack.back(); m_lemma_min_stack.pop_back(); @@ -1701,7 +1715,7 @@ namespace sat { void solver::minimize_lemma() { m_unmark.reset(); updt_lemma_lvl_set(); - + unsigned sz = m_lemma.size(); unsigned i = 1; // the first literal is the FUIP unsigned j = 1; @@ -1717,12 +1731,12 @@ namespace sat { j++; } } - + reset_unmark(0); m_lemma.shrink(j); m_stats.m_minimized_lits += sz - j; } - + /** \brief Reset the mark of the variables in the current lemma. */ @@ -1742,17 +1756,17 @@ namespace sat { Only binary and ternary clauses are used. */ void solver::dyn_sub_res() { - unsigned sz = m_lemma.size(); + unsigned sz = m_lemma.size(); for (unsigned i = 0; i < sz; i++) { mark_lit(m_lemma[i]); } - + literal l0 = m_lemma[0]; // l0 is the FUIP, and we never remove the FUIP. - // + // // In the following loop, we use unmark_lit(l) to remove a // literal from m_lemma. - + for (unsigned i = 0; i < sz; i++) { literal l = m_lemma[i]; if (!is_marked_lit(l)) @@ -1764,8 +1778,8 @@ namespace sat { for (; it != end; ++it) { // In this for-loop, the conditions l0 != ~l2 and l0 != ~l3 // are not really needed if the solver does not miss unit propagations. - // However, we add them anyway because we don't want to rely on this - // property of the propagator. + // However, we add them anyway because we don't want to rely on this + // property of the propagator. // For example, if this property is relaxed in the future, then the code // without the conditions l0 != ~l2 and l0 != ~l3 may remove the FUIP if (it->is_binary_clause()) { @@ -1811,10 +1825,10 @@ namespace sat { // p1 \/ ~p2 // p2 \/ ~p3 // p3 \/ ~p4 - // q1 \/ q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2 - // q1 \/ ~q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2 - // ~q1 \/ q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2 - // ~q1 \/ ~q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2 + // q1 \/ q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2 + // q1 \/ ~q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2 + // ~q1 \/ q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2 + // ~q1 \/ ~q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2 // ... // // 2. Now suppose we learned the lemma @@ -1825,15 +1839,15 @@ namespace sat { // That is, l \/ l2 is an implied clause. Note that probing does not add // this clause to the clause database (there are too many). // - // 4. Lemma (*) is deleted (garbage collected). + // 4. Lemma (*) is deleted (garbage collected). // // 5. l is decided to be false, p1, p2, p3 and p4 are propagated using BCP, // but l2 is not since the lemma (*) was deleted. - // + // // Probing module still "knows" that l \/ l2 is valid binary clause - // + // // 6. A new lemma is created where ~l2 is the FUIP and the lemma also contains l. - // If we remove l0 != ~l2 may try to delete the FUIP. + // If we remove l0 != ~l2 may try to delete the FUIP. if (is_marked_lit(~l2) && l0 != ~l2) { // eliminate ~l2 from lemma because we have the clause l \/ l2 unmark_lit(~l2); @@ -1844,7 +1858,7 @@ namespace sat { // can't eliminat FUIP SASSERT(is_marked_lit(m_lemma[0])); - + unsigned j = 0; for (unsigned i = 0; i < sz; i++) { literal l = m_lemma[i]; @@ -1856,7 +1870,7 @@ namespace sat { } m_stats.m_dyn_sub_res += sz - j; - + SASSERT(j >= 1); m_lemma.shrink(j); } @@ -1949,7 +1963,7 @@ namespace sat { // Misc // // ----------------------- - + void solver::updt_params(params_ref const & p) { m_params = p; m_config.updt_params(p); @@ -1971,7 +1985,7 @@ namespace sat { void solver::set_cancel(bool f) { m_cancel = f; } - + void solver::collect_statistics(statistics & st) { m_stats.collect_statistics(st); m_cleaner.collect_statistics(st); @@ -2067,7 +2081,7 @@ namespace sat { } } } - + void solver::display_units(std::ostream & out) const { unsigned end = scope_lvl() == 0 ? m_trail.size() : m_scopes[0].m_trail_lim; for (unsigned i = 0; i < end; i++) { @@ -2221,26 +2235,26 @@ namespace sat { // Simplification // // ----------------------- - void solver::cleanup() { - if (scope_lvl() > 0 || inconsistent()) - return; + void solver::cleanup() { + if (scope_lvl() > 0 || inconsistent()) + return; if (m_cleaner() && m_ext) m_ext->clauses_modifed(); } - void solver::simplify(bool learned) { - if (scope_lvl() > 0 || inconsistent()) - return; - m_simplifier(learned); - m_simplifier.free_memory(); + void solver::simplify(bool learned) { + if (scope_lvl() > 0 || inconsistent()) + return; + m_simplifier(learned); + m_simplifier.free_memory(); if (m_ext) m_ext->clauses_modifed(); } - unsigned solver::scc_bin() { - if (scope_lvl() > 0 || inconsistent()) - return 0; - unsigned r = m_scc(); + unsigned solver::scc_bin() { + if (scope_lvl() > 0 || inconsistent()) + return 0; + unsigned r = m_scc(); if (r > 0 && m_ext) m_ext->clauses_modifed(); return r; @@ -2314,10 +2328,10 @@ namespace sat { out << " :inconsistent " << (m_inconsistent ? "true" : "false") << "\n"; out << " :vars " << num_vars() << "\n"; out << " :elim-vars " << num_elim << "\n"; - out << " :lits " << num_lits << "\n"; + out << " :lits " << num_lits << "\n"; out << " :assigned " << m_trail.size() << "\n"; - out << " :binary-clauses " << num_bin << "\n"; - out << " :ternary-clauses " << num_ter << "\n"; + out << " :binary-clauses " << num_bin << "\n"; + out << " :ternary-clauses " << num_ter << "\n"; out << " :clauses " << num_cls << "\n"; out << " :del-clause " << m_stats.m_del_clause << "\n"; out << " :avg-clause-size " << (total_cls == 0 ? 0.0 : static_cast(num_lits) / static_cast(total_cls)) << "\n";