1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Gereon Kremer, Andres Noetzli |
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 solver for extended functions of theory of strings. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/strings/extf_solver.h" |
17 |
|
|
18 |
|
#include "options/strings_options.h" |
19 |
|
#include "theory/strings/sequences_rewriter.h" |
20 |
|
#include "theory/strings/theory_strings_preprocess.h" |
21 |
|
#include "theory/strings/theory_strings_utils.h" |
22 |
|
#include "util/statistics_registry.h" |
23 |
|
|
24 |
|
using namespace std; |
25 |
|
using namespace cvc5::context; |
26 |
|
using namespace cvc5::kind; |
27 |
|
|
28 |
|
namespace cvc5 { |
29 |
|
namespace theory { |
30 |
|
namespace strings { |
31 |
|
|
32 |
8954 |
ExtfSolver::ExtfSolver(SolverState& s, |
33 |
|
InferenceManager& im, |
34 |
|
TermRegistry& tr, |
35 |
|
StringsRewriter& rewriter, |
36 |
|
BaseSolver& bs, |
37 |
|
CoreSolver& cs, |
38 |
|
ExtTheory& et, |
39 |
8954 |
SequencesStatistics& statistics) |
40 |
|
: d_state(s), |
41 |
|
d_im(im), |
42 |
|
d_termReg(tr), |
43 |
|
d_rewriter(rewriter), |
44 |
|
d_bsolver(bs), |
45 |
|
d_csolver(cs), |
46 |
|
d_extt(et), |
47 |
|
d_statistics(statistics), |
48 |
8954 |
d_preproc(d_termReg.getSkolemCache(), &statistics.d_reductions), |
49 |
|
d_hasExtf(s.getSatContext(), false), |
50 |
|
d_extfInferCache(s.getSatContext()), |
51 |
17908 |
d_reduced(s.getUserContext()) |
52 |
|
{ |
53 |
8954 |
d_extt.addFunctionKind(kind::STRING_SUBSTR); |
54 |
8954 |
d_extt.addFunctionKind(kind::STRING_UPDATE); |
55 |
8954 |
d_extt.addFunctionKind(kind::STRING_STRIDOF); |
56 |
8954 |
d_extt.addFunctionKind(kind::STRING_ITOS); |
57 |
8954 |
d_extt.addFunctionKind(kind::STRING_STOI); |
58 |
8954 |
d_extt.addFunctionKind(kind::STRING_STRREPL); |
59 |
8954 |
d_extt.addFunctionKind(kind::STRING_STRREPLALL); |
60 |
8954 |
d_extt.addFunctionKind(kind::STRING_REPLACE_RE); |
61 |
8954 |
d_extt.addFunctionKind(kind::STRING_REPLACE_RE_ALL); |
62 |
8954 |
d_extt.addFunctionKind(kind::STRING_STRCTN); |
63 |
8954 |
d_extt.addFunctionKind(kind::STRING_IN_REGEXP); |
64 |
8954 |
d_extt.addFunctionKind(kind::STRING_LEQ); |
65 |
8954 |
d_extt.addFunctionKind(kind::STRING_TO_CODE); |
66 |
8954 |
d_extt.addFunctionKind(kind::STRING_TOLOWER); |
67 |
8954 |
d_extt.addFunctionKind(kind::STRING_TOUPPER); |
68 |
8954 |
d_extt.addFunctionKind(kind::STRING_REV); |
69 |
8954 |
d_extt.addFunctionKind(kind::SEQ_UNIT); |
70 |
8954 |
d_extt.addFunctionKind(kind::SEQ_NTH); |
71 |
|
|
72 |
8954 |
d_true = NodeManager::currentNM()->mkConst(true); |
73 |
8954 |
d_false = NodeManager::currentNM()->mkConst(false); |
74 |
8954 |
} |
75 |
|
|
76 |
8954 |
ExtfSolver::~ExtfSolver() {} |
77 |
|
|
78 |
102049 |
bool ExtfSolver::doReduction(int effort, Node n) |
79 |
|
{ |
80 |
102049 |
Assert(d_extfInfoTmp.find(n) != d_extfInfoTmp.end()); |
81 |
102049 |
if (!d_extfInfoTmp[n].d_modelActive) |
82 |
|
{ |
83 |
|
// n is not active in the model, no need to reduce |
84 |
|
Trace("strings-extf-debug") << "...skip due to model active" << std::endl; |
85 |
|
return false; |
86 |
|
} |
87 |
102049 |
if (d_reduced.find(n)!=d_reduced.end()) |
88 |
|
{ |
89 |
|
// already sent a reduction lemma |
90 |
67276 |
Trace("strings-extf-debug") << "...skip due to reduced" << std::endl; |
91 |
67276 |
return false; |
92 |
|
} |
93 |
|
// determine the effort level to process the extf at |
94 |
|
// 0 - at assertion time, 1+ - after no other reduction is applicable |
95 |
34773 |
int r_effort = -1; |
96 |
|
// polarity : 1 true, -1 false, 0 neither |
97 |
34773 |
int pol = 0; |
98 |
34773 |
Kind k = n.getKind(); |
99 |
34773 |
if (n.getType().isBoolean() && !d_extfInfoTmp[n].d_const.isNull()) |
100 |
|
{ |
101 |
13146 |
pol = d_extfInfoTmp[n].d_const.getConst<bool>() ? 1 : -1; |
102 |
|
} |
103 |
34773 |
if (k == STRING_STRCTN) |
104 |
|
{ |
105 |
6227 |
if (pol == 1) |
106 |
|
{ |
107 |
1797 |
r_effort = 1; |
108 |
|
} |
109 |
4430 |
else if (pol == -1) |
110 |
|
{ |
111 |
4044 |
if (effort == 2) |
112 |
|
{ |
113 |
192 |
Node x = n[0]; |
114 |
192 |
Node s = n[1]; |
115 |
192 |
std::vector<Node> lexp; |
116 |
192 |
Node lenx = d_state.getLength(x, lexp); |
117 |
192 |
Node lens = d_state.getLength(s, lexp); |
118 |
101 |
if (d_state.areEqual(lenx, lens)) |
119 |
|
{ |
120 |
20 |
Trace("strings-extf-debug") |
121 |
10 |
<< " resolve extf : " << n |
122 |
10 |
<< " based on equal lengths disequality." << std::endl; |
123 |
|
// We can reduce negative contains to a disequality when lengths are |
124 |
|
// equal. In other words, len( x ) = len( s ) implies |
125 |
|
// ~contains( x, s ) reduces to x != s. |
126 |
10 |
if (!d_state.areDisequal(x, s)) |
127 |
|
{ |
128 |
|
// len( x ) = len( s ) ^ ~contains( x, s ) => x != s |
129 |
6 |
lexp.push_back(lenx.eqNode(lens)); |
130 |
6 |
lexp.push_back(n.negate()); |
131 |
12 |
Node xneqs = x.eqNode(s).negate(); |
132 |
6 |
d_im.sendInference( |
133 |
|
lexp, xneqs, InferenceId::STRINGS_CTN_NEG_EQUAL, false, true); |
134 |
|
} |
135 |
|
// this depends on the current assertions, so this |
136 |
|
// inference is context-dependent |
137 |
10 |
d_extt.markReduced(n, ExtReducedId::STRINGS_NEG_CTN_DEQ, true); |
138 |
10 |
return true; |
139 |
|
} |
140 |
|
else |
141 |
|
{ |
142 |
91 |
r_effort = 2; |
143 |
|
} |
144 |
|
} |
145 |
|
} |
146 |
|
} |
147 |
28546 |
else if (k == STRING_SUBSTR) |
148 |
|
{ |
149 |
905 |
r_effort = 1; |
150 |
|
} |
151 |
27641 |
else if (k == SEQ_UNIT) |
152 |
|
{ |
153 |
|
// never necessary to reduce seq.unit |
154 |
138 |
return false; |
155 |
|
} |
156 |
27503 |
else if (k != STRING_IN_REGEXP) |
157 |
|
{ |
158 |
20094 |
r_effort = 2; |
159 |
|
} |
160 |
34625 |
if (effort != r_effort) |
161 |
|
{ |
162 |
30886 |
Trace("strings-extf-debug") << "...skip due to effort" << std::endl; |
163 |
|
// not the right effort level to reduce |
164 |
30886 |
return false; |
165 |
|
} |
166 |
7478 |
Node c_n = pol == -1 ? n.negate() : n; |
167 |
7478 |
Trace("strings-process-debug") |
168 |
3739 |
<< "Process reduction for " << n << ", pol = " << pol << std::endl; |
169 |
3739 |
if (k == STRING_STRCTN && pol == 1) |
170 |
|
{ |
171 |
3594 |
Node x = n[0]; |
172 |
3594 |
Node s = n[1]; |
173 |
|
// positive contains reduces to a equality |
174 |
1797 |
SkolemCache* skc = d_termReg.getSkolemCache(); |
175 |
3594 |
Node eq = d_termReg.eagerReduce(n, skc); |
176 |
1797 |
Assert(!eq.isNull()); |
177 |
1797 |
Assert(eq.getKind() == ITE && eq[0] == n); |
178 |
1797 |
eq = eq[1]; |
179 |
3594 |
std::vector<Node> expn; |
180 |
1797 |
expn.push_back(n); |
181 |
1797 |
d_im.sendInference(expn, expn, eq, InferenceId::STRINGS_CTN_POS, false, true); |
182 |
3594 |
Trace("strings-extf-debug") |
183 |
1797 |
<< " resolve extf : " << n << " based on positive contain reduction." |
184 |
1797 |
<< std::endl; |
185 |
3594 |
Trace("strings-red-lemma") << "Reduction (positive contains) lemma : " << n |
186 |
1797 |
<< " => " << eq << std::endl; |
187 |
|
// context-dependent because it depends on the polarity of n itself |
188 |
3594 |
d_extt.markReduced(n, ExtReducedId::STRINGS_POS_CTN, true); |
189 |
|
} |
190 |
1942 |
else if (k != kind::STRING_TO_CODE) |
191 |
|
{ |
192 |
1392 |
NodeManager* nm = NodeManager::currentNM(); |
193 |
1392 |
Assert(k == STRING_SUBSTR || k == STRING_UPDATE || k == STRING_STRCTN |
194 |
|
|| k == STRING_STRIDOF || k == STRING_ITOS || k == STRING_STOI |
195 |
|
|| k == STRING_STRREPL || k == STRING_STRREPLALL || k == SEQ_NTH |
196 |
|
|| k == STRING_REPLACE_RE || k == STRING_REPLACE_RE_ALL |
197 |
|
|| k == STRING_LEQ || k == STRING_TOLOWER || k == STRING_TOUPPER |
198 |
|
|| k == STRING_REV); |
199 |
2784 |
std::vector<Node> new_nodes; |
200 |
2784 |
Node res = d_preproc.simplify(n, new_nodes); |
201 |
1392 |
Assert(res != n); |
202 |
1392 |
new_nodes.push_back(n.eqNode(res)); |
203 |
|
Node nnlem = |
204 |
2784 |
new_nodes.size() == 1 ? new_nodes[0] : nm->mkNode(AND, new_nodes); |
205 |
2784 |
Trace("strings-red-lemma") |
206 |
1392 |
<< "Reduction_" << effort << " lemma : " << nnlem << std::endl; |
207 |
1392 |
Trace("strings-red-lemma") << "...from " << n << std::endl; |
208 |
2784 |
Trace("strings-red-lemma") |
209 |
1392 |
<< "Reduction_" << effort << " rewritten : " << Rewriter::rewrite(nnlem) << std::endl; |
210 |
1392 |
d_im.sendInference(d_emptyVec, nnlem, InferenceId::STRINGS_REDUCTION, false, true); |
211 |
2784 |
Trace("strings-extf-debug") |
212 |
1392 |
<< " resolve extf : " << n << " based on reduction." << std::endl; |
213 |
|
// add as reduction lemma |
214 |
1392 |
d_reduced.insert(n); |
215 |
|
} |
216 |
3739 |
return true; |
217 |
|
} |
218 |
|
|
219 |
19714 |
void ExtfSolver::checkExtfReductions(int effort) |
220 |
|
{ |
221 |
|
// Notice we don't make a standard call to ExtTheory::doReductions here, |
222 |
|
// since certain optimizations like context-dependent reductions and |
223 |
|
// stratifying effort levels are done in doReduction below. |
224 |
36233 |
std::vector<Node> extf = d_extt.getActive(); |
225 |
39428 |
Trace("strings-process") << " checking " << extf.size() << " active extf" |
226 |
19714 |
<< std::endl; |
227 |
118568 |
for (const Node& n : extf) |
228 |
|
{ |
229 |
102049 |
Assert(!d_state.isInConflict()); |
230 |
204098 |
Trace("strings-process") |
231 |
102049 |
<< " check " << n |
232 |
102049 |
<< ", active in model=" << d_extfInfoTmp[n].d_modelActive << std::endl; |
233 |
102049 |
bool ret = doReduction(effort, n); |
234 |
102049 |
if (ret) |
235 |
|
{ |
236 |
|
// we do not mark as reduced, since we may want to evaluate |
237 |
3749 |
if (d_im.hasProcessed()) |
238 |
|
{ |
239 |
6390 |
return; |
240 |
|
} |
241 |
|
} |
242 |
|
} |
243 |
|
} |
244 |
|
|
245 |
30751 |
void ExtfSolver::checkExtfEval(int effort) |
246 |
|
{ |
247 |
61502 |
Trace("strings-extf-list") |
248 |
30751 |
<< "Active extended functions, effort=" << effort << " : " << std::endl; |
249 |
30751 |
d_extfInfoTmp.clear(); |
250 |
30751 |
NodeManager* nm = NodeManager::currentNM(); |
251 |
30751 |
bool has_nreduce = false; |
252 |
61291 |
std::vector<Node> terms = d_extt.getActive(); |
253 |
|
// the set of terms we have done extf inferences for |
254 |
61291 |
std::unordered_set<Node> inferProcessed; |
255 |
255461 |
for (const Node& n : terms) |
256 |
|
{ |
257 |
|
// Setup information about n, including if it is equal to a constant. |
258 |
224921 |
ExtfInfoTmp& einfo = d_extfInfoTmp[n]; |
259 |
449631 |
Node r = d_state.getRepresentative(n); |
260 |
224921 |
einfo.d_const = d_bsolver.getConstantEqc(r); |
261 |
|
// Get the current values of the children of n. |
262 |
|
// Notice that we look up the value of the direct children of n, and not |
263 |
|
// their free variables. In other words, given a term: |
264 |
|
// t = (str.replace "B" (str.replace x "A" "B") "C") |
265 |
|
// we may build the explanation that: |
266 |
|
// ((str.replace x "A" "B") = "B") => t = (str.replace "B" "B" "C") |
267 |
|
// instead of basing this on the free variable x: |
268 |
|
// (x = "A") => t = (str.replace "B" (str.replace "A" "A" "B") "C") |
269 |
|
// Although both allow us to infer t = "C", it is important to use the |
270 |
|
// first kind of inference since it ensures that its subterms have the |
271 |
|
// expected values. Otherwise, we may in rare cases fail to realize that |
272 |
|
// the subterm (str.replace x "A" "B") does not currently have the correct |
273 |
|
// value, say in this example that (str.replace x "A" "B") != "B". |
274 |
449631 |
std::vector<Node> exp; |
275 |
449631 |
std::vector<Node> schildren; |
276 |
224921 |
bool schanged = false; |
277 |
738235 |
for (const Node& nc : n) |
278 |
|
{ |
279 |
1026628 |
Node sc = getCurrentSubstitutionFor(effort, nc, exp); |
280 |
513314 |
schildren.push_back(sc); |
281 |
513314 |
schanged = schanged || sc != nc; |
282 |
|
} |
283 |
|
// If there is information involving the children, attempt to do an |
284 |
|
// inference and/or mark n as reduced. |
285 |
224921 |
bool reduced = false; |
286 |
449631 |
Node to_reduce = n; |
287 |
224921 |
if (schanged) |
288 |
|
{ |
289 |
216574 |
Node sn = nm->mkNode(n.getKind(), schildren); |
290 |
216574 |
Trace("strings-extf-debug") |
291 |
108287 |
<< "Check extf " << n << " == " << sn |
292 |
108287 |
<< ", constant = " << einfo.d_const << ", effort=" << effort << "..." |
293 |
108287 |
<< std::endl; |
294 |
108287 |
einfo.d_exp.insert(einfo.d_exp.end(), exp.begin(), exp.end()); |
295 |
|
// inference is rewriting the substituted node |
296 |
216574 |
Node nrc = Rewriter::rewrite(sn); |
297 |
|
// if rewrites to a constant, then do the inference and mark as reduced |
298 |
108287 |
if (nrc.isConst()) |
299 |
|
{ |
300 |
62862 |
if (effort < 3) |
301 |
|
{ |
302 |
62862 |
d_extt.markReduced(n, ExtReducedId::STRINGS_SR_CONST); |
303 |
125724 |
Trace("strings-extf-debug") |
304 |
62862 |
<< " resolvable by evaluation..." << std::endl; |
305 |
125724 |
std::vector<Node> exps; |
306 |
|
// The following optimization gets the "symbolic definition" of |
307 |
|
// an extended term. The symbolic definition of a term t is a term |
308 |
|
// t' where constants are replaced by their corresponding proxy |
309 |
|
// variables. |
310 |
|
// For example, if lsym is a proxy variable for "", then |
311 |
|
// str.replace( lsym, lsym, lsym ) is the symbolic definition for |
312 |
|
// str.replace( "", "", "" ). It is generally better to use symbolic |
313 |
|
// definitions when doing cd-rewriting for the purpose of minimizing |
314 |
|
// clauses, e.g. we infer the unit equality: |
315 |
|
// str.replace( lsym, lsym, lsym ) == "" |
316 |
|
// instead of making this inference multiple times: |
317 |
|
// x = "" => str.replace( x, x, x ) == "" |
318 |
|
// y = "" => str.replace( y, y, y ) == "" |
319 |
125724 |
Trace("strings-extf-debug") |
320 |
62862 |
<< " get symbolic definition..." << std::endl; |
321 |
125724 |
Node nrs; |
322 |
|
// only use symbolic definitions if option is set |
323 |
138194 |
if (options::stringInferSym()) |
324 |
|
{ |
325 |
62862 |
nrs = d_termReg.getSymbolicDefinition(sn, exps); |
326 |
|
} |
327 |
62862 |
if (!nrs.isNull()) |
328 |
|
{ |
329 |
104244 |
Trace("strings-extf-debug") |
330 |
52122 |
<< " rewrite " << nrs << "..." << std::endl; |
331 |
104244 |
Node nrsr = Rewriter::rewrite(nrs); |
332 |
|
// ensure the symbolic form is not rewritable |
333 |
52122 |
if (nrsr != nrs) |
334 |
|
{ |
335 |
|
// we cannot use the symbolic definition if it rewrites |
336 |
2818 |
Trace("strings-extf-debug") |
337 |
1409 |
<< " symbolic definition is trivial..." << std::endl; |
338 |
1409 |
nrs = Node::null(); |
339 |
|
} |
340 |
|
} |
341 |
|
else |
342 |
|
{ |
343 |
21480 |
Trace("strings-extf-debug") |
344 |
10740 |
<< " could not infer symbolic definition." << std::endl; |
345 |
|
} |
346 |
125724 |
Node conc; |
347 |
62862 |
if (!nrs.isNull()) |
348 |
|
{ |
349 |
101426 |
Trace("strings-extf-debug") |
350 |
50713 |
<< " symbolic def : " << nrs << std::endl; |
351 |
50713 |
if (!d_state.areEqual(nrs, nrc)) |
352 |
|
{ |
353 |
|
// infer symbolic unit |
354 |
1188 |
if (n.getType().isBoolean()) |
355 |
|
{ |
356 |
927 |
conc = nrc == d_true ? nrs : nrs.negate(); |
357 |
|
} |
358 |
|
else |
359 |
|
{ |
360 |
261 |
conc = nrs.eqNode(nrc); |
361 |
|
} |
362 |
1188 |
einfo.d_exp.clear(); |
363 |
|
} |
364 |
|
} |
365 |
|
else |
366 |
|
{ |
367 |
12149 |
if (!d_state.areEqual(n, nrc)) |
368 |
|
{ |
369 |
555 |
if (n.getType().isBoolean()) |
370 |
|
{ |
371 |
250 |
if (d_state.areEqual(n, nrc == d_true ? d_false : d_true)) |
372 |
|
{ |
373 |
207 |
einfo.d_exp.push_back(nrc == d_true ? n.negate() : n); |
374 |
207 |
conc = d_false; |
375 |
|
} |
376 |
|
else |
377 |
|
{ |
378 |
43 |
conc = nrc == d_true ? n : n.negate(); |
379 |
|
} |
380 |
|
} |
381 |
|
else |
382 |
|
{ |
383 |
305 |
conc = n.eqNode(nrc); |
384 |
|
} |
385 |
|
} |
386 |
|
} |
387 |
62862 |
if (!conc.isNull()) |
388 |
|
{ |
389 |
3486 |
Trace("strings-extf") |
390 |
1743 |
<< " resolve extf : " << sn << " -> " << nrc << std::endl; |
391 |
1743 |
InferenceId inf = effort == 0 ? InferenceId::STRINGS_EXTF : InferenceId::STRINGS_EXTF_N; |
392 |
1743 |
d_im.sendInference(einfo.d_exp, conc, inf, false, true); |
393 |
1743 |
d_statistics.d_cdSimplifications << n.getKind(); |
394 |
|
} |
395 |
|
} |
396 |
|
else |
397 |
|
{ |
398 |
|
// check if it is already equal, if so, mark as reduced. Otherwise, do |
399 |
|
// nothing. |
400 |
|
if (d_state.areEqual(n, nrc)) |
401 |
|
{ |
402 |
|
Trace("strings-extf") |
403 |
|
<< " resolved extf, since satisfied by model: " << n |
404 |
|
<< std::endl; |
405 |
|
einfo.d_modelActive = false; |
406 |
|
} |
407 |
|
} |
408 |
62862 |
reduced = true; |
409 |
|
} |
410 |
|
else |
411 |
|
{ |
412 |
|
// if this was a predicate which changed after substitution + rewriting |
413 |
45425 |
if (!einfo.d_const.isNull() && nrc.getType().isBoolean() && nrc != n) |
414 |
|
{ |
415 |
10474 |
bool pol = einfo.d_const == d_true; |
416 |
20948 |
Node nrcAssert = pol ? nrc : nrc.negate(); |
417 |
20948 |
Node nAssert = pol ? n : n.negate(); |
418 |
10474 |
Assert(effort < 3); |
419 |
10474 |
einfo.d_exp.push_back(nAssert); |
420 |
10474 |
Trace("strings-extf-debug") << " decomposable..." << std::endl; |
421 |
20948 |
Trace("strings-extf") << " resolve extf : " << sn << " -> " << nrc |
422 |
10474 |
<< ", const = " << einfo.d_const << std::endl; |
423 |
|
// We send inferences internal here, which may help show unsat. |
424 |
|
// However, we do not make a determination whether n can be marked |
425 |
|
// reduced since this argument may be circular: we may infer than n |
426 |
|
// can be reduced to something else, but that thing may argue that it |
427 |
|
// can be reduced to n, in theory. |
428 |
10474 |
InferenceId infer = |
429 |
10474 |
effort == 0 ? InferenceId::STRINGS_EXTF_D : InferenceId::STRINGS_EXTF_D_N; |
430 |
10474 |
d_im.sendInternalInference(einfo.d_exp, nrcAssert, infer); |
431 |
|
} |
432 |
45425 |
to_reduce = nrc; |
433 |
|
} |
434 |
|
} |
435 |
|
// We must use the original n here to avoid circular justifications for |
436 |
|
// why extended functions are reduced. In particular, n should never be a |
437 |
|
// duplicate of another term considered in the block of code for |
438 |
|
// checkExtfInference below. |
439 |
|
// if not reduced and not processed |
440 |
611901 |
if (!reduced && !n.isNull() |
441 |
386980 |
&& inferProcessed.find(n) == inferProcessed.end()) |
442 |
|
{ |
443 |
162059 |
inferProcessed.insert(n); |
444 |
162059 |
Assert(effort < 3); |
445 |
162059 |
if (effort == 1) |
446 |
|
{ |
447 |
38886 |
Trace("strings-extf") |
448 |
19443 |
<< " cannot rewrite extf : " << to_reduce << std::endl; |
449 |
|
} |
450 |
|
// we take to_reduce to be the (partially) reduced version of n, which |
451 |
|
// is justified by the explanation in einfo. |
452 |
162059 |
checkExtfInference(n, to_reduce, einfo, effort); |
453 |
162059 |
if (Trace.isOn("strings-extf-list")) |
454 |
|
{ |
455 |
|
Trace("strings-extf-list") << " * " << to_reduce; |
456 |
|
if (!einfo.d_const.isNull()) |
457 |
|
{ |
458 |
|
Trace("strings-extf-list") << ", const = " << einfo.d_const; |
459 |
|
} |
460 |
|
if (n != to_reduce) |
461 |
|
{ |
462 |
|
Trace("strings-extf-list") << ", from " << n; |
463 |
|
} |
464 |
|
Trace("strings-extf-list") << std::endl; |
465 |
|
} |
466 |
162059 |
if (d_extt.isActive(n) && einfo.d_modelActive) |
467 |
|
{ |
468 |
162059 |
has_nreduce = true; |
469 |
|
} |
470 |
|
} |
471 |
224921 |
if (d_state.isInConflict()) |
472 |
|
{ |
473 |
211 |
Trace("strings-extf-debug") << " conflict, return." << std::endl; |
474 |
211 |
return; |
475 |
|
} |
476 |
|
} |
477 |
30540 |
d_hasExtf = has_nreduce; |
478 |
|
} |
479 |
|
|
480 |
162059 |
void ExtfSolver::checkExtfInference(Node n, |
481 |
|
Node nr, |
482 |
|
ExtfInfoTmp& in, |
483 |
|
int effort) |
484 |
|
{ |
485 |
162059 |
if (in.d_const.isNull()) |
486 |
|
{ |
487 |
202562 |
return; |
488 |
|
} |
489 |
71196 |
NodeManager* nm = NodeManager::currentNM(); |
490 |
142392 |
Trace("strings-extf-infer") << "checkExtfInference: " << n << " : " << nr |
491 |
71196 |
<< " == " << in.d_const << std::endl; |
492 |
|
|
493 |
|
// add original to explanation |
494 |
71196 |
if (n.getType().isBoolean()) |
495 |
|
{ |
496 |
|
// if Boolean, it's easy |
497 |
36165 |
in.d_exp.push_back(in.d_const.getConst<bool>() ? n : n.negate()); |
498 |
|
} |
499 |
|
else |
500 |
|
{ |
501 |
|
// otherwise, must explain via base node |
502 |
70062 |
Node r = d_state.getRepresentative(n); |
503 |
|
// explain using the base solver |
504 |
35031 |
d_bsolver.explainConstantEqc(n, r, in.d_exp); |
505 |
|
} |
506 |
|
|
507 |
|
// d_extfInferCache stores whether we have made the inferences associated |
508 |
|
// with a node n, |
509 |
|
// this may need to be generalized if multiple inferences apply |
510 |
|
|
511 |
71196 |
if (nr.getKind() == STRING_STRCTN) |
512 |
|
{ |
513 |
20836 |
Assert(in.d_const.isConst()); |
514 |
20836 |
bool pol = in.d_const.getConst<bool>(); |
515 |
25739 |
if ((pol && nr[1].getKind() == STRING_CONCAT) |
516 |
41602 |
|| (!pol && nr[0].getKind() == STRING_CONCAT)) |
517 |
|
{ |
518 |
|
// If str.contains( x, str.++( y1, ..., yn ) ), |
519 |
|
// we may infer str.contains( x, y1 ), ..., str.contains( x, yn ) |
520 |
|
// The following recognizes two situations related to the above reasoning: |
521 |
|
// (1) If ~str.contains( x, yi ) holds for some i, we are in conflict, |
522 |
|
// (2) If str.contains( x, yj ) already holds for some j, then the term |
523 |
|
// str.contains( x, yj ) is irrelevant since it is satisfied by all models |
524 |
|
// for str.contains( x, str.++( y1, ..., yn ) ). |
525 |
|
|
526 |
|
// Notice that the dual of the above reasoning also holds, i.e. |
527 |
|
// If ~str.contains( str.++( x1, ..., xn ), y ), |
528 |
|
// we may infer ~str.contains( x1, y ), ..., ~str.contains( xn, y ) |
529 |
|
// This is also handled here. |
530 |
1037 |
if (d_extfInferCache.find(nr) == d_extfInferCache.end()) |
531 |
|
{ |
532 |
403 |
d_extfInferCache.insert(nr); |
533 |
|
|
534 |
403 |
int index = pol ? 1 : 0; |
535 |
806 |
std::vector<Node> children; |
536 |
403 |
children.push_back(nr[0]); |
537 |
403 |
children.push_back(nr[1]); |
538 |
1541 |
for (const Node& nrc : nr[index]) |
539 |
|
{ |
540 |
1138 |
children[index] = nrc; |
541 |
2276 |
Node conc = nm->mkNode(STRING_STRCTN, children); |
542 |
1138 |
conc = Rewriter::rewrite(pol ? conc : conc.negate()); |
543 |
|
// check if it already (does not) hold |
544 |
1138 |
if (d_state.hasTerm(conc)) |
545 |
|
{ |
546 |
46 |
if (d_state.areEqual(conc, d_false)) |
547 |
|
{ |
548 |
|
// we are in conflict |
549 |
|
d_im.sendInference(in.d_exp, conc, InferenceId::STRINGS_CTN_DECOMPOSE); |
550 |
|
} |
551 |
46 |
else if (d_extt.hasFunctionKind(conc.getKind())) |
552 |
|
{ |
553 |
|
// can mark as reduced, since model for n implies model for conc |
554 |
|
d_extt.markReduced(conc, ExtReducedId::STRINGS_CTN_DECOMPOSE); |
555 |
|
} |
556 |
|
} |
557 |
|
} |
558 |
|
} |
559 |
|
} |
560 |
|
else |
561 |
|
{ |
562 |
79196 |
if (std::find(d_extfInfoTmp[nr[0]].d_ctn[pol].begin(), |
563 |
39598 |
d_extfInfoTmp[nr[0]].d_ctn[pol].end(), |
564 |
79196 |
nr[1]) |
565 |
59397 |
== d_extfInfoTmp[nr[0]].d_ctn[pol].end()) |
566 |
|
{ |
567 |
39522 |
Trace("strings-extf-debug") << " store contains info : " << nr[0] |
568 |
19761 |
<< " " << pol << " " << nr[1] << std::endl; |
569 |
|
// Store s (does not) contains t, since nr = (~)contains( s, t ) holds. |
570 |
19761 |
d_extfInfoTmp[nr[0]].d_ctn[pol].push_back(nr[1]); |
571 |
19761 |
d_extfInfoTmp[nr[0]].d_ctnFrom[pol].push_back(n); |
572 |
|
// Do transistive closure on contains, e.g. |
573 |
|
// if contains( s, t ) and ~contains( s, r ), then ~contains( t, r ). |
574 |
|
|
575 |
|
// The following infers new (negative) contains based on the above |
576 |
|
// reasoning, provided that ~contains( t, r ) does not |
577 |
|
// already hold in the current context. We test this by checking that |
578 |
|
// contains( t, r ) is not already asserted false in the current |
579 |
|
// context. We also handle the case where contains( t, r ) is equivalent |
580 |
|
// to t = r, in which case we check that t != r does not already hold |
581 |
|
// in the current context. |
582 |
|
|
583 |
|
// Notice that form of the above inference is enough to find |
584 |
|
// conflicts purely due to contains predicates. For example, if we |
585 |
|
// have only positive occurrences of contains, then no conflicts due to |
586 |
|
// contains predicates are possible and this schema does nothing. For |
587 |
|
// example, note that contains( s, t ) and contains( t, r ) implies |
588 |
|
// contains( s, r ), which we could but choose not to infer. Instead, |
589 |
|
// we prefer being lazy: only if ~contains( s, r ) appears later do we |
590 |
|
// infer ~contains( t, r ), which suffices to show a conflict. |
591 |
19761 |
bool opol = !pol; |
592 |
23211 |
for (unsigned i = 0, size = d_extfInfoTmp[nr[0]].d_ctn[opol].size(); |
593 |
23211 |
i < size; |
594 |
|
i++) |
595 |
|
{ |
596 |
6900 |
Node onr = d_extfInfoTmp[nr[0]].d_ctn[opol][i]; |
597 |
|
Node concOrig = |
598 |
6900 |
nm->mkNode(STRING_STRCTN, pol ? nr[1] : onr, pol ? onr : nr[1]); |
599 |
6900 |
Node conc = Rewriter::rewrite(concOrig); |
600 |
|
// For termination concerns, we only do the inference if the contains |
601 |
|
// does not rewrite (and thus does not introduce new terms). |
602 |
3450 |
if (conc == concOrig) |
603 |
|
{ |
604 |
17 |
bool do_infer = false; |
605 |
17 |
conc = conc.negate(); |
606 |
17 |
bool pol2 = conc.getKind() != NOT; |
607 |
34 |
Node lit = pol2 ? conc : conc[0]; |
608 |
17 |
if (lit.getKind() == EQUAL) |
609 |
|
{ |
610 |
|
do_infer = pol2 ? !d_state.areEqual(lit[0], lit[1]) |
611 |
|
: !d_state.areDisequal(lit[0], lit[1]); |
612 |
|
} |
613 |
|
else |
614 |
|
{ |
615 |
17 |
do_infer = !d_state.areEqual(lit, pol2 ? d_true : d_false); |
616 |
|
} |
617 |
17 |
if (do_infer) |
618 |
|
{ |
619 |
18 |
std::vector<Node> exp_c; |
620 |
9 |
exp_c.insert(exp_c.end(), in.d_exp.begin(), in.d_exp.end()); |
621 |
18 |
Node ofrom = d_extfInfoTmp[nr[0]].d_ctnFrom[opol][i]; |
622 |
9 |
Assert(d_extfInfoTmp.find(ofrom) != d_extfInfoTmp.end()); |
623 |
27 |
exp_c.insert(exp_c.end(), |
624 |
9 |
d_extfInfoTmp[ofrom].d_exp.begin(), |
625 |
36 |
d_extfInfoTmp[ofrom].d_exp.end()); |
626 |
9 |
d_im.sendInference(exp_c, conc, InferenceId::STRINGS_CTN_TRANS); |
627 |
|
} |
628 |
|
} |
629 |
|
} |
630 |
|
} |
631 |
|
else |
632 |
|
{ |
633 |
|
// If we already know that s (does not) contain t, then n may be |
634 |
|
// redundant. However, we do not mark n as reduced here, since strings |
635 |
|
// reductions may require dependencies between extended functions. |
636 |
|
// Marking reduced here could lead to incorrect models if an |
637 |
|
// extended function is marked reduced based on an assignment to |
638 |
|
// something that depends on n. |
639 |
38 |
Trace("strings-extf-debug") << " redundant." << std::endl; |
640 |
|
} |
641 |
|
} |
642 |
20836 |
return; |
643 |
|
} |
644 |
|
|
645 |
|
// If it's not a predicate, see if we can solve the equality n = c, where c |
646 |
|
// is the constant that extended term n is equal to. |
647 |
100720 |
Node inferEq = nr.eqNode(in.d_const); |
648 |
100720 |
Node inferEqr = Rewriter::rewrite(inferEq); |
649 |
100720 |
Node inferEqrr = inferEqr; |
650 |
50360 |
if (inferEqr.getKind() == EQUAL) |
651 |
|
{ |
652 |
|
// try to use the extended rewriter for equalities |
653 |
35424 |
inferEqrr = d_rewriter.rewriteEqualityExt(inferEqr); |
654 |
|
} |
655 |
50360 |
if (inferEqrr != inferEqr) |
656 |
|
{ |
657 |
2035 |
inferEqrr = Rewriter::rewrite(inferEqrr); |
658 |
4070 |
Trace("strings-extf-infer") << "checkExtfInference: " << inferEq |
659 |
2035 |
<< " ...reduces to " << inferEqrr << std::endl; |
660 |
2035 |
d_im.sendInternalInference(in.d_exp, inferEqrr, InferenceId::STRINGS_EXTF_EQ_REW); |
661 |
|
} |
662 |
|
} |
663 |
|
|
664 |
513314 |
Node ExtfSolver::getCurrentSubstitutionFor(int effort, |
665 |
|
Node n, |
666 |
|
std::vector<Node>& exp) |
667 |
|
{ |
668 |
513314 |
if (effort >= 3) |
669 |
|
{ |
670 |
|
// model values |
671 |
|
Node mv = d_state.getModel()->getRepresentative(n); |
672 |
|
Trace("strings-subs") << " model val : " << mv << std::endl; |
673 |
|
return mv; |
674 |
|
} |
675 |
1026628 |
Node nr = d_state.getRepresentative(n); |
676 |
1026628 |
Node c = d_bsolver.explainBestContentEqc(n, nr, exp); |
677 |
513314 |
if (!c.isNull()) |
678 |
|
{ |
679 |
298834 |
return c; |
680 |
|
} |
681 |
214480 |
else if (effort >= 1 && n.getType().isStringLike()) |
682 |
|
{ |
683 |
16924 |
Assert(effort < 3); |
684 |
|
// normal forms |
685 |
16924 |
NormalForm& nfnr = d_csolver.getNormalForm(nr); |
686 |
33848 |
Node ns = d_csolver.getNormalString(nfnr.d_base, exp); |
687 |
33848 |
Trace("strings-subs") << " normal eqc : " << ns << " " << nfnr.d_base |
688 |
16924 |
<< " " << nr << std::endl; |
689 |
16924 |
if (!nfnr.d_base.isNull()) |
690 |
|
{ |
691 |
16924 |
d_im.addToExplanation(n, nfnr.d_base, exp); |
692 |
|
} |
693 |
16924 |
return ns; |
694 |
|
} |
695 |
197556 |
return n; |
696 |
|
} |
697 |
|
|
698 |
7356 |
const std::map<Node, ExtfInfoTmp>& ExtfSolver::getInfo() const |
699 |
|
{ |
700 |
7356 |
return d_extfInfoTmp; |
701 |
|
} |
702 |
|
bool ExtfSolver::hasExtendedFunctions() const { return d_hasExtf.get(); } |
703 |
|
|
704 |
7356 |
std::vector<Node> ExtfSolver::getActive(Kind k) const |
705 |
|
{ |
706 |
7356 |
return d_extt.getActive(k); |
707 |
|
} |
708 |
|
|
709 |
|
bool StringsExtfCallback::getCurrentSubstitution( |
710 |
|
int effort, |
711 |
|
const std::vector<Node>& vars, |
712 |
|
std::vector<Node>& subs, |
713 |
|
std::map<Node, std::vector<Node> >& exp) |
714 |
|
{ |
715 |
|
Trace("strings-subs") << "getCurrentSubstitution, effort = " << effort |
716 |
|
<< std::endl; |
717 |
|
for (const Node& v : vars) |
718 |
|
{ |
719 |
|
Trace("strings-subs") << " get subs for " << v << "..." << std::endl; |
720 |
|
Node s = d_esolver->getCurrentSubstitutionFor(effort, v, exp[v]); |
721 |
|
subs.push_back(s); |
722 |
|
} |
723 |
|
return true; |
724 |
|
} |
725 |
|
|
726 |
|
std::string ExtfSolver::debugPrintModel() |
727 |
|
{ |
728 |
|
std::stringstream ss; |
729 |
|
std::vector<Node> extf; |
730 |
|
d_extt.getTerms(extf); |
731 |
|
// each extended function should have at least one annotation below |
732 |
|
for (const Node& n : extf) |
733 |
|
{ |
734 |
|
ss << "- " << n; |
735 |
|
ExtReducedId id; |
736 |
|
if (!d_extt.isActive(n, id)) |
737 |
|
{ |
738 |
|
ss << " :extt-inactive " << id; |
739 |
|
} |
740 |
|
if (!d_extfInfoTmp[n].d_modelActive) |
741 |
|
{ |
742 |
|
ss << " :model-inactive"; |
743 |
|
} |
744 |
|
if (d_reduced.find(n) != d_reduced.end()) |
745 |
|
{ |
746 |
|
ss << " :reduced"; |
747 |
|
} |
748 |
|
ss << std::endl; |
749 |
|
} |
750 |
|
return ss.str(); |
751 |
|
} |
752 |
|
|
753 |
|
} // namespace strings |
754 |
|
} // namespace theory |
755 |
103067 |
} // namespace cvc5 |