Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Gereon Kremer, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Implementation of the inference manager for the theory of strings.
14 : : */
15 : :
16 : : #include "theory/strings/inference_manager.h"
17 : :
18 : : #include "options/strings_options.h"
19 : : #include "theory/ext_theory.h"
20 : : #include "theory/rewriter.h"
21 : : #include "theory/strings/theory_strings_utils.h"
22 : : #include "theory/strings/word.h"
23 : : #include "util/rational.h"
24 : :
25 : : using namespace std;
26 : : using namespace cvc5::context;
27 : : using namespace cvc5::internal::kind;
28 : :
29 : : namespace cvc5::internal {
30 : : namespace theory {
31 : : namespace strings {
32 : :
33 : 50196 : InferenceManager::InferenceManager(Env& env,
34 : : Theory& t,
35 : : SolverState& s,
36 : : TermRegistry& tr,
37 : : ExtTheory& e,
38 : 50196 : SequencesStatistics& statistics)
39 : : : InferenceManagerBuffered(env, t, s, "theory::strings::"),
40 : : d_state(s),
41 : : d_termReg(tr),
42 : : d_extt(e),
43 : : d_statistics(statistics),
44 : 10068 : d_ipc(isProofEnabled() ? new InferProofCons(env, context()) : nullptr),
45 [ + + ][ + + ]: 60264 : d_ipcl(isProofEnabled() ? new InferProofCons(env, context()) : nullptr)
46 : : {
47 : 50196 : NodeManager* nm = nodeManager();
48 : 50196 : d_zero = nm->mkConstInt(Rational(0));
49 : 50196 : d_one = nm->mkConstInt(Rational(1));
50 : 50196 : d_true = nm->mkConst(true);
51 : 50196 : d_false = nm->mkConst(false);
52 : 50196 : }
53 : :
54 : 98446 : void InferenceManager::doPending()
55 : : {
56 : 98446 : doPendingFacts();
57 [ + + ]: 98446 : if (d_state.isInConflict())
58 : : {
59 : : // just clear the pending vectors, nothing else to do
60 : 5915 : clearPendingLemmas();
61 : 5915 : clearPendingPhaseRequirements();
62 : 5915 : return;
63 : : }
64 : 92531 : doPendingLemmas();
65 : 92531 : doPendingPhaseRequirements();
66 : : }
67 : :
68 : 36569 : bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
69 : : Node conc,
70 : : InferenceId infer)
71 : : {
72 : 109707 : if (conc.getKind() == Kind::AND
73 [ + + ][ + + ]: 36569 : || (conc.getKind() == Kind::NOT && conc[0].getKind() == Kind::OR))
[ + + ][ + + ]
[ + + ][ - - ]
74 : : {
75 [ + + ]: 1933 : Node conj = conc.getKind() == Kind::AND ? conc : conc[0];
76 : 1933 : bool pol = conc.getKind() == Kind::AND;
77 : 1933 : bool ret = true;
78 [ + + ]: 7494 : for (const Node& cc : conj)
79 : : {
80 [ + + ]: 5561 : bool retc = sendInternalInference(exp, pol ? cc : cc.negate(), infer);
81 [ + + ][ + + ]: 5561 : ret = ret && retc;
82 : : }
83 : 1933 : return ret;
84 : : }
85 : 34636 : bool pol = conc.getKind() != Kind::NOT;
86 [ + + ]: 69272 : Node lit = pol ? conc : conc[0];
87 [ + + ]: 34636 : if (lit.getKind() == Kind::EQUAL)
88 : : {
89 [ + + ]: 13212 : for (unsigned i = 0; i < 2; i++)
90 : : {
91 : 9262 : if (!lit[i].isConst() && !d_state.hasTerm(lit[i]))
92 : : {
93 : : // introduces a new non-constant term, do not infer
94 : 702 : return false;
95 : : }
96 : : }
97 : : // does it already hold?
98 : 7900 : if (pol ? d_state.areEqual(lit[0], lit[1])
99 : 3950 : : d_state.areDisequal(lit[0], lit[1]))
100 : : {
101 : 3054 : return true;
102 : : }
103 : : }
104 [ + + ]: 29984 : else if (lit.isConst())
105 : : {
106 [ - + ]: 719 : if (lit.getConst<bool>())
107 : : {
108 : 0 : Assert(pol);
109 : : // trivially holds
110 : 0 : return true;
111 : : }
112 : : }
113 [ + + ]: 29265 : else if (!d_state.hasTerm(lit))
114 : : {
115 : : // introduces a new non-constant term, do not infer
116 : 26916 : return false;
117 : : }
118 [ + + ][ + + ]: 2349 : else if (d_state.areEqual(lit, pol ? d_true : d_false))
119 : : {
120 : : // already holds
121 : 2322 : return true;
122 : : }
123 : 1642 : sendInference(exp, conc, infer);
124 : 1642 : return true;
125 : : }
126 : :
127 : 121264 : bool InferenceManager::sendInference(const std::vector<Node>& exp,
128 : : const std::vector<Node>& noExplain,
129 : : Node eq,
130 : : InferenceId infer,
131 : : bool isRev,
132 : : bool asLemma)
133 : : {
134 [ + + ]: 121264 : if (eq.isNull())
135 : : {
136 : 96 : eq = d_false;
137 : : }
138 [ + + ]: 121168 : else if (rewrite(eq) == d_true)
139 : : {
140 : : // if trivial, return
141 : 2 : return false;
142 : : }
143 : : // wrap in infer info and send below
144 : 121262 : InferInfo ii(infer);
145 : 121262 : ii.d_idRev = isRev;
146 : 121262 : ii.d_conc = eq;
147 : 121262 : ii.d_premises = exp;
148 : 121262 : ii.d_noExplain = noExplain;
149 : 121262 : sendInference(ii, asLemma);
150 : 121262 : return true;
151 : : }
152 : :
153 : 118837 : bool InferenceManager::sendInference(const std::vector<Node>& exp,
154 : : Node eq,
155 : : InferenceId infer,
156 : : bool isRev,
157 : : bool asLemma)
158 : : {
159 : 118837 : std::vector<Node> noExplain;
160 : 237674 : return sendInference(exp, noExplain, eq, infer, isRev, asLemma);
161 : : }
162 : :
163 : 131881 : void InferenceManager::sendInference(InferInfo& ii, bool asLemma)
164 : : {
165 [ - + ][ - + ]: 131881 : Assert(!ii.isTrivial());
[ - - ]
166 : : // This inference manager will be processing the side effects of this
167 : : // inferences if the inference manager has not been marked already.
168 [ + + ]: 131881 : if (ii.d_sim == nullptr)
169 : : {
170 : 121262 : ii.d_sim = this;
171 : : }
172 [ + - ]: 263762 : Trace("strings-infer-debug")
173 : 131881 : << "sendInference: " << ii << ", asLemma = " << asLemma << std::endl;
174 : : // check if we should send a conflict, lemma or a fact
175 [ + + ]: 131881 : if (ii.isConflict())
176 : : {
177 [ + - ]: 2305 : Trace("strings-infer-debug") << "...as conflict" << std::endl;
178 [ + - ]: 4610 : Trace("strings-lemma") << "Strings::Conflict: " << ii.d_premises << " by "
179 : 2305 : << ii.getId() << std::endl;
180 [ + - ]: 2305 : Trace("strings-conflict") << "CONFLICT: inference conflict " << ii.d_premises << " by " << ii.getId() << std::endl;
181 : 2305 : ++(d_statistics.d_conflictsInfer);
182 : : // process the conflict immediately
183 : 2305 : processConflict(ii);
184 : 2305 : return;
185 : : }
186 [ + + ][ + - ]: 129576 : else if (asLemma || options().strings.stringInferAsLemmas || !ii.isFact())
[ + + ][ + + ]
187 : : {
188 [ + - ]: 39157 : Trace("strings-infer-debug") << "...as lemma" << std::endl;
189 : 39157 : addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(ii)));
190 : 39157 : return;
191 : : }
192 [ + - ]: 90419 : if (options().strings.stringInferSym)
193 : : {
194 : 90419 : std::vector<Node> unproc;
195 [ + + ]: 296773 : for (const Node& ac : ii.d_premises)
196 : : {
197 : 206354 : d_termReg.removeProxyEqs(ac, unproc);
198 : : }
199 [ + + ]: 90419 : if (unproc.empty())
200 : : {
201 : 4 : Node eqs = ii.d_conc;
202 : : // keep the same id for now, since we are transforming the form of the
203 : : // inference, not the root reason.
204 : 2 : InferInfo iiSubsLem(ii.getId());
205 : 2 : iiSubsLem.d_sim = this;
206 : 2 : iiSubsLem.d_conc = eqs;
207 [ - + ]: 2 : if (TraceIsOn("strings-lemma-debug"))
208 : : {
209 [ - - ]: 0 : Trace("strings-lemma-debug")
210 : 0 : << "Strings::Infer " << iiSubsLem << std::endl;
211 [ - - ]: 0 : Trace("strings-lemma-debug")
212 : 0 : << "Strings::Infer Alternate : " << eqs << std::endl;
213 : : }
214 [ + - ]: 2 : Trace("strings-infer-debug") << "...as symbolic lemma" << std::endl;
215 : 2 : addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(iiSubsLem)));
216 : 2 : return;
217 : : }
218 [ - + ]: 90417 : if (TraceIsOn("strings-lemma-debug"))
219 : : {
220 [ - - ]: 0 : for (const Node& u : unproc)
221 : : {
222 [ - - ]: 0 : Trace("strings-lemma-debug")
223 : 0 : << " non-trivial explanation : " << u << std::endl;
224 : : }
225 : : }
226 : : }
227 [ + - ]: 90417 : Trace("strings-infer-debug") << "...as fact" << std::endl;
228 : : // add to pending to be processed as a fact
229 : 90417 : addPendingFact(std::unique_ptr<InferInfo>(new InferInfo(ii)));
230 : : }
231 : :
232 : 4789 : bool InferenceManager::sendSplit(Node a, Node b, InferenceId infer, bool preq)
233 : : {
234 : 9578 : Node eq = a.eqNode(b);
235 : 4789 : eq = rewrite(eq);
236 [ - + ]: 4789 : if (eq.isConst())
237 : : {
238 : 0 : return false;
239 : : }
240 : 4789 : NodeManager* nm = nodeManager();
241 : 4789 : InferInfo iiSplit(infer);
242 : 4789 : iiSplit.d_sim = this;
243 : 4789 : iiSplit.d_conc = nm->mkNode(Kind::OR, eq, nm->mkNode(Kind::NOT, eq));
244 : 4789 : addPendingPhaseRequirement(eq, preq);
245 : 4789 : addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(iiSplit)));
246 : 4789 : return true;
247 : : }
248 : :
249 : 1426960 : void InferenceManager::addToExplanation(Node a,
250 : : Node b,
251 : : std::vector<Node>& exp) const
252 : : {
253 [ + + ]: 1426960 : if (a != b)
254 : : {
255 : : // prefer having constants on the RHS, which helps proof reconstruction
256 [ + + ][ + - ]: 620689 : if (a.isConst() && !b.isConst())
[ + + ]
257 : : {
258 : 4396 : Node tmp = a;
259 : 2198 : a = b;
260 : 2198 : b = tmp;
261 : : }
262 [ + - ]: 1241380 : Trace("strings-explain")
263 : 620689 : << "Add to explanation : " << a << " == " << b << std::endl;
264 [ - + ][ - + ]: 620689 : Assert(d_state.areEqual(a, b));
[ - - ]
265 : 620689 : exp.push_back(a.eqNode(b));
266 : : }
267 : 1426960 : }
268 : :
269 : 0 : void InferenceManager::addToExplanation(Node lit, std::vector<Node>& exp) const
270 : : {
271 [ - - ]: 0 : if (!lit.isNull())
272 : : {
273 : 0 : Assert(!lit.isConst());
274 : 0 : exp.push_back(lit);
275 : : }
276 : 0 : }
277 : :
278 : 8595180 : bool InferenceManager::hasProcessed() const
279 : : {
280 [ + + ][ + + ]: 8595180 : return d_state.isInConflict() || hasPending();
281 : : }
282 : :
283 : 132 : void InferenceManager::markInactive(Node n, ExtReducedId id, bool contextDepend)
284 : : {
285 : 132 : d_extt.markInactive(n, id, contextDepend);
286 : 132 : }
287 : :
288 : 3442 : void InferenceManager::processConflict(const InferInfo& ii)
289 : : {
290 [ - + ][ - + ]: 3442 : Assert(!d_state.isInConflict());
[ - - ]
291 [ + + ]: 3442 : if (ii.getId() == InferenceId::STRINGS_PREFIX_CONFLICT)
292 : : {
293 : 740 : bool isSuf = ii.d_idRev;
294 : : // The shape of prefix conflicts is P1? ^ P2? ^ (= x y)?
295 : : // where if applicable:
296 : : // P1 implies a prefix on string x,
297 : : // P2 implies a (conflicting) prefix on string y.
298 : : // See EqcInfo::mkMergeConflict.
299 [ + - ]: 1480 : Trace("strings-prefix-min") << "Minimize prefix conflict " << ii.d_premises
300 : 740 : << ", isSuf=" << isSuf << std::endl;
301 : 740 : size_t npremises = ii.d_premises.size();
302 : 740 : Node eq = ii.d_premises[npremises - 1];
303 : : // if we included an equality, we will try to minimize its explanation
304 [ + - ]: 740 : if (eq.getKind() == Kind::EQUAL)
305 : : {
306 : 740 : InferInfo iim(InferenceId::STRINGS_PREFIX_CONFLICT_MIN);
307 [ - - ]: 2220 : Node pft[2] = {eq[0], eq[1]};
308 [ + + ]: 1103 : for (size_t i = 0; i < (npremises - 1); i++)
309 : : {
310 [ + - ]: 363 : if (ii.d_premises[i].getKind() == Kind::STRING_IN_REGEXP)
311 : : {
312 [ + + ]: 363 : size_t eindex = ii.d_premises[i][0] == eq[0] ? 0 : 1;
313 [ - + ][ - + ]: 363 : Assert(ii.d_premises[i][0] == eq[eindex]);
[ - - ]
314 : : // the basis of prefix for eq[eindex] is the RE of this premise
315 : 363 : pft[eindex] = ii.d_premises[i][1];
316 : : }
317 : : // include it in the explanation
318 : 363 : iim.d_premises.push_back(ii.d_premises[i]);
319 : : }
320 [ + - ]: 1480 : Trace("strings-prefix-min")
321 : 740 : << "Prefix terms: " << pft[0] << " / " << pft[1] << std::endl;
322 [ + + ][ - - ]: 3700 : Node pfv[2];
323 [ + + ]: 2220 : for (size_t i = 0; i < 2; i++)
324 : : {
325 : 1480 : pfv[i] = utils::getConstantEndpoint(pft[i], isSuf);
326 : : }
327 [ + - ]: 1480 : Trace("strings-prefix-min")
328 : 740 : << "Prefixes: " << pfv[0] << " / " << pfv[1] << std::endl;
329 [ + + ]: 2076 : for (size_t i = 0; i < 2; i++)
330 : : {
331 : 1408 : if (pft[1 - i] == eq[1 - i] && pft[i] != eq[i])
332 : : {
333 : : // if the other side is justified by itself and we are justified
334 : : // externally, we can try to minimize the explanation of this
335 : : // get the minimal conflicting prefix
336 : 359 : std::vector<TNode> assumptions;
337 : 359 : explain(eq, assumptions);
338 : 359 : std::map<TNode, TNode> emap = getExplanationMap(assumptions);
339 : : Node mexp =
340 : 718 : mkPrefixExplainMin(eq[i], pfv[i], assumptions, emap, isSuf);
341 : : // if we minimized the conflict, process it
342 [ + + ]: 359 : if (!mexp.isNull())
343 : : {
344 : : // must flatten here
345 : 72 : utils::flattenOp(Kind::AND, mexp, iim.d_premises);
346 : 72 : iim.d_conc = ii.d_conc;
347 : 72 : processConflict(iim);
348 : 72 : return;
349 : : }
350 : : }
351 : : }
352 : : }
353 : : // otherwise if we fail to minimize, process the original
354 : : }
355 : : // setup the fact to reproduce the proof in the call below
356 [ + + ]: 3370 : if (d_ipcl != nullptr)
357 : : {
358 : 1590 : d_ipcl->notifyLemma(ii);
359 : : }
360 : : // make the trust node
361 [ + + ]: 3370 : TrustNode tconf = mkConflictExp(ii.d_premises, d_ipcl.get());
362 [ - + ][ - + ]: 3370 : Assert(tconf.getKind() == TrustNodeKind::CONFLICT);
[ - - ]
363 [ + - ][ - - ]: 6740 : Trace("strings-assert") << "(assert (not " << tconf.getNode()
364 [ - + ]: 3370 : << ")) ; conflict " << ii.getId() << std::endl;
365 : : // send the trusted conflict
366 : 3370 : trustedConflict(tconf, ii.getId());
367 : : }
368 : :
369 : 87841 : void InferenceManager::processFact(InferInfo& ii, ProofGenerator*& pg)
370 : : {
371 [ + - ][ - - ]: 175682 : Trace("strings-assert") << "(assert (=> " << ii.getPremises(nodeManager())
372 [ - + ]: 87841 : << " " << ii.d_conc << ")) ; fact " << ii.getId()
373 : 87841 : << std::endl;
374 [ + - ]: 175682 : Trace("strings-lemma") << "Strings::Fact: " << ii.d_conc << " from "
375 [ - - ]: 87841 : << ii.getPremises(nodeManager()) << " by "
376 [ - + ]: 87841 : << ii.getId() << std::endl;
377 [ + + ]: 87841 : if (d_ipc != nullptr)
378 : : {
379 : : // ensure the proof generator is ready to explain this fact in the
380 : : // current SAT context
381 : 37507 : d_ipc->notifyFact(ii);
382 [ + - ]: 37507 : pg = d_ipc.get();
383 : : }
384 : : // ensure facts are for rewritten terms
385 [ + - ]: 87841 : if (Configuration::isAssertionBuild())
386 : : {
387 [ + + ]: 175682 : Node atom = ii.d_conc.getKind() == Kind::NOT ? ii.d_conc[0] : ii.d_conc;
388 [ + + ]: 87841 : if (atom.getKind() == Kind::EQUAL)
389 : : {
390 [ - + ][ - + ]: 87643 : Assert(rewrite(atom[0])==atom[0]);
[ - - ]
391 [ - + ][ - + ]: 87643 : Assert(rewrite(atom[1])==atom[1]);
[ - - ]
392 : : }
393 : : else
394 : : {
395 [ - + ][ - + ]: 198 : Assert(rewrite(atom)==atom);
[ - - ]
396 : : }
397 : : }
398 : 87841 : }
399 : :
400 : 43554 : TrustNode InferenceManager::processLemma(InferInfo& ii, LemmaProperty& p)
401 : : {
402 [ - + ][ - + ]: 43554 : Assert(!ii.isTrivial());
[ - - ]
403 [ - + ][ - + ]: 43554 : Assert(!ii.isConflict());
[ - - ]
404 : : // set up the explanation and no-explanation
405 : 87108 : std::vector<Node> exp;
406 [ + + ]: 137684 : for (const Node& ec : ii.d_premises)
407 : : {
408 : 94130 : utils::flattenOp(Kind::AND, ec, exp);
409 : : }
410 : 87108 : std::vector<Node> noExplain;
411 [ - + ]: 43554 : if (!options().strings.stringRExplainLemmas)
412 : : {
413 : : // if we aren't regressing the explanation, we add all literals to
414 : : // noExplain and ignore ii.d_ant.
415 : 0 : noExplain.insert(noExplain.end(), exp.begin(), exp.end());
416 : : }
417 : : else
418 : : {
419 : : // otherwise, the no-explain literals are those provided
420 [ + + ]: 47577 : for (const Node& ecn : ii.d_noExplain)
421 : : {
422 : 4023 : utils::flattenOp(Kind::AND, ecn, noExplain);
423 : : }
424 : : }
425 : : // ensure that the proof generator is ready to explain the final conclusion
426 : : // of the lemma (ii.d_conc).
427 [ + + ]: 43554 : if (d_ipcl != nullptr)
428 : : {
429 : 16650 : d_ipcl->notifyLemma(ii);
430 : : }
431 [ + + ]: 43554 : TrustNode tlem = mkLemmaExp(ii.d_conc, exp, noExplain, d_ipcl.get());
432 [ + - ][ - + ]: 87108 : Trace("strings-pending") << "Process pending lemma : " << tlem.getNode()
[ - - ]
433 : 43554 : << std::endl;
434 : :
435 : : // Process the side effects of the inference info.
436 : : // Register the new skolems from this inference. We register them here
437 : : // (lazily), since this is the moment when we have decided to process the
438 : : // inference.
439 : 2576 : for (const std::pair<const LengthStatus, std::vector<Node> >& sks :
440 [ + + ]: 48706 : ii.d_skolems)
441 : : {
442 [ + + ]: 5152 : for (const Node& n : sks.second)
443 : : {
444 : 2576 : d_termReg.registerTermAtomic(n, sks.first);
445 : : }
446 : : }
447 [ + + ]: 43554 : if (ii.getId() == InferenceId::STRINGS_REDUCTION)
448 : : {
449 : 4442 : p |= LemmaProperty::NEEDS_JUSTIFY;
450 : : }
451 : : // send phase requirements
452 [ + + ]: 45515 : for (const std::pair<const Node, bool>& pp : ii.d_pendingPhase)
453 : : {
454 : 1961 : Node ppr = rewrite(pp.first);
455 : 1961 : addPendingPhaseRequirement(ppr, pp.second);
456 : : }
457 [ + - ][ - - ]: 87108 : Trace("strings-assert") << "(assert " << tlem.getNode() << ") ; lemma "
458 [ - + ]: 43554 : << ii.getId() << std::endl;
459 [ + - ][ - - ]: 87108 : Trace("strings-lemma") << "Strings::Lemma: " << tlem.getNode() << " by "
460 [ - + ]: 43554 : << ii.getId() << std::endl;
461 : 87108 : return tlem;
462 : : }
463 : :
464 : 359 : std::map<TNode, TNode> InferenceManager::getExplanationMap(
465 : : const std::vector<TNode>& assumptions)
466 : : {
467 : 359 : std::map<TNode, TNode> emap;
468 [ + + ]: 1286 : for (TNode e : assumptions)
469 : : {
470 [ + + ]: 927 : if (e.getKind() != Kind::EQUAL)
471 : : {
472 : : // skip non-equalities, which could be included if we internally
473 : : // concluded an equality as a fact from a non-equality
474 : 49 : continue;
475 : : }
476 [ + + ]: 2634 : for (size_t i = 0; i < 2; i++)
477 : : {
478 : 1756 : emap[e[i]] = e;
479 : : }
480 : : }
481 : 359 : return emap;
482 : : }
483 : 359 : Node InferenceManager::mkPrefixExplainMin(Node x,
484 : : Node prefix,
485 : : const std::vector<TNode>& assumptions,
486 : : const std::map<TNode, TNode>& emap,
487 : : bool isSuf)
488 : : {
489 [ - + ][ - + ]: 359 : Assert(prefix.isConst());
[ - - ]
490 [ + - ]: 718 : Trace("strings-prefix-min")
491 [ - - ]: 0 : << "mkPrefixExplainMin: " << x << " for " << (isSuf ? "suffix" : "prefix")
492 : 359 : << " " << prefix << std::endl;
493 [ + - ]: 359 : Trace("strings-prefix-min") << "- via: " << assumptions << std::endl;
494 : 718 : std::vector<TNode> minAssumptions;
495 : : // the current node(s) we are looking at
496 : 718 : std::vector<TNode> cc;
497 : 359 : cc.push_back(x);
498 : 359 : size_t pindex = 0;
499 : 718 : std::vector<Node> pchars = Word::getChars(prefix);
500 : 359 : std::map<TNode, TNode>::const_iterator it;
501 : 359 : bool isConflict = false;
502 [ + - ][ + + ]: 1419 : while (pindex < pchars.size() && !cc.empty())
[ + + ]
503 : : {
504 [ + - ]: 2564 : Trace("strings-prefix-min")
505 : 1282 : << " " << pindex << "/" << pchars.size() << ", " << cc << std::endl;
506 : 1282 : TNode c = cc.back();
507 : 1282 : cc.pop_back();
508 [ + + ]: 1282 : if (c.isConst())
509 : : {
510 : : // check for conflict
511 : 337 : std::vector<Node> cchars = Word::getChars(c);
512 : 337 : size_t cindex = 0;
513 [ + - ][ + + ]: 347 : while (pindex < pchars.size() && cindex < cchars.size())
[ + + ]
514 : : {
515 [ + + ]: 150 : size_t pii = isSuf ? (pchars.size() - 1) - pindex : pindex;
516 [ + + ]: 150 : size_t cii = isSuf ? (cchars.size() - 1) - cindex : cindex;
517 [ + + ]: 150 : if (cchars[cii] != pchars[pii])
518 : : {
519 [ + - ]: 280 : Trace("strings-prefix-min") << "...conflict at " << pindex
520 : 140 : << " while processing " << c << std::endl;
521 : 140 : isConflict = true;
522 : 140 : break;
523 : : }
524 : 10 : pindex++;
525 : 10 : cindex++;
526 : : }
527 [ + + ]: 337 : if (isConflict)
528 : : {
529 : 140 : break;
530 : : }
531 : 197 : continue;
532 : : }
533 : 945 : it = emap.find(c);
534 [ + + ]: 945 : if (it != emap.end())
535 : : {
536 : 857 : TNode ceq = it->second;
537 : : // do not continue if not already processed, which also avoids
538 : : // non-termination
539 : 857 : if (std::find(minAssumptions.begin(), minAssumptions.end(), ceq)
540 [ + + ]: 1714 : == minAssumptions.end())
541 : : {
542 [ - + ][ - + ]: 560 : Assert(ceq.getKind() == Kind::EQUAL);
[ - - ]
543 : 560 : Assert(ceq[0] == c || ceq[1] == c);
544 : : // add to explanation and look at the term it is equal to
545 : 560 : minAssumptions.push_back(ceq);
546 [ + + ]: 1120 : TNode oc = ceq[ceq[0] == c ? 1 : 0];
547 : 560 : cc.push_back(oc);
548 : 560 : continue;
549 : : }
550 : : }
551 : : // we don't know what it is equal to
552 : : // if it is a concatenation, try to recurse into children
553 [ + + ]: 385 : if (c.getKind() == Kind::STRING_CONCAT)
554 : : {
555 [ + + ]: 1093 : for (size_t i = 0, nchild = c.getNumChildren(); i < nchild; i++)
556 : : {
557 : : // reverse if it is a prefix
558 [ + + ]: 790 : size_t ii = isSuf ? i : (nchild - 1) - i;
559 : 790 : cc.push_back(c[ii]);
560 : : }
561 : 303 : continue;
562 : : }
563 [ + - ]: 82 : Trace("strings-prefix-min") << "-> no explanation for " << c << std::endl;
564 : 82 : break;
565 : : }
566 [ + + ][ + + ]: 359 : if (isConflict && minAssumptions.size() < assumptions.size())
[ + + ]
567 : : {
568 [ + - ]: 144 : Trace("strings-prefix-min")
569 : 72 : << "-> min-explained: " << minAssumptions << std::endl;
570 [ + - ]: 144 : Trace("strings-exp-min-stats")
571 : 0 : << "Min-explain (prefix) " << minAssumptions.size() << " / "
572 : 72 : << assumptions.size() << std::endl;
573 : 72 : return nodeManager()->mkAnd(minAssumptions);
574 : : }
575 : 287 : return Node::null();
576 : : }
577 : :
578 : : } // namespace strings
579 : : } // namespace theory
580 : : } // namespace cvc5::internal
|
