diff --git a/src/ast/simplifiers/CMakeLists.txt b/src/ast/simplifiers/CMakeLists.txt index 356944281..d43bbe203 100644 --- a/src/ast/simplifiers/CMakeLists.txt +++ b/src/ast/simplifiers/CMakeLists.txt @@ -1,6 +1,7 @@ z3_add_component(simplifiers SOURCES bit_blaster.cpp + bv1_blaster.cpp bound_manager.cpp bound_propagator.cpp bound_simplifier.cpp @@ -32,6 +33,7 @@ z3_add_component(simplifiers substitution TACTIC_HEADERS bit_blaster.h + bv1_blaster.h bit2int.h blast_term_ite_simplifier.h elim_bounds.h diff --git a/src/ast/simplifiers/bv1_blaster.cpp b/src/ast/simplifiers/bv1_blaster.cpp new file mode 100644 index 000000000..e91b1795a --- /dev/null +++ b/src/ast/simplifiers/bv1_blaster.cpp @@ -0,0 +1,292 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + bv1_blaster.cpp + +Abstract: + + Simplifier for "blasting" bit-vectors of size n into bit-vectors of size 1. + This simplifier only supports concat and extract operators. + This transformation is useful for handling benchmarks that contain + many BV equalities. + + Remark: other operators can be mapped into concat/extract by using + the simplifiers. + +Author: + + Leonardo (leonardo) 2011-10-25 + +--*/ +#include "ast/simplifiers/bv1_blaster.h" +#include "ast/ast_util.h" +#include "ast/rewriter/bv_rewriter.h" +#include "ast/rewriter/rewriter_types.h" +#include "util/common_msgs.h" + +bv1_blaster_simplifier::rw_cfg::rw_cfg(ast_manager& m, params_ref const& p) : + m_manager(m), + m_util(m), + m_saved(m), + m_bit1(m), + m_bit0(m) { + m_bit1 = butil().mk_numeral(rational(1), 1); + m_bit0 = butil().mk_numeral(rational(0), 1); + updt_params(p); +} + +void bv1_blaster_simplifier::rw_cfg::updt_params(params_ref const& p) { + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); + m_max_steps = p.get_uint("max_steps", UINT_MAX); +} + +bool bv1_blaster_simplifier::rw_cfg::max_steps_exceeded(unsigned num_steps) const { + if (memory::get_allocation_size() > m_max_memory) + throw rewriter_exception(Z3_MAX_MEMORY_MSG); + return num_steps > m_max_steps; +} + +void bv1_blaster_simplifier::rw_cfg::get_bits(expr* arg, bit_buffer& bits) { + SASSERT(butil().is_concat(arg) || butil().get_bv_size(arg) == 1); + if (butil().is_concat(arg)) + bits.append(to_app(arg)->get_num_args(), to_app(arg)->get_args()); + else + bits.push_back(arg); +} + +void bv1_blaster_simplifier::rw_cfg::mk_const(func_decl* f, expr_ref& result) { + SASSERT(f->get_family_id() == null_family_id); + SASSERT(f->get_arity() == 0); + expr* r; + if (m_const2bits.find(f, r)) { + result = r; + return; + } + sort* s = f->get_range(); + SASSERT(butil().is_bv_sort(s)); + unsigned bv_size = butil().get_bv_size(s); + if (bv_size == 1) { + result = m().mk_const(f); + return; + } + sort* b = butil().mk_sort(1); + ptr_buffer bits; + for (unsigned i = 0; i < bv_size; ++i) { + bits.push_back(m().mk_fresh_const(nullptr, b)); + m_newbits.push_back(to_app(bits.back())->get_decl()); + m_saved.push_back(m_newbits.back()); + } + r = butil().mk_concat(bits.size(), bits.data()); + m_saved.push_back(r); + m_saved.push_back(f); + m_const2bits.insert(f, r); + result = r; +} + +void bv1_blaster_simplifier::rw_cfg::blast_bv_term(expr* t, expr_ref& result) { + bit_buffer bits; + unsigned bv_size = butil().get_bv_size(t); + if (bv_size == 1) { + result = t; + return; + } + unsigned i = bv_size; + while (i > 0) { + --i; + bits.push_back(butil().mk_extract(i, i, t)); + } + result = butil().mk_concat(bits.size(), bits.data()); +} + +void bv1_blaster_simplifier::rw_cfg::reduce_eq(expr* arg1, expr* arg2, expr_ref& result) { + bit_buffer bits1; + bit_buffer bits2; + get_bits(arg1, bits1); + get_bits(arg2, bits2); + SASSERT(bits1.size() == bits2.size()); + bit_buffer new_eqs; + unsigned i = bits1.size(); + while (i > 0) { + --i; + new_eqs.push_back(m().mk_eq(bits1[i], bits2[i])); + } + result = mk_and(m(), new_eqs.size(), new_eqs.data()); +} + +void bv1_blaster_simplifier::rw_cfg::reduce_ite(expr* c, expr* t, expr* e, expr_ref& result) { + bit_buffer t_bits; + bit_buffer e_bits; + get_bits(t, t_bits); + get_bits(e, e_bits); + SASSERT(t_bits.size() == e_bits.size()); + bit_buffer new_ites; + unsigned num = t_bits.size(); + for (unsigned i = 0; i < num; ++i) + new_ites.push_back(t_bits[i] == e_bits[i] ? t_bits[i] : m().mk_ite(c, t_bits[i], e_bits[i])); + result = butil().mk_concat(new_ites.size(), new_ites.data()); +} + +void bv1_blaster_simplifier::rw_cfg::reduce_num(func_decl* f, expr_ref& result) { + SASSERT(f->get_num_parameters() == 2); + SASSERT(f->get_parameter(0).is_rational()); + SASSERT(f->get_parameter(1).is_int()); + bit_buffer bits; + rational v = f->get_parameter(0).get_rational(); + rational two(2); + unsigned sz = f->get_parameter(1).get_int(); + for (unsigned i = 0; i < sz; ++i) { + if ((v % two).is_zero()) + bits.push_back(m_bit0); + else + bits.push_back(m_bit1); + v = div(v, two); + } + std::reverse(bits.begin(), bits.end()); + result = butil().mk_concat(bits.size(), bits.data()); +} + +void bv1_blaster_simplifier::rw_cfg::reduce_extract(func_decl* f, expr* arg, expr_ref& result) { + bit_buffer arg_bits; + get_bits(arg, arg_bits); + SASSERT(arg_bits.size() == butil().get_bv_size(arg)); + unsigned high = butil().get_extract_high(f); + unsigned low = butil().get_extract_low(f); + unsigned sz = arg_bits.size(); + unsigned start = sz - 1 - high; + unsigned end = sz - 1 - low; + bit_buffer bits; + for (unsigned i = start; i <= end; ++i) + bits.push_back(arg_bits[i]); + result = butil().mk_concat(bits.size(), bits.data()); +} + +void bv1_blaster_simplifier::rw_cfg::reduce_concat(unsigned num, expr* const* args, expr_ref& result) { + bit_buffer bits; + bit_buffer arg_bits; + for (unsigned i = 0; i < num; ++i) { + expr* arg = args[i]; + arg_bits.reset(); + get_bits(arg, arg_bits); + bits.append(arg_bits.size(), arg_bits.data()); + } + result = butil().mk_concat(bits.size(), bits.data()); +} + +void bv1_blaster_simplifier::rw_cfg::reduce_bin_xor(expr* arg1, expr* arg2, expr_ref& result) { + bit_buffer bits1; + bit_buffer bits2; + get_bits(arg1, bits1); + get_bits(arg2, bits2); + SASSERT(bits1.size() == bits2.size()); + bit_buffer new_bits; + unsigned num = bits1.size(); + for (unsigned i = 0; i < num; ++i) + new_bits.push_back(m().mk_ite(m().mk_eq(bits1[i], bits2[i]), m_bit0, m_bit1)); + result = butil().mk_concat(new_bits.size(), new_bits.data()); +} + +void bv1_blaster_simplifier::rw_cfg::reduce_xor(unsigned num_args, expr* const* args, expr_ref& result) { + SASSERT(num_args > 0); + if (num_args == 1) { + result = args[0]; + return; + } + reduce_bin_xor(args[0], args[1], result); + for (unsigned i = 2; i < num_args; ++i) + reduce_bin_xor(result, args[i], result); +} + +br_status bv1_blaster_simplifier::rw_cfg::reduce_app(func_decl* f, unsigned num, expr* const* args, + expr_ref& result, proof_ref& result_pr) { + result_pr = nullptr; + if (num == 0 && f->get_family_id() == null_family_id && butil().is_bv_sort(f->get_range())) { + mk_const(f, result); + return BR_DONE; + } + + if (m().is_eq(f)) { + SASSERT(num == 2); + if (butil().is_bv(args[0])) { + reduce_eq(args[0], args[1], result); + return BR_DONE; + } + return BR_FAILED; + } + + if (m().is_ite(f)) { + SASSERT(num == 3); + if (butil().is_bv(args[1])) { + reduce_ite(args[0], args[1], args[2], result); + return BR_DONE; + } + return BR_FAILED; + } + + if (f->get_family_id() == butil().get_family_id()) { + switch (f->get_decl_kind()) { + case OP_BV_NUM: + reduce_num(f, result); + return BR_DONE; + case OP_EXTRACT: + SASSERT(num == 1); + reduce_extract(f, args[0], result); + return BR_DONE; + case OP_CONCAT: + reduce_concat(num, args, result); + return BR_DONE; + case OP_BXOR: + reduce_xor(num, args, result); + return BR_DONE; + default: + return BR_FAILED; + } + } + + if (butil().is_bv_sort(f->get_range())) { + blast_bv_term(m().mk_app(f, num, args), result); + return BR_DONE; + } + + return BR_FAILED; +} + +void bv1_blaster_simplifier::collect_param_descrs(param_descrs& r) { + insert_max_memory(r); + insert_max_steps(r); +} + +void bv1_blaster_simplifier::reduce() { + auto& cfg = m_rw.cfg(); + unsigned prev_bits = cfg.m_newbits.size(); + + expr_ref new_curr(m); + proof_ref new_pr(m); + + for (unsigned idx : indices()) { + auto const& d = m_fmls[idx]; + m_rw(d.fml(), new_curr, new_pr); + if (d.fml() != new_curr) + m_fmls.update(idx, dependent_expr(m, new_curr, mp(d.pr(), new_pr), d.dep())); + } + + if (prev_bits == cfg.m_newbits.size()) + return; + + // Hide newly introduced bit variables in the model + for (unsigned i = prev_bits; i < cfg.m_newbits.size(); ++i) + m_fmls.model_trail().hide(cfg.m_newbits[i]); + + // Push definitions for constants whose bits were just introduced + obj_hashtable new_bit_set; + for (unsigned i = prev_bits; i < cfg.m_newbits.size(); ++i) + new_bit_set.insert(cfg.m_newbits[i]); + + for (auto const& [f, v] : cfg.m_const2bits) { + SASSERT(cfg.butil().is_concat(v)); + func_decl* first = to_app(to_app(v)->get_arg(0))->get_decl(); + if (new_bit_set.contains(first)) + m_fmls.model_trail().push(f, v, nullptr, {}); + } +} diff --git a/src/ast/simplifiers/bv1_blaster.h b/src/ast/simplifiers/bv1_blaster.h new file mode 100644 index 000000000..28666bbd2 --- /dev/null +++ b/src/ast/simplifiers/bv1_blaster.h @@ -0,0 +1,98 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + bv1_blaster.h + +Abstract: + + Simplifier for "blasting" bit-vectors of size n into bit-vectors of size 1. + This simplifier only supports concat and extract operators. + This transformation is useful for handling benchmarks that contain + many BV equalities. + + Remark: other operators can be mapped into concat/extract by using + the simplifiers. + +Author: + + Leonardo (leonardo) 2011-10-25 + +--*/ +#pragma once + +#include "ast/simplifiers/dependent_expr_state.h" +#include "ast/bv_decl_plugin.h" +#include "ast/rewriter/rewriter_def.h" +#include "util/params.h" + +class bv1_blaster_simplifier : public dependent_expr_simplifier { + + struct rw_cfg : public default_rewriter_cfg { + ast_manager & m_manager; + bv_util m_util; + obj_map m_const2bits; + ptr_vector m_newbits; + ast_ref_vector m_saved; + expr_ref m_bit1; + expr_ref m_bit0; + unsigned long long m_max_memory; + unsigned m_max_steps; + + ast_manager& m() const { return m_manager; } + bv_util& butil() { return m_util; } + bv_util const& butil() const { return m_util; } + + void cleanup_buffers() { m_saved.finalize(); } + + rw_cfg(ast_manager& m, params_ref const& p); + void updt_params(params_ref const& p); + bool rewrite_patterns() const { return false; } + bool max_steps_exceeded(unsigned num_steps) const; + + typedef ptr_buffer bit_buffer; + + void get_bits(expr* arg, bit_buffer& bits); + void mk_const(func_decl* f, expr_ref& result); + void blast_bv_term(expr* t, expr_ref& result); + void reduce_eq(expr* arg1, expr* arg2, expr_ref& result); + void reduce_ite(expr* c, expr* t, expr* e, expr_ref& result); + void reduce_num(func_decl* f, expr_ref& result); + void reduce_extract(func_decl* f, expr* arg, expr_ref& result); + void reduce_concat(unsigned num, expr* const* args, expr_ref& result); + void reduce_bin_xor(expr* arg1, expr* arg2, expr_ref& result); + void reduce_xor(unsigned num_args, expr* const* args, expr_ref& result); + + br_status reduce_app(func_decl* f, unsigned num, expr* const* args, + expr_ref& result, proof_ref& result_pr); + + bool reduce_quantifier(quantifier* old_q, expr* new_body, + expr* const* new_patterns, expr* const* new_no_patterns, + expr_ref& result, proof_ref& result_pr) { + return false; + } + }; + + struct rw : public rewriter_tpl { + rw_cfg m_cfg; + rw(ast_manager& m, params_ref const& p) : + rewriter_tpl(m, m.proofs_enabled(), m_cfg), + m_cfg(m, p) {} + }; + + rw m_rw; + +public: + bv1_blaster_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& s) + : dependent_expr_simplifier(m, s), m_rw(m, p) {} + + char const* name() const override { return "bv1-blast"; } + void updt_params(params_ref const& p) override { m_rw.cfg().updt_params(p); } + void collect_param_descrs(param_descrs& r) override; + void reduce() override; +}; + +/* + ADD_SIMPLIFIER("bv1-blast", "reduce bit-vector expressions into bit-vectors of size 1 (notes: only equality, extract and concat are supported).", "alloc(bv1_blaster_simplifier, m, p, s)") +*/ diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp index 264a01a1a..47bec0e7f 100644 --- a/src/tactic/bv/bv1_blaster_tactic.cpp +++ b/src/tactic/bv/bv1_blaster_tactic.cpp @@ -7,13 +7,7 @@ Module Name: Abstract: - Rewriter for "blasting" bit-vectors of size n into bit-vectors of size 1. - This rewriter only supports concat and extract operators. - This transformation is useful for handling benchmarks that contain - many BV equalities. - - Remark: other operators can be mapped into concat/extract by using - the simplifiers. + Probe for checking if a goal is in the QF_BV fragment that uses only =, extract, and concat. Author: @@ -22,469 +16,50 @@ Author: Notes: --*/ -#include "tactic/tactical.h" -#include "tactic/bv/bit_blaster_model_converter.h" +#include "tactic/bv/bv1_blaster_tactic.h" +#include "tactic/tactic.h" #include "ast/bv_decl_plugin.h" -#include "ast/rewriter/rewriter_def.h" #include "ast/for_each_expr.h" -#include "ast/ast_util.h" -#include "ast/rewriter/bv_rewriter.h" - -class bv1_blaster_tactic : public tactic { - - struct rw_cfg : public default_rewriter_cfg { - ast_manager & m_manager; - bv_util m_util; - obj_map m_const2bits; - ptr_vector m_newbits; - ast_ref_vector m_saved; - expr_ref m_bit1; - expr_ref m_bit0; - - unsigned long long m_max_memory; // in bytes - unsigned m_max_steps; - bool m_produce_models; - - ast_manager & m() const { return m_manager; } - bv_util & butil() { return m_util; } - bv_util const & butil() const { return m_util; } - - void cleanup_buffers() { - m_saved.finalize(); - } - - rw_cfg(ast_manager & m, params_ref const & p): - m_manager(m), - m_util(m), - m_saved(m), - m_bit1(m), - m_bit0(m) { - m_bit1 = butil().mk_numeral(rational(1), 1); - m_bit0 = butil().mk_numeral(rational(0), 1); - updt_params(p); - } - - void updt_params(params_ref const & p) { - m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); - m_max_steps = p.get_uint("max_steps", UINT_MAX); - m_produce_models = p.get_bool("produce_models", false); - } - - bool rewrite_patterns() const { UNREACHABLE(); return false; } - - bool max_steps_exceeded(unsigned num_steps) const { - if (memory::get_allocation_size() > m_max_memory) - throw tactic_exception(TACTIC_MAX_MEMORY_MSG); - return num_steps > m_max_steps; - } - - typedef ptr_buffer bit_buffer; - - void get_bits(expr * arg, bit_buffer & bits) { - SASSERT(butil().is_concat(arg) || butil().get_bv_size(arg) == 1); - if (butil().is_concat(arg)) - bits.append(to_app(arg)->get_num_args(), to_app(arg)->get_args()); - else - bits.push_back(arg); - } - - void mk_const(func_decl * f, expr_ref & result) { - SASSERT(f->get_family_id() == null_family_id); - SASSERT(f->get_arity() == 0); - expr * r; - if (m_const2bits.find(f, r)) { - result = r; - return; - } - sort * s = f->get_range(); - SASSERT(butil().is_bv_sort(s)); - unsigned bv_size = butil().get_bv_size(s); - if (bv_size == 1) { - result = m().mk_const(f); - return; - } - sort * b = butil().mk_sort(1); - ptr_buffer bits; - for (unsigned i = 0; i < bv_size; ++i) { - bits.push_back(m().mk_fresh_const(nullptr, b)); - m_newbits.push_back(to_app(bits.back())->get_decl()); - m_saved.push_back(m_newbits.back()); - } - r = butil().mk_concat(bits.size(), bits.data()); - m_saved.push_back(r); - m_saved.push_back(f); - m_const2bits.insert(f, r); - result = r; - } - - void blast_bv_term(expr * t, expr_ref & result) { - bit_buffer bits; - unsigned bv_size = butil().get_bv_size(t); - if (bv_size == 1) { - result = t; - return; - } - unsigned i = bv_size; - while (i > 0) { - --i; - bits.push_back(butil().mk_extract(i, i, t)); - } - result = butil().mk_concat(bits.size(), bits.data()); - } - - void reduce_eq(expr * arg1, expr * arg2, expr_ref & result) { - bit_buffer bits1; - bit_buffer bits2; - get_bits(arg1, bits1); - get_bits(arg2, bits2); - SASSERT(bits1.size() == bits2.size()); - bit_buffer new_eqs; - unsigned i = bits1.size(); - while (i > 0) { - --i; - new_eqs.push_back(m().mk_eq(bits1[i], bits2[i])); - } - result = mk_and(m(), new_eqs.size(), new_eqs.data()); - } - - void reduce_ite(expr * c, expr * t, expr * e, expr_ref & result) { - bit_buffer t_bits; - bit_buffer e_bits; - get_bits(t, t_bits); - get_bits(e, e_bits); - SASSERT(t_bits.size() == e_bits.size()); - bit_buffer new_ites; - unsigned num = t_bits.size(); - for (unsigned i = 0; i < num; ++i) - new_ites.push_back(t_bits[i] == e_bits[i] ? t_bits[i] : m().mk_ite(c, t_bits[i], e_bits[i])); - result = butil().mk_concat(new_ites.size(), new_ites.data()); - } - - void reduce_num(func_decl * f, expr_ref & result) { - SASSERT(f->get_num_parameters() == 2); - SASSERT(f->get_parameter(0).is_rational()); - SASSERT(f->get_parameter(1).is_int()); - bit_buffer bits; - rational v = f->get_parameter(0).get_rational(); - rational two(2); - unsigned sz = f->get_parameter(1).get_int(); - for (unsigned i = 0; i < sz; ++i) { - if ((v % two).is_zero()) - bits.push_back(m_bit0); - else - bits.push_back(m_bit1); - v = div(v, two); - } - std::reverse(bits.begin(), bits.end()); - result = butil().mk_concat(bits.size(), bits.data()); - } - - void reduce_extract(func_decl * f, expr * arg, expr_ref & result) { - bit_buffer arg_bits; - get_bits(arg, arg_bits); - SASSERT(arg_bits.size() == butil().get_bv_size(arg)); - unsigned high = butil().get_extract_high(f); - unsigned low = butil().get_extract_low(f); - unsigned sz = arg_bits.size(); - unsigned start = sz - 1 - high; - unsigned end = sz - 1 - low; - bit_buffer bits; - for (unsigned i = start; i <= end; ++i) { - bits.push_back(arg_bits[i]); - } - result = butil().mk_concat(bits.size(), bits.data()); - } - - void reduce_concat(unsigned num, expr * const * args, expr_ref & result) { - bit_buffer bits; - bit_buffer arg_bits; - for (unsigned i = 0; i < num; ++i) { - expr * arg = args[i]; - arg_bits.reset(); - get_bits(arg, arg_bits); - bits.append(arg_bits.size(), arg_bits.data()); - } - result = butil().mk_concat(bits.size(), bits.data()); - } - - void reduce_bin_xor(expr * arg1, expr * arg2, expr_ref & result) { - bit_buffer bits1; - bit_buffer bits2; - get_bits(arg1, bits1); - get_bits(arg2, bits2); - SASSERT(bits1.size() == bits2.size()); - bit_buffer new_bits; - unsigned num = bits1.size(); - for (unsigned i = 0; i < num; ++i) { - new_bits.push_back(m().mk_ite(m().mk_eq(bits1[i], bits2[i]), m_bit0, m_bit1)); - } - result = butil().mk_concat(new_bits.size(), new_bits.data()); - } - - void reduce_xor(unsigned num_args, expr * const * args, expr_ref & result) { - SASSERT(num_args > 0); -#if 1 - if (num_args == 1) { - result = args[0]; - return; - } - reduce_bin_xor(args[0], args[1], result); - for (unsigned i = 2; i < num_args; ++i) { - reduce_bin_xor(result, args[i], result); - } -#else - ptr_buffer args_bits; - for (unsigned i = 0; i < num_args; ++i) { - bit_buffer * buff_i = alloc(bit_buffer); - get_bits(args[i], *buff_i); - args_bits.push_back(buff_i); - } - bit_buffer new_bits; - unsigned sz = butil().get_bv_size(args[0]); - for (unsigned i = 0; i < sz; ++i) { - ptr_buffer eqs; - for (unsigned j = 0; j < num_args; ++j) { - bit_buffer * buff_j = args_bits[j]; - eqs.push_back(m().mk_eq(buff_j->get(i), m_bit1)); - } - expr * cond = m().mk_xor(eqs.size(), eqs.c_ptr()); - new_bits.push_back(m().mk_ite(cond, m_bit1, m_bit0)); - } - result = butil().mk_concat(new_bits.size(), new_bits.c_ptr()); - std::for_each(args_bits.begin(), args_bits.end(), delete_proc()); -#endif - } - - br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { - result_pr = nullptr; - if (num == 0 && f->get_family_id() == null_family_id && butil().is_bv_sort(f->get_range())) { - mk_const(f, result); - return BR_DONE; - } - - if (m().is_eq(f)) { - SASSERT(num == 2); - if (butil().is_bv(args[0])) { - reduce_eq(args[0], args[1], result); - return BR_DONE; - } - return BR_FAILED; - } - - if (m().is_ite(f)) { - SASSERT(num == 3); - if (butil().is_bv(args[1])) { - reduce_ite(args[0], args[1], args[2], result); - return BR_DONE; - } - return BR_FAILED; - } - - if (f->get_family_id() == butil().get_family_id()) { - switch (f->get_decl_kind()) { - case OP_BV_NUM: - reduce_num(f, result); - return BR_DONE; - case OP_EXTRACT: - SASSERT(num == 1); - reduce_extract(f, args[0], result); - return BR_DONE; - case OP_CONCAT: - reduce_concat(num, args, result); - return BR_DONE; - case OP_BXOR: - reduce_xor(num, args, result); - return BR_DONE; - default: - UNREACHABLE(); - return BR_FAILED; - } - } - - if (butil().is_bv_sort(f->get_range())) { - blast_bv_term(m().mk_app(f, num, args), result); - return BR_DONE; - } - - return BR_FAILED; - } - - bool reduce_quantifier(quantifier * old_q, - expr * new_body, - expr * const * new_patterns, - expr * const * new_no_patterns, - expr_ref & result, - proof_ref & result_pr) { - UNREACHABLE(); - return false; - } - }; - - struct rw : public rewriter_tpl { - rw_cfg m_cfg; - - rw(ast_manager & m, params_ref const & p): - rewriter_tpl(m, m.proofs_enabled(), m_cfg), - m_cfg(m, p) { - } - }; - - - struct imp { - rw m_rw; - unsigned m_num_steps; - - imp(ast_manager & m, params_ref const & p): - m_rw(m, p) { - } - - struct not_target : public std::exception {}; - - struct visitor { - family_id m_bv_fid; - visitor(family_id bv_fid):m_bv_fid(bv_fid) {} - void operator()(var const * n) { throw not_target(); } - void operator()(app const * n) { - if (n->get_family_id() == m_bv_fid) { - switch (n->get_decl_kind()) { - case OP_BV_NUM: - case OP_EXTRACT: - case OP_CONCAT: - return; - case OP_BXOR: - // it doesn't payoff to do the reduction in this case. - throw not_target(); - default: - throw not_target(); - } - } - } - void operator()(quantifier const * n) { throw not_target(); } - }; - - bool is_target(goal const & g) const { - expr_fast_mark1 visited; - unsigned sz = g.size(); - visitor proc(m_rw.cfg().butil().get_family_id()); - try { - for (unsigned i = 0; i < sz; ++i) { - expr * f = g.form(i); - for_each_expr_core(proc, visited, f); - } - } - catch (const not_target &) { - return false; - } - return true; - } - - ast_manager & m() const { return m_rw.m(); } - - - void operator()(goal_ref const & g, - goal_ref_buffer & result) { - - if (!is_target(*g)) - throw tactic_exception("bv1 blaster cannot be applied to goal"); - - tactic_report report("bv1-blaster", *g); - m_num_steps = 0; - - bool proofs_enabled = g->proofs_enabled(); - expr_ref new_curr(m()); - proof_ref new_pr(m()); - unsigned size = g->size(); - for (unsigned idx = 0; idx < size; ++idx) { - if (g->inconsistent()) - break; - expr * curr = g->form(idx); - m_rw(curr, new_curr, new_pr); - m_num_steps += m_rw.get_num_steps(); - if (proofs_enabled) { - proof * pr = g->pr(idx); - new_pr = m().mk_modus_ponens(pr, new_pr); - } - g->update(idx, new_curr, new_pr, g->dep(idx)); - } - - if (g->models_enabled()) - g->add(mk_bv1_blaster_model_converter(m(), m_rw.cfg().m_const2bits, m_rw.cfg().m_newbits)); - g->inc_depth(); - result.push_back(g.get()); - m_rw.cfg().cleanup(); - } - - unsigned get_num_steps() const { return m_num_steps; } - }; - - imp * m_imp; - params_ref m_params; -public: - bv1_blaster_tactic(ast_manager & m, params_ref const & p = params_ref()): - m_params(p) { - m_imp = alloc(imp, m, p); - } - - tactic * translate(ast_manager & m) override { - return alloc(bv1_blaster_tactic, m, m_params); - } - - ~bv1_blaster_tactic() override { - dealloc(m_imp); - } - - char const* name() const override { return "bv1_blaster"; } - - void updt_params(params_ref const & p) override { - m_params.append(p); - m_imp->m_rw.cfg().updt_params(m_params); - } - - void collect_param_descrs(param_descrs & r) override { - insert_max_memory(r); - insert_max_steps(r); - } - - bool is_target(goal const & g) const { - return m_imp->is_target(g); - } - - /** - \brief "Blast" bit-vectors of size n in s into bit-vectors of size 1. - If s contains other bit-vectors operators different from concat/extract, then this is method is a NO-OP. - It also does not support quantifiers. - Return a model_converter that converts any model for the updated set into a model for the old set. - */ - void operator()(goal_ref const & g, - goal_ref_buffer & result) override { - (*m_imp)(g, result); - } - - void cleanup() override { - imp * d = alloc(imp, m_imp->m(), m_params); - std::swap(d, m_imp); - dealloc(d); - } - - unsigned get_num_steps() const { - return m_imp->get_num_steps(); - } - -}; - -tactic * mk_bv1_blaster_tactic(ast_manager & m, params_ref const & p) { - return clean(alloc(bv1_blaster_tactic, m, p)); -} class is_qfbv_eq_probe : public probe { -public: - result operator()(goal const & g) override { - bv1_blaster_tactic t(g.m()); - return t.is_target(g); + struct not_target : public std::exception {}; + struct visitor { + family_id m_bv_fid; + visitor(family_id bv_fid) : m_bv_fid(bv_fid) {} + void operator()(var const* n) { throw not_target(); } + void operator()(app const* n) { + if (n->get_family_id() == m_bv_fid) { + switch (n->get_decl_kind()) { + case OP_BV_NUM: + case OP_EXTRACT: + case OP_CONCAT: + return; + default: + throw not_target(); + } + } + } + void operator()(quantifier const* n) { throw not_target(); } + }; + +public: + result operator()(goal const& g) override { + bv_util util(g.m()); + expr_fast_mark1 visited; + visitor proc(util.get_family_id()); + try { + for (unsigned i = 0; i < g.size(); ++i) + for_each_expr_core(proc, visited, g.form(i)); + } + catch (const not_target&) { + return false; + } + return true; } }; -probe * mk_is_qfbv_eq_probe() { +probe* mk_is_qfbv_eq_probe() { return alloc(is_qfbv_eq_probe); } + diff --git a/src/tactic/bv/bv1_blaster_tactic.h b/src/tactic/bv/bv1_blaster_tactic.h index 9cc7f90d5..17833fbf3 100644 --- a/src/tactic/bv/bv1_blaster_tactic.h +++ b/src/tactic/bv/bv1_blaster_tactic.h @@ -41,12 +41,22 @@ the simplifiers. #pragma once #include "util/params.h" +#include "tactic/dependent_expr_state_tactic.h" +#include "tactic/probe.h" +#include "ast/simplifiers/bv1_blaster.h" class ast_manager; class tactic; -tactic * mk_bv1_blaster_tactic(ast_manager & m, params_ref const & p = params_ref()); +inline tactic * mk_bv1_blaster_tactic(ast_manager & m, params_ref const & p = params_ref()) { + return alloc(dependent_expr_state_tactic, m, p, + [](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* { + return alloc(bv1_blaster_simplifier, m, p, s); + }); +} + probe * mk_is_qfbv_eq_probe(); /* ADD_TACTIC("bv1-blast", "reduce bit-vector expressions into bit-vectors of size 1 (notes: only equality, extract and concat are supported).", "mk_bv1_blaster_tactic(m, p)") ADD_PROBE("is-qfbv-eq", "true if the goal is in a fragment of QF_BV which uses only =, extract, concat.", "mk_is_qfbv_eq_probe()") */ +