Skip to content

Commit

Permalink
perf and div/mod axioms #4532
Browse files Browse the repository at this point in the history 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Jun 22, 2020
1 parent 38d6771 commit 8758baf
Show file tree
Hide file tree
Showing 2 changed files with 38 additions and 5 deletions.
6 changes: 5 additions & 1 deletion src/ast/rewriter/arith_rewriter.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -975,6 +975,10 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
result = arg1;
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()) {
return BR_FAILED;
}
Expand Down Expand Up @@ -1119,7 +1123,7 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
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);
return BR_DONE;
}
Expand Down
37 changes: 33 additions & 4 deletions src/smt/theory_lra.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1325,12 +1325,14 @@ class theory_lra::imp {
mk_axiom(q_le_0, m_le_0);
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);
#endif
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);
expr_ref upper(m);
Expand Down Expand Up @@ -1361,9 +1363,18 @@ class theory_lra::imp {
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()) {
mk_axiom(~p_ge_0, div_ge_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]() {
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())));
Expand All @@ -1373,14 +1384,22 @@ class theory_lra::imp {
else {
mk_axiom(~p_ge_0, div_le_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]() {
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())));
};
if_trace_stream _ts(m, log);
}
#endif
}
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 mod q) >= 0
Expand All @@ -1396,20 +1415,30 @@ class theory_lra::imp {
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)));
#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);
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]() {
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 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);
}
Expand Down

0 comments on commit 8758baf

Please sign in to comment.