Module Z3.AST

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.

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.