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