Z3
z3++.h
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4  Thin C++ layer on top of the Z3 C API.
5  Main features:
6  - Smart pointers for all Z3 objects.
7  - Object-Oriented interface.
8  - Operator overloading.
9  - Exceptions for signaling Z3 errors
10 
11  The C API can be used simultaneously with the C++ layer.
12  However, if you use the C API directly, you will have to check the error conditions manually.
13  Of course, you can invoke the method check_error() of the context object.
14 Author:
15 
16  Leonardo (leonardo) 2012-03-28
17 
18 Notes:
19 
20 --*/
21 #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; }
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); }
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); }
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 
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  }
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(); }
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); }
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) {
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) {
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) {
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) {
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
ast_vector_tpl(context &c)
Definition: z3++.h:1861
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
bool is_uint(unsigned i) const
Definition: z3++.h:2279
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
stats statistics() const
Definition: z3++.h:2837
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
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.
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
expr get_const_interp(func_decl c) const
Definition: z3++.h:2223
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 is_decided_unsat() const
Definition: z3++.h:2538
bool operator!=(cube_iterator const &other)
Definition: z3++.h:2472
void Z3_API Z3_fixedpoint_add_rule(Z3_context c, Z3_fixedpoint d, Z3_ast rule, Z3_symbol name)
Add a universal Horn clause as a named rule. The horn_rule should be of the form:
bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned int....
Z3_ast Z3_API Z3_mk_fpa_rtz(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
bool is_eq() const
Definition: z3++.h:1028
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
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
bool is_bool() const
Return true if this sort is the Boolean sort.
Definition: z3++.h:544
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
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
bool is_datatype() const
Return true if this is a Datatype expression.
Definition: z3++.h:706
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.
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:934
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.
unsigned uint_value(unsigned i) const
Definition: z3++.h:2281
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_entry entry(unsigned i) const
Definition: z3++.h:2167
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
double double_value(unsigned i) const
Definition: z3++.h:2282
std::string documentation(symbol const &s)
Definition: z3++.h:452
stats statistics() const
Definition: z3++.h:2372
Z3_error_code check_error() const
Definition: z3++.h:407
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.
std::string help() const
Definition: z3++.h:2841
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
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d)
Return the constant declaration name as a symbol.
Z3_string Z3_API Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s)
Retrieve documentation string corresponding to parameter name s.
model get_model() const
Definition: z3++.h:2822
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
unsigned size() const
Definition: z3++.h:2530
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...
expr operator[](int i) const
Definition: z3++.h:2531
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
func_decl get_const_decl(unsigned i) const
Definition: z3++.h:2212
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.
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.
expr extract(expr const &offset, expr const &length) const
sequence and regular expression operations.
Definition: z3++.h:1154
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
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
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....
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...
func_decl get_func_decl(unsigned i) const
Definition: z3++.h:2213
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.
Definition: z3++.h:130
Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v)
Array update.
func_entry & operator=(func_entry const &s)
Definition: z3++.h: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
std::string get_string() const
Definition: z3++.h:908
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
Definition: z3++.h:137
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
bool is_algebraic() const
Return true if expression is an algebraic number.
Definition: z3++.h:780
unsigned get_numeral_uint() const
Return uint value of numeral, throw if result cannot fit in machine uint.
Definition: z3++.h:833
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(double &d) const
Definition: z3++.h:746
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 ...
expr extract(unsigned hi, unsigned lo) const
Definition: z3++.h:1140
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....
sort array_domain() const
Return the domain of this Array sort.
Definition: z3++.h:605
char const * msg() const
Definition: z3++.h:87
T operator[](int i) const
Definition: z3++.h:1867
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
friend expr operator^(expr const &a, expr const &b)
Definition: z3++.h:1565
~array()
Definition: z3++.h:391
void pop_back()
Definition: z3++.h:1871
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.
sort array_range() const
Return the range of this Array sort.
Definition: z3++.h:611
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.
Z3_ast Z3_API Z3_mk_int64(Z3_context c, int64_t v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
T const & operator[](int i) const
Definition: z3++.h:395
unsigned id() const
retrieve unique identifier for func_decl.
Definition: z3++.h:527
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....
Definition: z3++.h:221
expr lshr(expr const &a, expr const &b)
logic shift right operator for bitvectors
Definition: z3++.h:1753
expr as_expr() const
Definition: z3++.h:2550
expr udiv(expr const &a, expr const &b)
unsigned division operator for bitvectors.
Definition: z3++.h:1718
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
friend expr concat(expr const &a, expr const &b)
Definition: z3++.h: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.
std::string help() const
Definition: z3++.h:2621
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...
bool is_bv() const
Return true if this is a Bit-vector expression.
Definition: z3++.h:698
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
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_vector assertions() const
Definition: z3++.h:2835
bool is_exists() const
Return true if this expression is an existential quantifier.
Definition: z3++.h:767
model(context &c, Z3_model m)
Definition: z3++.h:2187
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
model convert_model(model const &m) const
Definition: z3++.h:2539
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.
double operator()(goal const &g) const
Definition: z3++.h:2699
bool is_real() const
Return true if this is a real expression.
Definition: z3++.h:690
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)
Return the number of parameters associated with a declaration.
bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
Compare terms.
check_result query(expr &q)
Definition: z3++.h:2855
#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.
Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name)
Return a probe associated with the given name. The complete list of probes may be obtained using the ...
bool is_datatype() const
Return true if this sort is a Datatype sort.
Definition: z3++.h:568
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...
int to_int() const
Definition: z3++.h:421
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.
func_decl operator[](int i) const
Definition: z3++.h:2215
expr rotate_right(unsigned i)
Definition: z3++.h:1133
~tactic()
Definition: z3++.h:2602
bool is_array() const
Return true if this is a Array expression.
Definition: z3++.h:702
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.
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
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
expr nth(expr const &index) const
Definition: z3++.h:1181
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 Z3_API Z3_get_sort_id(Z3_context c, Z3_sort s)
Return a unique identifier for s.
expr itos() const
Definition: z3++.h:1197
Z3_context Z3_API Z3_mk_context_rc(Z3_config c)
Create a context using the given configuration. This function is similar to Z3_mk_context....
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.
bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, uint64_t *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine uint64_t int....
ast_vector_tpl(context &c, Z3_ast_vector v)
Definition: z3++.h:1862
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.
bool is_int() const
Return true if this sort is the Integer sort.
Definition: z3++.h:548
expr operator!(expr const &a)
Definition: z3++.h:1307
ast_vector_tpl & set(unsigned idx, ast &a)
Definition: z3++.h:1880
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
expr operator[](expr const &index) const
Definition: z3++.h:1221
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g)
Return true if the given goal contains the formula false.
bool enable_exceptions() const
Definition: z3++.h:198
expr ule(expr const &a, expr const &b)
unsigned less than or equal to operator for bitvectors.
Definition: z3++.h: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
std::string key(unsigned i) const
Definition: z3++.h:2278
void Z3_API Z3_ast_vector_resize(Z3_context c, Z3_ast_vector v, unsigned n)
Resize the AST vector v.
expr simplify(params const &p) const
Return a simplified version of this expression. The parameter p is a set of parameters for the Z3 sim...
Definition: z3++.h:1240
Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s)
Return the length of the sequence s.
Z3_ast Z3_API Z3_mk_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s)
Check if prefix is a prefix of s.
Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s)
Return the set of units modulo model conversion.
Z3_string Z3_API Z3_stats_get_key(Z3_context c, Z3_stats s, unsigned idx)
Return the key (a string) for a particular statistical data.
void set(char const *param, int value)
Update global parameter param with Integer value.
Definition: z3++.h:211
static param_descrs simplify_param_descrs(context &c)
Definition: z3++.h: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.
sort domain(unsigned i) const
Definition: z3++.h:632
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
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 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.
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
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
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.
bool is_re() const
Return true if this is a regular expression.
Definition: z3++.h:718
expr pw(expr const &a, expr const &b)
Definition: z3++.h:1269
bool empty() const
Definition: z3++.h:1872
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...
bool is_numeral_i64(int64_t &i) const
Definition: z3++.h:740
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
unsigned Z3_API Z3_ast_vector_size(Z3_context c, Z3_ast_vector v)
Return the size of the given AST vector.
expr_vector assertions() const
Definition: z3++.h:2874
bool is_fpa() const
Return true if this sort is a Floating point sort.
Definition: z3++.h:588
expr operator~(expr const &a)
Definition: z3++.h:1629
unsigned num_entries() const
Definition: z3++.h:2166
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.
Z3_ast Z3_API Z3_mk_fpa_rtn(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
def tactics(ctx=None)
Definition: z3py.py:7887
friend expr int2bv(unsigned n, expr const &a)
Definition: z3++.h:1773
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.
friend expr operator-(expr const &a)
Definition: z3++.h: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_symbol_kind kind() const
Definition: z3++.h:419
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
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 length() const
Definition: z3++.h:1187
expr bvmul_no_underflow(expr const &a, expr const &b)
Definition: z3++.h:1799
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.
expr denominator() const
Definition: z3++.h:890
Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.
sort range() const
Definition: z3++.h:633
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
unsigned size() const
Definition: z3++.h:2277
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 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.
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
Z3_decl_kind decl_kind() const
Definition: z3++.h:635
bool is_re() const
Return true if this sort is a regular expression sort.
Definition: z3++.h:580
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.
iterator begin() const
Definition: z3++.h:1917
ast(context &c, Z3_ast n)
Definition: z3++.h:489
ast_vector_tpl & operator=(ast_vector_tpl const &s)
Definition: z3++.h:1873
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
Z3_goal_prec precision() const
Definition: z3++.h:2532
void set(char const *k, char const *s)
Definition: z3++.h:476
expr bv_const(char const *name, unsigned sz)
Definition: z3++.h:3090
context & ctx() const
Definition: z3++.h:406
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.
Z3_sort_kind sort_kind() const
Return the internal sort kind.
Definition: z3++.h:536
T back() const
Definition: z3++.h:1870
expr string_val(char const *s)
Definition: z3++.h:3126
tactic(context &c, char const *name)
Definition: z3++.h:2599
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
bool is_lambda() const
Return true if this expression is a lambda expression.
Definition: z3++.h:771
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
expr_vector unsat_core() const
Definition: z3++.h:2823
Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1)
Coerce an integer to a real.
iterator end() const
Definition: z3++.h:1918
Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, unsigned backtrack_level)
extract a next cube for a solver. The last cube is the constant true or false. The number of (non-con...
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point remainder.
Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)
Shift left.
~config()
Definition: z3++.h:109
bool is_arith() const
Return true if this sort is the Integer or Real sort.
Definition: z3++.h:556
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).
bool is_relation() const
Return true if this sort is a Relation sort.
Definition: z3++.h:572
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
bool is_real() const
Return true if this sort is the Real sort.
Definition: z3++.h:552
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 resize(unsigned sz)
Definition: z3++.h:1869
void Z3_API Z3_del_config(Z3_config c)
Delete the given configuration object.
expr body() const
Return the 'body' of this quantifier.
Definition: z3++.h:956
expr operator()() const
Definition: z3++.h:3152
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 hash() const
Definition: z3++.h:496
optimize(context &c)
Definition: z3++.h:2765
goal operator[](int i) const
Definition: z3++.h:2587
expr min(expr const &a, expr const &b)
Definition: z3++.h:1576
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].
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:750
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
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
expr_vector objectives() const
Definition: z3++.h:2836
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
Z3_goal_prec Z3_API Z3_goal_precision(Z3_context c, Z3_goal g)
Return the "precision" of the given goal. Goals can be transformed using over and under approximation...
expr operator+(expr const &a, expr const &b)
Definition: z3++.h: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.
std::string help() const
Definition: z3++.h:2877
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.
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3050
bool is_arith() const
Return true if this is an integer or real expression.
Definition: z3++.h:694
bool is_well_sorted() const
Return true if this expression is well sorted (aka type correct).
Definition: z3++.h:785
bool is_numeral_u64(uint64_t &i) const
Definition: z3++.h:741
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...
bool is_implies() const
Definition: z3++.h:1027
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...
std::string str() const
Definition: z3++.h:420
expr re_complement(expr const &a)
Definition: z3++.h:3428
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.
bool inconsistent() const
Definition: z3++.h:2533
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.
bool is_fpa() const
Return true if this is a FloatingPoint expression. .
Definition: z3++.h:732
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
expr at(expr const &index) const
Definition: z3++.h:1175
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
bool is_true() const
Definition: z3++.h:1021
ast_vector_tpl< sort > sort_vector
Definition: z3++.h:72
bool is_bool() const
Return true if this is a Boolean expression.
Definition: z3++.h:682
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
unsigned fpa_ebits() const
Definition: z3++.h:597
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_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_lbool bool_value() const
Definition: z3++.h:878
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
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.
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
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,...
expr const_array(sort const &d, expr const &v)
Definition: z3++.h:3310
stats(stats const &s)
Definition: z3++.h:2267
bool is_and() const
Definition: z3++.h:1024
std::string to_string() const
Definition: z3++.h:498
cube_iterator operator++(int)
Definition: z3++.h:2465
bool is_or() const
Definition: z3++.h:1025
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f)
Retrieve set of rules from fixedpoint context.
expr_vector non_units() const
Definition: z3++.h:2375
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.
friend std::ostream & operator<<(std::ostream &out, model const &m)
Definition: z3++.h:2256
Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target)
Copy a solver s from the context source to the context target.
int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s)
Return the symbol int value.
void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p)
Decrement the reference counter of the given parameter set.
~func_entry()
Definition: z3++.h:2133
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:677
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)
Decrement the reference counter of the given optimize context.
int64_t get_numeral_int64() const
Return int64_t value of numeral, throw if result cannot fit in int64_t.
Definition: z3++.h:850
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...
expr stoi() const
Definition: z3++.h:1192
check_result check(expr_vector const &assumptions)
Definition: z3++.h:2354
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).
T * ptr()
Definition: z3++.h:397
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
unsigned lo() const
Definition: z3++.h:1141
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
bool is_array() const
Return true if this sort is a Array sort.
Definition: z3++.h:564
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.
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_vector const * operator->() const
Definition: z3++.h:2466
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 abs(expr const &a)
Definition: z3++.h:1606
expr replace(expr const &src, expr const &dst) const
Definition: z3++.h:1158
symbol(symbol const &s)
Definition: z3++.h:416
expr value() const
Definition: z3++.h:2142
Z3_ast_vector Z3_API Z3_parse_smtlib2_file(Z3_context c, Z3_string file_name, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Similar to Z3_parse_smtlib2_string, but reads the benchmark from a file.
unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e)
Return the number of arguments in a Z3_func_entry object.
bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, int64_t *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int64_t int....
Z3_symbol_kind
The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See Z3_...
Definition: z3_api.h: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.
unsigned arity() const
Definition: z3++.h:631
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,...
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
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
unsigned num_exprs() const
Definition: z3++.h:2536
object(context &c)
Definition: z3++.h:404
friend expr operator>(expr const &a, expr const &b)
Definition: z3++.h:1539
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
bool is_numeral(std::string &s, unsigned precision) const
Definition: z3++.h:745
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
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 arg(unsigned i) const
Return the i-th argument of this application. This method assumes the expression is an application.
Definition: z3++.h:949
expr_vector const & operator*() const
Definition: z3++.h:2467
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
bool is_relation() const
Return true if this is a Relation expression.
Definition: z3++.h:710
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
bool is_const() const
Return true if this expression is a constant (i.e., an application with 0 arguments).
Definition: z3++.h:754
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...
unsigned h() const
Definition: z3++.h:2763
Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1)
Repeat the given bit-vector up length i.
unsigned size() const
Definition: z3++.h:2586
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.
unsigned id() const
retrieve unique identifier for expression.
Definition: z3++.h:802
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.
bool is_decided_sat() const
Definition: z3++.h:2537
Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re)
Create the regular language re*.
expr sext(expr const &a, unsigned i)
Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i,...
Definition: z3++.h: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...
Definition: z3++.h:134
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.
Z3_sort Z3_API Z3_mk_real_sort(Z3_context c)
Create the real type.
friend expr pbeq(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:2024
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....
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.
Z3_ast Z3_API Z3_mk_fpa_rna(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
bool is_numeral_i(int &i) const
Definition: z3++.h:742
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.
Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length)
Extract subsequence starting at offset of length.
Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset)
Return index of first occurrence of substr in s starting from offset offset. If s does not contain su...
expr_vector units() const
Definition: z3++.h:2376
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
expr_vector rules() const
Definition: z3++.h:2875
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.
friend std::ostream & operator<<(std::ostream &out, ast_vector_tpl const &v)
Definition: z3++.h:1919
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.
ast_vector_tpl(ast_vector_tpl const &s)
Definition: z3++.h:1863
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
bool is_forall() const
Return true if this expression is a universal quantifier.
Definition: z3++.h:763
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.
bool is_bv() const
Return true if this sort is a Bit-vector sort.
Definition: z3++.h:560
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 else_value() const
Definition: z3++.h:2165
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 numerator() const
Definition: z3++.h:882
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
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 unit() const
Definition: z3++.h:1164
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].
expr simplify() const
Return a simplified version of this expression.
Definition: z3++.h:1236
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:141
expr star(expr const &re)
Definition: z3++.h:3407
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_vector trail(array< unsigned > &levels) const
Definition: z3++.h:2378
expr operator==(expr const &a, expr const &b)
Definition: z3++.h:1338
symbol name() const
Return name of sort.
Definition: z3++.h:540
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
Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s)
Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the commands Z3_solver_ch...
unsigned hi() const
Definition: z3++.h:1142
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point division.
unsigned num_args() const
Definition: z3++.h:2143
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
expr arg(unsigned i) const
Definition: z3++.h:2144
unsigned fpa_sbits() const
Definition: z3++.h:599
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.
void check_parser_error() const
Definition: z3++.h:185
Z3_probe Z3_API Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned...
Z3_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f)
Return a string describing all fixedpoint available parameters.
expr bool_const(char const *name)
Definition: z3++.h: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.
solver mk_solver() const
Definition: z3++.h:2611
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
rounding_mode
Definition: z3++.h:133
std::string reason_unknown() const
Definition: z3++.h:2371
Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize t)
Return a string containing a description of parameters accepted by optimize.
bool is_ite() const
Definition: z3++.h:1029
Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s)
Return the symbol name.
model get_model() const
Definition: z3++.h:2365
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.
unsigned num_consts() const
Definition: z3++.h:2210
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
expr proof() const
Definition: z3++.h:2388
bool is_numeral_u(unsigned &i) const
Definition: z3++.h:743
check_result query(func_decl_vector &relations)
Definition: z3++.h:2856
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
symbol name() const
Definition: z3++.h:634
Definition: z3++.h:138
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.
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
Z3_ast Z3_API Z3_mk_int(Z3_context c, int v, Z3_sort ty)
Create a numeral of an int, bit-vector, or finite-domain sort.
T const * ptr() const
Definition: z3++.h:396
handle minimize(expr const &e)
Definition: z3++.h:2801
apply_result apply(goal const &g) const
Definition: z3++.h:2612
friend probe operator<(probe const &p1, probe const &p2)
Definition: z3++.h:2730
unsigned id() const
retrieve unique identifier for func_decl.
Definition: z3++.h:629
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
cube_iterator & operator++()
Definition: z3++.h: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)
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
Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c, Z3_fixedpoint d, Z3_ast query)
Pose a query against the asserted rules.
bool has_interp(func_decl f) const
Definition: z3++.h:2238
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
unsigned size() const
Definition: z3++.h:2214
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.
apply_result operator()(goal const &g) const
Definition: z3++.h:2618
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.
Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s)
Return the set of non units in the solver state.
Z3_ast m_ast
Definition: z3++.h: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
unsigned size() const
Definition: z3++.h:1866
unsigned size() const
Definition: z3++.h:393
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
uint64_t get_numeral_uint64() const
Return uint64_t value of numeral, throw if result cannot fit in uint64_t.
Definition: z3++.h:867
expr ult(expr const &a, expr const &b)
unsigned less than operator for bitvectors.
Definition: z3++.h:1700
bool is_var() const
Return true if this expression is a variable.
Definition: z3++.h:776
T * operator->() const
Definition: z3++.h:1914
void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p)
Increment the reference counter of the given parameter set.
unsigned depth() const
Definition: z3++.h:2534
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.
bool operator!=(iterator const &other) const
Definition: z3++.h:1903
void Z3_API Z3_params_set_symbol(Z3_context c, Z3_params p, Z3_symbol k, Z3_symbol v)
Add a symbol parameter k with value v to the parameter set p.
friend expr pbge(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:2016
expr int_val(int n)
Definition: z3++.h:3098
void Z3_API Z3_global_param_reset_all(void)
Restore the value of all global (and module) parameters. This command will not affect already created...
void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m)
Increment the reference counter of the given model.
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a minimization constraint.
func_decl(func_decl const &s)
Definition: z3++.h: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 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.
Definition: z3++.h:136
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.
expr_vector parse_string(char const *s)
parsing
Definition: z3++.h: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.
model get_model() const
Definition: z3++.h:2545
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
bool is_quantifier() const
Return true if this expression is a quantifier.
Definition: z3++.h:758
Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s)
Return the parameter description set for the given solver object.
unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f)
Return the number of entries in the given function interpretation.
void 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
double apply(goal const &g) const
Definition: z3++.h:2698
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,...
bool is_not() const
Definition: z3++.h:1023
expr eval(expr const &n, bool model_completion=false) const
Definition: z3++.h:2200
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3243
bool operator==(iterator const &other) const
Definition: z3++.h:1900
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.
Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq)
Create an empty sequence of the sequence sort seq.
~ast()
Definition: z3++.h:491
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.
expr_vector unsat_core() const
Definition: z3++.h:2373
int get_numeral_int() const
Return int value of numeral, throw if result cannot fit in machine int.
Definition: z3++.h:814
cube_generator(solver &s)
Definition: z3++.h:2484
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
func_interp add_func_interp(func_decl &f, expr &else_val)
Definition: z3++.h:2243
expr_vector assertions() const
Definition: z3++.h:2374
unsigned num_args() const
Return the number of arguments in this application. This method assumes the expression is an applicat...
Definition: z3++.h:941
unsigned bv_size() const
Return the size of this Bit-vector sort.
Definition: z3++.h:595
Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned remainder.
Z3_ast_kind kind() const
Definition: z3++.h:495
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(context &c, Z3_sort s)
Definition: z3++.h:519
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).
Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, bool const *bits)
create a bit-vector numeral from a vector of Booleans.
Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t)
Create a new solver that is implemented using the given tactic. The solver supports the commands Z3_s...
expr implies(expr const &a, expr const &b)
Definition: z3++.h: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
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.
stats statistics() const
Definition: z3++.h:2872
solver(context &c, char const *logic)
Definition: z3++.h:2308
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.
std::string dimacs() const
Definition: z3++.h:2411
void add_rule(expr &rule, symbol const &name)
Definition: z3++.h:2853
std::string get_escaped_string() const
for a string value expression return an escaped or unescaped string value.
Definition: z3++.h:902
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
void push_back(T const &e)
Definition: z3++.h:1868
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
expr sqrt(expr const &a, expr const &rm)
Definition: z3++.h:1622
expr operator[](expr_vector const &index) const
Definition: z3++.h:1229
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:71
Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[])
Create the union of the regular languages.
void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)
Decrement the reference counter of the given probe.
expr uge(expr const &a, expr const &b)
unsigned greater than or equal to operator for bitvectors.
Definition: z3++.h: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
bool is_seq() const
Return true if this sort is a Sequence sort.
Definition: z3++.h:576
void set(char const *param, bool value)
Update global parameter param with Boolean value.
Definition: z3++.h:207
bool is_numeral(std::string &s) const
Definition: z3++.h:744
void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 file with assertions, soft constraints and optimization objectives....
void set(params const &p)
Definition: z3++.h:2320
bool is_double(unsigned i) const
Definition: z3++.h:2280
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.
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
void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p)
Set parameters on fixedpoint context.
bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.
bool is_finite_domain() const
Return true if this is a Finite-domain expression.
Definition: z3++.h:728
expr operator-(expr const &a)
Definition: z3++.h:1450
func_interp get_func_interp(func_decl f) const
Definition: z3++.h:2229
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
std::string dimacs() const
Definition: z3++.h:2563
cube_iterator end()
Definition: z3++.h:2499
handle(unsigned h)
Definition: z3++.h:2762
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
Definition: z3++.h:135
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:739
Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a)
Create a unit sequence of a.
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.
void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a)
Increment the reference counter of the given AST. The context c should have been created using Z3_mk_...
bool is_const() const
Definition: z3++.h:641
bool is_seq() const
Return true if this is a sequence expression.
Definition: z3++.h:714
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.
expr_vector trail() const
Definition: z3++.h:2377
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
bool is_finite_domain() const
Return true if this sort is a Finite domain sort.
Definition: z3++.h:584
bool is_distinct() const
Definition: z3++.h:1030
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 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
bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t)
Return true if the given expression t is well sorted.
param_descrs get_param_descrs()
Definition: z3++.h: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.
Z3_probe Z3_API Z3_probe_or(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when p1 or p2 evaluates to true.
goal(goal const &s)
Definition: z3++.h: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
bool is_xor() const
Definition: z3++.h:1026
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.
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
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 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.
bool is_int() const
Return true if this is an integer expression.
Definition: z3++.h:686
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
bool is_false() const
Definition: z3++.h:1022
void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives....
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)
Check if container contains containee.
unsigned num_funcs() const
Definition: z3++.h:2211
check_result
Definition: z3++.h:129
Z3_ast Z3_API Z3_mk_zero_ext(Z3_context c, unsigned i, Z3_ast t1)
Extend the given bit-vector with zeros to the (unsigned) equivalent bit-vector of size m+i,...
Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m)
Convert the given model into a string.
param_descrs get_param_descrs()
Definition: z3++.h:2878
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