A | |
| AST [Z3] | The abstract syntax tree (AST) module |
| ASTMap [Z3.AST] | Map from AST to AST |
| ASTVector [Z3.AST] | Vectors of ASTs |
| AlgebraicNumber [Z3.Arithmetic.Real] | Algebraic Numbers |
| ApplyResult [Z3.Tactic] | Tactic application results |
| Arithmetic [Z3] | Functions to manipulate arithmetic expressions |
B | |
| BitVector [Z3] | Functions to manipulate bit-vector expressions |
| Boolean [Z3] | Boolean expressions; Propositional logic and equality |
C | |
| Constructor [Z3.Datatype] | Datatype Constructors |
D | |
| Datatype [Z3] | Functions to manipulate Datatype expressions |
E | |
| Entry [Z3.Statistics] | Statistical data is organized into pairs of [Key, Entry], where every Entry is either a floating point or integer value. |
| Enumeration [Z3] | Functions to manipulate Enumeration expressions |
| Expr [Z3] | General Expressions (terms) |
F | |
| FiniteDomain [Z3] | Functions to manipulate Finite Domain expressions |
| Fixedpoint [Z3] | Fixedpoint solving |
| FloatingPoint [Z3] | Floating-Point Arithmetic |
| FuncDecl [Z3] | Function declarations |
| FuncEntry [Z3.Model.FuncInterp] | Function interpretations entries |
| FuncInterp [Z3.Model] | Function interpretations |
G | |
| Goal [Z3] | Goals |
I | |
| Integer [Z3.Arithmetic] | Integer Arithmetic |
L | |
| Log [Z3] | Interaction logging for Z3 Interaction logs are used to record calls into the API into a text file. |
M | |
| Memory [Z3] | Memory management * |
| Model [Z3] | Models |
O | |
| Optimize [Z3] | Optimization |
P | |
| ParamDescrs [Z3.Params] | ParamDescrs describe sets of parameters (of Solvers, Tactics, ...) |
| Parameter [Z3.FuncDecl] | Parameters of Func_Decls |
| Params [Z3] | Parameter sets (of Solvers, Tactics, ...) |
| Pattern [Z3.Quantifier] | Quantifier patterns |
| Probe [Z3] | Probes |
| Proof [Z3] | Functions to manipulate proof expressions |
Q | |
| Quantifier [Z3] | Quantifier expressions |
R | |
| Real [Z3.Arithmetic] | Real Arithmetic |
| Relation [Z3] | Functions to manipulate Relation expressions |
| RoundingMode [Z3.FloatingPoint] | Rounding Modes |
S | |
| SMT [Z3] | Functions for handling SMT and SMT2 expressions and files |
| Seq [Z3] | Sequences, Strings and Regular Expressions * |
| Set [Z3] | Functions to manipulate Set expressions |
| Solver [Z3] | Solvers |
| Sort [Z3] | The Sort module implements type information for ASTs |
| Statistics [Z3] | Objects that track statistical information. |
| Symbol [Z3] | Symbols are used to name several term and type constructors |
T | |
| Tactic [Z3] | Tactics |
| Tuple [Z3] | Functions to manipulate Tuple expressions |
V | |
| Version [Z3] | Version information |
Z | |
| Z3 | The Z3 ML/OCaml Interface. |
| Z3Array [Z3] | Functions to manipulate Array expressions |
| Z3List [Z3] | Functions to manipulate List expressions |
| Z3enums |