z3-sys 0.11.0

// Auto-generated by z3-sys bindgen feature — do not edit manually.

/// The different kinds of symbol.
/// In Z3, a symbol can be represented using integers and strings (See [`Z3_get_symbol_kind`]).
///
/// # See also
///
/// - [`Z3_mk_int_symbol`]
/// - [`Z3_mk_string_symbol`]
#[doc(alias = "Z3_symbol_kind")]
#[repr(u32)]
#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)]
pub enum SymbolKind {
    /// Corresponds to `Z3_INT_SYMBOL` in the C API.
    #[doc(alias = "Z3_INT_SYMBOL")]
    Int = 0,
    /// Corresponds to `Z3_STRING_SYMBOL` in the C API.
    #[doc(alias = "Z3_STRING_SYMBOL")]
    String = 1,
}
pub type Z3_symbol_kind = SymbolKind;
/// The different kinds of parameters that can be associated with function symbols.
///
/// # See also
///
/// - [`Z3_get_decl_num_parameters`]
/// - [`Z3_get_decl_parameter_kind`]
#[doc(alias = "Z3_parameter_kind")]
#[repr(u32)]
#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)]
pub enum ParameterKind {
    /// used for integer parameters.
    #[doc(alias = "Z3_PARAMETER_INT")]
    Int = 0,
    /// used for double parameters.
    #[doc(alias = "Z3_PARAMETER_DOUBLE")]
    Double = 1,
    /// used for parameters that are rational numbers.
    #[doc(alias = "Z3_PARAMETER_RATIONAL")]
    Rational = 2,
    /// used for parameters that are symbols.
    #[doc(alias = "Z3_PARAMETER_SYMBOL")]
    Symbol = 3,
    /// used for sort parameters.
    #[doc(alias = "Z3_PARAMETER_SORT")]
    Sort = 4,
    /// used for expression parameters.
    #[doc(alias = "Z3_PARAMETER_AST")]
    Ast = 5,
    /// used for function declaration parameters.
    #[doc(alias = "Z3_PARAMETER_FUNC_DECL")]
    FuncDecl = 6,
    /// used for parameters that are private to Z3. They cannot be accessed.
    #[doc(alias = "Z3_PARAMETER_INTERNAL")]
    Internal = 7,
    /// used for string parameters.
    #[doc(alias = "Z3_PARAMETER_ZSTRING")]
    Zstring = 8,
}
pub type Z3_parameter_kind = ParameterKind;
/// The different kinds of Z3 types (See [`Z3_get_sort_kind`]).
#[doc(alias = "Z3_sort_kind")]
#[repr(u32)]
#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)]
pub enum SortKind {
    /// Corresponds to `Z3_UNINTERPRETED_SORT` in the C API.
    #[doc(alias = "Z3_UNINTERPRETED_SORT")]
    Uninterpreted = 0,
    /// Corresponds to `Z3_BOOL_SORT` in the C API.
    #[doc(alias = "Z3_BOOL_SORT")]
    Bool = 1,
    /// Corresponds to `Z3_INT_SORT` in the C API.
    #[doc(alias = "Z3_INT_SORT")]
    Int = 2,
    /// Corresponds to `Z3_REAL_SORT` in the C API.
    #[doc(alias = "Z3_REAL_SORT")]
    Real = 3,
    /// Corresponds to `Z3_BV_SORT` in the C API.
    #[doc(alias = "Z3_BV_SORT")]
    Bv = 4,
    /// Corresponds to `Z3_ARRAY_SORT` in the C API.
    #[doc(alias = "Z3_ARRAY_SORT")]
    Array = 5,
    /// Corresponds to `Z3_DATATYPE_SORT` in the C API.
    #[doc(alias = "Z3_DATATYPE_SORT")]
    Datatype = 6,
    /// Corresponds to `Z3_RELATION_SORT` in the C API.
    #[doc(alias = "Z3_RELATION_SORT")]
    Relation = 7,
    /// Corresponds to `Z3_FINITE_DOMAIN_SORT` in the C API.
    #[doc(alias = "Z3_FINITE_DOMAIN_SORT")]
    FiniteDomain = 8,
    /// Corresponds to `Z3_FLOATING_POINT_SORT` in the C API.
    #[doc(alias = "Z3_FLOATING_POINT_SORT")]
    FloatingPoint = 9,
    /// Corresponds to `Z3_ROUNDING_MODE_SORT` in the C API.
    #[doc(alias = "Z3_ROUNDING_MODE_SORT")]
    RoundingMode = 10,
    /// Corresponds to `Z3_SEQ_SORT` in the C API.
    #[doc(alias = "Z3_SEQ_SORT")]
    Seq = 11,
    /// Corresponds to `Z3_RE_SORT` in the C API.
    #[doc(alias = "Z3_RE_SORT")]
    Re = 12,
    /// Corresponds to `Z3_CHAR_SORT` in the C API.
    #[doc(alias = "Z3_CHAR_SORT")]
    Char = 13,
    /// Corresponds to `Z3_TYPE_VAR` in the C API.
    #[doc(alias = "Z3_TYPE_VAR")]
    TypeVar = 14,
    /// Corresponds to `Z3_UNKNOWN_SORT` in the C API.
    #[doc(alias = "Z3_UNKNOWN_SORT")]
    Unknown = 1000,
}
pub type Z3_sort_kind = SortKind;
/// The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
#[doc(alias = "Z3_ast_kind")]
#[repr(u32)]
#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)]
pub enum AstKind {
    /// numeral constants
    #[doc(alias = "Z3_NUMERAL_AST")]
    Numeral = 0,
    /// constant and applications
    #[doc(alias = "Z3_APP_AST")]
    App = 1,
    /// bound variables
    #[doc(alias = "Z3_VAR_AST")]
    Var = 2,
    /// quantifiers
    #[doc(alias = "Z3_QUANTIFIER_AST")]
    Quantifier = 3,
    /// sort
    #[doc(alias = "Z3_SORT_AST")]
    Sort = 4,
    /// function declaration
    #[doc(alias = "Z3_FUNC_DECL_AST")]
    FuncDecl = 5,
    /// internal
    #[doc(alias = "Z3_UNKNOWN_AST")]
    Unknown = 1000,
}
pub type Z3_ast_kind = AstKind;
/// The different kinds of interpreted function kinds.
#[doc(alias = "Z3_decl_kind")]
#[repr(u32)]
#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)]
pub enum DeclKind {
    /// The constant true.
    #[doc(alias = "Z3_OP_TRUE")]
    True = 256,
    /// The constant false.
    #[doc(alias = "Z3_OP_FALSE")]
    False = 257,
    /// The equality predicate.
    #[doc(alias = "Z3_OP_EQ")]
    Eq = 258,
    /// The n-ary distinct predicate (every argument is mutually distinct).
    #[doc(alias = "Z3_OP_DISTINCT")]
    Distinct = 259,
    /// The ternary if-then-else term.
    #[doc(alias = "Z3_OP_ITE")]
    Ite = 260,
    /// n-ary conjunction.
    #[doc(alias = "Z3_OP_AND")]
    And = 261,
    /// n-ary disjunction.
    #[doc(alias = "Z3_OP_OR")]
    Or = 262,
    /// equivalence (binary).
    #[doc(alias = "Z3_OP_IFF")]
    Iff = 263,
    /// Exclusive or.
    #[doc(alias = "Z3_OP_XOR")]
    Xor = 264,
    /// Negation.
    #[doc(alias = "Z3_OP_NOT")]
    Not = 265,
    /// Implication.
    #[doc(alias = "Z3_OP_IMPLIES")]
    Implies = 266,
    /// Binary equivalence modulo namings. This binary predicate is used in proof terms.
    /// It captures equisatisfiability and equivalence modulo renamings.
    #[doc(alias = "Z3_OP_OEQ")]
    Oeq = 267,
    /// Arithmetic numeral.
    #[doc(alias = "Z3_OP_ANUM")]
    Anum = 512,
    /// Arithmetic algebraic numeral. Algebraic numbers are used to represent irrational numbers in Z3.
    #[doc(alias = "Z3_OP_AGNUM")]
    Agnum = 513,
    /// <=.
    #[doc(alias = "Z3_OP_LE")]
    Le = 514,
    /// >=.
    #[doc(alias = "Z3_OP_GE")]
    Ge = 515,
    /// <.
    #[doc(alias = "Z3_OP_LT")]
    Lt = 516,
    /// >.
    #[doc(alias = "Z3_OP_GT")]
    Gt = 517,
    /// Addition - Binary.
    #[doc(alias = "Z3_OP_ADD")]
    Add = 518,
    /// Binary subtraction.
    #[doc(alias = "Z3_OP_SUB")]
    Sub = 519,
    /// Unary minus.
    #[doc(alias = "Z3_OP_UMINUS")]
    Uminus = 520,
    /// Multiplication - Binary.
    #[doc(alias = "Z3_OP_MUL")]
    Mul = 521,
    /// Division - Binary.
    #[doc(alias = "Z3_OP_DIV")]
    Div = 522,
    /// Integer division - Binary.
    #[doc(alias = "Z3_OP_IDIV")]
    Idiv = 523,
    /// Remainder - Binary.
    #[doc(alias = "Z3_OP_REM")]
    Rem = 524,
    /// Modulus - Binary.
    #[doc(alias = "Z3_OP_MOD")]
    Mod = 525,
    /// Coercion of integer to real - Unary.
    #[doc(alias = "Z3_OP_TO_REAL")]
    ToReal = 526,
    /// Coercion of real to integer - Unary.
    #[doc(alias = "Z3_OP_TO_INT")]
    ToInt = 527,
    /// Check if real is also an integer - Unary.
    #[doc(alias = "Z3_OP_IS_INT")]
    IsInt = 528,
    /// Power operator x^y.
    #[doc(alias = "Z3_OP_POWER")]
    Power = 529,
    /// Corresponds to `Z3_OP_ABS` in the C API.
    #[doc(alias = "Z3_OP_ABS")]
    Abs = 530,
    /// Array store. It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j).
    /// Array store takes at least 3 arguments.
    #[doc(alias = "Z3_OP_STORE")]
    Store = 768,
    /// Array select.
    #[doc(alias = "Z3_OP_SELECT")]
    Select = 769,
    /// The constant array. For example, select(const(v),i) = v holds for every v and i. The function is unary.
    #[doc(alias = "Z3_OP_CONST_ARRAY")]
    ConstArray = 770,
    /// Array map operator.
    /// It satisfies map\[f](a1,..,a_n)\[i] = f(a1\[i],...,a_n\[i]) for every i.
    #[doc(alias = "Z3_OP_ARRAY_MAP")]
    ArrayMap = 771,
    /// Default value of arrays. For example default(const(v)) = v. The function is unary.
    #[doc(alias = "Z3_OP_ARRAY_DEFAULT")]
    ArrayDefault = 772,
    /// Set union between two Boolean arrays (two arrays whose range type is Boolean). The function is binary.
    #[doc(alias = "Z3_OP_SET_UNION")]
    SetUnion = 773,
    /// Set intersection between two Boolean arrays. The function is binary.
    #[doc(alias = "Z3_OP_SET_INTERSECT")]
    SetIntersect = 774,
    /// Set difference between two Boolean arrays. The function is binary.
    #[doc(alias = "Z3_OP_SET_DIFFERENCE")]
    SetDifference = 775,
    /// Set complement of a Boolean array. The function is unary.
    #[doc(alias = "Z3_OP_SET_COMPLEMENT")]
    SetComplement = 776,
    /// Subset predicate between two Boolean arrays. The relation is binary.
    #[doc(alias = "Z3_OP_SET_SUBSET")]
    SetSubset = 777,
    /// An array value that behaves as the function graph of the
    /// function passed as parameter.
    #[doc(alias = "Z3_OP_AS_ARRAY")]
    AsArray = 778,
    /// Array extensionality function. It takes two arrays as arguments and produces an index, such that the arrays
    /// are different if they are different on the index.
    #[doc(alias = "Z3_OP_ARRAY_EXT")]
    ArrayExt = 779,
    /// Bit-vector numeral.
    #[doc(alias = "Z3_OP_BNUM")]
    Bnum = 1024,
    /// One bit bit-vector.
    #[doc(alias = "Z3_OP_BIT1")]
    Bit1 = 1025,
    /// Zero bit bit-vector.
    #[doc(alias = "Z3_OP_BIT0")]
    Bit0 = 1026,
    /// Unary minus.
    #[doc(alias = "Z3_OP_BNEG")]
    Bneg = 1027,
    /// Binary addition.
    #[doc(alias = "Z3_OP_BADD")]
    Badd = 1028,
    /// Binary subtraction.
    #[doc(alias = "Z3_OP_BSUB")]
    Bsub = 1029,
    /// Binary multiplication.
    #[doc(alias = "Z3_OP_BMUL")]
    Bmul = 1030,
    /// Binary signed division.
    #[doc(alias = "Z3_OP_BSDIV")]
    Bsdiv = 1031,
    /// Binary unsigned division.
    #[doc(alias = "Z3_OP_BUDIV")]
    Budiv = 1032,
    /// Binary signed remainder.
    #[doc(alias = "Z3_OP_BSREM")]
    Bsrem = 1033,
    /// Binary unsigned remainder.
    #[doc(alias = "Z3_OP_BUREM")]
    Burem = 1034,
    /// Binary signed modulus.
    #[doc(alias = "Z3_OP_BSMOD")]
    Bsmod = 1035,
    /// Unary function. bsdiv(x,0) is congruent to bsdiv0(x).
    #[doc(alias = "Z3_OP_BSDIV0")]
    Bsdiv0 = 1036,
    /// Unary function. budiv(x,0) is congruent to budiv0(x).
    #[doc(alias = "Z3_OP_BUDIV0")]
    Budiv0 = 1037,
    /// Unary function. bsrem(x,0) is congruent to bsrem0(x).
    #[doc(alias = "Z3_OP_BSREM0")]
    Bsrem0 = 1038,
    /// Unary function. burem(x,0) is congruent to burem0(x).
    #[doc(alias = "Z3_OP_BUREM0")]
    Burem0 = 1039,
    /// Unary function. bsmod(x,0) is congruent to bsmod0(x).
    #[doc(alias = "Z3_OP_BSMOD0")]
    Bsmod0 = 1040,
    /// Unsigned bit-vector <= - Binary relation.
    #[doc(alias = "Z3_OP_ULEQ")]
    Uleq = 1041,
    /// Signed bit-vector  <= - Binary relation.
    #[doc(alias = "Z3_OP_SLEQ")]
    Sleq = 1042,
    /// Unsigned bit-vector  >= - Binary relation.
    #[doc(alias = "Z3_OP_UGEQ")]
    Ugeq = 1043,
    /// Signed bit-vector  >= - Binary relation.
    #[doc(alias = "Z3_OP_SGEQ")]
    Sgeq = 1044,
    /// Unsigned bit-vector  < - Binary relation.
    #[doc(alias = "Z3_OP_ULT")]
    Ult = 1045,
    /// Signed bit-vector < - Binary relation.
    #[doc(alias = "Z3_OP_SLT")]
    Slt = 1046,
    /// Unsigned bit-vector > - Binary relation.
    #[doc(alias = "Z3_OP_UGT")]
    Ugt = 1047,
    /// Signed bit-vector > - Binary relation.
    #[doc(alias = "Z3_OP_SGT")]
    Sgt = 1048,
    /// Bit-wise and - Binary.
    #[doc(alias = "Z3_OP_BAND")]
    Band = 1049,
    /// Bit-wise or - Binary.
    #[doc(alias = "Z3_OP_BOR")]
    Bor = 1050,
    /// Bit-wise not - Unary.
    #[doc(alias = "Z3_OP_BNOT")]
    Bnot = 1051,
    /// Bit-wise xor - Binary.
    #[doc(alias = "Z3_OP_BXOR")]
    Bxor = 1052,
    /// Bit-wise nand - Binary.
    #[doc(alias = "Z3_OP_BNAND")]
    Bnand = 1053,
    /// Bit-wise nor - Binary.
    #[doc(alias = "Z3_OP_BNOR")]
    Bnor = 1054,
    /// Bit-wise xnor - Binary.
    #[doc(alias = "Z3_OP_BXNOR")]
    Bxnor = 1055,
    /// Bit-vector concatenation - Binary.
    #[doc(alias = "Z3_OP_CONCAT")]
    Concat = 1056,
    /// Bit-vector sign extension.
    #[doc(alias = "Z3_OP_SIGN_EXT")]
    SignExt = 1057,
    /// Bit-vector zero extension.
    #[doc(alias = "Z3_OP_ZERO_EXT")]
    ZeroExt = 1058,
    /// Bit-vector extraction.
    #[doc(alias = "Z3_OP_EXTRACT")]
    Extract = 1059,
    /// Repeat bit-vector n times.
    #[doc(alias = "Z3_OP_REPEAT")]
    Repeat = 1060,
    /// Bit-vector reduce or - Unary.
    #[doc(alias = "Z3_OP_BREDOR")]
    Bredor = 1061,
    /// Bit-vector reduce and - Unary.
    #[doc(alias = "Z3_OP_BREDAND")]
    Bredand = 1062,
    /// .
    #[doc(alias = "Z3_OP_BCOMP")]
    Bcomp = 1063,
    /// Shift left.
    #[doc(alias = "Z3_OP_BSHL")]
    Bshl = 1064,
    /// Logical shift right.
    #[doc(alias = "Z3_OP_BLSHR")]
    Blshr = 1065,
    /// Arithmetical shift right.
    #[doc(alias = "Z3_OP_BASHR")]
    Bashr = 1066,
    /// Left rotation.
    #[doc(alias = "Z3_OP_ROTATE_LEFT")]
    RotateLeft = 1067,
    /// Right rotation.
    #[doc(alias = "Z3_OP_ROTATE_RIGHT")]
    RotateRight = 1068,
    /// (extended) Left rotation. Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one.
    #[doc(alias = "Z3_OP_EXT_ROTATE_LEFT")]
    ExtRotateLeft = 1069,
    /// (extended) Right rotation. Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one.
    #[doc(alias = "Z3_OP_EXT_ROTATE_RIGHT")]
    ExtRotateRight = 1070,
    /// Corresponds to `Z3_OP_BIT2BOOL` in the C API.
    #[doc(alias = "Z3_OP_BIT2BOOL")]
    Bit2bool = 1071,
    /// Coerce integer to bit-vector.
    #[doc(alias = "Z3_OP_INT2BV")]
    Int2bv = 1072,
    /// Coerce bit-vector to integer.
    #[doc(alias = "Z3_OP_BV2INT")]
    Bv2int = 1073,
    /// Coerce signed bit-vector to integer.
    #[doc(alias = "Z3_OP_SBV2INT")]
    Sbv2int = 1074,
    /// Compute the carry bit in a full-adder.
    /// The meaning is given by the equivalence
    /// (carry l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3)))
    #[doc(alias = "Z3_OP_CARRY")]
    Carry = 1075,
    /// Compute ternary XOR.
    /// The meaning is given by the equivalence
    /// (xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3)
    #[doc(alias = "Z3_OP_XOR3")]
    Xor3 = 1076,
    /// a predicate to check that bit-wise signed multiplication does not overflow.
    /// Signed multiplication overflows if the operands have the same sign and the result of multiplication
    /// does not fit within the available bits. \sa Z3_mk_bvmul_no_overflow.
    #[doc(alias = "Z3_OP_BSMUL_NO_OVFL")]
    BsmulNoOvfl = 1077,
    /// check that bit-wise unsigned multiplication does not overflow.
    /// Unsigned multiplication overflows if the result does not fit within the available bits.
    ///
    /// # See also
    ///
    /// - [`Z3_mk_bvmul_no_overflow`]
    #[doc(alias = "Z3_OP_BUMUL_NO_OVFL")]
    BumulNoOvfl = 1078,
    /// check that bit-wise signed multiplication does not underflow.
    /// Signed multiplication underflows if the operands have opposite signs and the result of multiplication
    /// does not fit within the available bits. Z3_mk_bvmul_no_underflow.
    #[doc(alias = "Z3_OP_BSMUL_NO_UDFL")]
    BsmulNoUdfl = 1079,
    /// Binary signed division.
    /// 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.
    #[doc(alias = "Z3_OP_BSDIV_I")]
    BsdivI = 1080,
    /// Binary unsigned division.
    /// 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.
    #[doc(alias = "Z3_OP_BUDIV_I")]
    BudivI = 1081,
    /// Binary signed remainder.
    /// 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.
    #[doc(alias = "Z3_OP_BSREM_I")]
    BsremI = 1082,
    /// Binary unsigned remainder.
    /// 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.
    #[doc(alias = "Z3_OP_BUREM_I")]
    BuremI = 1083,
    /// Binary signed modulus.
    /// 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.
    #[doc(alias = "Z3_OP_BSMOD_I")]
    BsmodI = 1084,
    /// Undef/Null proof object.
    #[doc(alias = "Z3_OP_PR_UNDEF")]
    PrUndef = 1280,
    /// Proof for the expression 'true'.
    #[doc(alias = "Z3_OP_PR_TRUE")]
    PrTrue = 1281,
    /// Proof for a fact asserted by the user.
    #[doc(alias = "Z3_OP_PR_ASSERTED")]
    PrAsserted = 1282,
    /// Proof for a fact (tagged as goal) asserted by the user.
    #[doc(alias = "Z3_OP_PR_GOAL")]
    PrGoal = 1283,
    /// Given a proof for p and a proof for (implies p q), produces a proof for q.
    ///
    /// T1: p
    /// T2: (implies p q)
    /// [mp T1 T2]: q
    ///
    /// The second antecedents may also be a proof for (iff p q).
    #[doc(alias = "Z3_OP_PR_MODUS_PONENS")]
    PrModusPonens = 1284,
    /// A proof for (R t t), where R is a reflexive relation. This proof object has no antecedents.
    /// The only reflexive relations that are used are
    /// equivalence modulo namings, equality and equivalence.
    /// That is, R is either '~', '=' or 'iff'.
    #[doc(alias = "Z3_OP_PR_REFLEXIVITY")]
    PrReflexivity = 1285,
    /// Given an symmetric relation R and a proof for (R t s), produces a proof for (R s t).
    /// ```text
    /// T1: (R t s)
    /// [symmetry T1]: (R s t)
    /// ```
    /// T1 is the antecedent of this proof object.
    #[doc(alias = "Z3_OP_PR_SYMMETRY")]
    PrSymmetry = 1286,
    /// Given a transitive relation R, and proofs for (R t s) and (R s u), produces a proof
    /// for (R t u).
    /// ```text
    /// T1: (R t s)
    /// T2: (R s u)
    /// [trans T1 T2]: (R t u)
    /// ```
    #[doc(alias = "Z3_OP_PR_TRANSITIVITY")]
    PrTransitivity = 1287,
    /// Condensed transitivity proof.
    /// It combines several symmetry and transitivity proofs. Example:
    /// ```text
    /// T1: (R a b)
    /// T2: (R c b)
    /// T3: (R c d)
    /// [trans* T1 T2 T3]: (R a d)
    /// ```
    /// R must be a symmetric and transitive relation.
    ///
    /// Assuming that this proof object is a proof for (R s t), then
    /// a proof checker must check if it is possible to prove (R s t)
    /// using the antecedents, symmetry and transitivity.  That is,
    /// if there is a path from s to t, if we view every
    /// antecedent (R a b) as an edge between a and b.
    #[doc(alias = "Z3_OP_PR_TRANSITIVITY_STAR")]
    PrTransitivityStar = 1288,
    /// Monotonicity proof object.
    ///
    /// T1: (R t_1 s_1)
    /// ...
    /// Tn: (R t_n s_n)
    /// [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n))
    ///
    /// Remark: if t_i == s_i, then the antecedent Ti is suppressed.
    /// That is, reflexivity proofs are suppressed to save space.
    #[doc(alias = "Z3_OP_PR_MONOTONICITY")]
    PrMonotonicity = 1289,
    /// Given a proof for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)).
    ///
    /// T1: (~ p q)
    /// [quant-intro T1]: (~ (forall (x) p) (forall (x) q))
    #[doc(alias = "Z3_OP_PR_QUANT_INTRO")]
    PrQuantIntro = 1290,
    /// Given a proof p, produces a proof of lambda x . p, where x are free variables in p.
    ///
    /// T1: f
    /// [proof-bind T1] forall (x) f
    #[doc(alias = "Z3_OP_PR_BIND")]
    PrBind = 1291,
    /// Distributivity proof object.
    /// Given that f (= or) distributes over g (= and), produces a proof for
    /// ```text
    /// (= (f a (g c d))
    /// (g (f a c) (f a d)))
    /// ```
    /// If f and g are associative, this proof also justifies the following equality:
    /// ```text
    /// (= (f (g a b) (g c d))
    /// (g (f a c) (f a d) (f b c) (f b d)))
    /// ```
    /// where each f and g can have arbitrary number of arguments.
    ///
    /// This proof object has no antecedents.
    /// Remark. This rule is used by the CNF conversion pass and
    /// instantiated by f = or, and g = and.
    #[doc(alias = "Z3_OP_PR_DISTRIBUTIVITY")]
    PrDistributivity = 1292,
    /// Given a proof for (and l_1 ... l_n), produces a proof for l_i
    ///
    /// T1: (and l_1 ... l_n)
    /// [and-elim T1]: l_i
    #[doc(alias = "Z3_OP_PR_AND_ELIM")]
    PrAndElim = 1293,
    /// Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i).
    ///
    /// T1: (not (or l_1 ... l_n))
    /// [not-or-elim T1]: (not l_i)
    #[doc(alias = "Z3_OP_PR_NOT_OR_ELIM")]
    PrNotOrElim = 1294,
    /// A proof for a local rewriting step (= t s).
    /// The head function symbol of t is interpreted.
    ///
    /// This proof object has no antecedents.
    /// The conclusion of a rewrite rule is either an equality (= t s),
    /// an equivalence (iff t s), or equi-satisfiability (~ t s).
    /// Remark: if f is bool, then = is iff.
    /// Examples:
    /// ```text
    /// (= (+ x 0) x)
    /// (= (+ x 1 2) (+ 3 x))
    /// (iff (or x false) x)
    /// ```
    #[doc(alias = "Z3_OP_PR_REWRITE")]
    PrRewrite = 1295,
    /// A proof for rewriting an expression t into an expression s.
    /// This proof object can have n antecedents.
    /// The antecedents are proofs for equalities used as substitution rules.
    /// The proof rule is used in a few cases. The cases are:
    /// - When applying contextual simplification (CONTEXT_SIMPLIFIER=true)
    /// - When converting bit-vectors to Booleans (BIT2BOOL=true)
    #[doc(alias = "Z3_OP_PR_REWRITE_STAR")]
    PrRewriteStar = 1296,
    /// A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents.
    #[doc(alias = "Z3_OP_PR_PULL_QUANT")]
    PrPullQuant = 1297,
    /// A proof for:
    /// ```text
    /// (iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m] ... p_n[x_1 ... x_m]))
    /// (and (forall (x_1 ... x_m) p_1[x_1 ... x_m])
    /// ...
    /// (forall (x_1 ... x_m) p_n[x_1 ... x_m])))
    /// ```
    /// This proof object has no antecedents.
    #[doc(alias = "Z3_OP_PR_PUSH_QUANT")]
    PrPushQuant = 1298,
    /// A proof for (iff (forall (x_1 ... x_n y_1 ... y_m) p[x_1 ... x_n])
    /// (forall (x_1 ... x_n) p[x_1 ... x_n]))
    ///
    /// It is used to justify the elimination of unused variables.
    /// This proof object has no antecedents.
    #[doc(alias = "Z3_OP_PR_ELIM_UNUSED_VARS")]
    PrElimUnusedVars = 1299,
    /// A proof for destructive equality resolution:
    /// (iff (forall (x) (or (not (= x t)) P\[x])) P\[t])
    /// if x does not occur in t.
    ///
    /// This proof object has no antecedents.
    ///
    /// Several variables can be eliminated simultaneously.
    #[doc(alias = "Z3_OP_PR_DER")]
    PrDer = 1300,
    /// A proof of (or (not (forall (x) (P x))) (P a))
    #[doc(alias = "Z3_OP_PR_QUANT_INST")]
    PrQuantInst = 1301,
    /// Mark a hypothesis in a natural deduction style proof.
    #[doc(alias = "Z3_OP_PR_HYPOTHESIS")]
    PrHypothesis = 1302,
    ///
    /// T1: false
    /// [lemma T1]: (or (not l_1) ... (not l_n))
    ///
    /// This proof object has one antecedent: a hypothetical proof for false.
    /// It converts the proof in a proof for (or (not l_1) ... (not l_n)),
    /// when T1 contains the open hypotheses: l_1, ..., l_n.
    /// The hypotheses are closed after an application of a lemma.
    /// Furthermore, there are no other open hypotheses in the subtree covered by
    /// the lemma.
    #[doc(alias = "Z3_OP_PR_LEMMA")]
    PrLemma = 1303,
    /// ```text
    /// T1:      (or l_1 ... l_n l_1' ... l_m')
    /// T2:      (not l_1)
    /// ...
    /// T(n+1):  (not l_n)
    /// [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m')
    /// ```
    #[doc(alias = "Z3_OP_PR_UNIT_RESOLUTION")]
    PrUnitResolution = 1304,
    /// ```text
    /// T1: p
    /// [iff-true T1]: (iff p true)
    /// ```
    #[doc(alias = "Z3_OP_PR_IFF_TRUE")]
    PrIffTrue = 1305,
    /// ```text
    /// T1: (not p)
    /// [iff-false T1]: (iff p false)
    /// ```
    #[doc(alias = "Z3_OP_PR_IFF_FALSE")]
    PrIffFalse = 1306,
    ///
    /// \[comm\]: (= (f a b) (f b a))
    ///
    /// f is a commutative operator.
    ///
    /// This proof object has no antecedents.
    /// Remark: if f is bool, then = is iff.
    #[doc(alias = "Z3_OP_PR_COMMUTATIVITY")]
    PrCommutativity = 1307,
    /// Proof object used to justify Tseitin's like axioms:
    /// ```text
    /// (or (not (and p q)) p)
    /// (or (not (and p q)) q)
    /// (or (not (and p q r)) p)
    /// (or (not (and p q r)) q)
    /// (or (not (and p q r)) r)
    /// ...
    /// (or (and p q) (not p) (not q))
    /// (or (not (or p q)) p q)
    /// (or (or p q) (not p))
    /// (or (or p q) (not q))
    /// (or (not (iff p q)) (not p) q)
    /// (or (not (iff p q)) p (not q))
    /// (or (iff p q) (not p) (not q))
    /// (or (iff p q) p q)
    /// (or (not (ite a b c)) (not a) b)
    /// (or (not (ite a b c)) a c)
    /// (or (ite a b c) (not a) (not b))
    /// (or (ite a b c) a (not c))
    /// (or (not (not a)) (not a))
    /// (or (not a) a)
    /// ```
    /// This proof object has no antecedents.
    /// Note: all axioms are propositional tautologies.
    /// Note also that 'and' and 'or' can take multiple arguments.
    /// You can recover the propositional tautologies by
    /// unfolding the Boolean connectives in the axioms a small
    /// bounded number of steps (=3).
    #[doc(alias = "Z3_OP_PR_DEF_AXIOM")]
    PrDefAxiom = 1308,
    /// Clausal proof adding axiom
    #[doc(alias = "Z3_OP_PR_ASSUMPTION_ADD")]
    PrAssumptionAdd = 1309,
    /// Clausal proof lemma addition
    #[doc(alias = "Z3_OP_PR_LEMMA_ADD")]
    PrLemmaAdd = 1310,
    /// Clausal proof lemma deletion
    #[doc(alias = "Z3_OP_PR_REDUNDANT_DEL")]
    PrRedundantDel = 1311,
    /// ,
    /// Clausal proof trail of additions and deletions
    #[doc(alias = "Z3_OP_PR_CLAUSE_TRAIL")]
    PrClauseTrail = 1312,
    /// Introduces a name for a formula/term.
    /// Suppose e is an expression with free variables x, and def-intro
    /// introduces the name n(x). The possible cases are:
    ///
    /// When e is of Boolean type:
    /// \[def-intro\]: (and (or n (not e)) (or (not n) e))
    ///
    /// or:
    /// \[def-intro\]: (or (not n) e)
    /// when e only occurs positively.
    ///
    /// When e is of the form (ite cond th el):
    /// \[def-intro\]: (and (or (not cond) (= n th)) (or cond (= n el)))
    ///
    /// Otherwise:
    /// \[def-intro\]: (= n e)
    #[doc(alias = "Z3_OP_PR_DEF_INTRO")]
    PrDefIntro = 1313,
    ///
    /// [apply-def T1]: F ~ n
    ///
    /// F is 'equivalent' to n, given that T1 is a proof that
    /// n is a name for F.
    #[doc(alias = "Z3_OP_PR_APPLY_DEF")]
    PrApplyDef = 1314,
    ///
    /// T1: (iff p q)
    /// [iff~ T1]: (~ p q)
    #[doc(alias = "Z3_OP_PR_IFF_OEQ")]
    PrIffOeq = 1315,
    /// Proof for a (positive) NNF step. Example:
    ///
    /// T1: (not s_1) ~ r_1
    /// T2: (not s_2) ~ r_2
    /// T3: s_1 ~ r_1'
    /// T4: s_2 ~ r_2'
    /// [nnf-pos T1 T2 T3 T4]: (~ (iff s_1 s_2) (and (or r_1 r_2') (or r_1' r_2)))
    ///
    /// The negation normal form steps NNF_POS and NNF_NEG are used in the following cases:
    /// (a) When creating the NNF of a positive force quantifier.
    /// The quantifier is retained (unless the bound variables are eliminated).
    /// Example
    ///
    /// T1: q ~ q_new
    /// [nnf-pos T1]: (~ (forall (x T) q) (forall (x T) q_new))
    ///
    /// (b) When recursively creating NNF over Boolean formulas, where the top-level
    /// connective is changed during NNF conversion. The relevant Boolean connectives
    /// for NNF_POS are 'implies', 'iff', 'xor', 'ite'.
    /// NNF_NEG furthermore handles the case where negation is pushed
    /// over Boolean connectives 'and' and 'or'.
    #[doc(alias = "Z3_OP_PR_NNF_POS")]
    PrNnfPos = 1316,
    /// Proof for a (negative) NNF step. Examples:
    ///
    /// T1: (not s_1) ~ r_1
    /// ...
    /// Tn: (not s_n) ~ r_n
    /// [nnf-neg T1 ... Tn]: (not (and s_1 ... s_n)) ~ (or r_1 ... r_n)
    ///
    /// and
    ///
    /// T1: (not s_1) ~ r_1
    /// ...
    /// Tn: (not s_n) ~ r_n
    /// [nnf-neg T1 ... Tn]: (not (or s_1 ... s_n)) ~ (and r_1 ... r_n)
    ///
    /// and
    ///
    /// T1: (not s_1) ~ r_1
    /// T2: (not s_2) ~ r_2
    /// T3: s_1 ~ r_1'
    /// T4: s_2 ~ r_2'
    /// [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2))
    /// (and (or r_1 r_2) (or r_1' r_2')))
    #[doc(alias = "Z3_OP_PR_NNF_NEG")]
    PrNnfNeg = 1317,
    /// Proof for:
    ///
    /// \[sk\]: (~ (not (forall x (p x y))) (not (p (sk y) y)))
    /// \[sk\]: (~ (exists x (p x y)) (p (sk y) y))
    ///
    /// This proof object has no antecedents.
    #[doc(alias = "Z3_OP_PR_SKOLEMIZE")]
    PrSkolemize = 1318,
    /// Modus ponens style rule for equi-satisfiability.
    ///
    /// T1: p
    /// T2: (~ p q)
    /// [mp~ T1 T2]: q
    #[doc(alias = "Z3_OP_PR_MODUS_PONENS_OEQ")]
    PrModusPonensOeq = 1319,
    /// Generic proof for theory lemmas.
    /// The theory lemma function comes with one or more parameters.
    /// The first parameter indicates the name of the theory.
    /// For the theory of arithmetic, additional parameters provide hints for
    /// checking the theory lemma.
    /// The hints for arithmetic are:
    ///
    /// - farkas - followed by rational coefficients. Multiply the coefficients to the
    /// inequalities in the lemma, add the (negated) inequalities and obtain a contradiction.
    ///
    /// - triangle-eq - Indicates a lemma related to the equivalence:
    ///
    /// (iff (= t1 t2) (and (<= t1 t2) (<= t2 t1)))
    ///
    /// - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test.
    #[doc(alias = "Z3_OP_PR_TH_LEMMA")]
    PrThLemma = 1320,
    /// Hyper-resolution rule.
    ///
    /// The premises of the rules is a sequence of clauses.
    /// The first clause argument is the main clause of the rule.
    /// with a literal from the first (main) clause.
    ///
    /// Premises of the rules are of the form
    /// ```text
    /// (or l0 l1 l2 .. ln)
    /// ```
    /// or
    /// ```text
    /// (=> (and l1 l2 .. ln) l0)
    /// ```
    /// or in the most general (ground) form:
    /// ```text
    /// (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln))
    /// ```
    /// In other words we use the following (Prolog style) convention for Horn
    /// implications:
    /// The head of a Horn implication is position 0,
    /// the first conjunct in the body of an implication is position 1
    /// the second conjunct in the body of an implication is position 2
    ///
    /// For general implications where the head is a disjunction, the
    /// first n positions correspond to the n disjuncts in the head.
    /// The next m positions correspond to the m conjuncts in the body.
    ///
    /// The premises can be universally quantified so that the most
    /// general non-ground form is:
    ///
    /// ```text
    /// (forall (vars) (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln)))
    /// ```
    ///
    /// The hyper-resolution rule takes a sequence of parameters.
    /// The parameters are substitutions of bound variables separated by pairs
    /// of literal positions from the main clause and side clause.
    #[doc(alias = "Z3_OP_PR_HYPER_RESOLVE")]
    PrHyperResolve = 1321,
    /// Insert a record into a relation.
    /// The function takes `n`+1 arguments, where the first argument is the relation and the remaining `n` elements
    /// correspond to the `n` columns of the relation.
    #[doc(alias = "Z3_OP_RA_STORE")]
    RaStore = 1536,
    /// Creates the empty relation.
    #[doc(alias = "Z3_OP_RA_EMPTY")]
    RaEmpty = 1537,
    /// Tests if the relation is empty.
    #[doc(alias = "Z3_OP_RA_IS_EMPTY")]
    RaIsEmpty = 1538,
    /// Create the relational join.
    #[doc(alias = "Z3_OP_RA_JOIN")]
    RaJoin = 1539,
    /// Create the union or convex hull of two relations.
    /// The function takes two arguments.
    #[doc(alias = "Z3_OP_RA_UNION")]
    RaUnion = 1540,
    /// Widen two relations.
    /// The function takes two arguments.
    #[doc(alias = "Z3_OP_RA_WIDEN")]
    RaWiden = 1541,
    /// Project the columns (provided as numbers in the parameters).
    /// The function takes one argument.
    #[doc(alias = "Z3_OP_RA_PROJECT")]
    RaProject = 1542,
    /// Filter (restrict) a relation with respect to a predicate.
    /// The first argument is a relation.
    /// The second argument is a predicate with free de-Bruijn indices
    /// corresponding to the columns of the relation.
    /// So the first column in the relation has index 0.
    #[doc(alias = "Z3_OP_RA_FILTER")]
    RaFilter = 1543,
    /// Intersect the first relation with respect to negation
    /// of the second relation (the function takes two arguments).
    /// Logically, the specification can be described by a function
    ///
    /// target = filter_by_negation(pos, neg, columns)
    ///
    /// where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, such that
    /// target are elements in x in pos, such that there is no y in neg that agrees with
    /// x on the columns c1, d1, .., cN, dN.
    #[doc(alias = "Z3_OP_RA_NEGATION_FILTER")]
    RaNegationFilter = 1544,
    /// rename columns in the relation.
    /// The function takes one argument.
    /// The parameters contain the renaming as a cycle.
    #[doc(alias = "Z3_OP_RA_RENAME")]
    RaRename = 1545,
    /// Complement the relation.
    #[doc(alias = "Z3_OP_RA_COMPLEMENT")]
    RaComplement = 1546,
    /// Check if a record is an element of the relation.
    /// The function takes `n`+1 arguments, where the first argument is a relation,
    /// and the remaining `n` arguments correspond to a record.
    #[doc(alias = "Z3_OP_RA_SELECT")]
    RaSelect = 1547,
    /// Create a fresh copy (clone) of a relation.
    /// The function is logically the identity, but
    /// in the context of a register machine allows
    /// for `Z3_OP_RA_UNION` to perform destructive updates to the first argument.
    #[doc(alias = "Z3_OP_RA_CLONE")]
    RaClone = 1548,
    /// Corresponds to `Z3_OP_FD_CONSTANT` in the C API.
    #[doc(alias = "Z3_OP_FD_CONSTANT")]
    FdConstant = 1549,
    /// A less than predicate over the finite domain Z3_FINITE_DOMAIN_SORT.
    #[doc(alias = "Z3_OP_FD_LT")]
    FdLt = 1550,
    /// Corresponds to `Z3_OP_SEQ_UNIT` in the C API.
    #[doc(alias = "Z3_OP_SEQ_UNIT")]
    SeqUnit = 1551,
    /// Corresponds to `Z3_OP_SEQ_EMPTY` in the C API.
    #[doc(alias = "Z3_OP_SEQ_EMPTY")]
    SeqEmpty = 1552,
    /// Corresponds to `Z3_OP_SEQ_CONCAT` in the C API.
    #[doc(alias = "Z3_OP_SEQ_CONCAT")]
    SeqConcat = 1553,
    /// Corresponds to `Z3_OP_SEQ_PREFIX` in the C API.
    #[doc(alias = "Z3_OP_SEQ_PREFIX")]
    SeqPrefix = 1554,
    /// Corresponds to `Z3_OP_SEQ_SUFFIX` in the C API.
    #[doc(alias = "Z3_OP_SEQ_SUFFIX")]
    SeqSuffix = 1555,
    /// Corresponds to `Z3_OP_SEQ_CONTAINS` in the C API.
    #[doc(alias = "Z3_OP_SEQ_CONTAINS")]
    SeqContains = 1556,
    /// Corresponds to `Z3_OP_SEQ_EXTRACT` in the C API.
    #[doc(alias = "Z3_OP_SEQ_EXTRACT")]
    SeqExtract = 1557,
    /// Corresponds to `Z3_OP_SEQ_REPLACE` in the C API.
    #[doc(alias = "Z3_OP_SEQ_REPLACE")]
    SeqReplace = 1558,
    /// Corresponds to `Z3_OP_SEQ_REPLACE_RE` in the C API.
    #[doc(alias = "Z3_OP_SEQ_REPLACE_RE")]
    SeqReplaceRe = 1559,
    /// Corresponds to `Z3_OP_SEQ_REPLACE_RE_ALL` in the C API.
    #[doc(alias = "Z3_OP_SEQ_REPLACE_RE_ALL")]
    SeqReplaceReAll = 1560,
    /// Corresponds to `Z3_OP_SEQ_REPLACE_ALL` in the C API.
    #[doc(alias = "Z3_OP_SEQ_REPLACE_ALL")]
    SeqReplaceAll = 1561,
    /// Corresponds to `Z3_OP_SEQ_AT` in the C API.
    #[doc(alias = "Z3_OP_SEQ_AT")]
    SeqAt = 1562,
    /// Corresponds to `Z3_OP_SEQ_NTH` in the C API.
    #[doc(alias = "Z3_OP_SEQ_NTH")]
    SeqNth = 1563,
    /// Corresponds to `Z3_OP_SEQ_LENGTH` in the C API.
    #[doc(alias = "Z3_OP_SEQ_LENGTH")]
    SeqLength = 1564,
    /// Corresponds to `Z3_OP_SEQ_INDEX` in the C API.
    #[doc(alias = "Z3_OP_SEQ_INDEX")]
    SeqIndex = 1565,
    /// Corresponds to `Z3_OP_SEQ_LAST_INDEX` in the C API.
    #[doc(alias = "Z3_OP_SEQ_LAST_INDEX")]
    SeqLastIndex = 1566,
    /// Corresponds to `Z3_OP_SEQ_TO_RE` in the C API.
    #[doc(alias = "Z3_OP_SEQ_TO_RE")]
    SeqToRe = 1567,
    /// Corresponds to `Z3_OP_SEQ_IN_RE` in the C API.
    #[doc(alias = "Z3_OP_SEQ_IN_RE")]
    SeqInRe = 1568,
    /// Corresponds to `Z3_OP_SEQ_MAP` in the C API.
    #[doc(alias = "Z3_OP_SEQ_MAP")]
    SeqMap = 1569,
    /// Corresponds to `Z3_OP_SEQ_MAPI` in the C API.
    #[doc(alias = "Z3_OP_SEQ_MAPI")]
    SeqMapi = 1570,
    /// Corresponds to `Z3_OP_SEQ_FOLDL` in the C API.
    #[doc(alias = "Z3_OP_SEQ_FOLDL")]
    SeqFoldl = 1571,
    /// Corresponds to `Z3_OP_SEQ_FOLDLI` in the C API.
    #[doc(alias = "Z3_OP_SEQ_FOLDLI")]
    SeqFoldli = 1572,
    /// Corresponds to `Z3_OP_STR_TO_INT` in the C API.
    #[doc(alias = "Z3_OP_STR_TO_INT")]
    StrToInt = 1573,
    /// Corresponds to `Z3_OP_INT_TO_STR` in the C API.
    #[doc(alias = "Z3_OP_INT_TO_STR")]
    IntToStr = 1574,
    /// Corresponds to `Z3_OP_UBV_TO_STR` in the C API.
    #[doc(alias = "Z3_OP_UBV_TO_STR")]
    UbvToStr = 1575,
    /// Corresponds to `Z3_OP_SBV_TO_STR` in the C API.
    #[doc(alias = "Z3_OP_SBV_TO_STR")]
    SbvToStr = 1576,
    /// Corresponds to `Z3_OP_STR_TO_CODE` in the C API.
    #[doc(alias = "Z3_OP_STR_TO_CODE")]
    StrToCode = 1577,
    /// Corresponds to `Z3_OP_STR_FROM_CODE` in the C API.
    #[doc(alias = "Z3_OP_STR_FROM_CODE")]
    StrFromCode = 1578,
    /// Corresponds to `Z3_OP_STRING_LT` in the C API.
    #[doc(alias = "Z3_OP_STRING_LT")]
    StringLt = 1579,
    /// Corresponds to `Z3_OP_STRING_LE` in the C API.
    #[doc(alias = "Z3_OP_STRING_LE")]
    StringLe = 1580,
    /// Corresponds to `Z3_OP_RE_PLUS` in the C API.
    #[doc(alias = "Z3_OP_RE_PLUS")]
    RePlus = 1581,
    /// Corresponds to `Z3_OP_RE_STAR` in the C API.
    #[doc(alias = "Z3_OP_RE_STAR")]
    ReStar = 1582,
    /// Corresponds to `Z3_OP_RE_OPTION` in the C API.
    #[doc(alias = "Z3_OP_RE_OPTION")]
    ReOption = 1583,
    /// Corresponds to `Z3_OP_RE_CONCAT` in the C API.
    #[doc(alias = "Z3_OP_RE_CONCAT")]
    ReConcat = 1584,
    /// Corresponds to `Z3_OP_RE_UNION` in the C API.
    #[doc(alias = "Z3_OP_RE_UNION")]
    ReUnion = 1585,
    /// Corresponds to `Z3_OP_RE_RANGE` in the C API.
    #[doc(alias = "Z3_OP_RE_RANGE")]
    ReRange = 1586,
    /// Corresponds to `Z3_OP_RE_DIFF` in the C API.
    #[doc(alias = "Z3_OP_RE_DIFF")]
    ReDiff = 1587,
    /// Corresponds to `Z3_OP_RE_INTERSECT` in the C API.
    #[doc(alias = "Z3_OP_RE_INTERSECT")]
    ReIntersect = 1588,
    /// Corresponds to `Z3_OP_RE_LOOP` in the C API.
    #[doc(alias = "Z3_OP_RE_LOOP")]
    ReLoop = 1589,
    /// Corresponds to `Z3_OP_RE_POWER` in the C API.
    #[doc(alias = "Z3_OP_RE_POWER")]
    RePower = 1590,
    /// Corresponds to `Z3_OP_RE_COMPLEMENT` in the C API.
    #[doc(alias = "Z3_OP_RE_COMPLEMENT")]
    ReComplement = 1591,
    /// Corresponds to `Z3_OP_RE_EMPTY_SET` in the C API.
    #[doc(alias = "Z3_OP_RE_EMPTY_SET")]
    ReEmptySet = 1592,
    /// Corresponds to `Z3_OP_RE_FULL_SET` in the C API.
    #[doc(alias = "Z3_OP_RE_FULL_SET")]
    ReFullSet = 1593,
    /// Corresponds to `Z3_OP_RE_FULL_CHAR_SET` in the C API.
    #[doc(alias = "Z3_OP_RE_FULL_CHAR_SET")]
    ReFullCharSet = 1594,
    /// Corresponds to `Z3_OP_RE_OF_PRED` in the C API.
    #[doc(alias = "Z3_OP_RE_OF_PRED")]
    ReOfPred = 1595,
    /// Corresponds to `Z3_OP_RE_REVERSE` in the C API.
    #[doc(alias = "Z3_OP_RE_REVERSE")]
    ReReverse = 1596,
    /// Corresponds to `Z3_OP_RE_DERIVATIVE` in the C API.
    #[doc(alias = "Z3_OP_RE_DERIVATIVE")]
    ReDerivative = 1597,
    /// Corresponds to `Z3_OP_CHAR_CONST` in the C API.
    #[doc(alias = "Z3_OP_CHAR_CONST")]
    CharConst = 1598,
    /// Corresponds to `Z3_OP_CHAR_LE` in the C API.
    #[doc(alias = "Z3_OP_CHAR_LE")]
    CharLe = 1599,
    /// Corresponds to `Z3_OP_CHAR_TO_INT` in the C API.
    #[doc(alias = "Z3_OP_CHAR_TO_INT")]
    CharToInt = 1600,
    /// Corresponds to `Z3_OP_CHAR_TO_BV` in the C API.
    #[doc(alias = "Z3_OP_CHAR_TO_BV")]
    CharToBv = 1601,
    /// Corresponds to `Z3_OP_CHAR_FROM_BV` in the C API.
    #[doc(alias = "Z3_OP_CHAR_FROM_BV")]
    CharFromBv = 1602,
    /// Corresponds to `Z3_OP_CHAR_IS_DIGIT` in the C API.
    #[doc(alias = "Z3_OP_CHAR_IS_DIGIT")]
    CharIsDigit = 1603,
    /// A label (used by the Boogie Verification condition generator).
    /// The label has two parameters, a string and a Boolean polarity.
    /// It takes one argument, a formula.
    #[doc(alias = "Z3_OP_LABEL")]
    Label = 1792,
    /// A label literal (used by the Boogie Verification condition generator).
    /// A label literal has a set of string parameters. It takes no arguments.
    #[doc(alias = "Z3_OP_LABEL_LIT")]
    LabelLit = 1793,
    /// datatype constructor.
    #[doc(alias = "Z3_OP_DT_CONSTRUCTOR")]
    DtConstructor = 2048,
    /// datatype recognizer.
    #[doc(alias = "Z3_OP_DT_RECOGNISER")]
    DtRecogniser = 2049,
    /// datatype recognizer.
    #[doc(alias = "Z3_OP_DT_IS")]
    DtIs = 2050,
    /// datatype accessor.
    #[doc(alias = "Z3_OP_DT_ACCESSOR")]
    DtAccessor = 2051,
    /// datatype field update.
    #[doc(alias = "Z3_OP_DT_UPDATE_FIELD")]
    DtUpdateField = 2052,
    /// Cardinality constraint.
    /// E.g., x + y + z <= 2
    #[doc(alias = "Z3_OP_PB_AT_MOST")]
    PbAtMost = 2304,
    /// Cardinality constraint.
    /// E.g., x + y + z >= 2
    #[doc(alias = "Z3_OP_PB_AT_LEAST")]
    PbAtLeast = 2305,
    /// Generalized Pseudo-Boolean cardinality constraint.
    /// Example  2*x + 3*y <= 4
    #[doc(alias = "Z3_OP_PB_LE")]
    PbLe = 2306,
    /// Generalized Pseudo-Boolean cardinality constraint.
    /// Example  2*x + 3*y + 2*z >= 4
    #[doc(alias = "Z3_OP_PB_GE")]
    PbGe = 2307,
    /// Generalized Pseudo-Boolean equality constraint.
    /// Example  2*x + 1*y + 2*z + 1*u = 4
    #[doc(alias = "Z3_OP_PB_EQ")]
    PbEq = 2308,
    /// A relation that is a total linear order
    #[doc(alias = "Z3_OP_SPECIAL_RELATION_LO")]
    SpecialRelationLo = 40960,
    /// A relation that is a partial order
    #[doc(alias = "Z3_OP_SPECIAL_RELATION_PO")]
    SpecialRelationPo = 40961,
    /// A relation that is a piecewise linear order
    #[doc(alias = "Z3_OP_SPECIAL_RELATION_PLO")]
    SpecialRelationPlo = 40962,
    /// A relation that is a tree order
    #[doc(alias = "Z3_OP_SPECIAL_RELATION_TO")]
    SpecialRelationTo = 40963,
    /// Transitive closure of a relation
    #[doc(alias = "Z3_OP_SPECIAL_RELATION_TC")]
    SpecialRelationTc = 40964,
    /// Transitive reflexive closure of a relation
    #[doc(alias = "Z3_OP_SPECIAL_RELATION_TRC")]
    SpecialRelationTrc = 40965,
    /// Floating-point rounding mode RNE
    #[doc(alias = "Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN")]
    FpaRmNearestTiesToEven = 45056,
    /// Floating-point rounding mode RNA
    #[doc(alias = "Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY")]
    FpaRmNearestTiesToAway = 45057,
    /// Floating-point rounding mode RTP
    #[doc(alias = "Z3_OP_FPA_RM_TOWARD_POSITIVE")]
    FpaRmTowardPositive = 45058,
    /// Floating-point rounding mode RTN
    #[doc(alias = "Z3_OP_FPA_RM_TOWARD_NEGATIVE")]
    FpaRmTowardNegative = 45059,
    /// Floating-point rounding mode RTZ
    #[doc(alias = "Z3_OP_FPA_RM_TOWARD_ZERO")]
    FpaRmTowardZero = 45060,
    /// Floating-point value
    #[doc(alias = "Z3_OP_FPA_NUM")]
    FpaNum = 45061,
    /// Floating-point +oo
    #[doc(alias = "Z3_OP_FPA_PLUS_INF")]
    FpaPlusInf = 45062,
    /// Floating-point -oo
    #[doc(alias = "Z3_OP_FPA_MINUS_INF")]
    FpaMinusInf = 45063,
    /// Floating-point NaN
    #[doc(alias = "Z3_OP_FPA_NAN")]
    FpaNan = 45064,
    /// Floating-point +zero
    #[doc(alias = "Z3_OP_FPA_PLUS_ZERO")]
    FpaPlusZero = 45065,
    /// Floating-point -zero
    #[doc(alias = "Z3_OP_FPA_MINUS_ZERO")]
    FpaMinusZero = 45066,
    /// Floating-point addition
    #[doc(alias = "Z3_OP_FPA_ADD")]
    FpaAdd = 45067,
    /// Floating-point subtraction
    #[doc(alias = "Z3_OP_FPA_SUB")]
    FpaSub = 45068,
    /// Floating-point negation
    #[doc(alias = "Z3_OP_FPA_NEG")]
    FpaNeg = 45069,
    /// Floating-point multiplication
    #[doc(alias = "Z3_OP_FPA_MUL")]
    FpaMul = 45070,
    /// Floating-point division
    #[doc(alias = "Z3_OP_FPA_DIV")]
    FpaDiv = 45071,
    /// Floating-point remainder
    #[doc(alias = "Z3_OP_FPA_REM")]
    FpaRem = 45072,
    /// Floating-point absolute value
    #[doc(alias = "Z3_OP_FPA_ABS")]
    FpaAbs = 45073,
    /// Floating-point minimum
    #[doc(alias = "Z3_OP_FPA_MIN")]
    FpaMin = 45074,
    /// Floating-point maximum
    #[doc(alias = "Z3_OP_FPA_MAX")]
    FpaMax = 45075,
    /// Floating-point fused multiply-add
    #[doc(alias = "Z3_OP_FPA_FMA")]
    FpaFma = 45076,
    /// Floating-point square root
    #[doc(alias = "Z3_OP_FPA_SQRT")]
    FpaSqrt = 45077,
    /// Floating-point round to integral
    #[doc(alias = "Z3_OP_FPA_ROUND_TO_INTEGRAL")]
    FpaRoundToIntegral = 45078,
    /// Floating-point equality
    #[doc(alias = "Z3_OP_FPA_EQ")]
    FpaEq = 45079,
    /// Floating-point less than
    #[doc(alias = "Z3_OP_FPA_LT")]
    FpaLt = 45080,
    /// Floating-point greater than
    #[doc(alias = "Z3_OP_FPA_GT")]
    FpaGt = 45081,
    /// Floating-point less than or equal
    #[doc(alias = "Z3_OP_FPA_LE")]
    FpaLe = 45082,
    /// Floating-point greater than or equal
    #[doc(alias = "Z3_OP_FPA_GE")]
    FpaGe = 45083,
    /// Floating-point isNaN
    #[doc(alias = "Z3_OP_FPA_IS_NAN")]
    FpaIsNan = 45084,
    /// Floating-point isInfinite
    #[doc(alias = "Z3_OP_FPA_IS_INF")]
    FpaIsInf = 45085,
    /// Floating-point isZero
    #[doc(alias = "Z3_OP_FPA_IS_ZERO")]
    FpaIsZero = 45086,
    /// Floating-point isNormal
    #[doc(alias = "Z3_OP_FPA_IS_NORMAL")]
    FpaIsNormal = 45087,
    /// Floating-point isSubnormal
    #[doc(alias = "Z3_OP_FPA_IS_SUBNORMAL")]
    FpaIsSubnormal = 45088,
    /// Floating-point isNegative
    #[doc(alias = "Z3_OP_FPA_IS_NEGATIVE")]
    FpaIsNegative = 45089,
    /// Floating-point isPositive
    #[doc(alias = "Z3_OP_FPA_IS_POSITIVE")]
    FpaIsPositive = 45090,
    /// Floating-point constructor from 3 bit-vectors
    #[doc(alias = "Z3_OP_FPA_FP")]
    FpaFp = 45091,
    /// Floating-point conversion (various)
    #[doc(alias = "Z3_OP_FPA_TO_FP")]
    FpaToFp = 45092,
    /// Floating-point conversion from unsigned bit-vector
    #[doc(alias = "Z3_OP_FPA_TO_FP_UNSIGNED")]
    FpaToFpUnsigned = 45093,
    /// Floating-point conversion to unsigned bit-vector
    #[doc(alias = "Z3_OP_FPA_TO_UBV")]
    FpaToUbv = 45094,
    /// Floating-point conversion to signed bit-vector
    #[doc(alias = "Z3_OP_FPA_TO_SBV")]
    FpaToSbv = 45095,
    /// Floating-point conversion to real number
    #[doc(alias = "Z3_OP_FPA_TO_REAL")]
    FpaToReal = 45096,
    /// Floating-point conversion to IEEE-754 bit-vector
    #[doc(alias = "Z3_OP_FPA_TO_IEEE_BV")]
    FpaToIeeeBv = 45097,
    /// (Implicitly) represents the internal bitvector-
    /// representation of a floating-point term (used for the lazy encoding
    /// of non-relevant terms in theory_fpa)
    #[doc(alias = "Z3_OP_FPA_BVWRAP")]
    FpaBvwrap = 45098,
    /// Conversion of a 3-bit bit-vector term to a
    /// floating-point rounding-mode term
    ///
    /// The conversion uses the following values:
    /// 0 = 000 = Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN,
    /// 1 = 001 = Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY,
    /// 2 = 010 = Z3_OP_FPA_RM_TOWARD_POSITIVE,
    /// 3 = 011 = Z3_OP_FPA_RM_TOWARD_NEGATIVE,
    /// 4 = 100 = Z3_OP_FPA_RM_TOWARD_ZERO.
    #[doc(alias = "Z3_OP_FPA_BV2RM")]
    FpaBv2rm = 45099,
    /// internal (often interpreted) symbol, but no additional
    /// information is exposed. Tools may use the string representation of the
    /// function declaration to obtain more information.
    #[doc(alias = "Z3_OP_INTERNAL")]
    Internal = 45100,
    /// function declared as recursive
    #[doc(alias = "Z3_OP_RECURSIVE")]
    Recursive = 45101,
    /// kind used for uninterpreted symbols.
    #[doc(alias = "Z3_OP_UNINTERPRETED")]
    Uninterpreted = 45102,
}
pub type Z3_decl_kind = DeclKind;
/// The different kinds of parameters that can be associated with parameter sets.
/// (see [`Z3_mk_params`]).
#[doc(alias = "Z3_param_kind")]
#[repr(u32)]
#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)]
pub enum ParamKind {
    /// integer parameters.
    #[doc(alias = "Z3_PK_UINT")]
    Uint = 0,
    /// boolean parameters.
    #[doc(alias = "Z3_PK_BOOL")]
    Bool = 1,
    /// double parameters.
    #[doc(alias = "Z3_PK_DOUBLE")]
    Double = 2,
    /// symbol parameters.
    #[doc(alias = "Z3_PK_SYMBOL")]
    Symbol = 3,
    /// string parameters.
    #[doc(alias = "Z3_PK_STRING")]
    String = 4,
    /// all internal parameter kinds which are not exposed in the API.
    #[doc(alias = "Z3_PK_OTHER")]
    Other = 5,
    /// invalid parameter.
    #[doc(alias = "Z3_PK_INVALID")]
    Invalid = 6,
}
pub type Z3_param_kind = ParamKind;
/// Z3 pretty printing modes (See [`Z3_set_ast_print_mode`]).
#[doc(alias = "Z3_ast_print_mode")]
#[repr(u32)]
#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)]
pub enum AstPrintMode {
    /// Print AST nodes in SMTLIB verbose format.
    #[doc(alias = "Z3_PRINT_SMTLIB_FULL")]
    SmtlibFull = 0,
    /// Print AST nodes using a low-level format.
    #[doc(alias = "Z3_PRINT_LOW_LEVEL")]
    LowLevel = 1,
    /// Print AST nodes in SMTLIB 2.x compliant format.
    #[doc(alias = "Z3_PRINT_SMTLIB2_COMPLIANT")]
    Smtlib2Compliant = 2,
}
pub type Z3_ast_print_mode = AstPrintMode;
/// Z3 error codes (See [`Z3_get_error_code`]).
#[doc(alias = "Z3_error_code")]
#[repr(u32)]
#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)]
pub enum ErrorCode {
    /// No error.
    #[doc(alias = "Z3_OK")]
    Ok = 0,
    /// User tried to build an invalid (type incorrect) AST.
    #[doc(alias = "Z3_SORT_ERROR")]
    SortError = 1,
    /// Index out of bounds.
    #[doc(alias = "Z3_IOB")]
    Iob = 2,
    /// Invalid argument was provided.
    #[doc(alias = "Z3_INVALID_ARG")]
    InvalidArg = 3,
    /// An error occurred when parsing a string or file.
    #[doc(alias = "Z3_PARSER_ERROR")]
    ParserError = 4,
    /// Parser output is not available, that is, user didn't invoke [`Z3_parse_smtlib2_string`] or [`Z3_parse_smtlib2_file`].
    #[doc(alias = "Z3_NO_PARSER")]
    NoParser = 5,
    /// Invalid pattern was used to build a quantifier.
    #[doc(alias = "Z3_INVALID_PATTERN")]
    InvalidPattern = 6,
    /// A memory allocation failure was encountered.
    #[doc(alias = "Z3_MEMOUT_FAIL")]
    MemoutFail = 7,
    /// A file could not be accessed.
    #[doc(alias = "Z3_FILE_ACCESS_ERROR")]
    FileAccessError = 8,
    /// An error internal to Z3 occurred.
    #[doc(alias = "Z3_INTERNAL_FATAL")]
    InternalFatal = 9,
    /// API call is invalid in the current state.
    #[doc(alias = "Z3_INVALID_USAGE")]
    InvalidUsage = 10,
    /// Trying to decrement the reference counter of an AST that was deleted or the reference counter was not initialized with [`Z3_inc_ref`].
    #[doc(alias = "Z3_DEC_REF_ERROR")]
    DecRefError = 11,
    /// Internal Z3 exception. Additional details can be retrieved using [`Z3_get_error_msg`].
    #[doc(alias = "Z3_EXCEPTION")]
    Exception = 12,
}
pub type Z3_error_code = ErrorCode;
/// A Goal is essentially a set of formulas.
/// Z3 provide APIs for building strategies/tactics for solving and transforming Goals.
/// Some of these transformations apply under/over approximations.
#[doc(alias = "Z3_goal_prec")]
#[repr(u32)]
#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)]
pub enum GoalPrec {
    /// Approximations/Relaxations were not applied on the goal (sat and unsat answers were preserved).
    #[doc(alias = "Z3_GOAL_PRECISE")]
    Precise = 0,
    /// Goal is the product of a under-approximation (sat answers are preserved).
    #[doc(alias = "Z3_GOAL_UNDER")]
    Under = 1,
    /// Goal is the product of an over-approximation (unsat answers are preserved).
    #[doc(alias = "Z3_GOAL_OVER")]
    Over = 2,
    /// Goal is garbage (it is the product of over- and under-approximations, sat and unsat answers are not preserved).
    #[doc(alias = "Z3_GOAL_UNDER_OVER")]
    UnderOver = 3,
}
pub type Z3_goal_prec = GoalPrec;