From e938ee33bbb27dfeaca5adc0c18a560d05793794 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 25 May 2020 14:11:51 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 103 ++++++++++++++++++++++++---- src/ast/rewriter/arith_rewriter.h | 6 +- 2 files changed, 92 insertions(+), 17 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index d0b43ebb3..860ad2a48 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -241,26 +241,56 @@ bool arith_rewriter::is_bound(expr * arg1, expr * arg2, op_kind kind, expr_ref & bool arith_rewriter::is_non_negative(expr* e) { - seq_util seq(m()); - if (seq.str.is_length(e)) + rational r; + auto is_even_power = [&](expr* e) { + expr* n = nullptr, *p = nullptr; + unsigned pu; + return m_util.is_power(e, n, p) && m_util.is_unsigned(p, pu) && (pu % 2 == 0); + }; + if (m_seq.str.is_length(e)) return true; - // TBD: check for even power - return false; + if (is_even_power(e)) + return true; + if (!m_util.is_mul(e)) + return false; + expr_mark mark; + ptr_buffer args; + flat_mul(e, args); + bool sign = false; + for (expr* arg : args) { + if (is_even_power(arg)) + continue; + if (m_seq.str.is_length(e)) + continue; + if (m_util.is_numeral(arg, r)) { + if (r.is_neg()) + sign = !sign; + continue; + } + mark.mark(arg, !mark.is_marked(arg)); + } + if (sign) + return false; + for (expr* arg : args) + if (mark.is_marked(arg)) + return false; + return true; } /** * perform static analysis on arg1 to determine a non-negative lower bound. * a + b + r1 <= r2 -> false if r1 > r2 and a >= 0, b >= 0 * a + b + r1 >= r2 -> false if r1 < r2 and a <= 0, b <= 0 + * a + b + r1 >= r1 -> a = 0 and b = 0 if a >= 0, b >= 0 where a, b are multipliers */ -bool arith_rewriter::is_separated(expr* arg1, expr* arg2, op_kind kind, expr_ref& result) { +br_status arith_rewriter::is_separated(expr* arg1, expr* arg2, op_kind kind, expr_ref& result) { if (kind != LE && kind != GE) - return false; + return BR_FAILED; rational bound(0), r1, r2; expr_ref narg(m()); bool has_bound = true; if (!m_util.is_numeral(arg2, r2)) - return false; + return BR_FAILED; auto update_bound = [&](expr* arg) { if (m_util.is_numeral(arg, r1)) { bound += r1; @@ -281,16 +311,58 @@ bool arith_rewriter::is_separated(expr* arg1, expr* arg2, op_kind kind, expr_ref update_bound(arg1); } if (!has_bound) - return false; - if (kind == LE && r1 > r2) { + return BR_FAILED; + + if (kind == LE && r1 < r2) + return BR_FAILED; + if (kind == GE && r1 > r2) + return BR_FAILED; + if (kind == LE && r1 > r2) { result = m().mk_false(); - return true; + return BR_DONE; } - if (kind == GE && r1 < r2) { + if (kind == GE && r1 < r2) { result = m().mk_false(); - return true; + return BR_DONE; } - return false; + + SASSERT(r1 == r2); + expr_ref zero(m_util.mk_numeral(rational(0), m().get_sort(arg1)), m()); + + if (r1.is_zero() && m_util.is_mul(arg1)) { + expr_ref_buffer eqs(m()); + ptr_buffer args; + flat_mul(arg1, args); + for (expr* arg : args) { + if (m_util.is_numeral(arg)) + continue; + eqs.push_back(m().mk_eq(arg, zero)); + } + result = m().mk_and(eqs); + return BR_REWRITE2; + } + + if (kind == LE && m_util.is_add(arg1)) { + expr_ref_buffer leqs(m()); + for (expr* arg : *to_app(arg1)) { + if (!m_util.is_numeral(arg)) + leqs.push_back(m_util.mk_le(arg, zero)); + } + result = m().mk_and(leqs); + return BR_REWRITE2; + } + + if (kind == GE && m_util.is_add(arg1)) { + expr_ref_buffer geqs(m()); + for (expr* arg : *to_app(arg1)) { + if (!m_util.is_numeral(arg)) + geqs.push_back(m_util.mk_ge(arg, zero)); + } + result = m().mk_and(geqs); + return BR_REWRITE2; + } + + return BR_FAILED; } bool arith_rewriter::elim_to_real_var(expr * var, expr_ref & new_var) { @@ -481,8 +553,9 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin ANUM_LE_GE_EQ(); } } - if (is_separated(arg1, arg2, kind, result)) - return BR_DONE; + br_status st1 = is_separated(arg1, arg2, kind, result); + if (st1 != BR_FAILED) + return st1; if (is_bound(arg1, arg2, kind, result)) return BR_DONE; if (is_bound(arg2, arg1, inv(kind), result)) diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h index a93d5f1df..06a565bb3 100644 --- a/src/ast/rewriter/arith_rewriter.h +++ b/src/ast/rewriter/arith_rewriter.h @@ -21,11 +21,13 @@ Notes: #include "ast/rewriter/poly_rewriter.h" #include "ast/arith_decl_plugin.h" +#include "ast/seq_decl_plugin.h" class arith_rewriter_core { protected: typedef rational numeral; arith_util m_util; + seq_util m_seq; bool m_expand_power; bool m_mul2power; bool m_expand_tan; @@ -43,7 +45,7 @@ protected: bool use_power() const { return m_mul2power && !m_expand_power; } decl_kind power_decl_kind() const { return OP_POWER; } public: - arith_rewriter_core(ast_manager & m):m_util(m) {} + arith_rewriter_core(ast_manager & m):m_util(m), m_seq(m) {} bool is_zero(expr * n) const { return m_util.is_zero(n); } }; @@ -64,7 +66,7 @@ class arith_rewriter : public poly_rewriter { enum op_kind { LE, GE, EQ }; static op_kind inv(op_kind k) { return k == LE ? GE : (k == GE ? LE : EQ); } bool is_bound(expr * arg1, expr * arg2, op_kind kind, expr_ref & result); - bool is_separated(expr * arg1, expr * arg2, op_kind kind, expr_ref & result); + br_status is_separated(expr * arg1, expr * arg2, op_kind kind, expr_ref & result); bool is_non_negative(expr* e); br_status mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kind, expr_ref & result);