|
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 () |
|
std::ostream & | operator<< (std::ostream &out, exception const &e) |
|
check_result | to_check_result (Z3_lbool l) |
|
void | check_context (object const &a, object const &b) |
|
std::ostream & | operator<< (std::ostream &out, symbol const &s) |
|
std::ostream & | operator<< (std::ostream &out, param_descrs const &d) |
|
std::ostream & | operator<< (std::ostream &out, params const &p) |
|
std::ostream & | operator<< (std::ostream &out, ast const &n) |
|
bool | eq (ast const &a, ast const &b) |
|
expr | select (expr const &a, expr const &i) |
| forward declarations More...
|
|
expr | select (expr const &a, expr_vector const &i) |
|
expr | implies (expr const &a, expr 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 | mod (expr const &a, expr const &b) |
|
expr | mod (expr const &a, int b) |
|
expr | mod (int a, expr const &b) |
|
expr | operator% (expr const &a, expr const &b) |
|
expr | operator% (expr const &a, int b) |
|
expr | operator% (int a, expr const &b) |
|
expr | rem (expr const &a, expr const &b) |
|
expr | rem (expr const &a, int b) |
|
expr | rem (int a, expr const &b) |
|
expr | operator! (expr const &a) |
|
expr | is_int (expr const &e) |
|
expr | operator&& (expr const &a, expr const &b) |
|
expr | operator&& (expr const &a, bool b) |
|
expr | operator&& (bool a, expr const &b) |
|
expr | operator|| (expr const &a, expr const &b) |
|
expr | operator|| (expr const &a, bool b) |
|
expr | operator|| (bool a, expr const &b) |
|
expr | operator== (expr const &a, expr const &b) |
|
expr | operator== (expr const &a, int b) |
|
expr | operator== (int a, expr const &b) |
|
expr | operator== (expr const &a, double b) |
|
expr | operator== (double a, expr const &b) |
|
expr | operator!= (expr const &a, expr const &b) |
|
expr | operator!= (expr const &a, int b) |
|
expr | operator!= (int a, expr const &b) |
|
expr | operator!= (expr const &a, double b) |
|
expr | operator!= (double a, expr const &b) |
|
expr | operator+ (expr const &a, expr const &b) |
|
expr | operator+ (expr const &a, int b) |
|
expr | operator+ (int a, expr const &b) |
|
expr | operator* (expr const &a, expr const &b) |
|
expr | operator* (expr const &a, int b) |
|
expr | operator* (int a, expr const &b) |
|
expr | operator>= (expr const &a, expr const &b) |
|
expr | operator/ (expr const &a, expr const &b) |
|
expr | operator/ (expr const &a, int b) |
|
expr | operator/ (int a, expr const &b) |
|
expr | operator- (expr const &a) |
|
expr | operator- (expr const &a, expr const &b) |
|
expr | operator- (expr const &a, int b) |
|
expr | operator- (int a, expr const &b) |
|
expr | operator<= (expr const &a, expr const &b) |
|
expr | operator<= (expr const &a, int b) |
|
expr | operator<= (int a, expr const &b) |
|
expr | operator>= (expr const &a, int b) |
|
expr | operator>= (int a, expr const &b) |
|
expr | operator< (expr const &a, expr const &b) |
|
expr | operator< (expr const &a, int b) |
|
expr | operator< (int a, expr const &b) |
|
expr | operator> (expr const &a, expr const &b) |
|
expr | operator> (expr const &a, int b) |
|
expr | operator> (int a, expr const &b) |
|
expr | operator& (expr const &a, expr const &b) |
|
expr | operator& (expr const &a, int b) |
|
expr | operator& (int a, expr const &b) |
|
expr | operator^ (expr const &a, expr const &b) |
|
expr | operator^ (expr const &a, int b) |
|
expr | operator^ (int a, expr const &b) |
|
expr | operator| (expr const &a, expr const &b) |
|
expr | operator| (expr const &a, int b) |
|
expr | operator| (int a, expr const &b) |
|
expr | nand (expr const &a, expr const &b) |
|
expr | nor (expr const &a, expr const &b) |
|
expr | xnor (expr const &a, expr const &b) |
|
expr | min (expr const &a, expr const &b) |
|
expr | max (expr const &a, expr const &b) |
|
expr | bvredor (expr const &a) |
|
expr | bvredand (expr const &a) |
|
expr | abs (expr const &a) |
|
expr | sqrt (expr const &a, expr const &rm) |
|
expr | fp_eq (expr const &a, expr const &b) |
|
expr | operator~ (expr const &a) |
|
expr | fma (expr const &a, expr const &b, expr const &c, expr const &rm) |
|
expr | fpa_fp (expr const &sgn, expr const &exp, expr const &sig) |
|
expr | fpa_to_sbv (expr const &t, unsigned sz) |
|
expr | fpa_to_ubv (expr const &t, unsigned sz) |
|
expr | sbv_to_fpa (expr const &t, sort s) |
|
expr | ubv_to_fpa (expr const &t, sort s) |
|
expr | fpa_to_fpa (expr const &t, sort s) |
|
expr | round_fpa_to_closest_integer (expr const &t) |
|
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 | sle (expr const &a, expr const &b) |
| signed less than or equal to operator for bitvectors. More...
|
|
expr | sle (expr const &a, int b) |
|
expr | sle (int a, expr const &b) |
|
expr | slt (expr const &a, expr const &b) |
| signed less than operator for bitvectors. More...
|
|
expr | slt (expr const &a, int b) |
|
expr | slt (int a, expr const &b) |
|
expr | sge (expr const &a, expr const &b) |
| signed greater than or equal to operator for bitvectors. More...
|
|
expr | sge (expr const &a, int b) |
|
expr | sge (int a, expr const &b) |
|
expr | sgt (expr const &a, expr const &b) |
| signed greater than operator for bitvectors. More...
|
|
expr | sgt (expr const &a, int b) |
|
expr | sgt (int a, expr const &b) |
|
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 | srem (expr const &a, expr const &b) |
| signed remainder operator for bitvectors More...
|
|
expr | srem (expr const &a, int b) |
|
expr | srem (int a, expr const &b) |
|
expr | smod (expr const &a, expr const &b) |
| signed modulus operator for bitvectors More...
|
|
expr | smod (expr const &a, int b) |
|
expr | smod (int a, expr const &b) |
|
expr | urem (expr const &a, expr const &b) |
| unsigned reminder operator for bitvectors More...
|
|
expr | urem (expr const &a, int b) |
|
expr | urem (int a, expr const &b) |
|
expr | shl (expr const &a, expr const &b) |
| shift left operator for bitvectors More...
|
|
expr | shl (expr const &a, int b) |
|
expr | shl (int a, expr const &b) |
|
expr | lshr (expr const &a, expr const &b) |
| logic shift right operator for bitvectors More...
|
|
expr | lshr (expr const &a, int b) |
|
expr | lshr (int a, expr const &b) |
|
expr | ashr (expr const &a, expr const &b) |
| arithmetic shift right operator for bitvectors More...
|
|
expr | ashr (expr const &a, int b) |
|
expr | ashr (int a, expr const &b) |
|
expr | zext (expr const &a, unsigned i) |
| 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. More...
|
|
expr | bv2int (expr const &a, bool is_signed) |
| bit-vector and integer conversions. More...
|
|
expr | int2bv (unsigned n, expr const &a) |
|
expr | bvadd_no_overflow (expr const &a, expr const &b, bool is_signed) |
| bit-vector overflow/underflow checks More...
|
|
expr | bvadd_no_underflow (expr const &a, expr const &b) |
|
expr | bvsub_no_overflow (expr const &a, expr const &b) |
|
expr | bvsub_no_underflow (expr const &a, expr const &b, bool is_signed) |
|
expr | bvsdiv_no_overflow (expr const &a, expr const &b) |
|
expr | bvneg_no_overflow (expr const &a) |
|
expr | bvmul_no_overflow (expr const &a, expr const &b, bool is_signed) |
|
expr | bvmul_no_underflow (expr const &a, expr const &b) |
|
expr | sext (expr const &a, unsigned i) |
| 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. More...
|
|
func_decl | linear_order (sort const &a, unsigned index) |
|
func_decl | partial_order (sort const &a, unsigned index) |
|
func_decl | piecewise_linear_order (sort const &a, unsigned index) |
|
func_decl | tree_order (sort const &a, unsigned index) |
|
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 | lambda (expr const &x, expr const &b) |
|
expr | lambda (expr const &x1, expr const &x2, expr const &b) |
|
expr | lambda (expr const &x1, expr const &x2, expr const &x3, expr const &b) |
|
expr | lambda (expr const &x1, expr const &x2, expr const &x3, expr const &x4, expr const &b) |
|
expr | lambda (expr_vector const &xs, expr const &b) |
|
expr | pble (expr_vector const &es, int const *coeffs, int bound) |
|
expr | pbge (expr_vector const &es, int const *coeffs, int bound) |
|
expr | pbeq (expr_vector const &es, int const *coeffs, int bound) |
|
expr | atmost (expr_vector const &es, unsigned bound) |
|
expr | atleast (expr_vector const &es, unsigned bound) |
|
expr | sum (expr_vector const &args) |
|
expr | distinct (expr_vector const &args) |
|
expr | concat (expr const &a, expr const &b) |
|
expr | concat (expr_vector const &args) |
|
expr | map (expr const &f, expr const &list) |
|
expr | mapi (expr const &f, expr const &i, expr const &list) |
|
expr | foldl (expr const &f, expr const &a, expr const &list) |
|
expr | foldli (expr const &f, expr const &i, expr const &a, expr const &list) |
|
expr | mk_or (expr_vector const &args) |
|
expr | mk_and (expr_vector const &args) |
|
expr | mk_xor (expr_vector const &args) |
|
std::ostream & | operator<< (std::ostream &out, model const &m) |
|
std::ostream & | operator<< (std::ostream &out, stats const &s) |
|
std::ostream & | operator<< (std::ostream &out, check_result r) |
|
std::ostream & | operator<< (std::ostream &out, solver const &s) |
|
std::ostream & | operator<< (std::ostream &out, goal const &g) |
|
std::ostream & | operator<< (std::ostream &out, apply_result const &r) |
|
tactic | operator& (tactic const &t1, tactic const &t2) |
|
tactic | operator| (tactic const &t1, tactic const &t2) |
|
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 | par_or (unsigned n, tactic const *tactics) |
|
tactic | par_and_then (tactic const &t1, tactic const &t2) |
|
simplifier | operator& (simplifier const &t1, simplifier const &t2) |
|
simplifier | with (simplifier const &t, params const &p) |
|
probe | operator<= (probe const &p1, probe const &p2) |
|
probe | operator<= (probe const &p1, double p2) |
|
probe | operator<= (double p1, probe const &p2) |
|
probe | operator>= (probe const &p1, probe const &p2) |
|
probe | operator>= (probe const &p1, double p2) |
|
probe | operator>= (double p1, probe const &p2) |
|
probe | operator< (probe const &p1, probe const &p2) |
|
probe | operator< (probe const &p1, double p2) |
|
probe | operator< (double p1, probe const &p2) |
|
probe | operator> (probe const &p1, probe const &p2) |
|
probe | operator> (probe const &p1, double p2) |
|
probe | operator> (double p1, probe const &p2) |
|
probe | operator== (probe const &p1, probe const &p2) |
|
probe | operator== (probe const &p1, double p2) |
|
probe | operator== (double p1, probe const &p2) |
|
probe | operator&& (probe const &p1, probe const &p2) |
|
probe | operator|| (probe const &p1, probe const &p2) |
|
probe | operator! (probe const &p) |
|
std::ostream & | operator<< (std::ostream &out, optimize const &s) |
|
std::ostream & | operator<< (std::ostream &out, fixedpoint const &f) |
|
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) |
|
func_decl | function (char const *name, sort_vector const &domain, sort const &range) |
|
func_decl | function (std::string const &name, sort_vector const &domain, sort const &range) |
|
func_decl | recfun (symbol const &name, unsigned arity, sort const *domain, sort const &range) |
|
func_decl | recfun (char const *name, unsigned arity, sort const *domain, sort const &range) |
|
func_decl | recfun (char const *name, sort const &d1, sort const &range) |
|
func_decl | recfun (char const *name, sort const &d1, sort const &d2, sort const &range) |
|
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 | store (expr const &a, expr_vector const &i, expr const &v) |
|
expr | as_array (func_decl &f) |
|
expr | const_array (sort const &d, expr const &v) |
|
expr | empty_set (sort const &s) |
|
expr | full_set (sort const &s) |
|
expr | set_add (expr const &s, expr const &e) |
|
expr | set_del (expr const &s, expr const &e) |
|
expr | set_union (expr const &a, expr const &b) |
|
expr | set_intersect (expr const &a, expr const &b) |
|
expr | set_difference (expr const &a, expr const &b) |
|
expr | set_complement (expr const &a) |
|
expr | set_member (expr const &s, expr const &e) |
|
expr | set_subset (expr const &a, expr const &b) |
|
expr | empty (sort const &s) |
|
expr | suffixof (expr const &a, expr const &b) |
|
expr | prefixof (expr const &a, expr const &b) |
|
expr | indexof (expr const &s, expr const &substr, expr const &offset) |
|
expr | last_indexof (expr const &s, expr const &substr) |
|
expr | to_re (expr const &s) |
|
expr | in_re (expr const &s, expr const &re) |
|
expr | plus (expr const &re) |
|
expr | option (expr const &re) |
|
expr | star (expr const &re) |
|
expr | re_empty (sort const &s) |
|
expr | re_full (sort const &s) |
|
expr | re_intersect (expr_vector const &args) |
|
expr | re_diff (expr const &a, expr const &b) |
|
expr | re_complement (expr const &a) |
|
expr | range (expr const &lo, expr const &hi) |
|