Z3
 
Loading...
Searching...
No Matches
Data Structures | Namespaces | Macros | Typedefs | Enumerations | Functions
z3++.h File Reference

Go to the source code of this file.

Data Structures

class  exception
 Exception used to sign API usage errors. More...
 
class  config
 Z3 global configuration object. More...
 
class  context
 A Context manages all other Z3 objects, global configuration options, etc. More...
 
class  array< T >
 
class  object
 
class  symbol
 
class  param_descrs
 
class  params
 
class  ast
 
class  ast_vector_tpl< T >
 
class  ast_vector_tpl< T >::iterator
 
class  sort
 A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort. More...
 
class  func_decl
 Function declaration (aka function definition). It is the signature of interpreted and uninterpreted functions in Z3. The basic building block in Z3 is the function application. More...
 
class  expr
 A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort Boolean. Every expression has a sort. More...
 
class  expr::iterator
 
class  cast_ast< ast >
 
class  cast_ast< expr >
 
class  cast_ast< sort >
 
class  cast_ast< func_decl >
 
class  func_entry
 
class  func_interp
 
class  model
 
struct  model::translate
 
class  stats
 
class  parameter
 class for auxiliary parameters associated with func_decl The class is initialized with a func_decl or application expression and an index The accessor get_expr, get_sort, ... is available depending on the value of kind(). The caller is responsible to check that the kind of the parameter aligns with the call (get_expr etc). More...
 
class  solver
 
struct  solver::simple
 
struct  solver::translate
 
class  solver::cube_iterator
 
class  solver::cube_generator
 
class  goal
 
class  apply_result
 
class  tactic
 
class  simplifier
 
class  probe
 
class  optimize
 
class  optimize::handle
 
class  fixedpoint
 
class  constructor_list
 
class  constructors
 
class  on_clause
 
class  user_propagator_base
 

Namespaces

namespace  z3
 Z3 C++ namespace.
 

Macros

#define Z3_THROW(x)   {}
 
#define _Z3_MK_BIN_(a, b, binop)
 
#define _Z3_MK_UN_(a, mkun)
 
#define MK_EXPR1(_fn, _arg)
 
#define MK_EXPR2(_fn, _arg1, _arg2)
 

Typedefs

typedef ast_vector_tpl< astast_vector
 
typedef ast_vector_tpl< exprexpr_vector
 
typedef ast_vector_tpl< sortsort_vector
 
typedef ast_vector_tpl< func_declfunc_decl_vector
 
typedef std::function< void(expr const &proof, expr_vector const &clause)> on_clause_eh_t
 

Enumerations

enum  check_result { unsat , sat , unknown }
 
enum  rounding_mode {
  RNA , RNE , RTP , RTN ,
  RTZ
}
 

Functions

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
 
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)
 
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.
 
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.
 
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.
 
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.
 
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.
 
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.
 
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.
 
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.
 
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.
 
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.
 
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
 
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
 
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
 
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
 
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
 
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
 
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.
 
expr bv2int (expr const &a, bool is_signed)
 bit-vector and integer conversions.
 
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
 
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.
 
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)
 
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)
 

Macro Definition Documentation

◆ _Z3_MK_BIN_

#define _Z3_MK_BIN_ (   a,
  b,
  binop 
)
Value:
check_context(a, b); \
Z3_ast r = binop(a.ctx(), a, b); \
a.check_error(); \
return expr(a.ctx(), r); \

Definition at line 1621 of file z3++.h.

