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 |