From f3b0ede6e833c124034a2b2e43006732f40bc46d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 7 Jun 2017 16:35:35 -0700 Subject: [PATCH] update lookahead to include extensions Signed-off-by: Nikolaj Bjorner --- contrib/cmake/src/sat/CMakeLists.txt | 1 + src/api/api_interp.cpp | 28 +- src/api/dotnet/InterpolationContext.cs | 17 +- src/api/z3_interp.h | 11 +- src/cmd_context/basic_cmds.cpp | 2 +- src/sat/card_extension.cpp | 442 ++----- src/sat/card_extension.h | 89 +- src/sat/sat_extension.h | 1 + src/sat/sat_lookahead.cpp | 1597 +++++++++++++++++++++++ src/sat/sat_lookahead.h | 1600 ++---------------------- src/sat/sat_solver.cpp | 8 +- src/sat/sat_types.h | 1 + src/sat/sat_watched.h | 2 +- 13 files changed, 1855 insertions(+), 1944 deletions(-) create mode 100644 src/sat/sat_lookahead.cpp diff --git a/contrib/cmake/src/sat/CMakeLists.txt b/contrib/cmake/src/sat/CMakeLists.txt index fcfe53e02..0f9b9c20c 100644 --- a/contrib/cmake/src/sat/CMakeLists.txt +++ b/contrib/cmake/src/sat/CMakeLists.txt @@ -14,6 +14,7 @@ z3_add_component(sat sat_iff3_finder.cpp sat_integrity_checker.cpp sat_local_search.cpp + sat_lookahead.cpp sat_model_converter.cpp sat_mus.cpp sat_parallel.cpp diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index a1fa8f137..05921cc91 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -542,14 +542,15 @@ extern "C" { } - int Z3_read_interpolation_problem(Z3_context ctx, unsigned *_num, Z3_ast *cnsts[], unsigned *parents[], const char *filename, Z3_string_ptr error, unsigned *ret_num_theory, Z3_ast *theory[]){ + int Z3_read_interpolation_problem(Z3_context ctx, Z3_ast_vector cnsts, unsigned* _num, unsigned* parents[], const char *filename, Z3_string_ptr error, Z3_ast_vector theory){ hash_map file_params; get_file_params(filename, file_params); unsigned num_theory = 0; - if (file_params.find("THEORY") != file_params.end()) + if (file_params.find("THEORY") != file_params.end()) { num_theory = atoi(file_params["THEORY"].c_str()); + } Z3_ast_vector assertions = iZ3_parse(ctx, filename, error); if (assertions == 0) @@ -559,23 +560,15 @@ extern "C" { num_theory = Z3_ast_vector_size(ctx, assertions); unsigned num = Z3_ast_vector_size(ctx, assertions) - num_theory; - read_cnsts.resize(num); read_parents.resize(num); - read_theory.resize(num_theory); - for (unsigned j = 0; j < num_theory; j++) - read_theory[j] = Z3_ast_vector_get(ctx, assertions, j); - for (unsigned j = 0; j < num; j++) - read_cnsts[j] = Z3_ast_vector_get(ctx, assertions, j + num_theory); + for (unsigned j = 0; theory && j < num_theory; j++) + Z3_ast_vector_push(ctx, theory, Z3_ast_vector_get(ctx, assertions, j)); + + for (unsigned j = 0; j < num; j++) + Z3_ast_vector_push(ctx, cnsts, Z3_ast_vector_get(ctx, assertions, j + num_theory)); - if (ret_num_theory) - *ret_num_theory = num_theory; - if (theory) - *theory = &read_theory[0]; - if (!parents){ - *_num = num; - *cnsts = &read_cnsts[0]; Z3_ast_vector_dec_ref(ctx, assertions); return true; } @@ -586,7 +579,7 @@ extern "C" { hash_map pred_map; for (unsigned j = 0; j < num; j++){ - Z3_ast lhs = 0, rhs = read_cnsts[j]; + Z3_ast lhs = 0, rhs = Z3_ast_vector_get(ctx, cnsts, j); if (Z3_get_decl_kind(ctx, Z3_get_app_decl(ctx, Z3_to_app(ctx, rhs))) == Z3_OP_IMPLIES){ Z3_app app1 = Z3_to_app(ctx, rhs); @@ -627,7 +620,7 @@ extern "C" { read_error << "formula " << j + 1 << ": should be (implies {children} fmla parent)"; goto fail; } - read_cnsts[j] = lhs; + Z3_ast_vector_set(ctx, cnsts, j, lhs); Z3_ast name = rhs; if (pred_map.find(name) != pred_map.end()){ read_error << "formula " << j + 1 << ": duplicate symbol"; @@ -646,7 +639,6 @@ extern "C" { } *_num = num; - *cnsts = &read_cnsts[0]; *parents = &read_parents[0]; Z3_ast_vector_dec_ref(ctx, assertions); return true; diff --git a/src/api/dotnet/InterpolationContext.cs b/src/api/dotnet/InterpolationContext.cs index 3f2feb5a6..e2b814983 100644 --- a/src/api/dotnet/InterpolationContext.cs +++ b/src/api/dotnet/InterpolationContext.cs @@ -133,19 +133,16 @@ namespace Microsoft.Z3 /// well documented. public int ReadInterpolationProblem(string filename, out Expr[] cnsts, out uint[] parents, out string error, out Expr[] theory) { - uint num = 0, num_theory = 0; - IntPtr[] n_cnsts; - IntPtr[] n_theory; + uint num = 0; IntPtr n_err_str; - int r = Native.Z3_read_interpolation_problem(nCtx, ref num, out n_cnsts, out parents, filename, out n_err_str, ref num_theory, out n_theory); + ASTVector _cnsts = new ASTVector(this); + ASTVector _theory = new ASTVector(this); + + int r = Native.Z3_read_interpolation_problem(nCtx, _cnsts.NativeObject, ref num, out parents, filename, out n_err_str, _theory.NativeObject); error = Marshal.PtrToStringAnsi(n_err_str); - cnsts = new Expr[num]; + cnsts = _cnsts.ToExprArray(); parents = new uint[num]; - theory = new Expr[num_theory]; - for (int i = 0; i < num; i++) - cnsts[i] = Expr.Create(this, n_cnsts[i]); - for (int i = 0; i < num_theory; i++) - theory[i] = Expr.Create(this, n_theory[i]); + theory = _theory.ToExprArray(); return r; } diff --git a/src/api/z3_interp.h b/src/api/z3_interp.h index bcee0e22d..7646695f8 100644 --- a/src/api/z3_interp.h +++ b/src/api/z3_interp.h @@ -207,18 +207,17 @@ extern "C" { where each value is represented using the common symbols between the formulas in the subtree and the remainder of the formulas. - def_API('Z3_read_interpolation_problem', INT, (_in(CONTEXT), _out(UINT), _out_managed_array(1, AST), _out_managed_array(1, UINT), _in(STRING), _out(STRING), _out(UINT), _out_managed_array(6, AST))) + def_API('Z3_read_interpolation_problem', INT, (_in(CONTEXT), _in(AST_VECTOR), _out(UINT), _out_managed_array(2, UINT), _in(STRING), _out(STRING), _in(AST_VECTOR))) */ int Z3_API Z3_read_interpolation_problem(Z3_context ctx, - unsigned *num, - Z3_ast *cnsts[], - unsigned *parents[], + Z3_ast_vector cnsts, + unsigned* num, + unsigned* parents[], Z3_string filename, Z3_string_ptr error, - unsigned *num_theory, - Z3_ast *theory[]); + Z3_ast_vector theory); diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 26cd0628e..6d6217b50 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -266,7 +266,7 @@ UNARY_CMD(pp_cmd, "display", "", "display the given term.", CPK_EXPR, expr ctx.regular_stream() << std::endl; }); -UNARY_CMD(echo_cmd, "echo", "", "display the given string", CPK_STRING, char const *, ctx.regular_stream() << arg << std::endl;); +UNARY_CMD(echo_cmd, "echo", "", "display the given string", CPK_STRING, char const *, ctx.regular_stream() << "\"" << arg << "\"" << std::endl;); class set_get_option_cmd : public cmd { diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp index 5032da6ff..0e3a24f56 100644 --- a/src/sat/card_extension.cpp +++ b/src/sat/card_extension.cpp @@ -79,12 +79,6 @@ namespace sat { } } - void card_extension::init_watch(bool_var v) { - if (m_var_infos.size() <= static_cast(v)) { - m_var_infos.resize(static_cast(v)+100); - } - } - void card_extension::init_watch(card& c, bool is_true) { clear_watch(c); if (c.lit() != null_literal && c.lit().sign() == is_true) { @@ -94,7 +88,7 @@ namespace sat { SASSERT(c.lit() == null_literal || value(c.lit()) == l_true); unsigned j = 0, sz = c.size(), bound = c.k(); if (bound == sz) { - for (unsigned i = 0; i < sz && !s().inconsistent(); ++i) { + for (unsigned i = 0; i < sz && !inconsistent(); ++i) { assign(c, c[i]); } return; @@ -135,7 +129,7 @@ namespace sat { set_conflict(c, alit); } else if (j == bound) { - for (unsigned i = 0; i < bound && !s().inconsistent(); ++i) { + for (unsigned i = 0; i < bound && !inconsistent(); ++i) { assign(c, c[i]); } } @@ -149,20 +143,12 @@ namespace sat { void card_extension::clear_watch(card& c) { unsigned sz = std::min(c.k() + 1, c.size()); for (unsigned i = 0; i < sz; ++i) { - unwatch_literal(c[i], &c); + unwatch_literal(c[i], c); } } - void card_extension::unwatch_literal(literal lit, card* c) { - if (m_var_infos.size() <= static_cast(lit.var())) { - return; - } - ptr_vector*& cards = m_var_infos[lit.var()].m_card_watch[lit.sign()]; - if (!is_tag_empty(cards)) { - if (remove(*cards, c)) { - cards = set_tag_empty(cards); - } - } + void card_extension::unwatch_literal(literal lit, card& c) { + get_wlist(~lit).erase(watched(c.index())); } void card_extension::assign(card& c, literal lit) { @@ -177,7 +163,7 @@ namespace sat { m_num_propagations_since_pop++; //TRACE("sat", tout << "#prop: " << m_stats.m_num_propagations << " - " << c.lit() << " => " << lit << "\n";); SASSERT(validate_unit_propagation(c)); - if (s().m_config.m_drat) { + if (get_config().m_drat) { svector ps; literal_vector lits; if (c.lit() != null_literal) lits.push_back(~c.lit()); @@ -186,27 +172,16 @@ namespace sat { } lits.push_back(lit); ps.push_back(drat::premise(drat::s_ext(), c.lit())); // null_literal case. - s().m_drat.add(lits, ps); + drat_add(lits, ps); } - s().assign(lit, justification::mk_ext_justification(c.index())); + assign(lit, justification::mk_ext_justification(c.index())); break; } } void card_extension::watch_literal(card& c, literal lit) { TRACE("sat_verbose", tout << "watch: " << lit << "\n";); - init_watch(lit.var()); - ptr_vector* cards = m_var_infos[lit.var()].m_card_watch[lit.sign()]; - if (cards == 0) { - cards = alloc(ptr_vector); - m_var_infos[lit.var()].m_card_watch[lit.sign()] = cards; - } - else if (is_tag_empty(cards)) { - cards = set_tag_non_empty(cards); - m_var_infos[lit.var()].m_card_watch[lit.sign()] = cards; - } - TRACE("sat_verbose", tout << "insert: " << lit.var() << " " << lit.sign() << "\n";); - cards->push_back(&c); + get_wlist(~lit).push_back(watched(c.index())); } void card_extension::set_conflict(card& c, literal lit) { @@ -214,8 +189,8 @@ namespace sat { TRACE("sat", display(tout, c, true); ); SASSERT(validate_conflict(c)); SASSERT(value(lit) == l_false); - s().set_conflict(justification::mk_ext_justification(c.index()), ~lit); - SASSERT(s().inconsistent()); + set_conflict(justification::mk_ext_justification(c.index()), ~lit); + SASSERT(inconsistent()); } // pb: @@ -322,7 +297,7 @@ namespace sat { lbool card_extension::add_assign(pb& p, literal alit) { TRACE("sat", display(tout << "assign: " << alit << "\n", p, true);); - SASSERT(!s().inconsistent()); + SASSERT(!inconsistent()); unsigned sz = p.size(); unsigned bound = p.k(); unsigned num_watch = p.num_watch(); @@ -332,7 +307,7 @@ namespace sat { SASSERT(num_watch <= sz); SASSERT(num_watch > 0); unsigned index = 0; - m_a_max = 0; + m_a_max = 0; m_pb_undef.reset(); for (; index < num_watch; ++index) { literal lit = p[index].second; @@ -364,7 +339,7 @@ namespace sat { } } - SASSERT(!s().inconsistent()); + SASSERT(!inconsistent()); DEBUG_CODE(for (auto idx : m_pb_undef) { SASSERT(value(p[idx].second) == l_undef); }); if (slack < bound) { @@ -400,7 +375,7 @@ namespace sat { } for (literal lit : to_assign) { - if (s().inconsistent()) break; + if (inconsistent()) break; if (value(lit) == l_undef) { assign(p, lit); } @@ -415,37 +390,18 @@ namespace sat { void card_extension::watch_literal(pb& p, wliteral l) { literal lit = l.second; - init_watch(lit.var()); - ptr_vector* pbs = m_var_infos[lit.var()].m_pb_watch[lit.sign()]; - if (pbs == 0) { - pbs = alloc(ptr_vector); - m_var_infos[lit.var()].m_pb_watch[lit.sign()] = pbs; - } - else if (is_tag_empty(pbs)) { - pbs = set_tag_non_empty(pbs); - m_var_infos[lit.var()].m_pb_watch[lit.sign()] = pbs; - } - TRACE("sat_verbose", tout << "insert: " << lit.var() << " " << lit.sign() << "\n";); - pbs->push_back(&p); + get_wlist(~lit).push_back(watched(p.index())); } void card_extension::clear_watch(pb& p) { unsigned sz = p.size(); for (unsigned i = 0; i < sz; ++i) { - unwatch_literal(p[i].second, &p); + unwatch_literal(p[i].second, p); } } - void card_extension::unwatch_literal(literal lit, pb* p) { - if (m_var_infos.size() <= static_cast(lit.var())) { - return; - } - pb_watch*& pbs = m_var_infos[lit.var()].m_pb_watch[lit.sign()]; - if (!is_tag_empty(pbs)) { - if (remove(*pbs, p)) { - pbs = set_tag_empty(pbs); - } - } + void card_extension::unwatch_literal(literal lit, pb& p) { + get_wlist(~lit).erase(watched(p.index())); } void card_extension::set_conflict(pb& p, literal lit) { @@ -453,8 +409,8 @@ namespace sat { TRACE("sat", display(tout, p, true); ); // SASSERT(validate_conflict(p)); SASSERT(value(lit) == l_false); - s().set_conflict(justification::mk_ext_justification(p.index()), ~lit); - SASSERT(s().inconsistent()); + set_conflict(justification::mk_ext_justification(p.index()), ~lit); + SASSERT(inconsistent()); } void card_extension::assign(pb& p, literal lit) { @@ -468,15 +424,15 @@ namespace sat { SASSERT(validate_unit_propagation(p, lit)); m_stats.m_num_pb_propagations++; m_num_propagations_since_pop++; - if (s().m_config.m_drat) { + if (get_config().m_drat) { svector ps; literal_vector lits; get_pb_antecedents(lit, p, lits); lits.push_back(lit); ps.push_back(drat::premise(drat::s_ext(), p.lit())); - s().m_drat.add(lits, ps); + drat_add(lits, ps); } - s().assign(lit, justification::mk_ext_justification(p.index())); + assign(lit, justification::mk_ext_justification(p.index())); break; } } @@ -513,53 +469,6 @@ namespace sat { out << ">= " << p.k() << "\n"; } - void card_extension::asserted_pb(literal l, ptr_vector* pbs, pb* p0) { - TRACE("sat", tout << "literal: " << l << " has pb: " << !is_tag_empty(pbs) << " p0 != 0: " << (p0 != 0) << "\n";); - if (!is_tag_empty(pbs)) { - ptr_vector::iterator begin = pbs->begin(); - ptr_vector::iterator it = begin, it2 = it, end = pbs->end(); - for (; it != end; ++it) { - pb& p = *(*it); - if (p.lit() != null_literal && value(p.lit()) != l_true) { - continue; - } - switch (add_assign(p, ~l)) { - case l_true: // unit propagation, keep watching the literal - if (it2 != it) { - *it2 = *it; - } - ++it2; - break; - case l_false: // conflict. - SASSERT(s().inconsistent()); - for (; it != end; ++it, ++it2) { - *it2 = *it; - } - pbs->set_end(it2); - return; - case l_undef: // watch literal was swapped - if (s().inconsistent()) { - ++it; - for (; it != end; ++it, ++it2) { - *it2 = *it; - } - pbs->set_end(it2); - return; - } - break; - } - } - pbs->set_end(it2); - if (pbs->empty()) { - m_var_infos[l.var()].m_pb_watch[!l.sign()] = set_tag_empty(pbs); - } - } - - if (p0 != 0 && !s().inconsistent()) { - init_watch(*p0, !l.sign()); - } - } - // xor: void card_extension::copy_xor(card_extension& result) { @@ -575,20 +484,12 @@ namespace sat { } void card_extension::clear_watch(xor& x) { - unwatch_literal(x[0], &x); - unwatch_literal(x[1], &x); + unwatch_literal(x[0], x); + unwatch_literal(x[1], x); } - void card_extension::unwatch_literal(literal lit, xor* c) { - if (m_var_infos.size() <= static_cast(lit.var())) { - return; - } - xor_watch*& xors = m_var_infos[lit.var()].m_xor_watch; - if (!is_tag_empty(xors)) { - if (remove(*xors, c)) { - xors = set_tag_empty(xors); - } - } + void card_extension::unwatch_literal(literal lit, xor& c) { + get_wlist(~lit).erase(watched(c.index())); } bool card_extension::parity(xor const& x, unsigned offset) const { @@ -620,16 +521,15 @@ namespace sat { switch (j) { case 0: if (!parity(x, 0)) { - literal_set litset; - for (unsigned i = 0; i < sz; ++i) { - litset.insert(x[i]); + unsigned l = lvl(x[0]); + j = 1; + for (unsigned i = 1; i < sz; ++i) { + if (lvl(x[i]) > l) { + j = i; + l = lvl(x[i]); + } } - literal_vector const& lits = s().m_trail; - unsigned idx = lits.size()-1; - while (!litset.contains(lits[idx])) { - --idx; - } - set_conflict(x, lits[idx]); + set_conflict(x, x[j]); } break; case 1: @@ -644,18 +544,18 @@ namespace sat { } void card_extension::assign(xor& x, literal lit) { - SASSERT(!s().inconsistent()); + SASSERT(!inconsistent()); switch (value(lit)) { case l_true: break; case l_false: set_conflict(x, lit); - SASSERT(s().inconsistent()); + SASSERT(inconsistent()); break; default: m_stats.m_num_xor_propagations++; m_num_propagations_since_pop++; - if (s().m_config.m_drat) { + if (get_config().m_drat) { svector ps; literal_vector lits; if (x.lit() != null_literal) lits.push_back(~x.lit()); @@ -664,25 +564,17 @@ namespace sat { } lits.push_back(lit); ps.push_back(drat::premise(drat::s_ext(), x.lit())); - s().m_drat.add(lits, ps); + drat_add(lits, ps); } TRACE("sat", display(tout << lit << " ", x, true);); - s().assign(lit, justification::mk_ext_justification(x.index())); + assign(lit, justification::mk_ext_justification(x.index())); break; } } void card_extension::watch_literal(xor& x, literal lit) { TRACE("sat_verbose", tout << "watch: " << lit << "\n";); - init_watch(lit.var()); - xor_watch*& xors = m_var_infos[lit.var()].m_xor_watch; - if (xors == 0) { - xors = alloc(ptr_vector); - } - else if (is_tag_empty(xors)) { - xors = set_tag_non_empty(xors); - } - xors->push_back(&x); + get_wlist(~lit).push_back(watched(x.index())); TRACE("sat_verbose", tout << "insert: " << lit.var() << " " << lit.sign() << "\n";); } @@ -693,8 +585,8 @@ namespace sat { if (value(lit) == l_true) lit.neg(); SASSERT(validate_conflict(x)); TRACE("sat", display(tout << lit << " ", x, true);); - s().set_conflict(justification::mk_ext_justification(x.index()), ~lit); - SASSERT(s().inconsistent()); + set_conflict(justification::mk_ext_justification(x.index()), ~lit); + SASSERT(inconsistent()); } lbool card_extension::add_assign(xor& x, literal alit) { @@ -735,48 +627,8 @@ namespace sat { else if (!parity(x, 0)) { set_conflict(x, ~x[1]); } - return s().inconsistent() ? l_false : l_true; + return inconsistent() ? l_false : l_true; } - - void card_extension::asserted_xor(literal l, ptr_vector* xors, xor* x) { - TRACE("sat", tout << l << " " << !is_tag_empty(xors) << " " << (x != 0) << "\n";); - if (!is_tag_empty(xors)) { - ptr_vector::iterator begin = xors->begin(); - ptr_vector::iterator it = begin, it2 = it, end = xors->end(); - for (; it != end; ++it) { - xor& c = *(*it); - if (c.lit() != null_literal && value(c.lit()) != l_true) { - continue; - } - switch (add_assign(c, ~l)) { - case l_false: // conflict - for (; it != end; ++it, ++it2) { - *it2 = *it; - } - SASSERT(s().inconsistent()); - xors->set_end(it2); - return; - case l_undef: // watch literal was swapped - break; - case l_true: // unit propagation, keep watching the literal - if (it2 != it) { - *it2 = *it; - } - ++it2; - break; - } - } - xors->set_end(it2); - if (xors->empty()) { - m_var_infos[l.var()].m_xor_watch = set_tag_empty(xors); - } - } - - if (x != 0 && !s().inconsistent()) { - init_watch(*x, !l.sign()); - } - } - void card_extension::normalize_active_coeffs() { while (!m_active_var_set.empty()) m_active_var_set.erase(); @@ -841,7 +693,6 @@ namespace sat { m_active_vars.reset(); } - bool card_extension::resolve_conflict() { if (0 == m_num_propagations_since_pop) { return false; @@ -1084,9 +935,9 @@ namespace sat { TRACE("sat", tout << m_lemma << "\n";); - if (s().m_config.m_drat) { + if (get_config().m_drat) { svector ps; // TBD fill in - s().m_drat.add(m_lemma, ps); + drat_add(m_lemma, ps); } s().m_lemma.reset(); @@ -1155,16 +1006,11 @@ namespace sat { return p; } - card_extension::card_extension(): m_solver(0), m_has_xor(false) { + card_extension::card_extension(): m_solver(0), m_lookahead(0) { TRACE("sat", tout << this << "\n";); } card_extension::~card_extension() { - for (unsigned i = 0; i < m_var_infos.size(); ++i) { - m_var_infos[i].reset(); - } - m_var_trail.reset(); - m_var_lim.reset(); m_stats.reset(); } @@ -1180,9 +1026,9 @@ namespace sat { m_card_axioms.push_back(c); } else { - init_watch(v); - m_var_infos[v].m_card = c; - m_var_trail.push_back(v); + get_wlist(literal(v, false)).push_back(index); + get_wlist(literal(v, true)).push_back(index); + m_index_trail.push_back(index); } } @@ -1197,27 +1043,57 @@ namespace sat { m_pb_axioms.push_back(p); } else { - init_watch(v); - m_var_infos[v].m_pb = p; - m_var_trail.push_back(v); + get_wlist(literal(v, false)).push_back(index); + get_wlist(literal(v, true)).push_back(index); + m_index_trail.push_back(index); } } void card_extension::add_xor(bool_var v, literal_vector const& lits) { - m_has_xor = true; unsigned index = 4*m_xors.size() + 0x1; SASSERT(is_xor_index(index)); + SASSERT(v != null_bool_var); xor* x = new (memory::allocate(xor::get_obj_size(lits.size()))) xor(index, literal(v, false), lits); m_xors.push_back(x); - init_watch(v); - m_var_infos[v].m_xor = x; - m_var_trail.push_back(v); + get_wlist(literal(v, false)).push_back(index); + get_wlist(literal(v, true)).push_back(index); + m_index_trail.push_back(index); } void card_extension::propagate(literal l, ext_constraint_idx idx, bool & keep) { - UNREACHABLE(); + TRACE("sat", tout << l << " " << idx << "\n";); + if (is_pb_index(idx)) { + pb& p = index2pb(idx); + if (l.var() == p.lit().var()) { + init_watch(p, !l.sign()); + } + else { + keep = l_undef != add_assign(p, ~l); + } + } + else if (is_card_index(idx)) { + card& c = index2card(idx); + if (l.var() == c.lit().var()) { + init_watch(c, !l.sign()); + } + else { + keep = l_undef != add_assign(c, ~l); + } + } + else if (is_xor_index(idx)) { + xor& x = index2xor(idx); + if (l.var() == x.lit().var()) { + init_watch(x, !l.sign()); + } + else { + keep = l_undef != add_assign(x, ~l); + } + } + else { + UNREACHABLE(); + } } @@ -1454,100 +1330,53 @@ namespace sat { } SASSERT(validate_unit_propagation(c)); - for (unsigned i = 0; i < bound && !s().inconsistent(); ++i) { + for (unsigned i = 0; i < bound && !inconsistent(); ++i) { assign(c, c[i]); } - return s().inconsistent() ? l_false : l_true; + return inconsistent() ? l_false : l_true; } void card_extension::asserted(literal l) { - bool_var v = l.var(); - if (s().inconsistent()) return; - if (v >= m_var_infos.size()) return; - var_info& vinfo = m_var_infos[v]; - ptr_vector* cards = vinfo.m_card_watch[!l.sign()]; - ptr_vector* xors = vinfo.m_xor_watch; - ptr_vector* pbs = vinfo.m_pb_watch[!l.sign()]; - pb* p = vinfo.m_pb; - card* crd = vinfo.m_card; - xor* x = vinfo.m_xor; - - if (!is_tag_empty(cards)) { - ptr_vector::iterator begin = cards->begin(); - ptr_vector::iterator it = begin, it2 = it, end = cards->end(); - for (; it != end; ++it) { - card& c = *(*it); - if (c.lit() != null_literal && value(c.lit()) != l_true) { - continue; - } - switch (add_assign(c, ~l)) { - case l_false: // conflict - for (; it != end; ++it, ++it2) { - *it2 = *it; - } - SASSERT(s().inconsistent()); - cards->set_end(it2); - return; - case l_undef: // watch literal was swapped - break; - case l_true: // unit propagation, keep watching the literal - if (it2 != it) { - *it2 = *it; - } - ++it2; - break; - } - } - cards->set_end(it2); - if (cards->empty()) { - m_var_infos[v].m_card_watch[!l.sign()] = set_tag_empty(cards); - } - } - - if (crd != 0 && !s().inconsistent()) { - init_watch(*crd, !l.sign()); - } - - if ((!is_tag_empty(pbs) || p) && !s().inconsistent()) { - asserted_pb(l, pbs, p); - } - - if (m_has_xor && !s().inconsistent()) { - asserted_xor(l, xors, x); - } } check_result card_extension::check() { return CR_DONE; } void card_extension::push() { - m_var_lim.push_back(m_var_trail.size()); + m_index_lim.push_back(m_index_trail.size()); } void card_extension::pop(unsigned n) { TRACE("sat_verbose", tout << "pop:" << n << "\n";); - unsigned new_lim = m_var_lim.size() - n; - unsigned sz = m_var_lim[new_lim]; - while (m_var_trail.size() > sz) { - bool_var v = m_var_trail.back(); - m_var_trail.pop_back(); - if (v != null_bool_var) { - card* c = m_var_infos[v].m_card; - if (c) { - clear_watch(*c); - m_var_infos[v].m_card = 0; - dealloc(c); - } - xor* x = m_var_infos[v].m_xor; - if (x) { - clear_watch(*x); - m_var_infos[v].m_xor = 0; - dealloc(x); - } + unsigned new_lim = m_index_lim.size() - n; + unsigned sz = m_index_lim[new_lim]; + while (m_index_trail.size() > sz) { + unsigned index = m_index_trail.back(); + m_index_trail.pop_back(); + if (is_card_index(index)) { + SASSERT(m_cards.back()->index() == index); + clear_watch(*m_cards.back()); + dealloc(m_cards.back()); + m_cards.pop_back(); + } + else if (is_pb_index(index)) { + SASSERT(m_pbs.back()->index() == index); + clear_watch(*m_pbs.back()); + dealloc(m_pbs.back()); + m_pbs.pop_back(); + } + else if (is_xor_index(index)) { + SASSERT(m_xors.back()->index() == index); + clear_watch(*m_xors.back()); + dealloc(m_xors.back()); + m_xors.pop_back(); + } + else { + UNREACHABLE(); } } - m_var_lim.resize(new_lim); + m_index_lim.resize(new_lim); m_num_propagations_since_pop = 0; } @@ -1604,30 +1433,6 @@ namespace sat { } } - void card_extension::display_watch(std::ostream& out, bool_var v, bool sign) const { - card_watch const* w = m_var_infos[v].m_card_watch[sign]; - if (!is_tag_empty(w)) { - card_watch const& wl = *w; - out << literal(v, sign) << " |-> "; - for (unsigned i = 0; i < wl.size(); ++i) { - out << wl[i]->lit() << " "; - } - out << "\n"; - } - } - - void card_extension::display_watch(std::ostream& out, bool_var v) const { - xor_watch const* w = m_var_infos[v].m_xor_watch; - if (!is_tag_empty(w)) { - xor_watch const& wl = *w; - out << "v" << v << " |-> "; - for (unsigned i = 0; i < wl.size(); ++i) { - out << wl[i]->lit() << " "; - } - out << "\n"; - } - } - void card_extension::display(std::ostream& out, ineq& ineq) const { for (unsigned i = 0; i < ineq.m_lits.size(); ++i) { out << ineq.m_coeffs[i] << "*" << ineq.m_lits[i] << " "; @@ -1694,17 +1499,6 @@ namespace sat { } std::ostream& card_extension::display(std::ostream& out) const { - for (unsigned vi = 0; vi < m_var_infos.size(); ++vi) { - display_watch(out, vi, false); - display_watch(out, vi, true); - display_watch(out, vi); - } - for (unsigned vi = 0; vi < m_var_infos.size(); ++vi) { - card* c = m_var_infos[vi].m_card; - if (c) display(out, *c, false); - xor* x = m_var_infos[vi].m_xor; - if (x) display(out, *x, false); - } return out; } diff --git a/src/sat/card_extension.h b/src/sat/card_extension.h index fbe1141b1..9720bde9c 100644 --- a/src/sat/card_extension.h +++ b/src/sat/card_extension.h @@ -21,8 +21,10 @@ Revision History: #include"sat_extension.h" #include"sat_solver.h" +#include"sat_lookahead.h" #include"scoped_ptr_vector.h" + namespace sat { class card_extension : public extension { @@ -116,52 +118,8 @@ namespace sat { void push(literal l, unsigned c) { m_lits.push_back(l); m_coeffs.push_back(c); } }; - typedef ptr_vector card_watch; - typedef ptr_vector xor_watch; - typedef ptr_vector pb_watch; - struct var_info { - card_watch* m_card_watch[2]; - pb_watch* m_pb_watch[2]; - xor_watch* m_xor_watch; - card* m_card; - pb* m_pb; - xor* m_xor; - var_info(): m_xor_watch(0), m_card(0), m_xor(0), m_pb(0) { - m_card_watch[0] = 0; - m_card_watch[1] = 0; - m_pb_watch[0] = 0; - m_pb_watch[1] = 0; - } - void reset() { - dealloc(m_card); - dealloc(m_xor); - dealloc(m_pb); - dealloc(card_extension::set_tag_non_empty(m_card_watch[0])); - dealloc(card_extension::set_tag_non_empty(m_card_watch[1])); - dealloc(card_extension::set_tag_non_empty(m_pb_watch[0])); - dealloc(card_extension::set_tag_non_empty(m_pb_watch[1])); - dealloc(card_extension::set_tag_non_empty(m_xor_watch)); - } - }; - - template - static ptr_vector* set_tag_empty(ptr_vector* c) { - return TAG(ptr_vector*, c, 1); - } - - template - static bool is_tag_empty(ptr_vector const* c) { - return !c || GET_TAG(c) == 1; - } - - template - static ptr_vector* set_tag_non_empty(ptr_vector* c) { - return UNTAG(ptr_vector*, c); - } - - - solver* m_solver; + lookahead* m_lookahead; stats m_stats; ptr_vector m_cards; @@ -172,9 +130,8 @@ namespace sat { scoped_ptr_vector m_pb_axioms; // watch literals - svector m_var_infos; - unsigned_vector m_var_trail; - unsigned_vector m_var_lim; + unsigned_vector m_index_trail; + unsigned_vector m_index_lim; // conflict resolution unsigned m_num_marks; @@ -185,7 +142,6 @@ namespace sat { tracked_uint_set m_active_var_set; literal_vector m_lemma; unsigned m_num_propagations_since_pop; - bool m_has_xor; unsigned_vector m_parity_marks; literal_vector m_parity_trail; @@ -206,7 +162,7 @@ namespace sat { void clear_watch(card& c); void reset_coeffs(); void reset_marked_literals(); - void unwatch_literal(literal w, card* c); + void unwatch_literal(literal w, card& c); void get_card_antecedents(literal l, card const& c, literal_vector & r); @@ -214,13 +170,12 @@ namespace sat { void copy_xor(card_extension& result); void clear_watch(xor& x); void watch_literal(xor& x, literal lit); - void unwatch_literal(literal w, xor* x); + void unwatch_literal(literal w, xor& x); void init_watch(xor& x, bool is_true); void assign(xor& x, literal lit); void set_conflict(xor& x, literal lit); bool parity(xor const& x, unsigned offset) const; lbool add_assign(xor& x, literal alit); - void asserted_xor(literal l, ptr_vector* xors, xor* x); void get_xor_antecedents(literal l, unsigned index, justification js, literal_vector& r); void get_xor_antecedents(literal l, xor const& x, literal_vector & r); @@ -236,7 +191,6 @@ namespace sat { // pb functionality unsigned m_a_max; void copy_pb(card_extension& result); - void asserted_pb(literal l, ptr_vector* pbs, pb* p); void init_watch(pb& p, bool is_true); lbool add_assign(pb& p, literal alit); void add_index(pb& p, unsigned index, literal lit); @@ -244,28 +198,18 @@ namespace sat { void clear_watch(pb& p); void set_conflict(pb& p, literal lit); void assign(pb& p, literal l); - void unwatch_literal(literal w, pb* p); + void unwatch_literal(literal w, pb& p); void get_pb_antecedents(literal l, pb const& p, literal_vector & r); - - template - bool remove(ptr_vector& ts, T* t) { - unsigned sz = ts.size(); - for (unsigned j = 0; j < sz; ++j) { - if (ts[j] == t) { - std::swap(ts[j], ts[sz-1]); - ts.pop_back(); - return sz == 1; - } - } - return false; - } - - - - inline lbool value(literal lit) const { return m_solver->value(lit); } + inline lbool value(literal lit) const { return m_lookahead ? m_lookahead->value(lit) : m_solver->value(lit); } inline unsigned lvl(literal lit) const { return m_solver->lvl(lit); } inline unsigned lvl(bool_var v) const { return m_solver->lvl(v); } + inline bool inconsistent() const { return m_lookahead ? m_lookahead->inconsistent() : m_solver->inconsistent(); } + inline watch_list& get_wlist(literal l) { return m_lookahead ? m_lookahead->get_wlist(l) : m_solver->get_wlist(l); } + inline void assign(literal l, justification j) { if (m_lookahead) m_lookahead->assign(l); else m_solver->assign(l, j); } + inline void set_conflict(justification j, literal l) { if (m_lookahead) m_lookahead->set_conflict(); else m_solver->set_conflict(j, l); } + inline config const& get_config() const { return m_solver->get_config(); } + inline void drat_add(literal_vector const& c, svector const& premises) { m_solver->m_drat.add(c, premises); } void normalize_active_coeffs(); @@ -296,13 +240,12 @@ namespace sat { void display(std::ostream& out, card const& c, bool values) const; void display(std::ostream& out, pb const& p, bool values) const; void display(std::ostream& out, xor const& c, bool values) const; - void display_watch(std::ostream& out, bool_var v) const; - void display_watch(std::ostream& out, bool_var v, bool sign) const; public: card_extension(); virtual ~card_extension(); virtual void set_solver(solver* s) { m_solver = s; } + virtual void set_lookahead(lookahead* l) { m_lookahead = l; } void add_at_least(bool_var v, literal_vector const& lits, unsigned k); void add_pb_ge(bool_var v, svector const& wlits, unsigned k); void add_xor(bool_var v, literal_vector const& lits); diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h index a875bad6c..44a704f80 100644 --- a/src/sat/sat_extension.h +++ b/src/sat/sat_extension.h @@ -33,6 +33,7 @@ namespace sat { public: virtual ~extension() {} virtual void set_solver(solver* s) = 0; + virtual void set_lookahead(lookahead* s) = 0; virtual void propagate(literal l, ext_constraint_idx idx, bool & keep) = 0; virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) = 0; virtual void asserted(literal l) = 0; diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp new file mode 100644 index 000000000..597efa49a --- /dev/null +++ b/src/sat/sat_lookahead.cpp @@ -0,0 +1,1597 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + sat_lookahead.h + +Abstract: + + Lookahead SAT solver in the style of March. + Thanks also to the presentation in sat11.w. + +Author: + + Nikolaj Bjorner (nbjorner) 2017-2-11 + +Notes: + +--*/ +#include "sat_solver.h" +#include "sat_extension.h" +#include "sat_lookahead.h" + +namespace sat { + lookahead::scoped_ext::scoped_ext(lookahead& p): p(p) { + if (p.m_s.m_ext) p.m_s.m_ext->set_lookahead(&p); + } + + lookahead::scoped_ext::~scoped_ext() { + if (p.m_s.m_ext) p.m_s.m_ext->set_lookahead(0); + } + + void lookahead::flip_prefix() { + if (m_trail_lim.size() < 64) { + uint64 mask = (1ull << m_trail_lim.size()); + m_prefix = mask | (m_prefix & (mask - 1)); + } + } + + void lookahead::prune_prefix() { + if (m_trail_lim.size() < 64) { + m_prefix &= (1ull << m_trail_lim.size()) - 1; + } + } + + void lookahead::update_prefix(literal l) { + bool_var x = l.var(); + unsigned p = m_vprefix[x].m_prefix; + unsigned pl = m_vprefix[x].m_length; + unsigned mask = (1 << std::min(31u, pl)) - 1; + if (pl >= m_trail_lim.size() || (p & mask) != (m_prefix & mask)) { + m_vprefix[x].m_length = m_trail_lim.size(); + m_vprefix[x].m_prefix = static_cast(m_prefix); + } + } + + bool lookahead::active_prefix(bool_var x) { + unsigned lvl = m_trail_lim.size(); + unsigned p = m_vprefix[x].m_prefix; + unsigned l = m_vprefix[x].m_length; + if (l > lvl) return false; + if (l == lvl || l >= 31) return m_prefix == p; + unsigned mask = ((1 << std::min(l,31u)) - 1); + return (m_prefix & mask) == (p & mask); + } + + void lookahead::add_binary(literal l1, literal l2) { + TRACE("sat", tout << "binary: " << l1 << " " << l2 << "\n";); + SASSERT(l1 != l2); + // don't add tautologies and don't add already added binaries + if (~l1 == l2) return; + if (!m_binary[(~l1).index()].empty() && m_binary[(~l1).index()].back() == l2) return; + m_binary[(~l1).index()].push_back(l2); + m_binary[(~l2).index()].push_back(l1); + m_binary_trail.push_back((~l1).index()); + ++m_stats.m_add_binary; + if (m_s.m_config.m_drat) validate_binary(l1, l2); + } + + void lookahead::del_binary(unsigned idx) { + // TRACE("sat", display(tout << "Delete " << to_literal(idx) << "\n");); + literal_vector & lits = m_binary[idx]; + SASSERT(!lits.empty()); + literal l = lits.back(); + lits.pop_back(); + SASSERT(!m_binary[(~l).index()].empty()); + IF_VERBOSE(0, if (m_binary[(~l).index()].back() != ~to_literal(idx)) verbose_stream() << "pop bad literal: " << idx << " " << (~l).index() << "\n";); + SASSERT(m_binary[(~l).index()].back() == ~to_literal(idx)); + m_binary[(~l).index()].pop_back(); + ++m_stats.m_del_binary; + } + + + void lookahead::validate_binary(literal l1, literal l2) { + if (m_search_mode == lookahead_mode::searching) { + m_assumptions.push_back(l1); + m_assumptions.push_back(l2); + m_drat.add(m_assumptions); + m_assumptions.pop_back(); + m_assumptions.pop_back(); + } + } + + + void lookahead::inc_bstamp() { + ++m_bstamp_id; + if (m_bstamp_id == 0) { + ++m_bstamp_id; + m_bstamp.fill(0); + } + } + void lookahead::inc_istamp() { + ++m_istamp_id; + if (m_istamp_id == 0) { + ++m_istamp_id; + for (unsigned i = 0; i < m_lits.size(); ++i) { + m_lits[i].m_double_lookahead = 0; + } + } + } + + void lookahead::set_bstamps(literal l) { + inc_bstamp(); + set_bstamp(l); + literal_vector const& conseq = m_binary[l.index()]; + literal_vector::const_iterator it = conseq.begin(); + literal_vector::const_iterator end = conseq.end(); + for (; it != end; ++it) { + set_bstamp(*it); + } + } + + /** + \brief add one-step transitive closure of binary implications + return false if we learn a unit literal. + \pre all implicants of ~u are stamped. + u \/ v is true + **/ + + bool lookahead::add_tc1(literal u, literal v) { + unsigned sz = m_binary[v.index()].size(); + for (unsigned i = 0; i < sz; ++i) { + literal w = m_binary[v.index()][i]; + // ~v \/ w + if (!is_fixed(w)) { + if (is_stamped(~w)) { + // u \/ v, ~v \/ w, u \/ ~w => u is unit + TRACE("sat", tout << "tc1: " << u << "\n";); + assign(u); + return false; + } + if (m_num_tc1 < m_config.m_tc1_limit) { + ++m_num_tc1; + IF_VERBOSE(3, verbose_stream() << "tc1: " << u << " " << w << "\n";); + add_binary(u, w); + } + } + } + return true; + } + + + /** + \brief main routine for adding a new binary clause dynamically. + */ + void lookahead::try_add_binary(literal u, literal v) { + SASSERT(m_search_mode == lookahead_mode::searching); + SASSERT(u.var() != v.var()); + if (!is_undef(u) || !is_undef(v)) { + IF_VERBOSE(0, verbose_stream() << "adding assigned binary " << v << " " << u << "\n";); + } + set_bstamps(~u); + if (is_stamped(~v)) { + TRACE("sat", tout << "try_add_binary: " << u << "\n";); + assign(u); // u \/ ~v, u \/ v => u is a unit literal + } + else if (!is_stamped(v) && add_tc1(u, v)) { + // u \/ v is not in index + set_bstamps(~v); + if (is_stamped(~u)) { + TRACE("sat", tout << "try_add_binary: " << v << "\n";); + assign(v); // v \/ ~u, u \/ v => v is a unit literal + } + else if (add_tc1(v, u)) { + update_prefix(u); + update_prefix(v); + add_binary(u, v); + } + } + } + + // ------------------------------------- + // pre-selection + // see also 91 - 102 sat11.w + + + void lookahead::pre_select() { + m_lookahead.reset(); + if (select(scope_lvl())) { + get_scc(); + if (inconsistent()) return; + find_heights(); + construct_lookahead_table(); + } + } + + + bool lookahead::select(unsigned level) { + init_pre_selection(level); + unsigned level_cand = std::max(m_config.m_level_cand, m_freevars.size() / 50); + unsigned max_num_cand = level == 0 ? m_freevars.size() : level_cand / level; + max_num_cand = std::max(m_config.m_min_cutoff, max_num_cand); + + float sum = 0; + for (bool newbies = false; ; newbies = true) { + sum = init_candidates(level, newbies); + if (!m_candidates.empty()) break; + if (is_sat()) { + return false; + } + if (newbies) { + enable_trace("sat"); + TRACE("sat", display(tout);); + TRACE("sat", tout << sum << "\n";); + } + } + SASSERT(!m_candidates.empty()); + // cut number of candidates down to max_num_cand. + // step 1. cut it to at most 2*max_num_cand. + // step 2. use a heap to sift through the rest. + bool progress = true; + while (progress && m_candidates.size() >= max_num_cand * 2) { + progress = false; + float mean = sum / (float)(m_candidates.size() + 0.0001); + sum = 0; + for (unsigned i = 0; i < m_candidates.size() && m_candidates.size() >= max_num_cand * 2; ++i) { + if (m_candidates[i].m_rating >= mean) { + sum += m_candidates[i].m_rating; + } + else { + m_candidates[i] = m_candidates.back(); + m_candidates.pop_back(); + --i; + progress = true; + } + } + } + TRACE("sat", display_candidates(tout);); + SASSERT(!m_candidates.empty()); + if (m_candidates.size() > max_num_cand) { + unsigned j = m_candidates.size()/2; + while (j > 0) { + --j; + sift_up(j); + } + while (true) { + m_candidates[0] = m_candidates.back(); + m_candidates.pop_back(); + if (m_candidates.size() == max_num_cand) break; + sift_up(0); + } + } + SASSERT(!m_candidates.empty() && m_candidates.size() <= max_num_cand); + TRACE("sat", display_candidates(tout);); + return true; + } + + void lookahead::sift_up(unsigned j) { + unsigned i = j; + candidate c = m_candidates[j]; + for (unsigned k = 2*j + 1; k < m_candidates.size(); i = k, k = 2*k + 1) { + // pick largest parent + if (k + 1 < m_candidates.size() && m_candidates[k].m_rating < m_candidates[k+1].m_rating) { + ++k; + } + if (c.m_rating <= m_candidates[k].m_rating) break; + m_candidates[i] = m_candidates[k]; + } + if (i > j) m_candidates[i] = c; + } + + float lookahead::init_candidates(unsigned level, bool newbies) { + m_candidates.reset(); + float sum = 0; + for (bool_var const* it = m_freevars.begin(), * end = m_freevars.end(); it != end; ++it) { + SASSERT(is_undef(*it)); + bool_var x = *it; + if (!m_select_lookahead_vars.empty() && m_select_lookahead_vars.contains(x)) { + m_candidates.push_back(candidate(x, m_rating[x])); + sum += m_rating[x]; + } + else if (newbies || active_prefix(x)) { + m_candidates.push_back(candidate(x, m_rating[x])); + sum += m_rating[x]; + } + } + TRACE("sat", display_candidates(tout << "sum: " << sum << "\n");); + return sum; + } + + + std::ostream& lookahead::display_candidates(std::ostream& out) const { + for (unsigned i = 0; i < m_candidates.size(); ++i) { + out << "var: " << m_candidates[i].m_var << " rating: " << m_candidates[i].m_rating << "\n"; + } + return out; + } + + bool lookahead::is_unsat() const { + for (unsigned i = 0; i < m_clauses.size(); ++i) { + clause& c = *m_clauses[i]; + unsigned j = 0; + for (; j < c.size() && is_false(c[j]); ++j) {} + if (j == c.size()) { + TRACE("sat", tout << c << "\n";); + TRACE("sat", display(tout);); + return true; + } + } + return false; + } + + bool lookahead::is_sat() const { + for (bool_var const* it = m_freevars.begin(), * end = m_freevars.end(); it != end; ++it) { + literal l(*it, false); + literal_vector const& lits1 = m_binary[l.index()]; + for (unsigned i = 0; i < lits1.size(); ++i) { + if (!is_true(lits1[i])) { + TRACE("sat", tout << l << " " << lits1[i] << "\n";); + return false; + } + } + l.neg(); + literal_vector const& lits2 = m_binary[l.index()]; + for (unsigned i = 0; i < lits2.size(); ++i) { + if (!is_true(lits2[i])) { + TRACE("sat", tout << l << " " << lits2[i] << "\n";); + return false; + } + } + } + for (unsigned i = 0; i < m_clauses.size(); ++i) { + clause& c = *m_clauses[i]; + unsigned j = 0; + for (; j < c.size() && !is_true(c[j]); ++j) {} + if (j == c.size()) { + return false; + } + } + return true; + } + + void lookahead::init_pre_selection(unsigned level) { + unsigned max_level = m_config.m_max_hlevel; + if (level <= 1) { + ensure_H(2); + h_scores(m_H[0], m_H[1]); + for (unsigned j = 0; j < 2; ++j) { + for (unsigned i = 0; i < 2; ++i) { + h_scores(m_H[i + 1], m_H[(i + 2) % 3]); + } + } + m_heur = &m_H[1]; + } + else if (level < max_level) { + ensure_H(level); + h_scores(m_H[level-1], m_H[level]); + m_heur = &m_H[level]; + } + else { + ensure_H(max_level); + h_scores(m_H[max_level-1], m_H[max_level]); + m_heur = &m_H[max_level]; + } + } + + void lookahead::ensure_H(unsigned level) { + while (m_H.size() <= level) { + m_H.push_back(svector()); + m_H.back().resize(m_num_vars * 2, 0); + } + } + + void lookahead::h_scores(svector& h, svector& hp) { + float sum = 0; + for (bool_var const* it = m_freevars.begin(), * end = m_freevars.end(); it != end; ++it) { + literal l(*it, false); + sum += h[l.index()] + h[(~l).index()]; + } + float factor = 2 * m_freevars.size() / sum; + float sqfactor = factor * factor; + float afactor = factor * m_config.m_alpha; + for (bool_var const* it = m_freevars.begin(), * end = m_freevars.end(); it != end; ++it) { + literal l(*it, false); + float pos = l_score(l, h, factor, sqfactor, afactor); + float neg = l_score(~l, h, factor, sqfactor, afactor); + hp[l.index()] = pos; + hp[(~l).index()] = neg; + m_rating[l.var()] = pos * neg; + } + } + + float lookahead::l_score(literal l, svector const& h, float factor, float sqfactor, float afactor) { + float sum = 0, tsum = 0; + literal_vector::iterator it = m_binary[l.index()].begin(), end = m_binary[l.index()].end(); + for (; it != end; ++it) { + bool_var v = it->var(); + if (it->index() >= h.size()) + IF_VERBOSE(0, verbose_stream() << l << " " << *it << " " << h.size() << "\n";); + if (is_undef(*it)) sum += h[it->index()]; + // if (m_freevars.contains(it->var())) sum += h[it->index()]; + } + watch_list& wlist = m_watches[l.index()]; + watch_list::iterator wit = wlist.begin(), wend = wlist.end(); + for (; wit != wend; ++wit) { + switch (wit->get_kind()) { + case watched::BINARY: + UNREACHABLE(); + break; + case watched::TERNARY: { + literal l1 = wit->get_literal1(); + literal l2 = wit->get_literal2(); + // if (is_undef(l1) && is_undef(l2)) + tsum += h[l1.index()] * h[l2.index()]; + break; + } + case watched::CLAUSE: { + clause_offset cls_off = wit->get_clause_offset(); + clause & c = *(m_cls_allocator.get_clause(cls_off)); + // approximation compared to ternary clause case: + // we pick two other literals from the clause. + if (c[0] == ~l) { + tsum += h[c[1].index()] * h[c[2].index()]; + } + else { + SASSERT(c[1] == ~l); + tsum += h[c[0].index()] * h[c[2].index()]; + } + break; + } + } + } + sum = (float)(0.1 + afactor*sum + sqfactor*tsum); + return std::min(m_config.m_max_score, sum); + } + + // ------------------------------------ + // Implication graph + // Compute implication ordering and strongly connected components. + // sat11.w 103 - 114. + + void lookahead::get_scc() { + unsigned num_candidates = m_candidates.size(); + init_scc(); + for (unsigned i = 0; i < num_candidates && !inconsistent(); ++i) { + literal lit(m_candidates[i].m_var, false); + if (get_rank(lit) == 0) get_scc(lit); + if (get_rank(~lit) == 0) get_scc(~lit); + } + TRACE("sat", display_scc(tout);); + } + void lookahead::init_scc() { + inc_bstamp(); + for (unsigned i = 0; i < m_candidates.size(); ++i) { + literal lit(m_candidates[i].m_var, false); + init_dfs_info(lit); + init_dfs_info(~lit); + } + for (unsigned i = 0; i < m_candidates.size(); ++i) { + literal lit(m_candidates[i].m_var, false); + init_arcs(lit); + init_arcs(~lit); + } + m_rank = 0; + m_active = null_literal; + m_settled = null_literal; + TRACE("sat", display_dfs(tout);); + } + void lookahead::init_dfs_info(literal l) { + unsigned idx = l.index(); + m_dfs[idx].reset(); + set_bstamp(l); + } + // arcs are added in the opposite direction of implications. + // So for implications l => u we add arcs u -> l + void lookahead::init_arcs(literal l) { + literal_vector const& succ = m_binary[l.index()]; + for (unsigned i = 0; i < succ.size(); ++i) { + literal u = succ[i]; + SASSERT(u != l); + if (u.index() > l.index() && is_stamped(u)) { + add_arc(~l, ~u); + add_arc( u, l); + } + } + } + + void lookahead::get_scc(literal v) { + TRACE("scc", tout << v << "\n";); + set_parent(v, null_literal); + activate_scc(v); + do { + literal ll = get_min(v); + if (has_arc(v)) { + literal u = pop_arc(v); + unsigned r = get_rank(u); + if (r > 0) { + // u was processed before ll + if (r < get_rank(ll)) set_min(v, u); + } + else { + // process u in dfs order, add v to dfs stack for u + set_parent(u, v); + v = u; + activate_scc(v); + } + } + else { + literal u = get_parent(v); + if (v == ll) { + found_scc(v); + } + else if (get_rank(ll) < get_rank(get_min(u))) { + set_min(u, ll); + } + // walk back in the dfs stack + v = u; + } + } + while (v != null_literal && !inconsistent()); + } + + void lookahead::activate_scc(literal l) { + SASSERT(get_rank(l) == 0); + set_rank(l, ++m_rank); + set_link(l, m_active); + set_min(l, l); + m_active = l; + } + // make v root of the scc equivalence class + // set vcomp to be the highest rated literal + void lookahead::found_scc(literal v) { + literal t = m_active; + m_active = get_link(v); + literal best = v; + float best_rating = get_rating(v); + set_rank(v, UINT_MAX); + set_link(v, m_settled); m_settled = t; + while (t != v) { + if (t == ~v) { + TRACE("sat", display_scc(tout << "found contradiction during scc search\n");); + set_conflict(); + break; + } + set_rank(t, UINT_MAX); + set_parent(t, v); + float t_rating = get_rating(t); + if (t_rating > best_rating) { + best = t; + best_rating = t_rating; + } + t = get_link(t); + } + set_parent(v, v); + set_vcomp(v, best); + if (get_rank(~v) == UINT_MAX) { + set_vcomp(v, ~get_vcomp(get_parent(~v))); + } + } + + std::ostream& lookahead::display_dfs(std::ostream& out) const { + for (unsigned i = 0; i < m_candidates.size(); ++i) { + literal l(m_candidates[i].m_var, false); + display_dfs(out, l); + display_dfs(out, ~l); + } + return out; + } + + std::ostream& lookahead::display_dfs(std::ostream& out, literal l) const { + arcs const& a1 = get_arcs(l); + if (!a1.empty()) { + out << l << " -> " << a1 << "\n"; + } + return out; + } + + std::ostream& lookahead::display_scc(std::ostream& out) const { + display_dfs(out); + for (unsigned i = 0; i < m_candidates.size(); ++i) { + literal l(m_candidates[i].m_var, false); + display_scc(out, l); + display_scc(out, ~l); + } + return out; + } + + std::ostream& lookahead::display_scc(std::ostream& out, literal l) const { + out << l << " := " << get_parent(l) + << " min: " << get_min(l) + << " rank: " << get_rank(l) + << " height: " << get_height(l) + << " link: " << get_link(l) + << " child: " << get_child(l) + << " vcomp: " << get_vcomp(l) << "\n"; + return out; + } + + + // ------------------------------------ + // lookahead forest + // sat11.w 115-121 + + literal lookahead::get_child(literal u) const { + if (u == null_literal) return m_root_child; + return m_dfs[u.index()].m_min; + } + + void lookahead::set_child(literal v, literal u) { + if (v == null_literal) m_root_child = u; + else m_dfs[v.index()].m_min = u; + } + + /* + \brief Assign heights to the nodes. + Nodes within the same strongly connected component are given the same height. + The code assumes that m_settled is topologically sorted such that + 1. nodes in the same equivalence class come together + 2. the equivalence class representative is last + + */ + void lookahead::find_heights() { + m_root_child = null_literal; + literal pp = null_literal; + unsigned h = 0; + literal w, uu; + TRACE("sat", + for (literal u = m_settled; u != null_literal; u = get_link(u)) { + tout << u << " "; + } + tout << "\n";); + for (literal u = m_settled; u != null_literal; u = uu) { + TRACE("sat", tout << "process: " << u << "\n";); + uu = get_link(u); + literal p = get_parent(u); + if (p != pp) { + // new equivalence class + h = 0; + w = null_literal; + pp = p; + } + // traverse nodes in order of implication + unsigned sz = num_next(~u); + for (unsigned j = 0; j < sz; ++j) { + literal v = ~get_next(~u, j); + TRACE("sat", tout << "child " << v << " link: " << get_link(v) << "\n";); + literal pv = get_parent(v); + // skip nodes in same equivalence, they will all be processed + if (pv == p) continue; + unsigned hh = get_height(pv); + // update the maximal height descendant + if (hh >= h) { + h = hh + 1; + w = pv; + } + } + if (p == u) { + // u is an equivalence class representative + // it is processed last + literal v = get_child(w); + set_height(u, h); + set_child(u, null_literal); + set_link(u, v); + set_child(w, u); + TRACE("sat", tout << "child(" << w << ") = " << u << " link(" << u << ") = " << v << "\n";); + } + } + TRACE("sat", + display_forest(tout << "forest: ", get_child(null_literal)); + tout << "\n"; + display_scc(tout); ); + } + std::ostream& lookahead::display_forest(std::ostream& out, literal l) { + for (literal u = l; u != null_literal; u = get_link(u)) { + out << u << " "; + l = get_child(u); + if (l != null_literal) { + out << "("; + display_forest(out, l); + out << ") "; + } + } + return out; + } + + void lookahead::construct_lookahead_table() { + literal u = get_child(null_literal), v = null_literal; + unsigned offset = 0; + SASSERT(m_lookahead.empty()); + while (u != null_literal) { + set_rank(u, m_lookahead.size()); + set_lookahead(get_vcomp(u)); + if (null_literal != get_child(u)) { + set_parent(u, v); + v = u; + u = get_child(u); + } + else { + while (true) { + set_offset(get_rank(u), offset); + offset += 2; + set_parent(u, v == null_literal ? v : get_vcomp(v)); + u = get_link(u); + if (u == null_literal && v != null_literal) { + u = v; + v = get_parent(u); + } + else { + break; + } + } + } + } + SASSERT(2*m_lookahead.size() == offset); + TRACE("sat", for (unsigned i = 0; i < m_lookahead.size(); ++i) + tout << m_lookahead[i].m_lit << " : " << m_lookahead[i].m_offset << "\n";); + } + + + // ------------------------------------ + // clause management + + void lookahead::attach_clause(clause& c) { + if (c.size() == 3) { + attach_ternary(c[0], c[1], c[2]); + } + else { + literal block_lit = c[c.size() >> 2]; + clause_offset cls_off = m_cls_allocator.get_offset(&c); + m_watches[(~c[0]).index()].push_back(watched(block_lit, cls_off)); + m_watches[(~c[1]).index()].push_back(watched(block_lit, cls_off)); + SASSERT(is_undef(c[0])); + SASSERT(is_undef(c[1])); + } + } + + void lookahead::detach_clause(clause& c) { + clause_offset cls_off = m_cls_allocator.get_offset(&c); + m_retired_clauses.push_back(&c); + erase_clause_watch(get_wlist(~c[0]), cls_off); + erase_clause_watch(get_wlist(~c[1]), cls_off); + } + + void lookahead::del_clauses() { + clause * const* end = m_clauses.end(); + clause * const * it = m_clauses.begin(); + for (; it != end; ++it) { + m_cls_allocator.del_clause(*it); + } + } + + void lookahead::detach_ternary(literal l1, literal l2, literal l3) { + ++m_stats.m_del_ternary; + m_retired_ternary.push_back(ternary(l1, l2, l3)); + // implicitly erased: erase_ternary_watch(get_wlist(~l1), l2, l3); + erase_ternary_watch(get_wlist(~l2), l1, l3); + erase_ternary_watch(get_wlist(~l3), l1, l2); + } + + void lookahead::attach_ternary(ternary const& t) { + attach_ternary(t.m_u, t.m_v, t.m_w); + } + + void lookahead::attach_ternary(literal l1, literal l2, literal l3) { + ++m_stats.m_add_ternary; + TRACE("sat", tout << l1 << " " << l2 << " " << l3 << "\n";); + m_watches[(~l1).index()].push_back(watched(l2, l3)); + m_watches[(~l2).index()].push_back(watched(l1, l3)); + m_watches[(~l3).index()].push_back(watched(l1, l2)); + } + + // ------------------------------------ + // initialization + + void lookahead::init_var(bool_var v) { + m_binary.push_back(literal_vector()); + m_binary.push_back(literal_vector()); + m_watches.push_back(watch_list()); + m_watches.push_back(watch_list()); + m_full_watches.push_back(clause_vector()); + m_full_watches.push_back(clause_vector()); + m_bstamp.push_back(0); + m_bstamp.push_back(0); + m_stamp.push_back(0); + m_dfs.push_back(dfs_info()); + m_dfs.push_back(dfs_info()); + m_lits.push_back(lit_info()); + m_lits.push_back(lit_info()); + m_rating.push_back(0); + m_vprefix.push_back(prefix()); + if (!m_s.was_eliminated(v)) + m_freevars.insert(v); + } + + void lookahead::init() { + m_delta_trigger = m_num_vars/10; + m_config.m_dl_success = 0.8; + m_inconsistent = false; + m_qhead = 0; + m_bstamp_id = 0; + + for (unsigned i = 0; i < m_num_vars; ++i) { + init_var(i); + } + + // copy binary clauses + unsigned sz = m_s.m_watches.size(); + for (unsigned l_idx = 0; l_idx < sz; ++l_idx) { + literal l = ~to_literal(l_idx); + watch_list const & wlist = m_s.m_watches[l_idx]; + watch_list::const_iterator it = wlist.begin(); + watch_list::const_iterator end = wlist.end(); + for (; it != end; ++it) { + if (!it->is_binary_non_learned_clause()) + continue; + literal l2 = it->get_literal(); + SASSERT(!m_s.was_eliminated(l.var())); + SASSERT(!m_s.was_eliminated(l2.var())); + if (l.index() < l2.index()) + add_binary(l, l2); + } + } + + copy_clauses(m_s.m_clauses); + copy_clauses(m_s.m_learned); + + // copy units + unsigned trail_sz = m_s.init_trail_size(); + for (unsigned i = 0; i < trail_sz; ++i) { + literal l = m_s.m_trail[i]; + if (!m_s.was_eliminated(l.var())) { + if (m_s.m_config.m_drat) m_drat.add(l, false); + assign(l); + } + } + propagate(); + m_qhead = m_trail.size(); + TRACE("sat", m_s.display(tout); display(tout);); + } + + void lookahead::copy_clauses(clause_vector const& clauses) { + // copy clauses + clause_vector::const_iterator it = clauses.begin(); + clause_vector::const_iterator end = clauses.end(); + for (; it != end; ++it) { + clause& c = *(*it); + if (c.was_removed()) continue; + clause* c1 = m_cls_allocator.mk_clause(c.size(), c.begin(), false); + m_clauses.push_back(c1); + attach_clause(*c1); + for (unsigned i = 0; i < c.size(); ++i) { + m_full_watches[(~c[i]).index()].push_back(c1); + SASSERT(!m_s.was_eliminated(c[i].var())); + } + if (m_s.m_config.m_drat) m_drat.add(c, false); + } + } + + // ------------------------------------ + // search + + + void lookahead::push(literal lit, unsigned level) { + SASSERT(m_search_mode == lookahead_mode::searching); + m_binary_trail_lim.push_back(m_binary_trail.size()); + m_trail_lim.push_back(m_trail.size()); + m_num_tc1_lim.push_back(m_num_tc1); + m_retired_clause_lim.push_back(m_retired_clauses.size()); + m_retired_ternary_lim.push_back(m_retired_ternary.size()); + m_qhead_lim.push_back(m_qhead); + scoped_level _sl(*this, level); + m_assumptions.push_back(~lit); + assign(lit); + propagate(); + } + + void lookahead::pop() { + if (m_assumptions.empty()) IF_VERBOSE(0, verbose_stream() << "empty pop\n";); + m_assumptions.pop_back(); + m_inconsistent = false; + SASSERT(m_search_mode == lookahead_mode::searching); + + // m_freevars only for main search + // undo assignments + unsigned old_sz = m_trail_lim.back(); + for (unsigned i = m_trail.size(); i > old_sz; ) { + --i; + literal l = m_trail[i]; + set_undef(l); + TRACE("sat", tout << "inserting free var v" << l.var() << "\n";); + m_freevars.insert(l.var()); + } + m_trail.shrink(old_sz); // reset assignment. + m_trail_lim.pop_back(); + + m_num_tc1 = m_num_tc1_lim.back(); + m_num_tc1_lim.pop_back(); + + // unretire clauses + old_sz = m_retired_clause_lim.back(); + for (unsigned i = old_sz; i < m_retired_clauses.size(); ++i) { + attach_clause(*m_retired_clauses[i]); + } + m_retired_clauses.resize(old_sz); + m_retired_clause_lim.pop_back(); + + old_sz = m_retired_ternary_lim.back(); + for (unsigned i = old_sz; i < m_retired_ternary.size(); ++i) { + attach_ternary(m_retired_ternary[i]); + } + m_retired_ternary.shrink(old_sz); + m_retired_ternary_lim.pop_back(); + + // remove local binary clauses + old_sz = m_binary_trail_lim.back(); + for (unsigned i = m_binary_trail.size(); i > old_sz; ) { + del_binary(m_binary_trail[--i]); + } + m_binary_trail.shrink(old_sz); + m_binary_trail_lim.pop_back(); + + // reset propagation queue + m_qhead = m_qhead_lim.back(); + m_qhead_lim.pop_back(); + } + + bool lookahead::push_lookahead2(literal lit, unsigned level) { + scoped_level _sl(*this, level); + SASSERT(m_search_mode == lookahead_mode::lookahead1); + m_search_mode = lookahead_mode::lookahead2; + assign(lit); + propagate(); + bool unsat = inconsistent(); + SASSERT(m_search_mode == lookahead_mode::lookahead2); + m_search_mode = lookahead_mode::lookahead1; + m_inconsistent = false; + return unsat; + } + + void lookahead::push_lookahead1(literal lit, unsigned level) { + SASSERT(m_search_mode == lookahead_mode::searching); + m_search_mode = lookahead_mode::lookahead1; + scoped_level _sl(*this, level); + assign(lit); + propagate(); + } + + void lookahead::pop_lookahead1(literal lit) { + bool unsat = inconsistent(); + SASSERT(m_search_mode == lookahead_mode::lookahead1); + m_inconsistent = false; + m_search_mode = lookahead_mode::searching; + // convert windfalls to binary clauses. + if (!unsat) { + literal nlit = ~lit; + + for (unsigned i = 0; i < m_wstack.size(); ++i) { + literal l2 = m_wstack[i]; + //update_prefix(~lit); + //update_prefix(m_wstack[i]); + TRACE("sat", tout << "windfall: " << nlit << " " << l2 << "\n";); + // if we use try_add_binary, then this may produce new assignments + // these assignments get put on m_trail, and they are cleared by + // reset_wnb. We would need to distinguish the trail that comes + // from lookahead levels and the main search level for this to work. + add_binary(nlit, l2); + } + m_stats.m_windfall_binaries += m_wstack.size(); + } + m_wstack.reset(); + } + + clause const& lookahead::get_clause(watch_list::iterator it) const { + clause_offset cls_off = it->get_clause_offset(); + return *(m_cls_allocator.get_clause(cls_off)); + } + + bool lookahead::is_nary_propagation(clause const& c, literal l) const { + bool r = c.size() > 2 && ((c[0] == l && is_false(c[1])) || (c[1] == l && is_false(c[0]))); + DEBUG_CODE(if (r) for (unsigned j = 2; j < c.size(); ++j) SASSERT(is_false(c[j]));); + return r; + } + + + // + // The current version is modeled after CDCL SAT solving data-structures. + // It borrows from the watch list data-structure. The cost tradeoffs are somewhat + // biased towards CDCL search overheads. + // If we walk over the positive occurrences of l, then those clauses can be retired so + // that they don't interfere with calculation of H. Instead of removing clauses from the watch + // list one can swap them to the "back" and adjust a size indicator of the watch list + // Only the size indicator needs to be updated on backtracking. + // + + void lookahead::propagate_clauses(literal l) { + SASSERT(is_true(l)); + if (inconsistent()) return; + watch_list& wlist = m_watches[l.index()]; + watch_list::iterator it = wlist.begin(), it2 = it, end = wlist.end(); + for (; it != end && !inconsistent(); ++it) { + switch (it->get_kind()) { + case watched::BINARY: + UNREACHABLE(); + break; + case watched::TERNARY: { + literal l1 = it->get_literal1(); + literal l2 = it->get_literal2(); + bool skip = false; + if (is_fixed(l1)) { + if (is_false(l1)) { + if (is_undef(l2)) { + propagated(l2); + } + else if (is_false(l2)) { + TRACE("sat", tout << l1 << " " << l2 << " " << l << "\n";); + set_conflict(); + } + } + else { + // retire this clause + } + } + else if (is_fixed(l2)) { + if (is_false(l2)) { + propagated(l1); + } + else { + // retire this clause + } + } + else { + switch (m_search_mode) { + case lookahead_mode::searching: + detach_ternary(~l, l1, l2); + try_add_binary(l1, l2); + skip = true; + break; + case lookahead_mode::lookahead1: + m_weighted_new_binaries += (*m_heur)[l1.index()] * (*m_heur)[l2.index()]; + break; + case lookahead2: + break; + } + } + if (!skip) { + *it2 = *it; + it2++; + } + break; + } + case watched::CLAUSE: { + if (is_true(it->get_blocked_literal())) { + *it2 = *it; + ++it2; + break; + } + clause_offset cls_off = it->get_clause_offset(); + clause & c = *(m_cls_allocator.get_clause(cls_off)); + if (c[0] == ~l) + std::swap(c[0], c[1]); + if (is_true(c[0])) { + it->set_blocked_literal(c[0]); + *it2 = *it; + it2++; + break; + } + literal * l_it = c.begin() + 2; + literal * l_end = c.end(); + bool found = false; + for (; l_it != l_end && !found; ++l_it) { + if (!is_false(*l_it)) { + found = true; + c[1] = *l_it; + *l_it = ~l; + m_watches[(~c[1]).index()].push_back(watched(c[0], cls_off)); + TRACE("sat_verbose", tout << "move watch from " << l << " to " << c[1] << " for clause " << c << "\n";); + } + } + if (found) { + found = false; + for (; l_it != l_end && !found; ++l_it) { + found = !is_false(*l_it); + } + // normal clause was converted to a binary clause. + if (!found && is_undef(c[1]) && is_undef(c[0])) { + TRACE("sat", tout << "got binary " << l << ": " << c << "\n";); + switch (m_search_mode) { + case lookahead_mode::searching: + detach_clause(c); + try_add_binary(c[0], c[1]); + break; + case lookahead_mode::lookahead1: + m_weighted_new_binaries += (*m_heur)[c[0].index()]* (*m_heur)[c[1].index()]; + break; + case lookahead_mode::lookahead2: + break; + } + } + else if (found && m_search_mode == lookahead_mode::lookahead1 && m_weighted_new_binaries == 0) { + // leave a trail that some clause was reduced but potentially not an autarky + l_it = c.begin() + 2; + found = false; + for (; l_it != l_end && !found; found = is_true(*l_it), ++l_it) ; + if (!found) { + m_weighted_new_binaries = (float)0.001; + } + } + break; + } + if (is_false(c[0])) { + TRACE("sat", tout << "conflict " << l << ": " << c << "\n";); + set_conflict(); + *it2 = *it; + ++it2; + } + else { + TRACE("sat", tout << "propagating " << l << ": " << c << "\n";); + SASSERT(is_undef(c[0])); + DEBUG_CODE(for (unsigned i = 2; i < c.size(); ++i) { + SASSERT(is_false(c[i])); + }); + *it2 = *it; + it2++; + propagated(c[0]); + } + break; + } + case watched::EXT_CONSTRAINT: { + bool keep = true; + SASSERT(m_s.m_ext); + m_s.m_ext->propagate(l, it->get_ext_constraint_idx(), keep); + if (m_inconsistent) { + set_conflict(); + } + else if (keep) { + *it2 = *it; + it2++; + } + break; + } + default: + UNREACHABLE(); + break; + } + } + for (; it != end; ++it, ++it2) { + *it2 = *it; + } + wlist.set_end(it2); + } + + void lookahead::propagate_binary(literal l) { + literal_vector const& lits = m_binary[l.index()]; + TRACE("sat", tout << l << " => " << lits << "\n";); + unsigned sz = lits.size(); + for (unsigned i = 0; !inconsistent() && i < sz; ++i) { + assign(lits[i]); + } + } + + void lookahead::propagate() { + while (!inconsistent() && m_qhead < m_trail.size()) { + unsigned i = m_qhead; + unsigned sz = m_trail.size(); + for (; i < sz && !inconsistent(); ++i) { + literal l = m_trail[i]; + TRACE("sat", tout << "propagate " << l << " @ " << m_level << "\n";); + propagate_binary(l); + } + i = m_qhead; + for (; i < sz && !inconsistent(); ++i) { + propagate_clauses(m_trail[i]); + } + m_qhead = sz; + } + + TRACE("sat_verbose", display(tout << scope_lvl() << " " << (inconsistent()?"unsat":"sat") << "\n");); + } + + void lookahead::compute_wnb() { + init_wnb(); + TRACE("sat", display_lookahead(tout); ); + unsigned base = 2; + bool change = true; + bool first = true; + while (change && !inconsistent()) { + change = false; + for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) { + checkpoint(); + literal lit = m_lookahead[i].m_lit; + if (is_fixed_at(lit, c_fixed_truth)) continue; + unsigned level = base + m_lookahead[i].m_offset; + if (m_stamp[lit.var()] >= level) { + continue; + } + if (scope_lvl() == 1) { + IF_VERBOSE(3, verbose_stream() << scope_lvl() << " " << lit << " binary: " << m_binary_trail.size() << " trail: " << m_trail_lim.back() << "\n";); + } + TRACE("sat", tout << "lookahead: " << lit << " @ " << m_lookahead[i].m_offset << "\n";); + reset_wnb(lit); + push_lookahead1(lit, level); + if (!first) do_double(lit, base); + bool unsat = inconsistent(); + pop_lookahead1(lit); + if (unsat) { + TRACE("sat", tout << "backtracking and settting " << ~lit << "\n";); + reset_wnb(); + assign(~lit); + propagate(); + init_wnb(); + change = true; + } + else { + update_wnb(lit, level); + } + SASSERT(inconsistent() || !is_unsat()); + } + if (c_fixed_truth - 2 * m_lookahead.size() < base) { + break; + } + if (first && !change) { + first = false; + change = true; + } + reset_wnb(); + init_wnb(); + // base += 2 * m_lookahead.size(); + } + reset_wnb(); + TRACE("sat", display_lookahead(tout); ); + } + + void lookahead::init_wnb() { + TRACE("sat", tout << "init_wnb: " << m_qhead << "\n";); + m_qhead_lim.push_back(m_qhead); + m_trail_lim.push_back(m_trail.size()); + } + + void lookahead::reset_wnb() { + m_qhead = m_qhead_lim.back(); + TRACE("sat", tout << "reset_wnb: " << m_qhead << "\n";); + unsigned old_sz = m_trail_lim.back(); + for (unsigned i = old_sz; i < m_trail.size(); ++i) { + set_undef(m_trail[i]); + } + m_trail.shrink(old_sz); + m_trail_lim.pop_back(); + m_qhead_lim.pop_back(); + } + + literal lookahead::select_literal() { + literal l = null_literal; + float h = 0; + unsigned count = 1; + for (unsigned i = 0; i < m_lookahead.size(); ++i) { + literal lit = m_lookahead[i].m_lit; + if (lit.sign() || !is_undef(lit)) { + continue; + } + float diff1 = get_wnb(lit), diff2 = get_wnb(~lit); + float mixd = mix_diff(diff1, diff2); + + if (mixd == h) ++count; + if (mixd > h || (mixd == h && m_s.m_rand(count) == 0)) { + CTRACE("sat", l != null_literal, tout << lit << " mix diff: " << mixd << "\n";); + if (mixd > h) count = 1; + h = mixd; + l = diff1 < diff2 ? lit : ~lit; + } + } + // if (count > 1) std::cout << count << "\n"; + TRACE("sat", tout << "selected: " << l << "\n";); + return l; + } + + + void lookahead::reset_wnb(literal l) { + m_weighted_new_binaries = 0; + + // inherit propagation effect from parent. + literal p = get_parent(l); + set_wnb(l, p == null_literal ? 0 : get_wnb(p)); + } + + bool lookahead::check_autarky(literal l, unsigned level) { + return false; + // no propagations are allowed to reduce clauses. + clause_vector::const_iterator it = m_full_watches[l.index()].begin(); + clause_vector::const_iterator end = m_full_watches[l.index()].end(); + for (; it != end; ++it) { + clause& c = *(*it); + unsigned sz = c.size(); + bool found = false; + for (unsigned i = 0; !found && i < sz; ++i) { + found = is_true(c[i]); + if (found) { + TRACE("sat", tout << c[i] << " is true in " << c << "\n";); + } + } + IF_VERBOSE(2, verbose_stream() << "skip autarky " << l << "\n";); + if (!found) return false; + } + // + // bail out if there is a pending binary propagation. + // In general, we would have to check, recursively that + // a binary propagation does not create reduced clauses. + // + literal_vector const& lits = m_binary[l.index()]; + TRACE("sat", tout << l << ": " << lits << "\n";); + for (unsigned i = 0; i < lits.size(); ++i) { + literal l2 = lits[i]; + if (is_true(l2)) continue; + SASSERT(!is_false(l2)); + return false; + } + + return true; + } + + + void lookahead::update_wnb(literal l, unsigned level) { + if (m_weighted_new_binaries == 0) { + if (!check_autarky(l, level)) { + // skip + } + else if (get_wnb(l) == 0) { + ++m_stats.m_autarky_propagations; + IF_VERBOSE(1, verbose_stream() << "(sat.lookahead autarky " << l << ")\n";); + + TRACE("sat", tout << "autarky: " << l << " @ " << m_stamp[l.var()] + << " " + << (!m_binary[l.index()].empty() || !m_full_watches[l.index()].empty()) << "\n";); + reset_wnb(); + assign(l); + propagate(); + init_wnb(); + } + else { + ++m_stats.m_autarky_equivalences; + // l => p is known, but p => l is possibly not. + // add p => l. + // justification: any consequence of l + // that is not a consequence of p does not + // reduce the clauses. + literal p = get_parent(l); + SASSERT(p != null_literal); + if (m_stamp[p.var()] > m_stamp[l.var()]) { + TRACE("sat", tout << "equivalence " << l << " == " << p << "\n"; display(tout);); + IF_VERBOSE(1, verbose_stream() << "(sat.lookahead equivalence " << l << " == " << p << ")\n";); + add_binary(~l, p); + set_level(l, p); + } + } + } + else { + inc_wnb(l, m_weighted_new_binaries); + } + } + + void lookahead::do_double(literal l, unsigned& base) { + if (!inconsistent() && scope_lvl() > 1 && dl_enabled(l)) { + if (get_wnb(l) > m_delta_trigger) { + if (dl_no_overflow(base)) { + ++m_stats.m_double_lookahead_rounds; + double_look(l, base); + m_delta_trigger = get_wnb(l); + dl_disable(l); + } + } + else { + m_delta_trigger *= m_config.m_delta_rho; + } + } + } + + void lookahead::double_look(literal l, unsigned& base) { + SASSERT(!inconsistent()); + SASSERT(dl_no_overflow(base)); + unsigned dl_truth = base + 2 * m_lookahead.size() * (m_config.m_dl_max_iterations + 1); + scoped_level _sl(*this, dl_truth); + IF_VERBOSE(2, verbose_stream() << "double: " << l << "\n";); + init_wnb(); + assign(l); + propagate(); + bool change = true; + unsigned num_iterations = 0; + while (change && num_iterations < m_config.m_dl_max_iterations && !inconsistent()) { + change = false; + num_iterations++; + base += 2*m_lookahead.size(); + for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) { + literal lit = m_lookahead[i].m_lit; + if (is_fixed_at(lit, dl_truth)) continue; + if (push_lookahead2(lit, base + m_lookahead[i].m_offset)) { + TRACE("sat", tout << "unit: " << ~lit << "\n";); + ++m_stats.m_double_lookahead_propagations; + SASSERT(m_level == dl_truth); + reset_wnb(); + assign(~lit); + propagate(); + change = true; + init_wnb(); + } + } + SASSERT(dl_truth - 2 * m_lookahead.size() > base); + } + reset_wnb(); + SASSERT(m_level == dl_truth); + base = dl_truth; + } + + void lookahead::validate_assign(literal l) { + if (m_s.m_config.m_drat && m_search_mode == lookahead_mode::searching) { + m_assumptions.push_back(l); + m_drat.add(m_assumptions); + m_assumptions.pop_back(); + } + } + + void lookahead::assign(literal l) { + SASSERT(m_level > 0); + if (is_undef(l)) { + TRACE("sat", tout << "assign: " << l << " @ " << m_level << " " << m_trail_lim.size() << " " << m_search_mode << "\n";); + set_true(l); + m_trail.push_back(l); + if (m_search_mode == lookahead_mode::searching) { + m_stats.m_propagations++; + TRACE("sat", tout << "removing free var v" << l.var() << "\n";); + m_freevars.remove(l.var()); + validate_assign(l); + } + } + else if (is_false(l)) { + TRACE("sat", tout << "conflict: " << l << " @ " << m_level << " " << m_search_mode << "\n";); + SASSERT(!is_true(l)); + validate_assign(l); + set_conflict(); + } + } + + void lookahead::propagated(literal l) { + assign(l); + switch (m_search_mode) { + case lookahead_mode::searching: + break; + case lookahead_mode::lookahead1: + m_wstack.push_back(l); + break; + case lookahead_mode::lookahead2: + break; + } + } + + bool lookahead::backtrack(literal_vector& trail) { + while (inconsistent()) { + if (trail.empty()) return false; + pop(); + flip_prefix(); + assign(~trail.back()); + trail.pop_back(); + propagate(); + } + return true; + } + + lbool lookahead::search() { + m_model.reset(); + scoped_level _sl(*this, c_fixed_truth); + literal_vector trail; + m_search_mode = lookahead_mode::searching; + while (true) { + TRACE("sat", display(tout);); + inc_istamp(); + checkpoint(); + if (inconsistent()) { + if (!backtrack(trail)) return l_false; + continue; + } + literal l = choose(); + if (inconsistent()) { + if (!backtrack(trail)) return l_false; + continue; + } + if (l == null_literal) { + return l_true; + } + TRACE("sat", tout << "choose: " << l << " " << trail << "\n";); + ++m_stats.m_decisions; + IF_VERBOSE(1, verbose_stream() << "select " << pp_prefix(m_prefix, m_trail_lim.size()) << ": " << l << " " << m_trail.size() << "\n";); + push(l, c_fixed_truth); + trail.push_back(l); + SASSERT(inconsistent() || !is_unsat()); + } + } + + void lookahead::init_model() { + m_model.reset(); + for (unsigned i = 0; i < m_num_vars; ++i) { + lbool val; + literal lit(i, false); + if (is_undef(lit)) { + val = l_undef; + } + if (is_true(lit)) { + val = l_true; + } + else { + val = l_false; + } + m_model.push_back(val); + } + } + + std::ostream& lookahead::display_binary(std::ostream& out) const { + for (unsigned i = 0; i < m_binary.size(); ++i) { + literal_vector const& lits = m_binary[i]; + if (!lits.empty()) { + out << to_literal(i) << " -> " << lits << "\n"; + } + } + return out; + } + + std::ostream& lookahead::display_clauses(std::ostream& out) const { + for (unsigned i = 0; i < m_clauses.size(); ++i) { + out << *m_clauses[i] << "\n"; + } + return out; + } + + std::ostream& lookahead::display_values(std::ostream& out) const { + for (unsigned i = 0; i < m_trail.size(); ++i) { + literal l = m_trail[i]; + out << l << "\n"; + } + return out; + } + + std::ostream& lookahead::display_lookahead(std::ostream& out) const { + for (unsigned i = 0; i < m_lookahead.size(); ++i) { + literal lit = m_lookahead[i].m_lit; + unsigned offset = m_lookahead[i].m_offset; + out << lit << "\toffset: " << offset; + out << (is_undef(lit)?" undef": (is_true(lit) ? " true": " false")); + out << " wnb: " << get_wnb(lit); + out << "\n"; + } + return out; + } + + void lookahead::init_search() { + m_search_mode = lookahead_mode::searching; + scoped_level _sl(*this, c_fixed_truth); + init(); + } + + void lookahead::checkpoint() { + if (!m_rlimit.inc()) { + throw solver_exception(Z3_CANCELED_MSG); + } + if (memory::get_allocation_size() > m_s.m_config.m_max_memory) { + throw solver_exception(Z3_MAX_MEMORY_MSG); + } + } + + + + + literal lookahead::choose() { + literal l = null_literal; + while (l == null_literal) { + pre_select(); + if (m_lookahead.empty()) { + break; + } + compute_wnb(); + if (inconsistent()) { + break; + } + l = select_literal(); + } + SASSERT(inconsistent() || !is_unsat()); + return l; + } + + +} diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 6708e61f5..f1e78bf8f 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -64,6 +64,7 @@ namespace sat { reslimit m_rlimit; friend class ccc; + friend class card_extension; struct config { double m_dl_success; @@ -191,192 +192,55 @@ namespace sat { } }; + class scoped_ext { + lookahead& p; + public: + scoped_ext(lookahead& p); + ~scoped_ext(); + }; + // ------------------------------------- // prefix updates. I use low order bits. - void flip_prefix() { - if (m_trail_lim.size() < 64) { - uint64 mask = (1ull << m_trail_lim.size()); - m_prefix = mask | (m_prefix & (mask - 1)); - } - } - - void prune_prefix() { - if (m_trail_lim.size() < 64) { - m_prefix &= (1ull << m_trail_lim.size()) - 1; - } - } + void flip_prefix(); + void prune_prefix(); /** length < trail_lim.size: - mask m_prefix and p wrt length - update if different. */ - void update_prefix(literal l) { - bool_var x = l.var(); - unsigned p = m_vprefix[x].m_prefix; - unsigned pl = m_vprefix[x].m_length; - unsigned mask = (1 << std::min(31u, pl)) - 1; - if (pl >= m_trail_lim.size() || (p & mask) != (m_prefix & mask)) { - m_vprefix[x].m_length = m_trail_lim.size(); - m_vprefix[x].m_prefix = static_cast(m_prefix); - } - } + void update_prefix(literal l); - bool active_prefix(bool_var x) { - unsigned lvl = m_trail_lim.size(); - unsigned p = m_vprefix[x].m_prefix; - unsigned l = m_vprefix[x].m_length; - if (l > lvl) return false; - if (l == lvl || l >= 31) return m_prefix == p; - unsigned mask = ((1 << std::min(l,31u)) - 1); - return (m_prefix & mask) == (p & mask); - } + bool active_prefix(bool_var x); // ---------------------------------------- - void add_binary(literal l1, literal l2) { - TRACE("sat", tout << "binary: " << l1 << " " << l2 << "\n";); - SASSERT(l1 != l2); - // don't add tautologies and don't add already added binaries - if (~l1 == l2) return; - if (!m_binary[(~l1).index()].empty() && m_binary[(~l1).index()].back() == l2) return; - m_binary[(~l1).index()].push_back(l2); - m_binary[(~l2).index()].push_back(l1); - m_binary_trail.push_back((~l1).index()); - ++m_stats.m_add_binary; - if (m_s.m_config.m_drat) validate_binary(l1, l2); - } - - void del_binary(unsigned idx) { - // TRACE("sat", display(tout << "Delete " << to_literal(idx) << "\n");); - literal_vector & lits = m_binary[idx]; - SASSERT(!lits.empty()); - literal l = lits.back(); - lits.pop_back(); - SASSERT(!m_binary[(~l).index()].empty()); - IF_VERBOSE(0, if (m_binary[(~l).index()].back() != ~to_literal(idx)) verbose_stream() << "pop bad literal: " << idx << " " << (~l).index() << "\n";); - SASSERT(m_binary[(~l).index()].back() == ~to_literal(idx)); - m_binary[(~l).index()].pop_back(); - ++m_stats.m_del_binary; - } - - void validate_binary(literal l1, literal l2) { - if (m_search_mode == lookahead_mode::searching) { - m_assumptions.push_back(l1); - m_assumptions.push_back(l2); - m_drat.add(m_assumptions); - m_assumptions.pop_back(); - m_assumptions.pop_back(); - } - } + void add_binary(literal l1, literal l2); + void del_binary(unsigned idx); + void validate_binary(literal l1, literal l2); // ------------------------------------- // track consequences of binary clauses // see also 72 - 79 in sat11.w - void inc_bstamp() { - ++m_bstamp_id; - if (m_bstamp_id == 0) { - ++m_bstamp_id; - m_bstamp.fill(0); - } - } - void inc_istamp() { - ++m_istamp_id; - if (m_istamp_id == 0) { - ++m_istamp_id; - for (unsigned i = 0; i < m_lits.size(); ++i) { - m_lits[i].m_double_lookahead = 0; - } - } - } - void set_bstamp(literal l) { - m_bstamp[l.index()] = m_bstamp_id; - } - void set_bstamps(literal l) { - inc_bstamp(); - set_bstamp(l); - literal_vector const& conseq = m_binary[l.index()]; - literal_vector::const_iterator it = conseq.begin(); - literal_vector::const_iterator end = conseq.end(); - for (; it != end; ++it) { - set_bstamp(*it); - } - } + void inc_bstamp(); + void inc_istamp(); + void set_bstamp(literal l) { m_bstamp[l.index()] = m_bstamp_id; } + void set_bstamps(literal l); bool is_stamped(literal l) const { return m_bstamp[l.index()] == m_bstamp_id; } - - /** - \brief add one-step transitive closure of binary implications - return false if we learn a unit literal. - \pre all implicants of ~u are stamped. - u \/ v is true - **/ - - bool add_tc1(literal u, literal v) { - unsigned sz = m_binary[v.index()].size(); - for (unsigned i = 0; i < sz; ++i) { - literal w = m_binary[v.index()][i]; - // ~v \/ w - if (!is_fixed(w)) { - if (is_stamped(~w)) { - // u \/ v, ~v \/ w, u \/ ~w => u is unit - TRACE("sat", tout << "tc1: " << u << "\n";); - assign(u); - return false; - } - if (m_num_tc1 < m_config.m_tc1_limit) { - ++m_num_tc1; - IF_VERBOSE(3, verbose_stream() << "tc1: " << u << " " << w << "\n";); - add_binary(u, w); - } - } - } - return true; - } + bool add_tc1(literal u, literal v); /** \brief main routine for adding a new binary clause dynamically. */ - void try_add_binary(literal u, literal v) { - SASSERT(m_search_mode == lookahead_mode::searching); - SASSERT(u.var() != v.var()); - if (!is_undef(u) || !is_undef(v)) { - IF_VERBOSE(0, verbose_stream() << "adding assigned binary " << v << " " << u << "\n";); - } - set_bstamps(~u); - if (is_stamped(~v)) { - TRACE("sat", tout << "try_add_binary: " << u << "\n";); - assign(u); // u \/ ~v, u \/ v => u is a unit literal - } - else if (!is_stamped(v) && add_tc1(u, v)) { - // u \/ v is not in index - set_bstamps(~v); - if (is_stamped(~u)) { - TRACE("sat", tout << "try_add_binary: " << v << "\n";); - assign(v); // v \/ ~u, u \/ v => v is a unit literal - } - else if (add_tc1(v, u)) { - update_prefix(u); - update_prefix(v); - add_binary(u, v); - } - } - } + void try_add_binary(literal u, literal v); // ------------------------------------- // pre-selection // see also 91 - 102 sat11.w - void pre_select() { - m_lookahead.reset(); - if (select(scope_lvl())) { - get_scc(); - if (inconsistent()) return; - find_heights(); - construct_lookahead_table(); - } - } + void pre_select(); struct candidate { bool_var m_var; @@ -388,244 +252,16 @@ namespace sat { float get_rating(bool_var v) const { return m_rating[v]; } float get_rating(literal l) const { return get_rating(l.var()); } - - bool select(unsigned level) { - init_pre_selection(level); - unsigned level_cand = std::max(m_config.m_level_cand, m_freevars.size() / 50); - unsigned max_num_cand = level == 0 ? m_freevars.size() : level_cand / level; - max_num_cand = std::max(m_config.m_min_cutoff, max_num_cand); - - float sum = 0; - for (bool newbies = false; ; newbies = true) { - sum = init_candidates(level, newbies); - if (!m_candidates.empty()) break; - if (is_sat()) { - return false; - } - if (newbies) { - enable_trace("sat"); - TRACE("sat", display(tout);); - TRACE("sat", tout << sum << "\n";); - } - } - SASSERT(!m_candidates.empty()); - // cut number of candidates down to max_num_cand. - // step 1. cut it to at most 2*max_num_cand. - // step 2. use a heap to sift through the rest. - bool progress = true; - while (progress && m_candidates.size() >= max_num_cand * 2) { - progress = false; - float mean = sum / (float)(m_candidates.size() + 0.0001); - sum = 0; - for (unsigned i = 0; i < m_candidates.size() && m_candidates.size() >= max_num_cand * 2; ++i) { - if (m_candidates[i].m_rating >= mean) { - sum += m_candidates[i].m_rating; - } - else { - m_candidates[i] = m_candidates.back(); - m_candidates.pop_back(); - --i; - progress = true; - } - } - } - TRACE("sat", display_candidates(tout);); - SASSERT(!m_candidates.empty()); - if (m_candidates.size() > max_num_cand) { - unsigned j = m_candidates.size()/2; - while (j > 0) { - --j; - sift_up(j); - } - while (true) { - m_candidates[0] = m_candidates.back(); - m_candidates.pop_back(); - if (m_candidates.size() == max_num_cand) break; - sift_up(0); - } - } - SASSERT(!m_candidates.empty() && m_candidates.size() <= max_num_cand); - TRACE("sat", display_candidates(tout);); - return true; - } - - void sift_up(unsigned j) { - unsigned i = j; - candidate c = m_candidates[j]; - for (unsigned k = 2*j + 1; k < m_candidates.size(); i = k, k = 2*k + 1) { - // pick largest parent - if (k + 1 < m_candidates.size() && m_candidates[k].m_rating < m_candidates[k+1].m_rating) { - ++k; - } - if (c.m_rating <= m_candidates[k].m_rating) break; - m_candidates[i] = m_candidates[k]; - } - if (i > j) m_candidates[i] = c; - } - - float init_candidates(unsigned level, bool newbies) { - m_candidates.reset(); - float sum = 0; - for (bool_var const* it = m_freevars.begin(), * end = m_freevars.end(); it != end; ++it) { - SASSERT(is_undef(*it)); - bool_var x = *it; - if (!m_select_lookahead_vars.empty() && m_select_lookahead_vars.contains(x)) { - m_candidates.push_back(candidate(x, m_rating[x])); - sum += m_rating[x]; - } - else if (newbies || active_prefix(x)) { - m_candidates.push_back(candidate(x, m_rating[x])); - sum += m_rating[x]; - } - } - TRACE("sat", display_candidates(tout << "sum: " << sum << "\n");); - return sum; - } - - std::ostream& display_candidates(std::ostream& out) const { - for (unsigned i = 0; i < m_candidates.size(); ++i) { - out << "var: " << m_candidates[i].m_var << " rating: " << m_candidates[i].m_rating << "\n"; - } - return out; - } - - bool is_unsat() const { - for (unsigned i = 0; i < m_clauses.size(); ++i) { - clause& c = *m_clauses[i]; - unsigned j = 0; - for (; j < c.size() && is_false(c[j]); ++j) {} - if (j == c.size()) { - TRACE("sat", tout << c << "\n";); - TRACE("sat", display(tout);); - return true; - } - } - return false; - } - - bool is_sat() const { - for (bool_var const* it = m_freevars.begin(), * end = m_freevars.end(); it != end; ++it) { - literal l(*it, false); - literal_vector const& lits1 = m_binary[l.index()]; - for (unsigned i = 0; i < lits1.size(); ++i) { - if (!is_true(lits1[i])) { - TRACE("sat", tout << l << " " << lits1[i] << "\n";); - return false; - } - } - l.neg(); - literal_vector const& lits2 = m_binary[l.index()]; - for (unsigned i = 0; i < lits2.size(); ++i) { - if (!is_true(lits2[i])) { - TRACE("sat", tout << l << " " << lits2[i] << "\n";); - return false; - } - } - } - for (unsigned i = 0; i < m_clauses.size(); ++i) { - clause& c = *m_clauses[i]; - unsigned j = 0; - for (; j < c.size() && !is_true(c[j]); ++j) {} - if (j == c.size()) { - return false; - } - } - return true; - } - - void init_pre_selection(unsigned level) { - unsigned max_level = m_config.m_max_hlevel; - if (level <= 1) { - ensure_H(2); - h_scores(m_H[0], m_H[1]); - for (unsigned j = 0; j < 2; ++j) { - for (unsigned i = 0; i < 2; ++i) { - h_scores(m_H[i + 1], m_H[(i + 2) % 3]); - } - } - m_heur = &m_H[1]; - } - else if (level < max_level) { - ensure_H(level); - h_scores(m_H[level-1], m_H[level]); - m_heur = &m_H[level]; - } - else { - ensure_H(max_level); - h_scores(m_H[max_level-1], m_H[max_level]); - m_heur = &m_H[max_level]; - } - } - - void ensure_H(unsigned level) { - while (m_H.size() <= level) { - m_H.push_back(svector()); - m_H.back().resize(m_num_vars * 2, 0); - } - } - - void h_scores(svector& h, svector& hp) { - float sum = 0; - for (bool_var const* it = m_freevars.begin(), * end = m_freevars.end(); it != end; ++it) { - literal l(*it, false); - sum += h[l.index()] + h[(~l).index()]; - } - float factor = 2 * m_freevars.size() / sum; - float sqfactor = factor * factor; - float afactor = factor * m_config.m_alpha; - for (bool_var const* it = m_freevars.begin(), * end = m_freevars.end(); it != end; ++it) { - literal l(*it, false); - float pos = l_score(l, h, factor, sqfactor, afactor); - float neg = l_score(~l, h, factor, sqfactor, afactor); - hp[l.index()] = pos; - hp[(~l).index()] = neg; - m_rating[l.var()] = pos * neg; - } - } - - float l_score(literal l, svector const& h, float factor, float sqfactor, float afactor) { - float sum = 0, tsum = 0; - literal_vector::iterator it = m_binary[l.index()].begin(), end = m_binary[l.index()].end(); - for (; it != end; ++it) { - bool_var v = it->var(); - if (it->index() >= h.size()) - IF_VERBOSE(0, verbose_stream() << l << " " << *it << " " << h.size() << "\n";); - if (is_undef(*it)) sum += h[it->index()]; - // if (m_freevars.contains(it->var())) sum += h[it->index()]; - } - watch_list& wlist = m_watches[l.index()]; - watch_list::iterator wit = wlist.begin(), wend = wlist.end(); - for (; wit != wend; ++wit) { - switch (wit->get_kind()) { - case watched::BINARY: - UNREACHABLE(); - break; - case watched::TERNARY: { - literal l1 = wit->get_literal1(); - literal l2 = wit->get_literal2(); - // if (is_undef(l1) && is_undef(l2)) - tsum += h[l1.index()] * h[l2.index()]; - break; - } - case watched::CLAUSE: { - clause_offset cls_off = wit->get_clause_offset(); - clause & c = *(m_cls_allocator.get_clause(cls_off)); - // approximation compared to ternary clause case: - // we pick two other literals from the clause. - if (c[0] == ~l) { - tsum += h[c[1].index()] * h[c[2].index()]; - } - else { - SASSERT(c[1] == ~l); - tsum += h[c[0].index()] * h[c[2].index()]; - } - break; - } - } - } - sum = (float)(0.1 + afactor*sum + sqfactor*tsum); - return std::min(m_config.m_max_score, sum); - } + bool select(unsigned level); + void sift_up(unsigned j); + float init_candidates(unsigned level, bool newbies); + std::ostream& display_candidates(std::ostream& out) const; + bool is_unsat() const; + bool is_sat() const; + void init_pre_selection(unsigned level); + void ensure_H(unsigned level); + void h_scores(svector& h, svector& hp); + float l_score(literal l, svector const& h, float factor, float sqfactor, float afactor); // ------------------------------------ // Implication graph @@ -664,51 +300,10 @@ namespace sat { literal m_settled; vector m_dfs; - void get_scc() { - unsigned num_candidates = m_candidates.size(); - init_scc(); - for (unsigned i = 0; i < num_candidates && !inconsistent(); ++i) { - literal lit(m_candidates[i].m_var, false); - if (get_rank(lit) == 0) get_scc(lit); - if (get_rank(~lit) == 0) get_scc(~lit); - } - TRACE("sat", display_scc(tout);); - } - void init_scc() { - inc_bstamp(); - for (unsigned i = 0; i < m_candidates.size(); ++i) { - literal lit(m_candidates[i].m_var, false); - init_dfs_info(lit); - init_dfs_info(~lit); - } - for (unsigned i = 0; i < m_candidates.size(); ++i) { - literal lit(m_candidates[i].m_var, false); - init_arcs(lit); - init_arcs(~lit); - } - m_rank = 0; - m_active = null_literal; - m_settled = null_literal; - TRACE("sat", display_dfs(tout);); - } - void init_dfs_info(literal l) { - unsigned idx = l.index(); - m_dfs[idx].reset(); - set_bstamp(l); - } - // arcs are added in the opposite direction of implications. - // So for implications l => u we add arcs u -> l - void init_arcs(literal l) { - literal_vector const& succ = m_binary[l.index()]; - for (unsigned i = 0; i < succ.size(); ++i) { - literal u = succ[i]; - SASSERT(u != l); - if (u.index() > l.index() && is_stamped(u)) { - add_arc(~l, ~u); - add_arc( u, l); - } - } - } + void get_scc(); + void init_scc(); + void init_dfs_info(literal l); + void init_arcs(literal l); void add_arc(literal u, literal v) { m_dfs[u.index()].m_next.push_back(v); } bool has_arc(literal v) const { return m_dfs[v.index()].m_next.size() > m_dfs[v.index()].m_nextp; } arcs get_arcs(literal v) const { return m_dfs[v.index()].m_next; } @@ -727,115 +322,13 @@ namespace sat { void set_height(literal v, unsigned h) { m_dfs[v.index()].m_height = h; } void set_parent(literal v, literal p) { TRACE("scc", tout << v << " <- " << p << "\n";); m_dfs[v.index()].m_parent = p; } void set_vcomp(literal v, literal u) { m_dfs[v.index()].m_vcomp = u; } - void get_scc(literal v) { - TRACE("scc", tout << v << "\n";); - set_parent(v, null_literal); - activate_scc(v); - do { - literal ll = get_min(v); - if (has_arc(v)) { - literal u = pop_arc(v); - unsigned r = get_rank(u); - if (r > 0) { - // u was processed before ll - if (r < get_rank(ll)) set_min(v, u); - } - else { - // process u in dfs order, add v to dfs stack for u - set_parent(u, v); - v = u; - activate_scc(v); - } - } - else { - literal u = get_parent(v); - if (v == ll) { - found_scc(v); - } - else if (get_rank(ll) < get_rank(get_min(u))) { - set_min(u, ll); - } - // walk back in the dfs stack - v = u; - } - } - while (v != null_literal && !inconsistent()); - } - void activate_scc(literal l) { - SASSERT(get_rank(l) == 0); - set_rank(l, ++m_rank); - set_link(l, m_active); - set_min(l, l); - m_active = l; - } - // make v root of the scc equivalence class - // set vcomp to be the highest rated literal - void found_scc(literal v) { - literal t = m_active; - m_active = get_link(v); - literal best = v; - float best_rating = get_rating(v); - set_rank(v, UINT_MAX); - set_link(v, m_settled); m_settled = t; - while (t != v) { - if (t == ~v) { - TRACE("sat", display_scc(tout << "found contradiction during scc search\n");); - set_conflict(); - break; - } - set_rank(t, UINT_MAX); - set_parent(t, v); - float t_rating = get_rating(t); - if (t_rating > best_rating) { - best = t; - best_rating = t_rating; - } - t = get_link(t); - } - set_parent(v, v); - set_vcomp(v, best); - if (get_rank(~v) == UINT_MAX) { - set_vcomp(v, ~get_vcomp(get_parent(~v))); - } - } - - std::ostream& display_dfs(std::ostream& out) const { - for (unsigned i = 0; i < m_candidates.size(); ++i) { - literal l(m_candidates[i].m_var, false); - display_dfs(out, l); - display_dfs(out, ~l); - } - return out; - } - - std::ostream& display_dfs(std::ostream& out, literal l) const { - arcs const& a1 = get_arcs(l); - if (!a1.empty()) { - out << l << " -> " << a1 << "\n"; - } - return out; - } - - std::ostream& display_scc(std::ostream& out) const { - display_dfs(out); - for (unsigned i = 0; i < m_candidates.size(); ++i) { - literal l(m_candidates[i].m_var, false); - display_scc(out, l); - display_scc(out, ~l); - } - return out; - } - - std::ostream& display_scc(std::ostream& out, literal l) const { - out << l << " := " << get_parent(l) - << " min: " << get_min(l) - << " rank: " << get_rank(l) - << " height: " << get_height(l) - << " link: " << get_link(l) - << " child: " << get_child(l) - << " vcomp: " << get_vcomp(l) << "\n"; - return out; - } + void get_scc(literal v); + void activate_scc(literal l); + void found_scc(literal v); + std::ostream& display_dfs(std::ostream& out) const; + std::ostream& display_dfs(std::ostream& out, literal l) const; + std::ostream& display_scc(std::ostream& out) const; + std::ostream& display_scc(std::ostream& out, literal l) const; // ------------------------------------ @@ -844,86 +337,10 @@ namespace sat { literal m_root_child; - literal get_child(literal u) const { - if (u == null_literal) return m_root_child; - return m_dfs[u.index()].m_min; - } - void set_child(literal v, literal u) { - if (v == null_literal) m_root_child = u; - else m_dfs[v.index()].m_min = u; - } - - /* - \brief Assign heights to the nodes. - Nodes within the same strongly connected component are given the same height. - The code assumes that m_settled is topologically sorted such that - 1. nodes in the same equivalence class come together - 2. the equivalence class representative is last - - */ - void find_heights() { - m_root_child = null_literal; - literal pp = null_literal; - unsigned h = 0; - literal w, uu; - TRACE("sat", - for (literal u = m_settled; u != null_literal; u = get_link(u)) { - tout << u << " "; - } - tout << "\n";); - for (literal u = m_settled; u != null_literal; u = uu) { - TRACE("sat", tout << "process: " << u << "\n";); - uu = get_link(u); - literal p = get_parent(u); - if (p != pp) { - // new equivalence class - h = 0; - w = null_literal; - pp = p; - } - // traverse nodes in order of implication - unsigned sz = num_next(~u); - for (unsigned j = 0; j < sz; ++j) { - literal v = ~get_next(~u, j); - TRACE("sat", tout << "child " << v << " link: " << get_link(v) << "\n";); - literal pv = get_parent(v); - // skip nodes in same equivalence, they will all be processed - if (pv == p) continue; - unsigned hh = get_height(pv); - // update the maximal height descendant - if (hh >= h) { - h = hh + 1; - w = pv; - } - } - if (p == u) { - // u is an equivalence class representative - // it is processed last - literal v = get_child(w); - set_height(u, h); - set_child(u, null_literal); - set_link(u, v); - set_child(w, u); - TRACE("sat", tout << "child(" << w << ") = " << u << " link(" << u << ") = " << v << "\n";); - } - } - TRACE("sat", - display_forest(tout << "forest: ", get_child(null_literal)); - tout << "\n"; - display_scc(tout); ); - } - std::ostream& display_forest(std::ostream& out, literal l) { - for (literal u = l; u != null_literal; u = get_link(u)) { - out << u << " "; - l = get_child(u); - if (l != null_literal) { - out << "("; - display_forest(out, l); - out << ") "; - } - } - return out; - } + literal get_child(literal u) const; + void set_child(literal v, literal u); + void find_heights(); + std::ostream& display_forest(std::ostream& out, literal l); struct literal_offset { literal m_lit; @@ -931,696 +348,55 @@ namespace sat { literal_offset(literal l): m_lit(l), m_offset(0) {} }; svector m_lookahead; - void set_offset(unsigned idx, unsigned offset) { - m_lookahead[idx].m_offset = offset; - } - void set_lookahead(literal l) { - m_lookahead.push_back(literal_offset(l)); - } - void construct_lookahead_table() { - literal u = get_child(null_literal), v = null_literal; - unsigned offset = 0; - SASSERT(m_lookahead.empty()); - while (u != null_literal) { - set_rank(u, m_lookahead.size()); - set_lookahead(get_vcomp(u)); - if (null_literal != get_child(u)) { - set_parent(u, v); - v = u; - u = get_child(u); - } - else { - while (true) { - set_offset(get_rank(u), offset); - offset += 2; - set_parent(u, v == null_literal ? v : get_vcomp(v)); - u = get_link(u); - if (u == null_literal && v != null_literal) { - u = v; - v = get_parent(u); - } - else { - break; - } - } - } - } - SASSERT(2*m_lookahead.size() == offset); - TRACE("sat", for (unsigned i = 0; i < m_lookahead.size(); ++i) - tout << m_lookahead[i].m_lit << " : " << m_lookahead[i].m_offset << "\n";); - } + void set_offset(unsigned idx, unsigned offset) { m_lookahead[idx].m_offset = offset; } + void set_lookahead(literal l) { m_lookahead.push_back(literal_offset(l)); } + void construct_lookahead_table(); // ------------------------------------ // clause management - void attach_clause(clause& c) { - if (c.size() == 3) { - attach_ternary(c[0], c[1], c[2]); - } - else { - literal block_lit = c[c.size() >> 2]; - clause_offset cls_off = m_cls_allocator.get_offset(&c); - m_watches[(~c[0]).index()].push_back(watched(block_lit, cls_off)); - m_watches[(~c[1]).index()].push_back(watched(block_lit, cls_off)); - SASSERT(is_undef(c[0])); - SASSERT(is_undef(c[1])); - } - } - - void detach_clause(clause& c) { - clause_offset cls_off = m_cls_allocator.get_offset(&c); - m_retired_clauses.push_back(&c); - erase_clause_watch(get_wlist(~c[0]), cls_off); - erase_clause_watch(get_wlist(~c[1]), cls_off); - } - - void del_clauses() { - clause * const* end = m_clauses.end(); - clause * const * it = m_clauses.begin(); - for (; it != end; ++it) { - m_cls_allocator.del_clause(*it); - } - } - - void detach_ternary(literal l1, literal l2, literal l3) { - ++m_stats.m_del_ternary; - m_retired_ternary.push_back(ternary(l1, l2, l3)); - // implicitly erased: erase_ternary_watch(get_wlist(~l1), l2, l3); - erase_ternary_watch(get_wlist(~l2), l1, l3); - erase_ternary_watch(get_wlist(~l3), l1, l2); - } - - void attach_ternary(ternary const& t) { - attach_ternary(t.m_u, t.m_v, t.m_w); - } - - void attach_ternary(literal l1, literal l2, literal l3) { - ++m_stats.m_add_ternary; - TRACE("sat", tout << l1 << " " << l2 << " " << l3 << "\n";); - m_watches[(~l1).index()].push_back(watched(l2, l3)); - m_watches[(~l2).index()].push_back(watched(l1, l3)); - m_watches[(~l3).index()].push_back(watched(l1, l2)); - } - + void attach_clause(clause& c); + void detach_clause(clause& c); + void del_clauses(); + void detach_ternary(literal l1, literal l2, literal l3); + void attach_ternary(ternary const& t); + void attach_ternary(literal l1, literal l2, literal l3); watch_list& get_wlist(literal l) { return m_watches[l.index()]; } // ------------------------------------ // initialization - void init_var(bool_var v) { - m_binary.push_back(literal_vector()); - m_binary.push_back(literal_vector()); - m_watches.push_back(watch_list()); - m_watches.push_back(watch_list()); - m_full_watches.push_back(clause_vector()); - m_full_watches.push_back(clause_vector()); - m_bstamp.push_back(0); - m_bstamp.push_back(0); - m_stamp.push_back(0); - m_dfs.push_back(dfs_info()); - m_dfs.push_back(dfs_info()); - m_lits.push_back(lit_info()); - m_lits.push_back(lit_info()); - m_rating.push_back(0); - m_vprefix.push_back(prefix()); - if (!m_s.was_eliminated(v)) - m_freevars.insert(v); - } - - void init() { - m_delta_trigger = m_num_vars/10; - m_config.m_dl_success = 0.8; - m_inconsistent = false; - m_qhead = 0; - m_bstamp_id = 0; - - for (unsigned i = 0; i < m_num_vars; ++i) { - init_var(i); - } - - // copy binary clauses - unsigned sz = m_s.m_watches.size(); - for (unsigned l_idx = 0; l_idx < sz; ++l_idx) { - literal l = ~to_literal(l_idx); - watch_list const & wlist = m_s.m_watches[l_idx]; - watch_list::const_iterator it = wlist.begin(); - watch_list::const_iterator end = wlist.end(); - for (; it != end; ++it) { - if (!it->is_binary_non_learned_clause()) - continue; - literal l2 = it->get_literal(); - SASSERT(!m_s.was_eliminated(l.var())); - SASSERT(!m_s.was_eliminated(l2.var())); - if (l.index() < l2.index()) - add_binary(l, l2); - } - } - - copy_clauses(m_s.m_clauses); - copy_clauses(m_s.m_learned); - - // copy units - unsigned trail_sz = m_s.init_trail_size(); - for (unsigned i = 0; i < trail_sz; ++i) { - literal l = m_s.m_trail[i]; - if (!m_s.was_eliminated(l.var())) { - if (m_s.m_config.m_drat) m_drat.add(l, false); - assign(l); - } - } - propagate(); - m_qhead = m_trail.size(); - TRACE("sat", m_s.display(tout); display(tout);); - } - - void copy_clauses(clause_vector const& clauses) { - // copy clauses - clause_vector::const_iterator it = clauses.begin(); - clause_vector::const_iterator end = clauses.end(); - for (; it != end; ++it) { - clause& c = *(*it); - if (c.was_removed()) continue; - clause* c1 = m_cls_allocator.mk_clause(c.size(), c.begin(), false); - m_clauses.push_back(c1); - attach_clause(*c1); - for (unsigned i = 0; i < c.size(); ++i) { - m_full_watches[(~c[i]).index()].push_back(c1); - SASSERT(!m_s.was_eliminated(c[i].var())); - } - if (m_s.m_config.m_drat) m_drat.add(c, false); - } - } + void init_var(bool_var v); + void init(); + void copy_clauses(clause_vector const& clauses); // ------------------------------------ // search - void push(literal lit, unsigned level) { - SASSERT(m_search_mode == lookahead_mode::searching); - m_binary_trail_lim.push_back(m_binary_trail.size()); - m_trail_lim.push_back(m_trail.size()); - m_num_tc1_lim.push_back(m_num_tc1); - m_retired_clause_lim.push_back(m_retired_clauses.size()); - m_retired_ternary_lim.push_back(m_retired_ternary.size()); - m_qhead_lim.push_back(m_qhead); - scoped_level _sl(*this, level); - m_assumptions.push_back(~lit); - assign(lit); - propagate(); - } - - void pop() { - if (m_assumptions.empty()) IF_VERBOSE(0, verbose_stream() << "empty pop\n";); - m_assumptions.pop_back(); - m_inconsistent = false; - SASSERT(m_search_mode == lookahead_mode::searching); - - // m_freevars only for main search - // undo assignments - unsigned old_sz = m_trail_lim.back(); - for (unsigned i = m_trail.size(); i > old_sz; ) { - --i; - literal l = m_trail[i]; - set_undef(l); - TRACE("sat", tout << "inserting free var v" << l.var() << "\n";); - m_freevars.insert(l.var()); - } - m_trail.shrink(old_sz); // reset assignment. - m_trail_lim.pop_back(); - - m_num_tc1 = m_num_tc1_lim.back(); - m_num_tc1_lim.pop_back(); - - // unretire clauses - old_sz = m_retired_clause_lim.back(); - for (unsigned i = old_sz; i < m_retired_clauses.size(); ++i) { - attach_clause(*m_retired_clauses[i]); - } - m_retired_clauses.resize(old_sz); - m_retired_clause_lim.pop_back(); - - old_sz = m_retired_ternary_lim.back(); - for (unsigned i = old_sz; i < m_retired_ternary.size(); ++i) { - attach_ternary(m_retired_ternary[i]); - } - m_retired_ternary.shrink(old_sz); - m_retired_ternary_lim.pop_back(); - - // remove local binary clauses - old_sz = m_binary_trail_lim.back(); - for (unsigned i = m_binary_trail.size(); i > old_sz; ) { - del_binary(m_binary_trail[--i]); - } - m_binary_trail.shrink(old_sz); - m_binary_trail_lim.pop_back(); - - // reset propagation queue - m_qhead = m_qhead_lim.back(); - m_qhead_lim.pop_back(); - } - - bool push_lookahead2(literal lit, unsigned level) { - scoped_level _sl(*this, level); - SASSERT(m_search_mode == lookahead_mode::lookahead1); - m_search_mode = lookahead_mode::lookahead2; - assign(lit); - propagate(); - bool unsat = inconsistent(); - SASSERT(m_search_mode == lookahead_mode::lookahead2); - m_search_mode = lookahead_mode::lookahead1; - m_inconsistent = false; - return unsat; - } - - void push_lookahead1(literal lit, unsigned level) { - SASSERT(m_search_mode == lookahead_mode::searching); - m_search_mode = lookahead_mode::lookahead1; - scoped_level _sl(*this, level); - assign(lit); - propagate(); - } - - void pop_lookahead1(literal lit) { - bool unsat = inconsistent(); - SASSERT(m_search_mode == lookahead_mode::lookahead1); - m_inconsistent = false; - m_search_mode = lookahead_mode::searching; - // convert windfalls to binary clauses. - if (!unsat) { - literal nlit = ~lit; - - for (unsigned i = 0; i < m_wstack.size(); ++i) { - literal l2 = m_wstack[i]; - //update_prefix(~lit); - //update_prefix(m_wstack[i]); - TRACE("sat", tout << "windfall: " << nlit << " " << l2 << "\n";); - // if we use try_add_binary, then this may produce new assignments - // these assignments get put on m_trail, and they are cleared by - // reset_wnb. We would need to distinguish the trail that comes - // from lookahead levels and the main search level for this to work. - add_binary(nlit, l2); - } - m_stats.m_windfall_binaries += m_wstack.size(); - } - m_wstack.reset(); - } - + void push(literal lit, unsigned level); + void pop(); + bool push_lookahead2(literal lit, unsigned level); + void push_lookahead1(literal lit, unsigned level); + void pop_lookahead1(literal lit); float mix_diff(float l, float r) const { return l + r + (1 << 10) * l * r; } - - clause const& get_clause(watch_list::iterator it) const { - clause_offset cls_off = it->get_clause_offset(); - return *(m_cls_allocator.get_clause(cls_off)); - } - - bool is_nary_propagation(clause const& c, literal l) const { - bool r = c.size() > 2 && ((c[0] == l && is_false(c[1])) || (c[1] == l && is_false(c[0]))); - DEBUG_CODE(if (r) for (unsigned j = 2; j < c.size(); ++j) SASSERT(is_false(c[j]));); - return r; - } - - // - // The current version is modeled after CDCL SAT solving data-structures. - // It borrows from the watch list data-structure. The cost tradeoffs are somewhat - // biased towards CDCL search overheads. - // If we walk over the positive occurrences of l, then those clauses can be retired so - // that they don't interfere with calculation of H. Instead of removing clauses from the watch - // list one can swap them to the "back" and adjust a size indicator of the watch list - // Only the size indicator needs to be updated on backtracking. - // - void propagate_clauses(literal l) { - SASSERT(is_true(l)); - if (inconsistent()) return; - watch_list& wlist = m_watches[l.index()]; - watch_list::iterator it = wlist.begin(), it2 = it, end = wlist.end(); - for (; it != end && !inconsistent(); ++it) { - switch (it->get_kind()) { - case watched::BINARY: - UNREACHABLE(); - break; - case watched::TERNARY: { - literal l1 = it->get_literal1(); - literal l2 = it->get_literal2(); - bool skip = false; - if (is_fixed(l1)) { - if (is_false(l1)) { - if (is_undef(l2)) { - propagated(l2); - } - else if (is_false(l2)) { - TRACE("sat", tout << l1 << " " << l2 << " " << l << "\n";); - set_conflict(); - } - } - else { - // retire this clause - } - } - else if (is_fixed(l2)) { - if (is_false(l2)) { - propagated(l1); - } - else { - // retire this clause - } - } - else { - switch (m_search_mode) { - case lookahead_mode::searching: - detach_ternary(~l, l1, l2); - try_add_binary(l1, l2); - skip = true; - break; - case lookahead_mode::lookahead1: - m_weighted_new_binaries += (*m_heur)[l1.index()] * (*m_heur)[l2.index()]; - break; - case lookahead2: - break; - } - } - if (!skip) { - *it2 = *it; - it2++; - } - break; - } - case watched::CLAUSE: { - if (is_true(it->get_blocked_literal())) { - *it2 = *it; - ++it2; - break; - } - clause_offset cls_off = it->get_clause_offset(); - clause & c = *(m_cls_allocator.get_clause(cls_off)); - if (c[0] == ~l) - std::swap(c[0], c[1]); - if (is_true(c[0])) { - it->set_blocked_literal(c[0]); - *it2 = *it; - it2++; - break; - } - literal * l_it = c.begin() + 2; - literal * l_end = c.end(); - bool found = false; - for (; l_it != l_end && !found; ++l_it) { - if (!is_false(*l_it)) { - found = true; - c[1] = *l_it; - *l_it = ~l; - m_watches[(~c[1]).index()].push_back(watched(c[0], cls_off)); - TRACE("sat_verbose", tout << "move watch from " << l << " to " << c[1] << " for clause " << c << "\n";); - } - } - if (found) { - found = false; - for (; l_it != l_end && !found; ++l_it) { - found = !is_false(*l_it); - } - // normal clause was converted to a binary clause. - if (!found && is_undef(c[1]) && is_undef(c[0])) { - TRACE("sat", tout << "got binary " << l << ": " << c << "\n";); - switch (m_search_mode) { - case lookahead_mode::searching: - detach_clause(c); - try_add_binary(c[0], c[1]); - break; - case lookahead_mode::lookahead1: - m_weighted_new_binaries += (*m_heur)[c[0].index()]* (*m_heur)[c[1].index()]; - break; - case lookahead_mode::lookahead2: - break; - } - } - else if (found && m_search_mode == lookahead_mode::lookahead1 && m_weighted_new_binaries == 0) { - // leave a trail that some clause was reduced but potentially not an autarky - l_it = c.begin() + 2; - found = false; - for (; l_it != l_end && !found; found = is_true(*l_it), ++l_it) ; - if (!found) { - m_weighted_new_binaries = (float)0.001; - } - } - break; - } - if (is_false(c[0])) { - TRACE("sat", tout << "conflict " << l << ": " << c << "\n";); - set_conflict(); - *it2 = *it; - ++it2; - } - else { - TRACE("sat", tout << "propagating " << l << ": " << c << "\n";); - SASSERT(is_undef(c[0])); - DEBUG_CODE(for (unsigned i = 2; i < c.size(); ++i) { - SASSERT(is_false(c[i])); - }); - *it2 = *it; - it2++; - propagated(c[0]); - } - break; - } - case watched::EXT_CONSTRAINT: - UNREACHABLE(); - break; - default: - UNREACHABLE(); - break; - } - } - for (; it != end; ++it, ++it2) { - *it2 = *it; - } - wlist.set_end(it2); - } - - void propagate_binary(literal l) { - literal_vector const& lits = m_binary[l.index()]; - TRACE("sat", tout << l << " => " << lits << "\n";); - unsigned sz = lits.size(); - for (unsigned i = 0; !inconsistent() && i < sz; ++i) { - assign(lits[i]); - } - } - - void propagate() { - while (!inconsistent() && m_qhead < m_trail.size()) { - unsigned i = m_qhead; - unsigned sz = m_trail.size(); - for (; i < sz && !inconsistent(); ++i) { - literal l = m_trail[i]; - TRACE("sat", tout << "propagate " << l << " @ " << m_level << "\n";); - propagate_binary(l); - } - i = m_qhead; - for (; i < sz && !inconsistent(); ++i) { - propagate_clauses(m_trail[i]); - } - m_qhead = sz; - } - - TRACE("sat_verbose", display(tout << scope_lvl() << " " << (inconsistent()?"unsat":"sat") << "\n");); - } - - literal choose() { - literal l = null_literal; - while (l == null_literal) { - pre_select(); - if (m_lookahead.empty()) { - break; - } - compute_wnb(); - if (inconsistent()) { - break; - } - l = select_literal(); - } - SASSERT(inconsistent() || !is_unsat()); - return l; - } - - void compute_wnb() { - init_wnb(); - TRACE("sat", display_lookahead(tout); ); - unsigned base = 2; - bool change = true; - bool first = true; - while (change && !inconsistent()) { - change = false; - for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) { - checkpoint(); - literal lit = m_lookahead[i].m_lit; - if (is_fixed_at(lit, c_fixed_truth)) continue; - unsigned level = base + m_lookahead[i].m_offset; - if (m_stamp[lit.var()] >= level) { - continue; - } - if (scope_lvl() == 1) { - IF_VERBOSE(3, verbose_stream() << scope_lvl() << " " << lit << " binary: " << m_binary_trail.size() << " trail: " << m_trail_lim.back() << "\n";); - } - TRACE("sat", tout << "lookahead: " << lit << " @ " << m_lookahead[i].m_offset << "\n";); - reset_wnb(lit); - push_lookahead1(lit, level); - if (!first) do_double(lit, base); - bool unsat = inconsistent(); - pop_lookahead1(lit); - if (unsat) { - TRACE("sat", tout << "backtracking and settting " << ~lit << "\n";); - reset_wnb(); - assign(~lit); - propagate(); - init_wnb(); - change = true; - } - else { - update_wnb(lit, level); - } - SASSERT(inconsistent() || !is_unsat()); - } - if (c_fixed_truth - 2 * m_lookahead.size() < base) { - break; - } - if (first && !change) { - first = false; - change = true; - } - reset_wnb(); - init_wnb(); - // base += 2 * m_lookahead.size(); - } - reset_wnb(); - TRACE("sat", display_lookahead(tout); ); - } - - void init_wnb() { - TRACE("sat", tout << "init_wnb: " << m_qhead << "\n";); - m_qhead_lim.push_back(m_qhead); - m_trail_lim.push_back(m_trail.size()); - } - - void reset_wnb() { - m_qhead = m_qhead_lim.back(); - TRACE("sat", tout << "reset_wnb: " << m_qhead << "\n";); - unsigned old_sz = m_trail_lim.back(); - for (unsigned i = old_sz; i < m_trail.size(); ++i) { - set_undef(m_trail[i]); - } - m_trail.shrink(old_sz); - m_trail_lim.pop_back(); - m_qhead_lim.pop_back(); - } - - literal select_literal() { - literal l = null_literal; - float h = 0; - unsigned count = 1; - for (unsigned i = 0; i < m_lookahead.size(); ++i) { - literal lit = m_lookahead[i].m_lit; - if (lit.sign() || !is_undef(lit)) { - continue; - } - float diff1 = get_wnb(lit), diff2 = get_wnb(~lit); - float mixd = mix_diff(diff1, diff2); - - if (mixd == h) ++count; - if (mixd > h || (mixd == h && m_s.m_rand(count) == 0)) { - CTRACE("sat", l != null_literal, tout << lit << " mix diff: " << mixd << "\n";); - if (mixd > h) count = 1; - h = mixd; - l = diff1 < diff2 ? lit : ~lit; - } - } -// if (count > 1) std::cout << count << "\n"; - TRACE("sat", tout << "selected: " << l << "\n";); - return l; - } - + clause const& get_clause(watch_list::iterator it) const; + bool is_nary_propagation(clause const& c, literal l) const; + void propagate_clauses(literal l); + void propagate_binary(literal l); + void propagate(); + literal choose(); + void compute_wnb(); + void init_wnb(); + void reset_wnb(); + literal select_literal(); void set_wnb(literal l, float f) { m_lits[l.index()].m_wnb = f; } void inc_wnb(literal l, float f) { m_lits[l.index()].m_wnb += f; } float get_wnb(literal l) const { return m_lits[l.index()].m_wnb; } - void reset_wnb(literal l) { - m_weighted_new_binaries = 0; - - // inherit propagation effect from parent. - literal p = get_parent(l); - set_wnb(l, p == null_literal ? 0 : get_wnb(p)); - } - - bool check_autarky(literal l, unsigned level) { - return false; - // no propagations are allowed to reduce clauses. - clause_vector::const_iterator it = m_full_watches[l.index()].begin(); - clause_vector::const_iterator end = m_full_watches[l.index()].end(); - for (; it != end; ++it) { - clause& c = *(*it); - unsigned sz = c.size(); - bool found = false; - for (unsigned i = 0; !found && i < sz; ++i) { - found = is_true(c[i]); - if (found) { - TRACE("sat", tout << c[i] << " is true in " << c << "\n";); - } - } - IF_VERBOSE(2, verbose_stream() << "skip autarky " << l << "\n";); - if (!found) return false; - } - // - // bail out if there is a pending binary propagation. - // In general, we would have to check, recursively that - // a binary propagation does not create reduced clauses. - // - literal_vector const& lits = m_binary[l.index()]; - TRACE("sat", tout << l << ": " << lits << "\n";); - for (unsigned i = 0; i < lits.size(); ++i) { - literal l2 = lits[i]; - if (is_true(l2)) continue; - SASSERT(!is_false(l2)); - return false; - } - - return true; - } - - void update_wnb(literal l, unsigned level) { - if (m_weighted_new_binaries == 0) { - if (!check_autarky(l, level)) { - // skip - } - else if (get_wnb(l) == 0) { - ++m_stats.m_autarky_propagations; - IF_VERBOSE(1, verbose_stream() << "(sat.lookahead autarky " << l << ")\n";); - - TRACE("sat", tout << "autarky: " << l << " @ " << m_stamp[l.var()] - << " " - << (!m_binary[l.index()].empty() || !m_full_watches[l.index()].empty()) << "\n";); - reset_wnb(); - assign(l); - propagate(); - init_wnb(); - } - else { - ++m_stats.m_autarky_equivalences; - // l => p is known, but p => l is possibly not. - // add p => l. - // justification: any consequence of l - // that is not a consequence of p does not - // reduce the clauses. - literal p = get_parent(l); - SASSERT(p != null_literal); - if (m_stamp[p.var()] > m_stamp[l.var()]) { - TRACE("sat", tout << "equivalence " << l << " == " << p << "\n"; display(tout);); - IF_VERBOSE(1, verbose_stream() << "(sat.lookahead equivalence " << l << " == " << p << ")\n";); - add_binary(~l, p); - set_level(l, p); - } - } - } - else { - inc_wnb(l, m_weighted_new_binaries); - } - } - + void reset_wnb(literal l); + bool check_autarky(literal l, unsigned level); + void update_wnb(literal l, unsigned level); bool dl_enabled(literal l) const { return m_lits[l.index()].m_double_lookahead != m_istamp_id; } void dl_disable(literal l) { m_lits[l.index()].m_double_lookahead = m_istamp_id; } bool dl_no_overflow(unsigned base) const { return base + 2 * m_lookahead.size() * static_cast(m_config.m_dl_max_iterations + 1) < c_fixed_truth; } @@ -1629,217 +405,25 @@ namespace sat { return is_fixed(lit) && (!is_false(lit) || m_stamp[lit.var()] >= level); } - void do_double(literal l, unsigned& base) { - if (!inconsistent() && scope_lvl() > 1 && dl_enabled(l)) { - if (get_wnb(l) > m_delta_trigger) { - if (dl_no_overflow(base)) { - ++m_stats.m_double_lookahead_rounds; - double_look(l, base); - m_delta_trigger = get_wnb(l); - dl_disable(l); - } - } - else { - m_delta_trigger *= m_config.m_delta_rho; - } - } - } - - void double_look(literal l, unsigned& base) { - SASSERT(!inconsistent()); - SASSERT(dl_no_overflow(base)); - unsigned dl_truth = base + 2 * m_lookahead.size() * (m_config.m_dl_max_iterations + 1); - scoped_level _sl(*this, dl_truth); - IF_VERBOSE(2, verbose_stream() << "double: " << l << "\n";); - init_wnb(); - assign(l); - propagate(); - bool change = true; - unsigned num_iterations = 0; - while (change && num_iterations < m_config.m_dl_max_iterations && !inconsistent()) { - change = false; - num_iterations++; - base += 2*m_lookahead.size(); - for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) { - literal lit = m_lookahead[i].m_lit; - if (is_fixed_at(lit, dl_truth)) continue; - if (push_lookahead2(lit, base + m_lookahead[i].m_offset)) { - TRACE("sat", tout << "unit: " << ~lit << "\n";); - ++m_stats.m_double_lookahead_propagations; - SASSERT(m_level == dl_truth); - reset_wnb(); - assign(~lit); - propagate(); - change = true; - init_wnb(); - } - } - SASSERT(dl_truth - 2 * m_lookahead.size() > base); - } - reset_wnb(); - SASSERT(m_level == dl_truth); - base = dl_truth; - } - + void do_double(literal l, unsigned& base); + void double_look(literal l, unsigned& base); void set_conflict() { TRACE("sat", tout << "conflict\n";); m_inconsistent = true; } bool inconsistent() { return m_inconsistent; } unsigned scope_lvl() const { return m_trail_lim.size(); } - void validate_assign(literal l) { - if (m_s.m_config.m_drat && m_search_mode == lookahead_mode::searching) { - m_assumptions.push_back(l); - m_drat.add(m_assumptions); - m_assumptions.pop_back(); - } - } - - void assign(literal l) { - SASSERT(m_level > 0); - if (is_undef(l)) { - TRACE("sat", tout << "assign: " << l << " @ " << m_level << " " << m_trail_lim.size() << " " << m_search_mode << "\n";); - set_true(l); - m_trail.push_back(l); - if (m_search_mode == lookahead_mode::searching) { - m_stats.m_propagations++; - TRACE("sat", tout << "removing free var v" << l.var() << "\n";); - m_freevars.remove(l.var()); - validate_assign(l); - } - } - else if (is_false(l)) { - TRACE("sat", tout << "conflict: " << l << " @ " << m_level << " " << m_search_mode << "\n";); - SASSERT(!is_true(l)); - validate_assign(l); - set_conflict(); - } - } - - void propagated(literal l) { - assign(l); - switch (m_search_mode) { - case lookahead_mode::searching: - break; - case lookahead_mode::lookahead1: - m_wstack.push_back(l); - break; - case lookahead_mode::lookahead2: - break; - } - } - - bool backtrack(literal_vector& trail) { - while (inconsistent()) { - if (trail.empty()) return false; - pop(); - flip_prefix(); - assign(~trail.back()); - trail.pop_back(); - propagate(); - } - return true; - } - - lbool search() { - m_model.reset(); - scoped_level _sl(*this, c_fixed_truth); - literal_vector trail; - m_search_mode = lookahead_mode::searching; - while (true) { - TRACE("sat", display(tout);); - inc_istamp(); - checkpoint(); - if (inconsistent()) { - if (!backtrack(trail)) return l_false; - continue; - } - literal l = choose(); - if (inconsistent()) { - if (!backtrack(trail)) return l_false; - continue; - } - if (l == null_literal) { - return l_true; - } - TRACE("sat", tout << "choose: " << l << " " << trail << "\n";); - ++m_stats.m_decisions; - IF_VERBOSE(1, verbose_stream() << "select " << pp_prefix(m_prefix, m_trail_lim.size()) << ": " << l << " " << m_trail.size() << "\n";); - push(l, c_fixed_truth); - trail.push_back(l); - SASSERT(inconsistent() || !is_unsat()); - } - } - - void init_model() { - m_model.reset(); - for (unsigned i = 0; i < m_num_vars; ++i) { - lbool val; - literal lit(i, false); - if (is_undef(lit)) { - val = l_undef; - } - if (is_true(lit)) { - val = l_true; - } - else { - val = l_false; - } - m_model.push_back(val); - } - } - - std::ostream& display_binary(std::ostream& out) const { - for (unsigned i = 0; i < m_binary.size(); ++i) { - literal_vector const& lits = m_binary[i]; - if (!lits.empty()) { - out << to_literal(i) << " -> " << lits << "\n"; - } - } - return out; - } - - std::ostream& display_clauses(std::ostream& out) const { - for (unsigned i = 0; i < m_clauses.size(); ++i) { - out << *m_clauses[i] << "\n"; - } - return out; - } - - std::ostream& display_values(std::ostream& out) const { - for (unsigned i = 0; i < m_trail.size(); ++i) { - literal l = m_trail[i]; - out << l << "\n"; - } - return out; - } - - std::ostream& display_lookahead(std::ostream& out) const { - for (unsigned i = 0; i < m_lookahead.size(); ++i) { - literal lit = m_lookahead[i].m_lit; - unsigned offset = m_lookahead[i].m_offset; - out << lit << "\toffset: " << offset; - out << (is_undef(lit)?" undef": (is_true(lit) ? " true": " false")); - out << " wnb: " << get_wnb(lit); - out << "\n"; - } - return out; - } - - void init_search() { - m_search_mode = lookahead_mode::searching; - scoped_level _sl(*this, c_fixed_truth); - init(); - } - - void checkpoint() { - if (!m_rlimit.inc()) { - throw solver_exception(Z3_CANCELED_MSG); - } - if (memory::get_allocation_size() > m_s.m_config.m_max_memory) { - throw solver_exception(Z3_MAX_MEMORY_MSG); - } - } - + void validate_assign(literal l); + void assign(literal l); + void propagated(literal l); + bool backtrack(literal_vector& trail); + lbool search(); + void init_model(); + std::ostream& display_binary(std::ostream& out) const; + std::ostream& display_clauses(std::ostream& out) const; + std::ostream& display_values(std::ostream& out) const; + std::ostream& display_lookahead(std::ostream& out) const; + void init_search(); + void checkpoint(); public: lookahead(solver& s) : @@ -1857,12 +441,14 @@ namespace sat { m_s.rlimit().pop_child(); } + lbool check() { init_search(); return search(); } literal select_lookahead(bool_var_vector const& vars) { + scoped_ext _sext(*this); m_search_mode = lookahead_mode::searching; scoped_level _sl(*this, c_fixed_truth); init(); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index e45373b5c..1f8f3aa19 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -779,14 +779,14 @@ namespace sat { case watched::EXT_CONSTRAINT: SASSERT(m_ext); m_ext->propagate(l, it->get_ext_constraint_idx(), keep); - if (keep) { - *it2 = *it; - it2++; - } if (m_inconsistent) { CONFLICT_CLEANUP(); return false; } + if (keep) { + *it2 = *it; + it2++; + } break; default: UNREACHABLE(); diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h index 0ea82c6ac..977799366 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -124,6 +124,7 @@ namespace sat { }; class solver; + class lookahead; class clause; class clause_wrapper; class integrity_checker; diff --git a/src/sat/sat_watched.h b/src/sat/sat_watched.h index 03eaf2798..254dba5b6 100644 --- a/src/sat/sat_watched.h +++ b/src/sat/sat_watched.h @@ -103,7 +103,7 @@ namespace sat { } bool is_ext_constraint() const { return get_kind() == EXT_CONSTRAINT; } - ext_constraint_idx get_ext_constraint_idx() const { SASSERT(is_ext_constraint()); return m_val2; } + ext_constraint_idx get_ext_constraint_idx() const { SASSERT(is_ext_constraint()); return m_val1; } bool operator==(watched const & w) const { return m_val1 == w.m_val1 && m_val2 == w.m_val2; } bool operator!=(watched const & w) const { return !operator==(w); }