mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-16 19:06:17 +00:00
Code Activity

perf and div/mod axioms #4532

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-06-22 14:51:58 -07:00
parent 38d6771a5e
commit 8758baf24e
2 changed files with 38 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/rewriter/arith_rewriter.cpp
View file

@ -975,6 +975,10 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
result = arg1; result = arg1;
return BR_DONE; return BR_DONE;
} }
if (m_util.is_numeral(arg2, v2, is_int) && v2.is_minus_one()) {
result = m_util.mk_mul(m_util.mk_int(-1), arg1);
return BR_REWRITE1;
}
if (m_util.is_numeral(arg2, v2, is_int) && v2.is_zero()) { if (m_util.is_numeral(arg2, v2, is_int) && v2.is_zero()) {
return BR_FAILED; return BR_FAILED;
} }
@ -1119,7 +1123,7 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
return BR_DONE; return BR_DONE;
} }
if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_one()) { if (m_util.is_numeral(arg2, v2, is_int) && is_int && (v2.is_one() || v2.is_minus_one())) {
result = m_util.mk_numeral(numeral(0), true); result = m_util.mk_numeral(numeral(0), true);
return BR_DONE; return BR_DONE;
} }

37
src/smt/theory_lra.cpp
View file

@ -1325,12 +1325,14 @@ public:
mk_axiom(q_le_0, m_le_0); mk_axiom(q_le_0, m_le_0);
return; return;
} }
#if 0
expr_ref eqr(m.mk_eq(a.mk_add(a.mk_mul(q, div), mod), p), m);
ctx().get_rewriter()(eqr);
literal eq = mk_literal(eqr);
#else
literal eq = th.mk_eq(a.mk_add(a.mk_mul(q, div), mod), p, false); literal eq = th.mk_eq(a.mk_add(a.mk_mul(q, div), mod), p, false);
#endif
literal mod_ge_0 = mk_literal(a.mk_ge(mod, zero)); literal mod_ge_0 = mk_literal(a.mk_ge(mod, zero));
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));
literal p_le_0 = mk_literal(a.mk_le(p, zero));
rational k(0); rational k(0);
expr_ref upper(m); expr_ref upper(m);
@ -1361,9 +1363,18 @@ public:
if_trace_stream _ts(m, log); if_trace_stream _ts(m, log);
} }
#if 0
// creates more literals than useful.
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));
literal p_le_0 = mk_literal(a.mk_le(p, zero));
if (k.is_pos()) { if (k.is_pos()) {
mk_axiom(~p_ge_0, div_ge_0); mk_axiom(~p_ge_0, div_ge_0);
mk_axiom(~p_le_0, div_le_0); mk_axiom(~p_le_0, div_le_0);
mk_axiom(p_ge_0, ~div_ge_0);
mk_axiom(p_le_0, ~div_le_0);
std::function<void(void)> log = [&,this]() { std::function<void(void)> log = [&,this]() {
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_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_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var())));
@ -1373,14 +1384,22 @@ public:
else { else {
mk_axiom(~p_ge_0, div_le_0); mk_axiom(~p_ge_0, div_le_0);
mk_axiom(~p_le_0, div_ge_0); mk_axiom(~p_le_0, div_ge_0);
mk_axiom(p_ge_0, ~div_le_0);
mk_axiom(p_le_0, ~div_ge_0);
std::function<void(void)> log = [&,this]() { std::function<void(void)> log = [&,this]() {
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_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()))); 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())));
}; };
if_trace_stream _ts(m, log); if_trace_stream _ts(m, log);
} }
#endif
} }
else { else {
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));
literal p_le_0 = mk_literal(a.mk_le(p, zero));
// q >= 0 or p = (p mod q) + q * (p div q) // q >= 0 or p = (p mod q) + q * (p div q)
// q <= 0 or p = (p mod q) + q * (p div q) // q <= 0 or p = (p mod q) + q * (p div q)
// q >= 0 or (p mod q) >= 0 // q >= 0 or (p mod q) >= 0
@ -1396,20 +1415,30 @@ public:
mk_axiom(q_le_0, mod_ge_0); 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_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))); mk_axiom(q_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero)));
#if 0
// seem expensive
mk_axiom(q_le_0, ~p_ge_0, div_ge_0); 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_le_0, ~p_le_0, div_le_0);
mk_axiom(q_ge_0, ~p_ge_0, div_le_0); mk_axiom(q_ge_0, ~p_ge_0, div_le_0);
mk_axiom(q_ge_0, ~p_le_0, div_ge_0); mk_axiom(q_ge_0, ~p_le_0, div_ge_0);
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);
mk_axiom(q_ge_0, p_le_0, ~div_ge_0);
#endif
std::function<void(void)> log = [&,this]() { 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(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(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_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))); th.log_axiom_unit(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_add(mod, q), zero)));
#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_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_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_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()))); 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_trace_stream _ts(m, log);
} }