Crate z3

Modules

ast

Structs

Config	Configuration used to initialize logical contexts.
Context	Manager of all other Z3 objects, global configuration options, etc.
DatatypeBuilder	Build a datatype sort.
DatatypeSort
DatatypeVariant
FuncDecl	Function declaration. Every constant and function have an associated declaration.
Model	Model for the constraints inserted into the logical context.
Optimize	Context for solving optimization queries.
Params
Pattern	A pattern for quantifier instantiation, used to guide quantifier instantiation.
Solver	(Incremental) solver, possibly specialized by a particular tactic or logic.
Sort	Sorts represent the various 'types' of Asts.

Enums

SatResult	Result of a satisfiability query.
Symbol	Symbols are used to name several term and type constructors.