From 018411bc5816c1655f20193663ae643d990cd169 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 1 Dec 2017 08:23:55 -0800 Subject: [PATCH] fix bug in PB constraint init_watch handling, adding transitive reduction, HLE, ULT, Signed-off-by: Nikolaj Bjorner --- src/sat/ba_solver.cpp | 53 ++++++------ src/sat/ba_solver.h | 8 +- src/sat/sat_asymm_branch.cpp | 81 +++++++++++++------ src/sat/sat_asymm_branch.h | 8 +- src/sat/sat_asymm_branch_params.pyg | 2 + src/sat/sat_lookahead.cpp | 94 +++++++++++++++++++--- src/sat/sat_scc.cpp | 120 +++++++++++++++------------- src/sat/sat_scc.h | 14 ++-- src/sat/sat_simplifier_params.pyg | 2 +- src/sat/sat_solver.h | 2 +- 10 files changed, 248 insertions(+), 136 deletions(-) diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index a1a80df97..05dde2331 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -216,12 +216,12 @@ namespace sat { // ---------------------------- // card - bool ba_solver::init_watch(card& c, bool is_true) { + bool ba_solver::init_watch(card& c) { clear_watch(c); literal root = c.lit(); - if (root != null_literal && root.sign() == is_true) { + if (root != null_literal && value(root) == l_false) { c.negate(); - root.neg(); + root.neg(); } if (root != null_literal) { if (!is_watched(root, c)) watch_literal(root, c); @@ -352,7 +352,7 @@ namespace sat { IF_VERBOSE(100, display(verbose_stream() << "nullify tracking literal\n", p, true);); SASSERT(lvl(p.lit()) == 0); nullify_tracking_literal(p); - init_watch(p, true); + init_watch(p); } SASSERT(p.lit() == null_literal || value(p.lit()) != l_false); @@ -379,7 +379,7 @@ namespace sat { } else if (true_val == 0 && num_false == 0) { if (p.lit() == null_literal || value(p.lit()) == l_true) { - init_watch(p, true); + init_watch(p); } } else if (true_val >= p.k()) { @@ -431,7 +431,7 @@ namespace sat { return; } else if (p.lit() == null_literal || value(p.lit()) == l_true) { - init_watch(p, true); + init_watch(p); } else { SASSERT(value(p.lit()) == l_undef); @@ -510,13 +510,13 @@ namespace sat { // watch a prefix of literals, such that the slack of these is >= k - bool ba_solver::init_watch(pb& p, bool is_true) { + bool ba_solver::init_watch(pb& p) { clear_watch(p); - if (p.lit() != null_literal && p.lit().sign() == is_true) { - p.negate(); + if (p.lit() != null_literal && value(p.lit()) == l_false) { + p.negate(); } - SASSERT(p.lit() == null_literal || value(p.lit()) == l_true); + VERIFY(p.lit() == null_literal || value(p.lit()) == l_true); unsigned sz = p.size(), bound = p.k(); // put the non-false literals into the head. @@ -548,7 +548,7 @@ namespace sat { if (slack < bound) { literal lit = p[j].second; - SASSERT(value(lit) == l_false); + VERIFY(value(lit) == l_false); for (unsigned i = j + 1; i < sz; ++i) { if (lvl(lit) < lvl(p[i].second)) { lit = p[i].second; @@ -826,7 +826,7 @@ namespace sat { SASSERT(p.well_formed()); if (p.lit() == null_literal || value(p.lit()) == l_true) { - init_watch(p, true); + init_watch(p); } } } @@ -909,9 +909,9 @@ namespace sat { return odd; } - bool ba_solver::init_watch(xor& x, bool is_true) { + bool ba_solver::init_watch(xor& x) { clear_watch(x); - if (x.lit() != null_literal && x.lit().sign() == is_true) { + if (x.lit() != null_literal && value(x.lit()) == l_false) { x.negate(); } TRACE("ba", display(tout, x, true);); @@ -1566,7 +1566,7 @@ namespace sat { m_constraint_to_reinit.push_back(c); } else if (lit == null_literal) { - init_watch(*c, true); + init_watch(*c); } else { if (m_solver) m_solver->set_external(lit.var()); @@ -1577,12 +1577,12 @@ namespace sat { } - bool ba_solver::init_watch(constraint& c, bool is_true) { + bool ba_solver::init_watch(constraint& c) { if (inconsistent()) return false; switch (c.tag()) { - case card_t: return init_watch(c.to_card(), is_true); - case pb_t: return init_watch(c.to_pb(), is_true); - case xor_t: return init_watch(c.to_xor(), is_true); + case card_t: return init_watch(c.to_card()); + case pb_t: return init_watch(c.to_pb()); + case xor_t: return init_watch(c.to_xor()); } UNREACHABLE(); return false; @@ -1642,7 +1642,7 @@ namespace sat { constraint& c = index2constraint(idx); TRACE("ba", tout << l << "\n";); if (c.lit() != null_literal && l.var() == c.lit().var()) { - init_watch(c, !l.sign()); + init_watch(c); return true; } else if (c.lit() != null_literal && value(c.lit()) != l_true) { @@ -2358,7 +2358,7 @@ namespace sat { unsigned sz = m_constraint_to_reinit_last_sz; for (unsigned i = sz; i < m_constraint_to_reinit.size(); ++i) { constraint* c = m_constraint_to_reinit[i]; - if (!init_watch(*c, true) && !s().at_base_lvl()) { + if (!init_watch(*c) && !s().at_base_lvl()) { m_constraint_to_reinit[sz++] = c; } } @@ -2677,7 +2677,7 @@ namespace sat { } else { if (c.lit() == null_literal || value(c.lit()) == l_true) { - init_watch(c, true); + init_watch(c); } SASSERT(c.lit() == null_literal || is_watched(c.lit(), c)); SASSERT(c.well_formed()); @@ -2753,10 +2753,7 @@ namespace sat { recompile(c); } else { - // review for potential incompleteness: if c.lit() == l_false, do propagations happen? - if (c.lit() == null_literal || value(c.lit()) == l_true) { - init_watch(c, true); - } + if (c.lit() == null_literal || value(c.lit()) != l_undef) init_watch(c); SASSERT(c.well_formed()); } } @@ -2870,7 +2867,6 @@ namespace sat { s().set_external(v); } } - IF_VERBOSE(10, verbose_stream() << "non-external variables converted: " << ext << "\n";); return ext; } @@ -2897,7 +2893,6 @@ namespace sat { ++pure_literals; } } - IF_VERBOSE(10, verbose_stream() << "pure literals converted: " << pure_literals << " " << inconsistent() << "\n";); return pure_literals; } @@ -3119,7 +3114,7 @@ namespace sat { } } c2.set_size(c2.size() - 1); - init_watch(c2, true); + init_watch(c2); m_simplify_change = true; #endif } diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h index 4eb46609f..b5ea1e1ad 100644 --- a/src/sat/ba_solver.h +++ b/src/sat/ba_solver.h @@ -296,7 +296,7 @@ namespace sat { void watch_literal(wliteral w, pb& p); bool is_watched(literal l, constraint const& c) const; void add_constraint(constraint* c); - bool init_watch(constraint& c, bool is_true); + bool init_watch(constraint& c); void init_watch(bool_var v); void clear_watch(constraint& c); lbool add_assign(constraint& c, literal l); @@ -320,7 +320,7 @@ namespace sat { // cardinality - bool init_watch(card& c, bool is_true); + bool init_watch(card& c); lbool add_assign(card& c, literal lit); void clear_watch(card& c); void reset_coeffs(); @@ -334,7 +334,7 @@ namespace sat { // xor specific functionality void clear_watch(xor& x); - bool init_watch(xor& x, bool is_true); + bool init_watch(xor& x); bool parity(xor const& x, unsigned offset) const; lbool add_assign(xor& x, literal alit); void get_xor_antecedents(literal l, unsigned index, justification js, literal_vector& r); @@ -345,7 +345,7 @@ namespace sat { // pb functionality unsigned m_a_max; - bool init_watch(pb& p, bool is_true); + bool init_watch(pb& p); lbool add_assign(pb& p, literal alit); void add_index(pb& p, unsigned index, literal lit); void clear_watch(pb& p); diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index f88f4c5a7..869b4ac4c 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -59,7 +59,7 @@ namespace sat { } }; - void asymm_branch::process(clause_vector& clauses) { + void asymm_branch::process(scc& scc, clause_vector& clauses) { int64 limit = -m_asymm_branch_limit; std::stable_sort(clauses.begin(), clauses.end(), clause_size_lt()); m_counter -= clauses.size(); @@ -83,8 +83,9 @@ namespace sat { } s.checkpoint(); clause & c = *(*it); - if (!process(c)) + if (m_asymm_branch_sampled ? !process_sampled(scc, c) : !process(c)) { continue; // clause was removed + } *it2 = *it; ++it2; } @@ -103,7 +104,7 @@ namespace sat { void asymm_branch::operator()(bool force) { ++m_calls; - if (m_calls <= 1) + if (m_calls <= m_asymm_branch_delay) return; if (!m_asymm_branch && !m_asymm_branch_all) return; @@ -118,9 +119,27 @@ namespace sat { TRACE("asymm_branch_detail", s.display(tout);); report rpt(*this); svector saved_phase(s.m_phase); - m_counter = 0; - process(s.m_clauses); - m_counter = -m_counter; + if (m_asymm_branch_sampled) { + scc scc(s, m_params); + while (true) { + unsigned elim = m_elim_literals; + scc.init_big(true); + process(scc, s.m_clauses); + process(scc, s.m_learned); + s.propagate(false); + if (s.m_inconsistent) + break; + std::cout << m_elim_literals - elim << "\n"; + if (m_elim_literals == elim) + break; + } + } + else { + scc scc(s, m_params); + m_counter = 0; + process(scc, s.m_clauses); + m_counter = -m_counter; + } s.m_phase = saved_phase; m_asymm_branch_limit *= 2; if (m_asymm_branch_limit > UINT_MAX) @@ -145,12 +164,6 @@ namespace sat { return true; } - void asymm_branch::setup_big() { - scc scc(s, m_params); - vector const& big = scc.get_big(true); // include learned binary clauses - - } - struct asymm_branch::compare_left { scc& s; compare_left(scc& s): s(s) {} @@ -206,19 +219,34 @@ namespace sat { right = right2; } } - right = scc.get_right(m_neg[0]); - for (unsigned i = 1; i < m_neg.size(); ++i) { - literal lit = m_neg[i]; - int right2 = scc.get_right(lit); - if (right > right2) { - // ~first => ~lit - m_to_delete.push_back(~lit); - } - else { - right = right2; + if (m_to_delete.empty()) { + right = scc.get_right(m_neg[0]); + for (unsigned i = 1; i < m_neg.size(); ++i) { + literal lit = m_neg[i]; + int right2 = scc.get_right(lit); + if (right > right2) { + // ~first => ~lit + m_to_delete.push_back(~lit); + } + else { + right = right2; + } } } if (!m_to_delete.empty()) { +#if 0 + std::cout << "delete " << m_to_delete << "\n"; + + std::cout << "pos\n"; + for (literal l : m_pos) { + std::cout << l << ": " << scc.get_left(l) << " " << scc.get_right(l) << "\n"; + } + std::cout << "neg\n"; + for (literal l : m_neg) { + std::cout << l << ": " << scc.get_left(l) << " " << scc.get_right(l) << "\n"; + } + std::cout << "\n"; +#endif unsigned j = 0; for (unsigned i = 0; i < c.size(); ++i) { if (!m_to_delete.contains(c[i])) { @@ -282,13 +310,13 @@ namespace sat { break; } } - new_sz = j; - m_elim_literals += c.size() - new_sz; + new_sz = j; // std::cout << "cleanup: " << c.id() << ": " << literal_vector(new_sz, c.begin()) << " delta: " << (c.size() - new_sz) << " " << skip_idx << " " << new_sz << "\n"; return re_attach(scoped_d, c, new_sz); } bool asymm_branch::re_attach(scoped_detach& scoped_d, clause& c, unsigned new_sz) { + m_elim_literals += c.size() - new_sz; switch(new_sz) { case 0: s.set_conflict(justification()); @@ -315,8 +343,9 @@ namespace sat { } } - bool asymm_branch::process2(scc& scc, clause & c) { + bool asymm_branch::process_sampled(scc& scc, clause & c) { scoped_detach scoped_d(s, c); + sort(scc, c); if (uhte(scc, c)) { scoped_d.del_clause(); return false; @@ -372,6 +401,8 @@ namespace sat { void asymm_branch::updt_params(params_ref const & _p) { sat_asymm_branch_params p(_p); m_asymm_branch = p.asymm_branch(); + m_asymm_branch_delay = p.asymm_branch_delay(); + m_asymm_branch_sampled = p.asymm_branch_sampled(); m_asymm_branch_limit = p.asymm_branch_limit(); m_asymm_branch_all = p.asymm_branch_all(); if (m_asymm_branch_limit > UINT_MAX) diff --git a/src/sat/sat_asymm_branch.h b/src/sat/sat_asymm_branch.h index 87e5cbac5..b7e2b0218 100644 --- a/src/sat/sat_asymm_branch.h +++ b/src/sat/sat_asymm_branch.h @@ -39,6 +39,8 @@ namespace sat { // config bool m_asymm_branch; + unsigned m_asymm_branch_delay; + bool m_asymm_branch_sampled; bool m_asymm_branch_all; int64 m_asymm_branch_limit; @@ -60,9 +62,9 @@ namespace sat { bool process(clause & c); - bool process2(scc& scc, clause & c); + bool process_sampled(scc& scc, clause & c); - void process(clause_vector & c); + void process(scc& scc, clause_vector & c); bool process_all(clause & c); @@ -72,8 +74,6 @@ namespace sat { bool propagate_literal(clause const& c, literal l); - void setup_big(); - public: asymm_branch(solver & s, params_ref const & p); diff --git a/src/sat/sat_asymm_branch_params.pyg b/src/sat/sat_asymm_branch_params.pyg index bc50804ba..a457220be 100644 --- a/src/sat/sat_asymm_branch_params.pyg +++ b/src/sat/sat_asymm_branch_params.pyg @@ -2,5 +2,7 @@ def_module_params(module_name='sat', class_name='sat_asymm_branch_params', export=True, params=(('asymm_branch', BOOL, True, 'asymmetric branching'), + ('asymm_branch.delay', UINT, 1, 'number of simplification rounds to wait until invoking asymmetric branch simplification'), + ('asymm_branch.sampled', BOOL, False, 'use sampling based asymmetric branching based on binary implication graph'), ('asymm_branch.limit', UINT, 100000000, 'approx. maximum number of literals visited during asymmetric branching'), ('asymm_branch.all', BOOL, False, 'asymmetric branching on all literals per clause'))) diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 306912b57..7464c4156 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -20,6 +20,7 @@ Notes: #include "sat/sat_solver.h" #include "sat/sat_extension.h" #include "sat/sat_lookahead.h" +#include "sat/sat_scc.h" #include "util/union_find.h" namespace sat { @@ -2304,15 +2305,86 @@ namespace sat { void lookahead::add_hyper_binary() { + unsigned num_lits = m_s.num_vars() * 2; + +#if 0 std::cout << "binary trail size: " << m_binary_trail.size() << "\n"; std::cout << "Are windfalls still on the trail at base level?\n"; - unsigned num_lits = m_s.num_vars() * 2; +#endif + + unsigned disconnected1 = 0; + unsigned disconnected2 = 0; + +#if 1 + typedef std::pair u_pair; + hashtable, default_eq > imp; + for (unsigned idx = 0; idx < num_lits; ++idx) { + literal u = get_parent(to_literal(idx)); + if (null_literal != u) { + for (watched const& w : m_s.m_watches[idx]) { + if (!w.is_binary_clause()) continue; + literal v = get_parent(w.get_literal()); + if (null_literal != v) { + imp.insert(std::make_pair(u.index(), v.index())); + } + } + } + } + + scc scc(m_s, m_s.m_params); + scc.init_big(true); + svector> candidates; + unsigned_vector bin_size(num_lits); for (unsigned idx : m_binary_trail) { bin_size[idx]++; } - + for (unsigned idx = 0; idx < num_lits; ++idx) { + literal u = to_literal(idx); + if (u != get_parent(u)) continue; + if (m_s.was_eliminated(u.var())) continue; + literal_vector const& lits = m_binary[idx]; + for (unsigned sz = bin_size[idx]; sz > 0; --sz) { + literal v = lits[lits.size() - sz]; + if (v != get_parent(v)) continue; + if (m_s.was_eliminated(v.var())) continue; + if (imp.contains(std::make_pair(u.index(), v.index()))) continue; + if (scc.reaches(u, v)) continue; + candidates.push_back(std::make_pair(u, v)); + } + } + for (unsigned i = 0; i < 5; ++i) { + scc.init_big(true); + unsigned k = 0; + union_find_default_ctx ufctx; + union_find uf(ufctx); + for (unsigned i = 0; i < num_lits; ++i) uf.mk_var(); + for (unsigned j = 0; j < candidates.size(); ++j) { + literal u = candidates[j].first; + literal v = candidates[j].second; + if (!scc.reaches(u, v)) { + if (uf.find(u.index()) != uf.find(v.index())) { + ++disconnected1; + uf.merge(u.index(), v.index()); + uf.merge((~u).index(), (~v).index()); + m_s.mk_clause(~u, v, true); + } + else { + candidates[k] = candidates[j]; + ++k; + } + } + } + std::cout << candidates.size() << " -> " << k << "\n"; + if (k == candidates.size()) break; + candidates.shrink(k); + } + std::cout << "candidates: " << candidates.size() << "\n"; + +#endif + +#if 0 union_find_default_ctx ufctx; union_find uf(ufctx); for (unsigned i = 0; i < num_lits; ++i) uf.mk_var(); @@ -2329,21 +2401,25 @@ namespace sat { } } - unsigned disconnected = 0; for (unsigned i = 0; i < m_binary.size(); ++i) { literal u = to_literal(i); - if (u == get_parent(u)) { + if (u == get_parent(u) && !m_s.was_eliminated(u.var())) { for (literal v : m_binary[i]) { - if (v == get_parent(v) && uf.find(u.index()) != uf.find(v.index())) { - ++disconnected; + if (v == get_parent(v) && + !m_s.was_eliminated(v.var()) && + uf.find(u.index()) != uf.find(v.index())) { + ++disconnected2; uf.merge(u.index(), v.index()); - m_s.mk_clause(~u, v, true); + // m_s.mk_clause(~u, v, true); } } } } - IF_VERBOSE(10, verbose_stream() << "(sat-lookahead :bca " << disconnected << ")\n";); - m_stats.m_bca += disconnected; +#endif + + IF_VERBOSE(10, verbose_stream() << "(sat-lookahead :bca " << disconnected1 << " " << disconnected2 << ")\n";); + //IF_VERBOSE(10, verbose_stream() << "(sat-lookahead :bca " << disconnected << ")\n";); + //m_stats.m_bca += disconnected; } void lookahead::normalize_parents() { diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp index 9da54da29..7615a19a3 100644 --- a/src/sat/sat_scc.cpp +++ b/src/sat/sat_scc.cpp @@ -234,17 +234,7 @@ namespace sat { return to_elim.size(); } - // shuffle vertices to obtain different DAG traversal each time - void scc::shuffle(literal_vector& lits) { - unsigned sz = lits.size(); - if (sz > 1) { - for (unsigned i = sz; i-- > 0; ) { - std::swap(lits[i], lits[m_rand(i+1)]); - } - } - } - - vector const& scc::get_big(bool learned) { + void scc::init_big(bool learned) { unsigned num_lits = m_solver.num_vars() * 2; m_dag.reset(); m_roots.reset(); @@ -263,53 +253,21 @@ namespace sat { edges.push_back(v); } } - shuffle(edges); + shuffle(edges.size(), edges.c_ptr(), m_rand); } - return m_dag; + init_dfs_num(learned); } - void scc::get_dfs_num(bool learned) { - unsigned num_lits = m_solver.num_vars() * 2; - SASSERT(m_left.size() == num_lits); - SASSERT(m_right.size() == num_lits); - literal_vector todo; - // retrieve literals that have no predecessors - for (unsigned l_idx = 0; l_idx < num_lits; l_idx++) { - literal u(to_literal(l_idx)); - if (m_roots[u.index()]) todo.push_back(u); - } - shuffle(todo); - int dfs_num = 0; - while (!todo.empty()) { - literal u = todo.back(); - int& d = m_left[u.index()]; - // already visited - if (d > 0) { - if (m_right[u.index()] < 0) { - m_right[u.index()] = dfs_num; - } - todo.pop_back(); - } - // visited as child: - else if (d < 0) { - d = -d; - for (literal v : m_dag[u.index()]) { - if (m_left[v.index()] == 0) { - m_left[v.index()] = - d - 1; - m_root[v.index()] = m_root[u.index()]; - m_parent[v.index()] = u; - todo.push_back(v); - } - } - } - // new root. - else { - d = --dfs_num; - } - } - } + struct scc::pframe { + literal m_parent; + literal m_child; + pframe(literal p, literal c): + m_parent(p), m_child(c) {} + literal child() const { return m_child; } + literal parent() const { return m_parent; } + }; - unsigned scc::reduce_tr(bool learned) { + void scc::init_dfs_num(bool learned) { unsigned num_lits = m_solver.num_vars() * 2; m_left.reset(); m_right.reset(); @@ -317,11 +275,61 @@ namespace sat { m_parent.reset(); m_left.resize(num_lits, 0); m_right.resize(num_lits, -1); + m_root.resize(num_lits, null_literal); + m_parent.resize(num_lits, null_literal); for (unsigned i = 0; i < num_lits; ++i) { m_root[i] = to_literal(i); m_parent[i] = to_literal(i); } - get_dfs_num(learned); + svector todo; + // retrieve literals that have no predecessors + for (unsigned l_idx = 0; l_idx < num_lits; l_idx++) { + literal u(to_literal(l_idx)); + if (m_roots[u.index()]) { + todo.push_back(pframe(null_literal, u)); + } + } + shuffle(todo.size(), todo.c_ptr(), m_rand); + int dfs_num = 0; + while (!todo.empty()) { + literal u = todo.back().child(); + if (m_left[u.index()] > 0) { + // already visited + if (m_right[u.index()] < 0) { + m_right[u.index()] = ++dfs_num; + } + todo.pop_back(); + } + else { + SASSERT(m_left[u.index()] == 0); + m_left[u.index()] = ++dfs_num; + for (literal v : m_dag[u.index()]) { + if (m_left[v.index()] == 0) { + todo.push_back(pframe(u, v)); + } + } + literal p = todo.back().parent(); + if (p != null_literal) { + m_root[u.index()] = m_root[p.index()]; + m_parent[u.index()] = p; + } + } + } + for (unsigned i = 0; i < num_lits; ++i) { + if (m_right[i] < 0) { + VERIFY(m_left[i] == 0); + m_left[i] = ++dfs_num; + m_right[i] = ++dfs_num; + } + } + for (unsigned i = 0; i < num_lits; ++i) { + VERIFY(m_left[i] < m_right[i]); + } + } + + unsigned scc::reduce_tr(bool learned) { + unsigned num_lits = m_solver.num_vars() * 2; + init_big(learned); unsigned idx = 0; unsigned elim = m_num_elim_bin; for (watch_list & wlist : m_solver.m_watches) { @@ -333,7 +341,7 @@ namespace sat { watched& w = *it; if (learned ? w.is_binary_learned_clause() : w.is_binary_unblocked_clause()) { literal v = w.get_literal(); - if (m_left[u.index()] + 1 < m_left[v.index()]) { + if (reaches(u, v) && u != get_parent(v)) { ++m_num_elim_bin; } else { diff --git a/src/sat/sat_scc.h b/src/sat/sat_scc.h index 806cf8f33..2973245a3 100644 --- a/src/sat/sat_scc.h +++ b/src/sat/sat_scc.h @@ -44,10 +44,13 @@ namespace sat { svector m_left, m_right; literal_vector m_root, m_parent; - void shuffle(literal_vector& lits); void reduce_tr(); unsigned reduce_tr(bool learned); + void init_dfs_num(bool learned); + + struct pframe; + public: scc(solver & s, params_ref const & p); @@ -60,17 +63,14 @@ namespace sat { void reset_statistics(); /* - \brief retrieve binary implication graph + \brief create binary implication graph and associated data-structures to check transitivity. */ - vector const& get_big(bool learned); - + void init_big(bool learned); int get_left(literal l) const { return m_left[l.index()]; } int get_right(literal l) const { return m_right[l.index()]; } literal get_parent(literal l) const { return m_parent[l.index()]; } literal get_root(literal l) const { return m_root[l.index()]; } - - void get_dfs_num(bool learned); - + bool reaches(literal u, literal v) const { return m_left[u.index()] < m_left[v.index()] && m_right[v.index()] < m_right[u.index()]; } }; }; diff --git a/src/sat/sat_simplifier_params.pyg b/src/sat/sat_simplifier_params.pyg index b78980774..32d318536 100644 --- a/src/sat/sat_simplifier_params.pyg +++ b/src/sat/sat_simplifier_params.pyg @@ -2,7 +2,7 @@ def_module_params(module_name='sat', class_name='sat_simplifier_params', export=True, params=(('elim_blocked_clauses', BOOL, False, 'eliminate blocked clauses'), - ('abce', BOOL, BOOL, False, 'eliminate blocked clauses using asymmmetric literals'), + ('abce', BOOL, False, 'eliminate blocked clauses using asymmmetric literals'), ('cce', BOOL, False, 'eliminate covered clauses'), ('acce', BOOL, False, 'eliminate covered clauses using asymmetric added literals'), ('elim_blocked_clauses_at', UINT, 2, 'eliminate blocked clauses only once at the given simplification round'), diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 7cadffd27..602850487 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -191,7 +191,7 @@ namespace sat { // Misc // // ----------------------- - void updt_params(params_ref const & p); + void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); void collect_statistics(statistics & st) const;