Z3
 
Loading...
Searching...
No Matches
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
 CconfigZ3 global configuration object
 Cconstructor_list
 Cconstructors
 CContext
 CcontextA Context manages all other Z3 objects, global configuration options, etc
 Csolver::cube_generator
 Csolver::cube_iterator
 CDatatype
 Cexception
 CexceptionException used to sign API usage errors
 CFuncEntry
 Coptimize::handle
 Cast_vector_tpl< T >::iterator
 Cexpr::iterator
 Cobject
 Cast_vector_tpl< expr >
 Capply_result
 Cast
 CexprA 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_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
 CsortA 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
 Csimplifier
 Csolver
 Cstats
 Csymbol
 Ctactic
 Con_clause
 COnClause
 COptimizeObjectiveOptimize
 CParamDescrsRef
 CparameterClass for auxiliary parameters associated with func_decl The class is initialized with a func_decl or application expression and an index The accessor get_expr, get_sort, ... is available depending on the value of kind(). The caller is responsible to check that the kind of the parameter aligns with the call (get_expr etc)
 CParamsRefParameter Sets
 CParserContext
 CProbe
 CPropClosures
 CScopedConstructor
 CScopedConstructorList
 Csolver::simple
 CSimplifier
 CStatisticsStatistics
 CTactic
 Cmodel::translate
 Csolver::translate
 Cuser_propagator_base
 CUserPropagateBase
 CZ3PPObjectASTs base class
 CApplyResult
 CAstRef
 CExprRefExpressions
 CArithRef
 CArrayRef
 CBitVecRef
 CBoolRef
 CCharRef
 CDatatypeRef
 CFPRMRef
 CFPRef
 CFiniteDomainRef
 CPatternRefPatterns
 CReRef
 CSeqRef
 CFuncDeclRefFunction Declarations
 CSortRef
 CArithSortRefArithmetic
 CArraySortRefArrays
 CBitVecSortRefBit-Vectors
 CBoolSortRefBooleans
 CCharSortRef
 CDatatypeSortRef
 CFPRMSortRef
 CFPSortRef
 CFiniteDomainSortRef
 CReSortRef
 CSeqSortRefStrings, Sequences and Regular expressions
 CTypeVarRef
 CAstVector
 CFixedpointFixedpoint
 CFuncInterp
 CGoal
 CModelRef
 COptimize
 CSolver