Data Structures

Here are the data structures with brief descriptions:

[detail level 123]

Nz3	Z3 C++ namespace
Ccast_ast
Cast_vector_tpl
Citerator
Cexception	Exception used to sign API usage errors
Cconfig	Z3 global configuration object
Ccontext	A Context manages all other Z3 objects, global configuration options, etc
Carray
Cobject
Csymbol
Cparam_descrs
Cparams
Cast
Cast_map	A map from ASTs to ASTs
Csort	A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 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
Cparser_context
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
Citerator
Ccast_ast< ast >
Ccast_ast< expr >
Ccast_ast< sort >
Ccast_ast< func_decl >
Cfunc_entry
Cfunc_interp
Cmodel
Ctranslate
Cstats
Cparameter	Class 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)
Csolver
Csimple
Ctranslate
Ccube_iterator
Ccube_generator
Cgoal
Capply_result
Ctactic
Csimplifier
Cprobe
Coptimize
Ctranslate
Chandle
Cfixedpoint
Cconstructor_list
Cconstructors
Con_clause
Cuser_propagator_base
Crcf_num	Wrapper for Z3 Real Closed Field (RCF) numerals
Nz3py
CContext
CZ3PPObject	ASTs base class
CAstRef
CSortRef
CTypeVarRef
CFuncDeclRef	Function Declarations
CExprRef	Expressions
CBoolSortRef	Booleans
CBoolRef
CPatternRef	Patterns
CQuantifierRef	Quantifiers
CArithSortRef	Arithmetic
CArithRef
CIntNumRef
CRatNumRef
CAlgebraicNumRef
CBitVecSortRef	Bit-Vectors
CBitVecRef
CBitVecNumRef
CArraySortRef	Arrays
CArrayRef
CFiniteSetSortRef	Finite Sets
CFiniteSetRef
CDatatype
CScopedConstructor
CScopedConstructorList
CDatatypeSortRef
CDatatypeRef
CParamsRef	Parameter Sets
CParamDescrsRef
CGoal
CAstVector
CAstMap
CFuncEntry
CFuncInterp
CModelRef
CStatistics	Statistics
CCheckSatResult
CSolver
CFixedpoint	Fixedpoint
CFiniteDomainSortRef
CFiniteDomainRef
CFiniteDomainNumRef
COptimizeObjective	Optimize
COptimize
CApplyResult
CSimplifier
CTactic
CProbe
CParserContext
CFPSortRef
CFPRMSortRef
CFPRef
CFPRMRef
CFPNumRef
CSeqSortRef	Strings, Sequences and Regular expressions
CCharSortRef
CSeqRef
CCharRef
CReSortRef
CReRef
COnClause
CPropClosures
CUserPropagateBase