From 74824ac901622096bf90996fd46aa188b823b80b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 15 Jan 2022 09:35:25 -0800 Subject: [PATCH] #5753 get_antecedent has to be well-founded. It got broken when using eval during propagation and egraph explain during conflict resolution. --- .../arith_internalize.cpp | 697 --- .../pb_solver.cpp | 3806 ----------------- src/sat/smt/euf_solver.cpp | 6 +- src/sat/smt/euf_solver.h | 4 +- src/sat/smt/q_clause.h | 17 +- src/sat/smt/q_ematch.cpp | 37 +- src/sat/smt/q_ematch.h | 3 +- src/sat/smt/q_eval.cpp | 15 - src/sat/smt/q_eval.h | 1 - src/sat/smt/q_mam.cpp | 14 +- 10 files changed, 53 insertions(+), 4547 deletions(-) delete mode 100644 enc_temp_folder/7df563538829fc9a7856736edcf0b3/arith_internalize.cpp delete mode 100644 enc_temp_folder/e6c4896a12a9fc61d88ea292bf2dca16/pb_solver.cpp diff --git a/enc_temp_folder/7df563538829fc9a7856736edcf0b3/arith_internalize.cpp b/enc_temp_folder/7df563538829fc9a7856736edcf0b3/arith_internalize.cpp deleted file mode 100644 index 0665c6195..000000000 --- a/enc_temp_folder/7df563538829fc9a7856736edcf0b3/arith_internalize.cpp +++ /dev/null @@ -1,697 +0,0 @@ -/*++ -Copyright (c) 2020 Microsoft Corporation - -Module Name: - - arith_internalize.cpp - -Abstract: - - Theory plugin for arithmetic - -Author: - - Nikolaj Bjorner (nbjorner) 2020-09-08 - ---*/ - -#include "sat/smt/euf_solver.h" -#include "sat/smt/arith_solver.h" - -namespace arith { - - sat::literal solver::internalize(expr* e, bool sign, bool root, bool learned) { - init_internalize(); - flet _is_learned(m_is_redundant, learned); - internalize_atom(e); - literal lit = ctx.expr2literal(e); - if (sign) - lit.neg(); - return lit; - } - - void solver::internalize(expr* e, bool redundant) { - init_internalize(); - flet _is_learned(m_is_redundant, redundant); - if (m.is_bool(e)) - internalize_atom(e); - else - internalize_term(e); - } - - void solver::init_internalize() { - force_push(); - // initialize 0, 1 variables: - - if (!m_internalize_initialized) { - get_one(true); - get_one(false); - get_zero(true); - get_zero(false); - ctx.push(value_trail(m_internalize_initialized)); - m_internalize_initialized = true; - } - } - - lpvar solver::get_one(bool is_int) { - return add_const(1, is_int ? m_one_var : m_rone_var, is_int); - } - - lpvar solver::get_zero(bool is_int) { - return add_const(0, is_int ? m_zero_var : m_rzero_var, is_int); - } - - void solver::ensure_nla() { - if (!m_nla) { - m_nla = alloc(nla::solver, *m_solver.get(), m.limit()); - for (auto const& _s : m_scopes) { - (void)_s; - m_nla->push(); - } - smt_params_helper prms(s().params()); - m_nla->settings().run_order() = prms.arith_nl_order(); - m_nla->settings().run_tangents() = prms.arith_nl_tangents(); - m_nla->settings().run_horner() = prms.arith_nl_horner(); - m_nla->settings().horner_subs_fixed() = prms.arith_nl_horner_subs_fixed(); - m_nla->settings().horner_frequency() = prms.arith_nl_horner_frequency(); - m_nla->settings().horner_row_length_limit() = prms.arith_nl_horner_row_length_limit(); - m_nla->settings().run_grobner() = prms.arith_nl_grobner(); - m_nla->settings().run_nra() = prms.arith_nl_nra(); - m_nla->settings().grobner_subs_fixed() = prms.arith_nl_grobner_subs_fixed(); - m_nla->settings().grobner_eqs_growth() = prms.arith_nl_grobner_eqs_growth(); - m_nla->settings().grobner_expr_size_growth() = prms.arith_nl_grobner_expr_size_growth(); - m_nla->settings().grobner_expr_degree_growth() = prms.arith_nl_grobner_expr_degree_growth(); - m_nla->settings().grobner_max_simplified() = prms.arith_nl_grobner_max_simplified(); - m_nla->settings().grobner_number_of_conflicts_to_report() = prms.arith_nl_grobner_cnfl_to_report(); - m_nla->settings().grobner_quota() = prms.arith_nl_gr_q(); - m_nla->settings().grobner_frequency() = prms.arith_nl_grobner_frequency(); - m_nla->settings().expensive_patching() = prms.arith_nl_expp(); - } - } - - void solver::found_unsupported(expr* n) { - ctx.push(value_trail(m_not_handled)); - TRACE("arith", tout << "unsupported " << mk_pp(n, m) << "\n";); - m_not_handled = n; - } - - void solver::found_underspecified(expr* n) { - if (a.is_underspecified(n)) { - TRACE("arith", tout << "Unhandled: " << mk_pp(n, m) << "\n";); - m_underspecified.push_back(to_app(n)); - } - expr* e = nullptr, * x = nullptr, * y = nullptr; - if (a.is_div(n, x, y)) { - e = a.mk_div0(x, y); - } - else if (a.is_idiv(n, x, y)) { - e = a.mk_idiv0(x, y); - } - else if (a.is_rem(n, x, y)) { - e = a.mk_rem0(x, y); - } - else if (a.is_mod(n, x, y)) { - e = a.mk_mod0(x, y); - } - else if (a.is_power(n, x, y)) { - e = a.mk_power0(x, y); - } - if (e) { - literal lit = eq_internalize(n, e); - add_unit(lit); - } - } - - lpvar solver::add_const(int c, lpvar& var, bool is_int) { - if (var != UINT_MAX) { - return var; - } - ctx.push(value_trail(var)); - app_ref cnst(a.mk_numeral(rational(c), is_int), m); - mk_enode(cnst); - theory_var v = mk_evar(cnst); - var = lp().add_var(v, is_int); - add_def_constraint_and_equality(var, lp::GE, rational(c)); - add_def_constraint_and_equality(var, lp::LE, rational(c)); - TRACE("arith", tout << "add " << cnst << ", var = " << var << "\n";); - return var; - } - - lpvar solver::register_theory_var_in_lar_solver(theory_var v) { - lpvar lpv = lp().external_to_local(v); - if (lpv != lp::null_lpvar) - return lpv; - return lp().add_var(v, is_int(v)); - } - - void solver::linearize_term(expr* term, scoped_internalize_state& st) { - st.push(term, rational::one()); - linearize(st); - } - - void solver::linearize_ineq(expr* lhs, expr* rhs, scoped_internalize_state& st) { - st.push(lhs, rational::one()); - st.push(rhs, rational::minus_one()); - linearize(st); - } - - void solver::linearize(scoped_internalize_state& st) { - expr_ref_vector& terms = st.terms(); - svector& vars = st.vars(); - vector& coeffs = st.coeffs(); - rational& offset = st.offset(); - rational r; - expr* n1, * n2; - unsigned index = 0; - while (index < terms.size()) { - SASSERT(index >= vars.size()); - expr* n = terms.get(index); - st.to_ensure_enode().push_back(n); - if (a.is_add(n)) { - for (expr* arg : *to_app(n)) { - st.push(arg, coeffs[index]); - } - st.set_back(index); - } - else if (a.is_sub(n)) { - unsigned sz = to_app(n)->get_num_args(); - terms[index] = to_app(n)->get_arg(0); - for (unsigned i = 1; i < sz; ++i) { - st.push(to_app(n)->get_arg(i), -coeffs[index]); - } - } - else if (a.is_mul(n, n1, n2) && a.is_extended_numeral(n1, r)) { - coeffs[index] *= r; - terms[index] = n2; - st.to_ensure_enode().push_back(n1); - } - else if (a.is_mul(n, n1, n2) && a.is_extended_numeral(n2, r)) { - coeffs[index] *= r; - terms[index] = n1; - st.to_ensure_enode().push_back(n2); - } - else if (a.is_mul(n)) { - theory_var v = internalize_mul(to_app(n)); - coeffs[vars.size()] = coeffs[index]; - vars.push_back(v); - ++index; - } - else if (a.is_power(n, n1, n2) && is_app(n1) && a.is_extended_numeral(n2, r) && r.is_unsigned() && r <= 10) { - theory_var v = internalize_power(to_app(n), to_app(n1), r.get_unsigned()); - coeffs[vars.size()] = coeffs[index]; - vars.push_back(v); - ++index; - } - else if (a.is_numeral(n, r)) { - offset += coeffs[index] * r; - ++index; - } - else if (a.is_uminus(n, n1)) { - coeffs[index].neg(); - terms[index] = n1; - } - else if (a.is_to_real(n, n1)) { - terms[index] = n1; - if (!ctx.get_enode(n)) { - app* t = to_app(n); - VERIFY(internalize_term(to_app(n1))); - mk_enode(t); - theory_var v = mk_evar(n); - theory_var w = mk_evar(n1); - lpvar vj = register_theory_var_in_lar_solver(v); - lpvar wj = register_theory_var_in_lar_solver(w); - auto lu_constraints = lp().add_equality(vj, wj); - add_def_constraint(lu_constraints.first); - add_def_constraint(lu_constraints.second); - } - } - else if (is_app(n) && a.get_family_id() == to_app(n)->get_family_id()) { - bool is_first = nullptr == ctx.get_enode(n); - app* t = to_app(n); - internalize_args(t); - mk_enode(t); - theory_var v = mk_evar(n); - coeffs[vars.size()] = coeffs[index]; - vars.push_back(v); - ++index; - if (!is_first) { - // skip recursive internalization - } - else if (a.is_to_int(n, n1)) - mk_to_int_axiom(t); - else if (a.is_abs(n)) - mk_abs_axiom(t); - else if (a.is_idiv(n, n1, n2)) { - if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n); - m_idiv_terms.push_back(n); - app_ref mod(a.mk_mod(n1, n2), m); - internalize(mod, m_is_redundant); - st.to_ensure_var().push_back(n1); - st.to_ensure_var().push_back(n2); - } - else if (a.is_mod(n, n1, n2)) { - if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n); - mk_idiv_mod_axioms(n1, n2); - st.to_ensure_var().push_back(n1); - st.to_ensure_var().push_back(n2); - } - else if (a.is_rem(n, n1, n2)) { - if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n); - mk_rem_axiom(n1, n2); - st.to_ensure_var().push_back(n1); - st.to_ensure_var().push_back(n2); - } - else if (a.is_div(n, n1, n2)) { - if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n); - mk_div_axiom(n1, n2); - st.to_ensure_var().push_back(n1); - st.to_ensure_var().push_back(n2); - } - else if (!a.is_div0(n) && !a.is_mod0(n) && !a.is_idiv0(n) && !a.is_rem0(n) && !a.is_power0(n)) { - found_unsupported(n); - } - else { - // no-op - } - } - else { - if (is_app(n)) { - internalize_args(to_app(n)); - for (expr* arg : *to_app(n)) - if ((a.is_real(arg) || a.is_int(arg)) && !m.is_bool(arg)) - internalize_term(arg); - } - theory_var v = mk_evar(n); - coeffs[vars.size()] = coeffs[index]; - vars.push_back(v); - ++index; - } - } - for (unsigned i = st.to_ensure_enode().size(); i-- > 0; ) { - expr* n = st.to_ensure_enode()[i]; - if (is_app(n)) { - mk_enode(to_app(n)); - } - } - st.to_ensure_enode().reset(); - for (unsigned i = st.to_ensure_var().size(); i-- > 0; ) { - expr* n = st.to_ensure_var()[i]; - if (is_app(n)) - internalize_term(to_app(n)); - } - st.to_ensure_var().reset(); - } - - void solver::eq_internalized(enode* n) { - internalize_term(n->get_arg(0)->get_expr()); - internalize_term(n->get_arg(1)->get_expr()); - } - - bool solver::internalize_atom(expr* atom) { - TRACE("arith", tout << mk_pp(atom, m) << "\n";); - expr* n1, *n2; - rational r; - lp_api::bound_kind k; - theory_var v = euf::null_theory_var; - bool_var bv = ctx.get_si().add_bool_var(atom); - m_bool_var2bound.erase(bv); - literal lit(bv, false); - ctx.attach_lit(lit, atom); - - if (a.is_le(atom, n1, n2) && a.is_extended_numeral(n2, r)) { - v = internalize_def(n1); - k = lp_api::upper_t; - } - else if (a.is_ge(atom, n1, n2) && a.is_extended_numeral(n2, r)) { - v = internalize_def(n1); - k = lp_api::lower_t; - } - else if (a.is_le(atom, n1, n2) && a.is_extended_numeral(n1, r)) { - v = internalize_def(n2); - k = lp_api::lower_t; - } - else if (a.is_ge(atom, n1, n2) && a.is_extended_numeral(n1, r)) { - v = internalize_def(n2); - k = lp_api::upper_t; - } - else if (a.is_le(atom, n1, n2)) { - expr_ref n3(a.mk_sub(n1, n2), m); - v = internalize_def(n3); - k = lp_api::upper_t; - r = 0; - } - else if (a.is_ge(atom, n1, n2)) { - expr_ref n3(a.mk_sub(n1, n2), m); - v = internalize_def(n3); - k = lp_api::lower_t; - r = 0; - } - else if (a.is_lt(atom, n1, n2)) { - expr_ref n3(a.mk_sub(n1, n2), m); - v = internalize_def(n3); - k = lp_api::lower_t; - r = 0; - lit.neg(); - } - else if (a.is_gt(atom, n1, n2)) { - expr_ref n3(a.mk_sub(n1, n2), m); - v = internalize_def(n3); - k = lp_api::upper_t; - r = 0; - lit.neg(); - } - else if (a.is_is_int(atom)) { - mk_is_int_axiom(atom); - return true; - } - else { - TRACE("arith", tout << "Could not internalize " << mk_pp(atom, m) << "\n";); - found_unsupported(atom); - return true; - } - - enode* n = ctx.get_enode(atom); - theory_var w = mk_var(n); - ctx.attach_th_var(n, this, w); - ctx.get_egraph().set_merge_enabled(n, false); - if (is_int(v) && !r.is_int()) - r = (k == lp_api::upper_t) ? floor(r) : ceil(r); - api_bound* b = mk_var_bound(lit, v, k, r); - m_bounds[v].push_back(b); - updt_unassigned_bounds(v, +1); - m_bounds_trail.push_back(v); - m_bool_var2bound.insert(bv, b); - TRACE("arith_verbose", tout << "Internalized " << lit << ": " << mk_pp(atom, m) << " " << *b << "\n";); - m_new_bounds.push_back(b); - //add_use_lists(b); - return true; - } - - bool solver::internalize_term(expr* term) { - if (!has_var(term)) - register_theory_var_in_lar_solver(internalize_def(term)); - return true; - } - - theory_var solver::internalize_def(expr* term, scoped_internalize_state& st) { - TRACE("arith", tout << expr_ref(term, m) << "\n";); - if (ctx.get_enode(term)) - return mk_evar(term); - - linearize_term(term, st); - if (is_unit_var(st)) - return st.vars()[0]; - - theory_var v = mk_evar(term); - SASSERT(euf::null_theory_var != v); - st.coeffs().resize(st.vars().size() + 1); - st.coeffs()[st.vars().size()] = rational::minus_one(); - st.vars().push_back(v); - return v; - } - - // term - v = 0 - theory_var solver::internalize_def(expr* term) { - scoped_internalize_state st(*this); - linearize_term(term, st); - return internalize_linearized_def(term, st); - } - - void solver::internalize_args(app* t, bool force) { - SASSERT(!m.is_bool(t)); - TRACE("arith", tout << mk_pp(t, m) << " " << force << " " << reflect(t) << "\n";); - if (!force && !reflect(t)) - return; - for (expr* arg : *t) - e_internalize(arg); - } - - theory_var solver::internalize_power(app* t, app* n, unsigned p) { - internalize_args(t, true); - bool _has_var = has_var(t); - mk_enode(t); - theory_var v = mk_evar(t); - if (_has_var) - return v; - internalize_term(n); - theory_var w = mk_evar(n); - - if (p == 0) { - mk_power0_axioms(t, n); - } - else { - svector vars; - for (unsigned i = 0; i < p; ++i) - vars.push_back(register_theory_var_in_lar_solver(w)); - ensure_nla(); - m_solver->register_existing_terms(); - m_nla->add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.data()); - } - return v; - } - - theory_var solver::internalize_mul(app* t) { - SASSERT(a.is_mul(t)); - internalize_args(t, true); - bool _has_var = has_var(t); - mk_enode(t); - theory_var v = mk_evar(t); - - if (!_has_var) { - svector vars; - for (expr* n : *t) { - if (is_app(n)) VERIFY(internalize_term(to_app(n))); - SASSERT(ctx.get_enode(n)); - theory_var v = mk_evar(n); - vars.push_back(register_theory_var_in_lar_solver(v)); - } - TRACE("arith", tout << "v" << v << " := " << mk_pp(t, m) << "\n" << vars << "\n";); - m_solver->register_existing_terms(); - ensure_nla(); - m_nla->add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.data()); - } - return v; - } - - theory_var solver::internalize_linearized_def(expr* term, scoped_internalize_state& st) { - theory_var v = mk_evar(term); - TRACE("arith", tout << mk_bounded_pp(term, m) << " v" << v << "\n";); - - if (is_unit_var(st) && v == st.vars()[0]) { - return st.vars()[0]; - } - else if (is_one(st) && a.is_numeral(term)) { - return lp().local_to_external(get_one(a.is_int(term))); - } - else if (is_zero(st) && a.is_numeral(term)) { - return lp().local_to_external(get_zero(a.is_int(term))); - } - else { - init_left_side(st); - lpvar vi = get_lpvar(v); - if (vi == UINT_MAX) { - if (m_left_side.empty()) { - vi = lp().add_var(v, a.is_int(term)); - add_def_constraint_and_equality(vi, lp::GE, st.offset()); - add_def_constraint_and_equality(vi, lp::LE, st.offset()); - register_fixed_var(v, st.offset()); - return v; - } - if (!st.offset().is_zero()) { - m_left_side.push_back(std::make_pair(st.offset(), get_one(a.is_int(term)))); - } - if (m_left_side.empty()) { - vi = lp().add_var(v, a.is_int(term)); - add_def_constraint_and_equality(vi, lp::GE, rational(0)); - add_def_constraint_and_equality(vi, lp::LE, rational(0)); - } - else { - vi = lp().add_term(m_left_side, v); - SASSERT(lp::tv::is_term(vi)); - TRACE("arith_verbose", - tout << "v" << v << " := " << mk_pp(term, m) - << " slack: " << vi << " scopes: " << m_scopes.size() << "\n"; - lp().print_term(lp().get_term(lp::tv::raw(vi)), tout) << "\n";); - } - } - return v; - } - } - - bool solver::is_unit_var(scoped_internalize_state& st) { - return st.offset().is_zero() && st.vars().size() == 1 && st.coeffs()[0].is_one(); - } - - bool solver::is_one(scoped_internalize_state& st) { - return st.offset().is_one() && st.vars().empty(); - } - - bool solver::is_zero(scoped_internalize_state& st) { - return st.offset().is_zero() && st.vars().empty(); - } - - void solver::init_left_side(scoped_internalize_state& st) { - SASSERT(all_zeros(m_columns)); - svector const& vars = st.vars(); - vector const& coeffs = st.coeffs(); - for (unsigned i = 0; i < vars.size(); ++i) { - theory_var var = vars[i]; - rational const& coeff = coeffs[i]; - if (m_columns.size() <= static_cast(var)) { - m_columns.setx(var, coeff, rational::zero()); - } - else { - m_columns[var] += coeff; - } - } - m_left_side.clear(); - // reset the coefficients after they have been used. - for (theory_var var : vars) { - rational const& r = m_columns[var]; - if (!r.is_zero()) { - auto vi = register_theory_var_in_lar_solver(var); - if (lp::tv::is_term(vi)) - vi = lp().map_term_index_to_column_index(vi); - m_left_side.push_back(std::make_pair(r, vi)); - m_columns[var].reset(); - } - } - SASSERT(all_zeros(m_columns)); - } - - - enode* solver::mk_enode(expr* e) { - TRACE("arith", tout << expr_ref(e, m) << "\n";); - enode* n = ctx.get_enode(e); - if (n) - return n; - if (!a.is_arith_expr(e)) - n = e_internalize(e); - else { - ptr_buffer args; - if (reflect(e)) - for (expr* arg : *to_app(e)) - args.push_back(e_internalize(arg)); - n = ctx.mk_enode(e, args.size(), args.data()); - ctx.attach_node(n); - } - return n; - } - - theory_var solver::mk_evar(expr* n) { - enode* e = mk_enode(n); - if (e->is_attached_to(get_id())) - return e->get_th_var(get_id()); - theory_var v = mk_var(e); - TRACE("arith_verbose", tout << "v" << v << " " << mk_pp(n, m) << "\n";); - SASSERT(m_bounds.size() <= static_cast(v) || m_bounds[v].empty()); - reserve_bounds(v); - ctx.attach_th_var(e, this, v); - SASSERT(euf::null_theory_var != v); - return v; - } - - bool solver::has_var(expr* e) { - enode* n = ctx.get_enode(e); - return n && n->is_attached_to(get_id()); - } - - void solver::add_eq_constraint(lp::constraint_index index, enode* n1, enode* n2) { - m_constraint_sources.setx(index, equality_source, null_source); - m_equalities.setx(index, enode_pair(n1, n2), enode_pair(nullptr, nullptr)); - } - - void solver::add_ineq_constraint(lp::constraint_index index, literal lit) { - m_constraint_sources.setx(index, inequality_source, null_source); - m_inequalities.setx(index, lit, sat::null_literal); - } - - void solver::add_def_constraint(lp::constraint_index index) { - m_constraint_sources.setx(index, definition_source, null_source); - m_definitions.setx(index, euf::null_theory_var, euf::null_theory_var); - } - - void solver::add_def_constraint(lp::constraint_index index, theory_var v) { - m_constraint_sources.setx(index, definition_source, null_source); - m_definitions.setx(index, v, euf::null_theory_var); - } - - void solver::add_def_constraint_and_equality(lpvar vi, lp::lconstraint_kind kind, - const rational& bound) { - lpvar vi_equal; - lp::constraint_index ci = lp().add_var_bound_check_on_equal(vi, kind, bound, vi_equal); - add_def_constraint(ci); - if (vi_equal != lp::null_lpvar) - report_equality_of_fixed_vars(vi, vi_equal); - m_new_eq = true; - } - - bool solver::reflect(expr* n) const { - return get_config().m_arith_reflect || a.is_underspecified(n) || !a.is_arith_expr(n); - } - - lpvar solver::get_lpvar(theory_var v) const { - return lp().external_to_local(v); - } - - lp::tv solver::get_tv(theory_var v) const { - return lp::tv::raw(get_lpvar(v)); - } - - /** - \brief We must redefine this method, because theory of arithmetic contains - underspecified operators such as division by 0. - (/ a b) is essentially an uninterpreted function when b = 0. - Thus, 'a' must be considered a shared var if it is the child of an underspecified operator. - - if merge(a / b, x + y) and a / b is root, then x + y become shared and all z + u in equivalence class of x + y. - - TBD: when the set of underspecified subterms is small, compute the shared variables below it. - Recompute the set if there are merges that invalidate it. - Use the set to determine if a variable is shared. - */ - bool solver::is_shared(theory_var v) const { - if (m_underspecified.empty()) { - return false; - } - enode* n = var2enode(v); - enode* r = n->get_root(); - unsigned usz = m_underspecified.size(); - if (r->num_parents() > 2 * usz) { - for (unsigned i = 0; i < usz; ++i) { - app* u = m_underspecified[i]; - unsigned sz = u->get_num_args(); - for (unsigned j = 0; j < sz; ++j) - if (expr2enode(u->get_arg(j))->get_root() == r) - return true; - } - } - else { - for (enode* parent : euf::enode_parents(r)) - if (a.is_underspecified(parent->get_expr())) - return true; - } - return false; - } - - struct solver::undo_value : public trail { - solver& s; - undo_value(solver& s):s(s) {} - void undo() override { - s.m_value2var.erase(s.m_fixed_values.back()); - s.m_fixed_values.pop_back(); - } - }; - - - void solver::register_fixed_var(theory_var v, rational const& value) { - if (m_value2var.contains(value)) - return; - m_fixed_values.push_back(value); - m_value2var.insert(value, v); - ctx.push(undo_value(*this)); - } - - -} - diff --git a/enc_temp_folder/e6c4896a12a9fc61d88ea292bf2dca16/pb_solver.cpp b/enc_temp_folder/e6c4896a12a9fc61d88ea292bf2dca16/pb_solver.cpp deleted file mode 100644 index 8ac81343a..000000000 --- a/enc_temp_folder/e6c4896a12a9fc61d88ea292bf2dca16/pb_solver.cpp +++ /dev/null @@ -1,3806 +0,0 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - pb_solver.cpp - -Abstract: - - Extension for cardinality reasoning. - -Author: - - Nikolaj Bjorner (nbjorner) 2017-01-30 - ---*/ - -#include -#include "util/mpz.h" -#include "sat/sat_types.h" -#include "sat/smt/pb_solver.h" -#include "sat/smt/euf_solver.h" -#include "sat/sat_simplifier_params.hpp" - -namespace pb { - - static unsigned _bad_id = 11111111; // 2759; // -#define BADLOG(_cmd_) if (p.id() == _bad_id) { _cmd_; } - - - // ----------------------- - // constraint - - void solver::set_conflict(constraint& c, literal lit) { - m_stats.m_num_conflicts++; - TRACE("ba", display(tout, c, true); ); - if (!validate_conflict(c)) { - IF_VERBOSE(0, display(verbose_stream(), c, true)); - UNREACHABLE(); - } - SASSERT(validate_conflict(c)); - SASSERT(value(lit) == l_false); - set_conflict(sat::justification::mk_ext_justification(s().scope_lvl(), c.cindex()), ~lit); - SASSERT(inconsistent()); - } - - void solver::assign(constraint& c, literal lit) { - if (inconsistent()) return; - switch (value(lit)) { - case l_true: - break; - case l_false: - set_conflict(c, lit); - break; - default: - m_stats.m_num_propagations++; - m_num_propagations_since_pop++; - //TRACE("ba", tout << "#prop: " << m_stats.m_num_propagations << " - " << c.lit() << " => " << lit << "\n";); - SASSERT(validate_unit_propagation(c, lit)); - assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), c.cindex())); - break; - } - } - - // ------------------- - // pb_base - - void solver::simplify(constraint& p) { - SASSERT(s().at_base_lvl()); - if (p.lit() != sat::null_literal && value(p.lit()) == l_false) { - TRACE("ba", tout << "pb: flip sign " << p << "\n";); - IF_VERBOSE(1, verbose_stream() << "sign is flipped " << p << "\n";); - return; - } - bool nullify = p.lit() != sat::null_literal && value(p.lit()) == l_true; - if (nullify) { - IF_VERBOSE(100, display(verbose_stream() << "nullify tracking literal\n", p, true);); - SASSERT(lvl(p.lit()) == 0); - p.nullify_tracking_literal(*this); - init_watch(p); - } - - SASSERT(p.lit() == sat::null_literal || value(p.lit()) != l_false); - - unsigned true_val = 0, slack = 0, num_false = 0; - for (unsigned i = 0; i < p.size(); ++i) { - literal l = p.get_lit(i); - bool_var v = l.var(); - if (s().was_eliminated(v)) { - VERIFY(p.learned()); - remove_constraint(p, "contains eliminated"); - return; - } - switch (value(l)) { - case l_true: true_val += p.get_coeff(i); break; - case l_false: ++num_false; break; - default: slack += p.get_coeff(i); break; - } - } - if (p.k() == 1 && p.lit() == sat::null_literal) { - literal_vector lits(p.literals()); - s().mk_clause(lits.size(), lits.data(), sat::status::th(p.learned(), get_id())); - IF_VERBOSE(100, display(verbose_stream() << "add clause: " << lits << "\n", p, true);); - remove_constraint(p, "implies clause"); - } - else if (true_val == 0 && num_false == 0) { - if (p.lit() == sat::null_literal || value(p.lit()) == l_true) { - init_watch(p); - } - } - else if (true_val >= p.k()) { - if (p.lit() != sat::null_literal) { - IF_VERBOSE(100, display(verbose_stream() << "assign true literal ", p, true);); - s().assign_scoped(p.lit()); - } - remove_constraint(p, "is true"); - } - else if (slack + true_val < p.k()) { - if (p.lit() != sat::null_literal) { - IF_VERBOSE(100, display(verbose_stream() << "assign false literal ", p, true);); - s().assign_scoped(~p.lit()); - } - else { - IF_VERBOSE(1, verbose_stream() << "unsat during simplification\n";); - s().set_conflict(sat::justification(0)); - } - remove_constraint(p, "is false"); - } - else if (slack + true_val == p.k()) { - literal_vector lits(p.literals()); - assert_unconstrained(p.lit(), lits); - remove_constraint(p, "is tight"); - } - else { - unsigned sz = p.size(); - clear_watch(p); - unsigned j = 0; - for (unsigned i = 0; i < sz; ++i) { - literal l = p.get_lit(i); - if (value(l) == l_undef) { - if (i != j) p.swap(i, j); - ++j; - } - } - sz = j; - // _bad_id = p.id(); - BADLOG(display(verbose_stream() << "simplify ", p, true)); - - unsigned k = p.k() - true_val; - - if (k == 1 && p.lit() == sat::null_literal) { - literal_vector lits(sz, p.literals().data()); - s().mk_clause(sz, lits.data(), sat::status::th(p.learned(), get_id())); - remove_constraint(p, "is clause"); - return; - } - p.set_size(sz); - p.set_k(k); - if (p.lit() == sat::null_literal || value(p.lit()) == l_true) { - init_watch(p); - } - else { - SASSERT(value(p.lit()) == l_undef); - } - BADLOG(display(verbose_stream() << "simplified ", p, true); verbose_stream() << "\n"); - // display(verbose_stream(), c, true); - _bad_id = 11111111; - SASSERT(p.well_formed()); - m_simplify_change = true; - } - } - - /* - \brief split PB constraint into two because root is reused in arguments. - - x <=> a*x + B*y >= k - - x => a*x + By >= k - ~x => a*x + By < k - - k*~x + a*x + By >= k - (B+a-k + 1)*x + a*~x + B*~y >= B + a - k + 1 - - (k - a) * ~x + By >= k - a - k' * x + B'y >= k' - - */ - - void solver::split_root(constraint& p) { - SASSERT(p.lit() != sat::null_literal); - SASSERT(!p.learned()); - m_weights.resize(2*s().num_vars(), 0); - unsigned k = p.k(); - unsigned w, w1, w2; - literal root = p.lit(); - m_weights[(~root).index()] = k; - for (unsigned i = 0; i < p.size(); ++i) { - m_weights[p.get_lit(i).index()] += p.get_coeff(i); - } - literal_vector lits(p.literals()); - lits.push_back(~root); - - for (literal l : lits) { - w1 = m_weights[l.index()]; - w2 = m_weights[(~l).index()]; - if (w1 >= w2) { - if (w2 >= k) { - for (literal l2 : lits) m_weights[l2.index()] = 0; - // constraint is true - return; - } - k -= w2; - m_weights[(~l).index()] = 0; - m_weights[l.index()] = w1 - w2; - } - } - SASSERT(k > 0); - - // ~root * (k - a) + p >= k - a - - m_wlits.reset(); - for (literal l : lits) { - w = m_weights[l.index()]; - if (w != 0) { - m_wlits.push_back(wliteral(w, l)); - } - m_weights[l.index()] = 0; - } - - add_pb_ge(sat::null_literal, m_wlits, k, false); - } - - - // ------------------- - // pb - - - /* - Chai Kuhlmann: - Lw - set of watched literals - Lu - set of unwatched literals that are not false - - Lw = Lw \ { alit } - Sw -= value - a_max = max { a | l in Lw u Lu, l = undef } - while (Sw < k + a_max & Lu != 0) { - a_s = max { a | l in Lu } - Sw += a_s - Lw = Lw u {l_s} - Lu = Lu \ {l_s} - } - if (Sw < k) return conflict - for (li in Lw | Sw < k + ai) - assign li - return no-conflict - - a_max index: index of non-false literal with maximal weight. - */ - - void solver::add_index(pbc& p, unsigned index, literal lit) { - if (value(lit) == l_undef) { - m_pb_undef.push_back(index); - if (p[index].first > m_a_max) { - m_a_max = p[index].first; - } - } - } - - /* - \brief propagate assignment to alit in constraint p. - - TBD: - - consider reordering literals in watch list so that the search for watched literal takes average shorter time. - - combine with caching literals that are assigned to 'true' to a cold store where they are not being revisited. - Since 'true' literals may be unassigned (unless they are assigned at level 0) the cache has to be backtrack - friendly (and the overhead of backtracking has to be taken into account). - */ - lbool solver::add_assign(pbc& p, literal alit) { - BADLOG(display(verbose_stream() << "assign: " << alit << " watch: " << p.num_watch() << " size: " << p.size(), p, true)); - TRACE("ba", display(tout << "assign: " << alit << "\n", p, true);); - SASSERT(!inconsistent()); - unsigned sz = p.size(); - unsigned bound = p.k(); - unsigned num_watch = p.num_watch(); - unsigned slack = p.slack(); - SASSERT(value(alit) == l_false); - SASSERT(p.lit() == sat::null_literal || value(p.lit()) == l_true); - SASSERT(num_watch <= sz); - SASSERT(num_watch > 0); - unsigned index = 0; - m_a_max = 0; - m_pb_undef.reset(); - for (; index < num_watch; ++index) { - literal lit = p[index].second; - if (lit == alit) { - break; - } - add_index(p, index, lit); - } - if (index == num_watch || num_watch == 0) { - _bad_id = p.id(); - BADLOG( - verbose_stream() << "BAD: " << p.id() << "\n"; - display(verbose_stream(), p, true); - verbose_stream() << "alit: " << alit << "\n"; - verbose_stream() << "num watch " << num_watch << "\n"); - UNREACHABLE(); - return l_undef; - } - - SASSERT(validate_watch(p, sat::null_literal)); - // SASSERT(validate_watch(p, sat::null_literal)); - - SASSERT(index < num_watch); - unsigned index1 = index + 1; - for (; m_a_max == 0 && index1 < num_watch; ++index1) { - add_index(p, index1, p[index1].second); - } - - unsigned val = p[index].first; - SASSERT(value(p[index].second) == l_false); - SASSERT(val <= slack); - slack -= val; - - // find literals to swap with: - for (unsigned j = num_watch; j < sz && slack < bound + m_a_max; ++j) { - literal lit = p[j].second; - if (value(lit) != l_false) { - slack += p[j].first; - SASSERT(!p.is_watched(*this, p[j].second)); - p.watch_literal(*this, p[j].second); - p.swap(num_watch, j); - add_index(p, num_watch, lit); - ++num_watch; - } - } - - SASSERT(!inconsistent()); - DEBUG_CODE(for (auto idx : m_pb_undef) { SASSERT(value(p[idx].second) == l_undef); }); - - if (slack < bound) { - // maintain watching the literal - slack += val; - p.set_slack(slack); - p.set_num_watch(num_watch); - SASSERT(validate_watch(p, sat::null_literal)); - BADLOG(display(verbose_stream() << "conflict: " << alit << " watch: " << p.num_watch() << " size: " << p.size(), p, true)); - SASSERT(bound <= slack); - TRACE("ba", tout << "conflict " << alit << "\n";); - set_conflict(p, alit); - return l_false; - } - - if (num_watch == 1) { _bad_id = p.id(); } - - BADLOG(verbose_stream() << "size: " << p.size() << " index: " << index << " num watch: " << num_watch << "\n"); - - // swap out the watched literal. - --num_watch; - SASSERT(num_watch > 0); - p.set_slack(slack); - p.set_num_watch(num_watch); - p.swap(num_watch, index); - - - // - // slack >= bound, but slack - w(l) < bound - // l must be true. - // - if (slack < bound + m_a_max) { - BADLOG(verbose_stream() << "slack " << slack << " " << bound << " " << m_a_max << "\n";); - TRACE("ba", tout << p << "\n"; for(auto j : m_pb_undef) tout << j << " "; tout << "\n";); - for (unsigned index1 : m_pb_undef) { - if (index1 == num_watch) { - index1 = index; - } - wliteral wl = p[index1]; - literal lit = wl.second; - SASSERT(value(lit) == l_undef); - if (slack < bound + wl.first) { - BADLOG(verbose_stream() << "Assign " << lit << " " << wl.first << "\n"); - assign(p, lit); - } - } - } - - SASSERT(validate_watch(p, alit)); // except that alit is still watched. - - TRACE("ba", display(tout << "assign: " << alit << "\n", p, true);); - - BADLOG(verbose_stream() << "unwatch " << alit << " watch: " << p.num_watch() << " size: " << p.size() << " slack: " << p.slack() << " " << inconsistent() << "\n"); - - return l_undef; - } - - void solver::recompile(pbc& p) { - // IF_VERBOSE(2, verbose_stream() << "re: " << p << "\n";); - SASSERT(p.num_watch() == 0); - m_weights.resize(2*s().num_vars(), 0); - for (wliteral wl : p) { - m_weights[wl.second.index()] += wl.first; - } - unsigned k = p.k(); - unsigned sz = p.size(); - bool all_units = true; - unsigned j = 0; - for (unsigned i = 0; i < sz && 0 < k; ++i) { - literal l = p[i].second; - unsigned w1 = m_weights[l.index()]; - unsigned w2 = m_weights[(~l).index()]; - if (w1 == 0 || w1 < w2) { - continue; - } - else if (k <= w2) { - k = 0; - break; - } - else { - SASSERT(w2 <= w1 && w2 < k); - k -= w2; - w1 -= w2; - m_weights[l.index()] = 0; - m_weights[(~l).index()] = 0; - if (w1 == 0) { - continue; - } - else { - p[j] = wliteral(w1, l); - all_units &= w1 == 1; - ++j; - } - } - } - sz = j; - // clear weights - for (wliteral wl : p) { - m_weights[wl.second.index()] = 0; - m_weights[(~wl.second).index()] = 0; - } - - if (k == 0) { - if (p.lit() != sat::null_literal) { - s().assign_scoped(p.lit()); - } - remove_constraint(p, "recompiled to true"); - return; - } - - else if (k == 1 && p.lit() == sat::null_literal) { - literal_vector lits(sz, p.literals().data()); - s().mk_clause(sz, lits.data(), sat::status::th(p.learned(), get_id())); - remove_constraint(p, "recompiled to clause"); - return; - } - - else if (all_units) { - literal_vector lits(sz, p.literals().data()); - add_at_least(p.lit(), lits, k, p.learned()); - remove_constraint(p, "recompiled to cardinality"); - return; - } - else { - p.set_size(sz); - p.update_max_sum(); - if (p.max_sum() < k) { - if (p.lit() == sat::null_literal) { - s().set_conflict(sat::justification(0)); - } - else { - s().assign_scoped(~p.lit()); - } - remove_constraint(p, "recompiled to false"); - return; - } - p.set_k(k); - SASSERT(p.well_formed()); - - if (clausify(p)) { - return; - } - if (p.lit() == sat::null_literal || value(p.lit()) == l_true) { - init_watch(p); - } - } - } - - - // --------------------------- - // conflict resolution - - - void solver::inc_coeff(literal l, unsigned offset) { - SASSERT(offset > 0); - bool_var v = l.var(); - SASSERT(v != sat::null_bool_var); - m_coeffs.reserve(v + 1, 0); - TRACE("ba_verbose", tout << l << " " << offset << "\n";); - - int64_t coeff0 = m_coeffs[v]; - if (coeff0 == 0) { - m_active_vars.push_back(v); - } - - int64_t loffset = static_cast(offset); - int64_t inc = l.sign() ? -loffset : loffset; - int64_t coeff1 = inc + coeff0; - m_coeffs[v] = coeff1; - if (coeff1 > INT_MAX || coeff1 < INT_MIN) { - m_overflow = true; - return; - } - - if (coeff0 > 0 && inc < 0) { - inc_bound(std::max((int64_t)0, coeff1) - coeff0); - } - else if (coeff0 < 0 && inc > 0) { - inc_bound(coeff0 - std::min((int64_t)0, coeff1)); - } - int64_t lbound = static_cast(m_bound); - - // reduce coefficient to be no larger than bound. - if (coeff1 > lbound) { - m_coeffs[v] = lbound; - } - else if (coeff1 < 0 && -coeff1 > lbound) { - m_coeffs[v] = -lbound; - } - } - - int64_t solver::get_coeff(bool_var v) const { - return m_coeffs.get(v, 0); - } - - uint64_t solver::get_coeff(literal lit) const { - int64_t c1 = get_coeff(lit.var()); - SASSERT((c1 < 0) == lit.sign()); - int64_t c = std::abs(c1); - m_overflow |= (c != c1); - return static_cast(c); - } - - wliteral solver::get_wliteral(bool_var v) { - int64_t c1 = get_coeff(v); - literal l = literal(v, c1 < 0); - c1 = std::abs(c1); - unsigned c = static_cast(c1); - // TRACE("ba", tout << l << " " << c << "\n";); - m_overflow |= c != c1; - return wliteral(c, l); - } - - unsigned solver::get_abs_coeff(bool_var v) const { - int64_t c1 = std::abs(get_coeff(v)); - unsigned c = static_cast(c1); - m_overflow |= c != c1; - return c; - } - - int solver::get_int_coeff(bool_var v) const { - int64_t c1 = m_coeffs.get(v, 0); - int c = static_cast(c1); - m_overflow |= c != c1; - return c; - } - - void solver::inc_bound(int64_t i) { - int64_t new_bound = m_bound; - new_bound += i; - unsigned nb = static_cast(new_bound); - m_overflow |= new_bound < 0 || nb != new_bound; - m_bound = nb; - } - - void solver::reset_coeffs() { - for (unsigned i = m_active_vars.size(); i-- > 0; ) { - m_coeffs[m_active_vars[i]] = 0; - } - m_active_vars.reset(); - } - - - static bool _debug_conflict = false; - static literal _debug_consequent = sat::null_literal; - static unsigned_vector _debug_var2position; - -// #define DEBUG_CODE(_x_) _x_ - - void solver::bail_resolve_conflict(unsigned idx) { - literal_vector const& lits = s().m_trail; - while (m_num_marks > 0) { - bool_var v = lits[idx].var(); - if (s().is_marked(v)) { - s().reset_mark(v); - --m_num_marks; - } - if (idx == 0 && !_debug_conflict) { - _debug_conflict = true; - _debug_var2position.reserve(s().num_vars()); - for (unsigned i = 0; i < lits.size(); ++i) { - _debug_var2position[lits[i].var()] = i; - } - IF_VERBOSE(0, - active2pb(m_A); - uint64_t c = 0; - for (wliteral l : m_A.m_wlits) c += l.first; - verbose_stream() << "sum of coefficients: " << c << "\n"; - display(verbose_stream(), m_A, true); - verbose_stream() << "conflicting literal: " << s().m_not_l << "\n";); - - for (literal l : lits) { - if (s().is_marked(l.var())) { - IF_VERBOSE(0, verbose_stream() << "missing mark: " << l << "\n";); - s().reset_mark(l.var()); - } - } - m_num_marks = 0; - resolve_conflict(); - } - --idx; - } - } - - lbool solver::resolve_conflict() { - if (0 == m_num_propagations_since_pop) { - return l_undef; - } - - if (s().m_config.m_pb_resolve == sat::PB_ROUNDING) { - return resolve_conflict_rs(); - } - - m_overflow = false; - reset_coeffs(); - m_num_marks = 0; - m_bound = 0; - literal consequent = s().m_not_l; - sat::justification js = s().m_conflict; - TRACE("ba", tout << consequent << " " << js << "\n";); - bool unique_max; - m_conflict_lvl = s().get_max_lvl(consequent, js, unique_max); - if (m_conflict_lvl == 0) { - return l_undef; - } - if (consequent != sat::null_literal) { - consequent.neg(); - process_antecedent(consequent, 1); - } - literal_vector const& lits = s().m_trail; - unsigned idx = lits.size() - 1; - unsigned offset = 1; - DEBUG_CODE(active2pb(m_A);); - - do { - - - if (m_overflow || offset > (1 << 12)) { - IF_VERBOSE(20, verbose_stream() << "offset: " << offset << "\n"; - DEBUG_CODE(active2pb(m_A); display(verbose_stream(), m_A););); - goto bail_out; - } - - if (offset == 0) { - goto process_next_resolvent; - } - - DEBUG_CODE(TRACE("sat_verbose", display(tout, m_A););); - TRACE("ba", tout << "process consequent: " << consequent << " : "; s().display_justification(tout, js) << "\n";); - SASSERT(offset > 0); - - DEBUG_CODE(justification2pb(js, consequent, offset, m_B);); - - if (_debug_conflict) { - IF_VERBOSE(0, - verbose_stream() << consequent << "\n"; - s().display_justification(verbose_stream(), js); - verbose_stream() << "\n";); - _debug_consequent = consequent; - } - switch(js.get_kind()) { - case sat::justification::NONE: - SASSERT (consequent != sat::null_literal); - inc_bound(offset); - break; - case sat::justification::BINARY: - inc_bound(offset); - SASSERT (consequent != sat::null_literal); - inc_coeff(consequent, offset); - process_antecedent(js.get_literal(), offset); - break; - case sat::justification::TERNARY: - inc_bound(offset); - SASSERT (consequent != sat::null_literal); - inc_coeff(consequent, offset); - process_antecedent(js.get_literal1(), offset); - process_antecedent(js.get_literal2(), offset); - break; - case sat::justification::CLAUSE: { - inc_bound(offset); - sat::clause & c = s().get_clause(js); - unsigned i = 0; - if (consequent != sat::null_literal) { - inc_coeff(consequent, offset); - if (c[0] == consequent) { - i = 1; - } - else { - SASSERT(c[1] == consequent); - process_antecedent(c[0], offset); - i = 2; - } - } - unsigned sz = c.size(); - for (; i < sz; i++) - process_antecedent(c[i], offset); - break; - } - case sat::justification::EXT_JUSTIFICATION: { - auto cindex = js.get_ext_justification_idx(); - auto* ext = sat::constraint_base::to_extension(cindex); - if (ext != this) { - m_lemma.reset(); - ext->get_antecedents(consequent, idx, m_lemma, false); - for (literal l : m_lemma) process_antecedent(~l, offset); - break; - } - constraint& cnstr = index2constraint(cindex); - ++m_stats.m_num_resolves; - switch (cnstr.tag()) { - case pb::tag_t::card_t: { - card& c = cnstr.to_card(); - inc_bound(static_cast(offset) * c.k()); - process_card(c, offset); - break; - } - case pb::tag_t::pb_t: { - pbc& p = cnstr.to_pb(); - m_lemma.reset(); - inc_bound(offset); - inc_coeff(consequent, offset); - get_antecedents(consequent, p, m_lemma); - TRACE("ba", display(tout, p, true); tout << m_lemma << "\n";); - if (_debug_conflict) { - verbose_stream() << consequent << " "; - verbose_stream() << "antecedents: " << m_lemma << "\n"; - } - for (literal l : m_lemma) process_antecedent(~l, offset); - break; - } - default: - UNREACHABLE(); - break; - } - break; - } - default: - UNREACHABLE(); - break; - } - - SASSERT(validate_lemma()); - - DEBUG_CODE( - active2pb(m_C); - VERIFY(validate_resolvent()); - m_A = m_C; - TRACE("ba", display(tout << "conflict: ", m_A););); - - cut(); - - process_next_resolvent: - - // find the next marked variable in the assignment stack - bool_var v; - while (true) { - consequent = lits[idx]; - v = consequent.var(); - if (s().is_marked(v)) { - if (s().lvl(v) == m_conflict_lvl) { - break; - } - } - if (idx == 0) { - IF_VERBOSE(2, verbose_stream() << "did not find marked literal\n";); - goto bail_out; - } - SASSERT(idx > 0); - --idx; - } - - SASSERT(lvl(v) == m_conflict_lvl); - s().reset_mark(v); - --idx; - TRACE("sat_verbose", tout << "Unmark: v" << v << "\n";); - --m_num_marks; - js = s().m_justification[v]; - offset = get_abs_coeff(v); - if (offset > m_bound) { - int64_t bound64 = static_cast(m_bound); - m_coeffs[v] = (get_coeff(v) < 0) ? -bound64 : bound64; - offset = m_bound; - DEBUG_CODE(active2pb(m_A);); - } - SASSERT(value(consequent) == l_true); - } - while (m_num_marks > 0); - - DEBUG_CODE(for (bool_var i = 0; i < static_cast(s().num_vars()); ++i) SASSERT(!s().is_marked(i));); - SASSERT(validate_lemma()); - - if (!create_asserting_lemma()) { - goto bail_out; - } - active2lemma(); - - - DEBUG_CODE(VERIFY(validate_conflict(m_lemma, m_A));); - - return l_true; - - bail_out: - if (m_overflow) { - ++m_stats.m_num_overflow; - m_overflow = false; - } - bail_resolve_conflict(idx); - return l_undef; - } - - - unsigned solver::ineq::bv_coeff(bool_var v) const { - for (unsigned i = size(); i-- > 0; ) { - if (lit(i).var() == v) return coeff(i); - } - UNREACHABLE(); - return 0; - } - - void solver::ineq::divide(unsigned c) { - if (c == 1) return; - for (unsigned i = size(); i-- > 0; ) { - m_wlits[i].first = (coeff(i) + c - 1) / c; - } - m_k = (m_k + c - 1) / c; - } - - /** - * Remove literal at position i, subtract coefficient from bound. - */ - void solver::ineq::weaken(unsigned i) { - unsigned ci = coeff(i); - SASSERT(m_k >= ci); - m_k -= ci; - m_wlits[i] = m_wlits.back(); - m_wlits.pop_back(); - } - - /** - * Round coefficient of inequality to 1. - */ - void solver::round_to_one(ineq& ineq, bool_var v) { - unsigned c = ineq.bv_coeff(v); - if (c == 1) return; - unsigned sz = ineq.size(); - for (unsigned i = 0; i < sz; ++i) { - unsigned ci = ineq.coeff(i); - unsigned q = ci % c; - if (q != 0 && !is_false(ineq.lit(i))) { -#if 1 - // code review by Elffers: - ineq.weaken(i); - --i; - --sz; -#else - if (q == ci) { - ineq.weaken(i); - --i; - --sz; - } - else { - ineq.m_wlits[i].first -= q; - ineq.m_k -= q; - } -#endif - } - } - ineq.divide(c); - TRACE("ba", display(tout << "var: " << v << " " << c << ": ", ineq, true);); - } - - void solver::round_to_one(bool_var w) { - unsigned c = get_abs_coeff(w); - if (c == 1 || c == 0) return; - for (bool_var v : m_active_vars) { - wliteral wl = get_wliteral(v); - unsigned q = wl.first % c; - if (q != 0 && !is_false(wl.second)) { - m_coeffs[v] = wl.first - q; - m_bound -= q; - SASSERT(m_bound > 0); - } - } - SASSERT(validate_lemma()); - divide(c); - SASSERT(validate_lemma()); - TRACE("ba", active2pb(m_B); display(tout, m_B, true);); - } - - void solver::divide(unsigned c) { - SASSERT(c != 0); - if (c == 1) return; - reset_active_var_set(); - unsigned j = 0, sz = m_active_vars.size(); - for (unsigned i = 0; i < sz; ++i) { - bool_var v = m_active_vars[i]; - int ci = get_int_coeff(v); - if (!test_and_set_active(v) || ci == 0) continue; - if (ci > 0) { - m_coeffs[v] = (ci + c - 1) / c; - } - else { - m_coeffs[v] = -static_cast((-ci + c - 1) / c); - } - m_active_vars[j++] = v; - } - m_active_vars.shrink(j); - m_bound = static_cast((m_bound + c - 1) / c); - } - - void solver::resolve_on(literal consequent) { - round_to_one(consequent.var()); - m_coeffs[consequent.var()] = 0; - } - - void solver::resolve_with(ineq const& ineq) { - TRACE("ba", display(tout, ineq, true);); - inc_bound(ineq.m_k); - TRACE("ba", tout << "bound: " << m_bound << "\n";); - - for (unsigned i = ineq.size(); i-- > 0; ) { - literal l = ineq.lit(i); - inc_coeff(l, static_cast(ineq.coeff(i))); - TRACE("ba", tout << "bound: " << m_bound << " lit: " << l << " coeff: " << ineq.coeff(i) << "\n";); - } - } - - void solver::reset_marks(unsigned idx) { - while (m_num_marks > 0) { - SASSERT(idx > 0); - bool_var v = s().m_trail[idx].var(); - if (s().is_marked(v)) { - s().reset_mark(v); - --m_num_marks; - } - --idx; - } - } - - /** - * \brief mark variables that are on the assignment stack but - * below the current processing level. - */ - void solver::mark_variables(ineq const& ineq) { - for (wliteral wl : ineq.m_wlits) { - literal l = wl.second; - if (!is_false(l)) continue; - bool_var v = l.var(); - unsigned level = lvl(v); - if (!s().is_marked(v) && !is_visited(v) && level == m_conflict_lvl) { - s().mark(v); - ++m_num_marks; - } - } - } - - lbool solver::resolve_conflict_rs() { - if (0 == m_num_propagations_since_pop) { - return l_undef; - } - m_overflow = false; - reset_coeffs(); - init_visited(); - m_num_marks = 0; - m_bound = 0; - literal consequent = s().m_not_l; - sat::justification js = s().m_conflict; - bool unique_max; - m_conflict_lvl = s().get_max_lvl(consequent, js, unique_max); - if (m_conflict_lvl == 0) { - return l_undef; - } - if (consequent != sat::null_literal) { - consequent.neg(); - process_antecedent(consequent, 1); - } - TRACE("ba", tout << consequent << " " << js << "\n";); - unsigned idx = s().m_trail.size() - 1; - - do { - TRACE("ba", s().display_justification(tout << "process consequent: " << consequent << " : ", js) << "\n"; - if (consequent != sat::null_literal) { active2pb(m_A); display(tout, m_A, true); } - ); - - switch (js.get_kind()) { - case sat::justification::NONE: - SASSERT(consequent != sat::null_literal); - round_to_one(consequent.var()); - inc_bound(1); - inc_coeff(consequent, 1); - break; - case sat::justification::BINARY: - SASSERT(consequent != sat::null_literal); - round_to_one(consequent.var()); - inc_bound(1); - inc_coeff(consequent, 1); - process_antecedent(js.get_literal()); - break; - case sat::justification::TERNARY: - SASSERT(consequent != sat::null_literal); - round_to_one(consequent.var()); - inc_bound(1); - inc_coeff(consequent, 1); - process_antecedent(js.get_literal1()); - process_antecedent(js.get_literal2()); - break; - case sat::justification::CLAUSE: { - sat::clause & c = s().get_clause(js); - unsigned i = 0; - if (consequent != sat::null_literal) { - round_to_one(consequent.var()); - inc_coeff(consequent, 1); - if (c[0] == consequent) { - i = 1; - } - else { - SASSERT(c[1] == consequent); - process_antecedent(c[0]); - i = 2; - } - } - inc_bound(1); - unsigned sz = c.size(); - for (; i < sz; i++) - process_antecedent(c[i]); - break; - } - case sat::justification::EXT_JUSTIFICATION: { - ++m_stats.m_num_resolves; - sat::ext_justification_idx index = js.get_ext_justification_idx(); - auto* ext = sat::constraint_base::to_extension(index); - if (ext != this) { - m_lemma.reset(); - ext->get_antecedents(consequent, index, m_lemma, false); - for (literal l : m_lemma) - process_antecedent(~l, 1); - break; - } - constraint& p = index2constraint(index); - SASSERT(!p.was_removed()); - unsigned k = p.k(), sz = p.size(); - m_A.reset(0); - for (unsigned i = 0; i < sz; ++i) { - literal l = p.get_lit(i); - unsigned c = p.get_coeff(i); - if (l == consequent || !is_visited(l.var())) { - m_A.push(l, c); - } - else { - SASSERT(k > c); - TRACE("ba", tout << "visited: " << l << "\n";); - k -= c; - } - } - SASSERT(k > 0); - if (p.lit() != sat::null_literal) m_A.push(~p.lit(), k); - m_A.m_k = k; - - mark_variables(m_A); - if (consequent == sat::null_literal) { - SASSERT(validate_ineq(m_A)); - m_bound = static_cast(m_A.m_k); - for (wliteral wl : m_A.m_wlits) { - process_antecedent(wl.second, wl.first); - } - } - else { - round_to_one(consequent.var()); - if (p.is_pb()) round_to_one(m_A, consequent.var()); - SASSERT(validate_ineq(m_A)); - resolve_with(m_A); - } - break; - } - default: - UNREACHABLE(); - break; - } - - SASSERT(validate_lemma()); - cut(); - - // find the next marked variable in the assignment stack - bool_var v; - while (true) { - consequent = s().m_trail[idx]; - v = consequent.var(); - mark_visited(v); - if (s().is_marked(v)) { - int64_t c = get_coeff(v); - if (c == 0 || ((c < 0) == consequent.sign())) { - s().reset_mark(v); - --m_num_marks; - } - else { - break; - } - } - if (idx == 0) { - TRACE("ba", tout << "there is no consequent\n";); - goto bail_out; - } - --idx; - } - - SASSERT(lvl(v) == m_conflict_lvl); - s().reset_mark(v); - --idx; - --m_num_marks; - js = s().m_justification[v]; - } - while (m_num_marks > 0 && !m_overflow); - TRACE("ba", active2pb(m_A); display(tout, m_A, true);); - - // TBD: check if this is useful - if (!m_overflow && consequent != sat::null_literal) { - round_to_one(consequent.var()); - } - if (!m_overflow && create_asserting_lemma()) { - active2lemma(); - return l_true; - } - - bail_out: - TRACE("ba", tout << "bail " << m_overflow << "\n";); - if (m_overflow) { - ++m_stats.m_num_overflow; - m_overflow = false; - } - return l_undef; - } - - - bool solver::create_asserting_lemma() { - int64_t bound64 = m_bound; - int64_t slack = -bound64; - reset_active_var_set(); - unsigned j = 0, sz = m_active_vars.size(); - for (unsigned i = 0; i < sz; ++i) { - bool_var v = m_active_vars[i]; - unsigned c = get_abs_coeff(v); - if (!test_and_set_active(v) || c == 0) continue; - slack += c; - m_active_vars[j++] = v; - } - m_active_vars.shrink(j); - m_lemma.reset(); - m_lemma.push_back(sat::null_literal); - unsigned num_skipped = 0; - int64_t asserting_coeff = 0; - for (unsigned i = 0; 0 <= slack && i < m_active_vars.size(); ++i) { - bool_var v = m_active_vars[i]; - int64_t coeff = get_coeff(v); - lbool val = value(v); - bool is_true = val == l_true; - bool append = coeff != 0 && val != l_undef && ((coeff < 0) == is_true); - if (append) { - literal lit(v, !is_true); - if (lvl(lit) == m_conflict_lvl) { - if (m_lemma[0] == sat::null_literal) { - asserting_coeff = std::abs(coeff); - slack -= asserting_coeff; - m_lemma[0] = ~lit; - } - else { - ++num_skipped; - if (asserting_coeff < std::abs(coeff)) { - m_lemma[0] = ~lit; - slack -= (std::abs(coeff) - asserting_coeff); - asserting_coeff = std::abs(coeff); - } - } - } - else if (lvl(lit) < m_conflict_lvl) { - slack -= std::abs(coeff); - m_lemma.push_back(~lit); - } - } - } - if (slack >= 0) { - TRACE("ba", tout << "slack is non-negative\n";); - IF_VERBOSE(20, verbose_stream() << "(sat.card slack: " << slack << " skipped: " << num_skipped << ")\n";); - return false; - } - if (m_overflow) { - TRACE("ba", tout << "overflow\n";); - return false; - } - if (m_lemma[0] == sat::null_literal) { - if (m_lemma.size() == 1) { - s().set_conflict(sat::justification(0)); - } - TRACE("ba", tout << "no asserting literal\n";); - return false; - } - - TRACE("ba", tout << m_lemma << "\n";); - - if (get_config().m_drat && m_solver) { - s().m_drat.add(m_lemma, sat::status::th(true, get_id())); - } - - s().m_lemma.reset(); - s().m_lemma.append(m_lemma); - for (unsigned i = 1; i < m_lemma.size(); ++i) { - CTRACE("ba", s().is_marked(m_lemma[i].var()), tout << "marked: " << m_lemma[i] << "\n";); - s().mark(m_lemma[i].var()); - } - return true; - } - - /* - \brief compute a cut for current resolvent. - */ - - void solver::cut() { - - // bypass cut if there is a unit coefficient - for (bool_var v : m_active_vars) { - if (1 == get_abs_coeff(v)) return; - } - - unsigned g = 0; - - for (unsigned i = 0; g != 1 && i < m_active_vars.size(); ++i) { - bool_var v = m_active_vars[i]; - unsigned coeff = get_abs_coeff(v); - if (coeff == 0) { - continue; - } - if (m_bound < coeff) { - int64_t bound64 = m_bound; - if (get_coeff(v) > 0) { - m_coeffs[v] = bound64; - } - else { - m_coeffs[v] = -bound64; - } - coeff = m_bound; - } - SASSERT(0 < coeff && coeff <= m_bound); - if (g == 0) { - g = coeff; - } - else { - g = u_gcd(g, coeff); - } - } - - if (g >= 2) { - reset_active_var_set(); - unsigned j = 0, sz = m_active_vars.size(); - for (unsigned i = 0; i < sz; ++i) { - bool_var v = m_active_vars[i]; - int64_t c = m_coeffs[v]; - if (!test_and_set_active(v) || c == 0) continue; - m_coeffs[v] /= static_cast(g); - m_active_vars[j++] = v; - } - m_active_vars.shrink(j); - m_bound = (m_bound + g - 1) / g; - ++m_stats.m_num_cut; - } - } - - void solver::process_card(card& c, unsigned offset) { - literal lit = c.lit(); - SASSERT(c.k() <= c.size()); - SASSERT(lit == sat::null_literal || value(lit) != l_undef); - SASSERT(0 < offset); - for (unsigned i = c.k(); i < c.size(); ++i) { - process_antecedent(c[i], offset); - } - for (unsigned i = 0; i < c.k(); ++i) { - inc_coeff(c[i], offset); - } - if (lit != sat::null_literal) { - uint64_t offset1 = static_cast(offset) * c.k(); - if (offset1 > UINT_MAX) { - m_overflow = true; - } - if (value(lit) == l_true) { - process_antecedent(~lit, static_cast(offset1)); - } - else { - process_antecedent(lit, static_cast(offset1)); - } - } - } - - void solver::process_antecedent(literal l, unsigned offset) { - SASSERT(value(l) == l_false); - bool_var v = l.var(); - unsigned level = lvl(v); - - if (!s().is_marked(v) && level == m_conflict_lvl) { - s().mark(v); - ++m_num_marks; - if (_debug_conflict && _debug_consequent != sat::null_literal && _debug_var2position[_debug_consequent.var()] < _debug_var2position[l.var()]) { - IF_VERBOSE(0, verbose_stream() << "antecedent " << l << " is above consequent in stack\n";); - } - } - inc_coeff(l, offset); - } - - literal solver::get_asserting_literal(literal p) { - if (get_abs_coeff(p.var()) != 0) { - return p; - } - unsigned level = 0; - for (unsigned i = 0; i < m_active_vars.size(); ++i) { - bool_var v = m_active_vars[i]; - literal lit(v, get_coeff(v) < 0); - if (value(lit) == l_false && lvl(lit) > level) { - p = lit; - level = lvl(lit); - } - } - return p; - } - - solver::solver(euf::solver& ctx, euf::theory_id id) : - solver(ctx.get_manager(), ctx.get_si(), id) {} - - solver::solver(ast_manager& m, sat::sat_internalizer& si, euf::theory_id id) - : euf::th_solver(m, symbol("ba"), id), - si(si), m_pb(m), - m_lookahead(nullptr), - m_constraint_id(0), m_ba(*this), m_sort(m_ba) { - TRACE("ba", tout << this << "\n";); - m_num_propagations_since_pop = 0; - } - - solver::~solver() { - m_stats.reset(); - for (constraint* c : m_constraints) { - c->deallocate(m_allocator); - } - for (constraint* c : m_learned) { - c->deallocate(m_allocator); - } - } - - void solver::add_at_least(bool_var v, literal_vector const& lits, unsigned k) { - literal lit = v == sat::null_bool_var ? sat::null_literal : literal(v, false); - add_at_least(lit, lits, k, m_is_redundant); - } - - constraint* solver::add_at_least(literal lit, literal_vector const& lits, unsigned k, bool learned) { - if (k == 1 && lit == sat::null_literal) { - literal_vector _lits(lits); - s().mk_clause(_lits.size(), _lits.data(), sat::status::th(learned, get_id())); - return nullptr; - } - if (k == 0 && lit == sat::null_literal) - return nullptr; - - if (k == 0) { - s().assign_unit(lit); - return nullptr; - } - - - if (!learned && clausify(lit, lits.size(), lits.data(), k)) { - return nullptr; - } - void * mem = m_allocator.allocate(card::get_obj_size(lits.size())); - sat::constraint_base::initialize(mem, this); - card* c = new (sat::constraint_base::ptr2mem(mem)) card(next_id(), lit, lits, k); - c->set_learned(learned); - add_constraint(c); - return c; - } - - void solver::add_constraint(constraint* c) { - literal_vector lits(c->literals()); - if (c->learned()) { - m_learned.push_back(c); - } - else { - SASSERT(!m_solver || s().at_base_lvl()); - m_constraints.push_back(c); - } - literal lit = c->lit(); - if (c->learned() && m_solver && !s().at_base_lvl()) { - SASSERT(lit == sat::null_literal); - // gets initialized after backjump. - m_constraint_to_reinit.push_back(c); - } - else if (lit == sat::null_literal) { - init_watch(*c); - } - else { - if (m_solver) m_solver->set_external(lit.var()); - c->watch_literal(*this, lit); - c->watch_literal(*this, ~lit); - } - if (!c->well_formed()) - std::cout << *c << "\n"; - VERIFY(c->well_formed()); - if (m_solver && m_solver->get_config().m_drat) { - std::function fn = [&](std::ostream& out) { - out << "c ba constraint " << *c << " 0\n"; - }; - m_solver->get_drat().log_adhoc(fn); - } - } - - - bool solver::init_watch(constraint& c) { - return !inconsistent() && c.init_watch(*this); - } - - lbool solver::add_assign(constraint& c, literal l) { - switch (c.tag()) { - case pb::tag_t::card_t: return add_assign(c.to_card(), l); - case pb::tag_t::pb_t: return add_assign(c.to_pb(), l); - } - UNREACHABLE(); - return l_undef; - } - - constraint* solver::add_pb_ge(literal lit, svector const& wlits, unsigned k, bool learned) { - bool units = true; - for (wliteral wl : wlits) units &= wl.first == 1; - if (k == 0 && lit == sat::null_literal) { - return nullptr; - } - if (!learned) { - for (wliteral wl : wlits) s().set_external(wl.second.var()); - } - if (units || k == 1) { - literal_vector lits; - for (wliteral wl : wlits) lits.push_back(wl.second); - return add_at_least(lit, lits, k, learned); - } - void * mem = m_allocator.allocate(pbc::get_obj_size(wlits.size())); - sat::constraint_base::initialize(mem, this); - pbc* p = new (sat::constraint_base::ptr2mem(mem)) pbc(next_id(), lit, wlits, k); - p->set_learned(learned); - add_constraint(p); - return p; - } - - void solver::add_pb_ge(bool_var v, svector const& wlits, unsigned k) { - literal lit = v == sat::null_bool_var ? sat::null_literal : literal(v, false); - add_pb_ge(lit, wlits, k, m_is_redundant); - } - - bool solver::is_external(bool_var v) { - return false; - } - - /* - \brief return true to keep watching literal. - */ - bool solver::propagated(literal l, sat::ext_constraint_idx idx) { - SASSERT(value(l) == l_true); - constraint& c = index2constraint(idx); - if (c.lit() != sat::null_literal && l.var() == c.lit().var()) { - init_watch(c); - return true; - } - else if (c.lit() != sat::null_literal && value(c.lit()) != l_true) { - return true; - } - else { - return l_undef != add_assign(c, ~l); - } - } - - - double solver::get_reward(literal l, sat::ext_justification_idx idx, sat::literal_occs_fun& occs) const { - constraint const& c = index2constraint(idx); - return c.get_reward(*this, occs); - } - - - void solver::ensure_parity_size(bool_var v) { - if (m_parity_marks.size() <= static_cast(v)) { - m_parity_marks.resize(static_cast(v) + 1, 0); - } - } - - unsigned solver::get_parity(bool_var v) { - return m_parity_marks.get(v, 0); - } - - void solver::inc_parity(bool_var v) { - ensure_parity_size(v); - m_parity_marks[v]++; - } - - void solver::reset_parity(bool_var v) { - ensure_parity_size(v); - m_parity_marks[v] = 0; - } - - - /** - \brief retrieve a sufficient set of literals from p that imply l. - - Find partition: - - - Ax + coeff*l + B*y >= k - - all literals in x are false. - - B < k - - Then x is an explanation for l - - */ - - bool solver::assigned_above(literal above, literal below) { - unsigned l = lvl(above); - SASSERT(l == lvl(below)); - if (l == 0) return false; - unsigned start = s().m_scopes[l-1].m_trail_lim; - literal_vector const& lits = s().m_trail; - for (unsigned sz = lits.size(); sz-- > start; ) { - if (lits[sz] == above) return true; - if (lits[sz] == below) return false; - } - UNREACHABLE(); - return false; - } - - void solver::get_antecedents(literal l, pbc const& p, literal_vector& r) { - TRACE("ba", display(tout << l << " level: " << s().scope_lvl() << " ", p, true);); - SASSERT(p.lit() == sat::null_literal || value(p.lit()) == l_true); - - if (p.lit() != sat::null_literal) { - r.push_back(p.lit()); - } - - unsigned k = p.k(); - - if (_debug_conflict) { - IF_VERBOSE(0, display(verbose_stream(), p, true); - verbose_stream() << "literal: " << l << " value: " << value(l) << " num-watch: " << p.num_watch() << " slack: " << p.slack() << "\n";); - } - - if (value(l) == l_false) { - // The literal comes from a conflict. - // it is forced true, but assigned to false. - unsigned slack = 0; - for (wliteral wl : p) { - if (value(wl.second) != l_false) { - slack += wl.first; - } - } - SASSERT(slack < k); - for (wliteral wl : p) { - literal lit = wl.second; - if (lit != l && value(lit) == l_false) { - unsigned w = wl.first; - if (slack + w < k) { - slack += w; - } - else { - r.push_back(~lit); - } - } - } - } - else { - // comes from a unit propagation - SASSERT(value(l) == l_true); - unsigned coeff = 0, j = 0; - for (; j < p.size(); ++j) { - if (p[j].second == l) { - coeff = p[j].first; - break; - } - } - - ++j; - if (j < p.num_watch()) { - j = p.num_watch(); - } - CTRACE("ba", coeff == 0, display(tout << l << " coeff: " << coeff << "\n", p, true);); - - if (_debug_conflict) { - std::cout << "coeff " << coeff << "\n"; - } - - SASSERT(coeff > 0); - unsigned slack = p.max_sum() - coeff; - - // we need antecedents to be deeper than alit. - for (; j < p.size(); ++j) { - literal lit = p[j].second; - unsigned w = p[j].first; - if (l_false != value(lit)) { - // skip - } - else if (lvl(lit) > lvl(l)) { - // skip - } - else if (lvl(lit) == lvl(l) && assigned_above(~lit, l)) { - // skip - } - else if (slack + w < k) { - slack += w; - } - else { - r.push_back(~lit); - } - } - } - SASSERT(validate_unit_propagation(p, r, l)); - } - - bool solver::is_extended_binary(sat::ext_justification_idx idx, literal_vector & r) { - return index2constraint(idx).is_extended_binary(r); - } - - - void solver::get_antecedents(literal l, card const& c, literal_vector& r) { - if (l == ~c.lit()) { - for (unsigned i = c.k() - 1; i < c.size(); ++i) { - VERIFY(value(c[i]) == l_false); - r.push_back(~c[i]); - } - return; - } - DEBUG_CODE( - bool found = false; - for (unsigned i = 0; !found && i < c.k(); ++i) { - found = c[i] == l; - } - CTRACE("ba",!found, s().display(tout << l << ":" << c << "\n");); - SASSERT(found);); - - VERIFY(c.lit() == sat::null_literal || value(c.lit()) != l_false); - if (c.lit() != sat::null_literal) r.push_back(value(c.lit()) == l_true ? c.lit() : ~c.lit()); - for (unsigned i = c.k(); i < c.size(); ++i) { - SASSERT(value(c[i]) == l_false); - r.push_back(~c[i]); - } - } - - - // ---------------------------- - // constraint generic methods - - void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector & r, bool probing) { - get_antecedents(l, index2constraint(idx), r, probing); - } - - - void solver::get_antecedents(literal l, constraint const& c, literal_vector& r, bool probing) { - switch (c.tag()) { - case pb::tag_t::card_t: get_antecedents(l, c.to_card(), r); break; - case pb::tag_t::pb_t: get_antecedents(l, c.to_pb(), r); break; - default: UNREACHABLE(); break; - } - if (get_config().m_drat && m_solver && !probing) { - literal_vector lits; - for (literal lit : r) - lits.push_back(~lit); - lits.push_back(l); - s().m_drat.add(lits, sat::status::th(true, get_id())); - } - } - - void solver::clear_watch(constraint& c) { - c.clear_watch(*this); - } - - void solver::remove_constraint(constraint& c, char const* reason) { - TRACE("ba", display(tout << "remove ", c, true) << " " << reason << "\n";); - IF_VERBOSE(21, display(verbose_stream() << "remove " << reason << " ", c, true);); - c.nullify_tracking_literal(*this); - clear_watch(c); - c.set_removed(); - m_constraint_removed = true; - } - - // -------------------------------- - // validation - - bool solver::validate_unit_propagation(constraint const& c, literal l) const { - return true; - return c.validate_unit_propagation(*this, l); - } - - bool solver::validate_conflict(constraint const& c) const { - return eval(c) == l_false; - } - - lbool solver::eval(constraint const& c) const { - lbool v1 = c.lit() == sat::null_literal ? l_true : value(c.lit()); - return eval(v1, c.eval(*this)); - } - - lbool solver::eval(sat::model const& m, constraint const& c) const { - lbool v1 = c.lit() == sat::null_literal ? l_true : pb::value(m, c.lit()); - return eval(v1, c.eval(m)); - } - - lbool solver::eval(lbool a, lbool b) const { - if (a == l_undef || b == l_undef) return l_undef; - return (a == b) ? l_true : l_false; - } - - bool solver::validate() { - if (!validate_watch_literals()) { - return false; - } - for (constraint* c : m_constraints) { - if (!validate_watched_constraint(*c)) - return false; - } - for (constraint* c : m_learned) { - if (!validate_watched_constraint(*c)) - return false; - } - return true; - } - - bool solver::validate_watch_literals() const { - for (unsigned v = 0; v < s().num_vars(); ++v) { - literal lit(v, false); - if (lvl(lit) == 0) continue; - if (!validate_watch_literal(lit)) return false; - if (!validate_watch_literal(~lit)) return false; - } - return true; - } - - bool solver::validate_watch_literal(literal lit) const { - if (lvl(lit) == 0) return true; - for (auto const & w : get_wlist(lit)) { - if (w.get_kind() == sat::watched::EXT_CONSTRAINT) { - constraint const& c = index2constraint(w.get_ext_constraint_idx()); - if (!c.is_watching(~lit) && lit.var() != c.lit().var()) { - IF_VERBOSE(0, display(verbose_stream() << lit << " " << lvl(lit) << " is not watched in " << c << "\n", c, true);); - UNREACHABLE(); - return false; - } - } - } - return true; - } - - bool solver::validate_watched_constraint(constraint const& c) const { - if (c.is_pb() && !validate_watch(c.to_pb(), sat::null_literal)) { - return false; - } - if (c.lit() != sat::null_literal && value(c.lit()) != l_true) return true; - SASSERT(c.lit() == sat::null_literal || lvl(c.lit()) == 0 || (c.is_watched(*this, c.lit()) && c.is_watched(*this, ~c.lit()))); - if (eval(c) == l_true) { - return true; - } - literal_vector lits(c.literals()); - for (literal l : lits) { - if (lvl(l) == 0) continue; - bool found = c.is_watched(*this, l); - if (found != c.is_watching(l)) { - - IF_VERBOSE(0, - verbose_stream() << "Discrepancy of watched literal: " << l << " id: " << c.id() - << " clause: " << c << (found?" is watched, but shouldn't be":" not watched, but should be") << "\n"; - s().display_watch_list(verbose_stream() << l << ": ", get_wlist(l)) << "\n"; - s().display_watch_list(verbose_stream() << ~l << ": ", get_wlist(~l)) << "\n"; - verbose_stream() << "value: " << value(l) << " level: " << lvl(l) << "\n"; - display(verbose_stream(), c, true); - if (c.lit() != sat::null_literal) verbose_stream() << value(c.lit()) << "\n";); - - IF_VERBOSE(0, s().display_watches(verbose_stream())); - - UNREACHABLE(); - return false; - } - } - return true; - } - - bool solver::validate_watch(pbc const& p, literal alit) const { - for (unsigned i = 0; i < p.size(); ++i) { - literal l = p[i].second; - if (l != alit && lvl(l) != 0 && p.is_watched(*this, l) != (i < p.num_watch())) { - IF_VERBOSE(0, display(verbose_stream(), p, true); - verbose_stream() << "literal " << l << " at position " << i << " " << p.is_watched(*this, l) << "\n";); - UNREACHABLE(); - return false; - } - } - unsigned slack = 0; - for (unsigned i = 0; i < p.num_watch(); ++i) { - slack += p[i].first; - } - if (slack != p.slack()) { - IF_VERBOSE(0, display(verbose_stream(), p, true);); - UNREACHABLE(); - return false; - } - return true; - } - - - /** - \brief Lex on (glue, size) - */ - struct constraint_glue_psm_lt { - bool operator()(constraint const * c1, constraint const * c2) const { - return - (c1->glue() < c2->glue()) || - (c1->glue() == c2->glue() && - (c1->psm() < c2->psm() || - (c1->psm() == c2->psm() && c1->size() < c2->size()))); - } - }; - - void solver::update_psm(constraint& c) const { - unsigned r = 0; - switch (c.tag()) { - case pb::tag_t::card_t: - for (literal l : c.to_card()) { - if (s().m_phase[l.var()] == !l.sign()) ++r; - } - break; - case pb::tag_t::pb_t: - for (wliteral l : c.to_pb()) { - if (s().m_phase[l.second.var()] == !l.second.sign()) ++r; - } - break; - default: - break; - } - c.set_psm(r); - } - - void solver::gc() { - if (m_learned.size() >= 2 * m_constraints.size() && - (s().at_search_lvl() || s().at_base_lvl())) { - for (auto & c : m_learned) update_psm(*c); - std::stable_sort(m_learned.begin(), m_learned.end(), constraint_glue_psm_lt()); - gc_half("glue-psm"); - cleanup_constraints(m_learned, true); - } - } - - void solver::gc_half(char const* st_name) { - TRACE("ba", tout << "gc\n";); - unsigned sz = m_learned.size(); - unsigned new_sz = sz/2; - unsigned removed = 0; - for (unsigned i = new_sz; i < sz; i++) { - constraint* c = m_learned[i]; - if (!m_constraint_to_reinit.contains(c)) { - remove_constraint(*c, "gc"); - c->deallocate(m_allocator); - ++removed; - } - else { - m_learned[new_sz++] = c; - } - } - m_stats.m_num_gc += removed; - m_learned.shrink(new_sz); - IF_VERBOSE(2, verbose_stream() << "(sat-gc :strategy " << st_name << " :deleted " << removed << ")\n";); - } - - - void solver::gc_vars(unsigned num_vars) { - gc_vars(num_vars, m_constraints); - gc_vars(num_vars, m_learned); - } - - void solver::gc_vars(unsigned num_vars, ptr_vector& cs) { - unsigned j = 0; - for (unsigned i = 0; i < cs.size(); ++i) { - auto* c = cs[i]; - unsigned m = c->fold_max_var(0); - if (m >= num_vars) { - clear_watch(*c); - c->nullify_tracking_literal(*this); - c->deallocate(m_allocator); - } - else - cs[j++] = c; - } - cs.shrink(j); - } - - - lbool solver::add_assign(card& c, literal alit) { - // literal is assigned to false. - unsigned sz = c.size(); - unsigned bound = c.k(); - TRACE("ba", tout << "assign: " << c.lit() << ": " << ~alit << "@" << lvl(~alit) << " " << c << "\n";); - - SASSERT(0 < bound && bound <= sz); - if (bound == sz) { - if (c.lit() != sat::null_literal && value(c.lit()) == l_undef) { - assign(c, ~c.lit()); - return inconsistent() ? l_false : l_true; - } - set_conflict(c, alit); - return l_false; - } - SASSERT(value(alit) == l_false); - VERIFY(c.lit() == sat::null_literal || value(c.lit()) != l_false); - unsigned index = 0; - for (index = 0; index <= bound; ++index) { - if (c[index] == alit) { - break; - } - } - if (index == bound + 1) { - // literal is no longer watched. - return l_undef; - } - VERIFY(index <= bound); - VERIFY(c[index] == alit); - - // find a literal to swap with: - for (unsigned i = bound + 1; i < sz; ++i) { - literal lit2 = c[i]; - if (value(lit2) != l_false) { - c.swap(index, i); - c.watch_literal(*this, lit2); - return l_undef; - } - } - - // conflict - if (bound != index && value(c[bound]) == l_false) { - TRACE("ba", tout << "conflict " << c[bound] << " " << alit << "\n";); - if (c.lit() != sat::null_literal && value(c.lit()) == l_undef) { - if (index + 1 < bound) c.swap(index, bound - 1); - assign(c, ~c.lit()); - return inconsistent() ? l_false : l_true; - } - set_conflict(c, alit); - return l_false; - } - - if (index != bound) { - c.swap(index, bound); - } - - // TRACE("ba", tout << "no swap " << index << " " << alit << "\n";); - // there are no literals to swap with, - // prepare for unit propagation by swapping the false literal into - // position bound. Then literals in positions 0..bound-1 have to be - // assigned l_true. - - if (c.lit() != sat::null_literal && value(c.lit()) == l_undef) { - return l_true; - } - - for (unsigned i = 0; i < bound; ++i) { - assign(c, c[i]); - } - - if (c.learned() && c.glue() > 2) { - unsigned glue; - if (s().num_diff_false_levels_below(c.size(), c.begin(), c.glue()-1, glue)) { - c.set_glue(glue); - } - } - - return inconsistent() ? l_false : l_true; - } - - void solver::asserted(literal l) { - } - - - sat::check_result solver::check() { return sat::check_result::CR_DONE; } - - void solver::push() { - m_constraint_to_reinit_lim.push_back(m_constraint_to_reinit.size()); - } - - void solver::pop(unsigned n) { - TRACE("sat_verbose", tout << "pop:" << n << "\n";); - unsigned new_lim = m_constraint_to_reinit_lim.size() - n; - m_constraint_to_reinit_last_sz = m_constraint_to_reinit_lim[new_lim]; - m_constraint_to_reinit_lim.shrink(new_lim); - m_num_propagations_since_pop = 0; - } - - void solver::pop_reinit() { - unsigned sz = m_constraint_to_reinit_last_sz; - for (unsigned i = sz; i < m_constraint_to_reinit.size(); ++i) { - constraint* c = m_constraint_to_reinit[i]; - if (!init_watch(*c) && !s().at_base_lvl()) { - m_constraint_to_reinit[sz++] = c; - } - } - m_constraint_to_reinit.shrink(sz); - } - - void solver::simplify() { - if (!s().at_base_lvl()) - s().pop_to_base_level(); - if (s().inconsistent()) - return; - unsigned trail_sz = 0, count = 0; - do { - trail_sz = s().init_trail_size(); - m_simplify_change = false; - m_clause_removed = false; - m_constraint_removed = false; - for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) simplify(*m_constraints[i]); - for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) simplify(*m_learned[i]); - init_use_lists(); - remove_unused_defs(); - set_non_external(); - elim_pure(); - for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) subsumption(*m_constraints[i]); - for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) subsumption(*m_learned[i]); - unit_strengthen(); - cleanup_clauses(); - cleanup_constraints(); - - count++; - } - while (count < 10 && (m_simplify_change || trail_sz < s().init_trail_size())); - - gc(); - - // validate_eliminated(); - - IF_VERBOSE(1, - unsigned subs = m_stats.m_num_bin_subsumes + m_stats.m_num_clause_subsumes + m_stats.m_num_pb_subsumes; - verbose_stream() << "(ba.simplify" << " :constraints " << m_constraints.size(); - if (!m_learned.empty()) verbose_stream() << " :lemmas " << m_learned.size(); - if (subs > 0) verbose_stream() << " :subsumes " << subs; - if (m_stats.m_num_gc > 0) verbose_stream() << " :gc " << m_stats.m_num_gc; - verbose_stream() << ")\n";); - - // IF_VERBOSE(0, s().display(verbose_stream())); - // mutex_reduction(); - // if (s().m_clauses.size() < 80000) lp_lookahead_reduction(); - } - - void solver::mutex_reduction() { - literal_vector lits; - for (unsigned v = 0; v < s().num_vars(); ++v) { - lits.push_back(literal(v, false)); - lits.push_back(literal(v, true)); - } - vector mutexes; - s().find_mutexes(lits, mutexes); - for (literal_vector& mux : mutexes) { - if (mux.size() > 2) { - IF_VERBOSE(1, verbose_stream() << "mux: " << mux << "\n";); - for (unsigned i = 0; i < mux.size(); ++i) mux[i].neg(); - add_at_least(sat::null_literal, mux, mux.size() - 1, false); - } - } - } - - // ------------------------- - // sorting networks - literal solver::ba_sort::mk_false() { - return ~mk_true(); - } - - literal solver::ba_sort::mk_true() { - if (m_true == sat::null_literal) { - bool_var v = s.s().mk_var(false, false); - m_true = literal(v, false); - s.s().mk_clause(1,&m_true); - } - VERIFY(m_true != sat::null_literal); - return m_true; - } - - literal solver::ba_sort::mk_not(literal l) { - return ~l; - } - - literal solver::ba_sort::fresh(char const*) { - bool_var v = s.s().mk_var(false, true); - return literal(v, false); - } - - - literal solver::ba_sort::mk_max(unsigned n, literal const* lits) { - m_lits.reset(); - for (unsigned i = 0; i < n; ++i) { - if (lits[i] == m_true) return m_true; - if (lits[i] == ~m_true) continue; - m_lits.push_back(lits[i]); - } - switch (m_lits.size()) { - case 0: - return ~m_true; - case 1: - return m_lits[0]; - default: { - literal max = fresh("max"); - for (unsigned i = 0; i < n; ++i) { - s.s().mk_clause(~m_lits[i], max); - } - m_lits.push_back(~max); - s.s().mk_clause(m_lits.size(), m_lits.data()); - return max; - } - } - } - - literal solver::ba_sort::mk_min(unsigned n, literal const* lits) { - m_lits.reset(); - for (unsigned i = 0; i < n; ++i) { - if (lits[i] == ~m_true) return ~m_true; - if (lits[i] == m_true) continue; - m_lits.push_back(lits[i]); - } - switch (m_lits.size()) { - case 0: - return m_true; - case 1: - return m_lits[0]; - default: { - literal min = fresh("min"); - for (unsigned i = 0; i < n; ++i) { - s.s().mk_clause(~min, m_lits[i]); - m_lits[i] = ~m_lits[i]; - } - m_lits.push_back(min); - s.s().mk_clause(m_lits.size(), m_lits.data()); - return min; - } - } - } - - void solver::ba_sort::mk_clause(unsigned n, literal const* lits) { - m_lits.reset(); - m_lits.append(n, lits); - s.s().mk_clause(n, m_lits.data()); - } - - std::ostream& solver::ba_sort::pp(std::ostream& out, literal l) const { - return out << l; - } - - - // ------------------------------- - // set literals equivalent - - void solver::reserve_roots() { - m_root_vars.reserve(s().num_vars(), false); - for (unsigned i = m_roots.size(); i < 2 * s().num_vars(); ++i) { - m_roots.push_back(sat::to_literal(i)); - } - } - - bool solver::set_root(literal l, literal r) { - if (s().is_assumption(l.var())) { - return false; - } - reserve_roots(); - m_roots[l.index()] = r; - m_roots[(~l).index()] = ~r; - m_root_vars[l.var()] = true; - return true; - } - - void solver::flush_roots() { - if (m_roots.empty()) return; - reserve_roots(); - // validate(); - m_constraint_removed = false; - for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) - flush_roots(*m_constraints[i]); - for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) - flush_roots(*m_learned[i]); - cleanup_constraints(); - // validate(); - - // validate_eliminated(); - } - - void solver::validate_eliminated() { - validate_eliminated(m_constraints); - validate_eliminated(m_learned); - } - - void solver::validate_eliminated(ptr_vector const& cs) { - for (constraint const* c : cs) { - if (c->learned()) continue; - for (auto l : constraint::literal_iterator(*c)) - VERIFY(!s().was_eliminated(l.var())); - } - } - - void solver::recompile(constraint& c) { - if (c.id() == _bad_id) { - IF_VERBOSE(0, display(verbose_stream() << "recompile\n", c, true);); - } - switch (c.tag()) { - case pb::tag_t::card_t: - recompile(c.to_card()); - break; - case pb::tag_t::pb_t: - recompile(c.to_pb()); - break; - default: - UNREACHABLE(); - } - } - - void solver::recompile(card& c) { - SASSERT(c.lit() == sat::null_literal || c.is_watched(*this, c.lit())); - - // pre-condition is that the literals, except c.lit(), in c are unwatched. - if (c.id() == _bad_id) std::cout << "recompile: " << c << "\n"; - m_weights.resize(2*s().num_vars(), 0); - for (literal l : c) { - ++m_weights[l.index()]; - } - unsigned k = c.k(); - bool all_units = true; - unsigned sz = c.size(); - unsigned_vector coeffs; - literal_vector lits; - unsigned j = 0; - for (unsigned i = 0; i < sz && 0 < k; ++i) { - literal l = c[i]; - unsigned w = m_weights[l.index()]; - unsigned w2 = m_weights[(~l).index()]; - if (w == 0 || w < w2) { - continue; - } - else if (k <= w2) { - k = 0; - break; - } - else { - SASSERT(w2 <= w && w2 < k); - k -= w2; - w -= w2; - m_weights[(~l).index()] = 0; - m_weights[l.index()] = 0; - if (w == 0) { - continue; - } - else { - all_units &= (w == 1); - coeffs.push_back(w); - c[j++] = l; - } - } - } - sz = j; - - // clear weights - for (literal l : c) { - m_weights[l.index()] = 0; - m_weights[(~l).index()] = 0; - } - - if (k == 0 && c.lit() == sat::null_literal) { - remove_constraint(c, "recompiled to true"); - return; - } - - if (k == 1 && c.lit() == sat::null_literal) { - literal_vector lits(sz, c.literals().data()); - s().mk_clause(sz, lits.data(), sat::status::th(c.learned(), get_id())); - remove_constraint(c, "recompiled to clause"); - return; - } - - if (sz == 0) { - if (c.lit() == sat::null_literal) { - if (k > 0) { - s().mk_clause(0, nullptr, sat::status::th(false, get_id())); - } - } - else if (k > 0) { - literal lit = ~c.lit(); - s().mk_clause(1, &lit, sat::status::th(c.learned(), get_id())); - } - else { - literal lit = c.lit(); - s().mk_clause(1, &lit, sat::status::th(c.learned(), get_id())); - } - remove_constraint(c, "recompiled to clause"); - return; - } - if (all_units && sz < k) { - if (c.lit() == sat::null_literal) { - s().mk_clause(0, nullptr, sat::status::th(c.learned(), get_id())); - } - else { - literal lit = ~c.lit(); - s().mk_clause(1, &lit, sat::status::th(c.learned(), get_id())); - } - remove_constraint(c, "recompiled to clause"); - return; - } - VERIFY(!all_units || c.size() - c.k() >= sz - k); - c.set_size(sz); - c.set_k(k); - - if (all_units && clausify(c)) { - return; - } - - if (!all_units) { - TRACE("ba", tout << "replacing by pb: " << c << "\n";); - m_wlits.reset(); - for (unsigned i = 0; i < sz; ++i) { - m_wlits.push_back(wliteral(coeffs[i], c[i])); - } - literal root = c.lit(); - remove_constraint(c, "recompiled to pb"); - add_pb_ge(root, m_wlits, k, c.learned()); - } - else { - if (c.lit() == sat::null_literal || value(c.lit()) == l_true) { - init_watch(c); - } - SASSERT(c.lit() == sat::null_literal || c.is_watched(*this, c.lit())); - SASSERT(c.well_formed()); - } - } - - bool solver::clausify(literal lit, unsigned n, literal const* lits, unsigned k) { - return false; - bool is_def = lit != sat::null_literal; - if ((!is_def || !s().was_eliminated(lit)) && - !std::any_of(lits, lits + n, [&](literal l) { return s().was_eliminated(l); })) { - literal def_lit = m_sort.ge(is_def, k, n, lits); - if (is_def) { - s().mk_clause(~lit, def_lit); - s().mk_clause( lit, ~def_lit); - } - return true; - } - return false; - } - - - bool solver::clausify(card& c) { - return false; - if (get_config().m_card_solver) - return false; - - // - // TBD: conditions for when to clausify are TBD and - // handling of conditional cardinality as well. - // - if (!c.learned() && clausify(c.lit(), c.size(), c.begin(), c.k())) { - IF_VERBOSE(1, verbose_stream() << "clausify " << c << "\n";); - // compiled - } - remove_constraint(c, "recompiled to clauses"); - return true; - } - - bool solver::clausify(pbc& p) { - return false; - if (get_config().m_card_solver) - return false; - - bool ok = !p.learned(); - bool is_def = p.lit() != sat::null_literal; - for (wliteral wl : p) { - ok &= !s().was_eliminated(wl.second); - } - ok &= !is_def || !s().was_eliminated(p.lit()); - if (!ok) { - remove_constraint(p, "recompiled to clauses"); - return true; - } - - if (is_cardinality(p, m_lemma)) { - literal lit = m_sort.ge(is_def, p.k(), m_lemma.size(), m_lemma.data()); - if (is_def) { - s().mk_clause(p.lit(), ~lit); - s().mk_clause(~p.lit(), lit); - } - remove_constraint(p, "recompiled to clauses"); - return true; - } - return false; - } - - bool solver::is_cardinality(pbc const& p, literal_vector& lits) { - lits.reset(); - p.size(); - for (wliteral wl : p) { - if (lits.size() > 2*p.size() + wl.first) { - return false; - } - for (unsigned i = 0; i < wl.first; ++i) { - lits.push_back(wl.second); - } - } - return true; - } - - void solver::flush_roots(constraint& c) { - if (c.lit() != sat::null_literal && !c.is_watched(*this, c.lit())) { - c.watch_literal(*this, c.lit()); - c.watch_literal(*this, ~c.lit()); - } - SASSERT(c.lit() == sat::null_literal || c.is_watched(*this, c.lit())); - bool found = c.lit() != sat::null_literal && m_root_vars[c.lit().var()]; - for (unsigned i = 0; !found && i < c.size(); ++i) { - found = m_root_vars[c.get_lit(i).var()]; - } - if (!found) return; - clear_watch(c); - - // this could create duplicate literals - for (unsigned i = 0; i < c.size(); ++i) { - literal lit = m_roots[c.get_lit(i).index()]; - c.set_lit(i, lit); - } - - literal root = c.lit(); - if (root != sat::null_literal && m_roots[root.index()] != root) { - root = m_roots[root.index()]; - c.nullify_tracking_literal(*this); - c.update_literal(root); - c.watch_literal(*this, root); - c.watch_literal(*this, ~root); - } - - bool found_dup = false; - bool found_root = false; - init_visited(); - for (unsigned i = 0; i < c.size(); ++i) { - literal l = c.get_lit(i); - if (is_visited(l)) { - found_dup = true; - break; - } - else { - mark_visited(l); - mark_visited(~l); - } - } - for (unsigned i = 0; i < c.size(); ++i) { - found_root |= c.get_lit(i).var() == root.var(); - } - - if (found_root) { - split_root(c); - c.negate(); - split_root(c); - remove_constraint(c, "flush roots"); - } - else if (found_dup) { - recompile(c); - } - else { - if (c.lit() == sat::null_literal || value(c.lit()) != l_undef) init_watch(c); - SASSERT(c.well_formed()); - } - } - - unsigned solver::get_num_unblocked_bin(literal l) { - return s().m_simplifier.num_nonlearned_bin(l); - } - - /* - \brief garbage collection. - This entails - - finding pure literals, - - setting literals that are not used in the extension to non-external. - - subsumption - - resolution - - blocked literals - */ - void solver::init_use_lists() { - m_clause_use_list.init(s().num_vars()); - m_cnstr_use_list.reset(); - m_cnstr_use_list.resize(2*s().num_vars()); - for (sat::clause* c : s().m_clauses) { - if (!c->frozen()) - m_clause_use_list.insert(*c); - } - for (constraint* cp : m_constraints) { - literal lit = cp->lit(); - if (lit != sat::null_literal) { - m_cnstr_use_list[lit.index()].push_back(cp); - m_cnstr_use_list[(~lit).index()].push_back(cp); - } - for (literal l : constraint::literal_iterator(*cp)) { - m_cnstr_use_list[l.index()].push_back(cp); - if (lit != sat::null_literal) m_cnstr_use_list[(~l).index()].push_back(cp); - } - } - } - - void solver::remove_unused_defs() { - if (incremental_mode()) return; - // remove constraints where indicator literal isn't used. - for (constraint* cp : m_constraints) { - constraint& c = *cp; - literal lit = c.lit(); - if (lit != sat::null_literal && - value(lit) == l_undef && - use_count(lit) == 1 && - use_count(~lit) == 1 && - get_num_unblocked_bin(lit) == 0 && - get_num_unblocked_bin(~lit) == 0) { - remove_constraint(c, "unused def"); - } - } - } - - bool solver::incremental_mode() const { - sat_simplifier_params p(s().m_params); - bool incremental_mode = s().get_config().m_incremental && !p.override_incremental(); - incremental_mode |= s().tracking_assumptions(); - return incremental_mode; - } - - unsigned solver::set_non_external() { - // set variables to be non-external if they are not used in theory constraints. - unsigned ext = 0; - if (!incremental_mode() && s().get_extension() == this) { - for (unsigned v = 0; v < s().num_vars(); ++v) { - literal lit(v, false); - if (s().is_external(v) && - m_cnstr_use_list[lit.index()].empty() && - m_cnstr_use_list[(~lit).index()].empty()) { - s().set_non_external(v); - ++ext; - } - } - } - // ensure that lemmas use only non-eliminated variables - for (constraint* cp : m_learned) { - constraint& c = *cp; - if (c.was_removed()) continue; - SASSERT(c.lit() == sat::null_literal); - for (unsigned i = 0; i < c.size(); ++i) { - bool_var v = c.get_lit(i).var(); - if (s().was_eliminated(v)) { - remove_constraint(c, "contains eliminated var"); - break; - } - } - } - return ext; - } - - bool solver::elim_pure(literal lit) { - if (value(lit) == l_undef && !m_cnstr_use_list[lit.index()].empty() && - use_count(~lit) == 0 && get_num_unblocked_bin(~lit) == 0) { - IF_VERBOSE(100, verbose_stream() << "pure literal: " << lit << "\n";); - s().assign_scoped(lit); - return true; - } - return false; - } - - unsigned solver::elim_pure() { - if (!get_config().m_elim_vars || incremental_mode()) { - return 0; - } - // eliminate pure literals - unsigned pure_literals = 0; - for (unsigned v = 0; v < s().num_vars(); ++v) { - literal lit(v, false); - if (value(v) != l_undef) continue; - if (m_cnstr_use_list[lit.index()].empty() && - m_cnstr_use_list[(~lit).index()].empty()) continue; - - if (elim_pure(lit) || elim_pure(~lit)) { - ++pure_literals; - } - } - return pure_literals; - } - - /** - * Strengthen inequalities using binary implication information. - * - * x -> ~y, x -> ~z, y + z + u >= 2 - * ---------------------------------- - * y + z + u + ~x >= 3 - * - * for c : constraints - * for l : c: - * slack <- of c under root(~l) - * if slack < 0: - * add ~root(~l) to c, k <- k + 1 - */ - void solver::unit_strengthen() { - sat::big big(s().m_rand); - big.init(s(), true); - for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) - unit_strengthen(big, *m_constraints[i]); - for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) - unit_strengthen(big, *m_learned[i]); - } - - void solver::unit_strengthen(sat::big& big, constraint& p) { - if (p.lit() != sat::null_literal) return; - unsigned sz = p.size(); - for (unsigned i = 0; i < sz; ++i) { - literal u = p.get_lit(i); - literal r = big.get_root(u); - if (r == u) continue; - unsigned k = p.k(), b = 0; - for (unsigned j = 0; j < sz; ++j) { - literal v = p.get_lit(j); - if (r == big.get_root(v)) { - b += p.get_coeff(j); - } - } - if (b > k) { - r.neg(); - unsigned coeff = b - k; - - svector wlits; - // add coeff * r to p - wlits.push_back(wliteral(coeff, r)); - for (unsigned j = 0; j < sz; ++j) { - u = p.get_lit(j); - unsigned c = p.get_coeff(j); - if (r == u) { - wlits[0].first += c; - } - else if (~r == u) { - if (coeff == c) { - wlits[0] = wlits.back(); - wlits.pop_back(); - b -= c; - } - else if (coeff < c) { - wlits[0].first = c - coeff; - wlits[0].second.neg(); - b -= coeff; - } - else { - // coeff > c - wlits[0].first = coeff - c; - b -= c; - } - } - else { - wlits.push_back(wliteral(c, u)); - } - } - ++m_stats.m_num_big_strengthenings; - p.set_removed(); - add_pb_ge(sat::null_literal, wlits, b, p.learned()); - return; - } - } - } - - void solver::subsumption(constraint& cnstr) { - if (cnstr.was_removed()) - return; - if (cnstr.k() <= 1) - return; - switch (cnstr.tag()) { - case pb::tag_t::card_t: - subsumption(cnstr.to_card()); - break; - case pb::tag_t::pb_t: - subsumption(cnstr.to_pb()); - break; - } - } - - void solver::init_visited() { s().init_visited(); } - void solver::mark_visited(literal l) { s().mark_visited(l); } - void solver::mark_visited(bool_var v) { s().mark_visited(v); } - bool solver::is_visited(bool_var v) const { return s().is_visited(v); } - bool solver::is_visited(literal l) const { return s().is_visited(l); } - - void solver::cleanup_clauses() { - if (m_clause_removed) { - cleanup_clauses(s().m_clauses); - cleanup_clauses(s().m_learned); - } - } - - typedef sat::clause_vector clause_vector; - typedef sat::clause clause; - - void solver::cleanup_clauses(clause_vector& clauses) { - // version in simplify first clears - // all watch literals, then reinserts them. - // this ensures linear time cleanup. - clause_vector::iterator it = clauses.begin(); - clause_vector::iterator end = clauses.end(); - clause_vector::iterator it2 = it; - for (; it != end; ++it) { - clause* c = *it; - if (c->was_removed() && s().can_delete(*c)) { - s().detach_clause(*c); - s().del_clause(*c); - } - else { - if (it2 != it) { - *it2 = *it; - } - ++it2; - } - } - clauses.set_end(it2); - } - - void solver::cleanup_constraints() { - if (m_constraint_removed) { - cleanup_constraints(m_constraints, false); - cleanup_constraints(m_learned, true); - m_constraint_removed = false; - } - } - - void solver::cleanup_constraints(ptr_vector& cs, bool learned) { - ptr_vector::iterator it = cs.begin(); - ptr_vector::iterator it2 = it; - ptr_vector::iterator end = cs.end(); - for (; it != end; ++it) { - constraint& c = *(*it); - if (c.was_removed()) { - clear_watch(c); - c.nullify_tracking_literal(*this); - c.deallocate(m_allocator); - } - else if (learned && !c.learned()) { - m_constraints.push_back(&c); - } - else { - if (it != it2) { - *it2 = *it; - } - ++it2; - } - } - cs.set_end(it2); - } - - - /* - \brief subsumption between two cardinality constraints - - A >= k subsumes A + B >= k' for k' <= k - - A + A' >= k subsumes A + B >= k' for k' + |A'| <= k - - A + lit >= k self subsumes A + ~lit + B >= k' into A + B >= k' for k' <= k - - version that generalizes self-subsumption to more than one literal - A + ~L + B >= k' => A + B >= k' if A + A' + L >= k and k' + |L| + |A'| <= k - */ - bool solver::subsumes(card& c1, card& c2, literal_vector & comp) { - if (c2.lit() != sat::null_literal) return false; - - unsigned c2_exclusive = 0; - unsigned common = 0; - comp.reset(); - for (literal l : c2) { - if (is_visited(l)) { - ++common; - } - else if (is_visited(~l)) { - comp.push_back(l); - } - else { - ++c2_exclusive; - } - } - - unsigned c1_exclusive = c1.size() - common - comp.size(); - return c1_exclusive + c2.k() + comp.size() <= c1.k(); - } - - /* - \brief L + A >= k subsumes L + C if |A| < k - A + L + B >= k self-subsumes A + ~L + C >= 1 - if k + 1 - |B| - |C| - |L| > 0 - */ - bool solver::subsumes(card& c1, sat::clause& c2, bool& self) { - unsigned common = 0, complement = 0, c2_exclusive = 0; - self = false; - - for (literal l : c2) { - if (is_visited(l)) { - ++common; - } - else if (is_visited(~l)) { - ++complement; - } - else { - ++c2_exclusive; - } - } - unsigned c1_exclusive = c1.size() - common - complement; - if (complement > 0 && c1.k() + 1 > c1_exclusive + c2_exclusive + common) { - self = true; - return true; - } - return c1.size() - common < c1.k(); - } - - /* - \brief Ax >= k subsumes By >= k' if - all coefficients in A are <= B and k >= k' - */ - bool solver::subsumes(pbc const& p1, constraint const& p2) { - if (p1.k() < p2.k() || p1.size() > p2.size()) return false; - unsigned num_sub = 0; - for (unsigned i = 0; i < p2.size(); ++i) { - literal l = p2.get_lit(i); - if (is_visited(l) && m_weights[l.index()] <= p2.get_coeff(i)) { - ++num_sub; - } - if (p1.size() + i > p2.size() + num_sub) return false; - } - return num_sub == p1.size(); - } - - void solver::subsumes(pbc& p1, literal lit) { - for (constraint* c : m_cnstr_use_list[lit.index()]) { - if (c == &p1 || c->was_removed()) continue; - bool s = false; - switch (c->tag()) { - case pb::tag_t::card_t: - s = subsumes(p1, c->to_card()); - break; - case pb::tag_t::pb_t: - s = subsumes(p1, c->to_pb()); - break; - default: - break; - } - if (s) { - ++m_stats.m_num_pb_subsumes; - set_non_learned(p1); - remove_constraint(*c, "subsumed"); - } - } - } - - literal solver::get_min_occurrence_literal(card const& c) { - unsigned occ_count = UINT_MAX; - literal lit = sat::null_literal; - for (literal l : c) { - unsigned occ_count1 = m_cnstr_use_list[l.index()].size(); - if (occ_count1 < occ_count) { - lit = l; - occ_count = occ_count1; - } - } - return lit; - } - - void solver::card_subsumption(card& c1, literal lit) { - literal_vector slit; - for (constraint* c : m_cnstr_use_list[lit.index()]) { - if (!c->is_card() || c == &c1 || c->was_removed()) { - continue; - } - card& c2 = c->to_card(); - - SASSERT(&c1 != &c2); - if (subsumes(c1, c2, slit)) { - if (slit.empty()) { - TRACE("ba", tout << "subsume cardinality\n" << c1 << "\n" << c2 << "\n";); - remove_constraint(c2, "subsumed"); - ++m_stats.m_num_pb_subsumes; - set_non_learned(c1); - } - else { - TRACE("ba", tout << "self subsume cardinality\n";); - IF_VERBOSE(11, - verbose_stream() << "self-subsume cardinality\n"; - verbose_stream() << c1 << "\n"; - verbose_stream() << c2 << "\n";); - clear_watch(c2); - unsigned j = 0; - for (unsigned i = 0; i < c2.size(); ++i) { - if (!is_visited(~c2[i])) { - c2[j++] = c2[i]; - } - } - c2.set_size(j); - init_watch(c2); - m_simplify_change = true; - } - } - } - } - - void solver::clause_subsumption(card& c1, literal lit, sat::clause_vector& removed_clauses) { - SASSERT(!c1.was_removed()); - sat::clause_use_list& occurs = m_clause_use_list.get(lit); - sat::clause_use_list::iterator it = occurs.mk_iterator(); - while (!it.at_end()) { - sat::clause& c2 = it.curr(); - bool self; - if (!c2.was_removed() && subsumes(c1, c2, self)) { - if (self) { - // self-subsumption is TBD - } - else { - TRACE("ba", tout << "remove\n" << c1 << "\n" << c2 << "\n";); - removed_clauses.push_back(&c2); - ++m_stats.m_num_clause_subsumes; - set_non_learned(c1); - } - } - it.next(); - } - } - - void solver::set_non_learned(constraint& c) { - literal lit = c.lit(); - if (lit != sat::null_literal) { - s().set_external(lit.var()); - } - for (literal lit : constraint::literal_iterator(c)) { - s().set_external(lit.var()); - SASSERT(!s().was_eliminated(lit.var())); - } - c.set_learned(false); - } - - typedef sat::watch_list watch_list; - - void solver::binary_subsumption(card& c1, literal lit) { - if (c1.k() + 1 != c1.size()) return; - SASSERT(is_visited(lit)); - SASSERT(!c1.was_removed()); - watch_list & wlist = get_wlist(~lit); - watch_list::iterator it = wlist.begin(); - watch_list::iterator it2 = it; - watch_list::iterator end = wlist.end(); - for (; it != end; ++it) { - sat::watched w = *it; - if (w.is_binary_clause() && is_visited(w.get_literal())) { - ++m_stats.m_num_bin_subsumes; - IF_VERBOSE(20, verbose_stream() << c1 << " subsumes (" << lit << " " << w.get_literal() << ")\n";); - if (!w.is_learned()) { - set_non_learned(c1); - } - } - else { - if (it != it2) { - *it2 = *it; - } - ++it2; - } - } - wlist.set_end(it2); - } - - void solver::subsumption(card& c1) { - if (c1.was_removed() || c1.lit() != sat::null_literal) { - return; - } - sat::clause_vector removed_clauses; - init_visited(); - for (literal l : c1) mark_visited(l); - for (unsigned i = 0; i < std::min(c1.size(), c1.k() + 1); ++i) { - literal lit = c1[i]; - card_subsumption(c1, lit); - clause_subsumption(c1, lit, removed_clauses); - binary_subsumption(c1, lit); - } - m_clause_removed |= !removed_clauses.empty(); - for (clause *c : removed_clauses) { - c->set_removed(true); - m_clause_use_list.erase(*c); - } - } - - void solver::subsumption(pbc& p1) { - if (p1.was_removed() || p1.lit() != sat::null_literal) { - return; - } - init_visited(); - for (wliteral l : p1) { - SASSERT(m_weights.size() <= l.second.index() || m_weights[l.second.index()] == 0); - m_weights.setx(l.second.index(), l.first, 0); - mark_visited(l.second); - } - for (unsigned i = 0; i < std::min(10u, p1.num_watch()); ++i) { - unsigned j = s().m_rand() % p1.num_watch(); - subsumes(p1, p1[j].second); - } - for (wliteral l : p1) { - m_weights[l.second.index()] = 0; - } - } - - void solver::clauses_modifed() {} - - lbool solver::get_phase(bool_var v) { return l_undef; } - - /* - \brief lit <=> conjunction of unconstrained lits - */ - void solver::assert_unconstrained(literal lit, literal_vector const& lits) { - if (lit == sat::null_literal) { - for (literal l : lits) { - if (value(l) == l_undef) { - s().assign_scoped(l); - } - } - } - else { - // add clauses for: lit <=> conjunction of undef literals - SASSERT(value(lit) == l_undef); - literal_vector cl; - cl.push_back(lit); - for (literal l : lits) { - if (value(l) == l_undef) { - s().mk_clause(~lit, l); - cl.push_back(~l); - } - } - s().mk_clause(cl); - } - } - - sat::extension* solver::copy(sat::solver* s) { - return clone_aux(m, *s, si, m_id); - } - - euf::th_solver* solver::clone(euf::solver& new_ctx) { - return clone_aux(new_ctx.get_manager(), new_ctx.s(), new_ctx.get_si(), get_id()); - } - - euf::th_solver* solver::clone_aux(ast_manager& m, sat::solver& s, sat::sat_internalizer& si, euf::theory_id id) { - solver* result = alloc(solver, m, si, id); - result->set_solver(&s); - copy_constraints(result, m_constraints); - return result; - } - - void solver::copy_constraints(solver* result, ptr_vector const& constraints) { - literal_vector lits; - svector wlits; - for (constraint* cp : constraints) { - switch (cp->tag()) { - case pb::tag_t::card_t: { - card const& c = cp->to_card(); - lits.reset(); - for (literal l : c) lits.push_back(l); - result->add_at_least(c.lit(), lits, c.k(), c.learned()); - break; - } - case pb::tag_t::pb_t: { - pbc const& p = cp->to_pb(); - wlits.reset(); - for (wliteral w : p) { - wlits.push_back(w); - } - result->add_pb_ge(p.lit(), wlits, p.k(), p.learned()); - break; - } - default: - UNREACHABLE(); - } - } - } - - void solver::init_use_list(sat::ext_use_list& ul) { - ul.init(s().num_vars()); - for (constraint const* cp : m_constraints) { - sat::ext_constraint_idx idx = cp->cindex(); - if (cp->lit() != sat::null_literal) { - ul.insert(cp->lit(), idx); - ul.insert(~cp->lit(), idx); - } - cp->init_use_list(ul); - } - } - - // - // literal is used in a clause (C or l), it - // it occurs negatively in constraint c. - // all literals in C are marked - // - bool solver::is_blocked(literal l, sat::ext_constraint_idx idx) { - constraint const& c = index2constraint(idx); - sat::simplifier& sim = s().m_simplifier; - if (c.lit() != sat::null_literal) return false; - return c.is_blocked(sim, l); - } - - - void solver::find_mutexes(literal_vector& lits, vector & mutexes) { - sat::literal_set slits(lits); - bool change = false; - for (constraint* cp : m_constraints) { - if (!cp->is_card()) continue; - card const& c = cp->to_card(); - if (c.size() == c.k() + 1) { - literal_vector mux; - for (literal lit : c) { - if (slits.contains(~lit)) { - mux.push_back(~lit); - } - } - if (mux.size() <= 1) { - continue; - } - - for (literal m : mux) { - slits.remove(m); - } - change = true; - mutexes.push_back(mux); - } - } - if (!change) return; - lits.reset(); - for (literal l : slits) { - lits.push_back(l); - } - } - - void solver::display(std::ostream& out, ineq const& ineq, bool values) const { - for (unsigned i = 0; i < ineq.size(); ++i) { - if (ineq.coeff(i) != 1) out << ineq.coeff(i) << "*"; - out << ineq.lit(i) << " "; - if (values) out << value(ineq.lit(i)) << " "; - } - out << ">= " << ineq.m_k << "\n"; - } - - - std::ostream& solver::display(std::ostream& out) const { - for (constraint const* c : m_constraints) { - out << (*c) << "\n"; - } - if (!m_learned.empty()) { - out << "learned:\n"; - } - for (constraint const* c : m_learned) { - out << (*c) << "\n"; - } - return out; - } - - std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const { - return out << index2constraint(idx); - } - - std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const { - return out << index2constraint(idx); - } - - std::ostream& solver::display(std::ostream& out, constraint const& c, bool values) const { - return c.display(out, *this, values); - } - - void solver::collect_statistics(statistics& st) const { - st.update("pb propagations", m_stats.m_num_propagations); - st.update("pb conflicts", m_stats.m_num_conflicts); - st.update("pb resolves", m_stats.m_num_resolves); - st.update("pb cuts", m_stats.m_num_cut); - st.update("pb gc", m_stats.m_num_gc); - st.update("pb overflow", m_stats.m_num_overflow); - st.update("pb big strengthenings", m_stats.m_num_big_strengthenings); - st.update("pb lemmas", m_stats.m_num_lemmas); - st.update("pb subsumes", m_stats.m_num_bin_subsumes + m_stats.m_num_clause_subsumes + m_stats.m_num_pb_subsumes); - } - - - bool solver::validate_unit_propagation(pbc const& p, literal_vector const& r, literal alit) const { - // all elements of r are true, - for (literal l : r) { - if (value(l) != l_true) { - IF_VERBOSE(0, verbose_stream() << "value of " << l << " is " << value(l) << "\n"; - display(verbose_stream(), p, true);); - return false; - } - if (value(alit) == l_true && lvl(l) > lvl(alit)) { - IF_VERBOSE(0, - verbose_stream() << "level of premise " << l << " is " << lvl(l) << "\n"; - verbose_stream() << "level of asserting literal " << alit << " is " << lvl(alit) << "\n"; - display(verbose_stream(), p, true);); - return false; - } - // if (value(alit) == l_true && lvl(l) == lvl(alit)) { - // std::cout << "same level " << alit << " " << l << "\n"; - // } - } - // the sum of elements not in r or alit add up to less than k. - unsigned sum = 0; - // - // a*x + b*alit + c*r >= k - // sum a < k - // val(r) = false - // hence alit has to be true. - for (wliteral wl : p) { - literal lit = wl.second; - if (lit != alit && !r.contains(~lit)) { - sum += wl.first; - } - } - if (sum >= p.k()) { - IF_VERBOSE(0, - verbose_stream() << "sum is " << sum << " >= " << p.k() << "\n"; - display(verbose_stream(), p, true); - verbose_stream() << "id: " << p.id() << "\n"; - sum = 0; - for (wliteral wl : p) sum += wl.first; - verbose_stream() << "overall sum " << sum << "\n"; - verbose_stream() << "asserting literal: " << alit << "\n"; - verbose_stream() << "reason: " << r << "\n";); - return false; - } - for (wliteral wl : p) { - if (alit == wl.second) { - return true; - } - } - IF_VERBOSE(0, verbose_stream() << alit << " not found among literals\n";); - return false; - } - - - bool solver::validate_lemma() { - int64_t bound64 = m_bound; - int64_t val = -bound64; - reset_active_var_set(); - for (bool_var v : m_active_vars) { - if (!test_and_set_active(v)) continue; - wliteral wl = get_wliteral(v); - if (wl.first == 0) continue; - if (!is_false(wl.second)) { - val += wl.first; - } - } - CTRACE("ba", val >= 0, active2pb(m_A); display(tout, m_A, true);); - return val < 0; - } - - /** - * the slack of inequalities on the stack should be non-positive. - */ - bool solver::validate_ineq(ineq const& ineq) const { - int64_t k = -static_cast(ineq.m_k); - for (wliteral wl : ineq.m_wlits) { - if (!is_false(wl.second)) - k += wl.first; - } - CTRACE("ba", k > 0, display(tout, ineq, true);); - return k <= 0; - } - - void solver::reset_active_var_set() { - while (!m_active_var_set.empty()) m_active_var_set.erase(); - } - - bool solver::test_and_set_active(bool_var v) { - if (m_active_var_set.contains(v)) { - return false; - } - else { - m_active_var_set.insert(v); - return true; - } - } - - void solver::active2pb(ineq& p) { - p.reset(m_bound); - active2wlits(p.m_wlits); - } - - void solver::active2wlits() { - m_wlits.reset(); - active2wlits(m_wlits); - } - - void solver::active2wlits(svector& wlits) { - uint64_t sum = 0; - reset_active_var_set(); - for (bool_var v : m_active_vars) { - if (!test_and_set_active(v)) continue; - wliteral wl = get_wliteral(v); - if (wl.first == 0) continue; - wlits.push_back(wl); - sum += wl.first; - } - m_overflow |= sum >= UINT_MAX/2; - } - - constraint* solver::active2lemma() { - switch (get_config().m_pb_lemma_format) { - case sat::PB_LEMMA_CARDINALITY: - return active2card(); - case sat::PB_LEMMA_PB: - return active2constraint(); - default: - UNREACHABLE(); - return nullptr; - } - } - - constraint* solver::active2constraint() { - active2wlits(); - if (m_overflow) { - return nullptr; - } - constraint* c = add_pb_ge(sat::null_literal, m_wlits, m_bound, true); - TRACE("ba", if (c) display(tout, *c, true);); - ++m_stats.m_num_lemmas; - return c; - } - - /* - Chai Kuhlmann: - - a1*l1 + ... + a_n*l_n >= k - s.t. - a1 >= a2 >= .. >= a_n - - let m be such that - - sum_{i = 1}^{m-1} a_i < k <= sum_{i = 1}^{m} - - then - - l1 + ... + l_n >= m - - furthermore, for the largest n' <= n, such that - - sum_{i = n'+1}^n a_i + sum_{i = 1}^{m-1} a_i < k - - then - - l1 + ... + l_n' >= m - - */ - struct compare_wlit { - bool operator()(wliteral l1, wliteral l2) const { - return l1.first > l2.first; - } - }; - - - constraint* solver::active2card() { - active2wlits(); - if (m_overflow) { - return nullptr; - } - std::sort(m_wlits.begin(), m_wlits.end(), compare_wlit()); - unsigned k = 0; - uint64_t sum = 0, sum0 = 0; - for (wliteral wl : m_wlits) { - if (sum >= m_bound) break; - sum0 = sum; - sum += wl.first; - ++k; - } - if (k == 1) { - return nullptr; - } - while (!m_wlits.empty()) { - wliteral wl = m_wlits.back(); - if (wl.first + sum0 >= m_bound) break; - m_wlits.pop_back(); - sum0 += wl.first; - } - - unsigned slack = 0; - unsigned max_level = 0; - unsigned num_max_level = 0; - for (wliteral wl : m_wlits) { - if (value(wl.second) != l_false) ++slack; - unsigned level = lvl(wl.second); - if (level > max_level) { - max_level = level; - num_max_level = 1; - } - else if (max_level == level) { - ++num_max_level; - } - } - if (m_overflow) { - return nullptr; - } - - if (slack >= k) { -#if 0 - return active2constraint(); - active2pb(m_A); - std::cout << "not asserting\n"; - display(std::cout, m_A, true); -#endif - return nullptr; - } - - // produce asserting cardinality constraint - literal_vector lits; - for (wliteral wl : m_wlits) { - lits.push_back(wl.second); - } - constraint* c = add_at_least(sat::null_literal, lits, k, true); - - ++m_stats.m_num_lemmas; - - if (c) { - lits.reset(); - for (wliteral wl : m_wlits) { - if (value(wl.second) == l_false) lits.push_back(wl.second); - } - unsigned glue = s().num_diff_levels(lits.size(), lits.data()); - c->set_glue(glue); - } - return c; - } - - - void solver::justification2pb(sat::justification const& js, literal lit, unsigned offset, ineq& ineq) { - switch (js.get_kind()) { - case sat::justification::NONE: - SASSERT(lit != sat::null_literal); - ineq.reset(offset); - ineq.push(lit, offset); - break; - case sat::justification::BINARY: - SASSERT(lit != sat::null_literal); - ineq.reset(offset); - ineq.push(lit, offset); - ineq.push(js.get_literal(), offset); - break; - case sat::justification::TERNARY: - SASSERT(lit != sat::null_literal); - ineq.reset(offset); - ineq.push(lit, offset); - ineq.push(js.get_literal1(), offset); - ineq.push(js.get_literal2(), offset); - break; - case sat::justification::CLAUSE: { - ineq.reset(offset); - sat::clause & c = s().get_clause(js); - for (literal l : c) ineq.push(l, offset); - break; - } - case sat::justification::EXT_JUSTIFICATION: { - sat::ext_justification_idx index = js.get_ext_justification_idx(); - VERIFY(this == sat::constraint_base::to_extension(index)); - constraint& cnstr = index2constraint(index); - constraint2pb(cnstr, lit, offset, ineq); - break; - } - default: - UNREACHABLE(); - break; - } - } - - void solver::constraint2pb(constraint& cnstr, literal lit, unsigned offset, ineq& ineq) { - switch (cnstr.tag()) { - case pb::tag_t::card_t: { - card& c = cnstr.to_card(); - ineq.reset(static_cast(offset)*c.k()); - for (literal l : c) ineq.push(l, offset); - if (c.lit() != sat::null_literal) ineq.push(~c.lit(), offset*c.k()); - break; - } - case pb::tag_t::pb_t: { - pbc& p = cnstr.to_pb(); - ineq.reset(static_cast(offset) * p.k()); - for (wliteral wl : p) ineq.push(wl.second, offset * wl.first); - if (p.lit() != sat::null_literal) ineq.push(~p.lit(), offset * p.k()); - break; - } - default: - UNREACHABLE(); - break; - } - } - - // validate that m_A & m_B implies m_C - - bool solver::validate_resolvent() { - return true; - u_map coeffs; - uint64_t k = m_A.m_k + m_B.m_k; - for (unsigned i = 0; i < m_A.size(); ++i) { - uint64_t coeff = m_A.coeff(i); - SASSERT(!coeffs.contains(m_A.lit(i).index())); - coeffs.insert(m_A.lit(i).index(), coeff); - } - for (unsigned i = 0; i < m_B.size(); ++i) { - uint64_t coeff1 = m_B.coeff(i), coeff2; - literal lit = m_B.lit(i); - if (coeffs.find((~lit).index(), coeff2)) { - if (coeff1 == coeff2) { - coeffs.remove((~lit).index()); - k += coeff1; - } - else if (coeff1 < coeff2) { - coeffs.insert((~lit).index(), coeff2 - coeff1); - k += coeff1; - } - else { - SASSERT(coeff2 < coeff1); - coeffs.remove((~lit).index()); - coeffs.insert(lit.index(), coeff1 - coeff2); - k += coeff2; - } - } - else if (coeffs.find(lit.index(), coeff2)) { - coeffs.insert(lit.index(), coeff1 + coeff2); - } - else { - coeffs.insert(lit.index(), coeff1); - } - } - // C is above the sum of A and B - for (unsigned i = 0; i < m_C.size(); ++i) { - literal lit = m_C.lit(i); - uint64_t coeff; - if (coeffs.find(lit.index(), coeff)) { - if (coeff > m_C.coeff(i) && m_C.coeff(i) < m_C.m_k) { - goto violated; - } - coeffs.remove(lit.index()); - } - } - if (!coeffs.empty()) goto violated; - if (m_C.m_k > k) goto violated; - SASSERT(coeffs.empty()); - SASSERT(m_C.m_k <= k); - return true; - - violated: - // last ditch effort by translating to SAT. - sat::solver s0(s().m_params, s().rlimit()); - u_map translation; - literal l1 = translate_to_sat(s0, translation, m_A); - if (l1 == sat::null_literal) return true; - literal l2 = translate_to_sat(s0, translation, m_B); - if (l2 == sat::null_literal) return true; - ineq notC = negate(m_B); - literal l3 = translate_to_sat(s0, translation, notC); - if (l3 == sat::null_literal) return true; - s0.assign_scoped(l1); - s0.assign_scoped(l2); - s0.assign_scoped(l3); - lbool is_sat = s0.check(); - TRACE("ba", s0.display(tout << "trying sat encoding");); - if (is_sat == l_false) return true; - - IF_VERBOSE(0, - display(verbose_stream(), m_A); - display(verbose_stream(), m_B); - display(verbose_stream(), m_C); - for (auto& e : coeffs) { - verbose_stream() << sat::to_literal(e.m_key) << ": " << e.m_value << "\n"; - }); - - UNREACHABLE(); - return false; - } - - /** - \brief translate PB inequality to SAT formula. - */ - literal solver::translate_to_sat(sat::solver& s, u_map& translation, ineq const& pb) { - SASSERT(pb.m_k > 0); - if (pb.size() > 1) { - ineq a, b; - a.reset(pb.m_k); - b.reset(pb.m_k); - for (unsigned i = 0; i < pb.size()/2; ++i) { - a.push(pb.lit(i), pb.coeff(i)); - } - for (unsigned i = pb.size()/2; i < pb.size(); ++i) { - b.push(pb.lit(i), pb.coeff(i)); - } - bool_var v = s.mk_var(); - literal lit(v, false); - literal_vector lits; - lits.push_back(~lit); - push_lit(lits, translate_to_sat(s, translation, a)); - push_lit(lits, translate_to_sat(s, translation, b)); - push_lit(lits, translate_to_sat(s, translation, a, b)); - s.mk_clause(lits); - return lit; - } - if (pb.coeff(0) >= pb.m_k) { - return translate_to_sat(s, translation, pb.lit(0)); - } - else { - return sat::null_literal; - } - } - - /* - \brief encode the case where Sum(a) >= k-1 & Sum(b) >= 1 \/ ... \/ Sum(a) >= 1 & Sum(b) >= k-1 - */ - literal solver::translate_to_sat(sat::solver& s, u_map& translation, ineq& a, ineq& b) { - uint64_t k0 = a.m_k; - literal_vector lits; - for (unsigned k = 1; k < a.m_k - 1; ++k) { - a.m_k = k; b.m_k = k0 - k; - literal lit1 = translate_to_sat(s, translation, a); - literal lit2 = translate_to_sat(s, translation, b); - if (lit1 != sat::null_literal && lit2 != sat::null_literal) { - bool_var v = s.mk_var(); - literal lit(v, false); - s.mk_clause(~lit, lit1); - s.mk_clause(~lit, lit2); - lits.push_back(lit); - } - } - a.m_k = k0; - b.m_k = k0; - switch (lits.size()) { - case 0: return sat::null_literal; - case 1: return lits[0]; - default: { - bool_var v = s.mk_var(); - literal lit(v, false); - lits.push_back(~lit); - s.mk_clause(lits); - return lit; - } - } - } - - literal solver::translate_to_sat(sat::solver& s, u_map& translation, literal lit) { - bool_var v; - if (!translation.find(lit.var(), v)) { - v = s.mk_var(); - translation.insert(lit.var(), v); - } - return literal(v, lit.sign()); - } - - solver::ineq solver::negate(ineq const& a) const { - ineq result; - uint64_t sum = 0; - for (unsigned i = 0; i < a.size(); ++i) { - result.push(~a.lit(i), a.coeff(i)); - sum += a.coeff(i); - } - SASSERT(sum >= a.m_k + 1); - result.m_k = sum + 1 - a.m_k; - return result; - } - - void solver::push_lit(literal_vector& lits, literal lit) { - if (lit != sat::null_literal) { - lits.push_back(lit); - } - } - - bool solver::validate_conflict(literal_vector const& lits, ineq& p) { - for (literal l : lits) { - if (value(l) != l_false) { - TRACE("ba", tout << "literal " << l << " is not false\n";); - return false; - } - if (!p.contains(l)) { - TRACE("ba", tout << "lemma contains literal " << l << " not in inequality\n";); - return false; - } - } - uint64_t value = 0; - for (unsigned i = 0; i < p.size(); ++i) { - uint64_t coeff = p.coeff(i); - if (!lits.contains(p.lit(i))) { - value += coeff; - } - } - CTRACE("ba", value >= p.m_k, tout << "slack: " << value << " bound " << p.m_k << "\n"; - display(tout, p); - tout << lits << "\n";); - return value < p.m_k; - } - - bool solver::check_model(sat::model const& m) const { - bool ok = true; - for (constraint const* c : m_constraints) { - if (c->was_removed()) { - continue; - } - if (c->is_pure() && c->lit() != sat::null_literal && m[c->lit().var()] == (c->lit().sign() ? l_true : l_false)) { - continue; - } - switch (eval(m, *c)) { - case l_false: - IF_VERBOSE(0, verbose_stream() << "failed checking " << c->id() << ": " << *c << "\n";); - ok = false; - break; - case l_true: - break; - case l_undef: - IF_VERBOSE(0, verbose_stream() << "undef " << c->id() << ": " << *c << "\n";); - break; - } - } - return ok; - } - - bool solver::extract_pb(std::function& add_cardinality, - std::function& add_pb) { - - unsigned_vector coeffs; - literal_vector lits; - for (constraint* cp : m_constraints) { - switch (cp->tag()) { - case pb::tag_t::card_t: { - card const& c = cp->to_card(); - unsigned n = c.size(); - unsigned k = c.k(); - - if (c.lit() == sat::null_literal) { - // c.lits() >= k - // <=> - // ~c.lits() <= n - k - lits.reset(); - for (unsigned j = 0; j < n; ++j) lits.push_back(c[j]); - add_cardinality(lits.size(), lits.data(), n - k); - } - else { - // - // c.lit() <=> c.lits() >= k - // - // (c.lits() < k) or c.lit() - // = (c.lits() + (n - k + 1)*~c.lit()) <= n - // - // ~c.lit() or (c.lits() >= k) - // = ~c.lit() or (~c.lits() <= n - k) - // = k*c.lit() + ~c.lits() <= n - // - lits.reset(); - coeffs.reset(); - for (literal l : c) lits.push_back(l), coeffs.push_back(1); - lits.push_back(~c.lit()); coeffs.push_back(n - k + 1); - add_pb(lits.size(), lits.data(), coeffs.data(), n); - - lits.reset(); - coeffs.reset(); - for (literal l : c) lits.push_back(~l), coeffs.push_back(1); - lits.push_back(c.lit()); coeffs.push_back(k); - add_pb(lits.size(), lits.data(), coeffs.data(), n); - } - break; - } - case pb::tag_t::pb_t: { - pbc const& p = cp->to_pb(); - lits.reset(); - coeffs.reset(); - unsigned sum = 0; - for (wliteral wl : p) sum += wl.first; - - if (p.lit() == sat::null_literal) { - // w1 + .. + w_n >= k - // <=> - // ~wl + ... + ~w_n <= sum_of_weights - k - for (wliteral wl : p) lits.push_back(~(wl.second)), coeffs.push_back(wl.first); - add_pb(lits.size(), lits.data(), coeffs.data(), sum - p.k()); - } - else { - // lit <=> w1 + .. + w_n >= k - // <=> - // lit or w1 + .. + w_n <= k - 1 - // ~lit or w1 + .. + w_n >= k - // <=> - // (sum - k + 1)*~lit + w1 + .. + w_n <= sum - // k*lit + ~wl + ... + ~w_n <= sum - lits.push_back(p.lit()), coeffs.push_back(p.k()); - for (wliteral wl : p) lits.push_back(~(wl.second)), coeffs.push_back(wl.first); - add_pb(lits.size(), lits.data(), coeffs.data(), sum); - - lits.reset(); - coeffs.reset(); - lits.push_back(~p.lit()), coeffs.push_back(sum + 1 - p.k()); - for (wliteral wl : p) lits.push_back(wl.second), coeffs.push_back(wl.first); - add_pb(lits.size(), lits.data(), coeffs.data(), sum); - } - break; - } - } - } - return true; - } - -}; - - diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index bb2d61b0a..c057541b8 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -243,11 +243,11 @@ namespace euf { m_egraph.explain_eq(m_explain, a, b); } - void solver::add_diseq_antecedent(enode* a, enode* b) { - sat::bool_var v = get_egraph().explain_diseq(m_explain, a, b); + void solver::add_diseq_antecedent(ptr_vector& ex, enode* a, enode* b) { + sat::bool_var v = get_egraph().explain_diseq(ex, a, b); SASSERT(v == sat::null_bool_var || s().value(v) == l_false); if (v != sat::null_bool_var) - m_explain.push_back(to_ptr(sat::literal(v, true))); + ex.push_back(to_ptr(sat::literal(v, true))); } bool solver::propagate(enode* a, enode* b, ext_justification_idx idx) { diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 859c0640c..b42d1fde8 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -305,7 +305,9 @@ namespace euf { void get_antecedents(literal l, ext_justification_idx idx, literal_vector& r, bool probing) override; void get_antecedents(literal l, th_explain& jst, literal_vector& r, bool probing); void add_antecedent(enode* a, enode* b); - void add_diseq_antecedent(enode* a, enode* b); + void add_diseq_antecedent(ptr_vector& ex, enode* a, enode* b); + void add_explain(size_t* p) { m_explain.push_back(p); } + void reset_explain() { m_explain.reset(); } void set_eliminated(bool_var v) override; void asserted(literal l) override; sat::check_result check() override; diff --git a/src/sat/smt/q_clause.h b/src/sat/smt/q_clause.h index 0c89b2ade..e1e31b199 100644 --- a/src/sat/smt/q_clause.h +++ b/src/sat/smt/q_clause.h @@ -122,18 +122,17 @@ namespace q { return out << "]"; } - struct justification { - expr* m_lhs, *m_rhs; + expr* m_lhs, * m_rhs; bool m_sign; - unsigned m_num_ev; - euf::enode_pair* m_evidence; - clause& m_clause; + unsigned m_num_ex; + size_t** m_explain; + clause& m_clause; euf::enode* const* m_binding; - justification(lit const& l, clause& c, euf::enode* const* b, unsigned n, euf::enode_pair* ev): - m_lhs(l.lhs), m_rhs(l.rhs), m_sign(l.sign), m_num_ev(n), m_evidence(ev), m_clause(c), m_binding(b) {} - sat::ext_constraint_idx to_index() const { - return sat::constraint_base::mem2base(this); + justification(lit const& l, clause& c, euf::enode* const* b, unsigned n, size_t** ev) : + m_lhs(l.lhs), m_rhs(l.rhs), m_sign(l.sign), m_num_ex(n), m_explain(ev), m_clause(c), m_binding(b) {} + sat::ext_constraint_idx to_index() const { + return sat::constraint_base::mem2base(this); } static justification& from_index(size_t idx) { return *reinterpret_cast(sat::constraint_base::from_index(idx)->mem()); diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index af8fc3652..495912f11 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -97,23 +97,46 @@ namespace q { } } + /** + * Create a justification for binding b. + * The justification involves equalities in the E-graph that have + * explanations. Retrieve the explanations while the justification + * is created to ensure the justification trail is well-founded + * during conflict resolution. + */ sat::ext_justification_idx ematch::mk_justification(unsigned idx, clause& c, euf::enode* const* b) { void* mem = ctx.get_region().allocate(justification::get_obj_size()); sat::constraint_base::initialize(mem, &m_qs); bool sign = false; - expr* l = nullptr, *r = nullptr; - lit lit(expr_ref(l, m), expr_ref(r, m), sign); + expr* l = nullptr, * r = nullptr; + lit lit(expr_ref(l, m), expr_ref(r, m), sign); if (idx != UINT_MAX) lit = c[idx]; - auto* ev = static_cast(ctx.get_region().allocate(sizeof(euf::enode_pair) * m_evidence.size())); - for (unsigned i = m_evidence.size(); i-- > 0; ) - ev[i] = m_evidence[i]; - auto* constraint = new (sat::constraint_base::ptr2mem(mem)) justification(lit, c, b, m_evidence.size(), ev); + m_explain.reset(); + ctx.get_egraph().begin_explain(); + ctx.reset_explain(); + for (auto const& [a, b] : m_evidence) { + SASSERT(a->get_root() == b->get_root() || ctx.get_egraph().are_diseq(a, b)); + if (a->get_root() == b->get_root()) + ctx.get_egraph().explain_eq(m_explain, a, b); + else + ctx.add_diseq_antecedent(m_explain, a, b); + } + ctx.get_egraph().end_explain(); + std::cout << "exp size " << m_explain.size() << "\n"; + + size_t** ev = static_cast(ctx.get_region().allocate(sizeof(size_t*) * m_explain.size())); + for (unsigned i = m_explain.size(); i-- > 0; ) + ev[i] = m_explain[i]; + auto* constraint = new (sat::constraint_base::ptr2mem(mem)) justification(lit, c, b, m_explain.size(), ev); return constraint->to_index(); } void ematch::get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) { - m_eval.explain(l, justification::from_index(idx), r, probing); + justification& j = justification::from_index(idx); + for (unsigned i = 0; i < j.m_num_ex; ++i) + ctx.add_explain(j.m_explain[i]); + r.push_back(j.m_clause.m_literal); } quantifier_ref ematch::nnf_skolem(quantifier* q) { diff --git a/src/sat/smt/q_ematch.h b/src/sat/smt/q_ematch.h index 184272c8f..98ee26fc4 100644 --- a/src/sat/smt/q_ematch.h +++ b/src/sat/smt/q_ematch.h @@ -94,7 +94,8 @@ namespace q { euf::enode* const* copy_nodes(clause& c, euf::enode* const* _binding); binding* tmp_binding(clause& c, app* pat, euf::enode* const* _binding); binding* alloc_binding(clause& c, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_top, unsigned max_top); - + + ptr_vector m_explain; sat::ext_justification_idx mk_justification(unsigned idx, clause& c, euf::enode* const* b); void ensure_ground_enodes(expr* e); diff --git a/src/sat/smt/q_eval.cpp b/src/sat/smt/q_eval.cpp index a01bb9d9d..1cfbe7779 100644 --- a/src/sat/smt/q_eval.cpp +++ b/src/sat/smt/q_eval.cpp @@ -246,20 +246,5 @@ namespace q { } return m_eval[e->get_id()]; } - - void eval::explain(sat::literal l, justification& j, sat::literal_vector& r, bool probing) { - clause& c = j.m_clause; - for (unsigned i = 0; i < j.m_num_ev; ++i) { - auto [a, b] = j.m_evidence[i]; - SASSERT(a->get_root() == b->get_root() || ctx.get_egraph().are_diseq(a, b)); - if (a->get_root() == b->get_root()) - ctx.add_antecedent(a, b); - else - ctx.add_diseq_antecedent(a, b); - } - r.push_back(c.m_literal); - (void)probing; // ignored - } - } diff --git a/src/sat/smt/q_eval.h b/src/sat/smt/q_eval.h index ef016407a..6d2f09501 100644 --- a/src/sat/smt/q_eval.h +++ b/src/sat/smt/q_eval.h @@ -43,7 +43,6 @@ namespace q { public: eval(euf::solver& ctx); - void explain(sat::literal l, justification& j, sat::literal_vector& r, bool probing); lbool operator()(euf::enode* const* binding, clause& c, euf::enode_pair_vector& evidence); lbool operator()(euf::enode* const* binding, clause& c, unsigned& idx, euf::enode_pair_vector& evidence); diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp index a4d719cfd..edf00615b 100644 --- a/src/sat/smt/q_mam.cpp +++ b/src/sat/smt/q_mam.cpp @@ -553,8 +553,8 @@ namespace q { void unmark(unsigned head) { for (unsigned i = m_candidates.size(); i-- > head; ) { enode* app = m_candidates[i]; - if (app->is_marked1()) - app->unmark1(); + if (app->is_marked2()) + app->unmark2(); } } @@ -946,9 +946,9 @@ namespace q { void linearise_core() { m_aux.reset(); app * first_app = nullptr; - unsigned first_app_reg; - unsigned first_app_sz; - unsigned first_app_num_unbound_vars; + unsigned first_app_reg = 0; + unsigned first_app_sz = 0; + unsigned first_app_num_unbound_vars = 0; // generate first the non-BIND operations for (unsigned reg : m_todo) { expr * p = m_registers[reg]; @@ -2022,9 +2022,9 @@ namespace q { code_tree::scoped_unmark _unmark(t); while ((app = t->next_candidate()) && !ctx.resource_limits_exceeded()) { TRACE("trigger_bug", tout << "candidate\n" << ctx.bpp(app) << "\n";); - if (!app->is_marked1() && app->is_cgr()) { + if (!app->is_marked2() && app->is_cgr()) { execute_core(t, app); - app->mark1(); + app->mark2(); } } }