From e40b8a2d13751fadd20de16e20803a1995ab6d82 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 18 Nov 2023 09:56:06 -0800 Subject: [PATCH] household chores in legacy arithmetic solver --- src/smt/theory_arith.h | 10 ++++----- src/smt/theory_arith_aux.h | 41 ++++++++++++++------------------- src/smt/theory_arith_core.h | 45 +++++++++++++++---------------------- src/smt/theory_arith_eq.h | 21 +++++++---------- 4 files changed, 48 insertions(+), 69 deletions(-) diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 8cbf844b9e0..86c05aec64e 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -301,7 +301,7 @@ namespace smt { inf_numeral const & get_value() const { return m_value; } virtual bool has_justification() const { return false; } virtual void push_justification(antecedents& antecedents, numeral const& coeff, bool proofs_enabled) {} - virtual void display(theory_arith const& th, std::ostream& out) const; + virtual std::ostream& display(theory_arith const& th, std::ostream& out) const; }; @@ -327,7 +327,7 @@ namespace smt { void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) override { a.push_lit(literal(get_bool_var(), !m_is_true), coeff, proofs_enabled); } - void display(theory_arith const& th, std::ostream& out) const override; + std::ostream& display(theory_arith const& th, std::ostream& out) const override; }; class eq_bound : public bound { @@ -345,7 +345,7 @@ namespace smt { SASSERT(m_lhs->get_root() == m_rhs->get_root()); a.push_eq(enode_pair(m_lhs, m_rhs), coeff, proofs_enabled); } - void display(theory_arith const& th, std::ostream& out) const override; + std::ostream& display(theory_arith const& th, std::ostream& out) const override; }; class derived_bound : public bound { @@ -361,7 +361,7 @@ namespace smt { void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) override; virtual void push_lit(literal l, numeral const&) { m_lits.push_back(l); } virtual void push_eq(enode_pair const& p, numeral const&) { m_eqs.push_back(p); } - void display(theory_arith const& th, std::ostream& out) const override; + std::ostream& display(theory_arith const& th, std::ostream& out) const override; }; @@ -824,7 +824,7 @@ namespace smt { unsigned m_assume_eq_head = 0; bool random_update(theory_var v); void mutate_assignment(); - bool assume_eqs_core(); + bool assume_eqs(); bool delayed_assume_eqs(); // ----------------------------------- diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 470ea5f7b4a..8141377c455 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -370,8 +370,8 @@ namespace smt { template - void theory_arith::bound::display(theory_arith const& th, std::ostream& out) const { - out << "v" << get_var() << " " << get_bound_kind() << " " << get_value(); + std::ostream& theory_arith::bound::display(theory_arith const& th, std::ostream& out) const { + return out << "v" << get_var() << " " << get_bound_kind() << " " << get_value(); } @@ -414,11 +414,10 @@ namespace smt { } template - void theory_arith::atom::display(theory_arith const& th, std::ostream& out) const { + std::ostream& theory_arith::atom::display(theory_arith const& th, std::ostream& out) const { literal l(get_bool_var(), !m_is_true); - // out << "v" << bound::get_var() << " " << bound::get_bound_kind() << " " << get_k() << " "; - // out << l << ":"; th.ctx.display_detailed_literal(out, l); + return out; } // ----------------------------------- @@ -428,10 +427,10 @@ namespace smt { // ----------------------------------- template - void theory_arith::eq_bound::display(theory_arith const& th, std::ostream& out) const { + std::ostream& theory_arith::eq_bound::display(theory_arith const& th, std::ostream& out) const { ast_manager& m = th.get_manager(); - out << "#" << m_lhs->get_owner_id() << " " << mk_pp(m_lhs->get_expr(), m) << " = " - << "#" << m_rhs->get_owner_id() << " " << mk_pp(m_rhs->get_expr(), m); + return out << "#" << m_lhs->get_owner_id() << " " << mk_pp(m_lhs->get_expr(), m) << " = " + << "#" << m_rhs->get_owner_id() << " " << mk_pp(m_rhs->get_expr(), m); } // ----------------------------------- @@ -752,7 +751,7 @@ namespace smt { } template - void theory_arith::derived_bound::display(theory_arith const& th, std::ostream& out) const { + std::ostream& theory_arith::derived_bound::display(theory_arith const& th, std::ostream& out) const { ast_manager& m = th.get_manager(); out << "v" << bound::get_var() << " " << bound::get_bound_kind() << " " << bound::get_value() << "\n"; out << "expr: " << mk_pp(th.var2expr(bound::get_var()), m) << "\n"; @@ -765,8 +764,9 @@ namespace smt { << "#" << b->get_owner_id() << " " << mk_pp(b->get_expr(), m) << "\n"; } for (literal l : m_lits) { - out << l << ":"; th.ctx.display_detailed_literal(out, l) << "\n"; + out << l << ":"; th.ctx.display_detailed_literal(out, l) << "\n"; } + return out; } @@ -2195,33 +2195,27 @@ namespace smt { } template - bool theory_arith::assume_eqs_core() { + bool theory_arith::assume_eqs() { // See comment in m_liberal_final_check declaration if (m_liberal_final_check) mutate_assignment(); TRACE("assume_eq_int", display(tout);); unsigned old_sz = m_assume_eq_candidates.size(); - TRACE("func_interp_bug", display(tout);); m_var_value_table.reset(); bool result = false; int num = get_num_vars(); for (theory_var v = 0; v < num; v++) { enode * n = get_enode(v); - TRACE("func_interp_bug", tout << mk_pp(n->get_expr(), get_manager()) << " -> " << m_value[v] << " root #" << n->get_root()->get_owner_id() << " " << is_relevant_and_shared(n) << "\n";); - if (!is_relevant_and_shared(n)) { + if (!is_relevant_and_shared(n)) continue; - } theory_var other = null_theory_var; other = m_var_value_table.insert_if_not_there(v); - if (other == v) { + if (other == v) continue; - } enode * n2 = get_enode(other); - if (n->get_root() == n2->get_root()) { + if (n->get_root() == n2->get_root()) continue; - } - TRACE("func_interp_bug", tout << "adding to assume_eq queue #" << n->get_owner_id() << " #" << n2->get_owner_id() << "\n";); m_assume_eq_candidates.push_back({ other , v }); result = true; } @@ -2242,10 +2236,9 @@ namespace smt { enode* n1 = get_enode(v1); enode* n2 = get_enode(v2); m_assume_eq_head++; - CTRACE("func_interp_bug", - get_value(v1) == get_value(v2) && - n1->get_root() != n2->get_root(), - tout << "assuming eq: #" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";); + CTRACE("arith", + get_value(v1) == get_value(v2) && n1->get_root() != n2->get_root(), + tout << "assuming eq: " << ctx.pp(n1) << " = #" << ctx.pp(n2) << "\n";); if (get_value(v1) == get_value(v2) && n1->get_root() != n2->get_root() && assume_eq(n1, n2)) { diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 9fb99c0b45f..4e4464a5226 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -1167,10 +1167,7 @@ namespace smt { --i; } } - CTRACE("arith", atoms.size() > 1, - for (unsigned i = 0; i < atoms.size(); ++i) { - atoms[i]->display(*this, tout); tout << "\n"; - }); + CTRACE("arith", atoms.size() > 1, for (auto* a : atoms) a->display(*this, tout) << "\n";); ptr_vector occs(m_var_occs[v]); std::sort(atoms.begin(), atoms.end(), compare_atoms()); @@ -1277,7 +1274,7 @@ namespace smt { template bool theory_arith::internalize_atom(app * n, bool gate_ctx) { - TRACE("arith_internalize", tout << "internalizing atom:\n" << mk_pp(n, m) << "\n";); + TRACE("arith_internalize", tout << "internalizing atom:\n" << mk_bounded_pp(n, m) << "\n";); SASSERT(m_util.is_le(n) || m_util.is_ge(n) || m_util.is_is_int(n)); SASSERT(!ctx.b_internalized(n)); atom_kind kind; @@ -1302,7 +1299,8 @@ namespace smt { app * lhs = to_app(n->get_arg(0)); app * rhs = to_app(n->get_arg(1)); expr * rhs2; - if (m_util.is_to_real(rhs, rhs2) && is_app(rhs2)) { rhs = to_app(rhs2); } + if (m_util.is_to_real(rhs, rhs2) && is_app(rhs2)) + rhs = to_app(rhs2); if (!m_util.is_numeral(rhs)) { throw default_exception("malformed atomic constraint"); } @@ -1335,16 +1333,14 @@ namespace smt { occs.push_back(a); m_atoms.push_back(a); insert_bv2a(bv, a); - TRACE("arith_internalize", tout << "succeeded... v" << v << " " << kind << " " << k << "\n"; - for (unsigned i = 0; i + 1 < occs.size(); ++i) tout << occs[i] << "\n";); + TRACE("arith_internalize", tout << "succeeded... v" << v << " " << kind << " " << k << "\n"); return true; } template bool theory_arith::internalize_term(app * term) { - TRACE("arith_internalize", tout << "internalising term:\n" << mk_pp(term, m) << "\n";); theory_var v = internalize_term_core(term); - TRACE("arith_internalize", tout << "theory_var: " << v << "\n";); + TRACE("arith_internalize", tout << "internalising term: v" << v << " " << mk_bounded_pp(term, m) << "\n";); return v != null_theory_var; } @@ -1375,9 +1371,9 @@ namespace smt { template void theory_arith::assign_eh(bool_var v, bool is_true) { - TRACE("arith_verbose", tout << "p" << v << " := " << (is_true?"true":"false") << "\n";); atom * a = get_bv2a(v); if (!a) return; + TRACE("arith", tout << "assign p" << literal(v,!is_true) << " : " << mk_bounded_pp(ctx.bool_var2expr(v), m) << "\n";); SASSERT(ctx.get_assignment(a->get_bool_var()) != l_undef); SASSERT((ctx.get_assignment(a->get_bool_var()) == l_true) == is_true); a->assign_eh(is_true, get_epsilon(a->get_var())); @@ -1401,9 +1397,7 @@ namespace smt { template void theory_arith::new_eq_eh(theory_var v1, theory_var v2) { - TRACE("arith_new_eq_eh", tout << "#" << get_enode(v1)->get_owner_id() << " = #" << get_enode(v2)->get_owner_id() << "\n";); - TRACE("arith_new_eq_eh_detail", tout << mk_pp(get_enode(v1)->get_expr(), m) << "\n" << - mk_pp(get_enode(v2)->get_expr(), m) << "\n";); + TRACE("arith_new_eq_eh", tout << ctx.pp(get_enode(v1)) << "\n" << ctx.pp(get_enode(v2)) << "\n";); enode * n1 = get_enode(v1); @@ -1503,7 +1497,7 @@ namespace smt { TRACE("arith", tout << "check_int_feasibility(), ok: " << ok << "\n";); break; case 1: - if (assume_eqs_core()) + if (assume_eqs()) ok = FC_CONTINUE; else ok = FC_DONE; @@ -1571,7 +1565,6 @@ namespace smt { template void theory_arith::propagate() { - TRACE("arith_propagate", tout << "propagate\n"; display(tout);); if (!process_atoms()) return; propagate_core(); @@ -1597,9 +1590,9 @@ namespace smt { failed(); return false; } - if (ctx.get_cancel_flag()) { + if (ctx.get_cancel_flag()) return true; - } + CASSERT("arith", satisfy_bounds()); discard_update_trail(); @@ -2812,7 +2805,8 @@ namespace smt { template void theory_arith::explain_bound(row const & r, int idx, bool is_lower, inf_numeral & delta, antecedents& ante) { SASSERT(delta >= inf_numeral::zero()); - TRACE("arith_conflict", tout << "relax: " << relax_bounds() << " lits: " << ante.lits().size() << " eqs: " << ante.eqs().size() << " idx: " << idx << "\n";); + TRACE("arith_conflict", tout << "delta: " << delta << " relax: " << relax_bounds() << " lits: " << ante.lits().size() << " eqs: " << ante.eqs().size() << " idx: " << idx << "\n";); + if (!relax_bounds() && (!ante.lits().empty() || !ante.eqs().empty())) { return; } @@ -3002,12 +2996,10 @@ namespace smt { TRACE("propagate_bounds", ante.display(tout) << " --> "; - ctx.display_detailed_literal(tout, l); - tout << "\n";); - - + ctx.display_detailed_literal(tout, l) << "\n"); - TRACE("arith", tout << ctx.get_scope_level() << "\n"; + TRACE("arith", tout << "@" << ctx.get_scope_level() << ": "; + ante.display(tout) << " --> "; ctx.display_detailed_literal(tout, l) << "\n"); if (ante.lits().size() < small_lemma_size() && ante.eqs().empty()) { @@ -3078,7 +3070,6 @@ namespace smt { } } - TRACE("arith_eq", tout << "done\n";); m_to_check.reset(); m_in_to_check.reset(); } @@ -3108,7 +3099,7 @@ namespace smt { TRACE("arith_conflict", if (proof_rule) tout << proof_rule << "\n"; - tout << "scope: " << ctx.get_scope_level() << "\n"; + tout << "@" << ctx.get_scope_level() << "\n"; for (unsigned i = 0; i < num_literals; i++) { ctx.display_detailed_literal(tout, lits[i]); tout << " "; @@ -3392,7 +3383,7 @@ namespace smt { } template - void theory_arith::pop_scope_eh(unsigned num_scopes) { + void theory_arith::pop_scope_eh(unsigned num_scopes) { CASSERT("arith", wf_rows()); CASSERT("arith", wf_columns()); CASSERT("arith", valid_row_assignment()); diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h index cffac245988..ebdd6e73eec 100644 --- a/src/smt/theory_arith_eq.h +++ b/src/smt/theory_arith_eq.h @@ -43,7 +43,6 @@ namespace smt { return; numeral const & val = lower_bound(v).get_rational(); value_sort_pair key(val, is_int_src(v)); - TRACE("arith_eq", tout << mk_pp(get_enode(v)->get_expr(), get_manager()) << " = " << val << "\n";); theory_var v2; if (m_fixed_var_table.find(key, v2)) { if (v2 < static_cast(get_num_vars()) && is_fixed(v2) && lower_bound(v2).get_rational() == val) { @@ -310,26 +309,22 @@ namespace smt { } // add new entry m_var_offset2row_id.insert(key, rid); - } - + } } template void theory_arith::propagate_eq_to_core(theory_var x, theory_var y, antecedents& antecedents) { // Ignore equality if variables are already known to be equal. - ast_manager& m = get_manager(); - (void)m; if (is_equal(x, y)) return; - // I doesn't make sense to propagate an equality (to the core) of variables of different sort. - if (var2expr(x)->get_sort() != var2expr(y)->get_sort()) { - TRACE("arith", tout << mk_pp(var2expr(x), m) << " = " << mk_pp(var2expr(y), m) << "\n";); - return; - } - context & ctx = get_context(); enode * _x = get_enode(x); enode * _y = get_enode(y); + // I doesn't make sense to propagate an equality (to the core) of variables of different sort. + CTRACE("arith", _x->get_sort() != _y->get_sort(), tout << enode_pp(_x, ctx) << " = " << enode_pp(_y, ctx) << "\n"); + if (_x->get_sort() != _y->get_sort()) + return; + eq_vector const& eqs = antecedents.eqs(); literal_vector const& lits = antecedents.lits(); justification * js = @@ -346,9 +341,9 @@ namespace smt { for (literal lit : lits) ctx.display_detailed_literal(tout, lit) << "\n"; for (auto const& p : eqs) - tout << pp(p.first, m) << " = " << pp(p.second, m) << "\n"; + tout << enode_pp(p.first, ctx) << " = " << enode_pp(p.second, ctx) << "\n"; tout << " ==> "; - tout << pp(_x, m) << " = " << pp(_y, m) << "\n";); + tout << enode_pp(_x, ctx) << " = " << enode_pp(_y, ctx) << "\n";); ctx.assign_eq(_x, _y, eq_justification(js)); } };