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
|
Interpolation [Z3] |
Interpolation
|
L | |
Log [Z3] |
Interaction logging for Z3
Note that this is a global, static log and if multiple Context
objects are created, it logs the interaction with all of them.
|
M | |
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
|
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 |
The enumeration types of Z3.
|