Class Hierarchy

Go to the graphical class hierarchy

This inheritance list is sorted roughly, but not completely, alphabetically:

[detail level 12345]

Carray< T >
CAstMap
Ccast_ast< T >
Ccast_ast< ast >
Ccast_ast< expr >
Ccast_ast< func_decl >
Ccast_ast< sort >
CCheckSatResult
Cconfig	Z3 global configuration object
CContext
Ccontext	A Context manages all other Z3 objects, global configuration options, etc
Csolver::cube_generator
Csolver::cube_iterator
CDatatype
▼Cexception
Cexception	Exception used to sign API usage errors
CFuncEntry
Coptimize::handle
Cast_vector_tpl< T >::iterator
Cexpr::iterator
▼Cobject
Cast_vector_tpl< expr >
Capply_result
►Cast
Cexpr	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
Cfunc_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
Csort	A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort
Cast_vector_tpl< T >
Cfixedpoint
Cfunc_entry
Cfunc_interp
Cgoal
Cmodel
Coptimize
Cparam_descrs
Cparams
Cprobe
Csolver
Cstats
Csymbol
Ctactic
COptimizeObjective	Optimize
CParamDescrsRef
CParamsRef	Parameter Sets
CProbe
CPropClosures
Cscoped_context
CScopedConstructor
CScopedConstructorList
Csolver::simple
CStatistics	Statistics
CTactic
Cmodel::translate
Csolver::translate
Cuser_propagator_base
CUserPropagateBase
▼CZ3PPObject	ASTs base class
CApplyResult
►CAstRef
►CExprRef	Expressions
►CArithRef
CAlgebraicNumRef
CIntNumRef
CRatNumRef
CArrayRef
►CBitVecRef
CBitVecNumRef
►CBoolRef
CQuantifierRef	Quantifiers
CDatatypeRef
►CFiniteDomainRef
CFiniteDomainNumRef
►CFPRef
CFPNumRef
CFPRMRef
CPatternRef	Patterns
CReRef
CSeqRef
CFuncDeclRef	Function Declarations
►CSortRef
CArithSortRef	Arithmetic
CArraySortRef	Arrays
CBitVecSortRef	Bit-Vectors
CBoolSortRef	Booleans
CCharSortRef
CDatatypeSortRef
CFiniteDomainSortRef
CFPRMSortRef
CFPSortRef
CReSortRef
CSeqSortRef	Strings, Sequences and Regular expressions
CAstVector
CFixedpoint	Fixedpoint
CFuncInterp
CGoal
CModelRef
COptimize
CSolver
Cbool
Ccopy
CFraction
Cfunction< void(unsigned, expr const &)>
Cfunction< void(unsigned, unsigned)>
Cfunction< void(void)>
Cio
CIterable
Cmath
Crounding_mode
Cstring
Csys
Cunique_ptr< T[]>
Cunsigned
CZ3_apply_result
CZ3_ast
CZ3_ast_vector
CZ3_config
CZ3_context
CZ3_fixedpoint
CZ3_func_entry
CZ3_func_interp
CZ3_goal
CZ3_model
CZ3_optimize
CZ3_param_descrs
CZ3_params
CZ3_probe
CZ3_solver
CZ3_solver_callback
CZ3_stats
CZ3_symbol
CZ3_tactic
Cz3core