Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Andres Noetzli
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 term registry for the theory of strings.
14 : : */
15 : :
16 : : #include "theory/strings/term_registry.h"
17 : :
18 : : #include "options/smt_options.h"
19 : : #include "options/strings_options.h"
20 : : #include "printer/smt2/smt2_printer.h"
21 : : #include "smt/logic_exception.h"
22 : : #include "theory/rewriter.h"
23 : : #include "theory/strings/inference_manager.h"
24 : : #include "theory/strings/regexp_entail.h"
25 : : #include "theory/strings/theory_strings_utils.h"
26 : : #include "theory/strings/word.h"
27 : : #include "theory/theory.h"
28 : : #include "util/rational.h"
29 : : #include "util/string.h"
30 : :
31 : : using namespace std;
32 : : using namespace cvc5::context;
33 : : using namespace cvc5::internal::kind;
34 : :
35 : : namespace cvc5::internal {
36 : : namespace theory {
37 : : namespace strings {
38 : :
39 : 49899 : TermRegistry::TermRegistry(Env& env, Theory& t, SolverState& s)
40 : : : EnvObj(env),
41 : 49899 : d_theory(t),
42 : 49899 : d_state(s),
43 : 49899 : d_im(nullptr),
44 : 49899 : d_hasStrCode(false),
45 : 49899 : d_hasSeqUpdate(false),
46 : 49899 : d_skCache(nodeManager(), env.getRewriter()),
47 : 49899 : d_aent(nodeManager(), env.getRewriter()),
48 : 49899 : d_functionsTerms(context()),
49 : 49899 : d_inputVars(userContext()),
50 : 49899 : d_preregisteredTerms(context()),
51 : 49899 : d_registeredTerms(userContext()),
52 : 49899 : d_registeredTypes(userContext()),
53 : 49899 : d_proxyVar(userContext()),
54 : 49899 : d_proxyVarToLength(userContext()),
55 : 49899 : d_lengthLemmaTermsCache(userContext()),
56 : 70177 : d_epg(env.isTheoryProofProducing()
57 : : ? new EagerProofGenerator(
58 : : env,
59 : 10139 : userContext(),
60 : 10139 : "strings::TermRegistry::EagerProofGenerator")
61 : : : nullptr),
62 : 99798 : d_inFullEffortCheck(false)
63 : : {
64 : 49899 : NodeManager* nm = nodeManager();
65 : 49899 : d_zero = nm->mkConstInt(Rational(0));
66 : 49899 : d_one = nm->mkConstInt(Rational(1));
67 : 49899 : d_negOne = nm->mkConstInt(Rational(-1));
68 [ - + ][ - + ]: 49899 : Assert(options().strings.stringsAlphaCard <= String::num_codes());
[ - - ]
69 : 49899 : d_alphaCard = options().strings.stringsAlphaCard;
70 : 49899 : }
71 : :
72 : 49554 : TermRegistry::~TermRegistry() {}
73 : :
74 : 111380 : uint32_t TermRegistry::getAlphabetCardinality() const { return d_alphaCard; }
75 : :
76 : 49899 : void TermRegistry::finishInit(InferenceManager* im) { d_im = im; }
77 : :
78 : 142143 : Node TermRegistry::eagerReduce(Node t, SkolemCache* sc, uint32_t alphaCard)
79 : : {
80 : 142143 : NodeManager* nm = t.getNodeManager();
81 : 142143 : Node lemma;
82 : 142143 : Kind tk = t.getKind();
83 [ + + ]: 142143 : if (tk == Kind::STRING_TO_CODE)
84 : : {
85 : : // ite( str.len(s)==1, 0 <= str.code(s) < |A|, str.code(s)=-1 )
86 : 4036 : Node len = nm->mkNode(Kind::STRING_LENGTH, t[0]);
87 : 4036 : Node code_len = len.eqNode(nm->mkConstInt(Rational(1)));
88 : 4036 : Node code_eq_neg1 = t.eqNode(nm->mkConstInt(Rational(-1)));
89 : 2018 : Node code_range = utils::mkCodeRange(t, alphaCard);
90 : 2018 : lemma = nm->mkNode(Kind::ITE, code_len, code_range, code_eq_neg1);
91 : 2018 : }
92 [ + + ]: 140125 : else if (tk == Kind::SEQ_NTH)
93 : : {
94 [ - + ]: 2358 : if (t[0].getType().isString())
95 : : {
96 : 0 : Node s = t[0];
97 : 0 : Node n = t[1];
98 : : // start point is greater than or equal zero
99 : 0 : Node c1 = nm->mkNode(Kind::GEQ, n, nm->mkConstInt(0));
100 : : // start point is less than end of string
101 : 0 : Node c2 = nm->mkNode(Kind::GT, nm->mkNode(Kind::STRING_LENGTH, s), n);
102 : : // check whether this application of seq.nth is defined.
103 : 0 : Node cond = nm->mkNode(Kind::AND, c1, c2);
104 : 0 : Node code_range = utils::mkCodeRange(t, alphaCard);
105 : : // the lemma for `seq.nth`
106 : 0 : lemma = nm->mkNode(
107 : 0 : Kind::ITE, cond, code_range, t.eqNode(nm->mkConstInt(Rational(-1))));
108 : : // IF: n >=0 AND n < len( s )
109 : : // THEN: 0 <= (seq.nth s n) < |A|
110 : : // ELSE: (seq.nth s n) = -1
111 : 0 : }
112 : : }
113 [ + + ][ + + ]: 137767 : else if (tk == Kind::STRING_INDEXOF || tk == Kind::STRING_INDEXOF_RE)
114 : : {
115 : : // (and
116 : : // (or (= (f x y n) (- 1)) (>= (f x y n) n))
117 : : // (<= (f x y n) (str.len x)))
118 : : //
119 : : // where f in { str.indexof, str.indexof_re }
120 : 1928 : Node l = nm->mkNode(Kind::STRING_LENGTH, t[0]);
121 : 2892 : lemma = nm->mkNode(Kind::AND,
122 : 2892 : nm->mkNode(Kind::OR,
123 : 1928 : t.eqNode(nm->mkConstInt(Rational(-1))),
124 : 1928 : nm->mkNode(Kind::GEQ, t, t[2])),
125 : 2892 : nm->mkNode(Kind::LEQ, t, l));
126 : 964 : }
127 [ + + ]: 136803 : else if (tk == Kind::STRING_STOI)
128 : : {
129 : : // (>= (str.to_int x) (- 1))
130 : 206 : lemma = nm->mkNode(Kind::GEQ, t, nm->mkConstInt(Rational(-1)));
131 : : }
132 [ + + ]: 136597 : else if (tk == Kind::STRING_CONTAINS)
133 : : {
134 : : // ite( (str.contains s r), (= s (str.++ sk1 r sk2)), (not (= s r)))
135 : : Node sk1 =
136 : 1496 : sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_PRE, "sc1");
137 : : Node sk2 =
138 : 1496 : sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_POST, "sc2");
139 : 748 : lemma = t[0].eqNode(nm->mkNode(Kind::STRING_CONCAT, sk1, t[1], sk2));
140 : 748 : lemma = nm->mkNode(Kind::ITE, t, lemma, t[0].eqNode(t[1]).notNode());
141 : 748 : }
142 [ + + ]: 135849 : else if (tk == Kind::STRING_IN_REGEXP)
143 : : {
144 : : // for (str.in_re t R), if R has a fixed length L, then we infer the lemma:
145 : : // (str.in_re t R) => (= (str.len t) L).
146 : 6212 : Node len = RegExpEntail::getFixedLengthForRegexp(t[1]);
147 [ + + ]: 3106 : if (!len.isNull())
148 : : {
149 : 820 : lemma = nm->mkNode(
150 : 1230 : Kind::IMPLIES, t, nm->mkNode(Kind::STRING_LENGTH, t[0]).eqNode(len));
151 : : }
152 : 3106 : }
153 [ + + ]: 132743 : else if (tk == Kind::STRING_FROM_CODE)
154 : : {
155 : : // str.from_code(t) ---> ite(0 <= t < |A|, t = str.to_code(k), k = "")
156 : 128 : Node k = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "kFromCode");
157 : 128 : Node tc = t[0];
158 : 128 : Node card = nm->mkConstInt(Rational(alphaCard));
159 : : Node cond = nm->mkNode(Kind::AND,
160 : 256 : nm->mkNode(Kind::LEQ, nm->mkConstInt(0), tc),
161 : 512 : nm->mkNode(Kind::LT, tc, card));
162 : 128 : Node emp = Word::mkEmptyWord(t.getType());
163 : 384 : lemma = nm->mkNode(Kind::ITE,
164 : : cond,
165 : 256 : tc.eqNode(nm->mkNode(Kind::STRING_TO_CODE, k)),
166 : 384 : k.eqNode(emp));
167 : 128 : }
168 : 142143 : return lemma;
169 : 0 : }
170 : :
171 : 34791 : Node TermRegistry::lengthPositive(Node t)
172 : : {
173 : 34791 : NodeManager* nm = t.getNodeManager();
174 : 34791 : Node zero = nm->mkConstInt(Rational(0));
175 : 34791 : Node emp = Word::mkEmptyWord(t.getType());
176 : 34791 : Node tlen = nm->mkNode(Kind::STRING_LENGTH, t);
177 : 34791 : Node tlenEqZero = tlen.eqNode(zero);
178 : 34791 : Node tEqEmp = t.eqNode(emp);
179 : 69582 : Node caseEmpty = nm->mkNode(Kind::AND, tlenEqZero, tEqEmp);
180 : 69582 : Node caseNEmpty = nm->mkNode(Kind::GT, tlen, zero);
181 : : // (or (and (= (str.len t) 0) (= t "")) (> (str.len t) 0))
182 : 69582 : return nm->mkNode(Kind::OR, caseEmpty, caseNEmpty);
183 : 34791 : }
184 : :
185 : 351948 : void TermRegistry::preRegisterTerm(TNode n)
186 : : {
187 [ + + ]: 351948 : if (d_preregisteredTerms.find(n) != d_preregisteredTerms.end())
188 : : {
189 : 2449 : return;
190 : : }
191 : 349499 : eq::EqualityEngine* ee = d_state.getEqualityEngine();
192 : 349499 : d_preregisteredTerms.insert(n);
193 [ + - ]: 698998 : Trace("strings-preregister")
194 : 349499 : << "TheoryString::preregister : " << n << std::endl;
195 : : // check for logic exceptions
196 : 349499 : Kind k = n.getKind();
197 : 349499 : if (k == Kind::EQUAL && n[0].getType().isRegExp())
198 : : {
199 : : // if an equality between regular expressions was introduced during solving,
200 : : // e.g. by theory combination, we send the equivalance for its quantified
201 : : // reduction here, e.g.
202 : : // (R1 = R2) = (forall s. (s in R1) = (s in R2)).
203 : : Node res =
204 : 0 : d_env.getRewriter()->rewriteViaRule(ProofRewriteRule::RE_EQ_ELIM, n);
205 : 0 : Node lem = nodeManager()->mkNode(Kind::EQUAL, n, res);
206 : 0 : d_im->lemma(lem, InferenceId::STRINGS_RE_EQ_ELIM_EQUIV);
207 : 0 : }
208 [ + + ]: 349499 : if (k == Kind::STRING_IN_REGEXP)
209 : : {
210 : 4851 : d_im->preferPhase(n, true);
211 : : }
212 [ + + ]: 344648 : else if (k == Kind::STRING_TO_CODE)
213 : : {
214 : 3571 : d_hasStrCode = true;
215 : : }
216 [ + + ][ + + ]: 341077 : else if (k == Kind::SEQ_NTH || k == Kind::STRING_UPDATE)
217 : : {
218 : 4905 : d_hasSeqUpdate = true;
219 : : }
220 [ + + ]: 336172 : else if (k == Kind::CONST_SEQUENCE)
221 : : {
222 : : // If we are a constant sequence that has "nested" constant sequences
223 : : // implicitly, e.g. for sequences of sequences, then we must ensure that
224 : : // all subterms of this constant are also considered as terms by the
225 : : // solver. Otherwise, these terms would be hidden inside of the sequence
226 : : // constant. To do so, we ensure a purify skolem is introduced for each
227 : : // subterm. For example, for the sequence constant t:
228 : : // (str.++ (as seq.empty (Seq Int)) (seq.unit (str.++ 0 1)))
229 : : // We add the lemma:
230 : : // k1 = (as seq.empty (Seq Int)) ^ k2 = (seq.unit (str.++ 0 1)) ^
231 : : // t = (str.++ k1 k2).
232 : : // The right hand sides of the first two equalties will lead to
233 : : // preregistering these sequence constants in the same way.
234 : : // These lemmas can be justified trivially by MACRO_SR_PRED_INTRO.
235 : 853 : Node nc = utils::mkConcatForConstSequence(n);
236 : 853 : Kind nck = nc.getKind();
237 [ + + ]: 853 : if (nck != Kind::CONST_SEQUENCE)
238 : : {
239 : 380 : std::vector<Node> eqs;
240 : 380 : std::vector<Node> children;
241 [ + + ]: 915 : for (const Node& ncc : nc)
242 : : {
243 [ + + ]: 535 : if (ncc.getKind() == Kind::CONST_SEQUENCE)
244 : : {
245 : 108 : Node skolem = SkolemManager::mkPurifySkolem(ncc);
246 : 108 : children.push_back(skolem);
247 : 108 : eqs.push_back(skolem.eqNode(ncc));
248 : 108 : }
249 : : else
250 : : {
251 : 427 : children.push_back(ncc);
252 : : }
253 : 535 : }
254 : 380 : Node ret = nodeManager()->mkNode(nck, children);
255 : 380 : eqs.push_back(n.eqNode(ret));
256 : 380 : Node lem = nodeManager()->mkAnd(eqs);
257 [ + - ]: 760 : Trace("strings-preregister")
258 : 380 : << "Const sequence lemma: " << lem << std::endl;
259 : 380 : d_im->lemma(lem, InferenceId::STRINGS_CONST_SEQ_PURIFY);
260 : 380 : }
261 : 853 : }
262 [ + + ]: 349499 : if (options().strings.stringEagerReg)
263 : : {
264 : 348796 : registerTerm(n);
265 : : }
266 : 349499 : TypeNode tn = n.getType();
267 : 349499 : registerType(tn);
268 [ + + ][ - + ]: 349499 : if (tn.isRegExp() && n.isVar())
[ - + ]
269 : : {
270 : 0 : std::stringstream ss;
271 : 0 : ss << "Regular expression variables are not supported.";
272 : 0 : throw LogicException(ss.str());
273 : 0 : }
274 [ + + ]: 349499 : if (tn.isBoolean())
275 : : {
276 : : // All kinds that we do congruence over that may return a Boolean go here
277 [ + + ][ + + ]: 142188 : if (k == Kind::STRING_CONTAINS || k == Kind::STRING_LEQ
278 [ + + ][ + + ]: 137872 : || k == Kind::SEQ_NTH || k == Kind::EQUAL)
279 : : {
280 : : // Get triggered for both equal and dis-equal
281 : 137280 : d_state.addEqualityEngineTriggerPredicate(n);
282 : : }
283 : : }
284 : : else
285 : : {
286 : : // Function applications/predicates
287 : 207311 : ee->addTerm(n);
288 : : }
289 : : // Set d_functionsTerms stores all function applications that are
290 : : // relevant to theory combination. Notice that this is a subset of
291 : : // the applications whose kinds are function kinds in the equality
292 : : // engine. This means it does not include applications of operators
293 : : // like re.++, which is not a function kind in the equality engine.
294 : : // Concatenation terms do not need to be considered here because
295 : : // their arguments have string type and do not introduce any shared
296 : : // terms.
297 [ + + ]: 617818 : if (n.hasOperator() && ee->isFunctionKind(k)
298 [ + - ][ + + ]: 127213 : && kindToTheoryId(k) == THEORY_STRINGS && k != Kind::STRING_CONCAT
299 [ + + ][ + + ]: 617818 : && k != Kind::STRING_IN_REGEXP)
[ + + ]
300 : : {
301 : 97244 : d_functionsTerms.push_back(n);
302 : : }
303 : 349499 : }
304 : :
305 : 532 : void TermRegistry::preRegisterInputVar(TNode n) { d_inputVars.insert(n); }
306 : :
307 : 1741 : void TermRegistry::registerSubterms(Node n)
308 : : {
309 : 1741 : std::unordered_set<TNode> visited;
310 : 1741 : std::vector<TNode> visit;
311 : 1741 : TNode cur;
312 : 1741 : visit.push_back(n);
313 : : do
314 : : {
315 : 2658 : cur = visit.back();
316 : 2658 : visit.pop_back();
317 [ + + ]: 2658 : if (d_registeredTerms.find(cur) == d_registeredTerms.end())
318 : : {
319 : 648 : registerTermInternal(cur);
320 : 648 : Kind k = cur.getKind();
321 : : // only traverse beneath operators belonging to strings
322 [ + + ][ + + ]: 648 : if (k == Kind::EQUAL || theory::kindToTheoryId(k) == THEORY_STRINGS)
[ + + ]
323 : : {
324 : : // strings does not have any closure kinds
325 [ - + ][ - + ]: 520 : Assert (!cur.isClosure());
[ - - ]
326 : 520 : visit.insert(visit.end(), cur.begin(), cur.end());
327 : : }
328 : : }
329 [ + + ]: 2658 : } while (!visit.empty());
330 : 1741 : }
331 : :
332 : 526615 : void TermRegistry::registerTerm(Node n)
333 : : {
334 [ + + ]: 526615 : if (d_registeredTerms.find(n) != d_registeredTerms.end())
335 : : {
336 : 315478 : return;
337 : : }
338 : 211137 : registerTermInternal(n);
339 : : }
340 : :
341 : 211785 : void TermRegistry::registerTermInternal(Node n)
342 : : {
343 [ - + ][ - + ]: 211785 : Assert(d_registeredTerms.find(n) == d_registeredTerms.end());
[ - - ]
344 [ + - ]: 423570 : Trace("strings-register")
345 : 211785 : << "TheoryStrings::registerTermInternal() " << n << std::endl;
346 : 211785 : d_registeredTerms.insert(n);
347 : : // ensure the type is registered
348 : 211785 : TypeNode tn = n.getType();
349 : 211785 : TrustNode regTermLem;
350 [ + + ]: 211785 : if (tn.isStringLike())
351 : : {
352 : : // register length information:
353 : : // for variables, split on empty vs positive length
354 : : // for concat/const/replace, introduce proxy var and state length relation
355 : 68590 : regTermLem = getRegisterTermLemma(n);
356 : : }
357 : : else
358 : : {
359 : : // we don't send out eager reduction lemma for str.contains currently
360 : 143195 : bool doEagerReduce = true;
361 : 143195 : Kind k = n.getKind();
362 [ + + ]: 143195 : if (k == Kind::STRING_CONTAINS)
363 : : {
364 : 2384 : doEagerReduce = false;
365 : : }
366 [ + + ]: 140811 : else if (k == Kind::STRING_TO_CODE)
367 : : {
368 : : // code for proxy are implied
369 : 2033 : Node c = SkolemManager::getOriginalForm(n[0]);
370 : 2033 : doEagerReduce = !c.isConst();
371 : 2033 : }
372 [ + + ]: 143195 : if (doEagerReduce)
373 : : {
374 : 140287 : regTermLem = eagerReduceTrusted(n);
375 : : }
376 : : }
377 [ + + ]: 211785 : if (!regTermLem.isNull())
378 : : {
379 [ + - ]: 49942 : Trace("strings-lemma") << "Strings::Lemma REG-TERM : " << regTermLem
380 : 24971 : << std::endl;
381 [ + - ]: 49942 : Trace("strings-assert")
382 [ - + ][ - - ]: 24971 : << "(assert " << regTermLem.getNode() << ")" << std::endl;
383 : 24971 : d_im->trustedLemma(regTermLem, InferenceId::STRINGS_REGISTER_TERM);
384 : : }
385 : 211785 : }
386 : :
387 : 140386 : TrustNode TermRegistry::eagerReduceTrusted(const Node& n)
388 : : {
389 : 140386 : TrustNode regTermLem;
390 : 140386 : Node eagerRedLemma = eagerReduce(n, &d_skCache, d_alphaCard);
391 [ + + ]: 140386 : if (!eagerRedLemma.isNull())
392 : : {
393 [ + + ]: 2717 : if (d_epg != nullptr)
394 : : {
395 : 2757 : regTermLem = d_epg->mkTrustNode(
396 : 919 : eagerRedLemma, ProofRule::STRING_EAGER_REDUCTION, {}, {n});
397 : : }
398 : : else
399 : : {
400 : 1798 : regTermLem = TrustNode::mkTrustLemma(eagerRedLemma, nullptr);
401 : : }
402 : : }
403 : 280772 : return regTermLem;
404 : 140386 : }
405 : :
406 : 349499 : void TermRegistry::registerType(TypeNode tn)
407 : : {
408 [ + + ]: 349499 : if (d_registeredTypes.find(tn) != d_registeredTypes.end())
409 : : {
410 : 341676 : return;
411 : : }
412 : 7823 : d_registeredTypes.insert(tn);
413 [ + + ]: 7823 : if (tn.isStringLike())
414 : : {
415 : : // preregister the empty word for the type
416 : 2451 : Node emp = Word::mkEmptyWord(tn);
417 : : // always preregister and register unconditionally eagerly
418 : 2451 : preRegisterTerm(emp);
419 : 2451 : registerTerm(emp);
420 : 2451 : }
421 : : }
422 : :
423 : 68590 : TrustNode TermRegistry::getRegisterTermLemma(Node n)
424 : : {
425 [ - + ][ - + ]: 68590 : Assert(n.getType().isStringLike());
[ - - ]
426 : 68590 : NodeManager* nm = nodeManager();
427 : : // register length information:
428 : : // for variables, split on empty vs positive length
429 : : // for concat/const/replace, introduce proxy var and state length relation
430 : 68590 : Node lsum;
431 : 68590 : Kind nk = n.getKind();
432 [ + + ][ + + ]: 68590 : if (nk != Kind::STRING_CONCAT && !n.isConst())
[ + + ]
433 : : {
434 : 47479 : Node lsumb = nm->mkNode(Kind::STRING_LENGTH, n);
435 : 47479 : lsum = rewrite(lsumb);
436 : : // can register length term if it does not rewrite
437 [ + + ]: 47479 : if (lsum == lsumb)
438 : : {
439 : 46237 : registerTermAtomic(n, LENGTH_SPLIT);
440 : 46237 : return TrustNode::null();
441 : : }
442 [ + + ]: 47479 : }
443 : 22353 : Node sk = d_skCache.mkSkolemCached(n, SkolemCache::SK_PURIFY, "lsym");
444 : 44706 : Node eq = rewrite(sk.eqNode(n));
445 : 22353 : d_proxyVar[n] = sk;
446 : : // If we are introducing a proxy for a constant or concat term, we do not
447 : : // need to send lemmas about its length, since its length is already
448 : : // implied.
449 [ + + ][ + + ]: 22353 : if (n.isConst() || nk == Kind::STRING_CONCAT)
[ + + ]
450 : : {
451 : : // do not send length lemma for sk.
452 : 21111 : registerTermAtomic(sk, LENGTH_IGNORE);
453 : : }
454 : 22353 : Node skl = nm->mkNode(Kind::STRING_LENGTH, sk);
455 [ + + ]: 22353 : if (nk == Kind::STRING_CONCAT)
456 : : {
457 : 13443 : std::vector<Node> nodeVec;
458 : 13443 : NodeNodeMap::const_iterator itl;
459 [ + + ]: 46356 : for (const Node& nc : n)
460 : : {
461 : 32913 : itl = d_proxyVarToLength.find(nc);
462 [ + + ]: 32913 : if (itl != d_proxyVarToLength.end())
463 : : {
464 : 105 : nodeVec.push_back(itl->second);
465 : : }
466 : : else
467 : : {
468 : 32808 : Node lni = nm->mkNode(Kind::STRING_LENGTH, nc);
469 : 32808 : nodeVec.push_back(lni);
470 : 32808 : }
471 : 32913 : }
472 : 13443 : lsum = nm->mkNode(Kind::ADD, nodeVec);
473 : 13443 : lsum = rewrite(lsum);
474 : 13443 : }
475 [ + + ]: 8910 : else if (n.isConst())
476 : : {
477 : 7668 : lsum = nm->mkConstInt(Rational(Word::getLength(n)));
478 : : }
479 [ - + ][ - + ]: 22353 : Assert(!lsum.isNull());
[ - - ]
480 : 22353 : d_proxyVarToLength[sk] = lsum;
481 : 44706 : Node ceq = rewrite(skl.eqNode(lsum));
482 : :
483 : 44706 : Node ret = nm->mkNode(Kind::AND, eq, ceq);
484 : :
485 : : // it is a simple rewrite to justify this
486 [ + + ]: 22353 : if (d_epg != nullptr)
487 : : {
488 : 17336 : return d_epg->mkTrustNode(ret, ProofRule::MACRO_SR_PRED_INTRO, {}, {ret});
489 : : }
490 : 13685 : return TrustNode::mkTrustLemma(ret, nullptr);
491 : 68590 : }
492 : :
493 : 69924 : void TermRegistry::registerTermAtomic(Node n, LengthStatus s)
494 : : {
495 [ + + ]: 69924 : if (d_lengthLemmaTermsCache.find(n) != d_lengthLemmaTermsCache.end())
496 : : {
497 : 44755 : return;
498 : : }
499 : 46246 : d_lengthLemmaTermsCache.insert(n);
500 : :
501 [ + + ]: 46246 : if (s == LENGTH_IGNORE)
502 : : {
503 : : // ignore it
504 : 21077 : return;
505 : : }
506 : 25169 : std::map<Node, bool> reqPhase;
507 : 25169 : TrustNode lenLem = getRegisterTermAtomicLemma(n, s, reqPhase);
508 [ + + ]: 25169 : if (!lenLem.isNull())
509 : : {
510 [ + - ]: 50320 : Trace("strings-lemma") << "Strings::Lemma REGISTER-TERM-ATOMIC : " << lenLem
511 : 25160 : << std::endl;
512 [ + - ]: 50320 : Trace("strings-assert")
513 [ - + ][ - - ]: 25160 : << "(assert " << lenLem.getNode() << ")" << std::endl;
514 : 25160 : d_im->trustedLemma(lenLem, InferenceId::STRINGS_REGISTER_TERM_ATOMIC);
515 : : }
516 [ + + ]: 75489 : for (const std::pair<const Node, bool>& rp : reqPhase)
517 : : {
518 : 50320 : d_im->preferPhase(rp.first, rp.second);
519 : : }
520 : 25169 : }
521 : :
522 : 120966 : SkolemCache* TermRegistry::getSkolemCache() { return &d_skCache; }
523 : :
524 : 27369 : const context::CDList<TNode>& TermRegistry::getFunctionTerms() const
525 : : {
526 : 27369 : return d_functionsTerms;
527 : : }
528 : :
529 : 85 : const context::CDHashSet<Node>& TermRegistry::getInputVars() const
530 : : {
531 : 85 : return d_inputVars;
532 : : }
533 : :
534 : 42312 : bool TermRegistry::hasStringCode() const { return d_hasStrCode; }
535 : :
536 : 804 : bool TermRegistry::hasSeqUpdate() const { return d_hasSeqUpdate; }
537 : :
538 : 1649 : bool TermRegistry::isHandledUpdateOrSubstr(Node n)
539 : : {
540 [ + + ][ + - ]: 1649 : Assert(n.getKind() == Kind::STRING_UPDATE
[ - + ][ - + ]
[ - - ]
541 : : || n.getKind() == Kind::STRING_SUBSTR);
542 : 1649 : NodeManager* nm = nodeManager();
543 : 1649 : Node lenN = n[2];
544 [ + + ]: 1649 : if (n.getKind() == Kind::STRING_UPDATE)
545 : : {
546 : 1614 : lenN = nm->mkNode(Kind::STRING_LENGTH, n[2]);
547 : : }
548 : 1649 : Node one = nm->mkConstInt(Rational(1));
549 : 3298 : return d_aent.checkEq(lenN, one);
550 : 1649 : }
551 : :
552 : 0 : Node TermRegistry::getUpdateBase(Node n)
553 : : {
554 [ - - ]: 0 : while (n.getKind() == Kind::STRING_UPDATE)
555 : : {
556 : 0 : n = n[0];
557 : : }
558 : 0 : return n;
559 : : }
560 : :
561 : 25169 : TrustNode TermRegistry::getRegisterTermAtomicLemma(
562 : : Node n, LengthStatus s, std::map<Node, bool>& reqPhase)
563 : : {
564 [ + + ]: 25169 : if (n.isConst())
565 : : {
566 : : // No need to send length for constant terms. This case may be triggered
567 : : // for cases where the skolem cache automatically replaces a skolem by
568 : : // a constant.
569 : 9 : return TrustNode::null();
570 : : }
571 [ - + ][ - + ]: 25160 : Assert(n.getType().isStringLike());
[ - - ]
572 : 25160 : NodeManager* nm = nodeManager();
573 : 25160 : Node n_len = nm->mkNode(Kind::STRING_LENGTH, n);
574 : 25160 : Node emp = Word::mkEmptyWord(n.getType());
575 [ - + ]: 25160 : if (s == LENGTH_GEQ_ONE)
576 : : {
577 : 0 : Node neq_empty = n.eqNode(emp).negate();
578 : 0 : Node len_n_gt_z = nm->mkNode(Kind::GT, n_len, d_zero);
579 : 0 : Node len_geq_one = nm->mkNode(Kind::AND, neq_empty, len_n_gt_z);
580 [ - - ]: 0 : Trace("strings-lemma") << "Strings::Lemma SK-GEQ-ONE : " << len_geq_one
581 : 0 : << std::endl;
582 [ - - ]: 0 : Trace("strings-assert") << "(assert " << len_geq_one << ")" << std::endl;
583 : 0 : return TrustNode::mkTrustLemma(len_geq_one, nullptr);
584 : 0 : }
585 : :
586 [ - + ]: 25160 : if (s == LENGTH_ONE)
587 : : {
588 : 0 : Node len_one = n_len.eqNode(d_one);
589 [ - - ]: 0 : Trace("strings-lemma") << "Strings::Lemma SK-ONE : " << len_one
590 : 0 : << std::endl;
591 [ - - ]: 0 : Trace("strings-assert") << "(assert " << len_one << ")" << std::endl;
592 : 0 : return TrustNode::mkTrustLemma(len_one, nullptr);
593 : 0 : }
594 [ - + ][ - + ]: 25160 : Assert(s == LENGTH_SPLIT);
[ - - ]
595 : :
596 : : // get the positive length lemma
597 : 25160 : Node lenLemma = lengthPositive(n);
598 : : // split whether the string is empty
599 : 25160 : Node n_len_eq_z = n_len.eqNode(d_zero);
600 : 25160 : Node n_len_eq_z_2 = n.eqNode(emp);
601 : 50320 : Node case_empty = nm->mkNode(Kind::AND, n_len_eq_z, n_len_eq_z_2);
602 : 25160 : Node case_emptyr = rewrite(case_empty);
603 [ + - ]: 25160 : if (!case_emptyr.isConst())
604 : : {
605 : : // prefer trying the empty case first
606 : : // notice that preferPhase must only be called on rewritten literals that
607 : : // occur in the CNF stream.
608 : 25160 : n_len_eq_z = rewrite(n_len_eq_z);
609 [ - + ][ - + ]: 25160 : Assert(!n_len_eq_z.isConst());
[ - - ]
610 : 25160 : reqPhase[n_len_eq_z] = true;
611 : 25160 : n_len_eq_z_2 = rewrite(n_len_eq_z_2);
612 [ - + ][ - + ]: 25160 : Assert(!n_len_eq_z_2.isConst());
[ - - ]
613 : 25160 : reqPhase[n_len_eq_z_2] = true;
614 : : }
615 : : else
616 : : {
617 : : // If n = "" ---> true or len( n ) = 0 ----> true, then we expect that
618 : : // n ---> "". Since this method is only called on non-constants n, it must
619 : : // be that n = "" ^ len( n ) = 0 does not rewrite to true.
620 : 0 : Assert(!case_emptyr.getConst<bool>());
621 : : }
622 : :
623 [ + + ]: 25160 : if (d_epg != nullptr)
624 : : {
625 : 18310 : return d_epg->mkTrustNode(lenLemma, ProofRule::STRING_LENGTH_POS, {}, {n});
626 : : }
627 : 16005 : return TrustNode::mkTrustLemma(lenLemma, nullptr);
628 : 25160 : }
629 : :
630 : 413489 : Node TermRegistry::getSymbolicDefinition(Node n, std::vector<Node>& exp) const
631 : : {
632 [ + + ]: 413489 : if (n.getNumChildren() == 0)
633 : : {
634 : 232069 : Node pn = getProxyVariableFor(n);
635 [ + + ]: 232069 : if (pn.isNull())
636 : : {
637 : 37130 : return Node::null();
638 : : }
639 : 194939 : Node eq = n.eqNode(pn);
640 : 194939 : eq = rewrite(eq);
641 [ + + ]: 194939 : if (std::find(exp.begin(), exp.end(), eq) == exp.end())
642 : : {
643 : 181513 : exp.push_back(eq);
644 : : }
645 : 194939 : return pn;
646 : 232069 : }
647 : 181420 : std::vector<Node> children;
648 [ + + ]: 181420 : if (n.getMetaKind() == metakind::PARAMETERIZED)
649 : : {
650 : 563 : children.push_back(n.getOperator());
651 : : }
652 [ + + ]: 450031 : for (const Node& nc : n)
653 : : {
654 [ + + ]: 326938 : if (n.getType().isRegExp())
655 : : {
656 : 46949 : children.push_back(nc);
657 : : }
658 : : else
659 : : {
660 : 279989 : Node ns = getSymbolicDefinition(nc, exp);
661 [ + + ]: 279989 : if (ns.isNull())
662 : : {
663 : 58327 : return Node::null();
664 : : }
665 : : else
666 : : {
667 : 221662 : children.push_back(ns);
668 : : }
669 [ + + ]: 279989 : }
670 [ + + ]: 326938 : }
671 : 123093 : return nodeManager()->mkNode(n.getKind(), children);
672 : 181420 : }
673 : :
674 : 436696 : Node TermRegistry::getProxyVariableFor(Node n) const
675 : : {
676 : 436696 : NodeNodeMap::const_iterator it = d_proxyVar.find(n);
677 [ + + ]: 436696 : if (it != d_proxyVar.end())
678 : : {
679 : 254566 : return (*it).second;
680 : : }
681 : 182130 : return Node::null();
682 : : }
683 : :
684 : 6367 : Node TermRegistry::ensureProxyVariableFor(Node n)
685 : : {
686 : 6367 : Node proxy = getProxyVariableFor(n);
687 [ + + ]: 6367 : if (proxy.isNull())
688 : : {
689 : 54 : registerTerm(n);
690 : 54 : proxy = getProxyVariableFor(n);
691 : : }
692 [ - + ][ - + ]: 6367 : Assert(!proxy.isNull());
[ - - ]
693 : 6367 : return proxy;
694 : 0 : }
695 : :
696 : 207201 : void TermRegistry::removeProxyEqs(Node n, std::vector<Node>& unproc) const
697 : : {
698 [ + + ]: 207201 : if (n.getKind() == Kind::AND)
699 : : {
700 [ + + ]: 1150 : for (const Node& nc : n)
701 : : {
702 : 819 : removeProxyEqs(nc, unproc);
703 : 819 : }
704 : 331 : return;
705 : : }
706 [ + - ]: 206870 : Trace("strings-subs-proxy") << "Input : " << n << std::endl;
707 : 206870 : Node ns = rewrite(n);
708 [ + + ]: 206870 : if (ns.getKind() == Kind::EQUAL)
709 : : {
710 [ + + ]: 618342 : for (size_t i = 0; i < 2; i++)
711 : : {
712 : : // determine whether this side has a proxy variable
713 [ + + ]: 412228 : if (d_proxyVar.find(ns[i]) != d_proxyVar.end())
714 : : {
715 [ - + ]: 198186 : if (getProxyVariableFor(ns[1 - i]) == ns[i])
716 : : {
717 [ - - ]: 0 : Trace("strings-subs-proxy")
718 : 0 : << "...trivial definition via " << ns[i] << std::endl;
719 : : // it is a trivial equality, e.g. between a proxy variable
720 : : // and its definition
721 : 0 : return;
722 : : }
723 : : }
724 : : }
725 : : }
726 [ + + ][ - + ]: 206870 : if (!n.isConst() || !n.getConst<bool>())
[ + + ]
727 : : {
728 [ + - ]: 206814 : Trace("strings-subs-proxy") << "...unprocessed" << std::endl;
729 : 206814 : unproc.push_back(n);
730 : : }
731 [ + - ]: 206870 : }
732 : :
733 : 65629 : void TermRegistry::notifyStartFullEffortCheck()
734 : : {
735 : 65629 : d_inFullEffortCheck = true;
736 : 65629 : d_relevantTerms.clear();
737 : : // get the asserted terms
738 : 65629 : std::set<Kind> irrKinds;
739 : 65629 : d_theory.collectAssertedTerms(d_relevantTerms, true, irrKinds);
740 : : // also, get the additionally relevant terms
741 : 65629 : d_theory.computeRelevantTerms(d_relevantTerms);
742 : 65629 : }
743 : :
744 : 65629 : void TermRegistry::notifyEndFullEffortCheck() { d_inFullEffortCheck = false; }
745 : :
746 : 2019849 : const std::set<Node>& TermRegistry::getRelevantTermSet() const
747 : : {
748 : : // must be in full effort check for relevant terms to be valid
749 [ - + ][ - + ]: 2019849 : Assert(d_inFullEffortCheck);
[ - - ]
750 : 2019849 : return d_relevantTerms;
751 : : }
752 : :
753 : 1164 : Node TermRegistry::mkNConcat(Node n1, Node n2) const
754 : : {
755 : 1164 : return rewrite(NodeManager::mkNode(Kind::STRING_CONCAT, n1, n2));
756 : : }
757 : :
758 : 0 : Node TermRegistry::mkNConcat(Node n1, Node n2, Node n3) const
759 : : {
760 : 0 : return rewrite(NodeManager::mkNode(Kind::STRING_CONCAT, n1, n2, n3));
761 : : }
762 : :
763 : 1289685 : Node TermRegistry::mkNConcat(const std::vector<Node>& c, TypeNode tn) const
764 : : {
765 : 1289685 : return rewrite(utils::mkConcat(c, tn));
766 : : }
767 : :
768 : : } // namespace strings
769 : : } // namespace theory
770 : : } // namespace cvc5::internal
|
