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