Module z3::ast

Structs

Array	Ast node representing an array value. An array in Z3 is a mapping from indices to values.
BV	Ast node representing a bitvector value.
Bool	Ast node representing a boolean value.
Datatype	Ast node representing a datatype or enumeration value.
Dynamic	A dynamically typed Ast node.
Int	Ast node representing an integer value.
Real	Ast node representing a real value.
Set	Ast node representing a set value.

Traits

Ast	Abstract syntax tree (AST) nodes represent terms, constants, or expressions. The Ast trait contains methods common to all AST subtypes.

Functions

exists_const	Create an existential quantifier.
forall_const	Create a universal quantifier.