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