Index of modules


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.