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-08-20/src/expr/kind_template.cpp /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-20/src/theory/builtin/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-20/src/theory/booleans/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-20/src/theory/uf/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-20/src/theory/arith/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-20/src/theory/bv/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-20/src/theory/fp/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-20/src/theory/arrays/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-20/src/theory/datatypes/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-20/src/theory/sep/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-20/src/theory/sets/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-20/src/theory/bags/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-20/src/theory/strings/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-20/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-08-20/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 |
10965 |
const char* toString(cvc5::Kind k) |
60 |
|
{ |
61 |
|
using namespace cvc5::kind; |
62 |
|
|
63 |
10965 |
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 |
491 |
case EQUAL: return "EQUAL"; |
77 |
4 |
case DISTINCT: return "DISTINCT"; |
78 |
22 |
case VARIABLE: return "VARIABLE"; |
79 |
689 |
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 |
401 |
case NOT: return "NOT"; |
90 |
440 |
case AND: return "AND"; |
91 |
3 |
case IMPLIES: return "IMPLIES"; |
92 |
433 |
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 |
5 |
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 |
449 |
case PLUS: return "PLUS"; |
107 |
6 |
case MULT: return "MULT"; |
108 |
|
case NONLINEAR_MULT: return "NONLINEAR_MULT"; |
109 |
371 |
case MINUS: return "MINUS"; |
110 |
14 |
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 POW2: return "POW2"; |
121 |
|
case EXPONENTIAL: return "EXPONENTIAL"; |
122 |
|
case SINE: return "SINE"; |
123 |
|
case COSINE: return "COSINE"; |
124 |
|
case TANGENT: return "TANGENT"; |
125 |
|
case COSECANT: return "COSECANT"; |
126 |
|
case SECANT: return "SECANT"; |
127 |
|
case COTANGENT: return "COTANGENT"; |
128 |
|
case ARCSINE: return "ARCSINE"; |
129 |
|
case ARCCOSINE: return "ARCCOSINE"; |
130 |
|
case ARCTANGENT: return "ARCTANGENT"; |
131 |
|
case ARCCOSECANT: return "ARCCOSECANT"; |
132 |
|
case ARCSECANT: return "ARCSECANT"; |
133 |
|
case ARCCOTANGENT: return "ARCCOTANGENT"; |
134 |
|
case SQRT: return "SQRT"; |
135 |
|
case DIVISIBLE_OP: return "DIVISIBLE_OP"; |
136 |
242 |
case CONST_RATIONAL: return "CONST_RATIONAL"; |
137 |
18 |
case LT: return "LT"; |
138 |
369 |
case LEQ: return "LEQ"; |
139 |
14 |
case GT: return "GT"; |
140 |
25 |
case GEQ: return "GEQ"; |
141 |
|
case INDEXED_ROOT_PREDICATE_OP: return "INDEXED_ROOT_PREDICATE_OP"; |
142 |
|
case INDEXED_ROOT_PREDICATE: return "INDEXED_ROOT_PREDICATE"; |
143 |
|
case IS_INTEGER: return "IS_INTEGER"; |
144 |
|
case TO_INTEGER: return "TO_INTEGER"; |
145 |
|
case TO_REAL: return "TO_REAL"; |
146 |
|
case CAST_TO_REAL: return "CAST_TO_REAL"; |
147 |
|
case PI: return "PI"; |
148 |
|
case IAND_OP: return "IAND_OP"; |
149 |
|
case IAND: return "IAND"; |
150 |
|
|
151 |
|
/* from bv */ |
152 |
|
case BITVECTOR_TYPE: return "BITVECTOR_TYPE"; |
153 |
56 |
case CONST_BITVECTOR: return "CONST_BITVECTOR"; |
154 |
|
case BITVECTOR_BB_TERM: return "BITVECTOR_BB_TERM"; |
155 |
1 |
case BITVECTOR_CONCAT: return "BITVECTOR_CONCAT"; |
156 |
62 |
case BITVECTOR_AND: return "BITVECTOR_AND"; |
157 |
14 |
case BITVECTOR_COMP: return "BITVECTOR_COMP"; |
158 |
84 |
case BITVECTOR_OR: return "BITVECTOR_OR"; |
159 |
53 |
case BITVECTOR_XOR: return "BITVECTOR_XOR"; |
160 |
86 |
case BITVECTOR_NOT: return "BITVECTOR_NOT"; |
161 |
|
case BITVECTOR_NAND: return "BITVECTOR_NAND"; |
162 |
|
case BITVECTOR_NOR: return "BITVECTOR_NOR"; |
163 |
|
case BITVECTOR_XNOR: return "BITVECTOR_XNOR"; |
164 |
42 |
case BITVECTOR_MULT: return "BITVECTOR_MULT"; |
165 |
46 |
case BITVECTOR_NEG: return "BITVECTOR_NEG"; |
166 |
58 |
case BITVECTOR_ADD: return "BITVECTOR_ADD"; |
167 |
41 |
case BITVECTOR_SUB: return "BITVECTOR_SUB"; |
168 |
42 |
case BITVECTOR_UDIV: return "BITVECTOR_UDIV"; |
169 |
42 |
case BITVECTOR_UREM: return "BITVECTOR_UREM"; |
170 |
41 |
case BITVECTOR_SDIV: return "BITVECTOR_SDIV"; |
171 |
|
case BITVECTOR_SMOD: return "BITVECTOR_SMOD"; |
172 |
39 |
case BITVECTOR_SREM: return "BITVECTOR_SREM"; |
173 |
37 |
case BITVECTOR_ASHR: return "BITVECTOR_ASHR"; |
174 |
44 |
case BITVECTOR_LSHR: return "BITVECTOR_LSHR"; |
175 |
44 |
case BITVECTOR_SHL: return "BITVECTOR_SHL"; |
176 |
2 |
case BITVECTOR_ULE: return "BITVECTOR_ULE"; |
177 |
39 |
case BITVECTOR_ULT: return "BITVECTOR_ULT"; |
178 |
2 |
case BITVECTOR_UGE: return "BITVECTOR_UGE"; |
179 |
1 |
case BITVECTOR_UGT: return "BITVECTOR_UGT"; |
180 |
|
case BITVECTOR_SLE: return "BITVECTOR_SLE"; |
181 |
2 |
case BITVECTOR_SLT: return "BITVECTOR_SLT"; |
182 |
2 |
case BITVECTOR_SGE: return "BITVECTOR_SGE"; |
183 |
|
case BITVECTOR_SGT: return "BITVECTOR_SGT"; |
184 |
16 |
case BITVECTOR_ULTBV: return "BITVECTOR_ULTBV"; |
185 |
4 |
case BITVECTOR_SLTBV: return "BITVECTOR_SLTBV"; |
186 |
|
case BITVECTOR_REDAND: return "BITVECTOR_REDAND"; |
187 |
|
case BITVECTOR_REDOR: return "BITVECTOR_REDOR"; |
188 |
12 |
case BITVECTOR_ITE: return "BITVECTOR_ITE"; |
189 |
|
case BITVECTOR_TO_NAT: return "BITVECTOR_TO_NAT"; |
190 |
|
case BITVECTOR_ACKERMANNIZE_UDIV: return "BITVECTOR_ACKERMANNIZE_UDIV"; |
191 |
|
case BITVECTOR_ACKERMANNIZE_UREM: return "BITVECTOR_ACKERMANNIZE_UREM"; |
192 |
|
case BITVECTOR_EAGER_ATOM: return "BITVECTOR_EAGER_ATOM"; |
193 |
|
case BITVECTOR_BITOF_OP: return "BITVECTOR_BITOF_OP"; |
194 |
|
case BITVECTOR_BITOF: return "BITVECTOR_BITOF"; |
195 |
|
case BITVECTOR_EXTRACT_OP: return "BITVECTOR_EXTRACT_OP"; |
196 |
24 |
case BITVECTOR_EXTRACT: return "BITVECTOR_EXTRACT"; |
197 |
|
case BITVECTOR_REPEAT_OP: return "BITVECTOR_REPEAT_OP"; |
198 |
3 |
case BITVECTOR_REPEAT: return "BITVECTOR_REPEAT"; |
199 |
|
case BITVECTOR_ROTATE_LEFT_OP: return "BITVECTOR_ROTATE_LEFT_OP"; |
200 |
|
case BITVECTOR_ROTATE_LEFT: return "BITVECTOR_ROTATE_LEFT"; |
201 |
|
case BITVECTOR_ROTATE_RIGHT_OP: return "BITVECTOR_ROTATE_RIGHT_OP"; |
202 |
|
case BITVECTOR_ROTATE_RIGHT: return "BITVECTOR_ROTATE_RIGHT"; |
203 |
|
case BITVECTOR_SIGN_EXTEND_OP: return "BITVECTOR_SIGN_EXTEND_OP"; |
204 |
|
case BITVECTOR_SIGN_EXTEND: return "BITVECTOR_SIGN_EXTEND"; |
205 |
|
case BITVECTOR_ZERO_EXTEND_OP: return "BITVECTOR_ZERO_EXTEND_OP"; |
206 |
|
case BITVECTOR_ZERO_EXTEND: return "BITVECTOR_ZERO_EXTEND"; |
207 |
1 |
case INT_TO_BITVECTOR_OP: return "INT_TO_BITVECTOR_OP"; |
208 |
|
case INT_TO_BITVECTOR: return "INT_TO_BITVECTOR"; |
209 |
|
|
210 |
|
/* from fp */ |
211 |
|
case CONST_FLOATINGPOINT: return "CONST_FLOATINGPOINT"; |
212 |
1 |
case CONST_ROUNDINGMODE: return "CONST_ROUNDINGMODE"; |
213 |
|
case FLOATINGPOINT_TYPE: return "FLOATINGPOINT_TYPE"; |
214 |
|
case FLOATINGPOINT_FP: return "FLOATINGPOINT_FP"; |
215 |
|
case FLOATINGPOINT_EQ: return "FLOATINGPOINT_EQ"; |
216 |
2 |
case FLOATINGPOINT_ABS: return "FLOATINGPOINT_ABS"; |
217 |
2 |
case FLOATINGPOINT_NEG: return "FLOATINGPOINT_NEG"; |
218 |
2 |
case FLOATINGPOINT_ADD: return "FLOATINGPOINT_ADD"; |
219 |
3 |
case FLOATINGPOINT_SUB: return "FLOATINGPOINT_SUB"; |
220 |
2 |
case FLOATINGPOINT_MULT: return "FLOATINGPOINT_MULT"; |
221 |
2 |
case FLOATINGPOINT_DIV: return "FLOATINGPOINT_DIV"; |
222 |
|
case FLOATINGPOINT_FMA: return "FLOATINGPOINT_FMA"; |
223 |
2 |
case FLOATINGPOINT_SQRT: return "FLOATINGPOINT_SQRT"; |
224 |
2 |
case FLOATINGPOINT_REM: return "FLOATINGPOINT_REM"; |
225 |
|
case FLOATINGPOINT_RTI: return "FLOATINGPOINT_RTI"; |
226 |
|
case FLOATINGPOINT_MIN: return "FLOATINGPOINT_MIN"; |
227 |
1 |
case FLOATINGPOINT_MAX: return "FLOATINGPOINT_MAX"; |
228 |
|
case FLOATINGPOINT_MIN_TOTAL: return "FLOATINGPOINT_MIN_TOTAL"; |
229 |
|
case FLOATINGPOINT_MAX_TOTAL: return "FLOATINGPOINT_MAX_TOTAL"; |
230 |
|
case FLOATINGPOINT_LEQ: return "FLOATINGPOINT_LEQ"; |
231 |
|
case FLOATINGPOINT_LT: return "FLOATINGPOINT_LT"; |
232 |
|
case FLOATINGPOINT_GEQ: return "FLOATINGPOINT_GEQ"; |
233 |
|
case FLOATINGPOINT_GT: return "FLOATINGPOINT_GT"; |
234 |
1 |
case FLOATINGPOINT_ISN: return "FLOATINGPOINT_ISN"; |
235 |
1 |
case FLOATINGPOINT_ISSN: return "FLOATINGPOINT_ISSN"; |
236 |
2 |
case FLOATINGPOINT_ISZ: return "FLOATINGPOINT_ISZ"; |
237 |
1 |
case FLOATINGPOINT_ISINF: return "FLOATINGPOINT_ISINF"; |
238 |
1 |
case FLOATINGPOINT_ISNAN: return "FLOATINGPOINT_ISNAN"; |
239 |
2 |
case FLOATINGPOINT_ISNEG: return "FLOATINGPOINT_ISNEG"; |
240 |
1 |
case FLOATINGPOINT_ISPOS: return "FLOATINGPOINT_ISPOS"; |
241 |
|
case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: return "FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP"; |
242 |
|
case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: return "FLOATINGPOINT_TO_FP_IEEE_BITVECTOR"; |
243 |
|
case FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: return "FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP"; |
244 |
|
case FLOATINGPOINT_TO_FP_FLOATINGPOINT: return "FLOATINGPOINT_TO_FP_FLOATINGPOINT"; |
245 |
|
case FLOATINGPOINT_TO_FP_REAL_OP: return "FLOATINGPOINT_TO_FP_REAL_OP"; |
246 |
|
case FLOATINGPOINT_TO_FP_REAL: return "FLOATINGPOINT_TO_FP_REAL"; |
247 |
|
case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: return "FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP"; |
248 |
|
case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: return "FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR"; |
249 |
|
case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP: return "FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP"; |
250 |
|
case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: return "FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR"; |
251 |
|
case FLOATINGPOINT_TO_FP_GENERIC_OP: return "FLOATINGPOINT_TO_FP_GENERIC_OP"; |
252 |
2 |
case FLOATINGPOINT_TO_FP_GENERIC: return "FLOATINGPOINT_TO_FP_GENERIC"; |
253 |
|
case FLOATINGPOINT_TO_UBV_OP: return "FLOATINGPOINT_TO_UBV_OP"; |
254 |
|
case FLOATINGPOINT_TO_UBV: return "FLOATINGPOINT_TO_UBV"; |
255 |
|
case FLOATINGPOINT_TO_UBV_TOTAL_OP: return "FLOATINGPOINT_TO_UBV_TOTAL_OP"; |
256 |
|
case FLOATINGPOINT_TO_UBV_TOTAL: return "FLOATINGPOINT_TO_UBV_TOTAL"; |
257 |
|
case FLOATINGPOINT_TO_SBV_OP: return "FLOATINGPOINT_TO_SBV_OP"; |
258 |
|
case FLOATINGPOINT_TO_SBV: return "FLOATINGPOINT_TO_SBV"; |
259 |
|
case FLOATINGPOINT_TO_SBV_TOTAL_OP: return "FLOATINGPOINT_TO_SBV_TOTAL_OP"; |
260 |
|
case FLOATINGPOINT_TO_SBV_TOTAL: return "FLOATINGPOINT_TO_SBV_TOTAL"; |
261 |
|
case FLOATINGPOINT_TO_REAL: return "FLOATINGPOINT_TO_REAL"; |
262 |
|
case FLOATINGPOINT_TO_REAL_TOTAL: return "FLOATINGPOINT_TO_REAL_TOTAL"; |
263 |
|
case FLOATINGPOINT_COMPONENT_NAN: return "FLOATINGPOINT_COMPONENT_NAN"; |
264 |
|
case FLOATINGPOINT_COMPONENT_INF: return "FLOATINGPOINT_COMPONENT_INF"; |
265 |
|
case FLOATINGPOINT_COMPONENT_ZERO: return "FLOATINGPOINT_COMPONENT_ZERO"; |
266 |
|
case FLOATINGPOINT_COMPONENT_SIGN: return "FLOATINGPOINT_COMPONENT_SIGN"; |
267 |
|
case FLOATINGPOINT_COMPONENT_EXPONENT: return "FLOATINGPOINT_COMPONENT_EXPONENT"; |
268 |
|
case FLOATINGPOINT_COMPONENT_SIGNIFICAND: return "FLOATINGPOINT_COMPONENT_SIGNIFICAND"; |
269 |
|
case ROUNDINGMODE_BITBLAST: return "ROUNDINGMODE_BITBLAST"; |
270 |
|
|
271 |
|
/* from arrays */ |
272 |
|
case ARRAY_TYPE: return "ARRAY_TYPE"; |
273 |
13 |
case SELECT: return "SELECT"; |
274 |
13 |
case STORE: return "STORE"; |
275 |
|
case EQ_RANGE: return "EQ_RANGE"; |
276 |
|
case STORE_ALL: return "STORE_ALL"; |
277 |
|
case ARR_TABLE_FUN: return "ARR_TABLE_FUN"; |
278 |
|
case ARRAY_LAMBDA: return "ARRAY_LAMBDA"; |
279 |
|
case PARTIAL_SELECT_0: return "PARTIAL_SELECT_0"; |
280 |
|
case PARTIAL_SELECT_1: return "PARTIAL_SELECT_1"; |
281 |
|
|
282 |
|
/* from datatypes */ |
283 |
|
case CONSTRUCTOR_TYPE: return "CONSTRUCTOR_TYPE"; |
284 |
|
case SELECTOR_TYPE: return "SELECTOR_TYPE"; |
285 |
|
case TESTER_TYPE: return "TESTER_TYPE"; |
286 |
|
case UPDATER_TYPE: return "UPDATER_TYPE"; |
287 |
73 |
case APPLY_CONSTRUCTOR: return "APPLY_CONSTRUCTOR"; |
288 |
34 |
case APPLY_SELECTOR: return "APPLY_SELECTOR"; |
289 |
|
case APPLY_SELECTOR_TOTAL: return "APPLY_SELECTOR_TOTAL"; |
290 |
|
case APPLY_TESTER: return "APPLY_TESTER"; |
291 |
|
case APPLY_UPDATER: return "APPLY_UPDATER"; |
292 |
|
case DATATYPE_TYPE: return "DATATYPE_TYPE"; |
293 |
|
case PARAMETRIC_DATATYPE: return "PARAMETRIC_DATATYPE"; |
294 |
|
case APPLY_TYPE_ASCRIPTION: return "APPLY_TYPE_ASCRIPTION"; |
295 |
|
case ASCRIPTION_TYPE: return "ASCRIPTION_TYPE"; |
296 |
|
case DT_SIZE: return "DT_SIZE"; |
297 |
|
case DT_HEIGHT_BOUND: return "DT_HEIGHT_BOUND"; |
298 |
|
case DT_SIZE_BOUND: return "DT_SIZE_BOUND"; |
299 |
|
case DT_SYGUS_BOUND: return "DT_SYGUS_BOUND"; |
300 |
374 |
case DT_SYGUS_EVAL: return "DT_SYGUS_EVAL"; |
301 |
|
case MATCH: return "MATCH"; |
302 |
|
case MATCH_CASE: return "MATCH_CASE"; |
303 |
|
case MATCH_BIND_CASE: return "MATCH_BIND_CASE"; |
304 |
|
case TUPLE_PROJECT_OP: return "TUPLE_PROJECT_OP"; |
305 |
2 |
case TUPLE_PROJECT: return "TUPLE_PROJECT"; |
306 |
|
|
307 |
|
/* from sep */ |
308 |
|
case SEP_NIL: return "SEP_NIL"; |
309 |
|
case SEP_EMP: return "SEP_EMP"; |
310 |
|
case SEP_PTO: return "SEP_PTO"; |
311 |
|
case SEP_STAR: return "SEP_STAR"; |
312 |
|
case SEP_WAND: return "SEP_WAND"; |
313 |
|
case SEP_LABEL: return "SEP_LABEL"; |
314 |
|
|
315 |
|
/* from sets */ |
316 |
|
case EMPTYSET: return "EMPTYSET"; |
317 |
|
case SET_TYPE: return "SET_TYPE"; |
318 |
8 |
case UNION: return "UNION"; |
319 |
6 |
case INTERSECTION: return "INTERSECTION"; |
320 |
6 |
case SETMINUS: return "SETMINUS"; |
321 |
|
case SUBSET: return "SUBSET"; |
322 |
6 |
case MEMBER: return "MEMBER"; |
323 |
|
case SINGLETON_OP: return "SINGLETON_OP"; |
324 |
|
case SINGLETON: return "SINGLETON"; |
325 |
|
case INSERT: return "INSERT"; |
326 |
|
case CARD: return "CARD"; |
327 |
|
case COMPLEMENT: return "COMPLEMENT"; |
328 |
|
case UNIVERSE_SET: return "UNIVERSE_SET"; |
329 |
|
case COMPREHENSION: return "COMPREHENSION"; |
330 |
|
case CHOOSE: return "CHOOSE"; |
331 |
|
case IS_SINGLETON: return "IS_SINGLETON"; |
332 |
|
case JOIN: return "JOIN"; |
333 |
|
case PRODUCT: return "PRODUCT"; |
334 |
|
case TRANSPOSE: return "TRANSPOSE"; |
335 |
|
case TCLOSURE: return "TCLOSURE"; |
336 |
|
case JOIN_IMAGE: return "JOIN_IMAGE"; |
337 |
|
case IDEN: return "IDEN"; |
338 |
|
|
339 |
|
/* from bags */ |
340 |
|
case EMPTYBAG: return "EMPTYBAG"; |
341 |
|
case BAG_TYPE: return "BAG_TYPE"; |
342 |
|
case UNION_MAX: return "UNION_MAX"; |
343 |
|
case UNION_DISJOINT: return "UNION_DISJOINT"; |
344 |
|
case INTERSECTION_MIN: return "INTERSECTION_MIN"; |
345 |
|
case DIFFERENCE_SUBTRACT: return "DIFFERENCE_SUBTRACT"; |
346 |
|
case DIFFERENCE_REMOVE: return "DIFFERENCE_REMOVE"; |
347 |
|
case SUBBAG: return "SUBBAG"; |
348 |
|
case BAG_COUNT: return "BAG_COUNT"; |
349 |
|
case DUPLICATE_REMOVAL: return "DUPLICATE_REMOVAL"; |
350 |
|
case MK_BAG_OP: return "MK_BAG_OP"; |
351 |
|
case MK_BAG: return "MK_BAG"; |
352 |
|
case BAG_IS_SINGLETON: return "BAG_IS_SINGLETON"; |
353 |
|
case BAG_CARD: return "BAG_CARD"; |
354 |
|
case BAG_FROM_SET: return "BAG_FROM_SET"; |
355 |
|
case BAG_TO_SET: return "BAG_TO_SET"; |
356 |
|
case BAG_CHOOSE: return "BAG_CHOOSE"; |
357 |
|
|
358 |
|
/* from strings */ |
359 |
40 |
case STRING_CONCAT: return "STRING_CONCAT"; |
360 |
1 |
case STRING_IN_REGEXP: return "STRING_IN_REGEXP"; |
361 |
30 |
case STRING_LENGTH: return "STRING_LENGTH"; |
362 |
7 |
case STRING_SUBSTR: return "STRING_SUBSTR"; |
363 |
|
case STRING_UPDATE: return "STRING_UPDATE"; |
364 |
5 |
case STRING_CHARAT: return "STRING_CHARAT"; |
365 |
4 |
case STRING_CONTAINS: return "STRING_CONTAINS"; |
366 |
|
case STRING_LT: return "STRING_LT"; |
367 |
|
case STRING_LEQ: return "STRING_LEQ"; |
368 |
6 |
case STRING_INDEXOF: return "STRING_INDEXOF"; |
369 |
|
case STRING_INDEXOF_RE: return "STRING_INDEXOF_RE"; |
370 |
5 |
case STRING_REPLACE: return "STRING_REPLACE"; |
371 |
|
case STRING_REPLACE_ALL: return "STRING_REPLACE_ALL"; |
372 |
|
case STRING_REPLACE_RE: return "STRING_REPLACE_RE"; |
373 |
|
case STRING_REPLACE_RE_ALL: return "STRING_REPLACE_RE_ALL"; |
374 |
4 |
case STRING_PREFIX: return "STRING_PREFIX"; |
375 |
4 |
case STRING_SUFFIX: return "STRING_SUFFIX"; |
376 |
|
case STRING_IS_DIGIT: return "STRING_IS_DIGIT"; |
377 |
5 |
case STRING_ITOS: return "STRING_ITOS"; |
378 |
6 |
case STRING_STOI: return "STRING_STOI"; |
379 |
|
case STRING_TO_CODE: return "STRING_TO_CODE"; |
380 |
|
case STRING_FROM_CODE: return "STRING_FROM_CODE"; |
381 |
|
case STRING_TOLOWER: return "STRING_TOLOWER"; |
382 |
|
case STRING_TOUPPER: return "STRING_TOUPPER"; |
383 |
|
case STRING_REV: return "STRING_REV"; |
384 |
61 |
case CONST_STRING: return "CONST_STRING"; |
385 |
|
case SEQUENCE_TYPE: return "SEQUENCE_TYPE"; |
386 |
|
case CONST_SEQUENCE: return "CONST_SEQUENCE"; |
387 |
|
case SEQ_UNIT: return "SEQ_UNIT"; |
388 |
|
case SEQ_NTH: return "SEQ_NTH"; |
389 |
|
case SEQ_NTH_TOTAL: return "SEQ_NTH_TOTAL"; |
390 |
6 |
case STRING_TO_REGEXP: return "STRING_TO_REGEXP"; |
391 |
4 |
case REGEXP_CONCAT: return "REGEXP_CONCAT"; |
392 |
3 |
case REGEXP_UNION: return "REGEXP_UNION"; |
393 |
3 |
case REGEXP_INTER: return "REGEXP_INTER"; |
394 |
1 |
case REGEXP_DIFF: return "REGEXP_DIFF"; |
395 |
3 |
case REGEXP_STAR: return "REGEXP_STAR"; |
396 |
1 |
case REGEXP_PLUS: return "REGEXP_PLUS"; |
397 |
1 |
case REGEXP_OPT: return "REGEXP_OPT"; |
398 |
|
case REGEXP_RANGE: return "REGEXP_RANGE"; |
399 |
1 |
case REGEXP_COMPLEMENT: return "REGEXP_COMPLEMENT"; |
400 |
|
case REGEXP_EMPTY: return "REGEXP_EMPTY"; |
401 |
|
case REGEXP_SIGMA: return "REGEXP_SIGMA"; |
402 |
|
case REGEXP_REPEAT_OP: return "REGEXP_REPEAT_OP"; |
403 |
|
case REGEXP_REPEAT: return "REGEXP_REPEAT"; |
404 |
|
case REGEXP_LOOP_OP: return "REGEXP_LOOP_OP"; |
405 |
|
case REGEXP_LOOP: return "REGEXP_LOOP"; |
406 |
|
case REGEXP_RV: return "REGEXP_RV"; |
407 |
|
|
408 |
|
/* from quantifiers */ |
409 |
|
case FORALL: return "FORALL"; |
410 |
|
case EXISTS: return "EXISTS"; |
411 |
4508 |
case INST_CONSTANT: return "INST_CONSTANT"; |
412 |
|
case BOUND_VAR_LIST: return "BOUND_VAR_LIST"; |
413 |
|
case INST_PATTERN: return "INST_PATTERN"; |
414 |
|
case INST_NO_PATTERN: return "INST_NO_PATTERN"; |
415 |
|
case INST_ATTRIBUTE: return "INST_ATTRIBUTE"; |
416 |
|
case INST_POOL: return "INST_POOL"; |
417 |
|
case INST_ADD_TO_POOL: return "INST_ADD_TO_POOL"; |
418 |
|
case SKOLEM_ADD_TO_POOL: return "SKOLEM_ADD_TO_POOL"; |
419 |
|
case INST_PATTERN_LIST: return "INST_PATTERN_LIST"; |
420 |
|
|
421 |
|
// clang-format on |
422 |
4 |
case LAST_KIND: return "LAST_KIND"; |
423 |
2 |
default: return "?"; |
424 |
|
} |
425 |
|
} |
426 |
|
|
427 |
6670 |
std::ostream& operator<<(std::ostream& out, cvc5::Kind k) |
428 |
|
{ |
429 |
6670 |
out << toString(k); |
430 |
6670 |
return out; |
431 |
|
} |
432 |
|
|
433 |
|
/** Returns true if the given kind is associative. This is used by ExprManager to |
434 |
|
* decide whether it's safe to modify big expressions by changing the grouping of |
435 |
|
* the arguments. */ |
436 |
|
/* TODO: This could be generated. */ |
437 |
4404593 |
bool isAssociative(::cvc5::Kind k) |
438 |
|
{ |
439 |
4404593 |
switch(k) { |
440 |
2109698 |
case kind::AND: |
441 |
|
case kind::OR: |
442 |
|
case kind::MULT: |
443 |
|
case kind::PLUS: |
444 |
2109698 |
return true; |
445 |
|
|
446 |
2294895 |
default: |
447 |
2294895 |
return false; |
448 |
|
} |
449 |
|
} |
450 |
|
|
451 |
4295 |
std::string kindToString(::cvc5::Kind k) { return toString(k); } |
452 |
|
|
453 |
|
} // namespace kind |
454 |
|
|
455 |
|
const char* toString(TypeConstant tc) |
456 |
|
{ |
457 |
|
switch (tc) |
458 |
|
{ |
459 |
|
// clang-format off |
460 |
|
case BUILTIN_OPERATOR_TYPE: return "the type for built-in operators"; |
461 |
|
case SEXPR_TYPE: return "the type of a symbolic expression"; |
462 |
|
case BOOLEAN_TYPE: return "Boolean type"; |
463 |
|
case REAL_TYPE: return "real type"; |
464 |
|
case INTEGER_TYPE: return "integer type"; |
465 |
|
case ROUNDINGMODE_TYPE: return "floating-point rounding mode"; |
466 |
|
case STRING_TYPE: return "String type"; |
467 |
|
case REGEXP_TYPE: return "RegExp type"; |
468 |
|
case BOUND_VAR_LIST_TYPE: return "the type of bound variable lists"; |
469 |
|
case INST_PATTERN_TYPE: return "instantiation pattern type"; |
470 |
|
case INST_PATTERN_LIST_TYPE: return "the type of instantiation pattern lists"; |
471 |
|
|
472 |
|
// clang-format on |
473 |
|
default: return "UNKNOWN_TYPE_CONSTANT"; |
474 |
|
} |
475 |
|
} |
476 |
|
std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) |
477 |
|
{ |
478 |
|
return out << toString(typeConstant); |
479 |
|
} |
480 |
|
|
481 |
|
namespace theory { |
482 |
|
|
483 |
304525265 |
TheoryId kindToTheoryId(::cvc5::Kind k) |
484 |
|
{ |
485 |
304525265 |
switch (k) |
486 |
|
{ |
487 |
|
case kind::UNDEFINED_KIND: |
488 |
|
case kind::NULL_EXPR: |
489 |
|
break; |
490 |
|
// clang-format off |
491 |
|
case kind::SORT_TAG: return THEORY_BUILTIN; |
492 |
2502225 |
case kind::SORT_TYPE: return THEORY_BUILTIN; |
493 |
51929 |
case kind::UNINTERPRETED_CONSTANT: return THEORY_BUILTIN; |
494 |
|
case kind::ABSTRACT_VALUE: return THEORY_BUILTIN; |
495 |
|
case kind::BUILTIN: return THEORY_BUILTIN; |
496 |
1329607 |
case kind::EQUAL: return THEORY_BUILTIN; |
497 |
13232 |
case kind::DISTINCT: return THEORY_BUILTIN; |
498 |
5815316 |
case kind::VARIABLE: return THEORY_BUILTIN; |
499 |
11004198 |
case kind::BOUND_VARIABLE: return THEORY_BUILTIN; |
500 |
2280935 |
case kind::SKOLEM: return THEORY_BUILTIN; |
501 |
|
case kind::SEXPR: return THEORY_BUILTIN; |
502 |
19288 |
case kind::LAMBDA: return THEORY_BUILTIN; |
503 |
12861 |
case kind::WITNESS: return THEORY_BUILTIN; |
504 |
|
case kind::TYPE_CONSTANT: return THEORY_BUILTIN; |
505 |
60685 |
case kind::FUNCTION_TYPE: return THEORY_BUILTIN; |
506 |
8545521 |
case kind::CONST_BOOLEAN: return THEORY_BOOL; |
507 |
24632987 |
case kind::NOT: return THEORY_BOOL; |
508 |
11822753 |
case kind::AND: return THEORY_BOOL; |
509 |
1370217 |
case kind::IMPLIES: return THEORY_BOOL; |
510 |
15672180 |
case kind::OR: return THEORY_BOOL; |
511 |
3009491 |
case kind::XOR: return THEORY_BOOL; |
512 |
7316479 |
case kind::ITE: return THEORY_BOOL; |
513 |
34878430 |
case kind::APPLY_UF: return THEORY_UF; |
514 |
215298 |
case kind::BOOLEAN_TERM_VARIABLE: return THEORY_UF; |
515 |
83103 |
case kind::CARDINALITY_CONSTRAINT: return THEORY_UF; |
516 |
50741 |
case kind::COMBINED_CARDINALITY_CONSTRAINT: return THEORY_UF; |
517 |
|
case kind::PARTIAL_APPLY_UF: return THEORY_UF; |
518 |
|
case kind::CARDINALITY_VALUE: return THEORY_UF; |
519 |
67470 |
case kind::HO_APPLY: return THEORY_UF; |
520 |
40643681 |
case kind::PLUS: return THEORY_ARITH; |
521 |
4917663 |
case kind::MULT: return THEORY_ARITH; |
522 |
4938121 |
case kind::NONLINEAR_MULT: return THEORY_ARITH; |
523 |
656951 |
case kind::MINUS: return THEORY_ARITH; |
524 |
52638 |
case kind::UMINUS: return THEORY_ARITH; |
525 |
8610 |
case kind::DIVISION: return THEORY_ARITH; |
526 |
1401 |
case kind::DIVISION_TOTAL: return THEORY_ARITH; |
527 |
4158 |
case kind::INTS_DIVISION: return THEORY_ARITH; |
528 |
29038 |
case kind::INTS_DIVISION_TOTAL: return THEORY_ARITH; |
529 |
1890 |
case kind::INTS_MODULUS: return THEORY_ARITH; |
530 |
17957 |
case kind::INTS_MODULUS_TOTAL: return THEORY_ARITH; |
531 |
283 |
case kind::ABS: return THEORY_ARITH; |
532 |
|
case kind::DIVISIBLE: return THEORY_ARITH; |
533 |
491 |
case kind::POW: return THEORY_ARITH; |
534 |
3685 |
case kind::POW2: return THEORY_ARITH; |
535 |
24068 |
case kind::EXPONENTIAL: return THEORY_ARITH; |
536 |
98574 |
case kind::SINE: return THEORY_ARITH; |
537 |
378 |
case kind::COSINE: return THEORY_ARITH; |
538 |
48 |
case kind::TANGENT: return THEORY_ARITH; |
539 |
12 |
case kind::COSECANT: return THEORY_ARITH; |
540 |
12 |
case kind::SECANT: return THEORY_ARITH; |
541 |
24 |
case kind::COTANGENT: return THEORY_ARITH; |
542 |
36 |
case kind::ARCSINE: return THEORY_ARITH; |
543 |
36 |
case kind::ARCCOSINE: return THEORY_ARITH; |
544 |
103 |
case kind::ARCTANGENT: return THEORY_ARITH; |
545 |
|
case kind::ARCCOSECANT: return THEORY_ARITH; |
546 |
|
case kind::ARCSECANT: return THEORY_ARITH; |
547 |
|
case kind::ARCCOTANGENT: return THEORY_ARITH; |
548 |
521 |
case kind::SQRT: return THEORY_ARITH; |
549 |
|
case kind::DIVISIBLE_OP: return THEORY_ARITH; |
550 |
12218152 |
case kind::CONST_RATIONAL: return THEORY_ARITH; |
551 |
391728 |
case kind::LT: return THEORY_ARITH; |
552 |
704875 |
case kind::LEQ: return THEORY_ARITH; |
553 |
141439 |
case kind::GT: return THEORY_ARITH; |
554 |
15326674 |
case kind::GEQ: return THEORY_ARITH; |
555 |
|
case kind::INDEXED_ROOT_PREDICATE_OP: return THEORY_ARITH; |
556 |
|
case kind::INDEXED_ROOT_PREDICATE: return THEORY_ARITH; |
557 |
526 |
case kind::IS_INTEGER: return THEORY_ARITH; |
558 |
6123 |
case kind::TO_INTEGER: return THEORY_ARITH; |
559 |
89 |
case kind::TO_REAL: return THEORY_ARITH; |
560 |
17726 |
case kind::CAST_TO_REAL: return THEORY_ARITH; |
561 |
38758 |
case kind::PI: return THEORY_ARITH; |
562 |
|
case kind::IAND_OP: return THEORY_ARITH; |
563 |
16960 |
case kind::IAND: return THEORY_ARITH; |
564 |
8041400 |
case kind::BITVECTOR_TYPE: return THEORY_BV; |
565 |
5461151 |
case kind::CONST_BITVECTOR: return THEORY_BV; |
566 |
|
case kind::BITVECTOR_BB_TERM: return THEORY_BV; |
567 |
1077654 |
case kind::BITVECTOR_CONCAT: return THEORY_BV; |
568 |
561137 |
case kind::BITVECTOR_AND: return THEORY_BV; |
569 |
740856 |
case kind::BITVECTOR_COMP: return THEORY_BV; |
570 |
741088 |
case kind::BITVECTOR_OR: return THEORY_BV; |
571 |
38503 |
case kind::BITVECTOR_XOR: return THEORY_BV; |
572 |
483459 |
case kind::BITVECTOR_NOT: return THEORY_BV; |
573 |
1510 |
case kind::BITVECTOR_NAND: return THEORY_BV; |
574 |
1964 |
case kind::BITVECTOR_NOR: return THEORY_BV; |
575 |
2084 |
case kind::BITVECTOR_XNOR: return THEORY_BV; |
576 |
887614 |
case kind::BITVECTOR_MULT: return THEORY_BV; |
577 |
245863 |
case kind::BITVECTOR_NEG: return THEORY_BV; |
578 |
629500 |
case kind::BITVECTOR_ADD: return THEORY_BV; |
579 |
7099 |
case kind::BITVECTOR_SUB: return THEORY_BV; |
580 |
87185 |
case kind::BITVECTOR_UDIV: return THEORY_BV; |
581 |
93148 |
case kind::BITVECTOR_UREM: return THEORY_BV; |
582 |
367 |
case kind::BITVECTOR_SDIV: return THEORY_BV; |
583 |
308 |
case kind::BITVECTOR_SMOD: return THEORY_BV; |
584 |
187 |
case kind::BITVECTOR_SREM: return THEORY_BV; |
585 |
48319 |
case kind::BITVECTOR_ASHR: return THEORY_BV; |
586 |
217037 |
case kind::BITVECTOR_LSHR: return THEORY_BV; |
587 |
204791 |
case kind::BITVECTOR_SHL: return THEORY_BV; |
588 |
7450 |
case kind::BITVECTOR_ULE: return THEORY_BV; |
589 |
833774 |
case kind::BITVECTOR_ULT: return THEORY_BV; |
590 |
3968 |
case kind::BITVECTOR_UGE: return THEORY_BV; |
591 |
4457 |
case kind::BITVECTOR_UGT: return THEORY_BV; |
592 |
7792 |
case kind::BITVECTOR_SLE: return THEORY_BV; |
593 |
913896 |
case kind::BITVECTOR_SLT: return THEORY_BV; |
594 |
4150 |
case kind::BITVECTOR_SGE: return THEORY_BV; |
595 |
4665 |
case kind::BITVECTOR_SGT: return THEORY_BV; |
596 |
27891 |
case kind::BITVECTOR_ULTBV: return THEORY_BV; |
597 |
37049 |
case kind::BITVECTOR_SLTBV: return THEORY_BV; |
598 |
|
case kind::BITVECTOR_REDAND: return THEORY_BV; |
599 |
|
case kind::BITVECTOR_REDOR: return THEORY_BV; |
600 |
161488 |
case kind::BITVECTOR_ITE: return THEORY_BV; |
601 |
11482 |
case kind::BITVECTOR_TO_NAT: return THEORY_BV; |
602 |
|
case kind::BITVECTOR_ACKERMANNIZE_UDIV: return THEORY_BV; |
603 |
|
case kind::BITVECTOR_ACKERMANNIZE_UREM: return THEORY_BV; |
604 |
4572 |
case kind::BITVECTOR_EAGER_ATOM: return THEORY_BV; |
605 |
|
case kind::BITVECTOR_BITOF_OP: return THEORY_BV; |
606 |
4754878 |
case kind::BITVECTOR_BITOF: return THEORY_BV; |
607 |
|
case kind::BITVECTOR_EXTRACT_OP: return THEORY_BV; |
608 |
633869 |
case kind::BITVECTOR_EXTRACT: return THEORY_BV; |
609 |
|
case kind::BITVECTOR_REPEAT_OP: return THEORY_BV; |
610 |
1807 |
case kind::BITVECTOR_REPEAT: return THEORY_BV; |
611 |
|
case kind::BITVECTOR_ROTATE_LEFT_OP: return THEORY_BV; |
612 |
1504 |
case kind::BITVECTOR_ROTATE_LEFT: return THEORY_BV; |
613 |
|
case kind::BITVECTOR_ROTATE_RIGHT_OP: return THEORY_BV; |
614 |
2014 |
case kind::BITVECTOR_ROTATE_RIGHT: return THEORY_BV; |
615 |
|
case kind::BITVECTOR_SIGN_EXTEND_OP: return THEORY_BV; |
616 |
230445 |
case kind::BITVECTOR_SIGN_EXTEND: return THEORY_BV; |
617 |
|
case kind::BITVECTOR_ZERO_EXTEND_OP: return THEORY_BV; |
618 |
17071 |
case kind::BITVECTOR_ZERO_EXTEND: return THEORY_BV; |
619 |
|
case kind::INT_TO_BITVECTOR_OP: return THEORY_BV; |
620 |
1851 |
case kind::INT_TO_BITVECTOR: return THEORY_BV; |
621 |
18503 |
case kind::CONST_FLOATINGPOINT: return THEORY_FP; |
622 |
5282 |
case kind::CONST_ROUNDINGMODE: return THEORY_FP; |
623 |
46641 |
case kind::FLOATINGPOINT_TYPE: return THEORY_FP; |
624 |
408 |
case kind::FLOATINGPOINT_FP: return THEORY_FP; |
625 |
21 |
case kind::FLOATINGPOINT_EQ: return THEORY_FP; |
626 |
1547 |
case kind::FLOATINGPOINT_ABS: return THEORY_FP; |
627 |
2182 |
case kind::FLOATINGPOINT_NEG: return THEORY_FP; |
628 |
5443 |
case kind::FLOATINGPOINT_ADD: return THEORY_FP; |
629 |
40 |
case kind::FLOATINGPOINT_SUB: return THEORY_FP; |
630 |
1394 |
case kind::FLOATINGPOINT_MULT: return THEORY_FP; |
631 |
1399 |
case kind::FLOATINGPOINT_DIV: return THEORY_FP; |
632 |
|
case kind::FLOATINGPOINT_FMA: return THEORY_FP; |
633 |
183 |
case kind::FLOATINGPOINT_SQRT: return THEORY_FP; |
634 |
1265 |
case kind::FLOATINGPOINT_REM: return THEORY_FP; |
635 |
1502 |
case kind::FLOATINGPOINT_RTI: return THEORY_FP; |
636 |
|
case kind::FLOATINGPOINT_MIN: return THEORY_FP; |
637 |
13 |
case kind::FLOATINGPOINT_MAX: return THEORY_FP; |
638 |
|
case kind::FLOATINGPOINT_MIN_TOTAL: return THEORY_FP; |
639 |
1003 |
case kind::FLOATINGPOINT_MAX_TOTAL: return THEORY_FP; |
640 |
2699 |
case kind::FLOATINGPOINT_LEQ: return THEORY_FP; |
641 |
501 |
case kind::FLOATINGPOINT_LT: return THEORY_FP; |
642 |
29 |
case kind::FLOATINGPOINT_GEQ: return THEORY_FP; |
643 |
4 |
case kind::FLOATINGPOINT_GT: return THEORY_FP; |
644 |
139 |
case kind::FLOATINGPOINT_ISN: return THEORY_FP; |
645 |
225 |
case kind::FLOATINGPOINT_ISSN: return THEORY_FP; |
646 |
1037 |
case kind::FLOATINGPOINT_ISZ: return THEORY_FP; |
647 |
1351 |
case kind::FLOATINGPOINT_ISINF: return THEORY_FP; |
648 |
1036 |
case kind::FLOATINGPOINT_ISNAN: return THEORY_FP; |
649 |
1362 |
case kind::FLOATINGPOINT_ISNEG: return THEORY_FP; |
650 |
263 |
case kind::FLOATINGPOINT_ISPOS: return THEORY_FP; |
651 |
|
case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: return THEORY_FP; |
652 |
2195 |
case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: return THEORY_FP; |
653 |
|
case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: return THEORY_FP; |
654 |
177 |
case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: return THEORY_FP; |
655 |
|
case kind::FLOATINGPOINT_TO_FP_REAL_OP: return THEORY_FP; |
656 |
46 |
case kind::FLOATINGPOINT_TO_FP_REAL: return THEORY_FP; |
657 |
|
case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: return THEORY_FP; |
658 |
16 |
case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: return THEORY_FP; |
659 |
|
case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP: return THEORY_FP; |
660 |
566 |
case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: return THEORY_FP; |
661 |
|
case kind::FLOATINGPOINT_TO_FP_GENERIC_OP: return THEORY_FP; |
662 |
310 |
case kind::FLOATINGPOINT_TO_FP_GENERIC: return THEORY_FP; |
663 |
|
case kind::FLOATINGPOINT_TO_UBV_OP: return THEORY_FP; |
664 |
|
case kind::FLOATINGPOINT_TO_UBV: return THEORY_FP; |
665 |
|
case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP: return THEORY_FP; |
666 |
|
case kind::FLOATINGPOINT_TO_UBV_TOTAL: return THEORY_FP; |
667 |
|
case kind::FLOATINGPOINT_TO_SBV_OP: return THEORY_FP; |
668 |
44 |
case kind::FLOATINGPOINT_TO_SBV: return THEORY_FP; |
669 |
|
case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP: return THEORY_FP; |
670 |
1300 |
case kind::FLOATINGPOINT_TO_SBV_TOTAL: return THEORY_FP; |
671 |
512 |
case kind::FLOATINGPOINT_TO_REAL: return THEORY_FP; |
672 |
44 |
case kind::FLOATINGPOINT_TO_REAL_TOTAL: return THEORY_FP; |
673 |
9107 |
case kind::FLOATINGPOINT_COMPONENT_NAN: return THEORY_FP; |
674 |
9595 |
case kind::FLOATINGPOINT_COMPONENT_INF: return THEORY_FP; |
675 |
9105 |
case kind::FLOATINGPOINT_COMPONENT_ZERO: return THEORY_FP; |
676 |
8915 |
case kind::FLOATINGPOINT_COMPONENT_SIGN: return THEORY_FP; |
677 |
15339 |
case kind::FLOATINGPOINT_COMPONENT_EXPONENT: return THEORY_FP; |
678 |
20070 |
case kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND: return THEORY_FP; |
679 |
702 |
case kind::ROUNDINGMODE_BITBLAST: return THEORY_FP; |
680 |
326118 |
case kind::ARRAY_TYPE: return THEORY_ARRAYS; |
681 |
1123749 |
case kind::SELECT: return THEORY_ARRAYS; |
682 |
513289 |
case kind::STORE: return THEORY_ARRAYS; |
683 |
511 |
case kind::EQ_RANGE: return THEORY_ARRAYS; |
684 |
12569 |
case kind::STORE_ALL: return THEORY_ARRAYS; |
685 |
|
case kind::ARR_TABLE_FUN: return THEORY_ARRAYS; |
686 |
|
case kind::ARRAY_LAMBDA: return THEORY_ARRAYS; |
687 |
|
case kind::PARTIAL_SELECT_0: return THEORY_ARRAYS; |
688 |
|
case kind::PARTIAL_SELECT_1: return THEORY_ARRAYS; |
689 |
|
case kind::CONSTRUCTOR_TYPE: return THEORY_DATATYPES; |
690 |
|
case kind::SELECTOR_TYPE: return THEORY_DATATYPES; |
691 |
|
case kind::TESTER_TYPE: return THEORY_DATATYPES; |
692 |
|
case kind::UPDATER_TYPE: return THEORY_DATATYPES; |
693 |
2635773 |
case kind::APPLY_CONSTRUCTOR: return THEORY_DATATYPES; |
694 |
236655 |
case kind::APPLY_SELECTOR: return THEORY_DATATYPES; |
695 |
2999858 |
case kind::APPLY_SELECTOR_TOTAL: return THEORY_DATATYPES; |
696 |
1791539 |
case kind::APPLY_TESTER: return THEORY_DATATYPES; |
697 |
265 |
case kind::APPLY_UPDATER: return THEORY_DATATYPES; |
698 |
2961010 |
case kind::DATATYPE_TYPE: return THEORY_DATATYPES; |
699 |
11583 |
case kind::PARAMETRIC_DATATYPE: return THEORY_DATATYPES; |
700 |
5 |
case kind::APPLY_TYPE_ASCRIPTION: return THEORY_DATATYPES; |
701 |
|
case kind::ASCRIPTION_TYPE: return THEORY_DATATYPES; |
702 |
3109510 |
case kind::DT_SIZE: return THEORY_DATATYPES; |
703 |
|
case kind::DT_HEIGHT_BOUND: return THEORY_DATATYPES; |
704 |
|
case kind::DT_SIZE_BOUND: return THEORY_DATATYPES; |
705 |
59460 |
case kind::DT_SYGUS_BOUND: return THEORY_DATATYPES; |
706 |
3396074 |
case kind::DT_SYGUS_EVAL: return THEORY_DATATYPES; |
707 |
36 |
case kind::MATCH: return THEORY_DATATYPES; |
708 |
80 |
case kind::MATCH_CASE: return THEORY_DATATYPES; |
709 |
32 |
case kind::MATCH_BIND_CASE: return THEORY_DATATYPES; |
710 |
|
case kind::TUPLE_PROJECT_OP: return THEORY_DATATYPES; |
711 |
18 |
case kind::TUPLE_PROJECT: return THEORY_DATATYPES; |
712 |
4859 |
case kind::SEP_NIL: return THEORY_SEP; |
713 |
1379 |
case kind::SEP_EMP: return THEORY_SEP; |
714 |
9731 |
case kind::SEP_PTO: return THEORY_SEP; |
715 |
5414 |
case kind::SEP_STAR: return THEORY_SEP; |
716 |
754 |
case kind::SEP_WAND: return THEORY_SEP; |
717 |
20435 |
case kind::SEP_LABEL: return THEORY_SEP; |
718 |
19152 |
case kind::EMPTYSET: return THEORY_SETS; |
719 |
625124 |
case kind::SET_TYPE: return THEORY_SETS; |
720 |
87769 |
case kind::UNION: return THEORY_SETS; |
721 |
75277 |
case kind::INTERSECTION: return THEORY_SETS; |
722 |
50601 |
case kind::SETMINUS: return THEORY_SETS; |
723 |
2817 |
case kind::SUBSET: return THEORY_SETS; |
724 |
774624 |
case kind::MEMBER: return THEORY_SETS; |
725 |
|
case kind::SINGLETON_OP: return THEORY_SETS; |
726 |
117579 |
case kind::SINGLETON: return THEORY_SETS; |
727 |
44 |
case kind::INSERT: return THEORY_SETS; |
728 |
1544826 |
case kind::CARD: return THEORY_SETS; |
729 |
73 |
case kind::COMPLEMENT: return THEORY_SETS; |
730 |
5425 |
case kind::UNIVERSE_SET: return THEORY_SETS; |
731 |
877 |
case kind::COMPREHENSION: return THEORY_SETS; |
732 |
1102 |
case kind::CHOOSE: return THEORY_SETS; |
733 |
448 |
case kind::IS_SINGLETON: return THEORY_SETS; |
734 |
53239 |
case kind::JOIN: return THEORY_SETS; |
735 |
3844 |
case kind::PRODUCT: return THEORY_SETS; |
736 |
29379 |
case kind::TRANSPOSE: return THEORY_SETS; |
737 |
5002 |
case kind::TCLOSURE: return THEORY_SETS; |
738 |
1435 |
case kind::JOIN_IMAGE: return THEORY_SETS; |
739 |
309 |
case kind::IDEN: return THEORY_SETS; |
740 |
577 |
case kind::EMPTYBAG: return THEORY_BAGS; |
741 |
21568 |
case kind::BAG_TYPE: return THEORY_BAGS; |
742 |
715 |
case kind::UNION_MAX: return THEORY_BAGS; |
743 |
2850 |
case kind::UNION_DISJOINT: return THEORY_BAGS; |
744 |
1591 |
case kind::INTERSECTION_MIN: return THEORY_BAGS; |
745 |
484 |
case kind::DIFFERENCE_SUBTRACT: return THEORY_BAGS; |
746 |
|
case kind::DIFFERENCE_REMOVE: return THEORY_BAGS; |
747 |
28 |
case kind::SUBBAG: return THEORY_BAGS; |
748 |
581552 |
case kind::BAG_COUNT: return THEORY_BAGS; |
749 |
657 |
case kind::DUPLICATE_REMOVAL: return THEORY_BAGS; |
750 |
|
case kind::MK_BAG_OP: return THEORY_BAGS; |
751 |
5393 |
case kind::MK_BAG: return THEORY_BAGS; |
752 |
|
case kind::BAG_IS_SINGLETON: return THEORY_BAGS; |
753 |
|
case kind::BAG_CARD: return THEORY_BAGS; |
754 |
|
case kind::BAG_FROM_SET: return THEORY_BAGS; |
755 |
|
case kind::BAG_TO_SET: return THEORY_BAGS; |
756 |
|
case kind::BAG_CHOOSE: return THEORY_BAGS; |
757 |
997368 |
case kind::STRING_CONCAT: return THEORY_STRINGS; |
758 |
313451 |
case kind::STRING_IN_REGEXP: return THEORY_STRINGS; |
759 |
34490825 |
case kind::STRING_LENGTH: return THEORY_STRINGS; |
760 |
657691 |
case kind::STRING_SUBSTR: return THEORY_STRINGS; |
761 |
2135 |
case kind::STRING_UPDATE: return THEORY_STRINGS; |
762 |
592 |
case kind::STRING_CHARAT: return THEORY_STRINGS; |
763 |
175445 |
case kind::STRING_CONTAINS: return THEORY_STRINGS; |
764 |
65 |
case kind::STRING_LT: return THEORY_STRINGS; |
765 |
6869 |
case kind::STRING_LEQ: return THEORY_STRINGS; |
766 |
955879 |
case kind::STRING_INDEXOF: return THEORY_STRINGS; |
767 |
230515 |
case kind::STRING_INDEXOF_RE: return THEORY_STRINGS; |
768 |
183673 |
case kind::STRING_REPLACE: return THEORY_STRINGS; |
769 |
4812 |
case kind::STRING_REPLACE_ALL: return THEORY_STRINGS; |
770 |
14530 |
case kind::STRING_REPLACE_RE: return THEORY_STRINGS; |
771 |
8909 |
case kind::STRING_REPLACE_RE_ALL: return THEORY_STRINGS; |
772 |
538 |
case kind::STRING_PREFIX: return THEORY_STRINGS; |
773 |
119 |
case kind::STRING_SUFFIX: return THEORY_STRINGS; |
774 |
26 |
case kind::STRING_IS_DIGIT: return THEORY_STRINGS; |
775 |
12023 |
case kind::STRING_ITOS: return THEORY_STRINGS; |
776 |
53249 |
case kind::STRING_STOI: return THEORY_STRINGS; |
777 |
1934615 |
case kind::STRING_TO_CODE: return THEORY_STRINGS; |
778 |
659 |
case kind::STRING_FROM_CODE: return THEORY_STRINGS; |
779 |
1090 |
case kind::STRING_TOLOWER: return THEORY_STRINGS; |
780 |
924 |
case kind::STRING_TOUPPER: return THEORY_STRINGS; |
781 |
1976 |
case kind::STRING_REV: return THEORY_STRINGS; |
782 |
797547 |
case kind::CONST_STRING: return THEORY_STRINGS; |
783 |
59681 |
case kind::SEQUENCE_TYPE: return THEORY_STRINGS; |
784 |
11459 |
case kind::CONST_SEQUENCE: return THEORY_STRINGS; |
785 |
7036 |
case kind::SEQ_UNIT: return THEORY_STRINGS; |
786 |
40362 |
case kind::SEQ_NTH: return THEORY_STRINGS; |
787 |
22 |
case kind::SEQ_NTH_TOTAL: return THEORY_STRINGS; |
788 |
66444 |
case kind::STRING_TO_REGEXP: return THEORY_STRINGS; |
789 |
53570 |
case kind::REGEXP_CONCAT: return THEORY_STRINGS; |
790 |
18874 |
case kind::REGEXP_UNION: return THEORY_STRINGS; |
791 |
7390 |
case kind::REGEXP_INTER: return THEORY_STRINGS; |
792 |
383 |
case kind::REGEXP_DIFF: return THEORY_STRINGS; |
793 |
38897 |
case kind::REGEXP_STAR: return THEORY_STRINGS; |
794 |
140 |
case kind::REGEXP_PLUS: return THEORY_STRINGS; |
795 |
104 |
case kind::REGEXP_OPT: return THEORY_STRINGS; |
796 |
8833 |
case kind::REGEXP_RANGE: return THEORY_STRINGS; |
797 |
7149 |
case kind::REGEXP_COMPLEMENT: return THEORY_STRINGS; |
798 |
570 |
case kind::REGEXP_EMPTY: return THEORY_STRINGS; |
799 |
7819 |
case kind::REGEXP_SIGMA: return THEORY_STRINGS; |
800 |
|
case kind::REGEXP_REPEAT_OP: return THEORY_STRINGS; |
801 |
14 |
case kind::REGEXP_REPEAT: return THEORY_STRINGS; |
802 |
|
case kind::REGEXP_LOOP_OP: return THEORY_STRINGS; |
803 |
76 |
case kind::REGEXP_LOOP: return THEORY_STRINGS; |
804 |
804 |
case kind::REGEXP_RV: return THEORY_STRINGS; |
805 |
1202508 |
case kind::FORALL: return THEORY_QUANTIFIERS; |
806 |
8637 |
case kind::EXISTS: return THEORY_QUANTIFIERS; |
807 |
117895 |
case kind::INST_CONSTANT: return THEORY_QUANTIFIERS; |
808 |
288985 |
case kind::BOUND_VAR_LIST: return THEORY_QUANTIFIERS; |
809 |
19005 |
case kind::INST_PATTERN: return THEORY_QUANTIFIERS; |
810 |
32 |
case kind::INST_NO_PATTERN: return THEORY_QUANTIFIERS; |
811 |
6630 |
case kind::INST_ATTRIBUTE: return THEORY_QUANTIFIERS; |
812 |
52 |
case kind::INST_POOL: return THEORY_QUANTIFIERS; |
813 |
|
case kind::INST_ADD_TO_POOL: return THEORY_QUANTIFIERS; |
814 |
64 |
case kind::SKOLEM_ADD_TO_POOL: return THEORY_QUANTIFIERS; |
815 |
41051 |
case kind::INST_PATTERN_LIST: return THEORY_QUANTIFIERS; |
816 |
|
|
817 |
|
// clang-format on |
818 |
|
case kind::LAST_KIND: break; |
819 |
|
} |
820 |
|
throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind"); |
821 |
|
} |
822 |
|
|
823 |
38909881 |
TheoryId typeConstantToTheoryId(::cvc5::TypeConstant typeConstant) |
824 |
|
{ |
825 |
38909881 |
switch (typeConstant) |
826 |
|
{ |
827 |
|
// clang-format off |
828 |
|
case BUILTIN_OPERATOR_TYPE: return THEORY_BUILTIN; |
829 |
|
case SEXPR_TYPE: return THEORY_BUILTIN; |
830 |
5069115 |
case BOOLEAN_TYPE: return THEORY_BOOL; |
831 |
2326779 |
case REAL_TYPE: return THEORY_ARITH; |
832 |
28174546 |
case INTEGER_TYPE: return THEORY_ARITH; |
833 |
2376 |
case ROUNDINGMODE_TYPE: return THEORY_FP; |
834 |
3337042 |
case STRING_TYPE: return THEORY_STRINGS; |
835 |
23 |
case REGEXP_TYPE: return THEORY_STRINGS; |
836 |
|
case BOUND_VAR_LIST_TYPE: return THEORY_QUANTIFIERS; |
837 |
|
case INST_PATTERN_TYPE: return THEORY_QUANTIFIERS; |
838 |
|
case INST_PATTERN_LIST_TYPE: return THEORY_QUANTIFIERS; |
839 |
|
|
840 |
|
// clang-format on |
841 |
|
case LAST_TYPE: break; |
842 |
|
} |
843 |
|
throw IllegalArgumentException( |
844 |
|
"", "k", __PRETTY_FUNCTION__, "bad type constant"); |
845 |
|
} |
846 |
|
|
847 |
|
} // namespace theory |
848 |
|
} // namespace cvc5 |