1 /*++
2 Copyright (c) 2016 Microsoft Corporation
3 
4 Module Name:
5 
6     enum2bv_rewriter.h
7 
8 Abstract:
9 
10     Conversion from enumeration types to bit-vectors.
11 
12 Author:
13 
14     Nikolaj Bjorner (nbjorner) 2016-10-18
15 
16 Notes:
17 
18 --*/
19 #pragma once
20 
21 #include "ast/datatype_decl_plugin.h"
22 #include "ast/rewriter/rewriter_types.h"
23 #include "ast/expr_functors.h"
24 
25 class enum2bv_rewriter {
26     struct imp;
27     imp* m_imp;
28 public:
29     enum2bv_rewriter(ast_manager & m, params_ref const& p);
30     ~enum2bv_rewriter();
31 
32     void updt_params(params_ref const & p);
33     ast_manager & m() const;
34     unsigned get_num_steps() const;
35     void cleanup();
36     obj_map<func_decl, func_decl*> const& enum2bv() const;
37     obj_map<func_decl, func_decl*> const& bv2enum() const;
38     obj_map<func_decl, expr*> const& enum2def() const;
39     void operator()(expr * e, expr_ref & result, proof_ref & result_proof);
40     void push();
41     void pop(unsigned num_scopes);
42     void flush_side_constraints(expr_ref_vector& side_constraints);
43     unsigned num_translated() const;
44     void set_is_fd(i_sort_pred* sp) const;
45 };
46 
47