GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sets/theory_sets_type_rules.h Lines: 159 206 77.2 %
Date: 2021-03-23 Branches: 291 1112 26.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_sets_type_rules.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Kshitij Bansal, Mudathir Mohamed
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 Sets theory type rules.
13
 **
14
 ** Sets theory type rules.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H
20
#define CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H
21
22
#include <climits>
23
24
#include "theory/sets/normal_form.h"
25
26
namespace CVC4 {
27
namespace theory {
28
namespace sets {
29
30
struct SetsBinaryOperatorTypeRule
31
{
32
7136
  inline static TypeNode computeType(NodeManager* nodeManager,
33
                                     TNode n,
34
                                     bool check)
35
  {
36
7136
    Assert(n.getKind() == kind::UNION || n.getKind() == kind::INTERSECTION
37
           || n.getKind() == kind::SETMINUS);
38
7136
    TypeNode setType = n[0].getType(check);
39
7136
    if (check)
40
    {
41
7136
      if (!setType.isSet())
42
      {
43
        throw TypeCheckingExceptionPrivate(
44
            n, "operator expects a set, first argument is not");
45
      }
46
14272
      TypeNode secondSetType = n[1].getType(check);
47
7136
      if (secondSetType != setType)
48
      {
49
4
        std::stringstream ss;
50
2
        ss << "Operator " << n.getKind()
51
2
           << " expects two sets of the same type. Found types '" << setType
52
2
           << "' and '" << secondSetType << "'.";
53
2
        throw TypeCheckingExceptionPrivate(n, ss.str());
54
      }
55
    }
56
7134
    return setType;
57
  }
58
59
4287
  inline static bool computeIsConst(NodeManager* nodeManager, TNode n)
60
  {
61
    // only UNION has a const rule in kinds.
62
    // INTERSECTION and SETMINUS are not used in the canonical representation of
63
    // sets and therefore they do not have const rules in kinds
64
4287
    Assert(n.getKind() == kind::UNION);
65
4287
    return NormalForm::checkNormalConstant(n);
66
  }
67
}; /* struct SetsBinaryOperatorTypeRule */
68
69
struct SubsetTypeRule {
70
370
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
71
  {
72
370
    Assert(n.getKind() == kind::SUBSET);
73
740
    TypeNode setType = n[0].getType(check);
74
370
    if( check ) {
75
370
      if(!setType.isSet()) {
76
        throw TypeCheckingExceptionPrivate(n, "set subset operating on non-set");
77
      }
78
740
      TypeNode secondSetType = n[1].getType(check);
79
370
      if(secondSetType != setType) {
80
        if( !setType.isComparableTo( secondSetType ) ){
81
          throw TypeCheckingExceptionPrivate(n, "set subset operating on sets of different types");
82
        }
83
      }
84
    }
85
740
    return nodeManager->booleanType();
86
  }
87
};/* struct SetSubsetTypeRule */
88
89
struct MemberTypeRule
90
{
91
23843
  inline static TypeNode computeType(NodeManager* nodeManager,
92
                                     TNode n,
93
                                     bool check)
94
  {
95
23843
    Assert(n.getKind() == kind::MEMBER);
96
47686
    TypeNode setType = n[1].getType(check);
97
23843
    if (check)
98
    {
99
23843
      if (!setType.isSet())
100
      {
101
        throw TypeCheckingExceptionPrivate(
102
            n, "checking for membership in a non-set");
103
      }
104
47686
      TypeNode elementType = n[0].getType(check);
105
      // e.g. (member 1 (singleton 1.0)) is true whereas
106
      // (member 1.0 (singleton 1)) throws a typing error
107
23843
      if (!elementType.isSubtypeOf(setType.getSetElementType()))
108
      {
109
        std::stringstream ss;
110
        ss << "member operating on sets of different types:\n"
111
           << "child type:  " << elementType << "\n"
112
           << "not subtype: " << setType.getSetElementType() << "\n"
113
           << "in term : " << n;
114
        throw TypeCheckingExceptionPrivate(n, ss.str());
115
      }
116
    }
117
47686
    return nodeManager->booleanType();
118
  }
119
}; /* struct MemberTypeRule */
120
121
struct SingletonTypeRule
122
{
123
3784
  inline static TypeNode computeType(NodeManager* nodeManager,
124
                                     TNode n,
125
                                     bool check)
126
  {
127
3784
    Assert(n.getKind() == kind::SINGLETON && n.hasOperator()
128
           && n.getOperator().getKind() == kind::SINGLETON_OP);
129
130
7568
    SingletonOp op = n.getOperator().getConst<SingletonOp>();
131
7568
    TypeNode type1 = op.getType();
132
3784
    if (check)
133
    {
134
7568
      TypeNode type2 = n[0].getType(check);
135
7568
      TypeNode leastCommonType = TypeNode::leastCommonTypeNode(type1, type2);
136
      // the type of the element should be a subtype of the type of the operator
137
      // e.g. (singleton (singleton_op Real) 1) where 1 is an Int
138
3784
      if (leastCommonType.isNull() || leastCommonType != type1)
139
      {
140
        std::stringstream ss;
141
        ss << "The type '" << type2 << "' of the element is not a subtype of '"
142
           << type1 << "' in term : " << n;
143
        throw TypeCheckingExceptionPrivate(n, ss.str());
144
      }
145
    }
146
7568
    return nodeManager->mkSetType(type1);
147
  }
148
149
3177
  inline static bool computeIsConst(NodeManager* nodeManager, TNode n)
150
  {
151
3177
    Assert(n.getKind() == kind::SINGLETON);
152
3177
    return n[0].isConst();
153
  }
154
}; /* struct SingletonTypeRule */
155
156
struct EmptySetTypeRule {
157
1695
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
158
  {
159
1695
    Assert(n.getKind() == kind::EMPTYSET);
160
3390
    EmptySet emptySet = n.getConst<EmptySet>();
161
3390
    return emptySet.getType();
162
  }
163
};/* struct EmptySetTypeRule */
164
165
struct CardTypeRule {
166
2791
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
167
  {
168
2791
    Assert(n.getKind() == kind::CARD);
169
5582
    TypeNode setType = n[0].getType(check);
170
2791
    if( check ) {
171
2791
      if(!setType.isSet()) {
172
        throw TypeCheckingExceptionPrivate(n, "cardinality operates on a set, non-set object found");
173
      }
174
    }
175
5582
    return nodeManager->integerType();
176
  }
177
};/* struct CardTypeRule */
178
179
struct ComplementTypeRule {
180
23
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
181
  {
182
23
    Assert(n.getKind() == kind::COMPLEMENT);
183
23
    TypeNode setType = n[0].getType(check);
184
23
    if( check ) {
185
23
      if(!setType.isSet()) {
186
        throw TypeCheckingExceptionPrivate(n, "COMPLEMENT operates on a set, non-set object found");
187
      }
188
    }
189
23
    return setType;
190
  }
191
};/* struct ComplementTypeRule */
192
193
struct UniverseSetTypeRule {
194
134
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
195
  {
196
134
    Assert(n.getKind() == kind::UNIVERSE_SET);
197
    // for nullary operators, we only computeType for check=true, since they are given TypeAttr() on creation
198
134
    Assert(check);
199
134
    TypeNode setType = n.getType();
200
134
    if(!setType.isSet()) {
201
      throw TypeCheckingExceptionPrivate(n, "Non-set type found for universe set");
202
    }
203
134
    return setType;
204
  }
205
};/* struct ComplementTypeRule */
206
207
struct ComprehensionTypeRule
208
{
209
52
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
210
  {
211
52
    Assert(n.getKind() == kind::COMPREHENSION);
212
52
    if (check)
213
    {
214
52
      if (n[0].getType(check) != nodeManager->boundVarListType())
215
      {
216
        throw TypeCheckingExceptionPrivate(
217
            n, "first argument of set comprehension is not bound var list");
218
      }
219
52
      if (n[1].getType(check) != nodeManager->booleanType())
220
      {
221
        throw TypeCheckingExceptionPrivate(
222
            n, "body of set comprehension is not boolean");
223
      }
224
    }
225
52
    return nodeManager->mkSetType(n[2].getType(check));
226
  }
227
}; /* struct ComprehensionTypeRule */
228
229
struct ChooseTypeRule
230
{
231
16
  inline static TypeNode computeType(NodeManager* nodeManager,
232
                                     TNode n,
233
                                     bool check)
234
  {
235
16
    Assert(n.getKind() == kind::CHOOSE);
236
32
    TypeNode setType = n[0].getType(check);
237
16
    if (check)
238
    {
239
16
      if (!setType.isSet())
240
      {
241
        throw TypeCheckingExceptionPrivate(
242
            n, "CHOOSE operator expects a set, a non-set is found");
243
      }
244
    }
245
32
    return setType.getSetElementType();
246
  }
247
}; /* struct ChooseTypeRule */
248
249
struct IsSingletonTypeRule
250
{
251
18
  inline static TypeNode computeType(NodeManager* nodeManager,
252
                                     TNode n,
253
                                     bool check)
254
  {
255
18
    Assert(n.getKind() == kind::IS_SINGLETON);
256
36
    TypeNode setType = n[0].getType(check);
257
18
    if (check)
258
    {
259
18
      if (!setType.isSet())
260
      {
261
        throw TypeCheckingExceptionPrivate(
262
            n, "IS_SINGLETON operator expects a set, a non-set is found");
263
      }
264
    }
265
36
    return nodeManager->booleanType();
266
  }
267
}; /* struct IsSingletonTypeRule */
268
269
struct InsertTypeRule {
270
31
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
271
  {
272
31
    Assert(n.getKind() == kind::INSERT);
273
31
    size_t numChildren = n.getNumChildren();
274
31
    Assert(numChildren >= 2);
275
31
    TypeNode setType = n[numChildren-1].getType(check);
276
31
    if( check ) {
277
31
      if(!setType.isSet()) {
278
        throw TypeCheckingExceptionPrivate(n, "inserting into a non-set");
279
      }
280
106
      for(size_t i = 0; i < numChildren-1; ++i) {
281
150
        TypeNode elementType = n[i].getType(check);
282
75
        if(elementType != setType.getSetElementType()) {
283
          throw TypeCheckingExceptionPrivate
284
            (n, "type of element should be same as element type of set being inserted into");
285
        }
286
      }
287
    }
288
31
    return setType;
289
  }
290
};/* struct InsertTypeRule */
291
292
struct RelBinaryOperatorTypeRule {
293
373
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
294
  {
295
373
    Assert(n.getKind() == kind::PRODUCT || n.getKind() == kind::JOIN);
296
297
746
    TypeNode firstRelType = n[0].getType(check);
298
746
    TypeNode secondRelType = n[1].getType(check);
299
373
    TypeNode resultType = firstRelType;
300
301
373
    if(!firstRelType.isSet() || !secondRelType.isSet()) {
302
      throw TypeCheckingExceptionPrivate(n, " Relational operator operates on non-sets");
303
    }
304
373
    if(!firstRelType[0].isTuple() || !secondRelType[0].isTuple()) {
305
      throw TypeCheckingExceptionPrivate(n, " Relational operator operates on non-relations (sets of tuples)");
306
    }
307
308
746
    std::vector<TypeNode> newTupleTypes;
309
746
    std::vector<TypeNode> firstTupleTypes = firstRelType[0].getTupleTypes();
310
746
    std::vector<TypeNode> secondTupleTypes = secondRelType[0].getTupleTypes();
311
312
    // JOIN is not allowed to apply on two unary sets
313
373
    if( n.getKind() == kind::JOIN ) {
314
326
      if((firstTupleTypes.size() == 1) && (secondTupleTypes.size() == 1)) {
315
        throw TypeCheckingExceptionPrivate(n, " Join operates on two unary relations");
316
326
      } else if(firstTupleTypes.back() != secondTupleTypes.front()) {
317
        throw TypeCheckingExceptionPrivate(n, " Join operates on two non-joinable relations");
318
      }
319
326
      newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end()-1);
320
326
      newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin()+1, secondTupleTypes.end());
321
47
    }else if( n.getKind() == kind::PRODUCT ) {
322
47
      newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end());
323
47
      newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin(), secondTupleTypes.end());
324
    }
325
373
    resultType = nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes));
326
327
746
    return resultType;
328
  }
329
};/* struct RelBinaryOperatorTypeRule */
330
331
struct RelTransposeTypeRule {
332
119
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
333
  {
334
119
    Assert(n.getKind() == kind::TRANSPOSE);
335
238
    TypeNode setType = n[0].getType(check);
336
119
    if(check && (!setType.isSet() || !setType.getSetElementType().isTuple())) {
337
        throw TypeCheckingExceptionPrivate(n, "relation transpose operates on non-relation");
338
    }
339
238
    std::vector<TypeNode> tupleTypes = setType[0].getTupleTypes();
340
119
    std::reverse(tupleTypes.begin(), tupleTypes.end());
341
238
    return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes));
342
  }
343
};/* struct RelTransposeTypeRule */
344
345
struct RelTransClosureTypeRule {
346
45
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
347
  {
348
45
    Assert(n.getKind() == kind::TCLOSURE);
349
45
    TypeNode setType = n[0].getType(check);
350
45
    if(check) {
351
45
      if(!setType.isSet() || !setType.getSetElementType().isTuple()) {
352
        throw TypeCheckingExceptionPrivate(n, " transitive closure operates on non-relation");
353
      }
354
90
      std::vector<TypeNode> tupleTypes = setType[0].getTupleTypes();
355
45
      if(tupleTypes.size() != 2) {
356
        throw TypeCheckingExceptionPrivate(n, " transitive closure operates on non-binary relations");
357
      }
358
45
      if(tupleTypes[0] != tupleTypes[1]) {
359
        throw TypeCheckingExceptionPrivate(n, " transitive closure operates on non-homogeneous binary relations");
360
      }
361
    }
362
45
    return setType;
363
  }
364
};/* struct RelTransClosureTypeRule */
365
366
struct JoinImageTypeRule {
367
38
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
368
  {
369
38
    Assert(n.getKind() == kind::JOIN_IMAGE);
370
371
76
    TypeNode firstRelType = n[0].getType(check);
372
373
38
    if(!firstRelType.isSet()) {
374
      throw TypeCheckingExceptionPrivate(n, " JoinImage operator operates on non-relations");
375
    }
376
38
    if(!firstRelType[0].isTuple()) {
377
      throw TypeCheckingExceptionPrivate(n, " JoinImage operator operates on non-relations (sets of tuples)");
378
    }
379
380
76
    std::vector<TypeNode> tupleTypes = firstRelType[0].getTupleTypes();
381
38
    if(tupleTypes.size() != 2) {
382
      throw TypeCheckingExceptionPrivate(n, " JoinImage operates on a non-binary relation");
383
    }
384
76
    TypeNode valType = n[1].getType(check);
385
38
    if (valType != nodeManager->integerType()) {
386
      throw TypeCheckingExceptionPrivate(
387
          n, " JoinImage cardinality constraint must be integer");
388
    }
389
38
    if (n[1].getKind() != kind::CONST_RATIONAL) {
390
      throw TypeCheckingExceptionPrivate(
391
          n, " JoinImage cardinality constraint must be a constant");
392
    }
393
76
    CVC4::Rational r(INT_MAX);
394
38
    if (n[1].getConst<Rational>() > r) {
395
      throw TypeCheckingExceptionPrivate(
396
          n, " JoinImage Exceeded INT_MAX in cardinality constraint");
397
    }
398
38
    if (n[1].getConst<Rational>().getNumerator().getSignedInt() < 0) {
399
      throw TypeCheckingExceptionPrivate(
400
          n, " JoinImage cardinality constraint must be non-negative");
401
    }
402
76
    std::vector<TypeNode> newTupleTypes;
403
38
    newTupleTypes.push_back(tupleTypes[0]);
404
76
    return nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes));
