From 3b82604590078d570bbfe03550eb839dbfc3d245 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 1 Apr 2016 15:37:40 +0100 Subject: [PATCH 01/17] whitespace --- src/model/func_interp.h | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/model/func_interp.h b/src/model/func_interp.h index b264f4f1d..7ad2fefd8 100644 --- a/src/model/func_interp.h +++ b/src/model/func_interp.h @@ -12,7 +12,7 @@ Abstract: modulo a model. Main goal: Remove some code duplication and make the evaluator more efficient. - + Example of code duplication that existed in Z3: - smt_model_generator was creating func_values that were essentially partial func_interps - smt_model_generator was creating if-then-else (lambda) exprs representing func_values @@ -39,17 +39,17 @@ class func_entry { bool m_args_are_values; //!< true if is_value(m_args[i]) is true for all i in [0, arity) // m_result and m_args[i] must be ground terms. - + expr * m_result; expr * m_args[]; static unsigned get_obj_size(unsigned arity) { return sizeof(func_entry) + arity * sizeof(expr*); } func_entry(ast_manager & m, unsigned arity, expr * const * args, expr * result); - + friend class func_interp; - + void set_result(ast_manager & m, expr * r); - + public: static func_entry * mk(ast_manager & m, unsigned arity, expr * const * args, expr * result); bool args_are_values() const { return m_args_are_values; } @@ -69,7 +69,7 @@ class func_interp { ptr_vector m_entries; expr * m_else; bool m_args_are_values; //!< true if forall e in m_entries e.args_are_values() == true - + expr * m_interp; //!< cache for representing the whole interpretation as a single expression (it uses ite terms). void reset_interp_cache(); @@ -83,7 +83,7 @@ public: ast_manager & m () const { return m_manager; } func_interp * copy() const; - + unsigned get_arity() const { return m_arity; } bool is_partial() const { return m_else == 0; } @@ -95,7 +95,7 @@ public: expr * get_else() const { return m_else; } void set_else(expr * e); - + void insert_entry(expr * const * args, expr * r); void insert_new_entry(expr * const * args, expr * r); func_entry * get_entry(expr * const * args) const; From ccd18283e7d3b5b26fe21bdbc4cacc958d5894f9 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 1 Apr 2016 15:38:38 +0100 Subject: [PATCH 02/17] Moved extension_converter func_interp entry compression to func_interp. Relates to #547 --- src/model/func_interp.cpp | 55 +++++++++++++++++++++--- src/model/func_interp.h | 3 ++ src/tactic/extension_model_converter.cpp | 44 +------------------ src/tactic/extension_model_converter.h | 3 -- 4 files changed, 53 insertions(+), 52 deletions(-) diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp index 90810f294..45bcd7780 100644 --- a/src/model/func_interp.cpp +++ b/src/model/func_interp.cpp @@ -104,11 +104,54 @@ void func_interp::reset_interp_cache() { m_manager.dec_ref(m_interp); m_interp = 0; } - + +bool func_interp::is_fi_entry_expr(expr * e, ptr_vector & args) { + args.reset(); + if (!is_app(e) || !m().is_ite(to_app(e))) + return false; + + app * a = to_app(e); + expr * c = a->get_arg(0); + expr * t = a->get_arg(1); + expr * f = a->get_arg(2); + + if ((m_arity == 0) || + (m_arity == 1 && (!m().is_eq(c) || to_app(c)->get_num_args() != 2)) || + (m_arity > 1 && (!m().is_and(c) || to_app(c)->get_num_args() != m_arity))) + return false; + + args.resize(m_arity, 0); + for (unsigned i = 0; i < m_arity; i++) { + expr * ci = (m_arity == 1 && i == 0) ? to_app(c) : to_app(c)->get_arg(i); + + if (!m().is_eq(ci) || to_app(ci)->get_num_args() != 2) + return false; + + expr * a0 = to_app(ci)->get_arg(0); + expr * a1 = to_app(ci)->get_arg(1); + if (is_var(a0) && to_var(a0)->get_idx() == i) + args[i] = a1; + else if (is_var(a1) && to_var(a1)->get_idx() == i) + args[i] = a0; + else + return false; + } + + return true; +} + void func_interp::set_else(expr * e) { reset_interp_cache(); - m_manager.inc_ref(e); m_manager.dec_ref(m_else); + + ptr_vector args; + while (is_fi_entry_expr(e, args)) { + TRACE("func_interp", tout << "fi entry expr: " << mk_ismt2_pp(e, m()) << std::endl;); + insert_entry(args.c_ptr(), to_app(e)->get_arg(1)); + e = to_app(e)->get_arg(2); + } + + m_manager.inc_ref(e); m_else = e; } @@ -148,7 +191,7 @@ func_entry * func_interp::get_entry(expr * const * args) const { void func_interp::insert_entry(expr * const * args, expr * r) { reset_interp_cache(); - func_entry * entry = get_entry(args); + func_entry * entry = get_entry(args); if (entry != 0) { entry->set_result(m_manager, r); return; @@ -201,7 +244,7 @@ expr * func_interp::get_max_occ_result() const { for (; it != end; ++it) { func_entry * curr = *it; expr * r = curr->get_result(); - unsigned occs = 0; + unsigned occs = 0; num_occs.find(r, occs); occs++; num_occs.insert(r, occs); @@ -283,13 +326,13 @@ expr * func_interp::get_interp() const { return r; } -func_interp * func_interp::translate(ast_translation & translator) const { +func_interp * func_interp::translate(ast_translation & translator) const { func_interp * new_fi = alloc(func_interp, translator.to(), m_arity); ptr_vector::const_iterator it = m_entries.begin(); ptr_vector::const_iterator end = m_entries.end(); for (; it != end; ++it) { - func_entry * curr = *it; + func_entry * curr = *it; ptr_buffer new_args; for (unsigned i=0; iget_arg(i))); diff --git a/src/model/func_interp.h b/src/model/func_interp.h index 7ad2fefd8..d0d61546e 100644 --- a/src/model/func_interp.h +++ b/src/model/func_interp.h @@ -110,6 +110,9 @@ public: expr * get_interp() const; func_interp * translate(ast_translation & translator) const; + +private: + bool is_fi_entry_expr(expr * e, ptr_vector & args); }; #endif diff --git a/src/tactic/extension_model_converter.cpp b/src/tactic/extension_model_converter.cpp index ebd530a58..cdd096455 100644 --- a/src/tactic/extension_model_converter.cpp +++ b/src/tactic/extension_model_converter.cpp @@ -43,41 +43,6 @@ static void display_decls_info(std::ostream & out, model_ref & md) { } } -bool extension_model_converter::is_fi_entry_expr(expr * e, unsigned arity, ptr_vector & args) { - args.reset(); - if (!is_app(e) || !m().is_ite(to_app(e))) - return false; - - app * a = to_app(e); - expr * c = a->get_arg(0); - expr * t = a->get_arg(1); - expr * f = a->get_arg(2); - - if ((arity == 0) || - (arity == 1 && (!m().is_eq(c) || to_app(c)->get_num_args() != 2)) || - (arity > 1 && (!m().is_and(c) || to_app(c)->get_num_args() != arity))) - return false; - - args.resize(arity, 0); - for (unsigned i = 0; i < arity; i++) { - expr * ci = (arity == 1 && i == 0) ? to_app(c) : to_app(c)->get_arg(i); - - if (!m().is_eq(ci) || to_app(ci)->get_num_args() != 2) - return false; - - expr * a0 = to_app(ci)->get_arg(0); - expr * a1 = to_app(ci)->get_arg(1); - if (is_var(a0) && to_var(a0)->get_idx() == i) - args[i] = a1; - else if (is_var(a1) && to_var(a1)->get_idx() == i) - args[i] = a0; - else - return false; - } - - return true; -} - void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) { SASSERT(goal_idx == 0); TRACE("extension_mc", model_v2_pp(tout, *md); display_decls_info(tout, md);); @@ -97,14 +62,7 @@ void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) { } else { func_interp * new_fi = alloc(func_interp, m(), arity); - expr * e = val.get(); - ptr_vector args; - while (is_fi_entry_expr(e, arity, args)) { - TRACE("extension_mc", tout << "fi entry: " << mk_ismt2_pp(e, m()) << std::endl;); - new_fi->insert_entry(args.c_ptr(), to_app(e)->get_arg(1)); - e = to_app(e)->get_arg(2); - } - new_fi->set_else(e); + new_fi->set_else(val); md->register_decl(f, new_fi); } } diff --git a/src/tactic/extension_model_converter.h b/src/tactic/extension_model_converter.h index 9431906f3..46644eec2 100644 --- a/src/tactic/extension_model_converter.h +++ b/src/tactic/extension_model_converter.h @@ -43,9 +43,6 @@ public: void insert(func_decl * v, expr * def); virtual model_converter * translate(ast_translation & translator); - -private: - bool is_fi_entry_expr(expr * e, unsigned arity, ptr_vector & args); }; From c7f17463214aaa711f7dccc81b0db80852c01471 Mon Sep 17 00:00:00 2001 From: mikolas Date: Sat, 2 Apr 2016 20:33:42 +0100 Subject: [PATCH 03/17] Starting to work on trailing 0 analysis. --- src/ast/rewriter/bv_rewriter.cpp | 12 + src/ast/rewriter/bv_rewriter.h | 1 + src/ast/rewriter/bv_rewriter_params.pyg | 3 +- src/ast/rewriter/bv_trailing.cpp | 282 ++++++++++++++++++++++++ src/ast/rewriter/bv_trailing.h | 33 +++ 5 files changed, 330 insertions(+), 1 deletion(-) create mode 100644 src/ast/rewriter/bv_trailing.cpp create mode 100644 src/ast/rewriter/bv_trailing.h diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 7322977a0..e90768cfc 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/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; diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h index f01743ca9..64c68a8a7 100644 --- a/src/ast/rewriter/bv_rewriter.h +++ b/src/ast/rewriter/bv_rewriter.h @@ -69,6 +69,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); 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..c12b7ad44 --- /dev/null +++ b/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; 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()); + 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); +} + + diff --git a/src/ast/rewriter/bv_trailing.h b/src/ast/rewriter/bv_trailing.h new file mode 100644 index 000000000..42e531527 --- /dev/null +++ b/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_ */ From 78cb1e3c7b1d9dda5173ef33b39a91098de99e42 Mon Sep 17 00:00:00 2001 From: mikolas Date: Sun, 3 Apr 2016 14:22:13 +0100 Subject: [PATCH 04/17] 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_ */ From ddb6ae4eab44b8f2fab6c5b9184e8d13a7c7b880 Mon Sep 17 00:00:00 2001 From: mikolas Date: Sun, 3 Apr 2016 18:27:56 +0100 Subject: [PATCH 05/17] More work on trailing 0 analysis. --- src/ast/rewriter/bv_trailing.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/bv_trailing.cpp b/src/ast/rewriter/bv_trailing.cpp index 67bbacfd4..eccd2e8cb 100644 --- a/src/ast/rewriter/bv_trailing.cpp +++ b/src/ast/rewriter/bv_trailing.cpp @@ -46,7 +46,7 @@ struct bv_trailing::imp { unsigned max1, min1, max2, min2; count_trailing(e1, min1, max1, TRAILING_DEPTH); count_trailing(e2, min2, max2, TRAILING_DEPTH); - if (min1 > max2 || min2 > max2) { + if (min1 > max2 || min2 > max1) { result = m().mk_false(); return BR_DONE; } From fced47386e405b26ce6c72b592c85b9710e6a76e Mon Sep 17 00:00:00 2001 From: mikolas Date: Mon, 4 Apr 2016 11:31:23 +0100 Subject: [PATCH 06/17] More work on trailing 0 analysis. --- src/ast/rewriter/bv_rewriter.cpp | 4 +--- src/ast/rewriter/bv_rewriter.h | 3 +++ src/ast/rewriter/bv_trailing.h | 1 - 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index d30e082f2..19b4bd122 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -20,7 +20,6 @@ Notes: #include"bv_rewriter_params.hpp" #include"poly_rewriter_def.h" #include"ast_smt2_pp.h" -#include"bv_trailing.h" void bv_rewriter::updt_local_params(params_ref const & _p) { @@ -2094,8 +2093,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { } if (m_trailing) { - bv_trailing bvt(m_mk_extract); - st = bvt.eq_remove_trailing(lhs, rhs, result); + st = m_rm_trailing.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; diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h index e9b76768a..7135c52ba 100644 --- a/src/ast/rewriter/bv_rewriter.h +++ b/src/ast/rewriter/bv_rewriter.h @@ -23,6 +23,7 @@ Notes: #include"bv_decl_plugin.h" #include"arith_decl_plugin.h" #include"mk_extract_proc.h" +#include"bv_trailing.h" class bv_rewriter_core { protected: @@ -47,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; @@ -138,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_trailing.h b/src/ast/rewriter/bv_trailing.h index 4ff24a5d9..0af909e8f 100644 --- a/src/ast/rewriter/bv_trailing.h +++ b/src/ast/rewriter/bv_trailing.h @@ -17,7 +17,6 @@ #ifndef BV_TRAILING_H_ #define BV_TRAILING_H_ #include"ast.h" -#include"bv_rewriter.h" #include"rewriter_types.h" #include"mk_extract_proc.h" class bv_trailing { From 248feace34b6679f2803d23bc3c3ac949807be7b Mon Sep 17 00:00:00 2001 From: Mikolas Janota Date: Mon, 4 Apr 2016 17:00:35 +0100 Subject: [PATCH 07/17] fixing the behavior in bv_trailing --- src/ast/rewriter/bv_rewriter.cpp | 1 + src/ast/rewriter/bv_trailing.cpp | 45 +++++++++++++++++++++++--------- 2 files changed, 34 insertions(+), 12 deletions(-) diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 19b4bd122..f77bce5c2 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -2094,6 +2094,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { if (m_trailing) { st = m_rm_trailing.eq_remove_trailing(lhs, rhs, result); + //m_rm_trailing.reset_cache(); 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; diff --git a/src/ast/rewriter/bv_trailing.cpp b/src/ast/rewriter/bv_trailing.cpp index eccd2e8cb..ef6a1e577 100644 --- a/src/ast/rewriter/bv_trailing.cpp +++ b/src/ast/rewriter/bv_trailing.cpp @@ -26,18 +26,46 @@ struct bv_trailing::imp { mk_extract_proc& m_mk_extract; bv_util& m_util; ast_manager& m_m; - map m_count_cache; + 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()) { } - virtual ~imp() { } + virtual ~imp() { + reset_cache(); + } ast_manager & m() const { return m_util.get_manager(); } - void reset_cache() { m_count_cache.reset(); } + void cache(unsigned depth, expr * e, unsigned min, unsigned max) { + SASSERT(depth <= TRAILING_DEPTH); + 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); + 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() { + for (unsigned i = 0; i <= TRAILING_DEPTH; ++i) { + 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); + m_count_cache[i].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";); @@ -223,21 +251,14 @@ struct bv_trailing::imp { } 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; + if (is_cached(depth, e, min, max)) 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); + cache(depth, e, min, max); // store result into the cache } void count_trailing_concat(app * a, unsigned& min, unsigned& max, unsigned depth) { From 9ba5bbfd33eadf7246124967ef6974c48ef650c3 Mon Sep 17 00:00:00 2001 From: mikolas Date: Mon, 4 Apr 2016 20:17:48 +0100 Subject: [PATCH 08/17] Re-factoring and comments in bv_trailing. --- src/ast/rewriter/bv_rewriter.cpp | 2 +- src/ast/rewriter/bv_trailing.cpp | 132 +++++++++++++++++-------------- src/ast/rewriter/bv_trailing.h | 18 ++++- 3 files changed, 89 insertions(+), 63 deletions(-) diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index f77bce5c2..def05f014 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -2094,7 +2094,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { if (m_trailing) { st = m_rm_trailing.eq_remove_trailing(lhs, rhs, result); - //m_rm_trailing.reset_cache(); + 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; diff --git a/src/ast/rewriter/bv_trailing.cpp b/src/ast/rewriter/bv_trailing.cpp index ef6a1e577..ed2a17a73 100644 --- a/src/ast/rewriter/bv_trailing.cpp +++ b/src/ast/rewriter/bv_trailing.cpp @@ -18,6 +18,8 @@ #include"bv_decl_plugin.h" #include"ast_smt2_pp.h" +// This is not very elegant at this point, this number shouldn't be too big, +// give up analysis after TRAILING_DEPTH depth. #define TRAILING_DEPTH 4 struct bv_trailing::imp { @@ -35,38 +37,11 @@ struct bv_trailing::imp { { } virtual ~imp() { - reset_cache(); + reset_cache(0); } ast_manager & m() const { return m_util.get_manager(); } - void cache(unsigned depth, expr * e, unsigned min, unsigned max) { - SASSERT(depth <= TRAILING_DEPTH); - 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); - 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() { - for (unsigned i = 0; i <= TRAILING_DEPTH; ++i) { - 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); - m_count_cache[i].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";); SASSERT(m_util.is_bv(e1) && m_util.is_bv(e2)); @@ -74,28 +49,51 @@ struct bv_trailing::imp { unsigned max1, min1, max2, min2; count_trailing(e1, min1, max1, TRAILING_DEPTH); count_trailing(e2, min2, max2, TRAILING_DEPTH); - if (min1 > max2 || min2 > max1) { + if (min1 > max2 || min2 > max1) { // bounds have empty intersection result = m().mk_false(); return BR_DONE; } - const unsigned min = std::min(min1, min2); - if (min == 0) { + 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) { // unlikely but we check anyhow for safety + 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()); - remove_trailing(e1, min, out1, TRAILING_DEPTH); - remove_trailing(e2, min, out2, TRAILING_DEPTH); - result = m().mk_eq(out1, out2); - return BR_REWRITE2; + 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, which 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(); @@ -104,7 +102,7 @@ struct bv_trailing::imp { return 0; } unsigned min, max; - count_trailing(a, min, max, depth); + count_trailing(a, min, max, depth); // caching is important here const unsigned to_rm = std::min(min, n); if (to_rm == 0) { result = a; @@ -177,7 +175,7 @@ struct bv_trailing::imp { result = a; return 0; } - unsigned num = a->get_num_args(); + const unsigned num = a->get_num_args(); unsigned retv = 0; unsigned i = num; expr_ref new_last(NULL, m()); @@ -221,13 +219,6 @@ struct bv_trailing::imp { return retv; } - 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; - } - unsigned remove_trailing_core(expr * e, unsigned n, expr_ref& result, unsigned depth) { SASSERT(m_util.is_bv(e)); if (!depth) return 0; @@ -250,16 +241,6 @@ struct bv_trailing::imp { return 0; } - void count_trailing(expr * e, unsigned& min, unsigned& max, unsigned depth) { - if (is_cached(depth, e, min, max)) - 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)); - cache(depth, e, min, max); // store result into the cache - } void count_trailing_concat(app * a, unsigned& min, unsigned& max, unsigned depth) { if (depth <= 1) { @@ -352,6 +333,35 @@ struct bv_trailing::imp { max = m_util.get_bv_size(e); } } + + void cache(unsigned depth, expr * e, unsigned min, unsigned max) { + SASSERT(depth <= TRAILING_DEPTH); + 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); + 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) { + for (unsigned i = 0; i <= TRAILING_DEPTH; ++i) { + 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); + m_count_cache[i].reset(); + } + } + }; bv_trailing::bv_trailing(mk_extract_proc& mk_extract) { @@ -366,10 +376,14 @@ br_status bv_trailing::eq_remove_trailing(expr * e1, expr * e2, expr_ref& resul 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); +void bv_trailing::count_trailing(expr * e, unsigned& min, unsigned& max) { + m_imp->count_trailing(e, min, max, TRAILING_DEPTH); } -void bv_trailing::reset_cache() { - m_imp->reset_cache(); +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 index 0af909e8f..862a1bea6 100644 --- a/src/ast/rewriter/bv_trailing.h +++ b/src/ast/rewriter/bv_trailing.h @@ -7,6 +7,8 @@ Abstract: + A utility to count trailing zeros of an expression. Treats 2x and x++0 equivalently. + Author: @@ -23,10 +25,20 @@ class bv_trailing { public: bv_trailing(mk_extract_proc& ep); virtual ~bv_trailing(); - void count_trailing(expr * e, unsigned& min, unsigned& max, unsigned depth); + 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); - unsigned remove_trailing(expr * e, unsigned n, expr_ref& result, unsigned depth); - void reset_cache(); + + // 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; From dbffc15b986c2f2b14d406c4e109e77e9e624ae9 Mon Sep 17 00:00:00 2001 From: Mikolas Janota Date: Tue, 5 Apr 2016 18:43:59 +0100 Subject: [PATCH 09/17] Improvements in caching of bv_trailing. --- src/ast/rewriter/bv_trailing.cpp | 49 +++++++++++++++++++++----------- 1 file changed, 32 insertions(+), 17 deletions(-) diff --git a/src/ast/rewriter/bv_trailing.cpp b/src/ast/rewriter/bv_trailing.cpp index ed2a17a73..9a5c0107d 100644 --- a/src/ast/rewriter/bv_trailing.cpp +++ b/src/ast/rewriter/bv_trailing.cpp @@ -18,9 +18,9 @@ #include"bv_decl_plugin.h" #include"ast_smt2_pp.h" -// This is not very elegant at this point, this number shouldn't be too big, -// give up analysis after TRAILING_DEPTH depth. -#define TRAILING_DEPTH 4 +// 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; @@ -28,13 +28,17 @@ struct bv_trailing::imp { mk_extract_proc& m_mk_extract; bv_util& m_util; ast_manager& m_m; - map m_count_cache[TRAILING_DEPTH + 1]; + + // 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()) - { } + , m_m(mk_extract.m()) { + for (unsigned i = 0; i <= TRAILING_DEPTH; ++i) + m_count_cache[i] = NULL; + } virtual ~imp() { reset_cache(0); @@ -93,7 +97,7 @@ struct bv_trailing::imp { return retv; } - // assumes that count_trailing gives me a lower bound, which we can also remove from each summand + // 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(); @@ -221,8 +225,7 @@ struct bv_trailing::imp { 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; + if (!depth || !n) return 0; unsigned sz; unsigned retv = 0; numeral e_val; @@ -336,14 +339,24 @@ struct bv_trailing::imp { 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)); + 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); - const map::obj_map_entry * const oe = m_count_cache[depth].find_core(e); + 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; @@ -351,14 +364,16 @@ struct bv_trailing::imp { return true; } - void reset_cache(unsigned condition) { - for (unsigned i = 0; i <= TRAILING_DEPTH; ++i) { - if (m_count_cache[i].size() < condition) continue; - map::iterator it = m_count_cache[i].begin(); - map::iterator end = m_count_cache[i].end(); + 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); - m_count_cache[i].reset(); + dealloc(m_count_cache[i]); + m_count_cache[i] = NULL; } } From 7ad9dec6c2f52109898c64b37dc9dd1a1027349e Mon Sep 17 00:00:00 2001 From: Mikolas Janota Date: Wed, 6 Apr 2016 11:03:21 +0100 Subject: [PATCH 10/17] Adding cpp files for bv_trailing to CMakeLists. --- contrib/cmake/src/ast/rewriter/CMakeLists.txt | 2 ++ 1 file changed, 2 insertions(+) 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 From e2b7ad246afdd79cf6f55f9ada0ce4e59d81e73f Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 6 Apr 2016 15:34:31 +0100 Subject: [PATCH 11/17] bv_trailing: fix compiler warning + use of ast_manager --- src/ast/rewriter/bv_trailing.cpp | 56 +++++++++++++++----------------- 1 file changed, 27 insertions(+), 29 deletions(-) diff --git a/src/ast/rewriter/bv_trailing.cpp b/src/ast/rewriter/bv_trailing.cpp index 9a5c0107d..d3087e776 100644 --- a/src/ast/rewriter/bv_trailing.cpp +++ b/src/ast/rewriter/bv_trailing.cpp @@ -27,7 +27,7 @@ struct bv_trailing::imp { typedef obj_map > map; mk_extract_proc& m_mk_extract; bv_util& m_util; - ast_manager& m_m; + 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]; @@ -35,7 +35,7 @@ struct bv_trailing::imp { imp(mk_extract_proc& mk_extract) : m_mk_extract(mk_extract) , m_util(mk_extract.bvutil()) - , m_m(mk_extract.m()) { + , m(mk_extract.m()) { for (unsigned i = 0; i <= TRAILING_DEPTH; ++i) m_count_cache[i] = NULL; } @@ -44,36 +44,34 @@ struct bv_trailing::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";); + 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(); + 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); + 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(); + result = m.mk_true(); return BR_DONE; } - expr_ref out1(m()); - expr_ref out2(m()); + 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); + 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; } @@ -84,7 +82,7 @@ struct bv_trailing::imp { 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";); + 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 @@ -92,8 +90,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); - 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";); + 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; } @@ -120,15 +118,15 @@ struct bv_trailing::imp { return sz; } - expr_ref_vector new_args(m()); - expr_ref tmp(m()); + 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()); + result = m.mk_app(m_util.get_fid(), OP_BADD, new_args.size(), new_args.c_ptr()); return to_rm; } @@ -139,7 +137,7 @@ struct bv_trailing::imp { result = a; return 0; } - expr_ref tmp(m()); + expr_ref tmp(m); expr * const coefficient = a->get_arg(0); const unsigned retv = remove_trailing(coefficient, n, tmp, depth - 1); SASSERT(retv <= n); @@ -147,7 +145,7 @@ struct bv_trailing::imp { result = a; return 0; } - expr_ref_vector new_args(m()); + 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()) @@ -168,7 +166,7 @@ struct bv_trailing::imp { 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()); + default: result = m.mk_app(m_util.get_fid(), OP_BMUL, new_args.size(), new_args.c_ptr()); } return retv; } @@ -182,7 +180,7 @@ struct bv_trailing::imp { const unsigned num = a->get_num_args(); unsigned retv = 0; unsigned i = num; - expr_ref new_last(NULL, m()); + expr_ref new_last(NULL, m); while (i && retv < n) { i--; expr * const curr = a->get_arg(i); @@ -203,8 +201,8 @@ struct bv_trailing::imp { 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) @@ -342,9 +340,9 @@ struct bv_trailing::imp { if (depth == 0) return; if (m_count_cache[depth] == NULL) m_count_cache[depth] = alloc(map); - m().inc_ref(e); + 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";); + 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) { @@ -360,7 +358,7 @@ struct bv_trailing::imp { 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";); + TRACE("bv-trailing", tout << "cached@" << depth << ": " << mk_ismt2_pp(e, m) << '[' << m_util.get_bv_size(e) << "]\n: " << min << '-' << max << "\n";); return true; } @@ -371,7 +369,7 @@ struct bv_trailing::imp { 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); + for (; it != end; ++it) m.dec_ref(it->m_key); dealloc(m_count_cache[i]); m_count_cache[i] = NULL; } @@ -384,7 +382,7 @@ bv_trailing::bv_trailing(mk_extract_proc& mk_extract) { } bv_trailing::~bv_trailing() { - if (m_imp) dealloc(m_imp); + dealloc(m_imp); } br_status bv_trailing::eq_remove_trailing(expr * e1, expr * e2, expr_ref& result) { From e527aca29619d241a869c142bf75729ef466a2b0 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 6 Apr 2016 15:39:32 +0100 Subject: [PATCH 12/17] Bugfix for unspecified else-case in func_interps. --- src/model/func_interp.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp index 45bcd7780..7103c495d 100644 --- a/src/model/func_interp.cpp +++ b/src/model/func_interp.cpp @@ -145,7 +145,7 @@ void func_interp::set_else(expr * e) { m_manager.dec_ref(m_else); ptr_vector args; - while (is_fi_entry_expr(e, args)) { + while (e && is_fi_entry_expr(e, args)) { TRACE("func_interp", tout << "fi entry expr: " << mk_ismt2_pp(e, m()) << std::endl;); insert_entry(args.c_ptr(), to_app(e)->get_arg(1)); e = to_app(e)->get_arg(2); From 3a532c08a680beb1e5c8ba48a489cb87817a9d70 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 6 Apr 2016 19:24:08 +0100 Subject: [PATCH 13/17] Bugfix for func_interp else-case compression --- src/model/func_interp.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp index 7103c495d..5c53e64ba 100644 --- a/src/model/func_interp.cpp +++ b/src/model/func_interp.cpp @@ -141,8 +141,10 @@ bool func_interp::is_fi_entry_expr(expr * e, ptr_vector & args) { } void func_interp::set_else(expr * e) { + if (e == m_else) + return; + reset_interp_cache(); - m_manager.dec_ref(m_else); ptr_vector args; while (e && is_fi_entry_expr(e, args)) { @@ -152,6 +154,7 @@ void func_interp::set_else(expr * e) { } m_manager.inc_ref(e); + m_manager.dec_ref(m_else); m_else = e; } From 5971c2065351888af7d9468195ce6eb8c1f606ae Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 7 Apr 2016 13:08:17 +0100 Subject: [PATCH 14/17] Bugfixes for bv_trailing. --- src/ast/rewriter/bv_trailing.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/bv_trailing.cpp b/src/ast/rewriter/bv_trailing.cpp index d3087e776..414854f3a 100644 --- a/src/ast/rewriter/bv_trailing.cpp +++ b/src/ast/rewriter/bv_trailing.cpp @@ -194,8 +194,7 @@ struct bv_trailing::imp { return 0; } - if (!i) {// all args eaten completely - SASSERT(new_last.get() == NULL); + if (!i && !new_last) {// all args eaten completely SASSERT(retv == m_util.get_bv_size(a)); result = NULL; return retv; @@ -204,7 +203,7 @@ struct bv_trailing::imp { expr_ref_vector new_args(m); for (unsigned j = 0; j < i; ++j) new_args.push_back(a->get_arg(j)); - if (new_last.get()) new_args.push_back(new_last); + if (new_last) 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; @@ -228,7 +227,7 @@ struct bv_trailing::imp { unsigned retv = 0; numeral e_val; if (m_util.is_numeral(e, e_val, sz)) { - retv = remove_trailing(n, e_val); + 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) : NULL; return retv; From 0597b579b1e043d0f9b0115cbb1f62e2763502bb Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 7 Apr 2016 19:10:31 +0100 Subject: [PATCH 15/17] Bugfixes for bvarray2uf conversion. --- src/tactic/bv/bvarray2uf_rewriter.cpp | 42 ++++++++++++++++----------- src/tactic/bv/bvarray2uf_tactic.cpp | 12 ++++---- 2 files changed, 30 insertions(+), 24 deletions(-) diff --git a/src/tactic/bv/bvarray2uf_rewriter.cpp b/src/tactic/bv/bvarray2uf_rewriter.cpp index 54c654d54..d4e738ed7 100644 --- a/src/tactic/bv/bvarray2uf_rewriter.cpp +++ b/src/tactic/bv/bvarray2uf_rewriter.cpp @@ -25,6 +25,7 @@ Notes: #include"ast_pp.h" #include"bvarray2uf_rewriter.h" #include"rewriter_def.h" +#include"ref_util.h" // [1] C. M. Wintersteiger, Y. Hamadi, and L. de Moura: Efficiently Solving // Quantified Bit-Vector Formulas, in Formal Methods in System Design, @@ -50,10 +51,7 @@ bvarray2uf_rewriter_cfg::bvarray2uf_rewriter_cfg(ast_manager & m, params_ref con } bvarray2uf_rewriter_cfg::~bvarray2uf_rewriter_cfg() { - for (obj_map::iterator it = m_arrays_fs.begin(); - it != m_arrays_fs.end(); - it++) - m_manager.dec_ref(it->m_value); + dec_ref_map_key_values(m_manager, m_arrays_fs); } void bvarray2uf_rewriter_cfg::reset() {} @@ -110,12 +108,12 @@ func_decl_ref bvarray2uf_rewriter_cfg::mk_uf_for_array(expr * e) { if (m_array_util.is_as_array(e)) return func_decl_ref(static_cast(to_app(e)->get_decl()->get_parameter(0).get_ast()), m_manager); else { - app * a = to_app(e); func_decl * bv_f = 0; if (!m_arrays_fs.find(e, bv_f)) { - sort * domain = get_index_sort(a); - sort * range = get_value_sort(a); + sort * domain = get_index_sort(e); + sort * range = get_value_sort(e); bv_f = m_manager.mk_fresh_func_decl("f_t", "", 1, &domain, range); + TRACE("bvarray2uf_rw", tout << "for " << mk_ismt2_pp(e, m_manager) << " new func_decl is " << mk_ismt2_pp(bv_f, m_manager) << std::endl; ); if (is_uninterp_const(e)) { if (m_emc) m_emc->insert(to_app(e)->get_decl(), @@ -124,8 +122,12 @@ func_decl_ref bvarray2uf_rewriter_cfg::mk_uf_for_array(expr * e) { else if (m_fmc) m_fmc->insert(bv_f); m_arrays_fs.insert(e, bv_f); + m_manager.inc_ref(e); m_manager.inc_ref(bv_f); } + else { + TRACE("bvarray2uf_rw", tout << "for " << mk_ismt2_pp(e, m_manager) << " found " << mk_ismt2_pp(bv_f, m_manager) << std::endl; ); + } return func_decl_ref(bv_f, m_manager); } @@ -138,18 +140,24 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr SASSERT(num == 2); // From [1]: Finally, we replace equations of the form t = s, // where t and s are arrays, with \forall x . f_t(x) = f_s(x). - func_decl_ref f_t(mk_uf_for_array(args[0]), m_manager); - func_decl_ref f_s(mk_uf_for_array(args[1]), m_manager); + if (m_manager.are_equal(args[0], args[1])) { + result = m_manager.mk_true(); + res = BR_DONE; + } + else { + func_decl_ref f_t(mk_uf_for_array(args[0]), m_manager); + func_decl_ref f_s(mk_uf_for_array(args[1]), m_manager); - sort * sorts[1] = { get_index_sort(m_manager.get_sort(args[0])) }; - symbol names[1] = { symbol("x") }; - var_ref x(m_manager.mk_var(0, sorts[0]), m_manager); + sort * sorts[1] = { get_index_sort(m_manager.get_sort(args[0])) }; + symbol names[1] = { symbol("x") }; + var_ref x(m_manager.mk_var(0, sorts[0]), m_manager); - expr_ref body(m_manager); - body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), m_manager.mk_app(f_s, x.get())); + expr_ref body(m_manager); + body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), m_manager.mk_app(f_s, x.get())); - result = m_manager.mk_forall(1, sorts, names, body); - res = BR_DONE; + result = m_manager.mk_forall(1, sorts, names, body); + res = BR_DONE; + } } else if (m_manager.is_distinct(f) && is_bv_array(f->get_domain()[0])) { result = m_manager.mk_distinct_expanded(num, args); @@ -310,7 +318,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr } } - CTRACE("bvarray2uf_rw", res==BR_DONE, tout << "result: " << mk_ismt2_pp(result, m()) << std::endl; ); + CTRACE("bvarray2uf_rw", res == BR_DONE, tout << "result: " << mk_ismt2_pp(result, m()) << std::endl; ); return res; } diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp index 42ceaf78c..ecf1889a2 100644 --- a/src/tactic/bv/bvarray2uf_tactic.cpp +++ b/src/tactic/bv/bvarray2uf_tactic.cpp @@ -62,7 +62,6 @@ class bvarray2uf_tactic : public tactic { SASSERT(g->is_well_sorted()); tactic_report report("bvarray2uf", *g); mc = 0; pc = 0; core = 0; result.reset(); - fail_if_proof_generation("bvarray2uf", g); fail_if_unsat_core_generation("bvarray2uf", g); TRACE("bvarray2uf", tout << "Before: " << std::endl; g->display(tout); ); @@ -73,7 +72,6 @@ class bvarray2uf_tactic : public tactic { filter_model_converter * fmc = alloc(filter_model_converter, m_manager); mc = concat(emc, fmc); m_rw.set_mcs(emc, fmc); - } @@ -86,10 +84,10 @@ class bvarray2uf_tactic : public tactic { break; expr * curr = g->form(idx); m_rw(curr, new_curr, new_pr); - //if (m_produce_proofs) { - // proof * pr = g->pr(idx); - // new_pr = m.mk_modus_ponens(pr, new_pr); - //} + if (m_produce_proofs) { + proof * pr = g->pr(idx); + new_pr = m_manager.mk_modus_ponens(pr, new_pr); + } g->update(idx, new_curr, new_pr, g->dep(idx)); } @@ -143,7 +141,7 @@ public: virtual void cleanup() { ast_manager & m = m_imp->m(); imp * d = alloc(imp, m, m_params); - std::swap(d, m_imp); + std::swap(d, m_imp); dealloc(d); } From bd0bd08ecf15c97a37cd17d021513a83255a37ff Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 8 Apr 2016 16:58:11 +0100 Subject: [PATCH 16/17] add is_considered_uninterpreted checks into acker_helper --- src/ackermannization/ackr_helper.h | 15 ++------------- 1 file changed, 2 insertions(+), 13 deletions(-) diff --git a/src/ackermannization/ackr_helper.h b/src/ackermannization/ackr_helper.h index 5c572907e..70d6ab57b 100644 --- a/src/ackermannization/ackr_helper.h +++ b/src/ackermannization/ackr_helper.h @@ -33,19 +33,8 @@ class ackr_helper { which are not marked as uninterpreted but effectively are. */ inline bool should_ackermannize(app const * a) const { - if (a->get_family_id() == m_bvutil.get_family_id()) { - switch (a->get_decl_kind()) { - case OP_BSDIV0: - case OP_BUDIV0: - case OP_BSREM0: - case OP_BUREM0: - case OP_BSMOD0: - return true; - default: - return is_uninterp(a); - } - } - return (is_uninterp(a)); + decl_plugin * p = m_bvutil.get_manager().get_plugin(a->get_family_id()); + return p->is_considered_uninterpreted(a->get_decl()); } inline bv_util& bvutil() { return m_bvutil; } From 16e487b32a07a3c218cb0f0f76afc9321c9ed37d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 8 Apr 2016 17:20:09 +0100 Subject: [PATCH 17/17] Bugfix for ackermann helper --- src/ackermannization/ackr_helper.h | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/ackermannization/ackr_helper.h b/src/ackermannization/ackr_helper.h index 70d6ab57b..327763da4 100644 --- a/src/ackermannization/ackr_helper.h +++ b/src/ackermannization/ackr_helper.h @@ -33,8 +33,12 @@ class ackr_helper { which are not marked as uninterpreted but effectively are. */ inline bool should_ackermannize(app const * a) const { - decl_plugin * p = m_bvutil.get_manager().get_plugin(a->get_family_id()); - return p->is_considered_uninterpreted(a->get_decl()); + if (is_uninterp(a)) + return true; + else { + decl_plugin * p = m_bvutil.get_manager().get_plugin(a->get_family_id()); + return p->is_considered_uninterpreted(a->get_decl()); + } } inline bv_util& bvutil() { return m_bvutil; }