Z3
Data Structures
Here are the data structures with brief descriptions:
[detail level 123]
 Nz3Z3 C++ namespace
 Ccast_ast
 Cast_vector_tpl
 Citerator
 CexceptionException used to sign API usage errors
 CconfigZ3 global configuration object
 CcontextA Context manages all other Z3 objects, global configuration options, etc
 Cscoped_context
 Carray
 Cobject
 Csymbol
 Cparam_descrs
 Cparams
 Cast
 CsortA Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 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
 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
 Ccast_ast< ast >
 Ccast_ast< expr >
 Ccast_ast< sort >
 Ccast_ast< func_decl >
 Cfunc_entry
 Cfunc_interp
 Cmodel
 Ctranslate
 Cstats
 Csolver
 Ccube_generator
 Ccube_iterator
 Csimple
 Ctranslate
 Cgoal
 Capply_result
 Ctactic
 Cprobe
 Coptimize
 Chandle
 Cfixedpoint
 Cuser_propagator_base
 Nz3py
 CContext
 CZ3PPObjectASTs base class
 CAstRef
 CSortRef
 CFuncDeclRefFunction Declarations
 CExprRefExpressions
 CBoolSortRefBooleans
 CBoolRef
 CPatternRefPatterns
 CQuantifierRefQuantifiers
 CArithSortRefArithmetic
 CArithRef
 CIntNumRef
 CRatNumRef
 CAlgebraicNumRef
 CBitVecSortRefBit-Vectors
 CBitVecRef
 CBitVecNumRef
 CArraySortRefArrays
 CArrayRef
 CDatatype
 CScopedConstructor
 CScopedConstructorList
 CDatatypeSortRef
 CDatatypeRef
 CParamsRefParameter Sets
 CParamDescrsRef
 CGoal
 CAstVector
 CAstMap
 CFuncEntry
 CFuncInterp
 CModelRef
 CStatisticsStatistics
 CCheckSatResult
 CSolver
 CFixedpointFixedpoint
 CFiniteDomainSortRef
 CFiniteDomainRef
 CFiniteDomainNumRef
 COptimizeObjectiveOptimize
 COptimize
 CApplyResult
 CTactic
 CProbe
 CFPSortRef
 CFPRMSortRef
 CFPRef
 CFPRMRef
 CFPNumRef
 CSeqSortRefStrings, Sequences and Regular expressions
 CSeqRef
 CReSortRef
 CReRef
 CPropClosures
 CUserPropagateBase