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
]
C
array< T >
C
AstMap
C
cast_ast< T >
C
cast_ast< ast >
C
cast_ast< expr >
C
cast_ast< func_decl >
C
cast_ast< sort >
C
CheckSatResult
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
exception
C
exception
Exception used to sign API usage errors
C
FuncEntry
C
optimize::handle
C
ast_vector_tpl< T >::iterator
▼
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
ParamsRef
Parameter Sets
C
Probe
C
PropClosures
C
scoped_context
C
ScopedConstructor
C
ScopedConstructorList
C
solver::simple
C
Statistics
Statistics
C
Tactic
C
model::translate
C
solver::translate
C
user_propagator_base
C
UserPropagateBase
▼
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
C
FPNumRef
▼
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
C
FiniteDomainSortRef
C
ReSortRef
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 Jul 13 2021 00:00:00 for Z3 by
1.9.1