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 | param_descrs |
class | params |
class | ast |
class | ast_vector_tpl< T >::iterator |
class | ast_vector_tpl< T > |
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::iterator |
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 | func_entry |
class | func_interp |
class | model |
class | stats |
class | parameter |
class 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). More... | |
class | solver::cube_iterator |
class | solver::cube_generator |
class | solver |
class | goal |
class | apply_result |
class | tactic |
class | simplifier |
class | probe |
class | optimize::handle |
class | optimize |
class | fixedpoint |
class | constructor_list |
class | constructors |
class | on_clause |
class | user_propagator_base |