#[repr(u32)]
pub enum AstKind {
Numeral,
App,
Var,
Quantifier,
Sort,
FuncDecl,
Unknown,
}
Expand description
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
This corresponds to Z3_ast_kind
in the C API.
Variants§
Numeral
numeral constants
This corresponds to Z3_NUMERAL_AST
in the C API.
App
constant and applications
This corresponds to Z3_APP_AST
in the C API.
Var
bound variables
This corresponds to Z3_VAR_AST
in the C API.
Quantifier
quantifiers
This corresponds to Z3_QUANTIFIER_AST
in the C API.
Sort
sort
This corresponds to Z3_SORT_AST
in the C API.
FuncDecl
function declaration
This corresponds to Z3_FUNC_DECL_AST
in the C API.
Unknown
internal
This corresponds to Z3_UNKNOWN_AST
in the C API.