mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

working on reconciling perf for arithmetic solvers

Browse source 
this update integrates inferences to smt.arith.solver=6 related to grobner basis computation and handling of div/mod axioms to reconcile performance with smt.arith.solver=2.

The default of smt.arth.nl.grobner_subs_fixed is changed to 1 to make comparison with solver=2 more direct.

The selection of cluster equalities for solver=6 was reconciled with how it is done for solver=2.
This commit is contained in:
Nikolaj Bjorner 2022-07-11 07:38:51 -07:00
parent 9d9414c111
commit b68af0c1e5
19 changed files with 357 additions and 282 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/params/smt_params_helper.pyg
View file

@ -71,7 +71,7 @@ def_module_params(module_name='smt',
('arith.nl.grobner_max_simplified', UINT, 10000, 'grobner\'s maximum number of simplifications'),
('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'),
('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'),
('arith.nl.grobner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),
('arith.nl.grobner_subs_fixed', UINT, 1, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),
('arith.nl.delay', UINT, 500, 'number of calls to final check before invoking bounded nlsat check'),
('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'),

2
src/smt/theory_arith_core.h
View file

@ -592,7 +592,7 @@ namespace smt {
// (or (= y 0) (<= (* y (div x y)) x))
else if (!m_util.is_numeral(divisor)) {
expr_ref div_ge(m), div_le(m), ge(m), le(m);
expr_ref div_ge(m);
div_ge = m_util.mk_ge(m_util.mk_sub(dividend, m_util.mk_mul(divisor, div)), zero);
s(div_ge);
mk_axiom(eqz, div_ge, false);

63
src/smt/theory_arith_nl.h
View file

@ -80,14 +80,12 @@ void theory_arith<Ext>::mark_dependents(theory_var v, svector<theory_var> & vars
if (is_fixed(v))
return;
column & c = m_columns[v];
typename svector<col_entry>::iterator it = c.begin_entries();
typename svector<col_entry>::iterator end = c.end_entries();
for (; it != end; ++it) {
if (it->is_dead() || already_visited_rows.contains(it->m_row_id))
for (auto& ce : c) {
if (ce.is_dead() || already_visited_rows.contains(ce.m_row_id))
continue;
TRACE("non_linear_bug", tout << "visiting row: " << it->m_row_id << "\n";);
already_visited_rows.insert(it->m_row_id);
row & r = m_rows[it->m_row_id];
TRACE("non_linear_bug", tout << "visiting row: " << ce.m_row_id << "\n";);
already_visited_rows.insert(ce.m_row_id);
row & r = m_rows[ce.m_row_id];
theory_var s = r.get_base_var();
// ignore quasi base vars... actually they should not be used if the problem is non linear...
if (is_quasi_base(s))
@ -97,14 +95,10 @@ void theory_arith<Ext>::mark_dependents(theory_var v, svector<theory_var> & vars
// was eliminated by substitution.
if (s != null_theory_var && is_free(s) && s != v)
continue;
typename vector<row_entry>::const_iterator it2 = r.begin_entries();
typename vector<row_entry>::const_iterator end2 = r.end_entries();
for (; it2 != end2; ++it2) {
if (!it2->is_dead() && !is_fixed(it2->m_var))
mark_var(it2->m_var, vars, already_found);
if (!it2->is_dead() && is_fixed(it2->m_var)) {
TRACE("non_linear", tout << "skipped fixed\n";);
}
for (auto& re : r) {
if (!re.is_dead() && !is_fixed(re.m_var))
mark_var(re.m_var, vars, already_found);
CTRACE("non_linear", !re.is_dead() && is_fixed(re.m_var), tout << "skipped fixed\n");
}
}
}
@ -119,6 +113,7 @@ void theory_arith<Ext>::get_non_linear_cluster(svector<theory_var> & vars) {
return;
var_set already_found;
row_set already_visited_rows;
for (theory_var v : m_nl_monomials) {
expr * n = var2expr(v);
if (ctx.is_relevant(n))
@ -130,9 +125,9 @@ void theory_arith<Ext>::get_non_linear_cluster(svector<theory_var> & vars) {
TRACE("non_linear", tout << "marking dependents of: v" << v << "\n";);
mark_dependents(v, vars, already_found, already_visited_rows);
}
TRACE("non_linear", tout << "variables in non linear cluster:\n";
for (theory_var v : vars) tout << "v" << v << " ";
tout << "\n";);
TRACE("non_linear", tout << "variables in non linear cluster: ";
for (theory_var v : vars) tout << "v" << v << " "; tout << "\n";
for (theory_var v : m_nl_monomials) tout << "non-linear v" << v << " " << mk_pp(var2expr(v), m) << "\n";);
}
@ -1740,22 +1735,21 @@ grobner::monomial * theory_arith<Ext>::mk_gb_monomial(rational const & _coeff, e
*/
template<typename Ext>
void theory_arith<Ext>::add_row_to_gb(row const & r, grobner & gb) {
TRACE("non_linear", tout << "adding row to gb\n"; display_row(tout, r););
TRACE("grobner", tout << "adding row to gb\n"; display_row(tout, r););
ptr_buffer<grobner::monomial> monomials;
v_dependency * dep = nullptr;
m_tmp_var_set.reset();
typename vector<row_entry>::const_iterator it = r.begin_entries();
typename vector<row_entry>::const_iterator end = r.end_entries();
for (; it != end; ++it) {
if (!it->is_dead()) {
rational coeff = it->m_coeff.to_rational();
expr * m = var2expr(it->m_var);
TRACE("non_linear", tout << "monomial: " << mk_pp(m, get_manager()) << "\n";);
grobner::monomial * new_m = mk_gb_monomial(coeff, m, gb, dep, m_tmp_var_set);
TRACE("non_linear", tout << "new monomial:\n"; if (new_m) gb.display_monomial(tout, *new_m); else tout << "null"; tout << "\n";);
if (new_m)
monomials.push_back(new_m);
}
for (auto& re : r) {
if (re.is_dead())
continue;
rational coeff = re.m_coeff.to_rational();
expr * m = var2expr(re.m_var);
grobner::monomial * new_m = mk_gb_monomial(coeff, m, gb, dep, m_tmp_var_set);
if (new_m)
monomials.push_back(new_m);
TRACE("grobner",
tout << "monomial: " << mk_pp(m, get_manager()) << "\n";
tout << "new monomial: "; if (new_m) gb.display_monomial(tout, *new_m); else tout << "null"; tout << "\n";);
}
gb.assert_eq_0(monomials.size(), monomials.data(), dep);
}
@ -2158,8 +2152,9 @@ bool theory_arith<Ext>::get_gb_eqs_and_look_for_conflict(ptr_vector<grobner::equ
eqs.reset();
gb.get_equations(eqs);
TRACE("grobner", tout << "after gb\n";
std::function<void(std::ostream& out, expr* v)> _fn = [&](std::ostream& out, expr* v) { out << "v" << expr2var(v); };
for (grobner::equation* eq : eqs)
gb.display_equation(tout, *eq);
gb.display_equation(tout, *eq, _fn);
);
for (grobner::equation* eq : eqs) {
if (is_inconsistent(eq, gb) || is_inconsistent2(eq, gb)) {
@ -2259,7 +2254,9 @@ typename theory_arith<Ext>::gb_result theory_arith<Ext>::compute_grobner(svector
ptr_vector<grobner::equation> eqs;
do {
TRACE("non_linear_gb", tout << "before:\n"; gb.display(tout););
TRACE("grobner", tout << "before grobner:\n";
std::function<void(std::ostream& out, expr* v)> _fn = [&](std::ostream& out, expr* v) { out << "v" << expr2var(v); };
gb.display(tout, _fn));
compute_basis(gb, warn);
update_statistics(gb);
TRACE("non_linear_gb", tout << "after:\n"; gb.display(tout););

82
src/smt/theory_lra.cpp
View file

@ -276,23 +276,23 @@ class theory_lra::imp {
m_nla->push();
}
smt_params_helper prms(ctx().get_params());
m_nla->settings().run_order() = prms.arith_nl_order();
m_nla->settings().run_tangents() = prms.arith_nl_tangents();
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_frequency() = prms.arith_nl_horner_frequency();
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_nra() = prms.arith_nl_nra();
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_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_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_quota() = prms.arith_nl_gr_q();
m_nla->settings().grobner_frequency() = prms.arith_nl_grobner_frequency();
m_nla->settings().expensive_patching() = false;
m_nla->settings().run_order = prms.arith_nl_order();
m_nla->settings().run_tangents = prms.arith_nl_tangents();
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_frequency = prms.arith_nl_horner_frequency();
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_nra = prms.arith_nl_nra();
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_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_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_quota = prms.arith_nl_gr_q();
m_nla->settings().grobner_frequency = prms.arith_nl_grobner_frequency();
m_nla->settings().expensive_patching = false;
}
}
@ -1224,9 +1224,9 @@ public:
return;
}
expr_ref mod_r(a.mk_add(a.mk_mul(q, div), mod), m);
ctx().get_rewriter()(mod_r);
expr_ref eq_r(th.mk_eq_atom(mod_r, p), m);
ctx().internalize(eq_r, false);
ctx().internalize(eq_r, false);
literal eq = ctx().get_literal(eq_r);
rational k(0);
@ -1256,6 +1256,38 @@ public:
}
else {
expr_ref abs_q(m.mk_ite(a.mk_ge(q, zero), q, a.mk_uminus(q)), m);
expr_ref mone(a.mk_int(-1), m);
expr_ref modmq(a.mk_sub(mod, abs_q), m);
ctx().get_rewriter()(modmq);
literal eqz = mk_literal(m.mk_eq(q, zero));
literal mod_ge_0 = mk_literal(a.mk_ge(mod, zero));
literal mod_lt_q = mk_literal(a.mk_le(modmq, mone));
// q = 0 or p = (p mod q) + q * (p div q)
// q = 0 or (p mod q) >= 0
// q = 0 or (p mod q) < abs(q)
mk_axiom(eqz, eq);
mk_axiom(eqz, mod_ge_0);
mk_axiom(eqz, mod_lt_q);
if (a.is_zero(p)) {
mk_axiom(eqz, mk_literal(m.mk_eq(div, zero)));
mk_axiom(eqz, mk_literal(m.mk_eq(mod, zero)));
}
// (or (= y 0) (<= (* y (div x y)) x))
else if (!a.is_numeral(q)) {
expr_ref div_ge(m);
div_ge = a.mk_ge(a.mk_sub(p, a.mk_mul(q, div)), zero);
ctx().get_rewriter()(div_ge);
mk_axiom(eqz, mk_literal(div_ge));
TRACE("arith", tout << eqz << " " << div_ge << "\n");
}
#if 0
/*literal div_ge_0 = */ mk_literal(a.mk_ge(div, zero));
/*literal div_le_0 = */ mk_literal(a.mk_le(div, zero));
/*literal p_ge_0 = */ mk_literal(a.mk_ge(p, zero));
@ -1266,7 +1298,7 @@ public:
// q >= 0 or (p mod q) >= 0
// q <= 0 or (p mod q) >= 0
// q <= 0 or (p mod q) < q
// q >= 0 or (p mod q) < -q
// q >= 0 or (p mod q) < -q
literal q_ge_0 = mk_literal(a.mk_ge(q, zero));
literal q_le_0 = mk_literal(a.mk_le(q, zero));
literal mod_ge_0 = mk_literal(a.mk_ge(mod, zero));
@ -1277,11 +1309,11 @@ public:
mk_axiom(q_le_0, mod_ge_0);
mk_axiom(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero)));
mk_axiom(q_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero)));
#endif
#if 0
// seem expensive
mk_axiom(q_le_0, ~p_ge_0, div_ge_0);
mk_axiom(q_le_0, ~p_le_0, div_le_0);
mk_axiom(q_ge_0, ~p_ge_0, div_le_0);
@ -1293,19 +1325,21 @@ public:
mk_axiom(q_ge_0, p_le_0, ~div_ge_0);
#endif
#if 0
std::function<void(void)> log = [&,this]() {
th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var())));
th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var())));
th.log_axiom_unit(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_sub(mod, q), zero)));
th.log_axiom_unit(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_add(mod, q), zero)));
};
if_trace_stream _ts(m, log);
#endif
#if 0
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var())));
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var())));
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var())));
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var())));
#endif
};
if_trace_stream _ts(m, log);
}
if (params().m_arith_enum_const_mod && k.is_pos() && k < rational(8)) {
unsigned _k = k.get_unsigned();