Z3
Class Hierarchy
Go to the graphical class hierarchy
This inheritance list is sorted roughly, but not completely, alphabetically:
[detail level
1
2
3
4
5
6
]
C
array< T >
C
AstMap
►
C
AutoCloseable
C
Context
C
cast_ast< T >
C
cast_ast< ast >
C
cast_ast< expr >
C
cast_ast< func_decl >
C
cast_ast< sort >
C
CheckSatResult
►
C
Comparable
►
C
AST
►
C
Expr
►
C
ArithExpr
C
AlgebraicNum
►
C
IntExpr
C
IntNum
►
C
RealExpr
C
RatNum
►
C
ArrayExpr
C
Lambda
►
C
BitVecExpr
C
BitVecNum
►
C
BoolExpr
C
Quantifier
C
DatatypeExpr
►
C
FPExpr
C
FPNum
►
C
FPRMExpr
C
FPRMNum
►
C
FiniteDomainExpr
C
FiniteDomainNum
C
ReExpr
C
SeqExpr
C
FuncDecl
C
Pattern
►
C
Sort
►
C
ArithSort
C
IntSort
C
RealSort
C
ArraySort
C
BitVecSort
C
BoolSort
C
DatatypeSort
C
EnumSort
C
FPRMSort
C
FPSort
C
FiniteDomainSort
C
ListSort
C
ReSort
C
RelationSort
C
SeqSort
C
SetSort
C
TupleSort
C
UninterpretedSort
C
config
Z3 global configuration object
C
context
A Context manages all other Z3 objects, global configuration options, etc
C
Context
C
solver::cube_generator
C
solver::cube_iterator
C
Datatype
C
Statistics.Entry
C
exception
Exception used to sign API usage errors
C
FuncEntry
C
Global
C
optimize::handle
C
IDecRefQueue< T extends Z3Object >
C
IDecRefQueue< ApplyResult >
C
IDecRefQueue< AST >
C
IDecRefQueue< ASTMap >
C
IDecRefQueue< ASTVector >
►
C
IDecRefQueue< Constructor >
C
ConstructorDecRefQueue
►
C
IDecRefQueue< ConstructorList >
C
ConstructorListDecRefQueue
C
IDecRefQueue< Fixedpoint >
C
IDecRefQueue< FuncInterp >
C
IDecRefQueue< FuncInterp.Entry >
C
IDecRefQueue< Goal >
C
IDecRefQueue< Model >
C
IDecRefQueue< Optimize >
C
IDecRefQueue< ParamDescrs >
C
IDecRefQueue< Params >
C
IDecRefQueue< Probe >
C
IDecRefQueue< Solver >
C
IDecRefQueue< Statistics >
C
IDecRefQueue< Tactic >
C
ast_vector_tpl< T >::iterator
C
Log
C
Native
►
C
object
C
ast_vector_tpl< expr >
C
apply_result
►
C
ast
C
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
C
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
C
sort
A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort
C
ast_vector_tpl< T >
C
fixedpoint
C
func_entry
C
func_interp
C
goal
C
model
C
optimize
C
param_descrs
C
params
C
probe
C
solver
C
stats
C
symbol
C
tactic
C
OptimizeObjective
Optimize
C
ParamDescrsRef
C
FuncDecl.Parameter
C
ParamsRef
Parameter Sets
C
Probe
►
C
RuntimeException
►
C
Z3Exception
C
Model.ModelEvaluationFailedException
C
ScopedConstructor
C
ScopedConstructorList
C
solver::simple
C
Statistics
Statistics
C
Status
C
Tactic
C
model::translate
C
solver::translate
C
Version
C
Z3_ast_kind
C
Z3_ast_print_mode
C
Z3_decl_kind
C
Z3_error_code
C
Z3_goal_prec
C
Z3_lbool
C
Z3_param_kind
C
Z3_parameter_kind
C
Z3_sort_kind
C
Z3_symbol_kind
►
C
Z3Object
C
AST
C
ASTVector
C
ApplyResult
C
Constructor
C
ConstructorList
C
Fixedpoint
C
FuncInterp
C
Goal
C
Model
C
Optimize
C
ParamDescrs
C
Params
C
Probe
C
Solver
C
Statistics
►
C
Symbol
C
IntSymbol
C
StringSymbol
C
Tactic
►
C
Z3PPObject
ASTs base class
C
ApplyResult
►
C
AstRef
►
C
ExprRef
Expressions
►
C
ArithRef
C
AlgebraicNumRef
C
IntNumRef
C
RatNumRef
C
ArrayRef
►
C
BitVecRef
C
BitVecNumRef
►
C
BoolRef
C
QuantifierRef
Quantifiers
C
DatatypeRef
C
FPRMRef
►
C
FPRef
FP Expressions
C
FPNumRef
FP Numerals
►
C
FiniteDomainRef
C
FiniteDomainNumRef
C
PatternRef
Patterns
C
ReRef
C
SeqRef
C
FuncDeclRef
Function Declarations
►
C
SortRef
C
ArithSortRef
Arithmetic
C
ArraySortRef
Arrays
C
BitVecSortRef
Bit-Vectors
C
BoolSortRef
Booleans
C
DatatypeSortRef
C
FPRMSortRef
C
FPSortRef
FP Sorts
C
FiniteDomainSortRef
C
ReSortRef
Regular expressions
C
SeqSortRef
Strings, Sequences and Regular expressions
C
AstVector
C
Fixedpoint
Fixedpoint
C
FuncInterp
C
Goal
C
ModelRef
C
Optimize
C
Solver
Generated on Tue Apr 26 2022 04:28:26 for Z3 by
1.9.3