| ▼Ncom | |
| ►Nmicrosoft | |
| ►Nz3 | |
| CAlgebraicNum | |
| CApplyResult | |
| CArithExpr | |
| CArithSort | |
| CArrayExpr | |
| CArraySort | |
| CAST | |
| CASTVector | |
| CBitVecExpr | |
| CBitVecNum | |
| CBitVecSort | |
| CBoolExpr | |
| CBoolSort | |
| CConstructor | |
| CConstructorDecRefQueue | |
| CConstructorList | |
| CConstructorListDecRefQueue | |
| CContext | |
| CDatatypeExpr | |
| CDatatypeSort | |
| CEnumSort | |
| CExpr | |
| CFiniteDomainExpr | |
| CFiniteDomainNum | |
| CFiniteDomainSort | |
| CFixedpoint | |
| CFPExpr | |
| CFPNum | |
| CFPRMExpr | |
| CFPRMNum | |
| CFPRMSort | |
| CFPSort | |
| ►CFuncDecl | |
| CParameter | |
| CFuncInterp | |
| CGlobal | |
| CGoal | |
| CIDecRefQueue | |
| ►CInterpolationContext | |
| CCheckInterpolantResult | |
| CComputeInterpolantResult | |
| CReadInterpolationProblemResult | |
| CIntExpr | |
| CIntNum | |
| CIntSort | |
| CIntSymbol | |
| CListSort | |
| CLog | |
| ►CModel | |
| CModelEvaluationFailedException | |
| ►COptimize | |
| CHandle | |
| CParamDescrs | |
| CParams | |
| CPattern | |
| CProbe | |
| CQuantifier | |
| CRatNum | |
| CRealExpr | |
| CRealSort | |
| CReExpr | |
| CRelationSort | |
| CReSort | |
| CSeqExpr | |
| CSeqSort | |
| CSetSort | |
| CSolver | |
| CSort | |
| ►CStatistics | |
| CEntry | |
| CStatus | |
| CStringSymbol | |
| CSymbol | |
| CTactic | |
| CTupleSort | |
| CUninterpretedSort | |
| CVersion | |
| CZ3Exception | |
| CZ3Object | |
| ▼NMicrosoft | |
| ►NZ3 | |
| CAlgebraicNum | Algebraic numbers |
| CApplyResult | ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced |
| CArithExpr | Arithmetic expressions (int/real) |
| CArithSort | An arithmetic sort, i.e., Int or Real |
| CArrayExpr | Array expressions |
| CArraySort | Array sorts |
| CAST | The abstract syntax tree (AST) class |
| CASTMap | Map from AST to AST |
| CASTVector | Vectors of ASTs |
| CBitVecExpr | Bit-vector expressions |
| CBitVecNum | Bit-vector numerals |
| CBitVecSort | Bit-vector sorts |
| CBoolExpr | Boolean expressions |
| CBoolSort | A Boolean sort |
| CConstructor | Constructors are used for datatype sorts |
| CConstructorList | Lists of constructors |
| CContext | The main interaction with Z3 happens via the Context |
| CDatatypeExpr | Datatype expressions |
| CDatatypeSort | Datatype sorts |
| CDecRefQueueContracts | |
| CDeprecated | The main interaction with Z3 happens via the Context |
| CEnumSort | Enumeration sorts |
| CExpr | Expressions are terms |
| CFiniteDomainExpr | Finite-domain expressions |
| CFiniteDomainNum | Finite-domain numerals |
| CFiniteDomainSort | Finite domain sorts |
| CFixedpoint | Object for managing fixedpoints |
| CFPExpr | FloatingPoint Expressions |
| CFPNum | FloatiungPoint Numerals |
| CFPRMExpr | FloatingPoint RoundingMode Expressions |
| CFPRMNum | Floating-point rounding mode numerals |
| CFPRMSort | The FloatingPoint RoundingMode sort |
| CFPSort | FloatingPoint sort |
| ►CFuncDecl | Function declarations |
| CParameter | Function declarations can have Parameters associated with them |
| ►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 |
| CEntry | 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 |
| CIDecRefQueue | DecRefQueue interface |
| CInterpolationContext | The InterpolationContext is suitable for generation of interpolants |
| CIntExpr | Int expressions |
| CIntNum | Integer Numerals |
| CIntSort | An Integer sort |
| CIntSymbol | Numbered symbols |
| CListSort | List sorts |
| ►CModel | A Model contains interpretations (assignments) of constants and functions |
| CModelEvaluationFailedException | A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model |
| ►COptimize | Object for managing optimizization context |
| CHandle | Handle to objectives returned by objective functions |
| CParamDescrs | A ParamDescrs describes a set of parameters |
| CParams | A Params objects represents a configuration in the form of Symbol/value pairs |
| 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 |
| CProbe | |
| CQuantifier | Quantifier expressions |
| CRatNum | Rational Numerals |
| CRealExpr | Real expressions |
| CRealSort | A real sort |
| CReExpr | Regular expression expressions |
| CRelationSort | Relation sorts |
| CReSort | A regular expression sort |
| CSeqExpr | Sequence expressions |
| CSeqSort | A Sequence sort |
| CSetSort | Set sorts |
| CSolver | Solvers |
| CSort | The Sort class implements type information for ASTs |
| ►CStatistics | Objects of this class track statistical information about solvers |
| CEntry | Statistical data is organized into pairs of [Key, Entry], where every Entry is either a DoubleEntry or a UIntEntry |
| CStringSymbol | Named symbols |
| 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-tactic) in the SMT 2.0 front-end |
| CTupleSort | Tuple sorts |
| CUninterpretedSort | Uninterpreted Sorts |
| CZ3Exception | The exception base class for error reporting from Z3 |
| CZ3Object | Internal base class for interfacing with native Z3 objects. Should not be used externally |
| ▼NSystem | |
| ►NDiagnostics | |
| ►NContracts | |
| CContractClass | |
| CContractClassFor | |
| CContractInvariantMethod | |
| CContractVerification | |
| CPure | |
| ▼Nz3 | Z3 C++ namespace |
| Capply_result | |
| Carray | |
| Cast | |
| Cast_vector_tpl | |
| Ccast_ast | |
| Ccast_ast< ast > | |
| Ccast_ast< expr > | |
| Ccast_ast< func_decl > | |
| Ccast_ast< sort > | |
| Cconfig | Z3 global configuration object |
| ►Ccontext | A Context manages all other Z3 objects, global configuration options, etc |
| Cinterpolation | |
| Cexception | Exception used to sign API usage errors |
| 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 |
| Cfunc_entry | |
| Cfunc_interp | |
| Cgoal | |
| Cmodel | |
| Cobject | |
| ►Coptimize | |
| Chandle | |
| Cparam_descrs | |
| Cparams | |
| Cprobe | |
| ►Csolver | |
| Csimple | |
| Ctranslate | |
| Csort | A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort |
| Cstats | |
| Csymbol | |
| Ctactic | |
| ▼Nz3py | |
| CAlgebraicNumRef | |
| CApplyResult | |
| CArithRef | |
| CArithSortRef | Arithmetic |
| CArrayRef | |
| CArraySortRef | Arrays |
| CAstMap | |
| CAstRef | |
| CAstVector | |
| CBitVecNumRef | |
| CBitVecRef | |
| CBitVecSortRef | Bit-Vectors |
| CBoolRef | |
| CBoolSortRef | Booleans |
| CCheckSatResult | |
| CContext | |
| CDatatype | |
| CDatatypeRef | |
| CDatatypeSortRef | |
| CExprRef | Expressions |
| CFiniteDomainNumRef | |
| CFiniteDomainRef | |
| CFiniteDomainSortRef | |
| CFixedpoint | Fixedpoint |
| CFPNumRef | FP Numerals |
| CFPRef | FP Expressions |
| CFPRMRef | |
| CFPRMSortRef | |
| CFPSortRef | FP Sorts |
| CFuncDeclRef | Function Declarations |
| CFuncEntry | |
| CFuncInterp | |
| CGoal | |
| CIntNumRef | |
| CModelRef | |
| COptimize | |
| COptimizeObjective | Optimize |
| CParamDescrsRef | |
| CParamsRef | Parameter Sets |
| CPatternRef | Patterns |
| CProbe | |
| CQuantifierRef | Quantifiers |
| CRatNumRef | |
| CReRef | |
| CReSortRef | Regular expressions |
| CScopedConstructor | |
| CScopedConstructorList | |
| CSeqRef | |
| CSeqSortRef | Strings, Sequences and Regular expressions |
| CSolver | |
| CSortRef | |
| CStatistics | Statistics |
| CTactic | |
| CZ3PPObject | ASTs base class |
| CAttribute | |
| CAutoCloseable | |
| CComparable | |
| CException | |
| CIComparable | |
| CIDisposable | |
| CRuntimeException | |
1.8.15