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 theory of strings.
11 : : */
12 : :
13 : : #include "theory/strings/theory_strings.h"
14 : :
15 : : #include "expr/attribute.h"
16 : : #include "expr/bound_var_manager.h"
17 : : #include "expr/kind.h"
18 : : #include "expr/sequence.h"
19 : : #include "options/smt_options.h"
20 : : #include "options/strings_options.h"
21 : : #include "options/theory_options.h"
22 : : #include "printer/smt2/smt2_printer.h"
23 : : #include "smt/logic_exception.h"
24 : : #include "theory/decision_manager.h"
25 : : #include "theory/ext_theory.h"
26 : : #include "theory/rewriter.h"
27 : : #include "theory/strings/theory_strings_utils.h"
28 : : #include "theory/strings/type_enumerator.h"
29 : : #include "theory/strings/word.h"
30 : : #include "theory/theory_model.h"
31 : : #include "theory/valuation.h"
32 : :
33 : : using namespace std;
34 : : using namespace cvc5::context;
35 : : using namespace cvc5::internal::kind;
36 : :
37 : : namespace cvc5::internal {
38 : : namespace theory {
39 : : namespace strings {
40 : :
41 : 51092 : TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation)
42 : : : Theory(THEORY_STRINGS, env, out, valuation),
43 : 51092 : d_notify(*this),
44 : 51092 : d_statistics(statisticsRegistry()),
45 : 51092 : d_state(env, d_valuation),
46 : 51092 : d_termReg(env, *this, d_state),
47 : 51092 : d_arithEntail(
48 : : env.getNodeManager(),
49 [ + + ]: 51092 : options().strings.stringRecArithApprox ? env.getRewriter() : nullptr,
50 : 51092 : options().strings.stringRecArithApprox),
51 : 51092 : d_strEntail(d_env.getRewriter(), d_arithEntail),
52 : 102184 : d_rewriter(env.getNodeManager(),
53 : 51092 : d_arithEntail,
54 : 51092 : d_strEntail,
55 : : &d_statistics.d_rewrites,
56 : : d_termReg.getAlphabetCardinality()),
57 [ + - ]: 102184 : d_eagerSolver(options().strings.stringEagerSolver
58 : 51092 : ? new EagerSolver(env, d_state)
59 : : : nullptr),
60 : 51092 : d_extTheoryCb(),
61 : 51092 : d_im(env, *this, d_state, d_termReg, d_extTheory, d_statistics),
62 : 51092 : d_extTheory(env, d_extTheoryCb, d_im),
63 : : // the checker depends on the cardinality of the alphabet
64 : 51092 : d_checker(nodeManager(), d_termReg.getAlphabetCardinality()),
65 : 51092 : d_bsolver(env, d_state, d_im, d_termReg),
66 : 51092 : d_csolver(env, d_state, d_im, d_termReg, d_bsolver),
67 : 51092 : d_esolver(env,
68 : 51092 : d_state,
69 : 51092 : d_im,
70 : 51092 : d_termReg,
71 : 51092 : d_rewriter,
72 : 51092 : d_bsolver,
73 : 51092 : d_csolver,
74 : 51092 : d_extTheory,
75 : 51092 : d_statistics),
76 : 51092 : d_psolver(env, d_state, d_im, d_termReg, d_bsolver, d_csolver),
77 : 51092 : d_asolver(env,
78 : 51092 : d_state,
79 : 51092 : d_im,
80 : 51092 : d_termReg,
81 : 51092 : d_bsolver,
82 : 51092 : d_csolver,
83 : 51092 : d_esolver,
84 : 51092 : d_extTheory),
85 : 51092 : d_rsolver(
86 : 51092 : env, d_state, d_im, d_termReg, d_csolver, d_esolver, d_statistics),
87 : 102184 : d_regexp_elim(
88 : : env,
89 : 51092 : options().strings.regExpElim == options::RegExpElimMode::AGG,
90 : 51092 : userContext()),
91 : 51092 : d_stringsFmf(env, valuation, d_termReg),
92 : 51092 : d_mcd(env, d_state, d_csolver),
93 : 51092 : d_strat(d_env),
94 : 51092 : d_absModelCounter(0),
95 : 51092 : d_strGapModelCounter(0),
96 : 51092 : d_cpacb(*this),
97 [ + + ][ + + ]: 61877 : d_psrewPg(env.isTheoryProofProducing()
[ - - ]
98 : : ? new TrustProofGenerator(
99 : 10785 : env, TrustId::STRINGS_PP_STATIC_REWRITE, {})
100 : 51092 : : nullptr)
101 : : {
102 : 51092 : d_termReg.finishInit(&d_im);
103 : :
104 : 51092 : d_zero = nodeManager()->mkConstInt(Rational(0));
105 : 51092 : d_one = nodeManager()->mkConstInt(Rational(1));
106 : 51092 : d_neg_one = nodeManager()->mkConstInt(Rational(-1));
107 : 51092 : d_true = nodeManager()->mkConst(true);
108 : 51092 : d_false = nodeManager()->mkConst(false);
109 : :
110 : : // set up the extended function callback
111 : 51092 : d_extTheoryCb.d_esolver = &d_esolver;
112 : :
113 : : // use the state object as the official theory state
114 : 51092 : d_theoryState = &d_state;
115 : : // use the inference manager as the official inference manager
116 : 51092 : d_inferManager = &d_im;
117 : 51092 : }
118 : :
119 : 101488 : TheoryStrings::~TheoryStrings() {}
120 : :
121 : 51092 : TheoryRewriter* TheoryStrings::getTheoryRewriter() { return &d_rewriter; }
122 : :
123 : 19899 : ProofRuleChecker* TheoryStrings::getProofChecker() { return &d_checker; }
124 : :
125 : 51092 : bool TheoryStrings::needsEqualityEngine(EeSetupInfo& esi)
126 : : {
127 : 51092 : esi.d_notify = &d_notify;
128 : 51092 : esi.d_name = "theory::strings::ee";
129 : 51092 : esi.d_notifyNewClass = true;
130 : 51092 : esi.d_notifyMerge = true;
131 : 51092 : esi.d_notifyDisequal = true;
132 : 51092 : return true;
133 : : }
134 : :
135 : 51092 : void TheoryStrings::finishInit()
136 : : {
137 [ - + ][ - + ]: 51092 : Assert(d_equalityEngine != nullptr);
[ - - ]
138 : :
139 : : // witness is used to eliminate str.from_code
140 : 51092 : d_valuation.setUnevaluatedKind(Kind::WITNESS);
141 : :
142 : 51092 : bool eagerEval = options().strings.stringEagerEval;
143 : : // The kinds we are treating as function application in congruence
144 : 51092 : d_equalityEngine->addFunctionKind(Kind::STRING_LENGTH, eagerEval);
145 : 51092 : d_equalityEngine->addFunctionKind(Kind::STRING_CONCAT, eagerEval);
146 : 51092 : d_equalityEngine->addFunctionKind(Kind::STRING_IN_REGEXP, eagerEval);
147 : 51092 : d_equalityEngine->addFunctionKind(Kind::STRING_TO_CODE, eagerEval);
148 : 51092 : d_equalityEngine->addFunctionKind(Kind::SEQ_UNIT, eagerEval);
149 : 51092 : d_equalityEngine->addFunctionKind(Kind::STRING_UNIT, false);
150 : : // `seq.nth` is not always defined, and so we do not evaluate it eagerly.
151 : 51092 : d_equalityEngine->addFunctionKind(Kind::SEQ_NTH, false);
152 : : // extended functions
153 : 51092 : d_equalityEngine->addFunctionKind(Kind::STRING_CONTAINS, eagerEval);
154 : 51092 : d_equalityEngine->addFunctionKind(Kind::STRING_LEQ, eagerEval);
155 : 51092 : d_equalityEngine->addFunctionKind(Kind::STRING_SUBSTR, eagerEval);
156 : 51092 : d_equalityEngine->addFunctionKind(Kind::STRING_UPDATE, eagerEval);
157 : 51092 : d_equalityEngine->addFunctionKind(Kind::STRING_ITOS, eagerEval);
158 : 51092 : d_equalityEngine->addFunctionKind(Kind::STRING_STOI, eagerEval);
159 : 51092 : d_equalityEngine->addFunctionKind(Kind::STRING_INDEXOF, eagerEval);
160 : 51092 : d_equalityEngine->addFunctionKind(Kind::STRING_INDEXOF_RE, eagerEval);
161 : 51092 : d_equalityEngine->addFunctionKind(Kind::STRING_REPLACE, eagerEval);
162 : 51092 : d_equalityEngine->addFunctionKind(Kind::STRING_REPLACE_ALL, eagerEval);
163 : 51092 : d_equalityEngine->addFunctionKind(Kind::STRING_REPLACE_RE, eagerEval);
164 : 51092 : d_equalityEngine->addFunctionKind(Kind::STRING_REPLACE_RE_ALL, eagerEval);
165 : 51092 : d_equalityEngine->addFunctionKind(Kind::STRING_REPLACE_ALL, eagerEval);
166 : 51092 : d_equalityEngine->addFunctionKind(Kind::STRING_TO_LOWER, eagerEval);
167 : 51092 : d_equalityEngine->addFunctionKind(Kind::STRING_TO_UPPER, eagerEval);
168 : 51092 : d_equalityEngine->addFunctionKind(Kind::STRING_REV, eagerEval);
169 : :
170 : : // memberships are not relevant for model building
171 : 51092 : d_valuation.setIrrelevantKind(Kind::STRING_IN_REGEXP);
172 : 51092 : d_valuation.setIrrelevantKind(Kind::STRING_LEQ);
173 : : // seq nth doesn't always evaluate
174 : 51092 : d_valuation.setSemiEvaluatedKind(Kind::SEQ_NTH);
175 : 51092 : }
176 : :
177 : 0 : std::string TheoryStrings::identify() const
178 : : {
179 : 0 : return std::string("TheoryStrings");
180 : : }
181 : :
182 : 2203527 : bool TheoryStrings::propagateLit(TNode literal)
183 : : {
184 [ + + ]: 2203527 : if (d_state.hasPendingConflict())
185 : : {
186 : : // pending conflict also implies we are done
187 : 1105 : return false;
188 : : }
189 : 2202422 : return d_im.propagateLit(literal);
190 : : }
191 : :
192 : 122372 : TrustNode TheoryStrings::explain(TNode literal)
193 : : {
194 [ + - ]: 122372 : Trace("strings-explain") << "explain called on " << literal << std::endl;
195 : 122372 : return d_im.explainLit(literal);
196 : : }
197 : :
198 : 50519 : void TheoryStrings::presolve()
199 : : {
200 [ + - ]: 101038 : Trace("strings-presolve")
201 : 0 : << "TheoryStrings::Presolving : get fmf options "
202 [ - - ]: 50519 : << (options().strings.stringFMF ? "true" : "false") << std::endl;
203 : 50519 : d_strat.initializeStrategy();
204 : :
205 : : // if strings fmf is enabled, register the strategy
206 [ + + ]: 50519 : if (options().strings.stringFMF)
207 : : {
208 : 85 : d_stringsFmf.presolve();
209 : : // This strategy is local to a check-sat call, since we refresh the strategy
210 : : // on every call to presolve.
211 : 85 : d_im.getDecisionManager()->registerStrategy(
212 : : DecisionManager::STRAT_STRINGS_SUM_LENGTHS,
213 : : d_stringsFmf.getDecisionStrategy(),
214 : : DecisionManager::STRAT_SCOPE_LOCAL_SOLVE);
215 : : }
216 [ + - ]: 50519 : Trace("strings-presolve") << "Finished presolve" << std::endl;
217 : 50519 : }
218 : :
219 : : /////////////////////////////////////////////////////////////////////////////
220 : : // MODEL GENERATION
221 : : /////////////////////////////////////////////////////////////////////////////
222 : :
223 : 15427 : bool TheoryStrings::collectModelValues(TheoryModel* m,
224 : : const std::set<Node>& termSet)
225 : : {
226 : 15427 : d_absModelCounter = 0;
227 : 15427 : d_strGapModelCounter = 0;
228 [ - + ]: 15427 : if (TraceIsOn("strings-debug-model"))
229 : : {
230 [ - - ]: 0 : Trace("strings-debug-model")
231 : 0 : << "TheoryStrings::collectModelValues" << std::endl;
232 [ - - ]: 0 : Trace("strings-debug-model") << "Equivalence classes are:" << std::endl;
233 : 0 : Trace("strings-debug-model") << debugPrintStringsEqc() << std::endl;
234 [ - - ]: 0 : Trace("strings-debug-model") << "Extended functions are:" << std::endl;
235 : 0 : Trace("strings-debug-model") << d_esolver.debugPrintModel() << std::endl;
236 : : }
237 [ + - ]: 15427 : Trace("strings-model") << "TheoryStrings::collectModelValues" << std::endl;
238 : : // Collects representatives by types and orders sequence types by how nested
239 : : // they are
240 : 15427 : std::map<TypeNode, std::unordered_set<Node>> repSet;
241 : 15427 : std::unordered_set<TypeNode> toProcess;
242 : : // Generate model
243 : 15427 : ModelCons* mc = d_state.getModelConstructor();
244 [ - + ][ - + ]: 15427 : Assert(mc != nullptr);
[ - - ]
245 : : // get the relevant string equivalence classes
246 : 15427 : std::vector<Node> auxEq;
247 : 15427 : mc->getStringRepresentativesFrom(termSet, toProcess, repSet, auxEq);
248 : : // assert the auxiliary equalities
249 [ - + ]: 15427 : for (const Node& aeq : auxEq)
250 : : {
251 : 0 : Assert(aeq.getKind() == Kind::EQUAL);
252 [ - - ]: 0 : Trace("strings-model") << "-> auxiliary equality " << aeq << std::endl;
253 [ - - ]: 0 : if (!m->assertEquality(aeq[0], aeq[1], true))
254 : : {
255 : 0 : Unreachable() << "TheoryStrings::collectModelValues: Inconsistent "
256 : 0 : "auxiliary equality"
257 : 0 : << std::endl;
258 : : return false;
259 : : }
260 : : }
261 : :
262 [ + + ]: 17634 : while (!toProcess.empty())
263 : : {
264 : : // Pick one of the remaining types to collect model values for
265 : 2213 : TypeNode tn = *toProcess.begin();
266 [ + + ]: 2213 : if (!collectModelInfoType(tn, toProcess, repSet, m))
267 : : {
268 : 6 : return false;
269 : : }
270 [ + + ]: 2213 : }
271 : :
272 : 15421 : return true;
273 : 15427 : }
274 : :
275 : : /**
276 : : * Object to sort by the value of pairs in the write model returned by the
277 : : * sequences array solver.
278 : : */
279 : : struct SortSeqIndex
280 : : {
281 : 32 : SortSeqIndex() {}
282 : : /** the comparison */
283 : 0 : bool operator()(const std::pair<Node, Node>& i,
284 : : const std::pair<Node, Node>& j)
285 : : {
286 : 0 : Assert(i.first.isConst() && i.first.getType().isInteger()
287 : : && j.first.isConst() && j.first.getType().isInteger());
288 : 0 : return i.first.getConst<Rational>() < j.first.getConst<Rational>();
289 : : }
290 : : };
291 : :
292 : 2218 : bool TheoryStrings::collectModelInfoType(
293 : : TypeNode tn,
294 : : std::unordered_set<TypeNode>& toProcess,
295 : : const std::map<TypeNode, std::unordered_set<Node>>& repSet,
296 : : TheoryModel* m)
297 : : {
298 : : // Make sure that the model values for the element type of sequences are
299 : : // computed first
300 [ + + ][ + + ]: 2218 : if (tn.isSequence() && tn.getSequenceElementType().isSequence())
[ + + ][ + + ]
[ - - ]
301 : : {
302 : 15 : TypeNode tnElem = tn.getSequenceElementType();
303 : 15 : if (toProcess.find(tnElem) != toProcess.end()
304 [ + + ][ + + ]: 30 : && !collectModelInfoType(tnElem, toProcess, repSet, m))
[ + + ][ + + ]
[ - - ]
305 : : {
306 : 2 : return false;
307 : : }
308 [ + + ]: 15 : }
309 : 2216 : toProcess.erase(tn);
310 : :
311 : 2216 : SEnumLenSet sels;
312 : 2216 : ModelCons* mc = d_state.getModelConstructor();
313 : : // get partition of strings of equal lengths for the representatives of the
314 : : // current type
315 : 2216 : std::vector<std::vector<Node>> col;
316 : 2216 : std::vector<Node> lts;
317 : 2216 : const std::vector<Node> repVec(repSet.at(tn).begin(), repSet.at(tn).end());
318 : 2216 : mc->separateByLength(m, repVec, col, lts);
319 [ - + ][ - + ]: 2216 : Assert(col.size() == lts.size());
[ - - ]
320 : : // indices in col that have lengths that are too big to represent
321 : 2216 : std::unordered_set<size_t> oobIndices;
322 : :
323 : 2216 : NodeManager* nm = nodeManager();
324 : 2216 : std::map<Node, Node> processed;
325 : : // step 1 : get all values for known lengths
326 : 2216 : std::vector<Node> lts_values;
327 : : // mapping from lengths used to the index in col that used that length
328 : 2216 : std::map<size_t, size_t> values_used;
329 : : // A list of pairs of indices in col that used the same length term. We use
330 : : // this as candidates to add length splitting on below (STRINGS_CMI_SPLIT),
331 : : // which is used as a safeguard when model construction fails unexpectedly
332 : : // by running out of values.
333 : 2216 : std::vector<std::pair<size_t, size_t>> len_splits;
334 [ + + ]: 12649 : for (size_t i = 0, csize = col.size(); i < csize; i++)
335 : : {
336 [ + - ]: 10433 : Trace("strings-model") << "Checking length for { " << col[i];
337 [ + - ]: 10433 : Trace("strings-model") << " } (length is " << lts[i] << ")" << std::endl;
338 : 10433 : Node len_value = lts[i];
339 [ - + ]: 10433 : if (len_value.isNull())
340 : : {
341 : 0 : lts_values.push_back(Node::null());
342 : : }
343 : 10433 : else if (len_value.getConst<Rational>()
344 [ + + ]: 20866 : > options().strings.stringsModelMaxLength)
345 : : {
346 : : // note that we give a warning instead of throwing logic exception if we
347 : : // cannot construct the string, these are then assigned witness terms
348 : : // below
349 : 68 : warning()
350 : 136 : << "The model was computed to have strings of length " << len_value
351 : : << ". Based on the current value of option --strings-model-max-len, "
352 : 68 : "we only allow strings up to length "
353 : 68 : << options().strings.stringsModelMaxLength << std::endl;
354 : 68 : oobIndices.insert(i);
355 : 68 : lts_values.push_back(len_value);
356 : : }
357 : : else
358 : : {
359 : : std::size_t lvalue =
360 : 10365 : len_value.getConst<Rational>().getNumerator().toUnsignedInt();
361 : 10365 : auto itvu = values_used.find(lvalue);
362 [ + + ]: 10365 : if (itvu == values_used.end())
363 : : {
364 : 8434 : values_used[lvalue] = i;
365 : : }
366 : : else
367 : : {
368 : 1931 : len_splits.emplace_back(i, itvu->second);
369 : : }
370 : 10365 : lts_values.push_back(len_value);
371 : : }
372 : 10433 : }
373 : : ////step 2 : assign arbitrary values for unknown lengths?
374 : : // confirmed by calculus invariant, see paper
375 [ + - ]: 2216 : Trace("strings-model") << "Assign to equivalence classes..." << std::endl;
376 : 2216 : std::map<Node, Node> pure_eq_assign;
377 : : // if we are using the sequences array solver, get the connected sequences
378 : 2216 : const std::map<Node, Node>* conSeq = nullptr;
379 : 2216 : std::map<Node, Node>::const_iterator itcs;
380 [ + + ]: 2216 : if (options().strings.seqArray != options::SeqArrayMode::NONE)
381 : : {
382 : 62 : conSeq = &d_asolver.getConnectedSequences();
383 : : }
384 : : // step 3 : assign values to equivalence classes that are pure variables
385 [ + + ]: 12629 : for (size_t i = 0, csize = col.size(); i < csize; i++)
386 : : {
387 : 10419 : bool wasOob = (oobIndices.find(i) != oobIndices.end());
388 : 10419 : std::vector<Node> pure_eq;
389 : 10419 : Node lenValue = lts_values[i];
390 [ + - ]: 20838 : Trace("strings-model") << "Considering " << col[i].size()
391 : 0 : << " equivalence classes of type " << tn
392 : 10419 : << " for length " << lenValue << std::endl;
393 [ + + ]: 25421 : for (const Node& eqc : col[i])
394 : : {
395 [ + - ]: 15002 : Trace("strings-model") << "- eqc: " << eqc << std::endl;
396 : : // check if col[i][j] has only variables
397 [ + + ]: 15002 : if (eqc.isConst())
398 : : {
399 : 9004 : processed[eqc] = eqc;
400 : : // Make sure that constants are asserted to the theory model that we
401 : : // are building. It is possible that new constants were introduced by
402 : : // the eager evaluation in the equality engine. These terms are missing
403 : : // in the term set and, as a result, are skipped when the equality
404 : : // engine is asserted to the theory model.
405 : 9004 : m->getEqualityEngine()->addTerm(eqc);
406 : :
407 : : // For sequences constants, also add the elements (expanding elements
408 : : // as necessary)
409 [ + + ]: 9004 : if (eqc.getType().isSequence())
410 : : {
411 : 365 : const std::vector<Node> elems = eqc.getConst<Sequence>().getVec();
412 : 365 : std::vector<TNode> visit(elems.begin(), elems.end());
413 [ + + ]: 574 : for (size_t j = 0; j < visit.size(); j++)
414 : : {
415 : 209 : Node se = visit[j];
416 [ - + ][ - + ]: 209 : Assert(se.isConst());
[ - - ]
417 [ + + ]: 209 : if (se.getType().isSequence())
418 : : {
419 : 16 : const std::vector<Node> selems = se.getConst<Sequence>().getVec();
420 : 16 : visit.insert(visit.end(), selems.begin(), selems.end());
421 : 16 : }
422 : 209 : m->getEqualityEngine()->addTerm(se);
423 : 209 : }
424 : 365 : }
425 : :
426 [ + - ]: 9004 : Trace("strings-model") << "-> constant" << std::endl;
427 : 12372 : continue;
428 : 9004 : }
429 : 5998 : std::vector<Node> nfe = mc->getNormalForm(eqc);
430 [ + + ]: 5998 : if (nfe.size() != 1)
431 : : {
432 : : // will be assigned via a concatenation of normal form eqc
433 [ + - ]: 6634 : Trace("strings-model")
434 : 3317 : << " -> will be assigned by normal form " << nfe << std::endl;
435 : 3317 : continue;
436 : : }
437 : : // check if the length is too big to represent
438 [ + + ]: 2681 : if (wasOob)
439 : : {
440 : 51 : processed[eqc] = eqc;
441 [ + - ][ + - ]: 51 : Assert(!lenValue.isNull() && lenValue.isConst());
[ - + ][ - + ]
[ - - ]
442 : : // make the abstract value (witness ((x String)) (= (str.len x)
443 : : // lenValue))
444 : : Node w = utils::mkAbstractStringValueForLength(
445 : 102 : eqc, lenValue, d_absModelCounter);
446 : 51 : d_absModelCounter++;
447 [ + - ]: 102 : Trace("strings-model")
448 : 51 : << "-> length out of bounds, assign abstract " << w << std::endl;
449 [ - + ]: 51 : if (!m->assertEquality(eqc, w, true))
450 : : {
451 : 0 : Unreachable() << "TheoryStrings::collectModelInfoType: Inconsistent "
452 : 0 : "abstract equality"
453 : 0 : << std::endl;
454 : : return false;
455 : : }
456 : 51 : continue;
457 [ - + ]: 51 : }
458 : : // ensure we have decided on length value at this point
459 [ - + ]: 2630 : if (lenValue.isNull())
460 : : {
461 : : // start with length two (other lengths have special precendence)
462 : 0 : size_t lvalue = 2;
463 [ - - ]: 0 : while (values_used.find(lvalue) != values_used.end())
464 : : {
465 : 0 : lvalue++;
466 : : }
467 [ - - ]: 0 : Trace("strings-model")
468 : 0 : << "*** Decide to make length of " << lvalue << std::endl;
469 : 0 : lenValue = nm->mkConstInt(Rational(lvalue));
470 : 0 : values_used[lvalue] = i;
471 : : }
472 : : // is it an equivalence class with a seq.unit term?
473 : 2630 : Node assignedValue;
474 [ - + ]: 2630 : if (nfe[0].getKind() == Kind::STRING_UNIT)
475 : : {
476 : : // str.unit is applied to integers, where we are guaranteed the model
477 : : // exists. We preempitively get the model value here, so that we
478 : : // avoid repeated model values for strings.
479 : 0 : Node val = d_valuation.getCandidateModelValue(nfe[0][0]);
480 : 0 : assignedValue = utils::mkUnit(eqc.getType(), val);
481 : 0 : assignedValue = rewrite(assignedValue);
482 [ - - ]: 0 : Trace("strings-model")
483 : 0 : << "-> assign via str.unit: " << assignedValue << std::endl;
484 : 0 : }
485 [ + + ]: 2630 : else if (nfe[0].getKind() == Kind::SEQ_UNIT)
486 : : {
487 [ + + ]: 156 : if (nfe[0][0].getType().isStringLike())
488 : : {
489 : : // By this point, we should have assigned model values for the
490 : : // elements of this sequence type because of the check in the
491 : : // beginning of this method
492 : 16 : Node argVal = m->getRepresentative(nfe[0][0]);
493 [ - + ][ - + ]: 8 : Assert(nfe[0].getKind() == Kind::SEQ_UNIT);
[ - - ]
494 : 8 : assignedValue = utils::mkUnit(eqc.getType(), argVal);
495 : 8 : }
496 : : else
497 : : {
498 : : // Otherwise, we use the term itself. We cannot get the model
499 : : // value of this term, since it might not be available yet, as
500 : : // it may belong to a theory that has not built its model yet.
501 : : // Hence, we assign a (non-constant) skeleton (seq.unit argVal).
502 : 148 : assignedValue = nfe[0];
503 : : }
504 : 156 : assignedValue = rewrite(assignedValue);
505 [ + - ]: 312 : Trace("strings-model")
506 : 156 : << "-> assign via seq.unit: " << assignedValue << std::endl;
507 : : }
508 [ + + ][ + + ]: 2474 : else if (d_termReg.hasStringCode() && lenValue == d_one)
[ + + ]
509 : : {
510 : : // It has a code and the length of these equivalence classes are one.
511 : : // Note this code is solely for strings, not sequences.
512 : 1491 : EqcInfo* eip = d_state.getOrMakeEqcInfo(eqc, false);
513 [ + - ][ + + ]: 1491 : if (eip && !eip->d_codeTerm.get().isNull())
[ + + ]
514 : : {
515 : : // its value must be equal to its code
516 : 1312 : Node ct = nm->mkNode(Kind::STRING_TO_CODE, eip->d_codeTerm.get());
517 : 1312 : Node ctv = d_valuation.getCandidateModelValue(ct);
518 : : unsigned cvalue =
519 : 1312 : ctv.getConst<Rational>().getNumerator().toUnsignedInt();
520 [ + - ]: 1312 : Trace("strings-model") << "(code: " << cvalue << ") ";
521 : 1312 : std::vector<unsigned> vec;
522 : 1312 : vec.push_back(cvalue);
523 : 1312 : assignedValue = nm->mkConst(String(vec));
524 [ + - ]: 2624 : Trace("strings-model")
525 : 1312 : << "-> assign via str.code: " << assignedValue << std::endl;
526 : 1312 : }
527 : : }
528 [ + + ]: 983 : else if (options().strings.seqArray != options::SeqArrayMode::NONE)
529 : : {
530 : 100 : TypeNode eqcType = eqc.getType();
531 : : // determine skeleton based on the write model, if it exists
532 : 100 : const std::map<Node, Node>& writeModel = d_asolver.getWriteModel(eqc);
533 [ + + ]: 100 : if (!writeModel.empty())
534 : : {
535 [ + - ]: 64 : Trace("strings-model") << "Write model for " << eqc << " (type " << tn
536 : 32 : << ") is:" << std::endl;
537 : 32 : std::vector<std::pair<Node, Node>> writes;
538 : 32 : std::unordered_set<Node> usedWrites;
539 [ + + ]: 80 : for (const std::pair<const Node, Node>& w : writeModel)
540 : : {
541 [ + - ]: 48 : Trace("strings-model") << " " << w.first << " -> " << w.second;
542 : 48 : Node ivalue = d_valuation.getCandidateModelValue(w.first);
543 : 48 : Assert(ivalue.isConst() && ivalue.getType().isInteger());
544 : : // ignore if out of bounds
545 : 48 : Rational irat = ivalue.getConst<Rational>();
546 [ + + ][ + + ]: 48 : if (irat.sgn() == -1 || irat >= lenValue.getConst<Rational>())
[ + + ]
547 : : {
548 [ + - ]: 36 : Trace("strings-model")
549 : 18 : << " (index " << irat << " out of bounds)" << std::endl;
550 : 18 : continue;
551 : : }
552 [ + + ]: 30 : if (usedWrites.find(ivalue) != usedWrites.end())
553 : : {
554 [ + - ]: 4 : Trace("strings-model")
555 : 2 : << " (index " << irat << " already written)" << std::endl;
556 : 2 : continue;
557 : : }
558 [ + - ]: 28 : Trace("strings-model") << " (index " << irat << ")" << std::endl;
559 : 28 : usedWrites.insert(ivalue);
560 : 56 : Node wsunit = utils::mkUnit(eqcType, w.second);
561 : 28 : writes.emplace_back(ivalue, wsunit);
562 [ + + ][ + + ]: 68 : }
563 : : // sort based on index value
564 : 32 : SortSeqIndex ssi;
565 : 32 : std::sort(writes.begin(), writes.end(), ssi);
566 : 32 : std::vector<Node> cc;
567 : 32 : uint32_t currIndex = 0;
568 [ + + ]: 92 : for (size_t w = 0, wsize = writes.size(); w <= wsize; w++)
569 : : {
570 : : uint32_t nextIndex;
571 [ + + ]: 60 : if (w == writes.size())
572 : : {
573 : 32 : nextIndex =
574 : 32 : lenValue.getConst<Rational>().getNumerator().toUnsignedInt();
575 : : }
576 : : else
577 : : {
578 : 28 : Node windex = writes[w].first;
579 [ - + ][ - + ]: 28 : Assert(windex.getConst<Rational>()
[ - - ]
580 : : <= Rational(String::maxSize()));
581 : 28 : nextIndex =
582 : 28 : windex.getConst<Rational>().getNumerator().toUnsignedInt();
583 [ - + ][ - + ]: 28 : Assert(nextIndex >= currIndex);
[ - - ]
584 : 28 : }
585 [ + + ]: 60 : if (nextIndex > currIndex)
586 : : {
587 [ + - ]: 24 : Trace("strings-model") << "Make skeleton from " << currIndex
588 : 12 : << " ... " << nextIndex << std::endl;
589 : : // allocate arbitrary value to fill gap
590 [ - + ][ - + ]: 12 : Assert(conSeq != nullptr);
[ - - ]
591 : 12 : Node base = eqc;
592 : 12 : itcs = conSeq->find(eqc);
593 [ + + ]: 12 : if (itcs != conSeq->end())
594 : : {
595 : 4 : base = itcs->second;
596 : : }
597 : : // use a skeleton for the gap and not a concrete value, as we
598 : : // do not know how which values from the element type are
599 : : // allowable (i.e. unconstrained) to assign to the gap
600 : 12 : Node cgap = mkSkeletonFromBase(base, currIndex, nextIndex);
601 : 12 : cc.push_back(cgap);
602 : 12 : }
603 : : // then take read
604 [ + + ]: 60 : if (w < wsize)
605 : : {
606 : 28 : cc.push_back(writes[w].second);
607 : : }
608 : 60 : currIndex = nextIndex + 1;
609 : : }
610 : 32 : assignedValue = utils::mkConcat(cc, tn);
611 [ + - ]: 64 : Trace("strings-model")
612 : 0 : << "-> assign via seq.update/nth eqc: " << assignedValue
613 : 32 : << std::endl;
614 : 32 : }
615 : 100 : }
616 [ + + ]: 2630 : if (!assignedValue.isNull())
617 : : {
618 : 1500 : pure_eq_assign[eqc] = assignedValue;
619 : 1500 : m->getEqualityEngine()->addTerm(assignedValue);
620 : : }
621 : : else
622 : : {
623 [ + - ]: 1130 : Trace("strings-model") << "-> no assignment" << std::endl;
624 : : }
625 : 2630 : pure_eq.push_back(eqc);
626 [ + + ][ - ]: 5998 : }
627 : :
628 : : // assign a new length if necessary
629 [ + + ]: 10419 : if (!pure_eq.empty())
630 : : {
631 [ + - ]: 3056 : Trace("strings-model") << "Need to assign values of length " << lenValue
632 : 1528 : << " to equivalence classes ";
633 [ + + ]: 4158 : for (unsigned j = 0; j < pure_eq.size(); j++)
634 : : {
635 [ + - ]: 2630 : Trace("strings-model") << pure_eq[j] << " ";
636 : : }
637 [ + - ]: 1528 : Trace("strings-model") << std::endl;
638 : :
639 : : // use type enumerator
640 [ - + ][ - + ]: 1528 : Assert(lenValue.getConst<Rational>() <= Rational(String::maxSize()))
[ - - ]
641 : 0 : << "Exceeded UINT32_MAX in string model";
642 : : uint32_t currLen =
643 : 1528 : lenValue.getConst<Rational>().getNumerator().toUnsignedInt();
644 [ + - ]: 3056 : Trace("strings-model") << "Cardinality of alphabet is "
645 : 1528 : << d_termReg.getAlphabetCardinality() << std::endl;
646 : 1528 : SEnumLen* sel = sels.getEnumerator(currLen, tn);
647 [ + + ]: 4152 : for (const Node& eqc : pure_eq)
648 : : {
649 : 2630 : Node c;
650 : 2630 : std::map<Node, Node>::iterator itp = pure_eq_assign.find(eqc);
651 [ + + ]: 2630 : if (itp == pure_eq_assign.end())
652 : : {
653 : : do
654 : : {
655 [ + + ]: 1475 : if (sel->isFinished())
656 : : {
657 : : // We are in a case where model construction is impossible due to
658 : : // an insufficient number of constants of a given length.
659 : :
660 : : // Consider an integer equivalence class E whose value is assigned
661 : : // n in the model. Let { S_1, ..., S_m } be the set of string
662 : : // equivalence classes such that len( x ) is a member of E for
663 : : // some member x of each class S1, ...,Sm. Since our calculus is
664 : : // saturated with respect to cardinality inference (see Liang
665 : : // et al, Figure 6, CAV 2014), we have that m <= A^n, where A is
666 : : // the cardinality of our alphabet.
667 : :
668 : : // Now, consider the case where there exists two integer
669 : : // equivalence classes E1 and E2 that are assigned n, and moreover
670 : : // we did not received notification from arithmetic that E1 = E2.
671 : : // This typically should never happen, but assume in the following
672 : : // that it does.
673 : :
674 : : // Now, it may be the case that there are string equivalence
675 : : // classes { S_1, ..., S_m1 } whose lengths are in E1,
676 : : // and classes { S'_1, ..., S'_m2 } whose lengths are in E2, where
677 : : // m1 + m2 > A^n. In this case, we have insufficient strings to
678 : : // assign to { S_1, ..., S_m1, S'_1, ..., S'_m2 }. If this
679 : : // happens, we add a split on len( u1 ) = len( u2 ) for some
680 : : // len( u1 ) in E1, len( u2 ) in E2. We do this for each pair of
681 : : // integer equivalence classes that are assigned to the same value
682 : : // in the model.
683 [ - + ][ - + ]: 6 : AlwaysAssert(!len_splits.empty());
[ - - ]
684 [ + + ]: 16 : for (const std::pair<size_t, size_t>& sl : len_splits)
685 : : {
686 : : // ensure we use proxy variables or else the split may be
687 : : // rewritten away
688 : 10 : Node k1 = col[sl.first][0];
689 : 10 : Node kp1 = d_termReg.getProxyVariableFor(k1);
690 : 10 : Node k2 = col[sl.second][0];
691 : 10 : Node kp2 = d_termReg.getProxyVariableFor(k2);
692 : : Node s1 =
693 [ + + ]: 10 : nm->mkNode(Kind::STRING_LENGTH, kp1.isNull() ? k1 : kp1);
694 : : Node s2 =
695 [ + + ]: 10 : nm->mkNode(Kind::STRING_LENGTH, kp2.isNull() ? k2 : kp2);
696 : 10 : Node eq = s1.eqNode(s2);
697 : 20 : Node spl = nm->mkNode(Kind::OR, eq, eq.negate());
698 : 10 : d_im.lemma(spl, InferenceId::STRINGS_CMI_SPLIT);
699 [ + - ]: 20 : Trace("strings-lemma")
700 : 10 : << "Strings::CollectModelInfoSplit: " << spl << std::endl;
701 : 10 : }
702 : : // we added a lemma, so can return here
703 : 6 : return false;
704 : : }
705 : 1469 : c = sel->getCurrent();
706 : : // if we are a sequence with infinite element type
707 : 4407 : if (tn.isSequence()
708 [ + + ][ + + ]: 1469 : && !d_env.isFiniteType(tn.getSequenceElementType()))
[ + + ][ + + ]
[ - - ]
709 : : {
710 : : // Make a skeleton instead.
711 : 23 : c = mkSkeletonFor(c);
712 : : }
713 : : // increment
714 : 1469 : sel->increment();
715 [ + + ]: 1469 : } while (m->hasTerm(c));
716 : : }
717 : : else
718 : : {
719 : 1500 : c = itp->second;
720 : : }
721 [ + - ]: 5248 : Trace("strings-model")
722 : 2624 : << "*** Assigned constant " << c << " for " << eqc << std::endl;
723 : 2624 : processed[eqc] = c;
724 [ - + ]: 2624 : if (!m->assertEquality(eqc, c, true))
725 : : {
726 : : // this should never happen due to the model soundness argument
727 : : // for strings
728 : 0 : Unreachable()
729 : 0 : << "TheoryStrings::collectModelInfoType: Inconsistent equality"
730 : 0 : << std::endl;
731 : : return false;
732 : : }
733 [ + + ]: 2630 : }
734 : : }
735 [ + + ][ + + ]: 10425 : }
736 [ + - ]: 2210 : Trace("strings-model") << "String Model : Pure Assigned." << std::endl;
737 : : // step 4 : assign constants to all other equivalence classes
738 [ + + ]: 17194 : for (const Node& rn : repVec)
739 : : {
740 [ + + ]: 14984 : if (processed.find(rn) != processed.end())
741 : : {
742 : 11669 : continue;
743 : : }
744 : :
745 : 3315 : std::vector<Node> nf = mc->getNormalForm(rn);
746 [ - + ]: 3315 : if (TraceIsOn("strings-model"))
747 : : {
748 [ - - ]: 0 : Trace("strings-model")
749 : 0 : << "Construct model for " << rn << " based on normal form ";
750 [ - - ]: 0 : for (unsigned j = 0, size = nf.size(); j < size; j++)
751 : : {
752 : 0 : Node n = nf[j];
753 [ - - ]: 0 : if (j > 0)
754 : : {
755 [ - - ]: 0 : Trace("strings-model") << " ++ ";
756 : : }
757 [ - - ]: 0 : Trace("strings-model") << n;
758 : 0 : Node r = d_state.getRepresentative(n);
759 : 0 : if (!r.isConst() && processed.find(r) == processed.end())
760 : : {
761 [ - - ]: 0 : Trace("strings-model") << "(UNPROCESSED)";
762 : : }
763 : 0 : }
764 : : }
765 [ + - ]: 3315 : Trace("strings-model") << std::endl;
766 : 3315 : std::vector<Node> nc;
767 [ + + ]: 15342 : for (const Node& n : nf)
768 : : {
769 : 24054 : Node r = d_state.getRepresentative(n);
770 [ + + ][ + - ]: 12027 : Assert(r.isConst() || processed.find(r) != processed.end());
[ - + ][ - + ]
[ - - ]
771 [ + + ]: 12027 : nc.push_back(r.isConst() ? r : processed[r]);
772 : 12027 : }
773 : 3315 : Node cc = d_termReg.mkNConcat(nc, tn);
774 [ + - ]: 6630 : Trace("strings-model") << "*** Determined constant " << cc << " for " << rn
775 : 3315 : << std::endl;
776 : 3315 : processed[rn] = cc;
777 [ - + ]: 3315 : if (!m->assertEquality(rn, cc, true))
778 : : {
779 : : // this should never happen due to the model soundness argument
780 : : // for strings
781 : 0 : Unreachable() << "TheoryStrings::collectModelInfoType: "
782 : 0 : "Inconsistent equality (unprocessed eqc)"
783 : 0 : << std::endl;
784 : : return false;
785 : : }
786 [ + + ]: 3315 : else if (!cc.isConst())
787 : : {
788 : : // the value may be specified by seq.unit components, ensure this
789 : : // is marked as the skeleton for constructing values in this class.
790 : 67 : m->assertSkeleton(cc);
791 : : }
792 [ + - ][ + - ]: 3315 : }
[ + - ]
793 : : // Trace("strings-model") << "String Model : Assigned." << std::endl;
794 [ + - ]: 2210 : Trace("strings-model") << "String Model : Finished." << std::endl;
795 : 2210 : return true;
796 : 2216 : }
797 : :
798 : 23 : Node TheoryStrings::mkSkeletonFor(Node c)
799 : : {
800 : 23 : NodeManager* nm = nodeManager();
801 : 23 : SkolemManager* sm = nm->getSkolemManager();
802 : 23 : BoundVarManager* bvm = nm->getBoundVarManager();
803 : 23 : TypeNode tn = c.getType();
804 [ - + ][ - + ]: 23 : Assert(tn.isSequence());
[ - - ]
805 [ - + ][ - + ]: 23 : Assert(c.getKind() == Kind::CONST_SEQUENCE);
[ - - ]
806 : 23 : const Sequence& sn = c.getConst<Sequence>();
807 : 23 : const std::vector<Node>& snvec = sn.getVec();
808 : 23 : std::vector<Node> skChildren;
809 : 23 : TypeNode etn = tn.getSequenceElementType();
810 [ + + ]: 63 : for (const Node& snv : snvec)
811 : : {
812 [ - + ][ - + ]: 40 : Assert(snv.getType() == etn);
[ - - ]
813 : 80 : Node v = bvm->mkBoundVar(BoundVarId::STRINGS_SEQ_MODEL, snv, etn);
814 : : // use a skolem, not a bound variable
815 : 40 : Node kv = sm->mkPurifySkolem(v);
816 : 40 : skChildren.push_back(utils::mkUnit(tn, kv));
817 : 40 : }
818 : 69 : return utils::mkConcat(skChildren, c.getType());
819 : 23 : }
820 : :
821 : 12 : Node TheoryStrings::mkSkeletonFromBase(Node r,
822 : : size_t currIndex,
823 : : size_t nextIndex)
824 : : {
825 [ - + ][ - + ]: 12 : Assert(nextIndex > currIndex);
[ - - ]
826 [ - + ][ - + ]: 12 : Assert(!r.isNull());
[ - - ]
827 : 12 : NodeManager* nm = nodeManager();
828 : 12 : SkolemManager* sm = nm->getSkolemManager();
829 : 12 : TypeNode tn = r.getType();
830 : 12 : std::vector<Node> skChildren;
831 [ + - ]: 12 : if (tn.isSequence())
832 : : {
833 : 12 : std::vector<Node> cacheVals(2);
834 : 12 : cacheVals[0] = r;
835 : 12 : TypeNode etn = tn.getSequenceElementType();
836 [ + + ]: 24 : for (size_t i = currIndex; i < nextIndex; i++)
837 : : {
838 : 12 : cacheVals[1] = nm->mkConstInt(Rational(i));
839 : : Node kv = sm->mkInternalSkolemFunction(
840 : 12 : InternalSkolemId::SEQ_MODEL_BASE_ELEMENT, etn, cacheVals);
841 : 12 : skChildren.push_back(utils::mkUnit(tn, kv));
842 : 12 : }
843 : 12 : }
844 : : else
845 : : {
846 : : // allocate a unique symbolic (unspecified) string of length one, and
847 : : // repeat it (nextIndex-currIndex) times.
848 : : // Notice that this is guaranteed to be a unique (unspecified) character,
849 : : // since the only existing str.unit terms originate from our reductions,
850 : : // and hence are only applied to non-negative arguments. If the user
851 : : // was able to give arbitrary constraints over str.unit terms, then this
852 : : // construction would require a character not used in the model value of
853 : : // any other string.
854 : 0 : d_strGapModelCounter++;
855 : : Node symChar =
856 : 0 : utils::mkUnit(tn, nm->mkConstInt(-Rational(d_strGapModelCounter)));
857 : 0 : skChildren.resize(nextIndex - currIndex, symChar);
858 : 0 : }
859 : 24 : return utils::mkConcat(skChildren, tn);
860 : 12 : }
861 : :
862 : : /////////////////////////////////////////////////////////////////////////////
863 : : // MAIN SOLVER
864 : : /////////////////////////////////////////////////////////////////////////////
865 : :
866 : 364181 : void TheoryStrings::preRegisterTerm(TNode n)
867 : : {
868 [ + - ]: 728362 : Trace("strings-preregister")
869 : 364181 : << "TheoryStrings::preRegisterTerm: " << n << std::endl;
870 : 364181 : d_termReg.preRegisterTerm(n);
871 : : // Register the term with the extended theory. Notice we do not recurse on
872 : : // this term here since preRegisterTerm is already called recursively on all
873 : : // subterms in preregistered literals.
874 : 364181 : d_extTheory.registerTerm(n);
875 : 364181 : }
876 : :
877 : 2177833 : bool TheoryStrings::preNotifyFact(TNode atom,
878 : : bool pol,
879 : : CVC5_UNUSED TNode fact,
880 : : CVC5_UNUSED bool isPrereg,
881 : : bool isInternal)
882 : : {
883 [ + + ]: 2177833 : if (atom.getKind() == Kind::EQUAL)
884 : : {
885 : : // this is only required for internal facts, others are already registered
886 [ + + ]: 2124977 : if (isInternal)
887 : : {
888 : : // We must ensure these terms are registered. We register eagerly here for
889 : : // performance reasons. Alternatively, terms could be registered at full
890 : : // effort in e.g. BaseSolver::init.
891 [ + + ]: 295719 : for (const Node& t : atom)
892 : : {
893 : 197146 : d_termReg.registerTerm(t);
894 : 197146 : }
895 : : }
896 : : // store disequalities between strings that occur as literals
897 : 2124977 : if (!pol && atom[0].getType().isStringLike())
898 : : {
899 : 372896 : d_state.addDisequality(atom[0], atom[1]);
900 : : }
901 : : }
902 : 2177833 : return false;
903 : : }
904 : :
905 : 2177833 : void TheoryStrings::notifyFact(TNode atom,
906 : : bool polarity,
907 : : TNode fact,
908 : : bool isInternal)
909 : : {
910 [ + - ]: 2177833 : if (d_eagerSolver)
911 : : {
912 : 2177833 : d_eagerSolver->notifyFact(atom, polarity, fact, isInternal);
913 : : }
914 : : // process pending conflicts due to reasoning about endpoints
915 [ + + ][ + + ]: 2177833 : if (!d_state.isInConflict() && d_state.hasPendingConflict())
[ + + ]
916 : : {
917 : 1123 : InferInfo iiPendingConf(InferenceId::UNKNOWN);
918 : 1123 : d_state.getPendingConflict(iiPendingConf);
919 [ + - ]: 2246 : Trace("strings-pending")
920 : 1123 : << "Process pending conflict " << iiPendingConf.d_premises << std::endl;
921 [ + - ]: 2246 : Trace("strings-conflict")
922 : 1123 : << "CONFLICT: Eager : " << iiPendingConf.d_premises << std::endl;
923 : 1123 : ++(d_statistics.d_conflictsEager);
924 : : // call the inference manager to send the conflict
925 : 1123 : d_im.processConflict(iiPendingConf);
926 : 1123 : return;
927 : 1123 : }
928 : : // if not doing eager registration, we now register all subterms of the atom
929 [ + + ]: 2176710 : if (!options().strings.stringEagerReg)
930 : : {
931 : 1546 : d_termReg.registerSubterms(atom);
932 : : }
933 [ + - ]: 2176710 : Trace("strings-pending-debug") << " Now collect terms" << std::endl;
934 [ + - ]: 2176710 : Trace("strings-pending-debug") << " Finished collect terms" << std::endl;
935 : : }
936 : :
937 : 914531 : void TheoryStrings::postCheck(Effort e)
938 : : {
939 : 914531 : d_im.doPendingFacts();
940 : :
941 [ - + ][ - + ]: 914531 : Assert(d_strat.isStrategyInit());
[ - - ]
942 [ + + ]: 1822336 : if (!d_state.isInConflict() && !d_valuation.needCheck()
943 [ + + ][ + + ]: 1822336 : && d_strat.hasStrategyEffort(e))
[ + + ]
944 : : {
945 [ + - ]: 139318 : Trace("strings-check-debug")
946 : 69659 : << "Theory of strings " << e << " effort check " << std::endl;
947 [ - + ]: 69659 : if (TraceIsOn("strings-eqc"))
948 : : {
949 : 0 : Trace("strings-eqc") << debugPrintStringsEqc() << std::endl;
950 : : }
951 : : // Start the full effort check. This will compute the relevant term set,
952 : : // which is independent of the loop below, which adds internal facts.
953 : 69659 : d_termReg.notifyStartFullEffortCheck();
954 : 69659 : ++(d_statistics.d_checkRuns);
955 : 69659 : bool sentLemma = false;
956 : 69659 : bool hadPending = false;
957 [ + - ]: 69659 : Trace("strings-check") << "Check at effort " << e << "..." << std::endl;
958 : : do
959 : : {
960 : 105078 : d_im.reset();
961 : : // assume the default model constructor in case we answer sat after this
962 : : // check
963 : 105078 : d_state.setModelConstructor(&d_mcd);
964 : 105078 : ++(d_statistics.d_strategyRuns);
965 [ + - ]: 105078 : Trace("strings-check") << " * Run strategy..." << std::endl;
966 : 105078 : runStrategy(e);
967 : : // remember if we had pending facts or lemmas
968 : 105078 : hadPending = d_im.hasPending();
969 : : // Send the facts *and* the lemmas. We send lemmas regardless of whether
970 : : // we send facts since some lemmas cannot be dropped. Other lemmas are
971 : : // otherwise avoided by aborting the strategy when a fact is ready.
972 : 105078 : d_im.doPending();
973 : : // Did we successfully send a lemma? Notice that if hasPending = true
974 : : // and sentLemma = false, then the above call may have:
975 : : // (1) had no pending lemmas, but successfully processed pending facts,
976 : : // (2) unsuccessfully processed pending lemmas.
977 : : // In either case, we repeat the strategy if we are not in conflict.
978 : 105078 : sentLemma = d_im.hasSentLemma();
979 [ - + ]: 105078 : if (TraceIsOn("strings-check"))
980 : : {
981 [ - - ]: 0 : Trace("strings-check") << " ...finish run strategy: ";
982 : 0 : Trace("strings-check") << (hadPending ? "hadPending " : "");
983 : 0 : Trace("strings-check") << (sentLemma ? "sentLemma " : "");
984 : 0 : Trace("strings-check") << (d_state.isInConflict() ? "conflict " : "");
985 [ - - ][ - - ]: 0 : if (!hadPending && !sentLemma && !d_state.isInConflict())
[ - - ][ - - ]
986 : : {
987 [ - - ]: 0 : Trace("strings-check") << "(none)";
988 : : }
989 [ - - ]: 0 : Trace("strings-check") << std::endl;
990 : : }
991 : : // repeat if we did not add a lemma or conflict, and we had pending
992 : : // facts or lemmas.
993 [ + + ][ + + ]: 105078 : } while (!d_state.isInConflict() && !sentLemma && hadPending);
[ + + ][ + + ]
994 : : // End the full effort check.
995 : 69659 : d_termReg.notifyEndFullEffortCheck();
996 : : }
997 [ + - ]: 1829062 : Trace("strings-check") << "Theory of strings, done check : " << e
998 : 914531 : << std::endl;
999 [ - + ][ - + ]: 914531 : Assert(!d_im.hasPendingFact());
[ - - ]
1000 [ - + ][ - + ]: 914531 : Assert(!d_im.hasPendingLemma());
[ - - ]
1001 : 914531 : }
1002 : :
1003 : 26293 : bool TheoryStrings::needsCheckLastEffort()
1004 : : {
1005 [ + - ]: 26293 : if (options().strings.stringModelBasedReduction)
1006 : : {
1007 : 26293 : bool hasExtf = d_esolver.hasExtendedFunctions();
1008 [ + - ]: 52586 : Trace("strings-process")
1009 : 26293 : << "needsCheckLastEffort: hasExtf = " << hasExtf << std::endl;
1010 : 26293 : return hasExtf;
1011 : : }
1012 : 0 : return false;
1013 : : }
1014 : :
1015 : : /** Conflict when merging two constants */
1016 : 3361 : void TheoryStrings::conflict(TNode a, TNode b)
1017 : : {
1018 [ - + ]: 3361 : if (d_state.isInConflict())
1019 : : {
1020 : : // already in conflict
1021 : 0 : return;
1022 : : }
1023 : 3361 : d_im.conflictEqConstantMerge(a, b);
1024 [ + - ]: 3361 : Trace("strings-conflict") << "CONFLICT: Eq engine conflict" << std::endl;
1025 : 3361 : ++(d_statistics.d_conflictsEqEngine);
1026 : : }
1027 : :
1028 : 275565 : void TheoryStrings::eqNotifyNewClass(TNode t)
1029 : : {
1030 : 275565 : Kind k = t.getKind();
1031 [ + + ][ + + ]: 275565 : if (k == Kind::STRING_LENGTH || k == Kind::STRING_TO_CODE)
1032 : : {
1033 [ + - ]: 82079 : Trace("strings-debug") << "New length eqc : " << t << std::endl;
1034 : :
1035 : 82079 : eq::EqualityEngine* ee = d_state.getEqualityEngine();
1036 : 164158 : Node r = ee->getRepresentative(t[0]);
1037 : 82079 : EqcInfo* ei = d_state.getOrMakeEqcInfo(r);
1038 [ + + ]: 82079 : if (k == Kind::STRING_LENGTH)
1039 : : {
1040 : 78484 : ei->d_lengthTerm = t;
1041 : : }
1042 : : else
1043 : : {
1044 : 3595 : ei->d_codeTerm = t[0];
1045 : : }
1046 : 82079 : }
1047 [ + - ]: 275565 : if (d_eagerSolver)
1048 : : {
1049 : 275565 : d_eagerSolver->eqNotifyNewClass(t);
1050 : : }
1051 : 275565 : }
1052 : :
1053 : 2923511 : void TheoryStrings::eqNotifyMerge(TNode t1, TNode t2)
1054 : : {
1055 : 2923511 : EqcInfo* e2 = d_state.getOrMakeEqcInfo(t2, false);
1056 [ + + ]: 2923511 : if (e2 == nullptr)
1057 : : {
1058 : 1303505 : return;
1059 : : }
1060 : : // always create it if e2 was non-null
1061 : 1620006 : EqcInfo* e1 = d_state.getOrMakeEqcInfo(t1);
1062 : :
1063 [ + - ]: 1620006 : if (d_eagerSolver)
1064 : : {
1065 : 1620006 : d_eagerSolver->eqNotifyMerge(e1, t1, e2, t2);
1066 : : }
1067 : :
1068 : : // add information from e2 to e1
1069 [ + + ]: 1620006 : if (!e2->d_lengthTerm.get().isNull())
1070 : : {
1071 : 806597 : e1->d_lengthTerm.set(e2->d_lengthTerm);
1072 : : }
1073 [ + + ]: 1620006 : if (!e2->d_codeTerm.get().isNull())
1074 : : {
1075 : 11769 : e1->d_codeTerm.set(e2->d_codeTerm);
1076 : : }
1077 [ - + ]: 1620006 : if (e2->d_cardinalityLemK.get() > e1->d_cardinalityLemK.get())
1078 : : {
1079 : 0 : e1->d_cardinalityLemK.set(e2->d_cardinalityLemK);
1080 : : }
1081 [ + + ]: 1620006 : if (!e2->d_normalizedLength.get().isNull())
1082 : : {
1083 : 168 : e1->d_normalizedLength.set(e2->d_normalizedLength);
1084 : : }
1085 : : }
1086 : :
1087 : 29087 : void TheoryStrings::computeCareGraph()
1088 : : {
1089 : : // computing the care graph here is probably still necessary, due to operators
1090 : : // that take non-string arguments TODO: verify
1091 [ + - ]: 58174 : Trace("strings-cg")
1092 : 0 : << "TheoryStrings::computeCareGraph(): Build term indices..."
1093 : 29087 : << std::endl;
1094 : : // Term index for each (type, operator) pair. We require the operator here
1095 : : // since operators are polymorphic, taking strings/sequences.
1096 : 29087 : std::map<std::pair<TypeNode, Node>, TNodeTrie> index;
1097 : 29087 : std::map<Node, unsigned> arity;
1098 : 29087 : const context::CDList<TNode>& fterms = d_termReg.getFunctionTerms();
1099 : 29087 : size_t functionTerms = fterms.size();
1100 [ + + ]: 95710 : for (unsigned i = 0; i < functionTerms; ++i)
1101 : : {
1102 : 66623 : TNode f1 = fterms[i];
1103 [ + - ]: 66623 : Trace("strings-cg") << "...build for " << f1 << std::endl;
1104 : 66623 : Node op = f1.getOperator();
1105 : 66623 : std::vector<TNode> reps;
1106 : 66623 : bool has_trigger_arg = false;
1107 [ + + ]: 150947 : for (unsigned j = 0; j < f1.getNumChildren(); j++)
1108 : : {
1109 : 84324 : reps.push_back(d_equalityEngine->getRepresentative(f1[j]));
1110 [ + + ]: 84324 : if (d_equalityEngine->isTriggerTerm(f1[j], THEORY_STRINGS))
1111 : : {
1112 : 57737 : has_trigger_arg = true;
1113 : : }
1114 : : }
1115 [ + + ]: 66623 : if (has_trigger_arg)
1116 : : {
1117 : 46522 : TypeNode ft = utils::getOwnerStringType(f1);
1118 [ - + ][ - - ]: 46522 : AlwaysAssert(ft.isStringLike())
1119 [ - + ][ - + ]: 46522 : << "Unexpected term in getOwnerStringType : " << f1 << ", type "
[ - - ]
1120 : : << ft;
1121 : 46522 : std::pair<TypeNode, Node> ikey = std::pair<TypeNode, Node>(ft, op);
1122 : 46522 : index[ikey].addTerm(f1, reps);
1123 : 46522 : arity[op] = reps.size();
1124 : 46522 : }
1125 : 66623 : }
1126 : : // for each index
1127 [ + + ]: 35601 : for (std::pair<const std::pair<TypeNode, Node>, TNodeTrie>& ti : index)
1128 : : {
1129 [ + - ]: 13028 : Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Process index "
1130 : 6514 : << ti.first << "..." << std::endl;
1131 : 6514 : Node op = ti.first.second;
1132 : 6514 : nodeTriePathPairProcess(&ti.second, arity[op], d_cpacb);
1133 : 6514 : }
1134 : 29087 : }
1135 : :
1136 : 189963 : void TheoryStrings::notifySharedTerm(TNode n)
1137 : : {
1138 : : // a new shared term causes new terms to be relevant, hence we register
1139 : : // them if not doing eager registration.
1140 [ + + ]: 189963 : if (!options().strings.stringEagerReg)
1141 : : {
1142 : 195 : d_termReg.registerSubterms(n);
1143 : : }
1144 : 189963 : TypeNode tn = n.getType();
1145 [ + + ]: 189963 : if (!d_env.isFirstClassType(tn))
1146 : : {
1147 [ - + ][ - + ]: 1 : Assert(tn.isRegExp());
[ - - ]
1148 : 1 : std::stringstream ss;
1149 : 1 : ss << "Regular expression terms are not supported in theory combination";
1150 : 1 : throw LogicException(ss.str());
1151 : 1 : }
1152 : 189963 : }
1153 : :
1154 : 221981 : TrustNode TheoryStrings::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
1155 : : {
1156 [ + - ]: 221981 : Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl;
1157 : 221981 : Kind ak = atom.getKind();
1158 [ + + ]: 221981 : if (ak == Kind::STRING_FROM_CODE)
1159 : : {
1160 : : // for the sake of proofs, we use the eager reduction utility
1161 : 99 : Node k = nodeManager()->getSkolemManager()->mkPurifySkolem(atom);
1162 : 99 : TrustNode lemma = d_termReg.eagerReduceTrusted(atom);
1163 : 99 : lems.push_back(SkolemLemma(lemma, k));
1164 : : // We rewrite the term to its purify variable, which can be justified
1165 : : // trivially.
1166 : 99 : return TrustNode::mkTrustRewrite(atom, k, nullptr);
1167 : 99 : }
1168 [ + + ]: 221882 : if (ak == Kind::REGEXP_RANGE)
1169 : : {
1170 [ + + ]: 1150 : for (const Node& nc : atom)
1171 : : {
1172 [ + + ]: 767 : if (!nc.isConst())
1173 : : {
1174 : 1 : throw LogicException(
1175 : 2 : "expecting a constant string term in regexp range");
1176 : : }
1177 [ - + ][ - + ]: 766 : Assert(nc.getConst<String>().size() == 1);
[ - - ]
1178 : 767 : }
1179 : : }
1180 : :
1181 : 221881 : TrustNode ret;
1182 : 221881 : Node atomRet = atom;
1183 : 221881 : if (options().strings.regExpElim != options::RegExpElimMode::OFF
1184 [ + + ][ + + ]: 221881 : && ak == Kind::STRING_IN_REGEXP)
[ + + ]
1185 : : {
1186 : : // aggressive elimination of regular expression membership
1187 : 264 : ret = d_regexp_elim.eliminateTrusted(atomRet);
1188 [ + + ]: 264 : if (!ret.isNull())
1189 : : {
1190 [ + - ][ - + ]: 392 : Trace("strings-ppr") << " rewrote " << atom << " -> " << ret.getNode()
[ - - ]
1191 : 0 : << " via regular expression elimination."
1192 : 196 : << std::endl;
1193 : 196 : atomRet = ret.getNode();
1194 : : }
1195 : : }
1196 [ + + ]: 221881 : if (options().strings.stringFMF)
1197 : : {
1198 : : // Our decision strategy will minimize the length of this term if it is a
1199 : : // variable but not an internally generated Skolem, or a term that does
1200 : : // not belong to this theory.
1201 [ + + ][ + + ]: 29384 : if (atom.isVar() ? !d_termReg.getSkolemCache()->isSkolem(atom)
[ - - ]
1202 : 7040 : : kindToTheoryId(ak) != THEORY_STRINGS
1203 [ - + ][ - - ]: 18212 : && atom.getType().isStringLike())
[ - + ][ + + ]
[ - - ]
1204 : : {
1205 : 532 : d_termReg.preRegisterInputVar(atom);
1206 [ + - ]: 532 : Trace("strings-preregister") << "input variable: " << atom << std::endl;
1207 : : }
1208 : : }
1209 : :
1210 : : // all characters of constants should fall in the alphabet
1211 [ + + ][ + + ]: 221881 : if (atom.isConst() && atom.getType().isString())
[ + + ][ + + ]
[ - - ]
1212 : : {
1213 : 11311 : uint32_t alphaCard = d_termReg.getAlphabetCardinality();
1214 : 11311 : std::vector<unsigned> vec = atom.getConst<String>().getVec();
1215 [ + + ]: 37052 : for (unsigned u : vec)
1216 : : {
1217 [ - + ]: 25741 : if (u >= alphaCard)
1218 : : {
1219 : 0 : std::stringstream ss;
1220 : 0 : ss << "Characters in string \"" << atom
1221 : 0 : << "\" are outside of the given alphabet.";
1222 : 0 : throw LogicException(ss.str());
1223 : 0 : }
1224 : : }
1225 : 11311 : }
1226 [ - + ]: 221881 : if (!options().strings.stringExp)
1227 : : {
1228 [ - - ][ - - ]: 0 : if (ak == Kind::STRING_INDEXOF || ak == Kind::STRING_INDEXOF_RE
1229 [ - - ][ - - ]: 0 : || ak == Kind::STRING_ITOS || ak == Kind::STRING_STOI
1230 [ - - ][ - - ]: 0 : || ak == Kind::STRING_REPLACE || ak == Kind::STRING_SUBSTR
1231 [ - - ][ - - ]: 0 : || ak == Kind::STRING_REPLACE_ALL || ak == Kind::SEQ_NTH
1232 [ - - ][ - - ]: 0 : || ak == Kind::STRING_REPLACE_RE || ak == Kind::STRING_REPLACE_RE_ALL
1233 [ - - ][ - - ]: 0 : || ak == Kind::STRING_CONTAINS || ak == Kind::STRING_LEQ
1234 [ - - ][ - - ]: 0 : || ak == Kind::STRING_TO_LOWER || ak == Kind::STRING_TO_UPPER
1235 [ - - ][ - - ]: 0 : || ak == Kind::STRING_REV || ak == Kind::STRING_UPDATE)
1236 : : {
1237 : 0 : std::stringstream ss;
1238 : 0 : ss << "Term of kind " << printer::smt2::Smt2Printer::smtKindStringOf(atom)
1239 : 0 : << " not supported in default mode, try --strings-exp";
1240 : 0 : throw LogicException(ss.str());
1241 : 0 : }
1242 : : }
1243 : 221881 : return ret;
1244 : 221881 : }
1245 : :
1246 : 30271 : TrustNode TheoryStrings::ppStaticRewrite(TNode atom)
1247 : : {
1248 : 30271 : Kind ak = atom.getKind();
1249 [ + + ]: 30271 : if (ak == Kind::EQUAL)
1250 : : {
1251 [ + + ]: 5624 : if (atom[0].getType().isRegExp())
1252 : : {
1253 : 10 : Node res = d_rewriter.rewriteViaRule(ProofRewriteRule::RE_EQ_ELIM, atom);
1254 [ - + ][ - + ]: 10 : Assert(!res.isNull());
[ - - ]
1255 [ + + ]: 10 : return TrustNode::mkTrustRewrite(atom, res, d_psrewPg.get());
1256 : 10 : }
1257 : : // always apply aggressive equality rewrites here
1258 : 5614 : Node ret = d_rewriter.rewriteEqualityExt(atom);
1259 [ + + ]: 5614 : if (ret != atom)
1260 : : {
1261 [ + + ]: 688 : return TrustNode::mkTrustRewrite(atom, ret, d_psrewPg.get());
1262 : : }
1263 [ + + ]: 5614 : }
1264 : 29573 : return TrustNode::null();
1265 : : }
1266 : :
1267 : : /** run the given inference step */
1268 : 979464 : void TheoryStrings::runInferStep(InferStep s, Theory::Effort e, int effort)
1269 : : {
1270 [ + - ]: 979464 : Trace("strings-process") << "Run " << s;
1271 [ + + ]: 979464 : if (effort > 0)
1272 : : {
1273 [ + - ]: 47940 : Trace("strings-process") << ", effort = " << effort;
1274 : : }
1275 [ + - ]: 979464 : Trace("strings-process") << "..." << std::endl;
1276 [ + + ][ + + ]: 979464 : switch (s)
[ + + ][ + + ]
[ + + ][ + + ]
[ + - ][ + + ]
[ + + ][ + - ]
1277 : : {
1278 : 103991 : case InferStep::CHECK_INIT: d_bsolver.checkInit(); break;
1279 : 85481 : case InferStep::CHECK_CONST_EQC:
1280 : 85481 : d_bsolver.checkConstantEquivalenceClasses();
1281 : 85481 : break;
1282 : 133365 : case InferStep::CHECK_EXTF_EVAL: d_esolver.checkExtfEval(effort); break;
1283 : 80672 : case InferStep::CHECK_CYCLES: d_csolver.checkCycles(); break;
1284 : 80636 : case InferStep::CHECK_FLAT_FORMS: d_csolver.checkFlatForms(); break;
1285 : 65366 : case InferStep::CHECK_NORMAL_FORMS_EQ_PROP:
1286 : 65366 : d_csolver.checkNormalFormsEqProp();
1287 : 65366 : break;
1288 : 53191 : case InferStep::CHECK_NORMAL_FORMS_EQ:
1289 : 53191 : d_csolver.checkNormalFormsEq();
1290 : 53191 : break;
1291 : 43305 : case InferStep::CHECK_NORMAL_FORMS_DEQ:
1292 : 43305 : d_csolver.checkNormalFormsDeq();
1293 : 43305 : break;
1294 : 42319 : case InferStep::CHECK_CODES: d_psolver.checkCodes(); break;
1295 : 42125 : case InferStep::CHECK_LENGTH_EQC: d_csolver.checkLengthsEqc(); break;
1296 : 389 : case InferStep::CHECK_SEQUENCES_ARRAY_CONCAT:
1297 : 389 : d_asolver.checkArrayConcat();
1298 : 389 : break;
1299 : 245 : case InferStep::CHECK_SEQUENCES_ARRAY: d_asolver.checkArray(); break;
1300 : 170 : case InferStep::CHECK_SEQUENCES_ARRAY_EAGER:
1301 : 170 : d_asolver.checkArrayEager();
1302 : 170 : break;
1303 : 0 : case InferStep::CHECK_REGISTER_TERMS_NF:
1304 : 0 : d_csolver.checkRegisterTermsNormalForms();
1305 : 0 : break;
1306 : 68628 : case InferStep::CHECK_EXTF_REDUCTION_EAGER:
1307 : 68628 : d_esolver.checkExtfReductionsEager();
1308 : 68628 : break;
1309 : 39891 : case InferStep::CHECK_EXTF_REDUCTION:
1310 : 39891 : d_esolver.checkExtfReductions(e);
1311 : 39891 : break;
1312 : 65373 : case InferStep::CHECK_MEMBERSHIP_EAGER:
1313 : 65373 : d_rsolver.checkMembershipsEager();
1314 : 65373 : break;
1315 : 37977 : case InferStep::CHECK_MEMBERSHIP: d_rsolver.checkMemberships(e); break;
1316 : 36340 : case InferStep::CHECK_CARDINALITY: d_bsolver.checkCardinality(); break;
1317 : 0 : default: Unreachable(); break;
1318 : : }
1319 [ + - ]: 1958928 : Trace("strings-process") << "Done " << s
1320 : 0 : << ", addedFact = " << d_im.hasPendingFact()
1321 : 0 : << ", addedLemma = " << d_im.hasPendingLemma()
1322 : 979464 : << ", conflict = " << d_state.isInConflict()
1323 : 979464 : << std::endl;
1324 : 979464 : }
1325 : :
1326 : 105078 : void TheoryStrings::runStrategy(Theory::Effort e)
1327 : : {
1328 : 105078 : std::vector<std::pair<InferStep, int>>::iterator it = d_strat.stepBegin(e);
1329 : 105078 : std::vector<std::pair<InferStep, int>>::iterator stepEnd = d_strat.stepEnd(e);
1330 : :
1331 [ + - ]: 105078 : Trace("strings-process") << "----check, next round---" << std::endl;
1332 [ + + ]: 1956469 : while (it != stepEnd)
1333 : : {
1334 : 1919059 : InferStep curr = it->first;
1335 : 1919059 : int effort = it->second;
1336 [ + + ]: 1919059 : if (curr == InferStep::BREAK)
1337 : : {
1338 : : // if we have a pending inference or lemma, we will process it
1339 [ + + ]: 939595 : if (d_im.hasProcessed())
1340 : : {
1341 : 65209 : break;
1342 : : }
1343 : : }
1344 : : else
1345 : : {
1346 : 979464 : runInferStep(curr, e, effort);
1347 [ + + ]: 979464 : if (d_state.isInConflict())
1348 : : {
1349 : 2459 : break;
1350 : : }
1351 : : }
1352 : 1851391 : ++it;
1353 : : }
1354 [ + - ]: 105078 : Trace("strings-process") << "----finished round---" << std::endl;
1355 : 105078 : }
1356 : :
1357 : 0 : std::string TheoryStrings::debugPrintStringsEqc()
1358 : : {
1359 : 0 : std::stringstream ss;
1360 [ - - ]: 0 : for (unsigned t = 0; t < 2; t++)
1361 : : {
1362 : 0 : eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(d_equalityEngine);
1363 [ - - ]: 0 : ss << (t == 0 ? "STRINGS:" : "OTHER:") << std::endl;
1364 [ - - ]: 0 : while (!eqcs2_i.isFinished())
1365 : : {
1366 : 0 : Node eqc = (*eqcs2_i);
1367 : 0 : bool print = (t == 0 && eqc.getType().isStringLike())
1368 : 0 : || (t == 1 && !eqc.getType().isStringLike());
1369 [ - - ]: 0 : if (print)
1370 : : {
1371 : 0 : eq::EqClassIterator eqc2_i = eq::EqClassIterator(eqc, d_equalityEngine);
1372 : 0 : ss << "Eqc( " << eqc << " ) : { ";
1373 [ - - ]: 0 : while (!eqc2_i.isFinished())
1374 : : {
1375 : 0 : if ((*eqc2_i) != eqc && (*eqc2_i).getKind() != Kind::EQUAL)
1376 : : {
1377 : 0 : ss << (*eqc2_i) << " ";
1378 : : }
1379 : 0 : ++eqc2_i;
1380 : : }
1381 : 0 : ss << " } " << std::endl;
1382 : 0 : EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false);
1383 [ - - ]: 0 : if (ei)
1384 : : {
1385 [ - - ]: 0 : Trace("strings-eqc-debug")
1386 : 0 : << "* Length term : " << ei->d_lengthTerm.get() << std::endl;
1387 [ - - ]: 0 : Trace("strings-eqc-debug")
1388 : 0 : << "* Cardinality lemma k : " << ei->d_cardinalityLemK.get()
1389 : 0 : << std::endl;
1390 [ - - ]: 0 : Trace("strings-eqc-debug")
1391 : 0 : << "* Normalization length lemma : "
1392 : 0 : << ei->d_normalizedLength.get() << std::endl;
1393 : : }
1394 : : }
1395 : 0 : ++eqcs2_i;
1396 : 0 : }
1397 : 0 : ss << std::endl;
1398 : : }
1399 : 0 : ss << std::endl;
1400 : 0 : return ss.str();
1401 : 0 : }
1402 : :
1403 : : } // namespace strings
1404 : : } // namespace theory
1405 : : } // namespace cvc5::internal
|
