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