Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Class Hierarchy

Go to the graphical class hierarchy

This inheritance list is sorted roughly, but not completely, alphabetically:
[detail level 123]
 Carray< T >
 Ccast_ast< T >
 Ccast_ast< ast >
 Ccast_ast< expr >
 Ccast_ast< func_decl >
 Ccast_ast< sort >
 CconfigZ3 global configuration object
 CcontextA Context manages all other Z3 objects, global configuration options, etc
 Csolver::cube_generator
 Csolver::cube_iterator
 CexceptionException used to sign API usage errors
 Coptimize::handle
 Cast_vector_tpl< T >::iterator
 Cobject
 Cast_vector_tpl< expr >
 Capply_result
 Cast
 CexprA 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_declFunction 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
 CsortA 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
 Csolver
 Cstats
 Csymbol
 Ctactic
 Csolver::simple
 Csolver::translate
 Cmodel::translate
 Cbool
 Crounding_mode
 Cstring
 CT *
 Cunsigned
 CZ3_apply_result
 CZ3_ast
 CZ3_ast_vector
 CZ3_config
 CZ3_context
 CZ3_fixedpoint
 CZ3_func_entry
 CZ3_func_interp
 CZ3_goal
 CZ3_model
 CZ3_optimize
 CZ3_param_descrs
 CZ3_params
 CZ3_probe
 CZ3_solver
 CZ3_stats
 CZ3_symbol
 CZ3_tactic