405
  }
406
};/* struct JoinImageTypeRule */
407
408
struct RelIdenTypeRule {
409
9
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
410
  {
411
9
    Assert(n.getKind() == kind::IDEN);
412
18
    TypeNode setType = n[0].getType(check);
413
9
    if(check) {
414
9
      if(!setType.isSet() && !setType.getSetElementType().isTuple()) {
415
        throw TypeCheckingExceptionPrivate(n, " Identity operates on non-relation");
416
      }
417
9
      if(setType[0].getTupleTypes().size() != 1) {
418
        throw TypeCheckingExceptionPrivate(n, " Identity operates on non-unary relations");
419
      }
420
    }
421
18
    std::vector<TypeNode> tupleTypes = setType[0].getTupleTypes();
422
9
    tupleTypes.push_back(tupleTypes[0]);
423
18
    return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes));
424
  }
425
};/* struct RelIdenTypeRule */
426
427
struct SetsProperties {
428
  inline static Cardinality computeCardinality(TypeNode type) {
429
    Assert(type.getKind() == kind::SET_TYPE);
430
    Cardinality elementCard = 2;
431
    elementCard ^= type[0].getCardinality();
432
    return elementCard;
433
  }
434
435
  inline static bool isWellFounded(TypeNode type) {
436
    return type[0].isWellFounded();
437
  }
438
439
8
  inline static Node mkGroundTerm(TypeNode type) {
440
8
    Assert(type.isSet());
441
8
    return NodeManager::currentNM()->mkConst(EmptySet(type));
442
  }
443
};/* struct SetsProperties */
444
445
}/* CVC4::theory::sets namespace */
446
}/* CVC4::theory namespace */
447
}/* CVC4 namespace */
448
449
#endif /* CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H */