1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 expr_replacer.cpp
7
8 Abstract:
9
10 Abstract (functor) for replacing constants with expressions.
11
12 Author:
13
14 Leonardo (leonardo) 2011-04-29
15
16 Notes:
17
18 --*/
19 #include "ast/rewriter/expr_replacer.h"
20 #include "ast/rewriter/rewriter_def.h"
21 #include "ast/rewriter/th_rewriter.h"
22
operator ()(expr * t,expr_ref & result,proof_ref & result_pr)23 void expr_replacer::operator()(expr * t, expr_ref & result, proof_ref & result_pr) {
24 expr_dependency_ref result_dep(m());
25 operator()(t, result, result_pr, result_dep);
26 }
27
operator ()(expr * t,expr_ref & result)28 void expr_replacer::operator()(expr * t, expr_ref & result) {
29 proof_ref pr(m());
30 operator()(t, result, pr);
31 }
32
33 struct expr_replacer::scoped_set_subst {
34 expr_replacer & m_r;
scoped_set_substexpr_replacer::scoped_set_subst35 scoped_set_subst(expr_replacer & r, expr_substitution & s):m_r(r) { m_r.set_substitution(&s); }
~scoped_set_substexpr_replacer::scoped_set_subst36 ~scoped_set_subst() { m_r.set_substitution(nullptr); }
37 };
38
apply_substitution(expr * s,expr * def,proof * def_pr,expr_ref & t)39 void expr_replacer::apply_substitution(expr * s, expr * def, proof * def_pr, expr_ref & t) {
40 expr_substitution sub(m());
41 sub.insert(s, def, def_pr);
42 scoped_set_subst set(*this, sub);
43 (*this)(t);
44 }
45
apply_substitution(expr * s,expr * def,expr_ref & t)46 void expr_replacer::apply_substitution(expr * s, expr * def, expr_ref & t) {
47 expr_substitution sub(m());
48 sub.insert(s, def);
49 scoped_set_subst set(*this, sub);
50 (*this)(t);
51 }
52
53 struct default_expr_replacer_cfg : public default_rewriter_cfg {
54 ast_manager & m;
55 expr_substitution * m_subst;
56 expr_dependency_ref m_used_dependencies;
57
default_expr_replacer_cfgdefault_expr_replacer_cfg58 default_expr_replacer_cfg(ast_manager & _m):
59 m(_m),
60 m_subst(nullptr),
61 m_used_dependencies(_m) {
62 }
63
get_substdefault_expr_replacer_cfg64 bool get_subst(expr * s, expr * & t, proof * & pr) {
65 if (m_subst == nullptr)
66 return false;
67 expr_dependency * d = nullptr;
68 if (m_subst->find(s, t, pr, d)) {
69 m_used_dependencies = m.mk_join(m_used_dependencies, d);
70 return true;
71 }
72 return false;
73 }
74
max_steps_exceededdefault_expr_replacer_cfg75 bool max_steps_exceeded(unsigned num_steps) const {
76 return false;
77 }
78 };
79
80 template class rewriter_tpl<default_expr_replacer_cfg>;
81
82 class default_expr_replacer : public expr_replacer {
83 default_expr_replacer_cfg m_cfg;
84 rewriter_tpl<default_expr_replacer_cfg> m_replacer;
85 public:
default_expr_replacer(ast_manager & m,bool proofs_enabled)86 default_expr_replacer(ast_manager & m, bool proofs_enabled):
87 m_cfg(m),
88 m_replacer(m, m.proofs_enabled() && proofs_enabled, m_cfg) {
89 }
90
m() const91 ast_manager & m() const override { return m_replacer.m(); }
92
set_substitution(expr_substitution * s)93 void set_substitution(expr_substitution * s) override {
94 m_replacer.cleanup();
95 m_replacer.cfg().m_subst = s;
96 }
97
operator ()(expr * t,expr_ref & result,proof_ref & result_pr,expr_dependency_ref & result_dep)98 void operator()(expr * t, expr_ref & result, proof_ref & result_pr, expr_dependency_ref & result_dep) override {
99 result_dep = nullptr;
100 m_replacer.operator()(t, result, result_pr);
101 if (m_cfg.m_used_dependencies != 0) {
102 result_dep = m_cfg.m_used_dependencies;
103 m_replacer.reset(); // reset cache
104 m_cfg.m_used_dependencies = nullptr;
105 }
106 }
107
108
get_num_steps() const109 unsigned get_num_steps() const override {
110 return m_replacer.get_num_steps();
111 }
112
reset()113 void reset() override {
114 m_replacer.reset();
115 }
116 };
117
mk_default_expr_replacer(ast_manager & m,bool proofs_allowed)118 expr_replacer * mk_default_expr_replacer(ast_manager & m, bool proofs_allowed) {
119 return alloc(default_expr_replacer, m, proofs_allowed);
120 }
121
122 /**
123 \brief Adapter for using th_rewriter as an expr_replacer.
124 */
125 class th_rewriter2expr_replacer : public expr_replacer {
126 th_rewriter m_r;
127 public:
th_rewriter2expr_replacer(ast_manager & m,params_ref const & p)128 th_rewriter2expr_replacer(ast_manager & m, params_ref const & p):
129 m_r(m, p) {
130 }
131
~th_rewriter2expr_replacer()132 ~th_rewriter2expr_replacer() override {}
133
m() const134 ast_manager & m() const override { return m_r.m(); }
135
set_substitution(expr_substitution * s)136 void set_substitution(expr_substitution * s) override { m_r.set_substitution(s); }
137
operator ()(expr * t,expr_ref & result,proof_ref & result_pr,expr_dependency_ref & result_dep)138 void operator()(expr * t, expr_ref & result, proof_ref & result_pr, expr_dependency_ref & result_dep) override {
139 m_r(t, result, result_pr);
140 result_dep = m_r.get_used_dependencies();
141 m_r.reset_used_dependencies();
142 }
143
get_num_steps() const144 unsigned get_num_steps() const override {
145 return m_r.get_num_steps();
146 }
147
reset()148 void reset() override {
149 m_r.reset();
150 }
151
152 };
153
mk_expr_simp_replacer(ast_manager & m,params_ref const & p)154 expr_replacer * mk_expr_simp_replacer(ast_manager & m, params_ref const & p) {
155 return alloc(th_rewriter2expr_replacer, m, p);
156 }
157