From 78cb1e3c7b1d9dda5173ef33b39a91098de99e42 Mon Sep 17 00:00:00 2001 From: mikolas Date: Sun, 3 Apr 2016 14:22:13 +0100 Subject: [PATCH] More work on trailing 0 analysis. --- src/ast/rewriter/bv_rewriter.cpp | 35 +------- src/ast/rewriter/bv_rewriter.h | 13 +-- src/ast/rewriter/bv_trailing.cpp | 114 ++++++++++++++++++++++----- src/ast/rewriter/bv_trailing.h | 4 +- src/ast/rewriter/mk_extract_proc.cpp | 49 ++++++++++++ src/ast/rewriter/mk_extract_proc.h | 34 ++++++++ 6 files changed, 181 insertions(+), 68 deletions(-) create mode 100644 src/ast/rewriter/mk_extract_proc.cpp create mode 100644 src/ast/rewriter/mk_extract_proc.h diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index e90768cfc..d30e082f2 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -23,39 +23,6 @@ Notes: #include"bv_trailing.h" -mk_extract_proc::mk_extract_proc(bv_util & u): - m_util(u), - m_high(0), - m_low(UINT_MAX), - m_domain(0), - m_f_cached(0) { -} - -mk_extract_proc::~mk_extract_proc() { - if (m_f_cached) { - // m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain - ast_manager & m = m_util.get_manager(); - m.dec_ref(m_f_cached); - } -} - -app * mk_extract_proc::operator()(unsigned high, unsigned low, expr * arg) { - ast_manager & m = m_util.get_manager(); - sort * s = m.get_sort(arg); - if (m_low == low && m_high == high && m_domain == s) - return m.mk_app(m_f_cached, arg); - // m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain - if (m_f_cached) - m.dec_ref(m_f_cached); - app * r = to_app(m_util.mk_extract(high, low, arg)); - m_high = high; - m_low = low; - m_domain = s; - m_f_cached = r->get_decl(); - m.inc_ref(m_f_cached); - return r; -} - void bv_rewriter::updt_local_params(params_ref const & _p) { bv_rewriter_params p(_p); m_hi_div0 = p.hi_div0(); @@ -2127,7 +2094,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { } if (m_trailing) { - bv_trailing bvt(m(), m_mk_extract); + bv_trailing bvt(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";); diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h index 64c68a8a7..e9b76768a 100644 --- a/src/ast/rewriter/bv_rewriter.h +++ b/src/ast/rewriter/bv_rewriter.h @@ -22,18 +22,7 @@ Notes: #include"poly_rewriter.h" #include"bv_decl_plugin.h" #include"arith_decl_plugin.h" - -class mk_extract_proc { - bv_util & m_util; - unsigned m_high; - unsigned m_low; - sort * m_domain; - func_decl * m_f_cached; -public: - mk_extract_proc(bv_util & u); - ~mk_extract_proc(); - app * operator()(unsigned high, unsigned low, expr * arg); -}; +#include"mk_extract_proc.h" class bv_rewriter_core { protected: diff --git a/src/ast/rewriter/bv_trailing.cpp b/src/ast/rewriter/bv_trailing.cpp index c12b7ad44..67bbacfd4 100644 --- a/src/ast/rewriter/bv_trailing.cpp +++ b/src/ast/rewriter/bv_trailing.cpp @@ -22,19 +22,22 @@ struct bv_trailing::imp { typedef rational numeral; - bv_util m_util; + typedef obj_map > map; + mk_extract_proc& m_mk_extract; + 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) + map m_count_cache; + imp(mk_extract_proc& mk_extract) + : m_mk_extract(mk_extract) + , m_util(mk_extract.bvutil()) + , m_m(mk_extract.m()) { } virtual ~imp() { } ast_manager & m() const { return m_util.get_manager(); } + void reset_cache() { m_count_cache.reset(); } 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";); @@ -65,14 +68,47 @@ struct bv_trailing::imp { return BR_REWRITE2; } - unsigned remove_trailing_mul(app * a, unsigned n, expr_ref& result, unsigned depth) { - SASSERT(m_util.is_bv_mul(a)); + unsigned remove_trailing_add(app * a, unsigned n, expr_ref& result, unsigned depth) { + SASSERT(m_util.is_bv_add(a)); + const unsigned num = a->get_num_args(); if (depth <= 1) { result = a; return 0; } + unsigned min, max; + count_trailing(a, min, max, depth); + const unsigned to_rm = std::min(min, n); + if (to_rm == 0) { + result = a; + return 0; + } + + const unsigned sz = m_util.get_bv_size(a); + + if (to_rm == sz) { + result = NULL; + return sz; + } + + expr_ref_vector new_args(m()); + expr_ref tmp(m()); + for (unsigned i = 0; i < num; ++i) { + expr * const curr = a->get_arg(i); + const unsigned crm = remove_trailing(curr, to_rm, tmp, depth - 1); + new_args.push_back(tmp); + SASSERT(crm == to_rm); + } + result = m().mk_app(m_util.get_fid(), OP_BADD, new_args.size(), new_args.c_ptr()); + return to_rm; + } + + unsigned remove_trailing_mul(app * a, unsigned n, expr_ref& result, unsigned depth) { + SASSERT(m_util.is_bv_mul(a)); const unsigned num = a->get_num_args(); - if (!num) return 0; + if (depth <= 1 || !num) { + result = a; + return 0; + } expr_ref tmp(m()); expr * const coefficient = a->get_arg(0); const unsigned retv = remove_trailing(coefficient, n, tmp, depth - 1); @@ -114,7 +150,7 @@ struct bv_trailing::imp { return 0; } unsigned num = a->get_num_args(); - unsigned retv = 0; + unsigned retv = 0; unsigned i = num; expr_ref new_last(NULL, m()); while (i && retv < n) { @@ -130,8 +166,9 @@ struct bv_trailing::imp { return 0; } - if (!i) { + if (!i) {// all args eaten completely SASSERT(new_last.get() == NULL); + SASSERT(retv == m_util.get_bv_size(a)); result = NULL; return retv; } @@ -140,7 +177,8 @@ struct bv_trailing::imp { for (size_t j=0; jget_arg(j)); if (new_last.get()) new_args.push_back(new_last); - result = m_util.mk_concat(new_args.size(), new_args.c_ptr()); + result = new_args.size() == 1 ? new_args.get(0) + : m_util.mk_concat(new_args.size(), new_args.c_ptr()); return retv; } @@ -157,8 +195,8 @@ struct bv_trailing::imp { 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";); + CTRACE("bv-trailing", result.get(), tout << mk_ismt2_pp(e, m()) << "\n--->\n" << mk_ismt2_pp(result.get(), m()) << "\n";); + CTRACE("bv-trailing", !result.get(), tout << mk_ismt2_pp(e, m()) << "\n---> [EMPTY]\n";); return retv; } @@ -177,17 +215,29 @@ struct bv_trailing::imp { } if (m_util.is_bv_mul(e)) return remove_trailing_mul(to_app(e), n, result, depth); + if (m_util.is_bv_add(e)) + return remove_trailing_add(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) { + std::pair cached; + if (m_count_cache.find(e, cached)) { // check cache first + min = cached.first; + max = cached.second; + return; + } 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)); + // store into the cache + cached.first = min; + cached.second = max; + m_count_cache.insert(e, cached); } void count_trailing_concat(app * a, unsigned& min, unsigned& max, unsigned depth) { @@ -213,6 +263,29 @@ struct bv_trailing::imp { } } + void count_trailing_add(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(); + const unsigned sz = m_util.get_bv_size(a); + min = max = sz; // treat empty addition as 0 + unsigned tmp_min; + unsigned tmp_max; + bool known_parity = true; + bool is_odd = false; + for (unsigned i = 0; i < num; ++i) { + expr * const curr = a->get_arg(i); + count_trailing(curr, tmp_min, tmp_max, depth - 1); + min = std::min(min, tmp_min); + known_parity = known_parity && (!tmp_max || tmp_min); + if (known_parity && !tmp_max) is_odd = !is_odd; + if (!known_parity && !min) break; // no more information can be gained + } + max = known_parity && is_odd ? 0 : sz; // max is known if parity is 1 + } + void count_trailing_mul(app * a, unsigned& min, unsigned& max, unsigned depth) { if (depth <= 1) { min = 0; @@ -251,6 +324,7 @@ struct bv_trailing::imp { return; } if (m_util.is_bv_mul(e)) count_trailing_mul(to_app(e), min, max, depth); + else if (m_util.is_bv_add(e)) count_trailing_add(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; @@ -259,18 +333,14 @@ struct bv_trailing::imp { } }; -bv_trailing::bv_trailing(ast_manager& m, mk_extract_proc& mk_extract) { - m_imp = alloc(imp, m, mk_extract); +bv_trailing::bv_trailing(mk_extract_proc& mk_extract) { + m_imp = alloc(imp, 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); } @@ -279,4 +349,6 @@ unsigned bv_trailing::remove_trailing(expr * e, unsigned n, expr_ref& result, un return m_imp->remove_trailing(e, n, result, depth); } - +void bv_trailing::reset_cache() { + m_imp->reset_cache(); +} diff --git a/src/ast/rewriter/bv_trailing.h b/src/ast/rewriter/bv_trailing.h index 42e531527..4ff24a5d9 100644 --- a/src/ast/rewriter/bv_trailing.h +++ b/src/ast/rewriter/bv_trailing.h @@ -19,13 +19,15 @@ #include"ast.h" #include"bv_rewriter.h" #include"rewriter_types.h" +#include"mk_extract_proc.h" class bv_trailing { public: - bv_trailing(ast_manager&m, mk_extract_proc& ep); + bv_trailing(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); + void reset_cache(); protected: struct imp; imp * m_imp; diff --git a/src/ast/rewriter/mk_extract_proc.cpp b/src/ast/rewriter/mk_extract_proc.cpp new file mode 100644 index 000000000..5f470acd3 --- /dev/null +++ b/src/ast/rewriter/mk_extract_proc.cpp @@ -0,0 +1,49 @@ +/*++ + Copyright (c) 2016 Microsoft Corporation + + Module Name: + + mk_extract_proc.cpp + + Abstract: + + + Author: + + Mikolas Janota (MikolasJanota) + + Revision History: +--*/ +#include"mk_extract_proc.h" +mk_extract_proc::mk_extract_proc(bv_util & u): + m_util(u), + m_high(0), + m_low(UINT_MAX), + m_domain(0), + m_f_cached(0) { +} + +mk_extract_proc::~mk_extract_proc() { + if (m_f_cached) { + // m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain + ast_manager & m = m_util.get_manager(); + m.dec_ref(m_f_cached); + } +} + +app * mk_extract_proc::operator()(unsigned high, unsigned low, expr * arg) { + ast_manager & m = m_util.get_manager(); + sort * s = m.get_sort(arg); + if (m_low == low && m_high == high && m_domain == s) + return m.mk_app(m_f_cached, arg); + // m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain + if (m_f_cached) + m.dec_ref(m_f_cached); + app * r = to_app(m_util.mk_extract(high, low, arg)); + m_high = high; + m_low = low; + m_domain = s; + m_f_cached = r->get_decl(); + m.inc_ref(m_f_cached); + return r; +} diff --git a/src/ast/rewriter/mk_extract_proc.h b/src/ast/rewriter/mk_extract_proc.h new file mode 100644 index 000000000..2b242d0f5 --- /dev/null +++ b/src/ast/rewriter/mk_extract_proc.h @@ -0,0 +1,34 @@ + /*++ + Copyright (c) 2016 Microsoft Corporation + + Module Name: + + mk_extract_proc.h + + Abstract: + + + Author: + + Mikolas Janota (MikolasJanota) + + Revision History: + --*/ +#ifndef MK_EXTRACT_PROC_H_ +#define MK_EXTRACT_PROC_H_ +#include"ast.h" +#include"bv_decl_plugin.h" +class mk_extract_proc { + bv_util & m_util; + unsigned m_high; + unsigned m_low; + sort * m_domain; + func_decl * m_f_cached; +public: + mk_extract_proc(bv_util & u); + ~mk_extract_proc(); + app * operator()(unsigned high, unsigned low, expr * arg); + ast_manager & m() { return m_util.get_manager(); } + bv_util & bvutil() { return m_util; } +}; +#endif /* MK_EXTRACT_PROC_H_ */