1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Andres Noetzli, Tianyi Liang |
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 |
|
* Base solver for the theory of strings. This class implements term |
14 |
|
* indexing and constant inference for the theory of strings. |
15 |
|
*/ |
16 |
|
|
17 |
|
#include "theory/strings/base_solver.h" |
18 |
|
|
19 |
|
#include "expr/sequence.h" |
20 |
|
#include "options/strings_options.h" |
21 |
|
#include "theory/rewriter.h" |
22 |
|
#include "theory/strings/theory_strings_utils.h" |
23 |
|
#include "theory/strings/word.h" |
24 |
|
#include "util/rational.h" |
25 |
|
|
26 |
|
using namespace std; |
27 |
|
using namespace cvc5::context; |
28 |
|
using namespace cvc5::kind; |
29 |
|
|
30 |
|
namespace cvc5 { |
31 |
|
namespace theory { |
32 |
|
namespace strings { |
33 |
|
|
34 |
9853 |
BaseSolver::BaseSolver(SolverState& s, InferenceManager& im) |
35 |
9853 |
: d_state(s), d_im(im), d_congruent(s.getSatContext()) |
36 |
|
{ |
37 |
9853 |
d_false = NodeManager::currentNM()->mkConst(false); |
38 |
9853 |
d_cardSize = utils::getAlphabetCardinality(); |
39 |
9853 |
} |
40 |
|
|
41 |
9853 |
BaseSolver::~BaseSolver() {} |
42 |
|
|
43 |
37049 |
void BaseSolver::checkInit() |
44 |
|
{ |
45 |
|
// build term index |
46 |
37049 |
d_eqcInfo.clear(); |
47 |
37049 |
d_termIndex.clear(); |
48 |
37049 |
d_stringsEqc.clear(); |
49 |
|
|
50 |
37049 |
Trace("strings-base") << "BaseSolver::checkInit" << std::endl; |
51 |
|
// count of congruent, non-congruent per operator (independent of type), |
52 |
|
// for debugging. |
53 |
74098 |
std::map<Kind, std::pair<uint32_t, uint32_t>> congruentCount; |
54 |
37049 |
eq::EqualityEngine* ee = d_state.getEqualityEngine(); |
55 |
37049 |
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee); |
56 |
3655565 |
while (!eqcs_i.isFinished()) |
57 |
|
{ |
58 |
3618516 |
Node eqc = (*eqcs_i); |
59 |
3618516 |
TypeNode tn = eqc.getType(); |
60 |
1809258 |
if (!tn.isRegExp()) |
61 |
|
{ |
62 |
3293486 |
Node emps; |
63 |
|
// get the term index for type tn |
64 |
1646743 |
std::map<Kind, TermIndex>& tti = d_termIndex[tn]; |
65 |
1646743 |
if (tn.isStringLike()) |
66 |
|
{ |
67 |
646741 |
d_stringsEqc.push_back(eqc); |
68 |
646741 |
emps = Word::mkEmptyWord(tn); |
69 |
|
} |
70 |
3293486 |
Node var; |
71 |
1646743 |
eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee); |
72 |
22450821 |
while (!eqc_i.isFinished()) |
73 |
|
{ |
74 |
20804078 |
Node n = *eqc_i; |
75 |
10402039 |
Kind k = n.getKind(); |
76 |
10402039 |
Trace("strings-base") << "initialize term: " << n << std::endl; |
77 |
|
// process constant-like terms |
78 |
10402039 |
if (utils::isConstantLike(n)) |
79 |
|
{ |
80 |
925442 |
Node prev = d_eqcInfo[eqc].d_bestContent; |
81 |
462721 |
if (!prev.isNull()) |
82 |
|
{ |
83 |
|
// we have either (seq.unit x) = C, or (seq.unit x) = (seq.unit y) |
84 |
|
// where C is a sequence constant. |
85 |
|
Node cval = |
86 |
300 |
prev.isConst() ? prev : (n.isConst() ? n : Node::null()); |
87 |
300 |
std::vector<Node> exp; |
88 |
150 |
exp.push_back(prev.eqNode(n)); |
89 |
300 |
Node s, t; |
90 |
150 |
if (cval.isNull()) |
91 |
|
{ |
92 |
|
// injectivity of seq.unit |
93 |
26 |
s = prev[0]; |
94 |
26 |
t = n[0]; |
95 |
|
} |
96 |
|
else |
97 |
|
{ |
98 |
|
// should not have two constants in the same equivalence class |
99 |
124 |
Assert(cval.getType().isSequence()); |
100 |
248 |
std::vector<Node> cchars = Word::getChars(cval); |
101 |
124 |
if (cchars.size() == 1) |
102 |
|
{ |
103 |
248 |
Node oval = prev.isConst() ? n : prev; |
104 |
124 |
Assert(oval.getKind() == SEQ_UNIT); |
105 |
124 |
s = oval[0]; |
106 |
124 |
t = cchars[0].getConst<Sequence>().getVec()[0]; |
107 |
|
// oval is congruent (ignored) in this context |
108 |
124 |
d_congruent.insert(oval); |
109 |
|
} |
110 |
|
else |
111 |
|
{ |
112 |
|
// (seq.unit x) = C => false if |C| != 1. |
113 |
|
d_im.sendInference( |
114 |
|
exp, d_false, InferenceId::STRINGS_UNIT_CONST_CONFLICT); |
115 |
|
return; |
116 |
|
} |
117 |
|
} |
118 |
150 |
if (!d_state.areEqual(s, t)) |
119 |
|
{ |
120 |
|
// (seq.unit x) = (seq.unit y) => x=y, or |
121 |
|
// (seq.unit x) = (seq.unit c) => x=c |
122 |
38 |
Assert(s.getType() == t.getType()); |
123 |
38 |
d_im.sendInference(exp, s.eqNode(t), InferenceId::STRINGS_UNIT_INJ); |
124 |
|
} |
125 |
|
} |
126 |
|
// update best content |
127 |
462721 |
if (prev.isNull() || n.isConst()) |
128 |
|
{ |
129 |
462571 |
d_eqcInfo[eqc].d_bestContent = n; |
130 |
462571 |
d_eqcInfo[eqc].d_bestScore = 0; |
131 |
462571 |
d_eqcInfo[eqc].d_base = n; |
132 |
462571 |
d_eqcInfo[eqc].d_exp = Node::null(); |
133 |
|
} |
134 |
|
} |
135 |
10402039 |
if (tn.isInteger()) |
136 |
|
{ |
137 |
|
// do nothing |
138 |
|
} |
139 |
|
// process indexing |
140 |
7986779 |
else if (n.getNumChildren() > 0) |
141 |
|
{ |
142 |
5880900 |
if (k != EQUAL) |
143 |
|
{ |
144 |
1346573 |
if (d_congruent.find(n) == d_congruent.end()) |
145 |
|
{ |
146 |
2049072 |
std::vector<Node> c; |
147 |
2049072 |
Node nc = tti[k].add(n, 0, d_state, emps, c); |
148 |
1024536 |
if (nc != n) |
149 |
|
{ |
150 |
209884 |
Trace("strings-base-debug") |
151 |
104942 |
<< "...found congruent term " << nc << std::endl; |
152 |
|
// check if we have inferred a new equality by removal of empty |
153 |
|
// components |
154 |
104942 |
if (k == STRING_CONCAT && !d_state.areEqual(nc, n)) |
155 |
|
{ |
156 |
11874 |
std::vector<Node> exp; |
157 |
|
// the number of empty components of n, nc |
158 |
5937 |
size_t count[2] = {0, 0}; |
159 |
36491 |
while (count[0] < nc.getNumChildren() |
160 |
21214 |
|| count[1] < n.getNumChildren()) |
161 |
|
{ |
162 |
|
// explain empty prefixes |
163 |
45831 |
for (unsigned t = 0; t < 2; t++) |
164 |
|
{ |
165 |
61108 |
Node nn = t == 0 ? nc : n; |
166 |
47854 |
while (count[t] < nn.getNumChildren() |
167 |
126262 |
&& (nn[count[t]] == emps |
168 |
70354 |
|| d_state.areEqual(nn[count[t]], emps))) |
169 |
|
{ |
170 |
8650 |
if (nn[count[t]] != emps) |
171 |
|
{ |
172 |
8650 |
exp.push_back(nn[count[t]].eqNode(emps)); |
173 |
|
} |
174 |
8650 |
count[t]++; |
175 |
|
} |
176 |
|
} |
177 |
30554 |
Trace("strings-base-debug") |
178 |
15277 |
<< " counts = " << count[0] << ", " << count[1] |
179 |
15277 |
<< std::endl; |
180 |
|
// explain equal components |
181 |
15277 |
if (count[0] < nc.getNumChildren()) |
182 |
|
{ |
183 |
11250 |
Assert(count[1] < n.getNumChildren()); |
184 |
11250 |
if (nc[count[0]] != n[count[1]]) |
185 |
|
{ |
186 |
207 |
exp.push_back(nc[count[0]].eqNode(n[count[1]])); |
187 |
|
} |
188 |
11250 |
count[0]++; |
189 |
11250 |
count[1]++; |
190 |
|
} |
191 |
|
} |
192 |
|
// infer the equality |
193 |
5937 |
d_im.sendInference(exp, n.eqNode(nc), InferenceId::STRINGS_I_NORM); |
194 |
|
} |
195 |
|
else |
196 |
|
{ |
197 |
|
// We cannot mark one of the terms as reduced here (via |
198 |
|
// ExtTheory::markCongruent) since extended function terms |
199 |
|
// rely on reductions to other extended function terms. We |
200 |
|
// may have a pair of extended function terms f(a)=f(b) where |
201 |
|
// the reduction of argument a depends on the term b. |
202 |
|
// Thus, marking f(b) as reduced by virtue of the fact we |
203 |
|
// have f(a) is incorrect, since then we are effectively |
204 |
|
// assuming that the reduction of f(a) depends on itself. |
205 |
|
} |
206 |
|
// this node is congruent to another one, we can ignore it |
207 |
209884 |
Trace("strings-base-debug") |
208 |
104942 |
<< " congruent term : " << n << " (via " << nc << ")" |
209 |
104942 |
<< std::endl; |
210 |
104942 |
d_congruent.insert(n); |
211 |
104942 |
congruentCount[k].first++; |
212 |
|
} |
213 |
919594 |
else if (k == STRING_CONCAT && c.size() == 1) |
214 |
|
{ |
215 |
64366 |
Trace("strings-base-debug") |
216 |
32183 |
<< " congruent term by singular : " << n << " " << c[0] |
217 |
32183 |
<< std::endl; |
218 |
|
// singular case |
219 |
32183 |
if (!d_state.areEqual(c[0], n)) |
220 |
|
{ |
221 |
24706 |
Node ns; |
222 |
24706 |
std::vector<Node> exp; |
223 |
|
// explain empty components |
224 |
12353 |
bool foundNEmpty = false; |
225 |
39056 |
for (const Node& nnc : n) |
226 |
|
{ |
227 |
26703 |
if (d_state.areEqual(nnc, emps)) |
228 |
|
{ |
229 |
14350 |
if (nnc != emps) |
230 |
|
{ |
231 |
14350 |
exp.push_back(nnc.eqNode(emps)); |
232 |
|
} |
233 |
|
} |
234 |
|
else |
235 |
|
{ |
236 |
12353 |
Assert(!foundNEmpty); |
237 |
12353 |
ns = nnc; |
238 |
12353 |
foundNEmpty = true; |
239 |
|
} |
240 |
|
} |
241 |
12353 |
AlwaysAssert(foundNEmpty); |
242 |
|
// infer the equality |
243 |
12353 |
d_im.sendInference(exp, n.eqNode(ns), InferenceId::STRINGS_I_NORM_S); |
244 |
|
} |
245 |
32183 |
d_congruent.insert(n); |
246 |
32183 |
congruentCount[k].first++; |
247 |
|
} |
248 |
|
else |
249 |
|
{ |
250 |
887411 |
congruentCount[k].second++; |
251 |
|
} |
252 |
|
} |
253 |
|
else |
254 |
|
{ |
255 |
322037 |
congruentCount[k].first++; |
256 |
|
} |
257 |
|
} |
258 |
|
} |
259 |
2105879 |
else if (!n.isConst()) |
260 |
|
{ |
261 |
1829539 |
if (d_congruent.find(n) == d_congruent.end()) |
262 |
|
{ |
263 |
|
// We mark all but the oldest variable in the equivalence class as |
264 |
|
// congruent. |
265 |
974551 |
if (var.isNull()) |
266 |
|
{ |
267 |
638605 |
var = n; |
268 |
|
} |
269 |
335946 |
else if (var > n) |
270 |
|
{ |
271 |
354802 |
Trace("strings-base-debug") |
272 |
177401 |
<< " congruent variable : " << var << std::endl; |
273 |
177401 |
d_congruent.insert(var); |
274 |
177401 |
var = n; |
275 |
|
} |
276 |
|
else |
277 |
|
{ |
278 |
317090 |
Trace("strings-base-debug") |
279 |
158545 |
<< " congruent variable : " << n << std::endl; |
280 |
158545 |
d_congruent.insert(n); |
281 |
|
} |
282 |
|
} |
283 |
|
} |
284 |
10402039 |
++eqc_i; |
285 |
|
} |
286 |
|
} |
287 |
1809258 |
++eqcs_i; |
288 |
|
} |
289 |
37049 |
if (Trace.isOn("strings-base")) |
290 |
|
{ |
291 |
|
for (const std::pair<const Kind, std::pair<uint32_t, uint32_t>>& cc : |
292 |
|
congruentCount) |
293 |
|
{ |
294 |
|
Trace("strings-base") |
295 |
|
<< " Terms[" << cc.first << "] = " << cc.second.second << "/" |
296 |
|
<< (cc.second.first + cc.second.second) << std::endl; |
297 |
|
} |
298 |
|
} |
299 |
37049 |
Trace("strings-base") << "BaseSolver::checkInit finished" << std::endl; |
300 |
|
} |
301 |
|
|
302 |
31103 |
void BaseSolver::checkConstantEquivalenceClasses() |
303 |
|
{ |
304 |
|
// do fixed point |
305 |
31103 |
size_t prevSize = 0; |
306 |
62206 |
std::vector<Node> vecc; |
307 |
|
do |
308 |
|
{ |
309 |
31103 |
vecc.clear(); |
310 |
62206 |
Trace("strings-base-debug") |
311 |
31103 |
<< "Check constant equivalence classes..." << std::endl; |
312 |
31103 |
prevSize = d_eqcInfo.size(); |
313 |
80763 |
for (std::pair<const TypeNode, std::map<Kind, TermIndex>>& tindex : |
314 |
31103 |
d_termIndex) |
315 |
|
{ |
316 |
80763 |
checkConstantEquivalenceClasses( |
317 |
161526 |
&tindex.second[STRING_CONCAT], vecc, true); |
318 |
|
} |
319 |
31103 |
} while (!d_im.hasProcessed() && d_eqcInfo.size() > prevSize); |
320 |
|
|
321 |
31103 |
if (!d_im.hasProcessed()) |
322 |
|
{ |
323 |
|
// now, go back and set "most content" terms |
324 |
31103 |
vecc.clear(); |
325 |
80763 |
for (std::pair<const TypeNode, std::map<Kind, TermIndex>>& tindex : |
326 |
31103 |
d_termIndex) |
327 |
|
{ |
328 |
80763 |
checkConstantEquivalenceClasses( |
329 |
161526 |
&tindex.second[STRING_CONCAT], vecc, false); |
330 |
|
} |
331 |
|
} |
332 |
31103 |
} |
333 |
|
|
334 |
833699 |
void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti, |
335 |
|
std::vector<Node>& vecc, |
336 |
|
bool ensureConst, |
337 |
|
bool isConst) |
338 |
|
{ |
339 |
1667398 |
Node n = ti->d_data; |
340 |
833699 |
if (!n.isNull()) |
341 |
|
{ |
342 |
|
// construct the constant if applicable |
343 |
798644 |
Node c; |
344 |
399322 |
if (isConst) |
345 |
|
{ |
346 |
99082 |
c = utils::mkNConcat(vecc, n.getType()); |
347 |
|
} |
348 |
399322 |
if (!isConst || !d_state.areEqual(n, c)) |
349 |
|
{ |
350 |
300240 |
if (Trace.isOn("strings-debug")) |
351 |
|
{ |
352 |
|
Trace("strings-debug") |
353 |
|
<< "Constant eqc : " << c << " for " << n << std::endl; |
354 |
|
Trace("strings-debug") << " "; |
355 |
|
for (const Node& v : vecc) |
356 |
|
{ |
357 |
|
Trace("strings-debug") << v << " "; |
358 |
|
} |
359 |
|
Trace("strings-debug") << std::endl; |
360 |
|
} |
361 |
300240 |
size_t count = 0; |
362 |
300240 |
size_t countc = 0; |
363 |
600480 |
std::vector<Node> exp; |
364 |
|
// non-constant vector |
365 |
600480 |
std::vector<Node> vecnc; |
366 |
300240 |
size_t contentSize = 0; |
367 |
1709264 |
while (count < n.getNumChildren()) |
368 |
|
{ |
369 |
|
// Add explanations for the empty children |
370 |
1409024 |
Node emps; |
371 |
764036 |
while (count < n.getNumChildren() |
372 |
1468548 |
&& d_state.isEqualEmptyWord(n[count], emps)) |
373 |
|
{ |
374 |
29762 |
d_im.addToExplanation(n[count], emps, exp); |
375 |
29762 |
count++; |
376 |
|
} |
377 |
704512 |
if (count < n.getNumChildren()) |
378 |
|
{ |
379 |
689196 |
if (vecc[countc].isNull()) |
380 |
|
{ |
381 |
629848 |
Assert(!isConst); |
382 |
|
// no constant for this component, leave it as is |
383 |
629848 |
vecnc.push_back(n[count]); |
384 |
|
} |
385 |
|
else |
386 |
|
{ |
387 |
59348 |
if (!isConst) |
388 |
|
{ |
389 |
|
// use the constant |
390 |
59348 |
vecnc.push_back(vecc[countc]); |
391 |
59348 |
Assert(vecc[countc].isConst()); |
392 |
59348 |
contentSize += Word::getLength(vecc[countc]); |
393 |
|
} |
394 |
118696 |
Trace("strings-debug") << "...explain " << n[count] << " " |
395 |
59348 |
<< vecc[countc] << std::endl; |
396 |
59348 |
if (!d_state.areEqual(n[count], vecc[countc])) |
397 |
|
{ |
398 |
|
Node nrr = d_state.getRepresentative(n[count]); |
399 |
|
Assert(!d_eqcInfo[nrr].d_bestContent.isNull() |
400 |
|
&& d_eqcInfo[nrr].d_bestContent.isConst()); |
401 |
|
// must flatten to avoid nested AND in explanations |
402 |
|
utils::flattenOp(AND, d_eqcInfo[nrr].d_exp, exp); |
403 |
|
// now explain equality to base |
404 |
|
d_im.addToExplanation(n[count], d_eqcInfo[nrr].d_base, exp); |
405 |
|
} |
406 |
|
else |
407 |
|
{ |
408 |
59348 |
d_im.addToExplanation(n[count], vecc[countc], exp); |
409 |
|
} |
410 |
59348 |
countc++; |
411 |
|
} |
412 |
689196 |
count++; |
413 |
|
} |
414 |
|
} |
415 |
|
// exp contains an explanation of n==c |
416 |
300240 |
Assert(!isConst || countc == vecc.size()); |
417 |
300240 |
if (!isConst) |
418 |
|
{ |
419 |
|
// no use storing something with no content |
420 |
300240 |
if (contentSize > 0) |
421 |
|
{ |
422 |
106860 |
Node nr = d_state.getRepresentative(n); |
423 |
53430 |
BaseEqcInfo& bei = d_eqcInfo[nr]; |
424 |
106860 |
if (!bei.d_bestContent.isConst() |
425 |
53430 |
&& (bei.d_bestContent.isNull() || contentSize > bei.d_bestScore)) |
426 |
|
{ |
427 |
|
// The equivalence class is not entailed to be equal to a constant |
428 |
|
// and we found a better concatenation |
429 |
92072 |
Node nct = utils::mkNConcat(vecnc, n.getType()); |
430 |
46036 |
Assert(!nct.isConst()); |
431 |
46036 |
bei.d_bestContent = nct; |
432 |
46036 |
bei.d_bestScore = contentSize; |
433 |
46036 |
bei.d_base = n; |
434 |
46036 |
if (!exp.empty()) |
435 |
|
{ |
436 |
17265 |
bei.d_exp = utils::mkAnd(exp); |
437 |
|
} |
438 |
92072 |
Trace("strings-debug") |
439 |
46036 |
<< "Set eqc best content " << n << " to " << nct |
440 |
46036 |
<< ", explanation = " << bei.d_exp << std::endl; |
441 |
|
} |
442 |
|
} |
443 |
|
} |
444 |
|
else if (d_state.hasTerm(c)) |
445 |
|
{ |
446 |
|
d_im.sendInference(exp, n.eqNode(c), InferenceId::STRINGS_I_CONST_MERGE); |
447 |
|
return; |
448 |
|
} |
449 |
|
else if (!d_im.hasProcessed()) |
450 |
|
{ |
451 |
|
Node nr = d_state.getRepresentative(n); |
452 |
|
BaseEqcInfo& bei = d_eqcInfo[nr]; |
453 |
|
if (!bei.d_bestContent.isConst()) |
454 |
|
{ |
455 |
|
bei.d_bestContent = c; |
456 |
|
bei.d_base = n; |
457 |
|
bei.d_exp = utils::mkAnd(exp); |
458 |
|
Trace("strings-debug") |
459 |
|
<< "Set eqc const " << n << " to " << c |
460 |
|
<< ", explanation = " << bei.d_exp << std::endl; |
461 |
|
} |
462 |
|
else if (c != bei.d_bestContent) |
463 |
|
{ |
464 |
|
// conflict |
465 |
|
Trace("strings-debug") |
466 |
|
<< "Conflict, other constant was " << bei.d_bestContent |
467 |
|
<< ", this constant was " << c << std::endl; |
468 |
|
if (bei.d_exp.isNull()) |
469 |
|
{ |
470 |
|
// n==c ^ n == c' => false |
471 |
|
d_im.addToExplanation(n, bei.d_bestContent, exp); |
472 |
|
} |
473 |
|
else |
474 |
|
{ |
475 |
|
// n==c ^ n == d_base == c' => false |
476 |
|
exp.push_back(bei.d_exp); |
477 |
|
d_im.addToExplanation(n, bei.d_base, exp); |
478 |
|
} |
479 |
|
d_im.sendInference(exp, d_false, InferenceId::STRINGS_I_CONST_CONFLICT); |
480 |
|
return; |
481 |
|
} |
482 |
|
else |
483 |
|
{ |
484 |
|
Trace("strings-debug") << "Duplicate constant." << std::endl; |
485 |
|
} |
486 |
|
} |
487 |
|
} |
488 |
|
} |
489 |
1692398 |
for (std::pair<const TNode, TermIndex>& p : ti->d_children) |
490 |
|
{ |
491 |
858699 |
std::map<Node, BaseEqcInfo>::const_iterator it = d_eqcInfo.find(p.first); |
492 |
858699 |
if (it != d_eqcInfo.end() && it->second.d_bestContent.isConst()) |
493 |
|
{ |
494 |
279137 |
vecc.push_back(it->second.d_bestContent); |
495 |
279137 |
checkConstantEquivalenceClasses(&p.second, vecc, ensureConst, isConst); |
496 |
279137 |
vecc.pop_back(); |
497 |
|
} |
498 |
579562 |
else if (!ensureConst) |
499 |
|
{ |
500 |
|
// can still proceed, with null |
501 |
393036 |
vecc.push_back(Node::null()); |
502 |
393036 |
checkConstantEquivalenceClasses(&p.second, vecc, ensureConst, false); |
503 |
393036 |
vecc.pop_back(); |
504 |
|
} |
505 |
858699 |
if (d_im.hasProcessed()) |
506 |
|
{ |
507 |
|
break; |
508 |
|
} |
509 |
|
} |
510 |
|
} |
511 |
|
|
512 |
7959 |
void BaseSolver::checkCardinality() |
513 |
|
{ |
514 |
|
// This will create a partition of eqc, where each collection has length that |
515 |
|
// are pairwise propagated to be equal. We do not require disequalities |
516 |
|
// between the lengths of each collection, since we split on disequalities |
517 |
|
// between lengths of string terms that are disequal (DEQ-LENGTH-SP). |
518 |
15918 |
std::map<TypeNode, std::vector<std::vector<Node> > > cols; |
519 |
15918 |
std::map<TypeNode, std::vector<Node> > lts; |
520 |
7959 |
d_state.separateByLength(d_stringsEqc, cols, lts); |
521 |
9428 |
for (std::pair<const TypeNode, std::vector<std::vector<Node> > >& c : cols) |
522 |
|
{ |
523 |
1469 |
checkCardinalityType(c.first, c.second, lts[c.first]); |
524 |
|
} |
525 |
7959 |
} |
526 |
|
|
527 |
1469 |
void BaseSolver::checkCardinalityType(TypeNode tn, |
528 |
|
std::vector<std::vector<Node> >& cols, |
529 |
|
std::vector<Node>& lts) |
530 |
|
{ |
531 |
2938 |
Trace("strings-card") << "Check cardinality (type " << tn << ")..." |
532 |
1469 |
<< std::endl; |
533 |
1469 |
NodeManager* nm = NodeManager::currentNM(); |
534 |
|
uint32_t typeCardSize; |
535 |
1469 |
if (tn.isString()) // string-only |
536 |
|
{ |
537 |
1375 |
typeCardSize = d_cardSize; |
538 |
|
} |
539 |
|
else |
540 |
|
{ |
541 |
94 |
Assert(tn.isSequence()); |
542 |
188 |
TypeNode etn = tn.getSequenceElementType(); |
543 |
94 |
if (!d_state.isFiniteType(etn)) |
544 |
|
{ |
545 |
|
// infinite cardinality, we are fine |
546 |
88 |
return; |
547 |
|
} |
548 |
|
// TODO (cvc4-projects #23): how to handle sequence for finite types? |
549 |
6 |
return; |
550 |
|
} |
551 |
|
// for each collection |
552 |
9195 |
for (unsigned i = 0, csize = cols.size(); i < csize; ++i) |
553 |
|
{ |
554 |
7820 |
Node lr = lts[i]; |
555 |
15640 |
Trace("strings-card") << "Number of strings with length equal to " << lr |
556 |
7820 |
<< " is " << cols[i].size() << std::endl; |
557 |
7820 |
if (cols[i].size() <= 1) |
558 |
|
{ |
559 |
|
// no restriction on sets in the partition of size 1 |
560 |
6165 |
continue; |
561 |
|
} |
562 |
|
// size > c^k |
563 |
1655 |
unsigned card_need = 1; |
564 |
1655 |
double curr = static_cast<double>(cols[i].size()); |
565 |
1655 |
while (curr > typeCardSize) |
566 |
|
{ |
567 |
|
curr = curr / static_cast<double>(typeCardSize); |
568 |
|
card_need++; |
569 |
|
} |
570 |
3310 |
Trace("strings-card") |
571 |
1655 |
<< "Need length " << card_need |
572 |
1655 |
<< " for this number of strings (where alphabet size is " |
573 |
1655 |
<< typeCardSize << ") given type " << tn << "." << std::endl; |
574 |
|
// check if we need to split |
575 |
1655 |
bool needsSplit = true; |
576 |
1655 |
if (lr.isConst()) |
577 |
|
{ |
578 |
|
// if constant, compare |
579 |
3188 |
Node cmp = nm->mkNode(GEQ, lr, nm->mkConst(Rational(card_need))); |
580 |
1594 |
cmp = Rewriter::rewrite(cmp); |
581 |
1594 |
needsSplit = !cmp.getConst<bool>(); |
582 |
|
} |
583 |
|
else |
584 |
|
{ |
585 |
|
// find the minimimum constant that we are unknown to be disequal from, or |
586 |
|
// otherwise stop if we increment such that cardinality does not apply. |
587 |
|
// We always start with r=1 since by the invariants of our term registry, |
588 |
|
// a term is either equal to the empty string, or has length >= 1. |
589 |
61 |
unsigned r = 1; |
590 |
61 |
bool success = true; |
591 |
61 |
while (r < card_need && success) |
592 |
|
{ |
593 |
|
Node rr = nm->mkConst(Rational(r)); |
594 |
|
if (d_state.areDisequal(rr, lr)) |
595 |
|
{ |
596 |
|
r++; |
597 |
|
} |
598 |
|
else |
599 |
|
{ |
600 |
|
success = false; |
601 |
|
} |
602 |
|
} |
603 |
61 |
if (r > 0) |
604 |
|
{ |
605 |
122 |
Trace("strings-card") |
606 |
61 |
<< "Symbolic length " << lr << " must be at least " << r |
607 |
61 |
<< " due to constant disequalities." << std::endl; |
608 |
|
} |
609 |
61 |
needsSplit = r < card_need; |
610 |
|
} |
611 |
|
|
612 |
1655 |
if (!needsSplit) |
613 |
|
{ |
614 |
|
// don't need to split |
615 |
1655 |
continue; |
616 |
|
} |
617 |
|
// first, try to split to merge equivalence classes |
618 |
|
for (std::vector<Node>::iterator itr1 = cols[i].begin(); |
619 |
|
itr1 != cols[i].end(); |
620 |
|
++itr1) |
621 |
|
{ |
622 |
|
for (std::vector<Node>::iterator itr2 = itr1 + 1; itr2 != cols[i].end(); |
623 |
|
++itr2) |
624 |
|
{ |
625 |
|
if (!d_state.areDisequal(*itr1, *itr2)) |
626 |
|
{ |
627 |
|
// add split lemma |
628 |
|
if (d_im.sendSplit(*itr1, *itr2, InferenceId::STRINGS_CARD_SP)) |
629 |
|
{ |
630 |
|
return; |
631 |
|
} |
632 |
|
} |
633 |
|
} |
634 |
|
} |
635 |
|
// otherwise, we need a length constraint |
636 |
|
uint32_t int_k = static_cast<uint32_t>(card_need); |
637 |
|
EqcInfo* ei = d_state.getOrMakeEqcInfo(lr, true); |
638 |
|
Trace("strings-card") << "Previous cardinality used for " << lr << " is " |
639 |
|
<< ((int)ei->d_cardinalityLemK.get() - 1) |
640 |
|
<< std::endl; |
641 |
|
if (int_k + 1 > ei->d_cardinalityLemK.get()) |
642 |
|
{ |
643 |
|
Node k_node = nm->mkConst(Rational(int_k)); |
644 |
|
// add cardinality lemma |
645 |
|
Node dist = nm->mkNode(DISTINCT, cols[i]); |
646 |
|
std::vector<Node> expn; |
647 |
|
expn.push_back(dist); |
648 |
|
for (std::vector<Node>::iterator itr1 = cols[i].begin(); |
649 |
|
itr1 != cols[i].end(); |
650 |
|
++itr1) |
651 |
|
{ |
652 |
|
Node len = nm->mkNode(STRING_LENGTH, *itr1); |
653 |
|
if (len != lr) |
654 |
|
{ |
655 |
|
Node len_eq_lr = len.eqNode(lr); |
656 |
|
expn.push_back(len_eq_lr); |
657 |
|
} |
658 |
|
} |
659 |
|
Node len = nm->mkNode(STRING_LENGTH, cols[i][0]); |
660 |
|
Node cons = nm->mkNode(GEQ, len, k_node); |
661 |
|
cons = Rewriter::rewrite(cons); |
662 |
|
ei->d_cardinalityLemK.set(int_k + 1); |
663 |
|
if (!cons.isConst() || !cons.getConst<bool>()) |
664 |
|
{ |
665 |
|
d_im.sendInference( |
666 |
|
expn, expn, cons, InferenceId::STRINGS_CARDINALITY, false, true); |
667 |
|
return; |
668 |
|
} |
669 |
|
} |
670 |
|
} |
671 |
1375 |
Trace("strings-card") << "...end check cardinality" << std::endl; |
672 |
|
} |
673 |
|
|
674 |
3148238 |
bool BaseSolver::isCongruent(Node n) |
675 |
|
{ |
676 |
3148238 |
return d_congruent.find(n) != d_congruent.end(); |
677 |
|
} |
678 |
|
|
679 |
1471107 |
Node BaseSolver::getConstantEqc(Node eqc) |
680 |
|
{ |
681 |
1471107 |
std::map<Node, BaseEqcInfo>::const_iterator it = d_eqcInfo.find(eqc); |
682 |
1471107 |
if (it != d_eqcInfo.end() && it->second.d_bestContent.isConst()) |
683 |
|
{ |
684 |
525372 |
return it->second.d_bestContent; |
685 |
|
} |
686 |
945735 |
return Node::null(); |
687 |
|
} |
688 |
|
|
689 |
55792 |
Node BaseSolver::explainConstantEqc(Node n, Node eqc, std::vector<Node>& exp) |
690 |
|
{ |
691 |
55792 |
std::map<Node, BaseEqcInfo>::const_iterator it = d_eqcInfo.find(eqc); |
692 |
55792 |
if (it != d_eqcInfo.end()) |
693 |
|
{ |
694 |
55792 |
BaseEqcInfo& bei = d_eqcInfo[eqc]; |
695 |
55792 |
if (!bei.d_bestContent.isConst()) |
696 |
|
{ |
697 |
|
return Node::null(); |
698 |
|
} |
699 |
55792 |
if (!bei.d_exp.isNull()) |
700 |
|
{ |
701 |
|
utils::flattenOp(AND, bei.d_exp, exp); |
702 |
|
} |
703 |
55792 |
if (!bei.d_base.isNull()) |
704 |
|
{ |
705 |
55792 |
d_im.addToExplanation(n, bei.d_base, exp); |
706 |
|
} |
707 |
55792 |
return bei.d_bestContent; |
708 |
|
} |
709 |
|
return Node::null(); |
710 |
|
} |
711 |
|
|
712 |
904602 |
Node BaseSolver::explainBestContentEqc(Node n, Node eqc, std::vector<Node>& exp) |
713 |
|
{ |
714 |
904602 |
std::map<Node, BaseEqcInfo>::const_iterator it = d_eqcInfo.find(eqc); |
715 |
904602 |
if (it != d_eqcInfo.end()) |
716 |
|
{ |
717 |
475957 |
BaseEqcInfo& bei = d_eqcInfo[eqc]; |
718 |
475957 |
Assert(!bei.d_bestContent.isNull()); |
719 |
475957 |
if (!bei.d_exp.isNull()) |
720 |
|
{ |
721 |
42513 |
utils::flattenOp(AND, bei.d_exp, exp); |
722 |
|
} |
723 |
475957 |
if (!bei.d_base.isNull()) |
724 |
|
{ |
725 |
475957 |
d_im.addToExplanation(n, bei.d_base, exp); |
726 |
|
} |
727 |
475957 |
return bei.d_bestContent; |
728 |
|
} |
729 |
|
|
730 |
428645 |
return Node::null(); |
731 |
|
} |
732 |
|
|
733 |
30285 |
const std::vector<Node>& BaseSolver::getStringEqc() const |
734 |
|
{ |
735 |
30285 |
return d_stringsEqc; |
736 |
|
} |
737 |
|
|
738 |
3449180 |
Node BaseSolver::TermIndex::add(TNode n, |
739 |
|
unsigned index, |
740 |
|
const SolverState& s, |
741 |
|
Node er, |
742 |
|
std::vector<Node>& c) |
743 |
|
{ |
744 |
3449180 |
if (index == n.getNumChildren()) |
745 |
|
{ |
746 |
1024536 |
if (d_data.isNull()) |
747 |
|
{ |
748 |
919594 |
d_data = n; |
749 |
|
} |
750 |
1024536 |
return d_data; |
751 |
|
} |
752 |
2424644 |
Assert(index < n.getNumChildren()); |
753 |
4849288 |
TNode nir = s.getRepresentative(n[index]); |
754 |
|
// if it is empty, and doing CONCAT, ignore |
755 |
2424644 |
if (nir == er && n.getKind() == STRING_CONCAT) |
756 |
|
{ |
757 |
226383 |
return add(n, index + 1, s, er, c); |
758 |
|
} |
759 |
2198261 |
c.push_back(nir); |
760 |
2198261 |
return d_children[nir].add(n, index + 1, s, er, c); |
761 |
|
} |
762 |
|
|
763 |
|
} // namespace strings |
764 |
|
} // namespace theory |
765 |
29340 |
} // namespace cvc5 |