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< ast > ast_vector
 
typedef ast_vector_tpl< expr > expr_vector
 
typedef ast_vector_tpl< sort > sort_vector
 
typedef ast_vector_tpl< func_decl > func_decl_vector
 
typedef std::function< void(expr const &proof, std::vector< unsigned > const &deps, expr_vector const &clause)> on_clause_eh_t
 

Enumerations

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

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 map (expr const &f, expr const &list)
 
expr mapi (expr const &f, expr const &i, expr const &list)
 
expr foldl (expr const &f, expr const &a, expr const &list)
 
expr foldli (expr const &f, expr const &i, expr const &a, expr const &list)
 
expr mk_or (expr_vector const &args)
 
expr mk_and (expr_vector const &args)
 
expr mk_xor (expr_vector const &args)
 
std::ostream & operator<< (std::ostream &out, model const &m)
 
std::ostream & operator<< (std::ostream &out, stats const &s)
 
std::ostream & operator<< (std::ostream &out, check_result r)
 
std::ostream & operator<< (std::ostream &out, solver const &s)
 
std::ostream & operator<< (std::ostream &out, goal const &g)
 
std::ostream & operator<< (std::ostream &out, apply_result const &r)
 
tactic operator& (tactic const &t1, tactic const &t2)
 
tactic operator| (tactic const &t1, tactic const &t2)
 
tactic repeat (tactic const &t, unsigned max=UINT_MAX)
 
tactic with (tactic const &t, params const &p)
 
tactic try_for (tactic const &t, unsigned ms)
 
tactic par_or (unsigned n, tactic const *tactics)
 
tactic par_and_then (tactic const &t1, tactic const &t2)
 
simplifier operator& (simplifier const &t1, simplifier const &t2)
 
simplifier with (simplifier const &t, params const &p)
 
probe operator<= (probe const &p1, probe const &p2)
 
probe operator<= (probe const &p1, double p2)
 
probe operator<= (double p1, probe const &p2)
 
probe operator>= (probe const &p1, probe const &p2)
 
probe operator>= (probe const &p1, double p2)
 
probe operator>= (double p1, probe const &p2)
 
probe operator< (probe const &p1, probe const &p2)
 
probe operator< (probe const &p1, double p2)
 
probe operator< (double p1, probe const &p2)
 
probe operator> (probe const &p1, probe const &p2)
 
probe operator> (probe const &p1, double p2)
 
probe operator> (double p1, probe const &p2)
 
probe operator== (probe const &p1, probe const &p2)
 
probe operator== (probe const &p1, double p2)
 
probe operator== (double p1, probe const &p2)
 
probe operator&& (probe const &p1, probe const &p2)
 
probe operator|| (probe const &p1, probe const &p2)
 
probe operator! (probe const &p)
 
std::ostream & operator<< (std::ostream &out, optimize const &s)
 
std::ostream & operator<< (std::ostream &out, fixedpoint const &f)
 
tactic fail_if (probe const &p)
 
tactic when (probe const &p, tactic const &t)
 
tactic cond (probe const &p, tactic const &t1, tactic const &t2)
 
expr to_real (expr const &a)
 
func_decl function (symbol const &name, unsigned arity, sort const *domain, sort const &range)
 
func_decl function (char const *name, unsigned arity, sort const *domain, sort const &range)
 
func_decl function (char const *name, sort const &domain, sort const &range)
 
func_decl function (char const *name, sort const &d1, sort const &d2, sort const &range)
 
func_decl function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &range)
 
func_decl function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &range)
 
func_decl function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &d5, sort const &range)
 
func_decl function (char const *name, sort_vector const &domain, sort const &range)
 
func_decl function (std::string const &name, sort_vector const &domain, sort const &range)
 
func_decl recfun (symbol const &name, unsigned arity, sort const *domain, sort const &range)
 
func_decl recfun (char const *name, unsigned arity, sort const *domain, sort const &range)
 
func_decl recfun (char const *name, sort const &d1, sort const &range)
 
func_decl recfun (char const *name, sort const &d1, sort const &d2, sort const &range)
 
expr select (expr const &a, int i)
 
expr store (expr const &a, expr const &i, expr const &v)
 
expr store (expr const &a, int i, expr const &v)
 
expr store (expr const &a, expr i, int v)
 
expr store (expr const &a, int i, int v)
 
expr store (expr const &a, expr_vector const &i, expr const &v)
 
expr as_array (func_decl &f)
 
expr const_array (sort const &d, expr const &v)
 
expr empty_set (sort const &s)
 
expr full_set (sort const &s)
 
expr set_add (expr const &s, expr const &e)
 
expr set_del (expr const &s, expr const &e)
 
expr set_union (expr const &a, expr const &b)
 
expr set_intersect (expr const &a, expr const &b)
 
expr set_difference (expr const &a, expr const &b)
 
expr set_complement (expr const &a)
 
expr set_member (expr const &s, expr const &e)
 
expr set_subset (expr const &a, expr const &b)
 
expr empty (sort const &s)
 
expr suffixof (expr const &a, expr const &b)
 
expr prefixof (expr const &a, expr const &b)
 
expr indexof (expr const &s, expr const &substr, expr const &offset)
 
expr last_indexof (expr const &s, expr const &substr)
 
expr to_re (expr const &s)
 
expr in_re (expr const &s, expr const &re)
 
expr plus (expr const &re)
 
expr option (expr const &re)
 
expr star (expr const &re)
 
expr re_empty (sort const &s)
 
expr re_full (sort const &s)
 
expr re_intersect (expr_vector const &args)
 
expr re_diff (expr const &a, expr const &b)
 
expr re_complement (expr const &a)
 
expr range (expr const &lo, expr const &hi)
 

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 1622 of file z3++.h.

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

◆ _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 1669 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 3997 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 4002 of file z3++.h.

◆ Z3_THROW

#define Z3_THROW (   x)    {}

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

Generated by doxygen 1.9.8