GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/skolem_cache.cpp Lines: 118 130 90.8 %
Date: 2021-03-23 Branches: 286 577 49.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file skolem_cache.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, Yoni Zohar
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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.\endverbatim
11
 **
12
 ** \brief Implementation of a cache of skolems for theory of strings.
13
 **/
14
15
#include "theory/strings/skolem_cache.h"
16
17
#include "expr/attribute.h"
18
#include "expr/bound_var_manager.h"
19
#include "expr/skolem_manager.h"
20
#include "theory/rewriter.h"
21
#include "theory/strings/arith_entail.h"
22
#include "theory/strings/theory_strings_utils.h"
23
#include "theory/strings/word.h"
24
#include "util/rational.h"
25
26
using namespace CVC4::kind;
27
28
namespace CVC4 {
29
namespace theory {
30
namespace strings {
31
32
/**
33
 * A bound variable corresponding to the universally quantified integer
34
 * variable used to range over the valid positions in a string, used
35
 * for axiomatizing the behavior of some term.
36
 */
37
struct IndexVarAttributeId
38
{
39
};
40
typedef expr::Attribute<IndexVarAttributeId, Node> IndexVarAttribute;
41
42
9784
SkolemCache::SkolemCache(bool useOpts) : d_useOpts(useOpts)
43
{
44
9784
  NodeManager* nm = NodeManager::currentNM();
45
9784
  d_strType = nm->stringType();
46
9784
  d_zero = nm->mkConst(Rational(0));
47
9784
}
48
49
25448
Node SkolemCache::mkSkolemCached(Node a, Node b, SkolemId id, const char* c)
50
{
51
25448
  return mkTypedSkolemCached(d_strType, a, b, id, c);
52
}
53
54
13026
Node SkolemCache::mkSkolemCached(Node a, SkolemId id, const char* c)
55
{
56
13026
  return mkSkolemCached(a, Node::null(), id, c);
57
}
58
59
25681
Node SkolemCache::mkTypedSkolemCached(
60
    TypeNode tn, Node a, Node b, SkolemId id, const char* c)
61
{
62
51362
  Trace("skolem-cache") << "mkTypedSkolemCached start: (" << id << ", " << a
63
25681
                        << ", " << b << ")" << std::endl;
64
25681
  SkolemId idOrig = id;
65
  // do not rewrite beforehand if we are not using optimizations, this is so
66
  // that the proof checker does not depend on the rewriter.
67
25681
  if (d_useOpts)
68
  {
69
24086
    a = a.isNull() ? a : Rewriter::rewrite(a);
70
24086
    b = b.isNull() ? b : Rewriter::rewrite(b);
71
  }
72
25681
  std::tie(id, a, b) = normalizeStringSkolem(id, a, b);
73
74
  // optimization: if we aren't asking for the purification skolem for constant
75
  // a, and the skolem is equivalent to a, then we just return a.
76
25681
  if (d_useOpts && idOrig != SK_PURIFY && id == SK_PURIFY && a.isConst())
77
  {
78
1082
    Trace("skolem-cache") << "...optimization: return constant " << a
79
541
                          << std::endl;
80
541
    return a;
81
  }
82
83
25140
  std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id);
84
25140
  if (it != d_skolemCache[a][b].end())
85
  {
86
12617
    Trace("skolem-cache") << "...return existing " << it->second << std::endl;
87
    // already cached
88
12617
    return it->second;
89
  }
90
91
12523
  NodeManager* nm = NodeManager::currentNM();
92
12523
  SkolemManager* sm = nm->getSkolemManager();
93
25046
  Node sk;
94
12523
  switch (id)
95
  {
96
    // exists k. k = a
97
12422
    case SK_PURIFY:
98
12422
      sk = sm->mkPurifySkolem(a, c, "string purify skolem");
99
12422
      break;
100
    // these are eliminated by normalizeStringSkolem
101
    case SK_ID_V_SPT:
102
    case SK_ID_V_SPT_REV:
103
    case SK_ID_VC_SPT:
104
    case SK_ID_VC_SPT_REV:
105
    case SK_FIRST_CTN_POST:
106
    case SK_ID_C_SPT:
107
    case SK_ID_C_SPT_REV:
108
    case SK_ID_DC_SPT:
109
    case SK_ID_DC_SPT_REM:
110
    case SK_ID_DEQ_X:
111
    case SK_ID_DEQ_Y:
112
    case SK_FIRST_CTN_PRE:
113
    case SK_PREFIX:
114
    case SK_SUFFIX_REM:
115
      Unhandled() << "Expected to eliminate Skolem ID " << id << std::endl;
116
      break;
117
101
    case SK_NUM_OCCUR:
118
    case SK_OCCUR_INDEX:
119
    default:
120
    {
121
101
      Notice() << "Don't know how to handle Skolem ID " << id << std::endl;
122
202
      Node v = nm->mkBoundVar(tn);
123
202
      Node cond = nm->mkConst(true);
124
202
      sk = sm->mkSkolem(v, cond, c, "string skolem");
125
    }
126
101
    break;
127
  }
128
12523
  Trace("skolem-cache") << "...returned " << sk << std::endl;
129
12523
  d_allSkolems.insert(sk);
130
12523
  d_skolemCache[a][b][id] = sk;
131
12523
  return sk;
132
}
133
158
Node SkolemCache::mkTypedSkolemCached(TypeNode tn,
134
                                      Node a,
135
                                      SkolemId id,
136
                                      const char* c)
137
{
138
158
  return mkTypedSkolemCached(tn, a, Node::null(), id, c);
139
}
140
141
31
Node SkolemCache::mkSkolemSeqNth(TypeNode seqType, const char* c)
142
{
143
31
  Assert(seqType.isSequence());
144
31
  NodeManager* nm = NodeManager::currentNM();
145
62
  std::vector<TypeNode> argTypes;
146
31
  argTypes.push_back(seqType);
147
31
  argTypes.push_back(nm->integerType());
148
62
  TypeNode elemType = seqType.getSequenceElementType();
149
62
  TypeNode ufType = nm->mkFunctionType(argTypes, elemType);
150
  return mkTypedSkolemCached(
151
62
      ufType, Node::null(), Node::null(), SkolemCache::SK_NTH, c);
152
}
153
154
1110
Node SkolemCache::mkSkolem(const char* c)
155
{
156
  // TODO: eliminate this
157
1110
  Node n = NodeManager::currentNM()->mkSkolem(c, d_strType, "string skolem");
158
1110
  d_allSkolems.insert(n);
159
1110
  return n;
160
}
161
162
3660
bool SkolemCache::isSkolem(Node n) const
163
{
164
3660
  return d_allSkolems.find(n) != d_allSkolems.end();
165
}
166
167
std::tuple<SkolemCache::SkolemId, Node, Node>
168
25681
SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
169
{
170
171
25681
  NodeManager* nm = NodeManager::currentNM();
172
173
  // eliminate in terms of prefix/suffix_rem
174
25681
  if (id == SK_FIRST_CTN_POST)
175
  {
176
    // SK_FIRST_CTN_POST(x, y) --->
177
    //   SK_SUFFIX_REM(x, (+ (str.len SK_FIRST_CTN_PRE(x, y)) (str.len y)))
178
2191
    id = SK_SUFFIX_REM;
179
4382
    Node pre = mkSkolemCached(a, b, SK_FIRST_CTN_PRE, "pre");
180
6573
    b = nm->mkNode(
181
8764
        PLUS, nm->mkNode(STRING_LENGTH, pre), nm->mkNode(STRING_LENGTH, b));
182
  }
183
23490
  else if (id == SK_ID_V_SPT || id == SK_ID_C_SPT)
184
  {
185
    // SK_ID_*_SPT(x, y) ---> SK_SUFFIX_REM(x, (str.len y))
186
370
    id = SK_SUFFIX_REM;
187
370
    b = nm->mkNode(STRING_LENGTH, b);
188
  }
189
23120
  else if (id == SK_ID_V_SPT_REV || id == SK_ID_C_SPT_REV)
190
  {
191
    // SK_ID_*_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) (str.len y)))
192
450
    id = SK_PREFIX;
193
1800
    b = nm->mkNode(
194
1800
        MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkNode(STRING_LENGTH, b));
195
  }
196
22670
  else if (id == SK_ID_VC_SPT)
197
  {
198
    // SK_ID_VC_SPT(x, y) ---> SK_SUFFIX_REM(x, 1)
199
2166
    id = SK_SUFFIX_REM;
200
2166
    b = nm->mkConst(Rational(1));
201
  }
202
20504
  else if (id == SK_ID_VC_SPT_REV)
203
  {
204
    // SK_ID_VC_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) 1))
205
2541
    id = SK_PREFIX;
206
7623
    b = nm->mkNode(
207
10164
        MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkConst(Rational(1)));
208
  }
209
17963
  else if (id == SK_ID_DC_SPT)
210
  {
211
    // SK_ID_DC_SPT(x, y) ---> SK_PREFIX(x, 1)
212
    id = SK_PREFIX;
213
    b = nm->mkConst(Rational(1));
214
  }
215
17963
  else if (id == SK_ID_DC_SPT_REM)
216
  {
217
    // SK_ID_DC_SPT_REM(x, y) ---> SK_SUFFIX_REM(x, 1)
218
    id = SK_SUFFIX_REM;
219
    b = nm->mkConst(Rational(1));
220
  }
221
17963
  else if (id == SK_ID_DEQ_X)
222
  {
223
    // SK_ID_DEQ_X(x, y) ---> SK_PREFIX(y, (str.len x))
224
    id = SK_PREFIX;
225
    Node aOld = a;
226
    a = b;
227
    b = nm->mkNode(STRING_LENGTH, aOld);
228
  }
229
17963
  else if (id == SK_ID_DEQ_Y)
230
  {
231
    // SK_ID_DEQ_Y(x, y) ---> SK_PREFIX(x, (str.len y))
232
    id = SK_PREFIX;
233
    b = nm->mkNode(STRING_LENGTH, b);
234
  }
235
17963
  else if (id == SK_FIRST_CTN_PRE)
236
  {
237
    // SK_FIRST_CTN_PRE(x,y) ---> SK_PREFIX(x, indexof(x,y,0))
238
4386
    id = SK_PREFIX;
239
4386
    b = nm->mkNode(STRING_STRIDOF, a, b, d_zero);
240
  }
241
242
25681
  if (id == SK_ID_V_UNIFIED_SPT || id == SK_ID_V_UNIFIED_SPT_REV)
243
  {
244
2767
    bool isRev = (id == SK_ID_V_UNIFIED_SPT_REV);
245
5534
    Node la = nm->mkNode(STRING_LENGTH, a);
246
5534
    Node lb = nm->mkNode(STRING_LENGTH, b);
247
4006
    Node ta = isRev ? utils::mkPrefix(a, nm->mkNode(MINUS, la, lb))
248
6773
                    : utils::mkSuffix(a, lb);
249
4006
    Node tb = isRev ? utils::mkPrefix(b, nm->mkNode(MINUS, lb, la))
250
6773
                    : utils::mkSuffix(b, la);
251
2767
    id = SK_PURIFY;
252
    // SK_ID_V_UNIFIED_SPT(x,y) --->
253
    //   ite(len(x) >= len(y), substr(x,0,str.len(y)), substr(y,0,str.len(x))
254
2767
    a = nm->mkNode(ITE, nm->mkNode(GEQ, la, lb), ta, tb);
255
2767
    b = Node::null();
256
  }
257
258
  // now, eliminate prefix/suffix_rem in terms of purify
259
25681
  if (id == SK_PREFIX)
260
  {
261
    // SK_PREFIX(x,y) ---> SK_PURIFY(substr(x,0,y))
262
8482
    id = SK_PURIFY;
263
8482
    a = utils::mkPrefix(a, b);
264
8482
    b = Node::null();
265
  }
266
17199
  else if (id == SK_SUFFIX_REM)
267
  {
268
    // SK_SUFFIX_REM(x,y) ---> SK_PURIFY(substr(x,y,str.len(x)-y))
269
5832
    id = SK_PURIFY;
270
5832
    a = utils::mkSuffix(a, b);
271
5832
    b = Node::null();
272
  }
273
274
25681
  if (d_useOpts)
275
  {
276
24086
    a = a.isNull() ? a : Rewriter::rewrite(a);
277
24086
    b = b.isNull() ? b : Rewriter::rewrite(b);
278
  }
279
51362
  Trace("skolem-cache") << "normalizeStringSkolem end: (" << id << ", " << a
280
25681
                        << ", " << b << ")" << std::endl;
281
25681
  return std::make_tuple(id, a, b);
282
}
283
284
260
Node SkolemCache::mkIndexVar(Node t)
285
{
286
260
  NodeManager* nm = NodeManager::currentNM();
287
520
  TypeNode intType = nm->integerType();
288
260
  BoundVarManager* bvm = nm->getBoundVarManager();
289
520
  return bvm->mkBoundVar<IndexVarAttribute>(t, intType);
290
}
291
292
}  // namespace strings
293
}  // namespace theory
294
26685
}  // namespace CVC4