module AST: sig
.. end
The abstract syntax tree (AST) module
type
ast
module ASTVector: sig
.. end
Vectors of ASTs
module ASTMap: sig
.. end
Map from AST to AST
val hash : ast -> int
The AST's hash code.
Returns A hash code
val get_id : ast -> int
A unique identifier for the AST (unique among all ASTs).
val get_ast_kind : ast -> Z3enums.ast_kind
The kind of the AST.
val is_expr : ast -> bool
Indicates whether the AST is an Expr
val is_var : ast -> bool
Indicates whether the AST is a bound variable
val is_quantifier : ast -> bool
Indicates whether the AST is a Quantifier
val is_sort : ast -> bool
Indicates whether the AST is a Sort
val is_func_decl : ast -> bool
Indicates whether the AST is a func_decl
val to_string : ast -> string
A string representation of the AST.
val to_sexpr : ast -> string
A string representation of the AST in s-expression notation.
val equal : ast -> ast -> bool
Comparison operator.
Returns True if the two ast's are from the same context
and represent the same sort; false otherwise.
val compare : ast -> ast -> int
Object Comparison.
Returns Negative if the first ast should be sorted before the second, positive if after else zero.
val translate : ast -> context -> ast
Translates (copies) the AST to another context.
Returns A copy of the AST which is associated with the other context.
val unwrap_ast : ast -> Z3native.ptr
Unwraps an AST.
This function is used for transitions between native and
managed objects. It returns the native pointer to the AST. Note that
AST objects are reference counted and unwrapping an AST disables automatic
reference counting, i.e., all references to the IntPtr that is returned
must be handled externally and through native calls (see e.g.,
Z3native.inc_ref
).
AST.wrap_ast
val wrap_ast : context -> Z3native.z3_ast -> ast
Wraps an AST.
This function is used for transitions between native and
managed objects. Note that the native ast that is passed must be a
native object obtained from Z3 (e.g., through AST.unwrap_ast
)
and that it must have a correct reference count (see e.g.,
Z3native.inc_ref
).