Z3
z3++.h
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4  Thin C++ layer on top of the Z3 C API.
5  Main features:
6  - Smart pointers for all Z3 objects.
7  - Object-Oriented interface.
8  - Operator overloading.
9  - Exceptions for signining Z3 errors
10 
11  The C API can be used simultaneously with the C++ layer.
12  However, if you use the C API directly, you will have to check the error conditions manually.
13  Of course, you can invoke the method check_error() of the context object.
14 Author:
15 
16  Leonardo (leonardo) 2012-03-28
17 
18 Notes:
19 
20 --*/
21 #ifndef Z3PP_H_
22 #define Z3PP_H_
23 
24 #include<cassert>
25 #include<iostream>
26 #include<string>
27 #include<sstream>
28 #include<z3.h>
29 #include<limits.h>
30 
31 #undef min
32 #undef max
33 
39 
44 
48 namespace z3 {
49 
50  class exception;
51  class config;
52  class context;
53  class symbol;
54  class params;
55  class param_descrs;
56  class ast;
57  class sort;
58  class func_decl;
59  class expr;
60  class solver;
61  class goal;
62  class tactic;
63  class probe;
64  class model;
65  class func_interp;
66  class func_entry;
67  class statistics;
68  class apply_result;
69  template<typename T> class ast_vector_tpl;
74 
75  inline void set_param(char const * param, char const * value) { Z3_global_param_set(param, value); }
76  inline void set_param(char const * param, bool value) { Z3_global_param_set(param, value ? "true" : "false"); }
77  inline void set_param(char const * param, int value) { std::ostringstream oss; oss << value; Z3_global_param_set(param, oss.str().c_str()); }
79 
83  class exception {
84  std::string m_msg;
85  public:
86  exception(char const * msg):m_msg(msg) {}
87  char const * msg() const { return m_msg.c_str(); }
88  friend std::ostream & operator<<(std::ostream & out, exception const & e);
89  };
90  inline std::ostream & operator<<(std::ostream & out, exception const & e) { out << e.msg(); return out; }
91 
92 #if !defined(Z3_THROW)
93 #if __cpp_exceptions || _CPPUNWIND || __EXCEPTIONS
94 #define Z3_THROW(x) throw x
95 #else
96 #define Z3_THROW(x) {}
97 #endif
98 #endif // !defined(Z3_THROW)
99 
103  class config {
104  Z3_config m_cfg;
105  config(config const & s);
106  config & operator=(config const & s);
107  public:
108  config() { m_cfg = Z3_mk_config(); }
109  ~config() { Z3_del_config(m_cfg); }
110  operator Z3_config() const { return m_cfg; }
114  void set(char const * param, char const * value) { Z3_set_param_value(m_cfg, param, value); }
118  void set(char const * param, bool value) { Z3_set_param_value(m_cfg, param, value ? "true" : "false"); }
122  void set(char const * param, int value) {
123  std::ostringstream oss;
124  oss << value;
125  Z3_set_param_value(m_cfg, param, oss.str().c_str());
126  }
127  };
128 
131  };
132 
139  };
140 
142  if (l == Z3_L_TRUE) return sat;
143  else if (l == Z3_L_FALSE) return unsat;
144  return unknown;
145  }
146 
147 
153  class context {
154  private:
155  bool m_enable_exceptions;
156  rounding_mode m_rounding_mode;
157  Z3_context m_ctx;
158  void init(config & c) {
159  m_ctx = Z3_mk_context_rc(c);
160  m_enable_exceptions = true;
161  m_rounding_mode = RNA;
162  Z3_set_error_handler(m_ctx, 0);
164  }
165 
166 
167  context(context const & s);
168  context & operator=(context const & s);
169  public:
170  context() { config c; init(c); }
171  context(config & c) { init(c); }
172  ~context() { Z3_del_context(m_ctx); }
173  operator Z3_context() const { return m_ctx; }
174 
179  Z3_error_code e = Z3_get_error_code(m_ctx);
180  if (e != Z3_OK && enable_exceptions())
181  Z3_THROW(exception(Z3_get_error_msg(m_ctx, e)));
182  return e;
183  }
184 
185  void check_parser_error() const {
186  check_error();
187  }
188 
196  void set_enable_exceptions(bool f) { m_enable_exceptions = f; }
197 
198  bool enable_exceptions() const { return m_enable_exceptions; }
199 
203  void set(char const * param, char const * value) { Z3_update_param_value(m_ctx, param, value); }
207  void set(char const * param, bool value) { Z3_update_param_value(m_ctx, param, value ? "true" : "false"); }
211  void set(char const * param, int value) {
212  std::ostringstream oss;
213  oss << value;
214  Z3_update_param_value(m_ctx, param, oss.str().c_str());
215  }
216 
221  void interrupt() { Z3_interrupt(m_ctx); }
222 
226  symbol str_symbol(char const * s);
230  symbol int_symbol(int n);
234  sort bool_sort();
238  sort int_sort();
242  sort real_sort();
246  sort bv_sort(unsigned sz);
250  sort string_sort();
254  sort seq_sort(sort& s);
264  sort array_sort(sort d, sort r);
265  sort array_sort(sort_vector const& d, sort r);
272  sort fpa_sort(unsigned ebits, unsigned sbits);
276  template<size_t precision>
277  sort fpa_sort();
291  sort enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts);
292 
299  func_decl tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs);
300 
304  sort uninterpreted_sort(char const* name);
305  sort uninterpreted_sort(symbol const& name);
306 
307  func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range);
308  func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range);
309  func_decl function(symbol const& name, sort_vector const& domain, sort const& range);
310  func_decl function(char const * name, sort_vector const& domain, sort const& range);
311  func_decl function(char const * name, sort const & domain, sort const & range);
312  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range);
313  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range);
314  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range);
315  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range);
316 
317  func_decl recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range);
318  func_decl recfun(char const * name, unsigned arity, sort const * domain, sort const & range);
319  func_decl recfun(char const * name, sort const & domain, sort const & range);
320  func_decl recfun(char const * name, sort const & d1, sort const & d2, sort const & range);
321 
322  void recdef(func_decl, expr_vector const& args, expr const& body);
323 
324  expr constant(symbol const & name, sort const & s);
325  expr constant(char const * name, sort const & s);
326  expr bool_const(char const * name);
327  expr int_const(char const * name);
328  expr real_const(char const * name);
329  expr bv_const(char const * name, unsigned sz);
330  expr fpa_const(char const * name, unsigned ebits, unsigned sbits);
331 
332  template<size_t precision>
333  expr fpa_const(char const * name);
334 
335  expr bool_val(bool b);
336 
337  expr int_val(int n);
338  expr int_val(unsigned n);
339  expr int_val(int64_t n);
340  expr int_val(uint64_t n);
341  expr int_val(char const * n);
342 
343  expr real_val(int n, int d);
344  expr real_val(int n);
345  expr real_val(unsigned n);
346  expr real_val(int64_t n);
347  expr real_val(uint64_t n);
348  expr real_val(char const * n);
349 
350  expr bv_val(int n, unsigned sz);
351  expr bv_val(unsigned n, unsigned sz);
352  expr bv_val(int64_t n, unsigned sz);
353  expr bv_val(uint64_t n, unsigned sz);
354  expr bv_val(char const * n, unsigned sz);
355  expr bv_val(unsigned n, bool const* bits);
356 
357  expr fpa_val(double n);
358  expr fpa_val(float n);
359 
360  expr string_val(char const* s);
361  expr string_val(std::string const& s);
362 
363  expr num_val(int n, sort const & s);
364 
368  expr_vector parse_string(char const* s);
369  expr_vector parse_file(char const* file);
370 
371  expr_vector parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
372  expr_vector parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
373 
374 
375  };
376 
377 
378 
379 
380  template<typename T>
381  class array {
382  T * m_array;
383  unsigned m_size;
384  array(array const & s);
385  array & operator=(array const & s);
386  public:
387  array(unsigned sz):m_size(sz) { m_array = new T[sz]; }
388  template<typename T2>
389  array(ast_vector_tpl<T2> const & v);
390  ~array() { delete[] m_array; }
391  unsigned size() const { return m_size; }
392  T & operator[](int i) { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
393  T const & operator[](int i) const { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
394  T const * ptr() const { return m_array; }
395  T * ptr() { return m_array; }
396  };
397 
398  class object {
399  protected:
401  public:
402  object(context & c):m_ctx(&c) {}
403  object(object const & s):m_ctx(s.m_ctx) {}
404  context & ctx() const { return *m_ctx; }
406  friend void check_context(object const & a, object const & b);
407  };
408  inline void check_context(object const & a, object const & b) { (void)a; (void)b; assert(a.m_ctx == b.m_ctx); }
409 
410  class symbol : public object {
411  Z3_symbol m_sym;
412  public:
413  symbol(context & c, Z3_symbol s):object(c), m_sym(s) {}
414  symbol(symbol const & s):object(s), m_sym(s.m_sym) {}
415  symbol & operator=(symbol const & s) { m_ctx = s.m_ctx; m_sym = s.m_sym; return *this; }
416  operator Z3_symbol() const { return m_sym; }
417  Z3_symbol_kind kind() const { return Z3_get_symbol_kind(ctx(), m_sym); }
418  std::string str() const { assert(kind() == Z3_STRING_SYMBOL); return Z3_get_symbol_string(ctx(), m_sym); }
419  int to_int() const { assert(kind() == Z3_INT_SYMBOL); return Z3_get_symbol_int(ctx(), m_sym); }
420  friend std::ostream & operator<<(std::ostream & out, symbol const & s);
421  };
422 
423  inline std::ostream & operator<<(std::ostream & out, symbol const & s) {
424  if (s.kind() == Z3_INT_SYMBOL)
425  out << "k!" << s.to_int();
426  else
427  out << s.str().c_str();
428  return out;
429  }
430 
431 
432  class param_descrs : public object {
433  Z3_param_descrs m_descrs;
434  public:
435  param_descrs(context& c, Z3_param_descrs d): object(c), m_descrs(d) { Z3_param_descrs_inc_ref(c, d); }
436  param_descrs(param_descrs const& o): object(o.ctx()), m_descrs(o.m_descrs) { Z3_param_descrs_inc_ref(ctx(), m_descrs); }
438  Z3_param_descrs_inc_ref(o.ctx(), o.m_descrs);
439  Z3_param_descrs_dec_ref(ctx(), m_descrs);
440  m_descrs = o.m_descrs;
441  m_ctx = o.m_ctx;
442  return *this;
443  }
446 
447  unsigned size() { return Z3_param_descrs_size(ctx(), m_descrs); }
448  symbol name(unsigned i) { return symbol(ctx(), Z3_param_descrs_get_name(ctx(), m_descrs, i)); }
449  Z3_param_kind kind(symbol const& s) { return Z3_param_descrs_get_kind(ctx(), m_descrs, s); }
450  std::string documentation(symbol const& s) { char const* r = Z3_param_descrs_get_documentation(ctx(), m_descrs, s); check_error(); return r; }
451  std::string to_string() const { return Z3_param_descrs_to_string(ctx(), m_descrs); }
452  };
453 
454  inline std::ostream& operator<<(std::ostream & out, param_descrs const & d) { return out << d.to_string(); }
455 
456  class params : public object {
457  Z3_params m_params;
458  public:
459  params(context & c):object(c) { m_params = Z3_mk_params(c); Z3_params_inc_ref(ctx(), m_params); }
460  params(params const & s):object(s), m_params(s.m_params) { Z3_params_inc_ref(ctx(), m_params); }
461  ~params() { Z3_params_dec_ref(ctx(), m_params); }
462  operator Z3_params() const { return m_params; }
463  params & operator=(params const & s) {
464  Z3_params_inc_ref(s.ctx(), s.m_params);
465  Z3_params_dec_ref(ctx(), m_params);
466  m_ctx = s.m_ctx;
467  m_params = s.m_params;
468  return *this;
469  }
470  void set(char const * k, bool b) { Z3_params_set_bool(ctx(), m_params, ctx().str_symbol(k), b); }
471  void set(char const * k, unsigned n) { Z3_params_set_uint(ctx(), m_params, ctx().str_symbol(k), n); }
472  void set(char const * k, double n) { Z3_params_set_double(ctx(), m_params, ctx().str_symbol(k), n); }
473  void set(char const * k, symbol const & s) { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), s); }
474  void set(char const * k, char const* s) { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), ctx().str_symbol(s)); }
475  friend std::ostream & operator<<(std::ostream & out, params const & p);
476  };
477 
478  inline std::ostream & operator<<(std::ostream & out, params const & p) {
479  out << Z3_params_to_string(p.ctx(), p); return out;
480  }
481 
482  class ast : public object {
483  protected:
484  Z3_ast m_ast;
485  public:
486  ast(context & c):object(c), m_ast(0) {}
487  ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
488  ast(ast const & s):object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
489  ~ast() { if (m_ast) Z3_dec_ref(*m_ctx, m_ast); }
490  operator Z3_ast() const { return m_ast; }
491  operator bool() const { return m_ast != 0; }
492  ast & operator=(ast const & s) { Z3_inc_ref(s.ctx(), s.m_ast); if (m_ast) Z3_dec_ref(ctx(), m_ast); m_ctx = s.m_ctx; m_ast = s.m_ast; return *this; }
493  Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }
494  unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }
495  friend std::ostream & operator<<(std::ostream & out, ast const & n);
496  std::string to_string() const { return std::string(Z3_ast_to_string(ctx(), m_ast)); }
497 
498 
502  friend bool eq(ast const & a, ast const & b);
503  };
504  inline std::ostream & operator<<(std::ostream & out, ast const & n) {
505  out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
506  }
507 
508  inline bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b); }
509 
510 
514  class sort : public ast {
515  public:
516  sort(context & c):ast(c) {}
517  sort(context & c, Z3_sort s):ast(c, reinterpret_cast<Z3_ast>(s)) {}
518  sort(context & c, Z3_ast a):ast(c, a) {}
519  sort(sort const & s):ast(s) {}
520  operator Z3_sort() const { return reinterpret_cast<Z3_sort>(m_ast); }
524  sort & operator=(sort const & s) { return static_cast<sort&>(ast::operator=(s)); }
528  Z3_sort_kind sort_kind() const { return Z3_get_sort_kind(*m_ctx, *this); }
532  symbol name() const { Z3_symbol s = Z3_get_sort_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
536  bool is_bool() const { return sort_kind() == Z3_BOOL_SORT; }
540  bool is_int() const { return sort_kind() == Z3_INT_SORT; }
544  bool is_real() const { return sort_kind() == Z3_REAL_SORT; }
548  bool is_arith() const { return is_int() || is_real(); }
552  bool is_bv() const { return sort_kind() == Z3_BV_SORT; }
556  bool is_array() const { return sort_kind() == Z3_ARRAY_SORT; }
560  bool is_datatype() const { return sort_kind() == Z3_DATATYPE_SORT; }
564  bool is_relation() const { return sort_kind() == Z3_RELATION_SORT; }
568  bool is_seq() const { return sort_kind() == Z3_SEQ_SORT; }
572  bool is_re() const { return sort_kind() == Z3_RE_SORT; }
576  bool is_finite_domain() const { return sort_kind() == Z3_FINITE_DOMAIN_SORT; }
580  bool is_fpa() const { return sort_kind() == Z3_FLOATING_POINT_SORT; }
581 
587  unsigned bv_size() const { assert(is_bv()); unsigned r = Z3_get_bv_sort_size(ctx(), *this); check_error(); return r; }
588 
589  unsigned fpa_ebits() const { assert(is_fpa()); unsigned r = Z3_fpa_get_ebits(ctx(), *this); check_error(); return r; }
590 
591  unsigned fpa_sbits() const { assert(is_fpa()); unsigned r = Z3_fpa_get_sbits(ctx(), *this); check_error(); return r; }
597  sort array_domain() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_domain(ctx(), *this); check_error(); return sort(ctx(), s); }
603  sort array_range() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_range(ctx(), *this); check_error(); return sort(ctx(), s); }
604  };
605 
610  class func_decl : public ast {
611  public:
612  func_decl(context & c):ast(c) {}
613  func_decl(context & c, Z3_func_decl n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
614  func_decl(func_decl const & s):ast(s) {}
615  operator Z3_func_decl() const { return reinterpret_cast<Z3_func_decl>(m_ast); }
616  func_decl & operator=(func_decl const & s) { return static_cast<func_decl&>(ast::operator=(s)); }
617 
618  unsigned arity() const { return Z3_get_arity(ctx(), *this); }
619  sort domain(unsigned i) const { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }
620  sort range() const { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }
621  symbol name() const { Z3_symbol s = Z3_get_decl_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
622  Z3_decl_kind decl_kind() const { return Z3_get_decl_kind(ctx(), *this); }
623 
624  bool is_const() const { return arity() == 0; }
625 
626  expr operator()() const;
627  expr operator()(unsigned n, expr const * args) const;
628  expr operator()(expr_vector const& v) const;
629  expr operator()(expr const & a) const;
630  expr operator()(int a) const;
631  expr operator()(expr const & a1, expr const & a2) const;
632  expr operator()(expr const & a1, int a2) const;
633  expr operator()(int a1, expr const & a2) const;
634  expr operator()(expr const & a1, expr const & a2, expr const & a3) const;
635  expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const;
636  expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const;
637  };
638 
643  class expr : public ast {
644  public:
645  expr(context & c):ast(c) {}
646  expr(context & c, Z3_ast n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
647  expr(expr const & n):ast(n) {}
648  expr & operator=(expr const & n) { return static_cast<expr&>(ast::operator=(n)); }
649 
653  sort get_sort() const { Z3_sort s = Z3_get_sort(*m_ctx, m_ast); check_error(); return sort(*m_ctx, s); }
654 
658  bool is_bool() const { return get_sort().is_bool(); }
662  bool is_int() const { return get_sort().is_int(); }
666  bool is_real() const { return get_sort().is_real(); }
670  bool is_arith() const { return get_sort().is_arith(); }
674  bool is_bv() const { return get_sort().is_bv(); }
678  bool is_array() const { return get_sort().is_array(); }
682  bool is_datatype() const { return get_sort().is_datatype(); }
686  bool is_relation() const { return get_sort().is_relation(); }
690  bool is_seq() const { return get_sort().is_seq(); }
694  bool is_re() const { return get_sort().is_re(); }
695 
704  bool is_finite_domain() const { return get_sort().is_finite_domain(); }
708  bool is_fpa() const { return get_sort().is_fpa(); }
709 
715  bool is_numeral() const { return kind() == Z3_NUMERAL_AST; }
716  bool is_numeral_i64(int64_t& i) const { bool r = Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}
717  bool is_numeral_u64(uint64_t& i) const { bool r = Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}
718  bool is_numeral_i(int& i) const { bool r = Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}
719  bool is_numeral_u(unsigned& i) const { bool r = Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
720  bool is_numeral(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; }
721  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; }
722  bool is_numeral(double& d) const { if (!is_numeral()) return false; d = Z3_get_numeral_double(ctx(), m_ast); check_error(); return true; }
726  bool is_app() const { return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
730  bool is_const() const { return is_app() && num_args() == 0; }
734  bool is_quantifier() const { return kind() == Z3_QUANTIFIER_AST; }
735 
739  bool is_forall() const { return Z3_is_quantifier_forall(ctx(), m_ast); }
743  bool is_exists() const { return Z3_is_quantifier_exists(ctx(), m_ast); }
747  bool is_lambda() const { return Z3_is_lambda(ctx(), m_ast); }
752  bool is_var() const { return kind() == Z3_VAR_AST; }
756  bool is_algebraic() const { return Z3_is_algebraic_number(ctx(), m_ast); }
757 
761  bool is_well_sorted() const { bool r = Z3_is_well_sorted(ctx(), m_ast); check_error(); return r; }
762 
769  std::string get_decimal_string(int precision) const {
770  assert(is_numeral() || is_algebraic());
771  return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
772  }
773 
784  int get_numeral_int() const {
785  int result = 0;
786  if (!is_numeral_i(result)) {
787  assert(ctx().enable_exceptions());
788  if (!ctx().enable_exceptions()) return 0;
789  Z3_THROW(exception("numeral does not fit in machine int"));
790  }
791  return result;
792  }
793 
803  unsigned get_numeral_uint() const {
804  assert(is_numeral());
805  unsigned result = 0;
806  if (!is_numeral_u(result)) {
807  assert(ctx().enable_exceptions());
808  if (!ctx().enable_exceptions()) return 0;
809  Z3_THROW(exception("numeral does not fit in machine uint"));
810  }
811  return result;
812  }
813 
820  int64_t get_numeral_int64() const {
821  assert(is_numeral());
822  int64_t result = 0;
823  if (!is_numeral_i64(result)) {
824  assert(ctx().enable_exceptions());
825  if (!ctx().enable_exceptions()) return 0;
826  Z3_THROW(exception("numeral does not fit in machine int64_t"));
827  }
828  return result;
829  }
830 
837  uint64_t get_numeral_uint64() const {
838  assert(is_numeral());
839  uint64_t result = 0;
840  if (!is_numeral_u64(result)) {
841  assert(ctx().enable_exceptions());
842  if (!ctx().enable_exceptions()) return 0;
843  Z3_THROW(exception("numeral does not fit in machine uint64_t"));
844  }
845  return result;
846  }
847 
849  return Z3_get_bool_value(ctx(), m_ast);
850  }
851 
852  expr numerator() const {
853  assert(is_numeral());
854  Z3_ast r = Z3_get_numerator(ctx(), m_ast);
855  check_error();
856  return expr(ctx(),r);
857  }
858 
859 
860  expr denominator() const {
861  assert(is_numeral());
862  Z3_ast r = Z3_get_denominator(ctx(), m_ast);
863  check_error();
864  return expr(ctx(),r);
865  }
866 
867  operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
868 
873  assert(is_fpa());
874  Z3_sort s = ctx().fpa_rounding_mode();
875  check_error();
876  return sort(ctx(), s);
877  }
878 
879 
886  func_decl decl() const { Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }
893  unsigned num_args() const { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
901  expr arg(unsigned i) const { Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }
902 
908  expr body() const { assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
909 
915  friend expr operator!(expr const & a);
916 
923  friend expr operator&&(expr const & a, expr const & b);
924 
925 
932  friend expr operator&&(expr const & a, bool b);
939  friend expr operator&&(bool a, expr const & b);
940 
947  friend expr operator||(expr const & a, expr const & b);
954  friend expr operator||(expr const & a, bool b);
955 
962  friend expr operator||(bool a, expr const & b);
963 
964  friend expr implies(expr const & a, expr const & b);
965  friend expr implies(expr const & a, bool b);
966  friend expr implies(bool a, expr const & b);
967 
968  friend expr mk_or(expr_vector const& args);
969  friend expr mk_and(expr_vector const& args);
970 
971  friend expr ite(expr const & c, expr const & t, expr const & e);
972 
973  bool is_true() const { return is_app() && Z3_OP_TRUE == decl().decl_kind(); }
974  bool is_false() const { return is_app() && Z3_OP_FALSE == decl().decl_kind(); }
975  bool is_not() const { return is_app() && Z3_OP_NOT == decl().decl_kind(); }
976  bool is_and() const { return is_app() && Z3_OP_AND == decl().decl_kind(); }
977  bool is_or() const { return is_app() && Z3_OP_OR == decl().decl_kind(); }
978  bool is_xor() const { return is_app() && Z3_OP_XOR == decl().decl_kind(); }
979  bool is_implies() const { return is_app() && Z3_OP_IMPLIES == decl().decl_kind(); }
980  bool is_eq() const { return is_app() && Z3_OP_EQ == decl().decl_kind(); }
981  bool is_ite() const { return is_app() && Z3_OP_ITE == decl().decl_kind(); }
982 
983  friend expr distinct(expr_vector const& args);
984  friend expr concat(expr const& a, expr const& b);
985  friend expr concat(expr_vector const& args);
986 
987  friend expr operator==(expr const & a, expr const & b);
988  friend expr operator==(expr const & a, int b);
989  friend expr operator==(int a, expr const & b);
990 
991  friend expr operator!=(expr const & a, expr const & b);
992  friend expr operator!=(expr const & a, int b);
993  friend expr operator!=(int a, expr const & b);
994 
995  friend expr operator+(expr const & a, expr const & b);
996  friend expr operator+(expr const & a, int b);
997  friend expr operator+(int a, expr const & b);
998  friend expr sum(expr_vector const& args);
999 
1000  friend expr operator*(expr const & a, expr const & b);
1001  friend expr operator*(expr const & a, int b);
1002  friend expr operator*(int a, expr const & b);
1003 
1004  /* \brief Power operator */
1005  friend expr pw(expr const & a, expr const & b);
1006  friend expr pw(expr const & a, int b);
1007  friend expr pw(int a, expr const & b);
1008 
1009  /* \brief mod operator */
1010  friend expr mod(expr const& a, expr const& b);
1011  friend expr mod(expr const& a, int b);
1012  friend expr mod(int a, expr const& b);
1013 
1014  /* \brief rem operator */
1015  friend expr rem(expr const& a, expr const& b);
1016  friend expr rem(expr const& a, int b);
1017  friend expr rem(int a, expr const& b);
1018 
1019  friend expr is_int(expr const& e);
1020 
1021  friend expr operator/(expr const & a, expr const & b);
1022  friend expr operator/(expr const & a, int b);
1023  friend expr operator/(int a, expr const & b);
1024 
1025  friend expr operator-(expr const & a);
1026 
1027  friend expr operator-(expr const & a, expr const & b);
1028  friend expr operator-(expr const & a, int b);
1029  friend expr operator-(int a, expr const & b);
1030 
1031  friend expr operator<=(expr const & a, expr const & b);
1032  friend expr operator<=(expr const & a, int b);
1033  friend expr operator<=(int a, expr const & b);
1034 
1035 
1036  friend expr operator>=(expr const & a, expr const & b);
1037  friend expr operator>=(expr const & a, int b);
1038  friend expr operator>=(int a, expr const & b);
1039 
1040  friend expr operator<(expr const & a, expr const & b);
1041  friend expr operator<(expr const & a, int b);
1042  friend expr operator<(int a, expr const & b);
1043 
1044  friend expr operator>(expr const & a, expr const & b);
1045  friend expr operator>(expr const & a, int b);
1046  friend expr operator>(int a, expr const & b);
1047 
1048  friend expr pble(expr_vector const& es, int const * coeffs, int bound);
1049  friend expr pbge(expr_vector const& es, int const * coeffs, int bound);
1050  friend expr pbeq(expr_vector const& es, int const * coeffs, int bound);
1051  friend expr atmost(expr_vector const& es, unsigned bound);
1052  friend expr atleast(expr_vector const& es, unsigned bound);
1053 
1054  friend expr operator&(expr const & a, expr const & b);
1055  friend expr operator&(expr const & a, int b);
1056  friend expr operator&(int a, expr const & b);
1057 
1058  friend expr operator^(expr const & a, expr const & b);
1059  friend expr operator^(expr const & a, int b);
1060  friend expr operator^(int a, expr const & b);
1061 
1062  friend expr operator|(expr const & a, expr const & b);
1063  friend expr operator|(expr const & a, int b);
1064  friend expr operator|(int a, expr const & b);
1065  friend expr nand(expr const& a, expr const& b);
1066  friend expr nor(expr const& a, expr const& b);
1067  friend expr xnor(expr const& a, expr const& b);
1068 
1069  friend expr min(expr const& a, expr const& b);
1070  friend expr max(expr const& a, expr const& b);
1071 
1072  expr rotate_left(unsigned i) { Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
1073  expr rotate_right(unsigned i) { Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
1074  expr repeat(unsigned i) { Z3_ast r = Z3_mk_repeat(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
1075 
1076  friend expr abs(expr const & a);
1077  friend expr sqrt(expr const & a, expr const & rm);
1078 
1079  friend expr operator~(expr const & a);
1080  expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }
1081  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)); }
1082  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)); }
1083 
1087  friend expr fma(expr const& a, expr const& b, expr const& c);
1088 
1094  expr extract(expr const& offset, expr const& length) const {
1095  check_context(*this, offset); check_context(offset, length);
1096  Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
1097  }
1098  expr replace(expr const& src, expr const& dst) const {
1099  check_context(*this, src); check_context(src, dst);
1100  Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
1101  check_error();
1102  return expr(ctx(), r);
1103  }
1104  expr unit() const {
1105  Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
1106  check_error();
1107  return expr(ctx(), r);
1108  }
1109  expr contains(expr const& s) {
1110  check_context(*this, s);
1111  Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
1112  check_error();
1113  return expr(ctx(), r);
1114  }
1115  expr at(expr const& index) const {
1116  check_context(*this, index);
1117  Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
1118  check_error();
1119  return expr(ctx(), r);
1120  }
1121  expr length() const {
1122  Z3_ast r = Z3_mk_seq_length(ctx(), *this);
1123  check_error();
1124  return expr(ctx(), r);
1125  }
1126  expr stoi() const {
1127  Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
1128  check_error();
1129  return expr(ctx(), r);
1130  }
1131  expr itos() const {
1132  Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
1133  check_error();
1134  return expr(ctx(), r);
1135  }
1136 
1137  friend expr range(expr const& lo, expr const& hi);
1141  expr loop(unsigned lo) {
1142  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0);
1143  check_error();
1144  return expr(ctx(), r);
1145  }
1146  expr loop(unsigned lo, unsigned hi) {
1147  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi);
1148  check_error();
1149  return expr(ctx(), r);
1150  }
1151 
1152 
1156  expr simplify() const { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
1160  expr simplify(params const & p) const { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
1161 
1165  expr substitute(expr_vector const& src, expr_vector const& dst);
1166 
1170  expr substitute(expr_vector const& dst);
1171 
1172  };
1173 
1174 #define _Z3_MK_BIN_(a, b, binop) \
1175  check_context(a, b); \
1176  Z3_ast r = binop(a.ctx(), a, b); \
1177  a.check_error(); \
1178  return expr(a.ctx(), r); \
1179 
1180 
1181  inline expr implies(expr const & a, expr const & b) {
1182  assert(a.is_bool() && b.is_bool());
1183  _Z3_MK_BIN_(a, b, Z3_mk_implies);
1184  }
1185  inline expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); }
1186  inline expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); }
1187 
1188 
1189  inline expr pw(expr const & a, expr const & b) { _Z3_MK_BIN_(a, b, Z3_mk_power); }
1190  inline expr pw(expr const & a, int b) { return pw(a, a.ctx().num_val(b, a.get_sort())); }
1191  inline expr pw(int a, expr const & b) { return pw(b.ctx().num_val(a, b.get_sort()), b); }
1192 
1193  inline expr mod(expr const& a, expr const& b) { _Z3_MK_BIN_(a, b, Z3_mk_mod); }
1194  inline expr mod(expr const & a, int b) { return mod(a, a.ctx().num_val(b, a.get_sort())); }
1195  inline expr mod(int a, expr const & b) { return mod(b.ctx().num_val(a, b.get_sort()), b); }
1196 
1197  inline expr rem(expr const& a, expr const& b) {
1198  if (a.is_fpa() && b.is_fpa()) {
1199  _Z3_MK_BIN_(a, b, Z3_mk_fpa_rem);
1200  } else {
1201  _Z3_MK_BIN_(a, b, Z3_mk_rem);
1202  }
1203  }
1204  inline expr rem(expr const & a, int b) { return rem(a, a.ctx().num_val(b, a.get_sort())); }
1205  inline expr rem(int a, expr const & b) { return rem(b.ctx().num_val(a, b.get_sort()), b); }
1206 
1207 #undef _Z3_MK_BIN_
1208 
1209 #define _Z3_MK_UN_(a, mkun) \
1210  Z3_ast r = mkun(a.ctx(), a); \
1211  a.check_error(); \
1212  return expr(a.ctx(), r); \
1213 
1214 
1215  inline expr operator!(expr const & a) { assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); }
1216 
1217  inline expr is_int(expr const& e) { _Z3_MK_UN_(e, Z3_mk_is_int); }
1218 
1219 #undef _Z3_MK_UN_
1220 
1221  inline expr operator&&(expr const & a, expr const & b) {
1222  check_context(a, b);
1223  assert(a.is_bool() && b.is_bool());
1224  Z3_ast args[2] = { a, b };
1225  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1226  a.check_error();
1227  return expr(a.ctx(), r);
1228  }
1229 
1230  inline expr operator&&(expr const & a, bool b) { return a && a.ctx().bool_val(b); }
1231  inline expr operator&&(bool a, expr const & b) { return b.ctx().bool_val(a) && b; }
1232 
1233  inline expr operator||(expr const & a, expr const & b) {
1234  check_context(a, b);
1235  assert(a.is_bool() && b.is_bool());
1236  Z3_ast args[2] = { a, b };
1237  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1238  a.check_error();
1239  return expr(a.ctx(), r);
1240  }
1241 
1242  inline expr operator||(expr const & a, bool b) { return a || a.ctx().bool_val(b); }
1243 
1244  inline expr operator||(bool a, expr const & b) { return b.ctx().bool_val(a) || b; }
1245 
1246  inline expr operator==(expr const & a, expr const & b) {
1247  check_context(a, b);
1248  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1249  a.check_error();
1250  return expr(a.ctx(), r);
1251  }
1252  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()); }
1253  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; }
1254 
1255  inline expr operator!=(expr const & a, expr const & b) {
1256  check_context(a, b);
1257  Z3_ast args[2] = { a, b };
1258  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1259  a.check_error();
1260  return expr(a.ctx(), r);
1261  }
1262  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()); }
1263  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; }
1264 
1265  inline expr operator+(expr const & a, expr const & b) {
1266  check_context(a, b);
1267  Z3_ast r = 0;
1268  if (a.is_arith() && b.is_arith()) {
1269  Z3_ast args[2] = { a, b };
1270  r = Z3_mk_add(a.ctx(), 2, args);
1271  }
1272  else if (a.is_bv() && b.is_bv()) {
1273  r = Z3_mk_bvadd(a.ctx(), a, b);
1274  }
1275  else if (a.is_seq() && b.is_seq()) {
1276  return concat(a, b);
1277  }
1278  else if (a.is_re() && b.is_re()) {
1279  Z3_ast _args[2] = { a, b };
1280  r = Z3_mk_re_union(a.ctx(), 2, _args);
1281  }
1282  else if (a.is_fpa() && b.is_fpa()) {
1283  r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1284  }
1285  else {
1286  // operator is not supported by given arguments.
1287  assert(false);
1288  }
1289  a.check_error();
1290  return expr(a.ctx(), r);
1291  }
1292  inline expr operator+(expr const & a, int b) { return a + a.ctx().num_val(b, a.get_sort()); }
1293  inline expr operator+(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) + b; }
1294 
1295  inline expr operator*(expr const & a, expr const & b) {
1296  check_context(a, b);
1297  Z3_ast r = 0;
1298  if (a.is_arith() && b.is_arith()) {
1299  Z3_ast args[2] = { a, b };
1300  r = Z3_mk_mul(a.ctx(), 2, args);
1301  }
1302  else if (a.is_bv() && b.is_bv()) {
1303  r = Z3_mk_bvmul(a.ctx(), a, b);
1304  }
1305  else if (a.is_fpa() && b.is_fpa()) {
1306  r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1307  }
1308  else {
1309  // operator is not supported by given arguments.
1310  assert(false);
1311  }
1312  a.check_error();
1313  return expr(a.ctx(), r);
1314  }
1315  inline expr operator*(expr const & a, int b) { return a * a.ctx().num_val(b, a.get_sort()); }
1316  inline expr operator*(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) * b; }
1317 
1318 
1319  inline expr operator>=(expr const & a, expr const & b) {
1320  check_context(a, b);
1321  Z3_ast r = 0;
1322  if (a.is_arith() && b.is_arith()) {
1323  r = Z3_mk_ge(a.ctx(), a, b);
1324  }
1325  else if (a.is_bv() && b.is_bv()) {
1326  r = Z3_mk_bvsge(a.ctx(), a, b);
1327  }
1328  else {
1329  // operator is not supported by given arguments.
1330  assert(false);
1331  }
1332  a.check_error();
1333  return expr(a.ctx(), r);
1334  }
1335 
1336  inline expr operator/(expr const & a, expr const & b) {
1337  check_context(a, b);
1338  Z3_ast r = 0;
1339  if (a.is_arith() && b.is_arith()) {
1340  r = Z3_mk_div(a.ctx(), a, b);
1341  }
1342  else if (a.is_bv() && b.is_bv()) {
1343  r = Z3_mk_bvsdiv(a.ctx(), a, b);
1344  }
1345  else if (a.is_fpa() && b.is_fpa()) {
1346  r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1347  }
1348  else {
1349  // operator is not supported by given arguments.
1350  assert(false);
1351  }
1352  a.check_error();
1353  return expr(a.ctx(), r);
1354  }
1355  inline expr operator/(expr const & a, int b) { return a / a.ctx().num_val(b, a.get_sort()); }
1356  inline expr operator/(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) / b; }
1357 
1358  inline expr operator-(expr const & a) {
1359  Z3_ast r = 0;
1360  if (a.is_arith()) {
1361  r = Z3_mk_unary_minus(a.ctx(), a);
1362  }
1363  else if (a.is_bv()) {
1364  r = Z3_mk_bvneg(a.ctx(), a);
1365  }
1366  else if (a.is_fpa()) {
1367  r = Z3_mk_fpa_neg(a.ctx(), a);
1368  }
1369  else {
1370  // operator is not supported by given arguments.
1371  assert(false);
1372  }
1373  a.check_error();
1374  return expr(a.ctx(), r);
1375  }
1376 
1377  inline expr operator-(expr const & a, expr const & b) {
1378  check_context(a, b);
1379  Z3_ast r = 0;
1380  if (a.is_arith() && b.is_arith()) {
1381  Z3_ast args[2] = { a, b };
1382  r = Z3_mk_sub(a.ctx(), 2, args);
1383  }
1384  else if (a.is_bv() && b.is_bv()) {
1385  r = Z3_mk_bvsub(a.ctx(), a, b);
1386  }
1387  else if (a.is_fpa() && b.is_fpa()) {
1388  r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1389  }
1390  else {
1391  // operator is not supported by given arguments.
1392  assert(false);
1393  }
1394  a.check_error();
1395  return expr(a.ctx(), r);
1396  }
1397  inline expr operator-(expr const & a, int b) { return a - a.ctx().num_val(b, a.get_sort()); }
1398  inline expr operator-(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) - b; }
1399 
1400  inline expr operator<=(expr const & a, expr const & b) {
1401  check_context(a, b);
1402  Z3_ast r = 0;
1403  if (a.is_arith() && b.is_arith()) {
1404  r = Z3_mk_le(a.ctx(), a, b);
1405  }
1406  else if (a.is_bv() && b.is_bv()) {
1407  r = Z3_mk_bvsle(a.ctx(), a, b);
1408  }
1409  else if (a.is_fpa() && b.is_fpa()) {
1410  r = Z3_mk_fpa_leq(a.ctx(), a, b);
1411  }
1412  else {
1413  // operator is not supported by given arguments.
1414  assert(false);
1415  }
1416  a.check_error();
1417  return expr(a.ctx(), r);
1418  }
1419  inline expr operator<=(expr const & a, int b) { return a <= a.ctx().num_val(b, a.get_sort()); }
1420  inline expr operator<=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) <= b; }
1421 
1422  inline expr operator>=(expr const & a, int b) { return a >= a.ctx().num_val(b, a.get_sort()); }
1423  inline expr operator>=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) >= b; }
1424 
1425  inline expr operator<(expr const & a, expr const & b) {
1426  check_context(a, b);
1427  Z3_ast r = 0;
1428  if (a.is_arith() && b.is_arith()) {
1429  r = Z3_mk_lt(a.ctx(), a, b);
1430  }
1431  else if (a.is_bv() && b.is_bv()) {
1432  r = Z3_mk_bvslt(a.ctx(), a, b);
1433  }
1434  else if (a.is_fpa() && b.is_fpa()) {
1435  r = Z3_mk_fpa_lt(a.ctx(), a, b);
1436  }
1437  else {
1438  // operator is not supported by given arguments.
1439  assert(false);
1440  }
1441  a.check_error();
1442  return expr(a.ctx(), r);
1443  }
1444  inline expr operator<(expr const & a, int b) { return a < a.ctx().num_val(b, a.get_sort()); }
1445  inline expr operator<(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) < b; }
1446 
1447  inline expr operator>(expr const & a, expr const & b) {
1448  check_context(a, b);
1449  Z3_ast r = 0;
1450  if (a.is_arith() && b.is_arith()) {
1451  r = Z3_mk_gt(a.ctx(), a, b);
1452  }
1453  else if (a.is_bv() && b.is_bv()) {
1454  r = Z3_mk_bvsgt(a.ctx(), a, b);
1455  }
1456  else if (a.is_fpa() && b.is_fpa()) {
1457  r = Z3_mk_fpa_gt(a.ctx(), a, b);
1458  }
1459  else {
1460  // operator is not supported by given arguments.
1461  assert(false);
1462  }
1463  a.check_error();
1464  return expr(a.ctx(), r);
1465  }
1466  inline expr operator>(expr const & a, int b) { return a > a.ctx().num_val(b, a.get_sort()); }
1467  inline expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > b; }
1468 
1469  inline expr operator&(expr const & a, expr const & b) { check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); return expr(a.ctx(), r); }
1470  inline expr operator&(expr const & a, int b) { return a & a.ctx().num_val(b, a.get_sort()); }
1471  inline expr operator&(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) & b; }
1472 
1473  inline expr operator^(expr const & a, expr const & b) { check_context(a, b); Z3_ast r = Z3_mk_bvxor(a.ctx(), a, b); return expr(a.ctx(), r); }
1474  inline expr operator^(expr const & a, int b) { return a ^ a.ctx().num_val(b, a.get_sort()); }
1475  inline expr operator^(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) ^ b; }
1476 
1477  inline expr operator|(expr const & a, expr const & b) { check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); return expr(a.ctx(), r); }
1478  inline expr operator|(expr const & a, int b) { return a | a.ctx().num_val(b, a.get_sort()); }
1479  inline expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; }
1480 
1481  inline expr nand(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); return expr(a.ctx(), r); }
1482  inline expr nor(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); return expr(a.ctx(), r); }
1483  inline expr xnor(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); return expr(a.ctx(), r); }
1484  inline expr min(expr const& a, expr const& b) {
1485  check_context(a, b);
1486  Z3_ast r;
1487  if (a.is_arith()) {
1488  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
1489  }
1490  else if (a.is_bv()) {
1491  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
1492  }
1493  else {
1494  assert(a.is_fpa());
1495  r = Z3_mk_fpa_min(a.ctx(), a, b);
1496  }
1497  return expr(a.ctx(), r);
1498  }
1499  inline expr max(expr const& a, expr const& b) {
1500  check_context(a, b);
1501  Z3_ast r;
1502  if (a.is_arith()) {
1503  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
1504  }
1505  else if (a.is_bv()) {
1506  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
1507  }
1508  else {
1509  assert(a.is_fpa());
1510  r = Z3_mk_fpa_max(a.ctx(), a, b);
1511  }
1512  return expr(a.ctx(), r);
1513  }
1514  inline expr abs(expr const & a) {
1515  Z3_ast r;
1516  if (a.is_int()) {
1517  expr zero = a.ctx().int_val(0);
1518  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1519  }
1520  else if (a.is_real()) {
1521  expr zero = a.ctx().real_val(0);
1522  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1523  }
1524  else {
1525  r = Z3_mk_fpa_abs(a.ctx(), a);
1526  }
1527  return expr(a.ctx(), r);
1528  }
1529  inline expr sqrt(expr const & a, expr const& rm) {
1530  check_context(a, rm);
1531  assert(a.is_fpa());
1532  Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
1533  return expr(a.ctx(), r);
1534  }
1535  inline expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
1536 
1537  inline expr fma(expr const& a, expr const& b, expr const& c, expr const& rm) {
1538  check_context(a, b); check_context(a, c); check_context(a, rm);
1539  assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
1540  Z3_ast r = Z3_mk_fpa_fma(a.ctx(), rm, a, b, c);
1541  a.check_error();
1542  return expr(a.ctx(), r);
1543  }
1544 
1550  inline expr ite(expr const & c, expr const & t, expr const & e) {
1551  check_context(c, t); check_context(c, e);
1552  assert(c.is_bool());
1553  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
1554  c.check_error();
1555  return expr(c.ctx(), r);
1556  }
1557 
1558 
1563  inline expr to_expr(context & c, Z3_ast a) {
1564  c.check_error();
1565  assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
1566  Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
1567  Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
1569  return expr(c, a);
1570  }
1571 
1572  inline sort to_sort(context & c, Z3_sort s) {
1573  c.check_error();
1574  return sort(c, s);
1575  }
1576 
1577  inline func_decl to_func_decl(context & c, Z3_func_decl f) {
1578  c.check_error();
1579  return func_decl(c, f);
1580  }
1581 
1585  inline expr ule(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
1586  inline expr ule(expr const & a, int b) { return ule(a, a.ctx().num_val(b, a.get_sort())); }
1587  inline expr ule(int a, expr const & b) { return ule(b.ctx().num_val(a, b.get_sort()), b); }
1591  inline expr ult(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }
1592  inline expr ult(expr const & a, int b) { return ult(a, a.ctx().num_val(b, a.get_sort())); }
1593  inline expr ult(int a, expr const & b) { return ult(b.ctx().num_val(a, b.get_sort()), b); }
1597  inline expr uge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }
1598  inline expr uge(expr const & a, int b) { return uge(a, a.ctx().num_val(b, a.get_sort())); }
1599  inline expr uge(int a, expr const & b) { return uge(b.ctx().num_val(a, b.get_sort()), b); }
1603  inline expr ugt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
1604  inline expr ugt(expr const & a, int b) { return ugt(a, a.ctx().num_val(b, a.get_sort())); }
1605  inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), b); }
1609  inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
1610  inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); }
1611  inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); }
1612 
1616  inline expr srem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsrem(a.ctx(), a, b)); }
1617  inline expr srem(expr const & a, int b) { return srem(a, a.ctx().num_val(b, a.get_sort())); }
1618  inline expr srem(int a, expr const & b) { return srem(b.ctx().num_val(a, b.get_sort()), b); }
1619 
1623  inline expr smod(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsmod(a.ctx(), a, b)); }
1624  inline expr smod(expr const & a, int b) { return smod(a, a.ctx().num_val(b, a.get_sort())); }
1625  inline expr smod(int a, expr const & b) { return smod(b.ctx().num_val(a, b.get_sort()), b); }
1626 
1630  inline expr urem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvurem(a.ctx(), a, b)); }
1631  inline expr urem(expr const & a, int b) { return urem(a, a.ctx().num_val(b, a.get_sort())); }
1632  inline expr urem(int a, expr const & b) { return urem(b.ctx().num_val(a, b.get_sort()), b); }
1633 
1637  inline expr shl(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvshl(a.ctx(), a, b)); }
1638  inline expr shl(expr const & a, int b) { return shl(a, a.ctx().num_val(b, a.get_sort())); }
1639  inline expr shl(int a, expr const & b) { return shl(b.ctx().num_val(a, b.get_sort()), b); }
1640 
1644  inline expr lshr(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvlshr(a.ctx(), a, b)); }
1645  inline expr lshr(expr const & a, int b) { return lshr(a, a.ctx().num_val(b, a.get_sort())); }
1646  inline expr lshr(int a, expr const & b) { return lshr(b.ctx().num_val(a, b.get_sort()), b); }
1647 
1651  inline expr ashr(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvashr(a.ctx(), a, b)); }
1652  inline expr ashr(expr const & a, int b) { return ashr(a, a.ctx().num_val(b, a.get_sort())); }
1653  inline expr ashr(int a, expr const & b) { return ashr(b.ctx().num_val(a, b.get_sort()), b); }
1654 
1658  inline expr zext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_zero_ext(a.ctx(), i, a)); }
1659 
1663  inline expr sext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_sign_ext(a.ctx(), i, a)); }
1664 
1665  template<typename T> class cast_ast;
1666 
1667  template<> class cast_ast<ast> {
1668  public:
1669  ast operator()(context & c, Z3_ast a) { return ast(c, a); }
1670  };
1671 
1672  template<> class cast_ast<expr> {
1673  public:
1674  expr operator()(context & c, Z3_ast a) {
1675  assert(Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
1676  Z3_get_ast_kind(c, a) == Z3_APP_AST ||
1678  Z3_get_ast_kind(c, a) == Z3_VAR_AST);
1679  return expr(c, a);
1680  }
1681  };
1682 
1683  template<> class cast_ast<sort> {
1684  public:
1685  sort operator()(context & c, Z3_ast a) {
1686  assert(Z3_get_ast_kind(c, a) == Z3_SORT_AST);
1687  return sort(c, reinterpret_cast<Z3_sort>(a));
1688  }
1689  };
1690 
1691  template<> class cast_ast<func_decl> {
1692  public:
1693  func_decl operator()(context & c, Z3_ast a) {
1694  assert(Z3_get_ast_kind(c, a) == Z3_FUNC_DECL_AST);
1695  return func_decl(c, reinterpret_cast<Z3_func_decl>(a));
1696  }
1697  };
1698 
1699  template<typename T>
1700  class ast_vector_tpl : public object {
1701  Z3_ast_vector m_vector;
1702  void init(Z3_ast_vector v) { Z3_ast_vector_inc_ref(ctx(), v); m_vector = v; }
1703  public:
1705  ast_vector_tpl(context & c, Z3_ast_vector v):object(c) { init(v); }
1706  ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
1708  operator Z3_ast_vector() const { return m_vector; }
1709  unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); }
1710  T operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
1711  void push_back(T const & e) { Z3_ast_vector_push(ctx(), m_vector, e); check_error(); }
1712  void resize(unsigned sz) { Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }
1713  T back() const { return operator[](size() - 1); }
1714  void pop_back() { assert(size() > 0); resize(size() - 1); }
1715  bool empty() const { return size() == 0; }
1717  Z3_ast_vector_inc_ref(s.ctx(), s.m_vector);
1718  Z3_ast_vector_dec_ref(ctx(), m_vector);
1719  m_ctx = s.m_ctx;
1720  m_vector = s.m_vector;
1721  return *this;
1722  }
1723  /*
1724  Disabled pending C++98 build upgrade
1725  bool contains(T const& x) const {
1726  for (T y : *this) if (eq(x, y)) return true;
1727  return false;
1728  }
1729  */
1730 
1731  class iterator {
1732  ast_vector_tpl const* m_vector;
1733  unsigned m_index;
1734  public:
1735  iterator(ast_vector_tpl const* v, unsigned i): m_vector(v), m_index(i) {}
1736  iterator(iterator& other): m_vector(other.m_vector), m_index(other.m_index) {}
1737  iterator operator=(iterator const& other) { m_vector = other.m_vector; m_index = other.m_index; return *this; }
1738 
1739  bool operator==(iterator const& other) {
1740  return other.m_index == m_index;
1741  };
1742  bool operator!=(iterator const& other) {
1743  return other.m_index != m_index;
1744  };
1746  ++m_index;
1747  return *this;
1748  }
1749  iterator operator++(int) { iterator tmp = *this; ++m_index; return tmp; }
1750  T * operator->() const { return &(operator*()); }
1751  T operator*() const { return (*m_vector)[m_index]; }
1752  };
1753  iterator begin() const { return iterator(this, 0); }
1754  iterator end() const { return iterator(this, size()); }
1755  friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
1756  };
1757 
1758 
1759  template<typename T>
1760  template<typename T2>
1762  m_array = new T[v.size()];
1763  m_size = v.size();
1764  for (unsigned i = 0; i < m_size; i++) {
1765  m_array[i] = v[i];
1766  }
1767  }
1768 
1769  // Basic functions for creating quantified formulas.
1770  // The C API should be used for creating quantifiers with patterns, weights, many variables, etc.
1771  inline expr forall(expr const & x, expr const & b) {
1772  check_context(x, b);
1773  Z3_app vars[] = {(Z3_app) x};
1774  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1775  }
1776  inline expr forall(expr const & x1, expr const & x2, expr const & b) {
1777  check_context(x1, b); check_context(x2, b);
1778  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1779  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1780  }
1781  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
1782  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1783  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1784  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1785  }
1786  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
1787  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1788  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1789  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1790  }
1791  inline expr forall(expr_vector const & xs, expr const & b) {
1792  array<Z3_app> vars(xs);
1793  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);
1794  }
1795  inline expr exists(expr const & x, expr const & b) {
1796  check_context(x, b);
1797  Z3_app vars[] = {(Z3_app) x};
1798  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1799  }
1800  inline expr exists(expr const & x1, expr const & x2, expr const & b) {
1801  check_context(x1, b); check_context(x2, b);
1802  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1803  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1804  }
1805  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
1806  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1807  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1808  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1809  }
1810  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
1811  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1812  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1813  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1814  }
1815  inline expr exists(expr_vector const & xs, expr const & b) {
1816  array<Z3_app> vars(xs);
1817  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);
1818  }
1819  inline expr lambda(expr const & x, expr const & b) {
1820  check_context(x, b);
1821  Z3_app vars[] = {(Z3_app) x};
1822  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 1, vars, b); b.check_error(); return expr(b.ctx(), r);
1823  }
1824  inline expr lambda(expr const & x1, expr const & x2, expr const & b) {
1825  check_context(x1, b); check_context(x2, b);
1826  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1827  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 2, vars, b); b.check_error(); return expr(b.ctx(), r);
1828  }
1829  inline expr lambda(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
1830  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1831  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1832  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 3, vars, b); b.check_error(); return expr(b.ctx(), r);
1833  }
1834  inline expr lambda(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
1835  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1836  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1837  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 4, vars, b); b.check_error(); return expr(b.ctx(), r);
1838  }
1839  inline expr lambda(expr_vector const & xs, expr const & b) {
1840  array<Z3_app> vars(xs);
1841  Z3_ast r = Z3_mk_lambda_const(b.ctx(), vars.size(), vars.ptr(), b); b.check_error(); return expr(b.ctx(), r);
1842  }
1843 
1844  inline expr pble(expr_vector const& es, int const* coeffs, int bound) {
1845  assert(es.size() > 0);
1846  context& ctx = es[0].ctx();
1847  array<Z3_ast> _es(es);
1848  Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
1849  ctx.check_error();
1850  return expr(ctx, r);
1851  }
1852  inline expr pbge(expr_vector const& es, int const* coeffs, int bound) {
1853  assert(es.size() > 0);
1854  context& ctx = es[0].ctx();
1855  array<Z3_ast> _es(es);
1856  Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
1857  ctx.check_error();
1858  return expr(ctx, r);
1859  }
1860  inline expr pbeq(expr_vector const& es, int const* coeffs, int bound) {
1861  assert(es.size() > 0);
1862  context& ctx = es[0].ctx();
1863  array<Z3_ast> _es(es);
1864  Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
1865  ctx.check_error();
1866  return expr(ctx, r);
1867  }
1868  inline expr atmost(expr_vector const& es, unsigned bound) {
1869  assert(es.size() > 0);
1870  context& ctx = es[0].ctx();
1871  array<Z3_ast> _es(es);
1872  Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
1873  ctx.check_error();
1874  return expr(ctx, r);
1875  }
1876  inline expr atleast(expr_vector const& es, unsigned bound) {
1877  assert(es.size() > 0);
1878  context& ctx = es[0].ctx();
1879  array<Z3_ast> _es(es);
1880  Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
1881  ctx.check_error();
1882  return expr(ctx, r);
1883  }
1884  inline expr sum(expr_vector const& args) {
1885  assert(args.size() > 0);
1886  context& ctx = args[0].ctx();
1887  array<Z3_ast> _args(args);
1888  Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
1889  ctx.check_error();
1890  return expr(ctx, r);
1891  }
1892 
1893  inline expr distinct(expr_vector const& args) {
1894  assert(args.size() > 0);
1895  context& ctx = args[0].ctx();
1896  array<Z3_ast> _args(args);
1897  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
1898  ctx.check_error();
1899  return expr(ctx, r);
1900  }
1901 
1902  inline expr concat(expr const& a, expr const& b) {
1903  check_context(a, b);
1904  Z3_ast r;
1905  if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
1906  Z3_ast _args[2] = { a, b };
1907  r = Z3_mk_seq_concat(a.ctx(), 2, _args);
1908  }
1909  else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
1910  Z3_ast _args[2] = { a, b };
1911  r = Z3_mk_re_concat(a.ctx(), 2, _args);
1912  }
1913  else {
1914  r = Z3_mk_concat(a.ctx(), a, b);
1915  }
1916  a.ctx().check_error();
1917  return expr(a.ctx(), r);
1918  }
1919 
1920  inline expr concat(expr_vector const& args) {
1921  Z3_ast r;
1922  assert(args.size() > 0);
1923  if (args.size() == 1) {
1924  return args[0];
1925  }
1926  context& ctx = args[0].ctx();
1927  array<Z3_ast> _args(args);
1928  if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
1929  r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
1930  }
1931  else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
1932  r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
1933  }
1934  else {
1935  r = _args[args.size()-1];
1936  for (unsigned i = args.size()-1; i > 0; ) {
1937  --i;
1938  r = Z3_mk_concat(ctx, _args[i], r);
1939  ctx.check_error();
1940  }
1941  }
1942  ctx.check_error();
1943  return expr(ctx, r);
1944  }
1945 
1946  inline expr mk_or(expr_vector const& args) {
1947  array<Z3_ast> _args(args);
1948  Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
1949  args.check_error();
1950  return expr(args.ctx(), r);
1951  }
1952  inline expr mk_and(expr_vector const& args) {
1953  array<Z3_ast> _args(args);
1954  Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
1955  args.check_error();
1956  return expr(args.ctx(), r);
1957  }
1958 
1959 
1960  class func_entry : public object {
1961  Z3_func_entry m_entry;
1962  void init(Z3_func_entry e) {
1963  m_entry = e;
1964  Z3_func_entry_inc_ref(ctx(), m_entry);
1965  }
1966  public:
1967  func_entry(context & c, Z3_func_entry e):object(c) { init(e); }
1968  func_entry(func_entry const & s):object(s) { init(s.m_entry); }
1970  operator Z3_func_entry() const { return m_entry; }
1972  Z3_func_entry_inc_ref(s.ctx(), s.m_entry);
1973  Z3_func_entry_dec_ref(ctx(), m_entry);
1974  m_ctx = s.m_ctx;
1975  m_entry = s.m_entry;
1976  return *this;
1977  }
1978  expr value() const { Z3_ast r = Z3_func_entry_get_value(ctx(), m_entry); check_error(); return expr(ctx(), r); }
1979  unsigned num_args() const { unsigned r = Z3_func_entry_get_num_args(ctx(), m_entry); check_error(); return r; }
1980  expr arg(unsigned i) const { Z3_ast r = Z3_func_entry_get_arg(ctx(), m_entry, i); check_error(); return expr(ctx(), r); }
1981  };
1982 
1983  class func_interp : public object {
1984  Z3_func_interp m_interp;
1985  void init(Z3_func_interp e) {
1986  m_interp = e;
1987  Z3_func_interp_inc_ref(ctx(), m_interp);
1988  }
1989  public:
1990  func_interp(context & c, Z3_func_interp e):object(c) { init(e); }
1991  func_interp(func_interp const & s):object(s) { init(s.m_interp); }
1993  operator Z3_func_interp() const { return m_interp; }
1995  Z3_func_interp_inc_ref(s.ctx(), s.m_interp);
1996  Z3_func_interp_dec_ref(ctx(), m_interp);
1997  m_ctx = s.m_ctx;
1998  m_interp = s.m_interp;
1999  return *this;
2000  }
2001  expr else_value() const { Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), r); }
2002  unsigned num_entries() const { unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }
2003  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); }
2004  void add_entry(expr_vector const& args, expr& value) {
2005  Z3_func_interp_add_entry(ctx(), m_interp, args, value);
2006  check_error();
2007  }
2008  void set_else(expr& value) {
2009  Z3_func_interp_set_else(ctx(), m_interp, value);
2010  check_error();
2011  }
2012  };
2013 
2014  class model : public object {
2015  Z3_model m_model;
2016  void init(Z3_model m) {
2017  m_model = m;
2018  Z3_model_inc_ref(ctx(), m);
2019  }
2020  public:
2021  struct translate {};
2022  model(context & c):object(c) { init(Z3_mk_model(c)); }
2023  model(context & c, Z3_model m):object(c) { init(m); }
2024  model(model const & s):object(s) { init(s.m_model); }
2025  model(model& src, context& dst, translate) : object(dst) { init(Z3_model_translate(src.ctx(), src, dst)); }
2026  ~model() { Z3_model_dec_ref(ctx(), m_model); }
2027  operator Z3_model() const { return m_model; }
2028  model & operator=(model const & s) {
2029  Z3_model_inc_ref(s.ctx(), s.m_model);
2030  Z3_model_dec_ref(ctx(), m_model);
2031  m_ctx = s.m_ctx;
2032  m_model = s.m_model;
2033  return *this;
2034  }
2035 
2036  expr eval(expr const & n, bool model_completion=false) const {
2037  check_context(*this, n);
2038  Z3_ast r = 0;
2039  bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
2040  check_error();
2041  if (status == false && ctx().enable_exceptions())
2042  Z3_THROW(exception("failed to evaluate expression"));
2043  return expr(ctx(), r);
2044  }
2045 
2046  unsigned num_consts() const { return Z3_model_get_num_consts(ctx(), m_model); }
2047  unsigned num_funcs() const { return Z3_model_get_num_funcs(ctx(), m_model); }
2048  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); }
2049  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); }
2050  unsigned size() const { return num_consts() + num_funcs(); }
2051  func_decl operator[](int i) const {
2052  assert(0 <= i);
2053  return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
2054  }
2055 
2056  // returns interpretation of constant declaration c.
2057  // If c is not assigned any value in the model it returns
2058  // an expression with a null ast reference.
2060  check_context(*this, c);
2061  Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);
2062  check_error();
2063  return expr(ctx(), r);
2064  }
2066  check_context(*this, f);
2067  Z3_func_interp r = Z3_model_get_func_interp(ctx(), m_model, f);
2068  check_error();
2069  return func_interp(ctx(), r);
2070  }
2071 
2072  // returns true iff the model contains an interpretation
2073  // for function f.
2074  bool has_interp(func_decl f) const {
2075  check_context(*this, f);
2076  return Z3_model_has_interp(ctx(), m_model, f);
2077  }
2078 
2080  Z3_func_interp r = Z3_add_func_interp(ctx(), m_model, f, else_val);
2081  check_error();
2082  return func_interp(ctx(), r);
2083  }
2084 
2085  void add_const_interp(func_decl& f, expr& value) {
2086  Z3_add_const_interp(ctx(), m_model, f, value);
2087  check_error();
2088  }
2089 
2090  friend std::ostream & operator<<(std::ostream & out, model const & m);
2091  };
2092  inline std::ostream & operator<<(std::ostream & out, model const & m) { out << Z3_model_to_string(m.ctx(), m); return out; }
2093 
2094  class stats : public object {
2095  Z3_stats m_stats;
2096  void init(Z3_stats e) {
2097  m_stats = e;
2098  Z3_stats_inc_ref(ctx(), m_stats);
2099  }
2100  public:
2101  stats(context & c):object(c), m_stats(0) {}
2102  stats(context & c, Z3_stats e):object(c) { init(e); }
2103  stats(stats const & s):object(s) { init(s.m_stats); }
2104  ~stats() { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); }
2105  operator Z3_stats() const { return m_stats; }
2106  stats & operator=(stats const & s) {
2107  Z3_stats_inc_ref(s.ctx(), s.m_stats);
2108  if (m_stats) Z3_stats_dec_ref(ctx(), m_stats);
2109  m_ctx = s.m_ctx;
2110  m_stats = s.m_stats;
2111  return *this;
2112  }
2113  unsigned size() const { return Z3_stats_size(ctx(), m_stats); }
2114  std::string key(unsigned i) const { Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; }
2115  bool is_uint(unsigned i) const { bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r; }
2116  bool is_double(unsigned i) const { bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r; }
2117  unsigned uint_value(unsigned i) const { unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; }
2118  double double_value(unsigned i) const { double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
2119  friend std::ostream & operator<<(std::ostream & out, stats const & s);
2120  };
2121  inline std::ostream & operator<<(std::ostream & out, stats const & s) { out << Z3_stats_to_string(s.ctx(), s); return out; }
2122 
2123 
2124  inline std::ostream & operator<<(std::ostream & out, check_result r) {
2125  if (r == unsat) out << "unsat";
2126  else if (r == sat) out << "sat";
2127  else out << "unknown";
2128  return out;
2129  }
2130 
2131 
2132  class solver : public object {
2133  Z3_solver m_solver;
2134  void init(Z3_solver s) {
2135  m_solver = s;
2136  Z3_solver_inc_ref(ctx(), s);
2137  }
2138  public:
2139  struct simple {};
2140  struct translate {};
2141  solver(context & c):object(c) { init(Z3_mk_solver(c)); }
2143  solver(context & c, Z3_solver s):object(c) { init(s); }
2144  solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); }
2145  solver(context & c, solver const& src, translate): object(c) { init(Z3_solver_translate(src.ctx(), src, c)); }
2146  solver(solver const & s):object(s) { init(s.m_solver); }
2147  ~solver() { Z3_solver_dec_ref(ctx(), m_solver); }
2148  operator Z3_solver() const { return m_solver; }
2149  solver & operator=(solver const & s) {
2150  Z3_solver_inc_ref(s.ctx(), s.m_solver);
2151  Z3_solver_dec_ref(ctx(), m_solver);
2152  m_ctx = s.m_ctx;
2153  m_solver = s.m_solver;
2154  return *this;
2155  }
2156  void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
2157  void set(char const * k, bool v) { params p(ctx()); p.set(k, v); set(p); }
2158  void set(char const * k, unsigned v) { params p(ctx()); p.set(k, v); set(p); }
2159  void set(char const * k, double v) { params p(ctx()); p.set(k, v); set(p); }
2160  void set(char const * k, symbol const & v) { params p(ctx()); p.set(k, v); set(p); }
2161  void set(char const * k, char const* v) { params p(ctx()); p.set(k, v); set(p); }
2162  void push() { Z3_solver_push(ctx(), m_solver); check_error(); }
2163  void pop(unsigned n = 1) { Z3_solver_pop(ctx(), m_solver, n); check_error(); }
2164  void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); }
2165  void add(expr const & e) { assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); }
2166  void add(expr const & e, expr const & p) {
2167  assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
2168  Z3_solver_assert_and_track(ctx(), m_solver, e, p);
2169  check_error();
2170  }
2171  void add(expr const & e, char const * p) {
2172  add(e, ctx().bool_const(p));
2173  }
2174  // fails for some compilers:
2175  // void add(expr_vector const& v) { check_context(*this, v); for (expr e : v) add(e); }
2176  void from_file(char const* file) { Z3_solver_from_file(ctx(), m_solver, file); ctx().check_parser_error(); }
2177  void from_string(char const* s) { Z3_solver_from_string(ctx(), m_solver, s); ctx().check_parser_error(); }
2178 
2180  check_result check(unsigned n, expr * const assumptions) {
2181  array<Z3_ast> _assumptions(n);
2182  for (unsigned i = 0; i < n; i++) {
2183  check_context(*this, assumptions[i]);
2184  _assumptions[i] = assumptions[i];
2185  }
2186  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
2187  check_error();
2188  return to_check_result(r);
2189  }
2191  unsigned n = assumptions.size();
2192  array<Z3_ast> _assumptions(n);
2193  for (unsigned i = 0; i < n; i++) {
2194  check_context(*this, assumptions[i]);
2195  _assumptions[i] = assumptions[i];
2196  }
2197  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
2198  check_error();
2199  return to_check_result(r);
2200  }
2201  model get_model() const { Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }
2203  Z3_lbool r = Z3_solver_get_consequences(ctx(), m_solver, assumptions, vars, conseq);
2204  check_error();
2205  return to_check_result(r);
2206  }
2207  std::string reason_unknown() const { Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }
2208  stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }
2209  expr_vector unsat_core() const { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2210  expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2211  expr_vector non_units() const { Z3_ast_vector r = Z3_solver_get_non_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2212  expr_vector units() const { Z3_ast_vector r = Z3_solver_get_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2213  expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
2214  friend std::ostream & operator<<(std::ostream & out, solver const & s);
2215 
2216  std::string to_smt2(char const* status = "unknown") {
2217  array<Z3_ast> es(assertions());
2218  Z3_ast const* fmls = es.ptr();
2219  Z3_ast fml = 0;
2220  unsigned sz = es.size();
2221  if (sz > 0) {
2222  --sz;
2223  fml = fmls[sz];
2224  }
2225  else {
2226  fml = ctx().bool_val(true);
2227  }
2228  return std::string(Z3_benchmark_to_smtlib_string(
2229  ctx(),
2230  "", "", status, "",
2231  sz,
2232  fmls,
2233  fml));
2234  }
2235 
2237 
2238 
2239  expr_vector cube(expr_vector& vars, unsigned cutoff) {
2240  Z3_ast_vector r = Z3_solver_cube(ctx(), m_solver, vars, cutoff);
2241  check_error();
2242  return expr_vector(ctx(), r);
2243  }
2244 
2246  solver& m_solver;
2247  unsigned& m_cutoff;
2248  expr_vector& m_vars;
2249  expr_vector m_cube;
2250  bool m_end;
2251  bool m_empty;
2252 
2253  void inc() {
2254  assert(!m_end && !m_empty);
2255  m_cube = m_solver.cube(m_vars, m_cutoff);
2256  m_cutoff = 0xFFFFFFFF;
2257  if (m_cube.size() == 1 && m_cube[0].is_false()) {
2258  m_cube = z3::expr_vector(m_solver.ctx());
2259  m_end = true;
2260  }
2261  else if (m_cube.empty()) {
2262  m_empty = true;
2263  }
2264  }
2265  public:
2266  cube_iterator(solver& s, expr_vector& vars, unsigned& cutoff, bool end):
2267  m_solver(s),
2268  m_cutoff(cutoff),
2269  m_vars(vars),
2270  m_cube(s.ctx()),
2271  m_end(end),
2272  m_empty(false) {
2273  if (!m_end) {
2274  inc();
2275  }
2276  }
2277 
2279  assert(!m_end);
2280  if (m_empty) {
2281  m_end = true;
2282  }
2283  else {
2284  inc();
2285  }
2286  return *this;
2287  }
2288  cube_iterator operator++(int) { assert(false); return *this; }
2289  expr_vector const * operator->() const { return &(operator*()); }
2290  expr_vector const& operator*() const { return m_cube; }
2291 
2292  bool operator==(cube_iterator const& other) {
2293  return other.m_end == m_end;
2294  };
2295  bool operator!=(cube_iterator const& other) {
2296  return other.m_end != m_end;
2297  };
2298 
2299  };
2300 
2302  solver& m_solver;
2303  unsigned m_cutoff;
2304  expr_vector m_default_vars;
2305  expr_vector& m_vars;
2306  public:
2308  m_solver(s),
2309  m_cutoff(0xFFFFFFFF),
2310  m_default_vars(s.ctx()),
2311  m_vars(m_default_vars)
2312  {}
2313 
2315  m_solver(s),
2316  m_cutoff(0xFFFFFFFF),
2317  m_default_vars(s.ctx()),
2318  m_vars(vars)
2319  {}
2320 
2321  cube_iterator begin() { return cube_iterator(m_solver, m_vars, m_cutoff, false); }
2322  cube_iterator end() { return cube_iterator(m_solver, m_vars, m_cutoff, true); }
2323  void set_cutoff(unsigned c) { m_cutoff = c; }
2324  };
2325 
2326  cube_generator cubes() { return cube_generator(*this); }
2327  cube_generator cubes(expr_vector& vars) { return cube_generator(*this, vars); }
2328 
2329  };
2330  inline std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
2331 
2332  class goal : public object {
2333  Z3_goal m_goal;
2334  void init(Z3_goal s) {
2335  m_goal = s;
2336  Z3_goal_inc_ref(ctx(), s);
2337  }
2338  public:
2339  goal(context & c, bool models=true, bool unsat_cores=false, bool proofs=false):object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); }
2340  goal(context & c, Z3_goal s):object(c) { init(s); }
2341  goal(goal const & s):object(s) { init(s.m_goal); }
2342  ~goal() { Z3_goal_dec_ref(ctx(), m_goal); }
2343  operator Z3_goal() const { return m_goal; }
2344  goal & operator=(goal const & s) {
2345  Z3_goal_inc_ref(s.ctx(), s.m_goal);
2346  Z3_goal_dec_ref(ctx(), m_goal);
2347  m_ctx = s.m_ctx;
2348  m_goal = s.m_goal;
2349  return *this;
2350  }
2351  void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
2352  // void add(expr_vector const& v) { check_context(*this, v); for (expr e : v) add(e); }
2353  unsigned size() const { return Z3_goal_size(ctx(), m_goal); }
2354  expr operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
2355  Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); }
2356  bool inconsistent() const { return Z3_goal_inconsistent(ctx(), m_goal); }
2357  unsigned depth() const { return Z3_goal_depth(ctx(), m_goal); }
2358  void reset() { Z3_goal_reset(ctx(), m_goal); }
2359  unsigned num_exprs() const { return Z3_goal_num_exprs(ctx(), m_goal); }
2360  bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal); }
2361  bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal); }
2362  model convert_model(model const & m) const {
2363  check_context(*this, m);
2364  Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, m);
2365  check_error();
2366  return model(ctx(), new_m);
2367  }
2368  model get_model() const {
2369  Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, 0);
2370  check_error();
2371  return model(ctx(), new_m);
2372  }
2373  expr as_expr() const {
2374  unsigned n = size();
2375  if (n == 0)
2376  return ctx().bool_val(true);
2377  else if (n == 1)
2378  return operator[](0);
2379  else {
2380  array<Z3_ast> args(n);
2381  for (unsigned i = 0; i < n; i++)
2382  args[i] = operator[](i);
2383  return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
2384  }
2385  }
2386  std::string dimacs() const { return std::string(Z3_goal_to_dimacs_string(ctx(), m_goal)); }
2387  friend std::ostream & operator<<(std::ostream & out, goal const & g);
2388  };
2389  inline std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; }
2390 
2391  class apply_result : public object {
2392  Z3_apply_result m_apply_result;
2393  void init(Z3_apply_result s) {
2394  m_apply_result = s;
2396  }
2397  public:
2398  apply_result(context & c, Z3_apply_result s):object(c) { init(s); }
2399  apply_result(apply_result const & s):object(s) { init(s.m_apply_result); }
2400  ~apply_result() { Z3_apply_result_dec_ref(ctx(), m_apply_result); }
2401  operator Z3_apply_result() const { return m_apply_result; }
2403  Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result);
2404  Z3_apply_result_dec_ref(ctx(), m_apply_result);
2405  m_ctx = s.m_ctx;
2406  m_apply_result = s.m_apply_result;
2407  return *this;
2408  }
2409  unsigned size() const { return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }
2410  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); }
2411  friend std::ostream & operator<<(std::ostream & out, apply_result const & r);
2412  };
2413  inline std::ostream & operator<<(std::ostream & out, apply_result const & r) { out << Z3_apply_result_to_string(r.ctx(), r); return out; }
2414 
2415  class tactic : public object {
2416  Z3_tactic m_tactic;
2417  void init(Z3_tactic s) {
2418  m_tactic = s;
2419  Z3_tactic_inc_ref(ctx(), s);
2420  }
2421  public:
2422  tactic(context & c, char const * name):object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); }
2423  tactic(context & c, Z3_tactic s):object(c) { init(s); }
2424  tactic(tactic const & s):object(s) { init(s.m_tactic); }
2425  ~tactic() { Z3_tactic_dec_ref(ctx(), m_tactic); }
2426  operator Z3_tactic() const { return m_tactic; }
2427  tactic & operator=(tactic const & s) {
2428  Z3_tactic_inc_ref(s.ctx(), s.m_tactic);
2429  Z3_tactic_dec_ref(ctx(), m_tactic);
2430  m_ctx = s.m_ctx;
2431  m_tactic = s.m_tactic;
2432  return *this;
2433  }
2434  solver mk_solver() const { Z3_solver r = Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error(); return solver(ctx(), r); }
2435  apply_result apply(goal const & g) const {
2436  check_context(*this, g);
2437  Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g);
2438  check_error();
2439  return apply_result(ctx(), r);
2440  }
2441  apply_result operator()(goal const & g) const {
2442  return apply(g);
2443  }
2444  std::string help() const { char const * r = Z3_tactic_get_help(ctx(), m_tactic); check_error(); return r; }
2445  friend tactic operator&(tactic const & t1, tactic const & t2);
2446  friend tactic operator|(tactic const & t1, tactic const & t2);
2447  friend tactic repeat(tactic const & t, unsigned max);
2448  friend tactic with(tactic const & t, params const & p);
2449  friend tactic try_for(tactic const & t, unsigned ms);
2450  friend tactic par_or(unsigned n, tactic const* tactics);
2451  friend tactic par_and_then(tactic const& t1, tactic const& t2);
2453  };
2454 
2455  inline tactic operator&(tactic const & t1, tactic const & t2) {
2456  check_context(t1, t2);
2457  Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
2458  t1.check_error();
2459  return tactic(t1.ctx(), r);
2460  }
2461 
2462  inline tactic operator|(tactic const & t1, tactic const & t2) {
2463  check_context(t1, t2);
2464  Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
2465  t1.check_error();
2466  return tactic(t1.ctx(), r);
2467  }
2468 
2469  inline tactic repeat(tactic const & t, unsigned max=UINT_MAX) {
2470  Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
2471  t.check_error();
2472  return tactic(t.ctx(), r);
2473  }
2474 
2475  inline tactic with(tactic const & t, params const & p) {
2476  Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
2477  t.check_error();
2478  return tactic(t.ctx(), r);
2479  }
2480  inline tactic try_for(tactic const & t, unsigned ms) {
2481  Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
2482  t.check_error();
2483  return tactic(t.ctx(), r);
2484  }
2485  inline tactic par_or(unsigned n, tactic const* tactics) {
2486  if (n == 0) {
2487  Z3_THROW(exception("a non-zero number of tactics need to be passed to par_or"));
2488  }
2489  array<Z3_tactic> buffer(n);
2490  for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
2491  return tactic(tactics[0].ctx(), Z3_tactic_par_or(tactics[0].ctx(), n, buffer.ptr()));
2492  }
2493 
2494  inline tactic par_and_then(tactic const & t1, tactic const & t2) {
2495  check_context(t1, t2);
2496  Z3_tactic r = Z3_tactic_par_and_then(t1.ctx(), t1, t2);
2497  t1.check_error();
2498  return tactic(t1.ctx(), r);
2499  }
2500 
2501  class probe : public object {
2502  Z3_probe m_probe;
2503  void init(Z3_probe s) {
2504  m_probe = s;
2505  Z3_probe_inc_ref(ctx(), s);
2506  }
2507  public:
2508  probe(context & c, char const * name):object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); }
2509  probe(context & c, double val):object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); }
2510  probe(context & c, Z3_probe s):object(c) { init(s); }
2511  probe(probe const & s):object(s) { init(s.m_probe); }
2512  ~probe() { Z3_probe_dec_ref(ctx(), m_probe); }
2513  operator Z3_probe() const { return m_probe; }
2514  probe & operator=(probe const & s) {
2515  Z3_probe_inc_ref(s.ctx(), s.m_probe);
2516  Z3_probe_dec_ref(ctx(), m_probe);
2517  m_ctx = s.m_ctx;
2518  m_probe = s.m_probe;
2519  return *this;
2520  }
2521  double apply(goal const & g) const { double r = Z3_probe_apply(ctx(), m_probe, g); check_error(); return r; }
2522  double operator()(goal const & g) const { return apply(g); }
2523  friend probe operator<=(probe const & p1, probe const & p2);
2524  friend probe operator<=(probe const & p1, double p2);
2525  friend probe operator<=(double p1, probe const & p2);
2526  friend probe operator>=(probe const & p1, probe const & p2);
2527  friend probe operator>=(probe const & p1, double p2);
2528  friend probe operator>=(double p1, probe const & p2);
2529  friend probe operator<(probe const & p1, probe const & p2);
2530  friend probe operator<(probe const & p1, double p2);
2531  friend probe operator<(double p1, probe const & p2);
2532  friend probe operator>(probe const & p1, probe const & p2);
2533  friend probe operator>(probe const & p1, double p2);
2534  friend probe operator>(double p1, probe const & p2);
2535  friend probe operator==(probe const & p1, probe const & p2);
2536  friend probe operator==(probe const & p1, double p2);
2537  friend probe operator==(double p1, probe const & p2);
2538  friend probe operator&&(probe const & p1, probe const & p2);
2539  friend probe operator||(probe const & p1, probe const & p2);
2540  friend probe operator!(probe const & p);
2541  };
2542 
2543  inline probe operator<=(probe const & p1, probe const & p2) {
2544  check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2545  }
2546  inline probe operator<=(probe const & p1, double p2) { return p1 <= probe(p1.ctx(), p2); }
2547  inline probe operator<=(double p1, probe const & p2) { return probe(p2.ctx(), p1) <= p2; }
2548  inline probe operator>=(probe const & p1, probe const & p2) {
2549  check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2550  }
2551  inline probe operator>=(probe const & p1, double p2) { return p1 >= probe(p1.ctx(), p2); }
2552  inline probe operator>=(double p1, probe const & p2) { return probe(p2.ctx(), p1) >= p2; }
2553  inline probe operator<(probe const & p1, probe const & p2) {
2554  check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2555  }
2556  inline probe operator<(probe const & p1, double p2) { return p1 < probe(p1.ctx(), p2); }
2557  inline probe operator<(double p1, probe const & p2) { return probe(p2.ctx(), p1) < p2; }
2558  inline probe operator>(probe const & p1, probe const & p2) {
2559  check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2560  }
2561  inline probe operator>(probe const & p1, double p2) { return p1 > probe(p1.ctx(), p2); }
2562  inline probe operator>(double p1, probe const & p2) { return probe(p2.ctx(), p1) > p2; }
2563  inline probe operator==(probe const & p1, probe const & p2) {
2564  check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2565  }
2566  inline probe operator==(probe const & p1, double p2) { return p1 == probe(p1.ctx(), p2); }
2567  inline probe operator==(double p1, probe const & p2) { return probe(p2.ctx(), p1) == p2; }
2568  inline probe operator&&(probe const & p1, probe const & p2) {
2569  check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2570  }
2571  inline probe operator||(probe const & p1, probe const & p2) {
2572  check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2573  }
2574  inline probe operator!(probe const & p) {
2575  Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
2576  }
2577 
2578  class optimize : public object {
2579  Z3_optimize m_opt;
2580 
2581  public:
2582  class handle {
2583  unsigned m_h;
2584  public:
2585  handle(unsigned h): m_h(h) {}
2586  unsigned h() const { return m_h; }
2587  };
2588  optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }
2590  Z3_optimize_inc_ref(o.ctx(), o.m_opt);
2591  m_opt = o.m_opt;
2592  }
2594  Z3_optimize_inc_ref(o.ctx(), o.m_opt);
2595  Z3_optimize_dec_ref(ctx(), m_opt);
2596  m_opt = o.m_opt;
2597  m_ctx = o.m_ctx;
2598  return *this;
2599  }
2601  operator Z3_optimize() const { return m_opt; }
2602  void add(expr const& e) {
2603  assert(e.is_bool());
2604  Z3_optimize_assert(ctx(), m_opt, e);
2605  }
2606  handle add(expr const& e, unsigned weight) {
2607  assert(e.is_bool());
2608  std::stringstream strm;
2609  strm << weight;
2610  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, strm.str().c_str(), 0));
2611  }
2612  handle add(expr const& e, char const* weight) {
2613  assert(e.is_bool());
2614  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0));
2615  }
2616  handle maximize(expr const& e) {
2617  return handle(Z3_optimize_maximize(ctx(), m_opt, e));
2618  }
2619  handle minimize(expr const& e) {
2620  return handle(Z3_optimize_minimize(ctx(), m_opt, e));
2621  }
2622  void push() {
2623  Z3_optimize_push(ctx(), m_opt);
2624  }
2625  void pop() {
2626  Z3_optimize_pop(ctx(), m_opt);
2627  }
2630  unsigned n = asms.size();
2631  array<Z3_ast> _asms(n);
2632  for (unsigned i = 0; i < n; i++) {
2633  check_context(*this, asms[i]);
2634  _asms[i] = asms[i];
2635  }
2636  Z3_lbool r = Z3_optimize_check(ctx(), m_opt, n, _asms.ptr());
2637  check_error();
2638  return to_check_result(r);
2639  }
2640  model get_model() const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }
2641  expr_vector unsat_core() const { Z3_ast_vector r = Z3_optimize_get_unsat_core(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
2642  void set(params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }
2643  expr lower(handle const& h) {
2644  Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());
2645  check_error();
2646  return expr(ctx(), r);
2647  }
2648  expr upper(handle const& h) {
2649  Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h());
2650  check_error();
2651  return expr(ctx(), r);
2652  }
2653  expr_vector assertions() const { Z3_ast_vector r = Z3_optimize_get_assertions(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
2654  expr_vector objectives() const { Z3_ast_vector r = Z3_optimize_get_objectives(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
2655  stats statistics() const { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); }
2656  friend std::ostream & operator<<(std::ostream & out, optimize const & s);
2657  void from_file(char const* filename) { Z3_optimize_from_file(ctx(), m_opt, filename); check_error(); }
2658  void from_string(char const* constraints) { Z3_optimize_from_string(ctx(), m_opt, constraints); check_error(); }
2659  std::string help() const { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error(); return r; }
2660  };
2661  inline std::ostream & operator<<(std::ostream & out, optimize const & s) { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }
2662 
2663  class fixedpoint : public object {
2664  Z3_fixedpoint m_fp;
2665  public:
2668  operator Z3_fixedpoint() const { return m_fp; }
2669  void from_string(char const* s) { Z3_fixedpoint_from_string(ctx(), m_fp, s); check_error(); }
2670  void from_file(char const* s) { Z3_fixedpoint_from_file(ctx(), m_fp, s); check_error(); }
2671  void add_rule(expr& rule, symbol const& name) { Z3_fixedpoint_add_rule(ctx(), m_fp, rule, name); check_error(); }
2672  void add_fact(func_decl& f, unsigned * args) { Z3_fixedpoint_add_fact(ctx(), m_fp, f, f.arity(), args); check_error(); }
2675  array<Z3_func_decl> rs(relations);
2676  Z3_lbool r = Z3_fixedpoint_query_relations(ctx(), m_fp, rs.size(), rs.ptr());
2677  check_error();
2678  return to_check_result(r);
2679  }
2680  expr get_answer() { Z3_ast r = Z3_fixedpoint_get_answer(ctx(), m_fp); check_error(); return expr(ctx(), r); }
2681  std::string reason_unknown() { return Z3_fixedpoint_get_reason_unknown(ctx(), m_fp); }
2682  void update_rule(expr& rule, symbol const& name) { Z3_fixedpoint_update_rule(ctx(), m_fp, rule, name); check_error(); }
2683  unsigned get_num_levels(func_decl& p) { unsigned r = Z3_fixedpoint_get_num_levels(ctx(), m_fp, p); check_error(); return r; }
2684  expr get_cover_delta(int level, func_decl& p) {
2685  Z3_ast r = Z3_fixedpoint_get_cover_delta(ctx(), m_fp, level, p);
2686  check_error();
2687  return expr(ctx(), r);
2688  }
2689  void add_cover(int level, func_decl& p, expr& property) { Z3_fixedpoint_add_cover(ctx(), m_fp, level, p, property); check_error(); }
2690  stats statistics() const { Z3_stats r = Z3_fixedpoint_get_statistics(ctx(), m_fp); check_error(); return stats(ctx(), r); }
2692  expr_vector assertions() const { Z3_ast_vector r = Z3_fixedpoint_get_assertions(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
2693  expr_vector rules() const { Z3_ast_vector r = Z3_fixedpoint_get_rules(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
2694  void set(params const & p) { Z3_fixedpoint_set_params(ctx(), m_fp, p); check_error(); }
2695  std::string help() const { return Z3_fixedpoint_get_help(ctx(), m_fp); }
2697  std::string to_string() { return Z3_fixedpoint_to_string(ctx(), m_fp, 0, 0); }
2698  std::string to_string(expr_vector const& queries) {
2699  array<Z3_ast> qs(queries);
2700  return Z3_fixedpoint_to_string(ctx(), m_fp, qs.size(), qs.ptr());
2701  }
2702  void push() { Z3_fixedpoint_push(ctx(), m_fp); check_error(); }
2703  void pop() { Z3_fixedpoint_pop(ctx(), m_fp); check_error(); }
2704  };
2705  inline std::ostream & operator<<(std::ostream & out, fixedpoint const & f) { return out << Z3_fixedpoint_to_string(f.ctx(), f, 0, 0); }
2706 
2707  inline tactic fail_if(probe const & p) {
2708  Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
2709  p.check_error();
2710  return tactic(p.ctx(), r);
2711  }
2712  inline tactic when(probe const & p, tactic const & t) {
2713  check_context(p, t);
2714  Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
2715  t.check_error();
2716  return tactic(t.ctx(), r);
2717  }
2718  inline tactic cond(probe const & p, tactic const & t1, tactic const & t2) {
2719  check_context(p, t1); check_context(p, t2);
2720  Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
2721  t1.check_error();
2722  return tactic(t1.ctx(), r);
2723  }
2724 
2725  inline symbol context::str_symbol(char const * s) { Z3_symbol r = Z3_mk_string_symbol(m_ctx, s); check_error(); return symbol(*this, r); }
2726  inline symbol context::int_symbol(int n) { Z3_symbol r = Z3_mk_int_symbol(m_ctx, n); check_error(); return symbol(*this, r); }
2727 
2728  inline sort context::bool_sort() { Z3_sort s = Z3_mk_bool_sort(m_ctx); check_error(); return sort(*this, s); }
2729  inline sort context::int_sort() { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }
2730  inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
2731  inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
2732  inline sort context::string_sort() { Z3_sort s = Z3_mk_string_sort(m_ctx); check_error(); return sort(*this, s); }
2733  inline sort context::seq_sort(sort& s) { Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); }
2734  inline sort context::re_sort(sort& s) { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
2735  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); }
2736 
2737  template<>
2738  inline sort context::fpa_sort<16>() { return fpa_sort(5, 11); }
2739 
2740  template<>
2741  inline sort context::fpa_sort<32>() { return fpa_sort(8, 24); }
2742 
2743  template<>
2744  inline sort context::fpa_sort<64>() { return fpa_sort(11, 53); }
2745 
2746  template<>
2747  inline sort context::fpa_sort<128>() { return fpa_sort(15, 113); }
2748 
2750  switch (m_rounding_mode) {
2751  case RNA: return sort(*this, Z3_mk_fpa_rna(m_ctx));
2752  case RNE: return sort(*this, Z3_mk_fpa_rne(m_ctx));
2753  case RTP: return sort(*this, Z3_mk_fpa_rtp(m_ctx));
2754  case RTN: return sort(*this, Z3_mk_fpa_rtn(m_ctx));
2755  case RTZ: return sort(*this, Z3_mk_fpa_rtz(m_ctx));
2756  default: return sort(*this);
2757  }
2758  }
2759 
2760  inline void context::set_rounding_mode(rounding_mode rm) { m_rounding_mode = rm; }
2761 
2762  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); }
2764  array<Z3_sort> dom(d);
2765  Z3_sort s = Z3_mk_array_sort_n(m_ctx, dom.size(), dom.ptr(), r); check_error(); return sort(*this, s);
2766  }
2767  inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
2768  array<Z3_symbol> _enum_names(n);
2769  for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
2770  array<Z3_func_decl> _cs(n);
2771  array<Z3_func_decl> _ts(n);
2772  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2773  sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
2774  check_error();
2775  for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
2776  return s;
2777  }
2778  inline func_decl context::tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs) {
2779  array<Z3_symbol> _names(n);
2780  array<Z3_sort> _sorts(n);
2781  for (unsigned i = 0; i < n; i++) { _names[i] = Z3_mk_string_symbol(*this, names[i]); _sorts[i] = sorts[i]; }
2782  array<Z3_func_decl> _projs(n);
2783  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2784  Z3_func_decl tuple;
2785  sort _ignore_s = to_sort(*this, Z3_mk_tuple_sort(*this, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));
2786  check_error();
2787  for (unsigned i = 0; i < n; i++) { projs.push_back(func_decl(*this, _projs[i])); }
2788  return func_decl(*this, tuple);
2789  }
2790 
2791  inline sort context::uninterpreted_sort(char const* name) {
2792  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2793  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
2794  }
2796  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
2797  }
2798 
2799  inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
2800  array<Z3_sort> args(arity);
2801  for (unsigned i = 0; i < arity; i++) {
2802  check_context(domain[i], range);
2803  args[i] = domain[i];
2804  }
2805  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
2806  check_error();
2807  return func_decl(*this, f);
2808  }
2809 
2810  inline func_decl context::function(char const * name, unsigned arity, sort const * domain, sort const & range) {
2811  return function(range.ctx().str_symbol(name), arity, domain, range);
2812  }
2813 
2814  inline func_decl context::function(symbol const& name, sort_vector const& domain, sort const& range) {
2815  array<Z3_sort> args(domain.size());
2816  for (unsigned i = 0; i < domain.size(); i++) {
2817  check_context(domain[i], range);
2818  args[i] = domain[i];
2819  }
2820  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
2821  check_error();
2822  return func_decl(*this, f);
2823  }
2824 
2825  inline func_decl context::function(char const * name, sort_vector const& domain, sort const& range) {
2826  return function(range.ctx().str_symbol(name), domain, range);
2827  }
2828 
2829 
2830  inline func_decl context::function(char const * name, sort const & domain, sort const & range) {
2831  check_context(domain, range);
2832  Z3_sort args[1] = { domain };
2833  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
2834  check_error();
2835  return func_decl(*this, f);
2836  }
2837 
2838  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & range) {
2840  Z3_sort args[2] = { d1, d2 };
2841  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
2842  check_error();
2843  return func_decl(*this, f);
2844  }
2845 
2846  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
2848  Z3_sort args[3] = { d1, d2, d3 };
2849  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
2850  check_error();
2851  return func_decl(*this, f);
2852  }
2853 
2854  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
2856  Z3_sort args[4] = { d1, d2, d3, d4 };
2857  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
2858  check_error();
2859  return func_decl(*this, f);
2860  }
2861 
2862  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) {
2864  Z3_sort args[5] = { d1, d2, d3, d4, d5 };
2865  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
2866  check_error();
2867  return func_decl(*this, f);
2868  }
2869 
2870  inline func_decl context::recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
2871  array<Z3_sort> args(arity);
2872  for (unsigned i = 0; i < arity; i++) {
2873  check_context(domain[i], range);
2874  args[i] = domain[i];
2875  }
2876  Z3_func_decl f = Z3_mk_rec_func_decl(m_ctx, name, arity, args.ptr(), range);
2877  check_error();
2878  return func_decl(*this, f);
2879 
2880  }
2881 
2882  inline func_decl context::recfun(char const * name, unsigned arity, sort const * domain, sort const & range) {
2883  return recfun(str_symbol(name), arity, domain, range);
2884  }
2885 
2886  inline func_decl context::recfun(char const * name, sort const& d1, sort const & range) {
2887  return recfun(str_symbol(name), 1, &d1, range);
2888  }
2889 
2890  inline func_decl context::recfun(char const * name, sort const& d1, sort const& d2, sort const & range) {
2891  sort dom[2] = { d1, d2 };
2892  return recfun(str_symbol(name), 2, dom, range);
2893  }
2894 
2895  inline void context::recdef(func_decl f, expr_vector const& args, expr const& body) {
2896  check_context(f, args); check_context(f, body);
2897  array<Z3_ast> vars(args);
2898  Z3_add_rec_def(f.ctx(), f, vars.size(), vars.ptr(), body);
2899  }
2900 
2901  inline expr context::constant(symbol const & name, sort const & s) {
2902  Z3_ast r = Z3_mk_const(m_ctx, name, s);
2903  check_error();
2904  return expr(*this, r);
2905  }
2906  inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); }
2907  inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); }
2908  inline expr context::int_const(char const * name) { return constant(name, int_sort()); }
2909  inline expr context::real_const(char const * name) { return constant(name, real_sort()); }
2910  inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); }
2911  inline expr context::fpa_const(char const * name, unsigned ebits, unsigned sbits) { return constant(name, fpa_sort(ebits, sbits)); }
2912 
2913  template<size_t precision>
2914  inline expr context::fpa_const(char const * name) { return constant(name, fpa_sort<precision>()); }
2915 
2916  inline expr context::bool_val(bool b) { return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }
2917 
2918  inline expr context::int_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
2919  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); }
2920  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); }
2921  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); }
2922  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); }
2923 
2924  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); }
2925  inline expr context::real_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
2926  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); }
2927  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); }
2928  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); }
2929  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); }
2930 
2931  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); }
2932  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); }
2933  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); }
2934  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); }
2935  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); }
2936  inline expr context::bv_val(unsigned n, bool const* bits) {
2937  array<bool> _bits(n);
2938  for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
2939  Z3_ast r = Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error(); return expr(*this, r);
2940  }
2941 
2942  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); }
2943  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); }
2944 
2945  inline expr context::string_val(char const* s) { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
2946  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); }
2947 
2948  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); }
2949 
2950  inline expr func_decl::operator()(unsigned n, expr const * args) const {
2951  array<Z3_ast> _args(n);
2952  for (unsigned i = 0; i < n; i++) {
2953  check_context(*this, args[i]);
2954  _args[i] = args[i];
2955  }
2956  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
2957  check_error();
2958  return expr(ctx(), r);
2959 
2960  }
2961  inline expr func_decl::operator()(expr_vector const& args) const {
2962  array<Z3_ast> _args(args.size());
2963  for (unsigned i = 0; i < args.size(); i++) {
2964  check_context(*this, args[i]);
2965  _args[i] = args[i];
2966  }
2967  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
2968  check_error();
2969  return expr(ctx(), r);
2970  }
2971  inline expr func_decl::operator()() const {
2972  Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
2973  ctx().check_error();
2974  return expr(ctx(), r);
2975  }
2976  inline expr func_decl::operator()(expr const & a) const {
2977  check_context(*this, a);
2978  Z3_ast args[1] = { a };
2979  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
2980  ctx().check_error();
2981  return expr(ctx(), r);
2982  }
2983  inline expr func_decl::operator()(int a) const {
2984  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
2985  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
2986  ctx().check_error();
2987  return expr(ctx(), r);
2988  }
2989  inline expr func_decl::operator()(expr const & a1, expr const & a2) const {
2990  check_context(*this, a1); check_context(*this, a2);
2991  Z3_ast args[2] = { a1, a2 };
2992  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
2993  ctx().check_error();
2994  return expr(ctx(), r);
2995  }
2996  inline expr func_decl::operator()(expr const & a1, int a2) const {
2997  check_context(*this, a1);
2998  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
2999  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3000  ctx().check_error();
3001  return expr(ctx(), r);
3002  }
3003  inline expr func_decl::operator()(int a1, expr const & a2) const {
3004  check_context(*this, a2);
3005  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
3006  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3007  ctx().check_error();
3008  return expr(ctx(), r);
3009  }
3010  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3) const {
3011  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
3012  Z3_ast args[3] = { a1, a2, a3 };
3013  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
3014  ctx().check_error();
3015  return expr(ctx(), r);
3016  }
3017  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const {
3018  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
3019  Z3_ast args[4] = { a1, a2, a3, a4 };
3020  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
3021  ctx().check_error();
3022  return expr(ctx(), r);
3023  }
3024  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const {
3025  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
3026  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
3027  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
3028  ctx().check_error();
3029  return expr(ctx(), r);
3030  }
3031 
3032  inline expr to_real(expr const & a) { Z3_ast r = Z3_mk_int2real(a.ctx(), a); a.check_error(); return expr(a.ctx(), r); }
3033 
3034  inline func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3035  return range.ctx().function(name, arity, domain, range);
3036  }
3037  inline func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range) {
3038  return range.ctx().function(name, arity, domain, range);
3039  }
3040  inline func_decl function(char const * name, sort const & domain, sort const & range) {
3041  return range.ctx().function(name, domain, range);
3042  }
3043  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range) {
3044  return range.ctx().function(name, d1, d2, range);
3045  }
3046  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
3047  return range.ctx().function(name, d1, d2, d3, range);
3048  }
3049  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
3050  return range.ctx().function(name, d1, d2, d3, d4, range);
3051  }
3052  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) {
3053  return range.ctx().function(name, d1, d2, d3, d4, d5, range);
3054  }
3055  inline func_decl function(char const* name, sort_vector const& domain, sort const& range) {
3056  return range.ctx().function(name, domain, range);
3057  }
3058  inline func_decl function(std::string const& name, sort_vector const& domain, sort const& range) {
3059  return range.ctx().function(name.c_str(), domain, range);
3060  }
3061 
3062  inline func_decl recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3063  return range.ctx().recfun(name, arity, domain, range);
3064  }
3065  inline func_decl recfun(char const * name, unsigned arity, sort const * domain, sort const & range) {
3066  return range.ctx().recfun(name, arity, domain, range);
3067  }
3068  inline func_decl recfun(char const * name, sort const& d1, sort const & range) {
3069  return range.ctx().recfun(name, d1, range);
3070  }
3071  inline func_decl recfun(char const * name, sort const& d1, sort const& d2, sort const & range) {
3072  return range.ctx().recfun(name, d1, d2, range);
3073  }
3074 
3075  inline expr select(expr const & a, expr const & i) {
3076  check_context(a, i);
3077  Z3_ast r = Z3_mk_select(a.ctx(), a, i);
3078  a.check_error();
3079  return expr(a.ctx(), r);
3080  }
3081  inline expr select(expr const & a, int i) {
3082  return select(a, a.ctx().num_val(i, a.get_sort().array_domain()));
3083  }
3084  inline expr select(expr const & a, expr_vector const & i) {
3085  check_context(a, i);
3086  array<Z3_ast> idxs(i);
3087  Z3_ast r = Z3_mk_select_n(a.ctx(), a, idxs.size(), idxs.ptr());
3088  a.check_error();
3089  return expr(a.ctx(), r);
3090  }
3091 
3092  inline expr store(expr const & a, expr const & i, expr const & v) {
3093  check_context(a, i); check_context(a, v);
3094  Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
3095  a.check_error();
3096  return expr(a.ctx(), r);
3097  }
3098 
3099  inline expr store(expr const & a, int i, expr const & v) { return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), v); }
3100  inline expr store(expr const & a, expr i, int v) { return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
3101  inline expr store(expr const & a, int i, int v) {
3102  return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
3103  }
3104  inline expr store(expr const & a, expr_vector const & i, expr const & v) {
3105  check_context(a, i); check_context(a, v);
3106  array<Z3_ast> idxs(i);
3107  Z3_ast r = Z3_mk_store_n(a.ctx(), a, idxs.size(), idxs.ptr(), v);
3108  a.check_error();
3109  return expr(a.ctx(), r);
3110  }
3111 
3112  inline expr as_array(func_decl & f) {
3113  Z3_ast r = Z3_mk_as_array(f.ctx(), f);
3114  f.check_error();
3115  return expr(f.ctx(), r);
3116  }
3117 
3118 #define MK_EXPR1(_fn, _arg) \
3119  Z3_ast r = _fn(_arg.ctx(), _arg); \
3120  _arg.check_error(); \
3121  return expr(_arg.ctx(), r);
3122 
3123 #define MK_EXPR2(_fn, _arg1, _arg2) \
3124  check_context(_arg1, _arg2); \
3125  Z3_ast r = _fn(_arg1.ctx(), _arg1, _arg2); \
3126  _arg1.check_error(); \
3127  return expr(_arg1.ctx(), r);
3128 
3129  inline expr const_array(sort const & d, expr const & v) {
3130  MK_EXPR2(Z3_mk_const_array, d, v);
3131  }
3132 
3133  inline expr empty_set(sort const& s) {
3135  }
3136 
3137  inline expr full_set(sort const& s) {
3139  }
3140 
3141  inline expr set_add(expr const& s, expr const& e) {
3142  MK_EXPR2(Z3_mk_set_add, s, e);
3143  }
3144 
3145  inline expr set_del(expr const& s, expr const& e) {
3146  MK_EXPR2(Z3_mk_set_del, s, e);
3147  }
3148 
3149  inline expr set_union(expr const& a, expr const& b) {
3150  check_context(a, b);
3151  Z3_ast es[2] = { a, b };
3152  Z3_ast r = Z3_mk_set_union(a.ctx(), 2, es);
3153  a.check_error();
3154  return expr(a.ctx(), r);
3155  }
3156 
3157  inline expr set_intersect(expr const& a, expr const& b) {
3158  check_context(a, b);
3159  Z3_ast es[2] = { a, b };
3160  Z3_ast r = Z3_mk_set_intersect(a.ctx(), 2, es);
3161  a.check_error();
3162  return expr(a.ctx(), r);
3163  }
3164 
3165  inline expr set_difference(expr const& a, expr const& b) {
3167  }
3168 
3169  inline expr set_complement(expr const& a) {
3171  }
3172 
3173  inline expr set_member(expr const& s, expr const& e) {
3174  MK_EXPR2(Z3_mk_set_member, s, e);
3175  }
3176 
3177  inline expr set_subset(expr const& a, expr const& b) {
3178  MK_EXPR2(Z3_mk_set_subset, a, b);
3179  }
3180 
3181  // sequence and regular expression operations.
3182  // union is +
3183  // concat is overloaded to handle sequences and regular expressions
3184 
3185  inline expr empty(sort const& s) {
3186  Z3_ast r = Z3_mk_seq_empty(s.ctx(), s);
3187  s.check_error();
3188  return expr(s.ctx(), r);
3189  }
3190  inline expr suffixof(expr const& a, expr const& b) {
3191  check_context(a, b);
3192  Z3_ast r = Z3_mk_seq_suffix(a.ctx(), a, b);
3193  a.check_error();
3194  return expr(a.ctx(), r);
3195  }
3196  inline expr prefixof(expr const& a, expr const& b) {
3197  check_context(a, b);
3198  Z3_ast r = Z3_mk_seq_prefix(a.ctx(), a, b);
3199  a.check_error();
3200  return expr(a.ctx(), r);
3201  }
3202  inline expr indexof(expr const& s, expr const& substr, expr const& offset) {
3203  check_context(s, substr); check_context(s, offset);
3204  Z3_ast r = Z3_mk_seq_index(s.ctx(), s, substr, offset);
3205  s.check_error();
3206  return expr(s.ctx(), r);
3207  }
3208  inline expr to_re(expr const& s) {
3210  }
3211  inline expr in_re(expr const& s, expr const& re) {
3212  MK_EXPR2(Z3_mk_seq_in_re, s, re);
3213  }
3214  inline expr plus(expr const& re) {
3215  MK_EXPR1(Z3_mk_re_plus, re);
3216  }
3217  inline expr option(expr const& re) {
3219  }
3220  inline expr star(expr const& re) {
3221  MK_EXPR1(Z3_mk_re_star, re);
3222  }
3223  inline expr re_empty(sort const& s) {
3224  Z3_ast r = Z3_mk_re_empty(s.ctx(), s);
3225  s.check_error();
3226  return expr(s.ctx(), r);
3227  }
3228  inline expr re_full(sort const& s) {
3229  Z3_ast r = Z3_mk_re_full(s.ctx(), s);
3230  s.check_error();
3231  return expr(s.ctx(), r);
3232  }
3233  inline expr re_intersect(expr_vector const& args) {
3234  assert(args.size() > 0);
3235  context& ctx = args[0].ctx();
3236  array<Z3_ast> _args(args);
3237  Z3_ast r = Z3_mk_re_intersect(ctx, _args.size(), _args.ptr());
3238  ctx.check_error();
3239  return expr(ctx, r);
3240  }
3241  inline expr re_complement(expr const& a) {
3243  }
3244  inline expr range(expr const& lo, expr const& hi) {
3245  check_context(lo, hi);
3246  Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
3247  lo.check_error();
3248  return expr(lo.ctx(), r);
3249  }
3250 
3251 
3252 
3253 
3254 
3255  inline expr_vector context::parse_string(char const* s) {
3256  Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0);
3257  check_error();
3258  return expr_vector(*this, r);
3259 
3260  }
3261  inline expr_vector context::parse_file(char const* s) {
3262  Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0);
3263  check_error();
3264  return expr_vector(*this, r);
3265  }
3266 
3267  inline expr_vector context::parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls) {
3268  array<Z3_symbol> sort_names(sorts.size());
3269  array<Z3_symbol> decl_names(decls.size());
3270  array<Z3_sort> sorts1(sorts);
3271  array<Z3_func_decl> decls1(decls);
3272  for (unsigned i = 0; i < sorts.size(); ++i) {
3273  sort_names[i] = sorts[i].name();
3274  }
3275  for (unsigned i = 0; i < decls.size(); ++i) {
3276  decl_names[i] = decls[i].name();
3277  }
3278 
3279  Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
3280  check_error();
3281  return expr_vector(*this, r);
3282  }
3283 
3284  inline expr_vector context::parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls) {
3285  array<Z3_symbol> sort_names(sorts.size());
3286  array<Z3_symbol> decl_names(decls.size());
3287  array<Z3_sort> sorts1(sorts);
3288  array<Z3_func_decl> decls1(decls);
3289  for (unsigned i = 0; i < sorts.size(); ++i) {
3290  sort_names[i] = sorts[i].name();
3291  }
3292  for (unsigned i = 0; i < decls.size(); ++i) {
3293  decl_names[i] = decls[i].name();
3294  }
3295  Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
3296  check_error();
3297  return expr_vector(*this, r);
3298  }
3299 
3300 
3301  inline expr expr::substitute(expr_vector const& src, expr_vector const& dst) {
3302  assert(src.size() == dst.size());
3303  array<Z3_ast> _src(src.size());
3304  array<Z3_ast> _dst(dst.size());
3305  for (unsigned i = 0; i < src.size(); ++i) {
3306  _src[i] = src[i];
3307  _dst[i] = dst[i];
3308  }
3309  Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
3310  check_error();
3311  return expr(ctx(), r);
3312  }
3313 
3314  inline expr expr::substitute(expr_vector const& dst) {
3315  array<Z3_ast> _dst(dst.size());
3316  for (unsigned i = 0; i < dst.size(); ++i) {
3317  _dst[i] = dst[i];
3318  }
3319  Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
3320  check_error();
3321  return expr(ctx(), r);
3322  }
3323 
3324 
3325 
3326 }
3327 
3330 #undef Z3_THROW
3331 #endif
3332 
Z3_probe Z3_API Z3_probe_and(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when p1 and p2 evaluates to true.
cube_generator cubes(expr_vector &vars)
Definition: z3++.h:2327
ast_vector_tpl(context &c)
Definition: z3++.h:1704
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
expr distinct(expr_vector const &args)
Definition: z3++.h:1893
bool is_uint(unsigned i) const
Definition: z3++.h:2115
expr mod(expr const &a, expr const &b)
Definition: z3++.h:1193
friend expr mk_or(expr_vector const &args)
Definition: z3++.h:1946
Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
stats statistics() const
Definition: z3++.h:2655
Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi)
Create a regular expression loop. The supplied regular expression r is repeated between lo and hi tim...
Z3_goal Z3_API Z3_mk_goal(Z3_context c, bool models, bool unsat_cores, bool proofs)
Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or trans...
Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o)
Return objectives on the optimization context. If the objective function is a max-sat objective it is...
Z3_ast Z3_API Z3_mk_fpa_fma(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Floating-point fused multiply-add.
void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s)
Increment the reference counter of the given statistics object.
Z3_ast Z3_API Z3_mk_true(Z3_context c)
Create an AST node representing true.
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)
Create a new fixedpoint context.
Z3_probe Z3_API Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the va...
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:146
Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)
Create a bit-vector type of the given size.
friend expr operator|(expr const &a, expr const &b)
Definition: z3++.h:1477
Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nor.
void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value)
Set a global (or module) parameter. This setting is shared by all Z3 contexts.
sort bool_sort()
Return the Boolean sort.
Definition: z3++.h:2728
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.
friend expr atmost(expr_vector const &es, unsigned bound)
Definition: z3++.h:1868
expr get_const_interp(func_decl c) const
Definition: z3++.h:2059
friend expr operator+(expr const &a, expr const &b)
Definition: z3++.h:1265
Z3_string Z3_API Z3_apply_result_to_string(Z3_context c, Z3_apply_result r)
Convert the Z3_apply_result object returned by Z3_tactic_apply into a string.
void add_const_interp(func_decl &f, expr &value)
Definition: z3++.h:2085
expr mk_and(expr_vector const &args)
Definition: z3++.h:1952
friend expr pw(expr const &a, expr const &b)
Definition: z3++.h:1189
bool is_decided_unsat() const
Definition: z3++.h:2361
bool operator!=(cube_iterator const &other)
Definition: z3++.h:2295
void Z3_API Z3_fixedpoint_add_rule(Z3_context c, Z3_fixedpoint d, Z3_ast rule, Z3_symbol name)
Add a universal Horn clause as a named rule. The horn_rule should be of the form:
bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned int....
Z3_ast Z3_API Z3_mk_fpa_rtz(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
bool is_eq() const
Definition: z3++.h:980
void set(char const *k, bool v)
Definition: z3++.h:2157
model(context &c)
Definition: z3++.h:2022
Z3_ast Z3_API Z3_mk_false(Z3_context c)
Create an AST node representing false.
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas on the solver.
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
Z3_probe Z3_API Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than or equal to the...
iterator operator++(int)
Definition: z3++.h:1749
tactic & operator=(tactic const &s)
Definition: z3++.h:2427
bool is_bool() const
Return true if this sort is the Boolean sort.
Definition: z3++.h:536
sort re_sort(sort &seq_sort)
Return a regular expression sort over sequences seq_sort.
Definition: z3++.h:2734
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
bool is_datatype() const
Return true if this is a Datatype expression.
Definition: z3++.h:682
void add_fact(func_decl &f, unsigned *args)
Definition: z3++.h:2672
Z3_param_descrs Z3_API Z3_tactic_get_param_descrs(Z3_context c, Z3_tactic t)
Return the parameter description set for the given tactic object.
probe(context &c, Z3_probe s)
Definition: z3++.h:2510
void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g)
Erase all formulas from the given goal.
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:886
expr pbeq(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:1860
Z3_sort Z3_API Z3_mk_tuple_sort(Z3_context c, Z3_symbol mk_tuple_name, unsigned num_fields, Z3_symbol const field_names[], Z3_sort const field_sorts[], Z3_func_decl *mk_tuple_decl, Z3_func_decl proj_decl[])
Create a tuple type.
friend expr xnor(expr const &a, expr const &b)
Definition: z3++.h:1483
bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx)
Return true if the given statistical data is a unsigned integer.
unsigned uint_value(unsigned i) const
Definition: z3++.h:2117
probe & operator=(probe const &s)
Definition: z3++.h:2514
Z3_tactic Z3_API Z3_tactic_when(Z3_context c, Z3_probe p, Z3_tactic t)
Return a tactic that applies t to a given goal is the probe p evaluates to true. If p evaluates to fa...
func_entry entry(unsigned i) const
Definition: z3++.h:2003
Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err)
Return a string describing the given error code.
unsigned get_num_levels(func_decl &p)
Definition: z3++.h:2683
double double_value(unsigned i) const
Definition: z3++.h:2118
std::string documentation(symbol const &s)
Definition: z3++.h:450
stats statistics() const
Definition: z3++.h:2208
Z3_error_code check_error() const
Definition: z3++.h:405
Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
std::string help() const
Definition: z3++.h:2659
void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t)
Increment the reference counter of the given tactic.
sort fpa_rounding_mode()
Return a RoundingMode sort.
Definition: z3++.h:2749
friend expr operator>=(expr const &a, expr const &b)
Definition: z3++.h:1319
#define Z3_THROW(x)
Definition: z3++.h:96
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d)
Return the constant declaration name as a symbol.
Z3_string Z3_API Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s)
Retrieve documentation string corresponding to parameter name s.
model get_model() const
Definition: z3++.h:2640
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits)
Create a FloatingPoint sort.
Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g)
Convert a goal into a DIMACS formatted string. The goal must be in CNF. You can convert a goal to CNF...
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2725
unsigned size() const
Definition: z3++.h:2353
void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f)
Increment the reference counter of the given Z3_func_interp object.
expr zext(expr const &a, unsigned i)
Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i,...
Definition: z3++.h:1658
bool operator==(cube_iterator const &other)
Definition: z3++.h:2292
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.
void set(char const *k, symbol const &s)
Definition: z3++.h:473
Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index)
Retrieve from s the unit sequence positioned at position index.
Z3_params Z3_API Z3_mk_params(Z3_context c)
Create a Z3 (empty) parameter set. Starting at Z3 4.0, parameter sets are used to configure many comp...
expr operator[](int i) const
Definition: z3++.h:2354
Z3_tactic Z3_API Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1.
friend bool eq(ast const &a, ast const &b)
Return true if the ASTs are structurally identical.
Definition: z3++.h:508
Z3_symbol_kind Z3_API Z3_get_symbol_kind(Z3_context c, Z3_symbol s)
Return Z3_INT_SYMBOL if the symbol was constructed using Z3_mk_int_symbol, and Z3_STRING_SYMBOL if th...
void Z3_API Z3_ast_vector_inc_ref(Z3_context c, Z3_ast_vector v)
Increment the reference counter of the given AST vector.
void push()
Definition: z3++.h:2162
expr contains(expr const &s)
Definition: z3++.h:1109
func_decl get_const_decl(unsigned i) const
Definition: z3++.h:2048
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
tactic cond(probe const &p, tactic const &t1, tactic const &t2)
Definition: z3++.h:2718
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
expr extract(expr const &offset, expr const &length) const
sequence and regular expression operations.
Definition: z3++.h:1094
solver(context &c, simple)
Definition: z3++.h:2142
void Z3_API Z3_params_set_uint(Z3_context c, Z3_params p, Z3_symbol k, unsigned v)
Add a unsigned parameter k with value v to the parameter set p.
expr(context &c)
Definition: z3++.h:645
void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a)
Add a constant interpretation.
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3244
expr bv_val(int n, unsigned sz)
Definition: z3++.h:2931
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than.
expr operator!=(expr const &a, expr const &b)
Definition: z3++.h:1255
Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2)
Logical shift right.
Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i)
Return the declaration of the i-th function in the given model.
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
Z3_ast_vector Z3_API Z3_fixedpoint_from_string(Z3_context c, Z3_fixedpoint f, Z3_string s)
Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context....
Definition: z3_api.h:1323
func_interp & operator=(func_interp const &s)
Definition: z3++.h:1994
friend expr operator!=(expr const &a, expr const &b)
Definition: z3++.h:1255
iterator & operator++()
Definition: z3++.h:1745
Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2)
Arithmetic shift right.
Z3_probe Z3_API Z3_probe_gt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than the value retur...
func_decl get_func_decl(unsigned i) const
Definition: z3++.h:2049
probe(context &c, double val)
Definition: z3++.h:2509
bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a)
Return true if the given AST is a real algebraic number.
expr select(expr const &a, expr const &i)
Definition: z3++.h:3075
Definition: z3++.h:130
Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v)
Array update.
func_entry & operator=(func_entry const &s)
Definition: z3++.h:1971
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
Z3_ast Z3_API Z3_ast_vector_get(Z3_context c, Z3_ast_vector v, unsigned i)
Return the AST at position i in the AST vector v.
void set(char const *param, char const *value)
Set global parameter param with string value.
Definition: z3++.h:114
Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name)
Return a tactic associated with the given name. The complete list of tactics may be obtained using th...
void set(char const *k, char const *v)
Definition: z3++.h:2161
Definition: z3++.h:137
expr fma(expr const &a, expr const &b, expr const &c, expr const &rm)
Definition: z3++.h:1537
tactic when(probe const &p, tactic const &t)
Definition: z3++.h:2712
Z3_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.
void set_else(expr &value)
Definition: z3++.h:2008
config()
Definition: z3++.h:108
friend std::ostream & operator<<(std::ostream &out, params const &p)
Definition: z3++.h:478
void set(char const *k, double n)
Definition: z3++.h:472
bool is_algebraic() const
Return true if expression is an algebraic number.
Definition: z3++.h:756
unsigned get_numeral_uint() const
Return uint value of numeral, throw if result cannot fit in machine uint.
Definition: z3++.h:803
void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s)
Decrement the reference counter of the given statistics object.
Z3_sort Z3_API Z3_get_array_sort_range(Z3_context c, Z3_sort t)
Return the range of the given array sort.
expr lower(handle const &h)
Definition: z3++.h:2643
cube_generator cubes()
Definition: z3++.h:2326
bool is_numeral(double &d) const
Definition: z3++.h:722
expr operator *(expr const &a, expr const &b)
Definition: z3++.h:1295
friend expr operator/(expr const &a, expr const &b)
Definition: z3++.h:1336
friend expr operator &&(expr const &a, expr const &b)
Return an expression representing a and b.
Definition: z3++.h:1221
Z3_probe Z3_API Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned ...
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
void set(char const *param, char const *value)
Update global parameter param with string value.
Definition: z3++.h:203
array(unsigned sz)
Definition: z3++.h:387
std::ostream & operator<<(std::ostream &out, exception const &e)
Definition: z3++.h:90
Z3_solver Z3_API Z3_mk_solver(Z3_context c)
Create a new solver. This solver is a "combined solver" (see combined_solver module) that internally ...
expr extract(unsigned hi, unsigned lo) const
Definition: z3++.h:1080
A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort.
Definition: z3++.h:514
~solver()
Definition: z3++.h:2147
Z3_ast Z3_API Z3_substitute(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const from[], Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs....
sort array_domain() const
Return the domain of this Array sort.
Definition: z3++.h:597
char const * msg() const
Definition: z3++.h:87
T operator[](int i) const
Definition: z3++.h:1710
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
optimize(optimize &o)
Definition: z3++.h:2589
Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than.
Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)
Create a new optimize context.
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.
func_decl(context &c)
Definition: z3++.h:612
void push()
Definition: z3++.h:2702
friend expr operator^(expr const &a, expr const &b)
Definition: z3++.h:1473
~array()
Definition: z3++.h:390
void pop_back()
Definition: z3++.h:1714
expr full_set(sort const &s)
Definition: z3++.h:3137
model(model &src, context &dst, translate)
Definition: z3++.h:2025
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.
sort array_range() const
Return the range of this Array sort.
Definition: z3++.h:603
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s)
Convert string to integer.
friend std::ostream & operator<<(std::ostream &out, ast const &n)
Definition: z3++.h:504
Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem)
Remove an element to a set.
Z3_ast Z3_API Z3_mk_int64(Z3_context c, int64_t v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
T const & operator[](int i) const
Definition: z3++.h:393
Z3_ast Z3_API Z3_mk_set_union(Z3_context c, unsigned num_args, Z3_ast const args[])
Take the union of a list of sets.
Z3_func_decl Z3_API Z3_model_get_const_decl(Z3_context c, Z3_model m, unsigned i)
Return the i-th constant in the given model.
sort bv_sort(unsigned sz)
Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz.
Definition: z3++.h:2731
void interrupt()
Interrupt the current procedure being executed by any object managed by this context....
Definition: z3++.h:221
expr lshr(expr const &a, expr const &b)
logic shift right operator for bitvectors
Definition: z3++.h:1644
expr as_expr() const
Definition: z3++.h:2373
expr udiv(expr const &a, expr const &b)
unsigned division operator for bitvectors.
Definition: z3++.h:1609
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
friend expr concat(expr const &a, expr const &b)
Definition: z3++.h:1902
friend expr mod(expr const &a, expr const &b)
Definition: z3++.h:1193
Z3_symbol Z3_API Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, unsigned i)
Return the name of the parameter at given index i.
std::string help() const
Definition: z3++.h:2444
bool is_bv() const
Return true if this is a Bit-vector expression.
Definition: z3++.h:674
expr upper(handle const &h)
Definition: z3++.h:2648
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1358
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1321
goal(context &c, Z3_goal s)
Definition: z3++.h:2340
optimize & operator=(optimize const &o)
Definition: z3++.h:2593
Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].
std::string to_string() const
Definition: z3++.h:451
expr_vector assertions() const
Definition: z3++.h:2653
bool is_exists() const
Return true if this expression is an existential quantifier.
Definition: z3++.h:743
model(context &c, Z3_model m)
Definition: z3++.h:2023
sort array_sort(sort d, sort r)
Return an array sort for arrays from d to r.
Definition: z3++.h:2762
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:2901
model convert_model(model const &m) const
Definition: z3++.h:2362
void pop()
Definition: z3++.h:2625
Z3_ast Z3_API Z3_func_entry_get_arg(Z3_context c, Z3_func_entry e, unsigned i)
Return an argument of a Z3_func_entry object.
double operator()(goal const &g) const
Definition: z3++.h:2522
bool is_real() const
Return true if this is a real expression.
Definition: z3++.h:666
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)
Return the number of parameters associated with a declaration.
bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
Compare terms.
check_result query(expr &q)
Definition: z3++.h:2673
#define _Z3_MK_UN_(a, mkun)
Definition: z3++.h:1209
fixedpoint(context &c)
Definition: z3++.h:2666
Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than or equal to.
Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name)
Return a probe associated with the given name. The complete list of probes may be obtained using the ...
bool is_datatype() const
Return true if this sort is a Datatype sort.
Definition: z3++.h:560
Z3_string Z3_API Z3_ast_vector_to_string(Z3_context c, Z3_ast_vector v)
Convert AST vector into a string.
tactic(tactic const &s)
Definition: z3++.h:2424
Z3_model Z3_API Z3_goal_convert_model(Z3_context c, Z3_goal g, Z3_model m)
Convert a model of the formulas of a goal to a model of an original goal. The model may be null,...
friend expr operator||(expr const &a, expr const &b)
Return an expression representing a or b.
Definition: z3++.h:1233
sort fpa_rounding_mode()
Return a RoundingMode sort.
Definition: z3++.h:872
void set_enable_exceptions(bool f)
The C++ API uses by defaults exceptions on errors. For applications that don't work well with excepti...
Definition: z3++.h:196
~probe()
Definition: z3++.h:2512
Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic)
Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unkn...
int to_int() const
Definition: z3++.h:419
Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d)
Return declaration kind corresponding to declaration.
func_decl operator[](int i) const
Definition: z3++.h:2051
expr rotate_right(unsigned i)
Definition: z3++.h:1073
~tactic()
Definition: z3++.h:2425
bool is_array() const
Return true if this is a Array expression.
Definition: z3++.h:678
bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a)
Determine if ast is an existential quantifier.
sort operator()(context &c, Z3_ast a)
Definition: z3++.h:1685
check_result check()
Definition: z3++.h:2628
Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[])
Create the intersection of the regular languages.
friend probe operator||(probe const &p1, probe const &p2)
Definition: z3++.h:2571
expr is_int(expr const &e)
Definition: z3++.h:1217
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.
Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s)
Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.
Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[])
Check whether the assertions in the given solver and optional assumptions are consistent or not.
expr operator^(expr const &a, expr const &b)
Definition: z3++.h:1473
unsigned Z3_API Z3_fpa_get_ebits(Z3_context c, Z3_sort s)
Retrieves the number of bits reserved for the exponent in a FloatingPoint sort.
friend std::ostream & operator<<(std::ostream &out, optimize const &s)
Definition: z3++.h:2661
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)
Create the constant array.
std::string get_decimal_string(int precision) const
Return string representation of numeral or algebraic number This method assumes the expression is num...
Definition: z3++.h:769
Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].
void from_string(char const *constraints)
Definition: z3++.h:2658
Exception used to sign API usage errors.
Definition: z3++.h:83
Z3_stats Z3_API Z3_fixedpoint_get_statistics(Z3_context c, Z3_fixedpoint d)
Retrieve statistics information from the last call to Z3_fixedpoint_query.
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
expr itos() const
Definition: z3++.h:1131
Z3_context Z3_API Z3_mk_context_rc(Z3_config c)
Create a context using the given configuration. This function is similar to Z3_mk_context....
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.
bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, uint64_t *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine uint64_t int....
ast_vector_tpl(context &c, Z3_ast_vector v)
Definition: z3++.h:1705
A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort ...
Definition: z3++.h:643
void reset_params()
Definition: z3++.h:78
void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value)
Set a value of a context parameter.
bool is_int() const
Return true if this sort is the Integer sort.
Definition: z3++.h:540
expr operator!(expr const &a)
Definition: z3++.h:1215
bool operator==(iterator const &other)
Definition: z3++.h:1739
expr set_subset(expr const &a, expr const &b)
Definition: z3++.h:3177
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)
Create the empty set.
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition: z3++.h:3123
unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s)
Retrieves the number of bits reserved for the significand in a FloatingPoint sort.
expr & operator=(expr const &n)
Definition: z3++.h:648
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g)
Return true if the given goal contains the formula false.
bool enable_exceptions() const
Definition: z3++.h:198
expr ule(expr const &a, expr const &b)
unsigned less than or equal to operator for bitvectors.
Definition: z3++.h:1585
expr in_re(expr const &s, expr const &re)
Definition: z3++.h:3211
symbol name(unsigned i)
Definition: z3++.h:448
void recdef(func_decl, expr_vector const &args, expr const &body)
Definition: z3++.h:2895
std::string key(unsigned i) const
Definition: z3++.h:2114
void Z3_API Z3_ast_vector_resize(Z3_context c, Z3_ast_vector v, unsigned n)
Resize the AST vector v.
expr simplify(params const &p) const
Return a simplified version of this expression. The parameter p is a set of parameters for the Z3 sim...
Definition: z3++.h:1160
Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s)
Return the length of the sequence s.
Z3_ast Z3_API Z3_mk_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s)
Check if prefix is a prefix of s.
Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s)
Return the set of units modulo model conversion.
Z3_string Z3_API Z3_stats_get_key(Z3_context c, Z3_stats s, unsigned idx)
Return the key (a string) for a particular statistical data.
void set(char const *param, int value)
Update global parameter param with Integer value.
Definition: z3++.h:211
static param_descrs simplify_param_descrs(context &c)
Definition: z3++.h:445
friend expr mk_and(expr_vector const &args)
Definition: z3++.h:1952
Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i)
Return the i-th argument of the given application.
sort domain(unsigned i) const
Definition: z3++.h:619
Z3_ast Z3_API Z3_mk_fpa_rne(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
cube_iterator begin()
Definition: z3++.h:2321
Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re)
Create the complement of the regular language re.
void update_rule(expr &rule, symbol const &name)
Definition: z3++.h:2682
bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g)
Return true if the goal contains false, and it is precise or the product of an over approximation.
func_decl operator()(context &c, Z3_ast a)
Definition: z3++.h:1693
friend expr fma(expr const &a, expr const &b, expr const &c)
FloatingPoint fused multiply-add.
std::string to_string(expr_vector const &queries)
Definition: z3++.h:2698
void Z3_API Z3_func_interp_dec_ref(Z3_context c, Z3_func_interp f)
Decrement the reference counter of the given Z3_func_interp object.
ast_vector_tpl< func_decl > func_decl_vector
Definition: z3++.h:73
stats(context &c)
Definition: z3++.h:2101
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.
void Z3_API Z3_ast_vector_dec_ref(Z3_context c, Z3_ast_vector v)
Decrement the reference counter of the given AST vector.
expr operator>=(expr const &a, expr const &b)
Definition: z3++.h:1319
std::string reason_unknown()
Definition: z3++.h:2681
void add_entry(expr_vector const &args, expr &value)
Definition: z3++.h:2004
Z3_ast Z3_API Z3_mk_set_intersect(Z3_context c, unsigned num_args, Z3_ast const args[])
Take the intersection of a list of sets.
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
bool is_re() const
Return true if this is a regular expression.
Definition: z3++.h:694
expr pw(expr const &a, expr const &b)
Definition: z3++.h:1189
bool empty() const
Definition: z3++.h:1715
Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)
Return the declaration of a constant or function application.
friend std::ostream & operator<<(std::ostream &out, goal const &g)
Definition: z3++.h:2389
Z3_string Z3_API Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p)
Convert a parameter description set into a string. This function is mainly used for printing the cont...
bool is_numeral_i64(int64_t &i) const
Definition: z3++.h:716
friend probe operator>=(probe const &p1, probe const &p2)
Definition: z3++.h:2548
expr(context &c, Z3_ast n)
Definition: z3++.h:646
~goal()
Definition: z3++.h:2342
Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast default_value)
Create a fresh func_interp object, add it to a model for a specified function. It has reference count...
expr set_difference(expr const &a, expr const &b)
Definition: z3++.h:3165
unsigned Z3_API Z3_ast_vector_size(Z3_context c, Z3_ast_vector v)
Return the size of the given AST vector.
expr_vector assertions() const
Definition: z3++.h:2692
bool is_fpa() const
Return true if this sort is a Floating point sort.
Definition: z3++.h:580
expr operator~(expr const &a)
Definition: z3++.h:1535
unsigned num_entries() const
Definition: z3++.h:2002
Z3_ast Z3_API Z3_mk_lambda_const(Z3_context c, unsigned num_bound, Z3_app const bound[], Z3_ast body)
Create a lambda expression using a list of constants that form the set of bound variables.
void Z3_API Z3_fixedpoint_pop(Z3_context c, Z3_fixedpoint d)
Backtrack one backtracking point.
Z3_ast Z3_API Z3_mk_fpa_rtn(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
def tactics(ctx=None)
Definition: z3py.py:7791
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.
friend expr operator-(expr const &a)
Definition: z3++.h:1358
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a string.
Z3_error_code Z3_API Z3_get_error_code(Z3_context c)
Return the error code for the last API call.
friend expr distinct(expr_vector const &args)
Definition: z3++.h:1893
check_result check(unsigned n, expr *const assumptions)
Definition: z3++.h:2180
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.
check_result check(expr_vector assumptions)
Definition: z3++.h:2190
expr rem(expr const &a, expr const &b)
Definition: z3++.h:1197
Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[])
Check consistency and produce optimal values.
probe(context &c, char const *name)
Definition: z3++.h:2508
friend std::ostream & operator<<(std::ostream &out, solver const &s)
Definition: z3++.h:2330
Z3_symbol_kind kind() const
Definition: z3++.h:417
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
expr get_answer()
Definition: z3++.h:2680
Z3_sort Z3_API Z3_mk_string_sort(Z3_context c)
Create a sort for 8 bit strings.
~stats()
Definition: z3++.h:2104
friend expr min(expr const &a, expr const &b)
Definition: z3++.h:1484
sort seq_sort(sort &s)
Return a sequence sort over base sort s.
Definition: z3++.h:2733
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.
Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2)
Maximum of floating-point numbers.
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
friend expr operator<=(expr const &a, expr const &b)
Definition: z3++.h:1400
Z3_tactic Z3_API Z3_tactic_or_else(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that first applies t1 to a given goal, if it fails then returns the result of t2 appl...
expr length() const
Definition: z3++.h:1121
Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s)
Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.
Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve upper bound value or approximation for the i'th optimization objective.
A Context manages all other Z3 objects, global configuration options, etc.
Definition: z3++.h:153
Definition: z3++.h:482
Z3 C++ namespace.
Definition: z3++.h:48
Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Take the set difference between two sets.
expr denominator() const
Definition: z3++.h:860
Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.
sort range() const
Definition: z3++.h:620
expr set_add(expr const &s, expr const &e)
Definition: z3++.h:3141
expr ashr(expr const &a, expr const &b)
arithmetic shift right operator for bitvectors
Definition: z3++.h:1651
expr re_empty(sort const &s)
Definition: z3++.h:3223
unsigned size() const
Definition: z3++.h:2113
void Z3_API Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode)
Select mode for the format used for pretty-printing AST nodes.
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.
Z3_ast Z3_API Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows dividend).
sort fpa_sort()
Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128).
friend tactic operator|(tactic const &t1, tactic const &t2)
Definition: z3++.h:2462
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
expr nor(expr const &a, expr const &b)
Definition: z3++.h:1482
Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p)
Return a probe that evaluates to "true" when p does not evaluate to true.
Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c)
Return the parameter description set for the simplify procedure.
void Z3_API Z3_fixedpoint_push(Z3_context c, Z3_fixedpoint d)
Create a backtracking point.
solver(context &c, Z3_solver s)
Definition: z3++.h:2143
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
Z3 global configuration object.
Definition: z3++.h:103
Z3_decl_kind decl_kind() const
Definition: z3++.h:622
bool is_re() const
Return true if this sort is a regular expression sort.
Definition: z3++.h:572
solver & operator=(solver const &s)
Definition: z3++.h:2149
Z3_ast Z3_API Z3_mk_fpa_rtp(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
void set(char const *param, int value)
Set global parameter param with integer value.
Definition: z3++.h:122
void add_cover(int level, func_decl &p, expr &property)
Definition: z3++.h:2689
expr substitute(expr_vector const &src, expr_vector const &dst)
Apply substitution. Replace src expressions by dst.
Definition: z3++.h:3301
Z3_ast_vector Z3_API Z3_parse_smtlib2_string(Z3_context c, Z3_string str, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Parse the given string using the SMT-LIB2 parser.
iterator begin() const
Definition: z3++.h:1753
ast(context &c, Z3_ast n)
Definition: z3++.h:487
ast_vector_tpl & operator=(ast_vector_tpl const &s)
Definition: z3++.h:1716
expr_vector cube(expr_vector &vars, unsigned cutoff)
Definition: z3++.h:2239
expr operator<=(expr const &a, expr const &b)
Definition: z3++.h:1400
handle add(expr const &e, char const *weight)
Definition: z3++.h:2612
friend std::ostream & operator<<(std::ostream &out, apply_result const &r)
Definition: z3++.h:2413
Z3_goal_prec precision() const
Definition: z3++.h:2355
void set(char const *k, char const *s)
Definition: z3++.h:474
expr bv_const(char const *name, unsigned sz)
Definition: z3++.h:2910
context & ctx() const
Definition: z3++.h:404
sort fpa_sort()
Definition: z3++.h:2738
void Z3_API Z3_param_descrs_inc_ref(Z3_context c, Z3_param_descrs p)
Increment the reference counter of the given parameter description set.
Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f)
Return the 'else' value of the given function interpretation.
Z3_sort_kind sort_kind() const
Return the internal sort kind.
Definition: z3++.h:528
T back() const
Definition: z3++.h:1713
expr string_val(char const *s)
Definition: z3++.h:2945
tactic(context &c, char const *name)
Definition: z3++.h:2422
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.
void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d)
Increment the reference counter of the given fixedpoint context.
void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p)
Increment the reference counter of the given probe.
sort string_sort()
Return the sort for ASCII strings.
Definition: z3++.h:2732
bool is_lambda() const
Return true if this expression is a lambda expression.
Definition: z3++.h:747
tactic with(tactic const &t, params const &p)
Definition: z3++.h:2475
expr empty_set(sort const &s)
Definition: z3++.h:3133
Z3_ast Z3_API Z3_mk_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s)
Check if suffix is a suffix of s.
Z3_ast_vector Z3_API Z3_mk_ast_vector(Z3_context c)
Return an empty AST vector.
Z3_bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast *v)
Evaluate the AST node t in the given model. Return true if succeeded, and store the result in v.
expr as_array(func_decl &f)
Definition: z3++.h:3112
expr plus(expr const &re)
Definition: z3++.h:3214
expr xnor(expr const &a, expr const &b)
Definition: z3++.h:1483
void reset()
Definition: z3++.h:2164
expr_vector unsat_core() const
Definition: z3++.h:2641
Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1)
Coerce an integer to a real.
iterator end() const
Definition: z3++.h:1754
Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, unsigned backtrack_level)
extract a next cube for a solver. The last cube is the constant true or false. The number of (non-con...
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point remainder.
Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)
Shift left.
~config()
Definition: z3++.h:109
bool is_arith() const
Return true if this sort is the Integer or Real sort.
Definition: z3++.h:548
void from_string(char const *s)
Definition: z3++.h:2177
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
bool is_relation() const
Return true if this sort is a Relation sort.
Definition: z3++.h:564
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst)
Replace the first occurrence of src with dst in s.
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:176
unsigned Z3_API Z3_goal_depth(Z3_context c, Z3_goal g)
Return the depth of the given goal. It tracks how many transformations were applied to it.
void Z3_API Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r)
Increment the reference counter of the given Z3_apply_result object.
friend expr atleast(expr_vector const &es, unsigned bound)
Definition: z3++.h:1876
bool is_real() const
Return true if this sort is the Real sort.
Definition: z3++.h:544
void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e)
Increment the reference counter of the given Z3_func_entry object.
void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a)
Decrement the reference counter of the given AST. The context c should have been created using Z3_mk_...
iterator(iterator &other)
Definition: z3++.h:1736
func_entry(context &c, Z3_func_entry e)
Definition: z3++.h:1967
void resize(unsigned sz)
Definition: z3++.h:1712
void Z3_API Z3_del_config(Z3_config c)
Delete the given configuration object.
expr body() const
Return the 'body' of this quantifier.
Definition: z3++.h:908
expr operator()() const
Definition: z3++.h:2971
void add(expr const &e, char const *p)
Definition: z3++.h:2171
func_decl to_func_decl(context &c, Z3_func_decl f)
Definition: z3++.h:1577
unsigned hash() const
Definition: z3++.h:494
optimize(context &c)
Definition: z3++.h:2588
goal operator[](int i) const
Definition: z3++.h:2410
expr min(expr const &a, expr const &b)
Definition: z3++.h:1484
cube_iterator(solver &s, expr_vector &vars, unsigned &cutoff, bool end)
Definition: z3++.h:2266
param_descrs(param_descrs const &o)
Definition: z3++.h:436
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)
Create a backtracking point.
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re)
Create the regular language [re].
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:726
expr(expr const &n)
Definition: z3++.h:647
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].
Z3_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const to[])
Substitute the free variables in a with the expressions in to. For every i smaller than num_exprs,...
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
unsigned Z3_API Z3_get_bv_sort_size(Z3_context c, Z3_sort t)
Return the size of the given bit-vector sort.
Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve lower bound value or approximation for the i'th optimization objective.
Definition: z3++.h:1960
Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)
Create an array type.
check_result check()
Definition: z3++.h:2179
expr_vector objectives() const
Definition: z3++.h:2654
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.
Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Check for subsetness of sets.
std::string to_smt2(char const *status="unknown")
Definition: z3++.h:2216
Z3_goal_prec Z3_API Z3_goal_precision(Z3_context c, Z3_goal g)
Return the "precision" of the given goal. Goals can be transformed using over and under approximation...
expr operator+(expr const &a, expr const &b)
Definition: z3++.h:1265
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2799
expr operator &&(expr const &a, expr const &b)
Definition: z3++.h:1221
expr operator()(context &c, Z3_ast a)
Definition: z3++.h:1674
Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than or equal to.
Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem)
Add an element to a set.
std::string help() const
Definition: z3++.h:2695
friend probe operator!(probe const &p)
Definition: z3++.h:2574
Z3_ast Z3_API Z3_mk_store_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const *idxs, Z3_ast v)
n-ary Array update.
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2870
bool is_arith() const
Return true if this is an integer or real expression.
Definition: z3++.h:670
bool is_well_sorted() const
Return true if this expression is well sorted (aka type correct).
Definition: z3++.h:761
bool is_numeral_u64(uint64_t &i) const
Definition: z3++.h:717
Z3_ast Z3_API Z3_mk_real(Z3_context c, int num, int den)
Create a real from a fraction.
Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg)
Take the complement of a set.
friend tactic operator &(tactic const &t1, tactic const &t2)
Definition: z3++.h:2455
unsigned Z3_API Z3_get_ast_hash(Z3_context c, Z3_ast a)
Return a hash code for the given AST. The hash code is structural. You can use Z3_get_ast_id intercha...
bool is_implies() const
Definition: z3++.h:979
Z3_string Z3_API Z3_params_to_string(Z3_context c, Z3_params p)
Convert a parameter set into a string. This function is mainly used for printing the contents of a pa...
std::string str() const
Definition: z3++.h:418
expr re_complement(expr const &a)
Definition: z3++.h:3241
expr srem(expr const &a, expr const &b)
signed remainder operator for bitvectors
Definition: z3++.h:1616
Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than or equal to.
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.
expr set_intersect(expr const &a, expr const &b)
Definition: z3++.h:3157
void from_string(char const *s)
Definition: z3++.h:2669
Z3_ast Z3_API Z3_mk_exists_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Similar to Z3_mk_forall_const.
bool inconsistent() const
Definition: z3++.h:2356
exception(char const *msg)
Definition: z3++.h:86
Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f)
Create array with the same interpretation as a function. The array satisfies the property (f x) = (se...
solver(solver const &s)
Definition: z3++.h:2146
Z3_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const *domain, Z3_sort range)
Create an array type with N arguments.
bool is_fpa() const
Return true if this is a FloatingPoint expression. .
Definition: z3++.h:708
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:98
Z3_ast_vector Z3_API Z3_fixedpoint_from_file(Z3_context c, Z3_fixedpoint f, Z3_string s)
Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context....
~optimize()
Definition: z3++.h:2600
unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a)
Return the number of argument of an application. If t is an constant, then the number of arguments is...
friend expr max(expr const &a, expr const &b)
Definition: z3++.h:1499
Z3_tactic Z3_API Z3_tactic_par_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1....
expr fpa_const(char const *name, unsigned ebits, unsigned sbits)
Definition: z3++.h:2911
expr at(expr const &index) const
Definition: z3++.h:1115
void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g)
Decrement the reference counter of the given goal.
Z3_string Z3_API Z3_fixedpoint_get_reason_unknown(Z3_context c, Z3_fixedpoint d)
Retrieve a string that describes the last status returned by Z3_fixedpoint_query.
expr re_intersect(expr_vector const &args)
Definition: z3++.h:3233
Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string s)
Create a string constant out of the string that is passed in.
expr real_val(int n, int d)
Definition: z3++.h:2924
bool is_true() const
Definition: z3++.h:973
ast_vector_tpl< sort > sort_vector
Definition: z3++.h:72
bool is_bool() const
Return true if this is a Boolean expression.
Definition: z3++.h:658
void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a file.
void add(expr const &e)
Definition: z3++.h:2602
unsigned fpa_ebits() const
Definition: z3++.h:589
Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a)
Return the numerator (as a numeral AST) of a numeral AST of sort Real.
expr prefixof(expr const &a, expr const &b)
Definition: z3++.h:3196
void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h)
Register a Z3 error handler.
Z3_ast Z3_API Z3_mk_sign_ext(Z3_context c, unsigned i, Z3_ast t1)
Sign-extend of the given bit-vector to the (signed) equivalent bit-vector of size m+i,...
func_interp(func_interp const &s)
Definition: z3++.h:1991
Z3_func_interp Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f)
Return the interpretation of the function f in the model m. Return NULL, if the model does not assign...
model & operator=(model const &s)
Definition: z3++.h:2028
void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m)
Decrement the reference counter of the given model.
expr_vector parse_file(char const *file)
Definition: z3++.h:3261
Z3_lbool bool_value() const
Definition: z3++.h:848
Z3_ast Z3_API Z3_mk_rotate_right(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the right i times.
tactic par_and_then(tactic const &t1, tactic const &t2)
Definition: z3++.h:2494
unsigned Z3_API Z3_param_descrs_size(Z3_context c, Z3_param_descrs p)
Return the number of parameters in the given parameter description set.
friend expr operator==(expr const &a, expr const &b)
Definition: z3++.h:1246
void set(char const *param, bool value)
Set global parameter param with Boolean value.
Definition: z3++.h:118
unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m)
Return the number of constants assigned by the given model.
expr loop(unsigned lo)
create a looping regular expression.
Definition: z3++.h:1141
Z3_ast Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a)
Return the interpretation (i.e., assignment) of constant a in the model m. Return NULL,...
void add(expr const &e)
Definition: z3++.h:2165
void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d)
Decrement the reference counter of the given fixedpoint context.
Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point multiplication.
unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g)
Return the number of formulas in the given goal.
expr repeat(unsigned i)
Definition: z3++.h:1074
expr ugt(expr const &a, expr const &b)
unsigned greater than operator for bitvectors.
Definition: z3++.h:1603
Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.
goal & operator=(goal const &s)
Definition: z3++.h:2344
expr option(expr const &re)
Definition: z3++.h:3217
~params()
Definition: z3++.h:461
Z3_sort Z3_API Z3_get_array_sort_domain(Z3_context c, Z3_sort t)
Return the domain of the given array sort. In the case of a multi-dimensional array,...
expr const_array(sort const &d, expr const &v)
Definition: z3++.h:3129
stats(stats const &s)
Definition: z3++.h:2103
bool is_and() const
Definition: z3++.h:976
std::string to_string() const
Definition: z3++.h:496
cube_iterator operator++(int)
Definition: z3++.h:2288
bool is_or() const
Definition: z3++.h:977
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f)
Retrieve set of rules from fixedpoint context.
expr_vector non_units() const
Definition: z3++.h:2211
expr set_member(expr const &s, expr const &e)
Definition: z3++.h:3173
Z3_model Z3_API Z3_mk_model(Z3_context c)
Create a fresh model object. It has reference count 0.
friend std::ostream & operator<<(std::ostream &out, model const &m)
Definition: z3++.h:2092
Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target)
Copy a solver s from the context source to the context target.
int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s)
Return the symbol int value.
void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p)
Decrement the reference counter of the given parameter set.
~func_entry()
Definition: z3++.h:1969
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:653
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)
Decrement the reference counter of the given optimize context.
int64_t get_numeral_int64() const
Return int64_t value of numeral, throw if result cannot fit in int64_t.
Definition: z3++.h:820
sort uninterpreted_sort(char const *name)
create an uninterpreted sort with the name given by the string or symbol.
Definition: z3++.h:2791
double Z3_API Z3_probe_apply(Z3_context c, Z3_probe p, Z3_goal g)
Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0....
Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s)
Retrieve the unsat core for the last Z3_solver_check_assumptions The unsat core is a subset of the as...
expr stoi() const
Definition: z3++.h:1126
void reset()
Definition: z3++.h:2358
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows divisor).
T * ptr()
Definition: z3++.h:395
params(params const &s)
Definition: z3++.h:460
Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e)
Return the value of this point.
unsigned Z3_API Z3_stats_get_uint_value(Z3_context c, Z3_stats s, unsigned idx)
Return the unsigned value of the given statistical data.
void set_param(char const *param, char const *value)
Definition: z3++.h:75
unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id)
Assert soft constraint to the optimization context.
Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than.
unsigned lo() const
Definition: z3++.h:1081
friend void check_context(object const &a, object const &b)
Definition: z3++.h:408
bool is_array() const
Return true if this sort is a Array sort.
Definition: z3++.h:556
Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g)
Convert a goal into a string.
handle maximize(expr const &e)
Definition: z3++.h:2616
unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m)
Return the number of function interpretations in the given model.
friend expr operator *(expr const &a, expr const &b)
Definition: z3++.h:1295
Z3_param_kind
The different kinds of parameters that can be associated with parameter sets. (see Z3_mk_params).
Definition: z3_api.h:1280
bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int....
friend probe operator<=(probe const &p1, probe const &p2)
Definition: z3++.h:2543
expr get_cover_delta(int level, func_decl &p)
Definition: z3++.h:2684
Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a string of a numeric constant term.
expr_vector const * operator->() const
Definition: z3++.h:2289
expr int_const(char const *name)
Definition: z3++.h:2908
Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 rem arg2.
friend std::ostream & operator<<(std::ostream &out, exception const &e)
Definition: z3++.h:90
expr abs(expr const &a)
Definition: z3++.h:1514
expr replace(expr const &src, expr const &dst) const
Definition: z3++.h:1098
symbol(symbol const &s)
Definition: z3++.h:414
expr value() const
Definition: z3++.h:1978
Z3_ast_vector Z3_API Z3_parse_smtlib2_file(Z3_context c, Z3_string file_name, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Similar to Z3_parse_smtlib2_string, but reads the benchmark from a file.
unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e)
Return the number of arguments in a Z3_func_entry object.
bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, int64_t *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int64_t int....
Z3_symbol_kind
The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See Z3_...
Definition: z3_api.h:112
expr sum(expr_vector const &args)
Definition: z3++.h:1884
Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re)
Create the regular language re+.
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
sort(context &c)
Definition: z3++.h:516
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)
Retrieve the model for the last Z3_optimize_check.
unsigned arity() const
Definition: z3++.h:618
bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx)
Return true if the given statistical data is a double.
goal(context &c, bool models=true, bool unsat_cores=false, bool proofs=false)
Definition: z3++.h:2339
expr suffixof(expr const &a, expr const &b)
Definition: z3++.h:3190
void from_file(char const *filename)
Definition: z3++.h:2657
void Z3_API Z3_interrupt(Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers,...
bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a)
Test if there exists an interpretation (i.e., assignment) for a in the model m.
check_result consequences(expr_vector &assumptions, expr_vector &vars, expr_vector &conseq)
Definition: z3++.h:2202
expr operator<(expr const &a, expr const &b)
Definition: z3++.h:1425
unsigned num_exprs() const
Definition: z3++.h:2359
object(context &c)
Definition: z3++.h:402
friend expr operator>(expr const &a, expr const &b)
Definition: z3++.h:1447
handle add(expr const &e, unsigned weight)
Definition: z3++.h:2606
bool is_numeral(std::string &s, unsigned precision) const
Definition: z3++.h:721
Z3_param_descrs Z3_API Z3_fixedpoint_get_param_descrs(Z3_context c, Z3_fixedpoint f)
Return the parameter description set for the given fixedpoint object.
ast(context &c)
Definition: z3++.h:486
object(object const &s)
Definition: z3++.h:403
friend expr nand(expr const &a, expr const &b)
Definition: z3++.h:1481
void set(params const &p)
Definition: z3++.h:2694
expr arg(unsigned i) const
Return the i-th argument of this application. This method assumes the expression is an application.
Definition: z3++.h:901
expr atleast(expr_vector const &es, unsigned bound)
Definition: z3++.h:1876
friend tactic with(tactic const &t, params const &p)
Definition: z3++.h:2475
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
expr real_const(char const *name)
Definition: z3++.h:2909
bool is_relation() const
Return true if this is a Relation expression.
Definition: z3++.h:686
Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort s)
Create a sequence sort out of the sort for the elements.
sort(context &c, Z3_ast a)
Definition: z3++.h:518
bool is_const() const
Return true if this expression is a constant (i.e., an application with 0 arguments).
Definition: z3++.h:730
friend probe operator==(probe const &p1, probe const &p2)
Definition: z3++.h:2563
unsigned h() const
Definition: z3++.h:2586
Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1)
Repeat the given bit-vector up length i.
unsigned size() const
Definition: z3++.h:2409
friend expr operator &(expr const &a, expr const &b)
Definition: z3++.h:1469
unsigned Z3_API Z3_fixedpoint_get_num_levels(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred)
Query the PDR engine for the maximal levels properties are known about predicate.
Z3_tactic Z3_API Z3_tactic_using_params(Z3_context c, Z3_tactic t, Z3_params p)
Return a tactic that applies t using the given set of parameters.
double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a)
Return numeral as a double.
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.
bool is_decided_sat() const
Definition: z3++.h:2360
Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re)
Create the regular language re*.
expr sext(expr const &a, unsigned i)
Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i,...
Definition: z3++.h:1663
Z3_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s)
Check whether the assertions in a given solver are consistent or not.
Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context dst)
translate model from context c to context dst.
void from_file(char const *file)
Definition: z3++.h:2176
Z3_sort Z3_API Z3_get_domain(Z3_context c, Z3_func_decl d, unsigned i)
Return the sort of the i-th parameter of the given function declaration.
void Z3_API Z3_fixedpoint_add_cover(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property)
Add property about the predicate pred. Add a property of predicate pred at level. It gets pushed forw...
Definition: z3++.h:134
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.
Z3_sort Z3_API Z3_mk_real_sort(Z3_context c)
Create the real type.
friend expr pbeq(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:1860
Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision)
Return numeral as a string in decimal notation. The result has at most precision decimal places.
Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set)
Check for set membership.
Z3_ast Z3_API Z3_mk_fpa_rna(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
bool is_numeral_i(int &i) const
Definition: z3++.h:718
expr empty(sort const &s)
Definition: z3++.h:3185
Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, uint64_t v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length)
Extract subsequence starting at offset of length.
Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset)
Return index of first occurrence of substr in s starting from offset offset. If s does not contain su...
expr_vector units() const
Definition: z3++.h:2212
Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point addition.
Z3_config Z3_API Z3_mk_config(void)
Create a configuration object for the Z3 context object.
symbol & operator=(symbol const &s)
Definition: z3++.h:415
~model()
Definition: z3++.h:2026
cube_generator(solver &s, expr_vector &vars)
Definition: z3++.h:2314
friend tactic par_and_then(tactic const &t1, tactic const &t2)
Definition: z3++.h:2494
expr_vector rules() const
Definition: z3++.h:2693
sort real_sort()
Return the Real sort.
Definition: z3++.h:2730
void set(char const *k, unsigned v)
Definition: z3++.h:2158
Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi)
Create the range regular expression over two sequences of length 1.
unsigned Z3_API Z3_goal_num_exprs(Z3_context c, Z3_goal g)
Return the number of formulas, subformulas and terms in the given goal.
friend std::ostream & operator<<(std::ostream &out, ast_vector_tpl const &v)
Definition: z3++.h:1755
expr re_full(sort const &s)
Definition: z3++.h:3228
expr_vector const & operator *() const
Definition: z3++.h:2290
Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d)
Return the range of the given declaration.
ast_vector_tpl(ast_vector_tpl const &s)
Definition: z3++.h:1706
friend expr rem(expr const &a, expr const &b)
Definition: z3++.h:1197
expr num_val(int n, sort const &s)
Definition: z3++.h:2948
bool is_forall() const
Return true if this expression is a universal quantifier.
Definition: z3++.h:739
void Z3_API Z3_fixedpoint_update_rule(Z3_context c, Z3_fixedpoint d, Z3_ast a, Z3_symbol name)
Update a named rule. A rule with the same name must have been previously created.
bool eq(ast const &a, ast const &b)
Definition: z3++.h:508
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.
bool is_bv() const
Return true if this sort is a Bit-vector sort.
Definition: z3++.h:552
symbol int_symbol(int n)
Create a Z3 symbol based on the given integer.
Definition: z3++.h:2726
Z3_tactic Z3_API Z3_tactic_repeat(Z3_context c, Z3_tactic t, unsigned max)
Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of...
expr loop(unsigned lo, unsigned hi)
Definition: z3++.h:1146
expr else_value() const
Definition: z3++.h:2001
expr fpa_val(double n)
Definition: z3++.h:2942
Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d)
Retrieve statistics information from the last call to Z3_optimize_check.
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
friend probe operator>(probe const &p1, probe const &p2)
Definition: z3++.h:2558
expr numerator() const
Definition: z3++.h:852
expr indexof(expr const &s, expr const &substr, expr const &offset)
Definition: z3++.h:3202
void from_file(char const *s)
Definition: z3++.h:2670
void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p)
Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p.
expr set_complement(expr const &a)
Definition: z3++.h:3169
Z3_ast Z3_API Z3_mk_fpa_numeral_double(Z3_context c, double v, Z3_sort ty)
Create a numeral of FloatingPoint sort from a double.
Z3_tactic Z3_API Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal if the probe p evaluates to true, and t2 if p evaluat...
param_descrs & operator=(param_descrs const &o)
Definition: z3++.h:437
expr unit() const
Definition: z3++.h:1104
expr operator>(expr const &a, expr const &b)
Definition: z3++.h:1447
Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] - ... - args[num_args - 1].
expr simplify() const
Return a simplified version of this expression.
Definition: z3++.h:1156
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:141
expr star(expr const &re)
Definition: z3++.h:3220
Z3_tactic Z3_API Z3_tactic_par_or(Z3_context c, unsigned num, Z3_tactic const ts[])
Return a tactic that applies the given tactics in parallel.
friend expr operator~(expr const &a)
Definition: z3++.h:1535
Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
expr operator==(expr const &a, expr const &b)
Definition: z3++.h:1246
symbol name() const
Return name of sort.
Definition: z3++.h:532
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)
Create a new incremental solver.
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
Z3_tactic Z3_API Z3_tactic_try_for(Z3_context c, Z3_tactic t, unsigned ms)
Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms mil...
#define MK_EXPR1(_fn, _arg)
Definition: z3++.h:3118
param_descrs(context &c, Z3_param_descrs d)
Definition: z3++.h:435
void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value)
Set a configuration parameter.
friend tactic repeat(tactic const &t, unsigned max)
Definition: z3++.h:2469
expr operator|(expr const &a, expr const &b)
Definition: z3++.h:1477
Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s)
Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the commands Z3_solver_ch...
unsigned hi() const
Definition: z3++.h:1082
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point division.
unsigned num_args() const
Definition: z3++.h:1979
friend tactic par_or(unsigned n, tactic const *tactics)
Definition: z3++.h:2485
expr pbge(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:1852
Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re)
Create an empty regular expression of sort re.
friend expr abs(expr const &a)
Definition: z3++.h:1514
tactic(context &c, Z3_tactic s)
Definition: z3++.h:2423
void check_context(object const &a, object const &b)
Definition: z3++.h:408
expr arg(unsigned i) const
Definition: z3++.h:1980
unsigned fpa_sbits() const
Definition: z3++.h:591
Z3_ast_vector Z3_API Z3_optimize_get_assertions(Z3_context c, Z3_optimize o)
Return the set of asserted formulas on the optimization context.
void check_parser_error() const
Definition: z3++.h:185
Z3_probe Z3_API Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned...
Z3_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f)
Return a string describing all fixedpoint available parameters.
expr bool_const(char const *name)
Definition: z3++.h:2907
expr urem(expr const &a, expr const &b)
unsigned reminder operator for bitvectors
Definition: z3++.h:1630
void Z3_API Z3_params_set_double(Z3_context c, Z3_params p, Z3_symbol k, double v)
Add a double parameter k with value v to the parameter set p.
solver mk_solver() const
Definition: z3++.h:2434
void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a)
Add a new formula a to the given goal. The formula is split according to the following procedure that...
Z3_tactic Z3_API Z3_tactic_fail_if(Z3_context c, Z3_probe p)
Return a tactic that fails if the probe p evaluates to false.
rounding_mode
Definition: z3++.h:133
std::string reason_unknown() const
Definition: z3++.h:2207
Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize t)
Return a string containing a description of parameters accepted by optimize.
bool is_ite() const
Definition: z3++.h:981
Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s)
Return the symbol name.
model get_model() const
Definition: z3++.h:2201
bool operator!=(iterator const &other)
Definition: z3++.h:1742
void set_rounding_mode(rounding_mode rm)
Sets RoundingMode of FloatingPoints.
Definition: z3++.h:2760
friend expr ite(expr const &c, expr const &t, expr const &e)
Create the if-then-else expression ite(c, t, e)
Definition: z3++.h:1550
Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c, Z3_solver s, Z3_ast_vector assumptions, Z3_ast_vector variables, Z3_ast_vector consequences)
retrieve consequences from solver that determine values of the supplied function symbols.
Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i)
Return one of the subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
unsigned num_consts() const
Definition: z3++.h:2046
friend expr nor(expr const &a, expr const &b)
Definition: z3++.h:1482
params & operator=(params const &s)
Definition: z3++.h:463
friend std::ostream & operator<<(std::ostream &out, symbol const &s)
Definition: z3++.h:423
Z3_sort_kind Z3_API Z3_get_sort_kind(Z3_context c, Z3_sort t)
Return the sort kind (e.g., array, tuple, int, bool, etc).
model(model const &s)
Definition: z3++.h:2024
expr proof() const
Definition: z3++.h:2213
bool is_numeral_u(unsigned &i) const
Definition: z3++.h:719
check_result query(func_decl_vector &relations)
Definition: z3++.h:2674
Z3_lbool Z3_API Z3_get_bool_value(Z3_context c, Z3_ast a)
Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF otherwise.
probe(probe const &s)
Definition: z3++.h:2511
Z3_param_kind Z3_API Z3_param_descrs_get_kind(Z3_context c, Z3_param_descrs p, Z3_symbol n)
Return the kind associated with the given parameter name n.
iterator(ast_vector_tpl const *v, unsigned i)
Definition: z3++.h:1735
symbol name() const
Definition: z3++.h:621
Definition: z3++.h:138
friend expr operator<(expr const &a, expr const &b)
Definition: z3++.h:1425
friend expr operator!(expr const &a)
Return an expression representing not(a).
Definition: z3++.h:1215
solver(context &c, solver const &src, translate)
Definition: z3++.h:2145
Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
solver(context &c)
Definition: z3++.h:2141
expr operator &(expr const &a, expr const &b)
Definition: z3++.h:1469
void Z3_API Z3_apply_result_dec_ref(Z3_context c, Z3_apply_result r)
Decrement the reference counter of the given Z3_apply_result object.
Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re)
Create an universal regular expression of sort re.
void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value)
add a function entry to a function interpretation.
friend expr sum(expr_vector const &args)
Definition: z3++.h:1884
expr lambda(expr const &x, expr const &b)
Definition: z3++.h:1819
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)
Determine if an ast is a universal quantifier.
func_decl(context &c, Z3_func_decl n)
Definition: z3++.h:613
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(Z3_context c, Z3_fixedpoint f)
Retrieve set of background assertions from fixedpoint context.
ast_vector_tpl< ast > ast_vector
Definition: z3++.h:69
Z3_ast Z3_API Z3_mk_int(Z3_context c, int v, Z3_sort ty)
Create a numeral of an int, bit-vector, or finite-domain sort.
T const * ptr() const
Definition: z3++.h:394
handle minimize(expr const &e)
Definition: z3++.h:2619
apply_result apply(goal const &g) const
Definition: z3++.h:2435
friend probe operator<(probe const &p1, probe const &p2)
Definition: z3++.h:2553
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
cube_iterator & operator++()
Definition: z3++.h:2278
void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g)
Increment the reference counter of the given goal.
Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred)
void set(char const *k, double v)
Definition: z3++.h:2159
void add(expr const &e, expr const &p)
Definition: z3++.h:2166
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.
expr store(expr const &a, expr const &i, expr const &v)
Definition: z3++.h:3092
Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c, Z3_fixedpoint d, Z3_ast query)
Pose a query against the asserted rules.
bool has_interp(func_decl f) const
Definition: z3++.h:2074
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
unsigned size() const
Definition: z3++.h:2050
void set(char const *k, unsigned n)
Definition: z3++.h:471
apply_result operator()(goal const &g) const
Definition: z3++.h:2441
friend expr pble(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:1844
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point subtraction.
Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s)
Return the set of non units in the solver state.
Z3_ast m_ast
Definition: z3++.h:484
Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned division.
void set(char const *k, bool b)
Definition: z3++.h:470
unsigned size() const
Definition: z3++.h:1709
unsigned size() const
Definition: z3++.h:391
tactic repeat(tactic const &t, unsigned max=UINT_MAX)
Definition: z3++.h:2469
expr bool_val(bool b)
Definition: z3++.h:2916
~context()
Definition: z3++.h:172
expr operator||(expr const &a, expr const &b)
Definition: z3++.h:1233
uint64_t get_numeral_uint64() const
Return uint64_t value of numeral, throw if result cannot fit in uint64_t.
Definition: z3++.h:837
expr ult(expr const &a, expr const &b)
unsigned less than operator for bitvectors.
Definition: z3++.h:1591
bool is_var() const
Return true if this expression is a variable.
Definition: z3++.h:752
T * operator->() const
Definition: z3++.h:1750
void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p)
Increment the reference counter of the given parameter set.
unsigned depth() const
Definition: z3++.h:2357
Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables.
Z3_string Z3_API Z3_tactic_get_help(Z3_context c, Z3_tactic t)
Return a string containing a description of parameters accepted by the given tactic.
void Z3_API Z3_params_set_symbol(Z3_context c, Z3_params p, Z3_symbol k, Z3_symbol v)
Add a symbol parameter k with value v to the parameter set p.
friend expr pbge(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:1852
expr int_val(int n)
Definition: z3++.h:2918
void Z3_API Z3_global_param_reset_all(void)
Restore the value of all global (and module) parameters. This command will not affect already created...
void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m)
Increment the reference counter of the given model.
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a minimization constraint.
func_decl(func_decl const &s)
Definition: z3++.h:614
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
iterator operator=(iterator const &other)
Definition: z3++.h:1737
Z3_ast Z3_API Z3_mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re)
Check if seq is in the language generated by the regular expression re.
expr mk_or(expr_vector const &args)
Definition: z3++.h:1946
tactic fail_if(probe const &p)
Definition: z3++.h:2707
Z3_param_kind kind(symbol const &s)
Definition: z3++.h:449
stats(context &c, Z3_stats e)
Definition: z3++.h:2102
expr exists(expr const &x, expr const &b)
Definition: z3++.h:1795
std::string to_string()
Definition: z3++.h:2697
ast operator()(context &c, Z3_ast a)
Definition: z3++.h:1669
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
Definition: z3++.h:136
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.
expr_vector parse_string(char const *s)
parsing
Definition: z3++.h:3255
void Z3_API Z3_add_rec_def(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast args[], Z3_ast body)
Define the body of a recursive function.
model get_model() const
Definition: z3++.h:2368
void Z3_API Z3_func_interp_set_else(Z3_context c, Z3_func_interp f, Z3_ast else_value)
Return the 'else' value of the given function interpretation.
friend probe operator &&(probe const &p1, probe const &p2)
Definition: z3++.h:2568
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
context(config &c)
Definition: z3++.h:171
bool is_quantifier() const
Return true if this expression is a quantifier.
Definition: z3++.h:734
Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s)
Return the parameter description set for the given solver object.
unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f)
Return the number of entries in the given function interpretation.
void set(char const *k, symbol const &v)
Definition: z3++.h:2160
expr ite(expr const &c, expr const &t, expr const &e)
Create the if-then-else expression ite(c, t, e)
Definition: z3++.h:1550
double apply(goal const &g) const
Definition: z3++.h:2521
bool Z3_API Z3_goal_is_decided_sat(Z3_context c, Z3_goal g)
Return true if the goal is empty, and it is precise or the product of a under approximation.
func_entry(func_entry const &s)
Definition: z3++.h:1968
Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast t1)
Extract the bits high down to low from a bit-vector of size m to yield a new bit-vector of size n,...
bool is_not() const
Definition: z3++.h:975
expr eval(expr const &n, bool model_completion=false) const
Definition: z3++.h:2036
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3062
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.
Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq)
Create an empty sequence of the sequence sort seq.
~ast()
Definition: z3++.h:489
Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq)
Create a regular expression that accepts the sequence seq.
double Z3_API Z3_stats_get_double_value(Z3_context c, Z3_stats s, unsigned idx)
Return the double value of the given statistical data.
expr_vector unsat_core() const
Definition: z3++.h:2209
int get_numeral_int() const
Return int value of numeral, throw if result cannot fit in machine int.
Definition: z3++.h:784
cube_generator(solver &s)
Definition: z3++.h:2307
void Z3_API Z3_fixedpoint_add_fact(Z3_context c, Z3_fixedpoint d, Z3_func_decl r, unsigned num_args, unsigned args[])
Add a Database fact.
ast & operator=(ast const &s)
Definition: z3++.h:492
func_interp add_func_interp(func_decl &f, expr &else_val)
Definition: z3++.h:2079
expr_vector assertions() const
Definition: z3++.h:2210
unsigned num_args() const
Return the number of arguments in this application. This method assumes the expression is an applicat...
Definition: z3++.h:893
unsigned bv_size() const
Return the size of this Bit-vector sort.
Definition: z3++.h:587
Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned remainder.
Z3_ast_kind kind() const
Definition: z3++.h:493
expr forall(expr const &x, expr const &b)
Definition: z3++.h:1771
void Z3_API Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, bool v)
Add a Boolean parameter k with value v to the parameter set p.
sort(context &c, Z3_sort s)
Definition: z3++.h:517
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point square root.
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
void set_cutoff(unsigned c)
Definition: z3++.h:2323
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, bool const *bits)
create a bit-vector numeral from a vector of Booleans.
Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t)
Create a new solver that is implemented using the given tactic. The solver supports the commands Z3_s...
expr implies(expr const &a, expr const &b)
Definition: z3++.h:1181
Z3_func_entry Z3_API Z3_func_interp_get_entry(Z3_context c, Z3_func_interp f, unsigned i)
Return a "point" of the given function interpretation. It represents the value of f in a particular p...
friend expr sqrt(expr const &a, expr const &rm)
Definition: z3++.h:1529
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1174
Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c, Z3_string name, Z3_string logic, Z3_string status, Z3_string attributes, unsigned num_assumptions, Z3_ast const assumptions[], Z3_ast formula)
Convert the given benchmark into SMT-LIB formatted string.
expr to_expr(context &c, Z3_ast a)
Wraps a Z3_ast as an expr object. It also checks for errors. This function allows the user to use the...
Definition: z3++.h:1563
expr rotate_left(unsigned i)
Definition: z3++.h:1072
expr concat(expr const &a, expr const &b)
Definition: z3++.h:1902
symbol(context &c, Z3_symbol s)
Definition: z3++.h:413
int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the integer value associated with an integer parameter.
stats statistics() const
Definition: z3++.h:2690
solver(context &c, char const *logic)
Definition: z3++.h:2144
tactic try_for(tactic const &t, unsigned ms)
Definition: z3++.h:2480
func_interp(context &c, Z3_func_interp e)
Definition: z3++.h:1990
void register_relation(func_decl &p)
Definition: z3++.h:2691
unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d)
Alias for Z3_get_domain_size.
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.
void add_rule(expr &rule, symbol const &name)
Definition: z3++.h:2671
expr shl(expr const &a, expr const &b)
shift left operator for bitvectors
Definition: z3++.h:1637
params(context &c)
Definition: z3++.h:459
Z3_ast Z3_API Z3_mk_rotate_left(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the left i times.
friend tactic try_for(tactic const &t, unsigned ms)
Definition: z3++.h:2480
void push_back(T const &e)
Definition: z3++.h:1711
expr pble(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:1844
expr max(expr const &a, expr const &b)
Definition: z3++.h:1499
expr sqrt(expr const &a, expr const &rm)
Definition: z3++.h:1529
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:71
Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[])
Create the union of the regular languages.
void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)
Decrement the reference counter of the given probe.
expr uge(expr const &a, expr const &b)
unsigned greater than or equal to operator for bitvectors.
Definition: z3++.h:1597
void push()
Definition: z3++.h:2622
bool is_seq() const
Return true if this sort is a Sequence sort.
Definition: z3++.h:568
void set(char const *param, bool value)
Update global parameter param with Boolean value.
Definition: z3++.h:207
bool is_numeral(std::string &s) const
Definition: z3++.h:720
void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 file with assertions, soft constraints and optimization objectives....
void set(params const &p)
Definition: z3++.h:2156
bool is_double(unsigned i) const
Definition: z3++.h:2116
Z3_ast Z3_API Z3_goal_formula(Z3_context c, Z3_goal g, unsigned idx)
Return a formula from the given goal.
sort & operator=(sort const &s)
Return true if this sort and s are equal.
Definition: z3++.h:524
Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort d)
Return the sort name as a symbol.
func_decl tuple_sort(char const *name, unsigned n, char const *const *names, sort const *sorts, func_decl_vector &projs)
Return a tuple constructor. name is the name of the returned constructor, n are the number of argumen...
Definition: z3++.h:2778
context * m_ctx
Definition: z3++.h:400
unsigned size()
Definition: z3++.h:447
void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p)
Set parameters on fixedpoint context.
bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.
bool is_finite_domain() const
Return true if this is a Finite-domain expression.
Definition: z3++.h:704
expr operator-(expr const &a)
Definition: z3++.h:1358
func_interp get_func_interp(func_decl f) const
Definition: z3++.h:2065
void pop(unsigned n=1)
Definition: z3++.h:2163
friend std::ostream & operator<<(std::ostream &out, stats const &s)
Definition: z3++.h:2121
expr smod(expr const &a, expr const &b)
signed modulus operator for bitvectors
Definition: z3++.h:1623
Z3_ast Z3_API Z3_mk_fpa_numeral_float(Z3_context c, float v, Z3_sort ty)
Create a numeral of FloatingPoint sort from a float.
expr to_real(expr const &a)
Definition: z3++.h:3032
std::string dimacs() const
Definition: z3++.h:2386
cube_iterator end()
Definition: z3++.h:2322
handle(unsigned h)
Definition: z3++.h:2585
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
friend expr implies(expr const &a, expr const &b)
Definition: z3++.h:1181
void Z3_API Z3_fixedpoint_register_relation(Z3_context c, Z3_fixedpoint d, Z3_func_decl f)
Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics...
param_descrs get_param_descrs()
Definition: z3++.h:2236
Definition: z3++.h:135
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:715
Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a)
Create a unit sequence of a.
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.
void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a)
Increment the reference counter of the given AST. The context c should have been created using Z3_mk_...
bool is_const() const
Definition: z3++.h:624
bool is_seq() const
Return true if this is a sequence expression.
Definition: z3++.h:690
ast(ast const &s)
Definition: z3++.h:488
sort enumeration_sort(char const *name, unsigned n, char const *const *enum_names, func_decl_vector &cs, func_decl_vector &ts)
Return an enumeration sort: enum_names[0], ..., enum_names[n-1]. cs and ts are output parameters....
Definition: z3++.h:2767
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.
Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2)
Minimum of floating-point numbers.
tactic par_or(unsigned n, tactic const *tactics)
Definition: z3++.h:2485
void Z3_API Z3_func_entry_dec_ref(Z3_context c, Z3_func_entry e)
Decrement the reference counter of the given Z3_func_entry object.
Z3_ast_vector Z3_API Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o)
Retrieve the unsat core for the last Z3_optimize_check The unsat core is a subset of the assumptions ...
sort(sort const &s)
Definition: z3++.h:519
bool is_finite_domain() const
Return true if this sort is a Finite domain sort.
Definition: z3++.h:576
void pop()
Definition: z3++.h:2703
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:982
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a maximization constraint.
Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i)
Array read. The argument a is the array and i is the index of the array that gets read.
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than or equal.
apply_result(context &c, Z3_apply_result s)
Definition: z3++.h:2398
expr nand(expr const &a, expr const &b)
Definition: z3++.h:1481
unsigned Z3_API Z3_apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r)
Return the number of subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort seq)
Create a regular expression sort out of a sequence sort.
Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d)
Retrieve a formula that encodes satisfying answers to the query.
Z3_string Z3_API Z3_fixedpoint_to_string(Z3_context c, Z3_fixedpoint f, unsigned num_queries, Z3_ast queries[])
Print the current rules and background axioms as a string.
Z3_lbool Z3_API Z3_fixedpoint_query_relations(Z3_context c, Z3_fixedpoint d, unsigned num_relations, Z3_func_decl const relations[])
Pose multiple queries against the asserted rules.
expr operator/(expr const &a, expr const &b)
Definition: z3++.h:1336
Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than.
Function declaration (aka function definition). It is the signature of interpreted and uninterpreted ...
Definition: z3++.h:610
expr set_union(expr const &a, expr const &b)
Definition: z3++.h:3149
Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a)
Return the denominator (as a numeral AST) of a numeral AST of sort Real.
T & operator[](int i)
Definition: z3++.h:392
bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t)
Return true if the given expression t is well sorted.
param_descrs get_param_descrs()
Definition: z3++.h:2452
Z3_probe Z3_API Z3_probe_or(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when p1 or p2 evaluates to true.
goal(goal const &s)
Definition: z3++.h:2341
sort int_sort()
Return the integer sort.
Definition: z3++.h:2729
expr set_del(expr const &s, expr const &e)
Definition: z3++.h:3145
bool is_xor() const
Definition: z3++.h:978
void set(params const &p)
Definition: z3++.h:2642
check_result check(expr_vector const &asms)
Definition: z3++.h:2629
void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g)
Decrement the reference counter of the given tactic.
stats & operator=(stats const &s)
Definition: z3++.h:2106
Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c, Z3_symbol name, unsigned n, Z3_symbol const enum_names[], Z3_func_decl enum_consts[], Z3_func_decl enum_testers[])
Create a enumeration sort.
func_decl & operator=(func_decl const &s)
Definition: z3++.h:616
apply_result & operator=(apply_result const &s)
Definition: z3++.h:2402
Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s)
Integer to string conversion.
expr atmost(expr_vector const &es, unsigned bound)
Definition: z3++.h:1868
void Z3_API Z3_ast_vector_push(Z3_context c, Z3_ast_vector v, Z3_ast a)
Add the AST a in the end of the AST vector v. The size of v is increased by one.
Z3_func_decl Z3_API Z3_mk_rec_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a recursive function.
bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a)
Determine if ast is a lambda expression.
sort to_sort(context &c, Z3_sort s)
Definition: z3++.h:1572
context()
Definition: z3++.h:170
void Z3_API Z3_param_descrs_dec_ref(Z3_context c, Z3_param_descrs p)
Decrement the reference counter of the given parameter description set.
bool is_int() const
Return true if this is an integer expression.
Definition: z3++.h:662
void add(expr const &f)
Definition: z3++.h:2351
Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than.
friend expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3244
expr to_re(expr const &s)
Definition: z3++.h:3208
bool is_false() const
Definition: z3++.h:974
void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives....
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)
Check if container contains containee.
unsigned num_funcs() const
Definition: z3++.h:2047
check_result
Definition: z3++.h:129
Z3_ast Z3_API Z3_mk_zero_ext(Z3_context c, unsigned i, Z3_ast t1)
Extend the given bit-vector with zeros to the (unsigned) equivalent bit-vector of size m+i,...
Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m)
Convert the given model into a string.
param_descrs get_param_descrs()
Definition: z3++.h:2696
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition: z3_api.h:82
Z3_ast Z3_API Z3_mk_select_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const *idxs)
n-ary Array read. The argument a is the array and idxs are the indices of the array that gets read.
apply_result(apply_result const &s)
Definition: z3++.h:2399