Class Hierarchy

Go to the graphical class hierarchy

This inheritance list is sorted roughly, but not completely, alphabetically:

[detail level 1234567]

Carray< T >
CAstMap
►CBoolExpr
CQuantifier	Quantifier expressions.
Ccast_ast< T >
Ccast_ast< ast >
Ccast_ast< expr >
Ccast_ast< func_decl >
Ccast_ast< sort >
CCheckSatResult
Cconfig	Z3 global configuration object
Ccontext	A Context manages all other Z3 objects, global configuration options, etc
CContext
CDatatype
CStatistics.Entry	Statistical data is organized into pairs of [Key, Entry], where every Entry is either a DoubleEntry or a UIntEntry
CStatistics.Entry
Cexception	Exception used to sign API usage errors
►CException
►CZ3Exception
CModel.ModelEvaluationFailedException
►CZ3Exception	The exception base class for error reporting from Z3
CModel.ModelEvaluationFailedException	A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model.
CFuncEntry
CGlobal
►CIComparable
►CAST	The abstract syntax tree (AST) class.
CExpr	Expressions are terms.
CFuncDecl	Function declarations.
CPattern	Patterns 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.
CSort	The Sort class implements type information for ASTs.
CIDecRefQueue
►CIDisposable
CContext	The main interaction with Z3 happens via the Context.
►CZ3Object	Internal base class for interfacing with native Z3 objects. Should not be used externally.
CApplyResult	ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced.
CAST	The abstract syntax tree (AST) class.
CConstructor	Constructors are used for datatype sorts.
CFuncInterp	A 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.
CFuncInterp.Entry	An Entry object represents an element in the finite map used to encode a function interpretation.
CGoal	A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers.
CModel	A Model contains interpretations (assignments) of constants and functions.
CParams	A ParameterSet represents a configuration in the form of Symbol/value pairs.
CProbe	Probes 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.
CSolver	Solvers.
CStatistics	Objects of this class track statistical information about solvers.
CSymbol	Symbols are used to name several term and type constructors.
CTactic	Tactics 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.
►CIDisposable
►CContext
CInterpolationContext	The InterpolationContext is suitable for generation of interpolants.
►CZ3Object
CApplyResult
►CAST
►CExpr
►CArithExpr
CAlgebraicNum
►CIntExpr
CIntNum
►CRealExpr
CRatNum
CArrayExpr
►CBitVecExpr
CBitVecNum
►CBoolExpr
CQuantifier
CDatatypeExpr
CFuncDecl
CPattern
►CSort
►CArithSort
CIntSort
CRealSort
CArraySort
CBitVecSort
CBoolSort
CDatatypeSort
CEnumSort
CFiniteDomainSort
CListSort
CRelationSort
CSetSort
CTupleSort
CUninterpretedSort
CConstructor
CConstructorList
CFixedpoint
CFuncInterp
CFuncInterp.Entry
CGoal
CModel
CParamDescrs
CParams
CProbe
CSolver
CStatistics
►CSymbol
CIntSymbol
CStringSymbol
CTactic
CNative.LIB
CLinkedList< Long >
CLog
CNative
CNative
►Cobject
Capply_result
►Cast
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
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
Csort	A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort
Cast_vector_tpl< T >
Cfunc_entry
Cfunc_interp
Cgoal
Cmodel
Cparams
Cprobe
Csolver
Cstats
Csymbol
Ctactic
CParamDescrsRef
CFuncDecl.Parameter
CFuncDecl.Parameter	Function declarations can have Parameters associated with them.
CParamsRef	Parameter Sets
CProbe
CScopedConstructor
CScopedConstructorList
CStatistics	Statistics
CStatus
CTactic
CVersion
CZ3_ast_kind
CZ3_ast_print_mode
CZ3_decl_kind
CZ3_error_code
CZ3_goal_prec
CZ3_lbool
CZ3_param_kind
CZ3_parameter_kind
CZ3_sort_kind
CZ3_symbol_kind
►CZ3PPObject	ASTs base class
CApplyResult
►CAstRef
►CExprRef	Expressions
►CArithRef
CAlgebraicNumRef
CIntNumRef
CRatNumRef
CArrayRef
►CBitVecRef
CBitVecNumRef
►CBoolRef
CQuantifierRef	Quantifiers
CDatatypeRef
CPatternRef	Patterns
CFuncDeclRef	Function Declarations
►CSortRef
CArithSortRef	Arithmetic
CArraySortRef	Arrays
CBitVecSortRef	Bit-Vectors
CBoolSortRef	Booleans
CDatatypeSortRef
CAstVector
CFixedpoint	Fixedpoint
CFuncInterp
CGoal
CModelRef
CSolver
CBigInteger
Cboolean
CBoolSort
CCollections
Cconst string
CContracts
CContracts
CContracts
CContracts
CContracts
CContracts
CContracts
CContracts
CContracts
CContracts
CContracts
CContracts
CContracts
CContracts
CContracts
CContracts
CContracts
CContracts
CContracts
CContracts
CContracts
CContracts
CContracts
Cdouble
Cfinal int
CFraction
CGeneric
CGeneric
CGeneric
Cint
CInteropServices
CInteropServices
CInteropServices
CInteropServices
CInteropServices
CIntPtr
CIntSort
Cio
CLinkedList
Clong
CMap
CObject
Creadonly bool
Creadonly Fixedpoint.DecRefQueue
Creadonly ParamDescrs.DecRefQueue
Creadonly string
Creadonly uint
Creadonly Z3_parameter_kind
CRealSort
Cstatic bool
Cstring
CString
Csys
CSystem
CT *
CText
CThreading
Cuint
Cunsigned
CZ3_apply_result
CZ3_ast
CZ3_ast_vector
CZ3_config
CZ3_context
CZ3_func_entry
CZ3_func_interp
CZ3_goal
CZ3_model
CZ3_params
CZ3_probe
CZ3_solver
CZ3_stats
CZ3_symbol
CZ3_tactic