Z3
z3++.h
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4  Thin C++ layer on top of the Z3 C API.
5  Main features:
6  - Smart pointers for all Z3 objects.
7  - Object-Oriented interface.
8  - Operator overloading.
9  - Exceptions for signaling Z3 errors
10 
11  The C API can be used simultaneously with the C++ layer.
12  However, if you use the C API directly, you will have to check the error conditions manually.
13  Of course, you can invoke the method check_error() of the context object.
14 Author:
15 
16  Leonardo (leonardo) 2012-03-28
17 
18 Notes:
19 
20 --*/
21 #pragma once
22 
23 #include<cassert>
24 #include<iostream>
25 #include<string>
26 #include<sstream>
27 #include<memory>
28 #include<vector>
29 #include<z3.h>
30 #include<limits.h>
31 #include<functional>
32 
33 #undef min
34 #undef max
35 
50 namespace z3 {
51 
52  class exception;
53  class config;
54  class context;
55  class symbol;
56  class params;
57  class param_descrs;
58  class ast;
59  class sort;
60  class func_decl;
61  class expr;
62  class solver;
63  class goal;
64  class tactic;
65  class probe;
66  class model;
67  class func_interp;
68  class func_entry;
69  class statistics;
70  class apply_result;
71  template<typename T> class cast_ast;
72  template<typename T> class ast_vector_tpl;
77 
78  inline void set_param(char const * param, char const * value) { Z3_global_param_set(param, value); }
79  inline void set_param(char const * param, bool value) { Z3_global_param_set(param, value ? "true" : "false"); }
80  inline void set_param(char const * param, int value) { auto str = std::to_string(value); Z3_global_param_set(param, str.c_str()); }
82 
86  class exception : public std::exception {
87  std::string m_msg;
88  public:
89  virtual ~exception() throw() {}
90  exception(char const * msg):m_msg(msg) {}
91  char const * msg() const { return m_msg.c_str(); }
92  char const * what() const throw() { return m_msg.c_str(); }
93  friend std::ostream & operator<<(std::ostream & out, exception const & e);
94  };
95  inline std::ostream & operator<<(std::ostream & out, exception const & e) { out << e.msg(); return out; }
96 
97 #if !defined(Z3_THROW)
98 #if __cpp_exceptions || _CPPUNWIND || __EXCEPTIONS
99 #define Z3_THROW(x) throw x
100 #else
101 #define Z3_THROW(x) {}
102 #endif
103 #endif // !defined(Z3_THROW)
104 
108  class config {
109  Z3_config m_cfg;
110  config(config const &) = delete;
111  config & operator=(config const &) = delete;
112  public:
113  config() { m_cfg = Z3_mk_config(); }
114  ~config() { Z3_del_config(m_cfg); }
115  operator Z3_config() const { return m_cfg; }
119  void set(char const * param, char const * value) { Z3_set_param_value(m_cfg, param, value); }
123  void set(char const * param, bool value) { Z3_set_param_value(m_cfg, param, value ? "true" : "false"); }
127  void set(char const * param, int value) {
128  auto str = std::to_string(value);
129  Z3_set_param_value(m_cfg, param, str.c_str());
130  }
131  };
132 
135  };
136 
143  };
144 
146  if (l == Z3_L_TRUE) return sat;
147  else if (l == Z3_L_FALSE) return unsat;
148  return unknown;
149  }
150 
151 
157  class context {
158  private:
159  friend class user_propagator_base;
160  bool m_enable_exceptions;
161  rounding_mode m_rounding_mode;
162  Z3_context m_ctx = nullptr;
163  void init(config & c) {
164  set_context(Z3_mk_context_rc(c));
165  }
166  void set_context(Z3_context ctx) {
167  m_ctx = ctx;
168  m_enable_exceptions = true;
169  m_rounding_mode = RNE;
170  Z3_set_error_handler(m_ctx, 0);
172  }
173 
174 
175  context(context const &) = delete;
176  context & operator=(context const &) = delete;
177 
178  context(Z3_context c) { set_context(c); }
179  void detach() { m_ctx = nullptr; }
180  public:
181  context() { config c; init(c); }
182  context(config & c) { init(c); }
183  ~context() { if (m_ctx) Z3_del_context(m_ctx); }
184  operator Z3_context() const { return m_ctx; }
185 
190  Z3_error_code e = Z3_get_error_code(m_ctx);
191  if (e != Z3_OK && enable_exceptions())
192  Z3_THROW(exception(Z3_get_error_msg(m_ctx, e)));
193  return e;
194  }
195 
196  void check_parser_error() const {
197  check_error();
198  }
199 
207  void set_enable_exceptions(bool f) { m_enable_exceptions = f; }
208 
209  bool enable_exceptions() const { return m_enable_exceptions; }
210 
214  void set(char const * param, char const * value) { Z3_update_param_value(m_ctx, param, value); }
218  void set(char const * param, bool value) { Z3_update_param_value(m_ctx, param, value ? "true" : "false"); }
222  void set(char const * param, int value) {
223  auto str = std::to_string(value);
224  Z3_update_param_value(m_ctx, param, str.c_str());
225  }
226 
231  void interrupt() { Z3_interrupt(m_ctx); }
232 
236  symbol str_symbol(char const * s);
240  symbol int_symbol(int n);
244  sort bool_sort();
248  sort int_sort();
252  sort real_sort();
256  sort bv_sort(unsigned sz);
257 
261  sort char_sort();
265  sort string_sort();
269  sort seq_sort(sort& s);
279  sort array_sort(sort d, sort r);
280  sort array_sort(sort_vector const& d, sort r);
287  sort fpa_sort(unsigned ebits, unsigned sbits);
291  template<size_t precision>
292  sort fpa_sort();
306  sort enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts);
307 
314  func_decl tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs);
315 
319  sort uninterpreted_sort(char const* name);
320  sort uninterpreted_sort(symbol const& name);
321 
322  func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range);
323  func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range);
324  func_decl function(symbol const& name, sort_vector const& domain, sort const& range);
325  func_decl function(char const * name, sort_vector const& domain, sort const& range);
326  func_decl function(char const * name, sort const & domain, sort const & range);
327  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range);
328  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range);
329  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range);
330  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range);
331 
332  func_decl recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range);
333  func_decl recfun(char const * name, unsigned arity, sort const * domain, sort const & range);
334  func_decl recfun(char const * name, sort const & domain, sort const & range);
335  func_decl recfun(char const * name, sort const & d1, sort const & d2, sort const & range);
336 
337  void recdef(func_decl, expr_vector const& args, expr const& body);
338  func_decl user_propagate_function(symbol const& name, sort_vector const& domain, sort const& range);
339 
340  expr constant(symbol const & name, sort const & s);
341  expr constant(char const * name, sort const & s);
342  expr bool_const(char const * name);
343  expr int_const(char const * name);
344  expr real_const(char const * name);
345  expr string_const(char const * name);
346  expr bv_const(char const * name, unsigned sz);
347  expr fpa_const(char const * name, unsigned ebits, unsigned sbits);
348 
349  template<size_t precision>
350  expr fpa_const(char const * name);
351 
353 
354  expr bool_val(bool b);
355 
356  expr int_val(int n);
357  expr int_val(unsigned n);
358  expr int_val(int64_t n);
359  expr int_val(uint64_t n);
360  expr int_val(char const * n);
361 
362  expr real_val(int n, int d);
363  expr real_val(int n);
364  expr real_val(unsigned n);
365  expr real_val(int64_t n);
366  expr real_val(uint64_t n);
367  expr real_val(char const * n);
368 
369  expr bv_val(int n, unsigned sz);
370  expr bv_val(unsigned n, unsigned sz);
371  expr bv_val(int64_t n, unsigned sz);
372  expr bv_val(uint64_t n, unsigned sz);
373  expr bv_val(char const * n, unsigned sz);
374  expr bv_val(unsigned n, bool const* bits);
375 
376  expr fpa_val(double n);
377  expr fpa_val(float n);
378  expr fpa_nan(sort const & s);
379  expr fpa_inf(sort const & s, bool sgn);
380 
381  expr string_val(char const* s);
382  expr string_val(char const* s, unsigned n);
383  expr string_val(std::string const& s);
384  expr string_val(std::u32string const& s);
385 
386  expr num_val(int n, sort const & s);
387 
391  expr_vector parse_string(char const* s);
392  expr_vector parse_file(char const* file);
393 
394  expr_vector parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
395  expr_vector parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
396  };
397 
398 
399  template<typename T>
400  class array {
401  std::unique_ptr<T[]> m_array;
402  unsigned m_size;
403  array(array const &) = delete;
404  array & operator=(array const &) = delete;
405  public:
406  array(unsigned sz):m_array(new T[sz]),m_size(sz) {}
407  template<typename T2>
408  array(ast_vector_tpl<T2> const & v);
409  void resize(unsigned sz) { m_array.reset(new T[sz]); m_size = sz; }
410  unsigned size() const { return m_size; }
411  T & operator[](int i) { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
412  T const & operator[](int i) const { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
413  T const * ptr() const { return m_array.get(); }
414  T * ptr() { return m_array.get(); }
415  };
416 
417  class object {
418  protected:
420  public:
421  object(context & c):m_ctx(&c) {}
422  context & ctx() const { return *m_ctx; }
424  friend void check_context(object const & a, object const & b);
425  };
426  inline void check_context(object const & a, object const & b) { (void)a; (void)b; assert(a.m_ctx == b.m_ctx); }
427 
428  class symbol : public object {
429  Z3_symbol m_sym;
430  public:
431  symbol(context & c, Z3_symbol s):object(c), m_sym(s) {}
432  operator Z3_symbol() const { return m_sym; }
433  Z3_symbol_kind kind() const { return Z3_get_symbol_kind(ctx(), m_sym); }
434  std::string str() const { assert(kind() == Z3_STRING_SYMBOL); return Z3_get_symbol_string(ctx(), m_sym); }
435  int to_int() const { assert(kind() == Z3_INT_SYMBOL); return Z3_get_symbol_int(ctx(), m_sym); }
436  friend std::ostream & operator<<(std::ostream & out, symbol const & s);
437  };
438 
439  inline std::ostream & operator<<(std::ostream & out, symbol const & s) {
440  if (s.kind() == Z3_INT_SYMBOL)
441  out << "k!" << s.to_int();
442  else
443  out << s.str();
444  return out;
445  }
446 
447 
448  class param_descrs : public object {
449  Z3_param_descrs m_descrs;
450  public:
451  param_descrs(context& c, Z3_param_descrs d): object(c), m_descrs(d) { Z3_param_descrs_inc_ref(c, d); }
452  param_descrs(param_descrs const& o): object(o.ctx()), m_descrs(o.m_descrs) { Z3_param_descrs_inc_ref(ctx(), m_descrs); }
454  Z3_param_descrs_inc_ref(o.ctx(), o.m_descrs);
455  Z3_param_descrs_dec_ref(ctx(), m_descrs);
456  m_descrs = o.m_descrs;
457  object::operator=(o);
458  return *this;
459  }
462 
463  unsigned size() { return Z3_param_descrs_size(ctx(), m_descrs); }
464  symbol name(unsigned i) { return symbol(ctx(), Z3_param_descrs_get_name(ctx(), m_descrs, i)); }
465  Z3_param_kind kind(symbol const& s) { return Z3_param_descrs_get_kind(ctx(), m_descrs, s); }
466  std::string documentation(symbol const& s) { char const* r = Z3_param_descrs_get_documentation(ctx(), m_descrs, s); check_error(); return r; }
467  std::string to_string() const { return Z3_param_descrs_to_string(ctx(), m_descrs); }
468  };
469 
470  inline std::ostream& operator<<(std::ostream & out, param_descrs const & d) { return out << d.to_string(); }
471 
472  class params : public object {
473  Z3_params m_params;
474  public:
475  params(context & c):object(c) { m_params = Z3_mk_params(c); Z3_params_inc_ref(ctx(), m_params); }
476  params(params const & s):object(s), m_params(s.m_params) { Z3_params_inc_ref(ctx(), m_params); }
477  ~params() { Z3_params_dec_ref(ctx(), m_params); }
478  operator Z3_params() const { return m_params; }
479  params & operator=(params const & s) {
480  Z3_params_inc_ref(s.ctx(), s.m_params);
481  Z3_params_dec_ref(ctx(), m_params);
482  object::operator=(s);
483  m_params = s.m_params;
484  return *this;
485  }
486  void set(char const * k, bool b) { Z3_params_set_bool(ctx(), m_params, ctx().str_symbol(k), b); }
487  void set(char const * k, unsigned n) { Z3_params_set_uint(ctx(), m_params, ctx().str_symbol(k), n); }
488  void set(char const * k, double n) { Z3_params_set_double(ctx(), m_params, ctx().str_symbol(k), n); }
489  void set(char const * k, symbol const & s) { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), s); }
490  void set(char const * k, char const* s) { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), ctx().str_symbol(s)); }
491  friend std::ostream & operator<<(std::ostream & out, params const & p);
492  };
493 
494  inline std::ostream & operator<<(std::ostream & out, params const & p) {
495  out << Z3_params_to_string(p.ctx(), p); return out;
496  }
497 
498  class ast : public object {
499  protected:
501  public:
502  ast(context & c):object(c), m_ast(0) {}
503  ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
504  ast(ast const & s) :object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
505  ~ast() { if (m_ast) { Z3_dec_ref(*m_ctx, m_ast); } }
506  operator Z3_ast() const { return m_ast; }
507  operator bool() const { return m_ast != 0; }
508  ast & operator=(ast const & s) {
509  Z3_inc_ref(s.ctx(), s.m_ast);
510  if (m_ast)
511  Z3_dec_ref(ctx(), m_ast);
512  object::operator=(s);
513  m_ast = s.m_ast;
514  return *this;
515  }
516  Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }
517  unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }
518  friend std::ostream & operator<<(std::ostream & out, ast const & n);
519  std::string to_string() const { return std::string(Z3_ast_to_string(ctx(), m_ast)); }
520 
521 
525  friend bool eq(ast const & a, ast const & b);
526  };
527  inline std::ostream & operator<<(std::ostream & out, ast const & n) {
528  out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
529  }
530 
531  inline bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b); }
532 
533  template<typename T>
534  class ast_vector_tpl : public object {
535  Z3_ast_vector m_vector;
536  void init(Z3_ast_vector v) { Z3_ast_vector_inc_ref(ctx(), v); m_vector = v; }
537  public:
539  ast_vector_tpl(context & c, Z3_ast_vector v):object(c) { init(v); }
540  ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
541  ast_vector_tpl(context& c, ast_vector_tpl const& src): object(c) { init(Z3_ast_vector_translate(src.ctx(), src, c)); }
542 
543  ~ast_vector_tpl() { Z3_ast_vector_dec_ref(ctx(), m_vector); }
544  operator Z3_ast_vector() const { return m_vector; }
545  unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); }
546  T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
547  void push_back(T const & e) { Z3_ast_vector_push(ctx(), m_vector, e); check_error(); }
548  void resize(unsigned sz) { Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }
549  T back() const { return operator[](size() - 1); }
550  void pop_back() { assert(size() > 0); resize(size() - 1); }
551  bool empty() const { return size() == 0; }
553  Z3_ast_vector_inc_ref(s.ctx(), s.m_vector);
554  Z3_ast_vector_dec_ref(ctx(), m_vector);
555  object::operator=(s);
556  m_vector = s.m_vector;
557  return *this;
558  }
559  ast_vector_tpl& set(unsigned idx, ast& a) {
560  Z3_ast_vector_set(ctx(), m_vector, idx, a);
561  return *this;
562  }
563  /*
564  Disabled pending C++98 build upgrade
565  bool contains(T const& x) const {
566  for (T y : *this) if (eq(x, y)) return true;
567  return false;
568  }
569  */
570 
571  class iterator final {
572  ast_vector_tpl const* m_vector;
573  unsigned m_index;
574  public:
575  iterator(ast_vector_tpl const* v, unsigned i): m_vector(v), m_index(i) {}
576 
577  bool operator==(iterator const& other) const noexcept {
578  return other.m_index == m_index;
579  };
580  bool operator!=(iterator const& other) const noexcept {
581  return other.m_index != m_index;
582  };
583  iterator& operator++() noexcept {
584  ++m_index;
585  return *this;
586  }
587  void set(T& arg) {
588  Z3_ast_vector_set(m_vector->ctx(), *m_vector, m_index, arg);
589  }
590  iterator operator++(int) noexcept { iterator tmp = *this; ++m_index; return tmp; }
591  T * operator->() const { return &(operator*()); }
592  T operator*() const { return (*m_vector)[m_index]; }
593  };
594  iterator begin() const noexcept { return iterator(this, 0); }
595  iterator end() const { return iterator(this, size()); }
596  friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
597  std::string to_string() const { return std::string(Z3_ast_vector_to_string(ctx(), m_vector)); }
598  };
599 
600 
604  class sort : public ast {
605  public:
606  sort(context & c):ast(c) {}
607  sort(context & c, Z3_sort s):ast(c, reinterpret_cast<Z3_ast>(s)) {}
608  sort(context & c, Z3_ast a):ast(c, a) {}
609  operator Z3_sort() const { return reinterpret_cast<Z3_sort>(m_ast); }
610 
614  unsigned id() const { unsigned r = Z3_get_sort_id(ctx(), *this); check_error(); return r; }
615 
619  Z3_sort_kind sort_kind() const { return Z3_get_sort_kind(*m_ctx, *this); }
623  symbol name() const { Z3_symbol s = Z3_get_sort_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
627  bool is_bool() const { return sort_kind() == Z3_BOOL_SORT; }
631  bool is_int() const { return sort_kind() == Z3_INT_SORT; }
635  bool is_real() const { return sort_kind() == Z3_REAL_SORT; }
639  bool is_arith() const { return is_int() || is_real(); }
643  bool is_bv() const { return sort_kind() == Z3_BV_SORT; }
647  bool is_array() const { return sort_kind() == Z3_ARRAY_SORT; }
651  bool is_datatype() const { return sort_kind() == Z3_DATATYPE_SORT; }
655  bool is_relation() const { return sort_kind() == Z3_RELATION_SORT; }
659  bool is_seq() const { return sort_kind() == Z3_SEQ_SORT; }
663  bool is_re() const { return sort_kind() == Z3_RE_SORT; }
667  bool is_finite_domain() const { return sort_kind() == Z3_FINITE_DOMAIN_SORT; }
671  bool is_fpa() const { return sort_kind() == Z3_FLOATING_POINT_SORT; }
672 
678  unsigned bv_size() const { assert(is_bv()); unsigned r = Z3_get_bv_sort_size(ctx(), *this); check_error(); return r; }
679 
680  unsigned fpa_ebits() const { assert(is_fpa()); unsigned r = Z3_fpa_get_ebits(ctx(), *this); check_error(); return r; }
681 
682  unsigned fpa_sbits() const { assert(is_fpa()); unsigned r = Z3_fpa_get_sbits(ctx(), *this); check_error(); return r; }
688  sort array_domain() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_domain(ctx(), *this); check_error(); return sort(ctx(), s); }
694  sort array_range() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_range(ctx(), *this); check_error(); return sort(ctx(), s); }
695 
696  friend std::ostream & operator<<(std::ostream & out, sort const & s) { return out << Z3_sort_to_string(s.ctx(), Z3_sort(s.m_ast)); }
697 
700  };
701 
706  class func_decl : public ast {
707  public:
708  func_decl(context & c):ast(c) {}
709  func_decl(context & c, Z3_func_decl n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
710  operator Z3_func_decl() const { return reinterpret_cast<Z3_func_decl>(m_ast); }
711 
715  unsigned id() const { unsigned r = Z3_get_func_decl_id(ctx(), *this); check_error(); return r; }
716 
717  unsigned arity() const { return Z3_get_arity(ctx(), *this); }
718  sort domain(unsigned i) const { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }
719  sort range() const { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }
720  symbol name() const { Z3_symbol s = Z3_get_decl_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
721  Z3_decl_kind decl_kind() const { return Z3_get_decl_kind(ctx(), *this); }
722 
724  Z3_func_decl tc = Z3_mk_transitive_closure(ctx(), *this); check_error(); return func_decl(ctx(), tc);
725  }
726 
727  bool is_const() const { return arity() == 0; }
728 
729  expr operator()() const;
730  expr operator()(unsigned n, expr const * args) const;
731  expr operator()(expr_vector const& v) const;
732  expr operator()(expr const & a) const;
733  expr operator()(int a) const;
734  expr operator()(expr const & a1, expr const & a2) const;
735  expr operator()(expr const & a1, int a2) const;
736  expr operator()(int a1, expr const & a2) const;
737  expr operator()(expr const & a1, expr const & a2, expr const & a3) const;
738  expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const;
739  expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const;
740 
742 
743  };
744 
748  expr select(expr const & a, expr const& i);
749  expr select(expr const & a, expr_vector const & i);
750 
755  class expr : public ast {
756  public:
757  expr(context & c):ast(c) {}
758  expr(context & c, Z3_ast n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
759 
763  sort get_sort() const { Z3_sort s = Z3_get_sort(*m_ctx, m_ast); check_error(); return sort(*m_ctx, s); }
764 
768  bool is_bool() const { return get_sort().is_bool(); }
772  bool is_int() const { return get_sort().is_int(); }
776  bool is_real() const { return get_sort().is_real(); }
780  bool is_arith() const { return get_sort().is_arith(); }
784  bool is_bv() const { return get_sort().is_bv(); }
788  bool is_array() const { return get_sort().is_array(); }
792  bool is_datatype() const { return get_sort().is_datatype(); }
796  bool is_relation() const { return get_sort().is_relation(); }
800  bool is_seq() const { return get_sort().is_seq(); }
804  bool is_re() const { return get_sort().is_re(); }
805 
814  bool is_finite_domain() const { return get_sort().is_finite_domain(); }
818  bool is_fpa() const { return get_sort().is_fpa(); }
819 
825  bool is_numeral() const { return kind() == Z3_NUMERAL_AST; }
826  bool is_numeral_i64(int64_t& i) const { bool r = Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}
827  bool is_numeral_u64(uint64_t& i) const { bool r = Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}
828  bool is_numeral_i(int& i) const { bool r = Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}
829  bool is_numeral_u(unsigned& i) const { bool r = Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
830  bool is_numeral(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; }
831  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; }
832  bool is_numeral(double& d) const { if (!is_numeral()) return false; d = Z3_get_numeral_double(ctx(), m_ast); check_error(); return true; }
833  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; }
834 
835  double as_double() const { double d = 0; is_numeral(d); return d; }
836  uint64_t as_uint64() const { uint64_t r = 0; is_numeral_u64(r); return r; }
837  int64_t as_int64() const { int64_t r = 0; is_numeral_i64(r); return r; }
838 
839 
843  bool is_app() const { return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
847  bool is_const() const { return is_app() && num_args() == 0; }
851  bool is_quantifier() const { return kind() == Z3_QUANTIFIER_AST; }
852 
856  bool is_forall() const { return Z3_is_quantifier_forall(ctx(), m_ast); }
860  bool is_exists() const { return Z3_is_quantifier_exists(ctx(), m_ast); }
864  bool is_lambda() const { return Z3_is_lambda(ctx(), m_ast); }
869  bool is_var() const { return kind() == Z3_VAR_AST; }
873  bool is_algebraic() const { return Z3_is_algebraic_number(ctx(), m_ast); }
874 
878  bool is_well_sorted() const { bool r = Z3_is_well_sorted(ctx(), m_ast); check_error(); return r; }
879 
883  expr mk_is_inf() const {
884  assert(is_fpa());
886  check_error();
887  return expr(ctx(), r);
888  }
889 
893  expr mk_is_nan() const {
894  assert(is_fpa());
896  check_error();
897  return expr(ctx(), r);
898  }
899 
903  expr mk_is_normal() const {
904  assert(is_fpa());
906  check_error();
907  return expr(ctx(), r);
908  }
909 
914  assert(is_fpa());
916  check_error();
917  return expr(ctx(), r);
918  }
919 
923  expr mk_is_zero() const {
924  assert(is_fpa());
926  check_error();
927  return expr(ctx(), r);
928  }
929 
933  expr mk_to_ieee_bv() const {
934  assert(is_fpa());
936  check_error();
937  return expr(ctx(), r);
938  }
939 
943  expr mk_from_ieee_bv(sort const &s) const {
944  assert(is_bv());
945  Z3_ast r = Z3_mk_fpa_to_fp_bv(ctx(), m_ast, s);
946  check_error();
947  return expr(ctx(), r);
948  }
949 
956  std::string get_decimal_string(int precision) const {
957  assert(is_numeral() || is_algebraic());
958  return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
959  }
960 
964  expr algebraic_lower(unsigned precision) const {
965  assert(is_algebraic());
966  Z3_ast r = Z3_get_algebraic_number_lower(ctx(), m_ast, precision);
967  check_error();
968  return expr(ctx(), r);
969  }
970 
971  expr algebraic_upper(unsigned precision) const {
972  assert(is_algebraic());
973  Z3_ast r = Z3_get_algebraic_number_upper(ctx(), m_ast, precision);
974  check_error();
975  return expr(ctx(), r);
976  }
977 
982  assert(is_algebraic());
984  check_error();
985  return expr_vector(ctx(), r);
986  }
987 
991  unsigned algebraic_i() const {
992  assert(is_algebraic());
993  unsigned i = Z3_algebraic_get_i(ctx(), m_ast);
994  check_error();
995  return i;
996  }
997 
1001  unsigned id() const { unsigned r = Z3_get_ast_id(ctx(), m_ast); check_error(); return r; }
1002 
1013  int get_numeral_int() const {
1014  int result = 0;
1015  if (!is_numeral_i(result)) {
1016  assert(ctx().enable_exceptions());
1017  if (!ctx().enable_exceptions()) return 0;
1018  Z3_THROW(exception("numeral does not fit in machine int"));
1019  }
1020  return result;
1021  }
1022 
1032  unsigned get_numeral_uint() const {
1033  assert(is_numeral());
1034  unsigned result = 0;
1035  if (!is_numeral_u(result)) {
1036  assert(ctx().enable_exceptions());
1037  if (!ctx().enable_exceptions()) return 0;
1038  Z3_THROW(exception("numeral does not fit in machine uint"));
1039  }
1040  return result;
1041  }
1042 
1049  int64_t get_numeral_int64() const {
1050  assert(is_numeral());
1051  int64_t result = 0;
1052  if (!is_numeral_i64(result)) {
1053  assert(ctx().enable_exceptions());
1054  if (!ctx().enable_exceptions()) return 0;
1055  Z3_THROW(exception("numeral does not fit in machine int64_t"));
1056  }
1057  return result;
1058  }
1059 
1066  uint64_t get_numeral_uint64() const {
1067  assert(is_numeral());
1068  uint64_t result = 0;
1069  if (!is_numeral_u64(result)) {
1070  assert(ctx().enable_exceptions());
1071  if (!ctx().enable_exceptions()) return 0;
1072  Z3_THROW(exception("numeral does not fit in machine uint64_t"));
1073  }
1074  return result;
1075  }
1076 
1078  return Z3_get_bool_value(ctx(), m_ast);
1079  }
1080 
1081  expr numerator() const {
1082  assert(is_numeral());
1083  Z3_ast r = Z3_get_numerator(ctx(), m_ast);
1084  check_error();
1085  return expr(ctx(),r);
1086  }
1087 
1088 
1089  expr denominator() const {
1090  assert(is_numeral());
1092  check_error();
1093  return expr(ctx(),r);
1094  }
1095 
1096 
1101  bool is_string_value() const { return Z3_is_string(ctx(), m_ast); }
1102 
1108  std::string get_string() const {
1109  assert(is_string_value());
1110  char const* s = Z3_get_string(ctx(), m_ast);
1111  check_error();
1112  return std::string(s);
1113  }
1114 
1120  std::u32string get_u32string() const {
1121  assert(is_string_value());
1122  unsigned n = Z3_get_string_length(ctx(), m_ast);
1123  std::u32string s;
1124  s.resize(n);
1125  Z3_get_string_contents(ctx(), m_ast, n, (unsigned*)s.data());
1126  return s;
1127  }
1128 
1129  operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
1130 
1137  func_decl decl() const { Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }
1144  unsigned num_args() const { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
1152  expr arg(unsigned i) const { Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }
1159  expr_vector args() const {
1160  expr_vector vec(ctx());
1161  unsigned argCnt = num_args();
1162  for (unsigned i = 0; i < argCnt; i++)
1163  vec.push_back(arg(i));
1164  return vec;
1165  }
1166 
1172  expr body() const { assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
1173 
1179  friend expr operator!(expr const & a);
1180 
1187  friend expr operator&&(expr const & a, expr const & b);
1188 
1189 
1196  friend expr operator&&(expr const & a, bool b);
1203  friend expr operator&&(bool a, expr const & b);
1204 
1211  friend expr operator||(expr const & a, expr const & b);
1218  friend expr operator||(expr const & a, bool b);
1219 
1226  friend expr operator||(bool a, expr const & b);
1227 
1228  friend expr implies(expr const & a, expr const & b);
1229  friend expr implies(expr const & a, bool b);
1230  friend expr implies(bool a, expr const & b);
1231 
1232  friend expr mk_or(expr_vector const& args);
1233  friend expr mk_xor(expr_vector const& args);
1234  friend expr mk_and(expr_vector const& args);
1235 
1236  friend expr ite(expr const & c, expr const & t, expr const & e);
1237 
1238  bool is_true() const { return is_app() && Z3_OP_TRUE == decl().decl_kind(); }
1239  bool is_false() const { return is_app() && Z3_OP_FALSE == decl().decl_kind(); }
1240  bool is_not() const { return is_app() && Z3_OP_NOT == decl().decl_kind(); }
1241  bool is_and() const { return is_app() && Z3_OP_AND == decl().decl_kind(); }
1242  bool is_or() const { return is_app() && Z3_OP_OR == decl().decl_kind(); }
1243  bool is_xor() const { return is_app() && Z3_OP_XOR == decl().decl_kind(); }
1244  bool is_implies() const { return is_app() && Z3_OP_IMPLIES == decl().decl_kind(); }
1245  bool is_eq() const { return is_app() && Z3_OP_EQ == decl().decl_kind(); }
1246  bool is_ite() const { return is_app() && Z3_OP_ITE == decl().decl_kind(); }
1247  bool is_distinct() const { return is_app() && Z3_OP_DISTINCT == decl().decl_kind(); }
1248 
1249  friend expr distinct(expr_vector const& args);
1250  friend expr concat(expr const& a, expr const& b);
1251  friend expr concat(expr_vector const& args);
1252 
1253  friend expr operator==(expr const & a, expr const & b);
1254  friend expr operator==(expr const & a, int b);
1255  friend expr operator==(int a, expr const & b);
1256 
1257  friend expr operator!=(expr const & a, expr const & b);
1258  friend expr operator!=(expr const & a, int b);
1259  friend expr operator!=(int a, expr const & b);
1260 
1261  friend expr operator+(expr const & a, expr const & b);
1262  friend expr operator+(expr const & a, int b);
1263  friend expr operator+(int a, expr const & b);
1264  friend expr sum(expr_vector const& args);
1265 
1266  friend expr operator*(expr const & a, expr const & b);
1267  friend expr operator*(expr const & a, int b);
1268  friend expr operator*(int a, expr const & b);
1269 
1270  /* \brief Power operator */
1271  friend expr pw(expr const & a, expr const & b);
1272  friend expr pw(expr const & a, int b);
1273  friend expr pw(int a, expr const & b);
1274 
1275  /* \brief mod operator */
1276  friend expr mod(expr const& a, expr const& b);
1277  friend expr mod(expr const& a, int b);
1278  friend expr mod(int a, expr const& b);
1279 
1280  /* \brief rem operator */
1281  friend expr rem(expr const& a, expr const& b);
1282  friend expr rem(expr const& a, int b);
1283  friend expr rem(int a, expr const& b);
1284 
1285  friend expr is_int(expr const& e);
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);
1292 
1293  friend expr operator-(expr const & a, expr const & b);
1294  friend expr operator-(expr const & a, int b);
1295  friend expr operator-(int a, expr const & b);
1296 
1297  friend expr operator<=(expr const & a, expr const & b);
1298  friend expr operator<=(expr const & a, int b);
1299  friend expr operator<=(int a, expr const & b);
1300 
1301 
1302  friend expr operator>=(expr const & a, expr const & b);
1303  friend expr operator>=(expr const & a, int b);
1304  friend expr operator>=(int a, expr const & b);
1305 
1306  friend expr operator<(expr const & a, expr const & b);
1307  friend expr operator<(expr const & a, int b);
1308  friend expr operator<(int a, expr const & b);
1309 
1310  friend expr operator>(expr const & a, expr const & b);
1311  friend expr operator>(expr const & a, int b);
1312  friend expr operator>(int a, expr const & b);
1313 
1314  friend expr pble(expr_vector const& es, int const * coeffs, int bound);
1315  friend expr pbge(expr_vector const& es, int const * coeffs, int bound);
1316  friend expr pbeq(expr_vector const& es, int const * coeffs, int bound);
1317  friend expr atmost(expr_vector const& es, unsigned bound);
1318  friend expr atleast(expr_vector const& es, unsigned bound);
1319 
1320  friend expr operator&(expr const & a, expr const & b);
1321  friend expr operator&(expr const & a, int b);
1322  friend expr operator&(int a, expr const & b);
1323 
1324  friend expr operator^(expr const & a, expr const & b);
1325  friend expr operator^(expr const & a, int b);
1326  friend expr operator^(int a, expr const & b);
1327 
1328  friend expr operator|(expr const & a, expr const & b);
1329  friend expr operator|(expr const & a, int b);
1330  friend expr operator|(int a, expr const & b);
1331  friend expr nand(expr const& a, expr const& b);
1332  friend expr nor(expr const& a, expr const& b);
1333  friend expr xnor(expr const& a, expr const& b);
1334 
1335  friend expr min(expr const& a, expr const& b);
1336  friend expr max(expr const& a, expr const& b);
1337 
1338  friend expr bv2int(expr const& a, bool is_signed);
1339  friend expr int2bv(unsigned n, expr const& a);
1340  friend expr bvadd_no_overflow(expr const& a, expr const& b, bool is_signed);
1341  friend expr bvadd_no_underflow(expr const& a, expr const& b);
1342  friend expr bvsub_no_overflow(expr const& a, expr const& b);
1343  friend expr bvsub_no_underflow(expr const& a, expr const& b, bool is_signed);
1344  friend expr bvsdiv_no_overflow(expr const& a, expr const& b);
1345  friend expr bvneg_no_overflow(expr const& a);
1346  friend expr bvmul_no_overflow(expr const& a, expr const& b, bool is_signed);
1347  friend expr bvmul_no_underflow(expr const& a, expr const& b);
1348 
1349  expr rotate_left(unsigned i) const { Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
1350  expr rotate_right(unsigned i) const { Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
1351  expr repeat(unsigned i) const { Z3_ast r = Z3_mk_repeat(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
1352 
1353  friend expr bvredor(expr const & a);
1354  friend expr bvredand(expr const & a);
1355 
1356  friend expr abs(expr const & a);
1357  friend expr sqrt(expr const & a, expr const & rm);
1358  friend expr fp_eq(expr const & a, expr const & b);
1359 
1360  friend expr operator~(expr const & a);
1361  expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }
1362  expr bit2bool(unsigned i) const { Z3_ast r = Z3_mk_bit2bool(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
1363  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)); }
1364  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)); }
1365 
1369  friend expr fma(expr const& a, expr const& b, expr const& c, expr const& rm);
1370 
1374  friend expr fpa_fp(expr const& sgn, expr const& exp, expr const& sig);
1375 
1379  friend expr fpa_to_sbv(expr const& t, unsigned sz);
1380 
1384  friend expr fpa_to_ubv(expr const& t, unsigned sz);
1385 
1389  friend expr sbv_to_fpa(expr const& t, sort s);
1390 
1394  friend expr ubv_to_fpa(expr const& t, sort s);
1395 
1399  friend expr fpa_to_fpa(expr const& t, sort s);
1400 
1404  friend expr round_fpa_to_closest_integer(expr const& t);
1405 
1411  expr extract(expr const& offset, expr const& length) const {
1412  check_context(*this, offset); check_context(offset, length);
1413  Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
1414  }
1415  expr replace(expr const& src, expr const& dst) const {
1416  check_context(*this, src); check_context(src, dst);
1417  Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
1418  check_error();
1419  return expr(ctx(), r);
1420  }
1421  expr unit() const {
1422  Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
1423  check_error();
1424  return expr(ctx(), r);
1425  }
1426  expr contains(expr const& s) const {
1427  check_context(*this, s);
1428  Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
1429  check_error();
1430  return expr(ctx(), r);
1431  }
1432  expr at(expr const& index) const {
1433  check_context(*this, index);
1434  Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
1435  check_error();
1436  return expr(ctx(), r);
1437  }
1438  expr nth(expr const& index) const {
1439  check_context(*this, index);
1440  Z3_ast r = Z3_mk_seq_nth(ctx(), *this, index);
1441  check_error();
1442  return expr(ctx(), r);
1443  }
1444  expr length() const {
1445  Z3_ast r = Z3_mk_seq_length(ctx(), *this);
1446  check_error();
1447  return expr(ctx(), r);
1448  }
1449  expr stoi() const {
1450  Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
1451  check_error();
1452  return expr(ctx(), r);
1453  }
1454  expr itos() const {
1455  Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
1456  check_error();
1457  return expr(ctx(), r);
1458  }
1459  expr ubvtos() const {
1460  Z3_ast r = Z3_mk_ubv_to_str(ctx(), *this);
1461  check_error();
1462  return expr(ctx(), r);
1463  }
1464  expr sbvtos() const {
1465  Z3_ast r = Z3_mk_sbv_to_str(ctx(), *this);
1466  check_error();
1467  return expr(ctx(), r);
1468  }
1469  expr char_to_int() const {
1470  Z3_ast r = Z3_mk_char_to_int(ctx(), *this);
1471  check_error();
1472  return expr(ctx(), r);
1473  }
1474  expr char_to_bv() const {
1475  Z3_ast r = Z3_mk_char_to_bv(ctx(), *this);
1476  check_error();
1477  return expr(ctx(), r);
1478  }
1479  expr char_from_bv() const {
1480  Z3_ast r = Z3_mk_char_from_bv(ctx(), *this);
1481  check_error();
1482  return expr(ctx(), r);
1483  }
1484  expr is_digit() const {
1485  Z3_ast r = Z3_mk_char_is_digit(ctx(), *this);
1486  check_error();
1487  return expr(ctx(), r);
1488  }
1489 
1490  friend expr range(expr const& lo, expr const& hi);
1494  expr loop(unsigned lo) {
1495  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0);
1496  check_error();
1497  return expr(ctx(), r);
1498  }
1499  expr loop(unsigned lo, unsigned hi) {
1500  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi);
1501  check_error();
1502  return expr(ctx(), r);
1503  }
1504 
1508  expr operator[](expr const& index) const {
1509  assert(is_array() || is_seq());
1510  if (is_array()) {
1511  return select(*this, index);
1512  }
1513  return nth(index);
1514  }
1515 
1516  expr operator[](expr_vector const& index) const {
1517  return select(*this, index);
1518  }
1519 
1523  expr simplify() const { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
1527  expr simplify(params const & p) const { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
1528 
1532  expr substitute(expr_vector const& src, expr_vector const& dst);
1533 
1537  expr substitute(expr_vector const& dst);
1538 
1539 
1540  class iterator {
1541  expr& e;
1542  unsigned i;
1543  public:
1544  iterator(expr& e, unsigned i): e(e), i(i) {}
1545  bool operator==(iterator const& other) noexcept {
1546  return i == other.i;
1547  }
1548  bool operator!=(iterator const& other) noexcept {
1549  return i != other.i;
1550  }
1551  expr operator*() const { return e.arg(i); }
1552  iterator& operator++() { ++i; return *this; }
1553  iterator operator++(int) { assert(false); return *this; }
1554  };
1555 
1556  iterator begin() { return iterator(*this, 0); }
1557  iterator end() { return iterator(*this, is_app() ? num_args() : 0); }
1558 
1559  };
1560 
1561 #define _Z3_MK_BIN_(a, b, binop) \
1562  check_context(a, b); \
1563  Z3_ast r = binop(a.ctx(), a, b); \
1564  a.check_error(); \
1565  return expr(a.ctx(), r); \
1566 
1567 
1568  inline expr implies(expr const & a, expr const & b) {
1569  assert(a.is_bool() && b.is_bool());
1570  _Z3_MK_BIN_(a, b, Z3_mk_implies);
1571  }
1572  inline expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); }
1573  inline expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); }
1574 
1575 
1576  inline expr pw(expr const & a, expr const & b) { _Z3_MK_BIN_(a, b, Z3_mk_power); }
1577  inline expr pw(expr const & a, int b) { return pw(a, a.ctx().num_val(b, a.get_sort())); }
1578  inline expr pw(int a, expr const & b) { return pw(b.ctx().num_val(a, b.get_sort()), b); }
1579 
1580  inline expr mod(expr const& a, expr const& b) {
1581  if (a.is_bv()) {
1582  _Z3_MK_BIN_(a, b, Z3_mk_bvsmod);
1583  }
1584  else {
1585  _Z3_MK_BIN_(a, b, Z3_mk_mod);
1586  }
1587  }
1588  inline expr mod(expr const & a, int b) { return mod(a, a.ctx().num_val(b, a.get_sort())); }
1589  inline expr mod(int a, expr const & b) { return mod(b.ctx().num_val(a, b.get_sort()), b); }
1590 
1591  inline expr operator%(expr const& a, expr const& b) { return mod(a, b); }
1592  inline expr operator%(expr const& a, int b) { return mod(a, b); }
1593  inline expr operator%(int a, expr const& b) { return mod(a, b); }
1594 
1595 
1596  inline expr rem(expr const& a, expr const& b) {
1597  if (a.is_fpa() && b.is_fpa()) {
1598  _Z3_MK_BIN_(a, b, Z3_mk_fpa_rem);
1599  } else {
1600  _Z3_MK_BIN_(a, b, Z3_mk_rem);
1601  }
1602  }
1603  inline expr rem(expr const & a, int b) { return rem(a, a.ctx().num_val(b, a.get_sort())); }
1604  inline expr rem(int a, expr const & b) { return rem(b.ctx().num_val(a, b.get_sort()), b); }
1605 
1606 #undef _Z3_MK_BIN_
1607 
1608 #define _Z3_MK_UN_(a, mkun) \
1609  Z3_ast r = mkun(a.ctx(), a); \
1610  a.check_error(); \
1611  return expr(a.ctx(), r); \
1612 
1613 
1614  inline expr operator!(expr const & a) { assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); }
1615 
1616  inline expr is_int(expr const& e) { _Z3_MK_UN_(e, Z3_mk_is_int); }
1617 
1618 #undef _Z3_MK_UN_
1619 
1620  inline expr operator&&(expr const & a, expr const & b) {
1621  check_context(a, b);
1622  assert(a.is_bool() && b.is_bool());
1623  Z3_ast args[2] = { a, b };
1624  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1625  a.check_error();
1626  return expr(a.ctx(), r);
1627  }
1628 
1629  inline expr operator&&(expr const & a, bool b) { return a && a.ctx().bool_val(b); }
1630  inline expr operator&&(bool a, expr const & b) { return b.ctx().bool_val(a) && b; }
1631 
1632  inline expr operator||(expr const & a, expr const & b) {
1633  check_context(a, b);
1634  assert(a.is_bool() && b.is_bool());
1635  Z3_ast args[2] = { a, b };
1636  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1637  a.check_error();
1638  return expr(a.ctx(), r);
1639  }
1640 
1641  inline expr operator||(expr const & a, bool b) { return a || a.ctx().bool_val(b); }
1642 
1643  inline expr operator||(bool a, expr const & b) { return b.ctx().bool_val(a) || b; }
1644 
1645  inline expr operator==(expr const & a, expr const & b) {
1646  check_context(a, b);
1647  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1648  a.check_error();
1649  return expr(a.ctx(), r);
1650  }
1651  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()); }
1652  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; }
1653  inline expr operator==(expr const & a, double b) { assert(a.is_fpa()); return a == a.ctx().fpa_val(b); }
1654  inline expr operator==(double a, expr const & b) { assert(b.is_fpa()); return b.ctx().fpa_val(a) == b; }
1655 
1656  inline expr operator!=(expr const & a, expr const & b) {
1657  check_context(a, b);
1658  Z3_ast args[2] = { a, b };
1659  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1660  a.check_error();
1661  return expr(a.ctx(), r);
1662  }
1663  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()); }
1664  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; }
1665  inline expr operator!=(expr const & a, double b) { assert(a.is_fpa()); return a != a.ctx().fpa_val(b); }
1666  inline expr operator!=(double a, expr const & b) { assert(b.is_fpa()); return b.ctx().fpa_val(a) != b; }
1667 
1668  inline expr operator+(expr const & a, expr const & b) {
1669  check_context(a, b);
1670  Z3_ast r = 0;
1671  if (a.is_arith() && b.is_arith()) {
1672  Z3_ast args[2] = { a, b };
1673  r = Z3_mk_add(a.ctx(), 2, args);
1674  }
1675  else if (a.is_bv() && b.is_bv()) {
1676  r = Z3_mk_bvadd(a.ctx(), a, b);
1677  }
1678  else if (a.is_seq() && b.is_seq()) {
1679  return concat(a, b);
1680  }
1681  else if (a.is_re() && b.is_re()) {
1682  Z3_ast _args[2] = { a, b };
1683  r = Z3_mk_re_union(a.ctx(), 2, _args);
1684  }
1685  else if (a.is_fpa() && b.is_fpa()) {
1686  r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1687  }
1688  else {
1689  // operator is not supported by given arguments.
1690  assert(false);
1691  }
1692  a.check_error();
1693  return expr(a.ctx(), r);
1694  }
1695  inline expr operator+(expr const & a, int b) { return a + a.ctx().num_val(b, a.get_sort()); }
1696  inline expr operator+(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) + b; }
1697 
1698  inline expr operator*(expr const & a, expr const & b) {
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_mul(a.ctx(), 2, args);
1704  }
1705  else if (a.is_bv() && b.is_bv()) {
1706  r = Z3_mk_bvmul(a.ctx(), a, b);
1707  }
1708  else if (a.is_fpa() && b.is_fpa()) {
1709  r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1710  }
1711  else {
1712  // operator is not supported by given arguments.
1713  assert(false);
1714  }
1715  a.check_error();
1716  return expr(a.ctx(), r);
1717  }
1718  inline expr operator*(expr const & a, int b) { return a * a.ctx().num_val(b, a.get_sort()); }
1719  inline expr operator*(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) * b; }
1720 
1721 
1722  inline expr operator>=(expr const & a, expr const & b) {
1723  check_context(a, b);
1724  Z3_ast r = 0;
1725  if (a.is_arith() && b.is_arith()) {
1726  r = Z3_mk_ge(a.ctx(), a, b);
1727  }
1728  else if (a.is_bv() && b.is_bv()) {
1729  r = Z3_mk_bvsge(a.ctx(), a, b);
1730  }
1731  else if (a.is_fpa() && b.is_fpa()) {
1732  r = Z3_mk_fpa_geq(a.ctx(), a, b);
1733  }
1734  else {
1735  // operator is not supported by given arguments.
1736  assert(false);
1737  }
1738  a.check_error();
1739  return expr(a.ctx(), r);
1740  }
1741 
1742  inline expr operator/(expr const & a, expr const & b) {
1743  check_context(a, b);
1744  Z3_ast r = 0;
1745  if (a.is_arith() && b.is_arith()) {
1746  r = Z3_mk_div(a.ctx(), a, b);
1747  }
1748  else if (a.is_bv() && b.is_bv()) {
1749  r = Z3_mk_bvsdiv(a.ctx(), a, b);
1750  }
1751  else if (a.is_fpa() && b.is_fpa()) {
1752  r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1753  }
1754  else {
1755  // operator is not supported by given arguments.
1756  assert(false);
1757  }
1758  a.check_error();
1759  return expr(a.ctx(), r);
1760  }
1761  inline expr operator/(expr const & a, int b) { return a / a.ctx().num_val(b, a.get_sort()); }
1762  inline expr operator/(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) / b; }
1763 
1764  inline expr operator-(expr const & a) {
1765  Z3_ast r = 0;
1766  if (a.is_arith()) {
1767  r = Z3_mk_unary_minus(a.ctx(), a);
1768  }
1769  else if (a.is_bv()) {
1770  r = Z3_mk_bvneg(a.ctx(), a);
1771  }
1772  else if (a.is_fpa()) {
1773  r = Z3_mk_fpa_neg(a.ctx(), a);
1774  }
1775  else {
1776  // operator is not supported by given arguments.
1777  assert(false);
1778  }
1779  a.check_error();
1780  return expr(a.ctx(), r);
1781  }
1782 
1783  inline expr operator-(expr const & a, expr const & b) {
1784  check_context(a, b);
1785  Z3_ast r = 0;
1786  if (a.is_arith() && b.is_arith()) {
1787  Z3_ast args[2] = { a, b };
1788  r = Z3_mk_sub(a.ctx(), 2, args);
1789  }
1790  else if (a.is_bv() && b.is_bv()) {
1791  r = Z3_mk_bvsub(a.ctx(), a, b);
1792  }
1793  else if (a.is_fpa() && b.is_fpa()) {
1794  r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1795  }
1796  else {
1797  // operator is not supported by given arguments.
1798  assert(false);
1799  }
1800  a.check_error();
1801  return expr(a.ctx(), r);
1802  }
1803  inline expr operator-(expr const & a, int b) { return a - a.ctx().num_val(b, a.get_sort()); }
1804  inline expr operator-(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) - b; }
1805 
1806  inline expr operator<=(expr const & a, expr const & b) {
1807  check_context(a, b);
1808  Z3_ast r = 0;
1809  if (a.is_arith() && b.is_arith()) {
1810  r = Z3_mk_le(a.ctx(), a, b);
1811  }
1812  else if (a.is_bv() && b.is_bv()) {
1813  r = Z3_mk_bvsle(a.ctx(), a, b);
1814  }
1815  else if (a.is_fpa() && b.is_fpa()) {
1816  r = Z3_mk_fpa_leq(a.ctx(), a, b);
1817  }
1818  else {
1819  // operator is not supported by given arguments.
1820  assert(false);
1821  }
1822  a.check_error();
1823  return expr(a.ctx(), r);
1824  }
1825  inline expr operator<=(expr const & a, int b) { return a <= a.ctx().num_val(b, a.get_sort()); }
1826  inline expr operator<=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) <= b; }
1827 
1828  inline expr operator>=(expr const & a, int b) { return a >= a.ctx().num_val(b, a.get_sort()); }
1829  inline expr operator>=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) >= b; }
1830 
1831  inline expr operator<(expr const & a, expr const & b) {
1832  check_context(a, b);
1833  Z3_ast r = 0;
1834  if (a.is_arith() && b.is_arith()) {
1835  r = Z3_mk_lt(a.ctx(), a, b);
1836  }
1837  else if (a.is_bv() && b.is_bv()) {
1838  r = Z3_mk_bvslt(a.ctx(), a, b);
1839  }
1840  else if (a.is_fpa() && b.is_fpa()) {
1841  r = Z3_mk_fpa_lt(a.ctx(), a, b);
1842  }
1843  else {
1844  // operator is not supported by given arguments.
1845  assert(false);
1846  }
1847  a.check_error();
1848  return expr(a.ctx(), r);
1849  }
1850  inline expr operator<(expr const & a, int b) { return a < a.ctx().num_val(b, a.get_sort()); }
1851  inline expr operator<(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) < b; }
1852 
1853  inline expr operator>(expr const & a, expr const & b) {
1854  check_context(a, b);
1855  Z3_ast r = 0;
1856  if (a.is_arith() && b.is_arith()) {
1857  r = Z3_mk_gt(a.ctx(), a, b);
1858  }
1859  else if (a.is_bv() && b.is_bv()) {
1860  r = Z3_mk_bvsgt(a.ctx(), a, b);
1861  }
1862  else if (a.is_fpa() && b.is_fpa()) {
1863  r = Z3_mk_fpa_gt(a.ctx(), a, b);
1864  }
1865  else {
1866  // operator is not supported by given arguments.
1867  assert(false);
1868  }
1869  a.check_error();
1870  return expr(a.ctx(), r);
1871  }
1872  inline expr operator>(expr const & a, int b) { return a > a.ctx().num_val(b, a.get_sort()); }
1873  inline expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > b; }
1874 
1875  inline expr operator&(expr const & a, 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); }
1876  inline expr operator&(expr const & a, int b) { return a & a.ctx().num_val(b, a.get_sort()); }
1877  inline expr operator&(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) & b; }
1878 
1879  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); }
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) { 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); }
1884  inline expr operator|(expr const & a, int b) { return a | a.ctx().num_val(b, a.get_sort()); }
1885  inline expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; }
1886 
1887  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); }
1888  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); }
1889  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); }
1890  inline expr min(expr const& a, expr const& b) {
1891  check_context(a, b);
1892  Z3_ast r;
1893  if (a.is_arith()) {
1894  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
1895  }
1896  else if (a.is_bv()) {
1897  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
1898  }
1899  else {
1900  assert(a.is_fpa());
1901  r = Z3_mk_fpa_min(a.ctx(), a, b);
1902  }
1903  return expr(a.ctx(), r);
1904  }
1905  inline expr max(expr const& a, expr const& b) {
1906  check_context(a, b);
1907  Z3_ast r;
1908  if (a.is_arith()) {
1909  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
1910  }
1911  else if (a.is_bv()) {
1912  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
1913  }
1914  else {
1915  assert(a.is_fpa());
1916  r = Z3_mk_fpa_max(a.ctx(), a, b);
1917  }
1918  return expr(a.ctx(), r);
1919  }
1920  inline expr bvredor(expr const & a) {
1921  assert(a.is_bv());
1922  Z3_ast r = Z3_mk_bvredor(a.ctx(), a);
1923  a.check_error();
1924  return expr(a.ctx(), r);
1925  }
1926  inline expr bvredand(expr const & a) {
1927  assert(a.is_bv());
1928  Z3_ast r = Z3_mk_bvredand(a.ctx(), a);
1929  a.check_error();
1930  return expr(a.ctx(), r);
1931  }
1932  inline expr abs(expr const & a) {
1933  Z3_ast r;
1934  if (a.is_int()) {
1935  expr zero = a.ctx().int_val(0);
1936  expr ge = a >= zero;
1937  expr na = -a;
1938  r = Z3_mk_ite(a.ctx(), ge, a, na);
1939  }
1940  else if (a.is_real()) {
1941  expr zero = a.ctx().real_val(0);
1942  expr ge = a >= zero;
1943  expr na = -a;
1944  r = Z3_mk_ite(a.ctx(), ge, a, na);
1945  }
1946  else {
1947  r = Z3_mk_fpa_abs(a.ctx(), a);
1948  }
1949  a.check_error();
1950  return expr(a.ctx(), r);
1951  }
1952  inline expr sqrt(expr const & a, expr const& rm) {
1953  check_context(a, rm);
1954  assert(a.is_fpa());
1955  Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
1956  a.check_error();
1957  return expr(a.ctx(), r);
1958  }
1959  inline expr fp_eq(expr const & a, expr const & b) {
1960  check_context(a, b);
1961  assert(a.is_fpa());
1962  Z3_ast r = Z3_mk_fpa_eq(a.ctx(), a, b);
1963  a.check_error();
1964  return expr(a.ctx(), r);
1965  }
1966  inline expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
1967 
1968  inline expr fma(expr const& a, expr const& b, expr const& c, expr const& rm) {
1969  check_context(a, b); check_context(a, c); check_context(a, rm);
1970  assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
1971  Z3_ast r = Z3_mk_fpa_fma(a.ctx(), rm, a, b, c);
1972  a.check_error();
1973  return expr(a.ctx(), r);
1974  }
1975 
1976  inline expr fpa_fp(expr const& sgn, expr const& exp, expr const& sig) {
1977  check_context(sgn, exp); check_context(exp, sig);
1978  assert(sgn.is_bv() && exp.is_bv() && sig.is_bv());
1979  Z3_ast r = Z3_mk_fpa_fp(sgn.ctx(), sgn, exp, sig);
1980  sgn.check_error();
1981  return expr(sgn.ctx(), r);
1982  }
1983 
1984  inline expr fpa_to_sbv(expr const& t, unsigned sz) {
1985  assert(t.is_fpa());
1986  Z3_ast r = Z3_mk_fpa_to_sbv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
1987  t.check_error();
1988  return expr(t.ctx(), r);
1989  }
1990 
1991  inline expr fpa_to_ubv(expr const& t, unsigned sz) {
1992  assert(t.is_fpa());
1993  Z3_ast r = Z3_mk_fpa_to_ubv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
1994  t.check_error();
1995  return expr(t.ctx(), r);
1996  }
1997 
1998  inline expr sbv_to_fpa(expr const& t, sort s) {
1999  assert(t.is_bv());
2000  Z3_ast r = Z3_mk_fpa_to_fp_signed(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2001  t.check_error();
2002  return expr(t.ctx(), r);
2003  }
2004 
2005  inline expr ubv_to_fpa(expr const& t, sort s) {
2006  assert(t.is_bv());
2008  t.check_error();
2009  return expr(t.ctx(), r);
2010  }
2011 
2012  inline expr fpa_to_fpa(expr const& t, sort s) {
2013  assert(t.is_fpa());
2014  Z3_ast r = Z3_mk_fpa_to_fp_float(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2015  t.check_error();
2016  return expr(t.ctx(), r);
2017  }
2018 
2020  assert(t.is_fpa());
2022  t.check_error();
2023  return expr(t.ctx(), r);
2024  }
2025 
2031  inline expr ite(expr const & c, expr const & t, expr const & e) {
2032  check_context(c, t); check_context(c, e);
2033  assert(c.is_bool());
2034  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
2035  c.check_error();
2036  return expr(c.ctx(), r);
2037  }
2038 
2039 
2044  inline expr to_expr(context & c, Z3_ast a) {
2045  c.check_error();
2046  assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
2047  Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
2048  Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
2050  return expr(c, a);
2051  }
2052 
2053  inline sort to_sort(context & c, Z3_sort s) {
2054  c.check_error();
2055  return sort(c, s);
2056  }
2057 
2059  c.check_error();
2060  return func_decl(c, f);
2061  }
2062 
2066  inline expr sle(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsle(a.ctx(), a, b)); }
2067  inline expr sle(expr const & a, int b) { return sle(a, a.ctx().num_val(b, a.get_sort())); }
2068  inline expr sle(int a, expr const & b) { return sle(b.ctx().num_val(a, b.get_sort()), b); }
2072  inline expr slt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvslt(a.ctx(), a, b)); }
2073  inline expr slt(expr const & a, int b) { return slt(a, a.ctx().num_val(b, a.get_sort())); }
2074  inline expr slt(int a, expr const & b) { return slt(b.ctx().num_val(a, b.get_sort()), b); }
2078  inline expr sge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsge(a.ctx(), a, b)); }
2079  inline expr sge(expr const & a, int b) { return sge(a, a.ctx().num_val(b, a.get_sort())); }
2080  inline expr sge(int a, expr const & b) { return sge(b.ctx().num_val(a, b.get_sort()), b); }
2084  inline expr sgt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsgt(a.ctx(), a, b)); }
2085  inline expr sgt(expr const & a, int b) { return sgt(a, a.ctx().num_val(b, a.get_sort())); }
2086  inline expr sgt(int a, expr const & b) { return sgt(b.ctx().num_val(a, b.get_sort()), b); }
2087 
2088 
2092  inline expr ule(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
2093  inline expr ule(expr const & a, int b) { return ule(a, a.ctx().num_val(b, a.get_sort())); }
2094  inline expr ule(int a, expr const & b) { return ule(b.ctx().num_val(a, b.get_sort()), b); }
2098  inline expr ult(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }
2099  inline expr ult(expr const & a, int b) { return ult(a, a.ctx().num_val(b, a.get_sort())); }
2100  inline expr ult(int a, expr const & b) { return ult(b.ctx().num_val(a, b.get_sort()), b); }
2104  inline expr uge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }
2105  inline expr uge(expr const & a, int b) { return uge(a, a.ctx().num_val(b, a.get_sort())); }
2106  inline expr uge(int a, expr const & b) { return uge(b.ctx().num_val(a, b.get_sort()), b); }
2110  inline expr ugt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
2111  inline expr ugt(expr const & a, int b) { return ugt(a, a.ctx().num_val(b, a.get_sort())); }
2112  inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), b); }
2116  inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
2117  inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); }
2118  inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); }
2119 
2123  inline expr srem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsrem(a.ctx(), a, b)); }
2124  inline expr srem(expr const & a, int b) { return srem(a, a.ctx().num_val(b, a.get_sort())); }
2125  inline expr srem(int a, expr const & b) { return srem(b.ctx().num_val(a, b.get_sort()), b); }
2126 
2130  inline expr smod(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsmod(a.ctx(), a, b)); }
2131  inline expr smod(expr const & a, int b) { return smod(a, a.ctx().num_val(b, a.get_sort())); }
2132  inline expr smod(int a, expr const & b) { return smod(b.ctx().num_val(a, b.get_sort()), b); }
2133 
2137  inline expr urem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvurem(a.ctx(), a, b)); }
2138  inline expr urem(expr const & a, int b) { return urem(a, a.ctx().num_val(b, a.get_sort())); }
2139  inline expr urem(int a, expr const & b) { return urem(b.ctx().num_val(a, b.get_sort()), b); }
2140 
2144  inline expr shl(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvshl(a.ctx(), a, b)); }
2145  inline expr shl(expr const & a, int b) { return shl(a, a.ctx().num_val(b, a.get_sort())); }
2146  inline expr shl(int a, expr const & b) { return shl(b.ctx().num_val(a, b.get_sort()), b); }
2147 
2151  inline expr lshr(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvlshr(a.ctx(), a, b)); }
2152  inline expr lshr(expr const & a, int b) { return lshr(a, a.ctx().num_val(b, a.get_sort())); }
2153  inline expr lshr(int a, expr const & b) { return lshr(b.ctx().num_val(a, b.get_sort()), b); }
2154 
2158  inline expr ashr(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvashr(a.ctx(), a, b)); }
2159  inline expr ashr(expr const & a, int b) { return ashr(a, a.ctx().num_val(b, a.get_sort())); }
2160  inline expr ashr(int a, expr const & b) { return ashr(b.ctx().num_val(a, b.get_sort()), b); }
2161 
2165  inline expr zext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_zero_ext(a.ctx(), i, a)); }
2166 
2170  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); }
2171  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); }
2172 
2176  inline expr bvadd_no_overflow(expr const& a, expr const& b, bool is_signed) {
2177  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);
2178  }
2179  inline expr bvadd_no_underflow(expr const& a, expr const& b) {
2180  check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2181  }
2182  inline expr bvsub_no_overflow(expr const& a, expr const& b) {
2183  check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2184  }
2185  inline expr bvsub_no_underflow(expr const& a, expr const& b, bool is_signed) {
2186  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);
2187  }
2188  inline expr bvsdiv_no_overflow(expr const& a, expr const& b) {
2189  check_context(a, b); Z3_ast r = Z3_mk_bvsdiv_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2190  }
2191  inline expr bvneg_no_overflow(expr const& a) {
2192  Z3_ast r = Z3_mk_bvneg_no_overflow(a.ctx(), a); a.check_error(); return expr(a.ctx(), r);
2193  }
2194  inline expr bvmul_no_overflow(expr const& a, expr const& b, bool is_signed) {
2195  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);
2196  }
2197  inline expr bvmul_no_underflow(expr const& a, expr const& b) {
2198  check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2199  }
2200 
2201 
2205  inline expr sext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_sign_ext(a.ctx(), i, a)); }
2206 
2207  inline func_decl linear_order(sort const& a, unsigned index) {
2208  return to_func_decl(a.ctx(), Z3_mk_linear_order(a.ctx(), a, index));
2209  }
2210  inline func_decl partial_order(sort const& a, unsigned index) {
2211  return to_func_decl(a.ctx(), Z3_mk_partial_order(a.ctx(), a, index));
2212  }
2213  inline func_decl piecewise_linear_order(sort const& a, unsigned index) {
2214  return to_func_decl(a.ctx(), Z3_mk_piecewise_linear_order(a.ctx(), a, index));
2215  }
2216  inline func_decl tree_order(sort const& a, unsigned index) {
2217  return to_func_decl(a.ctx(), Z3_mk_tree_order(a.ctx(), a, index));
2218  }
2219 
2220  template<> class cast_ast<ast> {
2221  public:
2222  ast operator()(context & c, Z3_ast a) { return ast(c, a); }
2223  };
2224 
2225  template<> class cast_ast<expr> {
2226  public:
2228  assert(Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
2229  Z3_get_ast_kind(c, a) == Z3_APP_AST ||
2231  Z3_get_ast_kind(c, a) == Z3_VAR_AST);
2232  return expr(c, a);
2233  }
2234  };
2235 
2236  template<> class cast_ast<sort> {
2237  public:
2239  assert(Z3_get_ast_kind(c, a) == Z3_SORT_AST);
2240  return sort(c, reinterpret_cast<Z3_sort>(a));
2241  }
2242  };
2243 
2244  template<> class cast_ast<func_decl> {
2245  public:
2247  assert(Z3_get_ast_kind(c, a) == Z3_FUNC_DECL_AST);
2248  return func_decl(c, reinterpret_cast<Z3_func_decl>(a));
2249  }
2250  };
2251 
2252  template<typename T>
2253  template<typename T2>
2254  array<T>::array(ast_vector_tpl<T2> const & v):m_array(new T[v.size()]), m_size(v.size()) {
2255  for (unsigned i = 0; i < m_size; i++) {
2256  m_array[i] = v[i];
2257  }
2258  }
2259 
2260  // Basic functions for creating quantified formulas.
2261  // The C API should be used for creating quantifiers with patterns, weights, many variables, etc.
2262  inline expr forall(expr const & x, expr const & b) {
2263  check_context(x, b);
2264  Z3_app vars[] = {(Z3_app) x};
2265  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2266  }
2267  inline expr forall(expr const & x1, expr const & x2, expr const & b) {
2268  check_context(x1, b); check_context(x2, b);
2269  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2270  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2271  }
2272  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
2273  check_context(x1, b); check_context(x2, b); check_context(x3, b);
2274  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2275  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2276  }
2277  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
2278  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2279  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2280  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2281  }
2282  inline expr forall(expr_vector const & xs, expr const & b) {
2283  array<Z3_app> vars(xs);
2284  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);
2285  }
2286  inline expr exists(expr const & x, expr const & b) {
2287  check_context(x, b);
2288  Z3_app vars[] = {(Z3_app) x};
2289  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2290  }
2291  inline expr exists(expr const & x1, expr const & x2, expr const & b) {
2292  check_context(x1, b); check_context(x2, b);
2293  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2294  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2295  }
2296  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
2297  check_context(x1, b); check_context(x2, b); check_context(x3, b);
2298  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2299  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2300  }
2301  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
2302  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2303  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2304  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2305  }
2306  inline expr exists(expr_vector const & xs, expr const & b) {
2307  array<Z3_app> vars(xs);
2308  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);
2309  }
2310  inline expr lambda(expr const & x, expr const & b) {
2311  check_context(x, b);
2312  Z3_app vars[] = {(Z3_app) x};
2313  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 1, vars, b); b.check_error(); return expr(b.ctx(), r);
2314  }
2315  inline expr lambda(expr const & x1, expr const & x2, expr const & b) {
2316  check_context(x1, b); check_context(x2, b);
2317  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2318  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 2, vars, b); b.check_error(); return expr(b.ctx(), r);
2319  }
2320  inline expr lambda(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
2321  check_context(x1, b); check_context(x2, b); check_context(x3, b);
2322  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2323  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 3, vars, b); b.check_error(); return expr(b.ctx(), r);
2324  }
2325  inline expr lambda(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
2326  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2327  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2328  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 4, vars, b); b.check_error(); return expr(b.ctx(), r);
2329  }
2330  inline expr lambda(expr_vector const & xs, expr const & b) {
2331  array<Z3_app> vars(xs);
2332  Z3_ast r = Z3_mk_lambda_const(b.ctx(), vars.size(), vars.ptr(), b); b.check_error(); return expr(b.ctx(), r);
2333  }
2334 
2335  inline expr pble(expr_vector const& es, int const* coeffs, int bound) {
2336  assert(es.size() > 0);
2337  context& ctx = es[0u].ctx();
2338  array<Z3_ast> _es(es);
2339  Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
2340  ctx.check_error();
2341  return expr(ctx, r);
2342  }
2343  inline expr pbge(expr_vector const& es, int const* coeffs, int bound) {
2344  assert(es.size() > 0);
2345  context& ctx = es[0u].ctx();
2346  array<Z3_ast> _es(es);
2347  Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
2348  ctx.check_error();
2349  return expr(ctx, r);
2350  }
2351  inline expr pbeq(expr_vector const& es, int const* coeffs, int bound) {
2352  assert(es.size() > 0);
2353  context& ctx = es[0u].ctx();
2354  array<Z3_ast> _es(es);
2355  Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
2356  ctx.check_error();
2357  return expr(ctx, r);
2358  }
2359  inline expr atmost(expr_vector const& es, unsigned bound) {
2360  assert(es.size() > 0);
2361  context& ctx = es[0u].ctx();
2362  array<Z3_ast> _es(es);
2363  Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
2364  ctx.check_error();
2365  return expr(ctx, r);
2366  }
2367  inline expr atleast(expr_vector const& es, unsigned bound) {
2368  assert(es.size() > 0);
2369  context& ctx = es[0u].ctx();
2370  array<Z3_ast> _es(es);
2371  Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
2372  ctx.check_error();
2373  return expr(ctx, r);
2374  }
2375  inline expr sum(expr_vector const& args) {
2376  assert(args.size() > 0);
2377  context& ctx = args[0u].ctx();
2378  array<Z3_ast> _args(args);
2379  Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
2380  ctx.check_error();
2381  return expr(ctx, r);
2382  }
2383 
2384  inline expr distinct(expr_vector const& args) {
2385  assert(args.size() > 0);
2386  context& ctx = args[0u].ctx();
2387  array<Z3_ast> _args(args);
2388  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
2389  ctx.check_error();
2390  return expr(ctx, r);
2391  }
2392 
2393  inline expr concat(expr const& a, expr const& b) {
2394  check_context(a, b);
2395  Z3_ast r;
2396  if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
2397  Z3_ast _args[2] = { a, b };
2398  r = Z3_mk_seq_concat(a.ctx(), 2, _args);
2399  }
2400  else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
2401  Z3_ast _args[2] = { a, b };
2402  r = Z3_mk_re_concat(a.ctx(), 2, _args);
2403  }
2404  else {
2405  r = Z3_mk_concat(a.ctx(), a, b);
2406  }
2407  a.ctx().check_error();
2408  return expr(a.ctx(), r);
2409  }
2410 
2411  inline expr concat(expr_vector const& args) {
2412  Z3_ast r;
2413  assert(args.size() > 0);
2414  if (args.size() == 1) {
2415  return args[0u];
2416  }
2417  context& ctx = args[0u].ctx();
2418  array<Z3_ast> _args(args);
2419  if (Z3_is_seq_sort(ctx, args[0u].get_sort())) {
2420  r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
2421  }
2422  else if (Z3_is_re_sort(ctx, args[0u].get_sort())) {
2423  r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
2424  }
2425  else {
2426  r = _args[args.size()-1];
2427  for (unsigned i = args.size()-1; i > 0; ) {
2428  --i;
2429  r = Z3_mk_concat(ctx, _args[i], r);
2430  ctx.check_error();
2431  }
2432  }
2433  ctx.check_error();
2434  return expr(ctx, r);
2435  }
2436 
2437  inline expr mk_or(expr_vector const& args) {
2438  array<Z3_ast> _args(args);
2439  Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2440  args.check_error();
2441  return expr(args.ctx(), r);
2442  }
2443  inline expr mk_and(expr_vector const& args) {
2444  array<Z3_ast> _args(args);
2445  Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2446  args.check_error();
2447  return expr(args.ctx(), r);
2448  }
2449  inline expr mk_xor(expr_vector const& args) {
2450  if (args.empty())
2451  return args.ctx().bool_val(false);
2452  expr r = args[0u];
2453  for (unsigned i = 1; i < args.size(); ++i)
2454  r = r ^ args[i];
2455  return r;
2456  }
2457 
2458 
2459  class func_entry : public object {
2460  Z3_func_entry m_entry;
2461  void init(Z3_func_entry e) {
2462  m_entry = e;
2463  Z3_func_entry_inc_ref(ctx(), m_entry);
2464  }
2465  public:
2466  func_entry(context & c, Z3_func_entry e):object(c) { init(e); }
2467  func_entry(func_entry const & s):object(s) { init(s.m_entry); }
2469  operator Z3_func_entry() const { return m_entry; }
2471  Z3_func_entry_inc_ref(s.ctx(), s.m_entry);
2472  Z3_func_entry_dec_ref(ctx(), m_entry);
2473  object::operator=(s);
2474  m_entry = s.m_entry;
2475  return *this;
2476  }
2477  expr value() const { Z3_ast r = Z3_func_entry_get_value(ctx(), m_entry); check_error(); return expr(ctx(), r); }
2478  unsigned num_args() const { unsigned r = Z3_func_entry_get_num_args(ctx(), m_entry); check_error(); return r; }
2479  expr arg(unsigned i) const { Z3_ast r = Z3_func_entry_get_arg(ctx(), m_entry, i); check_error(); return expr(ctx(), r); }
2480  };
2481 
2482  class func_interp : public object {
2483  Z3_func_interp m_interp;
2484  void init(Z3_func_interp e) {
2485  m_interp = e;
2486  Z3_func_interp_inc_ref(ctx(), m_interp);
2487  }
2488  public:
2489  func_interp(context & c, Z3_func_interp e):object(c) { init(e); }
2490  func_interp(func_interp const & s):object(s) { init(s.m_interp); }
2492  operator Z3_func_interp() const { return m_interp; }
2494  Z3_func_interp_inc_ref(s.ctx(), s.m_interp);
2495  Z3_func_interp_dec_ref(ctx(), m_interp);
2496  object::operator=(s);
2497  m_interp = s.m_interp;
2498  return *this;
2499  }
2500  expr else_value() const { Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), r); }
2501  unsigned num_entries() const { unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }
2502  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); }
2503  void add_entry(expr_vector const& args, expr& value) {
2504  Z3_func_interp_add_entry(ctx(), m_interp, args, value);
2505  check_error();
2506  }
2507  void set_else(expr& value) {
2508  Z3_func_interp_set_else(ctx(), m_interp, value);
2509  check_error();
2510  }
2511  };
2512 
2513  class model : public object {
2514  Z3_model m_model;
2515  void init(Z3_model m) {
2516  m_model = m;
2517  Z3_model_inc_ref(ctx(), m);
2518  }
2519  public:
2520  struct translate {};
2521  model(context & c):object(c) { init(Z3_mk_model(c)); }
2522  model(context & c, Z3_model m):object(c) { init(m); }
2523  model(model const & s):object(s) { init(s.m_model); }
2524  model(model& src, context& dst, translate) : object(dst) { init(Z3_model_translate(src.ctx(), src, dst)); }
2525  ~model() { Z3_model_dec_ref(ctx(), m_model); }
2526  operator Z3_model() const { return m_model; }
2527  model & operator=(model const & s) {
2528  Z3_model_inc_ref(s.ctx(), s.m_model);
2529  Z3_model_dec_ref(ctx(), m_model);
2530  object::operator=(s);
2531  m_model = s.m_model;
2532  return *this;
2533  }
2534 
2535  expr eval(expr const & n, bool model_completion=false) const {
2536  check_context(*this, n);
2537  Z3_ast r = 0;
2538  bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
2539  check_error();
2540  if (status == false && ctx().enable_exceptions())
2541  Z3_THROW(exception("failed to evaluate expression"));
2542  return expr(ctx(), r);
2543  }
2544 
2545  unsigned num_consts() const { return Z3_model_get_num_consts(ctx(), m_model); }
2546  unsigned num_funcs() const { return Z3_model_get_num_funcs(ctx(), m_model); }
2547  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); }
2548  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); }
2549  unsigned size() const { return num_consts() + num_funcs(); }
2550  func_decl operator[](int i) const {
2551  assert(0 <= i);
2552  return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
2553  }
2554 
2555  // returns interpretation of constant declaration c.
2556  // If c is not assigned any value in the model it returns
2557  // an expression with a null ast reference.
2559  check_context(*this, c);
2560  Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);
2561  check_error();
2562  return expr(ctx(), r);
2563  }
2565  check_context(*this, f);
2566  Z3_func_interp r = Z3_model_get_func_interp(ctx(), m_model, f);
2567  check_error();
2568  return func_interp(ctx(), r);
2569  }
2570 
2571  // returns true iff the model contains an interpretation
2572  // for function f.
2573  bool has_interp(func_decl f) const {
2574  check_context(*this, f);
2575  return Z3_model_has_interp(ctx(), m_model, f);
2576  }
2577 
2579  Z3_func_interp r = Z3_add_func_interp(ctx(), m_model, f, else_val);
2580  check_error();
2581  return func_interp(ctx(), r);
2582  }
2583 
2584  void add_const_interp(func_decl& f, expr& value) {
2585  Z3_add_const_interp(ctx(), m_model, f, value);
2586  check_error();
2587  }
2588 
2589  friend std::ostream & operator<<(std::ostream & out, model const & m);
2590 
2591  std::string to_string() const { return m_model ? std::string(Z3_model_to_string(ctx(), m_model)) : "null"; }
2592  };
2593  inline std::ostream & operator<<(std::ostream & out, model const & m) { return out << m.to_string(); }
2594 
2595  class stats : public object {
2596  Z3_stats m_stats;
2597  void init(Z3_stats e) {
2598  m_stats = e;
2599  Z3_stats_inc_ref(ctx(), m_stats);
2600  }
2601  public:
2602  stats(context & c):object(c), m_stats(0) {}
2603  stats(context & c, Z3_stats e):object(c) { init(e); }
2604  stats(stats const & s):object(s) { init(s.m_stats); }
2605  ~stats() { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); }
2606  operator Z3_stats() const { return m_stats; }
2607  stats & operator=(stats const & s) {
2608  Z3_stats_inc_ref(s.ctx(), s.m_stats);
2609  if (m_stats) Z3_stats_dec_ref(ctx(), m_stats);
2610  object::operator=(s);
2611  m_stats = s.m_stats;
2612  return *this;
2613  }
2614  unsigned size() const { return Z3_stats_size(ctx(), m_stats); }
2615  std::string key(unsigned i) const { Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; }
2616  bool is_uint(unsigned i) const { bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r; }
2617  bool is_double(unsigned i) const { bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r; }
2618  unsigned uint_value(unsigned i) const { unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; }
2619  double double_value(unsigned i) const { double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
2620  friend std::ostream & operator<<(std::ostream & out, stats const & s);
2621  };
2622  inline std::ostream & operator<<(std::ostream & out, stats const & s) { out << Z3_stats_to_string(s.ctx(), s); return out; }
2623 
2624 
2625  inline std::ostream & operator<<(std::ostream & out, check_result r) {
2626  if (r == unsat) out << "unsat";
2627  else if (r == sat) out << "sat";
2628  else out << "unknown";
2629  return out;
2630  }
2631 
2632 
2633  class solver : public object {
2634  Z3_solver m_solver;
2635  void init(Z3_solver s) {
2636  m_solver = s;
2637  if (s)
2638  Z3_solver_inc_ref(ctx(), s);
2639  }
2640  public:
2641  struct simple {};
2642  struct translate {};
2643  solver(context & c):object(c) { init(Z3_mk_solver(c)); }
2645  solver(context & c, Z3_solver s):object(c) { init(s); }
2646  solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); }
2647  solver(context & c, solver const& src, translate): object(c) { Z3_solver s = Z3_solver_translate(src.ctx(), src, c); check_error(); init(s); }
2648  solver(solver const & s):object(s) { init(s.m_solver); }
2649  ~solver() { Z3_solver_dec_ref(ctx(), m_solver); }
2650  operator Z3_solver() const { return m_solver; }
2651  solver & operator=(solver const & s) {
2652  Z3_solver_inc_ref(s.ctx(), s.m_solver);
2653  Z3_solver_dec_ref(ctx(), m_solver);
2654  object::operator=(s);
2655  m_solver = s.m_solver;
2656  return *this;
2657  }
2658  void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
2659  void set(char const * k, bool v) { params p(ctx()); p.set(k, v); set(p); }
2660  void set(char const * k, unsigned v) { params p(ctx()); p.set(k, v); set(p); }
2661  void set(char const * k, double v) { params p(ctx()); p.set(k, v); set(p); }
2662  void set(char const * k, symbol const & v) { params p(ctx()); p.set(k, v); set(p); }
2663  void set(char const * k, char const* v) { params p(ctx()); p.set(k, v); set(p); }
2664  void push() { Z3_solver_push(ctx(), m_solver); check_error(); }
2665  void pop(unsigned n = 1) { Z3_solver_pop(ctx(), m_solver, n); check_error(); }
2666  void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); }
2667  void add(expr const & e) { assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); }
2668  void add(expr const & e, expr const & p) {
2669  assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
2670  Z3_solver_assert_and_track(ctx(), m_solver, e, p);
2671  check_error();
2672  }
2673  void add(expr const & e, char const * p) {
2674  add(e, ctx().bool_const(p));
2675  }
2676  void add(expr_vector const& v) {
2677  check_context(*this, v);
2678  for (unsigned i = 0; i < v.size(); ++i)
2679  add(v[i]);
2680  }
2681  void from_file(char const* file) { Z3_solver_from_file(ctx(), m_solver, file); ctx().check_parser_error(); }
2682  void from_string(char const* s) { Z3_solver_from_string(ctx(), m_solver, s); ctx().check_parser_error(); }
2683 
2685  check_result check(unsigned n, expr * const assumptions) {
2686  array<Z3_ast> _assumptions(n);
2687  for (unsigned i = 0; i < n; i++) {
2688  check_context(*this, assumptions[i]);
2689  _assumptions[i] = assumptions[i];
2690  }
2691  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
2692  check_error();
2693  return to_check_result(r);
2694  }
2695  check_result check(expr_vector const& assumptions) {
2696  unsigned n = assumptions.size();
2697  array<Z3_ast> _assumptions(n);
2698  for (unsigned i = 0; i < n; i++) {
2699  check_context(*this, assumptions[i]);
2700  _assumptions[i] = assumptions[i];
2701  }
2702  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
2703  check_error();
2704  return to_check_result(r);
2705  }
2706  model get_model() const { Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }
2708  Z3_lbool r = Z3_solver_get_consequences(ctx(), m_solver, assumptions, vars, conseq);
2709  check_error();
2710  return to_check_result(r);
2711  }
2712  std::string reason_unknown() const { Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }
2713  stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }
2717  expr_vector units() const { Z3_ast_vector r = Z3_solver_get_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2718  expr_vector trail() const { Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2720  Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver);
2721  check_error();
2722  expr_vector result(ctx(), r);
2723  unsigned sz = result.size();
2724  levels.resize(sz);
2725  Z3_solver_get_levels(ctx(), m_solver, r, sz, levels.ptr());
2726  check_error();
2727  return result;
2728  }
2729  expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
2730  friend std::ostream & operator<<(std::ostream & out, solver const & s);
2731 
2732  std::string to_smt2(char const* status = "unknown") {
2733  array<Z3_ast> es(assertions());
2734  Z3_ast const* fmls = es.ptr();
2735  Z3_ast fml = 0;
2736  unsigned sz = es.size();
2737  if (sz > 0) {
2738  --sz;
2739  fml = fmls[sz];
2740  }
2741  else {
2742  fml = ctx().bool_val(true);
2743  }
2744  return std::string(Z3_benchmark_to_smtlib_string(
2745  ctx(),
2746  "", "", status, "",
2747  sz,
2748  fmls,
2749  fml));
2750  }
2751 
2752  std::string dimacs(bool include_names = true) const { return std::string(Z3_solver_to_dimacs_string(ctx(), m_solver, include_names)); }
2753 
2755 
2756 
2757  expr_vector cube(expr_vector& vars, unsigned cutoff) {
2758  Z3_ast_vector r = Z3_solver_cube(ctx(), m_solver, vars, cutoff);
2759  check_error();
2760  return expr_vector(ctx(), r);
2761  }
2762 
2764  solver& m_solver;
2765  unsigned& m_cutoff;
2766  expr_vector& m_vars;
2767  expr_vector m_cube;
2768  bool m_end;
2769  bool m_empty;
2770 
2771  void inc() {
2772  assert(!m_end && !m_empty);
2773  m_cube = m_solver.cube(m_vars, m_cutoff);
2774  m_cutoff = 0xFFFFFFFF;
2775  if (m_cube.size() == 1 && m_cube[0u].is_false()) {
2776  m_cube = z3::expr_vector(m_solver.ctx());
2777  m_end = true;
2778  }
2779  else if (m_cube.empty()) {
2780  m_empty = true;
2781  }
2782  }
2783  public:
2784  cube_iterator(solver& s, expr_vector& vars, unsigned& cutoff, bool end):
2785  m_solver(s),
2786  m_cutoff(cutoff),
2787  m_vars(vars),
2788  m_cube(s.ctx()),
2789  m_end(end),
2790  m_empty(false) {
2791  if (!m_end) {
2792  inc();
2793  }
2794  }
2795 
2797  assert(!m_end);
2798  if (m_empty) {
2799  m_end = true;
2800  }
2801  else {
2802  inc();
2803  }
2804  return *this;
2805  }
2806  cube_iterator operator++(int) { assert(false); return *this; }
2807  expr_vector const * operator->() const { return &(operator*()); }
2808  expr_vector const& operator*() const noexcept { return m_cube; }
2809 
2810  bool operator==(cube_iterator const& other) noexcept {
2811  return other.m_end == m_end;
2812  };
2813  bool operator!=(cube_iterator const& other) noexcept {
2814  return other.m_end != m_end;
2815  };
2816 
2817  };
2818 
2820  solver& m_solver;
2821  unsigned m_cutoff;
2822  expr_vector m_default_vars;
2823  expr_vector& m_vars;
2824  public:
2826  m_solver(s),
2827  m_cutoff(0xFFFFFFFF),
2828  m_default_vars(s.ctx()),
2829  m_vars(m_default_vars)
2830  {}
2831 
2833  m_solver(s),
2834  m_cutoff(0xFFFFFFFF),
2835  m_default_vars(s.ctx()),
2836  m_vars(vars)
2837  {}
2838 
2839  cube_iterator begin() { return cube_iterator(m_solver, m_vars, m_cutoff, false); }
2840  cube_iterator end() { return cube_iterator(m_solver, m_vars, m_cutoff, true); }
2841  void set_cutoff(unsigned c) noexcept { m_cutoff = c; }
2842  };
2843 
2844  cube_generator cubes() { return cube_generator(*this); }
2845  cube_generator cubes(expr_vector& vars) { return cube_generator(*this, vars); }
2846 
2847  };
2848  inline std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
2849 
2850  class goal : public object {
2851  Z3_goal m_goal;
2852  void init(Z3_goal s) {
2853  m_goal = s;
2854  Z3_goal_inc_ref(ctx(), s);
2855  }
2856  public:
2857  goal(context & c, bool models=true, bool unsat_cores=false, bool proofs=false):object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); }
2858  goal(context & c, Z3_goal s):object(c) { init(s); }
2859  goal(goal const & s):object(s) { init(s.m_goal); }
2860  ~goal() { Z3_goal_dec_ref(ctx(), m_goal); }
2861  operator Z3_goal() const { return m_goal; }
2862  goal & operator=(goal const & s) {
2863  Z3_goal_inc_ref(s.ctx(), s.m_goal);
2864  Z3_goal_dec_ref(ctx(), m_goal);
2865  object::operator=(s);
2866  m_goal = s.m_goal;
2867  return *this;
2868  }
2869  void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
2870  void add(expr_vector const& v) { check_context(*this, v); for (unsigned i = 0; i < v.size(); ++i) add(v[i]); }
2871  unsigned size() const { return Z3_goal_size(ctx(), m_goal); }
2872  expr operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
2873  Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); }
2874  bool inconsistent() const { return Z3_goal_inconsistent(ctx(), m_goal); }
2875  unsigned depth() const { return Z3_goal_depth(ctx(), m_goal); }
2876  void reset() { Z3_goal_reset(ctx(), m_goal); }
2877  unsigned num_exprs() const { return Z3_goal_num_exprs(ctx(), m_goal); }
2878  bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal); }
2879  bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal); }
2880  model convert_model(model const & m) const {
2881  check_context(*this, m);
2882  Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, m);
2883  check_error();
2884  return model(ctx(), new_m);
2885  }
2886  model get_model() const {
2887  Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, 0);
2888  check_error();
2889  return model(ctx(), new_m);
2890  }
2891  expr as_expr() const {
2892  unsigned n = size();
2893  if (n == 0)
2894  return ctx().bool_val(true);
2895  else if (n == 1)
2896  return operator[](0);
2897  else {
2898  array<Z3_ast> args(n);
2899  for (unsigned i = 0; i < n; i++)
2900  args[i] = operator[](i);
2901  return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
2902  }
2903  }
2904  std::string dimacs(bool include_names = true) const { return std::string(Z3_goal_to_dimacs_string(ctx(), m_goal, include_names)); }
2905  friend std::ostream & operator<<(std::ostream & out, goal const & g);
2906  };
2907  inline std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; }
2908 
2909  class apply_result : public object {
2910  Z3_apply_result m_apply_result;
2911  void init(Z3_apply_result s) {
2912  m_apply_result = s;
2914  }
2915  public:
2916  apply_result(context & c, Z3_apply_result s):object(c) { init(s); }
2917  apply_result(apply_result const & s):object(s) { init(s.m_apply_result); }
2918  ~apply_result() { Z3_apply_result_dec_ref(ctx(), m_apply_result); }
2919  operator Z3_apply_result() const { return m_apply_result; }
2921  Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result);
2922  Z3_apply_result_dec_ref(ctx(), m_apply_result);
2923  object::operator=(s);
2924  m_apply_result = s.m_apply_result;
2925  return *this;
2926  }
2927  unsigned size() const { return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }
2928  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); }
2929  friend std::ostream & operator<<(std::ostream & out, apply_result const & r);
2930  };
2931  inline std::ostream & operator<<(std::ostream & out, apply_result const & r) { out << Z3_apply_result_to_string(r.ctx(), r); return out; }
2932 
2933  class tactic : public object {
2934  Z3_tactic m_tactic;
2935  void init(Z3_tactic s) {
2936  m_tactic = s;
2937  Z3_tactic_inc_ref(ctx(), s);
2938  }
2939  public:
2940  tactic(context & c, char const * name):object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); }
2941  tactic(context & c, Z3_tactic s):object(c) { init(s); }
2942  tactic(tactic const & s):object(s) { init(s.m_tactic); }
2943  ~tactic() { Z3_tactic_dec_ref(ctx(), m_tactic); }
2944  operator Z3_tactic() const { return m_tactic; }
2945  tactic & operator=(tactic const & s) {
2946  Z3_tactic_inc_ref(s.ctx(), s.m_tactic);
2947  Z3_tactic_dec_ref(ctx(), m_tactic);
2948  object::operator=(s);
2949  m_tactic = s.m_tactic;
2950  return *this;
2951  }
2952  solver mk_solver() const { Z3_solver r = Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error(); return solver(ctx(), r); }
2953  apply_result apply(goal const & g) const {
2954  check_context(*this, g);
2955  Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g);
2956  check_error();
2957  return apply_result(ctx(), r);
2958  }
2959  apply_result operator()(goal const & g) const {
2960  return apply(g);
2961  }
2962  std::string help() const { char const * r = Z3_tactic_get_help(ctx(), m_tactic); check_error(); return r; }
2963  friend tactic operator&(tactic const & t1, tactic const & t2);
2964  friend tactic operator|(tactic const & t1, tactic const & t2);
2965  friend tactic repeat(tactic const & t, unsigned max);
2966  friend tactic with(tactic const & t, params const & p);
2967  friend tactic try_for(tactic const & t, unsigned ms);
2968  friend tactic par_or(unsigned n, tactic const* tactics);
2969  friend tactic par_and_then(tactic const& t1, tactic const& t2);
2971  };
2972 
2973  inline tactic operator&(tactic const & t1, tactic const & t2) {
2974  check_context(t1, t2);
2975  Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
2976  t1.check_error();
2977  return tactic(t1.ctx(), r);
2978  }
2979 
2980  inline tactic operator|(tactic const & t1, tactic const & t2) {
2981  check_context(t1, t2);
2982  Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
2983  t1.check_error();
2984  return tactic(t1.ctx(), r);
2985  }
2986 
2987  inline tactic repeat(tactic const & t, unsigned max=UINT_MAX) {
2988  Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
2989  t.check_error();
2990  return tactic(t.ctx(), r);
2991  }
2992 
2993  inline tactic with(tactic const & t, params const & p) {
2994  Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
2995  t.check_error();
2996  return tactic(t.ctx(), r);
2997  }
2998  inline tactic try_for(tactic const & t, unsigned ms) {
2999  Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
3000  t.check_error();
3001  return tactic(t.ctx(), r);
3002  }
3003  inline tactic par_or(unsigned n, tactic const* tactics) {
3004  if (n == 0) {
3005  Z3_THROW(exception("a non-zero number of tactics need to be passed to par_or"));
3006  }
3007  array<Z3_tactic> buffer(n);
3008  for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
3009  return tactic(tactics[0u].ctx(), Z3_tactic_par_or(tactics[0u].ctx(), n, buffer.ptr()));
3010  }
3011 
3012  inline tactic par_and_then(tactic const & t1, tactic const & t2) {
3013  check_context(t1, t2);
3014  Z3_tactic r = Z3_tactic_par_and_then(t1.ctx(), t1, t2);
3015  t1.check_error();
3016  return tactic(t1.ctx(), r);
3017  }
3018 
3019  class probe : public object {
3020  Z3_probe m_probe;
3021  void init(Z3_probe s) {
3022  m_probe = s;
3023  Z3_probe_inc_ref(ctx(), s);
3024  }
3025  public:
3026  probe(context & c, char const * name):object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); }
3027  probe(context & c, double val):object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); }
3028  probe(context & c, Z3_probe s):object(c) { init(s); }
3029  probe(probe const & s):object(s) { init(s.m_probe); }
3030  ~probe() { Z3_probe_dec_ref(ctx(), m_probe); }
3031  operator Z3_probe() const { return m_probe; }
3032  probe & operator=(probe const & s) {
3033  Z3_probe_inc_ref(s.ctx(), s.m_probe);
3034  Z3_probe_dec_ref(ctx(), m_probe);
3035  object::operator=(s);
3036  m_probe = s.m_probe;
3037  return *this;
3038  }
3039  double apply(goal const & g) const { double r = Z3_probe_apply(ctx(), m_probe, g); check_error(); return r; }
3040  double operator()(goal const & g) const { return apply(g); }
3041  friend probe operator<=(probe const & p1, probe const & p2);
3042  friend probe operator<=(probe const & p1, double p2);
3043  friend probe operator<=(double p1, probe const & p2);
3044  friend probe operator>=(probe const & p1, probe const & p2);
3045  friend probe operator>=(probe const & p1, double p2);
3046  friend probe operator>=(double p1, probe const & p2);
3047  friend probe operator<(probe const & p1, probe const & p2);
3048  friend probe operator<(probe const & p1, double p2);
3049  friend probe operator<(double p1, probe const & p2);
3050  friend probe operator>(probe const & p1, probe const & p2);
3051  friend probe operator>(probe const & p1, double p2);
3052  friend probe operator>(double p1, probe const & p2);
3053  friend probe operator==(probe const & p1, probe const & p2);
3054  friend probe operator==(probe const & p1, double p2);
3055  friend probe operator==(double p1, probe const & p2);
3056  friend probe operator&&(probe const & p1, probe const & p2);
3057  friend probe operator||(probe const & p1, probe const & p2);
3058  friend probe operator!(probe const & p);
3059  };
3060 
3061  inline probe operator<=(probe const & p1, probe const & p2) {
3062  check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3063  }
3064  inline probe operator<=(probe const & p1, double p2) { return p1 <= probe(p1.ctx(), p2); }
3065  inline probe operator<=(double p1, probe const & p2) { return probe(p2.ctx(), p1) <= p2; }
3066  inline probe operator>=(probe const & p1, probe const & p2) {
3067  check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3068  }
3069  inline probe operator>=(probe const & p1, double p2) { return p1 >= probe(p1.ctx(), p2); }
3070  inline probe operator>=(double p1, probe const & p2) { return probe(p2.ctx(), p1) >= p2; }
3071  inline probe operator<(probe const & p1, probe const & p2) {
3072  check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3073  }
3074  inline probe operator<(probe const & p1, double p2) { return p1 < probe(p1.ctx(), p2); }
3075  inline probe operator<(double p1, probe const & p2) { return probe(p2.ctx(), p1) < p2; }
3076  inline probe operator>(probe const & p1, probe const & p2) {
3077  check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3078  }
3079  inline probe operator>(probe const & p1, double p2) { return p1 > probe(p1.ctx(), p2); }
3080  inline probe operator>(double p1, probe const & p2) { return probe(p2.ctx(), p1) > p2; }
3081  inline probe operator==(probe const & p1, probe const & p2) {
3082  check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3083  }
3084  inline probe operator==(probe const & p1, double p2) { return p1 == probe(p1.ctx(), p2); }
3085  inline probe operator==(double p1, probe const & p2) { return probe(p2.ctx(), p1) == p2; }
3086  inline probe operator&&(probe const & p1, probe const & p2) {
3087  check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3088  }
3089  inline probe operator||(probe const & p1, probe const & p2) {
3090  check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3091  }
3092  inline probe operator!(probe const & p) {
3093  Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
3094  }
3095 
3096  class optimize : public object {
3097  Z3_optimize m_opt;
3098 
3099  public:
3100  class handle final {
3101  unsigned m_h;
3102  public:
3103  handle(unsigned h): m_h(h) {}
3104  unsigned h() const { return m_h; }
3105  };
3106  optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }
3107  optimize(optimize const & o):object(o), m_opt(o.m_opt) {
3108  Z3_optimize_inc_ref(o.ctx(), o.m_opt);
3109  }
3111  m_opt = Z3_mk_optimize(c);
3112  Z3_optimize_inc_ref(c, m_opt);
3113  add(expr_vector(c, src.assertions()));
3114  expr_vector v(c, src.objectives());
3115  for (expr_vector::iterator it = v.begin(); it != v.end(); ++it) minimize(*it);
3116  }
3118  Z3_optimize_inc_ref(o.ctx(), o.m_opt);
3119  Z3_optimize_dec_ref(ctx(), m_opt);
3120  m_opt = o.m_opt;
3121  object::operator=(o);
3122  return *this;
3123  }
3125  operator Z3_optimize() const { return m_opt; }
3126  void add(expr const& e) {
3127  assert(e.is_bool());
3128  Z3_optimize_assert(ctx(), m_opt, e);
3129  }
3130  void add(expr_vector const& es) {
3131  for (expr_vector::iterator it = es.begin(); it != es.end(); ++it) add(*it);
3132  }
3133  void add(expr const& e, expr const& t) {
3134  assert(e.is_bool());
3135  Z3_optimize_assert_and_track(ctx(), m_opt, e, t);
3136  }
3137  void add(expr const& e, char const* p) {
3138  assert(e.is_bool());
3139  add(e, ctx().bool_const(p));
3140  }
3141  handle add_soft(expr const& e, unsigned weight) {
3142  assert(e.is_bool());
3143  auto str = std::to_string(weight);
3144  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, str.c_str(), 0));
3145  }
3146  handle add_soft(expr const& e, char const* weight) {
3147  assert(e.is_bool());
3148  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0));
3149  }
3150  handle add(expr const& e, unsigned weight) {
3151  return add_soft(e, weight);
3152  }
3153  handle maximize(expr const& e) {
3154  return handle(Z3_optimize_maximize(ctx(), m_opt, e));
3155  }
3156  handle minimize(expr const& e) {
3157  return handle(Z3_optimize_minimize(ctx(), m_opt, e));
3158  }
3159  void push() {
3160  Z3_optimize_push(ctx(), m_opt);
3161  }
3162  void pop() {
3163  Z3_optimize_pop(ctx(), m_opt);
3164  }
3167  unsigned n = asms.size();
3168  array<Z3_ast> _asms(n);
3169  for (unsigned i = 0; i < n; i++) {
3170  check_context(*this, asms[i]);
3171  _asms[i] = asms[i];
3172  }
3173  Z3_lbool r = Z3_optimize_check(ctx(), m_opt, n, _asms.ptr());
3174  check_error();
3175  return to_check_result(r);
3176  }
3177  model get_model() const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }
3179  void set(params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }
3180  expr lower(handle const& h) {
3181  Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());
3182  check_error();
3183  return expr(ctx(), r);
3184  }
3185  expr upper(handle const& h) {
3186  Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h());
3187  check_error();
3188  return expr(ctx(), r);
3189  }
3192  stats statistics() const { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); }
3193  friend std::ostream & operator<<(std::ostream & out, optimize const & s);
3194  void from_file(char const* filename) { Z3_optimize_from_file(ctx(), m_opt, filename); check_error(); }
3195  void from_string(char const* constraints) { Z3_optimize_from_string(ctx(), m_opt, constraints); check_error(); }
3196  std::string help() const { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error(); return r; }
3197  };
3198  inline std::ostream & operator<<(std::ostream & out, optimize const & s) { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }
3199 
3200  class fixedpoint : public object {
3201  Z3_fixedpoint m_fp;
3202  public:
3204  fixedpoint(fixedpoint const & o):object(o), m_fp(o.m_fp) { Z3_fixedpoint_inc_ref(ctx(), m_fp); }
3207  Z3_fixedpoint_inc_ref(o.ctx(), o.m_fp);
3208  Z3_fixedpoint_dec_ref(ctx(), m_fp);
3209  m_fp = o.m_fp;
3210  object::operator=(o);
3211  return *this;
3212  }
3213  operator Z3_fixedpoint() const { return m_fp; }
3214  expr_vector from_string(char const* s) {
3215  Z3_ast_vector r = Z3_fixedpoint_from_string(ctx(), m_fp, s);
3216  check_error();
3217  return expr_vector(ctx(), r);
3218  }
3219  expr_vector from_file(char const* s) {
3220  Z3_ast_vector r = Z3_fixedpoint_from_file(ctx(), m_fp, s);
3221  check_error();
3222  return expr_vector(ctx(), r);
3223  }
3224  void add_rule(expr& rule, symbol const& name) { Z3_fixedpoint_add_rule(ctx(), m_fp, rule, name); check_error(); }
3225  void add_fact(func_decl& f, unsigned * args) { Z3_fixedpoint_add_fact(ctx(), m_fp, f, f.arity(), args); check_error(); }
3228  array<Z3_func_decl> rs(relations);
3229  Z3_lbool r = Z3_fixedpoint_query_relations(ctx(), m_fp, rs.size(), rs.ptr());
3230  check_error();
3231  return to_check_result(r);
3232  }
3233  expr get_answer() { Z3_ast r = Z3_fixedpoint_get_answer(ctx(), m_fp); check_error(); return expr(ctx(), r); }
3234  std::string reason_unknown() { return Z3_fixedpoint_get_reason_unknown(ctx(), m_fp); }
3235  void update_rule(expr& rule, symbol const& name) { Z3_fixedpoint_update_rule(ctx(), m_fp, rule, name); check_error(); }
3236  unsigned get_num_levels(func_decl& p) { unsigned r = Z3_fixedpoint_get_num_levels(ctx(), m_fp, p); check_error(); return r; }
3237  expr get_cover_delta(int level, func_decl& p) {
3238  Z3_ast r = Z3_fixedpoint_get_cover_delta(ctx(), m_fp, level, p);
3239  check_error();
3240  return expr(ctx(), r);
3241  }
3242  void add_cover(int level, func_decl& p, expr& property) { Z3_fixedpoint_add_cover(ctx(), m_fp, level, p, property); check_error(); }
3243  stats statistics() const { Z3_stats r = Z3_fixedpoint_get_statistics(ctx(), m_fp); check_error(); return stats(ctx(), r); }
3247  void set(params const & p) { Z3_fixedpoint_set_params(ctx(), m_fp, p); check_error(); }
3248  std::string help() const { return Z3_fixedpoint_get_help(ctx(), m_fp); }
3250  std::string to_string() { return Z3_fixedpoint_to_string(ctx(), m_fp, 0, 0); }
3251  std::string to_string(expr_vector const& queries) {
3252  array<Z3_ast> qs(queries);
3253  return Z3_fixedpoint_to_string(ctx(), m_fp, qs.size(), qs.ptr());
3254  }
3255  };
3256  inline std::ostream & operator<<(std::ostream & out, fixedpoint const & f) { return out << Z3_fixedpoint_to_string(f.ctx(), f, 0, 0); }
3257 
3258  inline tactic fail_if(probe const & p) {
3259  Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
3260  p.check_error();
3261  return tactic(p.ctx(), r);
3262  }
3263  inline tactic when(probe const & p, tactic const & t) {
3264  check_context(p, t);
3265  Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
3266  t.check_error();
3267  return tactic(t.ctx(), r);
3268  }
3269  inline tactic cond(probe const & p, tactic const & t1, tactic const & t2) {
3270  check_context(p, t1); check_context(p, t2);
3271  Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
3272  t1.check_error();
3273  return tactic(t1.ctx(), r);
3274  }
3275 
3276  inline symbol context::str_symbol(char const * s) { Z3_symbol r = Z3_mk_string_symbol(m_ctx, s); check_error(); return symbol(*this, r); }
3277  inline symbol context::int_symbol(int n) { Z3_symbol r = Z3_mk_int_symbol(m_ctx, n); check_error(); return symbol(*this, r); }
3278 
3279  inline sort context::bool_sort() { Z3_sort s = Z3_mk_bool_sort(m_ctx); check_error(); return sort(*this, s); }
3280  inline sort context::int_sort() { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }
3281  inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
3282  inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
3283  inline sort context::string_sort() { Z3_sort s = Z3_mk_string_sort(m_ctx); check_error(); return sort(*this, s); }
3284  inline sort context::char_sort() { Z3_sort s = Z3_mk_char_sort(m_ctx); check_error(); return sort(*this, s); }
3285  inline sort context::seq_sort(sort& s) { Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); }
3286  inline sort context::re_sort(sort& s) { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
3287  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); }
3288 
3289  template<>
3290  inline sort context::fpa_sort<16>() { return fpa_sort(5, 11); }
3291 
3292  template<>
3293  inline sort context::fpa_sort<32>() { return fpa_sort(8, 24); }
3294 
3295  template<>
3296  inline sort context::fpa_sort<64>() { return fpa_sort(11, 53); }
3297 
3298  template<>
3299  inline sort context::fpa_sort<128>() { return fpa_sort(15, 113); }
3300 
3302 
3303  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); }
3305  array<Z3_sort> dom(d);
3306  Z3_sort s = Z3_mk_array_sort_n(m_ctx, dom.size(), dom.ptr(), r); check_error(); return sort(*this, s);
3307  }
3308  inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
3309  array<Z3_symbol> _enum_names(n);
3310  for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
3311  array<Z3_func_decl> _cs(n);
3312  array<Z3_func_decl> _ts(n);
3313  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3314  sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
3315  check_error();
3316  for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
3317  return s;
3318  }
3319  inline func_decl context::tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs) {
3320  array<Z3_symbol> _names(n);
3321  array<Z3_sort> _sorts(n);
3322  for (unsigned i = 0; i < n; i++) { _names[i] = Z3_mk_string_symbol(*this, names[i]); _sorts[i] = sorts[i]; }
3323  array<Z3_func_decl> _projs(n);
3324  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3325  Z3_func_decl tuple;
3326  sort _ignore_s = to_sort(*this, Z3_mk_tuple_sort(*this, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));
3327  check_error();
3328  for (unsigned i = 0; i < n; i++) { projs.push_back(func_decl(*this, _projs[i])); }
3329  return func_decl(*this, tuple);
3330  }
3331 
3332  inline sort context::uninterpreted_sort(char const* name) {
3333  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3334  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
3335  }
3337  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
3338  }
3339 
3340  inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3341  array<Z3_sort> args(arity);
3342  for (unsigned i = 0; i < arity; i++) {
3343  check_context(domain[i], range);
3344  args[i] = domain[i];
3345  }
3346  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
3347  check_error();
3348  return func_decl(*this, f);
3349  }
3350 
3351  inline func_decl context::function(char const * name, unsigned arity, sort const * domain, sort const & range) {
3352  return function(range.ctx().str_symbol(name), arity, domain, range);
3353  }
3354 
3355  inline func_decl context::function(symbol const& name, sort_vector const& domain, sort const& range) {
3356  array<Z3_sort> args(domain.size());
3357  for (unsigned i = 0; i < domain.size(); i++) {
3358  check_context(domain[i], range);
3359  args[i] = domain[i];
3360  }
3361  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
3362  check_error();
3363  return func_decl(*this, f);
3364  }
3365 
3366  inline func_decl context::function(char const * name, sort_vector const& domain, sort const& range) {
3367  return function(range.ctx().str_symbol(name), domain, range);
3368  }
3369 
3370 
3371  inline func_decl context::function(char const * name, sort const & domain, sort const & range) {
3372  check_context(domain, range);
3373  Z3_sort args[1] = { domain };
3374  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
3375  check_error();
3376  return func_decl(*this, f);
3377  }
3378 
3379  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & range) {
3381  Z3_sort args[2] = { d1, d2 };
3382  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
3383  check_error();
3384  return func_decl(*this, f);
3385  }
3386 
3387  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
3389  Z3_sort args[3] = { d1, d2, d3 };
3390  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
3391  check_error();
3392  return func_decl(*this, f);
3393  }
3394 
3395  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
3397  Z3_sort args[4] = { d1, d2, d3, d4 };
3398  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
3399  check_error();
3400  return func_decl(*this, f);
3401  }
3402 
3403  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) {
3405  Z3_sort args[5] = { d1, d2, d3, d4, d5 };
3406  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
3407  check_error();
3408  return func_decl(*this, f);
3409  }
3410 
3411  inline func_decl context::recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3412  array<Z3_sort> args(arity);
3413  for (unsigned i = 0; i < arity; i++) {
3414  check_context(domain[i], range);
3415  args[i] = domain[i];
3416  }
3417  Z3_func_decl f = Z3_mk_rec_func_decl(m_ctx, name, arity, args.ptr(), range);
3418  check_error();
3419  return func_decl(*this, f);
3420 
3421  }
3422 
3423  inline func_decl context::recfun(char const * name, unsigned arity, sort const * domain, sort const & range) {
3424  return recfun(str_symbol(name), arity, domain, range);
3425  }
3426 
3427  inline func_decl context::recfun(char const * name, sort const& d1, sort const & range) {
3428  return recfun(str_symbol(name), 1, &d1, range);
3429  }
3430 
3431  inline func_decl context::recfun(char const * name, sort const& d1, sort const& d2, sort const & range) {
3432  sort dom[2] = { d1, d2 };
3433  return recfun(str_symbol(name), 2, dom, range);
3434  }
3435 
3436  inline void context::recdef(func_decl f, expr_vector const& args, expr const& body) {
3437  check_context(f, args); check_context(f, body);
3438  array<Z3_ast> vars(args);
3439  Z3_add_rec_def(f.ctx(), f, vars.size(), vars.ptr(), body);
3440  }
3441 
3442  inline func_decl context::user_propagate_function(symbol const& name, sort_vector const& domain, sort const& range) {
3443  check_context(domain, range);
3444  array<Z3_sort> domain1(domain);
3445  Z3_func_decl f = Z3_solver_propagate_declare(range.ctx(), name, domain1.size(), domain1.ptr(), range);
3446  check_error();
3447  return func_decl(*this, f);
3448  }
3449 
3450  inline expr context::constant(symbol const & name, sort const & s) {
3451  Z3_ast r = Z3_mk_const(m_ctx, name, s);
3452  check_error();
3453  return expr(*this, r);
3454  }
3455  inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); }
3456  inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); }
3457  inline expr context::int_const(char const * name) { return constant(name, int_sort()); }
3458  inline expr context::real_const(char const * name) { return constant(name, real_sort()); }
3459  inline expr context::string_const(char const * name) { return constant(name, string_sort()); }
3460  inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); }
3461  inline expr context::fpa_const(char const * name, unsigned ebits, unsigned sbits) { return constant(name, fpa_sort(ebits, sbits)); }
3462 
3463  template<size_t precision>
3464  inline expr context::fpa_const(char const * name) { return constant(name, fpa_sort<precision>()); }
3465 
3466  inline void context::set_rounding_mode(rounding_mode rm) { m_rounding_mode = rm; }
3467 
3469  switch (m_rounding_mode) {
3470  case RNA: return expr(*this, Z3_mk_fpa_rna(m_ctx));
3471  case RNE: return expr(*this, Z3_mk_fpa_rne(m_ctx));
3472  case RTP: return expr(*this, Z3_mk_fpa_rtp(m_ctx));
3473  case RTN: return expr(*this, Z3_mk_fpa_rtn(m_ctx));
3474  case RTZ: return expr(*this, Z3_mk_fpa_rtz(m_ctx));
3475  default: return expr(*this);
3476  }
3477  }
3478 
3479  inline expr context::bool_val(bool b) { return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }
3480 
3481  inline expr context::int_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
3482  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); }
3483  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); }
3484  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); }
3485  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); }
3486 
3487  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); }
3488  inline expr context::real_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
3489  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); }
3490  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); }
3491  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); }
3492  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); }
3493 
3494  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); }
3495  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); }
3496  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); }
3497  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); }
3498  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); }
3499  inline expr context::bv_val(unsigned n, bool const* bits) {
3500  array<bool> _bits(n);
3501  for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
3502  Z3_ast r = Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error(); return expr(*this, r);
3503  }
3504 
3505  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); }
3506  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); }
3507  inline expr context::fpa_nan(sort const & s) { Z3_ast r = Z3_mk_fpa_nan(m_ctx, s); check_error(); return expr(*this, r); }
3508  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); }
3509 
3510  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); }
3511  inline expr context::string_val(char const* s) { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
3512  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); }
3513  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); }
3514 
3515  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); }
3516 
3517  inline expr func_decl::operator()(unsigned n, expr const * args) const {
3518  array<Z3_ast> _args(n);
3519  for (unsigned i = 0; i < n; i++) {
3520  check_context(*this, args[i]);
3521  _args[i] = args[i];
3522  }
3523  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
3524  check_error();
3525  return expr(ctx(), r);
3526 
3527  }
3528  inline expr func_decl::operator()(expr_vector const& args) const {
3529  array<Z3_ast> _args(args.size());
3530  for (unsigned i = 0; i < args.size(); i++) {
3531  check_context(*this, args[i]);
3532  _args[i] = args[i];
3533  }
3534  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
3535  check_error();
3536  return expr(ctx(), r);
3537  }
3538  inline expr func_decl::operator()() const {
3539  Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
3540  ctx().check_error();
3541  return expr(ctx(), r);
3542  }
3543  inline expr func_decl::operator()(expr const & a) const {
3544  check_context(*this, a);
3545  Z3_ast args[1] = { a };
3546  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3547  ctx().check_error();
3548  return expr(ctx(), r);
3549  }
3550  inline expr func_decl::operator()(int a) const {
3551  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
3552  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3553  ctx().check_error();
3554  return expr(ctx(), r);
3555  }
3556  inline expr func_decl::operator()(expr const & a1, expr const & a2) const {
3557  check_context(*this, a1); check_context(*this, a2);
3558  Z3_ast args[2] = { a1, a2 };
3559  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3560  ctx().check_error();
3561  return expr(ctx(), r);
3562  }
3563  inline expr func_decl::operator()(expr const & a1, int a2) const {
3564  check_context(*this, a1);
3565  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
3566  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3567  ctx().check_error();
3568  return expr(ctx(), r);
3569  }
3570  inline expr func_decl::operator()(int a1, expr const & a2) const {
3571  check_context(*this, a2);
3572  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
3573  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3574  ctx().check_error();
3575  return expr(ctx(), r);
3576  }
3577  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3) const {
3578  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
3579  Z3_ast args[3] = { a1, a2, a3 };
3580  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
3581  ctx().check_error();
3582  return expr(ctx(), r);
3583  }
3584  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const {
3585  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
3586  Z3_ast args[4] = { a1, a2, a3, a4 };
3587  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
3588  ctx().check_error();
3589  return expr(ctx(), r);
3590  }
3591  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const {
3592  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
3593  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
3594  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
3595  ctx().check_error();
3596  return expr(ctx(), r);
3597  }
3598 
3599  inline expr to_real(expr const & a) { Z3_ast r = Z3_mk_int2real(a.ctx(), a); a.check_error(); return expr(a.ctx(), r); }
3600 
3601  inline func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3602  return range.ctx().function(name, arity, domain, range);
3603  }
3604  inline func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range) {
3605  return range.ctx().function(name, arity, domain, range);
3606  }
3607  inline func_decl function(char const * name, sort const & domain, sort const & range) {
3608  return range.ctx().function(name, domain, range);
3609  }
3610  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range) {
3611  return range.ctx().function(name, d1, d2, range);
3612  }
3613  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
3614  return range.ctx().function(name, d1, d2, d3, range);
3615  }
3616  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
3617  return range.ctx().function(name, d1, d2, d3, d4, range);
3618  }
3619  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range) {
3620  return range.ctx().function(name, d1, d2, d3, d4, d5, range);
3621  }
3622  inline func_decl function(char const* name, sort_vector const& domain, sort const& range) {
3623  return range.ctx().function(name, domain, range);
3624  }
3625  inline func_decl function(std::string const& name, sort_vector const& domain, sort const& range) {
3626  return range.ctx().function(name.c_str(), domain, range);
3627  }
3628 
3629  inline func_decl recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3630  return range.ctx().recfun(name, arity, domain, range);
3631  }
3632  inline func_decl recfun(char const * name, unsigned arity, sort const * domain, sort const & range) {
3633  return range.ctx().recfun(name, arity, domain, range);
3634  }
3635  inline func_decl