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 : 51092 : 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 : 51092 : SequencesStatistics& statistics)
39 : : : EnvObj(env),
40 : 51092 : d_state(s),
41 : 51092 : d_im(im),
42 : 51092 : d_termReg(tr),
43 : 51092 : d_rewriter(rewriter),
44 : 51092 : d_bsolver(bs),
45 : 51092 : d_csolver(cs),
46 : 51092 : d_extt(et),
47 : 51092 : d_statistics(statistics),
48 : 51092 : d_preproc(env, d_termReg.getSkolemCache(), &statistics.d_reductions),
49 : 51092 : d_hasExtf(context(), false),
50 : 51092 : d_extfInferCache(context()),
51 : 153276 : d_reduced(userContext())
52 : : {
53 : 51092 : d_extt.addFunctionKind(Kind::STRING_SUBSTR);
54 : 51092 : d_extt.addFunctionKind(Kind::STRING_UPDATE);
55 : 51092 : d_extt.addFunctionKind(Kind::STRING_INDEXOF);
56 : 51092 : d_extt.addFunctionKind(Kind::STRING_INDEXOF_RE);
57 : 51092 : d_extt.addFunctionKind(Kind::STRING_ITOS);
58 : 51092 : d_extt.addFunctionKind(Kind::STRING_STOI);
59 : 51092 : d_extt.addFunctionKind(Kind::STRING_REPLACE);
60 : 51092 : d_extt.addFunctionKind(Kind::STRING_REPLACE_ALL);
61 : 51092 : d_extt.addFunctionKind(Kind::STRING_REPLACE_RE);
62 : 51092 : d_extt.addFunctionKind(Kind::STRING_REPLACE_RE_ALL);
63 : 51092 : d_extt.addFunctionKind(Kind::STRING_CONTAINS);
64 : 51092 : d_extt.addFunctionKind(Kind::STRING_IN_REGEXP);
65 : 51092 : d_extt.addFunctionKind(Kind::STRING_LEQ);
66 : 51092 : d_extt.addFunctionKind(Kind::STRING_TO_CODE);
67 : 51092 : d_extt.addFunctionKind(Kind::STRING_TO_LOWER);
68 : 51092 : d_extt.addFunctionKind(Kind::STRING_TO_UPPER);
69 : 51092 : d_extt.addFunctionKind(Kind::STRING_REV);
70 : 51092 : d_extt.addFunctionKind(Kind::STRING_UNIT);
71 : 51092 : d_extt.addFunctionKind(Kind::SEQ_UNIT);
72 : 51092 : d_extt.addFunctionKind(Kind::SEQ_NTH);
73 : :
74 : 51092 : d_true = nodeManager()->mkConst(true);
75 : 51092 : d_false = nodeManager()->mkConst(false);
76 : 51092 : }
77 : :
78 : 50744 : ExtfSolver::~ExtfSolver() {}
79 : :
80 : 452070 : bool ExtfSolver::shouldDoReduction(int effort, Node n, int pol)
81 : : {
82 [ + - ]: 904140 : Trace("strings-extf-debug") << "shouldDoReduction " << n << ", pol " << pol
83 : 452070 : << ", effort " << effort << std::endl;
84 [ + + ]: 452070 : if (!isActiveInModel(n))
85 : : {
86 : : // n is not active in the model, no need to reduce
87 [ + - ]: 2297 : Trace("strings-extf-debug") << "...skip due to model active" << std::endl;
88 : 2297 : return false;
89 : : }
90 : : // check with negation if requested (only applied to Boolean terms)
91 : 449773 : Assert(n.getType().isBoolean() || pol != -1);
92 [ + + ]: 449773 : Node nn = pol == -1 ? n.notNode() : n;
93 [ + + ]: 449773 : if (d_reduced.find(nn) != d_reduced.end())
94 : : {
95 : : // already sent a reduction lemma
96 [ + - ]: 264675 : Trace("strings-extf-debug") << "...skip due to reduced" << std::endl;
97 : 264675 : return false;
98 : : }
99 : 185098 : Kind k = n.getKind();
100 : : // determine if it is the right effort
101 [ + + ][ + + ]: 185098 : if (k == Kind::STRING_SUBSTR || (k == Kind::STRING_CONTAINS && pol == 1))
[ + + ]
102 : : {
103 : : // we reduce these semi-eagerly, at effort 1
104 : 3255 : return (effort == 1);
105 : : }
106 [ + + ][ + - ]: 181843 : else if (k == Kind::STRING_CONTAINS && pol == -1)
107 : : {
108 : : // negative contains reduces at level 2, or 3 if guessing model
109 [ + - ]: 27612 : int reffort = options().strings.stringModelBasedReduction ? 3 : 2;
110 : 27612 : return (effort == reffort);
111 : : }
112 [ + - ]: 149986 : else if (k == Kind::SEQ_UNIT || k == Kind::STRING_UNIT
113 [ + + ][ + + ]: 149986 : || k == Kind::STRING_IN_REGEXP || k == Kind::STRING_TO_CODE
114 [ + + ][ + + ]: 304217 : || (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 : 119461 : return false;
120 : : }
121 [ + + ]: 34770 : 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 : 27381 : return (effort == 2);
138 : 449773 : }
139 : :
140 : 5169 : void ExtfSolver::doReduction(Node n, int pol)
141 : : {
142 [ + - ]: 10338 : Trace("strings-extf-debug")
143 : 5169 : << "doReduction " << n << ", pol " << pol << std::endl;
144 : : // polarity : 1 true, -1 false, 0 neither
145 : 5169 : Kind k = n.getKind();
146 [ + + ][ + + ]: 5169 : 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 [ + + ]: 5169 : Node nn = pol == -1 ? n.notNode() : n;
176 [ + - ]: 10338 : Trace("strings-process-debug")
177 : 5169 : << "Process reduction for " << n << ", pol = " << pol << std::endl;
178 [ + + ][ + + ]: 5169 : if (k == Kind::STRING_CONTAINS && pol == 1)
179 : : {
180 : 496 : Node x = n[0];
181 : 496 : Node s = n[1];
182 : : // positive contains reduces to a equality
183 : 496 : SkolemCache* skc = d_termReg.getSkolemCache();
184 : 496 : Node eq = d_termReg.eagerReduce(n, skc, d_termReg.getAlphabetCardinality());
185 [ - + ][ - + ]: 496 : Assert(!eq.isNull());
[ - - ]
186 : 496 : Assert(eq.getKind() == Kind::ITE && eq[0] == n);
187 : 496 : eq = eq[1];
188 : 496 : std::vector<Node> expn;
189 : 496 : expn.push_back(n);
190 : 496 : d_im.sendInference(
191 : : expn, expn, eq, InferenceId::STRINGS_CTN_POS, false, true);
192 [ + - ]: 992 : Trace("strings-extf-debug")
193 : 0 : << " resolve extf : " << n << " based on positive contain reduction."
194 : 496 : << std::endl;
195 [ + - ]: 992 : Trace("strings-red-lemma") << "Reduction (positive contains) lemma : " << n
196 : 496 : << " => " << eq << std::endl;
197 : : // reduced positively
198 [ - + ][ - + ]: 496 : Assert(nn == n);
[ - - ]
199 : 496 : d_reduced.insert(nn);
200 : 496 : }
201 : : else
202 : : {
203 : 4673 : NodeManager* nm = nodeManager();
204 [ + + ][ + + ]: 4673 : Assert(k == Kind::STRING_SUBSTR || k == Kind::STRING_UPDATE
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + - ]
[ - + ][ - + ]
[ - - ]
205 : : || k == Kind::STRING_CONTAINS || k == Kind::STRING_INDEXOF
206 : : || k == Kind::STRING_INDEXOF_RE || k == Kind::STRING_ITOS
207 : : || k == Kind::STRING_STOI || k == Kind::STRING_REPLACE
208 : : || k == Kind::STRING_REPLACE_ALL || k == Kind::SEQ_NTH
209 : : || k == Kind::STRING_REPLACE_RE || k == Kind::STRING_REPLACE_RE_ALL
210 : : || k == Kind::STRING_LEQ || k == Kind::STRING_TO_LOWER
211 : : || k == Kind::STRING_TO_UPPER || k == Kind::STRING_REV)
212 : 0 : << "Unknown reduction: " << k;
213 : 4673 : std::vector<Node> new_nodes;
214 : 4673 : Node res = d_preproc.simplify(n, new_nodes);
215 [ - + ][ - + ]: 4673 : Assert(res != n);
[ - - ]
216 : 4673 : new_nodes.push_back(n.eqNode(res));
217 : : Node nnlem =
218 [ - + ]: 4673 : new_nodes.size() == 1 ? new_nodes[0] : nm->mkNode(Kind::AND, new_nodes);
219 : : // in rare case where it rewrites to true, just record it is reduced
220 [ - + ]: 4673 : if (rewrite(nnlem) == d_true)
221 : : {
222 [ - - ]: 0 : Trace("strings-extf-debug")
223 : 0 : << " resolve extf : " << n << " based on (trivial) reduction."
224 : 0 : << std::endl;
225 : 0 : d_reduced.insert(nn);
226 : : }
227 : : else
228 : : {
229 : 4673 : InferInfo ii(InferenceId::STRINGS_REDUCTION);
230 : : // ensure that we are called to process the side effects
231 : 4673 : ii.d_sim = this;
232 : 4673 : ii.d_conc = nnlem;
233 : 4673 : d_im.sendInference(ii, true);
234 [ + - ]: 9346 : Trace("strings-extf-debug")
235 : 4673 : << " resolve extf : " << n << " based on reduction." << std::endl;
236 : 4673 : d_reductionWaitingMap[nnlem] = nn;
237 : 4673 : }
238 : 4673 : }
239 : 5169 : }
240 : :
241 : 68628 : void ExtfSolver::checkExtfReductionsEager()
242 : : {
243 : : // return value is ignored
244 : 68628 : checkExtfReductionsInternal(1);
245 : 68628 : }
246 : :
247 : 39891 : void ExtfSolver::checkExtfReductions(Theory::Effort e)
248 : : {
249 [ + + ]: 39891 : int effort = e == Theory::EFFORT_LAST_CALL ? 3 : 2;
250 : : // return value is ignored
251 : 39891 : checkExtfReductionsInternal(effort);
252 : 39891 : }
253 : :
254 : 108519 : bool ExtfSolver::checkExtfReductionsInternal(int effort)
255 : : {
256 : : // Notice we don't make a standard call to ExtTheory::doReductions here,
257 : : // since certain optimizations like context-dependent reductions and
258 : : // stratifying effort levels are done in doReduction below.
259 : : // We only have to reduce extended functions that are both relevant and
260 : : // active (see getRelevantActive).
261 : 108519 : std::vector<Node> extf = getRelevantActive();
262 [ + - ]: 217038 : Trace("strings-process") << " checking " << extf.size() << " active extf"
263 : 108519 : << std::endl;
264 [ + + ]: 555420 : for (const Node& n : extf)
265 : : {
266 [ - + ][ - + ]: 452070 : Assert(!d_state.isInConflict());
[ - - ]
267 [ + - ]: 904140 : Trace("strings-extf-debug")
268 : 0 : << " check " << n
269 : 452070 : << ", active in model=" << d_extfInfoTmp[n].d_modelActive << std::endl;
270 : : // polarity, 1: positive, -1: negative, 0: neither
271 : 452070 : int pol = 0;
272 [ + + ]: 452070 : if (n.getType().isBoolean())
273 : : {
274 : 139874 : Node rep = d_state.getRepresentative(n);
275 [ + - ]: 69937 : if (rep.isConst())
276 : : {
277 [ + + ]: 69937 : pol = rep.getConst<bool>() ? 1 : -1;
278 : : }
279 : 69937 : }
280 [ + + ]: 452070 : if (shouldDoReduction(effort, n, pol))
281 : : {
282 : 5169 : doReduction(n, pol);
283 : : // we do not mark as inactive, since we may want to evaluate
284 [ + - ]: 5169 : if (d_im.hasProcessed())
285 : : {
286 : 5169 : return true;
287 : : }
288 : : }
289 : : }
290 : 103350 : return false;
291 : 108519 : }
292 : :
293 : 133365 : void ExtfSolver::checkExtfEval(int effort)
294 : : {
295 [ + - ]: 266730 : Trace("strings-extf-list")
296 : 133365 : << "Active extended functions, effort=" << effort << " : " << std::endl;
297 : 133365 : d_extfInfoTmp.clear();
298 : 133365 : d_extfToOrig.clear();
299 : 133365 : NodeManager* nm = nodeManager();
300 : 133365 : bool has_nreduce = false;
301 : 133365 : std::vector<Node> terms = d_extt.getActive();
302 : : // the set of terms we have done extf inferences for
303 : 133365 : std::unordered_set<Node> inferProcessed;
304 [ + + ]: 1004874 : for (const Node& n : terms)
305 : : {
306 : : // Setup information about n, including if it is equal to a constant.
307 : 872374 : ExtfInfoTmp& einfo = d_extfInfoTmp[n];
308 [ - + ][ - + ]: 872374 : Assert(einfo.d_exp.empty());
[ - - ]
309 : 1744748 : Node r = d_state.getRepresentative(n);
310 : 872374 : einfo.d_const = d_bsolver.getConstantEqc(r);
311 : : // Get the current values of the children of n.
312 : : // Notice that we look up the value of the direct children of n, and not
313 : : // their free variables. In other words, given a term:
314 : : // t = (str.replace "B" (str.replace x "A" "B") "C")
315 : : // we may build the explanation that:
316 : : // ((str.replace x "A" "B") = "B") => t = (str.replace "B" "B" "C")
317 : : // instead of basing this on the free variable x:
318 : : // (x = "A") => t = (str.replace "B" (str.replace "A" "A" "B") "C")
319 : : // Although both allow us to infer t = "C", it is important to use the
320 : : // first kind of inference since it ensures that its subterms have the
321 : : // expected values. Otherwise, we may in rare cases fail to realize that
322 : : // the subterm (str.replace x "A" "B") does not currently have the correct
323 : : // value, say in this example that (str.replace x "A" "B") != "B".
324 : 872374 : std::vector<Node> exp;
325 : 872374 : std::vector<Node> schildren;
326 : : // seq.unit is parameterized
327 [ - + ]: 872374 : if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
328 : : {
329 : 0 : schildren.push_back(n.getOperator());
330 : : }
331 : 872374 : bool schanged = false;
332 [ + + ]: 2869986 : for (const Node& nc : n)
333 : : {
334 : 1997612 : Node sc = getCurrentSubstitutionFor(effort, nc, exp);
335 : 1997612 : schildren.push_back(sc);
336 [ + + ][ + + ]: 1997612 : schanged = schanged || sc != nc;
337 : 1997612 : }
338 : : // If there is information involving the children, attempt to do an
339 : : // inference and/or mark n as reduced.
340 : 872374 : bool reduced = false;
341 : 872374 : Node to_reduce = n;
342 [ + + ]: 872374 : if (schanged)
343 : : {
344 : 337024 : Node sn = nm->mkNode(n.getKind(), schildren);
345 [ + - ]: 674048 : Trace("strings-extf-debug")
346 : 0 : << "Check extf " << n << " == " << sn
347 : 0 : << ", constant = " << einfo.d_const << ", effort=" << effort
348 : 337024 : << ", exp " << exp << std::endl;
349 : 337024 : einfo.d_initExp.insert(einfo.d_initExp.end(), exp.begin(), exp.end());
350 : 337024 : einfo.d_exp.insert(einfo.d_exp.end(), exp.begin(), exp.end());
351 : : // inference is rewriting the substituted node
352 : 337024 : Node nrc = rewrite(sn);
353 : : // if rewrites to a constant, then do the inference and mark as reduced
354 [ + + ]: 337024 : 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 [ + + ]: 149669 : if (effort < 3)
360 : : {
361 : 142836 : d_extt.markInactive(n, ExtReducedId::STRINGS_SR_CONST);
362 [ + - ]: 285672 : Trace("strings-extf-debug")
363 : 142836 : << " resolvable by evaluation..." << std::endl;
364 : 142836 : 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 [ + - ]: 285672 : Trace("strings-extf-debug")
379 : 142836 : << " get symbolic definition..." << std::endl;
380 : 142836 : Node nrs;
381 : : // only use symbolic definitions if option is set
382 [ + - ]: 142836 : if (options().strings.stringInferSym)
383 : : {
384 : 142836 : nrs = d_termReg.getSymbolicDefinition(sn, exps);
385 : : }
386 [ + + ]: 142836 : if (!nrs.isNull())
387 : : {
388 [ + - ]: 206862 : Trace("strings-extf-debug")
389 : 103431 : << " rewrite " << nrs << "..." << std::endl;
390 : 103431 : Node nrsr = rewrite(nrs);
391 : : // ensure the symbolic form is not rewritable
392 [ + + ]: 103431 : if (nrsr != nrs)
393 : : {
394 : : // we cannot use the symbolic definition if it rewrites
395 [ + - ]: 12800 : Trace("strings-extf-debug")
396 : 6400 : << " symbolic definition is trivial..." << std::endl;
397 : 6400 : nrs = Node::null();
398 : : }
399 : 103431 : }
400 : : else
401 : : {
402 [ + - ]: 78810 : Trace("strings-extf-debug")
403 : 39405 : << " could not infer symbolic definition." << std::endl;
404 : : }
405 : 142836 : Node conc;
406 [ + + ]: 142836 : if (!nrs.isNull())
407 : : {
408 [ + - ]: 194062 : Trace("strings-extf-debug")
409 : 97031 : << " symbolic def : " << nrs << std::endl;
410 [ + + ]: 97031 : if (!d_state.areEqual(nrs, nrc))
411 : : {
412 : : // infer symbolic unit
413 [ + + ]: 2857 : if (n.getType().isBoolean())
414 : : {
415 [ + + ]: 1887 : conc = nrc == d_true ? nrs : nrs.negate();
416 : : }
417 : : else
418 : : {
419 : 970 : conc = nrs.eqNode(nrc);
420 : : }
421 : 2857 : einfo.d_exp.clear();
422 : : }
423 : : }
424 : : else
425 : : {
426 [ + + ]: 45805 : if (!d_state.areEqual(n, nrc))
427 : : {
428 [ + + ]: 5281 : if (n.getType().isBoolean())
429 : : {
430 [ + + ]: 3149 : conc = nrc == d_true ? n : n.negate();
431 : : }
432 : : else
433 : : {
434 : 2132 : conc = n.eqNode(nrc);
435 : : }
436 : : }
437 : : }
438 [ + + ]: 142836 : if (!conc.isNull())
439 : : {
440 [ + - ]: 16276 : Trace("strings-extf")
441 : 8138 : << " resolve extf : " << sn << " -> " << nrc << std::endl;
442 [ + + ]: 8138 : InferenceId inf = effort == 0 ? InferenceId::STRINGS_EXTF
443 : : : InferenceId::STRINGS_EXTF_N;
444 : 8138 : d_im.sendInference(einfo.d_exp, conc, inf, false, true);
445 : 8138 : d_statistics.d_cdSimplifications << n.getKind();
446 : : }
447 : 142836 : }
448 : : else
449 : : {
450 : : // check if it is already equal, if so, mark as reduced. Otherwise, do
451 : : // nothing.
452 [ + + ]: 6833 : if (d_state.areEqual(n, nrc))
453 : : {
454 [ + - ]: 4648 : Trace("strings-extf")
455 : 0 : << " resolved extf, since satisfied by model: " << n
456 : 2324 : << std::endl;
457 : 2324 : einfo.d_modelActive = false;
458 : : }
459 : : }
460 : 149669 : reduced = true;
461 : : }
462 [ + + ]: 187355 : else if (effort < 3)
463 : : {
464 : : // if this was a predicate which changed after substitution + rewriting
465 : : // We only do this before models are constructed (effort<3)
466 [ + + ][ + + ]: 186905 : if (!einfo.d_const.isNull() && nrc.getType().isBoolean() && nrc != n)
[ + + ][ + + ]
[ + + ][ - - ]
467 : : {
468 : 28027 : bool pol = einfo.d_const == d_true;
469 [ + + ]: 28027 : Node nrcAssert = pol ? nrc : nrc.negate();
470 [ + + ]: 28027 : Node nAssert = pol ? n : n.negate();
471 : 28027 : einfo.d_exp.push_back(nAssert);
472 [ + - ]: 28027 : Trace("strings-extf-debug") << " decomposable..." << std::endl;
473 [ + - ]: 56054 : Trace("strings-extf") << " resolve extf : " << sn << " -> " << nrc
474 : 28027 : << ", const = " << einfo.d_const << std::endl;
475 : : // We send inferences internal here, which may help show unsat.
476 : : // However, we do not make a determination whether n can be marked
477 : : // reduced since this argument may be circular: we may infer than n
478 : : // can be reduced to something else, but that thing may argue that it
479 : : // can be reduced to n, in theory.
480 [ + + ]: 28027 : InferenceId infer = effort == 0 ? InferenceId::STRINGS_EXTF_D
481 : : : InferenceId::STRINGS_EXTF_D_N;
482 : 28027 : d_im.sendInternalInference(einfo.d_exp, nrcAssert, infer);
483 : 28027 : }
484 : 186905 : to_reduce = nrc;
485 : : }
486 : 337024 : }
487 : : // We must use the original n here to avoid circular justifications for
488 : : // why extended functions are reduced. In particular, n should never be a
489 : : // duplicate of another term considered in the block of code for
490 : : // checkExtfInference below.
491 : : // if not reduced and not processed
492 [ + - ]: 722705 : if (!reduced && !n.isNull()
493 [ + + ][ + - ]: 1595079 : && inferProcessed.find(n) == inferProcessed.end())
[ + + ]
494 : : {
495 : 722705 : inferProcessed.insert(n);
496 [ + + ]: 722705 : if (effort == 1)
497 : : {
498 [ + - ]: 183106 : Trace("strings-extf")
499 : 91553 : << " cannot rewrite extf : " << to_reduce << std::endl;
500 : : }
501 : : // we take to_reduce to be the (partially) reduced version of n, which
502 : : // is justified by the explanation in einfo. We only do this if we are
503 : : // not based on the model (effort<3).
504 [ + + ]: 722705 : if (effort < 3)
505 : : {
506 : 722241 : checkExtfInference(n, to_reduce, einfo);
507 : : }
508 [ - + ]: 722705 : if (TraceIsOn("strings-extf-list"))
509 : : {
510 [ - - ]: 0 : Trace("strings-extf-list") << " * " << to_reduce;
511 [ - - ]: 0 : if (!einfo.d_const.isNull())
512 : : {
513 [ - - ]: 0 : Trace("strings-extf-list") << ", const = " << einfo.d_const;
514 : : }
515 [ - - ]: 0 : if (n != to_reduce)
516 : : {
517 [ - - ]: 0 : Trace("strings-extf-list") << ", from " << n;
518 : : }
519 [ - - ]: 0 : Trace("strings-extf-list") << std::endl;
520 : : }
521 [ + + ][ + - ]: 722705 : if (d_extt.isActive(n) && einfo.d_modelActive)
[ + - ][ + + ]
[ - - ]
522 : : {
523 : 722572 : has_nreduce = true;
524 : : }
525 : : }
526 [ + + ]: 872374 : if (d_state.isInConflict())
527 : : {
528 [ + - ]: 865 : Trace("strings-extf-debug") << " conflict, return." << std::endl;
529 : 865 : return;
530 : : }
531 [ + + ][ + + ]: 874969 : }
[ + + ][ + + ]
532 : 132500 : d_hasExtf = has_nreduce;
533 [ + + ][ + + ]: 134230 : }
534 : :
535 : 722241 : void ExtfSolver::checkExtfInference(Node n, Node nr, ExtfInfoTmp& in)
536 : : {
537 : : // see if any previous term rewrote to nr, if so, we can conclude that
538 : : // term is equal to n.
539 : 722241 : std::map<Node, Node>::iterator ito = d_extfToOrig.find(nr);
540 [ + + ]: 722241 : if (ito != d_extfToOrig.end())
541 : : {
542 : 18408 : Node no = ito->second;
543 [ + + ]: 18408 : if (!d_state.areEqual(n, no))
544 : : {
545 [ - + ][ - + ]: 720 : Assert(d_extfInfoTmp.find(no) != d_extfInfoTmp.end());
[ - - ]
546 : 720 : ExtfInfoTmp& eito = d_extfInfoTmp[no];
547 : 720 : Node conc = n.eqNode(no);
548 [ + - ]: 1440 : Trace("strings-extf-infer")
549 : 720 : << "infer same rewrite: " << conc << std::endl;
550 : 720 : std::vector<Node> exp;
551 : 720 : exp.insert(exp.end(), in.d_initExp.begin(), in.d_initExp.end());
552 : 720 : exp.insert(exp.end(), eito.d_initExp.begin(), eito.d_initExp.end());
553 [ + - ]: 720 : Trace("strings-extf-infer") << "..explaination is " << exp << std::endl;
554 : 720 : d_im.sendInference(exp, conc, InferenceId::STRINGS_EXTF_REW_SAME);
555 : 720 : }
556 : 18408 : return;
557 : 18408 : }
558 : : // store that n rewrites to nr
559 : 703833 : d_extfToOrig[nr] = n;
560 : :
561 [ + + ]: 703833 : if (in.d_const.isNull())
562 : : {
563 : 486007 : return;
564 : : }
565 : 217826 : NodeManager* nm = nodeManager();
566 [ + - ]: 435652 : Trace("strings-extf-infer")
567 : 0 : << "checkExtfInference: " << n << " : " << nr << " == " << in.d_const
568 : 217826 : << " with exp " << in.d_exp << std::endl;
569 : :
570 : : // add original to explanation
571 [ + + ]: 217826 : if (n.getType().isBoolean())
572 : : {
573 : : // if Boolean, it's easy
574 [ + + ]: 110708 : in.d_exp.push_back(in.d_const.getConst<bool>() ? n : n.negate());
575 : : }
576 : : else
577 : : {
578 : : // otherwise, must explain via base node
579 : 214236 : Node r = d_state.getRepresentative(n);
580 : : // explain using the base solver
581 : 107118 : d_bsolver.explainConstantEqc(n, r, in.d_exp);
582 : 107118 : }
583 : :
584 : : // d_extfInferCache stores whether we have made the inferences associated
585 : : // with a node n,
586 : : // this may need to be generalized if multiple inferences apply
587 : :
588 [ + + ]: 217826 : if (nr.getKind() == Kind::STRING_CONTAINS)
589 : : {
590 [ - + ][ - + ]: 66579 : Assert(in.d_const.isConst());
[ - - ]
591 : 66579 : bool pol = in.d_const.getConst<bool>();
592 [ + + ][ + + ]: 91863 : if ((pol && nr[1].getKind() == Kind::STRING_CONCAT)
[ - - ]
593 [ + + ][ + + ]: 91863 : || (!pol && nr[0].getKind() == Kind::STRING_CONCAT))
[ + + ][ + + ]
[ + + ][ - - ]
594 : : {
595 : : // If str.contains( x, str.++( y1, ..., yn ) ),
596 : : // we may infer str.contains( x, y1 ), ..., str.contains( x, yn )
597 : : // The following recognizes two situations related to the above reasoning:
598 : : // (1) If ~str.contains( x, yi ) holds for some i, we are in conflict,
599 : : // (2) If str.contains( x, yj ) already holds for some j, then the term
600 : : // str.contains( x, yj ) is irrelevant since it is satisfied by all models
601 : : // for str.contains( x, str.++( y1, ..., yn ) ).
602 : :
603 : : // Notice that the dual of the above reasoning also holds, i.e.
604 : : // If ~str.contains( str.++( x1, ..., xn ), y ),
605 : : // we may infer ~str.contains( x1, y ), ..., ~str.contains( xn, y )
606 : : // This is also handled here.
607 [ + + ]: 5640 : if (d_extfInferCache.find(nr) == d_extfInferCache.end())
608 : : {
609 : 3394 : d_extfInferCache.insert(nr);
610 : :
611 [ + + ]: 3394 : int index = pol ? 1 : 0;
612 : 3394 : std::vector<Node> children;
613 : 3394 : children.push_back(nr[0]);
614 : 3394 : children.push_back(nr[1]);
615 [ + + ]: 10575 : for (const Node& nrc : nr[index])
616 : : {
617 : 7202 : children[index] = nrc;
618 : 7202 : Node conc = nm->mkNode(Kind::STRING_CONTAINS, children);
619 [ + + ]: 7202 : conc = rewrite(pol ? conc : conc.negate());
620 : : // check if it already (does not) hold
621 [ + + ]: 7202 : if (d_state.hasTerm(conc))
622 : : {
623 [ + + ]: 640 : if (d_state.areEqual(conc, d_false))
624 : : {
625 : : // we are in conflict
626 : 21 : d_im.addToExplanation(conc, d_false, in.d_exp);
627 : 21 : d_im.sendInference(
628 : 21 : in.d_exp, d_false, InferenceId::STRINGS_CTN_DECOMPOSE);
629 [ - + ][ - + ]: 21 : Assert(d_state.isInConflict());
[ - - ]
630 : 21 : return;
631 : : }
632 [ + + ]: 619 : else if (d_extt.hasFunctionKind(conc.getKind()))
633 : : {
634 : : // can mark as reduced, since model for n implies model for conc
635 : 210 : d_extt.markInactive(conc, ExtReducedId::STRINGS_CTN_DECOMPOSE);
636 : : }
637 : : }
638 [ + + ][ + + ]: 10617 : }
[ + + ]
639 [ + + ]: 3394 : }
640 : : }
641 : : else
642 : : {
643 : 182817 : if (std::find(d_extfInfoTmp[nr[0]].d_ctn[pol].begin(),
644 : 121878 : d_extfInfoTmp[nr[0]].d_ctn[pol].end(),
645 : : nr[1])
646 [ + - ]: 182817 : == d_extfInfoTmp[nr[0]].d_ctn[pol].end())
647 : : {
648 [ + - ][ - - ]: 121878 : Trace("strings-extf-debug") << " store contains info : " << nr[0]
649 [ - + ][ - + ]: 60939 : << " " << pol << " " << nr[1] << std::endl;
[ - - ]
650 : : // Store s (does not) contains t, since nr = (~)contains( s, t ) holds.
651 : 60939 : d_extfInfoTmp[nr[0]].d_ctn[pol].push_back(nr[1]);
652 : 60939 : d_extfInfoTmp[nr[0]].d_ctnFrom[pol].push_back(n);
653 : : // Do transistive closure on contains, e.g.
654 : : // if contains( s, t ) and ~contains( s, r ), then ~contains( t, r ).
655 : :
656 : : // The following infers new (negative) contains based on the above
657 : : // reasoning, provided that ~contains( t, r ) does not
658 : : // already hold in the current context. We test this by checking that
659 : : // contains( t, r ) is not already asserted false in the current
660 : : // context. We also handle the case where contains( t, r ) is equivalent
661 : : // to t = r, in which case we check that t != r does not already hold
662 : : // in the current context.
663 : :
664 : : // Notice that form of the above inference is enough to find
665 : : // conflicts purely due to contains predicates. For example, if we
666 : : // have only positive occurrences of contains, then no conflicts due to
667 : : // contains predicates are possible and this schema does nothing. For
668 : : // example, note that contains( s, t ) and contains( t, r ) implies
669 : : // contains( s, r ), which we could but choose not to infer. Instead,
670 : : // we prefer being lazy: only if ~contains( s, r ) appears later do we
671 : : // infer ~contains( t, r ), which suffices to show a conflict.
672 : 60939 : bool opol = !pol;
673 : 65962 : for (unsigned i = 0, size = d_extfInfoTmp[nr[0]].d_ctn[opol].size();
674 [ + + ]: 65962 : i < size;
675 : : i++)
676 : : {
677 : 5023 : Node onr = d_extfInfoTmp[nr[0]].d_ctn[opol][i];
678 : : Node concOrig = nm->mkNode(
679 [ + + ][ + + ]: 10046 : Kind::STRING_CONTAINS, pol ? nr[1] : onr, pol ? onr : nr[1]);
680 : 5023 : Node conc = rewrite(concOrig);
681 : : // For termination concerns, we only do the inference if the contains
682 : : // does not rewrite (and thus does not introduce new terms).
683 [ + + ]: 5023 : if (conc == concOrig)
684 : : {
685 : 381 : bool do_infer = false;
686 : 381 : conc = conc.negate();
687 : 381 : bool pol2 = conc.getKind() != Kind::NOT;
688 [ - + ]: 381 : Node lit = pol2 ? conc : conc[0];
689 [ - + ]: 381 : if (lit.getKind() == Kind::EQUAL)
690 : : {
691 : 0 : do_infer = pol2 ? !d_state.areEqual(lit[0], lit[1])
692 : 0 : : !d_state.areDisequal(lit[0], lit[1]);
693 : : }
694 : : else
695 : : {
696 [ - + ]: 381 : do_infer = !d_state.areEqual(lit, pol2 ? d_true : d_false);
697 : : }
698 [ + + ]: 381 : if (do_infer)
699 : : {
700 : 173 : std::vector<Node> exp_c;
701 : 173 : exp_c.insert(exp_c.end(), in.d_exp.begin(), in.d_exp.end());
702 : 173 : Node ofrom = d_extfInfoTmp[nr[0]].d_ctnFrom[opol][i];
703 [ - + ][ - + ]: 173 : Assert(d_extfInfoTmp.find(ofrom) != d_extfInfoTmp.end());
[ - - ]
704 : 173 : exp_c.insert(exp_c.end(),
705 : 173 : d_extfInfoTmp[ofrom].d_exp.begin(),
706 : 173 : d_extfInfoTmp[ofrom].d_exp.end());
707 : 173 : d_im.sendInference(exp_c, conc, InferenceId::STRINGS_CTN_TRANS);
708 : 173 : }
709 : 381 : }
710 : 5023 : }
711 : : }
712 : : else
713 : : {
714 : : // If we already know that s (does not) contain t, then n may be
715 : : // redundant. However, we do not mark n as reduced here, since strings
716 : : // reductions may require dependencies between extended functions.
717 : : // Marking reduced here could lead to incorrect models if an
718 : : // extended function is marked reduced based on an assignment to
719 : : // something that depends on n.
720 [ - - ]: 0 : Trace("strings-extf-debug") << " redundant." << std::endl;
721 : : }
722 : : }
723 : 66558 : return;
724 : : }
725 : :
726 : : // If it's not a predicate, see if we can solve the equality n = c, where c
727 : : // is the constant that extended term n is equal to.
728 : 151247 : Node inferEq = nr.eqNode(in.d_const);
729 : 151247 : Node inferEqr = rewrite(inferEq);
730 : 151247 : Node inferEqrr = inferEqr;
731 [ + + ]: 151247 : if (inferEqr.getKind() == Kind::EQUAL)
732 : : {
733 : : // try to use the extended rewriter for equalities
734 : 107641 : inferEqrr = d_rewriter.rewriteEqualityExt(inferEqr);
735 : : }
736 [ + + ]: 151247 : if (inferEqrr != inferEqr)
737 : : {
738 : 10197 : inferEqrr = rewrite(inferEqrr);
739 [ + - ]: 20394 : Trace("strings-extf-infer")
740 : 0 : << "checkExtfInference: " << inferEq << " ...reduces to " << inferEqrr
741 : 10197 : << " with explanation " << in.d_exp << std::endl;
742 : 20394 : d_im.sendInternalInference(
743 : 10197 : in.d_exp, inferEqrr, InferenceId::STRINGS_EXTF_EQ_REW);
744 : : }
745 : 151247 : }
746 : :
747 : 1997612 : Node ExtfSolver::getCurrentSubstitutionFor(int effort,
748 : : Node n,
749 : : std::vector<Node>& exp)
750 : : {
751 [ + + ]: 1997612 : if (effort >= 3)
752 : : {
753 : : // model values
754 : 16174 : Node mv = d_state.getModel()->getRepresentative(n);
755 [ + - ]: 16174 : Trace("strings-subs") << " model val : " << mv << std::endl;
756 : 16174 : return mv;
757 : 16174 : }
758 : 3962876 : Node nr = d_state.getRepresentative(n);
759 : : // if the normal form is available, use it
760 [ + + ][ + + ]: 1981438 : if (effort >= 1 && n.getType().isStringLike())
[ + + ][ + + ]
[ - - ]
761 : : {
762 [ - + ][ - + ]: 154367 : Assert(effort < 3);
[ - - ]
763 : : // Return self if the normal form has not been computed. This may happen
764 : : // for terms that are not relevant in the current context.
765 [ + + ]: 154367 : if (!d_csolver.hasNormalForm(nr))
766 : : {
767 : 2 : return n;
768 : : }
769 : 154365 : NormalForm& nfnr = d_csolver.getNormalForm(nr);
770 : 154365 : Node ns;
771 [ + + ][ + + ]: 154365 : if (n.getKind() == Kind::STRING_CONCAT && n != nfnr.d_base)
[ + + ]
772 : : {
773 : : // if the normal base is a term (str.++ t1 t2), and we are a term
774 : : // (str.++ s1 s2), then we explain the normal form concatentation of
775 : : // s1 and s2, instead of explaining (= (str.++ s1 s2) (str.++ t1 t2)) and
776 : : // concatentating the normal form explanation of t1 and t2. This
777 : : // ensures the explanation when taking as a substitution does not have
778 : : // concatentation terms on the LHS of equalities, which can lead to
779 : : // cyclic proof dependencies.
780 : 3463 : std::vector<Node> vec;
781 [ + + ]: 10595 : for (const Node& nc : n)
782 : : {
783 : 14264 : Node ncr = d_state.getRepresentative(nc);
784 [ - + ][ - + ]: 7132 : Assert(d_csolver.hasNormalForm(ncr));
[ - - ]
785 : 7132 : NormalForm& nfnrc = d_csolver.getNormalForm(ncr);
786 : 7132 : Node nsc = d_csolver.getNormalString(nfnrc.d_base, exp);
787 : 7132 : d_im.addToExplanation(nc, nfnrc.d_base, exp);
788 : 7132 : vec.push_back(nsc);
789 : 7132 : }
790 : 3463 : TypeNode stype = n.getType();
791 : 3463 : ns = d_termReg.mkNConcat(vec, stype);
792 : 3463 : }
793 : : else
794 : : {
795 : 150902 : ns = d_csolver.getNormalString(nfnr.d_base, exp);
796 [ + - ]: 301804 : Trace("strings-subs") << " normal eqc : " << ns << " " << nfnr.d_base
797 : 150902 : << " " << nr << std::endl;
798 [ + - ]: 150902 : if (!nfnr.d_base.isNull())
799 : : {
800 : 150902 : d_im.addToExplanation(n, nfnr.d_base, exp);
801 : : }
802 : : }
803 : 154365 : return ns;
804 : 154365 : }
805 : : // otherwise, we use the best content heuristic
806 : 1827071 : std::vector<Node> cexp;
807 : 3654142 : Node c = d_bsolver.explainBestContentEqc(n, nr, cexp);
808 [ + + ][ + + ]: 1827071 : if (!c.isNull() && n.getKind() == Kind::STRING_CONCAT)
[ + + ]
809 : : {
810 : 19463 : cexp.clear();
811 : : // Similar to above, if we are a string concatentation, we ask for the
812 : : // best content of each of our children and concatenate them together.
813 : : // We consider the substitution only if at least one child had a best
814 : : // content. This prevents substitutions with concatenation terms on the
815 : : // left hand side, which can lead to cycles in the algorithm that elaborates
816 : : // proofs in very rare cases.
817 : 19463 : std::vector<Node> vec;
818 [ + + ]: 64967 : for (const Node& nc : n)
819 : : {
820 : 91008 : Node ncr = d_state.getRepresentative(nc);
821 : 91008 : Node cc = d_bsolver.explainBestContentEqc(nc, ncr, cexp);
822 [ + + ]: 45504 : if (!cc.isNull())
823 : : {
824 : 35287 : vec.push_back(cc);
825 : : }
826 : : else
827 : : {
828 : : // otherwise keep the same
829 : 10217 : vec.push_back(nc);
830 : : }
831 : 45504 : }
832 : 19463 : TypeNode stype = n.getType();
833 : 19463 : c = d_termReg.mkNConcat(vec, stype);
834 : 19463 : }
835 [ + + ]: 1827071 : if (!c.isNull())
836 : : {
837 : 963227 : exp.insert(exp.end(), cexp.begin(), cexp.end());
838 : 963227 : return c;
839 : : }
840 : 863844 : return n;
841 : 1981438 : }
842 : :
843 : 0 : const std::map<Node, ExtfInfoTmp>& ExtfSolver::getInfo() const
844 : : {
845 : 0 : return d_extfInfoTmp;
846 : : }
847 : 26293 : bool ExtfSolver::hasExtendedFunctions() const { return d_hasExtf.get(); }
848 : :
849 : 38317 : std::vector<Node> ExtfSolver::getActive(Kind k) const
850 : : {
851 : 38317 : return d_extt.getActive(k);
852 : : }
853 : :
854 : 452210 : bool ExtfSolver::isActiveInModel(Node n) const
855 : : {
856 : 452210 : std::map<Node, ExtfInfoTmp>::const_iterator it = d_extfInfoTmp.find(n);
857 [ - + ]: 452210 : if (it == d_extfInfoTmp.end())
858 : : {
859 : 0 : DebugUnhandled() << "isActiveInModel: Expected extf info for " << n;
860 : : return true;
861 : : }
862 : 452210 : return it->second.d_modelActive;
863 : : }
864 : :
865 : 108996 : std::vector<Node> ExtfSolver::getRelevantActive() const
866 : : {
867 : : // get the relevant term set
868 : 108996 : std::vector<Node> extf = d_extt.getActive();
869 : 108996 : const std::set<Node>& relevantTerms = d_termReg.getRelevantTermSet();
870 : :
871 : 108996 : std::vector<Node> res;
872 [ + + ]: 587477 : for (const Node& n : extf)
873 : : {
874 [ + + ]: 478481 : if (relevantTerms.find(n) == relevantTerms.end())
875 : : {
876 : : // not relevant
877 : 9417 : continue;
878 : : }
879 : 469064 : res.push_back(n);
880 : : }
881 : 217992 : return res;
882 : 108996 : }
883 : :
884 : 0 : bool StringsExtfCallback::getCurrentSubstitution(
885 : : int effort,
886 : : const std::vector<Node>& vars,
887 : : std::vector<Node>& subs,
888 : : std::map<Node, std::vector<Node> >& exp)
889 : : {
890 [ - - ]: 0 : Trace("strings-subs") << "getCurrentSubstitution, effort = " << effort
891 : 0 : << std::endl;
892 [ - - ]: 0 : for (const Node& v : vars)
893 : : {
894 [ - - ]: 0 : Trace("strings-subs") << " get subs for " << v << "..." << std::endl;
895 : 0 : Node s = d_esolver->getCurrentSubstitutionFor(effort, v, exp[v]);
896 : 0 : subs.push_back(s);
897 : 0 : }
898 : 0 : return true;
899 : : }
900 : :
901 : 0 : void ExtfSolver::processFact(InferInfo& ii, ProofGenerator*& pg)
902 : : {
903 : : // process it with the inference manager
904 : 0 : d_im.processFact(ii, pg);
905 : 0 : }
906 : :
907 : 4673 : TrustNode ExtfSolver::processLemma(InferInfo& ii, LemmaProperty& p)
908 : : {
909 : : // if this was the reduction lemma for a term, mark it reduced now
910 : 4673 : std::map<Node, Node>::iterator it = d_reductionWaitingMap.find(ii.d_conc);
911 [ + - ]: 4673 : if (it != d_reductionWaitingMap.end())
912 : : {
913 : 4673 : d_reduced.insert(it->second);
914 : 4673 : d_reductionWaitingMap.erase(it);
915 : : }
916 : : // now process it with the inference manager
917 : 9346 : return d_im.processLemma(ii, p);
918 : : }
919 : :
920 : 0 : std::string ExtfSolver::debugPrintModel()
921 : : {
922 : 0 : std::stringstream ss;
923 : 0 : std::vector<Node> extf;
924 : 0 : d_extt.getTerms(extf);
925 : : // each extended function should have at least one annotation below
926 [ - - ]: 0 : for (const Node& n : extf)
927 : : {
928 : 0 : ss << "- " << n;
929 : : ExtReducedId id;
930 [ - - ]: 0 : if (!d_extt.isActive(n, id))
931 : : {
932 : 0 : ss << " :extt-inactive " << id;
933 : : }
934 [ - - ]: 0 : if (!d_extfInfoTmp[n].d_modelActive)
935 : : {
936 : 0 : ss << " :model-inactive";
937 : : }
938 [ - - ]: 0 : if (d_reduced.find(n) != d_reduced.end())
939 : : {
940 : 0 : ss << " :reduced";
941 : : }
942 : 0 : ss << std::endl;
943 : : }
944 : 0 : return ss.str();
945 : 0 : }
946 : :
947 : 3706 : bool ExtfSolver::isReduced(const Node& n) const
948 : : {
949 : 3706 : return d_reduced.find(n) != d_reduced.end();
950 : : }
951 : :
952 : 880 : void ExtfSolver::markReduced(const Node& n) { d_reduced.insert(n); }
953 : :
954 : : } // namespace strings
955 : : } // namespace theory
956 : : } // namespace cvc5::internal
|
