Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : * Common algorithms on nodes.
10 : : *
11 : : * This file implements common algorithms applied to nodes, such as checking if
12 : : * a node contains a free or a bound variable.
13 : : */
14 : :
15 : : #include "expr/node_algorithm.h"
16 : :
17 : : #include "expr/attribute.h"
18 : : #include "expr/cardinality_constraint.h"
19 : : #include "expr/dtype.h"
20 : : #include "expr/skolem_manager.h"
21 : :
22 : : namespace cvc5::internal {
23 : : namespace expr {
24 : :
25 : 681900 : bool hasSubterm(TNode n, TNode t, bool strict)
26 : : {
27 [ + - ][ + + ]: 681900 : if (!strict && n == t)
[ + + ]
28 : : {
29 : 107709 : return true;
30 : : }
31 : :
32 : 574191 : std::unordered_set<TNode> visited;
33 : 574191 : std::vector<TNode> toProcess;
34 : :
35 : 574191 : toProcess.push_back(n);
36 : :
37 : : // incrementally iterate and add to toProcess
38 [ + + ]: 2542159 : for (unsigned i = 0; i < toProcess.size(); ++i)
39 : : {
40 : 2249099 : TNode current = toProcess[i];
41 [ + + ]: 15964128 : for (unsigned j = 0, j_end = current.getNumChildren(); j <= j_end; ++j)
42 : : {
43 : 15082557 : TNode child;
44 : : // try children then operator
45 [ + + ]: 15082557 : if (j < j_end)
46 : : {
47 : 13114557 : child = current[j];
48 : : }
49 [ + + ]: 1968000 : else if (current.hasOperator())
50 : : {
51 : 881603 : child = current.getOperator();
52 : : }
53 : : else
54 : : {
55 : 1086397 : break;
56 : : }
57 [ + + ]: 13996160 : if (child == t)
58 : : {
59 : 281131 : return true;
60 : : }
61 [ + + ]: 13715029 : if (!visited.insert(child).second)
62 : : {
63 : 957176 : continue;
64 : : }
65 : : else
66 : : {
67 : 12757853 : toProcess.push_back(child);
68 : : }
69 [ + + ][ + + ]: 15082557 : }
70 [ + + ]: 2249099 : }
71 : :
72 : 293060 : return false;
73 : 574191 : }
74 : :
75 : 0 : bool hasSubtermMulti(TNode n, TNode t)
76 : : {
77 : 0 : std::unordered_map<TNode, bool> visited;
78 : 0 : std::unordered_map<TNode, bool> contains;
79 : 0 : std::unordered_map<TNode, bool>::iterator it;
80 : 0 : std::vector<TNode> visit;
81 : 0 : TNode cur;
82 : 0 : visit.push_back(n);
83 : : do
84 : : {
85 : 0 : cur = visit.back();
86 : 0 : visit.pop_back();
87 : 0 : it = visited.find(cur);
88 : :
89 [ - - ]: 0 : if (it == visited.end())
90 : : {
91 [ - - ]: 0 : if (cur == t)
92 : : {
93 : 0 : visited[cur] = true;
94 : 0 : contains[cur] = true;
95 : : }
96 : : else
97 : : {
98 : 0 : visited[cur] = false;
99 : 0 : visit.push_back(cur);
100 [ - - ]: 0 : for (const Node& cc : cur)
101 : : {
102 : 0 : visit.push_back(cc);
103 : 0 : }
104 : : }
105 : : }
106 [ - - ]: 0 : else if (!it->second)
107 : : {
108 : 0 : bool doesContain = false;
109 [ - - ]: 0 : for (const Node& cn : cur)
110 : : {
111 : 0 : it = contains.find(cn);
112 : 0 : Assert(it != contains.end());
113 [ - - ]: 0 : if (it->second)
114 : : {
115 [ - - ]: 0 : if (doesContain)
116 : : {
117 : : // two children have t, return true
118 : 0 : return true;
119 : : }
120 : 0 : doesContain = true;
121 : : }
122 [ - - ]: 0 : }
123 : 0 : contains[cur] = doesContain;
124 : 0 : visited[cur] = true;
125 : : }
126 [ - - ]: 0 : } while (!visit.empty());
127 : 0 : return false;
128 : 0 : }
129 : :
130 : 2280852 : bool hasSubtermKind(Kind k, Node n)
131 : : {
132 : 2280852 : std::unordered_set<TNode> visited;
133 : 2280852 : std::vector<TNode> visit;
134 : 2280852 : TNode cur;
135 : 2280852 : visit.push_back(n);
136 : : do
137 : : {
138 : 26100116 : cur = visit.back();
139 : 26100116 : visit.pop_back();
140 [ + + ]: 26100116 : if (visited.insert(cur).second)
141 : : {
142 [ + + ]: 21053656 : if (cur.getKind() == k)
143 : : {
144 : 883 : return true;
145 : : }
146 [ + + ]: 21052773 : if (cur.hasOperator())
147 : : {
148 : 8901633 : visit.push_back(cur.getOperator());
149 : : }
150 : 21052773 : visit.insert(visit.end(), cur.begin(), cur.end());
151 : : }
152 [ + + ]: 26099233 : } while (!visit.empty());
153 : 2279969 : return false;
154 : 2280852 : }
155 : :
156 : 529750 : bool hasSubtermKinds(const std::unordered_set<Kind, kind::KindHashFunction>& ks,
157 : : TNode n)
158 : : {
159 [ - + ]: 529750 : if (ks.empty())
160 : : {
161 : 0 : return false;
162 : : }
163 : 529750 : std::unordered_set<TNode> visited;
164 : 529750 : return hasSubtermKinds(ks, n, visited) != Kind::UNDEFINED_KIND;
165 : 529750 : }
166 : :
167 : 529750 : Kind hasSubtermKinds(const std::unordered_set<Kind, kind::KindHashFunction>& ks,
168 : : TNode n,
169 : : std::unordered_set<TNode>& visited)
170 : : {
171 [ - + ][ - + ]: 529750 : Assert(!ks.empty());
[ - - ]
172 : 529750 : std::vector<TNode> visit;
173 : 529750 : TNode cur;
174 : 529750 : visit.push_back(n);
175 : : Kind k;
176 : : do
177 : : {
178 : 9198730 : cur = visit.back();
179 : 9198730 : visit.pop_back();
180 [ + + ]: 9198730 : if (visited.find(cur) == visited.end())
181 : : {
182 : 5995311 : k = cur.getKind();
183 [ + + ]: 5995311 : if (ks.find(k) != ks.end())
184 : : {
185 : 117951 : return k;
186 : : }
187 : 5877360 : visited.insert(cur);
188 [ + + ]: 5877360 : if (cur.hasOperator())
189 : : {
190 : 2896420 : visit.push_back(cur.getOperator());
191 : : }
192 : 5877360 : visit.insert(visit.end(), cur.begin(), cur.end());
193 : : }
194 [ + + ]: 9080779 : } while (!visit.empty());
195 : 411799 : return Kind::UNDEFINED_KIND;
196 : 529750 : }
197 : :
198 : 391944 : void getSubtermsKind(Kind k, TNode n, std::unordered_set<Node>& ts, bool nested)
199 : : {
200 : 391944 : std::unordered_set<Kind, kind::KindHashFunction> ks{k};
201 : 391944 : std::map<Kind, std::unordered_set<Node>> tsm;
202 : 391944 : getSubtermsKinds(ks, n, tsm, nested);
203 : 391944 : std::unordered_set<Node>& tsc = tsm[k];
204 : 391944 : ts.insert(tsc.begin(), tsc.end());
205 : 391944 : }
206 : :
207 : 391944 : void getSubtermsKinds(
208 : : const std::unordered_set<Kind, kind::KindHashFunction>& ks,
209 : : TNode n,
210 : : std::map<Kind, std::unordered_set<Node>>& ts,
211 : : bool nested)
212 : : {
213 [ - + ][ - + ]: 391944 : Assert(!ks.empty());
[ - - ]
214 [ + + ]: 783888 : for (Kind k : ks)
215 : : {
216 [ + - ]: 391944 : if (ts.find(k) == ts.end())
217 : : {
218 : 391944 : ts[k].clear();
219 : : }
220 : : }
221 : 391944 : std::unordered_set<TNode> visited;
222 : 391944 : std::vector<TNode> visit;
223 : 391944 : TNode cur;
224 : 391944 : visit.push_back(n);
225 : : Kind k;
226 : 391944 : std::map<Kind, std::unordered_set<Node>>::iterator itt;
227 : : do
228 : : {
229 : 3577836 : cur = visit.back();
230 : 3577836 : visit.pop_back();
231 [ + + ]: 3577836 : if (visited.insert(cur).second)
232 : : {
233 : 3231573 : k = cur.getKind();
234 : 3231573 : itt = ts.find(k);
235 [ + + ]: 3231573 : if (itt != ts.end())
236 : : {
237 : 1000789 : itt->second.insert(cur);
238 [ + + ]: 1000789 : if (!nested)
239 : : {
240 : 877 : continue;
241 : : }
242 : : }
243 [ + + ]: 3230696 : if (cur.hasOperator())
244 : : {
245 : 1016080 : visit.push_back(cur.getOperator());
246 : : }
247 : 3230696 : visit.insert(visit.end(), cur.begin(), cur.end());
248 : : }
249 [ + + ]: 3577836 : } while (!visit.empty());
250 : 391944 : }
251 : :
252 : 8376 : bool hasSubterm(TNode n, const std::vector<Node>& t, bool strict)
253 : : {
254 [ - + ]: 8376 : if (t.empty())
255 : : {
256 : 0 : return false;
257 : : }
258 [ + - ][ + + ]: 8376 : if (!strict && std::find(t.begin(), t.end(), n) != t.end())
[ + + ]
259 : : {
260 : 104 : return true;
261 : : }
262 : :
263 : 8272 : std::unordered_set<TNode> visited;
264 : 8272 : std::vector<TNode> toProcess;
265 : :
266 : 8272 : toProcess.push_back(n);
267 : :
268 : : // incrementally iterate and add to toProcess
269 [ + + ]: 86097 : for (unsigned i = 0; i < toProcess.size(); ++i)
270 : : {
271 : 80327 : TNode current = toProcess[i];
272 [ + + ]: 176409 : for (unsigned j = 0, j_end = current.getNumChildren(); j <= j_end; ++j)
273 : : {
274 : 145323 : TNode child;
275 : : // try children then operator
276 [ + + ]: 145323 : if (j < j_end)
277 : : {
278 : 67498 : child = current[j];
279 : : }
280 [ + + ]: 77825 : else if (current.hasOperator())
281 : : {
282 : 31086 : child = current.getOperator();
283 : : }
284 : : else
285 : : {
286 : 46739 : break;
287 : : }
288 [ + + ]: 98584 : if (std::find(t.begin(), t.end(), child) != t.end())
289 : : {
290 : 2502 : return true;
291 : : }
292 [ + + ]: 96082 : if (!visited.insert(child).second)
293 : : {
294 : 17336 : continue;
295 : : }
296 : : else
297 : : {
298 : 78746 : toProcess.push_back(child);
299 : : }
300 [ + + ][ + + ]: 145323 : }
301 [ + + ]: 80327 : }
302 : :
303 : 5770 : return false;
304 : 8272 : }
305 : :
306 : : struct HasBoundVarTag
307 : : {
308 : : };
309 : : struct HasBoundVarComputedTag
310 : : {
311 : : };
312 : : /** Attribute true for expressions with bound variables in them */
313 : : typedef expr::Attribute<HasBoundVarTag, bool> HasBoundVarAttr;
314 : : typedef expr::Attribute<HasBoundVarComputedTag, bool> HasBoundVarComputedAttr;
315 : :
316 : 209759419 : bool hasBoundVar(TNode n)
317 : : {
318 [ + + ]: 209759419 : if (!n.getAttribute(HasBoundVarComputedAttr()))
319 : : {
320 : 22025492 : bool hasBv = false;
321 [ + + ]: 22025492 : if (n.getKind() == Kind::BOUND_VARIABLE)
322 : : {
323 : 584224 : hasBv = true;
324 : : }
325 : : else
326 : : {
327 [ + + ][ + - ]: 36836731 : for (auto i = n.begin(); i != n.end() && !hasBv; ++i)
[ + + ]
328 : : {
329 [ + + ]: 28823099 : if (hasBoundVar(*i))
330 : : {
331 : 13427636 : hasBv = true;
332 : 13427636 : break;
333 : : }
334 : : }
335 : : }
336 [ + + ][ + + ]: 22025492 : if (!hasBv && n.hasOperator())
[ + + ]
337 : : {
338 : 6214824 : hasBv = hasBoundVar(n.getOperator());
339 : : }
340 : 22025492 : n.setAttribute(HasBoundVarAttr(), hasBv);
341 : 22025492 : n.setAttribute(HasBoundVarComputedAttr(), true);
342 [ + - ]: 44050984 : Trace("bva") << n << " has bva : " << n.getAttribute(HasBoundVarAttr())
343 : 22025492 : << std::endl;
344 : 22025492 : return hasBv;
345 : : }
346 : 187733927 : return n.getAttribute(HasBoundVarAttr());
347 : : }
348 : :
349 : 20606 : bool hasBoundVar(TNode n, const std::unordered_set<Node>& fvs)
350 : : {
351 [ + + ]: 20606 : if (fvs.empty())
352 : : {
353 : 5487 : return false;
354 : : }
355 : 15119 : std::unordered_set<TNode> visited;
356 : 15119 : std::vector<TNode> toProcess;
357 : 15119 : toProcess.push_back(n);
358 : : // incrementally iterate and add to toProcess
359 [ + + ]: 2335833 : for (unsigned i = 0; i < toProcess.size(); ++i)
360 : : {
361 : 2320754 : TNode current = toProcess[i];
362 [ + + ]: 2320754 : if (current.isClosure())
363 : : {
364 : : // check if any is contained in fvs
365 [ + + ]: 41195 : for (const Node& v : current[0])
366 : : {
367 [ + + ]: 25687 : if (fvs.find(v) != fvs.end())
368 : : {
369 : 40 : return true;
370 : : }
371 [ + + ][ + + ]: 41235 : }
372 : : }
373 [ + + ]: 7618315 : for (unsigned j = 0, j_end = current.getNumChildren(); j <= j_end; ++j)
374 : : {
375 : 6001027 : TNode child;
376 : : // try children then operator
377 [ + + ]: 6001027 : if (j < j_end)
378 : : {
379 : 3680313 : child = current[j];
380 : : }
381 [ + + ]: 2320714 : else if (current.hasOperator())
382 : : {
383 : 1617288 : child = current.getOperator();
384 : : }
385 : : else
386 : : {
387 : 703426 : break;
388 : : }
389 [ + + ]: 5297601 : if (!visited.insert(child).second)
390 : : {
391 : 2991886 : continue;
392 : : }
393 : : else
394 : : {
395 : 2305715 : toProcess.push_back(child);
396 : : }
397 [ + + ][ + ]: 6001027 : }
398 [ + + ]: 2320754 : }
399 : 15079 : return false;
400 : 15119 : }
401 : :
402 : : /**
403 : : * Check variables internal, which is used as a helper to implement many of the
404 : : * methods in this file.
405 : : *
406 : : * This computes the free variables in n, that is, the subterms of n of kind
407 : : * BOUND_VARIABLE that are not bound in n or occur in scope, adds these to fvs
408 : : * if computeFv is true.
409 : : *
410 : : * @param n The node under investigation
411 : : * @param fvs The set which free variables are added to
412 : : * @param scope The scope we are considering.
413 : : * @param wasShadow Flag set to true if variable shadowing was encountered.
414 : : * Only computed if checkShadow is true.
415 : : * @param computeFv If this flag is false, then we only return true/false and
416 : : * do not add to fvs.
417 : : * @param checkShadow If this flag is true, we immediately return true if a
418 : : * variable is shadowing. If this flag is false, we give an assertion failure
419 : : * when this occurs.
420 : : * @return true iff this node contains a free variable.
421 : : */
422 : 35361670 : bool checkVariablesInternal(TNode n,
423 : : std::unordered_set<Node>& fvs,
424 : : std::unordered_set<TNode>& scope,
425 : : bool& wasShadow,
426 : : bool computeFv = true,
427 : : bool checkShadow = false)
428 : : {
429 : 35361670 : std::unordered_set<TNode> visited;
430 : 35361670 : std::vector<TNode> visit;
431 : 35361670 : TNode cur;
432 : 35361670 : visit.push_back(n);
433 : : do
434 : : {
435 : 132759432 : cur = visit.back();
436 : 132759432 : visit.pop_back();
437 : : // can skip if it doesn't have a bound variable
438 [ + + ]: 132759432 : if (!hasBoundVar(cur))
439 : : {
440 : 63858070 : continue;
441 : : }
442 [ + + ]: 68901362 : if (visited.insert(cur).second)
443 : : {
444 [ + + ]: 62723948 : if (cur.getKind() == Kind::BOUND_VARIABLE)
445 : : {
446 [ + + ]: 29257735 : if (scope.find(cur) == scope.end())
447 : : {
448 [ + + ]: 28284717 : if (computeFv)
449 : : {
450 : 28284663 : fvs.insert(cur);
451 : : }
452 : : else
453 : : {
454 : 54 : return true;
455 : : }
456 : : }
457 : : }
458 [ + + ]: 33466213 : else if (cur.isClosure())
459 : : {
460 : : // add to scope
461 : 465936 : std::vector<TNode> boundvars;
462 [ + + ]: 1381189 : for (const TNode& cn : cur[0])
463 : : {
464 [ + + ]: 915253 : if (scope.find(cn) != scope.end())
465 : : {
466 [ - + ]: 488 : if (checkShadow)
467 : : {
468 : 0 : wasShadow = true;
469 : 0 : return true;
470 : : }
471 : : }
472 : : else
473 : : {
474 : : // add to scope if it is not shadowing
475 : 914765 : boundvars.push_back(cn);
476 : 914765 : scope.insert(cn);
477 : : }
478 [ + - ][ + - ]: 1381189 : }
479 : : // must make recursive call to use separate cache
480 [ - + ][ - - ]: 465936 : if (checkVariablesInternal(
481 : : cur[1], fvs, scope, wasShadow, computeFv, checkShadow)
482 [ + + ][ - + ]: 465936 : && !computeFv)
[ + - ]
483 : : {
484 : 0 : return true;
485 : : }
486 : : // cleanup
487 [ + + ]: 1380701 : for (const TNode& cn : boundvars)
488 : : {
489 : 914765 : scope.erase(cn);
490 : : }
491 [ + - ]: 465936 : }
492 : : else
493 : : {
494 [ + - ]: 33000277 : if (cur.hasOperator())
495 : : {
496 : 33000277 : visit.push_back(cur.getOperator());
497 : : }
498 : 33000277 : visit.insert(visit.end(), cur.begin(), cur.end());
499 : : }
500 : : }
501 [ + + ]: 132759378 : } while (!visit.empty());
502 : :
503 : 35361616 : return !fvs.empty();
504 : 35361670 : }
505 : :
506 : : /** Same as above, without checking for shadowing */
507 : 34895269 : bool getVariablesInternal(TNode n,
508 : : std::unordered_set<Node>& fvs,
509 : : std::unordered_set<TNode>& scope,
510 : : bool computeFv = true)
511 : : {
512 : 34895269 : bool wasShadow = false;
513 : 34895269 : return checkVariablesInternal(n, fvs, scope, wasShadow, computeFv, false);
514 : : }
515 : :
516 : 46017149 : bool hasFreeVar(TNode n)
517 : : {
518 : : // optimization for variables and constants
519 [ + + ]: 46017149 : if (n.getNumChildren() == 0)
520 : : {
521 : 26832472 : return n.getKind() == Kind::BOUND_VARIABLE;
522 : : }
523 : 19184677 : std::unordered_set<Node> fvs;
524 : 19184677 : std::unordered_set<TNode> scope;
525 : 19184677 : return getVariablesInternal(n, fvs, scope, false);
526 : 19184677 : }
527 : :
528 : 3175 : bool hasFreeOrShadowedVar(TNode n, bool& wasShadow)
529 : : {
530 : : // optimization for variables and constants
531 [ + + ]: 3175 : if (n.getNumChildren() == 0)
532 : : {
533 : 2710 : return n.getKind() == Kind::BOUND_VARIABLE;
534 : : }
535 : 465 : std::unordered_set<Node> fvs;
536 : 465 : std::unordered_set<TNode> scope;
537 : 465 : return checkVariablesInternal(n, fvs, scope, wasShadow, false, true);
538 : 465 : }
539 : :
540 : : struct HasClosureTag
541 : : {
542 : : };
543 : : struct HasClosureComputedTag
544 : : {
545 : : };
546 : : /** Attribute true for expressions with closures in them */
547 : : typedef expr::Attribute<HasClosureTag, bool> HasClosureAttr;
548 : : typedef expr::Attribute<HasClosureComputedTag, bool> HasClosureComputedAttr;
549 : :
550 : 3868 : bool hasClosure(Node n)
551 : : {
552 [ + + ]: 3868 : if (!n.getAttribute(HasClosureComputedAttr()))
553 : : {
554 : 2317 : bool hasC = false;
555 [ + + ]: 2317 : if (n.isClosure())
556 : : {
557 : 49 : hasC = true;
558 : : }
559 : : else
560 : : {
561 [ + + ][ + + ]: 4468 : for (auto i = n.begin(); i != n.end() && !hasC; ++i)
[ + + ]
562 : : {
563 : 2200 : hasC = hasClosure(*i);
564 : : }
565 : : }
566 [ + + ][ + + ]: 2317 : if (!hasC && n.hasOperator())
[ + + ]
567 : : {
568 : 1084 : hasC = hasClosure(n.getOperator());
569 : : }
570 : 2317 : n.setAttribute(HasClosureAttr(), hasC);
571 : 2317 : n.setAttribute(HasClosureComputedAttr(), true);
572 : 2317 : return hasC;
573 : : }
574 : 1551 : return n.getAttribute(HasClosureAttr());
575 : : }
576 : :
577 : 15699450 : bool getFreeVariables(TNode n, std::unordered_set<Node>& fvs)
578 : : {
579 : 15699450 : std::unordered_set<TNode> scope;
580 : 31398900 : return getVariablesInternal(n, fvs, scope);
581 : 15699450 : }
582 : :
583 : 0 : bool getFreeVariablesScope(TNode n,
584 : : std::unordered_set<Node>& fvs,
585 : : std::unordered_set<TNode>& scope)
586 : : {
587 : 0 : return getVariablesInternal(n, fvs, scope);
588 : : }
589 : 11142 : bool hasFreeVariablesScope(TNode n, std::unordered_set<TNode>& scope)
590 : : {
591 : 11142 : std::unordered_set<Node> fvs;
592 : 22284 : return getVariablesInternal(n, fvs, scope, false);
593 : 11142 : }
594 : :
595 : 2314 : bool getVariables(TNode n, std::unordered_set<Node>& vs)
596 : : {
597 : 2314 : std::unordered_set<TNode> visited;
598 : 4628 : return getVariables(n, vs, visited);
599 : 2314 : }
600 : :
601 : 2314 : bool getVariables(TNode n,
602 : : std::unordered_set<Node>& vs,
603 : : std::unordered_set<TNode>& visited)
604 : : {
605 : 2314 : std::vector<TNode> visit;
606 : 2314 : TNode cur;
607 : 2314 : visit.push_back(n);
608 : : do
609 : : {
610 : 57338 : cur = visit.back();
611 : 57338 : visit.pop_back();
612 : 57338 : std::unordered_set<TNode>::iterator itv = visited.find(cur);
613 [ + + ]: 57338 : if (itv == visited.end())
614 : : {
615 [ + + ]: 34464 : if (cur.isVar())
616 : : {
617 : 6965 : vs.insert(cur);
618 : : }
619 : : else
620 : : {
621 [ + + ]: 27499 : if (cur.hasOperator())
622 : : {
623 : 17782 : visit.push_back(cur.getOperator());
624 : : }
625 : 27499 : visit.insert(visit.end(), cur.begin(), cur.end());
626 : : }
627 : 34464 : visited.insert(cur);
628 : : }
629 [ + + ]: 57338 : } while (!visit.empty());
630 : :
631 : 4628 : return !vs.empty();
632 : 2314 : }
633 : :
634 : 23844 : void getSymbols(TNode n, std::unordered_set<Node>& syms)
635 : : {
636 : 23844 : std::unordered_set<TNode> visited;
637 : 23844 : getSymbols(n, syms, visited);
638 : 23844 : }
639 : :
640 : 109227 : void getSymbols(TNode n,
641 : : std::unordered_set<Node>& syms,
642 : : std::unordered_set<TNode>& visited)
643 : : {
644 : 109227 : std::vector<TNode> visit;
645 : 109227 : TNode cur;
646 : 109227 : visit.push_back(n);
647 : : do
648 : : {
649 : 2023424 : cur = visit.back();
650 : 2023424 : visit.pop_back();
651 [ + + ]: 2023424 : if (visited.find(cur) == visited.end())
652 : : {
653 : 1040825 : visited.insert(cur);
654 [ + + ][ + + ]: 1040825 : if (cur.isVar() && cur.getKind() != Kind::BOUND_VARIABLE)
[ + + ]
655 : : {
656 : 124956 : syms.insert(cur);
657 : : }
658 [ + + ]: 1040825 : if (cur.hasOperator())
659 : : {
660 : 628572 : visit.push_back(cur.getOperator());
661 : : }
662 : 1040825 : visit.insert(visit.end(), cur.begin(), cur.end());
663 : : }
664 [ + + ]: 2023424 : } while (!visit.empty());
665 : 109227 : }
666 : :
667 : 12810 : void getKindSubterms(TNode n,
668 : : Kind k,
669 : : bool topLevel,
670 : : std::unordered_set<Node>& ts)
671 : : {
672 : 12810 : std::unordered_set<TNode> visited;
673 : 12810 : std::vector<TNode> visit;
674 : 12810 : TNode cur;
675 : 12810 : visit.push_back(n);
676 : : do
677 : : {
678 : 148536 : cur = visit.back();
679 : 148536 : visit.pop_back();
680 [ + + ]: 148536 : if (visited.find(cur) == visited.end())
681 : : {
682 : 115855 : visited.insert(cur);
683 [ + + ]: 115855 : if (cur.getKind() == k)
684 : : {
685 : 349 : ts.insert(cur);
686 [ + + ]: 349 : if (topLevel)
687 : : {
688 : : // only considering top-level applications
689 : 217 : continue;
690 : : }
691 : : }
692 [ + + ]: 115638 : if (cur.hasOperator())
693 : : {
694 : 47035 : visit.push_back(cur.getOperator());
695 : : }
696 : 115638 : visit.insert(visit.end(), cur.begin(), cur.end());
697 : : }
698 [ + + ]: 148536 : } while (!visit.empty());
699 : 12810 : }
700 : :
701 : 3 : void getOperatorsMap(TNode n, std::map<TypeNode, std::unordered_set<Node>>& ops)
702 : : {
703 : 3 : std::unordered_set<TNode> visited;
704 : 3 : getOperatorsMap(n, ops, visited);
705 : 3 : }
706 : :
707 : 3 : void getOperatorsMap(TNode n,
708 : : std::map<TypeNode, std::unordered_set<Node>>& ops,
709 : : std::unordered_set<TNode>& visited)
710 : : {
711 : : // nodes that we still need to visit
712 : 3 : std::vector<TNode> visit;
713 : : // current node
714 : 3 : TNode cur;
715 : 3 : visit.push_back(n);
716 : : do
717 : : {
718 : 45 : cur = visit.back();
719 : 45 : visit.pop_back();
720 : : // if cur is in the cache, do nothing
721 [ + - ]: 45 : if (visited.find(cur) == visited.end())
722 : : {
723 : : // fetch the correct type
724 : 45 : TypeNode tn = cur.getType();
725 : : // add the current operator to the result
726 [ + + ]: 45 : if (cur.hasOperator())
727 : : {
728 : 22 : Node o;
729 [ + + ]: 22 : if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
730 : : {
731 : 2 : o = cur.getOperator();
732 : : }
733 : : else
734 : : {
735 : 20 : o = cur.getNodeManager()->operatorOf(cur.getKind());
736 : : }
737 : 22 : ops[tn].insert(o);
738 : 22 : }
739 : : // add children to visit in the future
740 : 45 : visit.insert(visit.end(), cur.begin(), cur.end());
741 : 45 : }
742 [ + + ]: 45 : } while (!visit.empty());
743 : 3 : }
744 : :
745 : 0 : void getTypes(TNode n, std::unordered_set<TypeNode>& types)
746 : : {
747 : 0 : std::unordered_set<TNode> visited;
748 : 0 : getTypes(n, types, visited);
749 : 0 : }
750 : :
751 : 17352 : void getTypes(TNode n,
752 : : std::unordered_set<TypeNode>& types,
753 : : std::unordered_set<TNode>& visited)
754 : : {
755 : 17352 : std::unordered_set<TNode>::iterator it;
756 : 17352 : std::vector<TNode> visit;
757 : 17352 : TNode cur;
758 : 17352 : visit.push_back(n);
759 : : do
760 : : {
761 : 383439 : cur = visit.back();
762 : 383439 : visit.pop_back();
763 : 383439 : it = visited.find(cur);
764 [ + + ]: 383439 : if (it == visited.end())
765 : : {
766 : 211149 : visited.insert(cur);
767 : 211149 : types.insert(cur.getType());
768 : : // special cases where the type is not part of the AST
769 [ + + ]: 211149 : if (cur.getKind() == Kind::CARDINALITY_CONSTRAINT)
770 : : {
771 : 10 : types.insert(
772 : 10 : cur.getOperator().getConst<CardinalityConstraint>().getType());
773 : : }
774 : 211149 : visit.insert(visit.end(), cur.begin(), cur.end());
775 : : }
776 [ + + ]: 383439 : } while (!visit.empty());
777 : 17352 : }
778 : :
779 : 370385 : void getComponentTypes(TypeNode t, std::unordered_set<TypeNode>& types)
780 : : {
781 : 370385 : std::vector<TypeNode> toProcess;
782 : 370385 : toProcess.push_back(t);
783 : : do
784 : : {
785 : 495658 : TypeNode curr = toProcess.back();
786 : 495658 : toProcess.pop_back();
787 : : // if not already visited
788 [ + + ]: 495658 : if (types.find(curr) == types.end())
789 : : {
790 : 274567 : types.insert(curr);
791 : : // get component types from the children
792 [ + + ]: 399840 : for (unsigned i = 0, nchild = curr.getNumChildren(); i < nchild; i++)
793 : : {
794 : 125273 : toProcess.push_back(curr[i]);
795 : : }
796 : : }
797 [ + + ]: 495658 : } while (!toProcess.empty());
798 : 370385 : }
799 : :
800 : 4014248 : bool match(Node x, Node y, std::unordered_map<Node, Node>& subs)
801 : : {
802 : 4014248 : std::unordered_set<std::pair<TNode, TNode>, TNodePairHashFunction> visited;
803 : : std::unordered_set<std::pair<TNode, TNode>, TNodePairHashFunction>::iterator
804 : 4014248 : it;
805 : 4014248 : std::unordered_map<Node, Node>::iterator subsIt;
806 : :
807 : 4014248 : std::vector<std::pair<TNode, TNode>> stack;
808 : 4014248 : stack.emplace_back(x, y);
809 : 4014248 : std::pair<TNode, TNode> curr;
810 : :
811 [ + + ]: 45213570 : while (!stack.empty())
812 : : {
813 : 41207205 : curr = stack.back();
814 : 41207205 : stack.pop_back();
815 [ + + ]: 41207205 : if (curr.first == curr.second)
816 : : {
817 : : // holds trivially
818 : 2566658 : continue;
819 : : }
820 : 38640547 : it = visited.find(curr);
821 [ + + ]: 38640547 : if (it != visited.end())
822 : : {
823 : : // already processed
824 : 9350909 : continue;
825 : : }
826 : 29289638 : visited.insert(curr);
827 [ + + ]: 29289638 : if (curr.first.getNumChildren() == 0)
828 : : {
829 [ + + ]: 11533665 : if (!curr.first.getType().isComparableTo(curr.second.getType()))
830 : : {
831 : : // the two subterms have different types
832 : 1 : return false;
833 : : }
834 : : // if the two subterms are not equal and the first one is a bound
835 : : // variable...
836 [ + + ]: 11533664 : if (curr.first.getKind() == Kind::BOUND_VARIABLE)
837 : : {
838 : : // and we have not seen this variable before...
839 : 11532958 : subsIt = subs.find(curr.first);
840 [ + + ]: 11532958 : if (subsIt == subs.cend())
841 : : {
842 : : // add the two subterms to `sub`
843 : 11532565 : subs.emplace(curr.first, curr.second);
844 : : }
845 : : else
846 : : {
847 : : // if we saw this variable before, make sure that (now and before) it
848 : : // maps to the same subterm
849 [ + + ]: 393 : if (curr.second != subsIt->second)
850 : : {
851 : 391 : return false;
852 : : }
853 : : }
854 : : }
855 : : else
856 : : {
857 : : // the two subterms are not equal
858 : 706 : return false;
859 : : }
860 : : }
861 : : else
862 : : {
863 : : // if the two subterms are not equal, make sure that their operators are
864 : : // equal
865 : : // we compare operators instead of kinds because different terms may have
866 : : // the same kind (both `(id x)` and `(square x)` have kind APPLY_UF)
867 : : // since many builtin operators like `ADD` allow arbitrary number of
868 : : // arguments, we also need to check if the two subterms have the same
869 : : // number of children
870 : 17755973 : if (curr.first.getNumChildren() != curr.second.getNumChildren()
871 : 35511946 : || curr.first.getOperator() != curr.second.getOperator())
872 : : {
873 : 6785 : return false;
874 : : }
875 : : // recurse on children
876 [ + + ]: 54946906 : for (size_t i = 0, n = curr.first.getNumChildren(); i < n; ++i)
877 : : {
878 : 37197718 : stack.emplace_back(curr.first[i], curr.second[i]);
879 : : }
880 : : }
881 : : }
882 : 4006365 : return true;
883 : 4014248 : }
884 : :
885 : 3909 : void getConversionConditions(Node n1,
886 : : Node n2,
887 : : std::vector<Node>& eqs,
888 : : bool isHo)
889 : : {
890 : 3909 : std::unordered_set<std::pair<TNode, TNode>, TNodePairHashFunction> visited;
891 : : std::unordered_set<std::pair<TNode, TNode>, TNodePairHashFunction>::iterator
892 : 3909 : it;
893 : 3909 : std::vector<std::pair<TNode, TNode>> stack;
894 : 3909 : stack.emplace_back(n1, n2);
895 : 3909 : std::pair<TNode, TNode> curr;
896 [ + + ]: 42335 : while (!stack.empty())
897 : : {
898 : 38426 : curr = stack.back();
899 : 38426 : stack.pop_back();
900 [ + + ]: 38426 : if (curr.first == curr.second)
901 : : {
902 : : // holds trivially
903 : 16441 : continue;
904 : : }
905 [ - + ][ - + ]: 65955 : AssertEqual(curr.first.getType(), curr.second.getType());
[ - - ]
906 : 21985 : it = visited.find(curr);
907 [ + + ]: 21985 : if (it != visited.end())
908 : : {
909 : : // already processed
910 : 3198 : continue;
911 : : }
912 : 18787 : visited.insert(curr);
913 : 18787 : bool rec = false;
914 : 18787 : if (curr.first.getNumChildren() > 0
915 [ + + ][ + + ]: 18787 : && curr.first.getNumChildren() == curr.second.getNumChildren())
[ + + ]
916 : : {
917 : 15837 : size_t prevSize = stack.size();
918 [ + + ]: 15837 : if (curr.first.getOperator() == curr.second.getOperator())
919 : : {
920 [ + + ]: 15834 : if (curr.first.isClosure())
921 : : {
922 : : // only recurse if equal variable lists
923 : 96 : rec = (curr.first[0] == curr.second[0]);
924 : : }
925 : : else
926 : : {
927 : 15738 : rec = true;
928 : : }
929 : : }
930 [ + - ]: 3 : else if (isHo && curr.first.getKind() == Kind::APPLY_UF
931 [ + - ][ + - ]: 6 : && curr.second.getKind() == Kind::APPLY_UF)
[ + - ]
932 : : {
933 : 3 : rec = true;
934 : : // if isHo, we recurse on distinct operators with the same type
935 : : // note that it is redundant to check type here, as we check the
936 : : // types of arguments below and undo if necessary
937 : 3 : stack.emplace_back(curr.first.getOperator(), curr.second.getOperator());
938 : : }
939 [ + + ]: 15837 : if (rec)
940 : : {
941 : : // recurse on children
942 [ + + ]: 50309 : for (size_t i = 0, n = curr.first.getNumChildren(); i < n; ++i)
943 : : {
944 : : // if there is a type mismatch, we can't unify
945 [ + + ]: 173010 : if (!CVC5_EQUAL(curr.first[i].getType(), curr.second[i].getType()))
946 : : {
947 : 88 : stack.resize(prevSize);
948 : 88 : rec = false;
949 : 88 : break;
950 : : }
951 : 34514 : stack.emplace_back(curr.first[i], curr.second[i]);
952 : : }
953 : : }
954 : : }
955 [ + + ]: 18787 : if (!rec)
956 : : {
957 : 3080 : eqs.push_back(curr.first.eqNode(curr.second));
958 : : }
959 : : }
960 : 3909 : }
961 : :
962 : 676619 : bool isBooleanConnective(TNode cur)
963 : : {
964 : 676619 : Kind k = cur.getKind();
965 [ + + ][ + + ]: 611828 : return k == Kind::NOT || k == Kind::IMPLIES || k == Kind::AND || k == Kind::OR
[ + + ]
966 [ + + ][ - + ]: 1009348 : || (k == Kind::ITE && cur.getType().isBoolean()) || k == Kind::XOR
[ + + ][ - - ]
967 : 1965066 : || (k == Kind::EQUAL && cur[0].getType().isBoolean());
968 : : }
969 : :
970 : 187013701 : bool isTheoryAtom(TNode n)
971 : : {
972 : 187013701 : Kind k = n.getKind();
973 [ - + ][ - + ]: 187013701 : Assert(k != Kind::NOT);
[ - - ]
974 [ + + ][ + + ]: 119223277 : return k != Kind::AND && k != Kind::OR && k != Kind::IMPLIES && k != Kind::ITE
[ + + ]
975 : 306236978 : && k != Kind::XOR && (k != Kind::EQUAL || !n[0].getType().isBoolean());
976 : : }
977 : :
978 : : struct HasAbstractSubtermTag
979 : : {
980 : : };
981 : : struct HasAbstractSubtermComputedTag
982 : : {
983 : : };
984 : : /** Attribute true for expressions that have subterms with abstract type */
985 : : using AbstractSubtermVarAttr = expr::Attribute<HasAbstractSubtermTag, bool>;
986 : : using HasAbstractSubtermComputedAttr =
987 : : expr::Attribute<HasAbstractSubtermComputedTag, bool>;
988 : :
989 : 22113424 : bool hasAbstractSubterm(TNode n)
990 : : {
991 [ + + ]: 22113424 : if (!n.getAttribute(HasAbstractSubtermComputedAttr()))
992 : : {
993 : 3980592 : bool hasAbs = false;
994 [ + + ]: 3980592 : if (n.getType().isAbstract())
995 : : {
996 : 2474 : hasAbs = true;
997 : : }
998 : : else
999 : : {
1000 [ + + ]: 12047758 : for (auto i = n.begin(); i != n.end(); ++i)
1001 : : {
1002 [ + + ]: 8070667 : if (hasAbstractSubterm(*i))
1003 : : {
1004 : 1027 : hasAbs = true;
1005 : 1027 : break;
1006 : : }
1007 : : }
1008 : : }
1009 [ + + ][ + + ]: 3980592 : if (!hasAbs && n.hasOperator())
[ + + ]
1010 : : {
1011 : 3791930 : hasAbs = hasAbstractSubterm(n.getOperator());
1012 : : }
1013 : 3980592 : n.setAttribute(AbstractSubtermVarAttr(), hasAbs);
1014 : 3980592 : n.setAttribute(HasAbstractSubtermComputedAttr(), true);
1015 : 3980592 : return hasAbs;
1016 : : }
1017 : 18132832 : return n.getAttribute(AbstractSubtermVarAttr());
1018 : : }
1019 : :
1020 : : } // namespace expr
1021 : : } // namespace cvc5::internal
|
