From 53e582ba22b5bdb8cdf34dc4b13d0aa090571e40 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 4 Jul 2018 11:59:01 +0100 Subject: [PATCH 1/2] invertible_tactic: add support for a few more operations that produce full domain --- src/tactic/core/reduce_invertible_tactic.cpp | 107 +++++++++++++------ 1 file changed, 77 insertions(+), 30 deletions(-) diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp index 47c002de8..c098ae667 100644 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ b/src/tactic/core/reduce_invertible_tactic.cpp @@ -168,6 +168,69 @@ private: if (mc && !(*mc)) *mc = alloc(generic_model_converter, m, "reduce-invertible"); } + bool is_full_domain_var(expr* v, const rational*& model) { + auto f = is_app(v) ? to_app(v)->get_decl() : nullptr; + if (!f || f->get_family_id() != m_bv.get_family_id() || f->get_arity() == 0) + return false; + + switch (f->get_decl_kind()) { + case OP_BADD: + case OP_BSUB: + case OP_BSHL: + case OP_BASHR: + case OP_BLSHR: + case OP_BOR: + model = &rational::zero(); + return true; + + case OP_BAND: + model = &rational::minus_one(); + return true; + + case OP_BMUL: + case OP_BSDIV: + case OP_BSDIV0: + case OP_BSDIV_I: + case OP_BUDIV: + case OP_BUDIV0: + case OP_BUDIV_I: + model = &rational::one(); + return true; + + default: + return false; + } + } + + bool rewrite_unconstr(expr* v, expr_ref& new_v, generic_model_converter_ref* mc, unsigned max_var) { + const rational* mdl; + if (!is_full_domain_var(v, mdl)) + return false; + + app* a = to_app(v); + expr* fst_arg = a->get_arg(0); + bool fst_is_var = is_var(fst_arg); + + for (unsigned i = 0, n = a->get_num_args(); i != n; ++i) { + auto arg = a->get_arg(i); + if (!m_parents[arg->get_id()].get() || is_var(arg) != fst_is_var) + return false; + + if (fst_is_var && to_var(arg)->get_idx() >= max_var) + return false; + } + + if (mc) { + ensure_mc(mc); + expr_ref num(m_bv.mk_numeral(*mdl, get_sort(fst_arg)), m); + for (unsigned i = 1, n = a->get_num_args(); i != n; ++i) { + (*mc)->add(a->get_arg(i), num); + } + } + new_v = fst_arg; + return true; + } + // TBD: could be made to be recursive, by walking multiple layers of parents. bool is_invertible(expr* v, expr*& p, expr_ref& new_v, generic_model_converter_ref* mc, unsigned max_var = 0) { @@ -176,6 +239,20 @@ private: if (m_inverted.is_marked(p)) return false; if (mc && !is_ground(p)) return false; + if (m_bv.is_bv_xor(p) || + m_bv.is_bv_not(p) || + m_bv.is_bv_neg(p)) { + if (mc) { + ensure_mc(mc); + (*mc)->add(v, p); + } + new_v = v; + return true; + } + + if (rewrite_unconstr(p, new_v, mc, max_var)) + return true; + if (m_bv.is_bv_add(p)) { if (mc) { ensure_mc(mc); @@ -191,25 +268,6 @@ private: return true; } - expr *a, *b; - // shift(a, b), where both a,b are single use. Set b = 0 and return a - if (m_bv.is_bv_shl(p, a, b) || - m_bv.is_bv_ashr(p, a, b) || - m_bv.is_bv_lshr(p, a, b)) { - if (!m_parents[(v == a ? b : a)->get_id()].get() || is_var(a) != is_var(b)) - return false; - - if (is_var(a) && to_var(v == a ? b : a)->get_idx() >= max_var) - return false; - - if (mc) { - ensure_mc(mc); - (*mc)->add(b, m_bv.mk_numeral(rational::zero(), get_sort(b))); - } - new_v = a; - return true; - } - if (m_bv.is_bv_mul(p)) { expr_ref rest(m); for (expr* arg : *to_app(p)) { @@ -264,20 +322,9 @@ private: } return true; } - if (m_bv.is_bv_xor(p)) { - if (mc) { - ensure_mc(mc); - (*mc)->add(v, p); - } - new_v = v; - return true; - } if (m_bv.is_bv_sub(p)) { // TBD } - if (m_bv.is_bv_neg(p)) { - // TBD - } if (m_bv.is_bv_udivi(p)) { // TBD } From 9826835e15847a22b8cbcf4a6707e8d63b29ce9a Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 4 Jul 2018 16:50:37 +0100 Subject: [PATCH 2/2] invertible: fix bug with numerals, e.g. (bvmull x y #x32) --- src/tactic/core/reduce_invertible_tactic.cpp | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp index c098ae667..3420a3f99 100644 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ b/src/tactic/core/reduce_invertible_tactic.cpp @@ -168,7 +168,7 @@ private: if (mc && !(*mc)) *mc = alloc(generic_model_converter, m, "reduce-invertible"); } - bool is_full_domain_var(expr* v, const rational*& model) { + bool is_full_domain_var(expr* v, rational& model) { auto f = is_app(v) ? to_app(v)->get_decl() : nullptr; if (!f || f->get_family_id() != m_bv.get_family_id() || f->get_arity() == 0) return false; @@ -180,11 +180,11 @@ private: case OP_BASHR: case OP_BLSHR: case OP_BOR: - model = &rational::zero(); + model = rational::zero(); return true; case OP_BAND: - model = &rational::minus_one(); + model = rational::power_of_two(m_bv.get_bv_size(v)) - rational::one(); return true; case OP_BMUL: @@ -194,7 +194,7 @@ private: case OP_BUDIV: case OP_BUDIV0: case OP_BUDIV_I: - model = &rational::one(); + model = rational::one(); return true; default: @@ -203,10 +203,11 @@ private: } bool rewrite_unconstr(expr* v, expr_ref& new_v, generic_model_converter_ref* mc, unsigned max_var) { - const rational* mdl; + rational mdl; if (!is_full_domain_var(v, mdl)) return false; + rational r; app* a = to_app(v); expr* fst_arg = a->get_arg(0); bool fst_is_var = is_var(fst_arg); @@ -218,11 +219,14 @@ private: if (fst_is_var && to_var(arg)->get_idx() >= max_var) return false; + + if (m_bv.is_numeral(arg, r) && r != mdl) + return false; } if (mc) { ensure_mc(mc); - expr_ref num(m_bv.mk_numeral(*mdl, get_sort(fst_arg)), m); + expr_ref num(m_bv.mk_numeral(mdl, get_sort(fst_arg)), m); for (unsigned i = 1, n = a->get_num_args(); i != n; ++i) { (*mc)->add(a->get_arg(i), num); }