diff --git a/contrib/cmake/src/ast/rewriter/CMakeLists.txt b/contrib/cmake/src/ast/rewriter/CMakeLists.txt index 921cace75..14bcebf46 100644 --- a/contrib/cmake/src/ast/rewriter/CMakeLists.txt +++ b/contrib/cmake/src/ast/rewriter/CMakeLists.txt @@ -20,6 +20,8 @@ z3_add_component(rewriter seq_rewriter.cpp th_rewriter.cpp var_subst.cpp + bv_trailing.cpp + mk_extract_proc.cpp COMPONENT_DEPENDENCIES ast automata diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 7322977a0..def05f014 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -22,45 +22,13 @@ Notes: #include"ast_smt2_pp.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(); 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 +2092,15 @@ 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";); @@ -2187,6 +2164,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; diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h index f01743ca9..7135c52ba 100644 --- a/src/ast/rewriter/bv_rewriter.h +++ b/src/ast/rewriter/bv_rewriter.h @@ -22,18 +22,8 @@ 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" +#include"bv_trailing.h" class bv_rewriter_core { protected: @@ -58,6 +48,7 @@ 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; @@ -69,6 +60,7 @@ class bv_rewriter : public poly_rewriter { bool m_udiv2mul; bool m_bvnot2arith; bool m_bv_sort_ac; + bool m_trailing; bool is_zero_bit(expr * x, unsigned idx); @@ -148,6 +140,7 @@ 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 5feece753..0f0163fb1 100644 --- a/src/ast/rewriter/bv_rewriter_params.pyg +++ b/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") )) diff --git a/src/ast/rewriter/bv_trailing.cpp b/src/ast/rewriter/bv_trailing.cpp new file mode 100644 index 000000000..9a5c0107d --- /dev/null +++ b/src/ast/rewriter/bv_trailing.cpp @@ -0,0 +1,404 @@ +/*++ + 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" + +// 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_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_m(mk_extract.m()) { + for (unsigned i = 0; i <= TRAILING_DEPTH; ++i) + m_count_cache[i] = NULL; + } + + virtual ~imp() { + reset_cache(0); + } + + 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 > 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 + result = m().mk_eq(e1, e2); + 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()); + const unsigned rm1 = remove_trailing(e1, min, out1, TRAILING_DEPTH); + const unsigned rm2 = remove_trailing(e2, min, out2, TRAILING_DEPTH); + SASSERT(rm1 == min && rm2 == min); + 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_ismt2_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); + 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; + } + + // 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)); + const unsigned num = a->get_num_args(); + 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 = 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 (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; + } + 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; + } + const 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) {// all args eaten completely + SASSERT(new_last.get() == NULL); + SASSERT(retv == m_util.get_bv_size(a)); + result = NULL; + return retv; + } + + expr_ref_vector new_args(m()); + for (size_t j=0; jget_arg(j)); + if (new_last.get()) new_args.push_back(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 || !n) 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_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] == NULL) + m_count_cache[depth] = alloc(map); + m().inc_ref(e); + m_count_cache[depth]->insert(e, std::make_pair(min, max)); + TRACE("bv-trailing", tout << "caching@" << depth <<": " << mk_ismt2_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] == NULL) + return false; + const map::obj_map_entry * const oe = m_count_cache[depth]->find_core(e); + if (oe == NULL) return false; + min = oe->get_data().m_value.first; + max = oe->get_data().m_value.second; + TRACE("bv-trailing", tout << "cached@" << depth << ": " << mk_ismt2_pp(e, m()) << '[' << m_util.get_bv_size(e) << "]\n: " << min << '-' << max << "\n";); + return true; + } + + void reset_cache(unsigned condition) { + SASSERT(m_count_cache[0] == NULL); + for (unsigned i = 1; i <= TRAILING_DEPTH; ++i) { + if (m_count_cache[i] == NULL) continue; + if (m_count_cache[i]->size() < condition) continue; + map::iterator it = m_count_cache[i]->begin(); + map::iterator end = m_count_cache[i]->end(); + for (; it != end; ++it) m().dec_ref(it->m_key); + dealloc(m_count_cache[i]); + m_count_cache[i] = NULL; + } + } + +}; + +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); +} + +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); +} diff --git a/src/ast/rewriter/bv_trailing.h b/src/ast/rewriter/bv_trailing.h new file mode 100644 index 000000000..862a1bea6 --- /dev/null +++ b/src/ast/rewriter/bv_trailing.h @@ -0,0 +1,46 @@ + /*++ + 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.h" +#include"rewriter_types.h" +#include"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); + + // 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); + + // Reset cache(s) if it exceeded size condition. + void reset_cache(unsigned condition); + protected: + struct imp; + imp * m_imp; +}; +#endif /* BV_TRAILING_H_ */ 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_ */