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. |