Z3
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  expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); return expr(ctx(), r); }
870  unsigned lo() const { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 1)); }
871  unsigned hi() const { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 0)); }
872 
876  expr simplify() const { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
880  expr simplify(params const & p) const { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
881 
885  expr substitute(expr_vector const& src, expr_vector const& dst);
886 
890  expr substitute(expr_vector const& dst);
891 
892  };
893 
894  inline expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); }
895  inline expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); }
896 
897  inline expr pw(expr const & a, expr const & b) {
898  assert(a.is_arith() && b.is_arith());
899  check_context(a, b);
900  Z3_ast r = Z3_mk_power(a.ctx(), a, b);
901  a.check_error();
902  return expr(a.ctx(), r);
903  }
904  inline expr pw(expr const & a, int b) { return pw(a, a.ctx().num_val(b, a.get_sort())); }
905  inline expr pw(int a, expr const & b) { return pw(b.ctx().num_val(a, b.get_sort()), b); }
906 
907 
908 
909 
910 
917  inline expr ite(expr const & c, expr const & t, expr const & e) {
918  check_context(c, t); check_context(c, e);
919  assert(c.is_bool());
920  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
921  c.check_error();
922  return expr(c.ctx(), r);
923  }
924 
925 
930  inline expr to_expr(context & c, Z3_ast a) {
931  c.check_error();
932  assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
933  Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
934  Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
936  return expr(c, a);
937  }
938 
939  inline sort to_sort(context & c, Z3_sort s) {
940  c.check_error();
941  return sort(c, s);
942  }
943 
945  c.check_error();
946  return func_decl(c, f);
947  }
948 
952  inline expr ule(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
953  inline expr ule(expr const & a, int b) { return ule(a, a.ctx().num_val(b, a.get_sort())); }
954  inline expr ule(int a, expr const & b) { return ule(b.ctx().num_val(a, b.get_sort()), b); }
958  inline expr ult(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }
959  inline expr ult(expr const & a, int b) { return ult(a, a.ctx().num_val(b, a.get_sort())); }
960  inline expr ult(int a, expr const & b) { return ult(b.ctx().num_val(a, b.get_sort()), b); }
964  inline expr uge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }
965  inline expr uge(expr const & a, int b) { return uge(a, a.ctx().num_val(b, a.get_sort())); }
966  inline expr uge(int a, expr const & b) { return uge(b.ctx().num_val(a, b.get_sort()), b); }
970  inline expr ugt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
971  inline expr ugt(expr const & a, int b) { return ugt(a, a.ctx().num_val(b, a.get_sort())); }
972  inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), b); }
976  inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
977  inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); }
978  inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); }
979 
980  template<typename T> class cast_ast;
981 
982  template<> class cast_ast<ast> {
983  public:
984  ast operator()(context & c, Z3_ast a) { return ast(c, a); }
985  };
986 
987  template<> class cast_ast<expr> {
988  public:
990  assert(Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
991  Z3_get_ast_kind(c, a) == Z3_APP_AST ||
993  Z3_get_ast_kind(c, a) == Z3_VAR_AST);
994  return expr(c, a);
995  }
996  };
997 
998  template<> class cast_ast<sort> {
999  public:
1001  assert(Z3_get_ast_kind(c, a) == Z3_SORT_AST);
1002  return sort(c, reinterpret_cast<Z3_sort>(a));
1003  }
1004  };
1005 
1006  template<> class cast_ast<func_decl> {
1007  public:
1009  assert(Z3_get_ast_kind(c, a) == Z3_FUNC_DECL_AST);
1010  return func_decl(c, reinterpret_cast<Z3_func_decl>(a));
1011  }
1012  };
1013 
1014  template<typename T>
1015  class ast_vector_tpl : public object {
1016  Z3_ast_vector m_vector;
1017  void init(Z3_ast_vector v) { Z3_ast_vector_inc_ref(ctx(), v); m_vector = v; }
1018  public:
1020  ast_vector_tpl(context & c, Z3_ast_vector v):object(c) { init(v); }
1021  ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
1023  operator Z3_ast_vector() const { return m_vector; }
1024  unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); }
1025  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); }
1026  void push_back(T const & e) { Z3_ast_vector_push(ctx(), m_vector, e); check_error(); }
1027  void resize(unsigned sz) { Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }
1028  T back() const { return operator[](size() - 1); }
1029  void pop_back() { assert(size() > 0); resize(size() - 1); }
1030  bool empty() const { return size() == 0; }
1032  Z3_ast_vector_inc_ref(s.ctx(), s.m_vector);
1033  Z3_ast_vector_dec_ref(ctx(), m_vector);
1034  m_ctx = s.m_ctx;
1035  m_vector = s.m_vector;
1036  return *this;
1037  }
1038  friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
1039  };
1040 
1041  template<typename T>
1042  template<typename T2>
1044  m_array = new T[v.size()];
1045  m_size = v.size();
1046  for (unsigned i = 0; i < m_size; i++) {
1047  m_array[i] = v[i];
1048  }
1049  }
1050 
1051  // Basic functions for creating quantified formulas.
1052  // The C API should be used for creating quantifiers with patterns, weights, many variables, etc.
1053  inline expr forall(expr const & x, expr const & b) {
1054  check_context(x, b);
1055  Z3_app vars[] = {(Z3_app) x};
1056  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1057  }
1058  inline expr forall(expr const & x1, expr const & x2, expr const & b) {
1059  check_context(x1, b); check_context(x2, b);
1060  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1061  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1062  }
1063  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
1064  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1065  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1066  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1067  }
1068  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
1069  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1070  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1071  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1072  }
1073  inline expr forall(expr_vector const & xs, expr const & b) {
1074  array<Z3_app> vars(xs);
1075  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);
1076  }
1077  inline expr exists(expr const & x, expr const & b) {
1078  check_context(x, b);
1079  Z3_app vars[] = {(Z3_app) x};
1080  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1081  }
1082  inline expr exists(expr const & x1, expr const & x2, expr const & b) {
1083  check_context(x1, b); check_context(x2, b);
1084  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1085  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1086  }
1087  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
1088  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1089  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1090  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1091  }
1092  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
1093  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1094  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1095  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1096  }
1097  inline expr exists(expr_vector const & xs, expr const & b) {
1098  array<Z3_app> vars(xs);
1099  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);
1100  }
1101 
1102 
1103  inline expr distinct(expr_vector const& args) {
1104  assert(args.size() > 0);
1105  context& ctx = args[0].ctx();
1106  array<Z3_ast> _args(args);
1107  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
1108  ctx.check_error();
1109  return expr(ctx, r);
1110  }
1111 
1112  class func_entry : public object {
1113  Z3_func_entry m_entry;
1114  void init(Z3_func_entry e) {
1115  m_entry = e;
1116  Z3_func_entry_inc_ref(ctx(), m_entry);
1117  }
1118  public:
1119  func_entry(context & c, Z3_func_entry e):object(c) { init(e); }
1120  func_entry(func_entry const & s):object(s) { init(s.m_entry); }
1122  operator Z3_func_entry() const { return m_entry; }
1124  Z3_func_entry_inc_ref(s.ctx(), s.m_entry);
1125  Z3_func_entry_dec_ref(ctx(), m_entry);
1126  m_ctx = s.m_ctx;
1127  m_entry = s.m_entry;
1128  return *this;
1129  }
1130  expr value() const { Z3_ast r = Z3_func_entry_get_value(ctx(), m_entry); check_error(); return expr(ctx(), r); }
1131  unsigned num_args() const { unsigned r = Z3_func_entry_get_num_args(ctx(), m_entry); check_error(); return r; }
1132  expr arg(unsigned i) const { Z3_ast r = Z3_func_entry_get_arg(ctx(), m_entry, i); check_error(); return expr(ctx(), r); }
1133  };
1134 
1135  class func_interp : public object {
1136  Z3_func_interp m_interp;
1137  void init(Z3_func_interp e) {
1138  m_interp = e;
1139  Z3_func_interp_inc_ref(ctx(), m_interp);
1140  }
1141  public:
1142  func_interp(context & c, Z3_func_interp e):object(c) { init(e); }
1143  func_interp(func_interp const & s):object(s) { init(s.m_interp); }
1145  operator Z3_func_interp() const { return m_interp; }
1147  Z3_func_interp_inc_ref(s.ctx(), s.m_interp);
1148  Z3_func_interp_dec_ref(ctx(), m_interp);
1149  m_ctx = s.m_ctx;
1150  m_interp = s.m_interp;
1151  return *this;
1152  }
1153  expr else_value() const { Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), r); }
1154  unsigned num_entries() const { unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }
1155  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); }
1156  };
1157 
1158  class model : public object {
1159  Z3_model m_model;
1160  void init(Z3_model m) {
1161  m_model = m;
1162  Z3_model_inc_ref(ctx(), m);
1163  }
1164  public:
1165  model(context & c, Z3_model m):object(c) { init(m); }
1166  model(model const & s):object(s) { init(s.m_model); }
1167  ~model() { Z3_model_dec_ref(ctx(), m_model); }
1168  operator Z3_model() const { return m_model; }
1169  model & operator=(model const & s) {
1170  Z3_model_inc_ref(s.ctx(), s.m_model);
1171  Z3_model_dec_ref(ctx(), m_model);
1172  m_ctx = s.m_ctx;
1173  m_model = s.m_model;
1174  return *this;
1175  }
1176 
1177  expr eval(expr const & n, bool model_completion=false) const {
1178  check_context(*this, n);
1179  Z3_ast r;
1180  Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
1181  check_error();
1182  if (status == Z3_FALSE)
1183  throw exception("failed to evaluate expression");
1184  return expr(ctx(), r);
1185  }
1186 
1187  unsigned num_consts() const { return Z3_model_get_num_consts(ctx(), m_model); }
1188  unsigned num_funcs() const { return Z3_model_get_num_funcs(ctx(), m_model); }
1189  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); }
1190  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); }
1191  unsigned size() const { return num_consts() + num_funcs(); }
1192  func_decl operator[](int i) const {
1193  assert(0 <= i);
1194  return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
1195  }
1196 
1198  check_context(*this, c);
1199  Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);
1200  check_error();
1201  return expr(ctx(), r);
1202  }
1204  check_context(*this, f);
1205  Z3_func_interp r = Z3_model_get_func_interp(ctx(), m_model, f);
1206  check_error();
1207  return func_interp(ctx(), r);
1208  }
1209 
1210  friend std::ostream & operator<<(std::ostream & out, model const & m) { out << Z3_model_to_string(m.ctx(), m); return out; }
1211  };
1212 
1213  class stats : public object {
1214  Z3_stats m_stats;
1215  void init(Z3_stats e) {
1216  m_stats = e;
1217  Z3_stats_inc_ref(ctx(), m_stats);
1218  }
1219  public:
1220  stats(context & c):object(c), m_stats(0) {}
1221  stats(context & c, Z3_stats e):object(c) { init(e); }
1222  stats(stats const & s):object(s) { init(s.m_stats); }
1223  ~stats() { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); }
1224  operator Z3_stats() const { return m_stats; }
1225  stats & operator=(stats const & s) {
1226  Z3_stats_inc_ref(s.ctx(), s.m_stats);
1227  if (m_stats) Z3_stats_dec_ref(ctx(), m_stats);
1228  m_ctx = s.m_ctx;
1229  m_stats = s.m_stats;
1230  return *this;
1231  }
1232  unsigned size() const { return Z3_stats_size(ctx(), m_stats); }
1233  std::string key(unsigned i) const { Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; }
1234  bool is_uint(unsigned i) const { Z3_bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r != 0; }
1235  bool is_double(unsigned i) const { Z3_bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r != 0; }
1236  unsigned uint_value(unsigned i) const { unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; }
1237  double double_value(unsigned i) const { double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
1238  friend std::ostream & operator<<(std::ostream & out, stats const & s) { out << Z3_stats_to_string(s.ctx(), s); return out; }
1239  };
1240 
1243  };
1244 
1245  inline std::ostream & operator<<(std::ostream & out, check_result r) {
1246  if (r == unsat) out << "unsat";
1247  else if (r == sat) out << "sat";
1248  else out << "unknown";
1249  return out;
1250  }
1251 
1253  if (l == Z3_L_TRUE) return sat;
1254  else if (l == Z3_L_FALSE) return unsat;
1255  return unknown;
1256  }
1257 
1258  class solver : public object {
1259  Z3_solver m_solver;
1260  void init(Z3_solver s) {
1261  m_solver = s;
1262  Z3_solver_inc_ref(ctx(), s);
1263  }
1264  public:
1265  solver(context & c):object(c) { init(Z3_mk_solver(c)); }
1266  solver(context & c, Z3_solver s):object(c) { init(s); }
1267  solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); }
1268  solver(solver const & s):object(s) { init(s.m_solver); }
1269  ~solver() { Z3_solver_dec_ref(ctx(), m_solver); }
1270  operator Z3_solver() const { return m_solver; }
1271  solver & operator=(solver const & s) {
1272  Z3_solver_inc_ref(s.ctx(), s.m_solver);
1273  Z3_solver_dec_ref(ctx(), m_solver);
1274  m_ctx = s.m_ctx;
1275  m_solver = s.m_solver;
1276  return *this;
1277  }
1278  void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
1279  void push() { Z3_solver_push(ctx(), m_solver); check_error(); }
1280  void pop(unsigned n = 1) { Z3_solver_pop(ctx(), m_solver, n); check_error(); }
1281  void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); }
1282  void add(expr const & e) { assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); }
1283  void add(expr const & e, expr const & p) {
1284  assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
1285  Z3_solver_assert_and_track(ctx(), m_solver, e, p);
1286  check_error();
1287  }
1288  void add(expr const & e, char const * p) {
1289  add(e, ctx().bool_const(p));
1290  }
1292  check_result check(unsigned n, expr * const assumptions) {
1293  array<Z3_ast> _assumptions(n);
1294  for (unsigned i = 0; i < n; i++) {
1295  check_context(*this, assumptions[i]);
1296  _assumptions[i] = assumptions[i];
1297  }
1298  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
1299  check_error();
1300  return to_check_result(r);
1301  }
1302  check_result check(expr_vector assumptions) {
1303  unsigned n = assumptions.size();
1304  array<Z3_ast> _assumptions(n);
1305  for (unsigned i = 0; i < n; i++) {
1306  check_context(*this, assumptions[i]);
1307  _assumptions[i] = assumptions[i];
1308  }
1309  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
1310  check_error();
1311  return to_check_result(r);
1312  }
1313  model get_model() const { Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }
1314  std::string reason_unknown() const { Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }
1315  stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }
1316  expr_vector unsat_core() const { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
1317  expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
1318  expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
1319  friend std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
1320 
1321  std::string to_smt2(char const* status = "unknown") {
1322  array<Z3_ast> es(assertions());
1323  Z3_ast const* fmls = es.ptr();
1324  Z3_ast fml = 0;
1325  unsigned sz = es.size();
1326  if (sz > 0) {
1327  --sz;
1328  fml = fmls[sz];
1329  }
1330  else {
1331  fml = ctx().bool_val(true);
1332  }
1333  return std::string(Z3_benchmark_to_smtlib_string(
1334  ctx(),
1335  "", "", status, "",
1336  sz,
1337  fmls,
1338  fml));
1339  }
1340  };
1341 
1342  class goal : public object {
1343  Z3_goal m_goal;
1344  void init(Z3_goal s) {
1345  m_goal = s;
1346  Z3_goal_inc_ref(ctx(), s);
1347  }
1348  public:
1349  goal(context & c, bool models=true, bool unsat_cores=false, bool proofs=false):object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); }
1350  goal(context & c, Z3_goal s):object(c) { init(s); }
1351  goal(goal const & s):object(s) { init(s.m_goal); }
1352  ~goal() { Z3_goal_dec_ref(ctx(), m_goal); }
1353  operator Z3_goal() const { return m_goal; }
1354  goal & operator=(goal const & s) {
1355  Z3_goal_inc_ref(s.ctx(), s.m_goal);
1356  Z3_goal_dec_ref(ctx(), m_goal);
1357  m_ctx = s.m_ctx;
1358  m_goal = s.m_goal;
1359  return *this;
1360  }
1361  void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
1362  unsigned size() const { return Z3_goal_size(ctx(), m_goal); }
1363  expr operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
1364  Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); }
1365  bool inconsistent() const { return Z3_goal_inconsistent(ctx(), m_goal) != 0; }
1366  unsigned depth() const { return Z3_goal_depth(ctx(), m_goal); }
1367  void reset() { Z3_goal_reset(ctx(), m_goal); }
1368  unsigned num_exprs() const { return Z3_goal_num_exprs(ctx(), m_goal); }
1369  bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal) != 0; }
1370  bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal) != 0; }
1371  expr as_expr() const {
1372  unsigned n = size();
1373  if (n == 0)
1374  return ctx().bool_val(true);
1375  else if (n == 1)
1376  return operator[](0);
1377  else {
1378  array<Z3_ast> args(n);
1379  for (unsigned i = 0; i < n; i++)
1380  args[i] = operator[](i);
1381  return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
1382  }
1383  }
1384  friend std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; }
1385  };
1386 
1387  class apply_result : public object {
1388  Z3_apply_result m_apply_result;
1389  void init(Z3_apply_result s) {
1390  m_apply_result = s;
1392  }
1393  public:
1394  apply_result(context & c, Z3_apply_result s):object(c) { init(s); }
1395  apply_result(apply_result const & s):object(s) { init(s.m_apply_result); }
1396  ~apply_result() { Z3_apply_result_dec_ref(ctx(), m_apply_result); }
1397  operator Z3_apply_result() const { return m_apply_result; }
1399  Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result);
1400  Z3_apply_result_dec_ref(ctx(), m_apply_result);
1401  m_ctx = s.m_ctx;
1402  m_apply_result = s.m_apply_result;
1403  return *this;
1404  }
1405  unsigned size() const { return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }
1406  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); }
1407  model convert_model(model const & m, unsigned i = 0) const {
1408  check_context(*this, m);
1409  Z3_model new_m = Z3_apply_result_convert_model(ctx(), m_apply_result, i, m);
1410  check_error();
1411  return model(ctx(), new_m);
1412  }
1413  friend std::ostream & operator<<(std::ostream & out, apply_result const & r) { out << Z3_apply_result_to_string(r.ctx(), r); return out; }
1414  };
1415 
1416  class tactic : public object {
1417  Z3_tactic m_tactic;
1418  void init(Z3_tactic s) {
1419  m_tactic = s;
1420  Z3_tactic_inc_ref(ctx(), s);
1421  }
1422  public:
1423  tactic(context & c, char const * name):object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); }
1424  tactic(context & c, Z3_tactic s):object(c) { init(s); }
1425  tactic(tactic const & s):object(s) { init(s.m_tactic); }
1426  ~tactic() { Z3_tactic_dec_ref(ctx(), m_tactic); }
1427  operator Z3_tactic() const { return m_tactic; }
1428  tactic & operator=(tactic const & s) {
1429  Z3_tactic_inc_ref(s.ctx(), s.m_tactic);
1430  Z3_tactic_dec_ref(ctx(), m_tactic);
1431  m_ctx = s.m_ctx;
1432  m_tactic = s.m_tactic;
1433  return *this;
1434  }
1435  solver mk_solver() const { Z3_solver r = Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error(); return solver(ctx(), r); }
1436  apply_result apply(goal const & g) const {
1437  check_context(*this, g);
1438  Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g);
1439  check_error();
1440  return apply_result(ctx(), r);
1441  }
1442  apply_result operator()(goal const & g) const {
1443  return apply(g);
1444  }
1445  std::string help() const { char const * r = Z3_tactic_get_help(ctx(), m_tactic); check_error(); return r; }
1446  friend tactic operator&(tactic const & t1, tactic const & t2) {
1447  check_context(t1, t2);
1448  Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
1449  t1.check_error();
1450  return tactic(t1.ctx(), r);
1451  }
1452  friend tactic operator|(tactic const & t1, tactic const & t2) {
1453  check_context(t1, t2);
1454  Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
1455  t1.check_error();
1456  return tactic(t1.ctx(), r);
1457  }
1458  friend tactic repeat(tactic const & t, unsigned max);
1459  friend tactic with(tactic const & t, params const & p);
1460  friend tactic try_for(tactic const & t, unsigned ms);
1461  };
1462 
1463  inline tactic repeat(tactic const & t, unsigned max=UINT_MAX) {
1464  Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
1465  t.check_error();
1466  return tactic(t.ctx(), r);
1467  }
1468 
1469  inline tactic with(tactic const & t, params const & p) {
1470  Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
1471  t.check_error();
1472  return tactic(t.ctx(), r);
1473  }
1474  inline tactic try_for(tactic const & t, unsigned ms) {
1475  Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
1476  t.check_error();
1477  return tactic(t.ctx(), r);
1478  }
1479 
1480 
1481  class probe : public object {
1482  Z3_probe m_probe;
1483  void init(Z3_probe s) {
1484  m_probe = s;
1485  Z3_probe_inc_ref(ctx(), s);
1486  }
1487  public:
1488  probe(context & c, char const * name):object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); }
1489  probe(context & c, double val):object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); }
1490  probe(context & c, Z3_probe s):object(c) { init(s); }
1491  probe(probe const & s):object(s) { init(s.m_probe); }
1492  ~probe() { Z3_probe_dec_ref(ctx(), m_probe); }
1493  operator Z3_probe() const { return m_probe; }
1494  probe & operator=(probe const & s) {
1495  Z3_probe_inc_ref(s.ctx(), s.m_probe);
1496  Z3_probe_dec_ref(ctx(), m_probe);
1497  m_ctx = s.m_ctx;
1498  m_probe = s.m_probe;
1499  return *this;
1500  }
1501  double apply(goal const & g) const { double r = Z3_probe_apply(ctx(), m_probe, g); check_error(); return r; }
1502  double operator()(goal const & g) const { return apply(g); }
1503  friend probe operator<=(probe const & p1, probe const & p2) {
1504  check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1505  }
1506  friend probe operator<=(probe const & p1, double p2) { return p1 <= probe(p1.ctx(), p2); }
1507  friend probe operator<=(double p1, probe const & p2) { return probe(p2.ctx(), p1) <= p2; }
1508  friend probe operator>=(probe const & p1, probe const & p2) {
1509  check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1510  }
1511  friend probe operator>=(probe const & p1, double p2) { return p1 >= probe(p1.ctx(), p2); }
1512  friend probe operator>=(double p1, probe const & p2) { return probe(p2.ctx(), p1) >= p2; }
1513  friend probe operator<(probe const & p1, probe const & p2) {
1514  check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1515  }
1516  friend probe operator<(probe const & p1, double p2) { return p1 < probe(p1.ctx(), p2); }
1517  friend probe operator<(double p1, probe const & p2) { return probe(p2.ctx(), p1) < p2; }
1518  friend probe operator>(probe const & p1, probe const & p2) {
1519  check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1520  }
1521  friend probe operator>(probe const & p1, double p2) { return p1 > probe(p1.ctx(), p2); }
1522  friend probe operator>(double p1, probe const & p2) { return probe(p2.ctx(), p1) > p2; }
1523  friend probe operator==(probe const & p1, probe const & p2) {
1524  check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1525  }
1526  friend probe operator==(probe const & p1, double p2) { return p1 == probe(p1.ctx(), p2); }
1527  friend probe operator==(double p1, probe const & p2) { return probe(p2.ctx(), p1) == p2; }
1528  friend probe operator&&(probe const & p1, probe const & p2) {
1529  check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1530  }
1531  friend probe operator||(probe const & p1, probe const & p2) {
1532  check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1533  }
1534  friend probe operator!(probe const & p) {
1535  Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
1536  }
1537  };
1538 
1539  inline tactic fail_if(probe const & p) {
1540  Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
1541  p.check_error();
1542  return tactic(p.ctx(), r);
1543  }
1544  inline tactic when(probe const & p, tactic const & t) {
1545  check_context(p, t);
1546  Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
1547  t.check_error();
1548  return tactic(t.ctx(), r);
1549  }
1550  inline tactic cond(probe const & p, tactic const & t1, tactic const & t2) {
1551  check_context(p, t1); check_context(p, t2);
1552  Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
1553  t1.check_error();
1554  return tactic(t1.ctx(), r);
1555  }
1556 
1557  inline symbol context::str_symbol(char const * s) { Z3_symbol r = Z3_mk_string_symbol(m_ctx, s); check_error(); return symbol(*this, r); }
1558  inline symbol context::int_symbol(int n) { Z3_symbol r = Z3_mk_int_symbol(m_ctx, n); check_error(); return symbol(*this, r); }
1559 
1560  inline sort context::bool_sort() { Z3_sort s = Z3_mk_bool_sort(m_ctx); check_error(); return sort(*this, s); }
1561  inline sort context::int_sort() { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }
1562  inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
1563  inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
1564  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); }
1565  inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
1566  array<Z3_symbol> _enum_names(n);
1567  for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
1568  array<Z3_func_decl> _cs(n);
1569  array<Z3_func_decl> _ts(n);
1570  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
1571  sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
1572  check_error();
1573  for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
1574  return s;
1575  }
1576 
1577  inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
1578  array<Z3_sort> args(arity);
1579  for (unsigned i = 0; i < arity; i++) {
1580  check_context(domain[i], range);
1581  args[i] = domain[i];
1582  }
1583  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
1584  check_error();
1585  return func_decl(*this, f);
1586  }
1587 
1588  inline func_decl context::function(char const * name, unsigned arity, sort const * domain, sort const & range) {
1589  return function(range.ctx().str_symbol(name), arity, domain, range);
1590  }
1591 
1592  inline func_decl context::function(symbol const& name, sort_vector const& domain, sort const& range) {
1593  array<Z3_sort> args(domain.size());
1594  for (unsigned i = 0; i < domain.size(); i++) {
1595  check_context(domain[i], range);
1596  args[i] = domain[i];
1597  }
1598  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
1599  check_error();
1600  return func_decl(*this, f);
1601  }
1602 
1603  inline func_decl context::function(char const * name, sort_vector const& domain, sort const& range) {
1604  return function(range.ctx().str_symbol(name), domain, range);
1605  }
1606 
1607 
1608  inline func_decl context::function(char const * name, sort const & domain, sort const & range) {
1609  check_context(domain, range);
1610  Z3_sort args[1] = { domain };
1611  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
1612  check_error();
1613  return func_decl(*this, f);
1614  }
1615 
1616  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & range) {
1617  check_context(d1, range); check_context(d2, range);
1618  Z3_sort args[2] = { d1, d2 };
1619  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
1620  check_error();
1621  return func_decl(*this, f);
1622  }
1623 
1624  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
1625  check_context(d1, range); check_context(d2, range); check_context(d3, range);
1626  Z3_sort args[3] = { d1, d2, d3 };
1627  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
1628  check_error();
1629  return func_decl(*this, f);
1630  }
1631 
1632  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
1633  check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range);
1634  Z3_sort args[4] = { d1, d2, d3, d4 };
1635  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
1636  check_error();
1637  return func_decl(*this, f);
1638  }
1639 
1640  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) {
1641  check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range); check_context(d5, range);
1642  Z3_sort args[5] = { d1, d2, d3, d4, d5 };
1643  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
1644  check_error();
1645  return func_decl(*this, f);
1646  }
1647 
1648  inline expr context::constant(symbol const & name, sort const & s) {
1649  Z3_ast r = Z3_mk_const(m_ctx, name, s);
1650  check_error();
1651  return expr(*this, r);
1652  }
1653  inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); }
1654  inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); }
1655  inline expr context::int_const(char const * name) { return constant(name, int_sort()); }
1656  inline expr context::real_const(char const * name) { return constant(name, real_sort()); }
1657  inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); }
1658 
1659  inline expr context::bool_val(bool b) { return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }
1660 
1661  inline expr context::int_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
1662  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); }
1663  inline expr context::int_val(__int64 n) { Z3_ast r = Z3_mk_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
1664  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); }
1665  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); }
1666 
1667  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); }
1668  inline expr context::real_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
1669  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); }
1670  inline expr context::real_val(__int64 n) { Z3_ast r = Z3_mk_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
1671  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); }
1672  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); }
1673 
1674  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); }
1675  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); }
1676  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); }
1677  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); }
1678  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); }
1679 
1680  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); }
1681 
1682  inline expr func_decl::operator()(unsigned n, expr const * args) const {
1683  array<Z3_ast> _args(n);
1684  for (unsigned i = 0; i < n; i++) {
1685  check_context(*this, args[i]);
1686  _args[i] = args[i];
1687  }
1688  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
1689  check_error();
1690  return expr(ctx(), r);
1691 
1692  }
1693  inline expr func_decl::operator()(expr_vector const& args) const {
1694  array<Z3_ast> _args(args.size());
1695  for (unsigned i = 0; i < args.size(); i++) {
1696  check_context(*this, args[i]);
1697  _args[i] = args[i];
1698  }
1699  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
1700  check_error();
1701  return expr(ctx(), r);
1702  }
1703  inline expr func_decl::operator()() const {
1704  Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
1705  ctx().check_error();
1706  return expr(ctx(), r);
1707  }
1708  inline expr func_decl::operator()(expr const & a) const {
1709  check_context(*this, a);
1710  Z3_ast args[1] = { a };
1711  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
1712  ctx().check_error();
1713  return expr(ctx(), r);
1714  }
1715  inline expr func_decl::operator()(int a) const {
1716  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
1717  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
1718  ctx().check_error();
1719  return expr(ctx(), r);
1720  }
1721  inline expr func_decl::operator()(expr const & a1, expr const & a2) const {
1722  check_context(*this, a1); check_context(*this, a2);
1723  Z3_ast args[2] = { a1, a2 };
1724  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
1725  ctx().check_error();
1726  return expr(ctx(), r);
1727  }
1728  inline expr func_decl::operator()(expr const & a1, int a2) const {
1729  check_context(*this, a1);
1730  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
1731  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
1732  ctx().check_error();
1733  return expr(ctx(), r);
1734  }
1735  inline expr func_decl::operator()(int a1, expr const & a2) const {
1736  check_context(*this, a2);
1737  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
1738  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
1739  ctx().check_error();
1740  return expr(ctx(), r);
1741  }
1742  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3) const {
1743  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
1744  Z3_ast args[3] = { a1, a2, a3 };
1745  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
1746  ctx().check_error();
1747  return expr(ctx(), r);
1748  }
1749  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const {
1750  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
1751  Z3_ast args[4] = { a1, a2, a3, a4 };
1752  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
1753  ctx().check_error();
1754  return expr(ctx(), r);
1755  }
1756  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const {
1757  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
1758  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
1759  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
1760  ctx().check_error();
1761  return expr(ctx(), r);
1762  }
1763 
1764  inline expr to_real(expr const & a) { Z3_ast r = Z3_mk_int2real(a.ctx(), a); a.check_error(); return expr(a.ctx(), r); }
1765 
1766  inline func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
1767  return range.ctx().function(name, arity, domain, range);
1768  }
1769  inline func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range) {
1770  return range.ctx().function(name, arity, domain, range);
1771  }
1772  inline func_decl function(char const * name, sort const & domain, sort const & range) {
1773  return range.ctx().function(name, domain, range);
1774  }
1775  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range) {
1776  return range.ctx().function(name, d1, d2, range);
1777  }
1778  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
1779  return range.ctx().function(name, d1, d2, d3, range);
1780  }
1781  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
1782  return range.ctx().function(name, d1, d2, d3, d4, range);
1783  }
1784  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) {
1785  return range.ctx().function(name, d1, d2, d3, d4, d5, range);
1786  }
1787 
1788  inline expr select(expr const & a, expr const & i) {
1789  check_context(a, i);
1790  Z3_ast r = Z3_mk_select(a.ctx(), a, i);
1791  a.check_error();
1792  return expr(a.ctx(), r);
1793  }
1794  inline expr select(expr const & a, int i) { return select(a, a.ctx().num_val(i, a.get_sort().array_domain())); }
1795  inline expr store(expr const & a, expr const & i, expr const & v) {
1796  check_context(a, i); check_context(a, v);
1797  Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
1798  a.check_error();
1799  return expr(a.ctx(), r);
1800  }
1801  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); }
1802  inline expr store(expr const & a, expr i, int v) { return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
1803  inline expr store(expr const & a, int i, int v) {
1804  return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
1805  }
1806  inline expr const_array(sort const & d, expr const & v) {
1807  check_context(d, v);
1808  Z3_ast r = Z3_mk_const_array(d.ctx(), d, v);
1809  d.check_error();
1810  return expr(d.ctx(), r);
1811  }
1812 
1813  inline expr expr::substitute(expr_vector const& src, expr_vector const& dst) {
1814  assert(src.size() == dst.size());
1815  array<Z3_ast> _src(src.size());
1816  array<Z3_ast> _dst(dst.size());
1817  for (unsigned i = 0; i < src.size(); ++i) {
1818  _src[i] = src[i];
1819  _dst[i] = dst[i];
1820  }
1821  Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
1822  check_error();
1823  return expr(ctx(), r);
1824  }
1825 
1826  inline expr expr::substitute(expr_vector const& dst) {
1827  array<Z3_ast> _dst(dst.size());
1828  for (unsigned i = 0; i < dst.size(); ++i) {
1829  _dst[i] = dst[i];
1830  }
1831  Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
1832  check_error();
1833  return expr(ctx(), r);
1834  }
1835 
1836 
1837 
1838 };
1839 
1842 
1843 #endif
1844 
ast_vector_tpl(context &c)
Definition: z3++.h:1019
expr distinct(expr_vector const &args)
Definition: z3++.h:1103
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:1314
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:1445
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:1560
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:897
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:1428
probe(context &c, Z3_probe s)
Definition: z3++.h:1490
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:1494
func_decl get_const_decl(unsigned i) const
Definition: z3++.h:1189
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:1516
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:1557
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:1245
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:1279
System.IntPtr Z3_goal
Definition: Native.cs:25
stats statistics() const
Definition: z3++.h:1315
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:1550
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:1674
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:1130
bool is_real() const
Return true if this is a real expression.
Definition: z3++.h:483
Definition: z3_api.h:1285
func_interp & operator=(func_interp const &s)
Definition: z3++.h:1146
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:1489
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:1788
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:1123
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:1544
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
int Z3_API Z3_get_decl_int_parameter(__in Z3_context c, __in Z3_func_decl d, unsigned idx)
Return the integer value associated with an integer parameter.
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:1269
expr simplify() const
Return a simplified version of this expression.
Definition: z3++.h:876
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
void pop_back()
Definition: z3++.h:1029
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:1563
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:1235
expr udiv(expr const &a, expr const &b)
unsigned division operator for bitvectors.
Definition: z3++.h:976
apply_result operator()(goal const &g) const
Definition: z3++.h:1442
bool empty() const
Definition: z3++.h:1030
T back() const
Definition: z3++.h:1028
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:1435
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1356
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:1283
goal(context &c, Z3_goal s)
Definition: z3++.h:1350
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:1177
model(context &c, Z3_model m)
Definition: z3++.h:1165
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:1564
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:1648
friend probe operator>(double p1, probe const &p2)
Definition: z3++.h:1522
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:1192
System.IntPtr Z3_func_entry
Definition: Native.cs:34
friend probe operator>=(probe const &p1, double p2)
Definition: z3++.h:1511
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:1425
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:1492
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:1426
sort operator()(context &c, Z3_ast a)
Definition: z3++.h:1000
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:1531
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.
unsigned lo() const
Definition: z3++.h:870
Exception used to sign API usage errors.
Definition: z3++.h:80
unsigned uint_value(unsigned i) const
Definition: z3++.h:1236
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.
ast_vector_tpl(context &c, Z3_ast_vector v)
Definition: z3++.h:1020
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:1368
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:1234
expr ule(expr const &a, expr const &b)
unsigned less than or equal to operator for bitvectors.
Definition: z3++.h:952
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:1316
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:1242
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.
unsigned Z3_API Z3_get_decl_num_parameters(__in Z3_context c, __in Z3_func_decl d)
Return the number of parameters associated with a declaration.
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:1154
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:1521
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:1008
ast_vector_tpl< func_decl > func_decl_vector
Definition: z3++.h:70
stats(context &c)
Definition: z3++.h:1220
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:897
friend std::ostream & operator<<(std::ostream &out, goal const &g)
Definition: z3++.h:1384
friend probe operator>=(probe const &p1, probe const &p2)
Definition: z3++.h:1508
expr(context &c, Z3_ast n)
Definition: z3++.h:463
~goal()
Definition: z3++.h:1352
friend expr operator^(expr const &a, int b)
Definition: z3++.h:861
expr operator[](int i) const
Definition: z3++.h:1363
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:1103
check_result check(unsigned n, expr *const assumptions)
Definition: z3++.h:1292
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:1302
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:1488
friend std::ostream & operator<<(std::ostream &out, solver const &s)
Definition: z3++.h:1319
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:1223
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:1197
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:1452
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:880
friend expr operator&(int a, expr const &b)
Definition: z3++.h:858
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:1266
Z3 global configuration object.
Definition: z3++.h:93
solver & operator=(solver const &s)
Definition: z3++.h:1271
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:1813
ast(context &c, Z3_ast n)
Definition: z3++.h:326
ast_vector_tpl & operator=(ast_vector_tpl const &s)
Definition: z3++.h:1031
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:1413
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:1318
expr bv_const(char const *name, unsigned sz)
Definition: z3++.h:1657
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...
tactic(context &c, char const *name)
Definition: z3++.h:1423
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:1469
System.IntPtr Z3_func_decl
Definition: Native.cs:16
void reset()
Definition: z3++.h:1281
friend expr operator<=(int a, expr const &b)
Definition: z3++.h:797
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:214
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:1119
void resize(unsigned sz)
Definition: z3++.h:1027
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
expr extract(unsigned hi, unsigned lo) const
Definition: z3++.h:869
void add(expr const &e, char const *p)
Definition: z3++.h:1288
func_decl to_func_decl(context &c, Z3_func_decl f)
Definition: z3++.h:944
unsigned depth() const
Definition: z3++.h:1366
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:1112
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:1291
unsigned size() const
Definition: z3++.h:1405
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.
std::string to_smt2(char const *status="unknown")
Definition: z3++.h:1321
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:1190
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:1577
expr operator()(context &c, Z3_ast a)
Definition: z3++.h:989
friend probe operator!(probe const &p)
Definition: z3++.h:1534
expr as_expr() const
Definition: z3++.h:1371
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:1268
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:1667
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:1143
Z3_decl_kind decl_kind() const
Definition: z3++.h:439
model & operator=(model const &s)
Definition: z3++.h:1169
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. The hash code is structural. You can use Z3_get_ast_id intercha...
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:1155
void add(expr const &e)
Definition: z3++.h:1282
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:970
goal & operator=(goal const &s)
Definition: z3++.h:1354
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:1806
stats(stats const &s)
Definition: z3++.h:1222
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:1210
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:1121
goal operator[](int i) const
Definition: z3++.h:1406
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:1526
Z3_sort Z3_API Z3_mk_int_sort(__in Z3_context c)
Create the integer type.
void reset()
Definition: z3++.h:1367
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
unsigned size() const
Definition: z3++.h:1024
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:1503
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:1655
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:1132
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
Z3_string Z3_API Z3_benchmark_to_smtlib_string(__in Z3_context c, __in Z3_string name, __in Z3_string logic, __in Z3_string status, __in Z3_string attributes, __in unsigned num_assumptions, __in_ecount(num_assumptions) Z3_ast const assumptions[], __in Z3_ast formula)
Convert the given benchmark into SMT-LIB formatted string.
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:1349
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:1446
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:1362
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:1469
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:1656
friend probe operator<=(double p1, probe const &p2)
Definition: z3++.h:1507
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:1203
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:1523
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:1512
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:1407
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:1167
sort real_sort()
Return the Real sort.
Definition: z3++.h:1562
System.IntPtr Z3_app
Definition: Native.cs:14
friend std::ostream & operator<<(std::ostream &out, ast_vector_tpl const &v)
Definition: z3++.h:1038
Z3_ast Z3_API Z3_mk_extract(__in Z3_context c, __in unsigned high, __in unsigned low, __in Z3_ast t1)
Extract the bits high down to low from a bitvector of size m to yield a new bitvector of size n...
bool inconsistent() const
Definition: z3++.h:1365
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
ast_vector_tpl(ast_vector_tpl const &s)
Definition: z3++.h:1021
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:1680
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:1187
symbol int_symbol(int n)
Create a Z3 symbol based on the given integer.
Definition: z3++.h:1558
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:1518
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:1517
unsigned num_funcs() const
Definition: z3++.h:1188
expr operator()() const
Definition: z3++.h:1703
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:1527
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:1252
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:1463
T operator[](int i) const
Definition: z3++.h:1025
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:1424
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:1654
double apply(goal const &g) const
Definition: z3++.h:1501
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:917
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:1166
unsigned hi() const
Definition: z3++.h:871
check_result
Definition: z3++.h:1241
probe(probe const &s)
Definition: z3++.h:1491
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:1364
solver(context &c)
Definition: z3++.h:1265
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:1370
System.IntPtr Z3_model
Definition: Native.cs:18
friend probe operator<(probe const &p1, probe const &p2)
Definition: z3++.h:1513
friend expr operator==(expr const &a, int b)
Definition: z3++.h:665
expr_vector assertions() const
Definition: z3++.h:1317
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:1528
void add(expr const &e, expr const &p)
Definition: z3++.h:1283
expr store(expr const &a, expr const &i, expr const &v)
Definition: z3++.h:1795
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:1233
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:1463
expr bool_val(bool b)
Definition: z3++.h:1659
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:958
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
apply_result apply(goal const &g) const
Definition: z3++.h:1436
expr int_val(int n)
Definition: z3++.h:1661
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:1313
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:1153
tactic fail_if(probe const &p)
Definition: z3++.h:1539
stats(context &c, Z3_stats e)
Definition: z3++.h:1221
expr exists(expr const &x, expr const &b)
Definition: z3++.h:1077
ast operator()(context &c, Z3_ast a)
Definition: z3++.h:984
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:917
T const & operator[](int i) const
Definition: z3++.h:261
func_entry(func_entry const &s)
Definition: z3++.h:1120
double double_value(unsigned i) const
Definition: z3++.h:1237
expr body() const
Return the 'body' of this quantifier.
Definition: z3++.h:570
~ast()
Definition: z3++.h:328
#define Z3_FALSE
False value. It is just an alias for 0.
Definition: z3_api.h:127
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:1053
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:1502
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:930
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:1267
tactic try_for(tactic const &t, unsigned ms)
Definition: z3++.h:1474
func_interp(context &c, Z3_func_interp e)
Definition: z3++.h:1142
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:1474
void push_back(T const &e)
Definition: z3++.h:1026
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:964
expr implies(expr const &a, bool b)
Definition: z3++.h:894
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:1278
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:1506
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:1280
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:1238
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:1764
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:1232
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:1565
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:966
apply_result(context &c, Z3_apply_result s)
Definition: z3++.h:1394
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:1351
sort int_sort()
Return the integer sort.
Definition: z3++.h:1561
stats & operator=(stats const &s)
Definition: z3++.h:1225
unsigned num_args() const
Definition: z3++.h:1131
func_decl & operator=(func_decl const &s)
Definition: z3++.h:433
apply_result & operator=(apply_result const &s)
Definition: z3++.h:1398
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:939
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:1369
void add(expr const &f)
Definition: z3++.h:1361
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:1191
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:1395