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 : : * Implementation of extended rewriting techniques.
11 : : */
12 : :
13 : : #include "theory/quantifiers/extended_rewrite.h"
14 : :
15 : : #include <sstream>
16 : :
17 : : #include "theory/arith/arith_msum.h"
18 : : #include "theory/bv/theory_bv_utils.h"
19 : : #include "theory/datatypes/datatypes_rewriter.h"
20 : : #include "theory/quantifiers/term_util.h"
21 : : #include "theory/rewriter.h"
22 : : #include "theory/strings/arith_entail.h"
23 : : #include "theory/strings/sequences_rewriter.h"
24 : : #include "theory/strings/theory_strings_utils.h"
25 : : #include "theory/strings/word.h"
26 : : #include "theory/theory.h"
27 : :
28 : : using namespace cvc5::internal::kind;
29 : : using namespace std;
30 : :
31 : : namespace cvc5::internal {
32 : : namespace theory {
33 : : namespace quantifiers {
34 : :
35 : : struct ExtRewriteAttributeId
36 : : {
37 : : };
38 : : typedef expr::Attribute<ExtRewriteAttributeId, Node> ExtRewriteAttribute;
39 : :
40 : : struct ExtRewriteAggAttributeId
41 : : {
42 : : };
43 : : typedef expr::Attribute<ExtRewriteAggAttributeId, Node> ExtRewriteAggAttribute;
44 : :
45 : 570986 : ExtendedRewriter::ExtendedRewriter(NodeManager* nm, Rewriter& rew, bool aggr)
46 : 570986 : : d_nm(nm), d_rew(rew), d_aggr(aggr)
47 : : {
48 : 570986 : d_true = d_nm->mkConst(true);
49 : 570986 : d_false = d_nm->mkConst(false);
50 : 570986 : d_intZero = d_nm->mkConstInt(Rational(0));
51 : 570986 : }
52 : :
53 : 547126 : void ExtendedRewriter::setCache(Node n, Node ret) const
54 : : {
55 [ + + ]: 547126 : if (d_aggr)
56 : : {
57 : : ExtRewriteAggAttribute erga;
58 : 540810 : n.setAttribute(erga, ret);
59 : : }
60 : : else
61 : : {
62 : : ExtRewriteAttribute era;
63 : 6316 : n.setAttribute(era, ret);
64 : : }
65 : 547126 : }
66 : :
67 : 1180314 : Node ExtendedRewriter::getCache(Node n) const
68 : : {
69 [ + + ]: 1180314 : if (d_aggr)
70 : : {
71 [ + + ]: 1165677 : if (n.hasAttribute(ExtRewriteAggAttribute()))
72 : : {
73 : 1782232 : return n.getAttribute(ExtRewriteAggAttribute());
74 : : }
75 : : }
76 : : else
77 : : {
78 [ + + ]: 14637 : if (n.hasAttribute(ExtRewriteAttribute()))
79 : : {
80 : 22958 : return n.getAttribute(ExtRewriteAttribute());
81 : : }
82 : : }
83 : 277719 : return Node::null();
84 : : }
85 : :
86 : 578402 : bool ExtendedRewriter::addToChildren(Node nc,
87 : : std::vector<Node>& children,
88 : : bool dropDup) const
89 : : {
90 : : // If the operator is non-additive, do not consider duplicates
91 : 578402 : if (dropDup
92 [ + + ][ + + ]: 578402 : && std::find(children.begin(), children.end(), nc) != children.end())
[ + + ]
93 : : {
94 : 4199 : return false;
95 : : }
96 : 574203 : children.push_back(nc);
97 : 574203 : return true;
98 : : }
99 : :
100 : 1180314 : Node ExtendedRewriter::extendedRewrite(Node n) const
101 : : {
102 [ + - ]: 1180314 : Trace("q-ext-rewrite-debug") << "extendedRewrite: " << n << std::endl;
103 : 1180314 : n = d_rew.rewrite(n);
104 : :
105 : : // has it already been computed?
106 : 1180314 : Node ncache = getCache(n);
107 [ + + ]: 1180314 : if (!ncache.isNull())
108 : : {
109 : 902595 : return ncache;
110 : : }
111 : :
112 : 277719 : Node ret = n;
113 : 277719 : NodeManager* nm = d_nm;
114 : :
115 : : //--------------------pre-rewrite
116 [ + + ]: 277719 : if (d_aggr)
117 : : {
118 : 274561 : Node pre_new_ret;
119 [ + + ]: 274561 : if (ret.getKind() == Kind::IMPLIES)
120 : : {
121 : 162 : pre_new_ret = nm->mkNode(Kind::OR, ret[0].negate(), ret[1]);
122 : 162 : debugExtendedRewrite(ret, pre_new_ret, "IMPLIES elim");
123 : : }
124 [ + + ]: 274399 : else if (ret.getKind() == Kind::XOR)
125 : : {
126 : 1966 : pre_new_ret = nm->mkNode(Kind::EQUAL, ret[0].negate(), ret[1]);
127 : 1966 : debugExtendedRewrite(ret, pre_new_ret, "XOR elim");
128 : : }
129 [ + + ]: 272433 : else if (ret.getKind() == Kind::NOT)
130 : : {
131 : 22748 : pre_new_ret = extendedRewriteNnf(ret);
132 : 22748 : debugExtendedRewrite(ret, pre_new_ret, "NNF");
133 : : }
134 [ + + ]: 274561 : if (!pre_new_ret.isNull())
135 : : {
136 : 8312 : ret = extendedRewrite(pre_new_ret);
137 : :
138 [ + - ]: 16624 : Trace("q-ext-rewrite-debug")
139 : 8312 : << "...ext-pre-rewrite : " << n << " -> " << pre_new_ret << std::endl;
140 : 8312 : setCache(n, ret);
141 : 8312 : return ret;
142 : : }
143 [ + + ]: 274561 : }
144 : : //--------------------end pre-rewrite
145 : :
146 : : //--------------------rewrite children
147 [ + + ]: 269407 : if (n.getNumChildren() > 0)
148 : : {
149 : 240252 : std::vector<Node> children;
150 [ + + ]: 240252 : if (n.getMetaKind() == metakind::PARAMETERIZED)
151 : : {
152 : 5843 : children.push_back(n.getOperator());
153 : : }
154 : 240252 : Kind k = n.getKind();
155 : 240252 : bool childChanged = false;
156 : 240252 : bool isNonAdditive = TermUtil::isNonAdditive(k);
157 : : // We flatten associative operators below, which requires k to be n-ary.
158 : 240252 : bool isAssoc = TermUtil::isAssoc(k, true);
159 [ + + ]: 809660 : for (unsigned i = 0; i < n.getNumChildren(); i++)
160 : : {
161 : 569408 : Node nc = extendedRewrite(n[i]);
162 [ + + ][ + + ]: 569408 : childChanged = nc != n[i] || childChanged;
[ + - ][ - - ]
163 [ + + ][ + + ]: 569408 : if (isAssoc && nc.getKind() == n.getKind())
[ + + ]
164 : : {
165 [ + + ]: 19622 : for (const Node& ncc : nc)
166 : : {
167 [ + + ]: 14308 : if (!addToChildren(ncc, children, isNonAdditive))
168 : : {
169 : 450 : childChanged = true;
170 : : }
171 : 14308 : }
172 : : }
173 [ + + ]: 564094 : else if (!addToChildren(nc, children, isNonAdditive))
174 : : {
175 : 3749 : childChanged = true;
176 : : }
177 : 569408 : }
178 [ - + ][ - + ]: 240252 : Assert(!children.empty());
[ - - ]
179 : : // Some commutative operators have rewriters that are agnostic to order,
180 : : // thus, we sort here.
181 [ + + ][ + + ]: 240252 : if (TermUtil::isComm(k) && (d_aggr || children.size() <= 5))
[ + + ][ + + ]
182 : : {
183 : 144542 : childChanged = true;
184 : 144542 : std::sort(children.begin(), children.end());
185 : : }
186 [ + + ]: 240252 : if (childChanged)
187 : : {
188 [ + + ][ + + ]: 158552 : if (isNonAdditive && children.size() == 1)
[ + + ]
189 : : {
190 : : // we may have subsumed children down to one
191 : 34 : ret = children[0];
192 : : }
193 : 158518 : else if (isAssoc
194 [ + + ][ + + ]: 158518 : && children.size() > kind::metakind::getMaxArityForKind(k))
[ + + ]
195 : : {
196 [ - + ][ - + ]: 2 : Assert(kind::metakind::getMaxArityForKind(k) >= 2);
[ - - ]
197 : : // kind may require binary construction
198 : 2 : ret = children[0];
199 [ + + ]: 6 : for (unsigned i = 1, nchild = children.size(); i < nchild; i++)
200 : : {
201 : 4 : ret = nm->mkNode(k, ret, children[i]);
202 : : }
203 : : }
204 : : else
205 : : {
206 : 158516 : ret = nm->mkNode(k, children);
207 : : }
208 : : }
209 : 240252 : }
210 : 269407 : ret = d_rew.rewrite(ret);
211 : : //--------------------end rewrite children
212 : :
213 : : // now, do extended rewrite
214 [ + - ]: 538814 : Trace("q-ext-rewrite-debug") << "Do extended rewrite on : " << ret
215 : 269407 : << " (from " << n << ")" << std::endl;
216 : 269407 : Node new_ret;
217 : :
218 : : //---------------------- theory-independent post-rewriting
219 [ + + ]: 269407 : if (ret.getKind() == Kind::ITE)
220 : : {
221 : 23342 : new_ret = extendedRewriteIte(Kind::ITE, ret);
222 : : }
223 [ + + ][ + + ]: 246065 : else if (ret.getKind() == Kind::AND || ret.getKind() == Kind::OR)
[ + + ]
224 : : {
225 : 71513 : new_ret = extendedRewriteAndOr(ret);
226 : : }
227 [ + + ]: 174552 : else if (ret.getKind() == Kind::EQUAL)
228 : : {
229 : 59368 : new_ret = extendedRewriteEqChain(
230 : 29684 : Kind::EQUAL, Kind::AND, Kind::OR, Kind::NOT, ret);
231 [ + + ]: 29684 : if (!new_ret.isNull())
232 : : {
233 : 2096 : debugExtendedRewrite(ret, new_ret, "Bool eq-chain simplify");
234 : : }
235 : : else
236 : : {
237 : 27588 : TypeNode tret = ret[0].getType();
238 [ + + ]: 27588 : if (tret.isInteger())
239 : : {
240 : 12372 : strings::ArithEntail ae(nm, &d_rew);
241 : 12372 : new_ret = ae.rewritePredViaEntailment(ret);
242 [ + + ]: 12372 : if (!new_ret.isNull())
243 : : {
244 : 60 : debugExtendedRewrite(ret, new_ret, "String EQUAL len entailment");
245 : : }
246 : 12372 : }
247 [ + + ]: 15216 : else if (tret.isStringLike())
248 : : {
249 : 2007 : new_ret = extendedRewriteStrings(ret);
250 : : }
251 : 27588 : }
252 : : }
253 [ + + ]: 144868 : else if (ret.getKind() == Kind::GEQ)
254 : : {
255 [ + + ]: 14098 : if (ret[0].getType().isInteger())
256 : : {
257 : 13894 : strings::ArithEntail ae(nm, &d_rew);
258 : 13894 : new_ret = ae.rewritePredViaEntailment(ret);
259 [ + + ]: 13894 : if (!new_ret.isNull())
260 : : {
261 : 38 : debugExtendedRewrite(ret, new_ret, "String GEQ len entailment");
262 : : }
263 : 13894 : }
264 : : }
265 [ + + ][ + - ]: 269407 : Assert(new_ret.isNull() || new_ret != ret);
[ - + ][ - + ]
[ - - ]
266 [ + + ][ + + ]: 269407 : if (new_ret.isNull() && ret.getKind() != Kind::ITE)
[ + + ]
267 : : {
268 : : // simple ITE pulling
269 : 229979 : new_ret = extendedRewritePullIte(Kind::ITE, ret);
270 : : }
271 : : //----------------------end theory-independent post-rewriting
272 : :
273 : : //----------------------theory-specific post-rewriting
274 [ + + ]: 269407 : if (new_ret.isNull())
275 : : {
276 : : TheoryId tid;
277 [ + + ]: 238071 : if (ret.getKind() == Kind::ITE)
278 : : {
279 : 19316 : tid = Theory::theoryOf(ret.getType());
280 : : }
281 : : else
282 : : {
283 : 218755 : tid = Theory::theoryOf(ret);
284 : : }
285 [ + - ]: 476142 : Trace("q-ext-rewrite-debug")
286 : 238071 : << "theoryOf( " << ret << " )= " << tid << std::endl;
287 [ + + ][ + ]: 238071 : switch (tid)
288 : : {
289 : 16551 : case THEORY_STRINGS: new_ret = extendedRewriteStrings(ret); break;
290 : 394 : case THEORY_SETS: new_ret = extendedRewriteSets(ret); break;
291 : 221126 : default: break;
292 : : }
293 : : }
294 : : //----------------------end theory-specific post-rewriting
295 : :
296 : : //----------------------aggressive rewrites
297 [ + + ][ + + ]: 269407 : if (new_ret.isNull() && d_aggr)
[ + + ]
298 : : {
299 : 235163 : new_ret = extendedRewriteAggr(ret);
300 : : }
301 : : //----------------------end aggressive rewrites
302 : :
303 : 269407 : setCache(n, ret);
304 [ + + ]: 269407 : if (!new_ret.isNull())
305 : : {
306 : 31456 : ret = extendedRewrite(new_ret);
307 : : }
308 [ + - ]: 538814 : Trace("q-ext-rewrite-debug")
309 : 269407 : << "...ext-rewrite : " << n << " -> " << ret << std::endl;
310 [ - + ]: 269407 : if (TraceIsOn("q-ext-rewrite-nf"))
311 : : {
312 [ - - ]: 0 : if (n == ret)
313 : : {
314 [ - - ]: 0 : Trace("q-ext-rewrite-nf") << "ext-rew normal form : " << n << std::endl;
315 : : }
316 : : }
317 : 269407 : setCache(n, ret);
318 : 269407 : return ret;
319 : 1180314 : }
320 : :
321 : 235163 : Node ExtendedRewriter::extendedRewriteAggr(Node n) const
322 : : {
323 : 235163 : Node new_ret;
324 [ + - ]: 470326 : Trace("q-ext-rewrite-debug2")
325 : 235163 : << "Do aggressive rewrites on " << n << std::endl;
326 : 235163 : bool polarity = n.getKind() != Kind::NOT;
327 [ + + ]: 235163 : Node ret_atom = n.getKind() == Kind::NOT ? n[0] : n;
328 : 262805 : if ((ret_atom.getKind() == Kind::EQUAL && ret_atom[0].getType().isRealOrInt())
329 [ + + ][ + + ]: 262805 : || ret_atom.getKind() == Kind::GEQ)
[ + + ]
330 : : {
331 : : // ITE term removal in polynomials
332 : : // e.g. ite( x=0, x, y ) = x+1 ---> ( x=0 ^ y = x+1 )
333 [ + - ]: 58614 : Trace("q-ext-rewrite-debug2")
334 : 29307 : << "Compute monomial sum " << ret_atom << std::endl;
335 : : // compute monomial sum
336 : 29307 : std::map<Node, Node> msum;
337 [ + - ]: 29307 : if (ArithMSum::getMonomialSumLit(ret_atom, msum))
338 : : {
339 [ + + ]: 90879 : for (std::map<Node, Node>::iterator itm = msum.begin(); itm != msum.end();
340 : 61572 : ++itm)
341 : : {
342 : 61636 : Node v = itm->first;
343 [ + - ]: 123272 : Trace("q-ext-rewrite-debug2")
344 : 61636 : << itm->first << " * " << itm->second << std::endl;
345 [ + + ]: 61636 : if (v.getKind() == Kind::ITE)
346 : : {
347 : 1370 : Node veq;
348 : 1370 : int res = ArithMSum::isolate(v, msum, veq, ret_atom.getKind());
349 [ + - ]: 1370 : if (res != 0)
350 : : {
351 [ + - ]: 2740 : Trace("q-ext-rewrite-debug")
352 : 1370 : << " have ITE relation, solved form : " << veq << std::endl;
353 : : // try pulling ITE
354 : 1370 : new_ret = extendedRewritePullIte(Kind::ITE, veq);
355 [ + + ]: 1370 : if (!new_ret.isNull())
356 : : {
357 [ - + ]: 64 : if (!polarity)
358 : : {
359 : 0 : new_ret = new_ret.negate();
360 : : }
361 : 64 : break;
362 : : }
363 : : }
364 : : else
365 : : {
366 [ - - ]: 0 : Trace("q-ext-rewrite-debug")
367 : 0 : << " failed to isolate " << v << " in " << n << std::endl;
368 : : }
369 [ + + ]: 1370 : }
370 [ + + ]: 61636 : }
371 : : }
372 : : else
373 : : {
374 [ - - ]: 0 : Trace("q-ext-rewrite-debug")
375 : 0 : << " failed to get monomial sum of " << n << std::endl;
376 : : }
377 : 29307 : }
378 : : // TODO (#1706) : conditional rewriting, condition merging
379 : 470326 : return new_ret;
380 : 235163 : }
381 : :
382 : 33261 : Node ExtendedRewriter::extendedRewriteIte(Kind itek, Node n, bool full) const
383 : : {
384 [ - + ][ - + ]: 33261 : Assert(n.getKind() == itek);
[ - - ]
385 [ - + ][ - + ]: 33261 : Assert(n[1] != n[2]);
[ - - ]
386 : :
387 : 33261 : NodeManager* nm = d_nm;
388 : :
389 [ + - ]: 33261 : Trace("ext-rew-ite") << "Rewrite ITE : " << n << std::endl;
390 : :
391 : 33261 : Node flip_cond;
392 [ - + ]: 33261 : if (n[0].getKind() == Kind::NOT)
393 : : {
394 : 0 : flip_cond = n[0][0];
395 : : }
396 [ + + ]: 33261 : else if (n[0].getKind() == Kind::OR)
397 : : {
398 : : // a | b ---> ~( ~a & ~b )
399 : 344 : flip_cond = TermUtil::simpleNegate(n[0]);
400 : : }
401 [ + + ]: 33261 : if (!flip_cond.isNull())
402 : : {
403 : 688 : Node new_ret = nm->mkNode(Kind::ITE, flip_cond, n[2], n[1]);
404 : : // only print debug trace if full=true
405 [ + - ]: 344 : if (full)
406 : : {
407 : 344 : debugExtendedRewrite(n, new_ret, "ITE flip");
408 : : }
409 : 344 : return new_ret;
410 : 344 : }
411 : : // Boolean true/false return
412 : 32917 : TypeNode tn = n.getType();
413 [ + + ]: 32917 : if (tn.isBoolean())
414 : : {
415 [ + + ]: 43962 : for (unsigned i = 1; i <= 2; i++)
416 : : {
417 [ - + ]: 29308 : if (n[i].isConst())
418 : : {
419 : 0 : Node cond = i == 1 ? n[0] : n[0].negate();
420 [ - - ]: 0 : Node other = n[i == 1 ? 2 : 1];
421 : 0 : Kind retk = Kind::AND;
422 [ - - ]: 0 : if (n[i].getConst<bool>())
423 : : {
424 : 0 : retk = Kind::OR;
425 : : }
426 : : else
427 : : {
428 : 0 : cond = cond.negate();
429 : : }
430 : 0 : Node new_ret = nm->mkNode(retk, cond, other);
431 [ - - ]: 0 : if (full)
432 : : {
433 : : // ite( A, true, B ) ---> A V B
434 : : // ite( A, false, B ) ---> ~A /\ B
435 : : // ite( A, B, true ) ---> ~A V B
436 : : // ite( A, B, false ) ---> A /\ B
437 : 0 : debugExtendedRewrite(n, new_ret, "ITE const return");
438 : : }
439 : 0 : return new_ret;
440 : 0 : }
441 : : }
442 : : }
443 : :
444 : : // get entailed equalities in the condition
445 : 32917 : std::vector<Node> eq_conds;
446 : 32917 : Kind ck = n[0].getKind();
447 [ + + ]: 32917 : if (ck == Kind::EQUAL)
448 : : {
449 : 16763 : eq_conds.push_back(n[0]);
450 : : }
451 [ + + ]: 16154 : else if (ck == Kind::AND)
452 : : {
453 [ + + ]: 30302 : for (const Node& cn : n[0])
454 : : {
455 [ + + ]: 24422 : if (cn.getKind() == Kind::EQUAL)
456 : : {
457 : 2290 : eq_conds.push_back(cn);
458 : : }
459 : 30302 : }
460 : : }
461 : :
462 : 32917 : Node new_ret;
463 : 32917 : Node b;
464 : 32917 : Node e;
465 : 32917 : Node t1 = n[1];
466 : 32917 : Node t2 = n[2];
467 : 32917 : std::stringstream ss_reason;
468 : :
469 [ + + ]: 51846 : for (const Node& eq : eq_conds)
470 : : {
471 : : // simple invariant ITE
472 [ + + ]: 56968 : for (unsigned i = 0; i <= 1; i++)
473 : : {
474 : : // ite( x = y ^ C, y, x ) ---> x
475 : : // this is subsumed by the rewrites below
476 : 38039 : if (t2 == eq[i] && t1 == eq[1 - i])
477 : : {
478 : 124 : new_ret = t2;
479 : 124 : ss_reason << "ITE simple rev subs";
480 : 124 : break;
481 : : }
482 : : }
483 [ + + ]: 19053 : if (!new_ret.isNull())
484 : : {
485 : 124 : break;
486 : : }
487 : : }
488 [ + + ]: 32917 : if (new_ret.isNull())
489 : : {
490 : : // merging branches
491 [ + + ]: 96927 : for (unsigned i = 1; i <= 2; i++)
492 : : {
493 [ + + ]: 65150 : if (n[i].getKind() == Kind::ITE)
494 : : {
495 : 11382 : Node no = n[3 - i];
496 [ + + ]: 32782 : for (unsigned j = 1; j <= 2; j++)
497 : : {
498 [ + + ]: 22416 : if (n[i][j] == no)
499 : : {
500 : : // e.g.
501 : : // ite( C1, ite( C2, t1, t2 ), t1 ) ----> ite( C1 ^ ~C2, t2, t1 )
502 [ + + ][ + + ]: 1016 : Node nc1 = i == 2 ? n[0].negate() : n[0];
[ - - ]
503 : 2032 : Node nc2 = j == 1 ? n[i][0].negate() : n[i][0];
504 : 2032 : Node new_cond = nm->mkNode(Kind::AND, nc1, nc2);
505 : 1016 : new_ret = nm->mkNode(Kind::ITE, new_cond, n[i][3 - j], no);
506 : 1016 : ss_reason << "ITE merge branch";
507 : 1016 : break;
508 : 1016 : }
509 : : }
510 : 11382 : }
511 [ + + ]: 65150 : if (!new_ret.isNull())
512 : : {
513 : 1016 : break;
514 : : }
515 : : }
516 : : }
517 : :
518 [ + + ][ + + ]: 32917 : if (new_ret.isNull() && d_aggr)
[ + + ]
519 : : {
520 : : // If x is less than t based on an ordering, then we use { x -> t } as a
521 : : // substitution to the children of ite( x = t ^ C, s, t ) below.
522 : 31771 : Subs subs;
523 : 31771 : inferSubstitution(n[0], subs, true);
524 : :
525 [ + - ]: 31771 : if (!subs.empty())
526 : : {
527 : : // reverse substitution to opposite child
528 : : // r{ x -> t } = s implies ite( x=t ^ C, s, r ) ---> r
529 : : // We can use ordinary substitute since the result of the substitution
530 : : // is not being returned. In other words, nn is only being used to query
531 : : // whether the second branch is a generalization of the first.
532 : 31771 : Node nn = subs.apply(t2);
533 [ + + ]: 31771 : if (nn != t2)
534 : : {
535 : 13542 : nn = d_rew.rewrite(nn);
536 [ + + ]: 13542 : if (nn == t1)
537 : : {
538 : 172 : new_ret = t2;
539 : 172 : ss_reason << "ITE rev subs";
540 : : }
541 : : }
542 : :
543 : : // ite( x=t ^ C, s, r ) ---> ite( x=t ^ C, s{ x -> t }, r )
544 : : // must use partial substitute here, to avoid substitution into witness
545 : 31771 : std::map<Kind, bool> rkinds;
546 : 31771 : nn = partialSubstitute(t1, subs, rkinds);
547 : 31771 : nn = d_rew.rewrite(nn);
548 [ + + ]: 31771 : if (nn != t1)
549 : : {
550 : : // If full=false, then we've duplicated a term u in the children of n.
551 : : // For example, when ITE pulling, we have n is of the form:
552 : : // ite( C, f( u, t1 ), f( u, t2 ) )
553 : : // We must show that at least one copy of u dissappears in this case.
554 [ + + ]: 7104 : if (nn == t2)
555 : : {
556 : 158 : new_ret = nn;
557 : 158 : ss_reason << "ITE subs invariant";
558 : : }
559 [ + + ][ + + ]: 6946 : else if (full || nn.isConst())
[ + + ]
560 : : {
561 : 2238 : new_ret = nm->mkNode(itek, n[0], nn, t2);
562 : 2238 : ss_reason << "ITE subs";
563 : : }
564 : : }
565 : 31771 : }
566 [ + + ]: 31771 : if (new_ret.isNull())
567 : : {
568 : : // ite( C, t, s ) ----> ite( C, t, s { C -> false } )
569 : : // use partial substitute to avoid substitution into witness
570 : 29203 : std::map<Node, Node> assign;
571 : 29203 : assign[n[0]] = d_false;
572 : 29203 : std::map<Kind, bool> rkinds;
573 : 29203 : Node nn = partialSubstitute(t2, assign, rkinds);
574 [ + + ]: 29203 : if (nn != t2)
575 : : {
576 : 3988 : nn = d_rew.rewrite(nn);
577 [ + + ]: 3988 : if (nn == t1)
578 : : {
579 : 68 : new_ret = nn;
580 : 68 : ss_reason << "ITE subs invariant false";
581 : : }
582 [ + + ][ - + ]: 3920 : else if (full || nn.isConst())
[ + + ]
583 : : {
584 : 572 : new_ret = nm->mkNode(itek, n[0], t1, nn);
585 : 572 : ss_reason << "ITE subs false";
586 : : }
587 : : }
588 : 29203 : }
589 : 31771 : }
590 : :
591 : : // only print debug trace if full=true
592 [ + + ][ + + ]: 32917 : if (!new_ret.isNull() && full)
[ + + ]
593 : : {
594 : 3682 : debugExtendedRewrite(n, new_ret, ss_reason.str().c_str());
595 : : }
596 : :
597 : 32917 : return new_ret;
598 : 33261 : }
599 : :
600 : 71513 : Node ExtendedRewriter::extendedRewriteAndOr(Node n) const
601 : : {
602 : : // all the below rewrites are aggressive
603 [ + + ]: 71513 : if (!d_aggr)
604 : : {
605 : 66 : return Node::null();
606 : : }
607 : 71447 : Node new_ret;
608 : : // we allow substitutions to recurse over any kind, except WITNESS which is
609 : : // managed by partialSubstitute.
610 : 71447 : std::map<Kind, bool> bcp_kinds;
611 : 71447 : new_ret = extendedRewriteBcp(Kind::AND, Kind::OR, Kind::NOT, bcp_kinds, n);
612 [ + + ]: 71447 : if (!new_ret.isNull())
613 : : {
614 : 3206 : debugExtendedRewrite(n, new_ret, "Bool bcp");
615 : 3206 : return new_ret;
616 : : }
617 : : // factoring
618 : 68241 : new_ret = extendedRewriteFactoring(Kind::AND, Kind::OR, n);
619 [ + + ]: 68241 : if (!new_ret.isNull())
620 : : {
621 : 1054 : debugExtendedRewrite(n, new_ret, "Bool factoring");
622 : 1054 : return new_ret;
623 : : }
624 : :
625 : : // equality resolution
626 : 134374 : new_ret = extendedRewriteEqRes(
627 : 67187 : Kind::AND, Kind::OR, Kind::EQUAL, Kind::NOT, bcp_kinds, n, false);
628 : 67187 : debugExtendedRewrite(n, new_ret, "Bool eq res");
629 : 67187 : return new_ret;
630 : 71447 : }
631 : :
632 : 231349 : Node ExtendedRewriter::extendedRewritePullIte(Kind itek, Node n) const
633 : : {
634 [ - + ][ - + ]: 231349 : Assert(n.getKind() != Kind::ITE);
[ - - ]
635 [ + + ]: 231349 : if (n.isClosure())
636 : : {
637 : : // don't pull ITE out of quantifiers
638 : 1473 : return n;
639 : : }
640 : 229876 : NodeManager* nm = d_nm;
641 : 229876 : TypeNode tn = n.getType();
642 : 229876 : std::vector<Node> children;
643 : 229876 : bool hasOp = (n.getMetaKind() == metakind::PARAMETERIZED);
644 [ + + ]: 229876 : if (hasOp)
645 : : {
646 : 5986 : children.push_back(n.getOperator());
647 : : }
648 : 229876 : unsigned nchildren = n.getNumChildren();
649 [ + + ]: 686720 : for (unsigned i = 0; i < nchildren; i++)
650 : : {
651 : 456844 : children.push_back(n[i]);
652 : : }
653 : 229876 : std::map<unsigned, std::map<unsigned, Node> > ite_c;
654 [ + + ]: 671634 : for (unsigned i = 0; i < nchildren; i++)
655 : : {
656 : : // these rewrites in this loop are currently classified as not aggressive,
657 : : // although in previous versions they were classified as aggressive. These
658 : : // are shown to help in some Kind2 problems.
659 [ + + ]: 450907 : if (n[i].getKind() == itek)
660 : : {
661 [ + + ]: 19334 : unsigned ii = hasOp ? i + 1 : i;
662 [ + + ]: 58002 : for (unsigned j = 0; j < 2; j++)
663 : : {
664 : 38668 : children[ii] = n[i][j + 1];
665 : 38668 : Node pull = nm->mkNode(n.getKind(), children);
666 : 38668 : Node pullr = d_rew.rewrite(pull);
667 : 38668 : children[ii] = n[i];
668 : 38668 : ite_c[i][j] = pullr;
669 : 38668 : }
670 [ + + ]: 19334 : if (ite_c[i][0] == ite_c[i][1])
671 : : {
672 : : // ITE dual invariance
673 : : // f( t1..s1..tn ) ---> t and f( t1..s2..tn ) ---> t implies
674 : : // f( t1..ite( A, s1, s2 )..tn ) ---> t
675 : 889 : debugExtendedRewrite(n, ite_c[i][0], "ITE dual invariant");
676 : 1778 : return ite_c[i][0];
677 : : }
678 : 31104 : if (nchildren == 2 && (n[1 - i].isVar() || n[1 - i].isConst())
679 : 31104 : && !n[1 - i].getType().isBoolean() && tn.isBoolean())
680 : : {
681 : : // always pull variable or constant with binary (theory) predicate
682 : : // e.g. P( x, ite( A, t1, t2 ) ) ---> ite( A, P( x, t1 ), P( x, t2 ) )
683 : 14128 : Node new_ret = nm->mkNode(Kind::ITE, n[i][0], ite_c[i][0], ite_c[i][1]);
684 : 7064 : debugExtendedRewrite(n, new_ret, "ITE pull var predicate");
685 : 7064 : return new_ret;
686 : 7064 : }
687 [ + + ]: 32207 : for (unsigned j = 0; j < 2; j++)
688 : : {
689 : 22022 : Node pullr = ite_c[i][j];
690 : 22022 : if (pullr.isConst() || pullr == n[i][j + 1])
691 : : {
692 : : // ITE single child elimination
693 : : // f( t1..s1..tn ) ---> t where t is a constant or s1 itself
694 : : // implies
695 : : // f( t1..ite( A, s1, s2 )..tn ) ---> ite( A, t, f( t1..s2..tn ) )
696 : 1196 : Node new_ret;
697 [ + + ][ + - ]: 1196 : if (tn.isBoolean() && pullr.isConst())
[ + + ]
698 : : {
699 : : // remove false/true child immediately
700 : 104 : bool pol = pullr.getConst<bool>();
701 : 104 : std::vector<Node> new_children;
702 : 104 : new_children.push_back((j == 0) == pol ? n[i][0]
703 : : : n[i][0].negate());
704 : 104 : new_children.push_back(ite_c[i][1 - j]);
705 [ + + ]: 104 : new_ret = nm->mkNode(pol ? Kind::OR : Kind::AND, new_children);
706 : 104 : debugExtendedRewrite(n, new_ret, "ITE Bool single elim");
707 : 104 : }
708 : : else
709 : : {
710 : 1092 : new_ret = nm->mkNode(itek, n[i][0], ite_c[i][0], ite_c[i][1]);
711 : 1092 : debugExtendedRewrite(n, new_ret, "ITE single elim");
712 : : }
713 : 1196 : return new_ret;
714 : 1196 : }
715 [ + + ]: 22022 : }
716 : : }
717 : : }
718 [ + + ]: 220727 : if (d_aggr)
719 : : {
720 [ + + ]: 227122 : for (std::pair<const unsigned, std::map<unsigned, Node> >& ip : ite_c)
721 : : {
722 : 9919 : Node nite = n[ip.first];
723 [ - + ][ - + ]: 9919 : Assert(nite.getKind() == itek);
[ - - ]
724 : : // now, simply pull the ITE and try ITE rewrites
725 : 19838 : Node pull_ite = nm->mkNode(itek, nite[0], ip.second[0], ip.second[1]);
726 : 9919 : pull_ite = d_rew.rewrite(pull_ite);
727 [ + - ]: 9919 : if (pull_ite.getKind() == Kind::ITE)
728 : : {
729 : 9919 : Node new_pull_ite = extendedRewriteIte(itek, pull_ite, false);
730 [ + + ]: 9919 : if (!new_pull_ite.isNull())
731 : : {
732 : 666 : debugExtendedRewrite(n, new_pull_ite, "ITE pull rewrite");
733 : 666 : return new_pull_ite;
734 : : }
735 [ + + ]: 9919 : }
736 : : else
737 : : {
738 : : // A general rewrite could eliminate the ITE by pulling.
739 : : // An example is:
740 : : // ~( ite( C, ~x, ~ite( C, y, x ) ) ) --->
741 : : // ite( C, ~~x, ite( C, y, x ) ) --->
742 : : // x
743 : : // where ~ is bitvector negation.
744 : 0 : debugExtendedRewrite(n, pull_ite, "ITE pull basic elim");
745 : 0 : return pull_ite;
746 : : }
747 [ + + ][ + + ]: 10585 : }
748 : : }
749 : :
750 : 220061 : return Node::null();
751 : 229876 : }
752 : :
753 : 22748 : Node ExtendedRewriter::extendedRewriteNnf(Node ret) const
754 : : {
755 [ - + ][ - + ]: 22748 : Assert(ret.getKind() == Kind::NOT);
[ - - ]
756 : :
757 : 22748 : Kind nk = ret[0].getKind();
758 : 22748 : bool neg_ch = false;
759 : 22748 : bool neg_ch_1 = false;
760 [ + + ][ + + ]: 22748 : if (nk == Kind::AND || nk == Kind::OR)
761 : : {
762 : 4165 : neg_ch = true;
763 [ + + ]: 4165 : nk = nk == Kind::AND ? Kind::OR : Kind::AND;
764 : : }
765 [ - + ]: 18583 : else if (nk == Kind::IMPLIES)
766 : : {
767 : 0 : neg_ch = true;
768 : 0 : neg_ch_1 = true;
769 : 0 : nk = Kind::AND;
770 : : }
771 [ + + ]: 18583 : else if (nk == Kind::ITE)
772 : : {
773 : 1555 : neg_ch = true;
774 : 1555 : neg_ch_1 = true;
775 : : }
776 [ + + ]: 17028 : else if (nk == Kind::XOR)
777 : : {
778 : 64 : nk = Kind::EQUAL;
779 : : }
780 : 16964 : else if (nk == Kind::EQUAL && ret[0][0].getType().isBoolean())
781 : : {
782 : 400 : neg_ch_1 = true;
783 : : }
784 : : else
785 : : {
786 : 16564 : return Node::null();
787 : : }
788 : :
789 : 6184 : std::vector<Node> new_children;
790 [ + + ]: 26187 : for (unsigned i = 0, nchild = ret[0].getNumChildren(); i < nchild; i++)
791 : : {
792 : 20003 : Node c = ret[0][i];
793 [ + + ][ + + ]: 20003 : c = (i == 0 ? neg_ch_1 : false) != neg_ch ? c.negate() : c;
[ + + ]
794 : 20003 : new_children.push_back(c);
795 : 20003 : }
796 : 6184 : return d_nm->mkNode(nk, new_children);
797 : 6184 : }
798 : :
799 : 71447 : Node ExtendedRewriter::extendedRewriteBcp(Kind andk,
800 : : Kind ork,
801 : : Kind notk,
802 : : std::map<Kind, bool>& bcp_kinds,
803 : : Node ret) const
804 : : {
805 : 71447 : Kind k = ret.getKind();
806 [ + + ][ + - ]: 71447 : Assert(k == andk || k == ork);
[ - + ][ - + ]
[ - - ]
807 [ + - ]: 71447 : Trace("ext-rew-bcp") << "BCP: **** INPUT: " << ret << std::endl;
808 : :
809 : 71447 : NodeManager* nm = d_nm;
810 : :
811 : 71447 : TypeNode tn = ret.getType();
812 : 71447 : Node truen = TermUtil::mkTypeMaxValue(tn);
813 : 71447 : Node falsen = TermUtil::mkTypeValue(tn, 0);
814 : :
815 : : // terms to process
816 : 71447 : std::vector<Node> to_process;
817 [ + + ]: 265670 : for (const Node& cn : ret)
818 : : {
819 : 194223 : to_process.push_back(cn);
820 : 194223 : }
821 : : // the processing terms
822 : 71447 : std::vector<Node> clauses;
823 : : // the terms we have propagated information to
824 : 71447 : std::unordered_set<Node> prop_clauses;
825 : : // the assignment
826 : 71447 : std::map<Node, Node> assign;
827 : 71447 : std::vector<Node> avars;
828 : 71447 : std::vector<Node> asubs;
829 : :
830 [ + + ]: 71447 : Kind ok = k == andk ? ork : andk;
831 : : // global polarity : when k=ork, everything is negated
832 : 71447 : bool gpol = k == andk;
833 : :
834 : : do
835 : : {
836 : : // process the current nodes
837 [ + + ]: 147742 : while (!to_process.empty())
838 : : {
839 : 74529 : std::vector<Node> new_to_process;
840 [ + + ]: 272039 : for (const Node& cn : to_process)
841 : : {
842 [ + - ]: 198368 : Trace("ext-rew-bcp-debug") << "process " << cn << std::endl;
843 : 198368 : Kind cnk = cn.getKind();
844 : 198368 : bool pol = cnk != notk;
845 [ + + ]: 198368 : Node cln = cnk == notk ? cn[0] : cn;
846 [ - + ][ - + ]: 198368 : Assert(cln.getKind() != notk);
[ - - ]
847 [ + + ][ + + ]: 198368 : if ((pol && cln.getKind() == k) || (!pol && cln.getKind() == ok))
[ + + ][ + + ]
[ + + ]
848 : : {
849 : : // flatten
850 [ + + ]: 1582 : for (const Node& ccln : cln)
851 : : {
852 [ + + ][ + + ]: 1114 : Node lccln = pol ? ccln : TermUtil::mkNegate(notk, ccln);
[ - - ]
853 : 1114 : new_to_process.push_back(lccln);
854 : 1114 : }
855 : : }
856 : : else
857 : : {
858 : : // add it to the assignment
859 [ + + ]: 197900 : Node val = gpol == pol ? truen : falsen;
860 : 197900 : std::map<Node, Node>::iterator it = assign.find(cln);
861 [ + - ]: 395800 : Trace("ext-rew-bcp")
862 : 197900 : << "BCP: assign " << cln << " -> " << val << std::endl;
863 [ + + ]: 197900 : if (it != assign.end())
864 : : {
865 [ + + ]: 964 : if (val != it->second)
866 : : {
867 [ + - ]: 858 : Trace("ext-rew-bcp") << "BCP: conflict!" << std::endl;
868 : : // a conflicting assignment: we are done
869 [ + + ]: 858 : return gpol ? falsen : truen;
870 : : }
871 : : }
872 : : else
873 : : {
874 : 196936 : assign[cln] = val;
875 : 196936 : avars.push_back(cln);
876 : 196936 : asubs.push_back(val);
877 : : }
878 : :
879 : : // also, treat it as clause if possible
880 : 197042 : if (cln.getNumChildren() > 0
881 [ + + ][ - + ]: 197042 : && (bcp_kinds.empty()
882 [ - - ][ + + ]: 197042 : || bcp_kinds.find(cln.getKind()) != bcp_kinds.end()))
883 : : {
884 : 171815 : if (std::find(clauses.begin(), clauses.end(), cn) == clauses.end()
885 [ + + ][ + - ]: 171815 : && prop_clauses.find(cn) == prop_clauses.end())
[ + + ]
886 : : {
887 [ + - ]: 171715 : Trace("ext-rew-bcp") << "BCP: new clause: " << cn << std::endl;
888 : 171715 : clauses.push_back(cn);
889 : : }
890 : : }
891 [ + + ]: 197900 : }
892 [ + + ]: 198368 : }
893 : 73671 : to_process.clear();
894 : 147342 : to_process.insert(
895 : 73671 : to_process.end(), new_to_process.begin(), new_to_process.end());
896 [ + + ]: 74529 : }
897 : :
898 : : // apply substitution to all subterms of clauses
899 : 73213 : std::vector<Node> new_clauses;
900 [ + + ]: 248624 : for (const Node& c : clauses)
901 : : {
902 : 175411 : bool cpol = c.getKind() != notk;
903 [ + + ]: 175411 : Node ca = c.getKind() == notk ? c[0] : c;
904 : 175411 : bool childChanged = false;
905 : 175411 : std::vector<Node> ccs_children;
906 [ + + ]: 583151 : for (const Node& cc : ca)
907 : : {
908 : : // always use partial substitute, to avoid substitution in witness
909 [ + - ]: 407740 : Trace("ext-rew-bcp-debug") << "...do partial substitute" << std::endl;
910 : : // substitution is only applicable to compatible kinds in bcp_kinds
911 : 407740 : Node ccs = partialSubstitute(cc, assign, bcp_kinds);
912 [ + + ][ + + ]: 407740 : childChanged = childChanged || ccs != cc;
913 : 407740 : ccs_children.push_back(ccs);
914 : 407740 : }
915 [ + + ]: 175411 : if (childChanged)
916 : : {
917 [ - + ]: 3590 : if (ca.getMetaKind() == metakind::PARAMETERIZED)
918 : : {
919 : 0 : ccs_children.insert(ccs_children.begin(), ca.getOperator());
920 : : }
921 : 3590 : Node ccs = nm->mkNode(ca.getKind(), ccs_children);
922 [ + + ][ + + ]: 3590 : ccs = cpol ? ccs : TermUtil::mkNegate(notk, ccs);
[ - - ]
923 [ + - ]: 7180 : Trace("ext-rew-bcp")
924 : 3590 : << "BCP: propagated " << c << " -> " << ccs << std::endl;
925 : 3590 : ccs = d_rew.rewrite(ccs);
926 [ + - ]: 3590 : Trace("ext-rew-bcp") << "BCP: rewritten to " << ccs << std::endl;
927 : 3590 : to_process.push_back(ccs);
928 : : // store this as a node that propagation touched. This marks c so that
929 : : // it will not be included in the final construction.
930 : 3590 : prop_clauses.insert(ca);
931 : 3590 : }
932 : : else
933 : : {
934 : 171821 : new_clauses.push_back(c);
935 : : }
936 : 175411 : }
937 : 73213 : clauses.clear();
938 : 73213 : clauses.insert(clauses.end(), new_clauses.begin(), new_clauses.end());
939 [ + + ]: 73213 : } while (!to_process.empty());
940 : :
941 : : // remake the node
942 [ + + ]: 70589 : if (!prop_clauses.empty())
943 : : {
944 : 2348 : std::vector<Node> children;
945 [ + + ]: 15718 : for (std::pair<const Node, Node>& l : assign)
946 : : {
947 : 13370 : Node a = l.first;
948 : : // if propagation did not touch a
949 [ + + ]: 13370 : if (prop_clauses.find(a) == prop_clauses.end())
950 : : {
951 [ + + ][ + - ]: 9784 : Assert(l.second == truen || l.second == falsen);
[ - + ][ - + ]
[ - - ]
952 [ + + ][ + + ]: 9784 : Node ln = (l.second == truen) == gpol ? a : TermUtil::mkNegate(notk, a);
[ - - ]
953 : 9784 : children.push_back(ln);
954 : 9784 : }
955 : 13370 : }
956 [ + + ]: 2348 : Node new_ret = children.size() == 1 ? children[0] : nm->mkNode(k, children);
957 [ + - ]: 2348 : Trace("ext-rew-bcp") << "BCP: **** OUTPUT: " << new_ret << std::endl;
958 : 2348 : return new_ret;
959 : 2348 : }
960 : :
961 : 68241 : return Node::null();
962 : 71447 : }
963 : :
964 : 68241 : Node ExtendedRewriter::extendedRewriteFactoring(Kind andk,
965 : : Kind ork,
966 : : Node n) const
967 : : {
968 [ + - ]: 68241 : Trace("ext-rew-factoring") << "Factoring: *** INPUT: " << n << std::endl;
969 : 68241 : NodeManager* nm = d_nm;
970 : :
971 : 68241 : Kind nk = n.getKind();
972 [ + + ][ + - ]: 68241 : Assert(nk == andk || nk == ork);
[ - + ][ - + ]
[ - - ]
973 [ + + ]: 68241 : Kind onk = nk == andk ? ork : andk;
974 : : // count the number of times atoms occur
975 : 68241 : std::map<Node, std::vector<Node> > lit_to_cl;
976 : 68241 : std::map<Node, std::vector<Node> > cl_to_lits;
977 [ + + ]: 249855 : for (const Node& nc : n)
978 : : {
979 : 181614 : Kind nck = nc.getKind();
980 [ + + ]: 181614 : if (nck == onk)
981 : : {
982 [ + + ]: 70472 : for (const Node& ncl : nc)
983 : : {
984 : 55612 : if (std::find(lit_to_cl[ncl].begin(), lit_to_cl[ncl].end(), nc)
985 [ + - ]: 111224 : == lit_to_cl[ncl].end())
986 : : {
987 : 55612 : lit_to_cl[ncl].push_back(nc);
988 : 55612 : cl_to_lits[nc].push_back(ncl);
989 : : }
990 : 55612 : }
991 : : }
992 : : else
993 : : {
994 : 166754 : lit_to_cl[nc].push_back(nc);
995 : 166754 : cl_to_lits[nc].push_back(nc);
996 : : }
997 : 181614 : }
998 : : // get the maximum shared literal to factor
999 : 68241 : unsigned max_size = 0;
1000 : 68241 : Node flit;
1001 [ + + ]: 282721 : for (const std::pair<const Node, std::vector<Node> >& ltc : lit_to_cl)
1002 : : {
1003 [ + + ]: 214480 : if (ltc.second.size() > max_size)
1004 : : {
1005 : 68861 : max_size = ltc.second.size();
1006 : 68861 : flit = ltc.first;
1007 : : }
1008 : : }
1009 [ + + ]: 68241 : if (max_size > 1)
1010 : : {
1011 : : // do the factoring
1012 : 1054 : std::vector<Node> children;
1013 : 1054 : std::vector<Node> fchildren;
1014 : 1054 : std::map<Node, std::vector<Node> >::iterator itl = lit_to_cl.find(flit);
1015 : 1054 : std::vector<Node>& cls = itl->second;
1016 [ + + ]: 4590 : for (const Node& nc : n)
1017 : : {
1018 [ + + ]: 3536 : if (std::find(cls.begin(), cls.end(), nc) == cls.end())
1019 : : {
1020 : 792 : children.push_back(nc);
1021 : : }
1022 : : else
1023 : : {
1024 : : // rebuild
1025 : 2744 : std::vector<Node>& lits = cl_to_lits[nc];
1026 : : std::vector<Node>::iterator itlfl =
1027 : 2744 : std::find(lits.begin(), lits.end(), flit);
1028 [ - + ][ - + ]: 2744 : Assert(itlfl != lits.end());
[ - - ]
1029 : 2744 : lits.erase(itlfl);
1030 : : // rebuild
1031 [ + - ]: 2744 : if (!lits.empty())
1032 : : {
1033 [ + + ]: 2744 : Node new_cl = lits.size() == 1 ? lits[0] : nm->mkNode(onk, lits);
1034 : 2744 : fchildren.push_back(new_cl);
1035 : 2744 : }
1036 : : }
1037 : 3536 : }
1038 : : // rebuild the factored children
1039 [ - + ][ - + ]: 1054 : Assert(!fchildren.empty());
[ - - ]
1040 [ - + ]: 1054 : Node fcn = fchildren.size() == 1 ? fchildren[0] : nm->mkNode(nk, fchildren);
1041 : 1054 : children.push_back(nm->mkNode(onk, flit, fcn));
1042 [ + + ]: 1054 : Node ret = children.size() == 1 ? children[0] : nm->mkNode(nk, children);
1043 [ + - ]: 1054 : Trace("ext-rew-factoring") << "Factoring: *** OUTPUT: " << ret << std::endl;
1044 : 1054 : return ret;
1045 : 1054 : }
1046 : : else
1047 : : {
1048 [ + - ]: 67187 : Trace("ext-rew-factoring") << "Factoring: no change" << std::endl;
1049 : : }
1050 : 67187 : return Node::null();
1051 : 68241 : }
1052 : :
1053 : 67187 : Node ExtendedRewriter::extendedRewriteEqRes(Kind andk,
1054 : : CVC5_UNUSED Kind ork,
1055 : : Kind eqk,
1056 : : Kind notk,
1057 : : std::map<Kind, bool>& bcp_kinds,
1058 : : Node n,
1059 : : bool isXor) const
1060 : : {
1061 [ + + ][ + - ]: 67187 : Assert(n.getKind() == andk || n.getKind() == ork);
[ - + ][ - + ]
[ - - ]
1062 [ + - ]: 67187 : Trace("ext-rew-eqres") << "Eq res: **** INPUT: " << n << std::endl;
1063 : :
1064 : 67187 : NodeManager* nm = d_nm;
1065 : 67187 : Kind nk = n.getKind();
1066 : 67187 : bool gpol = (nk == andk);
1067 [ + + ]: 226971 : for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++)
1068 : : {
1069 : 169087 : Node lit = n[i];
1070 [ + + ]: 169087 : if (lit.getKind() == eqk)
1071 : : {
1072 : : // eq is the equality we are basing a substitution on
1073 : 52245 : Node eq;
1074 [ + + ]: 52245 : if (gpol == isXor)
1075 : : {
1076 : : // can only turn disequality into equality if types are the same
1077 [ + + ]: 99456 : if (CVC5_EQUAL(lit[1].getType(), lit.getType()))
1078 : : {
1079 : : // t != s ---> ~t = s
1080 : 385 : if (lit[1].getKind() == notk && lit[0].getKind() != notk)
1081 : : {
1082 : 424 : eq = nm->mkNode(
1083 : 636 : Kind::EQUAL, lit[0], TermUtil::mkNegate(notk, lit[1]));
1084 : : }
1085 : : else
1086 : : {
1087 : 692 : eq = nm->mkNode(
1088 : 519 : Kind::EQUAL, TermUtil::mkNegate(notk, lit[0]), lit[1]);
1089 : : }
1090 : : }
1091 : : }
1092 : : else
1093 : : {
1094 : 27381 : eq = eqk == Kind::EQUAL ? lit : nm->mkNode(Kind::EQUAL, lit[0], lit[1]);
1095 : : }
1096 [ + + ]: 52245 : if (!eq.isNull())
1097 : : {
1098 : : // see if it corresponds to a substitution
1099 : 27766 : Subs subs;
1100 [ + + ]: 27766 : if (inferSubstitution(eq, subs))
1101 : : {
1102 [ - + ][ - + ]: 21577 : Assert(subs.size() == 1);
[ - - ]
1103 : 21577 : std::vector<Node> children;
1104 : 21577 : bool childrenChanged = false;
1105 : : // apply to all other children
1106 [ + + ]: 95215 : for (unsigned j = 0; j < nchild; j++)
1107 : : {
1108 : 73638 : Node ccs = n[j];
1109 [ + + ]: 73638 : if (i != j)
1110 : : {
1111 : : // Substitution is only applicable to compatible kinds. We always
1112 : : // use the partialSubstitute method to avoid substitution into
1113 : : // witness terms.
1114 : 52061 : ccs = partialSubstitute(ccs, subs, bcp_kinds);
1115 [ + + ][ + + ]: 52061 : childrenChanged = childrenChanged || n[j] != ccs;
[ + + ][ - - ]
1116 : : }
1117 : 73638 : children.push_back(ccs);
1118 : 73638 : }
1119 [ + + ]: 21577 : if (childrenChanged)
1120 : : {
1121 : 9303 : return nm->mkNode(nk, children);
1122 : : }
1123 [ + + ]: 21577 : }
1124 [ + + ]: 27766 : }
1125 [ + + ]: 52245 : }
1126 [ + + ]: 169087 : }
1127 : :
1128 : 57884 : return Node::null();
1129 : : }
1130 : :
1131 : : /** sort pairs by their second (unsigned) argument */
1132 : 59503 : static bool sortPairSecond(const std::pair<Node, unsigned>& a,
1133 : : const std::pair<Node, unsigned>& b)
1134 : : {
1135 : 59503 : return (a.second < b.second);
1136 : : }
1137 : :
1138 : : /** A simple subsumption trie used to compute pairwise list subsets */
1139 : : class SimpSubsumeTrie
1140 : : {
1141 : : public:
1142 : : /** the children of this node */
1143 : : std::map<Node, SimpSubsumeTrie> d_children;
1144 : : /** the term at this node */
1145 : : Node d_data;
1146 : : /** add term to the trie
1147 : : *
1148 : : * This adds term c to this trie, whose atom list is alist. This adds terms
1149 : : * s to subsumes such that the atom list of s is a subset of the atom list
1150 : : * of c. For example, say:
1151 : : * c1.alist = { A }
1152 : : * c2.alist = { C }
1153 : : * c3.alist = { B, C }
1154 : : * c4.alist = { A, B, D }
1155 : : * c5.alist = { A, B, C }
1156 : : * If these terms are added in the order c1, c2, c3, c4, c5, then:
1157 : : * addTerm c1 results in subsumes = {}
1158 : : * addTerm c2 results in subsumes = {}
1159 : : * addTerm c3 results in subsumes = { c2 }
1160 : : * addTerm c4 results in subsumes = { c1 }
1161 : : * addTerm c5 results in subsumes = { c1, c2, c3 }
1162 : : * Notice that the intended use case of this trie is to add term t before t'
1163 : : * only when size( t.alist ) <= size( t'.alist ).
1164 : : *
1165 : : * The last two arguments describe the state of the path [t0...tn] we
1166 : : * have followed in the trie during the recursive call.
1167 : : * If doAdd = true,
1168 : : * then n+1 = index and alist[1]...alist[n] = t1...tn. If index=alist.size()
1169 : : * we add c as the current node of this trie.
1170 : : * If doAdd = false,
1171 : : * then t1...tn occur in alist.
1172 : : */
1173 : 117567 : void addTerm(Node c,
1174 : : std::vector<Node>& alist,
1175 : : std::vector<Node>& subsumes,
1176 : : unsigned index = 0,
1177 : : bool doAdd = true)
1178 : : {
1179 [ + + ]: 117567 : if (!d_data.isNull())
1180 : : {
1181 : 64 : subsumes.push_back(d_data);
1182 : : }
1183 [ + + ]: 117567 : if (doAdd)
1184 : : {
1185 [ + + ]: 117433 : if (index == alist.size())
1186 : : {
1187 : 57724 : d_data = c;
1188 : 57724 : return;
1189 : : }
1190 : : }
1191 : : // try all children where we have this atom
1192 [ + + ]: 89313 : for (std::pair<const Node, SimpSubsumeTrie>& cp : d_children)
1193 : : {
1194 [ + + ]: 29470 : if (std::find(alist.begin(), alist.end(), cp.first) != alist.end())
1195 : : {
1196 : 134 : cp.second.addTerm(c, alist, subsumes, 0, false);
1197 : : }
1198 : : }
1199 [ + + ]: 59843 : if (doAdd)
1200 : : {
1201 : 59709 : d_children[alist[index]].addTerm(c, alist, subsumes, index + 1, doAdd);
1202 : : }
1203 : : }
1204 : : };
1205 : :
1206 : 29684 : Node ExtendedRewriter::extendedRewriteEqChain(
1207 : : Kind eqk, Kind andk, Kind ork, Kind notk, Node ret, bool isXor) const
1208 : : {
1209 [ - + ][ - + ]: 29684 : Assert(ret.getKind() == eqk);
[ - - ]
1210 : :
1211 : : // this rewrite is aggressive; it in fact has the precondition that other
1212 : : // aggressive rewrites (including BCP) have been applied.
1213 [ + + ]: 29684 : if (!d_aggr)
1214 : : {
1215 : 359 : return Node::null();
1216 : : }
1217 : :
1218 : 29325 : NodeManager* nm = d_nm;
1219 : :
1220 : 29325 : TypeNode tn = ret[0].getType();
1221 : :
1222 : : // sort/cancelling for Boolean EQUAL/XOR-chains
1223 [ + - ]: 29325 : Trace("ext-rew-eqchain") << "Eq-Chain : " << ret << std::endl;
1224 : :
1225 : : // get the children on either side
1226 : 29325 : bool gpol = true;
1227 : 29325 : std::vector<Node> children;
1228 [ + + ]: 87975 : for (unsigned r = 0, size = ret.getNumChildren(); r < size; r++)
1229 : : {
1230 : 58650 : Node curr = ret[r];
1231 : : // assume, if necessary, right associative
1232 : 59736 : while (curr.getKind() == eqk && curr[0].getType() == tn)
1233 : : {
1234 : 1086 : children.push_back(curr[0]);
1235 : 1086 : curr = curr[1];
1236 : : }
1237 : 58650 : children.push_back(curr);
1238 : 58650 : }
1239 : :
1240 : 29325 : std::map<Node, bool> cstatus;
1241 : : // add children to status
1242 [ + + ]: 89061 : for (const Node& c : children)
1243 : : {
1244 : 59736 : Node a = c;
1245 [ + + ]: 59736 : if (a.getKind() == notk)
1246 : : {
1247 : 2103 : gpol = !gpol;
1248 : 2103 : a = a[0];
1249 : : }
1250 [ + - ]: 59736 : Trace("ext-rew-eqchain") << "...child : " << a << std::endl;
1251 : 59736 : std::map<Node, bool>::iterator itc = cstatus.find(a);
1252 [ + + ]: 59736 : if (itc == cstatus.end())
1253 : : {
1254 : 59414 : cstatus[a] = true;
1255 : : }
1256 : : else
1257 : : {
1258 : : // cancels
1259 : 322 : cstatus.erase(a);
1260 [ - + ]: 322 : if (isXor)
1261 : : {
1262 : 0 : gpol = !gpol;
1263 : : }
1264 : : }
1265 : 59736 : }
1266 [ + - ]: 29325 : Trace("ext-rew-eqchain") << "Global polarity : " << gpol << std::endl;
1267 : :
1268 [ - + ]: 29325 : if (cstatus.empty())
1269 : : {
1270 : 0 : return TermUtil::mkTypeConst(ret.getType(), gpol);
1271 : : }
1272 : :
1273 : 29325 : children.clear();
1274 : :
1275 : : // compute the atoms of each child
1276 [ + - ]: 29325 : Trace("ext-rew-eqchain") << "eqchain-simplify: begin\n";
1277 [ + - ]: 29325 : Trace("ext-rew-eqchain") << " eqchain-simplify: get atoms...\n";
1278 : 29325 : std::map<Node, std::map<Node, bool> > atoms;
1279 : 29325 : std::map<Node, std::vector<Node> > alist;
1280 : 29325 : std::vector<std::pair<Node, unsigned> > atom_count;
1281 [ + + ]: 88417 : for (std::pair<const Node, bool>& cp : cstatus)
1282 : : {
1283 [ - + ]: 59092 : if (!cp.second)
1284 : : {
1285 : : // already eliminated
1286 : 0 : continue;
1287 : : }
1288 : 59092 : Node c = cp.first;
1289 : 59092 : Kind ck = c.getKind();
1290 [ + - ]: 59092 : Trace("ext-rew-eqchain") << " process c = " << c << std::endl;
1291 [ + + ][ + + ]: 59092 : if (ck == andk || ck == ork)
1292 : : {
1293 [ + + ]: 6214 : for (unsigned j = 0, nchild = c.getNumChildren(); j < nchild; j++)
1294 : : {
1295 : 4605 : Node cl = c[j];
1296 : 4605 : bool pol = cl.getKind() != notk;
1297 [ + + ]: 4605 : Node ca = pol ? cl : cl[0];
1298 [ + + ]: 4605 : bool newVal = (ck == andk ? !pol : pol);
1299 [ + - ]: 9210 : Trace("ext-rew-eqchain")
1300 : 4605 : << " atoms(" << c << ", " << ca << ") = " << newVal << std::endl;
1301 [ - + ][ - + ]: 4605 : Assert(atoms[c].find(ca) == atoms[c].end());
[ - - ]
1302 : : // polarity is flipped when we are AND
1303 : 4605 : atoms[c][ca] = newVal;
1304 : 4605 : alist[c].push_back(ca);
1305 : :
1306 : : // if this already exists as a child of the equality chain, eliminate.
1307 : : // this catches cases like ( x & y ) = ( ( x & y ) | z ), where we
1308 : : // consider ( x & y ) a unit, whereas below it is expanded to
1309 : : // ~( ~x | ~y ).
1310 : 4605 : std::map<Node, bool>::iterator itc = cstatus.find(ca);
1311 [ + + ][ + - ]: 4605 : if (itc != cstatus.end() && itc->second)
[ + + ]
1312 : : {
1313 : : // cancel it
1314 : 684 : cstatus[ca] = false;
1315 : 684 : cstatus[c] = false;
1316 : : // make new child
1317 : : // x = ( y | ~x ) ---> y & x
1318 : : // x = ( y | x ) ---> ~y | x
1319 : : // x = ( y & x ) ---> y | ~x
1320 : : // x = ( y & ~x ) ---> ~y & ~x
1321 : 684 : std::vector<Node> new_children;
1322 [ + + ]: 2092 : for (unsigned k = 0, nchildc = c.getNumChildren(); k < nchildc; k++)
1323 : : {
1324 [ + + ]: 1408 : if (j != k)
1325 : : {
1326 : 724 : new_children.push_back(c[k]);
1327 : : }
1328 : : }
1329 [ + + ]: 4104 : Node nc[2];
1330 : 684 : nc[0] = c[j];
1331 [ + + ]: 1368 : nc[1] = new_children.size() == 1 ? new_children[0]
1332 : 684 : : nm->mkNode(ck, new_children);
1333 : : // negate the proper child
1334 : 684 : unsigned nindex = (ck == andk) == pol ? 0 : 1;
1335 : 684 : nc[nindex] = TermUtil::mkNegate(notk, nc[nindex]);
1336 [ + + ]: 684 : Kind nk = pol ? ork : andk;
1337 : : // store as new child
1338 : 684 : children.push_back(nm->mkNode(nk, nc[0], nc[1]));
1339 [ - + ]: 684 : if (isXor)
1340 : : {
1341 : 0 : gpol = !gpol;
1342 : : }
1343 : 684 : break;
1344 [ + + ][ - - ]: 2736 : }
1345 [ + + ][ + + ]: 5289 : }
1346 : 2293 : }
1347 : : else
1348 : : {
1349 : 56799 : bool pol = ck != notk;
1350 [ + - ]: 56799 : Node ca = pol ? c : c[0];
1351 : 56799 : atoms[c][ca] = pol;
1352 [ + - ]: 113598 : Trace("ext-rew-eqchain")
1353 : 56799 : << " atoms(" << c << ", " << ca << ") = " << pol << std::endl;
1354 : 56799 : alist[c].push_back(ca);
1355 : 56799 : }
1356 : 59092 : atom_count.push_back(std::pair<Node, unsigned>(c, alist[c].size()));
1357 : 59092 : }
1358 : : // sort the atoms in each atom list
1359 : 29325 : for (std::map<Node, std::vector<Node> >::iterator it = alist.begin();
1360 [ + + ]: 88417 : it != alist.end();
1361 : 59092 : ++it)
1362 : : {
1363 : 59092 : std::sort(it->second.begin(), it->second.end());
1364 : : }
1365 : : // check subsumptions
1366 : : // sort by #atoms
1367 : 29325 : std::sort(atom_count.begin(), atom_count.end(), sortPairSecond);
1368 [ - + ]: 29325 : if (TraceIsOn("ext-rew-eqchain"))
1369 : : {
1370 [ - - ]: 0 : for (const std::pair<Node, unsigned>& ac : atom_count)
1371 : : {
1372 [ - - ]: 0 : Trace("ext-rew-eqchain") << " eqchain-simplify: " << ac.first << " has "
1373 : 0 : << ac.second << " atoms." << std::endl;
1374 : : }
1375 [ - - ]: 0 : Trace("ext-rew-eqchain") << " eqchain-simplify: compute subsumptions...\n";
1376 : : }
1377 : 29325 : SimpSubsumeTrie sst;
1378 [ + + ]: 88417 : for (std::pair<const Node, bool>& cp : cstatus)
1379 : : {
1380 [ + + ]: 59092 : if (!cp.second)
1381 : : {
1382 : : // already eliminated
1383 : 1368 : continue;
1384 : : }
1385 : 57724 : Node c = cp.first;
1386 : 57724 : std::map<Node, std::map<Node, bool> >::iterator itc = atoms.find(c);
1387 [ - + ][ - + ]: 57724 : Assert(itc != atoms.end());
[ - - ]
1388 [ + - ]: 115448 : Trace("ext-rew-eqchain")
1389 : 57724 : << " - add term " << c << " with atom list " << alist[c] << "...\n";
1390 : 57724 : std::vector<Node> subsumes;
1391 : 57724 : sst.addTerm(c, alist[c], subsumes);
1392 [ + + ]: 57724 : for (const Node& cc : subsumes)
1393 : : {
1394 [ - + ]: 20 : if (!cstatus[cc])
1395 : : {
1396 : : // subsumes a child that was already eliminated
1397 : 0 : continue;
1398 : : }
1399 [ + - ]: 40 : Trace("ext-rew-eqchain")
1400 : 20 : << " eqchain-simplify: " << c << " subsumes " << cc << std::endl;
1401 : : // for each of the atoms in cc
1402 : 20 : std::map<Node, std::map<Node, bool> >::iterator itcc = atoms.find(cc);
1403 [ - + ][ - + ]: 20 : Assert(itcc != atoms.end());
[ - - ]
1404 : 20 : std::vector<Node> common_children;
1405 : 20 : std::vector<Node> diff_children;
1406 [ + + ]: 64 : for (const std::pair<const Node, bool>& ap : itcc->second)
1407 : : {
1408 : : // compare the polarity
1409 : 44 : Node a = ap.first;
1410 : 44 : bool polcc = ap.second;
1411 [ - + ][ - + ]: 44 : Assert(itc->second.find(a) != itc->second.end());
[ - - ]
1412 : 44 : bool polc = itc->second[a];
1413 [ + - ]: 88 : Trace("ext-rew-eqchain")
1414 : 0 : << " eqchain-simplify: atom " << a
1415 : 44 : << " has polarities : " << polc << " " << polcc << "\n";
1416 [ + + ][ + + ]: 44 : Node lit = polc ? a : TermUtil::mkNegate(notk, a);
[ - - ]
1417 [ + + ]: 44 : if (polc != polcc)
1418 : : {
1419 : 24 : diff_children.push_back(lit);
1420 : : }
1421 : : else
1422 : : {
1423 : 20 : common_children.push_back(lit);
1424 : : }
1425 : 44 : }
1426 : 20 : std::vector<Node> rem_children;
1427 [ + + ]: 64 : for (const std::pair<const Node, bool>& ap : itc->second)
1428 : : {
1429 : 44 : Node a = ap.first;
1430 [ - + ]: 44 : if (atoms[cc].find(a) == atoms[cc].end())
1431 : : {
1432 : 0 : bool polc = ap.second;
1433 : 0 : rem_children.push_back(polc ? a : TermUtil::mkNegate(notk, a));
1434 : : }
1435 : 44 : }
1436 [ + - ]: 40 : Trace("ext-rew-eqchain")
1437 : 0 : << " #common/diff/rem: " << common_children.size() << "/"
1438 : 20 : << diff_children.size() << "/" << rem_children.size() << "\n";
1439 : 20 : bool do_rewrite = false;
1440 [ + - ]: 32 : if (common_children.empty() && itc->second.size() == itcc->second.size()
1441 [ + + ][ + - ]: 32 : && itcc->second.size() == 2)
[ + + ]
1442 : : {
1443 : : // x | y = ~x | ~y ---> ~( x = y )
1444 : 12 : do_rewrite = true;
1445 : 12 : children.push_back(diff_children[0]);
1446 : 12 : children.push_back(diff_children[1]);
1447 : 12 : gpol = !gpol;
1448 [ + - ]: 12 : Trace("ext-rew-eqchain") << " apply 2-child all-diff\n";
1449 : : }
1450 [ - + ][ - - ]: 8 : else if (common_children.empty() && diff_children.size() == 1)
[ - + ]
1451 : : {
1452 : 0 : do_rewrite = true;
1453 : : // x = ( ~x | y ) ---> ~( ~x | ~y )
1454 : 0 : Node remn = rem_children.size() == 1 ? rem_children[0]
1455 [ - - ]: 0 : : nm->mkNode(ork, rem_children);
1456 : 0 : remn = TermUtil::mkNegate(notk, remn);
1457 : 0 : children.push_back(nm->mkNode(ork, diff_children[0], remn));
1458 [ - - ]: 0 : if (!isXor)
1459 : : {
1460 : 0 : gpol = !gpol;
1461 : : }
1462 [ - - ]: 0 : Trace("ext-rew-eqchain") << " apply unit resolution\n";
1463 : 0 : }
1464 : 8 : else if (diff_children.size() == 1
1465 [ - + ][ - - ]: 8 : && itc->second.size() == itcc->second.size())
[ - + ]
1466 : : {
1467 : : // ( x | y | z ) = ( x | ~y | z ) ---> ( x | z )
1468 : 0 : do_rewrite = true;
1469 : 0 : Assert(!common_children.empty());
1470 : 0 : Node comn = common_children.size() == 1
1471 : 0 : ? common_children[0]
1472 [ - - ]: 0 : : nm->mkNode(ork, common_children);
1473 : 0 : children.push_back(comn);
1474 [ - - ]: 0 : if (isXor)
1475 : : {
1476 : 0 : gpol = !gpol;
1477 : : }
1478 [ - - ]: 0 : Trace("ext-rew-eqchain") << " apply resolution\n";
1479 : 0 : }
1480 [ + - ]: 8 : else if (diff_children.empty())
1481 : : {
1482 : 8 : do_rewrite = true;
1483 [ + - ]: 8 : if (rem_children.empty())
1484 : : {
1485 : : // x | y = x | y ---> true
1486 : : // this can happen if we have ( ~x & ~y ) = ( x | y )
1487 : 8 : children.push_back(TermUtil::mkTypeMaxValue(tn));
1488 [ - + ]: 8 : if (isXor)
1489 : : {
1490 : 0 : gpol = !gpol;
1491 : : }
1492 [ + - ]: 8 : Trace("ext-rew-eqchain") << " apply cancel\n";
1493 : : }
1494 : : else
1495 : : {
1496 : : // x | y = ( x | y | z ) ---> ( x | y | ~z )
1497 : 0 : Node remn = rem_children.size() == 1 ? rem_children[0]
1498 [ - - ]: 0 : : nm->mkNode(ork, rem_children);
1499 : 0 : remn = TermUtil::mkNegate(notk, remn);
1500 : 0 : Node comn = common_children.size() == 1
1501 : 0 : ? common_children[0]
1502 [ - - ]: 0 : : nm->mkNode(ork, common_children);
1503 : 0 : children.push_back(nm->mkNode(ork, comn, remn));
1504 [ - - ]: 0 : if (isXor)
1505 : : {
1506 : 0 : gpol = !gpol;
1507 : : }
1508 [ - - ]: 0 : Trace("ext-rew-eqchain") << " apply subsume\n";
1509 : 0 : }
1510 : : }
1511 [ + - ]: 20 : if (do_rewrite)
1512 : : {
1513 : : // eliminate the children, reverse polarity as needed
1514 [ + + ]: 60 : for (unsigned r = 0; r < 2; r++)
1515 : : {
1516 [ + + ]: 40 : Node c_rem = r == 0 ? c : cc;
1517 : 40 : cstatus[c_rem] = false;
1518 [ + + ]: 40 : if (c_rem.getKind() == andk)
1519 : : {
1520 : 20 : gpol = !gpol;
1521 : : }
1522 : 40 : }
1523 : 20 : break;
1524 : : }
1525 [ - + ][ - + ]: 60 : }
[ - + ]
1526 : 57724 : }
1527 [ + - ]: 29325 : Trace("ext-rew-eqchain") << "eqchain-simplify: finish" << std::endl;
1528 : :
1529 : : // sorted right associative chain
1530 : 29325 : bool has_nvar = false;
1531 : 29325 : unsigned nvar_index = 0;
1532 [ + + ]: 88417 : for (std::pair<const Node, bool>& cp : cstatus)
1533 : : {
1534 [ + + ]: 59092 : if (cp.second)
1535 : : {
1536 [ + + ]: 57684 : if (!cp.first.isVar())
1537 : : {
1538 : 38349 : has_nvar = true;
1539 : 38349 : nvar_index = children.size();
1540 : : }
1541 : 57684 : children.push_back(cp.first);
1542 : : }
1543 : : }
1544 : 29325 : std::sort(children.begin(), children.end());
1545 : :
1546 : 29325 : Node new_ret;
1547 [ + + ]: 29325 : if (!gpol)
1548 : : {
1549 : : // negate the constant child if it exists
1550 [ + + ]: 1851 : unsigned nindex = has_nvar ? nvar_index : 0;
1551 : 1851 : children[nindex] = TermUtil::mkNegate(notk, children[nindex]);
1552 : : }
1553 : 29325 : new_ret = children.back();
1554 : 29325 : unsigned index = children.size() - 1;
1555 [ + + ]: 58400 : while (index > 0)
1556 : : {
1557 : 29075 : index--;
1558 : 29075 : new_ret = nm->mkNode(eqk, children[index], new_ret);
1559 : : }
1560 : 29325 : new_ret = d_rew.rewrite(new_ret);
1561 [ + + ]: 29325 : if (new_ret != ret)
1562 : : {
1563 : 2096 : return new_ret;
1564 : : }
1565 : 27229 : return Node::null();
1566 : 29325 : }
1567 : :
1568 : 520775 : Node ExtendedRewriter::partialSubstitute(
1569 : : Node n,
1570 : : const std::map<Node, Node>& assign,
1571 : : const std::map<Kind, bool>& rkinds) const
1572 : : {
1573 : 520775 : std::unordered_map<TNode, Node> visited;
1574 : 520775 : std::unordered_map<TNode, Node>::iterator it;
1575 : 520775 : std::map<Node, Node>::const_iterator ita;
1576 : 520775 : std::vector<TNode> visit;
1577 : 520775 : TNode cur;
1578 : 520775 : visit.push_back(n);
1579 : : do
1580 : : {
1581 : 6835227 : cur = visit.back();
1582 : 6835227 : visit.pop_back();
1583 : 6835227 : it = visited.find(cur);
1584 : :
1585 [ + + ]: 6835227 : if (it == visited.end())
1586 : : {
1587 : 2856712 : ita = assign.find(cur);
1588 [ + + ]: 2856712 : if (ita != assign.end())
1589 : : {
1590 : 29748 : visited[cur] = ita->second;
1591 : : }
1592 : : else
1593 : : {
1594 : : // If rkinds is non-empty, then can only recurse on its kinds.
1595 : : // We also always disallow substitution into witness. Notice that
1596 : : // we disallow witness here, due to unsoundness when applying contextual
1597 : : // substitutions over witness terms (see #4620).
1598 : 2826964 : Kind k = cur.getKind();
1599 : 5653928 : if (k != Kind::WITNESS
1600 [ + - ][ - + ]: 2826964 : && (rkinds.empty() || rkinds.find(k) != rkinds.end()))
[ - - ][ + - ]
1601 : : {
1602 : 2826964 : visited[cur] = Node::null();
1603 : 2826964 : visit.push_back(cur);
1604 [ + + ]: 6314452 : for (const Node& cn : cur)
1605 : : {
1606 : 3487488 : visit.push_back(cn);
1607 : 3487488 : }
1608 : : }
1609 : : else
1610 : : {
1611 : 0 : visited[cur] = cur;
1612 : : }
1613 : : }
1614 : : }
1615 [ + + ]: 3978515 : else if (it->second.isNull())
1616 : : {
1617 : 2826964 : Node ret = cur;
1618 : 2826964 : bool childChanged = false;
1619 : 2826964 : std::vector<Node> children;
1620 [ + + ]: 2826964 : if (cur.getMetaKind() == metakind::PARAMETERIZED)
1621 : : {
1622 : 20256 : children.push_back(cur.getOperator());
1623 : : }
1624 [ + + ]: 6314452 : for (const Node& cn : cur)
1625 : : {
1626 : 3487488 : it = visited.find(cn);
1627 [ - + ][ - + ]: 3487488 : Assert(it != visited.end());
[ - - ]
1628 [ - + ][ - + ]: 3487488 : Assert(!it->second.isNull());
[ - - ]
1629 [ + + ][ + + ]: 3487488 : childChanged = childChanged || cn != it->second;
1630 : 3487488 : children.push_back(it->second);
1631 : 3487488 : }
1632 [ + + ]: 2826964 : if (childChanged)
1633 : : {
1634 : 112074 : ret = d_nm->mkNode(cur.getKind(), children);
1635 : : }
1636 : 2826964 : visited[cur] = ret;
1637 : 2826964 : }
1638 [ + + ]: 6835227 : } while (!visit.empty());
1639 [ - + ][ - + ]: 520775 : Assert(visited.find(n) != visited.end());
[ - - ]
1640 [ - + ][ - + ]: 520775 : Assert(!visited.find(n)->second.isNull());
[ - - ]
1641 : 1041550 : return visited[n];
1642 : 520775 : }
1643 : :
1644 : 83832 : Node ExtendedRewriter::partialSubstitute(
1645 : : Node n, const Subs& subs, const std::map<Kind, bool>& rkinds) const
1646 : : {
1647 : 83832 : std::map<Node, Node> assign;
1648 [ + + ]: 185336 : for (size_t i = 0, nvars = subs.size(); i < nvars; i++)
1649 : : {
1650 : 101504 : assign[subs.d_vars[i]] = subs.d_subs[i];
1651 : : }
1652 : 167664 : return partialSubstitute(n, assign, rkinds);
1653 : 83832 : }
1654 : :
1655 : 46175 : Node ExtendedRewriter::solveEquality(CVC5_UNUSED Node n) const
1656 : : {
1657 : : // TODO (#1706) : implement
1658 [ - + ][ - + ]: 46175 : Assert(n.getKind() == Kind::EQUAL);
[ - - ]
1659 : :
1660 : 46175 : return Node::null();
1661 : : }
1662 : :
1663 : 82799 : bool ExtendedRewriter::inferSubstitution(Node n, Subs& subs, bool usePred) const
1664 : : {
1665 [ + + ]: 82799 : if (n.getKind() == Kind::AND)
1666 : : {
1667 : 5590 : bool ret = false;
1668 [ + + ]: 28852 : for (const Node& nc : n)
1669 : : {
1670 : 23262 : bool cret = inferSubstitution(nc, subs, usePred);
1671 [ + + ][ + - ]: 23262 : ret = ret || cret;
1672 : 23262 : }
1673 : 5590 : return ret;
1674 : : }
1675 [ + + ]: 77209 : if (n.getKind() == Kind::EQUAL)
1676 : : {
1677 : : // see if it can be put into form x = y
1678 : 46175 : Node slv_eq = solveEquality(n);
1679 [ - + ]: 46175 : if (!slv_eq.isNull())
1680 : : {
1681 : 0 : n = slv_eq;
1682 : : }
1683 [ + + ]: 277050 : Node v[2];
1684 [ + + ]: 97543 : for (unsigned i = 0; i < 2; i++)
1685 : : {
1686 [ + + ]: 84927 : if (n[i].isConst())
1687 : : {
1688 : 33559 : subs.add(n[1 - i], n[i]);
1689 : 33559 : return true;
1690 : : }
1691 [ + + ]: 51368 : if (n[i].isVar())
1692 : : {
1693 : 34864 : v[i] = n[i];
1694 : : }
1695 : 16504 : else if (TermUtil::isNegate(n[i].getKind()) && n[i][0].isVar())
1696 : : {
1697 : 304 : v[i] = n[i][0];
1698 : : }
1699 : : }
1700 [ + + ]: 27288 : for (unsigned i = 0; i < 2; i++)
1701 : : {
1702 : 20099 : TNode r1 = v[i];
1703 : 20099 : Node r2 = v[1 - i];
1704 [ + + ][ + + ]: 20099 : if (r1.isVar() && ((r2.isVar() && r1 < r2) || r2.isConst()))
[ + + ][ - + ]
[ + + ]
1705 : : {
1706 : 5427 : r2 = n[1 - i];
1707 [ + + ]: 5427 : if (v[i] != n[i])
1708 : : {
1709 [ - + ][ - + ]: 216 : Assert(TermUtil::isNegate(n[i].getKind()));
[ - - ]
1710 : 216 : r2 = TermUtil::mkNegate(n[i].getKind(), r2);
1711 : : }
1712 [ + - ]: 5427 : if (!subs.contains(r1))
1713 : : {
1714 : 5427 : subs.add(r1, r2);
1715 : 5427 : return true;
1716 : : }
1717 : : }
1718 [ + + ][ + + ]: 25526 : }
1719 [ + + ][ + + ]: 184700 : }
[ - - ]
1720 [ + + ]: 38223 : if (usePred)
1721 : : {
1722 : 32034 : bool negated = n.getKind() == Kind::NOT;
1723 [ + + ]: 32034 : Node var = negated ? n[0] : n;
1724 : 32034 : Node s = d_nm->mkConst(!negated);
1725 : 32034 : subs.add(var, s);
1726 : 32034 : return true;
1727 : 32034 : }
1728 : 6189 : return false;
1729 : : }
1730 : :
1731 : 18558 : Node ExtendedRewriter::extendedRewriteStrings(const Node& node) const
1732 : : {
1733 [ + - ]: 37116 : Trace("q-ext-rewrite-debug")
1734 : 18558 : << "Extended rewrite strings : " << node << std::endl;
1735 : :
1736 : : // allow recursive approximations
1737 : 18558 : strings::ArithEntail ae(d_nm, &d_rew, true);
1738 : 18558 : strings::StringsEntail se(&d_rew, ae);
1739 : 18558 : strings::SequencesRewriter sr(d_nm, ae, se, nullptr);
1740 : :
1741 : 18558 : Kind k = node.getKind();
1742 [ + + ]: 18558 : if (k == Kind::EQUAL)
1743 : : {
1744 : : // we invoke the extended equality rewriter, which does standard
1745 : : // rewrites, which notice are only invoked at preprocessing
1746 : : // and not during Rewriter::rewrite.
1747 : 3685 : Node ret = sr.rewriteEqualityExt(node);
1748 [ + + ]: 3685 : if (ret != node)
1749 : : {
1750 : 328 : debugExtendedRewrite(node, ret, "STR_EXT_EQ_REWRITE");
1751 : 328 : return ret;
1752 : : }
1753 : :
1754 : : // ------- length entailment
1755 : 6714 : Node len0 = d_nm->mkNode(Kind::STRING_LENGTH, node[0]);
1756 : 6714 : Node len1 = d_nm->mkNode(Kind::STRING_LENGTH, node[1]);
1757 : 3357 : Node len_eq = len0.eqNode(len1);
1758 : 3357 : len_eq = d_rew.rewrite(len_eq);
1759 [ - + ]: 3357 : if (len_eq == d_false)
1760 : : {
1761 : 0 : debugExtendedRewrite(node, d_false, "String EQUAL len entailment");
1762 : 0 : return d_false;
1763 : : }
1764 : :
1765 : 3357 : TypeNode stype = node[0].getType();
1766 [ + + ]: 20142 : std::vector<Node> c[2];
1767 [ + + ]: 10071 : for (unsigned i = 0; i < 2; i++)
1768 : : {
1769 : 6714 : strings::utils::getConcat(node[i], c[i]);
1770 : : }
1771 : :
1772 : : // ------- homogeneous constants
1773 [ + + ]: 10070 : for (unsigned i = 0; i < 2; i++)
1774 : : {
1775 : 6714 : Node cn = se.checkHomogeneousString(node[i]);
1776 [ + + ][ + + ]: 6714 : if (!cn.isNull() && !strings::Word::isEmpty(cn))
[ + + ][ + + ]
[ - - ]
1777 : : {
1778 [ - + ][ - + ]: 1519 : Assert(cn.isConst());
[ - - ]
1779 [ - + ][ - + ]: 1519 : Assert(strings::Word::getLength(cn) == 1);
[ - - ]
1780 : :
1781 : : // The operands of the concat on each side of the equality without
1782 : : // constant strings
1783 [ + + ]: 9114 : std::vector<Node> trimmed[2];
1784 : : // Counts the number of `cn`s on each side
1785 : 1519 : size_t numCns[2] = {0, 0};
1786 [ + + ]: 4557 : for (size_t j = 0; j < 2; j++)
1787 : : {
1788 : : // Sort the operands of the concats on both sides of the equality
1789 : : // (since both sides may only contain one char, the order does not
1790 : : // matter)
1791 : 3038 : std::sort(c[j].begin(), c[j].end());
1792 [ + + ]: 6091 : for (const Node& cc : c[j])
1793 : : {
1794 [ + + ]: 3053 : if (cc.isConst())
1795 : : {
1796 : : // Count the number of `cn`s in the string constant and make
1797 : : // sure that all chars are `cn`s
1798 : 1488 : std::vector<Node> veccc = strings::Word::getChars(cc);
1799 [ + + ]: 3397 : for (const Node& cv : veccc)
1800 : : {
1801 [ - + ]: 1909 : if (cv != cn)
1802 : : {
1803 : : // This conflict case should mostly should be taken care of by
1804 : : // multiset reasoning in the strings rewriter, but we
1805 : : // recognize this conflict just in case.
1806 : 0 : debugExtendedRewrite(node, d_false, "STR_EQ_CONST_NHOMOG");
1807 : 0 : return d_false;
1808 : : }
1809 : 1909 : numCns[j]++;
1810 : : }
1811 [ + - ]: 1488 : }
1812 : : else
1813 : : {
1814 : 1565 : trimmed[j].push_back(cc);
1815 : : }
1816 : : }
1817 : : }
1818 : :
1819 : : // We have to remove the same number of `cn`s from both sides, so the
1820 : : // side with less `cn`s determines how many we can remove
1821 : 1519 : size_t trimmedConst = std::min(numCns[0], numCns[1]);
1822 [ + + ]: 4557 : for (size_t j = 0; j < 2; j++)
1823 : : {
1824 : 3038 : size_t diff = numCns[j] - trimmedConst;
1825 [ + + ]: 3038 : if (diff != 0)
1826 : : {
1827 : : // Add a constant string to the side with more `cn`s to restore
1828 : : // the difference in number of `cn`s
1829 : 1483 : std::vector<Node> vec(diff, cn);
1830 : 1483 : trimmed[j].push_back(strings::Word::mkWordFlatten(vec));
1831 : 1483 : }
1832 : : }
1833 : :
1834 : 1519 : Node lhs = strings::utils::mkConcat(trimmed[i], stype);
1835 : 1519 : Node ss = strings::utils::mkConcat(trimmed[1 - i], stype);
1836 : 1519 : if (lhs != node[i] || ss != node[1 - i])
1837 : : {
1838 : : // e.g.
1839 : : // "AA" = y ++ x ---> "AA" = x ++ y if x < y
1840 : : // "AAA" = y ++ "A" ++ z ---> "AA" = y ++ z
1841 : : //
1842 : : // We generally don't apply the extended equality rewriter if the
1843 : : // original node was an equality but we may be able to do additional
1844 : : // rewriting here.
1845 : 1 : Node new_ret = lhs.eqNode(ss);
1846 : 1 : debugExtendedRewrite(node, new_ret, "STR_EQ_CONST_NHOMOG");
1847 : 1 : return new_ret;
1848 : 1 : }
1849 [ + + ][ + + ]: 6077 : }
[ + + ][ - - ]
1850 [ + + ]: 6714 : }
1851 [ + + ][ + + ]: 13760 : }
[ + + ][ + + ]
[ + + ][ + + ]
[ - - ]
1852 [ + + ]: 14873 : else if (k == Kind::STRING_CONCAT)
1853 : : {
1854 : : // Sort adjacent operands in str.++ that all result in the same string or
1855 : : // the empty string.
1856 : : //
1857 : : // E.g.: (str.++ ... (str.replace "A" x "") "A" (str.substr "A" 0 z) ...)
1858 : : // --> (str.++ ... [sort those 3 arguments] ... )
1859 : 605 : std::vector<Node> vec(node.begin(), node.end());
1860 : 605 : size_t lastIdx = 0;
1861 : 605 : Node lastX;
1862 [ + + ]: 1941 : for (size_t i = 0, nsize = vec.size(); i < nsize; i++)
1863 : : {
1864 : 1336 : Node s = se.getStringOrEmpty(vec[i]);
1865 : 1336 : bool nextX = false;
1866 [ + + ]: 1336 : if (s != lastX)
1867 : : {
1868 : 1297 : nextX = true;
1869 : : }
1870 [ + + ]: 1336 : if (nextX)
1871 : : {
1872 : 1297 : std::sort(vec.begin() + lastIdx, vec.begin() + i);
1873 : 1297 : lastX = s;
1874 : 1297 : lastIdx = i;
1875 : : }
1876 : 1336 : }
1877 : 605 : std::sort(vec.begin() + lastIdx, vec.end());
1878 : 605 : TypeNode tn = node.getType();
1879 : 605 : Node retNode = strings::utils::mkConcat(vec, tn);
1880 [ + + ]: 605 : if (retNode != node)
1881 : : {
1882 : 6 : debugExtendedRewrite(node, retNode, "CONCAT_NORM_SORT");
1883 : 6 : return retNode;
1884 : : }
1885 [ + + ][ + + ]: 623 : }
[ + + ][ + + ]
1886 [ + + ]: 14268 : else if (k == Kind::STRING_SUBSTR)
1887 : : {
1888 : 2342 : NodeManager* nm = d_nm;
1889 : 4684 : Node tot_len = d_rew.rewrite(nm->mkNode(Kind::STRING_LENGTH, node[0]));
1890 : : // (str.substr s x y) --> "" if x < len(s) |= 0 >= y
1891 : 4684 : Node n1_lt_tot_len = d_rew.rewrite(nm->mkNode(Kind::LT, node[1], tot_len));
1892 [ + + ]: 2342 : if (ae.checkWithAssumption(n1_lt_tot_len, d_intZero, node[2], false))
1893 : : {
1894 : 2 : Node ret = strings::Word::mkEmptyWord(node.getType());
1895 : 2 : debugExtendedRewrite(node, ret, "SS_START_ENTAILS_ZERO_LEN");
1896 : 2 : return ret;
1897 : 2 : }
1898 : :
1899 : : // (str.substr s x y) --> "" if 0 < y |= x >= str.len(s)
1900 : 4680 : Node non_zero_len = d_rew.rewrite(nm->mkNode(Kind::LT, d_intZero, node[2]));
1901 [ + + ]: 2340 : if (ae.checkWithAssumption(non_zero_len, node[1], tot_len, false))
1902 : : {
1903 : 3 : Node ret = strings::Word::mkEmptyWord(node.getType());
1904 : 3 : debugExtendedRewrite(node, ret, "SS_NON_ZERO_LEN_ENTAILS_OOB");
1905 : 3 : return ret;
1906 : 3 : }
1907 : : // (str.substr s x y) --> "" if x >= 0 |= 0 >= str.len(s)
1908 : : Node geq_zero_start =
1909 : 4674 : d_rew.rewrite(nm->mkNode(Kind::GEQ, node[1], d_intZero));
1910 [ + + ]: 2337 : if (ae.checkWithAssumption(geq_zero_start, d_intZero, tot_len, false))
1911 : : {
1912 : 1 : Node ret = strings::Word::mkEmptyWord(node.getType());
1913 : 1 : debugExtendedRewrite(node, ret, "SS_GEQ_ZERO_START_ENTAILS_EMP_S");
1914 : 1 : return ret;
1915 : 1 : }
1916 [ + + ][ + + ]: 2353 : }
[ + + ][ + + ]
1917 [ + + ]: 11926 : else if (k == Kind::STRING_REPLACE)
1918 : : {
1919 [ + + ]: 153 : if (node[0] == node[2])
1920 : : {
1921 : : // (str.replace x y x) ---> (str.replace x (str.++ y1 ... yn) x)
1922 : : // if 1 >= (str.len x) and (= y "") ---> (= y1 "") ... (= yn "")
1923 [ + + ]: 14 : if (se.checkLengthOne(node[0]))
1924 : : {
1925 : 3 : TypeNode stype = node.getType();
1926 : 3 : Node empty = strings::Word::mkEmptyWord(stype);
1927 : 6 : Node rn1 = d_rew.rewrite(d_rew.rewriteEqualityExt(
1928 : 12 : d_nm->mkNode(Kind::EQUAL, node[1], empty)));
1929 [ + - ]: 3 : if (rn1 != node[1])
1930 : : {
1931 : 3 : std::vector<Node> emptyNodes;
1932 : : bool allEmptyEqs;
1933 : 3 : std::tie(allEmptyEqs, emptyNodes) =
1934 : 6 : strings::utils::collectEmptyEqs(rn1);
1935 : :
1936 [ + + ]: 3 : if (allEmptyEqs)
1937 : : {
1938 : 2 : Node nn1 = strings::utils::mkConcat(emptyNodes, stype);
1939 [ + + ]: 2 : if (node[1] != nn1)
1940 : : {
1941 : : Node ret =
1942 : 2 : d_nm->mkNode(Kind::STRING_REPLACE, node[0], nn1, node[2]);
1943 : 1 : debugExtendedRewrite(node, ret, "RPL_X_Y_X_SIMP");
1944 : 1 : return ret;
1945 : 1 : }
1946 [ + + ]: 2 : }
1947 [ + + ]: 3 : }
1948 [ + + ][ + + ]: 5 : }
[ + + ]
1949 : : }
1950 : 304 : Node cmp_con = d_nm->mkNode(Kind::STRING_CONTAINS, node[0], node[1]);
1951 : : // note we make a full recursive call to extended rewrite here, which should
1952 : : // be fine since the term we are rewriting is simpler than the current one.
1953 : 152 : Node cmp_conr = extendedRewrite(cmp_con);
1954 [ + + ][ + + ]: 152 : if (cmp_conr.getKind() == Kind::EQUAL || cmp_conr.getKind() == Kind::AND)
[ + + ]
1955 : : {
1956 : 19 : TypeNode stype = node.getType();
1957 : : // Rewriting the str.contains may return equalities of the form (= x "").
1958 : : // In that case, we can substitute the variables appearing in those
1959 : : // equalities with the empty string in the third argument of the
1960 : : // str.replace. For example:
1961 : : //
1962 : : // (str.replace x (str.++ x y) y) --> (str.replace x (str.++ x y) "")
1963 : : //
1964 : : // This can be done because str.replace changes x iff (str.++ x y) is in x
1965 : : // but that means that y must be empty in that case. Thus, we can
1966 : : // substitute y with "" in the third argument. Note that the third
1967 : : // argument does not matter when the str.replace does not apply.
1968 : : //
1969 : 19 : Node empty = strings::Word::mkEmptyWord(stype);
1970 : 19 : std::vector<Node> emptyNodes;
1971 : : bool allEmptyEqs;
1972 : 19 : std::tie(allEmptyEqs, emptyNodes) =
1973 : 38 : strings::utils::collectEmptyEqs(cmp_conr);
1974 [ + + ]: 19 : if (emptyNodes.size() > 0)
1975 : : {
1976 : : // Perform the substitutions
1977 : 36 : std::vector<TNode> substs(emptyNodes.size(), TNode(empty));
1978 : : Node nn2 = node[2].substitute(
1979 : 18 : emptyNodes.begin(), emptyNodes.end(), substs.begin(), substs.end());
1980 : :
1981 : : // If the contains rewrites to a conjunction of empty-string equalities
1982 : : // and we are doing the replacement in an empty string, we can rewrite
1983 : : // the string-to-replace with a concatenation of all the terms that must
1984 : : // be empty:
1985 : : //
1986 : : // (str.replace "" y z) ---> (str.replace "" (str.++ y1 ... yn) z)
1987 : : // if (str.contains "" y) ---> (and (= y1 "") ... (= yn ""))
1988 [ + + ][ + + ]: 18 : if (node[0] == empty && allEmptyEqs)
[ + - ][ + + ]
[ - - ]
1989 : : {
1990 : : std::vector<Node> emptyNodesList(emptyNodes.begin(),
1991 : 12 : emptyNodes.end());
1992 : 12 : Node nn1 = strings::utils::mkConcat(emptyNodesList, stype);
1993 : 12 : if (nn1 != node[1] || nn2 != node[2])
1994 : : {
1995 : 8 : Node res = d_nm->mkNode(Kind::STRING_REPLACE, node[0], nn1, nn2);
1996 : 4 : debugExtendedRewrite(node, res, "RPL_EMP_CNTS_SUBSTS");
1997 : 4 : return res;
1998 : 4 : }
1999 [ + + ][ + + ]: 16 : }
2000 : :
2001 [ + + ]: 14 : if (nn2 != node[2])
2002 : : {
2003 : 8 : Node res = d_nm->mkNode(Kind::STRING_REPLACE, node[0], node[1], nn2);
2004 : 4 : debugExtendedRewrite(node, res, "RPL_CNTS_SUBSTS");
2005 : 4 : return res;
2006 : 4 : }
2007 [ + + ][ + + ]: 26 : }
2008 [ + + ][ + + ]: 35 : }
[ + + ]
2009 [ + + ][ + + ]: 160 : }
2010 [ + + ]: 11773 : else if (k == Kind::STRING_CONTAINS)
2011 : : {
2012 [ + + ]: 5104 : if (node[0].getKind() == Kind::STRING_REPLACE)
2013 : : {
2014 : 12 : TypeNode stype = node[0].getType();
2015 : 12 : Node empty = strings::Word::mkEmptyWord(stype);
2016 : 12 : if (node[1].isConst() && node[0][1].isConst() && node[0][2].isConst())
2017 : : {
2018 : 12 : if (node[1] != empty && node[0][1] != empty && node[0][2] != empty
2019 : 10 : && !strings::Word::hasBidirectionalOverlap(node[1], node[0][1])
2020 : 12 : && !strings::Word::hasBidirectionalOverlap(node[1], node[0][2]))
2021 : : {
2022 : : // (str.contains (str.replace x c1 c2) c3) ---> (str.contains x c3)
2023 : : // if there is no overlap between c1 and c3 and none between c2 and c3
2024 : 2 : Node ret = d_nm->mkNode(Kind::STRING_CONTAINS, node[0][0], node[1]);
2025 : 1 : debugExtendedRewrite(node, ret, "CTN_REPL_CNSTS_TO_CTN");
2026 : 1 : return ret;
2027 : 1 : }
2028 : : }
2029 : : // (str.contains (str.replace x y z) w) --->
2030 : : // (str.contains (str.replace x y "") w)
2031 : : // if (str.contains z w) ---> false and (str.len w) = 1
2032 [ + + ]: 11 : if (se.checkLengthOne(node[1]))
2033 : : {
2034 : 16 : Node ctn = se.checkContains(node[0][2], node[1]);
2035 [ + + ][ + - ]: 8 : if (!ctn.isNull() && !ctn.getConst<bool>())
[ + + ]
2036 : : {
2037 : : Node ret = d_nm->mkNode(
2038 : : Kind::STRING_CONTAINS,
2039 : 8 : d_nm->mkNode(Kind::STRING_REPLACE, node[0][0], node[0][1], empty),
2040 : 16 : node[1]);
2041 : 4 : debugExtendedRewrite(node, ret, "CTN_REPL_SIMP_REPL");
2042 : 4 : return ret;
2043 : 4 : }
2044 [ + + ]: 8 : }
2045 [ + + ][ + + ]: 17 : }
2046 : 5099 : std::vector<Node> nc1;
2047 : 5099 : strings::utils::getConcat(node[0], nc1);
2048 : 5099 : std::vector<Node> nc2;
2049 : 5099 : strings::utils::getConcat(node[1], nc2);
2050 : :
2051 : : // extended component-wise containment
2052 : 5099 : std::vector<Node> nc1rb;
2053 : 5099 : std::vector<Node> nc1re;
2054 [ + + ]: 5099 : if (se.componentContainsExt(nc1, nc2, nc1rb, nc1re) != -1)
2055 : : {
2056 : 14 : debugExtendedRewrite(node, d_true, "CTN_COMPONENT_EXT");
2057 : 14 : return d_true;
2058 : : }
2059 : :
2060 [ + + ]: 10174 : for (const Node& n : nc2)
2061 : : {
2062 : : // (str.contains x (str.++ w (str.replace x y x) z)) --->
2063 : : // (= x (str.++ w (str.replace x y x) z))
2064 : : //
2065 : 5092 : if (n.getKind() == Kind::STRING_REPLACE && node[0] == n[0]
2066 : 5092 : && node[0] == n[2])
2067 : : {
2068 : 0 : Node ret = d_nm->mkNode(Kind::EQUAL, node[0], node[1]);
2069 : 0 : debugExtendedRewrite(node, ret, "CTN_REPL_SELF");
2070 : 0 : return ret;
2071 : 0 : }
2072 : : }
2073 [ + + ][ + + ]: 5141 : }
[ + + ][ + + ]
2074 : : // otherwise, the use of recursive approximations and rewriting via
2075 : : // the entailment utilities may make a standard conditional rewrite
2076 : : // applicable.
2077 : 18189 : RewriteResponse rr = sr.postRewrite(node);
2078 [ + + ]: 18189 : if (rr.d_node != node)
2079 : : {
2080 : 13 : return rr.d_node;
2081 : : }
2082 : :
2083 : 18176 : return Node::null();
2084 : 18558 : }
2085 : :
2086 : 394 : Node ExtendedRewriter::extendedRewriteSets(const Node& node) const
2087 : : {
2088 [ + + ][ + + ]: 435 : if (node.getKind() == Kind::SET_MINUS && node[1].getKind() == Kind::SET_MINUS
[ - - ]
2089 : 435 : && node[1][0] == node[0])
2090 : : {
2091 : : // Note this cannot be a rewrite rule or a ppRewrite, since it impacts the
2092 : : // cardinality graph. In particular, if we internally inspect (set.minus A
2093 : : // (setminus A B)), for instance if we are splitting the Venn regions of A
2094 : : // and (set.minus A B), then we should not transform this to an intersection
2095 : : // term. (set.minus A (set.minus A B)) = (set.inter A B)
2096 : 3 : NodeManager* nm = d_nm;
2097 : 6 : Node ret = nm->mkNode(Kind::SET_INTER, node[0], node[1][1]);
2098 : 3 : debugExtendedRewrite(node, ret, "SET_MINUS_MINUS");
2099 : 3 : return ret;
2100 : 3 : }
2101 : 391 : return Node::null();
2102 : : }
2103 : :
2104 : 112730 : void ExtendedRewriter::debugExtendedRewrite(Node n,
2105 : : Node ret,
2106 : : const char* c) const
2107 : : {
2108 : 225460 : Assert(ret.isNull() || n.getType().isComparableTo(ret.getType()))
2109 [ - + ][ - + ]: 112730 : << "Extended rewrite does not preserve type: " << n << " --> " << ret;
[ - - ]
2110 [ - + ]: 112730 : if (TraceIsOn("q-ext-rewrite"))
2111 : : {
2112 [ - - ]: 0 : if (!ret.isNull())
2113 : : {
2114 [ - - ]: 0 : Trace("q-ext-rewrite-apply") << "sygus-extr : apply " << c << std::endl;
2115 [ - - ]: 0 : Trace("q-ext-rewrite") << "sygus-extr : " << c << " : " << n
2116 : 0 : << " rewrites to " << ret << std::endl;
2117 : : }
2118 : : }
2119 : 112730 : }
2120 : :
2121 : : } // namespace quantifiers
2122 : : } // namespace theory
2123 : : } // namespace cvc5::internal
|
