1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 elim_term_ite.h 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2008-06-12. 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 #include "ast/normal_forms/defined_names.h" 22 #include "ast/rewriter/rewriter.h" 23 #include "ast/justified_expr.h" 24 25 class elim_term_ite_cfg : public default_rewriter_cfg { 26 ast_manager& m; 27 defined_names & m_defined_names; 28 vector<justified_expr> m_new_defs; 29 unsigned_vector m_lim; 30 public: elim_term_ite_cfg(ast_manager & m,defined_names & d)31 elim_term_ite_cfg(ast_manager & m, defined_names & d): m(m), m_defined_names(d) { 32 // TBD enable_ac_support(false); 33 } ~elim_term_ite_cfg()34 virtual ~elim_term_ite_cfg() {} new_defs()35 vector<justified_expr> const& new_defs() const { return m_new_defs; } 36 br_status reduce_app(func_decl* f, unsigned n, expr *const* args, expr_ref& result, proof_ref& result_pr); push()37 void push() { m_lim.push_back(m_new_defs.size()); } pop(unsigned n)38 void pop(unsigned n) {if (n > 0) { m_new_defs.shrink(m_lim[m_lim.size() - n]); m_lim.shrink(m_lim.size() - n); } } 39 }; 40 41 class elim_term_ite_rw : public rewriter_tpl<elim_term_ite_cfg> { 42 elim_term_ite_cfg m_cfg; 43 public: elim_term_ite_rw(ast_manager & m,defined_names & dn)44 elim_term_ite_rw(ast_manager& m, defined_names & dn): 45 rewriter_tpl<elim_term_ite_cfg>(m, m.proofs_enabled(), m_cfg), 46 m_cfg(m, dn) 47 {} new_defs()48 vector<justified_expr> const& new_defs() const { return m_cfg.new_defs(); } push()49 void push() { m_cfg.push(); } pop(unsigned n)50 void pop(unsigned n) { m_cfg.pop(n); } 51 }; 52 53 54 55 56