GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/builtin/theory_builtin_type_rules.h Lines: 73 118 61.9 %
Date: 2021-03-22 Branches: 164 484 33.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_builtin_type_rules.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Andrew Reynolds, Dejan Jovanovic
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 Type rules for the builtin theory
13
 **
14
 ** Type rules for the builtin theory.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H
20
#define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H
21
22
#include "expr/node.h"
23
#include "expr/type_node.h"
24
#include "theory/builtin/theory_builtin_rewriter.h" // for array and lambda representation
25
26
#include <sstream>
27
28
namespace CVC4 {
29
namespace theory {
30
namespace builtin {
31
32
class EqualityTypeRule {
33
 public:
34
4946912
  inline static TypeNode computeType(NodeManager* nodeManager,
35
                                     TNode n,
36
                                     bool check)
37
  {
38
4946912
    TypeNode booleanType = nodeManager->booleanType();
39
40
4946912
    if (check)
41
    {
42
9893824
      TypeNode lhsType = n[0].getType(check);
43
9893824
      TypeNode rhsType = n[1].getType(check);
44
45
4946912
      if (TypeNode::leastCommonTypeNode(lhsType, rhsType).isNull())
46
      {
47
156
        std::stringstream ss;
48
78
        ss << "Subexpressions must have a common base type:" << std::endl;
49
92
        ss << "Equation: " << n << std::endl;
50
64
        ss << "Type 1: " << lhsType << std::endl;
51
64
        ss << "Type 2: " << rhsType << std::endl;
52
53
64
        throw TypeCheckingExceptionPrivate(n, ss.str());
54
      }
55
      // TODO : check isFirstClass for these types? (github issue #1202)
56
    }
57
4946834
    return booleanType;
58
  }
59
};/* class EqualityTypeRule */
60
61
62
class DistinctTypeRule {
63
 public:
64
10473
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
65
10473
    if( check ) {
66
10473
      TNode::iterator child_it = n.begin();
67
10473
      TNode::iterator child_it_end = n.end();
68
20946
      TypeNode joinType = (*child_it).getType(check);
69
22707
      for (++child_it; child_it != child_it_end; ++child_it) {
70
24468
        TypeNode currentType = (*child_it).getType();
71
12234
        joinType = TypeNode::leastCommonTypeNode(joinType, currentType);
72
12234
        if (joinType.isNull()) {
73
          throw TypeCheckingExceptionPrivate(n, "Not all arguments are of the same type");
74
        }
75
      }
76
    }
77
10473
    return nodeManager->booleanType();
78
  }
79
};/* class DistinctTypeRule */
80
81
class SExprTypeRule {
82
 public:
83
573917
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
84
1147834
    std::vector<TypeNode> types;
85
2303598
    for(TNode::iterator child_it = n.begin(), child_it_end = n.end();
86
2303598
        child_it != child_it_end;
87
        ++child_it) {
88
1729681
      types.push_back((*child_it).getType(check));
89
    }
90
1147834
    return nodeManager->mkSExprType(types);
91
  }
92
};/* class SExprTypeRule */
93
94
class UninterpretedConstantTypeRule {
95
 public:
96
2559
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
97
2559
    return n.getConst<UninterpretedConstant>().getType();
98
  }
99
};/* class UninterpretedConstantTypeRule */
100
101
class AbstractValueTypeRule {
102
 public:
103
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
104
    // An UnknownTypeException means that this node has no type.  For now,
105
    // only abstract values are like this---and then, only if they are created
106
    // by the user and don't actually correspond to one that the SmtEngine gave
107
    // them previously.
108
    throw UnknownTypeException(n);
109
  }
110
};/* class AbstractValueTypeRule */
111
112
class LambdaTypeRule {
113
 public:
114
22409
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
115
22409
    if( n[0].getType(check) != nodeManager->boundVarListType() ) {
116
      std::stringstream ss;
117
      ss << "expected a bound var list for LAMBDA expression, got `"
118
         << n[0].getType().toString() << "'";
119
      throw TypeCheckingExceptionPrivate(n, ss.str());
120
    }
121
44818
    std::vector<TypeNode> argTypes;
122
87252
    for(TNode::iterator i = n[0].begin(); i != n[0].end(); ++i) {
123
64843
      argTypes.push_back((*i).getType());
124
    }
125
44818
    TypeNode rangeType = n[1].getType(check);
126
44818
    return nodeManager->mkFunctionType(argTypes, rangeType);
127
  }
128
  // computes whether a lambda is a constant value, via conversion to array representation
129
2417
  inline static bool computeIsConst(NodeManager* nodeManager, TNode n)
130
  {
131
2417
    Assert(n.getKind() == kind::LAMBDA);
132
    //get array representation of this function, if possible
133
4834
    Node na = TheoryBuiltinRewriter::getArrayRepresentationForLambda(n);
134
2417
    if( !na.isNull() ){
135
583
      Assert(na.getType().isArray());
136
583
      Trace("lambda-const") << "Array representation for " << n << " is " << na << " " << na.getType() << std::endl;
137
      // must have the standard bound variable list
138
743
      Node bvl = NodeManager::currentNM()->getBoundVarListForFunctionType( n.getType() );
139
583
      if( bvl==n[0] ){
140
        //array must be constant
141
423
        if( na.isConst() ){
142
423
          Trace("lambda-const") << "*** Constant lambda : " << n;
143
423
          Trace("lambda-const") << " since its array representation : " << na << " is constant." << std::endl;
144
423
          return true;
145
        }else{
146
          Trace("lambda-const") << "Non-constant lambda : " << n << " since array is not constant." << std::endl;
147
        }
148
      }else{
149
160
        Trace("lambda-const") << "Non-constant lambda : " << n << " since its varlist is not standard." << std::endl;
150
160
        Trace("lambda-const") << "  standard : " << bvl << std::endl;
151
160
        Trace("lambda-const") << "   current : " << n[0] << std::endl;
152
      }
153
    }else{
154
1834
      Trace("lambda-const") << "Non-constant lambda : " << n << " since it has no array representation." << std::endl;
155
    }
156
1994
    return false;
157
  }
