| Carray< T > | |
| CAstMap | |
| ►CAttribute | |
| CContractClass | |
| CContractClassFor | |
| CContractInvariantMethod | |
| CContractVerification | |
| CPure | |
| ►CAutoCloseable | |
| ►CContext | |
| CInterpolationContext | |
| Ccast_ast< T > | |
| Ccast_ast< ast > | |
| Ccast_ast< expr > | |
| Ccast_ast< func_decl > | |
| Ccast_ast< sort > | |
| CInterpolationContext.CheckInterpolantResult | |
| CCheckSatResult | |
| ►CComparable | |
| ►CAST | |
| ►CExpr | |
| ►CArithExpr | |
| CAlgebraicNum | |
| ►CIntExpr | |
| CIntNum | |
| ►CRealExpr | |
| CRatNum | |
| CArrayExpr | |
| ►CBitVecExpr | |
| CBitVecNum | |
| ►CBoolExpr | |
| CQuantifier | |
| CDatatypeExpr | |
| ►CFiniteDomainExpr | |
| CFiniteDomainNum | |
| ►CFPExpr | |
| CFPNum | |
| ►CFPRMExpr | |
| CFPRMNum | |
| CReExpr | |
| CSeqExpr | |
| CFuncDecl | |
| CPattern | |
| ►CSort | |
| ►CArithSort | |
| CIntSort | |
| CRealSort | |
| CArraySort | |
| CBitVecSort | |
| CBoolSort | |
| CDatatypeSort | |
| CEnumSort | |
| CFiniteDomainSort | |
| CFPRMSort | |
| CFPSort | |
| CListSort | |
| CRelationSort | |
| CReSort | |
| CSeqSort | |
| CSetSort | |
| CTupleSort | |
| CUninterpretedSort | |
| CInterpolationContext.ComputeInterpolantResult | |
| Cconfig | Z3 global configuration object |
| Ccontext | A Context manages all other Z3 objects, global configuration options, etc |
| CContext | |
| CDatatype | |
| CDeprecated | The main interaction with Z3 happens via the Context |
| 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 | |
| COptimize.Handle | |
| Coptimize::handle | |
| COptimize.Handle | Handle to objectives returned by objective functions |
| ►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 |
| ►CFiniteDomainExpr | Finite-domain expressions |
| CFiniteDomainNum | Finite-domain numerals |
| ►CFPExpr | FloatingPoint Expressions |
| CFPNum | FloatiungPoint Numerals |
| ►CFPRMExpr | FloatingPoint RoundingMode Expressions |
| CFPRMNum | Floating-point rounding mode numerals |
| CReExpr | Regular expression expressions |
| CSeqExpr | Sequence expressions |
| 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 |
| CReSort | A regular expression sort |
| CSeqSort | A Sequence sort |
| CSetSort | Set sorts |
| CTupleSort | Tuple sorts |
| CUninterpretedSort | Uninterpreted Sorts |
| CIDecRefQueue< T extends Z3Object > | |
| ►CIDecRefQueue | DecRefQueue interface |
| CDecRefQueueContracts | |
| CIDecRefQueue< ApplyResult > | |
| CIDecRefQueue< AST > | |
| CIDecRefQueue< ASTMap > | |
| CIDecRefQueue< ASTVector > | |
| ►CIDecRefQueue< Constructor > | |
| CConstructorDecRefQueue | |
| ►CIDecRefQueue< ConstructorList > | |
| CConstructorListDecRefQueue | |
| CIDecRefQueue< Fixedpoint > | |
| CIDecRefQueue< FuncInterp > | |
| CIDecRefQueue< FuncInterp.Entry > | |
| CIDecRefQueue< Goal > | |
| CIDecRefQueue< Model > | |
| CIDecRefQueue< Optimize > | |
| CIDecRefQueue< ParamDescrs > | |
| CIDecRefQueue< Params > | |
| CIDecRefQueue< Probe > | |
| CIDecRefQueue< Solver > | |
| CIDecRefQueue< Statistics > | |
| CIDecRefQueue< Tactic > | |
| ►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 |
| CASTMap | Map from AST to AST |
| 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 |
| COptimize | Object for managing optimizization context |
| CParamDescrs | A ParamDescrs describes a set of parameters |
| CParams | A Params objects represents a configuration in the form of Symbol/value pairs |
| CProbe | |
| 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-tactic) in the SMT 2.0 front-end |
| Ccontext::interpolation | |
| CLog | |
| CMap< PhantomReference< T >, Long > | |
| ►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 | |
| Coptimize | |
| Cparam_descrs | |
| Cparams | |
| Cprobe | |
| Csolver | |
| Cstats | |
| Csymbol | |
| Ctactic | |
| COptimizeObjective | Optimize |
| CParamDescrsRef | |
| CFuncDecl.Parameter | Function declarations can have Parameters associated with them |
| CFuncDecl.Parameter | |
| CParamsRef | Parameter Sets |
| CProbe | |
| CInterpolationContext.ReadInterpolationProblemResult | |
| CReferenceQueue< T > | |
| ►CRuntimeException | |
| ►CZ3Exception | |
| CModel.ModelEvaluationFailedException | |
| CScopedConstructor | |
| CScopedConstructorList | |
| Csolver::simple | |
| CStatistics | Statistics |
| CStatus | |
| CTactic | |
| Csolver::translate | |
| CVersion | |
| ►CZ3Object | |
| CApplyResult | |
| CAST | |
| CASTVector | |
| CConstructor | |
| CConstructorList | |
| CFixedpoint | |
| CFuncInterp | |
| CGoal | |
| CModel | |
| COptimize | |
| CParamDescrs | |
| CParams | |
| CProbe | |
| CSolver | |
| CStatistics | |
| ►CSymbol | |
| CIntSymbol | |
| CStringSymbol | |
| CTactic | |
| ►CZ3PPObject | ASTs base class |
| CApplyResult | |
| ►CAstRef | |
| ►CExprRef | Expressions |
| ►CArithRef | |
| CAlgebraicNumRef | |
| CIntNumRef | |
| CRatNumRef | |
| CArrayRef | |
| ►CBitVecRef | |
| CBitVecNumRef | |
| ►CBoolRef | |
| CQuantifierRef | Quantifiers |
| CDatatypeRef | |
| ►CFiniteDomainRef | |
| CFiniteDomainNumRef | |
| ►CFPRef | FP Expressions |
| CFPNumRef | FP Numerals |
| CFPRMRef | |
| CPatternRef | Patterns |
| CReRef | |
| CSeqRef | |
| CFuncDeclRef | Function Declarations |
| ►CSortRef | |
| CArithSortRef | Arithmetic |
| CArraySortRef | Arrays |
| CBitVecSortRef | Bit-Vectors |
| CBoolSortRef | Booleans |
| CDatatypeSortRef | |
| CFiniteDomainSortRef | |
| CFPRMSortRef | |
| CFPSortRef | FP Sorts |
| CReSortRef | Regular expressions |
| CSeqSortRef | Strings, Sequences and Regular expressions |
| CAstVector | |
| CFixedpoint | Fixedpoint |
| CFuncInterp | |
| CGoal | |
| CModelRef | |
| COptimize | |
| CSolver | |
| CBigInteger | |
| Cboolean | |
| CCollections | |
| CCollections | |
| CCompilerServices | |
| 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 | |
| CContracts | |
| CContracts | |
| CContracts | |
| CContracts | |
| CContracts | |
| CContracts | |
| CContracts | |
| CContracts | |
| Cdouble | |
| Cfinal long | |
| CFraction | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CGeneric | |
| CIdentityHashMap | |
| Cint | |
| Cinternal IntPtr | |
| Cinternal long | |
| Cinternal Native.Z3_error_handler | |
| CInteropServices | |
| CInteropServices | |
| CInteropServices | |
| CInteropServices | |
| CInteropServices | |
| CInteropServices | |
| CInteropServices | |
| CInteropServices | |
| CInteropServices | |
| CInteropServices | |
| CIntPtr | |
| Cio | |
| CLinq | |
| CLinq | |
| CLinq | |
| CLinq | |
| CLinq | |
| CLinq | |
| CLinq | |
| CLinq | |
| CLinq | |
| CLinq | |
| CLinq | |
| CLinq | |
| CLinq | |
| CLinq | |
| CLinq | |
| CLinq | |
| CLongPtr | |
| CMap | |
| Cmath | |
| CNumerics | |
| CNumerics | |
| CNumerics | |
| CNumerics | |
| CNumerics | |
| Cof | |
| CPermissions | |
| CPhantomReference | |
| Creadonly bool | |
| Creadonly List< IntPtr > | |
| Creadonly Object | |
| Creadonly string | |
| Creadonly Z3_parameter_kind | |
| CReference | |
| CReferenceQueue | |
| CReflection | |
| Cstatic bool | |
| Cstatic final Object | |
| Cstatic internal Object | |
| Cstring | |
| CString | |
| Csys | |
| CSystem | |
| CT * | |
| CText | |
| CText | |
| CText | |
| CText | |
| CText | |
| CText | |
| CText | |
| CText | |
| CText | |
| CText | |
| CText | |
| CText | |
| CText | |
| CText | |
| CThreading | |
| CThreading | |
| Cuint | |
| Cunsigned | |
| CZ3_apply_result | |
| CZ3_ast | |
| CZ3_ast_kind | |
| CZ3_ast_print_mode | |
| CZ3_ast_vector | |
| CZ3_config | |
| CZ3_context | |
| CZ3_decl_kind | |
| CZ3_func_entry | |
| CZ3_func_interp | |
| CZ3_goal | |
| CZ3_goal_prec | |
| CZ3_lbool | |
| CZ3_model | |
| CZ3_optimize | |
| CZ3_param_descrs | |
| CZ3_param_kind | |
| CZ3_parameter_kind | |
| CZ3_params | |
| CZ3_probe | |
| CZ3_solver | |
| CZ3_sort_kind | |
| CZ3_stats | |
| CZ3_symbol | |
| CZ3_symbol_kind | |
| CZ3_tactic | |
| Cz3core | |
1.8.15