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 | |
| RCF [Z3] |
Real closed field
|
| 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
|
| Simplifier [Z3] | |
| 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 |