distribute concat over bvxor and bvor, #2470

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

src/ast/rewriter/bv_rewriter.cpp

@@ -1737,6 +1737,9 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
     default:
         if (m_bv_sort_ac)
             std::sort(new_args.begin(), new_args.end(), ast_to_lt());
+        if (distribute_concat(OP_BOR, new_args.size(), new_args.c_ptr(), result)) {
+            return BR_REWRITE3;
+        }
         result = m_util.mk_bv_or(new_args.size(), new_args.c_ptr());
         return BR_DONE;
     }
@@ -1863,8 +1866,12 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
     }
 
     if (!merged && !flattened && (num_coeffs == 0 || (num_coeffs == 1 && !v1.is_zero() && v1 != (rational::power_of_two(sz) - numeral(1)))) &&
-        (!m_bv_sort_ac || is_sorted(num, args)))
+        (!m_bv_sort_ac || is_sorted(num, args))) {
+        if (distribute_concat(OP_BXOR, num, args, result)) {
+            return BR_REWRITE3;
+        }
         return BR_FAILED;
+    }
 
     ptr_buffer<expr> new_args;
     expr_ref c(m()); // may not be used
@@ -1906,11 +1913,35 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
     default:
         if (m_bv_sort_ac)
             std::sort(new_args.begin(), new_args.end(), ast_to_lt());
+        if (distribute_concat(OP_BXOR, new_args.size(), new_args.c_ptr(), result)) {
+            return BR_REWRITE3;
+        }
         result = m_util.mk_bv_xor(new_args.size(), new_args.c_ptr());
         return BR_DONE;
     }
 }
 
+bool bv_rewriter::distribute_concat(decl_kind k, unsigned n, expr* const* args, expr_ref& result) {
+    for (unsigned i = 0; i < n; ++i) {
+        expr* arg = args[i];
+        if (m_util.is_concat(arg)) {
+            expr* e = to_app(arg)->get_arg(0);
+            unsigned sz1 = get_bv_size(e);
+            unsigned sz2 = get_bv_size(arg);
+            ptr_buffer<expr> args1, args2;
+            for (unsigned j = 0; j < n; ++j) {
+                args1.push_back(m_mk_extract(sz2-1, sz1, args[j]));
+                args2.push_back(m_mk_extract(sz1-1,0, args[j]));
+            }
+            expr* arg1 = m().mk_app(get_fid(), k, args1.size(), args1.c_ptr());
+            expr* arg2 = m().mk_app(get_fid(), k, args2.size(), args2.c_ptr());
+            result = m_util.mk_concat(arg1, arg2);
+            return true;
+        }
+    }
+    return false;
+}
+
 br_status bv_rewriter::mk_bv_not(expr * arg, expr_ref & result) {
     if (m_util.is_bv_not(arg)) {
         result = to_app(arg)->get_arg(0);
@@ -1925,17 +1956,14 @@ br_status bv_rewriter::mk_bv_not(expr * arg, expr_ref & result) {
         return BR_DONE;
     }
 
-#if 1
     if (m_util.is_concat(arg)) {
         ptr_buffer<expr> new_args;
-        unsigned num = to_app(arg)->get_num_args();
-        for (unsigned i = 0; i < num; i++) {
-            new_args.push_back(m_util.mk_bv_not(to_app(arg)->get_arg(i)));
+        for (expr* a : *to_app(arg)) {
+            new_args.push_back(m_util.mk_bv_not(a));
         }
         result = m_util.mk_concat(new_args.size(), new_args.c_ptr());
         return BR_REWRITE2;
     }
-#endif
 
     if (m_bvnot2arith) {
         // (bvnot x) --> (bvsub -1 x)

src/ast/rewriter/bv_rewriter.h

@@ -107,6 +107,7 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     br_status mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result);
+    bool distribute_concat(decl_kind op, unsigned n, expr* const* args, expr_ref& result);
     bool is_minus_one_core(expr * arg) const;
     bool is_x_minus_one(expr * arg, expr * & x);
     bool is_add_no_overflow(expr* e);

src/smt/theory_lra.cpp

@@ -2015,29 +2015,16 @@ class theory_lra::imp {
         }
         while (m_asserted_qhead < m_asserted_atoms.size() && !ctx().inconsistent()) {
             bool_var bv  = m_asserted_atoms[m_asserted_qhead].m_bv;
-            bool is_true = m_asserted_atoms[m_asserted_qhead].m_is_true;
-
-#if 1
+            bool is_true = m_asserted_atoms[m_asserted_qhead].m_is_true;                
             m_to_check.push_back(bv);
-#else
-            propagate_bound(bv, is_true, b);
-#endif
             lp_api::bound& b = *m_bool_var2bound.find(bv);
-            assert_bound(bv, is_true, b);
-
-
+            assert_bound(bv, is_true, b);                
             ++m_asserted_qhead;
         }
         if (ctx().inconsistent()) {
             m_to_check.reset();
             return;
         }
-        /*for (; qhead < m_asserted_atoms.size() && !ctx().inconsistent(); ++qhead) {
-          bool_var bv  = m_asserted_atoms[qhead].m_bv;
-          bool is_true = m_asserted_atoms[qhead].m_is_true;
-          lp_api::bound& b = *m_bool_var2bound.find(bv);
-          propagate_bound_compound(bv, is_true, b);
-          }*/
 
         lbool lbl = make_feasible();