z3_sys/generated/enums.rs
1// Auto-generated by z3-sys bindgen feature — do not edit manually.
2
3/// The different kinds of symbol.
4/// In Z3, a symbol can be represented using integers and strings (See [`Z3_get_symbol_kind`]).
5///
6/// # See also
7///
8/// - [`Z3_mk_int_symbol`]
9/// - [`Z3_mk_string_symbol`]
10#[doc(alias = "Z3_symbol_kind")]
11#[repr(u32)]
12#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)]
13pub enum SymbolKind {
14 /// Corresponds to `Z3_INT_SYMBOL` in the C API.
15 #[doc(alias = "Z3_INT_SYMBOL")]
16 Int = 0,
17 /// Corresponds to `Z3_STRING_SYMBOL` in the C API.
18 #[doc(alias = "Z3_STRING_SYMBOL")]
19 String = 1,
20}
21pub type Z3_symbol_kind = SymbolKind;
22/// The different kinds of parameters that can be associated with function symbols.
23///
24/// # See also
25///
26/// - [`Z3_get_decl_num_parameters`]
27/// - [`Z3_get_decl_parameter_kind`]
28#[doc(alias = "Z3_parameter_kind")]
29#[repr(u32)]
30#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)]
31pub enum ParameterKind {
32 /// used for integer parameters.
33 #[doc(alias = "Z3_PARAMETER_INT")]
34 Int = 0,
35 /// used for double parameters.
36 #[doc(alias = "Z3_PARAMETER_DOUBLE")]
37 Double = 1,
38 /// used for parameters that are rational numbers.
39 #[doc(alias = "Z3_PARAMETER_RATIONAL")]
40 Rational = 2,
41 /// used for parameters that are symbols.
42 #[doc(alias = "Z3_PARAMETER_SYMBOL")]
43 Symbol = 3,
44 /// used for sort parameters.
45 #[doc(alias = "Z3_PARAMETER_SORT")]
46 Sort = 4,
47 /// used for expression parameters.
48 #[doc(alias = "Z3_PARAMETER_AST")]
49 Ast = 5,
50 /// used for function declaration parameters.
51 #[doc(alias = "Z3_PARAMETER_FUNC_DECL")]
52 FuncDecl = 6,
53 /// used for parameters that are private to Z3. They cannot be accessed.
54 #[doc(alias = "Z3_PARAMETER_INTERNAL")]
55 Internal = 7,
56 /// used for string parameters.
57 #[doc(alias = "Z3_PARAMETER_ZSTRING")]
58 Zstring = 8,
59}
60pub type Z3_parameter_kind = ParameterKind;
61/// The different kinds of Z3 types (See [`Z3_get_sort_kind`]).
62#[doc(alias = "Z3_sort_kind")]
63#[repr(u32)]
64#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)]
65pub enum SortKind {
66 /// Corresponds to `Z3_UNINTERPRETED_SORT` in the C API.
67 #[doc(alias = "Z3_UNINTERPRETED_SORT")]
68 Uninterpreted = 0,
69 /// Corresponds to `Z3_BOOL_SORT` in the C API.
70 #[doc(alias = "Z3_BOOL_SORT")]
71 Bool = 1,
72 /// Corresponds to `Z3_INT_SORT` in the C API.
73 #[doc(alias = "Z3_INT_SORT")]
74 Int = 2,
75 /// Corresponds to `Z3_REAL_SORT` in the C API.
76 #[doc(alias = "Z3_REAL_SORT")]
77 Real = 3,
78 /// Corresponds to `Z3_BV_SORT` in the C API.
79 #[doc(alias = "Z3_BV_SORT")]
80 Bv = 4,
81 /// Corresponds to `Z3_ARRAY_SORT` in the C API.
82 #[doc(alias = "Z3_ARRAY_SORT")]
83 Array = 5,
84 /// Corresponds to `Z3_DATATYPE_SORT` in the C API.
85 #[doc(alias = "Z3_DATATYPE_SORT")]
86 Datatype = 6,
87 /// Corresponds to `Z3_RELATION_SORT` in the C API.
88 #[doc(alias = "Z3_RELATION_SORT")]
89 Relation = 7,
90 /// Corresponds to `Z3_FINITE_DOMAIN_SORT` in the C API.
91 #[doc(alias = "Z3_FINITE_DOMAIN_SORT")]
92 FiniteDomain = 8,
93 /// Corresponds to `Z3_FLOATING_POINT_SORT` in the C API.
94 #[doc(alias = "Z3_FLOATING_POINT_SORT")]
95 FloatingPoint = 9,
96 /// Corresponds to `Z3_ROUNDING_MODE_SORT` in the C API.
97 #[doc(alias = "Z3_ROUNDING_MODE_SORT")]
98 RoundingMode = 10,
99 /// Corresponds to `Z3_SEQ_SORT` in the C API.
100 #[doc(alias = "Z3_SEQ_SORT")]
101 Seq = 11,
102 /// Corresponds to `Z3_RE_SORT` in the C API.
103 #[doc(alias = "Z3_RE_SORT")]
104 Re = 12,
105 /// Corresponds to `Z3_CHAR_SORT` in the C API.
106 #[doc(alias = "Z3_CHAR_SORT")]
107 Char = 13,
108 /// Corresponds to `Z3_TYPE_VAR` in the C API.
109 #[doc(alias = "Z3_TYPE_VAR")]
110 TypeVar = 14,
111 /// Corresponds to `Z3_UNKNOWN_SORT` in the C API.
112 #[doc(alias = "Z3_UNKNOWN_SORT")]
113 Unknown = 1000,
114}
115pub type Z3_sort_kind = SortKind;
116/// The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
117#[doc(alias = "Z3_ast_kind")]
118#[repr(u32)]
119#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)]
120pub enum AstKind {
121 /// numeral constants
122 #[doc(alias = "Z3_NUMERAL_AST")]
123 Numeral = 0,
124 /// constant and applications
125 #[doc(alias = "Z3_APP_AST")]
126 App = 1,
127 /// bound variables
128 #[doc(alias = "Z3_VAR_AST")]
129 Var = 2,
130 /// quantifiers
131 #[doc(alias = "Z3_QUANTIFIER_AST")]
132 Quantifier = 3,
133 /// sort
134 #[doc(alias = "Z3_SORT_AST")]
135 Sort = 4,
136 /// function declaration
137 #[doc(alias = "Z3_FUNC_DECL_AST")]
138 FuncDecl = 5,
139 /// internal
140 #[doc(alias = "Z3_UNKNOWN_AST")]
141 Unknown = 1000,
142}
143pub type Z3_ast_kind = AstKind;
144/// The different kinds of interpreted function kinds.
145#[doc(alias = "Z3_decl_kind")]
146#[repr(u32)]
147#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)]
148pub enum DeclKind {
149 /// The constant true.
150 #[doc(alias = "Z3_OP_TRUE")]
151 True = 256,
152 /// The constant false.
153 #[doc(alias = "Z3_OP_FALSE")]
154 False = 257,
155 /// The equality predicate.
156 #[doc(alias = "Z3_OP_EQ")]
157 Eq = 258,
158 /// The n-ary distinct predicate (every argument is mutually distinct).
159 #[doc(alias = "Z3_OP_DISTINCT")]
160 Distinct = 259,
161 /// The ternary if-then-else term.
162 #[doc(alias = "Z3_OP_ITE")]
163 Ite = 260,
164 /// n-ary conjunction.
165 #[doc(alias = "Z3_OP_AND")]
166 And = 261,
167 /// n-ary disjunction.
168 #[doc(alias = "Z3_OP_OR")]
169 Or = 262,
170 /// equivalence (binary).
171 #[doc(alias = "Z3_OP_IFF")]
172 Iff = 263,
173 /// Exclusive or.
174 #[doc(alias = "Z3_OP_XOR")]
175 Xor = 264,
176 /// Negation.
177 #[doc(alias = "Z3_OP_NOT")]
178 Not = 265,
179 /// Implication.
180 #[doc(alias = "Z3_OP_IMPLIES")]
181 Implies = 266,
182 /// Binary equivalence modulo namings. This binary predicate is used in proof terms.
183 /// It captures equisatisfiability and equivalence modulo renamings.
184 #[doc(alias = "Z3_OP_OEQ")]
185 Oeq = 267,
186 /// Arithmetic numeral.
187 #[doc(alias = "Z3_OP_ANUM")]
188 Anum = 512,
189 /// Arithmetic algebraic numeral. Algebraic numbers are used to represent irrational numbers in Z3.
190 #[doc(alias = "Z3_OP_AGNUM")]
191 Agnum = 513,
192 /// <=.
193 #[doc(alias = "Z3_OP_LE")]
194 Le = 514,
195 /// >=.
196 #[doc(alias = "Z3_OP_GE")]
197 Ge = 515,
198 /// <.
199 #[doc(alias = "Z3_OP_LT")]
200 Lt = 516,
201 /// >.
202 #[doc(alias = "Z3_OP_GT")]
203 Gt = 517,
204 /// Addition - Binary.
205 #[doc(alias = "Z3_OP_ADD")]
206 Add = 518,
207 /// Binary subtraction.
208 #[doc(alias = "Z3_OP_SUB")]
209 Sub = 519,
210 /// Unary minus.
211 #[doc(alias = "Z3_OP_UMINUS")]
212 Uminus = 520,
213 /// Multiplication - Binary.
214 #[doc(alias = "Z3_OP_MUL")]
215 Mul = 521,
216 /// Division - Binary.
217 #[doc(alias = "Z3_OP_DIV")]
218 Div = 522,
219 /// Integer division - Binary.
220 #[doc(alias = "Z3_OP_IDIV")]
221 Idiv = 523,
222 /// Remainder - Binary.
223 #[doc(alias = "Z3_OP_REM")]
224 Rem = 524,
225 /// Modulus - Binary.
226 #[doc(alias = "Z3_OP_MOD")]
227 Mod = 525,
228 /// Coercion of integer to real - Unary.
229 #[doc(alias = "Z3_OP_TO_REAL")]
230 ToReal = 526,
231 /// Coercion of real to integer - Unary.
232 #[doc(alias = "Z3_OP_TO_INT")]
233 ToInt = 527,
234 /// Check if real is also an integer - Unary.
235 #[doc(alias = "Z3_OP_IS_INT")]
236 IsInt = 528,
237 /// Power operator x^y.
238 #[doc(alias = "Z3_OP_POWER")]
239 Power = 529,
240 /// Corresponds to `Z3_OP_ABS` in the C API.
241 #[doc(alias = "Z3_OP_ABS")]
242 Abs = 530,
243 /// Array store. It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j).
244 /// Array store takes at least 3 arguments.
245 #[doc(alias = "Z3_OP_STORE")]
246 Store = 768,
247 /// Array select.
248 #[doc(alias = "Z3_OP_SELECT")]
249 Select = 769,
250 /// The constant array. For example, select(const(v),i) = v holds for every v and i. The function is unary.
251 #[doc(alias = "Z3_OP_CONST_ARRAY")]
252 ConstArray = 770,
253 /// Array map operator.
254 /// It satisfies map\[f](a1,..,a_n)\[i] = f(a1\[i],...,a_n\[i]) for every i.
255 #[doc(alias = "Z3_OP_ARRAY_MAP")]
256 ArrayMap = 771,
257 /// Default value of arrays. For example default(const(v)) = v. The function is unary.
258 #[doc(alias = "Z3_OP_ARRAY_DEFAULT")]
259 ArrayDefault = 772,
260 /// Set union between two Boolean arrays (two arrays whose range type is Boolean). The function is binary.
261 #[doc(alias = "Z3_OP_SET_UNION")]
262 SetUnion = 773,
263 /// Set intersection between two Boolean arrays. The function is binary.
264 #[doc(alias = "Z3_OP_SET_INTERSECT")]
265 SetIntersect = 774,
266 /// Set difference between two Boolean arrays. The function is binary.
267 #[doc(alias = "Z3_OP_SET_DIFFERENCE")]
268 SetDifference = 775,
269 /// Set complement of a Boolean array. The function is unary.
270 #[doc(alias = "Z3_OP_SET_COMPLEMENT")]
271 SetComplement = 776,
272 /// Subset predicate between two Boolean arrays. The relation is binary.
273 #[doc(alias = "Z3_OP_SET_SUBSET")]
274 SetSubset = 777,
275 /// An array value that behaves as the function graph of the
276 /// function passed as parameter.
277 #[doc(alias = "Z3_OP_AS_ARRAY")]
278 AsArray = 778,
279 /// Array extensionality function. It takes two arrays as arguments and produces an index, such that the arrays
280 /// are different if they are different on the index.
281 #[doc(alias = "Z3_OP_ARRAY_EXT")]
282 ArrayExt = 779,
283 /// Bit-vector numeral.
284 #[doc(alias = "Z3_OP_BNUM")]
285 Bnum = 1024,
286 /// One bit bit-vector.
287 #[doc(alias = "Z3_OP_BIT1")]
288 Bit1 = 1025,
289 /// Zero bit bit-vector.
290 #[doc(alias = "Z3_OP_BIT0")]
291 Bit0 = 1026,
292 /// Unary minus.
293 #[doc(alias = "Z3_OP_BNEG")]
294 Bneg = 1027,
295 /// Binary addition.
296 #[doc(alias = "Z3_OP_BADD")]
297 Badd = 1028,
298 /// Binary subtraction.
299 #[doc(alias = "Z3_OP_BSUB")]
300 Bsub = 1029,
301 /// Binary multiplication.
302 #[doc(alias = "Z3_OP_BMUL")]
303 Bmul = 1030,
304 /// Binary signed division.
305 #[doc(alias = "Z3_OP_BSDIV")]
306 Bsdiv = 1031,
307 /// Binary unsigned division.
308 #[doc(alias = "Z3_OP_BUDIV")]
309 Budiv = 1032,
310 /// Binary signed remainder.
311 #[doc(alias = "Z3_OP_BSREM")]
312 Bsrem = 1033,
313 /// Binary unsigned remainder.
314 #[doc(alias = "Z3_OP_BUREM")]
315 Burem = 1034,
316 /// Binary signed modulus.
317 #[doc(alias = "Z3_OP_BSMOD")]
318 Bsmod = 1035,
319 /// Unary function. bsdiv(x,0) is congruent to bsdiv0(x).
320 #[doc(alias = "Z3_OP_BSDIV0")]
321 Bsdiv0 = 1036,
322 /// Unary function. budiv(x,0) is congruent to budiv0(x).
323 #[doc(alias = "Z3_OP_BUDIV0")]
324 Budiv0 = 1037,
325 /// Unary function. bsrem(x,0) is congruent to bsrem0(x).
326 #[doc(alias = "Z3_OP_BSREM0")]
327 Bsrem0 = 1038,
328 /// Unary function. burem(x,0) is congruent to burem0(x).
329 #[doc(alias = "Z3_OP_BUREM0")]
330 Burem0 = 1039,
331 /// Unary function. bsmod(x,0) is congruent to bsmod0(x).
332 #[doc(alias = "Z3_OP_BSMOD0")]
333 Bsmod0 = 1040,
334 /// Unsigned bit-vector <= - Binary relation.
335 #[doc(alias = "Z3_OP_ULEQ")]
336 Uleq = 1041,
337 /// Signed bit-vector <= - Binary relation.
338 #[doc(alias = "Z3_OP_SLEQ")]
339 Sleq = 1042,
340 /// Unsigned bit-vector >= - Binary relation.
341 #[doc(alias = "Z3_OP_UGEQ")]
342 Ugeq = 1043,
343 /// Signed bit-vector >= - Binary relation.
344 #[doc(alias = "Z3_OP_SGEQ")]
345 Sgeq = 1044,
346 /// Unsigned bit-vector < - Binary relation.
347 #[doc(alias = "Z3_OP_ULT")]
348 Ult = 1045,
349 /// Signed bit-vector < - Binary relation.
350 #[doc(alias = "Z3_OP_SLT")]
351 Slt = 1046,
352 /// Unsigned bit-vector > - Binary relation.
353 #[doc(alias = "Z3_OP_UGT")]
354 Ugt = 1047,
355 /// Signed bit-vector > - Binary relation.
356 #[doc(alias = "Z3_OP_SGT")]
357 Sgt = 1048,
358 /// Bit-wise and - Binary.
359 #[doc(alias = "Z3_OP_BAND")]
360 Band = 1049,
361 /// Bit-wise or - Binary.
362 #[doc(alias = "Z3_OP_BOR")]
363 Bor = 1050,
364 /// Bit-wise not - Unary.
365 #[doc(alias = "Z3_OP_BNOT")]
366 Bnot = 1051,
367 /// Bit-wise xor - Binary.
368 #[doc(alias = "Z3_OP_BXOR")]
369 Bxor = 1052,
370 /// Bit-wise nand - Binary.
371 #[doc(alias = "Z3_OP_BNAND")]
372 Bnand = 1053,
373 /// Bit-wise nor - Binary.
374 #[doc(alias = "Z3_OP_BNOR")]
375 Bnor = 1054,
376 /// Bit-wise xnor - Binary.
377 #[doc(alias = "Z3_OP_BXNOR")]
378 Bxnor = 1055,
379 /// Bit-vector concatenation - Binary.
380 #[doc(alias = "Z3_OP_CONCAT")]
381 Concat = 1056,
382 /// Bit-vector sign extension.
383 #[doc(alias = "Z3_OP_SIGN_EXT")]
384 SignExt = 1057,
385 /// Bit-vector zero extension.
386 #[doc(alias = "Z3_OP_ZERO_EXT")]
387 ZeroExt = 1058,
388 /// Bit-vector extraction.
389 #[doc(alias = "Z3_OP_EXTRACT")]
390 Extract = 1059,
391 /// Repeat bit-vector n times.
392 #[doc(alias = "Z3_OP_REPEAT")]
393 Repeat = 1060,
394 /// Bit-vector reduce or - Unary.
395 #[doc(alias = "Z3_OP_BREDOR")]
396 Bredor = 1061,
397 /// Bit-vector reduce and - Unary.
398 #[doc(alias = "Z3_OP_BREDAND")]
399 Bredand = 1062,
400 /// .
401 #[doc(alias = "Z3_OP_BCOMP")]
402 Bcomp = 1063,
403 /// Shift left.
404 #[doc(alias = "Z3_OP_BSHL")]
405 Bshl = 1064,
406 /// Logical shift right.
407 #[doc(alias = "Z3_OP_BLSHR")]
408 Blshr = 1065,
409 /// Arithmetical shift right.
410 #[doc(alias = "Z3_OP_BASHR")]
411 Bashr = 1066,
412 /// Left rotation.
413 #[doc(alias = "Z3_OP_ROTATE_LEFT")]
414 RotateLeft = 1067,
415 /// Right rotation.
416 #[doc(alias = "Z3_OP_ROTATE_RIGHT")]
417 RotateRight = 1068,
418 /// (extended) Left rotation. Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one.
419 #[doc(alias = "Z3_OP_EXT_ROTATE_LEFT")]
420 ExtRotateLeft = 1069,
421 /// (extended) Right rotation. Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one.
422 #[doc(alias = "Z3_OP_EXT_ROTATE_RIGHT")]
423 ExtRotateRight = 1070,
424 /// Corresponds to `Z3_OP_BIT2BOOL` in the C API.
425 #[doc(alias = "Z3_OP_BIT2BOOL")]
426 Bit2bool = 1071,
427 /// Coerce integer to bit-vector.
428 #[doc(alias = "Z3_OP_INT2BV")]
429 Int2bv = 1072,
430 /// Coerce bit-vector to integer.
431 #[doc(alias = "Z3_OP_BV2INT")]
432 Bv2int = 1073,
433 /// Coerce signed bit-vector to integer.
434 #[doc(alias = "Z3_OP_SBV2INT")]
435 Sbv2int = 1074,
436 /// Compute the carry bit in a full-adder.
437 /// The meaning is given by the equivalence
438 /// (carry l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3)))
439 #[doc(alias = "Z3_OP_CARRY")]
440 Carry = 1075,
441 /// Compute ternary XOR.
442 /// The meaning is given by the equivalence
443 /// (xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3)
444 #[doc(alias = "Z3_OP_XOR3")]
445 Xor3 = 1076,
446 /// a predicate to check that bit-wise signed multiplication does not overflow.
447 /// Signed multiplication overflows if the operands have the same sign and the result of multiplication
448 /// does not fit within the available bits. \sa Z3_mk_bvmul_no_overflow.
449 #[doc(alias = "Z3_OP_BSMUL_NO_OVFL")]
450 BsmulNoOvfl = 1077,
451 /// check that bit-wise unsigned multiplication does not overflow.
452 /// Unsigned multiplication overflows if the result does not fit within the available bits.
453 ///
454 /// # See also
455 ///
456 /// - [`Z3_mk_bvmul_no_overflow`]
457 #[doc(alias = "Z3_OP_BUMUL_NO_OVFL")]
458 BumulNoOvfl = 1078,
459 /// check that bit-wise signed multiplication does not underflow.
460 /// Signed multiplication underflows if the operands have opposite signs and the result of multiplication
461 /// does not fit within the available bits. Z3_mk_bvmul_no_underflow.
462 #[doc(alias = "Z3_OP_BSMUL_NO_UDFL")]
463 BsmulNoUdfl = 1079,
464 /// Binary signed division.
465 /// It has the same semantics as Z3_OP_BSDIV, but created in a context where the second operand can be assumed to be non-zero.
466 #[doc(alias = "Z3_OP_BSDIV_I")]
467 BsdivI = 1080,
468 /// Binary unsigned division.
469 /// It has the same semantics as Z3_OP_BUDIV, but created in a context where the second operand can be assumed to be non-zero.
470 #[doc(alias = "Z3_OP_BUDIV_I")]
471 BudivI = 1081,
472 /// Binary signed remainder.
473 /// It has the same semantics as Z3_OP_BSREM, but created in a context where the second operand can be assumed to be non-zero.
474 #[doc(alias = "Z3_OP_BSREM_I")]
475 BsremI = 1082,
476 /// Binary unsigned remainder.
477 /// It has the same semantics as Z3_OP_BUREM, but created in a context where the second operand can be assumed to be non-zero.
478 #[doc(alias = "Z3_OP_BUREM_I")]
479 BuremI = 1083,
480 /// Binary signed modulus.
481 /// It has the same semantics as Z3_OP_BSMOD, but created in a context where the second operand can be assumed to be non-zero.
482 #[doc(alias = "Z3_OP_BSMOD_I")]
483 BsmodI = 1084,
484 /// Undef/Null proof object.
485 #[doc(alias = "Z3_OP_PR_UNDEF")]
486 PrUndef = 1280,
487 /// Proof for the expression 'true'.
488 #[doc(alias = "Z3_OP_PR_TRUE")]
489 PrTrue = 1281,
490 /// Proof for a fact asserted by the user.
491 #[doc(alias = "Z3_OP_PR_ASSERTED")]
492 PrAsserted = 1282,
493 /// Proof for a fact (tagged as goal) asserted by the user.
494 #[doc(alias = "Z3_OP_PR_GOAL")]
495 PrGoal = 1283,
496 /// Given a proof for p and a proof for (implies p q), produces a proof for q.
497 ///
498 /// T1: p
499 /// T2: (implies p q)
500 /// [mp T1 T2]: q
501 ///
502 /// The second antecedents may also be a proof for (iff p q).
503 #[doc(alias = "Z3_OP_PR_MODUS_PONENS")]
504 PrModusPonens = 1284,
505 /// A proof for (R t t), where R is a reflexive relation. This proof object has no antecedents.
506 /// The only reflexive relations that are used are
507 /// equivalence modulo namings, equality and equivalence.
508 /// That is, R is either '~', '=' or 'iff'.
509 #[doc(alias = "Z3_OP_PR_REFLEXIVITY")]
510 PrReflexivity = 1285,
511 /// Given an symmetric relation R and a proof for (R t s), produces a proof for (R s t).
512 /// ```text
513 /// T1: (R t s)
514 /// [symmetry T1]: (R s t)
515 /// ```
516 /// T1 is the antecedent of this proof object.
517 #[doc(alias = "Z3_OP_PR_SYMMETRY")]
518 PrSymmetry = 1286,
519 /// Given a transitive relation R, and proofs for (R t s) and (R s u), produces a proof
520 /// for (R t u).
521 /// ```text
522 /// T1: (R t s)
523 /// T2: (R s u)
524 /// [trans T1 T2]: (R t u)
525 /// ```
526 #[doc(alias = "Z3_OP_PR_TRANSITIVITY")]
527 PrTransitivity = 1287,
528 /// Condensed transitivity proof.
529 /// It combines several symmetry and transitivity proofs. Example:
530 /// ```text
531 /// T1: (R a b)
532 /// T2: (R c b)
533 /// T3: (R c d)
534 /// [trans* T1 T2 T3]: (R a d)
535 /// ```
536 /// R must be a symmetric and transitive relation.
537 ///
538 /// Assuming that this proof object is a proof for (R s t), then
539 /// a proof checker must check if it is possible to prove (R s t)
540 /// using the antecedents, symmetry and transitivity. That is,
541 /// if there is a path from s to t, if we view every
542 /// antecedent (R a b) as an edge between a and b.
543 #[doc(alias = "Z3_OP_PR_TRANSITIVITY_STAR")]
544 PrTransitivityStar = 1288,
545 /// Monotonicity proof object.
546 ///
547 /// T1: (R t_1 s_1)
548 /// ...
549 /// Tn: (R t_n s_n)
550 /// [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n))
551 ///
552 /// Remark: if t_i == s_i, then the antecedent Ti is suppressed.
553 /// That is, reflexivity proofs are suppressed to save space.
554 #[doc(alias = "Z3_OP_PR_MONOTONICITY")]
555 PrMonotonicity = 1289,
556 /// Given a proof for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)).
557 ///
558 /// T1: (~ p q)
559 /// [quant-intro T1]: (~ (forall (x) p) (forall (x) q))
560 #[doc(alias = "Z3_OP_PR_QUANT_INTRO")]
561 PrQuantIntro = 1290,
562 /// Given a proof p, produces a proof of lambda x . p, where x are free variables in p.
563 ///
564 /// T1: f
565 /// [proof-bind T1] forall (x) f
566 #[doc(alias = "Z3_OP_PR_BIND")]
567 PrBind = 1291,
568 /// Distributivity proof object.
569 /// Given that f (= or) distributes over g (= and), produces a proof for
570 /// ```text
571 /// (= (f a (g c d))
572 /// (g (f a c) (f a d)))
573 /// ```
574 /// If f and g are associative, this proof also justifies the following equality:
575 /// ```text
576 /// (= (f (g a b) (g c d))
577 /// (g (f a c) (f a d) (f b c) (f b d)))
578 /// ```
579 /// where each f and g can have arbitrary number of arguments.
580 ///
581 /// This proof object has no antecedents.
582 /// Remark. This rule is used by the CNF conversion pass and
583 /// instantiated by f = or, and g = and.
584 #[doc(alias = "Z3_OP_PR_DISTRIBUTIVITY")]
585 PrDistributivity = 1292,
586 /// Given a proof for (and l_1 ... l_n), produces a proof for l_i
587 ///
588 /// T1: (and l_1 ... l_n)
589 /// [and-elim T1]: l_i
590 #[doc(alias = "Z3_OP_PR_AND_ELIM")]
591 PrAndElim = 1293,
592 /// Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i).
593 ///
594 /// T1: (not (or l_1 ... l_n))
595 /// [not-or-elim T1]: (not l_i)
596 #[doc(alias = "Z3_OP_PR_NOT_OR_ELIM")]
597 PrNotOrElim = 1294,
598 /// A proof for a local rewriting step (= t s).
599 /// The head function symbol of t is interpreted.
600 ///
601 /// This proof object has no antecedents.
602 /// The conclusion of a rewrite rule is either an equality (= t s),
603 /// an equivalence (iff t s), or equi-satisfiability (~ t s).
604 /// Remark: if f is bool, then = is iff.
605 /// Examples:
606 /// ```text
607 /// (= (+ x 0) x)
608 /// (= (+ x 1 2) (+ 3 x))
609 /// (iff (or x false) x)
610 /// ```
611 #[doc(alias = "Z3_OP_PR_REWRITE")]
612 PrRewrite = 1295,
613 /// A proof for rewriting an expression t into an expression s.
614 /// This proof object can have n antecedents.
615 /// The antecedents are proofs for equalities used as substitution rules.
616 /// The proof rule is used in a few cases. The cases are:
617 /// - When applying contextual simplification (CONTEXT_SIMPLIFIER=true)
618 /// - When converting bit-vectors to Booleans (BIT2BOOL=true)
619 #[doc(alias = "Z3_OP_PR_REWRITE_STAR")]
620 PrRewriteStar = 1296,
621 /// A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents.
622 #[doc(alias = "Z3_OP_PR_PULL_QUANT")]
623 PrPullQuant = 1297,
624 /// A proof for:
625 /// ```text
626 /// (iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m] ... p_n[x_1 ... x_m]))
627 /// (and (forall (x_1 ... x_m) p_1[x_1 ... x_m])
628 /// ...
629 /// (forall (x_1 ... x_m) p_n[x_1 ... x_m])))
630 /// ```
631 /// This proof object has no antecedents.
632 #[doc(alias = "Z3_OP_PR_PUSH_QUANT")]
633 PrPushQuant = 1298,
634 /// A proof for (iff (forall (x_1 ... x_n y_1 ... y_m) p[x_1 ... x_n])
635 /// (forall (x_1 ... x_n) p[x_1 ... x_n]))
636 ///
637 /// It is used to justify the elimination of unused variables.
638 /// This proof object has no antecedents.
639 #[doc(alias = "Z3_OP_PR_ELIM_UNUSED_VARS")]
640 PrElimUnusedVars = 1299,
641 /// A proof for destructive equality resolution:
642 /// (iff (forall (x) (or (not (= x t)) P\[x])) P\[t])
643 /// if x does not occur in t.
644 ///
645 /// This proof object has no antecedents.
646 ///
647 /// Several variables can be eliminated simultaneously.
648 #[doc(alias = "Z3_OP_PR_DER")]
649 PrDer = 1300,
650 /// A proof of (or (not (forall (x) (P x))) (P a))
651 #[doc(alias = "Z3_OP_PR_QUANT_INST")]
652 PrQuantInst = 1301,
653 /// Mark a hypothesis in a natural deduction style proof.
654 #[doc(alias = "Z3_OP_PR_HYPOTHESIS")]
655 PrHypothesis = 1302,
656 ///
657 /// T1: false
658 /// [lemma T1]: (or (not l_1) ... (not l_n))
659 ///
660 /// This proof object has one antecedent: a hypothetical proof for false.
661 /// It converts the proof in a proof for (or (not l_1) ... (not l_n)),
662 /// when T1 contains the open hypotheses: l_1, ..., l_n.
663 /// The hypotheses are closed after an application of a lemma.
664 /// Furthermore, there are no other open hypotheses in the subtree covered by
665 /// the lemma.
666 #[doc(alias = "Z3_OP_PR_LEMMA")]
667 PrLemma = 1303,
668 /// ```text
669 /// T1: (or l_1 ... l_n l_1' ... l_m')
670 /// T2: (not l_1)
671 /// ...
672 /// T(n+1): (not l_n)
673 /// [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m')
674 /// ```
675 #[doc(alias = "Z3_OP_PR_UNIT_RESOLUTION")]
676 PrUnitResolution = 1304,
677 /// ```text
678 /// T1: p
679 /// [iff-true T1]: (iff p true)
680 /// ```
681 #[doc(alias = "Z3_OP_PR_IFF_TRUE")]
682 PrIffTrue = 1305,
683 /// ```text
684 /// T1: (not p)
685 /// [iff-false T1]: (iff p false)
686 /// ```
687 #[doc(alias = "Z3_OP_PR_IFF_FALSE")]
688 PrIffFalse = 1306,
689 ///
690 /// \[comm\]: (= (f a b) (f b a))
691 ///
692 /// f is a commutative operator.
693 ///
694 /// This proof object has no antecedents.
695 /// Remark: if f is bool, then = is iff.
696 #[doc(alias = "Z3_OP_PR_COMMUTATIVITY")]
697 PrCommutativity = 1307,
698 /// Proof object used to justify Tseitin's like axioms:
699 /// ```text
700 /// (or (not (and p q)) p)
701 /// (or (not (and p q)) q)
702 /// (or (not (and p q r)) p)
703 /// (or (not (and p q r)) q)
704 /// (or (not (and p q r)) r)
705 /// ...
706 /// (or (and p q) (not p) (not q))
707 /// (or (not (or p q)) p q)
708 /// (or (or p q) (not p))
709 /// (or (or p q) (not q))
710 /// (or (not (iff p q)) (not p) q)
711 /// (or (not (iff p q)) p (not q))
712 /// (or (iff p q) (not p) (not q))
713 /// (or (iff p q) p q)
714 /// (or (not (ite a b c)) (not a) b)
715 /// (or (not (ite a b c)) a c)
716 /// (or (ite a b c) (not a) (not b))
717 /// (or (ite a b c) a (not c))
718 /// (or (not (not a)) (not a))
719 /// (or (not a) a)
720 /// ```
721 /// This proof object has no antecedents.
722 /// Note: all axioms are propositional tautologies.
723 /// Note also that 'and' and 'or' can take multiple arguments.
724 /// You can recover the propositional tautologies by
725 /// unfolding the Boolean connectives in the axioms a small
726 /// bounded number of steps (=3).
727 #[doc(alias = "Z3_OP_PR_DEF_AXIOM")]
728 PrDefAxiom = 1308,
729 /// Clausal proof adding axiom
730 #[doc(alias = "Z3_OP_PR_ASSUMPTION_ADD")]
731 PrAssumptionAdd = 1309,
732 /// Clausal proof lemma addition
733 #[doc(alias = "Z3_OP_PR_LEMMA_ADD")]
734 PrLemmaAdd = 1310,
735 /// Clausal proof lemma deletion
736 #[doc(alias = "Z3_OP_PR_REDUNDANT_DEL")]
737 PrRedundantDel = 1311,
738 /// ,
739 /// Clausal proof trail of additions and deletions
740 #[doc(alias = "Z3_OP_PR_CLAUSE_TRAIL")]
741 PrClauseTrail = 1312,
742 /// Introduces a name for a formula/term.
743 /// Suppose e is an expression with free variables x, and def-intro
744 /// introduces the name n(x). The possible cases are:
745 ///
746 /// When e is of Boolean type:
747 /// \[def-intro\]: (and (or n (not e)) (or (not n) e))
748 ///
749 /// or:
750 /// \[def-intro\]: (or (not n) e)
751 /// when e only occurs positively.
752 ///
753 /// When e is of the form (ite cond th el):
754 /// \[def-intro\]: (and (or (not cond) (= n th)) (or cond (= n el)))
755 ///
756 /// Otherwise:
757 /// \[def-intro\]: (= n e)
758 #[doc(alias = "Z3_OP_PR_DEF_INTRO")]
759 PrDefIntro = 1313,
760 ///
761 /// [apply-def T1]: F ~ n
762 ///
763 /// F is 'equivalent' to n, given that T1 is a proof that
764 /// n is a name for F.
765 #[doc(alias = "Z3_OP_PR_APPLY_DEF")]
766 PrApplyDef = 1314,
767 ///
768 /// T1: (iff p q)
769 /// [iff~ T1]: (~ p q)
770 #[doc(alias = "Z3_OP_PR_IFF_OEQ")]
771 PrIffOeq = 1315,
772 /// Proof for a (positive) NNF step. Example:
773 ///
774 /// T1: (not s_1) ~ r_1
775 /// T2: (not s_2) ~ r_2
776 /// T3: s_1 ~ r_1'
777 /// T4: s_2 ~ r_2'
778 /// [nnf-pos T1 T2 T3 T4]: (~ (iff s_1 s_2) (and (or r_1 r_2') (or r_1' r_2)))
779 ///
780 /// The negation normal form steps NNF_POS and NNF_NEG are used in the following cases:
781 /// (a) When creating the NNF of a positive force quantifier.
782 /// The quantifier is retained (unless the bound variables are eliminated).
783 /// Example
784 ///
785 /// T1: q ~ q_new
786 /// [nnf-pos T1]: (~ (forall (x T) q) (forall (x T) q_new))
787 ///
788 /// (b) When recursively creating NNF over Boolean formulas, where the top-level
789 /// connective is changed during NNF conversion. The relevant Boolean connectives
790 /// for NNF_POS are 'implies', 'iff', 'xor', 'ite'.
791 /// NNF_NEG furthermore handles the case where negation is pushed
792 /// over Boolean connectives 'and' and 'or'.
793 #[doc(alias = "Z3_OP_PR_NNF_POS")]
794 PrNnfPos = 1316,
795 /// Proof for a (negative) NNF step. Examples:
796 ///
797 /// T1: (not s_1) ~ r_1
798 /// ...
799 /// Tn: (not s_n) ~ r_n
800 /// [nnf-neg T1 ... Tn]: (not (and s_1 ... s_n)) ~ (or r_1 ... r_n)
801 ///
802 /// and
803 ///
804 /// T1: (not s_1) ~ r_1
805 /// ...
806 /// Tn: (not s_n) ~ r_n
807 /// [nnf-neg T1 ... Tn]: (not (or s_1 ... s_n)) ~ (and r_1 ... r_n)
808 ///
809 /// and
810 ///
811 /// T1: (not s_1) ~ r_1
812 /// T2: (not s_2) ~ r_2
813 /// T3: s_1 ~ r_1'
814 /// T4: s_2 ~ r_2'
815 /// [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2))
816 /// (and (or r_1 r_2) (or r_1' r_2')))
817 #[doc(alias = "Z3_OP_PR_NNF_NEG")]
818 PrNnfNeg = 1317,
819 /// Proof for:
820 ///
821 /// \[sk\]: (~ (not (forall x (p x y))) (not (p (sk y) y)))
822 /// \[sk\]: (~ (exists x (p x y)) (p (sk y) y))
823 ///
824 /// This proof object has no antecedents.
825 #[doc(alias = "Z3_OP_PR_SKOLEMIZE")]
826 PrSkolemize = 1318,
827 /// Modus ponens style rule for equi-satisfiability.
828 ///
829 /// T1: p
830 /// T2: (~ p q)
831 /// [mp~ T1 T2]: q
832 #[doc(alias = "Z3_OP_PR_MODUS_PONENS_OEQ")]
833 PrModusPonensOeq = 1319,
834 /// Generic proof for theory lemmas.
835 /// The theory lemma function comes with one or more parameters.
836 /// The first parameter indicates the name of the theory.
837 /// For the theory of arithmetic, additional parameters provide hints for
838 /// checking the theory lemma.
839 /// The hints for arithmetic are:
840 ///
841 /// - farkas - followed by rational coefficients. Multiply the coefficients to the
842 /// inequalities in the lemma, add the (negated) inequalities and obtain a contradiction.
843 ///
844 /// - triangle-eq - Indicates a lemma related to the equivalence:
845 ///
846 /// (iff (= t1 t2) (and (<= t1 t2) (<= t2 t1)))
847 ///
848 /// - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test.
849 #[doc(alias = "Z3_OP_PR_TH_LEMMA")]
850 PrThLemma = 1320,
851 /// Hyper-resolution rule.
852 ///
853 /// The premises of the rules is a sequence of clauses.
854 /// The first clause argument is the main clause of the rule.
855 /// with a literal from the first (main) clause.
856 ///
857 /// Premises of the rules are of the form
858 /// ```text
859 /// (or l0 l1 l2 .. ln)
860 /// ```
861 /// or
862 /// ```text
863 /// (=> (and l1 l2 .. ln) l0)
864 /// ```
865 /// or in the most general (ground) form:
866 /// ```text
867 /// (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln))
868 /// ```
869 /// In other words we use the following (Prolog style) convention for Horn
870 /// implications:
871 /// The head of a Horn implication is position 0,
872 /// the first conjunct in the body of an implication is position 1
873 /// the second conjunct in the body of an implication is position 2
874 ///
875 /// For general implications where the head is a disjunction, the
876 /// first n positions correspond to the n disjuncts in the head.
877 /// The next m positions correspond to the m conjuncts in the body.
878 ///
879 /// The premises can be universally quantified so that the most
880 /// general non-ground form is:
881 ///
882 /// ```text
883 /// (forall (vars) (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln)))
884 /// ```
885 ///
886 /// The hyper-resolution rule takes a sequence of parameters.
887 /// The parameters are substitutions of bound variables separated by pairs
888 /// of literal positions from the main clause and side clause.
889 #[doc(alias = "Z3_OP_PR_HYPER_RESOLVE")]
890 PrHyperResolve = 1321,
891 /// Insert a record into a relation.
892 /// The function takes `n`+1 arguments, where the first argument is the relation and the remaining `n` elements
893 /// correspond to the `n` columns of the relation.
894 #[doc(alias = "Z3_OP_RA_STORE")]
895 RaStore = 1536,
896 /// Creates the empty relation.
897 #[doc(alias = "Z3_OP_RA_EMPTY")]
898 RaEmpty = 1537,
899 /// Tests if the relation is empty.
900 #[doc(alias = "Z3_OP_RA_IS_EMPTY")]
901 RaIsEmpty = 1538,
902 /// Create the relational join.
903 #[doc(alias = "Z3_OP_RA_JOIN")]
904 RaJoin = 1539,
905 /// Create the union or convex hull of two relations.
906 /// The function takes two arguments.
907 #[doc(alias = "Z3_OP_RA_UNION")]
908 RaUnion = 1540,
909 /// Widen two relations.
910 /// The function takes two arguments.
911 #[doc(alias = "Z3_OP_RA_WIDEN")]
912 RaWiden = 1541,
913 /// Project the columns (provided as numbers in the parameters).
914 /// The function takes one argument.
915 #[doc(alias = "Z3_OP_RA_PROJECT")]
916 RaProject = 1542,
917 /// Filter (restrict) a relation with respect to a predicate.
918 /// The first argument is a relation.
919 /// The second argument is a predicate with free de-Bruijn indices
920 /// corresponding to the columns of the relation.
921 /// So the first column in the relation has index 0.
922 #[doc(alias = "Z3_OP_RA_FILTER")]
923 RaFilter = 1543,
924 /// Intersect the first relation with respect to negation
925 /// of the second relation (the function takes two arguments).
926 /// Logically, the specification can be described by a function
927 ///
928 /// target = filter_by_negation(pos, neg, columns)
929 ///
930 /// where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, such that
931 /// target are elements in x in pos, such that there is no y in neg that agrees with
932 /// x on the columns c1, d1, .., cN, dN.
933 #[doc(alias = "Z3_OP_RA_NEGATION_FILTER")]
934 RaNegationFilter = 1544,
935 /// rename columns in the relation.
936 /// The function takes one argument.
937 /// The parameters contain the renaming as a cycle.
938 #[doc(alias = "Z3_OP_RA_RENAME")]
939 RaRename = 1545,
940 /// Complement the relation.
941 #[doc(alias = "Z3_OP_RA_COMPLEMENT")]
942 RaComplement = 1546,
943 /// Check if a record is an element of the relation.
944 /// The function takes `n`+1 arguments, where the first argument is a relation,
945 /// and the remaining `n` arguments correspond to a record.
946 #[doc(alias = "Z3_OP_RA_SELECT")]
947 RaSelect = 1547,
948 /// Create a fresh copy (clone) of a relation.
949 /// The function is logically the identity, but
950 /// in the context of a register machine allows
951 /// for `Z3_OP_RA_UNION` to perform destructive updates to the first argument.
952 #[doc(alias = "Z3_OP_RA_CLONE")]
953 RaClone = 1548,
954 /// Corresponds to `Z3_OP_FD_CONSTANT` in the C API.
955 #[doc(alias = "Z3_OP_FD_CONSTANT")]
956 FdConstant = 1549,
957 /// A less than predicate over the finite domain Z3_FINITE_DOMAIN_SORT.
958 #[doc(alias = "Z3_OP_FD_LT")]
959 FdLt = 1550,
960 /// Corresponds to `Z3_OP_SEQ_UNIT` in the C API.
961 #[doc(alias = "Z3_OP_SEQ_UNIT")]
962 SeqUnit = 1551,
963 /// Corresponds to `Z3_OP_SEQ_EMPTY` in the C API.
964 #[doc(alias = "Z3_OP_SEQ_EMPTY")]
965 SeqEmpty = 1552,
966 /// Corresponds to `Z3_OP_SEQ_CONCAT` in the C API.
967 #[doc(alias = "Z3_OP_SEQ_CONCAT")]
968 SeqConcat = 1553,
969 /// Corresponds to `Z3_OP_SEQ_PREFIX` in the C API.
970 #[doc(alias = "Z3_OP_SEQ_PREFIX")]
971 SeqPrefix = 1554,
972 /// Corresponds to `Z3_OP_SEQ_SUFFIX` in the C API.
973 #[doc(alias = "Z3_OP_SEQ_SUFFIX")]
974 SeqSuffix = 1555,
975 /// Corresponds to `Z3_OP_SEQ_CONTAINS` in the C API.
976 #[doc(alias = "Z3_OP_SEQ_CONTAINS")]
977 SeqContains = 1556,
978 /// Corresponds to `Z3_OP_SEQ_EXTRACT` in the C API.
979 #[doc(alias = "Z3_OP_SEQ_EXTRACT")]
980 SeqExtract = 1557,
981 /// Corresponds to `Z3_OP_SEQ_REPLACE` in the C API.
982 #[doc(alias = "Z3_OP_SEQ_REPLACE")]
983 SeqReplace = 1558,
984 /// Corresponds to `Z3_OP_SEQ_REPLACE_RE` in the C API.
985 #[doc(alias = "Z3_OP_SEQ_REPLACE_RE")]
986 SeqReplaceRe = 1559,
987 /// Corresponds to `Z3_OP_SEQ_REPLACE_RE_ALL` in the C API.
988 #[doc(alias = "Z3_OP_SEQ_REPLACE_RE_ALL")]
989 SeqReplaceReAll = 1560,
990 /// Corresponds to `Z3_OP_SEQ_REPLACE_ALL` in the C API.
991 #[doc(alias = "Z3_OP_SEQ_REPLACE_ALL")]
992 SeqReplaceAll = 1561,
993 /// Corresponds to `Z3_OP_SEQ_AT` in the C API.
994 #[doc(alias = "Z3_OP_SEQ_AT")]
995 SeqAt = 1562,
996 /// Corresponds to `Z3_OP_SEQ_NTH` in the C API.
997 #[doc(alias = "Z3_OP_SEQ_NTH")]
998 SeqNth = 1563,
999 /// Corresponds to `Z3_OP_SEQ_LENGTH` in the C API.
1000 #[doc(alias = "Z3_OP_SEQ_LENGTH")]
1001 SeqLength = 1564,
1002 /// Corresponds to `Z3_OP_SEQ_INDEX` in the C API.
1003 #[doc(alias = "Z3_OP_SEQ_INDEX")]
1004 SeqIndex = 1565,
1005 /// Corresponds to `Z3_OP_SEQ_LAST_INDEX` in the C API.
1006 #[doc(alias = "Z3_OP_SEQ_LAST_INDEX")]
1007 SeqLastIndex = 1566,
1008 /// Corresponds to `Z3_OP_SEQ_TO_RE` in the C API.
1009 #[doc(alias = "Z3_OP_SEQ_TO_RE")]
1010 SeqToRe = 1567,
1011 /// Corresponds to `Z3_OP_SEQ_IN_RE` in the C API.
1012 #[doc(alias = "Z3_OP_SEQ_IN_RE")]
1013 SeqInRe = 1568,
1014 /// Corresponds to `Z3_OP_SEQ_MAP` in the C API.
1015 #[doc(alias = "Z3_OP_SEQ_MAP")]
1016 SeqMap = 1569,
1017 /// Corresponds to `Z3_OP_SEQ_MAPI` in the C API.
1018 #[doc(alias = "Z3_OP_SEQ_MAPI")]
1019 SeqMapi = 1570,
1020 /// Corresponds to `Z3_OP_SEQ_FOLDL` in the C API.
1021 #[doc(alias = "Z3_OP_SEQ_FOLDL")]
1022 SeqFoldl = 1571,
1023 /// Corresponds to `Z3_OP_SEQ_FOLDLI` in the C API.
1024 #[doc(alias = "Z3_OP_SEQ_FOLDLI")]
1025 SeqFoldli = 1572,
1026 /// Corresponds to `Z3_OP_STR_TO_INT` in the C API.
1027 #[doc(alias = "Z3_OP_STR_TO_INT")]
1028 StrToInt = 1573,
1029 /// Corresponds to `Z3_OP_INT_TO_STR` in the C API.
1030 #[doc(alias = "Z3_OP_INT_TO_STR")]
1031 IntToStr = 1574,
1032 /// Corresponds to `Z3_OP_UBV_TO_STR` in the C API.
1033 #[doc(alias = "Z3_OP_UBV_TO_STR")]
1034 UbvToStr = 1575,
1035 /// Corresponds to `Z3_OP_SBV_TO_STR` in the C API.
1036 #[doc(alias = "Z3_OP_SBV_TO_STR")]
1037 SbvToStr = 1576,
1038 /// Corresponds to `Z3_OP_STR_TO_CODE` in the C API.
1039 #[doc(alias = "Z3_OP_STR_TO_CODE")]
1040 StrToCode = 1577,
1041 /// Corresponds to `Z3_OP_STR_FROM_CODE` in the C API.
1042 #[doc(alias = "Z3_OP_STR_FROM_CODE")]
1043 StrFromCode = 1578,
1044 /// Corresponds to `Z3_OP_STRING_LT` in the C API.
1045 #[doc(alias = "Z3_OP_STRING_LT")]
1046 StringLt = 1579,
1047 /// Corresponds to `Z3_OP_STRING_LE` in the C API.
1048 #[doc(alias = "Z3_OP_STRING_LE")]
1049 StringLe = 1580,
1050 /// Corresponds to `Z3_OP_RE_PLUS` in the C API.
1051 #[doc(alias = "Z3_OP_RE_PLUS")]
1052 RePlus = 1581,
1053 /// Corresponds to `Z3_OP_RE_STAR` in the C API.
1054 #[doc(alias = "Z3_OP_RE_STAR")]
1055 ReStar = 1582,
1056 /// Corresponds to `Z3_OP_RE_OPTION` in the C API.
1057 #[doc(alias = "Z3_OP_RE_OPTION")]
1058 ReOption = 1583,
1059 /// Corresponds to `Z3_OP_RE_CONCAT` in the C API.
1060 #[doc(alias = "Z3_OP_RE_CONCAT")]
1061 ReConcat = 1584,
1062 /// Corresponds to `Z3_OP_RE_UNION` in the C API.
1063 #[doc(alias = "Z3_OP_RE_UNION")]
1064 ReUnion = 1585,
1065 /// Corresponds to `Z3_OP_RE_RANGE` in the C API.
1066 #[doc(alias = "Z3_OP_RE_RANGE")]
1067 ReRange = 1586,
1068 /// Corresponds to `Z3_OP_RE_DIFF` in the C API.
1069 #[doc(alias = "Z3_OP_RE_DIFF")]
1070 ReDiff = 1587,
1071 /// Corresponds to `Z3_OP_RE_INTERSECT` in the C API.
1072 #[doc(alias = "Z3_OP_RE_INTERSECT")]
1073 ReIntersect = 1588,
1074 /// Corresponds to `Z3_OP_RE_LOOP` in the C API.
1075 #[doc(alias = "Z3_OP_RE_LOOP")]
1076 ReLoop = 1589,
1077 /// Corresponds to `Z3_OP_RE_POWER` in the C API.
1078 #[doc(alias = "Z3_OP_RE_POWER")]
1079 RePower = 1590,
1080 /// Corresponds to `Z3_OP_RE_COMPLEMENT` in the C API.
1081 #[doc(alias = "Z3_OP_RE_COMPLEMENT")]
1082 ReComplement = 1591,
1083 /// Corresponds to `Z3_OP_RE_EMPTY_SET` in the C API.
1084 #[doc(alias = "Z3_OP_RE_EMPTY_SET")]
1085 ReEmptySet = 1592,
1086 /// Corresponds to `Z3_OP_RE_FULL_SET` in the C API.
1087 #[doc(alias = "Z3_OP_RE_FULL_SET")]
1088 ReFullSet = 1593,
1089 /// Corresponds to `Z3_OP_RE_FULL_CHAR_SET` in the C API.
1090 #[doc(alias = "Z3_OP_RE_FULL_CHAR_SET")]
1091 ReFullCharSet = 1594,
1092 /// Corresponds to `Z3_OP_RE_OF_PRED` in the C API.
1093 #[doc(alias = "Z3_OP_RE_OF_PRED")]
1094 ReOfPred = 1595,
1095 /// Corresponds to `Z3_OP_RE_REVERSE` in the C API.
1096 #[doc(alias = "Z3_OP_RE_REVERSE")]
1097 ReReverse = 1596,
1098 /// Corresponds to `Z3_OP_RE_DERIVATIVE` in the C API.
1099 #[doc(alias = "Z3_OP_RE_DERIVATIVE")]
1100 ReDerivative = 1597,
1101 /// Corresponds to `Z3_OP_CHAR_CONST` in the C API.
1102 #[doc(alias = "Z3_OP_CHAR_CONST")]
1103 CharConst = 1598,
1104 /// Corresponds to `Z3_OP_CHAR_LE` in the C API.
1105 #[doc(alias = "Z3_OP_CHAR_LE")]
1106 CharLe = 1599,
1107 /// Corresponds to `Z3_OP_CHAR_TO_INT` in the C API.
1108 #[doc(alias = "Z3_OP_CHAR_TO_INT")]
1109 CharToInt = 1600,
1110 /// Corresponds to `Z3_OP_CHAR_TO_BV` in the C API.
1111 #[doc(alias = "Z3_OP_CHAR_TO_BV")]
1112 CharToBv = 1601,
1113 /// Corresponds to `Z3_OP_CHAR_FROM_BV` in the C API.
1114 #[doc(alias = "Z3_OP_CHAR_FROM_BV")]
1115 CharFromBv = 1602,
1116 /// Corresponds to `Z3_OP_CHAR_IS_DIGIT` in the C API.
1117 #[doc(alias = "Z3_OP_CHAR_IS_DIGIT")]
1118 CharIsDigit = 1603,
1119 /// A label (used by the Boogie Verification condition generator).
1120 /// The label has two parameters, a string and a Boolean polarity.
1121 /// It takes one argument, a formula.
1122 #[doc(alias = "Z3_OP_LABEL")]
1123 Label = 1792,
1124 /// A label literal (used by the Boogie Verification condition generator).
1125 /// A label literal has a set of string parameters. It takes no arguments.
1126 #[doc(alias = "Z3_OP_LABEL_LIT")]
1127 LabelLit = 1793,
1128 /// datatype constructor.
1129 #[doc(alias = "Z3_OP_DT_CONSTRUCTOR")]
1130 DtConstructor = 2048,
1131 /// datatype recognizer.
1132 #[doc(alias = "Z3_OP_DT_RECOGNISER")]
1133 DtRecogniser = 2049,
1134 /// datatype recognizer.
1135 #[doc(alias = "Z3_OP_DT_IS")]
1136 DtIs = 2050,
1137 /// datatype accessor.
1138 #[doc(alias = "Z3_OP_DT_ACCESSOR")]
1139 DtAccessor = 2051,
1140 /// datatype field update.
1141 #[doc(alias = "Z3_OP_DT_UPDATE_FIELD")]
1142 DtUpdateField = 2052,
1143 /// Cardinality constraint.
1144 /// E.g., x + y + z <= 2
1145 #[doc(alias = "Z3_OP_PB_AT_MOST")]
1146 PbAtMost = 2304,
1147 /// Cardinality constraint.
1148 /// E.g., x + y + z >= 2
1149 #[doc(alias = "Z3_OP_PB_AT_LEAST")]
1150 PbAtLeast = 2305,
1151 /// Generalized Pseudo-Boolean cardinality constraint.
1152 /// Example 2*x + 3*y <= 4
1153 #[doc(alias = "Z3_OP_PB_LE")]
1154 PbLe = 2306,
1155 /// Generalized Pseudo-Boolean cardinality constraint.
1156 /// Example 2*x + 3*y + 2*z >= 4
1157 #[doc(alias = "Z3_OP_PB_GE")]
1158 PbGe = 2307,
1159 /// Generalized Pseudo-Boolean equality constraint.
1160 /// Example 2*x + 1*y + 2*z + 1*u = 4
1161 #[doc(alias = "Z3_OP_PB_EQ")]
1162 PbEq = 2308,
1163 /// A relation that is a total linear order
1164 #[doc(alias = "Z3_OP_SPECIAL_RELATION_LO")]
1165 SpecialRelationLo = 40960,
1166 /// A relation that is a partial order
1167 #[doc(alias = "Z3_OP_SPECIAL_RELATION_PO")]
1168 SpecialRelationPo = 40961,
1169 /// A relation that is a piecewise linear order
1170 #[doc(alias = "Z3_OP_SPECIAL_RELATION_PLO")]
1171 SpecialRelationPlo = 40962,
1172 /// A relation that is a tree order
1173 #[doc(alias = "Z3_OP_SPECIAL_RELATION_TO")]
1174 SpecialRelationTo = 40963,
1175 /// Transitive closure of a relation
1176 #[doc(alias = "Z3_OP_SPECIAL_RELATION_TC")]
1177 SpecialRelationTc = 40964,
1178 /// Transitive reflexive closure of a relation
1179 #[doc(alias = "Z3_OP_SPECIAL_RELATION_TRC")]
1180 SpecialRelationTrc = 40965,
1181 /// Floating-point rounding mode RNE
1182 #[doc(alias = "Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN")]
1183 FpaRmNearestTiesToEven = 45056,
1184 /// Floating-point rounding mode RNA
1185 #[doc(alias = "Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY")]
1186 FpaRmNearestTiesToAway = 45057,
1187 /// Floating-point rounding mode RTP
1188 #[doc(alias = "Z3_OP_FPA_RM_TOWARD_POSITIVE")]
1189 FpaRmTowardPositive = 45058,
1190 /// Floating-point rounding mode RTN
1191 #[doc(alias = "Z3_OP_FPA_RM_TOWARD_NEGATIVE")]
1192 FpaRmTowardNegative = 45059,
1193 /// Floating-point rounding mode RTZ
1194 #[doc(alias = "Z3_OP_FPA_RM_TOWARD_ZERO")]
1195 FpaRmTowardZero = 45060,
1196 /// Floating-point value
1197 #[doc(alias = "Z3_OP_FPA_NUM")]
1198 FpaNum = 45061,
1199 /// Floating-point +oo
1200 #[doc(alias = "Z3_OP_FPA_PLUS_INF")]
1201 FpaPlusInf = 45062,
1202 /// Floating-point -oo
1203 #[doc(alias = "Z3_OP_FPA_MINUS_INF")]
1204 FpaMinusInf = 45063,
1205 /// Floating-point NaN
1206 #[doc(alias = "Z3_OP_FPA_NAN")]
1207 FpaNan = 45064,
1208 /// Floating-point +zero
1209 #[doc(alias = "Z3_OP_FPA_PLUS_ZERO")]
1210 FpaPlusZero = 45065,
1211 /// Floating-point -zero
1212 #[doc(alias = "Z3_OP_FPA_MINUS_ZERO")]
1213 FpaMinusZero = 45066,
1214 /// Floating-point addition
1215 #[doc(alias = "Z3_OP_FPA_ADD")]
1216 FpaAdd = 45067,
1217 /// Floating-point subtraction
1218 #[doc(alias = "Z3_OP_FPA_SUB")]
1219 FpaSub = 45068,
1220 /// Floating-point negation
1221 #[doc(alias = "Z3_OP_FPA_NEG")]
1222 FpaNeg = 45069,
1223 /// Floating-point multiplication
1224 #[doc(alias = "Z3_OP_FPA_MUL")]
1225 FpaMul = 45070,
1226 /// Floating-point division
1227 #[doc(alias = "Z3_OP_FPA_DIV")]
1228 FpaDiv = 45071,
1229 /// Floating-point remainder
1230 #[doc(alias = "Z3_OP_FPA_REM")]
1231 FpaRem = 45072,
1232 /// Floating-point absolute value
1233 #[doc(alias = "Z3_OP_FPA_ABS")]
1234 FpaAbs = 45073,
1235 /// Floating-point minimum
1236 #[doc(alias = "Z3_OP_FPA_MIN")]
1237 FpaMin = 45074,
1238 /// Floating-point maximum
1239 #[doc(alias = "Z3_OP_FPA_MAX")]
1240 FpaMax = 45075,
1241 /// Floating-point fused multiply-add
1242 #[doc(alias = "Z3_OP_FPA_FMA")]
1243 FpaFma = 45076,
1244 /// Floating-point square root
1245 #[doc(alias = "Z3_OP_FPA_SQRT")]
1246 FpaSqrt = 45077,
1247 /// Floating-point round to integral
1248 #[doc(alias = "Z3_OP_FPA_ROUND_TO_INTEGRAL")]
1249 FpaRoundToIntegral = 45078,
1250 /// Floating-point equality
1251 #[doc(alias = "Z3_OP_FPA_EQ")]
1252 FpaEq = 45079,
1253 /// Floating-point less than
1254 #[doc(alias = "Z3_OP_FPA_LT")]
1255 FpaLt = 45080,
1256 /// Floating-point greater than
1257 #[doc(alias = "Z3_OP_FPA_GT")]
1258 FpaGt = 45081,
1259 /// Floating-point less than or equal
1260 #[doc(alias = "Z3_OP_FPA_LE")]
1261 FpaLe = 45082,
1262 /// Floating-point greater than or equal
1263 #[doc(alias = "Z3_OP_FPA_GE")]
1264 FpaGe = 45083,
1265 /// Floating-point isNaN
1266 #[doc(alias = "Z3_OP_FPA_IS_NAN")]
1267 FpaIsNan = 45084,
1268 /// Floating-point isInfinite
1269 #[doc(alias = "Z3_OP_FPA_IS_INF")]
1270 FpaIsInf = 45085,
1271 /// Floating-point isZero
1272 #[doc(alias = "Z3_OP_FPA_IS_ZERO")]
1273 FpaIsZero = 45086,
1274 /// Floating-point isNormal
1275 #[doc(alias = "Z3_OP_FPA_IS_NORMAL")]
1276 FpaIsNormal = 45087,
1277 /// Floating-point isSubnormal
1278 #[doc(alias = "Z3_OP_FPA_IS_SUBNORMAL")]
1279 FpaIsSubnormal = 45088,
1280 /// Floating-point isNegative
1281 #[doc(alias = "Z3_OP_FPA_IS_NEGATIVE")]
1282 FpaIsNegative = 45089,
1283 /// Floating-point isPositive
1284 #[doc(alias = "Z3_OP_FPA_IS_POSITIVE")]
1285 FpaIsPositive = 45090,
1286 /// Floating-point constructor from 3 bit-vectors
1287 #[doc(alias = "Z3_OP_FPA_FP")]
1288 FpaFp = 45091,
1289 /// Floating-point conversion (various)
1290 #[doc(alias = "Z3_OP_FPA_TO_FP")]
1291 FpaToFp = 45092,
1292 /// Floating-point conversion from unsigned bit-vector
1293 #[doc(alias = "Z3_OP_FPA_TO_FP_UNSIGNED")]
1294 FpaToFpUnsigned = 45093,
1295 /// Floating-point conversion to unsigned bit-vector
1296 #[doc(alias = "Z3_OP_FPA_TO_UBV")]
1297 FpaToUbv = 45094,
1298 /// Floating-point conversion to signed bit-vector
1299 #[doc(alias = "Z3_OP_FPA_TO_SBV")]
1300 FpaToSbv = 45095,
1301 /// Floating-point conversion to real number
1302 #[doc(alias = "Z3_OP_FPA_TO_REAL")]
1303 FpaToReal = 45096,
1304 /// Floating-point conversion to IEEE-754 bit-vector
1305 #[doc(alias = "Z3_OP_FPA_TO_IEEE_BV")]
1306 FpaToIeeeBv = 45097,
1307 /// (Implicitly) represents the internal bitvector-
1308 /// representation of a floating-point term (used for the lazy encoding
1309 /// of non-relevant terms in theory_fpa)
1310 #[doc(alias = "Z3_OP_FPA_BVWRAP")]
1311 FpaBvwrap = 45098,
1312 /// Conversion of a 3-bit bit-vector term to a
1313 /// floating-point rounding-mode term
1314 ///
1315 /// The conversion uses the following values:
1316 /// 0 = 000 = Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN,
1317 /// 1 = 001 = Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY,
1318 /// 2 = 010 = Z3_OP_FPA_RM_TOWARD_POSITIVE,
1319 /// 3 = 011 = Z3_OP_FPA_RM_TOWARD_NEGATIVE,
1320 /// 4 = 100 = Z3_OP_FPA_RM_TOWARD_ZERO.
1321 #[doc(alias = "Z3_OP_FPA_BV2RM")]
1322 FpaBv2rm = 45099,
1323 /// internal (often interpreted) symbol, but no additional
1324 /// information is exposed. Tools may use the string representation of the
1325 /// function declaration to obtain more information.
1326 #[doc(alias = "Z3_OP_INTERNAL")]
1327 Internal = 45100,
1328 /// function declared as recursive
1329 #[doc(alias = "Z3_OP_RECURSIVE")]
1330 Recursive = 45101,
1331 /// kind used for uninterpreted symbols.
1332 #[doc(alias = "Z3_OP_UNINTERPRETED")]
1333 Uninterpreted = 45102,
1334}
1335pub type Z3_decl_kind = DeclKind;
1336/// The different kinds of parameters that can be associated with parameter sets.
1337/// (see [`Z3_mk_params`]).
1338#[doc(alias = "Z3_param_kind")]
1339#[repr(u32)]
1340#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)]
1341pub enum ParamKind {
1342 /// integer parameters.
1343 #[doc(alias = "Z3_PK_UINT")]
1344 Uint = 0,
1345 /// boolean parameters.
1346 #[doc(alias = "Z3_PK_BOOL")]
1347 Bool = 1,
1348 /// double parameters.
1349 #[doc(alias = "Z3_PK_DOUBLE")]
1350 Double = 2,
1351 /// symbol parameters.
1352 #[doc(alias = "Z3_PK_SYMBOL")]
1353 Symbol = 3,
1354 /// string parameters.
1355 #[doc(alias = "Z3_PK_STRING")]
1356 String = 4,
1357 /// all internal parameter kinds which are not exposed in the API.
1358 #[doc(alias = "Z3_PK_OTHER")]
1359 Other = 5,
1360 /// invalid parameter.
1361 #[doc(alias = "Z3_PK_INVALID")]
1362 Invalid = 6,
1363}
1364pub type Z3_param_kind = ParamKind;
1365/// Z3 pretty printing modes (See [`Z3_set_ast_print_mode`]).
1366#[doc(alias = "Z3_ast_print_mode")]
1367#[repr(u32)]
1368#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)]
1369pub enum AstPrintMode {
1370 /// Print AST nodes in SMTLIB verbose format.
1371 #[doc(alias = "Z3_PRINT_SMTLIB_FULL")]
1372 SmtlibFull = 0,
1373 /// Print AST nodes using a low-level format.
1374 #[doc(alias = "Z3_PRINT_LOW_LEVEL")]
1375 LowLevel = 1,
1376 /// Print AST nodes in SMTLIB 2.x compliant format.
1377 #[doc(alias = "Z3_PRINT_SMTLIB2_COMPLIANT")]
1378 Smtlib2Compliant = 2,
1379}
1380pub type Z3_ast_print_mode = AstPrintMode;
1381/// Z3 error codes (See [`Z3_get_error_code`]).
1382#[doc(alias = "Z3_error_code")]
1383#[repr(u32)]
1384#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)]
1385pub enum ErrorCode {
1386 /// No error.
1387 #[doc(alias = "Z3_OK")]
1388 Ok = 0,
1389 /// User tried to build an invalid (type incorrect) AST.
1390 #[doc(alias = "Z3_SORT_ERROR")]
1391 SortError = 1,
1392 /// Index out of bounds.
1393 #[doc(alias = "Z3_IOB")]
1394 Iob = 2,
1395 /// Invalid argument was provided.
1396 #[doc(alias = "Z3_INVALID_ARG")]
1397 InvalidArg = 3,
1398 /// An error occurred when parsing a string or file.
1399 #[doc(alias = "Z3_PARSER_ERROR")]
1400 ParserError = 4,
1401 /// Parser output is not available, that is, user didn't invoke [`Z3_parse_smtlib2_string`] or [`Z3_parse_smtlib2_file`].
1402 #[doc(alias = "Z3_NO_PARSER")]
1403 NoParser = 5,
1404 /// Invalid pattern was used to build a quantifier.
1405 #[doc(alias = "Z3_INVALID_PATTERN")]
1406 InvalidPattern = 6,
1407 /// A memory allocation failure was encountered.
1408 #[doc(alias = "Z3_MEMOUT_FAIL")]
1409 MemoutFail = 7,
1410 /// A file could not be accessed.
1411 #[doc(alias = "Z3_FILE_ACCESS_ERROR")]
1412 FileAccessError = 8,
1413 /// An error internal to Z3 occurred.
1414 #[doc(alias = "Z3_INTERNAL_FATAL")]
1415 InternalFatal = 9,
1416 /// API call is invalid in the current state.
1417 #[doc(alias = "Z3_INVALID_USAGE")]
1418 InvalidUsage = 10,
1419 /// Trying to decrement the reference counter of an AST that was deleted or the reference counter was not initialized with [`Z3_inc_ref`].
1420 #[doc(alias = "Z3_DEC_REF_ERROR")]
1421 DecRefError = 11,
1422 /// Internal Z3 exception. Additional details can be retrieved using [`Z3_get_error_msg`].
1423 #[doc(alias = "Z3_EXCEPTION")]
1424 Exception = 12,
1425}
1426pub type Z3_error_code = ErrorCode;
1427/// A Goal is essentially a set of formulas.
1428/// Z3 provide APIs for building strategies/tactics for solving and transforming Goals.
1429/// Some of these transformations apply under/over approximations.
1430#[doc(alias = "Z3_goal_prec")]
1431#[repr(u32)]
1432#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)]
1433pub enum GoalPrec {
1434 /// Approximations/Relaxations were not applied on the goal (sat and unsat answers were preserved).
1435 #[doc(alias = "Z3_GOAL_PRECISE")]
1436 Precise = 0,
1437 /// Goal is the product of a under-approximation (sat answers are preserved).
1438 #[doc(alias = "Z3_GOAL_UNDER")]
1439 Under = 1,
1440 /// Goal is the product of an over-approximation (unsat answers are preserved).
1441 #[doc(alias = "Z3_GOAL_OVER")]
1442 Over = 2,
1443 /// Goal is garbage (it is the product of over- and under-approximations, sat and unsat answers are not preserved).
1444 #[doc(alias = "Z3_GOAL_UNDER_OVER")]
1445 UnderOver = 3,
1446}
1447pub type Z3_goal_prec = GoalPrec;