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