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