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
 
struct  optimize::translate
 
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 sdiv (expr const &a, expr const &b)
 signed division operator for bitvectors.
 
expr sdiv (expr const &a, int b)
 
expr sdiv (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 1639 of file z3++.h.

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

◆ _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 1686 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 4046 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 4051 of file z3++.h.

◆ Z3_THROW

#define Z3_THROW (   x)    {}

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

Generated on Sat Dec 20 2025 19:33:22 for Z3 by doxygen 1.9.8