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 the inference manager for the theory of strings.
11 : : */
12 : :
13 : : #include "theory/strings/inference_manager.h"
14 : :
15 : : #include "options/strings_options.h"
16 : : #include "theory/ext_theory.h"
17 : : #include "theory/rewriter.h"
18 : : #include "theory/strings/theory_strings_utils.h"
19 : : #include "theory/strings/word.h"
20 : : #include "util/rational.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 : 28700 : InferenceManager::InferenceManager(Env& env,
31 : : Theory& t,
32 : : SolverState& s,
33 : : TermRegistry& tr,
34 : : ExtTheory& e,
35 : 28700 : SequencesStatistics& statistics)
36 : : : InferenceManagerBuffered(env, t, s, "theory::strings::"),
37 : 28700 : d_state(s),
38 : 28700 : d_termReg(tr),
39 : 28700 : d_extt(e),
40 : 28700 : d_statistics(statistics),
41 [ + + ]: 28700 : d_ipc(isProofEnabled() ? new InferProofCons(env, context()) : nullptr),
42 [ + + ]: 57400 : d_ipcl(isProofEnabled() ? new InferProofCons(env, context()) : nullptr)
43 : : {
44 : 28700 : NodeManager* nm = nodeManager();
45 : 28700 : d_zero = nm->mkConstInt(Rational(0));
46 : 28700 : d_one = nm->mkConstInt(Rational(1));
47 : 28700 : d_true = nm->mkConst(true);
48 : 28700 : d_false = nm->mkConst(false);
49 : 28700 : }
50 : :
51 : 48867 : bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
52 : : Node conc,
53 : : InferenceId infer)
54 : : {
55 : 146601 : if (conc.getKind() == Kind::AND
56 [ + + ][ + + ]: 48867 : || (conc.getKind() == Kind::NOT && conc[0].getKind() == Kind::OR))
[ + + ][ + + ]
[ + + ][ - - ]
57 : : {
58 [ + + ]: 4606 : Node conj = conc.getKind() == Kind::AND ? conc : conc[0];
59 : 4606 : bool pol = conc.getKind() == Kind::AND;
60 : 4606 : bool ret = true;
61 [ + + ]: 15499 : for (const Node& cc : conj)
62 : : {
63 [ + + ]: 10893 : bool retc = sendInternalInference(exp, pol ? cc : cc.negate(), infer);
64 [ + + ][ + + ]: 10893 : ret = ret && retc;
65 : 10893 : }
66 : 4606 : return ret;
67 : 4606 : }
68 : 44261 : bool pol = conc.getKind() != Kind::NOT;
69 [ + + ]: 44261 : Node lit = pol ? conc : conc[0];
70 [ + + ]: 44261 : if (lit.getKind() == Kind::EQUAL)
71 : : {
72 [ + + ]: 14145 : for (unsigned i = 0; i < 2; i++)
73 : : {
74 : 10010 : if (!lit[i].isConst() && !d_state.hasTerm(lit[i]))
75 : : {
76 : : // introduces a new non-constant term, do not infer
77 : 926 : return false;
78 : : }
79 : : }
80 : : // does it already hold?
81 : 8270 : if (pol ? d_state.areEqual(lit[0], lit[1])
82 : 4135 : : d_state.areDisequal(lit[0], lit[1]))
83 : : {
84 : 3189 : return true;
85 : : }
86 : : }
87 [ + + ]: 39200 : else if (lit.isConst())
88 : : {
89 [ - + ]: 844 : if (lit.getConst<bool>())
90 : : {
91 : 0 : Assert(pol);
92 : : // trivially holds
93 : 0 : return true;
94 : : }
95 : : }
96 [ + + ]: 38356 : else if (!d_state.hasTerm(lit))
97 : : {
98 : : // introduces a new non-constant term, do not infer
99 : 36256 : return false;
100 : : }
101 [ + + ][ + + ]: 2100 : else if (d_state.areEqual(lit, pol ? d_true : d_false))
102 : : {
103 : : // already holds
104 : 2078 : return true;
105 : : }
106 : 1812 : sendInference(exp, conc, infer);
107 : 1812 : return true;
108 : 44261 : }
109 : :
110 : 135123 : bool InferenceManager::sendInference(const std::vector<Node>& exp,
111 : : const std::vector<Node>& noExplain,
112 : : Node eq,
113 : : InferenceId infer,
114 : : bool isRev,
115 : : bool asLemma)
116 : : {
117 [ + + ]: 135123 : if (eq.isNull())
118 : : {
119 : 110 : eq = d_false;
120 : : }
121 [ + + ]: 135013 : else if (rewrite(eq) == d_true)
122 : : {
123 : : // if trivial, return
124 : 2 : return false;
125 : : }
126 : : // wrap in infer info and send below
127 : 135121 : InferInfo ii(infer);
128 : 135121 : ii.d_idRev = isRev;
129 : 135121 : ii.d_conc = eq;
130 : 135121 : ii.d_premises = exp;
131 : 135121 : ii.d_noExplain = noExplain;
132 : 135121 : sendInference(ii, asLemma);
133 : 135121 : return true;
134 : 135121 : }
135 : :
136 : 132661 : bool InferenceManager::sendInference(const std::vector<Node>& exp,
137 : : Node eq,
138 : : InferenceId infer,
139 : : bool isRev,
140 : : bool asLemma)
141 : : {
142 : 132661 : std::vector<Node> noExplain;
143 : 265322 : return sendInference(exp, noExplain, eq, infer, isRev, asLemma);
144 : 132661 : }
145 : :
146 : 146156 : void InferenceManager::sendInference(InferInfo& ii, bool asLemma)
147 : : {
148 [ - + ][ - + ]: 146156 : Assert(!ii.isTrivial());
[ - - ]
149 : : // This inference manager will be processing the side effects of this
150 : : // inferences if the inference manager has not been marked already.
151 [ + + ]: 146156 : if (ii.d_sim == nullptr)
152 : : {
153 : 135121 : ii.d_sim = this;
154 : : }
155 [ + - ]: 292312 : Trace("strings-infer-debug")
156 : 146156 : << "sendInference: " << ii << ", asLemma = " << asLemma << std::endl;
157 : : // check if we should send a conflict, lemma or a fact
158 [ + + ]: 146156 : if (ii.isConflict())
159 : : {
160 [ + - ]: 2473 : Trace("strings-infer-debug") << "...as conflict" << std::endl;
161 [ + - ]: 4946 : Trace("strings-lemma") << "Strings::Conflict: " << ii.d_premises << " by "
162 : 2473 : << ii.getId() << std::endl;
163 [ + - ]: 4946 : Trace("strings-conflict")
164 : 0 : << "CONFLICT: inference conflict " << ii.d_premises << " by "
165 : 2473 : << ii.getId() << std::endl;
166 : 2473 : ++(d_statistics.d_conflictsInfer);
167 : : // process the conflict immediately
168 : 2473 : processConflict(ii);
169 : 2473 : return;
170 : : }
171 [ + + ][ + - ]: 143683 : else if (asLemma || options().strings.stringInferAsLemmas || !ii.isFact())
[ + + ][ + + ]
172 : : {
173 [ + - ]: 41246 : Trace("strings-infer-debug") << "...as lemma" << std::endl;
174 : 41246 : addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(ii)));
175 : 41246 : return;
176 : : }
177 [ + - ]: 102437 : if (options().strings.stringInferSym)
178 : : {
179 : 102437 : std::vector<Node> unproc;
180 [ + + ]: 333473 : for (const Node& ac : ii.d_premises)
181 : : {
182 : 231036 : d_termReg.removeProxyEqs(ac, unproc);
183 : : }
184 [ + + ]: 102437 : if (unproc.empty())
185 : : {
186 : 2 : Node eqs = ii.d_conc;
187 : : // keep the same id for now, since we are transforming the form of the
188 : : // inference, not the root reason.
189 : 2 : InferInfo iiSubsLem(ii.getId());
190 : 2 : iiSubsLem.d_sim = this;
191 : 2 : iiSubsLem.d_conc = eqs;
192 [ - + ]: 2 : if (TraceIsOn("strings-lemma-debug"))
193 : : {
194 [ - - ]: 0 : Trace("strings-lemma-debug")
195 : 0 : << "Strings::Infer " << iiSubsLem << std::endl;
196 [ - - ]: 0 : Trace("strings-lemma-debug")
197 : 0 : << "Strings::Infer Alternate : " << eqs << std::endl;
198 : : }
199 [ + - ]: 2 : Trace("strings-infer-debug") << "...as symbolic lemma" << std::endl;
200 : 2 : addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(iiSubsLem)));
201 : 2 : return;
202 : 2 : }
203 [ - + ]: 102435 : if (TraceIsOn("strings-lemma-debug"))
204 : : {
205 [ - - ]: 0 : for (const Node& u : unproc)
206 : : {
207 [ - - ]: 0 : Trace("strings-lemma-debug")
208 : 0 : << " non-trivial explanation : " << u << std::endl;
209 : : }
210 : : }
211 [ + + ]: 102437 : }
212 [ + - ]: 102435 : Trace("strings-infer-debug") << "...as fact" << std::endl;
213 : : // add to pending to be processed as a fact
214 : 102435 : addPendingFact(std::unique_ptr<InferInfo>(new InferInfo(ii)));
215 : : }
216 : :
217 : 4829 : bool InferenceManager::sendSplit(Node a, Node b, InferenceId infer, bool preq)
218 : : {
219 : 4829 : Node eq = a.eqNode(b);
220 : 4829 : eq = rewrite(eq);
221 [ - + ]: 4829 : if (eq.isConst())
222 : : {
223 : 0 : return false;
224 : : }
225 : 4829 : NodeManager* nm = nodeManager();
226 : 4829 : InferInfo iiSplit(infer);
227 : 4829 : iiSplit.d_sim = this;
228 : 4829 : iiSplit.d_conc = nm->mkNode(Kind::OR, eq, nm->mkNode(Kind::NOT, eq));
229 : 4829 : addPendingPhaseRequirement(eq, preq);
230 : 4829 : addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(iiSplit)));
231 : 4829 : return true;
232 : 4829 : }
233 : :
234 : 1597651 : void InferenceManager::addToExplanation(Node a,
235 : : Node b,
236 : : std::vector<Node>& exp) const
237 : : {
238 [ + + ]: 1597651 : if (a != b)
239 : : {
240 : : // prefer having constants on the RHS, which helps proof reconstruction
241 [ + + ][ + - ]: 723970 : if (a.isConst() && !b.isConst())
[ + + ]
242 : : {
243 : 2564 : Node tmp = a;
244 : 2564 : a = b;
245 : 2564 : b = tmp;
246 : 2564 : }
247 [ + - ]: 1447940 : Trace("strings-explain")
248 : 723970 : << "Add to explanation : " << a << " == " << b << std::endl;
249 [ - + ][ - + ]: 723970 : Assert(d_state.areEqual(a, b));
[ - - ]
250 : 723970 : exp.push_back(a.eqNode(b));
251 : : }
252 : 1597651 : }
253 : :
254 : 0 : void InferenceManager::addToExplanation(Node lit, std::vector<Node>& exp) const
255 : : {
256 [ - - ]: 0 : if (!lit.isNull())
257 : : {
258 : 0 : Assert(!lit.isConst());
259 : 0 : exp.push_back(lit);
260 : : }
261 : 0 : }
262 : :
263 : 132 : void InferenceManager::markInactive(Node n, ExtReducedId id, bool contextDepend)
264 : : {
265 : 132 : d_extt.markInactive(n, id, contextDepend);
266 : 132 : }
267 : :
268 : 3636 : void InferenceManager::processConflict(const InferInfo& ii)
269 : : {
270 [ - + ][ - + ]: 3636 : Assert(!d_state.isInConflict());
[ - - ]
271 [ + + ]: 3636 : if (ii.getId() == InferenceId::STRINGS_PREFIX_CONFLICT)
272 : : {
273 : 770 : bool isSuf = ii.d_idRev;
274 : : // The shape of prefix conflicts is P1? ^ P2? ^ (= x y)?
275 : : // where if applicable:
276 : : // P1 implies a prefix on string x,
277 : : // P2 implies a (conflicting) prefix on string y.
278 : : // See EqcInfo::mkMergeConflict.
279 [ + - ]: 1540 : Trace("strings-prefix-min") << "Minimize prefix conflict " << ii.d_premises
280 : 770 : << ", isSuf=" << isSuf << std::endl;
281 : 770 : size_t npremises = ii.d_premises.size();
282 : 770 : Node eq = ii.d_premises[npremises - 1];
283 : : // if we included an equality, we will try to minimize its explanation
284 [ + - ]: 770 : if (eq.getKind() == Kind::EQUAL)
285 : : {
286 : 770 : InferInfo iim(InferenceId::STRINGS_PREFIX_CONFLICT_MIN);
287 : 3080 : Node pft[2] = {eq[0], eq[1]};
288 [ + + ]: 1151 : for (size_t i = 0; i < (npremises - 1); i++)
289 : : {
290 [ + - ]: 381 : if (ii.d_premises[i].getKind() == Kind::STRING_IN_REGEXP)
291 : : {
292 [ + + ]: 381 : size_t eindex = ii.d_premises[i][0] == eq[0] ? 0 : 1;
293 [ - + ][ - + ]: 381 : Assert(ii.d_premises[i][0] == eq[eindex]);
[ - - ]
294 : : // the basis of prefix for eq[eindex] is the RE of this premise
295 : 381 : pft[eindex] = ii.d_premises[i][1];
296 : : }
297 : : // include it in the explanation
298 : 381 : iim.d_premises.push_back(ii.d_premises[i]);
299 : : }
300 [ + - ]: 1540 : Trace("strings-prefix-min")
301 : 770 : << "Prefix terms: " << pft[0] << " / " << pft[1] << std::endl;
302 [ + + ]: 4620 : Node pfv[2];
303 [ + + ]: 2310 : for (size_t i = 0; i < 2; i++)
304 : : {
305 : 1540 : pfv[i] = utils::getConstantEndpoint(pft[i], isSuf);
306 : : }
307 [ + - ]: 1540 : Trace("strings-prefix-min")
308 : 770 : << "Prefixes: " << pfv[0] << " / " << pfv[1] << std::endl;
309 [ + + ]: 2166 : for (size_t i = 0; i < 2; i++)
310 : : {
311 : 1468 : if (pft[1 - i] == eq[1 - i] && pft[i] != eq[i])
312 : : {
313 : : // if the other side is justified by itself and we are justified
314 : : // externally, we can try to minimize the explanation of this
315 : : // get the minimal conflicting prefix
316 : 377 : std::vector<TNode> assumptions;
317 : 377 : explain(eq, assumptions);
318 : 377 : std::map<TNode, TNode> emap = getExplanationMap(assumptions);
319 : : Node mexp =
320 : 754 : mkPrefixExplainMin(eq[i], pfv[i], assumptions, emap, isSuf);
321 : : // if we minimized the conflict, process it
322 [ + + ]: 377 : if (!mexp.isNull())
323 : : {
324 : : // must flatten here
325 : 72 : utils::flattenOp(Kind::AND, mexp, iim.d_premises);
326 : 72 : iim.d_conc = ii.d_conc;
327 : 72 : processConflict(iim);
328 : 72 : return;
329 : : }
330 [ + + ][ + + ]: 521 : }
[ + + ]
331 : : }
332 [ + + ][ + + ]: 5390 : }
[ + + ][ - - ]
[ - - ]
333 : : // otherwise if we fail to minimize, process the original
334 [ + + ]: 770 : }
335 : : // setup the fact to reproduce the proof in the call below
336 [ + + ]: 3564 : if (d_ipcl != nullptr)
337 : : {
338 : 1731 : d_ipcl->notifyLemma(ii);
339 : : }
340 : : // make the trust node
341 [ + + ]: 3564 : TrustNode tconf = mkConflictExp(ii.d_premises, d_ipcl.get());
342 [ - + ][ - + ]: 3564 : Assert(tconf.getKind() == TrustNodeKind::CONFLICT);
[ - - ]
343 [ + - ][ - - ]: 7128 : Trace("strings-assert") << "(assert (not " << tconf.getNode()
344 [ - + ]: 3564 : << ")) ; conflict " << ii.getId() << std::endl;
345 : : // send the trusted conflict
346 : 3564 : trustedConflict(tconf, ii.getId());
347 : 3564 : }
348 : :
349 : 98868 : void InferenceManager::processFact(InferInfo& ii, ProofGenerator*& pg)
350 : : {
351 [ + - ][ - - ]: 197736 : Trace("strings-assert") << "(assert (=> " << ii.getPremises(nodeManager())
352 [ - + ]: 98868 : << " " << ii.d_conc << ")) ; fact " << ii.getId()
353 : 98868 : << std::endl;
354 [ + - ]: 197736 : Trace("strings-lemma") << "Strings::Fact: " << ii.d_conc << " from "
355 [ - - ]: 98868 : << ii.getPremises(nodeManager()) << " by "
356 [ - + ]: 98868 : << ii.getId() << std::endl;
357 [ + + ]: 98868 : if (d_ipc != nullptr)
358 : : {
359 : : // ensure the proof generator is ready to explain this fact in the
360 : : // current SAT context
361 : 44127 : d_ipc->notifyFact(ii);
362 [ + - ]: 44127 : pg = d_ipc.get();
363 : : }
364 : : // ensure facts are for rewritten terms
365 [ + - ]: 98868 : if (Configuration::isAssertionBuild())
366 : : {
367 [ + + ]: 98868 : Node atom = ii.d_conc.getKind() == Kind::NOT ? ii.d_conc[0] : ii.d_conc;
368 [ + + ]: 98868 : if (atom.getKind() == Kind::EQUAL)
369 : : {
370 [ - + ][ - + ]: 98675 : Assert(rewrite(atom[0]) == atom[0]);
[ - - ]
371 [ - + ][ - + ]: 98675 : Assert(rewrite(atom[1]) == atom[1]);
[ - - ]
372 : : }
373 : : else
374 : : {
375 [ - + ][ - + ]: 193 : Assert(rewrite(atom) == atom);
[ - - ]
376 : : }
377 : 98868 : }
378 : 98868 : }
379 : :
380 : 45638 : TrustNode InferenceManager::processLemma(InferInfo& ii, LemmaProperty& p)
381 : : {
382 [ - + ][ - + ]: 45638 : Assert(!ii.isTrivial());
[ - - ]
383 [ - + ][ - + ]: 45638 : Assert(!ii.isConflict());
[ - - ]
384 : : // set up the explanation and no-explanation
385 : 45638 : std::vector<Node> exp;
386 [ + + ]: 149806 : for (const Node& ec : ii.d_premises)
387 : : {
388 : 104168 : utils::flattenOp(Kind::AND, ec, exp);
389 : : }
390 : 45638 : std::vector<Node> noExplain;
391 [ - + ]: 45638 : if (!options().strings.stringRExplainLemmas)
392 : : {
393 : : // if we aren't regressing the explanation, we add all literals to
394 : : // noExplain and ignore ii.d_ant.
395 : 0 : noExplain.insert(noExplain.end(), exp.begin(), exp.end());
396 : : }
397 : : else
398 : : {
399 : : // otherwise, the no-explain literals are those provided
400 [ + + ]: 49752 : for (const Node& ecn : ii.d_noExplain)
401 : : {
402 : 4114 : utils::flattenOp(Kind::AND, ecn, noExplain);
403 : : }
404 : : }
405 : : // ensure that the proof generator is ready to explain the final conclusion
406 : : // of the lemma (ii.d_conc).
407 [ + + ]: 45638 : if (d_ipcl != nullptr)
408 : : {
409 : 18077 : d_ipcl->notifyLemma(ii);
410 : : }
411 [ + + ]: 45638 : TrustNode tlem = mkLemmaExp(ii.d_conc, exp, noExplain, d_ipcl.get());
412 [ + - ][ - + ]: 91276 : Trace("strings-pending") << "Process pending lemma : " << tlem.getNode()
[ - - ]
413 : 45638 : << std::endl;
414 : :
415 : : // Process the side effects of the inference info.
416 : : // Register the new skolems from this inference. We register them here
417 : : // (lazily), since this is the moment when we have decided to process the
418 : : // inference.
419 : 45638 : for (const std::pair<const LengthStatus, std::vector<Node> >& sks :
420 [ + + ]: 93901 : ii.d_skolems)
421 : : {
422 [ + + ]: 5250 : for (const Node& n : sks.second)
423 : : {
424 : 2625 : d_termReg.registerTermAtomic(n, sks.first);
425 : : }
426 : : }
427 [ + + ]: 45638 : if (ii.getId() == InferenceId::STRINGS_REDUCTION)
428 : : {
429 : 4697 : p |= LemmaProperty::NEEDS_JUSTIFY;
430 : : }
431 : : // send phase requirements
432 [ + + ]: 47655 : for (const std::pair<const Node, bool>& pp : ii.d_pendingPhase)
433 : : {
434 : 2017 : Node ppr = rewrite(pp.first);
435 : 2017 : addPendingPhaseRequirement(ppr, pp.second);
436 : 2017 : }
437 [ + - ][ - - ]: 91276 : Trace("strings-assert") << "(assert " << tlem.getNode() << ") ; lemma "
438 [ - + ]: 45638 : << ii.getId() << std::endl;
439 [ + - ][ - - ]: 91276 : Trace("strings-lemma") << "Strings::Lemma: " << tlem.getNode() << " by "
440 [ - + ]: 45638 : << ii.getId() << std::endl;
441 : 91276 : return tlem;
442 : 45638 : }
443 : :
444 : 377 : std::map<TNode, TNode> InferenceManager::getExplanationMap(
445 : : const std::vector<TNode>& assumptions)
446 : : {
447 : 377 : std::map<TNode, TNode> emap;
448 [ + + ]: 1336 : for (TNode e : assumptions)
449 : : {
450 [ + + ]: 959 : if (e.getKind() != Kind::EQUAL)
451 : : {
452 : : // skip non-equalities, which could be included if we internally
453 : : // concluded an equality as a fact from a non-equality
454 : 57 : continue;
455 : : }
456 [ + + ]: 2706 : for (size_t i = 0; i < 2; i++)
457 : : {
458 : 1804 : emap[e[i]] = e;
459 : : }
460 [ + + ]: 959 : }
461 : 377 : return emap;
462 : 0 : }
463 : 377 : Node InferenceManager::mkPrefixExplainMin(Node x,
464 : : Node prefix,
465 : : const std::vector<TNode>& assumptions,
466 : : const std::map<TNode, TNode>& emap,
467 : : bool isSuf)
468 : : {
469 [ - + ][ - + ]: 377 : Assert(prefix.isConst());
[ - - ]
470 [ + - ]: 754 : Trace("strings-prefix-min")
471 [ - - ]: 0 : << "mkPrefixExplainMin: " << x << " for " << (isSuf ? "suffix" : "prefix")
472 : 377 : << " " << prefix << std::endl;
473 [ + - ]: 377 : Trace("strings-prefix-min") << "- via: " << assumptions << std::endl;
474 : 377 : std::vector<TNode> minAssumptions;
475 : : // the current node(s) we are looking at
476 : 377 : std::vector<TNode> cc;
477 : 377 : cc.push_back(x);
478 : 377 : size_t pindex = 0;
479 : 377 : std::vector<Node> pchars = Word::getChars(prefix);
480 : 377 : std::map<TNode, TNode>::const_iterator it;
481 : 377 : bool isConflict = false;
482 [ + - ][ + + ]: 1473 : while (pindex < pchars.size() && !cc.empty())
[ + + ]
483 : : {
484 [ + - ]: 2644 : Trace("strings-prefix-min")
485 : 1322 : << " " << pindex << "/" << pchars.size() << ", " << cc << std::endl;
486 : 1322 : TNode c = cc.back();
487 : 1322 : cc.pop_back();
488 [ + + ]: 1322 : if (c.isConst())
489 : : {
490 : : // check for conflict
491 : 351 : std::vector<Node> cchars = Word::getChars(c);
492 : 351 : size_t cindex = 0;
493 [ + - ][ + + ]: 361 : while (pindex < pchars.size() && cindex < cchars.size())
[ + + ]
494 : : {
495 [ + + ]: 150 : size_t pii = isSuf ? (pchars.size() - 1) - pindex : pindex;
496 [ + + ]: 150 : size_t cii = isSuf ? (cchars.size() - 1) - cindex : cindex;
497 [ + + ]: 150 : if (cchars[cii] != pchars[pii])
498 : : {
499 [ + - ]: 280 : Trace("strings-prefix-min") << "...conflict at " << pindex
500 : 140 : << " while processing " << c << std::endl;
501 : 140 : isConflict = true;
502 : 140 : break;
503 : : }
504 : 10 : pindex++;
505 : 10 : cindex++;
506 : : }
507 [ + + ]: 351 : if (isConflict)
508 : : {
509 : 140 : break;
510 : : }
511 : 211 : continue;
512 [ + + ]: 351 : }
513 : 971 : it = emap.find(c);
514 [ + + ]: 971 : if (it != emap.end())
515 : : {
516 : 879 : TNode ceq = it->second;
517 : : // do not continue if not already processed, which also avoids
518 : : // non-termination
519 : 879 : if (std::find(minAssumptions.begin(), minAssumptions.end(), ceq)
520 [ + + ]: 1758 : == minAssumptions.end())
521 : : {
522 [ - + ][ - + ]: 578 : Assert(ceq.getKind() == Kind::EQUAL);
[ - - ]
523 : 578 : Assert(ceq[0] == c || ceq[1] == c);
524 : : // add to explanation and look at the term it is equal to
525 : 578 : minAssumptions.push_back(ceq);
526 [ + + ]: 578 : TNode oc = ceq[ceq[0] == c ? 1 : 0];
527 : 578 : cc.push_back(oc);
528 : 578 : continue;
529 : 578 : }
530 [ + + ]: 879 : }
531 : : // we don't know what it is equal to
532 : : // if it is a concatenation, try to recurse into children
533 [ + + ]: 393 : if (c.getKind() == Kind::STRING_CONCAT)
534 : : {
535 [ + + ]: 1109 : for (size_t i = 0, nchild = c.getNumChildren(); i < nchild; i++)
536 : : {
537 : : // reverse if it is a prefix
538 [ + + ]: 802 : size_t ii = isSuf ? i : (nchild - 1) - i;
539 : 802 : cc.push_back(c[ii]);
540 : : }
541 : 307 : continue;
542 : 307 : }
543 [ + - ]: 86 : Trace("strings-prefix-min") << "-> no explanation for " << c << std::endl;
544 : 86 : break;
545 [ + + ]: 1322 : }
546 [ + + ][ + + ]: 377 : if (isConflict && minAssumptions.size() < assumptions.size())
[ + + ]
547 : : {
548 [ + - ]: 144 : Trace("strings-prefix-min")
549 : 72 : << "-> min-explained: " << minAssumptions << std::endl;
550 [ + - ]: 144 : Trace("strings-exp-min-stats")
551 : 0 : << "Min-explain (prefix) " << minAssumptions.size() << " / "
552 : 72 : << assumptions.size() << std::endl;
553 : 72 : return nodeManager()->mkAnd(minAssumptions);
554 : : }
555 : 305 : return Node::null();
556 : 377 : }
557 : :
558 : : } // namespace strings
559 : : } // namespace theory
560 : : } // namespace cvc5::internal
|
