some simplifications based on Z3Prover#4178

Author: NikolajBjorner

src/ast/rewriter/bit_blaster/bit_blaster.cpp

@@ -36,6 +36,7 @@ static void sort_args(expr * & l1, expr * & l2, expr * & l3) {
     l1 = args[0]; l2 = args[1]; l3 = args[2];
 }
 
+
 void bit_blaster_cfg::mk_xor3(expr * l1, expr * l2, expr * l3, expr_ref & r) {
     TRACE("xor3", tout << "#" << l1->get_id() << " #" << l2->get_id() << " #" << l3->get_id(););
     sort_args(l1, l2, l3);

src/ast/rewriter/bit_blaster/bit_blaster.h

@@ -44,6 +44,7 @@ class bit_blaster_cfg {
     void mk_and(expr * a, expr * b, expr_ref & r) { m_rw.mk_and(a, b, r); }
     void mk_and(expr * a, expr * b, expr * c, expr_ref & r) { m_rw.mk_and(a, b, c, r); }
     void mk_and(unsigned sz, expr * const * args, expr_ref & r) { m_rw.mk_and(sz, args, r); }
+    void mk_ge2(expr* a, expr* b, expr* c, expr_ref& r) { m_rw.mk_ge2(a, b, c, r); }
     void mk_or(expr * a, expr * b, expr_ref & r) { m_rw.mk_or(a, b, r); }
     void mk_or(expr * a, expr * b, expr * c, expr_ref & r) { m_rw.mk_or(a, b, c, r); }
     void mk_or(unsigned sz, expr * const * args, expr_ref & r) { m_rw.mk_or(sz, args, r); }

src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp

@@ -64,6 +64,7 @@ struct blaster_cfg {
     void mk_ite(expr * c, expr * t, expr * e, expr_ref & r) { m_rewriter.mk_ite(c, t, e, r); }
     void mk_nand(expr * a, expr * b, expr_ref & r) { m_rewriter.mk_nand(a, b, r); }
     void mk_nor(expr * a, expr * b, expr_ref & r) { m_rewriter.mk_nor(a, b, r); }
+    void mk_ge2(expr * a, expr * b, expr * c, expr_ref& r) { m_rewriter.mk_ge2(a, b, c, r); }
 };
 
 class blaster : public bit_blaster_tpl<blaster_cfg> {

src/ast/rewriter/bit_blaster/bit_blaster_tpl.h

@@ -70,6 +70,7 @@ class bit_blaster_tpl : public Cfg {
     void mk_ite(expr * c, expr * t, expr * e, expr_ref & r) { Cfg::mk_ite(c, t, e, r); }
     void mk_nand(expr * a, expr * b, expr_ref & r) { Cfg::mk_nand(a, b, r); }
     void mk_nor(expr * a, expr * b, expr_ref & r) { Cfg::mk_nor(a, b, r); }
+    void mk_ge2(expr* a, expr* b, expr* c, expr_ref& r) { Cfg::mk_ge2(a, b, c, r); }
     //
 
 

src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h

@@ -1101,23 +1101,17 @@ template<typename Cfg>
 template<bool Signed>
 void bit_blaster_tpl<Cfg>::mk_le(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref & out) {
     SASSERT(sz > 0);
-    expr_ref i1(m()), i2(m()), i3(m()), not_a(m());
+    expr_ref not_a(m());
     mk_not(a_bits[0], not_a);
     mk_or(not_a, b_bits[0], out);
     for (unsigned idx = 1; idx < (Signed ? sz - 1 : sz); idx++) {
         mk_not(a_bits[idx], not_a);
-        mk_and(not_a,       b_bits[idx], i1);
-        mk_and(not_a,       out,         i2);
-        mk_and(b_bits[idx], out,         i3);
-        mk_or(i1, i2, i3, out);
+        mk_ge2(not_a, b_bits[idx], out, out);
     }
     if (Signed) {
         expr_ref not_b(m());
         mk_not(b_bits[sz-1], not_b);
-        mk_and(not_b,        a_bits[sz-1], i1);
-        mk_and(not_b,        out,          i2);
-        mk_and(a_bits[sz-1], out,          i3);
-        mk_or(i1, i2, i3, out);
+        mk_ge2(not_b, a_bits[sz-1], out, out);
     }
 }
 

src/ast/rewriter/bool_rewriter.cpp

@@ -1031,4 +1031,22 @@ void bool_rewriter::mk_nor(expr * arg1, expr * arg2, expr_ref & result) {
     mk_not(tmp, result);
 }
 
+
+void bool_rewriter::mk_ge2(expr* a, expr* b, expr* c, expr_ref& r) {
+    if (m().is_false(a)) mk_and(b, c, r);
+    else if (m().is_false(b)) mk_and(a, c, r);
+    else if (m().is_false(c)) mk_and(a, b, r);
+    else if (m().is_true(a)) mk_or(b, c, r);
+    else if (m().is_true(b)) mk_or(a, c, r);
+    else if (m().is_true(c)) mk_or(a, b, r);
+    else {
+        expr_ref i1(m()), i2(m()), i3(m());
+        mk_and(a, b, i1);
+        mk_and(a, c, i2);
+        mk_and(b, c, i3);
+        mk_or(i1, i2, i3, r);
+    }
+}
+
+
 template class rewriter_tpl<bool_rewriter_cfg>;

src/ast/rewriter/bool_rewriter.h

@@ -179,6 +179,7 @@ class bool_rewriter {
     void mk_nor(unsigned num_args, expr * const * args, expr_ref & result);
     void mk_nand(expr * arg1, expr * arg2, expr_ref & result);
     void mk_nor(expr * arg1, expr * arg2, expr_ref & result);
+    void mk_ge2(expr* a, expr* b, expr* c, expr_ref& result);
 };
 
 struct bool_rewriter_cfg : public default_rewriter_cfg {

src/ast/rewriter/bv_rewriter.cpp

@@ -513,6 +513,12 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
         return BR_REWRITE2;
     }
 
+    // (bvule c (+ c a)) -> (bvule a (2^n - c))  (could be generalized)
+    if (!is_signed && is_num1 && m_util.is_bv_add(b, a1, a2) && is_numeral(a1, r2, sz) && r1 == r2) {
+        result = m_util.mk_ule(a2, m_util.mk_numeral(-r1, sz));
+        return BR_REWRITE1;
+    }
+        
     if (m_le_extra) {
         const br_status cst = rw_leq_concats(is_signed, a, b, result);
         if (cst != BR_FAILED) {