na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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<expr> 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<expr> 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))

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<arith_rewriter_core> {
     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);