Z3
Class Hierarchy

Go to the graphical class hierarchy

This inheritance list is sorted roughly, but not completely, alphabetically:
[detail level 12345]
 Carray< T >
 CAstMap
 Ccast_ast< T >
 Ccast_ast< ast >
 Ccast_ast< expr >
 Ccast_ast< func_decl >
 Ccast_ast< sort >
 CCheckSatResult
 CconfigZ3 global configuration object
 Cconstructor_list
 Cconstructors
 CcontextA Context manages all other Z3 objects, global configuration options, etc
 CContext
 Csolver::cube_generator
 Csolver::cube_iterator
 CDatatype
 Cexception
 CFuncEntry
 Coptimize::handle
 Cast_vector_tpl< T >::iterator
 Cexpr::iterator
 Cobject
 Con_clause
 COnClause
 COptimizeObjectiveOptimize
 CParamDescrsRef
 CparameterClass 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)
 CParamsRefParameter Sets
 CParserContext
 CProbe
 CPropClosures
 CScopedConstructor
 CScopedConstructorList
 Csolver::simple
 CSimplifier
 CStatisticsStatistics
 CTactic
 Cmodel::translate
 Csolver::translate
 Cuser_propagator_base
 CUserPropagateBase
 CZ3PPObjectASTs base class
 Cbool
 Ccopy
 CFraction
 Cfunction< void(expr &, unsigned &, Z3_lbool &)>
 Cfunction< void(expr const &)>
 Cfunction< void(expr const &, expr const &)>
 Cfunction< void(expr const &proof, expr_vector const &clause)>
 Cfunction< void(void)>
 Cio
 CIterable
 Cmath
 Crounding_mode
 Cstring
 Csys
 Cunique_ptr< T[]>
 Cunsigned
 Cvector< unsigned >
 Cvector< z3::z3::context * >
 Cvector< Z3_constructor >
 CZ3_apply_result
 CZ3_ast
 CZ3_ast_vector
 CZ3_config
 CZ3_constructor_list
 CZ3_context
 CZ3_fixedpoint
 CZ3_func_entry
 CZ3_func_interp
 CZ3_goal
 CZ3_model
 CZ3_optimize
 CZ3_param_descrs
 CZ3_parameter_kind
 CZ3_params
 CZ3_probe
 CZ3_simplifier
 CZ3_solver
 CZ3_solver_callback
 CZ3_stats
 CZ3_symbol
 CZ3_tactic
 Cz3core