Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Tim King, Aina Niemetz, Clark Barrett
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 : : * Simplifications for ITE expressions.
14 : : *
15 : : * This module implements preprocessing phases designed to simplify ITE
16 : : * expressions. Based on:
17 : : * Kim, Somenzi, Jin. Efficient Term-ITE Conversion for SMT. FMCAD 2009.
18 : : * Burch, Jerry. Techniques for Verifying Superscalar Microprocessors. DAC
19 : : *'96
20 : : */
21 : : #include "preprocessing/util/ite_utilities.h"
22 : :
23 : : #include <utility>
24 : :
25 : : #include "expr/skolem_manager.h"
26 : : #include "preprocessing/assertion_pipeline.h"
27 : : #include "preprocessing/passes/rewrite.h"
28 : : #include "theory/theory.h"
29 : : #include "util/rational.h"
30 : :
31 : : using namespace std;
32 : : namespace cvc5::internal {
33 : : namespace preprocessing {
34 : : namespace util {
35 : :
36 : : namespace ite {
37 : :
38 : 117928 : inline static bool isTermITE(TNode e)
39 : : {
40 [ + + ][ + + ]: 117928 : return (e.getKind() == Kind::ITE && !e.getType().isBoolean());
[ + + ][ - - ]
41 : : }
42 : :
43 : 205760 : inline static bool triviallyContainsNoTermITEs(TNode e)
44 : : {
45 [ + + ][ + + ]: 205760 : return e.isConst() || e.isVar();
46 : : }
47 : :
48 : 5258 : static bool isTheoryAtom(TNode a)
49 : : {
50 : : using namespace kind;
51 [ + - ][ + + ]: 5258 : switch (a.getKind())
52 : : {
53 : 109 : case Kind::EQUAL:
54 : 109 : case Kind::DISTINCT: return !(a[0].getType().isBoolean());
55 : :
56 : : /* from uf */
57 : 0 : case Kind::APPLY_UF: return a.getType().isBoolean();
58 : 44 : case Kind::CARDINALITY_CONSTRAINT:
59 : : case Kind::DIVISIBLE:
60 : : case Kind::LT:
61 : : case Kind::LEQ:
62 : : case Kind::GT:
63 : : case Kind::GEQ:
64 : : case Kind::IS_INTEGER:
65 : : case Kind::BITVECTOR_COMP:
66 : : case Kind::BITVECTOR_ULT:
67 : : case Kind::BITVECTOR_ULE:
68 : : case Kind::BITVECTOR_UGT:
69 : : case Kind::BITVECTOR_UGE:
70 : : case Kind::BITVECTOR_SLT:
71 : : case Kind::BITVECTOR_SLE:
72 : : case Kind::BITVECTOR_SGT:
73 : 44 : case Kind::BITVECTOR_SGE: return true;
74 : 5105 : default: return false;
75 : : }
76 : : }
77 : :
78 : : struct CTIVStackElement
79 : : {
80 : : TNode curr;
81 : : unsigned pos;
82 : : CTIVStackElement() : curr(), pos(0) {}
83 : 98261 : CTIVStackElement(TNode c) : curr(c), pos(0) {}
84 : : }; /* CTIVStackElement */
85 : :
86 : : } // namespace ite
87 : :
88 : 50972 : ITEUtilities::ITEUtilities(Env& env)
89 : : : EnvObj(env),
90 : 50972 : d_containsVisitor(new ContainsTermITEVisitor()),
91 : : d_compressor(NULL),
92 : : d_simplifier(NULL),
93 : 101944 : d_careSimp(NULL)
94 : : {
95 [ - + ][ - + ]: 50972 : Assert(d_containsVisitor != NULL);
[ - - ]
96 : 50972 : }
97 : :
98 : 50627 : ITEUtilities::~ITEUtilities()
99 : : {
100 [ + + ]: 50627 : if (d_simplifier != NULL)
101 : : {
102 [ + - ]: 1 : delete d_simplifier;
103 : : }
104 [ + + ]: 50627 : if (d_compressor != NULL)
105 : : {
106 [ + - ]: 1 : delete d_compressor;
107 : : }
108 [ - + ]: 50627 : if (d_careSimp != NULL)
109 : : {
110 [ - - ]: 0 : delete d_careSimp;
111 : : }
112 : 50627 : }
113 : :
114 : 1 : Node ITEUtilities::simpITE(TNode assertion)
115 : : {
116 [ + - ]: 1 : if (d_simplifier == NULL)
117 : : {
118 : 1 : d_simplifier = new ITESimplifier(d_env, d_containsVisitor.get());
119 : : }
120 : 1 : return d_simplifier->simpITE(assertion);
121 : : }
122 : :
123 : 5 : bool ITEUtilities::simpIteDidALotOfWorkHeuristic() const
124 : : {
125 [ + + ]: 5 : if (d_simplifier == NULL)
126 : : {
127 : 4 : return false;
128 : : }
129 : : else
130 : : {
131 : 1 : return d_simplifier->doneALotOfWorkHeuristic();
132 : : }
133 : : }
134 : :
135 : : /* returns false if an assertion is discovered to be equal to false. */
136 : 1 : bool ITEUtilities::compress(AssertionPipeline* assertionsToPreprocess)
137 : : {
138 [ + - ]: 1 : if (d_compressor == NULL)
139 : : {
140 : 1 : d_compressor = new ITECompressor(d_env, d_containsVisitor.get());
141 : : }
142 : 1 : return d_compressor->compress(assertionsToPreprocess);
143 : : }
144 : :
145 : 0 : Node ITEUtilities::simplifyWithCare(TNode e)
146 : : {
147 [ - - ]: 0 : if (d_careSimp == NULL)
148 : : {
149 : 0 : d_careSimp = new ITECareSimplifier(nodeManager());
150 : : }
151 : 0 : return d_careSimp->simplifyWithCare(e);
152 : : }
153 : :
154 : 0 : void ITEUtilities::clear()
155 : : {
156 [ - - ]: 0 : if (d_simplifier != NULL)
157 : : {
158 : 0 : d_simplifier->clearSimpITECaches();
159 : : }
160 [ - - ]: 0 : if (d_compressor != NULL)
161 : : {
162 : 0 : d_compressor->garbageCollect();
163 : : }
164 [ - - ]: 0 : if (d_careSimp != NULL)
165 : : {
166 : 0 : d_careSimp->clear();
167 : : }
168 : 0 : d_containsVisitor->garbageCollect();
169 : 0 : }
170 : :
171 : : /** ContainsTermITEVisitor. */
172 : 85118 : ContainsTermITEVisitor::ContainsTermITEVisitor() : d_cache() {}
173 : 84773 : ContainsTermITEVisitor::~ContainsTermITEVisitor() {}
174 : 36930 : bool ContainsTermITEVisitor::containsTermITE(TNode e)
175 : : {
176 : : /* throughout execution skip through NOT nodes. */
177 [ - + ]: 36930 : e = (e.getKind() == Kind::NOT) ? e[0] : e;
178 [ + + ]: 36930 : if (ite::triviallyContainsNoTermITEs(e))
179 : : {
180 : 11442 : return false;
181 : : }
182 : :
183 : 25488 : NodeBoolMap::const_iterator end = d_cache.end();
184 : 25488 : NodeBoolMap::const_iterator tmp_it = d_cache.find(e);
185 [ + + ]: 25488 : if (tmp_it != end)
186 : : {
187 : 1167 : return (*tmp_it).second;
188 : : }
189 : :
190 : 24321 : bool foundTermIte = false;
191 : 24321 : std::vector<ite::CTIVStackElement> stack;
192 : 24321 : stack.push_back(ite::CTIVStackElement(e));
193 [ + + ][ + + ]: 289427 : while (!foundTermIte && !stack.empty())
[ + + ]
194 : : {
195 : 265106 : ite::CTIVStackElement& top = stack.back();
196 : 530212 : TNode curr = top.curr;
197 [ + + ]: 265106 : if (top.pos >= curr.getNumChildren())
198 : : {
199 : : // all of the children have been visited
200 : : // no term ites were found
201 : 96276 : d_cache[curr] = false;
202 : 96276 : stack.pop_back();
203 : : }
204 : : else
205 : : {
206 : : // this is someone's child
207 : 337660 : TNode child = curr[top.pos];
208 [ + + ]: 168830 : child = (child.getKind() == Kind::NOT) ? child[0] : child;
209 : 168830 : ++top.pos;
210 [ + + ]: 168830 : if (ite::triviallyContainsNoTermITEs(child))
211 : : {
212 : : // skip
213 : : }
214 : : else
215 : : {
216 : 75553 : tmp_it = d_cache.find(child);
217 [ + + ]: 75553 : if (tmp_it != end)
218 : : {
219 : 1613 : foundTermIte = (*tmp_it).second;
220 : : }
221 : : else
222 : : {
223 : 73940 : stack.push_back(ite::CTIVStackElement(child));
224 : 73940 : foundTermIte = ite::isTermITE(child);
225 : : }
226 : : }
227 : : }
228 : : }
229 [ + + ]: 24321 : if (foundTermIte)
230 : : {
231 [ + + ]: 3512 : while (!stack.empty())
232 : : {
233 : 1985 : TNode curr = stack.back().curr;
234 : 1985 : stack.pop_back();
235 : 1985 : d_cache[curr] = true;
236 : : }
237 : : }
238 : 24321 : return foundTermIte;
239 : : }
240 : 0 : void ContainsTermITEVisitor::garbageCollect() { d_cache.clear(); }
241 : :
242 : : /** IncomingArcCounter. */
243 : 1 : IncomingArcCounter::IncomingArcCounter(bool skipVars, bool skipConstants)
244 : 1 : : d_reachCount(), d_skipVariables(skipVars), d_skipConstants(skipConstants)
245 : : {
246 : 1 : }
247 : 1 : IncomingArcCounter::~IncomingArcCounter() {}
248 : :
249 : 1 : void IncomingArcCounter::computeReachability(
250 : : const std::vector<Node>& assertions)
251 : : {
252 : 3 : std::vector<TNode> tovisit(assertions.begin(), assertions.end());
253 : :
254 [ + + ]: 114525 : while (!tovisit.empty())
255 : : {
256 : 114524 : TNode back = tovisit.back();
257 : 114524 : tovisit.pop_back();
258 : :
259 : 114524 : bool skip = false;
260 [ + + ][ + ]: 114524 : switch (back.getMetaKind())
261 : : {
262 : 306 : case kind::metakind::CONSTANT: skip = d_skipConstants; break;
263 : 210 : case kind::metakind::VARIABLE: skip = d_skipVariables; break;
264 : 114008 : default: break;
265 : : }
266 : :
267 [ + + ]: 114524 : if (skip)
268 : : {
269 : 516 : continue;
270 : : }
271 [ + + ]: 114008 : if (d_reachCount.find(back) != d_reachCount.end())
272 : : {
273 : 106422 : d_reachCount[back] = 1 + d_reachCount[back];
274 : : }
275 : : else
276 : : {
277 : 7586 : d_reachCount[back] = 1;
278 [ + + ]: 122106 : for (TNode::iterator cit = back.begin(), end = back.end(); cit != end;
279 : 114520 : ++cit)
280 : : {
281 : 114520 : tovisit.push_back(*cit);
282 : : }
283 : : }
284 : : }
285 : 1 : }
286 : :
287 : 2 : void IncomingArcCounter::clear() { d_reachCount.clear(); }
288 : :
289 : : /** ITECompressor. */
290 : 1 : ITECompressor::ITECompressor(Env& env, ContainsTermITEVisitor* contains)
291 : : : EnvObj(env),
292 : : d_contains(contains),
293 : : d_assertions(NULL),
294 : : d_incoming(true, true),
295 : 1 : d_statistics(env.getStatisticsRegistry())
296 : : {
297 [ - + ][ - + ]: 1 : Assert(d_contains != NULL);
[ - - ]
298 : :
299 : 1 : d_true = nodeManager()->mkConst<bool>(true);
300 : 1 : d_false = nodeManager()->mkConst<bool>(false);
301 : 1 : }
302 : :
303 : 2 : ITECompressor::~ITECompressor() { reset(); }
304 : :
305 : 2 : void ITECompressor::reset()
306 : : {
307 : 2 : d_incoming.clear();
308 : 2 : d_compressed.clear();
309 : 2 : }
310 : :
311 : 0 : void ITECompressor::garbageCollect() { reset(); }
312 : :
313 : 1 : ITECompressor::Statistics::Statistics(StatisticsRegistry& reg)
314 : 1 : : d_compressCalls(reg.registerInt("ite-simp::compressCalls")),
315 : 1 : d_skolemsAdded(reg.registerInt("ite-simp::skolems"))
316 : : {
317 : 1 : }
318 : :
319 : 1720 : Node ITECompressor::push_back_boolean(Node original, Node compressed)
320 : : {
321 : 3440 : Node rewritten = rewrite(compressed);
322 : : // There is a bug if the rewritter takes a pure boolean expression
323 : : // and changes its theory
324 [ - + ]: 1720 : if (rewritten.isConst())
325 : : {
326 : 0 : d_compressed[compressed] = rewritten;
327 : 0 : d_compressed[original] = rewritten;
328 : 0 : d_compressed[rewritten] = rewritten;
329 : 0 : return rewritten;
330 : : }
331 [ - + ]: 1720 : else if (d_compressed.find(rewritten) != d_compressed.end())
332 : : {
333 : 0 : Node res = d_compressed[rewritten];
334 : 0 : d_compressed[original] = res;
335 : 0 : d_compressed[compressed] = res;
336 : 0 : return res;
337 : : }
338 : 5160 : else if (rewritten.isVar()
339 [ + - ][ + + ]: 1720 : || (rewritten.getKind() == Kind::NOT && rewritten[0].isVar()))
[ + + ][ + + ]
[ + + ][ - - ]
340 : : {
341 : 511 : d_compressed[original] = rewritten;
342 : 511 : d_compressed[compressed] = rewritten;
343 : 511 : d_compressed[rewritten] = rewritten;
344 : 511 : return rewritten;
345 : : }
346 : : else
347 : : {
348 : 1209 : NodeManager* nm = nodeManager();
349 : 3627 : Node skolem = NodeManager::mkDummySkolem("compress", nm->booleanType());
350 : 1209 : d_compressed[rewritten] = skolem;
351 : 1209 : d_compressed[original] = skolem;
352 : 1209 : d_compressed[compressed] = skolem;
353 : :
354 : 2418 : Node iff = skolem.eqNode(rewritten);
355 : 1209 : d_assertions->push_back(iff);
356 : 1209 : ++(d_statistics.d_skolemsAdded);
357 : 1209 : return skolem;
358 : : }
359 : : }
360 : :
361 : 7109 : bool ITECompressor::multipleParents(TNode c)
362 : : {
363 : 7109 : return d_incoming.lookupIncoming(c) >= 2;
364 : : }
365 : :
366 : 1920 : Node ITECompressor::compressBooleanITEs(Node toCompress)
367 : : {
368 [ - + ][ - + ]: 1920 : Assert(toCompress.getKind() == Kind::ITE);
[ - - ]
369 [ - + ][ - + ]: 1920 : Assert(toCompress.getType().isBoolean());
[ - - ]
370 : :
371 : 1920 : if (!(toCompress[1] == d_false || toCompress[2] == d_false))
372 : : {
373 : 3840 : Node cmpCnd = compressBoolean(toCompress[0]);
374 [ - + ]: 1920 : if (cmpCnd.isConst())
375 : : {
376 [ - - ]: 0 : Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2];
377 : 0 : Node res = compressBoolean(branch);
378 : 0 : d_compressed[toCompress] = res;
379 : 0 : return res;
380 : : }
381 : : else
382 : : {
383 : 3840 : Node cmpThen = compressBoolean(toCompress[1]);
384 : 3840 : Node cmpElse = compressBoolean(toCompress[2]);
385 : 3840 : Node newIte = cmpCnd.iteNode(cmpThen, cmpElse);
386 [ + + ]: 1920 : if (multipleParents(toCompress))
387 : : {
388 : 534 : return push_back_boolean(toCompress, newIte);
389 : : }
390 : : else
391 : : {
392 : 1386 : return newIte;
393 : : }
394 : : }
395 : : }
396 : :
397 : 0 : NodeBuilder nb(nodeManager(), Kind::AND);
398 : 0 : Node curr = toCompress;
399 : 0 : while (curr.getKind() == Kind::ITE
400 : 0 : && (curr[1] == d_false || curr[2] == d_false)
401 : 0 : && (!multipleParents(curr) || curr == toCompress))
402 : : {
403 : 0 : bool negateCnd = (curr[1] == d_false);
404 : 0 : Node compressCnd = compressBoolean(curr[0]);
405 [ - - ]: 0 : if (compressCnd.isConst())
406 : : {
407 [ - - ]: 0 : if (compressCnd.getConst<bool>() == negateCnd)
408 : : {
409 : 0 : return push_back_boolean(toCompress, d_false);
410 : : }
411 : : else
412 : : {
413 : : // equivalent to true don't push back
414 : : }
415 : : }
416 : : else
417 : : {
418 [ - - ]: 0 : Node pb = negateCnd ? compressCnd.notNode() : compressCnd;
419 : 0 : nb << pb;
420 : : }
421 [ - - ]: 0 : curr = negateCnd ? curr[2] : curr[1];
422 : : }
423 : 0 : Assert(toCompress != curr);
424 : :
425 : 0 : nb << compressBoolean(curr);
426 [ - - ]: 0 : Node res = nb.getNumChildren() == 1 ? nb[0] : (Node)nb;
427 : 0 : return push_back_boolean(toCompress, res);
428 : : }
429 : :
430 : 1122 : Node ITECompressor::compressTerm(Node toCompress)
431 : : {
432 [ + + ][ + + ]: 1122 : if (toCompress.isConst() || toCompress.isVar())
[ + + ]
433 : : {
434 : 513 : return toCompress;
435 : : }
436 : :
437 [ + + ]: 609 : if (d_compressed.find(toCompress) != d_compressed.end())
438 : : {
439 : 201 : return d_compressed[toCompress];
440 : : }
441 [ + + ]: 408 : if (toCompress.getKind() == Kind::ITE)
442 : : {
443 : 648 : Node cmpCnd = compressBoolean(toCompress[0]);
444 [ - + ]: 324 : if (cmpCnd.isConst())
445 : : {
446 [ - - ]: 0 : Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2];
447 : 0 : Node res = compressTerm(branch);
448 : 0 : d_compressed[toCompress] = res;
449 : 0 : return res;
450 : : }
451 : : else
452 : : {
453 : 648 : Node cmpThen = compressTerm(toCompress[1]);
454 : 648 : Node cmpElse = compressTerm(toCompress[2]);
455 : 648 : Node newIte = cmpCnd.iteNode(cmpThen, cmpElse);
456 : 324 : d_compressed[toCompress] = newIte;
457 : 324 : return newIte;
458 : : }
459 : : }
460 : :
461 : 168 : NodeBuilder nb(nodeManager(), toCompress.getKind());
462 : :
463 [ - + ]: 84 : if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED)
464 : : {
465 : 0 : nb << (toCompress.getOperator());
466 : : }
467 : 252 : for (Node::iterator it = toCompress.begin(), end = toCompress.end();
468 [ + + ]: 252 : it != end;
469 : 168 : ++it)
470 : : {
471 : 168 : nb << compressTerm(*it);
472 : : }
473 : 168 : Node compressed = (Node)nb;
474 [ + + ]: 84 : if (multipleParents(toCompress))
475 : : {
476 : 13 : d_compressed[toCompress] = compressed;
477 : : }
478 : 84 : return compressed;
479 : : }
480 : :
481 : 113402 : Node ITECompressor::compressBoolean(Node toCompress)
482 : : {
483 [ + + ][ - + ]: 113402 : if (toCompress.isConst() || toCompress.isVar())
[ + + ]
484 : : {
485 : 3 : return toCompress;
486 : : }
487 [ + + ]: 113399 : if (d_compressed.find(toCompress) != d_compressed.end())
488 : : {
489 : 106221 : return d_compressed[toCompress];
490 : : }
491 [ + + ]: 7178 : else if (toCompress.getKind() == Kind::ITE)
492 : : {
493 : 1920 : return compressBooleanITEs(toCompress);
494 : : }
495 : : else
496 : : {
497 : 5258 : bool ta = ite::isTheoryAtom(toCompress);
498 : 10516 : NodeBuilder nb(nodeManager(), toCompress.getKind());
499 [ - + ]: 5258 : if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED)
500 : : {
501 : 0 : nb << (toCompress.getOperator());
502 : : }
503 : 112878 : for (Node::iterator it = toCompress.begin(), end = toCompress.end();
504 [ + + ]: 112878 : it != end;
505 : 107620 : ++it)
506 : : {
507 : 214934 : Node pb = (ta) ? compressTerm(*it) : compressBoolean(*it);
508 : 107620 : nb << pb;
509 : : }
510 : 10516 : Node compressed = nb;
511 [ + + ][ + + ]: 5258 : if (ta || multipleParents(toCompress))
[ + + ][ + + ]
[ - - ]
512 : : {
513 : 1186 : return push_back_boolean(toCompress, compressed);
514 : : }
515 : : else
516 : : {
517 : 4072 : return compressed;
518 : : }
519 : : }
520 : : }
521 : :
522 : 1 : bool ITECompressor::compress(AssertionPipeline* assertionsToPreprocess)
523 : : {
524 : 1 : reset();
525 : :
526 : 1 : d_assertions = assertionsToPreprocess;
527 : 1 : d_incoming.computeReachability(assertionsToPreprocess->ref());
528 : :
529 : 1 : ++(d_statistics.d_compressCalls);
530 : 1 : verbose(2) << "Computed reachability" << endl;
531 : :
532 : 1 : bool nofalses = true;
533 : 1 : const std::vector<Node>& assertions = assertionsToPreprocess->ref();
534 : 1 : size_t original_size = assertions.size();
535 : 1 : verbose(2) << "compressing " << original_size << endl;
536 [ + + ][ + - ]: 5 : for (size_t i = 0; i < original_size && nofalses; ++i)
537 : : {
538 : 8 : Node assertion = assertions[i];
539 : 8 : Node compressed = compressBoolean(assertion);
540 : 4 : Node rewritten = rewrite(compressed);
541 : : // replace
542 : 4 : assertionsToPreprocess->replace(i, rewritten);
543 [ - + ][ - + ]: 4 : Assert(!d_contains->containsTermITE(rewritten));
[ - - ]
544 : :
545 : 4 : nofalses = (rewritten != d_false);
546 : : }
547 : :
548 : 1 : d_assertions = NULL;
549 : :
550 : 1 : return nofalses;
551 : : }
552 : :
553 : 1 : TermITEHeightCounter::TermITEHeightCounter() : d_termITEHeight() {}
554 : :
555 : 1 : TermITEHeightCounter::~TermITEHeightCounter() {}
556 : :
557 : 1 : void TermITEHeightCounter::clear() { d_termITEHeight.clear(); }
558 : :
559 : 0 : size_t TermITEHeightCounter::cache_size() const
560 : : {
561 : 0 : return d_termITEHeight.size();
562 : : }
563 : :
564 : : namespace ite {
565 : : struct TITEHStackElement
566 : : {
567 : : TNode curr;
568 : : unsigned pos;
569 : : uint32_t maxChildHeight;
570 : : TITEHStackElement() : curr(), pos(0), maxChildHeight(0) {}
571 : 0 : TITEHStackElement(TNode c) : curr(c), pos(0), maxChildHeight(0) {}
572 : : };
573 : : } /* namespace ite */
574 : :
575 : 0 : uint32_t TermITEHeightCounter::termITEHeight(TNode e)
576 : : {
577 [ - - ]: 0 : if (ite::triviallyContainsNoTermITEs(e))
578 : : {
579 : 0 : return 0;
580 : : }
581 : :
582 : 0 : NodeCountMap::const_iterator end = d_termITEHeight.end();
583 : 0 : NodeCountMap::const_iterator tmp_it = d_termITEHeight.find(e);
584 [ - - ]: 0 : if (tmp_it != end)
585 : : {
586 : 0 : return (*tmp_it).second;
587 : : }
588 : :
589 : 0 : uint32_t returnValue = 0;
590 : : // This is initially 0 as the very first call this is included in the max,
591 : : // but this has no effect.
592 : 0 : std::vector<ite::TITEHStackElement> stack;
593 : 0 : stack.push_back(ite::TITEHStackElement(e));
594 [ - - ]: 0 : while (!stack.empty())
595 : : {
596 : 0 : ite::TITEHStackElement& top = stack.back();
597 : 0 : top.maxChildHeight = std::max(top.maxChildHeight, returnValue);
598 : 0 : TNode curr = top.curr;
599 [ - - ]: 0 : if (top.pos >= curr.getNumChildren())
600 : : {
601 : : // done with the current node
602 [ - - ]: 0 : returnValue = top.maxChildHeight + (ite::isTermITE(curr) ? 1 : 0);
603 : 0 : d_termITEHeight[curr] = returnValue;
604 : 0 : stack.pop_back();
605 : 0 : continue;
606 : : }
607 : : else
608 : : {
609 : 0 : if (top.pos == 0 && curr.getKind() == Kind::ITE)
610 : : {
611 : 0 : ++top.pos;
612 : 0 : returnValue = 0;
613 : 0 : continue;
614 : : }
615 : : // this is someone's child
616 : 0 : TNode child = curr[top.pos];
617 : 0 : ++top.pos;
618 [ - - ]: 0 : if (ite::triviallyContainsNoTermITEs(child))
619 : : {
620 : 0 : returnValue = 0;
621 : : }
622 : : else
623 : : {
624 : 0 : tmp_it = d_termITEHeight.find(child);
625 [ - - ]: 0 : if (tmp_it != end)
626 : : {
627 : 0 : returnValue = (*tmp_it).second;
628 : : }
629 : : else
630 : : {
631 : 0 : stack.push_back(ite::TITEHStackElement(child));
632 : : }
633 : : }
634 : : }
635 : : }
636 : 0 : return returnValue;
637 : : }
638 : :
639 : 1 : ITESimplifier::ITESimplifier(Env& env, ContainsTermITEVisitor* contains)
640 : : : EnvObj(env),
641 : : d_containsVisitor(contains),
642 : : d_termITEHeight(),
643 : : d_constantLeaves(),
644 : : d_allocatedConstantLeaves(),
645 : : d_citeEqConstApplications(0),
646 : : d_constantIteEqualsConstantCache(),
647 : : d_replaceOverCache(),
648 : : d_replaceOverTermIteCache(),
649 : : d_leavesConstCache(),
650 : : d_simpConstCache(),
651 : : d_simpContextCache(),
652 : : d_simpITECache(),
653 : 1 : d_statistics(env.getStatisticsRegistry())
654 : : {
655 [ - + ][ - + ]: 1 : Assert(d_containsVisitor != NULL);
[ - - ]
656 : 1 : d_true = nodeManager()->mkConst<bool>(true);
657 : 1 : d_false = nodeManager()->mkConst<bool>(false);
658 : 1 : }
659 : :
660 : 2 : ITESimplifier::~ITESimplifier()
661 : : {
662 : 1 : clearSimpITECaches();
663 [ - + ][ - + ]: 1 : Assert(d_constantLeaves.empty());
664 [ - + ][ - + ]: 1 : Assert(d_allocatedConstantLeaves.empty());
665 : 2 : }
666 : :
667 : 156 : bool ITESimplifier::leavesAreConst(TNode e)
668 : : {
669 : 156 : return leavesAreConst(e, d_env.theoryOf(e));
670 : : }
671 : :
672 : 1 : void ITESimplifier::clearSimpITECaches()
673 : : {
674 : 1 : verbose(2) << "clear ite caches " << endl;
675 [ + + ]: 756 : for (size_t i = 0, N = d_allocatedConstantLeaves.size(); i < N; ++i)
676 : : {
677 : 755 : NodeVec* curr = d_allocatedConstantLeaves[i];
678 [ + - ]: 755 : delete curr;
679 : : }
680 : 1 : d_citeEqConstApplications = 0;
681 : 1 : d_constantLeaves.clear();
682 : 1 : d_allocatedConstantLeaves.clear();
683 : 1 : d_termITEHeight.clear();
684 : 1 : d_constantIteEqualsConstantCache.clear();
685 : 1 : d_replaceOverCache.clear();
686 : 1 : d_replaceOverTermIteCache.clear();
687 : 1 : d_simpITECache.clear();
688 : 1 : d_simpVars.clear();
689 : 1 : d_simpConstCache.clear();
690 : 1 : d_leavesConstCache.clear();
691 : 1 : d_simpContextCache.clear();
692 : 1 : }
693 : :
694 : 1 : bool ITESimplifier::doneALotOfWorkHeuristic() const
695 : : {
696 : : static const size_t SIZE_BOUND = 1000;
697 : 1 : verbose(2) << "d_citeEqConstApplications size " << d_citeEqConstApplications
698 : 1 : << endl;
699 : 1 : return (d_citeEqConstApplications > SIZE_BOUND);
700 : : }
701 : :
702 : 1 : ITESimplifier::Statistics::Statistics(StatisticsRegistry& reg)
703 : : : d_maxNonConstantsFolded(
704 : 1 : reg.registerInt("ite-simp::maxNonConstantsFolded")),
705 : 1 : d_unexpected(reg.registerInt("ite-simp::unexpected")),
706 : 1 : d_unsimplified(reg.registerInt("ite-simp::unsimplified")),
707 : 1 : d_exactMatchFold(reg.registerInt("ite-simp::exactMatchFold")),
708 : 1 : d_binaryPredFold(reg.registerInt("ite-simp::binaryPredFold")),
709 : 1 : d_specialEqualityFolds(reg.registerInt("ite-simp::specialEqualityFolds")),
710 : 1 : d_simpITEVisits(reg.registerInt("ite-simp::simpITE.visits")),
711 : : d_numBranches(0),
712 : : d_numFalseBranches(0),
713 : : d_itesMade(0),
714 : : d_instance(0),
715 : 1 : d_inSmaller(reg.registerHistogram<uint32_t>("ite-simp::inSmaller"))
716 : : {
717 : 1 : }
718 : :
719 : 1253 : bool ITESimplifier::isConstantIte(TNode e)
720 : : {
721 [ + + ]: 1253 : if (e.isConst())
722 : : {
723 : 573 : return true;
724 : : }
725 [ + - ]: 680 : else if (ite::isTermITE(e))
726 : : {
727 : 680 : NodeVec* constants = computeConstantLeaves(e);
728 : 680 : return constants != NULL;
729 : : }
730 : : else
731 : : {
732 : 0 : return false;
733 : : }
734 : : }
735 : :
736 : 43308 : ITESimplifier::NodeVec* ITESimplifier::computeConstantLeaves(TNode ite)
737 : : {
738 [ - + ][ - + ]: 43308 : Assert(ite::isTermITE(ite));
[ - - ]
739 : 43308 : ConstantLeavesMap::const_iterator it = d_constantLeaves.find(ite);
740 : 43308 : ConstantLeavesMap::const_iterator end = d_constantLeaves.end();
741 [ + + ]: 43308 : if (it != end)
742 : : {
743 : 42446 : return (*it).second;
744 : : }
745 : 1724 : TNode thenB = ite[1];
746 : 1724 : TNode elseB = ite[2];
747 : :
748 : : // special case 2 constant children
749 [ + + ][ + + ]: 862 : if (thenB.isConst() && elseB.isConst())
[ + + ]
750 : : {
751 : 152 : NodeVec* pair = new NodeVec(2);
752 : 152 : d_allocatedConstantLeaves.push_back(pair);
753 : :
754 : 152 : (*pair)[0] = std::min(thenB, elseB);
755 : 152 : (*pair)[1] = std::max(thenB, elseB);
756 : 152 : d_constantLeaves[ite] = pair;
757 : 152 : return pair;
758 : : }
759 : : // At least 1 is an ITE
760 [ + + ]: 1029 : if (!(thenB.isConst() || thenB.getKind() == Kind::ITE)
761 [ + + ][ + + ]: 1029 : || !(elseB.isConst() || elseB.getKind() == Kind::ITE))
[ + + ][ + + ]
762 : : {
763 : : // Cannot be a termITE tree
764 : 107 : d_constantLeaves[ite] = NULL;
765 : 107 : return NULL;
766 : : }
767 : :
768 : : // At least 1 is not a constant
769 [ + + ]: 1206 : TNode definitelyITE = thenB.isConst() ? elseB : thenB;
770 [ + + ]: 1206 : TNode maybeITE = thenB.isConst() ? thenB : elseB;
771 : :
772 : 603 : NodeVec* defChildren = computeConstantLeaves(definitelyITE);
773 [ - + ]: 603 : if (defChildren == NULL)
774 : : {
775 : 0 : d_constantLeaves[ite] = NULL;
776 : 0 : return NULL;
777 : : }
778 : :
779 : 1206 : NodeVec scratch;
780 : 603 : NodeVec* maybeChildren = NULL;
781 [ + + ]: 603 : if (maybeITE.getKind() == Kind::ITE)
782 : : {
783 : 192 : maybeChildren = computeConstantLeaves(maybeITE);
784 : : }
785 : : else
786 : : {
787 : 411 : scratch.push_back(maybeITE);
788 : 411 : maybeChildren = &scratch;
789 : : }
790 [ - + ]: 603 : if (maybeChildren == NULL)
791 : : {
792 : 0 : d_constantLeaves[ite] = NULL;
793 : 0 : return NULL;
794 : : }
795 : :
796 : 603 : NodeVec* both = new NodeVec(defChildren->size() + maybeChildren->size());
797 : 603 : d_allocatedConstantLeaves.push_back(both);
798 : 603 : NodeVec::iterator newEnd;
799 : : newEnd = std::set_union(defChildren->begin(),
800 : : defChildren->end(),
801 : : maybeChildren->begin(),
802 : : maybeChildren->end(),
803 : 603 : both->begin());
804 : 603 : both->resize(newEnd - both->begin());
805 : 603 : d_constantLeaves[ite] = both;
806 : 603 : return both;
807 : : }
808 : :
809 : : // This is uncached! Better for protoyping or getting limited size examples
810 : : struct IteTreeSearchData
811 : : {
812 : : set<Node> visited;
813 : : set<Node> constants;
814 : : set<Node> nonConstants;
815 : : int maxConstants;
816 : : int maxNonconstants;
817 : : int maxDepth;
818 : : bool failure;
819 : 0 : IteTreeSearchData()
820 : 0 : : maxConstants(-1), maxNonconstants(-1), maxDepth(-1), failure(false)
821 : : {
822 : 0 : }
823 : : };
824 : 0 : void iteTreeSearch(Node e, int depth, IteTreeSearchData& search)
825 : : {
826 [ - - ][ - - ]: 0 : if (search.maxDepth >= 0 && depth > search.maxDepth)
827 : : {
828 : 0 : search.failure = true;
829 : : }
830 [ - - ]: 0 : if (search.failure)
831 : : {
832 : 0 : return;
833 : : }
834 [ - - ]: 0 : if (search.visited.find(e) != search.visited.end())
835 : : {
836 : 0 : return;
837 : : }
838 : : else
839 : : {
840 : 0 : search.visited.insert(e);
841 : : }
842 : :
843 [ - - ]: 0 : if (e.isConst())
844 : : {
845 : 0 : search.constants.insert(e);
846 : 0 : if (search.maxConstants >= 0
847 [ - - ][ - - ]: 0 : && search.constants.size() > (unsigned)search.maxConstants)
[ - - ]
848 : : {
849 : 0 : search.failure = true;
850 : : }
851 : : }
852 [ - - ]: 0 : else if (e.getKind() == Kind::ITE)
853 : : {
854 : 0 : iteTreeSearch(e[1], depth + 1, search);
855 : 0 : iteTreeSearch(e[2], depth + 1, search);
856 : : }
857 : : else
858 : : {
859 : 0 : search.nonConstants.insert(e);
860 : 0 : if (search.maxNonconstants >= 0
861 [ - - ][ - - ]: 0 : && search.nonConstants.size() > (unsigned)search.maxNonconstants)
[ - - ]
862 : : {
863 : 0 : search.failure = true;
864 : : }
865 : : }
866 : : }
867 : :
868 : 0 : Node ITESimplifier::replaceOver(Node n, Node replaceWith, Node simpVar)
869 : : {
870 [ - - ]: 0 : if (n == simpVar)
871 : : {
872 : 0 : return replaceWith;
873 : : }
874 [ - - ]: 0 : else if (n.getNumChildren() == 0)
875 : : {
876 : 0 : return n;
877 : : }
878 : 0 : Assert(n.getNumChildren() > 0);
879 : 0 : Assert(!n.isVar());
880 : :
881 : 0 : pair<Node, Node> p = make_pair(n, replaceWith);
882 [ - - ]: 0 : if (d_replaceOverCache.find(p) != d_replaceOverCache.end())
883 : : {
884 : 0 : return d_replaceOverCache[p];
885 : : }
886 : :
887 : 0 : NodeBuilder builder(nodeManager(), n.getKind());
888 [ - - ]: 0 : if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
889 : : {
890 : 0 : builder << n.getOperator();
891 : : }
892 : 0 : unsigned i = 0;
893 [ - - ]: 0 : for (; i < n.getNumChildren(); ++i)
894 : : {
895 : 0 : Node newChild = replaceOver(n[i], replaceWith, simpVar);
896 : 0 : builder << newChild;
897 : : }
898 : : // Mark the substitution and continue
899 : 0 : Node result = builder;
900 : 0 : d_replaceOverCache[p] = result;
901 : 0 : return result;
902 : : }
903 : :
904 : 0 : Node ITESimplifier::replaceOverTermIte(Node e, Node simpAtom, Node simpVar)
905 : : {
906 [ - - ]: 0 : if (e.getKind() == Kind::ITE)
907 : : {
908 : 0 : pair<Node, Node> p = make_pair(e, simpAtom);
909 [ - - ]: 0 : if (d_replaceOverTermIteCache.find(p) != d_replaceOverTermIteCache.end())
910 : : {
911 : 0 : return d_replaceOverTermIteCache[p];
912 : : }
913 : 0 : Assert(!e.getType().isBoolean());
914 : 0 : Node cnd = e[0];
915 : 0 : Node newThen = replaceOverTermIte(e[1], simpAtom, simpVar);
916 : 0 : Node newElse = replaceOverTermIte(e[2], simpAtom, simpVar);
917 : 0 : Node newIte = cnd.iteNode(newThen, newElse);
918 : 0 : d_replaceOverTermIteCache[p] = newIte;
919 : 0 : return newIte;
920 : : }
921 : : else
922 : : {
923 : 0 : return replaceOver(simpAtom, e, simpVar);
924 : : }
925 : : }
926 : :
927 : 0 : Node ITESimplifier::attemptLiftEquality(TNode atom)
928 : : {
929 [ - - ]: 0 : if (atom.getKind() == Kind::EQUAL)
930 : : {
931 : 0 : TNode left = atom[0];
932 : 0 : TNode right = atom[1];
933 [ - - ]: 0 : if ((left.getKind() == Kind::ITE || right.getKind() == Kind::ITE)
934 : 0 : && !(left.getKind() == Kind::ITE && right.getKind() == Kind::ITE))
935 : : {
936 : : // exactly 1 is an ite
937 [ - - ]: 0 : TNode ite = left.getKind() == Kind::ITE ? left : right;
938 [ - - ]: 0 : TNode notIte = left.getKind() == Kind::ITE ? right : left;
939 : :
940 [ - - ]: 0 : if (notIte == ite[1])
941 : : {
942 : 0 : ++(d_statistics.d_exactMatchFold);
943 : 0 : return ite[0].iteNode(d_true, notIte.eqNode(ite[2]));
944 : : }
945 [ - - ]: 0 : else if (notIte == ite[2])
946 : : {
947 : 0 : ++(d_statistics.d_exactMatchFold);
948 : 0 : return ite[0].iteNode(notIte.eqNode(ite[1]), d_true);
949 : : }
950 : 0 : if (notIte.isConst() && (ite[1].isConst() || ite[2].isConst()))
951 : : {
952 : 0 : ++(d_statistics.d_exactMatchFold);
953 : 0 : return ite[0].iteNode(notIte.eqNode(ite[1]), notIte.eqNode(ite[2]));
954 : : }
955 : : }
956 : : }
957 : :
958 : : // try a similar more relaxed version for non-equality operators
959 : 0 : if (atom.getMetaKind() == kind::metakind::OPERATOR
960 : 0 : && atom.getNumChildren() == 2 && !atom[1].getType().isBoolean())
961 : : {
962 : 0 : TNode left = atom[0];
963 : 0 : TNode right = atom[1];
964 [ - - ]: 0 : if ((left.getKind() == Kind::ITE || right.getKind() == Kind::ITE)
965 : 0 : && !(left.getKind() == Kind::ITE && right.getKind() == Kind::ITE))
966 : : {
967 : : // exactly 1 is an ite
968 : 0 : bool leftIsIte = left.getKind() == Kind::ITE;
969 [ - - ]: 0 : Node ite = leftIsIte ? left : right;
970 [ - - ]: 0 : Node notIte = leftIsIte ? right : left;
971 : :
972 [ - - ]: 0 : if (notIte.isConst())
973 : : {
974 : 0 : IteTreeSearchData search;
975 : 0 : search.maxNonconstants = 2;
976 : 0 : iteTreeSearch(ite, 0, search);
977 [ - - ]: 0 : if (!search.failure)
978 : : {
979 : 0 : d_statistics.d_maxNonConstantsFolded.maxAssign(
980 : 0 : search.nonConstants.size());
981 [ - - ]: 0 : Trace("ite::simpite") << "used " << search.nonConstants.size()
982 : 0 : << " nonconstants" << endl;
983 : 0 : NodeManager* nm = nodeManager();
984 : 0 : Node simpVar = getSimpVar(notIte.getType());
985 [ - - ]: 0 : TNode newLeft = leftIsIte ? simpVar : notIte;
986 [ - - ]: 0 : TNode newRight = leftIsIte ? notIte : simpVar;
987 : 0 : Node newAtom = nm->mkNode(atom.getKind(), newLeft, newRight);
988 : :
989 : 0 : ++(d_statistics.d_binaryPredFold);
990 : 0 : return replaceOverTermIte(ite, newAtom, simpVar);
991 : : }
992 : : }
993 : : }
994 : : }
995 : :
996 : : // TODO "This is way too tailored. Must generalize!"
997 [ - - ]: 0 : if (atom.getKind() == Kind::EQUAL && atom.getNumChildren() == 2
998 : 0 : && ite::isTermITE(atom[0]) && atom[1].getKind() == Kind::MULT
999 : 0 : && atom[1].getNumChildren() == 2 && atom[1][0].isConst()
1000 : 0 : && atom[1][0].getConst<Rational>().isNegativeOne()
1001 : 0 : && ite::isTermITE(atom[1][1])
1002 : 0 : && d_termITEHeight.termITEHeight(atom[0]) == 1
1003 : 0 : && d_termITEHeight.termITEHeight(atom[1][1]) == 1
1004 : 0 : && (atom[0][1].isConst() || atom[0][2].isConst())
1005 : 0 : && (atom[1][1][1].isConst() || atom[1][1][2].isConst()))
1006 : : {
1007 : : // expand all 4 cases
1008 : :
1009 : 0 : Node negOne = atom[1][0];
1010 : :
1011 : 0 : Node lite = atom[0];
1012 : 0 : Node lC = lite[0];
1013 : 0 : Node lT = lite[1];
1014 : 0 : Node lE = lite[2];
1015 : :
1016 : 0 : NodeManager* nm = nodeManager();
1017 : 0 : Node negRite = atom[1][1];
1018 : 0 : Node rC = negRite[0];
1019 : 0 : Node rT = nm->mkNode(Kind::MULT, negOne, negRite[1]);
1020 : 0 : Node rE = nm->mkNode(Kind::MULT, negOne, negRite[2]);
1021 : :
1022 : : // (ite lC lT lE) = (ite rC rT rE)
1023 : : // (ite lc (= lT (ite rC rT rE) (= lE (ite rC rT rE))))
1024 : : // (ite lc (ite rC (= lT rT) (= lT rE))
1025 : : // (ite rC (= lE rT) (= lE rE)))
1026 : :
1027 : 0 : Node eqTT = lT.eqNode(rT);
1028 : 0 : Node eqTE = lT.eqNode(rE);
1029 : 0 : Node eqET = lE.eqNode(rT);
1030 : 0 : Node eqEE = lE.eqNode(rE);
1031 : 0 : Node thenLC = rC.iteNode(eqTT, eqTE);
1032 : 0 : Node elseLC = rC.iteNode(eqET, eqEE);
1033 : 0 : Node newIte = lC.iteNode(thenLC, elseLC);
1034 : :
1035 : 0 : ++(d_statistics.d_specialEqualityFolds);
1036 : 0 : return newIte;
1037 : : }
1038 : 0 : return Node::null();
1039 : : }
1040 : :
1041 : : // Interesting classes of atoms:
1042 : : // 2. Contains constants and 1 constant term ite
1043 : : // 3. Contains 2 constant term ites
1044 : 729 : Node ITESimplifier::transformAtom(TNode atom)
1045 : : {
1046 [ - + ]: 729 : if (!d_containsVisitor->containsTermITE(atom))
1047 : : {
1048 : 0 : if (atom.getKind() == Kind::EQUAL && atom[0].isConst() && atom[1].isConst())
1049 : : {
1050 : : // constant equality
1051 : 0 : return nodeManager()->mkConst<bool>(atom[0] == atom[1]);
1052 : : }
1053 : 0 : return Node::null();
1054 : : }
1055 : : else
1056 : : {
1057 : 1458 : Node acr = attemptConstantRemoval(atom);
1058 [ + + ]: 729 : if (!acr.isNull())
1059 : : {
1060 : 573 : return acr;
1061 : : }
1062 : : // Node ale = attemptLiftEquality(atom);
1063 : : // if(!ale.isNull()){
1064 : : // //return ale;
1065 : : // }
1066 : 156 : return Node::null();
1067 : : }
1068 : : }
1069 : :
1070 : 67339 : Node ITESimplifier::constantIteEqualsConstant(TNode cite, TNode constant)
1071 : : {
1072 : 67339 : d_statistics.d_instance = 0;
1073 : 67339 : ++(d_statistics.d_instance);
1074 [ + - ]: 134678 : Trace("ite::constantIteEqualsConstant")
1075 : 0 : << (d_statistics.d_instance) << "constantIteEqualsConstant(" << cite
1076 : 67339 : << ", " << constant << ")" << endl;
1077 [ + + ]: 67339 : if (cite.isConst())
1078 : : {
1079 [ + + ]: 45678 : Node res = (cite == constant) ? d_true : d_false;
1080 [ + - ]: 45678 : Trace("ite::constantIteEqualsConstant")
1081 : 22839 : << (d_statistics.d_instance) << "->" << res << endl;
1082 : 22839 : return res;
1083 : : }
1084 : 89000 : std::pair<Node, Node> pair = make_pair(cite, constant);
1085 : :
1086 : : NodePairMap::const_iterator eq_pos =
1087 : 44500 : d_constantIteEqualsConstantCache.find(pair);
1088 [ + + ]: 44500 : if (eq_pos != d_constantIteEqualsConstantCache.end())
1089 : : {
1090 [ + - ]: 5334 : Trace("ite::constantIteEqualsConstant")
1091 : 2667 : << (d_statistics.d_instance) << "->" << (*eq_pos).second << endl;
1092 : 2667 : return (*eq_pos).second;
1093 : : }
1094 : :
1095 : 41833 : ++d_citeEqConstApplications;
1096 : :
1097 : 41833 : NodeVec* leaves = computeConstantLeaves(cite);
1098 [ - + ][ - + ]: 41833 : Assert(leaves != NULL);
[ - - ]
1099 [ + + ]: 41833 : if (std::binary_search(leaves->begin(), leaves->end(), constant))
1100 : : {
1101 [ - + ]: 33383 : if (leaves->size() == 1)
1102 : : {
1103 : : // probably unreachable
1104 : 0 : d_constantIteEqualsConstantCache[pair] = d_true;
1105 [ - - ]: 0 : Trace("ite::constantIteEqualsConstant")
1106 : 0 : << (d_statistics.d_instance) << "->" << d_true << endl;
1107 : 0 : return d_true;
1108 : : }
1109 : : else
1110 : : {
1111 [ - + ][ - + ]: 33383 : Assert(cite.getKind() == Kind::ITE);
[ - - ]
1112 : 66766 : TNode cnd = cite[0];
1113 : 66766 : TNode tB = cite[1];
1114 : 66766 : TNode fB = cite[2];
1115 : 100149 : Node tEqs = constantIteEqualsConstant(tB, constant);
1116 : 100149 : Node fEqs = constantIteEqualsConstant(fB, constant);
1117 : 66766 : Node boolIte = cnd.iteNode(tEqs, fEqs);
1118 [ + + ][ + + ]: 33383 : if (!(tEqs.isConst() || fEqs.isConst()))
[ + + ]
1119 : : {
1120 : 1924 : ++(d_statistics.d_numBranches);
1121 : : }
1122 [ + + ][ + + ]: 33383 : if (!(tEqs == d_false || fEqs == d_false))
[ + + ]
1123 : : {
1124 : 2211 : ++(d_statistics.d_numFalseBranches);
1125 : : }
1126 : 33383 : ++(d_statistics.d_itesMade);
1127 : 33383 : d_constantIteEqualsConstantCache[pair] = boolIte;
1128 : : // Trace("ite::constantIteEqualsConstant") << instance << "->" << boolIte
1129 : : // << endl;
1130 : 33383 : return boolIte;
1131 : : }
1132 : : }
1133 : : else
1134 : : {
1135 : 8450 : d_constantIteEqualsConstantCache[pair] = d_false;
1136 [ + - ]: 16900 : Trace("ite::constantIteEqualsConstant")
1137 : 8450 : << (d_statistics.d_instance) << "->" << d_false << endl;
1138 : 8450 : return d_false;
1139 : : }
1140 : : }
1141 : :
1142 : 573 : Node ITESimplifier::intersectConstantIte(TNode lcite, TNode rcite)
1143 : : {
1144 : : // intersect the constant ite trees lcite and rcite
1145 : :
1146 [ + - ][ + - ]: 573 : if (lcite.isConst() || rcite.isConst())
[ + - ]
1147 : : {
1148 : 573 : bool lIsConst = lcite.isConst();
1149 [ - + ]: 1146 : TNode constant = lIsConst ? lcite : rcite;
1150 [ - + ]: 1146 : TNode cite = lIsConst ? rcite : lcite;
1151 : :
1152 : 573 : (d_statistics.d_inSmaller) << 1;
1153 : 573 : unsigned preItesMade = d_statistics.d_itesMade;
1154 : 573 : unsigned preNumBranches = d_statistics.d_numBranches;
1155 : 573 : unsigned preNumFalseBranches = d_statistics.d_numFalseBranches;
1156 : 1719 : Node bterm = constantIteEqualsConstant(cite, constant);
1157 [ + - ]: 1146 : Trace("intersectConstantIte")
1158 : 0 : << ((d_statistics.d_numBranches) - preNumBranches) << " "
1159 : 0 : << ((d_statistics.d_numFalseBranches) - preNumFalseBranches) << " "
1160 : 573 : << ((d_statistics.d_itesMade) - preItesMade) << endl;
1161 : 573 : return bterm;
1162 : : }
1163 : 0 : Assert(lcite.getKind() == Kind::ITE);
1164 : 0 : Assert(rcite.getKind() == Kind::ITE);
1165 : :
1166 : 0 : NodeVec* leftValues = computeConstantLeaves(lcite);
1167 : 0 : NodeVec* rightValues = computeConstantLeaves(rcite);
1168 : :
1169 : 0 : uint32_t smaller = std::min(leftValues->size(), rightValues->size());
1170 : :
1171 : 0 : (d_statistics.d_inSmaller) << smaller;
1172 : 0 : NodeVec intersection(smaller, Node::null());
1173 : 0 : NodeVec::iterator newEnd;
1174 : : newEnd = std::set_intersection(leftValues->begin(),
1175 : : leftValues->end(),
1176 : : rightValues->begin(),
1177 : : rightValues->end(),
1178 : 0 : intersection.begin());
1179 : 0 : intersection.resize(newEnd - intersection.begin());
1180 [ - - ]: 0 : if (intersection.empty())
1181 : : {
1182 : 0 : return d_false;
1183 : : }
1184 : : else
1185 : : {
1186 : 0 : NodeBuilder nb(nodeManager(), Kind::OR);
1187 : 0 : NodeVec::const_iterator it = intersection.begin(), end = intersection.end();
1188 [ - - ]: 0 : for (; it != end; ++it)
1189 : : {
1190 : 0 : Node inBoth = *it;
1191 : 0 : Node lefteq = constantIteEqualsConstant(lcite, inBoth);
1192 : 0 : Node righteq = constantIteEqualsConstant(rcite, inBoth);
1193 : 0 : Node bothHold = lefteq.andNode(righteq);
1194 : 0 : nb << bothHold;
1195 : : }
1196 [ - - ]: 0 : Node result = (nb.getNumChildren() > 1) ? (Node)nb : nb[0];
1197 : 0 : return result;
1198 : : }
1199 : : }
1200 : :
1201 : 0 : Node ITESimplifier::attemptEagerRemoval(TNode atom)
1202 : : {
1203 [ - - ]: 0 : if (atom.getKind() == Kind::EQUAL)
1204 : : {
1205 : 0 : TNode left = atom[0];
1206 : 0 : TNode right = atom[1];
1207 : 0 : if ((left.isConst() && right.getKind() == Kind::ITE && isConstantIte(right))
1208 : 0 : || (right.isConst() && left.getKind() == Kind::ITE
1209 : 0 : && isConstantIte(left)))
1210 : : {
1211 [ - - ]: 0 : TNode constant = left.isConst() ? left : right;
1212 [ - - ]: 0 : TNode cite = left.isConst() ? right : left;
1213 : :
1214 : 0 : std::pair<Node, Node> pair = make_pair(cite, constant);
1215 : : NodePairMap::const_iterator eq_pos =
1216 : 0 : d_constantIteEqualsConstantCache.find(pair);
1217 [ - - ]: 0 : if (eq_pos != d_constantIteEqualsConstantCache.end())
1218 : : {
1219 : 0 : Node ret = (*eq_pos).second;
1220 [ - - ]: 0 : if (ret.isConst())
1221 : : {
1222 : 0 : return ret;
1223 : : }
1224 : : else
1225 : : {
1226 : 0 : return Node::null();
1227 : : }
1228 : : }
1229 : :
1230 : 0 : NodeVec* leaves = computeConstantLeaves(cite);
1231 : 0 : Assert(leaves != NULL);
1232 [ - - ]: 0 : if (!std::binary_search(leaves->begin(), leaves->end(), constant))
1233 : : {
1234 : 0 : d_constantIteEqualsConstantCache[pair] = d_false;
1235 : 0 : return d_false;
1236 : : }
1237 : : }
1238 : : }
1239 : 0 : return Node::null();
1240 : : }
1241 : :
1242 : 729 : Node ITESimplifier::attemptConstantRemoval(TNode atom)
1243 : : {
1244 [ + + ]: 729 : if (atom.getKind() == Kind::EQUAL)
1245 : : {
1246 : 680 : TNode left = atom[0];
1247 : 680 : TNode right = atom[1];
1248 : 680 : if (isConstantIte(left) && isConstantIte(right))
1249 : : {
1250 : 573 : return intersectConstantIte(left, right);
1251 : : }
1252 : : }
1253 : 156 : return Node::null();
1254 : : }
1255 : :
1256 : 528 : bool ITESimplifier::leavesAreConst(TNode e, theory::TheoryId tid)
1257 : : {
1258 : 709 : Assert((e.getKind() == Kind::ITE && !e.getType().isBoolean())
1259 : : || d_env.theoryOf(e) != theory::THEORY_BOOL);
1260 [ + + ]: 528 : if (e.isConst())
1261 : : {
1262 : 16 : return true;
1263 : : }
1264 : :
1265 : 512 : unordered_map<Node, bool>::iterator it;
1266 : 512 : it = d_leavesConstCache.find(e);
1267 [ + + ]: 512 : if (it != d_leavesConstCache.end())
1268 : : {
1269 : 123 : return (*it).second;
1270 : : }
1271 : :
1272 : 389 : if (!containsTermITE(e) && theory::Theory::isLeafOf(e, tid))
1273 : : {
1274 : 33 : d_leavesConstCache[e] = false;
1275 : 33 : return false;
1276 : : }
1277 : :
1278 [ - + ][ - + ]: 356 : Assert(e.getNumChildren() > 0);
[ - - ]
1279 : 356 : size_t k = 0, sz = e.getNumChildren();
1280 : :
1281 [ + + ]: 356 : if (e.getKind() == Kind::ITE)
1282 : : {
1283 : 161 : k = 1;
1284 : : }
1285 : :
1286 [ + - ]: 372 : for (; k < sz; ++k)
1287 : : {
1288 [ + + ]: 372 : if (!leavesAreConst(e[k], tid))
1289 : : {
1290 : 356 : d_leavesConstCache[e] = false;
1291 : 356 : return false;
1292 : : }
1293 : : }
1294 : 0 : d_leavesConstCache[e] = true;
1295 : 0 : return true;
1296 : : }
1297 : :
1298 : 0 : Node ITESimplifier::simpConstants(TNode simpContext,
1299 : : TNode iteNode,
1300 : : TNode simpVar)
1301 : : {
1302 : 0 : NodePairMap::iterator it;
1303 : 0 : it = d_simpConstCache.find(pair<Node, Node>(simpContext, iteNode));
1304 [ - - ]: 0 : if (it != d_simpConstCache.end())
1305 : : {
1306 : 0 : return (*it).second;
1307 : : }
1308 : :
1309 [ - - ]: 0 : if (iteNode.getKind() == Kind::ITE)
1310 : : {
1311 : 0 : NodeBuilder builder(nodeManager(), Kind::ITE);
1312 : 0 : builder << iteNode[0];
1313 : 0 : unsigned i = 1;
1314 [ - - ]: 0 : for (; i < iteNode.getNumChildren(); ++i)
1315 : : {
1316 : 0 : Node n = simpConstants(simpContext, iteNode[i], simpVar);
1317 [ - - ]: 0 : if (n.isNull())
1318 : : {
1319 : 0 : return n;
1320 : : }
1321 : 0 : builder << n;
1322 : : }
1323 : : // Mark the substitution and continue
1324 : 0 : Node result = builder;
1325 : 0 : result = rewrite(result);
1326 : 0 : d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = result;
1327 : 0 : return result;
1328 : : }
1329 : :
1330 [ - - ]: 0 : if (!containsTermITE(iteNode))
1331 : : {
1332 : 0 : Node n = rewrite(simpContext.substitute(simpVar, iteNode));
1333 : 0 : d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n;
1334 : 0 : return n;
1335 : : }
1336 : :
1337 : 0 : Node iteNode2;
1338 : 0 : Node simpVar2;
1339 : 0 : d_simpContextCache.clear();
1340 : 0 : Node simpContext2 = createSimpContext(iteNode, iteNode2, simpVar2);
1341 [ - - ]: 0 : if (!simpContext2.isNull())
1342 : : {
1343 : 0 : Assert(!iteNode2.isNull());
1344 : 0 : simpContext2 = simpContext.substitute(simpVar, simpContext2);
1345 : 0 : Node n = simpConstants(simpContext2, iteNode2, simpVar2);
1346 [ - - ]: 0 : if (n.isNull())
1347 : : {
1348 : 0 : return n;
1349 : : }
1350 : 0 : d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n;
1351 : 0 : return n;
1352 : : }
1353 : 0 : return Node();
1354 : : }
1355 : :
1356 : 0 : Node ITESimplifier::getSimpVar(TypeNode t)
1357 : : {
1358 : 0 : std::unordered_map<TypeNode, Node>::iterator it;
1359 : 0 : it = d_simpVars.find(t);
1360 [ - - ]: 0 : if (it != d_simpVars.end())
1361 : : {
1362 : 0 : return (*it).second;
1363 : : }
1364 : : Node var = NodeManager::mkDummySkolem(
1365 : 0 : "iteSimp", t, "is a variable resulting from ITE simplification");
1366 : 0 : d_simpVars[t] = var;
1367 : 0 : return var;
1368 : : }
1369 : :
1370 : 0 : Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar)
1371 : : {
1372 : 0 : NodeMap::iterator it;
1373 : 0 : it = d_simpContextCache.find(c);
1374 [ - - ]: 0 : if (it != d_simpContextCache.end())
1375 : : {
1376 : 0 : return (*it).second;
1377 : : }
1378 : :
1379 [ - - ]: 0 : if (!containsTermITE(c))
1380 : : {
1381 : 0 : d_simpContextCache[c] = c;
1382 : 0 : return c;
1383 : : }
1384 : :
1385 : 0 : if (c.getKind() == Kind::ITE && !c.getType().isBoolean())
1386 : : {
1387 : : // Currently only support one ite node in a simp context
1388 : : // Return Null if more than one is found
1389 [ - - ]: 0 : if (!iteNode.isNull())
1390 : : {
1391 : 0 : return Node();
1392 : : }
1393 : 0 : simpVar = getSimpVar(c.getType());
1394 [ - - ]: 0 : if (simpVar.isNull())
1395 : : {
1396 : 0 : return Node();
1397 : : }
1398 : 0 : d_simpContextCache[c] = simpVar;
1399 : 0 : iteNode = c;
1400 : 0 : return simpVar;
1401 : : }
1402 : :
1403 : 0 : NodeBuilder builder(nodeManager(), c.getKind());
1404 [ - - ]: 0 : if (c.getMetaKind() == kind::metakind::PARAMETERIZED)
1405 : : {
1406 : 0 : builder << c.getOperator();
1407 : : }
1408 : 0 : unsigned i = 0;
1409 [ - - ]: 0 : for (; i < c.getNumChildren(); ++i)
1410 : : {
1411 : 0 : Node newChild = createSimpContext(c[i], iteNode, simpVar);
1412 [ - - ]: 0 : if (newChild.isNull())
1413 : : {
1414 : 0 : return newChild;
1415 : : }
1416 : 0 : builder << newChild;
1417 : : }
1418 : : // Mark the substitution and continue
1419 : 0 : Node result = builder;
1420 : 0 : d_simpContextCache[c] = result;
1421 : 0 : return result;
1422 : : }
1423 : : typedef std::unordered_set<Node> NodeSet;
1424 : 0 : void countReachable_(Node x, Kind k, NodeSet& visited, uint32_t& reached)
1425 : : {
1426 [ - - ]: 0 : if (visited.find(x) != visited.end())
1427 : : {
1428 : 0 : return;
1429 : : }
1430 : 0 : visited.insert(x);
1431 [ - - ]: 0 : if (x.getKind() == k)
1432 : : {
1433 : 0 : ++reached;
1434 : : }
1435 [ - - ]: 0 : for (unsigned i = 0, N = x.getNumChildren(); i < N; ++i)
1436 : : {
1437 : 0 : countReachable_(x[i], k, visited, reached);
1438 : : }
1439 : : }
1440 : :
1441 : 0 : uint32_t countReachable(TNode x, Kind k)
1442 : : {
1443 : 0 : NodeSet visited;
1444 : 0 : uint32_t reached = 0;
1445 : 0 : countReachable_(x, k, visited, reached);
1446 : 0 : return reached;
1447 : : }
1448 : :
1449 : 729 : Node ITESimplifier::simpITEAtom(TNode atom)
1450 : : {
1451 : : CVC5_UNUSED static int instance = 0;
1452 [ + - ]: 729 : Trace("ite::atom") << "still simplifying " << (++instance) << endl;
1453 : 1458 : Node attempt = transformAtom(atom);
1454 [ + - ]: 729 : Trace("ite::atom") << " finished " << instance << endl;
1455 [ + + ]: 729 : if (!attempt.isNull())
1456 : : {
1457 : 1146 : Node rewritten = rewrite(attempt);
1458 [ + - ]: 1146 : Trace("ite::print-success")
1459 : 0 : << instance << " "
1460 [ - - ]: 573 : << "rewriting " << countReachable(rewritten, Kind::ITE) << " from "
1461 [ - + ][ - + ]: 573 : << countReachable(atom, Kind::ITE) << endl
[ - - ]
1462 : 0 : << "\t rewritten " << rewritten << endl
1463 : 573 : << "\t input " << atom << endl;
1464 : 573 : return rewritten;
1465 : : }
1466 : :
1467 [ - + ]: 156 : if (leavesAreConst(atom))
1468 : : {
1469 : 0 : Node iteNode;
1470 : 0 : Node simpVar;
1471 : 0 : d_simpContextCache.clear();
1472 : 0 : Node simpContext = createSimpContext(atom, iteNode, simpVar);
1473 [ - - ]: 0 : if (!simpContext.isNull())
1474 : : {
1475 [ - - ]: 0 : if (iteNode.isNull())
1476 : : {
1477 : 0 : Assert(leavesAreConst(simpContext) && !containsTermITE(simpContext));
1478 : 0 : ++(d_statistics.d_unexpected);
1479 [ - - ]: 0 : Trace("ite::simpite") << instance << " "
1480 : 0 : << "how about?" << atom << endl;
1481 [ - - ]: 0 : Trace("ite::simpite") << instance << " "
1482 : 0 : << "\t" << simpContext << endl;
1483 : 0 : return rewrite(simpContext);
1484 : : }
1485 : 0 : Node n = simpConstants(simpContext, iteNode, simpVar);
1486 [ - - ]: 0 : if (!n.isNull())
1487 : : {
1488 : 0 : ++(d_statistics.d_unexpected);
1489 [ - - ]: 0 : Trace("ite::simpite") << instance << " "
1490 : 0 : << "here?" << atom << endl;
1491 [ - - ]: 0 : Trace("ite::simpite") << instance << " "
1492 : 0 : << "\t" << n << endl;
1493 : 0 : return n;
1494 : : }
1495 : : }
1496 : : }
1497 [ - + ]: 156 : if (TraceIsOn("ite::simpite"))
1498 : : {
1499 [ - - ]: 0 : if (countReachable(atom, Kind::ITE) > 0)
1500 : : {
1501 [ - - ]: 0 : Trace("ite::simpite") << instance << " "
1502 : 0 : << "remaining " << atom << endl;
1503 : : }
1504 : : }
1505 : 156 : ++(d_statistics.d_unsimplified);
1506 : 156 : return atom;
1507 : : }
1508 : :
1509 : : struct preprocess_stack_element
1510 : : {
1511 : : TNode d_node;
1512 : : bool d_children_added;
1513 : 2454 : preprocess_stack_element(TNode node) : d_node(node), d_children_added(false)
1514 : : {
1515 : 2454 : }
1516 : : }; /* struct preprocess_stack_element */
1517 : :
1518 : 1 : Node ITESimplifier::simpITE(TNode assertion)
1519 : : {
1520 : : // Do a topological sort of the subexpressions and substitute them
1521 : 1 : vector<preprocess_stack_element> toVisit;
1522 : 1 : toVisit.push_back(assertion);
1523 : :
1524 [ + + ]: 4373 : while (!toVisit.empty())
1525 : : {
1526 : : // cout << "call " << call << " : " << iteration << endl;
1527 : : // The current node we are processing
1528 : 4372 : preprocess_stack_element& stackHead = toVisit.back();
1529 : 4372 : TNode current = stackHead.d_node;
1530 : :
1531 : : // If node has no ITE's or already in the cache we're done, pop from the
1532 : : // stack
1533 : 13641 : if (current.getNumChildren() == 0
1534 [ + + ][ + + ]: 10386 : || (d_env.theoryOf(current) != theory::THEORY_BOOL
[ + + ][ - - ]
1535 [ + + ][ + + ]: 6014 : && !containsTermITE(current)))
[ + + ][ - - ]
1536 : : {
1537 : 525 : d_simpITECache[current] = current;
1538 : 525 : ++(d_statistics.d_simpITEVisits);
1539 : 525 : toVisit.pop_back();
1540 : 525 : continue;
1541 : : }
1542 : :
1543 : 3847 : NodeMap::iterator find = d_simpITECache.find(current);
1544 [ + + ]: 3847 : if (find != d_simpITECache.end())
1545 : : {
1546 : 11 : toVisit.pop_back();
1547 : 11 : continue;
1548 : : }
1549 : :
1550 : : // Not yet substituted, so process
1551 [ + + ]: 3836 : if (stackHead.d_children_added)
1552 : : {
1553 : : // Children have been processed, so substitute
1554 : 3836 : NodeBuilder builder(nodeManager(), current.getKind());
1555 [ - + ]: 1918 : if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
1556 : : {
1557 : 0 : builder << current.getOperator();
1558 : : }
1559 [ + + ]: 6869 : for (unsigned i = 0; i < current.getNumChildren(); ++i)
1560 : : {
1561 [ - + ][ - + ]: 4951 : Assert(d_simpITECache.find(current[i]) != d_simpITECache.end());
[ - - ]
1562 : 9902 : Node child = current[i];
1563 : 9902 : Node childRes = d_simpITECache[current[i]];
1564 : 4951 : builder << childRes;
1565 : : }
1566 : : // Mark the substitution and continue
1567 : 3836 : Node result = builder;
1568 : :
1569 : : // If this is an atom, we process it
1570 [ + + ][ - - ]: 1918 : if (d_env.theoryOf(result) != theory::THEORY_BOOL
1571 [ + + ][ + + ]: 1918 : && result.getType().isBoolean())
[ + + ][ + - ]
[ - - ]
1572 : : {
1573 : 729 : result = simpITEAtom(result);
1574 : : }
1575 : :
1576 : : // if(current != result && result.isConst()){
1577 : : // static int instance = 0;
1578 : : // //cout << instance << " " << result << current << endl;
1579 : : // }
1580 : :
1581 : 1918 : result = rewrite(result);
1582 : 1918 : d_simpITECache[current] = result;
1583 : 1918 : ++(d_statistics.d_simpITEVisits);
1584 : 1918 : toVisit.pop_back();
1585 : : }
1586 : : else
1587 : : {
1588 : : // Mark that we have added the children if any
1589 [ + - ]: 1918 : if (current.getNumChildren() > 0)
1590 : : {
1591 : 1918 : stackHead.d_children_added = true;
1592 : : // We need to add the children
1593 : 6869 : for (TNode::iterator child_it = current.begin();
1594 [ + + ]: 6869 : child_it != current.end();
1595 : 4951 : ++child_it)
1596 : : {
1597 : 9902 : TNode childNode = *child_it;
1598 : 4951 : NodeMap::iterator childFind = d_simpITECache.find(childNode);
1599 [ + + ]: 4951 : if (childFind == d_simpITECache.end())
1600 : : {
1601 : 2453 : toVisit.push_back(childNode);
1602 : : }
1603 : : }
1604 : : }
1605 : : else
1606 : : {
1607 : : // No children, so we're done
1608 : 0 : d_simpITECache[current] = current;
1609 : 0 : ++(d_statistics.d_simpITEVisits);
1610 : 0 : toVisit.pop_back();
1611 : : }
1612 : : }
1613 : : }
1614 : 2 : return d_simpITECache[assertion];
1615 : : }
1616 : :
1617 : 0 : ITECareSimplifier::ITECareSimplifier(NodeManager* nm) : d_careSetsOutstanding(0), d_usedSets()
1618 : : {
1619 : 0 : d_true = nm->mkConst<bool>(true);
1620 : 0 : d_false = nm->mkConst<bool>(false);
1621 : 0 : }
1622 : :
1623 : 0 : ITECareSimplifier::~ITECareSimplifier()
1624 : : {
1625 [ - - ][ - - ]: 0 : Assert(d_usedSets.empty());
1626 [ - - ][ - - ]: 0 : Assert(d_careSetsOutstanding == 0);
1627 : 0 : }
1628 : :
1629 : 0 : void ITECareSimplifier::clear()
1630 : : {
1631 : 0 : Assert(d_usedSets.empty());
1632 : 0 : Assert(d_careSetsOutstanding == 0);
1633 : 0 : }
1634 : :
1635 : 0 : ITECareSimplifier::CareSetPtr ITECareSimplifier::getNewSet()
1636 : : {
1637 [ - - ]: 0 : if (d_usedSets.empty())
1638 : : {
1639 : 0 : d_careSetsOutstanding++;
1640 : 0 : return ITECareSimplifier::CareSetPtr::mkNew(*this);
1641 : : }
1642 : : else
1643 : : {
1644 : : ITECareSimplifier::CareSetPtr cs =
1645 : 0 : ITECareSimplifier::CareSetPtr::recycle(d_usedSets.back());
1646 : 0 : cs.getCareSet().clear();
1647 : 0 : d_usedSets.pop_back();
1648 : 0 : return cs;
1649 : : }
1650 : : }
1651 : :
1652 : 0 : void ITECareSimplifier::updateQueue(CareMap& queue,
1653 : : TNode e,
1654 : : ITECareSimplifier::CareSetPtr& careSet)
1655 : : {
1656 : 0 : CareMap::iterator it = queue.find(e), iend = queue.end();
1657 [ - - ]: 0 : if (it != iend)
1658 : : {
1659 : 0 : set<Node>& cs2 = (*it).second.getCareSet();
1660 : 0 : ITECareSimplifier::CareSetPtr csNew = getNewSet();
1661 : 0 : set_intersection(careSet.getCareSet().begin(),
1662 : 0 : careSet.getCareSet().end(),
1663 : : cs2.begin(),
1664 : : cs2.end(),
1665 : 0 : inserter(csNew.getCareSet(), csNew.getCareSet().begin()));
1666 : 0 : (*it).second = csNew;
1667 : : }
1668 : : else
1669 : : {
1670 : 0 : queue[e] = careSet;
1671 : : }
1672 : 0 : }
1673 : :
1674 : 0 : Node ITECareSimplifier::substitute(TNode e,
1675 : : TNodeMap& substTable,
1676 : : TNodeMap& cache)
1677 : : {
1678 : 0 : TNodeMap::iterator it = cache.find(e), iend = cache.end();
1679 [ - - ]: 0 : if (it != iend)
1680 : : {
1681 : 0 : return it->second;
1682 : : }
1683 : :
1684 : : // do substitution?
1685 : 0 : it = substTable.find(e);
1686 : 0 : iend = substTable.end();
1687 [ - - ]: 0 : if (it != iend)
1688 : : {
1689 : 0 : Node result = substitute(it->second, substTable, cache);
1690 : 0 : cache[e] = result;
1691 : 0 : return result;
1692 : : }
1693 : :
1694 : 0 : size_t sz = e.getNumChildren();
1695 [ - - ]: 0 : if (sz == 0)
1696 : : {
1697 : 0 : cache[e] = e;
1698 : 0 : return e;
1699 : : }
1700 : :
1701 : 0 : NodeBuilder builder(e.getNodeManager(), e.getKind());
1702 [ - - ]: 0 : if (e.getMetaKind() == kind::metakind::PARAMETERIZED)
1703 : : {
1704 : 0 : builder << e.getOperator();
1705 : : }
1706 [ - - ]: 0 : for (unsigned i = 0; i < e.getNumChildren(); ++i)
1707 : : {
1708 : 0 : builder << substitute(e[i], substTable, cache);
1709 : : }
1710 : :
1711 : 0 : Node result = builder;
1712 : : // it = substTable.find(result);
1713 : : // if (it != iend) {
1714 : : // result = substitute(it->second, substTable, cache);
1715 : : // }
1716 : 0 : cache[e] = result;
1717 : 0 : return result;
1718 : : }
1719 : :
1720 : 0 : Node ITECareSimplifier::simplifyWithCare(TNode e)
1721 : : {
1722 : 0 : TNodeMap substTable;
1723 : :
1724 : : /* This extra block is to trigger the destructors for cs and cs2
1725 : : * before starting garbage collection.
1726 : : */
1727 : : {
1728 : 0 : CareMap queue;
1729 : 0 : CareMap::iterator it;
1730 : 0 : ITECareSimplifier::CareSetPtr cs = getNewSet();
1731 : 0 : ITECareSimplifier::CareSetPtr cs2;
1732 : 0 : queue[e] = cs;
1733 : :
1734 : 0 : TNode v;
1735 : : bool done;
1736 : : unsigned i;
1737 : :
1738 [ - - ]: 0 : while (!queue.empty())
1739 : : {
1740 : 0 : it = queue.end();
1741 : 0 : --it;
1742 : 0 : v = it->first;
1743 : 0 : cs = it->second;
1744 : 0 : set<Node>& css = cs.getCareSet();
1745 : 0 : queue.erase(v);
1746 : :
1747 : 0 : done = false;
1748 : 0 : set<Node>::iterator iCare, iCareEnd = css.end();
1749 : :
1750 : 0 : switch (v.getKind())
1751 : : {
1752 : 0 : case Kind::ITE:
1753 : : {
1754 : 0 : iCare = css.find(v[0]);
1755 [ - - ]: 0 : if (iCare != iCareEnd)
1756 : : {
1757 : 0 : Assert(substTable.find(v) == substTable.end());
1758 : 0 : substTable[v] = v[1];
1759 : 0 : updateQueue(queue, v[1], cs);
1760 : 0 : done = true;
1761 : 0 : break;
1762 : : }
1763 : : else
1764 : : {
1765 : 0 : iCare = css.find(v[0].negate());
1766 [ - - ]: 0 : if (iCare != iCareEnd)
1767 : : {
1768 : 0 : Assert(substTable.find(v) == substTable.end());
1769 : 0 : substTable[v] = v[2];
1770 : 0 : updateQueue(queue, v[2], cs);
1771 : 0 : done = true;
1772 : 0 : break;
1773 : : }
1774 : : }
1775 : 0 : updateQueue(queue, v[0], cs);
1776 : 0 : cs2 = getNewSet();
1777 : 0 : cs2.getCareSet() = css;
1778 : 0 : cs2.getCareSet().insert(v[0]);
1779 : 0 : updateQueue(queue, v[1], cs2);
1780 : 0 : cs2 = getNewSet();
1781 : 0 : cs2.getCareSet() = css;
1782 : 0 : cs2.getCareSet().insert(v[0].negate());
1783 : 0 : updateQueue(queue, v[2], cs2);
1784 : 0 : done = true;
1785 : 0 : break;
1786 : : }
1787 : 0 : case Kind::AND:
1788 : : {
1789 [ - - ]: 0 : for (i = 0; i < v.getNumChildren(); ++i)
1790 : : {
1791 : 0 : iCare = css.find(v[i].negate());
1792 [ - - ]: 0 : if (iCare != iCareEnd)
1793 : : {
1794 : 0 : Assert(substTable.find(v) == substTable.end());
1795 : 0 : substTable[v] = d_false;
1796 : 0 : done = true;
1797 : 0 : break;
1798 : : }
1799 : : }
1800 [ - - ]: 0 : if (done) break;
1801 : :
1802 : 0 : Assert(v.getNumChildren() > 1);
1803 : 0 : updateQueue(queue, v[0], cs);
1804 : 0 : cs2 = getNewSet();
1805 : 0 : cs2.getCareSet() = css;
1806 : 0 : cs2.getCareSet().insert(v[0]);
1807 [ - - ]: 0 : for (i = 1; i < v.getNumChildren(); ++i)
1808 : : {
1809 : 0 : updateQueue(queue, v[i], cs2);
1810 : : }
1811 : 0 : done = true;
1812 : 0 : break;
1813 : : }
1814 : 0 : case Kind::OR:
1815 : : {
1816 [ - - ]: 0 : for (i = 0; i < v.getNumChildren(); ++i)
1817 : : {
1818 : 0 : iCare = css.find(v[i]);
1819 [ - - ]: 0 : if (iCare != iCareEnd)
1820 : : {
1821 : 0 : Assert(substTable.find(v) == substTable.end());
1822 : 0 : substTable[v] = d_true;
1823 : 0 : done = true;
1824 : 0 : break;
1825 : : }
1826 : : }
1827 [ - - ]: 0 : if (done) break;
1828 : :
1829 : 0 : Assert(v.getNumChildren() > 1);
1830 : 0 : updateQueue(queue, v[0], cs);
1831 : 0 : cs2 = getNewSet();
1832 : 0 : cs2.getCareSet() = css;
1833 : 0 : cs2.getCareSet().insert(v[0].negate());
1834 [ - - ]: 0 : for (i = 1; i < v.getNumChildren(); ++i)
1835 : : {
1836 : 0 : updateQueue(queue, v[i], cs2);
1837 : : }
1838 : 0 : done = true;
1839 : 0 : break;
1840 : : }
1841 : 0 : default: break;
1842 : : }
1843 : :
1844 [ - - ]: 0 : if (done)
1845 : : {
1846 : 0 : continue;
1847 : : }
1848 : :
1849 [ - - ]: 0 : for (i = 0; i < v.getNumChildren(); ++i)
1850 : : {
1851 : 0 : updateQueue(queue, v[i], cs);
1852 : : }
1853 : : }
1854 : : }
1855 : : /* Perform garbage collection. */
1856 [ - - ]: 0 : while (!d_usedSets.empty())
1857 : : {
1858 : 0 : CareSetPtrVal* used = d_usedSets.back();
1859 : 0 : d_usedSets.pop_back();
1860 : 0 : Assert(used->safeToGarbageCollect());
1861 [ - - ]: 0 : delete used;
1862 : 0 : Assert(d_careSetsOutstanding > 0);
1863 : 0 : d_careSetsOutstanding--;
1864 : : }
1865 : :
1866 : 0 : TNodeMap cache;
1867 : 0 : return substitute(e, substTable, cache);
1868 : : }
1869 : :
1870 : 0 : ITECareSimplifier::CareSetPtr ITECareSimplifier::CareSetPtr::mkNew(
1871 : : ITECareSimplifier& simp)
1872 : : {
1873 : 0 : CareSetPtrVal* val = new CareSetPtrVal(simp);
1874 : 0 : return CareSetPtr(val);
1875 : : }
1876 : :
1877 : : } // namespace util
1878 : : } // namespace preprocessing
1879 : : } // namespace cvc5::internal
|
