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