Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Data Structures
Here are the data structures with brief descriptions:
[detail level 123]
 Nz3Z3 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 >
 CconfigZ3 global configuration object
 CcontextA Context manages all other Z3 objects, global configuration options, etc
 CexceptionException used to sign API usage errors
 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
 Cfixedpoint
 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
 Cfunc_entry
 Cfunc_interp
 Cgoal
 Cmodel
 Ctranslate
 Cobject
 Coptimize
 Chandle
 Cparam_descrs
 Cparams
 Cprobe
 Csolver
 Ccube_generator
 Ccube_iterator
 Csimple
 Ctranslate
 CsortA Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort
 Cstats
 Csymbol
 Ctactic