1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3 
4 Module Name:
5 
6     bv_elim.h
7 
8 Abstract:
9 
10     Eliminate bit-vectors variables from clauses, by
11     replacing them by bound Boolean variables.
12 
13 Author:
14 
15     Nikolaj Bjorner (nbjorner) 2008-12-16.
16 
17 Revision History:
18 
19 --*/
20 #pragma once
21 
22 #include "ast/ast.h"
23 #include "ast/rewriter/rewriter.h"
24 
25 class bv_elim_cfg : public default_rewriter_cfg {
26     ast_manager& m;
27 public:
bv_elim_cfg(ast_manager & m)28     bv_elim_cfg(ast_manager& m) : m(m) {}
29 
30     bool reduce_quantifier(quantifier * old_q,
31                            expr * new_body,
32                            expr * const * new_patterns,
33                            expr * const * new_no_patterns,
34                            expr_ref & result,
35                            proof_ref & result_pr);
36 };
37 
38 class bv_elim_rw : public rewriter_tpl<bv_elim_cfg> {
39 protected:
40     bv_elim_cfg  m_cfg;
41 public:
bv_elim_rw(ast_manager & m)42     bv_elim_rw(ast_manager & m):
43         rewriter_tpl<bv_elim_cfg>(m, m.proofs_enabled(), m_cfg),
44         m_cfg(m)
45     {}
46 };
47 
48 
49