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