Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Haniel Barbosa, Mathias Preiner
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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::internal::kind;
21 : :
22 : : namespace cvc5::internal {
23 : :
24 : 752769 : NodeConverter::NodeConverter(NodeManager* nm, bool forceIdem)
25 : 752769 : : d_nm(nm), d_forceIdem(forceIdem)
26 : : {
27 : 752769 : }
28 : :
29 : 42909400 : Node NodeConverter::convert(Node n, bool preserveTypes)
30 : : {
31 [ + + ]: 42909400 : if (n.isNull())
32 : : {
33 : 211 : return n;
34 : : }
35 [ + - ]: 42909200 : Trace("nconv-debug") << "NodeConverter::convert: " << n << std::endl;
36 : 42909200 : std::unordered_map<Node, Node>::iterator it;
37 : 85818300 : std::vector<TNode> visit;
38 : 85818300 : TNode cur;
39 : 42909200 : visit.push_back(n);
40 : 104659000 : do
41 : : {
42 : 147568000 : cur = visit.back();
43 : 147568000 : visit.pop_back();
44 : 147568000 : it = d_cache.find(cur);
45 [ + - ]: 147568000 : Trace("nconv-debug2") << "convert " << cur << std::endl;
46 [ + + ]: 147568000 : if (it == d_cache.end())
47 : : {
48 : 28271300 : d_cache[cur] = Node::null();
49 [ - + ][ - + ]: 28271300 : Assert(d_preCache.find(cur) == d_preCache.end());
[ - - ]
50 : 56542500 : Node curp = preConvert(cur);
51 : : // If curp = cur, then we did not pre-rewrite. Hence, we should not
52 : : // revisit cur, and instead set curp to null.
53 [ + + ]: 28271300 : curp = curp == cur ? Node::null() : curp;
54 : 28271300 : d_preCache[cur] = curp;
55 [ + + ]: 28271300 : if (!curp.isNull())
56 : : {
57 [ + - ]: 48 : Trace("nconv-debug2")
58 : 24 : << "..pre-rewrite changed " << cur << " into " << curp << std::endl;
59 : 48 : AlwaysAssert(!preserveTypes
60 : : || cur.getType().isComparableTo(curp.getType()))
61 : 24 : << "Pre-converting " << cur << " to " << curp << " changes type";
62 : 24 : visit.push_back(cur);
63 : 24 : visit.push_back(curp);
64 : : }
65 : : else
66 : : {
67 [ + + ]: 28271200 : if (!shouldTraverse(cur))
68 : : {
69 : 14529 : addToCache(cur, cur);
70 : : }
71 : : else
72 : : {
73 : 28256700 : visit.push_back(cur);
74 [ + + ]: 28256700 : if (cur.getMetaKind() == metakind::PARAMETERIZED)
75 : : {
76 : 2230550 : visit.push_back(cur.getOperator());
77 : : }
78 : 28256700 : visit.insert(visit.end(), cur.begin(), cur.end());
79 : : }
80 : : }
81 : : }
82 [ + + ]: 119297000 : else if (it->second.isNull())
83 : : {
84 [ + - ]: 28256700 : Trace("nconv-debug2") << "..post-visit " << cur << std::endl;
85 : 28256700 : it = d_preCache.find(cur);
86 [ - + ][ - + ]: 28256700 : Assert(it != d_preCache.end());
[ - - ]
87 [ + + ]: 28256700 : if (!it->second.isNull())
88 : : {
89 : : // it converts to what its prewrite converts to
90 [ - + ][ - + ]: 24 : Assert(d_cache.find(it->second) != d_cache.end());
[ - - ]
91 : 24 : Node ret = d_cache[it->second];
92 : 24 : addToCache(cur, ret);
93 [ + - ]: 48 : Trace("nconv-debug2")
94 : 24 : << "..from cache changed " << cur << " into " << ret << std::endl;
95 : : }
96 : : else
97 : : {
98 : 56513400 : Node ret = cur;
99 : 28256700 : bool childChanged = false;
100 : 28256700 : std::vector<Node> children;
101 [ + + ]: 28256700 : if (ret.getMetaKind() == metakind::PARAMETERIZED)
102 : : {
103 : 2230550 : it = d_cache.find(ret.getOperator());
104 [ - + ][ - + ]: 2230550 : Assert(it != d_cache.end());
[ - - ]
105 [ - + ][ - + ]: 2230550 : Assert(!it->second.isNull());
[ - - ]
106 [ + - ][ + + ]: 2230550 : childChanged = childChanged || ret.getOperator() != it->second;
[ + - ][ - - ]
107 : 2230550 : children.push_back(it->second);
108 : : }
109 [ + + ]: 102428000 : for (const Node& cn : ret)
110 : : {
111 : 74171600 : it = d_cache.find(cn);
112 [ - + ][ - + ]: 74171600 : Assert(it != d_cache.end());
[ - - ]
113 [ - + ][ - + ]: 74171600 : Assert(!it->second.isNull());
[ - - ]
114 [ + + ][ + + ]: 74171600 : childChanged = childChanged || cn != it->second;
115 : 74171600 : children.push_back(it->second);
116 : : }
117 [ + - ]: 28256700 : if (preserveTypes)
118 : : {
119 [ + + ]: 28256700 : if (childChanged)
120 : : {
121 : 4712910 : ret = d_nm->mkNode(ret.getKind(), children);
122 [ + - ]: 9425820 : Trace("nconv-debug2") << "..from children changed " << cur
123 : 4712910 : << " into " << ret << std::endl;
124 : : }
125 : : // run the callback for the current application
126 : 56513400 : Node cret = postConvert(ret);
127 [ + + ][ + + ]: 28256700 : if (!cret.isNull() && ret != cret)
[ + + ]
128 : : {
129 [ - + ][ - - ]: 2680380 : AlwaysAssert(cret.getType().isComparableTo(ret.getType()))
130 : 1340190 : << "Converting " << ret << " to " << cret << " changes type";
131 [ + - ]: 2680380 : Trace("nconv-debug2") << "..post-rewrite changed " << ret
132 : 1340190 : << " into " << cret << std::endl;
133 : 1340190 : ret = cret;
134 : : }
135 : : }
136 : : else
137 : : {
138 : : // use the untyped version
139 : 0 : Node cret = postConvertUntyped(cur, children, childChanged);
140 [ - - ]: 0 : if (!cret.isNull())
141 : : {
142 : 0 : ret = cret;
143 : : }
144 : : }
145 : 28256700 : addToCache(cur, ret);
146 : : }
147 : : }
148 [ + + ]: 147568000 : } while (!visit.empty());
149 [ - + ][ - + ]: 42909200 : Assert(d_cache.find(n) != d_cache.end());
[ - - ]
150 [ - + ][ - + ]: 42909200 : Assert(!d_cache.find(n)->second.isNull());
[ - - ]
151 : 42909200 : return d_cache[n];
152 : : }
153 : :
154 : 83816 : TypeNode NodeConverter::convertType(TypeNode tn)
155 : : {
156 [ - + ]: 83816 : if (tn.isNull())
157 : : {
158 : 0 : return tn;
159 : : }
160 [ + - ]: 83816 : Trace("nconv-debug") << "NodeConverter::convertType: " << tn << std::endl;
161 : 83816 : std::unordered_map<TypeNode, TypeNode>::iterator it;
162 : 167632 : std::vector<TypeNode> visit;
163 : 167632 : TypeNode cur;
164 : 83816 : visit.push_back(tn);
165 : 11528 : do
166 : : {
167 : 95344 : cur = visit.back();
168 : 95344 : visit.pop_back();
169 : 95344 : it = d_tcache.find(cur);
170 [ + - ]: 95344 : Trace("nconv-debug2") << "convert type " << cur << std::endl;
171 [ + + ]: 95344 : if (it == d_tcache.end())
172 : : {
173 : 7924 : d_tcache[cur] = TypeNode::null();
174 [ - + ][ - + ]: 7924 : Assert(d_preTCache.find(cur) == d_preTCache.end());
[ - - ]
175 : 15848 : TypeNode curp = preConvertType(cur);
176 : : // if curp = cur, set null to avoid infinite loop
177 [ + - ]: 7924 : curp = curp == cur ? TypeNode::null() : curp;
178 : 7924 : d_preTCache[cur] = curp;
179 [ - + ]: 7924 : if (!curp.isNull())
180 : : {
181 : 0 : visit.push_back(cur);
182 : 0 : visit.push_back(curp);
183 : : }
184 : : else
185 : : {
186 [ + + ]: 7924 : if (cur.getNumChildren() == 0)
187 : : {
188 : 4783 : TypeNode ret = postConvertType(cur);
189 : 4783 : addToTypeCache(cur, ret);
190 : : }
191 : : else
192 : : {
193 : 3141 : visit.push_back(cur);
194 : 3141 : visit.insert(visit.end(), cur.begin(), cur.end());
195 : : }
196 : : }
197 : : }
198 [ + + ]: 87420 : else if (it->second.isNull())
199 : : {
200 : 3141 : it = d_preTCache.find(cur);
201 [ - + ][ - + ]: 3141 : Assert(it != d_preTCache.end());
[ - - ]
202 [ - + ]: 3141 : if (!it->second.isNull())
203 : : {
204 : : // it converts to what its prewrite converts to
205 : 0 : Assert(d_tcache.find(it->second) != d_tcache.end());
206 : 0 : TypeNode ret = d_tcache[it->second];
207 : 0 : addToTypeCache(cur, ret);
208 : : }
209 : : else
210 : : {
211 : 6282 : TypeNode ret = cur;
212 : : // reconstruct using a node builder, which seems to be required for
213 : : // type nodes.
214 : 6282 : NodeBuilder nb(d_nm, ret.getKind());
215 : : // there are no parameterized types
216 [ - + ][ - + ]: 3141 : Assert (ret.getMetaKind() != kind::metakind::PARAMETERIZED);
[ - - ]
217 : 11528 : for (TypeNode::const_iterator j = ret.begin(), iend = ret.end();
218 [ + + ]: 11528 : j != iend;
219 : 8387 : ++j)
220 : : {
221 : 8387 : it = d_tcache.find(*j);
222 [ - + ][ - + ]: 8387 : Assert(it != d_tcache.end());
[ - - ]
223 [ - + ][ - + ]: 8387 : Assert(!it->second.isNull());
[ - - ]
224 : 8387 : nb << it->second;
225 : : }
226 : : // construct the type node
227 : 3141 : ret = nb.constructTypeNode();
228 [ + - ]: 3141 : Trace("nconv-debug") << cur << " <- " << ret << std::endl;
229 : : // run the callback for the current application
230 : 3141 : TypeNode cret = postConvertType(ret);
231 [ + - ]: 3141 : if (!cret.isNull())
232 : : {
233 : 3141 : ret = cret;
234 : : }
235 [ + - ]: 6282 : Trace("nconv-debug")
236 : 3141 : << cur << " <- " << ret << " (post-convert)" << std::endl;
237 : 3141 : addToTypeCache(cur, ret);
238 : : }
239 : : }
240 [ + + ]: 95344 : } while (!visit.empty());
241 [ - + ][ - + ]: 83816 : Assert(d_tcache.find(tn) != d_tcache.end());
[ - - ]
242 [ - + ][ - + ]: 83816 : Assert(!d_tcache.find(tn)->second.isNull());
[ - - ]
243 [ + - ]: 167632 : Trace("nconv-debug") << "NodeConverter::convertType: returns " << d_tcache[tn]
244 : 83816 : << std::endl;
245 : 83816 : return d_tcache[tn];
246 : : }
247 : :
248 : 28271300 : void NodeConverter::addToCache(TNode cur, TNode ret)
249 : : {
250 : 28271300 : d_cache[cur] = ret;
251 : : // also force idempotency, if specified
252 [ + - ]: 28271300 : if (d_forceIdem)
253 : : {
254 : 28271300 : d_cache[ret] = ret;
255 : : }
256 : 28271300 : }
257 : 7924 : void NodeConverter::addToTypeCache(TypeNode cur, TypeNode ret)
258 : : {
259 : 7924 : d_tcache[cur] = ret;
260 : : // also force idempotency, if specified
261 [ + - ]: 7924 : if (d_forceIdem)
262 : : {
263 : 7924 : d_tcache[ret] = ret;
264 : : }
265 : 7924 : }
266 : :
267 : 24076200 : Node NodeConverter::preConvert(Node n) { return n; }
268 : 0 : Node NodeConverter::postConvert(Node n) { return n; }
269 : :
270 : 0 : Node NodeConverter::postConvertUntyped(Node orig,
271 : : const std::vector<Node>& terms,
272 : : bool termsChanged)
273 : : {
274 : 0 : return orig;
275 : : }
276 : :
277 : 1295 : TypeNode NodeConverter::preConvertType(TypeNode tn) { return tn; }
278 : 1293 : TypeNode NodeConverter::postConvertType(TypeNode tn) { return tn; }
279 : 23925100 : bool NodeConverter::shouldTraverse(Node n) { return true; }
280 : :
281 : : } // namespace cvc5::internal
|
