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);
209  sort uninterpreted_sort(char const* name);
210  sort uninterpreted_sort(symbol const& name);
211 
212  func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range);
213  func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range);
214  func_decl function(symbol const& name, sort_vector const& domain, sort const& range);
215  func_decl function(char const * name, sort_vector const& domain, sort const& range);
216  func_decl function(char const * name, sort const & domain, sort const & range);
217  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range);
218  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range);
219  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range);
220  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range);
221 
222  expr constant(symbol const & name, sort const & s);
223  expr constant(char const * name, sort const & s);
224  expr bool_const(char const * name);
225  expr int_const(char const * name);
226  expr real_const(char const * name);
227  expr bv_const(char const * name, unsigned sz);
228 
229  expr bool_val(bool b);
230 
231  expr int_val(int n);
232  expr int_val(unsigned n);
233  expr int_val(__int64 n);
234  expr int_val(__uint64 n);
235  expr int_val(char const * n);
236 
237  expr real_val(int n, int d);
238  expr real_val(int n);
239  expr real_val(unsigned n);
240  expr real_val(__int64 n);
241  expr real_val(__uint64 n);
242  expr real_val(char const * n);
243 
244  expr bv_val(int n, unsigned sz);
245  expr bv_val(unsigned n, unsigned sz);
246  expr bv_val(__int64 n, unsigned sz);
247  expr bv_val(__uint64 n, unsigned sz);
248  expr bv_val(char const * n, unsigned sz);
249 
250  expr num_val(int n, sort const & s);
251  };
252 
253  template<typename T>
254  class array {
255  T * m_array;
256  unsigned m_size;
257  array(array const & s);
258  array & operator=(array const & s);
259  public:
260  array(unsigned sz):m_size(sz) { m_array = new T[sz]; }
261  template<typename T2>
262  array(ast_vector_tpl<T2> const & v);
263  ~array() { delete[] m_array; }
264  unsigned size() const { return m_size; }
265  T & operator[](int i) { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
266  T const & operator[](int i) const { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
267  T const * ptr() const { return m_array; }
268  T * ptr() { return m_array; }
269  };
270 
271  class object {
272  protected:
274  public:
275  object(context & c):m_ctx(&c) {}
276  object(object const & s):m_ctx(s.m_ctx) {}
277  context & ctx() const { return *m_ctx; }
278  void check_error() const { m_ctx->check_error(); }
279  friend void check_context(object const & a, object const & b);
280  };
281  inline void check_context(object const & a, object const & b) { assert(a.m_ctx == b.m_ctx); }
282 
283  class symbol : public object {
284  Z3_symbol m_sym;
285  public:
286  symbol(context & c, Z3_symbol s):object(c), m_sym(s) {}
287  symbol(symbol const & s):object(s), m_sym(s.m_sym) {}
288  symbol & operator=(symbol const & s) { m_ctx = s.m_ctx; m_sym = s.m_sym; return *this; }
289  operator Z3_symbol() const { return m_sym; }
290  Z3_symbol_kind kind() const { return Z3_get_symbol_kind(ctx(), m_sym); }
291  std::string str() const { assert(kind() == Z3_STRING_SYMBOL); return Z3_get_symbol_string(ctx(), m_sym); }
292  int to_int() const { assert(kind() == Z3_INT_SYMBOL); return Z3_get_symbol_int(ctx(), m_sym); }
293  friend std::ostream & operator<<(std::ostream & out, symbol const & s) {
294  if (s.kind() == Z3_INT_SYMBOL)
295  out << "k!" << s.to_int();
296  else
297  out << s.str().c_str();
298  return out;
299  }
300  };
301 
302 
303  class params : public object {
304  Z3_params m_params;
305  public:
306  params(context & c):object(c) { m_params = Z3_mk_params(c); Z3_params_inc_ref(ctx(), m_params); }
307  params(params const & s):object(s), m_params(s.m_params) { Z3_params_inc_ref(ctx(), m_params); }
308  ~params() { Z3_params_dec_ref(ctx(), m_params); }
309  operator Z3_params() const { return m_params; }
310  params & operator=(params const & s) {
311  Z3_params_inc_ref(s.ctx(), s.m_params);
312  Z3_params_dec_ref(ctx(), m_params);
313  m_ctx = s.m_ctx;
314  m_params = s.m_params;
315  return *this;
316  }
317  void set(char const * k, bool b) { Z3_params_set_bool(ctx(), m_params, ctx().str_symbol(k), b); }
318  void set(char const * k, unsigned n) { Z3_params_set_uint(ctx(), m_params, ctx().str_symbol(k), n); }
319  void set(char const * k, double n) { Z3_params_set_double(ctx(), m_params, ctx().str_symbol(k), n); }
320  void set(char const * k, symbol const & s) { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), s); }
321  friend std::ostream & operator<<(std::ostream & out, params const & p) {
322  out << Z3_params_to_string(p.ctx(), p); return out;
323  }
324  };
325 
326  class ast : public object {
327  protected:
329  public:
330  ast(context & c):object(c), m_ast(0) {}
331  ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
332  ast(ast const & s):object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
333  ~ast() { if (m_ast) Z3_dec_ref(*m_ctx, m_ast); }
334  operator Z3_ast() const { return m_ast; }
335  operator bool() const { return m_ast != 0; }
336  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; }
337  Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }
338  unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }
339  friend std::ostream & operator<<(std::ostream & out, ast const & n) {
340  out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
341  }
342 
346  friend bool eq(ast const & a, ast const & b);
347  };
348 
349  inline bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b) != 0; }
350 
351 
355  class sort : public ast {
356  public:
357  sort(context & c):ast(c) {}
358  sort(context & c, Z3_sort s):ast(c, reinterpret_cast<Z3_ast>(s)) {}
359  sort(sort const & s):ast(s) {}
360  operator Z3_sort() const { return reinterpret_cast<Z3_sort>(m_ast); }
364  sort & operator=(sort const & s) { return static_cast<sort&>(ast::operator=(s)); }
368  Z3_sort_kind sort_kind() const { return Z3_get_sort_kind(*m_ctx, *this); }
369 
373  bool is_bool() const { return sort_kind() == Z3_BOOL_SORT; }
377  bool is_int() const { return sort_kind() == Z3_INT_SORT; }
381  bool is_real() const { return sort_kind() == Z3_REAL_SORT; }
385  bool is_arith() const { return is_int() || is_real(); }
389  bool is_bv() const { return sort_kind() == Z3_BV_SORT; }
393  bool is_array() const { return sort_kind() == Z3_ARRAY_SORT; }
397  bool is_datatype() const { return sort_kind() == Z3_DATATYPE_SORT; }
401  bool is_relation() const { return sort_kind() == Z3_RELATION_SORT; }
405  bool is_finite_domain() const { return sort_kind() == Z3_FINITE_DOMAIN_SORT; }
406 
412  unsigned bv_size() const { assert(is_bv()); unsigned r = Z3_get_bv_sort_size(ctx(), *this); check_error(); return r; }
413 
419  sort array_domain() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_domain(ctx(), *this); check_error(); return sort(ctx(), s); }
425  sort array_range() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_range(ctx(), *this); check_error(); return sort(ctx(), s); }
426  };
427 
432  class func_decl : public ast {
433  public:
434  func_decl(context & c):ast(c) {}
435  func_decl(context & c, Z3_func_decl n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
436  func_decl(func_decl const & s):ast(s) {}
437  operator Z3_func_decl() const { return reinterpret_cast<Z3_func_decl>(m_ast); }
438  func_decl & operator=(func_decl const & s) { return static_cast<func_decl&>(ast::operator=(s)); }
439 
440  unsigned arity() const { return Z3_get_arity(ctx(), *this); }
441  sort domain(unsigned i) const { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }
442  sort range() const { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }
443  symbol name() const { Z3_symbol s = Z3_get_decl_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
444  Z3_decl_kind decl_kind() const { return Z3_get_decl_kind(ctx(), *this); }
445 
446  bool is_const() const { return arity() == 0; }
447 
448  expr operator()() const;
449  expr operator()(unsigned n, expr const * args) const;
450  expr operator()(expr_vector const& v) const;
451  expr operator()(expr const & a) const;
452  expr operator()(int a) const;
453  expr operator()(expr const & a1, expr const & a2) const;
454  expr operator()(expr const & a1, int a2) const;
455  expr operator()(int a1, expr const & a2) const;
456  expr operator()(expr const & a1, expr const & a2, expr const & a3) const;
457  expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const;
458  expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const;
459  };
460 
465  class expr : public ast {
466  public:
467  expr(context & c):ast(c) {}
468  expr(context & c, Z3_ast n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
469  expr(expr const & n):ast(n) {}
470  expr & operator=(expr const & n) { return static_cast<expr&>(ast::operator=(n)); }
471 
475  sort get_sort() const { Z3_sort s = Z3_get_sort(*m_ctx, m_ast); check_error(); return sort(*m_ctx, s); }
476 
480  bool is_bool() const { return get_sort().is_bool(); }
484  bool is_int() const { return get_sort().is_int(); }
488  bool is_real() const { return get_sort().is_real(); }
492  bool is_arith() const { return get_sort().is_arith(); }
496  bool is_bv() const { return get_sort().is_bv(); }
500  bool is_array() const { return get_sort().is_array(); }
504  bool is_datatype() const { return get_sort().is_datatype(); }
508  bool is_relation() const { return get_sort().is_relation(); }
517  bool is_finite_domain() const { return get_sort().is_finite_domain(); }
518 
522  bool is_numeral() const { return kind() == Z3_NUMERAL_AST; }
526  bool is_app() const { return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
530  bool is_const() const { return is_app() && num_args() == 0; }
534  bool is_quantifier() const { return kind() == Z3_QUANTIFIER_AST; }
538  bool is_var() const { return kind() == Z3_VAR_AST; }
539 
543  bool is_well_sorted() const { bool r = Z3_is_well_sorted(ctx(), m_ast) != 0; check_error(); return r; }
544 
545  operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
546 
553  func_decl decl() const { Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }
560  unsigned num_args() const { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
568  expr arg(unsigned i) const { Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }
569 
575  expr body() const { assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
576 
582  friend expr operator!(expr const & a) {
583  assert(a.is_bool());
584  Z3_ast r = Z3_mk_not(a.ctx(), a);
585  a.check_error();
586  return expr(a.ctx(), r);
587  }
588 
589 
596  friend expr operator&&(expr const & a, expr const & b) {
597  check_context(a, b);
598  assert(a.is_bool() && b.is_bool());
599  Z3_ast args[2] = { a, b };
600  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
601  a.check_error();
602  return expr(a.ctx(), r);
603  }
604 
605 
612  friend expr operator&&(expr const & a, bool b) { return a && a.ctx().bool_val(b); }
619  friend expr operator&&(bool a, expr const & b) { return b.ctx().bool_val(a) && b; }
620 
627  friend expr operator||(expr const & a, expr const & b) {
628  check_context(a, b);
629  assert(a.is_bool() && b.is_bool());
630  Z3_ast args[2] = { a, b };
631  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
632  a.check_error();
633  return expr(a.ctx(), r);
634  }
641  friend expr operator||(expr const & a, bool b) { return a || a.ctx().bool_val(b); }
648  friend expr operator||(bool a, expr const & b) { return b.ctx().bool_val(a) || b; }
649 
650  friend expr implies(expr const & a, expr const & b) {
651  check_context(a, b);
652  assert(a.is_bool() && b.is_bool());
653  Z3_ast r = Z3_mk_implies(a.ctx(), a, b);
654  a.check_error();
655  return expr(a.ctx(), r);
656  }
657  friend expr implies(expr const & a, bool b);
658  friend expr implies(bool a, expr const & b);
659 
660  friend expr ite(expr const & c, expr const & t, expr const & e);
661 
662  friend expr distinct(expr_vector const& args);
663  friend expr concat(expr const& a, expr const& b);
664 
665  friend expr operator==(expr const & a, expr const & b) {
666  check_context(a, b);
667  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
668  a.check_error();
669  return expr(a.ctx(), r);
670  }
671  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()); }
672  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; }
673 
674  friend expr operator!=(expr const & a, expr const & b) {
675  check_context(a, b);
676  Z3_ast args[2] = { a, b };
677  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
678  a.check_error();
679  return expr(a.ctx(), r);
680  }
681  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()); }
682  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; }
683 
684  friend expr operator+(expr const & a, expr const & b) {
685  check_context(a, b);
686  Z3_ast r = 0;
687  if (a.is_arith() && b.is_arith()) {
688  Z3_ast args[2] = { a, b };
689  r = Z3_mk_add(a.ctx(), 2, args);
690  }
691  else if (a.is_bv() && b.is_bv()) {
692  r = Z3_mk_bvadd(a.ctx(), a, b);
693  }
694  else {
695  // operator is not supported by given arguments.
696  assert(false);
697  }
698  a.check_error();
699  return expr(a.ctx(), r);
700  }
701  friend expr operator+(expr const & a, int b) { return a + a.ctx().num_val(b, a.get_sort()); }
702  friend expr operator+(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) + b; }
703 
704  friend expr operator*(expr const & a, expr const & b) {
705  check_context(a, b);
706  Z3_ast r = 0;
707  if (a.is_arith() && b.is_arith()) {
708  Z3_ast args[2] = { a, b };
709  r = Z3_mk_mul(a.ctx(), 2, args);
710  }
711  else if (a.is_bv() && b.is_bv()) {
712  r = Z3_mk_bvmul(a.ctx(), a, b);
713  }
714  else {
715  // operator is not supported by given arguments.
716  assert(false);
717  }
718  a.check_error();
719  return expr(a.ctx(), r);
720  }
721  friend expr operator*(expr const & a, int b) { return a * a.ctx().num_val(b, a.get_sort()); }
722  friend expr operator*(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) * b; }
723 
727  friend expr pw(expr const & a, expr const & b);
728  friend expr pw(expr const & a, int b);
729  friend expr pw(int a, expr const & b);
730 
731  friend expr operator/(expr const & a, expr const & b) {
732  check_context(a, b);
733  Z3_ast r = 0;
734  if (a.is_arith() && b.is_arith()) {
735  r = Z3_mk_div(a.ctx(), a, b);
736  }
737  else if (a.is_bv() && b.is_bv()) {
738  r = Z3_mk_bvsdiv(a.ctx(), a, b);
739  }
740  else {
741  // operator is not supported by given arguments.
742  assert(false);
743  }
744  a.check_error();
745  return expr(a.ctx(), r);
746  }
747  friend expr operator/(expr const & a, int b) { return a / a.ctx().num_val(b, a.get_sort()); }
748  friend expr operator/(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) / b; }
749 
750  friend expr operator-(expr const & a) {
751  Z3_ast r = 0;
752  if (a.is_arith()) {
753  r = Z3_mk_unary_minus(a.ctx(), a);
754  }
755  else if (a.is_bv()) {
756  r = Z3_mk_bvneg(a.ctx(), a);
757  }
758  else {
759  // operator is not supported by given arguments.
760  assert(false);
761  }
762  a.check_error();
763  return expr(a.ctx(), r);
764  }
765 
766  friend expr operator-(expr const & a, expr const & b) {
767  check_context(a, b);
768  Z3_ast r = 0;
769  if (a.is_arith() && b.is_arith()) {
770  Z3_ast args[2] = { a, b };
771  r = Z3_mk_sub(a.ctx(), 2, args);
772  }
773  else if (a.is_bv() && b.is_bv()) {
774  r = Z3_mk_bvsub(a.ctx(), a, b);
775  }
776  else {
777  // operator is not supported by given arguments.
778  assert(false);
779  }
780  a.check_error();
781  return expr(a.ctx(), r);
782  }
783  friend expr operator-(expr const & a, int b) { return a - a.ctx().num_val(b, a.get_sort()); }
784  friend expr operator-(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) - b; }
785 
786  friend expr operator<=(expr const & a, expr const & b) {
787  check_context(a, b);
788  Z3_ast r = 0;
789  if (a.is_arith() && b.is_arith()) {
790  r = Z3_mk_le(a.ctx(), a, b);
791  }
792  else if (a.is_bv() && b.is_bv()) {
793  r = Z3_mk_bvsle(a.ctx(), a, b);
794  }
795  else {
796  // operator is not supported by given arguments.
797  assert(false);
798  }
799  a.check_error();
800  return expr(a.ctx(), r);
801  }
802  friend expr operator<=(expr const & a, int b) { return a <= a.ctx().num_val(b, a.get_sort()); }
803  friend expr operator<=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) <= b; }
804 
805  friend expr operator>=(expr const & a, expr const & b) {
806  check_context(a, b);
807  Z3_ast r = 0;
808  if (a.is_arith() && b.is_arith()) {
809  r = Z3_mk_ge(a.ctx(), a, b);
810  }
811  else if (a.is_bv() && b.is_bv()) {
812  r = Z3_mk_bvsge(a.ctx(), a, b);
813  }
814  else {
815  // operator is not supported by given arguments.
816  assert(false);
817  }
818  a.check_error();
819  return expr(a.ctx(), r);
820  }
821  friend expr operator>=(expr const & a, int b) { return a >= a.ctx().num_val(b, a.get_sort()); }
822  friend expr operator>=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) >= b; }
823 
824  friend expr operator<(expr const & a, expr const & b) {
825  check_context(a, b);
826  Z3_ast r = 0;
827  if (a.is_arith() && b.is_arith()) {
828  r = Z3_mk_lt(a.ctx(), a, b);
829  }
830  else if (a.is_bv() && b.is_bv()) {
831  r = Z3_mk_bvslt(a.ctx(), a, b);
832  }
833  else {
834  // operator is not supported by given arguments.
835  assert(false);
836  }
837  a.check_error();
838  return expr(a.ctx(), r);
839  }
840  friend expr operator<(expr const & a, int b) { return a < a.ctx().num_val(b, a.get_sort()); }
841  friend expr operator<(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) < b; }
842 
843  friend expr operator>(expr const & a, expr const & b) {
844  check_context(a, b);
845  Z3_ast r = 0;
846  if (a.is_arith() && b.is_arith()) {
847  r = Z3_mk_gt(a.ctx(), a, b);
848  }
849  else if (a.is_bv() && b.is_bv()) {
850  r = Z3_mk_bvsgt(a.ctx(), a, b);
851  }
852  else {
853  // operator is not supported by given arguments.
854  assert(false);
855  }
856  a.check_error();
857  return expr(a.ctx(), r);
858  }
859  friend expr operator>(expr const & a, int b) { return a > a.ctx().num_val(b, a.get_sort()); }
860  friend expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > b; }
861 
862  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); }
863  friend expr operator&(expr const & a, int b) { return a & a.ctx().num_val(b, a.get_sort()); }
864  friend expr operator&(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) & b; }
865 
866  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); }
867  friend expr operator^(expr const & a, int b) { return a ^ a.ctx().num_val(b, a.get_sort()); }
868  friend expr operator^(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) ^ b; }
869 
870  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); }
871  friend expr operator|(expr const & a, int b) { return a | a.ctx().num_val(b, a.get_sort()); }
872  friend expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; }
873 
874  friend expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
875  expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); return expr(ctx(), r); }
876  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)); }
877  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)); }
878 
882  expr simplify() const { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
886  expr simplify(params const & p) const { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
887 
891  expr substitute(expr_vector const& src, expr_vector const& dst);
892 
896  expr substitute(expr_vector const& dst);
897 
898  };
899 
900  inline expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); }
901  inline expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); }
902 
903  inline expr pw(expr const & a, expr const & b) {
904  assert(a.is_arith() && b.is_arith());
905  check_context(a, b);
906  Z3_ast r = Z3_mk_power(a.ctx(), a, b);
907  a.check_error();
908  return expr(a.ctx(), r);
909  }
910  inline expr pw(expr const & a, int b) { return pw(a, a.ctx().num_val(b, a.get_sort())); }
911  inline expr pw(int a, expr const & b) { return pw(b.ctx().num_val(a, b.get_sort()), b); }
912 
913 
914 
915 
916 
923  inline expr ite(expr const & c, expr const & t, expr const & e) {
924  check_context(c, t); check_context(c, e);
925  assert(c.is_bool());
926  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
927  c.check_error();
928  return expr(c.ctx(), r);
929  }
930 
931 
936  inline expr to_expr(context & c, Z3_ast a) {
937  c.check_error();
938  assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
939  Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
940  Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
942  return expr(c, a);
943  }
944 
945  inline sort to_sort(context & c, Z3_sort s) {
946  c.check_error();
947  return sort(c, s);
948  }
949 
951  c.check_error();
952  return func_decl(c, f);
953  }
954 
958  inline expr ule(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
959  inline expr ule(expr const & a, int b) { return ule(a, a.ctx().num_val(b, a.get_sort())); }
960  inline expr ule(int a, expr const & b) { return ule(b.ctx().num_val(a, b.get_sort()), b); }
964  inline expr ult(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }
965  inline expr ult(expr const & a, int b) { return ult(a, a.ctx().num_val(b, a.get_sort())); }
966  inline expr ult(int a, expr const & b) { return ult(b.ctx().num_val(a, b.get_sort()), b); }
970  inline expr uge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }
971  inline expr uge(expr const & a, int b) { return uge(a, a.ctx().num_val(b, a.get_sort())); }
972  inline expr uge(int a, expr const & b) { return uge(b.ctx().num_val(a, b.get_sort()), b); }
976  inline expr ugt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
977  inline expr ugt(expr const & a, int b) { return ugt(a, a.ctx().num_val(b, a.get_sort())); }
978  inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), b); }
982  inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
983  inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); }
984  inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); }
985 
986  template<typename T> class cast_ast;
987 
988  template<> class cast_ast<ast> {
989  public:
990  ast operator()(context & c, Z3_ast a) { return ast(c, a); }
991  };
992 
993  template<> class cast_ast<expr> {
994  public:
996  assert(Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
997  Z3_get_ast_kind(c, a) == Z3_APP_AST ||
999  Z3_get_ast_kind(c, a) == Z3_VAR_AST);
1000  return expr(c, a);
1001  }
1002  };
1003 
1004  template<> class cast_ast<sort> {
1005  public:
1007  assert(Z3_get_ast_kind(c, a) == Z3_SORT_AST);
1008  return sort(c, reinterpret_cast<Z3_sort>(a));
1009  }
1010  };
1011 
1012  template<> class cast_ast<func_decl> {
1013  public:
1015  assert(Z3_get_ast_kind(c, a) == Z3_FUNC_DECL_AST);
1016  return func_decl(c, reinterpret_cast<Z3_func_decl>(a));
1017  }
1018  };
1019 
1020  template<typename T>
1021  class ast_vector_tpl : public object {
1022  Z3_ast_vector m_vector;
1023  void init(Z3_ast_vector v) { Z3_ast_vector_inc_ref(ctx(), v); m_vector = v; }
1024  public:
1026  ast_vector_tpl(context & c, Z3_ast_vector v):object(c) { init(v); }
1027  ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
1028  ~ast_vector_tpl() { Z3_ast_vector_dec_ref(ctx(), m_vector); }
1029  operator Z3_ast_vector() const { return m_vector; }
1030  unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); }
1031  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); }
1032  void push_back(T const & e) { Z3_ast_vector_push(ctx(), m_vector, e); check_error(); }
1033  void resize(unsigned sz) { Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }
1034  T back() const { return operator[](size() - 1); }
1035  void pop_back() { assert(size() > 0); resize(size() - 1); }
1036  bool empty() const { return size() == 0; }
1038  Z3_ast_vector_inc_ref(s.ctx(), s.m_vector);
1039  Z3_ast_vector_dec_ref(ctx(), m_vector);
1040  m_ctx = s.m_ctx;
1041  m_vector = s.m_vector;
1042  return *this;
1043  }
1044  friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
1045  };
1046 
1047  template<typename T>
1048  template<typename T2>
1050  m_array = new T[v.size()];
1051  m_size = v.size();
1052  for (unsigned i = 0; i < m_size; i++) {
1053  m_array[i] = v[i];
1054  }
1055  }
1056 
1057  // Basic functions for creating quantified formulas.
1058  // The C API should be used for creating quantifiers with patterns, weights, many variables, etc.
1059  inline expr forall(expr const & x, expr const & b) {
1060  check_context(x, b);
1061  Z3_app vars[] = {(Z3_app) x};
1062  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1063  }
1064  inline expr forall(expr const & x1, expr const & x2, expr const & b) {
1065  check_context(x1, b); check_context(x2, b);
1066  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1067  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1068  }
1069  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
1070  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1071  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1072  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1073  }
1074  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
1075  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1076  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1077  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1078  }
1079  inline expr forall(expr_vector const & xs, expr const & b) {
1080  array<Z3_app> vars(xs);
1081  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);
1082  }
1083  inline expr exists(expr const & x, expr const & b) {
1084  check_context(x, b);
1085  Z3_app vars[] = {(Z3_app) x};
1086  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1087  }
1088  inline expr exists(expr const & x1, expr const & x2, expr const & b) {
1089  check_context(x1, b); check_context(x2, b);
1090  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1091  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1092  }
1093  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
1094  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1095  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1096  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1097  }
1098  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
1099  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1100  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1101  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1102  }
1103  inline expr exists(expr_vector const & xs, expr const & b) {
1104  array<Z3_app> vars(xs);
1105  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);
1106  }
1107 
1108 
1109  inline expr distinct(expr_vector const& args) {
1110  assert(args.size() > 0);
1111  context& ctx = args[0].ctx();
1112  array<Z3_ast> _args(args);
1113  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
1114  ctx.check_error();
1115  return expr(ctx, r);
1116  }
1117 
1118  inline expr concat(expr const& a, expr const& b) {
1119  check_context(a, b);
1120  Z3_ast r = Z3_mk_concat(a.ctx(), a, b);
1121  a.ctx().check_error();
1122  return expr(a.ctx(), r);
1123  }
1124 
1125  class func_entry : public object {
1126  Z3_func_entry m_entry;
1127  void init(Z3_func_entry e) {
1128  m_entry = e;
1129  Z3_func_entry_inc_ref(ctx(), m_entry);
1130  }
1131  public:
1132  func_entry(context & c, Z3_func_entry e):object(c) { init(e); }
1133  func_entry(func_entry const & s):object(s) { init(s.m_entry); }
1134  ~func_entry() { Z3_func_entry_dec_ref(ctx(), m_entry); }
1135  operator Z3_func_entry() const { return m_entry; }
1137  Z3_func_entry_inc_ref(s.ctx(), s.m_entry);
1138  Z3_func_entry_dec_ref(ctx(), m_entry);
1139  m_ctx = s.m_ctx;
1140  m_entry = s.m_entry;
1141  return *this;
1142  }
1143  expr value() const { Z3_ast r = Z3_func_entry_get_value(ctx(), m_entry); check_error(); return expr(ctx(), r); }
1144  unsigned num_args() const { unsigned r = Z3_func_entry_get_num_args(ctx(), m_entry); check_error(); return r; }
1145  expr arg(unsigned i) const { Z3_ast r = Z3_func_entry_get_arg(ctx(), m_entry, i); check_error(); return expr(ctx(), r); }
1146  };
1147 
1148  class func_interp : public object {
1149  Z3_func_interp m_interp;
1150  void init(Z3_func_interp e) {
1151  m_interp = e;
1152  Z3_func_interp_inc_ref(ctx(), m_interp);
1153  }
1154  public:
1155  func_interp(context & c, Z3_func_interp e):object(c) { init(e); }
1156  func_interp(func_interp const & s):object(s) { init(s.m_interp); }
1157  ~func_interp() { Z3_func_interp_dec_ref(ctx(), m_interp); }
1158  operator Z3_func_interp() const { return m_interp; }
1160  Z3_func_interp_inc_ref(s.ctx(), s.m_interp);
1161  Z3_func_interp_dec_ref(ctx(), m_interp);
1162  m_ctx = s.m_ctx;
1163  m_interp = s.m_interp;
1164  return *this;
1165  }
1166  expr else_value() const { Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), r); }
1167  unsigned num_entries() const { unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }
1168  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); }
1169  };
1170 
1171  class model : public object {
1172  Z3_model m_model;
1173  void init(Z3_model m) {
1174  m_model = m;
1175  Z3_model_inc_ref(ctx(), m);
1176  }
1177  public:
1178  model(context & c, Z3_model m):object(c) { init(m); }
1179  model(model const & s):object(s) { init(s.m_model); }
1180  ~model() { Z3_model_dec_ref(ctx(), m_model); }
1181  operator Z3_model() const { return m_model; }
1182  model & operator=(model const & s) {
1183  Z3_model_inc_ref(s.ctx(), s.m_model);
1184  Z3_model_dec_ref(ctx(), m_model);
1185  m_ctx = s.m_ctx;
1186  m_model = s.m_model;
1187  return *this;
1188  }
1189 
1190  expr eval(expr const & n, bool model_completion=false) const {
1191  check_context(*this, n);
1192  Z3_ast r = 0;
1193  Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
1194  check_error();
1195  if (status == Z3_FALSE)
1196  throw exception("failed to evaluate expression");
1197  return expr(ctx(), r);
1198  }
1199 
1200  unsigned num_consts() const { return Z3_model_get_num_consts(ctx(), m_model); }
1201  unsigned num_funcs() const { return Z3_model_get_num_funcs(ctx(), m_model); }
1202  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); }
1203  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); }
1204  unsigned size() const { return num_consts() + num_funcs(); }
1205  func_decl operator[](int i) const {
1206  assert(0 <= i);
1207  return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
1208  }
1209 
1211  check_context(*this, c);
1212  Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);
1213  check_error();
1214  return expr(ctx(), r);
1215  }
1217  check_context(*this, f);
1218  Z3_func_interp r = Z3_model_get_func_interp(ctx(), m_model, f);
1219  check_error();
1220  return func_interp(ctx(), r);
1221  }
1222 
1223  friend std::ostream & operator<<(std::ostream & out, model const & m) { out << Z3_model_to_string(m.ctx(), m); return out; }
1224  };
1225 
1226  class stats : public object {
1227  Z3_stats m_stats;
1228  void init(Z3_stats e) {
1229  m_stats = e;
1230  Z3_stats_inc_ref(ctx(), m_stats);
1231  }
1232  public:
1233  stats(context & c):object(c), m_stats(0) {}
1234  stats(context & c, Z3_stats e):object(c) { init(e); }
1235  stats(stats const & s):object(s) { init(s.m_stats); }
1236  ~stats() { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); }
1237  operator Z3_stats() const { return m_stats; }
1238  stats & operator=(stats const & s) {
1239  Z3_stats_inc_ref(s.ctx(), s.m_stats);
1240  if (m_stats) Z3_stats_dec_ref(ctx(), m_stats);
1241  m_ctx = s.m_ctx;
1242  m_stats = s.m_stats;
1243  return *this;
1244  }
1245  unsigned size() const { return Z3_stats_size(ctx(), m_stats); }
1246  std::string key(unsigned i) const { Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; }
1247  bool is_uint(unsigned i) const { Z3_bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r != 0; }
1248  bool is_double(unsigned i) const { Z3_bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r != 0; }
1249  unsigned uint_value(unsigned i) const { unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; }
1250  double double_value(unsigned i) const { double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
1251  friend std::ostream & operator<<(std::ostream & out, stats const & s) { out << Z3_stats_to_string(s.ctx(), s); return out; }
1252  };
1253 
1256  };
1257 
1258  inline std::ostream & operator<<(std::ostream & out, check_result r) {
1259  if (r == unsat) out << "unsat";
1260  else if (r == sat) out << "sat";
1261  else out << "unknown";
1262  return out;
1263  }
1264 
1266  if (l == Z3_L_TRUE) return sat;
1267  else if (l == Z3_L_FALSE) return unsat;
1268  return unknown;
1269  }
1270 
1271  class solver : public object {
1272  Z3_solver m_solver;
1273  void init(Z3_solver s) {
1274  m_solver = s;
1275  Z3_solver_inc_ref(ctx(), s);
1276  }
1277  public:
1278  solver(context & c):object(c) { init(Z3_mk_solver(c)); }
1279  solver(context & c, Z3_solver s):object(c) { init(s); }
1280  solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); }
1281  solver(solver const & s):object(s) { init(s.m_solver); }
1282  ~solver() { Z3_solver_dec_ref(ctx(), m_solver); }
1283  operator Z3_solver() const { return m_solver; }
1284  solver & operator=(solver const & s) {
1285  Z3_solver_inc_ref(s.ctx(), s.m_solver);
1286  Z3_solver_dec_ref(ctx(), m_solver);
1287  m_ctx = s.m_ctx;
1288  m_solver = s.m_solver;
1289  return *this;
1290  }
1291  void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
1292  void push() { Z3_solver_push(ctx(), m_solver); check_error(); }
1293  void pop(unsigned n = 1) { Z3_solver_pop(ctx(), m_solver, n); check_error(); }
1294  void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); }
1295  void add(expr const & e) { assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); }
1296  void add(expr const & e, expr const & p) {
1297  assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
1298  Z3_solver_assert_and_track(ctx(), m_solver, e, p);
1299  check_error();
1300  }
1301  void add(expr const & e, char const * p) {
1302  add(e, ctx().bool_const(p));
1303  }
1304  check_result check() { Z3_lbool r = Z3_solver_check(ctx(), m_solver); check_error(); return to_check_result(r); }
1305  check_result check(unsigned n, expr * const assumptions) {
1306  array<Z3_ast> _assumptions(n);
1307  for (unsigned i = 0; i < n; i++) {
1308  check_context(*this, assumptions[i]);
1309  _assumptions[i] = assumptions[i];
1310  }
1311  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
1312  check_error();
1313  return to_check_result(r);
1314  }
1315  check_result check(expr_vector assumptions) {
1316  unsigned n = assumptions.size();
1317  array<Z3_ast> _assumptions(n);
1318  for (unsigned i = 0; i < n; i++) {
1319  check_context(*this, assumptions[i]);
1320  _assumptions[i] = assumptions[i];
1321  }
1322  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
1323  check_error();
1324  return to_check_result(r);
1325  }
1326  model get_model() const { Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }
1327  std::string reason_unknown() const { Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }
1328  stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }
1329  expr_vector unsat_core() const { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
1330  expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
1331  expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
1332  friend std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
1333 
1334  std::string to_smt2(char const* status = "unknown") {
1335  array<Z3_ast> es(assertions());
1336  Z3_ast const* fmls = es.ptr();
1337  Z3_ast fml = 0;
1338  unsigned sz = es.size();
1339  if (sz > 0) {
1340  --sz;
1341  fml = fmls[sz];
1342  }
1343  else {
1344  fml = ctx().bool_val(true);
1345  }
1346  return std::string(Z3_benchmark_to_smtlib_string(
1347  ctx(),
1348  "", "", status, "",
1349  sz,
1350  fmls,
1351  fml));
1352  }
1353  };
1354 
1355  class goal : public object {
1356  Z3_goal m_goal;
1357  void init(Z3_goal s) {
1358  m_goal = s;
1359  Z3_goal_inc_ref(ctx(), s);
1360  }
1361  public:
1362  goal(context & c, bool models=true, bool unsat_cores=false, bool proofs=false):object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); }
1363  goal(context & c, Z3_goal s):object(c) { init(s); }
1364  goal(goal const & s):object(s) { init(s.m_goal); }
1365  ~goal() { Z3_goal_dec_ref(ctx(), m_goal); }
1366  operator Z3_goal() const { return m_goal; }
1367  goal & operator=(goal const & s) {
1368  Z3_goal_inc_ref(s.ctx(), s.m_goal);
1369  Z3_goal_dec_ref(ctx(), m_goal);
1370  m_ctx = s.m_ctx;
1371  m_goal = s.m_goal;
1372  return *this;
1373  }
1374  void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
1375  unsigned size() const { return Z3_goal_size(ctx(), m_goal); }
1376  expr operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
1377  Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); }
1378  bool inconsistent() const { return Z3_goal_inconsistent(ctx(), m_goal) != 0; }
1379  unsigned depth() const { return Z3_goal_depth(ctx(), m_goal); }
1380  void reset() { Z3_goal_reset(ctx(), m_goal); }
1381  unsigned num_exprs() const { return Z3_goal_num_exprs(ctx(), m_goal); }
1382  bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal) != 0; }
1383  bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal) != 0; }
1384  expr as_expr() const {
1385  unsigned n = size();
1386  if (n == 0)
1387  return ctx().bool_val(true);
1388  else if (n == 1)
1389  return operator[](0);
1390  else {
1391  array<Z3_ast> args(n);
1392  for (unsigned i = 0; i < n; i++)
1393  args[i] = operator[](i);
1394  return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
1395  }
1396  }
1397  friend std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; }
1398  };
1399 
1400  class apply_result : public object {
1401  Z3_apply_result m_apply_result;
1402  void init(Z3_apply_result s) {
1403  m_apply_result = s;
1404  Z3_apply_result_inc_ref(ctx(), s);
1405  }
1406  public:
1407  apply_result(context & c, Z3_apply_result s):object(c) { init(s); }
1408  apply_result(apply_result const & s):object(s) { init(s.m_apply_result); }
1409  ~apply_result() { Z3_apply_result_dec_ref(ctx(), m_apply_result); }
1410  operator Z3_apply_result() const { return m_apply_result; }
1412  Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result);
1413  Z3_apply_result_dec_ref(ctx(), m_apply_result);
1414  m_ctx = s.m_ctx;
1415  m_apply_result = s.m_apply_result;
1416  return *this;
1417  }
1418  unsigned size() const { return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }
1419  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); }
1420  model convert_model(model const & m, unsigned i = 0) const {
1421  check_context(*this, m);
1422  Z3_model new_m = Z3_apply_result_convert_model(ctx(), m_apply_result, i, m);
1423  check_error();
1424  return model(ctx(), new_m);
1425  }
1426  friend std::ostream & operator<<(std::ostream & out, apply_result const & r) { out << Z3_apply_result_to_string(r.ctx(), r); return out; }
1427  };
1428 
1429  class tactic : public object {
1430  Z3_tactic m_tactic;
1431  void init(Z3_tactic s) {
1432  m_tactic = s;
1433  Z3_tactic_inc_ref(ctx(), s);
1434  }
1435  public:
1436  tactic(context & c, char const * name):object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); }
1437  tactic(context & c, Z3_tactic s):object(c) { init(s); }
1438  tactic(tactic const & s):object(s) { init(s.m_tactic); }
1439  ~tactic() { Z3_tactic_dec_ref(ctx(), m_tactic); }
1440  operator Z3_tactic() const { return m_tactic; }
1441  tactic & operator=(tactic const & s) {
1442  Z3_tactic_inc_ref(s.ctx(), s.m_tactic);
1443  Z3_tactic_dec_ref(ctx(), m_tactic);
1444  m_ctx = s.m_ctx;
1445  m_tactic = s.m_tactic;
1446  return *this;
1447  }
1448  solver mk_solver() const { Z3_solver r = Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error(); return solver(ctx(), r); }
1449  apply_result apply(goal const & g) const {
1450  check_context(*this, g);
1451  Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g);
1452  check_error();
1453  return apply_result(ctx(), r);
1454  }
1455  apply_result operator()(goal const & g) const {
1456  return apply(g);
1457  }
1458  std::string help() const { char const * r = Z3_tactic_get_help(ctx(), m_tactic); check_error(); return r; }
1459  friend tactic operator&(tactic const & t1, tactic const & t2) {
1460  check_context(t1, t2);
1461  Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
1462  t1.check_error();
1463  return tactic(t1.ctx(), r);
1464  }
1465  friend tactic operator|(tactic const & t1, tactic const & t2) {
1466  check_context(t1, t2);
1467  Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
1468  t1.check_error();
1469  return tactic(t1.ctx(), r);
1470  }
1471  friend tactic repeat(tactic const & t, unsigned max);
1472  friend tactic with(tactic const & t, params const & p);
1473  friend tactic try_for(tactic const & t, unsigned ms);
1474  };
1475 
1476  inline tactic repeat(tactic const & t, unsigned max=UINT_MAX) {
1477  Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
1478  t.check_error();
1479  return tactic(t.ctx(), r);
1480  }
1481 
1482  inline tactic with(tactic const & t, params const & p) {
1483  Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
1484  t.check_error();
1485  return tactic(t.ctx(), r);
1486  }
1487  inline tactic try_for(tactic const & t, unsigned ms) {
1488  Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
1489  t.check_error();
1490  return tactic(t.ctx(), r);
1491  }
1492 
1493 
1494  class probe : public object {
1495  Z3_probe m_probe;
1496  void init(Z3_probe s) {
1497  m_probe = s;
1498  Z3_probe_inc_ref(ctx(), s);
1499  }
1500  public:
1501  probe(context & c, char const * name):object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); }
1502  probe(context & c, double val):object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); }
1503  probe(context & c, Z3_probe s):object(c) { init(s); }
1504  probe(probe const & s):object(s) { init(s.m_probe); }
1505  ~probe() { Z3_probe_dec_ref(ctx(), m_probe); }
1506  operator Z3_probe() const { return m_probe; }
1507  probe & operator=(probe const & s) {
1508  Z3_probe_inc_ref(s.ctx(), s.m_probe);
1509  Z3_probe_dec_ref(ctx(), m_probe);
1510  m_ctx = s.m_ctx;
1511  m_probe = s.m_probe;
1512  return *this;
1513  }
1514  double apply(goal const & g) const { double r = Z3_probe_apply(ctx(), m_probe, g); check_error(); return r; }
1515  double operator()(goal const & g) const { return apply(g); }
1516  friend probe operator<=(probe const & p1, probe const & p2) {
1517  check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1518  }
1519  friend probe operator<=(probe const & p1, double p2) { return p1 <= probe(p1.ctx(), p2); }
1520  friend probe operator<=(double p1, probe const & p2) { return probe(p2.ctx(), p1) <= p2; }
1521  friend probe operator>=(probe const & p1, probe const & p2) {
1522  check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1523  }
1524  friend probe operator>=(probe const & p1, double p2) { return p1 >= probe(p1.ctx(), p2); }
1525  friend probe operator>=(double p1, probe const & p2) { return probe(p2.ctx(), p1) >= p2; }
1526  friend probe operator<(probe const & p1, probe const & p2) {
1527  check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1528  }
1529  friend probe operator<(probe const & p1, double p2) { return p1 < probe(p1.ctx(), p2); }
1530  friend probe operator<(double p1, probe const & p2) { return probe(p2.ctx(), p1) < p2; }
1531  friend probe operator>(probe const & p1, probe const & p2) {
1532  check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1533  }
1534  friend probe operator>(probe const & p1, double p2) { return p1 > probe(p1.ctx(), p2); }
1535  friend probe operator>(double p1, probe const & p2) { return probe(p2.ctx(), p1) > p2; }
1536  friend probe operator==(probe const & p1, probe const & p2) {
1537  check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1538  }
1539  friend probe operator==(probe const & p1, double p2) { return p1 == probe(p1.ctx(), p2); }
1540  friend probe operator==(double p1, probe const & p2) { return probe(p2.ctx(), p1) == p2; }
1541  friend probe operator&&(probe const & p1, probe const & p2) {
1542  check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1543  }
1544  friend probe operator||(probe const & p1, probe const & p2) {
1545  check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1546  }
1547  friend probe operator!(probe const & p) {
1548  Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
1549  }
1550  };
1551 
1552  class optimize : public object {
1553  Z3_optimize m_opt;
1554  public:
1555  class handle {
1556  unsigned m_h;
1557  public:
1558  handle(unsigned h): m_h(h) {}
1559  unsigned h() const { return m_h; }
1560  };
1561  optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }
1562  ~optimize() { Z3_optimize_dec_ref(ctx(), m_opt); }
1563  operator Z3_optimize() const { return m_opt; }
1564  void add(expr const& e) {
1565  assert(e.is_bool());
1566  Z3_optimize_assert(ctx(), m_opt, e);
1567  }
1568  handle add(expr const& e, unsigned weight) {
1569  assert(e.is_bool());
1570  std::stringstream strm;
1571  strm << weight;
1572  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, strm.str().c_str(), 0));
1573  }
1574  handle add(expr const& e, char const* weight) {
1575  assert(e.is_bool());
1576  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0));
1577  }
1578  handle maximize(expr const& e) {
1579  return handle(Z3_optimize_maximize(ctx(), m_opt, e));
1580  }
1581  handle minimize(expr const& e) {
1582  return handle(Z3_optimize_minimize(ctx(), m_opt, e));
1583  }
1584  void push() {
1585  Z3_optimize_push(ctx(), m_opt);
1586  }
1587  void pop() {
1588  Z3_optimize_pop(ctx(), m_opt);
1589  }
1590  check_result check() { Z3_lbool r = Z3_optimize_check(ctx(), m_opt); check_error(); return to_check_result(r); }
1591  model get_model() const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }
1592  void set(params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }
1593  expr lower(handle const& h) {
1594  Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());
1595  check_error();
1596  return expr(ctx(), r);
1597  }
1598  expr upper(handle const& h) {
1599  Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h());
1600  check_error();
1601  return expr(ctx(), r);
1602  }
1603  stats statistics() const { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); }
1604  friend std::ostream & operator<<(std::ostream & out, optimize const & s) { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }
1605  std::string help() const { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error(); return r; }
1606  };
1607 
1608  inline tactic fail_if(probe const & p) {
1609  Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
1610  p.check_error();
1611  return tactic(p.ctx(), r);
1612  }
1613  inline tactic when(probe const & p, tactic const & t) {
1614  check_context(p, t);
1615  Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
1616  t.check_error();
1617  return tactic(t.ctx(), r);
1618  }
1619  inline tactic cond(probe const & p, tactic const & t1, tactic const & t2) {
1620  check_context(p, t1); check_context(p, t2);
1621  Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
1622  t1.check_error();
1623  return tactic(t1.ctx(), r);
1624  }
1625 
1626  inline symbol context::str_symbol(char const * s) { Z3_symbol r = Z3_mk_string_symbol(m_ctx, s); check_error(); return symbol(*this, r); }
1627  inline symbol context::int_symbol(int n) { Z3_symbol r = Z3_mk_int_symbol(m_ctx, n); check_error(); return symbol(*this, r); }
1628 
1629  inline sort context::bool_sort() { Z3_sort s = Z3_mk_bool_sort(m_ctx); check_error(); return sort(*this, s); }
1630  inline sort context::int_sort() { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }
1631  inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
1632  inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
1633  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); }
1634  inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
1635  array<Z3_symbol> _enum_names(n);
1636  for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
1637  array<Z3_func_decl> _cs(n);
1638  array<Z3_func_decl> _ts(n);
1639  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
1640  sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
1641  check_error();
1642  for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
1643  return s;
1644  }
1645  inline sort context::uninterpreted_sort(char const* name) {
1646  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
1647  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
1648  }
1650  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
1651  }
1652 
1653  inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
1654  array<Z3_sort> args(arity);
1655  for (unsigned i = 0; i < arity; i++) {
1656  check_context(domain[i], range);
1657  args[i] = domain[i];
1658  }
1659  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
1660  check_error();
1661  return func_decl(*this, f);
1662  }
1663 
1664  inline func_decl context::function(char const * name, unsigned arity, sort const * domain, sort const & range) {
1665  return function(range.ctx().str_symbol(name), arity, domain, range);
1666  }
1667 
1668  inline func_decl context::function(symbol const& name, sort_vector const& domain, sort const& range) {
1669  array<Z3_sort> args(domain.size());
1670  for (unsigned i = 0; i < domain.size(); i++) {
1671  check_context(domain[i], range);
1672  args[i] = domain[i];
1673  }
1674  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
1675  check_error();
1676  return func_decl(*this, f);
1677  }
1678 
1679  inline func_decl context::function(char const * name, sort_vector const& domain, sort const& range) {
1680  return function(range.ctx().str_symbol(name), domain, range);
1681  }
1682 
1683 
1684  inline func_decl context::function(char const * name, sort const & domain, sort const & range) {
1685  check_context(domain, range);
1686  Z3_sort args[1] = { domain };
1687  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
1688  check_error();
1689  return func_decl(*this, f);
1690  }
1691 
1692  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & range) {
1693  check_context(d1, range); check_context(d2, range);
1694  Z3_sort args[2] = { d1, d2 };
1695  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
1696  check_error();
1697  return func_decl(*this, f);
1698  }
1699 
1700  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
1701  check_context(d1, range); check_context(d2, range); check_context(d3, range);
1702  Z3_sort args[3] = { d1, d2, d3 };
1703  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
1704  check_error();
1705  return func_decl(*this, f);
1706  }
1707 
1708  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
1709  check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range);
1710  Z3_sort args[4] = { d1, d2, d3, d4 };
1711  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
1712  check_error();
1713  return func_decl(*this, f);
1714  }
1715 
1716  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) {
1717  check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range); check_context(d5, range);
1718  Z3_sort args[5] = { d1, d2, d3, d4, d5 };
1719  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
1720  check_error();
1721  return func_decl(*this, f);
1722  }
1723 
1724  inline expr context::constant(symbol const & name, sort const & s) {
1725  Z3_ast r = Z3_mk_const(m_ctx, name, s);
1726  check_error();
1727  return expr(*this, r);
1728  }
1729  inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); }
1730  inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); }
1731  inline expr context::int_const(char const * name) { return constant(name, int_sort()); }
1732  inline expr context::real_const(char const * name) { return constant(name, real_sort()); }
1733  inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); }
1734 
1735  inline expr context::bool_val(bool b) { return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }
1736 
1737  inline expr context::int_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
1738  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); }
1739  inline expr context::int_val(__int64 n) { Z3_ast r = Z3_mk_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
1740  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); }
1741  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); }
1742 
1743  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); }
1744  inline expr context::real_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
1745  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); }
1746  inline expr context::real_val(__int64 n) { Z3_ast r = Z3_mk_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
1747  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); }
1748  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); }
1749 
1750  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); }
1751  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); }
1752  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); }
1753  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); }
1754  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); }
1755 
1756  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); }
1757 
1758  inline expr func_decl::operator()(unsigned n, expr const * args) const {
1759  array<Z3_ast> _args(n);
1760  for (unsigned i = 0; i < n; i++) {
1761  check_context(*this, args[i]);
1762  _args[i] = args[i];
1763  }
1764  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
1765  check_error();
1766  return expr(ctx(), r);
1767 
1768  }
1769  inline expr func_decl::operator()(expr_vector const& args) const {
1770  array<Z3_ast> _args(args.size());
1771  for (unsigned i = 0; i < args.size(); i++) {
1772  check_context(*this, args[i]);
1773  _args[i] = args[i];
1774  }
1775  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
1776  check_error();
1777  return expr(ctx(), r);
1778  }
1779  inline expr func_decl::operator()() const {
1780  Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
1781  ctx().check_error();
1782  return expr(ctx(), r);
1783  }
1784  inline expr func_decl::operator()(expr const & a) const {
1785  check_context(*this, a);
1786  Z3_ast args[1] = { a };
1787  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
1788  ctx().check_error();
1789  return expr(ctx(), r);
1790  }
1791  inline expr func_decl::operator()(int a) const {
1792  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
1793  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
1794  ctx().check_error();
1795  return expr(ctx(), r);
1796  }
1797  inline expr func_decl::operator()(expr const & a1, expr const & a2) const {
1798  check_context(*this, a1); check_context(*this, a2);
1799  Z3_ast args[2] = { a1, a2 };
1800  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
1801  ctx().check_error();
1802  return expr(ctx(), r);
1803  }
1804  inline expr func_decl::operator()(expr const & a1, int a2) const {
1805  check_context(*this, a1);
1806  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
1807  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
1808  ctx().check_error();
1809  return expr(ctx(), r);
1810  }
1811  inline expr func_decl::operator()(int a1, expr const & a2) const {
1812  check_context(*this, a2);
1813  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
1814  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
1815  ctx().check_error();
1816  return expr(ctx(), r);
1817  }
1818  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3) const {
1819  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
1820  Z3_ast args[3] = { a1, a2, a3 };
1821  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
1822  ctx().check_error();
1823  return expr(ctx(), r);
1824  }
1825  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const {
1826  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
1827  Z3_ast args[4] = { a1, a2, a3, a4 };
1828  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
1829  ctx().check_error();
1830  return expr(ctx(), r);
1831  }
1832  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const {
1833  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
1834  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
1835  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
1836  ctx().check_error();
1837  return expr(ctx(), r);
1838  }
1839 
1840  inline expr to_real(expr const & a) { Z3_ast r = Z3_mk_int2real(a.ctx(), a); a.check_error(); return expr(a.ctx(), r); }
1841 
1842  inline func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
1843  return range.ctx().function(name, arity, domain, range);
1844  }
1845  inline func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range) {
1846  return range.ctx().function(name, arity, domain, range);
1847  }
1848  inline func_decl function(char const * name, sort const & domain, sort const & range) {
1849  return range.ctx().function(name, domain, range);
1850  }
1851  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range) {
1852  return range.ctx().function(name, d1, d2, range);
1853  }
1854  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
1855  return range.ctx().function(name, d1, d2, d3, range);
1856  }
1857  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
1858  return range.ctx().function(name, d1, d2, d3, d4, range);
1859  }
1860  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) {
1861  return range.ctx().function(name, d1, d2, d3, d4, d5, range);
1862  }
1863 
1864  inline expr select(expr const & a, expr const & i) {
1865  check_context(a, i);
1866  Z3_ast r = Z3_mk_select(a.ctx(), a, i);
1867  a.check_error();
1868  return expr(a.ctx(), r);
1869  }
1870  inline expr select(expr const & a, int i) { return select(a, a.ctx().num_val(i, a.get_sort().array_domain())); }
1871  inline expr store(expr const & a, expr const & i, expr const & v) {
1872  check_context(a, i); check_context(a, v);
1873  Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
1874  a.check_error();
1875  return expr(a.ctx(), r);
1876  }
1877  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); }
1878  inline expr store(expr const & a, expr i, int v) { return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
1879  inline expr store(expr const & a, int i, int v) {
1880  return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
1881  }
1882  inline expr const_array(sort const & d, expr const & v) {
1883  check_context(d, v);
1884  Z3_ast r = Z3_mk_const_array(d.ctx(), d, v);
1885  d.check_error();
1886  return expr(d.ctx(), r);
1887  }
1888 
1889  inline expr expr::substitute(expr_vector const& src, expr_vector const& dst) {
1890  assert(src.size() == dst.size());
1891  array<Z3_ast> _src(src.size());
1892  array<Z3_ast> _dst(dst.size());
1893  for (unsigned i = 0; i < src.size(); ++i) {
1894  _src[i] = src[i];
1895  _dst[i] = dst[i];
1896  }
1897  Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
1898  check_error();
1899  return expr(ctx(), r);
1900  }
1901 
1902  inline expr expr::substitute(expr_vector const& dst) {
1903  array<Z3_ast> _dst(dst.size());
1904  for (unsigned i = 0; i < dst.size(); ++i) {
1905  _dst[i] = dst[i];
1906  }
1907  Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
1908  check_error();
1909  return expr(ctx(), r);
1910  }
1911 
1912 
1913 
1914 };
1915 
1918 
1919 #endif
1920 
Z3_probe Z3_API Z3_probe_and(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when p1 and p2 evaluates to true.
ast_vector_tpl(context &c)
Definition: z3++.h:1025
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
expr distinct(expr_vector const &args)
Definition: z3++.h:1109
Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
System.IntPtr Z3_optimize
Definition: Native.cs:36
void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s)
Increment the reference counter of the given statistics object.
Z3_ast Z3_API Z3_mk_true(Z3_context c)
Create an AST node representing true.
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).The distinct construct is us...
Z3_probe Z3_API Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the va...
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:194
Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)
Create a bit-vector type of the given size.
friend expr operator|(expr const &a, expr const &b)
Definition: z3++.h:870
System.IntPtr Z3_stats
Definition: Native.cs:29
void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value)
Set a global (or module) parameter. This setting is shared by all Z3 contexts.
std::string reason_unknown() const
Definition: z3++.h:1327
std::string help() const
Definition: z3++.h:1458
sort bool_sort()
Return the Boolean sort.
Definition: z3++.h:1629
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.
friend expr operator+(expr const &a, expr const &b)
Definition: z3++.h:684
Z3_string Z3_API Z3_apply_result_to_string(Z3_context c, Z3_apply_result r)
Convert the Z3_apply_result object returned by Z3_tactic_apply into a string.
Z3_bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g)
Return true if the given goal contains the formula false.
friend expr operator>=(expr const &a, int b)
Definition: z3++.h:821
bool is_int() const
Return true if this sort is the Integer sort.
Definition: z3++.h:377
Z3_ast Z3_API Z3_mk_false(Z3_context c)
Create an AST node representing false.
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas as a goal object.
Z3_probe Z3_API Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than or equal to the...
tactic & operator=(tactic const &s)
Definition: z3++.h:1441
probe(context &c, Z3_probe s)
Definition: z3++.h:1503
void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g)
Erase all formulas from the given goal.
probe & operator=(probe const &s)
Definition: z3++.h:1507
Z3_tactic Z3_API Z3_tactic_when(Z3_context c, Z3_probe p, 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...
func_decl get_const_decl(unsigned i) const
Definition: z3++.h:1202
Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned 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 Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t)
Increment the reference counter of the given tactic.
friend expr operator>=(expr const &a, expr const &b)
Definition: z3++.h:805
bool is_array() const
Return true if this is a Array expression.
Definition: z3++.h:500
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d)
Return the constant declaration name as a symbol.
System.IntPtr Z3_probe
Definition: Native.cs:28
friend probe operator<(probe const &p1, double p2)
Definition: z3++.h:1529
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:1626
void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f)
Increment the reference counter of the given Z3_func_interp object.
friend expr operator<=(expr const &a, int b)
Definition: z3++.h:802
Z3_params Z3_API Z3_mk_params(Z3_context c)
Create a Z3 (empty) parameter set. Starting at Z3 4.0, parameter sets are used to configure many comp...
Z3_tactic Z3_API Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1...
Z3_symbol_kind Z3_API Z3_get_symbol_kind(Z3_context c, Z3_symbol s)
Return Z3_INT_SYMBOL if the symbol was constructed using Z3_mk_int_symbol, and Z3_STRING_SYMBOL if th...
void Z3_API Z3_ast_vector_inc_ref(Z3_context c, Z3_ast_vector v)
Increment the reference counter of the given AST vector.
void push()
Definition: z3++.h:1292
System.IntPtr Z3_goal
Definition: Native.cs:25
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.
stats statistics() const
Definition: z3++.h:1328
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
tactic cond(probe const &p, tactic const &t1, tactic const &t2)
Definition: z3++.h:1619
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing -arg.The arguments must have int or real type.
void Z3_API Z3_params_set_uint(Z3_context c, Z3_params p, Z3_symbol k, unsigned v)
Add a unsigned parameter k with value v to the parameter set p.
expr(context &c)
Definition: z3++.h:467
char const * msg() const
Definition: z3++.h:84
expr bv_val(int n, unsigned sz)
Definition: z3++.h:1750
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed greater than.
Z3_model Z3_API Z3_apply_result_convert_model(Z3_context c, Z3_apply_result r, unsigned i, Z3_model m)
Convert a model for the subgoal Z3_apply_result_get_subgoal(c, r, i) into a model for the original go...
expr value() const
Definition: z3++.h:1143
Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o)
Check consistency and produce optimal values.
Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i)
Return the declaration of the i-th function in the given model.
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
bool is_real() const
Return true if this is a real expression.
Definition: z3++.h:488
Definition: z3_api.h:1313
func_interp & operator=(func_interp const &s)
Definition: z3++.h:1159
friend expr operator!=(expr const &a, expr const &b)
Definition: z3++.h:674
Z3_probe Z3_API Z3_probe_gt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than the value retur...
probe(context &c, double val)
Definition: z3++.h:1502
expr select(expr const &a, expr const &i)
Definition: z3++.h:1864
Definition: z3++.h:1255
std::string help() const
Definition: z3++.h:1605
Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v)
Array update.
func_entry & operator=(func_entry const &s)
Definition: z3++.h:1136
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
Z3_ast Z3_API Z3_ast_vector_get(Z3_context c, Z3_ast_vector v, unsigned i)
Return the AST at position i in the AST vector v.
Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name)
Return a tactic associated with the given name. The complete list of tactics may be obtained using th...
tactic when(probe const &p, tactic const &t)
Definition: z3++.h:1613
Z3_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.
config()
Definition: z3++.h:98
friend std::ostream & operator<<(std::ostream &out, params const &p)
Definition: z3++.h:321
void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s)
Decrement the reference counter of the given statistics object.
Z3_sort Z3_API Z3_get_array_sort_range(Z3_context c, Z3_sort t)
Return the range of the given array sort.
expr lower(handle const &h)
Definition: z3++.h:1593
friend expr operator/(expr const &a, expr const &b)
Definition: z3++.h:731
Z3_probe Z3_API Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned ...
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
Z3_ast Z3_API Z3_mk_int64(Z3_context c, __int64 v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
array(unsigned sz)
Definition: z3++.h:260
Z3_solver Z3_API Z3_mk_solver(Z3_context c)
Create a new (incremental) solver. This solver also uses a set of builtin tactics for handling the fi...
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:355
~solver()
Definition: z3++.h:1282
Z3_ast Z3_API Z3_substitute(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const from[], 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].
expr simplify() const
Return a simplified version of this expression.
Definition: z3++.h:882
unsigned bv_size() const
Return the size of this Bit-vector sort.
Definition: z3++.h:412
bool is_bv() const
Return true if this sort is a Bit-vector sort.
Definition: z3++.h:389
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than.
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)
Create a new optimize context.
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.
func_decl(context &c)
Definition: z3++.h:434
int to_int() const
Definition: z3++.h:292
friend expr operator^(expr const &a, expr const &b)
Definition: z3++.h:866
~array()
Definition: z3++.h:263
void pop_back()
Definition: z3++.h:1035
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
friend std::ostream & operator<<(std::ostream &out, ast const &n)
Definition: z3++.h:339
Z3_goal Z3_API Z3_mk_goal(Z3_context c, Z3_bool models, Z3_bool unsat_cores, Z3_bool proofs)
Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or trans...
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:1632
Z3_func_decl Z3_API Z3_model_get_const_decl(Z3_context c, Z3_model m, unsigned i)
Return the i-th constant in the given model.
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:1248
expr udiv(expr const &a, expr const &b)
unsigned division operator for bitvectors.
Definition: z3++.h:982
apply_result operator()(goal const &g) const
Definition: z3++.h:1455
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
bool empty() const
Definition: z3++.h:1036
T back() const
Definition: z3++.h:1034
solver mk_solver() const
Definition: z3++.h:1448
expr upper(handle const &h)
Definition: z3++.h:1598
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1385
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1311
goal(context &c, Z3_goal s)
Definition: z3++.h:1363
Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned 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 ...
expr eval(expr const &n, bool model_completion=false) const
Definition: z3++.h:1190
model(context &c, Z3_model m)
Definition: z3++.h:1178
sort array_sort(sort d, sort r)
Return an array sort for arrays from d to r.
Definition: z3++.h:1633
Z3_ast_kind kind() const
Definition: z3++.h:337
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:1724
friend probe operator>(double p1, probe const &p2)
Definition: z3++.h:1535
void pop()
Definition: z3++.h:1587
Z3_ast Z3_API Z3_func_entry_get_arg(Z3_context c, Z3_func_entry e, unsigned i)
Return an argument of a Z3_func_entry object.
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:110
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)
Return the number of parameters associated with a declaration.
func_decl operator[](int i) const
Definition: z3++.h:1205
Z3_bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
compare terms.
System.IntPtr Z3_func_entry
Definition: Native.cs:34
friend probe operator>=(probe const &p1, double p2)
Definition: z3++.h:1524
Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than or equal to.
friend expr operator/(expr const &a, int b)
Definition: z3++.h:747
Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name)
Return a probe associated with the given name. The complete list of probes may be obtained using the ...
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:648
Z3_string Z3_API Z3_ast_vector_to_string(Z3_context c, Z3_ast_vector v)
Convert AST vector into a string.
tactic(tactic const &s)
Definition: z3++.h:1438
friend expr operator||(expr const &a, expr const &b)
Return an expression representing a or b.
Definition: z3++.h:627
~probe()
Definition: z3++.h:1505
Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic)
Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unkn...
bool is_datatype() const
Return true if this is a Datatype expression.
Definition: z3++.h:504
Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d)
Return declaration kind corresponding to declaration.
~tactic()
Definition: z3++.h:1439
sort operator()(context &c, Z3_ast a)
Definition: z3++.h:1006
check_result check()
Definition: z3++.h:1590
friend probe operator||(probe const &p1, probe const &p2)
Definition: z3++.h:1544
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.
Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s)
Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.
friend expr operator*(int a, expr const &b)
Definition: z3++.h:722
Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[])
Check whether the assertions in the given solver and optional assumptions are consistent or not...
friend std::ostream & operator<<(std::ostream &out, optimize const &s)
Definition: z3++.h:1604
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)
Create the constant array.
Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned 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...
unsigned lo() const
Definition: z3++.h:876
Exception used to sign API usage errors.
Definition: z3++.h:80
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
unsigned uint_value(unsigned i) const
Definition: z3++.h:1249
Z3_context Z3_API Z3_mk_context_rc(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_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.
ast_vector_tpl(context &c, Z3_ast_vector v)
Definition: z3++.h:1026
A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort ...
Definition: z3++.h:465
void reset_params()
Definition: z3++.h:75
void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value)
Set a value of a context parameter.
#define __uint64
Definition: z3_api.h:66
def is_app(a)
Definition: z3py.py:981
expr & operator=(expr const &n)
Definition: z3++.h:470
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
unsigned num_exprs() const
Definition: z3++.h:1381
bool is_uint(unsigned i) const
Definition: z3++.h:1247
expr ule(expr const &a, expr const &b)
unsigned less than or equal to operator for bitvectors.
Definition: z3++.h:958
void Z3_API Z3_ast_vector_resize(Z3_context c, Z3_ast_vector v, unsigned n)
Resize the AST vector v.
expr_vector unsat_core() const
Definition: z3++.h:1329
Z3_string Z3_API Z3_stats_get_key(Z3_context c, Z3_stats s, unsigned idx)
Return the key (a string) for a particular statistical data.
Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i)
Return the i-th argument of the given application.
unsigned num_entries() const
Definition: z3++.h:1167
unsigned arity() const
Definition: z3++.h:440
bool is_finite_domain() const
Return true if this sort is a Finite domain sort.
Definition: z3++.h:405
System.IntPtr Z3_sort
Definition: Native.cs:15
friend probe operator>(probe const &p1, double p2)
Definition: z3++.h:1534
func_decl operator()(context &c, Z3_ast a)
Definition: z3++.h:1014
void Z3_API Z3_func_interp_dec_ref(Z3_context c, Z3_func_interp f)
Decrement the reference counter of the given Z3_func_interp object.
ast_vector_tpl< func_decl > func_decl_vector
Definition: z3++.h:70
stats(context &c)
Definition: z3++.h:1233
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.
void Z3_API Z3_ast_vector_dec_ref(Z3_context c, Z3_ast_vector v)
Decrement the reference counter of the given AST vector.
expr pw(expr const &a, expr const &b)
Definition: z3++.h:903
Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)
Return the declaration of a constant or function application.
friend std::ostream & operator<<(std::ostream &out, goal const &g)
Definition: z3++.h:1397
friend probe operator>=(probe const &p1, probe const &p2)
Definition: z3++.h:1521
expr(context &c, Z3_ast n)
Definition: z3++.h:468
~goal()
Definition: z3++.h:1365
unsigned Z3_API Z3_ast_vector_size(Z3_context c, Z3_ast_vector v)
Return the size of the given AST vector.
friend expr operator^(expr const &a, int b)
Definition: z3++.h:867
expr operator[](int i) const
Definition: z3++.h:1376
friend expr operator-(expr const &a, expr const &b)
Definition: z3++.h:766
friend expr operator-(expr const &a)
Definition: z3++.h:750
Z3_error_code Z3_API Z3_get_error_code(Z3_context c)
Return the error code for the last API call.
check_result check(unsigned n, expr *const assumptions)
Definition: z3++.h:1305
check_result check(expr_vector assumptions)
Definition: z3++.h:1315
friend expr operator*(expr const &a, int b)
Definition: z3++.h:721
friend expr operator&(expr const &a, int b)
Definition: z3++.h:863
friend expr operator*(expr const &a, expr const &b)
Definition: z3++.h:704
probe(context &c, char const *name)
Definition: z3++.h:1501
friend std::ostream & operator<<(std::ostream &out, solver const &s)
Definition: z3++.h:1332
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed less than.
~stats()
Definition: z3++.h:1236
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
def substitute(t, m)
Definition: z3py.py:7210
friend expr operator<=(expr const &a, expr const &b)
Definition: z3++.h:786
Z3_tactic Z3_API Z3_tactic_or_else(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that first applies t1 to a given goal, if it fails then returns the result of t2 appl...
expr get_const_interp(func_decl c) const
Definition: z3++.h:1210
Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s)
Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.
Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve upper bound value or approximation for the i&#39;th optimization objective.
A Context manages all other Z3 objects, global configuration options, etc.
Definition: z3++.h:122
Definition: z3++.h:326
Z3 C++ namespace.
Definition: z3++.h:45
Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.
void Z3_API Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode)
Select mode for the format used for pretty-printing AST nodes.
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.
friend tactic operator|(tactic const &t1, tactic const &t2)
Definition: z3++.h:1465
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed division.
def is_array(a)
Definition: z3py.py:3927
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:886
Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p)
Return a probe that evaluates to "true" when p does not evaluate to true.
friend expr operator&(int a, expr const &b)
Definition: z3++.h:864
solver(context &c, Z3_solver s)
Definition: z3++.h:1279
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
Z3 global configuration object.
Definition: z3++.h:93
solver & operator=(solver const &s)
Definition: z3++.h:1284
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:1889
ast(context &c, Z3_ast n)
Definition: z3++.h:331
ast_vector_tpl & operator=(ast_vector_tpl const &s)
Definition: z3++.h:1037
handle add(expr const &e, char const *weight)
Definition: z3++.h:1574
friend std::ostream & operator<<(std::ostream &out, apply_result const &r)
Definition: z3++.h:1426
bool is_finite_domain() const
Return true if this is a Finite-domain expression.
Definition: z3++.h:517
expr proof() const
Definition: z3++.h:1331
expr bv_const(char const *name, unsigned sz)
Definition: z3++.h:1733
Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f)
Return the &#39;else&#39; value of the given function interpretation.
tactic(context &c, char const *name)
Definition: z3++.h:1436
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.The arguments must either both have int type or both ha...
Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, unsigned __int64 v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p)
Increment the reference counter of the given probe.
std::string str() const
Definition: z3++.h:291
tactic with(tactic const &t, params const &p)
Definition: z3++.h:1482
Z3_ast_vector Z3_API Z3_mk_ast_vector(Z3_context c)
Return an empty AST vector.
System.IntPtr Z3_func_decl
Definition: Native.cs:16
Z3_bool Z3_API Z3_goal_is_decided_sat(Z3_context c, Z3_goal g)
Return true if the goal is empty, and it is precise or the product of a under approximation.
void reset()
Definition: z3++.h:1294
friend expr operator<=(int a, expr const &b)
Definition: z3++.h:803
Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1)
Coerce an integer to a real.
~config()
Definition: z3++.h:99
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
sort array_domain() const
Return the domain of this Array sort.
Definition: z3++.h:419
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:222
unsigned Z3_API Z3_goal_depth(Z3_context c, Z3_goal g)
Return the depth of the given goal. It tracks how many transformations were applied to it...
void Z3_API Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r)
Increment the reference counter of the given Z3_apply_result object.
void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e)
Increment the reference counter of the given Z3_func_entry object.
void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a)
Decrement the reference counter of the given AST. The context c should have been created using Z3_mk_...
func_entry(context &c, Z3_func_entry e)
Definition: z3++.h:1132
void resize(unsigned sz)
Definition: z3++.h:1033
void Z3_API Z3_del_config(Z3_config c)
Delete the given configuration object.
bool is_var() const
Return true if this expression is a variable.
Definition: z3++.h:538
expr extract(unsigned hi, unsigned lo) const
Definition: z3++.h:875
void add(expr const &e, char const *p)
Definition: z3++.h:1301
func_decl to_func_decl(context &c, Z3_func_decl f)
Definition: z3++.h:950
unsigned depth() const
Definition: z3++.h:1379
optimize(context &c)
Definition: z3++.h:1561
BEGIN_MLAPI_EXCLUDE Z3_string Z3_API Z3_get_error_msg_ex(Z3_context c, Z3_error_code err)
Return a string describing the given error code.
context & ctx() const
Definition: z3++.h:277
sort array_range() const
Return the range of this Array sort.
Definition: z3++.h:425
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)
Create a backtracking point.
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
expr(expr const &n)
Definition: z3++.h:469
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned 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...
Z3_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned 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_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
unsigned Z3_API Z3_get_bv_sort_size(Z3_context c, Z3_sort t)
Return the size of the given bit-vector sort.
Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve lower bound value or approximation for the i&#39;th optimization objective.
Definition: z3++.h:1125
bool is_const() const
Definition: z3++.h:446
Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)
Create an array type.
check_result check()
Definition: z3++.h:1304
unsigned size() const
Definition: z3++.h:1418
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.
std::string to_smt2(char const *status="unknown")
Definition: z3++.h:1334
Z3_goal_prec Z3_API Z3_goal_precision(Z3_context c, Z3_goal g)
Return the "precision" of the given goal. Goals can be transformed using over and under approximation...
func_decl get_func_decl(unsigned i) const
Definition: z3++.h:1203
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:1653
expr operator()(context &c, Z3_ast a)
Definition: z3++.h:995
Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed greater than or equal to.
friend probe operator!(probe const &p)
Definition: z3++.h:1547
expr as_expr() const
Definition: z3++.h:1384
bool is_numeral() const
Return true if this expression is a numeral.
Definition: z3++.h:522
Z3_ast Z3_API Z3_mk_real(Z3_context c, int num, int den)
Create a real from a fraction.
unsigned Z3_API Z3_get_ast_hash(Z3_context c, Z3_ast a)
Return a hash code for the given AST. The hash code is structural. You can use Z3_get_ast_id intercha...
def is_real(a)
Definition: z3py.py:2262
Z3_string Z3_API Z3_params_to_string(Z3_context c, Z3_params p)
Convert a parameter set into a string. This function is mainly used for printing the contents of a pa...
unsigned h() const
Definition: z3++.h:1559
Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed less than or equal to.
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.
Z3_ast Z3_API Z3_mk_exists_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Similar to Z3_mk_forall_const.
exception(char const *msg)
Definition: z3++.h:83
solver(solver const &s)
Definition: z3++.h:1281
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:143
~optimize()
Definition: z3++.h:1562
unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a)
Return the number of argument of an application. If t is an constant, then the number of arguments is...
friend expr operator!=(expr const &a, int b)
Definition: z3++.h:681
#define __int64
Definition: z3_api.h:62
void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g)
Decrement the reference counter of the given goal.
expr real_val(int n, int d)
Definition: z3++.h:1743
ast_vector_tpl< sort > sort_vector
Definition: z3++.h:69
void add(expr const &e)
Definition: z3++.h:1564
void check_error() const
Definition: z3++.h:278
void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h)
Register a Z3 error handler.
func_interp(func_interp const &s)
Definition: z3++.h:1156
Z3_decl_kind decl_kind() const
Definition: z3++.h:444
Z3_func_interp Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f)
Return the interpretation of the function f in the model m. Return NULL, if the model does not assign...
model & operator=(model const &s)
Definition: z3++.h:1182
friend expr operator-(int a, expr const &b)
Definition: z3++.h:784
void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m)
Decrement the reference counter of the given model.
friend expr operator==(expr const &a, expr const &b)
Definition: z3++.h:665
unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m)
Return the number of constants assigned by the given model.
stats statistics() const
Definition: z3++.h:1603
func_entry entry(unsigned i) const
Definition: z3++.h:1168
Z3_ast Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a)
Return the interpretation (i.e., assignment) of constant a in the model m. Return NULL...
void add(expr const &e)
Definition: z3++.h:1295
bool is_relation() const
Return true if this is a Relation expression.
Definition: z3++.h:508
unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g)
Return the number of formulas in the given goal.
bool is_bool() const
Return true if this sort is the Boolean sort.
Definition: z3++.h:373
expr ugt(expr const &a, expr const &b)
unsigned greater than operator for bitvectors.
Definition: z3++.h:976
goal & operator=(goal const &s)
Definition: z3++.h:1367
~params()
Definition: z3++.h:308
Z3_sort Z3_API Z3_get_array_sort_domain(Z3_context c, Z3_sort t)
Return the domain of the given array sort.
expr const_array(sort const &d, expr const &v)
Definition: z3++.h:1882
Z3_bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx)
Return Z3_TRUE if the given statistical data is a unsigned integer.
stats(stats const &s)
Definition: z3++.h:1235
T const * ptr() const
Definition: z3++.h:267
def is_int(a)
Definition: z3py.py:2244
def is_quantifier(a)
Definition: z3py.py:1769
friend std::ostream & operator<<(std::ostream &out, model const &m)
Definition: z3++.h:1223
int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s)
Return the symbol int value.
void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p)
Decrement the reference counter of the given parameter set.
~func_entry()
Definition: z3++.h:1134
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)
Decrement the reference counter of the given optimize context.
sort uninterpreted_sort(char const *name)
create an uninterpreted sort with the name given by the string or symbol.
Definition: z3++.h:1645
double Z3_API Z3_probe_apply(Z3_context c, Z3_probe p, Z3_goal g)
Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0...
Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s)
Retrieve the unsat core for the last Z3_solver_check_assumptions The unsat core is a subset of the as...
goal operator[](int i) const
Definition: z3++.h:1419
friend expr operator<(expr const &a, int b)
Definition: z3++.h:840
friend probe operator==(probe const &p1, double p2)
Definition: z3++.h:1539
void reset()
Definition: z3++.h:1380
T * ptr()
Definition: z3++.h:268
friend expr operator<(int a, expr const &b)
Definition: z3++.h:841
params(params const &s)
Definition: z3++.h:307
Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e)
Return the value of this point.
unsigned Z3_API Z3_stats_get_uint_value(Z3_context c, Z3_stats s, unsigned idx)
Return the unsigned value of the given statistical data.
void set_param(char const *param, char const *value)
Definition: z3++.h:72
unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id)
Assert soft constraint to the optimization context.
Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than.
Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g)
Convert a goal into a string.
handle maximize(expr const &e)
Definition: z3++.h:1578
unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m)
Return the number of function interpretations in the given model.
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:553
unsigned size() const
Definition: z3++.h:1030
friend probe operator<=(probe const &p1, probe const &p2)
Definition: z3++.h:1516
friend expr operator&&(expr const &a, expr const &b)
Return an expression representing a and b.
Definition: z3++.h:596
expr int_const(char const *name)
Definition: z3++.h:1731
friend expr operator&(expr const &a, expr const &b)
Definition: z3++.h:862
friend std::ostream & operator<<(std::ostream &out, exception const &e)
Definition: z3++.h:85
expr arg(unsigned i) const
Definition: z3++.h:1145
symbol(symbol const &s)
Definition: z3++.h:287
Z3_bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, Z3_bool model_completion, Z3_ast *v)
Evaluate the AST node t in the given model. Return Z3_TRUE if succeeded, and store the result in v...
unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e)
Return the number of arguments in a Z3_func_entry object.
unsigned num_args() const
Return the number of arguments in this application. This method assumes the expression is an applicat...
Definition: z3++.h:560
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:158
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
sort(context &c)
Definition: z3++.h:357
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:612
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)
Retrieve the model for the last Z3_optimize_check.
goal(context &c, bool models=true, bool unsat_cores=false, bool proofs=false)
Definition: z3++.h:1362
System.IntPtr Z3_apply_result
Definition: Native.cs:32
void Z3_API Z3_interrupt(Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers...
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:526
friend tactic operator&(tactic const &t1, tactic const &t2)
Definition: z3++.h:1459
object(context &c)
Definition: z3++.h:275
friend expr operator>(expr const &a, expr const &b)
Definition: z3++.h:843
unsigned size() const
Definition: z3++.h:1375
handle add(expr const &e, unsigned weight)
Definition: z3++.h:1568
ast(context &c)
Definition: z3++.h:330
Z3_symbol_kind kind() const
Definition: z3++.h:290
object(object const &s)
Definition: z3++.h:276
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
friend expr operator!=(int a, expr const &b)
Definition: z3++.h:682
expr real_const(char const *name)
Definition: z3++.h:1732
friend probe operator<=(double p1, probe const &p2)
Definition: z3++.h:1520
friend expr operator/(int a, expr const &b)
Definition: z3++.h:748
model get_model() const
Definition: z3++.h:1591
friend expr operator>(int a, expr const &b)
Definition: z3++.h:860
func_interp get_func_interp(func_decl f) const
Definition: z3++.h:1216
friend probe operator==(probe const &p1, probe const &p2)
Definition: z3++.h:1536
friend probe operator>=(double p1, probe const &p2)
Definition: z3++.h:1525
Z3_tactic Z3_API Z3_tactic_using_params(Z3_context c, Z3_tactic t, Z3_params p)
Return a tactic that applies t using the given set of parameters.
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.
Z3_sort_kind sort_kind() const
Return the internal sort kind.
Definition: z3++.h:368
bool is_arith() const
Return true if this sort is the Integer or Real sort.
Definition: z3++.h:385
Z3_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s)
Check whether the assertions in a given solver are consistent or not.
System.IntPtr Z3_solver
Definition: Native.cs:24
Z3_sort Z3_API Z3_get_domain(Z3_context c, Z3_func_decl d, unsigned i)
Return the sort of the i-th parameter of the given function declaration.
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.
Z3_sort Z3_API Z3_mk_real_sort(Z3_context c)
Create the real type.
model convert_model(model const &m, unsigned i=0) const
Definition: z3++.h:1420
bool is_well_sorted() const
Return true if this expression is well sorted (aka type correct).
Definition: z3++.h:543
Z3_config Z3_API Z3_mk_config(void)
Create a configuration object for the Z3 context object.
symbol & operator=(symbol const &s)
Definition: z3++.h:288
~model()
Definition: z3++.h:1180
sort real_sort()
Return the Real sort.
Definition: z3++.h:1631
unsigned Z3_API Z3_goal_num_exprs(Z3_context c, Z3_goal g)
Return the number of formulas, subformulas and terms in the given goal.
System.IntPtr Z3_app
Definition: Native.cs:14
friend std::ostream & operator<<(std::ostream &out, ast_vector_tpl const &v)
Definition: z3++.h:1044
Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d)
Return the range of the given declaration.
bool inconsistent() const
Definition: z3++.h:1378
bool is_const() const
Return true if this expression is a constant (i.e., an application with 0 arguments).
Definition: z3++.h:530
expr arg(unsigned i) const
Return the i-th argument of this application. This method assumes the expression is an application...
Definition: z3++.h:568
ast_vector_tpl(ast_vector_tpl const &s)
Definition: z3++.h:1027
expr num_val(int n, sort const &s)
Definition: z3++.h:1756
bool eq(ast const &a, ast const &b)
Definition: z3++.h:349
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.
symbol int_symbol(int n)
Create a Z3 symbol based on the given integer.
Definition: z3++.h:1627
unsigned num_consts() const
Definition: z3++.h:1200
Z3_tactic Z3_API Z3_tactic_repeat(Z3_context c, 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_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d)
Retrieve statistics information from the last call to Z3_optimize_check.
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
friend probe operator>(probe const &p1, probe const &p2)
Definition: z3++.h:1531
void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p)
Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p...
friend probe operator<(double p1, probe const &p2)
Definition: z3++.h:1530
unsigned num_funcs() const
Definition: z3++.h:1201
expr operator()() const
Definition: z3++.h:1779
friend probe operator==(double p1, probe const &p2)
Definition: z3++.h:1540
Z3_tactic Z3_API Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, 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...
Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] - ... - args[num_args - 1].The array args must have num_args ...
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:1265
friend expr operator~(expr const &a)
Definition: z3++.h:874
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1^arg2.
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
Z3_tactic Z3_API Z3_tactic_try_for(Z3_context c, Z3_tactic t, unsigned ms)
Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms mil...
void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value)
Set a configuration parameter.
Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s)
Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the commands Z3_solver_ch...
T operator[](int i) const
Definition: z3++.h:1031
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
tactic(context &c, Z3_tactic s)
Definition: z3++.h:1437
void check_context(object const &a, object const &b)
Definition: z3++.h:281
Z3_probe Z3_API Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned...
expr bool_const(char const *name)
Definition: z3++.h:1730
void Z3_API Z3_params_set_double(Z3_context c, Z3_params p, Z3_symbol k, double v)
Add a double parameter k with value v to the parameter set p.
void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a)
Add a new formula a to the given goal.
Z3_tactic Z3_API Z3_tactic_fail_if(Z3_context c, Z3_probe p)
Return a tactic that fails if the probe p evaluates to false.
double apply(goal const &g) const
Definition: z3++.h:1514
Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize t)
Return a string containing a description of parameters accepted by optimize.
Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s)
Return the symbol name.
System.IntPtr Z3_context
Definition: Native.cs:12
Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i)
Return one of the subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
params & operator=(params const &s)
Definition: z3++.h:310
friend std::ostream & operator<<(std::ostream &out, symbol const &s)
Definition: z3++.h:293
Z3_sort_kind Z3_API Z3_get_sort_kind(Z3_context c, Z3_sort t)
Return the sort kind (e.g., array, tuple, int, bool, etc).
model(model const &s)
Definition: z3++.h:1179
unsigned hi() const
Definition: z3++.h:877
probe(probe const &s)
Definition: z3++.h:1504
friend expr operator>(expr const &a, int b)
Definition: z3++.h:859
friend expr operator<(expr const &a, expr const &b)
Definition: z3++.h:824
friend expr operator!(expr const &a)
Return an expression representing not(a).
Definition: z3++.h:582
Z3_goal_prec precision() const
Definition: z3++.h:1377
solver(context &c)
Definition: z3++.h:1278
void Z3_API Z3_apply_result_dec_ref(Z3_context c, Z3_apply_result r)
Decrement the reference counter of the given Z3_apply_result object.
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two&#39;s complement subtraction.
func_decl(context &c, Z3_func_decl n)
Definition: z3++.h:435
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
ast_vector_tpl< ast > ast_vector
Definition: z3++.h:66
bool is_decided_unsat() const
Definition: z3++.h:1383
Z3_ast Z3_API Z3_mk_int(Z3_context c, int v, Z3_sort ty)
Create a numeral of an int, bit-vector, or finite-domain sort.
System.IntPtr Z3_model
Definition: Native.cs:18
handle minimize(expr const &e)
Definition: z3++.h:1581
friend probe operator<(probe const &p1, probe const &p2)
Definition: z3++.h:1526
friend expr operator==(expr const &a, int b)
Definition: z3++.h:671
expr_vector assertions() const
Definition: z3++.h:1330
void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g)
Increment the reference counter of the given goal.
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:475
friend probe operator&&(probe const &p1, probe const &p2)
Definition: z3++.h:1541
void add(expr const &e, expr const &p)
Definition: z3++.h:1296
Z3_bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g)
Return true if the goal contains false, and it is precise or the product of an over approximation...
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.
expr store(expr const &a, expr const &i, expr const &v)
Definition: z3++.h:1871
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:141
std::string key(unsigned i) const
Definition: z3++.h:1246
bool is_relation() const
Return true if this sort is a Relation sort.
Definition: z3++.h:401
Z3_ast m_ast
Definition: z3++.h:328
Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned division.
tactic repeat(tactic const &t, unsigned max=UINT_MAX)
Definition: z3++.h:1476
expr bool_val(bool b)
Definition: z3++.h:1735
~context()
Definition: z3++.h:135
expr ult(expr const &a, expr const &b)
unsigned less than operator for bitvectors.
Definition: z3++.h:964
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:619
void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p)
Increment the reference counter of the given parameter set.
Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables...
Z3_string Z3_API Z3_tactic_get_help(Z3_context c, Z3_tactic t)
Return a string containing a description of parameters accepted by the given tactic.
void Z3_API Z3_params_set_symbol(Z3_context c, Z3_params p, Z3_symbol k, Z3_symbol v)
Add a symbol parameter k with value v to the parameter set p.
bool is_int() const
Return true if this is an integer expression.
Definition: z3++.h:484
apply_result apply(goal const &g) const
Definition: z3++.h:1449
expr int_val(int n)
Definition: z3++.h:1737
bool is_arith() const
Return true if this is an integer or real expression.
Definition: z3++.h:492
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...
void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m)
Increment the reference counter of the given model.
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a minimization constraint.
model get_model() const
Definition: z3++.h:1326
func_decl(func_decl const &s)
Definition: z3++.h:436
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
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:641
expr else_value() const
Definition: z3++.h:1166
tactic fail_if(probe const &p)
Definition: z3++.h:1608
stats(context &c, Z3_stats e)
Definition: z3++.h:1234
expr exists(expr const &x, expr const &b)
Definition: z3++.h:1083
ast operator()(context &c, Z3_ast a)
Definition: z3++.h:990
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two&#39;s complement multiplication.
context(config &c)
Definition: z3++.h:134
bool is_array() const
Return true if this sort is a Array sort.
Definition: z3++.h:393
unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f)
Return the number of entries in the given function interpretation.
friend expr operator-(expr const &a, int b)
Definition: z3++.h:783
expr ite(expr const &c, expr const &t, expr const &e)
Create the if-then-else expression ite(c, t, e)
Definition: z3++.h:923
T const & operator[](int i) const
Definition: z3++.h:266
func_entry(func_entry const &s)
Definition: z3++.h:1133
Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast t1)
Extract the bits high down to low from a bitvector of size m to yield a new bitvector of size n...
double double_value(unsigned i) const
Definition: z3++.h:1250
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two&#39;s complement unary minus.
expr body() const
Return the &#39;body&#39; of this quantifier.
Definition: z3++.h:575
~ast()
Definition: z3++.h:333
#define Z3_FALSE
False value. It is just an alias for 0.
Definition: z3_api.h:135
double Z3_API Z3_stats_get_double_value(Z3_context c, Z3_stats s, unsigned idx)
Return the double value of the given statistical data.
ast & operator=(ast const &s)
Definition: z3++.h:336
bool is_bv() const
Return true if this is a Bit-vector expression.
Definition: z3++.h:496
expr forall(expr const &x, expr const &b)
Definition: z3++.h:1059
sort domain(unsigned i) const
Definition: z3++.h:441
bool is_bool() const
Return true if this is a Boolean expression.
Definition: z3++.h:480
sort(context &c, Z3_sort s)
Definition: z3++.h:358
unsigned hash() const
Definition: z3++.h:338
double operator()(goal const &g) const
Definition: z3++.h:1515
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
bool is_datatype() const
Return true if this sort is a Datatype sort.
Definition: z3++.h:397
Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t)
Create a new solver that is implemented using the given tactic. The solver supports the commands Z3_s...
Z3_func_entry Z3_API Z3_func_interp_get_entry(Z3_context c, Z3_func_interp f, unsigned i)
Return a "point" of the given function intepretation. It represents the value of f in a particular po...
Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c, Z3_string name, Z3_string logic, Z3_string status, Z3_string attributes, unsigned num_assumptions, Z3_ast const assumptions[], Z3_ast formula)
Convert the given benchmark into SMT-LIB formatted string.
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:936
friend expr operator+(int a, expr const &b)
Definition: z3++.h:702
expr concat(expr const &a, expr const &b)
Definition: z3++.h:1118
symbol(context &c, Z3_symbol s)
Definition: z3++.h:286
int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the integer value associated with an integer parameter.
solver(context &c, char const *logic)
Definition: z3++.h:1280
tactic try_for(tactic const &t, unsigned ms)
Definition: z3++.h:1487
func_interp(context &c, Z3_func_interp e)
Definition: z3++.h:1155
unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d)
Alias for Z3_get_domain_size.
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.
params(context &c)
Definition: z3++.h:306
void push_back(T const &e)
Definition: z3++.h:1032
sort range() const
Definition: z3++.h:442
System.IntPtr Z3_ast_vector
Definition: Native.cs:30
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:68
void Z3_API Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, Z3_bool v)
Add a Boolean parameter k with value v to the parameter set p.
def is_bv(a)
Definition: z3py.py:3415
void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)
Decrement the reference counter of the given probe.
expr uge(expr const &a, expr const &b)
unsigned greater than or equal to operator for bitvectors.
Definition: z3++.h:970
void push()
Definition: z3++.h:1584
expr implies(expr const &a, bool b)
Definition: z3++.h:900
friend expr operator+(expr const &a, int b)
Definition: z3++.h:701
Z3_ast Z3_API Z3_goal_formula(Z3_context c, Z3_goal g, unsigned idx)
Return a formula from the given goal.
sort & operator=(sort const &s)
Return true if this sort and s are equal.
Definition: z3++.h:364
bool is_quantifier() const
Return true if this expression is a quantifier.
Definition: z3++.h:534
friend probe operator<=(probe const &p1, double p2)
Definition: z3++.h:1519
context * m_ctx
Definition: z3++.h:273
unsigned size() const
Definition: z3++.h:264
symbol name() const
Definition: z3++.h:443
friend expr operator|(expr const &a, int b)
Definition: z3++.h:871
void pop(unsigned n=1)
Definition: z3++.h:1293
friend std::ostream & operator<<(std::ostream &out, stats const &s)
Definition: z3++.h:1251
expr to_real(expr const &a)
Definition: z3++.h:1840
handle(unsigned h)
Definition: z3++.h:1558
friend expr operator>=(int a, expr const &b)
Definition: z3++.h:822
unsigned size() const
Definition: z3++.h:1245
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two&#39;s complement addition.
friend expr implies(expr const &a, expr const &b)
Definition: z3++.h:650
Z3_bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t)
Return true if the given expression t is well sorted.
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.
void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a)
Increment the reference counter of the given AST. The context c should have been created using Z3_mk_...
ast(ast const &s)
Definition: z3++.h:332
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:1634
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.
friend expr operator==(int a, expr const &b)
Definition: z3++.h:672
friend expr operator|(int a, expr const &b)
Definition: z3++.h:872
void Z3_API Z3_func_entry_dec_ref(Z3_context c, Z3_func_entry e)
Decrement the reference counter of the given Z3_func_entry object.
sort(sort const &s)
Definition: z3++.h:359
Z3_bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx)
Return Z3_TRUE if the given statistical data is a double.
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a maximization constraint.
Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i)
Array read. The argument a is the array and i is the index of the array that gets read...
apply_result(context &c, Z3_apply_result s)
Definition: z3++.h:1407
unsigned Z3_API Z3_apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r)
Return the number of subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
System.IntPtr Z3_params
Definition: Native.cs:27
friend expr operator^(int a, expr const &b)
Definition: z3++.h:868
Function declaration (aka function definition). It is the signature of interpreted and uninterpreted ...
Definition: z3++.h:432
T & operator[](int i)
Definition: z3++.h:265
Z3_probe Z3_API Z3_probe_or(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when p1 or p2 evaluates to true.
sort int_sort()
Return the integer sort.
Definition: z3++.h:1630
goal(goal const &s)
Definition: z3++.h:1364
void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g)
Decrement the reference counter of the given tactic.
stats & operator=(stats const &s)
Definition: z3++.h:1238
Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c, Z3_symbol name, unsigned n, Z3_symbol const enum_names[], Z3_func_decl enum_consts[], Z3_func_decl enum_testers[])
Create a enumeration sort.
unsigned num_args() const
Definition: z3++.h:1144
func_decl & operator=(func_decl const &s)
Definition: z3++.h:438
apply_result & operator=(apply_result const &s)
Definition: z3++.h:1411
void Z3_API Z3_ast_vector_push(Z3_context c, Z3_ast_vector v, Z3_ast a)
Add the AST a in the end of the AST vector v. The size of v is increased by one.
System.IntPtr Z3_func_interp
Definition: Native.cs:33
bool is_real() const
Return true if this sort is the Real sort.
Definition: z3++.h:381
sort to_sort(context &c, Z3_sort s)
Definition: z3++.h:945
context()
Definition: z3++.h:133
bool is_decided_sat() const
Definition: z3++.h:1382
void add(expr const &f)
Definition: z3++.h:1374
check_result
Definition: z3++.h:1254
Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m)
Convert the given model into a string.
unsigned size() const
Definition: z3++.h:1204
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition: z3_api.h:119
apply_result(apply_result const &s)
Definition: z3++.h:1408