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 param_descrs;
53  class ast;
54  class sort;
55  class func_decl;
56  class expr;
57  class solver;
58  class goal;
59  class tactic;
60  class probe;
61  class model;
62  class func_interp;
63  class func_entry;
64  class statistics;
65  class apply_result;
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);
86  };
87  inline std::ostream & operator<<(std::ostream & out, exception const & e) { out << e.msg(); return out; }
88 
89 
90 
94  class config {
95  Z3_config m_cfg;
96  config(config const & s);
97  config & operator=(config const & s);
98  public:
99  config() { m_cfg = Z3_mk_config(); }
100  ~config() { Z3_del_config(m_cfg); }
101  operator Z3_config() const { return m_cfg; }
105  void set(char const * param, char const * value) { Z3_set_param_value(m_cfg, param, value); }
109  void set(char const * param, bool value) { Z3_set_param_value(m_cfg, param, value ? "true" : "false"); }
113  void set(char const * param, int value) {
114  std::ostringstream oss;
115  oss << value;
116  Z3_set_param_value(m_cfg, param, oss.str().c_str());
117  }
118  };
119 
122  };
123 
125  if (l == Z3_L_TRUE) return sat;
126  else if (l == Z3_L_FALSE) return unsat;
127  return unknown;
128  }
129 
130 
134  class context {
135  Z3_context m_ctx;
136  static void error_handler(Z3_context /*c*/, Z3_error_code /*e*/) { /* do nothing */ }
137  void init(config & c) {
138  m_ctx = Z3_mk_context_rc(c);
139  Z3_set_error_handler(m_ctx, error_handler);
141  }
142 
143  void init_interp(config & c) {
144  m_ctx = Z3_mk_interpolation_context(c);
145  Z3_set_error_handler(m_ctx, error_handler);
147  }
148 
149  context(context const & s);
150  context & operator=(context const & s);
151  public:
152  struct interpolation {};
153  context() { config c; init(c); }
154  context(config & c) { init(c); }
155  context(config & c, interpolation) { init_interp(c); }
156  ~context() { Z3_del_context(m_ctx); }
157  operator Z3_context() const { return m_ctx; }
158 
162  void check_error() const {
163  Z3_error_code e = Z3_get_error_code(m_ctx);
164  if (e != Z3_OK)
165  throw exception(Z3_get_error_msg(m_ctx, e));
166  }
167 
171  void set(char const * param, char const * value) { Z3_update_param_value(m_ctx, param, value); }
175  void set(char const * param, bool value) { Z3_update_param_value(m_ctx, param, value ? "true" : "false"); }
179  void set(char const * param, int value) {
180  std::ostringstream oss;
181  oss << value;
182  Z3_update_param_value(m_ctx, param, oss.str().c_str());
183  }
184 
189  void interrupt() { Z3_interrupt(m_ctx); }
190 
194  symbol str_symbol(char const * s);
198  symbol int_symbol(int n);
202  sort bool_sort();
206  sort int_sort();
210  sort real_sort();
214  sort bv_sort(unsigned sz);
218  sort string_sort();
222  sort seq_sort(sort& s);
226  sort re_sort(sort& seq_sort);
232  sort array_sort(sort d, sort r);
238  sort enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts);
242  sort uninterpreted_sort(char const* name);
243  sort uninterpreted_sort(symbol const& name);
244 
245  func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range);
246  func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range);
247  func_decl function(symbol const& name, sort_vector const& domain, sort const& range);
248  func_decl function(char const * name, sort_vector const& domain, sort const& range);
249  func_decl function(char const * name, sort const & domain, sort const & range);
250  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range);
251  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range);
252  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range);
253  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range);
254 
255  expr constant(symbol const & name, sort const & s);
256  expr constant(char const * name, sort const & s);
257  expr bool_const(char const * name);
258  expr int_const(char const * name);
259  expr real_const(char const * name);
260  expr bv_const(char const * name, unsigned sz);
261 
262  expr bool_val(bool b);
263 
264  expr int_val(int n);
265  expr int_val(unsigned n);
266  expr int_val(__int64 n);
267  expr int_val(__uint64 n);
268  expr int_val(char const * n);
269 
270  expr real_val(int n, int d);
271  expr real_val(int n);
272  expr real_val(unsigned n);
273  expr real_val(__int64 n);
274  expr real_val(__uint64 n);
275  expr real_val(char const * n);
276 
277  expr bv_val(int n, unsigned sz);
278  expr bv_val(unsigned n, unsigned sz);
279  expr bv_val(__int64 n, unsigned sz);
280  expr bv_val(__uint64 n, unsigned sz);
281  expr bv_val(char const * n, unsigned sz);
282 
283  expr string_val(char const* s);
284  expr string_val(std::string const& s);
285 
286  expr num_val(int n, sort const & s);
287 
291  expr parse_string(char const* s);
292  expr parse_file(char const* file);
293 
294  expr parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
295  expr parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
296 
300  check_result compute_interpolant(expr const& pat, params const& p, expr_vector& interp, model& m);
301  expr_vector get_interpolant(expr const& proof, expr const& pat, params const& p);
302 
303  };
304 
305 
306 
307 
308  template<typename T>
309  class array {
310  T * m_array;
311  unsigned m_size;
312  array(array const & s);
313  array & operator=(array const & s);
314  public:
315  array(unsigned sz):m_size(sz) { m_array = new T[sz]; }
316  template<typename T2>
317  array(ast_vector_tpl<T2> const & v);
318  ~array() { delete[] m_array; }
319  unsigned size() const { return m_size; }
320  T & operator[](int i) { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
321  T const & operator[](int i) const { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
322  T const * ptr() const { return m_array; }
323  T * ptr() { return m_array; }
324  };
325 
326  class object {
327  protected:
329  public:
330  object(context & c):m_ctx(&c) {}
331  object(object const & s):m_ctx(s.m_ctx) {}
332  context & ctx() const { return *m_ctx; }
333  void check_error() const { m_ctx->check_error(); }
334  friend void check_context(object const & a, object const & b);
335  };
336  inline void check_context(object const & a, object const & b) { assert(a.m_ctx == b.m_ctx); }
337 
338  class symbol : public object {
339  Z3_symbol m_sym;
340  public:
341  symbol(context & c, Z3_symbol s):object(c), m_sym(s) {}
342  symbol(symbol const & s):object(s), m_sym(s.m_sym) {}
343  symbol & operator=(symbol const & s) { m_ctx = s.m_ctx; m_sym = s.m_sym; return *this; }
344  operator Z3_symbol() const { return m_sym; }
345  Z3_symbol_kind kind() const { return Z3_get_symbol_kind(ctx(), m_sym); }
346  std::string str() const { assert(kind() == Z3_STRING_SYMBOL); return Z3_get_symbol_string(ctx(), m_sym); }
347  int to_int() const { assert(kind() == Z3_INT_SYMBOL); return Z3_get_symbol_int(ctx(), m_sym); }
348  friend std::ostream & operator<<(std::ostream & out, symbol const & s);
349  };
350 
351  inline std::ostream & operator<<(std::ostream & out, symbol const & s) {
352  if (s.kind() == Z3_INT_SYMBOL)
353  out << "k!" << s.to_int();
354  else
355  out << s.str().c_str();
356  return out;
357  }
358 
359 
360  class param_descrs : public object {
361  Z3_param_descrs m_descrs;
362  public:
363  param_descrs(context& c, Z3_param_descrs d): object(c), m_descrs(d) { Z3_param_descrs_inc_ref(c, d); }
364  param_descrs(param_descrs const& o): object(o.ctx()), m_descrs(o.m_descrs) { Z3_param_descrs_inc_ref(ctx(), m_descrs); }
366  Z3_param_descrs_inc_ref(o.ctx(), o.m_descrs);
367  Z3_param_descrs_dec_ref(ctx(), m_descrs);
368  m_descrs = o.m_descrs;
369  m_ctx = o.m_ctx;
370  return *this;
371  }
372  ~param_descrs() { Z3_param_descrs_dec_ref(ctx(), m_descrs); }
374 
375  unsigned size() { return Z3_param_descrs_size(ctx(), m_descrs); }
376  symbol name(unsigned i) { return symbol(ctx(), Z3_param_descrs_get_name(ctx(), m_descrs, i)); }
377  Z3_param_kind kind(symbol const& s) { return Z3_param_descrs_get_kind(ctx(), m_descrs, s); }
378  std::string documentation(symbol const& s) { char const* r = Z3_param_descrs_get_documentation(ctx(), m_descrs, s); check_error(); return r; }
379  std::string to_string() const { return Z3_param_descrs_to_string(ctx(), m_descrs); }
380  };
381 
382  inline std::ostream& operator<<(std::ostream & out, param_descrs const & d) { return out << d.to_string(); }
383 
384  class params : public object {
385  Z3_params m_params;
386  public:
387  params(context & c):object(c) { m_params = Z3_mk_params(c); Z3_params_inc_ref(ctx(), m_params); }
388  params(params const & s):object(s), m_params(s.m_params) { Z3_params_inc_ref(ctx(), m_params); }
389  ~params() { Z3_params_dec_ref(ctx(), m_params); }
390  operator Z3_params() const { return m_params; }
391  params & operator=(params const & s) {
392  Z3_params_inc_ref(s.ctx(), s.m_params);
393  Z3_params_dec_ref(ctx(), m_params);
394  m_ctx = s.m_ctx;
395  m_params = s.m_params;
396  return *this;
397  }
398  void set(char const * k, bool b) { Z3_params_set_bool(ctx(), m_params, ctx().str_symbol(k), b); }
399  void set(char const * k, unsigned n) { Z3_params_set_uint(ctx(), m_params, ctx().str_symbol(k), n); }
400  void set(char const * k, double n) { Z3_params_set_double(ctx(), m_params, ctx().str_symbol(k), n); }
401  void set(char const * k, symbol const & s) { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), s); }
402  friend std::ostream & operator<<(std::ostream & out, params const & p);
403  };
404 
405  inline std::ostream & operator<<(std::ostream & out, params const & p) {
406  out << Z3_params_to_string(p.ctx(), p); return out;
407  }
408 
409  class ast : public object {
410  protected:
411  Z3_ast m_ast;
412  public:
413  ast(context & c):object(c), m_ast(0) {}
414  ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
415  ast(ast const & s):object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
416  ~ast() { if (m_ast) Z3_dec_ref(*m_ctx, m_ast); }
417  operator Z3_ast() const { return m_ast; }
418  operator bool() const { return m_ast != 0; }
419  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; }
420  Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }
421  unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }
422  friend std::ostream & operator<<(std::ostream & out, ast const & n);
423 
427  friend bool eq(ast const & a, ast const & b);
428  };
429  inline std::ostream & operator<<(std::ostream & out, ast const & n) {
430  out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
431  }
432 
433  inline bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b) != 0; }
434 
435 
439  class sort : public ast {
440  public:
441  sort(context & c):ast(c) {}
442  sort(context & c, Z3_sort s):ast(c, reinterpret_cast<Z3_ast>(s)) {}
443  sort(sort const & s):ast(s) {}
444  operator Z3_sort() const { return reinterpret_cast<Z3_sort>(m_ast); }
448  sort & operator=(sort const & s) { return static_cast<sort&>(ast::operator=(s)); }
452  Z3_sort_kind sort_kind() const { return Z3_get_sort_kind(*m_ctx, *this); }
456  symbol name() const { Z3_symbol s = Z3_get_sort_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
460  bool is_bool() const { return sort_kind() == Z3_BOOL_SORT; }
464  bool is_int() const { return sort_kind() == Z3_INT_SORT; }
468  bool is_real() const { return sort_kind() == Z3_REAL_SORT; }
472  bool is_arith() const { return is_int() || is_real(); }
476  bool is_bv() const { return sort_kind() == Z3_BV_SORT; }
480  bool is_array() const { return sort_kind() == Z3_ARRAY_SORT; }
484  bool is_datatype() const { return sort_kind() == Z3_DATATYPE_SORT; }
488  bool is_relation() const { return sort_kind() == Z3_RELATION_SORT; }
492  bool is_seq() const { return sort_kind() == Z3_SEQ_SORT; }
496  bool is_re() const { return sort_kind() == Z3_RE_SORT; }
500  bool is_finite_domain() const { return sort_kind() == Z3_FINITE_DOMAIN_SORT; }
501 
507  unsigned bv_size() const { assert(is_bv()); unsigned r = Z3_get_bv_sort_size(ctx(), *this); check_error(); return r; }
508 
514  sort array_domain() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_domain(ctx(), *this); check_error(); return sort(ctx(), s); }
520  sort array_range() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_range(ctx(), *this); check_error(); return sort(ctx(), s); }
521  };
522 
527  class func_decl : public ast {
528  public:
529  func_decl(context & c):ast(c) {}
530  func_decl(context & c, Z3_func_decl n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
531  func_decl(func_decl const & s):ast(s) {}
532  operator Z3_func_decl() const { return reinterpret_cast<Z3_func_decl>(m_ast); }
533  func_decl & operator=(func_decl const & s) { return static_cast<func_decl&>(ast::operator=(s)); }
534 
535  unsigned arity() const { return Z3_get_arity(ctx(), *this); }
536  sort domain(unsigned i) const { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }
537  sort range() const { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }
538  symbol name() const { Z3_symbol s = Z3_get_decl_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
539  Z3_decl_kind decl_kind() const { return Z3_get_decl_kind(ctx(), *this); }
540 
541  bool is_const() const { return arity() == 0; }
542 
543  expr operator()() const;
544  expr operator()(unsigned n, expr const * args) const;
545  expr operator()(expr_vector const& v) const;
546  expr operator()(expr const & a) const;
547  expr operator()(int a) const;
548  expr operator()(expr const & a1, expr const & a2) const;
549  expr operator()(expr const & a1, int a2) const;
550  expr operator()(int a1, expr const & a2) const;
551  expr operator()(expr const & a1, expr const & a2, expr const & a3) const;
552  expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const;
553  expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const;
554  };
555 
560  class expr : public ast {
561  public:
562  expr(context & c):ast(c) {}
563  expr(context & c, Z3_ast n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
564  expr(expr const & n):ast(n) {}
565  expr & operator=(expr const & n) { return static_cast<expr&>(ast::operator=(n)); }
566 
570  sort get_sort() const { Z3_sort s = Z3_get_sort(*m_ctx, m_ast); check_error(); return sort(*m_ctx, s); }
571 
575  bool is_bool() const { return get_sort().is_bool(); }
579  bool is_int() const { return get_sort().is_int(); }
583  bool is_real() const { return get_sort().is_real(); }
587  bool is_arith() const { return get_sort().is_arith(); }
591  bool is_bv() const { return get_sort().is_bv(); }
595  bool is_array() const { return get_sort().is_array(); }
599  bool is_datatype() const { return get_sort().is_datatype(); }
603  bool is_relation() const { return get_sort().is_relation(); }
607  bool is_seq() const { return get_sort().is_seq(); }
611  bool is_re() const { return get_sort().is_re(); }
612 
621  bool is_finite_domain() const { return get_sort().is_finite_domain(); }
622 
628  bool is_numeral() const { return kind() == Z3_NUMERAL_AST; }
629  bool is_numeral_i64(__int64& i) const { bool r = 0 != Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}
630  bool is_numeral_u64(__uint64& i) const { bool r = 0 != Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}
631  bool is_numeral_i(int& i) const { bool r = 0 != Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}
632  bool is_numeral_u(unsigned& i) const { bool r = 0 != Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
633  bool is_numeral(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; }
634  bool is_numeral(std::string& s, unsigned precision) const { if (!is_numeral()) return false; s = Z3_get_numeral_decimal_string(ctx(), m_ast, precision); check_error(); return true; }
638  bool is_app() const { return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
642  bool is_const() const { return is_app() && num_args() == 0; }
646  bool is_quantifier() const { return kind() == Z3_QUANTIFIER_AST; }
650  bool is_var() const { return kind() == Z3_VAR_AST; }
654  bool is_algebraic() const { return 0 != Z3_is_algebraic_number(ctx(), m_ast); }
655 
659  bool is_well_sorted() const { bool r = Z3_is_well_sorted(ctx(), m_ast) != 0; check_error(); return r; }
660 
667  std::string get_decimal_string(int precision) const {
668  assert(is_numeral() || is_algebraic());
669  return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
670  }
671 
678  int get_numeral_int() const {
679  int result;
680  if (!is_numeral_i(result)) {
681  throw exception("numeral does not fit in machine int");
682  }
683  return result;
684  }
685 
692  unsigned get_numeral_uint() const {
693  assert(is_numeral());
694  unsigned result;
695  if (!is_numeral_u(result)) {
696  throw exception("numeral does not fit in machine uint");
697  }
698  return result;
699  }
700 
708  assert(is_numeral());
709  __int64 result;
710  if (!is_numeral_i64(result)) {
711  throw exception("numeral does not fit in machine __int64");
712  }
713  return result;
714  }
715 
723  assert(is_numeral());
724  __uint64 result;
725  if (!is_numeral_u64(result)) {
726  throw exception("numeral does not fit in machine __uint64");
727  }
728  return result;
729  }
730 
731 
732  operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
733 
740  func_decl decl() const { Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }
747  unsigned num_args() const { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
755  expr arg(unsigned i) const { Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }
756 
762  expr body() const { assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
763 
769  friend expr operator!(expr const & a);
770 
771 
778  friend expr operator&&(expr const & a, expr const & b);
779 
780 
787  friend expr operator&&(expr const & a, bool b);
794  friend expr operator&&(bool a, expr const & b);
795 
802  friend expr operator||(expr const & a, expr const & b);
809  friend expr operator||(expr const & a, bool b);
810 
817  friend expr operator||(bool a, expr const & b);
818 
819  friend expr implies(expr const & a, expr const & b);
820  friend expr implies(expr const & a, bool b);
821  friend expr implies(bool a, expr const & b);
822 
823  friend expr mk_or(expr_vector const& args);
824  friend expr mk_and(expr_vector const& args);
825 
826  friend expr ite(expr const & c, expr const & t, expr const & e);
827 
828  friend expr distinct(expr_vector const& args);
829  friend expr concat(expr const& a, expr const& b);
830  friend expr concat(expr_vector const& args);
831 
832  friend expr operator==(expr const & a, expr const & b);
833  friend expr operator==(expr const & a, int b);
834  friend expr operator==(int a, expr const & b);
835 
836  friend expr operator!=(expr const & a, expr const & b);
837  friend expr operator!=(expr const & a, int b);
838  friend expr operator!=(int a, expr const & b);
839 
840  friend expr operator+(expr const & a, expr const & b);
841  friend expr operator+(expr const & a, int b);
842  friend expr operator+(int a, expr const & b);
843 
844  friend expr operator*(expr const & a, expr const & b);
845  friend expr operator*(expr const & a, int b);
846  friend expr operator*(int a, expr const & b);
847 
851  friend expr pw(expr const & a, expr const & b);
852  friend expr pw(expr const & a, int b);
853  friend expr pw(int a, expr const & b);
854 
855  friend expr operator/(expr const & a, expr const & b);
856  friend expr operator/(expr const & a, int b);
857  friend expr operator/(int a, expr const & b);
858 
859  friend expr operator-(expr const & a);
860 
861  friend expr operator-(expr const & a, expr const & b);
862  friend expr operator-(expr const & a, int b);
863  friend expr operator-(int a, expr const & b);
864 
865  friend expr operator<=(expr const & a, expr const & b);
866  friend expr operator<=(expr const & a, int b);
867  friend expr operator<=(int a, expr const & b);
868 
869 
870  friend expr operator>=(expr const & a, expr const & b);
871  friend expr wasoperator(expr const & a, expr const & b);
872  friend expr operator>=(expr const & a, int b);
873  friend expr operator>=(int a, expr const & b);
874 
875  friend expr operator<(expr const & a, expr const & b);
876  friend expr operator<(expr const & a, int b);
877  friend expr operator<(int a, expr const & b);
878 
879  friend expr operator>(expr const & a, expr const & b);
880  friend expr operator>(expr const & a, int b);
881  friend expr operator>(int a, expr const & b);
882 
883  friend expr operator&(expr const & a, expr const & b);
884  friend expr operator&(expr const & a, int b);
885  friend expr operator&(int a, expr const & b);
886 
887  friend expr operator^(expr const & a, expr const & b);
888  friend expr operator^(expr const & a, int b);
889  friend expr operator^(int a, expr const & b);
890 
891  friend expr operator|(expr const & a, expr const & b);
892  friend expr operator|(expr const & a, int b);
893  friend expr operator|(int a, expr const & b);
894 
895  friend expr operator~(expr const & a);
896  expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }
897  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)); }
898  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)); }
899 
905  expr extract(expr const& offset, expr const& length) const {
906  check_context(*this, offset); check_context(offset, length);
907  Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
908  }
909  expr replace(expr const& src, expr const& dst) const {
910  check_context(*this, src); check_context(src, dst);
911  Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
912  check_error();
913  return expr(ctx(), r);
914  }
915  expr unit() const {
916  Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
917  check_error();
918  return expr(ctx(), r);
919  }
920  expr contains(expr const& s) {
921  check_context(*this, s);
922  Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
923  check_error();
924  return expr(ctx(), r);
925  }
926  expr at(expr const& index) const {
927  check_context(*this, index);
928  Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
929  check_error();
930  return expr(ctx(), r);
931  }
932  expr length() const {
933  Z3_ast r = Z3_mk_seq_length(ctx(), *this);
934  check_error();
935  return expr(ctx(), r);
936  }
937 
938 
939 
943  expr simplify() const { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
947  expr simplify(params const & p) const { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
948 
952  expr substitute(expr_vector const& src, expr_vector const& dst);
953 
957  expr substitute(expr_vector const& dst);
958 
959  };
960 
961  inline expr implies(expr const & a, expr const & b) {
962  check_context(a, b);
963  assert(a.is_bool() && b.is_bool());
964  Z3_ast r = Z3_mk_implies(a.ctx(), a, b);
965  a.check_error();
966  return expr(a.ctx(), r);
967  }
968  inline expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); }
969  inline expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); }
970 
971 
972  inline expr pw(expr const & a, expr const & b) {
973  assert(a.is_arith() && b.is_arith());
974  check_context(a, b);
975  Z3_ast r = Z3_mk_power(a.ctx(), a, b);
976  a.check_error();
977  return expr(a.ctx(), r);
978  }
979  inline expr pw(expr const & a, int b) { return pw(a, a.ctx().num_val(b, a.get_sort())); }
980  inline expr pw(int a, expr const & b) { return pw(b.ctx().num_val(a, b.get_sort()), b); }
981 
982 
983  inline expr operator!(expr const & a) {
984  assert(a.is_bool());
985  Z3_ast r = Z3_mk_not(a.ctx(), a);
986  a.check_error();
987  return expr(a.ctx(), r);
988  }
989 
990  inline expr operator&&(expr const & a, expr const & b) {
991  check_context(a, b);
992  assert(a.is_bool() && b.is_bool());
993  Z3_ast args[2] = { a, b };
994  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
995  a.check_error();
996  return expr(a.ctx(), r);
997  }
998 
999  inline expr operator&&(expr const & a, bool b) { return a && a.ctx().bool_val(b); }
1000  inline expr operator&&(bool a, expr const & b) { return b.ctx().bool_val(a) && b; }
1001 
1002  inline expr operator||(expr const & a, expr const & b) {
1003  check_context(a, b);
1004  assert(a.is_bool() && b.is_bool());
1005  Z3_ast args[2] = { a, b };
1006  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1007  a.check_error();
1008  return expr(a.ctx(), r);
1009  }
1010 
1011  inline expr operator||(expr const & a, bool b) { return a || a.ctx().bool_val(b); }
1012 
1013  inline expr operator||(bool a, expr const & b) { return b.ctx().bool_val(a) || b; }
1014 
1015  inline expr operator==(expr const & a, expr const & b) {
1016  check_context(a, b);
1017  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1018  a.check_error();
1019  return expr(a.ctx(), r);
1020  }
1021  inline expr operator==(expr const & a, int b) { assert(a.is_arith() || a.is_bv()); return a == a.ctx().num_val(b, a.get_sort()); }
1022  inline expr operator==(int a, expr const & b) { assert(b.is_arith() || b.is_bv()); return b.ctx().num_val(a, b.get_sort()) == b; }
1023 
1024  inline expr operator!=(expr const & a, expr const & b) {
1025  check_context(a, b);
1026  Z3_ast args[2] = { a, b };
1027  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1028  a.check_error();
1029  return expr(a.ctx(), r);
1030  }
1031  inline expr operator!=(expr const & a, int b) { assert(a.is_arith() || a.is_bv()); return a != a.ctx().num_val(b, a.get_sort()); }
1032  inline expr operator!=(int a, expr const & b) { assert(b.is_arith() || b.is_bv()); return b.ctx().num_val(a, b.get_sort()) != b; }
1033 
1034  inline expr operator+(expr const & a, expr const & b) {
1035  check_context(a, b);
1036  Z3_ast r = 0;
1037  if (a.is_arith() && b.is_arith()) {
1038  Z3_ast args[2] = { a, b };
1039  r = Z3_mk_add(a.ctx(), 2, args);
1040  }
1041  else if (a.is_bv() && b.is_bv()) {
1042  r = Z3_mk_bvadd(a.ctx(), a, b);
1043  }
1044  else if (a.is_seq() && b.is_seq()) {
1045  return concat(a, b);
1046  }
1047  else if (a.is_re() && b.is_re()) {
1048  Z3_ast _args[2] = { a, b };
1049  r = Z3_mk_re_union(a.ctx(), 2, _args);
1050  }
1051  else {
1052  // operator is not supported by given arguments.
1053  assert(false);
1054  }
1055  a.check_error();
1056  return expr(a.ctx(), r);
1057  }
1058  inline expr operator+(expr const & a, int b) { return a + a.ctx().num_val(b, a.get_sort()); }
1059  inline expr operator+(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) + b; }
1060 
1061  inline expr operator*(expr const & a, expr const & b) {
1062  check_context(a, b);
1063  Z3_ast r = 0;
1064  if (a.is_arith() && b.is_arith()) {
1065  Z3_ast args[2] = { a, b };
1066  r = Z3_mk_mul(a.ctx(), 2, args);
1067  }
1068  else if (a.is_bv() && b.is_bv()) {
1069  r = Z3_mk_bvmul(a.ctx(), a, b);
1070  }
1071  else {
1072  // operator is not supported by given arguments.
1073  assert(false);
1074  }
1075  a.check_error();
1076  return expr(a.ctx(), r);
1077  }
1078  inline expr operator*(expr const & a, int b) { return a * a.ctx().num_val(b, a.get_sort()); }
1079  inline expr operator*(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) * b; }
1080 
1081 
1082  inline expr operator>=(expr const & a, expr const & b) {
1083  check_context(a, b);
1084  Z3_ast r = 0;
1085  if (a.is_arith() && b.is_arith()) {
1086  r = Z3_mk_ge(a.ctx(), a, b);
1087  }
1088  else if (a.is_bv() && b.is_bv()) {
1089  r = Z3_mk_bvsge(a.ctx(), a, b);
1090  }
1091  else {
1092  // operator is not supported by given arguments.
1093  assert(false);
1094  }
1095  a.check_error();
1096  return expr(a.ctx(), r);
1097  }
1098 
1099  inline expr operator/(expr const & a, expr const & b) {
1100  check_context(a, b);
1101  Z3_ast r = 0;
1102  if (a.is_arith() && b.is_arith()) {
1103  r = Z3_mk_div(a.ctx(), a, b);
1104  }
1105  else if (a.is_bv() && b.is_bv()) {
1106  r = Z3_mk_bvsdiv(a.ctx(), a, b);
1107  }
1108  else {
1109  // operator is not supported by given arguments.
1110  assert(false);
1111  }
1112  a.check_error();
1113  return expr(a.ctx(), r);
1114  }
1115  inline expr operator/(expr const & a, int b) { return a / a.ctx().num_val(b, a.get_sort()); }
1116  inline expr operator/(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) / b; }
1117 
1118  inline expr operator-(expr const & a) {
1119  Z3_ast r = 0;
1120  if (a.is_arith()) {
1121  r = Z3_mk_unary_minus(a.ctx(), a);
1122  }
1123  else if (a.is_bv()) {
1124  r = Z3_mk_bvneg(a.ctx(), a);
1125  }
1126  else {
1127  // operator is not supported by given arguments.
1128  assert(false);
1129  }
1130  a.check_error();
1131  return expr(a.ctx(), r);
1132  }
1133 
1134  inline expr operator-(expr const & a, expr const & b) {
1135  check_context(a, b);
1136  Z3_ast r = 0;
1137  if (a.is_arith() && b.is_arith()) {
1138  Z3_ast args[2] = { a, b };
1139  r = Z3_mk_sub(a.ctx(), 2, args);
1140  }
1141  else if (a.is_bv() && b.is_bv()) {
1142  r = Z3_mk_bvsub(a.ctx(), a, b);
1143  }
1144  else {
1145  // operator is not supported by given arguments.
1146  assert(false);
1147  }
1148  a.check_error();
1149  return expr(a.ctx(), r);
1150  }
1151  inline expr operator-(expr const & a, int b) { return a - a.ctx().num_val(b, a.get_sort()); }
1152  inline expr operator-(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) - b; }
1153 
1154  inline expr operator<=(expr const & a, expr const & b) {
1155  check_context(a, b);
1156  Z3_ast r = 0;
1157  if (a.is_arith() && b.is_arith()) {
1158  r = Z3_mk_le(a.ctx(), a, b);
1159  }
1160  else if (a.is_bv() && b.is_bv()) {
1161  r = Z3_mk_bvsle(a.ctx(), a, b);
1162  }
1163  else {
1164  // operator is not supported by given arguments.
1165  assert(false);
1166  }
1167  a.check_error();
1168  return expr(a.ctx(), r);
1169  }
1170  inline expr operator<=(expr const & a, int b) { return a <= a.ctx().num_val(b, a.get_sort()); }
1171  inline expr operator<=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) <= b; }
1172 
1173  inline expr operator>=(expr const & a, int b) { return a >= a.ctx().num_val(b, a.get_sort()); }
1174  inline expr operator>=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) >= b; }
1175 
1176  inline expr operator<(expr const & a, expr const & b) {
1177  check_context(a, b);
1178  Z3_ast r = 0;
1179  if (a.is_arith() && b.is_arith()) {
1180  r = Z3_mk_lt(a.ctx(), a, b);
1181  }
1182  else if (a.is_bv() && b.is_bv()) {
1183  r = Z3_mk_bvslt(a.ctx(), a, b);
1184  }
1185  else {
1186  // operator is not supported by given arguments.
1187  assert(false);
1188  }
1189  a.check_error();
1190  return expr(a.ctx(), r);
1191  }
1192  inline expr operator<(expr const & a, int b) { return a < a.ctx().num_val(b, a.get_sort()); }
1193  inline expr operator<(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) < b; }
1194 
1195  inline expr operator>(expr const & a, expr const & b) {
1196  check_context(a, b);
1197  Z3_ast r = 0;
1198  if (a.is_arith() && b.is_arith()) {
1199  r = Z3_mk_gt(a.ctx(), a, b);
1200  }
1201  else if (a.is_bv() && b.is_bv()) {
1202  r = Z3_mk_bvsgt(a.ctx(), a, b);
1203  }
1204  else {
1205  // operator is not supported by given arguments.
1206  assert(false);
1207  }
1208  a.check_error();
1209  return expr(a.ctx(), r);
1210  }
1211  inline expr operator>(expr const & a, int b) { return a > a.ctx().num_val(b, a.get_sort()); }
1212  inline expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > b; }
1213 
1214  inline 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); }
1215  inline expr operator&(expr const & a, int b) { return a & a.ctx().num_val(b, a.get_sort()); }
1216  inline expr operator&(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) & b; }
1217 
1218  inline 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); }
1219  inline expr operator^(expr const & a, int b) { return a ^ a.ctx().num_val(b, a.get_sort()); }
1220  inline expr operator^(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) ^ b; }
1221 
1222  inline 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); }
1223  inline expr operator|(expr const & a, int b) { return a | a.ctx().num_val(b, a.get_sort()); }
1224  inline expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; }
1225 
1226  inline expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
1227 
1228 
1229 
1230 
1237  inline expr ite(expr const & c, expr const & t, expr const & e) {
1238  check_context(c, t); check_context(c, e);
1239  assert(c.is_bool());
1240  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
1241  c.check_error();
1242  return expr(c.ctx(), r);
1243  }
1244 
1245 
1250  inline expr to_expr(context & c, Z3_ast a) {
1251  c.check_error();
1252  assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
1253  Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
1254  Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
1255  Z3_get_ast_kind(c, a) == Z3_QUANTIFIER_AST);
1256  return expr(c, a);
1257  }
1258 
1259  inline sort to_sort(context & c, Z3_sort s) {
1260  c.check_error();
1261  return sort(c, s);
1262  }
1263 
1264  inline func_decl to_func_decl(context & c, Z3_func_decl f) {
1265  c.check_error();
1266  return func_decl(c, f);
1267  }
1268 
1272  inline expr ule(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
1273  inline expr ule(expr const & a, int b) { return ule(a, a.ctx().num_val(b, a.get_sort())); }
1274  inline expr ule(int a, expr const & b) { return ule(b.ctx().num_val(a, b.get_sort()), b); }
1278  inline expr ult(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }
1279  inline expr ult(expr const & a, int b) { return ult(a, a.ctx().num_val(b, a.get_sort())); }
1280  inline expr ult(int a, expr const & b) { return ult(b.ctx().num_val(a, b.get_sort()), b); }
1284  inline expr uge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }
1285  inline expr uge(expr const & a, int b) { return uge(a, a.ctx().num_val(b, a.get_sort())); }
1286  inline expr uge(int a, expr const & b) { return uge(b.ctx().num_val(a, b.get_sort()), b); }
1290  inline expr ugt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
1291  inline expr ugt(expr const & a, int b) { return ugt(a, a.ctx().num_val(b, a.get_sort())); }
1292  inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), b); }
1296  inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
1297  inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); }
1298  inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); }
1299 
1303  inline expr srem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsrem(a.ctx(), a, b)); }
1304  inline expr srem(expr const & a, int b) { return srem(a, a.ctx().num_val(b, a.get_sort())); }
1305  inline expr srem(int a, expr const & b) { return srem(b.ctx().num_val(a, b.get_sort()), b); }
1306 
1310  inline expr urem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvurem(a.ctx(), a, b)); }
1311  inline expr urem(expr const & a, int b) { return urem(a, a.ctx().num_val(b, a.get_sort())); }
1312  inline expr urem(int a, expr const & b) { return urem(b.ctx().num_val(a, b.get_sort()), b); }
1313 
1317  inline expr shl(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvshl(a.ctx(), a, b)); }
1318  inline expr shl(expr const & a, int b) { return shl(a, a.ctx().num_val(b, a.get_sort())); }
1319  inline expr shl(int a, expr const & b) { return shl(b.ctx().num_val(a, b.get_sort()), b); }
1320 
1324  inline expr lshr(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvlshr(a.ctx(), a, b)); }
1325  inline expr lshr(expr const & a, int b) { return lshr(a, a.ctx().num_val(b, a.get_sort())); }
1326  inline expr lshr(int a, expr const & b) { return lshr(b.ctx().num_val(a, b.get_sort()), b); }
1327 
1331  inline expr ashr(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvashr(a.ctx(), a, b)); }
1332  inline expr ashr(expr const & a, int b) { return ashr(a, a.ctx().num_val(b, a.get_sort())); }
1333  inline expr ashr(int a, expr const & b) { return ashr(b.ctx().num_val(a, b.get_sort()), b); }
1334 
1338  inline expr zext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_zero_ext(a.ctx(), i, a)); }
1339 
1343  inline expr sext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_sign_ext(a.ctx(), i, a)); }
1344 
1345  template<typename T> class cast_ast;
1346 
1347  template<> class cast_ast<ast> {
1348  public:
1349  ast operator()(context & c, Z3_ast a) { return ast(c, a); }
1350  };
1351 
1352  template<> class cast_ast<expr> {
1353  public:
1354  expr operator()(context & c, Z3_ast a) {
1355  assert(Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
1356  Z3_get_ast_kind(c, a) == Z3_APP_AST ||
1357  Z3_get_ast_kind(c, a) == Z3_QUANTIFIER_AST ||
1358  Z3_get_ast_kind(c, a) == Z3_VAR_AST);
1359  return expr(c, a);
1360  }
1361  };
1362 
1363  template<> class cast_ast<sort> {
1364  public:
1365  sort operator()(context & c, Z3_ast a) {
1366  assert(Z3_get_ast_kind(c, a) == Z3_SORT_AST);
1367  return sort(c, reinterpret_cast<Z3_sort>(a));
1368  }
1369  };
1370 
1371  template<> class cast_ast<func_decl> {
1372  public:
1373  func_decl operator()(context & c, Z3_ast a) {
1374  assert(Z3_get_ast_kind(c, a) == Z3_FUNC_DECL_AST);
1375  return func_decl(c, reinterpret_cast<Z3_func_decl>(a));
1376  }
1377  };
1378 
1379  template<typename T>
1380  class ast_vector_tpl : public object {
1381  Z3_ast_vector m_vector;
1382  void init(Z3_ast_vector v) { Z3_ast_vector_inc_ref(ctx(), v); m_vector = v; }
1383  public:
1384  ast_vector_tpl(context & c):object(c) { init(Z3_mk_ast_vector(c)); }
1385  ast_vector_tpl(context & c, Z3_ast_vector v):object(c) { init(v); }
1386  ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
1387  ~ast_vector_tpl() { Z3_ast_vector_dec_ref(ctx(), m_vector); }
1388  operator Z3_ast_vector() const { return m_vector; }
1389  unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); }
1390  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); }
1391  void push_back(T const & e) { Z3_ast_vector_push(ctx(), m_vector, e); check_error(); }
1392  void resize(unsigned sz) { Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }
1393  T back() const { return operator[](size() - 1); }
1394  void pop_back() { assert(size() > 0); resize(size() - 1); }
1395  bool empty() const { return size() == 0; }
1397  Z3_ast_vector_inc_ref(s.ctx(), s.m_vector);
1398  Z3_ast_vector_dec_ref(ctx(), m_vector);
1399  m_ctx = s.m_ctx;
1400  m_vector = s.m_vector;
1401  return *this;
1402  }
1403  friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
1404  };
1405 
1406 
1407  template<typename T>
1408  template<typename T2>
1410  m_array = new T[v.size()];
1411  m_size = v.size();
1412  for (unsigned i = 0; i < m_size; i++) {
1413  m_array[i] = v[i];
1414  }
1415  }
1416 
1417  // Basic functions for creating quantified formulas.
1418  // The C API should be used for creating quantifiers with patterns, weights, many variables, etc.
1419  inline expr forall(expr const & x, expr const & b) {
1420  check_context(x, b);
1421  Z3_app vars[] = {(Z3_app) x};
1422  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1423  }
1424  inline expr forall(expr const & x1, expr const & x2, expr const & b) {
1425  check_context(x1, b); check_context(x2, b);
1426  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1427  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1428  }
1429  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
1430  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1431  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1432  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1433  }
1434  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
1435  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1436  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1437  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1438  }
1439  inline expr forall(expr_vector const & xs, expr const & b) {
1440  array<Z3_app> vars(xs);
1441  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);
1442  }
1443  inline expr exists(expr const & x, expr const & b) {
1444  check_context(x, b);
1445  Z3_app vars[] = {(Z3_app) x};
1446  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1447  }
1448  inline expr exists(expr const & x1, expr const & x2, expr const & b) {
1449  check_context(x1, b); check_context(x2, b);
1450  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1451  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1452  }
1453  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
1454  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1455  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1456  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1457  }
1458  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
1459  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1460  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1461  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1462  }
1463  inline expr exists(expr_vector const & xs, expr const & b) {
1464  array<Z3_app> vars(xs);
1465  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);
1466  }
1467 
1468 
1469  inline expr distinct(expr_vector const& args) {
1470  assert(args.size() > 0);
1471  context& ctx = args[0].ctx();
1472  array<Z3_ast> _args(args);
1473  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
1474  ctx.check_error();
1475  return expr(ctx, r);
1476  }
1477 
1478  inline expr concat(expr const& a, expr const& b) {
1479  check_context(a, b);
1480  Z3_ast r;
1481  if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
1482  Z3_ast _args[2] = { a, b };
1483  r = Z3_mk_seq_concat(a.ctx(), 2, _args);
1484  }
1485  else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
1486  Z3_ast _args[2] = { a, b };
1487  r = Z3_mk_re_concat(a.ctx(), 2, _args);
1488  }
1489  else {
1490  r = Z3_mk_concat(a.ctx(), a, b);
1491  }
1492  a.ctx().check_error();
1493  return expr(a.ctx(), r);
1494  }
1495 
1496  inline expr concat(expr_vector const& args) {
1497  Z3_ast r;
1498  assert(args.size() > 0);
1499  if (args.size() == 1) {
1500  return args[0];
1501  }
1502  context& ctx = args[0].ctx();
1503  array<Z3_ast> _args(args);
1504  if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
1505  r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
1506  }
1507  else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
1508  r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
1509  }
1510  else {
1511  r = _args[args.size()-1];
1512  for (unsigned i = args.size()-1; i > 0; ) {
1513  --i;
1514  r = Z3_mk_concat(ctx, _args[i], r);
1515  ctx.check_error();
1516  }
1517  }
1518  ctx.check_error();
1519  return expr(ctx, r);
1520  }
1521 
1522  inline expr mk_or(expr_vector const& args) {
1523  array<Z3_ast> _args(args);
1524  Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
1525  args.check_error();
1526  return expr(args.ctx(), r);
1527  }
1528  inline expr mk_and(expr_vector const& args) {
1529  array<Z3_ast> _args(args);
1530  Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
1531  args.check_error();
1532  return expr(args.ctx(), r);
1533  }
1534 
1535 
1536  class func_entry : public object {
1537  Z3_func_entry m_entry;
1538  void init(Z3_func_entry e) {
1539  m_entry = e;
1540  Z3_func_entry_inc_ref(ctx(), m_entry);
1541  }
1542  public:
1543  func_entry(context & c, Z3_func_entry e):object(c) { init(e); }
1544  func_entry(func_entry const & s):object(s) { init(s.m_entry); }
1545  ~func_entry() { Z3_func_entry_dec_ref(ctx(), m_entry); }
1546  operator Z3_func_entry() const { return m_entry; }
1548  Z3_func_entry_inc_ref(s.ctx(), s.m_entry);
1549  Z3_func_entry_dec_ref(ctx(), m_entry);
1550  m_ctx = s.m_ctx;
1551  m_entry = s.m_entry;
1552  return *this;
1553  }
1554  expr value() const { Z3_ast r = Z3_func_entry_get_value(ctx(), m_entry); check_error(); return expr(ctx(), r); }
1555  unsigned num_args() const { unsigned r = Z3_func_entry_get_num_args(ctx(), m_entry); check_error(); return r; }
1556  expr arg(unsigned i) const { Z3_ast r = Z3_func_entry_get_arg(ctx(), m_entry, i); check_error(); return expr(ctx(), r); }
1557  };
1558 
1559  class func_interp : public object {
1560  Z3_func_interp m_interp;
1561  void init(Z3_func_interp e) {
1562  m_interp = e;
1563  Z3_func_interp_inc_ref(ctx(), m_interp);
1564  }
1565  public:
1566  func_interp(context & c, Z3_func_interp e):object(c) { init(e); }
1567  func_interp(func_interp const & s):object(s) { init(s.m_interp); }
1568  ~func_interp() { Z3_func_interp_dec_ref(ctx(), m_interp); }
1569  operator Z3_func_interp() const { return m_interp; }
1571  Z3_func_interp_inc_ref(s.ctx(), s.m_interp);
1572  Z3_func_interp_dec_ref(ctx(), m_interp);
1573  m_ctx = s.m_ctx;
1574  m_interp = s.m_interp;
1575  return *this;
1576  }
1577  expr else_value() const { Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), r); }
1578  unsigned num_entries() const { unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }
1579  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); }
1580  };
1581 
1582  class model : public object {
1583  Z3_model m_model;
1584  void init(Z3_model m) {
1585  m_model = m;
1586  Z3_model_inc_ref(ctx(), m);
1587  }
1588  public:
1589  model(context & c, Z3_model m):object(c) { init(m); }
1590  model(model const & s):object(s) { init(s.m_model); }
1591  ~model() { Z3_model_dec_ref(ctx(), m_model); }
1592  operator Z3_model() const { return m_model; }
1593  model & operator=(model const & s) {
1594  Z3_model_inc_ref(s.ctx(), s.m_model);
1595  Z3_model_dec_ref(ctx(), m_model);
1596  m_ctx = s.m_ctx;
1597  m_model = s.m_model;
1598  return *this;
1599  }
1600 
1601  expr eval(expr const & n, bool model_completion=false) const {
1602  check_context(*this, n);
1603  Z3_ast r = 0;
1604  Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
1605  check_error();
1606  if (status == Z3_FALSE)
1607  throw exception("failed to evaluate expression");
1608  return expr(ctx(), r);
1609  }
1610 
1611  unsigned num_consts() const { return Z3_model_get_num_consts(ctx(), m_model); }
1612  unsigned num_funcs() const { return Z3_model_get_num_funcs(ctx(), m_model); }
1613  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); }
1614  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); }
1615  unsigned size() const { return num_consts() + num_funcs(); }
1616  func_decl operator[](int i) const {
1617  assert(0 <= i);
1618  return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
1619  }
1620 
1621  // returns interpretation of constant declaration c.
1622  // If c is not assigned any value in the model it returns
1623  // an expression with a null ast reference.
1625  check_context(*this, c);
1626  Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);
1627  check_error();
1628  return expr(ctx(), r);
1629  }
1631  check_context(*this, f);
1632  Z3_func_interp r = Z3_model_get_func_interp(ctx(), m_model, f);
1633  check_error();
1634  return func_interp(ctx(), r);
1635  }
1636 
1637  // returns true iff the model contains an interpretation
1638  // for function f.
1639  bool has_interp(func_decl f) const {
1640  check_context(*this, f);
1641  return 0 != Z3_model_has_interp(ctx(), m_model, f);
1642  }
1643 
1644  friend std::ostream & operator<<(std::ostream & out, model const & m);
1645  };
1646  inline std::ostream & operator<<(std::ostream & out, model const & m) { out << Z3_model_to_string(m.ctx(), m); return out; }
1647 
1648  class stats : public object {
1649  Z3_stats m_stats;
1650  void init(Z3_stats e) {
1651  m_stats = e;
1652  Z3_stats_inc_ref(ctx(), m_stats);
1653  }
1654  public:
1655  stats(context & c):object(c), m_stats(0) {}
1656  stats(context & c, Z3_stats e):object(c) { init(e); }
1657  stats(stats const & s):object(s) { init(s.m_stats); }
1658  ~stats() { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); }
1659  operator Z3_stats() const { return m_stats; }
1660  stats & operator=(stats const & s) {
1661  Z3_stats_inc_ref(s.ctx(), s.m_stats);
1662  if (m_stats) Z3_stats_dec_ref(ctx(), m_stats);
1663  m_ctx = s.m_ctx;
1664  m_stats = s.m_stats;
1665  return *this;
1666  }
1667  unsigned size() const { return Z3_stats_size(ctx(), m_stats); }
1668  std::string key(unsigned i) const { Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; }
1669  bool is_uint(unsigned i) const { Z3_bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r != 0; }
1670  bool is_double(unsigned i) const { Z3_bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r != 0; }
1671  unsigned uint_value(unsigned i) const { unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; }
1672  double double_value(unsigned i) const { double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
1673  friend std::ostream & operator<<(std::ostream & out, stats const & s);
1674  };
1675  inline std::ostream & operator<<(std::ostream & out, stats const & s) { out << Z3_stats_to_string(s.ctx(), s); return out; }
1676 
1677 
1678  inline std::ostream & operator<<(std::ostream & out, check_result r) {
1679  if (r == unsat) out << "unsat";
1680  else if (r == sat) out << "sat";
1681  else out << "unknown";
1682  return out;
1683  }
1684 
1685 
1686  class solver : public object {
1687  Z3_solver m_solver;
1688  void init(Z3_solver s) {
1689  m_solver = s;
1690  Z3_solver_inc_ref(ctx(), s);
1691  }
1692  public:
1693  struct simple {};
1694  struct translate {};
1695  solver(context & c):object(c) { init(Z3_mk_solver(c)); }
1697  solver(context & c, Z3_solver s):object(c) { init(s); }
1698  solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); }
1699  solver(context & c, solver const& src, translate): object(c) { init(Z3_solver_translate(src.ctx(), src, c)); }
1700  solver(solver const & s):object(s) { init(s.m_solver); }
1701  ~solver() { Z3_solver_dec_ref(ctx(), m_solver); }
1702  operator Z3_solver() const { return m_solver; }
1703  solver & operator=(solver const & s) {
1704  Z3_solver_inc_ref(s.ctx(), s.m_solver);
1705  Z3_solver_dec_ref(ctx(), m_solver);
1706  m_ctx = s.m_ctx;
1707  m_solver = s.m_solver;
1708  return *this;
1709  }
1710  void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
1711  void push() { Z3_solver_push(ctx(), m_solver); check_error(); }
1712  void pop(unsigned n = 1) { Z3_solver_pop(ctx(), m_solver, n); check_error(); }
1713  void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); }
1714  void add(expr const & e) { assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); }
1715  void add(expr const & e, expr const & p) {
1716  assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
1717  Z3_solver_assert_and_track(ctx(), m_solver, e, p);
1718  check_error();
1719  }
1720  void add(expr const & e, char const * p) {
1721  add(e, ctx().bool_const(p));
1722  }
1723  check_result check() { Z3_lbool r = Z3_solver_check(ctx(), m_solver); check_error(); return to_check_result(r); }
1724  check_result check(unsigned n, expr * const assumptions) {
1725  array<Z3_ast> _assumptions(n);
1726  for (unsigned i = 0; i < n; i++) {
1727  check_context(*this, assumptions[i]);
1728  _assumptions[i] = assumptions[i];
1729  }
1730  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
1731  check_error();
1732  return to_check_result(r);
1733  }
1734  check_result check(expr_vector assumptions) {
1735  unsigned n = assumptions.size();
1736  array<Z3_ast> _assumptions(n);
1737  for (unsigned i = 0; i < n; i++) {
1738  check_context(*this, assumptions[i]);
1739  _assumptions[i] = assumptions[i];
1740  }
1741  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
1742  check_error();
1743  return to_check_result(r);
1744  }
1745  model get_model() const { Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }
1746  check_result consequences(expr_vector& assumptions, expr_vector& vars, expr_vector& conseq) {
1747  Z3_lbool r = Z3_solver_get_consequences(ctx(), m_solver, assumptions, vars, conseq);
1748  check_error();
1749  return to_check_result(r);
1750  }
1751  std::string reason_unknown() const { Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }
1752  stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }
1753  expr_vector unsat_core() const { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
1754  expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
1755  expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
1756  friend std::ostream & operator<<(std::ostream & out, solver const & s);
1757 
1758  std::string to_smt2(char const* status = "unknown") {
1759  array<Z3_ast> es(assertions());
1760  Z3_ast const* fmls = es.ptr();
1761  Z3_ast fml = 0;
1762  unsigned sz = es.size();
1763  if (sz > 0) {
1764  --sz;
1765  fml = fmls[sz];
1766  }
1767  else {
1768  fml = ctx().bool_val(true);
1769  }
1770  return std::string(Z3_benchmark_to_smtlib_string(
1771  ctx(),
1772  "", "", status, "",
1773  sz,
1774  fmls,
1775  fml));
1776  }
1778 
1779  };
1780  inline std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
1781 
1782  class goal : public object {
1783  Z3_goal m_goal;
1784  void init(Z3_goal s) {
1785  m_goal = s;
1786  Z3_goal_inc_ref(ctx(), s);
1787  }
1788  public:
1789  goal(context & c, bool models=true, bool unsat_cores=false, bool proofs=false):object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); }
1790  goal(context & c, Z3_goal s):object(c) { init(s); }
1791  goal(goal const & s):object(s) { init(s.m_goal); }
1792  ~goal() { Z3_goal_dec_ref(ctx(), m_goal); }
1793  operator Z3_goal() const { return m_goal; }
1794  goal & operator=(goal const & s) {
1795  Z3_goal_inc_ref(s.ctx(), s.m_goal);
1796  Z3_goal_dec_ref(ctx(), m_goal);
1797  m_ctx = s.m_ctx;
1798  m_goal = s.m_goal;
1799  return *this;
1800  }
1801  void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
1802  unsigned size() const { return Z3_goal_size(ctx(), m_goal); }
1803  expr operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
1804  Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); }
1805  bool inconsistent() const { return Z3_goal_inconsistent(ctx(), m_goal) != 0; }
1806  unsigned depth() const { return Z3_goal_depth(ctx(), m_goal); }
1807  void reset() { Z3_goal_reset(ctx(), m_goal); }
1808  unsigned num_exprs() const { return Z3_goal_num_exprs(ctx(), m_goal); }
1809  bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal) != 0; }
1810  bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal) != 0; }
1811  expr as_expr() const {
1812  unsigned n = size();
1813  if (n == 0)
1814  return ctx().bool_val(true);
1815  else if (n == 1)
1816  return operator[](0);
1817  else {
1818  array<Z3_ast> args(n);
1819  for (unsigned i = 0; i < n; i++)
1820  args[i] = operator[](i);
1821  return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
1822  }
1823  }
1824  friend std::ostream & operator<<(std::ostream & out, goal const & g);
1825  };
1826  inline std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; }
1827 
1828  class apply_result : public object {
1829  Z3_apply_result m_apply_result;
1830  void init(Z3_apply_result s) {
1831  m_apply_result = s;
1832  Z3_apply_result_inc_ref(ctx(), s);
1833  }
1834  public:
1835  apply_result(context & c, Z3_apply_result s):object(c) { init(s); }
1836  apply_result(apply_result const & s):object(s) { init(s.m_apply_result); }
1837  ~apply_result() { Z3_apply_result_dec_ref(ctx(), m_apply_result); }
1838  operator Z3_apply_result() const { return m_apply_result; }
1840  Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result);
1841  Z3_apply_result_dec_ref(ctx(), m_apply_result);
1842  m_ctx = s.m_ctx;
1843  m_apply_result = s.m_apply_result;
1844  return *this;
1845  }
1846  unsigned size() const { return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }
1847  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); }
1848  model convert_model(model const & m, unsigned i = 0) const {
1849  check_context(*this, m);
1850  Z3_model new_m = Z3_apply_result_convert_model(ctx(), m_apply_result, i, m);
1851  check_error();
1852  return model(ctx(), new_m);
1853  }
1854  friend std::ostream & operator<<(std::ostream & out, apply_result const & r);
1855  };
1856  inline std::ostream & operator<<(std::ostream & out, apply_result const & r) { out << Z3_apply_result_to_string(r.ctx(), r); return out; }
1857 
1858  class tactic : public object {
1859  Z3_tactic m_tactic;
1860  void init(Z3_tactic s) {
1861  m_tactic = s;
1862  Z3_tactic_inc_ref(ctx(), s);
1863  }
1864  public:
1865  tactic(context & c, char const * name):object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); }
1866  tactic(context & c, Z3_tactic s):object(c) { init(s); }
1867  tactic(tactic const & s):object(s) { init(s.m_tactic); }
1868  ~tactic() { Z3_tactic_dec_ref(ctx(), m_tactic); }
1869  operator Z3_tactic() const { return m_tactic; }
1870  tactic & operator=(tactic const & s) {
1871  Z3_tactic_inc_ref(s.ctx(), s.m_tactic);
1872  Z3_tactic_dec_ref(ctx(), m_tactic);
1873  m_ctx = s.m_ctx;
1874  m_tactic = s.m_tactic;
1875  return *this;
1876  }
1877  solver mk_solver() const { Z3_solver r = Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error(); return solver(ctx(), r); }
1878  apply_result apply(goal const & g) const {
1879  check_context(*this, g);
1880  Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g);
1881  check_error();
1882  return apply_result(ctx(), r);
1883  }
1884  apply_result operator()(goal const & g) const {
1885  return apply(g);
1886  }
1887  std::string help() const { char const * r = Z3_tactic_get_help(ctx(), m_tactic); check_error(); return r; }
1888  friend tactic operator&(tactic const & t1, tactic const & t2);
1889  friend tactic operator|(tactic const & t1, tactic const & t2);
1890  friend tactic repeat(tactic const & t, unsigned max);
1891  friend tactic with(tactic const & t, params const & p);
1892  friend tactic try_for(tactic const & t, unsigned ms);
1894  };
1895 
1896  inline tactic operator&(tactic const & t1, tactic const & t2) {
1897  check_context(t1, t2);
1898  Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
1899  t1.check_error();
1900  return tactic(t1.ctx(), r);
1901  }
1902 
1903  inline tactic operator|(tactic const & t1, tactic const & t2) {
1904  check_context(t1, t2);
1905  Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
1906  t1.check_error();
1907  return tactic(t1.ctx(), r);
1908  }
1909 
1910  inline tactic repeat(tactic const & t, unsigned max=UINT_MAX) {
1911  Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
1912  t.check_error();
1913  return tactic(t.ctx(), r);
1914  }
1915 
1916  inline tactic with(tactic const & t, params const & p) {
1917  Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
1918  t.check_error();
1919  return tactic(t.ctx(), r);
1920  }
1921  inline tactic try_for(tactic const & t, unsigned ms) {
1922  Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
1923  t.check_error();
1924  return tactic(t.ctx(), r);
1925  }
1926 
1927 
1928  class probe : public object {
1929  Z3_probe m_probe;
1930  void init(Z3_probe s) {
1931  m_probe = s;
1932  Z3_probe_inc_ref(ctx(), s);
1933  }
1934  public:
1935  probe(context & c, char const * name):object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); }
1936  probe(context & c, double val):object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); }
1937  probe(context & c, Z3_probe s):object(c) { init(s); }
1938  probe(probe const & s):object(s) { init(s.m_probe); }
1939  ~probe() { Z3_probe_dec_ref(ctx(), m_probe); }
1940  operator Z3_probe() const { return m_probe; }
1941  probe & operator=(probe const & s) {
1942  Z3_probe_inc_ref(s.ctx(), s.m_probe);
1943  Z3_probe_dec_ref(ctx(), m_probe);
1944  m_ctx = s.m_ctx;
1945  m_probe = s.m_probe;
1946  return *this;
1947  }
1948  double apply(goal const & g) const { double r = Z3_probe_apply(ctx(), m_probe, g); check_error(); return r; }
1949  double operator()(goal const & g) const { return apply(g); }
1950  friend probe operator<=(probe const & p1, probe const & p2);
1951  friend probe operator<=(probe const & p1, double p2);
1952  friend probe operator<=(double p1, probe const & p2);
1953  friend probe operator>=(probe const & p1, probe const & p2);
1954  friend probe operator>=(probe const & p1, double p2);
1955  friend probe operator>=(double p1, probe const & p2);
1956  friend probe operator<(probe const & p1, probe const & p2);
1957  friend probe operator<(probe const & p1, double p2);
1958  friend probe operator<(double p1, probe const & p2);
1959  friend probe operator>(probe const & p1, probe const & p2);
1960  friend probe operator>(probe const & p1, double p2);
1961  friend probe operator>(double p1, probe const & p2);
1962  friend probe operator==(probe const & p1, probe const & p2);
1963  friend probe operator==(probe const & p1, double p2);
1964  friend probe operator==(double p1, probe const & p2);
1965  friend probe operator&&(probe const & p1, probe const & p2);
1966  friend probe operator||(probe const & p1, probe const & p2);
1967  friend probe operator!(probe const & p);
1968  };
1969 
1970  inline probe operator<=(probe const & p1, probe const & p2) {
1971  check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1972  }
1973  inline probe operator<=(probe const & p1, double p2) { return p1 <= probe(p1.ctx(), p2); }
1974  inline probe operator<=(double p1, probe const & p2) { return probe(p2.ctx(), p1) <= p2; }
1975  inline probe operator>=(probe const & p1, probe const & p2) {
1976  check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1977  }
1978  inline probe operator>=(probe const & p1, double p2) { return p1 >= probe(p1.ctx(), p2); }
1979  inline probe operator>=(double p1, probe const & p2) { return probe(p2.ctx(), p1) >= p2; }
1980  inline probe operator<(probe const & p1, probe const & p2) {
1981  check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1982  }
1983  inline probe operator<(probe const & p1, double p2) { return p1 < probe(p1.ctx(), p2); }
1984  inline probe operator<(double p1, probe const & p2) { return probe(p2.ctx(), p1) < p2; }
1985  inline probe operator>(probe const & p1, probe const & p2) {
1986  check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1987  }
1988  inline probe operator>(probe const & p1, double p2) { return p1 > probe(p1.ctx(), p2); }
1989  inline probe operator>(double p1, probe const & p2) { return probe(p2.ctx(), p1) > p2; }
1990  inline probe operator==(probe const & p1, probe const & p2) {
1991  check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1992  }
1993  inline probe operator==(probe const & p1, double p2) { return p1 == probe(p1.ctx(), p2); }
1994  inline probe operator==(double p1, probe const & p2) { return probe(p2.ctx(), p1) == p2; }
1995  inline probe operator&&(probe const & p1, probe const & p2) {
1996  check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1997  }
1998  inline probe operator||(probe const & p1, probe const & p2) {
1999  check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2000  }
2001  inline probe operator!(probe const & p) {
2002  Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
2003  }
2004 
2005  class optimize : public object {
2006  Z3_optimize m_opt;
2007  public:
2008  class handle {
2009  unsigned m_h;
2010  public:
2011  handle(unsigned h): m_h(h) {}
2012  unsigned h() const { return m_h; }
2013  };
2014  optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }
2015  ~optimize() { Z3_optimize_dec_ref(ctx(), m_opt); }
2016  operator Z3_optimize() const { return m_opt; }
2017  void add(expr const& e) {
2018  assert(e.is_bool());
2019  Z3_optimize_assert(ctx(), m_opt, e);
2020  }
2021  handle add(expr const& e, unsigned weight) {
2022  assert(e.is_bool());
2023  std::stringstream strm;
2024  strm << weight;
2025  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, strm.str().c_str(), 0));
2026  }
2027  handle add(expr const& e, char const* weight) {
2028  assert(e.is_bool());
2029  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0));
2030  }
2031  handle maximize(expr const& e) {
2032  return handle(Z3_optimize_maximize(ctx(), m_opt, e));
2033  }
2034  handle minimize(expr const& e) {
2035  return handle(Z3_optimize_minimize(ctx(), m_opt, e));
2036  }
2037  void push() {
2038  Z3_optimize_push(ctx(), m_opt);
2039  }
2040  void pop() {
2041  Z3_optimize_pop(ctx(), m_opt);
2042  }
2043  check_result check() { Z3_lbool r = Z3_optimize_check(ctx(), m_opt); check_error(); return to_check_result(r); }
2044  model get_model() const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }
2045  void set(params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }
2046  expr lower(handle const& h) {
2047  Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());
2048  check_error();
2049  return expr(ctx(), r);
2050  }
2051  expr upper(handle const& h) {
2052  Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h());
2053  check_error();
2054  return expr(ctx(), r);
2055  }
2056  expr_vector assertions() const { Z3_ast_vector r = Z3_optimize_get_assertions(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
2057  expr_vector objectives() const { Z3_ast_vector r = Z3_optimize_get_objectives(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
2058  stats statistics() const { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); }
2059  friend std::ostream & operator<<(std::ostream & out, optimize const & s);
2060  void from_file(char const* filename) { Z3_optimize_from_file(ctx(), m_opt, filename); check_error(); }
2061  void from_string(char const* constraints) { Z3_optimize_from_string(ctx(), m_opt, constraints); check_error(); }
2062  std::string help() const { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error(); return r; }
2063  };
2064  inline std::ostream & operator<<(std::ostream & out, optimize const & s) { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }
2065 
2066  inline tactic fail_if(probe const & p) {
2067  Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
2068  p.check_error();
2069  return tactic(p.ctx(), r);
2070  }
2071  inline tactic when(probe const & p, tactic const & t) {
2072  check_context(p, t);
2073  Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
2074  t.check_error();
2075  return tactic(t.ctx(), r);
2076  }
2077  inline tactic cond(probe const & p, tactic const & t1, tactic const & t2) {
2078  check_context(p, t1); check_context(p, t2);
2079  Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
2080  t1.check_error();
2081  return tactic(t1.ctx(), r);
2082  }
2083 
2084  inline symbol context::str_symbol(char const * s) { Z3_symbol r = Z3_mk_string_symbol(m_ctx, s); check_error(); return symbol(*this, r); }
2085  inline symbol context::int_symbol(int n) { Z3_symbol r = Z3_mk_int_symbol(m_ctx, n); check_error(); return symbol(*this, r); }
2086 
2087  inline sort context::bool_sort() { Z3_sort s = Z3_mk_bool_sort(m_ctx); check_error(); return sort(*this, s); }
2088  inline sort context::int_sort() { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }
2089  inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
2090  inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
2091  inline sort context::string_sort() { Z3_sort s = Z3_mk_string_sort(m_ctx); check_error(); return sort(*this, s); }
2092  inline sort context::seq_sort(sort& s) { Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); }
2093  inline sort context::re_sort(sort& s) { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
2094 
2095  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); }
2096  inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
2097  array<Z3_symbol> _enum_names(n);
2098  for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
2099  array<Z3_func_decl> _cs(n);
2100  array<Z3_func_decl> _ts(n);
2101  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2102  sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
2103  check_error();
2104  for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
2105  return s;
2106  }
2107  inline sort context::uninterpreted_sort(char const* name) {
2108  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2109  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
2110  }
2112  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
2113  }
2114 
2115  inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
2116  array<Z3_sort> args(arity);
2117  for (unsigned i = 0; i < arity; i++) {
2118  check_context(domain[i], range);
2119  args[i] = domain[i];
2120  }
2121  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
2122  check_error();
2123  return func_decl(*this, f);
2124  }
2125 
2126  inline func_decl context::function(char const * name, unsigned arity, sort const * domain, sort const & range) {
2127  return function(range.ctx().str_symbol(name), arity, domain, range);
2128  }
2129 
2130  inline func_decl context::function(symbol const& name, sort_vector const& domain, sort const& range) {
2131  array<Z3_sort> args(domain.size());
2132  for (unsigned i = 0; i < domain.size(); i++) {
2133  check_context(domain[i], range);
2134  args[i] = domain[i];
2135  }
2136  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
2137  check_error();
2138  return func_decl(*this, f);
2139  }
2140 
2141  inline func_decl context::function(char const * name, sort_vector const& domain, sort const& range) {
2142  return function(range.ctx().str_symbol(name), domain, range);
2143  }
2144 
2145 
2146  inline func_decl context::function(char const * name, sort const & domain, sort const & range) {
2147  check_context(domain, range);
2148  Z3_sort args[1] = { domain };
2149  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
2150  check_error();
2151  return func_decl(*this, f);
2152  }
2153 
2154  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & range) {
2155  check_context(d1, range); check_context(d2, range);
2156  Z3_sort args[2] = { d1, d2 };
2157  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
2158  check_error();
2159  return func_decl(*this, f);
2160  }
2161 
2162  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
2163  check_context(d1, range); check_context(d2, range); check_context(d3, range);
2164  Z3_sort args[3] = { d1, d2, d3 };
2165  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
2166  check_error();
2167  return func_decl(*this, f);
2168  }
2169 
2170  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
2171  check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range);
2172  Z3_sort args[4] = { d1, d2, d3, d4 };
2173  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
2174  check_error();
2175  return func_decl(*this, f);
2176  }
2177 
2178  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) {
2179  check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range); check_context(d5, range);
2180  Z3_sort args[5] = { d1, d2, d3, d4, d5 };
2181  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
2182  check_error();
2183  return func_decl(*this, f);
2184  }
2185 
2186  inline expr context::constant(symbol const & name, sort const & s) {
2187  Z3_ast r = Z3_mk_const(m_ctx, name, s);
2188  check_error();
2189  return expr(*this, r);
2190  }
2191  inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); }
2192  inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); }
2193  inline expr context::int_const(char const * name) { return constant(name, int_sort()); }
2194  inline expr context::real_const(char const * name) { return constant(name, real_sort()); }
2195  inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); }
2196 
2197  inline expr context::bool_val(bool b) { return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }
2198 
2199  inline expr context::int_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
2200  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); }
2201  inline expr context::int_val(__int64 n) { Z3_ast r = Z3_mk_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
2202  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); }
2203  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); }
2204 
2205  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); }
2206  inline expr context::real_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
2207  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); }
2208  inline expr context::real_val(__int64 n) { Z3_ast r = Z3_mk_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
2209  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); }
2210  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); }
2211 
2212  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); }
2213  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); }
2214  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); }
2215  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); }
2216  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); }
2217 
2218  inline expr context::string_val(char const* s) { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
2219  inline expr context::string_val(std::string const& s) { Z3_ast r = Z3_mk_string(m_ctx, s.c_str()); check_error(); return expr(*this, r); }
2220 
2221  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); }
2222 
2223  inline expr func_decl::operator()(unsigned n, expr const * args) const {
2224  array<Z3_ast> _args(n);
2225  for (unsigned i = 0; i < n; i++) {
2226  check_context(*this, args[i]);
2227  _args[i] = args[i];
2228  }
2229  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
2230  check_error();
2231  return expr(ctx(), r);
2232 
2233  }
2234  inline expr func_decl::operator()(expr_vector const& args) const {
2235  array<Z3_ast> _args(args.size());
2236  for (unsigned i = 0; i < args.size(); i++) {
2237  check_context(*this, args[i]);
2238  _args[i] = args[i];
2239  }
2240  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
2241  check_error();
2242  return expr(ctx(), r);
2243  }
2244  inline expr func_decl::operator()() const {
2245  Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
2246  ctx().check_error();
2247  return expr(ctx(), r);
2248  }
2249  inline expr func_decl::operator()(expr const & a) const {
2250  check_context(*this, a);
2251  Z3_ast args[1] = { a };
2252  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
2253  ctx().check_error();
2254  return expr(ctx(), r);
2255  }
2256  inline expr func_decl::operator()(int a) const {
2257  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
2258  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
2259  ctx().check_error();
2260  return expr(ctx(), r);
2261  }
2262  inline expr func_decl::operator()(expr const & a1, expr const & a2) const {
2263  check_context(*this, a1); check_context(*this, a2);
2264  Z3_ast args[2] = { a1, a2 };
2265  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
2266  ctx().check_error();
2267  return expr(ctx(), r);
2268  }
2269  inline expr func_decl::operator()(expr const & a1, int a2) const {
2270  check_context(*this, a1);
2271  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
2272  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
2273  ctx().check_error();
2274  return expr(ctx(), r);
2275  }
2276  inline expr func_decl::operator()(int a1, expr const & a2) const {
2277  check_context(*this, a2);
2278  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
2279  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
2280  ctx().check_error();
2281  return expr(ctx(), r);
2282  }
2283  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3) const {
2284  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
2285  Z3_ast args[3] = { a1, a2, a3 };
2286  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
2287  ctx().check_error();
2288  return expr(ctx(), r);
2289  }
2290  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const {
2291  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
2292  Z3_ast args[4] = { a1, a2, a3, a4 };
2293  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
2294  ctx().check_error();
2295  return expr(ctx(), r);
2296  }
2297  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const {
2298  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
2299  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
2300  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
2301  ctx().check_error();
2302  return expr(ctx(), r);
2303  }
2304 
2305  inline expr to_real(expr const & a) { Z3_ast r = Z3_mk_int2real(a.ctx(), a); a.check_error(); return expr(a.ctx(), r); }
2306 
2307  inline func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
2308  return range.ctx().function(name, arity, domain, range);
2309  }
2310  inline func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range) {
2311  return range.ctx().function(name, arity, domain, range);
2312  }
2313  inline func_decl function(char const * name, sort const & domain, sort const & range) {
2314  return range.ctx().function(name, domain, range);
2315  }
2316  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range) {
2317  return range.ctx().function(name, d1, d2, range);
2318  }
2319  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
2320  return range.ctx().function(name, d1, d2, d3, range);
2321  }
2322  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
2323  return range.ctx().function(name, d1, d2, d3, d4, range);
2324  }
2325  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) {
2326  return range.ctx().function(name, d1, d2, d3, d4, d5, range);
2327  }
2328 
2329  inline expr select(expr const & a, expr const & i) {
2330  check_context(a, i);
2331  Z3_ast r = Z3_mk_select(a.ctx(), a, i);
2332  a.check_error();
2333  return expr(a.ctx(), r);
2334  }
2335  inline expr select(expr const & a, int i) { return select(a, a.ctx().num_val(i, a.get_sort().array_domain())); }
2336  inline expr store(expr const & a, expr const & i, expr const & v) {
2337  check_context(a, i); check_context(a, v);
2338  Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
2339  a.check_error();
2340  return expr(a.ctx(), r);
2341  }
2342  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); }
2343  inline expr store(expr const & a, expr i, int v) { return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
2344  inline expr store(expr const & a, int i, int v) {
2345  return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
2346  }
2347 
2348 #define MK_EXPR1(_fn, _arg) \
2349  Z3_ast r = _fn(_arg.ctx(), _arg); \
2350  _arg.check_error(); \
2351  return expr(_arg.ctx(), r);
2352 
2353 #define MK_EXPR2(_fn, _arg1, _arg2) \
2354  check_context(_arg1, _arg2); \
2355  Z3_ast r = _fn(_arg1.ctx(), _arg1, _arg2); \
2356  _arg1.check_error(); \
2357  return expr(_arg1.ctx(), r);
2358 
2359  inline expr const_array(sort const & d, expr const & v) {
2360  MK_EXPR2(Z3_mk_const_array, d, v);
2361  }
2362 
2363  inline expr empty_set(sort const& s) {
2365  }
2366 
2367  inline expr full_set(sort const& s) {
2369  }
2370 
2371  inline expr set_add(expr const& s, expr const& e) {
2372  MK_EXPR2(Z3_mk_set_add, s, e);
2373  }
2374 
2375  inline expr set_del(expr const& s, expr const& e) {
2376  MK_EXPR2(Z3_mk_set_del, s, e);
2377  }
2378 
2379  inline expr set_union(expr const& a, expr const& b) {
2380  check_context(a, b);
2381  Z3_ast es[2] = { a, b };
2382  Z3_ast r = Z3_mk_set_union(a.ctx(), 2, es);
2383  a.check_error();
2384  return expr(a.ctx(), r);
2385  }
2386 
2387  inline expr set_intersect(expr const& a, expr const& b) {
2388  check_context(a, b);
2389  Z3_ast es[2] = { a, b };
2390  Z3_ast r = Z3_mk_set_intersect(a.ctx(), 2, es);
2391  a.check_error();
2392  return expr(a.ctx(), r);
2393  }
2394 
2395  inline expr set_difference(expr const& a, expr const& b) {
2397  }
2398 
2399  inline expr set_complement(expr const& a) {
2401  }
2402 
2403  inline expr set_member(expr const& s, expr const& e) {
2404  MK_EXPR2(Z3_mk_set_member, s, e);
2405  }
2406 
2407  inline expr set_subset(expr const& a, expr const& b) {
2408  MK_EXPR2(Z3_mk_set_subset, a, b);
2409  }
2410 
2411  // sequence and regular expression operations.
2412  // union is +
2413  // concat is overloaded to handle sequences and regular expressions
2414 
2415  inline expr empty(sort const& s) {
2416  Z3_ast r = Z3_mk_seq_empty(s.ctx(), s);
2417  s.check_error();
2418  return expr(s.ctx(), r);
2419  }
2420  inline expr suffixof(expr const& a, expr const& b) {
2421  check_context(a, b);
2422  Z3_ast r = Z3_mk_seq_suffix(a.ctx(), a, b);
2423  a.check_error();
2424  return expr(a.ctx(), r);
2425  }
2426  inline expr prefixof(expr const& a, expr const& b) {
2427  check_context(a, b);
2428  Z3_ast r = Z3_mk_seq_prefix(a.ctx(), a, b);
2429  a.check_error();
2430  return expr(a.ctx(), r);
2431  }
2432  inline expr indexof(expr const& s, expr const& substr, expr const& offset) {
2433  check_context(s, substr); check_context(s, offset);
2434  Z3_ast r = Z3_mk_seq_index(s.ctx(), s, substr, offset);
2435  s.check_error();
2436  return expr(s.ctx(), r);
2437  }
2438  inline expr to_re(expr const& s) {
2439  Z3_ast r = Z3_mk_seq_to_re(s.ctx(), s);
2440  s.check_error();
2441  return expr(s.ctx(), r);
2442  }
2443  inline expr in_re(expr const& s, expr const& re) {
2444  check_context(s, re);
2445  Z3_ast r = Z3_mk_seq_in_re(s.ctx(), s, re);
2446  s.check_error();
2447  return expr(s.ctx(), r);
2448  }
2449  inline expr plus(expr const& re) {
2450  Z3_ast r = Z3_mk_re_plus(re.ctx(), re);
2451  re.check_error();
2452  return expr(re.ctx(), r);
2453  }
2454  inline expr option(expr const& re) {
2455  Z3_ast r = Z3_mk_re_option(re.ctx(), re);
2456  re.check_error();
2457  return expr(re.ctx(), r);
2458  }
2459  inline expr star(expr const& re) {
2460  Z3_ast r = Z3_mk_re_star(re.ctx(), re);
2461  re.check_error();
2462  return expr(re.ctx(), r);
2463  }
2464 
2465  inline expr interpolant(expr const& a) {
2466  return expr(a.ctx(), Z3_mk_interpolant(a.ctx(), a));
2467  }
2468 
2469  inline expr context::parse_string(char const* s) {
2470  Z3_ast r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0);
2471  check_error();
2472  return expr(*this, r);
2473 
2474  }
2475  inline expr context::parse_file(char const* s) {
2476  Z3_ast r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0);
2477  check_error();
2478  return expr(*this, r);
2479  }
2480 
2481  inline expr context::parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls) {
2482  array<Z3_symbol> sort_names(sorts.size());
2483  array<Z3_symbol> decl_names(decls.size());
2484  array<Z3_sort> sorts1(sorts);
2485  array<Z3_func_decl> decls1(decls);
2486  for (unsigned i = 0; i < sorts.size(); ++i) {
2487  sort_names[i] = sorts[i].name();
2488  }
2489  for (unsigned i = 0; i < decls.size(); ++i) {
2490  decl_names[i] = decls[i].name();
2491  }
2492  Z3_ast r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
2493  check_error();
2494  return expr(*this, r);
2495  }
2496 
2497  inline expr context::parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls) {
2498  array<Z3_symbol> sort_names(sorts.size());
2499  array<Z3_symbol> decl_names(decls.size());
2500  array<Z3_sort> sorts1(sorts);
2501  array<Z3_func_decl> decls1(decls);
2502  for (unsigned i = 0; i < sorts.size(); ++i) {
2503  sort_names[i] = sorts[i].name();
2504  }
2505  for (unsigned i = 0; i < decls.size(); ++i) {
2506  decl_names[i] = decls[i].name();
2507  }
2508  Z3_ast r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
2509  check_error();
2510  return expr(*this, r);
2511  }
2512 
2513 
2514  inline check_result context::compute_interpolant(expr const& pat, params const& p, expr_vector& i, model& m) {
2515  Z3_ast_vector interp = 0;
2516  Z3_model mdl = 0;
2517  Z3_lbool r = Z3_compute_interpolant(*this, pat, p, &interp, &mdl);
2518  switch (r) {
2519  case Z3_L_FALSE:
2520  i = expr_vector(*this, interp);
2521  break;
2522  case Z3_L_TRUE:
2523  m = model(*this, mdl);
2524  break;
2525  case Z3_L_UNDEF:
2526  break;
2527  }
2528  return to_check_result(r);
2529  }
2530 
2531  inline expr_vector context::get_interpolant(expr const& proof, expr const& pat, params const& p) {
2532  return expr_vector(*this, Z3_get_interpolant(*this, proof, pat, p));
2533  }
2534 
2535  inline expr expr::substitute(expr_vector const& src, expr_vector const& dst) {
2536  assert(src.size() == dst.size());
2537  array<Z3_ast> _src(src.size());
2538  array<Z3_ast> _dst(dst.size());
2539  for (unsigned i = 0; i < src.size(); ++i) {
2540  _src[i] = src[i];
2541  _dst[i] = dst[i];
2542  }
2543  Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
2544  check_error();
2545  return expr(ctx(), r);
2546  }
2547 
2548  inline expr expr::substitute(expr_vector const& dst) {
2549  array<Z3_ast> _dst(dst.size());
2550  for (unsigned i = 0; i < dst.size(); ++i) {
2551  _dst[i] = dst[i];
2552  }
2553  Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
2554  check_error();
2555  return expr(ctx(), r);
2556  }
2557 
2558 
2559 
2560 }
2561 
2564 
2565 #endif
2566 
ast_vector_tpl(context &c)
Definition: z3++.h:1384
Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c, Z3_solver s, Z3_ast_vector assumptions, Z3_ast_vector variables, Z3_ast_vector consequences)
retrieve consequences from solver that determine values of the supplied function symbols.
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...
expr distinct(expr_vector const &args)
Definition: z3++.h:1469
bool is_uint(unsigned i) const
Definition: z3++.h:1669
stats statistics() const
Definition: z3++.h:2058
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]).
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_sort_kind
The different kinds of Z3 types (See #Z3_get_sort_kind).
Definition: z3_api.h:153
expr parse_string(char const *s)
parsing
Definition: z3++.h:2469
Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)
Create a bit-vector type of the given size.
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.
sort bool_sort()
Return the Boolean sort.
Definition: z3++.h:2087
void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)
Decrement the reference counter of the given probe.
expr get_const_interp(func_decl c) const
Definition: z3++.h:1624
expr mk_and(expr_vector const &args)
Definition: z3++.h:1528
bool is_decided_unsat() const
Definition: z3++.h:1810
Z3_ast Z3_API Z3_mk_false(Z3_context c)
Create an AST node representing false.
tactic & operator=(tactic const &s)
Definition: z3++.h:1870
bool is_bool() const
Return true if this sort is the Boolean sort.
Definition: z3++.h:460
sort re_sort(sort &seq_sort)
Return a regular expression sort over sequences seq_sort.
Definition: z3++.h:2093
bool is_datatype() const
Return true if this is a Datatype expression.
Definition: z3++.h:599
probe(context &c, Z3_probe s)
Definition: z3++.h:1937
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:740
unsigned uint_value(unsigned i) const
Definition: z3++.h:1671
probe & operator=(probe const &s)
Definition: z3++.h:1941
func_entry entry(unsigned i) const
Definition: z3++.h:1579
Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err)
Return a string describing the given error code.
Z3_ast Z3_API Z3_mk_interpolant(Z3_context c, Z3_ast a)
Create an AST node marking a formula position for interpolation.
double double_value(unsigned i) const
Definition: z3++.h:1672
std::string documentation(symbol const &s)
Definition: z3++.h:378
stats statistics() const
Definition: z3++.h:1752
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].
std::string help() const
Definition: z3++.h:2062
Z3_string Z3_API Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s)
Retrieve documentation string corresponding to parameter name s.
model get_model() const
Definition: z3++.h:2044
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2084
unsigned size() const
Definition: z3++.h:1802
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.
expr zext(expr const &a, unsigned i)
Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i...
Definition: z3++.h:1338
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.
void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t)
Increment the reference counter of the given tactic.
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.
void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g)
Erase all formulas from the given goal.
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...
expr operator[](int i) const
Definition: z3++.h:1803
void push()
Definition: z3++.h:1711
expr contains(expr const &s)
Definition: z3++.h:920
func_decl get_const_decl(unsigned i) const
Definition: z3++.h:1613
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.
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:2077
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.
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
expr extract(expr const &offset, expr const &length) const
sequence and regular expression operations.
Definition: z3++.h:905
solver(context &c, simple)
Definition: z3++.h:1696
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:562
expr bv_val(int n, unsigned sz)
Definition: z3++.h:2212
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed greater than.
expr operator!=(expr const &a, expr const &b)
Definition: z3++.h:1024
Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2)
Logical shift right.
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.
Definition: z3_api.h:1288
func_interp & operator=(func_interp const &s)
Definition: z3++.h:1570
Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2)
Arithmetic shift right.
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...
func_decl get_func_decl(unsigned i) const
Definition: z3++.h:1614
probe(context &c, double val)
Definition: z3++.h:1936
expr select(expr const &a, expr const &i)
Definition: z3++.h:2329
Definition: z3++.h:121
expr operator &(expr const &a, expr const &b)
Definition: z3++.h:1214
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:1547
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
Z3_ast Z3_API Z3_goal_formula(Z3_context c, Z3_goal g, unsigned idx)
Return a formula from the given goal.
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.
tactic when(probe const &p, tactic const &t)
Definition: z3++.h:2071
config()
Definition: z3++.h:99
bool is_algebraic() const
Return true if expression is an algebraic number.
Definition: z3++.h:654
unsigned get_numeral_uint() const
Return uint value of numeral, throw if result cannot fit in machine uint.
Definition: z3++.h:692
expr lower(handle const &h)
Definition: z3++.h:2046
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...
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
array(unsigned sz)
Definition: z3++.h:315
expr extract(unsigned hi, unsigned lo) const
Definition: z3++.h:896
A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort.
Definition: z3++.h:439
~solver()
Definition: z3++.h:1701
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].
sort array_domain() const
Return the domain of this Array sort.
Definition: z3++.h:514
char const * msg() const
Definition: z3++.h:84
T operator[](int i) const
Definition: z3++.h:1390
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_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
__uint64 get_numeral_uint64() const
Return __uint64 value of numeral, throw if result cannot fit in __uint64.
Definition: z3++.h:722
Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than.
func_decl(context &c)
Definition: z3++.h:529
~array()
Definition: z3++.h:318
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...
void pop_back()
Definition: z3++.h:1394
expr full_set(sort const &s)
Definition: z3++.h:2367
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.
unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g)
Return the number of formulas in the given goal.
sort array_range() const
Return the range of this Array sort.
Definition: z3++.h:520
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.
Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem)
Remove an element to a set.
T const & operator[](int i) const
Definition: z3++.h:321
Z3_ast Z3_API Z3_mk_set_union(Z3_context c, unsigned num_args, Z3_ast const args[])
Take the union of a list of sets.
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:2090
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:189
expr lshr(expr const &a, expr const &b)
logic shift right operator for bitvectors
Definition: z3++.h:1324
expr as_expr() const
Definition: z3++.h:1811
expr udiv(expr const &a, expr const &b)
unsigned division operator for bitvectors.
Definition: z3++.h:1296
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
Z3_symbol Z3_API Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, unsigned i)
Return the number of parameters in the given parameter description set.
std::string help() const
Definition: z3++.h:1887
bool is_bv() const
Return true if this is a Bit-vector expression.
Definition: z3++.h:591
expr upper(handle const &h)
Definition: z3++.h:2051
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1349
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1286
goal(context &c, Z3_goal s)
Definition: z3++.h:1790
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].
std::string to_string() const
Definition: z3++.h:379
expr_vector assertions() const
Definition: z3++.h:2056
Z3_ast Z3_API Z3_parse_smtlib2_file(Z3_context c, Z3_string file_name, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Similar to Z3_parse_smtlib2_string, but reads the benchmark from a file.
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.
model(context &c, Z3_model m)
Definition: z3++.h:1589
sort array_sort(sort d, sort r)
Return an array sort for arrays from d to r.
Definition: z3++.h:2095
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:2186
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...
void pop()
Definition: z3++.h:2040
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.
int Z3_bool
Z3 Boolean type. It is just an alias for int.
Definition: z3_api.h:84
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.
double operator()(goal const &g) const
Definition: z3++.h:1949
bool is_real() const
Return true if this is a real expression.
Definition: z3++.h:583
Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than or equal to.
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
bool is_datatype() const
Return true if this sort is a Datatype sort.
Definition: z3++.h:484
tactic(tactic const &s)
Definition: z3++.h:1867
~probe()
Definition: z3++.h:1939
int to_int() const
Definition: z3++.h:347
func_decl operator[](int i) const
Definition: z3++.h:1616
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.
~tactic()
Definition: z3++.h:1868
bool is_array() const
Return true if this is a Array expression.
Definition: z3++.h:595
sort operator()(context &c, Z3_ast a)
Definition: z3++.h:1365
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.
check_result check()
Definition: z3++.h:2043
expr operator^(expr const &a, expr const &b)
Definition: z3++.h:1218
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)
Create the constant array.
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.
std::string get_decimal_string(int precision) const
Return string representation of numeral or algebraic number This method assumes the expression is num...
Definition: z3++.h:667
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].
void from_string(char const *constraints)
Definition: z3++.h:2061
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.
Exception used to sign API usage errors.
Definition: z3++.h:80
expr operator*(expr const &a, expr const &b)
Definition: z3++.h:1061
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
Z3_ast Z3_API Z3_parse_smtlib2_string(Z3_context c, Z3_string str, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Parse the given string using the SMT-LIB2 parser.
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.
ast_vector_tpl(context &c, Z3_ast_vector v)
Definition: z3++.h:1385
A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort ...
Definition: z3++.h:560
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.
bool is_int() const
Return true if this sort is the Integer sort.
Definition: z3++.h:464
expr operator!(expr const &a)
Definition: z3++.h:983
expr set_subset(expr const &a, expr const &b)
Definition: z3++.h:2407
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)
Create the empty set.
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition: z3++.h:2353
#define __uint64
Definition: z3_api.h:44
def is_app(a)
Definition: z3py.py:1029
expr & operator=(expr const &n)
Definition: z3++.h:565
expr ule(expr const &a, expr const &b)
unsigned less than or equal to operator for bitvectors.
Definition: z3++.h:1272
expr in_re(expr const &s, expr const &re)
Definition: z3++.h:2443
symbol name(unsigned i)
Definition: z3++.h:376
std::string key(unsigned i) const
Definition: z3++.h:1668
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:947
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
static param_descrs simplify_param_descrs(context &c)
Definition: z3++.h:373
sort domain(unsigned i) const
Definition: z3++.h:536
expr parse_file(char const *file)
Definition: z3++.h:2475
Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s)
Return the parameter description set for the given solver object.
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...
func_decl operator()(context &c, Z3_ast a)
Definition: z3++.h:1373
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:1655
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.
expr operator>=(expr const &a, expr const &b)
Definition: z3++.h:1082
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.
Z3_ast Z3_API Z3_mk_set_intersect(Z3_context c, unsigned num_args, Z3_ast const args[])
Take the intersection of a list of sets.
bool is_re() const
Return true if this is a regular expression.
Definition: z3++.h:611
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...
expr pw(expr const &a, expr const &b)
Definition: z3++.h:972
bool empty() const
Definition: z3++.h:1395
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.
Z3_string Z3_API Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p)
Convert a parameter description set into a string. This function is mainly used for printing the cont...
context(config &c, interpolation)
Definition: z3++.h:155
expr(context &c, Z3_ast n)
Definition: z3++.h:563
~goal()
Definition: z3++.h:1792
expr set_difference(expr const &a, expr const &b)
Definition: z3++.h:2395
Z3_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.
expr operator~(expr const &a)
Definition: z3++.h:1226
unsigned num_entries() const
Definition: z3++.h:1578
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.
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:1724
check_result check(expr_vector assumptions)
Definition: z3++.h:1734
probe(context &c, char const *name)
Definition: z3++.h:1935
Z3_symbol_kind kind() const
Definition: z3++.h:345
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed less than.
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...
~stats()
Definition: z3++.h:1658
sort seq_sort(sort &s)
Return a sequence sort over base sort s.
Definition: z3++.h:2092
def substitute(t, m)
Definition: z3py.py:7500
expr length() const
Definition: z3++.h:932
A Context manages all other Z3 objects, global configuration options, etc.
Definition: z3++.h:134
Definition: z3++.h:409
Z3 C++ namespace.
Definition: z3++.h:45
Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Take the set difference between two sets.
Z3_bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, unsigned __int64 *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned __int6...
sort range() const
Definition: z3++.h:537
expr set_add(expr const &s, expr const &e)
Definition: z3++.h:2371
expr ashr(expr const &a, expr const &b)
arithmetic shift right operator for bitvectors
Definition: z3++.h:1331
unsigned size() const
Definition: z3++.h:1667
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.
Z3_ast Z3_API Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed remainder (sign follows dividend).
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:4033
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c)
Return the parameter description set for the simplify procedure.
solver(context &c, Z3_solver s)
Definition: z3++.h:1697
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:94
Z3_decl_kind decl_kind() const
Definition: z3++.h:539
bool is_re() const
Return true if this sort is a regular expression sort.
Definition: z3++.h:496
solver & operator=(solver const &s)
Definition: z3++.h:1703
expr operator &&(expr const &a, expr const &b)
Definition: z3++.h:990
expr substitute(expr_vector const &src, expr_vector const &dst)
Apply substitution. Replace src expressions by dst.
Definition: z3++.h:2535
ast(context &c, Z3_ast n)
Definition: z3++.h:414
ast_vector_tpl & operator=(ast_vector_tpl const &s)
Definition: z3++.h:1396
expr operator<=(expr const &a, expr const &b)
Definition: z3++.h:1154
handle add(expr const &e, char const *weight)
Definition: z3++.h:2027
Z3_goal_prec precision() const
Definition: z3++.h:1804
expr bv_const(char const *name, unsigned sz)
Definition: z3++.h:2195
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...
context & ctx() const
Definition: z3++.h:332
void Z3_API Z3_param_descrs_inc_ref(Z3_context c, Z3_param_descrs p)
Increment the reference counter of the given parameter description set.
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.
Z3_sort_kind sort_kind() const
Return the internal sort kind.
Definition: z3++.h:452
expr string_val(char const *s)
Definition: z3++.h:2218
T back() const
Definition: z3++.h:1393
tactic(context &c, char const *name)
Definition: z3++.h:1865
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.
sort string_sort()
Return the sort for ASCII strings.
Definition: z3++.h:2091
tactic with(tactic const &t, params const &p)
Definition: z3++.h:1916
expr empty_set(sort const &s)
Definition: z3++.h:2363
expr plus(expr const &re)
Definition: z3++.h:2449
__int64 get_numeral_int64() const
Return __int64 value of numeral, throw if result cannot fit in __int64.
Definition: z3++.h:707
void reset()
Definition: z3++.h:1713
Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1)
Coerce an integer to a real.
Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)
Shift left.
~config()
Definition: z3++.h:100
bool is_arith() const
Return true if this sort is the Integer or Real sort.
Definition: z3++.h:472
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
bool is_relation() const
Return true if this sort is a Relation sort.
Definition: z3++.h:488
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...
void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p)
Increment the reference counter of the given probe.
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
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...
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:183
bool is_real() const
Return true if this sort is the Real sort.
Definition: z3++.h:468
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:1543
void resize(unsigned sz)
Definition: z3++.h:1392
void Z3_API Z3_del_config(Z3_config c)
Delete the given configuration object.
Z3_bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned int...
expr body() const
Return the &#39;body&#39; of this quantifier.
Definition: z3++.h:762
expr operator()() const
Definition: z3++.h:2244
void add(expr const &e, char const *p)
Definition: z3++.h:1720
func_decl to_func_decl(context &c, Z3_func_decl f)
Definition: z3++.h:1264
unsigned hash() const
Definition: z3++.h:421
optimize(context &c)
Definition: z3++.h:2014
goal operator[](int i) const
Definition: z3++.h:1847
Z3_lbool Z3_API Z3_compute_interpolant(Z3_context c, Z3_ast pat, Z3_params p, Z3_ast_vector *interp, Z3_model *model)
param_descrs(param_descrs const &o)
Definition: z3++.h:364
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:638
expr(expr const &n)
Definition: z3++.h:564
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].
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.
Definition: z3++.h:1536
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:1723
expr_vector objectives() const
Definition: z3++.h:2057
Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Check for subsetness of sets.
std::string to_smt2(char const *status="unknown")
Definition: z3++.h:1758
expr operator+(expr const &a, expr const &b)
Definition: z3++.h:1034
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...
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2115
expr operator()(context &c, Z3_ast a)
Definition: z3++.h:1354
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.
Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem)
Add an element to a set.
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.
bool is_arith() const
Return true if this is an integer or real expression.
Definition: z3++.h:587
bool is_well_sorted() const
Return true if this expression is well sorted (aka type correct).
Definition: z3++.h:659
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.
Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg)
Take the complement of a set.
def is_real(a)
Definition: z3py.py:2328
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...
std::string str() const
Definition: z3++.h:346
expr srem(expr const &a, expr const &b)
signed reminder operator for bitvectors
Definition: z3++.h:1303
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.
expr set_intersect(expr const &a, expr const &b)
Definition: z3++.h:2387
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...
bool inconsistent() const
Definition: z3++.h:1805
exception(char const *msg)
Definition: z3++.h:83
solver(solver const &s)
Definition: z3++.h:1700
void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g)
Decrement the reference counter of the given tactic.
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:105
void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a)
Add a new formula a to the given goal.
~optimize()
Definition: z3++.h:2015
Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g)
Convert a goal into a string.
expr at(expr const &index) const
Definition: z3++.h:926
#define __int64
Definition: z3_api.h:40
expr real_val(int n, int d)
Definition: z3++.h:2205
ast_vector_tpl< sort > sort_vector
Definition: z3++.h:69
bool is_bool() const
Return true if this is a Boolean expression.
Definition: z3++.h:575
void add(expr const &e)
Definition: z3++.h:2017
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.
expr prefixof(expr const &a, expr const &b)
Definition: z3++.h:2426
void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h)
Register a Z3 error handler.
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas on the solver.
Z3_ast Z3_API Z3_mk_sign_ext(Z3_context c, unsigned i, Z3_ast t1)
Sign-extend of the given bit-vector to the (signed) equivalent bit-vector of size m+i...
func_interp(func_interp const &s)
Definition: z3++.h:1567
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:1593
void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m)
Decrement the reference counter of the given model.
unsigned Z3_API Z3_param_descrs_size(Z3_context c, Z3_param_descrs p)
Return the number of parameters in the given parameter description set.
void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g)
Decrement the reference counter of the given goal.
unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m)
Return the number of constants assigned by the given model.
expr interpolant(expr const &a)
Definition: z3++.h:2465
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:1714
void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s)
Decrement the reference counter of the given statistics object.
expr ugt(expr const &a, expr const &b)
unsigned greater than operator for bitvectors.
Definition: z3++.h:1290
goal & operator=(goal const &s)
Definition: z3++.h:1794
expr option(expr const &re)
Definition: z3++.h:2454
~params()
Definition: z3++.h:389
expr const_array(sort const &d, expr const &v)
Definition: z3++.h:2359
stats(stats const &s)
Definition: z3++.h:1657
def is_int(a)
Definition: z3py.py:2310
expr set_member(expr const &s, expr const &e)
Definition: z3++.h:2403
def is_quantifier(a)
Definition: z3py.py:1833
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.
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.
void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p)
Decrement the reference counter of the given parameter set.
bool is_numeral_i64(__int64 &i) const
Definition: z3++.h:629
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...
~func_entry()
Definition: z3++.h:1545
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:570
sort uninterpreted_sort(char const *name)
create an uninterpreted sort with the name given by the string or symbol.
Definition: z3++.h:2107
void reset()
Definition: z3++.h:1807
T * ptr()
Definition: z3++.h:323
params(params const &s)
Definition: z3++.h:388
Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e)
Return the value of this point.
void set_param(char const *param, char const *value)
Definition: z3++.h:72
check_result compute_interpolant(expr const &pat, params const &p, expr_vector &interp, model &m)
Interpolation support.
Definition: z3++.h:2514
Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than.
unsigned lo() const
Definition: z3++.h:897
bool is_array() const
Return true if this sort is a Array sort.
Definition: z3++.h:480
handle maximize(expr const &e)
Definition: z3++.h:2031
unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m)
Return the number of function interpretations in the given model.
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 ...
Z3_param_kind
The different kinds of parameters that can be associated with parameter sets. (see Z3_mk_params)...
Definition: z3_api.h:1243
Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a string of a numeric constant term.
expr int_const(char const *name)
Definition: z3++.h:2193
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.
friend std::ostream & operator<<(std::ostream &out, exception const &e)
Definition: z3++.h:87
expr replace(expr const &src, expr const &dst) const
Definition: z3++.h:909
symbol(symbol const &s)
Definition: z3++.h:342
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...
expr value() const
Definition: z3++.h:1554
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.
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_symbol_kind
The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See #Z3...
Definition: z3_api.h:119
Z3_bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a)
Test if there exists an interpretation (i.e., assignment) for a in the model m.
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
sort(context &c)
Definition: z3++.h:441
unsigned arity() const
Definition: z3++.h:535
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.
goal(context &c, bool models=true, bool unsat_cores=false, bool proofs=false)
Definition: z3++.h:1789
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.
expr suffixof(expr const &a, expr const &b)
Definition: z3++.h:2420
void from_file(char const *filename)
Definition: z3++.h:2060
void Z3_API Z3_interrupt(Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers...
check_result consequences(expr_vector &assumptions, expr_vector &vars, expr_vector &conseq)
Definition: z3++.h:1746
expr operator<(expr const &a, expr const &b)
Definition: z3++.h:1176
unsigned num_exprs() const
Definition: z3++.h:1808
object(context &c)
Definition: z3++.h:330
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)
Create a new (incremental) solver.
handle add(expr const &e, unsigned weight)
Definition: z3++.h:2021
bool is_numeral(std::string &s, unsigned precision) const
Definition: z3++.h:634
ast(context &c)
Definition: z3++.h:413
object(object const &s)
Definition: z3++.h:331
expr arg(unsigned i) const
Return the i-th argument of this application. This method assumes the expression is an application...
Definition: z3++.h:755
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
expr real_const(char const *name)
Definition: z3++.h:2194
bool is_relation() const
Return true if this is a Relation expression.
Definition: z3++.h:603
bool is_const() const
Return true if this expression is a constant (i.e., an application with 0 arguments).
Definition: z3++.h:642
unsigned h() const
Definition: z3++.h:2012
unsigned size() const
Definition: z3++.h:1846
bool is_decided_sat() const
Definition: z3++.h:1809
Z3_param_descrs Z3_API Z3_tactic_get_param_descrs(Z3_context c, Z3_tactic t)
Return the parameter description set for the given tactic object.
model convert_model(model const &m, unsigned i=0) const
Definition: z3++.h:1848
expr sext(expr const &a, unsigned i)
Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector.
Definition: z3++.h:1343
Z3_sort Z3_API Z3_mk_real_sort(Z3_context c)
Create the real type.
Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision)
Return numeral as a string in decimal notation. The result has at most precision decimal places...
Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set)
Check for set membership.
bool is_numeral_i(int &i) const
Definition: z3++.h:631
expr empty(sort const &s)
Definition: z3++.h:2415
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:343
~model()
Definition: z3++.h:1591
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...
sort real_sort()
Return the Real sort.
Definition: z3++.h:2089
friend std::ostream & operator<<(std::ostream &out, ast_vector_tpl const &v)
Definition: z3++.h:1403
Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target)
Copy a solver s from the context source to a the context target.
void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g)
Increment the reference counter of the given goal.
ast_vector_tpl(ast_vector_tpl const &s)
Definition: z3++.h:1386
expr num_val(int n, sort const &s)
Definition: z3++.h:2221
bool eq(ast const &a, ast const &b)
Definition: z3++.h:433
bool is_bv() const
Return true if this sort is a Bit-vector sort.
Definition: z3++.h:476
symbol int_symbol(int n)
Create a Z3 symbol based on the given integer.
Definition: z3++.h:2085
Z3_bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int...
expr else_value() const
Definition: z3++.h:1577
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
expr indexof(expr const &s, expr const &substr, expr const &offset)
Definition: z3++.h:2432
expr set_complement(expr const &a)
Definition: z3++.h:2399
param_descrs & operator=(param_descrs const &o)
Definition: z3++.h:365
expr unit() const
Definition: z3++.h:915
expr operator>(expr const &a, expr const &b)
Definition: z3++.h:1195
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].
expr simplify() const
Return a simplified version of this expression.
Definition: z3++.h:943
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:124
expr star(expr const &re)
Definition: z3++.h:2459
expr operator==(expr const &a, expr const &b)
Definition: z3++.h:1015
symbol name() const
Return name of sort.
Definition: z3++.h:456
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.
#define MK_EXPR1(_fn, _arg)
Definition: z3++.h:2348
param_descrs(context &c, Z3_param_descrs d)
Definition: z3++.h:363
void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value)
Set a configuration parameter.
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...
expr operator|(expr const &a, expr const &b)
Definition: z3++.h:1222
unsigned hi() const
Definition: z3++.h:898
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
unsigned num_args() const
Definition: z3++.h:1555
tactic(context &c, Z3_tactic s)
Definition: z3++.h:1866
void check_context(object const &a, object const &b)
Definition: z3++.h:336
expr arg(unsigned i) const
Definition: z3++.h:1556
expr bool_const(char const *name)
Definition: z3++.h:2192
expr urem(expr const &a, expr const &b)
unsigned reminder operator for bitvectors
Definition: z3++.h:1310
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.
solver mk_solver() const
Definition: z3++.h:1877
std::string reason_unknown() const
Definition: z3++.h:1751
model get_model() const
Definition: z3++.h:1745
unsigned num_consts() const
Definition: z3++.h:1611
params & operator=(params const &s)
Definition: z3++.h:391
model(model const &s)
Definition: z3++.h:1590
expr proof() const
Definition: z3++.h:1755
bool is_numeral_u(unsigned &i) const
Definition: z3++.h:632
bool is_numeral_u64(__uint64 &i) const
Definition: z3++.h:630
probe(probe const &s)
Definition: z3++.h:1938
Z3_param_kind Z3_API Z3_param_descrs_get_kind(Z3_context c, Z3_param_descrs p, Z3_symbol n)
Return the kind associated with the given parameter name n.
symbol name() const
Definition: z3++.h:538
solver(context &c, solver const &src, translate)
Definition: z3++.h:1699
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 ...
solver(context &c)
Definition: z3++.h:1695
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:530
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
T const * ptr() const
Definition: z3++.h:322
handle minimize(expr const &e)
Definition: z3++.h:2034
apply_result apply(goal const &g) const
Definition: z3++.h:1878
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
void add(expr const &e, expr const &p)
Definition: z3++.h:1715
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:2336
bool has_interp(func_decl f) const
Definition: z3++.h:1639
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
unsigned size() const
Definition: z3++.h:1615
apply_result operator()(goal const &g) const
Definition: z3++.h:1884
Z3_ast m_ast
Definition: z3++.h:411
Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned division.
unsigned size() const
Definition: z3++.h:1389
unsigned size() const
Definition: z3++.h:319
tactic repeat(tactic const &t, unsigned max=UINT_MAX)
Definition: z3++.h:1910
expr bool_val(bool b)
Definition: z3++.h:2197
~context()
Definition: z3++.h:156
expr operator||(expr const &a, expr const &b)
Definition: z3++.h:1002
expr ult(expr const &a, expr const &b)
unsigned less than operator for bitvectors.
Definition: z3++.h:1278
bool is_var() const
Return true if this expression is a variable.
Definition: z3++.h:650
Z3_context Z3_API Z3_mk_interpolation_context(Z3_config cfg)
This function generates a Z3 context suitable for generation of interpolants. Formulas can be generat...
void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p)
Increment the reference counter of the given parameter set.
expr_vector get_interpolant(expr const &proof, expr const &pat, params const &p)
Definition: z3++.h:2531
unsigned depth() const
Definition: z3++.h:1806
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...
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.
expr int_val(int n)
Definition: z3++.h:2199
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.
func_decl(func_decl const &s)
Definition: z3++.h:531
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
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.
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.
expr mk_or(expr_vector const &args)
Definition: z3++.h:1522
tactic fail_if(probe const &p)
Definition: z3++.h:2066
Z3_param_kind kind(symbol const &s)
Definition: z3++.h:377
stats(context &c, Z3_stats e)
Definition: z3++.h:1656
expr exists(expr const &x, expr const &b)
Definition: z3++.h:1443
ast operator()(context &c, Z3_ast a)
Definition: z3++.h:1349
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:154
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...
bool is_quantifier() const
Return true if this expression is a quantifier.
Definition: z3++.h:646
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.
expr ite(expr const &c, expr const &t, expr const &e)
Create the if-then-else expression ite(c, t, e)
Definition: z3++.h:1237
double apply(goal const &g) const
Definition: z3++.h:1948
func_entry(func_entry const &s)
Definition: z3++.h:1544
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 bit-vector of size m to yield a new bit-vector of size n...
expr eval(expr const &n, bool model_completion=false) const
Definition: z3++.h:1601
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two&#39;s complement unary minus.
~ast()
Definition: z3++.h:416
#define Z3_FALSE
False value. It is just an alias for 0.
Definition: z3_api.h:100
expr_vector unsat_core() const
Definition: z3++.h:1753
int get_numeral_int() const
Return int value of numeral, throw if result cannot fit in machine int.
Definition: z3++.h:678
ast & operator=(ast const &s)
Definition: z3++.h:419
expr_vector assertions() const
Definition: z3++.h:1754
unsigned num_args() const
Return the number of arguments in this application. This method assumes the expression is an applicat...
Definition: z3++.h:747
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.
unsigned bv_size() const
Return the size of this Bit-vector sort.
Definition: z3++.h:507
Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned remainder.
Z3_ast_kind kind() const
Definition: z3++.h:420
expr forall(expr const &x, expr const &b)
Definition: z3++.h:1419
sort(context &c, Z3_sort s)
Definition: z3++.h:442
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).
expr implies(expr const &a, expr const &b)
Definition: z3++.h:961
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...
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:1250
expr concat(expr const &a, expr const &b)
Definition: z3++.h:1478
symbol(context &c, Z3_symbol s)
Definition: z3++.h:341
solver(context &c, char const *logic)
Definition: z3++.h:1698
tactic try_for(tactic const &t, unsigned ms)
Definition: z3++.h:1921
func_interp(context &c, Z3_func_interp e)
Definition: z3++.h:1566
expr shl(expr const &a, expr const &b)
shift left operator for bitvectors
Definition: z3++.h:1317
params(context &c)
Definition: z3++.h:387
void push_back(T const &e)
Definition: z3++.h:1391
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:3481
expr uge(expr const &a, expr const &b)
unsigned greater than or equal to operator for bitvectors.
Definition: z3++.h:1284
void push()
Definition: z3++.h:2037
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...
bool is_seq() const
Return true if this sort is a Sequence sort.
Definition: z3++.h:492
bool is_numeral(std::string &s) const
Definition: z3++.h:633
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.
bool is_double(unsigned i) const
Definition: z3++.h:1670
sort & operator=(sort const &s)
Return true if this sort and s are equal.
Definition: z3++.h:448
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...
context * m_ctx
Definition: z3++.h:328
unsigned size()
Definition: z3++.h:375
Z3_bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g)
Return true if the given goal contains the formula false.
bool is_finite_domain() const
Return true if this is a Finite-domain expression.
Definition: z3++.h:621
expr operator-(expr const &a)
Definition: z3++.h:1118
func_interp get_func_interp(func_decl f) const
Definition: z3++.h:1630
void pop(unsigned n=1)
Definition: z3++.h:1712
expr to_real(expr const &a)
Definition: z3++.h:2305
handle(unsigned h)
Definition: z3++.h:2011
Z3_ast_vector Z3_API Z3_get_interpolant(Z3_context c, Z3_ast pf, Z3_ast pat, Z3_params p)
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two&#39;s complement addition.
param_descrs get_param_descrs()
Definition: z3++.h:1777
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:628
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_...
Z3_bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, __int64 *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine __int64 int...
bool is_const() const
Definition: z3++.h:541
bool is_seq() const
Return true if this is a sequence expression.
Definition: z3++.h:607
ast(ast const &s)
Definition: z3++.h:415
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:2096
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:443
bool is_finite_domain() const
Return true if this sort is a Finite domain sort.
Definition: z3++.h:500
void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s)
Increment the reference counter of the given statistics object.
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955
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:1835
expr operator/(expr const &a, expr const &b)
Definition: z3++.h:1099
Function declaration (aka function definition). It is the signature of interpreted and uninterpreted ...
Definition: z3++.h:527
expr set_union(expr const &a, expr const &b)
Definition: z3++.h:2379
T & operator[](int i)
Definition: z3++.h:320
param_descrs get_param_descrs()
Definition: z3++.h:1893
sort int_sort()
Return the integer sort.
Definition: z3++.h:2088
goal(goal const &s)
Definition: z3++.h:1791
expr set_del(expr const &s, expr const &e)
Definition: z3++.h:2375
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.
stats & operator=(stats const &s)
Definition: z3++.h:1660
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.
func_decl & operator=(func_decl const &s)
Definition: z3++.h:533
apply_result & operator=(apply_result const &s)
Definition: z3++.h:1839
sort to_sort(context &c, Z3_sort s)
Definition: z3++.h:1259
context()
Definition: z3++.h:153
void Z3_API Z3_param_descrs_dec_ref(Z3_context c, Z3_param_descrs p)
Decrement the reference counter of the given parameter description set.
bool is_int() const
Return true if this is an integer expression.
Definition: z3++.h:579
void add(expr const &f)
Definition: z3++.h:1801
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 to_re(expr const &s)
Definition: z3++.h:2438
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...
unsigned num_funcs() const
Definition: z3++.h:1612
void check_error() const
Definition: z3++.h:333
check_result
Definition: z3++.h:120
Z3_ast Z3_API Z3_mk_zero_ext(Z3_context c, unsigned i, Z3_ast t1)
Extend the given bit-vector with zeros to the (unsigned) equivalent bit-vector of size m+i...
Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m)
Convert the given model into a string.
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition: z3_api.h:89
apply_result(apply_result const &s)
Definition: z3++.h:1836