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