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 : 49981 : StringProofRuleChecker::StringProofRuleChecker(NodeManager* nm,
34 : 49981 : uint32_t alphaCard)
35 : 49981 : : ProofRuleChecker(nm), d_alphaCard(alphaCard)
36 : : {
37 : 49981 : }
38 : :
39 : 18918 : void StringProofRuleChecker::registerTo(ProofChecker* pc)
40 : : {
41 : 18918 : pc->registerChecker(ProofRule::CONCAT_EQ, this);
42 : 18918 : pc->registerChecker(ProofRule::CONCAT_UNIFY, this);
43 : 18918 : pc->registerChecker(ProofRule::CONCAT_SPLIT, this);
44 : 18918 : pc->registerChecker(ProofRule::CONCAT_CSPLIT, this);
45 : 18918 : pc->registerChecker(ProofRule::CONCAT_LPROP, this);
46 : 18918 : pc->registerChecker(ProofRule::CONCAT_CPROP, this);
47 : 18918 : pc->registerChecker(ProofRule::STRING_DECOMPOSE, this);
48 : 18918 : pc->registerChecker(ProofRule::STRING_LENGTH_POS, this);
49 : 18918 : pc->registerChecker(ProofRule::STRING_LENGTH_NON_EMPTY, this);
50 : 18918 : pc->registerChecker(ProofRule::STRING_REDUCTION, this);
51 : 18918 : pc->registerChecker(ProofRule::STRING_EAGER_REDUCTION, this);
52 : 18918 : pc->registerChecker(ProofRule::RE_INTER, this);
53 : 18918 : pc->registerChecker(ProofRule::RE_CONCAT, this);
54 : 18918 : pc->registerChecker(ProofRule::RE_UNFOLD_POS, this);
55 : 18918 : pc->registerChecker(ProofRule::RE_UNFOLD_NEG, this);
56 : 18918 : pc->registerChecker(ProofRule::RE_UNFOLD_NEG_CONCAT_FIXED, this);
57 : 18918 : pc->registerChecker(ProofRule::STRING_CODE_INJ, this);
58 : 18918 : pc->registerChecker(ProofRule::STRING_SEQ_UNIT_INJ, this);
59 : 18918 : pc->registerChecker(ProofRule::STRING_EXT, this);
60 : : // trusted rule
61 : 18918 : pc->registerTrustedChecker(ProofRule::MACRO_STRING_INFERENCE, this, 2);
62 : 18918 : }
63 : :
64 : 25610 : Node StringProofRuleChecker::checkInternal(ProofRule id,
65 : : const std::vector<Node>& children,
66 : : const std::vector<Node>& args)
67 : : {
68 : 25610 : NodeManager* nm = nodeManager();
69 : : // core rules for word equations
70 [ + + ][ + + ]: 25610 : if (id == ProofRule::CONCAT_EQ || id == ProofRule::CONCAT_UNIFY
71 [ + + ][ + + ]: 18334 : || id == ProofRule::CONCAT_SPLIT || id == ProofRule::CONCAT_CSPLIT
72 [ + + ][ + + ]: 16989 : || id == ProofRule::CONCAT_LPROP || id == ProofRule::CONCAT_CPROP)
73 : : {
74 [ + - ]: 9569 : Trace("strings-pfcheck") << "Checking id " << id << std::endl;
75 [ - + ][ - + ]: 9569 : Assert(children.size() >= 1);
[ - - ]
76 [ - + ][ - + ]: 9569 : Assert(args.size() == 1);
[ - - ]
77 : : // all rules have an equality
78 [ - + ]: 9569 : if (children[0].getKind() != Kind::EQUAL)
79 : : {
80 : 0 : return Node::null();
81 : : }
82 : : // convert to concatenation form
83 : 9569 : std::vector<Node> tvec;
84 : 9569 : std::vector<Node> svec;
85 : 9569 : utils::getConcat(children[0][0], tvec);
86 : 9569 : utils::getConcat(children[0][1], svec);
87 : 9569 : size_t nchildt = tvec.size();
88 : 9569 : size_t nchilds = svec.size();
89 : 9569 : TypeNode stringType = children[0][0].getType();
90 : : // extract the Boolean corresponding to whether the rule is reversed
91 : : bool isRev;
92 [ - + ]: 9569 : if (!getBool(args[0], isRev))
93 : : {
94 : 0 : return Node::null();
95 : : }
96 [ + + ]: 9569 : if (id == ProofRule::CONCAT_EQ)
97 : : {
98 [ - + ][ - + ]: 4925 : Assert(children.size() == 1);
[ - - ]
99 : 4925 : size_t index = 0;
100 : 4925 : std::vector<Node> tremVec;
101 : 4925 : std::vector<Node> sremVec;
102 : : // scan the concatenation until we exhaust child proofs
103 [ + - ][ + - ]: 8786 : while (index < nchilds && index < nchildt)
104 : : {
105 [ + + ]: 8786 : Node currT = tvec[isRev ? (nchildt - 1 - index) : index];
106 [ + + ]: 8786 : Node currS = svec[isRev ? (nchilds - 1 - index) : index];
107 [ + + ]: 8786 : if (currT != currS)
108 : : {
109 : 4925 : break;
110 : : }
111 : 3861 : index++;
112 [ + + ][ + + ]: 13711 : }
113 [ - + ][ - + ]: 4925 : Assert(index <= nchildt);
[ - - ]
114 [ - + ][ - + ]: 4925 : Assert(index <= nchilds);
[ - - ]
115 : : // the remainders are equal
116 [ + + ][ + + ]: 14775 : tremVec.insert(isRev ? tremVec.begin() : tremVec.end(),
[ + + ]
117 : 4925 : tvec.begin() + (isRev ? 0 : index),
118 : 4925 : tvec.begin() + nchildt - (isRev ? index : 0));
119 [ + + ][ + + ]: 14775 : sremVec.insert(isRev ? sremVec.begin() : sremVec.end(),
[ + + ]
120 : 4925 : svec.begin() + (isRev ? 0 : index),
121 : 4925 : svec.begin() + nchilds - (isRev ? index : 0));
122 : : // convert back to node
123 : 4925 : Node trem = utils::mkConcat(tremVec, stringType);
124 : 4925 : Node srem = utils::mkConcat(sremVec, stringType);
125 : 4925 : return trem.eqNode(srem);
126 : 4925 : }
127 : : // all remaining rules do something with the first child of each side
128 [ + + ]: 4644 : Node t0 = tvec[isRev ? nchildt - 1 : 0];
129 [ + + ]: 4644 : Node s0 = svec[isRev ? nchilds - 1 : 0];
130 [ + + ]: 4644 : if (id == ProofRule::CONCAT_UNIFY)
131 : : {
132 [ - + ][ - + ]: 2351 : Assert(children.size() == 2);
[ - - ]
133 [ - + ]: 2351 : if (children[1].getKind() != Kind::EQUAL)
134 : : {
135 : 0 : return Node::null();
136 : : }
137 [ + + ]: 7053 : for (size_t i = 0; i < 2; i++)
138 : : {
139 : 4702 : Node l = children[1][i];
140 [ - + ]: 4702 : if (l.getKind() != Kind::STRING_LENGTH)
141 : : {
142 : 0 : return Node::null();
143 : : }
144 [ + + ]: 4702 : Node term = i == 0 ? t0 : s0;
145 [ + - ]: 4702 : if (l[0] == term)
146 : : {
147 : 4702 : continue;
148 : : }
149 : 0 : return Node::null();
150 [ + - ][ - + ]: 9404 : }
151 : 2351 : 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 : 9569 : }
243 [ + + ]: 16041 : 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 [ + + ]: 15993 : else if (id == ProofRule::STRING_REDUCTION
271 [ + + ]: 13616 : || id == ProofRule::STRING_EAGER_REDUCTION
272 [ + + ]: 12312 : || id == ProofRule::STRING_LENGTH_POS)
273 : : {
274 [ - + ][ - + ]: 13490 : Assert(children.empty());
[ - - ]
275 [ - + ][ - + ]: 13490 : 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 : 13490 : Node t = args[0];
280 : 13490 : Node ret;
281 [ + + ]: 13490 : if (id == ProofRule::STRING_REDUCTION)
282 : : {
283 [ - + ][ - + ]: 2377 : Assert(args.size() == 1);
[ - - ]
284 : : // we do not use optimizations
285 : 2377 : SkolemCache skc(nm, nullptr);
286 : 2377 : std::vector<Node> conj;
287 : 2377 : ret = StringsPreprocess::reduce(t, conj, &skc, d_alphaCard);
288 : 2377 : conj.push_back(t.eqNode(ret));
289 : 2377 : ret = nm->mkAnd(conj);
290 : 2377 : }
291 [ + + ]: 11113 : else if (id == ProofRule::STRING_EAGER_REDUCTION)
292 : : {
293 [ - + ][ - + ]: 1304 : Assert(args.size() == 1);
[ - - ]
294 : 1304 : SkolemCache skc(nm, nullptr);
295 : 1304 : ret = TermRegistry::eagerReduce(t, &skc, d_alphaCard);
296 : 1304 : }
297 [ + - ]: 9809 : else if (id == ProofRule::STRING_LENGTH_POS)
298 : : {
299 [ - + ][ - + ]: 9809 : Assert(args.size() == 1);
[ - - ]
300 : 9809 : ret = TermRegistry::lengthPositive(t);
301 : : }
302 [ - + ]: 13490 : if (ret.isNull())
303 : : {
304 : 0 : return Node::null();
305 : : }
306 : 13490 : return ret;
307 : 13490 : }
308 [ + + ]: 2503 : else if (id == ProofRule::STRING_LENGTH_NON_EMPTY)
309 : : {
310 [ - + ][ - + ]: 1268 : Assert(children.size() == 1);
[ - - ]
311 [ - + ][ - + ]: 1268 : Assert(args.empty());
[ - - ]
312 : 1268 : Node nemp = children[0];
313 [ + + ][ + + ]: 2504 : if (nemp.getKind() != Kind::NOT || nemp[0].getKind() != Kind::EQUAL
[ - - ]
314 : 2504 : || !nemp[0][1].isConst() || !nemp[0][1].getType().isStringLike())
315 : : {
316 : 248 : return Node::null();
317 : : }
318 [ - + ]: 1020 : if (!Word::isEmpty(nemp[0][1]))
319 : : {
320 : 0 : return Node::null();
321 : : }
322 : 1020 : Node zero = nm->mkConstInt(Rational(0));
323 : 2040 : Node clen = nm->mkNode(Kind::STRING_LENGTH, nemp[0][0]);
324 : 2040 : return clen.eqNode(zero).notNode();
325 : 1268 : }
326 [ + + ]: 1235 : else if (id == ProofRule::RE_INTER)
327 : : {
328 [ - + ][ - + ]: 58 : Assert(children.size() >= 1);
[ - - ]
329 [ - + ][ - + ]: 58 : Assert(args.empty());
[ - - ]
330 : 58 : std::vector<Node> reis;
331 : 58 : Node x;
332 : : // make the regular expression intersection that summarizes all
333 : : // memberships in the explanation
334 [ + + ]: 174 : for (const Node& c : children)
335 : : {
336 [ - + ]: 116 : if (c.getKind() != Kind::STRING_IN_REGEXP)
337 : : {
338 : 0 : return Node::null();
339 : : }
340 [ + + ]: 116 : if (x.isNull())
341 : : {
342 : 58 : x = c[0];
343 : : }
344 [ - + ]: 58 : else if (x != c[0])
345 : : {
346 : : // different LHS
347 : 0 : return Node::null();
348 : : }
349 : 116 : reis.push_back(c[1]);
350 : : }
351 : : Node rei =
352 [ - + ]: 58 : reis.size() == 1 ? reis[0] : nm->mkNode(Kind::REGEXP_INTER, reis);
353 : 58 : return nm->mkNode(Kind::STRING_IN_REGEXP, x, rei);
354 : 58 : }
355 [ + + ]: 1177 : else if (id == ProofRule::RE_CONCAT)
356 : : {
357 [ - + ]: 36 : if (children.size() < 2)
358 : : {
359 : 0 : return Node::null();
360 : : }
361 [ - + ][ - + ]: 36 : Assert(args.empty());
[ - - ]
362 : 36 : std::vector<Node> ts;
363 : 36 : std::vector<Node> rs;
364 : : // make the regular expression concatenation
365 [ + + ]: 234 : for (const Node& c : children)
366 : : {
367 [ - + ]: 198 : if (c.getKind() != Kind::STRING_IN_REGEXP)
368 : : {
369 : 0 : return Node::null();
370 : : }
371 : 198 : ts.push_back(c[0]);
372 : 198 : rs.push_back(c[1]);
373 : : }
374 : 36 : Node tc = nm->mkNode(Kind::STRING_CONCAT, ts);
375 : 36 : Node rc = nm->mkNode(Kind::REGEXP_CONCAT, rs);
376 : 36 : return nm->mkNode(Kind::STRING_IN_REGEXP, tc, rc);
377 : 36 : }
378 [ + + ][ + - ]: 1141 : else if (id == ProofRule::RE_UNFOLD_POS || id == ProofRule::RE_UNFOLD_NEG
379 [ + + ]: 653 : || id == ProofRule::RE_UNFOLD_NEG_CONCAT_FIXED)
380 : : {
381 [ - + ][ - + ]: 530 : Assert(children.size() == 1);
[ - - ]
382 : 530 : Node skChild = children[0];
383 [ + - ]: 530 : if (id == ProofRule::RE_UNFOLD_NEG
384 [ + + ]: 530 : || id == ProofRule::RE_UNFOLD_NEG_CONCAT_FIXED)
385 : : {
386 : 126 : if (skChild.getKind() != Kind::NOT
387 [ + - ][ - + ]: 42 : || skChild[0].getKind() != Kind::STRING_IN_REGEXP)
[ + - ][ - + ]
[ - - ]
388 : : {
389 [ - - ]: 0 : Trace("strings-pfcheck") << "...fail, non-neg member" << std::endl;
390 : 0 : return Node::null();
391 : : }
392 : : }
393 [ - + ]: 488 : else if (skChild.getKind() != Kind::STRING_IN_REGEXP)
394 : : {
395 [ - - ]: 0 : Trace("strings-pfcheck") << "...fail, non-pos member" << std::endl;
396 : 0 : return Node::null();
397 : : }
398 : 530 : Node conc;
399 [ + + ]: 530 : if (id == ProofRule::RE_UNFOLD_POS)
400 : : {
401 [ - + ][ - + ]: 488 : Assert(args.empty());
[ - - ]
402 : 488 : std::vector<Node> newSkolems;
403 : 488 : SkolemCache skc(nodeManager(), nullptr);
404 : : conc =
405 : 488 : RegExpOpr::reduceRegExpPos(nodeManager(), skChild, &skc, newSkolems);
406 : 488 : }
407 [ - + ]: 42 : else if (id == ProofRule::RE_UNFOLD_NEG)
408 : : {
409 : 0 : Assert(args.empty());
410 : 0 : conc = RegExpOpr::reduceRegExpNeg(nodeManager(), skChild);
411 : : }
412 [ + - ]: 42 : else if (id == ProofRule::RE_UNFOLD_NEG_CONCAT_FIXED)
413 : : {
414 [ - + ][ - + ]: 42 : Assert(args.size() == 1);
[ - - ]
415 : : bool isRev;
416 [ - + ]: 42 : if (!getBool(args[0], isRev))
417 : : {
418 : 0 : return Node::null();
419 : : }
420 : 42 : Node r = skChild[0][1];
421 [ - + ]: 42 : if (r.getKind() != Kind::REGEXP_CONCAT)
422 : : {
423 [ - - ]: 0 : Trace("strings-pfcheck") << "...fail, no concat regexp" << std::endl;
424 : 0 : return Node::null();
425 : : }
426 [ + + ]: 42 : size_t index = isRev ? r.getNumChildren() - 1 : 0;
427 : 84 : Node reLen = RegExpEntail::getFixedLengthForRegexp(r[index]);
428 [ - + ]: 42 : if (reLen.isNull())
429 : : {
430 [ - - ]: 0 : Trace("strings-pfcheck") << "...fail, non-fixed lengths" << std::endl;
431 : 0 : return Node::null();
432 : : }
433 : 84 : conc = RegExpOpr::reduceRegExpNegConcatFixed(
434 : 42 : nodeManager(), skChild, reLen, isRev);
435 [ + - ][ + - ]: 42 : }
436 : 530 : return conc;
437 : 530 : }
438 [ + + ]: 611 : else if (id == ProofRule::STRING_CODE_INJ)
439 : : {
440 [ - + ][ - + ]: 96 : Assert(children.empty());
[ - - ]
441 [ - + ][ - + ]: 96 : Assert(args.size() == 2);
[ - - ]
442 : 96 : Assert(args[0].getType().isStringLike()
443 : : && args[1].getType().isStringLike());
444 : 96 : Node c1 = nm->mkNode(Kind::STRING_TO_CODE, args[0]);
445 : 96 : Node c2 = nm->mkNode(Kind::STRING_TO_CODE, args[1]);
446 : 192 : Node eqNegOne = c1.eqNode(nm->mkConstInt(Rational(-1)));
447 : 96 : Node deq = c1.eqNode(c2).negate();
448 : 96 : Node eqn = args[0].eqNode(args[1]);
449 : 96 : return nm->mkNode(Kind::OR, eqNegOne, deq, eqn);
450 : 96 : }
451 [ + + ]: 515 : else if (id == ProofRule::STRING_SEQ_UNIT_INJ)
452 : : {
453 [ - + ][ - + ]: 65 : Assert(children.size() == 1);
[ - - ]
454 [ - + ][ - + ]: 65 : Assert(args.empty());
[ - - ]
455 [ - + ]: 65 : if (children[0].getKind() != Kind::EQUAL)
456 : : {
457 : 0 : return Node::null();
458 : : }
459 [ + + ]: 390 : Node t[2];
460 [ + + ]: 195 : for (size_t i = 0; i < 2; i++)
461 : : {
462 : 130 : Node c = children[0][i];
463 : 130 : Kind k = c.getKind();
464 [ + + ][ - + ]: 130 : if (k == Kind::SEQ_UNIT || k == Kind::STRING_UNIT)
465 : : {
466 : 118 : t[i] = c[0];
467 : : }
468 [ + - ]: 12 : else if (c.isConst())
469 : : {
470 : : // notice that Word::getChars is not the right call here, since it
471 : : // gets a vector of sequences of length one. We actually need to
472 : : // extract the character.
473 [ + - ]: 12 : if (Word::getLength(c) == 1)
474 : : {
475 : 12 : t[i] = Word::getNth(c, 0);
476 : : }
477 : : }
478 [ - + ]: 130 : if (t[i].isNull())
479 : : {
480 : 0 : return Node::null();
481 : : }
482 [ + - ]: 130 : }
483 [ + - ]: 130 : Trace("strings-pfcheck-debug")
484 : 0 : << "STRING_SEQ_UNIT_INJ: " << children[0] << " => " << t[0]
485 : 65 : << " == " << t[1] << std::endl;
486 [ - + ][ - + ]: 65 : AlwaysAssert(t[0].getType() == t[1].getType());
[ - - ]
487 : 65 : return t[0].eqNode(t[1]);
488 [ + + ][ - - ]: 195 : }
489 [ + + ]: 450 : else if (id == ProofRule::STRING_EXT)
490 : : {
491 [ - + ][ - + ]: 48 : Assert(children.size() == 1);
[ - - ]
492 [ - + ][ - + ]: 48 : Assert(args.empty());
[ - - ]
493 : 48 : Node deq = children[0];
494 [ + - ][ - + ]: 96 : if (deq.getKind() != Kind::NOT || deq[0].getKind() != Kind::EQUAL
[ - - ]
495 : 96 : || !deq[0][0].getType().isStringLike())
496 : : {
497 : 0 : return Node::null();
498 : : }
499 : 48 : SkolemCache skc(nm, nullptr);
500 : : return CoreSolver::getExtensionalityConclusion(
501 : 48 : nm, deq[0][0], deq[0][1], &skc);
502 : 48 : }
503 [ + - ]: 402 : else if (id == ProofRule::MACRO_STRING_INFERENCE)
504 : : {
505 [ - + ][ - + ]: 402 : Assert(args.size() >= 3);
[ - - ]
506 : 402 : return args[0];
507 : : }
508 : 0 : return Node::null();
509 : : }
510 : :
511 : : } // namespace strings
512 : : } // namespace theory
513 : : } // namespace cvc5::internal
|