158
};/* class LambdaTypeRule */
159
160
class WitnessTypeRule
161
{
162
 public:
163
4358
  inline static TypeNode computeType(NodeManager* nodeManager,
164
                                     TNode n,
165
                                     bool check)
166
  {
167
4358
    if (n[0].getType(check) != nodeManager->boundVarListType())
168
    {
169
      std::stringstream ss;
170
      ss << "expected a bound var list for WITNESS expression, got `"
171
         << n[0].getType().toString() << "'";
172
      throw TypeCheckingExceptionPrivate(n, ss.str());
173
    }
174
4358
    if (n[0].getNumChildren() != 1)
175
    {
176
      std::stringstream ss;
177
      ss << "expected a bound var list with one argument for WITNESS expression";
178
      throw TypeCheckingExceptionPrivate(n, ss.str());
179
    }
180
4358
    if (check)
181
    {
182
8716
      TypeNode rangeType = n[1].getType(check);
183
4358
      if (!rangeType.isBoolean())
184
      {
185
        std::stringstream ss;
186
        ss << "expected a body of a WITNESS expression to have Boolean type";
187
        throw TypeCheckingExceptionPrivate(n, ss.str());
188
      }
189
    }
190
    // The type of a witness function is the type of its bound variable.
191
4358
    return n[0][0].getType();
192
  }
193
}; /* class WitnessTypeRule */
194
195
class SortProperties {
196
 public:
197
  inline static bool isWellFounded(TypeNode type) {
198
    return true;
199
  }
200
  static Node mkGroundTerm(TypeNode type);
201
};/* class SortProperties */
202
203
class FunctionProperties {
204
 public:
205
153
  inline static Cardinality computeCardinality(TypeNode type) {
206
    // Don't assert this; allow other theories to use this cardinality
207
    // computation.
208
    //
209
    // Assert(type.getKind() == kind::FUNCTION_TYPE);
210
211
306
    Cardinality argsCard(1);
212
    // get the largest cardinality of function arguments/return type
213
393
    for(unsigned i = 0, i_end = type.getNumChildren() - 1; i < i_end; ++i) {
214
240
      argsCard *= type[i].getCardinality();
215
    }
216
217
306
    Cardinality valueCard = type[type.getNumChildren() - 1].getCardinality();
218
219
306
    return valueCard ^ argsCard;
220
  }
221
  /** Function type is well-founded if its component sorts are */
222
  static bool isWellFounded(TypeNode type)
223
  {
224
    for (TypeNode::iterator i = type.begin(), i_end = type.end(); i != i_end;
225
         ++i)
226
    {
227
      if (!(*i).isWellFounded())
228
      {
229
        return false;
230
      }
231
    }
232
    return true;
233
  }
234
  /**
235
   * Ground term for function sorts is (lambda x. t) where x is the
236
   * canonical variable list for its type and t is the canonical ground term of
237
   * its range.
238
   */
239
2
  static Node mkGroundTerm(TypeNode type)
240
  {
241
2
    NodeManager* nm = NodeManager::currentNM();
242
4
    Node bvl = nm->getBoundVarListForFunctionType(type);
243
4
    Node ret = type.getRangeType().mkGroundTerm();
244
4
    return nm->mkNode(kind::LAMBDA, bvl, ret);
245
  }
246
};/* class FuctionProperties */
247
248
class SExprProperties {
249
 public:
250
  inline static Cardinality computeCardinality(TypeNode type) {
251
    // Don't assert this; allow other theories to use this cardinality
252
    // computation.
253
    //
254
    // Assert(type.getKind() == kind::SEXPR_TYPE);
255
256
    Cardinality card(1);
257
    for(TypeNode::iterator i = type.begin(),
258
          i_end = type.end();
259
        i != i_end;
260
        ++i) {
261
      card *= (*i).getCardinality();
262
    }
263
264
    return card;
265
  }
266
267
  inline static bool isWellFounded(TypeNode type) {
268
    // Don't assert this; allow other theories to use this
269
    // wellfoundedness computation.
270
    //
271
    // Assert(type.getKind() == kind::SEXPR_TYPE);
272
273
    for(TypeNode::iterator i = type.begin(),
274
          i_end = type.end();
275
        i != i_end;
276
        ++i) {
277
      if(! (*i).isWellFounded()) {
278
        return false;
279
      }
280
    }
281
282
    return true;
283
  }
284
285
  inline static Node mkGroundTerm(TypeNode type) {
286
    Assert(type.getKind() == kind::SEXPR_TYPE);
287
288
    std::vector<Node> children;
289
    for(TypeNode::iterator i = type.begin(),
290
          i_end = type.end();
291
        i != i_end;
292
        ++i) {
293
      children.push_back((*i).mkGroundTerm());
294
    }
295
296
    return NodeManager::currentNM()->mkNode(kind::SEXPR, children);
297
  }
298
};/* class SExprProperties */
299
300
}/* CVC4::theory::builtin namespace */
301
}/* CVC4::theory namespace */
302
}/* CVC4 namespace */
303
304
#endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H */