| Carray< T > | |
| CAstMap | |
| 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 | |
| ►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. |
| Cexception | Exception used to sign API usage errors |
| CFuncEntry | |
| CGlobal | |
| ►CIComparable | |
| ►CAST | The abstract syntax tree (AST) class. |
| ►CExpr | Expressions are terms. |
| ►CArithExpr | Arithmetic expressions (int/real) |
| CAlgebraicNum | Algebraic numbers |
| ►CIntExpr | Int expressions |
| CIntNum | Integer Numerals |
| ►CRealExpr | Real expressions |
| CRatNum | Rational Numerals |
| CArrayExpr | Array expressions |
| ►CBitVecExpr | Bit-vector expressions |
| CBitVecNum | Bit-vector numerals |
| ►CBoolExpr | Boolean expressions |
| CQuantifier | Quantifier expressions. |
| CDatatypeExpr | Datatype expressions |
| ►CFPExpr | FloatingPoint Expressions |
| CFPNum | FloatiungPoint Numerals |
| ►CFPRMExpr | FloatingPoint RoundingMode Expressions |
| CFPRMNum | Floating-point rounding mode numerals |
| 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. |
| ►CArithSort | An arithmetic sort, i.e., Int or Real. |
| CIntSort | An Integer sort |
| CRealSort | A real sort |
| CArraySort | Array sorts. |
| CBitVecSort | Bit-vector sorts. |
| CBoolSort | A Boolean sort. |
| CDatatypeSort | Datatype sorts. |
| CEnumSort | Enumeration sorts. |
| CFiniteDomainSort | Finite domain sorts. |
| CFPRMSort | The FloatingPoint RoundingMode sort |
| CFPSort | FloatingPoint sort |
| CListSort | List sorts. |
| CRelationSort | Relation sorts. |
| CSetSort | Set sorts. |
| CTupleSort | Tuple sorts. |
| CUninterpretedSort | Uninterpreted Sorts |
| ►CIDecRefQueue | DecRefQueue interface |
| CDecRefQueueContracts | |
| CIDecRefQueue | |
| ►CIDisposable | |
| ►CContext | |
| CInterpolationContext | |
| ►CZ3Object | |
| CApplyResult | |
| ►CAST | |
| ►CExpr | |
| ►CArithExpr | |
| CAlgebraicNum | |
| ►CIntExpr | |
| CIntNum | |
| ►CRealExpr | |
| CRatNum | |
| CArrayExpr | |
| ►CBitVecExpr | |
| CBitVecNum | |
| ►CBoolExpr | |
| CQuantifier | |
| CDatatypeExpr | |
| ►CFPExpr | |
| CFPNum | |
| ►CFPRMExpr | |
| CFPRMNum | |
| CFuncDecl | |
| CPattern | |
| ►CSort | |
| ►CArithSort | |
| CIntSort | |
| CRealSort | |
| CArraySort | |
| CBitVecSort | |
| CBoolSort | |
| CDatatypeSort | |
| CEnumSort | |
| CFiniteDomainSort | |
| CFPRMSort | |
| CFPSort | |
| CListSort | |
| CRelationSort | |
| CSetSort | |
| CTupleSort | |
| CUninterpretedSort | |
| CASTVector | |
| CConstructor | |
| CConstructorList | |
| CFixedpoint | |
| CFuncInterp | |
| CFuncInterp.Entry | |
| CGoal | |
| CModel | |
| CParamDescrs | |
| CParams | |
| CProbe | |
| CSolver | |
| CStatistics | |
| ►CSymbol | |
| CIntSymbol | |
| CStringSymbol | |
| CTactic | |
| ►CIDisposable | |
| ►CContext | The main interaction with Z3 happens via the Context. |
| CInterpolationContext | The InterpolationContext is suitable for generation of interpolants. |
| ►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. |
| CASTVector | Vectors of ASTs. |
| CConstructor | Constructors are used for datatype sorts. |
| CConstructorList | Lists of constructors |
| CFixedpoint | Object for managing fixedpoints |
| 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. |
| CParamDescrs | A ParamDescrs describes a set of parameters. |
| CParams | A Params objects 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. |
| CIntSymbol | Numbered symbols |
| CStringSymbol | Named symbols |
| 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. |
| 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 | |
| ►CRuntimeException | |
| ►CZ3Exception | |
| CModel.ModelEvaluationFailedException | |
| 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 | |
| ►CFPRef | FP Expressions |
| CFPNumRef | FP Numerals |
| CFPRMRef | |
| CPatternRef | Patterns |
| CFuncDeclRef | Function Declarations |
| ►CSortRef | |
| CArithSortRef | Arithmetic |
| CArraySortRef | Arrays |
| CBitVecSortRef | Bit-Vectors |
| CBoolSortRef | Booleans |
| CDatatypeSortRef | |
| CFPRMSortRef | |
| CFPSortRef | FP Sorts |
| CAstVector | |
| CFixedpoint | Fixedpoint |
| CFuncInterp | |
| CGoal | |
| CModelRef | |
| CSolver | |
| CBigInteger | |
| Cboolean | |
| CCollections | |
| CCollections | |
| CCompilerServices | |
| 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 | |
| CContracts | |
| CContracts | |
| CContracts | |
| CContracts | |
| CContracts | |
| CContracts | |
| CContracts | |
| CContracts | |
| CContracts | |
| CContracts | |
| CContracts | |
| CContracts | |
| CContracts | |
| CContracts | |
| CContracts | |
| CContracts | |
| 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 | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| Cint | |
| CInteropServices | |
| CInteropServices | |
| CInteropServices | |
| CInteropServices | |
| CInteropServices | |
| CInteropServices | |
| CInteropServices | |
| CInteropServices | |
| CInteropServices | |
| CInteropServices | |
| CIntPtr | |
| Cio | |
| CLinkedList | |
| CLinq | |
| CLinq | |
| CLinq | |
| CLinq | |
| CLinq | |
| CLinq | |
| CLinq | |
| CLinq | |
| CLinq | |
| CLinq | |
| CLinq | |
| CLinq | |
| Clong | |
| CMap | |
| CNumerics | |
| CNumerics | |
| CNumerics | |
| CNumerics | |
| CObject | |
| CPermissions | |
| Creadonly bool | |
| Creadonly List< IntPtr > | |
| Creadonly Object | |
| Creadonly string | |
| Creadonly uint | |
| Creadonly Z3_parameter_kind | |
| CReflection | |
| Cstatic bool | |
| CString | |
| Cstring | |
| Csys | |
| CSystem | |
| CT * | |
| CText | |
| CText | |
| CText | |
| CText | |
| CText | |
| CText | |
| CText | |
| CText | |
| CText | |
| CText | |
| CText | |
| CText | |
| CText | |
| CThreading | |
| 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 | |
1.8.9.1