1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Node converter utility |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "expr/node_converter.h" |
17 |
|
|
18 |
|
#include "expr/attribute.h" |
19 |
|
|
20 |
|
using namespace cvc5::kind; |
21 |
|
|
22 |
|
namespace cvc5 { |
23 |
|
|
24 |
1 |
NodeConverter::NodeConverter(bool forceIdem) : d_forceIdem(forceIdem) {} |
25 |
|
|
26 |
144 |
Node NodeConverter::convert(Node n) |
27 |
|
{ |
28 |
144 |
if (n.isNull()) |
29 |
|
{ |
30 |
|
return n; |
31 |
|
} |
32 |
144 |
Trace("nconv-debug") << "NodeConverter::convert: " << n << std::endl; |
33 |
144 |
NodeManager* nm = NodeManager::currentNM(); |
34 |
144 |
std::unordered_map<Node, Node>::iterator it; |
35 |
288 |
std::vector<TNode> visit; |
36 |
288 |
TNode cur; |
37 |
144 |
visit.push_back(n); |
38 |
209 |
do |
39 |
|
{ |
40 |
353 |
cur = visit.back(); |
41 |
353 |
visit.pop_back(); |
42 |
353 |
it = d_cache.find(cur); |
43 |
353 |
Trace("nconv-debug2") << "convert " << cur << std::endl; |
44 |
353 |
if (it == d_cache.end()) |
45 |
|
{ |
46 |
80 |
d_cache[cur] = Node::null(); |
47 |
80 |
Assert(d_preCache.find(cur) == d_preCache.end()); |
48 |
160 |
Node curp = preConvert(cur); |
49 |
|
// If curp = cur, then we did not pre-rewrite. Hence, we should not |
50 |
|
// revisit cur, and instead set curp to null. |
51 |
80 |
curp = curp == cur ? Node::null() : curp; |
52 |
80 |
d_preCache[cur] = curp; |
53 |
80 |
if (!curp.isNull()) |
54 |
|
{ |
55 |
|
visit.push_back(cur); |
56 |
|
visit.push_back(curp); |
57 |
|
} |
58 |
|
else |
59 |
|
{ |
60 |
80 |
if (!shouldTraverse(cur)) |
61 |
|
{ |
62 |
|
addToCache(cur, cur); |
63 |
|
} |
64 |
|
else |
65 |
|
{ |
66 |
80 |
visit.push_back(cur); |
67 |
80 |
if (cur.getMetaKind() == metakind::PARAMETERIZED) |
68 |
|
{ |
69 |
2 |
visit.push_back(cur.getOperator()); |
70 |
|
} |
71 |
80 |
visit.insert(visit.end(), cur.begin(), cur.end()); |
72 |
|
} |
73 |
|
} |
74 |
|
} |
75 |
273 |
else if (it->second.isNull()) |
76 |
|
{ |
77 |
80 |
it = d_preCache.find(cur); |
78 |
80 |
Assert(it != d_preCache.end()); |
79 |
80 |
if (!it->second.isNull()) |
80 |
|
{ |
81 |
|
// it converts to what its prewrite converts to |
82 |
|
Assert(d_cache.find(it->second) != d_cache.end()); |
83 |
|
Node ret = d_cache[it->second]; |
84 |
|
addToCache(cur, ret); |
85 |
|
} |
86 |
|
else |
87 |
|
{ |
88 |
160 |
Node ret = cur; |
89 |
80 |
bool childChanged = false; |
90 |
160 |
std::vector<Node> children; |
91 |
80 |
if (ret.getMetaKind() == metakind::PARAMETERIZED) |
92 |
|
{ |
93 |
2 |
it = d_cache.find(ret.getOperator()); |
94 |
2 |
Assert(it != d_cache.end()); |
95 |
2 |
Assert(!it->second.isNull()); |
96 |
2 |
childChanged = childChanged || ret.getOperator() != it->second; |
97 |
2 |
children.push_back(it->second); |
98 |
|
} |
99 |
207 |
for (const Node& cn : ret) |
100 |
|
{ |
101 |
127 |
it = d_cache.find(cn); |
102 |
127 |
Assert(it != d_cache.end()); |
103 |
127 |
Assert(!it->second.isNull()); |
104 |
127 |
childChanged = childChanged || cn != it->second; |
105 |
127 |
children.push_back(it->second); |
106 |
|
} |
107 |
80 |
if (childChanged) |
108 |
|
{ |
109 |
63 |
ret = nm->mkNode(ret.getKind(), children); |
110 |
|
} |
111 |
|
// run the callback for the current application |
112 |
160 |
Node cret = postConvert(ret); |
113 |
80 |
if (!cret.isNull() && ret != cret) |
114 |
|
{ |
115 |
84 |
AlwaysAssert(cret.getType().isComparableTo(ret.getType())) |
116 |
42 |
<< "Converting " << ret << " to " << cret << " changes type"; |
117 |
42 |
ret = cret; |
118 |
|
} |
119 |
80 |
addToCache(cur, ret); |
120 |
|
} |
121 |
|
} |
122 |
353 |
} while (!visit.empty()); |
123 |
144 |
Assert(d_cache.find(n) != d_cache.end()); |
124 |
144 |
Assert(!d_cache.find(n)->second.isNull()); |
125 |
144 |
return d_cache[n]; |
126 |
|
} |
127 |
|
|
128 |
6 |
TypeNode NodeConverter::convertType(TypeNode tn) |
129 |
|
{ |
130 |
6 |
if (tn.isNull()) |
131 |
|
{ |
132 |
|
return tn; |
133 |
|
} |
134 |
6 |
Trace("nconv-debug") << "NodeConverter::convertType: " << tn << std::endl; |
135 |
6 |
std::unordered_map<TypeNode, TypeNode>::iterator it; |
136 |
12 |
std::vector<TypeNode> visit; |
137 |
12 |
TypeNode cur; |
138 |
6 |
visit.push_back(tn); |
139 |
3 |
do |
140 |
|
{ |
141 |
9 |
cur = visit.back(); |
142 |
9 |
visit.pop_back(); |
143 |
9 |
it = d_tcache.find(cur); |
144 |
9 |
Trace("nconv-debug2") << "convert type " << cur << std::endl; |
145 |
9 |
if (it == d_tcache.end()) |
146 |
|
{ |
147 |
3 |
d_tcache[cur] = TypeNode::null(); |
148 |
3 |
Assert(d_preTCache.find(cur) == d_preTCache.end()); |
149 |
6 |
TypeNode curp = preConvertType(cur); |
150 |
|
// if curp = cur, set null to avoid infinite loop |
151 |
3 |
curp = curp == cur ? TypeNode::null() : curp; |
152 |
3 |
d_preTCache[cur] = curp; |
153 |
3 |
if (!curp.isNull()) |
154 |
|
{ |
155 |
|
visit.push_back(cur); |
156 |
|
visit.push_back(curp); |
157 |
|
} |
158 |
|
else |
159 |
|
{ |
160 |
3 |
curp = curp.isNull() ? cur : curp; |
161 |
3 |
if (cur.getNumChildren() == 0) |
162 |
|
{ |
163 |
4 |
TypeNode ret = postConvertType(cur); |
164 |
2 |
addToTypeCache(cur, ret); |
165 |
|
} |
166 |
|
else |
167 |
|
{ |
168 |
1 |
visit.push_back(cur); |
169 |
1 |
visit.insert(visit.end(), cur.begin(), cur.end()); |
170 |
|
} |
171 |
|
} |
172 |
|
} |
173 |
6 |
else if (it->second.isNull()) |
174 |
|
{ |
175 |
1 |
it = d_preTCache.find(cur); |
176 |
1 |
Assert(it != d_preTCache.end()); |
177 |
1 |
if (!it->second.isNull()) |
178 |
|
{ |
179 |
|
// it converts to what its prewrite converts to |
180 |
|
Assert(d_tcache.find(it->second) != d_tcache.end()); |
181 |
|
TypeNode ret = d_tcache[it->second]; |
182 |
|
addToTypeCache(cur, ret); |
183 |
|
} |
184 |
|
else |
185 |
|
{ |
186 |
2 |
TypeNode ret = cur; |
187 |
|
// reconstruct using a node builder, which seems to be required for |
188 |
|
// type nodes. |
189 |
2 |
NodeBuilder nb(ret.getKind()); |
190 |
1 |
if (ret.getMetaKind() == kind::metakind::PARAMETERIZED) |
191 |
|
{ |
192 |
|
// push the operator |
193 |
|
nb << ret.getOperator(); |
194 |
|
} |
195 |
3 |
for (TypeNode::const_iterator j = ret.begin(), iend = ret.end(); |
196 |
3 |
j != iend; |
197 |
|
++j) |
198 |
|
{ |
199 |
2 |
it = d_tcache.find(*j); |
200 |
2 |
Assert(it != d_tcache.end()); |
201 |
2 |
Assert(!it->second.isNull()); |
202 |
2 |
nb << it->second; |
203 |
|
} |
204 |
|
// construct the type node |
205 |
1 |
ret = nb.constructTypeNode(); |
206 |
1 |
Trace("nconv-debug") << cur << " <- " << ret << std::endl; |
207 |
|
// run the callback for the current application |
208 |
2 |
TypeNode cret = postConvertType(ret); |
209 |
1 |
if (!cret.isNull()) |
210 |
|
{ |
211 |
1 |
ret = cret; |
212 |
|
} |
213 |
2 |
Trace("nconv-debug") |
214 |
1 |
<< cur << " <- " << ret << " (post-convert)" << std::endl; |
215 |
1 |
addToTypeCache(cur, ret); |
216 |
|
} |
217 |
|
} |
218 |
9 |
} while (!visit.empty()); |
219 |
6 |
Assert(d_tcache.find(tn) != d_tcache.end()); |
220 |
6 |
Assert(!d_tcache.find(tn)->second.isNull()); |
221 |
12 |
Trace("nconv-debug") << "NodeConverter::convertType: returns " << d_tcache[tn] |
222 |
6 |
<< std::endl; |
223 |
6 |
return d_tcache[tn]; |
224 |
|
} |
225 |
|
|
226 |
80 |
void NodeConverter::addToCache(TNode cur, TNode ret) |
227 |
|
{ |
228 |
80 |
d_cache[cur] = ret; |
229 |
|
// also force idempotency, if specified |
230 |
80 |
if (d_forceIdem) |
231 |
|
{ |
232 |
80 |
d_cache[ret] = ret; |
233 |
|
} |
234 |
80 |
} |
235 |
3 |
void NodeConverter::addToTypeCache(TypeNode cur, TypeNode ret) |
236 |
|
{ |
237 |
3 |
d_tcache[cur] = ret; |
238 |
|
// also force idempotency, if specified |
239 |
3 |
if (d_forceIdem) |
240 |
|
{ |
241 |
3 |
d_tcache[ret] = ret; |
242 |
|
} |
243 |
3 |
} |
244 |
|
|
245 |
80 |
Node NodeConverter::preConvert(Node n) { return Node::null(); } |
246 |
|
Node NodeConverter::postConvert(Node n) { return Node::null(); } |
247 |
|
|
248 |
3 |
TypeNode NodeConverter::preConvertType(TypeNode tn) { return TypeNode::null(); } |
249 |
|
TypeNode NodeConverter::postConvertType(TypeNode tn) |
250 |
|
{ |
251 |
|
return TypeNode::null(); |
252 |
|
} |
253 |
|
bool NodeConverter::shouldTraverse(Node n) { return true; } |
254 |
|
|
255 |
31125 |
} // namespace cvc5 |