1 /*++ 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 expr_replacer.h 7 8 Abstract: 9 10 Abstract (functor) for replacing expressions. 11 12 Author: 13 14 Leonardo (leonardo) 2011-04-29 15 16 Notes: 17 18 --*/ 19 #pragma once 20 21 #include "ast/ast.h" 22 #include "ast/expr_substitution.h" 23 #include "util/params.h" 24 25 /** 26 \brief Abstract interface for functors that replace constants with expressions. 27 */ 28 class expr_replacer { 29 struct scoped_set_subst; 30 public: ~expr_replacer()31 virtual ~expr_replacer() {} 32 33 virtual ast_manager & m() const = 0; 34 virtual void set_substitution(expr_substitution * s) = 0; 35 36 virtual void operator()(expr * t, expr_ref & result, proof_ref & result_pr, expr_dependency_ref & deps) = 0; 37 virtual void operator()(expr * t, expr_ref & result, proof_ref & result_pr); 38 virtual void operator()(expr * t, expr_ref & result); operator()39 virtual void operator()(expr_ref & t) { expr_ref s(t, m()); (*this)(s, t); } 40 get_num_steps()41 virtual unsigned get_num_steps() const { return 0; } 42 virtual void reset() = 0; 43 44 void apply_substitution(expr * s, expr * def, proof * def_pr, expr_ref & t); 45 void apply_substitution(expr * s, expr * def, expr_ref & t); 46 }; 47 48 /** 49 \brief Create a vanilla replacer. It just applies the substitution. 50 */ 51 expr_replacer * mk_default_expr_replacer(ast_manager & m, bool proofs_allowed); 52 53 /** 54 \brief Apply substitution and simplify. 55 */ 56 expr_replacer * mk_expr_simp_replacer(ast_manager & m, params_ref const & p = params_ref()); 57 58