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-05-22/src/expr/kind_template.cpp /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/builtin/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/booleans/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/uf/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/arith/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/bv/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/fp/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/arrays/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/datatypes/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/sep/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/sets/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/bags/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/strings/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/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-05-22/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 |
7888 |
const char* toString(cvc5::Kind k) |
60 |
|
{ |
61 |
|
using namespace cvc5::kind; |
62 |
|
|
63 |
7888 |
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 |
468 |
case EQUAL: return "EQUAL"; |
77 |
4 |
case DISTINCT: return "DISTINCT"; |
78 |
22 |
case VARIABLE: return "VARIABLE"; |
79 |
661 |
case BOUND_VARIABLE: return "BOUND_VARIABLE"; |
80 |
|
case SKOLEM: return "SKOLEM"; |
81 |
4 |
case SEXPR: return "SEXPR"; |
82 |
12 |
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 |
51 |
case CONST_BOOLEAN: return "CONST_BOOLEAN"; |
89 |
399 |
case NOT: return "NOT"; |
90 |
440 |
case AND: return "AND"; |
91 |
2 |
case IMPLIES: return "IMPLIES"; |
92 |
429 |
case OR: return "OR"; |
93 |
20 |
case XOR: return "XOR"; |
94 |
517 |
case ITE: return "ITE"; |
95 |
|
|
96 |
|
/* from uf */ |
97 |
79 |
case APPLY_UF: return "APPLY_UF"; |
98 |
6 |
case BOOLEAN_TERM_VARIABLE: return "BOOLEAN_TERM_VARIABLE"; |
99 |
|
case CARDINALITY_CONSTRAINT: return "CARDINALITY_CONSTRAINT"; |
100 |
|
case COMBINED_CARDINALITY_CONSTRAINT: return "COMBINED_CARDINALITY_CONSTRAINT"; |
101 |
|
case PARTIAL_APPLY_UF: return "PARTIAL_APPLY_UF"; |
102 |
|
case CARDINALITY_VALUE: return "CARDINALITY_VALUE"; |
103 |
|
case HO_APPLY: return "HO_APPLY"; |
104 |
|
|
105 |
|
/* from arith */ |
106 |
444 |
case PLUS: return "PLUS"; |
107 |
5 |
case MULT: return "MULT"; |
108 |
|
case NONLINEAR_MULT: return "NONLINEAR_MULT"; |
109 |
373 |
case MINUS: return "MINUS"; |
110 |
6 |
case UMINUS: return "UMINUS"; |
111 |
39 |
case DIVISION: return "DIVISION"; |
112 |
|
case DIVISION_TOTAL: return "DIVISION_TOTAL"; |
113 |
1 |
case INTS_DIVISION: return "INTS_DIVISION"; |
114 |
|
case INTS_DIVISION_TOTAL: return "INTS_DIVISION_TOTAL"; |
115 |
2 |
case INTS_MODULUS: return "INTS_MODULUS"; |
116 |
|
case INTS_MODULUS_TOTAL: return "INTS_MODULUS_TOTAL"; |
117 |
|
case ABS: return "ABS"; |
118 |
16 |
case DIVISIBLE: return "DIVISIBLE"; |
119 |
|
case POW: return "POW"; |
120 |
|
case EXPONENTIAL: return "EXPONENTIAL"; |
121 |
|
case SINE: return "SINE"; |
122 |
|
case COSINE: return "COSINE"; |
123 |
|
case TANGENT: return "TANGENT"; |
124 |
|
case COSECANT: return "COSECANT"; |
125 |
|
case SECANT: return "SECANT"; |
126 |
|
case COTANGENT: return "COTANGENT"; |
127 |
|
case ARCSINE: return "ARCSINE"; |
128 |
|
case ARCCOSINE: return "ARCCOSINE"; |
129 |
|
case ARCTANGENT: return "ARCTANGENT"; |
130 |
|
case ARCCOSECANT: return "ARCCOSECANT"; |
131 |
|
case ARCSECANT: return "ARCSECANT"; |
132 |
|
case ARCCOTANGENT: return "ARCCOTANGENT"; |
133 |
|
case SQRT: return "SQRT"; |
134 |
|
case DIVISIBLE_OP: return "DIVISIBLE_OP"; |
135 |
229 |
case CONST_RATIONAL: return "CONST_RATIONAL"; |
136 |
18 |
case LT: return "LT"; |
137 |
370 |
case LEQ: return "LEQ"; |
138 |
14 |
case GT: return "GT"; |
139 |
20 |
case GEQ: return "GEQ"; |
140 |
|
case INDEXED_ROOT_PREDICATE_OP: return "INDEXED_ROOT_PREDICATE_OP"; |
141 |
|
case INDEXED_ROOT_PREDICATE: return "INDEXED_ROOT_PREDICATE"; |
142 |
|
case IS_INTEGER: return "IS_INTEGER"; |
143 |
|
case TO_INTEGER: return "TO_INTEGER"; |
144 |
|
case TO_REAL: return "TO_REAL"; |
145 |
|
case CAST_TO_REAL: return "CAST_TO_REAL"; |
146 |
|
case PI: return "PI"; |
147 |
|
case IAND_OP: return "IAND_OP"; |
148 |
|
case IAND: return "IAND"; |
149 |
|
|
150 |
|
/* from bv */ |
151 |
|
case BITVECTOR_TYPE: return "BITVECTOR_TYPE"; |
152 |
56 |
case CONST_BITVECTOR: return "CONST_BITVECTOR"; |
153 |
|
case BITVECTOR_BB_TERM: return "BITVECTOR_BB_TERM"; |
154 |
1 |
case BITVECTOR_CONCAT: return "BITVECTOR_CONCAT"; |
155 |
62 |
case BITVECTOR_AND: return "BITVECTOR_AND"; |
156 |
14 |
case BITVECTOR_COMP: return "BITVECTOR_COMP"; |
157 |
84 |
case BITVECTOR_OR: return "BITVECTOR_OR"; |
158 |
53 |
case BITVECTOR_XOR: return "BITVECTOR_XOR"; |
159 |
86 |
case BITVECTOR_NOT: return "BITVECTOR_NOT"; |
160 |
|
case BITVECTOR_NAND: return "BITVECTOR_NAND"; |
161 |
|
case BITVECTOR_NOR: return "BITVECTOR_NOR"; |
162 |
|
case BITVECTOR_XNOR: return "BITVECTOR_XNOR"; |
163 |
42 |
case BITVECTOR_MULT: return "BITVECTOR_MULT"; |
164 |
46 |
case BITVECTOR_NEG: return "BITVECTOR_NEG"; |
165 |
58 |
case BITVECTOR_ADD: return "BITVECTOR_ADD"; |
166 |
41 |
case BITVECTOR_SUB: return "BITVECTOR_SUB"; |
167 |
42 |
case BITVECTOR_UDIV: return "BITVECTOR_UDIV"; |
168 |
42 |
case BITVECTOR_UREM: return "BITVECTOR_UREM"; |
169 |
41 |
case BITVECTOR_SDIV: return "BITVECTOR_SDIV"; |
170 |
|
case BITVECTOR_SMOD: return "BITVECTOR_SMOD"; |
171 |
39 |
case BITVECTOR_SREM: return "BITVECTOR_SREM"; |
172 |
37 |
case BITVECTOR_ASHR: return "BITVECTOR_ASHR"; |
173 |
44 |
case BITVECTOR_LSHR: return "BITVECTOR_LSHR"; |
174 |
44 |
case BITVECTOR_SHL: return "BITVECTOR_SHL"; |
175 |
2 |
case BITVECTOR_ULE: return "BITVECTOR_ULE"; |
176 |
39 |
case BITVECTOR_ULT: return "BITVECTOR_ULT"; |
177 |
2 |
case BITVECTOR_UGE: return "BITVECTOR_UGE"; |
178 |
1 |
case BITVECTOR_UGT: return "BITVECTOR_UGT"; |
179 |
|
case BITVECTOR_SLE: return "BITVECTOR_SLE"; |
180 |
2 |
case BITVECTOR_SLT: return "BITVECTOR_SLT"; |
181 |
2 |
case BITVECTOR_SGE: return "BITVECTOR_SGE"; |
182 |
|
case BITVECTOR_SGT: return "BITVECTOR_SGT"; |
183 |
16 |
case BITVECTOR_ULTBV: return "BITVECTOR_ULTBV"; |
184 |
4 |
case BITVECTOR_SLTBV: return "BITVECTOR_SLTBV"; |
185 |
|
case BITVECTOR_REDAND: return "BITVECTOR_REDAND"; |
186 |
|
case BITVECTOR_REDOR: return "BITVECTOR_REDOR"; |
187 |
12 |
case BITVECTOR_ITE: return "BITVECTOR_ITE"; |
188 |
|
case BITVECTOR_TO_NAT: return "BITVECTOR_TO_NAT"; |
189 |
|
case BITVECTOR_ACKERMANNIZE_UDIV: return "BITVECTOR_ACKERMANNIZE_UDIV"; |
190 |
|
case BITVECTOR_ACKERMANNIZE_UREM: return "BITVECTOR_ACKERMANNIZE_UREM"; |
191 |
|
case BITVECTOR_EAGER_ATOM: return "BITVECTOR_EAGER_ATOM"; |
192 |
|
case BITVECTOR_BITOF_OP: return "BITVECTOR_BITOF_OP"; |
193 |
|
case BITVECTOR_BITOF: return "BITVECTOR_BITOF"; |
194 |
|
case BITVECTOR_EXTRACT_OP: return "BITVECTOR_EXTRACT_OP"; |
195 |
24 |
case BITVECTOR_EXTRACT: return "BITVECTOR_EXTRACT"; |
196 |
|
case BITVECTOR_REPEAT_OP: return "BITVECTOR_REPEAT_OP"; |
197 |
3 |
case BITVECTOR_REPEAT: return "BITVECTOR_REPEAT"; |
198 |
|
case BITVECTOR_ROTATE_LEFT_OP: return "BITVECTOR_ROTATE_LEFT_OP"; |
199 |
|
case BITVECTOR_ROTATE_LEFT: return "BITVECTOR_ROTATE_LEFT"; |
200 |
|
case BITVECTOR_ROTATE_RIGHT_OP: return "BITVECTOR_ROTATE_RIGHT_OP"; |
201 |
|
case BITVECTOR_ROTATE_RIGHT: return "BITVECTOR_ROTATE_RIGHT"; |
202 |
|
case BITVECTOR_SIGN_EXTEND_OP: return "BITVECTOR_SIGN_EXTEND_OP"; |
203 |
|
case BITVECTOR_SIGN_EXTEND: return "BITVECTOR_SIGN_EXTEND"; |
204 |
|
case BITVECTOR_ZERO_EXTEND_OP: return "BITVECTOR_ZERO_EXTEND_OP"; |
205 |
|
case BITVECTOR_ZERO_EXTEND: return "BITVECTOR_ZERO_EXTEND"; |
206 |
1 |
case INT_TO_BITVECTOR_OP: return "INT_TO_BITVECTOR_OP"; |
207 |
|
case INT_TO_BITVECTOR: return "INT_TO_BITVECTOR"; |
208 |
|
|
209 |
|
/* from fp */ |
210 |
|
case CONST_FLOATINGPOINT: return "CONST_FLOATINGPOINT"; |
211 |
1 |
case CONST_ROUNDINGMODE: return "CONST_ROUNDINGMODE"; |
212 |
|
case FLOATINGPOINT_TYPE: return "FLOATINGPOINT_TYPE"; |
213 |
|
case FLOATINGPOINT_FP: return "FLOATINGPOINT_FP"; |
214 |
|
case FLOATINGPOINT_EQ: return "FLOATINGPOINT_EQ"; |
215 |
2 |
case FLOATINGPOINT_ABS: return "FLOATINGPOINT_ABS"; |
216 |
2 |
case FLOATINGPOINT_NEG: return "FLOATINGPOINT_NEG"; |
217 |
2 |
case FLOATINGPOINT_PLUS: return "FLOATINGPOINT_PLUS"; |
218 |
3 |
case FLOATINGPOINT_SUB: return "FLOATINGPOINT_SUB"; |
219 |
2 |
case FLOATINGPOINT_MULT: return "FLOATINGPOINT_MULT"; |
220 |
2 |
case FLOATINGPOINT_DIV: return "FLOATINGPOINT_DIV"; |
221 |
|
case FLOATINGPOINT_FMA: return "FLOATINGPOINT_FMA"; |
222 |
2 |
case FLOATINGPOINT_SQRT: return "FLOATINGPOINT_SQRT"; |
223 |
2 |
case FLOATINGPOINT_REM: return "FLOATINGPOINT_REM"; |
224 |
|
case FLOATINGPOINT_RTI: return "FLOATINGPOINT_RTI"; |
225 |
|
case FLOATINGPOINT_MIN: return "FLOATINGPOINT_MIN"; |
226 |
1 |
case FLOATINGPOINT_MAX: return "FLOATINGPOINT_MAX"; |
227 |
|
case FLOATINGPOINT_MIN_TOTAL: return "FLOATINGPOINT_MIN_TOTAL"; |
228 |
|
case FLOATINGPOINT_MAX_TOTAL: return "FLOATINGPOINT_MAX_TOTAL"; |
229 |
|
case FLOATINGPOINT_LEQ: return "FLOATINGPOINT_LEQ"; |
230 |
|
case FLOATINGPOINT_LT: return "FLOATINGPOINT_LT"; |
231 |
|
case FLOATINGPOINT_GEQ: return "FLOATINGPOINT_GEQ"; |
232 |
|
case FLOATINGPOINT_GT: return "FLOATINGPOINT_GT"; |
233 |
1 |
case FLOATINGPOINT_ISN: return "FLOATINGPOINT_ISN"; |
234 |
1 |
case FLOATINGPOINT_ISSN: return "FLOATINGPOINT_ISSN"; |
235 |
2 |
case FLOATINGPOINT_ISZ: return "FLOATINGPOINT_ISZ"; |
236 |
1 |
case FLOATINGPOINT_ISINF: return "FLOATINGPOINT_ISINF"; |
237 |
1 |
case FLOATINGPOINT_ISNAN: return "FLOATINGPOINT_ISNAN"; |
238 |
2 |
case FLOATINGPOINT_ISNEG: return "FLOATINGPOINT_ISNEG"; |
239 |
1 |
case FLOATINGPOINT_ISPOS: return "FLOATINGPOINT_ISPOS"; |
240 |
|
case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: return "FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP"; |
241 |
|
case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: return "FLOATINGPOINT_TO_FP_IEEE_BITVECTOR"; |
242 |
|
case FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: return "FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP"; |
243 |
|
case FLOATINGPOINT_TO_FP_FLOATINGPOINT: return "FLOATINGPOINT_TO_FP_FLOATINGPOINT"; |
244 |
|
case FLOATINGPOINT_TO_FP_REAL_OP: return "FLOATINGPOINT_TO_FP_REAL_OP"; |
245 |
|
case FLOATINGPOINT_TO_FP_REAL: return "FLOATINGPOINT_TO_FP_REAL"; |
246 |
|
case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: return "FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP"; |
247 |
|
case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: return "FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR"; |
248 |
|
case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP: return "FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP"; |
249 |
|
case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: return "FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR"; |
250 |
|
case FLOATINGPOINT_TO_FP_GENERIC_OP: return "FLOATINGPOINT_TO_FP_GENERIC_OP"; |
251 |
2 |
case FLOATINGPOINT_TO_FP_GENERIC: return "FLOATINGPOINT_TO_FP_GENERIC"; |
252 |
|
case FLOATINGPOINT_TO_UBV_OP: return "FLOATINGPOINT_TO_UBV_OP"; |
253 |
|
case FLOATINGPOINT_TO_UBV: return "FLOATINGPOINT_TO_UBV"; |
254 |
|
case FLOATINGPOINT_TO_UBV_TOTAL_OP: return "FLOATINGPOINT_TO_UBV_TOTAL_OP"; |
255 |
|
case FLOATINGPOINT_TO_UBV_TOTAL: return "FLOATINGPOINT_TO_UBV_TOTAL"; |
256 |
|
case FLOATINGPOINT_TO_SBV_OP: return "FLOATINGPOINT_TO_SBV_OP"; |
257 |
|
case FLOATINGPOINT_TO_SBV: return "FLOATINGPOINT_TO_SBV"; |
258 |
|
case FLOATINGPOINT_TO_SBV_TOTAL_OP: return "FLOATINGPOINT_TO_SBV_TOTAL_OP"; |
259 |
|
case FLOATINGPOINT_TO_SBV_TOTAL: return "FLOATINGPOINT_TO_SBV_TOTAL"; |
260 |
|
case FLOATINGPOINT_TO_REAL: return "FLOATINGPOINT_TO_REAL"; |
261 |
|
case FLOATINGPOINT_TO_REAL_TOTAL: return "FLOATINGPOINT_TO_REAL_TOTAL"; |
262 |
|
case FLOATINGPOINT_COMPONENT_NAN: return "FLOATINGPOINT_COMPONENT_NAN"; |
263 |
|
case FLOATINGPOINT_COMPONENT_INF: return "FLOATINGPOINT_COMPONENT_INF"; |
264 |
|
case FLOATINGPOINT_COMPONENT_ZERO: return "FLOATINGPOINT_COMPONENT_ZERO"; |
265 |
|
case FLOATINGPOINT_COMPONENT_SIGN: return "FLOATINGPOINT_COMPONENT_SIGN"; |
266 |
|
case FLOATINGPOINT_COMPONENT_EXPONENT: return "FLOATINGPOINT_COMPONENT_EXPONENT"; |
267 |
|
case FLOATINGPOINT_COMPONENT_SIGNIFICAND: return "FLOATINGPOINT_COMPONENT_SIGNIFICAND"; |
268 |
|
case ROUNDINGMODE_BITBLAST: return "ROUNDINGMODE_BITBLAST"; |
269 |
|
|
270 |
|
/* from arrays */ |
271 |
|
case ARRAY_TYPE: return "ARRAY_TYPE"; |
272 |
13 |
case SELECT: return "SELECT"; |
273 |
13 |
case STORE: return "STORE"; |
274 |
|
case EQ_RANGE: return "EQ_RANGE"; |
275 |
|
case STORE_ALL: return "STORE_ALL"; |
276 |
|
case ARR_TABLE_FUN: return "ARR_TABLE_FUN"; |
277 |
|
case ARRAY_LAMBDA: return "ARRAY_LAMBDA"; |
278 |
|
case PARTIAL_SELECT_0: return "PARTIAL_SELECT_0"; |
279 |
|
case PARTIAL_SELECT_1: return "PARTIAL_SELECT_1"; |
280 |
|
|
281 |
|
/* from datatypes */ |
282 |
|
case CONSTRUCTOR_TYPE: return "CONSTRUCTOR_TYPE"; |
283 |
|
case SELECTOR_TYPE: return "SELECTOR_TYPE"; |
284 |
|
case TESTER_TYPE: return "TESTER_TYPE"; |
285 |
|
case UPDATER_TYPE: return "UPDATER_TYPE"; |
286 |
73 |
case APPLY_CONSTRUCTOR: return "APPLY_CONSTRUCTOR"; |
287 |
34 |
case APPLY_SELECTOR: return "APPLY_SELECTOR"; |
288 |
|
case APPLY_SELECTOR_TOTAL: return "APPLY_SELECTOR_TOTAL"; |
289 |
|
case APPLY_TESTER: return "APPLY_TESTER"; |
290 |
|
case APPLY_UPDATER: return "APPLY_UPDATER"; |
291 |
|
case DATATYPE_TYPE: return "DATATYPE_TYPE"; |
292 |
|
case PARAMETRIC_DATATYPE: return "PARAMETRIC_DATATYPE"; |
293 |
|
case APPLY_TYPE_ASCRIPTION: return "APPLY_TYPE_ASCRIPTION"; |
294 |
|
case ASCRIPTION_TYPE: return "ASCRIPTION_TYPE"; |
295 |
|
case DT_SIZE: return "DT_SIZE"; |
296 |
|
case DT_HEIGHT_BOUND: return "DT_HEIGHT_BOUND"; |
297 |
|
case DT_SIZE_BOUND: return "DT_SIZE_BOUND"; |
298 |
|
case DT_SYGUS_BOUND: return "DT_SYGUS_BOUND"; |
299 |
383 |
case DT_SYGUS_EVAL: return "DT_SYGUS_EVAL"; |
300 |
|
case MATCH: return "MATCH"; |
301 |
|
case MATCH_CASE: return "MATCH_CASE"; |
302 |
|
case MATCH_BIND_CASE: return "MATCH_BIND_CASE"; |
303 |
|
case TUPLE_PROJECT_OP: return "TUPLE_PROJECT_OP"; |
304 |
|
case TUPLE_PROJECT: return "TUPLE_PROJECT"; |
305 |
|
|
306 |
|
/* from sep */ |
307 |
|
case SEP_NIL: return "SEP_NIL"; |
308 |
|
case SEP_EMP: return "SEP_EMP"; |
309 |
|
case SEP_PTO: return "SEP_PTO"; |
310 |
|
case SEP_STAR: return "SEP_STAR"; |
311 |
|
case SEP_WAND: return "SEP_WAND"; |
312 |
|
case SEP_LABEL: return "SEP_LABEL"; |
313 |
|
|
314 |
|
/* from sets */ |
315 |
|
case EMPTYSET: return "EMPTYSET"; |
316 |
|
case SET_TYPE: return "SET_TYPE"; |
317 |
8 |
case UNION: return "UNION"; |
318 |
6 |
case INTERSECTION: return "INTERSECTION"; |
319 |
6 |
case SETMINUS: return "SETMINUS"; |
320 |
|
case SUBSET: return "SUBSET"; |
321 |
6 |
case MEMBER: return "MEMBER"; |
322 |
|
case SINGLETON_OP: return "SINGLETON_OP"; |
323 |
|
case SINGLETON: return "SINGLETON"; |
324 |
|
case INSERT: return "INSERT"; |
325 |
|
case CARD: return "CARD"; |
326 |
|
case COMPLEMENT: return "COMPLEMENT"; |
327 |
|
case UNIVERSE_SET: return "UNIVERSE_SET"; |
328 |
|
case COMPREHENSION: return "COMPREHENSION"; |
329 |
|
case CHOOSE: return "CHOOSE"; |
330 |
|
case IS_SINGLETON: return "IS_SINGLETON"; |
331 |
|
case JOIN: return "JOIN"; |
332 |
|
case PRODUCT: return "PRODUCT"; |
333 |
|
case TRANSPOSE: return "TRANSPOSE"; |
334 |
|
case TCLOSURE: return "TCLOSURE"; |
335 |
|
case JOIN_IMAGE: return "JOIN_IMAGE"; |
336 |
|
case IDEN: return "IDEN"; |
337 |
|
|
338 |
|
/* from bags */ |
339 |
|
case EMPTYBAG: return "EMPTYBAG"; |
340 |
|
case BAG_TYPE: return "BAG_TYPE"; |
341 |
|
case UNION_MAX: return "UNION_MAX"; |
342 |
|
case UNION_DISJOINT: return "UNION_DISJOINT"; |
343 |
|
case INTERSECTION_MIN: return "INTERSECTION_MIN"; |
344 |
|
case DIFFERENCE_SUBTRACT: return "DIFFERENCE_SUBTRACT"; |
345 |
|
case DIFFERENCE_REMOVE: return "DIFFERENCE_REMOVE"; |
346 |
|
case SUBBAG: return "SUBBAG"; |
347 |
|
case BAG_COUNT: return "BAG_COUNT"; |
348 |
|
case DUPLICATE_REMOVAL: return "DUPLICATE_REMOVAL"; |
349 |
|
case MK_BAG_OP: return "MK_BAG_OP"; |
350 |
|
case MK_BAG: return "MK_BAG"; |
351 |
|
case BAG_IS_SINGLETON: return "BAG_IS_SINGLETON"; |
352 |
|
case BAG_CARD: return "BAG_CARD"; |
353 |
|
case BAG_FROM_SET: return "BAG_FROM_SET"; |
354 |
|
case BAG_TO_SET: return "BAG_TO_SET"; |
355 |
|
case BAG_CHOOSE: return "BAG_CHOOSE"; |
356 |
|
|
357 |
|
/* from strings */ |
358 |
40 |
case STRING_CONCAT: return "STRING_CONCAT"; |
359 |
1 |
case STRING_IN_REGEXP: return "STRING_IN_REGEXP"; |
360 |
30 |
case STRING_LENGTH: return "STRING_LENGTH"; |
361 |
7 |
case STRING_SUBSTR: return "STRING_SUBSTR"; |
362 |
|
case STRING_UPDATE: return "STRING_UPDATE"; |
363 |
5 |
case STRING_CHARAT: return "STRING_CHARAT"; |
364 |
4 |
case STRING_STRCTN: return "STRING_STRCTN"; |
365 |
|
case STRING_LT: return "STRING_LT"; |
366 |
|
case STRING_LEQ: return "STRING_LEQ"; |
367 |
6 |
case STRING_STRIDOF: return "STRING_STRIDOF"; |
368 |
5 |
case STRING_STRREPL: return "STRING_STRREPL"; |
369 |
|
case STRING_STRREPLALL: return "STRING_STRREPLALL"; |
370 |
|
case STRING_REPLACE_RE: return "STRING_REPLACE_RE"; |
371 |
|
case STRING_REPLACE_RE_ALL: return "STRING_REPLACE_RE_ALL"; |
372 |
4 |
case STRING_PREFIX: return "STRING_PREFIX"; |
373 |
4 |
case STRING_SUFFIX: return "STRING_SUFFIX"; |
374 |
|
case STRING_IS_DIGIT: return "STRING_IS_DIGIT"; |
375 |
5 |
case STRING_ITOS: return "STRING_ITOS"; |
376 |
6 |
case STRING_STOI: return "STRING_STOI"; |
377 |
|
case STRING_TO_CODE: return "STRING_TO_CODE"; |
378 |
|
case STRING_FROM_CODE: return "STRING_FROM_CODE"; |
379 |
|
case STRING_TOLOWER: return "STRING_TOLOWER"; |
380 |
|
case STRING_TOUPPER: return "STRING_TOUPPER"; |
381 |
|
case STRING_REV: return "STRING_REV"; |
382 |
61 |
case CONST_STRING: return "CONST_STRING"; |
383 |
|
case SEQUENCE_TYPE: return "SEQUENCE_TYPE"; |
384 |
|
case CONST_SEQUENCE: return "CONST_SEQUENCE"; |
385 |
|
case SEQ_UNIT: return "SEQ_UNIT"; |
386 |
|
case SEQ_NTH: return "SEQ_NTH"; |
387 |
|
case SEQ_NTH_TOTAL: return "SEQ_NTH_TOTAL"; |
388 |
6 |
case STRING_TO_REGEXP: return "STRING_TO_REGEXP"; |
389 |
4 |
case REGEXP_CONCAT: return "REGEXP_CONCAT"; |
390 |
3 |
case REGEXP_UNION: return "REGEXP_UNION"; |
391 |
3 |
case REGEXP_INTER: return "REGEXP_INTER"; |
392 |
1 |
case REGEXP_DIFF: return "REGEXP_DIFF"; |
393 |
3 |
case REGEXP_STAR: return "REGEXP_STAR"; |
394 |
1 |
case REGEXP_PLUS: return "REGEXP_PLUS"; |
395 |
1 |
case REGEXP_OPT: return "REGEXP_OPT"; |
396 |
|
case REGEXP_RANGE: return "REGEXP_RANGE"; |
397 |
1 |
case REGEXP_COMPLEMENT: return "REGEXP_COMPLEMENT"; |
398 |
|
case REGEXP_EMPTY: return "REGEXP_EMPTY"; |
399 |
|
case REGEXP_SIGMA: return "REGEXP_SIGMA"; |
400 |
|
case REGEXP_REPEAT_OP: return "REGEXP_REPEAT_OP"; |
401 |
|
case REGEXP_REPEAT: return "REGEXP_REPEAT"; |
402 |
|
case REGEXP_LOOP_OP: return "REGEXP_LOOP_OP"; |
403 |
|
case REGEXP_LOOP: return "REGEXP_LOOP"; |
404 |
|
case REGEXP_RV: return "REGEXP_RV"; |
405 |
|
|
406 |
|
/* from quantifiers */ |
407 |
|
case FORALL: return "FORALL"; |
408 |
|
case EXISTS: return "EXISTS"; |
409 |
1510 |
case INST_CONSTANT: return "INST_CONSTANT"; |
410 |
|
case BOUND_VAR_LIST: return "BOUND_VAR_LIST"; |
411 |
|
case INST_PATTERN: return "INST_PATTERN"; |
412 |
|
case INST_NO_PATTERN: return "INST_NO_PATTERN"; |
413 |
|
case INST_ATTRIBUTE: return "INST_ATTRIBUTE"; |
414 |
|
case INST_POOL: return "INST_POOL"; |
415 |
|
case INST_ADD_TO_POOL: return "INST_ADD_TO_POOL"; |
416 |
|
case SKOLEM_ADD_TO_POOL: return "SKOLEM_ADD_TO_POOL"; |
417 |
|
case INST_PATTERN_LIST: return "INST_PATTERN_LIST"; |
418 |
|
|
419 |
|
// clang-format on |
420 |
4 |
case LAST_KIND: return "LAST_KIND"; |
421 |
2 |
default: return "?"; |
422 |
|
} |
423 |
|
} |
424 |
|
|
425 |
3956 |
std::ostream& operator<<(std::ostream& out, cvc5::Kind k) |
426 |
|
{ |
427 |
3956 |
out << toString(k); |
428 |
3956 |
return out; |
429 |
|
} |
430 |
|
|
431 |
|
/** Returns true if the given kind is associative. This is used by ExprManager to |
432 |
|
* decide whether it's safe to modify big expressions by changing the grouping of |
433 |
|
* the arguments. */ |
434 |
|
/* TODO: This could be generated. */ |
435 |
4470196 |
bool isAssociative(::cvc5::Kind k) |
436 |
|
{ |
437 |
4470196 |
switch(k) { |
438 |
2135652 |
case kind::AND: |
439 |
|
case kind::OR: |
440 |
|
case kind::MULT: |
441 |
|
case kind::PLUS: |
442 |
2135652 |
return true; |
443 |
|
|
444 |
2334544 |
default: |
445 |
2334544 |
return false; |
446 |
|
} |
447 |
|
} |
448 |
|
|
449 |
3932 |
std::string kindToString(::cvc5::Kind k) { return toString(k); } |
450 |
|
|
451 |
|
} // namespace kind |
452 |
|
|
453 |
|
const char* toString(TypeConstant tc) |
454 |
|
{ |
455 |
|
switch (tc) |
456 |
|
{ |
457 |
|
// clang-format off |
458 |
|
case BUILTIN_OPERATOR_TYPE: return "the type for built-in operators"; |
459 |
|
case SEXPR_TYPE: return "the type of a symbolic expression"; |
460 |
|
case BOOLEAN_TYPE: return "Boolean type"; |
461 |
|
case REAL_TYPE: return "real type"; |
462 |
|
case INTEGER_TYPE: return "integer type"; |
463 |
|
case ROUNDINGMODE_TYPE: return "floating-point rounding mode"; |
464 |
|
case STRING_TYPE: return "String type"; |
465 |
|
case REGEXP_TYPE: return "RegExp type"; |
466 |
|
case BOUND_VAR_LIST_TYPE: return "the type of bound variable lists"; |
467 |
|
case INST_PATTERN_TYPE: return "instantiation pattern type"; |
468 |
|
case INST_PATTERN_LIST_TYPE: return "the type of instantiation pattern lists"; |
469 |
|
|
470 |
|
// clang-format on |
471 |
|
default: return "UNKNOWN_TYPE_CONSTANT"; |
472 |
|
} |
473 |
|
} |
474 |
|
std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) |
475 |
|
{ |
476 |
|
return out << toString(typeConstant); |
477 |
|
} |
478 |
|
|
479 |
|
namespace theory { |
480 |
|
|
481 |
302315927 |
TheoryId kindToTheoryId(::cvc5::Kind k) |
482 |
|
{ |
483 |
302315927 |
switch (k) |
484 |
|
{ |
485 |
|
case kind::UNDEFINED_KIND: |
486 |
|
case kind::NULL_EXPR: |
487 |
|
break; |
488 |
|
// clang-format off |
489 |
|
case kind::SORT_TAG: return THEORY_BUILTIN; |
490 |
2921130 |
case kind::SORT_TYPE: return THEORY_BUILTIN; |
491 |
54552 |
case kind::UNINTERPRETED_CONSTANT: return THEORY_BUILTIN; |
492 |
|
case kind::ABSTRACT_VALUE: return THEORY_BUILTIN; |
493 |
|
case kind::BUILTIN: return THEORY_BUILTIN; |
494 |
4379167 |
case kind::EQUAL: return THEORY_BUILTIN; |
495 |
13483 |
case kind::DISTINCT: return THEORY_BUILTIN; |
496 |
6266962 |
case kind::VARIABLE: return THEORY_BUILTIN; |
497 |
10924009 |
case kind::BOUND_VARIABLE: return THEORY_BUILTIN; |
498 |
2170318 |
case kind::SKOLEM: return THEORY_BUILTIN; |
499 |
|
case kind::SEXPR: return THEORY_BUILTIN; |
500 |
22295 |
case kind::LAMBDA: return THEORY_BUILTIN; |
501 |
13077 |
case kind::WITNESS: return THEORY_BUILTIN; |
502 |
|
case kind::TYPE_CONSTANT: return THEORY_BUILTIN; |
503 |
32940 |
case kind::FUNCTION_TYPE: return THEORY_BUILTIN; |
504 |
7500973 |
case kind::CONST_BOOLEAN: return THEORY_BOOL; |
505 |
22668910 |
case kind::NOT: return THEORY_BOOL; |
506 |
12431575 |
case kind::AND: return THEORY_BOOL; |
507 |
2687423 |
case kind::IMPLIES: return THEORY_BOOL; |
508 |
20126112 |
case kind::OR: return THEORY_BOOL; |
509 |
3023282 |
case kind::XOR: return THEORY_BOOL; |
510 |
7673243 |
case kind::ITE: return THEORY_BOOL; |
511 |
33520036 |
case kind::APPLY_UF: return THEORY_UF; |
512 |
209159 |
case kind::BOOLEAN_TERM_VARIABLE: return THEORY_UF; |
513 |
96421 |
case kind::CARDINALITY_CONSTRAINT: return THEORY_UF; |
514 |
51272 |
case kind::COMBINED_CARDINALITY_CONSTRAINT: return THEORY_UF; |
515 |
|
case kind::PARTIAL_APPLY_UF: return THEORY_UF; |
516 |
|
case kind::CARDINALITY_VALUE: return THEORY_UF; |
517 |
67094 |
case kind::HO_APPLY: return THEORY_UF; |
518 |
39164569 |
case kind::PLUS: return THEORY_ARITH; |
519 |
4964240 |
case kind::MULT: return THEORY_ARITH; |
520 |
5522077 |
case kind::NONLINEAR_MULT: return THEORY_ARITH; |
521 |
791248 |
case kind::MINUS: return THEORY_ARITH; |
522 |
40659 |
case kind::UMINUS: return THEORY_ARITH; |
523 |
8660 |
case kind::DIVISION: return THEORY_ARITH; |
524 |
1338 |
case kind::DIVISION_TOTAL: return THEORY_ARITH; |
525 |
3083 |
case kind::INTS_DIVISION: return THEORY_ARITH; |
526 |
19793 |
case kind::INTS_DIVISION_TOTAL: return THEORY_ARITH; |
527 |
2116 |
case kind::INTS_MODULUS: return THEORY_ARITH; |
528 |
17472 |
case kind::INTS_MODULUS_TOTAL: return THEORY_ARITH; |
529 |
281 |
case kind::ABS: return THEORY_ARITH; |
530 |
|
case kind::DIVISIBLE: return THEORY_ARITH; |
531 |
416 |
case kind::POW: return THEORY_ARITH; |
532 |
24126 |
case kind::EXPONENTIAL: return THEORY_ARITH; |
533 |
98576 |
case kind::SINE: return THEORY_ARITH; |
534 |
378 |
case kind::COSINE: return THEORY_ARITH; |
535 |
48 |
case kind::TANGENT: return THEORY_ARITH; |
536 |
12 |
case kind::COSECANT: return THEORY_ARITH; |
537 |
12 |
case kind::SECANT: return THEORY_ARITH; |
538 |
24 |
case kind::COTANGENT: return THEORY_ARITH; |
539 |
36 |
case kind::ARCSINE: return THEORY_ARITH; |
540 |
36 |
case kind::ARCCOSINE: return THEORY_ARITH; |
541 |
103 |
case kind::ARCTANGENT: return THEORY_ARITH; |
542 |
|
case kind::ARCCOSECANT: return THEORY_ARITH; |
543 |
|
case kind::ARCSECANT: return THEORY_ARITH; |
544 |
|
case kind::ARCCOTANGENT: return THEORY_ARITH; |
545 |
521 |
case kind::SQRT: return THEORY_ARITH; |
546 |
|
case kind::DIVISIBLE_OP: return THEORY_ARITH; |
547 |
11719794 |
case kind::CONST_RATIONAL: return THEORY_ARITH; |
548 |
352354 |
case kind::LT: return THEORY_ARITH; |
549 |
704338 |
case kind::LEQ: return THEORY_ARITH; |
550 |
146854 |
case kind::GT: return THEORY_ARITH; |
551 |
15604484 |
case kind::GEQ: return THEORY_ARITH; |
552 |
|
case kind::INDEXED_ROOT_PREDICATE_OP: return THEORY_ARITH; |
553 |
|
case kind::INDEXED_ROOT_PREDICATE: return THEORY_ARITH; |
554 |
526 |
case kind::IS_INTEGER: return THEORY_ARITH; |
555 |
5033 |
case kind::TO_INTEGER: return THEORY_ARITH; |
556 |
89 |
case kind::TO_REAL: return THEORY_ARITH; |
557 |
17725 |
case kind::CAST_TO_REAL: return THEORY_ARITH; |
558 |
38750 |
case kind::PI: return THEORY_ARITH; |
559 |
|
case kind::IAND_OP: return THEORY_ARITH; |
560 |
16967 |
case kind::IAND: return THEORY_ARITH; |
561 |
7640033 |
case kind::BITVECTOR_TYPE: return THEORY_BV; |
562 |
5397859 |
case kind::CONST_BITVECTOR: return THEORY_BV; |
563 |
|
case kind::BITVECTOR_BB_TERM: return THEORY_BV; |
564 |
1069474 |
case kind::BITVECTOR_CONCAT: return THEORY_BV; |
565 |
525878 |
case kind::BITVECTOR_AND: return THEORY_BV; |
566 |
691524 |
case kind::BITVECTOR_COMP: return THEORY_BV; |
567 |
718395 |
case kind::BITVECTOR_OR: return THEORY_BV; |
568 |
42841 |
case kind::BITVECTOR_XOR: return THEORY_BV; |
569 |
470230 |
case kind::BITVECTOR_NOT: return THEORY_BV; |
570 |
1738 |
case kind::BITVECTOR_NAND: return THEORY_BV; |
571 |
2331 |
case kind::BITVECTOR_NOR: return THEORY_BV; |
572 |
2441 |
case kind::BITVECTOR_XNOR: return THEORY_BV; |
573 |
920829 |
case kind::BITVECTOR_MULT: return THEORY_BV; |
574 |
230442 |
case kind::BITVECTOR_NEG: return THEORY_BV; |
575 |
841067 |
case kind::BITVECTOR_ADD: return THEORY_BV; |
576 |
7319 |
case kind::BITVECTOR_SUB: return THEORY_BV; |
577 |
71408 |
case kind::BITVECTOR_UDIV: return THEORY_BV; |
578 |
74573 |
case kind::BITVECTOR_UREM: return THEORY_BV; |
579 |
376 |
case kind::BITVECTOR_SDIV: return THEORY_BV; |
580 |
308 |
case kind::BITVECTOR_SMOD: return THEORY_BV; |
581 |
190 |
case kind::BITVECTOR_SREM: return THEORY_BV; |
582 |
61555 |
case kind::BITVECTOR_ASHR: return THEORY_BV; |
583 |
223475 |
case kind::BITVECTOR_LSHR: return THEORY_BV; |
584 |
211158 |
case kind::BITVECTOR_SHL: return THEORY_BV; |
585 |
7946 |
case kind::BITVECTOR_ULE: return THEORY_BV; |
586 |
943856 |
case kind::BITVECTOR_ULT: return THEORY_BV; |
587 |
4319 |
case kind::BITVECTOR_UGE: return THEORY_BV; |
588 |
4647 |
case kind::BITVECTOR_UGT: return THEORY_BV; |
589 |
8307 |
case kind::BITVECTOR_SLE: return THEORY_BV; |
590 |
997427 |
case kind::BITVECTOR_SLT: return THEORY_BV; |
591 |
4535 |
case kind::BITVECTOR_SGE: return THEORY_BV; |
592 |
4833 |
case kind::BITVECTOR_SGT: return THEORY_BV; |
593 |
25836 |
case kind::BITVECTOR_ULTBV: return THEORY_BV; |
594 |
37628 |
case kind::BITVECTOR_SLTBV: return THEORY_BV; |
595 |
|
case kind::BITVECTOR_REDAND: return THEORY_BV; |
596 |
|
case kind::BITVECTOR_REDOR: return THEORY_BV; |
597 |
159312 |
case kind::BITVECTOR_ITE: return THEORY_BV; |
598 |
582808 |
case kind::BITVECTOR_TO_NAT: return THEORY_BV; |
599 |
|
case kind::BITVECTOR_ACKERMANNIZE_UDIV: return THEORY_BV; |
600 |
|
case kind::BITVECTOR_ACKERMANNIZE_UREM: return THEORY_BV; |
601 |
5965 |
case kind::BITVECTOR_EAGER_ATOM: return THEORY_BV; |
602 |
|
case kind::BITVECTOR_BITOF_OP: return THEORY_BV; |
603 |
3585586 |
case kind::BITVECTOR_BITOF: return THEORY_BV; |
604 |
|
case kind::BITVECTOR_EXTRACT_OP: return THEORY_BV; |
605 |
705606 |
case kind::BITVECTOR_EXTRACT: return THEORY_BV; |
606 |
|
case kind::BITVECTOR_REPEAT_OP: return THEORY_BV; |
607 |
2143 |
case kind::BITVECTOR_REPEAT: return THEORY_BV; |
608 |
|
case kind::BITVECTOR_ROTATE_LEFT_OP: return THEORY_BV; |
609 |
1798 |
case kind::BITVECTOR_ROTATE_LEFT: return THEORY_BV; |
610 |
|
case kind::BITVECTOR_ROTATE_RIGHT_OP: return THEORY_BV; |
611 |
2260 |
case kind::BITVECTOR_ROTATE_RIGHT: return THEORY_BV; |
612 |
|
case kind::BITVECTOR_SIGN_EXTEND_OP: return THEORY_BV; |
613 |
267052 |
case kind::BITVECTOR_SIGN_EXTEND: return THEORY_BV; |
614 |
|
case kind::BITVECTOR_ZERO_EXTEND_OP: return THEORY_BV; |
615 |
19014 |
case kind::BITVECTOR_ZERO_EXTEND: return THEORY_BV; |
616 |
|
case kind::INT_TO_BITVECTOR_OP: return THEORY_BV; |
617 |
18159 |
case kind::INT_TO_BITVECTOR: return THEORY_BV; |
618 |
18103 |
case kind::CONST_FLOATINGPOINT: return THEORY_FP; |
619 |
4310 |
case kind::CONST_ROUNDINGMODE: return THEORY_FP; |
620 |
34180 |
case kind::FLOATINGPOINT_TYPE: return THEORY_FP; |
621 |
899 |
case kind::FLOATINGPOINT_FP: return THEORY_FP; |
622 |
21 |
case kind::FLOATINGPOINT_EQ: return THEORY_FP; |
623 |
257 |
case kind::FLOATINGPOINT_ABS: return THEORY_FP; |
624 |
2104 |
case kind::FLOATINGPOINT_NEG: return THEORY_FP; |
625 |
5212 |
case kind::FLOATINGPOINT_PLUS: return THEORY_FP; |
626 |
38 |
case kind::FLOATINGPOINT_SUB: return THEORY_FP; |
627 |
1176 |
case kind::FLOATINGPOINT_MULT: return THEORY_FP; |
628 |
1355 |
case kind::FLOATINGPOINT_DIV: return THEORY_FP; |
629 |
|
case kind::FLOATINGPOINT_FMA: return THEORY_FP; |
630 |
122 |
case kind::FLOATINGPOINT_SQRT: return THEORY_FP; |
631 |
1170 |
case kind::FLOATINGPOINT_REM: return THEORY_FP; |
632 |
1796 |
case kind::FLOATINGPOINT_RTI: return THEORY_FP; |
633 |
|
case kind::FLOATINGPOINT_MIN: return THEORY_FP; |
634 |
13 |
case kind::FLOATINGPOINT_MAX: return THEORY_FP; |
635 |
|
case kind::FLOATINGPOINT_MIN_TOTAL: return THEORY_FP; |
636 |
1003 |
case kind::FLOATINGPOINT_MAX_TOTAL: return THEORY_FP; |
637 |
3096 |
case kind::FLOATINGPOINT_LEQ: return THEORY_FP; |
638 |
503 |
case kind::FLOATINGPOINT_LT: return THEORY_FP; |
639 |
24 |
case kind::FLOATINGPOINT_GEQ: return THEORY_FP; |
640 |
4 |
case kind::FLOATINGPOINT_GT: return THEORY_FP; |
641 |
69 |
case kind::FLOATINGPOINT_ISN: return THEORY_FP; |
642 |
229 |
case kind::FLOATINGPOINT_ISSN: return THEORY_FP; |
643 |
1103 |
case kind::FLOATINGPOINT_ISZ: return THEORY_FP; |
644 |
1377 |
case kind::FLOATINGPOINT_ISINF: return THEORY_FP; |
645 |
992 |
case kind::FLOATINGPOINT_ISNAN: return THEORY_FP; |
646 |
1122 |
case kind::FLOATINGPOINT_ISNEG: return THEORY_FP; |
647 |
246 |
case kind::FLOATINGPOINT_ISPOS: return THEORY_FP; |
648 |
|
case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: return THEORY_FP; |
649 |
1226 |
case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: return THEORY_FP; |
650 |
|
case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: return THEORY_FP; |
651 |
177 |
case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: return THEORY_FP; |
652 |
|
case kind::FLOATINGPOINT_TO_FP_REAL_OP: return THEORY_FP; |
653 |
70 |
case kind::FLOATINGPOINT_TO_FP_REAL: return THEORY_FP; |
654 |
|
case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: return THEORY_FP; |
655 |
16 |
case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: return THEORY_FP; |
656 |
|
case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP: return THEORY_FP; |
657 |
566 |
case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: return THEORY_FP; |
658 |
|
case kind::FLOATINGPOINT_TO_FP_GENERIC_OP: return THEORY_FP; |
659 |
258 |
case kind::FLOATINGPOINT_TO_FP_GENERIC: return THEORY_FP; |
660 |
|
case kind::FLOATINGPOINT_TO_UBV_OP: return THEORY_FP; |
661 |
|
case kind::FLOATINGPOINT_TO_UBV: return THEORY_FP; |
662 |
|
case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP: return THEORY_FP; |
663 |
|
case kind::FLOATINGPOINT_TO_UBV_TOTAL: return THEORY_FP; |
664 |
|
case kind::FLOATINGPOINT_TO_SBV_OP: return THEORY_FP; |
665 |
|
case kind::FLOATINGPOINT_TO_SBV: return THEORY_FP; |
666 |
|
case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP: return THEORY_FP; |
667 |
|
case kind::FLOATINGPOINT_TO_SBV_TOTAL: return THEORY_FP; |
668 |
424 |
case kind::FLOATINGPOINT_TO_REAL: return THEORY_FP; |
669 |
56 |
case kind::FLOATINGPOINT_TO_REAL_TOTAL: return THEORY_FP; |
670 |
9095 |
case kind::FLOATINGPOINT_COMPONENT_NAN: return THEORY_FP; |
671 |
9566 |
case kind::FLOATINGPOINT_COMPONENT_INF: return THEORY_FP; |
672 |
9130 |
case kind::FLOATINGPOINT_COMPONENT_ZERO: return THEORY_FP; |
673 |
9022 |
case kind::FLOATINGPOINT_COMPONENT_SIGN: return THEORY_FP; |
674 |
13859 |
case kind::FLOATINGPOINT_COMPONENT_EXPONENT: return THEORY_FP; |
675 |
15270 |
case kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND: return THEORY_FP; |
676 |
628 |
case kind::ROUNDINGMODE_BITBLAST: return THEORY_FP; |
677 |
337812 |
case kind::ARRAY_TYPE: return THEORY_ARRAYS; |
678 |
1128478 |
case kind::SELECT: return THEORY_ARRAYS; |
679 |
691325 |
case kind::STORE: return THEORY_ARRAYS; |
680 |
511 |
case kind::EQ_RANGE: return THEORY_ARRAYS; |
681 |
11515 |
case kind::STORE_ALL: return THEORY_ARRAYS; |
682 |
|
case kind::ARR_TABLE_FUN: return THEORY_ARRAYS; |
683 |
|
case kind::ARRAY_LAMBDA: return THEORY_ARRAYS; |
684 |
|
case kind::PARTIAL_SELECT_0: return THEORY_ARRAYS; |
685 |
|
case kind::PARTIAL_SELECT_1: return THEORY_ARRAYS; |
686 |
|
case kind::CONSTRUCTOR_TYPE: return THEORY_DATATYPES; |
687 |
|
case kind::SELECTOR_TYPE: return THEORY_DATATYPES; |
688 |
|
case kind::TESTER_TYPE: return THEORY_DATATYPES; |
689 |
|
case kind::UPDATER_TYPE: return THEORY_DATATYPES; |
690 |
2480344 |
case kind::APPLY_CONSTRUCTOR: return THEORY_DATATYPES; |
691 |
197412 |
case kind::APPLY_SELECTOR: return THEORY_DATATYPES; |
692 |
2814150 |
case kind::APPLY_SELECTOR_TOTAL: return THEORY_DATATYPES; |
693 |
2249661 |
case kind::APPLY_TESTER: return THEORY_DATATYPES; |
694 |
265 |
case kind::APPLY_UPDATER: return THEORY_DATATYPES; |
695 |
3172028 |
case kind::DATATYPE_TYPE: return THEORY_DATATYPES; |
696 |
12708 |
case kind::PARAMETRIC_DATATYPE: return THEORY_DATATYPES; |
697 |
5 |
case kind::APPLY_TYPE_ASCRIPTION: return THEORY_DATATYPES; |
698 |
|
case kind::ASCRIPTION_TYPE: return THEORY_DATATYPES; |
699 |
3109369 |
case kind::DT_SIZE: return THEORY_DATATYPES; |
700 |
|
case kind::DT_HEIGHT_BOUND: return THEORY_DATATYPES; |
701 |
|
case kind::DT_SIZE_BOUND: return THEORY_DATATYPES; |
702 |
68196 |
case kind::DT_SYGUS_BOUND: return THEORY_DATATYPES; |
703 |
3647911 |
case kind::DT_SYGUS_EVAL: return THEORY_DATATYPES; |
704 |
36 |
case kind::MATCH: return THEORY_DATATYPES; |
705 |
80 |
case kind::MATCH_CASE: return THEORY_DATATYPES; |
706 |
32 |
case kind::MATCH_BIND_CASE: return THEORY_DATATYPES; |
707 |
|
case kind::TUPLE_PROJECT_OP: return THEORY_DATATYPES; |
708 |
18 |
case kind::TUPLE_PROJECT: return THEORY_DATATYPES; |
709 |
5061 |
case kind::SEP_NIL: return THEORY_SEP; |
710 |
1437 |
case kind::SEP_EMP: return THEORY_SEP; |
711 |
9787 |
case kind::SEP_PTO: return THEORY_SEP; |
712 |
6483 |
case kind::SEP_STAR: return THEORY_SEP; |
713 |
837 |
case kind::SEP_WAND: return THEORY_SEP; |
714 |
23860 |
case kind::SEP_LABEL: return THEORY_SEP; |
715 |
18558 |
case kind::EMPTYSET: return THEORY_SETS; |
716 |
616041 |
case kind::SET_TYPE: return THEORY_SETS; |
717 |
87796 |
case kind::UNION: return THEORY_SETS; |
718 |
72896 |
case kind::INTERSECTION: return THEORY_SETS; |
719 |
48690 |
case kind::SETMINUS: return THEORY_SETS; |
720 |
2627 |
case kind::SUBSET: return THEORY_SETS; |
721 |
799354 |
case kind::MEMBER: return THEORY_SETS; |
722 |
|
case kind::SINGLETON_OP: return THEORY_SETS; |
723 |
125400 |
case kind::SINGLETON: return THEORY_SETS; |
724 |
44 |
case kind::INSERT: return THEORY_SETS; |
725 |
1458471 |
case kind::CARD: return THEORY_SETS; |
726 |
73 |
case kind::COMPLEMENT: return THEORY_SETS; |
727 |
5945 |
case kind::UNIVERSE_SET: return THEORY_SETS; |
728 |
884 |
case kind::COMPREHENSION: return THEORY_SETS; |
729 |
1102 |
case kind::CHOOSE: return THEORY_SETS; |
730 |
448 |
case kind::IS_SINGLETON: return THEORY_SETS; |
731 |
52663 |
case kind::JOIN: return THEORY_SETS; |
732 |
3940 |
case kind::PRODUCT: return THEORY_SETS; |
733 |
29464 |
case kind::TRANSPOSE: return THEORY_SETS; |
734 |
5438 |
case kind::TCLOSURE: return THEORY_SETS; |
735 |
1435 |
case kind::JOIN_IMAGE: return THEORY_SETS; |
736 |
309 |
case kind::IDEN: return THEORY_SETS; |
737 |
580 |
case kind::EMPTYBAG: return THEORY_BAGS; |
738 |
20868 |
case kind::BAG_TYPE: return THEORY_BAGS; |
739 |
641 |
case kind::UNION_MAX: return THEORY_BAGS; |
740 |
2568 |
case kind::UNION_DISJOINT: return THEORY_BAGS; |
741 |
1507 |
case kind::INTERSECTION_MIN: return THEORY_BAGS; |
742 |
484 |
case kind::DIFFERENCE_SUBTRACT: return THEORY_BAGS; |
743 |
|
case kind::DIFFERENCE_REMOVE: return THEORY_BAGS; |
744 |
28 |
case kind::SUBBAG: return THEORY_BAGS; |
745 |
524661 |
case kind::BAG_COUNT: return THEORY_BAGS; |
746 |
743 |
case kind::DUPLICATE_REMOVAL: return THEORY_BAGS; |
747 |
|
case kind::MK_BAG_OP: return THEORY_BAGS; |
748 |
4943 |
case kind::MK_BAG: return THEORY_BAGS; |
749 |
|
case kind::BAG_IS_SINGLETON: return THEORY_BAGS; |
750 |
|
case kind::BAG_CARD: return THEORY_BAGS; |
751 |
|
case kind::BAG_FROM_SET: return THEORY_BAGS; |
752 |
|
case kind::BAG_TO_SET: return THEORY_BAGS; |
753 |
|
case kind::BAG_CHOOSE: return THEORY_BAGS; |
754 |
698829 |
case kind::STRING_CONCAT: return THEORY_STRINGS; |
755 |
160784 |
case kind::STRING_IN_REGEXP: return THEORY_STRINGS; |
756 |
28670831 |
case kind::STRING_LENGTH: return THEORY_STRINGS; |
757 |
523946 |
case kind::STRING_SUBSTR: return THEORY_STRINGS; |
758 |
2008 |
case kind::STRING_UPDATE: return THEORY_STRINGS; |
759 |
580 |
case kind::STRING_CHARAT: return THEORY_STRINGS; |
760 |
170897 |
case kind::STRING_STRCTN: return THEORY_STRINGS; |
761 |
65 |
case kind::STRING_LT: return THEORY_STRINGS; |
762 |
6442 |
case kind::STRING_LEQ: return THEORY_STRINGS; |
763 |
684495 |
case kind::STRING_STRIDOF: return THEORY_STRINGS; |
764 |
159704 |
case kind::STRING_STRREPL: return THEORY_STRINGS; |
765 |
2782 |
case kind::STRING_STRREPLALL: return THEORY_STRINGS; |
766 |
3466 |
case kind::STRING_REPLACE_RE: return THEORY_STRINGS; |
767 |
1358 |
case kind::STRING_REPLACE_RE_ALL: return THEORY_STRINGS; |
768 |
429 |
case kind::STRING_PREFIX: return THEORY_STRINGS; |
769 |
112 |
case kind::STRING_SUFFIX: return THEORY_STRINGS; |
770 |
26 |
case kind::STRING_IS_DIGIT: return THEORY_STRINGS; |
771 |
11377 |
case kind::STRING_ITOS: return THEORY_STRINGS; |
772 |
54857 |
case kind::STRING_STOI: return THEORY_STRINGS; |
773 |
1711613 |
case kind::STRING_TO_CODE: return THEORY_STRINGS; |
774 |
568 |
case kind::STRING_FROM_CODE: return THEORY_STRINGS; |
775 |
1112 |
case kind::STRING_TOLOWER: return THEORY_STRINGS; |
776 |
958 |
case kind::STRING_TOUPPER: return THEORY_STRINGS; |
777 |
2219 |
case kind::STRING_REV: return THEORY_STRINGS; |
778 |
566273 |
case kind::CONST_STRING: return THEORY_STRINGS; |
779 |
50637 |
case kind::SEQUENCE_TYPE: return THEORY_STRINGS; |
780 |
10069 |
case kind::CONST_SEQUENCE: return THEORY_STRINGS; |
781 |
5390 |
case kind::SEQ_UNIT: return THEORY_STRINGS; |
782 |
31140 |
case kind::SEQ_NTH: return THEORY_STRINGS; |
783 |
22 |
case kind::SEQ_NTH_TOTAL: return THEORY_STRINGS; |
784 |
28736 |
case kind::STRING_TO_REGEXP: return THEORY_STRINGS; |
785 |
28610 |
case kind::REGEXP_CONCAT: return THEORY_STRINGS; |
786 |
7476 |
case kind::REGEXP_UNION: return THEORY_STRINGS; |
787 |
1453 |
case kind::REGEXP_INTER: return THEORY_STRINGS; |
788 |
128 |
case kind::REGEXP_DIFF: return THEORY_STRINGS; |
789 |
23177 |
case kind::REGEXP_STAR: return THEORY_STRINGS; |
790 |
110 |
case kind::REGEXP_PLUS: return THEORY_STRINGS; |
791 |
86 |
case kind::REGEXP_OPT: return THEORY_STRINGS; |
792 |
8620 |
case kind::REGEXP_RANGE: return THEORY_STRINGS; |
793 |
1483 |
case kind::REGEXP_COMPLEMENT: return THEORY_STRINGS; |
794 |
486 |
case kind::REGEXP_EMPTY: return THEORY_STRINGS; |
795 |
4058 |
case kind::REGEXP_SIGMA: return THEORY_STRINGS; |
796 |
|
case kind::REGEXP_REPEAT_OP: return THEORY_STRINGS; |
797 |
14 |
case kind::REGEXP_REPEAT: return THEORY_STRINGS; |
798 |
|
case kind::REGEXP_LOOP_OP: return THEORY_STRINGS; |
799 |
76 |
case kind::REGEXP_LOOP: return THEORY_STRINGS; |
800 |
756 |
case kind::REGEXP_RV: return THEORY_STRINGS; |
801 |
1475938 |
case kind::FORALL: return THEORY_QUANTIFIERS; |
802 |
9067 |
case kind::EXISTS: return THEORY_QUANTIFIERS; |
803 |
118410 |
case kind::INST_CONSTANT: return THEORY_QUANTIFIERS; |
804 |
291585 |
case kind::BOUND_VAR_LIST: return THEORY_QUANTIFIERS; |
805 |
18892 |
case kind::INST_PATTERN: return THEORY_QUANTIFIERS; |
806 |
32 |
case kind::INST_NO_PATTERN: return THEORY_QUANTIFIERS; |
807 |
4080 |
case kind::INST_ATTRIBUTE: return THEORY_QUANTIFIERS; |
808 |
52 |
case kind::INST_POOL: return THEORY_QUANTIFIERS; |
809 |
|
case kind::INST_ADD_TO_POOL: return THEORY_QUANTIFIERS; |
810 |
64 |
case kind::SKOLEM_ADD_TO_POOL: return THEORY_QUANTIFIERS; |
811 |
37088 |
case kind::INST_PATTERN_LIST: return THEORY_QUANTIFIERS; |
812 |
|
|
813 |
|
// clang-format on |
814 |
|
case kind::LAST_KIND: break; |
815 |
|
} |
816 |
|
throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind"); |
817 |
|
} |
818 |
|
|
819 |
33484557 |
TheoryId typeConstantToTheoryId(::cvc5::TypeConstant typeConstant) |
820 |
|
{ |
821 |
33484557 |
switch (typeConstant) |
822 |
|
{ |
823 |
|
// clang-format off |
824 |
|
case BUILTIN_OPERATOR_TYPE: return THEORY_BUILTIN; |
825 |
|
case SEXPR_TYPE: return THEORY_BUILTIN; |
826 |
3778328 |
case BOOLEAN_TYPE: return THEORY_BOOL; |
827 |
2357668 |
case REAL_TYPE: return THEORY_ARITH; |
828 |
25025407 |
case INTEGER_TYPE: return THEORY_ARITH; |
829 |
1784 |
case ROUNDINGMODE_TYPE: return THEORY_FP; |
830 |
2321347 |
case STRING_TYPE: return THEORY_STRINGS; |
831 |
23 |
case REGEXP_TYPE: return THEORY_STRINGS; |
832 |
|
case BOUND_VAR_LIST_TYPE: return THEORY_QUANTIFIERS; |
833 |
|
case INST_PATTERN_TYPE: return THEORY_QUANTIFIERS; |
834 |
|
case INST_PATTERN_LIST_TYPE: return THEORY_QUANTIFIERS; |
835 |
|
|
836 |
|
// clang-format on |
837 |
|
case LAST_TYPE: break; |
838 |
|
} |
839 |
|
throw IllegalArgumentException( |
840 |
|
"", "k", __PRETTY_FUNCTION__, "bad type constant"); |
841 |
|
} |
842 |
|
|
843 |
|
} // namespace theory |
844 |
|
} // namespace cvc5 |