▼Ncom | |
▼Nmicrosoft | |
►Nz3 | |
▼Nz3 | Z3 C++ namespace |
Capply_result | |
Carray | |
Cast | |
▼Cast_vector_tpl | |
Citerator | |
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 |
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 | |
Ctranslate | |
Cobject | |
▼Coptimize | |
Chandle | |
Cparam_descrs | |
Cparams | |
Cprobe | |
▼Csolver | |
Ccube_generator | |
Ccube_iterator | |
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 |
CAutoCloseable | |
CComparable |