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 a cache of skolems for theory of strings.
11 : : */
12 : :
13 : : #include "theory/strings/skolem_cache.h"
14 : :
15 : : #include "expr/attribute.h"
16 : : #include "expr/bound_var_manager.h"
17 : : #include "expr/skolem_manager.h"
18 : : #include "theory/rewriter.h"
19 : : #include "theory/strings/arith_entail.h"
20 : : #include "theory/strings/theory_strings_utils.h"
21 : : #include "theory/strings/word.h"
22 : : #include "util/rational.h"
23 : :
24 : : using namespace cvc5::internal::kind;
25 : :
26 : : namespace cvc5::internal {
27 : : namespace theory {
28 : : namespace strings {
29 : :
30 : 57906 : SkolemCache::SkolemCache(NodeManager* nm, Rewriter* rr) : d_nm(nm), d_rr(rr)
31 : : {
32 : 57906 : d_strType = d_nm->stringType();
33 : 57906 : d_zero = d_nm->mkConstInt(Rational(0));
34 : 57906 : }
35 : :
36 : 65738 : Node SkolemCache::mkSkolemCached(Node a,
37 : : Node b,
38 : : StringSkolemId id,
39 : : const char* c)
40 : : {
41 : 65738 : return mkTypedSkolemCached(d_strType, a, b, id, c);
42 : : }
43 : :
44 : 39518 : Node SkolemCache::mkSkolemCached(Node a, StringSkolemId id, const char* c)
45 : : {
46 : 39518 : return mkSkolemCached(a, Node::null(), id, c);
47 : : }
48 : :
49 : 66637 : Node SkolemCache::mkTypedSkolemCached(
50 : : TypeNode tn, Node a, Node b, StringSkolemId id, const char* c)
51 : : {
52 [ + - ]: 133274 : Trace("skolem-cache") << "mkTypedSkolemCached start: (" << id << ", " << a
53 : 66637 : << ", " << b << ")" << std::endl;
54 : 66637 : StringSkolemId idOrig = id;
55 : : // do not rewrite beforehand if we are not using optimizations, this is so
56 : : // that the proof checker does not depend on the rewriter.
57 [ + + ]: 66637 : if (d_rr != nullptr)
58 : : {
59 [ - + ][ + - ]: 54843 : a = a.isNull() ? a : d_rr->rewrite(a);
[ - - ]
60 [ + + ][ + + ]: 54843 : b = b.isNull() ? b : d_rr->rewrite(b);
[ - - ]
61 : : }
62 : 66637 : std::tie(id, a, b) = normalizeStringSkolem(id, a, b);
63 : :
64 : : // optimization: if we aren't asking for the purification skolem for constant
65 : : // a, and the skolem is equivalent to a, then we just return a.
66 [ + + ][ + + ]: 66637 : if (d_rr != nullptr && idOrig != SK_PURIFY && id == SK_PURIFY && a.isConst())
[ + - ][ + + ]
[ + + ]
67 : : {
68 [ + - ]: 4336 : Trace("skolem-cache") << "...optimization: return constant " << a
69 : 2168 : << std::endl;
70 : 2168 : return a;
71 : : }
72 : :
73 : 64469 : std::map<StringSkolemId, Node>::iterator it = d_skolemCache[a][b].find(id);
74 [ + + ]: 64469 : if (it != d_skolemCache[a][b].end())
75 : : {
76 [ + - ]: 15286 : Trace("skolem-cache") << "...return existing " << it->second << std::endl;
77 : : // already cached
78 : 15286 : return it->second;
79 : : }
80 : :
81 : 49183 : SkolemManager* sm = d_nm->getSkolemManager();
82 : 49183 : Node sk;
83 [ + - ][ - ]: 49183 : switch (id)
84 : : {
85 : : // exists k. k = a
86 : 49183 : case SK_PURIFY:
87 : : {
88 : 49183 : sk = sm->mkPurifySkolem(a);
89 : : }
90 : 49183 : break;
91 : : // these are eliminated by normalizeStringSkolem
92 : 0 : case SK_ID_V_SPT:
93 : : case SK_ID_V_SPT_REV:
94 : : case SK_ID_VC_SPT:
95 : : case SK_ID_VC_SPT_REV:
96 : : case SK_ID_C_SPT:
97 : : case SK_ID_C_SPT_REV:
98 : : case SK_ID_DC_SPT:
99 : : case SK_ID_DC_SPT_REM:
100 : : case SK_ID_DEQ_X:
101 : : case SK_ID_DEQ_Y:
102 : : case SK_FIRST_CTN_PRE:
103 : : case SK_FIRST_CTN_POST:
104 : : case SK_PREFIX:
105 : : case SK_SUFFIX_REM:
106 : 0 : Unhandled() << "Expected to eliminate Skolem ID " << id << std::endl;
107 : : break;
108 : 0 : default:
109 : : {
110 [ - - ]: 0 : Trace("skolem-cache")
111 : 0 : << "Don't know how to handle Skolem ID " << id << std::endl;
112 : 0 : sk = NodeManager::mkDummySkolem(c, tn);
113 : : }
114 : 0 : break;
115 : : }
116 [ + - ]: 49183 : Trace("skolem-cache") << "...returned " << sk << std::endl;
117 : 49183 : d_allSkolems.insert(sk);
118 : 49183 : d_skolemCache[a][b][id] = sk;
119 : 49183 : return sk;
120 : 49183 : }
121 : 899 : Node SkolemCache::mkTypedSkolemCached(TypeNode tn,
122 : : Node a,
123 : : StringSkolemId id,
124 : : const char* c)
125 : : {
126 : 899 : return mkTypedSkolemCached(tn, a, Node::null(), id, c);
127 : : }
128 : :
129 : 1206 : Node SkolemCache::mkSkolem(const char* c)
130 : : {
131 : : // TODO: eliminate this
132 : 2412 : Node n = NodeManager::mkDummySkolem(c, d_strType);
133 : 1206 : d_allSkolems.insert(n);
134 : 1206 : return n;
135 : 0 : }
136 : :
137 : 4132 : bool SkolemCache::isSkolem(Node n) const
138 : : {
139 : 4132 : return d_allSkolems.find(n) != d_allSkolems.end();
140 : : }
141 : :
142 : : std::tuple<SkolemCache::StringSkolemId, Node, Node>
143 : 66637 : SkolemCache::normalizeStringSkolem(StringSkolemId id, Node a, Node b)
144 : : {
145 : : // eliminate in terms of prefix/suffix_rem
146 [ + + ]: 66637 : if (id == SK_FIRST_CTN_POST)
147 : : {
148 : : // SK_FIRST_CTN_POST(x, y) --->
149 : : // SK_SUFFIX_REM(x, (+ (str.len SK_FIRST_CTN_PRE(x, y)) (str.len y)))
150 : 2518 : id = SK_SUFFIX_REM;
151 : 5036 : Node pre = mkSkolemCached(a, b, SK_FIRST_CTN_PRE, "pre");
152 [ + + ][ - - ]: 12590 : b = d_nm->mkNode(Kind::ADD,
153 : 5036 : {d_nm->mkNode(Kind::STRING_LENGTH, pre),
154 : 7554 : d_nm->mkNode(Kind::STRING_LENGTH, b)});
155 : 2518 : }
156 [ + - ][ + + ]: 64119 : else if (id == SK_ID_V_SPT || id == SK_ID_C_SPT)
157 : : {
158 : : // SK_ID_*_SPT(x, y) ---> SK_SUFFIX_REM(x, (str.len y))
159 : 650 : id = SK_SUFFIX_REM;
160 : 650 : b = d_nm->mkNode(Kind::STRING_LENGTH, b);
161 : : }
162 [ + - ][ + + ]: 63469 : else if (id == SK_ID_V_SPT_REV || id == SK_ID_C_SPT_REV)
163 : : {
164 : : // SK_ID_*_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) (str.len y)))
165 : 852 : id = SK_PREFIX;
166 [ + + ][ - - ]: 4260 : b = d_nm->mkNode(Kind::SUB,
167 : 1704 : {d_nm->mkNode(Kind::STRING_LENGTH, a),
168 : 2556 : d_nm->mkNode(Kind::STRING_LENGTH, b)});
169 : : }
170 [ + + ]: 62617 : else if (id == SK_ID_VC_SPT)
171 : : {
172 : : // SK_ID_VC_SPT(x, y) ---> SK_SUFFIX_REM(x, 1)
173 : 3904 : id = SK_SUFFIX_REM;
174 : 3904 : b = d_nm->mkConstInt(Rational(1));
175 : : }
176 [ + + ]: 58713 : else if (id == SK_ID_VC_SPT_REV)
177 : : {
178 : : // SK_ID_VC_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) 1))
179 : 5500 : id = SK_PREFIX;
180 [ + + ][ - - ]: 27500 : b = d_nm->mkNode(
181 : : Kind::SUB,
182 : 22000 : {d_nm->mkNode(Kind::STRING_LENGTH, a), d_nm->mkConstInt(Rational(1))});
183 : : }
184 [ - + ]: 53213 : else if (id == SK_ID_DC_SPT)
185 : : {
186 : : // SK_ID_DC_SPT(x, y) ---> SK_PREFIX(x, 1)
187 : 0 : id = SK_PREFIX;
188 : 0 : b = d_nm->mkConstInt(Rational(1));
189 : : }
190 [ - + ]: 53213 : else if (id == SK_ID_DC_SPT_REM)
191 : : {
192 : : // SK_ID_DC_SPT_REM(x, y) ---> SK_SUFFIX_REM(x, 1)
193 : 0 : id = SK_SUFFIX_REM;
194 : 0 : b = d_nm->mkConstInt(Rational(1));
195 : : }
196 [ - + ]: 53213 : else if (id == SK_ID_DEQ_X)
197 : : {
198 : : // SK_ID_DEQ_X(x, y) ---> SK_PREFIX(y, (str.len x))
199 : 0 : id = SK_PREFIX;
200 : 0 : Node aOld = a;
201 : 0 : a = b;
202 : 0 : b = d_nm->mkNode(Kind::STRING_LENGTH, aOld);
203 : 0 : }
204 [ - + ]: 53213 : else if (id == SK_ID_DEQ_Y)
205 : : {
206 : : // SK_ID_DEQ_Y(x, y) ---> SK_PREFIX(x, (str.len y))
207 : 0 : id = SK_PREFIX;
208 : 0 : b = d_nm->mkNode(Kind::STRING_LENGTH, b);
209 : : }
210 [ + + ]: 53213 : else if (id == SK_FIRST_CTN_PRE)
211 : : {
212 : : // SK_FIRST_CTN_PRE(x,y) ---> SK_PREFIX(x, indexof(x,y,0))
213 : 5038 : id = SK_PREFIX;
214 : 5038 : b = d_nm->mkNode(Kind::STRING_INDEXOF, a, b, d_zero);
215 : : }
216 : :
217 [ + + ][ + + ]: 66637 : if (id == SK_ID_V_UNIFIED_SPT || id == SK_ID_V_UNIFIED_SPT_REV)
218 : : {
219 : 7063 : bool isRev = (id == SK_ID_V_UNIFIED_SPT_REV);
220 : 7063 : Node la = d_nm->mkNode(Kind::STRING_LENGTH, a);
221 : 7063 : Node lb = d_nm->mkNode(Kind::STRING_LENGTH, b);
222 : 13389 : Node ta = isRev ? utils::mkPrefix(a, d_nm->mkNode(Kind::SUB, la, lb))
223 : 21189 : : utils::mkSuffix(a, lb);
224 : 13389 : Node tb = isRev ? utils::mkPrefix(b, d_nm->mkNode(Kind::SUB, lb, la))
225 : 21189 : : utils::mkSuffix(b, la);
226 : 7063 : id = SK_PURIFY;
227 : : // SK_ID_V_UNIFIED_SPT(x,y) --->
228 : : // ite(len(x) >= len(y), substr(x,0,str.len(y)), substr(y,0,str.len(x))
229 : 7063 : a = d_nm->mkNode(Kind::ITE, d_nm->mkNode(Kind::GEQ, la, lb), ta, tb);
230 : 7063 : b = Node::null();
231 : 7063 : }
232 : :
233 : : // now, eliminate prefix/suffix_rem in terms of purify
234 [ + + ]: 66637 : if (id == SK_PREFIX)
235 : : {
236 : : // SK_PREFIX(x,y) ---> SK_PURIFY(substr(x,0,y))
237 : 16360 : id = SK_PURIFY;
238 : 16360 : a = utils::mkPrefix(a, b);
239 : 16360 : b = Node::null();
240 : : }
241 [ + + ]: 50277 : else if (id == SK_SUFFIX_REM)
242 : : {
243 : : // SK_SUFFIX_REM(x,y) ---> SK_PURIFY(substr(x,y,str.len(x)-y))
244 : 12042 : id = SK_PURIFY;
245 : 12042 : a = utils::mkSuffix(a, b);
246 : 12042 : b = Node::null();
247 : : }
248 [ + + ]: 38235 : else if (id == RE_FIRST_MATCH_PRE)
249 : : {
250 : 53 : id = SK_PURIFY;
251 : 106 : Node idof = d_nm->mkNode(Kind::STRING_INDEXOF_RE, a, b, d_zero);
252 : 53 : a = utils::mkPrefix(a, idof);
253 : 53 : b = Node::null();
254 : 53 : }
255 [ + + ]: 38182 : else if (id == RE_FIRST_MATCH)
256 : : {
257 : 53 : id = SK_PURIFY;
258 : 106 : Node idof = d_nm->mkNode(Kind::STRING_INDEXOF_RE, a, b, d_zero);
259 : 106 : Node occ = mkSkolemFun(d_nm, SkolemId::STRINGS_OCCUR_INDEX_RE, a, b);
260 : 53 : Node one = d_nm->mkConstInt(Rational(1));
261 : 106 : Node occ1 = d_nm->mkNode(Kind::APPLY_UF, occ, one);
262 : 106 : a = d_nm->mkNode(
263 : 159 : Kind::STRING_SUBSTR, a, idof, d_nm->mkNode(Kind::SUB, occ1, idof));
264 : 53 : b = Node::null();
265 : 53 : }
266 [ + + ]: 38129 : else if (id == RE_FIRST_MATCH_POST)
267 : : {
268 : 53 : id = SK_PURIFY;
269 : 106 : Node occ = mkSkolemFun(d_nm, SkolemId::STRINGS_OCCUR_INDEX_RE, a, b);
270 : 53 : Node one = d_nm->mkConstInt(Rational(1));
271 : 106 : Node occ1 = d_nm->mkNode(Kind::APPLY_UF, occ, one);
272 : 53 : a = utils::mkSuffix(a, occ1);
273 : 53 : b = Node::null();
274 : 53 : }
275 : :
276 [ + + ]: 66637 : if (d_rr != nullptr)
277 : : {
278 [ - + ][ + - ]: 54843 : a = a.isNull() ? a : d_rr->rewrite(a);
[ - - ]
279 [ + - ][ - + ]: 54843 : b = b.isNull() ? b : d_rr->rewrite(b);
[ - - ]
280 : : }
281 [ + - ]: 133274 : Trace("skolem-cache") << "normalizeStringSkolem end: (" << id << ", " << a
282 : 66637 : << ", " << b << ")" << std::endl;
283 : 66637 : return std::make_tuple(id, a, b);
284 : : }
285 : :
286 : 857 : Node SkolemCache::mkIndexVar(NodeManager* nm, Node t)
287 : : {
288 : 857 : TypeNode intType = nm->integerType();
289 : 857 : BoundVarManager* bvm = nm->getBoundVarManager();
290 : : // Note that proof rules may depend on the name of this variable.
291 : : return bvm->mkBoundVar(
292 : 1714 : BoundVarId::STRINGS_INDEX, t, "@var.str_index", intType);
293 : 857 : }
294 : :
295 : 236 : Node SkolemCache::mkLengthVar(NodeManager* nm, Node t)
296 : : {
297 : 236 : TypeNode intType = nm->integerType();
298 : 236 : BoundVarManager* bvm = nm->getBoundVarManager();
299 : : return bvm->mkBoundVar(
300 : 472 : BoundVarId::STRINGS_LENGTH, t, "@var.str_length", intType);
301 : 236 : }
302 : :
303 : 18 : Node SkolemCache::mkRegExpEqVar(NodeManager* nm, Node eq)
304 : : {
305 [ - + ][ - + ]: 18 : Assert(eq.getKind() == Kind::EQUAL);
[ - - ]
306 : 18 : TypeNode stringType = nm->stringType();
307 : 18 : BoundVarManager* bvm = nm->getBoundVarManager();
308 : : return bvm->mkBoundVar(
309 : 36 : BoundVarId::STRINGS_REG_EXP_EQ, eq, "@var.re_eq", stringType);
310 : 18 : }
311 : :
312 : 1448 : Node SkolemCache::mkSkolemFun(NodeManager* nm, SkolemId id, Node a, Node b)
313 : : {
314 : 1448 : std::vector<Node> cacheVals = getSkolemCacheVals(a, b);
315 : 1448 : SkolemManager* sm = nm->getSkolemManager();
316 : 1448 : Node k = sm->mkSkolemFunction(id, cacheVals);
317 : 1448 : d_allSkolems.insert(k);
318 : 2896 : return k;
319 : 1448 : }
320 : :
321 : 1448 : std::vector<Node> SkolemCache::getSkolemCacheVals(const Node& a,
322 : : const Node& b) const
323 : : {
324 : 1448 : std::vector<Node> cacheVals;
325 [ + + ]: 4344 : for (size_t i = 0; i < 2; i++)
326 : : {
327 [ + + ]: 2896 : Node n = i == 0 ? a : b;
328 [ + + ]: 2896 : if (!n.isNull())
329 : : {
330 [ + + ][ + + ]: 2325 : n = d_rr != nullptr ? d_rr->rewrite(n) : n;
[ - - ]
331 : 2325 : cacheVals.push_back(n);
332 : : }
333 : 2896 : }
334 : 1448 : return cacheVals;
335 : 0 : }
336 : :
337 : : } // namespace strings
338 : : } // namespace theory
339 : : } // namespace cvc5::internal
|
