00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021 #ifndef __Z3PP_H_
00022 #define __Z3PP_H_
00023
00024 #include<cassert>
00025 #include<iostream>
00026 #include<string>
00027 #include<sstream>
00028 #include<z3.h>
00029 #include<limits.h>
00030
00036
00041
00045 namespace z3 {
00046
00047 class exception;
00048 class config;
00049 class context;
00050 class symbol;
00051 class params;
00052 class ast;
00053 class sort;
00054 class func_decl;
00055 class expr;
00056 class solver;
00057 class goal;
00058 class tactic;
00059 class probe;
00060 class model;
00061 class func_interp;
00062 class func_entry;
00063 class statistics;
00064 class apply_result;
00065 class fixedpoint;
00066 template<typename T> class ast_vector_tpl;
00067 typedef ast_vector_tpl<ast> ast_vector;
00068 typedef ast_vector_tpl<expr> expr_vector;
00069 typedef ast_vector_tpl<sort> sort_vector;
00070 typedef ast_vector_tpl<func_decl> func_decl_vector;
00071
00072 inline void set_param(char const * param, char const * value) { Z3_global_param_set(param, value); }
00073 inline void set_param(char const * param, bool value) { Z3_global_param_set(param, value ? "true" : "false"); }
00074 inline void set_param(char const * param, int value) { std::ostringstream oss; oss << value; Z3_global_param_set(param, oss.str().c_str()); }
00075 inline void reset_params() { Z3_global_param_reset_all(); }
00076
00080 class exception {
00081 std::string m_msg;
00082 public:
00083 exception(char const * msg):m_msg(msg) {}
00084 char const * msg() const { return m_msg.c_str(); }
00085 friend std::ostream & operator<<(std::ostream & out, exception const & e) { out << e.msg(); return out; }
00086 };
00087
00088
00089
00093 class config {
00094 Z3_config m_cfg;
00095 config(config const & s);
00096 config & operator=(config const & s);
00097 public:
00098 config() { m_cfg = Z3_mk_config(); }
00099 ~config() { Z3_del_config(m_cfg); }
00100 operator Z3_config() const { return m_cfg; }
00104 void set(char const * param, char const * value) { Z3_set_param_value(m_cfg, param, value); }
00108 void set(char const * param, bool value) { Z3_set_param_value(m_cfg, param, value ? "true" : "false"); }
00112 void set(char const * param, int value) {
00113 std::ostringstream oss;
00114 oss << value;
00115 Z3_set_param_value(m_cfg, param, oss.str().c_str());
00116 }
00117 };
00118
00122 class context {
00123 Z3_context m_ctx;
00124 static void error_handler(Z3_context c, Z3_error_code e) { }
00125 void init(config & c) {
00126 m_ctx = Z3_mk_context_rc(c);
00127 Z3_set_error_handler(m_ctx, error_handler);
00128 Z3_set_ast_print_mode(m_ctx, Z3_PRINT_SMTLIB2_COMPLIANT);
00129 }
00130 context(context const & s);
00131 context & operator=(context const & s);
00132 public:
00133 context() { config c; init(c); }
00134 context(config & c) { init(c); }
00135 ~context() { Z3_del_context(m_ctx); }
00136 operator Z3_context() const { return m_ctx; }
00137
00141 void check_error() const {
00142 Z3_error_code e = Z3_get_error_code(m_ctx);
00143 if (e != Z3_OK)
00144 throw exception(Z3_get_error_msg_ex(m_ctx, e));
00145 }
00146
00150 void set(char const * param, char const * value) { Z3_update_param_value(m_ctx, param, value); }
00154 void set(char const * param, bool value) { Z3_update_param_value(m_ctx, param, value ? "true" : "false"); }
00158 void set(char const * param, int value) {
00159 std::ostringstream oss;
00160 oss << value;
00161 Z3_update_param_value(m_ctx, param, oss.str().c_str());
00162 }
00163
00168 void interrupt() { Z3_interrupt(m_ctx); }
00169
00173 symbol str_symbol(char const * s);
00177 symbol int_symbol(int n);
00181 sort bool_sort();
00185 sort int_sort();
00189 sort real_sort();
00193 sort bv_sort(unsigned sz);
00199 sort array_sort(sort d, sort r);
00205 sort enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts);
00206
00207 func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range);
00208 func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range);
00209 func_decl function(symbol const& name, sort_vector const& domain, sort const& range);
00210 func_decl function(char const * name, sort_vector const& domain, sort const& range);
00211 func_decl function(char const * name, sort const & domain, sort const & range);
00212 func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range);
00213 func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range);
00214 func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range);
00215 func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range);
00216
00217 expr constant(symbol const & name, sort const & s);
00218 expr constant(char const * name, sort const & s);
00219 expr bool_const(char const * name);
00220 expr int_const(char const * name);
00221 expr real_const(char const * name);
00222 expr bv_const(char const * name, unsigned sz);
00223
00224 expr bool_val(bool b);
00225
00226 expr int_val(int n);
00227 expr int_val(unsigned n);
00228 expr int_val(__int64 n);
00229 expr int_val(__uint64 n);
00230 expr int_val(char const * n);
00231
00232 expr real_val(int n, int d);
00233 expr real_val(int n);
00234 expr real_val(unsigned n);
00235 expr real_val(__int64 n);
00236 expr real_val(__uint64 n);
00237 expr real_val(char const * n);
00238
00239 expr bv_val(int n, unsigned sz);
00240 expr bv_val(unsigned n, unsigned sz);
00241 expr bv_val(__int64 n, unsigned sz);
00242 expr bv_val(__uint64 n, unsigned sz);
00243 expr bv_val(char const * n, unsigned sz);
00244
00245 expr num_val(int n, sort const & s);
00246 };
00247
00248 template<typename T>
00249 class array {
00250 T * m_array;
00251 unsigned m_size;
00252 array(array const & s);
00253 array & operator=(array const & s);
00254 public:
00255 array(unsigned sz):m_size(sz) { m_array = new T[sz]; }
00256 template<typename T2>
00257 array(ast_vector_tpl<T2> const & v);
00258 ~array() { delete[] m_array; }
00259 unsigned size() const { return m_size; }
00260 T & operator[](int i) { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
00261 T const & operator[](int i) const { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
00262 T const * ptr() const { return m_array; }
00263 T * ptr() { return m_array; }
00264 };
00265
00266 class object {
00267 protected:
00268 context * m_ctx;
00269 public:
00270 object(context & c):m_ctx(&c) {}
00271 object(object const & s):m_ctx(s.m_ctx) {}
00272 context & ctx() const { return *m_ctx; }
00273 void check_error() const { m_ctx->check_error(); }
00274 friend void check_context(object const & a, object const & b);
00275 };
00276 inline void check_context(object const & a, object const & b) { assert(a.m_ctx == b.m_ctx); }
00277
00278 class symbol : public object {
00279 Z3_symbol m_sym;
00280 public:
00281 symbol(context & c, Z3_symbol s):object(c), m_sym(s) {}
00282 symbol(symbol const & s):object(s), m_sym(s.m_sym) {}
00283 symbol & operator=(symbol const & s) { m_ctx = s.m_ctx; m_sym = s.m_sym; return *this; }
00284 operator Z3_symbol() const { return m_sym; }
00285 Z3_symbol_kind kind() const { return Z3_get_symbol_kind(ctx(), m_sym); }
00286 std::string str() const { assert(kind() == Z3_STRING_SYMBOL); return Z3_get_symbol_string(ctx(), m_sym); }
00287 int to_int() const { assert(kind() == Z3_INT_SYMBOL); return Z3_get_symbol_int(ctx(), m_sym); }
00288 friend std::ostream & operator<<(std::ostream & out, symbol const & s) {
00289 if (s.kind() == Z3_INT_SYMBOL)
00290 out << "k!" << s.to_int();
00291 else
00292 out << s.str().c_str();
00293 return out;
00294 }
00295 };
00296
00297
00298 class params : public object {
00299 Z3_params m_params;
00300 public:
00301 params(context & c):object(c) { m_params = Z3_mk_params(c); Z3_params_inc_ref(ctx(), m_params); }
00302 params(params const & s):object(s), m_params(s.m_params) { Z3_params_inc_ref(ctx(), m_params); }
00303 ~params() { Z3_params_dec_ref(ctx(), m_params); }
00304 operator Z3_params() const { return m_params; }
00305 params & operator=(params const & s) {
00306 Z3_params_inc_ref(s.ctx(), s.m_params);
00307 Z3_params_dec_ref(ctx(), m_params);
00308 m_ctx = s.m_ctx;
00309 m_params = s.m_params;
00310 return *this;
00311 }
00312 void set(char const * k, bool b) { Z3_params_set_bool(ctx(), m_params, ctx().str_symbol(k), b); }
00313 void set(char const * k, unsigned n) { Z3_params_set_uint(ctx(), m_params, ctx().str_symbol(k), n); }
00314 void set(char const * k, double n) { Z3_params_set_double(ctx(), m_params, ctx().str_symbol(k), n); }
00315 void set(char const * k, symbol const & s) { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), s); }
00316 friend std::ostream & operator<<(std::ostream & out, params const & p) {
00317 out << Z3_params_to_string(p.ctx(), p); return out;
00318 }
00319 };
00320
00321 class ast : public object {
00322 protected:
00323 Z3_ast m_ast;
00324 public:
00325 ast(context & c):object(c), m_ast(0) {}
00326 ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
00327 ast(ast const & s):object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
00328 ~ast() { if (m_ast) Z3_dec_ref(*m_ctx, m_ast); }
00329 operator Z3_ast() const { return m_ast; }
00330 operator bool() const { return m_ast != 0; }
00331 ast & operator=(ast const & s) { Z3_inc_ref(s.ctx(), s.m_ast); if (m_ast) Z3_dec_ref(ctx(), m_ast); m_ctx = s.m_ctx; m_ast = s.m_ast; return *this; }
00332 Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }
00333 unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }
00334 friend std::ostream & operator<<(std::ostream & out, ast const & n) {
00335 out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
00336 }
00337
00341 friend bool eq(ast const & a, ast const & b);
00342 };
00343
00344 inline bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b) != 0; }
00345
00346
00350 class sort : public ast {
00351 public:
00352 sort(context & c):ast(c) {}
00353 sort(context & c, Z3_sort s):ast(c, reinterpret_cast<Z3_ast>(s)) {}
00354 sort(sort const & s):ast(s) {}
00355 operator Z3_sort() const { return reinterpret_cast<Z3_sort>(m_ast); }
00359 sort & operator=(sort const & s) { return static_cast<sort&>(ast::operator=(s)); }
00363 Z3_sort_kind sort_kind() const { return Z3_get_sort_kind(*m_ctx, *this); }
00364
00368 bool is_bool() const { return sort_kind() == Z3_BOOL_SORT; }
00372 bool is_int() const { return sort_kind() == Z3_INT_SORT; }
00376 bool is_real() const { return sort_kind() == Z3_REAL_SORT; }
00380 bool is_arith() const { return is_int() || is_real(); }
00384 bool is_bv() const { return sort_kind() == Z3_BV_SORT; }
00388 bool is_array() const { return sort_kind() == Z3_ARRAY_SORT; }
00392 bool is_datatype() const { return sort_kind() == Z3_DATATYPE_SORT; }
00396 bool is_relation() const { return sort_kind() == Z3_RELATION_SORT; }
00400 bool is_finite_domain() const { return sort_kind() == Z3_FINITE_DOMAIN_SORT; }
00401
00407 unsigned bv_size() const { assert(is_bv()); unsigned r = Z3_get_bv_sort_size(ctx(), *this); check_error(); return r; }
00408
00414 sort array_domain() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_domain(ctx(), *this); check_error(); return sort(ctx(), s); }
00420 sort array_range() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_range(ctx(), *this); check_error(); return sort(ctx(), s); }
00421 };
00422
00427 class func_decl : public ast {
00428 public:
00429 func_decl(context & c):ast(c) {}
00430 func_decl(context & c, Z3_func_decl n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
00431 func_decl(func_decl const & s):ast(s) {}
00432 operator Z3_func_decl() const { return reinterpret_cast<Z3_func_decl>(m_ast); }
00433 func_decl & operator=(func_decl const & s) { return static_cast<func_decl&>(ast::operator=(s)); }
00434
00435 unsigned arity() const { return Z3_get_arity(ctx(), *this); }
00436 sort domain(unsigned i) const { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }
00437 sort range() const { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }
00438 symbol name() const { Z3_symbol s = Z3_get_decl_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
00439 Z3_decl_kind decl_kind() const { return Z3_get_decl_kind(ctx(), *this); }
00440
00441 bool is_const() const { return arity() == 0; }
00442
00443 expr operator()() const;
00444 expr operator()(unsigned n, expr const * args) const;
00445 expr operator()(expr_vector const& v) const;
00446 expr operator()(expr const & a) const;
00447 expr operator()(int a) const;
00448 expr operator()(expr const & a1, expr const & a2) const;
00449 expr operator()(expr const & a1, int a2) const;
00450 expr operator()(int a1, expr const & a2) const;
00451 expr operator()(expr const & a1, expr const & a2, expr const & a3) const;
00452 expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const;
00453 expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const;
00454 };
00455
00460 class expr : public ast {
00461 public:
00462 expr(context & c):ast(c) {}
00463 expr(context & c, Z3_ast n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
00464 expr(expr const & n):ast(n) {}
00465 expr & operator=(expr const & n) { return static_cast<expr&>(ast::operator=(n)); }
00466
00470 sort get_sort() const { Z3_sort s = Z3_get_sort(*m_ctx, m_ast); check_error(); return sort(*m_ctx, s); }
00471
00475 bool is_bool() const { return get_sort().is_bool(); }
00479 bool is_int() const { return get_sort().is_int(); }
00483 bool is_real() const { return get_sort().is_real(); }
00487 bool is_arith() const { return get_sort().is_arith(); }
00491 bool is_bv() const { return get_sort().is_bv(); }
00495 bool is_array() const { return get_sort().is_array(); }
00499 bool is_datatype() const { return get_sort().is_datatype(); }
00503 bool is_relation() const { return get_sort().is_relation(); }
00512 bool is_finite_domain() const { return get_sort().is_finite_domain(); }
00513
00517 bool is_numeral() const { return kind() == Z3_NUMERAL_AST; }
00521 bool is_app() const { return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
00525 bool is_const() const { return is_app() && num_args() == 0; }
00529 bool is_quantifier() const { return kind() == Z3_QUANTIFIER_AST; }
00533 bool is_var() const { return kind() == Z3_VAR_AST; }
00534
00538 bool is_well_sorted() const { bool r = Z3_is_well_sorted(ctx(), m_ast) != 0; check_error(); return r; }
00539
00540 operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
00541
00548 func_decl decl() const { Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }
00555 unsigned num_args() const { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
00563 expr arg(unsigned i) const { Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }
00564
00570 expr body() const { assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
00571
00577 friend expr operator!(expr const & a) {
00578 assert(a.is_bool());
00579 Z3_ast r = Z3_mk_not(a.ctx(), a);
00580 a.check_error();
00581 return expr(a.ctx(), r);
00582 }
00583
00584
00591 friend expr operator&&(expr const & a, expr const & b) {
00592 check_context(a, b);
00593 assert(a.is_bool() && b.is_bool());
00594 Z3_ast args[2] = { a, b };
00595 Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
00596 a.check_error();
00597 return expr(a.ctx(), r);
00598 }
00599
00600
00607 friend expr operator&&(expr const & a, bool b) { return a && a.ctx().bool_val(b); }
00614 friend expr operator&&(bool a, expr const & b) { return b.ctx().bool_val(a) && b; }
00615
00622 friend expr operator||(expr const & a, expr const & b) {
00623 check_context(a, b);
00624 assert(a.is_bool() && b.is_bool());
00625 Z3_ast args[2] = { a, b };
00626 Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
00627 a.check_error();
00628 return expr(a.ctx(), r);
00629 }
00636 friend expr operator||(expr const & a, bool b) { return a || a.ctx().bool_val(b); }
00643 friend expr operator||(bool a, expr const & b) { return b.ctx().bool_val(a) || b; }
00644
00645 friend expr implies(expr const & a, expr const & b) {
00646 check_context(a, b);
00647 assert(a.is_bool() && b.is_bool());
00648 Z3_ast r = Z3_mk_implies(a.ctx(), a, b);
00649 a.check_error();
00650 return expr(a.ctx(), r);
00651 }
00652 friend expr implies(expr const & a, bool b);
00653 friend expr implies(bool a, expr const & b);
00654
00655 friend expr ite(expr const & c, expr const & t, expr const & e);
00656
00657 friend expr distinct(expr_vector const& args);
00658
00659 friend expr operator==(expr const & a, expr const & b) {
00660 check_context(a, b);
00661 Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
00662 a.check_error();
00663 return expr(a.ctx(), r);
00664 }
00665 friend expr operator==(expr const & a, int b) { assert(a.is_arith() || a.is_bv()); return a == a.ctx().num_val(b, a.get_sort()); }
00666 friend expr operator==(int a, expr const & b) { assert(b.is_arith() || b.is_bv()); return b.ctx().num_val(a, b.get_sort()) == b; }
00667
00668 friend expr operator!=(expr const & a, expr const & b) {
00669 check_context(a, b);
00670 Z3_ast args[2] = { a, b };
00671 Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
00672 a.check_error();
00673 return expr(a.ctx(), r);
00674 }
00675 friend expr operator!=(expr const & a, int b) { assert(a.is_arith() || a.is_bv()); return a != a.ctx().num_val(b, a.get_sort()); }
00676 friend expr operator!=(int a, expr const & b) { assert(b.is_arith() || b.is_bv()); return b.ctx().num_val(a, b.get_sort()) != b; }
00677
00678 friend expr operator+(expr const & a, expr const & b) {
00679 check_context(a, b);
00680 Z3_ast r;
00681 if (a.is_arith() && b.is_arith()) {
00682 Z3_ast args[2] = { a, b };
00683 r = Z3_mk_add(a.ctx(), 2, args);
00684 }
00685 else if (a.is_bv() && b.is_bv()) {
00686 r = Z3_mk_bvadd(a.ctx(), a, b);
00687 }
00688 else {
00689
00690 assert(false);
00691 }
00692 a.check_error();
00693 return expr(a.ctx(), r);
00694 }
00695 friend expr operator+(expr const & a, int b) { return a + a.ctx().num_val(b, a.get_sort()); }
00696 friend expr operator+(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) + b; }
00697
00698 friend expr operator*(expr const & a, expr const & b) {
00699 check_context(a, b);
00700 Z3_ast r;
00701 if (a.is_arith() && b.is_arith()) {
00702 Z3_ast args[2] = { a, b };
00703 r = Z3_mk_mul(a.ctx(), 2, args);
00704 }
00705 else if (a.is_bv() && b.is_bv()) {
00706 r = Z3_mk_bvmul(a.ctx(), a, b);
00707 }
00708 else {
00709
00710 assert(false);
00711 }
00712 a.check_error();
00713 return expr(a.ctx(), r);
00714 }
00715 friend expr operator*(expr const & a, int b) { return a * a.ctx().num_val(b, a.get_sort()); }
00716 friend expr operator*(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) * b; }
00717
00721 friend expr pw(expr const & a, expr const & b);
00722 friend expr pw(expr const & a, int b);
00723 friend expr pw(int a, expr const & b);
00724
00725 friend expr operator/(expr const & a, expr const & b) {
00726 check_context(a, b);
00727 Z3_ast r;
00728 if (a.is_arith() && b.is_arith()) {
00729 r = Z3_mk_div(a.ctx(), a, b);
00730 }
00731 else if (a.is_bv() && b.is_bv()) {
00732 r = Z3_mk_bvsdiv(a.ctx(), a, b);
00733 }
00734 else {
00735
00736 assert(false);
00737 }
00738 a.check_error();
00739 return expr(a.ctx(), r);
00740 }
00741 friend expr operator/(expr const & a, int b) { return a / a.ctx().num_val(b, a.get_sort()); }
00742 friend expr operator/(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) / b; }
00743
00744 friend expr operator-(expr const & a) {
00745 Z3_ast r;
00746 if (a.is_arith()) {
00747 r = Z3_mk_unary_minus(a.ctx(), a);
00748 }
00749 else if (a.is_bv()) {
00750 r = Z3_mk_bvneg(a.ctx(), a);
00751 }
00752 else {
00753
00754 assert(false);
00755 }
00756 a.check_error();
00757 return expr(a.ctx(), r);
00758 }
00759
00760 friend expr operator-(expr const & a, expr const & b) {
00761 check_context(a, b);
00762 Z3_ast r;
00763 if (a.is_arith() && b.is_arith()) {
00764 Z3_ast args[2] = { a, b };
00765 r = Z3_mk_sub(a.ctx(), 2, args);
00766 }
00767 else if (a.is_bv() && b.is_bv()) {
00768 r = Z3_mk_bvsub(a.ctx(), a, b);
00769 }
00770 else {
00771
00772 assert(false);
00773 }
00774 a.check_error();
00775 return expr(a.ctx(), r);
00776 }
00777 friend expr operator-(expr const & a, int b) { return a - a.ctx().num_val(b, a.get_sort()); }
00778 friend expr operator-(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) - b; }
00779
00780 friend expr operator<=(expr const & a, expr const & b) {
00781 check_context(a, b);
00782 Z3_ast r;
00783 if (a.is_arith() && b.is_arith()) {
00784 r = Z3_mk_le(a.ctx(), a, b);
00785 }
00786 else if (a.is_bv() && b.is_bv()) {
00787 r = Z3_mk_bvsle(a.ctx(), a, b);
00788 }
00789 else {
00790
00791 assert(false);
00792 }
00793 a.check_error();
00794 return expr(a.ctx(), r);
00795 }
00796 friend expr operator<=(expr const & a, int b) { return a <= a.ctx().num_val(b, a.get_sort()); }
00797 friend expr operator<=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) <= b; }
00798
00799 friend expr operator>=(expr const & a, expr const & b) {
00800 check_context(a, b);
00801 Z3_ast r;
00802 if (a.is_arith() && b.is_arith()) {
00803 r = Z3_mk_ge(a.ctx(), a, b);
00804 }
00805 else if (a.is_bv() && b.is_bv()) {
00806 r = Z3_mk_bvsge(a.ctx(), a, b);
00807 }
00808 else {
00809
00810 assert(false);
00811 }
00812 a.check_error();
00813 return expr(a.ctx(), r);
00814 }
00815 friend expr operator>=(expr const & a, int b) { return a >= a.ctx().num_val(b, a.get_sort()); }
00816 friend expr operator>=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) >= b; }
00817
00818 friend expr operator<(expr const & a, expr const & b) {
00819 check_context(a, b);
00820 Z3_ast r;
00821 if (a.is_arith() && b.is_arith()) {
00822 r = Z3_mk_lt(a.ctx(), a, b);
00823 }
00824 else if (a.is_bv() && b.is_bv()) {
00825 r = Z3_mk_bvslt(a.ctx(), a, b);
00826 }
00827 else {
00828
00829 assert(false);
00830 }
00831 a.check_error();
00832 return expr(a.ctx(), r);
00833 }
00834 friend expr operator<(expr const & a, int b) { return a < a.ctx().num_val(b, a.get_sort()); }
00835 friend expr operator<(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) < b; }
00836
00837 friend expr operator>(expr const & a, expr const & b) {
00838 check_context(a, b);
00839 Z3_ast r;
00840 if (a.is_arith() && b.is_arith()) {
00841 r = Z3_mk_gt(a.ctx(), a, b);
00842 }
00843 else if (a.is_bv() && b.is_bv()) {
00844 r = Z3_mk_bvsgt(a.ctx(), a, b);
00845 }
00846 else {
00847
00848 assert(false);
00849 }
00850 a.check_error();
00851 return expr(a.ctx(), r);
00852 }
00853 friend expr operator>(expr const & a, int b) { return a > a.ctx().num_val(b, a.get_sort()); }
00854 friend expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > b; }
00855
00856 friend expr operator&(expr const & a, expr const & b) { check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); return expr(a.ctx(), r); }
00857 friend expr operator&(expr const & a, int b) { return a & a.ctx().num_val(b, a.get_sort()); }
00858 friend expr operator&(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) & b; }
00859
00860 friend expr operator^(expr const & a, expr const & b) { check_context(a, b); Z3_ast r = Z3_mk_bvxor(a.ctx(), a, b); return expr(a.ctx(), r); }
00861 friend expr operator^(expr const & a, int b) { return a ^ a.ctx().num_val(b, a.get_sort()); }
00862 friend expr operator^(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) ^ b; }
00863
00864 friend expr operator|(expr const & a, expr const & b) { check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); return expr(a.ctx(), r); }
00865 friend expr operator|(expr const & a, int b) { return a | a.ctx().num_val(b, a.get_sort()); }
00866 friend expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; }
00867
00868 friend expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
00869
00873 expr simplify() const { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
00877 expr simplify(params const & p) const { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
00878
00882 expr substitute(expr_vector const& src, expr_vector const& dst);
00883
00887 expr substitute(expr_vector const& dst);
00888
00889 };
00890
00891 inline expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); }
00892 inline expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); }
00893
00894 inline expr pw(expr const & a, expr const & b) {
00895 assert(a.is_arith() && b.is_arith());
00896 check_context(a, b);
00897 Z3_ast r = Z3_mk_power(a.ctx(), a, b);
00898 a.check_error();
00899 return expr(a.ctx(), r);
00900 }
00901 inline expr pw(expr const & a, int b) { return pw(a, a.ctx().num_val(b, a.get_sort())); }
00902 inline expr pw(int a, expr const & b) { return pw(b.ctx().num_val(a, b.get_sort()), b); }
00903
00904
00905
00906
00907
00914 inline expr ite(expr const & c, expr const & t, expr const & e) {
00915 check_context(c, t); check_context(c, e);
00916 assert(c.is_bool());
00917 Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
00918 c.check_error();
00919 return expr(c.ctx(), r);
00920 }
00921
00922
00927 inline expr to_expr(context & c, Z3_ast a) {
00928 c.check_error();
00929 assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
00930 Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
00931 Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
00932 Z3_get_ast_kind(c, a) == Z3_QUANTIFIER_AST);
00933 return expr(c, a);
00934 }
00935
00936 inline sort to_sort(context & c, Z3_sort s) {
00937 c.check_error();
00938 return sort(c, s);
00939 }
00940
00941 inline func_decl to_func_decl(context & c, Z3_func_decl f) {
00942 c.check_error();
00943 return func_decl(c, f);
00944 }
00945
00949 inline expr ule(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
00950 inline expr ule(expr const & a, int b) { return ule(a, a.ctx().num_val(b, a.get_sort())); }
00951 inline expr ule(int a, expr const & b) { return ule(b.ctx().num_val(a, b.get_sort()), b); }
00955 inline expr ult(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }
00956 inline expr ult(expr const & a, int b) { return ult(a, a.ctx().num_val(b, a.get_sort())); }
00957 inline expr ult(int a, expr const & b) { return ult(b.ctx().num_val(a, b.get_sort()), b); }
00961 inline expr uge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }
00962 inline expr uge(expr const & a, int b) { return uge(a, a.ctx().num_val(b, a.get_sort())); }
00963 inline expr uge(int a, expr const & b) { return uge(b.ctx().num_val(a, b.get_sort()), b); }
00967 inline expr ugt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
00968 inline expr ugt(expr const & a, int b) { return ugt(a, a.ctx().num_val(b, a.get_sort())); }
00969 inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), b); }
00973 inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
00974 inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); }
00975 inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); }
00976
00977 template<typename T> class cast_ast;
00978
00979 template<> class cast_ast<ast> {
00980 public:
00981 ast operator()(context & c, Z3_ast a) { return ast(c, a); }
00982 };
00983
00984 template<> class cast_ast<expr> {
00985 public:
00986 expr operator()(context & c, Z3_ast a) {
00987 assert(Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
00988 Z3_get_ast_kind(c, a) == Z3_APP_AST ||
00989 Z3_get_ast_kind(c, a) == Z3_QUANTIFIER_AST ||
00990 Z3_get_ast_kind(c, a) == Z3_VAR_AST);
00991 return expr(c, a);
00992 }
00993 };
00994
00995 template<> class cast_ast<sort> {
00996 public:
00997 sort operator()(context & c, Z3_ast a) {
00998 assert(Z3_get_ast_kind(c, a) == Z3_SORT_AST);
00999 return sort(c, reinterpret_cast<Z3_sort>(a));
01000 }
01001 };
01002
01003 template<> class cast_ast<func_decl> {
01004 public:
01005 func_decl operator()(context & c, Z3_ast a) {
01006 assert(Z3_get_ast_kind(c, a) == Z3_FUNC_DECL_AST);
01007 return func_decl(c, reinterpret_cast<Z3_func_decl>(a));
01008 }
01009 };
01010
01011 template<typename T>
01012 class ast_vector_tpl : public object {
01013 Z3_ast_vector m_vector;
01014 void init(Z3_ast_vector v) { Z3_ast_vector_inc_ref(ctx(), v); m_vector = v; }
01015 public:
01016 ast_vector_tpl(context & c):object(c) { init(Z3_mk_ast_vector(c)); }
01017 ast_vector_tpl(context & c, Z3_ast_vector v):object(c) { init(v); }
01018 ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
01019 ~ast_vector_tpl() { Z3_ast_vector_dec_ref(ctx(), m_vector); }
01020 operator Z3_ast_vector() const { return m_vector; }
01021 unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); }
01022 T operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
01023 void push_back(T const & e) { Z3_ast_vector_push(ctx(), m_vector, e); check_error(); }
01024 void resize(unsigned sz) { Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }
01025 T back() const { return operator[](size() - 1); }
01026 void pop_back() { assert(size() > 0); resize(size() - 1); }
01027 bool empty() const { return size() == 0; }
01028 ast_vector_tpl & operator=(ast_vector_tpl const & s) {
01029 Z3_ast_vector_inc_ref(s.ctx(), s.m_vector);
01030 Z3_ast_vector_dec_ref(ctx(), m_vector);
01031 m_ctx = s.m_ctx;
01032 m_vector = s.m_vector;
01033 return *this;
01034 }
01035 friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
01036 };
01037
01038 template<typename T>
01039 template<typename T2>
01040 array<T>::array(ast_vector_tpl<T2> const & v) {
01041 m_array = new T[v.size()];
01042 m_size = v.size();
01043 for (unsigned i = 0; i < m_size; i++) {
01044 m_array[i] = v[i];
01045 }
01046 }
01047
01048
01049
01050 inline expr forall(expr const & x, expr const & b) {
01051 check_context(x, b);
01052 Z3_app vars[] = {(Z3_app) x};
01053 Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
01054 }
01055 inline expr forall(expr const & x1, expr const & x2, expr const & b) {
01056 check_context(x1, b); check_context(x2, b);
01057 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
01058 Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
01059 }
01060 inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
01061 check_context(x1, b); check_context(x2, b); check_context(x3, b);
01062 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
01063 Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
01064 }
01065 inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
01066 check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
01067 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
01068 Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
01069 }
01070 inline expr forall(expr_vector const & xs, expr const & b) {
01071 array<Z3_app> vars(xs);
01072 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);
01073 }
01074 inline expr exists(expr const & x, expr const & b) {
01075 check_context(x, b);
01076 Z3_app vars[] = {(Z3_app) x};
01077 Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
01078 }
01079 inline expr exists(expr const & x1, expr const & x2, expr const & b) {
01080 check_context(x1, b); check_context(x2, b);
01081 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
01082 Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
01083 }
01084 inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
01085 check_context(x1, b); check_context(x2, b); check_context(x3, b);
01086 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
01087 Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
01088 }
01089 inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
01090 check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
01091 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
01092 Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
01093 }
01094 inline expr exists(expr_vector const & xs, expr const & b) {
01095 array<Z3_app> vars(xs);
01096 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);
01097 }
01098
01099
01100 inline expr distinct(expr_vector const& args) {
01101 assert(args.size() > 0);
01102 context& ctx = args[0].ctx();
01103 array<Z3_ast> _args(args);
01104 Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
01105 ctx.check_error();
01106 return expr(ctx, r);
01107 }
01108
01109 class func_entry : public object {
01110 Z3_func_entry m_entry;
01111 void init(Z3_func_entry e) {
01112 m_entry = e;
01113 Z3_func_entry_inc_ref(ctx(), m_entry);
01114 }
01115 public:
01116 func_entry(context & c, Z3_func_entry e):object(c) { init(e); }
01117 func_entry(func_entry const & s):object(s) { init(s.m_entry); }
01118 ~func_entry() { Z3_func_entry_dec_ref(ctx(), m_entry); }
01119 operator Z3_func_entry() const { return m_entry; }
01120 func_entry & operator=(func_entry const & s) {
01121 Z3_func_entry_inc_ref(s.ctx(), s.m_entry);
01122 Z3_func_entry_dec_ref(ctx(), m_entry);
01123 m_ctx = s.m_ctx;
01124 m_entry = s.m_entry;
01125 return *this;
01126 }
01127 expr value() const { Z3_ast r = Z3_func_entry_get_value(ctx(), m_entry); check_error(); return expr(ctx(), r); }
01128 unsigned num_args() const { unsigned r = Z3_func_entry_get_num_args(ctx(), m_entry); check_error(); return r; }
01129 expr arg(unsigned i) const { Z3_ast r = Z3_func_entry_get_arg(ctx(), m_entry, i); check_error(); return expr(ctx(), r); }
01130 };
01131
01132 class func_interp : public object {
01133 Z3_func_interp m_interp;
01134 void init(Z3_func_interp e) {
01135 m_interp = e;
01136 Z3_func_interp_inc_ref(ctx(), m_interp);
01137 }
01138 public:
01139 func_interp(context & c, Z3_func_interp e):object(c) { init(e); }
01140 func_interp(func_interp const & s):object(s) { init(s.m_interp); }
01141 ~func_interp() { Z3_func_interp_dec_ref(ctx(), m_interp); }
01142 operator Z3_func_interp() const { return m_interp; }
01143 func_interp & operator=(func_interp const & s) {
01144 Z3_func_interp_inc_ref(s.ctx(), s.m_interp);
01145 Z3_func_interp_dec_ref(ctx(), m_interp);
01146 m_ctx = s.m_ctx;
01147 m_interp = s.m_interp;
01148 return *this;
01149 }
01150 expr else_value() const { Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), r); }
01151 unsigned num_entries() const { unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }
01152 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); }
01153 };
01154
01155 class model : public object {
01156 Z3_model m_model;
01157 void init(Z3_model m) {
01158 m_model = m;
01159 Z3_model_inc_ref(ctx(), m);
01160 }
01161 public:
01162 model(context & c, Z3_model m):object(c) { init(m); }
01163 model(model const & s):object(s) { init(s.m_model); }
01164 ~model() { Z3_model_dec_ref(ctx(), m_model); }
01165 operator Z3_model() const { return m_model; }
01166 model & operator=(model const & s) {
01167 Z3_model_inc_ref(s.ctx(), s.m_model);
01168 Z3_model_dec_ref(ctx(), m_model);
01169 m_ctx = s.m_ctx;
01170 m_model = s.m_model;
01171 return *this;
01172 }
01173
01174 expr eval(expr const & n, bool model_completion=false) const {
01175 check_context(*this, n);
01176 Z3_ast r;
01177 Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
01178 check_error();
01179 if (status == Z3_FALSE)
01180 throw exception("failed to evaluate expression");
01181 return expr(ctx(), r);
01182 }
01183
01184 unsigned num_consts() const { return Z3_model_get_num_consts(ctx(), m_model); }
01185 unsigned num_funcs() const { return Z3_model_get_num_funcs(ctx(), m_model); }
01186 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); }
01187 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); }
01188 unsigned size() const { return num_consts() + num_funcs(); }
01189 func_decl operator[](int i) const {
01190 assert(0 <= i);
01191 return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
01192 }
01193
01194 expr get_const_interp(func_decl c) const {
01195 check_context(*this, c);
01196 Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);
01197 check_error();
01198 return expr(ctx(), r);
01199 }
01200 func_interp get_func_interp(func_decl f) const {
01201 check_context(*this, f);
01202 Z3_func_interp r = Z3_model_get_func_interp(ctx(), m_model, f);
01203 check_error();
01204 return func_interp(ctx(), r);
01205 }
01206
01207 friend std::ostream & operator<<(std::ostream & out, model const & m) { out << Z3_model_to_string(m.ctx(), m); return out; }
01208 };
01209
01210 class stats : public object {
01211 Z3_stats m_stats;
01212 void init(Z3_stats e) {
01213 m_stats = e;
01214 Z3_stats_inc_ref(ctx(), m_stats);
01215 }
01216 public:
01217 stats(context & c):object(c), m_stats(0) {}
01218 stats(context & c, Z3_stats e):object(c) { init(e); }
01219 stats(stats const & s):object(s) { init(s.m_stats); }
01220 ~stats() { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); }
01221 operator Z3_stats() const { return m_stats; }
01222 stats & operator=(stats const & s) {
01223 Z3_stats_inc_ref(s.ctx(), s.m_stats);
01224 if (m_stats) Z3_stats_dec_ref(ctx(), m_stats);
01225 m_ctx = s.m_ctx;
01226 m_stats = s.m_stats;
01227 return *this;
01228 }
01229 unsigned size() const { return Z3_stats_size(ctx(), m_stats); }
01230 std::string key(unsigned i) const { Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; }
01231 bool is_uint(unsigned i) const { Z3_bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r != 0; }
01232 bool is_double(unsigned i) const { Z3_bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r != 0; }
01233 unsigned uint_value(unsigned i) const { unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; }
01234 double double_value(unsigned i) const { double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
01235 friend std::ostream & operator<<(std::ostream & out, stats const & s) { out << Z3_stats_to_string(s.ctx(), s); return out; }
01236 };
01237
01238 enum check_result {
01239 unsat, sat, unknown
01240 };
01241
01242 inline std::ostream & operator<<(std::ostream & out, check_result r) {
01243 if (r == unsat) out << "unsat";
01244 else if (r == sat) out << "sat";
01245 else out << "unknown";
01246 return out;
01247 }
01248
01249 inline check_result to_check_result(Z3_lbool l) {
01250 if (l == Z3_L_TRUE) return sat;
01251 else if (l == Z3_L_FALSE) return unsat;
01252 return unknown;
01253 }
01254
01255 class solver : public object {
01256 Z3_solver m_solver;
01257 void init(Z3_solver s) {
01258 m_solver = s;
01259 Z3_solver_inc_ref(ctx(), s);
01260 }
01261 public:
01262 solver(context & c):object(c) { init(Z3_mk_solver(c)); }
01263 solver(context & c, Z3_solver s):object(c) { init(s); }
01264 solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); }
01265 solver(solver const & s):object(s) { init(s.m_solver); }
01266 ~solver() { Z3_solver_dec_ref(ctx(), m_solver); }
01267 operator Z3_solver() const { return m_solver; }
01268 solver & operator=(solver const & s) {
01269 Z3_solver_inc_ref(s.ctx(), s.m_solver);
01270 Z3_solver_dec_ref(ctx(), m_solver);
01271 m_ctx = s.m_ctx;
01272 m_solver = s.m_solver;
01273 return *this;
01274 }
01275 void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
01276 void push() { Z3_solver_push(ctx(), m_solver); check_error(); }
01277 void pop(unsigned n = 1) { Z3_solver_pop(ctx(), m_solver, n); check_error(); }
01278 void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); }
01279 void add(expr const & e) { assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); }
01280 void add(expr const & e, expr const & p) {
01281 assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
01282 Z3_solver_assert_and_track(ctx(), m_solver, e, p);
01283 check_error();
01284 }
01285 void add(expr const & e, char const * p) {
01286 add(e, ctx().bool_const(p));
01287 }
01288 check_result check() { Z3_lbool r = Z3_solver_check(ctx(), m_solver); check_error(); return to_check_result(r); }
01289 check_result check(unsigned n, expr * const assumptions) {
01290 array<Z3_ast> _assumptions(n);
01291 for (unsigned i = 0; i < n; i++) {
01292 check_context(*this, assumptions[i]);
01293 _assumptions[i] = assumptions[i];
01294 }
01295 Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
01296 check_error();
01297 return to_check_result(r);
01298 }
01299 check_result check(expr_vector assumptions) {
01300 unsigned n = assumptions.size();
01301 array<Z3_ast> _assumptions(n);
01302 for (unsigned i = 0; i < n; i++) {
01303 check_context(*this, assumptions[i]);
01304 _assumptions[i] = assumptions[i];
01305 }
01306 Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
01307 check_error();
01308 return to_check_result(r);
01309 }
01310 model get_model() const { Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }
01311 std::string reason_unknown() const { Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }
01312 stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }
01313 expr_vector unsat_core() const { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
01314 expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
01315 expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
01316 friend std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
01317 };
01318
01319 class goal : public object {
01320 Z3_goal m_goal;
01321 void init(Z3_goal s) {
01322 m_goal = s;
01323 Z3_goal_inc_ref(ctx(), s);
01324 }
01325 public:
01326 goal(context & c, bool models=true, bool unsat_cores=false, bool proofs=false):object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); }
01327 goal(context & c, Z3_goal s):object(c) { init(s); }
01328 goal(goal const & s):object(s) { init(s.m_goal); }
01329 ~goal() { Z3_goal_dec_ref(ctx(), m_goal); }
01330 operator Z3_goal() const { return m_goal; }
01331 goal & operator=(goal const & s) {
01332 Z3_goal_inc_ref(s.ctx(), s.m_goal);
01333 Z3_goal_dec_ref(ctx(), m_goal);
01334 m_ctx = s.m_ctx;
01335 m_goal = s.m_goal;
01336 return *this;
01337 }
01338 void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
01339 unsigned size() const { return Z3_goal_size(ctx(), m_goal); }
01340 expr operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
01341 Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); }
01342 bool inconsistent() const { return Z3_goal_inconsistent(ctx(), m_goal) != 0; }
01343 unsigned depth() const { return Z3_goal_depth(ctx(), m_goal); }
01344 void reset() { Z3_goal_reset(ctx(), m_goal); }
01345 unsigned num_exprs() const { return Z3_goal_num_exprs(ctx(), m_goal); }
01346 bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal) != 0; }
01347 bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal) != 0; }
01348 expr as_expr() const {
01349 unsigned n = size();
01350 if (n == 0)
01351 return ctx().bool_val(true);
01352 else if (n == 1)
01353 return operator[](0);
01354 else {
01355 array<Z3_ast> args(n);
01356 for (unsigned i = 0; i < n; i++)
01357 args[i] = operator[](i);
01358 return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
01359 }
01360 }
01361 friend std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; }
01362 };
01363
01364 class apply_result : public object {
01365 Z3_apply_result m_apply_result;
01366 void init(Z3_apply_result s) {
01367 m_apply_result = s;
01368 Z3_apply_result_inc_ref(ctx(), s);
01369 }
01370 public:
01371 apply_result(context & c, Z3_apply_result s):object(c) { init(s); }
01372 apply_result(apply_result const & s):object(s) { init(s.m_apply_result); }
01373 ~apply_result() { Z3_apply_result_dec_ref(ctx(), m_apply_result); }
01374 operator Z3_apply_result() const { return m_apply_result; }
01375 apply_result & operator=(apply_result const & s) {
01376 Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result);
01377 Z3_apply_result_dec_ref(ctx(), m_apply_result);
01378 m_ctx = s.m_ctx;
01379 m_apply_result = s.m_apply_result;
01380 return *this;
01381 }
01382 unsigned size() const { return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }
01383 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); }
01384 model convert_model(model const & m, unsigned i = 0) const {
01385 check_context(*this, m);
01386 Z3_model new_m = Z3_apply_result_convert_model(ctx(), m_apply_result, i, m);
01387 check_error();
01388 return model(ctx(), new_m);
01389 }
01390 friend std::ostream & operator<<(std::ostream & out, apply_result const & r) { out << Z3_apply_result_to_string(r.ctx(), r); return out; }
01391 };
01392
01393 class tactic : public object {
01394 Z3_tactic m_tactic;
01395 void init(Z3_tactic s) {
01396 m_tactic = s;
01397 Z3_tactic_inc_ref(ctx(), s);
01398 }
01399 public:
01400 tactic(context & c, char const * name):object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); }
01401 tactic(context & c, Z3_tactic s):object(c) { init(s); }
01402 tactic(tactic const & s):object(s) { init(s.m_tactic); }
01403 ~tactic() { Z3_tactic_dec_ref(ctx(), m_tactic); }
01404 operator Z3_tactic() const { return m_tactic; }
01405 tactic & operator=(tactic const & s) {
01406 Z3_tactic_inc_ref(s.ctx(), s.m_tactic);
01407 Z3_tactic_dec_ref(ctx(), m_tactic);
01408 m_ctx = s.m_ctx;
01409 m_tactic = s.m_tactic;
01410 return *this;
01411 }
01412 solver mk_solver() const { Z3_solver r = Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error(); return solver(ctx(), r); }
01413 apply_result apply(goal const & g) const {
01414 check_context(*this, g);
01415 Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g);
01416 check_error();
01417 return apply_result(ctx(), r);
01418 }
01419 apply_result operator()(goal const & g) const {
01420 return apply(g);
01421 }
01422 std::string help() const { char const * r = Z3_tactic_get_help(ctx(), m_tactic); check_error(); return r; }
01423 friend tactic operator&(tactic const & t1, tactic const & t2) {
01424 check_context(t1, t2);
01425 Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
01426 t1.check_error();
01427 return tactic(t1.ctx(), r);
01428 }
01429 friend tactic operator|(tactic const & t1, tactic const & t2) {
01430 check_context(t1, t2);
01431 Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
01432 t1.check_error();
01433 return tactic(t1.ctx(), r);
01434 }
01435 friend tactic repeat(tactic const & t, unsigned max);
01436 friend tactic with(tactic const & t, params const & p);
01437 friend tactic try_for(tactic const & t, unsigned ms);
01438 };
01439
01440 inline tactic repeat(tactic const & t, unsigned max=UINT_MAX) {
01441 Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
01442 t.check_error();
01443 return tactic(t.ctx(), r);
01444 }
01445
01446 inline tactic with(tactic const & t, params const & p) {
01447 Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
01448 t.check_error();
01449 return tactic(t.ctx(), r);
01450 }
01451 inline tactic try_for(tactic const & t, unsigned ms) {
01452 Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
01453 t.check_error();
01454 return tactic(t.ctx(), r);
01455 }
01456
01457
01458 class probe : public object {
01459 Z3_probe m_probe;
01460 void init(Z3_probe s) {
01461 m_probe = s;
01462 Z3_probe_inc_ref(ctx(), s);
01463 }
01464 public:
01465 probe(context & c, char const * name):object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); }
01466 probe(context & c, double val):object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); }
01467 probe(context & c, Z3_probe s):object(c) { init(s); }
01468 probe(probe const & s):object(s) { init(s.m_probe); }
01469 ~probe() { Z3_probe_dec_ref(ctx(), m_probe); }
01470 operator Z3_probe() const { return m_probe; }
01471 probe & operator=(probe const & s) {
01472 Z3_probe_inc_ref(s.ctx(), s.m_probe);
01473 Z3_probe_dec_ref(ctx(), m_probe);
01474 m_ctx = s.m_ctx;
01475 m_probe = s.m_probe;
01476 return *this;
01477 }
01478 double apply(goal const & g) const { double r = Z3_probe_apply(ctx(), m_probe, g); check_error(); return r; }
01479 double operator()(goal const & g) const { return apply(g); }
01480 friend probe operator<=(probe const & p1, probe const & p2) {
01481 check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
01482 }
01483 friend probe operator<=(probe const & p1, double p2) { return p1 <= probe(p1.ctx(), p2); }
01484 friend probe operator<=(double p1, probe const & p2) { return probe(p2.ctx(), p1) <= p2; }
01485 friend probe operator>=(probe const & p1, probe const & p2) {
01486 check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
01487 }
01488 friend probe operator>=(probe const & p1, double p2) { return p1 >= probe(p1.ctx(), p2); }
01489 friend probe operator>=(double p1, probe const & p2) { return probe(p2.ctx(), p1) >= p2; }
01490 friend probe operator<(probe const & p1, probe const & p2) {
01491 check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
01492 }
01493 friend probe operator<(probe const & p1, double p2) { return p1 < probe(p1.ctx(), p2); }
01494 friend probe operator<(double p1, probe const & p2) { return probe(p2.ctx(), p1) < p2; }
01495 friend probe operator>(probe const & p1, probe const & p2) {
01496 check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
01497 }
01498 friend probe operator>(probe const & p1, double p2) { return p1 > probe(p1.ctx(), p2); }
01499 friend probe operator>(double p1, probe const & p2) { return probe(p2.ctx(), p1) > p2; }
01500 friend probe operator==(probe const & p1, probe const & p2) {
01501 check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
01502 }
01503 friend probe operator==(probe const & p1, double p2) { return p1 == probe(p1.ctx(), p2); }
01504 friend probe operator==(double p1, probe const & p2) { return probe(p2.ctx(), p1) == p2; }
01505 friend probe operator&&(probe const & p1, probe const & p2) {
01506 check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
01507 }
01508 friend probe operator||(probe const & p1, probe const & p2) {
01509 check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
01510 }
01511 friend probe operator!(probe const & p) {
01512 Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
01513 }
01514 };
01515
01516 inline tactic fail_if(probe const & p) {
01517 Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
01518 p.check_error();
01519 return tactic(p.ctx(), r);
01520 }
01521 inline tactic when(probe const & p, tactic const & t) {
01522 check_context(p, t);
01523 Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
01524 t.check_error();
01525 return tactic(t.ctx(), r);
01526 }
01527 inline tactic cond(probe const & p, tactic const & t1, tactic const & t2) {
01528 check_context(p, t1); check_context(p, t2);
01529 Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
01530 t1.check_error();
01531 return tactic(t1.ctx(), r);
01532 }
01533
01534 inline symbol context::str_symbol(char const * s) { Z3_symbol r = Z3_mk_string_symbol(m_ctx, s); check_error(); return symbol(*this, r); }
01535 inline symbol context::int_symbol(int n) { Z3_symbol r = Z3_mk_int_symbol(m_ctx, n); check_error(); return symbol(*this, r); }
01536
01537 inline sort context::bool_sort() { Z3_sort s = Z3_mk_bool_sort(m_ctx); check_error(); return sort(*this, s); }
01538 inline sort context::int_sort() { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }
01539 inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
01540 inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
01541 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); }
01542 inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
01543 array<Z3_symbol> _enum_names(n);
01544 for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
01545 array<Z3_func_decl> _cs(n);
01546 array<Z3_func_decl> _ts(n);
01547 Z3_symbol _name = Z3_mk_string_symbol(*this, name);
01548 sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
01549 check_error();
01550 for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
01551 return s;
01552 }
01553
01554 inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
01555 array<Z3_sort> args(arity);
01556 for (unsigned i = 0; i < arity; i++) {
01557 check_context(domain[i], range);
01558 args[i] = domain[i];
01559 }
01560 Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
01561 check_error();
01562 return func_decl(*this, f);
01563 }
01564
01565 inline func_decl context::function(char const * name, unsigned arity, sort const * domain, sort const & range) {
01566 return function(range.ctx().str_symbol(name), arity, domain, range);
01567 }
01568
01569 inline func_decl context::function(symbol const& name, sort_vector const& domain, sort const& range) {
01570 array<Z3_sort> args(domain.size());
01571 for (unsigned i = 0; i < domain.size(); i++) {
01572 check_context(domain[i], range);
01573 args[i] = domain[i];
01574 }
01575 Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
01576 check_error();
01577 return func_decl(*this, f);
01578 }
01579
01580 inline func_decl context::function(char const * name, sort_vector const& domain, sort const& range) {
01581 return function(range.ctx().str_symbol(name), domain, range);
01582 }
01583
01584
01585 inline func_decl context::function(char const * name, sort const & domain, sort const & range) {
01586 check_context(domain, range);
01587 Z3_sort args[1] = { domain };
01588 Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
01589 check_error();
01590 return func_decl(*this, f);
01591 }
01592
01593 inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & range) {
01594 check_context(d1, range); check_context(d2, range);
01595 Z3_sort args[2] = { d1, d2 };
01596 Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
01597 check_error();
01598 return func_decl(*this, f);
01599 }
01600
01601 inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
01602 check_context(d1, range); check_context(d2, range); check_context(d3, range);
01603 Z3_sort args[3] = { d1, d2, d3 };
01604 Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
01605 check_error();
01606 return func_decl(*this, f);
01607 }
01608
01609 inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
01610 check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range);
01611 Z3_sort args[4] = { d1, d2, d3, d4 };
01612 Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
01613 check_error();
01614 return func_decl(*this, f);
01615 }
01616
01617 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) {
01618 check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range); check_context(d5, range);
01619 Z3_sort args[5] = { d1, d2, d3, d4, d5 };
01620 Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
01621 check_error();
01622 return func_decl(*this, f);
01623 }
01624
01625 inline expr context::constant(symbol const & name, sort const & s) {
01626 Z3_ast r = Z3_mk_const(m_ctx, name, s);
01627 check_error();
01628 return expr(*this, r);
01629 }
01630 inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); }
01631 inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); }
01632 inline expr context::int_const(char const * name) { return constant(name, int_sort()); }
01633 inline expr context::real_const(char const * name) { return constant(name, real_sort()); }
01634 inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); }
01635
01636 inline expr context::bool_val(bool b) { return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }
01637
01638 inline expr context::int_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
01639 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); }
01640 inline expr context::int_val(__int64 n) { Z3_ast r = Z3_mk_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
01641 inline expr context::int_val(__uint64 n) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
01642 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); }
01643
01644 inline expr context::real_val(int n, int d) { Z3_ast r = Z3_mk_real(m_ctx, n, d); check_error(); return expr(*this, r); }
01645 inline expr context::real_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
01646 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); }
01647 inline expr context::real_val(__int64 n) { Z3_ast r = Z3_mk_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
01648 inline expr context::real_val(__uint64 n) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
01649 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); }
01650
01651 inline expr context::bv_val(int n, unsigned sz) { Z3_ast r = Z3_mk_int(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
01652 inline expr context::bv_val(unsigned n, unsigned sz) { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
01653 inline expr context::bv_val(__int64 n, unsigned sz) { Z3_ast r = Z3_mk_int64(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
01654 inline expr context::bv_val(__uint64 n, unsigned sz) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
01655 inline expr context::bv_val(char const * n, unsigned sz) { Z3_ast r = Z3_mk_numeral(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
01656
01657 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); }
01658
01659 inline expr func_decl::operator()(unsigned n, expr const * args) const {
01660 array<Z3_ast> _args(n);
01661 for (unsigned i = 0; i < n; i++) {
01662 check_context(*this, args[i]);
01663 _args[i] = args[i];
01664 }
01665 Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
01666 check_error();
01667 return expr(ctx(), r);
01668
01669 }
01670 inline expr func_decl::operator()(expr_vector const& args) const {
01671 array<Z3_ast> _args(args.size());
01672 for (unsigned i = 0; i < args.size(); i++) {
01673 check_context(*this, args[i]);
01674 _args[i] = args[i];
01675 }
01676 Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
01677 check_error();
01678 return expr(ctx(), r);
01679 }
01680 inline expr func_decl::operator()() const {
01681 Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
01682 ctx().check_error();
01683 return expr(ctx(), r);
01684 }
01685 inline expr func_decl::operator()(expr const & a) const {
01686 check_context(*this, a);
01687 Z3_ast args[1] = { a };
01688 Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
01689 ctx().check_error();
01690 return expr(ctx(), r);
01691 }
01692 inline expr func_decl::operator()(int a) const {
01693 Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
01694 Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
01695 ctx().check_error();
01696 return expr(ctx(), r);
01697 }
01698 inline expr func_decl::operator()(expr const & a1, expr const & a2) const {
01699 check_context(*this, a1); check_context(*this, a2);
01700 Z3_ast args[2] = { a1, a2 };
01701 Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
01702 ctx().check_error();
01703 return expr(ctx(), r);
01704 }
01705 inline expr func_decl::operator()(expr const & a1, int a2) const {
01706 check_context(*this, a1);
01707 Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
01708 Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
01709 ctx().check_error();
01710 return expr(ctx(), r);
01711 }
01712 inline expr func_decl::operator()(int a1, expr const & a2) const {
01713 check_context(*this, a2);
01714 Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
01715 Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
01716 ctx().check_error();
01717 return expr(ctx(), r);
01718 }
01719 inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3) const {
01720 check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
01721 Z3_ast args[3] = { a1, a2, a3 };
01722 Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
01723 ctx().check_error();
01724 return expr(ctx(), r);
01725 }
01726 inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const {
01727 check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
01728 Z3_ast args[4] = { a1, a2, a3, a4 };
01729 Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
01730 ctx().check_error();
01731 return expr(ctx(), r);
01732 }
01733 inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const {
01734 check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
01735 Z3_ast args[5] = { a1, a2, a3, a4, a5 };
01736 Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
01737 ctx().check_error();
01738 return expr(ctx(), r);
01739 }
01740
01741 inline expr to_real(expr const & a) { Z3_ast r = Z3_mk_int2real(a.ctx(), a); a.check_error(); return expr(a.ctx(), r); }
01742
01743 inline func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
01744 return range.ctx().function(name, arity, domain, range);
01745 }
01746 inline func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range) {
01747 return range.ctx().function(name, arity, domain, range);
01748 }
01749 inline func_decl function(char const * name, sort const & domain, sort const & range) {
01750 return range.ctx().function(name, domain, range);
01751 }
01752 inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range) {
01753 return range.ctx().function(name, d1, d2, range);
01754 }
01755 inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
01756 return range.ctx().function(name, d1, d2, d3, range);
01757 }
01758 inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
01759 return range.ctx().function(name, d1, d2, d3, d4, range);
01760 }
01761 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) {
01762 return range.ctx().function(name, d1, d2, d3, d4, d5, range);
01763 }
01764
01765 inline expr select(expr const & a, expr const & i) {
01766 check_context(a, i);
01767 Z3_ast r = Z3_mk_select(a.ctx(), a, i);
01768 a.check_error();
01769 return expr(a.ctx(), r);
01770 }
01771 inline expr select(expr const & a, int i) { return select(a, a.ctx().num_val(i, a.get_sort().array_domain())); }
01772 inline expr store(expr const & a, expr const & i, expr const & v) {
01773 check_context(a, i); check_context(a, v);
01774 Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
01775 a.check_error();
01776 return expr(a.ctx(), r);
01777 }
01778 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); }
01779 inline expr store(expr const & a, expr i, int v) { return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
01780 inline expr store(expr const & a, int i, int v) {
01781 return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
01782 }
01783 inline expr const_array(sort const & d, expr const & v) {
01784 check_context(d, v);
01785 Z3_ast r = Z3_mk_const_array(d.ctx(), d, v);
01786 d.check_error();
01787 return expr(d.ctx(), r);
01788 }
01789
01790 inline expr expr::substitute(expr_vector const& src, expr_vector const& dst) {
01791 assert(src.size() == dst.size());
01792 array<Z3_ast> _src(src.size());
01793 array<Z3_ast> _dst(dst.size());
01794 for (unsigned i = 0; i < src.size(); ++i) {
01795 _src[i] = src[i];
01796 _dst[i] = dst[i];
01797 }
01798 Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
01799 check_error();
01800 return expr(ctx(), r);
01801 }
01802
01803 inline expr expr::substitute(expr_vector const& dst) {
01804 array<Z3_ast> _dst(dst.size());
01805 for (unsigned i = 0; i < dst.size(); ++i) {
01806 _dst[i] = dst[i];
01807 }
01808 Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
01809 check_error();
01810 return expr(ctx(), r);
01811 }
01812
01813
01814
01815 };
01816
01819
01820 #endif
01821