Skip to content

Commit

Permalink
household chores in legacy arithmetic solver
Browse files Browse the repository at this point in the history
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Nov 18, 2023
1 parent 5ab1afe commit e40b8a2
Show file tree
Hide file tree
Showing 4 changed files with 48 additions and 69 deletions.
10 changes: 5 additions & 5 deletions src/smt/theory_arith.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
};


Expand All @@ -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 {
Expand All @@ -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 {
Expand All @@ -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;

};

Expand Down Expand Up @@ -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();

// -----------------------------------
Expand Down
41 changes: 17 additions & 24 deletions src/smt/theory_arith_aux.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -370,8 +370,8 @@ namespace smt {


template<typename Ext>
void theory_arith<Ext>::bound::display(theory_arith<Ext> const& th, std::ostream& out) const {
out << "v" << get_var() << " " << get_bound_kind() << " " << get_value();
std::ostream& theory_arith<Ext>::bound::display(theory_arith<Ext> const& th, std::ostream& out) const {
return out << "v" << get_var() << " " << get_bound_kind() << " " << get_value();
}


Expand Down Expand Up @@ -414,11 +414,10 @@ namespace smt {
}

template<typename Ext>
void theory_arith<Ext>::atom::display(theory_arith<Ext> const& th, std::ostream& out) const {
std::ostream& theory_arith<Ext>::atom::display(theory_arith<Ext> 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;
}

// -----------------------------------
Expand All @@ -428,10 +427,10 @@ namespace smt {
// -----------------------------------

template<typename Ext>
void theory_arith<Ext>::eq_bound::display(theory_arith<Ext> const& th, std::ostream& out) const {
std::ostream& theory_arith<Ext>::eq_bound::display(theory_arith<Ext> 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);
}

// -----------------------------------
Expand Down Expand Up @@ -752,7 +751,7 @@ namespace smt {
}

template<typename Ext>
void theory_arith<Ext>::derived_bound::display(theory_arith<Ext> const& th, std::ostream& out) const {
std::ostream& theory_arith<Ext>::derived_bound::display(theory_arith<Ext> 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";
Expand All @@ -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;
}


Expand Down Expand Up @@ -2195,33 +2195,27 @@ namespace smt {
}

template<typename Ext>
bool theory_arith<Ext>::assume_eqs_core() {
bool theory_arith<Ext>::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;
}
Expand All @@ -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)) {
Expand Down
45 changes: 18 additions & 27 deletions src/smt/theory_arith_core.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<atom> occs(m_var_occs[v]);

std::sort(atoms.begin(), atoms.end(), compare_atoms());
Expand Down Expand Up @@ -1277,7 +1274,7 @@ namespace smt {

template<typename Ext>
bool theory_arith<Ext>::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;
Expand All @@ -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");
}
Expand Down Expand Up @@ -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<typename Ext>
bool theory_arith<Ext>::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;
}

Expand Down Expand Up @@ -1375,9 +1371,9 @@ namespace smt {

template<typename Ext>
void theory_arith<Ext>::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()));
Expand All @@ -1401,9 +1397,7 @@ namespace smt {

template<typename Ext>
void theory_arith<Ext>::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);

Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -1571,7 +1565,6 @@ namespace smt {

template<typename Ext>
void theory_arith<Ext>::propagate() {
TRACE("arith_propagate", tout << "propagate\n"; display(tout););
if (!process_atoms())
return;
propagate_core();
Expand All @@ -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();

Expand Down Expand Up @@ -2812,7 +2805,8 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::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;
}
Expand Down Expand Up @@ -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()) {
Expand Down Expand Up @@ -3078,7 +3070,6 @@ namespace smt {
}
}

TRACE("arith_eq", tout << "done\n";);
m_to_check.reset();
m_in_to_check.reset();
}
Expand Down Expand Up @@ -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 << " ";
Expand Down Expand Up @@ -3392,7 +3383,7 @@ namespace smt {
}

template<typename Ext>
void theory_arith<Ext>::pop_scope_eh(unsigned num_scopes) {
void theory_arith<Ext>::pop_scope_eh(unsigned num_scopes) {
CASSERT("arith", wf_rows());
CASSERT("arith", wf_columns());
CASSERT("arith", valid_row_assignment());
Expand Down
21 changes: 8 additions & 13 deletions src/smt/theory_arith_eq.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<int>(get_num_vars()) && is_fixed(v2) && lower_bound(v2).get_rational() == val) {
Expand Down Expand Up @@ -310,26 +309,22 @@ namespace smt {
}
// add new entry
m_var_offset2row_id.insert(key, rid);
}

}
}


template<typename Ext>
void theory_arith<Ext>::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 =
Expand All @@ -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));
}
};
Expand Down

0 comments on commit e40b8a2

Please sign in to comment.