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