Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Andres Noetzli, 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 the regular expression solver for the theory of strings.
14 : : */
15 : :
16 : : #include "theory/strings/regexp_solver.h"
17 : :
18 : : #include <cmath>
19 : :
20 : : #include "options/strings_options.h"
21 : : #include "smt/logic_exception.h"
22 : : #include "theory/ext_theory.h"
23 : : #include "theory/strings/term_registry.h"
24 : : #include "theory/strings/theory_strings_utils.h"
25 : : #include "util/statistics_value.h"
26 : :
27 : : using namespace cvc5::internal::kind;
28 : :
29 : : namespace cvc5::internal {
30 : : namespace theory {
31 : : namespace strings {
32 : :
33 : 51389 : RegExpSolver::RegExpSolver(Env& env,
34 : : SolverState& s,
35 : : InferenceManager& im,
36 : : TermRegistry& tr,
37 : : CoreSolver& cs,
38 : : ExtfSolver& es,
39 : 51389 : SequencesStatistics& stats)
40 : : : EnvObj(env),
41 : : d_state(s),
42 : : d_im(im),
43 : : d_csolver(cs),
44 : : d_esolver(es),
45 : : d_statistics(stats),
46 : 51389 : d_regexp_opr(env, tr.getSkolemCache())
47 : : {
48 : 51389 : d_emptyString = nodeManager()->mkConst(cvc5::internal::String(""));
49 : 51389 : d_emptyRegexp = nodeManager()->mkNode(Kind::REGEXP_NONE);
50 : 51389 : d_true = nodeManager()->mkConst(true);
51 : 51389 : d_false = nodeManager()->mkConst(false);
52 : 51389 : }
53 : :
54 : 32196 : std::map<Node, std::vector<Node>> RegExpSolver::computeAssertions(Kind k) const
55 : : {
56 : 32196 : std::map<Node, std::vector<Node>> assertions;
57 : : // add the memberships
58 : 64392 : std::vector<Node> xts = d_esolver.getActive(k);
59 : : // maps representatives to regular expression memberships in that class
60 [ + + ]: 35895 : for (const Node& n : xts)
61 : : {
62 [ - + ][ - + ]: 3699 : Assert(n.getKind() == k);
[ - - ]
63 : 11097 : Node r = d_state.getRepresentative(n);
64 [ + + ]: 3699 : if (r.isConst())
65 : : {
66 : 3515 : bool pol = r.getConst<bool>();
67 [ + - ]: 7030 : Trace("strings-process-debug")
68 : 3515 : << " add predicate : " << n << ", pol = " << pol << std::endl;
69 : 3515 : r = d_state.getRepresentative(n[0]);
70 [ + + ]: 3515 : assertions[r].push_back(pol ? n : n.negate());
71 : : }
72 : : else
73 : : {
74 [ + - ]: 368 : Trace("strings-process-debug")
75 : 184 : << " irrelevant (non-asserted) predicate : " << n << std::endl;
76 : : }
77 : : }
78 : 64392 : return assertions;
79 : : }
80 : :
81 : 32196 : void RegExpSolver::computeAssertedMemberships()
82 : : {
83 : 32196 : d_assertedMems = computeAssertions(Kind::STRING_IN_REGEXP);
84 : 32196 : }
85 : :
86 : 32196 : void RegExpSolver::checkMemberships(Theory::Effort e)
87 : : {
88 [ + - ]: 64392 : Trace("regexp-process") << "Checking Memberships, effort = " << e << " ... "
89 : 32196 : << std::endl;
90 : : // compute the memberships
91 : 32196 : computeAssertedMemberships();
92 [ + + ]: 32196 : if (e == Theory::EFFORT_FULL)
93 : : {
94 : : // check for regular expression inclusion
95 : 31104 : checkInclusions();
96 [ + + ]: 31104 : if (d_state.isInConflict())
97 : : {
98 : 60 : return;
99 : : }
100 : : // check for evaluations and inferences based on derivatives
101 : 31044 : checkEvaluations();
102 [ - + ]: 31044 : if (d_state.isInConflict())
103 : : {
104 : 0 : return;
105 : : }
106 : : }
107 : 32136 : checkUnfold(e);
108 : : }
109 : :
110 : 31104 : void RegExpSolver::checkInclusions()
111 : : {
112 : : // Check for conflict and chances to mark memberships inactive based on
113 : : // regular expression and intersection.
114 [ + - ]: 62208 : Trace("regexp-process") << "Checking inclusion/intersection ... "
115 : 31104 : << std::endl;
116 [ + + ]: 33145 : for (const std::pair<const Node, std::vector<Node>>& mr : d_assertedMems)
117 : : {
118 : : // copy the vector because it is modified in the call below
119 : 2101 : std::vector<Node> mems2 = mr.second;
120 [ + - ]: 4202 : Trace("regexp-process")
121 : 2101 : << "Memberships(" << mr.first << ") = " << mr.second << std::endl;
122 [ + - ][ + + ]: 2101 : if (options().strings.stringRegexpInclusion && !checkEqcInclusion(mems2))
[ + + ]
123 : : {
124 : : // conflict discovered, return
125 : 60 : return;
126 : : }
127 [ - + ]: 2041 : if (!checkEqcIntersect(mems2))
128 : : {
129 : : // conflict discovered, return
130 : 0 : return;
131 : : }
132 : : }
133 [ + - ]: 62088 : Trace("regexp-debug") << "... No Intersect Conflict in Memberships"
134 : 31044 : << std::endl;
135 : : }
136 : :
137 : 56972 : void RegExpSolver::checkMembershipsEager()
138 : : {
139 [ + + ]: 56972 : if (!options().strings.stringRegexpPosConcatEager)
140 : : {
141 : : // option not enabled
142 : 56964 : return;
143 : : }
144 : : // eagerly reduce positive membership into re.++
145 : 16 : std::vector<Node> mems = d_esolver.getActive(Kind::STRING_IN_REGEXP);
146 [ + + ]: 16 : for (const Node& n : mems)
147 : : {
148 [ - + ][ - + ]: 8 : Assert(n.getKind() == Kind::STRING_IN_REGEXP);
[ - - ]
149 [ - + ]: 8 : if (n[1].getKind() != Kind::REGEXP_CONCAT)
150 : : {
151 : : // not a membership into concatenation
152 : 0 : continue;
153 : : }
154 [ - + ]: 8 : if (d_esolver.isReduced(n))
155 : : {
156 : : // already reduced
157 : 0 : continue;
158 : : }
159 : 16 : Node r = d_state.getRepresentative(n);
160 [ + - ][ - + ]: 8 : if (!r.isConst() || !r.getConst<bool>())
[ - + ]
161 : : {
162 : : // not asserted true
163 : 0 : continue;
164 : : }
165 : : // unfold it
166 : 8 : doUnfold(n);
167 : : }
168 : : }
169 : :
170 : 64272 : bool RegExpSolver::shouldUnfold(Theory::Effort e, bool pol) const
171 : : {
172 : : // Check positive, then negative memberships. If we are doing
173 : : // model-based reductions, we process positive ones at FULL effort, and
174 : : // negative ones at LAST_CALL effort.
175 [ + - ]: 64272 : if (options().strings.stringModelBasedReduction)
176 : : {
177 [ + + ]: 64272 : if (pol)
178 : : {
179 : 32136 : return e == Theory::EFFORT_FULL;
180 : : }
181 : 32136 : return e == Theory::EFFORT_LAST_CALL;
182 : : }
183 : : // Otherwise we don't make the distinction
184 : 0 : return true;
185 : : }
186 : :
187 : 32136 : void RegExpSolver::checkUnfold(Theory::Effort e)
188 : : {
189 [ + - ]: 32136 : Trace("regexp-process") << "Checking unfold ... " << std::endl;
190 : : // get all memberships
191 : 64272 : std::map<Node, Node> allMems;
192 [ + + ]: 34607 : for (const std::pair<const Node, std::vector<Node>>& mr : d_assertedMems)
193 : : {
194 [ + + ]: 5834 : for (const Node& m : mr.second)
195 : : {
196 : 3363 : allMems[m] = mr.first;
197 : : }
198 : : }
199 : : // representatives of strings that are the LHS of positive memberships that
200 : : // we unfolded
201 : 64272 : std::unordered_set<Node> repUnfold;
202 [ + + ]: 96408 : for (size_t eval = 0; eval < 2; eval++)
203 : : {
204 : : // skip if we should not unfold
205 : 64272 : bool checkPol = (eval == 0);
206 [ + + ]: 64272 : if (!shouldUnfold(e, checkPol))
207 : : {
208 : 32136 : continue;
209 : : }
210 [ + + ]: 35499 : for (const std::pair<const Node, Node>& mp : allMems)
211 : : {
212 : 3363 : Node assertion = mp.first;
213 : 3363 : Node rep = mp.second;
214 : 3363 : bool polarity = assertion.getKind() != Kind::NOT;
215 [ + + ]: 3363 : if (polarity != checkPol)
216 : : {
217 : 1108 : continue;
218 : : }
219 : : // check regular expression membership
220 [ + - ]: 4510 : Trace("regexp-debug") << "Check : " << assertion << " "
221 : 2255 : << (d_esolver.isReduced(assertion)) << std::endl;
222 [ + + ]: 2255 : if (d_esolver.isReduced(assertion))
223 : : {
224 : 1236 : continue;
225 : : }
226 [ + + ]: 1019 : Node atom = polarity ? assertion : assertion[0];
227 [ + - ]: 2038 : Trace("strings-regexp")
228 : 0 : << "We have regular expression assertion : " << assertion
229 : 1019 : << std::endl;
230 [ - + ][ - + ]: 1019 : Assert(atom == rewrite(atom));
[ - - ]
231 [ + + ][ + + ]: 1019 : if (e == Theory::EFFORT_LAST_CALL && !d_esolver.isActiveInModel(atom))
[ + + ][ + + ]
[ - - ]
232 : : {
233 [ + - ]: 130 : Trace("strings-regexp")
234 : 65 : << "...ignore since inactive in model" << std::endl;
235 : 65 : continue;
236 : : }
237 [ + + ][ - + ]: 954 : if (!checkPol && repUnfold.find(rep) != repUnfold.end())
[ - + ]
238 : : {
239 : : // do not unfold negative memberships of strings that have new
240 : : // positive unfoldings. For example:
241 : : // x in ("A")* ^ NOT x in ("B")*
242 : : // We unfold x = "A" ++ x' only. The intution here is that positive
243 : : // unfoldings lead to stronger constraints (equalities are stronger
244 : : // than disequalities), and are easier to check.
245 : 0 : continue;
246 : : }
247 [ + + ]: 954 : if (!polarity)
248 : : {
249 [ - + ]: 78 : if (!options().strings.stringExp)
250 : : {
251 : : throw LogicException(
252 : : "Strings Incomplete (due to Negative Membership) by default, "
253 : 0 : "try --strings-exp option.");
254 : : }
255 : : }
256 : : // check if the term is atomic
257 [ + - ]: 1908 : Trace("strings-regexp")
258 : 954 : << "Unroll/simplify membership of atomic term " << rep << std::endl;
259 : : // if so, do simple unrolling
260 [ + + ]: 954 : if (doUnfold(assertion))
261 : : {
262 [ + + ]: 952 : if (checkPol)
263 : : {
264 : : // Remember that we have unfolded a membership for x
265 : : // notice that we only do this here, after we have definitely
266 : : // added a lemma.
267 : 874 : repUnfold.insert(rep);
268 : : }
269 : : }
270 : : }
271 [ - + ]: 32136 : if (d_state.isInConflict())
272 : : {
273 : 0 : break;
274 : : }
275 : : }
276 : 32136 : }
277 : :
278 : 962 : bool RegExpSolver::doUnfold(const Node& assertion)
279 : : {
280 : 962 : bool ret = false;
281 : 962 : bool polarity = assertion.getKind() != Kind::NOT;
282 [ + + ]: 1924 : Node atom = polarity ? assertion : assertion[0];
283 [ - + ][ - + ]: 962 : Assert(atom.getKind() == Kind::STRING_IN_REGEXP);
[ - - ]
284 [ + - ]: 962 : Trace("strings-regexp") << "Simplify on " << atom << std::endl;
285 : 962 : Node conc = d_regexp_opr.simplify(atom, polarity);
286 [ + - ]: 962 : Trace("strings-regexp") << "...finished, got " << conc << std::endl;
287 : : // if simplifying successfully generated a lemma
288 [ + - ]: 962 : if (!conc.isNull())
289 : : {
290 : 1924 : std::vector<Node> iexp;
291 : 1924 : std::vector<Node> noExplain;
292 : 962 : iexp.push_back(assertion);
293 : 962 : noExplain.push_back(assertion);
294 [ - + ][ - + ]: 962 : Assert(atom.getKind() == Kind::STRING_IN_REGEXP);
[ - - ]
295 [ + + ]: 962 : if (polarity)
296 : : {
297 : 884 : d_statistics.d_regexpUnfoldingsPos << atom[1].getKind();
298 : : }
299 : : else
300 : : {
301 : 78 : d_statistics.d_regexpUnfoldingsNeg << atom[1].getKind();
302 : : }
303 [ + + ]: 962 : InferenceId inf = polarity ? InferenceId::STRINGS_RE_UNFOLD_POS
304 : : : InferenceId::STRINGS_RE_UNFOLD_NEG;
305 : : // in very rare cases, we may find out that the unfolding lemma
306 : : // for a membership is equivalent to true, in spite of the RE
307 : : // not being rewritten to true.
308 : 962 : ret = d_im.sendInference(iexp, noExplain, conc, inf);
309 : 962 : d_esolver.markReduced(assertion);
310 : : }
311 : : else
312 : : {
313 : : // otherwise we are incomplete
314 : 0 : d_im.setModelUnsound(IncompleteId::STRINGS_REGEXP_NO_SIMPLIFY);
315 : : }
316 : 1924 : return ret;
317 : : }
318 : :
319 : 2101 : bool RegExpSolver::checkEqcInclusion(std::vector<Node>& mems)
320 : : {
321 : 4202 : std::unordered_set<Node> remove;
322 : :
323 [ + + ]: 4933 : for (const Node& m1 : mems)
324 : : {
325 : 2892 : bool m1Neg = m1.getKind() == Kind::NOT;
326 [ + + ]: 2892 : Node m1Lit = m1Neg ? m1[0] : m1;
327 : :
328 [ + + ]: 2892 : if (remove.find(m1) != remove.end())
329 : : {
330 : : // Skip memberships marked for removal
331 : 12 : continue;
332 : : }
333 : :
334 [ + + ]: 8047 : for (const Node& m2 : mems)
335 : : {
336 [ + + ]: 5301 : if (m1 == m2)
337 : : {
338 : 2859 : continue;
339 : : }
340 : :
341 : 2442 : bool m2Neg = m2.getKind() == Kind::NOT;
342 [ + + ]: 2442 : Node m2Lit = m2Neg ? m2[0] : m2;
343 : :
344 [ + + ]: 2442 : if (m1Neg == m2Neg)
345 : : {
346 : : // Check whether the RE in membership m1 contains the one in m2, if
347 : : // so then m1 can be marked reduced if positive polarity, m2 if
348 : : // negative polarity.
349 : : // Notice that we do not do this if the non-reduced membership has
350 : : // already been unfolded, since memberships may reduce to other
351 : : // memberships that are included in the original, thus making the
352 : : // justification for the reduction cyclic. For example, to reduce:
353 : : // (not (str.in_re x (re.++ (re.* R1) R2)))
354 : : // We may rely on justifying this by the fact that (writing x[i:j] for
355 : : // substring) either:
356 : : // (not (str.in_re x[:0] (re.* R1)))
357 : : // (not (str.in_re x[0:] R2))
358 : : // The first is trivially satisfied, the second is equivalent to
359 : : // (not (str.in_re x R2))
360 : : // where R2 is included in (re.++ (re.* R1) R2)). However, we cannot
361 : : // mark the latter as reduced.
362 [ + + ]: 1692 : bool basisUnfolded = d_esolver.isReduced(m1Neg ? m1 : m2);
363 [ + + ]: 1692 : if (!basisUnfolded)
364 : : {
365 : : // Both regular expression memberships have positive polarity
366 [ + + ]: 1074 : if (d_regexp_opr.regExpIncludes(m1Lit[1], m2Lit[1]))
367 : : {
368 [ + + ]: 90 : if (m1Neg)
369 : : {
370 : : // ~str.in.re(x, R1) includes ~str.in.re(x, R2) --->
371 : : // mark ~str.in.re(x, R2) as inactive
372 : 16 : d_im.markInactive(m2Lit,
373 : : ExtReducedId::STRINGS_REGEXP_INCLUDE_NEG);
374 : 16 : remove.insert(m2);
375 : : }
376 : : else
377 : : {
378 : : // str.in.re(x, R1) includes str.in.re(x, R2) --->
379 : : // mark str.in.re(x, R1) as inactive
380 : 74 : d_im.markInactive(m1Lit, ExtReducedId::STRINGS_REGEXP_INCLUDE);
381 : 74 : remove.insert(m1);
382 : :
383 : : // We don't need to process m1 anymore
384 : 74 : break;
385 : : }
386 : : }
387 : : }
388 : : }
389 : : else
390 : : {
391 [ + + ]: 750 : Node pos = m1Neg ? m2Lit : m1Lit;
392 [ + + ]: 750 : Node neg = m1Neg ? m1Lit : m2Lit;
393 [ + + ]: 750 : if (d_regexp_opr.regExpIncludes(neg[1], pos[1]))
394 : : {
395 : : // We have a conflict because we have a case where str.in.re(x, R1)
396 : : // and ~str.in.re(x, R2) but R2 includes R1, so there is no
397 : : // possible value for x that satisfies both memberships.
398 : 120 : std::vector<Node> vec_nodes;
399 : 60 : vec_nodes.push_back(pos);
400 : 60 : vec_nodes.push_back(neg.negate());
401 : :
402 [ - + ]: 60 : if (pos[0] != neg[0])
403 : : {
404 : 0 : vec_nodes.push_back(pos[0].eqNode(neg[0]));
405 : : }
406 : :
407 : 60 : Node conc;
408 : 60 : d_im.sendInference(
409 : : vec_nodes, conc, InferenceId::STRINGS_RE_INTER_INCLUDE, false, true);
410 : 60 : return false;
411 : : }
412 : : }
413 : : }
414 : : }
415 : :
416 : 0 : mems.erase(std::remove_if(
417 : : mems.begin(),
418 : : mems.end(),
419 : 4855 : [&remove](Node& n) { return remove.find(n) != remove.end(); }),
420 : 4082 : mems.end());
421 : :
422 : 2041 : return true;
423 : : }
424 : :
425 : 2041 : bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems)
426 : : {
427 : : // do not compute intersections if the re intersection mode is none
428 [ + + ]: 2041 : if (options().strings.stringRegExpInterMode == options::RegExpInterMode::NONE)
429 : : {
430 : 2039 : return true;
431 : : }
432 [ - + ]: 2 : if (mems.empty())
433 : : {
434 : : // nothing to do
435 : 0 : return true;
436 : : }
437 : : // the initial regular expression membership and its constant type
438 : 4 : Node mi;
439 : 2 : RegExpConstType rcti = RE_C_UNKNOWN;
440 : 2 : NodeManager* nm = nodeManager();
441 [ + + ]: 4 : for (const Node& m : mems)
442 : : {
443 [ - + ]: 2 : if (m.getKind() != Kind::STRING_IN_REGEXP)
444 : : {
445 : : // do not do negative
446 : 0 : Assert(m.getKind() == Kind::NOT
447 : : && m[0].getKind() == Kind::STRING_IN_REGEXP);
448 : 2 : continue;
449 : : }
450 : 2 : RegExpConstType rct = d_regexp_opr.getRegExpConstType(m[1]);
451 : 2 : if (rct == RE_C_VARIABLE
452 [ + - ][ - + ]: 2 : || (options().strings.stringRegExpInterMode
[ - + ]
453 : : == options::RegExpInterMode::CONSTANT
454 [ - - ]: 0 : && rct != RE_C_CONCRETE_CONSTANT))
455 : : {
456 : : // cannot do intersection on RE with variables, or with re.allchar based
457 : : // on option.
458 : 0 : continue;
459 : : }
460 : 2 : if (options().strings.stringRegExpInterMode
461 [ - + ]: 2 : == options::RegExpInterMode::ONE_CONSTANT)
462 : : {
463 : 0 : if (!mi.isNull() && rcti >= RE_C_CONSTANT && rct >= RE_C_CONSTANT)
464 : : {
465 : : // if both have re.allchar, do not do intersection if the
466 : : // options::RegExpInterMode::ONE_CONSTANT option is set.
467 : 0 : continue;
468 : : }
469 : : }
470 [ + - ]: 2 : if (mi.isNull())
471 : : {
472 : : // first regular expression seen
473 : 2 : mi = m;
474 : 2 : rcti = rct;
475 : 2 : continue;
476 : : }
477 : 0 : Node resR = d_regexp_opr.intersect(mi[1], m[1]);
478 [ - - ]: 0 : if (resR.isNull())
479 : : {
480 : : // failed to compute intersection, e.g. if there was a complement
481 : 0 : continue;
482 : : }
483 [ - - ]: 0 : if (resR == d_emptyRegexp)
484 : : {
485 : : // conflict, explain
486 : 0 : std::vector<Node> vec_nodes;
487 : 0 : vec_nodes.push_back(mi);
488 : 0 : vec_nodes.push_back(m);
489 [ - - ]: 0 : if (mi[0] != m[0])
490 : : {
491 : 0 : vec_nodes.push_back(mi[0].eqNode(m[0]));
492 : : }
493 : 0 : Node conc;
494 : 0 : d_im.sendInference(
495 : : vec_nodes, conc, InferenceId::STRINGS_RE_INTER_CONF, false, true);
496 : : // conflict, return
497 : 0 : return false;
498 : : }
499 : : // rewrite to ensure the equality checks below are precise
500 : 0 : Node mres = nm->mkNode(Kind::STRING_IN_REGEXP, mi[0], resR);
501 : 0 : Node mresr = rewrite(mres);
502 [ - - ]: 0 : if (mresr == mi)
503 : : {
504 : : // if R1 = intersect( R1, R2 ), then x in R1 ^ x in R2 is equivalent
505 : : // to x in R1, hence x in R2 can be marked redundant.
506 : 0 : d_im.markInactive(m, ExtReducedId::STRINGS_REGEXP_INTER_SUBSUME);
507 : : }
508 [ - - ]: 0 : else if (mresr == m)
509 : : {
510 : : // same as above, opposite direction
511 : 0 : d_im.markInactive(mi, ExtReducedId::STRINGS_REGEXP_INTER_SUBSUME);
512 : : }
513 : : else
514 : : {
515 : : // new conclusion
516 : : // (x in R1 ^ y in R2 ^ x = y) => (x in intersect(R1,R2))
517 : 0 : std::vector<Node> vec_nodes;
518 : 0 : vec_nodes.push_back(mi);
519 : 0 : vec_nodes.push_back(m);
520 [ - - ]: 0 : if (mi[0] != m[0])
521 : : {
522 : 0 : vec_nodes.push_back(mi[0].eqNode(m[0]));
523 : : }
524 : 0 : d_im.sendInference(
525 : : vec_nodes, mres, InferenceId::STRINGS_RE_INTER_INFER, false, true);
526 : : // both are inactive
527 : 0 : d_im.markInactive(m, ExtReducedId::STRINGS_REGEXP_INTER);
528 : 0 : d_im.markInactive(mi, ExtReducedId::STRINGS_REGEXP_INTER);
529 : : // do not send more than one lemma for this class
530 : 0 : return true;
531 : : }
532 : : }
533 : 2 : return true;
534 : : }
535 : :
536 : 1888 : bool RegExpSolver::checkPDerivative(Node x,
537 : : Node r,
538 : : Node atom,
539 : : std::vector<Node>& nf_exp)
540 : : {
541 [ - + ]: 1888 : if (d_state.areEqual(x, d_emptyString))
542 : : {
543 : 0 : Node exp;
544 : 0 : switch (d_regexp_opr.delta(r, exp))
545 : : {
546 : 0 : case 0:
547 : : {
548 : 0 : std::vector<Node> noExplain;
549 : 0 : noExplain.push_back(atom);
550 : 0 : noExplain.push_back(x.eqNode(d_emptyString));
551 : 0 : std::vector<Node> iexp = nf_exp;
552 : 0 : iexp.insert(iexp.end(), noExplain.begin(), noExplain.end());
553 : 0 : d_im.sendInference(iexp, noExplain, exp, InferenceId::STRINGS_RE_DELTA);
554 : 0 : d_im.markInactive(atom, ExtReducedId::STRINGS_REGEXP_PDERIVATIVE);
555 : 0 : return false;
556 : : }
557 : 0 : case 1:
558 : : {
559 : 0 : d_im.markInactive(atom, ExtReducedId::STRINGS_REGEXP_PDERIVATIVE);
560 : 0 : break;
561 : : }
562 : 0 : case 2:
563 : : {
564 : 0 : std::vector<Node> noExplain;
565 : 0 : noExplain.push_back(atom);
566 [ - - ]: 0 : if (x != d_emptyString)
567 : : {
568 : 0 : noExplain.push_back(x.eqNode(d_emptyString));
569 : : }
570 : 0 : std::vector<Node> iexp = nf_exp;
571 : 0 : iexp.insert(iexp.end(), noExplain.begin(), noExplain.end());
572 : 0 : d_im.sendInference(iexp, noExplain, d_false, InferenceId::STRINGS_RE_DELTA_CONF);
573 : 0 : return false;
574 : : }
575 : 0 : default:
576 : : // Impossible
577 : 0 : break;
578 : : }
579 : : }
580 : : else
581 : : {
582 [ + + ]: 1888 : if (deriveRegExp(x, r, atom, nf_exp))
583 : : {
584 : 8 : d_im.markInactive(atom, ExtReducedId::STRINGS_REGEXP_PDERIVATIVE);
585 : 8 : return false;
586 : : }
587 : : }
588 : 1880 : return true;
589 : : }
590 : :
591 : 1888 : cvc5::internal::String RegExpSolver::getHeadConst(Node x)
592 : : {
593 [ - + ]: 1888 : if (x.isConst())
594 : : {
595 : 0 : return x.getConst<String>();
596 : : }
597 [ + + ]: 1888 : else if (x.getKind() == Kind::STRING_CONCAT)
598 : : {
599 [ + + ]: 180 : if (x[0].isConst())
600 : : {
601 : 16 : return x[0].getConst<String>();
602 : : }
603 : : }
604 : 1872 : return d_emptyString.getConst<String>();
605 : : }
606 : :
607 : 1888 : bool RegExpSolver::deriveRegExp(Node x,
608 : : Node r,
609 : : Node atom,
610 : : std::vector<Node>& ant)
611 : : {
612 [ - + ][ - + ]: 1888 : Assert(x != d_emptyString);
[ - - ]
613 [ + - ]: 3776 : Trace("regexp-derive") << "RegExpSolver::deriveRegExp: x=" << x
614 : 1888 : << ", r= " << r << std::endl;
615 : 3776 : cvc5::internal::String s = getHeadConst(x);
616 : : // only allow RE_DERIVE for concrete constant regular expressions
617 [ + - ]: 8 : if (options().strings.stringRegexpDeriveConflicts && !s.empty()
618 [ + + ][ + - ]: 1896 : && d_regexp_opr.getRegExpConstType(r) == RE_C_CONCRETE_CONSTANT)
[ + + ][ + + ]
[ - - ]
619 : : {
620 : 16 : Node conc = Node::null();
621 : 16 : Node dc = r;
622 : 8 : bool flag = true;
623 [ + - ]: 8 : for (unsigned i = 0; i < s.size(); ++i)
624 : : {
625 : 8 : cvc5::internal::String c = s.substr(i, 1);
626 : 8 : Node dc2;
627 : 8 : int rt = d_regexp_opr.derivativeS(dc, c, dc2);
628 : 8 : dc = dc2;
629 [ + - ]: 8 : if (rt == 2)
630 : : {
631 : : // CONFLICT
632 : 8 : flag = false;
633 : 8 : break;
634 : : }
635 : : }
636 : : // send lemma
637 [ - + ]: 8 : if (flag)
638 : : {
639 [ - - ]: 0 : if (x.isConst())
640 : : {
641 : 0 : Assert(false)
642 : : << "Impossible: RegExpSolver::deriveRegExp: const string in const "
643 : 0 : "regular expression.";
644 : : return false;
645 : : }
646 : : else
647 : : {
648 : 0 : Assert(x.getKind() == Kind::STRING_CONCAT);
649 : 0 : std::vector<Node> vec_nodes;
650 [ - - ]: 0 : for (unsigned int i = 1; i < x.getNumChildren(); ++i)
651 : : {
652 : 0 : vec_nodes.push_back(x[i]);
653 : : }
654 : 0 : Node left = utils::mkConcat(vec_nodes, x.getType());
655 : 0 : left = rewrite(left);
656 : 0 : conc = nodeManager()->mkNode(Kind::STRING_IN_REGEXP, left, dc);
657 : : }
658 : : }
659 : 16 : std::vector<Node> iexp = ant;
660 : 8 : std::vector<Node> noExplain;
661 : 8 : noExplain.push_back(atom);
662 : 8 : iexp.push_back(atom);
663 : 8 : d_im.sendInference(iexp, noExplain, conc, InferenceId::STRINGS_RE_DERIVE);
664 : 8 : return true;
665 : : }
666 : 1880 : return false;
667 : : }
668 : :
669 : 2130 : Node RegExpSolver::getNormalSymRegExp(Node r, std::vector<Node>& nf_exp)
670 : : {
671 : 2130 : Node ret = r;
672 [ + + ][ + - ]: 2130 : switch (r.getKind())
673 : : {
674 : 94 : case Kind::REGEXP_NONE:
675 : : case Kind::REGEXP_ALLCHAR:
676 : 94 : case Kind::REGEXP_RANGE: break;
677 : 856 : case Kind::STRING_TO_REGEXP:
678 : : {
679 [ + + ]: 856 : if (!r[0].isConst())
680 : : {
681 : 1048 : Node tmp = d_csolver.getNormalString(r[0], nf_exp);
682 [ + + ]: 524 : if (tmp != r[0])
683 : : {
684 : 348 : ret = nodeManager()->mkNode(Kind::STRING_TO_REGEXP, tmp);
685 : : }
686 : : }
687 : 856 : break;
688 : : }
689 : 1180 : case Kind::REGEXP_CONCAT:
690 : : case Kind::REGEXP_UNION:
691 : : case Kind::REGEXP_INTER:
692 : : case Kind::REGEXP_STAR:
693 : : case Kind::REGEXP_COMPLEMENT:
694 : : {
695 : 2360 : std::vector<Node> vec_nodes;
696 [ + + ]: 2964 : for (const Node& cr : r)
697 : : {
698 : 1784 : vec_nodes.push_back(getNormalSymRegExp(cr, nf_exp));
699 : : }
700 : 1180 : ret = rewrite(nodeManager()->mkNode(r.getKind(), vec_nodes));
701 : 1180 : break;
702 : : }
703 : 0 : default:
704 : : {
705 [ - - ]: 0 : Trace("strings-error") << "Unsupported term: " << r
706 : 0 : << " in normalization SymRegExp." << std::endl;
707 : 0 : Assert(!utils::isRegExpKind(r.getKind()));
708 : : }
709 : : }
710 : 2130 : return ret;
711 : : }
712 : :
713 : 31044 : void RegExpSolver::checkEvaluations()
714 : : {
715 : 31044 : NodeManager* nm = nodeManager();
716 [ + + ]: 33071 : for (const std::pair<const Node, std::vector<Node>>& mr : d_assertedMems)
717 : : {
718 : 4054 : Node rep = mr.first;
719 [ + + ]: 4769 : for (const Node& assertion : mr.second)
720 : : {
721 : 2782 : bool polarity = assertion.getKind() != Kind::NOT;
722 [ + + ]: 2782 : Node atom = polarity ? assertion : assertion[0];
723 [ + - ]: 5564 : Trace("strings-regexp")
724 : 0 : << "We have regular expression assertion : " << assertion
725 : 2782 : << std::endl;
726 [ - + ][ - + ]: 2782 : Assert(atom == rewrite(atom));
[ - - ]
727 : 2782 : Node x = atom[0];
728 : 2782 : Node r = atom[1];
729 [ - + ][ - + ]: 2782 : Assert(rep == d_state.getRepresentative(x));
[ - - ]
730 : : // The following code takes normal forms into account for the purposes
731 : : // of simplifying a regular expression membership x in R. For example,
732 : : // if x = "A" in the current context, then we may be interested in
733 : : // reasoning about ( x in R ) * { x -> "A" }. Say we update the
734 : : // membership to nx in R', then:
735 : : // - nfexp => ( x in R ) <=> nx in R'
736 : : // - rnfexp => R = R'
737 : : // We use these explanations below as assumptions on inferences when
738 : : // appropriate. Notice that for inferring conflicts and tautologies,
739 : : // we use the normal form of x always. This is because we always want to
740 : : // discover conflicts/tautologies whenever possible.
741 : : // For inferences based on regular expression unfolding, we do not use
742 : : // the normal form of x. The reason is that it is better to unfold
743 : : // regular expression memberships in a context-indepedent manner,
744 : : // that is, not taking into account the current normal form of x, since
745 : : // this ensures these lemmas are still relevant after backtracking.
746 : 2782 : std::vector<Node> nfexp;
747 : 2782 : std::vector<Node> rnfexp;
748 : : // The normal form of x is stored in nx, while x is left unchanged.
749 : 2782 : Node nx = x;
750 [ + + ]: 2782 : if (!x.isConst())
751 : : {
752 : 2756 : nx = d_csolver.getNormalString(x, nfexp);
753 : : }
754 : : // If r is not a constant regular expression, we update it based on
755 : : // normal forms, which may concretize its variables.
756 [ + + ]: 2782 : if (!d_regexp_opr.checkConstRegExp(r))
757 : : {
758 : 346 : r = getNormalSymRegExp(r, rnfexp);
759 : 346 : nfexp.insert(nfexp.end(), rnfexp.begin(), rnfexp.end());
760 [ + - ]: 692 : Trace("strings-regexp-nf") << "Term " << atom << " is normalized to "
761 : 346 : << nx << " IN " << r << std::endl;
762 : :
763 : : // We rewrite the membership nx IN r.
764 : 692 : Node tmp = rewrite(nm->mkNode(Kind::STRING_IN_REGEXP, nx, r));
765 [ + - ]: 346 : Trace("strings-regexp-nf") << "Simplifies to " << tmp << std::endl;
766 [ + + ]: 346 : if (tmp.isConst())
767 : : {
768 [ + + ]: 80 : if (tmp.getConst<bool>() == polarity)
769 : : {
770 : : // it is satisfied in this SAT context
771 : 40 : d_im.markInactive(atom, ExtReducedId::STRINGS_REGEXP_RE_SYM_NF);
772 : 40 : continue;
773 : : }
774 : : else
775 : : {
776 : : // we have a conflict
777 : 80 : std::vector<Node> iexp = nfexp;
778 : 80 : std::vector<Node> noExplain;
779 : 40 : iexp.push_back(assertion);
780 : 40 : noExplain.push_back(assertion);
781 : 80 : Node conc = Node::null();
782 : 40 : d_im.sendInference(
783 : : iexp, noExplain, conc, InferenceId::STRINGS_RE_NF_CONFLICT);
784 : 40 : break;
785 : : }
786 : : }
787 : : }
788 [ + + ]: 2702 : if (polarity)
789 : : {
790 : 1888 : checkPDerivative(x, r, atom, rnfexp);
791 : : }
792 : : }
793 : : }
794 : 31044 : }
795 : :
796 : : } // namespace strings
797 : : } // namespace theory
798 : : } // namespace cvc5::internal
|
