Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Andres Noetzli, Daniel Larraz
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 a cache of skolems for theory of strings.
14 : : */
15 : :
16 : : #include "theory/strings/skolem_cache.h"
17 : :
18 : : #include "expr/attribute.h"
19 : : #include "expr/bound_var_manager.h"
20 : : #include "expr/skolem_manager.h"
21 : : #include "theory/rewriter.h"
22 : : #include "theory/strings/arith_entail.h"
23 : : #include "theory/strings/theory_strings_utils.h"
24 : : #include "theory/strings/word.h"
25 : : #include "util/rational.h"
26 : :
27 : : using namespace cvc5::internal::kind;
28 : :
29 : : namespace cvc5::internal {
30 : : namespace theory {
31 : : namespace strings {
32 : :
33 : 59551 : SkolemCache::SkolemCache(NodeManager* nm, Rewriter* rr) : d_nm(nm), d_rr(rr)
34 : : {
35 : 59551 : d_strType = d_nm->stringType();
36 : 59551 : d_zero = d_nm->mkConstInt(Rational(0));
37 : 59551 : }
38 : :
39 : 66651 : Node SkolemCache::mkSkolemCached(Node a,
40 : : Node b,
41 : : StringSkolemId id,
42 : : const char* c)
43 : : {
44 : 66651 : return mkTypedSkolemCached(d_strType, a, b, id, c);
45 : : }
46 : :
47 : 40228 : Node SkolemCache::mkSkolemCached(Node a, StringSkolemId id, const char* c)
48 : : {
49 : 40228 : return mkSkolemCached(a, Node::null(), id, c);
50 : : }
51 : :
52 : 67589 : Node SkolemCache::mkTypedSkolemCached(
53 : : TypeNode tn, Node a, Node b, StringSkolemId id, const char* c)
54 : : {
55 [ + - ]: 135178 : Trace("skolem-cache") << "mkTypedSkolemCached start: (" << id << ", " << a
56 : 67589 : << ", " << b << ")" << std::endl;
57 : 67589 : StringSkolemId idOrig = id;
58 : : // do not rewrite beforehand if we are not using optimizations, this is so
59 : : // that the proof checker does not depend on the rewriter.
60 [ + + ]: 67589 : if (d_rr != nullptr)
61 : : {
62 [ - + ][ + - ]: 54321 : a = a.isNull() ? a : d_rr->rewrite(a);
[ - - ]
63 [ + + ][ + + ]: 54321 : b = b.isNull() ? b : d_rr->rewrite(b);
[ - - ]
64 : : }
65 : 67589 : std::tie(id, a, b) = normalizeStringSkolem(id, a, b);
66 : :
67 : : // optimization: if we aren't asking for the purification skolem for constant
68 : : // a, and the skolem is equivalent to a, then we just return a.
69 [ + + ][ + + ]: 67589 : if (d_rr != nullptr && idOrig != SK_PURIFY && id == SK_PURIFY && a.isConst())
[ + - ][ + + ]
[ + + ]
70 : : {
71 [ + - ]: 4206 : Trace("skolem-cache") << "...optimization: return constant " << a
72 : 2103 : << std::endl;
73 : 2103 : return a;
74 : : }
75 : :
76 : 65486 : std::map<StringSkolemId, Node>::iterator it = d_skolemCache[a][b].find(id);
77 [ + + ]: 65486 : if (it != d_skolemCache[a][b].end())
78 : : {
79 [ + - ]: 15145 : Trace("skolem-cache") << "...return existing " << it->second << std::endl;
80 : : // already cached
81 : 15145 : return it->second;
82 : : }
83 : :
84 : 50341 : SkolemManager* sm = d_nm->getSkolemManager();
85 : 100682 : Node sk;
86 [ + - ][ - ]: 50341 : switch (id)
87 : : {
88 : : // exists k. k = a
89 : 50341 : case SK_PURIFY:
90 : : {
91 : 50341 : sk = sm->mkPurifySkolem(a);
92 : : }
93 : 50341 : break;
94 : : // these are eliminated by normalizeStringSkolem
95 : 0 : case SK_ID_V_SPT:
96 : : case SK_ID_V_SPT_REV:
97 : : case SK_ID_VC_SPT:
98 : : case SK_ID_VC_SPT_REV:
99 : : case SK_ID_C_SPT:
100 : : case SK_ID_C_SPT_REV:
101 : : case SK_ID_DC_SPT:
102 : : case SK_ID_DC_SPT_REM:
103 : : case SK_ID_DEQ_X:
104 : : case SK_ID_DEQ_Y:
105 : : case SK_FIRST_CTN_PRE:
106 : : case SK_FIRST_CTN_POST:
107 : : case SK_PREFIX:
108 : : case SK_SUFFIX_REM:
109 : 0 : Unhandled() << "Expected to eliminate Skolem ID " << id << std::endl;
110 : : break;
111 : 0 : default:
112 : : {
113 [ - - ]: 0 : Trace("skolem-cache")
114 : 0 : << "Don't know how to handle Skolem ID " << id << std::endl;
115 : 0 : sk = NodeManager::mkDummySkolem(c, tn, "string skolem");
116 : : }
117 : 0 : break;
118 : : }
119 [ + - ]: 50341 : Trace("skolem-cache") << "...returned " << sk << std::endl;
120 : 50341 : d_allSkolems.insert(sk);
121 : 50341 : d_skolemCache[a][b][id] = sk;
122 : 50341 : return sk;
123 : : }
124 : 938 : Node SkolemCache::mkTypedSkolemCached(TypeNode tn,
125 : : Node a,
126 : : StringSkolemId id,
127 : : const char* c)
128 : : {
129 : 938 : return mkTypedSkolemCached(tn, a, Node::null(), id, c);
130 : : }
131 : :
132 : 1095 : Node SkolemCache::mkSkolem(const char* c)
133 : : {
134 : : // TODO: eliminate this
135 : 2190 : Node n = NodeManager::mkDummySkolem(c, d_strType, "string skolem");
136 : 1095 : d_allSkolems.insert(n);
137 : 1095 : return n;
138 : : }
139 : :
140 : 4334 : bool SkolemCache::isSkolem(Node n) const
141 : : {
142 : 4334 : return d_allSkolems.find(n) != d_allSkolems.end();
143 : : }
144 : :
145 : : std::tuple<SkolemCache::StringSkolemId, Node, Node>
146 : 67589 : SkolemCache::normalizeStringSkolem(StringSkolemId id, Node a, Node b)
147 : : {
148 : : // eliminate in terms of prefix/suffix_rem
149 [ + + ]: 67589 : if (id == SK_FIRST_CTN_POST)
150 : : {
151 : : // SK_FIRST_CTN_POST(x, y) --->
152 : : // SK_SUFFIX_REM(x, (+ (str.len SK_FIRST_CTN_PRE(x, y)) (str.len y)))
153 : 2254 : id = SK_SUFFIX_REM;
154 : 4508 : Node pre = mkSkolemCached(a, b, SK_FIRST_CTN_PRE, "pre");
155 : 6762 : b = d_nm->mkNode(Kind::ADD,
156 : 4508 : d_nm->mkNode(Kind::STRING_LENGTH, pre),
157 : 6762 : d_nm->mkNode(Kind::STRING_LENGTH, b));
158 : : }
159 [ + - ][ + + ]: 65335 : else if (id == SK_ID_V_SPT || id == SK_ID_C_SPT)
160 : : {
161 : : // SK_ID_*_SPT(x, y) ---> SK_SUFFIX_REM(x, (str.len y))
162 : 705 : id = SK_SUFFIX_REM;
163 : 705 : b = d_nm->mkNode(Kind::STRING_LENGTH, b);
164 : : }
165 [ + - ][ + + ]: 64630 : else if (id == SK_ID_V_SPT_REV || id == SK_ID_C_SPT_REV)
166 : : {
167 : : // SK_ID_*_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) (str.len y)))
168 : 973 : id = SK_PREFIX;
169 : 2919 : b = d_nm->mkNode(Kind::SUB,
170 : 1946 : d_nm->mkNode(Kind::STRING_LENGTH, a),
171 : 2919 : d_nm->mkNode(Kind::STRING_LENGTH, b));
172 : : }
173 [ + + ]: 63657 : else if (id == SK_ID_VC_SPT)
174 : : {
175 : : // SK_ID_VC_SPT(x, y) ---> SK_SUFFIX_REM(x, 1)
176 : 4200 : id = SK_SUFFIX_REM;
177 : 4200 : b = d_nm->mkConstInt(Rational(1));
178 : : }
179 [ + + ]: 59457 : else if (id == SK_ID_VC_SPT_REV)
180 : : {
181 : : // SK_ID_VC_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) 1))
182 : 5799 : id = SK_PREFIX;
183 : 17397 : b = d_nm->mkNode(Kind::SUB,
184 : 11598 : d_nm->mkNode(Kind::STRING_LENGTH, a),
185 : 17397 : d_nm->mkConstInt(Rational(1)));
186 : : }
187 [ - + ]: 53658 : else if (id == SK_ID_DC_SPT)
188 : : {
189 : : // SK_ID_DC_SPT(x, y) ---> SK_PREFIX(x, 1)
190 : 0 : id = SK_PREFIX;
191 : 0 : b = d_nm->mkConstInt(Rational(1));
192 : : }
193 [ - + ]: 53658 : else if (id == SK_ID_DC_SPT_REM)
194 : : {
195 : : // SK_ID_DC_SPT_REM(x, y) ---> SK_SUFFIX_REM(x, 1)
196 : 0 : id = SK_SUFFIX_REM;
197 : 0 : b = d_nm->mkConstInt(Rational(1));
198 : : }
199 [ - + ]: 53658 : else if (id == SK_ID_DEQ_X)
200 : : {
201 : : // SK_ID_DEQ_X(x, y) ---> SK_PREFIX(y, (str.len x))
202 : 0 : id = SK_PREFIX;
203 : 0 : Node aOld = a;
204 : 0 : a = b;
205 : 0 : b = d_nm->mkNode(Kind::STRING_LENGTH, aOld);
206 : : }
207 [ - + ]: 53658 : else if (id == SK_ID_DEQ_Y)
208 : : {
209 : : // SK_ID_DEQ_Y(x, y) ---> SK_PREFIX(x, (str.len y))
210 : 0 : id = SK_PREFIX;
211 : 0 : b = d_nm->mkNode(Kind::STRING_LENGTH, b);
212 : : }
213 [ + + ]: 53658 : else if (id == SK_FIRST_CTN_PRE)
214 : : {
215 : : // SK_FIRST_CTN_PRE(x,y) ---> SK_PREFIX(x, indexof(x,y,0))
216 : 4510 : id = SK_PREFIX;
217 : 4510 : b = d_nm->mkNode(Kind::STRING_INDEXOF, a, b, d_zero);
218 : : }
219 : :
220 [ + + ][ + + ]: 67589 : if (id == SK_ID_V_UNIFIED_SPT || id == SK_ID_V_UNIFIED_SPT_REV)
221 : : {
222 : 7231 : bool isRev = (id == SK_ID_V_UNIFIED_SPT_REV);
223 : 14462 : Node la = d_nm->mkNode(Kind::STRING_LENGTH, a);
224 : 14462 : Node lb = d_nm->mkNode(Kind::STRING_LENGTH, b);
225 : 13669 : Node ta = isRev ? utils::mkPrefix(a, d_nm->mkNode(Kind::SUB, la, lb))
226 : 28924 : : utils::mkSuffix(a, lb);
227 : 13669 : Node tb = isRev ? utils::mkPrefix(b, d_nm->mkNode(Kind::SUB, lb, la))
228 : 21693 : : utils::mkSuffix(b, la);
229 : 7231 : id = SK_PURIFY;
230 : : // SK_ID_V_UNIFIED_SPT(x,y) --->
231 : : // ite(len(x) >= len(y), substr(x,0,str.len(y)), substr(y,0,str.len(x))
232 : 7231 : a = d_nm->mkNode(Kind::ITE, d_nm->mkNode(Kind::GEQ, la, lb), ta, tb);
233 : 7231 : b = Node::null();
234 : : }
235 : :
236 : : // now, eliminate prefix/suffix_rem in terms of purify
237 [ + + ]: 67589 : if (id == SK_PREFIX)
238 : : {
239 : : // SK_PREFIX(x,y) ---> SK_PURIFY(substr(x,0,y))
240 : 16657 : id = SK_PURIFY;
241 : 16657 : a = utils::mkPrefix(a, b);
242 : 16657 : b = Node::null();
243 : : }
244 [ + + ]: 50932 : else if (id == SK_SUFFIX_REM)
245 : : {
246 : : // SK_SUFFIX_REM(x,y) ---> SK_PURIFY(substr(x,y,str.len(x)-y))
247 : 12534 : id = SK_PURIFY;
248 : 12534 : a = utils::mkSuffix(a, b);
249 : 12534 : b = Node::null();
250 : : }
251 : :
252 [ + + ]: 67589 : if (d_rr != nullptr)
253 : : {
254 [ - + ][ + - ]: 54321 : a = a.isNull() ? a : d_rr->rewrite(a);
[ - - ]
255 [ + - ][ - + ]: 54321 : b = b.isNull() ? b : d_rr->rewrite(b);
[ - - ]
256 : : }
257 [ + - ]: 135178 : Trace("skolem-cache") << "normalizeStringSkolem end: (" << id << ", " << a
258 : 67589 : << ", " << b << ")" << std::endl;
259 : 67589 : return std::make_tuple(id, a, b);
260 : : }
261 : :
262 : 840 : Node SkolemCache::mkIndexVar(NodeManager* nm, Node t)
263 : : {
264 : 840 : TypeNode intType = nm->integerType();
265 : 840 : BoundVarManager* bvm = nm->getBoundVarManager();
266 : : // Note that proof rules may depend on the name of this variable.
267 : : return bvm->mkBoundVar(
268 : 1680 : BoundVarId::STRINGS_INDEX, t, "@var.str_index", intType);
269 : : }
270 : :
271 : 274 : Node SkolemCache::mkLengthVar(NodeManager* nm, Node t)
272 : : {
273 : 274 : TypeNode intType = nm->integerType();
274 : 274 : BoundVarManager* bvm = nm->getBoundVarManager();
275 : : return bvm->mkBoundVar(
276 : 548 : BoundVarId::STRINGS_LENGTH, t, "@var.str_length", intType);
277 : : }
278 : :
279 : 1472 : Node SkolemCache::mkSkolemFun(NodeManager* nm, SkolemId id, Node a, Node b)
280 : : {
281 : 2944 : std::vector<Node> cacheVals = getSkolemCacheVals(a, b);
282 : 1472 : SkolemManager* sm = nm->getSkolemManager();
283 : 1472 : Node k = sm->mkSkolemFunction(id, cacheVals);
284 : 1472 : d_allSkolems.insert(k);
285 : 2944 : return k;
286 : : }
287 : :
288 : 1472 : std::vector<Node> SkolemCache::getSkolemCacheVals(const Node& a,
289 : : const Node& b) const
290 : : {
291 : 1472 : std::vector<Node> cacheVals;
292 [ + + ]: 4416 : for (size_t i = 0; i < 2; i++)
293 : : {
294 [ + + ]: 5888 : Node n = i == 0 ? a : b;
295 [ + + ]: 2944 : if (!n.isNull())
296 : : {
297 [ + + ][ + + ]: 2430 : n = d_rr != nullptr ? d_rr->rewrite(n) : n;
[ - - ]
298 : 2430 : cacheVals.push_back(n);
299 : : }
300 : : }
301 : 1472 : return cacheVals;
302 : : }
303 : :
304 : : } // namespace strings
305 : : } // namespace theory
306 : : } // namespace cvc5::internal
|
