GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/theory_strings_type_rules.h Lines: 103 150 68.7 %
Date: 2021-03-22 Branches: 134 516 26.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_strings_type_rules.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tianyi Liang, 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 Typing rules for the theory of strings and regexps
13
 **
14
 ** Typing rules for the theory of strings and regexps
15
 **/
16
17
#include "cvc4_private.h"
18
#include "options/strings_options.h"
19
20
#ifndef CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
21
#define CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
22
23
#include "expr/sequence.h"
24
25
namespace CVC4 {
26
namespace theory {
27
namespace strings {
28
29
class StringConcatTypeRule
30
{
31
 public:
32
36439
  inline static TypeNode computeType(NodeManager* nodeManager,
33
                                     TNode n,
34
                                     bool check)
35
  {
36
36439
    TypeNode tret;
37
145426
    for (const Node& nc : n)
38
    {
39
217974
      TypeNode t = nc.getType(check);
40
108987
      if (tret.isNull())
41
      {
42
36439
        tret = t;
43
36439
        if (check)
44
        {
45
36439
          if (!t.isStringLike())
46
          {
47
            throw TypeCheckingExceptionPrivate(
48
                n, "expecting string-like terms in concat");
49
          }
50
        }
51
        else
52
        {
53
          break;
54
        }
55
      }
56
72548
      else if (t != tret)
57
      {
58
        throw TypeCheckingExceptionPrivate(
59
            n, "expecting all children to have the same type in concat");
60
      }
61
    }
62
36439
    return tret;
63
  }
64
};
65
66
class StringSubstrTypeRule
67
{
68
 public:
69
33333
  inline static TypeNode computeType(NodeManager* nodeManager,
70
                                     TNode n,
71
                                     bool check)
72
  {
73
33333
    TypeNode t = n[0].getType(check);
74
33333
    if (check)
75
    {
76
33333
      if (!t.isStringLike())
77
      {
78
        throw TypeCheckingExceptionPrivate(
79
            n, "expecting a string-like term in substr");
80
      }
81
66666
      TypeNode t2 = n[1].getType(check);
82
33333
      if (!t2.isInteger())
83
      {
84
        throw TypeCheckingExceptionPrivate(
85
            n, "expecting an integer start term in substr");
86
      }
87
33333
      t2 = n[2].getType(check);
88
33333
      if (!t2.isInteger())
89
      {
90
        throw TypeCheckingExceptionPrivate(
91
            n, "expecting an integer length term in substr");
92
      }
93
    }
94
33333
    return t;
95
  }
96
};
97
98
class StringUpdateTypeRule
99
{
100
 public:
101
137
  inline static TypeNode computeType(NodeManager* nodeManager,
102
                                     TNode n,
103
                                     bool check)
104
  {
105
137
    TypeNode t = n[0].getType(check);
106
137
    if (check)
107
    {
108
137
      if (!t.isStringLike())
109
      {
110
        throw TypeCheckingExceptionPrivate(
111
            n, "expecting a string-like term in update");
112
      }
113
274
      TypeNode t2 = n[1].getType(check);
114
137
      if (!t2.isInteger())
115
      {
116
        throw TypeCheckingExceptionPrivate(
117
            n, "expecting an integer start term in update");
118
      }
119
137
      t2 = n[2].getType(check);
120
137
      if (!t2.isStringLike())
121
      {
122
        throw TypeCheckingExceptionPrivate(
123
            n, "expecting an string-like replace term in update");
124
      }
125
    }
126
137
    return t;
127
  }
128
};
129
130
class StringAtTypeRule
131
{
132
 public:
133
134
  inline static TypeNode computeType(NodeManager* nodeManager,
134
                                     TNode n,
135
                                     bool check)
136
  {
137
134
    TypeNode t = n[0].getType(check);
138
134
    if (check)
139
    {
140
134
      if (!t.isStringLike())
141
      {
142
        throw TypeCheckingExceptionPrivate(
143
            n, "expecting a string-like term in str.at");
144
      }
145
268
      TypeNode t2 = n[1].getType(check);
146
134
      if (!t2.isInteger())
147
      {
148
        throw TypeCheckingExceptionPrivate(
149
            n, "expecting an integer start term in str.at");
150
      }
151
    }
152
134
    return t;
153
  }
154
};
155
156
class StringIndexOfTypeRule
157
{
158
 public:
159
2708
  inline static TypeNode computeType(NodeManager* nodeManager,
160
                                     TNode n,
161
                                     bool check)
162
  {
163
2708
    if (check)
164
    {
165
5416
      TypeNode t = n[0].getType(check);
166
2708
      if (!t.isStringLike())
167
      {
168
        throw TypeCheckingExceptionPrivate(
169
            n, "expecting a string-like term in indexof");
170
      }
171
5416
      TypeNode t2 = n[1].getType(check);
172
2708
      if (t != t2)
173
      {
174
        throw TypeCheckingExceptionPrivate(
175
            n,
176
            "expecting a term in second argument of indexof that is the same "
177
            "type as the first argument");
178
      }
179
2708
      t = n[2].getType(check);
180
2708
      if (!t.isInteger())
181
      {
182
        throw TypeCheckingExceptionPrivate(
183
            n, "expecting an integer term in third argument of indexof");
184
      }
185
    }
186
2708
    return nodeManager->integerType();
187
  }
188
};
189
190
class StringReplaceTypeRule
191
{
192
 public:
193
2223
  inline static TypeNode computeType(NodeManager* nodeManager,
194
                                     TNode n,
195
                                     bool check)
196
  {
197
2223
    TypeNode t = n[0].getType(check);
198
2223
    if (check)
199
    {
200
2223
      if (!t.isStringLike())
201
      {
202
        throw TypeCheckingExceptionPrivate(
203
            n, "expecting a string-like term in replace");
204
      }
205
4446
      TypeNode t2 = n[1].getType(check);
206
2223
      if (t != t2)
207
      {
208
        throw TypeCheckingExceptionPrivate(
209
            n,
210
            "expecting a term in second argument of replace that is the same "
211
            "type as the first argument");
212
      }
213
2223
      t2 = n[2].getType(check);
214
2223
      if (t != t2)
215
      {
216
        throw TypeCheckingExceptionPrivate(
217
            n,
218
            "expecting a term in third argument of replace that is the same "
219
            "type as the first argument");
220
      }
221
    }
222
2223
    return t;
223
  }
224
};
225
226
class StringStrToBoolTypeRule
227
{
228
 public:
229
161
  inline static TypeNode computeType(NodeManager* nodeManager,
230
                                     TNode n,
231
                                     bool check)
232
  {
233
161
    if (check)
234
    {
235
322
      TypeNode t = n[0].getType(check);
236
161
      if (!t.isStringLike())
237
      {
238
        std::stringstream ss;
239
        ss << "expecting a string-like term in argument of " << n.getKind();
240
        throw TypeCheckingExceptionPrivate(n, ss.str());
241
      }
242
    }
243
161
    return nodeManager->booleanType();
244
  }
245
};
246
247
class StringStrToIntTypeRule
248
{
249
 public:
250
91203
  inline static TypeNode computeType(NodeManager* nodeManager,
251
                                     TNode n,
252
                                     bool check)
253
  {
254
91203
    if (check)
255
    {
256
182406
      TypeNode t = n[0].getType(check);
257
91203
      if (!t.isStringLike())
258
      {
259
        std::stringstream ss;
260
        ss << "expecting a string-like term in argument of " << n.getKind();
261
        throw TypeCheckingExceptionPrivate(n, ss.str());
262
      }
263
    }
264
91203
    return nodeManager->integerType();
265
  }
266
};
267
268
class StringStrToStrTypeRule
269
{
270
 public:
271
158
  inline static TypeNode computeType(NodeManager* nodeManager,
272
                                     TNode n,
273
                                     bool check)
274
  {
275
158
    TypeNode t = n[0].getType(check);
276
158
    if (check)
277
    {
278
158
      if (!t.isStringLike())
279
      {
280
        std::stringstream ss;
281
        ss << "expecting a string term in argument of " << n.getKind();
282
        throw TypeCheckingExceptionPrivate(n, ss.str());
283
      }
284
    }
285
158
    return t;
286
  }
287
};
288
289
class StringRelationTypeRule
290
{
291
 public:
292
90138
  inline static TypeNode computeType(NodeManager* nodeManager,
293
                                     TNode n,
294
                                     bool check)
295
  {
296
90138
    if (check)
297
    {
298
180276
      TypeNode t = n[0].getType(check);
299
90138
      if (!t.isStringLike())
300
      {
301
        throw TypeCheckingExceptionPrivate(
302
            n, "expecting a string-like term in relation");
303
      }
304
180276
      TypeNode t2 = n[1].getType(check);
305
90138
      if (t != t2)
306
      {
307
        throw TypeCheckingExceptionPrivate(
308
            n, "expecting two terms of the same string-like type in relation");
309
      }
310
    }
311
90138
    return nodeManager->booleanType();
312
  }
313
};
314
315
class RegExpRangeTypeRule {
316
public:
317
158
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
318
  {
319
158
    if( check ) {
320
158
      TNode::iterator it = n.begin();
321
      unsigned ch[2];
322
323
474
      for(int i=0; i<2; ++i) {
324
632
        TypeNode t = (*it).getType(check);
325
316
        if (!t.isString())  // string-only
326
        {
327
          throw TypeCheckingExceptionPrivate(n, "expecting a string term in regexp range");
328
        }
329
316
        if (!(*it).isConst())
330
        {
331
          throw TypeCheckingExceptionPrivate(n, "expecting a constant string term in regexp range");
332
        }
333
316
        if( (*it).getConst<String>().size() != 1 ) {
334
          throw TypeCheckingExceptionPrivate(n, "expecting a single constant string term in regexp range");
335
        }
336
316
        unsigned ci = (*it).getConst<String>().front();
337
316
        ch[i] = ci;
338
316
        ++it;
339
      }
340
158
      if(ch[0] > ch[1]) {
341
        throw TypeCheckingExceptionPrivate(n, "expecting the first constant is less or equal to the second one in regexp range");
342
      }
343
158
      unsigned maxCh = options::stdPrintASCII() ? 127 : 255;
344
158
      if (ch[1] > maxCh)
345
      {
346
        std::stringstream ss;
347
        ss << "expecting characters whose code point is less than or equal to "
348
           << maxCh;
349
        throw TypeCheckingExceptionPrivate(n, ss.str());
350
      }
351
    }
352
158
    return nodeManager->regExpType();
353
  }
354
};
355
356
class ConstSequenceTypeRule
357
{
358
 public:
359
335
  static TypeNode computeType(NodeManager* nodeManager,
360
                                     TNode n,
361
                                     bool check)
362
  {
363
335
    Assert(n.getKind() == kind::CONST_SEQUENCE);
364
335
    return nodeManager->mkSequenceType(n.getConst<Sequence>().getType());
365
  }
366
};
367
368
class SeqUnitTypeRule
369
{
370
 public:
371
190
  static TypeNode computeType(NodeManager* nodeManager,
372
                                     TNode n,
373
                                     bool check)
374
  {
375
190
    return nodeManager->mkSequenceType(n[0].getType(check));
376
  }
377
};
378
379
class SeqNthTypeRule
380
{
381
 public:
382
186
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
383
  {
384
372
    TypeNode t = n[0].getType(check);
385
186
    TypeNode t1 = t.getSequenceElementType();
386
186
    if (check)
387
    {
388
186
      if (!t.isSequence())
389
      {
390
        throw TypeCheckingExceptionPrivate(n, "expecting a sequence in nth");
391
      }
392
372
      TypeNode t2 = n[1].getType(check);
393
186
      if (!t2.isInteger())
394
      {
395
        throw TypeCheckingExceptionPrivate(
396
            n, "expecting an integer start term in nth");
397
      }
398
    }
399
372
    return t1;
400
  }
401
};
402
403
/** Properties of the sequence type */
404
struct SequenceProperties
405
{
406
  static Cardinality computeCardinality(TypeNode type)
407
  {
408
    Assert(type.getKind() == kind::SEQUENCE_TYPE);
409
    return Cardinality::INTEGERS;
410
  }
411
  /** A sequence is well-founded if its element type is */
412
  static bool isWellFounded(TypeNode type)
413
  {
414
    return type[0].isWellFounded();
415
  }
416
  /** Make ground term for sequence type (return the empty sequence) */
417
  static Node mkGroundTerm(TypeNode type)
418
  {
419
    Assert(type.isSequence());
420
    // empty sequence
421
    std::vector<Node> seq;
422
    return NodeManager::currentNM()->mkConst(
423
        Sequence(type.getSequenceElementType(), seq));
424
  }
425
}; /* struct SequenceProperties */
426
427
}/* CVC4::theory::strings namespace */
428
}/* CVC4::theory namespace */
429
}/* CVC4 namespace */
430
431
#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H */