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-09-17/src/expr/kind_template.h /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-17/src/theory/builtin/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-17/src/theory/booleans/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-17/src/theory/uf/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-17/src/theory/arith/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-17/src/theory/bv/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-17/src/theory/fp/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-17/src/theory/arrays/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-17/src/theory/datatypes/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-17/src/theory/sep/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-17/src/theory/sets/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-17/src/theory/bags/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-17/src/theory/strings/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-17/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-09-17/src/expr/kind_template.h */ |
33 |
|
|
34 |
|
/****************************************************************************** |
35 |
|
* Top contributors (to current version): |
36 |
|
* Andres Noetzli, Morgan Deters, Aina Niemetz |
37 |
|
* |
38 |
|
* This file is part of the cvc5 project. |
39 |
|
* |
40 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
41 |
|
* in the top-level source directory and their institutional affiliations. |
42 |
|
* All rights reserved. See the file COPYING in the top-level source |
43 |
|
* directory for licensing information. |
44 |
|
* **************************************************************************** |
45 |
|
* |
46 |
|
* Template for the Node kind header. |
47 |
|
*/ |
48 |
|
|
49 |
|
#include "cvc5_public.h" |
50 |
|
|
51 |
|
#ifndef CVC5__KIND_H |
52 |
|
#define CVC5__KIND_H |
53 |
|
|
54 |
|
#include <iosfwd> |
55 |
|
|
56 |
|
#include "base/exception.h" |
57 |
|
#include "theory/theory_id.h" |
58 |
|
|
59 |
|
namespace cvc5 { |
60 |
|
namespace kind { |
61 |
|
|
62 |
|
enum Kind_t |
63 |
|
{ |
64 |
|
UNDEFINED_KIND = -1, /**< undefined */ |
65 |
|
NULL_EXPR, /**< Null kind */ |
66 |
|
// clang-format off |
67 |
|
|
68 |
|
/* from builtin */ |
69 |
|
SORT_TAG, /**< sort tag (1) */ |
70 |
|
SORT_TYPE, /**< specifies types of user-declared 'uninterpreted' sorts (2) */ |
71 |
|
UNINTERPRETED_CONSTANT, /**< expr/uninterpreted_constant.h (3) */ |
72 |
|
ABSTRACT_VALUE, /**< util/abstract_value.h (4) */ |
73 |
|
BUILTIN, /**< expr/kind.h (5) */ |
74 |
|
EQUAL, /**< equality (two parameters only, sorts must match) (6) */ |
75 |
|
DISTINCT, /**< disequality (N-ary, sorts must match) (7) */ |
76 |
|
VARIABLE, /**< a variable (not permitted in bindings) (8) */ |
77 |
|
BOUND_VARIABLE, /**< a bound variable (permitted in bindings and the associated lambda and quantifier bodies only) (9) */ |
78 |
|
SKOLEM, /**< a Skolem variable (internal only) (10) */ |
79 |
|
SEXPR, /**< a symbolic expression (any arity) (11) */ |
80 |
|
LAMBDA, /**< a lambda expression; first parameter is a BOUND_VAR_LIST, second is lambda body (12) */ |
81 |
|
WITNESS, /**< a witness expression; first parameter is a BOUND_VAR_LIST, second is the witness body (13) */ |
82 |
|
TYPE_CONSTANT, /**< expr/kind.h (14) */ |
83 |
|
FUNCTION_TYPE, /**< a function type (15) */ |
84 |
|
|
85 |
|
/* from booleans */ |
86 |
|
CONST_BOOLEAN, /**< util/bool.h (16) */ |
87 |
|
NOT, /**< logical not (17) */ |
88 |
|
AND, /**< logical and (N-ary) (18) */ |
89 |
|
IMPLIES, /**< logical implication (exactly two parameters) (19) */ |
90 |
|
OR, /**< logical or (N-ary) (20) */ |
91 |
|
XOR, /**< exclusive or (exactly two parameters) (21) */ |
92 |
|
ITE, /**< if-then-else, used for both Boolean and term ITE constructs; first parameter is (Boolean-sorted) condition, second is 'then', third is 'else' and these two parameters must have same base sort (22) */ |
93 |
|
|
94 |
|
/* from uf */ |
95 |
|
APPLY_UF, /**< application of an uninterpreted function; first parameter is the function, remaining ones are parameters to that function (23) */ |
96 |
|
BOOLEAN_TERM_VARIABLE, /**< Boolean term variable (24) */ |
97 |
|
CARDINALITY_CONSTRAINT, /**< cardinality constraint on sort S: first parameter is (any) term of sort S, second is a positive integer constant k that bounds the cardinality of S (25) */ |
98 |
|
COMBINED_CARDINALITY_CONSTRAINT, /**< combined cardinality constraint; parameter is a positive integer constant k that bounds the sum of the cardinalities of all sorts in the signature (26) */ |
99 |
|
PARTIAL_APPLY_UF, /**< partial uninterpreted function application (27) */ |
100 |
|
CARDINALITY_VALUE, /**< cardinality value of sort S: first parameter is (any) term of sort S (28) */ |
101 |
|
HO_APPLY, /**< higher-order (partial) function application (29) */ |
102 |
|
|
103 |
|
/* from arith */ |
104 |
|
PLUS, /**< arithmetic addition (N-ary) (30) */ |
105 |
|
MULT, /**< arithmetic multiplication (N-ary) (31) */ |
106 |
|
NONLINEAR_MULT, /**< synonym for MULT (32) */ |
107 |
|
MINUS, /**< arithmetic binary subtraction operator (33) */ |
108 |
|
UMINUS, /**< arithmetic unary negation (34) */ |
109 |
|
DIVISION, /**< real division, division by 0 undefined (user symbol) (35) */ |
110 |
|
DIVISION_TOTAL, /**< real division with interpreted division by 0 (internal symbol) (36) */ |
111 |
|
INTS_DIVISION, /**< integer division, division by 0 undefined (user symbol) (37) */ |
112 |
|
INTS_DIVISION_TOTAL, /**< integer division with interpreted division by 0 (internal symbol) (38) */ |
113 |
|
INTS_MODULUS, /**< integer modulus, division by 0 undefined (user symbol) (39) */ |
114 |
|
INTS_MODULUS_TOTAL, /**< integer modulus with interpreted division by 0 (internal symbol) (40) */ |
115 |
|
ABS, /**< absolute value (41) */ |
116 |
|
DIVISIBLE, /**< divisibility-by-k predicate; first parameter is a DIVISIBLE_OP, second is integer term (42) */ |
117 |
|
POW, /**< arithmetic power (43) */ |
118 |
|
POW2, /**< arithmetic power of 2 (44) */ |
119 |
|
EXPONENTIAL, /**< exponential (45) */ |
120 |
|
SINE, /**< sine (46) */ |
121 |
|
COSINE, /**< consine (47) */ |
122 |
|
TANGENT, /**< tangent (48) */ |
123 |
|
COSECANT, /**< cosecant (49) */ |
124 |
|
SECANT, /**< secant (50) */ |
125 |
|
COTANGENT, /**< cotangent (51) */ |
126 |
|
ARCSINE, /**< arc sine (52) */ |
127 |
|
ARCCOSINE, /**< arc consine (53) */ |
128 |
|
ARCTANGENT, /**< arc tangent (54) */ |
129 |
|
ARCCOSECANT, /**< arc cosecant (55) */ |
130 |
|
ARCSECANT, /**< arc secant (56) */ |
131 |
|
ARCCOTANGENT, /**< arc cotangent (57) */ |
132 |
|
SQRT, /**< square root (58) */ |
133 |
|
DIVISIBLE_OP, /**< util/divisible.h (59) */ |
134 |
|
CONST_RATIONAL, /**< util/rational.h (60) */ |
135 |
|
LT, /**< less than, x < y (61) */ |
136 |
|
LEQ, /**< less than or equal, x <= y (62) */ |
137 |
|
GT, /**< greater than, x > y (63) */ |
138 |
|
GEQ, /**< greater than or equal, x >= y (64) */ |
139 |
|
INDEXED_ROOT_PREDICATE_OP, /**< util/indexed_root_predicate.h (65) */ |
140 |
|
INDEXED_ROOT_PREDICATE, /**< indexed root predicate; first parameter is a INDEXED_ROOT_PREDICATE_OP, second is a real variable compared to zero, third is a polynomial (66) */ |
141 |
|
IS_INTEGER, /**< term-is-integer predicate (parameter is a real-sorted term) (67) */ |
142 |
|
TO_INTEGER, /**< convert term to integer by the floor function (parameter is a real-sorted term) (68) */ |
143 |
|
TO_REAL, /**< cast term to real (parameter is an integer-sorted term; this is a no-op in cvc5, as integer is a subtype of real) (69) */ |
144 |
|
CAST_TO_REAL, /**< cast term to real same as TO_REAL, but it is used internally, whereas TO_REAL is accessible in the API (70) */ |
145 |
|
PI, /**< pi (71) */ |
146 |
|
IAND_OP, /**< util/iand.h (72) */ |
147 |
|
IAND, /**< integer version of AND operator; first parameter is an IAND_OP, second and third are integer terms (73) */ |
148 |
|
|
149 |
|
/* from bv */ |
150 |
|
BITVECTOR_TYPE, /**< util/bitvector.h (74) */ |
151 |
|
CONST_BITVECTOR, /**< util/bitvector.h (75) */ |
152 |
|
BITVECTOR_BB_TERM, /**< create bit-vector from vector of Booleans (76) */ |
153 |
|
BITVECTOR_CONCAT, /**< concatenation of two or more bit-vectors (77) */ |
154 |
|
BITVECTOR_AND, /**< bitwise and of two or more bit-vectors (78) */ |
155 |
|
BITVECTOR_COMP, /**< equality comparison of two bit-vectors (returns one bit) (79) */ |
156 |
|
BITVECTOR_OR, /**< bitwise or of two or more bit-vectors (80) */ |
157 |
|
BITVECTOR_XOR, /**< bitwise xor of two or more bit-vectors (81) */ |
158 |
|
BITVECTOR_NOT, /**< bitwise not of a bit-vector (82) */ |
159 |
|
BITVECTOR_NAND, /**< bitwise nand of two bit-vectors (83) */ |
160 |
|
BITVECTOR_NOR, /**< bitwise nor of two bit-vectors (84) */ |
161 |
|
BITVECTOR_XNOR, /**< bitwise xnor of two bit-vectors (85) */ |
162 |
|
BITVECTOR_MULT, /**< multiplication of two or more bit-vectors (86) */ |
163 |
|
BITVECTOR_NEG, /**< unary negation of a bit-vector (87) */ |
164 |
|
BITVECTOR_ADD, /**< addition of two or more bit-vectors (88) */ |
165 |
|
BITVECTOR_SUB, /**< subtraction of two bit-vectors (89) */ |
166 |
|
BITVECTOR_UDIV, /**< unsigned division of two bit-vectors, truncating towards 0 (defined to be the all-ones bit pattern, if divisor is 0) (90) */ |
167 |
|
BITVECTOR_UREM, /**< unsigned remainder from truncating division of two bit-vectors (defined to be equal to the dividend, if divisor is 0) (91) */ |
168 |
|
BITVECTOR_SDIV, /**< 2's complement signed division (92) */ |
169 |
|
BITVECTOR_SMOD, /**< 2's complement signed remainder (sign follows divisor) (93) */ |
170 |
|
BITVECTOR_SREM, /**< 2's complement signed remainder (sign follows dividend) (94) */ |
171 |
|
BITVECTOR_ASHR, /**< bit-vector arithmetic shift right (the two bit-vector parameters must have same width) (95) */ |
172 |
|
BITVECTOR_LSHR, /**< bit-vector logical shift right (the two bit-vector parameters must have same width) (96) */ |
173 |
|
BITVECTOR_SHL, /**< bit-vector shift left (the two bit-vector parameters must have same width) (97) */ |
174 |
|
BITVECTOR_ULE, /**< bit-vector unsigned less than or equal (the two bit-vector parameters must have same width) (98) */ |
175 |
|
BITVECTOR_ULT, /**< bit-vector unsigned less than (the two bit-vector parameters must have same width) (99) */ |
176 |
|
BITVECTOR_UGE, /**< bit-vector unsigned greater than or equal (the two bit-vector parameters must have same width) (100) */ |
177 |
|
BITVECTOR_UGT, /**< bit-vector unsigned greater than (the two bit-vector parameters must have same width) (101) */ |
178 |
|
BITVECTOR_SLE, /**< bit-vector signed less than or equal (the two bit-vector parameters must have same width) (102) */ |
179 |
|
BITVECTOR_SLT, /**< bit-vector signed less than (the two bit-vector parameters must have same width) (103) */ |
180 |
|
BITVECTOR_SGE, /**< bit-vector signed greater than or equal (the two bit-vector parameters must have same width) (104) */ |
181 |
|
BITVECTOR_SGT, /**< bit-vector signed greater than (the two bit-vector parameters must have same width) (105) */ |
182 |
|
BITVECTOR_ULTBV, /**< bit-vector unsigned less than but returns bv of size 1 instead of boolean (106) */ |
183 |
|
BITVECTOR_SLTBV, /**< bit-vector signed less than but returns bv of size 1 instead of boolean (107) */ |
184 |
|
BITVECTOR_REDAND, /**< bit-vector redand (108) */ |
185 |
|
BITVECTOR_REDOR, /**< bit-vector redor (109) */ |
186 |
|
BITVECTOR_ITE, /**< same semantics as regular ITE, but condition is bv of size 1 instead of Boolean (110) */ |
187 |
|
BITVECTOR_TO_NAT, /**< bit-vector conversion to (nonnegative) integer; parameter is a bit-vector (111) */ |
188 |
|
BITVECTOR_ACKERMANNIZE_UDIV, /**< term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal-only symbol) (112) */ |
189 |
|
BITVECTOR_ACKERMANNIZE_UREM, /**< term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal-only symbol) (113) */ |
190 |
|
BITVECTOR_EAGER_ATOM, /**< formula to be treated as a bv atom via eager bit-blasting (internal-only symbol) (114) */ |
191 |
|
BITVECTOR_BITOF_OP, /**< util/bitvector.h (115) */ |
192 |
|
BITVECTOR_BITOF, /**< bit-vector boolean bit extract; first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term (116) */ |
193 |
|
BITVECTOR_EXTRACT_OP, /**< util/bitvector.h (117) */ |
194 |
|
BITVECTOR_EXTRACT, /**< bit-vector extract; first parameter is a BITVECTOR_EXTRACT_OP, second is a bit-vector term (118) */ |
195 |
|
BITVECTOR_REPEAT_OP, /**< util/bitvector.h (119) */ |
196 |
|
BITVECTOR_REPEAT, /**< bit-vector repeat; first parameter is a BITVECTOR_REPEAT_OP, second is a bit-vector term (120) */ |
197 |
|
BITVECTOR_ROTATE_LEFT_OP, /**< util/bitvector.h (121) */ |
198 |
|
BITVECTOR_ROTATE_LEFT, /**< bit-vector rotate left; first parameter is a BITVECTOR_ROTATE_LEFT_OP, second is a bit-vector term (122) */ |
199 |
|
BITVECTOR_ROTATE_RIGHT_OP, /**< util/bitvector.h (123) */ |
200 |
|
BITVECTOR_ROTATE_RIGHT, /**< bit-vector rotate right; first parameter is a BITVECTOR_ROTATE_RIGHT_OP, second is a bit-vector term (124) */ |
201 |
|
BITVECTOR_SIGN_EXTEND_OP, /**< util/bitvector.h (125) */ |
202 |
|
BITVECTOR_SIGN_EXTEND, /**< bit-vector sign-extend; first parameter is a BITVECTOR_SIGN_EXTEND_OP, second is a bit-vector term (126) */ |
203 |
|
BITVECTOR_ZERO_EXTEND_OP, /**< util/bitvector.h (127) */ |
204 |
|
BITVECTOR_ZERO_EXTEND, /**< bit-vector zero-extend; first parameter is a BITVECTOR_ZERO_EXTEND_OP, second is a bit-vector term (128) */ |
205 |
|
INT_TO_BITVECTOR_OP, /**< util/bitvector.h (129) */ |
206 |
|
INT_TO_BITVECTOR, /**< integer conversion to bit-vector; first parameter is an INT_TO_BITVECTOR_OP, second is an integer term (130) */ |
207 |
|
|
208 |
|
/* from fp */ |
209 |
|
CONST_FLOATINGPOINT, /**< util/floatingpoint.h (131) */ |
210 |
|
CONST_ROUNDINGMODE, /**< util/roundingmode.h (132) */ |
211 |
|
FLOATINGPOINT_TYPE, /**< util/floatingpoint.h (133) */ |
212 |
|
FLOATINGPOINT_FP, /**< construct a floating-point literal from bit vectors (134) */ |
213 |
|
FLOATINGPOINT_EQ, /**< floating-point equality (135) */ |
214 |
|
FLOATINGPOINT_ABS, /**< floating-point absolute value (136) */ |
215 |
|
FLOATINGPOINT_NEG, /**< floating-point negation (137) */ |
216 |
|
FLOATINGPOINT_ADD, /**< floating-point addition (138) */ |
217 |
|
FLOATINGPOINT_SUB, /**< floating-point sutraction (139) */ |
218 |
|
FLOATINGPOINT_MULT, /**< floating-point multiply (140) */ |
219 |
|
FLOATINGPOINT_DIV, /**< floating-point division (141) */ |
220 |
|
FLOATINGPOINT_FMA, /**< floating-point fused multiply and add (142) */ |
221 |
|
FLOATINGPOINT_SQRT, /**< floating-point square root (143) */ |
222 |
|
FLOATINGPOINT_REM, /**< floating-point remainder (144) */ |
223 |
|
FLOATINGPOINT_RTI, /**< floating-point round to integral (145) */ |
224 |
|
FLOATINGPOINT_MIN, /**< floating-point minimum (146) */ |
225 |
|
FLOATINGPOINT_MAX, /**< floating-point maximum (147) */ |
226 |
|
FLOATINGPOINT_MIN_TOTAL, /**< floating-point minimum (defined for all inputs) (148) */ |
227 |
|
FLOATINGPOINT_MAX_TOTAL, /**< floating-point maximum (defined for all inputs) (149) */ |
228 |
|
FLOATINGPOINT_LEQ, /**< floating-point less than or equal (150) */ |
229 |
|
FLOATINGPOINT_LT, /**< floating-point less than (151) */ |
230 |
|
FLOATINGPOINT_GEQ, /**< floating-point greater than or equal (152) */ |
231 |
|
FLOATINGPOINT_GT, /**< floating-point greater than (153) */ |
232 |
|
FLOATINGPOINT_ISN, /**< floating-point is normal (154) */ |
233 |
|
FLOATINGPOINT_ISSN, /**< floating-point is sub-normal (155) */ |
234 |
|
FLOATINGPOINT_ISZ, /**< floating-point is zero (156) */ |
235 |
|
FLOATINGPOINT_ISINF, /**< floating-point is infinite (157) */ |
236 |
|
FLOATINGPOINT_ISNAN, /**< floating-point is NaN (158) */ |
237 |
|
FLOATINGPOINT_ISNEG, /**< floating-point is negative (159) */ |
238 |
|
FLOATINGPOINT_ISPOS, /**< floating-point is positive (160) */ |
239 |
|
FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, /**< util/floatingpoint.h (161) */ |
240 |
|
FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, /**< convert an IEEE-754 bit vector to floating-point (162) */ |
241 |
|
FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, /**< util/floatingpoint.h (163) */ |
242 |
|
FLOATINGPOINT_TO_FP_FLOATINGPOINT, /**< convert between floating-point sorts (164) */ |
243 |
|
FLOATINGPOINT_TO_FP_REAL_OP, /**< util/floatingpoint.h (165) */ |
244 |
|
FLOATINGPOINT_TO_FP_REAL, /**< convert a real to floating-point (166) */ |
245 |
|
FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, /**< util/floatingpoint.h (167) */ |
246 |
|
FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, /**< convert a signed bit vector to floating-point (168) */ |
247 |
|
FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, /**< util/floatingpoint.h (169) */ |
248 |
|
FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, /**< convert an unsigned bit vector to floating-point (170) */ |
249 |
|
FLOATINGPOINT_TO_FP_GENERIC_OP, /**< util/floatingpoint.h (171) */ |
250 |
|
FLOATINGPOINT_TO_FP_GENERIC, /**< a generic conversion to floating-point, used in parsing only (172) */ |
251 |
|
FLOATINGPOINT_TO_UBV_OP, /**< util/floatingpoint.h (173) */ |
252 |
|
FLOATINGPOINT_TO_UBV, /**< convert a floating-point value to an unsigned bit vector (174) */ |
253 |
|
FLOATINGPOINT_TO_UBV_TOTAL_OP, /**< util/floatingpoint.h (175) */ |
254 |
|
FLOATINGPOINT_TO_UBV_TOTAL, /**< convert a floating-point value to an unsigned bit vector (defined for all inputs) (176) */ |
255 |
|
FLOATINGPOINT_TO_SBV_OP, /**< util/floatingpoint.h (177) */ |
256 |
|
FLOATINGPOINT_TO_SBV, /**< convert a floating-point value to a signed bit vector (178) */ |
257 |
|
FLOATINGPOINT_TO_SBV_TOTAL_OP, /**< util/floatingpoint.h (179) */ |
258 |
|
FLOATINGPOINT_TO_SBV_TOTAL, /**< convert a floating-point value to a signed bit vector (defined for all inputs) (180) */ |
259 |
|
FLOATINGPOINT_TO_REAL, /**< floating-point to real (181) */ |
260 |
|
FLOATINGPOINT_TO_REAL_TOTAL, /**< floating-point to real (defined for all inputs) (182) */ |
261 |
|
FLOATINGPOINT_COMPONENT_NAN, /**< NaN component of a word-blasted floating-point number (183) */ |
262 |
|
FLOATINGPOINT_COMPONENT_INF, /**< Inf component of a word-blasted floating-point number (184) */ |
263 |
|
FLOATINGPOINT_COMPONENT_ZERO, /**< Zero component of a word-blasted floating-point number (185) */ |
264 |
|
FLOATINGPOINT_COMPONENT_SIGN, /**< Sign component of a word-blasted floating-point number (186) */ |
265 |
|
FLOATINGPOINT_COMPONENT_EXPONENT, /**< Exponent component of a word-blasted floating-point number (187) */ |
266 |
|
FLOATINGPOINT_COMPONENT_SIGNIFICAND, /**< Significand component of a word-blasted floating-point number (188) */ |
267 |
|
ROUNDINGMODE_BITBLAST, /**< The bit-vector for a non-deterministic rounding mode (189) */ |
268 |
|
|
269 |
|
/* from arrays */ |
270 |
|
ARRAY_TYPE, /**< array type (190) */ |
271 |
|
SELECT, /**< array select; first parameter is an array term, second is the selection index (191) */ |
272 |
|
STORE, /**< array store; first parameter is an array term, second is the store index, third is the term to store at the index (192) */ |
273 |
|
EQ_RANGE, /**< equality of two arrays over an index range lower/upper (193) */ |
274 |
|
STORE_ALL, /**< expr/array_store_all.h (194) */ |
275 |
|
ARR_TABLE_FUN, /**< array table function (internal-only symbol) (195) */ |
276 |
|
ARRAY_LAMBDA, /**< array lambda (internal-only symbol) (196) */ |
277 |
|
PARTIAL_SELECT_0, /**< partial array select, for internal use only (197) */ |
278 |
|
PARTIAL_SELECT_1, /**< partial array select, for internal use only (198) */ |
279 |
|
|
280 |
|
/* from datatypes */ |
281 |
|
CONSTRUCTOR_TYPE, /**< constructor (199) */ |
282 |
|
SELECTOR_TYPE, /**< selector (200) */ |
283 |
|
TESTER_TYPE, /**< tester (201) */ |
284 |
|
UPDATER_TYPE, /**< datatype update (202) */ |
285 |
|
APPLY_CONSTRUCTOR, /**< constructor application; first parameter is the constructor, remaining parameters (if any) are parameters to the constructor (203) */ |
286 |
|
APPLY_SELECTOR, /**< selector application; parameter is a datatype term (undefined if mis-applied) (204) */ |
287 |
|
APPLY_SELECTOR_TOTAL, /**< selector application; parameter is a datatype term (defined rigidly if mis-applied) (205) */ |
288 |
|
APPLY_TESTER, /**< tester application; first parameter is a tester, second is a datatype term (206) */ |
289 |
|
APPLY_UPDATER, /**< datatype updater application; first parameter is an update, second is a datatype term to update, third is the value to update with (207) */ |
290 |
|
DATATYPE_TYPE, /**< expr/datatype_index.h (208) */ |
291 |
|
PARAMETRIC_DATATYPE, /**< parametric datatype (209) */ |
292 |
|
APPLY_TYPE_ASCRIPTION, /**< type ascription, for datatype constructor applications; first parameter is an ASCRIPTION_TYPE, second is the datatype constructor application being ascribed (210) */ |
293 |
|
ASCRIPTION_TYPE, /**< expr/ascription_type.h (211) */ |
294 |
|
DT_SIZE, /**< datatypes size (212) */ |
295 |
|
DT_HEIGHT_BOUND, /**< datatypes height bound (213) */ |
296 |
|
DT_SIZE_BOUND, /**< datatypes height bound (214) */ |
297 |
|
DT_SYGUS_BOUND, /**< datatypes sygus bound (215) */ |
298 |
|
DT_SYGUS_EVAL, /**< datatypes sygus evaluation function (216) */ |
299 |
|
MATCH, /**< match construct (217) */ |
300 |
|
MATCH_CASE, /**< a match case (218) */ |
301 |
|
MATCH_BIND_CASE, /**< a match case with bound variables (219) */ |
302 |
|
TUPLE_PROJECT_OP, /**< theory/datatypes/tuple_project_op.h (220) */ |
303 |
|
TUPLE_PROJECT, /**< projects a tuple from an existing tuple using indices passed in TupleProjectOp (221) */ |
304 |
|
|
305 |
|
/* from sep */ |
306 |
|
SEP_NIL, /**< separation nil (222) */ |
307 |
|
SEP_EMP, /**< separation empty heap (223) */ |
308 |
|
SEP_PTO, /**< points to relation (224) */ |
309 |
|
SEP_STAR, /**< separation star (225) */ |
310 |
|
SEP_WAND, /**< separation magic wand (226) */ |
311 |
|
SEP_LABEL, /**< separation label (internal use only) (227) */ |
312 |
|
|
313 |
|
/* from sets */ |
314 |
|
EMPTYSET, /**< expr/emptyset.h (228) */ |
315 |
|
SET_TYPE, /**< set type, takes as parameter the type of the elements (229) */ |
316 |
|
UNION, /**< set union (230) */ |
317 |
|
INTERSECTION, /**< set intersection (231) */ |
318 |
|
SETMINUS, /**< set subtraction (232) */ |
319 |
|
SUBSET, /**< subset predicate; first parameter a subset of second (233) */ |
320 |
|
MEMBER, /**< set membership predicate; first parameter a member of second (234) */ |
321 |
|
SINGLETON_OP, /**< theory/sets/singleton_op.h (235) */ |
322 |
|
SINGLETON, /**< constructs a set of a single element. First parameter is a SingletonOp. Second is a term (236) */ |
323 |
|
INSERT, /**< set obtained by inserting elements (first N-1 parameters) into a set (the last parameter) (237) */ |
324 |
|
CARD, /**< set cardinality operator (238) */ |
325 |
|
COMPLEMENT, /**< set COMPLEMENT (with respect to finite universe) (239) */ |
326 |
|
UNIVERSE_SET, /**< (finite) universe set, all set variables must be interpreted as subsets of it. (240) */ |
327 |
|
COMPREHENSION, /**< set comprehension specified by a bound variable list, a predicate, and a term. (241) */ |
328 |
|
CHOOSE, /**< return an element in the set given as a parameter (242) */ |
329 |
|
IS_SINGLETON, /**< return whether the given set is a singleton (243) */ |
330 |
|
JOIN, /**< set join (244) */ |
331 |
|
PRODUCT, /**< set cartesian product (245) */ |
332 |
|
TRANSPOSE, /**< set transpose (246) */ |
333 |
|
TCLOSURE, /**< set transitive closure (247) */ |
334 |
|
JOIN_IMAGE, /**< set join image (248) */ |
335 |
|
IDEN, /**< set identity (249) */ |
336 |
|
|
337 |
|
/* from bags */ |
338 |
|
EMPTYBAG, /**< expr/emptybag.h (250) */ |
339 |
|
BAG_TYPE, /**< bag type, takes as parameter the type of the elements (251) */ |
340 |
|
UNION_MAX, /**< union for bags (max) (252) */ |
341 |
|
UNION_DISJOINT, /**< disjoint union for bags (sum) (253) */ |
342 |
|
INTERSECTION_MIN, /**< bag intersection (min) (254) */ |
343 |
|
DIFFERENCE_SUBTRACT, /**< bag difference1 (subtracts multiplicities) (255) */ |
344 |
|
DIFFERENCE_REMOVE, /**< bag difference remove (removes shared elements) (256) */ |
345 |
|
SUBBAG, /**< inclusion predicate for bags (less than or equal multiplicities) (257) */ |
346 |
|
BAG_COUNT, /**< multiplicity of an element in a bag (258) */ |
347 |
|
DUPLICATE_REMOVAL, /**< eliminate duplicates in a bag (also known as the delta operator,or the squash operator) (259) */ |
348 |
|
MK_BAG_OP, /**< theory/bags/make_bag_op.h (260) */ |
349 |
|
MK_BAG, /**< constructs a bag from one element along with its multiplicity (261) */ |
350 |
|
BAG_IS_SINGLETON, /**< return whether the given bag is a singleton (262) */ |
351 |
|
BAG_CARD, /**< bag cardinality operator (263) */ |
352 |
|
BAG_FROM_SET, /**< converts a set to a bag (264) */ |
353 |
|
BAG_TO_SET, /**< converts a bag to a set (265) */ |
354 |
|
BAG_CHOOSE, /**< return an element in the bag given as a parameter (266) */ |
355 |
|
BAG_MAP, /**< bag map function (267) */ |
356 |
|
|
357 |
|
/* from strings */ |
358 |
|
STRING_CONCAT, /**< string concat (N-ary) (268) */ |
359 |
|
STRING_IN_REGEXP, /**< membership (269) */ |
360 |
|
STRING_LENGTH, /**< string length (270) */ |
361 |
|
STRING_SUBSTR, /**< string substr (271) */ |
362 |
|
STRING_UPDATE, /**< string update (272) */ |
363 |
|
STRING_CHARAT, /**< string charat (273) */ |
364 |
|
STRING_CONTAINS, /**< string contains (274) */ |
365 |
|
STRING_LT, /**< string less than (275) */ |
366 |
|
STRING_LEQ, /**< string less than or equal (276) */ |
367 |
|
STRING_INDEXOF, /**< string index of substring (277) */ |
368 |
|
STRING_INDEXOF_RE, /**< string index of regular expression match (278) */ |
369 |
|
STRING_REPLACE, /**< string replace (279) */ |
370 |
|
STRING_REPLACE_ALL, /**< string replace all (280) */ |
371 |
|
STRING_REPLACE_RE, /**< string replace regular expression match (281) */ |
372 |
|
STRING_REPLACE_RE_ALL, /**< string replace all regular expression matches (282) */ |
373 |
|
STRING_PREFIX, /**< string prefixof (283) */ |
374 |
|
STRING_SUFFIX, /**< string suffixof (284) */ |
375 |
|
STRING_IS_DIGIT, /**< string isdigit, returns true if argument is a string of length one that represents a digit (285) */ |
376 |
|
STRING_ITOS, /**< integer to string (286) */ |
377 |
|
STRING_STOI, /**< string to integer (total function) (287) */ |
378 |
|
STRING_TO_CODE, /**< string to code, returns the code of the first character of the string if it has length one, -1 otherwise (288) */ |
379 |
|
STRING_FROM_CODE, /**< string from code, returns a string containing a single character whose code point matches the argument to this function, empty string if the argument is out-of-bounds (289) */ |
380 |
|
STRING_TOLOWER, /**< string to lowercase conversion (290) */ |
381 |
|
STRING_TOUPPER, /**< string to uppercase conversion (291) */ |
382 |
|
STRING_REV, /**< string reverse (292) */ |
383 |
|
CONST_STRING, /**< util/string.h (293) */ |
384 |
|
SEQUENCE_TYPE, /**< seuence type, takes as parameter the type of the elements (294) */ |
385 |
|
CONST_SEQUENCE, /**< expr/sequence.h (295) */ |
386 |
|
SEQ_UNIT, /**< a sequence of length one (296) */ |
387 |
|
SEQ_NTH, /**< The nth element of a sequence (297) */ |
388 |
|
SEQ_NTH_TOTAL, /**< The nth element of a sequence (internal, for responses to expand definitions only) (298) */ |
389 |
|
STRING_TO_REGEXP, /**< convert string to regexp (299) */ |
390 |
|
REGEXP_CONCAT, /**< regexp concat (300) */ |
391 |
|
REGEXP_UNION, /**< regexp union (301) */ |
392 |
|
REGEXP_INTER, /**< regexp intersection (302) */ |
393 |
|
REGEXP_DIFF, /**< regexp difference (303) */ |
394 |
|
REGEXP_STAR, /**< regexp * (304) */ |
395 |
|
REGEXP_PLUS, /**< regexp + (305) */ |
396 |
|
REGEXP_OPT, /**< regexp ? (306) */ |
397 |
|
REGEXP_RANGE, /**< regexp range (307) */ |
398 |
|
REGEXP_COMPLEMENT, /**< regexp complement (308) */ |
399 |
|
REGEXP_EMPTY, /**< regexp empty (309) */ |
400 |
|
REGEXP_SIGMA, /**< regexp all characters (310) */ |
401 |
|
REGEXP_REPEAT_OP, /**< util/regexp.h (311) */ |
402 |
|
REGEXP_REPEAT, /**< regular expression repeat; first parameter is a REGEXP_REPEAT_OP, second is a regular expression term (312) */ |
403 |
|
REGEXP_LOOP_OP, /**< util/regexp.h (313) */ |
404 |
|
REGEXP_LOOP, /**< regular expression loop; first parameter is a REGEXP_LOOP_OP, second is a regular expression term (314) */ |
405 |
|
REGEXP_RV, /**< regexp rv (internal use only) (315) */ |
406 |
|
|
407 |
|
/* from quantifiers */ |
408 |
|
FORALL, /**< universally quantified formula; first parameter is an BOUND_VAR_LIST, second is quantifier body, and an optional third parameter is an INST_PATTERN_LIST (316) */ |
409 |
|
EXISTS, /**< existentially quantified formula; first parameter is an BOUND_VAR_LIST, second is quantifier body, and an optional third parameter is an INST_PATTERN_LIST (317) */ |
410 |
|
INST_CONSTANT, /**< instantiation constant (318) */ |
411 |
|
BOUND_VAR_LIST, /**< a list of bound variables (used to bind variables under a quantifier) (319) */ |
412 |
|
INST_PATTERN, /**< instantiation pattern (320) */ |
413 |
|
INST_NO_PATTERN, /**< instantiation no-pattern (321) */ |
414 |
|
INST_ATTRIBUTE, /**< instantiation attribute (322) */ |
415 |
|
INST_POOL, /**< instantiation pool (323) */ |
416 |
|
INST_ADD_TO_POOL, /**< instantiation add to pool (324) */ |
417 |
|
SKOLEM_ADD_TO_POOL, /**< skolemization add to pool (325) */ |
418 |
|
INST_PATTERN_LIST, /**< a list of instantiation patterns (326) */ |
419 |
|
LAST_KIND /**< marks the upper-bound of this enumeration */ |
420 |
|
// clang-format on |
421 |
|
|
422 |
|
}; /* enum Kind_t */ |
423 |
|
|
424 |
|
} // namespace kind |
425 |
|
|
426 |
|
// import Kind into the "cvc5" namespace but keep the individual kind |
427 |
|
// constants under kind:: |
428 |
|
typedef ::cvc5::kind::Kind_t Kind; |
429 |
|
|
430 |
|
namespace kind { |
431 |
|
|
432 |
|
/** |
433 |
|
* Converts an kind to a string. Note: This function is also used in |
434 |
|
* `safe_print()`. Changing this functions name or signature will result in |
435 |
|
* `safe_print()` printing "<unsupported>" instead of the proper strings for |
436 |
|
* the enum values. |
437 |
|
* |
438 |
|
* @param k The kind |
439 |
|
* @return The name of the kind |
440 |
|
*/ |
441 |
|
const char* toString(cvc5::Kind k); |
442 |
|
|
443 |
|
/** |
444 |
|
* Writes a kind name to a stream. |
445 |
|
* |
446 |
|
* @param out The stream to write to |
447 |
|
* @param k The kind to write to the stream |
448 |
|
* @return The stream |
449 |
|
*/ |
450 |
|
std::ostream& operator<<(std::ostream&, cvc5::Kind); |
451 |
|
|
452 |
|
/** Returns true if the given kind is associative. This is used by ExprManager to |
453 |
|
* decide whether it's safe to modify big expressions by changing the grouping of |
454 |
|
* the arguments. */ |
455 |
|
/* TODO: This could be generated. */ |
456 |
|
bool isAssociative(::cvc5::Kind k); |
457 |
|
std::string kindToString(::cvc5::Kind k); |
458 |
|
|
459 |
|
struct KindHashFunction |
460 |
|
{ |
461 |
15985840 |
inline size_t operator()(::cvc5::Kind k) const { return k; } |
462 |
|
}; /* struct KindHashFunction */ |
463 |
|
|
464 |
|
} // namespace kind |
465 |
|
|
466 |
|
/** |
467 |
|
* The enumeration for the built-in atomic types. |
468 |
|
*/ |
469 |
|
enum TypeConstant |
470 |
|
{ |
471 |
|
// clang-format off |
472 |
|
BUILTIN_OPERATOR_TYPE, /**< the type for built-in operators */ |
473 |
|
SEXPR_TYPE, /**< the type of a symbolic expression */ |
474 |
|
BOOLEAN_TYPE, /**< Boolean type */ |
475 |
|
REAL_TYPE, /**< real type */ |
476 |
|
INTEGER_TYPE, /**< integer type */ |
477 |
|
ROUNDINGMODE_TYPE, /**< floating-point rounding mode */ |
478 |
|
STRING_TYPE, /**< String type */ |
479 |
|
REGEXP_TYPE, /**< RegExp type */ |
480 |
|
BOUND_VAR_LIST_TYPE, /**< the type of bound variable lists */ |
481 |
|
INST_PATTERN_TYPE, /**< instantiation pattern type */ |
482 |
|
INST_PATTERN_LIST_TYPE, /**< the type of instantiation pattern lists */ |
483 |
|
LAST_TYPE |
484 |
|
// clang-format on |
485 |
|
}; /* enum TypeConstant */ |
486 |
|
|
487 |
|
/** |
488 |
|
* We hash the constants with their values. |
489 |
|
*/ |
490 |
|
struct TypeConstantHashFunction |
491 |
|
{ |
492 |
31302168 |
inline size_t operator()(TypeConstant tc) const { return tc; } |
493 |
|
}; /* struct TypeConstantHashFunction */ |
494 |
|
|
495 |
|
const char* toString(TypeConstant tc); |
496 |
|
std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant); |
497 |
|
|
498 |
|
namespace theory { |
499 |
|
|
500 |
|
::cvc5::theory::TheoryId kindToTheoryId(::cvc5::Kind k); |
501 |
|
::cvc5::theory::TheoryId typeConstantToTheoryId( |
502 |
|
::cvc5::TypeConstant typeConstant); |
503 |
|
|
504 |
|
} // namespace theory |
505 |
|
} // namespace cvc5 |
506 |
|
|
507 |
|
#endif /* CVC5__KIND_H */ |