Z3
Data Structures
Here are the data structures with brief descriptions:
[detail level 12345]
 Ncom
 Nmicrosoft
 NMicrosoft
 NZ3
 NSystem
 NDiagnostics
 Nz3Z3 C++ namespace
 Capply_result
 Carray
 Cast
 Cast_vector_tpl
 Ccast_ast
 Ccast_ast< ast >
 Ccast_ast< expr >
 Ccast_ast< func_decl >
 Ccast_ast< sort >
 CconfigZ3 global configuration object
 CcontextA Context manages all other Z3 objects, global configuration options, etc
 CexceptionException used to sign API usage errors
 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
 Cfunc_entry
 Cfunc_interp
 Cgoal
 Cmodel
 Cobject
 Coptimize
 Cparam_descrs
 Cparams
 Cprobe
 Csolver
 CsortA Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort
 Cstats
 Csymbol
 Ctactic
 Nz3py
 CAlgebraicNumRef
 CApplyResult
 CArithRef
 CArithSortRefArithmetic
 CArrayRef
 CArraySortRefArrays
 CAstMap
 CAstRef
 CAstVector
 CBitVecNumRef
 CBitVecRef
 CBitVecSortRefBit-Vectors
 CBoolRef
 CBoolSortRefBooleans
 CCheckSatResult
 CContext
 CDatatype
 CDatatypeRef
 CDatatypeSortRef
 CExprRefExpressions
 CFiniteDomainNumRef
 CFiniteDomainRef
 CFiniteDomainSortRef
 CFixedpointFixedpoint
 CFPNumRefFP Numerals
 CFPRefFP Expressions
 CFPRMRef
 CFPRMSortRef
 CFPSortRefFP Sorts
 CFuncDeclRefFunction Declarations
 CFuncEntry
 CFuncInterp
 CGoal
 CIntNumRef
 CModelRef
 COptimize
 COptimizeObjectiveOptimize
 CParamDescrsRef
 CParamsRefParameter Sets
 CPatternRefPatterns
 CProbe
 CQuantifierRefQuantifiers
 CRatNumRef
 CReRef
 CReSortRefRegular expressions
 CScopedConstructor
 CScopedConstructorList
 CSeqRef
 CSeqSortRefStrings, Sequences and Regular expressions
 CSolver
 CSortRef
 CStatisticsStatistics
 CTactic
 CZ3PPObjectASTs base class
 CAttribute
 CAutoCloseable
 CComparable
 CException
 CIComparable
 CIDisposable
 CRuntimeException