Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Andres Noetzli, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Implementation of arithmetic entailment computation for string terms.
14 : : */
15 : :
16 : : #include "theory/strings/arith_entail.h"
17 : :
18 : : #include "expr/attribute.h"
19 : : #include "expr/node_algorithm.h"
20 : : #include "proof/conv_proof_generator.h"
21 : : #include "theory/arith/arith_msum.h"
22 : : #include "theory/arith/arith_poly_norm.h"
23 : : #include "theory/arith/arith_subs.h"
24 : : #include "theory/rewriter.h"
25 : : #include "theory/strings/theory_strings_utils.h"
26 : : #include "theory/strings/word.h"
27 : : #include "theory/theory.h"
28 : : #include "util/rational.h"
29 : :
30 : : using namespace cvc5::internal::kind;
31 : :
32 : : namespace cvc5::internal {
33 : : namespace theory {
34 : : namespace strings {
35 : :
36 : 320145 : ArithEntail::ArithEntail(Rewriter* r) : d_rr(r)
37 : : {
38 : 320145 : d_one = NodeManager::currentNM()->mkConstInt(Rational(1));
39 : 320145 : d_zero = NodeManager::currentNM()->mkConstInt(Rational(0));
40 : 320145 : }
41 : :
42 : 103127 : Node ArithEntail::rewritePredViaEntailment(const Node& n, bool isSimple)
43 : : {
44 : 206254 : Node exp;
45 : 206254 : return rewritePredViaEntailment(n, exp, isSimple);
46 : : }
47 : :
48 : 104480 : Node ArithEntail::rewritePredViaEntailment(const Node& n,
49 : : Node& exp,
50 : : bool isSimple)
51 : : {
52 : 104480 : NodeManager* nm = NodeManager::currentNM();
53 : 104480 : if (n.getKind() == Kind::EQUAL && n[0].getType().isInteger())
54 : : {
55 : 40095 : exp = nm->mkNode(Kind::SUB, nm->mkNode(Kind::SUB, n[0], n[1]), d_one);
56 [ + + ]: 40095 : if (!findApprox(rewriteArith(exp), isSimple).isNull())
57 : : {
58 : 3988 : return nm->mkConst(false);
59 : : }
60 : 38101 : exp = nm->mkNode(Kind::SUB, nm->mkNode(Kind::SUB, n[1], n[0]), d_one);
61 [ + + ]: 38101 : if (!findApprox(rewriteArith(exp), isSimple).isNull())
62 : : {
63 : 2264 : return nm->mkConst(false);
64 : : }
65 : 36969 : exp = Node::null();
66 [ + + ]: 36969 : if (checkEq(n[0], n[1]))
67 : : {
68 : : // explanation is null
69 : 5392 : return nm->mkConst(true);
70 : : }
71 : : }
72 [ + - ]: 64385 : else if (n.getKind() == Kind::GEQ)
73 : : {
74 : 64385 : exp = nm->mkNode(Kind::SUB, n[0], n[1]);
75 [ + + ]: 64385 : if (!findApprox(rewriteArith(exp), isSimple).isNull())
76 : : {
77 : 2998 : return nm->mkConst(true);
78 : : }
79 : 62886 : exp = nm->mkNode(Kind::SUB, nm->mkNode(Kind::SUB, n[1], n[0]), d_one);
80 [ + + ]: 62886 : if (!findApprox(rewriteArith(exp), isSimple).isNull())
81 : : {
82 : 13026 : return nm->mkConst(false);
83 : : }
84 : 56373 : exp = Node::null();
85 : : }
86 : 90646 : return Node::null();
87 : : }
88 : :
89 : 2547010 : Node ArithEntail::rewriteArith(Node a)
90 : : {
91 [ - + ][ - - ]: 5094030 : AlwaysAssert(a.getType().isInteger())
92 : 2547010 : << "Bad term: " << a << " " << a.getType();
93 [ + + ]: 2547010 : if (d_rr != nullptr)
94 : : {
95 : 2121300 : return d_rr->rewrite(a);
96 : : }
97 : : // Otherwise, use the poly norm utility. This is important since the rewrite
98 : : // must be justified by ARITH_POLY_NORM when in proof mode (when d_rr is
99 : : // null).
100 : 851438 : Node an = arith::PolyNorm::getPolyNorm(a);
101 : 425719 : return an;
102 : : }
103 : :
104 : 51003 : Node ArithEntail::normalizeGeq(const Node& n) const
105 : : {
106 : 51003 : NodeManager* nm = NodeManager::currentNM();
107 : 97834 : if (n.getNumChildren() != 2 || !n[0].getType().isInteger()
108 : 97834 : || !n[1].getType().isInteger())
109 : : {
110 : 4228 : return Node::null();
111 : : }
112 [ + + ][ + + ]: 46775 : switch (n.getKind())
[ + ]
113 : : {
114 : 16281 : case Kind::GEQ: return n;
115 : 11156 : case Kind::LEQ: return nm->mkNode(Kind::GEQ, n[1], n[0]);
116 : 4324 : case Kind::LT:
117 : : return nm->mkNode(
118 : : Kind::GEQ,
119 : : n[1],
120 : 4324 : nm->mkNode(Kind::ADD, n[0], nm->mkConstInt(Rational(1))));
121 : 6106 : case Kind::GT:
122 : : return nm->mkNode(
123 : : Kind::GEQ,
124 : : n[0],
125 : 6106 : nm->mkNode(Kind::ADD, n[1], nm->mkConstInt(Rational(1))));
126 : 8908 : default: break;
127 : : }
128 : 8908 : return Node::null();
129 : : }
130 : :
131 : 55670 : Node ArithEntail::rewriteLengthIntro(const Node& n,
132 : : TConvProofGenerator* pg) const
133 : : {
134 : 55670 : NodeManager* nm = NodeManager::currentNM();
135 : 111340 : std::unordered_map<TNode, Node> visited;
136 : 55670 : std::unordered_map<TNode, Node>::iterator it;
137 : 111340 : std::vector<TNode> visit;
138 : 55670 : TNode cur;
139 : 55670 : visit.push_back(n);
140 : 1025140 : do
141 : : {
142 : 1080810 : cur = visit.back();
143 : 1080810 : it = visited.find(cur);
144 [ + + ]: 1080810 : if (it == visited.end())
145 : : {
146 [ + + ]: 580678 : if (cur.getNumChildren() == 0)
147 : : {
148 : 221389 : visit.pop_back();
149 : 221389 : visited[cur] = cur;
150 : 221389 : continue;
151 : : }
152 : 359289 : visited.emplace(cur, Node::null());
153 : 359289 : visit.insert(visit.end(), cur.begin(), cur.end());
154 : 359289 : continue;
155 : : }
156 : 500132 : visit.pop_back();
157 [ + + ]: 500132 : if (it->second.isNull())
158 : : {
159 : 359289 : Kind k = cur.getKind();
160 : 359289 : bool childChanged = false;
161 : 718578 : std::vector<Node> children;
162 [ + + ]: 1025140 : for (const Node& cn : cur)
163 : : {
164 : 665851 : it = visited.find(cn);
165 [ - + ][ - + ]: 665851 : Assert(it != visited.end());
[ - - ]
166 [ - + ][ - + ]: 665851 : Assert(!it->second.isNull());
[ - - ]
167 : 665851 : children.push_back(it->second);
168 [ + + ][ + + ]: 665851 : childChanged = childChanged || it->second != cn;
169 : : }
170 : 718578 : Node ret = cur;
171 [ + + ]: 359289 : if (childChanged)
172 : : {
173 : 38078 : ret = nm->mkNode(k, children);
174 : : }
175 [ + + ]: 359289 : if (k == Kind::STRING_LENGTH)
176 : : {
177 : 205380 : std::vector<Node> cc;
178 [ + + ]: 205380 : for (const Node& c : children)
179 : : {
180 : 102690 : utils::getConcat(c, cc);
181 : : }
182 : 205380 : std::vector<Node> sum;
183 [ + + ]: 242962 : for (const Node& c : cc)
184 : : {
185 [ + + ][ + + ]: 140272 : if (c.isConst() && c.getType().isString())
[ + + ][ + + ]
[ - - ]
186 : : {
187 : 42020 : sum.push_back(nm->mkConstInt(Rational(Word::getLength(c))));
188 : : }
189 : : else
190 : : {
191 : 98252 : sum.push_back(nm->mkNode(Kind::STRING_LENGTH, c));
192 : : }
193 : : }
194 [ - + ][ - + ]: 102690 : Assert(!sum.empty());
[ - - ]
195 [ + + ]: 205380 : Node rret = sum.size() == 1 ? sum[0] : nm->mkNode(Kind::ADD, sum);
196 [ + + ]: 102690 : if (pg != nullptr)
197 : : {
198 : 3468 : pg->addRewriteStep(ret,
199 : : rret,
200 : : nullptr,
201 : : false,
202 : : TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE);
203 : : }
204 : 102690 : ret = rret;
205 : : }
206 : 359289 : visited[cur] = ret;
207 : : }
208 [ + + ]: 1080810 : } while (!visit.empty());
209 [ - + ][ - + ]: 55670 : Assert(visited.find(n) != visited.end());
[ - - ]
210 [ - + ][ - + ]: 55670 : Assert(!visited.find(n)->second.isNull());
[ - - ]
211 : 111340 : return visited[n];
212 : : }
213 : :
214 : 45802 : bool ArithEntail::checkEq(Node a, Node b)
215 : : {
216 [ + + ]: 45802 : if (a == b)
217 : : {
218 : 3396 : return true;
219 : : }
220 : 84812 : Node ar = rewriteArith(a);
221 : 84812 : Node br = rewriteArith(b);
222 : 42406 : return ar == br;
223 : : }
224 : :
225 : 708499 : bool ArithEntail::check(Node a, Node b, bool strict, bool isSimple)
226 : : {
227 [ + + ]: 708499 : if (a == b)
228 : : {
229 : 53834 : return !strict;
230 : : }
231 : 1309330 : Node diff = NodeManager::currentNM()->mkNode(Kind::SUB, a, b);
232 : 654665 : return check(diff, strict, isSimple);
233 : : }
234 : :
235 : 1071290 : bool ArithEntail::check(Node a, bool strict, bool isSimple)
236 : : {
237 [ + + ]: 1071290 : if (a.isConst())
238 : : {
239 [ + + ]: 116278 : return a.getConst<Rational>().sgn() >= (strict ? 1 : 0);
240 : : }
241 : 2160300 : Node ar = strict ? NodeManager::currentNM()->mkNode(Kind::SUB, a, d_one) : a;
242 : 955009 : ar = rewriteArith(ar);
243 : : // if simple, just call the checkSimple routine.
244 [ + + ]: 955009 : if (isSimple)
245 : : {
246 : 45537 : return checkSimple(ar);
247 : : }
248 : 909472 : Node ara = findApprox(ar, isSimple);
249 : 909472 : return !ara.isNull();
250 : : }
251 : :
252 : 1115310 : Node ArithEntail::findApprox(Node ar, bool isSimple)
253 : : {
254 [ + + ]: 1115310 : std::map<Node, Node>& cache = isSimple ? d_approxCacheSimple : d_approxCache;
255 : 1115310 : std::map<Node, Node>::iterator it = cache.find(ar);
256 [ + + ]: 1115310 : if (it != cache.end())
257 : : {
258 : 784555 : return it->second;
259 : : }
260 : 661506 : Node ret;
261 [ + + ]: 330753 : if (checkSimple(ar))
262 : : {
263 : : // didn't need approximation
264 : 21794 : ret = ar;
265 : : }
266 : : else
267 : : {
268 : 308959 : ret = findApproxInternal(ar, isSimple);
269 : : }
270 : 330753 : cache[ar] = ret;
271 : 330753 : return ret;
272 : : }
273 : :
274 : 308959 : Node ArithEntail::findApproxInternal(Node ar, bool isSimple)
275 : : {
276 : 617918 : Assert(rewriteArith(ar) == ar)
277 : 308959 : << "Not rewritten " << ar << ", got " << rewriteArith(ar);
278 : 308959 : NodeManager* nm = NodeManager::currentNM();
279 : 617918 : std::map<Node, Node> msum;
280 [ + - ]: 617918 : Trace("strings-ent-approx-debug")
281 : 308959 : << "Setup arithmetic approximations for " << ar << std::endl;
282 [ - + ]: 308959 : if (!ArithMSum::getMonomialSum(ar, msum))
283 : : {
284 [ - - ]: 0 : Trace("strings-ent-approx-debug")
285 : 0 : << "...failed to get monomial sum!" << std::endl;
286 : 0 : return Node::null();
287 : : }
288 : : // for each monomial v*c, mApprox[v] a list of
289 : : // possibilities for how the term can be soundly approximated, that is,
290 : : // if mApprox[v] contains av, then v*c > av*c. Notice that if c
291 : : // is positive, then v > av, otherwise if c is negative, then v < av.
292 : : // In other words, av is an under-approximation if c is positive, and an
293 : : // over-approximation if c is negative.
294 : 308959 : bool changed = false;
295 : 617918 : std::map<Node, std::vector<Node> > mApprox;
296 : : // map from approximations to their monomial sums
297 : 617918 : std::map<Node, std::map<Node, Node> > approxMsums;
298 : : // aarSum stores each monomial that does not have multiple approximations
299 : 617918 : std::vector<Node> aarSum;
300 : : // stores the witness
301 : 617918 : arith::ArithSubs approxMap;
302 [ + + ]: 1007500 : for (std::pair<const Node, Node>& m : msum)
303 : : {
304 : 1397090 : Node v = m.first;
305 : 1397090 : Node c = m.second;
306 [ + - ]: 1397090 : Trace("strings-ent-approx-debug")
307 : 698545 : << "Get approximations " << v << "..." << std::endl;
308 [ + + ]: 698545 : if (v.isNull())
309 : : {
310 [ - + ][ - + ]: 453470 : Node mn = c.isNull() ? nm->mkConstInt(Rational(1)) : c;
[ - - ]
311 : 226735 : aarSum.push_back(mn);
312 : : }
313 : : else
314 : : {
315 : : // c.isNull() means c = 1
316 [ + + ][ + + ]: 471810 : bool isOverApprox = !c.isNull() && c.getConst<Rational>().sgn() == -1;
317 : 471810 : std::vector<Node>& approx = mApprox[v];
318 : 943620 : std::unordered_set<Node> visited;
319 : 943620 : std::vector<Node> toProcess;
320 : 471810 : toProcess.push_back(v);
321 : 67540 : do
322 : : {
323 : 1078700 : Node curr = toProcess.back();
324 [ + - ]: 539350 : Trace("strings-ent-approx-debug") << " process " << curr << std::endl;
325 : 539350 : curr = rewriteArith(curr);
326 : 539350 : toProcess.pop_back();
327 [ + + ]: 539350 : if (visited.find(curr) == visited.end())
328 : : {
329 : 532888 : visited.insert(curr);
330 : 1065780 : std::vector<Node> currApprox;
331 : 532888 : getArithApproximations(curr, currApprox, isOverApprox, isSimple);
332 [ + + ]: 532888 : if (currApprox.empty())
333 : : {
334 [ + - ]: 931176 : Trace("strings-ent-approx-debug")
335 : 465588 : << "...approximation: " << curr << std::endl;
336 : : // no approximations, thus curr is a possibility
337 : 465588 : approx.push_back(curr);
338 : : }
339 [ + + ]: 67300 : else if (isSimple)
340 : : {
341 : : // don't rewrite or re-approximate
342 : 17748 : approx = currApprox;
343 : : }
344 : : else
345 : : {
346 : : toProcess.insert(
347 : 49552 : toProcess.end(), currApprox.begin(), currApprox.end());
348 : : }
349 : : }
350 [ + + ]: 539350 : } while (!toProcess.empty());
351 [ - + ][ - + ]: 471810 : Assert(!approx.empty());
[ - - ]
352 : : // if we have only one approximation, move it to final
353 [ + + ]: 471810 : if (approx.size() == 1)
354 : : {
355 [ + + ]: 457662 : if (v != approx[0])
356 : : {
357 : 46680 : changed = true;
358 [ + - ]: 93360 : Trace("strings-ent-approx")
359 : 46680 : << "- Propagate (" << (d_rr == nullptr) << ", " << isSimple
360 : 46680 : << ") " << v << " = " << approx[0] << std::endl;
361 : 46680 : approxMap.add(v, approx[0]);
362 : : }
363 : 1372990 : Node mn = ArithMSum::mkCoeffTerm(c, approx[0]);
364 : 457662 : aarSum.push_back(mn);
365 : 457662 : mApprox.erase(v);
366 : : }
367 : : else
368 : : {
369 : : // compute monomial sum form for each approximation, used below
370 [ + + ]: 42570 : for (const Node& aa : approx)
371 : : {
372 [ + + ]: 28422 : if (approxMsums.find(aa) == approxMsums.end())
373 : : {
374 : : CVC5_UNUSED bool ret =
375 : 27704 : ArithMSum::getMonomialSum(aa, approxMsums[aa]);
376 [ - + ][ - + ]: 27704 : Assert(ret);
[ - - ]
377 : : }
378 : : }
379 : 14148 : changed = true;
380 : : }
381 : : }
382 : : }
383 [ + + ]: 308959 : if (!changed)
384 : : {
385 : : // approximations had no effect, return
386 [ + - ]: 256578 : Trace("strings-ent-approx-debug") << "...no approximations" << std::endl;
387 : 256578 : return Node::null();
388 : : }
389 : : // get the current "fixed" sum for the abstraction of ar
390 : : Node aar =
391 : 52381 : aarSum.empty()
392 : 2879 : ? d_zero
393 [ + + ][ + + ]: 104762 : : (aarSum.size() == 1 ? aarSum[0] : nm->mkNode(Kind::ADD, aarSum));
394 : 52381 : aar = rewriteArith(aar);
395 [ + - ]: 104762 : Trace("strings-ent-approx-debug")
396 : 52381 : << "...processed fixed sum " << aar << " with " << mApprox.size()
397 : 52381 : << " approximated monomials." << std::endl;
398 : : // if we have a choice of how to approximate
399 [ + + ]: 52381 : if (!mApprox.empty())
400 : : {
401 : : // convert aar back to monomial sum
402 : 13878 : std::map<Node, Node> msumAar;
403 [ - + ]: 13878 : if (!ArithMSum::getMonomialSum(aar, msumAar))
404 : : {
405 : 0 : return Node::null();
406 : : }
407 [ - + ]: 13878 : if (TraceIsOn("strings-ent-approx"))
408 : : {
409 [ - - ]: 0 : Trace("strings-ent-approx")
410 : 0 : << "---- Check arithmetic entailment by under-approximation " << ar
411 : 0 : << " >= 0" << std::endl;
412 [ - - ]: 0 : Trace("strings-ent-approx") << "FIXED:" << std::endl;
413 : 0 : ArithMSum::debugPrintMonomialSum(msumAar, "strings-ent-approx");
414 [ - - ]: 0 : Trace("strings-ent-approx") << "APPROX:" << std::endl;
415 [ - - ]: 0 : for (std::pair<const Node, std::vector<Node> >& a : mApprox)
416 : : {
417 : 0 : Node c = msum[a.first];
418 [ - - ]: 0 : Trace("strings-ent-approx") << " ";
419 [ - - ]: 0 : if (!c.isNull())
420 : : {
421 [ - - ]: 0 : Trace("strings-ent-approx") << c << " * ";
422 : : }
423 [ - - ]: 0 : Trace("strings-ent-approx")
424 : 0 : << a.second << " ...from " << a.first << std::endl;
425 : : }
426 [ - - ]: 0 : Trace("strings-ent-approx") << std::endl;
427 : : }
428 : 13878 : Rational one(1);
429 : : // incorporate monomials one at a time that have a choice of approximations
430 [ + + ]: 28026 : while (!mApprox.empty())
431 : : {
432 : 14148 : Node v;
433 : 14148 : Node vapprox;
434 : 14148 : int maxScore = -1;
435 : : // Look at each approximation, take the one with the best score.
436 : : // Notice that we are in the process of trying to prove
437 : : // ( c1*t1 + .. + cn*tn ) + ( approx_1 | ... | approx_m ) >= 0,
438 : : // where c1*t1 + .. + cn*tn is the "fixed" component of our sum (aar)
439 : : // and approx_1 ... approx_m are possible approximations. The
440 : : // intution here is that we want coefficients c1...cn to be positive.
441 : : // This is because arithmetic string terms t1...tn (which may be
442 : : // applications of len, indexof, str.to.int) are never entailed to be
443 : : // negative. Hence, we add the approx_i that contributes the "most"
444 : : // towards making all constants c1...cn positive and cancelling negative
445 : : // monomials in approx_i itself.
446 [ + - ]: 14148 : for (std::pair<const Node, std::vector<Node> >& nam : mApprox)
447 : : {
448 : 14148 : Node cr = msum[nam.first];
449 [ + + ]: 42570 : for (const Node& aa : nam.second)
450 : : {
451 : 28422 : unsigned helpsCancelCount = 0;
452 : 28422 : unsigned addsObligationCount = 0;
453 : 28422 : std::map<Node, Node>::iterator it;
454 : : // we are processing an approximation cr*( c1*t1 + ... + cn*tn )
455 [ + + ]: 62435 : for (std::pair<const Node, Node>& aam : approxMsums[aa])
456 : : {
457 : : // Say aar is of the form t + c*ti, and aam is the monomial ci*ti
458 : : // where ci != 0. We say aam:
459 : : // (1) helps cancel if c != 0 and c>0 != ci>0
460 : : // (2) adds obligation if c>=0 and c+ci<0
461 : 68026 : Node ti = aam.first;
462 : 68026 : Node ci = aam.second;
463 [ + + ]: 34013 : if (!cr.isNull())
464 : : {
465 [ + + ]: 80821 : ci = ci.isNull() ? cr
466 : 80821 : : rewriteArith(nm->mkNode(Kind::MULT, ci, cr));
467 : : }
468 [ + - ]: 34013 : Trace("strings-ent-approx-debug") << ci << "*" << ti << " ";
469 [ + + ]: 34013 : int ciSgn = ci.isNull() ? 1 : ci.getConst<Rational>().sgn();
470 : 34013 : it = msumAar.find(ti);
471 [ + + ]: 34013 : if (it != msumAar.end())
472 : : {
473 : 32838 : Node c = it->second;
474 [ + + ]: 16419 : int cSgn = c.isNull() ? 1 : c.getConst<Rational>().sgn();
475 [ + + ]: 16419 : if (cSgn == 0)
476 : : {
477 [ + + ]: 4022 : addsObligationCount += (ciSgn == -1 ? 1 : 0);
478 : : }
479 [ + + ]: 12397 : else if (cSgn != ciSgn)
480 : : {
481 : 8925 : helpsCancelCount++;
482 [ + + ]: 17850 : Rational r1 = c.isNull() ? one : c.getConst<Rational>();
483 [ + + ]: 17850 : Rational r2 = ci.isNull() ? one : ci.getConst<Rational>();
484 : 17850 : Rational r12 = r1 + r2;
485 [ + + ]: 8925 : if (r12.sgn() == -1)
486 : : {
487 : 4144 : addsObligationCount++;
488 : : }
489 : : }
490 : : }
491 : : else
492 : : {
493 [ + + ]: 17594 : addsObligationCount += (ciSgn == -1 ? 1 : 0);
494 : : }
495 : : }
496 [ + - ]: 56844 : Trace("strings-ent-approx-debug")
497 : 0 : << "counts=" << helpsCancelCount << "," << addsObligationCount
498 : 28422 : << " for " << aa << " into " << aar << std::endl;
499 [ + + ]: 28422 : int score = (addsObligationCount > 0 ? 0 : 2)
500 [ + + ]: 28422 : + (helpsCancelCount > 0 ? 1 : 0);
501 : : // if its the best, update v and vapprox
502 [ + + ][ + + ]: 28422 : if (v.isNull() || score > maxScore)
[ + + ]
503 : : {
504 : 19055 : v = nam.first;
505 : 19055 : vapprox = aa;
506 : 19055 : maxScore = score;
507 : : }
508 : : }
509 [ + - ]: 14148 : if (!v.isNull())
510 : : {
511 : 14148 : break;
512 : : }
513 : : }
514 [ + - ]: 28296 : Trace("strings-ent-approx") << "- Decide (" << (d_rr == nullptr) << ") "
515 : 14148 : << v << " = " << vapprox << std::endl;
516 : : // we incorporate v approximated by vapprox into the overall approximation
517 : : // for ar
518 [ + - ][ + - ]: 28296 : Assert(!v.isNull() && !vapprox.isNull());
[ - + ][ - - ]
519 [ - + ][ - + ]: 14148 : Assert(msum.find(v) != msum.end());
[ - - ]
520 : 28296 : Node mn = ArithMSum::mkCoeffTerm(msum[v], vapprox);
521 : 14148 : aar = nm->mkNode(Kind::ADD, aar, mn);
522 : 14148 : approxMap.add(v, vapprox);
523 : : // update the msumAar map
524 : 14148 : aar = rewriteArith(aar);
525 : 14148 : msumAar.clear();
526 [ - + ]: 14148 : if (!ArithMSum::getMonomialSum(aar, msumAar))
527 : : {
528 : 0 : Assert(false);
529 : : Trace("strings-ent-approx")
530 : : << "...failed to get monomial sum!" << std::endl;
531 : : return Node::null();
532 : : }
533 : : // we have processed the approximation for v
534 : 14148 : mApprox.erase(v);
535 : : }
536 [ + - ]: 13878 : Trace("strings-ent-approx") << "-----------------" << std::endl;
537 : : }
538 [ - + ]: 52381 : if (aar == ar)
539 : : {
540 [ - - ]: 0 : Trace("strings-ent-approx-debug")
541 : 0 : << "...approximation had no effect" << std::endl;
542 : : // this should never happen, but we avoid the infinite loop for sanity here
543 : 0 : Assert(false);
544 : : return Node::null();
545 : : }
546 : : // Check entailment on the approximation of ar.
547 : : // Notice that this may trigger further reasoning by approximation. For
548 : : // example, len( replace( x ++ y, substr( x, 0, n ), z ) ) may be
549 : : // under-approximated as len( x ) + len( y ) - len( substr( x, 0, n ) ) on
550 : : // this call, where in the recursive call we may over-approximate
551 : : // len( substr( x, 0, n ) ) as len( x ). In this example, we can infer
552 : : // that len( replace( x ++ y, substr( x, 0, n ), z ) ) >= len( y ) in two
553 : : // steps.
554 [ + + ]: 52381 : if (check(aar, false, isSimple))
555 : : {
556 [ + - ]: 9716 : Trace("strings-ent-approx")
557 : 0 : << "*** StrArithApprox: showed " << ar
558 : 4858 : << " >= 0 using under-approximation!" << std::endl;
559 [ + - ]: 9716 : Trace("strings-ent-approx")
560 : 4858 : << "*** StrArithApprox: rewritten was " << aar << std::endl;
561 : : // Apply arithmetic substitution, which ensures we only replace terms
562 : : // in the top-level arithmetic skeleton of ar.
563 : 9716 : Node approx = approxMap.applyArith(ar);
564 [ + - ]: 9716 : Trace("strings-ent-approx")
565 : 0 : << "*** StrArithApprox: under-approximation was " << approx
566 : 4858 : << std::endl;
567 : 4858 : return approx;
568 : : }
569 : 47523 : return Node::null();
570 : : }
571 : :
572 : 533747 : void ArithEntail::getArithApproximations(Node a,
573 : : std::vector<Node>& approx,
574 : : bool isOverApprox,
575 : : bool isSimple)
576 : : {
577 : 533747 : NodeManager* nm = NodeManager::currentNM();
578 : : // We do not handle ADD here since this leads to exponential behavior.
579 : : // Instead, this is managed, e.g. during checkApprox, where
580 : : // ADD terms are expanded "on-demand" during the reasoning.
581 [ + - ]: 1067490 : Trace("strings-ent-approx-debug")
582 : 533747 : << "Get arith approximations " << a << std::endl;
583 : 533747 : Kind ak = a.getKind();
584 [ + + ]: 533747 : if (ak == Kind::MULT)
585 : : {
586 : 1718 : Node c;
587 : 1718 : Node v;
588 [ + - ]: 859 : if (ArithMSum::getMonomial(a, c, v))
589 : : {
590 : 859 : bool isNeg = c.getConst<Rational>().sgn() == -1;
591 [ + + ]: 1718 : getArithApproximations(
592 : 96 : v, approx, isNeg ? !isOverApprox : isOverApprox, isSimple);
593 [ + + ]: 863 : for (unsigned i = 0, size = approx.size(); i < size; i++)
594 : : {
595 : 4 : approx[i] = nm->mkNode(Kind::MULT, c, approx[i]);
596 : : }
597 : : }
598 : : }
599 [ + + ]: 532888 : else if (ak == Kind::STRING_LENGTH)
600 : : {
601 : 301787 : Kind aak = a[0].getKind();
602 [ + + ]: 301787 : if (aak == Kind::STRING_SUBSTR)
603 : : {
604 : : // over,under-approximations for len( substr( x, n, m ) )
605 : 168750 : Node lenx = nm->mkNode(Kind::STRING_LENGTH, a[0][0]);
606 [ + + ]: 56250 : if (isOverApprox)
607 : : {
608 : : // m >= 0 implies
609 : : // m >= len( substr( x, n, m ) )
610 [ + + ]: 33134 : if (check(a[0][2], false, isSimple))
611 : : {
612 : 18380 : approx.push_back(a[0][2]);
613 : : }
614 [ + + ]: 33134 : if (check(lenx, a[0][1], false, isSimple))
615 : : {
616 : : // n <= len( x ) implies
617 : : // len( x ) - n >= len( substr( x, n, m ) )
618 : 14428 : approx.push_back(nm->mkNode(Kind::SUB, lenx, a[0][1]));
619 : : }
620 : : else
621 : : {
622 : : // len( x ) >= len( substr( x, n, m ) )
623 : 18706 : approx.push_back(lenx);
624 : : }
625 : : }
626 : : else
627 : : {
628 : : // 0 <= n and n+m <= len( x ) implies
629 : : // m <= len( substr( x, n, m ) )
630 : 69348 : Node npm = nm->mkNode(Kind::ADD, a[0][1], a[0][2]);
631 : 46232 : if (check(a[0][1], false, isSimple)
632 : 46232 : && check(lenx, npm, false, isSimple))
633 : : {
634 : 3920 : approx.push_back(a[0][2]);
635 : : }
636 : : // 0 <= n and n+m >= len( x ) implies
637 : : // len(x)-n <= len( substr( x, n, m ) )
638 : 46232 : if (check(a[0][1], false, isSimple)
639 : 46232 : && check(npm, lenx, false, isSimple))
640 : : {
641 : 2969 : approx.push_back(nm->mkNode(Kind::SUB, lenx, a[0][1]));
642 : : }
643 : : }
644 : : }
645 [ + + ]: 245537 : else if (aak == Kind::STRING_REPLACE)
646 : : {
647 : : // over,under-approximations for len( replace( x, y, z ) )
648 : : // notice this is either len( x ) or ( len( x ) + len( z ) - len( y ) )
649 : 45507 : Node lenx = nm->mkNode(Kind::STRING_LENGTH, a[0][0]);
650 : 45507 : Node leny = nm->mkNode(Kind::STRING_LENGTH, a[0][1]);
651 : 45507 : Node lenz = nm->mkNode(Kind::STRING_LENGTH, a[0][2]);
652 [ + + ]: 15169 : if (isOverApprox)
653 : : {
654 [ + + ]: 8363 : if (check(leny, lenz, false, isSimple))
655 : : {
656 : : // len( y ) >= len( z ) implies
657 : : // len( x ) >= len( replace( x, y, z ) )
658 : 1480 : approx.push_back(lenx);
659 : : }
660 : : else
661 : : {
662 : : // len( x ) + len( z ) >= len( replace( x, y, z ) )
663 : 6883 : approx.push_back(nm->mkNode(Kind::ADD, lenx, lenz));
664 : : }
665 : : }
666 : : else
667 : : {
668 [ + - ][ + + ]: 6806 : if (check(lenz, leny, false, isSimple)
[ - - ][ - - ]
669 : 6806 : || check(lenz, lenx, false, isSimple))
670 : : {
671 : : // len( y ) <= len( z ) or len( x ) <= len( z ) implies
672 : : // len( x ) <= len( replace( x, y, z ) )
673 : 2851 : approx.push_back(lenx);
674 : : }
675 : : else
676 : : {
677 : : // len( x ) - len( y ) <= len( replace( x, y, z ) )
678 : 3955 : approx.push_back(nm->mkNode(Kind::SUB, lenx, leny));
679 : : }
680 : : }
681 : : }
682 [ + + ]: 230368 : else if (aak == Kind::STRING_ITOS)
683 : : {
684 : : // over,under-approximations for len( int.to.str( x ) )
685 [ + + ]: 5102 : if (isOverApprox)
686 : : {
687 [ + + ]: 2806 : if (check(a[0][0], false, isSimple))
688 : : {
689 [ + + ]: 1433 : if (check(a[0][0], true, isSimple))
690 : : {
691 : : // x > 0 implies
692 : : // x >= len( int.to.str( x ) )
693 : 425 : approx.push_back(a[0][0]);
694 : : }
695 : : else
696 : : {
697 : : // x >= 0 implies
698 : : // x+1 >= len( int.to.str( x ) )
699 : 1008 : approx.push_back(
700 : 2016 : nm->mkNode(Kind::ADD, nm->mkConstInt(Rational(1)), a[0][0]));
701 : : }
702 : : }
703 : : }
704 : : else
705 : : {
706 [ + + ]: 2296 : if (check(a[0][0], false, isSimple))
707 : : {
708 : : // x >= 0 implies
709 : : // len( int.to.str( x ) ) >= 1
710 : 1430 : approx.push_back(nm->mkConstInt(Rational(1)));
711 : : }
712 : : // other crazy things are possible here, e.g.
713 : : // len( int.to.str( len( y ) + 10 ) ) >= 2
714 : : }
715 : : }
716 : : }
717 [ + + ]: 231101 : else if (ak == Kind::STRING_INDEXOF)
718 : : {
719 : : // over,under-approximations for indexof( x, y, n )
720 [ + + ]: 11569 : if (isOverApprox)
721 : : {
722 : 17715 : Node lenx = nm->mkNode(Kind::STRING_LENGTH, a[0]);
723 : 17715 : Node leny = nm->mkNode(Kind::STRING_LENGTH, a[1]);
724 [ + + ]: 5905 : if (check(lenx, leny, false, isSimple))
725 : : {
726 : : // len( x ) >= len( y ) implies
727 : : // len( x ) - len( y ) >= indexof( x, y, n )
728 : 263 : approx.push_back(nm->mkNode(Kind::SUB, lenx, leny));
729 : : }
730 : : else
731 : : {
732 : : // len( x ) >= indexof( x, y, n )
733 : 5642 : approx.push_back(lenx);
734 : : }
735 : : }
736 : : else
737 : : {
738 : : // TODO?:
739 : : // contains( substr( x, n, len( x ) ), y ) implies
740 : : // n <= indexof( x, y, n )
741 : : // ...hard to test, runs risk of non-termination
742 : :
743 : : // -1 <= indexof( x, y, n )
744 : 5664 : approx.push_back(nm->mkConstInt(Rational(-1)));
745 : : }
746 : : }
747 [ + + ]: 219532 : else if (ak == Kind::STRING_STOI)
748 : : {
749 : : // over,under-approximations for str.to.int( x )
750 [ + + ]: 62 : if (isOverApprox)
751 : : {
752 : : // TODO?:
753 : : // y >= 0 implies
754 : : // y >= str.to.int( int.to.str( y ) )
755 : : }
756 : : else
757 : : {
758 : : // -1 <= str.to.int( x )
759 : 32 : approx.push_back(nm->mkConstInt(Rational(-1)));
760 : : }
761 : : }
762 [ + - ]: 1067490 : Trace("strings-ent-approx-debug")
763 : 533747 : << "Return " << approx.size() << " approximations" << std::endl;
764 : 534510 : }
765 : :
766 : 4161 : bool ArithEntail::checkWithEqAssumption(Node assumption, Node a, bool strict)
767 : : {
768 [ - + ][ - + ]: 4161 : Assert(assumption.getKind() == Kind::EQUAL);
[ - - ]
769 [ + - ]: 8322 : Trace("strings-entail") << "checkWithEqAssumption: " << assumption << " " << a
770 : 4161 : << ", strict=" << strict << std::endl;
771 : :
772 : : // Find candidates variables to compute substitutions for
773 : 8322 : std::unordered_set<Node> candVars;
774 : 20805 : std::vector<Node> toVisit = {assumption};
775 [ + + ]: 28791 : while (!toVisit.empty())
776 : : {
777 : 49260 : Node curr = toVisit.back();
778 : 24630 : toVisit.pop_back();
779 : :
780 [ + + ]: 44807 : if (curr.getKind() == Kind::ADD || curr.getKind() == Kind::MULT
781 [ + + ][ + + ]: 44807 : || curr.getKind() == Kind::SUB || curr.getKind() == Kind::EQUAL)
[ + + ][ + + ]
782 : : {
783 [ + + ]: 30702 : for (const auto& currChild : curr)
784 : : {
785 : 20469 : toVisit.push_back(currChild);
786 : : }
787 : : }
788 [ + + ][ + - ]: 14397 : else if (curr.isVar() && Theory::theoryOf(curr) == THEORY_ARITH)
[ + + ][ + + ]
[ - - ]
789 : : {
790 : 3235 : candVars.insert(curr);
791 : : }
792 [ + + ]: 11162 : else if (curr.getKind() == Kind::STRING_LENGTH)
793 : : {
794 : 5080 : candVars.insert(curr);
795 : : }
796 : : }
797 : :
798 : : // Check if any of the candidate variables are in n
799 : 8322 : Node v;
800 [ - + ][ - + ]: 4161 : Assert(toVisit.empty());
[ - - ]
801 : 4161 : toVisit.push_back(a);
802 [ + + ]: 18040 : while (!toVisit.empty())
803 : : {
804 : 14111 : Node curr = toVisit.back();
805 : 14111 : toVisit.pop_back();
806 : :
807 [ + + ]: 24645 : for (const auto& currChild : curr)
808 : : {
809 : 10534 : toVisit.push_back(currChild);
810 : : }
811 : :
812 [ + + ]: 14111 : if (candVars.find(curr) != candVars.end())
813 : : {
814 : 232 : v = curr;
815 : 232 : break;
816 : : }
817 : : }
818 : :
819 [ + + ]: 4161 : if (v.isNull())
820 : : {
821 : : // No suitable candidate found
822 : 3929 : return false;
823 : : }
824 : :
825 : 696 : Node solution = ArithMSum::solveEqualityFor(assumption, v);
826 [ + + ]: 232 : if (solution.isNull())
827 : : {
828 : : // Could not solve for v
829 : 35 : return false;
830 : : }
831 [ + - ]: 394 : Trace("strings-entail") << "checkWithEqAssumption: subs " << v << " -> "
832 : 197 : << solution << std::endl;
833 : :
834 : 394 : TNode tv = v;
835 : 197 : TNode tsolution = solution;
836 : 197 : a = a.substitute(tv, tsolution);
837 : 197 : return check(a, strict);
838 : : }
839 : :
840 : 7605 : bool ArithEntail::checkWithAssumption(Node assumption,
841 : : Node a,
842 : : Node b,
843 : : bool strict)
844 : : {
845 : 7605 : NodeManager* nm = NodeManager::currentNM();
846 : :
847 [ + + ][ + + ]: 7605 : if (!assumption.isConst() && assumption.getKind() != Kind::EQUAL)
[ + + ]
848 : : {
849 : : // We rewrite inequality assumptions from x <= y to x + (str.len s) = y
850 : : // where s is some fresh string variable. We use (str.len s) because
851 : : // (str.len s) must be non-negative for the equation to hold.
852 : 8314 : Node x, y;
853 [ + + ]: 4157 : if (assumption.getKind() == Kind::GEQ)
854 : : {
855 : 2858 : x = assumption[0];
856 : 2858 : y = assumption[1];
857 : : }
858 : : else
859 : : {
860 : : // (not (>= s t)) --> (>= (t - 1) s)
861 : 2598 : Assert(assumption.getKind() == Kind::NOT
862 : : && assumption[0].getKind() == Kind::GEQ);
863 : 1299 : x = nm->mkNode(Kind::SUB, assumption[0][1], nm->mkConstInt(Rational(1)));
864 : 1299 : y = assumption[0][0];
865 : : }
866 : :
867 : 12471 : Node s = nm->mkBoundVar("slackVal", nm->stringType());
868 : 8314 : Node slen = nm->mkNode(Kind::STRING_LENGTH, s);
869 : 12471 : Node sleny = nm->mkNode(Kind::ADD, y, slen);
870 : 12471 : Node rr = rewriteArith(nm->mkNode(Kind::SUB, x, sleny));
871 [ - + ]: 4157 : if (rr.isConst())
872 : : {
873 : 0 : assumption = nm->mkConst(rr.getConst<Rational>().sgn() == 0);
874 : : }
875 : : else
876 : : {
877 : 4157 : assumption = nm->mkNode(Kind::EQUAL, x, sleny);
878 : : }
879 : : }
880 : :
881 : 15210 : Node diff = nm->mkNode(Kind::SUB, a, b);
882 : 7605 : bool res = false;
883 [ + + ]: 7605 : if (assumption.isConst())
884 : : {
885 : 3444 : bool assumptionBool = assumption.getConst<bool>();
886 [ + - ]: 3444 : if (assumptionBool)
887 : : {
888 : 3444 : res = check(diff, strict);
889 : : }
890 : : else
891 : : {
892 : 0 : res = true;
893 : : }
894 : : }
895 : : else
896 : : {
897 : 4161 : res = checkWithEqAssumption(assumption, diff, strict);
898 : : }
899 : 15210 : return res;
900 : : }
901 : :
902 : 0 : bool ArithEntail::checkWithAssumptions(std::vector<Node> assumptions,
903 : : Node a,
904 : : Node b,
905 : : bool strict)
906 : : {
907 : : // TODO: We currently try to show the entailment with each assumption
908 : : // independently. In the future, we should make better use of multiple
909 : : // assumptions.
910 : 0 : bool res = false;
911 [ - - ]: 0 : for (const auto& assumption : assumptions)
912 : : {
913 [ - - ]: 0 : if (checkWithAssumption(assumption, a, b, strict))
914 : : {
915 : 0 : res = true;
916 : 0 : break;
917 : : }
918 : : }
919 : 0 : return res;
920 : : }
921 : :
922 : : struct ArithEntailConstantBoundLowerId
923 : : {
924 : : };
925 : : typedef expr::Attribute<ArithEntailConstantBoundLowerId, Node>
926 : : ArithEntailConstantBoundLower;
927 : :
928 : : struct ArithEntailConstantBoundUpperId
929 : : {
930 : : };
931 : : typedef expr::Attribute<ArithEntailConstantBoundUpperId, Node>
932 : : ArithEntailConstantBoundUpper;
933 : :
934 : 74523 : void ArithEntail::setConstantBoundCache(TNode n, Node ret, bool isLower)
935 : : {
936 [ + + ]: 74523 : if (isLower)
937 : : {
938 : : ArithEntailConstantBoundLower acbl;
939 : 40656 : n.setAttribute(acbl, ret);
940 : : }
941 : : else
942 : : {
943 : : ArithEntailConstantBoundUpper acbu;
944 : 33867 : n.setAttribute(acbu, ret);
945 : : }
946 : 74523 : }
947 : :
948 : 915981 : bool ArithEntail::getConstantBoundCache(TNode n, bool isLower, Node& c)
949 : : {
950 [ + + ]: 915981 : if (isLower)
951 : : {
952 : : ArithEntailConstantBoundLower acbl;
953 [ + + ]: 830417 : if (n.hasAttribute(acbl))
954 : : {
955 : 789761 : c = n.getAttribute(acbl);
956 : 789761 : return true;
957 : : }
958 : : }
959 : : else
960 : : {
961 : : ArithEntailConstantBoundUpper acbu;
962 [ + + ]: 85564 : if (n.hasAttribute(acbu))
963 : : {
964 : 51697 : c = n.getAttribute(acbu);
965 : 51697 : return true;
966 : : }
967 : : }
968 : 74523 : return false;
969 : : }
970 : :
971 : 36309 : Node ArithEntail::getConstantBound(TNode a, bool isLower)
972 : : {
973 [ - + ][ - + ]: 36309 : Assert(rewriteArith(a) == a);
[ - - ]
974 : 36309 : Node ret;
975 [ + + ]: 36309 : if (getConstantBoundCache(a, isLower, ret))
976 : : {
977 : 29520 : return ret;
978 : : }
979 [ + + ]: 6789 : if (a.isConst())
980 : : {
981 : 1788 : ret = a;
982 : : }
983 [ + + ]: 5001 : else if (a.getKind() == Kind::STRING_LENGTH)
984 : : {
985 [ + - ]: 774 : if (isLower)
986 : : {
987 : 774 : ret = d_zero;
988 : : }
989 : : }
990 [ + + ][ + + ]: 4227 : else if (a.getKind() == Kind::ADD || a.getKind() == Kind::MULT)
[ + + ]
991 : : {
992 : 6840 : std::vector<Node> children;
993 : 3420 : bool success = true;
994 [ + + ]: 6686 : for (unsigned i = 0; i < a.getNumChildren(); i++)
995 : : {
996 : 5967 : Node ac = getConstantBound(a[i], isLower);
997 [ + + ]: 5967 : if (ac.isNull())
998 : : {
999 : 1740 : ret = ac;
1000 : 1740 : success = false;
1001 : 1740 : break;
1002 : : }
1003 : : else
1004 : : {
1005 [ + + ]: 4227 : if (ac.getConst<Rational>().sgn() == 0)
1006 : : {
1007 [ + + ]: 1139 : if (a.getKind() == Kind::MULT)
1008 : : {
1009 : 16 : ret = ac;
1010 : 16 : success = false;
1011 : 16 : break;
1012 : : }
1013 : : }
1014 : : else
1015 : : {
1016 [ + + ]: 3088 : if (a.getKind() == Kind::MULT)
1017 : : {
1018 [ + + ]: 963 : if ((ac.getConst<Rational>().sgn() > 0) != isLower)
1019 : : {
1020 : 945 : ret = Node::null();
1021 : 945 : success = false;
1022 : 945 : break;
1023 : : }
1024 : : }
1025 : 2143 : children.push_back(ac);
1026 : : }
1027 : : }
1028 : : }
1029 [ + + ]: 3420 : if (success)
1030 : : {
1031 [ + + ]: 719 : if (children.empty())
1032 : : {
1033 : 208 : ret = d_zero;
1034 : : }
1035 [ + - ]: 511 : else if (children.size() == 1)
1036 : : {
1037 : 511 : ret = children[0];
1038 : : }
1039 : : else
1040 : : {
1041 : 0 : ret = NodeManager::currentNM()->mkNode(a.getKind(), children);
1042 : 0 : ret = rewriteArith(ret);
1043 : : }
1044 : : }
1045 : : }
1046 [ + - ]: 13578 : Trace("strings-rewrite-cbound")
1047 [ - - ]: 0 : << "Constant " << (isLower ? "lower" : "upper") << " bound for " << a
1048 : 6789 : << " is " << ret << std::endl;
1049 [ + + ][ - + ]: 6789 : Assert(ret.isNull() || ret.isConst());
[ - + ][ - - ]
1050 : : // entailment check should be at least as powerful as computing a lower bound
1051 : 6789 : Assert(!isLower || ret.isNull() || ret.getConst<Rational>().sgn() < 0
1052 : : || check(a, false));
1053 : 6789 : Assert(!isLower || ret.isNull() || ret.getConst<Rational>().sgn() <= 0
1054 : : || check(a, true));
1055 : : // cache
1056 : 6789 : setConstantBoundCache(a, ret, isLower);
1057 : 6789 : return ret;
1058 : : }
1059 : :
1060 : 879672 : Node ArithEntail::getConstantBoundLength(TNode s, bool isLower) const
1061 : : {
1062 [ - + ][ - + ]: 879672 : Assert(s.getType().isStringLike());
[ - - ]
1063 : 879672 : Node ret;
1064 [ + + ]: 879672 : if (getConstantBoundCache(s, isLower, ret))
1065 : : {
1066 : 811938 : return ret;
1067 : : }
1068 : 67734 : NodeManager* nm = NodeManager::currentNM();
1069 : 67734 : Kind sk = s.getKind();
1070 [ + + ]: 67734 : if (s.isConst())
1071 : : {
1072 : 12138 : size_t len = Word::getLength(s);
1073 : 12138 : ret = nm->mkConstInt(Rational(len));
1074 : : }
1075 [ + + ][ + + ]: 55596 : else if (sk == Kind::SEQ_UNIT || sk == Kind::STRING_UNIT)
1076 : : {
1077 : 1290 : ret = nm->mkConstInt(1);
1078 : : }
1079 [ + + ]: 54306 : else if (sk == Kind::STRING_CONCAT)
1080 : : {
1081 : 39912 : Rational sum(0);
1082 : 19956 : bool success = true;
1083 [ + + ]: 45493 : for (const Node& sc : s)
1084 : : {
1085 : 35511 : Node b = getConstantBoundLength(sc, isLower);
1086 [ + + ]: 35511 : if (b.isNull())
1087 : : {
1088 [ - + ]: 9974 : if (isLower)
1089 : : {
1090 : : // assume zero and continue
1091 : 0 : continue;
1092 : : }
1093 : 9974 : success = false;
1094 : 9974 : break;
1095 : : }
1096 [ - + ][ - + ]: 25537 : Assert(b.isConst());
[ - - ]
1097 : 25537 : sum = sum + b.getConst<Rational>();
1098 : : }
1099 [ + + ][ + + ]: 19956 : if (success && (!isLower || sum.sgn() != 0))
[ + + ][ + + ]
1100 : : {
1101 : 4483 : ret = nm->mkConstInt(sum);
1102 : : }
1103 : : }
1104 [ + + ][ + + ]: 67734 : if (ret.isNull() && isLower)
[ + + ]
1105 : : {
1106 : 22674 : ret = d_zero;
1107 : : }
1108 : : // cache
1109 : 67734 : setConstantBoundCache(s, ret, isLower);
1110 : 67734 : return ret;
1111 : : }
1112 : :
1113 : 927823 : bool ArithEntail::checkSimple(Node a)
1114 : : {
1115 : : // check whether a >= 0
1116 [ + + ]: 927823 : if (a.isConst())
1117 : : {
1118 : 389173 : return a.getConst<Rational>().sgn() >= 0;
1119 : : }
1120 [ + + ]: 538650 : else if (a.getKind() == Kind::STRING_LENGTH)
1121 : : {
1122 : : // str.len( t ) >= 0
1123 : 68526 : return true;
1124 : : }
1125 [ + + ][ + + ]: 470124 : else if (a.getKind() == Kind::ADD || a.getKind() == Kind::MULT)
[ + + ]
1126 : : {
1127 [ + + ]: 561198 : for (unsigned i = 0; i < a.getNumChildren(); i++)
1128 : : {
1129 [ + + ]: 551461 : if (!checkSimple(a[i]))
1130 : : {
1131 : 429516 : return false;
1132 : : }
1133 : : }
1134 : : // t1 >= 0 ^ ... ^ tn >= 0 => t1 op ... op tn >= 0
1135 : 9737 : return true;
1136 : : }
1137 : :
1138 : 30871 : return false;
1139 : : }
1140 : :
1141 : 2463 : bool ArithEntail::inferZerosInSumGeq(Node x,
1142 : : std::vector<Node>& ys,
1143 : : std::vector<Node>& zeroYs)
1144 : : {
1145 [ - + ][ - + ]: 2463 : Assert(zeroYs.empty());
[ - - ]
1146 : :
1147 : 2463 : NodeManager* nm = NodeManager::currentNM();
1148 : :
1149 : : // Check if we can show that y1 + ... + yn >= x
1150 [ + + ]: 4926 : Node sum = (ys.size() > 1) ? nm->mkNode(Kind::ADD, ys) : ys[0];
1151 [ + + ]: 2463 : if (!check(sum, x))
1152 : : {
1153 : 2198 : return false;
1154 : : }
1155 : :
1156 : : // Try to remove yi one-by-one and check if we can still show:
1157 : : //
1158 : : // y1 + ... + yi-1 + yi+1 + ... + yn >= x
1159 : : //
1160 : : // If that's the case, we know that yi can be zero and the inequality still
1161 : : // holds.
1162 : 265 : size_t i = 0;
1163 [ + + ]: 782 : while (i < ys.size())
1164 : : {
1165 : 1034 : Node yi = ys[i];
1166 : 517 : std::vector<Node>::iterator pos = ys.erase(ys.begin() + i);
1167 [ + + ]: 517 : if (ys.size() > 1)
1168 : : {
1169 : 130 : sum = nm->mkNode(Kind::ADD, ys);
1170 : : }
1171 : : else
1172 : : {
1173 [ + + ]: 387 : sum = ys.size() == 1 ? ys[0] : d_zero;
1174 : : }
1175 : :
1176 [ + + ]: 517 : if (check(sum, x))
1177 : : {
1178 : 95 : zeroYs.push_back(yi);
1179 : : }
1180 : : else
1181 : : {
1182 : 422 : ys.insert(pos, yi);
1183 : 422 : i++;
1184 : : }
1185 : : }
1186 : 265 : return true;
1187 : : }
1188 : :
1189 : : } // namespace strings
1190 : : } // namespace theory
1191 : : } // namespace cvc5::internal
|