1627 {
1628 assert(a.is_bool() && b.is_bool());
1630 }
1631 inline expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); }
1632 inline expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); }
1633
1634
1635 inline expr pw(expr const & a, expr const & b) { _Z3_MK_BIN_(a, b, Z3_mk_power); }
1636 inline expr pw(expr const & a, int b) { return pw(a, a.ctx().num_val(b, a.get_sort())); }
1637 inline expr pw(int a, expr const & b) { return pw(b.ctx().num_val(a, b.get_sort()), b); }
1638
1639 inline expr mod(expr const& a, expr const& b) {
1640 if (a.is_bv()) {
1641 _Z3_MK_BIN_(a, b, Z3_mk_bvsmod);
1642 }
1643 else {
1644 _Z3_MK_BIN_(a, b, Z3_mk_mod);
1645 }
1646 }
1647 inline expr mod(expr const & a, int b) { return mod(a, a.ctx().num_val(b, a.get_sort())); }
1648 inline expr mod(int a, expr const & b) { return mod(b.ctx().num_val(a, b.get_sort()), b); }
1649
1650 inline expr operator%(expr const& a, expr const& b) { return mod(a, b); }
1651 inline expr operator%(expr const& a, int b) { return mod(a, b); }
1652 inline expr operator%(int a, expr const& b) { return mod(a, b); }
1653
1654
1655 inline expr rem(expr const& a, expr const& b) {
1656 if (a.is_fpa() && b.is_fpa()) {
1658 } else {
1659 _Z3_MK_BIN_(a, b, Z3_mk_rem);
1660 }
1661 }
1662 inline expr rem(expr const & a, int b) { return rem(a, a.ctx().num_val(b, a.get_sort())); }
1663 inline expr rem(int a, expr const & b) { return rem(b.ctx().num_val(a, b.get_sort()), b); }
1664
1665#undef _Z3_MK_BIN_
1666
1667#define _Z3_MK_UN_(a, mkun) \
1668 Z3_ast r = mkun(a.ctx(), a); \
1669 a.check_error(); \
1670 return expr(a.ctx(), r); \
1671
1672
1673 inline expr operator!(expr const & a) { assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); }
1674
1675 inline expr is_int(expr const& e) { _Z3_MK_UN_(e, Z3_mk_is_int); }
1676
1677#undef _Z3_MK_UN_
1678
1679 inline expr operator&&(expr const & a, expr const & b) {
1680 check_context(a, b);
1681 assert(a.is_bool() && b.is_bool());
1682 Z3_ast args[2] = { a, b };
1683 Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1684 a.check_error();
1685 return expr(a.ctx(), r);
1686 }
1687
1688 inline expr operator&&(expr const & a, bool b) { return a && a.ctx().bool_val(b); }
1689 inline expr operator&&(bool a, expr const & b) { return b.ctx().bool_val(a) && b; }
1690
1691 inline expr operator||(expr const & a, expr const & b) {
1692 check_context(a, b);
1693 assert(a.is_bool() && b.is_bool());
1694 Z3_ast args[2] = { a, b };
1695 Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1696 a.check_error();
1697 return expr(a.ctx(), r);
1698 }
1699
1700 inline expr operator||(expr const & a, bool b) { return a || a.ctx().bool_val(b); }
1701
1702 inline expr operator||(bool a, expr const & b) { return b.ctx().bool_val(a) || b; }
1703
1704 inline expr operator==(expr const & a, expr const & b) {
1705 check_context(a, b);
1706 Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1707 a.check_error();
1708 return expr(a.ctx(), r);
1709 }
1710 inline expr operator==(expr const & a, int b) { assert(a.is_arith() || a.is_bv() || a.is_fpa()); return a == a.ctx().num_val(b, a.get_sort()); }
1711 inline expr operator==(int a, expr const & b) { assert(b.is_arith() || b.is_bv() || b.is_fpa()); return b.ctx().num_val(a, b.get_sort()) == b; }
1712 inline expr operator==(expr const & a, double b) { assert(a.is_fpa()); return a == a.ctx().fpa_val(b); }
1713 inline expr operator==(double a, expr const & b) { assert(b.is_fpa()); return b.ctx().fpa_val(a) == b; }
1714
1715 inline expr operator!=(expr const & a, expr const & b) {
1716 check_context(a, b);
1717 Z3_ast args[2] = { a, b };
1718 Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1719 a.check_error();
1720 return expr(a.ctx(), r);
1721 }
1722 inline expr operator!=(expr const & a, int b) { assert(a.is_arith() || a.is_bv() || a.is_fpa()); return a != a.ctx().num_val(b, a.get_sort()); }
1723 inline expr operator!=(int a, expr const & b) { assert(b.is_arith() || b.is_bv() || b.is_fpa()); return b.ctx().num_val(a, b.get_sort()) != b; }
1724 inline expr operator!=(expr const & a, double b) { assert(a.is_fpa()); return a != a.ctx().fpa_val(b); }
1725 inline expr operator!=(double a, expr const & b) { assert(b.is_fpa()); return b.ctx().fpa_val(a) != b; }
1726
1727 inline expr operator+(expr const & a, expr const & b) {
1728 check_context(a, b);
1729 Z3_ast r = 0;
1730 if (a.is_arith() && b.is_arith()) {
1731 Z3_ast args[2] = { a, b };
1732 r = Z3_mk_add(a.ctx(), 2, args);
1733 }
1734 else if (a.is_bv() && b.is_bv()) {
1735 r = Z3_mk_bvadd(a.ctx(), a, b);
1736 }
1737 else if (a.is_seq() && b.is_seq()) {
1738 return concat(a, b);
1739 }
1740 else if (a.is_re() && b.is_re()) {
1741 Z3_ast _args[2] = { a, b };
1742 r = Z3_mk_re_union(a.ctx(), 2, _args);
1743 }
1744 else if (a.is_fpa() && b.is_fpa()) {
1745 r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1746 }
1747 else {
1748 // operator is not supported by given arguments.
1749 assert(false);
1750 }
1751 a.check_error();
1752 return expr(a.ctx(), r);
1753 }
1754 inline expr operator+(expr const & a, int b) { return a + a.ctx().num_val(b, a.get_sort()); }
1755 inline expr operator+(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) + b; }
1756
1757 inline expr operator*(expr const & a, expr const & b) {
1758 check_context(a, b);
1759 Z3_ast r = 0;
1760 if (a.is_arith() && b.is_arith()) {
1761 Z3_ast args[2] = { a, b };
1762 r = Z3_mk_mul(a.ctx(), 2, args);
1763 }
1764 else if (a.is_bv() && b.is_bv()) {
1765 r = Z3_mk_bvmul(a.ctx(), a, b);
1766 }
1767 else if (a.is_fpa() && b.is_fpa()) {
1768 r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1769 }
1770 else {
1771 // operator is not supported by given arguments.
1772 assert(false);
1773 }
1774 a.check_error();
1775 return expr(a.ctx(), r);
1776 }
1777 inline expr operator*(expr const & a, int b) { return a * a.ctx().num_val(b, a.get_sort()); }
1778 inline expr operator*(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) * b; }
1779
1780
1781 inline expr operator>=(expr const & a, expr const & b) {
1782 check_context(a, b);
1783 Z3_ast r = 0;
1784 if (a.is_arith() && b.is_arith()) {
1785 r = Z3_mk_ge(a.ctx(), a, b);
1786 }
1787 else if (a.is_bv() && b.is_bv()) {
1788 r = Z3_mk_bvsge(a.ctx(), a, b);
1789 }
1790 else if (a.is_fpa() && b.is_fpa()) {
1791 r = Z3_mk_fpa_geq(a.ctx(), a, b);
1792 }
1793 else {
1794 // operator is not supported by given arguments.
1795 assert(false);
1796 }
1797 a.check_error();
1798 return expr(a.ctx(), r);
1799 }
1800
1801 inline expr operator/(expr const & a, expr const & b) {
1802 check_context(a, b);
1803 Z3_ast r = 0;
1804 if (a.is_arith() && b.is_arith()) {
1805 r = Z3_mk_div(a.ctx(), a, b);
1806 }
1807 else if (a.is_bv() && b.is_bv()) {
1808 r = Z3_mk_bvsdiv(a.ctx(), a, b);
1809 }
1810 else if (a.is_fpa() && b.is_fpa()) {
1811 r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1812 }
1813 else {
1814 // operator is not supported by given arguments.
1815 assert(false);
1816 }
1817 a.check_error();
1818 return expr(a.ctx(), r);
1819 }
1820 inline expr operator/(expr const & a, int b) { return a / a.ctx().num_val(b, a.get_sort()); }
1821 inline expr operator/(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) / b; }
1822
1823 inline expr operator-(expr const & a) {
1824 Z3_ast r = 0;
1825 if (a.is_arith()) {
1826 r = Z3_mk_unary_minus(a.ctx(), a);
1827 }
1828 else if (a.is_bv()) {
1829 r = Z3_mk_bvneg(a.ctx(), a);
1830 }
1831 else if (a.is_fpa()) {
1832 r = Z3_mk_fpa_neg(a.ctx(), a);
1833 }
1834 else {
1835 // operator is not supported by given arguments.
1836 assert(false);
1837 }
1838 a.check_error();
1839 return expr(a.ctx(), r);
1840 }
1841
1842 inline expr operator-(expr const & a, expr const & b) {
1843 check_context(a, b);
1844 Z3_ast r = 0;
1845 if (a.is_arith() && b.is_arith()) {
1846 Z3_ast args[2] = { a, b };
1847 r = Z3_mk_sub(a.ctx(), 2, args);
1848 }
1849 else if (a.is_bv() && b.is_bv()) {
1850 r = Z3_mk_bvsub(a.ctx(), a, b);
1851 }
1852 else if (a.is_fpa() && b.is_fpa()) {
1853 r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1854 }
1855 else {
1856 // operator is not supported by given arguments.
1857 assert(false);
1858 }
1859 a.check_error();
1860 return expr(a.ctx(), r);
1861 }
1862 inline expr operator-(expr const & a, int b) { return a - a.ctx().num_val(b, a.get_sort()); }
1863 inline expr operator-(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) - b; }
1864
1865 inline expr operator<=(expr const & a, expr const & b) {
1866 check_context(a, b);
1867 Z3_ast r = 0;
1868 if (a.is_arith() && b.is_arith()) {
1869 r = Z3_mk_le(a.ctx(), a, b);
1870 }
1871 else if (a.is_bv() && b.is_bv()) {
1872 r = Z3_mk_bvsle(a.ctx(), a, b);
1873 }
1874 else if (a.is_fpa() && b.is_fpa()) {
1875 r = Z3_mk_fpa_leq(a.ctx(), a, b);
1876 }
1877 else {
1878 // operator is not supported by given arguments.
1879 assert(false);
1880 }
1881 a.check_error();
1882 return expr(a.ctx(), r);
1883 }
1884 inline expr operator<=(expr const & a, int b) { return a <= a.ctx().num_val(b, a.get_sort()); }
1885 inline expr operator<=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) <= b; }
1886
1887 inline expr operator>=(expr const & a, int b) { return a >= a.ctx().num_val(b, a.get_sort()); }
1888 inline expr operator>=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) >= b; }
1889
1890 inline expr operator<(expr const & a, expr const & b) {
1891 check_context(a, b);
1892 Z3_ast r = 0;
1893 if (a.is_arith() && b.is_arith()) {
1894 r = Z3_mk_lt(a.ctx(), a, b);
1895 }
1896 else if (a.is_bv() && b.is_bv()) {
1897 r = Z3_mk_bvslt(a.ctx(), a, b);
1898 }
1899 else if (a.is_fpa() && b.is_fpa()) {
1900 r = Z3_mk_fpa_lt(a.ctx(), a, b);
1901 }
1902 else {
1903 // operator is not supported by given arguments.
1904 assert(false);
1905 }
1906 a.check_error();
1907 return expr(a.ctx(), r);
1908 }
1909 inline expr operator<(expr const & a, int b) { return a < a.ctx().num_val(b, a.get_sort()); }
1910 inline expr operator<(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) < b; }
1911
1912 inline expr operator>(expr const & a, expr const & b) {
1913 check_context(a, b);
1914 Z3_ast r = 0;
1915 if (a.is_arith() && b.is_arith()) {
1916 r = Z3_mk_gt(a.ctx(), a, b);
1917 }
1918 else if (a.is_bv() && b.is_bv()) {
1919 r = Z3_mk_bvsgt(a.ctx(), a, b);
1920 }
1921 else if (a.is_fpa() && b.is_fpa()) {
1922 r = Z3_mk_fpa_gt(a.ctx(), a, b);
1923 }
1924 else {
1925 // operator is not supported by given arguments.
1926 assert(false);
1927 }
1928 a.check_error();
1929 return expr(a.ctx(), r);
1930 }
1931 inline expr operator>(expr const & a, int b) { return a > a.ctx().num_val(b, a.get_sort()); }
1932 inline expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > b; }
1933
1934 inline expr operator&(expr const & a, expr const & b) { if (a.is_bool()) return a && b; check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
1935 inline expr operator&(expr const & a, int b) { return a & a.ctx().num_val(b, a.get_sort()); }
1936 inline expr operator&(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) & b; }
1937
1938 inline expr operator^(expr const & a, expr const & b) { check_context(a, b); Z3_ast r = a.is_bool() ? Z3_mk_xor(a.ctx(), a, b) : Z3_mk_bvxor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
1939 inline expr operator^(expr const & a, int b) { return a ^ a.ctx().num_val(b, a.get_sort()); }
1940 inline expr operator^(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) ^ b; }
1941
1942 inline expr operator|(expr const & a, expr const & b) { if (a.is_bool()) return a || b; check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
1943 inline expr operator|(expr const & a, int b) { return a | a.ctx().num_val(b, a.get_sort()); }
1944 inline expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; }
1945
1946 inline expr nand(expr const& a, expr const& b) { if (a.is_bool()) return !(a && b); check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
1947 inline expr nor(expr const& a, expr const& b) { if (a.is_bool()) return !(a || b); check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
1948 inline expr xnor(expr const& a, expr const& b) { if (a.is_bool()) return !(a ^ b); check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
1949 inline expr min(expr const& a, expr const& b) {
1950 check_context(a, b);
1951 Z3_ast r;
1952 if (a.is_arith()) {
1953 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
1954 }
1955 else if (a.is_bv()) {
1956 r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
1957 }
1958 else {
1959 assert(a.is_fpa());
1960 r = Z3_mk_fpa_min(a.ctx(), a, b);
1961 }
1962 a.check_error();
1963 return expr(a.ctx(), r);
1964 }
1965 inline expr max(expr const& a, expr const& b) {
1966 check_context(a, b);
1967 Z3_ast r;
1968 if (a.is_arith()) {
1969 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
1970 }
1971 else if (a.is_bv()) {
1972 r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
1973 }
1974 else {
1975 assert(a.is_fpa());
1976 r = Z3_mk_fpa_max(a.ctx(), a, b);
1977 }
1978 a.check_error();
1979 return expr(a.ctx(), r);
1980 }
1981 inline expr bvredor(expr const & a) {
1982 assert(a.is_bv());
1983 Z3_ast r = Z3_mk_bvredor(a.ctx(), a);
1984 a.check_error();
1985 return expr(a.ctx(), r);
1986 }
1987 inline expr bvredand(expr const & a) {
1988 assert(a.is_bv());
1989 Z3_ast r = Z3_mk_bvredand(a.ctx(), a);
1990 a.check_error();
1991 return expr(a.ctx(), r);
1992 }
1993 inline expr abs(expr const & a) {
1994 Z3_ast r;
1995 if (a.is_int()) {
1996 expr zero = a.ctx().int_val(0);
1997 expr ge = a >= zero;
1998 expr na = -a;
1999 r = Z3_mk_ite(a.ctx(), ge, a, na);
2000 }
2001 else if (a.is_real()) {
2002 expr zero = a.ctx().real_val(0);
2003 expr ge = a >= zero;
2004 expr na = -a;
2005 r = Z3_mk_ite(a.ctx(), ge, a, na);
2006 }
2007 else {
2008 r = Z3_mk_fpa_abs(a.ctx(), a);
2009 }
2010 a.check_error();
2011 return expr(a.ctx(), r);
2012 }
2013 inline expr sqrt(expr const & a, expr const& rm) {
2014 check_context(a, rm);
2015 assert(a.is_fpa());
2016 Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
2017 a.check_error();
2018 return expr(a.ctx(), r);
2019 }
2020 inline expr fp_eq(expr const & a, expr const & b) {
2021 check_context(a, b);
2022 assert(a.is_fpa());
2023 Z3_ast r = Z3_mk_fpa_eq(a.ctx(), a, b);
2024 a.check_error();
2025 return expr(a.ctx(), r);
2026 }
2027 inline expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
2028
2029 inline expr fma(expr const& a, expr const& b, expr const& c, expr const& rm) {
2030 check_context(a, b); check_context(a, c); check_context(a, rm);
2031 assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
2032 Z3_ast r = Z3_mk_fpa_fma(a.ctx(), rm, a, b, c);
2033 a.check_error();
2034 return expr(a.ctx(), r);
2035 }
2036
2037 inline expr fpa_fp(expr const& sgn, expr const& exp, expr const& sig) {
2038 check_context(sgn, exp); check_context(exp, sig);
2039 assert(sgn.is_bv() && exp.is_bv() && sig.is_bv());
2040 Z3_ast r = Z3_mk_fpa_fp(sgn.ctx(), sgn, exp, sig);
2041 sgn.check_error();
2042 return expr(sgn.ctx(), r);
2043 }
2044
2045 inline expr fpa_to_sbv(expr const& t, unsigned sz) {
2046 assert(t.is_fpa());
2047 Z3_ast r = Z3_mk_fpa_to_sbv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
2048 t.check_error();
2049 return expr(t.ctx(), r);
2050 }
2051
2052 inline expr fpa_to_ubv(expr const& t, unsigned sz) {
2053 assert(t.is_fpa());
2054 Z3_ast r = Z3_mk_fpa_to_ubv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
2055 t.check_error();
2056 return expr(t.ctx(), r);
2057 }
2058
2059 inline expr sbv_to_fpa(expr const& t, sort s) {
2060 assert(t.is_bv());
2061 Z3_ast r = Z3_mk_fpa_to_fp_signed(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2062 t.check_error();
2063 return expr(t.ctx(), r);
2064 }
2065
2066 inline expr ubv_to_fpa(expr const& t, sort s) {
2067 assert(t.is_bv());
2068 Z3_ast r = Z3_mk_fpa_to_fp_unsigned(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2069 t.check_error();
2070 return expr(t.ctx(), r);
2071 }
2072
2073 inline expr fpa_to_fpa(expr const& t, sort s) {
2074 assert(t.is_fpa());
2075 Z3_ast r = Z3_mk_fpa_to_fp_float(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2076 t.check_error();
2077 return expr(t.ctx(), r);
2078 }
2079
2080 inline expr round_fpa_to_closest_integer(expr const& t) {
2081 assert(t.is_fpa());
2082 Z3_ast r = Z3_mk_fpa_round_to_integral(t.ctx(), t.ctx().fpa_rounding_mode(), t);
2083 t.check_error();
2084 return expr(t.ctx(), r);
2085 }
2086
2092 inline expr ite(expr const & c, expr const & t, expr const & e) {
2093 check_context(c, t); check_context(c, e);
2094 assert(c.is_bool());
2095 Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
2096 c.check_error();
2097 return expr(c.ctx(), r);
2098 }
2099
2100
2105 inline expr to_expr(context & c, Z3_ast a) {
2106 c.check_error();
2107 assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
2109 Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
2111 return expr(c, a);
2112 }
2113
2114 inline sort to_sort(context & c, Z3_sort s) {
2115 c.check_error();
2116 return sort(c, s);
2117 }
2118
2119 inline func_decl to_func_decl(context & c, Z3_func_decl f) {
2120 c.check_error();
2121 return func_decl(c, f);
2122 }
2123
2127 inline expr sle(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsle(a.ctx(), a, b)); }
2128 inline expr sle(expr const & a, int b) { return sle(a, a.ctx().num_val(b, a.get_sort())); }
2129 inline expr sle(int a, expr const & b) { return sle(b.ctx().num_val(a, b.get_sort()), b); }
2133 inline expr slt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvslt(a.ctx(), a, b)); }
2134 inline expr slt(expr const & a, int b) { return slt(a, a.ctx().num_val(b, a.get_sort())); }
2135 inline expr slt(int a, expr const & b) { return slt(b.ctx().num_val(a, b.get_sort()), b); }
2139 inline expr sge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsge(a.ctx(), a, b)); }
2140 inline expr sge(expr const & a, int b) { return sge(a, a.ctx().num_val(b, a.get_sort())); }
2141 inline expr sge(int a, expr const & b) { return sge(b.ctx().num_val(a, b.get_sort()), b); }
2145 inline expr sgt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsgt(a.ctx(), a, b)); }
2146 inline expr sgt(expr const & a, int b) { return sgt(a, a.ctx().num_val(b, a.get_sort())); }
2147 inline expr sgt(int a, expr const & b) { return sgt(b.ctx().num_val(a, b.get_sort()), b); }
2148
2149
2153 inline expr ule(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
2154 inline expr ule(expr const & a, int b) { return ule(a, a.ctx().num_val(b, a.get_sort())); }
2155 inline expr ule(int a, expr const & b) { return ule(b.ctx().num_val(a, b.get_sort()), b); }
2159 inline expr ult(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }
2160 inline expr ult(expr const & a, int b) { return ult(a, a.ctx().num_val(b, a.get_sort())); }
2161 inline expr ult(int a, expr const & b) { return ult(b.ctx().num_val(a, b.get_sort()), b); }
2165 inline expr uge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }
2166 inline expr uge(expr const & a, int b) { return uge(a, a.ctx().num_val(b, a.get_sort())); }
2167 inline expr uge(int a, expr const & b) { return uge(b.ctx().num_val(a, b.get_sort()), b); }
2171 inline expr ugt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
2172 inline expr ugt(expr const & a, int b) { return ugt(a, a.ctx().num_val(b, a.get_sort())); }
2173 inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), b); }
2177 inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
2178 inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); }
2179 inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); }
2180
2184 inline expr srem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsrem(a.ctx(), a, b)); }
2185 inline expr srem(expr const & a, int b) { return srem(a, a.ctx().num_val(b, a.get_sort())); }
2186 inline expr srem(int a, expr const & b) { return srem(b.ctx().num_val(a, b.get_sort()), b); }
2187
2191 inline expr smod(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsmod(a.ctx(), a, b)); }
2192 inline expr smod(expr const & a, int b) { return smod(a, a.ctx().num_val(b, a.get_sort())); }
2193 inline expr smod(int a, expr const & b) { return smod(b.ctx().num_val(a, b.get_sort()), b); }
2194
2198 inline expr urem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvurem(a.ctx(), a, b)); }
2199 inline expr urem(expr const & a, int b) { return urem(a, a.ctx().num_val(b, a.get_sort())); }
2200 inline expr urem(int a, expr const & b) { return urem(b.ctx().num_val(a, b.get_sort()), b); }
2201
2205 inline expr shl(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvshl(a.ctx(), a, b)); }
2206 inline expr shl(expr const & a, int b) { return shl(a, a.ctx().num_val(b, a.get_sort())); }
2207 inline expr shl(int a, expr const & b) { return shl(b.ctx().num_val(a, b.get_sort()), b); }
2208
2212 inline expr lshr(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvlshr(a.ctx(), a, b)); }
2213 inline expr lshr(expr const & a, int b) { return lshr(a, a.ctx().num_val(b, a.get_sort())); }
2214 inline expr lshr(int a, expr const & b) { return lshr(b.ctx().num_val(a, b.get_sort()), b); }
2215
2219 inline expr ashr(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvashr(a.ctx(), a, b)); }
2220 inline expr ashr(expr const & a, int b) { return ashr(a, a.ctx().num_val(b, a.get_sort())); }
2221 inline expr ashr(int a, expr const & b) { return ashr(b.ctx().num_val(a, b.get_sort()), b); }
2222
2226 inline expr zext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_zero_ext(a.ctx(), i, a)); }
2227
2231 inline expr bv2int(expr const& a, bool is_signed) { Z3_ast r = Z3_mk_bv2int(a.ctx(), a, is_signed); a.check_error(); return expr(a.ctx(), r); }
2232 inline expr int2bv(unsigned n, expr const& a) { Z3_ast r = Z3_mk_int2bv(a.ctx(), n, a); a.check_error(); return expr(a.ctx(), r); }
2233
2237 inline expr bvadd_no_overflow(expr const& a, expr const& b, bool is_signed) {
2238 check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_overflow(a.ctx(), a, b, is_signed); a.check_error(); return expr(a.ctx(), r);
2239 }
2240 inline expr bvadd_no_underflow(expr const& a, expr const& b) {
2241 check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2242 }
2243 inline expr bvsub_no_overflow(expr const& a, expr const& b) {
2244 check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2245 }
2246 inline expr bvsub_no_underflow(expr const& a, expr const& b, bool is_signed) {
2247 check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_underflow(a.ctx(), a, b, is_signed); a.check_error(); return expr(a.ctx(), r);
2248 }
2249 inline expr bvsdiv_no_overflow(expr const& a, expr const& b) {
2250 check_context(a, b); Z3_ast r = Z3_mk_bvsdiv_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2251 }
2252 inline expr bvneg_no_overflow(expr const& a) {
2253 Z3_ast r = Z3_mk_bvneg_no_overflow(a.ctx(), a); a.check_error(); return expr(a.ctx(), r);
2254 }
2255 inline expr bvmul_no_overflow(expr const& a, expr const& b, bool is_signed) {
2256 check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_overflow(a.ctx(), a, b, is_signed); a.check_error(); return expr(a.ctx(), r);
2257 }
2258 inline expr bvmul_no_underflow(expr const& a, expr const& b) {
2259 check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2260 }
2261
2262
2266 inline expr sext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_sign_ext(a.ctx(), i, a)); }
2267
2268 inline func_decl linear_order(sort const& a, unsigned index) {
2269 return to_func_decl(a.ctx(), Z3_mk_linear_order(a.ctx(), a, index));
2270 }
2271 inline func_decl partial_order(sort const& a, unsigned index) {
2272 return to_func_decl(a.ctx(), Z3_mk_partial_order(a.ctx(), a, index));
2273 }
2274 inline func_decl piecewise_linear_order(sort const& a, unsigned index) {
2275 return to_func_decl(a.ctx(), Z3_mk_piecewise_linear_order(a.ctx(), a, index));
2276 }
2277 inline func_decl tree_order(sort const& a, unsigned index) {
2278 return to_func_decl(a.ctx(), Z3_mk_tree_order(a.ctx(), a, index));
2279 }
2280
2281 template<> class cast_ast<ast> {
2282 public:
2283 ast operator()(context & c, Z3_ast a) { return ast(c, a); }
2284 };
2285
2286 template<> class cast_ast<expr> {
2287 public:
2288 expr operator()(context & c, Z3_ast a) {
2289 assert(Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
2290 Z3_get_ast_kind(c, a) == Z3_APP_AST ||
2292 Z3_get_ast_kind(c, a) == Z3_VAR_AST);
2293 return expr(c, a);
2294 }
2295 };
2296
2297 template<> class cast_ast<sort> {
2298 public:
2299 sort operator()(context & c, Z3_ast a) {
2300 assert(Z3_get_ast_kind(c, a) == Z3_SORT_AST);
2301 return sort(c, reinterpret_cast<Z3_sort>(a));
2302 }
2303 };
2304
2305 template<> class cast_ast<func_decl> {
2306 public:
2307 func_decl operator()(context & c, Z3_ast a) {
2308 assert(Z3_get_ast_kind(c, a) == Z3_FUNC_DECL_AST);
2309 return func_decl(c, reinterpret_cast<Z3_func_decl>(a));
2310 }
2311 };
2312
2313 template<typename T>
2314 template<typename T2>
2315 array<T>::array(ast_vector_tpl<T2> const & v):m_array(new T[v.size()]), m_size(v.size()) {
2316 for (unsigned i = 0; i < m_size; i++) {
2317 m_array[i] = v[i];
2318 }
2319 }
2320
2321 // Basic functions for creating quantified formulas.
2322 // The C API should be used for creating quantifiers with patterns, weights, many variables, etc.
2323 inline expr forall(expr const & x, expr const & b) {
2324 check_context(x, b);
2325 Z3_app vars[] = {(Z3_app) x};
2326 Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2327 }
2328 inline expr forall(expr const & x1, expr const & x2, expr const & b) {
2329 check_context(x1, b); check_context(x2, b);
2330 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2331 Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2332 }
2333 inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
2334 check_context(x1, b); check_context(x2, b); check_context(x3, b);
2335 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2336 Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2337 }
2338 inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
2339 check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2340 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2341 Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2342 }
2343 inline expr forall(expr_vector const & xs, expr const & b) {
2344 array<Z3_app> vars(xs);
2345 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);
2346 }
2347 inline expr exists(expr const & x, expr const & b) {
2348 check_context(x, b);
2349 Z3_app vars[] = {(Z3_app) x};
2350 Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2351 }
2352 inline expr exists(expr const & x1, expr const & x2, expr const & b) {
2353 check_context(x1, b); check_context(x2, b);
2354 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2355 Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2356 }
2357 inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
2358 check_context(x1, b); check_context(x2, b); check_context(x3, b);
2359 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2360 Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2361 }
2362 inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
2363 check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2364 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2365 Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2366 }
2367 inline expr exists(expr_vector const & xs, expr const & b) {
2368 array<Z3_app> vars(xs);
2369 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);
2370 }
2371 inline expr lambda(expr const & x, expr const & b) {
2372 check_context(x, b);
2373 Z3_app vars[] = {(Z3_app) x};
2374 Z3_ast r = Z3_mk_lambda_const(b.ctx(), 1, vars, b); b.check_error(); return expr(b.ctx(), r);
2375 }
2376 inline expr lambda(expr const & x1, expr const & x2, expr const & b) {
2377 check_context(x1, b); check_context(x2, b);
2378 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2379 Z3_ast r = Z3_mk_lambda_const(b.ctx(), 2, vars, b); b.check_error(); return expr(b.ctx(), r);
2380 }
2381 inline expr lambda(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
2382 check_context(x1, b); check_context(x2, b); check_context(x3, b);
2383 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2384 Z3_ast r = Z3_mk_lambda_const(b.ctx(), 3, vars, b); b.check_error(); return expr(b.ctx(), r);
2385 }
2386 inline expr lambda(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
2387 check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2388 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2389 Z3_ast r = Z3_mk_lambda_const(b.ctx(), 4, vars, b); b.check_error(); return expr(b.ctx(), r);
2390 }
2391 inline expr lambda(expr_vector const & xs, expr const & b) {
2392 array<Z3_app> vars(xs);
2393 Z3_ast r = Z3_mk_lambda_const(b.ctx(), vars.size(), vars.ptr(), b); b.check_error(); return expr(b.ctx(), r);
2394 }
2395
2396 inline expr pble(expr_vector const& es, int const* coeffs, int bound) {
2397 assert(es.size() > 0);
2398 context& ctx = es[0u].ctx();
2399 array<Z3_ast> _es(es);
2400 Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
2401 ctx.check_error();
2402 return expr(ctx, r);
2403 }
2404 inline expr pbge(expr_vector const& es, int const* coeffs, int bound) {
2405 assert(es.size() > 0);
2406 context& ctx = es[0u].ctx();
2407 array<Z3_ast> _es(es);
2408 Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
2409 ctx.check_error();
2410 return expr(ctx, r);
2411 }
2412 inline expr pbeq(expr_vector const& es, int const* coeffs, int bound) {
2413 assert(es.size() > 0);
2414 context& ctx = es[0u].ctx();
2415 array<Z3_ast> _es(es);
2416 Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
2417 ctx.check_error();
2418 return expr(ctx, r);
2419 }
2420 inline expr atmost(expr_vector const& es, unsigned bound) {
2421 assert(es.size() > 0);
2422 context& ctx = es[0u].ctx();
2423 array<Z3_ast> _es(es);
2424 Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
2425 ctx.check_error();
2426 return expr(ctx, r);
2427 }
2428 inline expr atleast(expr_vector const& es, unsigned bound) {
2429 assert(es.size() > 0);
2430 context& ctx = es[0u].ctx();
2431 array<Z3_ast> _es(es);
2432 Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
2433 ctx.check_error();
2434 return expr(ctx, r);
2435 }
2436 inline expr sum(expr_vector const& args) {
2437 assert(args.size() > 0);
2438 context& ctx = args[0u].ctx();
2439 array<Z3_ast> _args(args);
2440 Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
2441 ctx.check_error();
2442 return expr(ctx, r);
2443 }
2444
2445 inline expr distinct(expr_vector const& args) {
2446 assert(args.size() > 0);
2447 context& ctx = args[0u].ctx();
2448 array<Z3_ast> _args(args);
2449 Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
2450 ctx.check_error();
2451 return expr(ctx, r);
2452 }
2453
2454 inline expr concat(expr const& a, expr const& b) {
2455 check_context(a, b);
2456 Z3_ast r;
2457 if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
2458 Z3_ast _args[2] = { a, b };
2459 r = Z3_mk_seq_concat(a.ctx(), 2, _args);
2460 }
2461 else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
2462 Z3_ast _args[2] = { a, b };
2463 r = Z3_mk_re_concat(a.ctx(), 2, _args);
2464 }
2465 else {
2466 r = Z3_mk_concat(a.ctx(), a, b);
2467 }
2468 a.ctx().check_error();
2469 return expr(a.ctx(), r);
2470 }
2471
2472 inline expr concat(expr_vector const& args) {
2473 Z3_ast r;
2474 assert(args.size() > 0);
2475 if (args.size() == 1) {
2476 return args[0u];
2477 }
2478 context& ctx = args[0u].ctx();
2479 array<Z3_ast> _args(args);
2480 if (Z3_is_seq_sort(ctx, args[0u].get_sort())) {
2481 r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
2482 }
2483 else if (Z3_is_re_sort(ctx, args[0u].get_sort())) {
2484 r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
2485 }
2486 else {
2487 r = _args[args.size()-1];
2488 for (unsigned i = args.size()-1; i > 0; ) {
2489 --i;
2490 r = Z3_mk_concat(ctx, _args[i], r);
2491 ctx.check_error();
2492 }
2493 }
2494 ctx.check_error();
2495 return expr(ctx, r);
2496 }
2497
2498 inline expr mk_or(expr_vector const& args) {
2499 array<Z3_ast> _args(args);
2500 Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2501 args.check_error();
2502 return expr(args.ctx(), r);
2503 }
2504 inline expr mk_and(expr_vector const& args) {
2505 array<Z3_ast> _args(args);
2506 Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2507 args.check_error();
2508 return expr(args.ctx(), r);
2509 }
2510 inline expr mk_xor(expr_vector const& args) {
2511 if (args.empty())
2512 return args.ctx().bool_val(false);
2513 expr r = args[0u];
2514 for (unsigned i = 1; i < args.size(); ++i)
2515 r = r ^ args[i];
2516 return r;
2517 }
2518
2519
2520 class func_entry : public object {
2521 Z3_func_entry m_entry;
2522 void init(Z3_func_entry e) {
2523 m_entry = e;
2524 Z3_func_entry_inc_ref(ctx(), m_entry);
2525 }
2526 public:
2527 func_entry(context & c, Z3_func_entry e):object(c) { init(e); }
2528 func_entry(func_entry const & s):object(s) { init(s.m_entry); }
2529 ~func_entry() { Z3_func_entry_dec_ref(ctx(), m_entry); }
2530 operator Z3_func_entry() const { return m_entry; }
2531 func_entry & operator=(func_entry const & s) {
2532 Z3_func_entry_inc_ref(s.ctx(), s.m_entry);
2533 Z3_func_entry_dec_ref(ctx(), m_entry);
2534 object::operator=(s);
2535 m_entry = s.m_entry;
2536 return *this;
2537 }
2538 expr value() const { Z3_ast r = Z3_func_entry_get_value(ctx(), m_entry); check_error(); return expr(ctx(), r); }
2539 unsigned num_args() const { unsigned r = Z3_func_entry_get_num_args(ctx(), m_entry); check_error(); return r; }
2540 expr arg(unsigned i) const { Z3_ast r = Z3_func_entry_get_arg(ctx(), m_entry, i); check_error(); return expr(ctx(), r); }
2541 };
2542
2543 class func_interp : public object {
2544 Z3_func_interp m_interp;
2545 void init(Z3_func_interp e) {
2546 m_interp = e;
2547 Z3_func_interp_inc_ref(ctx(), m_interp);
2548 }
2549 public:
2550 func_interp(context & c, Z3_func_interp e):object(c) { init(e); }
2551 func_interp(func_interp const & s):object(s) { init(s.m_interp); }
2552 ~func_interp() { Z3_func_interp_dec_ref(ctx(), m_interp); }
2553 operator Z3_func_interp() const { return m_interp; }
2554 func_interp & operator=(func_interp const & s) {
2555 Z3_func_interp_inc_ref(s.ctx(), s.m_interp);
2556 Z3_func_interp_dec_ref(ctx(), m_interp);
2557 object::operator=(s);
2558 m_interp = s.m_interp;
2559 return *this;
2560 }
2561 expr else_value() const { Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), r); }
2562 unsigned num_entries() const { unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }
2563 func_entry entry(unsigned i) const { Z3_func_entry e = Z3_func_interp_get_entry(ctx(), m_interp, i); check_error(); return func_entry(ctx(), e); }
2564 void add_entry(expr_vector const& args, expr& value) {
2565 Z3_func_interp_add_entry(ctx(), m_interp, args, value);
2566 check_error();
2567 }
2568 void set_else(expr& value) {
2569 Z3_func_interp_set_else(ctx(), m_interp, value);
2570 check_error();
2571 }
2572 };
2573
2574 class model : public object {
2575 Z3_model m_model;
2576 void init(Z3_model m) {
2577 m_model = m;
2578 Z3_model_inc_ref(ctx(), m);
2579 }
2580 public:
2581 struct translate {};
2582 model(context & c):object(c) { init(Z3_mk_model(c)); }
2583 model(context & c, Z3_model m):object(c) { init(m); }
2584 model(model const & s):object(s) { init(s.m_model); }
2585 model(model& src, context& dst, translate) : object(dst) { init(Z3_model_translate(src.ctx(), src, dst)); }
2586 ~model() { Z3_model_dec_ref(ctx(), m_model); }
2587 operator Z3_model() const { return m_model; }
2588 model & operator=(model const & s) {
2589 Z3_model_inc_ref(s.ctx(), s.m_model);
2590 Z3_model_dec_ref(ctx(), m_model);
2591 object::operator=(s);
2592 m_model = s.m_model;
2593 return *this;
2594 }
2595
2596 expr eval(expr const & n, bool model_completion=false) const {
2597 check_context(*this, n);
2598 Z3_ast r = 0;
2599 bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
2600 check_error();
2601 if (status == false && ctx().enable_exceptions())
2602 Z3_THROW(exception("failed to evaluate expression"));
2603 return expr(ctx(), r);
2604 }
2605
2606 unsigned num_consts() const { return Z3_model_get_num_consts(ctx(), m_model); }
2607 unsigned num_funcs() const { return Z3_model_get_num_funcs(ctx(), m_model); }
2608 func_decl get_const_decl(unsigned i) const { Z3_func_decl r = Z3_model_get_const_decl(ctx(), m_model, i); check_error(); return func_decl(ctx(), r); }
2609 func_decl get_func_decl(unsigned i) const { Z3_func_decl r = Z3_model_get_func_decl(ctx(), m_model, i); check_error(); return func_decl(ctx(), r); }
2610 unsigned size() const { return num_consts() + num_funcs(); }
2611 func_decl operator[](int i) const {
2612 assert(0 <= i);
2613 return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
2614 }
2615
2616 // returns interpretation of constant declaration c.
2617 // If c is not assigned any value in the model it returns
2618 // an expression with a null ast reference.
2619 expr get_const_interp(func_decl c) const {
2620 check_context(*this, c);
2621 Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);
2622 check_error();
2623 return expr(ctx(), r);
2624 }
2625 func_interp get_func_interp(func_decl f) const {
2626 check_context(*this, f);
2627 Z3_func_interp r = Z3_model_get_func_interp(ctx(), m_model, f);
2628 check_error();
2629 return func_interp(ctx(), r);
2630 }
2631
2632 // returns true iff the model contains an interpretation
2633 // for function f.
2634 bool has_interp(func_decl f) const {
2635 check_context(*this, f);
2636 return Z3_model_has_interp(ctx(), m_model, f);
2637 }
2638
2639 func_interp add_func_interp(func_decl& f, expr& else_val) {
2640 Z3_func_interp r = Z3_add_func_interp(ctx(), m_model, f, else_val);
2641 check_error();
2642 return func_interp(ctx(), r);
2643 }
2644
2645 void add_const_interp(func_decl& f, expr& value) {
2646 Z3_add_const_interp(ctx(), m_model, f, value);
2647 check_error();
2648 }
2649
2650 friend std::ostream & operator<<(std::ostream & out, model const & m);
2651
2652 std::string to_string() const { return m_model ? std::string(Z3_model_to_string(ctx(), m_model)) : "null"; }
2653 };
2654 inline std::ostream & operator<<(std::ostream & out, model const & m) { return out << m.to_string(); }
2655
2656 class stats : public object {
2657 Z3_stats m_stats;
2658 void init(Z3_stats e) {
2659 m_stats = e;
2660 Z3_stats_inc_ref(ctx(), m_stats);
2661 }
2662 public:
2663 stats(context & c):object(c), m_stats(0) {}
2664 stats(context & c, Z3_stats e):object(c) { init(e); }
2665 stats(stats const & s):object(s) { init(s.m_stats); }
2666 ~stats() { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); }
2667 operator Z3_stats() const { return m_stats; }
2668 stats & operator=(stats const & s) {
2669 Z3_stats_inc_ref(s.ctx(), s.m_stats);
2670 if (m_stats) Z3_stats_dec_ref(ctx(), m_stats);
2671 object::operator=(s);
2672 m_stats = s.m_stats;
2673 return *this;
2674 }
2675 unsigned size() const { return Z3_stats_size(ctx(), m_stats); }
2676 std::string key(unsigned i) const { Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; }
2677 bool is_uint(unsigned i) const { bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r; }
2678 bool is_double(unsigned i) const { bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r; }
2679 unsigned uint_value(unsigned i) const { unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; }
2680 double double_value(unsigned i) const { double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
2681 friend std::ostream & operator<<(std::ostream & out, stats const & s);
2682 };
2683 inline std::ostream & operator<<(std::ostream & out, stats const & s) { out << Z3_stats_to_string(s.ctx(), s); return out; }
2684
2685
2686 inline std::ostream & operator<<(std::ostream & out, check_result r) {
2687 if (r == unsat) out << "unsat";
2688 else if (r == sat) out << "sat";
2689 else out << "unknown";
2690 return out;
2691 }
2692
2703 class parameter {
2704 Z3_parameter_kind m_kind;
2705 func_decl m_decl;
2706 unsigned m_index;
2707 context& ctx() const { return m_decl.ctx(); }
2708 void check_error() const { ctx().check_error(); }
2709 public:
2710 parameter(func_decl const& d, unsigned idx) : m_decl(d), m_index(idx) {
2711 if (ctx().enable_exceptions() && idx >= d.num_parameters())
2712 Z3_THROW(exception("parameter index is out of bounds"));
2713 m_kind = Z3_get_decl_parameter_kind(ctx(), d, idx);
2714 }
2715 parameter(expr const& e, unsigned idx) : m_decl(e.decl()), m_index(idx) {
2716 if (ctx().enable_exceptions() && idx >= m_decl.num_parameters())
2717 Z3_THROW(exception("parameter index is out of bounds"));
2718 m_kind = Z3_get_decl_parameter_kind(ctx(), m_decl, idx);
2719 }
2720 Z3_parameter_kind kind() const { return m_kind; }
2721 expr get_expr() const { Z3_ast a = Z3_get_decl_ast_parameter(ctx(), m_decl, m_index); check_error(); return expr(ctx(), a); }
2722 sort get_sort() const { Z3_sort s = Z3_get_decl_sort_parameter(ctx(), m_decl, m_index); check_error(); return sort(ctx(), s); }
2723 func_decl get_decl() const { Z3_func_decl f = Z3_get_decl_func_decl_parameter(ctx(), m_decl, m_index); check_error(); return func_decl(ctx(), f); }
2724 symbol get_symbol() const { Z3_symbol s = Z3_get_decl_symbol_parameter(ctx(), m_decl, m_index); check_error(); return symbol(ctx(), s); }
2725 std::string get_rational() const { Z3_string s = Z3_get_decl_rational_parameter(ctx(), m_decl, m_index); check_error(); return s; }
2726 double get_double() const { double d = Z3_get_decl_double_parameter(ctx(), m_decl, m_index); check_error(); return d; }
2727 int get_int() const { int i = Z3_get_decl_int_parameter(ctx(), m_decl, m_index); check_error(); return i; }
2728 };
2729
2730
2731 class solver : public object {
2732 Z3_solver m_solver;
2733 void init(Z3_solver s) {
2734 m_solver = s;
2735 if (s)
2736 Z3_solver_inc_ref(ctx(), s);
2737 }
2738 public:
2739 struct simple {};
2740 struct translate {};
2741 solver(context & c):object(c) { init(Z3_mk_solver(c)); check_error(); }
2742 solver(context & c, simple):object(c) { init(Z3_mk_simple_solver(c)); check_error(); }
2743 solver(context & c, Z3_solver s):object(c) { init(s); }
2744 solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); check_error(); }
2745 solver(context & c, solver const& src, translate): object(c) { Z3_solver s = Z3_solver_translate(src.ctx(), src, c); check_error(); init(s); }
2746 solver(solver const & s):object(s) { init(s.m_solver); }
2747 solver(solver const& s, simplifier const& simp);
2748 ~solver() { Z3_solver_dec_ref(ctx(), m_solver); }
2749 operator Z3_solver() const { return m_solver; }
2750 solver & operator=(solver const & s) {
2751 Z3_solver_inc_ref(s.ctx(), s.m_solver);
2752 Z3_solver_dec_ref(ctx(), m_solver);
2753 object::operator=(s);
2754 m_solver = s.m_solver;
2755 return *this;
2756 }
2757 void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
2758 void set(char const * k, bool v) { params p(ctx()); p.set(k, v); set(p); }
2759 void set(char const * k, unsigned v) { params p(ctx()); p.set(k, v); set(p); }
2760 void set(char const * k, double v) { params p(ctx()); p.set(k, v); set(p); }
2761 void set(char const * k, symbol const & v) { params p(ctx()); p.set(k, v); set(p); }
2762 void set(char const * k, char const* v) { params p(ctx()); p.set(k, v); set(p); }
2773 void push() { Z3_solver_push(ctx(), m_solver); check_error(); }
2774 void pop(unsigned n = 1) { Z3_solver_pop(ctx(), m_solver, n); check_error(); }
2775 void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); }
2776 void add(expr const & e) { assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); }
2777 void add(expr const & e, expr const & p) {
2778 assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
2779 Z3_solver_assert_and_track(ctx(), m_solver, e, p);
2780 check_error();
2781 }
2782 void add(expr const & e, char const * p) {
2783 add(e, ctx().bool_const(p));
2784 }
2785 void add(expr_vector const& v) {
2786 check_context(*this, v);
2787 for (unsigned i = 0; i < v.size(); ++i)
2788 add(v[i]);
2789 }
2790 void from_file(char const* file) { Z3_solver_from_file(ctx(), m_solver, file); ctx().check_parser_error(); }
2791 void from_string(char const* s) { Z3_solver_from_string(ctx(), m_solver, s); ctx().check_parser_error(); }
2792
2793 check_result check() { Z3_lbool r = Z3_solver_check(ctx(), m_solver); check_error(); return to_check_result(r); }
2794 check_result check(unsigned n, expr * const assumptions) {
2795 array<Z3_ast> _assumptions(n);
2796 for (unsigned i = 0; i < n; i++) {
2797 check_context(*this, assumptions[i]);
2798 _assumptions[i] = assumptions[i];
2799 }
2800 Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
2801 check_error();
2802 return to_check_result(r);
2803 }
2804 check_result check(expr_vector const& assumptions) {
2805 unsigned n = assumptions.size();
2806 array<Z3_ast> _assumptions(n);
2807 for (unsigned i = 0; i < n; i++) {
2808 check_context(*this, assumptions[i]);
2809 _assumptions[i] = assumptions[i];
2810 }
2811 Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
2812 check_error();
2813 return to_check_result(r);
2814 }
2815 model get_model() const { Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }
2816 check_result consequences(expr_vector& assumptions, expr_vector& vars, expr_vector& conseq) {
2817 Z3_lbool r = Z3_solver_get_consequences(ctx(), m_solver, assumptions, vars, conseq);
2818 check_error();
2819 return to_check_result(r);
2820 }
2821 std::string reason_unknown() const { Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }
2822 stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }
2823 expr_vector unsat_core() const { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2824 expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2825 expr_vector non_units() const { Z3_ast_vector r = Z3_solver_get_non_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2826 expr_vector units() const { Z3_ast_vector r = Z3_solver_get_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2827 expr_vector trail() const { Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2828 expr_vector trail(array<unsigned>& levels) const {
2829 Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver);
2830 check_error();
2831 expr_vector result(ctx(), r);
2832 unsigned sz = result.size();
2833 levels.resize(sz);
2834 Z3_solver_get_levels(ctx(), m_solver, r, sz, levels.ptr());
2835 check_error();
2836 return result;
2837 }
2838 expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
2839 friend std::ostream & operator<<(std::ostream & out, solver const & s);
2840
2841 std::string to_smt2(char const* status = "unknown") {
2842 array<Z3_ast> es(assertions());
2843 Z3_ast const* fmls = es.ptr();
2844 Z3_ast fml = 0;
2845 unsigned sz = es.size();
2846 if (sz > 0) {
2847 --sz;
2848 fml = fmls[sz];
2849 }
2850 else {
2851 fml = ctx().bool_val(true);
2852 }
2853 return std::string(Z3_benchmark_to_smtlib_string(
2854 ctx(),
2855 "", "", status, "",
2856 sz,
2857 fmls,
2858 fml));
2859 }
2860
2861 std::string dimacs(bool include_names = true) const { return std::string(Z3_solver_to_dimacs_string(ctx(), m_solver, include_names)); }
2862
2863 param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_solver_get_param_descrs(ctx(), m_solver)); }
2864
2865
2866 expr_vector cube(expr_vector& vars, unsigned cutoff) {
2867 Z3_ast_vector r = Z3_solver_cube(ctx(), m_solver, vars, cutoff);
2868 check_error();
2869 return expr_vector(ctx(), r);
2870 }
2871
2872 class cube_iterator {
2873 solver& m_solver;
2874 unsigned& m_cutoff;
2875 expr_vector& m_vars;
2876 expr_vector m_cube;
2877 bool m_end;
2878 bool m_empty;
2879
2880 void inc() {
2881 assert(!m_end && !m_empty);
2882 m_cube = m_solver.cube(m_vars, m_cutoff);
2883 m_cutoff = 0xFFFFFFFF;
2884 if (m_cube.size() == 1 && m_cube[0u].is_false()) {
2885 m_cube = z3::expr_vector(m_solver.ctx());
2886 m_end = true;
2887 }
2888 else if (m_cube.empty()) {
2889 m_empty = true;
2890 }
2891 }
2892 public:
2893 cube_iterator(solver& s, expr_vector& vars, unsigned& cutoff, bool end):
2894 m_solver(s),
2895 m_cutoff(cutoff),
2896 m_vars(vars),
2897 m_cube(s.ctx()),
2898 m_end(end),
2899 m_empty(false) {
2900 if (!m_end) {
2901 inc();
2902 }
2903 }
2904
2905 cube_iterator& operator++() {
2906 assert(!m_end);
2907 if (m_empty) {
2908 m_end = true;
2909 }
2910 else {
2911 inc();
2912 }
2913 return *this;
2914 }
2915 cube_iterator operator++(int) { assert(false); return *this; }
2916 expr_vector const * operator->() const { return &(operator*()); }
2917 expr_vector const& operator*() const noexcept { return m_cube; }
2918
2919 bool operator==(cube_iterator const& other) noexcept {
2920 return other.m_end == m_end;
2921 };
2922 bool operator!=(cube_iterator const& other) noexcept {
2923 return other.m_end != m_end;
2924 };
2925
2926 };
2927
2928 class cube_generator {
2929 solver& m_solver;
2930 unsigned m_cutoff;
2931 expr_vector m_default_vars;
2932 expr_vector& m_vars;
2933 public:
2934 cube_generator(solver& s):
2935 m_solver(s),
2936 m_cutoff(0xFFFFFFFF),
2937 m_default_vars(s.ctx()),
2938 m_vars(m_default_vars)
2939 {}
2940
2941 cube_generator(solver& s, expr_vector& vars):
2942 m_solver(s),
2943 m_cutoff(0xFFFFFFFF),
2944 m_default_vars(s.ctx()),
2945 m_vars(vars)
2946 {}
2947
2948 cube_iterator begin() { return cube_iterator(m_solver, m_vars, m_cutoff, false); }
2949 cube_iterator end() { return cube_iterator(m_solver, m_vars, m_cutoff, true); }
2950 void set_cutoff(unsigned c) noexcept { m_cutoff = c; }
2951 };
2952
2953 cube_generator cubes() { return cube_generator(*this); }
2954 cube_generator cubes(expr_vector& vars) { return cube_generator(*this, vars); }
2955
2956 };
2957 inline std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
2958
2959 class goal : public object {
2960 Z3_goal m_goal;
2961 void init(Z3_goal s) {
2962 m_goal = s;
2963 Z3_goal_inc_ref(ctx(), s);
2964 }
2965 public:
2966 goal(context & c, bool models=true, bool unsat_cores=false, bool proofs=false):object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); }
2967 goal(context & c, Z3_goal s):object(c) { init(s); }
2968 goal(goal const & s):object(s) { init(s.m_goal); }
2969 ~goal() { Z3_goal_dec_ref(ctx(), m_goal); }
2970 operator Z3_goal() const { return m_goal; }
2971 goal & operator=(goal const & s) {
2972 Z3_goal_inc_ref(s.ctx(), s.m_goal);
2973 Z3_goal_dec_ref(ctx(), m_goal);
2974 object::operator=(s);
2975 m_goal = s.m_goal;
2976 return *this;
2977 }
2978 void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
2979 void add(expr_vector const& v) { check_context(*this, v); for (unsigned i = 0; i < v.size(); ++i) add(v[i]); }
2980 unsigned size() const { return Z3_goal_size(ctx(), m_goal); }
2981 expr operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
2982 Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); }
2983 bool inconsistent() const { return Z3_goal_inconsistent(ctx(), m_goal); }
2984 unsigned depth() const { return Z3_goal_depth(ctx(), m_goal); }
2985 void reset() { Z3_goal_reset(ctx(), m_goal); }
2986 unsigned num_exprs() const { return Z3_goal_num_exprs(ctx(), m_goal); }
2987 bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal); }
2988 bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal); }
2989 model convert_model(model const & m) const {
2990 check_context(*this, m);
2991 Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, m);
2992 check_error();
2993 return model(ctx(), new_m);
2994 }
2995 model get_model() const {
2996 Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, 0);
2997 check_error();
2998 return model(ctx(), new_m);
2999 }
3000 expr as_expr() const {
3001 unsigned n = size();
3002 if (n == 0)
3003 return ctx().bool_val(true);
3004 else if (n == 1)
3005 return operator[](0u);
3006 else {
3007 array<Z3_ast> args(n);
3008 for (unsigned i = 0; i < n; i++)
3009 args[i] = operator[](i);
3010 return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
3011 }
3012 }
3013 std::string dimacs(bool include_names = true) const { return std::string(Z3_goal_to_dimacs_string(ctx(), m_goal, include_names)); }
3014 friend std::ostream & operator<<(std::ostream & out, goal const & g);
3015 };
3016 inline std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; }
3017
3018 class apply_result : public object {
3019 Z3_apply_result m_apply_result;
3020 void init(Z3_apply_result s) {
3021 m_apply_result = s;
3022 Z3_apply_result_inc_ref(ctx(), s);
3023 }
3024 public:
3025 apply_result(context & c, Z3_apply_result s):object(c) { init(s); }
3026 apply_result(apply_result const & s):object(s) { init(s.m_apply_result); }
3027 ~apply_result() { Z3_apply_result_dec_ref(ctx(), m_apply_result); }
3028 operator Z3_apply_result() const { return m_apply_result; }
3029 apply_result & operator=(apply_result const & s) {
3030 Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result);
3031 Z3_apply_result_dec_ref(ctx(), m_apply_result);
3032 object::operator=(s);
3033 m_apply_result = s.m_apply_result;
3034 return *this;
3035 }
3036 unsigned size() const { return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }
3037 goal operator[](int i) const { assert(0 <= i); Z3_goal r = Z3_apply_result_get_subgoal(ctx(), m_apply_result, i); check_error(); return goal(ctx(), r); }
3038 friend std::ostream & operator<<(std::ostream & out, apply_result const & r);
3039 };
3040 inline std::ostream & operator<<(std::ostream & out, apply_result const & r) { out << Z3_apply_result_to_string(r.ctx(), r); return out; }
3041
3042 class tactic : public object {
3043 Z3_tactic m_tactic;
3044 void init(Z3_tactic s) {
3045 m_tactic = s;
3046 Z3_tactic_inc_ref(ctx(), s);
3047 }
3048 public:
3049 tactic(context & c, char const * name):object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); }
3050 tactic(context & c, Z3_tactic s):object(c) { init(s); }
3051 tactic(tactic const & s):object(s) { init(s.m_tactic); }
3052 ~tactic() { Z3_tactic_dec_ref(ctx(), m_tactic); }
3053 operator Z3_tactic() const { return m_tactic; }
3054 tactic & operator=(tactic const & s) {
3055 Z3_tactic_inc_ref(s.ctx(), s.m_tactic);
3056 Z3_tactic_dec_ref(ctx(), m_tactic);
3057 object::operator=(s);
3058 m_tactic = s.m_tactic;
3059 return *this;
3060 }
3061 solver mk_solver() const { Z3_solver r = Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error(); return solver(ctx(), r); }
3062 apply_result apply(goal const & g) const {
3063 check_context(*this, g);
3064 Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g);
3065 check_error();
3066 return apply_result(ctx(), r);
3067 }
3068 apply_result operator()(goal const & g) const {
3069 return apply(g);
3070 }
3071 std::string help() const { char const * r = Z3_tactic_get_help(ctx(), m_tactic); check_error(); return r; }
3072 friend tactic operator&(tactic const & t1, tactic const & t2);
3073 friend tactic operator|(tactic const & t1, tactic const & t2);
3074 friend tactic repeat(tactic const & t, unsigned max);
3075 friend tactic with(tactic const & t, params const & p);
3076 friend tactic try_for(tactic const & t, unsigned ms);
3077 friend tactic par_or(unsigned n, tactic const* tactics);
3078 friend tactic par_and_then(tactic const& t1, tactic const& t2);
3079 param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_tactic_get_param_descrs(ctx(), m_tactic)); }
3080 };
3081
3082 inline tactic operator&(tactic const & t1, tactic const & t2) {
3083 check_context(t1, t2);
3084 Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
3085 t1.check_error();
3086 return tactic(t1.ctx(), r);
3087 }
3088
3089 inline tactic operator|(tactic const & t1, tactic const & t2) {
3090 check_context(t1, t2);
3091 Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
3092 t1.check_error();
3093 return tactic(t1.ctx(), r);
3094 }
3095
3096 inline tactic repeat(tactic const & t, unsigned max=UINT_MAX) {
3097 Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
3098 t.check_error();
3099 return tactic(t.ctx(), r);
3100 }
3101
3102 inline tactic with(tactic const & t, params const & p) {
3103 Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
3104 t.check_error();
3105 return tactic(t.ctx(), r);
3106 }
3107 inline tactic try_for(tactic const & t, unsigned ms) {
3108 Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
3109 t.check_error();
3110 return tactic(t.ctx(), r);
3111 }
3112 inline tactic par_or(unsigned n, tactic const* tactics) {
3113 if (n == 0) {
3114 Z3_THROW(exception("a non-zero number of tactics need to be passed to par_or"));
3115 }
3116 array<Z3_tactic> buffer(n);
3117 for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
3118 return tactic(tactics[0u].ctx(), Z3_tactic_par_or(tactics[0u].ctx(), n, buffer.ptr()));
3119 }
3120
3121 inline tactic par_and_then(tactic const & t1, tactic const & t2) {
3122 check_context(t1, t2);
3123 Z3_tactic r = Z3_tactic_par_and_then(t1.ctx(), t1, t2);
3124 t1.check_error();
3125 return tactic(t1.ctx(), r);
3126 }
3127
3128 class simplifier : public object {
3129 Z3_simplifier m_simplifier;
3130 void init(Z3_simplifier s) {
3131 m_simplifier = s;
3132 Z3_simplifier_inc_ref(ctx(), s);
3133 }
3134 public:
3135 simplifier(context & c, char const * name):object(c) { Z3_simplifier r = Z3_mk_simplifier(c, name); check_error(); init(r); }
3136 simplifier(context & c, Z3_simplifier s):object(c) { init(s); }
3137 simplifier(simplifier const & s):object(s) { init(s.m_simplifier); }
3138 ~simplifier() { Z3_simplifier_dec_ref(ctx(), m_simplifier); }
3139 operator Z3_simplifier() const { return m_simplifier; }
3140 simplifier & operator=(simplifier const & s) {
3141 Z3_simplifier_inc_ref(s.ctx(), s.m_simplifier);
3142 Z3_simplifier_dec_ref(ctx(), m_simplifier);
3143 object::operator=(s);
3144 m_simplifier = s.m_simplifier;
3145 return *this;
3146 }
3147 std::string help() const { char const * r = Z3_simplifier_get_help(ctx(), m_simplifier); check_error(); return r; }
3148 friend simplifier operator&(simplifier const & t1, simplifier const & t2);
3149 friend simplifier with(simplifier const & t, params const & p);
3150 param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_simplifier_get_param_descrs(ctx(), m_simplifier)); }
3151 };
3152
3153 inline solver::solver(solver const& s, simplifier const& simp):object(s) { init(Z3_solver_add_simplifier(s.ctx(), s, simp)); }
3154
3155
3156 inline simplifier operator&(simplifier const & t1, simplifier const & t2) {
3157 check_context(t1, t2);
3158 Z3_simplifier r = Z3_simplifier_and_then(t1.ctx(), t1, t2);
3159 t1.check_error();
3160 return simplifier(t1.ctx(), r);
3161 }
3162
3163 inline simplifier with(simplifier const & t, params const & p) {
3164 Z3_simplifier r = Z3_simplifier_using_params(t.ctx(), t, p);
3165 t.check_error();
3166 return simplifier(t.ctx(), r);
3167 }
3168
3169 class probe : public object {
3170 Z3_probe m_probe;
3171 void init(Z3_probe s) {
3172 m_probe = s;
3173 Z3_probe_inc_ref(ctx(), s);
3174 }
3175 public:
3176 probe(context & c, char const * name):object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); }
3177 probe(context & c, double val):object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); }
3178 probe(context & c, Z3_probe s):object(c) { init(s); }
3179 probe(probe const & s):object(s) { init(s.m_probe); }
3180 ~probe() { Z3_probe_dec_ref(ctx(), m_probe); }
3181 operator Z3_probe() const { return m_probe; }
3182 probe & operator=(probe const & s) {
3183 Z3_probe_inc_ref(s.ctx(), s.m_probe);
3184 Z3_probe_dec_ref(ctx(), m_probe);
3185 object::operator=(s);
3186 m_probe = s.m_probe;
3187 return *this;
3188 }
3189 double apply(goal const & g) const { double r = Z3_probe_apply(ctx(), m_probe, g); check_error(); return r; }
3190 double operator()(goal const & g) const { return apply(g); }
3191 friend probe operator<=(probe const & p1, probe const & p2);
3192 friend probe operator<=(probe const & p1, double p2);
3193 friend probe operator<=(double p1, probe const & p2);
3194 friend probe operator>=(probe const & p1, probe const & p2);
3195 friend probe operator>=(probe const & p1, double p2);
3196 friend probe operator>=(double p1, probe const & p2);
3197 friend probe operator<(probe const & p1, probe const & p2);
3198 friend probe operator<(probe const & p1, double p2);
3199 friend probe operator<(double p1, probe const & p2);
3200 friend probe operator>(probe const & p1, probe const & p2);
3201 friend probe operator>(probe const & p1, double p2);
3202 friend probe operator>(double p1, probe const & p2);
3203 friend probe operator==(probe const & p1, probe const & p2);
3204 friend probe operator==(probe const & p1, double p2);
3205 friend probe operator==(double p1, probe const & p2);
3206 friend probe operator&&(probe const & p1, probe const & p2);
3207 friend probe operator||(probe const & p1, probe const & p2);
3208 friend probe operator!(probe const & p);
3209 };
3210
3211 inline probe operator<=(probe const & p1, probe const & p2) {
3212 check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3213 }
3214 inline probe operator<=(probe const & p1, double p2) { return p1 <= probe(p1.ctx(), p2); }
3215 inline probe operator<=(double p1, probe const & p2) { return probe(p2.ctx(), p1) <= p2; }
3216 inline probe operator>=(probe const & p1, probe const & p2) {
3217 check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3218 }
3219 inline probe operator>=(probe const & p1, double p2) { return p1 >= probe(p1.ctx(), p2); }
3220 inline probe operator>=(double p1, probe const & p2) { return probe(p2.ctx(), p1) >= p2; }
3221 inline probe operator<(probe const & p1, probe const & p2) {
3222 check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3223 }
3224 inline probe operator<(probe const & p1, double p2) { return p1 < probe(p1.ctx(), p2); }
3225 inline probe operator<(double p1, probe const & p2) { return probe(p2.ctx(), p1) < p2; }
3226 inline probe operator>(probe const & p1, probe const & p2) {
3227 check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3228 }
3229 inline probe operator>(probe const & p1, double p2) { return p1 > probe(p1.ctx(), p2); }
3230 inline probe operator>(double p1, probe const & p2) { return probe(p2.ctx(), p1) > p2; }
3231 inline probe operator==(probe const & p1, probe const & p2) {
3232 check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3233 }
3234 inline probe operator==(probe const & p1, double p2) { return p1 == probe(p1.ctx(), p2); }
3235 inline probe operator==(double p1, probe const & p2) { return probe(p2.ctx(), p1) == p2; }
3236 inline probe operator&&(probe const & p1, probe const & p2) {
3237 check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3238 }
3239 inline probe operator||(probe const & p1, probe const & p2) {
3240 check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3241 }
3242 inline probe operator!(probe const & p) {
3243 Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
3244 }
3245
3246 class optimize : public object {
3247 Z3_optimize m_opt;
3248
3249 public:
3250 class handle final {
3251 unsigned m_h;
3252 public:
3253 handle(unsigned h): m_h(h) {}
3254 unsigned h() const { return m_h; }
3255 };
3256 optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }
3257 optimize(optimize const & o):object(o), m_opt(o.m_opt) {
3258 Z3_optimize_inc_ref(o.ctx(), o.m_opt);
3259 }
3260 optimize(context& c, optimize& src):object(c) {
3261 m_opt = Z3_mk_optimize(c);
3262 Z3_optimize_inc_ref(c, m_opt);
3263 add(expr_vector(c, src.assertions()));
3264 expr_vector v(c, src.objectives());
3265 for (expr_vector::iterator it = v.begin(); it != v.end(); ++it) minimize(*it);
3266 }
3267 optimize& operator=(optimize const& o) {
3268 Z3_optimize_inc_ref(o.ctx(), o.m_opt);
3269 Z3_optimize_dec_ref(ctx(), m_opt);
3270 m_opt = o.m_opt;
3271 object::operator=(o);
3272 return *this;
3273 }
3274 ~optimize() { Z3_optimize_dec_ref(ctx(), m_opt); }
3275 operator Z3_optimize() const { return m_opt; }
3276 void add(expr const& e) {
3277 assert(e.is_bool());
3278 Z3_optimize_assert(ctx(), m_opt, e);
3279 }
3280 void add(expr_vector const& es) {
3281 for (expr_vector::iterator it = es.begin(); it != es.end(); ++it) add(*it);
3282 }
3283 void add(expr const& e, expr const& t) {
3284 assert(e.is_bool());
3285 Z3_optimize_assert_and_track(ctx(), m_opt, e, t);
3286 }
3287 void add(expr const& e, char const* p) {
3288 assert(e.is_bool());
3289 add(e, ctx().bool_const(p));
3290 }
3291 handle add_soft(expr const& e, unsigned weight) {
3292 assert(e.is_bool());
3293 auto str = std::to_string(weight);
3294 return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, str.c_str(), 0));
3295 }
3296 handle add_soft(expr const& e, char const* weight) {
3297 assert(e.is_bool());
3298 return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0));
3299 }
3300 handle add(expr const& e, unsigned weight) {
3301 return add_soft(e, weight);
3302 }
3303 handle maximize(expr const& e) {
3304 return handle(Z3_optimize_maximize(ctx(), m_opt, e));
3305 }
3306 handle minimize(expr const& e) {
3307 return handle(Z3_optimize_minimize(ctx(), m_opt, e));
3308 }
3309 void push() {
3310 Z3_optimize_push(ctx(), m_opt);
3311 }
3312 void pop() {
3313 Z3_optimize_pop(ctx(), m_opt);
3314 }
3315 check_result check() { Z3_lbool r = Z3_optimize_check(ctx(), m_opt, 0, 0); check_error(); return to_check_result(r); }
3316 check_result check(expr_vector const& asms) {
3317 unsigned n = asms.size();
3318 array<Z3_ast> _asms(n);
3319 for (unsigned i = 0; i < n; i++) {
3320 check_context(*this, asms[i]);
3321 _asms[i] = asms[i];
3322 }
3323 Z3_lbool r = Z3_optimize_check(ctx(), m_opt, n, _asms.ptr());
3324 check_error();
3325 return to_check_result(r);
3326 }
3327 model get_model() const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }
3328 expr_vector unsat_core() const { Z3_ast_vector r = Z3_optimize_get_unsat_core(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
3329 void set(params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }
3330 expr lower(handle const& h) {
3331 Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());
3332 check_error();
3333 return expr(ctx(), r);
3334 }
3335 expr upper(handle const& h) {
3336 Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h());
3337 check_error();
3338 return expr(ctx(), r);
3339 }
3340 expr_vector assertions() const { Z3_ast_vector r = Z3_optimize_get_assertions(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
3341 expr_vector objectives() const { Z3_ast_vector r = Z3_optimize_get_objectives(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
3342 stats statistics() const { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); }
3343 friend std::ostream & operator<<(std::ostream & out, optimize const & s);
3344 void from_file(char const* filename) { Z3_optimize_from_file(ctx(), m_opt, filename); check_error(); }
3345 void from_string(char const* constraints) { Z3_optimize_from_string(ctx(), m_opt, constraints); check_error(); }
3346 std::string help() const { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error(); return r; }
3347 };
3348 inline std::ostream & operator<<(std::ostream & out, optimize const & s) { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }
3349
3350 class fixedpoint : public object {
3351 Z3_fixedpoint m_fp;
3352 public:
3353 fixedpoint(context& c):object(c) { m_fp = Z3_mk_fixedpoint(c); Z3_fixedpoint_inc_ref(c, m_fp); }
3354 fixedpoint(fixedpoint const & o):object(o), m_fp(o.m_fp) { Z3_fixedpoint_inc_ref(ctx(), m_fp); }
3355 ~fixedpoint() { Z3_fixedpoint_dec_ref(ctx(), m_fp); }
3356 fixedpoint & operator=(fixedpoint const & o) {
3357 Z3_fixedpoint_inc_ref(o.ctx(), o.m_fp);
3358 Z3_fixedpoint_dec_ref(ctx(), m_fp);
3359 m_fp = o.m_fp;
3360 object::operator=(o);
3361 return *this;
3362 }
3363 operator Z3_fixedpoint() const { return m_fp; }
3364 expr_vector from_string(char const* s) {
3365 Z3_ast_vector r = Z3_fixedpoint_from_string(ctx(), m_fp, s);
3366 check_error();
3367 return expr_vector(ctx(), r);
3368 }
3369 expr_vector from_file(char const* s) {
3370 Z3_ast_vector r = Z3_fixedpoint_from_file(ctx(), m_fp, s);
3371 check_error();
3372 return expr_vector(ctx(), r);
3373 }
3374 void add_rule(expr& rule, symbol const& name) { Z3_fixedpoint_add_rule(ctx(), m_fp, rule, name); check_error(); }
3375 void add_fact(func_decl& f, unsigned * args) { Z3_fixedpoint_add_fact(ctx(), m_fp, f, f.arity(), args); check_error(); }
3376 check_result query(expr& q) { Z3_lbool r = Z3_fixedpoint_query(ctx(), m_fp, q); check_error(); return to_check_result(r); }
3377 check_result query(func_decl_vector& relations) {
3378 array<Z3_func_decl> rs(relations);
3379 Z3_lbool r = Z3_fixedpoint_query_relations(ctx(), m_fp, rs.size(), rs.ptr());
3380 check_error();
3381 return to_check_result(r);
3382 }
3383 expr get_answer() { Z3_ast r = Z3_fixedpoint_get_answer(ctx(), m_fp); check_error(); return expr(ctx(), r); }
3384 std::string reason_unknown() { return Z3_fixedpoint_get_reason_unknown(ctx(), m_fp); }
3385 void update_rule(expr& rule, symbol const& name) { Z3_fixedpoint_update_rule(ctx(), m_fp, rule, name); check_error(); }
3386 unsigned get_num_levels(func_decl& p) { unsigned r = Z3_fixedpoint_get_num_levels(ctx(), m_fp, p); check_error(); return r; }
3387 expr get_cover_delta(int level, func_decl& p) {
3388 Z3_ast r = Z3_fixedpoint_get_cover_delta(ctx(), m_fp, level, p);
3389 check_error();
3390 return expr(ctx(), r);
3391 }
3392 void add_cover(int level, func_decl& p, expr& property) { Z3_fixedpoint_add_cover(ctx(), m_fp, level, p, property); check_error(); }
3393 stats statistics() const { Z3_stats r = Z3_fixedpoint_get_statistics(ctx(), m_fp); check_error(); return stats(ctx(), r); }
3394 void register_relation(func_decl& p) { Z3_fixedpoint_register_relation(ctx(), m_fp, p); }
3395 expr_vector assertions() const { Z3_ast_vector r = Z3_fixedpoint_get_assertions(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
3396 expr_vector rules() const { Z3_ast_vector r = Z3_fixedpoint_get_rules(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
3397 void set(params const & p) { Z3_fixedpoint_set_params(ctx(), m_fp, p); check_error(); }
3398 std::string help() const { return Z3_fixedpoint_get_help(ctx(), m_fp); }
3399 param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_fixedpoint_get_param_descrs(ctx(), m_fp)); }
3400 std::string to_string() { return Z3_fixedpoint_to_string(ctx(), m_fp, 0, 0); }
3401 std::string to_string(expr_vector const& queries) {
3402 array<Z3_ast> qs(queries);
3403 return Z3_fixedpoint_to_string(ctx(), m_fp, qs.size(), qs.ptr());
3404 }
3405 };
3406 inline std::ostream & operator<<(std::ostream & out, fixedpoint const & f) { return out << Z3_fixedpoint_to_string(f.ctx(), f, 0, 0); }
3407
3408 inline tactic fail_if(probe const & p) {
3409 Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
3410 p.check_error();
3411 return tactic(p.ctx(), r);
3412 }
3413 inline tactic when(probe const & p, tactic const & t) {
3414 check_context(p, t);
3415 Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
3416 t.check_error();
3417 return tactic(t.ctx(), r);
3418 }
3419 inline tactic cond(probe const & p, tactic const & t1, tactic const & t2) {
3420 check_context(p, t1); check_context(p, t2);
3421 Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
3422 t1.check_error();
3423 return tactic(t1.ctx(), r);
3424 }
3425
3426 inline symbol context::str_symbol(char const * s) { Z3_symbol r = Z3_mk_string_symbol(m_ctx, s); check_error(); return symbol(*this, r); }
3427 inline symbol context::int_symbol(int n) { Z3_symbol r = Z3_mk_int_symbol(m_ctx, n); check_error(); return symbol(*this, r); }
3428
3429 inline sort context::bool_sort() { Z3_sort s = Z3_mk_bool_sort(m_ctx); check_error(); return sort(*this, s); }
3430 inline sort context::int_sort() { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }
3431 inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
3432 inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
3433 inline sort context::string_sort() { Z3_sort s = Z3_mk_string_sort(m_ctx); check_error(); return sort(*this, s); }
3434 inline sort context::char_sort() { Z3_sort s = Z3_mk_char_sort(m_ctx); check_error(); return sort(*this, s); }
3435 inline sort context::seq_sort(sort& s) { Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); }
3436 inline sort context::re_sort(sort& s) { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
3437 inline sort context::fpa_sort(unsigned ebits, unsigned sbits) { Z3_sort s = Z3_mk_fpa_sort(m_ctx, ebits, sbits); check_error(); return sort(*this, s); }
3438
3439 template<>
3440 inline sort context::fpa_sort<16>() { return fpa_sort(5, 11); }
3441
3442 template<>
3443 inline sort context::fpa_sort<32>() { return fpa_sort(8, 24); }
3444
3445 template<>
3446 inline sort context::fpa_sort<64>() { return fpa_sort(11, 53); }
3447
3448 template<>
3449 inline sort context::fpa_sort<128>() { return fpa_sort(15, 113); }
3450
3451 inline sort context::fpa_rounding_mode_sort() { Z3_sort r = Z3_mk_fpa_rounding_mode_sort(m_ctx); check_error(); return sort(*this, r); }
3452
3453 inline sort context::array_sort(sort d, sort r) { Z3_sort s = Z3_mk_array_sort(m_ctx, d, r); check_error(); return sort(*this, s); }
3454 inline sort context::array_sort(sort_vector const& d, sort r) {
3455 array<Z3_sort> dom(d);
3456 Z3_sort s = Z3_mk_array_sort_n(m_ctx, dom.size(), dom.ptr(), r); check_error(); return sort(*this, s);
3457 }
3458 inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
3459 array<Z3_symbol> _enum_names(n);
3460 for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
3461 array<Z3_func_decl> _cs(n);
3462 array<Z3_func_decl> _ts(n);
3463 Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3464 sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
3465 check_error();
3466 for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
3467 return s;
3468 }
3469 inline func_decl context::tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs) {
3470 array<Z3_symbol> _names(n);
3471 array<Z3_sort> _sorts(n);
3472 for (unsigned i = 0; i < n; i++) { _names[i] = Z3_mk_string_symbol(*this, names[i]); _sorts[i] = sorts[i]; }
3473 array<Z3_func_decl> _projs(n);
3474 Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3475 Z3_func_decl tuple;
3476 sort _ignore_s = to_sort(*this, Z3_mk_tuple_sort(*this, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));
3477 check_error();
3478 for (unsigned i = 0; i < n; i++) { projs.push_back(func_decl(*this, _projs[i])); }
3479 return func_decl(*this, tuple);
3480 }
3481
3482 class constructor_list {
3483 context& ctx;
3484 Z3_constructor_list clist;
3485 public:
3486 constructor_list(constructors const& cs);
3487 ~constructor_list() { Z3_del_constructor_list(ctx, clist); }
3488 operator Z3_constructor_list() const { return clist; }
3489 };
3490
3491 class constructors {
3492 friend class constructor_list;
3493 context& ctx;
3494 std::vector<Z3_constructor> cons;
3495 std::vector<unsigned> num_fields;
3496 public:
3497 constructors(context& ctx): ctx(ctx) {}
3498
3499 ~constructors() {
3500 for (auto con : cons)
3501 Z3_del_constructor(ctx, con);
3502 }
3503
3504 void add(symbol const& name, symbol const& rec, unsigned n, symbol const* names, sort const* fields) {
3505 array<unsigned> sort_refs(n);
3506 array<Z3_sort> sorts(n);
3507 array<Z3_symbol> _names(n);
3508 for (unsigned i = 0; i < n; ++i) sorts[i] = fields[i], _names[i] = names[i];
3509 cons.push_back(Z3_mk_constructor(ctx, name, rec, n, _names.ptr(), sorts.ptr(), sort_refs.ptr()));
3510 num_fields.push_back(n);
3511 }
3512
3513 Z3_constructor operator[](unsigned i) const { return cons[i]; }
3514
3515 unsigned size() const { return (unsigned)cons.size(); }
3516
3517 void query(unsigned i, func_decl& constructor, func_decl& test, func_decl_vector& accs) {
3518 Z3_func_decl _constructor;
3519 Z3_func_decl _test;
3520 array<Z3_func_decl> accessors(num_fields[i]);
3521 accs.resize(0);
3523 cons[i],
3524 num_fields[i],
3525 &_constructor,
3526 &_test,
3527 accessors.ptr());
3528 constructor = func_decl(ctx, _constructor);
3529
3530 test = func_decl(ctx, _test);
3531 for (unsigned j = 0; j < num_fields[i]; ++j)
3532 accs.push_back(func_decl(ctx, accessors[j]));
3533 }
3534 };
3535
3536 inline constructor_list::constructor_list(constructors const& cs): ctx(cs.ctx) {
3537 array<Z3_constructor> cons(cs.size());
3538 for (unsigned i = 0; i < cs.size(); ++i)
3539 cons[i] = cs[i];
3540 clist = Z3_mk_constructor_list(ctx, cs.size(), cons.ptr());
3541 }
3542
3543 inline sort context::datatype(symbol const& name, constructors const& cs) {
3544 array<Z3_constructor> _cs(cs.size());
3545 for (unsigned i = 0; i < cs.size(); ++i) _cs[i] = cs[i];
3546 Z3_sort s = Z3_mk_datatype(*this, name, cs.size(), _cs.ptr());
3547 check_error();
3548 return sort(*this, s);
3549 }
3550
3551 inline sort_vector context::datatypes(
3552 unsigned n, symbol const* names,
3553 constructor_list *const* cons) {
3554 sort_vector result(*this);
3555 array<Z3_symbol> _names(n);
3556 array<Z3_sort> _sorts(n);
3557 array<Z3_constructor_list> _cons(n);
3558 for (unsigned i = 0; i < n; ++i)
3559 _names[i] = names[i], _cons[i] = *cons[i];
3560 Z3_mk_datatypes(*this, n, _names.ptr(), _sorts.ptr(), _cons.ptr());
3561 for (unsigned i = 0; i < n; ++i)
3562 result.push_back(sort(*this, _sorts[i]));
3563 return result;
3564 }
3565
3566
3567 inline sort context::datatype_sort(symbol const& name) {
3568 Z3_sort s = Z3_mk_datatype_sort(*this, name);
3569 check_error();
3570 return sort(*this, s);
3571 }
3572
3573
3574 inline sort context::uninterpreted_sort(char const* name) {
3575 Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3576 return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
3577 }
3578 inline sort context::uninterpreted_sort(symbol const& name) {
3579 return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
3580 }
3581
3582 inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3583 array<Z3_sort> args(arity);
3584 for (unsigned i = 0; i < arity; i++) {
3585 check_context(domain[i], range);
3586 args[i] = domain[i];
3587 }
3588 Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
3589 check_error();
3590 return func_decl(*this, f);
3591 }
3592
3593 inline func_decl context::function(char const * name, unsigned arity, sort const * domain, sort const & range) {
3594 return function(range.ctx().str_symbol(name), arity, domain, range);
3595 }
3596
3597 inline func_decl context::function(symbol const& name, sort_vector const& domain, sort const& range) {
3598 array<Z3_sort> args(domain.size());
3599 for (unsigned i = 0; i < domain.size(); i++) {
3600 check_context(domain[i], range);
3601 args[i] = domain[i];
3602 }
3603 Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
3604 check_error();
3605 return func_decl(*this, f);
3606 }
3607
3608 inline func_decl context::function(char const * name, sort_vector const& domain, sort const& range) {
3609 return function(range.ctx().str_symbol(name), domain, range);
3610 }
3611
3612
3613 inline func_decl context::function(char const * name, sort const & domain, sort const & range) {
3614 check_context(domain, range);
3615 Z3_sort args[1] = { domain };
3616 Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
3617 check_error();
3618 return func_decl(*this, f);
3619 }
3620
3621 inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & range) {
3622 check_context(d1, range); check_context(d2, range);
3623 Z3_sort args[2] = { d1, d2 };
3624 Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
3625 check_error();
3626 return func_decl(*this, f);
3627 }
3628
3629 inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
3630 check_context(d1, range); check_context(d2, range); check_context(d3, range);
3631 Z3_sort args[3] = { d1, d2, d3 };
3632 Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
3633 check_error();
3634 return func_decl(*this, f);
3635 }
3636
3637 inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
3638 check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range);
3639 Z3_sort args[4] = { d1, d2, d3, d4 };
3640 Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
3641 check_error();
3642 return func_decl(*this, f);
3643 }
3644
3645 inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range) {
3646 check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range); check_context(d5, range);
3647 Z3_sort args[5] = { d1, d2, d3, d4, d5 };
3648 Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
3649 check_error();
3650 return func_decl(*this, f);
3651 }
3652
3653 inline func_decl context::recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3654 array<Z3_sort> args(arity);
3655 for (unsigned i = 0; i < arity; i++) {
3656 check_context(domain[i], range);
3657 args[i] = domain[i];
3658 }
3659 Z3_func_decl f = Z3_mk_rec_func_decl(m_ctx, name, arity, args.ptr(), range);
3660 check_error();
3661 return func_decl(*this, f);
3662
3663 }
3664
3665 inline func_decl context::recfun(symbol const & name, sort_vector const& domain, sort const & range) {
3666 check_context(domain, range);
3667 array<Z3_sort> domain1(domain);
3668 Z3_func_decl f = Z3_mk_rec_func_decl(m_ctx, name, domain1.size(), domain1.ptr(), range);
3669 check_error();
3670 return func_decl(*this, f);
3671 }
3672
3673 inline func_decl context::recfun(char const * name, sort_vector const& domain, sort const & range) {
3674 return recfun(str_symbol(name), domain, range);
3675
3676 }
3677
3678 inline func_decl context::recfun(char const * name, unsigned arity, sort const * domain, sort const & range) {
3679 return recfun(str_symbol(name), arity, domain, range);
3680 }
3681
3682 inline func_decl context::recfun(char const * name, sort const& d1, sort const & range) {
3683 return recfun(str_symbol(name), 1, &d1, range);
3684 }
3685
3686 inline func_decl context::recfun(char const * name, sort const& d1, sort const& d2, sort const & range) {
3687 sort dom[2] = { d1, d2 };
3688 return recfun(str_symbol(name), 2, dom, range);
3689 }
3690
3691 inline void context::recdef(func_decl f, expr_vector const& args, expr const& body) {
3692 check_context(f, args); check_context(f, body);
3693 array<Z3_ast> vars(args);
3694 Z3_add_rec_def(f.ctx(), f, vars.size(), vars.ptr(), body);
3695 }
3696
3697 inline func_decl context::user_propagate_function(symbol const& name, sort_vector const& domain, sort const& range) {
3698 check_context(domain, range);
3699 array<Z3_sort> domain1(domain);
3700 Z3_func_decl f = Z3_solver_propagate_declare(range.ctx(), name, domain1.size(), domain1.ptr(), range);
3701 check_error();
3702 return func_decl(*this, f);
3703 }
3704
3705 inline expr context::constant(symbol const & name, sort const & s) {
3706 Z3_ast r = Z3_mk_const(m_ctx, name, s);
3707 check_error();
3708 return expr(*this, r);
3709 }
3710 inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); }
3711 inline expr context::variable(unsigned idx, sort const& s) {
3712 Z3_ast r = Z3_mk_bound(m_ctx, idx, s);
3713 check_error();
3714 return expr(*this, r);
3715 }
3716 inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); }
3717 inline expr context::int_const(char const * name) { return constant(name, int_sort()); }
3718 inline expr context::real_const(char const * name) { return constant(name, real_sort()); }
3719 inline expr context::string_const(char const * name) { return constant(name, string_sort()); }
3720 inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); }
3721 inline expr context::fpa_const(char const * name, unsigned ebits, unsigned sbits) { return constant(name, fpa_sort(ebits, sbits)); }
3722
3723 template<size_t precision>
3724 inline expr context::fpa_const(char const * name) { return constant(name, fpa_sort<precision>()); }
3725
3726 inline void context::set_rounding_mode(rounding_mode rm) { m_rounding_mode = rm; }
3727
3728 inline expr context::fpa_rounding_mode() {
3729 switch (m_rounding_mode) {
3730 case RNA: return expr(*this, Z3_mk_fpa_rna(m_ctx));
3731 case RNE: return expr(*this, Z3_mk_fpa_rne(m_ctx));
3732 case RTP: return expr(*this, Z3_mk_fpa_rtp(m_ctx));
3733 case RTN: return expr(*this, Z3_mk_fpa_rtn(m_ctx));
3734 case RTZ: return expr(*this, Z3_mk_fpa_rtz(m_ctx));
3735 default: return expr(*this);
3736 }
3737 }
3738
3739 inline expr context::bool_val(bool b) { return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }
3740
3741 inline expr context::int_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
3742 inline expr context::int_val(unsigned n) { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
3743 inline expr context::int_val(int64_t n) { Z3_ast r = Z3_mk_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
3744 inline expr context::int_val(uint64_t n) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
3745 inline expr context::int_val(char const * n) { Z3_ast r = Z3_mk_numeral(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
3746
3747 inline expr context::real_val(int64_t n, int64_t d) { Z3_ast r = Z3_mk_real_int64(m_ctx, n, d); check_error(); return expr(*this, r); }
3748 inline expr context::real_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
3749 inline expr context::real_val(unsigned n) { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
3750 inline expr context::real_val(int64_t n) { Z3_ast r = Z3_mk_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
3751 inline expr context::real_val(uint64_t n) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
3752 inline expr context::real_val(char const * n) { Z3_ast r = Z3_mk_numeral(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
3753
3754 inline expr context::bv_val(int n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_int(m_ctx, n, s); check_error(); return expr(*this, r); }
3755 inline expr context::bv_val(unsigned n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, s); check_error(); return expr(*this, r); }
3756 inline expr context::bv_val(int64_t n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_int64(m_ctx, n, s); check_error(); return expr(*this, r); }
3757 inline expr context::bv_val(uint64_t n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, s); check_error(); return expr(*this, r); }
3758 inline expr context::bv_val(char const * n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_numeral(m_ctx, n, s); check_error(); return expr(*this, r); }
3759 inline expr context::bv_val(unsigned n, bool const* bits) {
3760 array<bool> _bits(n);
3761 for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
3762 Z3_ast r = Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error(); return expr(*this, r);
3763 }
3764
3765 inline expr context::fpa_val(double n) { sort s = fpa_sort<64>(); Z3_ast r = Z3_mk_fpa_numeral_double(m_ctx, n, s); check_error(); return expr(*this, r); }
3766 inline expr context::fpa_val(float n) { sort s = fpa_sort<32>(); Z3_ast r = Z3_mk_fpa_numeral_float(m_ctx, n, s); check_error(); return expr(*this, r); }
3767 inline expr context::fpa_nan(sort const & s) { Z3_ast r = Z3_mk_fpa_nan(m_ctx, s); check_error(); return expr(*this, r); }
3768 inline expr context::fpa_inf(sort const & s, bool sgn) { Z3_ast r = Z3_mk_fpa_inf(m_ctx, s, sgn); check_error(); return expr(*this, r); }
3769
3770 inline expr context::string_val(char const* s, unsigned n) { Z3_ast r = Z3_mk_lstring(m_ctx, n, s); check_error(); return expr(*this, r); }
3771 inline expr context::string_val(char const* s) { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
3772 inline expr context::string_val(std::string const& s) { Z3_ast r = Z3_mk_string(m_ctx, s.c_str()); check_error(); return expr(*this, r); }
3773 inline expr context::string_val(std::u32string const& s) { Z3_ast r = Z3_mk_u32string(m_ctx, (unsigned)s.size(), (unsigned const*)s.c_str()); check_error(); return expr(*this, r); }
3774
3775 inline expr context::num_val(int n, sort const & s) { Z3_ast r = Z3_mk_int(m_ctx, n, s); check_error(); return expr(*this, r); }
3776
3777 inline expr func_decl::operator()(unsigned n, expr const * args) const {
3778 array<Z3_ast> _args(n);
3779 for (unsigned i = 0; i < n; i++) {
3780 check_context(*this, args[i]);
3781 _args[i] = args[i];
3782 }
3783 Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
3784 check_error();
3785 return expr(ctx(), r);
3786
3787 }
3788 inline expr func_decl::operator()(expr_vector const& args) const {
3789 array<Z3_ast> _args(args.size());
3790 for (unsigned i = 0; i < args.size(); i++) {
3791 check_context(*this, args[i]);
3792 _args[i] = args[i];
3793 }
3794 Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
3795 check_error();
3796 return expr(ctx(), r);
3797 }
3798 inline expr func_decl::operator()() const {
3799 Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
3800 ctx().check_error();
3801 return expr(ctx(), r);
3802 }
3803 inline expr func_decl::operator()(expr const & a) const {
3804 check_context(*this, a);
3805 Z3_ast args[1] = { a };
3806 Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3807 ctx().check_error();
3808 return expr(ctx(), r);
3809 }
3810 inline expr func_decl::operator()(int a) const {
3811 Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
3812 Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3813 ctx().check_error();
3814 return expr(ctx(), r);
3815 }
3816 inline expr func_decl::operator()(expr const & a1, expr const & a2) const {
3817 check_context(*this, a1); check_context(*this, a2);
3818 Z3_ast args[2] = { a1, a2 };
3819 Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3820 ctx().check_error();
3821 return expr(ctx(), r);
3822 }
3823 inline expr func_decl::operator()(expr const & a1, int a2) const {
3824 check_context(*this, a1);
3825 Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
3826 Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3827 ctx().check_error();
3828 return expr(ctx(), r);
3829 }
3830 inline expr func_decl::operator()(int a1, expr const & a2) const {
3831 check_context(*this, a2);
3832 Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
3833 Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3834 ctx().check_error();
3835 return expr(ctx(), r);
3836 }
3837 inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3) const {
3838 check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
3839 Z3_ast args[3] = { a1, a2, a3 };
3840 Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
3841 ctx().check_error();
3842 return expr(ctx(), r);
3843 }
3844 inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const {
3845 check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
3846 Z3_ast args[4] = { a1, a2, a3, a4 };
3847 Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
3848 ctx().check_error();
3849 return expr(ctx(), r);
3850 }
3851 inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const {
3852 check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
3853 Z3_ast args[5] = { a1, a2, a3, a4, a5 };
3854 Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
3855 ctx().check_error();
3856 return expr(ctx(), r);
3857 }
3858
3859 inline expr to_real(expr const & a) { Z3_ast r = Z3_mk_int2real(a.ctx(), a); a.check_error(); return expr(a.ctx(), r); }
3860
3861 inline func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3862 return range.ctx().function(name, arity, domain, range);
3863 }
3864 inline func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range) {
3865 return range.ctx().function(name, arity, domain, range);
3866 }
3867 inline func_decl function(char const * name, sort const & domain, sort const & range) {
3868 return range.ctx().function(name, domain, range);
3869 }
3870 inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range) {
3871 return range.ctx().function(name, d1, d2, range);
3872 }
3873 inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
3874 return range.ctx().function(name, d1, d2, d3, range);
3875 }
3876 inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
3877 return range.ctx().function(name, d1, d2, d3, d4, range);
3878 }
3879 inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range) {
3880 return range.ctx().function(name, d1, d2, d3, d4, d5, range);
3881 }
3882 inline func_decl function(char const* name, sort_vector const& domain, sort const& range) {
3883 return range.ctx().function(name, domain, range);
3884 }
3885 inline func_decl function(std::string const& name, sort_vector const& domain, sort const& range) {
3886 return range.ctx().function(name.c_str(), domain, range);
3887 }
3888
3889 inline func_decl recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3890 return range.ctx().recfun(name, arity, domain, range);
3891 }
3892 inline func_decl recfun(char const * name, unsigned arity, sort const * domain, sort const & range) {
3893 return range.ctx().recfun(name, arity, domain, range);
3894 }
3895 inline func_decl recfun(char const * name, sort const& d1, sort const & range) {
3896 return range.ctx().recfun(name, d1, range);
3897 }
3898 inline func_decl recfun(char const * name, sort const& d1, sort const& d2, sort const & range) {
3899 return range.ctx().recfun(name, d1, d2, range);
3900 }
3901
3902 inline expr select(expr const & a, expr const & i) {
3903 check_context(a, i);
3904 Z3_ast r = Z3_mk_select(a.ctx(), a, i);
3905 a.check_error();
3906 return expr(a.ctx(), r);
3907 }
3908 inline expr select(expr const & a, int i) {
3909 return select(a, a.ctx().num_val(i, a.get_sort().array_domain()));
3910 }
3911 inline expr select(expr const & a, expr_vector const & i) {
3912 check_context(a, i);
3913 array<Z3_ast> idxs(i);
3914 Z3_ast r = Z3_mk_select_n(a.ctx(), a, idxs.size(), idxs.ptr());
3915 a.check_error();
3916 return expr(a.ctx(), r);
3917 }
3918
3919 inline expr store(expr const & a, expr const & i, expr const & v) {
3920 check_context(a, i); check_context(a, v);
3921 Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
3922 a.check_error();
3923 return expr(a.ctx(), r);
3924 }
3925
3926 inline expr store(expr const & a, int i, expr const & v) { return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), v); }
3927 inline expr store(expr const & a, expr i, int v) { return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
3928 inline expr store(expr const & a, int i, int v) {
3929 return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
3930 }
3931 inline expr store(expr const & a, expr_vector const & i, expr const & v) {
3932 check_context(a, i); check_context(a, v);
3933 array<Z3_ast> idxs(i);
3934 Z3_ast r = Z3_mk_store_n(a.ctx(), a, idxs.size(), idxs.ptr(), v);
3935 a.check_error();
3936 return expr(a.ctx(), r);
3937 }
3938
3939 inline expr as_array(func_decl & f) {
3940 Z3_ast r = Z3_mk_as_array(f.ctx(), f);
3941 f.check_error();
3942 return expr(f.ctx(), r);
3943 }
3944
3945#define MK_EXPR1(_fn, _arg) \
3946 Z3_ast r = _fn(_arg.ctx(), _arg); \
3947 _arg.check_error(); \
3948 return expr(_arg.ctx(), r);
3949
3950#define MK_EXPR2(_fn, _arg1, _arg2) \
3951 check_context(_arg1, _arg2); \
3952 Z3_ast r = _fn(_arg1.ctx(), _arg1, _arg2); \
3953 _arg1.check_error(); \
3954 return expr(_arg1.ctx(), r);
3955
3956 inline expr const_array(sort const & d, expr const & v) {
3958 }
3959
3960 inline expr empty_set(sort const& s) {
3962 }
3963
3964 inline expr full_set(sort const& s) {
3966 }
3967
3968 inline expr set_add(expr const& s, expr const& e) {
3969 MK_EXPR2(Z3_mk_set_add, s, e);
3970 }
3971
3972 inline expr set_del(expr const& s, expr const& e) {
3973 MK_EXPR2(Z3_mk_set_del, s, e);
3974 }
3975
3976 inline expr set_union(expr const& a, expr const& b) {
3977 check_context(a, b);
3978 Z3_ast es[2] = { a, b };
3979 Z3_ast r = Z3_mk_set_union(a.ctx(), 2, es);
3980 a.check_error();
3981 return expr(a.ctx(), r);
3982 }
3983
3984 inline expr set_intersect(expr const& a, expr const& b) {
3985 check_context(a, b);
3986 Z3_ast es[2] = { a, b };
3987 Z3_ast r = Z3_mk_set_intersect(a.ctx(), 2, es);
3988 a.check_error();
3989 return expr(a.ctx(), r);
3990 }
3991
3992 inline expr set_difference(expr const& a, expr const& b) {
3994 }
3995
3996 inline expr set_complement(expr const& a) {
3998 }
3999
4000 inline expr set_member(expr const& s, expr const& e) {
4002 }
4003
4004 inline expr set_subset(expr const& a, expr const& b) {
4006 }
4007
4008 // sequence and regular expression operations.
4009 // union is +
4010 // concat is overloaded to handle sequences and regular expressions
4011
4012 inline expr empty(sort const& s) {
4013 Z3_ast r = Z3_mk_seq_empty(s.ctx(), s);
4014 s.check_error();
4015 return expr(s.ctx(), r);
4016 }
4017 inline expr suffixof(expr const& a, expr const& b) {
4018 check_context(a, b);
4019 Z3_ast r = Z3_mk_seq_suffix(a.ctx(), a, b);
4020 a.check_error();
4021 return expr(a.ctx(), r);
4022 }
4023 inline expr prefixof(expr const& a, expr const& b) {
4024 check_context(a, b);
4025 Z3_ast r = Z3_mk_seq_prefix(a.ctx(), a, b);
4026 a.check_error();
4027 return expr(a.ctx(), r);
4028 }
4029 inline expr indexof(expr const& s, expr const& substr, expr const& offset) {
4030 check_context(s, substr); check_context(s, offset);
4031 Z3_ast r = Z3_mk_seq_index(s.ctx(), s, substr, offset);
4032 s.check_error();
4033 return expr(s.ctx(), r);
4034 }
4035 inline expr last_indexof(expr const& s, expr const& substr) {
4036 check_context(s, substr);
4037 Z3_ast r = Z3_mk_seq_last_index(s.ctx(), s, substr);
4038 s.check_error();
4039 return expr(s.ctx(), r);
4040 }
4041 inline expr to_re(expr const& s) {
4043 }
4044 inline expr in_re(expr const& s, expr const& re) {
4045 MK_EXPR2(Z3_mk_seq_in_re, s, re);
4046 }
4047 inline expr plus(expr const& re) {
4049 }
4050 inline expr option(expr const& re) {
4052 }
4053 inline expr star(expr const& re) {
4055 }
4056 inline expr re_empty(sort const& s) {
4057 Z3_ast r = Z3_mk_re_empty(s.ctx(), s);
4058 s.check_error();
4059 return expr(s.ctx(), r);
4060 }
4061 inline expr re_full(sort const& s) {
4062 Z3_ast r = Z3_mk_re_full(s.ctx(), s);
4063 s.check_error();
4064 return expr(s.ctx(), r);
4065 }
4066 inline expr re_intersect(expr_vector const& args) {
4067 assert(args.size() > 0);
4068 context& ctx = args[0u].ctx();
4069 array<Z3_ast> _args(args);
4070 Z3_ast r = Z3_mk_re_intersect(ctx, _args.size(), _args.ptr());
4071 ctx.check_error();
4072 return expr(ctx, r);
4073 }
4074 inline expr re_diff(expr const& a, expr const& b) {
4075 check_context(a, b);
4076 context& ctx = a.ctx();
4077 Z3_ast r = Z3_mk_re_diff(ctx, a, b);
4078 ctx.check_error();
4079 return expr(ctx, r);
4080 }
4081 inline expr re_complement(expr const& a) {
4083 }
4084 inline expr range(expr const& lo, expr const& hi) {
4085 check_context(lo, hi);
4086 Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
4087 lo.check_error();
4088 return expr(lo.ctx(), r);
4089 }
4090
4091
4092
4093
4094
4095 inline expr_vector context::parse_string(char const* s) {
4096 Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0);
4097 check_error();
4098 return expr_vector(*this, r);
4099
4100 }
4101 inline expr_vector context::parse_file(char const* s) {
4102 Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0);
4103 check_error();
4104 return expr_vector(*this, r);
4105 }
4106
4107 inline expr_vector context::parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls) {
4108 array<Z3_symbol> sort_names(sorts.size());
4109 array<Z3_symbol> decl_names(decls.size());
4110 array<Z3_sort> sorts1(sorts);
4111 array<Z3_func_decl> decls1(decls);
4112 for (unsigned i = 0; i < sorts.size(); ++i) {
4113 sort_names[i] = sorts[i].name();
4114 }
4115 for (unsigned i = 0; i < decls.size(); ++i) {
4116 decl_names[i] = decls[i].name();
4117 }
4118
4119 Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
4120 check_error();
4121 return expr_vector(*this, r);
4122 }
4123
4124 inline expr_vector context::parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls) {
4125 array<Z3_symbol> sort_names(sorts.size());
4126 array<Z3_symbol> decl_names(decls.size());
4127 array<Z3_sort> sorts1(sorts);
4128 array<Z3_func_decl> decls1(decls);
4129 for (unsigned i = 0; i < sorts.size(); ++i) {
4130 sort_names[i] = sorts[i].name();
4131 }
4132 for (unsigned i = 0; i < decls.size(); ++i) {
4133 decl_names[i] = decls[i].name();
4134 }
4135 Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
4136 check_error();
4137 return expr_vector(*this, r);
4138 }
4139
4140 inline func_decl_vector sort::constructors() {
4141 assert(is_datatype());
4142 func_decl_vector cs(ctx());
4143 unsigned n = Z3_get_datatype_sort_num_constructors(ctx(), *this);
4144 for (unsigned i = 0; i < n; ++i)
4145 cs.push_back(func_decl(ctx(), Z3_get_datatype_sort_constructor(ctx(), *this, i)));
4146 return cs;
4147 }
4148
4149 inline func_decl_vector sort::recognizers() {
4150 assert(is_datatype());
4151 func_decl_vector rs(ctx());
4152 unsigned n = Z3_get_datatype_sort_num_constructors(ctx(), *this);
4153 for (unsigned i = 0; i < n; ++i)
4154 rs.push_back(func_decl(ctx(), Z3_get_datatype_sort_recognizer(ctx(), *this, i)));
4155 return rs;
4156 }
4157
4158 inline func_decl_vector func_decl::accessors() {
4159 sort s = range();
4160 assert(s.is_datatype());
4161 unsigned n = Z3_get_datatype_sort_num_constructors(ctx(), s);
4162 unsigned idx = 0;
4163 for (; idx < n; ++idx) {
4164 func_decl f(ctx(), Z3_get_datatype_sort_constructor(ctx(), s, idx));
4165 if (id() == f.id())
4166 break;
4167 }
4168 assert(idx < n);
4169 n = arity();
4170 func_decl_vector as(ctx());
4171 for (unsigned i = 0; i < n; ++i)
4172 as.push_back(func_decl(ctx(), Z3_get_datatype_sort_constructor_accessor(ctx(), s, idx, i)));
4173 return as;
4174 }
4175
4176
4177 inline expr expr::substitute(expr_vector const& src, expr_vector const& dst) {
4178 assert(src.size() == dst.size());
4179 array<Z3_ast> _src(src.size());
4180 array<Z3_ast> _dst(dst.size());
4181 for (unsigned i = 0; i < src.size(); ++i) {
4182 _src[i] = src[i];
4183 _dst[i] = dst[i];
4184 }
4185 Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
4186 check_error();
4187 return expr(ctx(), r);
4188 }
4189
4190 inline expr expr::substitute(expr_vector const& dst) {
4191 array<Z3_ast> _dst(dst.size());
4192 for (unsigned i = 0; i < dst.size(); ++i) {
4193 _dst[i] = dst[i];
4194 }
4195 Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
4196 check_error();
4197 return expr(ctx(), r);
4198 }
4199
4200 inline expr expr::substitute(func_decl_vector const& funs, expr_vector const& dst) {
4201 array<Z3_ast> _dst(dst.size());
4202 array<Z3_func_decl> _funs(funs.size());
4203 if (dst.size() != funs.size()) {
4204 Z3_THROW(exception("length of argument lists don't align"));
4205 return expr(ctx(), nullptr);
4206 }
4207 for (unsigned i = 0; i < dst.size(); ++i) {
4208 _dst[i] = dst[i];
4209 _funs[i] = funs[i];
4210 }
4211 Z3_ast r = Z3_substitute_funs(ctx(), m_ast, dst.size(), _funs.ptr(), _dst.ptr());
4212 check_error();
4213 return expr(ctx(), r);
4214 }
4215
4216 typedef std::function<void(expr const& proof, expr_vector const& clause)> on_clause_eh_t;
4217
4218 class on_clause {
4219 context& c;
4220 on_clause_eh_t m_on_clause;
4221
4222 static void _on_clause_eh(void* _ctx, Z3_ast _proof, Z3_ast_vector _literals) {
4223 on_clause* ctx = static_cast<on_clause*>(_ctx);
4224 expr_vector lits(ctx->c, _literals);
4225 expr proof(ctx->c, _proof);
4226 ctx->m_on_clause(proof, lits);
4227 }
4228 public:
4229 on_clause(solver& s, on_clause_eh_t& on_clause_eh): c(s.ctx()) {
4230 m_on_clause = on_clause_eh;
4231 Z3_solver_register_on_clause(c, s, this, _on_clause_eh);
4232 c.check_error();
4233 }
4234 };
4235
4236 class user_propagator_base {
4237
4238 typedef std::function<void(expr const&, expr const&)> fixed_eh_t;
4239 typedef std::function<void(void)> final_eh_t;
4240 typedef std::function<void(expr const&, expr const&)> eq_eh_t;
4241 typedef std::function<void(expr const&)> created_eh_t;
4242 typedef std::function<void(expr&, unsigned&, Z3_lbool&)> decide_eh_t;
4243
4244 final_eh_t m_final_eh;
4245 eq_eh_t m_eq_eh;
4246 fixed_eh_t m_fixed_eh;
4247 created_eh_t m_created_eh;
4248 decide_eh_t m_decide_eh;
4249 solver* s;
4250 context* c;
4251 std::vector<z3::context*> subcontexts;
4252
4253 Z3_solver_callback cb { nullptr };
4254
4255 struct scoped_cb {
4256 user_propagator_base& p;
4257 scoped_cb(void* _p, Z3_solver_callback cb):p(*static_cast<user_propagator_base*>(_p)) {
4258 p.cb = cb;
4259 }
4260 ~scoped_cb() {
4261 p.cb = nullptr;
4262 }
4263 };
4264
4265 static void push_eh(void* _p, Z3_solver_callback cb) {
4266 user_propagator_base* p = static_cast<user_propagator_base*>(_p);
4267 scoped_cb _cb(p, cb);
4268 static_cast<user_propagator_base*>(p)->push();
4269 }
4270
4271 static void pop_eh(void* _p, Z3_solver_callback cb, unsigned num_scopes) {
4272 user_propagator_base* p = static_cast<user_propagator_base*>(_p);
4273 scoped_cb _cb(p, cb);
4274 static_cast<user_propagator_base*>(_p)->pop(num_scopes);
4275 }
4276
4277 static void* fresh_eh(void* _p, Z3_context ctx) {
4278 user_propagator_base* p = static_cast<user_propagator_base*>(_p);
4279 context* c = new context(ctx);
4280 p->subcontexts.push_back(c);
4281 return p->fresh(*c);
4282 }
4283
4284 static void fixed_eh(void* _p, Z3_solver_callback cb, Z3_ast _var, Z3_ast _value) {
4285 user_propagator_base* p = static_cast<user_propagator_base*>(_p);
4286 scoped_cb _cb(p, cb);
4287 expr value(p->ctx(), _value);
4288 expr var(p->ctx(), _var);
4289 p->m_fixed_eh(var, value);
4290 }
4291
4292 static void eq_eh(void* _p, Z3_solver_callback cb, Z3_ast _x, Z3_ast _y) {
4293 user_propagator_base* p = static_cast<user_propagator_base*>(_p);
4294 scoped_cb _cb(p, cb);
4295 expr x(p->ctx(), _x), y(p->ctx(), _y);
4296 p->m_eq_eh(x, y);
4297 }
4298
4299 static void final_eh(void* p, Z3_solver_callback cb) {
4300 scoped_cb _cb(p, cb);
4301 static_cast<user_propagator_base*>(p)->m_final_eh();
4302 }
4303
4304 static void created_eh(void* _p, Z3_solver_callback cb, Z3_ast _e) {
4305 user_propagator_base* p = static_cast<user_propagator_base*>(_p);
4306 scoped_cb _cb(p, cb);
4307 expr e(p->ctx(), _e);
4308 p->m_created_eh(e);
4309 }
4310
4311 static void decide_eh(void* _p, Z3_solver_callback cb, Z3_ast* _val, unsigned* bit, Z3_lbool* is_pos) {
4312 user_propagator_base* p = static_cast<user_propagator_base*>(_p);
4313 scoped_cb _cb(p, cb);
4314 expr val(p->ctx(), *_val);
4315 p->m_decide_eh(val, *bit, *is_pos);
4316 // TBD: life time of val is within the scope of this callback.
4317 *_val = val;
4318 }
4319
4320 public:
4321 user_propagator_base(context& c) : s(nullptr), c(&c) {}
4322
4323 user_propagator_base(solver* s): s(s), c(nullptr) {
4324 Z3_solver_propagate_init(ctx(), *s, this, push_eh, pop_eh, fresh_eh);
4325 }
4326
4327 virtual void push() = 0;
4328 virtual void pop(unsigned num_scopes) = 0;
4329
4330 virtual ~user_propagator_base() {
4331 for (auto& subcontext : subcontexts) {
4332 subcontext->detach(); // detach first; the subcontexts will be freed internally!
4333 delete subcontext;
4334 }
4335 }
4336
4337 context& ctx() {
4338 return c ? *c : s->ctx();
4339 }
4340
4349 virtual user_propagator_base* fresh(context& ctx) = 0;
4350
4357 void register_fixed(fixed_eh_t& f) {
4358 m_fixed_eh = f;
4359 if (s) {
4360 Z3_solver_propagate_fixed(ctx(), *s, fixed_eh);
4361 }
4362 }
4363
4364 void register_fixed() {
4365 m_fixed_eh = [this](expr const &id, expr const &e) {
4366 fixed(id, e);
4367 };
4368 if (s) {
4369 Z3_solver_propagate_fixed(ctx(), *s, fixed_eh);
4370 }
4371 }
4372
4373 void register_eq(eq_eh_t& f) {
4374 m_eq_eh = f;
4375 if (s) {
4376 Z3_solver_propagate_eq(ctx(), *s, eq_eh);
4377 }
4378 }
4379
4380 void register_eq() {
4381 m_eq_eh = [this](expr const& x, expr const& y) {
4382 eq(x, y);
4383 };
4384 if (s) {
4385 Z3_solver_propagate_eq(ctx(), *s, eq_eh);
4386 }
4387 }
4388
4397 void register_final(final_eh_t& f) {
4398 m_final_eh = f;
4399 if (s) {
4400 Z3_solver_propagate_final(ctx(), *s, final_eh);
4401 }
4402 }
4403
4404 void register_final() {
4405 m_final_eh = [this]() {
4406 final();
4407 };
4408 if (s) {
4409 Z3_solver_propagate_final(ctx(), *s, final_eh);
4410 }
4411 }
4412
4413 void register_created(created_eh_t& c) {
4414 m_created_eh = c;
4415 if (s) {
4416 Z3_solver_propagate_created(ctx(), *s, created_eh);
4417 }
4418 }
4419
4420 void register_created() {
4421 m_created_eh = [this](expr const& e) {
4422 created(e);
4423 };
4424 if (s) {
4425 Z3_solver_propagate_created(ctx(), *s, created_eh);
4426 }
4427 }
4428
4429 void register_decide(decide_eh_t& c) {
4430 m_decide_eh = c;
4431 if (s) {
4432 Z3_solver_propagate_decide(ctx(), *s, decide_eh);
4433 }
4434 }
4435
4436 void register_decide() {
4437 m_decide_eh = [this](expr& val, unsigned& bit, Z3_lbool& is_pos) {
4438 decide(val, bit, is_pos);
4439 };
4440 if (s) {
4441 Z3_solver_propagate_decide(ctx(), *s, decide_eh);
4442 }
4443 }
4444
4445 virtual void fixed(expr const& /*id*/, expr const& /*e*/) { }
4446
4447 virtual void eq(expr const& /*x*/, expr const& /*y*/) { }
4448
4449 virtual void final() { }
4450
4451 virtual void created(expr const& /*e*/) {}
4452
4453 virtual void decide(expr& /*val*/, unsigned& /*bit*/, Z3_lbool& /*is_pos*/) {}
4454
4455 void next_split(expr const & e, unsigned idx, Z3_lbool phase) {
4456 assert(cb);
4457 Z3_solver_next_split(ctx(), cb, e, idx, phase);
4458 }
4459
4474 void add(expr const& e) {
4475 if (cb)
4476 Z3_solver_propagate_register_cb(ctx(), cb, e);
4477 else if (s)
4478 Z3_solver_propagate_register(ctx(), *s, e);
4479 else
4480 assert(false);
4481 }
4482
4483 void conflict(expr_vector const& fixed) {
4484 assert(cb);
4485 expr conseq = ctx().bool_val(false);
4486 array<Z3_ast> _fixed(fixed);
4487 Z3_solver_propagate_consequence(ctx(), cb, fixed.size(), _fixed.ptr(), 0, nullptr, nullptr, conseq);
4488 }
4489
4490 void conflict(expr_vector const& fixed, expr_vector const& lhs, expr_vector const& rhs) {
4491 assert(cb);
4492 assert(lhs.size() == rhs.size());
4493 expr conseq = ctx().bool_val(false);
4494 array<Z3_ast> _fixed(fixed);
4495 array<Z3_ast> _lhs(lhs);
4496 array<Z3_ast> _rhs(rhs);
4497 Z3_solver_propagate_consequence(ctx(), cb, fixed.size(), _fixed.ptr(), lhs.size(), _lhs.ptr(), _rhs.ptr(), conseq);
4498 }
4499
4500 void propagate(expr_vector const& fixed, expr const& conseq) {
4501 assert(cb);
4502 assert((Z3_context)conseq.ctx() == (Z3_context)ctx());
4503 array<Z3_ast> _fixed(fixed);
4504 Z3_solver_propagate_consequence(ctx(), cb, _fixed.size(), _fixed.ptr(), 0, nullptr, nullptr, conseq);
4505 }
4506
4507 void propagate(expr_vector const& fixed,
4508 expr_vector const& lhs, expr_vector const& rhs,
4509 expr const& conseq) {
4510 assert(cb);
4511 assert((Z3_context)conseq.ctx() == (Z3_context)ctx());
4512 assert(lhs.size() == rhs.size());
4513 array<Z3_ast> _fixed(fixed);
4514 array<Z3_ast> _lhs(lhs);
4515 array<Z3_ast> _rhs(rhs);
4516
4517 Z3_solver_propagate_consequence(ctx(), cb, _fixed.size(), _fixed.ptr(), lhs.size(), _lhs.ptr(), _rhs.ptr(), conseq);
4518 }
4519 };
4520
4521}
4522
4525#undef Z3_THROW
4526
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition z3++.h:3427
expr num_val(int n, sort const &s)
Definition z3++.h:3776
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition z3++.h:3654
expr bool_val(bool b)
Definition z3++.h:3740
expr int_val(int n)
Definition z3++.h:3742
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition z3++.h:3583
Z3_error_code check_error() const
Definition z3++.h:474
context & ctx() const
Definition z3++.h:473
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_pbeq(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
Z3_ast_vector Z3_API Z3_optimize_get_assertions(Z3_context c, Z3_optimize o)
Return the set of asserted formulas on the optimization context.
Z3_ast Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a)
Return the interpretation (i.e., assignment) of constant a in the model m. Return NULL,...
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
Z3_simplifier Z3_API Z3_simplifier_and_then(Z3_context c, Z3_simplifier t1, Z3_simplifier t2)
Return a simplifier that applies t1 to a given goal and t2 to every subgoal produced by t1.
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_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const *domain, Z3_sort range)
Create an array type with N arguments.
Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.
Z3_parameter_kind Z3_API Z3_get_decl_parameter_kind(Z3_context c, Z3_func_decl d, unsigned idx)
Return the parameter type associated with a declaration.
bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nor.
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.
void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p)
Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p.
Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f)
Return the 'else' value of the given function interpretation.
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.
void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d)
Increment the reference counter of the given fixedpoint context.
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.
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)
Create the constant array.
void Z3_API Z3_simplifier_inc_ref(Z3_context c, Z3_simplifier t)
Increment the reference counter of the given simplifier.
void Z3_API Z3_fixedpoint_add_rule(Z3_context c, Z3_fixedpoint d, Z3_ast rule, Z3_symbol name)
Add a universal Horn clause as a named rule. The horn_rule should be of the form:
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_vector Z3_API Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o)
Retrieve the unsat core for the last Z3_optimize_check The unsat core is a subset of the assumptions ...
Z3_sort Z3_API Z3_mk_char_sort(Z3_context c)
Create a sort for unicode characters.
Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re)
Create the regular language [re].
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.
void Z3_API Z3_query_constructor(Z3_context c, Z3_constructor constr, unsigned num_fields, Z3_func_decl *constructor, Z3_func_decl *tester, Z3_func_decl accessors[])
Query constructor for declared functions.
Z3_ast Z3_API Z3_substitute(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const from[], Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs....
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].
Z3_func_decl Z3_API Z3_get_decl_func_decl_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the expression value associated with an expression parameter.
Z3_goal_prec
Z3 custom error handler (See Z3_set_error_handler).
Definition z3_api.h:1384
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,...
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.
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_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Check for subsetness of sets.
Z3_ast Z3_API Z3_mk_int(Z3_context c, int v, Z3_sort ty)
Create a numeral of an int, bit-vector, or finite-domain sort.
Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c, Z3_solver s, Z3_ast_vector assumptions, Z3_ast_vector variables, Z3_ast_vector consequences)
retrieve consequences from solver that determine values of the supplied function symbols.
Z3_ast_vector Z3_API Z3_fixedpoint_from_file(Z3_context c, Z3_fixedpoint f, Z3_string s)
Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context....
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_full_set(Z3_context c, Z3_sort domain)
Create the full set.
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.
void Z3_API Z3_add_rec_def(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast args[], Z3_ast body)
Define the body of a recursive function.
Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s)
Return the parameter description set for the given solver object.
void Z3_API Z3_solver_next_split(Z3_context c, Z3_solver_callback cb, Z3_ast t, unsigned idx, Z3_lbool phase)
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_true(Z3_context c)
Create an AST node representing true.
Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve lower bound value or approximation for the i'th optimization objective.
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_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)
Retrieve the model for the last Z3_optimize_check.
void Z3_API Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r)
Increment the reference counter of the given Z3_apply_result object.
Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast default_value)
Create a fresh func_interp object, add it to a model for a specified function. It has reference count...
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_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.
Z3_param_descrs Z3_API Z3_fixedpoint_get_param_descrs(Z3_context c, Z3_fixedpoint f)
Return the parameter description set for the given fixedpoint object.
Z3_sort Z3_API Z3_mk_real_sort(Z3_context c)
Create the real type.
void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 file with assertions, soft constraints and optimization objectives....
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
Z3_string Z3_API Z3_simplifier_get_help(Z3_context c, Z3_simplifier t)
Return a string containing a description of parameters accepted by the given simplifier.
bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g)
Return true if the given goal contains the formula false.
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_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....
void Z3_API Z3_fixedpoint_update_rule(Z3_context c, Z3_fixedpoint d, Z3_ast a, Z3_symbol name)
Update a named rule. A rule with the same name must have been previously created.
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i)
Return the declaration of the i-th function in the given model.
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.
unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e)
Return the number of arguments in a Z3_func_entry object.
Z3_symbol Z3_API Z3_get_decl_symbol_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the double value associated with an double parameter.
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_fpa_rna(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
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_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].
void Z3_API Z3_simplifier_dec_ref(Z3_context c, Z3_simplifier g)
Decrement the reference counter of the given simplifier.
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point subtraction.
void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a)
Add a new formula a to the given goal. The formula is split according to the following procedure that...
Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e)
Return the value of this point.
Z3_ast_vector Z3_API Z3_fixedpoint_from_string(Z3_context c, Z3_fixedpoint f, Z3_string s)
Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context....
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.
Z3_ast Z3_API Z3_mk_false(Z3_context c)
Create an AST node representing false.
Z3_sort Z3_API Z3_mk_datatype(Z3_context c, Z3_symbol name, unsigned num_constructors, Z3_constructor constructors[])
Create datatype, such as lists, trees, records, enumerations or unions of records....
Z3_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s)
Check whether the assertions in a given solver are consistent or not.
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.
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
Z3_model Z3_API Z3_goal_convert_model(Z3_context c, Z3_goal g, Z3_model m)
Convert a model of the formulas of a goal to a model of an original goal. The model may be null,...
void Z3_API Z3_del_constructor(Z3_context c, Z3_constructor constr)
Reclaim memory allocated to constructor.
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_re_complement(Z3_context c, Z3_ast re)
Create the complement of the regular language re.
Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(Z3_context c, Z3_fixedpoint f)
Retrieve set of background assertions from fixedpoint context.
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas on the solver.
Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t)
Create a new solver that is implemented using the given tactic. The solver supports the commands Z3_s...
Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg)
Take the complement of a set.
bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx)
Return true if the given statistical data is a unsigned integer.
bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx)
Return true if the given statistical data is a double.
Z3_ast Z3_API Z3_mk_fpa_rtn(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m)
Return the number of constants assigned by the given model.
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_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1)
Take conjunction of bits in vector, return vector of length 1.
Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem)
Add an element to a set.
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_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_fpa_rtp(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
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_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.
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition z3_api.h:53
Z3_constructor Z3_API Z3_mk_constructor(Z3_context c, Z3_symbol name, Z3_symbol recognizer, unsigned num_fields, Z3_symbol const field_names[], Z3_sort_opt const sorts[], unsigned sort_refs[])
Create a constructor.
Z3_param_descrs Z3_API Z3_tactic_get_param_descrs(Z3_context c, Z3_tactic t)
Return the parameter description set for the given tactic object.
Z3_sort Z3_API Z3_mk_tuple_sort(Z3_context c, Z3_symbol mk_tuple_name, unsigned num_fields, Z3_symbol const field_names[], Z3_sort const field_sorts[], Z3_func_decl *mk_tuple_decl, Z3_func_decl proj_decl[])
Create a tuple type.
void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e)
Increment the reference counter of the given Z3_func_entry object.
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.
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
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_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2)
Maximum of floating-point numbers.
void Z3_API Z3_optimize_assert_and_track(Z3_context c, Z3_optimize o, Z3_ast a, Z3_ast t)
Assert tracked hard constraint to the optimization context.
unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id)
Assert soft constraint to the optimization context.
Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned division.
Z3_ast_vector Z3_API Z3_solver_get_trail(Z3_context c, Z3_solver s)
Return the trail modulo model conversion, in order of decision level The decision level can be retrie...
Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)
Shift left.
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.
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_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
unsigned Z3_API Z3_goal_num_exprs(Z3_context c, Z3_goal g)
Return the number of formulas, subformulas and terms in the given goal.
Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic)
Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unkn...
Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.
unsigned Z3_API Z3_apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r)
Return the number of subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
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_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.
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,...
Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[])
Create the intersection of the regular languages.
Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, unsigned backtrack_level)
extract a next cube for a solver. The last cube is the constant true or false. The number of (non-con...
Z3_ast Z3_API Z3_mk_u32string(Z3_context c, unsigned len, unsigned const chars[])
Create a string constant out of the string that is passed in It takes the length of the string as wel...
void Z3_API Z3_fixedpoint_add_fact(Z3_context c, Z3_fixedpoint d, Z3_func_decl r, unsigned num_args, unsigned args[])
Add a Database fact.
unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g)
Return the number of formulas in the given goal.
Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_symbol name, unsigned n, Z3_sort *domain, Z3_sort range)
void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s)
Increment the reference counter of the given statistics object.
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_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.
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.
Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort seq)
Create a regular expression sort out of a sequence sort.
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.
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.
void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m)
Decrement the reference counter of the given model.
Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, bool negative)
Create a floating-point infinity of sort s.
void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f)
Increment the reference counter of the given Z3_func_interp object.
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_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name)
create a forward reference to a recursive datatype being declared. The forward reference can be used ...
Z3_solver Z3_API Z3_mk_solver(Z3_context c)
Create a new solver. This solver is a "combined solver" (see combined_solver module) that internally ...
Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s)
Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.
void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g)
Increment the reference counter of the given goal.
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_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s)
Create a floating-point NaN of sort s.
unsigned Z3_API Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t)
Return number of constructors for datatype.
Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve upper bound value or approximation for the i'th optimization objective.
Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[])
Check whether the assertions in the given solver and optional assumptions are consistent or not.
Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than.
Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2)
Arithmetic shift right.
Z3_simplifier Z3_API Z3_simplifier_using_params(Z3_context c, Z3_simplifier t, Z3_params p)
Return a simplifier that applies t using the given set of parameters.
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...
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_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_union(Z3_context c, unsigned n, Z3_ast const args[])
Create the union of the regular languages.
Z3_param_descrs Z3_API Z3_simplifier_get_param_descrs(Z3_context c, Z3_simplifier t)
Return the parameter description set for the given simplifier object.
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the integer value associated with an integer parameter.
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th constructor.
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition z3_api.h:61
Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq)
Create an empty sequence of the sequence sort seq.
Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name)
Return a probe associated with the given name. The complete list of probes may be obtained using the ...
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_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s)
Check if suffix is a suffix of s.
Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target)
Copy a solver s from the context source to the context target.
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)
Create a backtracking point.
unsigned Z3_API Z3_stats_get_uint_value(Z3_context c, Z3_stats s, unsigned idx)
Return the unsigned value of the given statistical data.
void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p)
Increment the reference counter of the given probe.
Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point equality.
void Z3_API Z3_solver_propagate_register_cb(Z3_context c, Z3_solver_callback cb, Z3_ast e)
register an expression to propagate on with the solver. Only expressions of type Bool and type Bit-Ve...
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...
void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a)
Add a constant interpretation.
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d)
Decrement the reference counter of the given fixedpoint context.
Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m)
Convert the given model into a string.
Z3_string Z3_API Z3_tactic_get_help(Z3_context c, Z3_tactic t)
Return a string containing a description of parameters accepted by the given tactic.
void Z3_API Z3_solver_propagate_final(Z3_context c, Z3_solver s, Z3_final_eh final_eh)
register a callback on final check. This provides freedom to the propagator to delay actions or imple...
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition z3_api.h:95
Z3_ast_vector Z3_API Z3_parse_smtlib2_string(Z3_context c, Z3_string str, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Parse the given string using the SMT-LIB2 parser.
Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than or equal.
void Z3_API Z3_solver_register_on_clause(Z3_context c, Z3_solver s, void *user_context, Z3_on_clause_eh on_clause_eh)
register a callback to that retrieves assumed, inferred and deleted clauses during search.
Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g, bool include_names)
Convert a goal into a DIMACS formatted string. The goal must be in CNF. You can convert a goal to CNF...
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
double Z3_API Z3_stats_get_double_value(Z3_context c, Z3_stats s, unsigned idx)
Return the double value of the given statistical data.
Z3_ast Z3_API Z3_mk_fpa_numeral_float(Z3_context c, float v, Z3_sort ty)
Create a numeral of FloatingPoint sort from a float.
Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than.
Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c, Z3_fixedpoint d, Z3_ast query)
Pose a query against the asserted rules.
unsigned Z3_API Z3_goal_depth(Z3_context c, Z3_goal g)
Return the depth of the given goal. It tracks how many transformations were applied to it.
Z3_ast Z3_API Z3_mk_fpa_rtz(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
Z3_simplifier Z3_API Z3_mk_simplifier(Z3_context c, Z3_string name)
Return a simplifier associated with the given name. The complete list of simplifiers may be obtained ...
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned remainder.
void Z3_API Z3_mk_datatypes(Z3_context c, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort sorts[], Z3_constructor_list constructor_lists[])
Create mutually recursive datatypes.
Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s)
Return the set of non units in the solver state.
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_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o)
Return objectives on the optimization context. If the objective function is a max-sat objective it is...
Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset)
Return index of the first occurrence of substr in s starting from offset offset. If s does not contai...
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_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c, Z3_symbol name, unsigned n, Z3_symbol const enum_names[], Z3_func_decl enum_consts[], Z3_func_decl enum_testers[])
Create a enumeration sort.
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_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f)
Retrieve set of rules from fixedpoint context.
Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set)
Check for set membership.
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.
void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g)
Erase all formulas from the given goal.
void Z3_API Z3_func_interp_dec_ref(Z3_context c, Z3_func_interp f)
Decrement the reference counter of the given Z3_func_interp object.
void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)
Decrement the reference counter of the given probe.
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_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s)
Check if prefix is a prefix of s.
Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)
Create a bit-vector type of the given size.
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_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than.
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_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)
Create a new fixedpoint context.
void Z3_API Z3_solver_propagate_init(Z3_context c, Z3_solver s, void *user_context, Z3_push_eh push_eh, Z3_pop_eh pop_eh, Z3_fresh_eh fresh_eh)
register a user-properator with the solver.
Z3_func_decl Z3_API Z3_model_get_const_decl(Z3_context c, Z3_model m, unsigned i)
Return the i-th constant in the given model.
void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g)
Decrement the reference counter of the given tactic.
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)
Create a new incremental solver.
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.
Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c, Z3_string name, Z3_string logic, Z3_string status, Z3_string attributes, unsigned num_assumptions, Z3_ast const assumptions[], Z3_ast formula)
Convert the given benchmark into SMT-LIB formatted string.
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_bv_numeral(Z3_context c, unsigned sz, bool const *bits)
create a bit-vector numeral from a vector of Booleans.
void Z3_API Z3_func_entry_dec_ref(Z3_context c, Z3_func_entry e)
Decrement the reference counter of the given Z3_func_entry object.
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.
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_re_full(Z3_context c, Z3_sort re)
Create an universal regular expression of sort re.
Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2)
Minimum of floating-point numbers.
Z3_model Z3_API Z3_mk_model(Z3_context c)
Create a fresh model object. It has reference count 0.
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.
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,...
Z3_string Z3_API Z3_stats_get_key(Z3_context c, Z3_stats s, unsigned idx)
Return the key (a string) for a particular statistical data.
Z3_ast Z3_API Z3_mk_re_diff(Z3_context c, Z3_ast re1, Z3_ast re2)
Create the difference of regular expressions.
unsigned Z3_API Z3_fixedpoint_get_num_levels(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred)
Query the PDR engine for the maximal levels properties are known about predicate.
Z3_ast Z3_API Z3_mk_int64(Z3_context c, int64_t v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re)
Create an empty regular expression of sort re.
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a string.
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_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g)
Return true if the goal contains false, and it is precise or the product of an over approximation.
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_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.
Z3_ast_vector Z3_API Z3_parse_smtlib2_file(Z3_context c, Z3_string file_name, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Similar to Z3_parse_smtlib2_string, but reads the benchmark from a file.
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_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_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context dst)
translate model from context c to context dst.
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.
void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz, unsigned levels[])
retrieve the decision depth of Boolean literals (variables or their negations). Assumes a check-sat c...
Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred)
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_int2bv(Z3_context c, unsigned n, Z3_ast t1)
Create an n bit bit-vector from the integer argument t1.
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name)
Return a tactic associated with the given name. The complete list of tactics may be obtained using th...
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)
Create a new optimize context.
bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast *v)
Evaluate the AST node t in the given model. Return true if succeeded, and store the result in v.
void Z3_API Z3_del_constructor_list(Z3_context c, Z3_constructor_list clist)
Reclaim memory allocated for constructor list.
Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty)
Create a variable.
Z3_ast Z3_API Z3_substitute_funs(Z3_context c, Z3_ast a, unsigned num_funs, Z3_func_decl const from[], Z3_ast const to[])
Substitute funcions in from with new expressions in to.
Z3_ast Z3_API Z3_func_entry_get_arg(Z3_context c, Z3_func_entry e, unsigned i)
Return an argument of a Z3_func_entry object.
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m)
Return the number of function interpretations in the given model.
Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s)
Retrieve the unsat core for the last Z3_solver_check_assumptions The unsat core is a subset of the as...
void Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback cb, unsigned num_fixed, Z3_ast const *fixed, unsigned num_eqs, Z3_ast const *eq_lhs, Z3_ast const *eq_rhs, Z3_ast conseq)
propagate a consequence based on fixed values. This is a callback a client may invoke during the fixe...
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)
Decrement the reference counter of the given optimize context.
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_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.
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)
Create the empty set.
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re)
Create the regular language re+.
Z3_goal_prec Z3_API Z3_goal_precision(Z3_context c, Z3_goal g)
Return the "precision" of the given goal. Goals can be transformed using over and under approximation...
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1)
Coerce an integer to a real.
Z3_goal Z3_API Z3_mk_goal(Z3_context c, bool models, bool unsat_cores, bool proofs)
Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or trans...
double Z3_API Z3_get_decl_double_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the double value associated with an double parameter.
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_unsigned_int64(Z3_context c, uint64_t v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize t)
Return a string containing a description of parameters accepted by optimize.
Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th recognizer.
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d)
Retrieve statistics information from the last call to Z3_optimize_check.
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_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_solver_get_proof(Z3_context c, Z3_solver s)
Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.
Z3_string Z3_API Z3_get_decl_rational_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the rational value, as a string, associated with a rational parameter.
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a minimization constraint.
Z3_stats Z3_API Z3_fixedpoint_get_statistics(Z3_context c, Z3_fixedpoint d)
Retrieve statistics information from the last call to Z3_fixedpoint_query.
bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a)
Test if there exists an interpretation (i.e., assignment) for a in the model m.
void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t)
Increment the reference counter of the given tactic.
Z3_ast Z3_API Z3_mk_real_int64(Z3_context c, int64_t num, int64_t den)
Create a real from a fraction of int64.
void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a file.
Z3_ast Z3_API Z3_mk_seq_last_index(Z3_context c, Z3_ast s, Z3_ast substr)
Return index of the last occurrence of substr in s. If s does not contain substr, then the value is -...
Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 xor t2.
void Z3_API Z3_solver_propagate_eq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh)
register a callback on expression equalities.
Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string s)
Create a string constant out of the string that is passed in The string may contain escape encoding f...
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...
void Z3_API Z3_apply_result_dec_ref(Z3_context c, Z3_apply_result r)
Decrement the reference counter of the given Z3_apply_result object.
Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort s)
Create a sequence sort out of the sort for the elements.
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a maximization constraint.
Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s)
Return the set of units modulo model conversion.
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i)
Return one of the subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
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...
void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s)
Decrement the reference counter of the given statistics object.
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_func_entry Z3_API Z3_func_interp_get_entry(Z3_context c, Z3_func_interp f, unsigned i)
Return a "point" of the given function interpretation. It represents the value of f in a particular p...
Z3_func_decl Z3_API Z3_mk_rec_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a recursive function.
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
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_sort Z3_API Z3_get_decl_sort_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the sort value associated with a sort parameter.
Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c, unsigned num_constructors, Z3_constructor const constructors[])
Create list of constructors.
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than or equal.
void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh)
register a callback when a new expression with a registered function is used by the solver The regist...
Z3_ast Z3_API Z3_mk_fpa_numeral_double(Z3_context c, double v, Z3_sort ty)
Create a numeral of FloatingPoint sort from a double.
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_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.
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_string Z3_API Z3_fixedpoint_get_reason_unknown(Z3_context c, Z3_fixedpoint d)
Retrieve a string that describes the last status returned by Z3_fixedpoint_query.
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_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f)
Return a string describing all fixedpoint available parameters.
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_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
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].
Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s, bool include_names)
Convert a solver into a DIMACS formatted string.
Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Take the set difference between two sets.
void Z3_API Z3_solver_propagate_decide(Z3_context c, Z3_solver s, Z3_decide_eh decide_eh)
register a callback when the solver decides to split on a registered expression. The callback may set...
Z3_ast Z3_API Z3_mk_lstring(Z3_context c, unsigned len, Z3_string s)
Create a string constant out of the string that is passed in It takes the length of the string as wel...
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_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2)
Logical shift right.
Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the expression value associated with an expression parameter.
double Z3_API Z3_probe_apply(Z3_context c, Z3_probe p, Z3_goal g)
Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0....
void Z3_API Z3_func_interp_set_else(Z3_context c, Z3_func_interp f, Z3_ast else_value)
Return the 'else' value of the given function interpretation.
void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g)
Decrement the reference counter of the given goal.
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
void Z3_API Z3_solver_propagate_register(Z3_context c, Z3_solver s, Z3_ast e)
register an expression to propagate on with the solver. Only expressions of type Bool and type Bit-Ve...
Z3_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const to[])
Substitute the variables in a with the expressions in to. For every i smaller than num_exprs,...
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_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)
Create an array type.
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...
void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m)
Increment the reference counter of the given model.
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point division.
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits)
Create a FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point square root.
bool Z3_API Z3_goal_is_decided_sat(Z3_context c, Z3_goal g)
Return true if the goal is empty, and it is precise or the product of a under approximation.
void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p)
Set parameters on fixedpoint context.
void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives....
Z3_solver Z3_API Z3_solver_add_simplifier(Z3_context c, Z3_solver solver, Z3_simplifier simplifier)
Attach simplifier to a solver. The solver will use the simplifier for incremental pre-processing.
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_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d)
Retrieve a formula that encodes satisfying answers to the query.
void Z3_API Z3_solver_propagate_fixed(Z3_context c, Z3_solver s, Z3_fixed_eh fixed_eh)
register a callback for when an expression is bound to a fixed value. The supported expression types ...
void Z3_API Z3_fixedpoint_register_relation(Z3_context c, Z3_fixedpoint d, Z3_func_decl f)
Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics...
void Z3_API Z3_fixedpoint_add_cover(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property)
Add property about the predicate pred. Add a property of predicate pred at level. It gets pushed forw...
void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value)
add a function entry to a function interpretation.
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
Z3_lbool Z3_API Z3_fixedpoint_query_relations(Z3_context c, Z3_fixedpoint d, unsigned num_relations, Z3_func_decl const relations[])
Pose multiple queries against the asserted rules.
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_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_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.
Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s)
Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the commands Z3_solver_ch...
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_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_ast Z3_API Z3_goal_formula(Z3_context c, Z3_goal g, unsigned idx)
Return a formula from the given goal.
Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[])
Check consistency and produce optimal values.
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.
unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f)
Return the number of entries in the given function interpretation.
Z3_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.
Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(Z3_context c)
Create the RoundingMode sort.
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_fpa_rne(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
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_func_interp Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f)
Return the interpretation of the function f in the model m. Return NULL, if the model does not assign...
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.
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.
bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.
Z3_sort Z3_API Z3_mk_string_sort(Z3_context c)
Create a sort for unicode strings.
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor_accessor(Z3_context c, Z3_sort t, unsigned idx_c, unsigned idx_a)
Return idx_a'th accessor for the idx_c'th constructor.
Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1)
Take disjunction of bits in vector, return vector of length 1.
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
@ Z3_APP_AST
Definition z3_api.h:142
@ Z3_VAR_AST
Definition z3_api.h:143
@ Z3_SORT_AST
Definition z3_api.h:145
@ Z3_NUMERAL_AST
Definition z3_api.h:141
@ Z3_FUNC_DECL_AST
Definition z3_api.h:146
@ Z3_QUANTIFIER_AST
Definition z3_api.h:144
expr set_intersect(expr const &a, expr const &b)
Definition z3++.h:3985
expr re_intersect(expr_vector const &args)
Definition z3++.h:4067
expr store(expr const &a, expr const &i, expr const &v)
Definition z3++.h:3920
expr pw(expr const &a, expr const &b)
Definition z3++.h:1636
expr sbv_to_fpa(expr const &t, sort s)
Definition z3++.h:2060
expr bvneg_no_overflow(expr const &a)
Definition z3++.h:2253
expr indexof(expr const &s, expr const &substr, expr const &offset)
Definition z3++.h:4030
tactic par_or(unsigned n, tactic const *tactics)
Definition z3++.h:3113
tactic par_and_then(tactic const &t1, tactic const &t2)
Definition z3++.h:3122
expr srem(expr const &a, expr const &b)
signed remainder operator for bitvectors
Definition z3++.h:2185
expr bvadd_no_underflow(expr const &a, expr const &b)
Definition z3++.h:2241
expr prefixof(expr const &a, expr const &b)
Definition z3++.h:4024
expr sum(expr_vector const &args)
Definition z3++.h:2437
expr ugt(expr const &a, expr const &b)
unsigned greater than operator for bitvectors.
Definition z3++.h:2172
expr operator/(expr const &a, expr const &b)
Definition z3++.h:1802
expr exists(expr const &x, expr const &b)
Definition z3++.h:2348
expr fp_eq(expr const &a, expr const &b)
Definition z3++.h:2021
func_decl tree_order(sort const &a, unsigned index)
Definition z3++.h:2278
expr concat(expr const &a, expr const &b)
Definition z3++.h:2455
expr bvmul_no_underflow(expr const &a, expr const &b)
Definition z3++.h:2259
expr lambda(expr const &x, expr const &b)
Definition z3++.h:2372
ast_vector_tpl< func_decl > func_decl_vector
Definition z3++.h:78
expr fpa_to_fpa(expr const &t, sort s)
Definition z3++.h:2074
expr operator&&(expr const &a, expr const &b)
Definition z3++.h:1680
expr operator!=(expr const &a, expr const &b)
Definition z3++.h:1716
expr operator+(expr const &a, expr const &b)
Definition z3++.h:1728
expr set_complement(expr const &a)
Definition z3++.h:3997
check_result
Definition z3++.h:135
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition z3++.h:3890
expr const_array(sort const &d, expr const &v)
Definition z3++.h:3957
expr min(expr const &a, expr const &b)
Definition z3++.h:1950
expr set_difference(expr const &a, expr const &b)
Definition z3++.h:3993
expr forall(expr const &x, expr const &b)
Definition z3++.h:2324
expr operator>(expr const &a, expr const &b)
Definition z3++.h:1913
sort to_sort(context &c, Z3_sort s)
Definition z3++.h:2115
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...
Definition z3++.h:2106
expr bv2int(expr const &a, bool is_signed)
bit-vector and integer conversions.
Definition z3++.h:2232
expr operator%(expr const &a, expr const &b)
Definition z3++.h:1651
expr operator~(expr const &a)
Definition z3++.h:2028
expr sle(expr const &a, expr const &b)
signed less than or equal to operator for bitvectors.
Definition z3++.h:2128
expr nor(expr const &a, expr const &b)
Definition z3++.h:1948
expr fpa_fp(expr const &sgn, expr const &exp, expr const &sig)
Definition z3++.h:2038
expr bvsub_no_underflow(expr const &a, expr const &b, bool is_signed)
Definition z3++.h:2247
expr mk_xor(expr_vector const &args)
Definition z3++.h:2511
expr lshr(expr const &a, expr const &b)
logic shift right operator for bitvectors
Definition z3++.h:2213
expr operator*(expr const &a, expr const &b)
Definition z3++.h:1758
expr nand(expr const &a, expr const &b)
Definition z3++.h:1947
expr fpa_to_ubv(expr const &t, unsigned sz)
Definition z3++.h:2053
expr bvredor(expr const &a)
Definition z3++.h:1982
ast_vector_tpl< sort > sort_vector
Definition z3++.h:77
func_decl piecewise_linear_order(sort const &a, unsigned index)
Definition z3++.h:2275
expr slt(expr const &a, expr const &b)
signed less than operator for bitvectors.
Definition z3++.h:2134
tactic when(probe const &p, tactic const &t)
Definition z3++.h:3414
expr last_indexof(expr const &s, expr const &substr)
Definition z3++.h:4036
expr int2bv(unsigned n, expr const &a)
Definition z3++.h:2233
expr max(expr const &a, expr const &b)
Definition z3++.h:1966
expr xnor(expr const &a, expr const &b)
Definition z3++.h:1949
expr udiv(expr const &a, expr const &b)
unsigned division operator for bitvectors.
Definition z3++.h:2178
expr abs(expr const &a)
Definition z3++.h:1994
expr pbge(expr_vector const &es, int const *coeffs, int bound)
Definition z3++.h:2405
expr round_fpa_to_closest_integer(expr const &t)
Definition z3++.h:2081
expr distinct(expr_vector const &args)
Definition z3++.h:2446
expr ashr(expr const &a, expr const &b)
arithmetic shift right operator for bitvectors
Definition z3++.h:2220
expr bvmul_no_overflow(expr const &a, expr const &b, bool is_signed)
Definition z3++.h:2256
expr bvsub_no_overflow(expr const &a, expr const &b)
Definition z3++.h:2244
expr star(expr const &re)
Definition z3++.h:4054
expr urem(expr const &a, expr const &b)
unsigned reminder operator for bitvectors
Definition z3++.h:2199
tactic repeat(tactic const &t, unsigned max=UINT_MAX)
Definition z3++.h:3097
expr mod(expr const &a, expr const &b)
Definition z3++.h:1640
expr fma(expr const &a, expr const &b, expr const &c, expr const &rm)
Definition z3++.h:2030
check_result to_check_result(Z3_lbool l)
Definition z3++.h:147
expr mk_or(expr_vector const &args)
Definition z3++.h:2499
expr to_re(expr const &s)
Definition z3++.h:4042
void check_context(object const &a, object const &b)
Definition z3++.h:477
std::ostream & operator<<(std::ostream &out, exception const &e)
Definition z3++.h:97
expr ule(expr const &a, expr const &b)
unsigned less than or equal to operator for bitvectors.
Definition z3++.h:2154
func_decl to_func_decl(context &c, Z3_func_decl f)
Definition z3++.h:2120
tactic with(tactic const &t, params const &p)
Definition z3++.h:3103
expr ite(expr const &c, expr const &t, expr const &e)
Create the if-then-else expression ite(c, t, e)
Definition z3++.h:2093
expr ult(expr const &a, expr const &b)
unsigned less than operator for bitvectors.
Definition z3++.h:2160
expr pbeq(expr_vector const &es, int const *coeffs, int bound)
Definition z3++.h:2413
expr operator^(expr const &a, expr const &b)
Definition z3++.h:1939
expr operator<=(expr const &a, expr const &b)
Definition z3++.h:1866
expr set_union(expr const &a, expr const &b)
Definition z3++.h:3977
expr operator>=(expr const &a, expr const &b)
Definition z3++.h:1782
func_decl linear_order(sort const &a, unsigned index)
Definition z3++.h:2269
expr sqrt(expr const &a, expr const &rm)
Definition z3++.h:2014
expr pble(expr_vector const &es, int const *coeffs, int bound)
Definition z3++.h:2397
expr operator==(expr const &a, expr const &b)
Definition z3++.h:1705
expr full_set(sort const &s)
Definition z3++.h:3965
expr smod(expr const &a, expr const &b)
signed modulus operator for bitvectors
Definition z3++.h:2192
expr implies(expr const &a, expr const &b)
Definition z3++.h:1628
expr empty_set(sort const &s)
Definition z3++.h:3961
expr in_re(expr const &s, expr const &re)
Definition z3++.h:4045
expr bvadd_no_overflow(expr const &a, expr const &b, bool is_signed)
bit-vector overflow/underflow checks
Definition z3++.h:2238
expr suffixof(expr const &a, expr const &b)
Definition z3++.h:4018
expr re_diff(expr const &a, expr const &b)
Definition z3++.h:4075
expr set_add(expr const &s, expr const &e)
Definition z3++.h:3969
expr plus(expr const &re)
Definition z3++.h:4048
expr set_subset(expr const &a, expr const &b)
Definition z3++.h:4005
expr select(expr const &a, expr const &i)
forward declarations
Definition z3++.h:3903
expr bvredand(expr const &a)
Definition z3++.h:1988
expr operator&(expr const &a, expr const &b)
Definition z3++.h:1935
expr operator-(expr const &a)
Definition z3++.h:1824
expr set_member(expr const &s, expr const &e)
Definition z3++.h:4001
expr bvsdiv_no_overflow(expr const &a, expr const &b)
Definition z3++.h:2250
tactic try_for(tactic const &t, unsigned ms)
Definition z3++.h:3108
func_decl partial_order(sort const &a, unsigned index)
Definition z3++.h:2272
ast_vector_tpl< expr > expr_vector
Definition z3++.h:76
expr rem(expr const &a, expr const &b)
Definition z3++.h:1656
expr sge(expr const &a, expr const &b)
signed greater than or equal to operator for bitvectors.
Definition z3++.h:2140
expr operator!(expr const &a)
Definition z3++.h:1674
expr re_empty(sort const &s)
Definition z3++.h:4057
expr mk_and(expr_vector const &args)
Definition z3++.h:2505
@ RNE
Definition z3++.h:141
@ RNA
Definition z3++.h:140
@ RTZ
Definition z3++.h:144
@ RTN
Definition z3++.h:143
@ RTP
Definition z3++.h:142
expr sext(expr const &a, unsigned i)
Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i,...
Definition z3++.h:2267
expr to_real(expr const &a)
Definition z3++.h:3860
expr shl(expr const &a, expr const &b)
shift left operator for bitvectors
Definition z3++.h:2206
expr operator||(expr const &a, expr const &b)
Definition z3++.h:1692
std::function< void(expr const &proof, expr_vector const &clause)> on_clause_eh_t
Definition z3++.h:4217
expr set_del(expr const &s, expr const &e)
Definition z3++.h:3973
expr ubv_to_fpa(expr const &t, sort s)
Definition z3++.h:2067
tactic cond(probe const &p, tactic const &t1, tactic const &t2)
Definition z3++.h:3420
expr as_array(func_decl &f)
Definition z3++.h:3940
expr sgt(expr const &a, expr const &b)
signed greater than operator for bitvectors.
Definition z3++.h:2146
expr fpa_to_sbv(expr const &t, unsigned sz)
Definition z3++.h:2046
expr operator|(expr const &a, expr const &b)
Definition z3++.h:1943
expr atmost(expr_vector const &es, unsigned bound)
Definition z3++.h:2421
expr range(expr const &lo, expr const &hi)
Definition z3++.h:4085
expr zext(expr const &a, unsigned i)
Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i,...
Definition z3++.h:2227
expr atleast(expr_vector const &es, unsigned bound)
Definition z3++.h:2429
expr uge(expr const &a, expr const &b)
unsigned greater than or equal to operator for bitvectors.
Definition z3++.h:2166
expr operator<(expr const &a, expr const &b)
Definition z3++.h:1891
expr option(expr const &re)
Definition z3++.h:4051
expr re_full(sort const &s)
Definition z3++.h:4062
expr re_complement(expr const &a)
Definition z3++.h:4082
expr empty(sort const &s)
Definition z3++.h:4013
tactic fail_if(probe const &p)
Definition z3++.h:3409
on_clause_eh(ctx, p, clause)
Definition z3py.py:11398
_on_clause_eh
Definition z3py.py:11404
is_int(a)
Definition z3py.py:2682
eq(a, b)
Definition z3py.py:472
#define _Z3_MK_BIN_(a, b, binop)
Definition z3++.h:1621
#define MK_EXPR1(_fn, _arg)
Definition z3++.h:3946
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition z3++.h:3951
#define Z3_THROW(x)
Definition z3++.h:103
#define _Z3_MK_UN_(a, mkun)
Definition z3++.h:1668

◆ _Z3_MK_UN_

#define _Z3_MK_UN_ (   a,
  mkun 
)
Value:
Z3_ast r = mkun(a.ctx(), a); \
a.check_error(); \
return expr(a.ctx(), r); \

Definition at line 1668 of file z3++.h.

◆ MK_EXPR1

#define MK_EXPR1 (   _fn,
  _arg 
)
Value:
Z3_ast r = _fn(_arg.ctx(), _arg); \
_arg.check_error(); \
return expr(_arg.ctx(), r);

Definition at line 3946 of file z3++.h.

◆ MK_EXPR2

#define MK_EXPR2 (   _fn,
  _arg1,
  _arg2 
)
Value:
check_context(_arg1, _arg2); \
Z3_ast r = _fn(_arg1.ctx(), _arg1, _arg2); \
_arg1.check_error(); \
return expr(_arg1.ctx(), r);

Definition at line 3951 of file z3++.h.

◆ Z3_THROW

#define Z3_THROW (   x)    {}

Definition at line 103 of file z3++.h.