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/word.h"
25 : : #include "theory/strings/theory_strings_utils.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 : 570210 : ExtendedRewriter::ExtendedRewriter(NodeManager* nm, Rewriter& rew, bool aggr)
46 : 570210 : : d_nm(nm), d_rew(rew), d_aggr(aggr)
47 : : {
48 : 570210 : d_true = d_nm->mkConst(true);
49 : 570210 : d_false = d_nm->mkConst(false);
50 : 570210 : d_intZero = d_nm->mkConstInt(Rational(0));
51 : 570210 : }
52 : :
53 : 568982 : void ExtendedRewriter::setCache(Node n, Node ret) const
54 : : {
55 [ + + ]: 568982 : if (d_aggr)
56 : : {
57 : : ExtRewriteAggAttribute erga;
58 : 562782 : n.setAttribute(erga, ret);
59 : : }
60 : : else
61 : : {
62 : : ExtRewriteAttribute era;
63 : 6200 : n.setAttribute(era, ret);
64 : : }
65 : 568982 : }
66 : :
67 : 1187489 : Node ExtendedRewriter::getCache(Node n) const
68 : : {
69 [ + + ]: 1187489 : if (d_aggr)
70 : : {
71 [ + + ]: 1173299 : if (n.hasAttribute(ExtRewriteAggAttribute()))
72 : : {
73 : 1775450 : return n.getAttribute(ExtRewriteAggAttribute());
74 : : }
75 : : }
76 : : else
77 : : {
78 [ + + ]: 14190 : if (n.hasAttribute(ExtRewriteAttribute()))
79 : : {
80 : 22180 : return n.getAttribute(ExtRewriteAttribute());
81 : : }
82 : : }
83 : 288674 : return Node::null();
84 : : }
85 : :
86 : 583985 : 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 : 583985 : if (dropDup
92 [ + + ][ + + ]: 583985 : && std::find(children.begin(), children.end(), nc) != children.end())
[ + + ]
93 : : {
94 : 7262 : return false;
95 : : }
96 : 576723 : children.push_back(nc);
97 : 576723 : return true;
98 : : }
99 : :
100 : 1187489 : Node ExtendedRewriter::extendedRewrite(Node n) const
101 : : {
102 [ + - ]: 1187489 : Trace("q-ext-rewrite-debug") << "extendedRewrite: " << n << std::endl;
103 : 1187489 : n = d_rew.rewrite(n);
104 : :
105 : : // has it already been computed?
106 : 1187489 : Node ncache = getCache(n);
107 [ + + ]: 1187489 : if (!ncache.isNull())
108 : : {
109 : 898815 : return ncache;
110 : : }
111 : :
112 : 288674 : Node ret = n;
113 : 288674 : NodeManager* nm = d_nm;
114 : :
115 : : //--------------------pre-rewrite
116 [ + + ]: 288674 : if (d_aggr)
117 : : {
118 : 285574 : Node pre_new_ret;
119 [ + + ]: 285574 : if (ret.getKind() == Kind::IMPLIES)
120 : : {
121 : 390 : pre_new_ret = nm->mkNode(Kind::OR, ret[0].negate(), ret[1]);
122 : 390 : debugExtendedRewrite(ret, pre_new_ret, "IMPLIES elim");
123 : : }
124 [ + + ]: 285184 : else if (ret.getKind() == Kind::XOR)
125 : : {
126 : 1882 : pre_new_ret = nm->mkNode(Kind::EQUAL, ret[0].negate(), ret[1]);
127 : 1882 : debugExtendedRewrite(ret, pre_new_ret, "XOR elim");
128 : : }
129 [ + + ]: 283302 : else if (ret.getKind() == Kind::NOT)
130 : : {
131 : 25439 : pre_new_ret = extendedRewriteNnf(ret);
132 : 25439 : debugExtendedRewrite(ret, pre_new_ret, "NNF");
133 : : }
134 [ + + ]: 285574 : if (!pre_new_ret.isNull())
135 : : {
136 : 8366 : ret = extendedRewrite(pre_new_ret);
137 : :
138 [ + - ]: 16732 : Trace("q-ext-rewrite-debug")
139 : 8366 : << "...ext-pre-rewrite : " << n << " -> " << pre_new_ret << std::endl;
140 : 8366 : setCache(n, ret);
141 : 8366 : return ret;
142 : : }
143 [ + + ]: 285574 : }
144 : : //--------------------end pre-rewrite
145 : :
146 : : //--------------------rewrite children
147 [ + + ]: 280308 : if (n.getNumChildren() > 0)
148 : : {
149 : 246946 : std::vector<Node> children;
150 [ + + ]: 246946 : if (n.getMetaKind() == metakind::PARAMETERIZED)
151 : : {
152 : 5260 : children.push_back(n.getOperator());
153 : : }
154 : 246946 : Kind k = n.getKind();
155 : 246946 : bool childChanged = false;
156 : 246946 : bool isNonAdditive = TermUtil::isNonAdditive(k);
157 : : // We flatten associative operators below, which requires k to be n-ary.
158 : 246946 : bool isAssoc = TermUtil::isAssoc(k, true);
159 [ + + ]: 824986 : for (unsigned i = 0; i < n.getNumChildren(); i++)
160 : : {
161 : 578040 : Node nc = extendedRewrite(n[i]);
162 [ + + ][ + + ]: 578040 : childChanged = nc != n[i] || childChanged;
[ + - ][ - - ]
163 [ + + ][ + + ]: 578040 : if (isAssoc && nc.getKind() == n.getKind())
[ + + ]
164 : : {
165 [ + + ]: 12943 : for (const Node& ncc : nc)
166 : : {
167 [ + + ]: 9444 : if (!addToChildren(ncc, children, isNonAdditive))
168 : : {
169 : 2986 : childChanged = true;
170 : : }
171 : 9444 : }
172 : : }
173 [ + + ]: 574541 : else if (!addToChildren(nc, children, isNonAdditive))
174 : : {
175 : 4276 : childChanged = true;
176 : : }
177 : 578040 : }
178 [ - + ][ - + ]: 246946 : Assert(!children.empty());
[ - - ]
179 : : // Some commutative operators have rewriters that are agnostic to order,
180 : : // thus, we sort here.
181 [ + + ][ + + ]: 246946 : if (TermUtil::isComm(k) && (d_aggr || children.size() <= 5))
[ + + ][ + + ]
182 : : {
183 : 145922 : childChanged = true;
184 : 145922 : std::sort(children.begin(), children.end());
185 : : }
186 [ + + ]: 246946 : if (childChanged)
187 : : {
188 [ + + ][ + + ]: 157996 : if (isNonAdditive && children.size() == 1)
[ + + ]
189 : : {
190 : : // we may have subsumed children down to one
191 : 70 : ret = children[0];
192 : : }
193 : 157926 : else if (isAssoc
194 [ + + ][ + + ]: 157926 : && 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 : 157924 : ret = nm->mkNode(k, children);
207 : : }
208 : : }
209 : 246946 : }
210 : 280308 : ret = d_rew.rewrite(ret);
211 : : //--------------------end rewrite children
212 : :
213 : : // now, do extended rewrite
214 [ + - ]: 560616 : Trace("q-ext-rewrite-debug") << "Do extended rewrite on : " << ret
215 : 280308 : << " (from " << n << ")" << std::endl;
216 : 280308 : Node new_ret;
217 : :
218 : : //---------------------- theory-independent post-rewriting
219 [ + + ]: 280308 : if (ret.getKind() == Kind::ITE)
220 : : {
221 : 21807 : new_ret = extendedRewriteIte(Kind::ITE, ret);
222 : : }
223 [ + + ][ + + ]: 258501 : else if (ret.getKind() == Kind::AND || ret.getKind() == Kind::OR)
[ + + ]
224 : : {
225 : 73928 : new_ret = extendedRewriteAndOr(ret);
226 : : }
227 [ + + ]: 184573 : else if (ret.getKind() == Kind::EQUAL)
228 : : {
229 : 57430 : new_ret = extendedRewriteEqChain(
230 : 28715 : Kind::EQUAL, Kind::AND, Kind::OR, Kind::NOT, ret);
231 [ + + ]: 28715 : if (!new_ret.isNull())
232 : : {
233 : 2043 : debugExtendedRewrite(ret, new_ret, "Bool eq-chain simplify");
234 : : }
235 : : else
236 : : {
237 : 26672 : TypeNode tret = ret[0].getType();
238 [ + + ]: 26672 : if (tret.isInteger())
239 : : {
240 : 13853 : strings::ArithEntail ae(nm, &d_rew);
241 : 13853 : new_ret = ae.rewritePredViaEntailment(ret);
242 [ + + ]: 13853 : if (!new_ret.isNull())
243 : : {
244 : 60 : debugExtendedRewrite(ret, new_ret, "String EQUAL len entailment");
245 : : }
246 : 13853 : }
247 [ + + ]: 12819 : else if (tret.isStringLike())
248 : : {
249 : 2021 : new_ret = extendedRewriteStrings(ret);
250 : : }
251 : 26672 : }
252 : : }
253 [ + + ]: 155858 : else if (ret.getKind() == Kind::GEQ)
254 : : {
255 [ + + ]: 16729 : if (ret[0].getType().isInteger())
256 : : {
257 : 16530 : strings::ArithEntail ae(nm, &d_rew);
258 : 16530 : new_ret = ae.rewritePredViaEntailment(ret);
259 [ + + ]: 16530 : if (!new_ret.isNull())
260 : : {
261 : 38 : debugExtendedRewrite(ret, new_ret, "String GEQ len entailment");
262 : : }
263 : 16530 : }
264 : : }
265 [ + + ][ + - ]: 280308 : Assert(new_ret.isNull() || new_ret != ret);
[ - + ][ - + ]
[ - - ]
266 [ + + ][ + + ]: 280308 : if (new_ret.isNull() && ret.getKind() != Kind::ITE)
[ + + ]
267 : : {
268 : : // simple ITE pulling
269 : 242250 : new_ret = extendedRewritePullIte(Kind::ITE, ret);
270 : : }
271 : : //----------------------end theory-independent post-rewriting
272 : :
273 : : //----------------------theory-specific post-rewriting
274 [ + + ]: 280308 : if (new_ret.isNull())
275 : : {
276 : : TheoryId tid;
277 [ + + ]: 249707 : if (ret.getKind() == Kind::ITE)
278 : : {
279 : 18707 : tid = Theory::theoryOf(ret.getType());
280 : : }
281 : : else
282 : : {
283 : 231000 : tid = Theory::theoryOf(ret);
284 : : }
285 [ + - ]: 499414 : Trace("q-ext-rewrite-debug") << "theoryOf( " << ret << " )= " << tid
286 : 249707 : << std::endl;
287 [ + + ][ + ]: 249707 : switch (tid)
288 : : {
289 : 16561 : case THEORY_STRINGS: new_ret = extendedRewriteStrings(ret); break;
290 : 330 : case THEORY_SETS: new_ret = extendedRewriteSets(ret); break;
291 : 232816 : default: break;
292 : : }
293 : : }
294 : : //----------------------end theory-specific post-rewriting
295 : :
296 : : //----------------------aggressive rewrites
297 [ + + ][ + + ]: 280308 : if (new_ret.isNull() && d_aggr)
[ + + ]
298 : : {
299 : 246857 : new_ret = extendedRewriteAggr(ret);
300 : : }
301 : : //----------------------end aggressive rewrites
302 : :
303 : 280308 : setCache(n, ret);
304 [ + + ]: 280308 : if (!new_ret.isNull())
305 : : {
306 : 30721 : ret = extendedRewrite(new_ret);
307 : : }
308 [ + - ]: 560616 : Trace("q-ext-rewrite-debug") << "...ext-rewrite : " << n << " -> " << ret
309 : 280308 : << std::endl;
310 [ - + ]: 280308 : 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 : 280308 : setCache(n, ret);
318 : 280308 : return ret;
319 : 1187489 : }
320 : :
321 : 246857 : Node ExtendedRewriter::extendedRewriteAggr(Node n) const
322 : : {
323 : 246857 : Node new_ret;
324 [ + - ]: 493714 : Trace("q-ext-rewrite-debug2")
325 : 246857 : << "Do aggressive rewrites on " << n << std::endl;
326 : 246857 : bool polarity = n.getKind() != Kind::NOT;
327 [ + + ]: 246857 : Node ret_atom = n.getKind() == Kind::NOT ? n[0] : n;
328 : 272940 : if ((ret_atom.getKind() == Kind::EQUAL && ret_atom[0].getType().isRealOrInt())
329 [ + + ][ + + ]: 272940 : || 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 [ + - ]: 70726 : Trace("q-ext-rewrite-debug2")
334 : 35363 : << "Compute monomial sum " << ret_atom << std::endl;
335 : : // compute monomial sum
336 : 35363 : std::map<Node, Node> msum;
337 [ + - ]: 35363 : if (ArithMSum::getMonomialSumLit(ret_atom, msum))
338 : : {
339 [ + + ]: 108653 : for (std::map<Node, Node>::iterator itm = msum.begin(); itm != msum.end();
340 : 73290 : ++itm)
341 : : {
342 : 73354 : Node v = itm->first;
343 [ + - ]: 146708 : Trace("q-ext-rewrite-debug2")
344 : 73354 : << itm->first << " * " << itm->second << std::endl;
345 [ + + ]: 73354 : 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 [ + + ]: 73354 : }
371 : : }
372 : : else
373 : : {
374 [ - - ]: 0 : Trace("q-ext-rewrite-debug")
375 : 0 : << " failed to get monomial sum of " << n << std::endl;
376 : : }
377 : 35363 : }
378 : : // TODO (#1706) : conditional rewriting, condition merging
379 : 493714 : return new_ret;
380 : 246857 : }
381 : :
382 : 29949 : Node ExtendedRewriter::extendedRewriteIte(Kind itek, Node n, bool full) const
383 : : {
384 [ - + ][ - + ]: 29949 : Assert(n.getKind() == itek);
[ - - ]
385 [ - + ][ - + ]: 29949 : Assert(n[1] != n[2]);
[ - - ]
386 : :
387 : 29949 : NodeManager* nm = d_nm;
388 : :
389 [ + - ]: 29949 : Trace("ext-rew-ite") << "Rewrite ITE : " << n << std::endl;
390 : :
391 : 29949 : Node flip_cond;
392 [ - + ]: 29949 : if (n[0].getKind() == Kind::NOT)
393 : : {
394 : 0 : flip_cond = n[0][0];
395 : : }
396 [ + + ]: 29949 : else if (n[0].getKind() == Kind::OR)
397 : : {
398 : : // a | b ---> ~( ~a & ~b )
399 : 332 : flip_cond = TermUtil::simpleNegate(n[0]);
400 : : }
401 [ + + ]: 29949 : if (!flip_cond.isNull())
402 : : {
403 : 664 : Node new_ret = nm->mkNode(Kind::ITE, flip_cond, n[2], n[1]);
404 : : // only print debug trace if full=true
405 [ + - ]: 332 : if (full)
406 : : {
407 : 332 : debugExtendedRewrite(n, new_ret, "ITE flip");
408 : : }
409 : 332 : return new_ret;
410 : 332 : }
411 : : // Boolean true/false return
412 : 29617 : TypeNode tn = n.getType();
413 [ + + ]: 29617 : if (tn.isBoolean())
414 : : {
415 [ + + ]: 37638 : for (unsigned i = 1; i <= 2; i++)
416 : : {
417 [ - + ]: 25092 : 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 : 29617 : std::vector<Node> eq_conds;
446 : 29617 : Kind ck = n[0].getKind();
447 [ + + ]: 29617 : if (ck == Kind::EQUAL)
448 : : {
449 : 10999 : eq_conds.push_back(n[0]);
450 : : }
451 [ + + ]: 18618 : else if (ck == Kind::AND)
452 : : {
453 [ + + ]: 24710 : for (const Node& cn : n[0])
454 : : {
455 [ + + ]: 19602 : if (cn.getKind() == Kind::EQUAL)
456 : : {
457 : 2160 : eq_conds.push_back(cn);
458 : : }
459 : 24710 : }
460 : : }
461 : :
462 : 29617 : Node new_ret;
463 : 29617 : Node b;
464 : 29617 : Node e;
465 : 29617 : Node t1 = n[1];
466 : 29617 : Node t2 = n[2];
467 : 29617 : std::stringstream ss_reason;
468 : :
469 [ + + ]: 42690 : for (const Node& eq : eq_conds)
470 : : {
471 : : // simple invariant ITE
472 [ + + ]: 39350 : 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 : 26277 : if (t2 == eq[i] && t1 == eq[1 - i])
477 : : {
478 : 86 : new_ret = t2;
479 : 86 : ss_reason << "ITE simple rev subs";
480 : 86 : break;
481 : : }
482 : : }
483 [ + + ]: 13159 : if (!new_ret.isNull())
484 : : {
485 : 86 : break;
486 : : }
487 : : }
488 [ + + ]: 29617 : if (new_ret.isNull())
489 : : {
490 : : // merging branches
491 [ + + ]: 87479 : for (unsigned i = 1; i <= 2; i++)
492 : : {
493 [ + + ]: 58640 : if (n[i].getKind() == Kind::ITE)
494 : : {
495 : 8684 : Node no = n[3 - i];
496 [ + + ]: 25098 : for (unsigned j = 1; j <= 2; j++)
497 : : {
498 [ + + ]: 17106 : if (n[i][j] == no)
499 : : {
500 : : // e.g.
501 : : // ite( C1, ite( C2, t1, t2 ), t1 ) ----> ite( C1 ^ ~C2, t2, t1 )
502 [ + + ][ + + ]: 692 : Node nc1 = i == 2 ? n[0].negate() : n[0];
[ - - ]
503 : 1384 : Node nc2 = j == 1 ? n[i][0].negate() : n[i][0];
504 : 1384 : Node new_cond = nm->mkNode(Kind::AND, nc1, nc2);
505 : 692 : new_ret = nm->mkNode(Kind::ITE, new_cond, n[i][3 - j], no);
506 : 692 : ss_reason << "ITE merge branch";
507 : 692 : break;
508 : 692 : }
509 : : }
510 : 8684 : }
511 [ + + ]: 58640 : if (!new_ret.isNull())
512 : : {
513 : 692 : break;
514 : : }
515 : : }
516 : : }
517 : :
518 [ + + ][ + + ]: 29617 : 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 : 28833 : Subs subs;
523 : 28833 : inferSubstitution(n[0], subs, true);
524 : :
525 [ + - ]: 28833 : 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 : 28833 : Node nn = subs.apply(t2);
533 [ + + ]: 28833 : if (nn != t2)
534 : : {
535 : 9315 : nn = d_rew.rewrite(nn);
536 [ + + ]: 9315 : if (nn == t1)
537 : : {
538 : 110 : new_ret = t2;
539 : 110 : 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 : 28833 : std::map<Kind, bool> rkinds;
546 : 28833 : nn = partialSubstitute(t1, subs, rkinds);
547 : 28833 : nn = d_rew.rewrite(nn);
548 [ + + ]: 28833 : 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 [ + + ]: 5496 : if (nn == t2)
555 : : {
556 : 152 : new_ret = nn;
557 : 152 : ss_reason << "ITE subs invariant";
558 : : }
559 [ + + ][ + + ]: 5344 : else if (full || nn.isConst())
[ + + ]
560 : : {
561 : 1360 : new_ret = nm->mkNode(itek, n[0], nn, t2);
562 : 1360 : ss_reason << "ITE subs";
563 : : }
564 : : }
565 : 28833 : }
566 [ + + ]: 28833 : 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 : 27211 : std::map<Node, Node> assign;
571 : 27211 : assign[n[0]] = d_false;
572 : 27211 : std::map<Kind, bool> rkinds;
573 : 27211 : Node nn = partialSubstitute(t2, assign, rkinds);
574 [ + + ]: 27211 : if (nn != t2)
575 : : {
576 : 3592 : nn = d_rew.rewrite(nn);
577 [ + + ]: 3592 : if (nn == t1)
578 : : {
579 : 68 : new_ret = nn;
580 : 68 : ss_reason << "ITE subs invariant false";
581 : : }
582 [ + + ][ - + ]: 3524 : else if (full || nn.isConst())
[ + + ]
583 : : {
584 : 438 : new_ret = nm->mkNode(itek, n[0], t1, nn);
585 : 438 : ss_reason << "ITE subs false";
586 : : }
587 : : }
588 : 27211 : }
589 : 28833 : }
590 : :
591 : : // only print debug trace if full=true
592 [ + + ][ + + ]: 29617 : if (!new_ret.isNull() && full)
[ + + ]
593 : : {
594 : 2768 : debugExtendedRewrite(n, new_ret, ss_reason.str().c_str());
595 : : }
596 : :
597 : 29617 : return new_ret;
598 : 29949 : }
599 : :
600 : 73928 : Node ExtendedRewriter::extendedRewriteAndOr(Node n) const
601 : : {
602 : : // all the below rewrites are aggressive
603 [ + + ]: 73928 : if (!d_aggr)
604 : : {
605 : 66 : return Node::null();
606 : : }
607 : 73862 : Node new_ret;
608 : : // we allow substitutions to recurse over any kind, except WITNESS which is
609 : : // managed by partialSubstitute.
610 : 73862 : std::map<Kind, bool> bcp_kinds;
611 : 73862 : new_ret = extendedRewriteBcp(Kind::AND, Kind::OR, Kind::NOT, bcp_kinds, n);
612 [ + + ]: 73862 : if (!new_ret.isNull())
613 : : {
614 : 3032 : debugExtendedRewrite(n, new_ret, "Bool bcp");
615 : 3032 : return new_ret;
616 : : }
617 : : // factoring
618 : 70830 : new_ret = extendedRewriteFactoring(Kind::AND, Kind::OR, n);
619 [ + + ]: 70830 : if (!new_ret.isNull())
620 : : {
621 : 959 : debugExtendedRewrite(n, new_ret, "Bool factoring");
622 : 959 : return new_ret;
623 : : }
624 : :
625 : : // equality resolution
626 : 139742 : new_ret = extendedRewriteEqRes(
627 : 69871 : Kind::AND, Kind::OR, Kind::EQUAL, Kind::NOT, bcp_kinds, n, false);
628 : 69871 : debugExtendedRewrite(n, new_ret, "Bool eq res");
629 : 69871 : return new_ret;
630 : 73862 : }
631 : :
632 : 243620 : Node ExtendedRewriter::extendedRewritePullIte(Kind itek, Node n) const
633 : : {
634 [ - + ][ - + ]: 243620 : Assert(n.getKind() != Kind::ITE);
[ - - ]
635 [ + + ]: 243620 : if (n.isClosure())
636 : : {
637 : : // don't pull ITE out of quantifiers
638 : 2185 : return n;
639 : : }
640 : 241435 : NodeManager* nm = d_nm;
641 : 241435 : TypeNode tn = n.getType();
642 : 241435 : std::vector<Node> children;
643 : 241435 : bool hasOp = (n.getMetaKind() == metakind::PARAMETERIZED);
644 [ + + ]: 241435 : if (hasOp)
645 : : {
646 : 5403 : children.push_back(n.getOperator());
647 : : }
648 : 241435 : unsigned nchildren = n.getNumChildren();
649 [ + + ]: 704212 : for (unsigned i = 0; i < nchildren; i++)
650 : : {
651 : 462777 : children.push_back(n[i]);
652 : : }
653 : 241435 : std::map<unsigned, std::map<unsigned, Node> > ite_c;
654 [ + + ]: 689368 : 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 [ + + ]: 456924 : if (n[i].getKind() == itek)
660 : : {
661 [ + + ]: 17163 : unsigned ii = hasOp ? i + 1 : i;
662 [ + + ]: 51489 : for (unsigned j = 0; j < 2; j++)
663 : : {
664 : 34326 : children[ii] = n[i][j + 1];
665 : 34326 : Node pull = nm->mkNode(n.getKind(), children);
666 : 34326 : Node pullr = d_rew.rewrite(pull);
667 : 34326 : children[ii] = n[i];
668 : 34326 : ite_c[i][j] = pullr;
669 : 34326 : }
670 [ + + ]: 17163 : 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 : 1043 : debugExtendedRewrite(n, ite_c[i][0], "ITE dual invariant");
676 : 2086 : return ite_c[i][0];
677 : : }
678 : 27446 : if (nchildren == 2 && (n[1 - i].isVar() || n[1 - i].isConst())
679 : 27446 : && !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 : 14420 : Node new_ret = nm->mkNode(Kind::ITE, n[i][0], ite_c[i][0], ite_c[i][1]);
684 : 7210 : debugExtendedRewrite(n, new_ret, "ITE pull var predicate");
685 : 7210 : return new_ret;
686 : 7210 : }
687 [ + + ]: 25560 : for (unsigned j = 0; j < 2; j++)
688 : : {
689 : 17388 : Node pullr = ite_c[i][j];
690 : 17388 : 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 : 738 : Node new_ret;
697 [ + + ][ + - ]: 738 : if (tn.isBoolean() && pullr.isConst())
[ + + ]
698 : : {
699 : : // remove false/true child immediately
700 : 100 : bool pol = pullr.getConst<bool>();
701 : 100 : std::vector<Node> new_children;
702 : 100 : new_children.push_back((j == 0) == pol ? n[i][0]
703 : : : n[i][0].negate());
704 : 100 : new_children.push_back(ite_c[i][1 - j]);
705 [ + + ]: 100 : new_ret = nm->mkNode(pol ? Kind::OR : Kind::AND, new_children);
706 : 100 : debugExtendedRewrite(n, new_ret, "ITE Bool single elim");
707 : 100 : }
708 : : else
709 : : {
710 : 638 : new_ret = nm->mkNode(itek, n[i][0], ite_c[i][0], ite_c[i][1]);
711 : 638 : debugExtendedRewrite(n, new_ret, "ITE single elim");
712 : : }
713 : 738 : return new_ret;
714 : 738 : }
715 [ + + ]: 17388 : }
716 : : }
717 : : }
718 [ + + ]: 232444 : if (d_aggr)
719 : : {
720 [ + + ]: 237648 : for (std::pair<const unsigned, std::map<unsigned, Node> >& ip : ite_c)
721 : : {
722 : 8142 : Node nite = n[ip.first];
723 [ - + ][ - + ]: 8142 : Assert(nite.getKind() == itek);
[ - - ]
724 : : // now, simply pull the ITE and try ITE rewrites
725 : 16284 : Node pull_ite = nm->mkNode(itek, nite[0], ip.second[0], ip.second[1]);
726 : 8142 : pull_ite = d_rew.rewrite(pull_ite);
727 [ + - ]: 8142 : if (pull_ite.getKind() == Kind::ITE)
728 : : {
729 : 8142 : Node new_pull_ite = extendedRewriteIte(itek, pull_ite, false);
730 [ + + ]: 8142 : if (!new_pull_ite.isNull())
731 : : {
732 : 138 : debugExtendedRewrite(n, new_pull_ite, "ITE pull rewrite");
733 : 138 : return new_pull_ite;
734 : : }
735 [ + + ]: 8142 : }
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 [ + + ][ + + ]: 8280 : }
748 : : }
749 : :
750 : 232306 : return Node::null();
751 : 241435 : }
752 : :
753 : 25439 : Node ExtendedRewriter::extendedRewriteNnf(Node ret) const
754 : : {
755 [ - + ][ - + ]: 25439 : Assert(ret.getKind() == Kind::NOT);
[ - - ]
756 : :
757 : 25439 : Kind nk = ret[0].getKind();
758 : 25439 : bool neg_ch = false;
759 : 25439 : bool neg_ch_1 = false;
760 [ + + ][ + + ]: 25439 : if (nk == Kind::AND || nk == Kind::OR)
761 : : {
762 : 4590 : neg_ch = true;
763 [ + + ]: 4590 : nk = nk == Kind::AND ? Kind::OR : Kind::AND;
764 : : }
765 [ + + ]: 20849 : else if (nk == Kind::IMPLIES)
766 : : {
767 : 20 : neg_ch = true;
768 : 20 : neg_ch_1 = true;
769 : 20 : nk = Kind::AND;
770 : : }
771 [ + + ]: 20829 : else if (nk == Kind::ITE)
772 : : {
773 : 1031 : neg_ch = true;
774 : 1031 : neg_ch_1 = true;
775 : : }
776 [ + + ]: 19798 : else if (nk == Kind::XOR)
777 : : {
778 : 60 : nk = Kind::EQUAL;
779 : : }
780 : 19738 : else if (nk == Kind::EQUAL && ret[0][0].getType().isBoolean())
781 : : {
782 : 393 : neg_ch_1 = true;
783 : : }
784 : : else
785 : : {
786 : 19345 : return Node::null();
787 : : }
788 : :
789 : 6094 : std::vector<Node> new_children;
790 [ + + ]: 26076 : for (unsigned i = 0, nchild = ret[0].getNumChildren(); i < nchild; i++)
791 : : {
792 : 19982 : Node c = ret[0][i];
793 [ + + ][ + + ]: 19982 : c = (i == 0 ? neg_ch_1 : false) != neg_ch ? c.negate() : c;
[ + + ]
794 : 19982 : new_children.push_back(c);
795 : 19982 : }
796 : 6094 : return d_nm->mkNode(nk, new_children);
797 : 6094 : }
798 : :
799 : 73862 : Node ExtendedRewriter::extendedRewriteBcp(Kind andk,
800 : : Kind ork,
801 : : Kind notk,
802 : : std::map<Kind, bool>& bcp_kinds,
803 : : Node ret) const
804 : : {
805 : 73862 : Kind k = ret.getKind();
806 [ + + ][ + - ]: 73862 : Assert(k == andk || k == ork);
[ - + ][ - + ]
[ - - ]
807 [ + - ]: 73862 : Trace("ext-rew-bcp") << "BCP: **** INPUT: " << ret << std::endl;
808 : :
809 : 73862 : NodeManager* nm = d_nm;
810 : :
811 : 73862 : TypeNode tn = ret.getType();
812 : 73862 : Node truen = TermUtil::mkTypeMaxValue(tn);
813 : 73862 : Node falsen = TermUtil::mkTypeValue(tn, 0);
814 : :
815 : : // terms to process
816 : 73862 : std::vector<Node> to_process;
817 [ + + ]: 269519 : for (const Node& cn : ret)
818 : : {
819 : 195657 : to_process.push_back(cn);
820 : 195657 : }
821 : : // the processing terms
822 : 73862 : std::vector<Node> clauses;
823 : : // the terms we have propagated information to
824 : 73862 : std::unordered_set<Node> prop_clauses;
825 : : // the assignment
826 : 73862 : std::map<Node, Node> assign;
827 : 73862 : std::vector<Node> avars;
828 : 73862 : std::vector<Node> asubs;
829 : :
830 [ + + ]: 73862 : Kind ok = k == andk ? ork : andk;
831 : : // global polarity : when k=ork, everything is negated
832 : 73862 : bool gpol = k == andk;
833 : :
834 : : do
835 : : {
836 : : // process the current nodes
837 [ + + ]: 152198 : while (!to_process.empty())
838 : : {
839 : 76632 : std::vector<Node> new_to_process;
840 [ + + ]: 274969 : for (const Node& cn : to_process)
841 : : {
842 [ + - ]: 199089 : Trace("ext-rew-bcp-debug") << "process " << cn << std::endl;
843 : 199089 : Kind cnk = cn.getKind();
844 : 199089 : bool pol = cnk != notk;
845 [ + + ]: 199089 : Node cln = cnk == notk ? cn[0] : cn;
846 [ - + ][ - + ]: 199089 : Assert(cln.getKind() != notk);
[ - - ]
847 [ + + ][ + + ]: 199089 : if ((pol && cln.getKind() == k) || (!pol && cln.getKind() == ok))
[ + + ][ + + ]
[ + + ]
848 : : {
849 : : // flatten
850 [ + + ]: 1146 : for (const Node& ccln : cln)
851 : : {
852 [ + + ][ + + ]: 822 : Node lccln = pol ? ccln : TermUtil::mkNegate(notk, ccln);
[ - - ]
853 : 822 : new_to_process.push_back(lccln);
854 : 822 : }
855 : : }
856 : : else
857 : : {
858 : : // add it to the assignment
859 [ + + ]: 198765 : Node val = gpol == pol ? truen : falsen;
860 : 198765 : std::map<Node, Node>::iterator it = assign.find(cln);
861 [ + - ]: 397530 : Trace("ext-rew-bcp") << "BCP: assign " << cln << " -> " << val
862 : 198765 : << std::endl;
863 [ + + ]: 198765 : if (it != assign.end())
864 : : {
865 [ + + ]: 830 : if (val != it->second)
866 : : {
867 [ + - ]: 752 : Trace("ext-rew-bcp") << "BCP: conflict!" << std::endl;
868 : : // a conflicting assignment: we are done
869 [ + + ]: 752 : return gpol ? falsen : truen;
870 : : }
871 : : }
872 : : else
873 : : {
874 : 197935 : assign[cln] = val;
875 : 197935 : avars.push_back(cln);
876 : 197935 : asubs.push_back(val);
877 : : }
878 : :
879 : : // also, treat it as clause if possible
880 : 198013 : if (cln.getNumChildren() > 0
881 [ + + ][ - + ]: 198013 : && (bcp_kinds.empty()
882 [ - - ][ + + ]: 198013 : || bcp_kinds.find(cln.getKind()) != bcp_kinds.end()))
883 : : {
884 : 173218 : if (std::find(clauses.begin(), clauses.end(), cn) == clauses.end()
885 [ + + ][ + - ]: 173218 : && prop_clauses.find(cn) == prop_clauses.end())
[ + + ]
886 : : {
887 [ + - ]: 173178 : Trace("ext-rew-bcp") << "BCP: new clause: " << cn << std::endl;
888 : 173178 : clauses.push_back(cn);
889 : : }
890 : : }
891 [ + + ]: 198765 : }
892 [ + + ]: 199089 : }
893 : 75880 : to_process.clear();
894 : 151760 : to_process.insert(
895 : 75880 : to_process.end(), new_to_process.begin(), new_to_process.end());
896 [ + + ]: 76632 : }
897 : :
898 : : // apply substitution to all subterms of clauses
899 : 75566 : std::vector<Node> new_clauses;
900 [ + + ]: 252041 : for (const Node& c : clauses)
901 : : {
902 : 176475 : bool cpol = c.getKind() != notk;
903 [ + + ]: 176475 : Node ca = c.getKind() == notk ? c[0] : c;
904 : 176475 : bool childChanged = false;
905 : 176475 : std::vector<Node> ccs_children;
906 [ + + ]: 583945 : for (const Node& cc : ca)
907 : : {
908 : : // always use partial substitute, to avoid substitution in witness
909 [ + - ]: 407470 : Trace("ext-rew-bcp-debug") << "...do partial substitute" << std::endl;
910 : : // substitution is only applicable to compatible kinds in bcp_kinds
911 : 407470 : Node ccs = partialSubstitute(cc, assign, bcp_kinds);
912 [ + + ][ + + ]: 407470 : childChanged = childChanged || ccs != cc;
913 : 407470 : ccs_children.push_back(ccs);
914 : 407470 : }
915 [ + + ]: 176475 : if (childChanged)
916 : : {
917 [ - + ]: 3022 : if (ca.getMetaKind() == metakind::PARAMETERIZED)
918 : : {
919 : 0 : ccs_children.insert(ccs_children.begin(), ca.getOperator());
920 : : }
921 : 3022 : Node ccs = nm->mkNode(ca.getKind(), ccs_children);
922 [ + + ][ + + ]: 3022 : ccs = cpol ? ccs : TermUtil::mkNegate(notk, ccs);
[ - - ]
923 [ + - ]: 6044 : Trace("ext-rew-bcp") << "BCP: propagated " << c << " -> " << ccs
924 : 3022 : << std::endl;
925 : 3022 : ccs = d_rew.rewrite(ccs);
926 [ + - ]: 3022 : Trace("ext-rew-bcp") << "BCP: rewritten to " << ccs << std::endl;
927 : 3022 : 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 : 3022 : prop_clauses.insert(ca);
931 : 3022 : }
932 : : else
933 : : {
934 : 173453 : new_clauses.push_back(c);
935 : : }
936 : 176475 : }
937 : 75566 : clauses.clear();
938 : 75566 : clauses.insert(clauses.end(), new_clauses.begin(), new_clauses.end());
939 [ + + ]: 75566 : } while (!to_process.empty());
940 : :
941 : : // remake the node
942 [ + + ]: 73110 : if (!prop_clauses.empty())
943 : : {
944 : 2280 : std::vector<Node> children;
945 [ + + ]: 14276 : for (std::pair<const Node, Node>& l : assign)
946 : : {
947 : 11996 : Node a = l.first;
948 : : // if propagation did not touch a
949 [ + + ]: 11996 : if (prop_clauses.find(a) == prop_clauses.end())
950 : : {
951 [ + + ][ + - ]: 8978 : Assert(l.second == truen || l.second == falsen);
[ - + ][ - + ]
[ - - ]
952 [ + + ][ + + ]: 8978 : Node ln = (l.second == truen) == gpol ? a : TermUtil::mkNegate(notk, a);
[ - - ]
953 : 8978 : children.push_back(ln);
954 : 8978 : }
955 : 11996 : }
956 [ + + ]: 2280 : Node new_ret = children.size() == 1 ? children[0] : nm->mkNode(k, children);
957 [ + - ]: 2280 : Trace("ext-rew-bcp") << "BCP: **** OUTPUT: " << new_ret << std::endl;
958 : 2280 : return new_ret;
959 : 2280 : }
960 : :
961 : 70830 : return Node::null();
962 : 73862 : }
963 : :
964 : 70830 : Node ExtendedRewriter::extendedRewriteFactoring(Kind andk,
965 : : Kind ork,
966 : : Node n) const
967 : : {
968 [ + - ]: 70830 : Trace("ext-rew-factoring") << "Factoring: *** INPUT: " << n << std::endl;
969 : 70830 : NodeManager* nm = d_nm;
970 : :
971 : 70830 : Kind nk = n.getKind();
972 [ + + ][ + - ]: 70830 : Assert(nk == andk || nk == ork);
[ - + ][ - + ]
[ - - ]
973 [ + + ]: 70830 : Kind onk = nk == andk ? ork : andk;
974 : : // count the number of times atoms occur
975 : 70830 : std::map<Node, std::vector<Node> > lit_to_cl;
976 : 70830 : std::map<Node, std::vector<Node> > cl_to_lits;
977 [ + + ]: 255610 : for (const Node& nc : n)
978 : : {
979 : 184780 : Kind nck = nc.getKind();
980 [ + + ]: 184780 : if (nck == onk)
981 : : {
982 [ + + ]: 73560 : for (const Node& ncl : nc)
983 : : {
984 : 57521 : if (std::find(lit_to_cl[ncl].begin(), lit_to_cl[ncl].end(), nc)
985 [ + - ]: 115042 : == lit_to_cl[ncl].end())
986 : : {
987 : 57521 : lit_to_cl[ncl].push_back(nc);
988 : 57521 : cl_to_lits[nc].push_back(ncl);
989 : : }
990 : 57521 : }
991 : : }
992 : : else
993 : : {
994 : 168741 : lit_to_cl[nc].push_back(nc);
995 : 168741 : cl_to_lits[nc].push_back(nc);
996 : : }
997 : 184780 : }
998 : : // get the maximum shared literal to factor
999 : 70830 : unsigned max_size = 0;
1000 : 70830 : Node flit;
1001 [ + + ]: 289563 : for (const std::pair<const Node, std::vector<Node> >& ltc : lit_to_cl)
1002 : : {
1003 [ + + ]: 218733 : if (ltc.second.size() > max_size)
1004 : : {
1005 : 71459 : max_size = ltc.second.size();
1006 : 71459 : flit = ltc.first;
1007 : : }
1008 : : }
1009 [ + + ]: 70830 : if (max_size > 1)
1010 : : {
1011 : : // do the factoring
1012 : 959 : std::vector<Node> children;
1013 : 959 : std::vector<Node> fchildren;
1014 : 959 : std::map<Node, std::vector<Node> >::iterator itl = lit_to_cl.find(flit);
1015 : 959 : std::vector<Node>& cls = itl->second;
1016 [ + + ]: 4371 : for (const Node& nc : n)
1017 : : {
1018 [ + + ]: 3412 : if (std::find(cls.begin(), cls.end(), nc) == cls.end())
1019 : : {
1020 : 852 : children.push_back(nc);
1021 : : }
1022 : : else
1023 : : {
1024 : : // rebuild
1025 : 2560 : std::vector<Node>& lits = cl_to_lits[nc];
1026 : : std::vector<Node>::iterator itlfl =
1027 : 2560 : std::find(lits.begin(), lits.end(), flit);
1028 [ - + ][ - + ]: 2560 : Assert(itlfl != lits.end());
[ - - ]
1029 : 2560 : lits.erase(itlfl);
1030 : : // rebuild
1031 [ + - ]: 2560 : if (!lits.empty())
1032 : : {
1033 [ + + ]: 2560 : Node new_cl = lits.size() == 1 ? lits[0] : nm->mkNode(onk, lits);
1034 : 2560 : fchildren.push_back(new_cl);
1035 : 2560 : }
1036 : : }
1037 : 3412 : }
1038 : : // rebuild the factored children
1039 [ - + ][ - + ]: 959 : Assert(!fchildren.empty());
[ - - ]
1040 [ - + ]: 959 : Node fcn = fchildren.size() == 1 ? fchildren[0] : nm->mkNode(nk, fchildren);
1041 : 959 : children.push_back(nm->mkNode(onk, flit, fcn));
1042 [ + + ]: 959 : Node ret = children.size() == 1 ? children[0] : nm->mkNode(nk, children);
1043 [ + - ]: 959 : Trace("ext-rew-factoring") << "Factoring: *** OUTPUT: " << ret << std::endl;
1044 : 959 : return ret;
1045 : 959 : }
1046 : : else
1047 : : {
1048 [ + - ]: 69871 : Trace("ext-rew-factoring") << "Factoring: no change" << std::endl;
1049 : : }
1050 : 69871 : return Node::null();
1051 : 70830 : }
1052 : :
1053 : 69871 : Node ExtendedRewriter::extendedRewriteEqRes(Kind andk,
1054 : : Kind ork,
1055 : : Kind eqk,
1056 : : Kind notk,
1057 : : std::map<Kind, bool>& bcp_kinds,
1058 : : Node n,
1059 : : bool isXor) const
1060 : : {
1061 [ + + ][ + - ]: 69871 : Assert(n.getKind() == andk || n.getKind() == ork);
[ - + ][ - + ]
[ - - ]
1062 [ + - ]: 69871 : Trace("ext-rew-eqres") << "Eq res: **** INPUT: " << n << std::endl;
1063 : :
1064 : 69871 : NodeManager* nm = d_nm;
1065 : 69871 : Kind nk = n.getKind();
1066 : 69871 : bool gpol = (nk == andk);
1067 [ + + ]: 231690 : for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++)
1068 : : {
1069 : 171609 : Node lit = n[i];
1070 [ + + ]: 171609 : if (lit.getKind() == eqk)
1071 : : {
1072 : : // eq is the equality we are basing a substitution on
1073 : 50100 : Node eq;
1074 [ + + ]: 50100 : if (gpol == isXor)
1075 : : {
1076 : : // can only turn disequality into equality if types are the same
1077 [ + + ]: 22413 : if (lit[1].getType() == lit.getType())
1078 : : {
1079 : : // t != s ---> ~t = s
1080 : 381 : if (lit[1].getKind() == notk && lit[0].getKind() != notk)
1081 : : {
1082 : 420 : eq = nm->mkNode(
1083 : 630 : Kind::EQUAL, lit[0], TermUtil::mkNegate(notk, lit[1]));
1084 : : }
1085 : : else
1086 : : {
1087 : 684 : eq = nm->mkNode(
1088 : 513 : Kind::EQUAL, TermUtil::mkNegate(notk, lit[0]), lit[1]);
1089 : : }
1090 : : }
1091 : : }
1092 : : else
1093 : : {
1094 : 27687 : eq = eqk == Kind::EQUAL ? lit : nm->mkNode(Kind::EQUAL, lit[0], lit[1]);
1095 : : }
1096 [ + + ]: 50100 : if (!eq.isNull())
1097 : : {
1098 : : // see if it corresponds to a substitution
1099 : 28068 : Subs subs;
1100 [ + + ]: 28068 : if (inferSubstitution(eq, subs))
1101 : : {
1102 [ - + ][ - + ]: 22122 : Assert(subs.size() == 1);
[ - - ]
1103 : 22122 : std::vector<Node> children;
1104 : 22122 : bool childrenChanged = false;
1105 : : // apply to all other children
1106 [ + + ]: 99154 : for (unsigned j = 0; j < nchild; j++)
1107 : : {
1108 : 77032 : Node ccs = n[j];
1109 [ + + ]: 77032 : 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 : 54910 : ccs = partialSubstitute(ccs, subs, bcp_kinds);
1115 [ + + ][ + + ]: 54910 : childrenChanged = childrenChanged || n[j] != ccs;
[ + + ][ - - ]
1116 : : }
1117 : 77032 : children.push_back(ccs);
1118 : 77032 : }
1119 [ + + ]: 22122 : if (childrenChanged)
1120 : : {
1121 : 9790 : return nm->mkNode(nk, children);
1122 : : }
1123 [ + + ]: 22122 : }
1124 [ + + ]: 28068 : }
1125 [ + + ]: 50100 : }
1126 [ + + ]: 171609 : }
1127 : :
1128 : 60081 : return Node::null();
1129 : : }
1130 : :
1131 : : /** sort pairs by their second (unsigned) argument */
1132 : 57555 : static bool sortPairSecond(const std::pair<Node, unsigned>& a,
1133 : : const std::pair<Node, unsigned>& b)
1134 : : {
1135 : 57555 : 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 : 113670 : void addTerm(Node c,
1174 : : std::vector<Node>& alist,
1175 : : std::vector<Node>& subsumes,
1176 : : unsigned index = 0,
1177 : : bool doAdd = true)
1178 : : {
1179 [ + + ]: 113670 : if (!d_data.isNull())
1180 : : {
1181 : 64 : subsumes.push_back(d_data);
1182 : : }
1183 [ + + ]: 113670 : if (doAdd)
1184 : : {
1185 [ + + ]: 113536 : if (index == alist.size())
1186 : : {
1187 : 55786 : d_data = c;
1188 : 55786 : return;
1189 : : }
1190 : : }
1191 : : // try all children where we have this atom
1192 [ + + ]: 86369 : for (std::pair<const Node, SimpSubsumeTrie>& cp : d_children)
1193 : : {
1194 [ + + ]: 28485 : 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 [ + + ]: 57884 : if (doAdd)
1200 : : {
1201 : 57750 : d_children[alist[index]].addTerm(c, alist, subsumes, index + 1, doAdd);
1202 : : }
1203 : : }
1204 : : };
1205 : :
1206 : 28715 : Node ExtendedRewriter::extendedRewriteEqChain(
1207 : : Kind eqk, Kind andk, Kind ork, Kind notk, Node ret, bool isXor) const
1208 : : {
1209 [ - + ][ - + ]: 28715 : 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 [ + + ]: 28715 : if (!d_aggr)
1214 : : {
1215 : 359 : return Node::null();
1216 : : }
1217 : :
1218 : 28356 : NodeManager* nm = d_nm;
1219 : :
1220 : 28356 : TypeNode tn = ret[0].getType();
1221 : :
1222 : : // sort/cancelling for Boolean EQUAL/XOR-chains
1223 [ + - ]: 28356 : Trace("ext-rew-eqchain") << "Eq-Chain : " << ret << std::endl;
1224 : :
1225 : : // get the children on either side
1226 : 28356 : bool gpol = true;
1227 : 28356 : std::vector<Node> children;
1228 [ + + ]: 85068 : for (unsigned r = 0, size = ret.getNumChildren(); r < size; r++)
1229 : : {
1230 : 56712 : Node curr = ret[r];
1231 : : // assume, if necessary, right associative
1232 : 57782 : while (curr.getKind() == eqk && curr[0].getType() == tn)
1233 : : {
1234 : 1070 : children.push_back(curr[0]);
1235 : 1070 : curr = curr[1];
1236 : : }
1237 : 56712 : children.push_back(curr);
1238 : 56712 : }
1239 : :
1240 : 28356 : std::map<Node, bool> cstatus;
1241 : : // add children to status
1242 [ + + ]: 86138 : for (const Node& c : children)
1243 : : {
1244 : 57782 : Node a = c;
1245 [ + + ]: 57782 : if (a.getKind() == notk)
1246 : : {
1247 : 2015 : gpol = !gpol;
1248 : 2015 : a = a[0];
1249 : : }
1250 [ + - ]: 57782 : Trace("ext-rew-eqchain") << "...child : " << a << std::endl;
1251 : 57782 : std::map<Node, bool>::iterator itc = cstatus.find(a);
1252 [ + + ]: 57782 : if (itc == cstatus.end())
1253 : : {
1254 : 57464 : cstatus[a] = true;
1255 : : }
1256 : : else
1257 : : {
1258 : : // cancels
1259 : 318 : cstatus.erase(a);
1260 [ - + ]: 318 : if (isXor)
1261 : : {
1262 : 0 : gpol = !gpol;
1263 : : }
1264 : : }
1265 : 57782 : }
1266 [ + - ]: 28356 : Trace("ext-rew-eqchain") << "Global polarity : " << gpol << std::endl;
1267 : :
1268 [ - + ]: 28356 : if (cstatus.empty())
1269 : : {
1270 : 0 : return TermUtil::mkTypeConst(ret.getType(), gpol);
1271 : : }
1272 : :
1273 : 28356 : children.clear();
1274 : :
1275 : : // compute the atoms of each child
1276 [ + - ]: 28356 : Trace("ext-rew-eqchain") << "eqchain-simplify: begin\n";
1277 [ + - ]: 28356 : Trace("ext-rew-eqchain") << " eqchain-simplify: get atoms...\n";
1278 : 28356 : std::map<Node, std::map<Node, bool> > atoms;
1279 : 28356 : std::map<Node, std::vector<Node> > alist;
1280 : 28356 : std::vector<std::pair<Node, unsigned> > atom_count;
1281 [ + + ]: 85502 : for (std::pair<const Node, bool>& cp : cstatus)
1282 : : {
1283 [ - + ]: 57146 : if (!cp.second)
1284 : : {
1285 : : // already eliminated
1286 : 0 : continue;
1287 : : }
1288 : 57146 : Node c = cp.first;
1289 : 57146 : Kind ck = c.getKind();
1290 [ + - ]: 57146 : Trace("ext-rew-eqchain") << " process c = " << c << std::endl;
1291 [ + + ][ + + ]: 57146 : if (ck == andk || ck == ork)
1292 : : {
1293 [ + + ]: 6143 : for (unsigned j = 0, nchild = c.getNumChildren(); j < nchild; j++)
1294 : : {
1295 : 4555 : Node cl = c[j];
1296 : 4555 : bool pol = cl.getKind() != notk;
1297 [ + + ]: 4555 : Node ca = pol ? cl : cl[0];
1298 [ + + ]: 4555 : bool newVal = (ck == andk ? !pol : pol);
1299 [ + - ]: 9110 : Trace("ext-rew-eqchain")
1300 : 4555 : << " atoms(" << c << ", " << ca << ") = " << newVal << std::endl;
1301 [ - + ][ - + ]: 4555 : Assert(atoms[c].find(ca) == atoms[c].end());
[ - - ]
1302 : : // polarity is flipped when we are AND
1303 : 4555 : atoms[c][ca] = newVal;
1304 : 4555 : 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 : 4555 : std::map<Node, bool>::iterator itc = cstatus.find(ca);
1311 [ + + ][ + - ]: 4555 : if (itc != cstatus.end() && itc->second)
[ + + ]
1312 : : {
1313 : : // cancel it
1314 : 680 : cstatus[ca] = false;
1315 : 680 : 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 : 680 : std::vector<Node> new_children;
1322 [ + + ]: 2080 : for (unsigned k = 0, nchildc = c.getNumChildren(); k < nchildc; k++)
1323 : : {
1324 [ + + ]: 1400 : if (j != k)
1325 : : {
1326 : 720 : new_children.push_back(c[k]);
1327 : : }
1328 : : }
1329 [ + + ]: 4080 : Node nc[2];
1330 : 680 : nc[0] = c[j];
1331 [ + + ]: 1360 : nc[1] = new_children.size() == 1 ? new_children[0]
1332 : 680 : : nm->mkNode(ck, new_children);
1333 : : // negate the proper child
1334 : 680 : unsigned nindex = (ck == andk) == pol ? 0 : 1;
1335 : 680 : nc[nindex] = TermUtil::mkNegate(notk, nc[nindex]);
1336 [ + + ]: 680 : Kind nk = pol ? ork : andk;
1337 : : // store as new child
1338 : 680 : children.push_back(nm->mkNode(nk, nc[0], nc[1]));
1339 [ - + ]: 680 : if (isXor)
1340 : : {
1341 : 0 : gpol = !gpol;
1342 : : }
1343 : 680 : break;
1344 [ + + ][ - - ]: 2720 : }
1345 [ + + ][ + + ]: 5235 : }
1346 : 2268 : }
1347 : : else
1348 : : {
1349 : 54878 : bool pol = ck != notk;
1350 [ + - ]: 54878 : Node ca = pol ? c : c[0];
1351 : 54878 : atoms[c][ca] = pol;
1352 [ + - ]: 109756 : Trace("ext-rew-eqchain")
1353 : 54878 : << " atoms(" << c << ", " << ca << ") = " << pol << std::endl;
1354 : 54878 : alist[c].push_back(ca);
1355 : 54878 : }
1356 : 57146 : atom_count.push_back(std::pair<Node, unsigned>(c, alist[c].size()));
1357 : 57146 : }
1358 : : // sort the atoms in each atom list
1359 : 28356 : for (std::map<Node, std::vector<Node> >::iterator it = alist.begin();
1360 [ + + ]: 85502 : it != alist.end();
1361 : 57146 : ++it)
1362 : : {
1363 : 57146 : std::sort(it->second.begin(), it->second.end());
1364 : : }
1365 : : // check subsumptions
1366 : : // sort by #atoms
1367 : 28356 : std::sort(atom_count.begin(), atom_count.end(), sortPairSecond);
1368 [ - + ]: 28356 : 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 : 28356 : SimpSubsumeTrie sst;
1378 [ + + ]: 85502 : for (std::pair<const Node, bool>& cp : cstatus)
1379 : : {
1380 [ + + ]: 57146 : if (!cp.second)
1381 : : {
1382 : : // already eliminated
1383 : 1360 : continue;
1384 : : }
1385 : 55786 : Node c = cp.first;
1386 : 55786 : std::map<Node, std::map<Node, bool> >::iterator itc = atoms.find(c);
1387 [ - + ][ - + ]: 55786 : Assert(itc != atoms.end());
[ - - ]
1388 [ + - ]: 111572 : Trace("ext-rew-eqchain") << " - add term " << c << " with atom list "
1389 : 55786 : << alist[c] << "...\n";
1390 : 55786 : std::vector<Node> subsumes;
1391 : 55786 : sst.addTerm(c, alist[c], subsumes);
1392 [ + + ]: 55786 : 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") << " eqchain-simplify: " << c << " subsumes "
1400 : 20 : << 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") << " eqchain-simplify: atom " << a
1414 : 0 : << " has polarities : " << polc << " " << polcc
1415 : 44 : << "\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 : 55786 : }
1527 [ + - ]: 28356 : Trace("ext-rew-eqchain") << "eqchain-simplify: finish" << std::endl;
1528 : :
1529 : : // sorted right associative chain
1530 : 28356 : bool has_nvar = false;
1531 : 28356 : unsigned nvar_index = 0;
1532 [ + + ]: 85502 : for (std::pair<const Node, bool>& cp : cstatus)
1533 : : {
1534 [ + + ]: 57146 : if (cp.second)
1535 : : {
1536 [ + + ]: 55746 : if (!cp.first.isVar())
1537 : : {
1538 : 38633 : has_nvar = true;
1539 : 38633 : nvar_index = children.size();
1540 : : }
1541 : 55746 : children.push_back(cp.first);
1542 : : }
1543 : : }
1544 : 28356 : std::sort(children.begin(), children.end());
1545 : :
1546 : 28356 : Node new_ret;
1547 [ + + ]: 28356 : if (!gpol)
1548 : : {
1549 : : // negate the constant child if it exists
1550 [ + + ]: 1777 : unsigned nindex = has_nvar ? nvar_index : 0;
1551 : 1777 : children[nindex] = TermUtil::mkNegate(notk, children[nindex]);
1552 : : }
1553 : 28356 : new_ret = children.back();
1554 : 28356 : unsigned index = children.size() - 1;
1555 [ + + ]: 56458 : while (index > 0)
1556 : : {
1557 : 28102 : index--;
1558 : 28102 : new_ret = nm->mkNode(eqk, children[index], new_ret);
1559 : : }
1560 : 28356 : new_ret = d_rew.rewrite(new_ret);
1561 [ + + ]: 28356 : if (new_ret != ret)
1562 : : {
1563 : 2043 : return new_ret;
1564 : : }
1565 : 26313 : return Node::null();
1566 : 28356 : }
1567 : :
1568 : 518424 : Node ExtendedRewriter::partialSubstitute(
1569 : : Node n,
1570 : : const std::map<Node, Node>& assign,
1571 : : const std::map<Kind, bool>& rkinds) const
1572 : : {
1573 : 518424 : std::unordered_map<TNode, Node> visited;
1574 : 518424 : std::unordered_map<TNode, Node>::iterator it;
1575 : 518424 : std::map<Node, Node>::const_iterator ita;
1576 : 518424 : std::vector<TNode> visit;
1577 : 518424 : TNode cur;
1578 : 518424 : visit.push_back(n);
1579 : : do
1580 : : {
1581 : 6316701 : cur = visit.back();
1582 : 6316701 : visit.pop_back();
1583 : 6316701 : it = visited.find(cur);
1584 : :
1585 [ + + ]: 6316701 : if (it == visited.end())
1586 : : {
1587 : 2645829 : ita = assign.find(cur);
1588 [ + + ]: 2645829 : if (ita != assign.end())
1589 : : {
1590 : 26665 : 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 : 2619164 : Kind k = cur.getKind();
1599 : 5238328 : if (k != Kind::WITNESS
1600 [ + - ][ - + ]: 2619164 : && (rkinds.empty() || rkinds.find(k) != rkinds.end()))
[ - - ][ + - ]
1601 : : {
1602 : 2619164 : visited[cur] = Node::null();
1603 : 2619164 : visit.push_back(cur);
1604 [ + + ]: 5798277 : for (const Node& cn : cur)
1605 : : {
1606 : 3179113 : visit.push_back(cn);
1607 : 3179113 : }
1608 : : }
1609 : : else
1610 : : {
1611 : 0 : visited[cur] = cur;
1612 : : }
1613 : : }
1614 : : }
1615 [ + + ]: 3670872 : else if (it->second.isNull())
1616 : : {
1617 : 2619164 : Node ret = cur;
1618 : 2619164 : bool childChanged = false;
1619 : 2619164 : std::vector<Node> children;
1620 [ + + ]: 2619164 : if (cur.getMetaKind() == metakind::PARAMETERIZED)
1621 : : {
1622 : 15402 : children.push_back(cur.getOperator());
1623 : : }
1624 [ + + ]: 5798277 : for (const Node& cn : cur)
1625 : : {
1626 : 3179113 : it = visited.find(cn);
1627 [ - + ][ - + ]: 3179113 : Assert(it != visited.end());
[ - - ]
1628 [ - + ][ - + ]: 3179113 : Assert(!it->second.isNull());
[ - - ]
1629 [ + + ][ + + ]: 3179113 : childChanged = childChanged || cn != it->second;
1630 : 3179113 : children.push_back(it->second);
1631 : 3179113 : }
1632 [ + + ]: 2619164 : if (childChanged)
1633 : : {
1634 : 91040 : ret = d_nm->mkNode(cur.getKind(), children);
1635 : : }
1636 : 2619164 : visited[cur] = ret;
1637 : 2619164 : }
1638 [ + + ]: 6316701 : } while (!visit.empty());
1639 [ - + ][ - + ]: 518424 : Assert(visited.find(n) != visited.end());
[ - - ]
1640 [ - + ][ - + ]: 518424 : Assert(!visited.find(n)->second.isNull());
[ - - ]
1641 : 1036848 : return visited[n];
1642 : 518424 : }
1643 : :
1644 : 83743 : Node ExtendedRewriter::partialSubstitute(
1645 : : Node n, const Subs& subs, const std::map<Kind, bool>& rkinds) const
1646 : : {
1647 : 83743 : std::map<Node, Node> assign;
1648 [ + + ]: 181328 : for (size_t i = 0, nvars = subs.size(); i < nvars; i++)
1649 : : {
1650 : 97585 : assign[subs.d_vars[i]] = subs.d_subs[i];
1651 : : }
1652 : 167486 : return partialSubstitute(n, assign, rkinds);
1653 : 83743 : }
1654 : :
1655 : 40871 : Node ExtendedRewriter::solveEquality(Node n) const
1656 : : {
1657 : : // TODO (#1706) : implement
1658 [ - + ][ - + ]: 40871 : Assert(n.getKind() == Kind::EQUAL);
[ - - ]
1659 : :
1660 : 40871 : return Node::null();
1661 : : }
1662 : :
1663 : 75603 : bool ExtendedRewriter::inferSubstitution(Node n, Subs& subs, bool usePred) const
1664 : : {
1665 [ + + ]: 75603 : if (n.getKind() == Kind::AND)
1666 : : {
1667 : 4860 : bool ret = false;
1668 [ + + ]: 23562 : for (const Node& nc : n)
1669 : : {
1670 : 18702 : bool cret = inferSubstitution(nc, subs, usePred);
1671 [ + + ][ + - ]: 18702 : ret = ret || cret;
1672 : 18702 : }
1673 : 4860 : return ret;
1674 : : }
1675 [ + + ]: 70743 : if (n.getKind() == Kind::EQUAL)
1676 : : {
1677 : : // see if it can be put into form x = y
1678 : 40871 : Node slv_eq = solveEquality(n);
1679 [ - + ]: 40871 : if (!slv_eq.isNull())
1680 : : {
1681 : 0 : n = slv_eq;
1682 : : }
1683 [ + + ]: 245226 : Node v[2];
1684 [ + + ]: 85884 : for (unsigned i = 0; i < 2; i++)
1685 : : {
1686 [ + + ]: 76419 : if (n[i].isConst())
1687 : : {
1688 : 31406 : subs.add(n[1 - i], n[i]);
1689 : 31406 : return true;
1690 : : }
1691 [ + + ]: 45013 : if (n[i].isVar())
1692 : : {
1693 : 29773 : v[i] = n[i];
1694 : : }
1695 : 15240 : else if (TermUtil::isNegate(n[i].getKind()) && n[i][0].isVar())
1696 : : {
1697 : 300 : v[i] = n[i][0];
1698 : : }
1699 : : }
1700 [ + + ]: 23131 : for (unsigned i = 0; i < 2; i++)
1701 : : {
1702 : 16443 : TNode r1 = v[i];
1703 : 16443 : Node r2 = v[1 - i];
1704 [ + + ][ + + ]: 16443 : if (r1.isVar() && ((r2.isVar() && r1 < r2) || r2.isConst()))
[ + + ][ - + ]
[ + + ]
1705 : : {
1706 : 2777 : r2 = n[1 - i];
1707 [ + + ]: 2777 : if (v[i] != n[i])
1708 : : {
1709 [ - + ][ - + ]: 212 : Assert(TermUtil::isNegate(n[i].getKind()));
[ - - ]
1710 : 212 : r2 = TermUtil::mkNegate(n[i].getKind(), r2);
1711 : : }
1712 [ + - ]: 2777 : if (!subs.contains(r1))
1713 : : {
1714 : 2777 : subs.add(r1, r2);
1715 : 2777 : return true;
1716 : : }
1717 : : }
1718 [ + + ][ + + ]: 19220 : }
1719 [ + + ][ + + ]: 163484 : }
[ - - ]
1720 [ + + ]: 36560 : if (usePred)
1721 : : {
1722 : 30614 : bool negated = n.getKind() == Kind::NOT;
1723 [ + + ]: 30614 : Node var = negated ? n[0] : n;
1724 : 30614 : Node s = d_nm->mkConst(!negated);
1725 : 30614 : subs.add(var, s);
1726 : 30614 : return true;
1727 : 30614 : }
1728 : 5946 : return false;
1729 : : }
1730 : :
1731 : 18582 : Node ExtendedRewriter::extendedRewriteStrings(const Node& node) const
1732 : : {
1733 [ + - ]: 37164 : Trace("q-ext-rewrite-debug")
1734 : 18582 : << "Extended rewrite strings : " << node << std::endl;
1735 : :
1736 : : // allow recursive approximations
1737 : 18582 : strings::ArithEntail ae(d_nm, &d_rew, true);
1738 : 18582 : strings::StringsEntail se(&d_rew, ae);
1739 : 18582 : strings::SequencesRewriter sr(d_nm, ae, se, nullptr);
1740 : :
1741 : 18582 : Kind k = node.getKind();
1742 [ + + ]: 18582 : 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 : 3713 : Node ret = sr.rewriteEqualityExt(node);
1748 [ + + ]: 3713 : if (ret != node)
1749 : : {
1750 : 328 : debugExtendedRewrite(node, ret, "STR_EXT_EQ_REWRITE");
1751 : 328 : return ret;
1752 : : }
1753 : :
1754 : : // ------- length entailment
1755 : 6770 : Node len0 = d_nm->mkNode(Kind::STRING_LENGTH, node[0]);
1756 : 6770 : Node len1 = d_nm->mkNode(Kind::STRING_LENGTH, node[1]);
1757 : 3385 : Node len_eq = len0.eqNode(len1);
1758 : 3385 : len_eq = d_rew.rewrite(len_eq);
1759 [ - + ]: 3385 : if (len_eq == d_false)
1760 : : {
1761 : 0 : debugExtendedRewrite(node, d_false, "String EQUAL len entailment");
1762 : 0 : return d_false;
1763 : : }
1764 : :
1765 : 3385 : TypeNode stype = node[0].getType();
1766 [ + + ]: 20310 : std::vector<Node> c[2];
1767 [ + + ]: 10155 : for (unsigned i = 0; i < 2; i++)
1768 : : {
1769 : 6770 : strings::utils::getConcat(node[i], c[i]);
1770 : : }
1771 : :
1772 : : // ------- homogeneous constants
1773 [ + + ]: 10154 : for (unsigned i = 0; i < 2; i++)
1774 : : {
1775 : 6770 : Node cn = se.checkHomogeneousString(node[i]);
1776 [ + + ][ + + ]: 6770 : if (!cn.isNull() && !strings::Word::isEmpty(cn))
[ + + ][ + + ]
[ - - ]
1777 : : {
1778 [ - + ][ - + ]: 1531 : Assert(cn.isConst());
[ - - ]
1779 [ - + ][ - + ]: 1531 : Assert(strings::Word::getLength(cn) == 1);
[ - - ]
1780 : :
1781 : : // The operands of the concat on each side of the equality without
1782 : : // constant strings
1783 [ + + ]: 9186 : std::vector<Node> trimmed[2];
1784 : : // Counts the number of `cn`s on each side
1785 : 1531 : size_t numCns[2] = {0, 0};
1786 [ + + ]: 4593 : 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 : 3062 : std::sort(c[j].begin(), c[j].end());
1792 [ + + ]: 6139 : for (const Node& cc : c[j])
1793 : : {
1794 [ + + ]: 3077 : 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 : 1500 : std::vector<Node> veccc = strings::Word::getChars(cc);
1799 [ + + ]: 3429 : for (const Node& cv : veccc)
1800 : : {
1801 [ - + ]: 1929 : 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 : 1929 : numCns[j]++;
1810 : : }
1811 [ + - ]: 1500 : }
1812 : : else
1813 : : {
1814 : 1577 : 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 : 1531 : size_t trimmedConst = std::min(numCns[0], numCns[1]);
1822 [ + + ]: 4593 : for (size_t j = 0; j < 2; j++)
1823 : : {
1824 : 3062 : size_t diff = numCns[j] - trimmedConst;
1825 [ + + ]: 3062 : 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 : 1495 : std::vector<Node> vec(diff, cn);
1830 : 1495 : trimmed[j].push_back(strings::Word::mkWordFlatten(vec));
1831 : 1495 : }
1832 : : }
1833 : :
1834 : 1531 : Node lhs = strings::utils::mkConcat(trimmed[i], stype);
1835 : 1531 : Node ss = strings::utils::mkConcat(trimmed[1 - i], stype);
1836 : 1531 : 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 [ + + ][ + + ]: 6125 : }
[ + + ][ - - ]
1850 [ + + ]: 6770 : }
1851 [ + + ][ + + ]: 13872 : }
[ + + ][ + + ]
[ + + ][ + + ]
[ - - ]
1852 [ + + ]: 14869 : 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 : 613 : std::vector<Node> vec(node.begin(), node.end());
1860 : 613 : size_t lastIdx = 0;
1861 : 613 : Node lastX;
1862 [ + + ]: 1965 : for (size_t i = 0, nsize = vec.size(); i < nsize; i++)
1863 : : {
1864 : 1352 : Node s = se.getStringOrEmpty(vec[i]);
1865 : 1352 : bool nextX = false;
1866 [ + + ]: 1352 : if (s != lastX)
1867 : : {
1868 : 1313 : nextX = true;
1869 : : }
1870 [ + + ]: 1352 : if (nextX)
1871 : : {
1872 : 1313 : std::sort(vec.begin() + lastIdx, vec.begin() + i);
1873 : 1313 : lastX = s;
1874 : 1313 : lastIdx = i;
1875 : : }
1876 : 1352 : }
1877 : 613 : std::sort(vec.begin() + lastIdx, vec.end());
1878 : 613 : TypeNode tn = node.getType();
1879 : 613 : Node retNode = strings::utils::mkConcat(vec, tn);
1880 [ + + ]: 613 : if (retNode != node)
1881 : : {
1882 : 6 : debugExtendedRewrite(node, retNode, "CONCAT_NORM_SORT");
1883 : 6 : return retNode;
1884 : : }
1885 [ + + ][ + + ]: 631 : }
[ + + ][ + + ]
1886 [ + + ]: 14256 : else if (k == Kind::STRING_SUBSTR)
1887 : : {
1888 : 2338 : NodeManager* nm = d_nm;
1889 : 4676 : 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 : 4676 : Node n1_lt_tot_len = d_rew.rewrite(nm->mkNode(Kind::LT, node[1], tot_len));
1892 [ + + ]: 2338 : 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 : 4672 : Node non_zero_len = d_rew.rewrite(nm->mkNode(Kind::LT, d_intZero, node[2]));
1901 [ + + ]: 2336 : 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 : 4666 : d_rew.rewrite(nm->mkNode(Kind::GEQ, node[1], d_intZero));
1910 [ + + ]: 2333 : 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 [ + + ][ + + ]: 2349 : }
[ + + ][ + + ]
1917 [ + + ]: 11918 : 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 : 3 : Node rn1 = d_rew.rewrite(
1928 : 6 : d_rew.rewriteEqualityExt(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) = strings::utils::collectEmptyEqs(rn1);
1934 : :
1935 [ + + ]: 3 : if (allEmptyEqs)
1936 : : {
1937 : 2 : Node nn1 = strings::utils::mkConcat(emptyNodes, stype);
1938 [ + + ]: 2 : if (node[1] != nn1)
1939 : : {
1940 : 2 : Node ret = d_nm->mkNode(Kind::STRING_REPLACE, node[0], nn1, node[2]);
1941 : 1 : debugExtendedRewrite(node, ret, "RPL_X_Y_X_SIMP");
1942 : 1 : return ret;
1943 : 1 : }
1944 [ + + ]: 2 : }
1945 [ + + ]: 3 : }
1946 [ + + ][ + + ]: 5 : }
[ + + ]
1947 : : }
1948 : 304 : Node cmp_con = d_nm->mkNode(Kind::STRING_CONTAINS, node[0], node[1]);
1949 : : // note we make a full recursive call to extended rewrite here, which should
1950 : : // be fine since the term we are rewriting is simpler than the current one.
1951 : 152 : Node cmp_conr = extendedRewrite(cmp_con);
1952 [ + + ][ + + ]: 152 : if (cmp_conr.getKind() == Kind::EQUAL || cmp_conr.getKind() == Kind::AND)
[ + + ]
1953 : : {
1954 : 19 : TypeNode stype = node.getType();
1955 : : // Rewriting the str.contains may return equalities of the form (= x "").
1956 : : // In that case, we can substitute the variables appearing in those
1957 : : // equalities with the empty string in the third argument of the
1958 : : // str.replace. For example:
1959 : : //
1960 : : // (str.replace x (str.++ x y) y) --> (str.replace x (str.++ x y) "")
1961 : : //
1962 : : // This can be done because str.replace changes x iff (str.++ x y) is in x
1963 : : // but that means that y must be empty in that case. Thus, we can
1964 : : // substitute y with "" in the third argument. Note that the third argument
1965 : : // does not matter when the str.replace does not apply.
1966 : : //
1967 : 19 : Node empty = strings::Word::mkEmptyWord(stype);
1968 : 19 : std::vector<Node> emptyNodes;
1969 : : bool allEmptyEqs;
1970 : 19 : std::tie(allEmptyEqs, emptyNodes) = strings::utils::collectEmptyEqs(cmp_conr);
1971 [ + + ]: 19 : if (emptyNodes.size() > 0)
1972 : : {
1973 : : // Perform the substitutions
1974 : 36 : std::vector<TNode> substs(emptyNodes.size(), TNode(empty));
1975 : : Node nn2 = node[2].substitute(
1976 : 18 : emptyNodes.begin(), emptyNodes.end(), substs.begin(), substs.end());
1977 : :
1978 : : // If the contains rewrites to a conjunction of empty-string equalities
1979 : : // and we are doing the replacement in an empty string, we can rewrite
1980 : : // the string-to-replace with a concatenation of all the terms that must
1981 : : // be empty:
1982 : : //
1983 : : // (str.replace "" y z) ---> (str.replace "" (str.++ y1 ... yn) z)
1984 : : // if (str.contains "" y) ---> (and (= y1 "") ... (= yn ""))
1985 [ + + ][ + + ]: 18 : if (node[0] == empty && allEmptyEqs)
[ + - ][ + + ]
[ - - ]
1986 : : {
1987 : 12 : std::vector<Node> emptyNodesList(emptyNodes.begin(), emptyNodes.end());
1988 : 12 : Node nn1 = strings::utils::mkConcat(emptyNodesList, stype);
1989 : 12 : if (nn1 != node[1] || nn2 != node[2])
1990 : : {
1991 : 8 : Node res = d_nm->mkNode(Kind::STRING_REPLACE, node[0], nn1, nn2);
1992 : 4 : debugExtendedRewrite(node, res, "RPL_EMP_CNTS_SUBSTS");
1993 : 4 : return res;
1994 : 4 : }
1995 [ + + ][ + + ]: 16 : }
1996 : :
1997 [ + + ]: 14 : if (nn2 != node[2])
1998 : : {
1999 : 8 : Node res = d_nm->mkNode(Kind::STRING_REPLACE, node[0], node[1], nn2);
2000 : 4 : debugExtendedRewrite(node, res, "RPL_CNTS_SUBSTS");
2001 : 4 : return res;
2002 : 4 : }
2003 [ + + ][ + + ]: 26 : }
2004 [ + + ][ + + ]: 35 : }
[ + + ]
2005 [ + + ][ + + ]: 160 : }
2006 [ + + ]: 11765 : else if (k == Kind::STRING_CONTAINS)
2007 : : {
2008 [ + + ]: 5104 : if (node[0].getKind() == Kind::STRING_REPLACE)
2009 : : {
2010 : 12 : TypeNode stype = node[0].getType();
2011 : 12 : Node empty = strings::Word::mkEmptyWord(stype);
2012 : 12 : if (node[1].isConst() && node[0][1].isConst() && node[0][2].isConst())
2013 : : {
2014 : 12 : if (node[1] != empty && node[0][1] != empty && node[0][2] != empty
2015 : 10 : && !strings::Word::hasBidirectionalOverlap(node[1], node[0][1])
2016 : 12 : && !strings::Word::hasBidirectionalOverlap(node[1], node[0][2]))
2017 : : {
2018 : : // (str.contains (str.replace x c1 c2) c3) ---> (str.contains x c3)
2019 : : // if there is no overlap between c1 and c3 and none between c2 and c3
2020 : 2 : Node ret = d_nm->mkNode(Kind::STRING_CONTAINS, node[0][0], node[1]);
2021 : 1 : debugExtendedRewrite(node, ret, "CTN_REPL_CNSTS_TO_CTN");
2022 : 1 : return ret;
2023 : 1 : }
2024 : : }
2025 : : // (str.contains (str.replace x y z) w) --->
2026 : : // (str.contains (str.replace x y "") w)
2027 : : // if (str.contains z w) ---> false and (str.len w) = 1
2028 [ + + ]: 11 : if (se.checkLengthOne(node[1]))
2029 : : {
2030 : 16 : Node ctn = se.checkContains(node[0][2], node[1]);
2031 [ + + ][ + - ]: 8 : if (!ctn.isNull() && !ctn.getConst<bool>())
[ + + ]
2032 : : {
2033 : : Node ret = d_nm->mkNode(
2034 : : Kind::STRING_CONTAINS,
2035 : 8 : d_nm->mkNode(Kind::STRING_REPLACE, node[0][0], node[0][1], empty),
2036 : 16 : node[1]);
2037 : 4 : debugExtendedRewrite(node, ret, "CTN_REPL_SIMP_REPL");
2038 : 4 : return ret;
2039 : 4 : }
2040 [ + + ]: 8 : }
2041 [ + + ][ + + ]: 17 : }
2042 : 5099 : std::vector<Node> nc1;
2043 : 5099 : strings::utils::getConcat(node[0], nc1);
2044 : 5099 : std::vector<Node> nc2;
2045 : 5099 : strings::utils::getConcat(node[1], nc2);
2046 : :
2047 : : // extended component-wise containment
2048 : 5099 : std::vector<Node> nc1rb;
2049 : 5099 : std::vector<Node> nc1re;
2050 [ + + ]: 5099 : if (se.componentContainsExt(nc1, nc2, nc1rb, nc1re) != -1)
2051 : : {
2052 : 14 : debugExtendedRewrite(node, d_true, "CTN_COMPONENT_EXT");
2053 : 14 : return d_true;
2054 : : }
2055 : :
2056 [ + + ]: 10174 : for (const Node& n : nc2)
2057 : : {
2058 : : // (str.contains x (str.++ w (str.replace x y x) z)) --->
2059 : : // (= x (str.++ w (str.replace x y x) z))
2060 : : //
2061 : 5092 : if (n.getKind() == Kind::STRING_REPLACE && node[0] == n[0]
2062 : 5092 : && node[0] == n[2])
2063 : : {
2064 : 0 : Node ret = d_nm->mkNode(Kind::EQUAL, node[0], node[1]);
2065 : 0 : debugExtendedRewrite(node, ret, "CTN_REPL_SELF");
2066 : 0 : return ret;
2067 : 0 : }
2068 : : }
2069 [ + + ][ + + ]: 5141 : }
[ + + ][ + + ]
2070 : : // otherwise, the use of recursive approximations and rewriting via
2071 : : // the entailment utilities may make a standard conditional rewrite
2072 : : // applicable.
2073 : 18213 : RewriteResponse rr = sr.postRewrite(node);
2074 [ + + ]: 18213 : if (rr.d_node != node)
2075 : : {
2076 : 13 : return rr.d_node;
2077 : : }
2078 : :
2079 : 18200 : return Node::null();
2080 : 18582 : }
2081 : :
2082 : 330 : Node ExtendedRewriter::extendedRewriteSets(const Node& node) const
2083 : : {
2084 [ + + ][ + + ]: 355 : if (node.getKind() == Kind::SET_MINUS && node[1].getKind() == Kind::SET_MINUS
[ - - ]
2085 : 355 : && node[1][0] == node[0])
2086 : : {
2087 : : // Note this cannot be a rewrite rule or a ppRewrite, since it impacts the
2088 : : // cardinality graph. In particular, if we internally inspect (set.minus A
2089 : : // (setminus A B)), for instance if we are splitting the Venn regions of A
2090 : : // and (set.minus A B), then we should not transform this to an intersection
2091 : : // term. (set.minus A (set.minus A B)) = (set.inter A B)
2092 : 3 : NodeManager* nm = d_nm;
2093 : 6 : Node ret = nm->mkNode(Kind::SET_INTER, node[0], node[1][1]);
2094 : 3 : debugExtendedRewrite(node, ret, "SET_MINUS_MINUS");
2095 : 3 : return ret;
2096 : 3 : }
2097 : 327 : return Node::null();
2098 : : }
2099 : :
2100 : 116315 : void ExtendedRewriter::debugExtendedRewrite(Node n,
2101 : : Node ret,
2102 : : const char* c) const
2103 : : {
2104 : 232630 : Assert(ret.isNull() || n.getType().isComparableTo(ret.getType()))
2105 [ - + ][ - + ]: 116315 : << "Extended rewrite does not preserve type: " << n << " --> " << ret;
[ - - ]
2106 [ - + ]: 116315 : if (TraceIsOn("q-ext-rewrite"))
2107 : : {
2108 [ - - ]: 0 : if (!ret.isNull())
2109 : : {
2110 [ - - ]: 0 : Trace("q-ext-rewrite-apply") << "sygus-extr : apply " << c << std::endl;
2111 [ - - ]: 0 : Trace("q-ext-rewrite") << "sygus-extr : " << c << " : " << n
2112 : 0 : << " rewrites to " << ret << std::endl;
2113 : : }
2114 : : }
2115 : 116315 : }
2116 : :
2117 : : } // namespace quantifiers
2118 : : } // namespace theory
2119 : : } // namespace cvc5::internal
|
