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-2021 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 "theory/arith/arith_msum.h" |
21 |
|
#include "theory/rewriter.h" |
22 |
|
#include "theory/strings/theory_strings_utils.h" |
23 |
|
#include "theory/strings/word.h" |
24 |
|
#include "theory/theory.h" |
25 |
|
#include "util/rational.h" |
26 |
|
|
27 |
|
using namespace cvc5::kind; |
28 |
|
|
29 |
|
namespace cvc5 { |
30 |
|
namespace theory { |
31 |
|
namespace strings { |
32 |
|
|
33 |
12826 |
ArithEntail::ArithEntail(Rewriter* r) : d_rr(r) {} |
34 |
|
|
35 |
898 |
bool ArithEntail::checkEq(Node a, Node b) |
36 |
|
{ |
37 |
898 |
if (a == b) |
38 |
|
{ |
39 |
|
return true; |
40 |
|
} |
41 |
1796 |
Node ar = d_rr->rewrite(a); |
42 |
1796 |
Node br = d_rr->rewrite(b); |
43 |
898 |
return ar == br; |
44 |
|
} |
45 |
|
|
46 |
362676 |
bool ArithEntail::check(Node a, Node b, bool strict) |
47 |
|
{ |
48 |
362676 |
if (a == b) |
49 |
|
{ |
50 |
15917 |
return !strict; |
51 |
|
} |
52 |
693518 |
Node diff = NodeManager::currentNM()->mkNode(kind::MINUS, a, b); |
53 |
346759 |
return check(diff, strict); |
54 |
|
} |
55 |
|
|
56 |
|
struct StrCheckEntailArithTag |
57 |
|
{ |
58 |
|
}; |
59 |
|
struct StrCheckEntailArithComputedTag |
60 |
|
{ |
61 |
|
}; |
62 |
|
/** Attribute true for expressions for which check returned true */ |
63 |
|
typedef expr::Attribute<StrCheckEntailArithTag, bool> StrCheckEntailArithAttr; |
64 |
|
typedef expr::Attribute<StrCheckEntailArithComputedTag, bool> |
65 |
|
StrCheckEntailArithComputedAttr; |
66 |
|
|
67 |
626880 |
bool ArithEntail::check(Node a, bool strict) |
68 |
|
{ |
69 |
626880 |
if (a.isConst()) |
70 |
|
{ |
71 |
71600 |
return a.getConst<Rational>().sgn() >= (strict ? 1 : 0); |
72 |
|
} |
73 |
|
|
74 |
|
Node ar = strict ? NodeManager::currentNM()->mkNode( |
75 |
730134 |
kind::MINUS, a, NodeManager::currentNM()->mkConst(Rational(1))) |
76 |
1285414 |
: a; |
77 |
555280 |
ar = d_rr->rewrite(ar); |
78 |
|
|
79 |
555280 |
if (ar.getAttribute(StrCheckEntailArithComputedAttr())) |
80 |
|
{ |
81 |
477472 |
return ar.getAttribute(StrCheckEntailArithAttr()); |
82 |
|
} |
83 |
|
|
84 |
77808 |
bool ret = checkInternal(ar); |
85 |
77808 |
if (!ret) |
86 |
|
{ |
87 |
|
// try with approximations |
88 |
73058 |
ret = checkApprox(ar); |
89 |
|
} |
90 |
|
// cache the result |
91 |
77808 |
ar.setAttribute(StrCheckEntailArithAttr(), ret); |
92 |
77808 |
ar.setAttribute(StrCheckEntailArithComputedAttr(), true); |
93 |
77808 |
return ret; |
94 |
|
} |
95 |
|
|
96 |
73058 |
bool ArithEntail::checkApprox(Node ar) |
97 |
|
{ |
98 |
73058 |
Assert(d_rr->rewrite(ar) == ar); |
99 |
73058 |
NodeManager* nm = NodeManager::currentNM(); |
100 |
146116 |
std::map<Node, Node> msum; |
101 |
146116 |
Trace("strings-ent-approx-debug") |
102 |
73058 |
<< "Setup arithmetic approximations for " << ar << std::endl; |
103 |
73058 |
if (!ArithMSum::getMonomialSum(ar, msum)) |
104 |
|
{ |
105 |
|
Trace("strings-ent-approx-debug") |
106 |
|
<< "...failed to get monomial sum!" << std::endl; |
107 |
|
return false; |
108 |
|
} |
109 |
|
// for each monomial v*c, mApprox[v] a list of |
110 |
|
// possibilities for how the term can be soundly approximated, that is, |
111 |
|
// if mApprox[v] contains av, then v*c > av*c. Notice that if c |
112 |
|
// is positive, then v > av, otherwise if c is negative, then v < av. |
113 |
|
// In other words, av is an under-approximation if c is positive, and an |
114 |
|
// over-approximation if c is negative. |
115 |
73058 |
bool changed = false; |
116 |
146116 |
std::map<Node, std::vector<Node> > mApprox; |
117 |
|
// map from approximations to their monomial sums |
118 |
146116 |
std::map<Node, std::map<Node, Node> > approxMsums; |
119 |
|
// aarSum stores each monomial that does not have multiple approximations |
120 |
146116 |
std::vector<Node> aarSum; |
121 |
235959 |
for (std::pair<const Node, Node>& m : msum) |
122 |
|
{ |
123 |
325802 |
Node v = m.first; |
124 |
325802 |
Node c = m.second; |
125 |
325802 |
Trace("strings-ent-approx-debug") |
126 |
162901 |
<< "Get approximations " << v << "..." << std::endl; |
127 |
162901 |
if (v.isNull()) |
128 |
|
{ |
129 |
112436 |
Node mn = c.isNull() ? nm->mkConst(Rational(1)) : c; |
130 |
56218 |
aarSum.push_back(mn); |
131 |
|
} |
132 |
|
else |
133 |
|
{ |
134 |
|
// c.isNull() means c = 1 |
135 |
106683 |
bool isOverApprox = !c.isNull() && c.getConst<Rational>().sgn() == -1; |
136 |
106683 |
std::vector<Node>& approx = mApprox[v]; |
137 |
213366 |
std::unordered_set<Node> visited; |
138 |
213366 |
std::vector<Node> toProcess; |
139 |
106683 |
toProcess.push_back(v); |
140 |
27105 |
do |
141 |
|
{ |
142 |
267576 |
Node curr = toProcess.back(); |
143 |
133788 |
Trace("strings-ent-approx-debug") << " process " << curr << std::endl; |
144 |
133788 |
curr = d_rr->rewrite(curr); |
145 |
133788 |
toProcess.pop_back(); |
146 |
133788 |
if (visited.find(curr) == visited.end()) |
147 |
|
{ |
148 |
132510 |
visited.insert(curr); |
149 |
265020 |
std::vector<Node> currApprox; |
150 |
132510 |
getArithApproximations(curr, currApprox, isOverApprox); |
151 |
132510 |
if (currApprox.empty()) |
152 |
|
{ |
153 |
227964 |
Trace("strings-ent-approx-debug") |
154 |
113982 |
<< "...approximation: " << curr << std::endl; |
155 |
|
// no approximations, thus curr is a possibility |
156 |
113982 |
approx.push_back(curr); |
157 |
|
} |
158 |
|
else |
159 |
|
{ |
160 |
18528 |
toProcess.insert( |
161 |
37056 |
toProcess.end(), currApprox.begin(), currApprox.end()); |
162 |
|
} |
163 |
|
} |
164 |
133788 |
} while (!toProcess.empty()); |
165 |
106683 |
Assert(!approx.empty()); |
166 |
|
// if we have only one approximation, move it to final |
167 |
106683 |
if (approx.size() == 1) |
168 |
|
{ |
169 |
99489 |
changed = v != approx[0]; |
170 |
198978 |
Node mn = ArithMSum::mkCoeffTerm(c, approx[0]); |
171 |
99489 |
aarSum.push_back(mn); |
172 |
99489 |
mApprox.erase(v); |
173 |
|
} |
174 |
|
else |
175 |
|
{ |
176 |
|
// compute monomial sum form for each approximation, used below |
177 |
21687 |
for (const Node& aa : approx) |
178 |
|
{ |
179 |
14493 |
if (approxMsums.find(aa) == approxMsums.end()) |
180 |
|
{ |
181 |
|
CVC5_UNUSED bool ret = |
182 |
14218 |
ArithMSum::getMonomialSum(aa, approxMsums[aa]); |
183 |
14218 |
Assert(ret); |
184 |
|
} |
185 |
|
} |
186 |
7194 |
changed = true; |
187 |
|
} |
188 |
|
} |
189 |
|
} |
190 |
73058 |
if (!changed) |
191 |
|
{ |
192 |
|
// approximations had no effect, return |
193 |
60941 |
Trace("strings-ent-approx-debug") << "...no approximations" << std::endl; |
194 |
60941 |
return false; |
195 |
|
} |
196 |
|
// get the current "fixed" sum for the abstraction of ar |
197 |
12117 |
Node aar = aarSum.empty() |
198 |
13302 |
? nm->mkConst(Rational(0)) |
199 |
25419 |
: (aarSum.size() == 1 ? aarSum[0] : nm->mkNode(PLUS, aarSum)); |
200 |
12117 |
aar = d_rr->rewrite(aar); |
201 |
24234 |
Trace("strings-ent-approx-debug") |
202 |
24234 |
<< "...processed fixed sum " << aar << " with " << mApprox.size() |
203 |
12117 |
<< " approximated monomials." << std::endl; |
204 |
|
// if we have a choice of how to approximate |
205 |
12117 |
if (!mApprox.empty()) |
206 |
|
{ |
207 |
|
// convert aar back to monomial sum |
208 |
11520 |
std::map<Node, Node> msumAar; |
209 |
5760 |
if (!ArithMSum::getMonomialSum(aar, msumAar)) |
210 |
|
{ |
211 |
|
return false; |
212 |
|
} |
213 |
5760 |
if (Trace.isOn("strings-ent-approx")) |
214 |
|
{ |
215 |
|
Trace("strings-ent-approx") |
216 |
|
<< "---- Check arithmetic entailment by under-approximation " << ar |
217 |
|
<< " >= 0" << std::endl; |
218 |
|
Trace("strings-ent-approx") << "FIXED:" << std::endl; |
219 |
|
ArithMSum::debugPrintMonomialSum(msumAar, "strings-ent-approx"); |
220 |
|
Trace("strings-ent-approx") << "APPROX:" << std::endl; |
221 |
|
for (std::pair<const Node, std::vector<Node> >& a : mApprox) |
222 |
|
{ |
223 |
|
Node c = msum[a.first]; |
224 |
|
Trace("strings-ent-approx") << " "; |
225 |
|
if (!c.isNull()) |
226 |
|
{ |
227 |
|
Trace("strings-ent-approx") << c << " * "; |
228 |
|
} |
229 |
|
Trace("strings-ent-approx") |
230 |
|
<< a.second << " ...from " << a.first << std::endl; |
231 |
|
} |
232 |
|
Trace("strings-ent-approx") << std::endl; |
233 |
|
} |
234 |
11520 |
Rational one(1); |
235 |
|
// incorporate monomials one at a time that have a choice of approximations |
236 |
17350 |
while (!mApprox.empty()) |
237 |
|
{ |
238 |
11590 |
Node v; |
239 |
11590 |
Node vapprox; |
240 |
5795 |
int maxScore = -1; |
241 |
|
// Look at each approximation, take the one with the best score. |
242 |
|
// Notice that we are in the process of trying to prove |
243 |
|
// ( c1*t1 + .. + cn*tn ) + ( approx_1 | ... | approx_m ) >= 0, |
244 |
|
// where c1*t1 + .. + cn*tn is the "fixed" component of our sum (aar) |
245 |
|
// and approx_1 ... approx_m are possible approximations. The |
246 |
|
// intution here is that we want coefficients c1...cn to be positive. |
247 |
|
// This is because arithmetic string terms t1...tn (which may be |
248 |
|
// applications of len, indexof, str.to.int) are never entailed to be |
249 |
|
// negative. Hence, we add the approx_i that contributes the "most" |
250 |
|
// towards making all constants c1...cn positive and cancelling negative |
251 |
|
// monomials in approx_i itself. |
252 |
5795 |
for (std::pair<const Node, std::vector<Node> >& nam : mApprox) |
253 |
|
{ |
254 |
5795 |
Node cr = msum[nam.first]; |
255 |
17488 |
for (const Node& aa : nam.second) |
256 |
|
{ |
257 |
11693 |
unsigned helpsCancelCount = 0; |
258 |
11693 |
unsigned addsObligationCount = 0; |
259 |
11693 |
std::map<Node, Node>::iterator it; |
260 |
|
// we are processing an approximation cr*( c1*t1 + ... + cn*tn ) |
261 |
26028 |
for (std::pair<const Node, Node>& aam : approxMsums[aa]) |
262 |
|
{ |
263 |
|
// Say aar is of the form t + c*ti, and aam is the monomial ci*ti |
264 |
|
// where ci != 0. We say aam: |
265 |
|
// (1) helps cancel if c != 0 and c>0 != ci>0 |
266 |
|
// (2) adds obligation if c>=0 and c+ci<0 |
267 |
28670 |
Node ti = aam.first; |
268 |
28670 |
Node ci = aam.second; |
269 |
14335 |
if (!cr.isNull()) |
270 |
|
{ |
271 |
14335 |
ci = ci.isNull() ? cr : d_rr->rewrite(nm->mkNode(MULT, ci, cr)); |
272 |
|
} |
273 |
14335 |
Trace("strings-ent-approx-debug") << ci << "*" << ti << " "; |
274 |
14335 |
int ciSgn = ci.isNull() ? 1 : ci.getConst<Rational>().sgn(); |
275 |
14335 |
it = msumAar.find(ti); |
276 |
14335 |
if (it != msumAar.end()) |
277 |
|
{ |
278 |
16356 |
Node c = it->second; |
279 |
8178 |
int cSgn = c.isNull() ? 1 : c.getConst<Rational>().sgn(); |
280 |
8178 |
if (cSgn == 0) |
281 |
|
{ |
282 |
1523 |
addsObligationCount += (ciSgn == -1 ? 1 : 0); |
283 |
|
} |
284 |
6655 |
else if (cSgn != ciSgn) |
285 |
|
{ |
286 |
5763 |
helpsCancelCount++; |
287 |
11526 |
Rational r1 = c.isNull() ? one : c.getConst<Rational>(); |
288 |
11526 |
Rational r2 = ci.isNull() ? one : ci.getConst<Rational>(); |
289 |
11526 |
Rational r12 = r1 + r2; |
290 |
5763 |
if (r12.sgn() == -1) |
291 |
|
{ |
292 |
4142 |
addsObligationCount++; |
293 |
|
} |
294 |
|
} |
295 |
|
} |
296 |
|
else |
297 |
|
{ |
298 |
6157 |
addsObligationCount += (ciSgn == -1 ? 1 : 0); |
299 |
|
} |
300 |
|
} |
301 |
23386 |
Trace("strings-ent-approx-debug") |
302 |
11693 |
<< "counts=" << helpsCancelCount << "," << addsObligationCount |
303 |
11693 |
<< " for " << aa << " into " << aar << std::endl; |
304 |
23386 |
int score = (addsObligationCount > 0 ? 0 : 2) |
305 |
11693 |
+ (helpsCancelCount > 0 ? 1 : 0); |
306 |
|
// if its the best, update v and vapprox |
307 |
11693 |
if (v.isNull() || score > maxScore) |
308 |
|
{ |
309 |
7852 |
v = nam.first; |
310 |
7852 |
vapprox = aa; |
311 |
7852 |
maxScore = score; |
312 |
|
} |
313 |
|
} |
314 |
5795 |
if (!v.isNull()) |
315 |
|
{ |
316 |
5795 |
break; |
317 |
|
} |
318 |
|
} |
319 |
11590 |
Trace("strings-ent-approx") |
320 |
5795 |
<< "- Decide " << v << " = " << vapprox << std::endl; |
321 |
|
// we incorporate v approximated by vapprox into the overall approximation |
322 |
|
// for ar |
323 |
5795 |
Assert(!v.isNull() && !vapprox.isNull()); |
324 |
5795 |
Assert(msum.find(v) != msum.end()); |
325 |
11590 |
Node mn = ArithMSum::mkCoeffTerm(msum[v], vapprox); |
326 |
5795 |
aar = nm->mkNode(PLUS, aar, mn); |
327 |
|
// update the msumAar map |
328 |
5795 |
aar = d_rr->rewrite(aar); |
329 |
5795 |
msumAar.clear(); |
330 |
5795 |
if (!ArithMSum::getMonomialSum(aar, msumAar)) |
331 |
|
{ |
332 |
|
Assert(false); |
333 |
|
Trace("strings-ent-approx") |
334 |
|
<< "...failed to get monomial sum!" << std::endl; |
335 |
|
return false; |
336 |
|
} |
337 |
|
// we have processed the approximation for v |
338 |
5795 |
mApprox.erase(v); |
339 |
|
} |
340 |
5760 |
Trace("strings-ent-approx") << "-----------------" << std::endl; |
341 |
|
} |
342 |
12117 |
if (aar == ar) |
343 |
|
{ |
344 |
|
Trace("strings-ent-approx-debug") |
345 |
|
<< "...approximation had no effect" << std::endl; |
346 |
|
// this should never happen, but we avoid the infinite loop for sanity here |
347 |
|
Assert(false); |
348 |
|
return false; |
349 |
|
} |
350 |
|
// Check entailment on the approximation of ar. |
351 |
|
// Notice that this may trigger further reasoning by approximation. For |
352 |
|
// example, len( replace( x ++ y, substr( x, 0, n ), z ) ) may be |
353 |
|
// under-approximated as len( x ) + len( y ) - len( substr( x, 0, n ) ) on |
354 |
|
// this call, where in the recursive call we may over-approximate |
355 |
|
// len( substr( x, 0, n ) ) as len( x ). In this example, we can infer |
356 |
|
// that len( replace( x ++ y, substr( x, 0, n ), z ) ) >= len( y ) in two |
357 |
|
// steps. |
358 |
12117 |
if (check(aar)) |
359 |
|
{ |
360 |
2408 |
Trace("strings-ent-approx") |
361 |
1204 |
<< "*** StrArithApprox: showed " << ar |
362 |
1204 |
<< " >= 0 using under-approximation!" << std::endl; |
363 |
2408 |
Trace("strings-ent-approx") |
364 |
1204 |
<< "*** StrArithApprox: under-approximation was " << aar << std::endl; |
365 |
1204 |
return true; |
366 |
|
} |
367 |
10913 |
return false; |
368 |
|
} |
369 |
|
|
370 |
132791 |
void ArithEntail::getArithApproximations(Node a, |
371 |
|
std::vector<Node>& approx, |
372 |
|
bool isOverApprox) |
373 |
|
{ |
374 |
132791 |
NodeManager* nm = NodeManager::currentNM(); |
375 |
|
// We do not handle PLUS here since this leads to exponential behavior. |
376 |
|
// Instead, this is managed, e.g. during checkApprox, where |
377 |
|
// PLUS terms are expanded "on-demand" during the reasoning. |
378 |
265582 |
Trace("strings-ent-approx-debug") |
379 |
132791 |
<< "Get arith approximations " << a << std::endl; |
380 |
132791 |
Kind ak = a.getKind(); |
381 |
132791 |
if (ak == MULT) |
382 |
|
{ |
383 |
562 |
Node c; |
384 |
562 |
Node v; |
385 |
281 |
if (ArithMSum::getMonomial(a, c, v)) |
386 |
|
{ |
387 |
281 |
bool isNeg = c.getConst<Rational>().sgn() == -1; |
388 |
281 |
getArithApproximations(v, approx, isNeg ? !isOverApprox : isOverApprox); |
389 |
341 |
for (unsigned i = 0, size = approx.size(); i < size; i++) |
390 |
|
{ |
391 |
60 |
approx[i] = nm->mkNode(MULT, c, approx[i]); |
392 |
|
} |
393 |
|
} |
394 |
|
} |
395 |
132510 |
else if (ak == STRING_LENGTH) |
396 |
|
{ |
397 |
106145 |
Kind aak = a[0].getKind(); |
398 |
106145 |
if (aak == STRING_SUBSTR) |
399 |
|
{ |
400 |
|
// over,under-approximations for len( substr( x, n, m ) ) |
401 |
43226 |
Node lenx = nm->mkNode(STRING_LENGTH, a[0][0]); |
402 |
21613 |
if (isOverApprox) |
403 |
|
{ |
404 |
|
// m >= 0 implies |
405 |
|
// m >= len( substr( x, n, m ) ) |
406 |
13070 |
if (check(a[0][2])) |
407 |
|
{ |
408 |
8265 |
approx.push_back(a[0][2]); |
409 |
|
} |
410 |
13070 |
if (check(lenx, a[0][1])) |
411 |
|
{ |
412 |
|
// n <= len( x ) implies |
413 |
|
// len( x ) - n >= len( substr( x, n, m ) ) |
414 |
3953 |
approx.push_back(nm->mkNode(MINUS, lenx, a[0][1])); |
415 |
|
} |
416 |
|
else |
417 |
|
{ |
418 |
|
// len( x ) >= len( substr( x, n, m ) ) |
419 |
9117 |
approx.push_back(lenx); |
420 |
|
} |
421 |
|
} |
422 |
|
else |
423 |
|
{ |
424 |
|
// 0 <= n and n+m <= len( x ) implies |
425 |
|
// m <= len( substr( x, n, m ) ) |
426 |
17086 |
Node npm = nm->mkNode(PLUS, a[0][1], a[0][2]); |
427 |
8543 |
if (check(a[0][1]) && check(lenx, npm)) |
428 |
|
{ |
429 |
571 |
approx.push_back(a[0][2]); |
430 |
|
} |
431 |
|
// 0 <= n and n+m >= len( x ) implies |
432 |
|
// len(x)-n <= len( substr( x, n, m ) ) |
433 |
8543 |
if (check(a[0][1]) && check(npm, lenx)) |
434 |
|
{ |
435 |
407 |
approx.push_back(nm->mkNode(MINUS, lenx, a[0][1])); |
436 |
|
} |
437 |
|
} |
438 |
|
} |
439 |
84532 |
else if (aak == STRING_REPLACE) |
440 |
|
{ |
441 |
|
// over,under-approximations for len( replace( x, y, z ) ) |
442 |
|
// notice this is either len( x ) or ( len( x ) + len( z ) - len( y ) ) |
443 |
3908 |
Node lenx = nm->mkNode(STRING_LENGTH, a[0][0]); |
444 |
3908 |
Node leny = nm->mkNode(STRING_LENGTH, a[0][1]); |
445 |
3908 |
Node lenz = nm->mkNode(STRING_LENGTH, a[0][2]); |
446 |
1954 |
if (isOverApprox) |
447 |
|
{ |
448 |
1092 |
if (check(leny, lenz)) |
449 |
|
{ |
450 |
|
// len( y ) >= len( z ) implies |
451 |
|
// len( x ) >= len( replace( x, y, z ) ) |
452 |
306 |
approx.push_back(lenx); |
453 |
|
} |
454 |
|
else |
455 |
|
{ |
456 |
|
// len( x ) + len( z ) >= len( replace( x, y, z ) ) |
457 |
786 |
approx.push_back(nm->mkNode(PLUS, lenx, lenz)); |
458 |
|
} |
459 |
|
} |
460 |
|
else |
461 |
|
{ |
462 |
862 |
if (check(lenz, leny) || check(lenz, lenx)) |
463 |
|
{ |
464 |
|
// len( y ) <= len( z ) or len( x ) <= len( z ) implies |
465 |
|
// len( x ) <= len( replace( x, y, z ) ) |
466 |
435 |
approx.push_back(lenx); |
467 |
|
} |
468 |
|
else |
469 |
|
{ |
470 |
|
// len( x ) - len( y ) <= len( replace( x, y, z ) ) |
471 |
427 |
approx.push_back(nm->mkNode(MINUS, lenx, leny)); |
472 |
|
} |
473 |
|
} |
474 |
|
} |
475 |
82578 |
else if (aak == STRING_ITOS) |
476 |
|
{ |
477 |
|
// over,under-approximations for len( int.to.str( x ) ) |
478 |
200 |
if (isOverApprox) |
479 |
|
{ |
480 |
106 |
if (check(a[0][0], false)) |
481 |
|
{ |
482 |
38 |
if (check(a[0][0], true)) |
483 |
|
{ |
484 |
|
// x > 0 implies |
485 |
|
// x >= len( int.to.str( x ) ) |
486 |
5 |
approx.push_back(a[0][0]); |
487 |
|
} |
488 |
|
else |
489 |
|
{ |
490 |
|
// x >= 0 implies |
491 |
|
// x+1 >= len( int.to.str( x ) ) |
492 |
33 |
approx.push_back( |
493 |
66 |
nm->mkNode(PLUS, nm->mkConst(Rational(1)), a[0][0])); |
494 |
|
} |
495 |
|
} |
496 |
|
} |
497 |
|
else |
498 |
|
{ |
499 |
94 |
if (check(a[0][0])) |
500 |
|
{ |
501 |
|
// x >= 0 implies |
502 |
|
// len( int.to.str( x ) ) >= 1 |
503 |
22 |
approx.push_back(nm->mkConst(Rational(1))); |
504 |
|
} |
505 |
|
// other crazy things are possible here, e.g. |
506 |
|
// len( int.to.str( len( y ) + 10 ) ) >= 2 |
507 |
|
} |
508 |
|
} |
509 |
|
} |
510 |
26365 |
else if (ak == STRING_INDEXOF) |
511 |
|
{ |
512 |
|
// over,under-approximations for indexof( x, y, n ) |
513 |
2778 |
if (isOverApprox) |
514 |
|
{ |
515 |
3104 |
Node lenx = nm->mkNode(STRING_LENGTH, a[0]); |
516 |
3104 |
Node leny = nm->mkNode(STRING_LENGTH, a[1]); |
517 |
1552 |
if (check(lenx, leny)) |
518 |
|
{ |
519 |
|
// len( x ) >= len( y ) implies |
520 |
|
// len( x ) - len( y ) >= indexof( x, y, n ) |
521 |
13 |
approx.push_back(nm->mkNode(MINUS, lenx, leny)); |
522 |
|
} |
523 |
|
else |
524 |
|
{ |
525 |
|
// len( x ) >= indexof( x, y, n ) |
526 |
1539 |
approx.push_back(lenx); |
527 |
|
} |
528 |
|
} |
529 |
|
else |
530 |
|
{ |
531 |
|
// TODO?: |
532 |
|
// contains( substr( x, n, len( x ) ), y ) implies |
533 |
|
// n <= indexof( x, y, n ) |
534 |
|
// ...hard to test, runs risk of non-termination |
535 |
|
|
536 |
|
// -1 <= indexof( x, y, n ) |
537 |
1226 |
approx.push_back(nm->mkConst(Rational(-1))); |
538 |
|
} |
539 |
|
} |
540 |
23587 |
else if (ak == STRING_STOI) |
541 |
|
{ |
542 |
|
// over,under-approximations for str.to.int( x ) |
543 |
|
if (isOverApprox) |
544 |
|
{ |
545 |
|
// TODO?: |
546 |
|
// y >= 0 implies |
547 |
|
// y >= str.to.int( int.to.str( y ) ) |
548 |
|
} |
549 |
|
else |
550 |
|
{ |
551 |
|
// -1 <= str.to.int( x ) |
552 |
|
approx.push_back(nm->mkConst(Rational(-1))); |
553 |
|
} |
554 |
|
} |
555 |
132791 |
Trace("strings-ent-approx-debug") << "Return " << approx.size() << std::endl; |
556 |
132791 |
} |
557 |
|
|
558 |
63443 |
bool ArithEntail::checkWithEqAssumption(Node assumption, Node a, bool strict) |
559 |
|
{ |
560 |
63443 |
Assert(assumption.getKind() == kind::EQUAL); |
561 |
63443 |
Assert(d_rr->rewrite(assumption) == assumption); |
562 |
126886 |
Trace("strings-entail") << "checkWithEqAssumption: " << assumption << " " << a |
563 |
63443 |
<< ", strict=" << strict << std::endl; |
564 |
|
|
565 |
|
// Find candidates variables to compute substitutions for |
566 |
126886 |
std::unordered_set<Node> candVars; |
567 |
126886 |
std::vector<Node> toVisit = {assumption}; |
568 |
827301 |
while (!toVisit.empty()) |
569 |
|
{ |
570 |
763858 |
Node curr = toVisit.back(); |
571 |
381929 |
toVisit.pop_back(); |
572 |
|
|
573 |
1092656 |
if (curr.getKind() == kind::PLUS || curr.getKind() == kind::MULT |
574 |
683481 |
|| curr.getKind() == kind::MINUS || curr.getKind() == kind::EQUAL) |
575 |
|
{ |
576 |
462306 |
for (const auto& currChild : curr) |
577 |
|
{ |
578 |
318486 |
toVisit.push_back(currChild); |
579 |
|
} |
580 |
|
} |
581 |
238109 |
else if (curr.isVar() && Theory::theoryOf(curr) == THEORY_ARITH) |
582 |
|
{ |
583 |
12398 |
candVars.insert(curr); |
584 |
|
} |
585 |
225711 |
else if (curr.getKind() == kind::STRING_LENGTH) |
586 |
|
{ |
587 |
137515 |
candVars.insert(curr); |
588 |
|
} |
589 |
|
} |
590 |
|
|
591 |
|
// Check if any of the candidate variables are in n |
592 |
126886 |
Node v; |
593 |
63443 |
Assert(toVisit.empty()); |
594 |
63443 |
toVisit.push_back(a); |
595 |
625601 |
while (!toVisit.empty()) |
596 |
|
{ |
597 |
584982 |
Node curr = toVisit.back(); |
598 |
303903 |
toVisit.pop_back(); |
599 |
|
|
600 |
607302 |
for (const auto& currChild : curr) |
601 |
|
{ |
602 |
303399 |
toVisit.push_back(currChild); |
603 |
|
} |
604 |
|
|
605 |
303903 |
if (candVars.find(curr) != candVars.end()) |
606 |
|
{ |
607 |
22824 |
v = curr; |
608 |
22824 |
break; |
609 |
|
} |
610 |
|
} |
611 |
|
|
612 |
63443 |
if (v.isNull()) |
613 |
|
{ |
614 |
|
// No suitable candidate found |
615 |
40619 |
return false; |
616 |
|
} |
617 |
|
|
618 |
45648 |
Node solution = ArithMSum::solveEqualityFor(assumption, v); |
619 |
22824 |
if (solution.isNull()) |
620 |
|
{ |
621 |
|
// Could not solve for v |
622 |
38 |
return false; |
623 |
|
} |
624 |
45572 |
Trace("strings-entail") << "checkWithEqAssumption: subs " << v << " -> " |
625 |
22786 |
<< solution << std::endl; |
626 |
|
|
627 |
|
// use capture avoiding substitution |
628 |
22786 |
a = expr::substituteCaptureAvoiding(a, v, solution); |
629 |
22786 |
return check(a, strict); |
630 |
|
} |
631 |
|
|
632 |
96570 |
bool ArithEntail::checkWithAssumption(Node assumption, |
633 |
|
Node a, |
634 |
|
Node b, |
635 |
|
bool strict) |
636 |
|
{ |
637 |
96570 |
Assert(d_rr->rewrite(assumption) == assumption); |
638 |
|
|
639 |
96570 |
NodeManager* nm = NodeManager::currentNM(); |
640 |
|
|
641 |
96570 |
if (!assumption.isConst() && assumption.getKind() != kind::EQUAL) |
642 |
|
{ |
643 |
|
// We rewrite inequality assumptions from x <= y to x + (str.len s) = y |
644 |
|
// where s is some fresh string variable. We use (str.len s) because |
645 |
|
// (str.len s) must be non-negative for the equation to hold. |
646 |
126870 |
Node x, y; |
647 |
63435 |
if (assumption.getKind() == kind::GEQ) |
648 |
|
{ |
649 |
52371 |
x = assumption[0]; |
650 |
52371 |
y = assumption[1]; |
651 |
|
} |
652 |
|
else |
653 |
|
{ |
654 |
|
// (not (>= s t)) --> (>= (t - 1) s) |
655 |
11064 |
Assert(assumption.getKind() == kind::NOT |
656 |
|
&& assumption[0].getKind() == kind::GEQ); |
657 |
11064 |
x = nm->mkNode(kind::MINUS, assumption[0][1], nm->mkConst(Rational(1))); |
658 |
11064 |
y = assumption[0][0]; |
659 |
|
} |
660 |
|
|
661 |
126870 |
Node s = nm->mkBoundVar("slackVal", nm->stringType()); |
662 |
126870 |
Node slen = nm->mkNode(kind::STRING_LENGTH, s); |
663 |
63435 |
assumption = d_rr->rewrite( |
664 |
126870 |
nm->mkNode(kind::EQUAL, x, nm->mkNode(kind::PLUS, y, slen))); |
665 |
|
} |
666 |
|
|
667 |
193140 |
Node diff = nm->mkNode(kind::MINUS, a, b); |
668 |
96570 |
bool res = false; |
669 |
96570 |
if (assumption.isConst()) |
670 |
|
{ |
671 |
33127 |
bool assumptionBool = assumption.getConst<bool>(); |
672 |
33127 |
if (assumptionBool) |
673 |
|
{ |
674 |
33127 |
res = check(diff, strict); |
675 |
|
} |
676 |
|
else |
677 |
|
{ |
678 |
|
res = true; |
679 |
|
} |
680 |
|
} |
681 |
|
else |
682 |
|
{ |
683 |
63443 |
res = checkWithEqAssumption(assumption, diff, strict); |
684 |
|
} |
685 |
193140 |
return res; |
686 |
|
} |
687 |
|
|
688 |
|
bool ArithEntail::checkWithAssumptions(std::vector<Node> assumptions, |
689 |
|
Node a, |
690 |
|
Node b, |
691 |
|
bool strict) |
692 |
|
{ |
693 |
|
// TODO: We currently try to show the entailment with each assumption |
694 |
|
// independently. In the future, we should make better use of multiple |
695 |
|
// assumptions. |
696 |
|
bool res = false; |
697 |
|
for (const auto& assumption : assumptions) |
698 |
|
{ |
699 |
|
Assert(d_rr->rewrite(assumption) == assumption); |
700 |
|
|
701 |
|
if (checkWithAssumption(assumption, a, b, strict)) |
702 |
|
{ |
703 |
|
res = true; |
704 |
|
break; |
705 |
|
} |
706 |
|
} |
707 |
|
return res; |
708 |
|
} |
709 |
|
|
710 |
33789 |
Node ArithEntail::getConstantBound(Node a, bool isLower) |
711 |
|
{ |
712 |
33789 |
Assert(d_rr->rewrite(a) == a); |
713 |
33789 |
Node ret; |
714 |
33789 |
if (a.isConst()) |
715 |
|
{ |
716 |
14774 |
ret = a; |
717 |
|
} |
718 |
19015 |
else if (a.getKind() == kind::STRING_LENGTH) |
719 |
|
{ |
720 |
3414 |
if (isLower) |
721 |
|
{ |
722 |
3414 |
ret = NodeManager::currentNM()->mkConst(Rational(0)); |
723 |
|
} |
724 |
|
} |
725 |
15601 |
else if (a.getKind() == kind::PLUS || a.getKind() == kind::MULT) |
726 |
|
{ |
727 |
22144 |
std::vector<Node> children; |
728 |
11072 |
bool success = true; |
729 |
19839 |
for (unsigned i = 0; i < a.getNumChildren(); i++) |
730 |
|
{ |
731 |
27241 |
Node ac = getConstantBound(a[i], isLower); |
732 |
18474 |
if (ac.isNull()) |
733 |
|
{ |
734 |
5164 |
ret = ac; |
735 |
5164 |
success = false; |
736 |
5164 |
break; |
737 |
|
} |
738 |
|
else |
739 |
|
{ |
740 |
13310 |
if (ac.getConst<Rational>().sgn() == 0) |
741 |
|
{ |
742 |
2916 |
if (a.getKind() == kind::MULT) |
743 |
|
{ |
744 |
71 |
ret = ac; |
745 |
71 |
success = false; |
746 |
71 |
break; |
747 |
|
} |
748 |
|
} |
749 |
|
else |
750 |
|
{ |
751 |
10394 |
if (a.getKind() == kind::MULT) |
752 |
|
{ |
753 |
4547 |
if ((ac.getConst<Rational>().sgn() > 0) != isLower) |
754 |
|
{ |
755 |
4472 |
ret = Node::null(); |
756 |
4472 |
success = false; |
757 |
4472 |
break; |
758 |
|
} |
759 |
|
} |
760 |
5922 |
children.push_back(ac); |
761 |
|
} |
762 |
|
} |
763 |
|
} |
764 |
11072 |
if (success) |
765 |
|
{ |
766 |
1365 |
if (children.empty()) |
767 |
|
{ |
768 |
238 |
ret = NodeManager::currentNM()->mkConst(Rational(0)); |
769 |
|
} |
770 |
1127 |
else if (children.size() == 1) |
771 |
|
{ |
772 |
1127 |
ret = children[0]; |
773 |
|
} |
774 |
|
else |
775 |
|
{ |
776 |
|
ret = NodeManager::currentNM()->mkNode(a.getKind(), children); |
777 |
|
ret = d_rr->rewrite(ret); |
778 |
|
} |
779 |
|
} |
780 |
|
} |
781 |
67578 |
Trace("strings-rewrite-cbound") |
782 |
33789 |
<< "Constant " << (isLower ? "lower" : "upper") << " bound for " << a |
783 |
33789 |
<< " is " << ret << std::endl; |
784 |
33789 |
Assert(ret.isNull() || ret.isConst()); |
785 |
|
// entailment check should be at least as powerful as computing a lower bound |
786 |
33789 |
Assert(!isLower || ret.isNull() || ret.getConst<Rational>().sgn() < 0 |
787 |
|
|| check(a, false)); |
788 |
33789 |
Assert(!isLower || ret.isNull() || ret.getConst<Rational>().sgn() <= 0 |
789 |
|
|| check(a, true)); |
790 |
33789 |
return ret; |
791 |
|
} |
792 |
|
|
793 |
191648 |
bool ArithEntail::checkInternal(Node a) |
794 |
|
{ |
795 |
191648 |
Assert(d_rr->rewrite(a) == a); |
796 |
|
// check whether a >= 0 |
797 |
191648 |
if (a.isConst()) |
798 |
|
{ |
799 |
86975 |
return a.getConst<Rational>().sgn() >= 0; |
800 |
|
} |
801 |
104673 |
else if (a.getKind() == kind::STRING_LENGTH) |
802 |
|
{ |
803 |
|
// str.len( t ) >= 0 |
804 |
7951 |
return true; |
805 |
|
} |
806 |
96722 |
else if (a.getKind() == kind::PLUS || a.getKind() == kind::MULT) |
807 |
|
{ |
808 |
115539 |
for (unsigned i = 0; i < a.getNumChildren(); i++) |
809 |
|
{ |
810 |
113840 |
if (!checkInternal(a[i])) |
811 |
|
{ |
812 |
92274 |
return false; |
813 |
|
} |
814 |
|
} |
815 |
|
// t1 >= 0 ^ ... ^ tn >= 0 => t1 op ... op tn >= 0 |
816 |
1699 |
return true; |
817 |
|
} |
818 |
|
|
819 |
2749 |
return false; |
820 |
|
} |
821 |
|
|
822 |
645 |
bool ArithEntail::inferZerosInSumGeq(Node x, |
823 |
|
std::vector<Node>& ys, |
824 |
|
std::vector<Node>& zeroYs) |
825 |
|
{ |
826 |
645 |
Assert(zeroYs.empty()); |
827 |
|
|
828 |
645 |
NodeManager* nm = NodeManager::currentNM(); |
829 |
|
|
830 |
|
// Check if we can show that y1 + ... + yn >= x |
831 |
1290 |
Node sum = (ys.size() > 1) ? nm->mkNode(PLUS, ys) : ys[0]; |
832 |
645 |
if (!check(sum, x)) |
833 |
|
{ |
834 |
567 |
return false; |
835 |
|
} |
836 |
|
|
837 |
|
// Try to remove yi one-by-one and check if we can still show: |
838 |
|
// |
839 |
|
// y1 + ... + yi-1 + yi+1 + ... + yn >= x |
840 |
|
// |
841 |
|
// If that's the case, we know that yi can be zero and the inequality still |
842 |
|
// holds. |
843 |
78 |
size_t i = 0; |
844 |
422 |
while (i < ys.size()) |
845 |
|
{ |
846 |
344 |
Node yi = ys[i]; |
847 |
172 |
std::vector<Node>::iterator pos = ys.erase(ys.begin() + i); |
848 |
172 |
if (ys.size() > 1) |
849 |
|
{ |
850 |
60 |
sum = nm->mkNode(PLUS, ys); |
851 |
|
} |
852 |
|
else |
853 |
|
{ |
854 |
112 |
sum = ys.size() == 1 ? ys[0] : nm->mkConst(Rational(0)); |
855 |
|
} |
856 |
|
|
857 |
172 |
if (check(sum, x)) |
858 |
|
{ |
859 |
32 |
zeroYs.push_back(yi); |
860 |
|
} |
861 |
|
else |
862 |
|
{ |
863 |
140 |
ys.insert(pos, yi); |
864 |
140 |
i++; |
865 |
|
} |
866 |
|
} |
867 |
78 |
return true; |
868 |
|
} |
869 |
|
|
870 |
|
} // namespace strings |
871 |
|
} // namespace theory |
872 |
22755 |
} // namespace cvc5 |