Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
z3++.h
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4  Thin C++ layer on top of the Z3 C API.
5  Main features:
6  - Smart pointers for all Z3 objects.
7  - Object-Oriented interface.
8  - Operator overloading.
9  - Exceptions for signining Z3 errors
10 
11  The C API can be used simultaneously with the C++ layer.
12  However, if you use the C API directly, you will have to check the error conditions manually.
13  Of course, you can invoke the method check_error() of the context object.
14 Author:
15 
16  Leonardo (leonardo) 2012-03-28
17 
18 Notes:
19 
20 --*/
21 #ifndef __Z3PP_H_
22 #define __Z3PP_H_
23 
24 #include<cassert>
25 #include<iostream>
26 #include<string>
27 #include<sstream>
28 #include<z3.h>
29 #include<limits.h>
30 
36 
41 
45 namespace z3 {
46 
47  class exception;
48  class config;
49  class context;
50  class symbol;
51  class params;
52  class ast;
53  class sort;
54  class func_decl;
55  class expr;
56  class solver;
57  class goal;
58  class tactic;
59  class probe;
60  class model;
61  class func_interp;
62  class func_entry;
63  class statistics;
64  class apply_result;
65  class fixedpoint;
66 
70  class exception {
71  std::string m_msg;
72  public:
73  exception(char const * msg):m_msg(msg) {}
74  char const * msg() const { return m_msg.c_str(); }
75  friend std::ostream & operator<<(std::ostream & out, exception const & e) { out << e.msg(); return out; }
76  };
77 
81  class config {
82  Z3_config m_cfg;
83  config(config const & s);
84  config & operator=(config const & s);
85  public:
86  config() { m_cfg = Z3_mk_config(); }
87  ~config() { Z3_del_config(m_cfg); }
88  operator Z3_config() const { return m_cfg; }
92  void set(char const * param, char const * value) { Z3_set_param_value(m_cfg, param, value); }
96  void set(char const * param, bool value) { Z3_set_param_value(m_cfg, param, value ? "true" : "false"); }
100  void set(char const * param, int value) {
101  std::ostringstream oss;
102  oss << value;
103  Z3_set_param_value(m_cfg, param, oss.str().c_str());
104  }
105  };
106 
110  class context {
111  Z3_context m_ctx;
112  static void error_handler(Z3_context c, Z3_error_code e) { /* do nothing */ }
113  void init(config & c) {
114  m_ctx = Z3_mk_context_rc(c);
115  Z3_set_error_handler(m_ctx, error_handler);
117  }
118  context(context const & s);
119  context & operator=(context const & s);
120  public:
121  context() { config c; init(c); }
122  context(config & c) { init(c); }
123  ~context() { Z3_del_context(m_ctx); }
124  operator Z3_context() const { return m_ctx; }
125 
129  void check_error() const {
130  Z3_error_code e = Z3_get_error_code(m_ctx);
131  if (e != Z3_OK)
132  throw exception(Z3_get_error_msg_ex(m_ctx, e));
133  }
134 
138  void set(char const * param, char const * value) { Z3_update_param_value(m_ctx, param, value); }
142  void set(char const * param, bool value) { Z3_update_param_value(m_ctx, param, value ? "true" : "false"); }
146  void set(char const * param, int value) {
147  std::ostringstream oss;
148  oss << value;
149  Z3_update_param_value(m_ctx, param, oss.str().c_str());
150  }
151 
156  void interrupt() { Z3_interrupt(m_ctx); }
157 
161  symbol str_symbol(char const * s);
165  symbol int_symbol(int n);
169  sort bool_sort();
173  sort int_sort();
177  sort real_sort();
181  sort bv_sort(unsigned sz);
187  sort array_sort(sort d, sort r);
188 
189  func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range);
190  func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range);
191  func_decl function(char const * name, sort const & domain, sort const & range);
192  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range);
193  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range);
194  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range);
195  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range);
196 
197  expr constant(symbol const & name, sort const & s);
198  expr constant(char const * name, sort const & s);
199  expr bool_const(char const * name);
200  expr int_const(char const * name);
201  expr real_const(char const * name);
202  expr bv_const(char const * name, unsigned sz);
203 
204  expr bool_val(bool b);
205 
206  expr int_val(int n);
207  expr int_val(unsigned n);
208  expr int_val(__int64 n);
209  expr int_val(__uint64 n);
210  expr int_val(char const * n);
211 
212  expr real_val(int n, int d);
213  expr real_val(int n);
214  expr real_val(unsigned n);
215  expr real_val(__int64 n);
217  expr real_val(char const * n);
218 
219  expr bv_val(int n, unsigned sz);
220  expr bv_val(unsigned n, unsigned sz);
221  expr bv_val(__int64 n, unsigned sz);
222  expr bv_val(__uint64 n, unsigned sz);
223  expr bv_val(char const * n, unsigned sz);
224 
225  expr num_val(int n, sort const & s);
226  };
227 
228  template<typename T>
229  class array {
230  T * m_array;
231  unsigned m_size;
232  array(array const & s);
233  array & operator=(array const & s);
234  public:
235  array(unsigned sz):m_size(sz) { m_array = new T[sz]; }
236  ~array() { delete[] m_array; }
237  unsigned size() const { return m_size; }
238  T & operator[](unsigned i) { assert(i < m_size); return m_array[i]; }
239  T const & operator[](unsigned i) const { assert(i < m_size); return m_array[i]; }
240  T const * ptr() const { return m_array; }
241  T * ptr() { return m_array; }
242  };
243 
244  class object {
245  protected:
247  public:
248  object(context & c):m_ctx(&c) {}
249  object(object const & s):m_ctx(s.m_ctx) {}
250  context & ctx() const { return *m_ctx; }
251  void check_error() const { m_ctx->check_error(); }
252  friend void check_context(object const & a, object const & b) { assert(a.m_ctx == b.m_ctx); }
253  };
254 
255  class symbol : public object {
256  Z3_symbol m_sym;
257  public:
258  symbol(context & c, Z3_symbol s):object(c), m_sym(s) {}
259  symbol(symbol const & s):object(s), m_sym(s.m_sym) {}
260  symbol & operator=(symbol const & s) { m_ctx = s.m_ctx; m_sym = s.m_sym; return *this; }
261  operator Z3_symbol() const { return m_sym; }
262  Z3_symbol_kind kind() const { return Z3_get_symbol_kind(ctx(), m_sym); }
263  std::string str() const { assert(kind() == Z3_STRING_SYMBOL); return Z3_get_symbol_string(ctx(), m_sym); }
264  int to_int() const { assert(kind() == Z3_INT_SYMBOL); return Z3_get_symbol_int(ctx(), m_sym); }
265  friend std::ostream & operator<<(std::ostream & out, symbol const & s) {
266  if (s.kind() == Z3_INT_SYMBOL)
267  out << "k!" << s.to_int();
268  else
269  out << s.str().c_str();
270  return out;
271  }
272  };
273 
274  class params : public object {
275  Z3_params m_params;
276  public:
277  params(context & c):object(c) { m_params = Z3_mk_params(c); Z3_params_inc_ref(ctx(), m_params); }
278  params(params const & s):object(s), m_params(s.m_params) { Z3_params_inc_ref(ctx(), m_params); }
279  ~params() { Z3_params_dec_ref(ctx(), m_params); }
280  operator Z3_params() const { return m_params; }
281  params & operator=(params const & s) {
282  Z3_params_inc_ref(s.ctx(), s.m_params);
283  Z3_params_dec_ref(ctx(), m_params);
284  m_ctx = s.m_ctx;
285  m_params = s.m_params;
286  return *this;
287  }
288  void set(char const * k, bool b) { Z3_params_set_bool(ctx(), m_params, ctx().str_symbol(k), b); }
289  void set(char const * k, unsigned n) { Z3_params_set_uint(ctx(), m_params, ctx().str_symbol(k), n); }
290  void set(char const * k, double n) { Z3_params_set_double(ctx(), m_params, ctx().str_symbol(k), n); }
291  void set(char const * k, symbol const & s) { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), s); }
292  friend std::ostream & operator<<(std::ostream & out, params const & p) { out << Z3_params_to_string(p.ctx(), p); return out; }
293  };
294 
295  class ast : public object {
296  protected:
298  public:
299  ast(context & c):object(c), m_ast(0) {}
300  ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
301  ast(ast const & s):object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
302  ~ast() { if (m_ast) Z3_dec_ref(*m_ctx, m_ast); }
303  operator Z3_ast() const { return m_ast; }
304  operator bool() const { return m_ast != 0; }
305  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; }
306  Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }
307  unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }
308  friend std::ostream & operator<<(std::ostream & out, ast const & n) { out << Z3_ast_to_string(n.ctx(), n.m_ast); return out; }
309 
313  friend bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b) != 0; }
314  };
315 
319  class sort : public ast {
320  public:
321  sort(context & c):ast(c) {}
322  sort(context & c, Z3_sort s):ast(c, reinterpret_cast<Z3_ast>(s)) {}
323  sort(sort const & s):ast(s) {}
324  operator Z3_sort() const { return reinterpret_cast<Z3_sort>(m_ast); }
328  sort & operator=(sort const & s) { return static_cast<sort&>(ast::operator=(s)); }
332  Z3_sort_kind sort_kind() const { return Z3_get_sort_kind(*m_ctx, *this); }
333 
337  bool is_bool() const { return sort_kind() == Z3_BOOL_SORT; }
341  bool is_int() const { return sort_kind() == Z3_INT_SORT; }
345  bool is_real() const { return sort_kind() == Z3_REAL_SORT; }
349  bool is_arith() const { return is_int() || is_real(); }
353  bool is_bv() const { return sort_kind() == Z3_BV_SORT; }
357  bool is_array() const { return sort_kind() == Z3_ARRAY_SORT; }
361  bool is_datatype() const { return sort_kind() == Z3_DATATYPE_SORT; }
365  bool is_relation() const { return sort_kind() == Z3_RELATION_SORT; }
369  bool is_finite_domain() const { return sort_kind() == Z3_FINITE_DOMAIN_SORT; }
370 
376  unsigned bv_size() const { assert(is_bv()); unsigned r = Z3_get_bv_sort_size(ctx(), *this); check_error(); return r; }
377 
383  sort array_domain() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_domain(ctx(), *this); check_error(); return sort(ctx(), s); }
389  sort array_range() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_range(ctx(), *this); check_error(); return sort(ctx(), s); }
390  };
391 
396  class func_decl : public ast {
397  public:
398  func_decl(context & c):ast(c) {}
399  func_decl(context & c, Z3_func_decl n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
400  func_decl(func_decl const & s):ast(s) {}
401  operator Z3_func_decl() const { return reinterpret_cast<Z3_func_decl>(m_ast); }
402  func_decl & operator=(func_decl const & s) { return static_cast<func_decl&>(ast::operator=(s)); }
403 
404  unsigned arity() const { return Z3_get_arity(ctx(), *this); }
405  sort domain(unsigned i) const { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }
406  sort range() const { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }
407  symbol name() const { Z3_symbol s = Z3_get_decl_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
408  Z3_decl_kind decl_kind() const { return Z3_get_decl_kind(ctx(), *this); }
409 
410  bool is_const() const { return arity() == 0; }
411 
412  expr operator()(unsigned n, expr const * args) const;
413  expr operator()(expr const & a) const;
414  expr operator()(int a) const;
415  expr operator()(expr const & a1, expr const & a2) const;
416  expr operator()(expr const & a1, int a2) const;
417  expr operator()(int a1, expr const & a2) const;
418  expr operator()(expr const & a1, expr const & a2, expr const & a3) const;
419  expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const;
420  expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const;
421  };
422 
427  class expr : public ast {
428  public:
429  expr(context & c):ast(c) {}
430  expr(context & c, Z3_ast n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
431  expr(expr const & n):ast(n) {}
432  expr & operator=(expr const & n) { return static_cast<expr&>(ast::operator=(n)); }
433 
437  sort get_sort() const { Z3_sort s = Z3_get_sort(*m_ctx, m_ast); check_error(); return sort(*m_ctx, s); }
438 
442  bool is_bool() const { return get_sort().is_bool(); }
446  bool is_int() const { return get_sort().is_int(); }
450  bool is_real() const { return get_sort().is_real(); }
454  bool is_arith() const { return get_sort().is_arith(); }
458  bool is_bv() const { return get_sort().is_bv(); }
462  bool is_array() const { return get_sort().is_array(); }
466  bool is_datatype() const { return get_sort().is_datatype(); }
470  bool is_relation() const { return get_sort().is_relation(); }
479  bool is_finite_domain() const { return get_sort().is_finite_domain(); }
480 
484  bool is_numeral() const { return kind() == Z3_NUMERAL_AST; }
488  bool is_app() const { return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
492  bool is_const() const { return is_app() && num_args() == 0; }
496  bool is_quantifier() const { return kind() == Z3_QUANTIFIER_AST; }
500  bool is_var() const { return kind() == Z3_VAR_AST; }
501 
505  bool is_well_sorted() const { bool r = Z3_is_well_sorted(ctx(), m_ast) != 0; check_error(); return r; }
506 
507  operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
508 
515  func_decl decl() const { Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }
522  unsigned num_args() const { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
530  expr arg(unsigned i) const { Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }
531 
537  expr body() const { assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
538 
544  friend expr operator!(expr const & a) {
545  assert(a.is_bool());
546  Z3_ast r = Z3_mk_not(a.ctx(), a);
547  a.check_error();
548  return expr(a.ctx(), r);
549  }
550 
557  friend expr operator&&(expr const & a, expr const & b) {
558  check_context(a, b);
559  assert(a.is_bool() && b.is_bool());
560  Z3_ast args[2] = { a, b };
561  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
562  a.check_error();
563  return expr(a.ctx(), r);
564  }
565 
572  friend expr operator&&(expr const & a, bool b) { return a && a.ctx().bool_val(b); }
579  friend expr operator&&(bool a, expr const & b) { return b.ctx().bool_val(a) && b; }
580 
587  friend expr operator||(expr const & a, expr const & b) {
588  check_context(a, b);
589  assert(a.is_bool() && b.is_bool());
590  Z3_ast args[2] = { a, b };
591  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
592  a.check_error();
593  return expr(a.ctx(), r);
594  }
601  friend expr operator||(expr const & a, bool b) { return a || a.ctx().bool_val(b); }
608  friend expr operator||(bool a, expr const & b) { return b.ctx().bool_val(a) || b; }
609 
610  friend expr implies(expr const & a, expr const & b) {
611  check_context(a, b);
612  assert(a.is_bool() && b.is_bool());
613  Z3_ast r = Z3_mk_implies(a.ctx(), a, b);
614  a.check_error();
615  return expr(a.ctx(), r);
616  }
617 
618  friend expr operator==(expr const & a, expr const & b) {
619  check_context(a, b);
620  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
621  a.check_error();
622  return expr(a.ctx(), r);
623  }
624  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()); }
625  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; }
626 
627  friend expr operator!=(expr const & a, expr const & b) {
628  check_context(a, b);
629  Z3_ast args[2] = { a, b };
630  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
631  a.check_error();
632  return expr(a.ctx(), r);
633  }
634  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()); }
635  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; }
636 
637  friend expr operator+(expr const & a, expr const & b) {
638  check_context(a, b);
639  Z3_ast r;
640  if (a.is_arith() && b.is_arith()) {
641  Z3_ast args[2] = { a, b };
642  r = Z3_mk_add(a.ctx(), 2, args);
643  }
644  else if (a.is_bv() && b.is_bv()) {
645  r = Z3_mk_bvadd(a.ctx(), a, b);
646  }
647  else {
648  // operator is not supported by given arguments.
649  assert(false);
650  }
651  a.check_error();
652  return expr(a.ctx(), r);
653  }
654  friend expr operator+(expr const & a, int b) { return a + a.ctx().num_val(b, a.get_sort()); }
655  friend expr operator+(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) + b; }
656 
657  friend expr operator*(expr const & a, expr const & b) {
658  check_context(a, b);
659  Z3_ast r;
660  if (a.is_arith() && b.is_arith()) {
661  Z3_ast args[2] = { a, b };
662  r = Z3_mk_mul(a.ctx(), 2, args);
663  }
664  else if (a.is_bv() && b.is_bv()) {
665  r = Z3_mk_bvmul(a.ctx(), a, b);
666  }
667  else {
668  // operator is not supported by given arguments.
669  assert(false);
670  }
671  a.check_error();
672  return expr(a.ctx(), r);
673  }
674  friend expr operator*(expr const & a, int b) { return a * a.ctx().num_val(b, a.get_sort()); }
675  friend expr operator*(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) * b; }
676 
680  friend expr pw(expr const & a, expr const & b) {
681  assert(a.is_arith() && b.is_arith());
682  check_context(a, b);
683  Z3_ast r = Z3_mk_power(a.ctx(), a, b);
684  a.check_error();
685  return expr(a.ctx(), r);
686  }
687  friend expr pw(expr const & a, int b) { return pw(a, a.ctx().num_val(b, a.get_sort())); }
688  friend expr pw(int a, expr const & b) { return pw(b.ctx().num_val(a, b.get_sort()), b); }
689 
690  friend expr operator/(expr const & a, expr const & b) {
691  check_context(a, b);
692  Z3_ast r;
693  if (a.is_arith() && b.is_arith()) {
694  r = Z3_mk_div(a.ctx(), a, b);
695  }
696  else if (a.is_bv() && b.is_bv()) {
697  r = Z3_mk_bvsdiv(a.ctx(), a, b);
698  }
699  else {
700  // operator is not supported by given arguments.
701  assert(false);
702  }
703  a.check_error();
704  return expr(a.ctx(), r);
705  }
706  friend expr operator/(expr const & a, int b) { return a / a.ctx().num_val(b, a.get_sort()); }
707  friend expr operator/(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) / b; }
708 
709  friend expr operator-(expr const & a) {
710  Z3_ast r;
711  if (a.is_arith()) {
712  r = Z3_mk_unary_minus(a.ctx(), a);
713  }
714  else if (a.is_bv()) {
715  r = Z3_mk_bvneg(a.ctx(), a);
716  }
717  else {
718  // operator is not supported by given arguments.
719  assert(false);
720  }
721  a.check_error();
722  return expr(a.ctx(), r);
723  }
724 
725  friend expr operator-(expr const & a, expr const & b) {
726  check_context(a, b);
727  Z3_ast r;
728  if (a.is_arith() && b.is_arith()) {
729  Z3_ast args[2] = { a, b };
730  r = Z3_mk_sub(a.ctx(), 2, args);
731  }
732  else if (a.is_bv() && b.is_bv()) {
733  r = Z3_mk_bvsub(a.ctx(), a, b);
734  }
735  else {
736  // operator is not supported by given arguments.
737  assert(false);
738  }
739  a.check_error();
740  return expr(a.ctx(), r);
741  }
742  friend expr operator-(expr const & a, int b) { return a - a.ctx().num_val(b, a.get_sort()); }
743  friend expr operator-(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) - a; }
744 
745  friend expr operator<=(expr const & a, expr const & b) {
746  check_context(a, b);
747  Z3_ast r;
748  if (a.is_arith() && b.is_arith()) {
749  r = Z3_mk_le(a.ctx(), a, b);
750  }
751  else if (a.is_bv() && b.is_bv()) {
752  r = Z3_mk_bvsle(a.ctx(), a, b);
753  }
754  else {
755  // operator is not supported by given arguments.
756  assert(false);
757  }
758  a.check_error();
759  return expr(a.ctx(), r);
760  }
761  friend expr operator<=(expr const & a, int b) { return a <= a.ctx().num_val(b, a.get_sort()); }
762  friend expr operator<=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) <= a; }
763 
764  friend expr operator>=(expr const & a, expr const & b) {
765  check_context(a, b);
766  Z3_ast r;
767  if (a.is_arith() && b.is_arith()) {
768  r = Z3_mk_ge(a.ctx(), a, b);
769  }
770  else if (a.is_bv() && b.is_bv()) {
771  r = Z3_mk_bvsge(a.ctx(), a, b);
772  }
773  else {
774  // operator is not supported by given arguments.
775  assert(false);
776  }
777  a.check_error();
778  return expr(a.ctx(), r);
779  }
780  friend expr operator>=(expr const & a, int b) { return a >= a.ctx().num_val(b, a.get_sort()); }
781  friend expr operator>=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) >= a; }
782 
783  friend expr operator<(expr const & a, expr const & b) {
784  check_context(a, b);
785  Z3_ast r;
786  if (a.is_arith() && b.is_arith()) {
787  r = Z3_mk_lt(a.ctx(), a, b);
788  }
789  else if (a.is_bv() && b.is_bv()) {
790  r = Z3_mk_bvslt(a.ctx(), a, b);
791  }
792  else {
793  // operator is not supported by given arguments.
794  assert(false);
795  }
796  a.check_error();
797  return expr(a.ctx(), r);
798  }
799  friend expr operator<(expr const & a, int b) { return a < a.ctx().num_val(b, a.get_sort()); }
800  friend expr operator<(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) < a; }
801 
802  friend expr operator>(expr const & a, expr const & b) {
803  check_context(a, b);
804  Z3_ast r;
805  if (a.is_arith() && b.is_arith()) {
806  r = Z3_mk_gt(a.ctx(), a, b);
807  }
808  else if (a.is_bv() && b.is_bv()) {
809  r = Z3_mk_bvsgt(a.ctx(), a, b);
810  }
811  else {
812  // operator is not supported by given arguments.
813  assert(false);
814  }
815  a.check_error();
816  return expr(a.ctx(), r);
817  }
818  friend expr operator>(expr const & a, int b) { return a > a.ctx().num_val(b, a.get_sort()); }
819  friend expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > a; }
820 
821  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); }
822  friend expr operator&(expr const & a, int b) { return a & a.ctx().num_val(b, a.get_sort()); }
823  friend expr operator&(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) & b; }
824 
825  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); }
826  friend expr operator^(expr const & a, int b) { return a ^ a.ctx().num_val(b, a.get_sort()); }
827  friend expr operator^(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) ^ b; }
828 
829  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); }
830  friend expr operator|(expr const & a, int b) { return a | a.ctx().num_val(b, a.get_sort()); }
831  friend expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; }
832 
833  friend expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
834 
838  expr simplify() const { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
842  expr simplify(params const & p) const { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
843  };
844 
849  inline expr to_expr(context & c, Z3_ast a) {
850  c.check_error();
851  assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
852  Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
853  Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
855  return expr(c, a);
856  }
857 
858  inline sort to_sort(context & c, Z3_sort s) {
859  c.check_error();
860  return sort(c, s);
861  }
862 
864  c.check_error();
865  return func_decl(c, f);
866  }
867 
871  inline expr ule(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
872  inline expr ule(expr const & a, int b) { return ule(a, a.ctx().num_val(b, a.get_sort())); }
873  inline expr ule(int a, expr const & b) { return ule(b.ctx().num_val(a, b.get_sort()), a); }
877  inline expr ult(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }
878  inline expr ult(expr const & a, int b) { return ult(a, a.ctx().num_val(b, a.get_sort())); }
879  inline expr ult(int a, expr const & b) { return ult(b.ctx().num_val(a, b.get_sort()), a); }
883  inline expr uge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }
884  inline expr uge(expr const & a, int b) { return uge(a, a.ctx().num_val(b, a.get_sort())); }
885  inline expr uge(int a, expr const & b) { return uge(b.ctx().num_val(a, b.get_sort()), a); }
889  inline expr ugt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
890  inline expr ugt(expr const & a, int b) { return ugt(a, a.ctx().num_val(b, a.get_sort())); }
891  inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), a); }
895  inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
896  inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); }
897  inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), a); }
898 
899  // Basic functions for creating quantified formulas.
900  // The C API should be used for creating quantifiers with patterns, weights, many variables, etc.
901  inline expr forall(expr const & x, expr const & b) {
902  check_context(x, b);
903  Z3_app vars[] = {(Z3_app) x};
904  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
905  }
906  inline expr forall(expr const & x1, expr const & x2, expr const & b) {
907  check_context(x1, b); check_context(x2, b);
908  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
909  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
910  }
911  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
912  check_context(x1, b); check_context(x2, b); check_context(x3, b);
913  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
914  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
915  }
916  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
917  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
918  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
919  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
920  }
921  inline expr exists(expr const & x, expr const & b) {
922  check_context(x, b);
923  Z3_app vars[] = {(Z3_app) x};
924  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
925  }
926  inline expr exists(expr const & x1, expr const & x2, expr const & b) {
927  check_context(x1, b); check_context(x2, b);
928  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
929  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
930  }
931  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
932  check_context(x1, b); check_context(x2, b); check_context(x3, b);
933  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
934  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
935  }
936  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
937  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
938  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
939  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
940  }
941 
942  template<typename T> class cast_ast;
943 
944  template<> class cast_ast<ast> {
945  public:
946  ast operator()(context & c, Z3_ast a) { return ast(c, a); }
947  };
948 
949  template<> class cast_ast<expr> {
950  public:
952  assert(Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
953  Z3_get_ast_kind(c, a) == Z3_APP_AST ||
955  Z3_get_ast_kind(c, a) == Z3_VAR_AST);
956  return expr(c, a);
957  }
958  };
959 
960  template<> class cast_ast<sort> {
961  public:
963  assert(Z3_get_ast_kind(c, a) == Z3_SORT_AST);
964  return sort(c, reinterpret_cast<Z3_sort>(a));
965  }
966  };
967 
968  template<> class cast_ast<func_decl> {
969  public:
971  assert(Z3_get_ast_kind(c, a) == Z3_FUNC_DECL_AST);
972  return func_decl(c, reinterpret_cast<Z3_func_decl>(a));
973  }
974  };
975 
976  template<typename T>
977  class ast_vector_tpl : public object {
978  Z3_ast_vector m_vector;
979  void init(Z3_ast_vector v) { Z3_ast_vector_inc_ref(ctx(), v); m_vector = v; }
980  public:
982  ast_vector_tpl(context & c, Z3_ast_vector v):object(c) { init(v); }
983  ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
985  operator Z3_ast_vector() const { return m_vector; }
986  unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); }
987  T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
988  void push_back(T const & e) { Z3_ast_vector_push(ctx(), m_vector, e); check_error(); }
989  void resize(unsigned sz) { Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }
990  T back() const { return operator[](size() - 1); }
991  void pop_back() { assert(size() > 0); resize(size() - 1); }
992  bool empty() const { return size() == 0; }
994  Z3_ast_vector_inc_ref(s.ctx(), s.m_vector);
995  Z3_ast_vector_dec_ref(ctx(), m_vector);
996  m_ctx = s.m_ctx;
997  m_vector = s.m_vector;
998  return *this;
999  }
1000  friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
1001  };
1002 
1007 
1008  class func_entry : public object {
1009  Z3_func_entry m_entry;
1010  void init(Z3_func_entry e) {
1011  m_entry = e;
1012  Z3_func_entry_inc_ref(ctx(), m_entry);
1013  }
1014  public:
1015  func_entry(context & c, Z3_func_entry e):object(c) { init(e); }
1016  func_entry(func_entry const & s):object(s) { init(s.m_entry); }
1018  operator Z3_func_entry() const { return m_entry; }
1020  Z3_func_entry_inc_ref(s.ctx(), s.m_entry);
1021  Z3_func_entry_dec_ref(ctx(), m_entry);
1022  m_ctx = s.m_ctx;
1023  m_entry = s.m_entry;
1024  return *this;
1025  }
1026  expr value() const { Z3_ast r = Z3_func_entry_get_value(ctx(), m_entry); check_error(); return expr(ctx(), r); }
1027  unsigned num_args() const { unsigned r = Z3_func_entry_get_num_args(ctx(), m_entry); check_error(); return r; }
1028  expr arg(unsigned i) const { Z3_ast r = Z3_func_entry_get_arg(ctx(), m_entry, i); check_error(); return expr(ctx(), r); }
1029  };
1030 
1031  class func_interp : public object {
1032  Z3_func_interp m_interp;
1033  void init(Z3_func_interp e) {
1034  m_interp = e;
1035  Z3_func_interp_inc_ref(ctx(), m_interp);
1036  }
1037  public:
1038  func_interp(context & c, Z3_func_interp e):object(c) { init(e); }
1039  func_interp(func_interp const & s):object(s) { init(s.m_interp); }
1041  operator Z3_func_interp() const { return m_interp; }
1043  Z3_func_interp_inc_ref(s.ctx(), s.m_interp);
1044  Z3_func_interp_dec_ref(ctx(), m_interp);
1045  m_ctx = s.m_ctx;
1046  m_interp = s.m_interp;
1047  return *this;
1048  }
1049  expr else_value() const { Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), r); }
1050  unsigned num_entries() const { unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }
1051  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); }
1052  };
1053 
1054  class model : public object {
1055  Z3_model m_model;
1056  void init(Z3_model m) {
1057  m_model = m;
1058  Z3_model_inc_ref(ctx(), m);
1059  }
1060  public:
1061  model(context & c, Z3_model m):object(c) { init(m); }
1062  model(model const & s):object(s) { init(s.m_model); }
1063  ~model() { Z3_model_dec_ref(ctx(), m_model); }
1064  operator Z3_model() const { return m_model; }
1065  model & operator=(model const & s) {
1066  Z3_model_inc_ref(s.ctx(), s.m_model);
1067  Z3_model_dec_ref(ctx(), m_model);
1068  m_ctx = s.m_ctx;
1069  m_model = s.m_model;
1070  return *this;
1071  }
1072 
1073  expr eval(expr const & n, bool model_completion=false) const {
1074  check_context(*this, n);
1075  Z3_ast r;
1076  Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
1077  check_error();
1078  if (status == Z3_FALSE)
1079  throw exception("failed to evaluate expression");
1080  return expr(ctx(), r);
1081  }
1082 
1083  unsigned num_consts() const { return Z3_model_get_num_consts(ctx(), m_model); }
1084  unsigned num_funcs() const { return Z3_model_get_num_funcs(ctx(), m_model); }
1085  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); }
1086  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); }
1087  unsigned size() const { return num_consts() + num_funcs(); }
1088  func_decl operator[](unsigned i) const { return i < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts()); }
1089 
1091  check_context(*this, c);
1092  Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);
1093  check_error();
1094  return expr(ctx(), r);
1095  }
1097  check_context(*this, f);
1098  Z3_func_interp r = Z3_model_get_func_interp(ctx(), m_model, f);
1099  check_error();
1100  return func_interp(ctx(), r);
1101  }
1102 
1103  friend std::ostream & operator<<(std::ostream & out, model const & m) { out << Z3_model_to_string(m.ctx(), m); return out; }
1104  };
1105 
1106  class stats : public object {
1107  Z3_stats m_stats;
1108  void init(Z3_stats e) {
1109  m_stats = e;
1110  Z3_stats_inc_ref(ctx(), m_stats);
1111  }
1112  public:
1113  stats(context & c):object(c), m_stats(0) {}
1114  stats(context & c, Z3_stats e):object(c) { init(e); }
1115  stats(stats const & s):object(s) { init(s.m_stats); }
1116  ~stats() { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); }
1117  operator Z3_stats() const { return m_stats; }
1118  stats & operator=(stats const & s) {
1119  Z3_stats_inc_ref(s.ctx(), s.m_stats);
1120  if (m_stats) Z3_stats_dec_ref(ctx(), m_stats);
1121  m_ctx = s.m_ctx;
1122  m_stats = s.m_stats;
1123  return *this;
1124  }
1125  unsigned size() const { return Z3_stats_size(ctx(), m_stats); }
1126  std::string key(unsigned i) const { Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; }
1127  bool is_uint(unsigned i) const { Z3_bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r != 0; }
1128  bool is_double(unsigned i) const { Z3_bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r != 0; }
1129  unsigned uint_value(unsigned i) const { unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; }
1130  double double_value(unsigned i) const { double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
1131  friend std::ostream & operator<<(std::ostream & out, stats const & s) { out << Z3_stats_to_string(s.ctx(), s); return out; }
1132  };
1133 
1136  };
1137 
1138  inline std::ostream & operator<<(std::ostream & out, check_result r) {
1139  if (r == unsat) out << "unsat";
1140  else if (r == sat) out << "sat";
1141  else out << "unknown";
1142  return out;
1143  }
1144 
1146  if (l == Z3_L_TRUE) return sat;
1147  else if (l == Z3_L_FALSE) return unsat;
1148  return unknown;
1149  }
1150 
1151  class solver : public object {
1152  Z3_solver m_solver;
1153  void init(Z3_solver s) {
1154  m_solver = s;
1155  Z3_solver_inc_ref(ctx(), s);
1156  }
1157  public:
1158  solver(context & c):object(c) { init(Z3_mk_solver(c)); }
1159  solver(context & c, Z3_solver s):object(c) { init(s); }
1160  solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); }
1161  solver(solver const & s):object(s) { init(s.m_solver); }
1162  ~solver() { Z3_solver_dec_ref(ctx(), m_solver); }
1163  operator Z3_solver() const { return m_solver; }
1164  solver & operator=(solver const & s) {
1165  Z3_solver_inc_ref(s.ctx(), s.m_solver);
1166  Z3_solver_dec_ref(ctx(), m_solver);
1167  m_ctx = s.m_ctx;
1168  m_solver = s.m_solver;
1169  return *this;
1170  }
1171  void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
1172  void push() { Z3_solver_push(ctx(), m_solver); check_error(); }
1173  void pop(unsigned n = 1) { Z3_solver_pop(ctx(), m_solver, n); check_error(); }
1174  void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); }
1175  void add(expr const & e) { assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); }
1176  void add(expr const & e, expr const & p) {
1177  assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
1178  Z3_solver_assert_and_track(ctx(), m_solver, e, p);
1179  check_error();
1180  }
1181  void add(expr const & e, char const * p) {
1182  add(e, ctx().bool_const(p));
1183  }
1185  check_result check(unsigned n, expr * const assumptions) {
1186  array<Z3_ast> _assumptions(n);
1187  for (unsigned i = 0; i < n; i++) {
1188  check_context(*this, assumptions[i]);
1189  _assumptions[i] = assumptions[i];
1190  }
1191  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
1192  check_error();
1193  return to_check_result(r);
1194  }
1195  check_result check(expr_vector assumptions) {
1196  unsigned n = assumptions.size();
1197  array<Z3_ast> _assumptions(n);
1198  for (unsigned i = 0; i < n; i++) {
1199  check_context(*this, assumptions[i]);
1200  _assumptions[i] = assumptions[i];
1201  }
1202  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
1203  check_error();
1204  return to_check_result(r);
1205  }
1206  model get_model() const { Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }
1207  std::string reason_unknown() const { Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }
1208  stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }
1209  expr_vector unsat_core() const { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
1210  expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
1211  expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
1212  friend std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
1213  };
1214 
1215  class goal : public object {
1216  Z3_goal m_goal;
1217  void init(Z3_goal s) {
1218  m_goal = s;
1219  Z3_goal_inc_ref(ctx(), s);
1220  }
1221  public:
1222  goal(context & c, bool models=true, bool unsat_cores=false, bool proofs=false):object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); }
1223  goal(context & c, Z3_goal s):object(c) { init(s); }
1224  goal(goal const & s):object(s) { init(s.m_goal); }
1225  ~goal() { Z3_goal_dec_ref(ctx(), m_goal); }
1226  operator Z3_goal() const { return m_goal; }
1227  goal & operator=(goal const & s) {
1228  Z3_goal_inc_ref(s.ctx(), s.m_goal);
1229  Z3_goal_dec_ref(ctx(), m_goal);
1230  m_ctx = s.m_ctx;
1231  m_goal = s.m_goal;
1232  return *this;
1233  }
1234  void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
1235  unsigned size() const { return Z3_goal_size(ctx(), m_goal); }
1236  expr operator[](unsigned i) const { Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
1237  Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); }
1238  bool inconsistent() const { return Z3_goal_inconsistent(ctx(), m_goal) != 0; }
1239  unsigned depth() const { return Z3_goal_depth(ctx(), m_goal); }
1240  void reset() { Z3_goal_reset(ctx(), m_goal); }
1241  unsigned num_exprs() const { return Z3_goal_num_exprs(ctx(), m_goal); }
1242  bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal) != 0; }
1243  bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal) != 0; }
1244  friend std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; }
1245  };
1246 
1247  class apply_result : public object {
1248  Z3_apply_result m_apply_result;
1249  void init(Z3_apply_result s) {
1250  m_apply_result = s;
1252  }
1253  public:
1254  apply_result(context & c, Z3_apply_result s):object(c) { init(s); }
1255  apply_result(apply_result const & s):object(s) { init(s.m_apply_result); }
1256  ~apply_result() { Z3_apply_result_dec_ref(ctx(), m_apply_result); }
1257  operator Z3_apply_result() const { return m_apply_result; }
1259  Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result);
1260  Z3_apply_result_dec_ref(ctx(), m_apply_result);
1261  m_ctx = s.m_ctx;
1262  m_apply_result = s.m_apply_result;
1263  return *this;
1264  }
1265  unsigned size() const { return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }
1266  goal operator[](unsigned i) const { Z3_goal r = Z3_apply_result_get_subgoal(ctx(), m_apply_result, i); check_error(); return goal(ctx(), r); }
1267  goal operator[](int i) const { assert(i >= 0); return this->operator[](static_cast<unsigned>(i)); }
1268  model convert_model(model const & m, unsigned i = 0) const {
1269  check_context(*this, m);
1270  Z3_model new_m = Z3_apply_result_convert_model(ctx(), m_apply_result, i, m);
1271  check_error();
1272  return model(ctx(), new_m);
1273  }
1274  friend std::ostream & operator<<(std::ostream & out, apply_result const & r) { out << Z3_apply_result_to_string(r.ctx(), r); return out; }
1275  };
1276 
1277  class tactic : public object {
1278  Z3_tactic m_tactic;
1279  void init(Z3_tactic s) {
1280  m_tactic = s;
1281  Z3_tactic_inc_ref(ctx(), s);
1282  }
1283  public:
1284  tactic(context & c, char const * name):object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); }
1285  tactic(context & c, Z3_tactic s):object(c) { init(s); }
1286  tactic(tactic const & s):object(s) { init(s.m_tactic); }
1287  ~tactic() { Z3_tactic_dec_ref(ctx(), m_tactic); }
1288  operator Z3_tactic() const { return m_tactic; }
1289  tactic & operator=(tactic const & s) {
1290  Z3_tactic_inc_ref(s.ctx(), s.m_tactic);
1291  Z3_tactic_dec_ref(ctx(), m_tactic);
1292  m_ctx = s.m_ctx;
1293  m_tactic = s.m_tactic;
1294  return *this;
1295  }
1296  solver mk_solver() const { Z3_solver r = Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error(); return solver(ctx(), r); }
1297  apply_result apply(goal const & g) const {
1298  check_context(*this, g);
1299  Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g);
1300  check_error();
1301  return apply_result(ctx(), r);
1302  }
1303  apply_result operator()(goal const & g) const {
1304  return apply(g);
1305  }
1306  std::string help() const { char const * r = Z3_tactic_get_help(ctx(), m_tactic); check_error(); return r; }
1307  friend tactic operator&(tactic const & t1, tactic const & t2) {
1308  check_context(t1, t2);
1309  Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
1310  t1.check_error();
1311  return tactic(t1.ctx(), r);
1312  }
1313  friend tactic operator|(tactic const & t1, tactic const & t2) {
1314  check_context(t1, t2);
1315  Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
1316  t1.check_error();
1317  return tactic(t1.ctx(), r);
1318  }
1319  friend tactic repeat(tactic const & t, unsigned max=UINT_MAX) {
1320  Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
1321  t.check_error();
1322  return tactic(t.ctx(), r);
1323  }
1324  friend tactic with(tactic const & t, params const & p) {
1325  Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
1326  t.check_error();
1327  return tactic(t.ctx(), r);
1328  }
1329  friend tactic try_for(tactic const & t, unsigned ms) {
1330  Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
1331  t.check_error();
1332  return tactic(t.ctx(), r);
1333  }
1334  };
1335 
1336  class probe : public object {
1337  Z3_probe m_probe;
1338  void init(Z3_probe s) {
1339  m_probe = s;
1340  Z3_probe_inc_ref(ctx(), s);
1341  }
1342  public:
1343  probe(context & c, char const * name):object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); }
1344  probe(context & c, double val):object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); }
1345  probe(context & c, Z3_probe s):object(c) { init(s); }
1346  probe(probe const & s):object(s) { init(s.m_probe); }
1347  ~probe() { Z3_probe_dec_ref(ctx(), m_probe); }
1348  operator Z3_probe() const { return m_probe; }
1349  probe & operator=(probe const & s) {
1350  Z3_probe_inc_ref(s.ctx(), s.m_probe);
1351  Z3_probe_dec_ref(ctx(), m_probe);
1352  m_ctx = s.m_ctx;
1353  m_probe = s.m_probe;
1354  return *this;
1355  }
1356  double apply(goal const & g) const { double r = Z3_probe_apply(ctx(), m_probe, g); check_error(); return r; }
1357  double operator()(goal const & g) const { return apply(g); }
1358  friend probe operator<=(probe const & p1, probe const & p2) {
1359  check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1360  }
1361  friend probe operator<=(probe const & p1, double p2) { return p1 <= probe(p1.ctx(), p2); }
1362  friend probe operator<=(double p1, probe const & p2) { return probe(p2.ctx(), p1) <= p2; }
1363  friend probe operator>=(probe const & p1, probe const & p2) {
1364  check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1365  }
1366  friend probe operator>=(probe const & p1, double p2) { return p1 >= probe(p1.ctx(), p2); }
1367  friend probe operator>=(double p1, probe const & p2) { return probe(p2.ctx(), p1) >= p2; }
1368  friend probe operator<(probe const & p1, probe const & p2) {
1369  check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1370  }
1371  friend probe operator<(probe const & p1, double p2) { return p1 < probe(p1.ctx(), p2); }
1372  friend probe operator<(double p1, probe const & p2) { return probe(p2.ctx(), p1) < p2; }
1373  friend probe operator>(probe const & p1, probe const & p2) {
1374  check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1375  }
1376  friend probe operator>(probe const & p1, double p2) { return p1 > probe(p1.ctx(), p2); }
1377  friend probe operator>(double p1, probe const & p2) { return probe(p2.ctx(), p1) > p2; }
1378  friend probe operator==(probe const & p1, probe const & p2) {
1379  check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1380  }
1381  friend probe operator==(probe const & p1, double p2) { return p1 == probe(p1.ctx(), p2); }
1382  friend probe operator==(double p1, probe const & p2) { return probe(p2.ctx(), p1) == p2; }
1383  friend probe operator&&(probe const & p1, probe const & p2) {
1384  check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1385  }
1386  friend probe operator||(probe const & p1, probe const & p2) {
1387  check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1388  }
1389  friend probe operator!(probe const & p) {
1390  Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
1391  }
1392  };
1393 
1394  inline tactic fail_if(probe const & p) {
1395  Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
1396  p.check_error();
1397  return tactic(p.ctx(), r);
1398  }
1399  inline tactic when(probe const & p, tactic const & t) {
1400  check_context(p, t);
1401  Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
1402  t.check_error();
1403  return tactic(t.ctx(), r);
1404  }
1405  inline tactic cond(probe const & p, tactic const & t1, tactic const & t2) {
1406  check_context(p, t1); check_context(p, t2);
1407  Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
1408  t1.check_error();
1409  return tactic(t1.ctx(), r);
1410  }
1411 
1412  inline symbol context::str_symbol(char const * s) { Z3_symbol r = Z3_mk_string_symbol(m_ctx, s); check_error(); return symbol(*this, r); }
1413  inline symbol context::int_symbol(int n) { Z3_symbol r = Z3_mk_int_symbol(m_ctx, n); check_error(); return symbol(*this, r); }
1414 
1415  inline sort context::bool_sort() { Z3_sort s = Z3_mk_bool_sort(m_ctx); check_error(); return sort(*this, s); }
1416  inline sort context::int_sort() { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }
1417  inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
1418  inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
1419  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); }
1420 
1421  inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
1422  array<Z3_sort> args(arity);
1423  for (unsigned i = 0; i < arity; i++) {
1424  check_context(domain[i], range);
1425  args[i] = domain[i];
1426  }
1427  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
1428  check_error();
1429  return func_decl(*this, f);
1430  }
1431 
1432  inline func_decl context::function(char const * name, unsigned arity, sort const * domain, sort const & range) {
1433  return function(range.ctx().str_symbol(name), arity, domain, range);
1434  }
1435 
1436  inline func_decl context::function(char const * name, sort const & domain, sort const & range) {
1437  check_context(domain, range);
1438  Z3_sort args[1] = { domain };
1439  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
1440  check_error();
1441  return func_decl(*this, f);
1442  }
1443 
1444  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & range) {
1445  check_context(d1, range); check_context(d2, range);
1446  Z3_sort args[2] = { d1, d2 };
1447  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
1448  check_error();
1449  return func_decl(*this, f);
1450  }
1451 
1452  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
1453  check_context(d1, range); check_context(d2, range); check_context(d3, range);
1454  Z3_sort args[3] = { d1, d2, d3 };
1455  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
1456  check_error();
1457  return func_decl(*this, f);
1458  }
1459 
1460  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
1461  check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range);
1462  Z3_sort args[4] = { d1, d2, d3, d4 };
1463  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
1464  check_error();
1465  return func_decl(*this, f);
1466  }
1467 
1468  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) {
1469  check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range); check_context(d5, range);
1470  Z3_sort args[5] = { d1, d2, d3, d4, d5 };
1471  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
1472  check_error();
1473  return func_decl(*this, f);
1474  }
1475 
1476  inline expr context::constant(symbol const & name, sort const & s) {
1477  Z3_ast r = Z3_mk_const(m_ctx, name, s);
1478  check_error();
1479  return expr(*this, r);
1480  }
1481  inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); }
1482  inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); }
1483  inline expr context::int_const(char const * name) { return constant(name, int_sort()); }
1484  inline expr context::real_const(char const * name) { return constant(name, real_sort()); }
1485  inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); }
1486 
1487  inline expr context::bool_val(bool b) { return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }
1488 
1489  inline expr context::int_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
1490  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); }
1491  inline expr context::int_val(__int64 n) { Z3_ast r = Z3_mk_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
1492  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); }
1493  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); }
1494 
1495  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); }
1496  inline expr context::real_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
1497  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); }
1498  inline expr context::real_val(__int64 n) { Z3_ast r = Z3_mk_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
1499  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); }
1500  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); }
1501 
1502  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); }
1503  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); }
1504  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); }
1505  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); }
1506  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); }
1507 
1508  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); }
1509 
1510  inline expr func_decl::operator()(unsigned n, expr const * args) const {
1511  array<Z3_ast> _args(n);
1512  for (unsigned i = 0; i < n; i++) {
1513  check_context(*this, args[i]);
1514  _args[i] = args[i];
1515  }
1516  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
1517  check_error();
1518  return expr(ctx(), r);
1519 
1520  }
1521  inline expr func_decl::operator()(expr const & a) const {
1522  check_context(*this, a);
1523  Z3_ast args[1] = { a };
1524  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
1525  ctx().check_error();
1526  return expr(ctx(), r);
1527  }
1528  inline expr func_decl::operator()(int a) const {
1529  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
1530  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
1531  ctx().check_error();
1532  return expr(ctx(), r);
1533  }
1534  inline expr func_decl::operator()(expr const & a1, expr const & a2) const {
1535  check_context(*this, a1); check_context(*this, a2);
1536  Z3_ast args[2] = { a1, a2 };
1537  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
1538  ctx().check_error();
1539  return expr(ctx(), r);
1540  }
1541  inline expr func_decl::operator()(expr const & a1, int a2) const {
1542  check_context(*this, a1);
1543  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
1544  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
1545  ctx().check_error();
1546  return expr(ctx(), r);
1547  }
1548  inline expr func_decl::operator()(int a1, expr const & a2) const {
1549  check_context(*this, a2);
1550  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
1551  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
1552  ctx().check_error();
1553  return expr(ctx(), r);
1554  }
1555  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3) const {
1556  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
1557  Z3_ast args[3] = { a1, a2, a3 };
1558  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
1559  ctx().check_error();
1560  return expr(ctx(), r);
1561  }
1562  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const {
1563  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
1564  Z3_ast args[4] = { a1, a2, a3, a4 };
1565  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
1566  ctx().check_error();
1567  return expr(ctx(), r);
1568  }
1569  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const {
1570  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
1571  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
1572  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
1573  ctx().check_error();
1574  return expr(ctx(), r);
1575  }
1576 
1577  inline expr to_real(expr const & a) { Z3_ast r = Z3_mk_int2real(a.ctx(), a); a.check_error(); return expr(a.ctx(), r); }
1578 
1579  inline func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
1580  return range.ctx().function(name, arity, domain, range);
1581  }
1582  inline func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range) {
1583  return range.ctx().function(name, arity, domain, range);
1584  }
1585  inline func_decl function(char const * name, sort const & domain, sort const & range) {
1586  return range.ctx().function(name, domain, range);
1587  }
1588  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range) {
1589  return range.ctx().function(name, d1, d2, range);
1590  }
1591  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
1592  return range.ctx().function(name, d1, d2, d3, range);
1593  }
1594  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
1595  return range.ctx().function(name, d1, d2, d3, d4, range);
1596  }
1597  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) {
1598  return range.ctx().function(name, d1, d2, d3, d4, d5, range);
1599  }
1600 
1601  inline expr select(expr const & a, expr const & i) {
1602  check_context(a, i);
1603  Z3_ast r = Z3_mk_select(a.ctx(), a, i);
1604  a.check_error();
1605  return expr(a.ctx(), r);
1606  }
1607  inline expr select(expr const & a, int i) { return select(a, a.ctx().num_val(i, a.get_sort().array_domain())); }
1608  inline expr store(expr const & a, expr const & i, expr const & v) {
1609  check_context(a, i); check_context(a, v);
1610  Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
1611  a.check_error();
1612  return expr(a.ctx(), r);
1613  }
1614  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); }
1615  inline expr store(expr const & a, expr i, int v) { return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
1616  inline expr store(expr const & a, int i, int v) {
1617  return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
1618  }
1619  inline expr const_array(sort const & d, expr const & v) {
1620  check_context(d, v);
1621  Z3_ast r = Z3_mk_const_array(d.ctx(), d, v);
1622  d.check_error();
1623  return expr(d.ctx(), r);
1624  }
1625 
1626 
1627 };
1628 
1629 template class z3::ast_vector_tpl<z3::ast>;
1630 template class z3::ast_vector_tpl<z3::expr>;
1631 template class z3::ast_vector_tpl<z3::sort>;
1632 template class z3::ast_vector_tpl<z3::func_decl>;
1633 
1636 
1637 #endif
1638