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 : 380167 : ArithEntail::ArithEntail(NodeManager* nm, Rewriter* r, bool recApprox)
35 : 380167 : : d_rr(r), d_recApprox(recApprox)
36 : : {
37 : 380167 : d_one = nm->mkConstInt(Rational(1));
38 : 380167 : d_zero = nm->mkConstInt(Rational(0));
39 : 380167 : }
40 : :
41 : 106541 : Node ArithEntail::rewritePredViaEntailment(const Node& n, bool isSimple)
42 : : {
43 : 106541 : Node exp;
44 : 213082 : return rewritePredViaEntailment(n, exp, isSimple);
45 : 106541 : }
46 : :
47 : 107273 : Node ArithEntail::rewritePredViaEntailment(const Node& n,
48 : : Node& exp,
49 : : bool isSimple)
50 : : {
51 : 107273 : NodeManager* nm = n.getNodeManager();
52 : 107273 : if (n.getKind() == Kind::EQUAL && n[0].getType().isInteger())
53 : : {
54 : 28329 : exp = nm->mkNode(Kind::SUB, nm->mkNode(Kind::SUB, n[0], n[1]), d_one);
55 [ + + ]: 28329 : if (!findApprox(rewriteArith(exp), isSimple).isNull())
56 : : {
57 : 4458 : return nm->mkConst(false);
58 : : }
59 : 26100 : exp = nm->mkNode(Kind::SUB, nm->mkNode(Kind::SUB, n[1], n[0]), d_one);
60 [ + + ]: 26100 : if (!findApprox(rewriteArith(exp), isSimple).isNull())
61 : : {
62 : 2820 : return nm->mkConst(false);
63 : : }
64 : 24690 : exp = Node::null();
65 [ + + ]: 24690 : if (checkEq(n[0], n[1]))
66 : : {
67 : : // explanation is null
68 : 644 : return nm->mkConst(true);
69 : : }
70 : : }
71 [ + - ]: 78944 : else if (n.getKind() == Kind::GEQ)
72 : : {
73 : 78944 : exp = nm->mkNode(Kind::SUB, n[0], n[1]);
74 [ + + ]: 78944 : if (!findApprox(rewriteArith(exp), isSimple).isNull())
75 : : {
76 : 4298 : return nm->mkConst(true);
77 : : }
78 : 76795 : exp = nm->mkNode(Kind::SUB, nm->mkNode(Kind::SUB, n[1], n[0]), d_one);
79 [ + + ]: 76795 : if (!findApprox(rewriteArith(exp), isSimple).isNull())
80 : : {
81 : 12838 : return nm->mkConst(false);
82 : : }
83 : 70376 : exp = Node::null();
84 : : }
85 : 94744 : return Node::null();
86 : : }
87 : :
88 : 1727953 : Node ArithEntail::rewriteArith(Node a)
89 : : {
90 [ - + ][ - - ]: 3455906 : AlwaysAssert(a.getType().isInteger())
91 : 1727953 : << "Bad term: " << a << " " << a.getType();
92 [ + + ]: 1727953 : if (d_rr != nullptr)
93 : : {
94 : 243186 : return d_rr->rewrite(a);
95 : : }
96 : : else
97 : : {
98 : 1484767 : 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 : 1484767 : Node an = arith::PolyNorm::getPolyNorm(a);
104 : 1484767 : return an;
105 : 1484767 : }
106 : :
107 : 62049 : Node ArithEntail::normalizeGeq(const Node& n) const
108 : : {
109 : 62049 : NodeManager* nm = n.getNodeManager();
110 : 124098 : if (n.getNumChildren() != 2 || !n[0].getType().isInteger()
111 : 124098 : || !n[1].getType().isInteger())
112 : : {
113 : 62 : return Node::null();
114 : : }
115 [ + + ][ + + ]: 61987 : switch (n.getKind())
[ - ]
116 : : {
117 : 39841 : case Kind::GEQ: return n;
118 : 7248 : case Kind::LEQ: return nm->mkNode(Kind::GEQ, n[1], n[0]);
119 : 6256 : case Kind::LT:
120 : : return nm->mkNode(
121 : : Kind::GEQ,
122 : : n[1],
123 : 6256 : nm->mkNode(Kind::ADD, n[0], nm->mkConstInt(Rational(1))));
124 : 8642 : case Kind::GT:
125 : : return nm->mkNode(
126 : : Kind::GEQ,
127 : : n[0],
128 : 8642 : nm->mkNode(Kind::ADD, n[1], nm->mkConstInt(Rational(1))));
129 : 0 : default: break;
130 : : }
131 : 0 : return Node::null();
132 : : }
133 : :
134 : 1561856 : Node ArithEntail::rewriteLengthIntro(const Node& n,
135 : : TConvProofGenerator* pg) const
136 : : {
137 : 1561856 : NodeManager* nm = n.getNodeManager();
138 : 1561856 : std::unordered_map<TNode, Node> visited;
139 : 1561856 : std::unordered_map<TNode, Node>::iterator it;
140 : 1561856 : std::vector<TNode> visit;
141 : 1561856 : TNode cur;
142 : 1561856 : visit.push_back(n);
143 : : do
144 : : {
145 : 27097163 : cur = visit.back();
146 : 27097163 : it = visited.find(cur);
147 [ + + ]: 27097163 : if (it == visited.end())
148 : : {
149 [ + + ]: 14704901 : if (cur.getNumChildren() == 0)
150 : : {
151 : 5995445 : visit.pop_back();
152 : 5995445 : visited[cur] = cur;
153 : 5995445 : continue;
154 : : }
155 : 8709456 : visited.emplace(cur, Node::null());
156 : 8709456 : visit.insert(visit.end(), cur.begin(), cur.end());
157 : 8709456 : continue;
158 : : }
159 : 12392262 : visit.pop_back();
160 [ + + ]: 12392262 : if (it->second.isNull())
161 : : {
162 : 8709456 : Kind k = cur.getKind();
163 : 8709456 : bool childChanged = false;
164 : 8709456 : std::vector<Node> children;
165 [ + + ]: 25535307 : for (const Node& cn : cur)
166 : : {
167 : 16825851 : it = visited.find(cn);
168 [ - + ][ - + ]: 16825851 : Assert(it != visited.end());
[ - - ]
169 [ - + ][ - + ]: 16825851 : Assert(!it->second.isNull());
[ - - ]
170 : 16825851 : children.push_back(it->second);
171 [ + + ][ + + ]: 16825851 : childChanged = childChanged || it->second != cn;
172 : 16825851 : }
173 : 8709456 : Node ret = cur;
174 [ + + ]: 8709456 : if (childChanged)
175 : : {
176 : 581805 : ret = nm->mkNode(k, children);
177 : : }
178 : 8709456 : if (k == Kind::STRING_LENGTH
179 : 8709456 : && (ret[0].getKind() == Kind::STRING_CONCAT || ret[0].isConst()))
180 : : {
181 : 434065 : Node arg = ret[0];
182 : : // First ensure ACI norm, which ensures that we fully flatten
183 : : // e.g. (len (str.++ (str.++ a b) c)) ---> (len (str.++ a b c)) --->
184 : : // (+ (len a) (len b) (len c)) below.
185 [ + + ]: 434065 : if (arg.getKind() == Kind::STRING_CONCAT)
186 : : {
187 : 135430 : arg = expr::getACINormalForm(arg);
188 [ + + ]: 135430 : if (arg != ret[0])
189 : : {
190 : 78 : Node ret2 = nm->mkNode(k, {arg});
191 [ + + ]: 39 : if (pg != nullptr)
192 : : {
193 : 6 : pg->addRewriteStep(ret,
194 : : ret2,
195 : : nullptr,
196 : : false,
197 : : TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE);
198 : : }
199 : 39 : ret = ret2;
200 : 39 : }
201 : : }
202 : 434065 : std::vector<Node> cc;
203 : 434065 : utils::getConcat(arg, cc);
204 : 434065 : std::vector<Node> sum;
205 [ + + ]: 1156103 : for (const Node& c : cc)
206 : : {
207 [ + + ]: 722038 : if (c.isConst())
208 : : {
209 : 424449 : sum.push_back(nm->mkConstInt(Rational(Word::getLength(c))));
210 : : }
211 : : else
212 : : {
213 : 297589 : sum.push_back(nm->mkNode(Kind::STRING_LENGTH, c));
214 : : }
215 : : }
216 [ - + ][ - + ]: 434065 : Assert(!sum.empty());
[ - - ]
217 [ + + ]: 434065 : Node rret = sum.size() == 1 ? sum[0] : nm->mkNode(Kind::ADD, sum);
218 [ + + ]: 434065 : if (pg != nullptr)
219 : : {
220 : 359 : pg->addRewriteStep(ret,
221 : : rret,
222 : : nullptr,
223 : : false,
224 : : TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE);
225 : : }
226 : 434065 : ret = rret;
227 : 434065 : }
228 : 8709456 : visited[cur] = ret;
229 : 8709456 : }
230 [ + + ]: 27097163 : } while (!visit.empty());
231 [ - + ][ - + ]: 1561856 : Assert(visited.find(n) != visited.end());
[ - - ]
232 [ - + ][ - + ]: 1561856 : Assert(!visited.find(n)->second.isNull());
[ - - ]
233 : 3123712 : return visited[n];
234 : 1561856 : }
235 : :
236 : 34676 : bool ArithEntail::checkEq(Node a, Node b)
237 : : {
238 [ + + ]: 34676 : if (a == b)
239 : : {
240 : 319 : return true;
241 : : }
242 : 34357 : Node ar = rewriteArith(a);
243 : 34357 : Node br = rewriteArith(b);
244 : 34357 : return ar == br;
245 : 34357 : }
246 : :
247 : 898384 : bool ArithEntail::check(Node a, Node b, bool strict, bool isSimple)
248 : : {
249 [ + + ]: 898384 : if (a == b)
250 : : {
251 : 55566 : return !strict;
252 : : }
253 : 1685636 : Node diff = NodeManager::mkNode(Kind::SUB, a, b);
254 : 842818 : return check(diff, strict, isSimple);
255 : 842818 : }
256 : :
257 : 1372073 : bool ArithEntail::check(Node a, bool strict, bool isSimple)
258 : : {
259 [ + + ]: 1372073 : if (a.isConst())
260 : : {
261 [ + + ]: 149687 : return a.getConst<Rational>().sgn() >= (strict ? 1 : 0);
262 : : }
263 : 1669412 : Node ar = strict ? NodeManager::mkNode(Kind::SUB, a, d_one) : a;
264 [ + + ]: 1222386 : if (isSimple)
265 : : {
266 : 206653 : ar = arith::PolyNorm::getPolyNorm(ar);
267 : : // if simple, just call the checkSimple routine.
268 : 206653 : return checkSimple(ar);
269 : : }
270 : : else
271 : : {
272 : : // otherwise rewrite arith and find approximation
273 : 1015733 : ar = rewriteArith(ar);
274 : : }
275 : 1015733 : Node ara = findApprox(ar, isSimple);
276 : 1015733 : return !ara.isNull();
277 : 1222386 : }
278 : :
279 : 1226553 : Node ArithEntail::findApprox(Node ar, bool isSimple)
280 : : {
281 [ + + ]: 1226553 : std::map<Node, Node>& cache = isSimple ? d_approxCacheSimple : d_approxCache;
282 : 1226553 : std::map<Node, Node>::iterator it = cache.find(ar);
283 [ + + ]: 1226553 : if (it != cache.end())
284 : : {
285 : 824405 : return it->second;
286 : : }
287 : 402148 : Node ret;
288 [ + + ]: 402148 : if (checkSimple(ar))
289 : : {
290 : : // didn't need approximation
291 : 25094 : ret = ar;
292 : : }
293 : : else
294 : : {
295 : 377054 : ret = findApproxInternal(ar, isSimple);
296 : : }
297 : 402148 : cache[ar] = ret;
298 : 402148 : return ret;
299 : 402148 : }
300 : :
301 : 377054 : Node ArithEntail::findApproxInternal(Node ar, bool isSimple)
302 : : {
303 : : // if not using recursive approximations, we always set isSimple to true
304 [ + + ]: 377054 : if (!d_recApprox)
305 : : {
306 : 324405 : isSimple = true;
307 : : }
308 : 377054 : NodeManager* nm = ar.getNodeManager();
309 : 377054 : std::map<Node, Node> msum;
310 [ + - ]: 754108 : Trace("strings-ent-approx-debug")
311 : 377054 : << "Setup arithmetic approximations for " << ar << std::endl;
312 [ - + ]: 377054 : if (!ArithMSum::getMonomialSum(ar, msum))
313 : : {
314 [ - - ]: 0 : Trace("strings-ent-approx-debug")
315 : 0 : << "...failed to get monomial sum!" << std::endl;
316 : 0 : return Node::null();
317 : : }
318 : : // for each monomial v*c, mApprox[v] a list of
319 : : // possibilities for how the term can be soundly approximated, that is,
320 : : // if mApprox[v] contains av, then v*c > av*c. Notice that if c
321 : : // is positive, then v > av, otherwise if c is negative, then v < av.
322 : : // In other words, av is an under-approximation if c is positive, and an
323 : : // over-approximation if c is negative.
324 : 377054 : bool changed = false;
325 : 377054 : std::map<Node, std::vector<Node> > mApprox;
326 : : // map from approximations to their monomial sums
327 : 377054 : std::map<Node, std::map<Node, Node> > approxMsums;
328 : : // aarSum stores each monomial that does not have multiple approximations
329 : 377054 : std::vector<Node> aarSum;
330 : : // stores the witness
331 : 377054 : arith::ArithSubs approxMap;
332 [ + + ]: 1196328 : for (std::pair<const Node, Node>& m : msum)
333 : : {
334 : 819274 : Node v = m.first;
335 : 819274 : Node c = m.second;
336 [ + - ]: 1638548 : Trace("strings-ent-approx-debug")
337 : 819274 : << "Get approximations " << v << "..." << std::endl;
338 [ + + ]: 819274 : if (v.isNull())
339 : : {
340 [ - + ][ - + ]: 270848 : Node mn = c.isNull() ? nm->mkConstInt(Rational(1)) : c;
[ - - ]
341 : 270848 : aarSum.push_back(mn);
342 : 270848 : }
343 : : else
344 : : {
345 : : // c.isNull() means c = 1
346 [ + + ][ + + ]: 548426 : bool isOverApprox = !c.isNull() && c.getConst<Rational>().sgn() == -1;
347 : 548426 : std::vector<Node>& approx = mApprox[v];
348 : 548426 : std::unordered_set<Node> visited;
349 : 548426 : std::vector<Node> toProcess;
350 : 548426 : toProcess.push_back(v);
351 : : do
352 : : {
353 : 569235 : Node curr = toProcess.back();
354 [ + - ]: 569235 : Trace("strings-ent-approx-debug") << " process " << curr << std::endl;
355 : 569235 : curr = arith::PolyNorm::getPolyNorm(curr);
356 : 569235 : toProcess.pop_back();
357 [ + + ]: 569235 : if (visited.find(curr) == visited.end())
358 : : {
359 : 568292 : visited.insert(curr);
360 : 568292 : std::vector<Node> currApprox;
361 : 568292 : getArithApproximations(curr, currApprox, isOverApprox, isSimple);
362 [ + + ]: 568292 : if (currApprox.empty())
363 : : {
364 [ + - ]: 949158 : Trace("strings-ent-approx-debug")
365 : 474579 : << "...approximation: " << curr << std::endl;
366 : : // no approximations, thus curr is a possibility
367 : 474579 : approx.push_back(curr);
368 : : }
369 [ + + ]: 93713 : else if (isSimple)
370 : : {
371 : : // don't rewrite or re-approximate
372 : 81655 : approx = currApprox;
373 : : }
374 : : else
375 : : {
376 : 24116 : toProcess.insert(
377 : 24116 : toProcess.end(), currApprox.begin(), currApprox.end());
378 : : }
379 : 568292 : }
380 [ + + ]: 569235 : } while (!toProcess.empty());
381 [ - + ][ - + ]: 548426 : Assert(!approx.empty());
[ - - ]
382 : : // if we have only one approximation, move it to final
383 [ + + ]: 548426 : if (approx.size() == 1)
384 : : {
385 [ + + ]: 520230 : if (v != approx[0])
386 : : {
387 : 66059 : changed = true;
388 [ + - ]: 132118 : Trace("strings-ent-approx")
389 : 66059 : << "- Propagate (" << (d_rr == nullptr) << ", " << isSimple
390 : 66059 : << ") " << v << " = " << approx[0] << std::endl;
391 : 66059 : approxMap.add(v, approx[0]);
392 : : }
393 : 1040460 : Node mn = ArithMSum::mkCoeffTerm(c, approx[0]);
394 : 520230 : aarSum.push_back(mn);
395 : 520230 : mApprox.erase(v);
396 : 520230 : }
397 : : else
398 : : {
399 : : // compute monomial sum form for each approximation, used below
400 [ + + ]: 84592 : for (const Node& aa : approx)
401 : : {
402 [ + + ]: 56396 : if (approxMsums.find(aa) == approxMsums.end())
403 : : {
404 : : // ensure rewritten, which makes a difference if isSimple is true
405 : 54058 : Node aar = arith::PolyNorm::getPolyNorm(aa);
406 : : CVC5_UNUSED bool ret =
407 : 54058 : ArithMSum::getMonomialSum(aar, approxMsums[aa]);
408 : 54058 : Assert(ret) << "Could not find sum " << aa;
409 : 54058 : }
410 : : }
411 : 28196 : changed = true;
412 : : }
413 : 548426 : }
414 : 819274 : }
415 [ + + ]: 377054 : if (!changed)
416 : : {
417 : : // approximations had no effect, return
418 [ + - ]: 294368 : Trace("strings-ent-approx-debug") << "...no approximations" << std::endl;
419 : 294368 : return Node::null();
420 : : }
421 : : // get the current "fixed" sum for the abstraction of ar
422 : : Node aar =
423 : 82686 : aarSum.empty()
424 : 5073 : ? d_zero
425 [ + + ][ + + ]: 82686 : : (aarSum.size() == 1 ? aarSum[0] : nm->mkNode(Kind::ADD, aarSum));
426 : 82686 : aar = arith::PolyNorm::getPolyNorm(aar);
427 [ + - ]: 165372 : Trace("strings-ent-approx-debug")
428 : 82686 : << "...processed fixed sum " << aar << " with " << mApprox.size()
429 : 82686 : << " approximated monomials." << std::endl;
430 : : // if we have a choice of how to approximate
431 [ + + ]: 82686 : if (!mApprox.empty())
432 : : {
433 : : // convert aar back to monomial sum
434 : 27880 : std::map<Node, Node> msumAar;
435 [ - + ]: 27880 : if (!ArithMSum::getMonomialSum(aar, msumAar))
436 : : {
437 : 0 : return Node::null();
438 : : }
439 [ - + ]: 27880 : if (TraceIsOn("strings-ent-approx"))
440 : : {
441 [ - - ]: 0 : Trace("strings-ent-approx")
442 : 0 : << "---- Check arithmetic entailment by under-approximation " << ar
443 : 0 : << " >= 0" << std::endl;
444 [ - - ]: 0 : Trace("strings-ent-approx") << "FIXED:" << std::endl;
445 : 0 : ArithMSum::debugPrintMonomialSum(msumAar, "strings-ent-approx");
446 [ - - ]: 0 : Trace("strings-ent-approx") << "APPROX:" << std::endl;
447 [ - - ]: 0 : for (std::pair<const Node, std::vector<Node> >& a : mApprox)
448 : : {
449 : 0 : Node c = msum[a.first];
450 [ - - ]: 0 : Trace("strings-ent-approx") << " ";
451 [ - - ]: 0 : if (!c.isNull())
452 : : {
453 [ - - ]: 0 : Trace("strings-ent-approx") << c << " * ";
454 : : }
455 [ - - ]: 0 : Trace("strings-ent-approx")
456 : 0 : << a.second << " ...from " << a.first << std::endl;
457 : 0 : }
458 [ - - ]: 0 : Trace("strings-ent-approx") << std::endl;
459 : : }
460 : 27880 : Rational one(1);
461 : : // incorporate monomials one at a time that have a choice of approximations
462 [ + + ]: 56076 : while (!mApprox.empty())
463 : : {
464 : 28196 : Node v;
465 : 28196 : Node vapprox;
466 : 28196 : int maxScore = -1;
467 : : // Look at each approximation, take the one with the best score.
468 : : // Notice that we are in the process of trying to prove
469 : : // ( c1*t1 + .. + cn*tn ) + ( approx_1 | ... | approx_m ) >= 0,
470 : : // where c1*t1 + .. + cn*tn is the "fixed" component of our sum (aar)
471 : : // and approx_1 ... approx_m are possible approximations. The
472 : : // intution here is that we want coefficients c1...cn to be positive.
473 : : // This is because arithmetic string terms t1...tn (which may be
474 : : // applications of len, indexof, str.to.int) are never entailed to be
475 : : // negative. Hence, we add the approx_i that contributes the "most"
476 : : // towards making all constants c1...cn positive and cancelling negative
477 : : // monomials in approx_i itself.
478 [ + - ]: 28196 : for (std::pair<const Node, std::vector<Node> >& nam : mApprox)
479 : : {
480 : 28196 : Node cr = msum[nam.first];
481 [ + + ]: 84592 : for (const Node& aa : nam.second)
482 : : {
483 : 56396 : unsigned helpsCancelCount = 0;
484 : 56396 : unsigned addsObligationCount = 0;
485 : 56396 : std::map<Node, Node>::iterator it;
486 : : // we are processing an approximation cr*( c1*t1 + ... + cn*tn )
487 [ + + ]: 125307 : for (std::pair<const Node, Node>& aam : approxMsums[aa])
488 : : {
489 : : // Say aar is of the form t + c*ti, and aam is the monomial ci*ti
490 : : // where ci != 0. We say aam:
491 : : // (1) helps cancel if c != 0 and c>0 != ci>0
492 : : // (2) adds obligation if c>=0 and c+ci<0
493 : 68911 : Node ti = aam.first;
494 : 68911 : Node ci = aam.second;
495 [ + + ]: 68911 : if (!cr.isNull())
496 : : {
497 [ + + ]: 142146 : ci = ci.isNull() ? cr
498 : 46624 : : nm->mkConstInt(cr.getConst<Rational>()
499 [ + + ][ - - ]: 142146 : * ci.getConst<Rational>());
500 : : }
501 [ + - ]: 68911 : Trace("strings-ent-approx-debug") << ci << "*" << ti << " ";
502 [ + + ]: 68911 : int ciSgn = ci.isNull() ? 1 : ci.getConst<Rational>().sgn();
503 : 68911 : it = msumAar.find(ti);
504 [ + + ]: 68911 : if (it != msumAar.end())
505 : : {
506 : 28266 : Node c = it->second;
507 [ + + ]: 28266 : int cSgn = c.isNull() ? 1 : c.getConst<Rational>().sgn();
508 [ + + ]: 28266 : if (cSgn == 0)
509 : : {
510 [ + - ]: 4444 : addsObligationCount += (ciSgn == -1 ? 1 : 0);
511 : : }
512 [ + + ]: 23822 : else if (cSgn != ciSgn)
513 : : {
514 : 16180 : helpsCancelCount++;
515 [ + + ]: 16180 : Rational r1 = c.isNull() ? one : c.getConst<Rational>();
516 [ + + ]: 16180 : Rational r2 = ci.isNull() ? one : ci.getConst<Rational>();
517 : 16180 : Rational r12 = r1 + r2;
518 [ + + ]: 16180 : if (r12.sgn() == -1)
519 : : {
520 : 6309 : addsObligationCount++;
521 : : }
522 : 16180 : }
523 : 28266 : }
524 : : else
525 : : {
526 [ + + ]: 40645 : addsObligationCount += (ciSgn == -1 ? 1 : 0);
527 : : }
528 : 68911 : }
529 [ + - ]: 112792 : Trace("strings-ent-approx-debug")
530 : 0 : << "counts=" << helpsCancelCount << "," << addsObligationCount
531 : 56396 : << " for " << aa << " into " << aar << std::endl;
532 [ + + ]: 56396 : int score = (addsObligationCount > 0 ? 0 : 2)
533 [ + + ]: 56396 : + (helpsCancelCount > 0 ? 1 : 0);
534 : : // if its the best, update v and vapprox
535 [ + + ][ + + ]: 56396 : if (v.isNull() || score > maxScore)
[ + + ]
536 : : {
537 : 34582 : v = nam.first;
538 : 34582 : vapprox = aa;
539 : 34582 : maxScore = score;
540 : : }
541 : : }
542 [ + - ]: 28196 : if (!v.isNull())
543 : : {
544 : 28196 : break;
545 : : }
546 [ - + ]: 28196 : }
547 [ + - ]: 56392 : Trace("strings-ent-approx") << "- Decide (" << (d_rr == nullptr) << ") "
548 : 28196 : << v << " = " << vapprox << std::endl;
549 : : // we incorporate v approximated by vapprox into the overall approximation
550 : : // for ar
551 [ + - ][ + - ]: 28196 : Assert(!v.isNull() && !vapprox.isNull());
[ - + ][ - + ]
[ - - ]
552 [ - + ][ - + ]: 28196 : Assert(msum.find(v) != msum.end());
[ - - ]
553 : 56392 : Node mn = ArithMSum::mkCoeffTerm(msum[v], vapprox);
554 : 28196 : aar = nm->mkNode(Kind::ADD, aar, mn);
555 : 28196 : approxMap.add(v, vapprox);
556 : : // update the msumAar map
557 : 28196 : aar = arith::PolyNorm::getPolyNorm(aar);
558 : 28196 : msumAar.clear();
559 [ - + ]: 28196 : if (!ArithMSum::getMonomialSum(aar, msumAar))
560 : : {
561 : 0 : DebugUnhandled();
562 : : Trace("strings-ent-approx")
563 : : << "...failed to get monomial sum!" << std::endl;
564 : : return Node::null();
565 : : }
566 : : // we have processed the approximation for v
567 : 28196 : mApprox.erase(v);
568 [ + - ][ + - ]: 28196 : }
[ + - ]
569 [ + - ]: 27880 : Trace("strings-ent-approx") << "-----------------" << std::endl;
570 [ + - ][ + - ]: 27880 : }
571 [ - + ]: 82686 : if (aar == ar)
572 : : {
573 [ - - ]: 0 : Trace("strings-ent-approx-debug")
574 : 0 : << "...approximation had no effect" << std::endl;
575 : : // this should never happen, but we avoid the infinite loop for sanity here
576 : 0 : DebugUnhandled();
577 : : return Node::null();
578 : : }
579 : : // Check entailment on the approximation of ar.
580 : : // Notice that this may trigger further reasoning by approximation. For
581 : : // example, len( replace( x ++ y, substr( x, 0, n ), z ) ) may be
582 : : // under-approximated as len( x ) + len( y ) - len( substr( x, 0, n ) ) on
583 : : // this call, where in the recursive call we may over-approximate
584 : : // len( substr( x, 0, n ) ) as len( x ). In this example, we can infer
585 : : // that len( replace( x ++ y, substr( x, 0, n ), z ) ) >= len( y ) in two
586 : : // steps.
587 [ + + ]: 82686 : if (check(aar, false, isSimple))
588 : : {
589 [ + - ]: 11394 : Trace("strings-ent-approx")
590 : 0 : << "*** StrArithApprox: showed " << ar
591 : 5697 : << " >= 0 using under-approximation!" << std::endl;
592 [ + - ]: 11394 : Trace("strings-ent-approx")
593 : 5697 : << "*** StrArithApprox: rewritten was " << aar << std::endl;
594 : : // Apply arithmetic substitution, which ensures we only replace terms
595 : : // in the top-level arithmetic skeleton of ar.
596 : 5697 : Node approx = approxMap.applyArith(ar);
597 [ + - ]: 11394 : Trace("strings-ent-approx")
598 : 0 : << "*** StrArithApprox: under-approximation was " << approx
599 : 5697 : << std::endl;
600 : 5697 : return approx;
601 : 5697 : }
602 : 76989 : return Node::null();
603 : 377054 : }
604 : :
605 : 568298 : void ArithEntail::getArithApproximations(Node a,
606 : : std::vector<Node>& approx,
607 : : bool isOverApprox,
608 : : bool isSimple)
609 : : {
610 : 568298 : NodeManager* nm = a.getNodeManager();
611 : : // We do not handle ADD here since this leads to exponential behavior.
612 : : // Instead, this is managed, e.g. during checkApprox, where
613 : : // ADD terms are expanded "on-demand" during the reasoning.
614 [ + - ]: 1136596 : Trace("strings-ent-approx-debug")
615 : 568298 : << "Get arith approximations " << a << std::endl;
616 : 568298 : Kind ak = a.getKind();
617 [ + + ]: 568298 : if (ak == Kind::MULT)
618 : : {
619 : 1871 : Node c;
620 : 1871 : Node v;
621 [ + + ]: 1871 : if (ArithMSum::getMonomial(a, c, v))
622 : : {
623 : 6 : bool isNeg = c.getConst<Rational>().sgn() == -1;
624 [ - + ]: 12 : getArithApproximations(
625 : 0 : v, approx, isNeg ? !isOverApprox : isOverApprox, isSimple);
626 [ - + ]: 6 : for (unsigned i = 0, size = approx.size(); i < size; i++)
627 : : {
628 : 0 : approx[i] = nm->mkNode(Kind::MULT, c, approx[i]);
629 : : }
630 : : }
631 : 1871 : }
632 [ + + ]: 566427 : else if (ak == Kind::STRING_LENGTH)
633 : : {
634 : 410772 : Kind aak = a[0].getKind();
635 [ + + ]: 410772 : if (aak == Kind::STRING_SUBSTR)
636 : : {
637 : : // over,under-approximations for len( substr( x, n, m ) )
638 : 168350 : Node lenx = nm->mkNode(Kind::STRING_LENGTH, a[0][0]);
639 [ + + ]: 84175 : if (isOverApprox)
640 : : {
641 : : // m >= 0 implies
642 : : // m >= len( substr( x, n, m ) )
643 [ + + ]: 46401 : if (check(a[0][2], false, isSimple))
644 : : {
645 : 26835 : approx.push_back(a[0][2]);
646 : : }
647 [ + + ]: 46401 : if (check(lenx, a[0][1], false, isSimple))
648 : : {
649 : : // n <= len( x ) implies
650 : : // len( x ) - n >= len( substr( x, n, m ) )
651 : 20013 : approx.push_back(nm->mkNode(Kind::SUB, lenx, a[0][1]));
652 : : }
653 : : else
654 : : {
655 : : // len( x ) >= len( substr( x, n, m ) )
656 : 26388 : approx.push_back(lenx);
657 : : }
658 : : }
659 : : else
660 : : {
661 : : // 0 <= n and n+m <= len( x ) implies
662 : : // m <= len( substr( x, n, m ) )
663 : 75548 : Node npm = nm->mkNode(Kind::ADD, a[0][1], a[0][2]);
664 : 75548 : if (check(a[0][1], false, isSimple)
665 : 75548 : && check(lenx, npm, false, isSimple))
666 : : {
667 : 4222 : approx.push_back(a[0][2]);
668 : : }
669 : : // 0 <= n and n+m >= len( x ) implies
670 : : // len(x)-n <= len( substr( x, n, m ) )
671 : 75548 : if (check(a[0][1], false, isSimple)
672 : 75548 : && check(npm, lenx, false, isSimple))
673 : : {
674 : 3285 : approx.push_back(nm->mkNode(Kind::SUB, lenx, a[0][1]));
675 : : }
676 : 37774 : }
677 : 84175 : }
678 [ + + ]: 326597 : else if (aak == Kind::STRING_REPLACE)
679 : : {
680 : : // over,under-approximations for len( replace( x, y, z ) )
681 : : // notice this is either len( x ) or ( len( x ) + len( z ) - len( y ) )
682 : 34546 : Node lenx = nm->mkNode(Kind::STRING_LENGTH, a[0][0]);
683 : 34546 : Node leny = nm->mkNode(Kind::STRING_LENGTH, a[0][1]);
684 : 34546 : Node lenz = nm->mkNode(Kind::STRING_LENGTH, a[0][2]);
685 [ + + ]: 17273 : if (isOverApprox)
686 : : {
687 [ + + ]: 8633 : if (check(leny, lenz, false, isSimple))
688 : : {
689 : : // len( y ) >= len( z ) implies
690 : : // len( x ) >= len( replace( x, y, z ) )
691 : 1 : approx.push_back(lenx);
692 : : }
693 : : else
694 : : {
695 : : // len( x ) + len( z ) >= len( replace( x, y, z ) )
696 : 8632 : approx.push_back(nm->mkNode(Kind::ADD, lenx, lenz));
697 : : }
698 : : }
699 : : else
700 : : {
701 [ + - ][ + + ]: 8640 : if (check(lenz, leny, false, isSimple)
[ - - ][ - - ]
702 : 8640 : || check(lenz, lenx, false, isSimple))
703 : : {
704 : : // len( y ) <= len( z ) or len( x ) <= len( z ) implies
705 : : // len( x ) <= len( replace( x, y, z ) )
706 : 2802 : approx.push_back(lenx);
707 : : }
708 : : else
709 : : {
710 : : // len( x ) - len( y ) <= len( replace( x, y, z ) )
711 : 5838 : approx.push_back(nm->mkNode(Kind::SUB, lenx, leny));
712 : : }
713 : : }
714 : 17273 : }
715 [ + + ]: 309324 : else if (aak == Kind::STRING_ITOS)
716 : : {
717 : : // over,under-approximations for len( int.to.str( x ) )
718 [ + + ]: 2097 : if (isOverApprox)
719 : : {
720 [ + + ]: 1072 : if (check(a[0][0], false, isSimple))
721 : : {
722 [ + + ]: 100 : if (check(a[0][0], true, isSimple))
723 : : {
724 : : // x > 0 implies
725 : : // x >= len( int.to.str( x ) )
726 : 14 : approx.push_back(a[0][0]);
727 : : }
728 : : else
729 : : {
730 : : // x >= 0 implies
731 : : // x+1 >= len( int.to.str( x ) )
732 : 86 : approx.push_back(
733 : 172 : nm->mkNode(Kind::ADD, nm->mkConstInt(Rational(1)), a[0][0]));
734 : : }
735 : : }
736 : : }
737 : : else
738 : : {
739 [ + + ]: 1025 : if (check(a[0][0], false, isSimple))
740 : : {
741 : : // x >= 0 implies
742 : : // len( int.to.str( x ) ) >= 1
743 : 48 : approx.push_back(nm->mkConstInt(Rational(1)));
744 : : }
745 : : // other crazy things are possible here, e.g.
746 : : // len( int.to.str( len( y ) + 10 ) ) >= 2
747 : : }
748 : : }
749 : : }
750 [ + + ]: 155655 : else if (ak == Kind::STRING_INDEXOF)
751 : : {
752 : : // over,under-approximations for indexof( x, y, n )
753 [ + + ]: 24516 : if (isOverApprox)
754 : : {
755 : 23614 : Node lenx = nm->mkNode(Kind::STRING_LENGTH, a[0]);
756 : 23614 : Node leny = nm->mkNode(Kind::STRING_LENGTH, a[1]);
757 [ + + ]: 11807 : if (check(lenx, leny, false, isSimple))
758 : : {
759 : : // len( x ) >= len( y ) implies
760 : : // len( x ) - len( y ) >= indexof( x, y, n )
761 : 1201 : approx.push_back(nm->mkNode(Kind::SUB, lenx, leny));
762 : : }
763 : : else
764 : : {
765 : : // len( x ) >= indexof( x, y, n )
766 : 10606 : approx.push_back(lenx);
767 : : }
768 : 11807 : }
769 : : else
770 : : {
771 : : // TODO?:
772 : : // contains( substr( x, n, len( x ) ), y ) implies
773 : : // n <= indexof( x, y, n )
774 : : // ...hard to test, runs risk of non-termination
775 : :
776 : : // -1 <= indexof( x, y, n )
777 : 12709 : approx.push_back(nm->mkConstInt(Rational(-1)));
778 : : }
779 : : }
780 [ + + ]: 131139 : else if (ak == Kind::STRING_STOI)
781 : : {
782 : : // over,under-approximations for str.to.int( x )
783 [ + + ]: 346 : if (isOverApprox)
784 : : {
785 : : // TODO?:
786 : : // y >= 0 implies
787 : : // y >= str.to.int( int.to.str( y ) )
788 : : }
789 : : else
790 : : {
791 : : // -1 <= str.to.int( x )
792 : 176 : approx.push_back(nm->mkConstInt(Rational(-1)));
793 : : }
794 : : }
795 [ + - ]: 1136596 : Trace("strings-ent-approx-debug")
796 : 568298 : << "Return " << approx.size() << " approximations" << std::endl;
797 : 568304 : }
798 : :
799 : 3825 : bool ArithEntail::checkWithEqAssumption(Node assumption, Node a, bool strict)
800 : : {
801 [ - + ][ - + ]: 3825 : Assert(assumption.getKind() == Kind::EQUAL);
[ - - ]
802 [ + - ]: 7650 : Trace("strings-entail") << "checkWithEqAssumption: " << assumption << " " << a
803 : 3825 : << ", strict=" << strict << std::endl;
804 : :
805 : : // Find candidates variables to compute substitutions for
806 : 3825 : std::unordered_set<Node> candVars;
807 : 11475 : std::vector<Node> toVisit = {assumption};
808 [ + + ]: 26080 : while (!toVisit.empty())
809 : : {
810 : 22255 : Node curr = toVisit.back();
811 : 22255 : toVisit.pop_back();
812 : :
813 [ + + ]: 40496 : if (curr.getKind() == Kind::ADD || curr.getKind() == Kind::MULT
814 [ + + ][ + + ]: 40496 : || curr.getKind() == Kind::SUB || curr.getKind() == Kind::EQUAL)
[ + + ][ + + ]
815 : : {
816 [ + + ]: 27645 : for (const auto& currChild : curr)
817 : : {
818 : 18430 : toVisit.push_back(currChild);
819 : 18430 : }
820 : : }
821 [ + + ][ + - ]: 13040 : else if (curr.isVar() && Theory::theoryOf(curr) == THEORY_ARITH)
[ + + ][ + + ]
[ - - ]
822 : : {
823 : 3017 : candVars.insert(curr);
824 : : }
825 [ + + ]: 10023 : else if (curr.getKind() == Kind::STRING_LENGTH)
826 : : {
827 : 4498 : candVars.insert(curr);
828 : : }
829 : 22255 : }
830 : :
831 : : // Check if any of the candidate variables are in n
832 : 3825 : Node v;
833 [ - + ][ - + ]: 3825 : Assert(toVisit.empty());
[ - - ]
834 : 3825 : toVisit.push_back(a);
835 [ + + ]: 16505 : while (!toVisit.empty())
836 : : {
837 : 12840 : Node curr = toVisit.back();
838 : 12840 : toVisit.pop_back();
839 : :
840 [ + + ]: 22221 : for (const auto& currChild : curr)
841 : : {
842 : 9381 : toVisit.push_back(currChild);
843 : 9381 : }
844 : :
845 [ + + ]: 12840 : if (candVars.find(curr) != candVars.end())
846 : : {
847 : 160 : v = curr;
848 : 160 : break;
849 : : }
850 [ + + ]: 12840 : }
851 : :
852 [ + + ]: 3825 : if (v.isNull())
853 : : {
854 : : // No suitable candidate found
855 : 3665 : return false;
856 : : }
857 : :
858 : 320 : Node solution = ArithMSum::solveEqualityFor(assumption, v);
859 [ + + ]: 160 : if (solution.isNull())
860 : : {
861 : : // Could not solve for v
862 : 9 : return false;
863 : : }
864 [ + - ]: 302 : Trace("strings-entail") << "checkWithEqAssumption: subs " << v << " -> "
865 : 151 : << solution << std::endl;
866 : :
867 : 151 : TNode tv = v;
868 : 151 : TNode tsolution = solution;
869 : 151 : a = a.substitute(tv, tsolution);
870 : 151 : return check(a, strict);
871 : 3825 : }
872 : :
873 : 7016 : bool ArithEntail::checkWithAssumption(Node assumption,
874 : : Node a,
875 : : Node b,
876 : : bool strict)
877 : : {
878 : 7016 : NodeManager* nm = assumption.getNodeManager();
879 : :
880 [ + + ][ + + ]: 7016 : if (!assumption.isConst() && assumption.getKind() != Kind::EQUAL)
[ + + ]
881 : : {
882 : : // We rewrite inequality assumptions from x <= y to x + (str.len s) = y
883 : : // where s is some fresh string variable. We use (str.len s) because
884 : : // (str.len s) must be non-negative for the equation to hold.
885 : 3821 : Node x, y;
886 [ + + ]: 3821 : if (assumption.getKind() == Kind::GEQ)
887 : : {
888 : 2641 : x = assumption[0];
889 : 2641 : y = assumption[1];
890 : : }
891 : : else
892 : : {
893 : : // (not (>= s t)) --> (>= (t - 1) s)
894 : 1180 : Assert(assumption.getKind() == Kind::NOT
895 : : && assumption[0].getKind() == Kind::GEQ);
896 : 1180 : x = nm->mkNode(Kind::SUB, assumption[0][1], nm->mkConstInt(Rational(1)));
897 : 1180 : y = assumption[0][0];
898 : : }
899 : :
900 : 7642 : Node s = NodeManager::mkBoundVar("slackVal", nm->stringType());
901 : 3821 : Node slen = nm->mkNode(Kind::STRING_LENGTH, s);
902 : 7642 : Node sleny = nm->mkNode(Kind::ADD, y, slen);
903 : 7642 : Node rr = rewriteArith(nm->mkNode(Kind::SUB, x, sleny));
904 [ - + ]: 3821 : if (rr.isConst())
905 : : {
906 : 0 : assumption = nm->mkConst(rr.getConst<Rational>().sgn() == 0);
907 : : }
908 : : else
909 : : {
910 : 3821 : assumption = nm->mkNode(Kind::EQUAL, x, sleny);
911 : : }
912 : 3821 : }
913 : :
914 : 14032 : Node diff = nm->mkNode(Kind::SUB, a, b);
915 : 7016 : bool res = false;
916 [ + + ]: 7016 : if (assumption.isConst())
917 : : {
918 : 3191 : bool assumptionBool = assumption.getConst<bool>();
919 [ + - ]: 3191 : if (assumptionBool)
920 : : {
921 : 3191 : res = check(diff, strict);
922 : : }
923 : : else
924 : : {
925 : 0 : res = true;
926 : : }
927 : : }
928 : : else
929 : : {
930 : 3825 : res = checkWithEqAssumption(assumption, diff, strict);
931 : : }
932 : 7016 : return res;
933 : 7016 : }
934 : :
935 : 0 : bool ArithEntail::checkWithAssumptions(std::vector<Node> assumptions,
936 : : Node a,
937 : : Node b,
938 : : bool strict)
939 : : {
940 : : // TODO: We currently try to show the entailment with each assumption
941 : : // independently. In the future, we should make better use of multiple
942 : : // assumptions.
943 : 0 : bool res = false;
944 [ - - ]: 0 : for (const auto& assumption : assumptions)
945 : : {
946 [ - - ]: 0 : if (checkWithAssumption(assumption, a, b, strict))
947 : : {
948 : 0 : res = true;
949 : 0 : break;
950 : : }
951 : : }
952 : 0 : return res;
953 : : }
954 : :
955 : : struct ArithEntailConstantBoundLowerId
956 : : {
957 : : };
958 : : typedef expr::Attribute<ArithEntailConstantBoundLowerId, Node>
959 : : ArithEntailConstantBoundLower;
960 : :
961 : : struct ArithEntailConstantBoundUpperId
962 : : {
963 : : };
964 : : typedef expr::Attribute<ArithEntailConstantBoundUpperId, Node>
965 : : ArithEntailConstantBoundUpper;
966 : :
967 : 84854 : void ArithEntail::setConstantBoundCache(TNode n, Node ret, bool isLower)
968 : : {
969 [ + + ]: 84854 : if (isLower)
970 : : {
971 : : ArithEntailConstantBoundLower acbl;
972 : 46478 : n.setAttribute(acbl, ret);
973 : : }
974 : : else
975 : : {
976 : : ArithEntailConstantBoundUpper acbu;
977 : 38376 : n.setAttribute(acbu, ret);
978 : : }
979 : 84854 : }
980 : :
981 : 1280077 : bool ArithEntail::getConstantBoundCache(TNode n, bool isLower, Node& c)
982 : : {
983 [ + + ]: 1280077 : if (isLower)
984 : : {
985 : : ArithEntailConstantBoundLower acbl;
986 [ + + ]: 1180793 : if (n.hasAttribute(acbl))
987 : : {
988 : 1134315 : c = n.getAttribute(acbl);
989 : 1134315 : return true;
990 : : }
991 : : }
992 : : else
993 : : {
994 : : ArithEntailConstantBoundUpper acbu;
995 [ + + ]: 99284 : if (n.hasAttribute(acbu))
996 : : {
997 : 60908 : c = n.getAttribute(acbu);
998 : 60908 : return true;
999 : : }
1000 : : }
1001 : 84854 : return false;
1002 : : }
1003 : :
1004 : 43832 : Node ArithEntail::getConstantBound(TNode a, bool isLower)
1005 : : {
1006 [ - + ][ - + ]: 43832 : Assert(rewriteArith(a) == a);
[ - - ]
1007 : 43832 : Node ret;
1008 [ + + ]: 43832 : if (getConstantBoundCache(a, isLower, ret))
1009 : : {
1010 : 35730 : return ret;
1011 : : }
1012 [ + + ]: 8102 : if (a.isConst())
1013 : : {
1014 : 1812 : ret = a;
1015 : : }
1016 [ + + ]: 6290 : else if (a.getKind() == Kind::STRING_LENGTH)
1017 : : {
1018 [ + - ]: 1029 : if (isLower)
1019 : : {
1020 : 1029 : ret = d_zero;
1021 : : }
1022 : : }
1023 [ + + ][ + + ]: 5261 : else if (a.getKind() == Kind::ADD || a.getKind() == Kind::MULT)
[ + + ]
1024 : : {
1025 : 4389 : std::vector<Node> children;
1026 : 4389 : bool success = true;
1027 [ + + ]: 8229 : for (unsigned i = 0; i < a.getNumChildren(); i++)
1028 : : {
1029 : 7410 : Node ac = getConstantBound(a[i], isLower);
1030 [ + + ]: 7410 : if (ac.isNull())
1031 : : {
1032 : 2402 : success = false;
1033 : 2402 : break;
1034 : : }
1035 : : else
1036 : : {
1037 [ + + ]: 5008 : if (ac.getConst<Rational>().sgn() == 0)
1038 : : {
1039 [ + + ]: 1487 : if (a.getKind() == Kind::MULT)
1040 : : {
1041 : 26 : success = false;
1042 : 26 : break;
1043 : : }
1044 : : }
1045 : : else
1046 : : {
1047 [ + + ]: 3521 : if (a.getKind() == Kind::MULT)
1048 : : {
1049 [ + + ]: 1170 : if ((ac.getConst<Rational>().sgn() > 0) != isLower)
1050 : : {
1051 : 1142 : success = false;
1052 : 1142 : break;
1053 : : }
1054 : : }
1055 : 2379 : children.push_back(ac);
1056 : : }
1057 : : }
1058 [ + + ]: 7410 : }
1059 [ + + ]: 4389 : if (success)
1060 : : {
1061 [ + + ]: 819 : if (children.empty())
1062 : : {
1063 : 286 : ret = d_zero;
1064 : : }
1065 [ + - ]: 533 : else if (children.size() == 1)
1066 : : {
1067 : 533 : ret = children[0];
1068 : : }
1069 : : else
1070 : : {
1071 : 0 : ret = a.getNodeManager()->mkNode(a.getKind(), children);
1072 : 0 : ret = rewriteArith(ret);
1073 : : }
1074 : : }
1075 : 4389 : }
1076 [ + - ]: 16204 : Trace("strings-rewrite-cbound")
1077 [ - - ]: 0 : << "Constant " << (isLower ? "lower" : "upper") << " bound for " << a
1078 : 8102 : << " is " << ret << std::endl;
1079 [ + + ][ + - ]: 8102 : Assert(ret.isNull() || ret.isConst());
[ - + ][ - + ]
[ - - ]
1080 : : // entailment check should be at least as powerful as computing a lower bound
1081 : 8102 : Assert(!isLower || ret.isNull() || ret.getConst<Rational>().sgn() < 0
1082 : : || check(a, false));
1083 : 8102 : Assert(!isLower || ret.isNull() || ret.getConst<Rational>().sgn() <= 0
1084 : : || check(a, true));
1085 : : // cache
1086 : 8102 : setConstantBoundCache(a, ret, isLower);
1087 : 8102 : return ret;
1088 : 0 : }
1089 : :
1090 : 1236245 : Node ArithEntail::getConstantBoundLength(TNode s, bool isLower) const
1091 : : {
1092 [ - + ][ - + ]: 1236245 : Assert(s.getType().isStringLike());
[ - - ]
1093 : 1236245 : Node ret;
1094 [ + + ]: 1236245 : if (getConstantBoundCache(s, isLower, ret))
1095 : : {
1096 : 1159493 : return ret;
1097 : : }
1098 : 76752 : NodeManager* nm = s.getNodeManager();
1099 : 76752 : Kind sk = s.getKind();
1100 [ + + ]: 76752 : if (s.isConst())
1101 : : {
1102 : 13056 : size_t len = Word::getLength(s);
1103 : 13056 : ret = nm->mkConstInt(Rational(len));
1104 : : }
1105 [ + + ][ - + ]: 63696 : else if (sk == Kind::SEQ_UNIT || sk == Kind::STRING_UNIT)
1106 : : {
1107 : 1174 : ret = nm->mkConstInt(1);
1108 : : }
1109 [ + + ]: 62522 : else if (sk == Kind::STRING_CONCAT)
1110 : : {
1111 : 24886 : Rational sum(0);
1112 : 24886 : bool success = true;
1113 [ + + ]: 57764 : for (const Node& sc : s)
1114 : : {
1115 : 45305 : Node b = getConstantBoundLength(sc, isLower);
1116 [ + + ]: 45305 : if (b.isNull())
1117 : : {
1118 [ - + ]: 12427 : if (isLower)
1119 : : {
1120 : : // assume zero and continue
1121 : 0 : continue;
1122 : : }
1123 : 12427 : success = false;
1124 : 12427 : break;
1125 : : }
1126 [ - + ][ - + ]: 32878 : Assert(b.isConst());
[ - - ]
1127 : 32878 : sum = sum + b.getConst<Rational>();
1128 [ + - ][ + + ]: 57732 : }
[ - + ]
1129 [ + + ][ + + ]: 24886 : if (success && (!isLower || sum.sgn() != 0))
[ + + ][ + + ]
1130 : : {
1131 : 5717 : ret = nm->mkConstInt(sum);
1132 : : }
1133 : 24886 : }
1134 [ + + ][ + + ]: 76752 : if (ret.isNull() && isLower)
[ + + ]
1135 : : {
1136 : 25560 : ret = d_zero;
1137 : : }
1138 : : // cache
1139 : 76752 : setConstantBoundCache(s, ret, isLower);
1140 : 76752 : return ret;
1141 : 0 : }
1142 : :
1143 : 1515036 : bool ArithEntail::checkSimple(Node a)
1144 : : {
1145 : : // check whether a >= 0
1146 [ + + ]: 1515036 : if (a.isConst())
1147 : : {
1148 : 603404 : return a.getConst<Rational>().sgn() >= 0;
1149 : : }
1150 [ + + ]: 911632 : else if (a.getKind() == Kind::STRING_LENGTH)
1151 : : {
1152 : : // str.len( t ) >= 0
1153 : 146437 : return true;
1154 : : }
1155 [ + + ][ + + ]: 765195 : else if (a.getKind() == Kind::ADD || a.getKind() == Kind::MULT)
[ + + ]
1156 : : {
1157 [ + + ]: 920149 : for (unsigned i = 0; i < a.getNumChildren(); i++)
1158 : : {
1159 [ + + ]: 906101 : if (!checkSimple(a[i]))
1160 : : {
1161 : 697631 : return false;
1162 : : }
1163 : : }
1164 : : // t1 >= 0 ^ ... ^ tn >= 0 => t1 op ... op tn >= 0
1165 : 14048 : return true;
1166 : : }
1167 : :
1168 : 53516 : return false;
1169 : : }
1170 : :
1171 : 1867 : bool ArithEntail::inferZerosInSumGeq(Node x,
1172 : : std::vector<Node>& ys,
1173 : : std::vector<Node>& zeroYs)
1174 : : {
1175 [ - + ][ - + ]: 1867 : Assert(zeroYs.empty());
[ - - ]
1176 : :
1177 : 1867 : NodeManager* nm = x.getNodeManager();
1178 : :
1179 : : // Check if we can show that y1 + ... + yn >= x
1180 [ + + ]: 1867 : Node sum = (ys.size() > 1) ? nm->mkNode(Kind::ADD, ys) : ys[0];
1181 [ + + ]: 1867 : if (!check(sum, x))
1182 : : {
1183 : 1681 : return false;
1184 : : }
1185 : :
1186 : : // Try to remove yi one-by-one and check if we can still show:
1187 : : //
1188 : : // y1 + ... + yi-1 + yi+1 + ... + yn >= x
1189 : : //
1190 : : // If that's the case, we know that yi can be zero and the inequality still
1191 : : // holds.
1192 : 186 : size_t i = 0;
1193 [ + + ]: 761 : while (i < ys.size())
1194 : : {
1195 : 575 : Node yi = ys[i];
1196 : 575 : std::vector<Node>::iterator pos = ys.erase(ys.begin() + i);
1197 [ + + ]: 575 : if (ys.size() > 1)
1198 : : {
1199 : 298 : sum = nm->mkNode(Kind::ADD, ys);
1200 : : }
1201 : : else
1202 : : {
1203 [ + + ]: 277 : sum = ys.size() == 1 ? ys[0] : d_zero;
1204 : : }
1205 : :
1206 [ + + ]: 575 : if (check(sum, x))
1207 : : {
1208 : 98 : zeroYs.push_back(yi);
1209 : : }
1210 : : else
1211 : : {
1212 : 477 : ys.insert(pos, yi);
1213 : 477 : i++;
1214 : : }
1215 : 575 : }
1216 : 186 : return true;
1217 : 1867 : }
1218 : :
1219 : : } // namespace strings
1220 : : } // namespace theory
1221 : : } // namespace cvc5::internal
|
