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-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 : : * 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 : : /**
34 : : * A bound variable corresponding to the universally quantified integer
35 : : * variable used to range over the valid positions in a string, used
36 : : * for axiomatizing the behavior of some term.
37 : : */
38 : : struct IndexVarAttributeId
39 : : {
40 : : };
41 : : typedef expr::Attribute<IndexVarAttributeId, Node> IndexVarAttribute;
42 : :
43 : : /**
44 : : * A bound variable corresponding to the universally quantified integer
45 : : * variable used to range over the valid lengths of a string, used for
46 : : * axiomatizing the behavior of some term.
47 : : */
48 : : struct LengthVarAttributeId
49 : : {
50 : : };
51 : : typedef expr::Attribute<LengthVarAttributeId, Node> LengthVarAttribute;
52 : :
53 : 56863 : SkolemCache::SkolemCache(NodeManager* nm, Rewriter* rr) : d_nm(nm), d_rr(rr)
54 : : {
55 : 56863 : d_strType = d_nm->stringType();
56 : 56863 : d_zero = d_nm->mkConstInt(Rational(0));
57 : 56863 : }
58 : :
59 : 56901 : Node SkolemCache::mkSkolemCached(Node a,
60 : : Node b,
61 : : StringSkolemId id,
62 : : const char* c)
63 : : {
64 : 56901 : return mkTypedSkolemCached(d_strType, a, b, id, c);
65 : : }
66 : :
67 : 34089 : Node SkolemCache::mkSkolemCached(Node a, StringSkolemId id, const char* c)
68 : : {
69 : 34089 : return mkSkolemCached(a, Node::null(), id, c);
70 : : }
71 : :
72 : 57751 : Node SkolemCache::mkTypedSkolemCached(
73 : : TypeNode tn, Node a, Node b, StringSkolemId id, const char* c)
74 : : {
75 [ + - ]: 115502 : Trace("skolem-cache") << "mkTypedSkolemCached start: (" << id << ", " << a
76 : 57751 : << ", " << b << ")" << std::endl;
77 : 57751 : StringSkolemId idOrig = id;
78 : : // do not rewrite beforehand if we are not using optimizations, this is so
79 : : // that the proof checker does not depend on the rewriter.
80 [ + + ]: 57751 : if (d_rr != nullptr)
81 : : {
82 [ - + ][ + - ]: 46586 : a = a.isNull() ? a : d_rr->rewrite(a);
[ - - ]
83 [ + + ][ + + ]: 46586 : b = b.isNull() ? b : d_rr->rewrite(b);
[ - - ]
84 : : }
85 : 57751 : std::tie(id, a, b) = normalizeStringSkolem(id, a, b);
86 : :
87 : : // optimization: if we aren't asking for the purification skolem for constant
88 : : // a, and the skolem is equivalent to a, then we just return a.
89 [ + + ][ + + ]: 57751 : if (d_rr != nullptr && idOrig != SK_PURIFY && id == SK_PURIFY && a.isConst())
[ + - ][ + + ]
[ + + ]
90 : : {
91 [ + - ]: 3870 : Trace("skolem-cache") << "...optimization: return constant " << a
92 : 1935 : << std::endl;
93 : 1935 : return a;
94 : : }
95 : :
96 : 55816 : std::map<StringSkolemId, Node>::iterator it = d_skolemCache[a][b].find(id);
97 [ + + ]: 55816 : if (it != d_skolemCache[a][b].end())
98 : : {
99 [ + - ]: 12854 : Trace("skolem-cache") << "...return existing " << it->second << std::endl;
100 : : // already cached
101 : 12854 : return it->second;
102 : : }
103 : :
104 : 42962 : SkolemManager* sm = d_nm->getSkolemManager();
105 : 85924 : Node sk;
106 [ + - ][ - ]: 42962 : switch (id)
107 : : {
108 : : // exists k. k = a
109 : 42962 : case SK_PURIFY:
110 : : {
111 : 42962 : sk = sm->mkPurifySkolem(a);
112 : : }
113 : 42962 : break;
114 : : // these are eliminated by normalizeStringSkolem
115 : 0 : case SK_ID_V_SPT:
116 : : case SK_ID_V_SPT_REV:
117 : : case SK_ID_VC_SPT:
118 : : case SK_ID_VC_SPT_REV:
119 : : case SK_ID_C_SPT:
120 : : case SK_ID_C_SPT_REV:
121 : : case SK_ID_DC_SPT:
122 : : case SK_ID_DC_SPT_REM:
123 : : case SK_ID_DEQ_X:
124 : : case SK_ID_DEQ_Y:
125 : : case SK_FIRST_CTN_PRE:
126 : : case SK_FIRST_CTN_POST:
127 : : case SK_PREFIX:
128 : : case SK_SUFFIX_REM:
129 : 0 : Unhandled() << "Expected to eliminate Skolem ID " << id << std::endl;
130 : : break;
131 : 0 : default:
132 : : {
133 [ - - ]: 0 : Trace("skolem-cache")
134 : 0 : << "Don't know how to handle Skolem ID " << id << std::endl;
135 : 0 : sk = NodeManager::mkDummySkolem(c, tn, "string skolem");
136 : : }
137 : 0 : break;
138 : : }
139 [ + - ]: 42962 : Trace("skolem-cache") << "...returned " << sk << std::endl;
140 : 42962 : d_allSkolems.insert(sk);
141 : 42962 : d_skolemCache[a][b][id] = sk;
142 : 42962 : return sk;
143 : : }
144 : 850 : Node SkolemCache::mkTypedSkolemCached(TypeNode tn,
145 : : Node a,
146 : : StringSkolemId id,
147 : : const char* c)
148 : : {
149 : 850 : return mkTypedSkolemCached(tn, a, Node::null(), id, c);
150 : : }
151 : :
152 : 1095 : Node SkolemCache::mkSkolem(const char* c)
153 : : {
154 : : // TODO: eliminate this
155 : 2190 : Node n = NodeManager::mkDummySkolem(c, d_strType, "string skolem");
156 : 1095 : d_allSkolems.insert(n);
157 : 1095 : return n;
158 : : }
159 : :
160 : 4310 : bool SkolemCache::isSkolem(Node n) const
161 : : {
162 : 4310 : return d_allSkolems.find(n) != d_allSkolems.end();
163 : : }
164 : :
165 : : std::tuple<SkolemCache::StringSkolemId, Node, Node>
166 : 57751 : SkolemCache::normalizeStringSkolem(StringSkolemId id, Node a, Node b)
167 : : {
168 : : // eliminate in terms of prefix/suffix_rem
169 [ + + ]: 57751 : if (id == SK_FIRST_CTN_POST)
170 : : {
171 : : // SK_FIRST_CTN_POST(x, y) --->
172 : : // SK_SUFFIX_REM(x, (+ (str.len SK_FIRST_CTN_PRE(x, y)) (str.len y)))
173 : 1681 : id = SK_SUFFIX_REM;
174 : 3362 : Node pre = mkSkolemCached(a, b, SK_FIRST_CTN_PRE, "pre");
175 : 5043 : b = d_nm->mkNode(Kind::ADD,
176 : 3362 : d_nm->mkNode(Kind::STRING_LENGTH, pre),
177 : 5043 : d_nm->mkNode(Kind::STRING_LENGTH, b));
178 : : }
179 [ + - ][ + + ]: 56070 : else if (id == SK_ID_V_SPT || id == SK_ID_C_SPT)
180 : : {
181 : : // SK_ID_*_SPT(x, y) ---> SK_SUFFIX_REM(x, (str.len y))
182 : 696 : id = SK_SUFFIX_REM;
183 : 696 : b = d_nm->mkNode(Kind::STRING_LENGTH, b);
184 : : }
185 [ + - ][ + + ]: 55374 : else if (id == SK_ID_V_SPT_REV || id == SK_ID_C_SPT_REV)
186 : : {
187 : : // SK_ID_*_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) (str.len y)))
188 : 682 : id = SK_PREFIX;
189 : 2046 : b = d_nm->mkNode(Kind::SUB,
190 : 1364 : d_nm->mkNode(Kind::STRING_LENGTH, a),
191 : 2046 : d_nm->mkNode(Kind::STRING_LENGTH, b));
192 : : }
193 [ + + ]: 54692 : else if (id == SK_ID_VC_SPT)
194 : : {
195 : : // SK_ID_VC_SPT(x, y) ---> SK_SUFFIX_REM(x, 1)
196 : 3376 : id = SK_SUFFIX_REM;
197 : 3376 : b = d_nm->mkConstInt(Rational(1));
198 : : }
199 [ + + ]: 51316 : else if (id == SK_ID_VC_SPT_REV)
200 : : {
201 : : // SK_ID_VC_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) 1))
202 : 4704 : id = SK_PREFIX;
203 : 14112 : b = d_nm->mkNode(Kind::SUB,
204 : 9408 : d_nm->mkNode(Kind::STRING_LENGTH, a),
205 : 14112 : d_nm->mkConstInt(Rational(1)));
206 : : }
207 [ - + ]: 46612 : else if (id == SK_ID_DC_SPT)
208 : : {
209 : : // SK_ID_DC_SPT(x, y) ---> SK_PREFIX(x, 1)
210 : 0 : id = SK_PREFIX;
211 : 0 : b = d_nm->mkConstInt(Rational(1));
212 : : }
213 [ - + ]: 46612 : else if (id == SK_ID_DC_SPT_REM)
214 : : {
215 : : // SK_ID_DC_SPT_REM(x, y) ---> SK_SUFFIX_REM(x, 1)
216 : 0 : id = SK_SUFFIX_REM;
217 : 0 : b = d_nm->mkConstInt(Rational(1));
218 : : }
219 [ - + ]: 46612 : else if (id == SK_ID_DEQ_X)
220 : : {
221 : : // SK_ID_DEQ_X(x, y) ---> SK_PREFIX(y, (str.len x))
222 : 0 : id = SK_PREFIX;
223 : 0 : Node aOld = a;
224 : 0 : a = b;
225 : 0 : b = d_nm->mkNode(Kind::STRING_LENGTH, aOld);
226 : : }
227 [ - + ]: 46612 : else if (id == SK_ID_DEQ_Y)
228 : : {
229 : : // SK_ID_DEQ_Y(x, y) ---> SK_PREFIX(x, (str.len y))
230 : 0 : id = SK_PREFIX;
231 : 0 : b = d_nm->mkNode(Kind::STRING_LENGTH, b);
232 : : }
233 [ + + ]: 46612 : else if (id == SK_FIRST_CTN_PRE)
234 : : {
235 : : // SK_FIRST_CTN_PRE(x,y) ---> SK_PREFIX(x, indexof(x,y,0))
236 : 3364 : id = SK_PREFIX;
237 : 3364 : b = d_nm->mkNode(Kind::STRING_INDEXOF, a, b, d_zero);
238 : : }
239 : :
240 [ + + ][ + + ]: 57751 : if (id == SK_ID_V_UNIFIED_SPT || id == SK_ID_V_UNIFIED_SPT_REV)
241 : : {
242 : 6307 : bool isRev = (id == SK_ID_V_UNIFIED_SPT_REV);
243 : 12614 : Node la = d_nm->mkNode(Kind::STRING_LENGTH, a);
244 : 12614 : Node lb = d_nm->mkNode(Kind::STRING_LENGTH, b);
245 : 11539 : Node ta = isRev ? utils::mkPrefix(a, d_nm->mkNode(Kind::SUB, la, lb))
246 : 25228 : : utils::mkSuffix(a, lb);
247 : 11539 : Node tb = isRev ? utils::mkPrefix(b, d_nm->mkNode(Kind::SUB, lb, la))
248 : 18921 : : utils::mkSuffix(b, la);
249 : 6307 : id = SK_PURIFY;
250 : : // SK_ID_V_UNIFIED_SPT(x,y) --->
251 : : // ite(len(x) >= len(y), substr(x,0,str.len(y)), substr(y,0,str.len(x))
252 : 6307 : a = d_nm->mkNode(Kind::ITE, d_nm->mkNode(Kind::GEQ, la, lb), ta, tb);
253 : 6307 : b = Node::null();
254 : : }
255 : :
256 : : // now, eliminate prefix/suffix_rem in terms of purify
257 [ + + ]: 57751 : if (id == SK_PREFIX)
258 : : {
259 : : // SK_PREFIX(x,y) ---> SK_PURIFY(substr(x,0,y))
260 : 13791 : id = SK_PURIFY;
261 : 13791 : a = utils::mkPrefix(a, b);
262 : 13791 : b = Node::null();
263 : : }
264 [ + + ]: 43960 : else if (id == SK_SUFFIX_REM)
265 : : {
266 : : // SK_SUFFIX_REM(x,y) ---> SK_PURIFY(substr(x,y,str.len(x)-y))
267 : 10794 : id = SK_PURIFY;
268 : 10794 : a = utils::mkSuffix(a, b);
269 : 10794 : b = Node::null();
270 : : }
271 : :
272 [ + + ]: 57751 : if (d_rr != nullptr)
273 : : {
274 [ - + ][ + - ]: 46586 : a = a.isNull() ? a : d_rr->rewrite(a);
[ - - ]
275 [ + - ][ - + ]: 46586 : b = b.isNull() ? b : d_rr->rewrite(b);
[ - - ]
276 : : }
277 [ + - ]: 115502 : Trace("skolem-cache") << "normalizeStringSkolem end: (" << id << ", " << a
278 : 57751 : << ", " << b << ")" << std::endl;
279 : 57751 : return std::make_tuple(id, a, b);
280 : : }
281 : :
282 : 753 : Node SkolemCache::mkIndexVar(NodeManager* nm, Node t)
283 : : {
284 : 753 : TypeNode intType = nm->integerType();
285 : 753 : BoundVarManager* bvm = nm->getBoundVarManager();
286 : : // Note that proof rules may depend on the name of this variable.
287 : 1506 : return bvm->mkBoundVar<IndexVarAttribute>(t, "@var.str_index", intType);
288 : : }
289 : :
290 : 280 : Node SkolemCache::mkLengthVar(NodeManager* nm, Node t)
291 : : {
292 : 280 : TypeNode intType = nm->integerType();
293 : 280 : BoundVarManager* bvm = nm->getBoundVarManager();
294 : 560 : return bvm->mkBoundVar<LengthVarAttribute>(t, "@var.str_length", intType);
295 : : }
296 : :
297 : 1424 : Node SkolemCache::mkSkolemFun(NodeManager* nm, SkolemId id, Node a, Node b)
298 : : {
299 : 2848 : std::vector<Node> cacheVals = getSkolemCacheVals(a, b);
300 : 1424 : SkolemManager* sm = nm->getSkolemManager();
301 : 1424 : Node k = sm->mkSkolemFunction(id, cacheVals);
302 : 1424 : d_allSkolems.insert(k);
303 : 2848 : return k;
304 : : }
305 : :
306 : 1424 : std::vector<Node> SkolemCache::getSkolemCacheVals(const Node& a,
307 : : const Node& b) const
308 : : {
309 : 1424 : std::vector<Node> cacheVals;
310 [ + + ]: 4272 : for (size_t i = 0; i < 2; i++)
311 : : {
312 [ + + ]: 5696 : Node n = i == 0 ? a : b;
313 [ + + ]: 2848 : if (!n.isNull())
314 : : {
315 [ + + ][ + + ]: 2373 : n = d_rr != nullptr ? d_rr->rewrite(n) : n;
[ - - ]
316 : 2373 : cacheVals.push_back(n);
317 : : }
318 : : }
319 : 1424 : return cacheVals;
320 : : }
321 : :
322 : : } // namespace strings
323 : : } // namespace theory
324 : : } // namespace cvc5::internal
|
