Z3
Data Structures
Here are the data structures with brief descriptions:
[detail level 12345]
 Ncom
 Nmicrosoft
 Nz3
 NMicrosoft
 NZ3
 CApplyResultApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced.
 CASTThe abstract syntax tree (AST) class.
 CConstructorConstructors are used for datatype sorts.
 CContextThe main interaction with Z3 happens via the Context.
 CExprExpressions are terms.
 CFuncDeclFunction declarations.
 CFuncInterpA function interpretation is represented as a finite map and an 'else' value. Each entry in the finite map represents the value of a function given a set of arguments.
 CGoalA goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers.
 CModelA Model contains interpretations (assignments) of constants and functions.
 CNative
 CParamsA ParameterSet represents a configuration in the form of Symbol/value pairs.
 CPatternPatterns comprise a list of terms. The list should be non-empty. If the list comprises of more than one term, it is also called a multi-pattern.
 CProbeProbes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used. The complete list of probes may be obtained using the procedures Context.NumProbes and Context.ProbeNames. It may also be obtained using the command (help-tactics) in the SMT 2.0 front-end.
 CQuantifierQuantifier expressions.
 CSolverSolvers.
 CSortThe Sort class implements type information for ASTs.
 CStatisticsObjects of this class track statistical information about solvers.
 CSymbolSymbols are used to name several term and type constructors.
 CTacticTactics are the basic building block for creating custom solvers for specific problem domains. The complete list of tactics may be obtained using Context.NumTactics and Context.TacticNames. It may also be obtained using the command (help-tactics) in the SMT 2.0 front-end.
 CZ3ExceptionThe exception base class for error reporting from Z3
 CZ3ObjectInternal base class for interfacing with native Z3 objects. Should not be used externally.
 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
 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
 CFixedpointFixedpoint
 CFuncDeclRefFunction Declarations
 CFuncEntry
 CFuncInterp
 CGoal
 CIntNumRef
 CModelRef
 CParamDescrsRef
 CParamsRefParameter Sets
 CPatternRefPatterns
 CProbe
 CQuantifierRefQuantifiers
 CRatNumRef
 CScopedConstructor
 CScopedConstructorList
 CSolver
 CSortRef
 CStatisticsStatistics
 CTactic
 CZ3PPObjectASTs base class
 CBoolExpr
 CException
 CIComparable
 CIDecRefQueue
 CIDisposable