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 arithmetic entailment computation for string terms.
11 : : */
12 : :
13 : : #include "theory/strings/arith_entail.h"
14 : :
15 : : #include "expr/aci_norm.h"
16 : : #include "expr/attribute.h"
17 : : #include "expr/node_algorithm.h"
18 : : #include "proof/conv_proof_generator.h"
19 : : #include "theory/arith/arith_msum.h"
20 : : #include "theory/arith/arith_poly_norm.h"
21 : : #include "theory/arith/arith_subs.h"
22 : : #include "theory/rewriter.h"
23 : : #include "theory/strings/theory_strings_utils.h"
24 : : #include "theory/strings/word.h"
25 : : #include "theory/theory.h"
26 : : #include "util/rational.h"
27 : :
28 : : using namespace cvc5::internal::kind;
29 : :
30 : : namespace cvc5::internal {
31 : : namespace theory {
32 : : namespace strings {
33 : :
34 : 343181 : ArithEntail::ArithEntail(NodeManager* nm, Rewriter* r, bool recApprox)
35 : 343181 : : d_rr(r), d_recApprox(recApprox)
36 : : {
37 : 343181 : d_one = nm->mkConstInt(Rational(1));
38 : 343181 : d_zero = nm->mkConstInt(Rational(0));
39 : 343181 : }
40 : :
41 : 147259 : Node ArithEntail::rewritePredViaEntailment(const Node& n, bool isSimple)
42 : : {
43 : 147259 : Node exp;
44 : 294518 : return rewritePredViaEntailment(n, exp, isSimple);
45 : 147259 : }
46 : :
47 : 148354 : Node ArithEntail::rewritePredViaEntailment(const Node& n,
48 : : Node& exp,
49 : : bool isSimple)
50 : : {
51 : 148354 : NodeManager* nm = n.getNodeManager();
52 : 148354 : if (n.getKind() == Kind::EQUAL && n[0].getType().isInteger())
53 : : {
54 : 40060 : exp = nm->mkNode(Kind::SUB, nm->mkNode(Kind::SUB, n[0], n[1]), d_one);
55 [ + + ]: 40060 : if (!findApprox(rewriteArith(exp), isSimple).isNull())
56 : : {
57 : 6650 : return nm->mkConst(false);
58 : : }
59 : 36735 : exp = nm->mkNode(Kind::SUB, nm->mkNode(Kind::SUB, n[1], n[0]), d_one);
60 [ + + ]: 36735 : if (!findApprox(rewriteArith(exp), isSimple).isNull())
61 : : {
62 : 4254 : return nm->mkConst(false);
63 : : }
64 : 34608 : exp = Node::null();
65 [ + + ]: 34608 : if (checkEq(n[0], n[1]))
66 : : {
67 : : // explanation is null
68 : 842 : return nm->mkConst(true);
69 : : }
70 : : }
71 [ + - ]: 108294 : else if (n.getKind() == Kind::GEQ)
72 : : {
73 : 108294 : exp = nm->mkNode(Kind::SUB, n[0], n[1]);
74 [ + + ]: 108294 : if (!findApprox(rewriteArith(exp), isSimple).isNull())
75 : : {
76 : 6714 : return nm->mkConst(true);
77 : : }
78 : 104937 : exp = nm->mkNode(Kind::SUB, nm->mkNode(Kind::SUB, n[1], n[0]), d_one);
79 [ + + ]: 104937 : if (!findApprox(rewriteArith(exp), isSimple).isNull())
80 : : {
81 : 19694 : return nm->mkConst(false);
82 : : }
83 : 95090 : exp = Node::null();
84 : : }
85 : 129277 : return Node::null();
86 : : }
87 : :
88 : 2155019 : Node ArithEntail::rewriteArith(Node a)
89 : : {
90 [ - + ][ - - ]: 4310038 : AlwaysAssert(a.getType().isInteger())
91 : 2155019 : << "Bad term: " << a << " " << a.getType();
92 [ + + ]: 2155019 : if (d_rr != nullptr)
93 : : {
94 : 294985 : return d_rr->rewrite(a);
95 : : }
96 : : else
97 : : {
98 : 1860034 : a = rewriteLengthIntro(a);
99 : : }
100 : : // Otherwise, use the poly norm utility. This is important since the rewrite
101 : : // must be justified by ARITH_POLY_NORM when in proof mode (when d_rr is
102 : : // null).
103 : 1860034 : Node an = arith::PolyNorm::getPolyNorm(a);
104 : 1860034 : return an;
105 : 1860034 : }
106 : :
107 : 94280 : Node ArithEntail::normalizeGeq(const Node& n) const
108 : : {
109 : 94280 : NodeManager* nm = n.getNodeManager();
110 : 188560 : if (n.getNumChildren() != 2 || !n[0].getType().isInteger()
111 : 188560 : || !n[1].getType().isInteger())
112 : : {
113 : 99 : return Node::null();
114 : : }
115 [ + + ][ + + ]: 94181 : switch (n.getKind())
[ - ]
116 : : {
117 : 60807 : case Kind::GEQ: return n;
118 : 11074 : case Kind::LEQ: return nm->mkNode(Kind::GEQ, n[1], n[0]);
119 : 9152 : case Kind::LT:
120 : : return nm->mkNode(
121 : : Kind::GEQ,
122 : : n[1],
123 : 9152 : nm->mkNode(Kind::ADD, n[0], nm->mkConstInt(Rational(1))));
124 : 13148 : case Kind::GT:
125 : : return nm->mkNode(
126 : : Kind::GEQ,
127 : : n[0],
128 : 13148 : nm->mkNode(Kind::ADD, n[1], nm->mkConstInt(Rational(1))));
129 : 0 : default: break;
130 : : }
131 : 0 : return Node::null();
132 : : }
133 : :
134 : 1973355 : Node ArithEntail::rewriteLengthIntro(const Node& n,
135 : : TConvProofGenerator* pg) const
136 : : {
137 : 1973355 : NodeManager* nm = n.getNodeManager();
138 : 1973355 : std::unordered_map<TNode, Node> visited;
139 : 1973355 : std::unordered_map<TNode, Node>::iterator it;
140 : 1973355 : std::vector<TNode> visit;
141 : 1973355 : TNode cur;
142 : 1973355 : visit.push_back(n);
143 : : do
144 : : {
145 : 33709761 : cur = visit.back();
146 : 33709761 : it = visited.find(cur);
147 [ + + ]: 33709761 : if (it == visited.end())
148 : : {
149 [ + + ]: 18387179 : if (cur.getNumChildren() == 0)
150 : : {
151 : 7555162 : visit.pop_back();
152 : 7555162 : visited[cur] = cur;
153 : 7555162 : continue;
154 : : }
155 : 10832017 : visited.emplace(cur, Node::null());
156 : 10832017 : visit.insert(visit.end(), cur.begin(), cur.end());
157 : 10832017 : continue;
158 : : }
159 : 15322582 : visit.pop_back();
160 [ + + ]: 15322582 : if (it->second.isNull())
161 : : {
162 : 10832017 : Kind k = cur.getKind();
163 : 10832017 : bool childChanged = false;
164 : 10832017 : std::vector<Node> children;
165 [ + + ]: 10832017 : if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
166 : : {
167 : 185159 : children.push_back(cur.getOperator());
168 : : }
169 [ + + ]: 31736406 : for (const Node& cn : cur)
170 : : {
171 : 20904389 : it = visited.find(cn);
172 [ - + ][ - + ]: 20904389 : Assert(it != visited.end());
[ - - ]
173 [ - + ][ - + ]: 20904389 : Assert(!it->second.isNull());
[ - - ]
174 : 20904389 : children.push_back(it->second);
175 [ + + ][ + + ]: 20904389 : childChanged = childChanged || it->second != cn;
176 : 20904389 : }
177 : 10832017 : Node ret = cur;
178 [ + + ]: 10832017 : if (childChanged)
179 : : {
180 : 740449 : ret = nm->mkNode(k, children);
181 : : }
182 : 10832017 : if (k == Kind::STRING_LENGTH
183 : 10832017 : && (ret[0].getKind() == Kind::STRING_CONCAT || ret[0].isConst()))
184 : : {
185 : 545426 : Node arg = ret[0];
186 : : // First ensure ACI norm, which ensures that we fully flatten
187 : : // e.g. (len (str.++ (str.++ a b) c)) ---> (len (str.++ a b c)) --->
188 : : // (+ (len a) (len b) (len c)) below.
189 [ + + ]: 545426 : if (arg.getKind() == Kind::STRING_CONCAT)
190 : : {
191 : 170170 : arg = expr::getACINormalForm(arg);
192 [ + + ]: 170170 : if (arg != ret[0])
193 : : {
194 : 58 : Node ret2 = nm->mkNode(k, {arg});
195 [ + + ]: 58 : if (pg != nullptr)
196 : : {
197 : 9 : pg->addRewriteStep(ret,
198 : : ret2,
199 : : nullptr,
200 : : false,
201 : : TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE);
202 : : }
203 : 58 : ret = ret2;
204 : 58 : }
205 : : }
206 : 545426 : std::vector<Node> cc;
207 : 545426 : utils::getConcat(arg, cc);
208 : 545426 : std::vector<Node> sum;
209 [ + + ]: 1471515 : for (const Node& c : cc)
210 : : {
211 [ + + ]: 926089 : if (c.isConst())
212 : : {
213 : 536816 : sum.push_back(nm->mkConstInt(Rational(Word::getLength(c))));
214 : : }
215 : : else
216 : : {
217 : 389273 : sum.push_back(nm->mkNode(Kind::STRING_LENGTH, c));
218 : : }
219 : : }
220 [ - + ][ - + ]: 545426 : Assert(!sum.empty());
[ - - ]
221 [ + + ]: 545426 : Node rret = sum.size() == 1 ? sum[0] : nm->mkNode(Kind::ADD, sum);
222 [ + + ]: 545426 : if (pg != nullptr)
223 : : {
224 : 511 : pg->addRewriteStep(ret,
225 : : rret,
226 : : nullptr,
227 : : false,
228 : : TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE);
229 : : }
230 : 545426 : ret = rret;
231 : 545426 : }
232 : 10832017 : visited[cur] = ret;
233 : 10832017 : }
234 [ + + ]: 33709761 : } while (!visit.empty());
235 [ - + ][ - + ]: 1973355 : Assert(visited.find(n) != visited.end());
[ - - ]
236 [ - + ][ - + ]: 1973355 : Assert(!visited.find(n)->second.isNull());
[ - - ]
237 : 3946710 : return visited[n];
238 : 1973355 : }
239 : :
240 : 47800 : bool ArithEntail::checkEq(Node a, Node b)
241 : : {
242 [ + + ]: 47800 : if (a == b)
243 : : {
244 : 392 : return true;
245 : : }
246 : 47408 : Node ar = rewriteArith(a);
247 : 47408 : Node br = rewriteArith(b);
248 : 47408 : return ar == br;
249 : 47408 : }
250 : :
251 : 1081685 : bool ArithEntail::check(Node a, Node b, bool strict, bool isSimple)
252 : : {
253 [ + + ]: 1081685 : if (a == b)
254 : : {
255 : 65057 : return !strict;
256 : : }
257 : 2033256 : Node diff = NodeManager::mkNode(Kind::SUB, a, b);
258 : 1016628 : return check(diff, strict, isSimple);
259 : 1016628 : }
260 : :
261 : 1674339 : bool ArithEntail::check(Node a, bool strict, bool isSimple)
262 : : {
263 [ + + ]: 1674339 : if (a.isConst())
264 : : {
265 [ + + ]: 176125 : return a.getConst<Rational>().sgn() >= (strict ? 1 : 0);
266 : : }
267 : 2058223 : Node ar = strict ? NodeManager::mkNode(Kind::SUB, a, d_one) : a;
268 [ + + ]: 1498214 : if (isSimple)
269 : : {
270 : 255185 : ar = arith::PolyNorm::getPolyNorm(ar);
271 : : // if simple, just call the checkSimple routine.
272 : 255185 : return checkSimple(ar);
273 : : }
274 : : else
275 : : {
276 : : // otherwise rewrite arith and find approximation
277 : 1243029 : ar = rewriteArith(ar);
278 : : }
279 : 1243029 : Node ara = findApprox(ar, isSimple);
280 : 1243029 : return !ara.isNull();
281 : 1498214 : }
282 : :
283 : 1534023 : Node ArithEntail::findApprox(Node ar, bool isSimple)
284 : : {
285 [ + + ]: 1534023 : std::map<Node, Node>& cache = isSimple ? d_approxCacheSimple : d_approxCache;
286 : 1534023 : std::map<Node, Node>::iterator it = cache.find(ar);
287 [ + + ]: 1534023 : if (it != cache.end())
288 : : {
289 : 1036330 : return it->second;
290 : : }
291 : 497693 : Node ret;
292 [ + + ]: 497693 : if (checkSimple(ar))
293 : : {
294 : : // didn't need approximation
295 : 32266 : ret = ar;
296 : : }
297 : : else
298 : : {
299 : 465427 : ret = findApproxInternal(ar, isSimple);
300 : : }
301 : 497693 : cache[ar] = ret;
302 : 497693 : return ret;
303 : 497693 : }
304 : :
305 : 465427 : Node ArithEntail::findApproxInternal(Node ar, bool isSimple)
306 : : {
307 : : // if not using recursive approximations, we always set isSimple to true
308 [ + + ]: 465427 : if (!d_recApprox)
309 : : {
310 : 411988 : isSimple = true;
311 : : }
312 : 465427 : NodeManager* nm = ar.getNodeManager();
313 : 465427 : std::map<Node, Node> msum;
314 [ + - ]: 930854 : Trace("strings-ent-approx-debug")
315 : 465427 : << "Setup arithmetic approximations for " << ar << std::endl;
316 [ - + ]: 465427 : if (!ArithMSum::getMonomialSum(ar, msum))
317 : : {
318 [ - - ]: 0 : Trace("strings-ent-approx-debug")
319 : 0 : << "...failed to get monomial sum!" << std::endl;
320 : 0 : return Node::null();
321 : : }
322 : : // for each monomial v*c, mApprox[v] a list of
323 : : // possibilities for how the term can be soundly approximated, that is,
324 : : // if mApprox[v] contains av, then v*c > av*c. Notice that if c
325 : : // is positive, then v > av, otherwise if c is negative, then v < av.
326 : : // In other words, av is an under-approximation if c is positive, and an
327 : : // over-approximation if c is negative.
328 : 465427 : bool changed = false;
329 : 465427 : std::map<Node, std::vector<Node> > mApprox;
330 : : // map from approximations to their monomial sums
331 : 465427 : std::map<Node, std::map<Node, Node> > approxMsums;
332 : : // aarSum stores each monomial that does not have multiple approximations
333 : 465427 : std::vector<Node> aarSum;
334 : : // stores the witness
335 : 465427 : arith::ArithSubs approxMap;
336 [ + + ]: 1472382 : for (std::pair<const Node, Node>& m : msum)
337 : : {
338 : 1006955 : Node v = m.first;
339 : 1006955 : Node c = m.second;
340 [ + - ]: 2013910 : Trace("strings-ent-approx-debug")
341 : 1006955 : << "Get approximations " << v << "..." << std::endl;
342 [ + + ]: 1006955 : if (v.isNull())
343 : : {
344 [ - + ][ - + ]: 332661 : Node mn = c.isNull() ? nm->mkConstInt(Rational(1)) : c;
[ - - ]
345 : 332661 : aarSum.push_back(mn);
346 : 332661 : }
347 : : else
348 : : {
349 : : // c.isNull() means c = 1
350 [ + + ][ + + ]: 674294 : bool isOverApprox = !c.isNull() && c.getConst<Rational>().sgn() == -1;
351 : 674294 : std::vector<Node>& approx = mApprox[v];
352 : 674294 : std::unordered_set<Node> visited;
353 : 674294 : std::vector<Node> toProcess;
354 : 674294 : toProcess.push_back(v);
355 : : do
356 : : {
357 : 696464 : Node curr = toProcess.back();
358 [ + - ]: 696464 : Trace("strings-ent-approx-debug") << " process " << curr << std::endl;
359 : 696464 : curr = arith::PolyNorm::getPolyNorm(curr);
360 : 696464 : toProcess.pop_back();
361 [ + + ]: 696464 : if (visited.find(curr) == visited.end())
362 : : {
363 : 695348 : visited.insert(curr);
364 : 695348 : std::vector<Node> currApprox;
365 : 695348 : getArithApproximations(curr, currApprox, isOverApprox, isSimple);
366 [ + + ]: 695348 : if (currApprox.empty())
367 : : {
368 [ + - ]: 1155896 : Trace("strings-ent-approx-debug")
369 : 577948 : << "...approximation: " << curr << std::endl;
370 : : // no approximations, thus curr is a possibility
371 : 577948 : approx.push_back(curr);
372 : : }
373 [ + + ]: 117400 : else if (isSimple)
374 : : {
375 : : // don't rewrite or re-approximate
376 : 104487 : approx = currApprox;
377 : : }
378 : : else
379 : : {
380 : 25826 : toProcess.insert(
381 : 25826 : toProcess.end(), currApprox.begin(), currApprox.end());
382 : : }
383 : 695348 : }
384 [ + + ]: 696464 : } while (!toProcess.empty());
385 [ - + ][ - + ]: 674294 : Assert(!approx.empty());
[ - - ]
386 : : // if we have only one approximation, move it to final
387 [ + + ]: 674294 : if (approx.size() == 1)
388 : : {
389 [ + + ]: 640487 : if (v != approx[0])
390 : : {
391 : 83066 : changed = true;
392 [ + - ]: 166132 : Trace("strings-ent-approx")
393 : 83066 : << "- Propagate (" << (d_rr == nullptr) << ", " << isSimple
394 : 83066 : << ") " << v << " = " << approx[0] << std::endl;
395 : 83066 : approxMap.add(v, approx[0]);
396 : : }
397 : 1280974 : Node mn = ArithMSum::mkCoeffTerm(c, approx[0]);
398 : 640487 : aarSum.push_back(mn);
399 : 640487 : mApprox.erase(v);
400 : 640487 : }
401 : : else
402 : : {
403 : : // compute monomial sum form for each approximation, used below
404 [ + + ]: 101427 : for (const Node& aa : approx)
405 : : {
406 [ + + ]: 67620 : if (approxMsums.find(aa) == approxMsums.end())
407 : : {
408 : : // ensure rewritten, which makes a difference if isSimple is true
409 : 63972 : Node aar = arith::PolyNorm::getPolyNorm(aa);
410 : : CVC5_UNUSED bool ret =
411 : 63972 : ArithMSum::getMonomialSum(aar, approxMsums[aa]);
412 : 63972 : Assert(ret) << "Could not find sum " << aa;
413 : 63972 : }
414 : : }
415 : 33807 : changed = true;
416 : : }
417 : 674294 : }
418 : 1006955 : }
419 [ + + ]: 465427 : if (!changed)
420 : : {
421 : : // approximations had no effect, return
422 [ + - ]: 365020 : Trace("strings-ent-approx-debug") << "...no approximations" << std::endl;
423 : 365020 : return Node::null();
424 : : }
425 : : // get the current "fixed" sum for the abstraction of ar
426 : : Node aar =
427 : 100407 : aarSum.empty()
428 : 5609 : ? d_zero
429 [ + + ][ + + ]: 100407 : : (aarSum.size() == 1 ? aarSum[0] : nm->mkNode(Kind::ADD, aarSum));
430 : 100407 : aar = arith::PolyNorm::getPolyNorm(aar);
431 [ + - ]: 200814 : Trace("strings-ent-approx-debug")
432 : 100407 : << "...processed fixed sum " << aar << " with " << mApprox.size()
433 : 100407 : << " approximated monomials." << std::endl;
434 : : // if we have a choice of how to approximate
435 [ + + ]: 100407 : if (!mApprox.empty())
436 : : {
437 : : // convert aar back to monomial sum
438 : 32706 : std::map<Node, Node> msumAar;
439 [ - + ]: 32706 : if (!ArithMSum::getMonomialSum(aar, msumAar))
440 : : {
441 : 0 : return Node::null();
442 : : }
443 [ - + ]: 32706 : if (TraceIsOn("strings-ent-approx"))
444 : : {
445 [ - - ]: 0 : Trace("strings-ent-approx")
446 : 0 : << "---- Check arithmetic entailment by under-approximation " << ar
447 : 0 : << " >= 0" << std::endl;
448 [ - - ]: 0 : Trace("strings-ent-approx") << "FIXED:" << std::endl;
449 : 0 : ArithMSum::debugPrintMonomialSum(msumAar, "strings-ent-approx");
450 [ - - ]: 0 : Trace("strings-ent-approx") << "APPROX:" << std::endl;
451 [ - - ]: 0 : for (std::pair<const Node, std::vector<Node> >& a : mApprox)
452 : : {
453 : 0 : Node c = msum[a.first];
454 [ - - ]: 0 : Trace("strings-ent-approx") << " ";
455 [ - - ]: 0 : if (!c.isNull())
456 : : {
457 [ - - ]: 0 : Trace("strings-ent-approx") << c << " * ";
458 : : }
459 [ - - ]: 0 : Trace("strings-ent-approx")
460 : 0 : << a.second << " ...from " << a.first << std::endl;
461 : 0 : }
462 [ - - ]: 0 : Trace("strings-ent-approx") << std::endl;
463 : : }
464 : 32706 : Rational one(1);
465 : : // incorporate monomials one at a time that have a choice of approximations
466 [ + + ]: 66513 : while (!mApprox.empty())
467 : : {
468 : 33807 : Node v;
469 : 33807 : Node vapprox;
470 : 33807 : int maxScore = -1;
471 : : // Look at each approximation, take the one with the best score.
472 : : // Notice that we are in the process of trying to prove
473 : : // ( c1*t1 + .. + cn*tn ) + ( approx_1 | ... | approx_m ) >= 0,
474 : : // where c1*t1 + .. + cn*tn is the "fixed" component of our sum (aar)
475 : : // and approx_1 ... approx_m are possible approximations. The
476 : : // intution here is that we want coefficients c1...cn to be positive.
477 : : // This is because arithmetic string terms t1...tn (which may be
478 : : // applications of len, indexof, str.to.int) are never entailed to be
479 : : // negative. Hence, we add the approx_i that contributes the "most"
480 : : // towards making all constants c1...cn positive and cancelling negative
481 : : // monomials in approx_i itself.
482 [ + - ]: 33807 : for (std::pair<const Node, std::vector<Node> >& nam : mApprox)
483 : : {
484 : 33807 : Node cr = msum[nam.first];
485 [ + + ]: 101427 : for (const Node& aa : nam.second)
486 : : {
487 : 67620 : unsigned helpsCancelCount = 0;
488 : 67620 : unsigned addsObligationCount = 0;
489 : 67620 : std::map<Node, Node>::iterator it;
490 : : // we are processing an approximation cr*( c1*t1 + ... + cn*tn )
491 [ + + ]: 148736 : for (std::pair<const Node, Node>& aam : approxMsums[aa])
492 : : {
493 : : // Say aar is of the form t + c*ti, and aam is the monomial ci*ti
494 : : // where ci != 0. We say aam:
495 : : // (1) helps cancel if c != 0 and c>0 != ci>0
496 : : // (2) adds obligation if c>=0 and c+ci<0
497 : 81116 : Node ti = aam.first;
498 : 81116 : Node ci = aam.second;
499 [ + + ]: 81116 : if (!cr.isNull())
500 : : {
501 [ + + ]: 167534 : ci = ci.isNull() ? cr
502 : 54980 : : nm->mkConstInt(cr.getConst<Rational>()
503 [ + + ][ - - ]: 167534 : * ci.getConst<Rational>());
504 : : }
505 [ + - ]: 81116 : Trace("strings-ent-approx-debug") << ci << "*" << ti << " ";
506 [ + + ]: 81116 : int ciSgn = ci.isNull() ? 1 : ci.getConst<Rational>().sgn();
507 : 81116 : it = msumAar.find(ti);
508 [ + + ]: 81116 : if (it != msumAar.end())
509 : : {
510 : 32875 : Node c = it->second;
511 [ + + ]: 32875 : int cSgn = c.isNull() ? 1 : c.getConst<Rational>().sgn();
512 [ + + ]: 32875 : if (cSgn == 0)
513 : : {
514 [ + - ]: 4847 : addsObligationCount += (ciSgn == -1 ? 1 : 0);
515 : : }
516 [ + + ]: 28028 : else if (cSgn != ciSgn)
517 : : {
518 : 17683 : helpsCancelCount++;
519 [ + + ]: 17683 : Rational r1 = c.isNull() ? one : c.getConst<Rational>();
520 [ + + ]: 17683 : Rational r2 = ci.isNull() ? one : ci.getConst<Rational>();
521 : 17683 : Rational r12 = r1 + r2;
522 [ + + ]: 17683 : if (r12.sgn() == -1)
523 : : {
524 : 6574 : addsObligationCount++;
525 : : }
526 : 17683 : }
527 : 32875 : }
528 : : else
529 : : {
530 [ + + ]: 48241 : addsObligationCount += (ciSgn == -1 ? 1 : 0);
531 : : }
532 : 81116 : }
533 [ + - ]: 135240 : Trace("strings-ent-approx-debug")
534 : 0 : << "counts=" << helpsCancelCount << "," << addsObligationCount
535 : 67620 : << " for " << aa << " into " << aar << std::endl;
536 [ + + ]: 67620 : int score = (addsObligationCount > 0 ? 0 : 2)
537 [ + + ]: 67620 : + (helpsCancelCount > 0 ? 1 : 0);
538 : : // if its the best, update v and vapprox
539 [ + + ][ + + ]: 67620 : if (v.isNull() || score > maxScore)
[ + + ]
540 : : {
541 : 40504 : v = nam.first;
542 : 40504 : vapprox = aa;
543 : 40504 : maxScore = score;
544 : : }
545 : : }
546 [ + - ]: 33807 : if (!v.isNull())
547 : : {
548 : 33807 : break;
549 : : }
550 [ - + ]: 33807 : }
551 [ + - ]: 67614 : Trace("strings-ent-approx") << "- Decide (" << (d_rr == nullptr) << ") "
552 : 33807 : << v << " = " << vapprox << std::endl;
553 : : // we incorporate v approximated by vapprox into the overall approximation
554 : : // for ar
555 [ + - ][ + - ]: 33807 : Assert(!v.isNull() && !vapprox.isNull());
[ - + ][ - + ]
[ - - ]
556 [ - + ][ - + ]: 33807 : Assert(msum.find(v) != msum.end());
[ - - ]
557 : 67614 : Node mn = ArithMSum::mkCoeffTerm(msum[v], vapprox);
558 : 33807 : aar = nm->mkNode(Kind::ADD, aar, mn);
559 : 33807 : approxMap.add(v, vapprox);
560 : : // update the msumAar map
561 : 33807 : aar = arith::PolyNorm::getPolyNorm(aar);
562 : 33807 : msumAar.clear();
563 [ - + ]: 33807 : if (!ArithMSum::getMonomialSum(aar, msumAar))
564 : : {
565 : 0 : DebugUnhandled();
566 : : Trace("strings-ent-approx")
567 : : << "...failed to get monomial sum!" << std::endl;
568 : : return Node::null();
569 : : }
570 : : // we have processed the approximation for v
571 : 33807 : mApprox.erase(v);
572 [ + - ][ + - ]: 33807 : }
[ + - ]
573 [ + - ]: 32706 : Trace("strings-ent-approx") << "-----------------" << std::endl;
574 [ + - ][ + - ]: 32706 : }
575 [ - + ]: 100407 : if (aar == ar)
576 : : {
577 [ - - ]: 0 : Trace("strings-ent-approx-debug")
578 : 0 : << "...approximation had no effect" << std::endl;
579 : : // this should never happen, but we avoid the infinite loop for sanity here
580 : 0 : DebugUnhandled();
581 : : return Node::null();
582 : : }
583 : : // Check entailment on the approximation of ar.
584 : : // Notice that this may trigger further reasoning by approximation. For
585 : : // example, len( replace( x ++ y, substr( x, 0, n ), z ) ) may be
586 : : // under-approximated as len( x ) + len( y ) - len( substr( x, 0, n ) ) on
587 : : // this call, where in the recursive call we may over-approximate
588 : : // len( substr( x, 0, n ) ) as len( x ). In this example, we can infer
589 : : // that len( replace( x ++ y, substr( x, 0, n ), z ) ) >= len( y ) in two
590 : : // steps.
591 [ + + ]: 100407 : if (check(aar, false, isSimple))
592 : : {
593 [ + - ]: 13634 : Trace("strings-ent-approx")
594 : 0 : << "*** StrArithApprox: showed " << ar
595 : 6817 : << " >= 0 using under-approximation!" << std::endl;
596 [ + - ]: 13634 : Trace("strings-ent-approx")
597 : 6817 : << "*** StrArithApprox: rewritten was " << aar << std::endl;
598 : : // Apply arithmetic substitution, which ensures we only replace terms
599 : : // in the top-level arithmetic skeleton of ar.
600 : 6817 : Node approx = approxMap.applyArith(ar);
601 [ + - ]: 13634 : Trace("strings-ent-approx")
602 : 0 : << "*** StrArithApprox: under-approximation was " << approx
603 : 6817 : << std::endl;
604 : 6817 : return approx;
605 : 6817 : }
606 : 93590 : return Node::null();
607 : 465427 : }
608 : :
609 : 695354 : void ArithEntail::getArithApproximations(Node a,
610 : : std::vector<Node>& approx,
611 : : bool isOverApprox,
612 : : bool isSimple)
613 : : {
614 : 695354 : NodeManager* nm = a.getNodeManager();
615 : : // We do not handle ADD here since this leads to exponential behavior.
616 : : // Instead, this is managed, e.g. during checkApprox, where
617 : : // ADD terms are expanded "on-demand" during the reasoning.
618 [ + - ]: 1390708 : Trace("strings-ent-approx-debug")
619 : 695354 : << "Get arith approximations " << a << std::endl;
620 : 695354 : Kind ak = a.getKind();
621 [ + + ]: 695354 : if (ak == Kind::MULT)
622 : : {
623 : 1009 : Node c;
624 : 1009 : Node v;
625 [ + + ]: 1009 : if (ArithMSum::getMonomial(a, c, v))
626 : : {
627 : 6 : bool isNeg = c.getConst<Rational>().sgn() == -1;
628 [ - + ]: 12 : getArithApproximations(
629 : 0 : v, approx, isNeg ? !isOverApprox : isOverApprox, isSimple);
630 [ - + ]: 6 : for (unsigned i = 0, size = approx.size(); i < size; i++)
631 : : {
632 : 0 : approx[i] = nm->mkNode(Kind::MULT, c, approx[i]);
633 : : }
634 : : }
635 : 1009 : }
636 [ + + ]: 694345 : else if (ak == Kind::STRING_LENGTH)
637 : : {
638 : 507229 : Kind aak = a[0].getKind();
639 [ + + ]: 507229 : if (aak == Kind::STRING_SUBSTR)
640 : : {
641 : : // over,under-approximations for len( substr( x, n, m ) )
642 : 197352 : Node lenx = nm->mkNode(Kind::STRING_LENGTH, a[0][0]);
643 [ + + ]: 98676 : if (isOverApprox)
644 : : {
645 : : // m >= 0 implies
646 : : // m >= len( substr( x, n, m ) )
647 [ + + ]: 54866 : if (check(a[0][2], false, isSimple))
648 : : {
649 : 32105 : approx.push_back(a[0][2]);
650 : : }
651 [ + + ]: 54866 : if (check(lenx, a[0][1], false, isSimple))
652 : : {
653 : : // n <= len( x ) implies
654 : : // len( x ) - n >= len( substr( x, n, m ) )
655 : 24613 : approx.push_back(nm->mkNode(Kind::SUB, lenx, a[0][1]));
656 : : }
657 : : else
658 : : {
659 : : // len( x ) >= len( substr( x, n, m ) )
660 : 30253 : approx.push_back(lenx);
661 : : }
662 : : }
663 : : else
664 : : {
665 : : // 0 <= n and n+m <= len( x ) implies
666 : : // m <= len( substr( x, n, m ) )
667 : 87620 : Node npm = nm->mkNode(Kind::ADD, a[0][1], a[0][2]);
668 : 87620 : if (check(a[0][1], false, isSimple)
669 : 87620 : && check(lenx, npm, false, isSimple))
670 : : {
671 : 5278 : approx.push_back(a[0][2]);
672 : : }
673 : : // 0 <= n and n+m >= len( x ) implies
674 : : // len(x)-n <= len( substr( x, n, m ) )
675 : 87620 : if (check(a[0][1], false, isSimple)
676 : 87620 : && check(npm, lenx, false, isSimple))
677 : : {
678 : 4147 : approx.push_back(nm->mkNode(Kind::SUB, lenx, a[0][1]));
679 : : }
680 : 43810 : }
681 : 98676 : }
682 [ + + ]: 408553 : else if (aak == Kind::STRING_REPLACE)
683 : : {
684 : : // over,under-approximations for len( replace( x, y, z ) )
685 : : // notice this is either len( x ) or ( len( x ) + len( z ) - len( y ) )
686 : 39494 : Node lenx = nm->mkNode(Kind::STRING_LENGTH, a[0][0]);
687 : 39494 : Node leny = nm->mkNode(Kind::STRING_LENGTH, a[0][1]);
688 : 39494 : Node lenz = nm->mkNode(Kind::STRING_LENGTH, a[0][2]);
689 [ + + ]: 19747 : if (isOverApprox)
690 : : {
691 [ + + ]: 9844 : if (check(leny, lenz, false, isSimple))
692 : : {
693 : : // len( y ) >= len( z ) implies
694 : : // len( x ) >= len( replace( x, y, z ) )
695 : 5 : approx.push_back(lenx);
696 : : }
697 : : else
698 : : {
699 : : // len( x ) + len( z ) >= len( replace( x, y, z ) )
700 : 9839 : approx.push_back(nm->mkNode(Kind::ADD, lenx, lenz));
701 : : }
702 : : }
703 : : else
704 : : {
705 [ + - ][ + + ]: 9903 : if (check(lenz, leny, false, isSimple)
[ - - ][ - - ]
706 : 9903 : || check(lenz, lenx, false, isSimple))
707 : : {
708 : : // len( y ) <= len( z ) or len( x ) <= len( z ) implies
709 : : // len( x ) <= len( replace( x, y, z ) )
710 : 2566 : approx.push_back(lenx);
711 : : }
712 : : else
713 : : {
714 : : // len( x ) - len( y ) <= len( replace( x, y, z ) )
715 : 7337 : approx.push_back(nm->mkNode(Kind::SUB, lenx, leny));
716 : : }
717 : : }
718 : 19747 : }
719 [ + + ]: 388806 : else if (aak == Kind::STRING_ITOS)
720 : : {
721 : : // over,under-approximations for len( int.to.str( x ) )
722 [ + + ]: 5215 : if (isOverApprox)
723 : : {
724 [ + + ]: 2610 : if (check(a[0][0], false, isSimple))
725 : : {
726 [ + + ]: 1336 : if (check(a[0][0], true, isSimple))
727 : : {
728 : : // x > 0 implies
729 : : // x >= len( int.to.str( x ) )
730 : 14 : approx.push_back(a[0][0]);
731 : : }
732 : : else
733 : : {
734 : : // x >= 0 implies
735 : : // x+1 >= len( int.to.str( x ) )
736 : 1322 : approx.push_back(
737 : 2644 : nm->mkNode(Kind::ADD, nm->mkConstInt(Rational(1)), a[0][0]));
738 : : }
739 : : }
740 : : }
741 : : else
742 : : {
743 [ + + ]: 2605 : if (check(a[0][0], false, isSimple))
744 : : {
745 : : // x >= 0 implies
746 : : // len( int.to.str( x ) ) >= 1
747 : 1454 : approx.push_back(nm->mkConstInt(Rational(1)));
748 : : }
749 : : // other crazy things are possible here, e.g.
750 : : // len( int.to.str( len( y ) + 10 ) ) >= 2
751 : : }
752 : : }
753 : : }
754 [ + + ]: 187116 : else if (ak == Kind::STRING_INDEXOF)
755 : : {
756 : : // over,under-approximations for indexof( x, y, n )
757 [ + + ]: 33155 : if (isOverApprox)
758 : : {
759 : 32386 : Node lenx = nm->mkNode(Kind::STRING_LENGTH, a[0]);
760 : 32386 : Node leny = nm->mkNode(Kind::STRING_LENGTH, a[1]);
761 [ + + ]: 16193 : if (check(lenx, leny, false, isSimple))
762 : : {
763 : : // len( x ) >= len( y ) implies
764 : : // len( x ) - len( y ) >= indexof( x, y, n )
765 : 1744 : approx.push_back(nm->mkNode(Kind::SUB, lenx, leny));
766 : : }
767 : : else
768 : : {
769 : : // len( x ) >= indexof( x, y, n )
770 : 14449 : approx.push_back(lenx);
771 : : }
772 : 16193 : }
773 : : else
774 : : {
775 : : // TODO?:
776 : : // contains( substr( x, n, len( x ) ), y ) implies
777 : : // n <= indexof( x, y, n )
778 : : // ...hard to test, runs risk of non-termination
779 : :
780 : : // -1 <= indexof( x, y, n )
781 : 16962 : approx.push_back(nm->mkConstInt(Rational(-1)));
782 : : }
783 : : }
784 [ + + ]: 153961 : else if (ak == Kind::STRING_STOI)
785 : : {
786 : : // over,under-approximations for str.to.int( x )
787 [ + + ]: 476 : if (isOverApprox)
788 : : {
789 : : // TODO?:
790 : : // y >= 0 implies
791 : : // y >= str.to.int( int.to.str( y ) )
792 : : }
793 : : else
794 : : {
795 : : // -1 <= str.to.int( x )
796 : 241 : approx.push_back(nm->mkConstInt(Rational(-1)));
797 : : }
798 : : }
799 [ + - ]: 1390708 : Trace("strings-ent-approx-debug")
800 : 695354 : << "Return " << approx.size() << " approximations" << std::endl;
801 : 695360 : }
802 : :
803 : 3845 : bool ArithEntail::checkWithEqAssumption(Node assumption, Node a, bool strict)
804 : : {
805 [ - + ][ - + ]: 3845 : Assert(assumption.getKind() == Kind::EQUAL);
[ - - ]
806 [ + - ]: 7690 : Trace("strings-entail") << "checkWithEqAssumption: " << assumption << " " << a
807 : 3845 : << ", strict=" << strict << std::endl;
808 : :
809 : : // Find candidates variables to compute substitutions for
810 : 3845 : std::unordered_set<Node> candVars;
811 : 11535 : std::vector<Node> toVisit = {assumption};
812 [ + + ]: 26203 : while (!toVisit.empty())
813 : : {
814 : 22358 : Node curr = toVisit.back();
815 : 22358 : toVisit.pop_back();
816 : :
817 [ + + ]: 40683 : if (curr.getKind() == Kind::ADD || curr.getKind() == Kind::MULT
818 [ + + ][ + + ]: 40683 : || curr.getKind() == Kind::SUB || curr.getKind() == Kind::EQUAL)
[ + + ][ + + ]
819 : : {
820 [ + + ]: 27769 : for (const auto& currChild : curr)
821 : : {
822 : 18513 : toVisit.push_back(currChild);
823 : 18513 : }
824 : : }
825 [ + + ][ + - ]: 13102 : else if (curr.isVar() && Theory::theoryOf(curr) == THEORY_ARITH)
[ + + ][ + + ]
[ - - ]
826 : : {
827 : 3017 : candVars.insert(curr);
828 : : }
829 [ + + ]: 10085 : else if (curr.getKind() == Kind::STRING_LENGTH)
830 : : {
831 : 4522 : candVars.insert(curr);
832 : : }
833 : 22358 : }
834 : :
835 : : // Check if any of the candidate variables are in n
836 : 3845 : Node v;
837 [ - + ][ - + ]: 3845 : Assert(toVisit.empty());
[ - - ]
838 : 3845 : toVisit.push_back(a);
839 [ + + ]: 16615 : while (!toVisit.empty())
840 : : {
841 : 12926 : Node curr = toVisit.back();
842 : 12926 : toVisit.pop_back();
843 : :
844 [ + + ]: 22353 : for (const auto& currChild : curr)
845 : : {
846 : 9427 : toVisit.push_back(currChild);
847 : 9427 : }
848 : :
849 [ + + ]: 12926 : if (candVars.find(curr) != candVars.end())
850 : : {
851 : 156 : v = curr;
852 : 156 : break;
853 : : }
854 [ + + ]: 12926 : }
855 : :
856 [ + + ]: 3845 : if (v.isNull())
857 : : {
858 : : // No suitable candidate found
859 : 3689 : return false;
860 : : }
861 : :
862 : 312 : Node solution = ArithMSum::solveEqualityFor(assumption, v);
863 [ + + ]: 156 : if (solution.isNull())
864 : : {
865 : : // Could not solve for v
866 : 9 : return false;
867 : : }
868 [ + - ]: 294 : Trace("strings-entail") << "checkWithEqAssumption: subs " << v << " -> "
869 : 147 : << solution << std::endl;
870 : :
871 : 147 : TNode tv = v;
872 : 147 : TNode tsolution = solution;
873 : 147 : a = a.substitute(tv, tsolution);
874 : 147 : return check(a, strict);
875 : 3845 : }
876 : :
877 : 7070 : bool ArithEntail::checkWithAssumption(Node assumption,
878 : : Node a,
879 : : Node b,
880 : : bool strict)
881 : : {
882 : 7070 : NodeManager* nm = assumption.getNodeManager();
883 : :
884 [ + + ][ + + ]: 7070 : if (!assumption.isConst() && assumption.getKind() != Kind::EQUAL)
[ + + ]
885 : : {
886 : : // We rewrite inequality assumptions from x <= y to x + (str.len s) = y
887 : : // where s is some fresh string variable. We use (str.len s) because
888 : : // (str.len s) must be non-negative for the equation to hold.
889 : 3841 : Node x, y;
890 [ + + ]: 3841 : if (assumption.getKind() == Kind::GEQ)
891 : : {
892 : 2651 : x = assumption[0];
893 : 2651 : y = assumption[1];
894 : : }
895 : : else
896 : : {
897 : : // (not (>= s t)) --> (>= (t - 1) s)
898 : 1190 : Assert(assumption.getKind() == Kind::NOT
899 : : && assumption[0].getKind() == Kind::GEQ);
900 : 1190 : x = nm->mkNode(Kind::SUB, assumption[0][1], nm->mkConstInt(Rational(1)));
901 : 1190 : y = assumption[0][0];
902 : : }
903 : :
904 : 7682 : Node s = NodeManager::mkBoundVar("slackVal", nm->stringType());
905 : 3841 : Node slen = nm->mkNode(Kind::STRING_LENGTH, s);
906 : 7682 : Node sleny = nm->mkNode(Kind::ADD, y, slen);
907 : 7682 : Node rr = rewriteArith(nm->mkNode(Kind::SUB, x, sleny));
908 [ - + ]: 3841 : if (rr.isConst())
909 : : {
910 : 0 : assumption = nm->mkConst(rr.getConst<Rational>().sgn() == 0);
911 : : }
912 : : else
913 : : {
914 : 3841 : assumption = nm->mkNode(Kind::EQUAL, x, sleny);
915 : : }
916 : 3841 : }
917 : :
918 : 14140 : Node diff = nm->mkNode(Kind::SUB, a, b);
919 : 7070 : bool res = false;
920 [ + + ]: 7070 : if (assumption.isConst())
921 : : {
922 : 3225 : bool assumptionBool = assumption.getConst<bool>();
923 [ + - ]: 3225 : if (assumptionBool)
924 : : {
925 : 3225 : res = check(diff, strict);
926 : : }
927 : : else
928 : : {
929 : 0 : res = true;
930 : : }
931 : : }
932 : : else
933 : : {
934 : 3845 : res = checkWithEqAssumption(assumption, diff, strict);
935 : : }
936 : 7070 : return res;
937 : 7070 : }
938 : :
939 : 0 : bool ArithEntail::checkWithAssumptions(std::vector<Node> assumptions,
940 : : Node a,
941 : : Node b,
942 : : bool strict)
943 : : {
944 : : // TODO: We currently try to show the entailment with each assumption
945 : : // independently. In the future, we should make better use of multiple
946 : : // assumptions.
947 : 0 : bool res = false;
948 [ - - ]: 0 : for (const auto& assumption : assumptions)
949 : : {
950 [ - - ]: 0 : if (checkWithAssumption(assumption, a, b, strict))
951 : : {
952 : 0 : res = true;
953 : 0 : break;
954 : : }
955 : : }
956 : 0 : return res;
957 : : }
958 : :
959 : : struct ArithEntailConstantBoundLowerId
960 : : {
961 : : };
962 : : typedef expr::Attribute<ArithEntailConstantBoundLowerId, Node>
963 : : ArithEntailConstantBoundLower;
964 : :
965 : : struct ArithEntailConstantBoundUpperId
966 : : {
967 : : };
968 : : typedef expr::Attribute<ArithEntailConstantBoundUpperId, Node>
969 : : ArithEntailConstantBoundUpper;
970 : :
971 : 89766 : void ArithEntail::setConstantBoundCache(TNode n, Node ret, bool isLower)
972 : : {
973 [ + + ]: 89766 : if (isLower)
974 : : {
975 : : ArithEntailConstantBoundLower acbl;
976 : 49203 : n.setAttribute(acbl, ret);
977 : : }
978 : : else
979 : : {
980 : : ArithEntailConstantBoundUpper acbu;
981 : 40563 : n.setAttribute(acbu, ret);
982 : : }
983 : 89766 : }
984 : :
985 : 1183721 : bool ArithEntail::getConstantBoundCache(TNode n, bool isLower, Node& c)
986 : : {
987 [ + + ]: 1183721 : if (isLower)
988 : : {
989 : : ArithEntailConstantBoundLower acbl;
990 [ + + ]: 1078686 : if (n.hasAttribute(acbl))
991 : : {
992 : 1029483 : c = n.getAttribute(acbl);
993 : 1029483 : return true;
994 : : }
995 : : }
996 : : else
997 : : {
998 : : ArithEntailConstantBoundUpper acbu;
999 [ + + ]: 105035 : if (n.hasAttribute(acbu))
1000 : : {
1001 : 64472 : c = n.getAttribute(acbu);
1002 : 64472 : return true;
1003 : : }
1004 : : }
1005 : 89766 : return false;
1006 : : }
1007 : :
1008 : 53847 : Node ArithEntail::getConstantBound(TNode a, bool isLower)
1009 : : {
1010 [ - + ][ - + ]: 53847 : Assert(rewriteArith(a) == a);
[ - - ]
1011 : 53847 : Node ret;
1012 [ + + ]: 53847 : if (getConstantBoundCache(a, isLower, ret))
1013 : : {
1014 : 45207 : return ret;
1015 : : }
1016 [ + + ]: 8640 : if (a.isConst())
1017 : : {
1018 : 1892 : ret = a;
1019 : : }
1020 [ + + ]: 6748 : else if (a.getKind() == Kind::STRING_LENGTH)
1021 : : {
1022 [ + - ]: 1145 : if (isLower)
1023 : : {
1024 : 1145 : ret = d_zero;
1025 : : }
1026 : : }
1027 [ + + ][ + + ]: 5603 : else if (a.getKind() == Kind::ADD || a.getKind() == Kind::MULT)
[ + + ]
1028 : : {
1029 : 4628 : std::vector<Node> children;
1030 : 4628 : bool success = true;
1031 [ + + ]: 8793 : for (unsigned i = 0; i < a.getNumChildren(); i++)
1032 : : {
1033 : 7889 : Node ac = getConstantBound(a[i], isLower);
1034 [ + + ]: 7889 : if (ac.isNull())
1035 : : {
1036 : 2473 : success = false;
1037 : 2473 : break;
1038 : : }
1039 : : else
1040 : : {
1041 [ + + ]: 5416 : if (ac.getConst<Rational>().sgn() == 0)
1042 : : {
1043 [ + + ]: 1675 : if (a.getKind() == Kind::MULT)
1044 : : {
1045 : 27 : success = false;
1046 : 27 : break;
1047 : : }
1048 : : }
1049 : : else
1050 : : {
1051 [ + + ]: 3741 : if (a.getKind() == Kind::MULT)
1052 : : {
1053 [ + + ]: 1253 : if ((ac.getConst<Rational>().sgn() > 0) != isLower)
1054 : : {
1055 : 1224 : success = false;
1056 : 1224 : break;
1057 : : }
1058 : : }
1059 : 2517 : children.push_back(ac);
1060 : : }
1061 : : }
1062 [ + + ]: 7889 : }
1063 [ + + ]: 4628 : if (success)
1064 : : {
1065 [ + + ]: 904 : if (children.empty())
1066 : : {
1067 : 310 : ret = d_zero;
1068 : : }
1069 [ + - ]: 594 : else if (children.size() == 1)
1070 : : {
1071 : 594 : ret = children[0];
1072 : : }
1073 : : else
1074 : : {
1075 : 0 : ret = a.getNodeManager()->mkNode(a.getKind(), children);
1076 : 0 : ret = rewriteArith(ret);
1077 : : }
1078 : : }
1079 : 4628 : }
1080 [ + - ]: 17280 : Trace("strings-rewrite-cbound")
1081 [ - - ]: 0 : << "Constant " << (isLower ? "lower" : "upper") << " bound for " << a
1082 : 8640 : << " is " << ret << std::endl;
1083 [ + + ][ + - ]: 8640 : Assert(ret.isNull() || ret.isConst());
[ - + ][ - + ]
[ - - ]
1084 : : // entailment check should be at least as powerful as computing a lower bound
1085 : 8640 : Assert(!isLower || ret.isNull() || ret.getConst<Rational>().sgn() < 0
1086 : : || check(a, false));
1087 : 8640 : Assert(!isLower || ret.isNull() || ret.getConst<Rational>().sgn() <= 0
1088 : : || check(a, true));
1089 : : // cache
1090 : 8640 : setConstantBoundCache(a, ret, isLower);
1091 : 8640 : return ret;
1092 : 0 : }
1093 : :
1094 : 1129874 : Node ArithEntail::getConstantBoundLength(TNode s, bool isLower) const
1095 : : {
1096 [ - + ][ - + ]: 1129874 : Assert(s.getType().isStringLike());
[ - - ]
1097 : 1129874 : Node ret;
1098 [ + + ]: 1129874 : if (getConstantBoundCache(s, isLower, ret))
1099 : : {
1100 : 1048748 : return ret;
1101 : : }
1102 : 81126 : NodeManager* nm = s.getNodeManager();
1103 : 81126 : Kind sk = s.getKind();
1104 [ + + ]: 81126 : if (s.isConst())
1105 : : {
1106 : 13752 : size_t len = Word::getLength(s);
1107 : 13752 : ret = nm->mkConstInt(Rational(len));
1108 : : }
1109 [ + + ][ - + ]: 67374 : else if (sk == Kind::SEQ_UNIT || sk == Kind::STRING_UNIT)
1110 : : {
1111 : 1174 : ret = nm->mkConstInt(1);
1112 : : }
1113 [ + + ]: 66200 : else if (sk == Kind::STRING_CONCAT)
1114 : : {
1115 : 26104 : Rational sum(0);
1116 : 26104 : bool success = true;
1117 [ + + ]: 60361 : for (const Node& sc : s)
1118 : : {
1119 : 47293 : Node b = getConstantBoundLength(sc, isLower);
1120 [ + + ]: 47293 : if (b.isNull())
1121 : : {
1122 [ - + ]: 13036 : if (isLower)
1123 : : {
1124 : : // assume zero and continue
1125 : 0 : continue;
1126 : : }
1127 : 13036 : success = false;
1128 : 13036 : break;
1129 : : }
1130 [ - + ][ - + ]: 34257 : Assert(b.isConst());
[ - - ]
1131 : 34257 : sum = sum + b.getConst<Rational>();
1132 [ + - ][ + + ]: 60329 : }
[ - + ]
1133 [ + + ][ + + ]: 26104 : if (success && (!isLower || sum.sgn() != 0))
[ + + ][ + + ]
1134 : : {
1135 : 5658 : ret = nm->mkConstInt(sum);
1136 : : }
1137 : 26104 : }
1138 [ + + ][ + + ]: 81126 : if (ret.isNull() && isLower)
[ + + ]
1139 : : {
1140 : 27458 : ret = d_zero;
1141 : : }
1142 : : // cache
1143 : 81126 : setConstantBoundCache(s, ret, isLower);
1144 : 81126 : return ret;
1145 : 0 : }
1146 : :
1147 : 1865471 : bool ArithEntail::checkSimple(Node a)
1148 : : {
1149 : : // check whether a >= 0
1150 [ + + ]: 1865471 : if (a.isConst())
1151 : : {
1152 : 741422 : return a.getConst<Rational>().sgn() >= 0;
1153 : : }
1154 [ + + ]: 1124049 : else if (a.getKind() == Kind::STRING_LENGTH)
1155 : : {
1156 : : // str.len( t ) >= 0
1157 : 185845 : return true;
1158 : : }
1159 [ + + ][ + + ]: 938204 : else if (a.getKind() == Kind::ADD || a.getKind() == Kind::MULT)
[ + + ]
1160 : : {
1161 [ + + ]: 1130063 : for (unsigned i = 0; i < a.getNumChildren(); i++)
1162 : : {
1163 [ + + ]: 1112451 : if (!checkSimple(a[i]))
1164 : : {
1165 : 854550 : return false;
1166 : : }
1167 : : }
1168 : : // t1 >= 0 ^ ... ^ tn >= 0 => t1 op ... op tn >= 0
1169 : 17612 : return true;
1170 : : }
1171 : :
1172 : 66042 : return false;
1173 : : }
1174 : :
1175 : 1892 : bool ArithEntail::inferZerosInSumGeq(Node x,
1176 : : std::vector<Node>& ys,
1177 : : std::vector<Node>& zeroYs)
1178 : : {
1179 [ - + ][ - + ]: 1892 : Assert(zeroYs.empty());
[ - - ]
1180 : :
1181 : 1892 : NodeManager* nm = x.getNodeManager();
1182 : :
1183 : : // Check if we can show that y1 + ... + yn >= x
1184 [ + + ]: 1892 : Node sum = (ys.size() > 1) ? nm->mkNode(Kind::ADD, ys) : ys[0];
1185 [ + + ]: 1892 : if (!check(sum, x))
1186 : : {
1187 : 1696 : return false;
1188 : : }
1189 : :
1190 : : // Try to remove yi one-by-one and check if we can still show:
1191 : : //
1192 : : // y1 + ... + yi-1 + yi+1 + ... + yn >= x
1193 : : //
1194 : : // If that's the case, we know that yi can be zero and the inequality still
1195 : : // holds.
1196 : 196 : size_t i = 0;
1197 [ + + ]: 803 : while (i < ys.size())
1198 : : {
1199 : 607 : Node yi = ys[i];
1200 : 607 : std::vector<Node>::iterator pos = ys.erase(ys.begin() + i);
1201 [ + + ]: 607 : if (ys.size() > 1)
1202 : : {
1203 : 313 : sum = nm->mkNode(Kind::ADD, ys);
1204 : : }
1205 : : else
1206 : : {
1207 [ + + ]: 294 : sum = ys.size() == 1 ? ys[0] : d_zero;
1208 : : }
1209 : :
1210 [ + + ]: 607 : if (check(sum, x))
1211 : : {
1212 : 117 : zeroYs.push_back(yi);
1213 : : }
1214 : : else
1215 : : {
1216 : 490 : ys.insert(pos, yi);
1217 : 490 : i++;
1218 : : }
1219 : 607 : }
1220 : 196 : return true;
1221 : 1892 : }
1222 : :
1223 : : } // namespace strings
1224 : : } // namespace theory
1225 : : } // namespace cvc5::internal
|
