mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 11:58:31 +00:00
Code Activity

fix #3317

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-16 09:51:57 -07:00 • committed by Lev Nachmanson
parent a6941a3e75
commit 562be531e9
1 changed files with 60 additions and 55 deletions
Download patch file Download diff file Expand all files Collapse all files

109
src/smt/theory_lra.cpp
View file

@ -182,14 +182,15 @@ class theory_lra::imp {
vector<rational> m_coeffs; vector<rational> m_coeffs;
svector<theory_var> m_vars; svector<theory_var> m_vars;
rational m_offset; rational m_offset;
ptr_vector<expr> m_terms_to_internalize; ptr_vector<expr> m_to_ensure_enode, m_to_ensure_var;
internalize_state(ast_manager& m): m_terms(m) {} internalize_state(ast_manager& m): m_terms(m) {}
void reset() { void reset() {
m_terms.reset(); m_terms.reset();
m_coeffs.reset(); m_coeffs.reset();
m_offset.reset(); m_offset.reset();
m_vars.reset(); m_vars.reset();
m_terms_to_internalize.reset(); m_to_ensure_enode.reset();
m_to_ensure_var.reset();
} }
}; };
ptr_vector<internalize_state> m_internalize_states; ptr_vector<internalize_state> m_internalize_states;
@ -214,7 +215,8 @@ class theory_lra::imp {
vector<rational>& coeffs() { return m_st.m_coeffs; } vector<rational>& coeffs() { return m_st.m_coeffs; }
svector<theory_var>& vars() { return m_st.m_vars; } svector<theory_var>& vars() { return m_st.m_vars; }
rational& offset() { return m_st.m_offset; } rational& offset() { return m_st.m_offset; }
ptr_vector<expr>& terms_to_internalize() { return m_st.m_terms_to_internalize; } ptr_vector<expr>& to_ensure_enode() { return m_st.m_to_ensure_enode; }
ptr_vector<expr>& to_ensure_var() { return m_st.m_to_ensure_var; }
void push(expr* e, rational c) { m_st.m_terms.push_back(e); m_st.m_coeffs.push_back(c); } void push(expr* e, rational c) { m_st.m_terms.push_back(e); m_st.m_coeffs.push_back(c); }
void set_back(unsigned i) { void set_back(unsigned i) {
if (terms().size() == i + 1) return; if (terms().size() == i + 1) return;
@ -450,20 +452,20 @@ class theory_lra::imp {
m_nla->push(); m_nla->push();
} }
smt_params_helper prms(ctx().get_params()); smt_params_helper prms(ctx().get_params());
m_nla->settings().run_order() = prms.arith_nl_order(); m_nla->settings().run_order() = prms.arith_nl_order();
m_nla->settings().run_tangents() = prms.arith_nl_tangents(); m_nla->settings().run_tangents() = prms.arith_nl_tangents();
m_nla->settings().run_horner() = prms.arith_nl_horner(); 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_subs_fixed() = prms.arith_nl_horner_subs_fixed();
m_nla->settings().horner_frequency() = prms.arith_nl_horner_frequency(); 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().horner_row_length_limit() = prms.arith_nl_horner_row_length_limit();
m_nla->settings().run_grobner() = prms.arith_nl_grobner(); m_nla->settings().run_grobner() = prms.arith_nl_grobner();
m_nla->settings().grobner_subs_fixed() = prms.arith_nl_grobner_subs_fixed(); 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_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_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_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_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_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_quota() = prms.arith_nl_gr_q();
} }
} }
@ -543,7 +545,7 @@ class theory_lra::imp {
while (index < terms.size()) { while (index < terms.size()) {
SASSERT(index >= vars.size()); SASSERT(index >= vars.size());
expr* n = terms[index].get(); expr* n = terms[index].get();
st.terms_to_internalize().push_back(n); st.to_ensure_enode().push_back(n);
if (a.is_add(n)) { if (a.is_add(n)) {
for (expr* arg : *to_app(n)) { for (expr* arg : *to_app(n)) {
st.push(arg, coeffs[index]); st.push(arg, coeffs[index]);
@ -560,17 +562,15 @@ class theory_lra::imp {
else if (a.is_mul(n, n1, n2) && is_numeral(n1, r)) { else if (a.is_mul(n, n1, n2) && is_numeral(n1, r)) {
coeffs[index] *= r; coeffs[index] *= r;
terms[index] = n2; terms[index] = n2;
st.terms_to_internalize().push_back(n1); st.to_ensure_enode().push_back(n1);
} }
else if (a.is_mul(n, n1, n2) && is_numeral(n2, r)) { else if (a.is_mul(n, n1, n2) && is_numeral(n2, r)) {
coeffs[index] *= r; coeffs[index] *= r;
terms[index] = n1; terms[index] = n1;
st.terms_to_internalize().push_back(n2); st.to_ensure_enode().push_back(n2);
} }
else if (a.is_mul(n)) { else if (a.is_mul(n)) {
theory_var v; theory_var v = internalize_mul(to_app(n));
internalize_mul(to_app(n), v, r);
coeffs[index] *= r;
coeffs[vars.size()] = coeffs[index]; coeffs[vars.size()] = coeffs[index];
vars.push_back(v); vars.push_back(v);
++index; ++index;
@ -620,18 +620,26 @@ class theory_lra::imp {
app_ref mod(a.mk_mod(n1, n2), m); app_ref mod(a.mk_mod(n1, n2), m);
ctx().internalize(mod, false); ctx().internalize(mod, false);
if (ctx().relevancy()) ctx().add_relevancy_dependency(n, mod); if (ctx().relevancy()) ctx().add_relevancy_dependency(n, mod);
st.to_ensure_var().push_back(n1);
st.to_ensure_var().push_back(n2);
} }
else if (a.is_mod(n, n1, n2)) { else if (a.is_mod(n, n1, n2)) {
if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n); if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n);
if (!ctx().relevancy()) mk_idiv_mod_axioms(n1, n2); if (!ctx().relevancy()) 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)) { else if (a.is_rem(n, n1, n2)) {
if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n); if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n);
if (!ctx().relevancy()) mk_rem_axiom(n1, n2); if (!ctx().relevancy()) 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)) { else if (a.is_div(n, n1, n2)) {
if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n); if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n);
if (!ctx().relevancy()) mk_div_axiom(n1, n2); if (!ctx().relevancy()) 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)) { else if (!a.is_div0(n) && !a.is_mod0(n) && !a.is_idiv0(n) && !a.is_rem0(n)) {
found_unsupported(n); found_unsupported(n);
@ -650,52 +658,55 @@ class theory_lra::imp {
++index; ++index;
} }
} }
for (unsigned i = st.terms_to_internalize().size(); i-- > 0; ) { for (unsigned i = st.to_ensure_enode().size(); i-- > 0; ) {
expr* n = st.terms_to_internalize()[i]; expr* n = st.to_ensure_enode()[i];
if (is_app(n)) { if (is_app(n)) {
mk_enode(to_app(n)); mk_enode(to_app(n));
} }
} }
st.terms_to_internalize().reset(); 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 internalize_args(app* t) { void internalize_args(app* t) {
for (unsigned i = 0; reflect(t) && i < t->get_num_args(); ++i) { if (!reflect(t))
if (!ctx().e_internalized(t->get_arg(i))) { return;
ctx().internalize(t->get_arg(i), false); for (expr* arg : *t) {
if (!ctx().e_internalized(arg)) {
ctx().internalize(arg, false);
} }
} }
} }
void internalize_mul(app* t, theory_var& v, rational& r) { theory_var internalize_mul(app* t) {
SASSERT(a.is_mul(t)); SASSERT(a.is_mul(t));
internalize_args(t); internalize_args(t);
bool _has_var = has_var(t); bool _has_var = has_var(t);
mk_enode(t); mk_enode(t);
v = mk_var(t); theory_var v = mk_var(t);
svector<lpvar> vars;
r = rational::one();
rational r1;
for (expr* n : *t) { if (!_has_var) {
if (a.is_numeral(n, r1)) { svector<lpvar> vars;
r *= r1; for (expr* n : *t) {
}
else {
SASSERT(ctx().e_internalized(n)); SASSERT(ctx().e_internalized(n));
vars.push_back(register_theory_var_in_lar_solver(mk_var(n))); vars.push_back(register_theory_var_in_lar_solver(mk_var(n)));
} }
} TRACE("arith", tout << "v" << v << " := " << mk_pp(t, m) << "\n" << vars << "\n";);
TRACE("arith", tout << "v" << v << " := " << mk_pp(t, m) << "\n" << vars << "\n";);
if (!_has_var) {
m_solver->register_existing_terms(); m_solver->register_existing_terms();
m_switcher.add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.c_ptr()); m_switcher.add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.c_ptr());
} }
return v;
} }
enode * mk_enode(app * n) { enode * mk_enode(app * n) {
TRACE("arith", tout << expr_ref(n, m) << "\n";); TRACE("arith", tout << expr_ref(n, m) << " internalized: " << ctx().e_internalized(n) << "\n";);
if (ctx().e_internalized(n)) { if (ctx().e_internalized(n)) {
return get_enode(n); return get_enode(n);
} }
@ -758,6 +769,7 @@ class theory_lra::imp {
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)) {
TRACE("arith", tout << "fresh var: " << mk_pp(n, m) << "\n";);
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());
if (m_bounds.size() <= static_cast<unsigned>(v)) { if (m_bounds.size() <= static_cast<unsigned>(v)) {
@ -1825,10 +1837,9 @@ public:
VERIFY(a.is_idiv(n, p, q)); VERIFY(a.is_idiv(n, p, q));
theory_var v = mk_var(n); theory_var v = mk_var(n);
theory_var v1 = mk_var(p); theory_var v1 = mk_var(p);
if (!can_get_ivalue(v1)) if (!can_get_ivalue(v1))
continue; continue;
if (!can_get_ivalue(v))
continue;
lp::impq r1 = get_ivalue(v1); lp::impq r1 = get_ivalue(v1);
rational r2; rational r2;
@ -1847,8 +1858,8 @@ public:
TRACE("arith", tout << "unbounded " << expr_ref(n, m) << "\n";); TRACE("arith", tout << "unbounded " << expr_ref(n, m) << "\n";);
continue; continue;
} }
if (!can_get_ivalue(v)) if (!can_get_ivalue(v))
continue; continue;
lp::impq val_v = get_ivalue(v); lp::impq val_v = get_ivalue(v);
if (val_v.y.is_zero() && val_v.x == div(r1.x, r2)) continue; if (val_v.y.is_zero() && val_v.x == div(r1.x, r2)) continue;
@ -3248,12 +3259,6 @@ public:
m_core.push_back(lit); m_core.push_back(lit);
} }
// 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
/*
static unsigned cn = 0;
static unsigned num_l = 0;
num_l+=m_explanation.size();
std::cout << num_l / (++cn) << "\n";
*/
++m_num_conflicts; ++m_num_conflicts;
++m_stats.m_conflicts; ++m_stats.m_conflicts;
TRACE("arith", tout << "scope: " << ctx().get_scope_level() << "\n"; display_evidence(tout, m_explanation); ); TRACE("arith", tout << "scope: " << ctx().get_scope_level() << "\n"; display_evidence(tout, m_explanation); );