1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 bvarray2uf_rewriter.h 7 8 Abstract: 9 10 Rewriter that rewrites bit-vector arrays into bit-vector 11 (uninterpreted) functions. 12 13 Author: 14 15 Christoph (cwinter) 2015-11-04 16 17 Notes: 18 19 --*/ 20 #pragma once 21 22 #include "ast/rewriter/rewriter.h" 23 #include "tactic/generic_model_converter.h" 24 25 class bvarray2uf_rewriter_cfg : public default_rewriter_cfg { 26 ast_manager & m_manager; 27 expr_ref_vector m_out; 28 sort_ref_vector m_bindings; 29 bv_util m_bv_util; 30 array_util m_array_util; 31 generic_model_converter * m_fmc; 32 33 obj_map<expr, func_decl*> m_arrays_fs; 34 35 public: 36 bvarray2uf_rewriter_cfg(ast_manager & m, params_ref const & p); 37 ~bvarray2uf_rewriter_cfg(); 38 m()39 ast_manager & m() const { return m_manager; } updt_params(params_ref const & p)40 void updt_params(params_ref const & p) {} 41 42 void reset(); 43 44 bool pre_visit(expr * t); 45 46 br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr); 47 48 bool reduce_quantifier(quantifier * old_q, 49 expr * new_body, 50 expr * const * new_patterns, 51 expr * const * new_no_patterns, 52 expr_ref & result, 53 proof_ref & result_pr); 54 55 bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr); 56 57 expr_ref_vector extra_assertions; 58 set_mcs(generic_model_converter * fmc)59 void set_mcs(generic_model_converter * fmc) { m_fmc = fmc; } 60 61 protected: 62 sort * get_index_sort(expr * e); 63 sort * get_index_sort(sort * s); 64 sort * get_value_sort(expr * e); 65 sort * get_value_sort(sort * s); 66 bool is_bv_array(expr * e); 67 bool is_bv_array(sort * e); 68 func_decl_ref mk_uf_for_array(expr * e); 69 }; 70 71 72 struct bvarray2uf_rewriter : public rewriter_tpl<bvarray2uf_rewriter_cfg> { 73 bvarray2uf_rewriter_cfg m_cfg; bvarray2uf_rewriterbvarray2uf_rewriter74 bvarray2uf_rewriter(ast_manager & m, params_ref const & p) : 75 rewriter_tpl<bvarray2uf_rewriter_cfg>(m, m.proofs_enabled(), m_cfg), 76 m_cfg(m, p) { 77 } 78 set_mcsbvarray2uf_rewriter79 void set_mcs(generic_model_converter * fmc) { m_cfg.set_mcs(fmc); } 80 }; 81 82 83