GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/expr/type_properties.h Lines: 38 105 36.2 %
Date: 2021-03-23 Branches: 49 253 19.4 %

Line Exec Source
1
/*********************                                                        */
2
/** type_properties.h
3
 **
4
 ** Copyright 2010-2014  New York University and The University of Iowa,
5
 ** and as below.
6
 **
7
 ** This header file automatically generated by:
8
 **
9
 **     ../../../src/expr/mkkind /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/expr/type_properties_template.h /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/builtin/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/booleans/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/uf/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/arith/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/bv/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/fp/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/arrays/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/datatypes/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/sep/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/sets/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/bags/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/strings/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/quantifiers/kinds
10
 **
11
 ** for the CVC4 project.
12
 **/
13
14
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
15
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
16
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
17
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
18
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
19
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
20
21
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
22
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
23
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
24
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
25
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
26
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
27
28
/* Edit the template file instead:                     */
29
/* /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/expr/type_properties_template.h */
30
31
/*********************                                                        */
32
/*! \file type_properties_template.h
33
 ** \verbatim
34
 ** Top contributors (to current version):
35
 **   Morgan Deters, Mathias Preiner
36
 ** This file is part of the CVC4 project.
37
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
38
 ** in the top-level source directory and their institutional affiliations.
39
 ** All rights reserved.  See the file COPYING in the top-level source
40
 ** directory for licensing information.\endverbatim
41
 **
42
 ** \brief Template for the Type properties header
43
 **
44
 ** Template for the Type properties header.
45
 **/
