Z3 C++ namespace. More...
Data Structures | |
class | apply_result |
class | array |
class | ast |
class | ast_vector_tpl |
class | cast_ast |
class | cast_ast< ast > |
class | cast_ast< expr > |
class | cast_ast< func_decl > |
class | cast_ast< sort > |
class | config |
Z3 global configuration object. More... | |
class | constructor_list |
class | constructors |
class | context |
A Context manages all other Z3 objects, global configuration options, etc. More... | |
class | exception |
Exception used to sign API usage errors. 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 | fixedpoint |
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 | func_entry |
class | func_interp |
class | goal |
class | model |
class | object |
class | on_clause |
class | optimize |
class | param_descrs |
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 | params |
class | probe |
class | simplifier |
class | solver |
class | sort |
A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort. More... | |
class | stats |
class | symbol |
class | tactic |
class | user_propagator_base |
Typedefs | |
typedef ast_vector_tpl< ast > | ast_vector |
typedef ast_vector_tpl< expr > | expr_vector |
typedef ast_vector_tpl< sort > | sort_vector |
typedef ast_vector_tpl< func_decl > | func_decl_vector |
typedef std::function< void(expr const &proof, std::vector< unsigned > const &deps, expr_vector const &clause) | on_clause_eh_t) |
Enumerations | |
enum | check_result { unsat , sat , unknown } |
enum | rounding_mode { RNA , RNE , RTP , RTN , RTZ } |
Z3 C++ namespace.
Definition at line 1995 of file z3++.h.
Definition at line 3991 of file z3++.h.
arithmetic shift right operator for bitvectors
Definition at line 2221 of file z3++.h.
|
inline |
Definition at line 2430 of file z3++.h.
|
inline |
Definition at line 2422 of file z3++.h.
bit-vector overflow/underflow checks
Definition at line 2239 of file z3++.h.
Definition at line 2242 of file z3++.h.
Definition at line 2257 of file z3++.h.
Definition at line 2260 of file z3++.h.
Definition at line 2251 of file z3++.h.
Definition at line 2245 of file z3++.h.
Definition at line 2248 of file z3++.h.
Definition at line 478 of file z3++.h.
Referenced by cond(), exists(), exists(), exists(), exists(), forall(), forall(), forall(), forall(), context::function(), context::function(), context::function(), context::function(), context::function(), context::function(), context::function(), indexof(), lambda(), lambda(), lambda(), lambda(), last_indexof(), prefixof(), re_diff(), context::recdef(), context::recfun(), context::recfun(), select(), select(), set_intersect(), set_union(), store(), store(), suffixof(), context::user_propagate_function(), and when().
Definition at line 2456 of file z3++.h.
|
inline |
Definition at line 2474 of file z3++.h.
Definition at line 3471 of file z3++.h.
|
inline |
Definition at line 2447 of file z3++.h.
Definition at line 4064 of file z3++.h.
Definition at line 2349 of file z3++.h.
Definition at line 2354 of file z3++.h.
Definition at line 2359 of file z3++.h.
|
inline |
Definition at line 2364 of file z3++.h.
|
inline |
Definition at line 3460 of file z3++.h.
Definition at line 2514 of file z3++.h.
Definition at line 2521 of file z3++.h.
Definition at line 2325 of file z3++.h.
Definition at line 2330 of file z3++.h.
Definition at line 2335 of file z3++.h.
|
inline |
Definition at line 2340 of file z3++.h.
|
inline |
|
inline |
Definition at line 3931 of file z3++.h.
|
inline |
|
inline |
Definition at line 2500 of file z3++.h.
Definition at line 2507 of file z3++.h.
Definition at line 1967 of file z3++.h.
Definition at line 1951 of file z3++.h.
|
inline |
|
inline |
|
inline |
Definition at line 1641 of file z3++.h.
Referenced by operator%(), operator%(), and operator%().
Definition at line 3283 of file z3++.h.
Definition at line 1717 of file z3++.h.
|
inline |
Definition at line 3197 of file z3++.h.
Definition at line 3277 of file z3++.h.
Definition at line 1759 of file z3++.h.
Definition at line 1729 of file z3++.h.
Definition at line 1825 of file z3++.h.
Definition at line 1844 of file z3++.h.
Definition at line 1803 of file z3++.h.
Definition at line 1892 of file z3++.h.
Definition at line 3262 of file z3++.h.
|
inline |
|
inline |
|
inline |
|
inline |
Definition at line 1867 of file z3++.h.
Definition at line 3252 of file z3++.h.
Definition at line 3272 of file z3++.h.
Definition at line 1914 of file z3++.h.
Definition at line 3267 of file z3++.h.
Definition at line 1783 of file z3++.h.
Definition at line 3257 of file z3++.h.
Definition at line 3280 of file z3++.h.
Definition at line 2414 of file z3++.h.
Definition at line 2406 of file z3++.h.
Definition at line 2398 of file z3++.h.
Definition at line 4136 of file z3++.h.
Referenced by context::function(), function(), context::function(), function(), context::function(), function(), context::function(), function(), context::function(), function(), context::function(), function(), context::function(), function(), function(), context::function(), context::function(), function(), context::recfun(), recfun(), recfun(), context::recfun(), context::recfun(), context::recfun(), recfun(), context::recfun(), context::recfun(), recfun(), and context::user_propagate_function().
Definition at line 4126 of file z3++.h.
Definition at line 4108 of file z3++.h.
Definition at line 4113 of file z3++.h.
|
inline |
Definition at line 4118 of file z3++.h.
Definition at line 3950 of file z3++.h.
|
inline |
Definition at line 83 of file z3++.h.
forward declarations
Definition at line 3954 of file z3++.h.
Referenced by expr::operator[](), expr::operator[](), and select().
|
inline |
Definition at line 4036 of file z3++.h.
Definition at line 4028 of file z3++.h.
Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector.
Definition at line 2268 of file z3++.h.
|
inline |
|
inline |
Definition at line 147 of file z3++.h.
Referenced by solver::check(), optimize::check(), optimize::check(), solver::check(), solver::check(), solver::consequences(), fixedpoint::query(), and fixedpoint::query().
Wraps a Z3_ast as an expr object. It also checks for errors. This function allows the user to use the whole C API with the C++ layer defined in this file.
Definition at line 2107 of file z3++.h.
Referenced by ashr(), lshr(), sext(), sge(), sgt(), shl(), sle(), slt(), smod(), srem(), udiv(), uge(), ugt(), ule(), ult(), urem(), and zext().
|
inline |
Definition at line 2121 of file z3++.h.
Referenced by linear_order(), partial_order(), piecewise_linear_order(), and tree_order().
Definition at line 2116 of file z3++.h.
Referenced by context::enumeration_sort(), context::tuple_sort(), context::uninterpreted_sort(), and context::uninterpreted_sort().
|
inline |
Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where m is the size of the given bit-vector.
Definition at line 2228 of file z3++.h.