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