add option to rewrite and for arithmetic simplification

src/ast/rewriter/arith_rewriter.cpp

@@ -706,6 +706,31 @@ br_status arith_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result
     return st;
 }
 
+br_status arith_rewriter::mk_and_core(unsigned n, expr* const* args, expr_ref& result) {
+    if (n <= 1)
+        return BR_FAILED;
+    expr* x, * y, * z, * u;
+    rational a, b;
+    if (m_util.is_le(args[0], x, y) && m_util.is_numeral(x, a)) {
+        expr* arg0 = args[0];
+        ptr_buffer<expr> rest;
+        for (unsigned i = 1; i < n; ++i) {
+            if (m_util.is_le(args[i], z, u) && u == y && m_util.is_numeral(z, b)) {
+                if (b > a)
+                    arg0 = args[i];
+            }
+            else
+                rest.push_back(args[i]);
+        }
+        if (rest.size() < n - 1) {
+            rest.push_back(arg0);
+            result = m().mk_and(rest);
+            return BR_REWRITE1;
+        }
+    }
+    return BR_FAILED;
+}
+
 bool arith_rewriter::mk_eq_mod(expr* arg1, expr* arg2, expr_ref& result) {
     expr* x = nullptr, *y = nullptr, *z = nullptr, *u = nullptr;
     rational p, k, l;

src/ast/rewriter/arith_rewriter.h

@@ -149,6 +149,8 @@ public:
 
     br_status mk_abs_core(expr * arg, expr_ref & result);
 
+    br_status mk_and_core(unsigned n, expr* const* args, expr_ref& result);
+
     br_status mk_div_core(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_idiv_core(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_idivides(unsigned k, expr * arg, expr_ref & result);

src/ast/rewriter/bool_rewriter.cpp

@@ -175,7 +175,7 @@ br_status bool_rewriter::mk_flat_and_core(unsigned num_args, expr * const * args
         }
         if (mk_nflat_and_core(flat_args.size(), flat_args.data(), result) == BR_FAILED)
             result = m().mk_and(flat_args);
-        return BR_DONE;
+        return BR_REWRITE1;
     }
     return mk_nflat_and_core(num_args, args, result);
 }
@@ -874,7 +874,7 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
                 expr_ref tmp(m());
                 mk_not(c, tmp);
                 mk_and(tmp, e, result);
-                return BR_DONE;
+                return BR_REWRITE1;
             }
         }
         if (m().is_true(e) && m_elim_ite) {            
@@ -885,11 +885,11 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
         }
         if (m().is_false(e) && m_elim_ite) {
             mk_and(c, t, result);
-            return BR_DONE;
+            return BR_REWRITE1;
         }
         if (c == e && m_elim_ite) {
             mk_and(c, t, result);
-            return BR_DONE;
+            return BR_REWRITE1;
         }
         if (c == t && m_elim_ite) {
             mk_or(c, e, result);
@@ -912,13 +912,13 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
         expr_ref a(m());
         mk_and(c, t2, a);
         result = m().mk_not(m().mk_eq(t1, a));
-        return BR_REWRITE2;
+        return BR_REWRITE3;
     }
     if (m().is_not(t, t1) && m().is_eq(t1, t2, t1) && e == t1) {
         expr_ref a(m());
         mk_and(c, t2, a);
         result = m().mk_eq(t1, a);
-        return BR_REWRITE2;
+        return BR_REWRITE3;
     }
 #endif
 
@@ -931,14 +931,14 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
             expr_ref new_c(m());
             mk_and(c, not_c2, new_c);
             result = m().mk_ite(new_c, to_app(t)->get_arg(2), e);
-            return BR_REWRITE1;
+            return BR_REWRITE2;
         }
         // (ite c1 (ite c2 t1 t2) t2) ==> (ite (and c1 c2) t1 t2)
         if (e == to_app(t)->get_arg(2)) {
             expr_ref new_c(m());
             mk_and(c, to_app(t)->get_arg(0), new_c);
             result = m().mk_ite(new_c, to_app(t)->get_arg(1), e);
-            return BR_REWRITE1;
+            return BR_REWRITE2;
         }
 
 
@@ -955,7 +955,7 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
                 expr_ref new_c(m());
                 mk_or(and1, and2, new_c);
                 result = m().mk_ite(new_c, to_app(t)->get_arg(1), to_app(t)->get_arg(2));
-                return BR_REWRITE1;
+                return BR_REWRITE3;
             }
 
             // (ite c1 (ite c2 t1 t2) (ite c3 t2 t1)) ==> (ite (or (and c1 c2) (and (not c1) (not c3))) t1 t2)
@@ -972,7 +972,7 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
                 expr_ref new_c(m());
                 mk_or(and1, and2, new_c);
                 result = m().mk_ite(new_c, to_app(t)->get_arg(1), to_app(t)->get_arg(2));
-                return BR_REWRITE1;
+                return BR_REWRITE3;
             }
         }
     }

src/ast/rewriter/th_rewriter.cpp

@@ -215,6 +215,11 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
                 if (st != BR_FAILED)
                     return st;
             }
+            if (false && k == OP_AND) {
+                st = m_a_rw.mk_and_core(num, args, result);
+                if (st != BR_FAILED)
+                    return st;
+            }
             if (k == OP_EQ && m_seq_rw.u().has_seq() && is_app(args[0]) &&
                 to_app(args[0])->get_family_id() == m_seq_rw.get_fid()) {
                 st = m_seq_rw.mk_eq_core(args[0], args[1], result);

src/model/model_evaluator.cpp

@@ -262,6 +262,11 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 if (st != BR_FAILED)
                     return st;
             }
+            if (k == OP_AND) {
+                st = m_a_rw.mk_and_core(num, args, result);
+                if (st != BR_FAILED)
+                    return st;
+            }
             return m_b_rw.mk_app_core(f, num, args, result);
         }
         if (fid == m_a_rw.get_fid())