Module z3::ast

Abstract syntax tree (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.

Float

Ast node representing a float value.

Int

Ast node representing an integer value.

Real

Ast node representing a real value.

Set

Ast node representing a set value.

String

Ast node representing a string value.

Enums

AstKind

The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.

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.