Z3 C++ namespace.
More...
|
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 | 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) |
|
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) |
|
◆ ast_vector
◆ expr_vector
◆ func_decl_vector
◆ sort_vector
◆ check_result
Enumerator |
---|
unsat | |
sat | |
unknown | |
Definition at line 132 of file z3++.h.
◆ rounding_mode
Enumerator |
---|
RNA | |
RNE | |
RTP | |
RTN | |
RTZ | |
Definition at line 136 of file z3++.h.
◆ abs()
Definition at line 1919 of file z3++.h.
1922 expr zero = a.ctx().int_val(0);
1923 expr ge = a >= zero;
1927 else if (a.is_real()) {
1928 expr zero = a.ctx().real_val(0);
1929 expr ge = a >= zero;
1937 return expr(a.ctx(), r);
◆ as_array()
Definition at line 3665 of file z3++.h.
3668 return expr(f.ctx(), r);
◆ ashr() [1/3]
arithmetic shift right operator for bitvectors
Definition at line 2145 of file z3++.h.
Referenced by ashr().
◆ ashr() [2/3]
Definition at line 2146 of file z3++.h.
2146 {
return ashr(a, a.ctx().num_val(b, a.get_sort())); }
◆ ashr() [3/3]
Definition at line 2147 of file z3++.h.
2147 {
return ashr(b.ctx().num_val(a, b.get_sort()), b); }
◆ atleast()
Definition at line 2354 of file z3++.h.
2355 assert(es.size() > 0);
2356 context& ctx = es[0].ctx();
2357 array<Z3_ast> _es(es);
2358 Z3_ast r =
Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
2360 return expr(ctx, r);
◆ atmost()
Definition at line 2346 of file z3++.h.
2347 assert(es.size() > 0);
2348 context& ctx = es[0].ctx();
2349 array<Z3_ast> _es(es);
2350 Z3_ast r =
Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
2352 return expr(ctx, r);
◆ bv2int()
expr z3::bv2int |
( |
expr const & |
a, |
|
|
bool |
is_signed |
|
) |
| |
|
inline |
bit-vector and integer conversions.
Definition at line 2157 of file z3++.h.
2157 { Z3_ast r =
Z3_mk_bv2int(a.ctx(), a, is_signed); a.check_error();
return expr(a.ctx(), r); }
◆ bvadd_no_overflow()
expr z3::bvadd_no_overflow |
( |
expr const & |
a, |
|
|
expr const & |
b, |
|
|
bool |
is_signed |
|
) |
| |
|
inline |
bit-vector overflow/underflow checks
Definition at line 2163 of file z3++.h.
◆ bvadd_no_underflow()
expr z3::bvadd_no_underflow |
( |
expr const & |
a, |
|
|
expr const & |
b |
|
) |
| |
|
inline |
◆ bvmul_no_overflow()
expr z3::bvmul_no_overflow |
( |
expr const & |
a, |
|
|
expr const & |
b, |
|
|
bool |
is_signed |
|
) |
| |
|
inline |
◆ bvmul_no_underflow()
expr z3::bvmul_no_underflow |
( |
expr const & |
a, |
|
|
expr const & |
b |
|
) |
| |
|
inline |
◆ bvneg_no_overflow()
expr z3::bvneg_no_overflow |
( |
expr const & |
a | ) |
|
|
inline |
◆ bvredand()
Definition at line 1913 of file z3++.h.
1917 return expr(a.ctx(), r);
◆ bvredor()
Definition at line 1907 of file z3++.h.
1911 return expr(a.ctx(), r);
◆ bvsdiv_no_overflow()
expr z3::bvsdiv_no_overflow |
( |
expr const & |
a, |
|
|
expr const & |
b |
|
) |
| |
|
inline |
◆ bvsub_no_overflow()
expr z3::bvsub_no_overflow |
( |
expr const & |
a, |
|
|
expr const & |
b |
|
) |
| |
|
inline |
◆ bvsub_no_underflow()
expr z3::bvsub_no_underflow |
( |
expr const & |
a, |
|
|
expr const & |
b, |
|
|
bool |
is_signed |
|
) |
| |
|
inline |
◆ check_context()
void z3::check_context |
( |
object const & |
a, |
|
|
object const & |
b |
|
) |
| |
|
inline |
Definition at line 433 of file z3++.h.
433 { (void)a; (void)b; assert(a.m_ctx == b.m_ctx); }
Referenced by bvadd_no_overflow(), bvadd_no_underflow(), bvmul_no_overflow(), bvmul_no_underflow(), bvsdiv_no_overflow(), bvsub_no_overflow(), bvsub_no_underflow(), concat(), cond(), exists(), fma(), forall(), fp_eq(), fpa_fp(), context::function(), indexof(), ite(), lambda(), last_indexof(), max(), min(), nand(), nor(), operator!=(), operator&(), operator&&(), operator*(), operator+(), operator-(), operator/(), operator<(), operator<=(), operator==(), operator>(), operator>=(), operator^(), operator|(), operator||(), par_and_then(), prefixof(), range(), re_diff(), context::recdef(), context::recfun(), select(), set_intersect(), set_union(), sqrt(), store(), suffixof(), context::user_propagate_function(), when(), and xnor().
◆ concat() [1/2]
Definition at line 2380 of file z3++.h.
2384 Z3_ast _args[2] = { a, b };
2388 Z3_ast _args[2] = { a, b };
2394 a.ctx().check_error();
2395 return expr(a.ctx(), r);
Referenced by operator+().
◆ concat() [2/2]
Definition at line 2398 of file z3++.h.
2400 assert(args.size() > 0);
2401 if (args.size() == 1) {
2404 context& ctx = args[0].ctx();
2405 array<Z3_ast> _args(args);
2413 r = _args[args.size()-1];
2414 for (
unsigned i = args.size()-1; i > 0; ) {
2421 return expr(ctx, r);
◆ cond()
Definition at line 3255 of file z3++.h.
3259 return tactic(t1.ctx(), r);
◆ const_array()
◆ distinct()
Definition at line 2371 of file z3++.h.
2372 assert(args.size() > 0);
2373 context& ctx = args[0].ctx();
2374 array<Z3_ast> _args(args);
2377 return expr(ctx, r);
◆ empty()
Definition at line 3738 of file z3++.h.
3741 return expr(s.ctx(), r);
◆ empty_set()
◆ eq()
bool z3::eq |
( |
ast const & |
a, |
|
|
ast const & |
b |
|
) |
| |
|
inline |
◆ exists() [1/5]
Definition at line 2273 of file z3++.h.
2275 Z3_app vars[] = {(Z3_app) x};
2276 Z3_ast r =
Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error();
return expr(b.ctx(), r);
◆ exists() [2/5]
Definition at line 2278 of file z3++.h.
2280 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2281 Z3_ast r =
Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error();
return expr(b.ctx(), r);
◆ exists() [3/5]
Definition at line 2283 of file z3++.h.
2285 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2286 Z3_ast r =
Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error();
return expr(b.ctx(), r);
◆ exists() [4/5]
Definition at line 2288 of file z3++.h.
2290 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2291 Z3_ast r =
Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error();
return expr(b.ctx(), r);
◆ exists() [5/5]
Definition at line 2293 of file z3++.h.
2294 array<Z3_app> vars(xs);
2295 Z3_ast r =
Z3_mk_exists_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error();
return expr(b.ctx(), r);
◆ fail_if()
Definition at line 3244 of file z3++.h.
3247 return tactic(p.ctx(), r);
◆ fma()
Definition at line 1955 of file z3++.h.
1957 assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
1960 return expr(a.ctx(), r);
◆ forall() [1/5]
Definition at line 2249 of file z3++.h.
2251 Z3_app vars[] = {(Z3_app) x};
2252 Z3_ast r =
Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error();
return expr(b.ctx(), r);
◆ forall() [2/5]
Definition at line 2254 of file z3++.h.
2256 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2257 Z3_ast r =
Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error();
return expr(b.ctx(), r);
◆ forall() [3/5]
Definition at line 2259 of file z3++.h.
2261 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2262 Z3_ast r =
Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error();
return expr(b.ctx(), r);
◆ forall() [4/5]
Definition at line 2264 of file z3++.h.
2266 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2267 Z3_ast r =
Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error();
return expr(b.ctx(), r);
◆ forall() [5/5]
Definition at line 2269 of file z3++.h.
2270 array<Z3_app> vars(xs);
2271 Z3_ast r =
Z3_mk_forall_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error();
return expr(b.ctx(), r);
◆ fp_eq()
Definition at line 1946 of file z3++.h.
1951 return expr(a.ctx(), r);
◆ fpa_fp()
Definition at line 1963 of file z3++.h.
1965 assert(sgn.is_bv() && exp.is_bv() && sig.is_bv());
1968 return expr(sgn.ctx(), r);
◆ fpa_to_fpa()
Definition at line 1999 of file z3++.h.
2003 return expr(t.ctx(), r);
◆ fpa_to_sbv()
expr z3::fpa_to_sbv |
( |
expr const & |
t, |
|
|
unsigned |
sz |
|
) |
| |
|
inline |
Definition at line 1971 of file z3++.h.
1975 return expr(t.ctx(), r);
◆ fpa_to_ubv()
expr z3::fpa_to_ubv |
( |
expr const & |
t, |
|
|
unsigned |
sz |
|
) |
| |
|
inline |
Definition at line 1978 of file z3++.h.
1982 return expr(t.ctx(), r);
◆ full_set()
◆ function() [1/9]
◆ function() [2/9]
◆ function() [3/9]
◆ function() [4/9]
◆ function() [5/9]
func_decl z3::function |
( |
char const * |
name, |
|
|
sort const & |
domain, |
|
|
sort const & |
range |
|
) |
| |
|
inline |
◆ function() [6/9]
◆ function() [7/9]
func_decl z3::function |
( |
char const * |
name, |
|
|
unsigned |
arity, |
|
|
sort const * |
domain, |
|
|
sort const & |
range |
|
) |
| |
|
inline |
◆ function() [8/9]
◆ function() [9/9]
◆ implies() [1/3]
expr z3::implies |
( |
bool |
a, |
|
|
expr const & |
b |
|
) |
| |
|
inline |
Definition at line 1560 of file z3++.h.
1560 {
return implies(b.ctx().bool_val(a), b); }
◆ implies() [2/3]
expr z3::implies |
( |
expr const & |
a, |
|
|
bool |
b |
|
) |
| |
|
inline |
Definition at line 1559 of file z3++.h.
1559 {
return implies(a, a.ctx().bool_val(b)); }
◆ implies() [3/3]
Definition at line 1555 of file z3++.h.
1556 assert(a.is_bool() && b.is_bool());
Referenced by implies().
◆ in_re()
◆ indexof()
Definition at line 3755 of file z3++.h.
3759 return expr(s.ctx(), r);
◆ int2bv()
expr z3::int2bv |
( |
unsigned |
n, |
|
|
expr const & |
a |
|
) |
| |
|
inline |
Definition at line 2158 of file z3++.h.
2158 { Z3_ast r =
Z3_mk_int2bv(a.ctx(), n, a); a.check_error();
return expr(a.ctx(), r); }
◆ is_int()
◆ ite()
Create the if-then-else expression ite(c, t, e)
- Precondition
- c.is_bool()
Definition at line 2018 of file z3++.h.
2020 assert(c.is_bool());
2023 return expr(c.ctx(), r);
◆ lambda() [1/5]
Definition at line 2297 of file z3++.h.
2299 Z3_app vars[] = {(Z3_app) x};
2300 Z3_ast r =
Z3_mk_lambda_const(b.ctx(), 1, vars, b); b.check_error();
return expr(b.ctx(), r);
◆ lambda() [2/5]
Definition at line 2302 of file z3++.h.
2304 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2305 Z3_ast r =
Z3_mk_lambda_const(b.ctx(), 2, vars, b); b.check_error();
return expr(b.ctx(), r);
◆ lambda() [3/5]
Definition at line 2307 of file z3++.h.
2309 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2310 Z3_ast r =
Z3_mk_lambda_const(b.ctx(), 3, vars, b); b.check_error();
return expr(b.ctx(), r);
◆ lambda() [4/5]
Definition at line 2312 of file z3++.h.
2314 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2315 Z3_ast r =
Z3_mk_lambda_const(b.ctx(), 4, vars, b); b.check_error();
return expr(b.ctx(), r);
◆ lambda() [5/5]
Definition at line 2317 of file z3++.h.
2318 array<Z3_app> vars(xs);
2319 Z3_ast r =
Z3_mk_lambda_const(b.ctx(), vars.size(), vars.ptr(), b); b.check_error();
return expr(b.ctx(), r);
◆ last_indexof()
expr z3::last_indexof |
( |
expr const & |
s, |
|
|
expr const & |
substr |
|
) |
| |
|
inline |
Definition at line 3761 of file z3++.h.
3765 return expr(s.ctx(), r);
◆ linear_order()
◆ lshr() [1/3]
logic shift right operator for bitvectors
Definition at line 2138 of file z3++.h.
Referenced by lshr().
◆ lshr() [2/3]
Definition at line 2139 of file z3++.h.
2139 {
return lshr(a, a.ctx().num_val(b, a.get_sort())); }
◆ lshr() [3/3]
Definition at line 2140 of file z3++.h.
2140 {
return lshr(b.ctx().num_val(a, b.get_sort()), b); }
◆ max()
◆ min()
Definition at line 1877 of file z3++.h.
1883 else if (a.is_bv()) {
1890 return expr(a.ctx(), r);
◆ mk_and()
Definition at line 2430 of file z3++.h.
2431 array<Z3_ast> _args(args);
2432 Z3_ast r =
Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2434 return expr(args.ctx(), r);
◆ mk_or()
Definition at line 2424 of file z3++.h.
2425 array<Z3_ast> _args(args);
2426 Z3_ast r =
Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2428 return expr(args.ctx(), r);
◆ mk_xor()
Definition at line 2436 of file z3++.h.
2438 return args.ctx().bool_val(
false);
2440 for (
unsigned i = 1; i < args.size(); ++i)
◆ mod() [1/3]
◆ mod() [2/3]
Definition at line 1575 of file z3++.h.
1575 {
return mod(a, a.ctx().num_val(b, a.get_sort())); }
◆ mod() [3/3]
Definition at line 1576 of file z3++.h.
1576 {
return mod(b.ctx().num_val(a, b.get_sort()), b); }
◆ nand()
◆ nor()
◆ operator!() [1/2]
◆ operator!() [2/2]
Definition at line 3078 of file z3++.h.
3079 Z3_probe r =
Z3_probe_not(p.ctx(), p); p.check_error();
return probe(p.ctx(), r);
◆ operator!=() [1/5]
Definition at line 1653 of file z3++.h.
1653 { assert(b.is_fpa());
return b.ctx().fpa_val(a) != b; }
◆ operator!=() [2/5]
Definition at line 1652 of file z3++.h.
1652 { assert(a.is_fpa());
return a != a.ctx().fpa_val(b); }
◆ operator!=() [3/5]
Definition at line 1643 of file z3++.h.
1645 Z3_ast args[2] = { a, b };
1648 return expr(a.ctx(), r);
◆ operator!=() [4/5]
Definition at line 1650 of file z3++.h.
1650 { assert(a.is_arith() || a.is_bv() || a.is_fpa());
return a != a.ctx().num_val(b, a.get_sort()); }
◆ operator!=() [5/5]
Definition at line 1651 of file z3++.h.
1651 { assert(b.is_arith() || b.is_bv() || b.is_fpa());
return b.ctx().num_val(a, b.get_sort()) != b; }
◆ operator%() [1/3]
Definition at line 1578 of file z3++.h.
1578 {
return mod(a, b); }
◆ operator%() [2/3]
expr z3::operator% |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
inline |
Definition at line 1579 of file z3++.h.
1579 {
return mod(a, b); }
◆ operator%() [3/3]
expr z3::operator% |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
inline |
Definition at line 1580 of file z3++.h.
1580 {
return mod(a, b); }
◆ operator&() [1/4]
◆ operator&() [2/4]
expr z3::operator& |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
inline |
Definition at line 1863 of file z3++.h.
1863 {
return a & a.ctx().num_val(b, a.get_sort()); }
◆ operator&() [3/4]
expr z3::operator& |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
inline |
Definition at line 1864 of file z3++.h.
1864 {
return b.ctx().num_val(a, b.get_sort()) & b; }
◆ operator&() [4/4]
Definition at line 2959 of file z3++.h.
2963 return tactic(t1.ctx(), r);
◆ operator&&() [1/4]
expr z3::operator&& |
( |
bool |
a, |
|
|
expr const & |
b |
|
) |
| |
|
inline |
- Precondition
- b.is_bool()
Definition at line 1617 of file z3++.h.
1617 {
return b.ctx().bool_val(a) && b; }
◆ operator&&() [2/4]
expr z3::operator&& |
( |
expr const & |
a, |
|
|
bool |
b |
|
) |
| |
|
inline |
- Precondition
- a.is_bool()
Definition at line 1616 of file z3++.h.
1616 {
return a && a.ctx().bool_val(b); }
◆ operator&&() [3/4]
- Precondition
- a.is_bool()
-
b.is_bool()
Definition at line 1607 of file z3++.h.
1609 assert(a.is_bool() && b.is_bool());
1610 Z3_ast args[2] = { a, b };
1613 return expr(a.ctx(), r);
◆ operator&&() [4/4]
◆ operator*() [1/3]
Definition at line 1685 of file z3++.h.
1688 if (a.is_arith() && b.is_arith()) {
1689 Z3_ast args[2] = { a, b };
1692 else if (a.is_bv() && b.is_bv()) {
1695 else if (a.is_fpa() && b.is_fpa()) {
1696 r =
Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1703 return expr(a.ctx(), r);
◆ operator*() [2/3]
expr z3::operator* |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
inline |
Definition at line 1705 of file z3++.h.
1705 {
return a * a.ctx().num_val(b, a.get_sort()); }
◆ operator*() [3/3]
expr z3::operator* |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
inline |
Definition at line 1706 of file z3++.h.
1706 {
return b.ctx().num_val(a, b.get_sort()) * b; }
◆ operator+() [1/3]
Definition at line 1655 of file z3++.h.
1658 if (a.is_arith() && b.is_arith()) {
1659 Z3_ast args[2] = { a, b };
1662 else if (a.is_bv() && b.is_bv()) {
1665 else if (a.is_seq() && b.is_seq()) {
1668 else if (a.is_re() && b.is_re()) {
1669 Z3_ast _args[2] = { a, b };
1672 else if (a.is_fpa() && b.is_fpa()) {
1673 r =
Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1680 return expr(a.ctx(), r);
◆ operator+() [2/3]
expr z3::operator+ |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
inline |
Definition at line 1682 of file z3++.h.
1682 {
return a + a.ctx().num_val(b, a.get_sort()); }
◆ operator+() [3/3]
expr z3::operator+ |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
inline |
Definition at line 1683 of file z3++.h.
1683 {
return b.ctx().num_val(a, b.get_sort()) + b; }
◆ operator-() [1/4]
Definition at line 1751 of file z3++.h.
1756 else if (a.is_bv()) {
1759 else if (a.is_fpa()) {
1767 return expr(a.ctx(), r);
◆ operator-() [2/4]
Definition at line 1770 of file z3++.h.
1773 if (a.is_arith() && b.is_arith()) {
1774 Z3_ast args[2] = { a, b };
1777 else if (a.is_bv() && b.is_bv()) {
1780 else if (a.is_fpa() && b.is_fpa()) {
1781 r =
Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1788 return expr(a.ctx(), r);
◆ operator-() [3/4]
expr z3::operator- |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
inline |
Definition at line 1790 of file z3++.h.
1790 {
return a - a.ctx().num_val(b, a.get_sort()); }
◆ operator-() [4/4]
expr z3::operator- |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
inline |
Definition at line 1791 of file z3++.h.
1791 {
return b.ctx().num_val(a, b.get_sort()) - b; }
◆ operator/() [1/3]
Definition at line 1729 of file z3++.h.
1732 if (a.is_arith() && b.is_arith()) {
1735 else if (a.is_bv() && b.is_bv()) {
1738 else if (a.is_fpa() && b.is_fpa()) {
1739 r =
Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1746 return expr(a.ctx(), r);
◆ operator/() [2/3]
expr z3::operator/ |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
inline |
Definition at line 1748 of file z3++.h.
1748 {
return a / a.ctx().num_val(b, a.get_sort()); }
◆ operator/() [3/3]
expr z3::operator/ |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
inline |
Definition at line 1749 of file z3++.h.
1749 {
return b.ctx().num_val(a, b.get_sort()) / b; }
◆ operator<() [1/6]
probe z3::operator< |
( |
double |
p1, |
|
|
probe const & |
p2 |
|
) |
| |
|
inline |
Definition at line 3061 of file z3++.h.
3061 {
return probe(p2.ctx(), p1) < p2; }
◆ operator<() [2/6]
Definition at line 1818 of file z3++.h.
1821 if (a.is_arith() && b.is_arith()) {
1824 else if (a.is_bv() && b.is_bv()) {
1827 else if (a.is_fpa() && b.is_fpa()) {
1835 return expr(a.ctx(), r);
◆ operator<() [3/6]
expr z3::operator< |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
inline |
Definition at line 1837 of file z3++.h.
1837 {
return a < a.ctx().num_val(b, a.get_sort()); }
◆ operator<() [4/6]
expr z3::operator< |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
inline |
Definition at line 1838 of file z3++.h.
1838 {
return b.ctx().num_val(a, b.get_sort()) < b; }
◆ operator<() [5/6]
probe z3::operator< |
( |
probe const & |
p1, |
|
|
double |
p2 |
|
) |
| |
|
inline |
Definition at line 3060 of file z3++.h.
3060 {
return p1 < probe(p1.ctx(), p2); }
◆ operator<() [6/6]
◆ operator<<() [1/13]
std::ostream& z3::operator<< |
( |
std::ostream & |
out, |
|
|
apply_result const & |
r |
|
) |
| |
|
inline |
◆ operator<<() [2/13]
std::ostream& z3::operator<< |
( |
std::ostream & |
out, |
|
|
ast const & |
n |
|
) |
| |
|
inline |
◆ operator<<() [3/13]
std::ostream& z3::operator<< |
( |
std::ostream & |
out, |
|
|
check_result |
r |
|
) |
| |
|
inline |
Definition at line 2612 of file z3++.h.
2613 if (r ==
unsat) out <<
"unsat";
2614 else if (r ==
sat) out <<
"sat";
2615 else out <<
"unknown";
◆ operator<<() [4/13]
std::ostream& z3::operator<< |
( |
std::ostream & |
out, |
|
|
exception const & |
e |
|
) |
| |
|
inline |
Definition at line 94 of file z3++.h.
94 { out << e.msg();
return out; }
◆ operator<<() [5/13]
std::ostream& z3::operator<< |
( |
std::ostream & |
out, |
|
|
fixedpoint const & |
f |
|
) |
| |
|
inline |
◆ operator<<() [6/13]
std::ostream& z3::operator<< |
( |
std::ostream & |
out, |
|
|
goal const & |
g |
|
) |
| |
|
inline |
◆ operator<<() [7/13]
std::ostream& z3::operator<< |
( |
std::ostream & |
out, |
|
|
model const & |
m |
|
) |
| |
|
inline |
◆ operator<<() [8/13]
std::ostream& z3::operator<< |
( |
std::ostream & |
out, |
|
|
optimize const & |
s |
|
) |
| |
|
inline |
◆ operator<<() [9/13]
std::ostream& z3::operator<< |
( |
std::ostream & |
out, |
|
|
param_descrs const & |
d |
|
) |
| |
|
inline |
Definition at line 477 of file z3++.h.
477 {
return out << d.to_string(); }
◆ operator<<() [10/13]
std::ostream& z3::operator<< |
( |
std::ostream & |
out, |
|
|
params const & |
p |
|
) |
| |
|
inline |
◆ operator<<() [11/13]
std::ostream& z3::operator<< |
( |
std::ostream & |
out, |
|
|
solver const & |
s |
|
) |
| |
|
inline |
◆ operator<<() [12/13]
std::ostream& z3::operator<< |
( |
std::ostream & |
out, |
|
|
stats const & |
s |
|
) |
| |
|
inline |
◆ operator<<() [13/13]
std::ostream& z3::operator<< |
( |
std::ostream & |
out, |
|
|
symbol const & |
s |
|
) |
| |
|
inline |
Definition at line 446 of file z3++.h.
448 out <<
"k!" << s.to_int();
◆ operator<=() [1/6]
probe z3::operator<= |
( |
double |
p1, |
|
|
probe const & |
p2 |
|
) |
| |
|
inline |
Definition at line 3051 of file z3++.h.
3051 {
return probe(p2.ctx(), p1) <= p2; }
◆ operator<=() [2/6]
Definition at line 1793 of file z3++.h.
1796 if (a.is_arith() && b.is_arith()) {
1799 else if (a.is_bv() && b.is_bv()) {
1802 else if (a.is_fpa() && b.is_fpa()) {
1810 return expr(a.ctx(), r);
◆ operator<=() [3/6]
expr z3::operator<= |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
inline |
Definition at line 1812 of file z3++.h.
1812 {
return a <= a.ctx().num_val(b, a.get_sort()); }
◆ operator<=() [4/6]
expr z3::operator<= |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
inline |
Definition at line 1813 of file z3++.h.
1813 {
return b.ctx().num_val(a, b.get_sort()) <= b; }
◆ operator<=() [5/6]
probe z3::operator<= |
( |
probe const & |
p1, |
|
|
double |
p2 |
|
) |
| |
|
inline |
Definition at line 3050 of file z3++.h.
3050 {
return p1 <= probe(p1.ctx(), p2); }
◆ operator<=() [6/6]
◆ operator==() [1/8]
expr z3::operator== |
( |
double |
a, |
|
|
expr const & |
b |
|
) |
| |
|
inline |
Definition at line 1641 of file z3++.h.
1641 { assert(b.is_fpa());
return b.ctx().fpa_val(a) == b; }
◆ operator==() [2/8]
probe z3::operator== |
( |
double |
p1, |
|
|
probe const & |
p2 |
|
) |
| |
|
inline |
Definition at line 3071 of file z3++.h.
3071 {
return probe(p2.ctx(), p1) == p2; }
◆ operator==() [3/8]
expr z3::operator== |
( |
expr const & |
a, |
|
|
double |
b |
|
) |
| |
|
inline |
Definition at line 1640 of file z3++.h.
1640 { assert(a.is_fpa());
return a == a.ctx().fpa_val(b); }
◆ operator==() [4/8]
Definition at line 1632 of file z3++.h.
1634 Z3_ast r =
Z3_mk_eq(a.ctx(), a, b);
1636 return expr(a.ctx(), r);
◆ operator==() [5/8]
expr z3::operator== |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
inline |
Definition at line 1638 of file z3++.h.
1638 { assert(a.is_arith() || a.is_bv() || a.is_fpa());
return a == a.ctx().num_val(b, a.get_sort()); }
◆ operator==() [6/8]
expr z3::operator== |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
inline |
Definition at line 1639 of file z3++.h.
1639 { assert(b.is_arith() || b.is_bv() || b.is_fpa());
return b.ctx().num_val(a, b.get_sort()) == b; }
◆ operator==() [7/8]
probe z3::operator== |
( |
probe const & |
p1, |
|
|
double |
p2 |
|
) |
| |
|
inline |
Definition at line 3070 of file z3++.h.
3070 {
return p1 == probe(p1.ctx(), p2); }
◆ operator==() [8/8]
◆ operator>() [1/6]
probe z3::operator> |
( |
double |
p1, |
|
|
probe const & |
p2 |
|
) |
| |
|
inline |
Definition at line 3066 of file z3++.h.
3066 {
return probe(p2.ctx(), p1) > p2; }
◆ operator>() [2/6]
Definition at line 1840 of file z3++.h.
1843 if (a.is_arith() && b.is_arith()) {
1846 else if (a.is_bv() && b.is_bv()) {
1849 else if (a.is_fpa() && b.is_fpa()) {
1857 return expr(a.ctx(), r);
◆ operator>() [3/6]
expr z3::operator> |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
inline |
Definition at line 1859 of file z3++.h.
1859 {
return a > a.ctx().num_val(b, a.get_sort()); }
◆ operator>() [4/6]
expr z3::operator> |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
inline |
Definition at line 1860 of file z3++.h.
1860 {
return b.ctx().num_val(a, b.get_sort()) > b; }
◆ operator>() [5/6]
probe z3::operator> |
( |
probe const & |
p1, |
|
|
double |
p2 |
|
) |
| |
|
inline |
Definition at line 3065 of file z3++.h.
3065 {
return p1 > probe(p1.ctx(), p2); }
◆ operator>() [6/6]
◆ operator>=() [1/6]
probe z3::operator>= |
( |
double |
p1, |
|
|
probe const & |
p2 |
|
) |
| |
|
inline |
Definition at line 3056 of file z3++.h.
3056 {
return probe(p2.ctx(), p1) >= p2; }
◆ operator>=() [2/6]
Definition at line 1709 of file z3++.h.
1712 if (a.is_arith() && b.is_arith()) {
1715 else if (a.is_bv() && b.is_bv()) {
1718 else if (a.is_fpa() && b.is_fpa()) {
1726 return expr(a.ctx(), r);
◆ operator>=() [3/6]
expr z3::operator>= |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
inline |
Definition at line 1815 of file z3++.h.
1815 {
return a >= a.ctx().num_val(b, a.get_sort()); }
◆ operator>=() [4/6]
expr z3::operator>= |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
inline |
Definition at line 1816 of file z3++.h.
1816 {
return b.ctx().num_val(a, b.get_sort()) >= b; }
◆ operator>=() [5/6]
probe z3::operator>= |
( |
probe const & |
p1, |
|
|
double |
p2 |
|
) |
| |
|
inline |
Definition at line 3055 of file z3++.h.
3055 {
return p1 >= probe(p1.ctx(), p2); }
◆ operator>=() [6/6]
◆ operator^() [1/3]
◆ operator^() [2/3]
expr z3::operator^ |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
inline |
Definition at line 1867 of file z3++.h.
1867 {
return a ^ a.ctx().num_val(b, a.get_sort()); }
◆ operator^() [3/3]
expr z3::operator^ |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
inline |
Definition at line 1868 of file z3++.h.
1868 {
return b.ctx().num_val(a, b.get_sort()) ^ b; }
◆ operator|() [1/4]
◆ operator|() [2/4]
expr z3::operator| |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
inline |
Definition at line 1871 of file z3++.h.
1871 {
return a | a.ctx().num_val(b, a.get_sort()); }
◆ operator|() [3/4]
expr z3::operator| |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
inline |
Definition at line 1872 of file z3++.h.
1872 {
return b.ctx().num_val(a, b.get_sort()) | b; }
◆ operator|() [4/4]
Definition at line 2966 of file z3++.h.
2970 return tactic(t1.ctx(), r);
◆ operator||() [1/4]
expr z3::operator|| |
( |
bool |
a, |
|
|
expr const & |
b |
|
) |
| |
|
inline |
- Precondition
- b.is_bool()
Definition at line 1630 of file z3++.h.
1630 {
return b.ctx().bool_val(a) || b; }
◆ operator||() [2/4]
expr z3::operator|| |
( |
expr const & |
a, |
|
|
bool |
b |
|
) |
| |
|
inline |
- Precondition
- a.is_bool()
Definition at line 1628 of file z3++.h.
1628 {
return a || a.ctx().bool_val(b); }
◆ operator||() [3/4]
- Precondition
- a.is_bool()
-
b.is_bool()
Definition at line 1619 of file z3++.h.
1621 assert(a.is_bool() && b.is_bool());
1622 Z3_ast args[2] = { a, b };
1623 Z3_ast r =
Z3_mk_or(a.ctx(), 2, args);
1625 return expr(a.ctx(), r);
◆ operator||() [4/4]
◆ operator~()
Definition at line 1953 of file z3++.h.
1953 { Z3_ast r =
Z3_mk_bvnot(a.ctx(), a);
return expr(a.ctx(), r); }
◆ option()
◆ par_and_then()
Definition at line 2998 of file z3++.h.
3002 return tactic(t1.ctx(), r);
◆ par_or()
Definition at line 2989 of file z3++.h.
2991 Z3_THROW(exception(
"a non-zero number of tactics need to be passed to par_or"));
2993 array<Z3_tactic> buffer(n);
2994 for (
unsigned i = 0; i < n; ++i) buffer[i] =
tactics[i];
◆ partial_order()
◆ pbeq()
Definition at line 2338 of file z3++.h.
2339 assert(es.size() > 0);
2340 context& ctx = es[0].ctx();
2341 array<Z3_ast> _es(es);
2342 Z3_ast r =
Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
2344 return expr(ctx, r);
◆ pbge()
Definition at line 2330 of file z3++.h.
2331 assert(es.size() > 0);
2332 context& ctx = es[0].ctx();
2333 array<Z3_ast> _es(es);
2334 Z3_ast r =
Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
2336 return expr(ctx, r);
◆ pble()
Definition at line 2322 of file z3++.h.
2323 assert(es.size() > 0);
2324 context& ctx = es[0].ctx();
2325 array<Z3_ast> _es(es);
2326 Z3_ast r =
Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
2328 return expr(ctx, r);
◆ piecewise_linear_order()
func_decl z3::piecewise_linear_order |
( |
sort const & |
a, |
|
|
unsigned |
index |
|
) |
| |
|
inline |
◆ plus()
◆ prefixof()
Definition at line 3749 of file z3++.h.
3753 return expr(a.ctx(), r);
◆ pw() [1/3]
◆ pw() [2/3]
Definition at line 1564 of file z3++.h.
1564 {
return pw(a, a.ctx().num_val(b, a.get_sort())); }
◆ pw() [3/3]
Definition at line 1565 of file z3++.h.
1565 {
return pw(b.ctx().num_val(a, b.get_sort()), b); }
◆ range()
Definition at line 3810 of file z3++.h.
3814 return expr(lo.ctx(), r);
Referenced by AstVector::__getitem__(), z3py::AndThen(), z3py::ArraySort(), Goal::as_expr(), ApplyResult::as_expr(), FuncEntry::as_list(), FuncInterp::as_list(), z3py::AtLeast(), z3py::BoolVector(), Solver::check(), Optimize::check(), ExprRef::children(), z3py::Concat(), Solver::consequences(), z3py::CreateDatatypes(), ModelRef::decls(), z3py::describe_probes(), z3py::DisjointSum(), z3py::EnumSort(), z3py::eq(), z3py::FreshFunction(), context::function(), z3py::Function(), function(), Statistics::get_key_value(), z3py::Intersect(), z3py::IntVector(), z3py::is_quantifier(), Statistics::keys(), z3py::Lambda(), Context::MkArrayConst(), Context::MkArraySort(), Context::MkConst(), Context::MkConstDecl(), Context::MkFreshConst(), Context::MkFreshConstDecl(), Context::MkFreshFuncDecl(), Context::MkFuncDecl(), Context::MkRecFuncDecl(), z3py::OrElse(), z3py::ParOr(), z3py::probes(), UserPropagateBase::propagate(), z3py::RealVarVector(), z3py::RealVector(), z3py::RecAddDefinition(), context::recfun(), recfun(), z3py::RecFunction(), z3py::set_default_fp_sort(), Fixedpoint::set_predicate_representation(), ModelRef::sorts(), z3py::substitute(), z3py::substitute_vars(), z3py::tactics(), Solver::to_smt2(), z3py::TupleSort(), z3py::Union(), z3py::Update(), and context::user_propagate_function().
◆ re_complement()
expr z3::re_complement |
( |
expr const & |
a | ) |
|
|
inline |
◆ re_diff()
Definition at line 3800 of file z3++.h.
3802 context& ctx = a.ctx();
3805 return expr(ctx, r);
◆ re_empty()
Definition at line 3782 of file z3++.h.
3785 return expr(s.ctx(), r);
◆ re_full()
Definition at line 3787 of file z3++.h.
3790 return expr(s.ctx(), r);
◆ re_intersect()
Definition at line 3792 of file z3++.h.
3793 assert(args.size() > 0);
3794 context& ctx = args[0].ctx();
3795 array<Z3_ast> _args(args);
3798 return expr(ctx, r);
◆ recfun() [1/4]
◆ recfun() [2/4]
◆ recfun() [3/4]
func_decl z3::recfun |
( |
char const * |
name, |
|
|
unsigned |
arity, |
|
|
sort const * |
domain, |
|
|
sort const & |
range |
|
) |
| |
|
inline |
◆ recfun() [4/4]
◆ rem() [1/3]
Definition at line 1583 of file z3++.h.
1584 if (a.is_fpa() && b.is_fpa()) {
Referenced by rem().
◆ rem() [2/3]
Definition at line 1590 of file z3++.h.
1590 {
return rem(a, a.ctx().num_val(b, a.get_sort())); }
◆ rem() [3/3]
Definition at line 1591 of file z3++.h.
1591 {
return rem(b.ctx().num_val(a, b.get_sort()), b); }
◆ repeat()
tactic z3::repeat |
( |
tactic const & |
t, |
|
|
unsigned |
max = UINT_MAX |
|
) |
| |
|
inline |
Definition at line 2973 of file z3++.h.
2976 return tactic(t.ctx(), r);
◆ reset_params()
void z3::reset_params |
( |
| ) |
|
|
inline |
◆ round_fpa_to_closest_integer()
expr z3::round_fpa_to_closest_integer |
( |
expr const & |
t | ) |
|
|
inline |
Definition at line 2006 of file z3++.h.
2010 return expr(t.ctx(), r);
◆ sbv_to_fpa()
Definition at line 1985 of file z3++.h.
1989 return expr(t.ctx(), r);
◆ select() [1/3]
◆ select() [2/3]
Definition at line 3637 of file z3++.h.
3639 array<Z3_ast> idxs(i);
3642 return expr(a.ctx(), r);
◆ select() [3/3]
expr z3::select |
( |
expr const & |
a, |
|
|
int |
i |
|
) |
| |
|
inline |
Definition at line 3634 of file z3++.h.
3635 return select(a, a.ctx().num_val(i, a.get_sort().array_domain()));
◆ set_add()
◆ set_complement()
expr z3::set_complement |
( |
expr const & |
a | ) |
|
|
inline |
◆ set_del()
◆ set_difference()
◆ set_intersect()
Definition at line 3710 of file z3++.h.
3712 Z3_ast es[2] = { a, b };
3715 return expr(a.ctx(), r);
◆ set_member()
◆ set_param() [1/3]
void z3::set_param |
( |
char const * |
param, |
|
|
bool |
value |
|
) |
| |
|
inline |
◆ set_param() [2/3]
void z3::set_param |
( |
char const * |
param, |
|
|
char const * |
value |
|
) |
| |
|
inline |
◆ set_param() [3/3]
void z3::set_param |
( |
char const * |
param, |
|
|
int |
value |
|
) |
| |
|
inline |
◆ set_subset()
◆ set_union()
Definition at line 3702 of file z3++.h.
3704 Z3_ast es[2] = { a, b };
3707 return expr(a.ctx(), r);
◆ sext()
expr z3::sext |
( |
expr const & |
a, |
|
|
unsigned |
i |
|
) |
| |
|
inline |
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 2192 of file z3++.h.
◆ sge() [1/3]
signed greater than or equal to operator for bitvectors.
Definition at line 2065 of file z3++.h.
Referenced by sge().
◆ sge() [2/3]
Definition at line 2066 of file z3++.h.
2066 {
return sge(a, a.ctx().num_val(b, a.get_sort())); }
◆ sge() [3/3]
Definition at line 2067 of file z3++.h.
2067 {
return sge(b.ctx().num_val(a, b.get_sort()), b); }
◆ sgt() [1/3]
signed greater than operator for bitvectors.
Definition at line 2071 of file z3++.h.
Referenced by sgt().
◆ sgt() [2/3]
Definition at line 2072 of file z3++.h.
2072 {
return sgt(a, a.ctx().num_val(b, a.get_sort())); }
◆ sgt() [3/3]
Definition at line 2073 of file z3++.h.
2073 {
return sgt(b.ctx().num_val(a, b.get_sort()), b); }
◆ shl() [1/3]
shift left operator for bitvectors
Definition at line 2131 of file z3++.h.
Referenced by shl().
◆ shl() [2/3]
Definition at line 2132 of file z3++.h.
2132 {
return shl(a, a.ctx().num_val(b, a.get_sort())); }
◆ shl() [3/3]
Definition at line 2133 of file z3++.h.
2133 {
return shl(b.ctx().num_val(a, b.get_sort()), b); }
◆ sle() [1/3]
signed less than or equal to operator for bitvectors.
Definition at line 2053 of file z3++.h.
Referenced by sle().
◆ sle() [2/3]
Definition at line 2054 of file z3++.h.
2054 {
return sle(a, a.ctx().num_val(b, a.get_sort())); }
◆ sle() [3/3]
Definition at line 2055 of file z3++.h.
2055 {
return sle(b.ctx().num_val(a, b.get_sort()), b); }
◆ slt() [1/3]
signed less than operator for bitvectors.
Definition at line 2059 of file z3++.h.
Referenced by slt().
◆ slt() [2/3]
Definition at line 2060 of file z3++.h.
2060 {
return slt(a, a.ctx().num_val(b, a.get_sort())); }
◆ slt() [3/3]
Definition at line 2061 of file z3++.h.
2061 {
return slt(b.ctx().num_val(a, b.get_sort()), b); }
◆ smod() [1/3]
signed modulus operator for bitvectors
Definition at line 2117 of file z3++.h.
Referenced by smod().
◆ smod() [2/3]
Definition at line 2118 of file z3++.h.
2118 {
return smod(a, a.ctx().num_val(b, a.get_sort())); }
◆ smod() [3/3]
Definition at line 2119 of file z3++.h.
2119 {
return smod(b.ctx().num_val(a, b.get_sort()), b); }
◆ sqrt()
Definition at line 1939 of file z3++.h.
1944 return expr(a.ctx(), r);
◆ srem() [1/3]
signed remainder operator for bitvectors
Definition at line 2110 of file z3++.h.
Referenced by srem().
◆ srem() [2/3]
Definition at line 2111 of file z3++.h.
2111 {
return srem(a, a.ctx().num_val(b, a.get_sort())); }
◆ srem() [3/3]
Definition at line 2112 of file z3++.h.
2112 {
return srem(b.ctx().num_val(a, b.get_sort()), b); }
◆ star()
◆ store() [1/5]
Definition at line 3645 of file z3++.h.
3649 return expr(a.ctx(), r);
Referenced by store().
◆ store() [2/5]
Definition at line 3653 of file z3++.h.
3653 {
return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
◆ store() [3/5]
Definition at line 3657 of file z3++.h.
3659 array<Z3_ast> idxs(i);
3660 Z3_ast r =
Z3_mk_store_n(a.ctx(), a, idxs.size(), idxs.ptr(), v);
3662 return expr(a.ctx(), r);
◆ store() [4/5]
Definition at line 3652 of file z3++.h.
3652 {
return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), v); }
◆ store() [5/5]
expr z3::store |
( |
expr const & |
a, |
|
|
int |
i, |
|
|
int |
v |
|
) |
| |
|
inline |
Definition at line 3654 of file z3++.h.
3655 return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
◆ suffixof()
Definition at line 3743 of file z3++.h.
3747 return expr(a.ctx(), r);
◆ sum()
Definition at line 2362 of file z3++.h.
2363 assert(args.size() > 0);
2364 context& ctx = args[0].ctx();
2365 array<Z3_ast> _args(args);
2366 Z3_ast r =
Z3_mk_add(ctx, _args.size(), _args.ptr());
2368 return expr(ctx, r);
◆ to_check_result()
◆ to_expr()
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 2031 of file z3++.h.
Referenced by ashr(), lshr(), sext(), sge(), sgt(), shl(), sle(), slt(), smod(), srem(), udiv(), uge(), ugt(), ule(), ult(), urem(), and zext().
◆ to_func_decl()
◆ to_re()
◆ to_real()
Definition at line 3585 of file z3++.h.
3585 { Z3_ast r =
Z3_mk_int2real(a.ctx(), a); a.check_error();
return expr(a.ctx(), r); }
◆ to_sort()
◆ tree_order()
◆ try_for()
Definition at line 2984 of file z3++.h.
2987 return tactic(t.ctx(), r);
◆ ubv_to_fpa()
Definition at line 1992 of file z3++.h.
1996 return expr(t.ctx(), r);
◆ udiv() [1/3]
unsigned division operator for bitvectors.
Definition at line 2103 of file z3++.h.
Referenced by udiv().
◆ udiv() [2/3]
Definition at line 2104 of file z3++.h.
2104 {
return udiv(a, a.ctx().num_val(b, a.get_sort())); }
◆ udiv() [3/3]
Definition at line 2105 of file z3++.h.
2105 {
return udiv(b.ctx().num_val(a, b.get_sort()), b); }
◆ uge() [1/3]
unsigned greater than or equal to operator for bitvectors.
Definition at line 2091 of file z3++.h.
Referenced by uge().
◆ uge() [2/3]
Definition at line 2092 of file z3++.h.
2092 {
return uge(a, a.ctx().num_val(b, a.get_sort())); }
◆ uge() [3/3]
Definition at line 2093 of file z3++.h.
2093 {
return uge(b.ctx().num_val(a, b.get_sort()), b); }
◆ ugt() [1/3]
unsigned greater than operator for bitvectors.
Definition at line 2097 of file z3++.h.
Referenced by ugt().
◆ ugt() [2/3]
Definition at line 2098 of file z3++.h.
2098 {
return ugt(a, a.ctx().num_val(b, a.get_sort())); }
◆ ugt() [3/3]
Definition at line 2099 of file z3++.h.
2099 {
return ugt(b.ctx().num_val(a, b.get_sort()), b); }
◆ ule() [1/3]
unsigned less than or equal to operator for bitvectors.
Definition at line 2079 of file z3++.h.
Referenced by ule().
◆ ule() [2/3]
Definition at line 2080 of file z3++.h.
2080 {
return ule(a, a.ctx().num_val(b, a.get_sort())); }
◆ ule() [3/3]
Definition at line 2081 of file z3++.h.
2081 {
return ule(b.ctx().num_val(a, b.get_sort()), b); }
◆ ult() [1/3]
unsigned less than operator for bitvectors.
Definition at line 2085 of file z3++.h.
Referenced by ult().
◆ ult() [2/3]
Definition at line 2086 of file z3++.h.
2086 {
return ult(a, a.ctx().num_val(b, a.get_sort())); }
◆ ult() [3/3]
Definition at line 2087 of file z3++.h.
2087 {
return ult(b.ctx().num_val(a, b.get_sort()), b); }
◆ urem() [1/3]
unsigned reminder operator for bitvectors
Definition at line 2124 of file z3++.h.
Referenced by urem().
◆ urem() [2/3]
Definition at line 2125 of file z3++.h.
2125 {
return urem(a, a.ctx().num_val(b, a.get_sort())); }
◆ urem() [3/3]
Definition at line 2126 of file z3++.h.
2126 {
return urem(b.ctx().num_val(a, b.get_sort()), b); }
◆ when()
Definition at line 3249 of file z3++.h.
3253 return tactic(t.ctx(), r);
◆ with()
Definition at line 2979 of file z3++.h.
2982 return tactic(t.ctx(), r);
◆ xnor()
◆ zext()
expr z3::zext |
( |
expr const & |
a, |
|
|
unsigned |
i |
|
) |
| |
|
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 2152 of file z3++.h.
Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than.
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)
Create the empty set.
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.
Z3_ast Z3_API Z3_mk_re_diff(Z3_context c, Z3_ast re1, Z3_ast re2)
Create the difference of regular expressions.
Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig)
Create an expression of FloatingPoint sort from three bit-vector expressions.
Z3_tactic Z3_API Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal if the probe p evaluates to true, and t2 if p evaluat...
Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned division.
Z3_tactic Z3_API Z3_tactic_or_else(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that first applies t1 to a given goal, if it fails then returns the result of t2 appl...
Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m)
Convert the given model into a string.
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
Compare terms.
expr sgt(int a, expr const &b)
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.
void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value)
Set a global (or module) parameter. This setting is shared by all Z3 contexts.
Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 rem arg2.
Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2)
Minimum of floating-point numbers.
Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1)
Create an n bit bit-vector from the integer argument t1.
expr smod(int a, expr const &b)
Z3_probe Z3_API Z3_probe_gt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than the value retur...
Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort.
Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1)
Coerce an integer to a real.
Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v)
Array update.
Z3_probe Z3_API Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned ...
Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[])
Create the intersection of the regular languages.
#define _Z3_MK_BIN_(a, b, binop)
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
Z3_ast Z3_API Z3_mk_fpa_to_ubv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)
Conversion of a floating-point term into an unsigned bit-vector.
expr pw(int a, expr const &b)
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point subtraction.
Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.
Z3_ast Z3_API Z3_mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re)
Check if seq is in the language generated by the regular expression re.
Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
Z3_ast Z3_API Z3_mk_zero_ext(Z3_context c, unsigned i, Z3_ast t1)
Extend the given bit-vector with zeros to the (unsigned) equivalent bit-vector of size m+i,...
Z3_probe Z3_API Z3_probe_and(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when p1 and p2 evaluates to true.
Z3_string Z3_API Z3_params_to_string(Z3_context c, Z3_params p)
Convert a parameter set into a string. This function is mainly used for printing the contents of a pa...
Z3_ast Z3_API Z3_mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than or equal to.
Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2)
Arithmetic shift right.
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.
Z3_ast Z3_API Z3_mk_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s)
Check if suffix is a suffix of s.
expr range(expr const &lo, expr const &hi)
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
Z3_tactic Z3_API Z3_tactic_par_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1....
Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point addition.
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
Z3_tactic Z3_API Z3_tactic_repeat(Z3_context c, Z3_tactic t, unsigned max)
Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of...
Z3_probe Z3_API Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than or equal to the...
Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] - ... - args[num_args - 1].
expr rem(int a, expr const &b)
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.
Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than or equal to.
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point remainder.
Z3_ast Z3_API Z3_mk_lambda_const(Z3_context c, unsigned num_bound, Z3_app const bound[], Z3_ast body)
Create a lambda expression using a list of constants that form the set of bound variables.
Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i)
Array read. The argument a is the array and i is the index of the array that gets read.
expr shl(int a, expr const &b)
Z3_string Z3_API Z3_apply_result_to_string(Z3_context c, Z3_apply_result r)
Convert the Z3_apply_result object returned by Z3_tactic_apply into a string.
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.
Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than.
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem)
Remove an element to a set.
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t1)
Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast t1, bool is_signed)
Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is t...
expr sge(int a, expr const &b)
Z3_probe Z3_API Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the va...
Z3_ast Z3_API Z3_mk_select_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const *idxs)
n-ary Array read. The argument a is the array and idxs are the indices of the array that gets read.
Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].
Z3_ast Z3_API Z3_mk_set_intersect(Z3_context c, unsigned num_args, Z3_ast const args[])
Take the intersection of a list of sets.
Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nor.
Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point equality.
Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1)
Take conjunction of bits in vector, return vector of length 1.
#define _Z3_MK_UN_(a, mkun)
Z3_ast Z3_API Z3_mk_sign_ext(Z3_context c, unsigned i, Z3_ast t1)
Sign-extend of the given bit-vector to the (signed) equivalent bit-vector of size m+i,...
expr slt(int a, expr const &b)
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
expr ugt(int a, expr const &b)
Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.
Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].
Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2)
Maximum of floating-point numbers.
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
Z3_probe Z3_API Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned...
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Check for subsetness of sets.
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
Z3_tactic Z3_API Z3_tactic_fail_if(Z3_context c, Z3_probe p)
Return a tactic that fails if the probe p evaluates to false.
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.
expr lshr(int a, expr const &b)
Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than or equal to.
Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem)
Add an element to a set.
bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.
expr ashr(int a, expr const &b)
expr srem(int a, expr const &b)
Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re)
Create the complement of the regular language re.
Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set)
Check for set membership.
expr ule(int a, expr const &b)
Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re)
Create an universal regular expression of sort re.
expr concat(expr_vector const &args)
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.
Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re)
Create the regular language re+.
expr ult(int a, expr const &b)
Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re)
Create the regular language [re].
Z3_func_decl Z3_API Z3_mk_piecewise_linear_order(Z3_context c, Z3_sort a, unsigned id)
create a piecewise linear ordering relation over signature a and index id.
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].
Z3_ast Z3_API Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows dividend).
Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p)
Return a probe that evaluates to "true" when p does not evaluate to true.
Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.
Z3_tactic Z3_API Z3_tactic_using_params(Z3_context c, Z3_tactic t, Z3_params p)
Return a tactic that applies t using the given set of parameters.
void Z3_API Z3_global_param_reset_all(void)
Restore the value of all global (and module) parameters. This command will not affect already created...
expr sle(int a, expr const &b)
expr udiv(int a, expr const &b)
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
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...
expr select(expr const &a, int i)
Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned remainder.
Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[])
Create the union of the regular languages.
Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re)
Create an empty regular expression of sort re.
Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables.
Z3_tactic Z3_API Z3_tactic_par_or(Z3_context c, unsigned num, Z3_tactic const ts[])
Return a tactic that applies the given tactics in parallel.
Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.
Z3_tactic Z3_API Z3_tactic_try_for(Z3_context c, Z3_tactic t, unsigned ms)
Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms mil...
Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point multiplication.
Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].
expr implies(bool a, expr const &b)
expr store(expr const &a, expr_vector const &i, expr const &v)
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
Z3_func_decl Z3_API Z3_mk_partial_order(Z3_context c, Z3_sort a, unsigned id)
create a partial ordering relation over signature a and index id.
expr urem(int a, expr const &b)
Z3_ast Z3_API Z3_mk_exists_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Similar to Z3_mk_forall_const.
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than.
Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f)
Create array with the same interpretation as a function. The array satisfies the property (f x) = (se...
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq)
Create a regular expression that accepts the sequence seq.
Z3_probe Z3_API Z3_probe_or(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when p1 or p2 evaluates to true.
Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
expr max(expr const &a, expr const &b)
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.
Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflo...
Z3_ast Z3_API Z3_mk_set_union(Z3_context c, unsigned num_args, Z3_ast const args[])
Take the union of a list of sets.
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
Z3_ast Z3_API Z3_mk_seq_last_index(Z3_context c, Z3_ast, Z3_ast substr)
Return the last occurrence of substr in s. If s does not contain substr, then the value is -1,...
Z3_func_decl Z3_API Z3_mk_linear_order(Z3_context c, Z3_sort a, unsigned id)
create a linear ordering relation over signature a. The relation is identified by the index id.
Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than.
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.
void check_context(object const &a, object const &b)
Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)
Shift left.
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
Z3_func_decl Z3_API Z3_mk_tree_order(Z3_context c, Z3_sort a, unsigned id)
create a tree ordering relation over signature a identified using index id.
expr uge(int a, expr const &b)
Z3_ast Z3_API Z3_mk_store_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const *idxs, Z3_ast v)
n-ary Array update.
Z3_tactic Z3_API Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1.
Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg)
Take the complement of a set.
Z3_ast Z3_API Z3_mk_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s)
Check if prefix is a prefix of s.
Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2)
Logical shift right.
Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.
Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi)
Create the range regular expression over two sequences of length 1.
Z3_ast Z3_API Z3_mk_fpa_round_to_integral(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point roundToIntegral. Rounds a floating-point number to the closest integer,...
#define MK_EXPR2(_fn, _arg1, _arg2)
Z3_string Z3_API Z3_fixedpoint_to_string(Z3_context c, Z3_fixedpoint f, unsigned num_queries, Z3_ast queries[])
Print the current rules and background axioms as a string.
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
func_decl to_func_decl(context &c, Z3_func_decl f)
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Take the set difference between two sets.
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point division.
#define MK_EXPR1(_fn, _arg)
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows divisor).
Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re)
Create the regular language re*.
Z3_ast Z3_API Z3_mk_fpa_fma(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Floating-point fused multiply-add.
Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g)
Convert a goal into a string.
Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
expr mod(int a, expr const &b)
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq)
Create an empty sequence of the sequence sort seq.
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
Z3_tactic Z3_API Z3_tactic_when(Z3_context c, Z3_probe p, Z3_tactic t)
Return a tactic that applies t to a given goal is the probe p evaluates to true. If p evaluates to fa...
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)
Create the constant array.
Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than or equal.
Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than.
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.
Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset)
Return index of first occurrence of substr in s starting from offset offset. If s does not contain su...
Z3_ast Z3_API Z3_mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)
Conversion of a floating-point term into a signed bit-vector.
Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1)
Take disjunction of bits in vector, return vector of length 1.
Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 xor t2.
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than or equal.
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point square root.