Starting to work on trailing 0 analysis.

src/ast/rewriter/bv_rewriter.cpp

@@ -20,6 +20,7 @@ Notes:
 #include"bv_rewriter_params.hpp"
 #include"poly_rewriter_def.h"
 #include"ast_smt2_pp.h"
+#include"bv_trailing.h"
 
 
 mk_extract_proc::mk_extract_proc(bv_util & u):
@@ -61,6 +62,7 @@ void bv_rewriter::updt_local_params(params_ref const & _p) {
     m_elim_sign_ext = p.elim_sign_ext();
     m_mul2concat = p.mul2concat();
     m_bit2bool = p.bit2bool();
+    m_trailing = p.bv_trailing();
     m_blast_eq_value = p.blast_eq_value();
     m_split_concat_eq = p.split_concat_eq();
     m_udiv2mul = p.udiv2mul();
@@ -2124,6 +2126,15 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
             return st;
     }
 
+    if (m_trailing) {
+        bv_trailing bvt(m(), m_mk_extract);
+        st = bvt.eq_remove_trailing(lhs, rhs, result);
+        if (st != BR_FAILED) {
+            TRACE("eq_remove_trailing", tout << mk_ismt2_pp(lhs, m()) << "\n=\n" << mk_ismt2_pp(rhs, m()) << "\n----->\n" << mk_ismt2_pp(result, m()) << "\n";);
+            return st;
+        }
+    }
+
     st = mk_mul_eq(lhs, rhs, result);
     if (st != BR_FAILED) {
         TRACE("mk_mul_eq", tout << mk_ismt2_pp(lhs, m()) << "\n=\n" << mk_ismt2_pp(rhs, m()) << "\n----->\n" << mk_ismt2_pp(result,m()) << "\n";);
@@ -2187,6 +2198,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
     return BR_FAILED;
 }
 
