Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Andres Noetzli
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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/array_solver.h"
20 : : #include "theory/strings/sequences_rewriter.h"
21 : : #include "theory/strings/theory_strings_preprocess.h"
22 : : #include "theory/strings/theory_strings_utils.h"
23 : : #include "util/statistics_registry.h"
24 : :
25 : : using namespace std;
26 : : using namespace cvc5::context;
27 : : using namespace cvc5::internal::kind;
28 : :
29 : : namespace cvc5::internal {
30 : : namespace theory {
31 : : namespace strings {
32 : :
33 : 51396 : ExtfSolver::ExtfSolver(Env& env,
34 : : SolverState& s,
35 : : InferenceManager& im,
36 : : TermRegistry& tr,
37 : : StringsRewriter& rewriter,
38 : : BaseSolver& bs,
39 : : CoreSolver& cs,
40 : : ExtTheory& et,
41 : 51396 : SequencesStatistics& statistics)
42 : : : EnvObj(env),
43 : : d_state(s),
44 : : d_im(im),
45 : : d_termReg(tr),
46 : : d_rewriter(rewriter),
47 : : d_bsolver(bs),
48 : : d_csolver(cs),
49 : : d_extt(et),
50 : : d_statistics(statistics),
51 : 51396 : d_preproc(env, d_termReg.getSkolemCache(), &statistics.d_reductions),
52 : 0 : d_hasExtf(context(), false),
53 : : d_extfInferCache(context()),
54 : 51396 : d_reduced(userContext())
55 : : {
56 : 51396 : d_extt.addFunctionKind(Kind::STRING_SUBSTR);
57 : 51396 : d_extt.addFunctionKind(Kind::STRING_UPDATE);
58 : 51396 : d_extt.addFunctionKind(Kind::STRING_INDEXOF);
59 : 51396 : d_extt.addFunctionKind(Kind::STRING_INDEXOF_RE);
60 : 51396 : d_extt.addFunctionKind(Kind::STRING_ITOS);
61 : 51396 : d_extt.addFunctionKind(Kind::STRING_STOI);
62 : 51396 : d_extt.addFunctionKind(Kind::STRING_REPLACE);
63 : 51396 : d_extt.addFunctionKind(Kind::STRING_REPLACE_ALL);
64 : 51396 : d_extt.addFunctionKind(Kind::STRING_REPLACE_RE);
65 : 51396 : d_extt.addFunctionKind(Kind::STRING_REPLACE_RE_ALL);
66 : 51396 : d_extt.addFunctionKind(Kind::STRING_CONTAINS);
67 : 51396 : d_extt.addFunctionKind(Kind::STRING_IN_REGEXP);
68 : 51396 : d_extt.addFunctionKind(Kind::STRING_LEQ);
69 : 51396 : d_extt.addFunctionKind(Kind::STRING_TO_CODE);
70 : 51396 : d_extt.addFunctionKind(Kind::STRING_TO_LOWER);
71 : 51396 : d_extt.addFunctionKind(Kind::STRING_TO_UPPER);
72 : 51396 : d_extt.addFunctionKind(Kind::STRING_REV);
73 : 51396 : d_extt.addFunctionKind(Kind::STRING_UNIT);
74 : 51396 : d_extt.addFunctionKind(Kind::SEQ_UNIT);
75 : 51396 : d_extt.addFunctionKind(Kind::SEQ_NTH);
76 : :
77 : 51396 : d_true = nodeManager()->mkConst(true);
78 : 51396 : d_false = nodeManager()->mkConst(false);
79 : 51396 : }
80 : :
81 : 51140 : ExtfSolver::~ExtfSolver() {}
82 : :
83 : 415101 : bool ExtfSolver::shouldDoReduction(int effort, Node n, int pol)
84 : : {
85 [ + - ]: 830202 : Trace("strings-extf-debug") << "shouldDoReduction " << n << ", pol " << pol
86 : 415101 : << ", effort " << effort << std::endl;
87 [ + + ]: 415101 : if (!isActiveInModel(n))
88 : : {
89 : : // n is not active in the model, no need to reduce
90 [ + - ]: 2303 : Trace("strings-extf-debug") << "...skip due to model active" << std::endl;
91 : 2303 : return false;
92 : : }
93 : : // check with negation if requested (only applied to Boolean terms)
94 : 412798 : Assert(n.getType().isBoolean() || pol != -1);
95 [ + + ]: 825596 : Node nn = pol == -1 ? n.notNode() : n;
96 [ + + ]: 412798 : if (d_reduced.find(nn) != d_reduced.end())
97 : : {
98 : : // already sent a reduction lemma
99 [ + - ]: 238514 : Trace("strings-extf-debug") << "...skip due to reduced" << std::endl;
100 : 238514 : return false;
101 : : }
102 : 174284 : Kind k = n.getKind();
103 : : // determine if it is the right effort
104 [ + + ][ + + ]: 174284 : if (k == Kind::STRING_SUBSTR || (k == Kind::STRING_CONTAINS && pol == 1))
[ + + ]
105 : : {
106 : : // we reduce these semi-eagerly, at effort 1
107 : 3169 : return (effort == 1);
108 : : }
109 [ + + ][ + - ]: 171115 : else if (k == Kind::STRING_CONTAINS && pol == -1)
110 : : {
111 : : // negative contains reduces at level 2, or 3 if guessing model
112 [ + - ]: 20288 : int reffort = options().strings.stringModelBasedReduction ? 3 : 2;
113 : 20288 : return (effort == reffort);
114 : : }
115 [ + - ]: 146256 : else if (k == Kind::SEQ_UNIT || k == Kind::STRING_UNIT
116 [ + + ][ + + ]: 146256 : || k == Kind::STRING_IN_REGEXP || k == Kind::STRING_TO_CODE
117 [ + + ][ + + ]: 297083 : || (n.getType().isBoolean() && pol == 0))
[ - + ][ + + ]
[ + + ][ - - ]
118 : : {
119 : : // never necessary to reduce seq.unit. str.to_code or str.in_re here.
120 : : // also, we do not reduce str.contains that are preregistered but not
121 : : // asserted (pol=0).
122 : 121556 : return false;
123 : : }
124 [ + + ]: 29271 : else if (options().strings.seqArray != options::SeqArrayMode::NONE)
125 : : {
126 [ + + ]: 8636 : if (k == Kind::SEQ_NTH)
127 : : {
128 : : // don't need to reduce seq.nth when sequence update solver is used
129 : 7340 : return false;
130 : : }
131 [ - + ]: 194 : else if ((k == Kind::STRING_UPDATE || k == Kind::STRING_SUBSTR)
132 [ + + ][ + + ]: 1490 : && d_termReg.isHandledUpdateOrSubstr(n))
[ + + ][ + + ]
[ - - ]
133 : : {
134 : : // don't need to reduce certain seq.update
135 : : // don't need to reduce certain seq.extract with length 1
136 : 934 : return false;
137 : : }
138 : : }
139 : : // all other operators reduce at level 2
140 : 20997 : return (effort == 2);
141 : : }
142 : :
143 : 4963 : void ExtfSolver::doReduction(Node n, int pol)
144 : : {
145 [ + - ]: 9926 : Trace("strings-extf-debug")
146 : 4963 : << "doReduction " << n << ", pol " << pol << std::endl;
147 : : // polarity : 1 true, -1 false, 0 neither
148 : 4963 : Kind k = n.getKind();
149 [ + + ][ + + ]: 4963 : if (k == Kind::STRING_CONTAINS && pol == -1)
150 : : {
151 : 19 : Node x = n[0];
152 : 19 : Node s = n[1];
153 : 19 : std::vector<Node> lexp;
154 : 19 : Node lenx = d_state.getLength(x, lexp);
155 : 19 : Node lens = d_state.getLength(s, lexp);
156 : : // we use an optimized reduction for negative string contains if the
157 : : // lengths are equal
158 [ - + ]: 19 : if (d_state.areEqual(lenx, lens))
159 : : {
160 [ - - ]: 0 : Trace("strings-extf-debug")
161 : 0 : << " resolve extf : " << n << " based on equal lengths disequality."
162 : 0 : << std::endl;
163 : : // We can reduce negative contains to a disequality when lengths are
164 : : // equal. In other words, len( x ) = len( s ) implies
165 : : // ~contains( x, s ) reduces to x != s.
166 : : // len( x ) = len( s ) ^ ~contains( x, s ) => x != s
167 : 0 : lexp.push_back(lenx.eqNode(lens));
168 : 0 : lexp.push_back(n.negate());
169 : 0 : Node xneqs = x.eqNode(s).negate();
170 : 0 : d_im.sendInference(
171 : : lexp, xneqs, InferenceId::STRINGS_CTN_NEG_EQUAL, false, true);
172 : : // this depends on the current assertions, so this
173 : : // inference is context-dependent
174 : 0 : d_extt.markInactive(n, ExtReducedId::STRINGS_NEG_CTN_DEQ, true);
175 : 0 : return;
176 : : }
177 : : }
178 [ + + ]: 9926 : Node nn = pol == -1 ? n.notNode() : n;
179 [ + - ]: 9926 : Trace("strings-process-debug")
180 : 4963 : << "Process reduction for " << n << ", pol = " << pol << std::endl;
181 [ + + ][ + + ]: 4963 : if (k == Kind::STRING_CONTAINS && pol == 1)
182 : : {
183 : 894 : Node x = n[0];
184 : 894 : Node s = n[1];
185 : : // positive contains reduces to a equality
186 : 447 : SkolemCache* skc = d_termReg.getSkolemCache();
187 : 894 : Node eq = d_termReg.eagerReduce(n, skc, d_termReg.getAlphabetCardinality());
188 [ - + ][ - + ]: 447 : Assert(!eq.isNull());
[ - - ]
189 : 894 : Assert(eq.getKind() == Kind::ITE && eq[0] == n);
190 : 447 : eq = eq[1];
191 : 894 : std::vector<Node> expn;
192 : 447 : expn.push_back(n);
193 : 447 : d_im.sendInference(expn, expn, eq, InferenceId::STRINGS_CTN_POS, false, true);
194 [ + - ]: 894 : Trace("strings-extf-debug")
195 : 0 : << " resolve extf : " << n << " based on positive contain reduction."
196 : 447 : << std::endl;
197 [ + - ]: 894 : Trace("strings-red-lemma") << "Reduction (positive contains) lemma : " << n
198 : 447 : << " => " << eq << std::endl;
199 : : // reduced positively
200 [ - + ][ - + ]: 447 : Assert(nn == n);
[ - - ]
201 : 894 : d_reduced.insert(nn);
202 : : }
203 : : else
204 : : {
205 : 4516 : NodeManager* nm = nodeManager();
206 [ + + ][ + + ]: 4516 : Assert(k == Kind::STRING_SUBSTR || k == Kind::STRING_UPDATE
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ - + ]
[ - + ][ - - ]
207 : : || k == Kind::STRING_CONTAINS || k == Kind::STRING_INDEXOF
208 : : || k == Kind::STRING_INDEXOF_RE || k == Kind::STRING_ITOS
209 : : || k == Kind::STRING_STOI || k == Kind::STRING_REPLACE
210 : : || k == Kind::STRING_REPLACE_ALL || k == Kind::SEQ_NTH
211 : : || k == Kind::STRING_REPLACE_RE || k == Kind::STRING_REPLACE_RE_ALL
212 : : || k == Kind::STRING_LEQ || k == Kind::STRING_TO_LOWER
213 : : || k == Kind::STRING_TO_UPPER || k == Kind::STRING_REV)
214 : 0 : << "Unknown reduction: " << k;
215 : 9032 : std::vector<Node> new_nodes;
216 : 9032 : Node res = d_preproc.simplify(n, new_nodes);
217 [ - + ][ - + ]: 4516 : Assert(res != n);
[ - - ]
218 : 4516 : new_nodes.push_back(n.eqNode(res));
219 : : Node nnlem =
220 [ - + ]: 9032 : new_nodes.size() == 1 ? new_nodes[0] : nm->mkNode(Kind::AND, new_nodes);
221 : : // in rare case where it rewrites to true, just record it is reduced
222 [ - + ]: 4516 : if (rewrite(nnlem) == d_true)
223 : : {
224 [ - - ]: 0 : Trace("strings-extf-debug")
225 : 0 : << " resolve extf : " << n << " based on (trivial) reduction."
226 : 0 : << std::endl;
227 : 0 : d_reduced.insert(nn);
228 : : }
229 : : else
230 : : {
231 : 9032 : InferInfo ii(InferenceId::STRINGS_REDUCTION);
232 : : // ensure that we are called to process the side effects
233 : 4516 : ii.d_sim = this;
234 : 4516 : ii.d_conc = nnlem;
235 : 4516 : d_im.sendInference(ii, true);
236 [ + - ]: 9032 : Trace("strings-extf-debug")
237 : 4516 : << " resolve extf : " << n << " based on reduction." << std::endl;
238 : 4516 : d_reductionWaitingMap[nnlem] = nn;
239 : : }
240 : : }
241 : : }
242 : :
243 : 60340 : void ExtfSolver::checkExtfReductionsEager()
244 : : {
245 : : // return value is ignored
246 : 60340 : checkExtfReductionsInternal(1, true);
247 : 60340 : }
248 : :
249 : 34189 : void ExtfSolver::checkExtfReductions(Theory::Effort e)
250 : : {
251 [ + + ]: 34189 : int effort = e == Theory::EFFORT_LAST_CALL ? 3 : 2;
252 : : // return value is ignored
253 : 34189 : checkExtfReductionsInternal(effort, true);
254 : 34189 : }
255 : :
256 : 94529 : bool ExtfSolver::checkExtfReductionsInternal(int effort, bool doSend)
257 : : {
258 : : // Notice we don't make a standard call to ExtTheory::doReductions here,
259 : : // since certain optimizations like context-dependent reductions and
260 : : // stratifying effort levels are done in doReduction below.
261 : : // We only have to reduce extended functions that are both relevant and
262 : : // active (see getRelevantActive).
263 : 189058 : std::vector<Node> extf = getRelevantActive();
264 [ + - ]: 189058 : Trace("strings-process") << " checking " << extf.size() << " active extf"
265 : 94529 : << std::endl;
266 [ + + ]: 504667 : for (const Node& n : extf)
267 : : {
268 [ - + ][ - + ]: 415101 : Assert(!d_state.isInConflict());
[ - - ]
269 [ + - ]: 830202 : Trace("strings-extf-debug")
270 : 0 : << " check " << n
271 : 415101 : << ", active in model=" << d_extfInfoTmp[n].d_modelActive << std::endl;
272 : : // polarity, 1: positive, -1: negative, 0: neither
273 : 415101 : int pol = 0;
274 [ + + ]: 415101 : if (n.getType().isBoolean())
275 : : {
276 : 185175 : Node rep = d_state.getRepresentative(n);
277 [ + - ]: 61725 : if (rep.isConst())
278 : : {
279 [ + + ]: 61725 : pol = rep.getConst<bool>() ? 1 : -1;
280 : : }
281 : : }
282 [ + + ]: 415101 : if (shouldDoReduction(effort, n, pol))
283 : : {
284 : 4963 : doReduction(n, pol);
285 : : // we do not mark as inactive, since we may want to evaluate
286 [ + - ]: 4963 : if (d_im.hasProcessed())
287 : : {
288 : 4963 : return true;
289 : : }
290 : : }
291 : : }
292 : 89566 : return false;
293 : : }
294 : :
295 : 116944 : void ExtfSolver::checkExtfEval(int effort)
296 : : {
297 [ + - ]: 233888 : Trace("strings-extf-list")
298 : 116944 : << "Active extended functions, effort=" << effort << " : " << std::endl;
299 : 116944 : d_extfInfoTmp.clear();
300 : 116944 : NodeManager* nm = nodeManager();
301 : 116944 : bool has_nreduce = false;
302 : 116944 : std::vector<Node> terms = d_extt.getActive();
303 : : // the set of terms we have done extf inferences for
304 : 116944 : std::unordered_set<Node> inferProcessed;
305 [ + + ]: 908787 : for (const Node& n : terms)
306 : : {
307 : : // Setup information about n, including if it is equal to a constant.
308 : 792293 : ExtfInfoTmp& einfo = d_extfInfoTmp[n];
309 [ - + ][ - + ]: 792293 : Assert(einfo.d_exp.empty());
[ - - ]
310 : 1584590 : Node r = d_state.getRepresentative(n);
311 : 792293 : einfo.d_const = d_bsolver.getConstantEqc(r);
312 : : // Get the current values of the children of n.
313 : : // Notice that we look up the value of the direct children of n, and not
314 : : // their free variables. In other words, given a term:
315 : : // t = (str.replace "B" (str.replace x "A" "B") "C")
316 : : // we may build the explanation that:
317 : : // ((str.replace x "A" "B") = "B") => t = (str.replace "B" "B" "C")
318 : : // instead of basing this on the free variable x:
319 : : // (x = "A") => t = (str.replace "B" (str.replace "A" "A" "B") "C")
320 : : // Although both allow us to infer t = "C", it is important to use the
321 : : // first kind of inference since it ensures that its subterms have the
322 : : // expected values. Otherwise, we may in rare cases fail to realize that
323 : : // the subterm (str.replace x "A" "B") does not currently have the correct
324 : : // value, say in this example that (str.replace x "A" "B") != "B".
325 : 792293 : std::vector<Node> exp;
326 : 792293 : std::vector<Node> schildren;
327 : : // seq.unit is parameterized
328 [ - + ]: 792293 : if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
329 : : {
330 : 0 : schildren.push_back(n.getOperator());
331 : : }
332 : 792293 : bool schanged = false;
333 [ + + ]: 2564680 : for (const Node& nc : n)
334 : : {
335 : 1772380 : Node sc = getCurrentSubstitutionFor(effort, nc, exp);
336 : 1772380 : schildren.push_back(sc);
337 [ + + ][ + + ]: 1772380 : schanged = schanged || sc != nc;
338 : : }
339 : : // If there is information involving the children, attempt to do an
340 : : // inference and/or mark n as reduced.
341 : 792293 : bool reduced = false;
342 : 792293 : Node to_reduce = n;
343 [ + + ]: 792293 : if (schanged)
344 : : {
345 : 589590 : Node sn = nm->mkNode(n.getKind(), schildren);
346 [ + - ]: 589590 : Trace("strings-extf-debug")
347 : 0 : << "Check extf " << n << " == " << sn
348 : 0 : << ", constant = " << einfo.d_const << ", effort=" << effort
349 : 294795 : << ", exp " << exp << std::endl;
350 : 294795 : einfo.d_exp.insert(einfo.d_exp.end(), exp.begin(), exp.end());
351 : : // inference is rewriting the substituted node
352 : 589590 : Node nrc = rewrite(sn);
353 : : // if rewrites to a constant, then do the inference and mark as reduced
354 [ + + ]: 294795 : if (nrc.isConst())
355 : : {
356 : : // at effort=3, our substitution is from the model, and we don't do
357 : : // inferences based on the model, instead we check whether the
358 : : // cosntraint is already equal to its expected value below.
359 [ + + ]: 138087 : if (effort < 3)
360 : : {
361 : 131185 : d_extt.markInactive(n, ExtReducedId::STRINGS_SR_CONST);
362 [ + - ]: 262370 : Trace("strings-extf-debug")
363 : 131185 : << " resolvable by evaluation..." << std::endl;
364 : 262370 : std::vector<Node> exps;
365 : : // The following optimization gets the "symbolic definition" of
366 : : // an extended term. The symbolic definition of a term t is a term
367 : : // t' where constants are replaced by their corresponding proxy
368 : : // variables.
369 : : // For example, if lsym is a proxy variable for "", then
370 : : // str.replace( lsym, lsym, lsym ) is the symbolic definition for
371 : : // str.replace( "", "", "" ). It is generally better to use symbolic
372 : : // definitions when doing cd-rewriting for the purpose of minimizing
373 : : // clauses, e.g. we infer the unit equality:
374 : : // str.replace( lsym, lsym, lsym ) == ""
375 : : // instead of making this inference multiple times:
376 : : // x = "" => str.replace( x, x, x ) == ""
377 : : // y = "" => str.replace( y, y, y ) == ""
378 [ + - ]: 262370 : Trace("strings-extf-debug")
379 : 131185 : << " get symbolic definition..." << std::endl;
380 : 262370 : Node nrs;
381 : : // only use symbolic definitions if option is set
382 [ + - ]: 131185 : if (options().strings.stringInferSym)
383 : : {
384 : 131185 : nrs = d_termReg.getSymbolicDefinition(sn, exps);
385 : : }
386 [ + + ]: 131185 : if (!nrs.isNull())
387 : : {
388 [ + - ]: 187674 : Trace("strings-extf-debug")
389 : 93837 : << " rewrite " << nrs << "..." << std::endl;
390 : 187674 : Node nrsr = rewrite(nrs);
391 : : // ensure the symbolic form is not rewritable
392 [ + + ]: 93837 : if (nrsr != nrs)
393 : : {
394 : : // we cannot use the symbolic definition if it rewrites
395 [ + - ]: 10384 : Trace("strings-extf-debug")
396 : 5192 : << " symbolic definition is trivial..." << std::endl;
397 : 5192 : nrs = Node::null();
398 : : }
399 : : }
400 : : else
401 : : {
402 [ + - ]: 74696 : Trace("strings-extf-debug")
403 : 37348 : << " could not infer symbolic definition." << std::endl;
404 : : }
405 : 262370 : Node conc;
406 [ + + ]: 131185 : if (!nrs.isNull())
407 : : {
408 [ + - ]: 177290 : Trace("strings-extf-debug")
409 : 88645 : << " symbolic def : " << nrs << std::endl;
410 [ + + ]: 88645 : if (!d_state.areEqual(nrs, nrc))
411 : : {
412 : : // infer symbolic unit
413 [ + + ]: 2901 : if (n.getType().isBoolean())
414 : : {
415 [ + + ]: 1975 : conc = nrc == d_true ? nrs : nrs.negate();
416 : : }
417 : : else
418 : : {
419 : 926 : conc = nrs.eqNode(nrc);
420 : : }
421 : 2901 : einfo.d_exp.clear();
422 : : }
423 : : }
424 : : else
425 : : {
426 [ + + ]: 42540 : if (!d_state.areEqual(n, nrc))
427 : : {
428 [ + + ]: 4836 : if (n.getType().isBoolean())
429 : : {
430 [ + + ]: 3256 : conc = nrc == d_true ? n : n.negate();
431 : : }
432 : : else
433 : : {
434 : 1580 : conc = n.eqNode(nrc);
435 : : }
436 : : }
437 : : }
438 [ + + ]: 131185 : if (!conc.isNull())
439 : : {
440 [ + - ]: 15474 : Trace("strings-extf")
441 : 7737 : << " resolve extf : " << sn << " -> " << nrc << std::endl;
442 [ + + ]: 7737 : InferenceId inf = effort == 0 ? InferenceId::STRINGS_EXTF : InferenceId::STRINGS_EXTF_N;
443 : 7737 : d_im.sendInference(einfo.d_exp, conc, inf, false, true);
444 : 7737 : d_statistics.d_cdSimplifications << n.getKind();
445 : : }
446 : : }
447 : : else
448 : : {
449 : : // check if it is already equal, if so, mark as reduced. Otherwise, do
450 : : // nothing.
451 [ + + ]: 6902 : if (d_state.areEqual(n, nrc))
452 : : {
453 [ + - ]: 4668 : Trace("strings-extf")
454 : 0 : << " resolved extf, since satisfied by model: " << n
455 : 2334 : << std::endl;
456 : 2334 : einfo.d_modelActive = false;
457 : : }
458 : : }
459 : 138087 : reduced = true;
460 : : }
461 [ + + ]: 156708 : else if (effort < 3)
462 : : {
463 : : // if this was a predicate which changed after substitution + rewriting
464 : : // We only do this before models are constructed (effort<3)
465 [ + + ][ + + ]: 156247 : if (!einfo.d_const.isNull() && nrc.getType().isBoolean() && nrc != n)
[ + + ][ + + ]
[ + + ][ - - ]
466 : : {
467 : 22493 : bool pol = einfo.d_const == d_true;
468 [ + + ]: 44986 : Node nrcAssert = pol ? nrc : nrc.negate();
469 [ + + ]: 22493 : Node nAssert = pol ? n : n.negate();
470 : 22493 : einfo.d_exp.push_back(nAssert);
471 [ + - ]: 22493 : Trace("strings-extf-debug") << " decomposable..." << std::endl;
472 [ + - ]: 44986 : Trace("strings-extf") << " resolve extf : " << sn << " -> " << nrc
473 : 22493 : << ", const = " << einfo.d_const << std::endl;
474 : : // We send inferences internal here, which may help show unsat.
475 : : // However, we do not make a determination whether n can be marked
476 : : // reduced since this argument may be circular: we may infer than n
477 : : // can be reduced to something else, but that thing may argue that it
478 : : // can be reduced to n, in theory.
479 : 22493 : InferenceId infer =
480 [ + + ]: 22493 : effort == 0 ? InferenceId::STRINGS_EXTF_D : InferenceId::STRINGS_EXTF_D_N;
481 : 22493 : d_im.sendInternalInference(einfo.d_exp, nrcAssert, infer);
482 : : }
483 : 156247 : to_reduce = nrc;
484 : : }
485 : : }
486 : : // We must use the original n here to avoid circular justifications for
487 : : // why extended functions are reduced. In particular, n should never be a
488 : : // duplicate of another term considered in the block of code for
489 : : // checkExtfInference below.
490 : : // if not reduced and not processed
491 [ + - ]: 654206 : if (!reduced && !n.isNull()
492 [ + + ][ + - ]: 1446500 : && inferProcessed.find(n) == inferProcessed.end())
[ + + ]
493 : : {
494 : 654206 : inferProcessed.insert(n);
495 [ + + ]: 654206 : if (effort == 1)
496 : : {
497 [ + - ]: 162352 : Trace("strings-extf")
498 : 81176 : << " cannot rewrite extf : " << to_reduce << std::endl;
499 : : }
500 : : // we take to_reduce to be the (partially) reduced version of n, which
501 : : // is justified by the explanation in einfo. We only do this if we are
502 : : // not based on the model (effort<3).
503 [ + + ]: 654206 : if (effort < 3)
504 : : {
505 : 653731 : checkExtfInference(n, to_reduce, einfo, effort);
506 : : }
507 [ - + ]: 654206 : if (TraceIsOn("strings-extf-list"))
508 : : {
509 [ - - ]: 0 : Trace("strings-extf-list") << " * " << to_reduce;
510 [ - - ]: 0 : if (!einfo.d_const.isNull())
511 : : {
512 [ - - ]: 0 : Trace("strings-extf-list") << ", const = " << einfo.d_const;
513 : : }
514 [ - - ]: 0 : if (n != to_reduce)
515 : : {
516 [ - - ]: 0 : Trace("strings-extf-list") << ", from " << n;
517 : : }
518 [ - - ]: 0 : Trace("strings-extf-list") << std::endl;
519 : : }
520 [ + + ][ + - ]: 654206 : if (d_extt.isActive(n) && einfo.d_modelActive)
[ + - ][ + + ]
[ - - ]
521 : : {
522 : 654054 : has_nreduce = true;
523 : : }
524 : : }
525 [ + + ]: 792293 : if (d_state.isInConflict())
526 : : {
527 [ + - ]: 450 : Trace("strings-extf-debug") << " conflict, return." << std::endl;
528 : 450 : return;
529 : : }
530 : : }
531 : 116494 : d_hasExtf = has_nreduce;
532 : : }
533 : :
534 : 653731 : void ExtfSolver::checkExtfInference(Node n,
535 : : Node nr,
536 : : ExtfInfoTmp& in,
537 : : int effort)
538 : : {
539 [ + + ]: 653731 : if (in.d_const.isNull())
540 : : {
541 : 521653 : return;
542 : : }
543 : 185491 : NodeManager* nm = nodeManager();
544 [ + - ]: 370982 : Trace("strings-extf-infer")
545 : 0 : << "checkExtfInference: " << n << " : " << nr << " == " << in.d_const
546 : 185491 : << " with exp " << in.d_exp << std::endl;
547 : :
548 : : // add original to explanation
549 [ + + ]: 185491 : if (n.getType().isBoolean())
550 : : {
551 : : // if Boolean, it's easy
552 [ + + ]: 101045 : in.d_exp.push_back(in.d_const.getConst<bool>() ? n : n.negate());
553 : : }
554 : : else
555 : : {
556 : : // otherwise, must explain via base node
557 : 168892 : Node r = d_state.getRepresentative(n);
558 : : // explain using the base solver
559 : 84446 : d_bsolver.explainConstantEqc(n, r, in.d_exp);
560 : : }
561 : :
562 : : // d_extfInferCache stores whether we have made the inferences associated
563 : : // with a node n,
564 : : // this may need to be generalized if multiple inferences apply
565 : :
566 [ + + ]: 185491 : if (nr.getKind() == Kind::STRING_CONTAINS)
567 : : {
568 [ - + ][ - + ]: 53413 : Assert(in.d_const.isConst());
[ - - ]
569 : 53413 : bool pol = in.d_const.getConst<bool>();
570 [ + + ][ + + ]: 74049 : if ((pol && nr[1].getKind() == Kind::STRING_CONCAT)
[ - - ]
571 [ + + ][ + + ]: 74049 : || (!pol && nr[0].getKind() == Kind::STRING_CONCAT))
[ + + ][ + + ]
[ + + ][ - - ]
572 : : {
573 : : // If str.contains( x, str.++( y1, ..., yn ) ),
574 : : // we may infer str.contains( x, y1 ), ..., str.contains( x, yn )
575 : : // The following recognizes two situations related to the above reasoning:
576 : : // (1) If ~str.contains( x, yi ) holds for some i, we are in conflict,
577 : : // (2) If str.contains( x, yj ) already holds for some j, then the term
578 : : // str.contains( x, yj ) is irrelevant since it is satisfied by all models
579 : : // for str.contains( x, str.++( y1, ..., yn ) ).
580 : :
581 : : // Notice that the dual of the above reasoning also holds, i.e.
582 : : // If ~str.contains( str.++( x1, ..., xn ), y ),
583 : : // we may infer ~str.contains( x1, y ), ..., ~str.contains( xn, y )
584 : : // This is also handled here.
585 [ + + ]: 3632 : if (d_extfInferCache.find(nr) == d_extfInferCache.end())
586 : : {
587 : 2464 : d_extfInferCache.insert(nr);
588 : :
589 [ + + ]: 2464 : int index = pol ? 1 : 0;
590 : 2464 : std::vector<Node> children;
591 : 2464 : children.push_back(nr[0]);
592 : 2464 : children.push_back(nr[1]);
593 [ + + ]: 7744 : for (const Node& nrc : nr[index])
594 : : {
595 : 5304 : children[index] = nrc;
596 : 5304 : Node conc = nm->mkNode(Kind::STRING_CONTAINS, children);
597 [ + + ]: 5304 : conc = rewrite(pol ? conc : conc.negate());
598 : : // check if it already (does not) hold
599 [ + + ]: 5304 : if (d_state.hasTerm(conc))
600 : : {
601 [ + + ]: 564 : if (d_state.areEqual(conc, d_false))
602 : : {
603 : : // we are in conflict
604 : 24 : d_im.addToExplanation(conc, d_false, in.d_exp);
605 : 24 : d_im.sendInference(
606 : 24 : in.d_exp, d_false, InferenceId::STRINGS_CTN_DECOMPOSE);
607 [ - + ][ - + ]: 24 : Assert(d_state.isInConflict());
[ - - ]
608 : 24 : return;
609 : : }
610 [ + + ]: 540 : else if (d_extt.hasFunctionKind(conc.getKind()))
611 : : {
612 : : // can mark as reduced, since model for n implies model for conc
613 : 240 : d_extt.markInactive(conc, ExtReducedId::STRINGS_CTN_DECOMPOSE);
614 : : }
615 : : }
616 : : }
617 : : }
618 : : }
619 : : else
620 : : {
621 : 99562 : if (std::find(d_extfInfoTmp[nr[0]].d_ctn[pol].begin(),
622 : 99562 : d_extfInfoTmp[nr[0]].d_ctn[pol].end(),
623 : 199124 : nr[1])
624 [ + + ]: 149343 : == d_extfInfoTmp[nr[0]].d_ctn[pol].end())
625 : : {
626 [ + - ][ - - ]: 98246 : Trace("strings-extf-debug") << " store contains info : " << nr[0]
627 [ - + ][ - + ]: 49123 : << " " << pol << " " << nr[1] << std::endl;
[ - - ]
628 : : // Store s (does not) contains t, since nr = (~)contains( s, t ) holds.
629 : 49123 : d_extfInfoTmp[nr[0]].d_ctn[pol].push_back(nr[1]);
630 : 49123 : d_extfInfoTmp[nr[0]].d_ctnFrom[pol].push_back(n);
631 : : // Do transistive closure on contains, e.g.
632 : : // if contains( s, t ) and ~contains( s, r ), then ~contains( t, r ).
633 : :
634 : : // The following infers new (negative) contains based on the above
635 : : // reasoning, provided that ~contains( t, r ) does not
636 : : // already hold in the current context. We test this by checking that
637 : : // contains( t, r ) is not already asserted false in the current
638 : : // context. We also handle the case where contains( t, r ) is equivalent
639 : : // to t = r, in which case we check that t != r does not already hold
640 : : // in the current context.
641 : :
642 : : // Notice that form of the above inference is enough to find
643 : : // conflicts purely due to contains predicates. For example, if we
644 : : // have only positive occurrences of contains, then no conflicts due to
645 : : // contains predicates are possible and this schema does nothing. For
646 : : // example, note that contains( s, t ) and contains( t, r ) implies
647 : : // contains( s, r ), which we could but choose not to infer. Instead,
648 : : // we prefer being lazy: only if ~contains( s, r ) appears later do we
649 : : // infer ~contains( t, r ), which suffices to show a conflict.
650 : 49123 : bool opol = !pol;
651 : 53874 : for (unsigned i = 0, size = d_extfInfoTmp[nr[0]].d_ctn[opol].size();
652 [ + + ]: 53874 : i < size;
653 : : i++)
654 : : {
655 : 9502 : Node onr = d_extfInfoTmp[nr[0]].d_ctn[opol][i];
656 : : Node concOrig = nm->mkNode(
657 [ + + ][ + + ]: 14253 : Kind::STRING_CONTAINS, pol ? nr[1] : onr, pol ? onr : nr[1]);
658 : 9502 : Node conc = rewrite(concOrig);
659 : : // For termination concerns, we only do the inference if the contains
660 : : // does not rewrite (and thus does not introduce new terms).
661 [ + + ]: 4751 : if (conc == concOrig)
662 : : {
663 : 82 : bool do_infer = false;
664 : 82 : conc = conc.negate();
665 : 82 : bool pol2 = conc.getKind() != Kind::NOT;
666 [ - + ]: 164 : Node lit = pol2 ? conc : conc[0];
667 [ - + ]: 82 : if (lit.getKind() == Kind::EQUAL)
668 : : {
669 : 0 : do_infer = pol2 ? !d_state.areEqual(lit[0], lit[1])
670 : 0 : : !d_state.areDisequal(lit[0], lit[1]);
671 : : }
672 : : else
673 : : {
674 [ - + ]: 82 : do_infer = !d_state.areEqual(lit, pol2 ? d_true : d_false);
675 : : }
676 [ + + ]: 82 : if (do_infer)
677 : : {
678 : 162 : std::vector<Node> exp_c;
679 : 81 : exp_c.insert(exp_c.end(), in.d_exp.begin(), in.d_exp.end());
680 : 81 : Node ofrom = d_extfInfoTmp[nr[0]].d_ctnFrom[opol][i];
681 [ - + ][ - + ]: 81 : Assert(d_extfInfoTmp.find(ofrom) != d_extfInfoTmp.end());
[ - - ]
682 : 81 : exp_c.insert(exp_c.end(),
683 : 81 : d_extfInfoTmp[ofrom].d_exp.begin(),
684 : 243 : d_extfInfoTmp[ofrom].d_exp.end());
685 : 81 : d_im.sendInference(exp_c, conc, InferenceId::STRINGS_CTN_TRANS);
686 : : }
687 : : }
688 : : }
689 : : }
690 : : else
691 : : {
692 : : // If we already know that s (does not) contain t, then n may be
693 : : // redundant. However, we do not mark n as reduced here, since strings
694 : : // reductions may require dependencies between extended functions.
695 : : // Marking reduced here could lead to incorrect models if an
696 : : // extended function is marked reduced based on an assignment to
697 : : // something that depends on n.
698 [ + - ]: 658 : Trace("strings-extf-debug") << " redundant." << std::endl;
699 : : }
700 : : }
701 : 53389 : return;
702 : : }
703 : :
704 : : // If it's not a predicate, see if we can solve the equality n = c, where c
705 : : // is the constant that extended term n is equal to.
706 : 264156 : Node inferEq = nr.eqNode(in.d_const);
707 : 264156 : Node inferEqr = rewrite(inferEq);
708 : 264156 : Node inferEqrr = inferEqr;
709 [ + + ]: 132078 : if (inferEqr.getKind() == Kind::EQUAL)
710 : : {
711 : : // try to use the extended rewriter for equalities
712 : 85419 : inferEqrr = d_rewriter.rewriteEqualityExt(inferEqr);
713 : : }
714 [ + + ]: 132078 : if (inferEqrr != inferEqr)
715 : : {
716 : 8411 : inferEqrr = rewrite(inferEqrr);
717 [ + - ]: 16822 : Trace("strings-extf-infer")
718 : 0 : << "checkExtfInference: " << inferEq << " ...reduces to " << inferEqrr
719 : 8411 : << " with explanation " << in.d_exp << std::endl;
720 : 8411 : d_im.sendInternalInference(in.d_exp, inferEqrr, InferenceId::STRINGS_EXTF_EQ_REW);
721 : : }
722 : : }
723 : :
724 : 1772380 : Node ExtfSolver::getCurrentSubstitutionFor(int effort,
725 : : Node n,
726 : : std::vector<Node>& exp)
727 : : {
728 [ + + ]: 1772380 : if (effort >= 3)
729 : : {
730 : : // model values
731 : 32570 : Node mv = d_state.getModel()->getRepresentative(n);
732 [ + - ]: 16285 : Trace("strings-subs") << " model val : " << mv << std::endl;
733 : 16285 : return mv;
734 : : }
735 : 5268300 : Node nr = d_state.getRepresentative(n);
736 : : // if the normal form is available, use it
737 [ + + ][ + + ]: 1756100 : if (effort >= 1 && n.getType().isStringLike())
[ + + ][ + + ]
[ - - ]
738 : : {
739 [ - + ][ - + ]: 122697 : Assert(effort < 3);
[ - - ]
740 : : // Return self if the normal form has not been computed. This may happen
741 : : // for terms that are not relevant in the current context.
742 [ + + ]: 122697 : if (!d_csolver.hasNormalForm(nr))
743 : : {
744 : 2 : return n;
745 : : }
746 : 122695 : NormalForm& nfnr = d_csolver.getNormalForm(nr);
747 : 245390 : Node ns = d_csolver.getNormalString(nfnr.d_base, exp);
748 [ + - ]: 245390 : Trace("strings-subs") << " normal eqc : " << ns << " " << nfnr.d_base
749 : 122695 : << " " << nr << std::endl;
750 [ + - ]: 122695 : if (!nfnr.d_base.isNull())
751 : : {
752 : 122695 : d_im.addToExplanation(n, nfnr.d_base, exp);
753 : : }
754 : 122695 : return ns;
755 : : }
756 : : // otherwise, we use the best content heuristic
757 : 4900210 : Node c = d_bsolver.explainBestContentEqc(n, nr, exp);
758 [ + + ]: 1633400 : if (!c.isNull())
759 : : {
760 : 856057 : return c;
761 : : }
762 : 777346 : return n;
763 : : }
764 : :
765 : 0 : const std::map<Node, ExtfInfoTmp>& ExtfSolver::getInfo() const
766 : : {
767 : 0 : return d_extfInfoTmp;
768 : : }
769 : 24994 : bool ExtfSolver::hasExtendedFunctions() const { return d_hasExtf.get(); }
770 : :
771 : 32829 : std::vector<Node> ExtfSolver::getActive(Kind k) const
772 : : {
773 : 32829 : return d_extt.getActive(k);
774 : : }
775 : :
776 : 415244 : bool ExtfSolver::isActiveInModel(Node n) const
777 : : {
778 : 415244 : std::map<Node, ExtfInfoTmp>::const_iterator it = d_extfInfoTmp.find(n);
779 [ - + ]: 415244 : if (it == d_extfInfoTmp.end())
780 : : {
781 : 0 : Assert(false) << "isActiveInModel: Expected extf info for " << n;
782 : : return true;
783 : : }
784 : 415244 : return it->second.d_modelActive;
785 : : }
786 : :
787 : 95125 : std::vector<Node> ExtfSolver::getRelevantActive() const
788 : : {
789 : : // get the relevant term set
790 : 190250 : std::vector<Node> extf = d_extt.getActive();
791 : 95125 : const std::set<Node>& relevantTerms = d_termReg.getRelevantTermSet();
792 : :
793 : 95125 : std::vector<Node> res;
794 [ + + ]: 535605 : for (const Node& n : extf)
795 : : {
796 [ + + ]: 440480 : if (relevantTerms.find(n) == relevantTerms.end())
797 : : {
798 : : // not relevant
799 : 7932 : continue;
800 : : }
801 : 432548 : res.push_back(n);
802 : : }
803 : 190250 : return res;
804 : : }
805 : :
806 : 0 : bool StringsExtfCallback::getCurrentSubstitution(
807 : : int effort,
808 : : const std::vector<Node>& vars,
809 : : std::vector<Node>& subs,
810 : : std::map<Node, std::vector<Node> >& exp)
811 : : {
812 [ - - ]: 0 : Trace("strings-subs") << "getCurrentSubstitution, effort = " << effort
813 : 0 : << std::endl;
814 [ - - ]: 0 : for (const Node& v : vars)
815 : : {
816 [ - - ]: 0 : Trace("strings-subs") << " get subs for " << v << "..." << std::endl;
817 : 0 : Node s = d_esolver->getCurrentSubstitutionFor(effort, v, exp[v]);
818 : 0 : subs.push_back(s);
819 : : }
820 : 0 : return true;
821 : : }
822 : :
823 : 0 : void ExtfSolver::processFact(InferInfo& ii, ProofGenerator*& pg)
824 : : {
825 : : // process it with the inference manager
826 : 0 : d_im.processFact(ii, pg);
827 : 0 : }
828 : :
829 : 4516 : TrustNode ExtfSolver::processLemma(InferInfo& ii, LemmaProperty& p)
830 : : {
831 : : // if this was the reduction lemma for a term, mark it reduced now
832 : 4516 : std::map<Node, Node>::iterator it = d_reductionWaitingMap.find(ii.d_conc);
833 [ + - ]: 4516 : if (it != d_reductionWaitingMap.end())
834 : : {
835 : 4516 : d_reduced.insert(it->second);
836 : 4516 : d_reductionWaitingMap.erase(it);
837 : : }
838 : : // now process it with the inference manager
839 : 9032 : return d_im.processLemma(ii, p);
840 : : }
841 : :
842 : 0 : std::string ExtfSolver::debugPrintModel()
843 : : {
844 : 0 : std::stringstream ss;
845 : 0 : std::vector<Node> extf;
846 : 0 : d_extt.getTerms(extf);
847 : : // each extended function should have at least one annotation below
848 [ - - ]: 0 : for (const Node& n : extf)
849 : : {
850 : 0 : ss << "- " << n;
851 : : ExtReducedId id;
852 [ - - ]: 0 : if (!d_extt.isActive(n, id))
853 : : {
854 : 0 : ss << " :extt-inactive " << id;
855 : : }
856 [ - - ]: 0 : if (!d_extfInfoTmp[n].d_modelActive)
857 : : {
858 : 0 : ss << " :model-inactive";
859 : : }
860 [ - - ]: 0 : if (d_reduced.find(n) != d_reduced.end())
861 : : {
862 : 0 : ss << " :reduced";
863 : : }
864 : 0 : ss << std::endl;
865 : : }
866 : 0 : return ss.str();
867 : : }
868 : :
869 : 3955 : bool ExtfSolver::isReduced(const Node& n) const
870 : : {
871 : 3955 : return d_reduced.find(n) != d_reduced.end();
872 : : }
873 : :
874 : 962 : void ExtfSolver::markReduced(const Node& n) { d_reduced.insert(n); }
875 : :
876 : : } // namespace strings
877 : : } // namespace theory
878 : : } // namespace cvc5::internal
|
