|
Z3
|
|
|
Z3
|
|
| ▼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 |
1.8.9.1