GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bags/theory_bags_type_rules.h Lines: 91 127 71.7 %
Date: 2021-03-23 Branches: 177 678 26.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_bags_type_rules.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   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 Bags theory type rules.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H
18
#define CVC4__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H
19
20
#include "theory/bags/normal_form.h"
21
22
namespace CVC4 {
23
namespace theory {
24
namespace bags {
25
26
struct BinaryOperatorTypeRule
27
{
28
316
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
29
  {
30
316
    Assert(n.getKind() == kind::UNION_MAX || n.getKind() == kind::UNION_DISJOINT
31
           || n.getKind() == kind::INTERSECTION_MIN
32
           || n.getKind() == kind::DIFFERENCE_SUBTRACT
33
           || n.getKind() == kind::DIFFERENCE_REMOVE);
34
316
    TypeNode bagType = n[0].getType(check);
35
316
    if (check)
36
    {
37
316
      if (!bagType.isBag())
38
      {
39
        throw TypeCheckingExceptionPrivate(
40
            n, "operator expects a bag, first argument is not");
41
      }
42
632
      TypeNode secondBagType = n[1].getType(check);
43
316
      if (secondBagType != bagType)
44
      {
45
        std::stringstream ss;
46
        ss << "Operator " << n.getKind()
47
           << " expects two bags of the same type. Found types '" << bagType
48
           << "' and '" << secondBagType << "'.";
49
        throw TypeCheckingExceptionPrivate(n, ss.str());
50
      }
51
    }
52
316
    return bagType;
53
  }
54
55
121
  static bool computeIsConst(NodeManager* nodeManager, TNode n)
56
  {
57
    // only UNION_DISJOINT has a const rule in kinds.
58
    // Other binary operators do not have const rules in kinds
59
121
    Assert(n.getKind() == kind::UNION_DISJOINT);
60
121
    return NormalForm::isConstant(n);
61
  }
62
}; /* struct BinaryOperatorTypeRule */
63
64
struct SubBagTypeRule
65
{
66
10
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
67
  {
68
10
    Assert(n.getKind() == kind::SUBBAG);
69
20
    TypeNode bagType = n[0].getType(check);
70
10
    if (check)
71
    {
72
10
      if (!bagType.isBag())
73
      {
74
        throw TypeCheckingExceptionPrivate(n, "SUBBAG operating on non-bag");
75
      }
76
20
      TypeNode secondBagType = n[1].getType(check);
77
10
      if (secondBagType != bagType)
78
      {
79
        if (!bagType.isComparableTo(secondBagType))
80
        {
81
          throw TypeCheckingExceptionPrivate(
82
              n, "SUBBAG operating on bags of different types");
83
        }
84
      }
85
    }
86
20
    return nodeManager->booleanType();
87
  }
88
}; /* struct SubBagTypeRule */
89
90
struct CountTypeRule
91
{
92
496
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
93
  {
94
496
    Assert(n.getKind() == kind::BAG_COUNT);
95
992
    TypeNode bagType = n[1].getType(check);
96
496
    if (check)
97
    {
98
496
      if (!bagType.isBag())
99
      {
100
        throw TypeCheckingExceptionPrivate(
101
            n, "checking for membership in a non-bag");
102
      }
103
992
      TypeNode elementType = n[0].getType(check);
104
      // e.g. (count 1 (mkBag (mkBag_op Real) 1.0 3))) is 3 whereas
105
      // (count 1.0 (mkBag (mkBag_op Int) 1 3))) throws a typing error
106
496
      if (!elementType.isSubtypeOf(bagType.getBagElementType()))
107
      {
108
4
        std::stringstream ss;
109
        ss << "member operating on bags of different types:\n"
110
2
           << "child type:  " << elementType << "\n"
111
4
           << "not subtype: " << bagType.getBagElementType() << "\n"
112
2
           << "in term : " << n;
113
2
        throw TypeCheckingExceptionPrivate(n, ss.str());
114
      }
115
    }
116
988
    return nodeManager->integerType();
117
  }
118
}; /* struct CountTypeRule */
119
120
struct DuplicateRemovalTypeRule
121
{
122
16
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
123
  {
124
16
    Assert(n.getKind() == kind::DUPLICATE_REMOVAL);
125
16
    TypeNode bagType = n[0].getType(check);
126
16
    if (check)
127
    {
128
16
      if (!bagType.isBag())
129
      {
130
        std::stringstream ss;
131
        ss << "Applying DUPLICATE_REMOVAL on a non-bag argument in term " << n;
132
        throw TypeCheckingExceptionPrivate(n, ss.str());
133
      }
134
    }
135
16
    return bagType;
136
  }
137
}; /* struct DuplicateRemovalTypeRule */
138
139
struct MkBagTypeRule
140
{
141
257
  static TypeNode computeType(NodeManager* nm, TNode n, bool check)
142
  {
143
257
    Assert(n.getKind() == kind::MK_BAG && n.hasOperator()
144
           && n.getOperator().getKind() == kind::MK_BAG_OP);
145
514
    MakeBagOp op = n.getOperator().getConst<MakeBagOp>();
146
514
    TypeNode expectedElementType = op.getType();
147
257
    if (check)
148
    {
149
257
      if (n.getNumChildren() != 2)
150
      {
151
        std::stringstream ss;
152
        ss << "operands in term " << n << " are " << n.getNumChildren()
153
           << ", but MK_BAG expects 2 operands.";
154
        throw TypeCheckingExceptionPrivate(n, ss.str());
155
      }
156
514
      TypeNode type1 = n[1].getType(check);
157
257
      if (!type1.isInteger())
158
      {
159
        std::stringstream ss;
160
        ss << "MK_BAG expects an integer for " << n[1] << ". Found" << type1;
161
        throw TypeCheckingExceptionPrivate(n, ss.str());
162
      }
163
164
514
      TypeNode actualElementType = n[0].getType(check);
165
      // the type of the element should be a subtype of the type of the operator
166
      // e.g. (mkBag (mkBag_op Real) 1 1) where 1 is an Int
167
257
      if (!actualElementType.isSubtypeOf(expectedElementType))
168
      {
169
        std::stringstream ss;
170
        ss << "The type '" << actualElementType
171
           << "' of the element is not a subtype of '" << expectedElementType
172
           << "' in term : " << n;
173
        throw TypeCheckingExceptionPrivate(n, ss.str());
174
      }
175
    }
176
177
514
    return nm->mkBagType(expectedElementType);
178
  }
179
180
210
  static bool computeIsConst(NodeManager* nodeManager, TNode n)
181
  {
182
210
    Assert(n.getKind() == kind::MK_BAG);
183
    // for a bag to be a constant, both the element and its multiplicity should
184
    // be constants, and the multiplicity should be > 0.
185
757
    return n[0].isConst() && n[1].isConst()
186
960
           && n[1].getConst<Rational>().sgn() == 1;
187
  }
188
}; /* struct MkBagTypeRule */
189
190
struct IsSingletonTypeRule
191
{
192
10
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
193
  {
194
10
    Assert(n.getKind() == kind::BAG_IS_SINGLETON);
195
20
    TypeNode bagType = n[0].getType(check);
196
10
    if (check)
197
    {
198
10
      if (!bagType.isBag())
199
      {
200
        throw TypeCheckingExceptionPrivate(
201
            n, "BAG_IS_SINGLETON operator expects a bag, a non-bag is found");
202
      }
203
    }
204
20
    return nodeManager->booleanType();
205
  }
206
}; /* struct IsMkBagTypeRule */
207
208
struct EmptyBagTypeRule
209
{
210
1344
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
211
  {
212
1344
    Assert(n.getKind() == kind::EMPTYBAG);
213
2688
    EmptyBag emptyBag = n.getConst<EmptyBag>();
214
2688
    return emptyBag.getType();
215
  }
216
}; /* struct EmptyBagTypeRule */
217
218
struct CardTypeRule
219
{
220
14
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
221
  {
222
14
    Assert(n.getKind() == kind::BAG_CARD);
223
28
    TypeNode bagType = n[0].getType(check);
224
14
    if (check)
225
    {
226
14
      if (!bagType.isBag())
227
      {
228
        throw TypeCheckingExceptionPrivate(
229
            n, "cardinality operates on a bag, non-bag object found");
230
      }
231
    }
232
28
    return nodeManager->integerType();
233
  }
234
}; /* struct CardTypeRule */
235
236
struct ChooseTypeRule
237
{
238
8
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
239
  {
240
8
    Assert(n.getKind() == kind::BAG_CHOOSE);
241
16
    TypeNode bagType = n[0].getType(check);
242
8
    if (check)
243
    {
244
8
      if (!bagType.isBag())
245
      {
246
        throw TypeCheckingExceptionPrivate(
247
            n, "CHOOSE operator expects a bag, a non-bag is found");
248
      }
249
    }
250
16
    return bagType.getBagElementType();
251
  }
252
}; /* struct ChooseTypeRule */
253
254
struct FromSetTypeRule
255
{
256
10
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
257
  {
258
10
    Assert(n.getKind() == kind::BAG_FROM_SET);
259
20
    TypeNode setType = n[0].getType(check);
260
10
    if (check)
261
    {
262
10
      if (!setType.isSet())
263
      {
264
        throw TypeCheckingExceptionPrivate(
265
            n, "bag.from_set operator expects a set, a non-set is found");
266
      }
267
    }
268
20
    TypeNode elementType = setType.getSetElementType();
269
10
    TypeNode bagType = nodeManager->mkBagType(elementType);
270
20
    return bagType;
271
  }
272
}; /* struct FromSetTypeRule */
273
274
struct ToSetTypeRule
275
{
276
10
  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
277
  {
278
10
    Assert(n.getKind() == kind::BAG_TO_SET);
279
20
    TypeNode bagType = n[0].getType(check);
280
10
    if (check)
281
    {
282
10
      if (!bagType.isBag())
283
      {
284
        throw TypeCheckingExceptionPrivate(
285
            n, "bag.to_set operator expects a bag, a non-bag is found");
286
      }
287
    }
288
20
    TypeNode elementType = bagType.getBagElementType();
289
10
    TypeNode setType = nodeManager->mkSetType(elementType);
290
20
    return setType;
291
  }
292
}; /* struct ToSetTypeRule */
293
294
struct BagsProperties
295
{
296
  static Cardinality computeCardinality(TypeNode type)
297
  {
298
    return Cardinality::INTEGERS;
299
  }
300
301
  static bool isWellFounded(TypeNode type) { return type[0].isWellFounded(); }
302
303
  static Node mkGroundTerm(TypeNode type)
304
  {
305
    Assert(type.isBag());
306
    return NodeManager::currentNM()->mkConst(EmptyBag(type));
307
  }
308
}; /* struct BagsProperties */
309
310
}  // namespace bags
311
}  // namespace theory
312
}  // namespace CVC4
313
314
#endif /* CVC4__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H */