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 strings proof checker.
11 : : */
12 : :
13 : : #include "theory/strings/proof_checker.h"
14 : :
15 : : #include "expr/sequence.h"
16 : : #include "options/strings_options.h"
17 : : #include "theory/rewriter.h"
18 : : #include "theory/strings/regexp_elim.h"
19 : : #include "theory/strings/regexp_entail.h"
20 : : #include "theory/strings/regexp_operation.h"
21 : : #include "theory/strings/skolem_cache.h"
22 : : #include "theory/strings/theory_strings_preprocess.h"
23 : : #include "theory/strings/theory_strings_utils.h"
24 : : #include "theory/strings/word.h"
25 : :
26 : : using namespace cvc5::internal::kind;
27 : :
28 : : namespace cvc5::internal {
29 : : namespace theory {
30 : : namespace strings {
31 : :
32 : 27722 : StringProofRuleChecker::StringProofRuleChecker(NodeManager* nm,
33 : 27722 : uint32_t alphaCard)
34 : 27722 : : ProofRuleChecker(nm), d_alphaCard(alphaCard)
35 : : {
36 : 27722 : }
37 : :
38 : 13932 : void StringProofRuleChecker::registerTo(ProofChecker* pc)
39 : : {
40 : 13932 : pc->registerChecker(ProofRule::CONCAT_EQ, this);
41 : 13932 : pc->registerChecker(ProofRule::CONCAT_UNIFY, this);
42 : 13932 : pc->registerChecker(ProofRule::CONCAT_SPLIT, this);
43 : 13932 : pc->registerChecker(ProofRule::CONCAT_CSPLIT, this);
44 : 13932 : pc->registerChecker(ProofRule::CONCAT_LPROP, this);
45 : 13932 : pc->registerChecker(ProofRule::CONCAT_CPROP, this);
46 : 13932 : pc->registerChecker(ProofRule::STRING_DECOMPOSE, this);
47 : 13932 : pc->registerChecker(ProofRule::STRING_LENGTH_POS, this);
48 : 13932 : pc->registerChecker(ProofRule::STRING_LENGTH_NON_EMPTY, this);
49 : 13932 : pc->registerChecker(ProofRule::STRING_REDUCTION, this);
50 : 13932 : pc->registerChecker(ProofRule::STRING_EAGER_REDUCTION, this);
51 : 13932 : pc->registerChecker(ProofRule::RE_INTER, this);
52 : 13932 : pc->registerChecker(ProofRule::RE_CONCAT, this);
53 : 13932 : pc->registerChecker(ProofRule::RE_UNFOLD_POS, this);
54 : 13932 : pc->registerChecker(ProofRule::RE_UNFOLD_NEG, this);
55 : 13932 : pc->registerChecker(ProofRule::RE_UNFOLD_NEG_CONCAT_FIXED, this);
56 : 13932 : pc->registerChecker(ProofRule::STRING_CODE_INJ, this);
57 : 13932 : pc->registerChecker(ProofRule::STRING_SEQ_UNIT_INJ, this);
58 : 13932 : pc->registerChecker(ProofRule::STRING_EXT, this);
59 : : // trusted rule
60 : 13932 : pc->registerTrustedChecker(ProofRule::MACRO_STRING_INFERENCE, this, 2);
61 : 13932 : }
62 : :
63 : 18511 : Node StringProofRuleChecker::checkInternal(ProofRule id,
64 : : const std::vector<Node>& children,
65 : : const std::vector<Node>& args)
66 : : {
67 : 18511 : NodeManager* nm = nodeManager();
68 : : // core rules for word equations
69 [ + + ][ + + ]: 18511 : if (id == ProofRule::CONCAT_EQ || id == ProofRule::CONCAT_UNIFY
70 [ + + ][ + + ]: 13976 : || id == ProofRule::CONCAT_SPLIT || id == ProofRule::CONCAT_CSPLIT
71 [ + + ][ + + ]: 13222 : || id == ProofRule::CONCAT_LPROP || id == ProofRule::CONCAT_CPROP)
72 : : {
73 [ + - ]: 5826 : Trace("strings-pfcheck") << "Checking id " << id << std::endl;
74 [ - + ][ - + ]: 5826 : Assert(children.size() >= 1);
[ - - ]
75 [ - + ][ - + ]: 5826 : Assert(args.size() == 1);
[ - - ]
76 : : // all rules have an equality
77 [ - + ]: 5826 : if (children[0].getKind() != Kind::EQUAL)
78 : : {
79 : 0 : return Node::null();
80 : : }
81 : : // convert to concatenation form
82 : 5826 : std::vector<Node> tvec;
83 : 5826 : std::vector<Node> svec;
84 : 5826 : utils::getConcat(children[0][0], tvec);
85 : 5826 : utils::getConcat(children[0][1], svec);
86 : 5826 : size_t nchildt = tvec.size();
87 : 5826 : size_t nchilds = svec.size();
88 : 5826 : TypeNode stringType = children[0][0].getType();
89 : : // extract the Boolean corresponding to whether the rule is reversed
90 : : bool isRev;
91 [ - + ]: 5826 : if (!getBool(args[0], isRev))
92 : : {
93 : 0 : return Node::null();
94 : : }
95 [ + + ]: 5826 : if (id == ProofRule::CONCAT_EQ)
96 : : {
97 [ - + ][ - + ]: 3173 : Assert(children.size() == 1);
[ - - ]
98 : 3173 : size_t index = 0;
99 : 3173 : std::vector<Node> tremVec;
100 : 3173 : std::vector<Node> sremVec;
101 : : // scan the concatenation until we exhaust child proofs
102 [ + - ][ + - ]: 5431 : while (index < nchilds && index < nchildt)
103 : : {
104 [ + + ]: 5431 : Node currT = tvec[isRev ? (nchildt - 1 - index) : index];
105 [ + + ]: 5431 : Node currS = svec[isRev ? (nchilds - 1 - index) : index];
106 [ + + ]: 5431 : if (currT != currS)
107 : : {
108 : 3173 : break;
109 : : }
110 : 2258 : index++;
111 [ + + ][ + + ]: 8604 : }
112 [ - + ][ - + ]: 3173 : Assert(index <= nchildt);
[ - - ]
113 [ - + ][ - + ]: 3173 : Assert(index <= nchilds);
[ - - ]
114 : : // the remainders are equal
115 [ + + ][ + + ]: 9519 : tremVec.insert(isRev ? tremVec.begin() : tremVec.end(),
[ + + ]
116 : 3173 : tvec.begin() + (isRev ? 0 : index),
117 : 3173 : tvec.begin() + nchildt - (isRev ? index : 0));
118 [ + + ][ + + ]: 9519 : sremVec.insert(isRev ? sremVec.begin() : sremVec.end(),
[ + + ]
119 : 3173 : svec.begin() + (isRev ? 0 : index),
120 : 3173 : svec.begin() + nchilds - (isRev ? index : 0));
121 : : // convert back to node
122 : 3173 : Node trem = utils::mkConcat(tremVec, stringType);
123 : 3173 : Node srem = utils::mkConcat(sremVec, stringType);
124 : 3173 : return trem.eqNode(srem);
125 : 3173 : }
126 : : // all remaining rules do something with the first child of each side
127 [ + + ]: 2653 : Node t0 = tvec[isRev ? nchildt - 1 : 0];
128 [ + + ]: 2653 : Node s0 = svec[isRev ? nchilds - 1 : 0];
129 [ + + ]: 2653 : if (id == ProofRule::CONCAT_UNIFY)
130 : : {
131 [ - + ][ - + ]: 1362 : Assert(children.size() == 2);
[ - - ]
132 [ - + ]: 1362 : if (children[1].getKind() != Kind::EQUAL)
133 : : {
134 : 0 : return Node::null();
135 : : }
136 [ + + ]: 4086 : for (size_t i = 0; i < 2; i++)
137 : : {
138 : 2724 : Node l = children[1][i];
139 [ - + ]: 2724 : if (l.getKind() != Kind::STRING_LENGTH)
140 : : {
141 : 0 : return Node::null();
142 : : }
143 [ + + ]: 2724 : Node term = i == 0 ? t0 : s0;
144 [ + - ]: 2724 : if (l[0] == term)
145 : : {
146 : 2724 : continue;
147 : : }
148 : 0 : return Node::null();
149 [ + - ][ - + ]: 5448 : }
150 : 1362 : return children[1][0][0].eqNode(children[1][1][0]);
151 : : }
152 [ + + ]: 1291 : else if (id == ProofRule::CONCAT_SPLIT)
153 : : {
154 [ - + ][ - + ]: 55 : Assert(children.size() == 2);
[ - - ]
155 : 55 : if (children[1].getKind() != Kind::NOT
156 [ + - ][ - + ]: 110 : || children[1][0].getKind() != Kind::EQUAL
[ - - ]
157 : 110 : || children[1][0][0].getKind() != Kind::STRING_LENGTH
158 : 110 : || children[1][0][0][0] != t0
159 : 110 : || children[1][0][1].getKind() != Kind::STRING_LENGTH
160 : 165 : || children[1][0][1][0] != s0)
161 : : {
162 : 0 : return Node::null();
163 : : }
164 : : }
165 [ + + ]: 1236 : else if (id == ProofRule::CONCAT_CSPLIT)
166 : : {
167 [ - + ][ - + ]: 699 : Assert(children.size() == 2);
[ - - ]
168 : 699 : Node zero = nm->mkConstInt(Rational(0));
169 : 699 : Node one = nm->mkConstInt(Rational(1));
170 : 699 : if (children[1].getKind() != Kind::NOT
171 [ + - ][ - + ]: 1398 : || children[1][0].getKind() != Kind::EQUAL
[ - - ]
172 : 1398 : || children[1][0][0].getKind() != Kind::STRING_LENGTH
173 : 2097 : || children[1][0][0][0] != t0 || children[1][0][1] != zero)
174 : : {
175 : 0 : return Node::null();
176 : : }
177 : : // note we guard that the length must be one here, despite
178 : : // utils::getConcatConclusion allowing splicing below.
179 [ + - ][ - + ]: 1398 : if (!s0.isConst() || !s0.getType().isStringLike()
[ - - ]
180 [ + - ][ - + ]: 1398 : || Word::getLength(s0) != 1)
[ + - ][ + - ]
[ - - ]
181 : : {
182 : 0 : return Node::null();
183 : : }
184 [ + - ][ + - ]: 699 : }
185 [ + + ]: 537 : else if (id == ProofRule::CONCAT_LPROP)
186 : : {
187 [ - + ][ - + ]: 377 : Assert(children.size() == 2);
[ - - ]
188 : 377 : if (children[1].getKind() != Kind::GT
189 [ + - ][ - + ]: 754 : || children[1][0].getKind() != Kind::STRING_LENGTH
[ - - ]
190 : 754 : || children[1][0][0] != t0
191 [ + - ][ + - ]: 754 : || children[1][1].getKind() != Kind::STRING_LENGTH
[ - - ]
192 : 1131 : || children[1][1][0] != s0)
193 : : {
194 : 0 : return Node::null();
195 : : }
196 : : }
197 [ + - ]: 160 : else if (id == ProofRule::CONCAT_CPROP)
198 : : {
199 [ - + ][ - + ]: 160 : Assert(children.size() == 2);
[ - - ]
200 : 160 : Node zero = nm->mkConstInt(Rational(0));
201 : :
202 [ + - ]: 320 : Trace("pfcheck-strings-cprop")
203 : 160 : << "CONCAT_PROP, isRev=" << isRev << std::endl;
204 : 160 : if (children[1].getKind() != Kind::NOT
205 [ + - ][ - + ]: 320 : || children[1][0].getKind() != Kind::EQUAL
[ - - ]
206 : 320 : || children[1][0][0].getKind() != Kind::STRING_LENGTH
207 : 480 : || children[1][0][0][0] != t0 || children[1][0][1] != zero)
208 : : {
209 [ - - ]: 0 : Trace("pfcheck-strings-cprop")
210 : 0 : << "...failed pattern match" << std::endl;
211 : 0 : return Node::null();
212 : : }
213 [ - + ]: 160 : if (tvec.size() <= 1)
214 : : {
215 [ - - ]: 0 : Trace("pfcheck-strings-cprop")
216 : 0 : << "...failed adjacent constant" << std::endl;
217 : 0 : return Node::null();
218 : : }
219 [ + + ]: 160 : Node w1 = tvec[isRev ? nchildt - 2 : 1];
220 : 160 : if (!w1.isConst() || !w1.getType().isStringLike() || Word::isEmpty(w1))
221 : : {
222 [ - - ]: 0 : Trace("pfcheck-strings-cprop")
223 : 0 : << "...failed adjacent constant content" << std::endl;
224 : 0 : return Node::null();
225 : : }
226 : 160 : Node w2 = s0;
227 : 160 : if (!w2.isConst() || !w2.getType().isStringLike() || Word::isEmpty(w2))
228 : : {
229 [ - - ]: 0 : Trace("pfcheck-strings-cprop") << "...failed constant" << std::endl;
230 : 0 : return Node::null();
231 : : }
232 : : // getConcatConclusion expects the adjacent constant to be included
233 [ + + ][ + + ]: 160 : t0 = nm->mkNode(Kind::STRING_CONCAT, isRev ? w1 : t0, isRev ? t0 : w1);
234 [ + - ][ + - ]: 160 : }
[ + - ]
235 : : // use skolem cache
236 : 1291 : SkolemCache skc(nm, nullptr);
237 : 1291 : std::vector<Node> newSkolems;
238 : : Node conc = utils::getConcatConclusion(
239 : 2582 : nodeManager(), t0, s0, id, isRev, &skc, newSkolems);
240 : 1291 : return conc;
241 : 5826 : }
242 [ + + ]: 12685 : else if (id == ProofRule::STRING_DECOMPOSE)
243 : : {
244 [ - + ][ - + ]: 35 : Assert(children.size() == 2);
[ - - ]
245 [ - + ][ - + ]: 35 : Assert(args.size() == 1);
[ - - ]
246 : : bool isRev;
247 [ - + ]: 35 : if (!getBool(args[0], isRev))
248 : : {
249 : 0 : return Node::null();
250 : : }
251 : 35 : Node geq = children[0];
252 : 35 : Node atom = children[1];
253 : 35 : Node zero = nm->mkConstInt(Rational(0));
254 [ + - ][ - + ]: 35 : if (geq.getKind() != Kind::GEQ || geq[1] != zero)
[ + - ][ - + ]
[ - - ]
255 : : {
256 : 0 : return Node::null();
257 : : }
258 [ + - ][ - + ]: 70 : if (atom.getKind() != Kind::GEQ || atom[0].getKind() != Kind::STRING_LENGTH
[ - - ]
259 : 70 : || geq[0] != atom[1])
260 : : {
261 : 0 : return Node::null();
262 : : }
263 : 35 : SkolemCache skc(nm, nullptr);
264 : 35 : std::vector<Node> newSkolems;
265 : : Node conc = utils::getDecomposeConclusion(
266 : 70 : nodeManager(), atom[0][0], atom[1], isRev, &skc, newSkolems);
267 : 35 : return conc;
268 : 35 : }
269 [ + + ]: 12650 : else if (id == ProofRule::STRING_REDUCTION
270 [ + + ]: 11044 : || id == ProofRule::STRING_EAGER_REDUCTION
271 [ + + ]: 9909 : || id == ProofRule::STRING_LENGTH_POS)
272 : : {
273 [ - + ][ - + ]: 10964 : Assert(children.empty());
[ - - ]
274 [ - + ][ - + ]: 10964 : Assert(args.size() >= 1);
[ - - ]
275 : : // These rules are based on calling a C++ method for returning a valid
276 : : // lemma involving a single argument term.
277 : : // Must convert to skolem form.
278 : 10964 : Node t = args[0];
279 : 10964 : Node ret;
280 [ + + ]: 10964 : if (id == ProofRule::STRING_REDUCTION)
281 : : {
282 [ - + ][ - + ]: 1606 : Assert(args.size() == 1);
[ - - ]
283 : : // we do not use optimizations
284 : 1606 : SkolemCache skc(nm, nullptr);
285 : 1606 : std::vector<Node> conj;
286 : 1606 : ret = StringsPreprocess::reduce(t, conj, &skc, d_alphaCard);
287 : 1606 : conj.push_back(t.eqNode(ret));
288 : 1606 : ret = nm->mkAnd(conj);
289 : 1606 : }
290 [ + + ]: 9358 : else if (id == ProofRule::STRING_EAGER_REDUCTION)
291 : : {
292 [ - + ][ - + ]: 1135 : Assert(args.size() == 1);
[ - - ]
293 : 1135 : SkolemCache skc(nm, nullptr);
294 : 1135 : ret = utils::eagerReduce(t, &skc, d_alphaCard);
295 : 1135 : }
296 [ + - ]: 8223 : else if (id == ProofRule::STRING_LENGTH_POS)
297 : : {
298 [ - + ][ - + ]: 8223 : Assert(args.size() == 1);
[ - - ]
299 : 8223 : ret = utils::lengthPositive(t);
300 : : }
301 [ - + ]: 10964 : if (ret.isNull())
302 : : {
303 : 0 : return Node::null();
304 : : }
305 : 10964 : return ret;
306 : 10964 : }
307 [ + + ]: 1686 : else if (id == ProofRule::STRING_LENGTH_NON_EMPTY)
308 : : {
309 [ - + ][ - + ]: 866 : Assert(children.size() == 1);
[ - - ]
310 [ - + ][ - + ]: 866 : Assert(args.empty());
[ - - ]
311 : 866 : Node nemp = children[0];
312 [ + + ][ + + ]: 1700 : if (nemp.getKind() != Kind::NOT || nemp[0].getKind() != Kind::EQUAL
[ - - ]
313 : 1700 : || !nemp[0][1].isConst() || !nemp[0][1].getType().isStringLike())
314 : : {
315 : 173 : return Node::null();
316 : : }
317 [ - + ]: 693 : if (!Word::isEmpty(nemp[0][1]))
318 : : {
319 : 0 : return Node::null();
320 : : }
321 : 693 : Node zero = nm->mkConstInt(Rational(0));
322 : 1386 : Node clen = nm->mkNode(Kind::STRING_LENGTH, nemp[0][0]);
323 : 1386 : return clen.eqNode(zero).notNode();
324 : 866 : }
325 [ + + ]: 820 : else if (id == ProofRule::RE_INTER)
326 : : {
327 [ - + ]: 57 : if (children.size() < 2)
328 : : {
329 : 0 : return Node::null();
330 : : }
331 [ - + ][ - + ]: 57 : Assert(args.empty());
[ - - ]
332 : 57 : std::vector<Node> reis;
333 : 57 : Node x;
334 : : // make the regular expression intersection that summarizes all
335 : : // memberships in the explanation
336 [ + + ]: 171 : for (const Node& c : children)
337 : : {
338 [ - + ]: 114 : if (c.getKind() != Kind::STRING_IN_REGEXP)
339 : : {
340 : 0 : return Node::null();
341 : : }
342 [ + + ]: 114 : if (x.isNull())
343 : : {
344 : 57 : x = c[0];
345 : : }
346 [ - + ]: 57 : else if (x != c[0])
347 : : {
348 : : // different LHS
349 : 0 : return Node::null();
350 : : }
351 : 114 : reis.push_back(c[1]);
352 : : }
353 : 57 : Node rei = nm->mkNode(Kind::REGEXP_INTER, reis);
354 : 57 : return nm->mkNode(Kind::STRING_IN_REGEXP, x, rei);
355 : 57 : }
356 [ + + ]: 763 : else if (id == ProofRule::RE_CONCAT)
357 : : {
358 [ - + ]: 76 : if (children.size() < 2)
359 : : {
360 : 0 : return Node::null();
361 : : }
362 [ - + ][ - + ]: 76 : Assert(args.empty());
[ - - ]
363 : 76 : std::vector<Node> ts;
364 : 76 : std::vector<Node> rs;
365 : : // make the regular expression concatenation
366 [ + + ]: 430 : for (const Node& c : children)
367 : : {
368 [ - + ]: 354 : if (c.getKind() != Kind::STRING_IN_REGEXP)
369 : : {
370 : 0 : return Node::null();
371 : : }
372 : 354 : ts.push_back(c[0]);
373 : 354 : rs.push_back(c[1]);
374 : : }
375 : 76 : Node tc = nm->mkNode(Kind::STRING_CONCAT, ts);
376 : 76 : Node rc = nm->mkNode(Kind::REGEXP_CONCAT, rs);
377 : 76 : return nm->mkNode(Kind::STRING_IN_REGEXP, tc, rc);
378 : 76 : }
379 [ + + ][ + + ]: 687 : else if (id == ProofRule::RE_UNFOLD_POS || id == ProofRule::RE_UNFOLD_NEG
380 [ + + ]: 349 : || id == ProofRule::RE_UNFOLD_NEG_CONCAT_FIXED)
381 : : {
382 [ - + ][ - + ]: 366 : Assert(children.size() == 1);
[ - - ]
383 : 366 : Node skChild = children[0];
384 [ + + ]: 366 : if (id == ProofRule::RE_UNFOLD_NEG
385 [ + + ]: 362 : || id == ProofRule::RE_UNFOLD_NEG_CONCAT_FIXED)
386 : : {
387 : 96 : if (skChild.getKind() != Kind::NOT
388 [ + - ][ - + ]: 32 : || skChild[0].getKind() != Kind::STRING_IN_REGEXP)
[ + - ][ - + ]
[ - - ]
389 : : {
390 [ - - ]: 0 : Trace("strings-pfcheck") << "...fail, non-neg member" << std::endl;
391 : 0 : return Node::null();
392 : : }
393 : : }
394 [ - + ]: 334 : else if (skChild.getKind() != Kind::STRING_IN_REGEXP)
395 : : {
396 [ - - ]: 0 : Trace("strings-pfcheck") << "...fail, non-pos member" << std::endl;
397 : 0 : return Node::null();
398 : : }
399 : 366 : Node conc;
400 [ + + ]: 366 : if (id == ProofRule::RE_UNFOLD_POS)
401 : : {
402 [ - + ][ - + ]: 334 : Assert(args.empty());
[ - - ]
403 : 334 : std::vector<Node> newSkolems;
404 : 334 : SkolemCache skc(nodeManager(), nullptr);
405 : : conc =
406 : 334 : RegExpOpr::reduceRegExpPos(nodeManager(), skChild, &skc, newSkolems);
407 : 334 : }
408 [ + + ]: 32 : else if (id == ProofRule::RE_UNFOLD_NEG)
409 : : {
410 [ - + ][ - + ]: 4 : Assert(args.empty());
[ - - ]
411 : 4 : conc = RegExpOpr::reduceRegExpNeg(nodeManager(), skChild);
412 : : }
413 [ + - ]: 28 : else if (id == ProofRule::RE_UNFOLD_NEG_CONCAT_FIXED)
414 : : {
415 [ - + ][ - + ]: 28 : Assert(args.size() == 1);
[ - - ]
416 : : bool isRev;
417 [ - + ]: 28 : if (!getBool(args[0], isRev))
418 : : {
419 : 0 : return Node::null();
420 : : }
421 : 28 : Node r = skChild[0][1];
422 [ - + ]: 28 : if (r.getKind() != Kind::REGEXP_CONCAT)
423 : : {
424 [ - - ]: 0 : Trace("strings-pfcheck") << "...fail, no concat regexp" << std::endl;
425 : 0 : return Node::null();
426 : : }
427 [ + + ]: 28 : size_t index = isRev ? r.getNumChildren() - 1 : 0;
428 : 56 : Node reLen = RegExpEntail::getFixedLengthForRegexp(r[index]);
429 [ - + ]: 28 : if (reLen.isNull())
430 : : {
431 [ - - ]: 0 : Trace("strings-pfcheck") << "...fail, non-fixed lengths" << std::endl;
432 : 0 : return Node::null();
433 : : }
434 : 56 : conc = RegExpOpr::reduceRegExpNegConcatFixed(
435 : 28 : nodeManager(), skChild, reLen, isRev);
436 [ + - ][ + - ]: 28 : }
437 : 366 : return conc;
438 : 366 : }
439 [ + + ]: 321 : else if (id == ProofRule::STRING_CODE_INJ)
440 : : {
441 [ - + ][ - + ]: 74 : Assert(children.empty());
[ - - ]
442 [ - + ][ - + ]: 74 : Assert(args.size() == 2);
[ - - ]
443 : 74 : Assert(args[0].getType().isStringLike()
444 : : && args[1].getType().isStringLike());
445 : 74 : Node c1 = nm->mkNode(Kind::STRING_TO_CODE, args[0]);
446 : 74 : Node c2 = nm->mkNode(Kind::STRING_TO_CODE, args[1]);
447 : 148 : Node eqNegOne = c1.eqNode(nm->mkConstInt(Rational(-1)));
448 : 74 : Node deq = c1.eqNode(c2).negate();
449 : 74 : Node eqn = args[0].eqNode(args[1]);
450 : 74 : return nm->mkNode(Kind::OR, eqNegOne, deq, eqn);
451 : 74 : }
452 [ + + ]: 247 : else if (id == ProofRule::STRING_SEQ_UNIT_INJ)
453 : : {
454 [ - + ][ - + ]: 43 : Assert(children.size() == 1);
[ - - ]
455 [ - + ][ - + ]: 43 : Assert(args.empty());
[ - - ]
456 [ - + ]: 43 : if (children[0].getKind() != Kind::EQUAL)
457 : : {
458 : 0 : return Node::null();
459 : : }
460 [ + + ]: 258 : Node t[2];
461 [ + + ]: 129 : for (size_t i = 0; i < 2; i++)
462 : : {
463 : 86 : Node c = children[0][i];
464 : 86 : Kind k = c.getKind();
465 [ + + ][ - + ]: 86 : if (k == Kind::SEQ_UNIT || k == Kind::STRING_UNIT)
466 : : {
467 : 78 : t[i] = c[0];
468 : : }
469 [ + - ]: 8 : else if (c.isConst())
470 : : {
471 : : // notice that Word::getChars is not the right call here, since it
472 : : // gets a vector of sequences of length one. We actually need to
473 : : // extract the character.
474 [ + - ]: 8 : if (Word::getLength(c) == 1)
475 : : {
476 : 8 : t[i] = Word::getNth(c, 0);
477 : : }
478 : : }
479 [ - + ]: 86 : if (t[i].isNull())
480 : : {
481 : 0 : return Node::null();
482 : : }
483 [ + - ]: 86 : }
484 [ + - ]: 86 : Trace("strings-pfcheck-debug")
485 : 0 : << "STRING_SEQ_UNIT_INJ: " << children[0] << " => " << t[0]
486 : 43 : << " == " << t[1] << std::endl;
487 [ - + ][ - + ]: 129 : AlwaysAssert(CVC5_EQUAL(t[0].getType(), t[1].getType()));
[ - - ]
488 : 43 : return t[0].eqNode(t[1]);
489 [ + + ][ - - ]: 129 : }
490 [ + + ]: 204 : else if (id == ProofRule::STRING_EXT)
491 : : {
492 [ - + ][ - + ]: 40 : Assert(children.size() == 1);
[ - - ]
493 [ - + ][ - + ]: 40 : Assert(args.empty());
[ - - ]
494 : 40 : Node deq = children[0];
495 [ + - ][ - + ]: 80 : if (deq.getKind() != Kind::NOT || deq[0].getKind() != Kind::EQUAL
[ - - ]
496 : 80 : || !deq[0][0].getType().isStringLike())
497 : : {
498 : 0 : return Node::null();
499 : : }
500 : 40 : SkolemCache skc(nm, nullptr);
501 : 40 : return utils::getExtensionalityConclusion(nm, deq[0][0], deq[0][1], &skc);
502 : 40 : }
503 [ + - ]: 164 : else if (id == ProofRule::MACRO_STRING_INFERENCE)
504 : : {
505 [ - + ][ - + ]: 164 : Assert(args.size() >= 3);
[ - - ]
506 : 164 : return args[0];
507 : : }
508 : 0 : return Node::null();
509 : : }
510 : :
511 : : } // namespace strings
512 : : } // namespace theory
513 : : } // namespace cvc5::internal
|
