Carray< T > | |
CAstMap | |
Ccast_ast< T > | |
Ccast_ast< ast > | |
Ccast_ast< expr > | |
Ccast_ast< func_decl > | |
Ccast_ast< sort > | |
CCheckSatResult | |
Cconfig | Z3 global configuration object |
Cconstructor_list | |
Cconstructors | |
CContext | |
Ccontext | A Context manages all other Z3 objects, global configuration options, etc |
Csolver::cube_generator | |
Csolver::cube_iterator | |
CDatatype | |
▼Cexception | |
Cexception | Exception used to sign API usage errors |
CFuncEntry | |
Coptimize::handle | |
Cast_vector_tpl< T >::iterator | |
Cexpr::iterator | |
▼Cobject | |
Cast_vector_tpl< expr > | |
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 > | |
Cfixedpoint | |
Cfunc_entry | |
Cfunc_interp | |
Cgoal | |
Cmodel | |
Coptimize | |
Cparam_descrs | |
Cparams | |
Cprobe | |
Csimplifier | |
Csolver | |
Cstats | |
Csymbol | |
Ctactic | |
Con_clause | |
COnClause | |
COptimizeObjective | Optimize |
CParamDescrsRef | |
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) |
CParamsRef | Parameter Sets |
CParserContext | |
CProbe | |
CPropClosures | |
CScopedConstructor | |
CScopedConstructorList | |
Csolver::simple | |
CSimplifier | |
CStatistics | Statistics |
CTactic | |
Cmodel::translate | |
Csolver::translate | |
Cuser_propagator_base | |
CUserPropagateBase | |
▼CZ3PPObject | ASTs base class |
CApplyResult | |
▼CAstRef | |
▼CExprRef | Expressions |
►CArithRef | |
CArrayRef | |
►CBitVecRef | |
►CBoolRef | |
CCharRef | |
CDatatypeRef | |
CFPRMRef | |
►CFPRef | |
►CFiniteDomainRef | |
CPatternRef | Patterns |
CReRef | |
CSeqRef | |
CFuncDeclRef | Function Declarations |
▼CSortRef | |
CArithSortRef | Arithmetic |
CArraySortRef | Arrays |
CBitVecSortRef | Bit-Vectors |
CBoolSortRef | Booleans |
CCharSortRef | |
CDatatypeSortRef | |
CFPRMSortRef | |
CFPSortRef | |
CFiniteDomainSortRef | |
CReSortRef | |
CSeqSortRef | Strings, Sequences and Regular expressions |
CTypeVarRef | |
CAstVector | |
CFixedpoint | Fixedpoint |
CFuncInterp | |
CGoal | |
CModelRef | |
COptimize | |
CSolver |