46
47
#include "cvc4_private.h"
48
49
#ifndef CVC4__TYPE_PROPERTIES_H
50
#define CVC4__TYPE_PROPERTIES_H
51
52
#include <sstream>
53
54
#include "base/check.h"
55
#include "expr/kind.h"
56
#include "expr/node.h"
57
#include "expr/type_node.h"
58
#include "options/language.h"
59
60
61
#include "theory/builtin/theory_builtin_type_rules.h"
62
63
#include "theory/builtin/theory_builtin_type_rules.h"
64
65
#include "theory/builtin/theory_builtin_type_rules.h"
66
67
#include "theory/builtin/theory_builtin_type_rules.h"
68
69
#include "expr/node_manager.h"
70
71
#include "expr/node_manager.h"
72
73
#include "expr/node_manager.h"
74
75
#include "theory/bv/theory_bv_type_rules.h"
76
77
#include "theory/type_enumerator.h"
78
79
#include "expr/node_manager.h"
80
81
#include "theory/fp/theory_fp_type_rules.h"
82
83
#include "theory/type_enumerator.h"
84
85
#include "theory/arrays/theory_arrays_type_rules.h"
86
87
#include "theory/arrays/theory_arrays_type_rules.h"
88
89
#include "theory/datatypes/theory_datatypes_type_rules.h"
90
91
#include "theory/builtin/theory_builtin_type_rules.h"
92
93
#include "theory/builtin/theory_builtin_type_rules.h"
94
95
#include "expr/dtype.h"
96
97
#include "expr/dtype.h"
98
99
#include "expr/dtype.h"
100
101
#include "expr/dtype.h"
102
103
#include "theory/sets/theory_sets_type_rules.h"
104
105
#include "theory/sets/theory_sets_type_rules.h"
106
107
#include "theory/bags/theory_bags_type_rules.h"
108
109
#include "theory/bags/theory_bags_type_rules.h"
110
111
#include "util/string.h"
112
113
#include "util/string.h"
114
115
#include "theory/strings/theory_strings_type_rules.h"
116
117
#include "theory/strings/theory_strings_type_rules.h"
118
119
120
namespace CVC4 {
121
namespace kind {
122
123
/**
124
 * Return the cardinality of the type constant represented by the
125
 * TypeConstant argument.  This function is auto-generated from Theory
126
 * "kinds" files, so includes contributions from each theory regarding
127
 * that theory's types.
128
 */
129
10053
inline Cardinality getCardinality(TypeConstant tc)
130
{
131
10053
  switch (tc)
132
  {
133
134
  case BUILTIN_OPERATOR_TYPE: return Cardinality(Cardinality::INTEGERS);
135
136
948
  case BOOLEAN_TYPE: return Cardinality(2);
137
138
110
  case REAL_TYPE: return Cardinality(Cardinality::REALS);
139
140
8965
  case INTEGER_TYPE: return Cardinality(Cardinality::INTEGERS);
141
142
  case ROUNDINGMODE_TYPE: return Cardinality(5);
143
144
30
  case STRING_TYPE: return Cardinality(Cardinality::INTEGERS);
145
146
  case REGEXP_TYPE: return Cardinality(Cardinality::INTEGERS);
147
148
  case BOUND_VAR_LIST_TYPE: return Cardinality(Cardinality::INTEGERS);
149
150
  case INST_PATTERN_TYPE: return Cardinality(Cardinality::INTEGERS);
151
152
  case INST_PATTERN_LIST_TYPE: return Cardinality(Cardinality::INTEGERS);
153
154
    default: InternalError() << "No cardinality known for type constant " << tc;
155
  }
156
} /* getCardinality(TypeConstant) */
157
158
/**
159
 * Return the cardinality of the type represented by the TypeNode
160
 * argument.  This function is auto-generated from Theory "kinds"
161
 * files, so includes contributions from each theory regarding that
162
 * theory's types.
163
 */
164
16950
inline Cardinality getCardinality(TypeNode typeNode) {
165
16950
  AssertArgument(!typeNode.isNull(), typeNode);
166
16950
  switch(Kind k = typeNode.getKind()) {
167
10053
  case TYPE_CONSTANT:
168
10053
    return getCardinality(typeNode.getConst<TypeConstant>());
169
170
849
  case SORT_TYPE: return Cardinality(Cardinality::INTEGERS);
171
172
153
  case FUNCTION_TYPE: return ::CVC4::theory::builtin::FunctionProperties::computeCardinality(typeNode);
173
174
  case SEXPR_TYPE: return ::CVC4::theory::builtin::SExprProperties::computeCardinality(typeNode);
175
176
2463
  case BITVECTOR_TYPE: return ::CVC4::theory::bv::CardinalityComputer::computeCardinality(typeNode);
177
178
12
  case FLOATINGPOINT_TYPE: return ::CVC4::theory::fp::CardinalityComputer::computeCardinality(typeNode);
179
180
292
  case ARRAY_TYPE: return ::CVC4::theory::arrays::ArraysProperties::computeCardinality(typeNode);
181
182
2
  case CONSTRUCTOR_TYPE: return ::CVC4::theory::datatypes::ConstructorProperties::computeCardinality(typeNode);
183
184
  case SELECTOR_TYPE: return ::CVC4::theory::builtin::FunctionProperties::computeCardinality(typeNode);
185
186
  case TESTER_TYPE: return ::CVC4::theory::builtin::FunctionProperties::computeCardinality(typeNode);
187
188
3126
  case DATATYPE_TYPE: return typeNode.getDType().getCardinality(typeNode);
189
190
  case PARAMETRIC_DATATYPE: return typeNode.getDType().getCardinality(typeNode);
191
192
  case SET_TYPE: return ::CVC4::theory::sets::SetsProperties::computeCardinality(typeNode);
193
194
  case BAG_TYPE: return ::CVC4::theory::bags::BagsProperties::computeCardinality(typeNode);
195
196
  case SEQUENCE_TYPE: return ::CVC4::theory::strings::SequenceProperties::computeCardinality(typeNode);
197
198
  default:
199
    InternalError() << "A theory kinds file did not provide a cardinality "
200
                    << "or cardinality computer for type:\n"
201
                    << typeNode << "\nof kind " << k;
202
  }
203
}/* getCardinality(TypeNode) */
204
205
inline bool isWellFounded(TypeConstant tc) {
206
  switch(tc) {
207
208
  case BUILTIN_OPERATOR_TYPE: return false;
209
210
  case BOOLEAN_TYPE: return true;
211
212
  case REAL_TYPE: return true;
213
214
  case INTEGER_TYPE: return true;
215
216
  case ROUNDINGMODE_TYPE: return true;
217
218
  case STRING_TYPE: return true;
219
220
  case REGEXP_TYPE: return true;
221
222
  case BOUND_VAR_LIST_TYPE: return false;
223
224
  case INST_PATTERN_TYPE: return false;
225
226
  case INST_PATTERN_LIST_TYPE: return false;
227
228
default:
229
  InternalError() << "No well-foundedness status known for type constant: "
230
                  << tc;
231
  }
232
}/* isWellFounded(TypeConstant) */
233
234
inline bool isWellFounded(TypeNode typeNode) {
235
  AssertArgument(!typeNode.isNull(), typeNode);
236
  switch(Kind k = typeNode.getKind()) {
237
  case TYPE_CONSTANT:
238
    return isWellFounded(typeNode.getConst<TypeConstant>());
239
240
  case SORT_TYPE: return ::CVC4::theory::builtin::SortProperties::isWellFounded(typeNode);
241
242
  case FUNCTION_TYPE: return ::CVC4::theory::builtin::FunctionProperties::isWellFounded(typeNode);
243
244
  case SEXPR_TYPE: return ::CVC4::theory::builtin::SExprProperties::isWellFounded(typeNode);
245
246
  case BITVECTOR_TYPE: return true;
247
248
  case FLOATINGPOINT_TYPE: return true;
249
250
  case ARRAY_TYPE: return ::CVC4::theory::arrays::ArraysProperties::isWellFounded(typeNode);
251
252
  case DATATYPE_TYPE: return typeNode.getDType().isWellFounded();
253
254
  case PARAMETRIC_DATATYPE: return typeNode.getDType().isWellFounded();
255
256
  case SET_TYPE: return ::CVC4::theory::sets::SetsProperties::isWellFounded(typeNode);
257
258
  case BAG_TYPE: return ::CVC4::theory::bags::BagsProperties::isWellFounded(typeNode);
259
260
  case SEQUENCE_TYPE: return ::CVC4::theory::strings::SequenceProperties::isWellFounded(typeNode);
261
262
  default:
263
    InternalError() << "A theory kinds file did not provide a well-foundedness "
264
                    << "or well-foundedness computer for type:\n"
265
                    << typeNode << "\nof kind " << k;
266
  }
267
}/* isWellFounded(TypeNode) */
268
269
1332
inline Node mkGroundTerm(TypeConstant tc)
270
{
271
1332
  switch (tc)
272
  {
273
274
  case BUILTIN_OPERATOR_TYPE: Unhandled() << tc;
275
276
33
  case BOOLEAN_TYPE: return NodeManager::currentNM()->mkConst(false);
277
278
11
  case REAL_TYPE: return NodeManager::currentNM()->mkConst(Rational(0));
279
280
815
  case INTEGER_TYPE: return NodeManager::currentNM()->mkConst(Rational(0));
281
282
7
  case ROUNDINGMODE_TYPE: return NodeManager::currentNM()->mkConst<RoundingMode>(RoundingMode());
283
284
466
  case STRING_TYPE: return NodeManager::currentNM()->mkConst(::CVC4::String());
285
286
  case REGEXP_TYPE: return NodeManager::currentNM()->mkNode(REGEXP_EMPTY, std::vector<Node>() );
287
288
  case BOUND_VAR_LIST_TYPE: Unhandled() << tc;
289
290
  case INST_PATTERN_TYPE: Unhandled() << tc;
291
292
  case INST_PATTERN_LIST_TYPE: Unhandled() << tc;
293
294
    default:
295
      InternalError() << "No ground term known for type constant: " << tc;
296
  }
297
} /* mkGroundTerm(TypeConstant) */
298
299
156151
inline Node mkGroundTerm(TypeNode typeNode)
300
{
301
156151
  AssertArgument(!typeNode.isNull(), typeNode);
302
156151
  switch (Kind k = typeNode.getKind())
303
  {
304
1332
    case TYPE_CONSTANT:
305
1332
      return mkGroundTerm(typeNode.getConst<TypeConstant>());
306
307
265
  case SORT_TYPE: return ::CVC4::theory::builtin::SortProperties::mkGroundTerm(typeNode);
308
309
2
  case FUNCTION_TYPE: return ::CVC4::theory::builtin::FunctionProperties::mkGroundTerm(typeNode);
310
311
  case SEXPR_TYPE: return ::CVC4::theory::builtin::SExprProperties::mkGroundTerm(typeNode);
312
313
810
  case BITVECTOR_TYPE: return (*CVC4::theory::TypeEnumerator(typeNode));
314
315
6
  case FLOATINGPOINT_TYPE: return (*CVC4::theory::TypeEnumerator(typeNode));
316
317
19
  case ARRAY_TYPE: return ::CVC4::theory::arrays::ArraysProperties::mkGroundTerm(typeNode);
318
319
153705
  case DATATYPE_TYPE: return typeNode.getDType().mkGroundTerm(typeNode);
320
321
4
  case PARAMETRIC_DATATYPE: return typeNode.getDType().mkGroundTerm(typeNode);
322
323
8
  case SET_TYPE: return ::CVC4::theory::sets::SetsProperties::mkGroundTerm(typeNode);
324
325
  case BAG_TYPE: return ::CVC4::theory::bags::BagsProperties::mkGroundTerm(typeNode);
326
327
  case SEQUENCE_TYPE: return ::CVC4::theory::strings::SequenceProperties::mkGroundTerm(typeNode);
328
329
    default:
330
      InternalError() << "A theory kinds file did not provide a ground term "
331
                      << "or ground term computer for type:\n"
332
                      << typeNode << "\nof kind " << k;
333
  }
334
} /* mkGroundTerm(TypeNode) */
335
336
}/* CVC4::kind namespace */
337
}/* CVC4 namespace */
338
339
#endif /* CVC4__TYPE_PROPERTIES_H */