Z3
Class Hierarchy

Go to the graphical class hierarchy

This inheritance list is sorted roughly, but not completely, alphabetically:
[detail level 123456]
 CArithExpr< IntSort >
 CArithExpr< RealSort >
 Carray< T >
 CArrayExpr< Sort, R >
 CArraySort< D, BoolSort >
 CAstMap
 CAutoCloseable
 Ccast_ast< T >
 Ccast_ast< ast >
 Ccast_ast< expr >
 Ccast_ast< func_decl >
 Ccast_ast< sort >
 CCheckSatResult
 CComparable
 CconfigZ3 global configuration object
 CcontextA Context manages all other Z3 objects, global configuration options, etc
 CContext
 Csolver::cube_generator
 Csolver::cube_iterator
 CDatatype
 CDeprecatedThe main interaction with Z3 happens via the Context.
 CStatistics.Entry
 CStatistics.EntryStatistical data is organized into pairs of [Key, Entry], where every Entry is either a DoubleEntry or a UIntEntry
 CException
 Cexception
 CExpr< ArraySort< D, R > >
 CExpr< BitVecSort >
 CExpr< BoolSort >
 CExpr< DatatypeSort< R > >
 CExpr< FiniteDomainSort< R > >
 CExpr< FPRMSort >
 CExpr< FPSort >
 CExpr< R >
 CExpr< ReSort< R > >
 CExpr< SeqSort< R > >
 CFuncDecl<?>
 CFuncEntry
 CGlobal
 COptimize.HandleHandle to objectives returned by objective functions.
 Coptimize::handle
 CIComparable
 CIDecRefQueue< T extends Z3Object >
 CIDecRefQueueDecRefQueue interface
 CIDecRefQueue< ApplyResult >
 CIDecRefQueue< AST >
 CIDecRefQueue< ASTMap >
 CIDecRefQueue< ASTVector >
 CIDecRefQueue< Constructor<?> >
 CIDecRefQueue< ConstructorList<?> >
 CIDecRefQueue< Fixedpoint >
 CIDecRefQueue< FuncInterp.Entry<?> >
 CIDecRefQueue< FuncInterp<?> >
 CIDecRefQueue< Goal >
 CIDecRefQueue< Model >
 CIDecRefQueue< Optimize >
 CIDecRefQueue< ParamDescrs >
 CIDecRefQueue< Params >
 CIDecRefQueue< Probe >
 CIDecRefQueue< Solver >
 CIDecRefQueue< Statistics >
 CIDecRefQueue< Tactic >
 CIDisposable
 Cast_vector_tpl< T >::iterator
 CLog
 Cobject
 COptimizeObjectiveOptimize
 CParamDescrsRef
 CFuncDecl.ParameterFunction declarations can have Parameters associated with them.
 CParamsRefParameter Sets
 CProbe
 CPropClosures
 CRuntimeException
 Cscoped_context
 CScopedConstructor
 CScopedConstructorList
 CSeqSort< com.microsoft.z3.BitVecSort >
 Csolver::simple
 CStatisticsStatistics
 CStatus
 CTactic
 Cmodel::translate
 Csolver::translate
 Cuser_propagator_base
 CUserPropagateBase
 CVersion
 CZ3Object
 CZ3PPObjectASTs base class