AlgebraicNum | |
AlgebraicNumRef | |
apply_result | |
ApplyResult | ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced |
ApplyResult | |
ApplyResult | |
ApplyResultDecRefQueue | |
ArithExpr | |
ArithRef | |
ArithSort | |
ArithSortRef | Arithmetic |
array< T > | |
ArrayExpr | |
ArrayRef | |
ArraySort | |
ArraySortRef | Arrays |
ast | |
AST | The abstract syntax tree (AST) class |
AST | |
ast_vector_tpl< T > | |
ASTDecRefQueue | |
AstMap | |
ASTMap | Map from AST to AST |
ASTMap | |
ASTMapDecRefQueue | |
AstRef | |
AstVector | |
ASTVector | |
ASTVector | Vectors of ASTs |
ASTVectorDecRefQueue | |
BitVecExpr | |
BitVecNum | |
BitVecNumRef | |
BitVecRef | |
BitVecSort | |
BitVecSortRef | Bit-Vectors |
BoolExpr | |
BoolExpr | |
BoolRef | |
BoolSort | |
BoolSortRef | Booleans |
cast_ast< ast > | |
cast_ast< expr > | |
cast_ast< func_decl > | |
cast_ast< sort > | |
CheckSatResult | |
config | Z3 global configuration object |
Constructor | Constructors are used for datatype sorts |
Constructor | |
ConstructorList | |
Context | |
Context | |
Context | The main interaction with Z3 happens via the Context |
context | A Context manages all other Z3 objects, global configuration options, etc |
Datatype | |
DatatypeExpr | |
DatatypeRef | |
DatatypeSort | |
DatatypeSortRef | |
Statistics.Entry | Statistical data is organized into pairs of [Key, Entry], where every Entry is either a DoubleEntry or a UIntEntry |
FuncInterp.Entry | |
Statistics.Entry | |
FuncInterp.Entry | An Entry object represents an element in the finite map used to encode a function interpretation |
EnumSort | |
Exception | |
exception | Exception used to sign API usage errors |
expr | A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort Boolean. Every expression has a sort |
Expr | |
Expr | Expressions are terms |
ExprRef | Expressions |
FiniteDomainSort | |
Fixedpoint | |
Fixedpoint | Fixedpoint |
FixedpointDecRefQueue | |
func_decl | Function declaration (aka function definition). It is the signature of interpreted and uninterpreted functions in Z3. The basic building block in Z3 is the function application |
func_entry | |
func_interp | |
FuncDecl | |
FuncDecl | Function declarations |
FuncDeclRef | Function Declarations |
FuncEntry | |
FuncInterp | |
FuncInterp | |
FuncInterp | A function interpretation is represented as a finite map and an 'else' value. Each entry in the finite map represents the value of a function given a set of arguments |
FuncInterpDecRefQueue | |
FuncInterpEntryDecRefQueue | |
Global | |
Goal | A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers |
goal | |
Goal | |
Goal | |
GoalDecRefQueue | |
IComparable | |
IDecRefQueue | |
IDecRefQueue | |
IDisposable | |
IDisposable | |
InterpolationContext | The InterpolationContext is suitable for generation of interpolants |
IntExpr | |
IntNum | |
IntNumRef | |
IntSort | |
IntSymbol | |
Native.LIB | |
ListSort | |
Log | |
model | |
Model | |
Model | A Model contains interpretations (assignments) of constants and functions |
ModelDecRefQueue | |
Model.ModelEvaluationFailedException | A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model |
Model.ModelEvaluationFailedException | |
ModelRef | |
Native | |
object | |
ParamDescrs | |
ParamDescrsDecRefQueue | |
ParamDescrsRef | |
FuncDecl.Parameter | |
FuncDecl.Parameter | Function declarations can have Parameters associated with them |
params | |
Params | A ParameterSet represents a configuration in the form of Symbol/value pairs |
Params | |
ParamsDecRefQueue | |
ParamsRef | Parameter Sets |
Pattern | |
Pattern | Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than one term, it is also called a multi-pattern |
PatternRef | Patterns |
Probe | |
Probe | |
probe | |
Probe | Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used. The complete list of probes may be obtained using the procedures Context.NumProbes and Context.ProbeNames . It may also be obtained using the command (help-tactics) in the SMT 2.0 front-end |
ProbeDecRefQueue | |
Quantifier | |
Quantifier | Quantifier expressions |
QuantifierRef | Quantifiers |
RatNum | |
RatNumRef | |
RealExpr | |
RealSort | |
RelationSort | |
ScopedConstructor | |
ScopedConstructorList | |
SetSort | |
Solver | |
Solver | Solvers |
solver | |
Solver | |
SolverDecRefQueue | |
sort | A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort |
Sort | |
Sort | Implements type information for ASTs |
SortRef | |
Statistics | Statistics |
Statistics | |
Statistics | Objects of this class track statistical information about solvers |
StatisticsDecRefQueue | |
stats | |
Status | |
StringSymbol | |
symbol | |
Symbol | |
Symbol | Symbols are used to name several term and type constructors |
tactic | |
Tactic | |
Tactic | |
Tactic | Tactics are the basic building block for creating custom solvers for specific problem domains. The complete list of tactics may be obtained using Context.NumTactics and Context.TacticNames . It may also be obtained using the command (help-tactics) in the SMT 2.0 front-end |
TacticDecRefQueue | |
TupleSort | |
UninterpretedSort | |
Version | |
Z3Exception | |
Z3Exception | The exception base class for error reporting from Z3 |
Z3Object | |
Z3Object | Internal base class for interfacing with native Z3 objects. Should not be used externally |
Z3PPObject | ASTs base class |