Structs
Abstract syntax tree node. That is, the data structure used in Z3
to represent terms, formulas, and types.
Configuration used to initialize logical contexts.
Manager of all other Z3 objects, global configuration options, etc.
Model for the constraints inserted into the logical context.
Context for solving optimization queries.
(Incremental) solver, possibly specialized by a particular tactic or logic.
Symbols are used to name several term and type constructors.