From 5de35d46eb30f46f02bfcb29c05b292482eca51a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 10 Jul 2019 08:54:32 +0100 Subject: [PATCH] fix #2390 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 26 ++++++++++++++++++++++++++ src/tactic/smtlogics/qflia_tactic.cpp | 2 +- 2 files changed, 27 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 21707d3c2..ddaa0339e 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -456,6 +456,32 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin st = BR_DONE; } } + expr* e1 = nullptr, *e2 = nullptr; + if (m_util.is_div(arg1, e1, e2) && (!is_numeral(e2, a2) || !a2.is_zero())) { + new_arg1 = e1; + new_arg2 = m_util.mk_mul(e2, arg2); + expr_ref zero(m_util.mk_numeral(rational(0), m_util.is_int(arg1)), m()); + expr_ref is_zero(m().mk_eq(zero, e2), m()); + expr_ref div0(m_util.mk_div(e1, zero), m()); + expr_ref mul2(m_util.mk_mul(e2, arg2), m()); + switch (kind) { + case LE: + result = m().mk_or( + m().mk_and(is_zero, m_util.mk_le(div0, arg2)), + m().mk_and(m_util.mk_gt(e2, zero), m_util.mk_le(e1, mul2)), + m().mk_and(m_util.mk_lt(e2, zero), m_util.mk_ge(e1, mul2))); + return BR_REWRITE2; + case GE: + result = m().mk_or( + m().mk_and(is_zero, m_util.mk_ge(div0, arg2)), + m().mk_and(m_util.mk_gt(e2, zero), m_util.mk_ge(e1, mul2)), + m().mk_and(m_util.mk_lt(e2, zero), m_util.mk_le(e1, mul2))); + return BR_REWRITE2; + case EQ: + result = m().mk_ite(is_zero, m().mk_eq(div0, arg2), m().mk_eq(e1, mul2)); + return BR_REWRITE2; + } + } if ((m_arith_lhs || m_arith_ineq_lhs) && is_numeral(arg2, a2) && is_neg_poly(arg1, new_arg1)) { a2.neg(); new_arg2 = m_util.mk_numeral(a2, m_util.is_int(new_arg1)); diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp index 1a535d18c..0899d6a3e 100644 --- a/src/tactic/smtlogics/qflia_tactic.cpp +++ b/src/tactic/smtlogics/qflia_tactic.cpp @@ -184,7 +184,7 @@ tactic * mk_preamble_tactic(ast_manager& m) { pull_ite_p.set_bool("push_ite_arith", false); pull_ite_p.set_bool("local_ctx", true); pull_ite_p.set_uint("local_ctx_limit", 10000000); - + pull_ite_p.set_bool("hoist_ite", true); params_ref ctx_simp_p; ctx_simp_p.set_uint("max_depth", 30);