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<ostream>
25 #include<string>
26 #include<memory>
27 #include<vector>
28 #include<z3.h>
29 #include<limits.h>
30 #include<functional>
31 
32 #undef min
33 #undef max
34 
49 namespace z3 {
50 
51  class exception;
52  class config;
53  class context;
54  class symbol;
55  class params;
56  class param_descrs;
57  class ast;
58  class sort;
59  class constructors;
60  class constructor_list;
61  class func_decl;
62  class expr;
63  class solver;
64  class goal;
65  class tactic;
66  class probe;
67  class model;
68  class func_interp;
69  class func_entry;
70  class statistics;
71  class apply_result;
72  template<typename T> class cast_ast;
73  template<typename T> class ast_vector_tpl;
78 
79  inline void set_param(char const * param, char const * value) { Z3_global_param_set(param, value); }
80  inline void set_param(char const * param, bool value) { Z3_global_param_set(param, value ? "true" : "false"); }
81  inline void set_param(char const * param, int value) { auto str = std::to_string(value); Z3_global_param_set(param, str.c_str()); }
83 
87  class exception : public std::exception {
88  std::string m_msg;
89  public:
90  virtual ~exception() throw() = default;
91  exception(char const * msg):m_msg(msg) {}
92  char const * msg() const { return m_msg.c_str(); }
93  char const * what() const throw() { return m_msg.c_str(); }
94  friend std::ostream & operator<<(std::ostream & out, exception const & e);
95  };
96  inline std::ostream & operator<<(std::ostream & out, exception const & e) { out << e.msg(); return out; }
97 
98 #if !defined(Z3_THROW)
99 #if __cpp_exceptions || _CPPUNWIND || __EXCEPTIONS
100 #define Z3_THROW(x) throw x
101 #else
102 #define Z3_THROW(x) {}
103 #endif
104 #endif // !defined(Z3_THROW)
105 
109  class config {
110  Z3_config m_cfg;
111  config(config const &) = delete;
112  config & operator=(config const &) = delete;
113  public:
114  config() { m_cfg = Z3_mk_config(); }
115  ~config() { Z3_del_config(m_cfg); }
116  operator Z3_config() const { return m_cfg; }
120  void set(char const * param, char const * value) { Z3_set_param_value(m_cfg, param, value); }
124  void set(char const * param, bool value) { Z3_set_param_value(m_cfg, param, value ? "true" : "false"); }
128  void set(char const * param, int value) {
129  auto str = std::to_string(value);
130  Z3_set_param_value(m_cfg, param, str.c_str());
131  }
132  };
133 
136  };
137 
143  RTZ
144  };
145 
147  if (l == Z3_L_TRUE) return sat;
148  else if (l == Z3_L_FALSE) return unsat;
149  return unknown;
150  }
151 
152 
158  class context {
159  private:
160  friend class user_propagator_base;
161  bool m_enable_exceptions = true;
162  rounding_mode m_rounding_mode;
163  Z3_context m_ctx = nullptr;
164  void init(config & c) {
165  set_context(Z3_mk_context_rc(c));
166  }
167  void set_context(Z3_context ctx) {
168  m_ctx = ctx;
169  m_enable_exceptions = true;
170  m_rounding_mode = RNE;
171  Z3_set_error_handler(m_ctx, 0);
173  }
174 
175 
176  context(context const &) = delete;
177  context & operator=(context const &) = delete;
178 
179  context(Z3_context c) { set_context(c); }
180  void detach() { m_ctx = nullptr; }
181  public:
182  context() { config c; init(c); }
183  context(config & c) { init(c); }
184  ~context() { if (m_ctx) Z3_del_context(m_ctx); }
185  operator Z3_context() const { return m_ctx; }
186 
191  Z3_error_code e = Z3_get_error_code(m_ctx);
192  if (e != Z3_OK && enable_exceptions())
193  Z3_THROW(exception(Z3_get_error_msg(m_ctx, e)));
194  return e;
195  }
196 
197  void check_parser_error() const {
198  check_error();
199  }
200 
208  void set_enable_exceptions(bool f) { m_enable_exceptions = f; }
209 
210  bool enable_exceptions() const { return m_enable_exceptions; }
211 
215  void set(char const * param, char const * value) { Z3_update_param_value(m_ctx, param, value); }
219  void set(char const * param, bool value) { Z3_update_param_value(m_ctx, param, value ? "true" : "false"); }
223  void set(char const * param, int value) {
224  auto str = std::to_string(value);
225  Z3_update_param_value(m_ctx, param, str.c_str());
226  }
227 
232  void interrupt() { Z3_interrupt(m_ctx); }
233 
237  symbol str_symbol(char const * s);
241  symbol int_symbol(int n);
245  sort bool_sort();
249  sort int_sort();
253  sort real_sort();
257  sort bv_sort(unsigned sz);
258 
262  sort char_sort();
266  sort string_sort();
270  sort seq_sort(sort& s);
280  sort array_sort(sort d, sort r);
281  sort array_sort(sort_vector const& d, sort r);
288  sort fpa_sort(unsigned ebits, unsigned sbits);
292  template<size_t precision>
307  sort enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts);
308 
315  func_decl tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs);
316 
317 
326  sort datatype(symbol const& name, constructors const& cs);
327 
334  sort_vector datatypes(unsigned n, symbol const* names,
335  constructor_list *const* cons);
336 
337 
342  sort datatype_sort(symbol const& name);
343 
344 
348  sort uninterpreted_sort(char const* name);
349  sort uninterpreted_sort(symbol const& name);
350 
351  func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range);
352  func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range);
353  func_decl function(symbol const& name, sort_vector const& domain, sort const& range);
354  func_decl function(char const * name, sort_vector const& domain, sort const& range);
355  func_decl function(char const * name, sort const & domain, sort const & range);
356  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range);
357  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range);
358  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range);
359  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range);
360 
361  func_decl recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range);
362  func_decl recfun(char const * name, unsigned arity, sort const * domain, sort const & range);
363  func_decl recfun(char const * name, sort const & domain, sort const & range);
364  func_decl recfun(char const * name, sort const & d1, sort const & d2, sort const & range);
365 
366  void recdef(func_decl, expr_vector const& args, expr const& body);
367  func_decl user_propagate_function(symbol const& name, sort_vector const& domain, sort const& range);
368 
372  expr constant(symbol const & name, sort const & s);
373  expr constant(char const * name, sort const & s);
377  expr bool_const(char const * name);
378  expr int_const(char const * name);
379  expr real_const(char const * name);
380  expr string_const(char const * name);
381  expr bv_const(char const * name, unsigned sz);
382  expr fpa_const(char const * name, unsigned ebits, unsigned sbits);
383 
384  template<size_t precision>
385  expr fpa_const(char const * name);
386 
390  expr variable(unsigned index, sort const& s);
391 
392 
394 
395  expr bool_val(bool b);
396 
397  expr int_val(int n);
398  expr int_val(unsigned n);
399  expr int_val(int64_t n);
400  expr int_val(uint64_t n);
401  expr int_val(char const * n);
402 
403  expr real_val(int n, int d);
404  expr real_val(int n);
405  expr real_val(unsigned n);
406  expr real_val(int64_t n);
407  expr real_val(uint64_t n);
408  expr real_val(char const * n);
409 
410  expr bv_val(int n, unsigned sz);
411  expr bv_val(unsigned n, unsigned sz);
412  expr bv_val(int64_t n, unsigned sz);
413  expr bv_val(uint64_t n, unsigned sz);
414  expr bv_val(char const * n, unsigned sz);
415  expr bv_val(unsigned n, bool const* bits);
416 
417  expr fpa_val(double n);
418  expr fpa_val(float n);
419  expr fpa_nan(sort const & s);
420  expr fpa_inf(sort const & s, bool sgn);
421 
422  expr string_val(char const* s);
423  expr string_val(char const* s, unsigned n);
424  expr string_val(std::string const& s);
425  expr string_val(std::u32string const& s);
426 
427  expr num_val(int n, sort const & s);
428 
432  expr_vector parse_string(char const* s);
433  expr_vector parse_file(char const* file);
434 
435  expr_vector parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
436  expr_vector parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
437  };
438 
439 
440  template<typename T>
441  class array {
442  std::unique_ptr<T[]> m_array;
443  unsigned m_size;
444  array(array const &) = delete;
445  array & operator=(array const &) = delete;
446  public:
447  array(unsigned sz):m_array(new T[sz]),m_size(sz) {}
448  template<typename T2>
449  array(ast_vector_tpl<T2> const & v);
450  void resize(unsigned sz) { m_array.reset(new T[sz]); m_size = sz; }
451  unsigned size() const { return m_size; }
452  T & operator[](int i) { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
453  T const & operator[](int i) const { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
454  T const * ptr() const { return m_array.get(); }
455  T * ptr() { return m_array.get(); }
456  };
457 
458  class object {
459  protected:
461  public:
462  object(context & c):m_ctx(&c) {}
463  context & ctx() const { return *m_ctx; }
465  friend void check_context(object const & a, object const & b);
466  };
467  inline void check_context(object const & a, object const & b) { (void)a; (void)b; assert(a.m_ctx == b.m_ctx); }
468 
469  class symbol : public object {
470  Z3_symbol m_sym;
471  public:
472  symbol(context & c, Z3_symbol s):object(c), m_sym(s) {}
473  operator Z3_symbol() const { return m_sym; }
474  Z3_symbol_kind kind() const { return Z3_get_symbol_kind(ctx(), m_sym); }
475  std::string str() const { assert(kind() == Z3_STRING_SYMBOL); return Z3_get_symbol_string(ctx(), m_sym); }
476  int to_int() const { assert(kind() == Z3_INT_SYMBOL); return Z3_get_symbol_int(ctx(), m_sym); }
477  friend std::ostream & operator<<(std::ostream & out, symbol const & s);
478  };
479 
480  inline std::ostream & operator<<(std::ostream & out, symbol const & s) {
481  if (s.kind() == Z3_INT_SYMBOL)
482  out << "k!" << s.to_int();
483  else
484  out << s.str();
485  return out;
486  }
487 
488 
489  class param_descrs : public object {
490  Z3_param_descrs m_descrs;
491  public:
492  param_descrs(context& c, Z3_param_descrs d): object(c), m_descrs(d) { Z3_param_descrs_inc_ref(c, d); }
493  param_descrs(param_descrs const& o): object(o.ctx()), m_descrs(o.m_descrs) { Z3_param_descrs_inc_ref(ctx(), m_descrs); }
495  Z3_param_descrs_inc_ref(o.ctx(), o.m_descrs);
496  Z3_param_descrs_dec_ref(ctx(), m_descrs);
497  m_descrs = o.m_descrs;
498  object::operator=(o);
499  return *this;
500  }
504 
505  unsigned size() { return Z3_param_descrs_size(ctx(), m_descrs); }
506  symbol name(unsigned i) { return symbol(ctx(), Z3_param_descrs_get_name(ctx(), m_descrs, i)); }
507  Z3_param_kind kind(symbol const& s) { return Z3_param_descrs_get_kind(ctx(), m_descrs, s); }
508  std::string documentation(symbol const& s) { char const* r = Z3_param_descrs_get_documentation(ctx(), m_descrs, s); check_error(); return r; }
509  std::string to_string() const { return Z3_param_descrs_to_string(ctx(), m_descrs); }
510  };
511 
512  inline std::ostream& operator<<(std::ostream & out, param_descrs const & d) { return out << d.to_string(); }
513 
514  class params : public object {
515  Z3_params m_params;
516  public:
517  params(context & c):object(c) { m_params = Z3_mk_params(c); Z3_params_inc_ref(ctx(), m_params); }
518  params(params const & s):object(s), m_params(s.m_params) { Z3_params_inc_ref(ctx(), m_params); }
519  ~params() { Z3_params_dec_ref(ctx(), m_params); }
520  operator Z3_params() const { return m_params; }
521  params & operator=(params const & s) {
522  Z3_params_inc_ref(s.ctx(), s.m_params);
523  Z3_params_dec_ref(ctx(), m_params);
524  object::operator=(s);
525  m_params = s.m_params;
526  return *this;
527  }
528  void set(char const * k, bool b) { Z3_params_set_bool(ctx(), m_params, ctx().str_symbol(k), b); }
529  void set(char const * k, unsigned n) { Z3_params_set_uint(ctx(), m_params, ctx().str_symbol(k), n); }
530  void set(char const * k, double n) { Z3_params_set_double(ctx(), m_params, ctx().str_symbol(k), n); }
531  void set(char const * k, symbol const & s) { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), s); }
532  void set(char const * k, char const* s) { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), ctx().str_symbol(s)); }
533  friend std::ostream & operator<<(std::ostream & out, params const & p);
534  };
535 
536  inline std::ostream & operator<<(std::ostream & out, params const & p) {
537  out << Z3_params_to_string(p.ctx(), p); return out;
538  }
539 
540  class ast : public object {
541  protected:
543  public:
544  ast(context & c):object(c), m_ast(0) {}
545  ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
546  ast(ast const & s) :object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
547  ~ast() { if (m_ast) { Z3_dec_ref(*m_ctx, m_ast); } }
548  operator Z3_ast() const { return m_ast; }
549  operator bool() const { return m_ast != 0; }
550  ast & operator=(ast const & s) {
551  Z3_inc_ref(s.ctx(), s.m_ast);
552  if (m_ast)
553  Z3_dec_ref(ctx(), m_ast);
554  object::operator=(s);
555  m_ast = s.m_ast;
556  return *this;
557  }
558  Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }
559  unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }
560  friend std::ostream & operator<<(std::ostream & out, ast const & n);
561  std::string to_string() const { return std::string(Z3_ast_to_string(ctx(), m_ast)); }
562 
563 
567  friend bool eq(ast const & a, ast const & b);
568  };
569  inline std::ostream & operator<<(std::ostream & out, ast const & n) {
570  out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
571  }
572 
573  inline bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b); }
574 
575  template<typename T>
576  class ast_vector_tpl : public object {
577  Z3_ast_vector m_vector;
578  void init(Z3_ast_vector v) { Z3_ast_vector_inc_ref(ctx(), v); m_vector = v; }
579  public:
581  ast_vector_tpl(context & c, Z3_ast_vector v):object(c) { init(v); }
582  ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
583  ast_vector_tpl(context& c, ast_vector_tpl const& src): object(c) { init(Z3_ast_vector_translate(src.ctx(), src, c)); }
584 
586  operator Z3_ast_vector() const { return m_vector; }
587  unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); }
588  T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
589  void push_back(T const & e) { Z3_ast_vector_push(ctx(), m_vector, e); check_error(); }
590  void resize(unsigned sz) { Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }
591  T back() const { return operator[](size() - 1); }
592  void pop_back() { assert(size() > 0); resize(size() - 1); }
593  bool empty() const { return size() == 0; }
595  Z3_ast_vector_inc_ref(s.ctx(), s.m_vector);
596  Z3_ast_vector_dec_ref(ctx(), m_vector);
597  object::operator=(s);
598  m_vector = s.m_vector;
599  return *this;
600  }
601  ast_vector_tpl& set(unsigned idx, ast& a) {
602  Z3_ast_vector_set(ctx(), m_vector, idx, a);
603  return *this;
604  }
605  /*
606  Disabled pending C++98 build upgrade
607  bool contains(T const& x) const {
608  for (T y : *this) if (eq(x, y)) return true;
609  return false;
610  }
611  */
612 
613  class iterator final {
614  ast_vector_tpl const* m_vector;
615  unsigned m_index;
616  public:
617  iterator(ast_vector_tpl const* v, unsigned i): m_vector(v), m_index(i) {}
618 
619  bool operator==(iterator const& other) const noexcept {
620  return other.m_index == m_index;
621  };
622  bool operator!=(iterator const& other) const noexcept {
623  return other.m_index != m_index;
624  };
625  iterator& operator++() noexcept {
626  ++m_index;
627  return *this;
628  }
629  void set(T& arg) {
630  Z3_ast_vector_set(m_vector->ctx(), *m_vector, m_index, arg);
631  }
632  iterator operator++(int) noexcept { iterator tmp = *this; ++m_index; return tmp; }
633  T * operator->() const { return &(operator*()); }
634  T operator*() const { return (*m_vector)[m_index]; }
635  };
636  iterator begin() const noexcept { return iterator(this, 0); }
637  iterator end() const { return iterator(this, size()); }
638  friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
639  std::string to_string() const { return std::string(Z3_ast_vector_to_string(ctx(), m_vector)); }
640  };
641 
642 
646  class sort : public ast {
647  public:
648  sort(context & c):ast(c) {}
649  sort(context & c, Z3_sort s):ast(c, reinterpret_cast<Z3_ast>(s)) {}
650  sort(context & c, Z3_ast a):ast(c, a) {}
651  operator Z3_sort() const { return reinterpret_cast<Z3_sort>(m_ast); }
652 
656  unsigned id() const { unsigned r = Z3_get_sort_id(ctx(), *this); check_error(); return r; }
657 
661  Z3_sort_kind sort_kind() const { return Z3_get_sort_kind(*m_ctx, *this); }
665  symbol name() const { Z3_symbol s = Z3_get_sort_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
669  bool is_bool() const { return sort_kind() == Z3_BOOL_SORT; }
673  bool is_int() const { return sort_kind() == Z3_INT_SORT; }
677  bool is_real() const { return sort_kind() == Z3_REAL_SORT; }
681  bool is_arith() const { return is_int() || is_real(); }
685  bool is_bv() const { return sort_kind() == Z3_BV_SORT; }
689  bool is_array() const { return sort_kind() == Z3_ARRAY_SORT; }
693  bool is_datatype() const { return sort_kind() == Z3_DATATYPE_SORT; }
697  bool is_relation() const { return sort_kind() == Z3_RELATION_SORT; }
701  bool is_seq() const { return sort_kind() == Z3_SEQ_SORT; }
705  bool is_re() const { return sort_kind() == Z3_RE_SORT; }
709  bool is_finite_domain() const { return sort_kind() == Z3_FINITE_DOMAIN_SORT; }
713  bool is_fpa() const { return sort_kind() == Z3_FLOATING_POINT_SORT; }
714 
720  unsigned bv_size() const { assert(is_bv()); unsigned r = Z3_get_bv_sort_size(ctx(), *this); check_error(); return r; }
721 
722  unsigned fpa_ebits() const { assert(is_fpa()); unsigned r = Z3_fpa_get_ebits(ctx(), *this); check_error(); return r; }
723 
724  unsigned fpa_sbits() const { assert(is_fpa()); unsigned r = Z3_fpa_get_sbits(ctx(), *this); check_error(); return r; }
730  sort array_domain() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_domain(ctx(), *this); check_error(); return sort(ctx(), s); }
736  sort array_range() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_range(ctx(), *this); check_error(); return sort(ctx(), s); }
737 
738  friend std::ostream & operator<<(std::ostream & out, sort const & s) { return out << Z3_sort_to_string(s.ctx(), Z3_sort(s.m_ast)); }
739 
742  };
743 
748  class func_decl : public ast {
749  public:
750  func_decl(context & c):ast(c) {}
751  func_decl(context & c, Z3_func_decl n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
752  operator Z3_func_decl() const { return reinterpret_cast<Z3_func_decl>(m_ast); }
753 
757  unsigned id() const { unsigned r = Z3_get_func_decl_id(ctx(), *this); check_error(); return r; }
758 
759  unsigned arity() const { return Z3_get_arity(ctx(), *this); }
760  sort domain(unsigned i) const { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }
761  sort range() const { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }
762  symbol name() const { Z3_symbol s = Z3_get_decl_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
763  Z3_decl_kind decl_kind() const { return Z3_get_decl_kind(ctx(), *this); }
764 
766  Z3_func_decl tc = Z3_mk_transitive_closure(ctx(), *this); check_error(); return func_decl(ctx(), tc);
767  }
768 
769  bool is_const() const { return arity() == 0; }
770 
771  expr operator()() const;
772  expr operator()(unsigned n, expr const * args) const;
773  expr operator()(expr_vector const& v) const;
774  expr operator()(expr const & a) const;
775  expr operator()(int a) const;
776  expr operator()(expr const & a1, expr const & a2) const;
777  expr operator()(expr const & a1, int a2) const;
778  expr operator()(int a1, expr const & a2) const;
779  expr operator()(expr const & a1, expr const & a2, expr const & a3) const;
780  expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const;
781  expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const;
782 
784 
785  };
786 
790  expr select(expr const & a, expr const& i);
791  expr select(expr const & a, expr_vector const & i);
792 
797  class expr : public ast {
798  public:
799  expr(context & c):ast(c) {}
800  expr(context & c, Z3_ast n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
801 
805  sort get_sort() const { Z3_sort s = Z3_get_sort(*m_ctx, m_ast); check_error(); return sort(*m_ctx, s); }
806 
810  bool is_bool() const { return get_sort().is_bool(); }
814  bool is_int() const { return get_sort().is_int(); }
818  bool is_real() const { return get_sort().is_real(); }
822  bool is_arith() const { return get_sort().is_arith(); }
826  bool is_bv() const { return get_sort().is_bv(); }
830  bool is_array() const { return get_sort().is_array(); }
834  bool is_datatype() const { return get_sort().is_datatype(); }
838  bool is_relation() const { return get_sort().is_relation(); }
842  bool is_seq() const { return get_sort().is_seq(); }
846  bool is_re() const { return get_sort().is_re(); }
847 
856  bool is_finite_domain() const { return get_sort().is_finite_domain(); }
860  bool is_fpa() const { return get_sort().is_fpa(); }
861 
867  bool is_numeral() const { return kind() == Z3_NUMERAL_AST; }
868  bool is_numeral_i64(int64_t& i) const { bool r = Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}
869  bool is_numeral_u64(uint64_t& i) const { bool r = Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}
870  bool is_numeral_i(int& i) const { bool r = Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}
871  bool is_numeral_u(unsigned& i) const { bool r = Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
872  bool is_numeral(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; }
873  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; }
874  bool is_numeral(double& d) const { if (!is_numeral()) return false; d = Z3_get_numeral_double(ctx(), m_ast); check_error(); return true; }
875  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; }
876 
877  double as_double() const { double d = 0; is_numeral(d); return d; }
878  uint64_t as_uint64() const { uint64_t r = 0; is_numeral_u64(r); return r; }
879  int64_t as_int64() const { int64_t r = 0; is_numeral_i64(r); return r; }
880 
881 
885  bool is_app() const { return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
889  bool is_const() const { return is_app() && num_args() == 0; }
893  bool is_quantifier() const { return kind() == Z3_QUANTIFIER_AST; }
894 
898  bool is_forall() const { return Z3_is_quantifier_forall(ctx(), m_ast); }
902  bool is_exists() const { return Z3_is_quantifier_exists(ctx(), m_ast); }
906  bool is_lambda() const { return Z3_is_lambda(ctx(), m_ast); }
911  bool is_var() const { return kind() == Z3_VAR_AST; }
915  bool is_algebraic() const { return Z3_is_algebraic_number(ctx(), m_ast); }
916 
920  bool is_well_sorted() const { bool r = Z3_is_well_sorted(ctx(), m_ast); check_error(); return r; }
921 
925  expr mk_is_inf() const {
926  assert(is_fpa());
928  check_error();
929  return expr(ctx(), r);
930  }
931 
935  expr mk_is_nan() const {
936  assert(is_fpa());
938  check_error();
939  return expr(ctx(), r);
940  }
941 
945  expr mk_is_normal() const {
946  assert(is_fpa());
948  check_error();
949  return expr(ctx(), r);
950  }
951 
956  assert(is_fpa());
958  check_error();
959  return expr(ctx(), r);
960  }
961 
965  expr mk_is_zero() const {
966  assert(is_fpa());
968  check_error();
969  return expr(ctx(), r);
970  }
971 
975  expr mk_to_ieee_bv() const {
976  assert(is_fpa());
978  check_error();
979  return expr(ctx(), r);
980  }
981 
985  expr mk_from_ieee_bv(sort const &s) const {
986  assert(is_bv());
987  Z3_ast r = Z3_mk_fpa_to_fp_bv(ctx(), m_ast, s);
988  check_error();
989  return expr(ctx(), r);
990  }
991 
998  std::string get_decimal_string(int precision) const {
999  assert(is_numeral() || is_algebraic());
1000  return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
1001  }
1002 
1006  expr algebraic_lower(unsigned precision) const {
1007  assert(is_algebraic());
1008  Z3_ast r = Z3_get_algebraic_number_lower(ctx(), m_ast, precision);
1009  check_error();
1010  return expr(ctx(), r);
1011  }
1012 
1013  expr algebraic_upper(unsigned precision) const {
1014  assert(is_algebraic());
1015  Z3_ast r = Z3_get_algebraic_number_upper(ctx(), m_ast, precision);
1016  check_error();
1017  return expr(ctx(), r);
1018  }
1019 
1024  assert(is_algebraic());
1026  check_error();
1027  return expr_vector(ctx(), r);
1028  }
1029 
1033  unsigned algebraic_i() const {
1034  assert(is_algebraic());
1035  unsigned i = Z3_algebraic_get_i(ctx(), m_ast);
1036  check_error();
1037  return i;
1038  }
1039 
1043  unsigned id() const { unsigned r = Z3_get_ast_id(ctx(), m_ast); check_error(); return r; }
1044 
1055  int get_numeral_int() const {
1056  int result = 0;
1057  if (!is_numeral_i(result)) {
1058  assert(ctx().enable_exceptions());
1059  if (!ctx().enable_exceptions()) return 0;
1060  Z3_THROW(exception("numeral does not fit in machine int"));
1061  }
1062  return result;
1063  }
1064 
1074  unsigned get_numeral_uint() const {
1075  assert(is_numeral());
1076  unsigned result = 0;
1077  if (!is_numeral_u(result)) {
1078  assert(ctx().enable_exceptions());
1079  if (!ctx().enable_exceptions()) return 0;
1080  Z3_THROW(exception("numeral does not fit in machine uint"));
1081  }
1082  return result;
1083  }
1084 
1091  int64_t get_numeral_int64() const {
1092  assert(is_numeral());
1093  int64_t result = 0;
1094  if (!is_numeral_i64(result)) {
1095  assert(ctx().enable_exceptions());
1096  if (!ctx().enable_exceptions()) return 0;
1097  Z3_THROW(exception("numeral does not fit in machine int64_t"));
1098  }
1099  return result;
1100  }
1101 
1108  uint64_t get_numeral_uint64() const {
1109  assert(is_numeral());
1110  uint64_t result = 0;
1111  if (!is_numeral_u64(result)) {
1112  assert(ctx().enable_exceptions());
1113  if (!ctx().enable_exceptions()) return 0;
1114  Z3_THROW(exception("numeral does not fit in machine uint64_t"));
1115  }
1116  return result;
1117  }
1118 
1120  return Z3_get_bool_value(ctx(), m_ast);
1121  }
1122 
1123  expr numerator() const {
1124  assert(is_numeral());
1125  Z3_ast r = Z3_get_numerator(ctx(), m_ast);
1126  check_error();
1127  return expr(ctx(),r);
1128  }
1129 
1130 
1131  expr denominator() const {
1132  assert(is_numeral());
1134  check_error();
1135  return expr(ctx(),r);
1136  }
1137 
1138 
1143  bool is_string_value() const { return Z3_is_string(ctx(), m_ast); }
1144 
1150  std::string get_string() const {
1151  assert(is_string_value());
1152  char const* s = Z3_get_string(ctx(), m_ast);
1153  check_error();
1154  return std::string(s);
1155  }
1156 
1162  std::u32string get_u32string() const {
1163  assert(is_string_value());
1164  unsigned n = Z3_get_string_length(ctx(), m_ast);
1165  std::u32string s;
1166  s.resize(n);
1167  Z3_get_string_contents(ctx(), m_ast, n, (unsigned*)s.data());
1168  return s;
1169  }
1170 
1171  operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
1172 
1179  func_decl decl() const { Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }
1186  unsigned num_args() const { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
1194  expr arg(unsigned i) const { Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }
1201  expr_vector args() const {
1202  expr_vector vec(ctx());
1203  unsigned argCnt = num_args();
1204  for (unsigned i = 0; i < argCnt; i++)
1205  vec.push_back(arg(i));
1206  return vec;
1207  }
1208 
1214  expr body() const { assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
1215 
1221  friend expr operator!(expr const & a);
1222 
1229  friend expr operator&&(expr const & a, expr const & b);
1230 
1231 
1238  friend expr operator&&(expr const & a, bool b);
1245  friend expr operator&&(bool a, expr const & b);
1246 
1253  friend expr operator||(expr const & a, expr const & b);
1260  friend expr operator||(expr const & a, bool b);
1261 
1268  friend expr operator||(bool a, expr const & b);
1269 
1270  friend expr implies(expr const & a, expr const & b);
1271  friend expr implies(expr const & a, bool b);
1272  friend expr implies(bool a, expr const & b);
1273 
1274  friend expr mk_or(expr_vector const& args);
1275  friend expr mk_xor(expr_vector const& args);
1276  friend expr mk_and(expr_vector const& args);
1277 
1278  friend expr ite(expr const & c, expr const & t, expr const & e);
1279 
1280  bool is_true() const { return is_app() && Z3_OP_TRUE == decl().decl_kind(); }
1281  bool is_false() const { return is_app() && Z3_OP_FALSE == decl().decl_kind(); }
1282  bool is_not() const { return is_app() && Z3_OP_NOT == decl().decl_kind(); }
1283  bool is_and() const { return is_app() && Z3_OP_AND == decl().decl_kind(); }
1284  bool is_or() const { return is_app() && Z3_OP_OR == decl().decl_kind(); }
1285  bool is_xor() const { return is_app() && Z3_OP_XOR == decl().decl_kind(); }
1286  bool is_implies() const { return is_app() && Z3_OP_IMPLIES == decl().decl_kind(); }
1287  bool is_eq() const { return is_app() && Z3_OP_EQ == decl().decl_kind(); }
1288  bool is_ite() const { return is_app() && Z3_OP_ITE == decl().decl_kind(); }
1289  bool is_distinct() const { return is_app() && Z3_OP_DISTINCT == decl().decl_kind(); }
1290 
1291  friend expr distinct(expr_vector const& args);
1292  friend expr concat(expr const& a, expr const& b);
1293  friend expr concat(expr_vector const& args);
1294 
1295  friend expr operator==(expr const & a, expr const & b);
1296  friend expr operator==(expr const & a, int b);
1297  friend expr operator==(int a, expr const & b);
1298 
1299  friend expr operator!=(expr const & a, expr const & b);
1300  friend expr operator!=(expr const & a, int b);
1301  friend expr operator!=(int a, expr const & b);
1302 
1303  friend expr operator+(expr const & a, expr const & b);
1304  friend expr operator+(expr const & a, int b);
1305  friend expr operator+(int a, expr const & b);
1306  friend expr sum(expr_vector const& args);
1307 
1308  friend expr operator*(expr const & a, expr const & b);
1309  friend expr operator*(expr const & a, int b);
1310  friend expr operator*(int a, expr const & b);
1311 
1312  /* \brief Power operator */
1313  friend expr pw(expr const & a, expr const & b);
1314  friend expr pw(expr const & a, int b);
1315  friend expr pw(int a, expr const & b);
1316 
1317  /* \brief mod operator */
1318  friend expr mod(expr const& a, expr const& b);
1319  friend expr mod(expr const& a, int b);
1320  friend expr mod(int a, expr const& b);
1321 
1322  /* \brief rem operator */
1323  friend expr rem(expr const& a, expr const& b);
1324  friend expr rem(expr const& a, int b);
1325  friend expr rem(int a, expr const& b);
1326 
1327  friend expr is_int(expr const& e);
1328 
1329  friend expr operator/(expr const & a, expr const & b);
1330  friend expr operator/(expr const & a, int b);
1331  friend expr operator/(int a, expr const & b);
1332 
1333  friend expr operator-(expr const & a);
1334 
1335  friend expr operator-(expr const & a, expr const & b);
1336  friend expr operator-(expr const & a, int b);
1337  friend expr operator-(int a, expr const & b);
1338 
1339  friend expr operator<=(expr const & a, expr const & b);
1340  friend expr operator<=(expr const & a, int b);
1341  friend expr operator<=(int a, expr const & b);
1342 
1343 
1344  friend expr operator>=(expr const & a, expr const & b);
1345  friend expr operator>=(expr const & a, int b);
1346  friend expr operator>=(int a, expr const & b);
1347 
1348  friend expr operator<(expr const & a, expr const & b);
1349  friend expr operator<(expr const & a, int b);
1350  friend expr operator<(int a, expr const & b);
1351 
1352  friend expr operator>(expr const & a, expr const & b);
1353  friend expr operator>(expr const & a, int b);
1354  friend expr operator>(int a, expr const & b);
1355 
1356  friend expr pble(expr_vector const& es, int const * coeffs, int bound);
1357  friend expr pbge(expr_vector const& es, int const * coeffs, int bound);
1358  friend expr pbeq(expr_vector const& es, int const * coeffs, int bound);
1359  friend expr atmost(expr_vector const& es, unsigned bound);
1360  friend expr atleast(expr_vector const& es, unsigned bound);
1361 
1362  friend expr operator&(expr const & a, expr const & b);
1363  friend expr operator&(expr const & a, int b);
1364  friend expr operator&(int a, expr const & b);
1365 
1366  friend expr operator^(expr const & a, expr const & b);
1367  friend expr operator^(expr const & a, int b);
1368  friend expr operator^(int a, expr const & b);
1369 
1370  friend expr operator|(expr const & a, expr const & b);
1371  friend expr operator|(expr const & a, int b);
1372  friend expr operator|(int a, expr const & b);
1373  friend expr nand(expr const& a, expr const& b);
1374  friend expr nor(expr const& a, expr const& b);
1375  friend expr xnor(expr const& a, expr const& b);
1376 
1377  friend expr min(expr const& a, expr const& b);
1378  friend expr max(expr const& a, expr const& b);
1379 
1380  friend expr bv2int(expr const& a, bool is_signed);
1381  friend expr int2bv(unsigned n, expr const& a);
1382  friend expr bvadd_no_overflow(expr const& a, expr const& b, bool is_signed);
1383  friend expr bvadd_no_underflow(expr const& a, expr const& b);
1384  friend expr bvsub_no_overflow(expr const& a, expr const& b);
1385  friend expr bvsub_no_underflow(expr const& a, expr const& b, bool is_signed);
1386  friend expr bvsdiv_no_overflow(expr const& a, expr const& b);
1387  friend expr bvneg_no_overflow(expr const& a);
1388  friend expr bvmul_no_overflow(expr const& a, expr const& b, bool is_signed);
1389  friend expr bvmul_no_underflow(expr const& a, expr const& b);
1390 
1391  expr rotate_left(unsigned i) const { Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
1392  expr rotate_right(unsigned i) const { Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
1393  expr repeat(unsigned i) const { Z3_ast r = Z3_mk_repeat(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
1394 
1395  friend expr bvredor(expr const & a);
1396  friend expr bvredand(expr const & a);
1397 
1398  friend expr abs(expr const & a);
1399  friend expr sqrt(expr const & a, expr const & rm);
1400  friend expr fp_eq(expr const & a, expr const & b);
1401 
1402  friend expr operator~(expr const & a);
1403  expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }
1404  expr bit2bool(unsigned i) const { Z3_ast r = Z3_mk_bit2bool(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
1405  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)); }
1406  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)); }
1407 
1411  friend expr fma(expr const& a, expr const& b, expr const& c, expr const& rm);
1412 
1416  friend expr fpa_fp(expr const& sgn, expr const& exp, expr const& sig);
1417 
1421  friend expr fpa_to_sbv(expr const& t, unsigned sz);
1422 
1426  friend expr fpa_to_ubv(expr const& t, unsigned sz);
1427 
1431  friend expr sbv_to_fpa(expr const& t, sort s);
1432 
1436  friend expr ubv_to_fpa(expr const& t, sort s);
1437 
1441  friend expr fpa_to_fpa(expr const& t, sort s);
1442 
1446  friend expr round_fpa_to_closest_integer(expr const& t);
1447 
1453  expr extract(expr const& offset, expr const& length) const {
1454  check_context(*this, offset); check_context(offset, length);
1455  Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
1456  }
1457  expr replace(expr const& src, expr const& dst) const {
1458  check_context(*this, src); check_context(src, dst);
1459  Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
1460  check_error();
1461  return expr(ctx(), r);
1462  }
1463  expr unit() const {
1464  Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
1465  check_error();
1466  return expr(ctx(), r);
1467  }
1468  expr contains(expr const& s) const {
1469  check_context(*this, s);
1470  Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
1471  check_error();
1472  return expr(ctx(), r);
1473  }
1474  expr at(expr const& index) const {
1475  check_context(*this, index);
1476  Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
1477  check_error();
1478  return expr(ctx(), r);
1479  }
1480  expr nth(expr const& index) const {
1481  check_context(*this, index);
1482  Z3_ast r = Z3_mk_seq_nth(ctx(), *this, index);
1483  check_error();
1484  return expr(ctx(), r);
1485  }
1486  expr length() const {
1487  Z3_ast r = Z3_mk_seq_length(ctx(), *this);
1488  check_error();
1489  return expr(ctx(), r);
1490  }
1491  expr stoi() const {
1492  Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
1493  check_error();
1494  return expr(ctx(), r);
1495  }
1496  expr itos() const {
1497  Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
1498  check_error();
1499  return expr(ctx(), r);
1500  }
1501  expr ubvtos() const {
1502  Z3_ast r = Z3_mk_ubv_to_str(ctx(), *this);
1503  check_error();
1504  return expr(ctx(), r);
1505  }
1506  expr sbvtos() const {
1507  Z3_ast r = Z3_mk_sbv_to_str(ctx(), *this);
1508  check_error();
1509  return expr(ctx(), r);
1510  }
1511  expr char_to_int() const {
1512  Z3_ast r = Z3_mk_char_to_int(ctx(), *this);
1513  check_error();
1514  return expr(ctx(), r);
1515  }
1516  expr char_to_bv() const {
1517  Z3_ast r = Z3_mk_char_to_bv(ctx(), *this);
1518  check_error();
1519  return expr(ctx(), r);
1520  }
1521  expr char_from_bv() const {
1522  Z3_ast r = Z3_mk_char_from_bv(ctx(), *this);
1523  check_error();
1524  return expr(ctx(), r);
1525  }
1526  expr is_digit() const {
1527  Z3_ast r = Z3_mk_char_is_digit(ctx(), *this);
1528  check_error();
1529  return expr(ctx(), r);
1530  }
1531 
1532  friend expr range(expr const& lo, expr const& hi);
1536  expr loop(unsigned lo) {
1537  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0);
1538  check_error();
1539  return expr(ctx(), r);
1540  }
1541  expr loop(unsigned lo, unsigned hi) {
1542  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi);
1543  check_error();
1544  return expr(ctx(), r);
1545  }
1546 
1550  expr operator[](expr const& index) const {
1551  assert(is_array() || is_seq());
1552  if (is_array()) {
1553  return select(*this, index);
1554  }
1555  return nth(index);
1556  }
1557 
1558  expr operator[](expr_vector const& index) const {
1559  return select(*this, index);
1560  }
1561 
1565  expr simplify() const { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
1569  expr simplify(params const & p) const { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
1570 
1574  expr substitute(expr_vector const& src, expr_vector const& dst);
1575 
1579  expr substitute(expr_vector const& dst);
1580 
1584  expr substitute(func_decl_vector const& funs, expr_vector const& bodies);
1585 
1586 
1587  class iterator {
1588  expr& e;
1589  unsigned i;
1590  public:
1591  iterator(expr& e, unsigned i): e(e), i(i) {}
1592  bool operator==(iterator const& other) noexcept {
1593  return i == other.i;
1594  }
1595  bool operator!=(iterator const& other) noexcept {
1596  return i != other.i;
1597  }
1598  expr operator*() const { return e.arg(i); }
1599  iterator& operator++() { ++i; return *this; }
1600  iterator operator++(int) { assert(false); return *this; }
1601  };
1602 
1603  iterator begin() { return iterator(*this, 0); }
1604  iterator end() { return iterator(*this, is_app() ? num_args() : 0); }
1605 
1606  };
1607 
1608 #define _Z3_MK_BIN_(a, b, binop) \
1609  check_context(a, b); \
1610  Z3_ast r = binop(a.ctx(), a, b); \
1611  a.check_error(); \
1612  return expr(a.ctx(), r); \
1613 
1614 
1615  inline expr implies(expr const & a, expr const & b) {
1616  assert(a.is_bool() && b.is_bool());
1617  _Z3_MK_BIN_(a, b, Z3_mk_implies);
1618  }
1619  inline expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); }
1620  inline expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); }
1621 
1622 
1623  inline expr pw(expr const & a, expr const & b) { _Z3_MK_BIN_(a, b, Z3_mk_power); }
1624  inline expr pw(expr const & a, int b) { return pw(a, a.ctx().num_val(b, a.get_sort())); }
1625  inline expr pw(int a, expr const & b) { return pw(b.ctx().num_val(a, b.get_sort()), b); }
1626 
1627  inline expr mod(expr const& a, expr const& b) {
1628  if (a.is_bv()) {
1629  _Z3_MK_BIN_(a, b, Z3_mk_bvsmod);
1630  }
1631  else {
1632  _Z3_MK_BIN_(a, b, Z3_mk_mod);
1633  }
1634  }
1635  inline expr mod(expr const & a, int b) { return mod(a, a.ctx().num_val(b, a.get_sort())); }
1636  inline expr mod(int a, expr const & b) { return mod(b.ctx().num_val(a, b.get_sort()), b); }
1637 
1638  inline expr operator%(expr const& a, expr const& b) { return mod(a, b); }
1639  inline expr operator%(expr const& a, int b) { return mod(a, b); }
1640  inline expr operator%(int a, expr const& b) { return mod(a, b); }
1641 
1642 
1643  inline expr rem(expr const& a, expr const& b) {
1644  if (a.is_fpa() && b.is_fpa()) {
1645  _Z3_MK_BIN_(a, b, Z3_mk_fpa_rem);
1646  } else {
1647  _Z3_MK_BIN_(a, b, Z3_mk_rem);
1648  }
1649  }
1650  inline expr rem(expr const & a, int b) { return rem(a, a.ctx().num_val(b, a.get_sort())); }
1651  inline expr rem(int a, expr const & b) { return rem(b.ctx().num_val(a, b.get_sort()), b); }
1652 
1653 #undef _Z3_MK_BIN_
1654 
1655 #define _Z3_MK_UN_(a, mkun) \
1656  Z3_ast r = mkun(a.ctx(), a); \
1657  a.check_error(); \
1658  return expr(a.ctx(), r); \
1659 
1660 
1661  inline expr operator!(expr const & a) { assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); }
1662 
1663  inline expr is_int(expr const& e) { _Z3_MK_UN_(e, Z3_mk_is_int); }
1664 
1665 #undef _Z3_MK_UN_
1666 
1667  inline expr operator&&(expr const & a, expr const & b) {
1668  check_context(a, b);
1669  assert(a.is_bool() && b.is_bool());
1670  Z3_ast args[2] = { a, b };
1671  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1672  a.check_error();
1673  return expr(a.ctx(), r);
1674  }
1675 
1676  inline expr operator&&(expr const & a, bool b) { return a && a.ctx().bool_val(b); }
1677  inline expr operator&&(bool a, expr const & b) { return b.ctx().bool_val(a) && b; }
1678 
1679  inline expr operator||(expr const & a, expr const & b) {
1680  check_context(a, b);
1681  assert(a.is_bool() && b.is_bool());
1682  Z3_ast args[2] = { a, b };
1683  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1684  a.check_error();
1685  return expr(a.ctx(), r);
1686  }
1687 
1688  inline expr operator||(expr const & a, bool b) { return a || a.ctx().bool_val(b); }
1689 
1690  inline expr operator||(bool a, expr const & b) { return b.ctx().bool_val(a) || b; }
1691 
1692  inline expr operator==(expr const & a, expr const & b) {
1693  check_context(a, b);
1694  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1695  a.check_error();
1696  return expr(a.ctx(), r);
1697  }
1698  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()); }
1699  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; }
1700  inline expr operator==(expr const & a, double b) { assert(a.is_fpa()); return a == a.ctx().fpa_val(b); }
1701  inline expr operator==(double a, expr const & b) { assert(b.is_fpa()); return b.ctx().fpa_val(a) == b; }
1702 
1703  inline expr operator!=(expr const & a, expr const & b) {
1704  check_context(a, b);
1705  Z3_ast args[2] = { a, b };
1706  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1707  a.check_error();
1708  return expr(a.ctx(), r);
1709  }
1710  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()); }
1711  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; }
1712  inline expr operator!=(expr const & a, double b) { assert(a.is_fpa()); return a != a.ctx().fpa_val(b); }
1713  inline expr operator!=(double a, expr const & b) { assert(b.is_fpa()); return b.ctx().fpa_val(a) != b; }
1714 
1715  inline expr operator+(expr const & a, expr const & b) {
1716  check_context(a, b);
1717  Z3_ast r = 0;
1718  if (a.is_arith() && b.is_arith()) {
1719  Z3_ast args[2] = { a, b };
1720  r = Z3_mk_add(a.ctx(), 2, args);
1721  }
1722  else if (a.is_bv() && b.is_bv()) {
1723  r = Z3_mk_bvadd(a.ctx(), a, b);
1724  }
1725  else if (a.is_seq() && b.is_seq()) {
1726  return concat(a, b);
1727  }
1728  else if (a.is_re() && b.is_re()) {
1729  Z3_ast _args[2] = { a, b };
1730  r = Z3_mk_re_union(a.ctx(), 2, _args);
1731  }
1732  else if (a.is_fpa() && b.is_fpa()) {
1733  r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1734  }
1735  else {
1736  // operator is not supported by given arguments.
1737  assert(false);
1738  }
1739  a.check_error();
1740  return expr(a.ctx(), r);
1741  }
1742  inline expr operator+(expr const & a, int b) { return a + a.ctx().num_val(b, a.get_sort()); }
1743  inline expr operator+(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) + b; }
1744 
1745  inline expr operator*(expr const & a, expr const & b) {
1746  check_context(a, b);
1747  Z3_ast r = 0;
1748  if (a.is_arith() && b.is_arith()) {
1749  Z3_ast args[2] = { a, b };
1750  r = Z3_mk_mul(a.ctx(), 2, args);
1751  }
1752  else if (a.is_bv() && b.is_bv()) {
1753  r = Z3_mk_bvmul(a.ctx(), a, b);
1754  }
1755  else if (a.is_fpa() && b.is_fpa()) {
1756  r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1757  }
1758  else {
1759  // operator is not supported by given arguments.
1760  assert(false);
1761  }
1762  a.check_error();
1763  return expr(a.ctx(), r);
1764  }
1765  inline expr operator*(expr const & a, int b) { return a * a.ctx().num_val(b, a.get_sort()); }
1766  inline expr operator*(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) * b; }
1767 
1768 
1769  inline expr operator>=(expr const & a, expr const & b) {
1770  check_context(a, b);
1771  Z3_ast r = 0;
1772  if (a.is_arith() && b.is_arith()) {
1773  r = Z3_mk_ge(a.ctx(), a, b);
1774  }
1775  else if (a.is_bv() && b.is_bv()) {
1776  r = Z3_mk_bvsge(a.ctx(), a, b);
1777  }
1778  else if (a.is_fpa() && b.is_fpa()) {
1779  r = Z3_mk_fpa_geq(a.ctx(), a, b);
1780  }
1781  else {
1782  // operator is not supported by given arguments.
1783  assert(false);
1784  }
1785  a.check_error();
1786  return expr(a.ctx(), r);
1787  }
1788 
1789  inline expr operator/(expr const & a, expr const & b) {
1790  check_context(a, b);
1791  Z3_ast r = 0;
1792  if (a.is_arith() && b.is_arith()) {
1793  r = Z3_mk_div(a.ctx(), a, b);
1794  }
1795  else if (a.is_bv() && b.is_bv()) {
1796  r = Z3_mk_bvsdiv(a.ctx(), a, b);
1797  }
1798  else if (a.is_fpa() && b.is_fpa()) {
1799  r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1800  }
1801  else {
1802  // operator is not supported by given arguments.
1803  assert(false);
1804  }
1805  a.check_error();
1806  return expr(a.ctx(), r);
1807  }
1808  inline expr operator/(expr const & a, int b) { return a / a.ctx().num_val(b, a.get_sort()); }
1809  inline expr operator/(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) / b; }
1810 
1811  inline expr operator-(expr const & a) {
1812  Z3_ast r = 0;
1813  if (a.is_arith()) {
1814  r = Z3_mk_unary_minus(a.ctx(), a);
1815  }
1816  else if (a.is_bv()) {
1817  r = Z3_mk_bvneg(a.ctx(), a);
1818  }
1819  else if (a.is_fpa()) {
1820  r = Z3_mk_fpa_neg(a.ctx(), a);
1821  }
1822  else {
1823  // operator is not supported by given arguments.
1824  assert(false);
1825  }
1826  a.check_error();
1827  return expr(a.ctx(), r);
1828  }
1829 
1830  inline expr operator-(expr const & a, expr const & b) {
1831  check_context(a, b);
1832  Z3_ast r = 0;
1833  if (a.is_arith() && b.is_arith()) {
1834  Z3_ast args[2] = { a, b };
1835  r = Z3_mk_sub(a.ctx(), 2, args);
1836  }
1837  else if (a.is_bv() && b.is_bv()) {
1838  r = Z3_mk_bvsub(a.ctx(), a, b);
1839  }
1840  else if (a.is_fpa() && b.is_fpa()) {
1841  r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1842  }
1843  else {
1844  // operator is not supported by given arguments.
1845  assert(false);
1846  }
1847  a.check_error();
1848  return expr(a.ctx(), r);
1849  }
1850  inline expr operator-(expr const & a, int b) { return a - a.ctx().num_val(b, a.get_sort()); }
1851  inline expr operator-(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) - b; }
1852 
1853  inline expr operator<=(expr const & a, expr const & b) {
1854  check_context(a, b);
1855  Z3_ast r = 0;
1856  if (a.is_arith() && b.is_arith()) {
1857  r = Z3_mk_le(a.ctx(), a, b);
1858  }
1859  else if (a.is_bv() && b.is_bv()) {
1860  r = Z3_mk_bvsle(a.ctx(), a, b);
1861  }
1862  else if (a.is_fpa() && b.is_fpa()) {
1863  r = Z3_mk_fpa_leq(a.ctx(), a, b);
1864  }
1865  else {
1866  // operator is not supported by given arguments.
1867  assert(false);
1868  }
1869  a.check_error();
1870  return expr(a.ctx(), r);
1871  }
1872  inline expr operator<=(expr const & a, int b) { return a <= a.ctx().num_val(b, a.get_sort()); }
1873  inline expr operator<=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) <= b; }
1874 
1875  inline expr operator>=(expr const & a, int b) { return a >= a.ctx().num_val(b, a.get_sort()); }
1876  inline expr operator>=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) >= b; }
1877 
1878  inline expr operator<(expr const & a, expr const & b) {
1879  check_context(a, b);
1880  Z3_ast r = 0;
1881  if (a.is_arith() && b.is_arith()) {
1882  r = Z3_mk_lt(a.ctx(), a, b);
1883  }
1884  else if (a.is_bv() && b.is_bv()) {
1885  r = Z3_mk_bvslt(a.ctx(), a, b);
1886  }
1887  else if (a.is_fpa() && b.is_fpa()) {
1888  r = Z3_mk_fpa_lt(a.ctx(), a, b);
1889  }
1890  else {
1891  // operator is not supported by given arguments.
1892  assert(false);
1893  }
1894  a.check_error();
1895  return expr(a.ctx(), r);
1896  }
1897  inline expr operator<(expr const & a, int b) { return a < a.ctx().num_val(b, a.get_sort()); }
1898  inline expr operator<(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) < b; }
1899 
1900  inline expr operator>(expr const & a, expr const & b) {
1901  check_context(a, b);
1902  Z3_ast r = 0;
1903  if (a.is_arith() && b.is_arith()) {
1904  r = Z3_mk_gt(a.ctx(), a, b);
1905  }
1906  else if (a.is_bv() && b.is_bv()) {
1907  r = Z3_mk_bvsgt(a.ctx(), a, b);
1908  }
1909  else if (a.is_fpa() && b.is_fpa()) {
1910  r = Z3_mk_fpa_gt(a.ctx(), a, b);
1911  }
1912  else {
1913  // operator is not supported by given arguments.
1914  assert(false);
1915  }
1916  a.check_error();
1917  return expr(a.ctx(), r);
1918  }
1919  inline expr operator>(expr const & a, int b) { return a > a.ctx().num_val(b, a.get_sort()); }
1920  inline expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > b; }
1921 
1922  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); a.check_error(); return expr(a.ctx(), r); }
1923  inline expr operator&(expr const & a, int b) { return a & a.ctx().num_val(b, a.get_sort()); }
1924  inline expr operator&(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) & b; }
1925 
1926  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); a.check_error(); return expr(a.ctx(), r); }
1927  inline expr operator^(expr const & a, int b) { return a ^ a.ctx().num_val(b, a.get_sort()); }
1928  inline expr operator^(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) ^ b; }
1929 
1930  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); a.check_error(); return expr(a.ctx(), r); }
1931  inline expr operator|(expr const & a, int b) { return a | a.ctx().num_val(b, a.get_sort()); }
1932  inline expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; }
1933 
1934  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); a.check_error(); return expr(a.ctx(), r); }
1935  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); a.check_error(); return expr(a.ctx(), r); }
1936  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); a.check_error(); return expr(a.ctx(), r); }
1937  inline expr min(expr const& a, expr const& b) {
1938  check_context(a, b);
1939  Z3_ast r;
1940  if (a.is_arith()) {
1941  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
1942  }
1943  else if (a.is_bv()) {
1944  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
1945  }
1946  else {
1947  assert(a.is_fpa());
1948  r = Z3_mk_fpa_min(a.ctx(), a, b);
1949  }
1950  a.check_error();
1951  return expr(a.ctx(), r);
1952  }
1953  inline expr max(expr const& a, expr const& b) {
1954  check_context(a, b);
1955  Z3_ast r;
1956  if (a.is_arith()) {
1957  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
1958  }
1959  else if (a.is_bv()) {
1960  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
1961  }
1962  else {
1963  assert(a.is_fpa());
1964  r = Z3_mk_fpa_max(a.ctx(), a, b);
1965  }
1966  a.check_error();
1967  return expr(a.ctx(), r);
1968  }
1969  inline expr bvredor(expr const & a) {
1970  assert(a.is_bv());
1971  Z3_ast r = Z3_mk_bvredor(a.ctx(), a);
1972  a.check_error();
1973  return expr(a.ctx(), r);
1974  }
1975  inline expr bvredand(expr const & a) {
1976  assert(a.is_bv());
1977  Z3_ast r = Z3_mk_bvredand(a.ctx(), a);
1978  a.check_error();
1979  return expr(a.ctx(), r);
1980  }
1981  inline expr abs(expr const & a) {
1982  Z3_ast r;
1983  if (a.is_int()) {
1984  expr zero = a.ctx().int_val(0);
1985  expr ge = a >= zero;
1986  expr na = -a;
1987  r = Z3_mk_ite(a.ctx(), ge, a, na);
1988  }
1989  else if (a.is_real()) {
1990  expr zero = a.ctx().real_val(0);
1991  expr ge = a >= zero;
1992  expr na = -a;
1993  r = Z3_mk_ite(a.ctx(), ge, a, na);
1994  }
1995  else {
1996  r = Z3_mk_fpa_abs(a.ctx(), a);
1997  }
1998  a.check_error();
1999  return expr(a.ctx(), r);
2000  }
2001  inline expr sqrt(expr const & a, expr const& rm) {
2002  check_context(a, rm);
2003  assert(a.is_fpa());
2004  Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
2005  a.check_error();
2006  return expr(a.ctx(), r);
2007  }
2008  inline expr fp_eq(expr const & a, expr const & b) {
2009  check_context(a, b);
2010  assert(a.is_fpa());
2011  Z3_ast r = Z3_mk_fpa_eq(a.ctx(), a, b);
2012  a.check_error();
2013  return expr(a.ctx(), r);
2014  }
2015  inline expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
2016 
2017  inline expr fma(expr const& a, expr const& b, expr const& c, expr const& rm) {
2018  check_context(a, b); check_context(a, c); check_context(a, rm);
2019  assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
2020  Z3_ast r = Z3_mk_fpa_fma(a.ctx(), rm, a, b, c);
2021  a.check_error();
2022  return expr(a.ctx(), r);
2023  }
2024 
2025  inline expr fpa_fp(expr const& sgn, expr const& exp, expr const& sig) {
2026  check_context(sgn, exp); check_context(exp, sig);
2027  assert(sgn.is_bv() && exp.is_bv() && sig.is_bv());
2028  Z3_ast r = Z3_mk_fpa_fp(sgn.ctx(), sgn, exp, sig);
2029  sgn.check_error();
2030  return expr(sgn.ctx(), r);
2031  }
2032 
2033  inline expr fpa_to_sbv(expr const& t, unsigned sz) {
2034  assert(t.is_fpa());
2035  Z3_ast r = Z3_mk_fpa_to_sbv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
2036  t.check_error();
2037  return expr(t.ctx(), r);
2038  }
2039 
2040  inline expr fpa_to_ubv(expr const& t, unsigned sz) {
2041  assert(t.is_fpa());
2042  Z3_ast r = Z3_mk_fpa_to_ubv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
2043  t.check_error();
2044  return expr(t.ctx(), r);
2045  }
2046 
2047  inline expr sbv_to_fpa(expr const& t, sort s) {
2048  assert(t.is_bv());
2049  Z3_ast r = Z3_mk_fpa_to_fp_signed(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2050  t.check_error();
2051  return expr(t.ctx(), r);
2052  }
2053 
2054  inline expr ubv_to_fpa(expr const& t, sort s) {
2055  assert(t.is_bv());
2057  t.check_error();
2058  return expr(t.ctx(), r);
2059  }
2060 
2061  inline expr fpa_to_fpa(expr const& t, sort s) {
2062  assert(t.is_fpa());
2063  Z3_ast r = Z3_mk_fpa_to_fp_float(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2064  t.check_error();
2065  return expr(t.ctx(), r);
2066  }
2067 
2069  assert(t.is_fpa());
2071  t.check_error();
2072  return expr(t.ctx(), r);
2073  }
2074 
2080  inline expr ite(expr const & c, expr const & t, expr const & e) {
2081  check_context(c, t); check_context(c, e);
2082  assert(c.is_bool());
2083  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
2084  c.check_error();
2085  return expr(c.ctx(), r);
2086  }
2087 
2088 
2093  inline expr to_expr(context & c, Z3_ast a) {
2094  c.check_error();
2095  assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
2096  Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
2097  Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
2099  return expr(c, a);
2100  }
2101 
2102  inline sort to_sort(context & c, Z3_sort s) {
2103  c.check_error();
2104  return sort(c, s);
2105  }
2106 
2108  c.check_error();
2109  return func_decl(c, f);
2110  }
2111 
2115  inline expr sle(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsle(a.ctx(), a, b)); }
2116  inline expr sle(expr const & a, int b) { return sle(a, a.ctx().num_val(b, a.get_sort())); }
2117  inline expr sle(int a, expr const & b) { return sle(b.ctx().num_val(a, b.get_sort()), b); }
2121  inline expr slt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvslt(a.ctx(), a, b)); }
2122  inline expr slt(expr const & a, int b) { return slt(a, a.ctx().num_val(b, a.get_sort())); }
2123  inline expr slt(int a, expr const & b) { return slt(b.ctx().num_val(a, b.get_sort()), b); }
2127  inline expr sge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsge(a.ctx(), a, b)); }
2128  inline expr sge(expr const & a, int b) { return sge(a, a.ctx().num_val(b, a.get_sort())); }
2129  inline expr sge(int a, expr const & b) { return sge(b.ctx().num_val(a, b.get_sort()), b); }
2133  inline expr sgt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsgt(a.ctx(), a, b)); }
2134  inline expr sgt(expr const & a, int b) { return sgt(a, a.ctx().num_val(b, a.get_sort())); }
2135  inline expr sgt(int a, expr const & b) { return sgt(b.ctx().num_val(a, b.get_sort()), b); }
2136 
2137 
2141  inline expr ule(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
2142  inline expr ule(expr const & a, int b) { return ule(a, a.ctx().num_val(b, a.get_sort())); }
2143  inline expr ule(int a, expr const & b) { return ule(b.ctx().num_val(a, b.get_sort()), b); }
2147  inline expr ult(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }
2148  inline expr ult(expr const & a, int b) { return ult(a, a.ctx().num_val(b, a.get_sort())); }
2149  inline expr ult(int a, expr const & b) { return ult(b.ctx().num_val(a, b.get_sort()), b); }
2153  inline expr uge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }
2154  inline expr uge(expr const & a, int b) { return uge(a, a.ctx().num_val(b, a.get_sort())); }
2155  inline expr uge(int a, expr const & b) { return uge(b.ctx().num_val(a, b.get_sort()), b); }
2159  inline expr ugt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
2160  inline expr ugt(expr const & a, int b) { return ugt(a, a.ctx().num_val(b, a.get_sort())); }
2161  inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), b); }
2165  inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
2166  inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); }
2167  inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); }
2168 
2172  inline expr srem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsrem(a.ctx(), a, b)); }
2173  inline expr srem(expr const & a, int b) { return srem(a, a.ctx().num_val(b, a.get_sort())); }
2174  inline expr srem(int a, expr const & b) { return srem(b.ctx().num_val(a, b.get_sort()), b); }
2175 
2179  inline expr smod(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsmod(a.ctx(), a, b)); }
2180  inline expr smod(expr const & a, int b) { return smod(a, a.ctx().num_val(b, a.get_sort())); }
2181  inline expr smod(int a, expr const & b) { return smod(b.ctx().num_val(a, b.get_sort()), b); }
2182 
2186  inline expr urem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvurem(a.ctx(), a, b)); }
2187  inline expr urem(expr const & a, int b) { return urem(a, a.ctx().num_val(b, a.get_sort())); }
2188  inline expr urem(int a, expr const & b) { return urem(b.ctx().num_val(a, b.get_sort()), b); }
2189 
2193  inline expr shl(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvshl(a.ctx(), a, b)); }
2194  inline expr shl(expr const & a, int b) { return shl(a, a.ctx().num_val(b, a.get_sort())); }
2195  inline expr shl(int a, expr const & b) { return shl(b.ctx().num_val(a, b.get_sort()), b); }
2196 
2200  inline expr lshr(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvlshr(a.ctx(), a, b)); }
2201  inline expr lshr(expr const & a, int b) { return lshr(a, a.ctx().num_val(b, a.get_sort())); }
2202  inline expr lshr(int a, expr const & b) { return lshr(b.ctx().num_val(a, b.get_sort()), b); }
2203 
2207  inline expr ashr(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvashr(a.ctx(), a, b)); }
2208  inline expr ashr(expr const & a, int b) { return ashr(a, a.ctx().num_val(b, a.get_sort())); }
2209  inline expr ashr(int a, expr const & b) { return ashr(b.ctx().num_val(a, b.get_sort()), b); }
2210 
2214  inline expr zext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_zero_ext(a.ctx(), i, a)); }
2215 
2219  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); }
2220  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); }
2221 
2225  inline expr bvadd_no_overflow(expr const& a, expr const& b, bool is_signed) {
2226  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);
2227  }
2228  inline expr bvadd_no_underflow(expr const& a, expr const& b) {
2229  check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2230  }
2231  inline expr bvsub_no_overflow(expr const& a, expr const& b) {
2232  check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2233  }
2234  inline expr bvsub_no_underflow(expr const& a, expr const& b, bool is_signed) {
2235  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);
2236  }
2237  inline expr bvsdiv_no_overflow(expr const& a, expr const& b) {
2238  check_context(a, b); Z3_ast r = Z3_mk_bvsdiv_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2239  }
2240  inline expr bvneg_no_overflow(expr const& a) {
2241  Z3_ast r = Z3_mk_bvneg_no_overflow(a.ctx(), a); a.check_error(); return expr(a.ctx(), r);
2242  }
2243  inline expr bvmul_no_overflow(expr const& a, expr const& b, bool is_signed) {
2244  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);
2245  }
2246  inline expr bvmul_no_underflow(expr const& a, expr const& b) {
2247  check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2248  }
2249 
2250 
2254  inline expr sext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_sign_ext(a.ctx(), i, a)); }
2255 
2256  inline func_decl linear_order(sort const& a, unsigned index) {
2257  return to_func_decl(a.ctx(), Z3_mk_linear_order(a.ctx(), a, index));
2258  }
2259  inline func_decl partial_order(sort const& a, unsigned index) {
2260  return to_func_decl(a.ctx(), Z3_mk_partial_order(a.ctx(), a, index));
2261  }
2262  inline func_decl piecewise_linear_order(sort const& a, unsigned index) {
2263  return to_func_decl(a.ctx(), Z3_mk_piecewise_linear_order(a.ctx(), a, index));
2264  }
2265  inline func_decl tree_order(sort const& a, unsigned index) {
2266  return to_func_decl(a.ctx(), Z3_mk_tree_order(a.ctx(), a, index));
2267  }
2268 
2269  template<> class cast_ast<ast> {
2270  public:
2271  ast operator()(context & c, Z3_ast a) { return ast(c, a); }
2272  };
2273 
2274  template<> class cast_ast<expr> {
2275  public:
2277  assert(Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
2278  Z3_get_ast_kind(c, a) == Z3_APP_AST ||
2280  Z3_get_ast_kind(c, a) == Z3_VAR_AST);
2281  return expr(c, a);
2282  }
2283  };
2284 
2285  template<> class cast_ast<sort> {
2286  public:
2288  assert(Z3_get_ast_kind(c, a) == Z3_SORT_AST);
2289  return sort(c, reinterpret_cast<Z3_sort>(a));
2290  }
2291  };
2292 
2293  template<> class cast_ast<func_decl> {
2294  public:
2296  assert(Z3_get_ast_kind(c, a) == Z3_FUNC_DECL_AST);
2297  return func_decl(c, reinterpret_cast<Z3_func_decl>(a));
2298  }
2299  };
2300 
2301  template<typename T>
2302  template<typename T2>
2303  array<T>::array(ast_vector_tpl<T2> const & v):m_array(new T[v.size()]), m_size(v.size()) {
2304  for (unsigned i = 0; i < m_size; i++) {
2305  m_array[i] = v[i];
2306  }
2307  }
2308 
2309  // Basic functions for creating quantified formulas.
2310  // The C API should be used for creating quantifiers with patterns, weights, many variables, etc.
2311  inline expr forall(expr const & x, expr const & b) {
2312  check_context(x, b);
2313  Z3_app vars[] = {(Z3_app) x};
2314  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2315  }
2316  inline expr forall(expr const & x1, expr const & x2, expr const & b) {
2317  check_context(x1, b); check_context(x2, b);
2318  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2319  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2320  }
2321  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
2322  check_context(x1, b); check_context(x2, b); check_context(x3, b);
2323  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2324  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2325  }
2326  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
2327  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2328  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2329  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2330  }
2331  inline expr forall(expr_vector const & xs, expr const & b) {
2332  array<Z3_app> vars(xs);
2333  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);
2334  }
2335  inline expr exists(expr const & x, expr const & b) {
2336  check_context(x, b);
2337  Z3_app vars[] = {(Z3_app) x};
2338  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2339  }
2340  inline expr exists(expr const & x1, expr const & x2, expr const & b) {
2341  check_context(x1, b); check_context(x2, b);
2342  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2343  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2344  }
2345  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
2346  check_context(x1, b); check_context(x2, b); check_context(x3, b);
2347  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2348  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2349  }
2350  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
2351  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2352  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2353  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2354  }
2355  inline expr exists(expr_vector const & xs, expr const & b) {
2356  array<Z3_app> vars(xs);
2357  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);
2358  }
2359  inline expr lambda(expr const & x, expr const & b) {
2360  check_context(x, b);
2361  Z3_app vars[] = {(Z3_app) x};
2362  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 1, vars, b); b.check_error(); return expr(b.ctx(), r);
2363  }
2364  inline expr lambda(expr const & x1, expr const & x2, expr const & b) {
2365  check_context(x1, b); check_context(x2, b);
2366  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2367  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 2, vars, b); b.check_error(); return expr(b.ctx(), r);
2368  }
2369  inline expr lambda(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
2370  check_context(x1, b); check_context(x2, b); check_context(x3, b);
2371  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2372  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 3, vars, b); b.check_error(); return expr(b.ctx(), r);
2373  }
2374  inline expr lambda(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
2375  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2376  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2377  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 4, vars, b); b.check_error(); return expr(b.ctx(), r);
2378  }
2379  inline expr lambda(expr_vector const & xs, expr const & b) {
2380  array<Z3_app> vars(xs);
2381  Z3_ast r = Z3_mk_lambda_const(b.ctx(), vars.size(), vars.ptr(), b); b.check_error(); return expr(b.ctx(), r);
2382  }
2383 
2384  inline expr pble(expr_vector const& es, int const* coeffs, int bound) {
2385  assert(es.size() > 0);
2386  context& ctx = es[0u].ctx();
2387  array<Z3_ast> _es(es);
2388  Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
2389  ctx.check_error();
2390  return expr(ctx, r);
2391  }
2392  inline expr pbge(expr_vector const& es, int const* coeffs, int bound) {
2393  assert(es.size() > 0);
2394  context& ctx = es[0u].ctx();
2395  array<Z3_ast> _es(es);
2396  Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
2397  ctx.check_error();
2398  return expr(ctx, r);
2399  }
2400  inline expr pbeq(expr_vector const& es, int const* coeffs, int bound) {
2401  assert(es.size() > 0);
2402  context& ctx = es[0u].ctx();
2403  array<Z3_ast> _es(es);
2404  Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
2405  ctx.check_error();
2406  return expr(ctx, r);
2407  }
2408  inline expr atmost(expr_vector const& es, unsigned bound) {
2409  assert(es.size() > 0);
2410  context& ctx = es[0u].ctx();
2411  array<Z3_ast> _es(es);
2412  Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
2413  ctx.check_error();
2414  return expr(ctx, r);
2415  }
2416  inline expr atleast(expr_vector const& es, unsigned bound) {
2417  assert(es.size() > 0);
2418  context& ctx = es[0u].ctx();
2419  array<Z3_ast> _es(es);
2420  Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
2421  ctx.check_error();
2422  return expr(ctx, r);
2423  }
2424  inline expr sum(expr_vector const& args) {
2425  assert(args.size() > 0);
2426  context& ctx = args[0u].ctx();
2427  array<Z3_ast> _args(args);
2428  Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
2429  ctx.check_error();
2430  return expr(ctx, r);
2431  }
2432 
2433  inline expr distinct(expr_vector const& args) {
2434  assert(args.size() > 0);
2435  context& ctx = args[0u].ctx();
2436  array<Z3_ast> _args(args);
2437  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
2438  ctx.check_error();
2439  return expr(ctx, r);
2440  }
2441 
2442  inline expr concat(expr const& a, expr const& b) {
2443  check_context(a, b);
2444  Z3_ast r;
2445  if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
2446  Z3_ast _args[2] = { a, b };
2447  r = Z3_mk_seq_concat(a.ctx(), 2, _args);
2448  }
2449  else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
2450  Z3_ast _args[2] = { a, b };
2451  r = Z3_mk_re_concat(a.ctx(), 2, _args);
2452  }
2453  else {
2454  r = Z3_mk_concat(a.ctx(), a, b);
2455  }
2456  a.ctx().check_error();
2457  return expr(a.ctx(), r);
2458  }
2459 
2460  inline expr concat(expr_vector const& args) {
2461  Z3_ast r;
2462  assert(args.size() > 0);
2463  if (args.size() == 1) {
2464  return args[0u];
2465  }
2466  context& ctx = args[0u].ctx();
2467  array<Z3_ast> _args(args);
2468  if (Z3_is_seq_sort(ctx, args[0u].get_sort())) {
2469  r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
2470  }
2471  else if (Z3_is_re_sort(ctx, args[0u].get_sort())) {
2472  r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
2473  }
2474  else {
2475  r = _args[args.size()-1];
2476  for (unsigned i = args.size()-1; i > 0; ) {
2477  --i;
2478  r = Z3_mk_concat(ctx, _args[i], r);
2479  ctx.check_error();
2480  }
2481  }
2482  ctx.check_error();
2483  return expr(ctx, r);
2484  }
2485 
2486  inline expr mk_or(expr_vector const& args) {
2487  array<Z3_ast> _args(args);
2488  Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2489  args.check_error();
2490  return expr(args.ctx(), r);
2491  }
2492  inline expr mk_and(expr_vector const& args) {
2493  array<Z3_ast> _args(args);
2494  Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2495  args.check_error();
2496  return expr(args.ctx(), r);
2497  }
2498  inline expr mk_xor(expr_vector const& args) {
2499  if (args.empty())
2500  return args.ctx().bool_val(false);
2501  expr r = args[0u];
2502  for (unsigned i = 1; i < args.size(); ++i)
2503  r = r ^ args[i];
2504  return r;
2505  }
2506 
2507 
2508  class func_entry : public object {
2509  Z3_func_entry m_entry;
2510  void init(Z3_func_entry e) {
2511  m_entry = e;
2512  Z3_func_entry_inc_ref(ctx(), m_entry);
2513  }
2514  public:
2515  func_entry(context & c, Z3_func_entry e):object(c) { init(e); }
2516  func_entry(func_entry const & s):object(s) { init(s.m_entry); }
2518  operator Z3_func_entry() const { return m_entry; }
2520  Z3_func_entry_inc_ref(s.ctx(), s.m_entry);
2521  Z3_func_entry_dec_ref(ctx(), m_entry);
2522  object::operator=(s);
2523  m_entry = s.m_entry;
2524  return *this;
2525  }
2526  expr value() const { Z3_ast r = Z3_func_entry_get_value(ctx(), m_entry); check_error(); return expr(ctx(), r); }
2527  unsigned num_args() const { unsigned r = Z3_func_entry_get_num_args(ctx(), m_entry); check_error(); return r; }
2528  expr arg(unsigned i) const { Z3_ast r = Z3_func_entry_get_arg(ctx(), m_entry, i); check_error(); return expr(ctx(), r); }
2529  };
2530 
2531  class func_interp : public object {
2532  Z3_func_interp m_interp;
2533  void init(Z3_func_interp e) {
2534  m_interp = e;
2535  Z3_func_interp_inc_ref(ctx(), m_interp);
2536  }
2537  public:
2538  func_interp(context & c, Z3_func_interp e):object(c) { init(e); }
2539  func_interp(func_interp const & s):object(s) { init(s.m_interp); }
2541  operator Z3_func_interp() const { return m_interp; }
2543  Z3_func_interp_inc_ref(s.ctx(), s.m_interp);
2544  Z3_func_interp_dec_ref(ctx(), m_interp);
2545  object::operator=(s);
2546  m_interp = s.m_interp;
2547  return *this;
2548  }
2549  expr else_value() const { Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), r); }
2550  unsigned num_entries() const { unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }
2551  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); }
2552  void add_entry(expr_vector const& args, expr& value) {
2553  Z3_func_interp_add_entry(ctx(), m_interp, args, value);
2554  check_error();
2555  }
2556  void set_else(expr& value) {
2557  Z3_func_interp_set_else(ctx(), m_interp, value);
2558  check_error();
2559  }
2560  };
2561 
2562  class model : public object {
2563  Z3_model m_model;
2564  void init(Z3_model m) {
2565  m_model = m;
2566  Z3_model_inc_ref(ctx(), m);
2567  }
2568  public:
2569  struct translate {};
2570  model(context & c):object(c) { init(Z3_mk_model(c)); }
2571  model(context & c, Z3_model m):object(c) { init(m); }
2572  model(model const & s):object(s) { init(s.m_model); }
2573  model(model& src, context& dst, translate) : object(dst) { init(Z3_model_translate(src.ctx(), src, dst)); }
2574  ~model() { Z3_model_dec_ref(ctx(), m_model); }
2575  operator Z3_model() const { return m_model; }
2576  model & operator=(model const & s) {
2577  Z3_model_inc_ref(s.ctx(), s.m_model);
2578  Z3_model_dec_ref(ctx(), m_model);
2579  object::operator=(s);
2580  m_model = s.m_model;
2581  return *this;
2582  }
2583 
2584  expr eval(expr const & n, bool model_completion=false) const {
2585  check_context(*this, n);
2586  Z3_ast r = 0;
2587  bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
2588  check_error();
2589  if (status == false && ctx().enable_exceptions())
2590  Z3_THROW(exception("failed to evaluate expression"));
2591  return expr(ctx(), r);
2592  }
2593 
2594  unsigned num_consts() const { return Z3_model_get_num_consts(ctx(), m_model); }
2595  unsigned num_funcs() const { return Z3_model_get_num_funcs(ctx(), m_model); }
2596  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); }
2597  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); }
2598  unsigned size() const { return num_consts() + num_funcs(); }
2599  func_decl operator[](int i) const {
2600  assert(0 <= i);
2601  return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
2602  }
2603 
2604  // returns interpretation of constant declaration c.
2605  // If c is not assigned any value in the model it returns
2606  // an expression with a null ast reference.
2608  check_context(*this, c);
2609  Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);
2610  check_error();
2611  return expr(ctx(), r);
2612  }
2614  check_context(*this, f);
2615  Z3_func_interp r = Z3_model_get_func_interp(ctx(), m_model, f);
2616  check_error();
2617  return func_interp(ctx(), r);
2618  }
2619 
2620  // returns true iff the model contains an interpretation
2621  // for function f.
2622  bool has_interp(func_decl f) const {
2623  check_context(*this, f);
2624  return Z3_model_has_interp(ctx(), m_model, f);
2625  }
2626 
2628  Z3_func_interp r = Z3_add_func_interp(ctx(), m_model, f, else_val);
2629  check_error();
2630  return func_interp(ctx(), r);
2631  }
2632 
2633  void add_const_interp(func_decl& f, expr& value) {
2634  Z3_add_const_interp(ctx(), m_model, f, value);
2635  check_error();
2636  }
2637 
2638  friend std::ostream & operator<<(std::ostream & out, model const & m);
2639 
2640  std::string to_string() const { return m_model ? std::string(Z3_model_to_string(ctx(), m_model)) : "null"; }
2641  };
2642  inline std::ostream & operator<<(std::ostream & out, model const & m) { return out << m.to_string(); }
2643 
2644  class stats : public object {
2645  Z3_stats m_stats;
2646  void init(Z3_stats e) {
2647  m_stats = e;
2648  Z3_stats_inc_ref(ctx(), m_stats);
2649  }
2650  public:
2651  stats(context & c):object(c), m_stats(0) {}
2652  stats(context & c, Z3_stats e):object(c) { init(e); }
2653  stats(stats const & s):object(s) { init(s.m_stats); }
2654  ~stats() { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); }
2655  operator Z3_stats() const { return m_stats; }
2656  stats & operator=(stats const & s) {
2657  Z3_stats_inc_ref(s.ctx(), s.m_stats);
2658  if (m_stats) Z3_stats_dec_ref(ctx(), m_stats);
2659  object::operator=(s);
2660  m_stats = s.m_stats;
2661  return *this;
2662  }
2663  unsigned size() const { return Z3_stats_size(ctx(), m_stats); }
2664  std::string key(unsigned i) const { Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; }
2665  bool is_uint(unsigned i) const { bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r; }
2666  bool is_double(unsigned i) const { bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r; }
2667  unsigned uint_value(unsigned i) const { unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; }
2668  double double_value(unsigned i) const { double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
2669  friend std::ostream & operator<<(std::ostream & out, stats const & s);
2670  };
2671  inline std::ostream & operator<<(std::ostream & out, stats const & s) { out << Z3_stats_to_string(s.ctx(), s); return out; }
2672 
2673 
2674  inline std::ostream & operator<<(std::ostream & out, check_result r) {
2675  if (r == unsat) out << "unsat";
2676  else if (r == sat) out << "sat";
2677  else out << "unknown";
2678  return out;
2679  }
2680 
2681 
2682  class solver : public object {
2683  Z3_solver m_solver;
2684  void init(Z3_solver s) {
2685  m_solver = s;
2686  if (s)
2687  Z3_solver_inc_ref(ctx(), s);
2688  }
2689  public:
2690  struct simple {};
2691  struct translate {};
2692  solver(context & c):object(c) { init(Z3_mk_solver(c)); check_error(); }
2694  solver(context & c, Z3_solver s):object(c) { init(s); }
2695  solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); check_error(); }
2696  solver(context & c, solver const& src, translate): object(c) { Z3_solver s = Z3_solver_translate(src.ctx(), src, c); check_error(); init(s); }
2697  solver(solver const & s):object(s) { init(s.m_solver); }
2698  ~solver() { Z3_solver_dec_ref(ctx(), m_solver); }
2699  operator Z3_solver() const { return m_solver; }
2700  solver & operator=(solver const & s) {
2701  Z3_solver_inc_ref(s.ctx(), s.m_solver);
2702  Z3_solver_dec_ref(ctx(), m_solver);
2703  object::operator=(s);
2704  m_solver = s.m_solver;
2705  return *this;
2706  }
2707  void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
2708  void set(char const * k, bool v) { params p(ctx()); p.set(k, v); set(p); }
2709  void set(char const * k, unsigned v) { params p(ctx()); p.set(k, v); set(p); }
2710  void set(char const * k, double v) { params p(ctx()); p.set(k, v); set(p); }
2711  void set(char const * k, symbol const & v) { params p(ctx()); p.set(k, v); set(p); }
2712  void set(char const * k, char const* v) { params p(ctx()); p.set(k, v); set(p); }
2713  void push() { Z3_solver_push(ctx(), m_solver); check_error(); }
2714  void pop(unsigned n = 1) { Z3_solver_pop(ctx(), m_solver, n); check_error(); }
2715  void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); }
2716  void add(expr const & e) { assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); }
2717  void add(expr const & e, expr const & p) {
2718  assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
2719  Z3_solver_assert_and_track(ctx(), m_solver, e, p);
2720  check_error();
2721  }
2722  void add(expr const & e, char const * p) {
2723  add(e, ctx().bool_const(p));
2724  }
2725  void add(expr_vector const& v) {
2726  check_context(*this, v);
2727  for (unsigned i = 0; i < v.size(); ++i)
2728  add(v[i]);
2729  }
2730  void from_file(char const* file) { Z3_solver_from_file(ctx(), m_solver, file); ctx().check_parser_error(); }
2731  void from_string(char const* s) { Z3_solver_from_string(ctx(), m_solver, s); ctx().check_parser_error(); }
2732 
2734  check_result check(unsigned n, expr * const assumptions) {
2735  array<Z3_ast> _assumptions(n);
2736  for (unsigned i = 0; i < n; i++) {
2737  check_context(*this, assumptions[i]);
2738  _assumptions[i] = assumptions[i];
2739  }
2740  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
2741  check_error();
2742  return to_check_result(r);
2743  }
2744  check_result check(expr_vector const& assumptions) {
2745  unsigned n = assumptions.size();
2746  array<Z3_ast> _assumptions(n);
2747  for (unsigned i = 0; i < n; i++) {
2748  check_context(*this, assumptions[i]);
2749  _assumptions[i] = assumptions[i];
2750  }
2751  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
2752  check_error();
2753  return to_check_result(r);
2754  }
2755  model get_model() const { Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }
2757  Z3_lbool r = Z3_solver_get_consequences(ctx(), m_solver, assumptions, vars, conseq);
2758  check_error();
2759  return to_check_result(r);
2760  }
2761  std::string reason_unknown() const { Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }
2762  stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }
2766  expr_vector units() const { Z3_ast_vector r = Z3_solver_get_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2767  expr_vector trail() const { Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2769  Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver);
2770  check_error();
2771  expr_vector result(ctx(), r);
2772  unsigned sz = result.size();
2773  levels.resize(sz);
2774  Z3_solver_get_levels(ctx(), m_solver, r, sz, levels.ptr());
2775  check_error();
2776  return result;
2777  }
2778  expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
2779  friend std::ostream & operator<<(std::ostream & out, solver const & s);
2780 
2781  std::string to_smt2(char const* status = "unknown") {
2782  array<Z3_ast> es(assertions());
2783  Z3_ast const* fmls = es.ptr();
2784  Z3_ast fml = 0;
2785  unsigned sz = es.size();
2786  if (sz > 0) {
2787  --sz;
2788  fml = fmls[sz];
2789  }
2790  else {
2791  fml = ctx().bool_val(true);
2792  }
2793  return std::string(Z3_benchmark_to_smtlib_string(
2794  ctx(),
2795  "", "", status, "",
2796  sz,
2797  fmls,
2798  fml));
2799  }
2800 
2801  std::string dimacs(bool include_names = true) const { return std::string(Z3_solver_to_dimacs_string(ctx(), m_solver, include_names)); }
2802 
2804 
2805 
2806  expr_vector cube(expr_vector& vars, unsigned cutoff) {
2807  Z3_ast_vector r = Z3_solver_cube(ctx(), m_solver, vars, cutoff);
2808  check_error();
2809  return expr_vector(ctx(), r);
2810  }
2811 
2813  solver& m_solver;
2814  unsigned& m_cutoff;
2815  expr_vector& m_vars;
2816  expr_vector m_cube;
2817  bool m_end;
2818  bool m_empty;
2819 
2820  void inc() {
2821  assert(!m_end && !m_empty);
2822  m_cube = m_solver.cube(m_vars, m_cutoff);
2823  m_cutoff = 0xFFFFFFFF;
2824  if (m_cube.size() == 1 && m_cube[0u].is_false()) {
2825  m_cube = z3::expr_vector(m_solver.ctx());
2826  m_end = true;
2827  }
2828  else if (m_cube.empty()) {
2829  m_empty = true;
2830  }
2831  }
2832  public:
2833  cube_iterator(solver& s, expr_vector& vars, unsigned& cutoff, bool end):
2834  m_solver(s),
2835  m_cutoff(cutoff),
2836  m_vars(vars),
2837  m_cube(s.ctx()),
2838  m_end(end),
2839  m_empty(false) {
2840  if (!m_end) {
2841  inc();
2842  }
2843  }
2844 
2846  assert(!m_end);
2847  if (m_empty) {
2848  m_end = true;
2849  }
2850  else {
2851  inc();
2852  }
2853  return *this;
2854  }
2855  cube_iterator operator++(int) { assert(false); return *this; }
2856  expr_vector const * operator->() const { return &(operator*()); }
2857  expr_vector const& operator*() const noexcept { return m_cube; }
2858 
2859  bool operator==(cube_iterator const& other) noexcept {
2860  return other.m_end == m_end;
2861  };
2862  bool operator!=(cube_iterator const& other) noexcept {
2863  return other.m_end != m_end;
2864  };
2865 
2866  };
2867 
2869  solver& m_solver;
2870  unsigned m_cutoff;
2871  expr_vector m_default_vars;
2872  expr_vector& m_vars;
2873  public:
2875  m_solver(s),
2876  m_cutoff(0xFFFFFFFF),
2877  m_default_vars(s.ctx()),
2878  m_vars(m_default_vars)
2879  {}
2880 
2882  m_solver(s),
2883  m_cutoff(0xFFFFFFFF),
2884  m_default_vars(s.ctx()),
2885  m_vars(vars)
2886  {}
2887 
2888  cube_iterator begin() { return cube_iterator(m_solver, m_vars, m_cutoff, false); }
2889  cube_iterator end() { return cube_iterator(m_solver, m_vars, m_cutoff, true); }
2890  void set_cutoff(unsigned c) noexcept { m_cutoff = c; }
2891  };
2892 
2893  cube_generator cubes() { return cube_generator(*this); }
2894  cube_generator cubes(expr_vector& vars) { return cube_generator(*this, vars); }
2895 
2896  };
2897  inline std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
2898 
2899  class goal : public object {
2900  Z3_goal m_goal;
2901  void init(Z3_goal s) {
2902  m_goal = s;
2903  Z3_goal_inc_ref(ctx(), s);
2904  }
2905  public:
2906  goal(context & c, bool models=true, bool unsat_cores=false, bool proofs=false):object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); }
2907  goal(context & c, Z3_goal s):object(c) { init(s); }
2908  goal(goal const & s):object(s) { init(s.m_goal); }
2909  ~goal() { Z3_goal_dec_ref(ctx(), m_goal); }
2910  operator Z3_goal() const { return m_goal; }
2911  goal & operator=(goal const & s) {
2912  Z3_goal_inc_ref(s.ctx(), s.m_goal);
2913  Z3_goal_dec_ref(ctx(), m_goal);
2914  object::operator=(s);
2915  m_goal = s.m_goal;
2916  return *this;
2917  }
2918  void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
2919  void add(expr_vector const& v) { check_context(*this, v); for (unsigned i = 0; i < v.size(); ++i) add(v[i]); }
2920  unsigned size() const { return Z3_goal_size(ctx(), m_goal); }
2921  expr operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
2922  Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); }
2923  bool inconsistent() const { return Z3_goal_inconsistent(ctx(), m_goal); }
2924  unsigned depth() const { return Z3_goal_depth(ctx(), m_goal); }
2925  void reset() { Z3_goal_reset(ctx(), m_goal); }
2926  unsigned num_exprs() const { return Z3_goal_num_exprs(ctx(), m_goal); }
2927  bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal); }
2928  bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal); }
2929  model convert_model(model const & m) const {
2930  check_context(*this, m);
2931  Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, m);
2932  check_error();
2933  return model(ctx(), new_m);
2934  }
2935  model get_model() const {
2936  Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, 0);
2937  check_error();
2938  return model(ctx(), new_m);
2939  }
2940  expr as_expr() const {
2941  unsigned n = size();
2942  if (n == 0)
2943  return ctx().bool_val(true);
2944  else if (n == 1)
2945  return operator[](0u);
2946  else {
2947  array<Z3_ast> args(n);
2948  for (unsigned i = 0; i < n; i++)
2949  args[i] = operator[](i);
2950  return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
2951  }
2952  }
2953  std::string dimacs(bool include_names = true) const { return std::string(Z3_goal_to_dimacs_string(ctx(), m_goal, include_names)); }
2954  friend std::ostream & operator<<(std::ostream & out, goal const & g);
2955  };
2956  inline std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; }
2957 
2958  class apply_result : public object {
2959  Z3_apply_result m_apply_result;
2960  void init(Z3_apply_result s) {
2961  m_apply_result = s;
2963  }
2964  public:
2965  apply_result(context & c, Z3_apply_result s):object(c) { init(s); }
2966  apply_result(apply_result const & s):object(s) { init(s.m_apply_result); }
2967  ~apply_result() { Z3_apply_result_dec_ref(ctx(), m_apply_result); }
2968  operator Z3_apply_result() const { return m_apply_result; }
2970  Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result);
2971  Z3_apply_result_dec_ref(ctx(), m_apply_result);
2972  object::operator=(s);
2973  m_apply_result = s.m_apply_result;
2974  return *this;
2975  }
2976  unsigned size() const { return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }
2977  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); }
2978  friend std::ostream & operator<<(std::ostream & out, apply_result const & r);
2979  };
2980  inline std::ostream & operator<<(std::ostream & out, apply_result const & r) { out << Z3_apply_result_to_string(r.ctx(), r); return out; }
2981 
2982  class tactic : public object {
2983  Z3_tactic m_tactic;
2984  void init(Z3_tactic s) {
2985  m_tactic = s;
2986  Z3_tactic_inc_ref(ctx(), s);
2987  }
2988  public:
2989  tactic(context & c, char const * name):object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); }
2990  tactic(context & c, Z3_tactic s):object(c) { init(s); }
2991  tactic(tactic const & s):object(s) { init(s.m_tactic); }
2992  ~tactic() { Z3_tactic_dec_ref(ctx(), m_tactic); }
2993  operator Z3_tactic() const { return m_tactic; }
2994  tactic & operator=(tactic const & s) {
2995  Z3_tactic_inc_ref(s.ctx(), s.m_tactic);
2996  Z3_tactic_dec_ref(ctx(), m_tactic);
2997  object::operator=(s);
2998  m_tactic = s.m_tactic;
2999  return *this;
3000  }
3001  solver mk_solver() const { Z3_solver r = Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error(); return solver(ctx(), r); }
3002  apply_result apply(goal const & g) const {
3003  check_context(*this, g);
3004  Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g);
3005  check_error();
3006  return apply_result(ctx(), r);
3007  }
3008  apply_result operator()(goal const & g) const {
3009  return apply(g);
3010  }
3011  std::string help() const { char const * r = Z3_tactic_get_help(ctx(), m_tactic); check_error(); return r; }
3012  friend tactic operator&(tactic const & t1, tactic const & t2);
3013  friend tactic operator|(tactic const & t1, tactic const & t2);
3014  friend tactic repeat(tactic const & t, unsigned max);
3015  friend tactic with(tactic const & t, params const & p);
3016  friend tactic try_for(tactic const & t, unsigned ms);
3017  friend tactic par_or(unsigned n, tactic const* tactics);
3018  friend tactic par_and_then(tactic const& t1, tactic const& t2);
3020  };
3021 
3022  inline tactic operator&(tactic const & t1, tactic const & t2) {
3023  check_context(t1, t2);
3024  Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
3025  t1.check_error();
3026  return tactic(t1.ctx(), r);
3027  }
3028 
3029  inline tactic operator|(tactic const & t1, tactic const & t2) {
3030  check_context(t1, t2);
3031  Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
3032  t1.check_error();
3033  return tactic(t1.ctx(), r);
3034  }
3035 
3036  inline tactic repeat(tactic const & t, unsigned max=UINT_MAX) {
3037  Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
3038  t.check_error();
3039  return tactic(t.ctx(), r);
3040  }
3041 
3042  inline tactic with(tactic const & t, params const & p) {
3043  Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
3044  t.check_error();
3045  return tactic(t.ctx(), r);
3046  }
3047  inline tactic try_for(tactic const & t, unsigned ms) {
3048  Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
3049  t.check_error();
3050  return tactic(t.ctx(), r);
3051  }
3052  inline tactic par_or(unsigned n, tactic const* tactics) {
3053  if (n == 0) {
3054  Z3_THROW(exception("a non-zero number of tactics need to be passed to par_or"));
3055  }
3056  array<Z3_tactic> buffer(n);
3057  for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
3058  return tactic(tactics[0u].ctx(), Z3_tactic_par_or(tactics[0u].ctx(), n, buffer.ptr()));
3059  }
3060 
3061  inline tactic par_and_then(tactic const & t1, tactic const & t2) {
3062  check_context(t1, t2);
3063  Z3_tactic r = Z3_tactic_par_and_then(t1.ctx(), t1, t2);
3064  t1.check_error();
3065  return tactic(t1.ctx(), r);
3066  }
3067 
3068  class probe : public object {
3069  Z3_probe m_probe;
3070  void init(Z3_probe s) {
3071  m_probe = s;
3072  Z3_probe_inc_ref(ctx(), s);
3073  }
3074  public:
3075  probe(context & c, char const * name):object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); }
3076  probe(context & c, double val):object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); }
3077  probe(context & c, Z3_probe s):object(c) { init(s); }
3078  probe(probe const & s):object(s) { init(s.m_probe); }
3079  ~probe() { Z3_probe_dec_ref(ctx(), m_probe); }
3080  operator Z3_probe() const { return m_probe; }
3081  probe & operator=(probe const & s) {
3082  Z3_probe_inc_ref(s.ctx(), s.m_probe);
3083  Z3_probe_dec_ref(ctx(), m_probe);
3084  object::operator=(s);
3085  m_probe = s.m_probe;
3086  return *this;
3087  }
3088  double apply(goal const & g) const { double r = Z3_probe_apply(ctx(), m_probe, g); check_error(); return r; }
3089  double operator()(goal const & g) const { return apply(g); }
3090  friend probe operator<=(probe const & p1, probe const & p2);
3091  friend probe operator<=(probe const & p1, double p2);
3092  friend probe operator<=(double p1, probe const & p2);
3093  friend probe operator>=(probe const & p1, probe const & p2);
3094  friend probe operator>=(probe const & p1, double p2);
3095  friend probe operator>=(double p1, probe const & p2);
3096  friend probe operator<(probe const & p1, probe const & p2);
3097  friend probe operator<(probe const & p1, double p2);
3098  friend probe operator<(double p1, probe const & p2);
3099  friend probe operator>(probe const & p1, probe const & p2);
3100  friend probe operator>(probe const & p1, double p2);
3101  friend probe operator>(double p1, probe const & p2);
3102  friend probe operator==(probe const & p1, probe const & p2);
3103  friend probe operator==(probe const & p1, double p2);
3104  friend probe operator==(double p1, probe const & p2);
3105  friend probe operator&&(probe const & p1, probe const & p2);
3106  friend probe operator||(probe const & p1, probe const & p2);
3107  friend probe operator!(probe const & p);
3108  };
3109 
3110  inline probe operator<=(probe const & p1, probe const & p2) {
3111  check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3112  }
3113  inline probe operator<=(probe const & p1, double p2) { return p1 <= probe(p1.ctx(), p2); }
3114  inline probe operator<=(double p1, probe const & p2) { return probe(p2.ctx(), p1) <= p2; }
3115  inline probe operator>=(probe const & p1, probe const & p2) {
3116  check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3117  }
3118  inline probe operator>=(probe const & p1, double p2) { return p1 >= probe(p1.ctx(), p2); }
3119  inline probe operator>=(double p1, probe const & p2) { return probe(p2.ctx(), p1) >= p2; }
3120  inline probe operator<(probe const & p1, probe const & p2) {
3121  check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3122  }
3123  inline probe operator<(probe const & p1, double p2) { return p1 < probe(p1.ctx(), p2); }
3124  inline probe operator<(double p1, probe const & p2) { return probe(p2.ctx(), p1) < p2; }
3125  inline probe operator>(probe const & p1, probe const & p2) {
3126  check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3127  }
3128  inline probe operator>(probe const & p1, double p2) { return p1 > probe(p1.ctx(), p2); }
3129  inline probe operator>(double p1, probe const & p2) { return probe(p2.ctx(), p1) > p2; }
3130  inline probe operator==(probe const & p1, probe const & p2) {
3131  check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3132  }
3133  inline probe operator==(probe const & p1, double p2) { return p1 == probe(p1.ctx(), p2); }
3134  inline probe operator==(double p1, probe const & p2) { return probe(p2.ctx(), p1) == p2; }
3135  inline probe operator&&(probe const & p1, probe const & p2) {
3136  check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3137  }
3138  inline probe operator||(probe const & p1, probe const & p2) {
3139  check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3140  }
3141  inline probe operator!(probe const & p) {
3142  Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
3143  }
3144 
3145  class optimize : public object {
3146  Z3_optimize m_opt;
3147 
3148  public:
3149  class handle final {
3150  unsigned m_h;
3151  public:
3152  handle(unsigned h): m_h(h) {}
3153  unsigned h() const { return m_h; }
3154  };
3155  optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }
3156  optimize(optimize const & o):object(o), m_opt(o.m_opt) {
3157  Z3_optimize_inc_ref(o.ctx(), o.m_opt);
3158  }
3160  m_opt = Z3_mk_optimize(c);
3161  Z3_optimize_inc_ref(c, m_opt);
3162  add(expr_vector(c, src.assertions()));
3163  expr_vector v(c, src.objectives());
3164  for (expr_vector::iterator it = v.begin(); it != v.end(); ++it) minimize(*it);
3165  }
3167  Z3_optimize_inc_ref(o.ctx(), o.m_opt);
3168  Z3_optimize_dec_ref(ctx(), m_opt);
3169  m_opt = o.m_opt;
3170  object::operator=(o);
3171  return *this;
3172  }
3174  operator Z3_optimize() const { return m_opt; }
3175  void add(expr const& e) {
3176  assert(e.is_bool());
3177  Z3_optimize_assert(ctx(), m_opt, e);
3178  }
3179  void add(expr_vector const& es) {
3180  for (expr_vector::iterator it = es.begin(); it != es.end(); ++it) add(*it);
3181  }
3182  void add(expr const& e, expr const& t) {
3183  assert(e.is_bool());
3184  Z3_optimize_assert_and_track(ctx(), m_opt, e, t);
3185  }
3186  void add(expr const& e, char const* p) {
3187  assert(e.is_bool());
3188  add(e, ctx().bool_const(p));
3189  }
3190  handle add_soft(expr const& e, unsigned weight) {
3191  assert(e.is_bool());
3192  auto str = std::to_string(weight);
3193  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, str.c_str(), 0));
3194  }
3195  handle add_soft(expr const& e, char const* weight) {
3196  assert(e.is_bool());
3197  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0));
3198  }
3199  handle add(expr const& e, unsigned weight) {
3200  return add_soft(e, weight);
3201  }
3202  handle maximize(expr const& e) {
3203  return handle(Z3_optimize_maximize(ctx(), m_opt, e));
3204  }
3205  handle minimize(expr const& e) {
3206  return handle(Z3_optimize_minimize(ctx(), m_opt, e));
3207  }
3208  void push() {
3209  Z3_optimize_push(ctx(), m_opt);
3210  }
3211  void pop() {
3212  Z3_optimize_pop(ctx(), m_opt);
3213  }
3216  unsigned n = asms.size();
3217  array<Z3_ast> _asms(n);
3218  for (unsigned i = 0; i < n; i++) {
3219  check_context(*this, asms[i]);
3220  _asms[i] = asms[i];
3221  }
3222  Z3_lbool r = Z3_optimize_check(ctx(), m_opt, n, _asms.ptr());
3223  check_error();
3224  return to_check_result(r);
3225  }
3226  model get_model() const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }
3228  void set(params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }
3229  expr lower(handle const& h) {
3230  Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());
3231  check_error();
3232  return expr(ctx(), r);
3233  }
3234  expr upper(handle const& h) {
3235  Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h());
3236  check_error();
3237  return expr(ctx(), r);
3238  }
3241  stats statistics() const { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); }
3242  friend std::ostream & operator<<(std::ostream & out, optimize const & s);
3243  void from_file(char const* filename) { Z3_optimize_from_file(ctx(), m_opt, filename); check_error(); }
3244  void from_string(char const* constraints) { Z3_optimize_from_string(ctx(), m_opt, constraints); check_error(); }
3245  std::string help() const { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error(); return r; }
3246  };
3247  inline std::ostream & operator<<(std::ostream & out, optimize const & s) { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }
3248 
3249  class fixedpoint : public object {
3250  Z3_fixedpoint m_fp;
3251  public:
3253  fixedpoint(fixedpoint const & o):object(o), m_fp(o.m_fp) { Z3_fixedpoint_inc_ref(ctx(), m_fp); }
3256  Z3_fixedpoint_inc_ref(o.ctx(), o.m_fp);
3257  Z3_fixedpoint_dec_ref(ctx(), m_fp);
3258  m_fp = o.m_fp;
3259  object::operator=(o);
3260  return *this;
3261  }
3262  operator Z3_fixedpoint() const { return m_fp; }
3263  expr_vector from_string(char const* s) {
3264  Z3_ast_vector r = Z3_fixedpoint_from_string(ctx(), m_fp, s);
3265  check_error();
3266  return expr_vector(ctx(), r);
3267  }
3268  expr_vector from_file(char const* s) {
3269  Z3_ast_vector r = Z3_fixedpoint_from_file(ctx(), m_fp, s);
3270  check_error();
3271  return expr_vector(ctx(), r);
3272  }
3273  void add_rule(expr& rule, symbol const& name) { Z3_fixedpoint_add_rule(ctx(), m_fp, rule, name); check_error(); }
3274  void add_fact(func_decl& f, unsigned * args) { Z3_fixedpoint_add_fact(ctx(), m_fp, f, f.arity(), args); check_error(); }
3277  array<Z3_func_decl> rs(relations);
3278  Z3_lbool r = Z3_fixedpoint_query_relations(ctx(), m_fp, rs.size(), rs.ptr());
3279  check_error();
3280  return to_check_result(r);
3281  }
3282  expr get_answer() { Z3_ast r = Z3_fixedpoint_get_answer(ctx(), m_fp); check_error(); return expr(ctx(), r); }
3283  std::string reason_unknown() { return Z3_fixedpoint_get_reason_unknown(ctx(), m_fp); }
3284  void update_rule(expr& rule, symbol const& name) { Z3_fixedpoint_update_rule(ctx(), m_fp, rule, name); check_error(); }
3285  unsigned get_num_levels(func_decl& p) { unsigned r = Z3_fixedpoint_get_num_levels(ctx(), m_fp, p); check_error(); return r; }
3286  expr get_cover_delta(int level, func_decl& p) {
3287  Z3_ast r = Z3_fixedpoint_get_cover_delta(ctx(), m_fp, level, p);
3288  check_error();
3289  return expr(ctx(), r);
3290  }
3291  void add_cover(int level, func_decl& p, expr& property) { Z3_fixedpoint_add_cover(ctx(), m_fp, level, p, property); check_error(); }
3292  stats statistics() const { Z3_stats r = Z3_fixedpoint_get_statistics(ctx(), m_fp); check_error(); return stats(ctx(), r); }
3296  void set(params const & p) { Z3_fixedpoint_set_params(ctx(), m_fp, p); check_error(); }
3297  std::string help() const { return Z3_fixedpoint_get_help(ctx(), m_fp); }
3299  std::string to_string() { return Z3_fixedpoint_to_string(ctx(), m_fp, 0, 0); }
3300  std::string to_string(expr_vector const& queries) {
3301  array<Z3_ast> qs(queries);
3302  return Z3_fixedpoint_to_string(ctx(), m_fp, qs.size(), qs.ptr());
3303  }
3304  };
3305  inline std::ostream & operator<<(std::ostream & out, fixedpoint const & f) { return out << Z3_fixedpoint_to_string(f.ctx(), f, 0, 0); }
3306 
3307  inline tactic fail_if(probe const & p) {
3308  Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
3309  p.check_error();
3310  return tactic(p.ctx(), r);
3311  }
3312  inline tactic when(probe const & p, tactic const & t) {
3313  check_context(p, t);
3314  Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
3315  t.check_error();
3316  return tactic(t.ctx(), r);
3317  }
3318  inline tactic cond(probe const & p, tactic const & t1, tactic const & t2) {
3319  check_context(p, t1); check_context(p, t2);
3320  Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
3321  t1.check_error();
3322  return tactic(t1.ctx(), r);
3323  }
3324 
3325  inline symbol context::str_symbol(char const * s) { Z3_symbol r = Z3_mk_string_symbol(m_ctx, s); check_error(); return symbol(*this, r); }
3326  inline symbol context::int_symbol(int n) { Z3_symbol r = Z3_mk_int_symbol(m_ctx, n); check_error(); return symbol(*this, r); }
3327 
3328  inline sort context::bool_sort() { Z3_sort s = Z3_mk_bool_sort(m_ctx); check_error(); return sort(*this, s); }
3329  inline sort context::int_sort() { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }
3330  inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
3331  inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
3332  inline sort context::string_sort() { Z3_sort s = Z3_mk_string_sort(m_ctx); check_error(); return sort(*this, s); }
3333  inline sort context::char_sort() { Z3_sort s = Z3_mk_char_sort(m_ctx); check_error(); return sort(*this, s); }
3334  inline sort context::seq_sort(sort& s) { Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); }
3335  inline sort context::re_sort(sort& s) { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
3336  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); }
3337 
3338  template<>
3339  inline sort context::fpa_sort<16>() { return fpa_sort(5, 11); }
3340 
3341  template<>
3342  inline sort context::fpa_sort<32>() { return fpa_sort(8, 24); }
3343 
3344  template<>
3345  inline sort context::fpa_sort<64>() { return fpa_sort(11, 53); }
3346 
3347  template<>
3348  inline sort context::fpa_sort<128>() { return fpa_sort(15, 113); }
3349 
3351 
3352  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); }
3354  array<Z3_sort> dom(d);
3355  Z3_sort s = Z3_mk_array_sort_n(m_ctx, dom.size(), dom.ptr(), r); check_error(); return sort(*this, s);
3356  }
3357  inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
3358  array<Z3_symbol> _enum_names(n);
3359  for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
3360  array<Z3_func_decl> _cs(n);
3361  array<Z3_func_decl> _ts(n);
3362  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3363  sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
3364  check_error();
3365  for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
3366  return s;
3367  }
3368  inline func_decl context::tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs) {
3369  array<Z3_symbol> _names(n);
3370  array<Z3_sort> _sorts(n);
3371  for (unsigned i = 0; i < n; i++) { _names[i] = Z3_mk_string_symbol(*this, names[i]); _sorts[i] = sorts[i]; }
3372  array<Z3_func_decl> _projs(n);
3373  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3374  Z3_func_decl tuple;
3375  sort _ignore_s = to_sort(*this, Z3_mk_tuple_sort(*this, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));
3376  check_error();
3377  for (unsigned i = 0; i < n; i++) { projs.push_back(func_decl(*this, _projs[i])); }
3378  return func_decl(*this, tuple);
3379  }
3380 
3382  context& ctx;
3383  Z3_constructor_list clist;
3384  public:
3385  constructor_list(constructors const& cs);
3387  operator Z3_constructor_list() const { return clist; }
3388  };
3389 
3391  friend class constructor_list;
3392  context& ctx;
3393  std::vector<Z3_constructor> cons;
3394  std::vector<unsigned> num_fields;
3395  public:
3396  constructors(context& ctx): ctx(ctx) {}
3397 
3399  for (auto con : cons)
3400  Z3_del_constructor(ctx, con);
3401  }
3402 
3403  void add(symbol const& name, symbol const& rec, unsigned n, symbol const* names, sort const* fields) {
3404  array<unsigned> sort_refs(n);
3405  array<Z3_sort> sorts(n);
3406  array<Z3_symbol> _names(n);
3407  for (unsigned i = 0; i < n; ++i) sorts[i] = fields[i], _names[i] = names[i];
3408  cons.push_back(Z3_mk_constructor(ctx, name, rec, n, _names.ptr(), sorts.ptr(), sort_refs.ptr()));
3409  num_fields.push_back(n);
3410  }
3411 
3412  Z3_constructor operator[](unsigned i) const { return cons[i]; }
3413 
3414  unsigned size() const { return (unsigned)cons.size(); }
3415 
3416  void query(unsigned i, func_decl& constructor, func_decl& test, func_decl_vector& accs) {
3417  Z3_func_decl _constructor;
3418  Z3_func_decl _test;
3419  array<Z3_func_decl> accessors(num_fields[i]);
3420  accs.resize(0);
3422  cons[i],
3423  num_fields[i],
3424  &_constructor,
3425  &_test,
3426  accessors.ptr());
3427  constructor = func_decl(ctx, _constructor);
3428 
3429  test = func_decl(ctx, _test);
3430  for (unsigned j = 0; j < num_fields[i]; ++j)
3431  accs.push_back(func_decl(ctx, accessors[j]));
3432  }
3433  };
3434 
3435  inline constructor_list::constructor_list(constructors const& cs): ctx(cs.ctx) {
3436  array<Z3_constructor> cons(cs.size());
3437  for (unsigned i = 0; i < cs.size(); ++i)
3438  cons[i] = cs[i];
3439  clist = Z3_mk_constructor_list(ctx, cs.size(), cons.ptr());
3440  }
3441 
3442  inline sort context::datatype(symbol const& name, constructors const& cs) {
3443  array<Z3_constructor> _cs(cs.size());
3444  for (unsigned i = 0; i < cs.size(); ++i) _cs[i] = cs[i];
3445  Z3_sort s = Z3_mk_datatype(*this, name, cs.size(), _cs.ptr());
3446  check_error();
3447  return sort(*this, s);
3448  }
3449 
3451  unsigned n, symbol const* names,
3452  constructor_list *const* cons) {
3453  sort_vector result(*this);
3454  array<Z3_symbol> _names(n);
3455  array<Z3_sort> _sorts(n);
3456  array<Z3_constructor_list> _cons(n);
3457  for (unsigned i = 0; i < n; ++i)
3458  _names[i] = names[i], _cons[i] = *cons[i];
3459  Z3_mk_datatypes(*this, n, _names.ptr(), _sorts.ptr(), _cons.ptr());
3460  for (unsigned i = 0; i < n; ++i)
3461  result.push_back(sort(*this, _sorts[i]));
3462  return result;
3463  }
3464 
3465 
3466  inline sort context::datatype_sort(symbol const& name) {
3467  Z3_sort s = Z3_mk_datatype_sort(*this, name);
3468  check_error();
3469  return sort(*this, s);
3470  }
3471 
3472 
3473  inline sort context::uninterpreted_sort(char const* name) {
3474  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3475  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
3476  }
3478  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
3479  }
3480 
3481  inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3482  array<Z3_sort> args(arity);
3483  for (unsigned i = 0; i < arity; i++) {
3484  check_context(domain[i], range);
3485  args[i] = domain[i];
3486  }
3487  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
3488  check_error();
3489  return func_decl(*this, f);
3490  }
3491 
3492  inline func_decl context::function(char const * name, unsigned arity, sort const * domain, sort const & range) {
3493  return function(range.ctx().str_symbol(name), arity, domain, range);
3494  }
3495 
3496  inline func_decl context::function(symbol const& name, sort_vector const& domain, sort const& range) {
3497  array<Z3_sort> args(domain.size());
3498  for (unsigned i = 0; i < domain.size(); i++) {
3499  check_context(domain[i], range);
3500  args[i] = domain[i];
3501  }
3502  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
3503  check_error();
3504  return func_decl(*this, f);
3505  }
3506 
3507  inline func_decl context::function(char const * name, sort_vector const& domain, sort const& range) {
3508  return function(range.ctx().str_symbol(name), domain, range);
3509  }
3510 
3511 
3512  inline func_decl context::function(char const * name, sort const & domain, sort const & range) {
3513  check_context(domain, range);
3514  Z3_sort args[1] = { domain };
3515  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
3516  check_error();
3517  return func_decl(*this, f);
3518  }
3519 
3520  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & range) {
3522  Z3_sort args[2] = { d1, d2 };
3523  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
3524  check_error();
3525  return func_decl(*this, f);
3526  }
3527 
3528  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
3530  Z3_sort args[3] = { d1, d2, d3 };
3531  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
3532  check_error();
3533  return func_decl(*this, f);
3534  }
3535 
3536  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
3538  Z3_sort args[4] = { d1, d2, d3, d4 };
3539  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
3540  check_error();
3541  return func_decl(*this, f);
3542  }
3543 
3544  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) {
3546  Z3_sort args[5] = { d1, d2, d3, d4, d5 };
3547  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
3548  check_error();
3549  return func_decl(*this, f);
3550  }
3551 
3552  inline func_decl context::recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3553  array<Z3_sort> args(arity);
3554  for (unsigned i = 0; i < arity; i++) {
3555  check_context(domain[i], range);
3556  args[i] = domain[i];
3557  }
3558  Z3_func_decl f = Z3_mk_rec_func_decl(m_ctx, name, arity, args.ptr(), range);
3559  check_error();
3560  return func_decl(*this, f);
3561 
3562  }
3563 
3564  inline func_decl context::recfun(char const * name, unsigned arity, sort const * domain, sort const & range) {
3565  return recfun(str_symbol(name), arity, domain, range);
3566  }
3567 
3568  inline func_decl context::recfun(char const * name, sort const& d1, sort const & range) {
3569  return recfun(str_symbol(name), 1, &d1, range);
3570  }
3571 
3572  inline func_decl context::recfun(char const * name, sort const& d1, sort const& d2, sort const & range) {
3573  sort dom[2] = { d1, d2 };
3574  return recfun(str_symbol(name), 2, dom, range);
3575  }
3576 
3577  inline void context::recdef(func_decl f, expr_vector const& args, expr const& body) {
3578  check_context(f, args); check_context(f, body);
3579  array<Z3_ast> vars(args);
3580  Z3_add_rec_def(f.ctx(), f, vars.size(), vars.ptr(), body);
3581  }
3582 
3583  inline func_decl context::user_propagate_function(symbol const& name, sort_vector const& domain, sort const& range) {
3584  check_context(domain, range);
3585  array<Z3_sort> domain1(domain);
3586  Z3_func_decl f = Z3_solver_propagate_declare(range.ctx(), name, domain1.size(), domain1.ptr(), range);
3587  check_error();
3588  return func_decl(*this, f);
3589  }
3590 
3591  inline expr context::constant(symbol const & name, sort const & s) {
3592  Z3_ast r = Z3_mk_const(m_ctx, name, s);
3593  check_error();
3594  return expr(*this, r);
3595  }
3596  inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); }
3597  inline expr context::variable(unsigned idx, sort const& s) {
3598  Z3_ast r = Z3_mk_bound(m_ctx, idx, s);
3599  check_error();
3600  return expr(*this, r);
3601  }
3602  inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); }
3603  inline expr context::int_const(char const * name) { return constant(name, int_sort()); }
3604  inline expr context::real_const(char const * name) { return constant(name, real_sort()); }
3605  inline expr context::string_const(char const * name) { return constant(name, string_sort()); }
3606  inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); }
3607  inline expr context::fpa_const(char const * name, unsigned ebits, unsigned sbits) { return constant(name, fpa_sort(ebits, sbits)); }
3608 
3609  template<size_t precision>
3610  inline expr context::fpa_const(char const * name) { return constant(name, fpa_sort<precision>()); }
3611 
3612  inline void context::set_rounding_mode(rounding_mode rm) { m_rounding_mode = rm; }
3613 
3615  switch (m_rounding_mode) {
3616  case RNA: return expr(*this, Z3_mk_fpa_rna(m_ctx));
3617  case RNE: return expr(*this, Z3_mk_fpa_rne(m_ctx));
3618  case RTP: return expr(*this, Z3_mk_fpa_rtp(m_ctx));
3619  case RTN: return expr(*this, Z3_mk_fpa_rtn(m_ctx));
3620  case RTZ: return expr(*this, Z3_mk_fpa_rtz(m_ctx));
3621  default: return expr(*this);
3622  }
3623  }
3624 
3625  inline expr context::bool_val(bool b) { return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }
3626 
3627  inline expr context::int_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
3628  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); }
3629  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); }
3630  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); }
3631  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); }
3632 
3633  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); }
3634  inline expr context::real_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
3635  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); }
3636  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); }
3637  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); }
3638  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); }
3639 
3640  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); }
3641  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); }
3642  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); }
3643  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); }
3644  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); }
3645  inline expr context::bv_val(unsigned n, bool const* bits) {
3646  array<bool> _bits(n);
3647  for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
3648  Z3_ast r = Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error(); return expr(*this, r);
3649  }
3650 
3651  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); }
3652  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); }
3653  inline expr context::fpa_nan(sort const & s) { Z3_ast r = Z3_mk_fpa_nan(m_ctx, s); check_error(); return expr(*this, r); }
3654  inline expr context::fpa_inf(sort const & s, bool sgn) { Z3_ast r = Z3_mk_fpa_inf(m_ctx, s, sgn); check_error(); return expr(*this, r); }
3655 
3656  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); }
3657  inline expr context::string_val(char const* s) { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
3658  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); }
3659  inline expr context::string_val(std::u32string const& s) { Z3_ast r = Z3_mk_u32string(m_ctx, (unsigned)s.size(), (unsigned const*)s.c_str()); check_error(); return expr(*this, r); }
3660 
3661  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); }
3662 
3663  inline expr func_decl::operator()(unsigned n, expr const * args) const {
3664  array<Z3_ast> _args(n);
3665  for (unsigned i = 0; i < n; i++) {
3666  check_context(*this, args[i]);
3667  _args[i] = args[i];
3668  }
3669  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
3670  check_error();
3671  return expr(ctx(), r);
3672 
3673  }
3674  inline expr func_decl::operator()(expr_vector const& args) const {
3675  array<Z3_ast> _args(args.size());
3676  for (unsigned i = 0; i < args.size(); i++) {
3677  check_context(*this, args[i]);
3678  _args[i] = args[i];
3679  }
3680  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
3681  check_error();
3682  return expr(ctx(), r);
3683  }
3684  inline expr func_decl::operator()() const {
3685  Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
3686  ctx().check_error();
3687  return expr(ctx(), r);
3688  }
3689  inline expr func_decl::operator()(expr const & a) const {
3690  check_context(*this, a);
3691  Z3_ast args[1] = { a };
3692  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3693  ctx().check_error();
3694  return expr(ctx(), r);
3695  }
3696  inline expr func_decl::operator()(int a) const {
3697  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
3698  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3699  ctx().check_error();
3700  return expr(ctx(), r);
3701  }
3702  inline expr func_decl::operator()(expr const & a1, expr const & a2) const {
3703  check_context(*this, a1);