Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
z3++.h
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4  Thin C++ layer on top of the Z3 C API.
5  Main features:
6  - Smart pointers for all Z3 objects.
7  - Object-Oriented interface.
8  - Operator overloading.
9  - Exceptions for signaling Z3 errors
10 
11  The C API can be used simultaneously with the C++ layer.
12  However, if you use the C API directly, you will have to check the error conditions manually.
13  Of course, you can invoke the method check_error() of the context object.
14 Author:
15 
16  Leonardo (leonardo) 2012-03-28
17 
18 Notes:
19 
20 --*/
21 #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(char const* s, unsigned n);
362  expr string_val(std::string const& s);
363 
364  expr num_val(int n, sort const & s);
365 
369  expr_vector parse_string(char const* s);
370  expr_vector parse_file(char const* file);
371 
372  expr_vector parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
373  expr_vector parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
374 
375 
376  };
377 
378 
379 
380 
381  template<typename T>
382  class array {
383  T * m_array;
384  unsigned m_size;
385  array(array const & s);
386  array & operator=(array const & s);
387  public:
388  array(unsigned sz):m_size(sz) { m_array = new T[sz]; }
389  template<typename T2>
390  array(ast_vector_tpl<T2> const & v);
391  ~array() { delete[] m_array; }
392  void resize(unsigned sz) { delete[] m_array; m_size = sz; m_array = new T[sz]; }
393  unsigned size() const { return m_size; }
394  T & operator[](int i) { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
395  T const & operator[](int i) const { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
396  T const * ptr() const { return m_array; }
397  T * ptr() { return m_array; }
398  };
399 
400  class object {
401  protected:
403  public:
404  object(context & c):m_ctx(&c) {}
405  object(object const & s):m_ctx(s.m_ctx) {}
406  context & ctx() const { return *m_ctx; }
407  Z3_error_code check_error() const { return m_ctx->check_error(); }
408  friend void check_context(object const & a, object const & b);
409  };
410  inline void check_context(object const & a, object const & b) { (void)a; (void)b; assert(a.m_ctx == b.m_ctx); }
411 
412  class symbol : public object {
413  Z3_symbol m_sym;
414  public:
415  symbol(context & c, Z3_symbol s):object(c), m_sym(s) {}
416  symbol(symbol const & s):object(s), m_sym(s.m_sym) {}
417  symbol & operator=(symbol const & s) { m_ctx = s.m_ctx; m_sym = s.m_sym; return *this; }
418  operator Z3_symbol() const { return m_sym; }
419  Z3_symbol_kind kind() const { return Z3_get_symbol_kind(ctx(), m_sym); }
420  std::string str() const { assert(kind() == Z3_STRING_SYMBOL); return Z3_get_symbol_string(ctx(), m_sym); }
421  int to_int() const { assert(kind() == Z3_INT_SYMBOL); return Z3_get_symbol_int(ctx(), m_sym); }
422  friend std::ostream & operator<<(std::ostream & out, symbol const & s);
423  };
424 
425  inline std::ostream & operator<<(std::ostream & out, symbol const & s) {
426  if (s.kind() == Z3_INT_SYMBOL)
427  out << "k!" << s.to_int();
428  else
429  out << s.str().c_str();
430  return out;
431  }
432 
433 
434  class param_descrs : public object {
435  Z3_param_descrs m_descrs;
436  public:
437  param_descrs(context& c, Z3_param_descrs d): object(c), m_descrs(d) { Z3_param_descrs_inc_ref(c, d); }
438  param_descrs(param_descrs const& o): object(o.ctx()), m_descrs(o.m_descrs) { Z3_param_descrs_inc_ref(ctx(), m_descrs); }
440  Z3_param_descrs_inc_ref(o.ctx(), o.m_descrs);
441  Z3_param_descrs_dec_ref(ctx(), m_descrs);
442  m_descrs = o.m_descrs;
443  m_ctx = o.m_ctx;
444  return *this;
445  }
448 
449  unsigned size() { return Z3_param_descrs_size(ctx(), m_descrs); }
450  symbol name(unsigned i) { return symbol(ctx(), Z3_param_descrs_get_name(ctx(), m_descrs, i)); }
451  Z3_param_kind kind(symbol const& s) { return Z3_param_descrs_get_kind(ctx(), m_descrs, s); }
452  std::string documentation(symbol const& s) { char const* r = Z3_param_descrs_get_documentation(ctx(), m_descrs, s); check_error(); return r; }
453  std::string to_string() const { return Z3_param_descrs_to_string(ctx(), m_descrs); }
454  };
455 
456  inline std::ostream& operator<<(std::ostream & out, param_descrs const & d) { return out << d.to_string(); }
457 
458  class params : public object {
459  Z3_params m_params;
460  public:
461  params(context & c):object(c) { m_params = Z3_mk_params(c); Z3_params_inc_ref(ctx(), m_params); }
462  params(params const & s):object(s), m_params(s.m_params) { Z3_params_inc_ref(ctx(), m_params); }
463  ~params() { Z3_params_dec_ref(ctx(), m_params); }
464  operator Z3_params() const { return m_params; }
465  params & operator=(params const & s) {
466  Z3_params_inc_ref(s.ctx(), s.m_params);
467  Z3_params_dec_ref(ctx(), m_params);
468  m_ctx = s.m_ctx;
469  m_params = s.m_params;
470  return *this;
471  }
472  void set(char const * k, bool b) { Z3_params_set_bool(ctx(), m_params, ctx().str_symbol(k), b); }
473  void set(char const * k, unsigned n) { Z3_params_set_uint(ctx(), m_params, ctx().str_symbol(k), n); }
474  void set(char const * k, double n) { Z3_params_set_double(ctx(), m_params, ctx().str_symbol(k), n); }
475  void set(char const * k, symbol const & s) { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), s); }
476  void set(char const * k, char const* s) { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), ctx().str_symbol(s)); }
477  friend std::ostream & operator<<(std::ostream & out, params const & p);
478  };
479 
480  inline std::ostream & operator<<(std::ostream & out, params const & p) {
481  out << Z3_params_to_string(p.ctx(), p); return out;
482  }
483 
484  class ast : public object {
485  protected:
486  Z3_ast m_ast;
487  public:
488  ast(context & c):object(c), m_ast(0) {}
489  ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
490  ast(ast const & s):object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
491  ~ast() { if (m_ast) Z3_dec_ref(*m_ctx, m_ast); }
492  operator Z3_ast() const { return m_ast; }
493  operator bool() const { return m_ast != 0; }
494  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; }
495  Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }
496  unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }
497  friend std::ostream & operator<<(std::ostream & out, ast const & n);
498  std::string to_string() const { return std::string(Z3_ast_to_string(ctx(), m_ast)); }
499 
500 
504  friend bool eq(ast const & a, ast const & b);
505  };
506  inline std::ostream & operator<<(std::ostream & out, ast const & n) {
507  out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
508  }
509 
510  inline bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b); }
511 
512 
516  class sort : public ast {
517  public:
518  sort(context & c):ast(c) {}
519  sort(context & c, Z3_sort s):ast(c, reinterpret_cast<Z3_ast>(s)) {}
520  sort(context & c, Z3_ast a):ast(c, a) {}
521  sort(sort const & s):ast(s) {}
522  operator Z3_sort() const { return reinterpret_cast<Z3_sort>(m_ast); }
523 
527  unsigned id() const { unsigned r = Z3_get_sort_id(ctx(), *this); check_error(); return r; }
528 
532  sort & operator=(sort const & s) { return static_cast<sort&>(ast::operator=(s)); }
536  Z3_sort_kind sort_kind() const { return Z3_get_sort_kind(*m_ctx, *this); }
540  symbol name() const { Z3_symbol s = Z3_get_sort_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
544  bool is_bool() const { return sort_kind() == Z3_BOOL_SORT; }
548  bool is_int() const { return sort_kind() == Z3_INT_SORT; }
552  bool is_real() const { return sort_kind() == Z3_REAL_SORT; }
556  bool is_arith() const { return is_int() || is_real(); }
560  bool is_bv() const { return sort_kind() == Z3_BV_SORT; }
564  bool is_array() const { return sort_kind() == Z3_ARRAY_SORT; }
568  bool is_datatype() const { return sort_kind() == Z3_DATATYPE_SORT; }
572  bool is_relation() const { return sort_kind() == Z3_RELATION_SORT; }
576  bool is_seq() const { return sort_kind() == Z3_SEQ_SORT; }
580  bool is_re() const { return sort_kind() == Z3_RE_SORT; }
584  bool is_finite_domain() const { return sort_kind() == Z3_FINITE_DOMAIN_SORT; }
588  bool is_fpa() const { return sort_kind() == Z3_FLOATING_POINT_SORT; }
589 
595  unsigned bv_size() const { assert(is_bv()); unsigned r = Z3_get_bv_sort_size(ctx(), *this); check_error(); return r; }
596 
597  unsigned fpa_ebits() const { assert(is_fpa()); unsigned r = Z3_fpa_get_ebits(ctx(), *this); check_error(); return r; }
598 
599  unsigned fpa_sbits() const { assert(is_fpa()); unsigned r = Z3_fpa_get_sbits(ctx(), *this); check_error(); return r; }
605  sort array_domain() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_domain(ctx(), *this); check_error(); return sort(ctx(), s); }
611  sort array_range() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_range(ctx(), *this); check_error(); return sort(ctx(), s); }
612  };
613 
618  class func_decl : public ast {
619  public:
620  func_decl(context & c):ast(c) {}
621  func_decl(context & c, Z3_func_decl n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
622  func_decl(func_decl const & s):ast(s) {}
623  operator Z3_func_decl() const { return reinterpret_cast<Z3_func_decl>(m_ast); }
624  func_decl & operator=(func_decl const & s) { return static_cast<func_decl&>(ast::operator=(s)); }
625 
629  unsigned id() const { unsigned r = Z3_get_func_decl_id(ctx(), *this); check_error(); return r; }
630 
631  unsigned arity() const { return Z3_get_arity(ctx(), *this); }
632  sort domain(unsigned i) const { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }
633  sort range() const { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }
634  symbol name() const { Z3_symbol s = Z3_get_decl_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
635  Z3_decl_kind decl_kind() const { return Z3_get_decl_kind(ctx(), *this); }
636 
638  Z3_func_decl tc = Z3_mk_transitive_closure(ctx(), *this); check_error(); return func_decl(ctx(), tc);
639  }
640 
641  bool is_const() const { return arity() == 0; }
642 
643  expr operator()() const;
644  expr operator()(unsigned n, expr const * args) const;
645  expr operator()(expr_vector const& v) const;
646  expr operator()(expr const & a) const;
647  expr operator()(int a) const;
648  expr operator()(expr const & a1, expr const & a2) const;
649  expr operator()(expr const & a1, int a2) const;
650  expr operator()(int a1, expr const & a2) const;
651  expr operator()(expr const & a1, expr const & a2, expr const & a3) const;
652  expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const;
653  expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const;
654  };
655 
659  expr select(expr const & a, expr const& i);
660  expr select(expr const & a, expr_vector const & i);
661 
667  class expr : public ast {
668  public:
669  expr(context & c):ast(c) {}
670  expr(context & c, Z3_ast n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
671  expr(expr const & n):ast(n) {}
672  expr & operator=(expr const & n) { return static_cast<expr&>(ast::operator=(n)); }
673 
677  sort get_sort() const { Z3_sort s = Z3_get_sort(*m_ctx, m_ast); check_error(); return sort(*m_ctx, s); }
678 
682  bool is_bool() const { return get_sort().is_bool(); }
686  bool is_int() const { return get_sort().is_int(); }
690  bool is_real() const { return get_sort().is_real(); }
694  bool is_arith() const { return get_sort().is_arith(); }
698  bool is_bv() const { return get_sort().is_bv(); }
702  bool is_array() const { return get_sort().is_array(); }
706  bool is_datatype() const { return get_sort().is_datatype(); }
710  bool is_relation() const { return get_sort().is_relation(); }
714  bool is_seq() const { return get_sort().is_seq(); }
718  bool is_re() const { return get_sort().is_re(); }
719 
728  bool is_finite_domain() const { return get_sort().is_finite_domain(); }
732  bool is_fpa() const { return get_sort().is_fpa(); }
733 
739  bool is_numeral() const { return kind() == Z3_NUMERAL_AST; }
740  bool is_numeral_i64(int64_t& i) const { bool r = Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}
741  bool is_numeral_u64(uint64_t& i) const { bool r = Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}
742  bool is_numeral_i(int& i) const { bool r = Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}
743  bool is_numeral_u(unsigned& i) const { bool r = Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
744  bool is_numeral(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; }
745  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; }
746  bool is_numeral(double& d) const { if (!is_numeral()) return false; d = Z3_get_numeral_double(ctx(), m_ast); check_error(); return true; }
750  bool is_app() const { return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
754  bool is_const() const { return is_app() && num_args() == 0; }
758  bool is_quantifier() const { return kind() == Z3_QUANTIFIER_AST; }
759 
763  bool is_forall() const { return Z3_is_quantifier_forall(ctx(), m_ast); }
767  bool is_exists() const { return Z3_is_quantifier_exists(ctx(), m_ast); }
771  bool is_lambda() const { return Z3_is_lambda(ctx(), m_ast); }
776  bool is_var() const { return kind() == Z3_VAR_AST; }
780  bool is_algebraic() const { return Z3_is_algebraic_number(ctx(), m_ast); }
781 
785  bool is_well_sorted() const { bool r = Z3_is_well_sorted(ctx(), m_ast); check_error(); return r; }
786 
793  std::string get_decimal_string(int precision) const {
794  assert(is_numeral() || is_algebraic());
795  return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
796  }
797 
798 
802  unsigned id() const { unsigned r = Z3_get_ast_id(ctx(), m_ast); check_error(); return r; }
803 
814  int get_numeral_int() const {
815  int result = 0;
816  if (!is_numeral_i(result)) {
817  assert(ctx().enable_exceptions());
818  if (!ctx().enable_exceptions()) return 0;
819  Z3_THROW(exception("numeral does not fit in machine int"));
820  }
821  return result;
822  }
823 
833  unsigned get_numeral_uint() const {
834  assert(is_numeral());
835  unsigned result = 0;
836  if (!is_numeral_u(result)) {
837  assert(ctx().enable_exceptions());
838  if (!ctx().enable_exceptions()) return 0;
839  Z3_THROW(exception("numeral does not fit in machine uint"));
840  }
841  return result;
842  }
843 
850  int64_t get_numeral_int64() const {
851  assert(is_numeral());
852  int64_t result = 0;
853  if (!is_numeral_i64(result)) {
854  assert(ctx().enable_exceptions());
855  if (!ctx().enable_exceptions()) return 0;
856  Z3_THROW(exception("numeral does not fit in machine int64_t"));
857  }
858  return result;
859  }
860 
867  uint64_t get_numeral_uint64() const {
868  assert(is_numeral());
869  uint64_t result = 0;
870  if (!is_numeral_u64(result)) {
871  assert(ctx().enable_exceptions());
872  if (!ctx().enable_exceptions()) return 0;
873  Z3_THROW(exception("numeral does not fit in machine uint64_t"));
874  }
875  return result;
876  }
877 
879  return Z3_get_bool_value(ctx(), m_ast);
880  }
881 
882  expr numerator() const {
883  assert(is_numeral());
884  Z3_ast r = Z3_get_numerator(ctx(), m_ast);
885  check_error();
886  return expr(ctx(),r);
887  }
888 
889 
890  expr denominator() const {
891  assert(is_numeral());
892  Z3_ast r = Z3_get_denominator(ctx(), m_ast);
893  check_error();
894  return expr(ctx(),r);
895  }
896 
902  std::string get_escaped_string() const {
903  char const* s = Z3_get_string(ctx(), m_ast);
904  check_error();
905  return std::string(s);
906  }
907 
908  std::string get_string() const {
909  unsigned n;
910  char const* s = Z3_get_lstring(ctx(), m_ast, &n);
911  check_error();
912  return std::string(s, n);
913  }
914 
915  operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
916 
921  assert(is_fpa());
922  Z3_sort s = ctx().fpa_rounding_mode();
923  check_error();
924  return sort(ctx(), s);
925  }
926 
927 
934  func_decl decl() const { Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }
941  unsigned num_args() const { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
949  expr arg(unsigned i) const { Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }
950 
956  expr body() const { assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
957 
963  friend expr operator!(expr const & a);
964 
971  friend expr operator&&(expr const & a, expr const & b);
972 
973 
980  friend expr operator&&(expr const & a, bool b);
987  friend expr operator&&(bool a, expr const & b);
988 
995  friend expr operator||(expr const & a, expr const & b);
1002  friend expr operator||(expr const & a, bool b);
1003 
1010  friend expr operator||(bool a, expr const & b);
1011 
1012  friend expr implies(expr const & a, expr const & b);
1013  friend expr implies(expr const & a, bool b);
1014  friend expr implies(bool a, expr const & b);
1015 
1016  friend expr mk_or(expr_vector const& args);
1017  friend expr mk_and(expr_vector const& args);
1018 
1019  friend expr ite(expr const & c, expr const & t, expr const & e);
1020 
1021  bool is_true() const { return is_app() && Z3_OP_TRUE == decl().decl_kind(); }
1022  bool is_false() const { return is_app() && Z3_OP_FALSE == decl().decl_kind(); }
1023  bool is_not() const { return is_app() && Z3_OP_NOT == decl().decl_kind(); }
1024  bool is_and() const { return is_app() && Z3_OP_AND == decl().decl_kind(); }
1025  bool is_or() const { return is_app() && Z3_OP_OR == decl().decl_kind(); }
1026  bool is_xor() const { return is_app() && Z3_OP_XOR == decl().decl_kind(); }
1027  bool is_implies() const { return is_app() && Z3_OP_IMPLIES == decl().decl_kind(); }
1028  bool is_eq() const { return is_app() && Z3_OP_EQ == decl().decl_kind(); }
1029  bool is_ite() const { return is_app() && Z3_OP_ITE == decl().decl_kind(); }
1030  bool is_distinct() const { return is_app() && Z3_OP_DISTINCT == decl().decl_kind(); }
1031 
1032  friend expr distinct(expr_vector const& args);
1033  friend expr concat(expr const& a, expr const& b);
1034  friend expr concat(expr_vector const& args);
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  friend expr sum(expr_vector const& args);
1048 
1049  friend expr operator*(expr const & a, expr const & b);
1050  friend expr operator*(expr const & a, int b);
1051  friend expr operator*(int a, expr const & b);
1052 
1053  /* \brief Power operator */
1054  friend expr pw(expr const & a, expr const & b);
1055  friend expr pw(expr const & a, int b);
1056  friend expr pw(int a, expr const & b);
1057 
1058  /* \brief mod operator */
1059  friend expr mod(expr const& a, expr const& b);
1060  friend expr mod(expr const& a, int b);
1061  friend expr mod(int a, expr const& b);
1062 
1063  /* \brief rem operator */
1064  friend expr rem(expr const& a, expr const& b);
1065  friend expr rem(expr const& a, int b);
1066  friend expr rem(int a, expr const& b);
1067 
1068  friend expr is_int(expr const& e);
1069 
1070  friend expr operator/(expr const & a, expr const & b);
1071  friend expr operator/(expr const & a, int b);
1072  friend expr operator/(int a, expr const & b);
1073 
1074  friend expr operator-(expr const & a);
1075 
1076  friend expr operator-(expr const & a, expr const & b);
1077  friend expr operator-(expr const & a, int b);
1078  friend expr operator-(int a, expr const & b);
1079 
1080  friend expr operator<=(expr const & a, expr const & b);
1081  friend expr operator<=(expr const & a, int b);
1082  friend expr operator<=(int a, expr const & b);
1083 
1084 
1085  friend expr operator>=(expr const & a, expr const & b);
1086  friend expr operator>=(expr const & a, int b);
1087  friend expr operator>=(int a, expr const & b);
1088 
1089  friend expr operator<(expr const & a, expr const & b);
1090  friend expr operator<(expr const & a, int b);
1091  friend expr operator<(int a, expr const & b);
1092 
1093  friend expr operator>(expr const & a, expr const & b);
1094  friend expr operator>(expr const & a, int b);
1095  friend expr operator>(int a, expr const & b);
1096 
1097  friend expr pble(expr_vector const& es, int const * coeffs, int bound);
1098  friend expr pbge(expr_vector const& es, int const * coeffs, int bound);
1099  friend expr pbeq(expr_vector const& es, int const * coeffs, int bound);
1100  friend expr atmost(expr_vector const& es, unsigned bound);
1101  friend expr atleast(expr_vector const& es, unsigned bound);
1102 
1103  friend expr operator&(expr const & a, expr const & b);
1104  friend expr operator&(expr const & a, int b);
1105  friend expr operator&(int a, expr const & b);
1106 
1107  friend expr operator^(expr const & a, expr const & b);
1108  friend expr operator^(expr const & a, int b);
1109  friend expr operator^(int a, expr const & b);
1110 
1111  friend expr operator|(expr const & a, expr const & b);
1112  friend expr operator|(expr const & a, int b);
1113  friend expr operator|(int a, expr const & b);
1114  friend expr nand(expr const& a, expr const& b);
1115  friend expr nor(expr const& a, expr const& b);
1116  friend expr xnor(expr const& a, expr const& b);
1117 
1118  friend expr min(expr const& a, expr const& b);
1119  friend expr max(expr const& a, expr const& b);
1120 
1121  friend expr bv2int(expr const& a, bool is_signed);
1122  friend expr int2bv(unsigned n, expr const& a);
1123  friend expr bvadd_no_overflow(expr const& a, expr const& b, bool is_signed);
1124  friend expr bvadd_no_underflow(expr const& a, expr const& b);
1125  friend expr bvsub_no_overflow(expr const& a, expr const& b);
1126  friend expr bvsub_no_underflow(expr const& a, expr const& b, bool is_signed);
1127  friend expr bvsdiv_no_overflow(expr const& a, expr const& b);
1128  friend expr bvneg_no_overflow(expr const& a);
1129  friend expr bvmul_no_overflow(expr const& a, expr const& b, bool is_signed);
1130  friend expr bvmul_no_underflow(expr const& a, expr const& b);
1131 
1132  expr rotate_left(unsigned i) { Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
1133  expr rotate_right(unsigned i) { Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
1134  expr repeat(unsigned i) { Z3_ast r = Z3_mk_repeat(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
1135 
1136  friend expr abs(expr const & a);
1137  friend expr sqrt(expr const & a, expr const & rm);
1138 
1139  friend expr operator~(expr const & a);
1140  expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }
1141  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)); }
1142  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)); }
1143 
1147  friend expr fma(expr const& a, expr const& b, expr const& c);
1148 
1154  expr extract(expr const& offset, expr const& length) const {
1155  check_context(*this, offset); check_context(offset, length);
1156  Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
1157  }
1158  expr replace(expr const& src, expr const& dst) const {
1159  check_context(*this, src); check_context(src, dst);
1160  Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
1161  check_error();
1162  return expr(ctx(), r);
1163  }
1164  expr unit() const {
1165  Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
1166  check_error();
1167  return expr(ctx(), r);
1168  }
1169  expr contains(expr const& s) {
1170  check_context(*this, s);
1171  Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
1172  check_error();
1173  return expr(ctx(), r);
1174  }
1175  expr at(expr const& index) const {
1176  check_context(*this, index);
1177  Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
1178  check_error();
1179  return expr(ctx(), r);
1180  }
1181  expr nth(expr const& index) const {
1182  check_context(*this, index);
1183  Z3_ast r = Z3_mk_seq_nth(ctx(), *this, index);
1184  check_error();
1185  return expr(ctx(), r);
1186  }
1187  expr length() const {
1188  Z3_ast r = Z3_mk_seq_length(ctx(), *this);
1189  check_error();
1190  return expr(ctx(), r);
1191  }
1192  expr stoi() const {
1193  Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
1194  check_error();
1195  return expr(ctx(), r);
1196  }
1197  expr itos() const {
1198  Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
1199  check_error();
1200  return expr(ctx(), r);
1201  }
1202 
1203  friend expr range(expr const& lo, expr const& hi);
1207  expr loop(unsigned lo) {
1208  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0);
1209  check_error();
1210  return expr(ctx(), r);
1211  }
1212  expr loop(unsigned lo, unsigned hi) {
1213  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi);
1214  check_error();
1215  return expr(ctx(), r);
1216  }
1217 
1221  expr operator[](expr const& index) const {
1222  assert(is_array() || is_seq());
1223  if (is_array()) {
1224  return select(*this, index);
1225  }
1226  return nth(index);
1227  }
1228 
1229  expr operator[](expr_vector const& index) const {
1230  return select(*this, index);
1231  }
1232 
1236  expr simplify() const { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
1240  expr simplify(params const & p) const { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
1241 
1245  expr substitute(expr_vector const& src, expr_vector const& dst);
1246 
1250  expr substitute(expr_vector const& dst);
1251 
1252  };
1253 
1254 #define _Z3_MK_BIN_(a, b, binop) \
1255  check_context(a, b); \
1256  Z3_ast r = binop(a.ctx(), a, b); \
1257  a.check_error(); \
1258  return expr(a.ctx(), r); \
1259 
1260 
1261  inline expr implies(expr const & a, expr const & b) {
1262  assert(a.is_bool() && b.is_bool());
1263  _Z3_MK_BIN_(a, b, Z3_mk_implies);
1264  }
1265  inline expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); }
1266  inline expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); }
1267 
1268 
1269  inline expr pw(expr const & a, expr const & b) { _Z3_MK_BIN_(a, b, Z3_mk_power); }
1270  inline expr pw(expr const & a, int b) { return pw(a, a.ctx().num_val(b, a.get_sort())); }
1271  inline expr pw(int a, expr const & b) { return pw(b.ctx().num_val(a, b.get_sort()), b); }
1272 
1273  inline expr mod(expr const& a, expr const& b) {
1274  if (a.is_bv()) {
1275  _Z3_MK_BIN_(a, b, Z3_mk_bvsmod);
1276  }
1277  else {
1278  _Z3_MK_BIN_(a, b, Z3_mk_mod);
1279  }
1280  }
1281  inline expr mod(expr const & a, int b) { return mod(a, a.ctx().num_val(b, a.get_sort())); }
1282  inline expr mod(int a, expr const & b) { return mod(b.ctx().num_val(a, b.get_sort()), b); }
1283 
1284  inline expr operator%(expr const& a, expr const& b) { return mod(a, b); }
1285  inline expr operator%(expr const& a, int b) { return mod(a, b); }
1286  inline expr operator%(int a, expr const& b) { return mod(a, b); }
1287 
1288 
1289  inline expr rem(expr const& a, expr const& b) {
1290  if (a.is_fpa() && b.is_fpa()) {
1291  _Z3_MK_BIN_(a, b, Z3_mk_fpa_rem);
1292  } else {
1293  _Z3_MK_BIN_(a, b, Z3_mk_rem);
1294  }
1295  }
1296  inline expr rem(expr const & a, int b) { return rem(a, a.ctx().num_val(b, a.get_sort())); }
1297  inline expr rem(int a, expr const & b) { return rem(b.ctx().num_val(a, b.get_sort()), b); }
1298 
1299 #undef _Z3_MK_BIN_
1300 
1301 #define _Z3_MK_UN_(a, mkun) \
1302  Z3_ast r = mkun(a.ctx(), a); \
1303  a.check_error(); \
1304  return expr(a.ctx(), r); \
1305 
1306 
1307  inline expr operator!(expr const & a) { assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); }
1308 
1309  inline expr is_int(expr const& e) { _Z3_MK_UN_(e, Z3_mk_is_int); }
1310 
1311 #undef _Z3_MK_UN_
1312 
1313  inline expr operator&&(expr const & a, expr const & b) {
1314  check_context(a, b);
1315  assert(a.is_bool() && b.is_bool());
1316  Z3_ast args[2] = { a, b };
1317  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1318  a.check_error();
1319  return expr(a.ctx(), r);
1320  }
1321 
1322  inline expr operator&&(expr const & a, bool b) { return a && a.ctx().bool_val(b); }
1323  inline expr operator&&(bool a, expr const & b) { return b.ctx().bool_val(a) && b; }
1324 
1325  inline expr operator||(expr const & a, expr const & b) {
1326  check_context(a, b);
1327  assert(a.is_bool() && b.is_bool());
1328  Z3_ast args[2] = { a, b };
1329  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1330  a.check_error();
1331  return expr(a.ctx(), r);
1332  }
1333 
1334  inline expr operator||(expr const & a, bool b) { return a || a.ctx().bool_val(b); }
1335 
1336  inline expr operator||(bool a, expr const & b) { return b.ctx().bool_val(a) || b; }
1337 
1338  inline expr operator==(expr const & a, expr const & b) {
1339  check_context(a, b);
1340  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1341  a.check_error();
1342  return expr(a.ctx(), r);
1343  }
1344  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()); }
1345  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; }
1346 
1347  inline expr operator!=(expr const & a, expr const & b) {
1348  check_context(a, b);
1349  Z3_ast args[2] = { a, b };
1350  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1351  a.check_error();
1352  return expr(a.ctx(), r);
1353  }
1354  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()); }
1355  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; }
1356 
1357  inline expr operator+(expr const & a, expr const & b) {
1358  check_context(a, b);
1359  Z3_ast r = 0;
1360  if (a.is_arith() && b.is_arith()) {
1361  Z3_ast args[2] = { a, b };
1362  r = Z3_mk_add(a.ctx(), 2, args);
1363  }
1364  else if (a.is_bv() && b.is_bv()) {
1365  r = Z3_mk_bvadd(a.ctx(), a, b);
1366  }
1367  else if (a.is_seq() && b.is_seq()) {
1368  return concat(a, b);
1369  }
1370  else if (a.is_re() && b.is_re()) {
1371  Z3_ast _args[2] = { a, b };
1372  r = Z3_mk_re_union(a.ctx(), 2, _args);
1373  }
1374  else if (a.is_fpa() && b.is_fpa()) {
1375  r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1376  }
1377  else {
1378  // operator is not supported by given arguments.
1379  assert(false);
1380  }
1381  a.check_error();
1382  return expr(a.ctx(), r);
1383  }
1384  inline expr operator+(expr const & a, int b) { return a + a.ctx().num_val(b, a.get_sort()); }
1385  inline expr operator+(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) + b; }
1386 
1387  inline expr operator*(expr const & a, expr const & b) {
1388  check_context(a, b);
1389  Z3_ast r = 0;
1390  if (a.is_arith() && b.is_arith()) {
1391  Z3_ast args[2] = { a, b };
1392  r = Z3_mk_mul(a.ctx(), 2, args);
1393  }
1394  else if (a.is_bv() && b.is_bv()) {
1395  r = Z3_mk_bvmul(a.ctx(), a, b);
1396  }
1397  else if (a.is_fpa() && b.is_fpa()) {
1398  r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1399  }
1400  else {
1401  // operator is not supported by given arguments.
1402  assert(false);
1403  }
1404  a.check_error();
1405  return expr(a.ctx(), r);
1406  }
1407  inline expr operator*(expr const & a, int b) { return a * a.ctx().num_val(b, a.get_sort()); }
1408  inline expr operator*(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) * b; }
1409 
1410 
1411  inline expr operator>=(expr const & a, expr const & b) {
1412  check_context(a, b);
1413  Z3_ast r = 0;
1414  if (a.is_arith() && b.is_arith()) {
1415  r = Z3_mk_ge(a.ctx(), a, b);
1416  }
1417  else if (a.is_bv() && b.is_bv()) {
1418  r = Z3_mk_bvsge(a.ctx(), a, b);
1419  }
1420  else {
1421  // operator is not supported by given arguments.
1422  assert(false);
1423  }
1424  a.check_error();
1425  return expr(a.ctx(), r);
1426  }
1427 
1428  inline expr operator/(expr const & a, expr const & b) {
1429  check_context(a, b);
1430  Z3_ast r = 0;
1431  if (a.is_arith() && b.is_arith()) {
1432  r = Z3_mk_div(a.ctx(), a, b);
1433  }
1434  else if (a.is_bv() && b.is_bv()) {
1435  r = Z3_mk_bvsdiv(a.ctx(), a, b);
1436  }
1437  else if (a.is_fpa() && b.is_fpa()) {
1438  r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1439  }
1440  else {
1441  // operator is not supported by given arguments.
1442  assert(false);
1443  }
1444  a.check_error();
1445  return expr(a.ctx(), r);
1446  }
1447  inline expr operator/(expr const & a, int b) { return a / a.ctx().num_val(b, a.get_sort()); }
1448  inline expr operator/(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) / b; }
1449 
1450  inline expr operator-(expr const & a) {
1451  Z3_ast r = 0;
1452  if (a.is_arith()) {
1453  r = Z3_mk_unary_minus(a.ctx(), a);
1454  }
1455  else if (a.is_bv()) {
1456  r = Z3_mk_bvneg(a.ctx(), a);
1457  }
1458  else if (a.is_fpa()) {
1459  r = Z3_mk_fpa_neg(a.ctx(), a);
1460  }
1461  else {
1462  // operator is not supported by given arguments.
1463  assert(false);
1464  }
1465  a.check_error();
1466  return expr(a.ctx(), r);
1467  }
1468 
1469  inline expr operator-(expr const & a, expr const & b) {
1470  check_context(a, b);
1471  Z3_ast r = 0;
1472  if (a.is_arith() && b.is_arith()) {
1473  Z3_ast args[2] = { a, b };
1474  r = Z3_mk_sub(a.ctx(), 2, args);
1475  }
1476  else if (a.is_bv() && b.is_bv()) {
1477  r = Z3_mk_bvsub(a.ctx(), a, b);
1478  }
1479  else if (a.is_fpa() && b.is_fpa()) {
1480  r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1481  }
1482  else {
1483  // operator is not supported by given arguments.
1484  assert(false);
1485  }
1486  a.check_error();
1487  return expr(a.ctx(), r);
1488  }
1489  inline expr operator-(expr const & a, int b) { return a - a.ctx().num_val(b, a.get_sort()); }
1490  inline expr operator-(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) - b; }
1491 
1492  inline expr operator<=(expr const & a, expr const & b) {
1493  check_context(a, b);
1494  Z3_ast r = 0;
1495  if (a.is_arith() && b.is_arith()) {
1496  r = Z3_mk_le(a.ctx(), a, b);
1497  }
1498  else if (a.is_bv() && b.is_bv()) {
1499  r = Z3_mk_bvsle(a.ctx(), a, b);
1500  }
1501  else if (a.is_fpa() && b.is_fpa()) {
1502  r = Z3_mk_fpa_leq(a.ctx(), a, b);
1503  }
1504  else {
1505  // operator is not supported by given arguments.
1506  assert(false);
1507  }
1508  a.check_error();
1509  return expr(a.ctx(), r);
1510  }
1511  inline expr operator<=(expr const & a, int b) { return a <= a.ctx().num_val(b, a.get_sort()); }
1512  inline expr operator<=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) <= b; }
1513 
1514  inline expr operator>=(expr const & a, int b) { return a >= a.ctx().num_val(b, a.get_sort()); }
1515  inline expr operator>=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) >= b; }
1516 
1517  inline expr operator<(expr const & a, expr const & b) {
1518  check_context(a, b);
1519  Z3_ast r = 0;
1520  if (a.is_arith() && b.is_arith()) {
1521  r = Z3_mk_lt(a.ctx(), a, b);
1522  }
1523  else if (a.is_bv() && b.is_bv()) {
1524  r = Z3_mk_bvslt(a.ctx(), a, b);
1525  }
1526  else if (a.is_fpa() && b.is_fpa()) {
1527  r = Z3_mk_fpa_lt(a.ctx(), a, b);
1528  }
1529  else {
1530  // operator is not supported by given arguments.
1531  assert(false);
1532  }
1533  a.check_error();
1534  return expr(a.ctx(), r);
1535  }
1536  inline expr operator<(expr const & a, int b) { return a < a.ctx().num_val(b, a.get_sort()); }
1537  inline expr operator<(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) < b; }
1538 
1539  inline expr operator>(expr const & a, expr const & b) {
1540  check_context(a, b);
1541  Z3_ast r = 0;
1542  if (a.is_arith() && b.is_arith()) {
1543  r = Z3_mk_gt(a.ctx(), a, b);
1544  }
1545  else if (a.is_bv() && b.is_bv()) {
1546  r = Z3_mk_bvsgt(a.ctx(), a, b);
1547  }
1548  else if (a.is_fpa() && b.is_fpa()) {
1549  r = Z3_mk_fpa_gt(a.ctx(), a, b);
1550  }
1551  else {
1552  // operator is not supported by given arguments.
1553  assert(false);
1554  }
1555  a.check_error();
1556  return expr(a.ctx(), r);
1557  }
1558  inline expr operator>(expr const & a, int b) { return a > a.ctx().num_val(b, a.get_sort()); }
1559  inline expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > b; }
1560 
1561  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); }
1562  inline expr operator&(expr const & a, int b) { return a & a.ctx().num_val(b, a.get_sort()); }
1563  inline expr operator&(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) & b; }
1564 
1565  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); }
1566  inline expr operator^(expr const & a, int b) { return a ^ a.ctx().num_val(b, a.get_sort()); }
1567  inline expr operator^(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) ^ b; }
1568 
1569  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); }
1570  inline expr operator|(expr const & a, int b) { return a | a.ctx().num_val(b, a.get_sort()); }
1571  inline expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; }
1572 
1573  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); }
1574  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); }
1575  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); }
1576  inline expr min(expr const& a, expr const& b) {
1577  check_context(a, b);
1578  Z3_ast r;
1579  if (a.is_arith()) {
1580  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
1581  }
1582  else if (a.is_bv()) {
1583  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
1584  }
1585  else {
1586  assert(a.is_fpa());
1587  r = Z3_mk_fpa_min(a.ctx(), a, b);
1588  }
1589  return expr(a.ctx(), r);
1590  }
1591  inline expr max(expr const& a, expr const& b) {
1592  check_context(a, b);
1593  Z3_ast r;
1594  if (a.is_arith()) {
1595  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
1596  }
1597  else if (a.is_bv()) {
1598  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
1599  }
1600  else {
1601  assert(a.is_fpa());
1602  r = Z3_mk_fpa_max(a.ctx(), a, b);
1603  }
1604  return expr(a.ctx(), r);
1605  }
1606  inline expr abs(expr const & a) {
1607  Z3_ast r;
1608  if (a.is_int()) {
1609  expr zero = a.ctx().int_val(0);
1610  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1611  }
1612  else if (a.is_real()) {
1613  expr zero = a.ctx().real_val(0);
1614  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1615  }
1616  else {
1617  r = Z3_mk_fpa_abs(a.ctx(), a);
1618  }
1619  a.check_error();
1620  return expr(a.ctx(), r);
1621  }
1622  inline expr sqrt(expr const & a, expr const& rm) {
1623  check_context(a, rm);
1624  assert(a.is_fpa());
1625  Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
1626  a.check_error();
1627  return expr(a.ctx(), r);
1628  }
1629  inline expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
1630 
1631  inline expr fma(expr const& a, expr const& b, expr const& c, expr const& rm) {
1632  check_context(a, b); check_context(a, c); check_context(a, rm);
1633  assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
1634  Z3_ast r = Z3_mk_fpa_fma(a.ctx(), rm, a, b, c);
1635  a.check_error();
1636  return expr(a.ctx(), r);
1637  }
1638 
1639 
1645  inline expr ite(expr const & c, expr const & t, expr const & e) {
1646  check_context(c, t); check_context(c, e);
1647  assert(c.is_bool());
1648  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
1649  c.check_error();
1650  return expr(c.ctx(), r);
1651  }
1652 
1653 
1658  inline expr to_expr(context & c, Z3_ast a) {
1659  c.check_error();
1660  assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
1661  Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
1662  Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
1664  return expr(c, a);
1665  }
1666 
1667  inline sort to_sort(context & c, Z3_sort s) {
1668  c.check_error();
1669  return sort(c, s);
1670  }
1671 
1672  inline func_decl to_func_decl(context & c, Z3_func_decl f) {
1673  c.check_error();
1674  return func_decl(c, f);
1675  }
1676 
1680  inline expr sle(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsle(a.ctx(), a, b)); }
1681  inline expr sle(expr const & a, int b) { return sle(a, a.ctx().num_val(b, a.get_sort())); }
1682  inline expr sle(int a, expr const & b) { return sle(b.ctx().num_val(a, b.get_sort()), b); }
1686  inline expr slt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvslt(a.ctx(), a, b)); }
1687  inline expr slt(expr const & a, int b) { return slt(a, a.ctx().num_val(b, a.get_sort())); }
1688  inline expr slt(int a, expr const & b) { return slt(b.ctx().num_val(a, b.get_sort()), b); }
1689 
1690 
1694  inline expr ule(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
1695  inline expr ule(expr const & a, int b) { return ule(a, a.ctx().num_val(b, a.get_sort())); }
1696  inline expr ule(int a, expr const & b) { return ule(b.ctx().num_val(a, b.get_sort()), b); }
1700  inline expr ult(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }
1701  inline expr ult(expr const & a, int b) { return ult(a, a.ctx().num_val(b, a.get_sort())); }
1702  inline expr ult(int a, expr const & b) { return ult(b.ctx().num_val(a, b.get_sort()), b); }
1706  inline expr uge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }
1707  inline expr uge(expr const & a, int b) { return uge(a, a.ctx().num_val(b, a.get_sort())); }
1708  inline expr uge(int a, expr const & b) { return uge(b.ctx().num_val(a, b.get_sort()), b); }
1712  inline expr ugt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
1713  inline expr ugt(expr const & a, int b) { return ugt(a, a.ctx().num_val(b, a.get_sort())); }
1714  inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), b); }
1718  inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
1719  inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); }
1720  inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); }
1721 
1725  inline expr srem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsrem(a.ctx(), a, b)); }
1726  inline expr srem(expr const & a, int b) { return srem(a, a.ctx().num_val(b, a.get_sort())); }
1727  inline expr srem(int a, expr const & b) { return srem(b.ctx().num_val(a, b.get_sort()), b); }
1728 
1732  inline expr smod(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsmod(a.ctx(), a, b)); }
1733  inline expr smod(expr const & a, int b) { return smod(a, a.ctx().num_val(b, a.get_sort())); }
1734  inline expr smod(int a, expr const & b) { return smod(b.ctx().num_val(a, b.get_sort()), b); }
1735 
1739  inline expr urem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvurem(a.ctx(), a, b)); }
1740  inline expr urem(expr const & a, int b) { return urem(a, a.ctx().num_val(b, a.get_sort())); }
1741  inline expr urem(int a, expr const & b) { return urem(b.ctx().num_val(a, b.get_sort()), b); }
1742 
1746  inline expr shl(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvshl(a.ctx(), a, b)); }
1747  inline expr shl(expr const & a, int b) { return shl(a, a.ctx().num_val(b, a.get_sort())); }
1748  inline expr shl(int a, expr const & b) { return shl(b.ctx().num_val(a, b.get_sort()), b); }
1749 
1753  inline expr lshr(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvlshr(a.ctx(), a, b)); }
1754  inline expr lshr(expr const & a, int b) { return lshr(a, a.ctx().num_val(b, a.get_sort())); }
1755  inline expr lshr(int a, expr const & b) { return lshr(b.ctx().num_val(a, b.get_sort()), b); }
1756 
1760  inline expr ashr(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvashr(a.ctx(), a, b)); }
1761  inline expr ashr(expr const & a, int b) { return ashr(a, a.ctx().num_val(b, a.get_sort())); }
1762  inline expr ashr(int a, expr const & b) { return ashr(b.ctx().num_val(a, b.get_sort()), b); }
1763 
1767  inline expr zext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_zero_ext(a.ctx(), i, a)); }
1768 
1772  inline expr bv2int(expr const& a, bool is_signed) { Z3_ast r = Z3_mk_bv2int(a.ctx(), a, is_signed); a.check_error(); return expr(a.ctx(), r); }
1773  inline expr int2bv(unsigned n, expr const& a) { Z3_ast r = Z3_mk_int2bv(a.ctx(), n, a); a.check_error(); return expr(a.ctx(), r); }
1774 
1778  inline expr bvadd_no_overflow(expr const& a, expr const& b, bool is_signed) {
1779  check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_overflow(a.ctx(), a, b, is_signed); a.check_error(); return expr(a.ctx(), r);
1780  }
1781  inline expr bvadd_no_underflow(expr const& a, expr const& b) {
1782  check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1783  }
1784  inline expr bvsub_no_overflow(expr const& a, expr const& b) {
1785  check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1786  }
1787  inline expr bvsub_no_underflow(expr const& a, expr const& b, bool is_signed) {
1788  check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_underflow(a.ctx(), a, b, is_signed); a.check_error(); return expr(a.ctx(), r);
1789  }
1790  inline expr bvsdiv_no_overflow(expr const& a, expr const& b) {
1791  check_context(a, b); Z3_ast r = Z3_mk_bvsdiv_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1792  }
1793  inline expr bvneg_no_overflow(expr const& a) {
1794  Z3_ast r = Z3_mk_bvneg_no_overflow(a.ctx(), a); a.check_error(); return expr(a.ctx(), r);
1795  }
1796  inline expr bvmul_no_overflow(expr const& a, expr const& b, bool is_signed) {
1797  check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_overflow(a.ctx(), a, b, is_signed); a.check_error(); return expr(a.ctx(), r);
1798  }
1799  inline expr bvmul_no_underflow(expr const& a, expr const& b) {
1800  check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1801  }
1802 
1803 
1807  inline expr sext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_sign_ext(a.ctx(), i, a)); }
1808 
1809  inline func_decl linear_order(sort const& a, unsigned index) {
1810  return to_func_decl(a.ctx(), Z3_mk_linear_order(a.ctx(), a, index));
1811  }
1812  inline func_decl partial_order(sort const& a, unsigned index) {
1813  return to_func_decl(a.ctx(), Z3_mk_partial_order(a.ctx(), a, index));
1814  }
1815  inline func_decl piecewise_linear_order(sort const& a, unsigned index) {
1816  return to_func_decl(a.ctx(), Z3_mk_piecewise_linear_order(a.ctx(), a, index));
1817  }
1818  inline func_decl tree_order(sort const& a, unsigned index) {
1819  return to_func_decl(a.ctx(), Z3_mk_tree_order(a.ctx(), a, index));
1820  }
1821 
1822  template<typename T> class cast_ast;
1823 
1824  template<> class cast_ast<ast> {
1825  public:
1826  ast operator()(context & c, Z3_ast a) { return ast(c, a); }
1827  };
1828 
1829  template<> class cast_ast<expr> {
1830  public:
1831  expr operator()(context & c, Z3_ast a) {
1832  assert(Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
1833  Z3_get_ast_kind(c, a) == Z3_APP_AST ||
1835  Z3_get_ast_kind(c, a) == Z3_VAR_AST);
1836  return expr(c, a);
1837  }
1838  };
1839 
1840  template<> class cast_ast<sort> {
1841  public:
1842  sort operator()(context & c, Z3_ast a) {
1843  assert(Z3_get_ast_kind(c, a) == Z3_SORT_AST);
1844  return sort(c, reinterpret_cast<Z3_sort>(a));
1845  }
1846  };
1847 
1848  template<> class cast_ast<func_decl> {
1849  public:
1850  func_decl operator()(context & c, Z3_ast a) {
1851  assert(Z3_get_ast_kind(c, a) == Z3_FUNC_DECL_AST);
1852  return func_decl(c, reinterpret_cast<Z3_func_decl>(a));
1853  }
1854  };
1855 
1856  template<typename T>
1857  class ast_vector_tpl : public object {
1858  Z3_ast_vector m_vector;
1859  void init(Z3_ast_vector v) { Z3_ast_vector_inc_ref(ctx(), v); m_vector = v; }
1860  public:
1862  ast_vector_tpl(context & c, Z3_ast_vector v):object(c) { init(v); }
1863  ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
1865  operator Z3_ast_vector() const { return m_vector; }
1866  unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); }
1867  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); }
1868  void push_back(T const & e) { Z3_ast_vector_push(ctx(), m_vector, e); check_error(); }
1869  void resize(unsigned sz) { Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }
1870  T back() const { return operator[](size() - 1); }
1871  void pop_back() { assert(size() > 0); resize(size() - 1); }
1872  bool empty() const { return size() == 0; }
1874  Z3_ast_vector_inc_ref(s.ctx(), s.m_vector);
1875  Z3_ast_vector_dec_ref(ctx(), m_vector);
1876  m_ctx = s.m_ctx;
1877  m_vector = s.m_vector;
1878  return *this;
1879  }
1880  ast_vector_tpl& set(unsigned idx, ast& a) {
1881  Z3_ast_vector_set(ctx(), m_vector, idx, a);
1882  return *this;
1883  }
1884  /*
1885  Disabled pending C++98 build upgrade
1886  bool contains(T const& x) const {
1887  for (T y : *this) if (eq(x, y)) return true;
1888  return false;
1889  }
1890  */
1891 
1892  class iterator {
1893  ast_vector_tpl const* m_vector;
1894  unsigned m_index;
1895  public:
1896  iterator(ast_vector_tpl const* v, unsigned i): m_vector(v), m_index(i) {}
1897  iterator(iterator const& other): m_vector(other.m_vector), m_index(other.m_index) {}
1898  iterator operator=(iterator const& other) { m_vector = other.m_vector; m_index = other.m_index; return *this; }
1899 
1900  bool operator==(iterator const& other) const {
1901  return other.m_index == m_index;
1902  };
1903  bool operator!=(iterator const& other) const {
1904  return other.m_index != m_index;
1905  };
1907  ++m_index;
1908  return *this;
1909  }
1910  void set(T& arg) {
1911  Z3_ast_vector_set(m_vector->ctx(), *m_vector, m_index, arg);
1912  }
1913  iterator operator++(int) { iterator tmp = *this; ++m_index; return tmp; }
1914  T * operator->() const { return &(operator*()); }
1915  T operator*() const { return (*m_vector)[m_index]; }
1916  };
1917  iterator begin() const { return iterator(this, 0); }
1918  iterator end() const { return iterator(this, size()); }
1919  friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
1920  };
1921 
1922 
1923  template<typename T>
1924  template<typename T2>
1926  m_array = new T[v.size()];
1927  m_size = v.size();
1928  for (unsigned i = 0; i < m_size; i++) {
1929  m_array[i] = v[i];
1930  }
1931  }
1932 
1933  // Basic functions for creating quantified formulas.
1934  // The C API should be used for creating quantifiers with patterns, weights, many variables, etc.
1935  inline expr forall(expr const & x, expr const & b) {
1936  check_context(x, b);
1937  Z3_app vars[] = {(Z3_app) x};
1938  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1939  }
1940  inline expr forall(expr const & x1, expr const & x2, expr const & b) {
1941  check_context(x1, b); check_context(x2, b);
1942  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1943  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1944  }
1945  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
1946  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1947  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1948  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1949  }
1950  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
1951  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1952  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1953  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1954  }
1955  inline expr forall(expr_vector const & xs, expr const & b) {
1956  array<Z3_app> vars(xs);
1957  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);
1958  }
1959  inline expr exists(expr const & x, expr const & b) {
1960  check_context(x, b);
1961  Z3_app vars[] = {(Z3_app) x};
1962  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1963  }
1964  inline expr exists(expr const & x1, expr const & x2, expr const & b) {
1965  check_context(x1, b); check_context(x2, b);
1966  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1967  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1968  }
1969  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
1970  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1971  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1972  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1973  }
1974  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
1975  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1976  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1977  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1978  }
1979  inline expr exists(expr_vector const & xs, expr const & b) {
1980  array<Z3_app> vars(xs);
1981  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);
1982  }
1983  inline expr lambda(expr const & x, expr const & b) {
1984  check_context(x, b);
1985  Z3_app vars[] = {(Z3_app) x};
1986  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 1, vars, b); b.check_error(); return expr(b.ctx(), r);
1987  }
1988  inline expr lambda(expr const & x1, expr const & x2, expr const & b) {
1989  check_context(x1, b); check_context(x2, b);
1990  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1991  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 2, vars, b); b.check_error(); return expr(b.ctx(), r);
1992  }
1993  inline expr lambda(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
1994  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1995  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1996  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 3, vars, b); b.check_error(); return expr(b.ctx(), r);
1997  }
1998  inline expr lambda(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
1999  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2000  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2001  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 4, vars, b); b.check_error(); return expr(b.ctx(), r);
2002  }
2003  inline expr lambda(expr_vector const & xs, expr const & b) {
2004  array<Z3_app> vars(xs);
2005  Z3_ast r = Z3_mk_lambda_const(b.ctx(), vars.size(), vars.ptr(), b); b.check_error(); return expr(b.ctx(), r);
2006  }
2007 
2008  inline expr pble(expr_vector const& es, int const* coeffs, int bound) {
2009  assert(es.size() > 0);
2010  context& ctx = es[0].ctx();
2011  array<Z3_ast> _es(es);
2012  Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
2013  ctx.check_error();
2014  return expr(ctx, r);
2015  }
2016  inline expr pbge(expr_vector const& es, int const* coeffs, int bound) {
2017  assert(es.size() > 0);
2018  context& ctx = es[0].ctx();
2019  array<Z3_ast> _es(es);
2020  Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
2021  ctx.check_error();
2022  return expr(ctx, r);
2023  }
2024  inline expr pbeq(expr_vector const& es, int const* coeffs, int bound) {
2025  assert(es.size() > 0);
2026  context& ctx = es[0].ctx();
2027  array<Z3_ast> _es(es);
2028  Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
2029  ctx.check_error();
2030  return expr(ctx, r);
2031  }
2032  inline expr atmost(expr_vector const& es, unsigned bound) {
2033  assert(es.size() > 0);
2034  context& ctx = es[0].ctx();
2035  array<Z3_ast> _es(es);
2036  Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
2037  ctx.check_error();
2038  return expr(ctx, r);
2039  }
2040  inline expr atleast(expr_vector const& es, unsigned bound) {
2041  assert(es.size() > 0);
2042  context& ctx = es[0].ctx();
2043  array<Z3_ast> _es(es);
2044  Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
2045  ctx.check_error();
2046  return expr(ctx, r);
2047  }
2048  inline expr sum(expr_vector const& args) {
2049  assert(args.size() > 0);
2050  context& ctx = args[0].ctx();
2051  array<Z3_ast> _args(args);
2052  Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
2053  ctx.check_error();
2054  return expr(ctx, r);
2055  }
2056 
2057  inline expr distinct(expr_vector const& args) {
2058  assert(args.size() > 0);
2059  context& ctx = args[0].ctx();
2060  array<Z3_ast> _args(args);
2061  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
2062  ctx.check_error();
2063  return expr(ctx, r);
2064  }
2065 
2066  inline expr concat(expr const& a, expr const& b) {
2067  check_context(a, b);
2068  Z3_ast r;
2069  if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
2070  Z3_ast _args[2] = { a, b };
2071  r = Z3_mk_seq_concat(a.ctx(), 2, _args);
2072  }
2073  else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
2074  Z3_ast _args[2] = { a, b };
2075  r = Z3_mk_re_concat(a.ctx(), 2, _args);
2076  }
2077  else {
2078  r = Z3_mk_concat(a.ctx(), a, b);
2079  }
2080  a.ctx().check_error();
2081  return expr(a.ctx(), r);
2082  }
2083 
2084  inline expr concat(expr_vector const& args) {
2085  Z3_ast r;
2086  assert(args.size() > 0);
2087  if (args.size() == 1) {
2088  return args[0];
2089  }
2090  context& ctx = args[0].ctx();
2091  array<Z3_ast> _args(args);
2092  if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
2093  r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
2094  }
2095  else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
2096  r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
2097  }
2098  else {
2099  r = _args[args.size()-1];
2100  for (unsigned i = args.size()-1; i > 0; ) {
2101  --i;
2102  r = Z3_mk_concat(ctx, _args[i], r);
2103  ctx.check_error();
2104  }
2105  }
2106  ctx.check_error();
2107  return expr(ctx, r);
2108  }
2109 
2110  inline expr mk_or(expr_vector const& args) {
2111  array<Z3_ast> _args(args);
2112  Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2113  args.check_error();
2114  return expr(args.ctx(), r);
2115  }
2116  inline expr mk_and(expr_vector const& args) {
2117  array<Z3_ast> _args(args);
2118  Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2119  args.check_error();
2120  return expr(args.ctx(), r);
2121  }
2122 
2123 
2124  class func_entry : public object {
2125  Z3_func_entry m_entry;
2126  void init(Z3_func_entry e) {
2127  m_entry = e;
2128  Z3_func_entry_inc_ref(ctx(), m_entry);
2129  }
2130  public:
2131  func_entry(context & c, Z3_func_entry e):object(c) { init(e); }
2132  func_entry(func_entry const & s):object(s) { init(s.m_entry); }
2134  operator Z3_func_entry() const { return m_entry; }
2136  Z3_func_entry_inc_ref(s.ctx(), s.m_entry);
2137  Z3_func_entry_dec_ref(ctx(), m_entry);
2138  m_ctx = s.m_ctx;
2139  m_entry = s.m_entry;
2140  return *this;
2141  }
2142  expr value() const { Z3_ast r = Z3_func_entry_get_value(ctx(), m_entry); check_error(); return expr(ctx(), r); }
2143  unsigned num_args() const { unsigned r = Z3_func_entry_get_num_args(ctx(), m_entry); check_error(); return r; }
2144  expr arg(unsigned i) const { Z3_ast r = Z3_func_entry_get_arg(ctx(), m_entry, i); check_error(); return expr(ctx(), r); }
2145  };
2146 
2147  class func_interp : public object {
2148  Z3_func_interp m_interp;
2149  void init(Z3_func_interp e) {
2150  m_interp = e;
2151  Z3_func_interp_inc_ref(ctx(), m_interp);
2152  }
2153  public:
2154  func_interp(context & c, Z3_func_interp e):object(c) { init(e); }
2155  func_interp(func_interp const & s):object(s) { init(s.m_interp); }
2157  operator Z3_func_interp() const { return m_interp; }
2159  Z3_func_interp_inc_ref(s.ctx(), s.m_interp);
2160  Z3_func_interp_dec_ref(ctx(), m_interp);
2161  m_ctx = s.m_ctx;
2162  m_interp = s.m_interp;
2163  return *this;
2164  }
2165  expr else_value() const { Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), r); }
2166  unsigned num_entries() const { unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }
2167  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); }
2168  void add_entry(expr_vector const& args, expr& value) {
2169  Z3_func_interp_add_entry(ctx(), m_interp, args, value);
2170  check_error();
2171  }
2172  void set_else(expr& value) {
2173  Z3_func_interp_set_else(ctx(), m_interp, value);
2174  check_error();
2175  }
2176  };
2177 
2178  class model : public object {
2179  Z3_model m_model;
2180  void init(Z3_model m) {
2181  m_model = m;
2182  Z3_model_inc_ref(ctx(), m);
2183  }
2184  public:
2185  struct translate {};
2186  model(context & c):object(c) { init(Z3_mk_model(c)); }
2187  model(context & c, Z3_model m):object(c) { init(m); }
2188  model(model const & s):object(s) { init(s.m_model); }
2189  model(model& src, context& dst, translate) : object(dst) { init(Z3_model_translate(src.ctx(), src, dst)); }
2190  ~model() { Z3_model_dec_ref(ctx(), m_model); }
2191  operator Z3_model() const { return m_model; }
2192  model & operator=(model const & s) {
2193  Z3_model_inc_ref(s.ctx(), s.m_model);
2194  Z3_model_dec_ref(ctx(), m_model);
2195  m_ctx = s.m_ctx;
2196  m_model = s.m_model;
2197  return *this;
2198  }
2199 
2200  expr eval(expr const & n, bool model_completion=false) const {
2201  check_context(*this, n);
2202  Z3_ast r = 0;
2203  bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
2204  check_error();
2205  if (status == false && ctx().enable_exceptions())
2206  Z3_THROW(exception("failed to evaluate expression"));
2207  return expr(ctx(), r);
2208  }
2209 
2210  unsigned num_consts() const { return Z3_model_get_num_consts(ctx(), m_model); }
2211  unsigned num_funcs() const { return Z3_model_get_num_funcs(ctx(), m_model); }
2212  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); }
2213  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); }
2214  unsigned size() const { return num_consts() + num_funcs(); }
2215  func_decl operator[](int i) const {
2216  assert(0 <= i);
2217  return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
2218  }
2219 
2220  // returns interpretation of constant declaration c.
2221  // If c is not assigned any value in the model it returns
2222  // an expression with a null ast reference.
2224  check_context(*this, c);
2225  Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);
2226  check_error();
2227  return expr(ctx(), r);
2228  }
2230  check_context(*this, f);
2231  Z3_func_interp r = Z3_model_get_func_interp(ctx(), m_model, f);
2232  check_error();
2233  return func_interp(ctx(), r);
2234  }
2235 
2236  // returns true iff the model contains an interpretation
2237  // for function f.
2238  bool has_interp(func_decl f) const {
2239  check_context(*this, f);
2240  return Z3_model_has_interp(ctx(), m_model, f);
2241  }
2242 
2244  Z3_func_interp r = Z3_add_func_interp(ctx(), m_model, f, else_val);
2245  check_error();
2246  return func_interp(ctx(), r);
2247  }
2248 
2249  void add_const_interp(func_decl& f, expr& value) {
2250  Z3_add_const_interp(ctx(), m_model, f, value);
2251  check_error();
2252  }
2253 
2254  friend std::ostream & operator<<(std::ostream & out, model const & m);
2255  };
2256  inline std::ostream & operator<<(std::ostream & out, model const & m) { out << Z3_model_to_string(m.ctx(), m); return out; }
2257 
2258  class stats : public object {
2259  Z3_stats m_stats;
2260  void init(Z3_stats e) {
2261  m_stats = e;
2262  Z3_stats_inc_ref(ctx(), m_stats);
2263  }
2264  public:
2265  stats(context & c):object(c), m_stats(0) {}
2266  stats(context & c, Z3_stats e):object(c) { init(e); }
2267  stats(stats const & s):object(s) { init(s.m_stats); }
2268  ~stats() { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); }
2269  operator Z3_stats() const { return m_stats; }
2270  stats & operator=(stats const & s) {
2271  Z3_stats_inc_ref(s.ctx(), s.m_stats);
2272  if (m_stats) Z3_stats_dec_ref(ctx(), m_stats);
2273  m_ctx = s.m_ctx;
2274  m_stats = s.m_stats;
2275  return *this;
2276  }
2277  unsigned size() const { return Z3_stats_size(ctx(), m_stats); }
2278  std::string key(unsigned i) const { Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; }
2279  bool is_uint(unsigned i) const { bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r; }
2280  bool is_double(unsigned i) const { bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r; }
2281  unsigned uint_value(unsigned i) const { unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; }
2282  double double_value(unsigned i) const { double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
2283  friend std::ostream & operator<<(std::ostream & out, stats const & s);
2284  };
2285  inline std::ostream & operator<<(std::ostream & out, stats const & s) { out << Z3_stats_to_string(s.ctx(), s); return out; }
2286 
2287 
2288  inline std::ostream & operator<<(std::ostream & out, check_result r) {
2289  if (r == unsat) out << "unsat";
2290  else if (r == sat) out << "sat";
2291  else out << "unknown";
2292  return out;
2293  }
2294 
2295 
2296  class solver : public object {
2297  Z3_solver m_solver;
2298  void init(Z3_solver s) {
2299  m_solver = s;
2300  Z3_solver_inc_ref(ctx(), s);
2301  }
2302  public:
2303  struct simple {};
2304  struct translate {};
2305  solver(context & c):object(c) { init(Z3_mk_solver(c)); }
2307  solver(context & c, Z3_solver s):object(c) { init(s); }
2308  solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); }
2309  solver(context & c, solver const& src, translate): object(c) { init(Z3_solver_translate(src.ctx(), src, c)); }
2310  solver(solver const & s):object(s) { init(s.m_solver); }
2311  ~solver() { Z3_solver_dec_ref(ctx(), m_solver); }
2312  operator Z3_solver() const { return m_solver; }
2313  solver & operator=(solver const & s) {
2314  Z3_solver_inc_ref(s.ctx(), s.m_solver);
2315  Z3_solver_dec_ref(ctx(), m_solver);
2316  m_ctx = s.m_ctx;
2317  m_solver = s.m_solver;
2318  return *this;
2319  }
2320  void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
2321  void set(char const * k, bool v) { params p(ctx()); p.set(k, v); set(p); }
2322  void set(char const * k, unsigned v) { params p(ctx()); p.set(k, v); set(p); }
2323  void set(char const * k, double v) { params p(ctx()); p.set(k, v); set(p); }
2324  void set(char const * k, symbol const & v) { params p(ctx()); p.set(k, v); set(p); }
2325  void set(char const * k, char const* v) { params p(ctx()); p.set(k, v); set(p); }
2326  void push() { Z3_solver_push(ctx(), m_solver); check_error(); }
2327  void pop(unsigned n = 1) { Z3_solver_pop(ctx(), m_solver, n); check_error(); }
2328  void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); }
2329  void add(expr const & e) { assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); }
2330  void add(expr const & e, expr const & p) {
2331  assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
2332  Z3_solver_assert_and_track(ctx(), m_solver, e, p);
2333  check_error();
2334  }
2335  void add(expr const & e, char const * p) {
2336  add(e, ctx().bool_const(p));
2337  }
2338  // fails for some compilers:
2339  // void add(expr_vector const& v) { check_context(*this, v); for (expr e : v) add(e); }
2340  void from_file(char const* file) { Z3_solver_from_file(ctx(), m_solver, file); ctx().check_parser_error(); }
2341  void from_string(char const* s) { Z3_solver_from_string(ctx(), m_solver, s); ctx().check_parser_error(); }
2342 
2344  check_result check(unsigned n, expr * const assumptions) {
2345  array<Z3_ast> _assumptions(n);
2346  for (unsigned i = 0; i < n; i++) {
2347  check_context(*this, assumptions[i]);
2348  _assumptions[i] = assumptions[i];
2349  }
2350  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
2351  check_error();
2352  return to_check_result(r);
2353  }
2354  check_result check(expr_vector const& assumptions) {
2355  unsigned n = assumptions.size();
2356  array<Z3_ast> _assumptions(n);
2357  for (unsigned i = 0; i < n; i++) {
2358  check_context(*this, assumptions[i]);
2359  _assumptions[i] = assumptions[i];
2360  }
2361  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
2362  check_error();
2363  return to_check_result(r);
2364  }
2365  model get_model() const { Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }
2366  check_result consequences(expr_vector& assumptions, expr_vector& vars, expr_vector& conseq) {
2367  Z3_lbool r = Z3_solver_get_consequences(ctx(), m_solver, assumptions, vars, conseq);
2368  check_error();
2369  return to_check_result(r);
2370  }
2371  std::string reason_unknown() const { Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }
2372  stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }
2373  expr_vector unsat_core() const { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2374  expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2375  expr_vector non_units() const { Z3_ast_vector r = Z3_solver_get_non_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2376  expr_vector units() const { Z3_ast_vector r = Z3_solver_get_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2377  expr_vector trail() const { Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2378  expr_vector trail(array<unsigned>& levels) const {
2379  Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver);
2380  check_error();
2381  expr_vector result(ctx(), r);
2382  unsigned sz = result.size();
2383  levels.resize(sz);
2384  Z3_solver_get_levels(ctx(), m_solver, r, sz, levels.ptr());
2385  check_error();
2386  return result;
2387  }
2388  expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
2389  friend std::ostream & operator<<(std::ostream & out, solver const & s);
2390 
2391  std::string to_smt2(char const* status = "unknown") {
2392  array<Z3_ast> es(assertions());
2393  Z3_ast const* fmls = es.ptr();
2394  Z3_ast fml = 0;
2395  unsigned sz = es.size();
2396  if (sz > 0) {
2397  --sz;
2398  fml = fmls[sz];
2399  }
2400  else {
2401  fml = ctx().bool_val(true);
2402  }
2403  return std::string(Z3_benchmark_to_smtlib_string(
2404  ctx(),
2405  "", "", status, "",
2406  sz,
2407  fmls,
2408  fml));
2409  }
2410 
2411  std::string dimacs() const { return std::string(Z3_solver_to_dimacs_string(ctx(), m_solver)); }
2412 
2414 
2415 
2416  expr_vector cube(expr_vector& vars, unsigned cutoff) {
2417  Z3_ast_vector r = Z3_solver_cube(ctx(), m_solver, vars, cutoff);
2418  check_error();
2419  return expr_vector(ctx(), r);
2420  }
2421 
2423  solver& m_solver;
2424  unsigned& m_cutoff;
2425  expr_vector& m_vars;
2426  expr_vector m_cube;
2427  bool m_end;
2428  bool m_empty;
2429 
2430  void inc() {
2431  assert(!m_end && !m_empty);
2432  m_cube = m_solver.cube(m_vars, m_cutoff);
2433  m_cutoff = 0xFFFFFFFF;
2434  if (m_cube.size() == 1 && m_cube[0].is_false()) {
2435  m_cube = z3::expr_vector(m_solver.ctx());
2436  m_end = true;
2437  }
2438  else if (m_cube.empty()) {
2439  m_empty = true;
2440  }
2441  }
2442  public:
2443  cube_iterator(solver& s, expr_vector& vars, unsigned& cutoff, bool end):
2444  m_solver(s),
2445  m_cutoff(cutoff),
2446  m_vars(vars),
2447  m_cube(s.ctx()),
2448  m_end(end),
2449  m_empty(false) {
2450  if (!m_end) {
2451  inc();
2452  }
2453  }
2454 
2456  assert(!m_end);
2457  if (m_empty) {
2458  m_end = true;
2459  }
2460  else {
2461  inc();
2462  }
2463  return *this;
2464  }
2465  cube_iterator operator++(int) { assert(false); return *this; }
2466  expr_vector const * operator->() const { return &(operator*()); }
2467  expr_vector const& operator*() const { return m_cube; }
2468 
2469  bool operator==(cube_iterator const& other) {
2470  return other.m_end == m_end;
2471  };
2472  bool operator!=(cube_iterator const& other) {
2473  return other.m_end != m_end;
2474  };
2475 
2476  };
2477 
2479  solver& m_solver;
2480  unsigned m_cutoff;
2481  expr_vector m_default_vars;
2482  expr_vector& m_vars;
2483  public:
2485  m_solver(s),
2486  m_cutoff(0xFFFFFFFF),
2487  m_default_vars(s.ctx()),
2488  m_vars(m_default_vars)
2489  {}
2490 
2491  cube_generator(solver& s, expr_vector& vars):
2492  m_solver(s),
2493  m_cutoff(0xFFFFFFFF),
2494  m_default_vars(s.ctx()),
2495  m_vars(vars)
2496  {}
2497 
2498  cube_iterator begin() { return cube_iterator(m_solver, m_vars, m_cutoff, false); }
2499  cube_iterator end() { return cube_iterator(m_solver, m_vars, m_cutoff, true); }
2500  void set_cutoff(unsigned c) { m_cutoff = c; }
2501  };
2502 
2503  cube_generator cubes() { return cube_generator(*this); }
2504  cube_generator cubes(expr_vector& vars) { return cube_generator(*this, vars); }
2505 
2506  };
2507  inline std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
2508 
2509  class goal : public object {
2510  Z3_goal m_goal;
2511  void init(Z3_goal s) {
2512  m_goal = s;
2513  Z3_goal_inc_ref(ctx(), s);
2514  }
2515  public:
2516  goal(context & c, bool models=true, bool unsat_cores=false, bool proofs=false):object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); }
2517  goal(context & c, Z3_goal s):object(c) { init(s); }
2518  goal(goal const & s):object(s) { init(s.m_goal); }
2519  ~goal() { Z3_goal_dec_ref(ctx(), m_goal); }
2520  operator Z3_goal() const { return m_goal; }
2521  goal & operator=(goal const & s) {
2522  Z3_goal_inc_ref(s.ctx(), s.m_goal);
2523  Z3_goal_dec_ref(ctx(), m_goal);
2524  m_ctx = s.m_ctx;
2525  m_goal = s.m_goal;
2526  return *this;
2527  }
2528  void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
2529  void add(expr_vector const& v) { check_context(*this, v); for (unsigned i = 0; i < v.size(); ++i) add(v[i]); }
2530  unsigned size() const { return Z3_goal_size(ctx(), m_goal); }
2531  expr operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
2532  Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); }
2533  bool inconsistent() const { return Z3_goal_inconsistent(ctx(), m_goal); }
2534  unsigned depth() const { return Z3_goal_depth(ctx(), m_goal); }
2535  void reset() { Z3_goal_reset(ctx(), m_goal); }
2536  unsigned num_exprs() const { return Z3_goal_num_exprs(ctx(), m_goal); }
2537  bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal); }
2538  bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal); }
2539  model convert_model(model const & m) const {
2540  check_context(*this, m);
2541  Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, m);
2542  check_error();
2543  return model(ctx(), new_m);
2544  }
2545  model get_model() const {
2546  Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, 0);
2547  check_error();
2548  return model(ctx(), new_m);
2549  }
2550  expr as_expr() const {
2551  unsigned n = size();
2552  if (n == 0)
2553  return ctx().bool_val(true);
2554  else if (n == 1)
2555  return operator[](0);
2556  else {
2557  array<Z3_ast> args(n);
2558  for (unsigned i = 0; i < n; i++)
2559  args[i] = operator[](i);
2560  return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
2561  }
2562  }
2563  std::string dimacs() const { return std::string(Z3_goal_to_dimacs_string(ctx(), m_goal)); }
2564  friend std::ostream & operator<<(std::ostream & out, goal const & g);
2565  };
2566  inline std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; }
2567 
2568  class apply_result : public object {
2569  Z3_apply_result m_apply_result;
2570  void init(Z3_apply_result s) {
2571  m_apply_result = s;
2573  }
2574  public:
2575  apply_result(context & c, Z3_apply_result s):object(c) { init(s); }
2576  apply_result(apply_result const & s):object(s) { init(s.m_apply_result); }
2577  ~apply_result() { Z3_apply_result_dec_ref(ctx(), m_apply_result); }
2578  operator Z3_apply_result() const { return m_apply_result; }
2580  Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result);
2581  Z3_apply_result_dec_ref(ctx(), m_apply_result);
2582  m_ctx = s.m_ctx;
2583  m_apply_result = s.m_apply_result;
2584  return *this;
2585  }
2586  unsigned size() const { return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }
2587  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); }
2588  friend std::ostream & operator<<(std::ostream & out, apply_result const & r);
2589  };
2590  inline std::ostream & operator<<(std::ostream & out, apply_result const & r) { out << Z3_apply_result_to_string(r.ctx(), r); return out; }
2591 
2592  class tactic : public object {
2593  Z3_tactic m_tactic;
2594  void init(Z3_tactic s) {
2595  m_tactic = s;
2596  Z3_tactic_inc_ref(ctx(), s);
2597  }
2598  public:
2599  tactic(context & c, char const * name):object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); }
2600  tactic(context & c, Z3_tactic s):object(c) { init(s); }
2601  tactic(tactic const & s):object(s) { init(s.m_tactic); }
2602  ~tactic() { Z3_tactic_dec_ref(ctx(), m_tactic); }
2603  operator Z3_tactic() const { return m_tactic; }
2604  tactic & operator=(tactic const & s) {
2605  Z3_tactic_inc_ref(s.ctx(), s.m_tactic);
2606  Z3_tactic_dec_ref(ctx(), m_tactic);
2607  m_ctx = s.m_ctx;
2608  m_tactic = s.m_tactic;
2609  return *this;
2610  }
2611  solver mk_solver() const { Z3_solver r = Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error(); return solver(ctx(), r); }
2612  apply_result apply(goal const & g) const {
2613  check_context(*this, g);
2614  Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g);
2615  check_error();
2616  return apply_result(ctx(), r);
2617  }
2618  apply_result operator()(goal const & g) const {
2619  return apply(g);
2620  }
2621  std::string help() const { char const * r = Z3_tactic_get_help(ctx(), m_tactic); check_error(); return r; }
2622  friend tactic operator&(tactic const & t1, tactic const & t2);
2623  friend tactic operator|(tactic const & t1, tactic const & t2);
2624  friend tactic repeat(tactic const & t, unsigned max);
2625  friend tactic with(tactic const & t, params const & p);
2626  friend tactic try_for(tactic const & t, unsigned ms);
2627  friend tactic par_or(unsigned n, tactic const* tactics);
2628  friend tactic par_and_then(tactic const& t1, tactic const& t2);
2630  };
2631 
2632  inline tactic operator&(tactic const & t1, tactic const & t2) {
2633  check_context(t1, t2);
2634  Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
2635  t1.check_error();
2636  return tactic(t1.ctx(), r);
2637  }
2638 
2639  inline tactic operator|(tactic const & t1, tactic const & t2) {
2640  check_context(t1, t2);
2641  Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
2642  t1.check_error();
2643  return tactic(t1.ctx(), r);
2644  }
2645 
2646  inline tactic repeat(tactic const & t, unsigned max=UINT_MAX) {
2647  Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
2648  t.check_error();
2649  return tactic(t.ctx(), r);
2650  }
2651 
2652  inline tactic with(tactic const & t, params const & p) {
2653  Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
2654  t.check_error();
2655  return tactic(t.ctx(), r);
2656  }
2657  inline tactic try_for(tactic const & t, unsigned ms) {
2658  Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
2659  t.check_error();
2660  return tactic(t.ctx(), r);
2661  }
2662  inline tactic par_or(unsigned n, tactic const* tactics) {
2663  if (n == 0) {
2664  Z3_THROW(exception("a non-zero number of tactics need to be passed to par_or"));
2665  }
2666  array<Z3_tactic> buffer(n);
2667  for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
2668  return tactic(tactics[0].ctx(), Z3_tactic_par_or(tactics[0].ctx(), n, buffer.ptr()));
2669  }
2670 
2671  inline tactic par_and_then(tactic const & t1, tactic const & t2) {
2672  check_context(t1, t2);
2673  Z3_tactic r = Z3_tactic_par_and_then(t1.ctx(), t1, t2);
2674  t1.check_error();
2675  return tactic(t1.ctx(), r);
2676  }
2677 
2678  class probe : public object {
2679  Z3_probe m_probe;
2680  void init(Z3_probe s) {
2681  m_probe = s;
2682  Z3_probe_inc_ref(ctx(), s);
2683  }
2684  public:
2685  probe(context & c, char const * name):object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); }
2686  probe(context & c, double val):object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); }
2687  probe(context & c, Z3_probe s):object(c) { init(s); }
2688  probe(probe const & s):object(s) { init(s.m_probe); }
2689  ~probe() { Z3_probe_dec_ref(ctx(), m_probe); }
2690  operator Z3_probe() const { return m_probe; }
2691  probe & operator=(probe const & s) {
2692  Z3_probe_inc_ref(s.ctx(), s.m_probe);
2693  Z3_probe_dec_ref(ctx(), m_probe);
2694  m_ctx = s.m_ctx;
2695  m_probe = s.m_probe;
2696  return *this;
2697  }
2698  double apply(goal const & g) const { double r = Z3_probe_apply(ctx(), m_probe, g); check_error(); return r; }
2699  double operator()(goal const & g) const { return apply(g); }
2700  friend probe operator<=(probe const & p1, probe const & p2);
2701  friend probe operator<=(probe const & p1, double p2);
2702  friend probe operator<=(double p1, probe const & p2);
2703  friend probe operator>=(probe const & p1, probe const & p2);
2704  friend probe operator>=(probe const & p1, double p2);
2705  friend probe operator>=(double p1, probe const & p2);
2706  friend probe operator<(probe const & p1, probe const & p2);
2707  friend probe operator<(probe const & p1, double p2);
2708  friend probe operator<(double p1, probe const & p2);
2709  friend probe operator>(probe const & p1, probe const & p2);
2710  friend probe operator>(probe const & p1, double p2);
2711  friend probe operator>(double p1, probe const & p2);
2712  friend probe operator==(probe const & p1, probe const & p2);
2713  friend probe operator==(probe const & p1, double p2);
2714  friend probe operator==(double p1, probe const & p2);
2715  friend probe operator&&(probe const & p1, probe const & p2);
2716  friend probe operator||(probe const & p1, probe const & p2);
2717  friend probe operator!(probe const & p);
2718  };
2719 
2720  inline probe operator<=(probe const & p1, probe const & p2) {
2721  check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2722  }
2723  inline probe operator<=(probe const & p1, double p2) { return p1 <= probe(p1.ctx(), p2); }
2724  inline probe operator<=(double p1, probe const & p2) { return probe(p2.ctx(), p1) <= p2; }
2725  inline probe operator>=(probe const & p1, probe const & p2) {
2726  check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2727  }
2728  inline probe operator>=(probe const & p1, double p2) { return p1 >= probe(p1.ctx(), p2); }
2729  inline probe operator>=(double p1, probe const & p2) { return probe(p2.ctx(), p1) >= p2; }
2730  inline probe operator<(probe const & p1, probe const & p2) {
2731  check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2732  }
2733  inline probe operator<(probe const & p1, double p2) { return p1 < probe(p1.ctx(), p2); }
2734  inline probe operator<(double p1, probe const & p2) { return probe(p2.ctx(), p1) < p2; }
2735  inline probe operator>(probe const & p1, probe const & p2) {
2736  check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2737  }
2738  inline probe operator>(probe const & p1, double p2) { return p1 > probe(p1.ctx(), p2); }
2739  inline probe operator>(double p1, probe const & p2) { return probe(p2.ctx(), p1) > p2; }
2740  inline probe operator==(probe const & p1, probe const & p2) {
2741  check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2742  }
2743  inline probe operator==(probe const & p1, double p2) { return p1 == probe(p1.ctx(), p2); }
2744  inline probe operator==(double p1, probe const & p2) { return probe(p2.ctx(), p1) == p2; }
2745  inline probe operator&&(probe const & p1, probe const & p2) {
2746  check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2747  }
2748  inline probe operator||(probe const & p1, probe const & p2) {
2749  check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2750  }
2751  inline probe operator!(probe const & p) {
2752  Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
2753  }
2754 
2755  class optimize : public object {
2756  Z3_optimize m_opt;
2757 
2758  public:
2759  class handle {
2760  unsigned m_h;
2761  public:
2762  handle(unsigned h): m_h(h) {}
2763  unsigned h() const { return m_h; }
2764  };
2765  optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }
2767  Z3_optimize_inc_ref(o.ctx(), o.m_opt);
2768  m_opt = o.m_opt;
2769  }
2771  Z3_optimize_inc_ref(o.ctx(), o.m_opt);
2772  Z3_optimize_dec_ref(ctx(), m_opt);
2773  m_opt = o.m_opt;
2774  m_ctx = o.m_ctx;
2775  return *this;
2776  }
2778  operator Z3_optimize() const { return m_opt; }
2779  void add(expr const& e) {
2780  assert(e.is_bool());
2781  Z3_optimize_assert(ctx(), m_opt, e);
2782  }
2783  handle add(expr const& e, unsigned weight) {
2784  assert(e.is_bool());
2785  std::stringstream strm;
2786  strm << weight;
2787  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, strm.str().c_str(), 0));
2788  }
2789  void add(expr const& e, expr const& t) {
2790  assert(e.is_bool());
2791  Z3_optimize_assert_and_track(ctx(), m_opt, e, t);
2792  }
2793 
2794  handle add(expr const& e, char const* weight) {
2795  assert(e.is_bool());
2796  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0));
2797  }
2798  handle maximize(expr const& e) {
2799  return handle(Z3_optimize_maximize(ctx(), m_opt, e));
2800  }
2801  handle minimize(expr const& e) {
2802  return handle(Z3_optimize_minimize(ctx(), m_opt, e));
2803  }
2804  void push() {
2805  Z3_optimize_push(ctx(), m_opt);
2806  }
2807  void pop() {
2808  Z3_optimize_pop(ctx(), m_opt);
2809  }
2811  check_result check(expr_vector const& asms) {
2812  unsigned n = asms.size();
2813  array<Z3_ast> _asms(n);
2814  for (unsigned i = 0; i < n; i++) {
2815  check_context(*this, asms[i]);
2816  _asms[i] = asms[i];
2817  }
2818  Z3_lbool r = Z3_optimize_check(ctx(), m_opt, n, _asms.ptr());
2819  check_error();
2820  return to_check_result(r);
2821  }
2822  model get_model() const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }
2823  expr_vector unsat_core() const { Z3_ast_vector r = Z3_optimize_get_unsat_core(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
2824  void set(params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }
2825  expr lower(handle const& h) {
2826  Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());
2827  check_error();
2828  return expr(ctx(), r);
2829  }
2830  expr upper(handle const& h) {
2831  Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h());
2832  check_error();
2833  return expr(ctx(), r);
2834  }
2835  expr_vector assertions() const { Z3_ast_vector r = Z3_optimize_get_assertions(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
2836  expr_vector objectives() const { Z3_ast_vector r = Z3_optimize_get_objectives(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
2837  stats statistics() const { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); }
2838  friend std::ostream & operator<<(std::ostream & out, optimize const & s);
2839  void from_file(char const* filename) { Z3_optimize_from_file(ctx(), m_opt, filename); check_error(); }
2840  void from_string(char const* constraints) { Z3_optimize_from_string(ctx(), m_opt, constraints); check_error(); }
2841  std::string help() const { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error(); return r; }
2842  };
2843  inline std::ostream & operator<<(std::ostream & out, optimize const & s) { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }
2844 
2845  class fixedpoint : public object {
2846  Z3_fixedpoint m_fp;
2847  public:
2850  operator Z3_fixedpoint() const { return m_fp; }
2851  void from_string(char const* s) { Z3_fixedpoint_from_string(ctx(), m_fp, s); check_error(); }
2852  void from_file(char const* s) { Z3_fixedpoint_from_file(ctx(), m_fp, s); check_error(); }
2853  void add_rule(expr& rule, symbol const& name) { Z3_fixedpoint_add_rule(ctx(), m_fp, rule, name); check_error(); }
2854  void add_fact(func_decl& f, unsigned * args) { Z3_fixedpoint_add_fact(ctx(), m_fp, f, f.arity(), args); check_error(); }
2856  check_result query(func_decl_vector& relations) {
2857  array<Z3_func_decl> rs(relations);
2858  Z3_lbool r = Z3_fixedpoint_query_relations(ctx(), m_fp, rs.size(), rs.ptr());
2859  check_error();
2860  return to_check_result(r);
2861  }
2862  expr get_answer() { Z3_ast r = Z3_fixedpoint_get_answer(ctx(), m_fp); check_error(); return expr(ctx(), r); }
2863  std::string reason_unknown() { return Z3_fixedpoint_get_reason_unknown(ctx(), m_fp); }
2864  void update_rule(expr& rule, symbol const& name) { Z3_fixedpoint_update_rule(ctx(), m_fp, rule, name); check_error(); }
2865  unsigned get_num_levels(func_decl& p) { unsigned r = Z3_fixedpoint_get_num_levels(ctx(), m_fp, p); check_error(); return r; }
2866  expr get_cover_delta(int level, func_decl& p) {
2867  Z3_ast r = Z3_fixedpoint_get_cover_delta(ctx(), m_fp, level, p);
2868  check_error();
2869  return expr(ctx(), r);
2870  }
2871  void add_cover(int level, func_decl& p, expr& property) { Z3_fixedpoint_add_cover(ctx(), m_fp, level, p, property); check_error(); }
2872  stats statistics() const { Z3_stats r = Z3_fixedpoint_get_statistics(ctx(), m_fp); check_error(); return stats(ctx(), r); }
2874  expr_vector assertions() const { Z3_ast_vector r = Z3_fixedpoint_get_assertions(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
2875  expr_vector rules() const { Z3_ast_vector r = Z3_fixedpoint_get_rules(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
2876  void set(params const & p) { Z3_fixedpoint_set_params(ctx(), m_fp, p); check_error(); }
2877  std::string help() const { return Z3_fixedpoint_get_help(ctx(), m_fp); }
2879  std::string to_string() { return Z3_fixedpoint_to_string(ctx(), m_fp, 0, 0); }
2880  std::string to_string(expr_vector const& queries) {
2881  array<Z3_ast> qs(queries);
2882  return Z3_fixedpoint_to_string(ctx(), m_fp, qs.size(), qs.ptr());
2883  }
2884  };
2885  inline std::ostream & operator<<(std::ostream & out, fixedpoint const & f) { return out << Z3_fixedpoint_to_string(f.ctx(), f, 0, 0); }
2886 
2887  inline tactic fail_if(probe const & p) {
2888  Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
2889  p.check_error();
2890  return tactic(p.ctx(), r);
2891  }
2892  inline tactic when(probe const & p, tactic const & t) {
2893  check_context(p, t);
2894  Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
2895  t.check_error();
2896  return tactic(t.ctx(), r);
2897  }
2898  inline tactic cond(probe const & p, tactic const & t1, tactic const & t2) {
2899  check_context(p, t1); check_context(p, t2);
2900  Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
2901  t1.check_error();
2902  return tactic(t1.ctx(), r);
2903  }
2904 
2905  inline symbol context::str_symbol(char const * s) { Z3_symbol r = Z3_mk_string_symbol(m_ctx, s); check_error(); return symbol(*this, r); }
2906  inline symbol context::int_symbol(int n) { Z3_symbol r = Z3_mk_int_symbol(m_ctx, n); check_error(); return symbol(*this, r); }
2907 
2908  inline sort context::bool_sort() { Z3_sort s = Z3_mk_bool_sort(m_ctx); check_error(); return sort(*this, s); }
2909  inline sort context::int_sort() { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }
2910  inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
2911  inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
2912  inline sort context::string_sort() { Z3_sort s = Z3_mk_string_sort(m_ctx); check_error(); return sort(*this, s); }
2913  inline sort context::seq_sort(sort& s) { Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); }
2914  inline sort context::re_sort(sort& s) { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
2915  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); }
2916 
2917  template<>
2918  inline sort context::fpa_sort<16>() { return fpa_sort(5, 11); }
2919 
2920  template<>
2921  inline sort context::fpa_sort<32>() { return fpa_sort(8, 24); }
2922 
2923  template<>
2924  inline sort context::fpa_sort<64>() { return fpa_sort(11, 53); }
2925 
2926  template<>
2927  inline sort context::fpa_sort<128>() { return fpa_sort(15, 113); }
2928 
2930  switch (m_rounding_mode) {
2931  case RNA: return sort(*this, Z3_mk_fpa_rna(m_ctx));
2932  case RNE: return sort(*this, Z3_mk_fpa_rne(m_ctx));
2933  case RTP: return sort(*this, Z3_mk_fpa_rtp(m_ctx));
2934  case RTN: return sort(*this, Z3_mk_fpa_rtn(m_ctx));
2935  case RTZ: return sort(*this, Z3_mk_fpa_rtz(m_ctx));
2936  default: return sort(*this);
2937  }
2938  }
2939 
2940  inline void context::set_rounding_mode(rounding_mode rm) { m_rounding_mode = rm; }
2941 
2942  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); }
2943  inline sort context::array_sort(sort_vector const& d, sort r) {
2944  array<Z3_sort> dom(d);
2945  Z3_sort s = Z3_mk_array_sort_n(m_ctx, dom.size(), dom.ptr(), r); check_error(); return sort(*this, s);
2946  }
2947  inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
2948  array<Z3_symbol> _enum_names(n);
2949  for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
2950  array<Z3_func_decl> _cs(n);
2951  array<Z3_func_decl> _ts(n);
2952  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2953  sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
2954  check_error();
2955  for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
2956  return s;
2957  }
2958  inline func_decl context::tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs) {
2959  array<Z3_symbol> _names(n);
2960  array<Z3_sort> _sorts(n);
2961  for (unsigned i = 0; i < n; i++) { _names[i] = Z3_mk_string_symbol(*this, names[i]); _sorts[i] = sorts[i]; }
2962  array<Z3_func_decl> _projs(n);
2963  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2964  Z3_func_decl tuple;
2965  sort _ignore_s = to_sort(*this, Z3_mk_tuple_sort(*this, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));
2966  check_error();
2967  for (unsigned i = 0; i < n; i++) { projs.push_back(func_decl(*this, _projs[i])); }
2968  return func_decl(*this, tuple);
2969  }
2970 
2971  inline sort context::uninterpreted_sort(char const* name) {
2972  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2973  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
2974  }
2976  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
2977  }
2978 
2979  inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
2980  array<Z3_sort> args(arity);
2981  for (unsigned i = 0; i < arity; i++) {
2982  check_context(domain[i], range);
2983  args[i] = domain[i];
2984  }
2985  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
2986  check_error();
2987  return func_decl(*this, f);
2988  }
2989 
2990  inline func_decl context::function(char const * name, unsigned arity, sort const * domain, sort const & range) {
2991  return function(range.ctx().str_symbol(name), arity, domain, range);
2992  }
2993 
2994  inline func_decl context::function(symbol const& name, sort_vector const& domain, sort const& range) {
2995  array<Z3_sort> args(domain.size());
2996  for (unsigned i = 0; i < domain.size(); i++) {
2997  check_context(domain[i], range);
2998  args[i] = domain[i];
2999  }
3000  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
3001  check_error();
3002  return func_decl(*this, f);
3003  }
3004 
3005  inline func_decl context::function(char const * name, sort_vector const& domain, sort const& range) {
3006  return function(range.ctx().str_symbol(name), domain, range);
3007  }
3008 
3009 
3010  inline func_decl context::function(char const * name, sort const & domain, sort const & range) {
3011  check_context(domain, range);
3012  Z3_sort args[1] = { domain };
3013  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
3014  check_error();
3015  return func_decl(*this, f);
3016  }
3017 
3018  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & range) {
3019  check_context(d1, range); check_context(d2, range);
3020  Z3_sort args[2] = { d1, d2 };
3021  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
3022  check_error();
3023  return func_decl(*this, f);
3024  }
3025 
3026  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
3027  check_context(d1, range); check_context(d2, range); check_context(d3, range);
3028  Z3_sort args[3] = { d1, d2, d3 };
3029  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
3030  check_error();
3031  return func_decl(*this, f);
3032  }
3033 
3034  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
3035  check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range);
3036  Z3_sort args[4] = { d1, d2, d3, d4 };
3037  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
3038  check_error();
3039  return func_decl(*this, f);
3040  }
3041 
3042  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) {
3043  check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range); check_context(d5, range);
3044  Z3_sort args[5] = { d1, d2, d3, d4, d5 };
3045  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
3046  check_error();
3047  return func_decl(*this, f);
3048  }
3049 
3050  inline func_decl context::recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3051  array<Z3_sort> args(arity);
3052  for (unsigned i = 0; i < arity; i++) {
3053  check_context(domain[i], range);
3054  args[i] = domain[i];
3055  }
3056  Z3_func_decl f = Z3_mk_rec_func_decl(m_ctx, name, arity, args.ptr(), range);
3057  check_error();
3058  return func_decl(*this, f);
3059 
3060  }
3061 
3062  inline func_decl context::recfun(char const * name, unsigned arity, sort const * domain, sort const & range) {
3063  return recfun(str_symbol(name), arity, domain, range);
3064  }
3065 
3066  inline func_decl context::recfun(char const * name, sort const& d1, sort const & range) {
3067  return recfun(str_symbol(name), 1, &d1, range);
3068  }
3069 
3070  inline func_decl context::recfun(char const * name, sort const& d1, sort const& d2, sort const & range) {
3071  sort dom[2] = { d1, d2 };
3072  return recfun(str_symbol(name), 2, dom, range);
3073  }
3074 
3075  inline void context::recdef(func_decl f, expr_vector const& args, expr const& body) {
3076  check_context(f, args); check_context(f, body);
3077  array<Z3_ast> vars(args);
3078  Z3_add_rec_def(f.ctx(), f, vars.size(), vars.ptr(), body);
3079  }
3080 
3081  inline expr context::constant(symbol const & name, sort const & s) {
3082  Z3_ast r = Z3_mk_const(m_ctx, name, s);
3083  check_error();
3084  return expr(*this, r);
3085  }
3086  inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); }
3087  inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); }
3088  inline expr context::int_const(char const * name) { return constant(name, int_sort()); }
3089  inline expr context::real_const(char const * name) { return constant(name, real_sort()); }
3090  inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); }
3091  inline expr context::fpa_const(char const * name, unsigned ebits, unsigned sbits) { return constant(name, fpa_sort(ebits, sbits)); }
3092 
3093  template<size_t precision>
3094  inline expr context::fpa_const(char const * name) { return constant(name, fpa_sort<precision>()); }
3095 
3096  inline expr context::bool_val(bool b) { return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }
3097 
3098  inline expr context::int_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
3099  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); }
3100  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); }
3101  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); }
3102  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); }
3103 
3104  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); }
3105  inline expr context::real_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
3106  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); }
3107  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); }
3108  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); }
3109  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); }
3110 
3111  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); }
3112  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); }
3113  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); }
3114  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); }
3115  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); }
3116  inline expr context::bv_val(unsigned n, bool const* bits) {
3117  array<bool> _bits(n);
3118  for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
3119  Z3_ast r = Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error(); return expr(*this, r);
3120  }
3121 
3122  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); }
3123  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); }
3124 
3125  inline expr context::string_val(char const* s, unsigned n) { Z3_ast r = Z3_mk_lstring(m_ctx, n, s); check_error(); return expr(*this, r); }
3126  inline expr context::string_val(char const* s) { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
3127  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); }
3128 
3129  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); }
3130 
3131  inline expr func_decl::operator()(unsigned n, expr const * args) const {
3132  array<Z3_ast> _args(n);
3133  for (unsigned i = 0; i < n; i++) {
3134  check_context(*this, args[i]);
3135  _args[i] = args[i];
3136  }
3137  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
3138  check_error();
3139  return expr(ctx(), r);
3140 
3141  }
3142  inline expr func_decl::operator()(expr_vector const& args) const {
3143  array<Z3_ast> _args(args.size());
3144  for (unsigned i = 0; i < args.size(); i++) {
3145  check_context(*this, args[i]);
3146  _args[i] = args[i];
3147  }
3148  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
3149  check_error();
3150  return expr(ctx(), r);
3151  }
3152  inline expr func_decl::operator()() const {
3153  Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
3154  ctx().check_error();
3155  return expr(ctx(), r);
3156  }
3157  inline expr func_decl::operator()(expr const & a) const {
3158  check_context(*this, a);
3159  Z3_ast args[1] = { a };
3160  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3161  ctx().check_error();
3162  return expr(ctx(), r);
3163  }
3164  inline expr func_decl::operator()(int a) const {
3165  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
3166  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3167  ctx().check_error();
3168  return expr(ctx(), r);
3169  }
3170  inline expr func_decl::operator()(expr const & a1, expr const & a2) const {
3171  check_context(*this, a1); check_context(*this, a2);
3172  Z3_ast args[2] = { a1, a2 };
3173  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3174  ctx().check_error();
3175  return expr(ctx(), r);
3176  }
3177  inline expr func_decl::operator()(expr const & a1, int a2) const {
3178  check_context(*this, a1);
3179  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
3180  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3181  ctx().check_error();
3182  return expr(ctx(), r);
3183  }
3184  inline expr func_decl::operator()(int a1, expr const & a2) const {
3185  check_context(*this, a2);
3186  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
3187  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3188  ctx().check_error();
3189  return expr(ctx(), r);
3190  }
3191  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3) const {
3192  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
3193  Z3_ast args[3] = { a1, a2, a3 };
3194  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
3195  ctx().check_error();
3196  return expr(ctx(), r);
3197  }
3198  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const {
3199  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
3200  Z3_ast args[4] = { a1, a2, a3, a4 };
3201  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
3202  ctx().check_error();
3203  return expr(ctx(), r);
3204  }
3205  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const {
3206  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
3207  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
3208  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
3209  ctx().check_error();
3210  return expr(ctx(), r);
3211  }
3212 
3213  inline expr to_real(expr const & a) { Z3_ast r = Z3_mk_int2real(a.ctx(), a); a.check_error(); return expr(a.ctx(), r); }
3214 
3215  inline func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3216  return range.ctx().function(name, arity, domain, range);
3217  }
3218  inline func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range) {
3219  return range.ctx().function(name, arity, domain, range);
3220  }
3221  inline func_decl function(char const * name, sort const & domain, sort const & range) {
3222  return range.ctx().function(name, domain, range);
3223  }
3224  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range) {
3225  return range.ctx().function(name, d1, d2, range);
3226  }
3227  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
3228  return range.ctx().function(name, d1, d2, d3, range);
3229  }
3230  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
3231  return range.ctx().function(name, d1, d2, d3, d4, range);
3232  }
3233  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) {
3234  return range.ctx().function(name, d1, d2, d3, d4, d5, range);
3235  }
3236  inline func_decl function(char const* name, sort_vector const& domain, sort const& range) {
3237  return range.ctx().function(name, domain, range);
3238  }
3239  inline func_decl function(std::string const& name, sort_vector const& domain, sort const& range) {
3240  return range.ctx().function(name.c_str(), domain, range);
3241  }
3242 
3243  inline func_decl recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3244  return range.ctx().recfun(name, arity, domain, range);
3245  }
3246  inline func_decl recfun(char const * name, unsigned arity, sort const * domain, sort const & range) {
3247  return range.ctx().recfun(name, arity, domain, range);
3248  }
3249  inline func_decl recfun(char const * name, sort const& d1, sort const & range) {
3250  return range.ctx().recfun(name, d1, range);
3251  }
3252  inline func_decl recfun(char const * name, sort const& d1, sort const& d2, sort const & range) {
3253  return range.ctx().recfun(name, d1, d2, range);
3254  }
3255 
3256  inline expr select(expr const & a, expr const & i) {
3257  check_context(a, i);
3258  Z3_ast r = Z3_mk_select(a.ctx(), a, i);
3259  a.check_error();
3260  return expr(a.ctx(), r);
3261  }
3262  inline expr select(expr const & a, int i) {
3263  return select(a, a.ctx().num_val(i, a.get_sort().array_domain()));
3264  }
3265  inline expr select(expr const & a, expr_vector const & i) {
3266  check_context(a, i);
3267  array<Z3_ast> idxs(i);
3268  Z3_ast r = Z3_mk_select_n(a.ctx(), a, idxs.size(), idxs.ptr());
3269  a.check_error();
3270  return expr(a.ctx(), r);
3271  }
3272 
3273  inline expr store(expr const & a, expr const & i, expr const & v) {
3274  check_context(a, i); check_context(a, v);
3275  Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
3276  a.check_error();
3277  return expr(a.ctx(), r);
3278  }
3279 
3280  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); }
3281  inline expr store(expr const & a, expr i, int v) { return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
3282  inline expr store(expr const & a, int i, int v) {
3283  return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
3284  }
3285  inline expr store(expr const & a, expr_vector const & i, expr const & v) {
3286  check_context(a, i); check_context(a, v);
3287  array<Z3_ast> idxs(i);
3288  Z3_ast r = Z3_mk_store_n(a.ctx(), a, idxs.size(), idxs.ptr(), v);
3289  a.check_error();
3290  return expr(a.ctx(), r);
3291  }
3292 
3293  inline expr as_array(func_decl & f) {
3294  Z3_ast r = Z3_mk_as_array(f.ctx(), f);
3295  f.check_error();
3296  return expr(f.ctx(), r);
3297  }
3298 
3299 #define MK_EXPR1(_fn, _arg) \
3300  Z3_ast r = _fn(_arg.ctx(), _arg); \
3301  _arg.check_error(); \
3302  return expr(_arg.ctx(), r);
3303 
3304 #define MK_EXPR2(_fn, _arg1, _arg2) \
3305  check_context(_arg1, _arg2); \
3306  Z3_ast r = _fn(_arg1.ctx(), _arg1, _arg2); \
3307  _arg1.check_error(); \
3308  return expr(_arg1.ctx(), r);
3309 
3310  inline expr const_array(sort const & d, expr const & v) {
3311  MK_EXPR2(Z3_mk_const_array, d, v);
3312  }
3313 
3314  inline expr empty_set(sort const& s) {
3316  }
3317 
3318  inline expr full_set(sort const& s) {
3320  }
3321 
3322  inline expr set_add(expr const& s, expr const& e) {
3323  MK_EXPR2(Z3_mk_set_add, s, e);
3324  }
3325 
3326  inline expr set_del(expr const& s, expr const& e) {
3327  MK_EXPR2(Z3_mk_set_del, s, e);
3328  }
3329 
3330  inline expr set_union(expr const& a, expr const& b) {
3331  check_context(a, b);
3332  Z3_ast es[2] = { a, b };
3333  Z3_ast r = Z3_mk_set_union(a.ctx(), 2, es);
3334  a.check_error();
3335  return expr(a.ctx(), r);
3336  }
3337 
3338  inline expr set_intersect(expr const& a, expr const& b) {
3339  check_context(a, b);
3340  Z3_ast es[2] = { a, b };
3341  Z3_ast r = Z3_mk_set_intersect(a.ctx(), 2, es);
3342  a.check_error();
3343  return expr(a.ctx(), r);
3344  }
3345 
3346  inline expr set_difference(expr const& a, expr const& b) {
3348  }
3349 
3350  inline expr set_complement(expr const& a) {
3352  }
3353 
3354  inline expr set_member(expr const& s, expr const& e) {
3355  MK_EXPR2(Z3_mk_set_member, s, e);
3356  }
3357 
3358  inline expr set_subset(expr const& a, expr const& b) {
3359  MK_EXPR2(Z3_mk_set_subset, a, b);
3360  }
3361 
3362  // sequence and regular expression operations.
3363  // union is +
3364  // concat is overloaded to handle sequences and regular expressions
3365 
3366  inline expr empty(sort const& s) {
3367  Z3_ast r = Z3_mk_seq_empty(s.ctx(), s);
3368  s.check_error();
3369  return expr(s.ctx(), r);
3370  }
3371  inline expr suffixof(expr const& a, expr const& b) {
3372  check_context(a, b);
3373  Z3_ast r = Z3_mk_seq_suffix(a.ctx(), a, b);
3374  a.check_error();
3375  return expr(a.ctx(), r);
3376  }
3377  inline expr prefixof(expr const& a, expr const& b) {
3378  check_context(a, b);
3379  Z3_ast r = Z3_mk_seq_prefix(a.ctx(), a, b);
3380  a.check_error();
3381  return expr(a.ctx(), r);
3382  }
3383  inline expr indexof(expr const& s, expr const& substr, expr const& offset) {
3384  check_context(s, substr); check_context(s, offset);
3385  Z3_ast r = Z3_mk_seq_index(s.ctx(), s, substr, offset);
3386  s.check_error();
3387  return expr(s.ctx(), r);
3388  }
3389  inline expr last_indexof(expr const& s, expr const& substr) {
3390  check_context(s, substr);
3391  Z3_ast r = Z3_mk_seq_last_index(s.ctx(), s, substr);
3392  s.check_error();
3393  return expr(s.ctx(), r);
3394  }
3395  inline expr to_re(expr const& s) {
3397  }
3398  inline expr in_re(expr const& s, expr const& re) {
3399  MK_EXPR2(Z3_mk_seq_in_re, s, re);
3400  }
3401  inline expr plus(expr const& re) {
3402  MK_EXPR1(Z3_mk_re_plus, re);
3403  }
3404  inline expr option(expr const& re) {
3406  }
3407  inline expr star(expr const& re) {
3408  MK_EXPR1(Z3_mk_re_star, re);
3409  }
3410  inline expr re_empty(sort const& s) {
3411  Z3_ast r = Z3_mk_re_empty(s.ctx(), s);
3412  s.check_error();
3413  return expr(s.ctx(), r);
3414  }
3415  inline expr re_full(sort const& s) {
3416  Z3_ast r = Z3_mk_re_full(s.ctx(), s);
3417  s.check_error();
3418  return expr(s.ctx(), r);
3419  }
3420  inline expr re_intersect(expr_vector const& args) {
3421  assert(args.size() > 0);
3422  context& ctx = args[0].ctx();
3423  array<Z3_ast> _args(args);
3424  Z3_ast r = Z3_mk_re_intersect(ctx, _args.size(), _args.ptr());
3425  ctx.check_error();
3426  return expr(ctx, r);
3427  }
3428  inline expr re_complement(expr const& a) {
3430  }
3431  inline expr range(expr const& lo, expr const& hi) {
3432  check_context(lo, hi);
3433  Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
3434  lo.check_error();
3435  return expr(lo.ctx(), r);
3436  }
3437 
3438 
3439 
3440 
3441 
3442  inline expr_vector context::parse_string(char const* s) {
3443  Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0);
3444  check_error();
3445  return expr_vector(*this, r);
3446 
3447  }
3448  inline expr_vector context::parse_file(char const* s) {
3449  Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0);
3450  check_error();
3451  return expr_vector(*this, r);
3452  }
3453 
3454  inline expr_vector context::parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls) {
3455  array<Z3_symbol> sort_names(sorts.size());
3456  array<Z3_symbol> decl_names(decls.size());
3457  array<Z3_sort> sorts1(sorts);
3458  array<Z3_func_decl> decls1(decls);
3459  for (unsigned i = 0; i < sorts.size(); ++i) {
3460  sort_names[i] = sorts[i].name();
3461  }
3462  for (unsigned i = 0; i < decls.size(); ++i) {
3463  decl_names[i] = decls[i].name();
3464  }
3465 
3466  Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
3467  check_error();
3468  return expr_vector(*this, r);
3469  }
3470 
3471  inline expr_vector context::parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls) {
3472  array<Z3_symbol> sort_names(sorts.size());
3473  array<Z3_symbol> decl_names(decls.size());
3474  array<Z3_sort> sorts1(sorts);
3475  array<Z3_func_decl> decls1(decls);
3476  for (unsigned i = 0; i < sorts.size(); ++i) {
3477  sort_names[i] = sorts[i].name();
3478  }
3479  for (unsigned i = 0; i < decls.size(); ++i) {
3480  decl_names[i] = decls[i].name();
3481  }
3482  Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
3483  check_error();
3484  return expr_vector(*this, r);
3485  }
3486 
3487 
3488  inline expr expr::substitute(expr_vector const& src, expr_vector const& dst) {
3489  assert(src.size() == dst.size());
3490  array<Z3_ast> _src(src.size());
3491  array<Z3_ast> _dst(dst.size());
3492  for (unsigned i = 0; i < src.size(); ++i) {
3493  _src[i] = src[i];
3494  _dst[i] = dst[i];
3495  }
3496  Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
3497  check_error();
3498  return expr(ctx(), r);
3499  }
3500 
3501  inline expr expr::substitute(expr_vector const& dst) {
3502  array<Z3_ast> _dst(dst.size());
3503  for (unsigned i = 0; i < dst.size(); ++i) {
3504  _dst[i] = dst[i];
3505  }
3506  Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
3507  check_error();
3508  return expr(ctx(), r);
3509  }
3510 
3511 
3512 
3513 }
3514 
3517 #undef Z3_THROW
3518 #endif
3519 
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:2504
Definition: z3++.h:134
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:2057
expr mod(expr const &a, expr const &b)
Definition: z3++.h:1273
friend expr mk_or(expr_vector const &args)
Definition: z3++.h:2110
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.
expr bvadd_no_overflow(expr const &a, expr const &b, bool is_signed)
bit-vector overflow/underflow checks
Definition: z3++.h:1778
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:147
bool is_numeral_u(unsigned &i) const
Definition: z3++.h:743
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:1569
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.
std::string reason_unknown() const
Definition: z3++.h:2371
std::string help() const
Definition: z3++.h:2621
sort bool_sort()
Return the Boolean sort.
Definition: z3++.h:2908
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:2032
void check_parser_error() const
Definition: z3++.h:185
friend expr operator+(expr const &a, expr const &b)
Definition: z3++.h:1357
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:2249
expr mk_and(expr_vector const &args)
Definition: z3++.h:2116
friend expr pw(expr const &a, expr const &b)
Definition: z3++.h:1269
bool operator!=(cube_iterator const &other)
Definition: z3++.h:2472
bool is_numeral_i64(int64_t &i) const
Definition: z3++.h:740
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.
void set(char const *k, bool v)
Definition: z3++.h:2321
iterator(iterator const &other)
Definition: z3++.h:1897
model(context &c)
Definition: z3++.h:2186
friend expr bv2int(expr const &a, bool is_signed)
bit-vector and integer conversions.
Definition: z3++.h:1772
bool is_int() const
Return true if this sort is the Integer sort.
Definition: z3++.h:548
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:1913
tactic & operator=(tactic const &s)
Definition: z3++.h:2604
expr operator[](expr const &index) const
Definition: z3++.h:1221
sort re_sort(sort &seq_sort)
Return a regular expression sort over sequences seq_sort.
Definition: z3++.h:2914
expr sle(expr const &a, expr const &b)
signed less than or equal to operator for bitvectors.
Definition: z3++.h:1680
void add_fact(func_decl &f, unsigned *args)
Definition: z3++.h:2854
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:2687
void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g)
Erase all formulas from the given goal.
expr pbeq(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:2024
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:1575
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.
probe & operator=(probe const &s)
Definition: z3++.h:2691
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_decl get_const_decl(unsigned i) const
Definition: z3++.h:2212
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:2865
std::string documentation(symbol const &s)
Definition: z3++.h:452
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.
Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c, Z3_func_decl f)
create transitive closure of binary relation.
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:2929
friend expr operator>=(expr const &a, expr const &b)
Definition: z3++.h:1411
#define Z3_THROW(x)
Definition: z3++.h:96
bool is_array() const
Return true if this is a Array expression.
Definition: z3++.h:702
unsigned id() const
retrieve unique identifier for expression.
Definition: z3++.h:802
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.
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:2905
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:1767
bool operator==(cube_iterator const &other)
Definition: z3++.h:2469
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:475
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. The sequence is empty if the index is...
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...
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:510
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...
func_decl piecewise_linear_order(sort const &a, unsigned index)
Definition: z3++.h:1815
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:2326
expr contains(expr const &s)
Definition: z3++.h:1169
friend expr bvmul_no_overflow(expr const &a, expr const &b, bool is_signed)
Definition: z3++.h:1796
expr length() const
Definition: z3++.h:1187
expr bvsub_no_underflow(expr const &a, expr const &b, bool is_signed)
Definition: z3++.h:1787
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.
stats statistics() const
Definition: z3++.h:2372
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:2898
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
friend expr bvadd_no_underflow(expr const &a, expr const &b)
Definition: z3++.h:1781
solver(context &c, simple)
Definition: z3++.h:2306
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:669
char const * msg() const
Definition: z3++.h:87
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:3431
expr bv_val(int n, unsigned sz)
Definition: z3++.h:3111
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:1347
expr value() const
Definition: z3++.h:2142
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.
friend expr bvsub_no_underflow(expr const &a, expr const &b, bool is_signed)
Definition: z3++.h:1787
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...
bool is_real() const
Return true if this is a real expression.
Definition: z3++.h:690
Definition: z3_api.h:1365
func_interp & operator=(func_interp const &s)
Definition: z3++.h:2158
friend expr operator!=(expr const &a, expr const &b)
Definition: z3++.h:1347
iterator & operator++()
Definition: z3++.h:1906
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...
probe(context &c, double val)
Definition: z3++.h:2686
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 itos() const
Definition: z3++.h:1197
std::string help() const
Definition: z3++.h:2841
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:2135
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
expr_vector units() const
Definition: z3++.h:2376
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:2325
expr fma(expr const &a, expr const &b, expr const &c, expr const &rm)
Definition: z3++.h:1631
tactic when(probe const &p, tactic const &t)
Definition: z3++.h:2892
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:2172
config()
Definition: z3++.h:108
friend std::ostream & operator<<(std::ostream &out, params const &p)
Definition: z3++.h:480
void set(char const *k, double n)
Definition: z3++.h:474
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:2825
cube_generator cubes()
Definition: z3++.h:2503
bool is_numeral_u64(uint64_t &i) const
Definition: z3++.h:741
friend expr operator/(expr const &a, expr const &b)
Definition: z3++.h:1428
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:388
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 ...
A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort.
Definition: z3++.h:516
~solver()
Definition: z3++.h:2311
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. The result is the new AST. The arrays from and to must have size num_exprs. For every i smaller than num_exprs, we must have that sort of from[i] must be equal to sort of to[i].
expr simplify() const
Return a simplified version of this expression.
Definition: z3++.h:1236
unsigned bv_size() const
Return the size of this Bit-vector sort.
Definition: z3++.h:595
bool is_bv() const
Return true if this sort is a Bit-vector sort.
Definition: z3++.h:560
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:2766
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:620
int to_int() const
Definition: z3++.h:421
friend expr operator^(expr const &a, expr const &b)
Definition: z3++.h:1565
~array()
Definition: z3++.h:391
expr full_set(sort const &s)
Definition: z3++.h:3318
model(model &src, context &dst, translate)
Definition: z3++.h:2189
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.
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:506
Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem)
Remove an element to a set.
bool is_true() const
Definition: z3++.h:1021
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.
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:2911
void interrupt()
Interrupt the current procedure being executed by any object managed by this context. This is a soft interruption: there is no guarantee the object will actually stop.
Definition: z3++.h:221
bool is_double(unsigned i) const
Definition: z3++.h:2280
expr lshr(expr const &a, expr const &b)
logic shift right operator for bitvectors
Definition: z3++.h:1753
expr udiv(expr const &a, expr const &b)
unsigned division operator for bitvectors.
Definition: z3++.h:1718
apply_result operator()(goal const &g) const
Definition: z3++.h:2618
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
solver mk_solver() const
Definition: z3++.h:2611
friend expr concat(expr const &a, expr const &b)
Definition: z3++.h:2066
friend expr mod(expr const &a, expr const &b)
Definition: z3++.h:1273
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.
Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflo...
expr upper(handle const &h)
Definition: z3++.h:2830
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1400
Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s)
Convert a solver into a DIMACS formatted string.
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1363
goal(context &c, Z3_goal s)
Definition: z3++.h:2517
void push_back(T const &e)
Definition: z3++.h:1868
optimize & operator=(optimize const &o)
Definition: z3++.h:2770
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:453
expr eval(expr const &n, bool model_completion=false) const
Definition: z3++.h:2200
model(context &c, Z3_model m)
Definition: z3++.h:2187
Z3_ast_kind kind() const
Definition: z3++.h:495
sort array_sort(sort d, sort r)
Return an array sort for arrays from d to r.
Definition: z3++.h:2942
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:3081
void pop()
Definition: z3++.h:2807
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.
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)
Return the number of parameters associated with a declaration.
func_decl operator[](int i) const
Definition: z3++.h:2215
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:2855
bool is_ite() const
Definition: z3++.h:1029
unsigned fpa_sbits() const
Definition: z3++.h:599
#define _Z3_MK_UN_(a, mkun)
Definition: z3++.h:1301
fixedpoint(context &c)
Definition: z3++.h:2848
Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than or equal to.
expr_vector const & operator*() const
Definition: z3++.h:2467
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 ...
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:2601
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:1325
sort fpa_rounding_mode()
Return a RoundingMode sort.
Definition: z3++.h:920
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:2689
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...
bool is_datatype() const
Return true if this is a Datatype expression.
Definition: z3++.h:706
void add(expr const &e, expr const &t)
Definition: z3++.h:2789
Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d)
Return declaration kind corresponding to declaration.
expr rotate_right(unsigned i)
Definition: z3++.h:1133
~tactic()
Definition: z3++.h:2602
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:1842
check_result check()
Definition: z3++.h:2810
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:2748
expr is_int(expr const &e)
Definition: z3++.h:1309
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.
friend expr bvadd_no_overflow(expr const &a, expr const &b, bool is_signed)
bit-vector overflow/underflow checks
Definition: z3++.h:1778
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:1565
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:2843
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)
Create the constant array.
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:2840
unsigned lo() const
Definition: z3++.h:1141
Exception used to sign API usage errors.
Definition: z3++.h:83
expr operator*(expr const &a, expr const &b)
Definition: z3++.h:1387
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.
unsigned uint_value(unsigned i) const
Definition: z3++.h:2281
unsigned Z3_API Z3_get_sort_id(Z3_context c, Z3_sort s)
Return a unique identifier for s.
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. However, in the context returned by this function, the user is responsible for managing Z3_ast reference counters. Managing reference counters is a burden and error-prone, but allows the user to use the memory more efficiently. The user must invoke Z3_inc_ref for any Z3_ast returned by Z3, and Z3_dec_ref whenever the Z3_ast is not needed anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD.
Definition: z3++.h:136
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.
expr nth(expr const &index) const
Definition: z3++.h:1181
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...
A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort ...
Definition: z3++.h:667
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.
expr operator!(expr const &a)
Definition: z3++.h:1307
expr set_subset(expr const &a, expr const &b)
Definition: z3++.h:3358
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:3304
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:672
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
unsigned num_exprs() const
Definition: z3++.h:2536
bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g)
Return true if the given goal contains the formula false.
bool is_uint(unsigned i) const
Definition: z3++.h:2279
expr ule(expr const &a, expr const &b)
unsigned less than or equal to operator for bitvectors.
Definition: z3++.h:1694
expr in_re(expr const &s, expr const &re)
Definition: z3++.h:3398
symbol name(unsigned i)
Definition: z3++.h:450
void recdef(func_decl, expr_vector const &args, expr const &body)
Definition: z3++.h:3075
void Z3_API Z3_ast_vector_resize(Z3_context c, Z3_ast_vector v, unsigned n)
Resize the AST vector v.
expr_vector unsat_core() const
Definition: z3++.h:2373
iterator begin() const
Definition: z3++.h:1917
bool is_lambda() const
Return true if this expression is a lambda expression.
Definition: z3++.h:771
Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s)
Return the length of the sequence s.
bool is_fpa() const
Return true if this is a FloatingPoint expression. .
Definition: z3++.h:732
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.
Definition: z3++.h:130
Z3_error_code check_error() const
Definition: z3++.h:407
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:447
friend expr mk_and(expr_vector const &args)
Definition: z3++.h:2116
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.
unsigned num_entries() const
Definition: z3++.h:2166
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:2498
unsigned arity() const
Definition: z3++.h:631
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:2864
bool enable_exceptions() const
Definition: z3++.h:198
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...
bool is_finite_domain() const
Return true if this sort is a Finite domain sort.
Definition: z3++.h:584
Z3_ast Z3_API Z3_mk_seq_nth(Z3_context c, Z3_ast s, Z3_ast index)
Retrieve from s the element positioned at position index. The function is under-specified if the inde...
func_decl operator()(context &c, Z3_ast a)
Definition: z3++.h:1850
ast_vector_tpl(ast_vector_tpl const &s)
Definition: z3++.h:1863
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:2880
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:2265
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:1411
std::string reason_unknown()
Definition: z3++.h:2863
expr replace(expr const &src, expr const &dst) const
Definition: z3++.h:1158
void add_entry(expr_vector const &args, expr &value)
Definition: z3++.h:2168
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.
expr pw(expr const &a, expr const &b)
Definition: z3++.h:1269
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:2566
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...
friend probe operator>=(probe const &p1, probe const &p2)
Definition: z3++.h:2725
expr(context &c, Z3_ast n)
Definition: z3++.h:670
~goal()
Definition: z3++.h:2519
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:3346
symbol name() const
Return name of sort.
Definition: z3++.h:540
T * operator->() const
Definition: z3++.h:1914
unsigned Z3_API Z3_ast_vector_size(Z3_context c, Z3_ast_vector v)
Return the size of the given AST vector.
bool is_and() const
Definition: z3++.h:1024
unsigned id() const
retrieve unique identifier for func_decl.
Definition: z3++.h:629
expr operator~(expr const &a)
Definition: z3++.h:1629
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.
expr operator[](int i) const
Definition: z3++.h:2531
bool empty() const
Definition: z3++.h:1872
Z3_ast Z3_API Z3_mk_fpa_rtn(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode...
expr_vector assertions() const
Definition: z3++.h:2874
friend expr int2bv(unsigned n, expr const &a)
Definition: z3++.h:1773
expr_vector assertions() const
Definition: z3++.h:2835
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.
expr_vector unsat_core() const
Definition: z3++.h:2823
friend expr operator-(expr const &a)
Definition: z3++.h:1450
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:2057
check_result check(unsigned n, expr *const assumptions)
Definition: z3++.h:2344
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.
expr rem(expr const &a, expr const &b)
Definition: z3++.h:1289
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.
friend expr operator*(expr const &a, expr const &b)
Definition: z3++.h:1387
probe(context &c, char const *name)
Definition: z3++.h:2685
friend std::ostream & operator<<(std::ostream &out, solver const &s)
Definition: z3++.h:2507
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:2862
Z3_sort Z3_API Z3_mk_string_sort(Z3_context c)
Create a sort for 8 bit strings.
~stats()
Definition: z3++.h:2268
bool is_forall() const
Return true if this expression is a universal quantifier.
Definition: z3++.h:763
friend expr min(expr const &a, expr const &b)
Definition: z3++.h:1576
sort seq_sort(sort &s)
Return a sequence sort over base sort s.
Definition: z3++.h:2913
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.
friend expr bvmul_no_underflow(expr const &a, expr const &b)
Definition: z3++.h:1799
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:1492
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 bvmul_no_underflow(expr const &a, expr const &b)
Definition: z3++.h:1799
expr get_const_interp(func_decl c) const
Definition: z3++.h:2223
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:484
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.
Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.
expr set_add(expr const &s, expr const &e)
Definition: z3++.h:3322
expr ashr(expr const &a, expr const &b)
arithmetic shift right operator for bitvectors
Definition: z3++.h:1760
expr re_empty(sort const &s)
Definition: z3++.h:3410
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).
void Z3_API Z3_optimize_assert_and_track(Z3_context c, Z3_optimize o, Z3_ast a, Z3_ast t)
Assert tracked hard constraint to the optimization context.
friend tactic operator|(tactic const &t1, tactic const &t2)
Definition: z3++.h:2639
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
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:1240
expr nor(expr const &a, expr const &b)
Definition: z3++.h:1574
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.
unsigned size() const
Definition: z3++.h:1866
Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c)
Return the parameter description set for the simplify procedure.
solver(context &c, Z3_solver s)
Definition: z3++.h:2307
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
solver & operator=(solver const &s)
Definition: z3++.h:2313
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:2871
expr substitute(expr_vector const &src, expr_vector const &dst)
Apply substitution. Replace src expressions by dst.
Definition: z3++.h:3488
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.
ast(context &c, Z3_ast n)
Definition: z3++.h:489
expr_vector cube(expr_vector &vars, unsigned cutoff)
Definition: z3++.h:2416
expr operator<=(expr const &a, expr const &b)
Definition: z3++.h:1492
handle add(expr const &e, char const *weight)
Definition: z3++.h:2794
friend std::ostream & operator<<(std::ostream &out, apply_result const &r)
Definition: z3++.h:2590
bool is_finite_domain() const
Return true if this is a Finite-domain expression.
Definition: z3++.h:728
expr proof() const
Definition: z3++.h:2388
void set(char const *k, char const *s)
Definition: z3++.h:476
expr bv_const(char const *name, unsigned sz)
Definition: z3++.h:3090
sort fpa_sort()
Definition: z3++.h:2918
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.
T back() const
Definition: z3++.h:1870
expr string_val(char const *s)
Definition: z3++.h:3126
uint64_t get_numeral_uint64() const
Return uint64_t value of numeral, throw if result cannot fit in uint64_t.
Definition: z3++.h:867
tactic(context &c, char const *name)
Definition: z3++.h:2599
ast_vector_tpl & set(unsigned idx, ast &a)
Definition: z3++.h:1880
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:2912
std::string str() const
Definition: z3++.h:420
tactic with(tactic const &t, params const &p)
Definition: z3++.h:2652
expr empty_set(sort const &s)
Definition: z3++.h:3314
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:3293
expr plus(expr const &re)
Definition: z3++.h:3401
func_decl partial_order(sort const &a, unsigned index)
Definition: z3++.h:1812
expr xnor(expr const &a, expr const &b)
Definition: z3++.h:1575
void reset()
Definition: z3++.h:2328
Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1)
Coerce an integer to a real.
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.
void resize(unsigned sz)
Definition: z3++.h:1869
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:793
~config()
Definition: z3++.h:109
void from_string(char const *s)
Definition: z3++.h:2341
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
sort array_domain() const
Return the domain of this Array sort.
Definition: z3++.h:605
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:177
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:2040
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_...
func_entry(context &c, Z3_func_entry e)
Definition: z3++.h:2131
void Z3_API Z3_del_config(Z3_config c)
Delete the given configuration object.
bool is_var() const
Return true if this expression is a variable.
Definition: z3++.h:776
ast_vector_tpl(context &c)
Definition: z3++.h:1861
expr extract(unsigned hi, unsigned lo) const
Definition: z3++.h:1140
model get_model() const
Definition: z3++.h:2545
expr operator[](expr_vector const &index) const
Definition: z3++.h:1229
void add(expr const &e, char const *p)
Definition: z3++.h:2335
func_decl to_func_decl(context &c, Z3_func_decl f)
Definition: z3++.h:1672
unsigned depth() const
Definition: z3++.h:2534
ast_vector_tpl(context &c, Z3_ast_vector v)
Definition: z3++.h:1862
optimize(context &c)
Definition: z3++.h:2765
expr min(expr const &a, expr const &b)
Definition: z3++.h:1576
context & ctx() const
Definition: z3++.h:406
sort array_range() const
Return the range of this Array sort.
Definition: z3++.h:611
cube_iterator(solver &s, expr_vector &vars, unsigned &cutoff, bool end)
Definition: z3++.h:2443
param_descrs(param_descrs const &o)
Definition: z3++.h:438
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].
expr(expr const &n)
Definition: z3++.h:671
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:2124
bool is_const() const
Definition: z3++.h:641
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:2343
unsigned size() const
Definition: z3++.h:2586
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:2391
iterator end() const
Definition: z3++.h:1918
unsigned get_numeral_uint() const
Return uint value of numeral, throw if result cannot fit in machine uint.
Definition: z3++.h:833
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...
func_decl get_func_decl(unsigned i) const
Definition: z3++.h:2213
expr operator+(expr const &a, expr const &b)
Definition: z3++.h:1357
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2979
expr operator()(context &c, Z3_ast a)
Definition: z3++.h:1831
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.
friend probe operator!(probe const &p)
Definition: z3++.h:2751
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.
expr as_expr() const
Definition: z3++.h:2550
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:739
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3050
expr bvadd_no_underflow(expr const &a, expr const &b)
Definition: z3++.h:1781
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.
expr int2bv(unsigned n, expr const &a)
Definition: z3++.h:1773
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...
expr bvneg_no_overflow(expr const &a)
Definition: z3++.h:1793
func_decl tree_order(sort const &a, unsigned index)
Definition: z3++.h:1818
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...
expr re_complement(expr const &a)
Definition: z3++.h:3428
model convert_model(model const &m) const
Definition: z3++.h:2539
unsigned h() const
Definition: z3++.h:2763
expr srem(expr const &a, expr const &b)
signed remainder operator for bitvectors
Definition: z3++.h:1725
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 operator&(expr const &a, expr const &b)
Definition: z3++.h:1561
expr set_intersect(expr const &a, expr const &b)
Definition: z3++.h:3338
void from_string(char const *s)
Definition: z3++.h:2851
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.
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:2310
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.
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:99
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:2777
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:1591
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:3091
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 select(expr const &a, expr const &i)
forward declarations
Definition: z3++.h:3256
expr re_intersect(expr_vector const &args)
Definition: z3++.h:3420
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:3104
ast_vector_tpl< sort > sort_vector
Definition: z3++.h:72
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:2779
bool operator==(iterator const &other) const
Definition: z3++.h:1900
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:3377
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:2155
Z3_decl_kind decl_kind() const
Definition: z3++.h:635
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:2192
void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m)
Decrement the reference counter of the given model.
expr operator%(expr const &a, expr const &b)
Definition: z3++.h:1284
expr_vector parse_file(char const *file)
Definition: z3++.h:3448
Z3_func_decl Z3_API Z3_mk_piecewise_linear_order(Z3_context c, Z3_sort a, unsigned id)
create a piecewise linear ordering relation over signature a and index id.
Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s)
Retrieve the string constant stored in s.
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:2671
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:1338
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:1207
stats statistics() const
Definition: z3++.h:2837
func_entry entry(unsigned i) const
Definition: z3++.h:2167
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:2329
void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d)
Decrement the reference counter of the given fixedpoint context.
bool is_relation() const
Return true if this is a Relation expression.
Definition: z3++.h:710
Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow...
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:1134
bool is_bool() const
Return true if this sort is the Boolean sort.
Definition: z3++.h:544
void resize(unsigned sz)
Definition: z3++.h:392
expr ugt(expr const &a, expr const &b)
unsigned greater than operator for bitvectors.
Definition: z3++.h:1712
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:2521
expr option(expr const &re)
Definition: z3++.h:3404
~params()
Definition: z3++.h:463
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, this function returns the sort of the first dimension.
expr const_array(sort const &d, expr const &v)
Definition: z3++.h:3310
stats(stats const &s)
Definition: z3++.h:2267
T const * ptr() const
Definition: z3++.h:396
cube_iterator operator++(int)
Definition: z3++.h:2465
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f)
Retrieve set of rules from fixedpoint context.
expr set_member(expr const &s, expr const &e)
Definition: z3++.h:3354
Z3_model Z3_API Z3_mk_model(Z3_context c)
Create a fresh model object. It has reference count 0.
unsigned id() const
retrieve unique identifier for func_decl.
Definition: z3++.h:527
bool is_distinct() const
Definition: z3++.h:1030
friend std::ostream & operator<<(std::ostream &out, model const &m)
Definition: z3++.h:2256
bool is_or() const
Definition: z3++.h:1025
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.
bool is_not() const
Definition: z3++.h:1023
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:2133
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)
Decrement the reference counter of the given optimize context.
sort uninterpreted_sort(char const *name)
create an uninterpreted sort with the name given by the string or symbol.
Definition: z3++.h:2971
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...
goal operator[](int i) const
Definition: z3++.h:2587
check_result check(expr_vector const &assumptions)
Definition: z3++.h:2354
unsigned fpa_ebits() const
Definition: z3++.h:597
expr_vector trail() const
Definition: z3++.h:2377
void reset()
Definition: z3++.h:2535
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows divisor).
bool is_numeral(double &d) const
Definition: z3++.h:746
T * ptr()
Definition: z3++.h:397
bool is_implies() const
Definition: z3++.h:1027
params(params const &s)
Definition: z3++.h:462
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.
expr bv2int(expr const &a, bool is_signed)
bit-vector and integer conversions.
Definition: z3++.h:1772
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
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:2798
unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m)
Return the number of function interpretations in the given model.
Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1)
Create an n bit bit-vector from the integer argument t1.
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:934
bool is_seq() const
Return true if this is a sequence expression.
Definition: z3++.h:714
std::string dimacs() const
Definition: z3++.h:2411
Z3_param_kind
The different kinds of parameters that can be associated with parameter sets. (see Z3_mk_params)...
Definition: z3_api.h:1322
friend expr bvsdiv_no_overflow(expr const &a, expr const &b)
Definition: z3++.h:1790
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:2720
friend expr operator&&(expr const &a, expr const &b)
Return an expression representing a and b.
Definition: z3++.h:1313
expr get_cover_delta(int level, func_decl &p)
Definition: z3++.h:2866
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 int_const(char const *name)
Definition: z3++.h:3088
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 expr operator&(expr const &a, expr const &b)
Definition: z3++.h:1561
friend std::ostream & operator<<(std::ostream &out, exception const &e)
Definition: z3++.h:90
expr arg(unsigned i) const
Definition: z3++.h:2144
expr abs(expr const &a)
Definition: z3++.h:1606
symbol(symbol const &s)
Definition: z3++.h:416
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...
unsigned num_args() const
Return the number of arguments in this application. This method assumes the expression is an applicat...
Definition: z3++.h:941
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:113
expr sum(expr_vector const &args)
Definition: z3++.h:2048
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:518
Z3_string Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned *length)
Retrieve the unescaped string constant stored in s.
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)
Retrieve the model for the last Z3_optimize_check.
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:2516
expr suffixof(expr const &a, expr const &b)
Definition: z3++.h:3371
void from_file(char const *filename)
Definition: z3++.h:2839
void Z3_API Z3_interrupt(Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers...
expr_vector const * operator->() const
Definition: z3++.h:2466
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:2366
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:750
friend tactic operator&(tactic const &t1, tactic const &t2)
Definition: z3++.h:2632
expr operator<(expr const &a, expr const &b)
Definition: z3++.h:1517
object(context &c)
Definition: z3++.h:404
friend expr operator>(expr const &a, expr const &b)
Definition: z3++.h:1539
unsigned size() const
Definition: z3++.h:2530
Z3_func_decl Z3_API Z3_mk_tree_order(Z3_context c, Z3_sort a, unsigned id)
create a tree ordering relation over signature a identified using index id.
handle add(expr const &e, unsigned weight)
Definition: z3++.h:2783
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:488
Z3_symbol_kind kind() const
Definition: z3++.h:419
object(object const &s)
Definition: z3++.h:405
friend expr nand(expr const &a, expr const &b)
Definition: z3++.h:1573
void set(params const &p)
Definition: z3++.h:2876
expr atleast(expr_vector const &es, unsigned bound)
Definition: z3++.h:2040
friend tactic with(tactic const &t, params const &p)
Definition: z3++.h:2652
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow...
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:3089
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.
Z3_func_decl Z3_API Z3_mk_partial_order(Z3_context c, Z3_sort a, unsigned id)
create a partial ordering relation over signature a and index id.
sort(context &c, Z3_ast a)
Definition: z3++.h:520
stats statistics() const
Definition: z3++.h:2872
model get_model() const
Definition: z3++.h:2822
func_interp get_func_interp(func_decl f) const
Definition: z3++.h:2229
friend probe operator==(probe const &p1, probe const &p2)
Definition: z3++.h:2740
Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast t1, bool is_signed)
Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is t...
bool is_numeral(std::string &s, unsigned precision) const
Definition: z3++.h:745
Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1)
Repeat the given bit-vector up length i.
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. ...
bool is_eq() const
Definition: z3++.h:1028
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_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t1)
Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector...
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.
Z3_sort_kind sort_kind() const
Return the internal sort kind.
Definition: z3++.h:536
bool is_numeral(std::string &s) const
Definition: z3++.h:744
bool is_arith() const
Return true if this sort is the Integer or Real sort.
Definition: z3++.h:556
Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re)
Create the regular language re*.
Definition: z3++.h:135
expr sext(expr const &a, unsigned i)
Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector.
Definition: z3++.h:1807
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:2340
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...
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:2024
expr at(expr const &index) const
Definition: z3++.h:1175
unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t)
Return a unique identifier for t. The identifier is unique up to structural equality. Thus, two ast nodes created by the same context and having the same children and same function symbols have the same identifiers. Ast nodes created in the same context, but having different children or different functions have different identifiers. Variables and quantifiers are also assigned different identifiers according to their structure.
void add(expr_vector const &v)
Definition: z3++.h:2529
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.
expr_vector trail(array< unsigned > &levels) const
Definition: z3++.h:2378
Z3_ast Z3_API Z3_mk_fpa_rna(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode...
expr empty(sort const &s)
Definition: z3++.h:3366
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.
bool is_well_sorted() const
Return true if this expression is well sorted (aka type correct).
Definition: z3++.h:785
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...
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:417
~model()
Definition: z3++.h:2190
cube_generator(solver &s, expr_vector &vars)
Definition: z3++.h:2491
friend tactic par_and_then(tactic const &t1, tactic const &t2)
Definition: z3++.h:2671
sort real_sort()
Return the Real sort.
Definition: z3++.h:2910
void set(char const *k, unsigned v)
Definition: z3++.h:2322
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.
expr re_full(sort const &s)
Definition: z3++.h:3415
Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d)
Return the range of the given declaration.
bool inconsistent() const
Definition: z3++.h:2533
bool is_const() const
Return true if this expression is a constant (i.e., an application with 0 arguments).
Definition: z3++.h:754
expr arg(unsigned i) const
Return the i-th argument of this application. This method assumes the expression is an application...
Definition: z3++.h:949
friend expr rem(expr const &a, expr const &b)
Definition: z3++.h:1289
expr num_val(int n, sort const &s)
Definition: z3++.h:3129
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:510
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.
unsigned num_consts() const
Definition: z3++.h:2210
symbol int_symbol(int n)
Create a Z3 symbol based on the given integer.
Definition: z3++.h:2906
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:1212
expr fpa_val(double n)
Definition: z3++.h:3122
func_decl transitive_closure(func_decl const &)
Definition: z3++.h:637
expr bvmul_no_overflow(expr const &a, expr const &b, bool is_signed)
Definition: z3++.h:1796
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:2735
expr indexof(expr const &s, expr const &substr, expr const &offset)
Definition: z3++.h:3383
void from_file(char const *s)
Definition: z3++.h:2852
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:3350
unsigned num_funcs() const
Definition: z3++.h:2211
bool is_algebraic() const
Return true if expression is an algebraic number.
Definition: z3++.h:780
expr operator()() const
Definition: z3++.h:3152
expr_vector non_units() const
Definition: z3++.h:2375
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:439
expr operator>(expr const &a, expr const &b)
Definition: z3++.h:1539
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].
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:141
expr star(expr const &re)
Definition: z3++.h:3407
std::string get_escaped_string() const
for a string value expression return an escaped or unescaped string value.
Definition: z3++.h:902
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:1629
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:1338
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:3299
param_descrs(context &c, Z3_param_descrs d)
Definition: z3++.h:437
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:2646
expr operator|(expr const &a, expr const &b)
Definition: z3++.h:1569
friend std::ostream & operator<<(std::ostream &out, ast_vector_tpl const &v)
Definition: z3++.h:1919
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...
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.
friend tactic par_or(unsigned n, tactic const *tactics)
Definition: z3++.h:2662
expr pbge(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:2016
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:1606
tactic(context &c, Z3_tactic s)
Definition: z3++.h:2600
void check_context(object const &a, object const &b)
Definition: z3++.h:410
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.
Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.
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:3087
expr urem(expr const &a, expr const &b)
unsigned reminder operator for bitvectors
Definition: z3++.h:1739
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.
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.
expr operator&&(expr const &a, expr const &b)
Definition: z3++.h:1313
double apply(goal const &g) const
Definition: z3++.h:2698
expr extract(expr const &offset, expr const &length) const
sequence and regular expression operations.
Definition: z3++.h:1154
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.
Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s)
Return the symbol name.
void set_rounding_mode(rounding_mode rm)
Sets RoundingMode of FloatingPoints.
Definition: z3++.h:2940
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:1645
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.
expr_vector rules() const
Definition: z3++.h:2875
friend expr nor(expr const &a, expr const &b)
Definition: z3++.h:1574
params & operator=(params const &s)
Definition: z3++.h:465
friend std::ostream & operator<<(std::ostream &out, symbol const &s)
Definition: z3++.h:425
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:2188
unsigned hi() const
Definition: z3++.h:1142
check_result query(func_decl_vector &relations)
Definition: z3++.h:2856
check_result
Definition: z3++.h:129
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:2688
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:1896
friend expr operator<(expr const &a, expr const &b)
Definition: z3++.h:1517
friend expr operator!(expr const &a)
Return an expression representing not(a).
Definition: z3++.h:1307
friend expr bvsub_no_overflow(expr const &a, expr const &b)
Definition: z3++.h:1784
solver(context &c, solver const &src, translate)
Definition: z3++.h:2309
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.
Z3_goal_prec precision() const
Definition: z3++.h:2532
solver(context &c)
Definition: z3++.h:2305
unsigned Z3_API Z3_get_func_decl_id(Z3_context c, Z3_func_decl f)
Return a unique identifier for f.
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:2048
Z3_ast Z3_API Z3_mk_lstring(Z3_context c, unsigned len, Z3_string s)
Create a string constant out of the string that is passed in It takes the length of the string as wel...
expr lambda(expr const &x, expr const &b)
Definition: z3++.h:1983
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:621
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
bool is_decided_unsat() const
Definition: z3++.h:2538
Definition: z3++.h:137
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.
handle minimize(expr const &e)
Definition: z3++.h:2801
friend probe operator<(probe const &p1, probe const &p2)
Definition: z3++.h:2730
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
expr_vector assertions() const
Definition: z3++.h:2374
cube_iterator & operator++()
Definition: z3++.h:2455
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)
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:677
friend probe operator&&(probe const &p1, probe const &p2)
Definition: z3++.h:2745
void set(char const *k, double v)
Definition: z3++.h:2323
void add(expr const &e, expr const &p)
Definition: z3++.h:2330
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:3273
bool is_exists() const
Return true if this expression is an existential quantifier.
Definition: z3++.h:767
Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c, Z3_fixedpoint d, Z3_ast query)
Pose a query against the asserted rules.
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
void set(char const *k, unsigned n)
Definition: z3++.h:473
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow...
friend expr pble(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:2008
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point subtraction.
std::string key(unsigned i) const
Definition: z3++.h:2278
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.
bool is_relation() const
Return true if this sort is a Relation sort.
Definition: z3++.h:572
Z3_ast m_ast
Definition: z3++.h:486
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:472
tactic repeat(tactic const &t, unsigned max=UINT_MAX)
Definition: z3++.h:2646
expr bool_val(bool b)
Definition: z3++.h:3096
~context()
Definition: z3++.h:172
expr operator||(expr const &a, expr const &b)
Definition: z3++.h:1325
expr ult(expr const &a, expr const &b)
unsigned less than operator for bitvectors.
Definition: z3++.h:1700
void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p)
Increment the reference counter of the given parameter set.
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.
bool is_int() const
Return true if this is an integer expression.
Definition: z3++.h:686
ast_vector_tpl & operator=(ast_vector_tpl const &s)
Definition: z3++.h:1873
friend expr pbge(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:2016
apply_result apply(goal const &g) const
Definition: z3++.h:2612
expr int_val(int n)
Definition: z3++.h:3098
bool is_arith() const
Return true if this is an integer or real expression.
Definition: z3++.h:694
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.
model get_model() const
Definition: z3++.h:2365
func_decl(func_decl const &s)
Definition: z3++.h:622
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:1898
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 else_value() const
Definition: z3++.h:2165
expr mk_or(expr_vector const &args)
Definition: z3++.h:2110
tactic fail_if(probe const &p)
Definition: z3++.h:2887
Z3_func_decl Z3_API Z3_mk_linear_order(Z3_context c, Z3_sort a, unsigned id)
create a linear ordering relation over signature a. The relation is identified by the index id...
Z3_param_kind kind(symbol const &s)
Definition: z3++.h:451
stats(context &c, Z3_stats e)
Definition: z3++.h:2266
expr exists(expr const &x, expr const &b)
Definition: z3++.h:1959
std::string to_string()
Definition: z3++.h:2879
ast operator()(context &c, Z3_ast a)
Definition: z3++.h:1826
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
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:3442
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.
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.
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
expr unit() const
Definition: z3++.h:1164
bool is_array() const
Return true if this sort is a Array sort.
Definition: z3++.h:564
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.
std::string dimacs() const
Definition: z3++.h:2563
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 Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz, unsigned levels[])
retrieve the decision depth of Boolean literals (variables or their negations). Assumes a check-sat c...
void set(char const *k, symbol const &v)
Definition: z3++.h:2324
expr ite(expr const &c, expr const &t, expr const &e)
Create the if-then-else expression ite(c, t, e)
Definition: z3++.h:1645
T const & operator[](int i) const
Definition: z3++.h:395
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:2132
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...
double double_value(unsigned i) const
Definition: z3++.h:2282
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3243
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.
expr body() const
Return the 'body' of this quantifier.
Definition: z3++.h:956
std::string get_string() const
Definition: z3++.h:908
~ast()
Definition: z3++.h:491
void pop_back()
Definition: z3++.h:1871
friend expr bvneg_no_overflow(expr const &a)
Definition: z3++.h:1793
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.
cube_generator(solver &s)
Definition: z3++.h:2484
T operator[](int i) const
Definition: z3++.h:1867
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:494
bool is_seq() const
Return true if this sort is a Sequence sort.
Definition: z3++.h:576
func_interp add_func_interp(func_decl &f, expr &else_val)
Definition: z3++.h:2243
bool is_bv() const
Return true if this is a Bit-vector expression.
Definition: z3++.h:698
Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned remainder.
expr forall(expr const &x, expr const &b)
Definition: z3++.h:1935
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 domain(unsigned i) const
Definition: z3++.h:632
bool is_bool() const
Return true if this is a Boolean expression.
Definition: z3++.h:682
int64_t get_numeral_int64() const
Return int64_t value of numeral, throw if result cannot fit in int64_t.
Definition: z3++.h:850
sort(context &c, Z3_sort s)
Definition: z3++.h:519
unsigned hash() const
Definition: z3++.h:496
double operator()(goal const &g) const
Definition: z3++.h:2699
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
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:2500
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).
bool is_datatype() const
Return true if this sort is a Datatype sort.
Definition: z3++.h:568
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...
std::string to_string() const
Definition: z3++.h:498
expr implies(expr const &a, expr const &b)
Definition: z3++.h:1261
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:1622
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1254
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:1658
expr rotate_left(unsigned i)
Definition: z3++.h:1132
bool has_interp(func_decl f) const
Definition: z3++.h:2238
expr concat(expr const &a, expr const &b)
Definition: z3++.h:2066
symbol(context &c, Z3_symbol s)
Definition: z3++.h:415
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.
solver(context &c, char const *logic)
Definition: z3++.h:2308
bool is_false() const
Definition: z3++.h:1022
tactic try_for(tactic const &t, unsigned ms)
Definition: z3++.h:2657
func_interp(context &c, Z3_func_interp e)
Definition: z3++.h:2154
void register_relation(func_decl &p)
Definition: z3++.h:2873
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:2853
expr shl(expr const &a, expr const &b)
shift left operator for bitvectors
Definition: z3++.h:1746
expr bvsdiv_no_overflow(expr const &a, expr const &b)
Definition: z3++.h:1790
params(context &c)
Definition: z3++.h:461
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:2657
expr pble(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:2008
expr max(expr const &a, expr const &b)
Definition: z3++.h:1591
sort range() const
Definition: z3++.h:633
expr sqrt(expr const &a, expr const &rm)
Definition: z3++.h:1622
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:71
bool is_re() const
Return true if this is a regular expression.
Definition: z3++.h:718
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:1706
void push()
Definition: z3++.h:2804
expr last_indexof(expr const &s, expr const &substr)
Definition: z3++.h:3389
expr slt(expr const &a, expr const &b)
signed less than operator for bitvectors.
Definition: z3++.h:1686
void set(char const *param, bool value)
Update global parameter param with Boolean value.
Definition: z3++.h:207
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. Add the parsed constraints and objectives to the optimization context.
void set(params const &p)
Definition: z3++.h:2320
bool is_re() const
Return true if this sort is a regular expression sort.
Definition: z3++.h:580
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:532
Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort d)
Return the sort name as a symbol.
bool is_quantifier() const
Return true if this expression is a quantifier.
Definition: z3++.h:758
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:2958
context * m_ctx
Definition: z3++.h:402
unsigned size()
Definition: z3++.h:449
unsigned size() const
Definition: z3++.h:393
void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p)
Set parameters on fixedpoint context.
bool operator!=(iterator const &other) const
Definition: z3++.h:1903
symbol name() const
Definition: z3++.h:634
std::string help() const
Definition: z3++.h:2877
bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.
expr operator-(expr const &a)
Definition: z3++.h:1450
void pop(unsigned n=1)
Definition: z3++.h:2327
friend std::ostream & operator<<(std::ostream &out, stats const &s)
Definition: z3++.h:2285
expr smod(expr const &a, expr const &b)
signed modulus operator for bitvectors
Definition: z3++.h:1732
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:3213
cube_iterator end()
Definition: z3++.h:2499
handle(unsigned h)
Definition: z3++.h:2762
unsigned size() const
Definition: z3++.h:2277
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:1261
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:2413
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_...
ast(ast const &s)
Definition: z3++.h:490
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:2947
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:2662
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:521
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:1007
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:2575
expr nand(expr const &a, expr const &b)
Definition: z3++.h:1573
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.
void Z3_API Z3_ast_vector_set(Z3_context c, Z3_ast_vector v, unsigned i, Z3_ast a)
Update position i of the AST vector v with the AST a.
expr stoi() const
Definition: z3++.h:1192
expr operator/(expr const &a, expr const &b)
Definition: z3++.h:1428
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:618
expr set_union(expr const &a, expr const &b)
Definition: z3++.h:3330
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:394
expr_vector objectives() const
Definition: z3++.h:2836
bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t)
Return true if the given expression t is well sorted.
int get_numeral_int() const
Return int value of numeral, throw if result cannot fit in machine int.
Definition: z3++.h:814
param_descrs get_param_descrs()
Definition: z3++.h:2629
Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow...
bool is_xor() const
Definition: z3++.h:1026
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.
rounding_mode
Definition: z3++.h:133
goal(goal const &s)
Definition: z3++.h:2518
sort int_sort()
Return the integer sort.
Definition: z3++.h:2909
Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow...
expr set_del(expr const &s, expr const &e)
Definition: z3++.h:3326
void set(params const &p)
Definition: z3++.h:2824
check_result check(expr_vector const &asms)
Definition: z3++.h:2811
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:2270
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.
Definition: z3++.h:138
unsigned num_args() const
Definition: z3++.h:2143
func_decl & operator=(func_decl const &s)
Definition: z3++.h:624
expr bvsub_no_overflow(expr const &a, expr const &b)
Definition: z3++.h:1784
Z3_lbool bool_value() const
Definition: z3++.h:878
apply_result & operator=(apply_result const &s)
Definition: z3++.h:2579
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:2032
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 is_real() const
Return true if this sort is the Real sort.
Definition: z3++.h:552
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:1667
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.
expr numerator() const
Definition: z3++.h:882
bool is_decided_sat() const
Definition: z3++.h:2537
void add(expr const &f)
Definition: z3++.h:2528
Z3_ast Z3_API Z3_mk_seq_last_index(Z3_context c, Z3_ast, Z3_ast substr)
Return the last occurrence of substr in s. If s does not contain substr, then the value is -1...
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:3431
Z3_ast_vector Z3_API Z3_solver_get_trail(Z3_context c, Z3_solver s)
Return the trail modulo model conversion, in order of decision level The decision level can be retrie...
expr to_re(expr const &s)
Definition: z3++.h:3395
func_decl linear_order(sort const &a, unsigned index)
Definition: z3++.h:1809
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. Add the parsed constraints and objectives to the optimization context.
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)
Check if container contains containee.
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.
expr denominator() const
Definition: z3++.h:890
bool is_numeral_i(int &i) const
Definition: z3++.h:742
param_descrs get_param_descrs()
Definition: z3++.h:2878
unsigned size() const
Definition: z3++.h:2214
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:2576
bool is_fpa() const
Return true if this sort is a Floating point sort.
Definition: z3++.h:588