|
Z3
|
|
|
Z3
|
|
| ▼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 |
| Cconstructor_list | |
| Cconstructors | |
| Ccontext | A Context manages all other Z3 objects, global configuration options, etc |
| 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 |
| Cfixedpoint | |
| 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 | |
| Con_clause | |
| ►Coptimize | |
| Cparam_descrs | |
| Cparameter | Class for auxiliary parameters associated with func_decl The class is initialized with a func_decl or application expression and an index The accessor get_expr, get_sort, ... is available depending on the value of kind(). The caller is responsible to check that the kind of the parameter aligns with the call (get_expr etc) |
| Cparams | |
| Cprobe | |
| Csimplifier | |
| ►Csolver | |
| Csort | A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort |
| Cstats | |
| Csymbol | |
| Ctactic | |
| Cuser_propagator_base | |
| ▼Nz3py | |
| CAlgebraicNumRef | |
| CApplyResult | |
| CArithRef | |
| CArithSortRef | Arithmetic |
| CArrayRef | |
| CArraySortRef | Arrays |
| CAstMap | |
| CAstRef | |
| CAstVector | |
| CBitVecNumRef | |
| CBitVecRef | |
| CBitVecSortRef | Bit-Vectors |
| CBoolRef | |
| CBoolSortRef | Booleans |
| CCharRef | |
| CCharSortRef | |
| CCheckSatResult | |
| CContext | |
| CDatatype | |
| CDatatypeRef | |
| CDatatypeSortRef | |
| CExprRef | Expressions |
| CFiniteDomainNumRef | |
| CFiniteDomainRef | |
| CFiniteDomainSortRef | |
| CFixedpoint | Fixedpoint |
| CFPNumRef | |
| CFPRef | |
| CFPRMRef | |
| CFPRMSortRef | |
| CFPSortRef | |
| CFuncDeclRef | Function Declarations |
| CFuncEntry | |
| CFuncInterp | |
| CGoal | |
| CIntNumRef | |
| CModelRef | |
| COnClause | |
| COptimize | |
| COptimizeObjective | Optimize |
| CParamDescrsRef | |
| CParamsRef | Parameter Sets |
| CParserContext | |
| CPatternRef | Patterns |
| CProbe | |
| CPropClosures | |
| CQuantifierRef | Quantifiers |
| CRatNumRef | |
| CReRef | |
| CReSortRef | |
| CScopedConstructor | |
| CScopedConstructorList | |
| CSeqRef | |
| CSeqSortRef | Strings, Sequences and Regular expressions |
| CSimplifier | |
| CSolver | |
| CSortRef | |
| CStatistics | Statistics |
| CTactic | |
| CTypeVarRef | |
| CUserPropagateBase | |
| CZ3PPObject | ASTs base class |
1.13.2