Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Mathias Preiner
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 : : * Evaluator for regular expression membership.
14 : : */
15 : :
16 : : #include "theory/strings/regexp_eval.h"
17 : :
18 : : #include "theory/strings/theory_strings_utils.h"
19 : : #include "util/string.h"
20 : :
21 : : using namespace cvc5::internal::kind;
22 : :
23 : : namespace cvc5::internal {
24 : : namespace theory {
25 : : namespace strings {
26 : :
27 : : /**
28 : : * An NFA state.
29 : : *
30 : : * Edges can be annotated with constant characters, re.allchar or re.range
31 : : * regular expressions.
32 : : *
33 : : * Regular expressions can be compiled to an NFA via construct. Evaluation
34 : : * is computed via addToNext and processNextChar.
35 : : */
36 : : class NfaState
37 : : {
38 : : public:
39 : : /**
40 : : * Returns the NFA for regular expression r, connects the dangling arrows
41 : : * to the given accept state.
42 : : */
43 : 8942 : static NfaState* construct(Node r,
44 : : NfaState* accept,
45 : : std::vector<std::shared_ptr<NfaState>>& scache)
46 : : {
47 : 8942 : NfaState* rs = constructInternal(r, scache);
48 : 8942 : rs->connectTo(accept);
49 : 8942 : return rs;
50 : : }
51 : : /**
52 : : * Adds this state and all children connected by null to next.
53 : : */
54 : 163200 : void addToNext(std::unordered_set<NfaState*>& next)
55 : : {
56 : : // have property that all child states are also added to next if this
57 : : // state has been added to next
58 [ + + ]: 163200 : if (next.find(this) != next.end())
59 : : {
60 : 2118 : return;
61 : : }
62 : 161082 : next.insert(this);
63 : : std::map<Node, std::vector<NfaState*>>::iterator it =
64 : 161082 : d_children.find(Node::null());
65 [ + + ]: 161082 : if (it != d_children.end())
66 : : {
67 [ + + ]: 187554 : for (NfaState* cs : it->second)
68 : : {
69 : 125731 : cs->addToNext(next);
70 : : }
71 : : }
72 : : }
73 : : /**
74 : : * Processes the next input character nextChar from this state. Adds all
75 : : * next states to process to the next set.
76 : : */
77 : 140464 : void processNextChar(unsigned nextChar, std::unordered_set<NfaState*>& next)
78 : : {
79 [ + + ]: 260377 : for (const std::pair<const Node, std::vector<NfaState*>>& c : d_children)
80 : : {
81 : 119913 : const Node& r = c.first;
82 [ + + ]: 119913 : if (r.isNull())
83 : : {
84 : 55298 : continue;
85 : : }
86 : 64615 : bool accepts = false;
87 [ + + ][ + - ]: 64615 : switch (r.getKind())
88 : : {
89 : 54661 : case Kind::CONST_STRING:
90 [ - + ][ - + ]: 54661 : Assert(r.getConst<String>().size() == 1);
[ - - ]
91 : 54661 : accepts = (nextChar == r.getConst<String>().front());
92 : 54661 : break;
93 : 2163 : case Kind::REGEXP_RANGE:
94 : : {
95 : 2163 : unsigned a = r[0].getConst<String>().front();
96 : 2163 : unsigned b = r[1].getConst<String>().front();
97 [ + + ][ + + ]: 2163 : accepts = (a <= nextChar && nextChar <= b);
98 : : }
99 : 2163 : break;
100 : 7791 : case Kind::REGEXP_ALLCHAR: accepts = true; break;
101 : 0 : default: Unreachable() << "Unknown NFA edge " << c.first; break;
102 : : }
103 [ + + ]: 64615 : if (accepts)
104 : : {
105 [ + + ]: 57054 : for (NfaState* cs : c.second)
106 : : {
107 : 28527 : cs->addToNext(next);
108 : : }
109 : : }
110 : : }
111 : 140464 : }
112 : :
113 : : private:
114 : : /**
115 : : * Returns the (partial) NFA for regular expression r, whose dangling arrows
116 : : * are in d_arrows of the returned NfaState.
117 : : */
118 : 48507 : static NfaState* constructInternal(
119 : : Node r, std::vector<std::shared_ptr<NfaState>>& scache)
120 : : {
121 : 48507 : Kind k = r.getKind();
122 : : // Concatenation does not introduce a new state, instead returns the
123 : : // state of the first child.
124 [ + + ]: 48507 : if (k == Kind::REGEXP_CONCAT)
125 : : {
126 : 6530 : NfaState* first = nullptr;
127 : 6530 : NfaState* curr = nullptr;
128 [ + + ]: 27356 : for (const Node& rc : r)
129 : : {
130 : 20826 : NfaState* rcs = constructInternal(rc, scache);
131 [ + + ]: 20826 : if (first == nullptr)
132 : : {
133 : 6530 : first = rcs;
134 : 6530 : curr = first;
135 : 6530 : continue;
136 : : }
137 : : // connect previous to next
138 : 14296 : curr->connectTo(rcs);
139 : : // update current
140 : 14296 : curr = rcs;
141 : : }
142 : : // should have had 2+ arguments
143 [ + - ][ + - ]: 13060 : Assert(curr != first && curr != nullptr && first != nullptr);
[ + - ][ - + ]
[ - - ]
144 : : // copy arrows from last to first
145 : 6530 : first->d_arrows = curr->d_arrows;
146 : 6530 : curr->d_arrows.clear();
147 : 6530 : return first;
148 : : }
149 : : // Otherwise allocate a state.
150 : 41977 : NfaState* s = allocateState(scache);
151 : 41977 : std::vector<std::pair<NfaState*, Node>>& sarrows = s->d_arrows;
152 [ + + ][ + + ]: 41977 : switch (k)
[ - ]
153 : : {
154 : 13925 : case Kind::STRING_TO_REGEXP:
155 : : {
156 [ - + ][ - + ]: 13925 : Assert(r[0].isConst());
[ - - ]
157 : 13925 : const String& str = r[0].getConst<String>();
158 [ + + ]: 13925 : if (str.size() == 0)
159 : : {
160 : : // The regular expression is a no-op.
161 : 445 : sarrows.emplace_back(s, Node::null());
162 : : }
163 : : else
164 : : {
165 : : // this constructs N states in concatenation, where N is the length of
166 : : // the string, each connected via single characters
167 : 13480 : const std::vector<unsigned>& vec = str.getVec();
168 : 13480 : NfaState* curr = s;
169 : 13480 : NodeManager* nm = NodeManager::currentNM();
170 [ + + ]: 32067 : for (size_t i = 0, nvec = vec.size(); i < nvec; i++)
171 : : {
172 : 37174 : std::vector<unsigned> charVec{vec[i]};
173 : 37174 : Node nextChar = nm->mkConst(String(charVec));
174 [ + + ]: 18587 : if (i + 1 == vec.size())
175 : : {
176 : : // the last edge is the dangling pointer of the first
177 : 13480 : sarrows.emplace_back(curr, nextChar);
178 : : }
179 : : else
180 : : {
181 : 5107 : NfaState* next = allocateState(scache);
182 : 5107 : curr->d_children[nextChar].push_back(next);
183 : 5107 : curr = next;
184 : : }
185 : : }
186 : : }
187 : : }
188 : 13925 : break;
189 : 13938 : case Kind::REGEXP_ALLCHAR:
190 : 13938 : case Kind::REGEXP_RANGE: sarrows.emplace_back(s, r); break;
191 : 3127 : case Kind::REGEXP_UNION:
192 : : {
193 : : // connect to all children via null, take union of arrows
194 : 3127 : std::vector<NfaState*>& schildren = s->d_children[Node::null()];
195 [ + + ]: 10879 : for (const Node& rc : r)
196 : : {
197 : 7752 : NfaState* rcs = constructInternal(rc, scache);
198 : 7752 : schildren.push_back(rcs);
199 : 7752 : std::vector<std::pair<NfaState*, Node>>& rcsarrows = rcs->d_arrows;
200 : 7752 : sarrows.insert(sarrows.end(), rcsarrows.begin(), rcsarrows.end());
201 : 7752 : rcsarrows.clear();
202 : : }
203 : : }
204 : 3127 : break;
205 : 10987 : case Kind::REGEXP_STAR:
206 : : {
207 : 10987 : NfaState* body = constructInternal(r[0], scache);
208 : 10987 : s->d_children[Node::null()].push_back(body);
209 : : // body loops back to this state
210 : 10987 : body->connectTo(s);
211 : : // skip moves on
212 : 10987 : sarrows.emplace_back(s, Node::null());
213 : : }
214 : 10987 : break;
215 : 0 : default: Unreachable() << "Unknown regular expression " << r; break;
216 : : }
217 : 41977 : return s;
218 : : }
219 : : /** Connect dangling arrows of this to state s and clear */
220 : 34225 : void connectTo(NfaState* s)
221 : : {
222 [ + + ]: 73075 : for (std::pair<NfaState*, Node>& a : d_arrows)
223 : : {
224 : 38850 : a.first->d_children[a.second].push_back(s);
225 : : }
226 : 34225 : d_arrows.clear();
227 : 34225 : }
228 : : /** Allocate state, add to cache (for memory management) */
229 : 47084 : static NfaState* allocateState(std::vector<std::shared_ptr<NfaState>>& scache)
230 : : {
231 : 94168 : std::shared_ptr<NfaState> ret = std::make_shared<NfaState>();
232 : 47084 : scache.push_back(ret);
233 : 94168 : return ret.get();
234 : : }
235 : : /**
236 : : * Edges from this state. Maps constant characters, re.allchar or re.range
237 : : * to the list of children connected via an edge with that label.
238 : : */
239 : : std::map<Node, std::vector<NfaState*>> d_children;
240 : : /** Current dangling pointers */
241 : : std::vector<std::pair<NfaState*, Node>> d_arrows;
242 : : };
243 : :
244 : 18333 : bool RegExpEval::canEvaluate(const Node& r)
245 : : {
246 : 36666 : std::unordered_set<TNode> visited;
247 : 36666 : std::vector<TNode> visit;
248 : 36666 : TNode cur;
249 : 18333 : visit.push_back(r);
250 : 73568 : do
251 : : {
252 : 91901 : cur = visit.back();
253 : 91901 : visit.pop_back();
254 : : // if not already visited
255 [ + + ]: 91901 : if (visited.insert(cur).second)
256 : : {
257 [ + + ][ + + ]: 71571 : switch (cur.getKind())
[ + ]
258 : : {
259 : 20217 : case Kind::STRING_TO_REGEXP:
260 [ - + ]: 20217 : if (!cur[0].isConst())
261 : : {
262 : 0 : return false;
263 : : }
264 : 20217 : break;
265 : 2968 : case Kind::REGEXP_RANGE:
266 [ - + ]: 2968 : if (!utils::isCharacterRange(cur))
267 : : {
268 : 0 : return false;
269 : : }
270 : 2968 : break;
271 : 10855 : case Kind::REGEXP_ALLCHAR: break;
272 : 37082 : case Kind::REGEXP_UNION:
273 : : case Kind::REGEXP_CONCAT:
274 : : case Kind::REGEXP_STAR:
275 [ + + ]: 110695 : for (const Node& cc : cur)
276 : : {
277 : 73613 : visit.push_back(cc);
278 : : }
279 : 37082 : break;
280 : 449 : default: return false;
281 : : }
282 : : }
283 [ + + ]: 91452 : } while (!visit.empty());
284 : 17884 : return true;
285 : : }
286 : :
287 : 8942 : bool RegExpEval::evaluate(String& s, const Node& r)
288 : : {
289 [ + - ]: 8942 : Trace("re-eval") << "Evaluate " << s << " in " << r << std::endl;
290 : : // no intersection, complement, and r must be constant.
291 [ - + ][ - + ]: 8942 : Assert(canEvaluate(r));
[ - - ]
292 : 17884 : NfaState accept;
293 : 17884 : std::vector<std::shared_ptr<NfaState>> scache;
294 : 8942 : NfaState* rs = NfaState::construct(r, &accept, scache);
295 [ + - ]: 8942 : Trace("re-eval") << "NFA size is " << (scache.size() + 1) << std::endl;
296 : 17884 : std::unordered_set<NfaState*> curr;
297 : 8942 : rs->addToNext(curr);
298 : 8942 : const std::vector<unsigned>& vec = s.getVec();
299 [ + + ]: 33439 : for (size_t i = 0, nvec = vec.size(); i < nvec; i++)
300 : : {
301 [ + - ]: 53274 : Trace("re-eval") << "..process next char " << vec[i]
302 : 26637 : << ", #states=" << curr.size() << std::endl;
303 : 26637 : std::unordered_set<NfaState*> next;
304 [ + + ]: 167101 : for (NfaState* cs : curr)
305 : : {
306 : 140464 : cs->processNextChar(vec[i], next);
307 : : }
308 : : // if there are no more states, we are done
309 [ + + ]: 26637 : if (next.empty())
310 : : {
311 : 2140 : return false;
312 : : }
313 : 24497 : curr = next;
314 : : }
315 [ + - ]: 6802 : Trace("re-eval") << "..finish #states=" << curr.size() << std::endl;
316 : 6802 : return curr.find(&accept) != curr.end();
317 : : }
318 : :
319 : : } // namespace strings
320 : : } // namespace theory
321 : : } // namespace cvc5::internal
|
