[][src]Crate z3

Structs

Ast

Abstract syntax tree node. That is, the data structure used in Z3 to represent terms, formulas, and types.

Config

Configuration used to initialize logical contexts.

Context

Manager of all other Z3 objects, global configuration options, etc.

Model

Model for the constraints inserted into the logical context.

Optimize

Context for solving optimization queries.

Solver

(Incremental) solver, possibly specialized by a particular tactic or logic.

Sort

Kind of Ast used to represent types.

Symbol

Symbols are used to name several term and type constructors.