Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules 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  template<typename T> class ast_vector_tpl;
71 
72  inline void set_param(char const * param, char const * value) { Z3_global_param_set(param, value); }
73  inline void set_param(char const * param, bool value) { Z3_global_param_set(param, value ? "true" : "false"); }
74  inline void set_param(char const * param, int value) { std::ostringstream oss; oss << value; Z3_global_param_set(param, oss.str().c_str()); }
76 
80  class exception {
81  std::string m_msg;
82  public:
83  exception(char const * msg):m_msg(msg) {}
84  char const * msg() const { return m_msg.c_str(); }
85  friend std::ostream & operator<<(std::ostream & out, exception const & e) { out << e.msg(); return out; }
86  };
87 
88 
89 
93  class config {
94  Z3_config m_cfg;
95  config(config const & s);
96  config & operator=(config const & s);
97  public:
98  config() { m_cfg = Z3_mk_config(); }
99  ~config() { Z3_del_config(m_cfg); }
100  operator Z3_config() const { return m_cfg; }
104  void set(char const * param, char const * value) { Z3_set_param_value(m_cfg, param, value); }
108  void set(char const * param, bool value) { Z3_set_param_value(m_cfg, param, value ? "true" : "false"); }
112  void set(char const * param, int value) {
113  std::ostringstream oss;
114  oss << value;
115  Z3_set_param_value(m_cfg, param, oss.str().c_str());
116  }
117  };
118 
122  class context {
123  Z3_context m_ctx;
124  static void error_handler(Z3_context c, Z3_error_code e) { /* do nothing */ }
125  void init(config & c) {
126  m_ctx = Z3_mk_context_rc(c);
127  Z3_set_error_handler(m_ctx, error_handler);
129  }
130  context(context const & s);
131  context & operator=(context const & s);
132  public:
133  context() { config c; init(c); }
134  context(config & c) { init(c); }
135  ~context() { Z3_del_context(m_ctx); }
136  operator Z3_context() const { return m_ctx; }
137 
141  void check_error() const {
142  Z3_error_code e = Z3_get_error_code(m_ctx);
143  if (e != Z3_OK)
144  throw exception(Z3_get_error_msg_ex(m_ctx, e));
145  }
146 
150  void set(char const * param, char const * value) { Z3_update_param_value(m_ctx, param, value); }
154  void set(char const * param, bool value) { Z3_update_param_value(m_ctx, param, value ? "true" : "false"); }
158  void set(char const * param, int value) {
159  std::ostringstream oss;
160  oss << value;
161  Z3_update_param_value(m_ctx, param, oss.str().c_str());
162  }
163 
168  void interrupt() { Z3_interrupt(m_ctx); }
169 
173  symbol str_symbol(char const * s);
177  symbol int_symbol(int n);
181  sort bool_sort();
185  sort int_sort();
189  sort real_sort();
193  sort bv_sort(unsigned sz);
199  sort array_sort(sort d, sort r);
205  sort enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts);
206 
207  func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range);
208  func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range);
209  func_decl function(symbol const& name, sort_vector const& domain, sort const& range);
210  func_decl function(char const * name, sort_vector const& domain, sort const& range);
211  func_decl function(char const * name, sort const & domain, sort const & range);
212  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range);
213  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range);
214  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range);
215  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range);
216 
217  expr constant(symbol const & name, sort const & s);
218  expr constant(char const * name, sort const & s);
219  expr bool_const(char const * name);
220  expr int_const(char const * name);
221  expr real_const(char const * name);
222  expr bv_const(char const * name, unsigned sz);
223 
224  expr bool_val(bool b);
225 
226  expr int_val(int n);
227  expr int_val(unsigned n);
228  expr int_val(__int64 n);
229  expr int_val(__uint64 n);
230  expr int_val(char const * n);
231 
232  expr real_val(int n, int d);
233  expr real_val(int n);
234  expr real_val(unsigned n);
235  expr real_val(__int64 n);
237  expr real_val(char const * n);
238 
239  expr bv_val(int n, unsigned sz);
240  expr bv_val(unsigned n, unsigned sz);
241  expr bv_val(__int64 n, unsigned sz);
242  expr bv_val(__uint64 n, unsigned sz);
243  expr bv_val(char const * n, unsigned sz);
244 
245  expr num_val(int n, sort const & s);
246  };
247 
248  template<typename T>
249  class array {
250  T * m_array;
251  unsigned m_size;
252  array(array const & s);
253  array & operator=(array const & s);
254  public:
255  array(unsigned sz):m_size(sz) { m_array = new T[sz]; }
256  template<typename T2>
257  array(ast_vector_tpl<T2> const & v);
258  ~array() { delete[] m_array; }
259  unsigned size() const { return m_size; }
260  T & operator[](int i) { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
261  T const & operator[](int i) const { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
262  T const * ptr() const { return m_array; }
263  T * ptr() { return m_array; }
264  };
265 
266  class object {
267  protected:
269  public:
270  object(context & c):m_ctx(&c) {}
271  object(object const & s):m_ctx(s.m_ctx) {}
272  context & ctx() const { return *m_ctx; }
273  void check_error() const { m_ctx->check_error(); }
274  friend void check_context(object const & a, object const & b);
275  };
276  inline void check_context(object const & a, object const & b) { assert(a.m_ctx == b.m_ctx); }
277 
278  class symbol : public object {
279  Z3_symbol m_sym;
280  public:
281  symbol(context & c, Z3_symbol s):object(c), m_sym(s) {}
282  symbol(symbol const & s):object(s), m_sym(s.m_sym) {}
283  symbol & operator=(symbol const & s) { m_ctx = s.m_ctx; m_sym = s.m_sym; return *this; }
284  operator Z3_symbol() const { return m_sym; }
285  Z3_symbol_kind kind() const { return Z3_get_symbol_kind(ctx(), m_sym); }
286  std::string str() const { assert(kind() == Z3_STRING_SYMBOL); return Z3_get_symbol_string(ctx(), m_sym); }
287  int to_int() const { assert(kind() == Z3_INT_SYMBOL); return Z3_get_symbol_int(ctx(), m_sym); }
288  friend std::ostream & operator<<(std::ostream & out, symbol const & s) {
289  if (s.kind() == Z3_INT_SYMBOL)
290  out << "k!" << s.to_int();
291  else
292  out << s.str().c_str();
293  return out;
294  }
295  };
296 
297 
298  class params : public object {
299  Z3_params m_params;
300  public:
301  params(context & c):object(c) { m_params = Z3_mk_params(c); Z3_params_inc_ref(ctx(), m_params); }
302  params(params const & s):object(s), m_params(s.m_params) { Z3_params_inc_ref(ctx(), m_params); }
303  ~params() { Z3_params_dec_ref(ctx(), m_params); }
304  operator Z3_params() const { return m_params; }
305  params & operator=(params const & s) {
306  Z3_params_inc_ref(s.ctx(), s.m_params);
307  Z3_params_dec_ref(ctx(), m_params);
308  m_ctx = s.m_ctx;
309  m_params = s.m_params;
310  return *this;
311  }
312  void set(char const * k, bool b) { Z3_params_set_bool(ctx(), m_params, ctx().str_symbol(k), b); }
313  void set(char const * k, unsigned n) { Z3_params_set_uint(ctx(), m_params, ctx().str_symbol(k), n); }
314  void set(char const * k, double n) { Z3_params_set_double(ctx(), m_params, ctx().str_symbol(k), n); }
315  void set(char const * k, symbol const & s) { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), s); }
316  friend std::ostream & operator<<(std::ostream & out, params const & p) {
317  out << Z3_params_to_string(p.ctx(), p); return out;
318  }
319  };
320 
321  class ast : public object {
322  protected:
324  public:
325  ast(context & c):object(c), m_ast(0) {}
326  ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
327  ast(ast const & s):object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
328  ~ast() { if (m_ast) Z3_dec_ref(*m_ctx, m_ast); }
329  operator Z3_ast() const { return m_ast; }
330  operator bool() const { return m_ast != 0; }
331  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; }
332  Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }
333  unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }
334  friend std::ostream & operator<<(std::ostream & out, ast const & n) {
335  out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
336  }
337 
341  friend bool eq(ast const & a, ast const & b);
342  };
343 
344  inline bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b) != 0; }
345 
346 
350  class sort : public ast {
351  public:
352  sort(context & c):ast(c) {}
353  sort(context & c, Z3_sort s):ast(c, reinterpret_cast<Z3_ast>(s)) {}
354  sort(sort const & s):ast(s) {}
355  operator Z3_sort() const { return reinterpret_cast<Z3_sort>(m_ast); }
359  sort & operator=(sort const & s) { return static_cast<sort&>(ast::operator=(s)); }
363  Z3_sort_kind sort_kind() const { return Z3_get_sort_kind(*m_ctx, *this); }
364 
368  bool is_bool() const { return sort_kind() == Z3_BOOL_SORT; }
372  bool is_int() const { return sort_kind() == Z3_INT_SORT; }
376  bool is_real() const { return sort_kind() == Z3_REAL_SORT; }
380  bool is_arith() const { return is_int() || is_real(); }
384  bool is_bv() const { return sort_kind() == Z3_BV_SORT; }
388  bool is_array() const { return sort_kind() == Z3_ARRAY_SORT; }
392  bool is_datatype() const { return sort_kind() == Z3_DATATYPE_SORT; }
396  bool is_relation() const { return sort_kind() == Z3_RELATION_SORT; }
400  bool is_finite_domain() const { return sort_kind() == Z3_FINITE_DOMAIN_SORT; }
401 
407  unsigned bv_size() const { assert(is_bv()); unsigned r = Z3_get_bv_sort_size(ctx(), *this); check_error(); return r; }
408 
414  sort array_domain() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_domain(ctx(), *this); check_error(); return sort(ctx(), s); }
420  sort array_range() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_range(ctx(), *this); check_error(); return sort(ctx(), s); }
421  };
422 
427  class func_decl : public ast {
428  public:
429  func_decl(context & c):ast(c) {}
430  func_decl(context & c, Z3_func_decl n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
431  func_decl(func_decl const & s):ast(s) {}
432  operator Z3_func_decl() const { return reinterpret_cast<Z3_func_decl>(m_ast); }
433  func_decl & operator=(func_decl const & s) { return static_cast<func_decl&>(ast::operator=(s)); }
434 
435  unsigned arity() const { return Z3_get_arity(ctx(), *this); }
436  sort domain(unsigned i) const { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }
437  sort range() const { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }
438  symbol name() const { Z3_symbol s = Z3_get_decl_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
439  Z3_decl_kind decl_kind() const { return Z3_get_decl_kind(ctx(), *this); }
440 
441  bool is_const() const { return arity() == 0; }
442 
443  expr operator()() const;
444  expr operator()(unsigned n, expr const * args) const;
445  expr operator()(expr_vector const& v) const;
446  expr operator()(expr const & a) const;
447  expr operator()(int a) const;
448  expr operator()(expr const & a1, expr const & a2) const;
449  expr operator()(expr const & a1, int a2) const;
450  expr operator()(int a1, expr const & a2) const;
451  expr operator()(expr const & a1, expr const & a2, expr const & a3) const;
452  expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const;
453  expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const;
454  };
455 
460  class expr : public ast {
461  public:
462  expr(context & c):ast(c) {}
463  expr(context & c, Z3_ast n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
464  expr(expr const & n):ast(n) {}
465  expr & operator=(expr const & n) { return static_cast<expr&>(ast::operator=(n)); }
466 
470  sort get_sort() const { Z3_sort s = Z3_get_sort(*m_ctx, m_ast); check_error(); return sort(*m_ctx, s); }
471 
475  bool is_bool() const { return get_sort().is_bool(); }
479  bool is_int() const { return get_sort().is_int(); }
483  bool is_real() const { return get_sort().is_real(); }
487  bool is_arith() const { return get_sort().is_arith(); }
491  bool is_bv() const { return get_sort().is_bv(); }
495  bool is_array() const { return get_sort().is_array(); }
499  bool is_datatype() const { return get_sort().is_datatype(); }
503  bool is_relation() const { return get_sort().is_relation(); }
512  bool is_finite_domain() const { return get_sort().is_finite_domain(); }
513 
517  bool is_numeral() const { return kind() == Z3_NUMERAL_AST; }
521  bool is_app() const { return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
525  bool is_const() const { return is_app() && num_args() == 0; }
529  bool is_quantifier() const { return kind() == Z3_QUANTIFIER_AST; }
533  bool is_var() const { return kind() == Z3_VAR_AST; }
534 
538  bool is_well_sorted() const { bool r = Z3_is_well_sorted(ctx(), m_ast) != 0; check_error(); return r; }
539 
540  operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
541 
548  func_decl decl() const { Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }
555  unsigned num_args() const { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
563  expr arg(unsigned i) const { Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }
564 
570  expr body() const { assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
571 
577  friend expr operator!(expr const & a) {
578  assert(a.is_bool());
579  Z3_ast r = Z3_mk_not(a.ctx(), a);
580  a.check_error();
581  return expr(a.ctx(), r);
582  }
583 
584 
591  friend expr operator&&(expr const & a, expr const & b) {
592  check_context(a, b);
593  assert(a.is_bool() && b.is_bool());
594  Z3_ast args[2] = { a, b };
595  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
596  a.check_error();
597  return expr(a.ctx(), r);
598  }
599 
600 
607  friend expr operator&&(expr const & a, bool b) { return a && a.ctx().bool_val(b); }
614  friend expr operator&&(bool a, expr const & b) { return b.ctx().bool_val(a) && b; }
615 
622  friend expr operator||(expr const & a, expr const & b) {
623  check_context(a, b);
624  assert(a.is_bool() && b.is_bool());
625  Z3_ast args[2] = { a, b };
626  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
627  a.check_error();
628  return expr(a.ctx(), r);
629  }
636  friend expr operator||(expr const & a, bool b) { return a || a.ctx().bool_val(b); }
643  friend expr operator||(bool a, expr const & b) { return b.ctx().bool_val(a) || b; }
644 
645  friend expr implies(expr const & a, expr const & b) {
646  check_context(a, b);
647  assert(a.is_bool() && b.is_bool());
648  Z3_ast r = Z3_mk_implies(a.ctx(), a, b);
649  a.check_error();
650  return expr(a.ctx(), r);
651  }
652  friend expr implies(expr const & a, bool b);
653  friend expr implies(bool a, expr const & b);
654 
655  friend expr ite(expr const & c, expr const & t, expr const & e);
656 
657  friend expr distinct(expr_vector const& args);
658 
659  friend expr operator==(expr const & a, expr const & b) {
660  check_context(a, b);
661  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
662  a.check_error();
663  return expr(a.ctx(), r);
664  }
665  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()); }
666  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; }
667 
668  friend expr operator!=(expr const & a, expr const & b) {
669  check_context(a, b);
670  Z3_ast args[2] = { a, b };
671  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
672  a.check_error();
673  return expr(a.ctx(), r);
674  }
675  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()); }
676  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; }
677 
678  friend expr operator+(expr const & a, expr const & b) {
679  check_context(a, b);
680  Z3_ast r;
681  if (a.is_arith() && b.is_arith()) {
682  Z3_ast args[2] = { a, b };
683  r = Z3_mk_add(a.ctx(), 2, args);
684  }
685  else if (a.is_bv() && b.is_bv()) {
686  r = Z3_mk_bvadd(a.ctx(), a, b);
687  }
688  else {
689  // operator is not supported by given arguments.
690  assert(false);
691  }
692  a.check_error();
693  return expr(a.ctx(), r);
694  }
695  friend expr operator+(expr const & a, int b) { return a + a.ctx().num_val(b, a.get_sort()); }
696  friend expr operator+(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) + b; }
697 
698  friend expr operator*(expr const & a, expr const & b) {
699  check_context(a, b);
700  Z3_ast r;
701  if (a.is_arith() && b.is_arith()) {
702  Z3_ast args[2] = { a, b };
703  r = Z3_mk_mul(a.ctx(), 2, args);
704  }
705  else if (a.is_bv() && b.is_bv()) {
706  r = Z3_mk_bvmul(a.ctx(), a, b);
707  }
708  else {
709  // operator is not supported by given arguments.
710  assert(false);
711  }
712  a.check_error();
713  return expr(a.ctx(), r);
714  }
715  friend expr operator*(expr const & a, int b) { return a * a.ctx().num_val(b, a.get_sort()); }
716  friend expr operator*(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) * b; }
717 
721  friend expr pw(expr const & a, expr const & b);
722  friend expr pw(expr const & a, int b);
723  friend expr pw(int a, expr const & b);
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  r = Z3_mk_div(a.ctx(), a, b);
730  }
731  else if (a.is_bv() && b.is_bv()) {
732  r = Z3_mk_bvsdiv(a.ctx(), a, b);
733  }
734  else {
735  // operator is not supported by given arguments.
736  assert(false);
737  }
738  a.check_error();
739  return expr(a.ctx(), r);
740  }
741  friend expr operator/(expr const & a, int b) { return a / a.ctx().num_val(b, a.get_sort()); }
742  friend expr operator/(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) / b; }
743 
744  friend expr operator-(expr const & a) {
745  Z3_ast r;
746  if (a.is_arith()) {
747  r = Z3_mk_unary_minus(a.ctx(), a);
748  }
749  else if (a.is_bv()) {
750  r = Z3_mk_bvneg(a.ctx(), a);
751  }
752  else {
753  // operator is not supported by given arguments.
754  assert(false);
755  }
756  a.check_error();
757  return expr(a.ctx(), r);
758  }
759 
760  friend expr operator-(expr const & a, expr const & b) {
761  check_context(a, b);
762  Z3_ast r;
763  if (a.is_arith() && b.is_arith()) {
764  Z3_ast args[2] = { a, b };
765  r = Z3_mk_sub(a.ctx(), 2, args);
766  }
767  else if (a.is_bv() && b.is_bv()) {
768  r = Z3_mk_bvsub(a.ctx(), a, b);
769  }
770  else {
771  // operator is not supported by given arguments.
772  assert(false);
773  }
774  a.check_error();
775  return expr(a.ctx(), r);
776  }
777  friend expr operator-(expr const & a, int b) { return a - a.ctx().num_val(b, a.get_sort()); }
778  friend expr operator-(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) - b; }
779 
780  friend expr operator<=(expr const & a, expr const & b) {
781  check_context(a, b);
782  Z3_ast r;
783  if (a.is_arith() && b.is_arith()) {
784  r = Z3_mk_le(a.ctx(), a, b);
785  }
786  else if (a.is_bv() && b.is_bv()) {
787  r = Z3_mk_bvsle(a.ctx(), a, b);
788  }
789  else {
790  // operator is not supported by given arguments.
791  assert(false);
792  }
793  a.check_error();
794  return expr(a.ctx(), r);
795  }
796  friend expr operator<=(expr const & a, int b) { return a <= a.ctx().num_val(b, a.get_sort()); }
797  friend expr operator<=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) <= b; }
798 
799  friend expr operator>=(expr const & a, expr const & b) {
800  check_context(a, b);
801  Z3_ast r;
802  if (a.is_arith() && b.is_arith()) {
803  r = Z3_mk_ge(a.ctx(), a, b);
804  }
805  else if (a.is_bv() && b.is_bv()) {
806  r = Z3_mk_bvsge(a.ctx(), a, b);
807  }
808  else {
809  // operator is not supported by given arguments.
810  assert(false);
811  }
812  a.check_error();
813  return expr(a.ctx(), r);
814  }
815  friend expr operator>=(expr const & a, int b) { return a >= a.ctx().num_val(b, a.get_sort()); }
816  friend expr operator>=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) >= b; }
817 
818  friend expr operator<(expr const & a, expr const & b) {
819  check_context(a, b);
820  Z3_ast r;
821  if (a.is_arith() && b.is_arith()) {
822  r = Z3_mk_lt(a.ctx(), a, b);
823  }
824  else if (a.is_bv() && b.is_bv()) {
825  r = Z3_mk_bvslt(a.ctx(), a, b);
826  }
827  else {
828  // operator is not supported by given arguments.
829  assert(false);
830  }
831  a.check_error();
832  return expr(a.ctx(), r);
833  }
834  friend expr operator<(expr const & a, int b) { return a < a.ctx().num_val(b, a.get_sort()); }
835  friend expr operator<(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) < b; }
836 
837  friend expr operator>(expr const & a, expr const & b) {
838  check_context(a, b);
839  Z3_ast r;
840  if (a.is_arith() && b.is_arith()) {
841  r = Z3_mk_gt(a.ctx(), a, b);
842  }
843  else if (a.is_bv() && b.is_bv()) {
844  r = Z3_mk_bvsgt(a.ctx(), a, b);
845  }
846  else {
847  // operator is not supported by given arguments.
848  assert(false);
849  }
850  a.check_error();
851  return expr(a.ctx(), r);
852  }
853  friend expr operator>(expr const & a, int b) { return a > a.ctx().num_val(b, a.get_sort()); }
854  friend expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > b; }
855 
856  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); }
857  friend expr operator&(expr const & a, int b) { return a & a.ctx().num_val(b, a.get_sort()); }
858  friend expr operator&(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) & b; }
859 
860  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); }
861  friend expr operator^(expr const & a, int b) { return a ^ a.ctx().num_val(b, a.get_sort()); }
862  friend expr operator^(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) ^ b; }
863 
864  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); }
865  friend expr operator|(expr const & a, int b) { return a | a.ctx().num_val(b, a.get_sort()); }
866  friend expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; }
867 
868  friend expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
869 
873  expr simplify() const { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
877  expr simplify(params const & p) const { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
878 
882  expr substitute(expr_vector const& src, expr_vector const& dst);
883 
887  expr substitute(expr_vector const& dst);
888 
889  };
890 
891  inline expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); }
892  inline expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); }
893 
894  inline expr pw(expr const & a, expr const & b) {
895  assert(a.is_arith() && b.is_arith());
896  check_context(a, b);
897  Z3_ast r = Z3_mk_power(a.ctx(), a, b);
898  a.check_error();
899  return expr(a.ctx(), r);
900  }
901  inline expr pw(expr const & a, int b) { return pw(a, a.ctx().num_val(b, a.get_sort())); }
902  inline expr pw(int a, expr const & b) { return pw(b.ctx().num_val(a, b.get_sort()), b); }
903 
904 
905 
906 
907 
914  inline expr ite(expr const & c, expr const & t, expr const & e) {
915  check_context(c, t); check_context(c, e);
916  assert(c.is_bool());
917  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
918  c.check_error();
919  return expr(c.ctx(), r);
920  }
921 
922 
927  inline expr to_expr(context & c, Z3_ast a) {
928  c.check_error();
929  assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
930  Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
931  Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
933  return expr(c, a);
934  }
935 
936  inline sort to_sort(context & c, Z3_sort s) {
937  c.check_error();
938  return sort(c, s);
939  }
940 
942  c.check_error();
943  return func_decl(c, f);
944  }
945 
949  inline expr ule(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
950  inline expr ule(expr const & a, int b) { return ule(a, a.ctx().num_val(b, a.get_sort())); }
951  inline expr ule(int a, expr const & b) { return ule(b.ctx().num_val(a, b.get_sort()), b); }
955  inline expr ult(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }
956  inline expr ult(expr const & a, int b) { return ult(a, a.ctx().num_val(b, a.get_sort())); }
957  inline expr ult(int a, expr const & b) { return ult(b.ctx().num_val(a, b.get_sort()), b); }
961  inline expr uge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }
962  inline expr uge(expr const & a, int b) { return uge(a, a.ctx().num_val(b, a.get_sort())); }
963  inline expr uge(int a, expr const & b) { return uge(b.ctx().num_val(a, b.get_sort()), b); }
967  inline expr ugt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
968  inline expr ugt(expr const & a, int b) { return ugt(a, a.ctx().num_val(b, a.get_sort())); }
969  inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), b); }
973  inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
974  inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); }
975  inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); }
976 
977  template<typename T> class cast_ast;
978 
979  template<> class cast_ast<ast> {
980  public:
981  ast operator()(context & c, Z3_ast a) { return ast(c, a); }
982  };
983 
984  template<> class cast_ast<expr> {
985  public:
987  assert(Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
988  Z3_get_ast_kind(c, a) == Z3_APP_AST ||
990  Z3_get_ast_kind(c, a) == Z3_VAR_AST);
991  return expr(c, a);
992  }
993  };
994 
995  template<> class cast_ast<sort> {
996  public:
998  assert(Z3_get_ast_kind(c, a) == Z3_SORT_AST);
999  return sort(c, reinterpret_cast<Z3_sort>(a));
1000  }
1001  };
1002 
1003  template<> class cast_ast<func_decl> {
1004  public:
1006  assert(Z3_get_ast_kind(c, a) == Z3_FUNC_DECL_AST);
1007  return func_decl(c, reinterpret_cast<Z3_func_decl>(a));
1008  }
1009  };
1010 
1011  template<typename T>
1012  class ast_vector_tpl : public object {
1013  Z3_ast_vector m_vector;
1014  void init(Z3_ast_vector v) { Z3_ast_vector_inc_ref(ctx(), v); m_vector = v; }
1015  public:
1017  ast_vector_tpl(context & c, Z3_ast_vector v):object(c) { init(v); }
1018  ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
1020  operator Z3_ast_vector() const { return m_vector; }
1021  unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); }
1022  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); }
1023  void push_back(T const & e) { Z3_ast_vector_push(ctx(), m_vector, e); check_error(); }
1024  void resize(unsigned sz) { Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }
1025  T back() const { return operator[](size() - 1); }
1026  void pop_back() { assert(size() > 0); resize(size() - 1); }
1027  bool empty() const { return size() == 0; }
1029  Z3_ast_vector_inc_ref(s.ctx(), s.m_vector);
1030  Z3_ast_vector_dec_ref(ctx(), m_vector);
1031  m_ctx = s.m_ctx;
1032  m_vector = s.m_vector;
1033  return *this;
1034  }
1035  friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
1036  };
1037 
1038  template<typename T>
1039  template<typename T2>
1041  m_array = new T[v.size()];
1042  m_size = v.size();
1043  for (unsigned i = 0; i < m_size; i++) {
1044  m_array[i] = v[i];
1045  }
1046  }
1047 
1048  // Basic functions for creating quantified formulas.
1049  // The C API should be used for creating quantifiers with patterns, weights, many variables, etc.
1050  inline expr forall(expr const & x, expr const & b) {
1051  check_context(x, b);
1052  Z3_app vars[] = {(Z3_app) x};
1053  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1054  }
1055  inline expr forall(expr const & x1, expr const & x2, expr const & b) {
1056  check_context(x1, b); check_context(x2, b);
1057  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1058  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1059  }
1060  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
1061  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1062  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1063  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1064  }
1065  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
1066  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1067  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1068  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1069  }
1070  inline expr forall(expr_vector const & xs, expr const & b) {
1071  array<Z3_app> vars(xs);
1072  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);
1073  }
1074  inline expr exists(expr const & x, expr const & b) {
1075  check_context(x, b);
1076  Z3_app vars[] = {(Z3_app) x};
1077  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1078  }
1079  inline expr exists(expr const & x1, expr const & x2, expr const & b) {
1080  check_context(x1, b); check_context(x2, b);
1081  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1082  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1083  }
1084  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
1085  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1086  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1087  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1088  }
1089  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
1090  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1091  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1092  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1093  }
1094  inline expr exists(expr_vector const & xs, expr const & b) {
1095  array<Z3_app> vars(xs);
1096  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);
1097  }
1098 
1099 
1100  inline expr distinct(expr_vector const& args) {
1101  assert(args.size() > 0);
1102  context& ctx = args[0].ctx();
1103  array<Z3_ast> _args(args);
1104  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
1105  ctx.check_error();
1106  return expr(ctx, r);
1107  }
1108 
1109  class func_entry : public object {
1110  Z3_func_entry m_entry;
1111  void init(Z3_func_entry e) {
1112  m_entry = e;
1113  Z3_func_entry_inc_ref(ctx(), m_entry);
1114  }
1115  public:
1116  func_entry(context & c, Z3_func_entry e):object(c) { init(e); }
1117  func_entry(func_entry const & s):object(s) { init(s.m_entry); }
1119  operator Z3_func_entry() const { return m_entry; }
1121  Z3_func_entry_inc_ref(s.ctx(), s.m_entry);
1122  Z3_func_entry_dec_ref(ctx(), m_entry);
1123  m_ctx = s.m_ctx;
1124  m_entry = s.m_entry;
1125  return *this;
1126  }
1127  expr value() const { Z3_ast r = Z3_func_entry_get_value(ctx(), m_entry); check_error(); return expr(ctx(), r); }
1128  unsigned num_args() const { unsigned r = Z3_func_entry_get_num_args(ctx(), m_entry); check_error(); return r; }
1129  expr arg(unsigned i) const { Z3_ast r = Z3_func_entry_get_arg(ctx(), m_entry, i); check_error(); return expr(ctx(), r); }
1130  };
1131 
1132  class func_interp : public object {
1133  Z3_func_interp m_interp;
1134  void init(Z3_func_interp e) {
1135  m_interp = e;
1136  Z3_func_interp_inc_ref(ctx(), m_interp);
1137  }
1138  public:
1139  func_interp(context & c, Z3_func_interp e):object(c) { init(e); }
1140  func_interp(func_interp const & s):object(s) { init(s.m_interp); }
1142  operator Z3_func_interp() const { return m_interp; }
1144  Z3_func_interp_inc_ref(s.ctx(), s.m_interp);
1145  Z3_func_interp_dec_ref(ctx(), m_interp);
1146  m_ctx = s.m_ctx;
1147  m_interp = s.m_interp;
1148  return *this;
1149  }
1150  expr else_value() const { Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), r); }
1151  unsigned num_entries() const { unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }
1152  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); }
1153  };
1154 
1155  class model : public object {
1156  Z3_model m_model;
1157  void init(Z3_model m) {
1158  m_model = m;
1159  Z3_model_inc_ref(ctx(), m);
1160  }
1161  public:
1162  model(context & c, Z3_model m):object(c) { init(m); }
1163  model(model const & s):object(s) { init(s.m_model); }
1164  ~model() { Z3_model_dec_ref(ctx(), m_model); }
1165  operator Z3_model() const { return m_model; }
1166  model & operator=(model const & s) {
1167  Z3_model_inc_ref(s.ctx(), s.m_model);
1168  Z3_model_dec_ref(ctx(), m_model);
1169  m_ctx = s.m_ctx;
1170  m_model = s.m_model;
1171  return *this;
1172  }
1173 
1174  expr eval(expr const & n, bool model_completion=false) const {
1175  check_context(*this, n);
1176  Z3_ast r;
1177  Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
1178  check_error();
1179  if (status == Z3_FALSE)
1180  throw exception("failed to evaluate expression");
1181  return expr(ctx(), r);
1182  }
1183 
1184  unsigned num_consts() const { return Z3_model_get_num_consts(ctx(), m_model); }
1185  unsigned num_funcs() const { return Z3_model_get_num_funcs(ctx(), m_model); }
1186  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); }
1187  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); }
1188  unsigned size() const { return num_consts() + num_funcs(); }
1189  func_decl operator[](int i) const {
1190  assert(0 <= i);
1191  return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
1192  }
1193 
1195  check_context(*this, c);
1196  Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);
1197  check_error();
1198  return expr(ctx(), r);
1199  }
1201  check_context(*this, f);
1202  Z3_func_interp r = Z3_model_get_func_interp(ctx(), m_model, f);
1203  check_error();
1204  return func_interp(ctx(), r);
1205  }
1206 
1207  friend std::ostream & operator<<(std::ostream & out, model const & m) { out << Z3_model_to_string(m.ctx(), m); return out; }
1208  };
1209 
1210  class stats : public object {
1211  Z3_stats m_stats;
1212  void init(Z3_stats e) {
1213  m_stats = e;
1214  Z3_stats_inc_ref(ctx(), m_stats);
1215  }
1216  public:
1217  stats(context & c):object(c), m_stats(0) {}
1218  stats(context & c, Z3_stats e):object(c) { init(e); }
1219  stats(stats const & s):object(s) { init(s.m_stats); }
1220  ~stats() { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); }
1221  operator Z3_stats() const { return m_stats; }
1222  stats & operator=(stats const & s) {
1223  Z3_stats_inc_ref(s.ctx(), s.m_stats);
1224  if (m_stats) Z3_stats_dec_ref(ctx(), m_stats);
1225  m_ctx = s.m_ctx;
1226  m_stats = s.m_stats;
1227  return *this;
1228  }
1229  unsigned size() const { return Z3_stats_size(ctx(), m_stats); }
1230  std::string key(unsigned i) const { Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; }
1231  bool is_uint(unsigned i) const { Z3_bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r != 0; }
1232  bool is_double(unsigned i) const { Z3_bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r != 0; }
1233  unsigned uint_value(unsigned i) const { unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; }
1234  double double_value(unsigned i) const { double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
1235  friend std::ostream & operator<<(std::ostream & out, stats const & s) { out << Z3_stats_to_string(s.ctx(), s); return out; }
1236  };
1237 
1240  };
1241 
1242  inline std::ostream & operator<<(std::ostream & out, check_result r) {
1243  if (r == unsat) out << "unsat";
1244  else if (r == sat) out << "sat";
1245  else out << "unknown";
1246  return out;
1247  }
1248 
1250  if (l == Z3_L_TRUE) return sat;
1251  else if (l == Z3_L_FALSE) return unsat;
1252  return unknown;
1253  }
1254 
1255  class solver : public object {
1256  Z3_solver m_solver;
1257  void init(Z3_solver s) {
1258  m_solver = s;
1259  Z3_solver_inc_ref(ctx(), s);
1260  }
1261  public:
1262  solver(context & c):object(c) { init(Z3_mk_solver(c)); }
1263  solver(context & c, Z3_solver s):object(c) { init(s); }
1264  solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); }
1265  solver(solver const & s):object(s) { init(s.m_solver); }
1266  ~solver() { Z3_solver_dec_ref(ctx(), m_solver); }
1267  operator Z3_solver() const { return m_solver; }
1268  solver & operator=(solver const & s) {
1269  Z3_solver_inc_ref(s.ctx(), s.m_solver);
1270  Z3_solver_dec_ref(ctx(), m_solver);
1271  m_ctx = s.m_ctx;
1272  m_solver = s.m_solver;
1273  return *this;
1274  }
1275  void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
1276  void push() { Z3_solver_push(ctx(), m_solver); check_error(); }
1277  void pop(unsigned n = 1) { Z3_solver_pop(ctx(), m_solver, n); check_error(); }
1278  void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); }
1279  void add(expr const & e) { assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); }
1280  void add(expr const & e, expr const & p) {
1281  assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
1282  Z3_solver_assert_and_track(ctx(), m_solver, e, p);
1283  check_error();
1284  }
1285  void add(expr const & e, char const * p) {
1286  add(e, ctx().bool_const(p));
1287  }
1289  check_result check(unsigned n, expr * const assumptions) {
1290  array<Z3_ast> _assumptions(n);
1291  for (unsigned i = 0; i < n; i++) {
1292  check_context(*this, assumptions[i]);
1293  _assumptions[i] = assumptions[i];
1294  }
1295  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
1296  check_error();
1297  return to_check_result(r);
1298  }
1299  check_result check(expr_vector assumptions) {
1300  unsigned n = assumptions.size();
1301  array<Z3_ast> _assumptions(n);
1302  for (unsigned i = 0; i < n; i++) {
1303  check_context(*this, assumptions[i]);
1304  _assumptions[i] = assumptions[i];
1305  }
1306  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
1307  check_error();
1308  return to_check_result(r);
1309  }
1310  model get_model() const { Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }
1311  std::string reason_unknown() const { Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }
1312  stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }
1313  expr_vector unsat_core() const { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
1314  expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
1315  expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
1316  friend std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
1317  };
1318 
1319  class goal : public object {
1320  Z3_goal m_goal;
1321  void init(Z3_goal s) {
1322  m_goal = s;
1323  Z3_goal_inc_ref(ctx(), s);
1324  }
1325  public:
1326  goal(context & c, bool models=true, bool unsat_cores=false, bool proofs=false):object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); }
1327  goal(context & c, Z3_goal s):object(c) { init(s); }
1328  goal(goal const & s):object(s) { init(s.m_goal); }
1329  ~goal() { Z3_goal_dec_ref(ctx(), m_goal); }
1330  operator Z3_goal() const { return m_goal; }
1331  goal & operator=(goal const & s) {
1332  Z3_goal_inc_ref(s.ctx(), s.m_goal);
1333  Z3_goal_dec_ref(ctx(), m_goal);
1334  m_ctx = s.m_ctx;
1335  m_goal = s.m_goal;
1336  return *this;
1337  }
1338  void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
1339  unsigned size() const { return Z3_goal_size(ctx(), m_goal); }
1340  expr operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
1341  Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); }
1342  bool inconsistent() const { return Z3_goal_inconsistent(ctx(), m_goal) != 0; }
1343  unsigned depth() const { return Z3_goal_depth(ctx(), m_goal); }
1344  void reset() { Z3_goal_reset(ctx(), m_goal); }
1345  unsigned num_exprs() const { return Z3_goal_num_exprs(ctx(), m_goal); }
1346  bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal) != 0; }
1347  bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal) != 0; }
1348  expr as_expr() const {
1349  unsigned n = size();
1350  if (n == 0)
1351  return ctx().bool_val(true);
1352  else if (n == 1)
1353  return operator[](0);
1354  else {
1355  array<Z3_ast> args(n);
1356  for (unsigned i = 0; i < n; i++)
1357  args[i] = operator[](i);
1358  return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
1359  }
1360  }
1361  friend std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; }
1362  };
1363 
1364  class apply_result : public object {
1365  Z3_apply_result m_apply_result;
1366  void init(Z3_apply_result s) {
1367  m_apply_result = s;
1369  }
1370  public:
1371  apply_result(context & c, Z3_apply_result s):object(c) { init(s); }
1372  apply_result(apply_result const & s):object(s) { init(s.m_apply_result); }
1373  ~apply_result() { Z3_apply_result_dec_ref(ctx(), m_apply_result); }
1374  operator Z3_apply_result() const { return m_apply_result; }
1376  Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result);
1377  Z3_apply_result_dec_ref(ctx(), m_apply_result);
1378  m_ctx = s.m_ctx;
1379  m_apply_result = s.m_apply_result;
1380  return *this;
1381  }
1382  unsigned size() const { return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }
1383  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); }
1384  model convert_model(model const & m, unsigned i = 0) const {
1385  check_context(*this, m);
1386  Z3_model new_m = Z3_apply_result_convert_model(ctx(), m_apply_result, i, m);
1387  check_error();
1388  return model(ctx(), new_m);
1389  }
1390  friend std::ostream & operator<<(std::ostream & out, apply_result const & r) { out << Z3_apply_result_to_string(r.ctx(), r); return out; }
1391  };
1392 
1393  class tactic : public object {
1394  Z3_tactic m_tactic;
1395  void init(Z3_tactic s) {
1396  m_tactic = s;
1397  Z3_tactic_inc_ref(ctx(), s);
1398  }
1399  public:
1400  tactic(context & c, char const * name):object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); }
1401  tactic(context & c, Z3_tactic s):object(c) { init(s); }
1402  tactic(tactic const & s):object(s) { init(s.m_tactic); }
1403  ~tactic() { Z3_tactic_dec_ref(ctx(), m_tactic); }
1404  operator Z3_tactic() const { return m_tactic; }
1405  tactic & operator=(tactic const & s) {
1406  Z3_tactic_inc_ref(s.ctx(), s.m_tactic);
1407  Z3_tactic_dec_ref(ctx(), m_tactic);
1408  m_ctx = s.m_ctx;
1409  m_tactic = s.m_tactic;
1410  return *this;
1411  }
1412  solver mk_solver() const { Z3_solver r = Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error(); return solver(ctx(), r); }
1413  apply_result apply(goal const & g) const {
1414  check_context(*this, g);
1415  Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g);
1416  check_error();
1417  return apply_result(ctx(), r);
1418  }
1419  apply_result operator()(goal const & g) const {
1420  return apply(g);
1421  }
1422  std::string help() const { char const * r = Z3_tactic_get_help(ctx(), m_tactic); check_error(); return r; }
1423  friend tactic operator&(tactic const & t1, tactic const & t2) {
1424  check_context(t1, t2);
1425  Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
1426  t1.check_error();
1427  return tactic(t1.ctx(), r);
1428  }
1429  friend tactic operator|(tactic const & t1, tactic const & t2) {
1430  check_context(t1, t2);
1431  Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
1432  t1.check_error();
1433  return tactic(t1.ctx(), r);
1434  }
1435  friend tactic repeat(tactic const & t, unsigned max);
1436  friend tactic with(tactic const & t, params const & p);
1437  friend tactic try_for(tactic const & t, unsigned ms);
1438  };
1439 
1440  inline tactic repeat(tactic const & t, unsigned max=UINT_MAX) {
1441  Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
1442  t.check_error();
1443  return tactic(t.ctx(), r);
1444  }
1445 
1446  inline tactic with(tactic const & t, params const & p) {
1447  Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
1448  t.check_error();
1449  return tactic(t.ctx(), r);
1450  }
1451  inline tactic try_for(tactic const & t, unsigned ms) {
1452  Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
1453  t.check_error();
1454  return tactic(t.ctx(), r);
1455  }
1456 
1457 
1458  class probe : public object {
1459  Z3_probe m_probe;
1460  void init(Z3_probe s) {
1461  m_probe = s;
1462  Z3_probe_inc_ref(ctx(), s);
1463  }
1464  public:
1465  probe(context & c, char const * name):object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); }
1466  probe(context & c, double val):object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); }
1467  probe(context & c, Z3_probe s):object(c) { init(s); }
1468  probe(probe const & s):object(s) { init(s.m_probe); }
1469  ~probe() { Z3_probe_dec_ref(ctx(), m_probe); }
1470  operator Z3_probe() const { return m_probe; }
1471  probe & operator=(probe const & s) {
1472  Z3_probe_inc_ref(s.ctx(), s.m_probe);
1473  Z3_probe_dec_ref(ctx(), m_probe);
1474  m_ctx = s.m_ctx;
1475  m_probe = s.m_probe;
1476  return *this;
1477  }
1478  double apply(goal const & g) const { double r = Z3_probe_apply(ctx(), m_probe, g); check_error(); return r; }
1479  double operator()(goal const & g) const { return apply(g); }
1480  friend probe operator<=(probe const & p1, probe const & p2) {
1481  check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1482  }
1483  friend probe operator<=(probe const & p1, double p2) { return p1 <= probe(p1.ctx(), p2); }
1484  friend probe operator<=(double p1, probe const & p2) { return probe(p2.ctx(), p1) <= p2; }
1485  friend probe operator>=(probe const & p1, probe const & p2) {
1486  check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1487  }
1488  friend probe operator>=(probe const & p1, double p2) { return p1 >= probe(p1.ctx(), p2); }
1489  friend probe operator>=(double p1, probe const & p2) { return probe(p2.ctx(), p1) >= p2; }
1490  friend probe operator<(probe const & p1, probe const & p2) {
1491  check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1492  }
1493  friend probe operator<(probe const & p1, double p2) { return p1 < probe(p1.ctx(), p2); }
1494  friend probe operator<(double p1, probe const & p2) { return probe(p2.ctx(), p1) < p2; }
1495  friend probe operator>(probe const & p1, probe const & p2) {
1496  check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1497  }
1498  friend probe operator>(probe const & p1, double p2) { return p1 > probe(p1.ctx(), p2); }
1499  friend probe operator>(double p1, probe const & p2) { return probe(p2.ctx(), p1) > p2; }
1500  friend probe operator==(probe const & p1, probe const & p2) {
1501  check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1502  }
1503  friend probe operator==(probe const & p1, double p2) { return p1 == probe(p1.ctx(), p2); }
1504  friend probe operator==(double p1, probe const & p2) { return probe(p2.ctx(), p1) == p2; }
1505  friend probe operator&&(probe const & p1, probe const & p2) {
1506  check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1507  }
1508  friend probe operator||(probe const & p1, probe const & p2) {
1509  check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1510  }
1511  friend probe operator!(probe const & p) {
1512  Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
1513  }
1514  };
1515 
1516  inline tactic fail_if(probe const & p) {
1517  Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
1518  p.check_error();
1519  return tactic(p.ctx(), r);
1520  }
1521  inline tactic when(probe const & p, tactic const & t) {
1522  check_context(p, t);
1523  Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
1524  t.check_error();
1525  return tactic(t.ctx(), r);
1526  }
1527  inline tactic cond(probe const & p, tactic const & t1, tactic const & t2) {
1528  check_context(p, t1); check_context(p, t2);
1529  Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
1530  t1.check_error();
1531  return tactic(t1.ctx(), r);
1532  }
1533 
1534  inline symbol context::str_symbol(char const * s) { Z3_symbol r = Z3_mk_string_symbol(m_ctx, s); check_error(); return symbol(*this, r); }
1535  inline symbol context::int_symbol(int n) { Z3_symbol r = Z3_mk_int_symbol(m_ctx, n); check_error(); return symbol(*this, r); }
1536 
1537  inline sort context::bool_sort() { Z3_sort s = Z3_mk_bool_sort(m_ctx); check_error(); return sort(*this, s); }
1538  inline sort context::int_sort() { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }
1539  inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
1540  inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
1541  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); }
1542  inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
1543  array<Z3_symbol> _enum_names(n);
1544  for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
1545  array<Z3_func_decl> _cs(n);
1546  array<Z3_func_decl> _ts(n);
1547  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
1548  sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
1549  check_error();
1550  for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
1551  return s;
1552  }
1553 
1554  inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
1555  array<Z3_sort> args(arity);
1556  for (unsigned i = 0; i < arity; i++) {
1557  check_context(domain[i], range);
1558  args[i] = domain[i];
1559  }
1560  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
1561  check_error();
1562  return func_decl(*this, f);
1563  }
1564 
1565  inline func_decl context::function(char const * name, unsigned arity, sort const * domain, sort const & range) {
1566  return function(range.ctx().str_symbol(name), arity, domain, range);
1567  }
1568 
1569  inline func_decl context::function(symbol const& name, sort_vector const& domain, sort const& range) {
1570  array<Z3_sort> args(domain.size());
1571  for (unsigned i = 0; i < domain.size(); i++) {
1572  check_context(domain[i], range);
1573  args[i] = domain[i];
1574  }
1575  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
1576  check_error();
1577  return func_decl(*this, f);
1578  }
1579 
1580  inline func_decl context::function(char const * name, sort_vector const& domain, sort const& range) {
1581  return function(range.ctx().str_symbol(name), domain, range);
1582  }
1583 
1584 
1585  inline func_decl context::function(char const * name, sort const & domain, sort const & range) {
1586  check_context(domain, range);
1587  Z3_sort args[1] = { domain };
1588  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
1589  check_error();
1590  return func_decl(*this, f);
1591  }
1592 
1593  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & range) {
1594  check_context(d1, range); check_context(d2, range);
1595  Z3_sort args[2] = { d1, d2 };
1596  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
1597  check_error();
1598  return func_decl(*this, f);
1599  }
1600 
1601  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
1602  check_context(d1, range); check_context(d2, range); check_context(d3, range);
1603  Z3_sort args[3] = { d1, d2, d3 };
1604  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
1605  check_error();
1606  return func_decl(*this, f);
1607  }
1608 
1609  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
1610  check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range);
1611  Z3_sort args[4] = { d1, d2, d3, d4 };
1612  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
1613  check_error();
1614  return func_decl(*this, f);
1615  }
1616 
1617  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) {
1618  check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range); check_context(d5, range);
1619  Z3_sort args[5] = { d1, d2, d3, d4, d5 };
1620  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
1621  check_error();
1622  return func_decl(*this, f);
1623  }
1624 
1625  inline expr context::constant(symbol const & name, sort const & s) {
1626  Z3_ast r = Z3_mk_const(m_ctx, name, s);
1627  check_error();
1628  return expr(*this, r);
1629  }
1630  inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); }
1631  inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); }
1632  inline expr context::int_const(char const * name) { return constant(name, int_sort()); }
1633  inline expr context::real_const(char const * name) { return constant(name, real_sort()); }
1634  inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); }
1635 
1636  inline expr context::bool_val(bool b) { return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }
1637 
1638  inline expr context::int_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
1639  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); }
1640  inline expr context::int_val(__int64 n) { Z3_ast r = Z3_mk_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
1641  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); }
1642  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); }
1643 
1644  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); }
1645  inline expr context::real_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
1646  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); }
1647  inline expr context::real_val(__int64 n) { Z3_ast r = Z3_mk_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
1648  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); }
1649  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); }
1650 
1651  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); }
1652  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); }
1653  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); }
1654  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); }
1655  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); }
1656 
1657  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); }
1658 
1659  inline expr func_decl::operator()(unsigned n, expr const * args) const {
1660  array<Z3_ast> _args(n);
1661  for (unsigned i = 0; i < n; i++) {
1662  check_context(*this, args[i]);
1663  _args[i] = args[i];
1664  }
1665  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
1666  check_error();
1667  return expr(ctx(), r);
1668 
1669  }
1670  inline expr func_decl::operator()(expr_vector const& args) const {
1671  array<Z3_ast> _args(args.size());
1672  for (unsigned i = 0; i < args.size(); i++) {
1673  check_context(*this, args[i]);
1674  _args[i] = args[i];
1675  }
1676  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
1677  check_error();
1678  return expr(ctx(), r);
1679  }
1680  inline expr func_decl::operator()() const {
1681  Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
1682  ctx().check_error();
1683  return expr(ctx(), r);
1684  }
1685  inline expr func_decl::operator()(expr const & a) const {
1686  check_context(*this, a);
1687  Z3_ast args[1] = { a };
1688  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
1689  ctx().check_error();
1690  return expr(ctx(), r);
1691  }
1692  inline expr func_decl::operator()(int a) const {
1693  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
1694  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
1695  ctx().check_error();
1696  return expr(ctx(), r);
1697  }
1698  inline expr func_decl::operator()(expr const & a1, expr const & a2) const {
1699  check_context(*this, a1); check_context(*this, a2);
1700  Z3_ast args[2] = { a1, a2 };
1701  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
1702  ctx().check_error();
1703  return expr(ctx(), r);
1704  }
1705  inline expr func_decl::operator()(expr const & a1, int a2) const {
1706  check_context(*this, a1);
1707  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
1708  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
1709  ctx().check_error();
1710  return expr(ctx(), r);
1711  }
1712  inline expr func_decl::operator()(int a1, expr const & a2) const {
1713  check_context(*this, a2);
1714  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
1715  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
1716  ctx().check_error();
1717  return expr(ctx(), r);
1718  }
1719  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3) const {
1720  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
1721  Z3_ast args[3] = { a1, a2, a3 };
1722  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
1723  ctx().check_error();
1724  return expr(ctx(), r);
1725  }
1726  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const {
1727  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
1728  Z3_ast args[4] = { a1, a2, a3, a4 };
1729  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
1730  ctx().check_error();
1731  return expr(ctx(), r);
1732  }
1733  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const {
1734  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
1735  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
1736  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
1737  ctx().check_error();
1738  return expr(ctx(), r);
1739  }
1740 
1741  inline expr to_real(expr const & a) { Z3_ast r = Z3_mk_int2real(a.ctx(), a); a.check_error(); return expr(a.ctx(), r); }
1742 
1743  inline func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
1744  return range.ctx().function(name, arity, domain, range);
1745  }
1746  inline func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range) {
1747  return range.ctx().function(name, arity, domain, range);
1748  }
1749  inline func_decl function(char const * name, sort const & domain, sort const & range) {
1750  return range.ctx().function(name, domain, range);
1751  }
1752  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range) {
1753  return range.ctx().function(name, d1, d2, range);
1754  }
1755  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
1756  return range.ctx().function(name, d1, d2, d3, range);
1757  }
1758  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
1759  return range.ctx().function(name, d1, d2, d3, d4, range);
1760  }
1761  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) {
1762  return range.ctx().function(name, d1, d2, d3, d4, d5, range);
1763  }
1764 
1765  inline expr select(expr const & a, expr const & i) {
1766  check_context(a, i);
1767  Z3_ast r = Z3_mk_select(a.ctx(), a, i);
1768  a.check_error();
1769  return expr(a.ctx(), r);
1770  }
1771  inline expr select(expr const & a, int i) { return select(a, a.ctx().num_val(i, a.get_sort().array_domain())); }
1772  inline expr store(expr const & a, expr const & i, expr const & v) {
1773  check_context(a, i); check_context(a, v);
1774  Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
1775  a.check_error();
1776  return expr(a.ctx(), r);
1777  }
1778  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); }
1779  inline expr store(expr const & a, expr i, int v) { return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
1780  inline expr store(expr const & a, int i, int v) {
1781  return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
1782  }
1783  inline expr const_array(sort const & d, expr const & v) {
1784  check_context(d, v);
1785  Z3_ast r = Z3_mk_const_array(d.ctx(), d, v);
1786  d.check_error();
1787  return expr(d.ctx(), r);
1788  }
1789 
1790  inline expr expr::substitute(expr_vector const& src, expr_vector const& dst) {
1791  assert(src.size() == dst.size());
1792  array<Z3_ast> _src(src.size());
1793  array<Z3_ast> _dst(dst.size());
1794  for (unsigned i = 0; i < src.size(); ++i) {
1795  _src[i] = src[i];
1796  _dst[i] = dst[i];
1797  }
1798  Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
1799  check_error();
1800  return expr(ctx(), r);
1801  }
1802 
1803  inline expr expr::substitute(expr_vector const& dst) {
1804  array<Z3_ast> _dst(dst.size());
1805  for (unsigned i = 0; i < dst.size(); ++i) {
1806  _dst[i] = dst[i];
1807  }
1808  Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
1809  check_error();
1810  return expr(ctx(), r);
1811  }
1812 
1813 
1814 
1815 };
1816 
1819 
1820 #endif
1821 
expr distinct(expr_vector const &args)
Definition: z3++.h:1100
Z3_ast Z3_API Z3_mk_const(__in Z3_context c, __in Z3_symbol s, __in Z3_sort ty)
Declare and create a constant.
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:186
Z3_ast Z3_API Z3_mk_power(__in Z3_context c, __in Z3_ast arg1, __in Z3_ast arg2)
Create an AST node representing arg1^arg2.
friend expr operator|(expr const &a, expr const &b)
Definition: z3++.h:864
System.IntPtr Z3_stats
Definition: Native.cs:29
std::string reason_unknown() const
Definition: z3++.h:1311
Z3_ast Z3_API Z3_mk_forall_const(__in Z3_context c, unsigned weight, unsigned num_bound, __in_ecount(num_bound) Z3_app const bound[], unsigned num_patterns, __in_ecount(num_patterns) Z3_pattern const patterns[], __in Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables...
std::string help() const
Definition: z3++.h:1422
Z3_bool Z3_API Z3_is_well_sorted(__in Z3_context c, __in Z3_ast t)
Return true if the given expression t is well sorted.
sort bool_sort()
Return the Boolean sort.
Definition: z3++.h:1537
friend expr operator+(expr const &a, expr const &b)
Definition: z3++.h:678
void Z3_API Z3_solver_assert_and_track(__in Z3_context c, __in Z3_solver s, __in Z3_ast a, __in Z3_ast p)
Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p...
friend expr pw(expr const &a, expr const &b)
Power operator.
Definition: z3++.h:894
Z3_ast Z3_API Z3_mk_bvule(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Unsigned less than or equal to.
Z3_context Z3_API Z3_mk_context_rc(__in Z3_config c)
Create a context using the given configuration. This function is similar to Z3_mk_context. However, in the context returned by this function, the user is responsible for managing Z3_ast reference counters. Managing reference counters is a burden and error-prone, but allows the user to use the memory more efficiently. The user must invoke Z3_inc_ref for any Z3_ast returned by Z3, and Z3_dec_ref whenever the Z3_ast is not needed anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD.
Z3_ast Z3_API Z3_mk_mul(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].The array args must have num_args el...
Z3_sort Z3_API Z3_mk_bool_sort(__in Z3_context c)
Create the Boolean type.
friend expr operator>=(expr const &a, int b)
Definition: z3++.h:815
Z3_string Z3_API Z3_solver_to_string(__in Z3_context c, __in Z3_solver s)
Convert a solver into a string.
Z3_lbool Z3_API Z3_solver_check(__in Z3_context c, __in Z3_solver s)
Check whether the assertions in a given solver are consistent or not.
void Z3_API Z3_inc_ref(__in Z3_context c, __in Z3_ast a)
Increment the reference counter of the given AST. The context c should have been created using Z3_mk_...
bool is_int() const
Return true if this sort is the Integer sort.
Definition: z3++.h:372
tactic & operator=(tactic const &s)
Definition: z3++.h:1405
probe(context &c, Z3_probe s)
Definition: z3++.h:1467
Z3_ast Z3_API Z3_mk_bvadd(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Standard two's complement addition.
probe & operator=(probe const &s)
Definition: z3++.h:1471
func_decl get_const_decl(unsigned i) const
Definition: z3++.h:1186
void Z3_API Z3_params_dec_ref(__in Z3_context c, __in Z3_params p)
Decrement the reference counter of the given parameter set.
void Z3_API Z3_apply_result_inc_ref(__in Z3_context c, __in Z3_apply_result r)
Increment the reference counter of the given Z3_apply_result object.
friend expr operator>=(expr const &a, expr const &b)
Definition: z3++.h:799
bool is_array() const
Return true if this is a Array expression.
Definition: z3++.h:495
System.IntPtr Z3_probe
Definition: Native.cs:28
Z3_tactic Z3_API Z3_mk_tactic(__in Z3_context c, __in Z3_string name)
Return a tactic associated with the given name. The complete list of tactics may be obtained using th...
friend probe operator<(probe const &p1, double p2)
Definition: z3++.h:1493
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:1534
Z3_string Z3_API Z3_tactic_get_help(__in Z3_context c, __in Z3_tactic t)
Return a string containing a description of parameters accepted by the given tactic.
Z3_sort Z3_API Z3_get_array_sort_range(__in Z3_context c, __in Z3_sort t)
Return the range of the given array sort.
void set(char const *k, symbol const &s)
Definition: z3++.h:315
std::ostream & operator<<(std::ostream &out, check_result r)
Definition: z3++.h:1242
friend expr operator<=(expr const &a, int b)
Definition: z3++.h:796
Z3_sort Z3_API Z3_mk_bv_sort(__in Z3_context c, __in unsigned sz)
Create a bit-vector type of the given size.
friend bool eq(ast const &a, ast const &b)
Return true if the ASTs are structurally identical.
Definition: z3++.h:344
void push()
Definition: z3++.h:1276
System.IntPtr Z3_goal
Definition: Native.cs:25
stats statistics() const
Definition: z3++.h:1312
Z3_symbol Z3_API Z3_get_decl_name(__in Z3_context c, __in Z3_func_decl d)
Return the constant declaration name as a symbol.
tactic cond(probe const &p, tactic const &t1, tactic const &t2)
Definition: z3++.h:1527
expr(context &c)
Definition: z3++.h:462
char const * msg() const
Definition: z3++.h:84
expr bv_val(int n, unsigned sz)
Definition: z3++.h:1651
Z3_probe Z3_API Z3_probe_eq(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned ...
void Z3_API Z3_model_inc_ref(__in Z3_context c, __in Z3_model m)
Increment the reference counter of the given model.
expr value() const
Definition: z3++.h:1127
bool is_real() const
Return true if this is a real expression.
Definition: z3++.h:483
Definition: z3_api.h:1150
func_interp & operator=(func_interp const &s)
Definition: z3++.h:1143
friend expr operator!=(expr const &a, expr const &b)
Definition: z3++.h:668
Z3_ast Z3_API Z3_mk_numeral(__in Z3_context c, __in Z3_string numeral, __in Z3_sort ty)
Create a numeral of a given sort.
Z3_ast Z3_API Z3_substitute_vars(__in Z3_context c, __in Z3_ast a, __in unsigned num_exprs, __in_ecount(num_exprs) Z3_ast const to[])
Substitute the free variables in a with the expressions in to. For every i smaller than num_exprs...
Z3_tactic Z3_API Z3_tactic_fail_if(__in Z3_context c, __in Z3_probe p)
Return a tactic that fails if the probe p evaluates to false.
unsigned Z3_API Z3_get_app_num_args(__in Z3_context c, __in Z3_app a)
Return the number of argument of an application. If t is an constant, then the number of arguments is...
probe(context &c, double val)
Definition: z3++.h:1466
void Z3_API Z3_func_entry_dec_ref(__in Z3_context c, __in Z3_func_entry e)
Decrement the reference counter of the given Z3_func_entry object.
expr select(expr const &a, expr const &i)
Definition: z3++.h:1765
Z3_ast Z3_API Z3_mk_bvor(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Bitwise or.
func_entry & operator=(func_entry const &s)
Definition: z3++.h:1120
void set(char const *param, char const *value)
Set global parameter param with string value.
Definition: z3++.h:104
Z3_sort Z3_API Z3_mk_enumeration_sort(__in Z3_context c, __in Z3_symbol name, __in unsigned n, __in_ecount(n) Z3_symbol const enum_names[], __out_ecount(n) Z3_func_decl enum_consts[], __out_ecount(n) Z3_func_decl enum_testers[])
Create a enumeration sort.
Z3_ast Z3_API Z3_model_get_const_interp(__in Z3_context c, __in Z3_model m, __in Z3_func_decl a)
Return the interpretation (i.e., assignment) of constant a in the model m. Return NULL...
tactic when(probe const &p, tactic const &t)
Definition: z3++.h:1521
config()
Definition: z3++.h:98
friend std::ostream & operator<<(std::ostream &out, params const &p)
Definition: z3++.h:316
void set(char const *k, double n)
Definition: z3++.h:314
Z3_func_decl Z3_API Z3_model_get_func_decl(__in Z3_context c, __in Z3_model m, __in unsigned i)
Return the declaration of the i-th function in the given model.
void Z3_API Z3_solver_dec_ref(__in Z3_context c, __in Z3_solver s)
Decrement the reference counter of the given solver.
void Z3_API Z3_goal_inc_ref(__in Z3_context c, __in Z3_goal g)
Increment the reference counter of the given goal.
friend expr operator/(expr const &a, expr const &b)
Definition: z3++.h:725
void set(char const *param, char const *value)
Update global parameter param with string value.
Definition: z3++.h:150
array(unsigned sz)
Definition: z3++.h:255
System.IntPtr Z3_tactic
Definition: Native.cs:26
A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort.
Definition: z3++.h:350
~solver()
Definition: z3++.h:1266
expr simplify() const
Return a simplified version of this expression.
Definition: z3++.h:873
unsigned bv_size() const
Return the size of this Bit-vector sort.
Definition: z3++.h:407
Z3_apply_result Z3_API Z3_tactic_apply(__in Z3_context c, __in Z3_tactic t, __in Z3_goal g)
Apply tactic t to the goal g.
bool is_bv() const
Return true if this sort is a Bit-vector sort.
Definition: z3++.h:384
Z3_ast Z3_API Z3_func_entry_get_value(__in Z3_context c, __in Z3_func_entry e)
Return the value of this point.
func_decl(context &c)
Definition: z3++.h:429
int to_int() const
Definition: z3++.h:287
friend expr operator^(expr const &a, expr const &b)
Definition: z3++.h:860
~array()
Definition: z3++.h:258
Z3_goal_prec Z3_API Z3_goal_precision(__in Z3_context c, __in Z3_goal g)
Return the "precision" of the given goal. Goals can be transformed using over and under approximation...
Z3_model Z3_API Z3_apply_result_convert_model(__in Z3_context c, __in Z3_apply_result r, __in unsigned i, __in Z3_model m)
Convert a model for the subgoal Z3_apply_result_get_subgoal(c, r, i) into a model for the original go...
friend std::ostream & operator<<(std::ostream &out, ast const &n)
Definition: z3++.h:334
sort bv_sort(unsigned sz)
Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz.
Definition: z3++.h:1540
void interrupt()
Interrupt the current procedure being executed by any object managed by this context. This is a soft interruption: there is no guarantee the object will actualy stop.
Definition: z3++.h:168
bool is_double(unsigned i) const
Definition: z3++.h:1232
expr udiv(expr const &a, expr const &b)
unsigned division operator for bitvectors.
Definition: z3++.h:973
apply_result operator()(goal const &g) const
Definition: z3++.h:1419
void Z3_API Z3_params_inc_ref(__in Z3_context c, __in Z3_params p)
Increment the reference counter of the given parameter set.
solver mk_solver() const
Definition: z3++.h:1412
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1221
Z3_symbol Z3_API Z3_mk_string_symbol(__in Z3_context c, __in Z3_string s)
Create a Z3 symbol using a C string.
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1148
goal(context &c, Z3_goal s)
Definition: z3++.h:1327
void push_back(T const &e)
Definition: z3++.h:1023
Z3_sort Z3_API Z3_mk_real_sort(__in Z3_context c)
Create the real type.
expr eval(expr const &n, bool model_completion=false) const
Definition: z3++.h:1174
model(context &c, Z3_model m)
Definition: z3++.h:1162
Z3_ast_kind kind() const
Definition: z3++.h:332
sort array_sort(sort d, sort r)
Return an array sort for arrays from d to r.
Definition: z3++.h:1541
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:1625
friend probe operator>(double p1, probe const &p2)
Definition: z3++.h:1499
System.IntPtr Z3_ast
Definition: Native.cs:13
int Z3_bool
Z3 Boolean type. It is just an alias for int.
Definition: z3_api.h:102
Z3_bool Z3_API Z3_goal_inconsistent(__in Z3_context c, __in Z3_goal g)
Return true if the given goal contains the formula false.
Z3_sort Z3_API Z3_get_range(__in Z3_context c, __in Z3_func_decl d)
Return the range of the given declaration.
func_decl operator[](int i) const
Definition: z3++.h:1189
System.IntPtr Z3_func_entry
Definition: Native.cs:34
friend probe operator>=(probe const &p1, double p2)
Definition: z3++.h:1488
friend expr operator/(expr const &a, int b)
Definition: z3++.h:741
friend expr operator||(bool a, expr const &b)
Return an expression representing a or b. The C++ Boolean value a is automatically converted into a Z...
Definition: z3++.h:643
tactic(tactic const &s)
Definition: z3++.h:1402
Z3_ast Z3_API Z3_mk_unsigned_int(__in Z3_context c, __in unsigned v, __in Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
friend expr operator||(expr const &a, expr const &b)
Return an expression representing a or b.
Definition: z3++.h:622
Z3_probe Z3_API Z3_probe_gt(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than the value retur...
~probe()
Definition: z3++.h:1469
bool is_datatype() const
Return true if this is a Datatype expression.
Definition: z3++.h:499
Z3_ast Z3_API Z3_goal_formula(__in Z3_context c, __in Z3_goal g, __in unsigned idx)
Return a formula from the given goal.
~tactic()
Definition: z3++.h:1403
sort operator()(context &c, Z3_ast a)
Definition: z3++.h:997
void Z3_API Z3_stats_inc_ref(__in Z3_context c, __in Z3_stats s)
Increment the reference counter of the given statistics object.
Z3_ast Z3_API Z3_mk_sub(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing args[0] - ... - args[num_args - 1].The array args must have num_args ...
friend probe operator||(probe const &p1, probe const &p2)
Definition: z3++.h:1508
friend expr operator*(int a, expr const &b)
Definition: z3++.h:716
Z3_ast Z3_API Z3_substitute(__in Z3_context c, __in Z3_ast a, __in unsigned num_exprs, __in_ecount(num_exprs) Z3_ast const from[], __in_ecount(num_exprs) Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs. The result is the new AST. The arrays from and to must have size num_exprs. For every i smaller than num_exprs, we must have that sort of from[i] must be equal to sort of to[i].
Z3_sort Z3_API Z3_mk_array_sort(__in Z3_context c, __in Z3_sort domain, __in Z3_sort range)
Create an array type.
Exception used to sign API usage errors.
Definition: z3++.h:80
unsigned uint_value(unsigned i) const
Definition: z3++.h:1233
Z3_bool Z3_API Z3_is_eq_ast(__in Z3_context c, __in Z3_ast t1, Z3_ast t2)
compare terms.
void Z3_API Z3_params_set_symbol(__in Z3_context c, __in Z3_params p, __in Z3_symbol k, __in Z3_symbol v)
Add a symbol parameter k with value v to the parameter set p.
A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort ...
Definition: z3++.h:460
void reset_params()
Definition: z3++.h:75
#define __uint64
Definition: z3_api.h:59
expr & operator=(expr const &n)
Definition: z3++.h:465
void Z3_API Z3_model_dec_ref(__in Z3_context c, __in Z3_model m)
Decrement the reference counter of the given model.
unsigned num_exprs() const
Definition: z3++.h:1345
Z3_ast Z3_API Z3_mk_gt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create greater than.
bool is_uint(unsigned i) const
Definition: z3++.h:1231
expr ule(expr const &a, expr const &b)
unsigned less than or equal to operator for bitvectors.
Definition: z3++.h:949
Z3_ast Z3_API Z3_mk_bvsdiv(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed division.
expr_vector unsat_core() const
Definition: z3++.h:1313
void Z3_API Z3_global_param_set(__in Z3_string param_id, __in Z3_string param_value)
Set a global (or module) parameter. This setting is shared by all Z3 contexts.
Z3_func_interp Z3_API Z3_model_get_func_interp(__in Z3_context c, __in Z3_model m, __in Z3_func_decl f)
Return the interpretation of the function f in the model m. Return NULL, if the model does not assign...
Z3_ast Z3_API Z3_mk_bvslt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed less than.
Z3_model Z3_API Z3_solver_get_model(__in Z3_context c, __in Z3_solver s)
Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.
Definition: z3++.h:1239
void Z3_API Z3_set_ast_print_mode(__in Z3_context c, __in Z3_ast_print_mode mode)
Select mode for the format used for pretty-printing AST nodes.
void set(char const *param, int value)
Update global parameter param with Integer value.
Definition: z3++.h:158
Z3_string Z3_API Z3_stats_to_string(__in Z3_context c, __in Z3_stats s)
Convert a statistics into a string.
unsigned num_entries() const
Definition: z3++.h:1151
unsigned arity() const
Definition: z3++.h:435
Z3_string Z3_API Z3_apply_result_to_string(__in Z3_context c, __in Z3_apply_result r)
Convert the Z3_apply_result object returned by Z3_tactic_apply into a string.
void Z3_API Z3_goal_reset(__in Z3_context c, __in Z3_goal g)
Erase all formulas from the given goal.
Z3_ast Z3_API Z3_mk_true(__in Z3_context c)
Create an AST node representing true.
bool is_finite_domain() const
Return true if this sort is a Finite domain sort.
Definition: z3++.h:400
System.IntPtr Z3_sort
Definition: Native.cs:15
friend probe operator>(probe const &p1, double p2)
Definition: z3++.h:1498
void Z3_API Z3_apply_result_dec_ref(__in Z3_context c, __in Z3_apply_result r)
Decrement the reference counter of the given Z3_apply_result object.
func_decl operator()(context &c, Z3_ast a)
Definition: z3++.h:1005
ast_vector_tpl(ast_vector_tpl const &s)
Definition: z3++.h:1018
ast_vector_tpl< func_decl > func_decl_vector
Definition: z3++.h:70
stats(context &c)
Definition: z3++.h:1217
Z3_tactic Z3_API Z3_tactic_repeat(__in Z3_context c, __in Z3_tactic t, unsigned max)
Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of...
Z3_ast_kind Z3_API Z3_get_ast_kind(__in Z3_context c, __in Z3_ast a)
Return the kind of the given AST.
void Z3_API Z3_goal_assert(__in Z3_context c, __in Z3_goal g, __in Z3_ast a)
Add a new formula a to the given goal.
expr pw(expr const &a, expr const &b)
Definition: z3++.h:894
friend std::ostream & operator<<(std::ostream &out, goal const &g)
Definition: z3++.h:1361
friend probe operator>=(probe const &p1, probe const &p2)
Definition: z3++.h:1485
expr(context &c, Z3_ast n)
Definition: z3++.h:463
~goal()
Definition: z3++.h:1329
friend expr operator^(expr const &a, int b)
Definition: z3++.h:861
expr operator[](int i) const
Definition: z3++.h:1340
bool empty() const
Definition: z3++.h:1027
friend expr operator-(expr const &a, expr const &b)
Definition: z3++.h:760
Z3_bool Z3_API Z3_stats_is_double(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return Z3_TRUE if the given statistical data is a double.
friend expr operator-(expr const &a)
Definition: z3++.h:744
friend expr distinct(expr_vector const &args)
Definition: z3++.h:1100
check_result check(unsigned n, expr *const assumptions)
Definition: z3++.h:1289
Z3_goal Z3_API Z3_apply_result_get_subgoal(__in Z3_context c, __in Z3_apply_result r, __in unsigned i)
Return one of the subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
check_result check(expr_vector assumptions)
Definition: z3++.h:1299
friend expr operator*(expr const &a, int b)
Definition: z3++.h:715
friend expr operator&(expr const &a, int b)
Definition: z3++.h:857
friend expr operator*(expr const &a, expr const &b)
Definition: z3++.h:698
probe(context &c, char const *name)
Definition: z3++.h:1465
friend std::ostream & operator<<(std::ostream &out, solver const &s)
Definition: z3++.h:1316
Z3_decl_kind Z3_API Z3_get_decl_kind(__in Z3_context c, __in Z3_func_decl d)
Return declaration kind corresponding to declaration.
~stats()
Definition: z3++.h:1220
Z3_tactic Z3_API Z3_tactic_try_for(__in Z3_context c, __in Z3_tactic t, __in unsigned ms)
Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms mil...
friend expr operator<=(expr const &a, expr const &b)
Definition: z3++.h:780
Z3_ast Z3_API Z3_get_quantifier_body(__in Z3_context c, __in Z3_ast a)
Return body of quantifier.
expr get_const_interp(func_decl c) const
Definition: z3++.h:1194
void Z3_API Z3_solver_inc_ref(__in Z3_context c, __in Z3_solver s)
Increment the reference counter of the given solver.
A Context manages all other Z3 objects, global configuration options, etc.
Definition: z3++.h:122
Definition: z3++.h:321
Z3 C++ namespace.
Definition: z3++.h:45
Z3_tactic Z3_API Z3_tactic_using_params(__in Z3_context c, __in Z3_tactic t, __in Z3_params p)
Return a tactic that applies t using the given set of parameters.
Z3_ast Z3_API Z3_mk_ge(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create greater than or equal to.
friend tactic operator|(tactic const &t1, tactic const &t2)
Definition: z3++.h:1429
void Z3_API Z3_dec_ref(__in Z3_context c, __in Z3_ast a)
Decrement the reference counter of the given AST. The context c should have been created using Z3_mk_...
Z3_ast Z3_API Z3_mk_int(__in Z3_context c, __in int v, __in Z3_sort ty)
Create a numeral of an int, bit-vector, or finite-domain sort.
expr simplify(params const &p) const
Return a simplified version of this expression. The parameter p is a set of parameters for the Z3 sim...
Definition: z3++.h:877
friend expr operator&(int a, expr const &b)
Definition: z3++.h:858
unsigned size() const
Definition: z3++.h:1021
Z3_tactic Z3_API Z3_tactic_and_then(__in Z3_context c, __in Z3_tactic t1, __in Z3_tactic t2)
Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1...
Z3_ast Z3_API Z3_mk_bvult(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Unsigned less than.
solver(context &c, Z3_solver s)
Definition: z3++.h:1263
Z3 global configuration object.
Definition: z3++.h:93
solver & operator=(solver const &s)
Definition: z3++.h:1268
void set(char const *param, int value)
Set global parameter param with integer value.
Definition: z3++.h:112
Z3_ast Z3_API Z3_simplify(__in Z3_context c, __in Z3_ast a)
Interface to simplifier.
System.IntPtr Z3_config
Definition: Native.cs:11
expr substitute(expr_vector const &src, expr_vector const &dst)
Apply substitution. Replace src expressions by dst.
Definition: z3++.h:1790
ast(context &c, Z3_ast n)
Definition: z3++.h:326
void Z3_API Z3_params_set_uint(__in Z3_context c, __in Z3_params p, __in Z3_symbol k, __in unsigned v)
Add a unsigned parameter k with value v to the parameter set p.
friend std::ostream & operator<<(std::ostream &out, apply_result const &r)
Definition: z3++.h:1390
Z3_ast_vector Z3_API Z3_solver_get_unsat_core(__in Z3_context c, __in Z3_solver s)
Retrieve the unsat core for the last Z3_solver_check_assumptions The unsat core is a subset of the as...
bool is_finite_domain() const
Return true if this is a Finite-domain expression.
Definition: z3++.h:512
expr proof() const
Definition: z3++.h:1315
expr bv_const(char const *name, unsigned sz)
Definition: z3++.h:1634
Z3_func_entry Z3_API Z3_func_interp_get_entry(__in Z3_context c, __in Z3_func_interp f, unsigned i)
Return a "point" of the given function intepretation. It represents the value of f in a particular po...
T back() const
Definition: z3++.h:1025
tactic(context &c, char const *name)
Definition: z3++.h:1400
Z3_solver Z3_API Z3_mk_solver_for_logic(__in Z3_context c, __in Z3_symbol logic)
Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unkn...
std::string str() const
Definition: z3++.h:286
Z3_bool Z3_API Z3_model_eval(__in Z3_context c, __in Z3_model m, __in Z3_ast t, __in Z3_bool model_completion, __out Z3_ast *v)
Evaluate the AST node t in the given model. Return Z3_TRUE if succeeded, and store the result in v...
void Z3_API Z3_probe_inc_ref(__in Z3_context c, __in Z3_probe p)
Increment the reference counter of the given probe.
Z3_ast Z3_API Z3_mk_bvmul(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Standard two's complement multiplication.
tactic with(tactic const &t, params const &p)
Definition: z3++.h:1446
System.IntPtr Z3_func_decl
Definition: Native.cs:16
void reset()
Definition: z3++.h:1278
friend expr operator<=(int a, expr const &b)
Definition: z3++.h:797
void resize(unsigned sz)
Definition: z3++.h:1024
Z3_probe Z3_API Z3_probe_not(__in Z3_context x, __in Z3_probe p)
Return a probe that evaluates to "true" when p does not evaluate to true.
unsigned Z3_API Z3_stats_size(__in Z3_context c, __in Z3_stats s)
Return the number of statistical data in s.
void Z3_API Z3_solver_assert(__in Z3_context c, __in Z3_solver s, __in Z3_ast a)
Assert a constraint into the solver.
~config()
Definition: z3++.h:99
Z3_symbol_kind Z3_API Z3_get_symbol_kind(__in Z3_context c, __in Z3_symbol s)
Return Z3_INT_SYMBOL if the symbol was constructed using Z3_mk_int_symbol, and Z3_STRING_SYMBOL if th...
unsigned Z3_API Z3_func_interp_get_num_entries(__in Z3_context c, __in Z3_func_interp f)
Return the number of entries in the given function interpretation.
sort array_domain() const
Return the domain of this Array sort.
Definition: z3++.h:414
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:212
BEGIN_MLAPI_EXCLUDE Z3_string Z3_API Z3_get_error_msg_ex(__in Z3_context c, __in Z3_error_code err)
Return a string describing the given error code.
func_entry(context &c, Z3_func_entry e)
Definition: z3++.h:1116
Z3_string Z3_API Z3_goal_to_string(__in Z3_context c, __in Z3_goal g)
Convert a goal into a string.
bool is_var() const
Return true if this expression is a variable.
Definition: z3++.h:533
ast_vector_tpl(context &c)
Definition: z3++.h:1016
void add(expr const &e, char const *p)
Definition: z3++.h:1285
func_decl to_func_decl(context &c, Z3_func_decl f)
Definition: z3++.h:941
unsigned depth() const
Definition: z3++.h:1343
ast_vector_tpl(context &c, Z3_ast_vector v)
Definition: z3++.h:1017
Z3_ast Z3_API Z3_mk_bvnot(__in Z3_context c, __in Z3_ast t1)
Bitwise negation.
context & ctx() const
Definition: z3++.h:272
sort array_range() const
Return the range of this Array sort.
Definition: z3++.h:420
double Z3_API Z3_stats_get_double_value(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return the double value of the given statistical data.
Z3_ast Z3_API Z3_mk_false(__in Z3_context c)
Create an AST node representing false.
expr(expr const &n)
Definition: z3++.h:464
Z3_string Z3_API Z3_params_to_string(__in Z3_context c, __in Z3_params p)
Convert a parameter set into a string. This function is mainly used for printing the contents of a pa...
void Z3_API Z3_ast_vector_push(__in Z3_context c, __in Z3_ast_vector v, __in Z3_ast a)
Add the AST a in the end of the AST vector v. The size of v is increased by one.
Definition: z3++.h:1109
void Z3_API Z3_solver_push(__in Z3_context c, __in Z3_solver s)
Create a backtracking point.
unsigned Z3_API Z3_goal_num_exprs(__in Z3_context c, __in Z3_goal g)
Return the number of formulas, subformulas and terms in the given goal.
bool is_const() const
Definition: z3++.h:441
check_result check()
Definition: z3++.h:1288
unsigned size() const
Definition: z3++.h:1382
Z3_ast Z3_API Z3_mk_ite(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2, __in Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
Z3_sort Z3_API Z3_get_array_sort_domain(__in Z3_context c, __in Z3_sort t)
Return the domain of the given array sort.
void Z3_API Z3_goal_dec_ref(__in Z3_context c, __in Z3_goal g)
Decrement the reference counter of the given goal.
func_decl get_func_decl(unsigned i) const
Definition: z3++.h:1187
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:1554
expr operator()(context &c, Z3_ast a)
Definition: z3++.h:986
friend probe operator!(probe const &p)
Definition: z3++.h:1511
expr as_expr() const
Definition: z3++.h:1348
bool is_numeral() const
Return true if this expression is a numeral.
Definition: z3++.h:517
Z3_tactic Z3_API Z3_tactic_cond(__in Z3_context c, __in Z3_probe p, __in Z3_tactic t1, __in Z3_tactic t2)
Return a tactic that applies t1 to a given goal if the probe p evaluates to true, and t2 if p evaluat...
unsigned Z3_API Z3_model_get_num_funcs(__in Z3_context c, __in Z3_model m)
Return the number of function interpretations in the given model.
exception(char const *msg)
Definition: z3++.h:83
solver(solver const &s)
Definition: z3++.h:1265
Z3_ast Z3_API Z3_mk_implies(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create an AST node representing t1 implies t2.
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:135
friend expr operator!=(expr const &a, int b)
Definition: z3++.h:675
Z3_ast Z3_API Z3_mk_bvugt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Unsigned greater than.
Z3_string Z3_API Z3_stats_get_key(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return the key (a string) for a particular statistical data.
#define __int64
Definition: z3_api.h:55
void Z3_API Z3_func_interp_inc_ref(__in Z3_context c, __in Z3_func_interp f)
Increment the reference counter of the given Z3_func_interp object.
expr real_val(int n, int d)
Definition: z3++.h:1644
ast_vector_tpl< sort > sort_vector
Definition: z3++.h:69
Z3_ast Z3_API Z3_mk_and(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].The array args must have num_arg...
unsigned Z3_API Z3_get_arity(__in Z3_context c, __in Z3_func_decl d)
Alias for Z3_get_domain_size.
int Z3_API Z3_get_symbol_int(__in Z3_context c, __in Z3_symbol s)
Return the symbol int value.
void check_error() const
Definition: z3++.h:273
Z3_ast Z3_API Z3_mk_select(__in Z3_context c, __in Z3_ast a, __in Z3_ast i)
Array read. The argument a is the array and i is the index of the array that gets read...
Z3_ast Z3_API Z3_mk_bvsle(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed less than or equal to.
func_interp(func_interp const &s)
Definition: z3++.h:1140
Z3_decl_kind decl_kind() const
Definition: z3++.h:439
model & operator=(model const &s)
Definition: z3++.h:1166
friend expr operator-(int a, expr const &b)
Definition: z3++.h:778
Z3_ast Z3_API Z3_mk_lt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create less than.
Z3_func_decl Z3_API Z3_model_get_const_decl(__in Z3_context c, __in Z3_model m, __in unsigned i)
Return the i-th constant in the given model.
unsigned Z3_API Z3_get_ast_hash(__in Z3_context c, __in Z3_ast a)
Return a hash code for the given AST.
friend expr operator==(expr const &a, expr const &b)
Definition: z3++.h:659
void set(char const *param, bool value)
Set global parameter param with Boolean value.
Definition: z3++.h:108
func_entry entry(unsigned i) const
Definition: z3++.h:1152
void add(expr const &e)
Definition: z3++.h:1279
bool is_relation() const
Return true if this is a Relation expression.
Definition: z3++.h:503
bool is_bool() const
Return true if this sort is the Boolean sort.
Definition: z3++.h:368
expr ugt(expr const &a, expr const &b)
unsigned greater than operator for bitvectors.
Definition: z3++.h:967
goal & operator=(goal const &s)
Definition: z3++.h:1331
Z3_ast Z3_API Z3_mk_bvsub(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Standard two's complement subtraction.
~params()
Definition: z3++.h:303
expr const_array(sort const &d, expr const &v)
Definition: z3++.h:1783
stats(stats const &s)
Definition: z3++.h:1219
T const * ptr() const
Definition: z3++.h:262
void Z3_API Z3_params_set_double(__in Z3_context c, __in Z3_params p, __in Z3_symbol k, __in double v)
Add a double parameter k with value v to the parameter set p.
Z3_ast Z3_API Z3_mk_int2real(__in Z3_context c, __in Z3_ast t1)
Coerce an integer to a real.
Z3_string Z3_API Z3_ast_to_string(__in Z3_context c, __in Z3_ast a)
Convert the given AST node into a string.
friend std::ostream & operator<<(std::ostream &out, model const &m)
Definition: z3++.h:1207
Z3_ast Z3_API Z3_solver_get_proof(__in Z3_context c, __in Z3_solver s)
Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.
~func_entry()
Definition: z3++.h:1118
goal operator[](int i) const
Definition: z3++.h:1383
Z3_probe Z3_API Z3_probe_const(__in Z3_context x, __in double val)
Return a probe that always evaluates to val.
friend expr operator<(expr const &a, int b)
Definition: z3++.h:834
friend probe operator==(probe const &p1, double p2)
Definition: z3++.h:1503
Z3_sort Z3_API Z3_mk_int_sort(__in Z3_context c)
Create the integer type.
void reset()
Definition: z3++.h:1344
T * ptr()
Definition: z3++.h:263
friend expr operator<(int a, expr const &b)
Definition: z3++.h:835
params(params const &s)
Definition: z3++.h:302
Z3_ast Z3_API Z3_mk_bvand(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Bitwise and.
void set_param(char const *param, char const *value)
Definition: z3++.h:72
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
void Z3_API Z3_del_context(__in Z3_context c)
Delete the given logical context.
void Z3_API Z3_set_error_handler(__in Z3_context c, __in Z3_error_handler h)
Register a Z3 error handler.
Z3_bool Z3_API Z3_goal_is_decided_sat(__in Z3_context c, __in Z3_goal g)
Return true if the goal is empty, and it is precise or the product of a under approximation.
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:548
Z3_ast Z3_API Z3_mk_bvuge(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Unsigned greater than or equal to.
friend probe operator<=(probe const &p1, probe const &p2)
Definition: z3++.h:1480
friend expr operator&&(expr const &a, expr const &b)
Return an expression representing a and b.
Definition: z3++.h:591
expr int_const(char const *name)
Definition: z3++.h:1632
friend expr operator&(expr const &a, expr const &b)
Definition: z3++.h:856
friend std::ostream & operator<<(std::ostream &out, exception const &e)
Definition: z3++.h:85
expr arg(unsigned i) const
Definition: z3++.h:1129
void Z3_API Z3_solver_set_params(__in Z3_context c, __in Z3_solver s, __in Z3_params p)
Set the given solver using the given parameters.
symbol(symbol const &s)
Definition: z3++.h:282
Z3_stats Z3_API Z3_solver_get_statistics(__in Z3_context c, __in Z3_solver s)
Return statistics for the given solver.
unsigned num_args() const
Return the number of arguments in this application. This method assumes the expression is an applicat...
Definition: z3++.h:555
Z3_symbol_kind
The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See Z3_...
Definition: z3_api.h:150
sort(context &c)
Definition: z3++.h:352
friend expr operator&&(expr const &a, bool b)
Return an expression representing a and b. The C++ Boolean value b is automatically converted into a ...
Definition: z3++.h:607
Z3_probe Z3_API Z3_probe_ge(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than or equal to the...
unsigned Z3_API Z3_model_get_num_consts(__in Z3_context c, __in Z3_model m)
Return the number of constants assigned by the given model.
Z3_ast Z3_API Z3_mk_not(__in Z3_context c, __in Z3_ast a)
Create an AST node representing not(a).
Z3_ast Z3_API Z3_mk_bvsge(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed greater than or equal to.
goal(context &c, bool models=true, bool unsat_cores=false, bool proofs=false)
Definition: z3++.h:1326
void Z3_API Z3_del_config(__in Z3_config c)
Delete the given configuration object.
System.IntPtr Z3_apply_result
Definition: Native.cs:32
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:521
friend tactic operator&(tactic const &t1, tactic const &t2)
Definition: z3++.h:1423
object(context &c)
Definition: z3++.h:270
friend expr operator>(expr const &a, expr const &b)
Definition: z3++.h:837
unsigned size() const
Definition: z3++.h:1339
Z3_bool Z3_API Z3_stats_is_uint(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return Z3_TRUE if the given statistical data is a unsigned integer.
ast(context &c)
Definition: z3++.h:325
Z3_ast Z3_API Z3_mk_div(__in Z3_context c, __in Z3_ast arg1, __in Z3_ast arg2)
Create an AST node representing arg1 div arg2.The arguments must either both have int type or both ha...
Z3_symbol_kind kind() const
Definition: z3++.h:285
object(object const &s)
Definition: z3++.h:271
Z3_ast Z3_API Z3_mk_bvneg(__in Z3_context c, __in Z3_ast t1)
Standard two's complement unary minus.
Z3_ast Z3_API Z3_mk_unary_minus(__in Z3_context c, __in Z3_ast arg)
Create an AST node representing -arg.The arguments must have int or real type.
Z3_sort Z3_API Z3_get_sort(__in Z3_context c, __in Z3_ast a)
Return the sort of an AST node.
friend tactic with(tactic const &t, params const &p)
Definition: z3++.h:1446
Z3_ast Z3_API Z3_func_entry_get_arg(__in Z3_context c, __in Z3_func_entry e, __in unsigned i)
Return an argument of a Z3_func_entry object.
friend expr operator!=(int a, expr const &b)
Definition: z3++.h:676
Z3_string Z3_API Z3_model_to_string(__in Z3_context c, __in Z3_model m)
Convert the given model into a string.
expr real_const(char const *name)
Definition: z3++.h:1633
friend probe operator<=(double p1, probe const &p2)
Definition: z3++.h:1484
friend expr operator/(int a, expr const &b)
Definition: z3++.h:742
friend expr operator>(int a, expr const &b)
Definition: z3++.h:854
func_interp get_func_interp(func_decl f) const
Definition: z3++.h:1200
void Z3_API Z3_func_entry_inc_ref(__in Z3_context c, __in Z3_func_entry e)
Increment the reference counter of the given Z3_func_entry object.
friend probe operator==(probe const &p1, probe const &p2)
Definition: z3++.h:1500
Z3_func_decl Z3_API Z3_get_app_decl(__in Z3_context c, __in Z3_app a)
Return the declaration of a constant or function application.
friend probe operator>=(double p1, probe const &p2)
Definition: z3++.h:1489
void Z3_API Z3_solver_reset(__in Z3_context c, __in Z3_solver s)
Remove all assertions from the solver.
Z3_solver Z3_API Z3_mk_solver(__in Z3_context c)
Create a new (incremental) solver. This solver also uses a set of builtin tactics for handling the fi...
Z3_sort_kind sort_kind() const
Return the internal sort kind.
Definition: z3++.h:363
bool is_arith() const
Return true if this sort is the Integer or Real sort.
Definition: z3++.h:380
System.IntPtr Z3_solver
Definition: Native.cs:24
unsigned Z3_API Z3_goal_size(__in Z3_context c, __in Z3_goal g)
Return the number of formulas in the given goal.
Z3_ast Z3_API Z3_func_interp_get_else(__in Z3_context c, __in Z3_func_interp f)
Return the 'else' value of the given function interpretation.
Z3_probe Z3_API Z3_probe_or(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when p1 or p2 evaluates to true.
Z3_ast Z3_API Z3_mk_bvsgt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed greater than.
model convert_model(model const &m, unsigned i=0) const
Definition: z3++.h:1384
bool is_well_sorted() const
Return true if this expression is well sorted (aka type correct).
Definition: z3++.h:538
unsigned Z3_API Z3_ast_vector_size(__in Z3_context c, __in Z3_ast_vector v)
Return the size of the given AST vector.
Z3_sort Z3_API Z3_get_domain(__in Z3_context c, __in Z3_func_decl d, __in unsigned i)
Return the sort of the i-th parameter of the given function declaration.
Z3_config Z3_API Z3_mk_config(void)
Create a configuration object for the Z3 context object.
void Z3_API Z3_tactic_dec_ref(__in Z3_context c, __in Z3_tactic g)
Decrement the reference counter of the given tactic.
Z3_bool Z3_API Z3_goal_is_decided_unsat(__in Z3_context c, __in Z3_goal g)
Return true if the goal contains false, and it is precise or the product of an over approximation...
symbol & operator=(symbol const &s)
Definition: z3++.h:283
~model()
Definition: z3++.h:1164
sort real_sort()
Return the Real sort.
Definition: z3++.h:1539
System.IntPtr Z3_app
Definition: Native.cs:14
bool inconsistent() const
Definition: z3++.h:1342
bool is_const() const
Return true if this expression is a constant (i.e., an application with 0 arguments).
Definition: z3++.h:525
expr arg(unsigned i) const
Return the i-th argument of this application. This method assumes the expression is an application...
Definition: z3++.h:563
Z3_ast Z3_API Z3_mk_distinct(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).The distinct construct is us...
expr num_val(int n, sort const &s)
Definition: z3++.h:1657
Z3_ast Z3_API Z3_mk_bvudiv(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Unsigned division.
Z3_ast Z3_API Z3_mk_or(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].The array args must have num_args ...
bool eq(ast const &a, ast const &b)
Definition: z3++.h:344
unsigned num_consts() const
Definition: z3++.h:1184
symbol int_symbol(int n)
Create a Z3 symbol based on the given integer.
Definition: z3++.h:1535
Z3_ast Z3_API Z3_mk_exists_const(__in Z3_context c, unsigned weight, unsigned num_bound, __in_ecount(num_bound) Z3_app const bound[], unsigned num_patterns, __in_ecount(num_patterns) Z3_pattern const patterns[], __in Z3_ast body)
Similar to Z3_mk_forall_const.
void Z3_API Z3_ast_vector_inc_ref(__in Z3_context c, __in Z3_ast_vector v)
Increment the reference counter of the given AST vector.
friend probe operator>(probe const &p1, probe const &p2)
Definition: z3++.h:1495
void Z3_API Z3_interrupt(__in Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers...
friend probe operator<(double p1, probe const &p2)
Definition: z3++.h:1494
unsigned num_funcs() const
Definition: z3++.h:1185
expr operator()() const
Definition: z3++.h:1680
unsigned Z3_API Z3_func_entry_get_num_args(__in Z3_context c, __in Z3_func_entry e)
Return the number of arguments in a Z3_func_entry object.
friend probe operator==(double p1, probe const &p2)
Definition: z3++.h:1504
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:1249
friend expr operator~(expr const &a)
Definition: z3++.h:868
Z3_tactic Z3_API Z3_tactic_when(__in Z3_context c, __in Z3_probe p, __in Z3_tactic t)
Return a tactic that applies t to a given goal is the probe p evaluates to true. If p evaluates to fa...
friend tactic repeat(tactic const &t, unsigned max)
Definition: z3++.h:1440
friend std::ostream & operator<<(std::ostream &out, ast_vector_tpl const &v)
Definition: z3++.h:1035
Z3_ast Z3_API Z3_ast_vector_get(__in Z3_context c, __in Z3_ast_vector v, __in unsigned i)
Return the AST at position i in the AST vector v.
tactic(context &c, Z3_tactic s)
Definition: z3++.h:1401
void check_context(object const &a, object const &b)
Definition: z3++.h:276
Z3_probe Z3_API Z3_probe_le(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the va...
expr bool_const(char const *name)
Definition: z3++.h:1631
double apply(goal const &g) const
Definition: z3++.h:1478
void Z3_API Z3_func_interp_dec_ref(__in Z3_context c, __in Z3_func_interp f)
Decrement the reference counter of the given Z3_func_interp object.
Z3_solver Z3_API Z3_mk_solver_from_tactic(__in Z3_context c, __in Z3_tactic t)
Create a new solver that is implemented using the given tactic. The solver supports the commands Z3_s...
friend expr ite(expr const &c, expr const &t, expr const &e)
Create the if-then-else expression ite(c, t, e)
Definition: z3++.h:914
System.IntPtr Z3_context
Definition: Native.cs:12
params & operator=(params const &s)
Definition: z3++.h:305
Z3_ast Z3_API Z3_mk_bvxor(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Bitwise exclusive-or.
Z3_string Z3_API Z3_ast_vector_to_string(__in Z3_context c, __in Z3_ast_vector v)
Convert AST vector into a string.
friend std::ostream & operator<<(std::ostream &out, symbol const &s)
Definition: z3++.h:288
Z3_ast_vector Z3_API Z3_solver_get_assertions(__in Z3_context c, __in Z3_solver s)
Return the set of asserted formulas as a goal object.
model(model const &s)
Definition: z3++.h:1163
check_result
Definition: z3++.h:1238
probe(probe const &s)
Definition: z3++.h:1468
friend expr operator>(expr const &a, int b)
Definition: z3++.h:853
friend expr operator<(expr const &a, expr const &b)
Definition: z3++.h:818
friend expr operator!(expr const &a)
Return an expression representing not(a).
Definition: z3++.h:577
Z3_goal_prec precision() const
Definition: z3++.h:1341
solver(context &c)
Definition: z3++.h:1262
Z3_probe Z3_API Z3_probe_lt(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned...
func_decl(context &c, Z3_func_decl n)
Definition: z3++.h:430
ast_vector_tpl< ast > ast_vector
Definition: z3++.h:66
bool is_decided_unsat() const
Definition: z3++.h:1347
System.IntPtr Z3_model
Definition: Native.cs:18
friend probe operator<(probe const &p1, probe const &p2)
Definition: z3++.h:1490
friend expr operator==(expr const &a, int b)
Definition: z3++.h:665
expr_vector assertions() const
Definition: z3++.h:1314
unsigned Z3_API Z3_goal_depth(__in Z3_context c, __in Z3_goal g)
Return the depth of the given goal. It tracks how many transformations were applied to it...
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:470
Z3_ast Z3_API Z3_mk_int64(__in Z3_context c, __in __int64 v, __in Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
friend probe operator&&(probe const &p1, probe const &p2)
Definition: z3++.h:1505
void add(expr const &e, expr const &p)
Definition: z3++.h:1280
expr store(expr const &a, expr const &i, expr const &v)
Definition: z3++.h:1772
void Z3_API Z3_params_set_bool(__in Z3_context c, __in Z3_params p, __in Z3_symbol k, __in Z3_bool v)
Add a Boolean parameter k with value v to the parameter set p.
void set(char const *k, unsigned n)
Definition: z3++.h:313
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
Z3_string Z3_API Z3_get_symbol_string(__in Z3_context c, __in Z3_symbol s)
Return the symbol name.
std::string key(unsigned i) const
Definition: z3++.h:1230
void Z3_API Z3_probe_dec_ref(__in Z3_context c, __in Z3_probe p)
Decrement the reference counter of the given probe.
bool is_relation() const
Return true if this sort is a Relation sort.
Definition: z3++.h:396
Z3_ast m_ast
Definition: z3++.h:323
Z3_ast Z3_API Z3_mk_eq(__in Z3_context c, __in Z3_ast l, __in Z3_ast r)
Create an AST node representing l = r.
void set(char const *k, bool b)
Definition: z3++.h:312
tactic repeat(tactic const &t, unsigned max=UINT_MAX)
Definition: z3++.h:1440
expr bool_val(bool b)
Definition: z3++.h:1636
Z3_ast Z3_API Z3_mk_unsigned_int64(__in Z3_context c, __in unsigned __int64 v, __in Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
~context()
Definition: z3++.h:135
expr ult(expr const &a, expr const &b)
unsigned less than operator for bitvectors.
Definition: z3++.h:955
friend expr operator&&(bool a, expr const &b)
Return an expression representing a and b. The C++ Boolean value a is automatically converted into a ...
Definition: z3++.h:614
Z3_ast Z3_API Z3_mk_store(__in Z3_context c, __in Z3_ast a, __in Z3_ast i, __in Z3_ast v)
Array update.
unsigned Z3_API Z3_get_bv_sort_size(__in Z3_context c, __in Z3_sort t)
Return the size of the given bit-vector sort.
bool is_int() const
Return true if this is an integer expression.
Definition: z3++.h:479
ast_vector_tpl & operator=(ast_vector_tpl const &s)
Definition: z3++.h:1028
apply_result apply(goal const &g) const
Definition: z3++.h:1413
expr int_val(int n)
Definition: z3++.h:1638
bool is_arith() const
Return true if this is an integer or real expression.
Definition: z3++.h:487
void Z3_API Z3_global_param_reset_all(void)
Restore the value of all global (and module) parameters. This command will not affect already created...
model get_model() const
Definition: z3++.h:1310
func_decl(func_decl const &s)
Definition: z3++.h:431
friend expr operator||(expr const &a, bool b)
Return an expression representing a or b. The C++ Boolean value b is automatically converted into a Z...
Definition: z3++.h:636
Z3_sort_kind Z3_API Z3_get_sort_kind(__in Z3_context c, __in Z3_sort t)
Return the sort kind (e.g., array, tuple, int, bool, etc).
expr else_value() const
Definition: z3++.h:1150
tactic fail_if(probe const &p)
Definition: z3++.h:1516
stats(context &c, Z3_stats e)
Definition: z3++.h:1218
expr exists(expr const &x, expr const &b)
Definition: z3++.h:1074
ast operator()(context &c, Z3_ast a)
Definition: z3++.h:981
context(config &c)
Definition: z3++.h:134
void Z3_API Z3_ast_vector_dec_ref(__in Z3_context c, __in Z3_ast_vector v)
Decrement the reference counter of the given AST vector.
bool is_array() const
Return true if this sort is a Array sort.
Definition: z3++.h:388
Z3_ast Z3_API Z3_mk_app(__in Z3_context c, __in Z3_func_decl d, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create a constant or function application.
friend expr operator-(expr const &a, int b)
Definition: z3++.h:777
Z3_func_decl Z3_API Z3_mk_func_decl(__in Z3_context c, __in Z3_symbol s, __in unsigned domain_size, __in_ecount(domain_size) Z3_sort const domain[], __in Z3_sort range)
Declare a constant or function.
expr ite(expr const &c, expr const &t, expr const &e)
Create the if-then-else expression ite(c, t, e)
Definition: z3++.h:914
T const & operator[](int i) const
Definition: z3++.h:261
func_entry(func_entry const &s)
Definition: z3++.h:1117
double double_value(unsigned i) const
Definition: z3++.h:1234
expr body() const
Return the 'body' of this quantifier.
Definition: z3++.h:570
~ast()
Definition: z3++.h:328
void pop_back()
Definition: z3++.h:1026
#define Z3_FALSE
False value. It is just an alias for 0.
Definition: z3_api.h:127
T operator[](int i) const
Definition: z3++.h:1022
ast & operator=(ast const &s)
Definition: z3++.h:331
void Z3_API Z3_stats_dec_ref(__in Z3_context c, __in Z3_stats s)
Decrement the reference counter of the given statistics object.
void Z3_API Z3_update_param_value(__in Z3_context c, __in Z3_string param_id, __in Z3_string param_value)
Set a value of a context parameter.
bool is_bv() const
Return true if this is a Bit-vector expression.
Definition: z3++.h:491
expr forall(expr const &x, expr const &b)
Definition: z3++.h:1050
sort domain(unsigned i) const
Definition: z3++.h:436
bool is_bool() const
Return true if this is a Boolean expression.
Definition: z3++.h:475
sort(context &c, Z3_sort s)
Definition: z3++.h:353
unsigned hash() const
Definition: z3++.h:333
double operator()(goal const &g) const
Definition: z3++.h:1479
bool is_datatype() const
Return true if this sort is a Datatype sort.
Definition: z3++.h:392
void Z3_API Z3_solver_pop(__in Z3_context c, __in Z3_solver s, unsigned n)
Backtrack n backtracking points.
expr to_expr(context &c, Z3_ast a)
Wraps a Z3_ast as an expr object. It also checks for errors. This function allows the user to use the...
Definition: z3++.h:927
friend expr operator+(int a, expr const &b)
Definition: z3++.h:696
symbol(context &c, Z3_symbol s)
Definition: z3++.h:281
solver(context &c, char const *logic)
Definition: z3++.h:1264
tactic try_for(tactic const &t, unsigned ms)
Definition: z3++.h:1451
func_interp(context &c, Z3_func_interp e)
Definition: z3++.h:1139
Z3_params Z3_API Z3_mk_params(__in Z3_context c)
Create a Z3 (empty) parameter set. Starting at Z3 4.0, parameter sets are used to configure many comp...
params(context &c)
Definition: z3++.h:301
friend tactic try_for(tactic const &t, unsigned ms)
Definition: z3++.h:1451
sort range() const
Definition: z3++.h:437
System.IntPtr Z3_ast_vector
Definition: Native.cs:30
Z3_tactic Z3_API Z3_tactic_or_else(__in Z3_context c, __in Z3_tactic t1, __in Z3_tactic t2)
Return a tactic that first applies t1 to a given goal, if it fails then returns the result of t2 appl...
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:68
Z3_error_code Z3_API Z3_get_error_code(__in Z3_context c)
Return the error code for the last API call.
expr uge(expr const &a, expr const &b)
unsigned greater than or equal to operator for bitvectors.
Definition: z3++.h:961
expr implies(expr const &a, bool b)
Definition: z3++.h:891
void set(char const *param, bool value)
Update global parameter param with Boolean value.
Definition: z3++.h:154
void set(params const &p)
Definition: z3++.h:1275
friend expr operator+(expr const &a, int b)
Definition: z3++.h:695
Z3_symbol Z3_API Z3_mk_int_symbol(__in Z3_context c, __in int i)
Create a Z3 symbol using an integer.
sort & operator=(sort const &s)
Return true if this sort and s are equal.
Definition: z3++.h:359
bool is_quantifier() const
Return true if this expression is a quantifier.
Definition: z3++.h:529
friend probe operator<=(probe const &p1, double p2)
Definition: z3++.h:1483
context * m_ctx
Definition: z3++.h:268
Z3_lbool Z3_API Z3_solver_check_assumptions(__in Z3_context c, __in Z3_solver s, __in unsigned num_assumptions, __in_ecount(num_assumptions) Z3_ast const assumptions[])
Check whether the assertions in the given solver and optional assumptions are consistent or not...
unsigned size() const
Definition: z3++.h:259
symbol name() const
Definition: z3++.h:438
friend expr operator|(expr const &a, int b)
Definition: z3++.h:865
Z3_ast Z3_API Z3_mk_add(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].The array args must have num_args el...
void pop(unsigned n=1)
Definition: z3++.h:1277
Z3_ast Z3_API Z3_get_app_arg(__in Z3_context c, __in Z3_app a, __in unsigned i)
Return the i-th argument of the given application.
friend std::ostream & operator<<(std::ostream &out, stats const &s)
Definition: z3++.h:1235
void Z3_API Z3_set_param_value(__in Z3_config c, __in Z3_string param_id, __in Z3_string param_value)
Set a configuration parameter.
expr to_real(expr const &a)
Definition: z3++.h:1741
Z3_probe Z3_API Z3_mk_probe(__in Z3_context c, __in Z3_string name)
Return a probe associated with the given name. The complete list of probes may be obtained using the ...
friend expr operator>=(int a, expr const &b)
Definition: z3++.h:816
unsigned size() const
Definition: z3++.h:1229
friend expr implies(expr const &a, expr const &b)
Definition: z3++.h:645
Z3_probe Z3_API Z3_probe_and(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when p1 and p2 evaluates to true.
void Z3_API Z3_tactic_inc_ref(__in Z3_context c, __in Z3_tactic t)
Increment the reference counter of the given tactic.
Z3_ast Z3_API Z3_mk_const_array(__in Z3_context c, __in Z3_sort domain, __in Z3_ast v)
Create the constant array.
Z3_ast Z3_API Z3_mk_le(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create less than or equal to.
ast(ast const &s)
Definition: z3++.h:327
sort enumeration_sort(char const *name, unsigned n, char const *const *enum_names, func_decl_vector &cs, func_decl_vector &ts)
Return an enumeration sort: enum_names[0], ..., enum_names[n-1]. cs and ts are output parameters...
Definition: z3++.h:1542
friend expr operator==(int a, expr const &b)
Definition: z3++.h:666
friend expr operator|(int a, expr const &b)
Definition: z3++.h:866
sort(sort const &s)
Definition: z3++.h:354
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
apply_result(context &c, Z3_apply_result s)
Definition: z3++.h:1371
double Z3_API Z3_probe_apply(__in Z3_context c, __in Z3_probe p, __in Z3_goal g)
Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0...
Z3_ast Z3_API Z3_simplify_ex(__in Z3_context c, __in Z3_ast a, __in Z3_params p)
Interface to simplifier.
System.IntPtr Z3_params
Definition: Native.cs:27
friend expr operator^(int a, expr const &b)
Definition: z3++.h:862
Function declaration (aka function definition). It is the signature of interpreted and uninterpreted ...
Definition: z3++.h:427
T & operator[](int i)
Definition: z3++.h:260
unsigned Z3_API Z3_apply_result_get_num_subgoals(__in Z3_context c, __in Z3_apply_result r)
Return the number of subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
goal(goal const &s)
Definition: z3++.h:1328
sort int_sort()
Return the integer sort.
Definition: z3++.h:1538
stats & operator=(stats const &s)
Definition: z3++.h:1222
unsigned num_args() const
Definition: z3++.h:1128
func_decl & operator=(func_decl const &s)
Definition: z3++.h:433
apply_result & operator=(apply_result const &s)
Definition: z3++.h:1375
unsigned Z3_API Z3_stats_get_uint_value(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return the unsigned value of the given statistical data.
System.IntPtr Z3_func_interp
Definition: Native.cs:33
void Z3_API Z3_ast_vector_resize(__in Z3_context c, __in Z3_ast_vector v, __in unsigned n)
Resize the AST vector v.
Z3_ast_vector Z3_API Z3_mk_ast_vector(__in Z3_context c)
Return an empty AST vector.
bool is_real() const
Return true if this sort is the Real sort.
Definition: z3++.h:376
sort to_sort(context &c, Z3_sort s)
Definition: z3++.h:936
Z3_goal Z3_API Z3_mk_goal(__in Z3_context c, __in Z3_bool models, __in Z3_bool unsat_cores, __in Z3_bool proofs)
Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or trans...
context()
Definition: z3++.h:133
bool is_decided_sat() const
Definition: z3++.h:1346
void add(expr const &f)
Definition: z3++.h:1338
Z3_ast Z3_API Z3_mk_real(__in Z3_context c, __in int num, __in int den)
Create a real from a fraction.
Z3_string Z3_API Z3_solver_get_reason_unknown(__in Z3_context c, __in Z3_solver s)
Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the commands Z3_solver_ch...
unsigned size() const
Definition: z3++.h:1188
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition: z3_api.h:111
apply_result(apply_result const &s)
Definition: z3++.h:1372