|
void | set_param (char const *param, char const *value) |
|
void | set_param (char const *param, bool value) |
|
void | set_param (char const *param, int value) |
|
void | reset_params () |
|
void | check_context (object const &a, object const &b) |
|
bool | eq (ast const &a, ast const &b) |
|
expr | implies (expr const &a, bool b) |
|
expr | implies (bool a, expr const &b) |
|
expr | pw (expr const &a, expr const &b) |
|
expr | pw (expr const &a, int b) |
|
expr | pw (int a, expr const &b) |
|
expr | ite (expr const &c, expr const &t, expr const &e) |
| Create the if-then-else expression ite(c, t, e) More...
|
|
expr | to_expr (context &c, Z3_ast a) |
| 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. More...
|
|
sort | to_sort (context &c, Z3_sort s) |
|
func_decl | to_func_decl (context &c, Z3_func_decl f) |
|
expr | ule (expr const &a, expr const &b) |
| unsigned less than or equal to operator for bitvectors. More...
|
|
expr | ule (expr const &a, int b) |
|
expr | ule (int a, expr const &b) |
|
expr | ult (expr const &a, expr const &b) |
| unsigned less than operator for bitvectors. More...
|
|
expr | ult (expr const &a, int b) |
|
expr | ult (int a, expr const &b) |
|
expr | uge (expr const &a, expr const &b) |
| unsigned greater than or equal to operator for bitvectors. More...
|
|
expr | uge (expr const &a, int b) |
|
expr | uge (int a, expr const &b) |
|
expr | ugt (expr const &a, expr const &b) |
| unsigned greater than operator for bitvectors. More...
|
|
expr | ugt (expr const &a, int b) |
|
expr | ugt (int a, expr const &b) |
|
expr | udiv (expr const &a, expr const &b) |
| unsigned division operator for bitvectors. More...
|
|
expr | udiv (expr const &a, int b) |
|
expr | udiv (int a, expr const &b) |
|
expr | forall (expr const &x, expr const &b) |
|
expr | forall (expr const &x1, expr const &x2, expr const &b) |
|
expr | forall (expr const &x1, expr const &x2, expr const &x3, expr const &b) |
|
expr | forall (expr const &x1, expr const &x2, expr const &x3, expr const &x4, expr const &b) |
|
expr | forall (expr_vector const &xs, expr const &b) |
|
expr | exists (expr const &x, expr const &b) |
|
expr | exists (expr const &x1, expr const &x2, expr const &b) |
|
expr | exists (expr const &x1, expr const &x2, expr const &x3, expr const &b) |
|
expr | exists (expr const &x1, expr const &x2, expr const &x3, expr const &x4, expr const &b) |
|
expr | exists (expr_vector const &xs, expr const &b) |
|
expr | distinct (expr_vector const &args) |
|
expr | concat (expr const &a, expr const &b) |
|
std::ostream & | operator<< (std::ostream &out, check_result r) |
|
check_result | to_check_result (Z3_lbool l) |
|
tactic | repeat (tactic const &t, unsigned max=UINT_MAX) |
|
tactic | with (tactic const &t, params const &p) |
|
tactic | try_for (tactic const &t, unsigned ms) |
|
tactic | fail_if (probe const &p) |
|
tactic | when (probe const &p, tactic const &t) |
|
tactic | cond (probe const &p, tactic const &t1, tactic const &t2) |
|
expr | to_real (expr const &a) |
|
func_decl | function (symbol const &name, unsigned arity, sort const *domain, sort const &range) |
|
func_decl | function (char const *name, unsigned arity, sort const *domain, sort const &range) |
|
func_decl | function (char const *name, sort const &domain, sort const &range) |
|
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &range) |
|
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &range) |
|
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &range) |
|
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &d5, sort const &range) |
|
expr | select (expr const &a, expr const &i) |
|
expr | select (expr const &a, int i) |
|
expr | store (expr const &a, expr const &i, expr const &v) |
|
expr | store (expr const &a, int i, expr const &v) |
|
expr | store (expr const &a, expr i, int v) |
|
expr | store (expr const &a, int i, int v) |
|
expr | const_array (sort const &d, expr const &v) |
|