diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt index 260a00bb8..ba57f757d 100644 --- a/src/ast/rewriter/CMakeLists.txt +++ b/src/ast/rewriter/CMakeLists.txt @@ -33,7 +33,6 @@ z3_add_component(rewriter seq_rewriter.cpp th_rewriter.cpp var_subst.cpp - bv_trailing.cpp mk_extract_proc.cpp COMPONENT_DEPENDENCIES ast diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index c4960135f..881bceaa5 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -29,7 +29,6 @@ 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_urem_simpl = p.bv_urem_simpl(); m_blast_eq_value = p.blast_eq_value(); m_split_concat_eq = p.split_concat_eq(); @@ -2591,15 +2590,6 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { return st; } - if (m_trailing) { - st = m_rm_trailing.eq_remove_trailing(lhs, rhs, result); - m_rm_trailing.reset_cache(1 << 12); - 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";); diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h index 03121da5a..de42fc4d2 100644 --- a/src/ast/rewriter/bv_rewriter.h +++ b/src/ast/rewriter/bv_rewriter.h @@ -23,7 +23,6 @@ Notes: #include "ast/bv_decl_plugin.h" #include "ast/arith_decl_plugin.h" #include "ast/rewriter/mk_extract_proc.h" -#include "ast/rewriter/bv_trailing.h" class bv_rewriter_core { protected: @@ -49,7 +48,6 @@ public: class bv_rewriter : public poly_rewriter { mk_extract_proc m_mk_extract; - bv_trailing m_rm_trailing; arith_util m_autil; bool m_hi_div0; bool m_elim_sign_ext; @@ -61,7 +59,6 @@ class bv_rewriter : public poly_rewriter { bool m_split_concat_eq; bool m_bvnot2arith; bool m_bv_sort_ac; - bool m_trailing; bool m_extract_prop; bool m_bvnot_simpl; bool m_le_extra; @@ -159,7 +156,6 @@ public: bv_rewriter(ast_manager & m, params_ref const & p = params_ref()): poly_rewriter(m, p), m_mk_extract(m_util), - m_rm_trailing(m_mk_extract), m_autil(m) { updt_local_params(p); } diff --git a/src/ast/rewriter/bv_rewriter_params.pyg b/src/ast/rewriter/bv_rewriter_params.pyg index 85b1b7446..ab46d107e 100644 --- a/src/ast/rewriter/bv_rewriter_params.pyg +++ b/src/ast/rewriter/bv_rewriter_params.pyg @@ -9,7 +9,6 @@ def_module_params(module_name='rewriter', ("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_trailing", BOOL, False, "lean removal of trailing zeros"), ("bv_extract_prop", BOOL, False, "attempt to partially propagate extraction inwards"), ("bv_not_simpl", BOOL, False, "apply simplifications for bvnot"), ("bv_ite2id", BOOL, False, "rewrite ite that can be simplified to identity"), diff --git a/src/ast/rewriter/bv_trailing.cpp b/src/ast/rewriter/bv_trailing.cpp deleted file mode 100644 index 85578db39..000000000 --- a/src/ast/rewriter/bv_trailing.cpp +++ /dev/null @@ -1,495 +0,0 @@ -/*++ - Copyright (c) 2016 Microsoft Corporation - - Module Name: - - bv_trailing.cpp - - Author: - - Mikolas Janota (MikolasJanota) - - Revision History: - -NSB code review: -This code needs to be rewritten or just removed. - -The main issue is that the analysis and extraction steps are separated. -They are out of sync and therefore buggy. -A saner implementation does the trailing elimination on a pair of vectors. -The vectors are initially singltons. They are expanded when processing a concat. -The vector with the largest bit-width is reduced maximally. -If it cannot be reduced, then bits are padded to align the two vectors. - ---*/ - -#include "ast/rewriter/bv_trailing.h" -#include "ast/bv_decl_plugin.h" -#include "ast/ast_pp.h" -#include "ast/ast_ll_pp.h" - -// The analyzer gives up analysis after going TRAILING_DEPTH deep. -// This number shouldn't be too big. -#define TRAILING_DEPTH 5 - -struct bv_trailing::imp { - typedef rational numeral; - typedef obj_map > map; - mk_extract_proc& m_mk_extract; - bv_util& m_util; - ast_manager& m; - - // keep a cache for each depth, using the convention that m_count_cache[TRAILING_DEPTH] is top-level - map* m_count_cache[TRAILING_DEPTH + 1]; - - imp(mk_extract_proc& mk_extract) - : m_mk_extract(mk_extract) - , m_util(mk_extract.bvutil()) - , m(mk_extract.m()) { - TRACE("bv-trailing", tout << "ctor\n";); - - for (unsigned i = 0; i <= TRAILING_DEPTH; ++i) - m_count_cache[i] = nullptr; - } - - virtual ~imp() { - reset_cache(0); - } - - br_status eq_remove_trailing(expr * e1, expr * e2, expr_ref& result) { - TRACE("bv-trailing", tout << mk_pp(e1, m) << "\n=\n" << mk_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 > max1) { // bounds have empty intersection - result = m.mk_false(); - return BR_DONE; - } - const unsigned min = std::min(min1, min2); // remove the minimum of the two lower bounds - if (min == 0) { // nothing to remove - return BR_FAILED; - } - const unsigned sz = m_util.get_bv_size(e1); - if (min == sz) { // everything removed, unlikely but we check anyhow for safety - result = m.mk_true(); - return BR_DONE; - } - expr_ref out1(m); - expr_ref out2(m); - TRACE("bv-trailing", tout << min << "\n";); - VERIFY(min == remove_trailing(e1, min, out1, TRAILING_DEPTH)); - VERIFY(min == remove_trailing(e2, min, out2, TRAILING_DEPTH)); - if (m.get_sort(out1) != m.get_sort(out2)) { - TRACE("bv-trailing", tout << "bug\n";); - return BR_FAILED; - } - const bool are_eq = m.are_equal(out1, out2); - result = are_eq ? m.mk_true() : m.mk_eq(out1, out2); - return are_eq ? BR_DONE : BR_REWRITE2; - } - - // This routine needs to be implemented carefully so that whenever it - // returns a lower bound on trailing zeros min, the routine remove_trailing - // must be capable of removing at least that many zeros from the expression. - void count_trailing(expr * e, unsigned& min, unsigned& max, unsigned depth) { - SASSERT(e && m_util.is_bv(e)); - if (is_cached(depth, e, min, max)) return; - count_trailing_core(e, min, max, depth); - TRACE("bv-trailing", tout << mk_pp(e, m) << "\n:" << min << " - " << max << "\n";); - SASSERT(min <= max); - SASSERT(max <= m_util.get_bv_size(e)); - cache(depth, e, min, max); // store result into the cache - } - - 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_pp(e, m) << "\n--->\n" << retv << ": " << result << "\n";); - return retv; - } - - // Assumes that count_trailing gives me a lower bound that we can also remove from each summand. - unsigned remove_trailing_add(app * a, unsigned n, expr_ref& result, unsigned depth) { - SASSERT(m_util.is_bv_add(a)); - if (depth <= 1) { - result = a; - return 0; - } - unsigned min, max; - count_trailing(a, min, max, depth); // caching is important here - 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 = nullptr; - return sz; - } - - expr_ref_vector new_args(m); - expr_ref tmp(m); - for (expr * curr : *a) { - VERIFY(to_rm == remove_trailing(curr, to_rm, tmp, depth - 1)); - new_args.push_back(std::move(tmp)); - } - 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 (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); - SASSERT(retv <= n); - if (retv == 0) { - result = a; - return 0; - } - const unsigned sz = m_util.get_bv_size(coefficient); - const unsigned new_sz = sz - retv; - SASSERT(m_util.get_bv_size(tmp) == new_sz); - - 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(std::move(tmp)); - - if (new_sz == 0) { - result = nullptr; - return retv; - } - - 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; - } - const unsigned num = a->get_num_args(); - unsigned retv = 0; - unsigned i; - expr_ref new_last(nullptr, m); - for (i = num; retv < n && i-- > 0; ) { - new_last = nullptr; - expr * const curr = a->get_arg(i); - unsigned cur_rm = remove_trailing(curr, n, new_last, depth - 1); - 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 == 0 && retv != m_util.get_bv_size(a)) - new_last = a->get_arg(0); - - if (i == 0 && !new_last) { // all args eaten completely - SASSERT(retv == m_util.get_bv_size(a)); - result = nullptr; - return retv; - } - - expr_ref_vector new_args(m); - for (unsigned j = 0; j < i; ++j) - new_args.push_back(a->get_arg(j)); - if (new_last) new_args.push_back(std::move(new_last)); - result = new_args.size() == 1 ? new_args.get(0) - : 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_core(expr * e, unsigned n, expr_ref& result, unsigned depth) { - SASSERT(m_util.is_bv(e)); - if (depth == 0) { - 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(std::min(n, sz), e_val); - const unsigned new_sz = sz - retv; - result = new_sz ? (retv ? m_util.mk_numeral(e_val, new_sz) : e) : nullptr; - return retv; - } - 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_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_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; - 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_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; - max = m_util.get_bv_size(e); - } - } - - void cache(unsigned depth, expr * e, unsigned min, unsigned max) { - SASSERT(depth <= TRAILING_DEPTH); - if (depth == 0) return; - if (m_count_cache[depth] == nullptr) - m_count_cache[depth] = alloc(map); - SASSERT(!m_count_cache[depth]->contains(e)); - m.inc_ref(e); - m_count_cache[depth]->insert(e, std::make_pair(min, max)); - TRACE("bv-trailing", tout << "caching@" << depth <<": " << mk_pp(e, m) << '[' << m_util.get_bv_size(e) << "]\n: " << min << '-' << max << "\n";); - } - - bool is_cached(unsigned depth, expr * e, unsigned& min, unsigned& max) { - SASSERT(depth <= TRAILING_DEPTH); - if (depth == 0) { - min = 0; - max = m_util.get_bv_size(e); - return true; - } - if (m_count_cache[depth] == nullptr) - return false; - const map::obj_map_entry * const oe = m_count_cache[depth]->find_core(e); - if (oe == nullptr) return false; - min = oe->get_data().m_value.first; - max = oe->get_data().m_value.second; - TRACE("bv-trailing", tout << "cached@" << depth << ": " << mk_pp(e, m) << '[' << m_util.get_bv_size(e) << "]\n: " << min << '-' << max << "\n";); - return true; - } - - void reset_cache(const unsigned condition) { - SASSERT(m_count_cache[0] == nullptr); - for (unsigned i = 1; i <= TRAILING_DEPTH; ++i) { - if (m_count_cache[i] == nullptr) continue; - TRACE("bv-trailing", tout << "may reset cache " << i << " " << condition << "\n";); - if (m_count_cache[i]->size() < condition) continue; - TRACE("bv-trailing", tout << "reset cache " << i << "\n";); - for (auto& kv : *m_count_cache[i]) { - m.dec_ref(kv.m_key); - } - dealloc(m_count_cache[i]); - m_count_cache[i] = nullptr; - } - } - -}; - -bv_trailing::bv_trailing(mk_extract_proc& mk_extract) { - m_imp = alloc(imp, mk_extract); -} - -bv_trailing::~bv_trailing() { - dealloc(m_imp); -} - -br_status bv_trailing::eq_remove_trailing(expr * e1, expr * e2, expr_ref& result) { - return m_imp->eq_remove_trailing(e1, e2, result); -} - -void bv_trailing::count_trailing(expr * e, unsigned& min, unsigned& max) { - m_imp->count_trailing(e, min, max, TRAILING_DEPTH); -} - -unsigned bv_trailing::remove_trailing(expr * e, unsigned n, expr_ref& result) { - return m_imp->remove_trailing(e, n, result, TRAILING_DEPTH); -} - -void bv_trailing::reset_cache(unsigned condition) { - m_imp->reset_cache(condition); -} - -#if 0 -sketch - - - void remove_trailing(expr* e1, expr* e2, expr_ref& result) { - 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 sz1 = m_util.get_bv_size(e1); - unsigned sz2 = sz1; - expr_ref_vector ls(m), rs(m); - ls.push_back(e1); - rs.push_back(e2); - while (true) { - if (sz1 < sz2) { - std::swap(sz1, sz2); - ls.swap(rs); - } - if (sz2 == 0) { - result = m.mk_true(); - return BR_DONE; - } - if (try_remove(sz1, ls)) - continue; - if (sz1 == m_util.get_bv_size(e1)) - return BR_FAILED; - if (sz1 > sz2) { - rs.push_back(m_util.mk_numeral(0, sz1 - sz2)); - } - expr_ref l(m_util.mk_concat(ls.size(), ls.c_ptr()), m); - expr_ref r(m_util.mk_concat(rs.size(), rs.c_ptr()), m); - result = m.mk_eq(l, r); - return BR_REWRITE3; - } - } - - bool try_remove(unsigned& sz, expr_ref_vector& es) { - SASSERT(!es.empty()); - expr_ref b(es.back(), m); - if (m_util.is_concat(b)) { - es.pop_back(); - for (expr* arg : *to_app(b)) { - es.push_back(arg); - } - return true; - } - if (m_util.is_numeral(e, e_val, e_sz)) { - unsigned new_sz = remove_trailing(e_sz, a); - if (new_sz == 0) { - es.pop_back(b); - sz -= e_sz; - return true; - } - if (new_sz == e_sz) { - return false; - } - sz -= (e_sz - new_sz); - es.pop_back(b); - es.push_back(m_util.mk_numeral(a, new_sz)); - return true; - } - if (m_util.is_bv_mul(e)) { - - } - return false; - } - -#endif diff --git a/src/ast/rewriter/bv_trailing.h b/src/ast/rewriter/bv_trailing.h deleted file mode 100644 index 1b42dd9c1..000000000 --- a/src/ast/rewriter/bv_trailing.h +++ /dev/null @@ -1,48 +0,0 @@ - /*++ - Copyright (c) 2016 Microsoft Corporation - - Module Name: - - bv_trailing.h - - Abstract: - - A utility to count trailing zeros of an expression. Treats 2x and x++0 equivalently. - - - Author: - - Mikolas Janota (MikolasJanota) - - Revision History: - --*/ -#ifndef BV_TRAILING_H_ -#define BV_TRAILING_H_ -#include "ast/ast.h" -#include "ast/rewriter/rewriter_types.h" -#include "ast/rewriter/mk_extract_proc.h" -class bv_trailing { - public: - bv_trailing(mk_extract_proc& ep); - virtual ~bv_trailing(); - public: - // Remove trailing zeros from both sides of an equality (might give False). - br_status eq_remove_trailing(expr * e1, expr * e2, expr_ref& result); - - private: - // Gives a lower and upper bound on trailing zeros in e. - void count_trailing(expr * e, unsigned& min, unsigned& max); - - // Attempts removing n trailing zeros from e. Returns how many were successfully removed. - // We're assuming that it can remove at least as many zeros as min returned by count_training. - // Removing the bit-width of e, sets result to NULL. - unsigned remove_trailing(expr * e, unsigned n, expr_ref& result); - - public: - // Reset cache(s) if it exceeded size condition. - void reset_cache(unsigned condition); - protected: - struct imp; - imp * m_imp; -}; -#endif /* BV_TRAILING_H_ */