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