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