1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3
4 Module Name:
5
6 macro_finder.cpp
7
8 Abstract:
9
10 <abstract>
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2010-04-05.
15
16 Revision History:
17
18 --*/
19
20 #include "ast/macros/macro_finder.h"
21 #include "ast/occurs.h"
22 #include "ast/ast_pp.h"
23 #include "ast/ast_ll_pp.h"
24
is_macro(expr * n,app_ref & head,expr_ref & def)25 bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) {
26 if (!is_forall(n))
27 return false;
28 TRACE("macro_finder", tout << "processing: " << mk_pp(n, m) << "\n";);
29 expr * body = to_quantifier(n)->get_expr();
30 unsigned num_decls = to_quantifier(n)->get_num_decls();
31 return m_util.is_simple_macro(body, num_decls, head, def);
32 }
33
34 /**
35 \brief Detect macros of the form
36 1- (forall (X) (= (+ (f X) (R X)) c))
37 2- (forall (X) (<= (+ (f X) (R X)) c))
38 3- (forall (X) (>= (+ (f X) (R X)) c))
39
40 The second and third cases are first converted into
41 (forall (X) (= (f X) (+ c (* -1 (R x)) (k X))))
42 and
43 (forall (X) (<= (k X) 0)) when case 2
44 (forall (X) (>= (k X) 0)) when case 3
45
46 For case 2 & 3, the new quantifiers are stored in new_exprs and new_prs.
47 */
is_arith_macro(expr * n,proof * pr,bool deps_valid,expr_dependency * dep,expr_ref_vector & new_exprs,proof_ref_vector & new_prs,expr_dependency_ref_vector & new_deps)48 bool macro_finder::is_arith_macro(expr * n, proof * pr, bool deps_valid, expr_dependency * dep, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
49 if (!is_forall(n))
50 return false;
51 expr * body = to_quantifier(n)->get_expr();
52 unsigned num_decls = to_quantifier(n)->get_num_decls();
53
54 if (!m_autil.is_le(body) && !m_autil.is_ge(body) && !m.is_eq(body))
55 return false;
56 if (!m_autil.is_add(to_app(body)->get_arg(0)))
57 return false;
58 app_ref head(m);
59 expr_ref def(m);
60 bool inv = false;
61 if (!m_util.is_arith_macro(body, num_decls, head, def, inv))
62 return false;
63 app_ref new_body(m);
64 func_decl * f = head->get_decl();
65 // functions introduced within macros are Skolem functions
66 // To avoid unsound expansion of these as macros (because they
67 // appear in model conversions and are therefore not fully
68 // replacable) we prevent these from being treated as macro functions.
69 if (m_macro_manager.contains(f) || f->is_skolem())
70 return false;
71
72 if (!inv || m.is_eq(body))
73 new_body = m.mk_app(to_app(body)->get_decl(), head, def);
74 else if (m_autil.is_le(body))
75 new_body = m_autil.mk_ge(head, def);
76 else
77 new_body = m_autil.mk_le(head, def);
78
79 quantifier_ref new_q(m);
80 new_q = m.update_quantifier(to_quantifier(n), new_body);
81 proof * new_pr = nullptr;
82 if (m.proofs_enabled()) {
83 proof * rw = m.mk_rewrite(n, new_q);
84 new_pr = m.mk_modus_ponens(pr, rw);
85 }
86 expr_dependency * new_dep = dep;
87 if (m.is_eq(body)) {
88 return m_macro_manager.insert(head->get_decl(), new_q, new_pr, new_dep);
89 }
90 // is ge or le
91 //
92 TRACE("macro_finder", tout << "is_arith_macro: is_ge or is_le " << f->get_name() << "\n";);
93 func_decl * k = m.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range());
94 app * k_app = m.mk_app(k, head->get_num_args(), head->get_args());
95 expr_ref_buffer new_rhs_args(m);
96 expr_ref new_rhs2(m_autil.mk_add(def, k_app), m);
97 expr * body1 = m.mk_eq(head, new_rhs2);
98 expr * body2 = m.mk_app(new_body->get_decl(), k_app, m_autil.mk_int(0));
99 quantifier * q1 = m.update_quantifier(new_q, body1);
100 expr * patterns[1] = { m.mk_pattern(k_app) };
101 quantifier * q2 = m.update_quantifier(new_q, 1, patterns, body2);
102 new_exprs.push_back(q1);
103 new_exprs.push_back(q2);
104 if (m.proofs_enabled()) {
105 // new_pr : new_q
106 // rw : [rewrite] new_q ~ q1 & q2
107 // mp : [modus_pones new_pr rw] q1 & q2
108 // pr1 : [and-elim mp] q1
109 // pr2 : [and-elim mp] q2
110 app * q1q2 = m.mk_and(q1,q2);
111 proof * rw = m.mk_oeq_rewrite(new_q, q1q2);
112 proof * mp = m.mk_modus_ponens(new_pr, rw);
113 proof * pr1 = m.mk_and_elim(mp, 0);
114 proof * pr2 = m.mk_and_elim(mp, 1);
115 new_prs.push_back(pr1);
116 new_prs.push_back(pr2);
117 }
118 if (deps_valid) {
119 new_deps.push_back(new_dep);
120 new_deps.push_back(new_dep);
121 }
122 return true;
123 }
124
is_arith_macro(expr * n,proof * pr,vector<justified_expr> & new_fmls)125 bool macro_finder::is_arith_macro(expr * n, proof * pr, vector<justified_expr>& new_fmls) {
126 if (!is_forall(n))
127 return false;
128 expr * body = to_quantifier(n)->get_expr();
129 unsigned num_decls = to_quantifier(n)->get_num_decls();
130
131 if (!m_autil.is_le(body) && !m_autil.is_ge(body) && !m.is_eq(body))
132 return false;
133 if (!m_autil.is_add(to_app(body)->get_arg(0)))
134 return false;
135 app_ref head(m);
136 expr_ref def(m);
137 bool inv = false;
138 if (!m_util.is_arith_macro(body, num_decls, head, def, inv))
139 return false;
140 app_ref new_body(m);
141 func_decl * f = head->get_decl();
142 if (m_macro_manager.contains(f) || f->is_skolem())
143 return false;
144
145 if (!inv || m.is_eq(body))
146 new_body = m.mk_app(to_app(body)->get_decl(), head, def);
147 else if (m_autil.is_le(body))
148 new_body = m_autil.mk_ge(head, def);
149 else
150 new_body = m_autil.mk_le(head, def);
151
152 quantifier_ref new_q(m);
153 new_q = m.update_quantifier(to_quantifier(n), new_body);
154 proof * new_pr = nullptr;
155 if (m.proofs_enabled()) {
156 proof * rw = m.mk_rewrite(n, new_q);
157 new_pr = m.mk_modus_ponens(pr, rw);
158 }
159 if (m.is_eq(body)) {
160 return m_macro_manager.insert(f, new_q, new_pr);
161 }
162 // is ge or le
163 //
164 TRACE("macro_finder", tout << "is_arith_macro: is_ge or is_le\n";);
165 func_decl * k = m.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range());
166 app * k_app = m.mk_app(k, head->get_num_args(), head->get_args());
167 expr_ref_buffer new_rhs_args(m);
168 expr_ref new_rhs2(m_autil.mk_add(def, k_app), m);
169 expr * body1 = m.mk_eq(head, new_rhs2);
170 expr * body2 = m.mk_app(new_body->get_decl(), k_app, m_autil.mk_int(0));
171 quantifier * q1 = m.update_quantifier(new_q, body1);
172 expr * patterns[1] = { m.mk_pattern(k_app) };
173 quantifier * q2 = m.update_quantifier(new_q, 1, patterns, body2);
174 proof* pr1 = nullptr, *pr2 = nullptr;
175 if (m.proofs_enabled()) {
176 // new_pr : new_q
177 // rw : [rewrite] new_q ~ q1 & q2
178 // mp : [modus_pones new_pr rw] q1 & q2
179 // pr1 : [and-elim mp] q1
180 // pr2 : [and-elim mp] q2
181 app * q1q2 = m.mk_and(q1,q2);
182 proof * rw = m.mk_oeq_rewrite(new_q, q1q2);
183 proof * mp = m.mk_modus_ponens(new_pr, rw);
184 pr1 = m.mk_and_elim(mp, 0);
185 pr2 = m.mk_and_elim(mp, 1);
186 }
187 new_fmls.push_back(justified_expr(m, q1, pr1));
188 new_fmls.push_back(justified_expr(m, q2, pr2));
189 return true;
190 }
191
192 /**
193 n is of the form: (forall (X) (iff (= (f X) t) def[X]))
194
195 Convert it into:
196
197 (forall (X) (= (f X) (ite def[X] t (k X))))
198 (forall (X) (not (= (k X) t)))
199
200 where k is a fresh symbol.
201
202 The new quantifiers and proofs are stored in new_exprs and new_prs
203 */
pseudo_predicate_macro2macro(ast_manager & m,app * head,app * t,expr * def,quantifier * q,proof * pr,bool deps_valid,expr_dependency * dep,expr_ref_vector & new_exprs,proof_ref_vector & new_prs,expr_dependency_ref_vector & new_deps)204 static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, expr * def, quantifier * q, proof * pr, bool deps_valid, expr_dependency * dep,
205 expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps ) {
206 func_decl * f = head->get_decl();
207 func_decl * k = m.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range());
208 app * k_app = m.mk_app(k, head->get_num_args(), head->get_args());
209 app * ite = m.mk_ite(def, t, k_app);
210 app * body_1 = m.mk_eq(head, ite);
211 app * body_2 = m.mk_not(m.mk_eq(k_app, t));
212 quantifier * q1 = m.update_quantifier(q, body_1);
213 expr * pats[1] = { m.mk_pattern(k_app) };
214 quantifier * q2 = m.update_quantifier(q, 1, pats, body_2); // erase patterns
215 new_exprs.push_back(q1);
216 new_exprs.push_back(q2);
217 if (m.proofs_enabled()) {
218 // r : [rewrite] q ~ q1 & q2
219 // pr : q
220 // mp : [modus_pones pr pr1] q1 & q2
221 // pr1 : [and-elim mp] q1
222 // pr2 : [and-elim mp] q2
223 app * q1q2 = m.mk_and(q1,q2);
224 proof * r = m.mk_oeq_rewrite(q, q1q2);
225 proof * mp = m.mk_modus_ponens(pr, r);
226 proof * pr1 = m.mk_and_elim(mp, 0);
227 proof * pr2 = m.mk_and_elim(mp, 1);
228 new_prs.push_back(pr1);
229 new_prs.push_back(pr2);
230 }
231 if (deps_valid) {
232 new_deps.push_back(dep);
233 new_deps.push_back(dep);
234 }
235 }
236
pseudo_predicate_macro2macro(ast_manager & m,app * head,app * t,expr * def,quantifier * q,proof * pr,vector<justified_expr> & new_fmls)237 static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, expr * def, quantifier * q, proof * pr,
238 vector<justified_expr>& new_fmls) {
239 func_decl * f = head->get_decl();
240 func_decl * k = m.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range());
241 app * k_app = m.mk_app(k, head->get_num_args(), head->get_args());
242 app * ite = m.mk_ite(def, t, k_app);
243 app * body_1 = m.mk_eq(head, ite);
244 app * body_2 = m.mk_not(m.mk_eq(k_app, t));
245 quantifier * q1 = m.update_quantifier(q, body_1);
246 proof * pr1 = nullptr, *pr2 = nullptr;
247 expr * pats[1] = { m.mk_pattern(k_app) };
248 quantifier * q2 = m.update_quantifier(q, 1, pats, body_2); // erase patterns
249 if (m.proofs_enabled()) {
250 // r : [rewrite] q ~ q1 & q2
251 // pr : q
252 // mp : [modus_pones pr pr1] q1 & q2
253 // pr1 : [and-elim mp] q1
254 // pr2 : [and-elim mp] q2
255 app * q1q2 = m.mk_and(q1,q2);
256 proof * r = m.mk_oeq_rewrite(q, q1q2);
257 proof * mp = m.mk_modus_ponens(pr, r);
258 pr1 = m.mk_and_elim(mp, 0);
259 pr2 = m.mk_and_elim(mp, 1);
260 }
261 new_fmls.push_back(justified_expr(m, q1, pr1));
262 new_fmls.push_back(justified_expr(m, q2, pr2));
263 }
264
macro_finder(ast_manager & m,macro_manager & mm)265 macro_finder::macro_finder(ast_manager & m, macro_manager & mm):
266 m(m),
267 m_macro_manager(mm),
268 m_util(mm.get_util()),
269 m_autil(m) {
270 }
271
~macro_finder()272 macro_finder::~macro_finder() {
273 }
274
expand_macros(expr_ref_vector const & exprs,proof_ref_vector const & prs,expr_dependency_ref_vector const & deps,expr_ref_vector & new_exprs,proof_ref_vector & new_prs,expr_dependency_ref_vector & new_deps)275 bool macro_finder::expand_macros(expr_ref_vector const& exprs, proof_ref_vector const& prs, expr_dependency_ref_vector const& deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
276 TRACE("macro_finder", tout << "starting expand_macros:\n";
277 m_macro_manager.display(tout););
278 bool found_new_macro = false;
279 unsigned num = exprs.size();
280 bool deps_valid = deps.size() == exprs.size();
281 SASSERT(deps_valid || deps.empty());
282 for (unsigned i = 0; i < num; i++) {
283 expr * n = exprs[i];
284 proof * pr = m.proofs_enabled() ? prs[i] : nullptr;
285 expr_dependency * dep = deps.get(i, nullptr);
286 expr_ref new_n(m), def(m);
287 proof_ref new_pr(m);
288 expr_dependency_ref new_dep(m);
289 m_macro_manager.expand_macros(n, pr, dep, new_n, new_pr, new_dep);
290 app_ref head(m), t(m);
291 if (is_macro(new_n, head, def) && m_macro_manager.insert(head->get_decl(), to_quantifier(new_n.get()), new_pr, new_dep)) {
292 TRACE("macro_finder", tout << "found new macro: " << head->get_decl()->get_name() << "\n" << new_n << "\n";);
293 found_new_macro = true;
294 }
295 else if (is_arith_macro(new_n, new_pr, deps_valid, new_dep, new_exprs, new_prs, new_deps)) {
296 TRACE("macro_finder", tout << "found new arith macro:\n" << new_n << "\n";);
297 found_new_macro = true;
298 }
299 else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) {
300 TRACE("macro_finder", tout << "found new pseudo macro:\n" << head->get_decl()->get_name() << "\n" << t << "\n" << def << "\n";);
301 pseudo_predicate_macro2macro(m, head, t, def, to_quantifier(new_n), new_pr, deps_valid, new_dep, new_exprs, new_prs, new_deps);
302 found_new_macro = true;
303 }
304 else {
305 new_exprs.push_back(new_n);
306 if (m.proofs_enabled())
307 new_prs.push_back(new_pr);
308 if (deps_valid)
309 new_deps.push_back(new_dep);
310 }
311 SASSERT(exprs.size() != deps.size() || new_exprs.size() == new_deps.size());
312 // SASSERT(!m.proofs_enabled() || new_exprs.size() == new_prs.size());
313
314 }
315 return found_new_macro;
316 }
317
operator ()(expr_ref_vector const & exprs,proof_ref_vector const & prs,expr_dependency_ref_vector const & deps,expr_ref_vector & new_exprs,proof_ref_vector & new_prs,expr_dependency_ref_vector & new_deps)318 void macro_finder::operator()(expr_ref_vector const& exprs, proof_ref_vector const & prs, expr_dependency_ref_vector const & deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
319 TRACE("macro_finder", tout << "processing macros...\n";);
320 expr_ref_vector _new_exprs(m);
321 proof_ref_vector _new_prs(m);
322 expr_dependency_ref_vector _new_deps(m);
323 unsigned num = exprs.size();
324 if (expand_macros(exprs, prs, deps, _new_exprs, _new_prs, _new_deps)) {
325 for (unsigned i = 0; i < num; ++i) {
326 expr_ref_vector old_exprs(m);
327 proof_ref_vector old_prs(m);
328 expr_dependency_ref_vector old_deps(m);
329 _new_exprs.swap(old_exprs);
330 _new_prs.swap(old_prs);
331 _new_deps.swap(old_deps);
332 SASSERT(_new_exprs.empty());
333 SASSERT(_new_prs.empty());
334 SASSERT(_new_deps.empty());
335 if (!expand_macros(old_exprs, old_prs, old_deps,
336 _new_exprs, _new_prs, _new_deps))
337 break;
338 }
339 }
340 new_exprs.append(_new_exprs);
341 new_prs.append(_new_prs);
342 new_deps.append(_new_deps);
343 }
344
345
346
expand_macros(unsigned num,justified_expr const * fmls,vector<justified_expr> & new_fmls)347 bool macro_finder::expand_macros(unsigned num, justified_expr const * fmls, vector<justified_expr>& new_fmls) {
348 TRACE("macro_finder", tout << "starting expand_macros:\n";
349 m_macro_manager.display(tout););
350 bool found_new_macro = false;
351 for (unsigned i = 0; i < num; i++) {
352 expr * n = fmls[i].get_fml();
353 proof * pr = m.proofs_enabled() ? fmls[i].get_proof() : nullptr;
354 expr_ref new_n(m), def(m);
355 proof_ref new_pr(m);
356 expr_dependency_ref new_dep(m);
357 m_macro_manager.expand_macros(n, pr, nullptr, new_n, new_pr, new_dep);
358 app_ref head(m), t(m);
359 if (is_macro(new_n, head, def) && m_macro_manager.insert(head->get_decl(), to_quantifier(new_n.get()), new_pr)) {
360 TRACE("macro_finder", tout << "found new macro: " << head->get_decl()->get_name() << "\n" << new_n << "\n";);
361 found_new_macro = true;
362 }
363 else if (is_arith_macro(new_n, new_pr, new_fmls)) {
364 TRACE("macro_finder", tout << "found new arith macro:\n" << new_n << "\n";);
365 found_new_macro = true;
366 }
367 else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) {
368 TRACE("macro_finder", tout << "found new pseudo macro:\n" << head << "\n" << t << "\n" << def << "\n";);
369 pseudo_predicate_macro2macro(m, head, t, def, to_quantifier(new_n), new_pr, new_fmls);
370 found_new_macro = true;
371 }
372 else {
373 new_fmls.push_back(justified_expr(m, new_n, new_pr));
374 }
375 }
376 return found_new_macro;
377 }
378
operator ()(unsigned n,justified_expr const * fmls,vector<justified_expr> & new_fmls)379 void macro_finder::operator()(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls) {
380 TRACE("macro_finder", tout << "processing macros...\n";);
381 vector<justified_expr> _new_fmls;
382 if (expand_macros(n, fmls, _new_fmls)) {
383 while (true) {
384 vector<justified_expr> old_fmls;
385 _new_fmls.swap(old_fmls);
386 SASSERT(_new_fmls.empty());
387 if (!expand_macros(old_fmls.size(), old_fmls.c_ptr(), _new_fmls))
388 break;
389 }
390 }
391 new_fmls.append(_new_fmls);
392 }
393
394
395