diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index 778b94c33..60adc3ae6 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -22,7 +22,7 @@ Revision History: #include"ast.h" -inline sort* get_array_range(sort const * s) { +inline sort* get_array_range(sort const * s) { return to_sort(s->get_parameter(s->get_num_parameters() - 1).get_ast()); } @@ -104,20 +104,20 @@ class array_decl_plugin : public decl_plugin { } // - // Contract for sort: - // parameters[0] - 1st dimension + // Contract for sort: + // parameters[0] - 1st dimension // ... // parameters[n-1] - nth dimension // parameters[n] - range // virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters); - + // // Contract for func_decl: // parameters[0] - array sort // Contract for others: // no parameters - virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); virtual void get_op_names(svector & op_names, symbol const & logic); @@ -184,6 +184,11 @@ public: sort * mk_array_sort(sort* dom, sort* range) { return mk_array_sort(1, &dom, range); } sort * mk_array_sort(unsigned arity, sort* const* domain, sort* range); + + app * mk_as_array(sort * s, func_decl * f) { + parameter param(f); + return m_manager.mk_app(m_fid, OP_AS_ARRAY, 1, ¶m, 0, 0, s); + } }; diff --git a/src/tactic/bv/bvarray2uf_rewriter.cpp b/src/tactic/bv/bvarray2uf_rewriter.cpp new file mode 100644 index 000000000..83038cfa9 --- /dev/null +++ b/src/tactic/bv/bvarray2uf_rewriter.cpp @@ -0,0 +1,377 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + bvarray2uf_rewriter.cpp + +Abstract: + + Rewriter that rewrites bit-vector arrays into bit-vector + (uninterpreted) functions. + +Author: + + Christoph (cwinter) 2015-11-04 + +Notes: + +--*/ + +#include"cooperate.h" +#include"bv_decl_plugin.h" +#include"array_decl_plugin.h" +#include"params.h" +#include"ast_pp.h" +#include"bvarray2uf_rewriter.h" + +// [1] C. M. Wintersteiger, Y. Hamadi, and L. de Moura: Efficiently Solving +// Quantified Bit-Vector Formulas, in Formal Methods in System Design, +// vol. 42, no. 1, pp. 3-23, Springer, 2013. + +bvarray2uf_rewriter_cfg::bvarray2uf_rewriter_cfg(ast_manager & m, params_ref const & p) : + m_manager(m), + m_out(m), + m_bindings(m), + m_bv_util(m), + m_array_util(m), + m_emc(0), + m_fmc(0), + extra_assertions(m) { + updt_params(p); + // We need to make sure that the mananger has the BV and array plugins loaded. + symbol s_bv("bv"); + if (!m_manager.has_plugin(s_bv)) + m_manager.register_plugin(s_bv, alloc(bv_decl_plugin)); + symbol s_array("array"); + if (!m_manager.has_plugin(s_array)) + m_manager.register_plugin(s_array, alloc(array_decl_plugin)); +} + +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); +} + +void bvarray2uf_rewriter_cfg::reset() {} + +sort * bvarray2uf_rewriter_cfg::get_index_sort(expr * e) { + return get_index_sort(m_manager.get_sort(e)); +} + +sort * bvarray2uf_rewriter_cfg::get_index_sort(sort * s) { + SASSERT(s->get_num_parameters() >= 2); + unsigned total_width = 0; + for (unsigned i = 0; i < s->get_num_parameters() - 1; i++) { + parameter const & p = s->get_parameter(i); + SASSERT(p.is_ast() && is_sort(to_sort(p.get_ast()))); + SASSERT(m_bv_util.is_bv_sort(to_sort(p.get_ast()))); + total_width += m_bv_util.get_bv_size(to_sort(p.get_ast())); + } + return m_bv_util.mk_sort(total_width); +} + +sort * bvarray2uf_rewriter_cfg::get_value_sort(expr * e) { + return get_value_sort(m_manager.get_sort(e)); +} + +sort * bvarray2uf_rewriter_cfg::get_value_sort(sort * s) { + SASSERT(s->get_num_parameters() >= 2); + parameter const & p = s->get_parameter(s->get_num_parameters() - 1); + SASSERT(p.is_ast() && is_sort(to_sort(p.get_ast()))); + return to_sort(p.get_ast()); +} + +bool bvarray2uf_rewriter_cfg::is_bv_array(expr * e) { + return is_bv_array(m_manager.get_sort(e)); +} + +bool bvarray2uf_rewriter_cfg::is_bv_array(sort * s) { + if (!m_array_util.is_array(s)) + return false; + + SASSERT(s->get_num_parameters() >= 2); + for (unsigned i = 0; i < s->get_num_parameters(); i++) { + parameter const & p = s->get_parameter(i); + if (!p.is_ast() || !is_sort(to_sort(p.get_ast())) || + !m_bv_util.is_bv_sort(to_sort(p.get_ast()))) + return false; + } + + return true; +} + +func_decl_ref bvarray2uf_rewriter_cfg::mk_uf_for_array(expr * e) { + SASSERT(is_bv_array(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); + bv_f = m_manager.mk_fresh_func_decl("f_t", "", 1, &domain, range); + if (is_uninterp_const(e)) { + if (m_emc) + m_emc->insert(to_app(e)->get_decl(), + m_array_util.mk_as_array(m_manager.get_sort(e), bv_f)); + } + else if (m_fmc) + m_fmc->insert(bv_f); + m_arrays_fs.insert(e, bv_f); + m_manager.inc_ref(bv_f); + } + + return func_decl_ref(bv_f, m_manager); + } +} + +br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + br_status res = BR_FAILED; + + if (m_manager.is_eq(f) && is_bv_array(f->get_domain()[0])) { + 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); + + 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())); + + 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); + res = BR_REWRITE1; + } + else if (f->get_family_id() == null_family_id) { + TRACE("bvarray2uf_rw", tout << "UF APP: " << f->get_name() << std::endl; ); + + bool has_bv_arrays = false; + func_decl_ref f_t(m_manager); + for (unsigned i = 0; i < num; i++) { + if (is_bv_array(args[i])) { + SASSERT(m_array_util.is_as_array(args[i])); + has_bv_arrays = true; + } + } + + expr_ref t(m_manager); + t = m_manager.mk_app(f, num, args); + + if (is_bv_array(t)) { + // From [1]: For every array term t we create a fresh uninterpreted function f_t. + f_t = mk_uf_for_array(t); + result = m_array_util.mk_as_array(m_manager.get_sort(t), f_t); + res = BR_DONE; + } + else if (has_bv_arrays) { + result = t; + res = BR_DONE; + } + else + res = BR_FAILED; + } + else if (m_array_util.get_family_id() == f->get_family_id()) { + TRACE("bvarray2uf_rw", tout << "APP: " << f->get_name() << std::endl; ); + + if (m_array_util.is_select(f)) { + SASSERT(num == 2); + expr * t = args[0]; + expr * i = args[1]; + TRACE("bvarray2uf_rw", tout << + "select; array: " << mk_ismt2_pp(t, m()) << + " index: " << mk_ismt2_pp(i, m()) << std::endl;); + + if (!is_bv_array(t)) + res = BR_FAILED; + else { + // From [1]: Then, we replace terms of the form select(t, i) with f_t(i). + func_decl_ref f_t(mk_uf_for_array(t), m_manager); + result = m_manager.mk_app(f_t, i); + res = BR_DONE; + } + } + else { + if (!is_bv_array(f->get_range())) + res = BR_FAILED; + else { + if (m_array_util.is_const(f)) { + SASSERT(num == 1); + expr_ref t(m_manager.mk_app(f, num, args), m_manager); + expr * v = args[0]; + func_decl_ref f_t(mk_uf_for_array(t), m_manager); + + result = m_array_util.mk_as_array(f->get_range(), f_t); + res = BR_DONE; + + // Add \forall x . f_t(x) = v + sort * sorts[1] = { get_index_sort(f->get_range()) }; + 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()), v); + + expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager); + extra_assertions.push_back(frllx); + } + else if (m_array_util.is_as_array(f)) { + res = BR_FAILED; + } + else if (m_array_util.is_map(f)) { + SASSERT(f->get_num_parameters() == 1); + SASSERT(f->get_parameter(0).is_ast()); + expr_ref t(m_manager.mk_app(f, num, args), m_manager); + func_decl_ref f_t(mk_uf_for_array(t), m_manager); + func_decl_ref map_f(to_func_decl(f->get_parameter(0).get_ast()), m_manager); + + func_decl_ref_vector ss(m_manager); + for (unsigned i = 0; i < num; i++) { + SASSERT(m_array_util.is_array(args[i])); + func_decl_ref fd(mk_uf_for_array(args[i]), m_manager); + ss.push_back(fd); + } + + // Add \forall x . f_t(x) = map_f(a[x], b[x], ...) + sort * sorts[1] = { get_index_sort(f->get_range()) }; + symbol names[1] = { symbol("x") }; + var_ref x(m_manager.mk_var(0, sorts[0]), m_manager); + + expr_ref_vector new_args(m_manager); + for (unsigned i = 0; i < num; i++) + new_args.push_back(m_manager.mk_app(ss[i].get(), x.get())); + + expr_ref body(m_manager); + body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), + m_manager.mk_app(map_f, num, new_args.c_ptr())); + + expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager); + extra_assertions.push_back(frllx); + + result = m_array_util.mk_as_array(f->get_range(), f_t); + res = BR_DONE; + } + else if (m_array_util.is_store(f)) { + SASSERT(num == 3); + expr * s = args[0]; + expr * i = args[1]; + expr * v = args[2]; + TRACE("bvarray2uf_rw", tout << + "store; array: " << mk_ismt2_pp(s, m()) << + " index: " << mk_ismt2_pp(i, m()) << + " value: " << mk_ismt2_pp(v, m()) << std::endl;); + if (!is_bv_array(s)) + res = BR_FAILED; + else { + expr_ref t(m_manager.mk_app(f, num, args), m_manager); + // From [1]: For every term t of the form store(s, i, v), we add the universal + // formula \forall x . x = i \vee f_t(x) = f_s(x), and the ground atom f_t(i) = v. + func_decl_ref f_s(mk_uf_for_array(s), m_manager); + func_decl_ref f_t(mk_uf_for_array(t), m_manager); + + result = m_array_util.mk_as_array(f->get_range(), f_t); + res = BR_DONE; + + sort * sorts[1] = { get_index_sort(f->get_range()) }; + 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_or(m_manager.mk_eq(x, i), + m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), + m_manager.mk_app(f_s, x.get()))); + + expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager); + extra_assertions.push_back(frllx); + + expr_ref ground_atom(m_manager); + ground_atom = m_manager.mk_eq(m_manager.mk_app(f_t, i), v); + extra_assertions.push_back(ground_atom); + TRACE("bvarray2uf_rw", tout << "ground atom: " << mk_ismt2_pp(ground_atom, m()) << std::endl; ); + } + } + else { + NOT_IMPLEMENTED_YET(); + res = BR_FAILED; + } + } + } + } + + CTRACE("bvarray2uf_rw", res==BR_DONE, tout << "result: " << mk_ismt2_pp(result, m()) << std::endl; ); + return res; +} + +bool bvarray2uf_rewriter_cfg::pre_visit(expr * t) +{ + TRACE("bvarray2uf_rw_q", tout << "pre_visit: " << mk_ismt2_pp(t, m()) << std::endl;); + + if (is_quantifier(t)) { + quantifier * q = to_quantifier(t); + TRACE("bvarray2uf_rw_q", tout << "pre_visit quantifier [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m()) << std::endl;); + sort_ref_vector new_bindings(m_manager); + for (unsigned i = 0; i < q->get_num_decls(); i++) + new_bindings.push_back(q->get_decl_sort(i)); + SASSERT(new_bindings.size() == q->get_num_decls()); + m_bindings.append(new_bindings); + } + return true; +} + +bool bvarray2uf_rewriter_cfg::reduce_quantifier(quantifier * old_q, + expr * new_body, + expr * const * new_patterns, + expr * const * new_no_patterns, + expr_ref & result, + proof_ref & result_pr) { + unsigned curr_sz = m_bindings.size(); + SASSERT(old_q->get_num_decls() <= curr_sz); + unsigned num_decls = old_q->get_num_decls(); + unsigned old_sz = curr_sz - num_decls; + string_buffer<> name_buffer; + ptr_buffer new_decl_sorts; + sbuffer new_decl_names; + for (unsigned i = 0; i < num_decls; i++) { + symbol const & n = old_q->get_decl_name(i); + sort * s = old_q->get_decl_sort(i); + + NOT_IMPLEMENTED_YET(); + + } + result = m().mk_quantifier(old_q->is_forall(), new_decl_sorts.size(), new_decl_sorts.c_ptr(), new_decl_names.c_ptr(), + new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(), + old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns); + result_pr = 0; + m_bindings.shrink(old_sz); + TRACE("bvarray2uf_rw_q", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " << + mk_ismt2_pp(old_q->get_expr(), m()) << std::endl << + " new body: " << mk_ismt2_pp(new_body, m()) << std::endl; + tout << "result = " << mk_ismt2_pp(result, m()) << std::endl;); + return true; +} + +bool bvarray2uf_rewriter_cfg::bvarray2uf_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & result_pr) { + if (t->get_idx() >= m_bindings.size()) + return false; + + expr_ref new_exp(m()); + sort * s = t->get_sort(); + + NOT_IMPLEMENTED_YET(); + + result = new_exp; + result_pr = 0; + TRACE("bvarray2uf_rw_q", tout << "reduce_var: " << mk_ismt2_pp(t, m()) << " -> " << mk_ismt2_pp(result, m()) << std::endl;); + return true; +} diff --git a/src/tactic/bv/bvarray2uf_rewriter.h b/src/tactic/bv/bvarray2uf_rewriter.h new file mode 100644 index 000000000..e65340cc3 --- /dev/null +++ b/src/tactic/bv/bvarray2uf_rewriter.h @@ -0,0 +1,87 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + bvarray2uf_rewriter.h + +Abstract: + + Rewriter that rewrites bit-vector arrays into bit-vector + (uninterpreted) functions. + +Author: + + Christoph (cwinter) 2015-11-04 + +Notes: + +--*/ +#ifndef BVARRAY2UF_REWRITER_H_ +#define BVARRAY2UF_REWRITER_H_ + +#include"rewriter_def.h" +#include"extension_model_converter.h" +#include"filter_model_converter.h" + +class bvarray2uf_rewriter_cfg : public default_rewriter_cfg { + ast_manager & m_manager; + expr_ref_vector m_out; + sort_ref_vector m_bindings; + bv_util m_bv_util; + array_util m_array_util; + extension_model_converter * m_emc; + filter_model_converter * m_fmc; + + obj_map m_arrays_fs; + +public: + bvarray2uf_rewriter_cfg(ast_manager & m, params_ref const & p); + ~bvarray2uf_rewriter_cfg(); + + ast_manager & m() const { return m_manager; } + void updt_params(params_ref const & p) {} + + void reset(); + + bool pre_visit(expr * t); + + 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); + + bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr); + + expr_ref_vector extra_assertions; + + void set_mcs(extension_model_converter * emc, filter_model_converter * fmc) { m_emc = emc; m_fmc = fmc; } + +protected: + sort * get_index_sort(expr * e); + sort * get_index_sort(sort * s); + sort * get_value_sort(expr * e); + sort * get_value_sort(sort * s); + bool is_bv_array(expr * e); + bool is_bv_array(sort * e); + func_decl_ref mk_uf_for_array(expr * e); +}; + +template class rewriter_tpl; + +struct bvarray2uf_rewriter : public rewriter_tpl { + bvarray2uf_rewriter_cfg m_cfg; + bvarray2uf_rewriter(ast_manager & m, params_ref const & p) : + rewriter_tpl(m, m.proofs_enabled(), m_cfg), + m_cfg(m, p) { + } + + void set_mcs(extension_model_converter * emc, filter_model_converter * fmc) { m_cfg.set_mcs(emc, fmc); } +}; + +#endif + diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp new file mode 100644 index 000000000..6bf1324f1 --- /dev/null +++ b/src/tactic/bv/bvarray2uf_tactic.cpp @@ -0,0 +1,168 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + bvarray2uf_tactic.cpp + +Abstract: + + Tactic that rewrites bit-vector arrays into bit-vector + (uninterpreted) functions. + +Author: + + Christoph (cwinter) 2015-11-04 + +Notes: + +--*/ +#include"tactical.h" +#include"bv_decl_plugin.h" +#include"expr_replacer.h" +#include"extension_model_converter.h" +#include"filter_model_converter.h" +#include"ast_smt2_pp.h" + +#include"bvarray2uf_tactic.h" +#include"bvarray2uf_rewriter.h" + +class bvarray2uf_tactic : public tactic { + + struct imp { + ast_manager & m_manager; + bool m_produce_models; + bool m_produce_proofs; + bool m_produce_cores; + volatile bool m_cancel; + bvarray2uf_rewriter m_rw; + + ast_manager & m() { return m_manager; } + + imp(ast_manager & m, params_ref const & p) : + m_manager(m), + m_produce_models(false), + m_cancel(false), + m_produce_proofs(false), + m_produce_cores(false), + m_rw(m, p) { + updt_params(p); + } + + void set_cancel(bool f) { + m_cancel = f; + } + + void checkpoint() { + if (m_cancel) + throw tactic_exception(TACTIC_CANCELED_MSG); + } + + void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) + { + 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); ); + m_produce_models = g->models_enabled(); + + if (m_produce_models) { + extension_model_converter * emc = alloc(extension_model_converter, m_manager); + filter_model_converter * fmc = alloc(filter_model_converter, m_manager); + mc = concat(emc, fmc); + m_rw.set_mcs(emc, fmc); + + } + + + m_rw.reset(); + expr_ref new_curr(m_manager); + proof_ref new_pr(m_manager); + 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); + //if (m_produce_proofs) { + // proof * pr = g->pr(idx); + // new_pr = m.mk_modus_ponens(pr, new_pr); + //} + g->update(idx, new_curr, new_pr, g->dep(idx)); + } + + for (unsigned i = 0; i < m_rw.m_cfg.extra_assertions.size(); i++) + g->assert_expr(m_rw.m_cfg.extra_assertions[i].get()); + + g->inc_depth(); + result.push_back(g.get()); + TRACE("bvarray2uf", tout << "After: " << std::endl; g->display(tout);); + SASSERT(g->is_well_sorted()); + } + + void updt_params(params_ref const & p) { + } + }; + + imp * m_imp; + params_ref m_params; + +public: + bvarray2uf_tactic(ast_manager & m, params_ref const & p) : + m_params(p) { + m_imp = alloc(imp, m, p); + } + + virtual tactic * translate(ast_manager & m) { + return alloc(bvarray2uf_tactic, m, m_params); + } + + virtual ~bvarray2uf_tactic() { + dealloc(m_imp); + } + + virtual void updt_params(params_ref const & p) { + m_params = p; + m_imp->updt_params(p); + } + + virtual void collect_param_descrs(param_descrs & r) { + insert_produce_models(r); + } + + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + (*m_imp)(in, result, mc, pc, core); + } + + virtual void cleanup() { + ast_manager & m = m_imp->m(); + imp * d = alloc(imp, m, m_params); + #pragma omp critical (tactic_cancel) + { + std::swap(d, m_imp); + } + dealloc(d); + } + + virtual void set_cancel(bool f) { + if (m_imp) + m_imp->set_cancel(f); + } + +}; + + +tactic * mk_bvarray2uf_tactic(ast_manager & m, params_ref const & p) { + return clean(alloc(bvarray2uf_tactic, m, p)); +} diff --git a/src/tactic/bv/bvarray2uf_tactic.h b/src/tactic/bv/bvarray2uf_tactic.h new file mode 100644 index 000000000..608a831e0 --- /dev/null +++ b/src/tactic/bv/bvarray2uf_tactic.h @@ -0,0 +1,33 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + bvarray2ufbvarray2uf_tactic.h + +Abstract: + + Tactic that rewrites bit-vector arrays into bit-vector + (uninterpreted) functions. + +Author: + + Christoph (cwinter) 2015-11-04 + +Notes: + +--*/ +#ifndef BV_ARRAY2UF_TACTIC_H_ +#define BV_ARRAY2UF_TACTIC_H_ + +#include"params.h" +class ast_manager; +class tactic; + +tactic * mk_bvarray2uf_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("bvarray2uf", "Rewrite bit-vector arrays into bit-vector (uninterpreted) functions.", "mk_bvarray2uf_tactic(m, p)") +*/ + + +#endif \ No newline at end of file