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 signaling 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 #pragma once
22 
23 #include<cassert>
24 #include<iostream>
25 #include<string>
26 #include<sstream>
27 #include<z3.h>
28 #include<limits.h>
29 #include<functional>
30 
31 #undef min
32 #undef max
33 
39 
44 
48 namespace z3 {
49 
50  class exception;
51  class config;
52  class context;
53  class symbol;
54  class params;
55  class param_descrs;
56  class ast;
57  class sort;
58  class func_decl;
59  class expr;
60  class solver;
61  class goal;
62  class tactic;
63  class probe;
64  class model;
65  class func_interp;
66  class func_entry;
67  class statistics;
68  class apply_result;
69  template<typename T> class cast_ast;
70  template<typename T> class ast_vector_tpl;
75 
76  inline void set_param(char const * param, char const * value) { Z3_global_param_set(param, value); }
77  inline void set_param(char const * param, bool value) { Z3_global_param_set(param, value ? "true" : "false"); }
78  inline void set_param(char const * param, int value) { auto str = std::to_string(value); Z3_global_param_set(param, str.c_str()); }
80 
84  class exception : public std::exception {
85  std::string m_msg;
86  public:
87  exception(char const * msg):m_msg(msg) {}
88  virtual ~exception() throw() {}
89  char const * msg() const { return m_msg.c_str(); }
90  char const * what() const throw() { return m_msg.c_str(); }
91  friend std::ostream & operator<<(std::ostream & out, exception const & e);
92  };
93  inline std::ostream & operator<<(std::ostream & out, exception const & e) { out << e.msg(); return out; }
94 
95 #if !defined(Z3_THROW)
96 #if __cpp_exceptions || _CPPUNWIND || __EXCEPTIONS
97 #define Z3_THROW(x) throw x
98 #else
99 #define Z3_THROW(x) {}
100 #endif
101 #endif // !defined(Z3_THROW)
102 
106  class config {
107  Z3_config m_cfg;
108  config(config const & s);
109  config & operator=(config const & s);
110  public:
111  config() { m_cfg = Z3_mk_config(); }
112  ~config() { Z3_del_config(m_cfg); }
113  operator Z3_config() const { return m_cfg; }
117  void set(char const * param, char const * value) { Z3_set_param_value(m_cfg, param, value); }
121  void set(char const * param, bool value) { Z3_set_param_value(m_cfg, param, value ? "true" : "false"); }
125  void set(char const * param, int value) {
126  auto str = std::to_string(value);
127  Z3_set_param_value(m_cfg, param, str.c_str());
128  }
129  };
130 
133  };
134 
141  };
142 
144  if (l == Z3_L_TRUE) return sat;
145  else if (l == Z3_L_FALSE) return unsat;
146  return unknown;
147  }
148 
149 
155  class context {
156  private:
157  bool m_enable_exceptions;
158  rounding_mode m_rounding_mode;
159  Z3_context m_ctx;
160  void init(config & c) {
161  set_context(Z3_mk_context_rc(c));
162  }
163  void set_context(Z3_context ctx) {
164  m_ctx = ctx;
165  m_enable_exceptions = true;
166  m_rounding_mode = RNA;
167  Z3_set_error_handler(m_ctx, 0);
169  }
170 
171 
172  context(context const & s);
173  context & operator=(context const & s);
174 
175  friend class scoped_context;
176  context(Z3_context c) { set_context(c); }
177  void detach() { m_ctx = nullptr; }
178  public:
179  context() { config c; init(c); }
180  context(config & c) { init(c); }
181  ~context() { if (m_ctx) Z3_del_context(m_ctx); }
182  operator Z3_context() const { return m_ctx; }
183 
188  Z3_error_code e = Z3_get_error_code(m_ctx);
189  if (e != Z3_OK && enable_exceptions())
190  Z3_THROW(exception(Z3_get_error_msg(m_ctx, e)));
191  return e;
192  }
193 
194  void check_parser_error() const {
195  check_error();
196  }
197 
205  void set_enable_exceptions(bool f) { m_enable_exceptions = f; }
206 
207  bool enable_exceptions() const { return m_enable_exceptions; }
208 
212  void set(char const * param, char const * value) { Z3_update_param_value(m_ctx, param, value); }
216  void set(char const * param, bool value) { Z3_update_param_value(m_ctx, param, value ? "true" : "false"); }
220  void set(char const * param, int value) {
221  auto str = std::to_string(value);
222  Z3_update_param_value(m_ctx, param, str.c_str());
223  }
224 
229  void interrupt() { Z3_interrupt(m_ctx); }
230 
234  symbol str_symbol(char const * s);
238  symbol int_symbol(int n);
242  sort bool_sort();
246  sort int_sort();
250  sort real_sort();
254  sort bv_sort(unsigned sz);
258  sort string_sort();
262  sort seq_sort(sort& s);
272  sort array_sort(sort d, sort r);
273  sort array_sort(sort_vector const& d, sort r);
280  sort fpa_sort(unsigned ebits, unsigned sbits);
284  template<size_t precision>
285  sort fpa_sort();
299  sort enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts);
300 
307  func_decl tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs);
308 
312  sort uninterpreted_sort(char const* name);
313  sort uninterpreted_sort(symbol const& name);
314 
315  func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range);
316  func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range);
317  func_decl function(symbol const& name, sort_vector const& domain, sort const& range);
318  func_decl function(char const * name, sort_vector const& domain, sort const& range);
319  func_decl function(char const * name, sort const & domain, sort const & range);
320  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range);
321  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range);
322  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range);
323  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range);
324 
325  func_decl recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range);
326  func_decl recfun(char const * name, unsigned arity, sort const * domain, sort const & range);
327  func_decl recfun(char const * name, sort const & domain, sort const & range);
328  func_decl recfun(char const * name, sort const & d1, sort const & d2, sort const & range);
329 
330  void recdef(func_decl, expr_vector const& args, expr const& body);
331 
332  expr constant(symbol const & name, sort const & s);
333  expr constant(char const * name, sort const & s);
334  expr bool_const(char const * name);
335  expr int_const(char const * name);
336  expr real_const(char const * name);
337  expr bv_const(char const * name, unsigned sz);
338  expr fpa_const(char const * name, unsigned ebits, unsigned sbits);
339 
340  template<size_t precision>
341  expr fpa_const(char const * name);
342 
343  expr bool_val(bool b);
344 
345  expr int_val(int n);
346  expr int_val(unsigned n);
347  expr int_val(int64_t n);
348  expr int_val(uint64_t n);
349  expr int_val(char const * n);
350 
351  expr real_val(int n, int d);
352  expr real_val(int n);
353  expr real_val(unsigned n);
354  expr real_val(int64_t n);
355  expr real_val(uint64_t n);
356  expr real_val(char const * n);
357 
358  expr bv_val(int n, unsigned sz);
359  expr bv_val(unsigned n, unsigned sz);
360  expr bv_val(int64_t n, unsigned sz);
361  expr bv_val(uint64_t n, unsigned sz);
362  expr bv_val(char const * n, unsigned sz);
363  expr bv_val(unsigned n, bool const* bits);
364 
365  expr fpa_val(double n);
366  expr fpa_val(float n);
367 
368  expr string_val(char const* s);
369  expr string_val(char const* s, unsigned n);
370  expr string_val(std::string const& s);
371 
372  expr num_val(int n, sort const & s);
373 
377  expr_vector parse_string(char const* s);
378  expr_vector parse_file(char const* file);
379 
380  expr_vector parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
381  expr_vector parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
382  };
383 
385  context m_ctx;
386  public:
387  scoped_context(Z3_context c): m_ctx(c) {}
388  ~scoped_context() { m_ctx.detach(); }
389  context& operator()() { return m_ctx; }
390  };
391 
392 
393  template<typename T>
394  class array {
395  T * m_array;
396  unsigned m_size;
397  array(array const & s);
398  array & operator=(array const & s);
399  public:
400  array(unsigned sz):m_size(sz) { m_array = new T[sz]; }
401  template<typename T2>
402  array(ast_vector_tpl<T2> const & v);
403  ~array() { delete[] m_array; }
404  void resize(unsigned sz) { delete[] m_array; m_size = sz; m_array = new T[sz]; }
405  unsigned size() const { return m_size; }
406  T & operator[](int i) { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
407  T const & operator[](int i) const { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
408  T const * ptr() const { return m_array; }
409  T * ptr() { return m_array; }
410  };
411 
412  class object {
413  protected:
415  public:
416  object(context & c):m_ctx(&c) {}
417  object(object const & s):m_ctx(s.m_ctx) {}
418  context & ctx() const { return *m_ctx; }
420  friend void check_context(object const & a, object const & b);
421  };
422  inline void check_context(object const & a, object const & b) { (void)a; (void)b; assert(a.m_ctx == b.m_ctx); }
423 
424  class symbol : public object {
425  Z3_symbol m_sym;
426  public:
427  symbol(context & c, Z3_symbol s):object(c), m_sym(s) {}
428  symbol(symbol const & s):object(s), m_sym(s.m_sym) {}
429  symbol & operator=(symbol const & s) { m_ctx = s.m_ctx; m_sym = s.m_sym; return *this; }
430  operator Z3_symbol() const { return m_sym; }
431  Z3_symbol_kind kind() const { return Z3_get_symbol_kind(ctx(), m_sym); }
432  std::string str() const { assert(kind() == Z3_STRING_SYMBOL); return Z3_get_symbol_string(ctx(), m_sym); }
433  int to_int() const { assert(kind() == Z3_INT_SYMBOL); return Z3_get_symbol_int(ctx(), m_sym); }
434  friend std::ostream & operator<<(std::ostream & out, symbol const & s);
435  };
436 
437  inline std::ostream & operator<<(std::ostream & out, symbol const & s) {
438  if (s.kind() == Z3_INT_SYMBOL)
439  out << "k!" << s.to_int();
440  else
441  out << s.str();
442  return out;
443  }
444 
445 
446  class param_descrs : public object {
447  Z3_param_descrs m_descrs;
448  public:
449  param_descrs(context& c, Z3_param_descrs d): object(c), m_descrs(d) { Z3_param_descrs_inc_ref(c, d); }
450  param_descrs(param_descrs const& o): object(o.ctx()), m_descrs(o.m_descrs) { Z3_param_descrs_inc_ref(ctx(), m_descrs); }
452  Z3_param_descrs_inc_ref(o.ctx(), o.m_descrs);
453  Z3_param_descrs_dec_ref(ctx(), m_descrs);
454  m_descrs = o.m_descrs;
455  m_ctx = o.m_ctx;
456  return *this;
457  }
460 
461  unsigned size() { return Z3_param_descrs_size(ctx(), m_descrs); }
462  symbol name(unsigned i) { return symbol(ctx(), Z3_param_descrs_get_name(ctx(), m_descrs, i)); }
463  Z3_param_kind kind(symbol const& s) { return Z3_param_descrs_get_kind(ctx(), m_descrs, s); }
464  std::string documentation(symbol const& s) { char const* r = Z3_param_descrs_get_documentation(ctx(), m_descrs, s); check_error(); return r; }
465  std::string to_string() const { return Z3_param_descrs_to_string(ctx(), m_descrs); }
466  };
467 
468  inline std::ostream& operator<<(std::ostream & out, param_descrs const & d) { return out << d.to_string(); }
469 
470  class params : public object {
471  Z3_params m_params;
472  public:
473  params(context & c):object(c) { m_params = Z3_mk_params(c); Z3_params_inc_ref(ctx(), m_params); }
474  params(params const & s):object(s), m_params(s.m_params) { Z3_params_inc_ref(ctx(), m_params); }
475  ~params() { Z3_params_dec_ref(ctx(), m_params); }
476  operator Z3_params() const { return m_params; }
477  params & operator=(params const & s) {
478  Z3_params_inc_ref(s.ctx(), s.m_params);
479  Z3_params_dec_ref(ctx(), m_params);
480  m_ctx = s.m_ctx;
481  m_params = s.m_params;
482  return *this;
483  }
484  void set(char const * k, bool b) { Z3_params_set_bool(ctx(), m_params, ctx().str_symbol(k), b); }
485  void set(char const * k, unsigned n) { Z3_params_set_uint(ctx(), m_params, ctx().str_symbol(k), n); }
486  void set(char const * k, double n) { Z3_params_set_double(ctx(), m_params, ctx().str_symbol(k), n); }
487  void set(char const * k, symbol const & s) { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), s); }
488  void set(char const * k, char const* s) { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), ctx().str_symbol(s)); }
489  friend std::ostream & operator<<(std::ostream & out, params const & p);
490  };
491 
492  inline std::ostream & operator<<(std::ostream & out, params const & p) {
493  out << Z3_params_to_string(p.ctx(), p); return out;
494  }
495 
496  class ast : public object {
497  protected:
498  Z3_ast m_ast;
499  public:
500  ast(context & c):object(c), m_ast(0) {}
501  ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
502  ast(ast const & s):object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
503  ~ast() { if (m_ast) Z3_dec_ref(*m_ctx, m_ast); }
504  operator Z3_ast() const { return m_ast; }
505  operator bool() const { return m_ast != 0; }
506  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; }
507  Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }
508  unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }
509  friend std::ostream & operator<<(std::ostream & out, ast const & n);
510  std::string to_string() const { return std::string(Z3_ast_to_string(ctx(), m_ast)); }
511 
512 
516  friend bool eq(ast const & a, ast const & b);
517  };
518  inline std::ostream & operator<<(std::ostream & out, ast const & n) {
519  out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
520  }
521 
522  inline bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b); }
523 
524  template<typename T>
525  class ast_vector_tpl : public object {
526  Z3_ast_vector m_vector;
527  void init(Z3_ast_vector v) { Z3_ast_vector_inc_ref(ctx(), v); m_vector = v; }
528  public:
530  ast_vector_tpl(context & c, Z3_ast_vector v):object(c) { init(v); }
531  ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
532  ast_vector_tpl(context& c, ast_vector_tpl const& src): object(c) { init(Z3_ast_vector_translate(src.ctx(), src, c)); }
533 
535  operator Z3_ast_vector() const { return m_vector; }
536  unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); }
537  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); }
538  void push_back(T const & e) { Z3_ast_vector_push(ctx(), m_vector, e); check_error(); }
539  void resize(unsigned sz) { Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }
540  T back() const { return operator[](size() - 1); }
541  void pop_back() { assert(size() > 0); resize(size() - 1); }
542  bool empty() const { return size() == 0; }
544  Z3_ast_vector_inc_ref(s.ctx(), s.m_vector);
545  Z3_ast_vector_dec_ref(ctx(), m_vector);
546  m_ctx = s.m_ctx;
547  m_vector = s.m_vector;
548  return *this;
549  }
550  ast_vector_tpl& set(unsigned idx, ast& a) {
551  Z3_ast_vector_set(ctx(), m_vector, idx, a);
552  return *this;
553  }
554  /*
555  Disabled pending C++98 build upgrade
556  bool contains(T const& x) const {
557  for (T y : *this) if (eq(x, y)) return true;
558  return false;
559  }
560  */
561 
562  class iterator {
563  ast_vector_tpl const* m_vector;
564  unsigned m_index;
565  public:
566  iterator(ast_vector_tpl const* v, unsigned i): m_vector(v), m_index(i) {}
567  iterator(iterator const& other): m_vector(other.m_vector), m_index(other.m_index) {}
568  iterator operator=(iterator const& other) { m_vector = other.m_vector; m_index = other.m_index; return *this; }
569 
570  bool operator==(iterator const& other) const {
571  return other.m_index == m_index;
572  };
573  bool operator!=(iterator const& other) const {
574  return other.m_index != m_index;
575  };
577  ++m_index;
578  return *this;
579  }
580  void set(T& arg) {
581  Z3_ast_vector_set(m_vector->ctx(), *m_vector, m_index, arg);
582  }
583  iterator operator++(int) { iterator tmp = *this; ++m_index; return tmp; }
584  T * operator->() const { return &(operator*()); }
585  T operator*() const { return (*m_vector)[m_index]; }
586  };
587  iterator begin() const { return iterator(this, 0); }
588  iterator end() const { return iterator(this, size()); }
589  friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
590  };
591 
592 
596  class sort : public ast {
597  public:
598  sort(context & c):ast(c) {}
599  sort(context & c, Z3_sort s):ast(c, reinterpret_cast<Z3_ast>(s)) {}
600  sort(context & c, Z3_ast a):ast(c, a) {}
601  sort(sort const & s):ast(s) {}
602  operator Z3_sort() const { return reinterpret_cast<Z3_sort>(m_ast); }
603 
607  unsigned id() const { unsigned r = Z3_get_sort_id(ctx(), *this); check_error(); return r; }
608 
612  sort & operator=(sort const & s) { return static_cast<sort&>(ast::operator=(s)); }
616  Z3_sort_kind sort_kind() const { return Z3_get_sort_kind(*m_ctx, *this); }
620  symbol name() const { Z3_symbol s = Z3_get_sort_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
624  bool is_bool() const { return sort_kind() == Z3_BOOL_SORT; }
628  bool is_int() const { return sort_kind() == Z3_INT_SORT; }
632  bool is_real() const { return sort_kind() == Z3_REAL_SORT; }
636  bool is_arith() const { return is_int() || is_real(); }
640  bool is_bv() const { return sort_kind() == Z3_BV_SORT; }
644  bool is_array() const { return sort_kind() == Z3_ARRAY_SORT; }
648  bool is_datatype() const { return sort_kind() == Z3_DATATYPE_SORT; }
652  bool is_relation() const { return sort_kind() == Z3_RELATION_SORT; }
656  bool is_seq() const { return sort_kind() == Z3_SEQ_SORT; }
660  bool is_re() const { return sort_kind() == Z3_RE_SORT; }
664  bool is_finite_domain() const { return sort_kind() == Z3_FINITE_DOMAIN_SORT; }
668  bool is_fpa() const { return sort_kind() == Z3_FLOATING_POINT_SORT; }
669 
675  unsigned bv_size() const { assert(is_bv()); unsigned r = Z3_get_bv_sort_size(ctx(), *this); check_error(); return r; }
676 
677  unsigned fpa_ebits() const { assert(is_fpa()); unsigned r = Z3_fpa_get_ebits(ctx(), *this); check_error(); return r; }
678 
679  unsigned fpa_sbits() const { assert(is_fpa()); unsigned r = Z3_fpa_get_sbits(ctx(), *this); check_error(); return r; }
685  sort array_domain() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_domain(ctx(), *this); check_error(); return sort(ctx(), s); }
691  sort array_range() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_range(ctx(), *this); check_error(); return sort(ctx(), s); }
692  };
693 
698  class func_decl : public ast {
699  public:
700  func_decl(context & c):ast(c) {}
701  func_decl(context & c, Z3_func_decl n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
702  func_decl(func_decl const & s):ast(s) {}
703  operator Z3_func_decl() const { return reinterpret_cast<Z3_func_decl>(m_ast); }
704  func_decl & operator=(func_decl const & s) { return static_cast<func_decl&>(ast::operator=(s)); }
705 
709  unsigned id() const { unsigned r = Z3_get_func_decl_id(ctx(), *this); check_error(); return r; }
710 
711  unsigned arity() const { return Z3_get_arity(ctx(), *this); }
712  sort domain(unsigned i) const { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }
713  sort range() const { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }
714  symbol name() const { Z3_symbol s = Z3_get_decl_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
715  Z3_decl_kind decl_kind() const { return Z3_get_decl_kind(ctx(), *this); }
716 
718  Z3_func_decl tc = Z3_mk_transitive_closure(ctx(), *this); check_error(); return func_decl(ctx(), tc);
719  }
720 
721  bool is_const() const { return arity() == 0; }
722 
723  expr operator()() const;
724  expr operator()(unsigned n, expr const * args) const;
725  expr operator()(expr_vector const& v) const;
726  expr operator()(expr const & a) const;
727  expr operator()(int a) const;
728  expr operator()(expr const & a1, expr const & a2) const;
729  expr operator()(expr const & a1, int a2) const;
730  expr operator()(int a1, expr const & a2) const;
731  expr operator()(expr const & a1, expr const & a2, expr const & a3) const;
732  expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const;
733  expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const;
734  };
735 
739  expr select(expr const & a, expr const& i);
740  expr select(expr const & a, expr_vector const & i);
741 
746  class expr : public ast {
747  public:
748  expr(context & c):ast(c) {}
749  expr(context & c, Z3_ast n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
750  expr(expr const & n):ast(n) {}
751  expr & operator=(expr const & n) { return static_cast<expr&>(ast::operator=(n)); }
752 
756  sort get_sort() const { Z3_sort s = Z3_get_sort(*m_ctx, m_ast); check_error(); return sort(*m_ctx, s); }
757 
761  bool is_bool() const { return get_sort().is_bool(); }
765  bool is_int() const { return get_sort().is_int(); }
769  bool is_real() const { return get_sort().is_real(); }
773  bool is_arith() const { return get_sort().is_arith(); }
777  bool is_bv() const { return get_sort().is_bv(); }
781  bool is_array() const { return get_sort().is_array(); }
785  bool is_datatype() const { return get_sort().is_datatype(); }
789  bool is_relation() const { return get_sort().is_relation(); }
793  bool is_seq() const { return get_sort().is_seq(); }
797  bool is_re() const { return get_sort().is_re(); }
798 
807  bool is_finite_domain() const { return get_sort().is_finite_domain(); }
811  bool is_fpa() const { return get_sort().is_fpa(); }
812 
818  bool is_numeral() const { return kind() == Z3_NUMERAL_AST; }
819  bool is_numeral_i64(int64_t& i) const { bool r = Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}
820  bool is_numeral_u64(uint64_t& i) const { bool r = Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}
821  bool is_numeral_i(int& i) const { bool r = Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}
822  bool is_numeral_u(unsigned& i) const { bool r = Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
823  bool is_numeral(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; }
824  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; }
825  bool is_numeral(double& d) const { if (!is_numeral()) return false; d = Z3_get_numeral_double(ctx(), m_ast); check_error(); return true; }
826  bool as_binary(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_binary_string(ctx(), m_ast); check_error(); return true; }
827 
831  bool is_app() const { return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
835  bool is_const() const { return is_app() && num_args() == 0; }
839  bool is_quantifier() const { return kind() == Z3_QUANTIFIER_AST; }
840 
844  bool is_forall() const { return Z3_is_quantifier_forall(ctx(), m_ast); }
848  bool is_exists() const { return Z3_is_quantifier_exists(ctx(), m_ast); }
852  bool is_lambda() const { return Z3_is_lambda(ctx(), m_ast); }
857  bool is_var() const { return kind() == Z3_VAR_AST; }
861  bool is_algebraic() const { return Z3_is_algebraic_number(ctx(), m_ast); }
862 
866  bool is_well_sorted() const { bool r = Z3_is_well_sorted(ctx(), m_ast); check_error(); return r; }
867 
874  std::string get_decimal_string(int precision) const {
875  assert(is_numeral() || is_algebraic());
876  return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
877  }
878 
882  expr algebraic_lower(unsigned precision) const {
883  assert(is_algebraic());
884  Z3_ast r = Z3_get_algebraic_number_lower(ctx(), m_ast, precision);
885  check_error();
886  return expr(ctx(), r);
887  }
888 
889  expr algebraic_upper(unsigned precision) const {
890  assert(is_algebraic());
891  Z3_ast r = Z3_get_algebraic_number_upper(ctx(), m_ast, precision);
892  check_error();
893  return expr(ctx(), r);
894  }
895 
900  assert(is_algebraic());
901  Z3_ast_vector r = Z3_algebraic_get_poly(ctx(), m_ast);
902  check_error();
903  return expr_vector(ctx(), r);
904  }
905 
909  unsigned algebraic_i() const {
910  assert(is_algebraic());
911  unsigned i = Z3_algebraic_get_i(ctx(), m_ast);
912  check_error();
913  return i;
914  }
915 
919  unsigned id() const { unsigned r = Z3_get_ast_id(ctx(), m_ast); check_error(); return r; }
920 
931  int get_numeral_int() const {
932  int result = 0;
933  if (!is_numeral_i(result)) {
934  assert(ctx().enable_exceptions());
935  if (!ctx().enable_exceptions()) return 0;
936  Z3_THROW(exception("numeral does not fit in machine int"));
937  }
938  return result;
939  }
940 
950  unsigned get_numeral_uint() const {
951  assert(is_numeral());
952  unsigned result = 0;
953  if (!is_numeral_u(result)) {
954  assert(ctx().enable_exceptions());
955  if (!ctx().enable_exceptions()) return 0;
956  Z3_THROW(exception("numeral does not fit in machine uint"));
957  }
958  return result;
959  }
960 
967  int64_t get_numeral_int64() const {
968  assert(is_numeral());
969  int64_t result = 0;
970  if (!is_numeral_i64(result)) {
971  assert(ctx().enable_exceptions());
972  if (!ctx().enable_exceptions()) return 0;
973  Z3_THROW(exception("numeral does not fit in machine int64_t"));
974  }
975  return result;
976  }
977 
984  uint64_t get_numeral_uint64() const {
985  assert(is_numeral());
986  uint64_t result = 0;
987  if (!is_numeral_u64(result)) {
988  assert(ctx().enable_exceptions());
989  if (!ctx().enable_exceptions()) return 0;
990  Z3_THROW(exception("numeral does not fit in machine uint64_t"));
991  }
992  return result;
993  }
994 
996  return Z3_get_bool_value(ctx(), m_ast);
997  }
998 
999  expr numerator() const {
1000  assert(is_numeral());
1001  Z3_ast r = Z3_get_numerator(ctx(), m_ast);
1002  check_error();
1003  return expr(ctx(),r);
1004  }
1005 
1006 
1007  expr denominator() const {
1008  assert(is_numeral());
1009  Z3_ast r = Z3_get_denominator(ctx(), m_ast);
1010  check_error();
1011  return expr(ctx(),r);
1012  }
1013 
1014 
1019  bool is_string_value() const { return Z3_is_string(ctx(), m_ast); }
1020 
1026  std::string get_escaped_string() const {
1027  assert(is_string_value());
1028  char const* s = Z3_get_string(ctx(), m_ast);
1029  check_error();
1030  return std::string(s);
1031  }
1032 
1033  std::string get_string() const {
1034  assert(is_string_value());
1035  unsigned n;
1036  char const* s = Z3_get_lstring(ctx(), m_ast, &n);
1037  check_error();
1038  return std::string(s, n);
1039  }
1040 
1041  operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
1042 
1047  assert(is_fpa());
1048  Z3_sort s = ctx().fpa_rounding_mode();
1049  check_error();
1050  return sort(ctx(), s);
1051  }
1052 
1053 
1060  func_decl decl() const { Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }
1067  unsigned num_args() const { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
1075  expr arg(unsigned i) const { Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }
1076 
1082  expr body() const { assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
1083 
1089  friend expr operator!(expr const & a);
1090 
1097  friend expr operator&&(expr const & a, expr const & b);
1098 
1099 
1106  friend expr operator&&(expr const & a, bool b);
1113  friend expr operator&&(bool a, expr const & b);
1114 
1121  friend expr operator||(expr const & a, expr const & b);
1128  friend expr operator||(expr const & a, bool b);
1129 
1136  friend expr operator||(bool a, expr const & b);
1137 
1138  friend expr implies(expr const & a, expr const & b);
1139  friend expr implies(expr const & a, bool b);
1140  friend expr implies(bool a, expr const & b);
1141 
1142  friend expr mk_or(expr_vector const& args);
1143  friend expr mk_and(expr_vector const& args);
1144 
1145  friend expr ite(expr const & c, expr const & t, expr const & e);
1146 
1147  bool is_true() const { return is_app() && Z3_OP_TRUE == decl().decl_kind(); }
1148  bool is_false() const { return is_app() && Z3_OP_FALSE == decl().decl_kind(); }
1149  bool is_not() const { return is_app() && Z3_OP_NOT == decl().decl_kind(); }
1150  bool is_and() const { return is_app() && Z3_OP_AND == decl().decl_kind(); }
1151  bool is_or() const { return is_app() && Z3_OP_OR == decl().decl_kind(); }
1152  bool is_xor() const { return is_app() && Z3_OP_XOR == decl().decl_kind(); }
1153  bool is_implies() const { return is_app() && Z3_OP_IMPLIES == decl().decl_kind(); }
1154  bool is_eq() const { return is_app() && Z3_OP_EQ == decl().decl_kind(); }
1155  bool is_ite() const { return is_app() && Z3_OP_ITE == decl().decl_kind(); }
1156  bool is_distinct() const { return is_app() && Z3_OP_DISTINCT == decl().decl_kind(); }
1157 
1158  friend expr distinct(expr_vector const& args);
1159  friend expr concat(expr const& a, expr const& b);
1160  friend expr concat(expr_vector const& args);
1161 
1162  friend expr operator==(expr const & a, expr const & b);
1163  friend expr operator==(expr const & a, int b);
1164  friend expr operator==(int a, expr const & b);
1165 
1166  friend expr operator!=(expr const & a, expr const & b);
1167  friend expr operator!=(expr const & a, int b);
1168  friend expr operator!=(int a, expr const & b);
1169 
1170  friend expr operator+(expr const & a, expr const & b);
1171  friend expr operator+(expr const & a, int b);
1172  friend expr operator+(int a, expr const & b);
1173  friend expr sum(expr_vector const& args);
1174 
1175  friend expr operator*(expr const & a, expr const & b);
1176  friend expr operator*(expr const & a, int b);
1177  friend expr operator*(int a, expr const & b);
1178 
1179  /* \brief Power operator */
1180  friend expr pw(expr const & a, expr const & b);
1181  friend expr pw(expr const & a, int b);
1182  friend expr pw(int a, expr const & b);
1183 
1184  /* \brief mod operator */
1185  friend expr mod(expr const& a, expr const& b);
1186  friend expr mod(expr const& a, int b);
1187  friend expr mod(int a, expr const& b);
1188 
1189  /* \brief rem operator */
1190  friend expr rem(expr const& a, expr const& b);
1191  friend expr rem(expr const& a, int b);
1192  friend expr rem(int a, expr const& b);
1193 
1194  friend expr is_int(expr const& e);
1195 
1196  friend expr operator/(expr const & a, expr const & b);
1197  friend expr operator/(expr const & a, int b);
1198  friend expr operator/(int a, expr const & b);
1199 
1200  friend expr operator-(expr const & a);
1201 
1202  friend expr operator-(expr const & a, expr const & b);
1203  friend expr operator-(expr const & a, int b);
1204  friend expr operator-(int a, expr const & b);
1205 
1206  friend expr operator<=(expr const & a, expr const & b);
1207  friend expr operator<=(expr const & a, int b);
1208  friend expr operator<=(int a, expr const & b);
1209 
1210 
1211  friend expr operator>=(expr const & a, expr const & b);
1212  friend expr operator>=(expr const & a, int b);
1213  friend expr operator>=(int a, expr const & b);
1214 
1215  friend expr operator<(expr const & a, expr const & b);
1216  friend expr operator<(expr const & a, int b);
1217  friend expr operator<(int a, expr const & b);
1218 
1219  friend expr operator>(expr const & a, expr const & b);
1220  friend expr operator>(expr const & a, int b);
1221  friend expr operator>(int a, expr const & b);
1222 
1223  friend expr pble(expr_vector const& es, int const * coeffs, int bound);
1224  friend expr pbge(expr_vector const& es, int const * coeffs, int bound);
1225  friend expr pbeq(expr_vector const& es, int const * coeffs, int bound);
1226  friend expr atmost(expr_vector const& es, unsigned bound);
1227  friend expr atleast(expr_vector const& es, unsigned bound);
1228 
1229  friend expr operator&(expr const & a, expr const & b);
1230  friend expr operator&(expr const & a, int b);
1231  friend expr operator&(int a, expr const & b);
1232 
1233  friend expr operator^(expr const & a, expr const & b);
1234  friend expr operator^(expr const & a, int b);
1235  friend expr operator^(int a, expr const & b);
1236 
1237  friend expr operator|(expr const & a, expr const & b);
1238  friend expr operator|(expr const & a, int b);
1239  friend expr operator|(int a, expr const & b);
1240  friend expr nand(expr const& a, expr const& b);
1241  friend expr nor(expr const& a, expr const& b);
1242  friend expr xnor(expr const& a, expr const& b);
1243 
1244  friend expr min(expr const& a, expr const& b);
1245  friend expr max(expr const& a, expr const& b);
1246 
1247  friend expr bv2int(expr const& a, bool is_signed);
1248  friend expr int2bv(unsigned n, expr const& a);
1249  friend expr bvadd_no_overflow(expr const& a, expr const& b, bool is_signed);
1250  friend expr bvadd_no_underflow(expr const& a, expr const& b);
1251  friend expr bvsub_no_overflow(expr const& a, expr const& b);
1252  friend expr bvsub_no_underflow(expr const& a, expr const& b, bool is_signed);
1253  friend expr bvsdiv_no_overflow(expr const& a, expr const& b);
1254  friend expr bvneg_no_overflow(expr const& a);
1255  friend expr bvmul_no_overflow(expr const& a, expr const& b, bool is_signed);
1256  friend expr bvmul_no_underflow(expr const& a, expr const& b);
1257 
1258  expr rotate_left(unsigned i) { Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
1259  expr rotate_right(unsigned i) { Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
1260  expr repeat(unsigned i) { Z3_ast r = Z3_mk_repeat(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
1261 
1262  friend expr abs(expr const & a);
1263  friend expr sqrt(expr const & a, expr const & rm);
1264 
1265  friend expr operator~(expr const & a);
1266  expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }
1267  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)); }
1268  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)); }
1269 
1273  friend expr fma(expr const& a, expr const& b, expr const& c, expr const& rm);
1274 
1280  expr extract(expr const& offset, expr const& length) const {
1281  check_context(*this, offset); check_context(offset, length);
1282  Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
1283  }
1284  expr replace(expr const& src, expr const& dst) const {
1285  check_context(*this, src); check_context(src, dst);
1286  Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
1287  check_error();
1288  return expr(ctx(), r);
1289  }
1290  expr unit() const {
1291  Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
1292  check_error();
1293  return expr(ctx(), r);
1294  }
1295  expr contains(expr const& s) {
1296  check_context(*this, s);
1297  Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
1298  check_error();
1299  return expr(ctx(), r);
1300  }
1301  expr at(expr const& index) const {
1302  check_context(*this, index);
1303  Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
1304  check_error();
1305  return expr(ctx(), r);
1306  }
1307  expr nth(expr const& index) const {
1308  check_context(*this, index);
1309  Z3_ast r = Z3_mk_seq_nth(ctx(), *this, index);
1310  check_error();
1311  return expr(ctx(), r);
1312  }
1313  expr length() const {
1314  Z3_ast r = Z3_mk_seq_length(ctx(), *this);
1315  check_error();
1316  return expr(ctx(), r);
1317  }
1318  expr stoi() const {
1319  Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
1320  check_error();
1321  return expr(ctx(), r);
1322  }
1323  expr itos() const {
1324  Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
1325  check_error();
1326  return expr(ctx(), r);
1327  }
1328 
1329  friend expr range(expr const& lo, expr const& hi);
1333  expr loop(unsigned lo) {
1334  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0);
1335  check_error();
1336  return expr(ctx(), r);
1337  }
1338  expr loop(unsigned lo, unsigned hi) {
1339  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi);
1340  check_error();
1341  return expr(ctx(), r);
1342  }
1343 
1347  expr operator[](expr const& index) const {
1348  assert(is_array() || is_seq());
1349  if (is_array()) {
1350  return select(*this, index);
1351  }
1352  return nth(index);
1353  }
1354 
1355  expr operator[](expr_vector const& index) const {
1356  return select(*this, index);
1357  }
1358 
1362  expr simplify() const { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
1366  expr simplify(params const & p) const { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
1367 
1371  expr substitute(expr_vector const& src, expr_vector const& dst);
1372 
1376  expr substitute(expr_vector const& dst);
1377 
1378  };
1379 
1380 #define _Z3_MK_BIN_(a, b, binop) \
1381  check_context(a, b); \
1382  Z3_ast r = binop(a.ctx(), a, b); \
1383  a.check_error(); \
1384  return expr(a.ctx(), r); \
1385 
1386 
1387  inline expr implies(expr const & a, expr const & b) {
1388  assert(a.is_bool() && b.is_bool());
1389  _Z3_MK_BIN_(a, b, Z3_mk_implies);
1390  }
1391  inline expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); }
1392  inline expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); }
1393 
1394 
1395  inline expr pw(expr const & a, expr const & b) { _Z3_MK_BIN_(a, b, Z3_mk_power); }
1396  inline expr pw(expr const & a, int b) { return pw(a, a.ctx().num_val(b, a.get_sort())); }
1397  inline expr pw(int a, expr const & b) { return pw(b.ctx().num_val(a, b.get_sort()), b); }
1398 
1399  inline expr mod(expr const& a, expr const& b) {
1400  if (a.is_bv()) {
1401  _Z3_MK_BIN_(a, b, Z3_mk_bvsmod);
1402  }
1403  else {
1404  _Z3_MK_BIN_(a, b, Z3_mk_mod);
1405  }
1406  }
1407  inline expr mod(expr const & a, int b) { return mod(a, a.ctx().num_val(b, a.get_sort())); }
1408  inline expr mod(int a, expr const & b) { return mod(b.ctx().num_val(a, b.get_sort()), b); }
1409 
1410  inline expr operator%(expr const& a, expr const& b) { return mod(a, b); }
1411  inline expr operator%(expr const& a, int b) { return mod(a, b); }
1412  inline expr operator%(int a, expr const& b) { return mod(a, b); }
1413 
1414 
1415  inline expr rem(expr const& a, expr const& b) {
1416  if (a.is_fpa() && b.is_fpa()) {
1417  _Z3_MK_BIN_(a, b, Z3_mk_fpa_rem);
1418  } else {
1419  _Z3_MK_BIN_(a, b, Z3_mk_rem);
1420  }
1421  }
1422  inline expr rem(expr const & a, int b) { return rem(a, a.ctx().num_val(b, a.get_sort())); }
1423  inline expr rem(int a, expr const & b) { return rem(b.ctx().num_val(a, b.get_sort()), b); }
1424 
1425 #undef _Z3_MK_BIN_
1426 
1427 #define _Z3_MK_UN_(a, mkun) \
1428  Z3_ast r = mkun(a.ctx(), a); \
1429  a.check_error(); \
1430  return expr(a.ctx(), r); \
1431 
1432 
1433  inline expr operator!(expr const & a) { assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); }
1434 
1435  inline expr is_int(expr const& e) { _Z3_MK_UN_(e, Z3_mk_is_int); }
1436 
1437 #undef _Z3_MK_UN_
1438 
1439  inline expr operator&&(expr const & a, expr const & b) {
1440  check_context(a, b);
1441  assert(a.is_bool() && b.is_bool());
1442  Z3_ast args[2] = { a, b };
1443  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1444  a.check_error();
1445  return expr(a.ctx(), r);
1446  }
1447 
1448  inline expr operator&&(expr const & a, bool b) { return a && a.ctx().bool_val(b); }
1449  inline expr operator&&(bool a, expr const & b) { return b.ctx().bool_val(a) && b; }
1450 
1451  inline expr operator||(expr const & a, expr const & b) {
1452  check_context(a, b);
1453  assert(a.is_bool() && b.is_bool());
1454  Z3_ast args[2] = { a, b };
1455  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1456  a.check_error();
1457  return expr(a.ctx(), r);
1458  }
1459 
1460  inline expr operator||(expr const & a, bool b) { return a || a.ctx().bool_val(b); }
1461 
1462  inline expr operator||(bool a, expr const & b) { return b.ctx().bool_val(a) || b; }
1463 
1464  inline expr operator==(expr const & a, expr const & b) {
1465  check_context(a, b);
1466  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1467  a.check_error();
1468  return expr(a.ctx(), r);
1469  }
1470  inline expr operator==(expr const & a, int b) { assert(a.is_arith() || a.is_bv() || a.is_fpa()); return a == a.ctx().num_val(b, a.get_sort()); }
1471  inline expr operator==(int a, expr const & b) { assert(b.is_arith() || b.is_bv() || b.is_fpa()); return b.ctx().num_val(a, b.get_sort()) == b; }
1472  inline expr operator==(expr const & a, double b) { assert(a.is_fpa()); return a == a.ctx().fpa_val(b); }
1473  inline expr operator==(double a, expr const & b) { assert(b.is_fpa()); return b.ctx().fpa_val(a) == b; }
1474 
1475  inline expr operator!=(expr const & a, expr const & b) {
1476  check_context(a, b);
1477  Z3_ast args[2] = { a, b };
1478  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1479  a.check_error();
1480  return expr(a.ctx(), r);
1481  }
1482  inline expr operator!=(expr const & a, int b) { assert(a.is_arith() || a.is_bv() || a.is_fpa()); return a != a.ctx().num_val(b, a.get_sort()); }
1483  inline expr operator!=(int a, expr const & b) { assert(b.is_arith() || b.is_bv() || b.is_fpa()); return b.ctx().num_val(a, b.get_sort()) != b; }
1484  inline expr operator!=(expr const & a, double b) { assert(a.is_fpa()); return a != a.ctx().fpa_val(b); }
1485  inline expr operator!=(double a, expr const & b) { assert(b.is_fpa()); return b.ctx().fpa_val(a) != b; }
1486 
1487  inline expr operator+(expr const & a, expr const & b) {
1488  check_context(a, b);
1489  Z3_ast r = 0;
1490  if (a.is_arith() && b.is_arith()) {
1491  Z3_ast args[2] = { a, b };
1492  r = Z3_mk_add(a.ctx(), 2, args);
1493  }
1494  else if (a.is_bv() && b.is_bv()) {
1495  r = Z3_mk_bvadd(a.ctx(), a, b);
1496  }
1497  else if (a.is_seq() && b.is_seq()) {
1498  return concat(a, b);
1499  }
1500  else if (a.is_re() && b.is_re()) {
1501  Z3_ast _args[2] = { a, b };
1502  r = Z3_mk_re_union(a.ctx(), 2, _args);
1503  }
1504  else if (a.is_fpa() && b.is_fpa()) {
1505  r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1506  }
1507  else {
1508  // operator is not supported by given arguments.
1509  assert(false);
1510  }
1511  a.check_error();
1512  return expr(a.ctx(), r);
1513  }
1514  inline expr operator+(expr const & a, int b) { return a + a.ctx().num_val(b, a.get_sort()); }
1515  inline expr operator+(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) + b; }
1516 
1517  inline expr operator*(expr const & a, expr const & b) {
1518  check_context(a, b);
1519  Z3_ast r = 0;
1520  if (a.is_arith() && b.is_arith()) {
1521  Z3_ast args[2] = { a, b };
1522  r = Z3_mk_mul(a.ctx(), 2, args);
1523  }
1524  else if (a.is_bv() && b.is_bv()) {
1525  r = Z3_mk_bvmul(a.ctx(), a, b);
1526  }
1527  else if (a.is_fpa() && b.is_fpa()) {
1528  r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1529  }
1530  else {
1531  // operator is not supported by given arguments.
1532  assert(false);
1533  }
1534  a.check_error();
1535  return expr(a.ctx(), r);
1536  }
1537  inline expr operator*(expr const & a, int b) { return a * a.ctx().num_val(b, a.get_sort()); }
1538  inline expr operator*(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) * b; }
1539 
1540 
1541  inline expr operator>=(expr const & a, expr const & b) {
1542  check_context(a, b);
1543  Z3_ast r = 0;
1544  if (a.is_arith() && b.is_arith()) {
1545  r = Z3_mk_ge(a.ctx(), a, b);
1546  }
1547  else if (a.is_bv() && b.is_bv()) {
1548  r = Z3_mk_bvsge(a.ctx(), a, b);
1549  }
1550  else if (a.is_fpa() && b.is_fpa()) {
1551  r = Z3_mk_fpa_geq(a.ctx(), a, b);
1552  }
1553  else {
1554  // operator is not supported by given arguments.
1555  assert(false);
1556  }
1557  a.check_error();
1558  return expr(a.ctx(), r);
1559  }
1560 
1561  inline expr operator/(expr const & a, expr const & b) {
1562  check_context(a, b);
1563  Z3_ast r = 0;
1564  if (a.is_arith() && b.is_arith()) {
1565  r = Z3_mk_div(a.ctx(), a, b);
1566  }
1567  else if (a.is_bv() && b.is_bv()) {
1568  r = Z3_mk_bvsdiv(a.ctx(), a, b);
1569  }
1570  else if (a.is_fpa() && b.is_fpa()) {
1571  r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1572  }
1573  else {
1574  // operator is not supported by given arguments.
1575  assert(false);
1576  }
1577  a.check_error();
1578  return expr(a.ctx(), r);
1579  }
1580  inline expr operator/(expr const & a, int b) { return a / a.ctx().num_val(b, a.get_sort()); }
1581  inline expr operator/(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) / b; }
1582 
1583  inline expr operator-(expr const & a) {
1584  Z3_ast r = 0;
1585  if (a.is_arith()) {
1586  r = Z3_mk_unary_minus(a.ctx(), a);
1587  }
1588  else if (a.is_bv()) {
1589  r = Z3_mk_bvneg(a.ctx(), a);
1590  }
1591  else if (a.is_fpa()) {
1592  r = Z3_mk_fpa_neg(a.ctx(), a);
1593  }
1594  else {
1595  // operator is not supported by given arguments.
1596  assert(false);
1597  }
1598  a.check_error();
1599  return expr(a.ctx(), r);
1600  }
1601 
1602  inline expr operator-(expr const & a, expr const & b) {
1603  check_context(a, b);
1604  Z3_ast r = 0;
1605  if (a.is_arith() && b.is_arith()) {
1606  Z3_ast args[2] = { a, b };
1607  r = Z3_mk_sub(a.ctx(), 2, args);
1608  }
1609  else if (a.is_bv() && b.is_bv()) {
1610  r = Z3_mk_bvsub(a.ctx(), a, b);
1611  }
1612  else if (a.is_fpa() && b.is_fpa()) {
1613  r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1614  }
1615  else {
1616  // operator is not supported by given arguments.
1617  assert(false);
1618  }
1619  a.check_error();
1620  return expr(a.ctx(), r);
1621  }
1622  inline expr operator-(expr const & a, int b) { return a - a.ctx().num_val(b, a.get_sort()); }
1623  inline expr operator-(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) - b; }
1624 
1625  inline expr operator<=(expr const & a, expr const & b) {
1626  check_context(a, b);
1627  Z3_ast r = 0;
1628  if (a.is_arith() && b.is_arith()) {
1629  r = Z3_mk_le(a.ctx(), a, b);
1630  }
1631  else if (a.is_bv() && b.is_bv()) {
1632  r = Z3_mk_bvsle(a.ctx(), a, b);
1633  }
1634  else if (a.is_fpa() && b.is_fpa()) {
1635  r = Z3_mk_fpa_leq(a.ctx(), a, b);
1636  }
1637  else {
1638  // operator is not supported by given arguments.
1639  assert(false);
1640  }
1641  a.check_error();
1642  return expr(a.ctx(), r);
1643  }
1644  inline expr operator<=(expr const & a, int b) { return a <= a.ctx().num_val(b, a.get_sort()); }
1645  inline expr operator<=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) <= b; }
1646 
1647  inline expr operator>=(expr const & a, int b) { return a >= a.ctx().num_val(b, a.get_sort()); }
1648  inline expr operator>=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) >= b; }
1649 
1650  inline expr operator<(expr const & a, expr const & b) {
1651  check_context(a, b);
1652  Z3_ast r = 0;
1653  if (a.is_arith() && b.is_arith()) {
1654  r = Z3_mk_lt(a.ctx(), a, b);
1655  }
1656  else if (a.is_bv() && b.is_bv()) {
1657  r = Z3_mk_bvslt(a.ctx(), a, b);
1658  }
1659  else if (a.is_fpa() && b.is_fpa()) {
1660  r = Z3_mk_fpa_lt(a.ctx(), a, b);
1661  }
1662  else {
1663  // operator is not supported by given arguments.
1664  assert(false);
1665  }
1666  a.check_error();
1667  return expr(a.ctx(), r);
1668  }
1669  inline expr operator<(expr const & a, int b) { return a < a.ctx().num_val(b, a.get_sort()); }
1670  inline expr operator<(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) < b; }
1671 
1672  inline expr operator>(expr const & a, expr const & b) {
1673  check_context(a, b);
1674  Z3_ast r = 0;
1675  if (a.is_arith() && b.is_arith()) {
1676  r = Z3_mk_gt(a.ctx(), a, b);
1677  }
1678  else if (a.is_bv() && b.is_bv()) {
1679  r = Z3_mk_bvsgt(a.ctx(), a, b);
1680  }
1681  else if (a.is_fpa() && b.is_fpa()) {
1682  r = Z3_mk_fpa_gt(a.ctx(), a, b);
1683  }
1684  else {
1685  // operator is not supported by given arguments.
1686  assert(false);
1687  }
1688  a.check_error();
1689  return expr(a.ctx(), r);
1690  }
1691  inline expr operator>(expr const & a, int b) { return a > a.ctx().num_val(b, a.get_sort()); }
1692  inline expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > b; }
1693 
1694  inline expr operator&(expr const & a, expr const & b) { if (a.is_bool()) return a && b; check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); return expr(a.ctx(), r); }
1695  inline expr operator&(expr const & a, int b) { return a & a.ctx().num_val(b, a.get_sort()); }
1696  inline expr operator&(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) & b; }
1697 
1698  inline expr operator^(expr const & a, expr const & b) { check_context(a, b); Z3_ast r = a.is_bool() ? Z3_mk_xor(a.ctx(), a, b) : Z3_mk_bvxor(a.ctx(), a, b); return expr(a.ctx(), r); }
1699  inline expr operator^(expr const & a, int b) { return a ^ a.ctx().num_val(b, a.get_sort()); }
1700  inline expr operator^(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) ^ b; }
1701 
1702  inline expr operator|(expr const & a, expr const & b) { if (a.is_bool()) return a || b; check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); return expr(a.ctx(), r); }
1703  inline expr operator|(expr const & a, int b) { return a | a.ctx().num_val(b, a.get_sort()); }
1704  inline expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; }
1705 
1706  inline expr nand(expr const& a, expr const& b) { if (a.is_bool()) return !(a && b); check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); return expr(a.ctx(), r); }
1707  inline expr nor(expr const& a, expr const& b) { if (a.is_bool()) return !(a || b); check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); return expr(a.ctx(), r); }
1708  inline expr xnor(expr const& a, expr const& b) { if (a.is_bool()) return !(a ^ b); check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); return expr(a.ctx(), r); }
1709  inline expr min(expr const& a, expr const& b) {
1710  check_context(a, b);
1711  Z3_ast r;
1712  if (a.is_arith()) {
1713  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
1714  }
1715  else if (a.is_bv()) {
1716  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
1717  }
1718  else {
1719  assert(a.is_fpa());
1720  r = Z3_mk_fpa_min(a.ctx(), a, b);
1721  }
1722  return expr(a.ctx(), r);
1723  }
1724  inline expr max(expr const& a, expr const& b) {
1725  check_context(a, b);
1726  Z3_ast r;
1727  if (a.is_arith()) {
1728  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
1729  }
1730  else if (a.is_bv()) {
1731  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
1732  }
1733  else {
1734  assert(a.is_fpa());
1735  r = Z3_mk_fpa_max(a.ctx(), a, b);
1736  }
1737  return expr(a.ctx(), r);
1738  }
1739  inline expr abs(expr const & a) {
1740  Z3_ast r;
1741  if (a.is_int()) {
1742  expr zero = a.ctx().int_val(0);
1743  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1744  }
1745  else if (a.is_real()) {
1746  expr zero = a.ctx().real_val(0);
1747  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1748  }
1749  else {
1750  r = Z3_mk_fpa_abs(a.ctx(), a);
1751  }
1752  a.check_error();
1753  return expr(a.ctx(), r);
1754  }
1755  inline expr sqrt(expr const & a, expr const& rm) {
1756  check_context(a, rm);
1757  assert(a.is_fpa());
1758  Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
1759  a.check_error();
1760  return expr(a.ctx(), r);
1761  }
1762  inline expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
1763 
1764  inline expr fma(expr const& a, expr const& b, expr const& c, expr const& rm) {
1765  check_context(a, b); check_context(a, c); check_context(a, rm);
1766  assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
1767  Z3_ast r = Z3_mk_fpa_fma(a.ctx(), rm, a, b, c);
1768  a.check_error();
1769  return expr(a.ctx(), r);
1770  }
1771 
1772 
1778  inline expr ite(expr const & c, expr const & t, expr const & e) {
1779  check_context(c, t); check_context(c, e);
1780  assert(c.is_bool());
1781  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
1782  c.check_error();
1783  return expr(c.ctx(), r);
1784  }
1785 
1786 
1791  inline expr to_expr(context & c, Z3_ast a) {
1792  c.check_error();
1793  assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
1794  Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
1795  Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
1797  return expr(c, a);
1798  }
1799 
1800  inline sort to_sort(context & c, Z3_sort s) {
1801  c.check_error();
1802  return sort(c, s);
1803  }
1804 
1805  inline func_decl to_func_decl(context & c, Z3_func_decl f) {
1806  c.check_error();
1807  return func_decl(c, f);
1808  }
1809 
1813  inline expr sle(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsle(a.ctx(), a, b)); }
1814  inline expr sle(expr const & a, int b) { return sle(a, a.ctx().num_val(b, a.get_sort())); }
1815  inline expr sle(int a, expr const & b) { return sle(b.ctx().num_val(a, b.get_sort()), b); }
1819  inline expr slt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvslt(a.ctx(), a, b)); }
1820  inline expr slt(expr const & a, int b) { return slt(a, a.ctx().num_val(b, a.get_sort())); }
1821  inline expr slt(int a, expr const & b) { return slt(b.ctx().num_val(a, b.get_sort()), b); }
1822 
1823 
1827  inline expr ule(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
1828  inline expr ule(expr const & a, int b) { return ule(a, a.ctx().num_val(b, a.get_sort())); }
1829  inline expr ule(int a, expr const & b) { return ule(b.ctx().num_val(a, b.get_sort()), b); }
1833  inline expr ult(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }
1834  inline expr ult(expr const & a, int b) { return ult(a, a.ctx().num_val(b, a.get_sort())); }
1835  inline expr ult(int a, expr const & b) { return ult(b.ctx().num_val(a, b.get_sort()), b); }
1839  inline expr uge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }
1840  inline expr uge(expr const & a, int b) { return uge(a, a.ctx().num_val(b, a.get_sort())); }
1841  inline expr uge(int a, expr const & b) { return uge(b.ctx().num_val(a, b.get_sort()), b); }
1845  inline expr ugt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
1846  inline expr ugt(expr const & a, int b) { return ugt(a, a.ctx().num_val(b, a.get_sort())); }
1847  inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), b); }
1851  inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
1852  inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); }
1853  inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); }
1854 
1858  inline expr srem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsrem(a.ctx(), a, b)); }
1859  inline expr srem(expr const & a, int b) { return srem(a, a.ctx().num_val(b, a.get_sort())); }
1860  inline expr srem(int a, expr const & b) { return srem(b.ctx().num_val(a, b.get_sort()), b); }
1861 
1865  inline expr smod(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsmod(a.ctx(), a, b)); }
1866  inline expr smod(expr const & a, int b) { return smod(a, a.ctx().num_val(b, a.get_sort())); }
1867  inline expr smod(int a, expr const & b) { return smod(b.ctx().num_val(a, b.get_sort()), b); }
1868 
1872  inline expr urem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvurem(a.ctx(), a, b)); }
1873  inline expr urem(expr const & a, int b) { return urem(a, a.ctx().num_val(b, a.get_sort())); }
1874  inline expr urem(int a, expr const & b) { return urem(b.ctx().num_val(a, b.get_sort()), b); }
1875 
1879  inline expr shl(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvshl(a.ctx(), a, b)); }
1880  inline expr shl(expr const & a, int b) { return shl(a, a.ctx().num_val(b, a.get_sort())); }
1881  inline expr shl(int a, expr const & b) { return shl(b.ctx().num_val(a, b.get_sort()), b); }
1882 
1886  inline expr lshr(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvlshr(a.ctx(), a, b)); }
1887  inline expr lshr(expr const & a, int b) { return lshr(a, a.ctx().num_val(b, a.get_sort())); }
1888  inline expr lshr(int a, expr const & b) { return lshr(b.ctx().num_val(a, b.get_sort()), b); }
1889 
1893  inline expr ashr(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvashr(a.ctx(), a, b)); }
1894  inline expr ashr(expr const & a, int b) { return ashr(a, a.ctx().num_val(b, a.get_sort())); }
1895  inline expr ashr(int a, expr const & b) { return ashr(b.ctx().num_val(a, b.get_sort()), b); }
1896 
1900  inline expr zext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_zero_ext(a.ctx(), i, a)); }
1901 
1905  inline expr bv2int(expr const& a, bool is_signed) { Z3_ast r = Z3_mk_bv2int(a.ctx(), a, is_signed); a.check_error(); return expr(a.ctx(), r); }
1906  inline expr int2bv(unsigned n, expr const& a) { Z3_ast r = Z3_mk_int2bv(a.ctx(), n, a); a.check_error(); return expr(a.ctx(), r); }
1907 
1911  inline expr bvadd_no_overflow(expr const& a, expr const& b, bool is_signed) {
1912  check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_overflow(a.ctx(), a, b, is_signed); a.check_error(); return expr(a.ctx(), r);
1913  }
1914  inline expr bvadd_no_underflow(expr const& a, expr const& b) {
1915  check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1916  }
1917  inline expr bvsub_no_overflow(expr const& a, expr const& b) {
1918  check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1919  }
1920  inline expr bvsub_no_underflow(expr const& a, expr const& b, bool is_signed) {
1921  check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_underflow(a.ctx(), a, b, is_signed); a.check_error(); return expr(a.ctx(), r);
1922  }
1923  inline expr bvsdiv_no_overflow(expr const& a, expr const& b) {
1924  check_context(a, b); Z3_ast r = Z3_mk_bvsdiv_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1925  }
1926  inline expr bvneg_no_overflow(expr const& a) {
1927  Z3_ast r = Z3_mk_bvneg_no_overflow(a.ctx(), a); a.check_error(); return expr(a.ctx(), r);
1928  }
1929  inline expr bvmul_no_overflow(expr const& a, expr const& b, bool is_signed) {
1930  check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_overflow(a.ctx(), a, b, is_signed); a.check_error(); return expr(a.ctx(), r);
1931  }
1932  inline expr bvmul_no_underflow(expr const& a, expr const& b) {
1933  check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1934  }
1935 
1936 
1940  inline expr sext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_sign_ext(a.ctx(), i, a)); }
1941 
1942  inline func_decl linear_order(sort const& a, unsigned index) {
1943  return to_func_decl(a.ctx(), Z3_mk_linear_order(a.ctx(), a, index));
1944  }
1945  inline func_decl partial_order(sort const& a, unsigned index) {
1946  return to_func_decl(a.ctx(), Z3_mk_partial_order(a.ctx(), a, index));
1947  }
1948  inline func_decl piecewise_linear_order(sort const& a, unsigned index) {
1949  return to_func_decl(a.ctx(), Z3_mk_piecewise_linear_order(a.ctx(), a, index));
1950  }
1951  inline func_decl tree_order(sort const& a, unsigned index) {
1952  return to_func_decl(a.ctx(), Z3_mk_tree_order(a.ctx(), a, index));
1953  }
1954 
1955  template<> class cast_ast<ast> {
1956  public:
1957  ast operator()(context & c, Z3_ast a) { return ast(c, a); }
1958  };
1959 
1960  template<> class cast_ast<expr> {
1961  public:
1962  expr operator()(context & c, Z3_ast a) {
1963  assert(Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
1964  Z3_get_ast_kind(c, a) == Z3_APP_AST ||
1966  Z3_get_ast_kind(c, a) == Z3_VAR_AST);
1967  return expr(c, a);
1968  }
1969  };
1970 
1971  template<> class cast_ast<sort> {
1972  public:
1973  sort operator()(context & c, Z3_ast a) {
1974  assert(Z3_get_ast_kind(c, a) == Z3_SORT_AST);
1975  return sort(c, reinterpret_cast<Z3_sort>(a));
1976  }
1977  };
1978 
1979  template<> class cast_ast<func_decl> {
1980  public:
1981  func_decl operator()(context & c, Z3_ast a) {
1982  assert(Z3_get_ast_kind(c, a) == Z3_FUNC_DECL_AST);
1983  return func_decl(c, reinterpret_cast<Z3_func_decl>(a));
1984  }
1985  };
1986 
1987  template<typename T>
1988  template<typename T2>
1990  m_array = new T[v.size()];
1991  m_size = v.size();
1992  for (unsigned i = 0; i < m_size; i++) {
1993  m_array[i] = v[i];
1994  }
1995  }
1996 
1997  // Basic functions for creating quantified formulas.
1998  // The C API should be used for creating quantifiers with patterns, weights, many variables, etc.
1999  inline expr forall(expr const & x, expr const & b) {
2000  check_context(x, b);
2001  Z3_app vars[] = {(Z3_app) x};
2002  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2003  }
2004  inline expr forall(expr const & x1, expr const & x2, expr const & b) {
2005  check_context(x1, b); check_context(x2, b);
2006  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2007  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2008  }
2009  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
2010  check_context(x1, b); check_context(x2, b); check_context(x3, b);
2011  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2012  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2013  }
2014  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
2015  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2016  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2017  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2018  }
2019  inline expr forall(expr_vector const & xs, expr const & b) {
2020  array<Z3_app> vars(xs);
2021  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);
2022  }
2023  inline expr exists(expr const & x, expr const & b) {
2024  check_context(x, b);
2025  Z3_app vars[] = {(Z3_app) x};
2026  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2027  }
2028  inline expr exists(expr const & x1, expr const & x2, expr const & b) {
2029  check_context(x1, b); check_context(x2, b);
2030  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2031  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2032  }
2033  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
2034  check_context(x1, b); check_context(x2, b); check_context(x3, b);
2035  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2036  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2037  }
2038  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
2039  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2040  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2041  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2042  }
2043  inline expr exists(expr_vector const & xs, expr const & b) {
2044  array<Z3_app> vars(xs);
2045  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);
2046  }
2047  inline expr lambda(expr const & x, expr const & b) {
2048  check_context(x, b);
2049  Z3_app vars[] = {(Z3_app) x};
2050  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 1, vars, b); b.check_error(); return expr(b.ctx(), r);
2051  }
2052  inline expr lambda(expr const & x1, expr const & x2, expr const & b) {
2053  check_context(x1, b); check_context(x2, b);
2054  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2055  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 2, vars, b); b.check_error(); return expr(b.ctx(), r);
2056  }
2057  inline expr lambda(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
2058  check_context(x1, b); check_context(x2, b); check_context(x3, b);
2059  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2060  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 3, vars, b); b.check_error(); return expr(b.ctx(), r);
2061  }
2062  inline expr lambda(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
2063  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2064  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2065  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 4, vars, b); b.check_error(); return expr(b.ctx(), r);
2066  }
2067  inline expr lambda(expr_vector const & xs, expr const & b) {
2068  array<Z3_app> vars(xs);
2069  Z3_ast r = Z3_mk_lambda_const(b.ctx(), vars.size(), vars.ptr(), b); b.check_error(); return expr(b.ctx(), r);
2070  }
2071 
2072  inline expr pble(expr_vector const& es, int const* coeffs, int bound) {
2073  assert(es.size() > 0);
2074  context& ctx = es[0].ctx();
2075  array<Z3_ast> _es(es);
2076  Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
2077  ctx.check_error();
2078  return expr(ctx, r);
2079  }
2080  inline expr pbge(expr_vector const& es, int const* coeffs, int bound) {
2081  assert(es.size() > 0);
2082  context& ctx = es[0].ctx();
2083  array<Z3_ast> _es(es);
2084  Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
2085  ctx.check_error();
2086  return expr(ctx, r);
2087  }
2088  inline expr pbeq(expr_vector const& es, int const* coeffs, int bound) {
2089  assert(es.size() > 0);
2090  context& ctx = es[0].ctx();
2091  array<Z3_ast> _es(es);
2092  Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
2093  ctx.check_error();
2094  return expr(ctx, r);
2095  }
2096  inline expr atmost(expr_vector const& es, unsigned bound) {
2097  assert(es.size() > 0);
2098  context& ctx = es[0].ctx();
2099  array<Z3_ast> _es(es);
2100  Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
2101  ctx.check_error();
2102  return expr(ctx, r);
2103  }
2104  inline expr atleast(expr_vector const& es, unsigned bound) {
2105  assert(es.size() > 0);
2106  context& ctx = es[0].ctx();
2107  array<Z3_ast> _es(es);
2108  Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
2109  ctx.check_error();
2110  return expr(ctx, r);
2111  }
2112  inline expr sum(expr_vector const& args) {
2113  assert(args.size() > 0);
2114  context& ctx = args[0].ctx();
2115  array<Z3_ast> _args(args);
2116  Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
2117  ctx.check_error();
2118  return expr(ctx, r);
2119  }
2120 
2121  inline expr distinct(expr_vector const& args) {
2122  assert(args.size() > 0);
2123  context& ctx = args[0].ctx();
2124  array<Z3_ast> _args(args);
2125  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
2126  ctx.check_error();
2127  return expr(ctx, r);
2128  }
2129 
2130  inline expr concat(expr const& a, expr const& b) {
2131  check_context(a, b);
2132  Z3_ast r;
2133  if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
2134  Z3_ast _args[2] = { a, b };
2135  r = Z3_mk_seq_concat(a.ctx(), 2, _args);
2136  }
2137  else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
2138  Z3_ast _args[2] = { a, b };
2139  r = Z3_mk_re_concat(a.ctx(), 2, _args);
2140  }
2141  else {
2142  r = Z3_mk_concat(a.ctx(), a, b);
2143  }
2144  a.ctx().check_error();
2145  return expr(a.ctx(), r);
2146  }
2147 
2148  inline expr concat(expr_vector const& args) {
2149  Z3_ast r;
2150  assert(args.size() > 0);
2151  if (args.size() == 1) {
2152  return args[0];
2153  }
2154  context& ctx = args[0].ctx();
2155  array<Z3_ast> _args(args);
2156  if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
2157  r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
2158  }
2159  else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
2160  r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
2161  }
2162  else {
2163  r = _args[args.size()-1];
2164  for (unsigned i = args.size()-1; i > 0; ) {
2165  --i;
2166  r = Z3_mk_concat(ctx, _args[i], r);
2167  ctx.check_error();
2168  }
2169  }
2170  ctx.check_error();
2171  return expr(ctx, r);
2172  }
2173 
2174  inline expr mk_or(expr_vector const& args) {
2175  array<Z3_ast> _args(args);
2176  Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2177  args.check_error();
2178  return expr(args.ctx(), r);
2179  }
2180  inline expr mk_and(expr_vector const& args) {
2181  array<Z3_ast> _args(args);
2182  Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2183  args.check_error();
2184  return expr(args.ctx(), r);
2185  }
2186 
2187 
2188  class func_entry : public object {
2189  Z3_func_entry m_entry;
2190  void init(Z3_func_entry e) {
2191  m_entry = e;
2192  Z3_func_entry_inc_ref(ctx(), m_entry);
2193  }
2194  public:
2195  func_entry(context & c, Z3_func_entry e):object(c) { init(e); }
2196  func_entry(func_entry const & s):object(s) { init(s.m_entry); }
2198  operator Z3_func_entry() const { return m_entry; }
2200  Z3_func_entry_inc_ref(s.ctx(), s.m_entry);
2201  Z3_func_entry_dec_ref(ctx(), m_entry);
2202  m_ctx = s.m_ctx;
2203  m_entry = s.m_entry;
2204  return *this;
2205  }
2206  expr value() const { Z3_ast r = Z3_func_entry_get_value(ctx(), m_entry); check_error(); return expr(ctx(), r); }
2207  unsigned num_args() const { unsigned r = Z3_func_entry_get_num_args(ctx(), m_entry); check_error(); return r; }
2208  expr arg(unsigned i) const { Z3_ast r = Z3_func_entry_get_arg(ctx(), m_entry, i); check_error(); return expr(ctx(), r); }
2209  };
2210 
2211  class func_interp : public object {
2212  Z3_func_interp m_interp;
2213  void init(Z3_func_interp e) {
2214  m_interp = e;
2215  Z3_func_interp_inc_ref(ctx(), m_interp);
2216  }
2217  public:
2218  func_interp(context & c, Z3_func_interp e):object(c) { init(e); }
2219  func_interp(func_interp const & s):object(s) { init(s.m_interp); }
2221  operator Z3_func_interp() const { return m_interp; }
2223  Z3_func_interp_inc_ref(s.ctx(), s.m_interp);
2224  Z3_func_interp_dec_ref(ctx(), m_interp);
2225  m_ctx = s.m_ctx;
2226  m_interp = s.m_interp;
2227  return *this;
2228  }
2229  expr else_value() const { Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), r); }
2230  unsigned num_entries() const { unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }
2231  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); }
2232  void add_entry(expr_vector const& args, expr& value) {
2233  Z3_func_interp_add_entry(ctx(), m_interp, args, value);
2234  check_error();
2235  }
2236  void set_else(expr& value) {
2237  Z3_func_interp_set_else(ctx(), m_interp, value);
2238  check_error();
2239  }
2240  };
2241 
2242  class model : public object {
2243  Z3_model m_model;
2244  void init(Z3_model m) {
2245  m_model = m;
2246  Z3_model_inc_ref(ctx(), m);
2247  }
2248  public:
2249  struct translate {};
2250  model(context & c):object(c) { init(Z3_mk_model(c)); }
2251  model(context & c, Z3_model m):object(c) { init(m); }
2252  model(model const & s):object(s) { init(s.m_model); }
2253  model(model& src, context& dst, translate) : object(dst) { init(Z3_model_translate(src.ctx(), src, dst)); }
2254  ~model() { Z3_model_dec_ref(ctx(), m_model); }
2255  operator Z3_model() const { return m_model; }
2256  model & operator=(model const & s) {
2257  Z3_model_inc_ref(s.ctx(), s.m_model);
2258  Z3_model_dec_ref(ctx(), m_model);
2259  m_ctx = s.m_ctx;
2260  m_model = s.m_model;
2261  return *this;
2262  }
2263 
2264  expr eval(expr const & n, bool model_completion=false) const {
2265  check_context(*this, n);
2266  Z3_ast r = 0;
2267  bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
2268  check_error();
2269  if (status == false && ctx().enable_exceptions())
2270  Z3_THROW(exception("failed to evaluate expression"));
2271  return expr(ctx(), r);
2272  }
2273 
2274  unsigned num_consts() const { return Z3_model_get_num_consts(ctx(), m_model); }
2275  unsigned num_funcs() const { return Z3_model_get_num_funcs(ctx(), m_model); }
2276  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); }
2277  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); }
2278  unsigned size() const { return num_consts() + num_funcs(); }
2279  func_decl operator[](int i) const {
2280  assert(0 <= i);
2281  return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
2282  }
2283 
2284  // returns interpretation of constant declaration c.
2285  // If c is not assigned any value in the model it returns
2286  // an expression with a null ast reference.
2288  check_context(*this, c);
2289  Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);
2290  check_error();
2291  return expr(ctx(), r);
2292  }
2294  check_context(*this, f);
2295  Z3_func_interp r = Z3_model_get_func_interp(ctx(), m_model, f);
2296  check_error();
2297  return func_interp(ctx(), r);
2298  }
2299 
2300  // returns true iff the model contains an interpretation
2301  // for function f.
2302  bool has_interp(func_decl f) const {
2303  check_context(*this, f);
2304  return Z3_model_has_interp(ctx(), m_model, f);
2305  }
2306 
2308  Z3_func_interp r = Z3_add_func_interp(ctx(), m_model, f, else_val);
2309  check_error();
2310  return func_interp(ctx(), r);
2311  }
2312 
2313  void add_const_interp(func_decl& f, expr& value) {
2314  Z3_add_const_interp(ctx(), m_model, f, value);
2315  check_error();
2316  }
2317 
2318  friend std::ostream & operator<<(std::ostream & out, model const & m);
2319 
2320  std::string to_string() const { return std::string(Z3_model_to_string(ctx(), m_model)); }
2321  };
2322  inline std::ostream & operator<<(std::ostream & out, model const & m) { out << Z3_model_to_string(m.ctx(), m); return out; }
2323 
2324  class stats : public object {
2325  Z3_stats m_stats;
2326  void init(Z3_stats e) {
2327  m_stats = e;
2328  Z3_stats_inc_ref(ctx(), m_stats);
2329  }
2330  public:
2331  stats(context & c):object(c), m_stats(0) {}
2332  stats(context & c, Z3_stats e):object(c) { init(e); }
2333  stats(stats const & s):object(s) { init(s.m_stats); }
2334  ~stats() { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); }
2335  operator Z3_stats() const { return m_stats; }
2336  stats & operator=(stats const & s) {
2337  Z3_stats_inc_ref(s.ctx(), s.m_stats);
2338  if (m_stats) Z3_stats_dec_ref(ctx(), m_stats);
2339  m_ctx = s.m_ctx;
2340  m_stats = s.m_stats;
2341  return *this;
2342  }
2343  unsigned size() const { return Z3_stats_size(ctx(), m_stats); }
2344  std::string key(unsigned i) const { Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; }
2345  bool is_uint(unsigned i) const { bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r; }
2346  bool is_double(unsigned i) const { bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r; }
2347  unsigned uint_value(unsigned i) const { unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; }
2348  double double_value(unsigned i) const { double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
2349  friend std::ostream & operator<<(std::ostream & out, stats const & s);
2350  };
2351  inline std::ostream & operator<<(std::ostream & out, stats const & s) { out << Z3_stats_to_string(s.ctx(), s); return out; }
2352 
2353 
2354  inline std::ostream & operator<<(std::ostream & out, check_result r) {
2355  if (r == unsat) out << "unsat";
2356  else if (r == sat) out << "sat";
2357  else out << "unknown";
2358  return out;
2359  }
2360 
2361 
2362  class solver : public object {
2363  Z3_solver m_solver;
2364  void init(Z3_solver s) {
2365  m_solver = s;
2366  Z3_solver_inc_ref(ctx(), s);
2367  }
2368  public:
2369  struct simple {};
2370  struct translate {};
2371  solver(context & c):object(c) { init(Z3_mk_solver(c)); }
2373  solver(context & c, Z3_solver s):object(c) { init(s); }
2374  solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); }
2375  solver(context & c, solver const& src, translate): object(c) { init(Z3_solver_translate(src.ctx(), src, c)); }
2376  solver(solver const & s):object(s) { init(s.m_solver); }
2377  ~solver() { Z3_solver_dec_ref(ctx(), m_solver); }
2378  operator Z3_solver() const { return m_solver; }
2379  solver & operator=(solver const & s) {
2380  Z3_solver_inc_ref(s.ctx(), s.m_solver);
2381  Z3_solver_dec_ref(ctx(), m_solver);
2382  m_ctx = s.m_ctx;
2383  m_solver = s.m_solver;
2384  return *this;
2385  }
2386  void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
2387  void set(char const * k, bool v) { params p(ctx()); p.set(k, v); set(p); }
2388  void set(char const * k, unsigned v) { params p(ctx()); p.set(k, v); set(p); }
2389  void set(char const * k, double v) { params p(ctx()); p.set(k, v); set(p); }
2390  void set(char const * k, symbol const & v) { params p(ctx()); p.set(k, v); set(p); }
2391  void set(char const * k, char const* v) { params p(ctx()); p.set(k, v); set(p); }
2392  void push() { Z3_solver_push(ctx(), m_solver); check_error(); }
2393  void pop(unsigned n = 1) { Z3_solver_pop(ctx(), m_solver, n); check_error(); }
2394  void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); }
2395  void add(expr const & e) { assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); }
2396  void add(expr const & e, expr const & p) {
2397  assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
2398  Z3_solver_assert_and_track(ctx(), m_solver, e, p);
2399  check_error();
2400  }
2401  void add(expr const & e, char const * p) {
2402  add(e, ctx().bool_const(p));
2403  }
2404  void add(expr_vector const& v) {
2405  check_context(*this, v);
2406  for (unsigned i = 0; i < v.size(); ++i)
2407  add(v[i]);
2408  }
2409  void from_file(char const* file) { Z3_solver_from_file(ctx(), m_solver, file); ctx().check_parser_error(); }
2410  void from_string(char const* s) { Z3_solver_from_string(ctx(), m_solver, s); ctx().check_parser_error(); }
2411 
2413  check_result check(unsigned n, expr * const assumptions) {
2414  array<Z3_ast> _assumptions(n);
2415  for (unsigned i = 0; i < n; i++) {
2416  check_context(*this, assumptions[i]);
2417  _assumptions[i] = assumptions[i];
2418  }
2419  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
2420  check_error();
2421  return to_check_result(r);
2422  }
2423  check_result check(expr_vector const& assumptions) {
2424  unsigned n = assumptions.size();
2425  array<Z3_ast> _assumptions(n);
2426  for (unsigned i = 0; i < n; i++) {
2427  check_context(*this, assumptions[i]);
2428  _assumptions[i] = assumptions[i];
2429  }
2430  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
2431  check_error();
2432  return to_check_result(r);
2433  }
2434  model get_model() const { Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }
2436  Z3_lbool r = Z3_solver_get_consequences(ctx(), m_solver, assumptions, vars, conseq);
2437  check_error();
2438  return to_check_result(r);
2439  }
2440  std::string reason_unknown() const { Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }
2441  stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }
2442  expr_vector unsat_core() const { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2443  expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2444  expr_vector non_units() const { Z3_ast_vector r = Z3_solver_get_non_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2445  expr_vector units() const { Z3_ast_vector r = Z3_solver_get_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2446  expr_vector trail() const { Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2448  Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver);
2449  check_error();
2450  expr_vector result(ctx(), r);
2451  unsigned sz = result.size();
2452  levels.resize(sz);
2453  Z3_solver_get_levels(ctx(), m_solver, r, sz, levels.ptr());
2454  check_error();
2455  return result;
2456  }
2457  expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
2458  friend std::ostream & operator<<(std::ostream & out, solver const & s);
2459 
2460  std::string to_smt2(char const* status = "unknown") {
2461  array<Z3_ast> es(assertions());
2462  Z3_ast const* fmls = es.ptr();
2463  Z3_ast fml = 0;
2464  unsigned sz = es.size();
2465  if (sz > 0) {
2466  --sz;
2467  fml = fmls[sz];
2468  }
2469  else {
2470  fml = ctx().bool_val(true);
2471  }
2472  return std::string(Z3_benchmark_to_smtlib_string(
2473  ctx(),
2474  "", "", status, "",
2475  sz,
2476  fmls,
2477  fml));
2478  }
2479 
2480  std::string dimacs(bool include_names = true) const { return std::string(Z3_solver_to_dimacs_string(ctx(), m_solver, include_names)); }
2481 
2483 
2484 
2485  expr_vector cube(expr_vector& vars, unsigned cutoff) {
2486  Z3_ast_vector r = Z3_solver_cube(ctx(), m_solver, vars, cutoff);
2487  check_error();
2488  return expr_vector(ctx(), r);
2489  }
2490 
2492  solver& m_solver;
2493  unsigned& m_cutoff;
2494  expr_vector& m_vars;
2495  expr_vector m_cube;
2496  bool m_end;
2497  bool m_empty;
2498 
2499  void inc() {
2500  assert(!m_end && !m_empty);
2501  m_cube = m_solver.cube(m_vars, m_cutoff);
2502  m_cutoff = 0xFFFFFFFF;
2503  if (m_cube.size() == 1 && m_cube[0].is_false()) {
2504  m_cube = z3::expr_vector(m_solver.ctx());
2505  m_end = true;
2506  }
2507  else if (m_cube.empty()) {
2508  m_empty = true;
2509  }
2510  }
2511  public:
2512  cube_iterator(solver& s, expr_vector& vars, unsigned& cutoff, bool end):
2513  m_solver(s),
2514  m_cutoff(cutoff),
2515  m_vars(vars),
2516  m_cube(s.ctx()),
2517  m_end(end),
2518  m_empty(false) {
2519  if (!m_end) {
2520  inc();
2521  }
2522  }
2523 
2525  assert(!m_end);
2526  if (m_empty) {
2527  m_end = true;
2528  }
2529  else {
2530  inc();
2531  }
2532  return *this;
2533  }
2534  cube_iterator operator++(int) { assert(false); return *this; }
2535  expr_vector const * operator->() const { return &(operator*()); }
2536  expr_vector const& operator*() const { return m_cube; }
2537 
2538  bool operator==(cube_iterator const& other) {
2539  return other.m_end == m_end;
2540  };
2541  bool operator!=(cube_iterator const& other) {
2542  return other.m_end != m_end;
2543  };
2544 
2545  };
2546 
2548  solver& m_solver;
2549  unsigned m_cutoff;
2550  expr_vector m_default_vars;
2551  expr_vector& m_vars;
2552  public:
2554  m_solver(s),
2555  m_cutoff(0xFFFFFFFF),
2556  m_default_vars(s.ctx()),
2557  m_vars(m_default_vars)
2558  {}
2559 
2561  m_solver(s),
2562  m_cutoff(0xFFFFFFFF),
2563  m_default_vars(s.ctx()),
2564  m_vars(vars)
2565  {}
2566 
2567  cube_iterator begin() { return cube_iterator(m_solver, m_vars, m_cutoff, false); }
2568  cube_iterator end() { return cube_iterator(m_solver, m_vars, m_cutoff, true); }
2569  void set_cutoff(unsigned c) { m_cutoff = c; }
2570  };
2571 
2572  cube_generator cubes() { return cube_generator(*this); }
2573  cube_generator cubes(expr_vector& vars) { return cube_generator(*this, vars); }
2574 
2575  };
2576  inline std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
2577 
2578  class goal : public object {
2579  Z3_goal m_goal;
2580  void init(Z3_goal s) {
2581  m_goal = s;
2582  Z3_goal_inc_ref(ctx(), s);
2583  }
2584  public:
2585  goal(context & c, bool models=true, bool unsat_cores=false, bool proofs=false):object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); }
2586  goal(context & c, Z3_goal s):object(c) { init(s); }
2587  goal(goal const & s):object(s) { init(s.m_goal); }
2588  ~goal() { Z3_goal_dec_ref(ctx(), m_goal); }
2589  operator Z3_goal() const { return m_goal; }
2590  goal & operator=(goal const & s) {
2591  Z3_goal_inc_ref(s.ctx(), s.m_goal);
2592  Z3_goal_dec_ref(ctx(), m_goal);
2593  m_ctx = s.m_ctx;
2594  m_goal = s.m_goal;
2595  return *this;
2596  }
2597  void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
2598  void add(expr_vector const& v) { check_context(*this, v); for (unsigned i = 0; i < v.size(); ++i) add(v[i]); }
2599  unsigned size() const { return Z3_goal_size(ctx(), m_goal); }
2600  expr operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
2601  Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); }
2602  bool inconsistent() const { return Z3_goal_inconsistent(ctx(), m_goal); }
2603  unsigned depth() const { return Z3_goal_depth(ctx(), m_goal); }
2604  void reset() { Z3_goal_reset(ctx(), m_goal); }
2605  unsigned num_exprs() const { return Z3_goal_num_exprs(ctx(), m_goal); }
2606  bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal); }
2607  bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal); }
2608  model convert_model(model const & m) const {
2609  check_context(*this, m);
2610  Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, m);
2611  check_error();
2612  return model(ctx(), new_m);
2613  }
2614  model get_model() const {
2615  Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, 0);
2616  check_error();
2617  return model(ctx(), new_m);
2618  }
2619  expr as_expr() const {
2620  unsigned n = size();
2621  if (n == 0)
2622  return ctx().bool_val(true);
2623  else if (n == 1)
2624  return operator[](0);
2625  else {
2626  array<Z3_ast> args(n);
2627  for (unsigned i = 0; i < n; i++)
2628  args[i] = operator[](i);
2629  return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
2630  }
2631  }
2632  std::string dimacs(bool include_names = true) const { return std::string(Z3_goal_to_dimacs_string(ctx(), m_goal, include_names)); }
2633  friend std::ostream & operator<<(std::ostream & out, goal const & g);
2634  };
2635  inline std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; }
2636 
2637  class apply_result : public object {
2638  Z3_apply_result m_apply_result;
2639  void init(Z3_apply_result s) {
2640  m_apply_result = s;
2642  }
2643  public:
2644  apply_result(context & c, Z3_apply_result s):object(c) { init(s); }
2645  apply_result(apply_result const & s):object(s) { init(s.m_apply_result); }
2646  ~apply_result() { Z3_apply_result_dec_ref(ctx(), m_apply_result); }
2647  operator Z3_apply_result() const { return m_apply_result; }
2649  Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result);
2650  Z3_apply_result_dec_ref(ctx(), m_apply_result);
2651  m_ctx = s.m_ctx;
2652  m_apply_result = s.m_apply_result;
2653  return *this;
2654  }
2655  unsigned size() const { return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }
2656  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); }
2657  friend std::ostream & operator<<(std::ostream & out, apply_result const & r);
2658  };
2659  inline std::ostream & operator<<(std::ostream & out, apply_result const & r) { out << Z3_apply_result_to_string(r.ctx(), r); return out; }
2660 
2661  class tactic : public object {
2662  Z3_tactic m_tactic;
2663  void init(Z3_tactic s) {
2664  m_tactic = s;
2665  Z3_tactic_inc_ref(ctx(), s);
2666  }
2667  public:
2668  tactic(context & c, char const * name):object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); }
2669  tactic(context & c, Z3_tactic s):object(c) { init(s); }
2670  tactic(tactic const & s):object(s) { init(s.m_tactic); }
2671  ~tactic() { Z3_tactic_dec_ref(ctx(), m_tactic); }
2672  operator Z3_tactic() const { return m_tactic; }
2673  tactic & operator=(tactic const & s) {
2674  Z3_tactic_inc_ref(s.ctx(), s.m_tactic);
2675  Z3_tactic_dec_ref(ctx(), m_tactic);
2676  m_ctx = s.m_ctx;
2677  m_tactic = s.m_tactic;
2678  return *this;
2679  }
2680  solver mk_solver() const { Z3_solver r = Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error(); return solver(ctx(), r); }
2681  apply_result apply(goal const & g) const {
2682  check_context(*this, g);
2683  Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g);
2684  check_error();
2685  return apply_result(ctx(), r);
2686  }
2687  apply_result operator()(goal const & g) const {
2688  return apply(g);
2689  }
2690  std::string help() const { char const * r = Z3_tactic_get_help(ctx(), m_tactic); check_error(); return r; }
2691  friend tactic operator&(tactic const & t1, tactic const & t2);
2692  friend tactic operator|(tactic const & t1, tactic const & t2);
2693  friend tactic repeat(tactic const & t, unsigned max);
2694  friend tactic with(tactic const & t, params const & p);
2695  friend tactic try_for(tactic const & t, unsigned ms);
2696  friend tactic par_or(unsigned n, tactic const* tactics);
2697  friend tactic par_and_then(tactic const& t1, tactic const& t2);
2699  };
2700 
2701  inline tactic operator&(tactic const & t1, tactic const & t2) {
2702  check_context(t1, t2);
2703  Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
2704  t1.check_error();
2705  return tactic(t1.ctx(), r);
2706  }
2707 
2708  inline tactic operator|(tactic const & t1, tactic const & t2) {
2709  check_context(t1, t2);
2710  Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
2711  t1.check_error();
2712  return tactic(t1.ctx(), r);
2713  }
2714 
2715  inline tactic repeat(tactic const & t, unsigned max=UINT_MAX) {
2716  Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
2717  t.check_error();
2718  return tactic(t.ctx(), r);
2719  }
2720 
2721  inline tactic with(tactic const & t, params const & p) {
2722  Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
2723  t.check_error();
2724  return tactic(t.ctx(), r);
2725  }
2726  inline tactic try_for(tactic const & t, unsigned ms) {
2727  Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
2728  t.check_error();
2729  return tactic(t.ctx(), r);
2730  }
2731  inline tactic par_or(unsigned n, tactic const* tactics) {
2732  if (n == 0) {
2733  Z3_THROW(exception("a non-zero number of tactics need to be passed to par_or"));
2734  }
2735  array<Z3_tactic> buffer(n);
2736  for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
2737  return tactic(tactics[0].ctx(), Z3_tactic_par_or(tactics[0].ctx(), n, buffer.ptr()));
2738  }
2739 
2740  inline tactic par_and_then(tactic const & t1, tactic const & t2) {
2741  check_context(t1, t2);
2742  Z3_tactic r = Z3_tactic_par_and_then(t1.ctx(), t1, t2);
2743  t1.check_error();
2744  return tactic(t1.ctx(), r);
2745  }
2746 
2747  class probe : public object {
2748  Z3_probe m_probe;
2749  void init(Z3_probe s) {
2750  m_probe = s;
2751  Z3_probe_inc_ref(ctx(), s);
2752  }
2753  public:
2754  probe(context & c, char const * name):object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); }
2755  probe(context & c, double val):object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); }
2756  probe(context & c, Z3_probe s):object(c) { init(s); }
2757  probe(probe const & s):object(s) { init(s.m_probe); }
2758  ~probe() { Z3_probe_dec_ref(ctx(), m_probe); }
2759  operator Z3_probe() const { return m_probe; }
2760  probe & operator=(probe const & s) {
2761  Z3_probe_inc_ref(s.ctx(), s.m_probe);
2762  Z3_probe_dec_ref(ctx(), m_probe);
2763  m_ctx = s.m_ctx;
2764  m_probe = s.m_probe;
2765  return *this;
2766  }
2767  double apply(goal const & g) const { double r = Z3_probe_apply(ctx(), m_probe, g); check_error(); return r; }
2768  double operator()(goal const & g) const { return apply(g); }
2769  friend probe operator<=(probe const & p1, probe const & p2);
2770  friend probe operator<=(probe const & p1, double p2);
2771  friend probe operator<=(double p1, probe const & p2);
2772  friend probe operator>=(probe const & p1, probe const & p2);
2773  friend probe operator>=(probe const & p1, double p2);
2774  friend probe operator>=(double p1, probe const & p2);
2775  friend probe operator<(probe const & p1, probe const & p2);
2776  friend probe operator<(probe const & p1, double p2);
2777  friend probe operator<(double p1, probe const & p2);
2778  friend probe operator>(probe const & p1, probe const & p2);
2779  friend probe operator>(probe const & p1, double p2);
2780  friend probe operator>(double p1, probe const & p2);
2781  friend probe operator==(probe const & p1, probe const & p2);
2782  friend probe operator==(probe const & p1, double p2);
2783  friend probe operator==(double p1, probe const & p2);
2784  friend probe operator&&(probe const & p1, probe const & p2);
2785  friend probe operator||(probe const & p1, probe const & p2);
2786  friend probe operator!(probe const & p);
2787  };
2788 
2789  inline probe operator<=(probe const & p1, probe const & p2) {
2790  check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2791  }
2792  inline probe operator<=(probe const & p1, double p2) { return p1 <= probe(p1.ctx(), p2); }
2793  inline probe operator<=(double p1, probe const & p2) { return probe(p2.ctx(), p1) <= p2; }
2794  inline probe operator>=(probe const & p1, probe const & p2) {
2795  check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2796  }
2797  inline probe operator>=(probe const & p1, double p2) { return p1 >= probe(p1.ctx(), p2); }
2798  inline probe operator>=(double p1, probe const & p2) { return probe(p2.ctx(), p1) >= p2; }
2799  inline probe operator<(probe const & p1, probe const & p2) {
2800  check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2801  }
2802  inline probe operator<(probe const & p1, double p2) { return p1 < probe(p1.ctx(), p2); }
2803  inline probe operator<(double p1, probe const & p2) { return probe(p2.ctx(), p1) < p2; }
2804  inline probe operator>(probe const & p1, probe const & p2) {
2805  check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2806  }
2807  inline probe operator>(probe const & p1, double p2) { return p1 > probe(p1.ctx(), p2); }
2808  inline probe operator>(double p1, probe const & p2) { return probe(p2.ctx(), p1) > p2; }
2809  inline probe operator==(probe const & p1, probe const & p2) {
2810  check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2811  }
2812  inline probe operator==(probe const & p1, double p2) { return p1 == probe(p1.ctx(), p2); }
2813  inline probe operator==(double p1, probe const & p2) { return probe(p2.ctx(), p1) == p2; }
2814  inline probe operator&&(probe const & p1, probe const & p2) {
2815  check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2816  }
2817  inline probe operator||(probe const & p1, probe const & p2) {
2818  check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2819  }
2820  inline probe operator!(probe const & p) {
2821  Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
2822  }
2823 
2824  class optimize : public object {
2825  Z3_optimize m_opt;
2826 
2827  public:
2828  class handle {
2829  unsigned m_h;
2830  public:
2831  handle(unsigned h): m_h(h) {}
2832  unsigned h() const { return m_h; }
2833  };
2834  optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }
2836  Z3_optimize_inc_ref(o.ctx(), o.m_opt);
2837  m_opt = o.m_opt;
2838  }
2840  m_opt = Z3_mk_optimize(c);
2841  Z3_optimize_inc_ref(c, m_opt);
2842  add(expr_vector(c, src.assertions()));
2843  expr_vector v(c, src.objectives());
2844  for (expr_vector::iterator it = v.begin(); it != v.end(); ++it) minimize(*it);
2845  }
2847  Z3_optimize_inc_ref(o.ctx(), o.m_opt);
2848  Z3_optimize_dec_ref(ctx(), m_opt);
2849  m_opt = o.m_opt;
2850  m_ctx = o.m_ctx;
2851  return *this;
2852  }
2854  operator Z3_optimize() const { return m_opt; }
2855  void add(expr const& e) {
2856  assert(e.is_bool());
2857  Z3_optimize_assert(ctx(), m_opt, e);
2858  }
2859  void add(expr_vector const& es) {
2860  for (expr_vector::iterator it = es.begin(); it != es.end(); ++it) add(*it);
2861  }
2862  void add(expr const& e, expr const& t) {
2863  assert(e.is_bool());
2864  Z3_optimize_assert_and_track(ctx(), m_opt, e, t);
2865  }
2866  void add(expr const& e, char const* p) {
2867  assert(e.is_bool());
2868  add(e, ctx().bool_const(p));
2869  }
2870  handle add_soft(expr const& e, unsigned weight) {
2871  assert(e.is_bool());
2872  auto str = std::to_string(weight);
2873  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, str.c_str(), 0));
2874  }
2875  handle add_soft(expr const& e, char const* weight) {
2876  assert(e.is_bool());
2877  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0));
2878  }
2879  handle add(expr const& e, unsigned weight) {
2880  return add_soft(e, weight);
2881  }
2882  handle maximize(expr const& e) {
2883  return handle(Z3_optimize_maximize(ctx(), m_opt, e));
2884  }
2885  handle minimize(expr const& e) {
2886  return handle(Z3_optimize_minimize(ctx(), m_opt, e));
2887  }
2888  void push() {
2889  Z3_optimize_push(ctx(), m_opt);
2890  }
2891  void pop() {
2892  Z3_optimize_pop(ctx(), m_opt);
2893  }
2896  unsigned n = asms.size();
2897  array<Z3_ast> _asms(n);
2898  for (unsigned i = 0; i < n; i++) {
2899  check_context(*this, asms[i]);
2900  _asms[i] = asms[i];
2901  }
2902  Z3_lbool r = Z3_optimize_check(ctx(), m_opt, n, _asms.ptr());
2903  check_error();
2904  return to_check_result(r);
2905  }
2906  model get_model() const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }
2907  expr_vector unsat_core() const { Z3_ast_vector r = Z3_optimize_get_unsat_core(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
2908  void set(params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }
2909  expr lower(handle const& h) {
2910  Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());
2911  check_error();
2912  return expr(ctx(), r);
2913  }
2914  expr upper(handle const& h) {
2915  Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h());
2916  check_error();
2917  return expr(ctx(), r);
2918  }
2919  expr_vector assertions() const { Z3_ast_vector r = Z3_optimize_get_assertions(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
2920  expr_vector objectives() const { Z3_ast_vector r = Z3_optimize_get_objectives(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
2921  stats statistics() const { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); }
2922  friend std::ostream & operator<<(std::ostream & out, optimize const & s);
2923  void from_file(char const* filename) { Z3_optimize_from_file(ctx(), m_opt, filename); check_error(); }
2924  void from_string(char const* constraints) { Z3_optimize_from_string(ctx(), m_opt, constraints); check_error(); }
2925  std::string help() const { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error(); return r; }
2926  };
2927  inline std::ostream & operator<<(std::ostream & out, optimize const & s) { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }
2928 
2929  class fixedpoint : public object {
2930  Z3_fixedpoint m_fp;
2931  public:
2934  operator Z3_fixedpoint() const { return m_fp; }
2935  void from_string(char const* s) { Z3_fixedpoint_from_string(ctx(), m_fp, s); check_error(); }
2936  void from_file(char const* s) { Z3_fixedpoint_from_file(ctx(), m_fp, s); check_error(); }
2937  void add_rule(expr& rule, symbol const& name) { Z3_fixedpoint_add_rule(ctx(), m_fp, rule, name); check_error(); }
2938  void add_fact(func_decl& f, unsigned * args) { Z3_fixedpoint_add_fact(ctx(), m_fp, f, f.arity(), args); check_error(); }
2941  array<Z3_func_decl> rs(relations);
2942  Z3_lbool r = Z3_fixedpoint_query_relations(ctx(), m_fp, rs.size(), rs.ptr());
2943  check_error();
2944  return to_check_result(r);
2945  }
2946  expr get_answer() { Z3_ast r = Z3_fixedpoint_get_answer(ctx(), m_fp); check_error(); return expr(ctx(), r); }
2947  std::string reason_unknown() { return Z3_fixedpoint_get_reason_unknown(ctx(), m_fp); }
2948  void update_rule(expr& rule, symbol const& name) { Z3_fixedpoint_update_rule(ctx(), m_fp, rule, name); check_error(); }
2949  unsigned get_num_levels(func_decl& p) { unsigned r = Z3_fixedpoint_get_num_levels(ctx(), m_fp, p); check_error(); return r; }
2950  expr get_cover_delta(int level, func_decl& p) {
2951  Z3_ast r = Z3_fixedpoint_get_cover_delta(ctx(), m_fp, level, p);
2952  check_error();
2953  return expr(ctx(), r);
2954  }
2955  void add_cover(int level, func_decl& p, expr& property) { Z3_fixedpoint_add_cover(ctx(), m_fp, level, p, property); check_error(); }
2956  stats statistics() const { Z3_stats r = Z3_fixedpoint_get_statistics(ctx(), m_fp); check_error(); return stats(ctx(), r); }
2958  expr_vector assertions() const { Z3_ast_vector r = Z3_fixedpoint_get_assertions(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
2959  expr_vector rules() const { Z3_ast_vector r = Z3_fixedpoint_get_rules(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
2960  void set(params const & p) { Z3_fixedpoint_set_params(ctx(), m_fp, p); check_error(); }
2961  std::string help() const { return Z3_fixedpoint_get_help(ctx(), m_fp); }
2963  std::string to_string() { return Z3_fixedpoint_to_string(ctx(), m_fp, 0, 0); }
2964  std::string to_string(expr_vector const& queries) {
2965  array<Z3_ast> qs(queries);
2966  return Z3_fixedpoint_to_string(ctx(), m_fp, qs.size(), qs.ptr());
2967  }
2968  };
2969  inline std::ostream & operator<<(std::ostream & out, fixedpoint const & f) { return out << Z3_fixedpoint_to_string(f.ctx(), f, 0, 0); }
2970 
2971  inline tactic fail_if(probe const & p) {
2972  Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
2973  p.check_error();
2974  return tactic(p.ctx(), r);
2975  }
2976  inline tactic when(probe const & p, tactic const & t) {
2977  check_context(p, t);
2978  Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
2979  t.check_error();
2980  return tactic(t.ctx(), r);
2981  }
2982  inline tactic cond(probe const & p, tactic const & t1, tactic const & t2) {
2983  check_context(p, t1); check_context(p, t2);
2984  Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
2985  t1.check_error();
2986  return tactic(t1.ctx(), r);
2987  }
2988 
2989  inline symbol context::str_symbol(char const * s) { Z3_symbol r = Z3_mk_string_symbol(m_ctx, s); check_error(); return symbol(*this, r); }
2990  inline symbol context::int_symbol(int n) { Z3_symbol r = Z3_mk_int_symbol(m_ctx, n); check_error(); return symbol(*this, r); }
2991 
2992  inline sort context::bool_sort() { Z3_sort s = Z3_mk_bool_sort(m_ctx); check_error(); return sort(*this, s); }
2993  inline sort context::int_sort() { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }
2994  inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
2995  inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
2996  inline sort context::string_sort() { Z3_sort s = Z3_mk_string_sort(m_ctx); check_error(); return sort(*this, s); }
2997  inline sort context::seq_sort(sort& s) { Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); }
2998  inline sort context::re_sort(sort& s) { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
2999  inline sort context::fpa_sort(unsigned ebits, unsigned sbits) { Z3_sort s = Z3_mk_fpa_sort(m_ctx, ebits, sbits); check_error(); return sort(*this, s); }
3000 
3001  template<>
3002  inline sort context::fpa_sort<16>() { return fpa_sort(5, 11); }
3003 
3004  template<>
3005  inline sort context::fpa_sort<32>() { return fpa_sort(8, 24); }
3006 
3007  template<>
3008  inline sort context::fpa_sort<64>() { return fpa_sort(11, 53); }
3009 
3010  template<>
3011  inline sort context::fpa_sort<128>() { return fpa_sort(15, 113); }
3012 
3014  switch (m_rounding_mode) {
3015  case RNA: return sort(*this, Z3_mk_fpa_rna(m_ctx));
3016  case RNE: return sort(*this, Z3_mk_fpa_rne(m_ctx));
3017  case RTP: return sort(*this, Z3_mk_fpa_rtp(m_ctx));
3018  case RTN: return sort(*this, Z3_mk_fpa_rtn(m_ctx));
3019  case RTZ: return sort(*this, Z3_mk_fpa_rtz(m_ctx));
3020  default: return sort(*this);
3021  }
3022  }
3023 
3024  inline void context::set_rounding_mode(rounding_mode rm) { m_rounding_mode = rm; }
3025 
3026  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); }
3028  array<Z3_sort> dom(d);
3029  Z3_sort s = Z3_mk_array_sort_n(m_ctx, dom.size(), dom.ptr(), r); check_error(); return sort(*this, s);
3030  }
3031  inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
3032  array<Z3_symbol> _enum_names(n);
3033  for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
3034  array<Z3_func_decl> _cs(n);
3035  array<Z3_func_decl> _ts(n);
3036  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3037  sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
3038  check_error();
3039  for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
3040  return s;
3041  }
3042  inline func_decl context::tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs) {
3043  array<Z3_symbol> _names(n);
3044  array<Z3_sort> _sorts(n);
3045  for (unsigned i = 0; i < n; i++) { _names[i] = Z3_mk_string_symbol(*this, names[i]); _sorts[i] = sorts[i]; }
3046  array<Z3_func_decl> _projs(n);
3047  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3048  Z3_func_decl tuple;
3049  sort _ignore_s = to_sort(*this, Z3_mk_tuple_sort(*this, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));
3050  check_error();
3051  for (unsigned i = 0; i < n; i++) { projs.push_back(func_decl(*this, _projs[i])); }
3052  return func_decl(*this, tuple);
3053  }
3054 
3055  inline sort context::uninterpreted_sort(char const* name) {
3056  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3057  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
3058  }
3060  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
3061  }
3062 
3063  inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3064  array<Z3_sort> args(arity);
3065  for (unsigned i = 0; i < arity; i++) {
3066  check_context(domain[i], range);
3067  args[i] = domain[i];
3068  }
3069  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
3070  check_error();
3071  return func_decl(*this, f);
3072  }
3073 
3074  inline func_decl context::function(char const * name, unsigned arity, sort const * domain, sort const & range) {
3075  return function(range.ctx().str_symbol(name), arity, domain, range);
3076  }
3077 
3078  inline func_decl context::function(symbol const& name, sort_vector const& domain, sort const& range) {
3079  array<Z3_sort> args(domain.size());
3080  for (unsigned i = 0; i < domain.size(); i++) {
3081  check_context(domain[i], range);
3082  args[i] = domain[i];
3083  }
3084  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
3085  check_error();
3086  return func_decl(*this, f);
3087  }
3088 
3089  inline func_decl context::function(char const * name, sort_vector const& domain, sort const& range) {
3090  return function(range.ctx().str_symbol(name), domain, range);
3091  }
3092 
3093 
3094  inline func_decl context::function(char const * name, sort const & domain, sort const & range) {
3095  check_context(domain, range);
3096  Z3_sort args[1] = { domain };
3097  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
3098  check_error();
3099  return func_decl(*this, f);
3100  }
3101 
3102  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & range) {
3104  Z3_sort args[2] = { d1, d2 };
3105  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
3106  check_error();
3107  return func_decl(*this, f);
3108  }
3109 
3110  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
3112  Z3_sort args[3] = { d1, d2, d3 };
3113  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
3114  check_error();
3115  return func_decl(*this, f);
3116  }
3117 
3118  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
3120  Z3_sort args[4] = { d1, d2, d3, d4 };
3121  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
3122  check_error();
3123  return func_decl(*this, f);
3124  }
3125 
3126  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) {
3128  Z3_sort args[5] = { d1, d2, d3, d4, d5 };
3129  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
3130  check_error();
3131  return func_decl(*this, f);
3132  }
3133 
3134  inline func_decl context::recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3135  array<Z3_sort> args(arity);
3136  for (unsigned i = 0; i < arity; i++) {
3137  check_context(domain[i], range);
3138  args[i] = domain[i];
3139  }
3140  Z3_func_decl f = Z3_mk_rec_func_decl(m_ctx, name, arity, args.ptr(), range);
3141  check_error();
3142  return func_decl(*this, f);
3143 
3144  }
3145 
3146  inline func_decl context::recfun(char const * name, unsigned arity, sort const * domain, sort const & range) {
3147  return recfun(str_symbol(name), arity, domain, range);
3148  }
3149 
3150  inline func_decl context::recfun(char const * name, sort const& d1, sort const & range) {
3151  return recfun(str_symbol(name), 1, &d1, range);
3152  }
3153 
3154  inline func_decl context::recfun(char const * name, sort const& d1, sort const& d2, sort const & range) {
3155  sort dom[2] = { d1, d2 };
3156  return recfun(str_symbol(name), 2, dom, range);
3157  }
3158 
3159  inline void context::recdef(func_decl f, expr_vector const& args, expr const& body) {
3160  check_context(f, args); check_context(f, body);
3161  array<Z3_ast> vars(args);
3162  Z3_add_rec_def(f.ctx(), f, vars.size(), vars.ptr(), body);
3163  }
3164 
3165  inline expr context::constant(symbol const & name, sort const & s) {
3166  Z3_ast r = Z3_mk_const(m_ctx, name, s);
3167  check_error();
3168  return expr(*this, r);
3169  }
3170  inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); }
3171  inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); }
3172  inline expr context::int_const(char const * name) { return constant(name, int_sort()); }
3173  inline expr context::real_const(char const * name) { return constant(name, real_sort()); }
3174  inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); }
3175  inline expr context::fpa_const(char const * name, unsigned ebits, unsigned sbits) { return constant(name, fpa_sort(ebits, sbits)); }
3176 
3177  template<size_t precision>
3178  inline expr context::fpa_const(char const * name) { return constant(name, fpa_sort<precision>()); }
3179 
3180  inline expr context::bool_val(bool b) { return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }
3181 
3182  inline expr context::int_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
3183  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); }
3184  inline expr context::int_val(int64_t n) { Z3_ast r = Z3_mk_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
3185  inline expr context::int_val(uint64_t n) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
3186  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); }
3187 
3188  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); }
3189  inline expr context::real_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
3190  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); }
3191  inline expr context::real_val(int64_t n) { Z3_ast r = Z3_mk_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
3192  inline expr context::real_val(uint64_t n) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
3193  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); }
3194 
3195  inline expr context::bv_val(int n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_int(m_ctx, n, s); check_error(); return expr(*this, r); }
3196  inline expr context::bv_val(unsigned n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, s); check_error(); return expr(*this, r); }
3197  inline expr context::bv_val(int64_t n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_int64(m_ctx, n, s); check_error(); return expr(*this, r); }
3198  inline expr context::bv_val(uint64_t n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, s); check_error(); return expr(*this, r); }
3199  inline expr context::bv_val(char const * n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_numeral(m_ctx, n, s); check_error(); return expr(*this, r); }
3200  inline expr context::bv_val(unsigned n, bool const* bits) {
3201  array<bool> _bits(n);
3202  for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
3203  Z3_ast r = Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error(); return expr(*this, r);
3204  }
3205 
3206  inline expr context::fpa_val(double n) { sort s = fpa_sort<64>(); Z3_ast r = Z3_mk_fpa_numeral_double(m_ctx, n, s); check_error(); return expr(*this, r); }
3207  inline expr context::fpa_val(float n) { sort s = fpa_sort<32>(); Z3_ast r = Z3_mk_fpa_numeral_float(m_ctx, n, s); check_error(); return expr(*this, r); }
3208 
3209  inline expr context::string_val(char const* s, unsigned n) { Z3_ast r = Z3_mk_lstring(m_ctx, n, s); check_error(); return expr(*this, r); }
3210  inline expr context::string_val(char const* s) { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
3211  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); }
3212 
3213  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); }
3214 
3215  inline expr func_decl::operator()(unsigned n, expr const * args) const {
3216  array<Z3_ast> _args(n);
3217  for (unsigned i = 0; i < n; i++) {
3218  check_context(*this, args[i]);
3219  _args[i] = args[i];
3220  }
3221  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
3222  check_error();
3223  return expr(ctx(), r);
3224 
3225  }
3226  inline expr func_decl::operator()(expr_vector const& args) const {
3227  array<Z3_ast> _args(args.size());
3228  for (unsigned i = 0; i < args.size(); i++) {
3229  check_context(*this, args[i]);
3230  _args[i] = args[i];
3231  }
3232  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
3233  check_error();
3234  return expr(ctx(), r);
3235  }
3236  inline expr func_decl::operator()() const {
3237  Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
3238  ctx().check_error();
3239  return expr(ctx(), r);
3240  }
3241  inline expr func_decl::operator()(expr const & a) const {
3242  check_context(*this, a);
3243  Z3_ast args[1] = { a };
3244  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3245  ctx().check_error();
3246  return expr(ctx(), r);
3247  }
3248  inline expr func_decl::operator()(int a) const {
3249  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
3250  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3251  ctx().check_error();
3252  return expr(ctx(), r);
3253  }
3254  inline expr func_decl::operator()(expr const & a1, expr const & a2) const {
3255  check_context(*this, a1); check_context(*this, a2);
3256  Z3_ast args[2] = { a1, a2 };
3257  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3258  ctx().check_error();
3259  return expr(ctx(), r);
3260  }
3261  inline expr func_decl::operator()(expr const & a1, int a2) const {
3262  check_context(*this, a1);
3263  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
3264  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3265  ctx().check_error();
3266  return expr(ctx(), r);
3267  }
3268  inline expr func_decl::operator()(int a1, expr const & a2) const {
3269  check_context(*this, a2);
3270  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
3271  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3272  ctx().check_error();
3273  return expr(ctx(), r);
3274  }
3275  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3) const {
3276  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
3277  Z3_ast args[3] = { a1, a2, a3 };
3278  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
3279  ctx().check_error();
3280  return expr(ctx(), r);
3281  }
3282  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const {
3283  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
3284  Z3_ast args[4] = { a1, a2, a3, a4 };
3285  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
3286  ctx().check_error();
3287  return expr(ctx(), r);
3288  }
3289  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const {
3290  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
3291  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
3292  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
3293  ctx().check_error();
3294  return expr(ctx(), r);
3295  }
3296 
3297  inline expr to_real(expr const & a) { Z3_ast r = Z3_mk_int2real(a.ctx(), a); a.check_error(); return expr(a.ctx(), r); }
3298 
3299  inline func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3300  return range.ctx().function(name, arity, domain, range);
3301  }
3302  inline func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range) {
3303  return range.ctx().function(name, arity, domain, range);
3304  }
3305  inline func_decl function(char const * name, sort const & domain, sort const & range) {
3306  return range.ctx().function(name, domain, range);
3307  }
3308  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range) {
3309  return range.ctx().function(name, d1, d2, range);
3310  }
3311  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
3312  return range.ctx().function(name, d1, d2, d3, range);
3313  }
3314  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
3315  return range.ctx().function(name, d1, d2, d3, d4, range);
3316  }
3317  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) {
3318  return range.ctx().function(name, d1, d2, d3, d4, d5, range);
3319  }
3320  inline func_decl function(char const* name, sort_vector const& domain, sort const& range) {
3321  return range.ctx().function(name, domain, range);
3322  }
3323  inline func_decl function(std::string const& name, sort_vector const& domain, sort const& range) {
3324  return range.ctx().function(name.c_str(), domain, range);
3325  }
3326 
3327  inline func_decl recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3328  return range.ctx().recfun(name, arity, domain, range);
3329  }
3330  inline func_decl recfun(char const * name, unsigned arity, sort const * domain, sort const & range) {
3331  return range.ctx().recfun(name, arity, domain, range);
3332  }
3333  inline func_decl recfun(char const * name, sort const& d1, sort const & range) {
3334  return range.ctx().recfun(name, d1, range);
3335  }
3336  inline func_decl recfun(char const * name, sort const& d1, sort const& d2, sort const & range) {
3337  return range.ctx().recfun(name, d1, d2, range);
3338  }
3339 
3340  inline expr select(expr const & a, expr const & i) {
3341  check_context(a, i);
3342  Z3_ast r = Z3_mk_select(a.ctx(), a, i);
3343  a.check_error();
3344  return expr(a.ctx(), r);
3345  }
3346  inline expr select(expr const & a, int i) {
3347  return select(a, a.ctx().num_val(i, a.get_sort().array_domain()));
3348  }
3349  inline expr select(expr const & a, expr_vector const & i) {
3350  check_context(a, i);
3351  array<Z3_ast> idxs(i);
3352  Z3_ast r = Z3_mk_select_n(a.ctx(), a, idxs.size(), idxs.ptr());
3353  a.check_error();
3354  return expr(a.ctx(), r);
3355  }
3356 
3357  inline expr store(expr const & a, expr const & i, expr const & v) {
3358  check_context(a, i); check_context(a, v);
3359  Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
3360  a.check_error();
3361  return expr(a.ctx(), r);
3362  }
3363 
3364  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); }
3365  inline expr store(expr const & a, expr i, int v) { return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
3366  inline expr store(expr const & a, int i, int v) {
3367  return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
3368  }
3369  inline expr store(expr const & a, expr_vector const & i, expr const & v) {
3370  check_context(a, i); check_context(a, v);
3371  array<Z3_ast> idxs(i);
3372  Z3_ast r = Z3_mk_store_n(a.ctx(), a, idxs.size(), idxs.ptr(), v);
3373  a.check_error();
3374  return expr(a.ctx(), r);
3375  }
3376 
3377  inline expr as_array(func_decl & f) {
3378  Z3_ast r = Z3_mk_as_array(f.ctx(), f);
3379  f.check_error();
3380  return expr(f.ctx(), r);
3381  }
3382 
3383 #define MK_EXPR1(_fn, _arg) \
3384  Z3_ast r = _fn(_arg.ctx(), _arg); \
3385  _arg.check_error(); \
3386  return expr(_arg.ctx(), r);
3387 
3388 #define MK_EXPR2(_fn, _arg1, _arg2) \
3389  check_context(_arg1, _arg2); \
3390  Z3_ast r = _fn(_arg1.ctx(), _arg1, _arg2); \
3391  _arg1.check_error(); \
3392  return expr(_arg1.ctx(), r);
3393 
3394  inline expr const_array(sort const & d, expr const & v) {
3395  MK_EXPR2(Z3_mk_const_array, d, v);
3396  }
3397 
3398  inline expr empty_set(sort const& s) {
3400  }
3401 
3402  inline expr full_set(sort const& s) {
3404  }
3405 
3406  inline expr set_add(expr const& s, expr const& e) {
3407  MK_EXPR2(Z3_mk_set_add, s, e);
3408  }
3409 
3410  inline expr set_del(expr const& s, expr const& e) {
3411  MK_EXPR2(Z3_mk_set_del, s, e);
3412  }
3413 
3414  inline expr set_union(expr const& a, expr const& b) {
3415  check_context(a, b);
3416  Z3_ast es[2] = { a, b };
3417  Z3_ast r = Z3_mk_set_union(a.ctx(), 2, es);
3418  a.check_error();
3419  return expr(a.ctx(), r);
3420  }
3421 
3422  inline expr set_intersect(expr const& a, expr const& b) {
3423  check_context(a, b);
3424  Z3_ast es[2] = { a, b };
3425  Z3_ast r = Z3_mk_set_intersect(a.ctx(), 2, es);
3426  a.check_error();
3427  return expr(a.ctx(), r);
3428  }
3429 
3430  inline expr set_difference(expr const& a, expr const& b) {
3432  }
3433 
3434  inline expr set_complement(expr const& a) {
3436  }
3437 
3438  inline expr set_member(expr const& s, expr const& e) {
3439  MK_EXPR2(Z3_mk_set_member, s, e);
3440  }
3441 
3442  inline expr set_subset(expr const& a, expr const& b) {
3443  MK_EXPR2(Z3_mk_set_subset, a, b);
3444  }
3445 
3446  // sequence and regular expression operations.
3447  // union is +
3448  // concat is overloaded to handle sequences and regular expressions
3449 
3450  inline expr empty(sort const& s) {
3451  Z3_ast r = Z3_mk_seq_empty(s.ctx(), s);
3452  s.check_error();
3453  return expr(s.ctx(), r);
3454  }
3455  inline expr suffixof(expr const& a, expr const& b) {
3456  check_context(a, b);
3457  Z3_ast r = Z3_mk_seq_suffix(a.ctx(), a, b);
3458  a.check_error();
3459  return expr(a.ctx(), r);
3460  }
3461  inline expr prefixof(expr const& a, expr const& b) {
3462  check_context(a, b);
3463  Z3_ast r = Z3_mk_seq_prefix(a.ctx(), a, b);
3464  a.check_error();
3465  return expr(a.ctx(), r);
3466  }
3467  inline expr indexof(expr const& s, expr const& substr, expr const& offset) {
3468  check_context(s, substr); check_context(s, offset);
3469  Z3_ast r = Z3_mk_seq_index(s.ctx(), s, substr, offset);
3470  s.check_error();
3471  return expr(s.ctx(), r);
3472  }
3473  inline expr last_indexof(expr const& s, expr const& substr) {
3474  check_context(s, substr);
3475  Z3_ast r = Z3_mk_seq_last_index(s.ctx(), s, substr);
3476  s.check_error();
3477  return expr(s.ctx(), r);
3478  }
3479  inline expr to_re(expr const& s) {
3481  }
3482  inline expr in_re(expr const& s, expr const& re) {
3483  MK_EXPR2(Z3_mk_seq_in_re, s, re);
3484  }
3485  inline expr plus(expr const& re) {
3486  MK_EXPR1(Z3_mk_re_plus, re);
3487  }
3488  inline expr option(expr const& re) {
3490  }
3491  inline expr star(expr const& re) {
3492  MK_EXPR1(Z3_mk_re_star, re);
3493  }
3494  inline expr re_empty(sort const& s) {
3495  Z3_ast r = Z3_mk_re_empty(s.ctx(), s);
3496  s.check_error();
3497  return expr(s.ctx(), r);
3498  }
3499  inline expr re_full(sort const& s) {
3500  Z3_ast r = Z3_mk_re_full(s.ctx(), s);
3501  s.check_error();
3502  return expr(s.ctx(), r);
3503  }
3504  inline expr re_intersect(expr_vector const& args) {
3505  assert(args.size() > 0);
3506  context& ctx = args[0].ctx();
3507  array<Z3_ast> _args(args);
3508  Z3_ast r = Z3_mk_re_intersect(ctx, _args.size(), _args.ptr());
3509  ctx.check_error();
3510  return expr(ctx, r);
3511  }
3512  inline expr re_complement(expr const& a) {
3514  }
3515  inline expr range(expr const& lo, expr const& hi) {
3516  check_context(lo, hi);
3517  Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
3518  lo.check_error();
3519  return expr(lo.ctx(), r);
3520  }
3521 
3522 
3523 
3524 
3525 
3526  inline expr_vector context::parse_string(char const* s) {
3527  Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0);
3528  check_error();
3529  return expr_vector(*this, r);
3530 
3531  }
3532  inline expr_vector context::parse_file(char const* s) {
3533  Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0);
3534  check_error();
3535  return expr_vector(*this, r);
3536  }
3537 
3538  inline expr_vector context::parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls) {
3539  array<Z3_symbol> sort_names(sorts.size());
3540  array<Z3_symbol> decl_names(decls.size());
3541  array<Z3_sort> sorts1(sorts);
3542  array<Z3_func_decl> decls1(decls);
3543  for (unsigned i = 0; i < sorts.size(); ++i) {
3544  sort_names[i] = sorts[i].name();
3545  }
3546  for (unsigned i = 0; i < decls.size(); ++i) {
3547  decl_names[i] = decls[i].name();
3548  }
3549 
3550  Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
3551  check_error();
3552  return expr_vector(*this, r);
3553  }
3554 
3555  inline expr_vector context::parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls) {
3556  array<Z3_symbol> sort_names(sorts.size());
3557  array<Z3_symbol> decl_names(decls.size());
3558  array<Z3_sort> sorts1(sorts);
3559  array<Z3_func_decl> decls1(decls);
3560  for (unsigned i = 0; i < sorts.size(); ++i) {
3561  sort_names[i] = sorts[i].name();
3562  }
3563  for (unsigned i = 0; i < decls.size(); ++i) {
3564  decl_names[i] = decls[i].name();
3565  }
3566  Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
3567  check_error();
3568  return expr_vector(*this, r);
3569  }
3570 
3571 
3572  inline expr expr::substitute(expr_vector const& src, expr_vector const& dst) {
3573  assert(src.size() == dst.size());
3574  array<Z3_ast> _src(src.size());
3575  array<Z3_ast> _dst(dst.size());
3576  for (unsigned i = 0; i < src.size(); ++i) {
3577  _src[i] = src[i];
3578  _dst[i] = dst[i];
3579  }
3580  Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
3581  check_error();
3582  return expr(ctx(), r);
3583  }
3584 
3585  inline expr expr::substitute(expr_vector const& dst) {
3586  array<Z3_ast> _dst(dst.size());
3587  for (unsigned i = 0; i < dst.size(); ++i) {
3588  _dst[i] = dst[i];
3589  }
3590  Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
3591  check_error();
3592  return expr(ctx(), r);
3593  }
3594 
3595 
3597 
3598  typedef std::function<void(unsigned, expr const&)> fixed_eh_t;
3599  typedef std::function<void(void)> final_eh_t;
3600  typedef std::function<void(unsigned, unsigned)> eq_eh_t;
3601 
3602  final_eh_t m_final_eh;
3603  eq_eh_t m_eq_eh;
3604  fixed_eh_t m_fixed_eh;
3605  solver* s;
3606  Z3_context c;
3607  Z3_solver_callback cb { nullptr };
3608 
3609  Z3_context ctx() {
3610  return c ? c : (Z3_context)s->ctx();
3611  }
3612 
3613  struct scoped_cb {
3615  scoped_cb(void* _p, Z3_solver_callback cb):p(static_cast<user_propagator_base*>(_p)) {
3616  p->cb = cb;
3617  }
3618  ~scoped_cb() {
3619  p->cb = nullptr;
3620  }
3621  };
3622 
3623  static void push_eh(void* p) {
3624  static_cast<user_propagator_base*>(p)->push();
3625  }
3626 
3627  static void pop_eh(void* p, unsigned num_scopes) {
3628  static_cast<user_propagator_base*>(p)->pop(num_scopes);
3629  }
3630 
3631  static void* fresh_eh(void* p, Z3_context ctx) {
3632  return static_cast<user_propagator_base*>(p)->fresh(ctx);
3633  }
3634 
3635  static void fixed_eh(void* _p, Z3_solver_callback cb, unsigned id, Z3_ast _value) {
3636  user_propagator_base* p = static_cast<user_propagator_base*>(_p);
3637  scoped_cb _cb(p, cb);
3638  scoped_context ctx(p->ctx());
3639  expr value(ctx(), _value);
3640  static_cast<user_propagator_base*>(p)->m_fixed_eh(id, value);
3641  }
3642 
3643  static void eq_eh(void* p, Z3_solver_callback cb, unsigned x, unsigned y) {
3644  scoped_cb _cb(p, cb);
3645  static_cast<user_propagator_base*>(p)->m_eq_eh(x, y);
3646  }
3647 
3648  static void final_eh(void* p, Z3_solver_callback cb) {
3649  scoped_cb _cb(p, cb);
3650  static_cast<user_propagator_base*>(p)->m_final_eh();
3651  }
3652 
3653 
3654  public:
3655  user_propagator_base(solver* s): s(s), c(nullptr) {}
3656  user_propagator_base(Z3_context c): s(nullptr), c(c) {}
3657 
3658  virtual void push() = 0;
3659  virtual void pop(unsigned num_scopes) = 0;
3660 
3669  virtual user_propagator_base* fresh(Z3_context ctx) = 0;
3670 
3677  void fixed(fixed_eh_t& f) {
3678  assert(s);
3679  m_fixed_eh = f;
3680  Z3_solver_propagate_fixed(ctx(), *s, fixed_eh);
3681  }
3682 
3683  void eq(eq_eh_t& f) {
3684  assert(s);
3685  m_eq_eh = f;
3686  Z3_solver_propagate_eq(ctx(), *s, eq_eh);
3687  }
3688 
3697  void final(final_eh_t& f) {
3698  assert(s);
3699  m_final_eh = f;
3700  Z3_solver_propagate_final(ctx(), *s, final_eh);
3701  }
3702 
3717  unsigned add(expr const& e) {
3718  assert(s);
3719  return Z3_solver_propagate_register(ctx(), *s, e);
3720  }
3721 
3722  void conflict(unsigned num_fixed, unsigned const* fixed) {
3723  assert(cb);
3724  scoped_context _ctx(ctx());
3725  expr conseq = _ctx().bool_val(false);
3726  Z3_solver_propagate_consequence(ctx(), cb, num_fixed, fixed, 0, nullptr, nullptr, conseq);
3727  }
3728 
3729  void propagate(unsigned num_fixed, unsigned const* fixed, expr const& conseq) {
3730  assert(cb);
3731  assert(conseq.ctx() == ctx());
3732  Z3_solver_propagate_consequence(ctx(), cb, num_fixed, fixed, 0, nullptr, nullptr, conseq);
3733  }
3734 
3735  void propagate(unsigned num_fixed, unsigned const* fixed,
3736  unsigned num_eqs, unsigned const* lhs, unsigned const * rhs,
3737  expr const& conseq) {
3738  assert(cb);
3739  assert(conseq.ctx() == ctx());
3740  Z3_solver_propagate_consequence(ctx(), cb, num_fixed, fixed, num_eqs, lhs, rhs, conseq);
3741  }
3742  };
3743 
3744 
3745 
3746 
3747 }
3748 
3751 #undef Z3_THROW
3752 
z3::optimize::check
check_result check()
Definition: z3++.h:2894
Z3_mk_re_plus
Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re)
Create the regular language re+.
z3::operator!=
expr operator!=(expr const &a, expr const &b)
Definition: z3++.h:1475
z3::array::~array
~array()
Definition: z3++.h:403
z3::expr::stoi
expr stoi() const
Definition: z3++.h:1318
Z3_model_get_func_interp
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...
z3::params::~params
~params()
Definition: z3++.h:475
z3::ast::~ast
~ast()
Definition: z3++.h:503
Z3_model_eval
Z3_bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast *v)
Evaluate the AST node t in the given model. Return true if succeeded, and store the result in v.
Z3_global_param_reset_all
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...
z3::optimize::add_soft
handle add_soft(expr const &e, char const *weight)
Definition: z3++.h:2875
Z3_mk_unary_minus
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
z3::plus
expr plus(expr const &re)
Definition: z3++.h:3485
z3::xnor
expr xnor(expr const &a, expr const &b)
Definition: z3++.h:1708
z3::stats::double_value
double double_value(unsigned i) const
Definition: z3++.h:2348
z3::goal
Definition: z3++.h:2578
z3::goal::add
void add(expr_vector const &v)
Definition: z3++.h:2598
z3::ast::ast
ast(context &c, Z3_ast n)
Definition: z3++.h:501
z3::suffixof
expr suffixof(expr const &a, expr const &b)
Definition: z3++.h:3455
z3::fail_if
tactic fail_if(probe const &p)
Definition: z3++.h:2971
z3::expr::lo
unsigned lo() const
Definition: z3++.h:1267
Z3_mk_store_n
Z3_ast Z3_API Z3_mk_store_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const *idxs, Z3_ast v)
n-ary Array update.
z3::optimize::from_string
void from_string(char const *constraints)
Definition: z3++.h:2924
z3::pw
expr pw(expr const &a, expr const &b)
Definition: z3++.h:1395
Z3_model_dec_ref
void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m)
Decrement the reference counter of the given model.
Z3_model_translate
Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context dst)
translate model from context c to context dst.
z3::ast::kind
Z3_ast_kind kind() const
Definition: z3++.h:507
z3::expr::at
expr at(expr const &index) const
Definition: z3++.h:1301
z3::expr::operator&
friend expr operator&(expr const &a, expr const &b)
Definition: z3++.h:1694
Z3_optimize_pop
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.
z3::set_difference
expr set_difference(expr const &a, expr const &b)
Definition: z3++.h:3430
Z3_mk_string_symbol
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.