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 | Handle to objectives returned by objective functions. |
COptimize.Handle | |
Coptimize::handle | |
►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. |
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 | 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-tactic) 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-tactic) in the SMT 2.0 front-end. |
Ccontext::interpolation | |
CLog | |
CMap< Integer, com.microsoft.z3.enumerations.Z3_ast_kind > | |
CMap< Integer, com.microsoft.z3.enumerations.Z3_ast_print_mode > | |
CMap< Integer, com.microsoft.z3.enumerations.Z3_decl_kind > | |
CMap< Integer, com.microsoft.z3.enumerations.Z3_error_code > | |
CMap< Integer, com.microsoft.z3.enumerations.Z3_goal_prec > | |
CMap< Integer, com.microsoft.z3.enumerations.Z3_lbool > | |
CMap< Integer, com.microsoft.z3.enumerations.Z3_param_kind > | |
CMap< Integer, com.microsoft.z3.enumerations.Z3_parameter_kind > | |
CMap< Integer, com.microsoft.z3.enumerations.Z3_sort_kind > | |
CMap< Integer, com.microsoft.z3.enumerations.Z3_symbol_kind > | |
CMap< PhantomReference< T >, Long > | |
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 | |
Coptimize | |
Cparam_descrs | |
Cparams | |
Cprobe | |
Csolver | |
Cstats | |
Csymbol | |
Ctactic | |
COptimizeObjective | Optimize |
CParamDescrsRef | |
CFuncDecl.Parameter | |
CFuncDecl.Parameter | Function declarations can have Parameters associated with them. |
CParamsRef | Parameter Sets |
CProbe | |
CInterpolationContext.ReadInterpolationProblemResult | |
CReferenceQueue< T > | |
►CRuntimeException | |
►CZ3Exception | |
CModel.ModelEvaluationFailedException | |
CScopedConstructor | |
CScopedConstructorList | |
Csolver::simple | |
CStatistics | Statistics |
CStatus | |
CTactic | |
Csolver::translate | |
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 | |
►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 int | |
CFraction | |
CGeneric | |
CGeneric | |
CGeneric | |
CGeneric | |
CGeneric | |
CGeneric | |
CGeneric | |
CGeneric | |
CGeneric | |
CGeneric | |
CGeneric | |
CGeneric | |
CGeneric | |
CGeneric | |
CGeneric | |
CGeneric | |
CGeneric | |
CGeneric | |
CGeneric | |
CGeneric | |
CGeneric | |
CHashMap | |
CIdentityHashMap | |
Cint | |
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 | |
Clong | |
CMap | |
Cmath | |
CNative.Z3_error_handler | |
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 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_vector | |
CZ3_config | |
CZ3_context | |
CZ3_func_entry | |
CZ3_func_interp | |
CZ3_goal | |
CZ3_model | |
CZ3_optimize | |
CZ3_param_descrs | |
CZ3_params | |
CZ3_probe | |
CZ3_solver | |
CZ3_stats | |
CZ3_symbol | |
CZ3_tactic | |
Cz3core | |