mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

chores in theory_lra

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-11-18 10:05:26 -08:00
parent e40b8a2d13
commit 5bec982cc5
1 changed files with 72 additions and 142 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

214
src/smt/theory_lra.cpp
View file

@ -77,7 +77,6 @@ class theory_lra::imp {
bool get_cancel_flag() override { return !m_imp.m.inc(); } bool get_cancel_flag() override { return !m_imp.m.inc(); }
}; };
theory_lra& th; theory_lra& th;
ast_manager& m; ast_manager& m;
arith_util a; arith_util a;
@ -198,12 +197,10 @@ class theory_lra::imp {
imp & m_th; imp & m_th;
var_value_hash(imp & th):m_th(th) {} var_value_hash(imp & th):m_th(th) {}
unsigned operator()(theory_var v) const { unsigned operator()(theory_var v) const {
if (m_th.use_nra_model()) { if (m_th.use_nra_model())
return m_th.is_int(v); return m_th.is_int(v);
} else
else {
return (unsigned)std::hash<lp::impq>()(m_th.get_ivalue(v)); return (unsigned)std::hash<lp::impq>()(m_th.get_ivalue(v));
}
} }
}; };
int_hashtable<var_value_hash, var_value_eq> m_model_eqs; int_hashtable<var_value_hash, var_value_eq> m_model_eqs;
@ -229,12 +226,14 @@ class theory_lra::imp {
bool is_real(enode* n) const { return a.is_real(n->get_expr()); } bool is_real(enode* n) const { return a.is_real(n->get_expr()); }
enode* get_enode(theory_var v) const { return th.get_enode(v); } enode* get_enode(theory_var v) const { return th.get_enode(v); }
enode* get_enode(expr* e) const { return ctx().get_enode(e); } enode* get_enode(expr* e) const { return ctx().get_enode(e); }
expr* get_owner(theory_var v) const { return get_enode(v)->get_expr(); } expr* get_owner(theory_var v) const { return get_enode(v)->get_expr(); }
enode_pp pp(enode* n) const { return enode_pp(n, ctx()); }
enode_pp pp(theory_var v) const { return pp(get_enode(v)); }
mk_bounded_pp bpp(expr* e) { return mk_bounded_pp(e, m); }
lpvar add_const(int c, lpvar& var, bool is_int) { lpvar add_const(int c, lpvar& var, bool is_int) {
if (var != UINT_MAX) { if (var != UINT_MAX)
return var; return var;
}
app_ref cnst(a.mk_numeral(rational(c), is_int), m); app_ref cnst(a.mk_numeral(rational(c), is_int), m);
mk_enode(cnst); mk_enode(cnst);
theory_var v = mk_var(cnst); theory_var v = mk_var(cnst);
@ -551,7 +550,7 @@ class theory_lra::imp {
theory_var v = mk_var(n); theory_var v = mk_var(n);
vars.push_back(register_theory_var_in_lar_solver(v)); vars.push_back(register_theory_var_in_lar_solver(v));
} }
TRACE("arith", tout << "v" << v << " := " << mk_pp(t, m) << "\n" << vars << "\n";); TRACE("arith", tout << "v" << v << " := " << bpp(t) << "\n" << vars << "\n";);
m_solver->register_existing_terms(); m_solver->register_existing_terms();
ensure_nla(); ensure_nla();
m_nla->add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.data()); m_nla->add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.data());
@ -560,7 +559,7 @@ class theory_lra::imp {
} }
enode * mk_enode(app * n) { enode * mk_enode(app * n) {
TRACE("arith", tout << mk_bounded_pp(n, m) << " internalized: " << ctx().e_internalized(n) << "\n";); TRACE("arith_verbose", tout << bpp(n) << " internalized: " << ctx().e_internalized(n) << "\n";);
if (reflect(n)) if (reflect(n))
for (expr* arg : *n) for (expr* arg : *n)
if (!ctx().e_internalized(arg)) if (!ctx().e_internalized(arg))
@ -606,20 +605,18 @@ class theory_lra::imp {
} }
theory_var mk_var(expr* n) { theory_var mk_var(expr* n) {
if (!ctx().e_internalized(n)) { if (!ctx().e_internalized(n))
ctx().internalize(n, false); ctx().internalize(n, false);
}
enode* e = get_enode(n); enode* e = get_enode(n);
theory_var v; theory_var v;
if (!th.is_attached_to_var(e)) { if (th.is_attached_to_var(e))
v = e->get_th_var(get_id());
else {
v = th.mk_var(e); v = th.mk_var(e);
SASSERT(m_bounds.size() <= static_cast<unsigned>(v) || m_bounds[v].empty()); SASSERT(m_bounds.size() <= static_cast<unsigned>(v) || m_bounds[v].empty());
reserve_bounds(v); reserve_bounds(v);
ctx().attach_th_var(e, &th, v); ctx().attach_th_var(e, &th, v);
} }
else {
v = e->get_th_var(get_id());
}
SASSERT(null_theory_var != v); SASSERT(null_theory_var != v);
return v; return v;
} }
@ -640,12 +637,10 @@ class theory_lra::imp {
for (unsigned i = 0; i < vars.size(); ++i) { for (unsigned i = 0; i < vars.size(); ++i) {
theory_var var = vars[i]; theory_var var = vars[i];
rational const& coeff = coeffs[i]; rational const& coeff = coeffs[i];
if (m_columns.size() <= static_cast<unsigned>(var)) { if (m_columns.size() <= static_cast<unsigned>(var))
m_columns.setx(var, coeff, rational::zero()); m_columns.setx(var, coeff, rational::zero());
} else
else {
m_columns[var] += coeff; m_columns[var] += coeff;
}
} }
m_left_side.clear(); m_left_side.clear();
// reset the coefficients after they have been used. // reset the coefficients after they have been used.
@ -653,7 +648,7 @@ class theory_lra::imp {
theory_var var = vars[i]; theory_var var = vars[i];
rational const& r = m_columns[var]; rational const& r = m_columns[var];
if (!r.is_zero()) { if (!r.is_zero()) {
m_left_side.push_back(std::make_pair(r, register_theory_var_in_lar_solver(var))); m_left_side.push_back({r, register_theory_var_in_lar_solver(var)});
m_columns[var].reset(); m_columns[var].reset();
} }
} }
@ -661,12 +656,7 @@ class theory_lra::imp {
} }
bool all_zeros(vector<rational> const& v) const { bool all_zeros(vector<rational> const& v) const {
for (rational const& r : v) { return all_of(v, [](rational const& r) { return r.is_zero(); });
if (!r.is_zero()) {
return false;
}
}
return true;
} }
void add_eq_constraint(lp::constraint_index index, enode* n1, enode* n2) { void add_eq_constraint(lp::constraint_index index, enode* n1, enode* n2) {
@ -689,7 +679,6 @@ class theory_lra::imp {
m_definitions.setx(index, v, null_theory_var); m_definitions.setx(index, v, null_theory_var);
} }
bool is_infeasible() const { bool is_infeasible() const {
return lp().get_status() == lp::lp_status::INFEASIBLE; return lp().get_status() == lp::lp_status::INFEASIBLE;
} }
@ -718,9 +707,8 @@ class theory_lra::imp {
lpvar vi_equal; lpvar vi_equal;
lp::constraint_index ci = lp().add_var_bound_check_on_equal(vi, kind, bound, vi_equal); lp::constraint_index ci = lp().add_var_bound_check_on_equal(vi, kind, bound, vi_equal);
add_def_constraint(ci); add_def_constraint(ci);
if (vi_equal != lp::null_lpvar) { if (vi_equal != lp::null_lpvar)
report_equality_of_fixed_vars(vi, vi_equal); report_equality_of_fixed_vars(vi, vi_equal);
}
m_new_def = true; m_new_def = true;
} }
@ -734,22 +722,9 @@ class theory_lra::imp {
theory_var z = internalize_linearized_def(term, st); theory_var z = internalize_linearized_def(term, st);
lpvar vi = register_theory_var_in_lar_solver(z); lpvar vi = register_theory_var_in_lar_solver(z);
add_def_constraint_and_equality(vi, lp::LE, rational::zero()); add_def_constraint_and_equality(vi, lp::LE, rational::zero());
if (is_infeasible()) {
IF_VERBOSE(0, verbose_stream() << "infeasible\n";);
// process_conflict(); // exit here?
}
add_def_constraint_and_equality(vi, lp::GE, rational::zero()); add_def_constraint_and_equality(vi, lp::GE, rational::zero());
if (is_infeasible()) {
IF_VERBOSE(0, verbose_stream() << "infeasible\n";);
// process_conflict(); // exit here?
}
TRACE("arith", TRACE("arith",
{ tout << "v" << v1 << " = " << "v" << v2 << ": " << pp(v1) << " = " << pp(v2) << "\n");
expr* o1 = get_enode(v1)->get_expr();
expr* o2 = get_enode(v2)->get_expr();
tout << "v" << v1 << " = " << "v" << v2 << ": "
<< mk_pp(o1, m) << " = " << mk_pp(o2, m) << "\n";
});
} }
void del_bounds(unsigned old_size) { void del_bounds(unsigned old_size) {
@ -764,7 +739,7 @@ class theory_lra::imp {
} }
void updt_unassigned_bounds(theory_var v, int inc) { void updt_unassigned_bounds(theory_var v, int inc) {
TRACE("arith", tout << "v" << v << " " << m_unassigned_bounds[v] << " += " << inc << "\n";); TRACE("arith_verbose", tout << "v" << v << " " << m_unassigned_bounds[v] << " += " << inc << "\n";);
ctx().push_trail(vector_value_trail<unsigned, false>(m_unassigned_bounds, v)); ctx().push_trail(vector_value_trail<unsigned, false>(m_unassigned_bounds, v));
m_unassigned_bounds[v] += inc; m_unassigned_bounds[v] += inc;
} }
@ -821,7 +796,7 @@ class theory_lra::imp {
theory_var internalize_linearized_def(app* term, scoped_internalize_state& st) { theory_var internalize_linearized_def(app* term, scoped_internalize_state& st) {
theory_var v = mk_var(term); theory_var v = mk_var(term);
TRACE("arith", tout << mk_bounded_pp(term, m) << " v" << v << "\n";); TRACE("arith_internalize", tout << "v" << v << " " << bpp(term) << "\n";);
if (is_unit_var(st) && v == st.vars()[0]) if (is_unit_var(st) && v == st.vars()[0])
return st.vars()[0]; return st.vars()[0];
@ -918,7 +893,7 @@ public:
} }
bool internalize_atom(app * atom, bool gate_ctx) { bool internalize_atom(app * atom, bool gate_ctx) {
TRACE("arith", tout << mk_pp(atom, m) << "\n";); TRACE("arith_internalize", tout << bpp(atom) << "\n";);
SASSERT(!ctx().b_internalized(atom)); SASSERT(!ctx().b_internalized(atom));
expr* n1, *n2; expr* n1, *n2;
rational r; rational r;
@ -953,17 +928,16 @@ public:
return true; return true;
} }
if (is_int(v) && !r.is_int()) { if (is_int(v) && !r.is_int())
r = (k == lp_api::upper_t) ? floor(r) : ceil(r); r = (k == lp_api::upper_t) ? floor(r) : ceil(r);
}
api_bound* b = mk_var_bound(bv, v, k, r); api_bound* b = mk_var_bound(bv, v, k, r);
m_bounds[v].push_back(b); m_bounds[v].push_back(b);
updt_unassigned_bounds(v, +1); updt_unassigned_bounds(v, +1);
m_bounds_trail.push_back(v); m_bounds_trail.push_back(v);
m_bool_var2bound.insert(bv, b); m_bool_var2bound.insert(bv, b);
TRACE("arith_verbose", tout << "Internalized " << bv << ": " << mk_pp(atom, m) << "\n";);
mk_bound_axioms(*b); mk_bound_axioms(*b);
//add_use_lists(b); TRACE("arith_internalize", tout << "Internalized " << bv << ": " << bpp(atom) << "\n";);
return true; return true;
} }
@ -989,14 +963,12 @@ public:
enode * n1 = get_enode(lhs); enode * n1 = get_enode(lhs);
enode * n2 = get_enode(rhs); enode * n2 = get_enode(rhs);
if (is_arith(n1) && is_arith(n2) && if (is_arith(n1) && is_arith(n2) && n1 != n2)
n1->get_th_var(get_id()) != null_theory_var &&
n2->get_th_var(get_id()) != null_theory_var && n1 != n2)
m_arith_eq_adapter.mk_axioms(n1, n2); m_arith_eq_adapter.mk_axioms(n1, n2);
} }
void assign_eh(bool_var v, bool is_true) { void assign_eh(bool_var v, bool is_true) {
TRACE("arith", tout << mk_bounded_pp(ctx().bool_var2expr(v), m) << " " << (literal(v, !is_true)) << "\n";); TRACE("arith", tout << "assign p" << literal(v, !is_true) << ": " << bpp(ctx().bool_var2expr(v)) << "\n";);
m_asserted_atoms.push_back(delayed_atom(v, is_true)); m_asserted_atoms.push_back(delayed_atom(v, is_true));
} }
@ -1041,16 +1013,14 @@ public:
} }
void apply_sort_cnstr(enode* n, sort*) { void apply_sort_cnstr(enode* n, sort*) {
TRACE("arith", tout << "sort constraint: " << enode_pp(n, ctx()) << "\n";); TRACE("arith", tout << "sort constraint: " << pp(n) << "\n";);
#if 0 #if 0
if (!th.is_attached_to_var(n)) { if (!th.is_attached_to_var(n))
mk_var(n->get_owner()); mk_var(n->get_owner());
}
#endif #endif
} }
void push_scope_eh() { void push_scope_eh() {
TRACE("arith", tout << "push\n";);
m_scopes.push_back(scope()); m_scopes.push_back(scope());
scope& sc = m_scopes.back(); scope& sc = m_scopes.back();
sc.m_bounds_lim = m_bounds_trail.size(); sc.m_bounds_lim = m_bounds_trail.size();
@ -1059,14 +1029,11 @@ public:
lp().push(); lp().push();
if (m_nla) if (m_nla)
m_nla->push(); m_nla->push();
} }
void pop_scope_eh(unsigned num_scopes) { void pop_scope_eh(unsigned num_scopes) {
TRACE("arith", tout << "pop " << num_scopes << "\n";); if (num_scopes == 0)
if (num_scopes == 0) {
return; return;
}
unsigned old_size = m_scopes.size() - num_scopes; unsigned old_size = m_scopes.size() - num_scopes;
del_bounds(m_scopes[old_size].m_bounds_lim); del_bounds(m_scopes[old_size].m_bounds_lim);
m_asserted_atoms.shrink(m_scopes[old_size].m_asserted_atoms_lim); m_asserted_atoms.shrink(m_scopes[old_size].m_asserted_atoms_lim);
@ -1531,13 +1498,14 @@ public:
} }
bool assume_eqs() { bool assume_eqs() {
if (delayed_assume_eqs()) if (delayed_assume_eqs())
return true; return true;
TRACE("arith", display(tout);); TRACE("arith_verbose", display(tout););
random_update(); random_update();
m_model_eqs.reset(); m_model_eqs.reset();
theory_var sz = static_cast<theory_var>(th.get_num_vars()); theory_var sz = static_cast<theory_var>(th.get_num_vars());
unsigned old_sz = m_assume_eq_candidates.size(); unsigned old_sz = m_assume_eq_candidates.size();
unsigned num_candidates = 0; unsigned num_candidates = 0;
@ -1545,30 +1513,23 @@ public:
for (theory_var i = 0; i < sz; ++i) { for (theory_var i = 0; i < sz; ++i) {
theory_var v = (i + start) % sz; theory_var v = (i + start) % sz;
enode* n1 = get_enode(v); enode* n1 = get_enode(v);
if (!th.is_relevant_and_shared(n1)) { if (!th.is_relevant_and_shared(n1))
continue; continue;
}
ensure_column(v); ensure_column(v);
if (!is_registered_var(v)) if (!is_registered_var(v))
continue; continue;
theory_var other = m_model_eqs.insert_if_not_there(v); theory_var other = m_model_eqs.insert_if_not_there(v);
TRACE("arith", tout << "insert: v" << v << " := " << get_value(v) << " found: v" << other << "\n";); if (other == v)
if (other == v) {
continue; continue;
}
enode* n2 = get_enode(other); enode* n2 = get_enode(other);
if (n1->get_root() != n2->get_root()) { if (n1->get_root() == n2->get_root())
TRACE("arith", tout << pp(n1, m) << " = " << pp(n2, m) << "\n"; continue;
tout << pp(n1, m) << " = " << pp(n2, m) << "\n"; m_assume_eq_candidates.push_back({v, other});
tout << "v" << v << " = " << "v" << other << "\n";); num_candidates++;
m_assume_eq_candidates.push_back(std::make_pair(v, other));
num_candidates++;
}
} }
if (num_candidates > 0) { if (num_candidates > 0)
ctx().push_trail(restore_vector(m_assume_eq_candidates, old_sz)); ctx().push_trail(restore_vector(m_assume_eq_candidates, old_sz));
}
return delayed_assume_eqs(); return delayed_assume_eqs();
} }
@ -1642,9 +1603,8 @@ public:
IF_VERBOSE(12, verbose_stream() << "final-check " << lp().get_status() << "\n"); IF_VERBOSE(12, verbose_stream() << "final-check " << lp().get_status() << "\n");
lbool is_sat = l_true; lbool is_sat = l_true;
SASSERT(lp().ax_is_correct()); SASSERT(lp().ax_is_correct());
if (!lp().is_feasible() || lp().has_changed_columns()) { if (!lp().is_feasible() || lp().has_changed_columns())
is_sat = make_feasible(); is_sat = make_feasible();
}
final_check_status st = FC_DONE; final_check_status st = FC_DONE;
switch (is_sat) { switch (is_sat) {
case l_true: case l_true:
@ -2128,31 +2088,28 @@ public:
propagate_nla(); propagate_nla();
if (ctx().inconsistent()) if (ctx().inconsistent())
return true; return true;
if (!can_propagate_core()) if (!can_propagate_core())
return false; return false;
m_new_def = false; m_new_def = false;
while (m_asserted_qhead < m_asserted_atoms.size() && !ctx().inconsistent() && m.inc()) { while (m_asserted_qhead < m_asserted_atoms.size() && !ctx().inconsistent() && m.inc()) {
auto [bv, is_true] = m_asserted_atoms[m_asserted_qhead]; auto [bv, is_true] = m_asserted_atoms[m_asserted_qhead];
// m_bv_to_propagate.push_back(bv);
api_bound* b = nullptr; api_bound* b = nullptr;
TRACE("arith", tout << "propagate: " << literal(bv, !is_true) << "\n"; TRACE("arith", tout << "propagate: " << literal(bv, !is_true) << "\n";
if (!m_bool_var2bound.contains(bv)) tout << "not found\n"); if (!m_bool_var2bound.contains(bv)) tout << "not found\n");
if (m_bool_var2bound.find(bv, b)) if (m_bool_var2bound.find(bv, b) && !assert_bound(bv, is_true, *b)) {
assert_bound(bv, is_true, *b); get_infeasibility_explanation_and_set_conflict();
return true;
}
++m_asserted_qhead; ++m_asserted_qhead;
} }
if (ctx().inconsistent()) { if (ctx().inconsistent())
m_bv_to_propagate.reset();
return true; return true;
}
lbool lbl = make_feasible(); lbool lbl = make_feasible();
if (!m.inc()) if (!m.inc())
return false; return true;
switch(lbl) { switch(lbl) {
case l_false: case l_false:
@ -2160,7 +2117,6 @@ public:
get_infeasibility_explanation_and_set_conflict(); get_infeasibility_explanation_and_set_conflict();
break; break;
case l_true: case l_true:
propagate_basic_bounds();
propagate_bounds_with_lp_solver(); propagate_bounds_with_lp_solver();
break; break;
case l_undef: case l_undef:
@ -2236,10 +2192,8 @@ public:
if (!m.inc()) if (!m.inc())
return; return;
if (is_infeasible()) { if (is_infeasible()) {
get_infeasibility_explanation_and_set_conflict(); get_infeasibility_explanation_and_set_conflict();
// verbose_stream() << "unsat\n";
} }
else { else {
for (auto& ib : m_bp.ibounds()) { for (auto& ib : m_bp.ibounds()) {
@ -2417,7 +2371,7 @@ public:
enode* n1 = get_enode(uv); enode* n1 = get_enode(uv);
enode* n2 = get_enode(vv); enode* n2 = get_enode(vv);
TRACE("arith", tout << "add-eq " << mk_pp(n1->get_expr(), m) << " == " << mk_pp(n2->get_expr(), m) << " " << n1->get_expr_id() << " == " << n2->get_expr_id() << "\n";); TRACE("arith", tout << "add-eq " << pp(n1) << " == " << pp(n2) << "\n";);
if (n1->get_root() == n2->get_root()) if (n1->get_root() == n2->get_root())
return false; return false;
expr* e1 = n1->get_expr(); expr* e1 = n1->get_expr();
@ -2721,18 +2675,6 @@ public:
} }
return end; return end;
} }
void propagate_basic_bounds() {
for (auto const& bv : m_bv_to_propagate) {
api_bound* b = nullptr;
if (m_bool_var2bound.find(bv, b)) {
propagate_bound(bv, ctx().get_assignment(bv) == l_true, *b);
if (ctx().inconsistent())
break;
}
}
m_bv_to_propagate.reset();
}
// for glb lo': lo' < lo: // for glb lo': lo' < lo:
// lo <= x -> lo' <= x // lo <= x -> lo' <= x
@ -2865,7 +2807,7 @@ public:
// //
void propagate_bound_compound(bool_var bv, bool is_true, api_bound& b) { void propagate_bound_compound(bool_var bv, bool is_true, api_bound& b) {
theory_var v = b.get_var(); theory_var v = b.get_var();
TRACE("arith", tout << mk_pp(get_owner(v), m) << "\n";); TRACE("arith", tout << pp(v) << "\n";);
if (static_cast<unsigned>(v) >= m_use_list.size()) { if (static_cast<unsigned>(v) >= m_use_list.size()) {
return; return;
} }
@ -2974,13 +2916,12 @@ public:
return lp::EQ; return lp::EQ;
} }
void assert_bound(bool_var bv, bool is_true, api_bound& b) { bool assert_bound(bool_var bv, bool is_true, api_bound& b) {
TRACE("arith", tout << b << "\n";); TRACE("arith", tout << b << "\n";);
lp::constraint_index ci = b.get_constraint(is_true); lp::constraint_index ci = b.get_constraint(is_true);
lp().activate(ci); lp().activate(ci);
if (is_infeasible()) { if (is_infeasible())
return; return false;
}
lp::lconstraint_kind k = bound2constraint_kind(b.is_int(), b.get_bound_kind(), is_true); lp::lconstraint_kind k = bound2constraint_kind(b.is_int(), b.get_bound_kind(), is_true);
if (k == lp::LT || k == lp::LE) { if (k == lp::LT || k == lp::LE) {
++m_stats.m_assert_lower; ++m_stats.m_assert_lower;
@ -2989,9 +2930,9 @@ public:
++m_stats.m_assert_upper; ++m_stats.m_assert_upper;
} }
inf_rational value = b.get_value(is_true); inf_rational value = b.get_value(is_true);
if (propagate_eqs() && value.is_rational()) { if (propagate_eqs() && value.is_rational())
propagate_eqs(b.tv(), ci, k, b, value.get_rational()); propagate_eqs(b.tv(), ci, k, b, value.get_rational());
} return true;
#if 0 #if 0
if (should_propagate()) if (should_propagate())
lp().add_column_rows_to_touched_rows(b.tv().id()); lp().add_column_rows_to_touched_rows(b.tv().id());
@ -3079,7 +3020,6 @@ public:
return true; return true;
} }
else { else {
TRACE("arith", tout << "not a term " << tv.to_string() << "\n";);
// m_solver already tracks bounds on proper variables, but not on terms. // m_solver already tracks bounds on proper variables, but not on terms.
bool is_strict = false; bool is_strict = false;
rational b; rational b;
@ -3155,7 +3095,7 @@ public:
u_dependency* ci1 = nullptr, *ci2 = nullptr, *ci3 = nullptr, *ci4 = nullptr; u_dependency* ci1 = nullptr, *ci2 = nullptr, *ci3 = nullptr, *ci4 = nullptr;
theory_var v1 = lp().local_to_external(vi1); theory_var v1 = lp().local_to_external(vi1);
theory_var v2 = lp().local_to_external(vi2); theory_var v2 = lp().local_to_external(vi2);
TRACE("arith", tout << "fixed: " << mk_pp(get_owner(v1), m) << " " << mk_pp(get_owner(v2), m) << "\n";); TRACE("arith", tout << "fixed: " << pp(v1) << " " << pp(v2) << "\n";);
// we expect lp() to ensure that none of these returns happen. // we expect lp() to ensure that none of these returns happen.
if (is_equal(v1, v2)) if (is_equal(v1, v2))
return; return;
@ -3191,8 +3131,8 @@ public:
for (auto c : m_core) for (auto c : m_core)
ctx().display_detailed_literal(tout << ctx().get_assign_level(c.var()) << " " << c << " ", c) << "\n"; ctx().display_detailed_literal(tout << ctx().get_assign_level(c.var()) << " " << c << " ", c) << "\n";
for (auto e : m_eqs) for (auto e : m_eqs)
tout << pp(e.first, m) << " = " << pp(e.second, m) << "\n"; tout << pp(e.first) << " = " << pp(e.second) << "\n";
tout << " ==> " << pp(x, m) << " = " << pp(y, m) << "\n"; tout << " ==> " << pp(x) << " = " << pp(y) << "\n";
); );
std::function<expr*(void)> fn = [&]() { return m.mk_eq(x->get_expr(), y->get_expr()); }; std::function<expr*(void)> fn = [&]() { return m.mk_eq(x->get_expr(), y->get_expr()); };
@ -3214,6 +3154,7 @@ public:
else else
return; return;
enode* y = get_enode(w); enode* y = get_enode(w);
TRACE("arith", tout << pp(x) << " == " << pp(y) << "\n");
if (x->get_sort() != y->get_sort()) if (x->get_sort() != y->get_sort())
return; return;
if (x->get_root() == y->get_root()) if (x->get_root() == y->get_root())
@ -3303,8 +3244,8 @@ public:
// lp().shrink_explanation_to_minimum(m_explanation); // todo, enable when perf is fixed // lp().shrink_explanation_to_minimum(m_explanation); // todo, enable when perf is fixed
++m_num_conflicts; ++m_num_conflicts;
++m_stats.m_conflicts; ++m_stats.m_conflicts;
TRACE("arith", TRACE("arith_conflict",
tout << "lemma scope: " << ctx().get_scope_level(); tout << "@" << ctx().get_scope_level() << (is_conflict ? " conflict":" lemma");
for (auto const& p : m_params) tout << " " << p; for (auto const& p : m_params) tout << " " << p;
tout << "\n"; tout << "\n";
display_evidence(tout, m_explanation);); display_evidence(tout, m_explanation););
@ -3330,16 +3271,6 @@ public:
ctx().mark_as_relevant(c); ctx().mark_as_relevant(c);
} }
TRACE("arith", ctx().display_literals_verbose(tout, m_core) << "\n";); TRACE("arith", ctx().display_literals_verbose(tout, m_core) << "\n";);
// DEBUG_CODE(
// for (literal const& c : m_core) {
// if (ctx().get_assignment(c) == l_true) {
// TRACE("arith", ctx().display_literal_verbose(tout, c) << " is true\n";);
// SASSERT(false);
// }
// }); // TODO: this check seems to be too strict.
// The lemmas can come in batches
// and the same literal can appear in several lemmas in a batch: it becomes l_true
// in earlier processing, but it was not so when the lemma was produced
ctx().mk_th_axiom(get_id(), m_core.size(), m_core.data()); ctx().mk_th_axiom(get_id(), m_core.size(), m_core.data());
} }
} }
@ -3359,7 +3290,6 @@ public:
m_assume_eq_head = 0; m_assume_eq_head = 0;
m_scopes.reset(); m_scopes.reset();
m_stats.reset(); m_stats.reset();
m_bv_to_propagate.reset();
m_model_is_initialized = false; m_model_is_initialized = false;
} }
@ -3385,7 +3315,7 @@ public:
m_nla->am().set(r, m_nla->am_value(t.id())); m_nla->am().set(r, m_nla->am_value(t.id()));
else { else {
m_todo_terms.push_back(std::make_pair(t, rational::one())); m_todo_terms.push_back({t, rational::one()});
TRACE("nl_value", tout << "v" << v << " " << t.to_string() << "\n";); TRACE("nl_value", tout << "v" << v << " " << t.to_string() << "\n";);
TRACE("nl_value", tout << "v" << v << " := w" << t.to_string() << "\n"; TRACE("nl_value", tout << "v" << v << " := w" << t.to_string() << "\n";
lp().print_term(lp().get_term(t), tout) << "\n";); lp().print_term(lp().get_term(t), tout) << "\n";);
@ -3405,7 +3335,7 @@ public:
auto wi = lp().column2tv(arg.column()); auto wi = lp().column2tv(arg.column());
c1 = arg.coeff() * wcoeff; c1 = arg.coeff() * wcoeff;
if (wi.is_term()) { if (wi.is_term()) {
m_todo_terms.push_back(std::make_pair(wi, c1)); m_todo_terms.push_back({wi, c1});
} }
else { else {
m_nla->am().set(r1, c1.to_mpq()); m_nla->am().set(r1, c1.to_mpq());
@ -3785,6 +3715,7 @@ public:
m_bounds[v].push_back(a); m_bounds[v].push_back(a);
m_bounds_trail.push_back(v); m_bounds_trail.push_back(v);
m_bool_var2bound.insert(bv, a); m_bool_var2bound.insert(bv, a);
TRACE("arith", tout << "internalized " << bv << ": " << mk_pp(b, m) << "\n";); TRACE("arith", tout << "internalized " << bv << ": " << mk_pp(b, m) << "\n";);
} }
if (is_strict) { if (is_strict) {
@ -3814,7 +3745,7 @@ public:
else if (can_get_value(v)) out << " = " << get_value(v); else if (can_get_value(v)) out << " = " << get_value(v);
if (is_int(v)) out << ", int"; if (is_int(v)) out << ", int";
if (ctx().is_shared(get_enode(v))) out << ", shared"; if (ctx().is_shared(get_enode(v))) out << ", shared";
out << " := " << enode_pp(get_enode(v), ctx()) << "\n"; out << " := " << pp(v) << "\n";
} }
} }
@ -3830,17 +3761,17 @@ public:
case inequality_source: { case inequality_source: {
literal lit = m_inequalities[idx]; literal lit = m_inequalities[idx];
ctx().literal2expr(lit, e); ctx().literal2expr(lit, e);
out << e << " " << ctx().get_assignment(lit) << "\n"; out << bpp(e) << " " << ctx().get_assignment(lit) << "\n";
break; break;
} }
case equality_source: case equality_source:
out << pp(m_equalities[idx].first, m) << " = " out << pp(m_equalities[idx].first) << " = "
<< pp(m_equalities[idx].second, m) << "\n"; << pp(m_equalities[idx].second) << "\n";
break; break;
case definition_source: { case definition_source: {
theory_var v = m_definitions[idx]; theory_var v = m_definitions[idx];
if (v != null_theory_var) if (v != null_theory_var)
out << "def: v" << v << " := " << pp(th.get_enode(v), m) << "\n"; out << "def: v" << v << " := " << pp(th.get_enode(v)) << "\n";
break; break;
} }
case null_source: case null_source:
@ -3851,9 +3782,8 @@ public:
break; break;
} }
} }
for (lp::explanation::cimpq ev : evidence) { for (lp::explanation::cimpq ev : evidence)
lp().constraints().display(out << ev.coeff() << ": ", ev.ci()); lp().constraints().display(out << ev.coeff() << ": ", ev.ci());
}
} }
void collect_statistics(::statistics & st) const { void collect_statistics(::statistics & st) const {