92 char const *
msg()
const {
return m_msg.c_str(); }
93 char const *
what()
const throw() {
return m_msg.c_str(); }
98 #if !defined(Z3_THROW)
99 #if __cpp_exceptions || _CPPUNWIND || __EXCEPTIONS
100 #define Z3_THROW(x) throw x
102 #define Z3_THROW(x) {}
116 operator Z3_config()
const {
return m_cfg; }
128 void set(
char const * param,
int value) {
129 auto str = std::to_string(value);
161 bool m_enable_exceptions =
true;
169 m_enable_exceptions =
true;
170 m_rounding_mode =
RNE;
180 void detach() { m_ctx =
nullptr; }
223 void set(
char const * param,
int value) {
224 auto str = std::to_string(value);
292 template<
size_t precision>
382 expr fpa_const(
char const * name,
unsigned ebits,
unsigned sbits);
384 template<
size_t precision>
442 std::unique_ptr<T[]> m_array;
447 array(
unsigned sz):m_array(new T[sz]),m_size(sz) {}
448 template<
typename T2>
450 void resize(
unsigned sz) { m_array.reset(
new T[sz]); m_size = sz; }
451 unsigned size()
const {
return m_size; }
452 T &
operator[](
int i) { assert(0 <= i); assert(
static_cast<unsigned>(i) < m_size);
return m_array[i]; }
453 T
const &
operator[](
int i)
const { assert(0 <= i); assert(
static_cast<unsigned>(i) < m_size);
return m_array[i]; }
454 T
const *
ptr()
const {
return m_array.get(); }
455 T *
ptr() {
return m_array.get(); }
465 friend void check_context(
object const & a,
object const & b);
482 out <<
"k!" << s.
to_int();
490 Z3_param_descrs m_descrs;
497 m_descrs = o.m_descrs;
498 object::operator=(o);
524 object::operator=(s);
525 m_params = s.m_params;
549 operator bool()
const {
return m_ast != 0; }
554 object::operator=(s);
560 friend std::ostream &
operator<<(std::ostream & out,
ast const & n);
567 friend bool eq(
ast const & a,
ast const & b);
597 object::operator=(s);
598 m_vector = s.m_vector;
620 return other.m_index == m_index;
623 return other.m_index != m_index;
790 expr
select(expr
const & a, expr
const& i);
1058 assert(
ctx().enable_exceptions());
1059 if (!
ctx().enable_exceptions())
return 0;
1076 unsigned result = 0;
1078 assert(
ctx().enable_exceptions());
1079 if (!
ctx().enable_exceptions())
return 0;
1095 assert(
ctx().enable_exceptions());
1096 if (!
ctx().enable_exceptions())
return 0;
1110 uint64_t result = 0;
1112 assert(
ctx().enable_exceptions());
1113 if (!
ctx().enable_exceptions())
return 0;
1154 return std::string(s);
1204 for (
unsigned i = 0; i < argCnt; i++)
1553 return select(*
this, index);
1559 return select(*
this, index);
1593 return i == other.i;
1596 return i != other.i;
1608 #define _Z3_MK_BIN_(a, b, binop) \
1609 check_context(a, b); \
1610 Z3_ast r = binop(a.ctx(), a, b); \
1612 return expr(a.ctx(), r); \
1655 #define _Z3_MK_UN_(a, mkun) \
1656 Z3_ast r = mkun(a.ctx(), a); \
1658 return expr(a.ctx(), r); \
1670 Z3_ast args[2] = { a, b };
1682 Z3_ast args[2] = { a, b };
1705 Z3_ast args[2] = { a, b };
1719 Z3_ast args[2] = { a, b };
1729 Z3_ast _args[2] = { a, b };
1749 Z3_ast args[2] = { a, b };
1816 else if (a.
is_bv()) {
1834 Z3_ast args[2] = { a, b };
1943 else if (a.
is_bv()) {
1959 else if (a.
is_bv()) {
1985 expr ge = a >= zero;
1991 expr ge = a >= zero;
2301 template<
typename T>
2302 template<
typename T2>
2304 for (
unsigned i = 0; i < m_size; i++) {
2385 assert(es.
size() > 0);
2390 return expr(ctx, r);
2393 assert(es.
size() > 0);
2398 return expr(ctx, r);
2401 assert(es.
size() > 0);
2406 return expr(ctx, r);
2409 assert(es.
size() > 0);
2414 return expr(ctx, r);
2417 assert(es.
size() > 0);
2422 return expr(ctx, r);
2425 assert(args.
size() > 0);
2430 return expr(ctx, r);
2434 assert(args.
size() > 0);
2439 return expr(ctx, r);
2446 Z3_ast _args[2] = { a, b };
2450 Z3_ast _args[2] = { a, b };
2462 assert(args.
size() > 0);
2463 if (args.
size() == 1) {
2475 r = _args[args.
size()-1];
2476 for (
unsigned i = args.
size()-1; i > 0; ) {
2483 return expr(ctx, r);
2502 for (
unsigned i = 1; i < args.
size(); ++i)
2522 object::operator=(s);
2523 m_entry = s.m_entry;
2545 object::operator=(s);
2546 m_interp = s.m_interp;
2579 object::operator=(s);
2580 m_model = s.m_model;
2589 if (status ==
false &&
ctx().enable_exceptions())
2638 friend std::ostream &
operator<<(std::ostream & out,
model const & m);
2659 object::operator=(s);
2660 m_stats = s.m_stats;
2669 friend std::ostream &
operator<<(std::ostream & out,
stats const & s);
2675 if (r ==
unsat) out <<
"unsat";
2676 else if (r ==
sat) out <<
"sat";
2677 else out <<
"unknown";
2703 object::operator=(s);
2704 m_solver = s.m_solver;
2723 add(e,
ctx().bool_const(p));
2727 for (
unsigned i = 0; i < v.
size(); ++i)
2736 for (
unsigned i = 0; i < n; i++) {
2738 _assumptions[i] = assumptions[i];
2745 unsigned n = assumptions.
size();
2747 for (
unsigned i = 0; i < n; i++) {
2749 _assumptions[i] = assumptions[i];
2772 unsigned sz = result.
size();
2781 std::string
to_smt2(
char const* status =
"unknown") {
2785 unsigned sz = es.
size();
2821 assert(!m_end && !m_empty);
2822 m_cube = m_solver.
cube(m_vars, m_cutoff);
2823 m_cutoff = 0xFFFFFFFF;
2824 if (m_cube.
size() == 1 && m_cube[0u].is_false()) {
2828 else if (m_cube.
empty()) {
2860 return other.m_end == m_end;
2863 return other.m_end != m_end;
2876 m_cutoff(0xFFFFFFFF),
2877 m_default_vars(s.
ctx()),
2878 m_vars(m_default_vars)
2883 m_cutoff(0xFFFFFFFF),
2884 m_default_vars(s.
ctx()),
2901 void init(Z3_goal s) {
2910 operator Z3_goal()
const {
return m_goal; }
2914 object::operator=(s);
2941 unsigned n =
size();
2948 for (
unsigned i = 0; i < n; i++)
2949 args[i] =
operator[](i);
2954 friend std::ostream &
operator<<(std::ostream & out,
goal const & g);
2959 Z3_apply_result m_apply_result;
2960 void init(Z3_apply_result s) {
2968 operator Z3_apply_result()
const {
return m_apply_result; }
2972 object::operator=(s);
2973 m_apply_result = s.m_apply_result;
2984 void init(Z3_tactic s) {
2993 operator Z3_tactic()
const {
return m_tactic; }
2997 object::operator=(s);
2998 m_tactic = s.m_tactic;
3054 Z3_THROW(
exception(
"a non-zero number of tactics need to be passed to par_or"));
3057 for (
unsigned i = 0; i < n; ++i) buffer[i] =
tactics[i];
3070 void init(Z3_probe s) {
3080 operator Z3_probe()
const {
return m_probe; }
3084 object::operator=(s);
3085 m_probe = s.m_probe;
3153 unsigned h()
const {
return m_h; }
3164 for (expr_vector::iterator it = v.
begin(); it != v.
end(); ++it)
minimize(*it);
3170 object::operator=(o);
3174 operator Z3_optimize()
const {
return m_opt; }
3180 for (expr_vector::iterator it = es.
begin(); it != es.
end(); ++it)
add(*it);
3188 add(e,
ctx().bool_const(p));
3192 auto str = std::to_string(weight);
3216 unsigned n = asms.
size();
3218 for (
unsigned i = 0; i < n; i++) {
3259 object::operator=(o);
3262 operator Z3_fixedpoint()
const {
return m_fp; }
3359 for (
unsigned i = 0; i < n; i++) { _enum_names[i] =
Z3_mk_string_symbol(*
this, enum_names[i]); }
3371 for (
unsigned i = 0; i < n; i++) { _names[i] =
Z3_mk_string_symbol(*
this, names[i]); _sorts[i] = sorts[i]; }
3383 Z3_constructor_list clist;
3387 operator Z3_constructor_list()
const {
return clist; }
3393 std::vector<Z3_constructor> cons;
3394 std::vector<unsigned> num_fields;
3399 for (
auto con : cons)
3407 for (
unsigned i = 0; i < n; ++i) sorts[i] = fields[i], _names[i] = names[i];
3409 num_fields.push_back(n);
3414 unsigned size()
const {
return (
unsigned)cons.size(); }
3427 constructor =
func_decl(ctx, _constructor);
3430 for (
unsigned j = 0; j < num_fields[i]; ++j)
3437 for (
unsigned i = 0; i < cs.
size(); ++i)
3444 for (
unsigned i = 0; i < cs.
size(); ++i) _cs[i] = cs[i];
3447 return sort(*
this, s);
3451 unsigned n,
symbol const* names,
3457 for (
unsigned i = 0; i < n; ++i)
3458 _names[i] = names[i], _cons[i] = *cons[i];
3460 for (
unsigned i = 0; i < n; ++i)
3469 return sort(*
this, s);
3483 for (
unsigned i = 0; i < arity; i++) {
3485 args[i] = domain[i];
3498 for (
unsigned i = 0; i < domain.
size(); i++) {
3500 args[i] = domain[i];
3530 Z3_sort args[3] = { d1, d2, d3 };
3538 Z3_sort args[4] = { d1, d2, d3, d4 };
3546 Z3_sort args[5] = { d1, d2, d3, d4, d5 };
3554 for (
unsigned i = 0; i < arity; i++) {
3556 args[i] = domain[i];
3573 sort dom[2] = { d1, d2 };
3594 return expr(*
this, r);
3600 return expr(*
this, r);
3609 template<
size_t precision>
3615 switch (m_rounding_mode) {
3621 default:
return expr(*
this);
3647 for (
unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
3665 for (
unsigned i = 0; i < n; i++) {
3676 for (
unsigned i = 0; i < args.
size(); i++) {