From 89f03190435995f6e6feb1b4e70eb26789d99e44 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Sep 2014 11:19:05 -0700 Subject: [PATCH] tune assertions of bounds Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith.h | 12 ++ src/smt/theory_arith_core.h | 252 ++++++++++++++++++++++-------------- 2 files changed, 169 insertions(+), 95 deletions(-) diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 7179ba8bf..638d3c6b0 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -573,6 +573,18 @@ namespace smt { void mk_clause(literal l1, literal l2, unsigned num_params, parameter * params); void mk_clause(literal l1, literal l2, literal l3, unsigned num_params, parameter * params); void mk_bound_axioms(atom * a); + void mk_bound_axiom(atom* a1, atom* a2); + ptr_vector m_new_atoms; + void flush_bound_axioms(); + typename atoms::iterator next_sup(atom* a1, atom_kind kind, + typename atoms::iterator it, + typename atoms::iterator end); + typename atoms::iterator next_inf(atom* a1, atom_kind kind, + typename atoms::iterator it, + typename atoms::iterator end); + struct compare_atoms { + bool operator()(atom* a1, atom* a2) const { return a1->get_k() < a2->get_k(); } + }; virtual bool default_internalizer() const { return false; } virtual bool internalize_atom(app * n, bool gate_ctx); virtual bool internalize_term(app * term); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 017833210..e037ea9e3 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -810,143 +810,204 @@ namespace smt { template void theory_arith::mk_bound_axioms(atom * a1) { + if (!get_context().is_searching()) { + // + // NB. We make an assumption that user push calls propagation + // before internal scopes are pushed. This flushes all newly + // asserted atoms into the right context. + // + m_new_atoms.push_back(a1); + return; + } theory_var v = a1->get_var(); - literal l1(a1->get_bool_var()); inf_numeral const & k1(a1->get_k()); atom_kind kind1 = a1->get_atom_kind(); - bool v_is_int = is_int(v); TRACE("mk_bound_axioms", tout << "making bound axioms for v" << v << " " << kind1 << " " << k1 << "\n";); atoms & occs = m_var_occs[v]; typename atoms::iterator it = occs.begin(); typename atoms::iterator end = occs.end(); - parameter coeffs[3] = { parameter(symbol("farkas")), parameter(rational(1)), parameter(rational(1)) }; typename atoms::iterator lo_inf = end, lo_sup = end; typename atoms::iterator hi_inf = end, hi_sup = end; - literal lit1, lit2, lit3, lit4; for (; it != end; ++it) { atom * a2 = *it; - inf_numeral const & k2 = a2->get_k(); - atom_kind kind2 = a2->get_atom_kind(); + inf_numeral const & k2(a2->get_k()); + atom_kind kind2 = a2->get_atom_kind(); SASSERT(k1 != k2 || kind1 != kind2); if (kind2 == A_LOWER) { if (k2 < k1) { if (lo_inf == end || k2 > (*lo_inf)->get_k()) { lo_inf = it; - lit1 = literal(a2->get_bool_var()); } } else if (lo_sup == end || k2 < (*lo_sup)->get_k()) { lo_sup = it; - lit2 = literal(a2->get_bool_var()); } } - else { - if (k2 < k1) { - if (hi_inf == end || k2 > (*hi_inf)->get_k()) { - hi_inf = it; - lit3 = literal(a2->get_bool_var()); - } - } - else if (hi_sup == end || k2 < (*hi_sup)->get_k()) { - hi_sup = it; - lit4 = literal(a2->get_bool_var()); + else if (k2 < k1) { + if (hi_inf == end || k2 > (*hi_inf)->get_k()) { + hi_inf = it; } } + else if (hi_sup == end || k2 < (*hi_sup)->get_k()) { + hi_sup = it; + } } + if (lo_inf != end) mk_bound_axiom(a1, *lo_inf); + if (lo_sup != end) mk_bound_axiom(a1, *lo_sup); + if (hi_inf != end) mk_bound_axiom(a1, *hi_inf); + if (hi_sup != end) mk_bound_axiom(a1, *hi_sup); + } + + template + void theory_arith::mk_bound_axiom(atom* a1, atom* a2) { + theory_var v = a1->get_var(); + literal l1(a1->get_bool_var()); + literal l2(a2->get_bool_var()); + inf_numeral const & k1(a1->get_k()); + inf_numeral const & k2(a2->get_k()); + atom_kind kind1 = a1->get_atom_kind(); + atom_kind kind2 = a2->get_atom_kind(); + bool v_is_int = is_int(v); + SASSERT(v === a2->get_var()); + SASSERT(k1 != k2 || kind1 != kind2); + parameter coeffs[3] = { parameter(symbol("farkas")), + parameter(rational(1)), parameter(rational(1)) }; if (kind1 == A_LOWER) { - if (lo_inf != end) { - // k1 >= lo_inf, k1 <= x => lo_inf <= x - mk_clause(~l1, lit1, 3, coeffs); - } - if (lo_sup != end) { - // k1 <= lo_sup, lo_sup <= x => k1 <= x - mk_clause(l1, ~lit2, 3, coeffs); - } - if (hi_inf != end) { - // k1 == hi_inf, k1 <= x or x <= hi_inf - if (k1 == (*hi_inf)->get_k()) { - mk_clause(l1, lit3, 3, coeffs); + if (kind2 == A_LOWER) { + if (k2 <= k1) { + mk_clause(~l1, l2, 3, coeffs); } else { - // k1 > hi_inf, k1 <= x => ~(x <= hi_inf) - mk_clause(~l1, ~lit3, 3, coeffs); - if (v_is_int && k1 == (*hi_inf)->get_k() + inf_numeral(1)) { - // k1 <= x or x <= k1-1 - mk_clause(l1, lit3, 3, coeffs); - } + mk_clause(l1, ~l2, 3, coeffs); } } - if (hi_sup != end) { - // k1 <= hi_sup, k1 <= x or x <= hi_sup - mk_clause(l1, lit4, 3, coeffs); + else if (k1 <= k2) { + // k1 <= k2, k1 <= x or x <= k2 + mk_clause(l1, l2, 3, coeffs); + } + else { + // k1 > hi_inf, k1 <= x => ~(x <= hi_inf) + mk_clause(~l1, ~l2, 3, coeffs); + if (v_is_int && k1 == k2 + inf_numeral(1)) { + // k1 <= x or x <= k1-1 + mk_clause(l1, l2, 3, coeffs); + } + } + } + else if (kind2 == A_LOWER) { + if (k1 >= k2) { + // k1 >= lo_inf, k1 >= x or lo_inf <= x + mk_clause(l1, l2, 3, coeffs); + } + else { + // k1 < k2, k2 <= x => ~(x <= k1) + mk_clause(~l1, ~l2, 3, coeffs); + if (v_is_int && k1 == k2 - inf_numeral(1)) { + // x <= k1 or k1+l <= x + mk_clause(l1, l2, 3, coeffs); + } + } } else { - if (lo_inf != end) { - // k1 >= lo_inf, k1 >= x or lo_inf <= x - mk_clause(l1, lit1, 3, coeffs); - } - if (lo_sup != end) { - if (k1 == (*lo_sup)->get_k()) { - mk_clause(l1, lit2, 3, coeffs); - } - else { - // k1 < lo_sup, lo_sup <= x => ~(x <= k1) - mk_clause(~l1, ~lit2, 3, coeffs); - if (v_is_int && k1 == (*lo_sup)->get_k() - inf_numeral(1)) { - // x <= k1 or k1+l <= x - mk_clause(l1, lit2, 3, coeffs); - } - - } - } - if (hi_inf != end) { - // k1 >= hi_inf, x <= hi_inf => x <= k1 - mk_clause(l1, ~lit3, 3, coeffs); - } - if (hi_sup != end) { - // k1 <= hi_sup , x <= k1 => x <= hi_sup - mk_clause(~l1, lit4, 3, coeffs); - } - } - return; - - for (; it != end; ++it) { - atom * a2 = *it; - literal l2(a2->get_bool_var()); - inf_numeral const & k2 = a2->get_k(); - atom_kind kind2 = a2->get_atom_kind(); - SASSERT(k1 != k2 || kind1 != kind2); - SASSERT(a2->get_var() == v); - if (kind1 == A_LOWER) { - if (kind2 == A_LOWER) { - // x >= k1, x >= k2 - if (k1 >= k2) mk_clause(~l1, l2, 3, coeffs); - else mk_clause(~l2, l1, 3, coeffs); - } - else { - // x >= k1, x <= k2 - if (k1 > k2) mk_clause(~l1, ~l2, 3, coeffs); - else mk_clause(l1, l2, 3, coeffs); - } + // kind1 == A_UPPER, kind2 == A_UPPER + if (k1 >= k2) { + // k1 >= k2, x <= k2 => x <= k1 + mk_clause(l1, ~l2, 3, coeffs); } else { - if (kind2 == A_LOWER) { - // x <= k1, x >= k2 - if (k1 < k2) mk_clause(~l1, ~l2, 3, coeffs); - else mk_clause(l1, l2, 3, coeffs); - } - else { - // x <= k1, x <= k2 - if (k1 < k2) mk_clause(~l1, l2, 3, coeffs); - else mk_clause(~l2, l1, 3, coeffs); + // k1 <= hi_sup , x <= k1 => x <= hi_sup + mk_clause(~l1, l2, 3, coeffs); + } + } + } + + template + void theory_arith::flush_bound_axioms() { + while (!m_new_atoms.empty()) { + ptr_vector atoms; + atoms.push_back(m_new_atoms.back()); + m_new_atoms.pop_back(); + theory_var v = atoms.back()->get_var(); + for (unsigned i = 0; i < m_new_atoms.size(); ++i) { + if (m_new_atoms[i]->get_var() == v) { + atoms.push_back(m_new_atoms[i]); + m_new_atoms[i] = m_new_atoms.back(); + m_new_atoms.pop_back(); + --i; } } + ptr_vector occs(m_var_occs[v]); + + std::sort(atoms.begin(), atoms.end(), compare_atoms()); + std::sort(occs.begin(), occs.end(), compare_atoms()); + + typename atoms::iterator begin = occs.begin(); + typename atoms::iterator end = occs.end(); + typename atoms::iterator lo_inf = begin, lo_sup = begin; + typename atoms::iterator hi_inf = begin, hi_sup = begin; + + for (unsigned i = 0; i < atoms.size(); ++i) { + atom* a1 = atoms[i]; + lo_inf = next_inf(a1, A_LOWER, lo_inf, end); + hi_inf = next_inf(a1, A_UPPER, hi_inf, end); + lo_sup = next_sup(a1, A_LOWER, lo_sup, end); + hi_sup = next_sup(a1, A_UPPER, hi_sup, end); + if (lo_inf != end) mk_bound_axiom(a1, *lo_inf); + if (lo_sup != end) mk_bound_axiom(a1, *lo_sup); + if (hi_inf != end) mk_bound_axiom(a1, *hi_inf); + if (hi_sup != end) mk_bound_axiom(a1, *hi_sup); + } } } + template + typename theory_arith::atoms::iterator + theory_arith::next_inf( + atom* a1, + atom_kind kind, + typename atoms::iterator it, + typename atoms::iterator end) { + inf_numeral const & k1(a1->get_k()); + typename atoms::iterator result = end; + for (; it != end; ++it) { + atom * a2 = *it; + if (a1 == a2) continue; + if (a2->get_atom_kind() != kind) continue; + inf_numeral const & k2(a2->get_k()); + if (k2 <= k1) { + result = it; + } + else { + break; + } + } + return result; + } + + template + typename theory_arith::atoms::iterator + theory_arith::next_sup( + atom* a1, + atom_kind kind, + typename atoms::iterator it, + typename atoms::iterator end) { + inf_numeral const & k1(a1->get_k()); + for (; it != end; ++it) { + atom * a2 = *it; + if (a1 == a2) continue; + if (a2->get_atom_kind() != kind) continue; + inf_numeral const & k2(a2->get_k()); + if (k2 > k1) { + return it; + } + } + return end; + } + + template bool theory_arith::internalize_atom(app * n, bool gate_ctx) { TRACE("arith_internalize", tout << "internalising atom:\n" << mk_pp(n, this->get_manager()) << "\n";); @@ -1248,6 +1309,7 @@ namespace smt { CASSERT("arith", wf_columns()); CASSERT("arith", valid_row_assignment()); + flush_bound_axioms(); propagate_linear_monomials(); while (m_asserted_qhead < m_asserted_bounds.size()) { bound * b = m_asserted_bounds[m_asserted_qhead];