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