1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Aina Niemetz |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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_operation.h" |
24 |
|
#include "theory/strings/term_registry.h" |
25 |
|
#include "theory/strings/theory_strings_preprocess.h" |
26 |
|
#include "theory/strings/theory_strings_utils.h" |
27 |
|
#include "theory/strings/word.h" |
28 |
|
|
29 |
|
using namespace cvc5::kind; |
30 |
|
|
31 |
|
namespace cvc5 { |
32 |
|
namespace theory { |
33 |
|
namespace strings { |
34 |
|
|
35 |
3600 |
void StringProofRuleChecker::registerTo(ProofChecker* pc) |
36 |
|
{ |
37 |
3600 |
pc->registerChecker(PfRule::CONCAT_EQ, this); |
38 |
3600 |
pc->registerChecker(PfRule::CONCAT_UNIFY, this); |
39 |
3600 |
pc->registerChecker(PfRule::CONCAT_CONFLICT, this); |
40 |
3600 |
pc->registerChecker(PfRule::CONCAT_SPLIT, this); |
41 |
3600 |
pc->registerChecker(PfRule::CONCAT_CSPLIT, this); |
42 |
3600 |
pc->registerChecker(PfRule::CONCAT_LPROP, this); |
43 |
3600 |
pc->registerChecker(PfRule::CONCAT_CPROP, this); |
44 |
3600 |
pc->registerChecker(PfRule::STRING_DECOMPOSE, this); |
45 |
3600 |
pc->registerChecker(PfRule::STRING_LENGTH_POS, this); |
46 |
3600 |
pc->registerChecker(PfRule::STRING_LENGTH_NON_EMPTY, this); |
47 |
3600 |
pc->registerChecker(PfRule::STRING_REDUCTION, this); |
48 |
3600 |
pc->registerChecker(PfRule::STRING_EAGER_REDUCTION, this); |
49 |
3600 |
pc->registerChecker(PfRule::RE_INTER, this); |
50 |
3600 |
pc->registerChecker(PfRule::RE_UNFOLD_POS, this); |
51 |
3600 |
pc->registerChecker(PfRule::RE_UNFOLD_NEG, this); |
52 |
3600 |
pc->registerChecker(PfRule::RE_UNFOLD_NEG_CONCAT_FIXED, this); |
53 |
3600 |
pc->registerChecker(PfRule::RE_ELIM, this); |
54 |
3600 |
pc->registerChecker(PfRule::STRING_CODE_INJ, this); |
55 |
3600 |
pc->registerChecker(PfRule::STRING_SEQ_UNIT_INJ, this); |
56 |
|
// trusted rules |
57 |
3600 |
pc->registerTrustedChecker(PfRule::STRING_TRUST, this, 2); |
58 |
3600 |
} |
59 |
|
|
60 |
2821 |
Node StringProofRuleChecker::checkInternal(PfRule id, |
61 |
|
const std::vector<Node>& children, |
62 |
|
const std::vector<Node>& args) |
63 |
|
{ |
64 |
2821 |
NodeManager* nm = NodeManager::currentNM(); |
65 |
|
// core rules for word equations |
66 |
2821 |
if (id == PfRule::CONCAT_EQ || id == PfRule::CONCAT_UNIFY |
67 |
1960 |
|| id == PfRule::CONCAT_CONFLICT || id == PfRule::CONCAT_SPLIT |
68 |
1957 |
|| id == PfRule::CONCAT_CSPLIT || id == PfRule::CONCAT_LPROP |
69 |
1786 |
|| id == PfRule::CONCAT_CPROP) |
70 |
|
{ |
71 |
1035 |
Trace("strings-pfcheck") << "Checking id " << id << std::endl; |
72 |
1035 |
Assert(children.size() >= 1); |
73 |
1035 |
Assert(args.size() == 1); |
74 |
|
// all rules have an equality |
75 |
1035 |
if (children[0].getKind() != EQUAL) |
76 |
|
{ |
77 |
|
return Node::null(); |
78 |
|
} |
79 |
|
// convert to concatenation form |
80 |
2070 |
std::vector<Node> tvec; |
81 |
2070 |
std::vector<Node> svec; |
82 |
1035 |
utils::getConcat(children[0][0], tvec); |
83 |
1035 |
utils::getConcat(children[0][1], svec); |
84 |
1035 |
size_t nchildt = tvec.size(); |
85 |
1035 |
size_t nchilds = svec.size(); |
86 |
2070 |
TypeNode stringType = children[0][0].getType(); |
87 |
|
// extract the Boolean corresponding to whether the rule is reversed |
88 |
|
bool isRev; |
89 |
1035 |
if (!getBool(args[0], isRev)) |
90 |
|
{ |
91 |
|
return Node::null(); |
92 |
|
} |
93 |
1035 |
if (id == PfRule::CONCAT_EQ) |
94 |
|
{ |
95 |
603 |
Assert(children.size() == 1); |
96 |
603 |
size_t index = 0; |
97 |
1206 |
std::vector<Node> tremVec; |
98 |
1206 |
std::vector<Node> sremVec; |
99 |
|
// scan the concatenation until we exhaust child proofs |
100 |
1213 |
while (index < nchilds && index < nchildt) |
101 |
|
{ |
102 |
1213 |
Node currT = tvec[isRev ? (nchildt - 1 - index) : index]; |
103 |
1213 |
Node currS = svec[isRev ? (nchilds - 1 - index) : index]; |
104 |
908 |
if (currT != currS) |
105 |
|
{ |
106 |
603 |
if (currT.isConst() && currS.isConst()) |
107 |
|
{ |
108 |
|
size_t sindex; |
109 |
|
// get the equal prefix/suffix, strip and add the remainders |
110 |
534 |
Node currR = Word::splitConstant(currT, currS, sindex, isRev); |
111 |
267 |
if (!currR.isNull()) |
112 |
|
{ |
113 |
|
// add the constant to remainder vec |
114 |
267 |
std::vector<Node>& rem = sindex == 0 ? tremVec : sremVec; |
115 |
267 |
rem.push_back(currR); |
116 |
|
// ignore the current component |
117 |
267 |
index++; |
118 |
|
// In other words, if we have (currS,currT) = ("ab","abc"), then |
119 |
|
// we proceed to the next component and add currR = "c" to |
120 |
|
// tremVec. |
121 |
|
} |
122 |
|
// otherwise if we are not the same prefix, then both will be added |
123 |
|
// Notice that we do not add maximal prefixes, in other words, |
124 |
|
// ("abc", "abd") may be added to the remainder vectors, and not |
125 |
|
// ("c", "d"). |
126 |
|
} |
127 |
603 |
break; |
128 |
|
} |
129 |
305 |
index++; |
130 |
|
} |
131 |
603 |
Assert(index <= nchildt); |
132 |
603 |
Assert(index <= nchilds); |
133 |
|
// the remainders are equal |
134 |
1809 |
tremVec.insert(isRev ? tremVec.begin() : tremVec.end(), |
135 |
1206 |
tvec.begin() + (isRev ? 0 : index), |
136 |
3015 |
tvec.begin() + nchildt - (isRev ? index : 0)); |
137 |
1809 |
sremVec.insert(isRev ? sremVec.begin() : sremVec.end(), |
138 |
1206 |
svec.begin() + (isRev ? 0 : index), |
139 |
3015 |
svec.begin() + nchilds - (isRev ? index : 0)); |
140 |
|
// convert back to node |
141 |
1206 |
Node trem = utils::mkConcat(tremVec, stringType); |
142 |
1206 |
Node srem = utils::mkConcat(sremVec, stringType); |
143 |
603 |
return trem.eqNode(srem); |
144 |
|
} |
145 |
|
// all remaining rules do something with the first child of each side |
146 |
864 |
Node t0 = tvec[isRev ? nchildt - 1 : 0]; |
147 |
864 |
Node s0 = svec[isRev ? nchilds - 1 : 0]; |
148 |
432 |
if (id == PfRule::CONCAT_UNIFY) |
149 |
|
{ |
150 |
258 |
Assert(children.size() == 2); |
151 |
258 |
if (children[1].getKind() != EQUAL) |
152 |
|
{ |
153 |
|
return Node::null(); |
154 |
|
} |
155 |
772 |
for (size_t i = 0; i < 2; i++) |
156 |
|
{ |
157 |
534 |
Node l = children[1][i]; |
158 |
516 |
if (l.getKind() != STRING_LENGTH) |
159 |
|
{ |
160 |
|
return Node::null(); |
161 |
|
} |
162 |
534 |
Node term = i == 0 ? t0 : s0; |
163 |
516 |
if (l[0] == term) |
164 |
|
{ |
165 |
496 |
continue; |
166 |
|
} |
167 |
|
// could be a spliced constant |
168 |
20 |
bool success = false; |
169 |
20 |
if (term.isConst() && l[0].isConst()) |
170 |
|
{ |
171 |
18 |
size_t lenL = Word::getLength(l[0]); |
172 |
36 |
success = (isRev && l[0] == Word::suffix(term, lenL)) |
173 |
54 |
|| (!isRev && l[0] == Word::prefix(term, lenL)); |
174 |
|
} |
175 |
20 |
if (!success) |
176 |
|
{ |
177 |
2 |
return Node::null(); |
178 |
|
} |
179 |
|
} |
180 |
256 |
return children[1][0][0].eqNode(children[1][1][0]); |
181 |
|
} |
182 |
174 |
else if (id == PfRule::CONCAT_CONFLICT) |
183 |
|
{ |
184 |
|
Assert(children.size() == 1); |
185 |
|
if (!t0.isConst() || !s0.isConst()) |
186 |
|
{ |
187 |
|
// not constants |
188 |
|
return Node::null(); |
189 |
|
} |
190 |
|
size_t sindex; |
191 |
|
Node r0 = Word::splitConstant(t0, s0, sindex, isRev); |
192 |
|
if (!r0.isNull()) |
193 |
|
{ |
194 |
|
// Not a conflict due to constants, i.e. s0 is a prefix of t0 or vice |
195 |
|
// versa. |
196 |
|
return Node::null(); |
197 |
|
} |
198 |
|
return nm->mkConst(false); |
199 |
|
} |
200 |
174 |
else if (id == PfRule::CONCAT_SPLIT) |
201 |
|
{ |
202 |
3 |
Assert(children.size() == 2); |
203 |
9 |
if (children[1].getKind() != NOT || children[1][0].getKind() != EQUAL |
204 |
6 |
|| children[1][0][0].getKind() != STRING_LENGTH |
205 |
6 |
|| children[1][0][0][0] != t0 |
206 |
6 |
|| children[1][0][1].getKind() != STRING_LENGTH |
207 |
9 |
|| children[1][0][1][0] != s0) |
208 |
|
{ |
209 |
|
return Node::null(); |
210 |
|
} |
211 |
|
} |
212 |
171 |
else if (id == PfRule::CONCAT_CSPLIT) |
213 |
|
{ |
214 |
154 |
Assert(children.size() == 2); |
215 |
308 |
Node zero = nm->mkConst(Rational(0)); |
216 |
308 |
Node one = nm->mkConst(Rational(1)); |
217 |
462 |
if (children[1].getKind() != NOT || children[1][0].getKind() != EQUAL |
218 |
308 |
|| children[1][0][0].getKind() != STRING_LENGTH |
219 |
462 |
|| children[1][0][0][0] != t0 || children[1][0][1] != zero) |
220 |
|
{ |
221 |
|
return Node::null(); |
222 |
|
} |
223 |
154 |
if (!s0.isConst() || !s0.getType().isStringLike() || Word::isEmpty(s0)) |
224 |
|
{ |
225 |
|
return Node::null(); |
226 |
|
} |
227 |
|
} |
228 |
17 |
else if (id == PfRule::CONCAT_LPROP) |
229 |
|
{ |
230 |
17 |
Assert(children.size() == 2); |
231 |
34 |
if (children[1].getKind() != GT |
232 |
34 |
|| children[1][0].getKind() != STRING_LENGTH |
233 |
34 |
|| children[1][0][0] != t0 |
234 |
34 |
|| children[1][1].getKind() != STRING_LENGTH |
235 |
51 |
|| children[1][1][0] != s0) |
236 |
|
{ |
237 |
|
return Node::null(); |
238 |
|
} |
239 |
|
} |
240 |
|
else if (id == PfRule::CONCAT_CPROP) |
241 |
|
{ |
242 |
|
Assert(children.size() == 2); |
243 |
|
Node zero = nm->mkConst(Rational(0)); |
244 |
|
|
245 |
|
Trace("pfcheck-strings-cprop") |
246 |
|
<< "CONCAT_PROP, isRev=" << isRev << std::endl; |
247 |
|
if (children[1].getKind() != NOT || children[1][0].getKind() != EQUAL |
248 |
|
|| children[1][0][0].getKind() != STRING_LENGTH |
249 |
|
|| children[1][0][0][0] != t0 || children[1][0][1] != zero) |
250 |
|
{ |
251 |
|
Trace("pfcheck-strings-cprop") |
252 |
|
<< "...failed pattern match" << std::endl; |
253 |
|
return Node::null(); |
254 |
|
} |
255 |
|
if (tvec.size() <= 1) |
256 |
|
{ |
257 |
|
Trace("pfcheck-strings-cprop") |
258 |
|
<< "...failed adjacent constant" << std::endl; |
259 |
|
return Node::null(); |
260 |
|
} |
261 |
|
Node w1 = tvec[isRev ? nchildt - 2 : 1]; |
262 |
|
if (!w1.isConst() || !w1.getType().isStringLike() || Word::isEmpty(w1)) |
263 |
|
{ |
264 |
|
Trace("pfcheck-strings-cprop") |
265 |
|
<< "...failed adjacent constant content" << std::endl; |
266 |
|
return Node::null(); |
267 |
|
} |
268 |
|
Node w2 = s0; |
269 |
|
if (!w2.isConst() || !w2.getType().isStringLike() || Word::isEmpty(w2)) |
270 |
|
{ |
271 |
|
Trace("pfcheck-strings-cprop") << "...failed constant" << std::endl; |
272 |
|
return Node::null(); |
273 |
|
} |
274 |
|
// getConclusion expects the adjacent constant to be included |
275 |
|
t0 = nm->mkNode(STRING_CONCAT, isRev ? w1 : t0, isRev ? t0 : w1); |
276 |
|
} |
277 |
|
// use skolem cache |
278 |
348 |
SkolemCache skc(false); |
279 |
348 |
std::vector<Node> newSkolems; |
280 |
348 |
Node conc = CoreSolver::getConclusion(t0, s0, id, isRev, &skc, newSkolems); |
281 |
174 |
return conc; |
282 |
|
} |
283 |
1786 |
else if (id == PfRule::STRING_DECOMPOSE) |
284 |
|
{ |
285 |
2 |
Assert(children.size() == 1); |
286 |
2 |
Assert(args.size() == 1); |
287 |
|
bool isRev; |
288 |
2 |
if (!getBool(args[0], isRev)) |
289 |
|
{ |
290 |
|
return Node::null(); |
291 |
|
} |
292 |
4 |
Node atom = children[0]; |
293 |
2 |
if (atom.getKind() != GEQ || atom[0].getKind() != STRING_LENGTH) |
294 |
|
{ |
295 |
|
return Node::null(); |
296 |
|
} |
297 |
4 |
SkolemCache sc(false); |
298 |
4 |
std::vector<Node> newSkolems; |
299 |
|
Node conc = CoreSolver::getConclusion( |
300 |
4 |
atom[0][0], atom[1], id, isRev, &sc, newSkolems); |
301 |
2 |
return conc; |
302 |
|
} |
303 |
1784 |
else if (id == PfRule::STRING_REDUCTION |
304 |
1437 |
|| id == PfRule::STRING_EAGER_REDUCTION |
305 |
1153 |
|| id == PfRule::STRING_LENGTH_POS) |
306 |
|
{ |
307 |
1365 |
Assert(children.empty()); |
308 |
1365 |
Assert(args.size() >= 1); |
309 |
|
// These rules are based on calling a C++ method for returning a valid |
310 |
|
// lemma involving a single argument term. |
311 |
|
// Must convert to skolem form. |
312 |
2730 |
Node t = args[0]; |
313 |
2730 |
Node ret; |
314 |
1365 |
if (id == PfRule::STRING_REDUCTION) |
315 |
|
{ |
316 |
347 |
Assert(args.size() == 1); |
317 |
|
// we do not use optimizations |
318 |
694 |
SkolemCache skc(false); |
319 |
694 |
std::vector<Node> conj; |
320 |
347 |
ret = StringsPreprocess::reduce(t, conj, &skc); |
321 |
347 |
conj.push_back(t.eqNode(ret)); |
322 |
347 |
ret = nm->mkAnd(conj); |
323 |
|
} |
324 |
1018 |
else if (id == PfRule::STRING_EAGER_REDUCTION) |
325 |
|
{ |
326 |
284 |
Assert(args.size() == 1); |
327 |
568 |
SkolemCache skc(false); |
328 |
284 |
ret = TermRegistry::eagerReduce(t, &skc); |
329 |
|
} |
330 |
734 |
else if (id == PfRule::STRING_LENGTH_POS) |
331 |
|
{ |
332 |
734 |
Assert(args.size() == 1); |
333 |
734 |
ret = TermRegistry::lengthPositive(t); |
334 |
|
} |
335 |
1365 |
if (ret.isNull()) |
336 |
|
{ |
337 |
|
return Node::null(); |
338 |
|
} |
339 |
1365 |
return ret; |
340 |
|
} |
341 |
419 |
else if (id == PfRule::STRING_LENGTH_NON_EMPTY) |
342 |
|
{ |
343 |
82 |
Assert(children.size() == 1); |
344 |
82 |
Assert(args.empty()); |
345 |
164 |
Node nemp = children[0]; |
346 |
246 |
if (nemp.getKind() != NOT || nemp[0].getKind() != EQUAL |
347 |
242 |
|| !nemp[0][1].isConst() || !nemp[0][1].getType().isStringLike()) |
348 |
|
{ |
349 |
10 |
return Node::null(); |
350 |
|
} |
351 |
72 |
if (!Word::isEmpty(nemp[0][1])) |
352 |
|
{ |
353 |
|
return Node::null(); |
354 |
|
} |
355 |
144 |
Node zero = nm->mkConst(Rational(0)); |
356 |
144 |
Node clen = nm->mkNode(STRING_LENGTH, nemp[0][0]); |
357 |
72 |
return clen.eqNode(zero).notNode(); |
358 |
|
} |
359 |
337 |
else if (id == PfRule::RE_INTER) |
360 |
|
{ |
361 |
11 |
Assert(children.size() >= 1); |
362 |
11 |
Assert(args.empty()); |
363 |
22 |
std::vector<Node> reis; |
364 |
22 |
Node x; |
365 |
|
// make the regular expression intersection that summarizes all |
366 |
|
// memberships in the explanation |
367 |
31 |
for (const Node& c : children) |
368 |
|
{ |
369 |
22 |
bool polarity = c.getKind() != NOT; |
370 |
42 |
Node catom = polarity ? c : c[0]; |
371 |
22 |
if (catom.getKind() != STRING_IN_REGEXP) |
372 |
|
{ |
373 |
|
return Node::null(); |
374 |
|
} |
375 |
22 |
if (x.isNull()) |
376 |
|
{ |
377 |
11 |
x = catom[0]; |
378 |
|
} |
379 |
11 |
else if (x != catom[0]) |
380 |
|
{ |
381 |
|
// different LHS |
382 |
2 |
return Node::null(); |
383 |
|
} |
384 |
40 |
Node xcurr = catom[0]; |
385 |
|
Node rcurr = |
386 |
40 |
polarity ? catom[1] : nm->mkNode(REGEXP_COMPLEMENT, catom[1]); |
387 |
20 |
reis.push_back(rcurr); |
388 |
|
} |
389 |
18 |
Node rei = reis.size() == 1 ? reis[0] : nm->mkNode(REGEXP_INTER, reis); |
390 |
9 |
return nm->mkNode(STRING_IN_REGEXP, x, rei); |
391 |
|
} |
392 |
326 |
else if (id == PfRule::RE_UNFOLD_POS || id == PfRule::RE_UNFOLD_NEG |
393 |
240 |
|| id == PfRule::RE_UNFOLD_NEG_CONCAT_FIXED) |
394 |
|
{ |
395 |
94 |
Assert(children.size() == 1); |
396 |
94 |
Assert(args.empty()); |
397 |
188 |
Node skChild = children[0]; |
398 |
94 |
if (id == PfRule::RE_UNFOLD_NEG || id == PfRule::RE_UNFOLD_NEG_CONCAT_FIXED) |
399 |
|
{ |
400 |
28 |
if (skChild.getKind() != NOT || skChild[0].getKind() != STRING_IN_REGEXP) |
401 |
|
{ |
402 |
|
Trace("strings-pfcheck") << "...fail, non-neg member" << std::endl; |
403 |
|
return Node::null(); |
404 |
|
} |
405 |
|
} |
406 |
80 |
else if (skChild.getKind() != STRING_IN_REGEXP) |
407 |
|
{ |
408 |
|
Trace("strings-pfcheck") << "...fail, non-pos member" << std::endl; |
409 |
|
return Node::null(); |
410 |
|
} |
411 |
188 |
Node conc; |
412 |
94 |
if (id == PfRule::RE_UNFOLD_POS) |
413 |
|
{ |
414 |
160 |
std::vector<Node> newSkolems; |
415 |
160 |
SkolemCache sc; |
416 |
80 |
conc = RegExpOpr::reduceRegExpPos(skChild, &sc, newSkolems); |
417 |
|
} |
418 |
14 |
else if (id == PfRule::RE_UNFOLD_NEG) |
419 |
|
{ |
420 |
6 |
conc = RegExpOpr::reduceRegExpNeg(skChild); |
421 |
|
} |
422 |
8 |
else if (id == PfRule::RE_UNFOLD_NEG_CONCAT_FIXED) |
423 |
|
{ |
424 |
8 |
if (skChild[0][1].getKind() != REGEXP_CONCAT) |
425 |
|
{ |
426 |
|
Trace("strings-pfcheck") << "...fail, no concat regexp" << std::endl; |
427 |
|
return Node::null(); |
428 |
|
} |
429 |
|
size_t index; |
430 |
16 |
Node reLen = RegExpOpr::getRegExpConcatFixed(skChild[0][1], index); |
431 |
8 |
if (reLen.isNull()) |
432 |
|
{ |
433 |
|
Trace("strings-pfcheck") << "...fail, non-fixed lengths" << std::endl; |
434 |
|
return Node::null(); |
435 |
|
} |
436 |
8 |
conc = RegExpOpr::reduceRegExpNegConcatFixed(skChild, reLen, index); |
437 |
|
} |
438 |
94 |
return conc; |
439 |
|
} |
440 |
232 |
else if (id == PfRule::RE_ELIM) |
441 |
|
{ |
442 |
2 |
Assert(children.empty()); |
443 |
2 |
Assert(args.size() == 2); |
444 |
|
bool isAgg; |
445 |
2 |
if (!getBool(args[1], isAgg)) |
446 |
|
{ |
447 |
|
return Node::null(); |
448 |
|
} |
449 |
4 |
Node ea = RegExpElimination::eliminate(args[0], isAgg); |
450 |
|
// if we didn't eliminate, then this trivially proves the reflexive equality |
451 |
2 |
if (ea.isNull()) |
452 |
|
{ |
453 |
|
ea = args[0]; |
454 |
|
} |
455 |
2 |
return args[0].eqNode(ea); |
456 |
|
} |
457 |
230 |
else if (id == PfRule::STRING_CODE_INJ) |
458 |
|
{ |
459 |
167 |
Assert(children.empty()); |
460 |
167 |
Assert(args.size() == 2); |
461 |
167 |
Assert(args[0].getType().isStringLike() |
462 |
|
&& args[1].getType().isStringLike()); |
463 |
334 |
Node c1 = nm->mkNode(STRING_TO_CODE, args[0]); |
464 |
334 |
Node c2 = nm->mkNode(STRING_TO_CODE, args[1]); |
465 |
334 |
Node eqNegOne = c1.eqNode(nm->mkConst(Rational(-1))); |
466 |
334 |
Node deq = c1.eqNode(c2).negate(); |
467 |
334 |
Node eqn = args[0].eqNode(args[1]); |
468 |
167 |
return nm->mkNode(kind::OR, eqNegOne, deq, eqn); |
469 |
|
} |
470 |
63 |
else if (id == PfRule::STRING_SEQ_UNIT_INJ) |
471 |
|
{ |
472 |
16 |
Assert(children.size() == 1); |
473 |
16 |
Assert(args.empty()); |
474 |
16 |
if (children[0].getKind() != EQUAL) |
475 |
|
{ |
476 |
|
return Node::null(); |
477 |
|
} |
478 |
32 |
Node t[2]; |
479 |
48 |
for (size_t i = 0; i < 2; i++) |
480 |
|
{ |
481 |
32 |
if (children[0][i].getKind() == SEQ_UNIT) |
482 |
|
{ |
483 |
28 |
t[i] = children[0][i][0]; |
484 |
|
} |
485 |
4 |
else if (children[0][i].isConst()) |
486 |
|
{ |
487 |
|
// notice that Word::getChars is not the right call here, since it |
488 |
|
// gets a vector of sequences of length one. We actually need to |
489 |
|
// extract the character, which is a sequence-specific operation. |
490 |
4 |
const Sequence& sx = children[0][i].getConst<Sequence>(); |
491 |
4 |
const std::vector<Node>& vec = sx.getVec(); |
492 |
4 |
if (vec.size() == 1) |
493 |
|
{ |
494 |
|
// the character of the single character sequence |
495 |
4 |
t[i] = vec[0]; |
496 |
|
} |
497 |
|
} |
498 |
32 |
if (t[i].isNull()) |
499 |
|
{ |
500 |
|
return Node::null(); |
501 |
|
} |
502 |
|
} |
503 |
32 |
Trace("strings-pfcheck-debug") |
504 |
16 |
<< "STRING_SEQ_UNIT_INJ: " << children[0] << " => " << t[0] |
505 |
16 |
<< " == " << t[1] << std::endl; |
506 |
16 |
AlwaysAssert(t[0].getType() == t[1].getType()); |
507 |
16 |
return t[0].eqNode(t[1]); |
508 |
|
} |
509 |
47 |
else if (id == PfRule::STRING_TRUST) |
510 |
|
{ |
511 |
|
// "trusted" rules |
512 |
47 |
Assert(!args.empty()); |
513 |
47 |
Assert(args[0].getType().isBoolean()); |
514 |
47 |
return args[0]; |
515 |
|
} |
516 |
|
return Node::null(); |
517 |
|
} |
518 |
|
|
519 |
|
} // namespace strings |
520 |
|
} // namespace theory |
521 |
28194 |
} // namespace cvc5 |