Crate z3[−][src]
Modules
ast | |
datatype_builder |
Structs
ApplyResult | |
Config | Configuration used to initialize logical contexts. |
Context | Manager of all other Z3 objects, global configuration options, etc. |
ContextHandle | Handle that can be used to interrupt a computation from another thread. |
DatatypeBuilder | Build a datatype sort. |
DatatypeSort | |
DatatypeVariant | |
FuncDecl | Function declaration. Every constant and function have an associated declaration. |
Goal | |
IsNotApp | a struct to represent when an ast is not a function application |
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. |
Probe | |
Solver | (Incremental) solver, possibly specialized by a particular tactic or logic. |
Sort | Sorts represent the various ‘types’ of |
SortDiffers | a struct to represent when two sorts are of different types |
Tactic |
Enums
AstKind | The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types. |
DatatypeAccessor | |
DeclKind | The different kinds of interpreted function kinds. |
GoalPrec | A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving and transforming Goals. Some of these transformations apply under/over approximations. |
SatResult | Result of a satisfiability query. |
SortKind | The different kinds of Z3 types (See |
Symbol | Symbols are used to name several term and type constructors. |