Namespaces | |
z3 | |
Z3 C++ namespace. | |
Data Structures | |
class | exception |
Exception used to sign API usage errors. More... | |
class | config |
Z3 global configuration object. More... | |
class | context |
A Context manages all other Z3 objects, global configuration options, etc. More... | |
class | array< T > |
class | object |
class | symbol |
class | params |
class | ast |
class | sort |
A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort. More... | |
class | func_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. More... | |
class | expr |
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. More... | |
class | cast_ast< ast > |
class | cast_ast< expr > |
class | cast_ast< sort > |
class | cast_ast< func_decl > |
class | ast_vector_tpl< T > |
class | func_entry |
class | func_interp |
class | model |
class | stats |
class | solver |
class | goal |
class | apply_result |
class | tactic |
class | probe |
Enumerations | |
enum | check_result { unsat, sat, unknown } |
enum check_result |
Enumerator | |
---|---|
unsat | |
sat | |
unknown |