[−][src]Crate z3
Modules
ast | |
datatype_builder |
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 |
Enums
DatatypeAccessor | |
SatResult | Result of a satisfiability query. |
Symbol | Symbols are used to name several term and type constructors. |