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-2024 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 : 110732 : inline static bool isTermITE(TNode e)
39 : : {
40 [ + + ][ + + ]: 110732 : return (e.getKind() == Kind::ITE && !e.getType().isBoolean());
[ + + ][ - - ]
41 : : }
42 : :
43 : 188185 : inline static bool triviallyContainsNoTermITEs(TNode e)
44 : : {
45 [ + + ][ + + ]: 188185 : 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 : 89245 : CTIVStackElement(TNode c) : curr(c), pos(0) {}
84 : : }; /* CTIVStackElement */
85 : :
86 : : } // namespace ite
87 : :
88 : 50436 : ITEUtilities::ITEUtilities(Env& env)
89 : : : EnvObj(env),
90 : 50436 : d_containsVisitor(new ContainsTermITEVisitor()),
91 : : d_compressor(NULL),
92 : : d_simplifier(NULL),
93 : 100872 : d_careSimp(NULL)
94 : : {
95 [ - + ][ - + ]: 50436 : Assert(d_containsVisitor != NULL);
[ - - ]
96 : 50436 : }
97 : :
98 : 50180 : ITEUtilities::~ITEUtilities()
99 : : {
100 [ + + ]: 50180 : if (d_simplifier != NULL)
101 : : {
102 [ + - ]: 1 : delete d_simplifier;
103 : : }
104 [ + + ]: 50180 : if (d_compressor != NULL)
105 : : {
106 [ + - ]: 1 : delete d_compressor;
107 : : }
108 [ - + ]: 50180 : if (d_careSimp != NULL)
109 : : {
110 [ - - ]: 0 : delete d_careSimp;
111 : : }
112 : 50180 : }
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 : 81852 : ContainsTermITEVisitor::ContainsTermITEVisitor() : d_cache() {}
173 : 81596 : ContainsTermITEVisitor::~ContainsTermITEVisitor() {}
174 : 34212 : bool ContainsTermITEVisitor::containsTermITE(TNode e)
175 : : {
176 : : /* throughout execution skip through NOT nodes. */
177 [ - + ]: 34212 : e = (e.getKind() == Kind::NOT) ? e[0] : e;
178 [ + + ]: 34212 : if (ite::triviallyContainsNoTermITEs(e))
179 : : {
180 : 10533 : return false;
181 : : }
182 : :
183 : 23679 : NodeBoolMap::const_iterator end = d_cache.end();
184 : 23679 : NodeBoolMap::const_iterator tmp_it = d_cache.find(e);
185 [ + + ]: 23679 : if (tmp_it != end)
186 : : {
187 : 1178 : return (*tmp_it).second;
188 : : }
189 : :
190 : 22501 : bool foundTermIte = false;
191 : 22501 : std::vector<ite::CTIVStackElement> stack;
192 : 22501 : stack.push_back(ite::CTIVStackElement(e));
193 [ + + ][ + + ]: 263734 : while (!foundTermIte && !stack.empty())
[ + + ]
194 : : {
195 : 241233 : ite::CTIVStackElement& top = stack.back();
196 : 482466 : TNode curr = top.curr;
197 [ + + ]: 241233 : if (top.pos >= curr.getNumChildren())
198 : : {
199 : : // all of the children have been visited
200 : : // no term ites were found
201 : 87260 : d_cache[curr] = false;
202 : 87260 : stack.pop_back();
203 : : }
204 : : else
205 : : {
206 : : // this is someone's child
207 : 307946 : TNode child = curr[top.pos];
208 [ + + ]: 153973 : child = (child.getKind() == Kind::NOT) ? child[0] : child;
209 : 153973 : ++top.pos;
210 [ + + ]: 153973 : if (ite::triviallyContainsNoTermITEs(child))
211 : : {
212 : : // skip
213 : : }
214 : : else
215 : : {
216 : 68033 : tmp_it = d_cache.find(child);
217 [ + + ]: 68033 : if (tmp_it != end)
218 : : {
219 : 1289 : foundTermIte = (*tmp_it).second;
220 : : }
221 : : else
222 : : {
223 : 66744 : stack.push_back(ite::CTIVStackElement(child));
224 : 66744 : foundTermIte = ite::isTermITE(child);
225 : : }
226 : : }
227 : : }
228 : : }
229 [ + + ]: 22501 : 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 : 22501 : 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 : 1209 : SkolemManager* sm = nm->getSkolemManager();
350 : 3627 : Node skolem = sm->mkDummySkolem("compress", nm->booleanType());
351 : 1209 : d_compressed[rewritten] = skolem;
352 : 1209 : d_compressed[original] = skolem;
353 : 1209 : d_compressed[compressed] = skolem;
354 : :
355 : 2418 : Node iff = skolem.eqNode(rewritten);
356 : 1209 : d_assertions->push_back(iff);
357 : 1209 : ++(d_statistics.d_skolemsAdded);
358 : 1209 : return skolem;
359 : : }
360 : : }
361 : :
362 : 7109 : bool ITECompressor::multipleParents(TNode c)
363 : : {
364 : 7109 : return d_incoming.lookupIncoming(c) >= 2;
365 : : }
366 : :
367 : 1920 : Node ITECompressor::compressBooleanITEs(Node toCompress)
368 : : {
369 [ - + ][ - + ]: 1920 : Assert(toCompress.getKind() == Kind::ITE);
[ - - ]
370 [ - + ][ - + ]: 1920 : Assert(toCompress.getType().isBoolean());
[ - - ]
371 : :
372 : 1920 : if (!(toCompress[1] == d_false || toCompress[2] == d_false))
373 : : {
374 : 3840 : Node cmpCnd = compressBoolean(toCompress[0]);
375 [ - + ]: 1920 : if (cmpCnd.isConst())
376 : : {
377 [ - - ]: 0 : Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2];
378 : 0 : Node res = compressBoolean(branch);
379 : 0 : d_compressed[toCompress] = res;
380 : 0 : return res;
381 : : }
382 : : else
383 : : {
384 : 3840 : Node cmpThen = compressBoolean(toCompress[1]);
385 : 3840 : Node cmpElse = compressBoolean(toCompress[2]);
386 : 3840 : Node newIte = cmpCnd.iteNode(cmpThen, cmpElse);
387 [ + + ]: 1920 : if (multipleParents(toCompress))
388 : : {
389 : 534 : return push_back_boolean(toCompress, newIte);
390 : : }
391 : : else
392 : : {
393 : 1386 : return newIte;
394 : : }
395 : : }
396 : : }
397 : :
398 : 0 : NodeBuilder nb(Kind::AND);
399 : 0 : Node curr = toCompress;
400 : 0 : while (curr.getKind() == Kind::ITE
401 : 0 : && (curr[1] == d_false || curr[2] == d_false)
402 : 0 : && (!multipleParents(curr) || curr == toCompress))
403 : : {
404 : 0 : bool negateCnd = (curr[1] == d_false);
405 : 0 : Node compressCnd = compressBoolean(curr[0]);
406 [ - - ]: 0 : if (compressCnd.isConst())
407 : : {
408 [ - - ]: 0 : if (compressCnd.getConst<bool>() == negateCnd)
409 : : {
410 : 0 : return push_back_boolean(toCompress, d_false);
411 : : }
412 : : else
413 : : {
414 : : // equivalent to true don't push back
415 : : }
416 : : }
417 : : else
418 : : {
419 [ - - ]: 0 : Node pb = negateCnd ? compressCnd.notNode() : compressCnd;
420 : 0 : nb << pb;
421 : : }
422 [ - - ]: 0 : curr = negateCnd ? curr[2] : curr[1];
423 : : }
424 : 0 : Assert(toCompress != curr);
425 : :
426 : 0 : nb << compressBoolean(curr);
427 [ - - ]: 0 : Node res = nb.getNumChildren() == 1 ? nb[0] : (Node)nb;
428 : 0 : return push_back_boolean(toCompress, res);
429 : : }
430 : :
431 : 1122 : Node ITECompressor::compressTerm(Node toCompress)
432 : : {
433 [ + + ][ + + ]: 1122 : if (toCompress.isConst() || toCompress.isVar())
[ + + ]
434 : : {
435 : 513 : return toCompress;
436 : : }
437 : :
438 [ + + ]: 609 : if (d_compressed.find(toCompress) != d_compressed.end())
439 : : {
440 : 201 : return d_compressed[toCompress];
441 : : }
442 [ + + ]: 408 : if (toCompress.getKind() == Kind::ITE)
443 : : {
444 : 648 : Node cmpCnd = compressBoolean(toCompress[0]);
445 [ - + ]: 324 : if (cmpCnd.isConst())
446 : : {
447 [ - - ]: 0 : Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2];
448 : 0 : Node res = compressTerm(branch);
449 : 0 : d_compressed[toCompress] = res;
450 : 0 : return res;
451 : : }
452 : : else
453 : : {
454 : 648 : Node cmpThen = compressTerm(toCompress[1]);
455 : 648 : Node cmpElse = compressTerm(toCompress[2]);
456 : 648 : Node newIte = cmpCnd.iteNode(cmpThen, cmpElse);
457 : 324 : d_compressed[toCompress] = newIte;
458 : 324 : return newIte;
459 : : }
460 : : }
461 : :
462 : 168 : NodeBuilder nb(toCompress.getKind());
463 : :
464 [ - + ]: 84 : if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED)
465 : : {
466 : 0 : nb << (toCompress.getOperator());
467 : : }
468 : 252 : for (Node::iterator it = toCompress.begin(), end = toCompress.end();
469 [ + + ]: 252 : it != end;
470 : 168 : ++it)
471 : : {
472 : 168 : nb << compressTerm(*it);
473 : : }
474 : 168 : Node compressed = (Node)nb;
475 [ + + ]: 84 : if (multipleParents(toCompress))
476 : : {
477 : 13 : d_compressed[toCompress] = compressed;
478 : : }
479 : 84 : return compressed;
480 : : }
481 : :
482 : 113402 : Node ITECompressor::compressBoolean(Node toCompress)
483 : : {
484 [ + + ][ - + ]: 113402 : if (toCompress.isConst() || toCompress.isVar())
[ + + ]
485 : : {
486 : 3 : return toCompress;
487 : : }
488 [ + + ]: 113399 : if (d_compressed.find(toCompress) != d_compressed.end())
489 : : {
490 : 106221 : return d_compressed[toCompress];
491 : : }
492 [ + + ]: 7178 : else if (toCompress.getKind() == Kind::ITE)
493 : : {
494 : 1920 : return compressBooleanITEs(toCompress);
495 : : }
496 : : else
497 : : {
498 : 5258 : bool ta = ite::isTheoryAtom(toCompress);
499 : 10516 : NodeBuilder nb(toCompress.getKind());
500 [ - + ]: 5258 : if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED)
501 : : {
502 : 0 : nb << (toCompress.getOperator());
503 : : }
504 : 112878 : for (Node::iterator it = toCompress.begin(), end = toCompress.end();
505 [ + + ]: 112878 : it != end;
506 : 107620 : ++it)
507 : : {
508 : 214934 : Node pb = (ta) ? compressTerm(*it) : compressBoolean(*it);
509 : 107620 : nb << pb;
510 : : }
511 : 10516 : Node compressed = nb;
512 [ + + ][ + + ]: 5258 : if (ta || multipleParents(toCompress))
[ + + ][ + + ]
[ - - ]
513 : : {
514 : 1186 : return push_back_boolean(toCompress, compressed);
515 : : }
516 : : else
517 : : {
518 : 4072 : return compressed;
519 : : }
520 : : }
521 : : }
522 : :
523 : 1 : bool ITECompressor::compress(AssertionPipeline* assertionsToPreprocess)
524 : : {
525 : 1 : reset();
526 : :
527 : 1 : d_assertions = assertionsToPreprocess;
528 : 1 : d_incoming.computeReachability(assertionsToPreprocess->ref());
529 : :
530 : 1 : ++(d_statistics.d_compressCalls);
531 : 1 : verbose(2) << "Computed reachability" << endl;
532 : :
533 : 1 : bool nofalses = true;
534 : 1 : const std::vector<Node>& assertions = assertionsToPreprocess->ref();
535 : 1 : size_t original_size = assertions.size();
536 : 1 : verbose(2) << "compressing " << original_size << endl;
537 [ + + ][ + - ]: 5 : for (size_t i = 0; i < original_size && nofalses; ++i)
538 : : {
539 : 8 : Node assertion = assertions[i];
540 : 8 : Node compressed = compressBoolean(assertion);
541 : 4 : Node rewritten = rewrite(compressed);
542 : : // replace
543 : 4 : assertionsToPreprocess->replace(i, rewritten);
544 [ - + ][ - + ]: 4 : Assert(!d_contains->containsTermITE(rewritten));
[ - - ]
545 : :
546 : 4 : nofalses = (rewritten != d_false);
547 : : }
548 : :
549 : 1 : d_assertions = NULL;
550 : :
551 : 1 : return nofalses;
552 : : }
553 : :
554 : 1 : TermITEHeightCounter::TermITEHeightCounter() : d_termITEHeight() {}
555 : :
556 : 1 : TermITEHeightCounter::~TermITEHeightCounter() {}
557 : :
558 : 1 : void TermITEHeightCounter::clear() { d_termITEHeight.clear(); }
559 : :
560 : 0 : size_t TermITEHeightCounter::cache_size() const
561 : : {
562 : 0 : return d_termITEHeight.size();
563 : : }
564 : :
565 : : namespace ite {
566 : : struct TITEHStackElement
567 : : {
568 : : TNode curr;
569 : : unsigned pos;
570 : : uint32_t maxChildHeight;
571 : : TITEHStackElement() : curr(), pos(0), maxChildHeight(0) {}
572 : 0 : TITEHStackElement(TNode c) : curr(c), pos(0), maxChildHeight(0) {}
573 : : };
574 : : } /* namespace ite */
575 : :
576 : 0 : uint32_t TermITEHeightCounter::termITEHeight(TNode e)
577 : : {
578 [ - - ]: 0 : if (ite::triviallyContainsNoTermITEs(e))
579 : : {
580 : 0 : return 0;
581 : : }
582 : :
583 : 0 : NodeCountMap::const_iterator end = d_termITEHeight.end();
584 : 0 : NodeCountMap::const_iterator tmp_it = d_termITEHeight.find(e);
585 [ - - ]: 0 : if (tmp_it != end)
586 : : {
587 : 0 : return (*tmp_it).second;
588 : : }
589 : :
590 : 0 : uint32_t returnValue = 0;
591 : : // This is initially 0 as the very first call this is included in the max,
592 : : // but this has no effect.
593 : 0 : std::vector<ite::TITEHStackElement> stack;
594 : 0 : stack.push_back(ite::TITEHStackElement(e));
595 [ - - ]: 0 : while (!stack.empty())
596 : : {
597 : 0 : ite::TITEHStackElement& top = stack.back();
598 : 0 : top.maxChildHeight = std::max(top.maxChildHeight, returnValue);
599 : 0 : TNode curr = top.curr;
600 [ - - ]: 0 : if (top.pos >= curr.getNumChildren())
601 : : {
602 : : // done with the current node
603 [ - - ]: 0 : returnValue = top.maxChildHeight + (ite::isTermITE(curr) ? 1 : 0);
604 : 0 : d_termITEHeight[curr] = returnValue;
605 : 0 : stack.pop_back();
606 : 0 : continue;
607 : : }
608 : : else
609 : : {
610 : 0 : if (top.pos == 0 && curr.getKind() == Kind::ITE)
611 : : {
612 : 0 : ++top.pos;
613 : 0 : returnValue = 0;
614 : 0 : continue;
615 : : }
616 : : // this is someone's child
617 : 0 : TNode child = curr[top.pos];
618 : 0 : ++top.pos;
619 [ - - ]: 0 : if (ite::triviallyContainsNoTermITEs(child))
620 : : {
621 : 0 : returnValue = 0;
622 : : }
623 : : else
624 : : {
625 : 0 : tmp_it = d_termITEHeight.find(child);
626 [ - - ]: 0 : if (tmp_it != end)
627 : : {
628 : 0 : returnValue = (*tmp_it).second;
629 : : }
630 : : else
631 : : {
632 : 0 : stack.push_back(ite::TITEHStackElement(child));
633 : : }
634 : : }
635 : : }
636 : : }
637 : 0 : return returnValue;
638 : : }
639 : :
640 : 1 : ITESimplifier::ITESimplifier(Env& env, ContainsTermITEVisitor* contains)
641 : : : EnvObj(env),
642 : : d_containsVisitor(contains),
643 : : d_termITEHeight(),
644 : : d_constantLeaves(),
645 : : d_allocatedConstantLeaves(),
646 : : d_citeEqConstApplications(0),
647 : : d_constantIteEqualsConstantCache(),
648 : : d_replaceOverCache(),
649 : : d_replaceOverTermIteCache(),
650 : : d_leavesConstCache(),
651 : : d_simpConstCache(),
652 : : d_simpContextCache(),
653 : : d_simpITECache(),
654 : 1 : d_statistics(env.getStatisticsRegistry())
655 : : {
656 [ - + ][ - + ]: 1 : Assert(d_containsVisitor != NULL);
[ - - ]
657 : 1 : d_true = nodeManager()->mkConst<bool>(true);
658 : 1 : d_false = nodeManager()->mkConst<bool>(false);
659 : 1 : }
660 : :
661 : 2 : ITESimplifier::~ITESimplifier()
662 : : {
663 : 1 : clearSimpITECaches();
664 [ - + ][ - + ]: 1 : Assert(d_constantLeaves.empty());
665 [ - + ][ - + ]: 1 : Assert(d_allocatedConstantLeaves.empty());
666 : 2 : }
667 : :
668 : 156 : bool ITESimplifier::leavesAreConst(TNode e)
669 : : {
670 : 156 : return leavesAreConst(e, d_env.theoryOf(e));
671 : : }
672 : :
673 : 1 : void ITESimplifier::clearSimpITECaches()
674 : : {
675 : 1 : verbose(2) << "clear ite caches " << endl;
676 [ + + ]: 756 : for (size_t i = 0, N = d_allocatedConstantLeaves.size(); i < N; ++i)
677 : : {
678 : 755 : NodeVec* curr = d_allocatedConstantLeaves[i];
679 [ + - ]: 755 : delete curr;
680 : : }
681 : 1 : d_citeEqConstApplications = 0;
682 : 1 : d_constantLeaves.clear();
683 : 1 : d_allocatedConstantLeaves.clear();
684 : 1 : d_termITEHeight.clear();
685 : 1 : d_constantIteEqualsConstantCache.clear();
686 : 1 : d_replaceOverCache.clear();
687 : 1 : d_replaceOverTermIteCache.clear();
688 : 1 : d_simpITECache.clear();
689 : 1 : d_simpVars.clear();
690 : 1 : d_simpConstCache.clear();
691 : 1 : d_leavesConstCache.clear();
692 : 1 : d_simpContextCache.clear();
693 : 1 : }
694 : :
695 : 1 : bool ITESimplifier::doneALotOfWorkHeuristic() const
696 : : {
697 : : static const size_t SIZE_BOUND = 1000;
698 : 1 : verbose(2) << "d_citeEqConstApplications size " << d_citeEqConstApplications
699 : 1 : << endl;
700 : 1 : return (d_citeEqConstApplications > SIZE_BOUND);
701 : : }
702 : :
703 : 1 : ITESimplifier::Statistics::Statistics(StatisticsRegistry& reg)
704 : : : d_maxNonConstantsFolded(
705 : 1 : reg.registerInt("ite-simp::maxNonConstantsFolded")),
706 : 1 : d_unexpected(reg.registerInt("ite-simp::unexpected")),
707 : 1 : d_unsimplified(reg.registerInt("ite-simp::unsimplified")),
708 : 1 : d_exactMatchFold(reg.registerInt("ite-simp::exactMatchFold")),
709 : 1 : d_binaryPredFold(reg.registerInt("ite-simp::binaryPredFold")),
710 : 1 : d_specialEqualityFolds(reg.registerInt("ite-simp::specialEqualityFolds")),
711 : 1 : d_simpITEVisits(reg.registerInt("ite-simp::simpITE.visits")),
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 : 1724 : TNode thenB = ite[1];
743 : 1724 : 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 [ + + ]: 1206 : TNode definitelyITE = thenB.isConst() ? elseB : thenB;
767 [ + + ]: 1206 : 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 : 1206 : 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 : : newEnd = std::set_union(defChildren->begin(),
797 : : defChildren->end(),
798 : : maybeChildren->begin(),
799 : : maybeChildren->end(),
800 : 603 : both->begin());
801 : 603 : both->resize(newEnd - both->begin());
802 : 603 : d_constantLeaves[ite] = both;
803 : 603 : return both;
804 : : }
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(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 : : }
895 : : // Mark the substitution and continue
896 : 0 : Node result = builder;
897 : 0 : d_replaceOverCache[p] = result;
898 : 0 : return result;
899 : : }
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 : : }
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 : : }
953 : : }
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 : : }
989 : : }
990 : : }
991 : : }
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 : : }
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 : 1458 : 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 : : }
1065 : : }
1066 : :
1067 : : static unsigned numBranches = 0;
1068 : : static unsigned numFalseBranches = 0;
1069 : : static unsigned itesMade = 0;
1070 : :
1071 : 67339 : Node ITESimplifier::constantIteEqualsConstant(TNode cite, TNode constant)
1072 : : {
1073 : : static int instance = 0;
1074 : 67339 : ++instance;
1075 [ + - ]: 134678 : Trace("ite::constantIteEqualsConstant")
1076 : 0 : << instance << "constantIteEqualsConstant(" << cite << ", " << constant
1077 : 67339 : << ")" << endl;
1078 [ + + ]: 67339 : if (cite.isConst())
1079 : : {
1080 [ + + ]: 45678 : Node res = (cite == constant) ? d_true : d_false;
1081 [ + - ]: 22839 : Trace("ite::constantIteEqualsConstant") << 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 : << 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 : << 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 : ++numBranches;
1121 : : }
1122 [ + + ][ + + ]: 33383 : if (!(tEqs == d_false || fEqs == d_false))
[ + + ]
1123 : : {
1124 : 2211 : ++numFalseBranches;
1125 : : }
1126 : 33383 : ++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 : << 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 = itesMade;
1154 : 573 : unsigned preNumBranches = numBranches;
1155 : 573 : unsigned preNumFalseBranches = numFalseBranches;
1156 : 1719 : Node bterm = constantIteEqualsConstant(cite, constant);
1157 [ + - ]: 1146 : Trace("intersectConstantIte") << (numBranches - preNumBranches) << " "
1158 : 0 : << (numFalseBranches - preNumFalseBranches)
1159 : 573 : << " " << (itesMade - preItesMade) << endl;
1160 : 573 : return bterm;
1161 : : }
1162 : 0 : Assert(lcite.getKind() == Kind::ITE);
1163 : 0 : Assert(rcite.getKind() == Kind::ITE);
1164 : :
1165 : 0 : NodeVec* leftValues = computeConstantLeaves(lcite);
1166 : 0 : NodeVec* rightValues = computeConstantLeaves(rcite);
1167 : :
1168 : 0 : uint32_t smaller = std::min(leftValues->size(), rightValues->size());
1169 : :
1170 : 0 : (d_statistics.d_inSmaller) << smaller;
1171 : 0 : NodeVec intersection(smaller, Node::null());
1172 : 0 : NodeVec::iterator newEnd;
1173 : : newEnd = std::set_intersection(leftValues->begin(),
1174 : : leftValues->end(),
1175 : : rightValues->begin(),
1176 : : rightValues->end(),
1177 : 0 : intersection.begin());
1178 : 0 : intersection.resize(newEnd - intersection.begin());
1179 [ - - ]: 0 : if (intersection.empty())
1180 : : {
1181 : 0 : return d_false;
1182 : : }
1183 : : else
1184 : : {
1185 : 0 : NodeBuilder nb(Kind::OR);
1186 : 0 : NodeVec::const_iterator it = intersection.begin(), end = intersection.end();
1187 [ - - ]: 0 : for (; it != end; ++it)
1188 : : {
1189 : 0 : Node inBoth = *it;
1190 : 0 : Node lefteq = constantIteEqualsConstant(lcite, inBoth);
1191 : 0 : Node righteq = constantIteEqualsConstant(rcite, inBoth);
1192 : 0 : Node bothHold = lefteq.andNode(righteq);
1193 : 0 : nb << bothHold;
1194 : : }
1195 [ - - ]: 0 : Node result = (nb.getNumChildren() > 1) ? (Node)nb : nb[0];
1196 : 0 : return result;
1197 : : }
1198 : : }
1199 : :
1200 : 0 : Node ITESimplifier::attemptEagerRemoval(TNode atom)
1201 : : {
1202 [ - - ]: 0 : if (atom.getKind() == Kind::EQUAL)
1203 : : {
1204 : 0 : TNode left = atom[0];
1205 : 0 : TNode right = atom[1];
1206 : 0 : if ((left.isConst() && right.getKind() == Kind::ITE && isConstantIte(right))
1207 : 0 : || (right.isConst() && left.getKind() == Kind::ITE
1208 : 0 : && isConstantIte(left)))
1209 : : {
1210 [ - - ]: 0 : TNode constant = left.isConst() ? left : right;
1211 [ - - ]: 0 : TNode cite = left.isConst() ? right : left;
1212 : :
1213 : 0 : std::pair<Node, Node> pair = make_pair(cite, constant);
1214 : : NodePairMap::const_iterator eq_pos =
1215 : 0 : d_constantIteEqualsConstantCache.find(pair);
1216 [ - - ]: 0 : if (eq_pos != d_constantIteEqualsConstantCache.end())
1217 : : {
1218 : 0 : Node ret = (*eq_pos).second;
1219 [ - - ]: 0 : if (ret.isConst())
1220 : : {
1221 : 0 : return ret;
1222 : : }
1223 : : else
1224 : : {
1225 : 0 : return Node::null();
1226 : : }
1227 : : }
1228 : :
1229 : 0 : NodeVec* leaves = computeConstantLeaves(cite);
1230 : 0 : Assert(leaves != NULL);
1231 [ - - ]: 0 : if (!std::binary_search(leaves->begin(), leaves->end(), constant))
1232 : : {
1233 : 0 : d_constantIteEqualsConstantCache[pair] = d_false;
1234 : 0 : return d_false;
1235 : : }
1236 : : }
1237 : : }
1238 : 0 : return Node::null();
1239 : : }
1240 : :
1241 : 729 : Node ITESimplifier::attemptConstantRemoval(TNode atom)
1242 : : {
1243 [ + + ]: 729 : if (atom.getKind() == Kind::EQUAL)
1244 : : {
1245 : 680 : TNode left = atom[0];
1246 : 680 : TNode right = atom[1];
1247 : 680 : if (isConstantIte(left) && isConstantIte(right))
1248 : : {
1249 : 573 : return intersectConstantIte(left, right);
1250 : : }
1251 : : }
1252 : 156 : return Node::null();
1253 : : }
1254 : :
1255 : 550 : bool ITESimplifier::leavesAreConst(TNode e, theory::TheoryId tid)
1256 : : {
1257 : 731 : Assert((e.getKind() == Kind::ITE && !e.getType().isBoolean())
1258 : : || d_env.theoryOf(e) != theory::THEORY_BOOL);
1259 [ + + ]: 550 : if (e.isConst())
1260 : : {
1261 : 27 : return true;
1262 : : }
1263 : :
1264 : 523 : unordered_map<Node, bool>::iterator it;
1265 : 523 : it = d_leavesConstCache.find(e);
1266 [ + + ]: 523 : if (it != d_leavesConstCache.end())
1267 : : {
1268 : 122 : return (*it).second;
1269 : : }
1270 : :
1271 : 401 : if (!containsTermITE(e) && theory::Theory::isLeafOf(e, tid))
1272 : : {
1273 : 34 : d_leavesConstCache[e] = false;
1274 : 34 : return false;
1275 : : }
1276 : :
1277 [ - + ][ - + ]: 367 : Assert(e.getNumChildren() > 0);
[ - - ]
1278 : 367 : size_t k = 0, sz = e.getNumChildren();
1279 : :
1280 [ + + ]: 367 : if (e.getKind() == Kind::ITE)
1281 : : {
1282 : 161 : k = 1;
1283 : : }
1284 : :
1285 [ + - ]: 394 : for (; k < sz; ++k)
1286 : : {
1287 [ + + ]: 394 : if (!leavesAreConst(e[k], tid))
1288 : : {
1289 : 367 : d_leavesConstCache[e] = false;
1290 : 367 : return false;
1291 : : }
1292 : : }
1293 : 0 : d_leavesConstCache[e] = true;
1294 : 0 : return true;
1295 : : }
1296 : :
1297 : 0 : Node ITESimplifier::simpConstants(TNode simpContext,
1298 : : TNode iteNode,
1299 : : TNode simpVar)
1300 : : {
1301 : 0 : NodePairMap::iterator it;
1302 : 0 : it = d_simpConstCache.find(pair<Node, Node>(simpContext, iteNode));
1303 [ - - ]: 0 : if (it != d_simpConstCache.end())
1304 : : {
1305 : 0 : return (*it).second;
1306 : : }
1307 : :
1308 [ - - ]: 0 : if (iteNode.getKind() == Kind::ITE)
1309 : : {
1310 : 0 : NodeBuilder builder(Kind::ITE);
1311 : 0 : builder << iteNode[0];
1312 : 0 : unsigned i = 1;
1313 [ - - ]: 0 : for (; i < iteNode.getNumChildren(); ++i)
1314 : : {
1315 : 0 : Node n = simpConstants(simpContext, iteNode[i], simpVar);
1316 [ - - ]: 0 : if (n.isNull())
1317 : : {
1318 : 0 : return n;
1319 : : }
1320 : 0 : builder << n;
1321 : : }
1322 : : // Mark the substitution and continue
1323 : 0 : Node result = builder;
1324 : 0 : result = rewrite(result);
1325 : 0 : d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = result;
1326 : 0 : return result;
1327 : : }
1328 : :
1329 [ - - ]: 0 : if (!containsTermITE(iteNode))
1330 : : {
1331 : 0 : Node n = rewrite(simpContext.substitute(simpVar, iteNode));
1332 : 0 : d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n;
1333 : 0 : return n;
1334 : : }
1335 : :
1336 : 0 : Node iteNode2;
1337 : 0 : Node simpVar2;
1338 : 0 : d_simpContextCache.clear();
1339 : 0 : Node simpContext2 = createSimpContext(iteNode, iteNode2, simpVar2);
1340 [ - - ]: 0 : if (!simpContext2.isNull())
1341 : : {
1342 : 0 : Assert(!iteNode2.isNull());
1343 : 0 : simpContext2 = simpContext.substitute(simpVar, simpContext2);
1344 : 0 : Node n = simpConstants(simpContext2, iteNode2, simpVar2);
1345 [ - - ]: 0 : if (n.isNull())
1346 : : {
1347 : 0 : return n;
1348 : : }
1349 : 0 : d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n;
1350 : 0 : return n;
1351 : : }
1352 : 0 : return Node();
1353 : : }
1354 : :
1355 : 0 : Node ITESimplifier::getSimpVar(TypeNode t)
1356 : : {
1357 : 0 : std::unordered_map<TypeNode, Node>::iterator it;
1358 : 0 : it = d_simpVars.find(t);
1359 [ - - ]: 0 : if (it != d_simpVars.end())
1360 : : {
1361 : 0 : return (*it).second;
1362 : : }
1363 : 0 : SkolemManager* sm = nodeManager()->getSkolemManager();
1364 : : Node var = sm->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(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(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.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
|
