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