1 /*++
2 Copyright (c) 2019 Microsoft Corporation
3
4 Module Name:
5
6 func_decl_replace.cpp
7
8 Abstract:
9
10 Replace functions in expressions.
11
12 Author:
13
14 Nikolaj Bjorner (nbjorner) 2019-03-28
15
16 Revision History:
17
18
19 --*/
20
21
22 #include "ast/rewriter/func_decl_replace.h"
23
operator ()(expr * e)24 expr_ref func_decl_replace::operator()(expr* e) {
25 m_todo.push_back(e);
26
27 while (!m_todo.empty()) {
28 expr* a = m_todo.back(), *b;
29 if (m_cache.contains(a)) {
30 m_todo.pop_back();
31 }
32 else if (is_var(a)) {
33 m_cache.insert(a, a);
34 m_todo.pop_back();
35 }
36 else if (is_app(a)) {
37 app* c = to_app(a);
38 unsigned n = c->get_num_args();
39 m_args.reset();
40 bool arg_differs = false;
41 for (unsigned i = 0; i < n; ++i) {
42 expr* d = nullptr, *arg = c->get_arg(i);
43 if (m_cache.find(arg, d)) {
44 m_args.push_back(d);
45 arg_differs |= arg != d;
46 SASSERT(arg->get_sort() == d->get_sort());
47 }
48 else {
49 m_todo.push_back(arg);
50 }
51 }
52 if (m_args.size() == n) {
53 if (arg_differs) {
54 b = m.mk_app(c->get_decl(), m_args.size(), m_args.data());
55 m_refs.push_back(b);
56 SASSERT(a->get_sort() == b->get_sort());
57 } else {
58 b = a;
59 }
60 func_decl* f = nullptr;
61 if (m_subst.find(c->get_decl(), f)) {
62 b = m.mk_app(f, m_args.size(), m_args.data());
63 m_refs.push_back(b);
64 }
65 m_cache.insert(a, b);
66 m_todo.pop_back();
67 }
68 }
69 else {
70 quantifier* q = to_quantifier(a);
71 SASSERT(is_quantifier(a));
72 expr* body = q->get_expr(), *new_body;
73 if (m_cache.find(body, new_body)) {
74 if (new_body == body) {
75 b = a;
76 }
77 else {
78 b = m.update_quantifier(q, new_body);
79 m_refs.push_back(b);
80 }
81 m_cache.insert(a, b);
82 m_todo.pop_back();
83 }
84 else {
85 m_todo.push_back(body);
86 }
87 }
88 }
89 return expr_ref(m_cache.find(e), m);
90 }
91
reset()92 void func_decl_replace::reset() {
93 m_cache.reset();
94 m_subst.reset();
95 m_refs.reset();
96 m_funs.reset();
97 }
98