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-05/src/expr/kind_template.cpp /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-05/src/theory/builtin/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-05/src/theory/booleans/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-05/src/theory/uf/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-05/src/theory/arith/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-05/src/theory/bv/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-05/src/theory/fp/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-05/src/theory/arrays/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-05/src/theory/datatypes/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-05/src/theory/sep/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-05/src/theory/sets/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-05/src/theory/bags/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-05/src/theory/strings/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-05/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-05/src/expr/kind_template.cpp */ |
33 |
|
|
34 |
|
/****************************************************************************** |
35 |
|
* Top contributors (to current version): |
36 |
|
* Andres Noetzli, Aina Niemetz, Christopher L. Conway |
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 |
|
* [[ Add one-line brief description here ]] |
47 |
|
* |
48 |
|
* [[ Add lengthier description here ]] |
49 |
|
* \todo document this file |
50 |
|
*/ |
51 |
|
|
52 |
|
#include <sstream> |
53 |
|
|
54 |
|
#include "expr/kind.h" |
55 |
|
|
56 |
|
namespace cvc5 { |
57 |
|
namespace kind { |
58 |
|
|
59 |
14601 |
const char* toString(cvc5::Kind k) |
60 |
|
{ |
61 |
|
using namespace cvc5::kind; |
62 |
|
|
63 |
14601 |
switch (k) |
64 |
|
{ |
65 |
|
/* special cases */ |
66 |
4 |
case UNDEFINED_KIND: return "UNDEFINED_KIND"; |
67 |
4 |
case NULL_EXPR: return "NULL"; |
68 |
|
// clang-format off |
69 |
|
|
70 |
|
/* from builtin */ |
71 |
|
case SORT_TAG: return "SORT_TAG"; |
72 |
|
case SORT_TYPE: return "SORT_TYPE"; |
73 |
|
case UNINTERPRETED_CONSTANT: return "UNINTERPRETED_CONSTANT"; |
74 |
|
case ABSTRACT_VALUE: return "ABSTRACT_VALUE"; |
75 |
|
case BUILTIN: return "BUILTIN"; |
76 |
847 |
case EQUAL: return "EQUAL"; |
77 |
4 |
case DISTINCT: return "DISTINCT"; |
78 |
33 |
case VARIABLE: return "VARIABLE"; |
79 |
1460 |
case BOUND_VARIABLE: return "BOUND_VARIABLE"; |
80 |
|
case SKOLEM: return "SKOLEM"; |
81 |
4 |
case SEXPR: return "SEXPR"; |
82 |
20 |
case LAMBDA: return "LAMBDA"; |
83 |
|
case WITNESS: return "WITNESS"; |
84 |
|
case TYPE_CONSTANT: return "TYPE_CONSTANT"; |
85 |
|
case FUNCTION_TYPE: return "FUNCTION_TYPE"; |
86 |
|
|
87 |
|
/* from booleans */ |
88 |
80 |
case CONST_BOOLEAN: return "CONST_BOOLEAN"; |
89 |
707 |
case NOT: return "NOT"; |
90 |
749 |
case AND: return "AND"; |
91 |
5 |
case IMPLIES: return "IMPLIES"; |
92 |
736 |
case OR: return "OR"; |
93 |
24 |
case XOR: return "XOR"; |
94 |
919 |
case ITE: return "ITE"; |
95 |
|
|
96 |
|
/* from uf */ |
97 |
146 |
case APPLY_UF: return "APPLY_UF"; |
98 |
5 |
case BOOLEAN_TERM_VARIABLE: return "BOOLEAN_TERM_VARIABLE"; |
99 |
|
case PARTIAL_APPLY_UF: return "PARTIAL_APPLY_UF"; |
100 |
|
case HO_APPLY: return "HO_APPLY"; |
101 |
|
case CARDINALITY_CONSTRAINT_OP: return "CARDINALITY_CONSTRAINT_OP"; |
102 |
|
case CARDINALITY_CONSTRAINT: return "CARDINALITY_CONSTRAINT"; |
103 |
|
case COMBINED_CARDINALITY_CONSTRAINT_OP: return "COMBINED_CARDINALITY_CONSTRAINT_OP"; |
104 |
|
case COMBINED_CARDINALITY_CONSTRAINT: return "COMBINED_CARDINALITY_CONSTRAINT"; |
105 |
|
|
106 |
|
/* from arith */ |
107 |
791 |
case PLUS: return "PLUS"; |
108 |
14 |
case MULT: return "MULT"; |
109 |
|
case NONLINEAR_MULT: return "NONLINEAR_MULT"; |
110 |
676 |
case MINUS: return "MINUS"; |
111 |
28 |
case UMINUS: return "UMINUS"; |
112 |
43 |
case DIVISION: return "DIVISION"; |
113 |
|
case DIVISION_TOTAL: return "DIVISION_TOTAL"; |
114 |
1 |
case INTS_DIVISION: return "INTS_DIVISION"; |
115 |
|
case INTS_DIVISION_TOTAL: return "INTS_DIVISION_TOTAL"; |
116 |
5 |
case INTS_MODULUS: return "INTS_MODULUS"; |
117 |
|
case INTS_MODULUS_TOTAL: return "INTS_MODULUS_TOTAL"; |
118 |
|
case ABS: return "ABS"; |
119 |
16 |
case DIVISIBLE: return "DIVISIBLE"; |
120 |
|
case POW: return "POW"; |
121 |
|
case POW2: return "POW2"; |
122 |
|
case EXPONENTIAL: return "EXPONENTIAL"; |
123 |
|
case SINE: return "SINE"; |
124 |
|
case COSINE: return "COSINE"; |
125 |
|
case TANGENT: return "TANGENT"; |
126 |
|
case COSECANT: return "COSECANT"; |
127 |
|
case SECANT: return "SECANT"; |
128 |
|
case COTANGENT: return "COTANGENT"; |
129 |
|
case ARCSINE: return "ARCSINE"; |
130 |
|
case ARCCOSINE: return "ARCCOSINE"; |
131 |
|
case ARCTANGENT: return "ARCTANGENT"; |
132 |
|
case ARCCOSECANT: return "ARCCOSECANT"; |
133 |
|
case ARCSECANT: return "ARCSECANT"; |
134 |
|
case ARCCOTANGENT: return "ARCCOTANGENT"; |
135 |
|
case SQRT: return "SQRT"; |
136 |
|
case DIVISIBLE_OP: return "DIVISIBLE_OP"; |
137 |
467 |
case CONST_RATIONAL: return "CONST_RATIONAL"; |
138 |
35 |
case LT: return "LT"; |
139 |
675 |
case LEQ: return "LEQ"; |
140 |
28 |
case GT: return "GT"; |
141 |
46 |
case GEQ: return "GEQ"; |
142 |
|
case INDEXED_ROOT_PREDICATE_OP: return "INDEXED_ROOT_PREDICATE_OP"; |
143 |
|
case INDEXED_ROOT_PREDICATE: return "INDEXED_ROOT_PREDICATE"; |
144 |
|
case IS_INTEGER: return "IS_INTEGER"; |
145 |
|
case TO_INTEGER: return "TO_INTEGER"; |
146 |
|
case TO_REAL: return "TO_REAL"; |
147 |
|
case CAST_TO_REAL: return "CAST_TO_REAL"; |
148 |
|
case PI: return "PI"; |
149 |
|
case IAND_OP: return "IAND_OP"; |
150 |
|
case IAND: return "IAND"; |
151 |
|
|
152 |
|
/* from bv */ |
153 |
|
case BITVECTOR_TYPE: return "BITVECTOR_TYPE"; |
154 |
105 |
case CONST_BITVECTOR: return "CONST_BITVECTOR"; |
155 |
|
case BITVECTOR_BB_TERM: return "BITVECTOR_BB_TERM"; |
156 |
2 |
case BITVECTOR_CONCAT: return "BITVECTOR_CONCAT"; |
157 |
88 |
case BITVECTOR_AND: return "BITVECTOR_AND"; |
158 |
14 |
case BITVECTOR_COMP: return "BITVECTOR_COMP"; |
159 |
110 |
case BITVECTOR_OR: return "BITVECTOR_OR"; |
160 |
69 |
case BITVECTOR_XOR: return "BITVECTOR_XOR"; |
161 |
112 |
case BITVECTOR_NOT: return "BITVECTOR_NOT"; |
162 |
|
case BITVECTOR_NAND: return "BITVECTOR_NAND"; |
163 |
|
case BITVECTOR_NOR: return "BITVECTOR_NOR"; |
164 |
|
case BITVECTOR_XNOR: return "BITVECTOR_XNOR"; |
165 |
51 |
case BITVECTOR_MULT: return "BITVECTOR_MULT"; |
166 |
58 |
case BITVECTOR_NEG: return "BITVECTOR_NEG"; |
167 |
82 |
case BITVECTOR_ADD: return "BITVECTOR_ADD"; |
168 |
50 |
case BITVECTOR_SUB: return "BITVECTOR_SUB"; |
169 |
53 |
case BITVECTOR_UDIV: return "BITVECTOR_UDIV"; |
170 |
53 |
case BITVECTOR_UREM: return "BITVECTOR_UREM"; |
171 |
51 |
case BITVECTOR_SDIV: return "BITVECTOR_SDIV"; |
172 |
|
case BITVECTOR_SMOD: return "BITVECTOR_SMOD"; |
173 |
47 |
case BITVECTOR_SREM: return "BITVECTOR_SREM"; |
174 |
43 |
case BITVECTOR_ASHR: return "BITVECTOR_ASHR"; |
175 |
54 |
case BITVECTOR_LSHR: return "BITVECTOR_LSHR"; |
176 |
54 |
case BITVECTOR_SHL: return "BITVECTOR_SHL"; |
177 |
4 |
case BITVECTOR_ULE: return "BITVECTOR_ULE"; |
178 |
46 |
case BITVECTOR_ULT: return "BITVECTOR_ULT"; |
179 |
3 |
case BITVECTOR_UGE: return "BITVECTOR_UGE"; |
180 |
2 |
case BITVECTOR_UGT: return "BITVECTOR_UGT"; |
181 |
|
case BITVECTOR_SLE: return "BITVECTOR_SLE"; |
182 |
3 |
case BITVECTOR_SLT: return "BITVECTOR_SLT"; |
183 |
3 |
case BITVECTOR_SGE: return "BITVECTOR_SGE"; |
184 |
|
case BITVECTOR_SGT: return "BITVECTOR_SGT"; |
185 |
16 |
case BITVECTOR_ULTBV: return "BITVECTOR_ULTBV"; |
186 |
4 |
case BITVECTOR_SLTBV: return "BITVECTOR_SLTBV"; |
187 |
|
case BITVECTOR_REDAND: return "BITVECTOR_REDAND"; |
188 |
|
case BITVECTOR_REDOR: return "BITVECTOR_REDOR"; |
189 |
12 |
case BITVECTOR_ITE: return "BITVECTOR_ITE"; |
190 |
|
case BITVECTOR_TO_NAT: return "BITVECTOR_TO_NAT"; |
191 |
|
case BITVECTOR_ACKERMANNIZE_UDIV: return "BITVECTOR_ACKERMANNIZE_UDIV"; |
192 |
|
case BITVECTOR_ACKERMANNIZE_UREM: return "BITVECTOR_ACKERMANNIZE_UREM"; |
193 |
|
case BITVECTOR_EAGER_ATOM: return "BITVECTOR_EAGER_ATOM"; |
194 |
|
case BITVECTOR_BITOF_OP: return "BITVECTOR_BITOF_OP"; |
195 |
|
case BITVECTOR_BITOF: return "BITVECTOR_BITOF"; |
196 |
|
case BITVECTOR_EXTRACT_OP: return "BITVECTOR_EXTRACT_OP"; |
197 |
26 |
case BITVECTOR_EXTRACT: return "BITVECTOR_EXTRACT"; |
198 |
|
case BITVECTOR_REPEAT_OP: return "BITVECTOR_REPEAT_OP"; |
199 |
3 |
case BITVECTOR_REPEAT: return "BITVECTOR_REPEAT"; |
200 |
|
case BITVECTOR_ROTATE_LEFT_OP: return "BITVECTOR_ROTATE_LEFT_OP"; |
201 |
|
case BITVECTOR_ROTATE_LEFT: return "BITVECTOR_ROTATE_LEFT"; |
202 |
|
case BITVECTOR_ROTATE_RIGHT_OP: return "BITVECTOR_ROTATE_RIGHT_OP"; |
203 |
|
case BITVECTOR_ROTATE_RIGHT: return "BITVECTOR_ROTATE_RIGHT"; |
204 |
|
case BITVECTOR_SIGN_EXTEND_OP: return "BITVECTOR_SIGN_EXTEND_OP"; |
205 |
|
case BITVECTOR_SIGN_EXTEND: return "BITVECTOR_SIGN_EXTEND"; |
206 |
|
case BITVECTOR_ZERO_EXTEND_OP: return "BITVECTOR_ZERO_EXTEND_OP"; |
207 |
|
case BITVECTOR_ZERO_EXTEND: return "BITVECTOR_ZERO_EXTEND"; |
208 |
1 |
case INT_TO_BITVECTOR_OP: return "INT_TO_BITVECTOR_OP"; |
209 |
|
case INT_TO_BITVECTOR: return "INT_TO_BITVECTOR"; |
210 |
|
|
211 |
|
/* from fp */ |
212 |
|
case CONST_FLOATINGPOINT: return "CONST_FLOATINGPOINT"; |
213 |
2 |
case CONST_ROUNDINGMODE: return "CONST_ROUNDINGMODE"; |
214 |
|
case FLOATINGPOINT_TYPE: return "FLOATINGPOINT_TYPE"; |
215 |
|
case FLOATINGPOINT_FP: return "FLOATINGPOINT_FP"; |
216 |
|
case FLOATINGPOINT_EQ: return "FLOATINGPOINT_EQ"; |
217 |
2 |
case FLOATINGPOINT_ABS: return "FLOATINGPOINT_ABS"; |
218 |
2 |
case FLOATINGPOINT_NEG: return "FLOATINGPOINT_NEG"; |
219 |
2 |
case FLOATINGPOINT_ADD: return "FLOATINGPOINT_ADD"; |
220 |
4 |
case FLOATINGPOINT_SUB: return "FLOATINGPOINT_SUB"; |
221 |
2 |
case FLOATINGPOINT_MULT: return "FLOATINGPOINT_MULT"; |
222 |
2 |
case FLOATINGPOINT_DIV: return "FLOATINGPOINT_DIV"; |
223 |
|
case FLOATINGPOINT_FMA: return "FLOATINGPOINT_FMA"; |
224 |
2 |
case FLOATINGPOINT_SQRT: return "FLOATINGPOINT_SQRT"; |
225 |
2 |
case FLOATINGPOINT_REM: return "FLOATINGPOINT_REM"; |
226 |
|
case FLOATINGPOINT_RTI: return "FLOATINGPOINT_RTI"; |
227 |
|
case FLOATINGPOINT_MIN: return "FLOATINGPOINT_MIN"; |
228 |
2 |
case FLOATINGPOINT_MAX: return "FLOATINGPOINT_MAX"; |
229 |
|
case FLOATINGPOINT_MIN_TOTAL: return "FLOATINGPOINT_MIN_TOTAL"; |
230 |
|
case FLOATINGPOINT_MAX_TOTAL: return "FLOATINGPOINT_MAX_TOTAL"; |
231 |
|
case FLOATINGPOINT_LEQ: return "FLOATINGPOINT_LEQ"; |
232 |
|
case FLOATINGPOINT_LT: return "FLOATINGPOINT_LT"; |
233 |
|
case FLOATINGPOINT_GEQ: return "FLOATINGPOINT_GEQ"; |
234 |
|
case FLOATINGPOINT_GT: return "FLOATINGPOINT_GT"; |
235 |
1 |
case FLOATINGPOINT_ISN: return "FLOATINGPOINT_ISN"; |
236 |
1 |
case FLOATINGPOINT_ISSN: return "FLOATINGPOINT_ISSN"; |
237 |
3 |
case FLOATINGPOINT_ISZ: return "FLOATINGPOINT_ISZ"; |
238 |
2 |
case FLOATINGPOINT_ISINF: return "FLOATINGPOINT_ISINF"; |
239 |
1 |
case FLOATINGPOINT_ISNAN: return "FLOATINGPOINT_ISNAN"; |
240 |
3 |
case FLOATINGPOINT_ISNEG: return "FLOATINGPOINT_ISNEG"; |
241 |
1 |
case FLOATINGPOINT_ISPOS: return "FLOATINGPOINT_ISPOS"; |
242 |
|
case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: return "FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP"; |
243 |
|
case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: return "FLOATINGPOINT_TO_FP_IEEE_BITVECTOR"; |
244 |
|
case FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: return "FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP"; |
245 |
|
case FLOATINGPOINT_TO_FP_FLOATINGPOINT: return "FLOATINGPOINT_TO_FP_FLOATINGPOINT"; |
246 |
|
case FLOATINGPOINT_TO_FP_REAL_OP: return "FLOATINGPOINT_TO_FP_REAL_OP"; |
247 |
|
case FLOATINGPOINT_TO_FP_REAL: return "FLOATINGPOINT_TO_FP_REAL"; |
248 |
|
case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: return "FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP"; |
249 |
|
case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: return "FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR"; |
250 |
|
case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP: return "FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP"; |
251 |
|
case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: return "FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR"; |
252 |
|
case FLOATINGPOINT_TO_FP_GENERIC_OP: return "FLOATINGPOINT_TO_FP_GENERIC_OP"; |
253 |
2 |
case FLOATINGPOINT_TO_FP_GENERIC: return "FLOATINGPOINT_TO_FP_GENERIC"; |
254 |
|
case FLOATINGPOINT_TO_UBV_OP: return "FLOATINGPOINT_TO_UBV_OP"; |
255 |
|
case FLOATINGPOINT_TO_UBV: return "FLOATINGPOINT_TO_UBV"; |
256 |
|
case FLOATINGPOINT_TO_UBV_TOTAL_OP: return "FLOATINGPOINT_TO_UBV_TOTAL_OP"; |
257 |
|
case FLOATINGPOINT_TO_UBV_TOTAL: return "FLOATINGPOINT_TO_UBV_TOTAL"; |
258 |
|
case FLOATINGPOINT_TO_SBV_OP: return "FLOATINGPOINT_TO_SBV_OP"; |
259 |
|
case FLOATINGPOINT_TO_SBV: return "FLOATINGPOINT_TO_SBV"; |
260 |
|
case FLOATINGPOINT_TO_SBV_TOTAL_OP: return "FLOATINGPOINT_TO_SBV_TOTAL_OP"; |
261 |
|
case FLOATINGPOINT_TO_SBV_TOTAL: return "FLOATINGPOINT_TO_SBV_TOTAL"; |
262 |
|
case FLOATINGPOINT_TO_REAL: return "FLOATINGPOINT_TO_REAL"; |
263 |
|
case FLOATINGPOINT_TO_REAL_TOTAL: return "FLOATINGPOINT_TO_REAL_TOTAL"; |
264 |
|
case FLOATINGPOINT_COMPONENT_NAN: return "FLOATINGPOINT_COMPONENT_NAN"; |
265 |
|
case FLOATINGPOINT_COMPONENT_INF: return "FLOATINGPOINT_COMPONENT_INF"; |
266 |
|
case FLOATINGPOINT_COMPONENT_ZERO: return "FLOATINGPOINT_COMPONENT_ZERO"; |
267 |
|
case FLOATINGPOINT_COMPONENT_SIGN: return "FLOATINGPOINT_COMPONENT_SIGN"; |
268 |
|
case FLOATINGPOINT_COMPONENT_EXPONENT: return "FLOATINGPOINT_COMPONENT_EXPONENT"; |
269 |
|
case FLOATINGPOINT_COMPONENT_SIGNIFICAND: return "FLOATINGPOINT_COMPONENT_SIGNIFICAND"; |
270 |
|
case ROUNDINGMODE_BITBLAST: return "ROUNDINGMODE_BITBLAST"; |
271 |
|
|
272 |
|
/* from arrays */ |
273 |
|
case ARRAY_TYPE: return "ARRAY_TYPE"; |
274 |
18 |
case SELECT: return "SELECT"; |
275 |
18 |
case STORE: return "STORE"; |
276 |
1 |
case EQ_RANGE: return "EQ_RANGE"; |
277 |
|
case STORE_ALL: return "STORE_ALL"; |
278 |
|
case ARR_TABLE_FUN: return "ARR_TABLE_FUN"; |
279 |
|
case ARRAY_LAMBDA: return "ARRAY_LAMBDA"; |
280 |
|
case PARTIAL_SELECT_0: return "PARTIAL_SELECT_0"; |
281 |
|
case PARTIAL_SELECT_1: return "PARTIAL_SELECT_1"; |
282 |
|
|
283 |
|
/* from datatypes */ |
284 |
|
case CONSTRUCTOR_TYPE: return "CONSTRUCTOR_TYPE"; |
285 |
|
case SELECTOR_TYPE: return "SELECTOR_TYPE"; |
286 |
|
case TESTER_TYPE: return "TESTER_TYPE"; |
287 |
|
case UPDATER_TYPE: return "UPDATER_TYPE"; |
288 |
87 |
case APPLY_CONSTRUCTOR: return "APPLY_CONSTRUCTOR"; |
289 |
40 |
case APPLY_SELECTOR: return "APPLY_SELECTOR"; |
290 |
|
case APPLY_SELECTOR_TOTAL: return "APPLY_SELECTOR_TOTAL"; |
291 |
|
case APPLY_TESTER: return "APPLY_TESTER"; |
292 |
|
case APPLY_UPDATER: return "APPLY_UPDATER"; |
293 |
|
case DATATYPE_TYPE: return "DATATYPE_TYPE"; |
294 |
|
case PARAMETRIC_DATATYPE: return "PARAMETRIC_DATATYPE"; |
295 |
|
case APPLY_TYPE_ASCRIPTION: return "APPLY_TYPE_ASCRIPTION"; |
296 |
|
case ASCRIPTION_TYPE: return "ASCRIPTION_TYPE"; |
297 |
|
case DT_SIZE: return "DT_SIZE"; |
298 |
|
case DT_HEIGHT_BOUND: return "DT_HEIGHT_BOUND"; |
299 |
|
case DT_SIZE_BOUND: return "DT_SIZE_BOUND"; |
300 |
|
case DT_SYGUS_BOUND: return "DT_SYGUS_BOUND"; |
301 |
370 |
case DT_SYGUS_EVAL: return "DT_SYGUS_EVAL"; |
302 |
|
case MATCH: return "MATCH"; |
303 |
|
case MATCH_CASE: return "MATCH_CASE"; |
304 |
|
case MATCH_BIND_CASE: return "MATCH_BIND_CASE"; |
305 |
|
case TUPLE_PROJECT_OP: return "TUPLE_PROJECT_OP"; |
306 |
2 |
case TUPLE_PROJECT: return "TUPLE_PROJECT"; |
307 |
|
case CODATATYPE_BOUND_VARIABLE: return "CODATATYPE_BOUND_VARIABLE"; |
308 |
|
|
309 |
|
/* from sep */ |
310 |
|
case SEP_NIL: return "SEP_NIL"; |
311 |
|
case SEP_EMP: return "SEP_EMP"; |
312 |
|
case SEP_PTO: return "SEP_PTO"; |
313 |
|
case SEP_STAR: return "SEP_STAR"; |
314 |
|
case SEP_WAND: return "SEP_WAND"; |
315 |
|
case SEP_LABEL: return "SEP_LABEL"; |
316 |
|
|
317 |
|
/* from sets */ |
318 |
|
case EMPTYSET: return "EMPTYSET"; |
319 |
|
case SET_TYPE: return "SET_TYPE"; |
320 |
10 |
case UNION: return "UNION"; |
321 |
8 |
case INTERSECTION: return "INTERSECTION"; |
322 |
8 |
case SETMINUS: return "SETMINUS"; |
323 |
|
case SUBSET: return "SUBSET"; |
324 |
8 |
case MEMBER: return "MEMBER"; |
325 |
|
case SINGLETON_OP: return "SINGLETON_OP"; |
326 |
|
case SINGLETON: return "SINGLETON"; |
327 |
|
case INSERT: return "INSERT"; |
328 |
|
case CARD: return "CARD"; |
329 |
|
case COMPLEMENT: return "COMPLEMENT"; |
330 |
|
case UNIVERSE_SET: return "UNIVERSE_SET"; |
331 |
|
case COMPREHENSION: return "COMPREHENSION"; |
332 |
|
case CHOOSE: return "CHOOSE"; |
333 |
|
case IS_SINGLETON: return "IS_SINGLETON"; |
334 |
|
case JOIN: return "JOIN"; |
335 |
|
case PRODUCT: return "PRODUCT"; |
336 |
|
case TRANSPOSE: return "TRANSPOSE"; |
337 |
|
case TCLOSURE: return "TCLOSURE"; |
338 |
|
case JOIN_IMAGE: return "JOIN_IMAGE"; |
339 |
|
case IDEN: return "IDEN"; |
340 |
|
|
341 |
|
/* from bags */ |
342 |
|
case EMPTYBAG: return "EMPTYBAG"; |
343 |
|
case BAG_TYPE: return "BAG_TYPE"; |
344 |
|
case UNION_MAX: return "UNION_MAX"; |
345 |
|
case UNION_DISJOINT: return "UNION_DISJOINT"; |
346 |
|
case INTERSECTION_MIN: return "INTERSECTION_MIN"; |
347 |
|
case DIFFERENCE_SUBTRACT: return "DIFFERENCE_SUBTRACT"; |
348 |
|
case DIFFERENCE_REMOVE: return "DIFFERENCE_REMOVE"; |
349 |
|
case SUBBAG: return "SUBBAG"; |
350 |
|
case BAG_COUNT: return "BAG_COUNT"; |
351 |
|
case DUPLICATE_REMOVAL: return "DUPLICATE_REMOVAL"; |
352 |
|
case MK_BAG_OP: return "MK_BAG_OP"; |
353 |
|
case MK_BAG: return "MK_BAG"; |
354 |
|
case BAG_IS_SINGLETON: return "BAG_IS_SINGLETON"; |
355 |
|
case BAG_CARD: return "BAG_CARD"; |
356 |
|
case BAG_FROM_SET: return "BAG_FROM_SET"; |
357 |
|
case BAG_TO_SET: return "BAG_TO_SET"; |
358 |
|
case BAG_CHOOSE: return "BAG_CHOOSE"; |
359 |
2 |
case BAG_MAP: return "BAG_MAP"; |
360 |
|
|
361 |
|
/* from strings */ |
362 |
62 |
case STRING_CONCAT: return "STRING_CONCAT"; |
363 |
2 |
case STRING_IN_REGEXP: return "STRING_IN_REGEXP"; |
364 |
42 |
case STRING_LENGTH: return "STRING_LENGTH"; |
365 |
11 |
case STRING_SUBSTR: return "STRING_SUBSTR"; |
366 |
|
case STRING_UPDATE: return "STRING_UPDATE"; |
367 |
7 |
case STRING_CHARAT: return "STRING_CHARAT"; |
368 |
6 |
case STRING_CONTAINS: return "STRING_CONTAINS"; |
369 |
|
case STRING_LT: return "STRING_LT"; |
370 |
|
case STRING_LEQ: return "STRING_LEQ"; |
371 |
9 |
case STRING_INDEXOF: return "STRING_INDEXOF"; |
372 |
|
case STRING_INDEXOF_RE: return "STRING_INDEXOF_RE"; |
373 |
7 |
case STRING_REPLACE: return "STRING_REPLACE"; |
374 |
|
case STRING_REPLACE_ALL: return "STRING_REPLACE_ALL"; |
375 |
|
case STRING_REPLACE_RE: return "STRING_REPLACE_RE"; |
376 |
|
case STRING_REPLACE_RE_ALL: return "STRING_REPLACE_RE_ALL"; |
377 |
6 |
case STRING_PREFIX: return "STRING_PREFIX"; |
378 |
6 |
case STRING_SUFFIX: return "STRING_SUFFIX"; |
379 |
|
case STRING_IS_DIGIT: return "STRING_IS_DIGIT"; |
380 |
7 |
case STRING_ITOS: return "STRING_ITOS"; |
381 |
9 |
case STRING_STOI: return "STRING_STOI"; |
382 |
|
case STRING_TO_CODE: return "STRING_TO_CODE"; |
383 |
|
case STRING_FROM_CODE: return "STRING_FROM_CODE"; |
384 |
|
case STRING_TOLOWER: return "STRING_TOLOWER"; |
385 |
|
case STRING_TOUPPER: return "STRING_TOUPPER"; |
386 |
|
case STRING_REV: return "STRING_REV"; |
387 |
103 |
case CONST_STRING: return "CONST_STRING"; |
388 |
|
case SEQUENCE_TYPE: return "SEQUENCE_TYPE"; |
389 |
|
case CONST_SEQUENCE: return "CONST_SEQUENCE"; |
390 |
|
case SEQ_UNIT: return "SEQ_UNIT"; |
391 |
|
case SEQ_NTH: return "SEQ_NTH"; |
392 |
|
case SEQ_NTH_TOTAL: return "SEQ_NTH_TOTAL"; |
393 |
12 |
case STRING_TO_REGEXP: return "STRING_TO_REGEXP"; |
394 |
8 |
case REGEXP_CONCAT: return "REGEXP_CONCAT"; |
395 |
6 |
case REGEXP_UNION: return "REGEXP_UNION"; |
396 |
6 |
case REGEXP_INTER: return "REGEXP_INTER"; |
397 |
2 |
case REGEXP_DIFF: return "REGEXP_DIFF"; |
398 |
6 |
case REGEXP_STAR: return "REGEXP_STAR"; |
399 |
2 |
case REGEXP_PLUS: return "REGEXP_PLUS"; |
400 |
2 |
case REGEXP_OPT: return "REGEXP_OPT"; |
401 |
|
case REGEXP_RANGE: return "REGEXP_RANGE"; |
402 |
2 |
case REGEXP_COMPLEMENT: return "REGEXP_COMPLEMENT"; |
403 |
|
case REGEXP_EMPTY: return "REGEXP_EMPTY"; |
404 |
|
case REGEXP_SIGMA: return "REGEXP_SIGMA"; |
405 |
|
case REGEXP_REPEAT_OP: return "REGEXP_REPEAT_OP"; |
406 |
|
case REGEXP_REPEAT: return "REGEXP_REPEAT"; |
407 |
|
case REGEXP_LOOP_OP: return "REGEXP_LOOP_OP"; |
408 |
|
case REGEXP_LOOP: return "REGEXP_LOOP"; |
409 |
|
case REGEXP_RV: return "REGEXP_RV"; |
410 |
|
|
411 |
|
/* from quantifiers */ |
412 |
|
case FORALL: return "FORALL"; |
413 |
|
case EXISTS: return "EXISTS"; |
414 |
3873 |
case INST_CONSTANT: return "INST_CONSTANT"; |
415 |
|
case BOUND_VAR_LIST: return "BOUND_VAR_LIST"; |
416 |
|
case INST_PATTERN: return "INST_PATTERN"; |
417 |
|
case INST_NO_PATTERN: return "INST_NO_PATTERN"; |
418 |
|
case INST_ATTRIBUTE: return "INST_ATTRIBUTE"; |
419 |
|
case INST_POOL: return "INST_POOL"; |
420 |
|
case INST_ADD_TO_POOL: return "INST_ADD_TO_POOL"; |
421 |
|
case SKOLEM_ADD_TO_POOL: return "SKOLEM_ADD_TO_POOL"; |
422 |
|
case INST_PATTERN_LIST: return "INST_PATTERN_LIST"; |
423 |
|
|
424 |
|
// clang-format on |
425 |
4 |
case LAST_KIND: return "LAST_KIND"; |
426 |
2 |
default: return "?"; |
427 |
|
} |
428 |
|
} |
429 |
|
|
430 |
7859 |
std::ostream& operator<<(std::ostream& out, cvc5::Kind k) |
431 |
|
{ |
432 |
7859 |
out << toString(k); |
433 |
7859 |
return out; |
434 |
|
} |
435 |
|
|
436 |
|
/** Returns true if the given kind is associative. This is used by ExprManager to |
437 |
|
* decide whether it's safe to modify big expressions by changing the grouping of |
438 |
|
* the arguments. */ |
439 |
|
/* TODO: This could be generated. */ |
440 |
3140523 |
bool isAssociative(::cvc5::Kind k) |
441 |
|
{ |
442 |
3140523 |
switch(k) { |
443 |
1377324 |
case kind::AND: |
444 |
|
case kind::OR: |
445 |
|
case kind::MULT: |
446 |
|
case kind::PLUS: |
447 |
1377324 |
return true; |
448 |
|
|
449 |
1763199 |
default: |
450 |
1763199 |
return false; |
451 |
|
} |
452 |
|
} |
453 |
|
|
454 |
6742 |
std::string kindToString(::cvc5::Kind k) { return toString(k); } |
455 |
|
|
456 |
|
} // namespace kind |
457 |
|
|
458 |
|
const char* toString(TypeConstant tc) |
459 |
|
{ |
460 |
|
switch (tc) |
461 |
|
{ |
462 |
|
// clang-format off |
463 |
|
case BUILTIN_OPERATOR_TYPE: return "the type for built-in operators"; |
464 |
|
case SEXPR_TYPE: return "the type of a symbolic expression"; |
465 |
|
case BOOLEAN_TYPE: return "Boolean type"; |
466 |
|
case REAL_TYPE: return "real type"; |
467 |
|
case INTEGER_TYPE: return "integer type"; |
468 |
|
case ROUNDINGMODE_TYPE: return "floating-point rounding mode"; |
469 |
|
case STRING_TYPE: return "String type"; |
470 |
|
case REGEXP_TYPE: return "RegExp type"; |
471 |
|
case BOUND_VAR_LIST_TYPE: return "the type of bound variable lists"; |
472 |
|
case INST_PATTERN_TYPE: return "instantiation pattern type"; |
473 |
|
case INST_PATTERN_LIST_TYPE: return "the type of instantiation pattern lists"; |
474 |
|
|
475 |
|
// clang-format on |
476 |
|
default: return "UNKNOWN_TYPE_CONSTANT"; |
477 |
|
} |
478 |
|
} |
479 |
|
std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) |
480 |
|
{ |
481 |
|
return out << toString(typeConstant); |
482 |
|
} |
483 |
|
|
484 |
|
namespace theory { |
485 |
|
|
486 |
341555450 |
TheoryId kindToTheoryId(::cvc5::Kind k) |
487 |
|
{ |
488 |
341555450 |
switch (k) |
489 |
|
{ |
490 |
|
case kind::UNDEFINED_KIND: |
491 |
|
case kind::NULL_EXPR: |
492 |
|
break; |
493 |
|
// clang-format off |
494 |
|
case kind::SORT_TAG: return THEORY_BUILTIN; |
495 |
2483059 |
case kind::SORT_TYPE: return THEORY_BUILTIN; |
496 |
51741 |
case kind::UNINTERPRETED_CONSTANT: return THEORY_BUILTIN; |
497 |
|
case kind::ABSTRACT_VALUE: return THEORY_BUILTIN; |
498 |
|
case kind::BUILTIN: return THEORY_BUILTIN; |
499 |
1604132 |
case kind::EQUAL: return THEORY_BUILTIN; |
500 |
14124 |
case kind::DISTINCT: return THEORY_BUILTIN; |
501 |
4479331 |
case kind::VARIABLE: return THEORY_BUILTIN; |
502 |
11017788 |
case kind::BOUND_VARIABLE: return THEORY_BUILTIN; |
503 |
2416959 |
case kind::SKOLEM: return THEORY_BUILTIN; |
504 |
|
case kind::SEXPR: return THEORY_BUILTIN; |
505 |
15821 |
case kind::LAMBDA: return THEORY_BUILTIN; |
506 |
11981 |
case kind::WITNESS: return THEORY_BUILTIN; |
507 |
|
case kind::TYPE_CONSTANT: return THEORY_BUILTIN; |
508 |
54680 |
case kind::FUNCTION_TYPE: return THEORY_BUILTIN; |
509 |
8673508 |
case kind::CONST_BOOLEAN: return THEORY_BOOL; |
510 |
27924129 |
case kind::NOT: return THEORY_BOOL; |
511 |
12484053 |
case kind::AND: return THEORY_BOOL; |
512 |
1622051 |
case kind::IMPLIES: return THEORY_BOOL; |
513 |
21473862 |
case kind::OR: return THEORY_BOOL; |
514 |
3309666 |
case kind::XOR: return THEORY_BOOL; |
515 |
8115555 |
case kind::ITE: return THEORY_BOOL; |
516 |
33167288 |
case kind::APPLY_UF: return THEORY_UF; |
517 |
215539 |
case kind::BOOLEAN_TERM_VARIABLE: return THEORY_UF; |
518 |
|
case kind::PARTIAL_APPLY_UF: return THEORY_UF; |
519 |
68078 |
case kind::HO_APPLY: return THEORY_UF; |
520 |
|
case kind::CARDINALITY_CONSTRAINT_OP: return THEORY_UF; |
521 |
31601 |
case kind::CARDINALITY_CONSTRAINT: return THEORY_UF; |
522 |
|
case kind::COMBINED_CARDINALITY_CONSTRAINT_OP: return THEORY_UF; |
523 |
17305 |
case kind::COMBINED_CARDINALITY_CONSTRAINT: return THEORY_UF; |
524 |
41498265 |
case kind::PLUS: return THEORY_ARITH; |
525 |
6255588 |
case kind::MULT: return THEORY_ARITH; |
526 |
6804605 |
case kind::NONLINEAR_MULT: return THEORY_ARITH; |
527 |
715832 |
case kind::MINUS: return THEORY_ARITH; |
528 |
69842 |
case kind::UMINUS: return THEORY_ARITH; |
529 |
9812 |
case kind::DIVISION: return THEORY_ARITH; |
530 |
1939 |
case kind::DIVISION_TOTAL: return THEORY_ARITH; |
531 |
4098 |
case kind::INTS_DIVISION: return THEORY_ARITH; |
532 |
12318 |
case kind::INTS_DIVISION_TOTAL: return THEORY_ARITH; |
533 |
2193 |
case kind::INTS_MODULUS: return THEORY_ARITH; |
534 |
28203 |
case kind::INTS_MODULUS_TOTAL: return THEORY_ARITH; |
535 |
301 |
case kind::ABS: return THEORY_ARITH; |
536 |
|
case kind::DIVISIBLE: return THEORY_ARITH; |
537 |
487 |
case kind::POW: return THEORY_ARITH; |
538 |
3838 |
case kind::POW2: return THEORY_ARITH; |
539 |
21473 |
case kind::EXPONENTIAL: return THEORY_ARITH; |
540 |
113249 |
case kind::SINE: return THEORY_ARITH; |
541 |
378 |
case kind::COSINE: return THEORY_ARITH; |
542 |
48 |
case kind::TANGENT: return THEORY_ARITH; |
543 |
12 |
case kind::COSECANT: return THEORY_ARITH; |
544 |
12 |
case kind::SECANT: return THEORY_ARITH; |
545 |
24 |
case kind::COTANGENT: return THEORY_ARITH; |
546 |
36 |
case kind::ARCSINE: return THEORY_ARITH; |
547 |
36 |
case kind::ARCCOSINE: return THEORY_ARITH; |
548 |
103 |
case kind::ARCTANGENT: return THEORY_ARITH; |
549 |
|
case kind::ARCCOSECANT: return THEORY_ARITH; |
550 |
|
case kind::ARCSECANT: return THEORY_ARITH; |
551 |
|
case kind::ARCCOTANGENT: return THEORY_ARITH; |
552 |
553 |
case kind::SQRT: return THEORY_ARITH; |
553 |
|
case kind::DIVISIBLE_OP: return THEORY_ARITH; |
554 |
16105052 |
case kind::CONST_RATIONAL: return THEORY_ARITH; |
555 |
377175 |
case kind::LT: return THEORY_ARITH; |
556 |
851894 |
case kind::LEQ: return THEORY_ARITH; |
557 |
184870 |
case kind::GT: return THEORY_ARITH; |
558 |
22452017 |
case kind::GEQ: return THEORY_ARITH; |
559 |
|
case kind::INDEXED_ROOT_PREDICATE_OP: return THEORY_ARITH; |
560 |
|
case kind::INDEXED_ROOT_PREDICATE: return THEORY_ARITH; |
561 |
559 |
case kind::IS_INTEGER: return THEORY_ARITH; |
562 |
6677 |
case kind::TO_INTEGER: return THEORY_ARITH; |
563 |
97 |
case kind::TO_REAL: return THEORY_ARITH; |
564 |
20739 |
case kind::CAST_TO_REAL: return THEORY_ARITH; |
565 |
40357 |
case kind::PI: return THEORY_ARITH; |
566 |
|
case kind::IAND_OP: return THEORY_ARITH; |
567 |
19402 |
case kind::IAND: return THEORY_ARITH; |
568 |
8436086 |
case kind::BITVECTOR_TYPE: return THEORY_BV; |
569 |
5452096 |
case kind::CONST_BITVECTOR: return THEORY_BV; |
570 |
|
case kind::BITVECTOR_BB_TERM: return THEORY_BV; |
571 |
1208023 |
case kind::BITVECTOR_CONCAT: return THEORY_BV; |
572 |
670343 |
case kind::BITVECTOR_AND: return THEORY_BV; |
573 |
873439 |
case kind::BITVECTOR_COMP: return THEORY_BV; |
574 |
955115 |
case kind::BITVECTOR_OR: return THEORY_BV; |
575 |
47872 |
case kind::BITVECTOR_XOR: return THEORY_BV; |
576 |
603164 |
case kind::BITVECTOR_NOT: return THEORY_BV; |
577 |
1510 |
case kind::BITVECTOR_NAND: return THEORY_BV; |
578 |
1964 |
case kind::BITVECTOR_NOR: return THEORY_BV; |
579 |
2084 |
case kind::BITVECTOR_XNOR: return THEORY_BV; |
580 |
1015645 |
case kind::BITVECTOR_MULT: return THEORY_BV; |
581 |
290100 |
case kind::BITVECTOR_NEG: return THEORY_BV; |
582 |
692123 |
case kind::BITVECTOR_ADD: return THEORY_BV; |
583 |
7416 |
case kind::BITVECTOR_SUB: return THEORY_BV; |
584 |
139936 |
case kind::BITVECTOR_UDIV: return THEORY_BV; |
585 |
154436 |
case kind::BITVECTOR_UREM: return THEORY_BV; |
586 |
376 |
case kind::BITVECTOR_SDIV: return THEORY_BV; |
587 |
308 |
case kind::BITVECTOR_SMOD: return THEORY_BV; |
588 |
190 |
case kind::BITVECTOR_SREM: return THEORY_BV; |
589 |
56115 |
case kind::BITVECTOR_ASHR: return THEORY_BV; |
590 |
260977 |
case kind::BITVECTOR_LSHR: return THEORY_BV; |
591 |
247864 |
case kind::BITVECTOR_SHL: return THEORY_BV; |
592 |
7461 |
case kind::BITVECTOR_ULE: return THEORY_BV; |
593 |
930724 |
case kind::BITVECTOR_ULT: return THEORY_BV; |
594 |
3980 |
case kind::BITVECTOR_UGE: return THEORY_BV; |
595 |
4459 |
case kind::BITVECTOR_UGT: return THEORY_BV; |
596 |
7795 |
case kind::BITVECTOR_SLE: return THEORY_BV; |
597 |
1066282 |
case kind::BITVECTOR_SLT: return THEORY_BV; |
598 |
4157 |
case kind::BITVECTOR_SGE: return THEORY_BV; |
599 |
4691 |
case kind::BITVECTOR_SGT: return THEORY_BV; |
600 |
37222 |
case kind::BITVECTOR_ULTBV: return THEORY_BV; |
601 |
48144 |
case kind::BITVECTOR_SLTBV: return THEORY_BV; |
602 |
|
case kind::BITVECTOR_REDAND: return THEORY_BV; |
603 |
|
case kind::BITVECTOR_REDOR: return THEORY_BV; |
604 |
196875 |
case kind::BITVECTOR_ITE: return THEORY_BV; |
605 |
11401 |
case kind::BITVECTOR_TO_NAT: return THEORY_BV; |
606 |
|
case kind::BITVECTOR_ACKERMANNIZE_UDIV: return THEORY_BV; |
607 |
|
case kind::BITVECTOR_ACKERMANNIZE_UREM: return THEORY_BV; |
608 |
4594 |
case kind::BITVECTOR_EAGER_ATOM: return THEORY_BV; |
609 |
|
case kind::BITVECTOR_BITOF_OP: return THEORY_BV; |
610 |
4879133 |
case kind::BITVECTOR_BITOF: return THEORY_BV; |
611 |
|
case kind::BITVECTOR_EXTRACT_OP: return THEORY_BV; |
612 |
662148 |
case kind::BITVECTOR_EXTRACT: return THEORY_BV; |
613 |
|
case kind::BITVECTOR_REPEAT_OP: return THEORY_BV; |
614 |
1807 |
case kind::BITVECTOR_REPEAT: return THEORY_BV; |
615 |
|
case kind::BITVECTOR_ROTATE_LEFT_OP: return THEORY_BV; |
616 |
1504 |
case kind::BITVECTOR_ROTATE_LEFT: return THEORY_BV; |
617 |
|
case kind::BITVECTOR_ROTATE_RIGHT_OP: return THEORY_BV; |
618 |
2014 |
case kind::BITVECTOR_ROTATE_RIGHT: return THEORY_BV; |
619 |
|
case kind::BITVECTOR_SIGN_EXTEND_OP: return THEORY_BV; |
620 |
251362 |
case kind::BITVECTOR_SIGN_EXTEND: return THEORY_BV; |
621 |
|
case kind::BITVECTOR_ZERO_EXTEND_OP: return THEORY_BV; |
622 |
17431 |
case kind::BITVECTOR_ZERO_EXTEND: return THEORY_BV; |
623 |
|
case kind::INT_TO_BITVECTOR_OP: return THEORY_BV; |
624 |
2047 |
case kind::INT_TO_BITVECTOR: return THEORY_BV; |
625 |
27391 |
case kind::CONST_FLOATINGPOINT: return THEORY_FP; |
626 |
6404 |
case kind::CONST_ROUNDINGMODE: return THEORY_FP; |
627 |
64634 |
case kind::FLOATINGPOINT_TYPE: return THEORY_FP; |
628 |
435 |
case kind::FLOATINGPOINT_FP: return THEORY_FP; |
629 |
21 |
case kind::FLOATINGPOINT_EQ: return THEORY_FP; |
630 |
1546 |
case kind::FLOATINGPOINT_ABS: return THEORY_FP; |
631 |
3265 |
case kind::FLOATINGPOINT_NEG: return THEORY_FP; |
632 |
7980 |
case kind::FLOATINGPOINT_ADD: return THEORY_FP; |
633 |
43 |
case kind::FLOATINGPOINT_SUB: return THEORY_FP; |
634 |
1662 |
case kind::FLOATINGPOINT_MULT: return THEORY_FP; |
635 |
1400 |
case kind::FLOATINGPOINT_DIV: return THEORY_FP; |
636 |
|
case kind::FLOATINGPOINT_FMA: return THEORY_FP; |
637 |
184 |
case kind::FLOATINGPOINT_SQRT: return THEORY_FP; |
638 |
1266 |
case kind::FLOATINGPOINT_REM: return THEORY_FP; |
639 |
1502 |
case kind::FLOATINGPOINT_RTI: return THEORY_FP; |
640 |
|
case kind::FLOATINGPOINT_MIN: return THEORY_FP; |
641 |
14 |
case kind::FLOATINGPOINT_MAX: return THEORY_FP; |
642 |
|
case kind::FLOATINGPOINT_MIN_TOTAL: return THEORY_FP; |
643 |
1998 |
case kind::FLOATINGPOINT_MAX_TOTAL: return THEORY_FP; |
644 |
13523 |
case kind::FLOATINGPOINT_LEQ: return THEORY_FP; |
645 |
501 |
case kind::FLOATINGPOINT_LT: return THEORY_FP; |
646 |
95 |
case kind::FLOATINGPOINT_GEQ: return THEORY_FP; |
647 |
4 |
case kind::FLOATINGPOINT_GT: return THEORY_FP; |
648 |
140 |
case kind::FLOATINGPOINT_ISN: return THEORY_FP; |
649 |
226 |
case kind::FLOATINGPOINT_ISSN: return THEORY_FP; |
650 |
1752 |
case kind::FLOATINGPOINT_ISZ: return THEORY_FP; |
651 |
3077 |
case kind::FLOATINGPOINT_ISINF: return THEORY_FP; |
652 |
1388 |
case kind::FLOATINGPOINT_ISNAN: return THEORY_FP; |
653 |
2815 |
case kind::FLOATINGPOINT_ISNEG: return THEORY_FP; |
654 |
264 |
case kind::FLOATINGPOINT_ISPOS: return THEORY_FP; |
655 |
|
case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: return THEORY_FP; |
656 |
2393 |
case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: return THEORY_FP; |
657 |
|
case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: return THEORY_FP; |
658 |
177 |
case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: return THEORY_FP; |
659 |
|
case kind::FLOATINGPOINT_TO_FP_REAL_OP: return THEORY_FP; |
660 |
1222 |
case kind::FLOATINGPOINT_TO_FP_REAL: return THEORY_FP; |
661 |
|
case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: return THEORY_FP; |
662 |
16 |
case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: return THEORY_FP; |
663 |
|
case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP: return THEORY_FP; |
664 |
566 |
case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: return THEORY_FP; |
665 |
|
case kind::FLOATINGPOINT_TO_FP_GENERIC_OP: return THEORY_FP; |
666 |
329 |
case kind::FLOATINGPOINT_TO_FP_GENERIC: return THEORY_FP; |
667 |
|
case kind::FLOATINGPOINT_TO_UBV_OP: return THEORY_FP; |
668 |
|
case kind::FLOATINGPOINT_TO_UBV: return THEORY_FP; |
669 |
|
case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP: return THEORY_FP; |
670 |
|
case kind::FLOATINGPOINT_TO_UBV_TOTAL: return THEORY_FP; |
671 |
|
case kind::FLOATINGPOINT_TO_SBV_OP: return THEORY_FP; |
672 |
44 |
case kind::FLOATINGPOINT_TO_SBV: return THEORY_FP; |
673 |
|
case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP: return THEORY_FP; |
674 |
1384 |
case kind::FLOATINGPOINT_TO_SBV_TOTAL: return THEORY_FP; |
675 |
974 |
case kind::FLOATINGPOINT_TO_REAL: return THEORY_FP; |
676 |
4025 |
case kind::FLOATINGPOINT_TO_REAL_TOTAL: return THEORY_FP; |
677 |
13840 |
case kind::FLOATINGPOINT_COMPONENT_NAN: return THEORY_FP; |
678 |
15026 |
case kind::FLOATINGPOINT_COMPONENT_INF: return THEORY_FP; |
679 |
13986 |
case kind::FLOATINGPOINT_COMPONENT_ZERO: return THEORY_FP; |
680 |
14127 |
case kind::FLOATINGPOINT_COMPONENT_SIGN: return THEORY_FP; |
681 |
22360 |
case kind::FLOATINGPOINT_COMPONENT_EXPONENT: return THEORY_FP; |
682 |
28039 |
case kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND: return THEORY_FP; |
683 |
696 |
case kind::ROUNDINGMODE_BITBLAST: return THEORY_FP; |
684 |
324784 |
case kind::ARRAY_TYPE: return THEORY_ARRAYS; |
685 |
1242341 |
case kind::SELECT: return THEORY_ARRAYS; |
686 |
470098 |
case kind::STORE: return THEORY_ARRAYS; |
687 |
537 |
case kind::EQ_RANGE: return THEORY_ARRAYS; |
688 |
11693 |
case kind::STORE_ALL: return THEORY_ARRAYS; |
689 |
|
case kind::ARR_TABLE_FUN: return THEORY_ARRAYS; |
690 |
|
case kind::ARRAY_LAMBDA: return THEORY_ARRAYS; |
691 |
|
case kind::PARTIAL_SELECT_0: return THEORY_ARRAYS; |
692 |
|
case kind::PARTIAL_SELECT_1: return THEORY_ARRAYS; |
693 |
|
case kind::CONSTRUCTOR_TYPE: return THEORY_DATATYPES; |
694 |
|
case kind::SELECTOR_TYPE: return THEORY_DATATYPES; |
695 |
|
case kind::TESTER_TYPE: return THEORY_DATATYPES; |
696 |
|
case kind::UPDATER_TYPE: return THEORY_DATATYPES; |
697 |
2799156 |
case kind::APPLY_CONSTRUCTOR: return THEORY_DATATYPES; |
698 |
225028 |
case kind::APPLY_SELECTOR: return THEORY_DATATYPES; |
699 |
3757682 |
case kind::APPLY_SELECTOR_TOTAL: return THEORY_DATATYPES; |
700 |
3751076 |
case kind::APPLY_TESTER: return THEORY_DATATYPES; |
701 |
303 |
case kind::APPLY_UPDATER: return THEORY_DATATYPES; |
702 |
3456014 |
case kind::DATATYPE_TYPE: return THEORY_DATATYPES; |
703 |
12146 |
case kind::PARAMETRIC_DATATYPE: return THEORY_DATATYPES; |
704 |
|
case kind::APPLY_TYPE_ASCRIPTION: return THEORY_DATATYPES; |
705 |
|
case kind::ASCRIPTION_TYPE: return THEORY_DATATYPES; |
706 |
6363741 |
case kind::DT_SIZE: return THEORY_DATATYPES; |
707 |
|
case kind::DT_HEIGHT_BOUND: return THEORY_DATATYPES; |
708 |
|
case kind::DT_SIZE_BOUND: return THEORY_DATATYPES; |
709 |
118487 |
case kind::DT_SYGUS_BOUND: return THEORY_DATATYPES; |
710 |
10523535 |
case kind::DT_SYGUS_EVAL: return THEORY_DATATYPES; |
711 |
36 |
case kind::MATCH: return THEORY_DATATYPES; |
712 |
80 |
case kind::MATCH_CASE: return THEORY_DATATYPES; |
713 |
32 |
case kind::MATCH_BIND_CASE: return THEORY_DATATYPES; |
714 |
|
case kind::TUPLE_PROJECT_OP: return THEORY_DATATYPES; |
715 |
18 |
case kind::TUPLE_PROJECT: return THEORY_DATATYPES; |
716 |
45 |
case kind::CODATATYPE_BOUND_VARIABLE: return THEORY_DATATYPES; |
717 |
5752 |
case kind::SEP_NIL: return THEORY_SEP; |
718 |
602 |
case kind::SEP_EMP: return THEORY_SEP; |
719 |
9725 |
case kind::SEP_PTO: return THEORY_SEP; |
720 |
5412 |
case kind::SEP_STAR: return THEORY_SEP; |
721 |
754 |
case kind::SEP_WAND: return THEORY_SEP; |
722 |
20420 |
case kind::SEP_LABEL: return THEORY_SEP; |
723 |
22963 |
case kind::EMPTYSET: return THEORY_SETS; |
724 |
943107 |
case kind::SET_TYPE: return THEORY_SETS; |
725 |
111693 |
case kind::UNION: return THEORY_SETS; |
726 |
101275 |
case kind::INTERSECTION: return THEORY_SETS; |
727 |
72223 |
case kind::SETMINUS: return THEORY_SETS; |
728 |
3574 |
case kind::SUBSET: return THEORY_SETS; |
729 |
1373813 |
case kind::MEMBER: return THEORY_SETS; |
730 |
|
case kind::SINGLETON_OP: return THEORY_SETS; |
731 |
175192 |
case kind::SINGLETON: return THEORY_SETS; |
732 |
47 |
case kind::INSERT: return THEORY_SETS; |
733 |
1995596 |
case kind::CARD: return THEORY_SETS; |
734 |
73 |
case kind::COMPLEMENT: return THEORY_SETS; |
735 |
6026 |
case kind::UNIVERSE_SET: return THEORY_SETS; |
736 |
901 |
case kind::COMPREHENSION: return THEORY_SETS; |
737 |
1102 |
case kind::CHOOSE: return THEORY_SETS; |
738 |
448 |
case kind::IS_SINGLETON: return THEORY_SETS; |
739 |
40659 |
case kind::JOIN: return THEORY_SETS; |
740 |
3544 |
case kind::PRODUCT: return THEORY_SETS; |
741 |
19650 |
case kind::TRANSPOSE: return THEORY_SETS; |
742 |
4798 |
case kind::TCLOSURE: return THEORY_SETS; |
743 |
1435 |
case kind::JOIN_IMAGE: return THEORY_SETS; |
744 |
309 |
case kind::IDEN: return THEORY_SETS; |
745 |
704 |
case kind::EMPTYBAG: return THEORY_BAGS; |
746 |
28434 |
case kind::BAG_TYPE: return THEORY_BAGS; |
747 |
799 |
case kind::UNION_MAX: return THEORY_BAGS; |
748 |
2951 |
case kind::UNION_DISJOINT: return THEORY_BAGS; |
749 |
1661 |
case kind::INTERSECTION_MIN: return THEORY_BAGS; |
750 |
624 |
case kind::DIFFERENCE_SUBTRACT: return THEORY_BAGS; |
751 |
1362 |
case kind::DIFFERENCE_REMOVE: return THEORY_BAGS; |
752 |
28 |
case kind::SUBBAG: return THEORY_BAGS; |
753 |
784963 |
case kind::BAG_COUNT: return THEORY_BAGS; |
754 |
657 |
case kind::DUPLICATE_REMOVAL: return THEORY_BAGS; |
755 |
|
case kind::MK_BAG_OP: return THEORY_BAGS; |
756 |
9866 |
case kind::MK_BAG: return THEORY_BAGS; |
757 |
|
case kind::BAG_IS_SINGLETON: return THEORY_BAGS; |
758 |
|
case kind::BAG_CARD: return THEORY_BAGS; |
759 |
|
case kind::BAG_FROM_SET: return THEORY_BAGS; |
760 |
|
case kind::BAG_TO_SET: return THEORY_BAGS; |
761 |
|
case kind::BAG_CHOOSE: return THEORY_BAGS; |
762 |
333 |
case kind::BAG_MAP: return THEORY_BAGS; |
763 |
1133451 |
case kind::STRING_CONCAT: return THEORY_STRINGS; |
764 |
361306 |
case kind::STRING_IN_REGEXP: return THEORY_STRINGS; |
765 |
28913900 |
case kind::STRING_LENGTH: return THEORY_STRINGS; |
766 |
904598 |
case kind::STRING_SUBSTR: return THEORY_STRINGS; |
767 |
2456 |
case kind::STRING_UPDATE: return THEORY_STRINGS; |
768 |
607 |
case kind::STRING_CHARAT: return THEORY_STRINGS; |
769 |
211898 |
case kind::STRING_CONTAINS: return THEORY_STRINGS; |
770 |
99 |
case kind::STRING_LT: return THEORY_STRINGS; |
771 |
7405 |
case kind::STRING_LEQ: return THEORY_STRINGS; |
772 |
450632 |
case kind::STRING_INDEXOF: return THEORY_STRINGS; |
773 |
194987 |
case kind::STRING_INDEXOF_RE: return THEORY_STRINGS; |
774 |
190949 |
case kind::STRING_REPLACE: return THEORY_STRINGS; |
775 |
5862 |
case kind::STRING_REPLACE_ALL: return THEORY_STRINGS; |
776 |
18545 |
case kind::STRING_REPLACE_RE: return THEORY_STRINGS; |
777 |
8971 |
case kind::STRING_REPLACE_RE_ALL: return THEORY_STRINGS; |
778 |
573 |
case kind::STRING_PREFIX: return THEORY_STRINGS; |
779 |
155 |
case kind::STRING_SUFFIX: return THEORY_STRINGS; |
780 |
26 |
case kind::STRING_IS_DIGIT: return THEORY_STRINGS; |
781 |
18365 |
case kind::STRING_ITOS: return THEORY_STRINGS; |
782 |
153200 |
case kind::STRING_STOI: return THEORY_STRINGS; |
783 |
2719847 |
case kind::STRING_TO_CODE: return THEORY_STRINGS; |
784 |
967 |
case kind::STRING_FROM_CODE: return THEORY_STRINGS; |
785 |
1806 |
case kind::STRING_TOLOWER: return THEORY_STRINGS; |
786 |
958 |
case kind::STRING_TOUPPER: return THEORY_STRINGS; |
787 |
2164 |
case kind::STRING_REV: return THEORY_STRINGS; |
788 |
911541 |
case kind::CONST_STRING: return THEORY_STRINGS; |
789 |
61327 |
case kind::SEQUENCE_TYPE: return THEORY_STRINGS; |
790 |
11639 |
case kind::CONST_SEQUENCE: return THEORY_STRINGS; |
791 |
7022 |
case kind::SEQ_UNIT: return THEORY_STRINGS; |
792 |
40893 |
case kind::SEQ_NTH: return THEORY_STRINGS; |
793 |
22 |
case kind::SEQ_NTH_TOTAL: return THEORY_STRINGS; |
794 |
69297 |
case kind::STRING_TO_REGEXP: return THEORY_STRINGS; |
795 |
59720 |
case kind::REGEXP_CONCAT: return THEORY_STRINGS; |
796 |
19859 |
case kind::REGEXP_UNION: return THEORY_STRINGS; |
797 |
7626 |
case kind::REGEXP_INTER: return THEORY_STRINGS; |
798 |
345 |
case kind::REGEXP_DIFF: return THEORY_STRINGS; |
799 |
42387 |
case kind::REGEXP_STAR: return THEORY_STRINGS; |
800 |
173 |
case kind::REGEXP_PLUS: return THEORY_STRINGS; |
801 |
124 |
case kind::REGEXP_OPT: return THEORY_STRINGS; |
802 |
12692 |
case kind::REGEXP_RANGE: return THEORY_STRINGS; |
803 |
7425 |
case kind::REGEXP_COMPLEMENT: return THEORY_STRINGS; |
804 |
1544 |
case kind::REGEXP_EMPTY: return THEORY_STRINGS; |
805 |
8314 |
case kind::REGEXP_SIGMA: return THEORY_STRINGS; |
806 |
|
case kind::REGEXP_REPEAT_OP: return THEORY_STRINGS; |
807 |
14 |
case kind::REGEXP_REPEAT: return THEORY_STRINGS; |
808 |
|
case kind::REGEXP_LOOP_OP: return THEORY_STRINGS; |
809 |
100 |
case kind::REGEXP_LOOP: return THEORY_STRINGS; |
810 |
804 |
case kind::REGEXP_RV: return THEORY_STRINGS; |
811 |
1282331 |
case kind::FORALL: return THEORY_QUANTIFIERS; |
812 |
10073 |
case kind::EXISTS: return THEORY_QUANTIFIERS; |
813 |
130834 |
case kind::INST_CONSTANT: return THEORY_QUANTIFIERS; |
814 |
305008 |
case kind::BOUND_VAR_LIST: return THEORY_QUANTIFIERS; |
815 |
19348 |
case kind::INST_PATTERN: return THEORY_QUANTIFIERS; |
816 |
32 |
case kind::INST_NO_PATTERN: return THEORY_QUANTIFIERS; |
817 |
7919 |
case kind::INST_ATTRIBUTE: return THEORY_QUANTIFIERS; |
818 |
52 |
case kind::INST_POOL: return THEORY_QUANTIFIERS; |
819 |
|
case kind::INST_ADD_TO_POOL: return THEORY_QUANTIFIERS; |
820 |
64 |
case kind::SKOLEM_ADD_TO_POOL: return THEORY_QUANTIFIERS; |
821 |
43405 |
case kind::INST_PATTERN_LIST: return THEORY_QUANTIFIERS; |
822 |
|
|
823 |
|
// clang-format on |
824 |
|
case kind::LAST_KIND: break; |
825 |
|
} |
826 |
|
throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind"); |
827 |
|
} |
828 |
|
|
829 |
44875198 |
TheoryId typeConstantToTheoryId(::cvc5::TypeConstant typeConstant) |
830 |
|
{ |
831 |
44875198 |
switch (typeConstant) |
832 |
|
{ |
833 |
|
// clang-format off |
834 |
|
case BUILTIN_OPERATOR_TYPE: return THEORY_BUILTIN; |
835 |
|
case SEXPR_TYPE: return THEORY_BUILTIN; |
836 |
4980699 |
case BOOLEAN_TYPE: return THEORY_BOOL; |
837 |
3173129 |
case REAL_TYPE: return THEORY_ARITH; |
838 |
32222102 |
case INTEGER_TYPE: return THEORY_ARITH; |
839 |
2637 |
case ROUNDINGMODE_TYPE: return THEORY_FP; |
840 |
4496588 |
case STRING_TYPE: return THEORY_STRINGS; |
841 |
43 |
case REGEXP_TYPE: return THEORY_STRINGS; |
842 |
|
case BOUND_VAR_LIST_TYPE: return THEORY_QUANTIFIERS; |
843 |
|
case INST_PATTERN_TYPE: return THEORY_QUANTIFIERS; |
844 |
|
case INST_PATTERN_LIST_TYPE: return THEORY_QUANTIFIERS; |
845 |
|
|
846 |
|
// clang-format on |
847 |
|
case LAST_TYPE: break; |
848 |
|
} |
849 |
|
throw IllegalArgumentException( |
850 |
|
"", "k", __PRETTY_FUNCTION__, "bad type constant"); |
851 |
|
} |
852 |
|
|
853 |
|
} // namespace theory |
854 |
|
} // namespace cvc5 |