+
 br_status bv_rewriter::mk_mkbv(unsigned num, expr * const * args, expr_ref & result) {
     if (m_mkbv2num) {
         unsigned i;

src/ast/rewriter/bv_rewriter.h

@@ -69,6 +69,7 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     bool       m_udiv2mul;
     bool       m_bvnot2arith;
     bool       m_bv_sort_ac;
+    bool       m_trailing;
 
     bool is_zero_bit(expr * x, unsigned idx);
 

src/ast/rewriter/bv_rewriter_params.pyg

@@ -9,5 +9,6 @@ def_module_params(module_name='rewriter',
                           ("hi_div0", BOOL, True, "use the 'hardware interpretation' for division by zero (for bit-vector terms)"),
                           ("mul2concat", BOOL, False, "replace multiplication by a power of two into a concatenation"),
                           ("bvnot2arith", BOOL, False, "replace (bvnot x) with (bvsub -1 x)"),
-                          ("bv_sort_ac", BOOL, False, "sort the arguments of all AC operators")
+                          ("bv_sort_ac", BOOL, False, "sort the arguments of all AC operators"),
+                          ("bv_trailing", BOOL, False, "lean removal of trailing zeros")
                           ))

src/ast/rewriter/bv_trailing.cpp

@@ -0,0 +1,282 @@
+/*++
+ Copyright (c) 2016 Microsoft Corporation
+
+ Module Name:
+
+  bv_trailing.cpp
+
+ Abstract:
+
+
+ Author:
+
+ Mikolas Janota (MikolasJanota)
+
+ Revision History:
+--*/
+#include"bv_trailing.h"
+#include"bv_decl_plugin.h"
+#include"ast_smt2_pp.h"
+
+#define  TRAILING_DEPTH 4
+
+struct bv_trailing::imp {
+    typedef rational numeral;
+    bv_util                       m_util;
+    ast_manager&         m_m;
+    mk_extract_proc&  m_mk_extract;
+    imp(ast_manager& m, mk_extract_proc& mk_extract)
+        : m_m(m)
+        , m_util(m)
+        , m_mk_extract(mk_extract)
+        { }
+
+    virtual ~imp() { }
+
+    ast_manager & m() const { return m_util.get_manager(); }
+
+
+    br_status eq_remove_trailing(expr * e1, expr * e2, expr_ref& result) {
+        TRACE("bv-trailing", tout << mk_ismt2_pp(e1, m()) << "\n=\n" << mk_ismt2_pp(e2, m()) << "\n";);
+        SASSERT(m_util.is_bv(e1) && m_util.is_bv(e2));
+        SASSERT(m_util.get_bv_size(e1) == m_util.get_bv_size(e2));
+        unsigned max1, min1, max2, min2;
+        count_trailing(e1, min1, max1, TRAILING_DEPTH);
+        count_trailing(e2, min2, max2, TRAILING_DEPTH);
+        if (min1 > max2 || min2 > max2) {
+            result = m().mk_false();
+            return BR_DONE;
+        }
+        const unsigned min = std::min(min1, min2);
+        if (min == 0) {
+            result = m().mk_eq(e1, e2);
+            return BR_FAILED;
+        }
+        const unsigned sz  = m_util.get_bv_size(e1);
+        if (min == sz) { // unlikely but we check anyhow for safety
+            result = m().mk_true();
+            return BR_DONE;
+        }
+        expr_ref out1(m());
+        expr_ref out2(m());
+        remove_trailing(e1, min, out1, TRAILING_DEPTH);
+        remove_trailing(e2, min, out2, TRAILING_DEPTH);
+        result = m().mk_eq(out1, out2);
+        return BR_REWRITE2;
+    }
+
+    unsigned remove_trailing_mul(app * a, unsigned n, expr_ref& result, unsigned depth) {
+        SASSERT(m_util.is_bv_mul(a));
+        if (depth <= 1) {
+            result = a;
+            return 0;
+        }
+        const unsigned num  = a->get_num_args();
+        if (!num) return 0;
+        expr_ref tmp(m());
+        expr * const coefficient = a->get_arg(0);
+        const unsigned retv = remove_trailing(coefficient, n, tmp, depth - 1);
+        SASSERT(retv <= n);
+        if (retv == 0) {
+            result = a;
+            return 0;
+        }
+        expr_ref_vector new_args(m());
+        numeral c_val;
+        unsigned c_sz;
+        if (!m_util.is_numeral(tmp, c_val, c_sz) || !c_val.is_one())
+            new_args.push_back(tmp);
+        const unsigned sz = m_util.get_bv_size(coefficient);
+        const unsigned new_sz = sz - retv;
+
+        if (!new_sz) {
+            result = NULL;
+            return retv;
+        }
+
+        SASSERT(m_util.get_bv_size(tmp) == new_sz);
+        for (unsigned i = 1; i < num; i++) {
+            expr * const curr = a->get_arg(i);
+            new_args.push_back(m_mk_extract(new_sz - 1, 0, curr));
+        }
+        switch (new_args.size()) {
+        case 0: result = m_util.mk_numeral(1, new_sz); break;
+        case 1: result = new_args.get(0); break;
+        default: result = m().mk_app(m_util.get_fid(), OP_BMUL, new_args.size(), new_args.c_ptr());
+        }
+        return retv;
+    }
+
+    unsigned remove_trailing_concat(app * a, unsigned n, expr_ref& result, unsigned depth) {
+        SASSERT(m_util.is_concat(a));
+        if (depth <= 1) {
+            result = a;
+            return 0;
+        }
+        unsigned num  = a->get_num_args();
+        unsigned  retv = 0;
+        unsigned i = num;
+        expr_ref new_last(NULL, m());
+        while (i && retv < n) {
+            i--;
+            expr * const curr = a->get_arg(i);
+            const unsigned cur_rm = remove_trailing(curr, n, new_last, depth - 1);
+            const unsigned curr_sz = m_util.get_bv_size(curr);
+            retv += cur_rm;
+            if (cur_rm < curr_sz) break;
+        }
+        if (retv == 0) {
+            result = a;
+            return 0;
+        }
+
+        if (!i) {
+            SASSERT(new_last.get() == NULL);
+            result = NULL;
+            return retv;
+        }
+
+        expr_ref_vector new_args(m());
+        for (size_t j=0; j<i;++j)
+            new_args.push_back(a->get_arg(j));
+        if (new_last.get()) new_args.push_back(new_last);
+        result = m_util.mk_concat(new_args.size(), new_args.c_ptr());
+        return retv;
+    }
+
+    unsigned remove_trailing(size_t max_rm, numeral& a) {
+        numeral two(2);
+        unsigned retv = 0;
+        while (max_rm && a.is_even()) {
+            div(a, two, a);
+            ++retv;
+            --max_rm;
+        }
+        return retv;
+    }
+
+    unsigned remove_trailing(expr * e, unsigned n, expr_ref& result, unsigned depth) {
+        const unsigned retv = remove_trailing_core(e, n, result, depth);
+        TRACE("bv-trailing", tout << mk_ismt2_pp(e, m()) << "\n" <<
+              "--->" << mk_ismt2_pp(result.get(), m()) << "\n";);
+        return retv;
+    }
+
+    unsigned remove_trailing_core(expr * e, unsigned n, expr_ref& result, unsigned depth) {
+        SASSERT(m_util.is_bv(e));
+        if (!depth) return 0;
+        if (n == 0) return 0;
+        unsigned sz;
+        unsigned retv = 0;
+        numeral e_val;
+        if (m_util.is_numeral(e, e_val, sz)) {
+            retv = remove_trailing(n, e_val);
+            const unsigned new_sz = sz - retv;
+            result = new_sz ? (retv ? m_util.mk_numeral(e_val, new_sz) : e) : NULL;
+            return retv;
+        }
+        if (m_util.is_bv_mul(e))
+            return remove_trailing_mul(to_app(e), n, result, depth);
+        if (m_util.is_concat(e))
+            return remove_trailing_concat(to_app(e), n, result, depth);
+        return 0;
+    }
+
+    void count_trailing(expr * e, unsigned& min, unsigned& max, unsigned depth) {
+        SASSERT(e && m_util.is_bv(e));
+        count_trailing_core(e, min, max, depth);
+        TRACE("bv-trailing", tout << mk_ismt2_pp(e, m()) << "\n:" << min << " - " << max << "\n";);
+        SASSERT(min <= max);
+        SASSERT(max <= m_util.get_bv_size(e));
+    }
+
+    void count_trailing_concat(app * a, unsigned& min, unsigned& max, unsigned depth) {
+        if (depth <= 1) {
+            min = 0;
+            max = m_util.get_bv_size(a);
+        }
+        max = min = 0; // treat empty concat as the empty string
+        unsigned num = a->get_num_args();
+        bool update_min = true;
+        bool update_max = true;
+        unsigned tmp_min, tmp_max;
+        while (num-- && update_max) {
+            expr * const curr = a->get_arg(num);
+            const unsigned curr_sz = m_util.get_bv_size(curr);
+            count_trailing(curr, tmp_min, tmp_max, depth - 1);
+            SASSERT(curr_sz != tmp_min || curr_sz == tmp_max);
+            max += tmp_max;
+            if (update_min) min += tmp_min;
+            //  continue updating only if eaten away completely
+            update_min &= curr_sz == tmp_min;
+            update_max &= curr_sz == tmp_max;
+        }
+    }
+
+    void count_trailing_mul(app * a, unsigned& min, unsigned& max, unsigned depth) {
+        if (depth <= 1) {
+            min = 0;
+            max = m_util.get_bv_size(a);
+        }
+
+        const unsigned num = a->get_num_args();
+        if (!num) {
+            max = min = 0; // treat empty multiplication as 1
+            return;
+        }
+        // assume that numerals are pushed in the front, count only for the first element
+        expr * const curr = a->get_arg(0);
+        unsigned tmp_max;
+        count_trailing(curr, min, tmp_max, depth - 1);
+        max = num == 1 ? tmp_max : m_util.get_bv_size(a);
+        return;
+    }
+
+    void count_trailing_core(expr * e, unsigned& min, unsigned& max, unsigned depth) {
+        if (!depth) {
+            min = 0;
+            max = m_util.get_bv_size(e);
+            return;
+        }
+        unsigned sz;
+        numeral e_val;
+        if (m_util.is_numeral(e, e_val, sz)) {
+            min = max = 0;
+            numeral two(2);
+            while (sz-- && e_val.is_even()) {
+                ++max;
+                ++min;
+                div(e_val, two, e_val);
+            }
+            return;
+        }
+        if (m_util.is_bv_mul(e)) count_trailing_mul(to_app(e), min, max, depth);
+        else if (m_util.is_concat(e)) count_trailing_concat(to_app(e), min, max, depth);
+        else {
+            min = 0;
+            max = m_util.get_bv_size(e);
+        }
+    }
+};
+
+bv_trailing::bv_trailing(ast_manager& m, mk_extract_proc& mk_extract) {
+    m_imp = alloc(imp, m, mk_extract);
+}
+
+bv_trailing::~bv_trailing() {
+    if (m_imp) dealloc(m_imp);
+}
+
+void bv_trailing::count_trailing(expr * e, unsigned& min, unsigned& max, unsigned depth) {
+    m_imp->count_trailing(e, min, max, depth);
+}
+
+br_status bv_trailing::eq_remove_trailing(expr * e1, expr * e2,  expr_ref& result) {
+    return m_imp->eq_remove_trailing(e1, e2, result);
+}
+
+unsigned bv_trailing::remove_trailing(expr * e, unsigned n, expr_ref& result, unsigned depth) {
+    return m_imp->remove_trailing(e, n, result, depth);
+}
+
+

src/ast/rewriter/bv_trailing.h

@@ -0,0 +1,33 @@
+ /*++
+ Copyright (c) 2016 Microsoft Corporation
+
+ Module Name:
+
+  bv_trailing.h
+
+ Abstract:
+
+
+ Author:
+
+ Mikolas Janota (MikolasJanota)
+
+ Revision History:
+ --*/
+#ifndef BV_TRAILING_H_
+#define BV_TRAILING_H_
+#include"ast.h"
+#include"bv_rewriter.h"
+#include"rewriter_types.h"
+class bv_trailing {
+    public:
+        bv_trailing(ast_manager&m, mk_extract_proc& ep);
+        virtual ~bv_trailing();
+        void count_trailing(expr * e, unsigned& min, unsigned& max, unsigned depth);
+        br_status eq_remove_trailing(expr * e1, expr * e2,  expr_ref& result);
+        unsigned remove_trailing(expr * e, unsigned n, expr_ref& result, unsigned depth);
+    protected:
+        struct imp;
+        imp *        m_imp;
+};
+#endif /* BV_TRAILING_H_ */