Z3
src/api/c++/z3++.h
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2012 Microsoft Corporation
00003 
00004     Thin C++ layer on top of the Z3 C API.
00005     Main features:
00006       - Smart pointers for all Z3 objects.
00007       - Object-Oriented interface.
00008       - Operator overloading.
00009       - Exceptions for signining Z3 errors
00010 
00011     The C API can be used simultaneously with the C++ layer.
00012     However, if you use the C API directly, you will have to check the error conditions manually.
00013     Of course, you can invoke the method check_error() of the context object.
00014 Author:
00015 
00016     Leonardo (leonardo) 2012-03-28
00017 
00018 Notes:
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) { /* do nothing */ }
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                 // operator is not supported by given arguments.
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                 // operator is not supported by given arguments.
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                 // operator is not supported by given arguments.
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                 // operator is not supported by given arguments.
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                 // operator is not supported by given arguments.
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                 // operator is not supported by given arguments.
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                 // operator is not supported by given arguments.
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                 // operator is not supported by given arguments.
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                 // operator is not supported by given arguments.
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     // Basic functions for creating quantified formulas.
01049     // The C API should be used for creating quantifiers with patterns, weights, many variables, etc.
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 
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines