Z3
Data Structures
Here are the data structures with brief descriptions:
AlgebraicNum
AlgebraicNumRef
apply_result
ApplyResultApplyResult 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
ArithSortRefArithmetic
array< T >
ArrayExpr
ArrayRef
ArraySort
ArraySortRefArrays
ast
ASTThe abstract syntax tree (AST) class
AST
ast_vector_tpl< T >
ASTDecRefQueue
AstMap
ASTMapMap from AST to AST
ASTMap
ASTMapDecRefQueue
AstRef
AstVector
ASTVector
ASTVectorVectors of ASTs
ASTVectorDecRefQueue
BitVecExpr
BitVecNum
BitVecNumRef
BitVecRef
BitVecSort
BitVecSortRefBit-Vectors
BoolExpr
BoolExpr
BoolRef
BoolSort
BoolSortRefBooleans
cast_ast< ast >
cast_ast< expr >
cast_ast< func_decl >
cast_ast< sort >
CheckSatResult
configZ3 global configuration object
ConstructorConstructors are used for datatype sorts
Constructor
ConstructorList
Context
Context
ContextThe main interaction with Z3 happens via the Context
contextA Context manages all other Z3 objects, global configuration options, etc
Datatype
DatatypeExpr
DatatypeRef
DatatypeSort
DatatypeSortRef
Statistics.EntryStatistical data is organized into pairs of [Key, Entry], where every Entry is either a DoubleEntry or a UIntEntry
FuncInterp.Entry
Statistics.Entry
FuncInterp.EntryAn Entry object represents an element in the finite map used to encode a function interpretation
EnumSort
Exception
exceptionException used to sign API usage errors
exprA 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
ExprExpressions are terms
ExprRefExpressions
FiniteDomainSort
Fixedpoint
FixedpointFixedpoint
FixedpointDecRefQueue
func_declFunction 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
FuncDeclFunction declarations
FuncDeclRefFunction Declarations
FuncEntry
FuncInterp
FuncInterp
FuncInterpA 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
GoalA 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
InterpolationContextThe InterpolationContext is suitable for generation of interpolants
IntExpr
IntNum
IntNumRef
IntSort
IntSymbol
Native.LIB
ListSort
Log
model
Model
ModelA Model contains interpretations (assignments) of constants and functions
ModelDecRefQueue
Model.ModelEvaluationFailedExceptionA ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model
Model.ModelEvaluationFailedException
ModelRef
Native
object
ParamDescrs
ParamDescrsDecRefQueue
ParamDescrsRef
FuncDecl.Parameter
FuncDecl.ParameterFunction declarations can have Parameters associated with them
params
ParamsA ParameterSet represents a configuration in the form of Symbol/value pairs
Params
ParamsDecRefQueue
ParamsRefParameter Sets
Pattern
PatternPatterns 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
PatternRefPatterns
Probe
Probe
probe
ProbeProbes 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
QuantifierQuantifier expressions
QuantifierRefQuantifiers
RatNum
RatNumRef
RealExpr
RealSort
RelationSort
ScopedConstructor
ScopedConstructorList
SetSort
Solver
SolverSolvers
solver
Solver
SolverDecRefQueue
sortA Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort
Sort
SortImplements type information for ASTs
SortRef
StatisticsStatistics
Statistics
StatisticsObjects of this class track statistical information about solvers
StatisticsDecRefQueue
stats
Status
StringSymbol
symbol
Symbol
SymbolSymbols are used to name several term and type constructors
tactic
Tactic
Tactic
TacticTactics 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
Z3ExceptionThe exception base class for error reporting from Z3
Z3Object
Z3ObjectInternal base class for interfacing with native Z3 objects. Should not be used externally
Z3PPObjectASTs base class
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines