Z3
z3++.h
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4  Thin C++ layer on top of the Z3 C API.
5  Main features:
6  - Smart pointers for all Z3 objects.
7  - Object-Oriented interface.
8  - Operator overloading.
9  - Exceptions for signining Z3 errors
10 
11  The C API can be used simultaneously with the C++ layer.
12  However, if you use the C API directly, you will have to check the error conditions manually.
13  Of course, you can invoke the method check_error() of the context object.
14 Author:
15 
16  Leonardo (leonardo) 2012-03-28
17 
18 Notes:
19 
20 --*/
21 #ifndef Z3PP_H_
22 #define Z3PP_H_
23 
24 #include<cassert>
25 #include<iostream>
26 #include<string>
27 #include<sstream>
28 #include<z3.h>
29 #include<limits.h>
30 
36 
41 
45 namespace z3 {
46 
47  class exception;
48  class config;
49  class context;
50  class symbol;
51  class params;
52  class param_descrs;
53  class ast;
54  class sort;
55  class func_decl;
56  class expr;
57  class solver;
58  class goal;
59  class tactic;
60  class probe;
61  class model;
62  class func_interp;
63  class func_entry;
64  class statistics;
65  class apply_result;
66  template<typename T> class ast_vector_tpl;
71 
72  inline void set_param(char const * param, char const * value) { Z3_global_param_set(param, value); }
73  inline void set_param(char const * param, bool value) { Z3_global_param_set(param, value ? "true" : "false"); }
74  inline void set_param(char const * param, int value) { std::ostringstream oss; oss << value; Z3_global_param_set(param, oss.str().c_str()); }
76 
80  class exception {
81  std::string m_msg;
82  public:
83  exception(char const * msg):m_msg(msg) {}
84  char const * msg() const { return m_msg.c_str(); }
85  friend std::ostream & operator<<(std::ostream & out, exception const & e);
86  };
87  inline std::ostream & operator<<(std::ostream & out, exception const & e) { out << e.msg(); return out; }
88 
89 #if !defined(Z3_THROW)
90 #if __cpp_exceptions || _CPPUNWIND || __EXCEPTIONS
91 #define Z3_THROW(x) throw x
92 #else
93 #define Z3_THROW(x) {}
94 #endif
95 #endif // !defined(Z3_THROW)
96 
100  class config {
101  Z3_config m_cfg;
102  config(config const & s);
103  config & operator=(config const & s);
104  public:
105  config() { m_cfg = Z3_mk_config(); }
106  ~config() { Z3_del_config(m_cfg); }
107  operator Z3_config() const { return m_cfg; }
111  void set(char const * param, char const * value) { Z3_set_param_value(m_cfg, param, value); }
115  void set(char const * param, bool value) { Z3_set_param_value(m_cfg, param, value ? "true" : "false"); }
119  void set(char const * param, int value) {
120  std::ostringstream oss;
121  oss << value;
122  Z3_set_param_value(m_cfg, param, oss.str().c_str());
123  }
124  };
125 
128  };
129 
131  if (l == Z3_L_TRUE) return sat;
132  else if (l == Z3_L_FALSE) return unsat;
133  return unknown;
134  }
135 
136 
140  class context {
141  bool m_enable_exceptions;
142  Z3_context m_ctx;
143  void init(config & c) {
144  m_ctx = Z3_mk_context_rc(c);
145  m_enable_exceptions = true;
146  Z3_set_error_handler(m_ctx, 0);
148  }
149 
150  void init_interp(config & c) {
151  m_ctx = Z3_mk_interpolation_context(c);
152  m_enable_exceptions = true;
153  Z3_set_error_handler(m_ctx, 0);
155  }
156 
157  context(context const & s);
158  context & operator=(context const & s);
159  public:
160  struct interpolation {};
161  context() { config c; init(c); }
162  context(config & c) { init(c); }
163  context(config & c, interpolation) { init_interp(c); }
164  ~context() { Z3_del_context(m_ctx); }
165  operator Z3_context() const { return m_ctx; }
166 
171  Z3_error_code e = Z3_get_error_code(m_ctx);
172  if (e != Z3_OK && enable_exceptions())
173  Z3_THROW(exception(Z3_get_error_msg(m_ctx, e)));
174  return e;
175  }
176 
177  void check_parser_error() const {
178  Z3_error_code e = Z3_get_error_code(*this);
179  if (e != Z3_OK && enable_exceptions()) {
180  Z3_string s = Z3_get_parser_error(*this);
181  if (s && *s) Z3_THROW(exception(s));
182  }
183  check_error();
184  }
185 
193  void set_enable_exceptions(bool f) { m_enable_exceptions = f; }
194 
195  bool enable_exceptions() const { return m_enable_exceptions; }
196 
200  void set(char const * param, char const * value) { Z3_update_param_value(m_ctx, param, value); }
204  void set(char const * param, bool value) { Z3_update_param_value(m_ctx, param, value ? "true" : "false"); }
208  void set(char const * param, int value) {
209  std::ostringstream oss;
210  oss << value;
211  Z3_update_param_value(m_ctx, param, oss.str().c_str());
212  }
213 
218  void interrupt() { Z3_interrupt(m_ctx); }
219 
223  symbol str_symbol(char const * s);
227  symbol int_symbol(int n);
231  sort bool_sort();
235  sort int_sort();
239  sort real_sort();
243  sort bv_sort(unsigned sz);
247  sort string_sort();
251  sort seq_sort(sort& s);
255  sort re_sort(sort& seq_sort);
261  sort array_sort(sort d, sort r);
262  sort array_sort(sort_vector const& d, sort r);
263 
269  sort enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts);
270 
277  func_decl tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs);
278 
282  sort uninterpreted_sort(char const* name);
283  sort uninterpreted_sort(symbol const& name);
284 
285  func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range);
286  func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range);
287  func_decl function(symbol const& name, sort_vector const& domain, sort const& range);
288  func_decl function(char const * name, sort_vector const& domain, sort const& range);
289  func_decl function(char const * name, sort const & domain, sort const & range);
290  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range);
291  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range);
292  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range);
293  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range);
294 
295  expr constant(symbol const & name, sort const & s);
296  expr constant(char const * name, sort const & s);
297  expr bool_const(char const * name);
298  expr int_const(char const * name);
299  expr real_const(char const * name);
300  expr bv_const(char const * name, unsigned sz);
301 
302  expr bool_val(bool b);
303 
304  expr int_val(int n);
305  expr int_val(unsigned n);
306  expr int_val(int64_t n);
307  expr int_val(uint64_t n);
308  expr int_val(char const * n);
309 
310  expr real_val(int n, int d);
311  expr real_val(int n);
312  expr real_val(unsigned n);
313  expr real_val(int64_t n);
314  expr real_val(uint64_t n);
315  expr real_val(char const * n);
316 
317  expr bv_val(int n, unsigned sz);
318  expr bv_val(unsigned n, unsigned sz);
319  expr bv_val(int64_t n, unsigned sz);
320  expr bv_val(uint64_t n, unsigned sz);
321  expr bv_val(char const * n, unsigned sz);
322  expr bv_val(unsigned n, bool const* bits);
323 
324  expr string_val(char const* s);
325  expr string_val(std::string const& s);
326 
327  expr num_val(int n, sort const & s);
328 
332  expr parse_string(char const* s);
333  expr parse_file(char const* file);
334 
335  expr parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
336  expr parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
337 
341  check_result compute_interpolant(expr const& pat, params const& p, expr_vector& interp, model& m);
342  expr_vector get_interpolant(expr const& proof, expr const& pat, params const& p);
343 
344  };
345 
346 
347 
348 
349  template<typename T>
350  class array {
351  T * m_array;
352  unsigned m_size;
353  array(array const & s);
354  array & operator=(array const & s);
355  public:
356  array(unsigned sz):m_size(sz) { m_array = new T[sz]; }
357  template<typename T2>
358  array(ast_vector_tpl<T2> const & v);
359  ~array() { delete[] m_array; }
360  unsigned size() const { return m_size; }
361  T & operator[](int i) { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
362  T const & operator[](int i) const { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
363  T const * ptr() const { return m_array; }
364  T * ptr() { return m_array; }
365  };
366 
367  class object {
368  protected:
370  public:
371  object(context & c):m_ctx(&c) {}
372  object(object const & s):m_ctx(s.m_ctx) {}
373  context & ctx() const { return *m_ctx; }
374  Z3_error_code check_error() const { return m_ctx->check_error(); }
375  friend void check_context(object const & a, object const & b);
376  };
377  inline void check_context(object const & a, object const & b) { (void)a; (void)b; assert(a.m_ctx == b.m_ctx); }
378 
379  class symbol : public object {
380  Z3_symbol m_sym;
381  public:
382  symbol(context & c, Z3_symbol s):object(c), m_sym(s) {}
383  symbol(symbol const & s):object(s), m_sym(s.m_sym) {}
384  symbol & operator=(symbol const & s) { m_ctx = s.m_ctx; m_sym = s.m_sym; return *this; }
385  operator Z3_symbol() const { return m_sym; }
386  Z3_symbol_kind kind() const { return Z3_get_symbol_kind(ctx(), m_sym); }
387  std::string str() const { assert(kind() == Z3_STRING_SYMBOL); return Z3_get_symbol_string(ctx(), m_sym); }
388  int to_int() const { assert(kind() == Z3_INT_SYMBOL); return Z3_get_symbol_int(ctx(), m_sym); }
389  friend std::ostream & operator<<(std::ostream & out, symbol const & s);
390  };
391 
392  inline std::ostream & operator<<(std::ostream & out, symbol const & s) {
393  if (s.kind() == Z3_INT_SYMBOL)
394  out << "k!" << s.to_int();
395  else
396  out << s.str().c_str();
397  return out;
398  }
399 
400 
401  class param_descrs : public object {
402  Z3_param_descrs m_descrs;
403  public:
404  param_descrs(context& c, Z3_param_descrs d): object(c), m_descrs(d) { Z3_param_descrs_inc_ref(c, d); }
405  param_descrs(param_descrs const& o): object(o.ctx()), m_descrs(o.m_descrs) { Z3_param_descrs_inc_ref(ctx(), m_descrs); }
407  Z3_param_descrs_inc_ref(o.ctx(), o.m_descrs);
408  Z3_param_descrs_dec_ref(ctx(), m_descrs);
409  m_descrs = o.m_descrs;
410  m_ctx = o.m_ctx;
411  return *this;
412  }
413  ~param_descrs() { Z3_param_descrs_dec_ref(ctx(), m_descrs); }
415 
416  unsigned size() { return Z3_param_descrs_size(ctx(), m_descrs); }
417  symbol name(unsigned i) { return symbol(ctx(), Z3_param_descrs_get_name(ctx(), m_descrs, i)); }
418  Z3_param_kind kind(symbol const& s) { return Z3_param_descrs_get_kind(ctx(), m_descrs, s); }
419  std::string documentation(symbol const& s) { char const* r = Z3_param_descrs_get_documentation(ctx(), m_descrs, s); check_error(); return r; }
420  std::string to_string() const { return Z3_param_descrs_to_string(ctx(), m_descrs); }
421  };
422 
423  inline std::ostream& operator<<(std::ostream & out, param_descrs const & d) { return out << d.to_string(); }
424 
425  class params : public object {
426  Z3_params m_params;
427  public:
428  params(context & c):object(c) { m_params = Z3_mk_params(c); Z3_params_inc_ref(ctx(), m_params); }
429  params(params const & s):object(s), m_params(s.m_params) { Z3_params_inc_ref(ctx(), m_params); }
430  ~params() { Z3_params_dec_ref(ctx(), m_params); }
431  operator Z3_params() const { return m_params; }
432  params & operator=(params const & s) {
433  Z3_params_inc_ref(s.ctx(), s.m_params);
434  Z3_params_dec_ref(ctx(), m_params);
435  m_ctx = s.m_ctx;
436  m_params = s.m_params;
437  return *this;
438  }
439  void set(char const * k, bool b) { Z3_params_set_bool(ctx(), m_params, ctx().str_symbol(k), b); }
440  void set(char const * k, unsigned n) { Z3_params_set_uint(ctx(), m_params, ctx().str_symbol(k), n); }
441  void set(char const * k, double n) { Z3_params_set_double(ctx(), m_params, ctx().str_symbol(k), n); }
442  void set(char const * k, symbol const & s) { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), s); }
443  friend std::ostream & operator<<(std::ostream & out, params const & p);
444  };
445 
446  inline std::ostream & operator<<(std::ostream & out, params const & p) {
447  out << Z3_params_to_string(p.ctx(), p); return out;
448  }
449 
450  class ast : public object {
451  protected:
452  Z3_ast m_ast;
453  public:
454  ast(context & c):object(c), m_ast(0) {}
455  ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
456  ast(ast const & s):object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
457  ~ast() { if (m_ast) Z3_dec_ref(*m_ctx, m_ast); }
458  operator Z3_ast() const { return m_ast; }
459  operator bool() const { return m_ast != 0; }
460  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; }
461  Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }
462  unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }
463  friend std::ostream & operator<<(std::ostream & out, ast const & n);
464  std::string to_string() const { return std::string(Z3_ast_to_string(ctx(), m_ast)); }
465 
466 
470  friend bool eq(ast const & a, ast const & b);
471  };
472  inline std::ostream & operator<<(std::ostream & out, ast const & n) {
473  out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
474  }
475 
476  inline bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b) != 0; }
477 
478 
482  class sort : public ast {
483  public:
484  sort(context & c):ast(c) {}
485  sort(context & c, Z3_sort s):ast(c, reinterpret_cast<Z3_ast>(s)) {}
486  sort(sort const & s):ast(s) {}
487  operator Z3_sort() const { return reinterpret_cast<Z3_sort>(m_ast); }
491  sort & operator=(sort const & s) { return static_cast<sort&>(ast::operator=(s)); }
495  Z3_sort_kind sort_kind() const { return Z3_get_sort_kind(*m_ctx, *this); }
499  symbol name() const { Z3_symbol s = Z3_get_sort_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
503  bool is_bool() const { return sort_kind() == Z3_BOOL_SORT; }
507  bool is_int() const { return sort_kind() == Z3_INT_SORT; }
511  bool is_real() const { return sort_kind() == Z3_REAL_SORT; }
515  bool is_arith() const { return is_int() || is_real(); }
519  bool is_bv() const { return sort_kind() == Z3_BV_SORT; }
523  bool is_array() const { return sort_kind() == Z3_ARRAY_SORT; }
527  bool is_datatype() const { return sort_kind() == Z3_DATATYPE_SORT; }
531  bool is_relation() const { return sort_kind() == Z3_RELATION_SORT; }
535  bool is_seq() const { return sort_kind() == Z3_SEQ_SORT; }
539  bool is_re() const { return sort_kind() == Z3_RE_SORT; }
543  bool is_finite_domain() const { return sort_kind() == Z3_FINITE_DOMAIN_SORT; }
544 
550  unsigned bv_size() const { assert(is_bv()); unsigned r = Z3_get_bv_sort_size(ctx(), *this); check_error(); return r; }
551 
557  sort array_domain() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_domain(ctx(), *this); check_error(); return sort(ctx(), s); }
563  sort array_range() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_range(ctx(), *this); check_error(); return sort(ctx(), s); }
564  };
565 
570  class func_decl : public ast {
571  public:
572  func_decl(context & c):ast(c) {}
573  func_decl(context & c, Z3_func_decl n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
574  func_decl(func_decl const & s):ast(s) {}
575  operator Z3_func_decl() const { return reinterpret_cast<Z3_func_decl>(m_ast); }
576  func_decl & operator=(func_decl const & s) { return static_cast<func_decl&>(ast::operator=(s)); }
577 
578  unsigned arity() const { return Z3_get_arity(ctx(), *this); }
579  sort domain(unsigned i) const { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }
580  sort range() const { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }
581  symbol name() const { Z3_symbol s = Z3_get_decl_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
582  Z3_decl_kind decl_kind() const { return Z3_get_decl_kind(ctx(), *this); }
583 
584  bool is_const() const { return arity() == 0; }
585 
586  expr operator()() const;
587  expr operator()(unsigned n, expr const * args) const;
588  expr operator()(expr_vector const& v) const;
589  expr operator()(expr const & a) const;
590  expr operator()(int a) const;
591  expr operator()(expr const & a1, expr const & a2) const;
592  expr operator()(expr const & a1, int a2) const;
593  expr operator()(int a1, expr const & a2) const;
594  expr operator()(expr const & a1, expr const & a2, expr const & a3) const;
595  expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const;
596  expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const;
597  };
598 
603  class expr : public ast {
604  public:
605  expr(context & c):ast(c) {}
606  expr(context & c, Z3_ast n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
607  expr(expr const & n):ast(n) {}
608  expr & operator=(expr const & n) { return static_cast<expr&>(ast::operator=(n)); }
609 
613  sort get_sort() const { Z3_sort s = Z3_get_sort(*m_ctx, m_ast); check_error(); return sort(*m_ctx, s); }
614 
618  bool is_bool() const { return get_sort().is_bool(); }
622  bool is_int() const { return get_sort().is_int(); }
626  bool is_real() const { return get_sort().is_real(); }
630  bool is_arith() const { return get_sort().is_arith(); }
634  bool is_bv() const { return get_sort().is_bv(); }
638  bool is_array() const { return get_sort().is_array(); }
642  bool is_datatype() const { return get_sort().is_datatype(); }
646  bool is_relation() const { return get_sort().is_relation(); }
650  bool is_seq() const { return get_sort().is_seq(); }
654  bool is_re() const { return get_sort().is_re(); }
655 
664  bool is_finite_domain() const { return get_sort().is_finite_domain(); }
665 
671  bool is_numeral() const { return kind() == Z3_NUMERAL_AST; }
672  bool is_numeral_i64(int64_t& i) const { bool r = 0 != Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}
673  bool is_numeral_u64(uint64_t& i) const { bool r = 0 != Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}
674  bool is_numeral_i(int& i) const { bool r = 0 != Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}
675  bool is_numeral_u(unsigned& i) const { bool r = 0 != Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
676  bool is_numeral(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; }
677  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; }
681  bool is_app() const { return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
685  bool is_const() const { return is_app() && num_args() == 0; }
689  bool is_quantifier() const { return kind() == Z3_QUANTIFIER_AST; }
693  bool is_var() const { return kind() == Z3_VAR_AST; }
697  bool is_algebraic() const { return 0 != Z3_is_algebraic_number(ctx(), m_ast); }
698 
702  bool is_well_sorted() const { bool r = Z3_is_well_sorted(ctx(), m_ast) != 0; check_error(); return r; }
703 
710  std::string get_decimal_string(int precision) const {
711  assert(is_numeral() || is_algebraic());
712  return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
713  }
714 
725  int get_numeral_int() const {
726  int result = 0;
727  if (!is_numeral_i(result)) {
728  assert(ctx().enable_exceptions());
729  if (!ctx().enable_exceptions()) return 0;
730  Z3_THROW(exception("numeral does not fit in machine int"));
731  }
732  return result;
733  }
734 
744  unsigned get_numeral_uint() const {
745  assert(is_numeral());
746  unsigned result = 0;
747  if (!is_numeral_u(result)) {
748  assert(ctx().enable_exceptions());
749  if (!ctx().enable_exceptions()) return 0;
750  Z3_THROW(exception("numeral does not fit in machine uint"));
751  }
752  return result;
753  }
754 
761  int64_t get_numeral_int64() const {
762  assert(is_numeral());
763  int64_t result = 0;
764  if (!is_numeral_i64(result)) {
765  assert(ctx().enable_exceptions());
766  if (!ctx().enable_exceptions()) return 0;
767  Z3_THROW(exception("numeral does not fit in machine int64_t"));
768  }
769  return result;
770  }
771 
778  uint64_t get_numeral_uint64() const {
779  assert(is_numeral());
780  uint64_t result = 0;
781  if (!is_numeral_u64(result)) {
782  assert(ctx().enable_exceptions());
783  if (!ctx().enable_exceptions()) return 0;
784  Z3_THROW(exception("numeral does not fit in machine uint64_t"));
785  }
786  return result;
787  }
788 
790  return Z3_get_bool_value(ctx(), m_ast);
791  }
792 
793  expr numerator() const {
794  assert(is_numeral());
795  Z3_ast r = Z3_get_numerator(ctx(), m_ast);
796  check_error();
797  return expr(ctx(),r);
798  }
799 
800 
801  expr denominator() const {
802  assert(is_numeral());
803  Z3_ast r = Z3_get_denominator(ctx(), m_ast);
804  check_error();
805  return expr(ctx(),r);
806  }
807 
808  operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
809 
816  func_decl decl() const { Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }
823  unsigned num_args() const { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
831  expr arg(unsigned i) const { Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }
832 
838  expr body() const { assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
839 
845  friend expr operator!(expr const & a);
846 
847 
854  friend expr operator&&(expr const & a, expr const & b);
855 
856 
863  friend expr operator&&(expr const & a, bool b);
870  friend expr operator&&(bool a, expr const & b);
871 
878  friend expr operator||(expr const & a, expr const & b);
885  friend expr operator||(expr const & a, bool b);
886 
893  friend expr operator||(bool a, expr const & b);
894 
895  friend expr implies(expr const & a, expr const & b);
896  friend expr implies(expr const & a, bool b);
897  friend expr implies(bool a, expr const & b);
898 
899  friend expr mk_or(expr_vector const& args);
900  friend expr mk_and(expr_vector const& args);
901 
902  friend expr ite(expr const & c, expr const & t, expr const & e);
903 
904  friend expr distinct(expr_vector const& args);
905  friend expr concat(expr const& a, expr const& b);
906  friend expr concat(expr_vector const& args);
907 
908  friend expr operator==(expr const & a, expr const & b);
909  friend expr operator==(expr const & a, int b);
910  friend expr operator==(int a, expr const & b);
911 
912  friend expr operator!=(expr const & a, expr const & b);
913  friend expr operator!=(expr const & a, int b);
914  friend expr operator!=(int a, expr const & b);
915 
916  friend expr operator+(expr const & a, expr const & b);
917  friend expr operator+(expr const & a, int b);
918  friend expr operator+(int a, expr const & b);
919  friend expr sum(expr_vector const& args);
920 
921  friend expr operator*(expr const & a, expr const & b);
922  friend expr operator*(expr const & a, int b);
923  friend expr operator*(int a, expr const & b);
924 
925  /* \brief Power operator */
926  friend expr pw(expr const & a, expr const & b);
927  friend expr pw(expr const & a, int b);
928  friend expr pw(int a, expr const & b);
929 
930  /* \brief mod operator */
931  friend expr mod(expr const& a, expr const& b);
932  friend expr mod(expr const& a, int b);
933  friend expr mod(int a, expr const& b);
934 
935  /* \brief rem operator */
936  friend expr rem(expr const& a, expr const& b);
937  friend expr rem(expr const& a, int b);
938  friend expr rem(int a, expr const& b);
939 
940  friend expr is_int(expr const& e);
941 
942  friend expr operator/(expr const & a, expr const & b);
943  friend expr operator/(expr const & a, int b);
944  friend expr operator/(int a, expr const & b);
945 
946  friend expr operator-(expr const & a);
947 
948  friend expr operator-(expr const & a, expr const & b);
949  friend expr operator-(expr const & a, int b);
950  friend expr operator-(int a, expr const & b);
951 
952  friend expr operator<=(expr const & a, expr const & b);
953  friend expr operator<=(expr const & a, int b);
954  friend expr operator<=(int a, expr const & b);
955 
956 
957  friend expr operator>=(expr const & a, expr const & b);
958  friend expr operator>=(expr const & a, int b);
959  friend expr operator>=(int a, expr const & b);
960 
961  friend expr operator<(expr const & a, expr const & b);
962  friend expr operator<(expr const & a, int b);
963  friend expr operator<(int a, expr const & b);
964 
965  friend expr operator>(expr const & a, expr const & b);
966  friend expr operator>(expr const & a, int b);
967  friend expr operator>(int a, expr const & b);
968 
969  friend expr pble(expr_vector const& es, int const * coeffs, int bound);
970  friend expr pbge(expr_vector const& es, int const * coeffs, int bound);
971  friend expr pbeq(expr_vector const& es, int const * coeffs, int bound);
972  friend expr atmost(expr_vector const& es, unsigned bound);
973  friend expr atleast(expr_vector const& es, unsigned bound);
974 
975  friend expr operator&(expr const & a, expr const & b);
976  friend expr operator&(expr const & a, int b);
977  friend expr operator&(int a, expr const & b);
978 
979  friend expr operator^(expr const & a, expr const & b);
980  friend expr operator^(expr const & a, int b);
981  friend expr operator^(int a, expr const & b);
982 
983  friend expr operator|(expr const & a, expr const & b);
984  friend expr operator|(expr const & a, int b);
985  friend expr operator|(int a, expr const & b);
986  friend expr nand(expr const& a, expr const& b);
987  friend expr nor(expr const& a, expr const& b);
988  friend expr xnor(expr const& a, expr const& b);
989 
990  expr rotate_left(unsigned i) { Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
991  expr rotate_right(unsigned i) { Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
992  expr repeat(unsigned i) { Z3_ast r = Z3_mk_repeat(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
993 
994  friend expr operator~(expr const & a);
995  expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }
996  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)); }
997  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)); }
998 
1004  expr extract(expr const& offset, expr const& length) const {
1005  check_context(*this, offset); check_context(offset, length);
1006  Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
1007  }
1008  expr replace(expr const& src, expr const& dst) const {
1009  check_context(*this, src); check_context(src, dst);
1010  Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
1011  check_error();
1012  return expr(ctx(), r);
1013  }
1014  expr unit() const {
1015  Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
1016  check_error();
1017  return expr(ctx(), r);
1018  }
1019  expr contains(expr const& s) {
1020  check_context(*this, s);
1021  Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
1022  check_error();
1023  return expr(ctx(), r);
1024  }
1025  expr at(expr const& index) const {
1026  check_context(*this, index);
1027  Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
1028  check_error();
1029  return expr(ctx(), r);
1030  }
1031  expr length() const {
1032  Z3_ast r = Z3_mk_seq_length(ctx(), *this);
1033  check_error();
1034  return expr(ctx(), r);
1035  }
1036  expr stoi() const {
1037  Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
1038  check_error();
1039  return expr(ctx(), r);
1040  }
1041  expr itos() const {
1042  Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
1043  check_error();
1044  return expr(ctx(), r);
1045  }
1046 
1047  friend expr range(expr const& lo, expr const& hi);
1051  expr loop(unsigned lo) {
1052  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0);
1053  check_error();
1054  return expr(ctx(), r);
1055  }
1056  expr loop(unsigned lo, unsigned hi) {
1057  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi);
1058  check_error();
1059  return expr(ctx(), r);
1060  }
1061 
1062 
1066  expr simplify() const { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
1070  expr simplify(params const & p) const { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
1071 
1075  expr substitute(expr_vector const& src, expr_vector const& dst);
1076 
1080  expr substitute(expr_vector const& dst);
1081 
1082  };
1083 
1084 #define _Z3_MK_BIN_(a, b, binop) \
1085  check_context(a, b); \
1086  Z3_ast r = binop(a.ctx(), a, b); \
1087  a.check_error(); \
1088  return expr(a.ctx(), r); \
1089 
1090 
1091  inline expr implies(expr const & a, expr const & b) {
1092  assert(a.is_bool() && b.is_bool());
1093  _Z3_MK_BIN_(a, b, Z3_mk_implies);
1094  }
1095  inline expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); }
1096  inline expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); }
1097 
1098 
1099  inline expr pw(expr const & a, expr const & b) { _Z3_MK_BIN_(a, b, Z3_mk_power); }
1100  inline expr pw(expr const & a, int b) { return pw(a, a.ctx().num_val(b, a.get_sort())); }
1101  inline expr pw(int a, expr const & b) { return pw(b.ctx().num_val(a, b.get_sort()), b); }
1102 
1103  inline expr mod(expr const& a, expr const& b) { _Z3_MK_BIN_(a, b, Z3_mk_mod); }
1104  inline expr mod(expr const & a, int b) { return mod(a, a.ctx().num_val(b, a.get_sort())); }
1105  inline expr mod(int a, expr const & b) { return mod(b.ctx().num_val(a, b.get_sort()), b); }
1106 
1107  inline expr rem(expr const& a, expr const& b) { _Z3_MK_BIN_(a, b, Z3_mk_rem); }
1108  inline expr rem(expr const & a, int b) { return rem(a, a.ctx().num_val(b, a.get_sort())); }
1109  inline expr rem(int a, expr const & b) { return rem(b.ctx().num_val(a, b.get_sort()), b); }
1110 
1111 #undef _Z3_MK_BIN_
1112 
1113 #define _Z3_MK_UN_(a, mkun) \
1114  Z3_ast r = mkun(a.ctx(), a); \
1115  a.check_error(); \
1116  return expr(a.ctx(), r); \
1117 
1118 
1119  inline expr operator!(expr const & a) { assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); }
1120 
1121  inline expr is_int(expr const& e) { _Z3_MK_UN_(e, Z3_mk_is_int); }
1122 
1123 #undef _Z3_MK_UN_
1124 
1125  inline expr operator&&(expr const & a, expr const & b) {
1126  check_context(a, b);
1127  assert(a.is_bool() && b.is_bool());
1128  Z3_ast args[2] = { a, b };
1129  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1130  a.check_error();
1131  return expr(a.ctx(), r);
1132  }
1133 
1134  inline expr operator&&(expr const & a, bool b) { return a && a.ctx().bool_val(b); }
1135  inline expr operator&&(bool a, expr const & b) { return b.ctx().bool_val(a) && b; }
1136 
1137  inline expr operator||(expr const & a, expr const & b) {
1138  check_context(a, b);
1139  assert(a.is_bool() && b.is_bool());
1140  Z3_ast args[2] = { a, b };
1141  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1142  a.check_error();
1143  return expr(a.ctx(), r);
1144  }
1145 
1146  inline expr operator||(expr const & a, bool b) { return a || a.ctx().bool_val(b); }
1147 
1148  inline expr operator||(bool a, expr const & b) { return b.ctx().bool_val(a) || b; }
1149 
1150  inline expr operator==(expr const & a, expr const & b) {
1151  check_context(a, b);
1152  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1153  a.check_error();
1154  return expr(a.ctx(), r);
1155  }
1156  inline expr operator==(expr const & a, int b) { assert(a.is_arith() || a.is_bv()); return a == a.ctx().num_val(b, a.get_sort()); }
1157  inline expr operator==(int a, expr const & b) { assert(b.is_arith() || b.is_bv()); return b.ctx().num_val(a, b.get_sort()) == b; }
1158 
1159  inline expr operator!=(expr const & a, expr const & b) {
1160  check_context(a, b);
1161  Z3_ast args[2] = { a, b };
1162  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1163  a.check_error();
1164  return expr(a.ctx(), r);
1165  }
1166  inline expr operator!=(expr const & a, int b) { assert(a.is_arith() || a.is_bv()); return a != a.ctx().num_val(b, a.get_sort()); }
1167  inline expr operator!=(int a, expr const & b) { assert(b.is_arith() || b.is_bv()); return b.ctx().num_val(a, b.get_sort()) != b; }
1168 
1169  inline expr operator+(expr const & a, expr const & b) {
1170  check_context(a, b);
1171  Z3_ast r = 0;
1172  if (a.is_arith() && b.is_arith()) {
1173  Z3_ast args[2] = { a, b };
1174  r = Z3_mk_add(a.ctx(), 2, args);
1175  }
1176  else if (a.is_bv() && b.is_bv()) {
1177  r = Z3_mk_bvadd(a.ctx(), a, b);
1178  }
1179  else if (a.is_seq() && b.is_seq()) {
1180  return concat(a, b);
1181  }
1182  else if (a.is_re() && b.is_re()) {
1183  Z3_ast _args[2] = { a, b };
1184  r = Z3_mk_re_union(a.ctx(), 2, _args);
1185  }
1186  else {
1187  // operator is not supported by given arguments.
1188  assert(false);
1189  }
1190  a.check_error();
1191  return expr(a.ctx(), r);
1192  }
1193  inline expr operator+(expr const & a, int b) { return a + a.ctx().num_val(b, a.get_sort()); }
1194  inline expr operator+(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) + b; }
1195 
1196  inline expr operator*(expr const & a, expr const & b) {
1197  check_context(a, b);
1198  Z3_ast r = 0;
1199  if (a.is_arith() && b.is_arith()) {
1200  Z3_ast args[2] = { a, b };
1201  r = Z3_mk_mul(a.ctx(), 2, args);
1202  }
1203  else if (a.is_bv() && b.is_bv()) {
1204  r = Z3_mk_bvmul(a.ctx(), a, b);
1205  }
1206  else {
1207  // operator is not supported by given arguments.
1208  assert(false);
1209  }
1210  a.check_error();
1211  return expr(a.ctx(), r);
1212  }
1213  inline expr operator*(expr const & a, int b) { return a * a.ctx().num_val(b, a.get_sort()); }
1214  inline expr operator*(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) * b; }
1215 
1216 
1217  inline expr operator>=(expr const & a, expr const & b) {
1218  check_context(a, b);
1219  Z3_ast r = 0;
1220  if (a.is_arith() && b.is_arith()) {
1221  r = Z3_mk_ge(a.ctx(), a, b);
1222  }
1223  else if (a.is_bv() && b.is_bv()) {
1224  r = Z3_mk_bvsge(a.ctx(), a, b);
1225  }
1226  else {
1227  // operator is not supported by given arguments.
1228  assert(false);
1229  }
1230  a.check_error();
1231  return expr(a.ctx(), r);
1232  }
1233 
1234  inline expr operator/(expr const & a, expr const & b) {
1235  check_context(a, b);
1236  Z3_ast r = 0;
1237  if (a.is_arith() && b.is_arith()) {
1238  r = Z3_mk_div(a.ctx(), a, b);
1239  }
1240  else if (a.is_bv() && b.is_bv()) {
1241  r = Z3_mk_bvsdiv(a.ctx(), a, b);
1242  }
1243  else {
1244  // operator is not supported by given arguments.
1245  assert(false);
1246  }
1247  a.check_error();
1248  return expr(a.ctx(), r);
1249  }
1250  inline expr operator/(expr const & a, int b) { return a / a.ctx().num_val(b, a.get_sort()); }
1251  inline expr operator/(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) / b; }
1252 
1253  inline expr operator-(expr const & a) {
1254  Z3_ast r = 0;
1255  if (a.is_arith()) {
1256  r = Z3_mk_unary_minus(a.ctx(), a);
1257  }
1258  else if (a.is_bv()) {
1259  r = Z3_mk_bvneg(a.ctx(), a);
1260  }
1261  else {
1262  // operator is not supported by given arguments.
1263  assert(false);
1264  }
1265  a.check_error();
1266  return expr(a.ctx(), r);
1267  }
1268 
1269  inline expr operator-(expr const & a, expr const & b) {
1270  check_context(a, b);
1271  Z3_ast r = 0;
1272  if (a.is_arith() && b.is_arith()) {
1273  Z3_ast args[2] = { a, b };
1274  r = Z3_mk_sub(a.ctx(), 2, args);
1275  }
1276  else if (a.is_bv() && b.is_bv()) {
1277  r = Z3_mk_bvsub(a.ctx(), a, b);
1278  }
1279  else {
1280  // operator is not supported by given arguments.
1281  assert(false);
1282  }
1283  a.check_error();
1284  return expr(a.ctx(), r);
1285  }
1286  inline expr operator-(expr const & a, int b) { return a - a.ctx().num_val(b, a.get_sort()); }
1287  inline expr operator-(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) - b; }
1288 
1289  inline expr operator<=(expr const & a, expr const & b) {
1290  check_context(a, b);
1291  Z3_ast r = 0;
1292  if (a.is_arith() && b.is_arith()) {
1293  r = Z3_mk_le(a.ctx(), a, b);
1294  }
1295  else if (a.is_bv() && b.is_bv()) {
1296  r = Z3_mk_bvsle(a.ctx(), a, b);
1297  }
1298  else {
1299  // operator is not supported by given arguments.
1300  assert(false);
1301  }
1302  a.check_error();
1303  return expr(a.ctx(), r);
1304  }
1305  inline expr operator<=(expr const & a, int b) { return a <= a.ctx().num_val(b, a.get_sort()); }
1306  inline expr operator<=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) <= b; }
1307 
1308  inline expr operator>=(expr const & a, int b) { return a >= a.ctx().num_val(b, a.get_sort()); }
1309  inline expr operator>=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) >= b; }
1310 
1311  inline expr operator<(expr const & a, expr const & b) {
1312  check_context(a, b);
1313  Z3_ast r = 0;
1314  if (a.is_arith() && b.is_arith()) {
1315  r = Z3_mk_lt(a.ctx(), a, b);
1316  }
1317  else if (a.is_bv() && b.is_bv()) {
1318  r = Z3_mk_bvslt(a.ctx(), a, b);
1319  }
1320  else {
1321  // operator is not supported by given arguments.
1322  assert(false);
1323  }
1324  a.check_error();
1325  return expr(a.ctx(), r);
1326  }
1327  inline expr operator<(expr const & a, int b) { return a < a.ctx().num_val(b, a.get_sort()); }
1328  inline expr operator<(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) < b; }
1329 
1330  inline expr operator>(expr const & a, expr const & b) {
1331  check_context(a, b);
1332  Z3_ast r = 0;
1333  if (a.is_arith() && b.is_arith()) {
1334  r = Z3_mk_gt(a.ctx(), a, b);
1335  }
1336  else if (a.is_bv() && b.is_bv()) {
1337  r = Z3_mk_bvsgt(a.ctx(), a, b);
1338  }
1339  else {
1340  // operator is not supported by given arguments.
1341  assert(false);
1342  }
1343  a.check_error();
1344  return expr(a.ctx(), r);
1345  }
1346  inline expr operator>(expr const & a, int b) { return a > a.ctx().num_val(b, a.get_sort()); }
1347  inline expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > b; }
1348 
1349  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); }
1350  inline expr operator&(expr const & a, int b) { return a & a.ctx().num_val(b, a.get_sort()); }
1351  inline expr operator&(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) & b; }
1352 
1353  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); }
1354  inline expr operator^(expr const & a, int b) { return a ^ a.ctx().num_val(b, a.get_sort()); }
1355  inline expr operator^(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) ^ b; }
1356 
1357  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); }
1358  inline expr operator|(expr const & a, int b) { return a | a.ctx().num_val(b, a.get_sort()); }
1359  inline expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; }
1360 
1361  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); }
1362  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); }
1363  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); }
1364 
1365  inline expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
1366 
1367 
1368 
1375  inline expr ite(expr const & c, expr const & t, expr const & e) {
1376  check_context(c, t); check_context(c, e);
1377  assert(c.is_bool());
1378  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
1379  c.check_error();
1380  return expr(c.ctx(), r);
1381  }
1382 
1383 
1388  inline expr to_expr(context & c, Z3_ast a) {
1389  c.check_error();
1390  assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
1391  Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
1392  Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
1394  return expr(c, a);
1395  }
1396 
1397  inline sort to_sort(context & c, Z3_sort s) {
1398  c.check_error();
1399  return sort(c, s);
1400  }
1401 
1402  inline func_decl to_func_decl(context & c, Z3_func_decl f) {
1403  c.check_error();
1404  return func_decl(c, f);
1405  }
1406 
1410  inline expr ule(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
1411  inline expr ule(expr const & a, int b) { return ule(a, a.ctx().num_val(b, a.get_sort())); }
1412  inline expr ule(int a, expr const & b) { return ule(b.ctx().num_val(a, b.get_sort()), b); }
1416  inline expr ult(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }
1417  inline expr ult(expr const & a, int b) { return ult(a, a.ctx().num_val(b, a.get_sort())); }
1418  inline expr ult(int a, expr const & b) { return ult(b.ctx().num_val(a, b.get_sort()), b); }
1422  inline expr uge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }
1423  inline expr uge(expr const & a, int b) { return uge(a, a.ctx().num_val(b, a.get_sort())); }
1424  inline expr uge(int a, expr const & b) { return uge(b.ctx().num_val(a, b.get_sort()), b); }
1428  inline expr ugt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
1429  inline expr ugt(expr const & a, int b) { return ugt(a, a.ctx().num_val(b, a.get_sort())); }
1430  inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), b); }
1434  inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
1435  inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); }
1436  inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); }
1437 
1441  inline expr srem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsrem(a.ctx(), a, b)); }
1442  inline expr srem(expr const & a, int b) { return srem(a, a.ctx().num_val(b, a.get_sort())); }
1443  inline expr srem(int a, expr const & b) { return srem(b.ctx().num_val(a, b.get_sort()), b); }
1444 
1448  inline expr smod(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsmod(a.ctx(), a, b)); }
1449  inline expr smod(expr const & a, int b) { return smod(a, a.ctx().num_val(b, a.get_sort())); }
1450  inline expr smod(int a, expr const & b) { return smod(b.ctx().num_val(a, b.get_sort()), b); }
1451 
1455  inline expr urem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvurem(a.ctx(), a, b)); }
1456  inline expr urem(expr const & a, int b) { return urem(a, a.ctx().num_val(b, a.get_sort())); }
1457  inline expr urem(int a, expr const & b) { return urem(b.ctx().num_val(a, b.get_sort()), b); }
1458 
1462  inline expr shl(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvshl(a.ctx(), a, b)); }
1463  inline expr shl(expr const & a, int b) { return shl(a, a.ctx().num_val(b, a.get_sort())); }
1464  inline expr shl(int a, expr const & b) { return shl(b.ctx().num_val(a, b.get_sort()), b); }
1465 
1469  inline expr lshr(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvlshr(a.ctx(), a, b)); }
1470  inline expr lshr(expr const & a, int b) { return lshr(a, a.ctx().num_val(b, a.get_sort())); }
1471  inline expr lshr(int a, expr const & b) { return lshr(b.ctx().num_val(a, b.get_sort()), b); }
1472 
1476  inline expr ashr(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvashr(a.ctx(), a, b)); }
1477  inline expr ashr(expr const & a, int b) { return ashr(a, a.ctx().num_val(b, a.get_sort())); }
1478  inline expr ashr(int a, expr const & b) { return ashr(b.ctx().num_val(a, b.get_sort()), b); }
1479 
1483  inline expr zext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_zero_ext(a.ctx(), i, a)); }
1484 
1488  inline expr sext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_sign_ext(a.ctx(), i, a)); }
1489 
1490  template<typename T> class cast_ast;
1491 
1492  template<> class cast_ast<ast> {
1493  public:
1494  ast operator()(context & c, Z3_ast a) { return ast(c, a); }
1495  };
1496 
1497  template<> class cast_ast<expr> {
1498  public:
1499  expr operator()(context & c, Z3_ast a) {
1500  assert(Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
1501  Z3_get_ast_kind(c, a) == Z3_APP_AST ||
1503  Z3_get_ast_kind(c, a) == Z3_VAR_AST);
1504  return expr(c, a);
1505  }
1506  };
1507 
1508  template<> class cast_ast<sort> {
1509  public:
1510  sort operator()(context & c, Z3_ast a) {
1511  assert(Z3_get_ast_kind(c, a) == Z3_SORT_AST);
1512  return sort(c, reinterpret_cast<Z3_sort>(a));
1513  }
1514  };
1515 
1516  template<> class cast_ast<func_decl> {
1517  public:
1518  func_decl operator()(context & c, Z3_ast a) {
1519  assert(Z3_get_ast_kind(c, a) == Z3_FUNC_DECL_AST);
1520  return func_decl(c, reinterpret_cast<Z3_func_decl>(a));
1521  }
1522  };
1523 
1524  template<typename T>
1525  class ast_vector_tpl : public object {
1526  Z3_ast_vector m_vector;
1527  void init(Z3_ast_vector v) { Z3_ast_vector_inc_ref(ctx(), v); m_vector = v; }
1528  public:
1530  ast_vector_tpl(context & c, Z3_ast_vector v):object(c) { init(v); }
1531  ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
1532  ~ast_vector_tpl() { Z3_ast_vector_dec_ref(ctx(), m_vector); }
1533  operator Z3_ast_vector() const { return m_vector; }
1534  unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); }
1535  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); }
1536  void push_back(T const & e) { Z3_ast_vector_push(ctx(), m_vector, e); check_error(); }
1537  void resize(unsigned sz) { Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }
1538  T back() const { return operator[](size() - 1); }
1539  void pop_back() { assert(size() > 0); resize(size() - 1); }
1540  bool empty() const { return size() == 0; }
1542  Z3_ast_vector_inc_ref(s.ctx(), s.m_vector);
1543  Z3_ast_vector_dec_ref(ctx(), m_vector);
1544  m_ctx = s.m_ctx;
1545  m_vector = s.m_vector;
1546  return *this;
1547  }
1548  /*
1549  Disabled pending C++98 build upgrade
1550  bool contains(T const& x) const {
1551  for (T y : *this) if (eq(x, y)) return true;
1552  return false;
1553  }
1554  */
1555 
1556  class iterator {
1557  ast_vector_tpl const* m_vector;
1558  unsigned m_index;
1559  public:
1560  iterator(ast_vector_tpl const* v, unsigned i): m_vector(v), m_index(i) {}
1561  iterator(iterator& other): m_vector(other.m_vector), m_index(other.m_index) {}
1562  iterator operator=(iterator const& other) { m_vector = other.m_vector; m_index = other.m_index; return *this; }
1563 
1564  bool operator==(iterator const& other) {
1565  return other.m_index == m_index;
1566  };
1567  bool operator!=(iterator const& other) {
1568  return other.m_index != m_index;
1569  };
1571  ++m_index;
1572  return *this;
1573  }
1574  iterator operator++(int) { iterator tmp = *this; ++m_index; return tmp; }
1575  T * operator->() const { return &(operator*()); }
1576  T operator*() const { return (*m_vector)[m_index]; }
1577  };
1578  iterator begin() const { return iterator(this, 0); }
1579  iterator end() const { return iterator(this, size()); }
1580  friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
1581  };
1582 
1583 
1584  template<typename T>
1585  template<typename T2>
1587  m_array = new T[v.size()];
1588  m_size = v.size();
1589  for (unsigned i = 0; i < m_size; i++) {
1590  m_array[i] = v[i];
1591  }
1592  }
1593 
1594  // Basic functions for creating quantified formulas.
1595  // The C API should be used for creating quantifiers with patterns, weights, many variables, etc.
1596  inline expr forall(expr const & x, expr const & b) {
1597  check_context(x, b);
1598  Z3_app vars[] = {(Z3_app) x};
1599  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1600  }
1601  inline expr forall(expr const & x1, expr const & x2, expr const & b) {
1602  check_context(x1, b); check_context(x2, b);
1603  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1604  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1605  }
1606  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
1607  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1608  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1609  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1610  }
1611  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
1612  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1613  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1614  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1615  }
1616  inline expr forall(expr_vector const & xs, expr const & b) {
1617  array<Z3_app> vars(xs);
1618  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);
1619  }
1620  inline expr exists(expr const & x, expr const & b) {
1621  check_context(x, b);
1622  Z3_app vars[] = {(Z3_app) x};
1623  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1624  }
1625  inline expr exists(expr const & x1, expr const & x2, expr const & b) {
1626  check_context(x1, b); check_context(x2, b);
1627  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1628  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1629  }
1630  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
1631  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1632  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1633  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1634  }
1635  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
1636  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1637  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1638  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1639  }
1640  inline expr exists(expr_vector const & xs, expr const & b) {
1641  array<Z3_app> vars(xs);
1642  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);
1643  }
1644  inline expr pble(expr_vector const& es, int const* coeffs, int bound) {
1645  assert(es.size() > 0);
1646  context& ctx = es[0].ctx();
1647  array<Z3_ast> _es(es);
1648  Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
1649  ctx.check_error();
1650  return expr(ctx, r);
1651  }
1652  inline expr pbge(expr_vector const& es, int const* coeffs, int bound) {
1653  assert(es.size() > 0);
1654  context& ctx = es[0].ctx();
1655  array<Z3_ast> _es(es);
1656  Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
1657  ctx.check_error();
1658  return expr(ctx, r);
1659  }
1660  inline expr pbeq(expr_vector const& es, int const* coeffs, int bound) {
1661  assert(es.size() > 0);
1662  context& ctx = es[0].ctx();
1663  array<Z3_ast> _es(es);
1664  Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
1665  ctx.check_error();
1666  return expr(ctx, r);
1667  }
1668  inline expr atmost(expr_vector const& es, unsigned bound) {
1669  assert(es.size() > 0);
1670  context& ctx = es[0].ctx();
1671  array<Z3_ast> _es(es);
1672  Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
1673  ctx.check_error();
1674  return expr(ctx, r);
1675  }
1676  inline expr atleast(expr_vector const& es, unsigned bound) {
1677  assert(es.size() > 0);
1678  context& ctx = es[0].ctx();
1679  array<Z3_ast> _es(es);
1680  Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
1681  ctx.check_error();
1682  return expr(ctx, r);
1683  }
1684  inline expr sum(expr_vector const& args) {
1685  assert(args.size() > 0);
1686  context& ctx = args[0].ctx();
1687  array<Z3_ast> _args(args);
1688  Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
1689  ctx.check_error();
1690  return expr(ctx, r);
1691  }
1692 
1693  inline expr distinct(expr_vector const& args) {
1694  assert(args.size() > 0);
1695  context& ctx = args[0].ctx();
1696  array<Z3_ast> _args(args);
1697  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
1698  ctx.check_error();
1699  return expr(ctx, r);
1700  }
1701 
1702  inline expr concat(expr const& a, expr const& b) {
1703  check_context(a, b);
1704  Z3_ast r;
1705  if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
1706  Z3_ast _args[2] = { a, b };
1707  r = Z3_mk_seq_concat(a.ctx(), 2, _args);
1708  }
1709  else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
1710  Z3_ast _args[2] = { a, b };
1711  r = Z3_mk_re_concat(a.ctx(), 2, _args);
1712  }
1713  else {
1714  r = Z3_mk_concat(a.ctx(), a, b);
1715  }
1716  a.ctx().check_error();
1717  return expr(a.ctx(), r);
1718  }
1719 
1720  inline expr concat(expr_vector const& args) {
1721  Z3_ast r;
1722  assert(args.size() > 0);
1723  if (args.size() == 1) {
1724  return args[0];
1725  }
1726  context& ctx = args[0].ctx();
1727  array<Z3_ast> _args(args);
1728  if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
1729  r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
1730  }
1731  else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
1732  r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
1733  }
1734  else {
1735  r = _args[args.size()-1];
1736  for (unsigned i = args.size()-1; i > 0; ) {
1737  --i;
1738  r = Z3_mk_concat(ctx, _args[i], r);
1739  ctx.check_error();
1740  }
1741  }
1742  ctx.check_error();
1743  return expr(ctx, r);
1744  }
1745 
1746  inline expr mk_or(expr_vector const& args) {
1747  array<Z3_ast> _args(args);
1748  Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
1749  args.check_error();
1750  return expr(args.ctx(), r);
1751  }
1752  inline expr mk_and(expr_vector const& args) {
1753  array<Z3_ast> _args(args);
1754  Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
1755  args.check_error();
1756  return expr(args.ctx(), r);
1757  }
1758 
1759 
1760  class func_entry : public object {
1761  Z3_func_entry m_entry;
1762  void init(Z3_func_entry e) {
1763  m_entry = e;
1764  Z3_func_entry_inc_ref(ctx(), m_entry);
1765  }
1766  public:
1767  func_entry(context & c, Z3_func_entry e):object(c) { init(e); }
1768  func_entry(func_entry const & s):object(s) { init(s.m_entry); }
1769  ~func_entry() { Z3_func_entry_dec_ref(ctx(), m_entry); }
1770  operator Z3_func_entry() const { return m_entry; }
1772  Z3_func_entry_inc_ref(s.ctx(), s.m_entry);
1773  Z3_func_entry_dec_ref(ctx(), m_entry);
1774  m_ctx = s.m_ctx;
1775  m_entry = s.m_entry;
1776  return *this;
1777  }
1778  expr value() const { Z3_ast r = Z3_func_entry_get_value(ctx(), m_entry); check_error(); return expr(ctx(), r); }
1779  unsigned num_args() const { unsigned r = Z3_func_entry_get_num_args(ctx(), m_entry); check_error(); return r; }
1780  expr arg(unsigned i) const { Z3_ast r = Z3_func_entry_get_arg(ctx(), m_entry, i); check_error(); return expr(ctx(), r); }
1781  };
1782 
1783  class func_interp : public object {
1784  Z3_func_interp m_interp;
1785  void init(Z3_func_interp e) {
1786  m_interp = e;
1787  Z3_func_interp_inc_ref(ctx(), m_interp);
1788  }
1789  public:
1790  func_interp(context & c, Z3_func_interp e):object(c) { init(e); }
1791  func_interp(func_interp const & s):object(s) { init(s.m_interp); }
1792  ~func_interp() { Z3_func_interp_dec_ref(ctx(), m_interp); }
1793  operator Z3_func_interp() const { return m_interp; }
1795  Z3_func_interp_inc_ref(s.ctx(), s.m_interp);
1796  Z3_func_interp_dec_ref(ctx(), m_interp);
1797  m_ctx = s.m_ctx;
1798  m_interp = s.m_interp;
1799  return *this;
1800  }
1801  expr else_value() const { Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), r); }
1802  unsigned num_entries() const { unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }
1803  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); }
1804  void add_entry(expr_vector const& args, expr& value) {
1805  Z3_func_interp_add_entry(ctx(), m_interp, args, value);
1806  check_error();
1807  }
1808  void set_else(expr& value) {
1809  Z3_func_interp_set_else(ctx(), m_interp, value);
1810  check_error();
1811  }
1812  };
1813 
1814  class model : public object {
1815  Z3_model m_model;
1816  void init(Z3_model m) {
1817  m_model = m;
1818  Z3_model_inc_ref(ctx(), m);
1819  }
1820  public:
1821  struct translate {};
1822  model(context & c):object(c) { init(Z3_mk_model(c)); }
1823  model(context & c, Z3_model m):object(c) { init(m); }
1824  model(model const & s):object(s) { init(s.m_model); }
1825  model(model& src, context& dst, translate) : object(dst) { init(Z3_model_translate(src.ctx(), src, dst)); }
1826  ~model() { Z3_model_dec_ref(ctx(), m_model); }
1827  operator Z3_model() const { return m_model; }
1828  model & operator=(model const & s) {
1829  Z3_model_inc_ref(s.ctx(), s.m_model);
1830  Z3_model_dec_ref(ctx(), m_model);
1831  m_ctx = s.m_ctx;
1832  m_model = s.m_model;
1833  return *this;
1834  }
1835 
1836  expr eval(expr const & n, bool model_completion=false) const {
1837  check_context(*this, n);
1838  Z3_ast r = 0;
1839  Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
1840  check_error();
1841  if (status == Z3_FALSE && ctx().enable_exceptions())
1842  Z3_THROW(exception("failed to evaluate expression"));
1843  return expr(ctx(), r);
1844  }
1845 
1846  unsigned num_consts() const { return Z3_model_get_num_consts(ctx(), m_model); }
1847  unsigned num_funcs() const { return Z3_model_get_num_funcs(ctx(), m_model); }
1848  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); }
1849  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); }
1850  unsigned size() const { return num_consts() + num_funcs(); }
1851  func_decl operator[](int i) const {
1852  assert(0 <= i);
1853  return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
1854  }
1855 
1856  // returns interpretation of constant declaration c.
1857  // If c is not assigned any value in the model it returns
1858  // an expression with a null ast reference.
1860  check_context(*this, c);
1861  Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);
1862  check_error();
1863  return expr(ctx(), r);
1864  }
1866  check_context(*this, f);
1867  Z3_func_interp r = Z3_model_get_func_interp(ctx(), m_model, f);
1868  check_error();
1869  return func_interp(ctx(), r);
1870  }
1871 
1872  // returns true iff the model contains an interpretation
1873  // for function f.
1874  bool has_interp(func_decl f) const {
1875  check_context(*this, f);
1876  return 0 != Z3_model_has_interp(ctx(), m_model, f);
1877  }
1878 
1880  Z3_func_interp r = Z3_add_func_interp(ctx(), m_model, f, else_val);
1881  check_error();
1882  return func_interp(ctx(), r);
1883  }
1884 
1885  void add_const_interp(func_decl& f, expr& value) {
1886  Z3_add_const_interp(ctx(), m_model, f, value);
1887  check_error();
1888  }
1889 
1890  friend std::ostream & operator<<(std::ostream & out, model const & m);
1891  };
1892  inline std::ostream & operator<<(std::ostream & out, model const & m) { out << Z3_model_to_string(m.ctx(), m); return out; }
1893 
1894  class stats : public object {
1895  Z3_stats m_stats;
1896  void init(Z3_stats e) {
1897  m_stats = e;
1898  Z3_stats_inc_ref(ctx(), m_stats);
1899  }
1900  public:
1901  stats(context & c):object(c), m_stats(0) {}
1902  stats(context & c, Z3_stats e):object(c) { init(e); }
1903  stats(stats const & s):object(s) { init(s.m_stats); }
1904  ~stats() { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); }
1905  operator Z3_stats() const { return m_stats; }
1906  stats & operator=(stats const & s) {
1907  Z3_stats_inc_ref(s.ctx(), s.m_stats);
1908  if (m_stats) Z3_stats_dec_ref(ctx(), m_stats);
1909  m_ctx = s.m_ctx;
1910  m_stats = s.m_stats;
1911  return *this;
1912  }
1913  unsigned size() const { return Z3_stats_size(ctx(), m_stats); }
1914  std::string key(unsigned i) const { Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; }
1915  bool is_uint(unsigned i) const { Z3_bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r != 0; }
1916  bool is_double(unsigned i) const { Z3_bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r != 0; }
1917  unsigned uint_value(unsigned i) const { unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; }
1918  double double_value(unsigned i) const { double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
1919  friend std::ostream & operator<<(std::ostream & out, stats const & s);
1920  };
1921  inline std::ostream & operator<<(std::ostream & out, stats const & s) { out << Z3_stats_to_string(s.ctx(), s); return out; }
1922 
1923 
1924  inline std::ostream & operator<<(std::ostream & out, check_result r) {
1925  if (r == unsat) out << "unsat";
1926  else if (r == sat) out << "sat";
1927  else out << "unknown";
1928  return out;
1929  }
1930 
1931 
1932  class solver : public object {
1933  Z3_solver m_solver;
1934  void init(Z3_solver s) {
1935  m_solver = s;
1936  Z3_solver_inc_ref(ctx(), s);
1937  }
1938  public:
1939  struct simple {};
1940  struct translate {};
1941  solver(context & c):object(c) { init(Z3_mk_solver(c)); }
1943  solver(context & c, Z3_solver s):object(c) { init(s); }
1944  solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); }
1945  solver(context & c, solver const& src, translate): object(c) { init(Z3_solver_translate(src.ctx(), src, c)); }
1946  solver(solver const & s):object(s) { init(s.m_solver); }
1947  ~solver() { Z3_solver_dec_ref(ctx(), m_solver); }
1948  operator Z3_solver() const { return m_solver; }
1949  solver & operator=(solver const & s) {
1950  Z3_solver_inc_ref(s.ctx(), s.m_solver);
1951  Z3_solver_dec_ref(ctx(), m_solver);
1952  m_ctx = s.m_ctx;
1953  m_solver = s.m_solver;
1954  return *this;
1955  }
1956  void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
1957  void set(char const * k, bool v) { params p(ctx()); p.set(k, v); set(p); }
1958  void set(char const * k, unsigned v) { params p(ctx()); p.set(k, v); set(p); }
1959  void set(char const * k, double v) { params p(ctx()); p.set(k, v); set(p); }
1960  void set(char const * k, symbol const & v) { params p(ctx()); p.set(k, v); set(p); }
1961  void set(char const * k, char const* v) { params p(ctx()); p.set(k, v); set(p); }
1962  void push() { Z3_solver_push(ctx(), m_solver); check_error(); }
1963  void pop(unsigned n = 1) { Z3_solver_pop(ctx(), m_solver, n); check_error(); }
1964  void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); }
1965  void add(expr const & e) { assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); }
1966  void add(expr const & e, expr const & p) {
1967  assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
1968  Z3_solver_assert_and_track(ctx(), m_solver, e, p);
1969  check_error();
1970  }
1971  void add(expr const & e, char const * p) {
1972  add(e, ctx().bool_const(p));
1973  }
1974  // fails for some compilers:
1975  // void add(expr_vector const& v) { check_context(*this, v); for (expr e : v) add(e); }
1976  void from_file(char const* file) { Z3_solver_from_file(ctx(), m_solver, file); ctx().check_parser_error(); }
1977  void from_string(char const* s) { Z3_solver_from_string(ctx(), m_solver, s); ctx().check_parser_error(); }
1978 
1979  check_result check() { Z3_lbool r = Z3_solver_check(ctx(), m_solver); check_error(); return to_check_result(r); }
1980  check_result check(unsigned n, expr * const assumptions) {
1981  array<Z3_ast> _assumptions(n);
1982  for (unsigned i = 0; i < n; i++) {
1983  check_context(*this, assumptions[i]);
1984  _assumptions[i] = assumptions[i];
1985  }
1986  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
1987  check_error();
1988  return to_check_result(r);
1989  }
1990  check_result check(expr_vector assumptions) {
1991  unsigned n = assumptions.size();
1992  array<Z3_ast> _assumptions(n);
1993  for (unsigned i = 0; i < n; i++) {
1994  check_context(*this, assumptions[i]);
1995  _assumptions[i] = assumptions[i];
1996  }
1997  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
1998  check_error();
1999  return to_check_result(r);
2000  }
2001  model get_model() const { Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }
2002  check_result consequences(expr_vector& assumptions, expr_vector& vars, expr_vector& conseq) {
2003  Z3_lbool r = Z3_solver_get_consequences(ctx(), m_solver, assumptions, vars, conseq);
2004  check_error();
2005  return to_check_result(r);
2006  }
2007  std::string reason_unknown() const { Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }
2008  stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }
2009  expr_vector unsat_core() const { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2010  expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2011  expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
2012  friend std::ostream & operator<<(std::ostream & out, solver const & s);
2013 
2014  std::string to_smt2(char const* status = "unknown") {
2015  array<Z3_ast> es(assertions());
2016  Z3_ast const* fmls = es.ptr();
2017  Z3_ast fml = 0;
2018  unsigned sz = es.size();
2019  if (sz > 0) {
2020  --sz;
2021  fml = fmls[sz];
2022  }
2023  else {
2024  fml = ctx().bool_val(true);
2025  }
2026  return std::string(Z3_benchmark_to_smtlib_string(
2027  ctx(),
2028  "", "", status, "",
2029  sz,
2030  fmls,
2031  fml));
2032  }
2033 
2035 
2036  };
2037  inline std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
2038 
2039  class goal : public object {
2040  Z3_goal m_goal;
2041  void init(Z3_goal s) {
2042  m_goal = s;
2043  Z3_goal_inc_ref(ctx(), s);
2044  }
2045  public:
2046  goal(context & c, bool models=true, bool unsat_cores=false, bool proofs=false):object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); }
2047  goal(context & c, Z3_goal s):object(c) { init(s); }
2048  goal(goal const & s):object(s) { init(s.m_goal); }
2049  ~goal() { Z3_goal_dec_ref(ctx(), m_goal); }
2050  operator Z3_goal() const { return m_goal; }
2051  goal & operator=(goal const & s) {
2052  Z3_goal_inc_ref(s.ctx(), s.m_goal);
2053  Z3_goal_dec_ref(ctx(), m_goal);
2054  m_ctx = s.m_ctx;
2055  m_goal = s.m_goal;
2056  return *this;
2057  }
2058  void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
2059  // fails for some compilers:
2060  // void add(expr_vector const& v) { check_context(*this, v); for (expr e : v) add(e); }
2061  unsigned size() const { return Z3_goal_size(ctx(), m_goal); }
2062  expr operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
2063  Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); }
2064  bool inconsistent() const { return Z3_goal_inconsistent(ctx(), m_goal) != 0; }
2065  unsigned depth() const { return Z3_goal_depth(ctx(), m_goal); }
2066  void reset() { Z3_goal_reset(ctx(), m_goal); }
2067  unsigned num_exprs() const { return Z3_goal_num_exprs(ctx(), m_goal); }
2068  bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal) != 0; }
2069  bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal) != 0; }
2070  expr as_expr() const {
2071  unsigned n = size();
2072  if (n == 0)
2073  return ctx().bool_val(true);
2074  else if (n == 1)
2075  return operator[](0);
2076  else {
2077  array<Z3_ast> args(n);
2078  for (unsigned i = 0; i < n; i++)
2079  args[i] = operator[](i);
2080  return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
2081  }
2082  }
2083  friend std::ostream & operator<<(std::ostream & out, goal const & g);
2084  };
2085  inline std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; }
2086 
2087  class apply_result : public object {
2088  Z3_apply_result m_apply_result;
2089  void init(Z3_apply_result s) {
2090  m_apply_result = s;
2091  Z3_apply_result_inc_ref(ctx(), s);
2092  }
2093  public:
2094  apply_result(context & c, Z3_apply_result s):object(c) { init(s); }
2095  apply_result(apply_result const & s):object(s) { init(s.m_apply_result); }
2096  ~apply_result() { Z3_apply_result_dec_ref(ctx(), m_apply_result); }
2097  operator Z3_apply_result() const { return m_apply_result; }
2099  Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result);
2100  Z3_apply_result_dec_ref(ctx(), m_apply_result);
2101  m_ctx = s.m_ctx;
2102  m_apply_result = s.m_apply_result;
2103  return *this;
2104  }
2105  unsigned size() const { return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }
2106  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); }
2107  model convert_model(model const & m, unsigned i = 0) const {
2108  check_context(*this, m);
2109  Z3_model new_m = Z3_apply_result_convert_model(ctx(), m_apply_result, i, m);
2110  check_error();
2111  return model(ctx(), new_m);
2112  }
2113  expr as_expr() const {
2114  unsigned n = size();
2115  if (n == 0)
2116  return ctx().bool_val(true);
2117  else if (n == 1)
2118  return operator[](0).as_expr();
2119  else {
2120  array<Z3_ast> args(n);
2121  for (unsigned i = 0; i < n; i++)
2122  args[i] = operator[](i).as_expr();
2123  return expr(ctx(), Z3_mk_or(ctx(), n, args.ptr()));
2124  }
2125  }
2126  friend std::ostream & operator<<(std::ostream & out, apply_result const & r);
2127  };
2128  inline std::ostream & operator<<(std::ostream & out, apply_result const & r) { out << Z3_apply_result_to_string(r.ctx(), r); return out; }
2129 
2130  class tactic : public object {
2131  Z3_tactic m_tactic;
2132  void init(Z3_tactic s) {
2133  m_tactic = s;
2134  Z3_tactic_inc_ref(ctx(), s);
2135  }
2136  public:
2137  tactic(context & c, char const * name):object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); }
2138  tactic(context & c, Z3_tactic s):object(c) { init(s); }
2139  tactic(tactic const & s):object(s) { init(s.m_tactic); }
2140  ~tactic() { Z3_tactic_dec_ref(ctx(), m_tactic); }
2141  operator Z3_tactic() const { return m_tactic; }
2142  tactic & operator=(tactic const & s) {
2143  Z3_tactic_inc_ref(s.ctx(), s.m_tactic);
2144  Z3_tactic_dec_ref(ctx(), m_tactic);
2145  m_ctx = s.m_ctx;
2146  m_tactic = s.m_tactic;
2147  return *this;
2148  }
2149  solver mk_solver() const { Z3_solver r = Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error(); return solver(ctx(), r); }
2150  apply_result apply(goal const & g) const {
2151  check_context(*this, g);
2152  Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g);
2153  check_error();
2154  return apply_result(ctx(), r);
2155  }
2156  apply_result operator()(goal const & g) const {
2157  return apply(g);
2158  }
2159  std::string help() const { char const * r = Z3_tactic_get_help(ctx(), m_tactic); check_error(); return r; }
2160  friend tactic operator&(tactic const & t1, tactic const & t2);
2161  friend tactic operator|(tactic const & t1, tactic const & t2);
2162  friend tactic repeat(tactic const & t, unsigned max);
2163  friend tactic with(tactic const & t, params const & p);
2164  friend tactic try_for(tactic const & t, unsigned ms);
2165  friend tactic par_or(unsigned n, tactic const* tactics);
2166  friend tactic par_and_then(tactic const& t1, tactic const& t2);
2168  };
2169 
2170  inline tactic operator&(tactic const & t1, tactic const & t2) {
2171  check_context(t1, t2);
2172  Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
2173  t1.check_error();
2174  return tactic(t1.ctx(), r);
2175  }
2176 
2177  inline tactic operator|(tactic const & t1, tactic const & t2) {
2178  check_context(t1, t2);
2179  Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
2180  t1.check_error();
2181  return tactic(t1.ctx(), r);
2182  }
2183 
2184  inline tactic repeat(tactic const & t, unsigned max=UINT_MAX) {
2185  Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
2186  t.check_error();
2187  return tactic(t.ctx(), r);
2188  }
2189 
2190  inline tactic with(tactic const & t, params const & p) {
2191  Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
2192  t.check_error();
2193  return tactic(t.ctx(), r);
2194  }
2195  inline tactic try_for(tactic const & t, unsigned ms) {
2196  Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
2197  t.check_error();
2198  return tactic(t.ctx(), r);
2199  }
2200  inline tactic par_or(unsigned n, tactic const* tactics) {
2201  if (n == 0) {
2202  Z3_THROW(exception("a non-zero number of tactics need to be passed to par_or"));
2203  }
2204  array<Z3_tactic> buffer(n);
2205  for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
2206  return tactic(tactics[0].ctx(), Z3_tactic_par_or(tactics[0].ctx(), n, buffer.ptr()));
2207  }
2208 
2209  inline tactic par_and_then(tactic const & t1, tactic const & t2) {
2210  check_context(t1, t2);
2211  Z3_tactic r = Z3_tactic_par_and_then(t1.ctx(), t1, t2);
2212  t1.check_error();
2213  return tactic(t1.ctx(), r);
2214  }
2215 
2216  class probe : public object {
2217  Z3_probe m_probe;
2218  void init(Z3_probe s) {
2219  m_probe = s;
2220  Z3_probe_inc_ref(ctx(), s);
2221  }
2222  public:
2223  probe(context & c, char const * name):object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); }
2224  probe(context & c, double val):object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); }
2225  probe(context & c, Z3_probe s):object(c) { init(s); }
2226  probe(probe const & s):object(s) { init(s.m_probe); }
2227  ~probe() { Z3_probe_dec_ref(ctx(), m_probe); }
2228  operator Z3_probe() const { return m_probe; }
2229  probe & operator=(probe const & s) {
2230  Z3_probe_inc_ref(s.ctx(), s.m_probe);
2231  Z3_probe_dec_ref(ctx(), m_probe);
2232  m_ctx = s.m_ctx;
2233  m_probe = s.m_probe;
2234  return *this;
2235  }
2236  double apply(goal const & g) const { double r = Z3_probe_apply(ctx(), m_probe, g); check_error(); return r; }
2237  double operator()(goal const & g) const { return apply(g); }
2238  friend probe operator<=(probe const & p1, probe const & p2);
2239  friend probe operator<=(probe const & p1, double p2);
2240  friend probe operator<=(double p1, probe const & p2);
2241  friend probe operator>=(probe const & p1, probe const & p2);
2242  friend probe operator>=(probe const & p1, double p2);
2243  friend probe operator>=(double p1, probe const & p2);
2244  friend probe operator<(probe const & p1, probe const & p2);
2245  friend probe operator<(probe const & p1, double p2);
2246  friend probe operator<(double p1, probe const & p2);
2247  friend probe operator>(probe const & p1, probe const & p2);
2248  friend probe operator>(probe const & p1, double p2);
2249  friend probe operator>(double p1, probe const & p2);
2250  friend probe operator==(probe const & p1, probe const & p2);
2251  friend probe operator==(probe const & p1, double p2);
2252  friend probe operator==(double p1, probe const & p2);
2253  friend probe operator&&(probe const & p1, probe const & p2);
2254  friend probe operator||(probe const & p1, probe const & p2);
2255  friend probe operator!(probe const & p);
2256  };
2257 
2258  inline probe operator<=(probe const & p1, probe const & p2) {
2259  check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2260  }
2261  inline probe operator<=(probe const & p1, double p2) { return p1 <= probe(p1.ctx(), p2); }
2262  inline probe operator<=(double p1, probe const & p2) { return probe(p2.ctx(), p1) <= p2; }
2263  inline probe operator>=(probe const & p1, probe const & p2) {
2264  check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2265  }
2266  inline probe operator>=(probe const & p1, double p2) { return p1 >= probe(p1.ctx(), p2); }
2267  inline probe operator>=(double p1, probe const & p2) { return probe(p2.ctx(), p1) >= p2; }
2268  inline probe operator<(probe const & p1, probe const & p2) {
2269  check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2270  }
2271  inline probe operator<(probe const & p1, double p2) { return p1 < probe(p1.ctx(), p2); }
2272  inline probe operator<(double p1, probe const & p2) { return probe(p2.ctx(), p1) < p2; }
2273  inline probe operator>(probe const & p1, probe const & p2) {
2274  check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2275  }
2276  inline probe operator>(probe const & p1, double p2) { return p1 > probe(p1.ctx(), p2); }
2277  inline probe operator>(double p1, probe const & p2) { return probe(p2.ctx(), p1) > p2; }
2278  inline probe operator==(probe const & p1, probe const & p2) {
2279  check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2280  }
2281  inline probe operator==(probe const & p1, double p2) { return p1 == probe(p1.ctx(), p2); }
2282  inline probe operator==(double p1, probe const & p2) { return probe(p2.ctx(), p1) == p2; }
2283  inline probe operator&&(probe const & p1, probe const & p2) {
2284  check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2285  }
2286  inline probe operator||(probe const & p1, probe const & p2) {
2287  check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2288  }
2289  inline probe operator!(probe const & p) {
2290  Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
2291  }
2292 
2293  class optimize : public object {
2294  Z3_optimize m_opt;
2295 
2296  public:
2297  class handle {
2298  unsigned m_h;
2299  public:
2300  handle(unsigned h): m_h(h) {}
2301  unsigned h() const { return m_h; }
2302  };
2303  optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }
2305  Z3_optimize_inc_ref(o.ctx(), o.m_opt);
2306  m_opt = o.m_opt;
2307  }
2309  Z3_optimize_inc_ref(o.ctx(), o.m_opt);
2310  Z3_optimize_dec_ref(ctx(), m_opt);
2311  m_opt = o.m_opt;
2312  m_ctx = o.m_ctx;
2313  return *this;
2314  }
2315  ~optimize() { Z3_optimize_dec_ref(ctx(), m_opt); }
2316  operator Z3_optimize() const { return m_opt; }
2317  void add(expr const& e) {
2318  assert(e.is_bool());
2319  Z3_optimize_assert(ctx(), m_opt, e);
2320  }
2321  handle add(expr const& e, unsigned weight) {
2322  assert(e.is_bool());
2323  std::stringstream strm;
2324  strm << weight;
2325  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, strm.str().c_str(), 0));
2326  }
2327  handle add(expr const& e, char const* weight) {
2328  assert(e.is_bool());
2329  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0));
2330  }
2331  handle maximize(expr const& e) {
2332  return handle(Z3_optimize_maximize(ctx(), m_opt, e));
2333  }
2334  handle minimize(expr const& e) {
2335  return handle(Z3_optimize_minimize(ctx(), m_opt, e));
2336  }
2337  void push() {
2338  Z3_optimize_push(ctx(), m_opt);
2339  }
2340  void pop() {
2341  Z3_optimize_pop(ctx(), m_opt);
2342  }
2343  check_result check() { Z3_lbool r = Z3_optimize_check(ctx(), m_opt); check_error(); return to_check_result(r); }
2344  model get_model() const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }
2345  void set(params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }
2346  expr lower(handle const& h) {
2347  Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());
2348  check_error();
2349  return expr(ctx(), r);
2350  }
2351  expr upper(handle const& h) {
2352  Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h());
2353  check_error();
2354  return expr(ctx(), r);
2355  }
2356  expr_vector assertions() const { Z3_ast_vector r = Z3_optimize_get_assertions(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
2357  expr_vector objectives() const { Z3_ast_vector r = Z3_optimize_get_objectives(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
2358  stats statistics() const { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); }
2359  friend std::ostream & operator<<(std::ostream & out, optimize const & s);
2360  void from_file(char const* filename) { Z3_optimize_from_file(ctx(), m_opt, filename); check_error(); }
2361  void from_string(char const* constraints) { Z3_optimize_from_string(ctx(), m_opt, constraints); check_error(); }
2362  std::string help() const { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error(); return r; }
2363  };
2364  inline std::ostream & operator<<(std::ostream & out, optimize const & s) { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }
2365 
2366  class fixedpoint : public object {
2367  Z3_fixedpoint m_fp;
2368  public:
2371  operator Z3_fixedpoint() const { return m_fp; }
2372  void from_string(char const* s) { Z3_fixedpoint_from_string(ctx(), m_fp, s); check_error(); }
2373  void from_file(char const* s) { Z3_fixedpoint_from_file(ctx(), m_fp, s); check_error(); }
2374  void add_rule(expr& rule, symbol const& name) { Z3_fixedpoint_add_rule(ctx(), m_fp, rule, name); check_error(); }
2375  void add_fact(func_decl& f, unsigned * args) { Z3_fixedpoint_add_fact(ctx(), m_fp, f, f.arity(), args); check_error(); }
2376  check_result query(expr& q) { Z3_lbool r = Z3_fixedpoint_query(ctx(), m_fp, q); check_error(); return to_check_result(r); }
2377  check_result query(func_decl_vector& relations) {
2378  array<Z3_func_decl> rs(relations);
2379  Z3_lbool r = Z3_fixedpoint_query_relations(ctx(), m_fp, rs.size(), rs.ptr());
2380  check_error();
2381  return to_check_result(r);
2382  }
2383  expr get_answer() { Z3_ast r = Z3_fixedpoint_get_answer(ctx(), m_fp); check_error(); return expr(ctx(), r); }
2384  std::string reason_unknown() { return Z3_fixedpoint_get_reason_unknown(ctx(), m_fp); }
2385  void update_rule(expr& rule, symbol const& name) { Z3_fixedpoint_update_rule(ctx(), m_fp, rule, name); check_error(); }
2386  unsigned get_num_levels(func_decl& p) { unsigned r = Z3_fixedpoint_get_num_levels(ctx(), m_fp, p); check_error(); return r; }
2387  expr get_cover_delta(int level, func_decl& p) {
2388  Z3_ast r = Z3_fixedpoint_get_cover_delta(ctx(), m_fp, level, p);
2389  check_error();
2390  return expr(ctx(), r);
2391  }
2392  void add_cover(int level, func_decl& p, expr& property) { Z3_fixedpoint_add_cover(ctx(), m_fp, level, p, property); check_error(); }
2393  stats statistics() const { Z3_stats r = Z3_fixedpoint_get_statistics(ctx(), m_fp); check_error(); return stats(ctx(), r); }
2395  expr_vector assertions() const { Z3_ast_vector r = Z3_fixedpoint_get_assertions(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
2396  expr_vector rules() const { Z3_ast_vector r = Z3_fixedpoint_get_rules(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
2397  void set(params const & p) { Z3_fixedpoint_set_params(ctx(), m_fp, p); check_error(); }
2398  std::string help() const { return Z3_fixedpoint_get_help(ctx(), m_fp); }
2400  std::string to_string() { return Z3_fixedpoint_to_string(ctx(), m_fp, 0, 0); }
2401  std::string to_string(expr_vector const& queries) {
2402  array<Z3_ast> qs(queries);
2403  return Z3_fixedpoint_to_string(ctx(), m_fp, qs.size(), qs.ptr());
2404  }
2405  void push() { Z3_fixedpoint_push(ctx(), m_fp); check_error(); }
2406  void pop() { Z3_fixedpoint_pop(ctx(), m_fp); check_error(); }
2407  };
2408  inline std::ostream & operator<<(std::ostream & out, fixedpoint const & f) { return out << Z3_fixedpoint_to_string(f.ctx(), f, 0, 0); }
2409 
2410  inline tactic fail_if(probe const & p) {
2411  Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
2412  p.check_error();
2413  return tactic(p.ctx(), r);
2414  }
2415  inline tactic when(probe const & p, tactic const & t) {
2416  check_context(p, t);
2417  Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
2418  t.check_error();
2419  return tactic(t.ctx(), r);
2420  }
2421  inline tactic cond(probe const & p, tactic const & t1, tactic const & t2) {
2422  check_context(p, t1); check_context(p, t2);
2423  Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
2424  t1.check_error();
2425  return tactic(t1.ctx(), r);
2426  }
2427 
2428  inline symbol context::str_symbol(char const * s) { Z3_symbol r = Z3_mk_string_symbol(m_ctx, s); check_error(); return symbol(*this, r); }
2429  inline symbol context::int_symbol(int n) { Z3_symbol r = Z3_mk_int_symbol(m_ctx, n); check_error(); return symbol(*this, r); }
2430 
2431  inline sort context::bool_sort() { Z3_sort s = Z3_mk_bool_sort(m_ctx); check_error(); return sort(*this, s); }
2432  inline sort context::int_sort() { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }
2433  inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
2434  inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
2435  inline sort context::string_sort() { Z3_sort s = Z3_mk_string_sort(m_ctx); check_error(); return sort(*this, s); }
2436  inline sort context::seq_sort(sort& s) { Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); }
2437  inline sort context::re_sort(sort& s) { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
2438 
2439  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); }
2440  inline sort context::array_sort(sort_vector const& d, sort r) {
2441  array<Z3_sort> dom(d);
2442  Z3_sort s = Z3_mk_array_sort_n(m_ctx, dom.size(), dom.ptr(), r); check_error(); return sort(*this, s);
2443  }
2444 
2445  inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
2446  array<Z3_symbol> _enum_names(n);
2447  for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
2448  array<Z3_func_decl> _cs(n);
2449  array<Z3_func_decl> _ts(n);
2450  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2451  sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
2452  check_error();
2453  for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
2454  return s;
2455  }
2456  inline func_decl context::tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs) {
2457  array<Z3_symbol> _names(n);
2458  array<Z3_sort> _sorts(n);
2459  for (unsigned i = 0; i < n; i++) { _names[i] = Z3_mk_string_symbol(*this, names[i]); _sorts[i] = sorts[i]; }
2460  array<Z3_func_decl> _projs(n);
2461  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2462  Z3_func_decl tuple;
2463  sort _ignore_s = to_sort(*this, Z3_mk_tuple_sort(*this, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));
2464  check_error();
2465  for (unsigned i = 0; i < n; i++) { projs.push_back(func_decl(*this, _projs[i])); }
2466  return func_decl(*this, tuple);
2467  }
2468 
2469  inline sort context::uninterpreted_sort(char const* name) {
2470  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2471  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
2472  }
2474  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
2475  }
2476 
2477  inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
2478  array<Z3_sort> args(arity);
2479  for (unsigned i = 0; i < arity; i++) {
2480  check_context(domain[i], range);
2481  args[i] = domain[i];
2482  }
2483  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
2484  check_error();
2485  return func_decl(*this, f);
2486  }
2487 
2488  inline func_decl context::function(char const * name, unsigned arity, sort const * domain, sort const & range) {
2489  return function(range.ctx().str_symbol(name), arity, domain, range);
2490  }
2491 
2492  inline func_decl context::function(symbol const& name, sort_vector const& domain, sort const& range) {
2493  array<Z3_sort> args(domain.size());
2494  for (unsigned i = 0; i < domain.size(); i++) {
2495  check_context(domain[i], range);
2496  args[i] = domain[i];
2497  }
2498  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
2499  check_error();
2500  return func_decl(*this, f);
2501  }
2502 
2503  inline func_decl context::function(char const * name, sort_vector const& domain, sort const& range) {
2504  return function(range.ctx().str_symbol(name), domain, range);
2505  }
2506 
2507 
2508  inline func_decl context::function(char const * name, sort const & domain, sort const & range) {
2509  check_context(domain, range);
2510  Z3_sort args[1] = { domain };
2511  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
2512  check_error();
2513  return func_decl(*this, f);
2514  }
2515 
2516  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & range) {
2517  check_context(d1, range); check_context(d2, range);
2518  Z3_sort args[2] = { d1, d2 };
2519  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
2520  check_error();
2521  return func_decl(*this, f);
2522  }
2523 
2524  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
2525  check_context(d1, range); check_context(d2, range); check_context(d3, range);
2526  Z3_sort args[3] = { d1, d2, d3 };
2527  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
2528  check_error();
2529  return func_decl(*this, f);
2530  }
2531 
2532  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
2533  check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range);
2534  Z3_sort args[4] = { d1, d2, d3, d4 };
2535  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
2536  check_error();
2537  return func_decl(*this, f);
2538  }
2539 
2540  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) {
2541  check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range); check_context(d5, range);
2542  Z3_sort args[5] = { d1, d2, d3, d4, d5 };
2543  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
2544  check_error();
2545  return func_decl(*this, f);
2546  }
2547 
2548  inline expr context::constant(symbol const & name, sort const & s) {
2549  Z3_ast r = Z3_mk_const(m_ctx, name, s);
2550  check_error();
2551  return expr(*this, r);
2552  }
2553  inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); }
2554  inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); }
2555  inline expr context::int_const(char const * name) { return constant(name, int_sort()); }
2556  inline expr context::real_const(char const * name) { return constant(name, real_sort()); }
2557  inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); }
2558 
2559  inline expr context::bool_val(bool b) { return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }
2560 
2561  inline expr context::int_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
2562  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); }
2563  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); }
2564  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); }
2565  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); }
2566 
2567  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); }
2568  inline expr context::real_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
2569  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); }
2570  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); }
2571  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); }
2572  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); }
2573 
2574  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); }
2575  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); }
2576  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); }
2577  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); }
2578  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); }
2579  inline expr context::bv_val(unsigned n, bool const* bits) {
2580  array<Z3_bool> _bits(n);
2581  for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
2582  Z3_ast r = Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error(); return expr(*this, r);
2583  }
2584 
2585  inline expr context::string_val(char const* s) { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
2586  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); }
2587 
2588  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); }
2589 
2590  inline expr func_decl::operator()(unsigned n, expr const * args) const {
2591  array<Z3_ast> _args(n);
2592  for (unsigned i = 0; i < n; i++) {
2593  check_context(*this, args[i]);
2594  _args[i] = args[i];
2595  }
2596  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
2597  check_error();
2598  return expr(ctx(), r);
2599 
2600  }
2601  inline expr func_decl::operator()(expr_vector const& args) const {
2602  array<Z3_ast> _args(args.size());
2603  for (unsigned i = 0; i < args.size(); i++) {
2604  check_context(*this, args[i]);
2605  _args[i] = args[i];
2606  }
2607  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
2608  check_error();
2609  return expr(ctx(), r);
2610  }
2611  inline expr func_decl::operator()() const {
2612  Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
2613  ctx().check_error();
2614  return expr(ctx(), r);
2615  }
2616  inline expr func_decl::operator()(expr const & a) const {
2617  check_context(*this, a);
2618  Z3_ast args[1] = { a };
2619  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
2620  ctx().check_error();
2621  return expr(ctx(), r);
2622  }
2623  inline expr func_decl::operator()(int a) const {
2624  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
2625  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
2626  ctx().check_error();
2627  return expr(ctx(), r);
2628  }
2629  inline expr func_decl::operator()(expr const & a1, expr const & a2) const {
2630  check_context(*this, a1); check_context(*this, a2);
2631  Z3_ast args[2] = { a1, a2 };
2632  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
2633  ctx().check_error();
2634  return expr(ctx(), r);
2635  }
2636  inline expr func_decl::operator()(expr const & a1, int a2) const {
2637  check_context(*this, a1);
2638  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
2639  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
2640  ctx().check_error();
2641  return expr(ctx(), r);
2642  }
2643  inline expr func_decl::operator()(int a1, expr const & a2) const {
2644  check_context(*this, a2);
2645  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
2646  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
2647  ctx().check_error();
2648  return expr(ctx(), r);
2649  }
2650  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3) const {
2651  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
2652  Z3_ast args[3] = { a1, a2, a3 };
2653  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
2654  ctx().check_error();
2655  return expr(ctx(), r);
2656  }
2657  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const {
2658  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
2659  Z3_ast args[4] = { a1, a2, a3, a4 };
2660  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
2661  ctx().check_error();
2662  return expr(ctx(), r);
2663  }
2664  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const {
2665  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
2666  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
2667  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
2668  ctx().check_error();
2669  return expr(ctx(), r);
2670  }
2671 
2672  inline expr to_real(expr const & a) { Z3_ast r = Z3_mk_int2real(a.ctx(), a); a.check_error(); return expr(a.ctx(), r); }
2673 
2674  inline func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
2675  return range.ctx().function(name, arity, domain, range);
2676  }
2677  inline func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range) {
2678  return range.ctx().function(name, arity, domain, range);
2679  }
2680  inline func_decl function(char const * name, sort const & domain, sort const & range) {
2681  return range.ctx().function(name, domain, range);
2682  }
2683  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range) {
2684  return range.ctx().function(name, d1, d2, range);
2685  }
2686  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
2687  return range.ctx().function(name, d1, d2, d3, range);
2688  }
2689  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
2690  return range.ctx().function(name, d1, d2, d3, d4, range);
2691  }
2692  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) {
2693  return range.ctx().function(name, d1, d2, d3, d4, d5, range);
2694  }
2695  inline func_decl function(char const* name, sort_vector const& domain, sort const& range) {
2696  return range.ctx().function(name, domain, range);
2697  }
2698  inline func_decl function(std::string const& name, sort_vector const& domain, sort const& range) {
2699  return range.ctx().function(name.c_str(), domain, range);
2700  }
2701 
2702  inline expr select(expr const & a, expr const & i) {
2703  check_context(a, i);
2704  Z3_ast r = Z3_mk_select(a.ctx(), a, i);
2705  a.check_error();
2706  return expr(a.ctx(), r);
2707  }
2708  inline expr select(expr const & a, int i) { return select(a, a.ctx().num_val(i, a.get_sort().array_domain())); }
2709  inline expr store(expr const & a, expr const & i, expr const & v) {
2710  check_context(a, i); check_context(a, v);
2711  Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
2712  a.check_error();
2713  return expr(a.ctx(), r);
2714  }
2715  inline expr select(expr const & a, expr_vector const & i) {
2716  check_context(a, i);
2717  array<Z3_ast> idxs(i);
2718  Z3_ast r = Z3_mk_select_n(a.ctx(), a, idxs.size(), idxs.ptr());
2719  a.check_error();
2720  return expr(a.ctx(), r);
2721  }
2722 
2723  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); }
2724  inline expr store(expr const & a, expr i, int v) { return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
2725  inline expr store(expr const & a, int i, int v) {
2726  return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
2727  }
2728  inline expr store(expr const & a, expr_vector const & i, expr const & v) {
2729  check_context(a, i); check_context(a, v);
2730  array<Z3_ast> idxs(i);
2731  Z3_ast r = Z3_mk_store_n(a.ctx(), a, idxs.size(), idxs.ptr(), v);
2732  a.check_error();
2733  return expr(a.ctx(), r);
2734  }
2735 
2736  inline expr as_array(func_decl & f) {
2737  Z3_ast r = Z3_mk_as_array(f.ctx(), f);
2738  f.check_error();
2739  return expr(f.ctx(), r);
2740  }
2741 
2742 #define MK_EXPR1(_fn, _arg) \
2743  Z3_ast r = _fn(_arg.ctx(), _arg); \
2744  _arg.check_error(); \
2745  return expr(_arg.ctx(), r);
2746 
2747 #define MK_EXPR2(_fn, _arg1, _arg2) \
2748  check_context(_arg1, _arg2); \
2749  Z3_ast r = _fn(_arg1.ctx(), _arg1, _arg2); \
2750  _arg1.check_error(); \
2751  return expr(_arg1.ctx(), r);
2752 
2753  inline expr const_array(sort const & d, expr const & v) {
2754  MK_EXPR2(Z3_mk_const_array, d, v);
2755  }
2756 
2757  inline expr empty_set(sort const& s) {
2759  }
2760 
2761  inline expr full_set(sort const& s) {
2763  }
2764 
2765  inline expr set_add(expr const& s, expr const& e) {
2766  MK_EXPR2(Z3_mk_set_add, s, e);
2767  }
2768 
2769  inline expr set_del(expr const& s, expr const& e) {
2770  MK_EXPR2(Z3_mk_set_del, s, e);
2771  }
2772 
2773  inline expr set_union(expr const& a, expr const& b) {
2774  check_context(a, b);
2775  Z3_ast es[2] = { a, b };
2776  Z3_ast r = Z3_mk_set_union(a.ctx(), 2, es);
2777  a.check_error();
2778  return expr(a.ctx(), r);
2779  }
2780 
2781  inline expr set_intersect(expr const& a, expr const& b) {
2782  check_context(a, b);
2783  Z3_ast es[2] = { a, b };
2784  Z3_ast r = Z3_mk_set_intersect(a.ctx(), 2, es);
2785  a.check_error();
2786  return expr(a.ctx(), r);
2787  }
2788 
2789  inline expr set_difference(expr const& a, expr const& b) {
2791  }
2792 
2793  inline expr set_complement(expr const& a) {
2795  }
2796 
2797  inline expr set_member(expr const& s, expr const& e) {
2798  MK_EXPR2(Z3_mk_set_member, s, e);
2799  }
2800 
2801  inline expr set_subset(expr const& a, expr const& b) {
2802  MK_EXPR2(Z3_mk_set_subset, a, b);
2803  }
2804 
2805  // sequence and regular expression operations.
2806  // union is +
2807  // concat is overloaded to handle sequences and regular expressions
2808 
2809  inline expr empty(sort const& s) {
2810  Z3_ast r = Z3_mk_seq_empty(s.ctx(), s);
2811  s.check_error();
2812  return expr(s.ctx(), r);
2813  }
2814  inline expr suffixof(expr const& a, expr const& b) {
2815  check_context(a, b);
2816  Z3_ast r = Z3_mk_seq_suffix(a.ctx(), a, b);
2817  a.check_error();
2818  return expr(a.ctx(), r);
2819  }
2820  inline expr prefixof(expr const& a, expr const& b) {
2821  check_context(a, b);
2822  Z3_ast r = Z3_mk_seq_prefix(a.ctx(), a, b);
2823  a.check_error();
2824  return expr(a.ctx(), r);
2825  }
2826  inline expr indexof(expr const& s, expr const& substr, expr const& offset) {
2827  check_context(s, substr); check_context(s, offset);
2828  Z3_ast r = Z3_mk_seq_index(s.ctx(), s, substr, offset);
2829  s.check_error();
2830  return expr(s.ctx(), r);
2831  }
2832  inline expr to_re(expr const& s) {
2834  }
2835  inline expr in_re(expr const& s, expr const& re) {
2836  MK_EXPR2(Z3_mk_seq_in_re, s, re);
2837  }
2838  inline expr plus(expr const& re) {
2839  MK_EXPR1(Z3_mk_re_plus, re);
2840  }
2841  inline expr option(expr const& re) {
2843  }
2844  inline expr star(expr const& re) {
2845  MK_EXPR1(Z3_mk_re_star, re);
2846  }
2847  inline expr re_empty(sort const& s) {
2848  Z3_ast r = Z3_mk_re_empty(s.ctx(), s);
2849  s.check_error();
2850  return expr(s.ctx(), r);
2851  }
2852  inline expr re_full(sort const& s) {
2853  Z3_ast r = Z3_mk_re_full(s.ctx(), s);
2854  s.check_error();
2855  return expr(s.ctx(), r);
2856  }
2857  inline expr re_intersect(expr_vector const& args) {
2858  assert(args.size() > 0);
2859  context& ctx = args[0].ctx();
2860  array<Z3_ast> _args(args);
2861  Z3_ast r = Z3_mk_re_intersect(ctx, _args.size(), _args.ptr());
2862  ctx.check_error();
2863  return expr(ctx, r);
2864  }
2865  inline expr re_complement(expr const& a) {
2867  }
2868  inline expr range(expr const& lo, expr const& hi) {
2869  check_context(lo, hi);
2870  Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
2871  lo.check_error();
2872  return expr(lo.ctx(), r);
2873  }
2874 
2875 
2876 
2877 
2878 
2879  inline expr interpolant(expr const& a) {
2880  return expr(a.ctx(), Z3_mk_interpolant(a.ctx(), a));
2881  }
2882 
2883  inline expr context::parse_string(char const* s) {
2884  Z3_ast r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0);
2885  check_parser_error();
2886  return expr(*this, r);
2887  }
2888  inline expr context::parse_file(char const* s) {
2889  Z3_ast r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0);
2890  check_parser_error();
2891  return expr(*this, r);
2892  }
2893 
2894  inline expr context::parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls) {
2895  array<Z3_symbol> sort_names(sorts.size());
2896  array<Z3_symbol> decl_names(decls.size());
2897  array<Z3_sort> sorts1(sorts);
2898  array<Z3_func_decl> decls1(decls);
2899  for (unsigned i = 0; i < sorts.size(); ++i) {
2900  sort_names[i] = sorts[i].name();
2901  }
2902  for (unsigned i = 0; i < decls.size(); ++i) {
2903  decl_names[i] = decls[i].name();
2904  }
2905  Z3_ast r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
2906  check_parser_error();
2907  return expr(*this, r);
2908  }
2909 
2910  inline expr context::parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls) {
2911  array<Z3_symbol> sort_names(sorts.size());
2912  array<Z3_symbol> decl_names(decls.size());
2913  array<Z3_sort> sorts1(sorts);
2914  array<Z3_func_decl> decls1(decls);
2915  for (unsigned i = 0; i < sorts.size(); ++i) {
2916  sort_names[i] = sorts[i].name();
2917  }
2918  for (unsigned i = 0; i < decls.size(); ++i) {
2919  decl_names[i] = decls[i].name();
2920  }
2921  Z3_ast r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
2922  check_parser_error();
2923  return expr(*this, r);
2924  }
2925 
2926 
2927  inline check_result context::compute_interpolant(expr const& pat, params const& p, expr_vector& i, model& m) {
2928  Z3_ast_vector interp = 0;
2929  Z3_model mdl = 0;
2930  Z3_lbool r = Z3_compute_interpolant(*this, pat, p, &interp, &mdl);
2931  switch (r) {
2932  case Z3_L_FALSE:
2933  i = expr_vector(*this, interp);
2934  break;
2935  case Z3_L_TRUE:
2936  m = model(*this, mdl);
2937  break;
2938  case Z3_L_UNDEF:
2939  break;
2940  }
2941  return to_check_result(r);
2942  }
2943 
2944  inline expr_vector context::get_interpolant(expr const& proof, expr const& pat, params const& p) {
2945  return expr_vector(*this, Z3_get_interpolant(*this, proof, pat, p));
2946  }
2947 
2948  inline expr expr::substitute(expr_vector const& src, expr_vector const& dst) {
2949  assert(src.size() == dst.size());
2950  array<Z3_ast> _src(src.size());
2951  array<Z3_ast> _dst(dst.size());
2952  for (unsigned i = 0; i < src.size(); ++i) {
2953  _src[i] = src[i];
2954  _dst[i] = dst[i];
2955  }
2956  Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
2957  check_error();
2958  return expr(ctx(), r);
2959  }
2960 
2961  inline expr expr::substitute(expr_vector const& dst) {
2962  array<Z3_ast> _dst(dst.size());
2963  for (unsigned i = 0; i < dst.size(); ++i) {
2964  _dst[i] = dst[i];
2965  }
2966  Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
2967  check_error();
2968  return expr(ctx(), r);
2969  }
2970 
2971 
2972 
2973 }
2974 
2977 #undef Z3_THROW
2978 #endif
2979 
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.
ast_vector_tpl(context &c)
Definition: z3++.h:1529
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:1693
bool is_uint(unsigned i) const
Definition: z3++.h:1915
expr mod(expr const &a, expr const &b)
Definition: z3++.h:1103
Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
stats statistics() const
Definition: z3++.h:2358
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_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...
void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s)
Increment the reference counter of the given statistics object.
Z3_ast Z3_API Z3_mk_true(Z3_context c)
Create an AST node representing true.
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)
Create a new fixedpoint context.
Z3_probe Z3_API Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the va...
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:146
expr parse_string(char const *s)
parsing
Definition: z3++.h:2883
Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)
Create a bit-vector type of the given size.
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:2431
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.
Z3_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...
expr get_const_interp(func_decl c) const
Definition: z3++.h:1859
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:1885
expr mk_and(expr_vector const &args)
Definition: z3++.h:1752
bool is_decided_unsat() const
Definition: z3++.h:2069
Z3_bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g)
Return true if the given goal contains the formula false.
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: ...
model(context &c)
Definition: z3++.h:1822
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:1574
tactic & operator=(tactic const &s)
Definition: z3++.h:2142
bool is_bool() const
Return true if this sort is the Boolean sort.
Definition: z3++.h:503
sort re_sort(sort &seq_sort)
Return a regular expression sort over sequences seq_sort.
Definition: z3++.h:2437
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
bool is_datatype() const
Return true if this is a Datatype expression.
Definition: z3++.h:642
void add_fact(func_decl &f, unsigned *args)
Definition: z3++.h:2375
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:2225
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:816
expr pbeq(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:1660
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.
unsigned uint_value(unsigned i) const
Definition: z3++.h:1917
probe & operator=(probe const &s)
Definition: z3++.h:2229
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:1803
Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err)
Return a string describing the given error code.
Z3_ast Z3_API Z3_mk_interpolant(Z3_context c, Z3_ast a)
Create an AST node marking a formula position for interpolation.
unsigned get_num_levels(func_decl &p)
Definition: z3++.h:2386
double double_value(unsigned i) const
Definition: z3++.h:1918
std::string documentation(symbol const &s)
Definition: z3++.h:419
stats statistics() const
Definition: z3++.h:2008
Z3_error_code check_error() const
Definition: z3++.h:374
Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
std::string help() const
Definition: z3++.h:2362
void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t)
Increment the reference counter of the given tactic.
#define Z3_THROW(x)
Definition: z3++.h:93
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:2344
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2428
unsigned size() const
Definition: z3++.h:2061
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:1483
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.
Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index)
Retrieve from s the unit sequence positioned at position index.
Z3_params Z3_API Z3_mk_params(Z3_context c)
Create a Z3 (empty) parameter set. Starting at Z3 4.0, parameter sets are used to configure many comp...
expr operator[](int i) const
Definition: z3++.h:2062
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...
Z3_symbol_kind Z3_API Z3_get_symbol_kind(Z3_context c, Z3_symbol s)
Return Z3_INT_SYMBOL if the symbol was constructed using Z3_mk_int_symbol, and Z3_STRING_SYMBOL if th...
void Z3_API Z3_ast_vector_inc_ref(Z3_context c, Z3_ast_vector v)
Increment the reference counter of the given AST vector.
void push()
Definition: z3++.h:1962
expr contains(expr const &s)
Definition: z3++.h:1019
func_decl get_const_decl(unsigned i) const
Definition: z3++.h:1848
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:2421
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:1004
solver(context &c, simple)
Definition: z3++.h:1942
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:605
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:2868
expr bv_val(int n, unsigned sz)
Definition: z3++.h:2574
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed greater than.
Z3_model Z3_API Z3_apply_result_convert_model(Z3_context c, Z3_apply_result r, unsigned i, Z3_model m)
Convert a model for the subgoal Z3_apply_result_get_subgoal(c, r, i) into a model for the original go...
expr operator!=(expr const &a, expr const &b)
Definition: z3++.h:1159
Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o)
Check consistency and produce optimal values.
Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2)
Logical shift right.
Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i)
Return the declaration of the i-th function in the given model.
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
Z3_ast_vector Z3_API Z3_fixedpoint_from_string(Z3_context c, Z3_fixedpoint f, Z3_string s)
Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context...
Definition: z3_api.h:1321
func_interp & operator=(func_interp const &s)
Definition: z3++.h:1794
iterator & operator++()
Definition: z3++.h:1570
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:1849
probe(context &c, double val)
Definition: z3++.h:2224
expr select(expr const &a, expr const &i)
Definition: z3++.h:2702
Definition: z3++.h:127
expr operator &(expr const &a, expr const &b)
Definition: z3++.h:1349
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:1771
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.
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...
tactic when(probe const &p, tactic const &t)
Definition: z3++.h:2415
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:1808
config()
Definition: z3++.h:105
bool is_algebraic() const
Return true if expression is an algebraic number.
Definition: z3++.h:697
unsigned get_numeral_uint() const
Return uint value of numeral, throw if result cannot fit in machine uint.
Definition: z3++.h:744
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:2346
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.
bool Z3_bool
Z3 Boolean type. It is just an alias for bool.
Definition: z3_api.h:77
array(unsigned sz)
Definition: z3++.h:356
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:995
A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort.
Definition: z3++.h:482
~solver()
Definition: z3++.h:1947
Z3_ast Z3_API Z3_substitute(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const from[], Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs. The result is the new AST. The arrays from and to must have size num_exprs. For every i smaller than num_exprs, we must have that sort of from[i] must be equal to sort of to[i].
sort array_domain() const
Return the domain of this Array sort.
Definition: z3++.h:557
char const * msg() const
Definition: z3++.h:84
T operator[](int i) const
Definition: z3++.h:1535
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:2304
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:572
void push()
Definition: z3++.h:2405
~array()
Definition: z3++.h:359
void pop_back()
Definition: z3++.h:1539
expr full_set(sort const &s)
Definition: z3++.h:2761
expr as_expr() const
Definition: z3++.h:2113
model(model &src, context &dst, translate)
Definition: z3++.h:1825
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:563
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.
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:362
Z3_goal Z3_API Z3_mk_goal(Z3_context c, Z3_bool models, Z3_bool unsat_cores, Z3_bool proofs)
Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or trans...
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.
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:2434
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.
void interrupt()
Interrupt the current procedure being executed by any object managed by this context. This is a soft interruption: there is no guarantee the object will actually stop.
Definition: z3++.h:218
expr lshr(expr const &a, expr const &b)
logic shift right operator for bitvectors
Definition: z3++.h:1469
expr as_expr() const
Definition: z3++.h:2070
expr udiv(expr const &a, expr const &b)
unsigned division operator for bitvectors.
Definition: z3++.h:1434
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
Z3_symbol Z3_API Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, unsigned i)
Return the number of parameters in the given parameter description set.
std::string help() const
Definition: z3++.h:2159
bool is_bv() const
Return true if this is a Bit-vector expression.
Definition: z3++.h:634
expr upper(handle const &h)
Definition: z3++.h:2351
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1356
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1319
goal(context &c, Z3_goal s)
Definition: z3++.h:2047
optimize & operator=(optimize const &o)
Definition: z3++.h:2308
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].
Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, Z3_bool const *bits)
create a bit-vector numeral from a vector of Booleans.
std::string to_string() const
Definition: z3++.h:420
expr_vector assertions() const
Definition: z3++.h:2356
Z3_ast 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.
model(context &c, Z3_model m)
Definition: z3++.h:1823
sort array_sort(sort d, sort r)
Return an array sort for arrays from d to r.
Definition: z3++.h:2439
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:2548
void pop()
Definition: z3++.h:2340
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:2237
bool is_real() const
Return true if this is a real expression.
Definition: z3++.h:626
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)
Return the number of parameters associated with a declaration.
check_result query(expr &q)
Definition: z3++.h:2376
Z3_bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
Compare terms.
#define _Z3_MK_UN_(a, mkun)
Definition: z3++.h:1113
fixedpoint(context &c)
Definition: z3++.h:2369
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:527
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:2139
void set_enable_exceptions(bool f)
The C++ API uses by defaults exceptions on errors. For applications that don&#39;t work well with excepti...
Definition: z3++.h:193
~probe()
Definition: z3++.h:2227
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:388
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:1851
expr rotate_right(unsigned i)
Definition: z3++.h:991
~tactic()
Definition: z3++.h:2140
bool is_array() const
Return true if this is a Array expression.
Definition: z3++.h:638
sort operator()(context &c, Z3_ast a)
Definition: z3++.h:1510
check_result check()
Definition: z3++.h:2343
Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[])
Create the intersection of the regular languages.
expr is_int(expr const &e)
Definition: z3++.h:1121
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.
Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s)
Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.
Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[])
Check whether the assertions in the given solver and optional assumptions are consistent or not...
expr operator^(expr const &a, expr const &b)
Definition: z3++.h:1353
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:710
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:2361
Exception used to sign API usage errors.
Definition: z3++.h:80
expr operator*(expr const &a, expr const &b)
Definition: z3++.h:1196
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.
Z3_ast 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.
expr itos() const
Definition: z3++.h:1041
Z3_context Z3_API Z3_mk_context_rc(Z3_config c)
Create a context using the given configuration. This function is similar to Z3_mk_context. However, in the context returned by this function, the user is responsible for managing Z3_ast reference counters. Managing reference counters is a burden and error-prone, but allows the user to use the memory more efficiently. The user must invoke Z3_inc_ref for any Z3_ast returned by Z3, and Z3_dec_ref whenever the Z3_ast is not needed anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD.
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.
ast_vector_tpl(context &c, Z3_ast_vector v)
Definition: z3++.h:1530
A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort ...
Definition: z3++.h:603
void reset_params()
Definition: z3++.h:75
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:507
expr operator!(expr const &a)
Definition: z3++.h:1119
bool operator==(iterator const &other)
Definition: z3++.h:1564
expr set_subset(expr const &a, expr const &b)
Definition: z3++.h:2801
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:2747
def is_app(a)
Definition: z3py.py:1069
expr & operator=(expr const &n)
Definition: z3++.h:608
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
bool enable_exceptions() const
Definition: z3++.h:195
expr ule(expr const &a, expr const &b)
unsigned less than or equal to operator for bitvectors.
Definition: z3++.h:1410
expr in_re(expr const &s, expr const &re)
Definition: z3++.h:2835
symbol name(unsigned i)
Definition: z3++.h:417
std::string key(unsigned i) const
Definition: z3++.h:1914
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:1070
Z3_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...
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_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.
static param_descrs simplify_param_descrs(context &c)
Definition: z3++.h:414
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:579
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:2385
expr parse_file(char const *file)
Definition: z3++.h:2888
func_decl operator()(context &c, Z3_ast a)
Definition: z3++.h:1518
std::string to_string(expr_vector const &queries)
Definition: z3++.h:2401
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:70
stats(context &c)
Definition: z3++.h:1901
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:1217
std::string reason_unknown()
Definition: z3++.h:2384
void add_entry(expr_vector const &args, expr &value)
Definition: z3++.h:1804
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:654
expr pw(expr const &a, expr const &b)
Definition: z3++.h:1099
bool empty() const
Definition: z3++.h:1540
Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)
Return the declaration of a constant or function application.
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:672
context(config &c, interpolation)
Definition: z3++.h:163
expr(context &c, Z3_ast n)
Definition: z3++.h:606
~goal()
Definition: z3++.h:2049
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:2789
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:2395
expr operator~(expr const &a)
Definition: z3++.h:1365
unsigned num_entries() const
Definition: z3++.h:1802
void Z3_API Z3_fixedpoint_pop(Z3_context c, Z3_fixedpoint d)
Backtrack one backtracking point.
def tactics(ctx=None)
Definition: z3py.py:7498
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.
check_result check(unsigned n, expr *const assumptions)
Definition: z3++.h:1980
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.
check_result check(expr_vector assumptions)
Definition: z3++.h:1990
expr rem(expr const &a, expr const &b)
Definition: z3++.h:1107
probe(context &c, char const *name)
Definition: z3++.h:2223
Z3_symbol_kind kind() const
Definition: z3++.h:386
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed less than.
expr get_answer()
Definition: z3++.h:2383
Z3_sort Z3_API Z3_mk_string_sort(Z3_context c)
Create a sort for 8 bit strings.
~stats()
Definition: z3++.h:1904
sort seq_sort(sort &s)
Return a sequence sort over base sort s.
Definition: z3++.h:2436
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
def substitute(t, m)
Definition: z3py.py:7825
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:1031
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&#39;th optimization objective.
A Context manages all other Z3 objects, global configuration options, etc.
Definition: z3++.h:140
Definition: z3++.h:450
Z3 C++ namespace.
Definition: z3++.h:45
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:801
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:580
expr set_add(expr const &s, expr const &e)
Definition: z3++.h:2765
expr ashr(expr const &a, expr const &b)
arithmetic shift right operator for bitvectors
Definition: z3++.h:1476
expr re_empty(sort const &s)
Definition: z3++.h:2847
unsigned size() const
Definition: z3++.h:1913
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&#39;s complement signed remainder (sign follows dividend).
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed division.
def is_array(a)
Definition: z3py.py:4144
expr nor(expr const &a, expr const &b)
Definition: z3++.h:1362
Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p)
Return a probe that evaluates to "true" when p does not evaluate to true.
Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c)
Return the parameter description set for the simplify procedure.
void Z3_API Z3_fixedpoint_push(Z3_context c, Z3_fixedpoint d)
Create a backtracking point.
solver(context &c, Z3_solver s)
Definition: z3++.h:1943
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:100
Z3_decl_kind decl_kind() const
Definition: z3++.h:582
bool is_re() const
Return true if this sort is a regular expression sort.
Definition: z3++.h:539
solver & operator=(solver const &s)
Definition: z3++.h:1949
expr operator &&(expr const &a, expr const &b)
Definition: z3++.h:1125
void add_cover(int level, func_decl &p, expr &property)
Definition: z3++.h:2392
Z3_bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
expr substitute(expr_vector const &src, expr_vector const &dst)
Apply substitution. Replace src expressions by dst.
Definition: z3++.h:2948
iterator begin() const
Definition: z3++.h:1578
ast(context &c, Z3_ast n)
Definition: z3++.h:455
ast_vector_tpl & operator=(ast_vector_tpl const &s)
Definition: z3++.h:1541
expr operator<=(expr const &a, expr const &b)
Definition: z3++.h:1289
handle add(expr const &e, char const *weight)
Definition: z3++.h:2327
Z3_goal_prec precision() const
Definition: z3++.h:2063
expr bv_const(char const *name, unsigned sz)
Definition: z3++.h:2557
context & ctx() const
Definition: z3++.h:373
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 &#39;else&#39; value of the given function interpretation.
Z3_sort_kind sort_kind() const
Return the internal sort kind.
Definition: z3++.h:495
expr string_val(char const *s)
Definition: z3++.h:2585
T back() const
Definition: z3++.h:1538
tactic(context &c, char const *name)
Definition: z3++.h:2137
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:2435
tactic with(tactic const &t, params const &p)
Definition: z3++.h:2190
expr empty_set(sort const &s)
Definition: z3++.h:2757
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.
expr as_array(func_decl &f)
Definition: z3++.h:2736
expr plus(expr const &re)
Definition: z3++.h:2838
Z3_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.
expr xnor(expr const &a, expr const &b)
Definition: z3++.h:1363
void reset()
Definition: z3++.h:1964
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:1579
Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)
Shift left.
~config()
Definition: z3++.h:106
bool is_arith() const
Return true if this sort is the Integer or Real sort.
Definition: z3++.h:515
void from_string(char const *s)
Definition: z3++.h:1977
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:531
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst)
Replace the first occurrence of src with dst in s.
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:176
unsigned Z3_API Z3_goal_depth(Z3_context c, Z3_goal g)
Return the depth of the given goal. It tracks how many transformations were applied to it...
void Z3_API Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r)
Increment the reference counter of the given Z3_apply_result object.
bool is_real() const
Return true if this sort is the Real sort.
Definition: z3++.h:511
void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e)
Increment the reference counter of the given Z3_func_entry object.
void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a)
Decrement the reference counter of the given AST. The context c should have been created using Z3_mk_...
iterator(iterator &other)
Definition: z3++.h:1561
func_entry(context &c, Z3_func_entry e)
Definition: z3++.h:1767
void resize(unsigned sz)
Definition: z3++.h:1537
void Z3_API Z3_del_config(Z3_config c)
Delete the given configuration object.
Z3_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...
expr body() const
Return the &#39;body&#39; of this quantifier.
Definition: z3++.h:838
expr operator()() const
Definition: z3++.h:2611
void add(expr const &e, char const *p)
Definition: z3++.h:1971
func_decl to_func_decl(context &c, Z3_func_decl f)
Definition: z3++.h:1402
unsigned hash() const
Definition: z3++.h:462
optimize(context &c)
Definition: z3++.h:2303
goal operator[](int i) const
Definition: z3++.h:2106
Z3_lbool Z3_API Z3_compute_interpolant(Z3_context c, Z3_ast pat, Z3_params p, Z3_ast_vector *interp, Z3_model *model)
param_descrs(param_descrs const &o)
Definition: z3++.h:405
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:681
expr(expr const &n)
Definition: z3++.h:607
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&#39;th optimization objective.
Definition: z3++.h:1760
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:1979
expr_vector objectives() const
Definition: z3++.h:2357
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:2014
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:1169
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2477
expr operator()(context &c, Z3_ast a)
Definition: z3++.h:1499
Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;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:2398
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.
bool is_arith() const
Return true if this is an integer or real expression.
Definition: z3++.h:630
bool is_well_sorted() const
Return true if this expression is well sorted (aka type correct).
Definition: z3++.h:702
bool is_numeral_u64(uint64_t &i) const
Definition: z3++.h:673
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.
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...
def is_real(a)
Definition: z3py.py:2370
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:387
expr re_complement(expr const &a)
Definition: z3++.h:2865
expr srem(expr const &a, expr const &b)
signed remainder operator for bitvectors
Definition: z3++.h:1441
Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed less than or equal to.
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.
expr set_intersect(expr const &a, expr const &b)
Definition: z3++.h:2781
void from_string(char const *s)
Definition: z3++.h:2372
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:2064
exception(char const *msg)
Definition: z3++.h:83
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:1946
Z3_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const *domain, Z3_sort range)
Create an array type with N arguments.
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:98
Z3_ast_vector Z3_API Z3_fixedpoint_from_file(Z3_context c, Z3_fixedpoint f, Z3_string s)
Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context...
~optimize()
Definition: z3++.h:2315
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...
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 at(expr const &index) const
Definition: z3++.h:1025
void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g)
Decrement the reference counter of the given goal.
Z3_string Z3_API Z3_fixedpoint_get_reason_unknown(Z3_context c, Z3_fixedpoint d)
Retrieve a string that describes the last status returned by Z3_fixedpoint_query. ...
expr re_intersect(expr_vector const &args)
Definition: z3++.h:2857
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:2567
ast_vector_tpl< sort > sort_vector
Definition: z3++.h:69
bool is_bool() const
Return true if this is a Boolean expression.
Definition: z3++.h:618
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:2317
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:2820
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:1791
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:1828
void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m)
Decrement the reference counter of the given model.
Z3_lbool bool_value() const
Definition: z3++.h:789
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:2209
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.
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:1051
expr interpolant(expr const &a)
Definition: z3++.h:2879
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:1965
void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d)
Decrement the reference counter of the given fixedpoint context.
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:992
expr ugt(expr const &a, expr const &b)
unsigned greater than operator for bitvectors.
Definition: z3++.h:1428
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:2051
expr option(expr const &re)
Definition: z3++.h:2841
~params()
Definition: z3++.h:430
Z3_sort Z3_API Z3_get_array_sort_domain(Z3_context c, Z3_sort t)
Return the domain of the given array sort. In the case of a multi-dimensional array, this function returns the sort of the first dimension.
expr const_array(sort const &d, expr const &v)
Definition: z3++.h:2753
Z3_bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx)
Return Z3_TRUE if the given statistical data is a unsigned integer.
stats(stats const &s)
Definition: z3++.h:1903
std::string to_string() const
Definition: z3++.h:464
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f)
Retrieve set of rules from fixedpoint context.
expr set_member(expr const &s, expr const &e)
Definition: z3++.h:2797
Z3_model Z3_API Z3_mk_model(Z3_context c)
Create a fresh model object. It has reference count 0.
def is_quantifier(a)
Definition: z3py.py:1875
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:1769
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:613
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:761
sort uninterpreted_sort(char const *name)
create an uninterpreted sort with the name given by the string or symbol.
Definition: z3++.h:2469
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:1036
void reset()
Definition: z3++.h:2066
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed remainder (sign follows divisor).
T * ptr()
Definition: z3++.h:364
params(params const &s)
Definition: z3++.h:429
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:72
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.
check_result compute_interpolant(expr const &pat, params const &p, expr_vector &interp, model &m)
Interpolation support.
Definition: z3++.h:2927
Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than.
unsigned lo() const
Definition: z3++.h:996
bool is_array() const
Return true if this sort is a Array sort.
Definition: z3++.h:523
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:2331
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_param_kind
The different kinds of parameters that can be associated with parameter sets. (see Z3_mk_params)...
Definition: z3_api.h:1278
expr get_cover_delta(int level, func_decl &p)
Definition: z3++.h:2387
Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a string of a numeric constant term.
expr int_const(char const *name)
Definition: z3++.h:2555
Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 rem arg2.
friend std::ostream & operator<<(std::ostream &out, exception const &e)
Definition: z3++.h:87
expr replace(expr const &src, expr const &dst) const
Definition: z3++.h:1008
symbol(symbol const &s)
Definition: z3++.h:383
Z3_bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, Z3_bool model_completion, Z3_ast *v)
Evaluate the AST node t in the given model. Return Z3_TRUE if succeeded, and store the result in v...
expr value() const
Definition: z3++.h:1778
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.
Z3_bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.
Z3_symbol_kind
The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See Z3_...
Definition: z3_api.h:112
expr sum(expr_vector const &args)
Definition: z3++.h:1684
Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re)
Create the regular language re+.
Z3_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.
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
sort(context &c)
Definition: z3++.h:484
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:578
goal(context &c, bool models=true, bool unsat_cores=false, bool proofs=false)
Definition: z3++.h:2046
expr suffixof(expr const &a, expr const &b)
Definition: z3++.h:2814
void from_file(char const *filename)
Definition: z3++.h:2360
void Z3_API Z3_interrupt(Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers...
check_result consequences(expr_vector &assumptions, expr_vector &vars, expr_vector &conseq)
Definition: z3++.h:2002
expr operator<(expr const &a, expr const &b)
Definition: z3++.h:1311
unsigned num_exprs() const
Definition: z3++.h:2067
object(context &c)
Definition: z3++.h:371
handle add(expr const &e, unsigned weight)
Definition: z3++.h:2321
bool is_numeral(std::string &s, unsigned precision) const
Definition: z3++.h:677
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:454
object(object const &s)
Definition: z3++.h:372
expr arg(unsigned i) const
Return the i-th argument of this application. This method assumes the expression is an application...
Definition: z3++.h:831
expr atleast(expr_vector const &es, unsigned bound)
Definition: z3++.h:1676
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
expr real_const(char const *name)
Definition: z3++.h:2556
bool is_relation() const
Return true if this is a Relation expression.
Definition: z3++.h:646
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.
bool is_const() const
Return true if this expression is a constant (i.e., an application with 0 arguments).
Definition: z3++.h:685
unsigned h() const
Definition: z3++.h:2301
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:2105
unsigned Z3_API Z3_fixedpoint_get_num_levels(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred)
Query the PDR engine for the maximal levels properties are known about predicate. ...
Z3_tactic Z3_API Z3_tactic_using_params(Z3_context c, Z3_tactic t, Z3_params p)
Return a tactic that applies t using the given set of parameters.
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:2068
Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re)
Create the regular language re*.
model convert_model(model const &m, unsigned i=0) const
Definition: z3++.h:2107
Z3_bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a)
Return true if the given AST is a real algebraic number.
expr sext(expr const &a, unsigned i)
Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector.
Definition: z3++.h:1488
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:1976
Z3_sort Z3_API Z3_get_domain(Z3_context c, Z3_func_decl d, unsigned i)
Return the sort of the i-th parameter of the given function declaration.
void Z3_API Z3_fixedpoint_add_cover(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property)
Add property about the predicate pred. Add a property of predicate pred at level. It gets pushed forw...
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.
Z3_ast Z3_API Z3_mk_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.
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.
bool is_numeral_i(int &i) const
Definition: z3++.h:674
expr empty(sort const &s)
Definition: z3++.h:2809
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...
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:384
~model()
Definition: z3++.h:1826
expr_vector rules() const
Definition: z3++.h:2396
sort real_sort()
Return the Real sort.
Definition: z3++.h:2433
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:1580
expr re_full(sort const &s)
Definition: z3++.h:2852
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:1531
expr num_val(int n, sort const &s)
Definition: z3++.h:2588
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:476
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:519
symbol int_symbol(int n)
Create a Z3 symbol based on the given integer.
Definition: z3++.h:2429
Z3_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...
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:1056
expr else_value() const
Definition: z3++.h:1801
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.
expr numerator() const
Definition: z3++.h:793
expr indexof(expr const &s, expr const &substr, expr const &offset)
Definition: z3++.h:2826
void from_file(char const *s)
Definition: z3++.h:2373
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:2793
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:406
expr unit() const
Definition: z3++.h:1014
expr operator>(expr const &a, expr const &b)
Definition: z3++.h:1330
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:1066
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:130
expr star(expr const &re)
Definition: z3++.h:2844
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.
Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
expr operator==(expr const &a, expr const &b)
Definition: z3++.h:1150
symbol name() const
Return name of sort.
Definition: z3++.h:499
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:2742
param_descrs(context &c, Z3_param_descrs d)
Definition: z3++.h:404
void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value)
Set a configuration parameter.
expr operator|(expr const &a, expr const &b)
Definition: z3++.h:1357
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:997
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
unsigned num_args() const
Definition: z3++.h:1779
expr pbge(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:1652
Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re)
Create an empty regular expression of sort re.
tactic(context &c, Z3_tactic s)
Definition: z3++.h:2138
void check_context(object const &a, object const &b)
Definition: z3++.h:377
expr arg(unsigned i) const
Definition: z3++.h:1780
Z3_ast_vector Z3_API Z3_optimize_get_assertions(Z3_context c, Z3_optimize o)
Return the set of asserted formulas on the optimization context.
void check_parser_error() const
Definition: z3++.h:177
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:2554
expr urem(expr const &a, expr const &b)
unsigned reminder operator for bitvectors
Definition: z3++.h:1455
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:2149
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.
std::string reason_unknown() const
Definition: z3++.h:2007
Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize t)
Return a string containing a description of parameters accepted by optimize.
Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s)
Return the symbol name.
model get_model() const
Definition: z3++.h:2001
bool operator!=(iterator const &other)
Definition: z3++.h:1567
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:1846
params & operator=(params const &s)
Definition: z3++.h:432
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:1824
expr proof() const
Definition: z3++.h:2011
bool is_numeral_u(unsigned &i) const
Definition: z3++.h:675
check_result query(func_decl_vector &relations)
Definition: z3++.h:2377
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:2226
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:1560
symbol name() const
Definition: z3++.h:581
solver(context &c, solver const &src, translate)
Definition: z3++.h:1945
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:1941
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.
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two&#39;s complement subtraction.
func_decl(context &c, Z3_func_decl n)
Definition: z3++.h:573
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:66
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:363
handle minimize(expr const &e)
Definition: z3++.h:2334
apply_result apply(goal const &g) const
Definition: z3++.h:2150
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g)
Increment the reference counter of the given goal.
Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred)
void add(expr const &e, expr const &p)
Definition: z3++.h:1966
Z3_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_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:2709
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:1874
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
unsigned size() const
Definition: z3++.h:1850
apply_result operator()(goal const &g) const
Definition: z3++.h:2156
Z3_ast m_ast
Definition: z3++.h:452
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:439
unsigned size() const
Definition: z3++.h:1534
unsigned size() const
Definition: z3++.h:360
tactic repeat(tactic const &t, unsigned max=UINT_MAX)
Definition: z3++.h:2184
expr bool_val(bool b)
Definition: z3++.h:2559
~context()
Definition: z3++.h:164
expr operator||(expr const &a, expr const &b)
Definition: z3++.h:1137
uint64_t get_numeral_uint64() const
Return uint64_t value of numeral, throw if result cannot fit in uint64_t.
Definition: z3++.h:778
expr ult(expr const &a, expr const &b)
unsigned less than operator for bitvectors.
Definition: z3++.h:1416
bool is_var() const
Return true if this expression is a variable.
Definition: z3++.h:693
Z3_context Z3_API Z3_mk_interpolation_context(Z3_config cfg)
This function generates a Z3 context suitable for generation of interpolants. Formulas can be generat...
T * operator->() const
Definition: z3++.h:1575
void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p)
Increment the reference counter of the given parameter set.
expr_vector get_interpolant(expr const &proof, expr const &pat, params const &p)
Definition: z3++.h:2944
unsigned depth() const
Definition: z3++.h:2065
Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables...
Z3_string Z3_API Z3_tactic_get_help(Z3_context c, Z3_tactic t)
Return a string containing a description of parameters accepted by the given tactic.
void Z3_API Z3_params_set_symbol(Z3_context c, Z3_params p, Z3_symbol k, Z3_symbol v)
Add a symbol parameter k with value v to the parameter set p.
expr int_val(int n)
Definition: z3++.h:2561
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:574
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:1562
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:1746
tactic fail_if(probe const &p)
Definition: z3++.h:2410
Z3_param_kind kind(symbol const &s)
Definition: z3++.h:418
stats(context &c, Z3_stats e)
Definition: z3++.h:1902
expr exists(expr const &x, expr const &b)
Definition: z3++.h:1620
std::string to_string()
Definition: z3++.h:2400
ast operator()(context &c, Z3_ast a)
Definition: z3++.h:1494
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.
void Z3_API Z3_func_interp_set_else(Z3_context c, Z3_func_interp f, Z3_ast else_value)
Return the &#39;else&#39; value of the given function interpretation.
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two&#39;s complement multiplication.
context(config &c)
Definition: z3++.h:162
bool is_quantifier() const
Return true if this expression is a quantifier.
Definition: z3++.h:689
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.
expr ite(expr const &c, expr const &t, expr const &e)
Create the if-then-else expression ite(c, t, e)
Definition: z3++.h:1375
double apply(goal const &g) const
Definition: z3++.h:2236
func_entry(func_entry const &s)
Definition: z3++.h:1768
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...
expr eval(expr const &n, bool model_completion=false) const
Definition: z3++.h:1836
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two&#39;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:457
#define Z3_FALSE
False value. It is just an alias for 0.
Definition: z3_api.h:93
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:2009
int get_numeral_int() const
Return int value of numeral, throw if result cannot fit in machine int.
Definition: z3++.h:725
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:460
func_interp add_func_interp(func_decl &f, expr &else_val)
Definition: z3++.h:1879
expr_vector assertions() const
Definition: z3++.h:2010
unsigned num_args() const
Return the number of arguments in this application. This method assumes the expression is an applicat...
Definition: z3++.h:823
Z3_string Z3_API Z3_get_parser_error(Z3_context c)
Retrieve that last error message information generated from parsing.
unsigned bv_size() const
Return the size of this Bit-vector sort.
Definition: z3++.h:550
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:461
expr forall(expr const &x, expr const &b)
Definition: z3++.h:1596
sort(context &c, Z3_sort s)
Definition: z3++.h:485
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
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_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:1091
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...
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1084
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:1388
expr rotate_left(unsigned i)
Definition: z3++.h:990
expr concat(expr const &a, expr const &b)
Definition: z3++.h:1702
symbol(context &c, Z3_symbol s)
Definition: z3++.h:382
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:2393
solver(context &c, char const *logic)
Definition: z3++.h:1944
tactic try_for(tactic const &t, unsigned ms)
Definition: z3++.h:2195
func_interp(context &c, Z3_func_interp e)
Definition: z3++.h:1790
void register_relation(func_decl &p)
Definition: z3++.h:2394
unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d)
Alias for Z3_get_domain_size.
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.
void add_rule(expr &rule, symbol const &name)
Definition: z3++.h:2374
expr shl(expr const &a, expr const &b)
shift left operator for bitvectors
Definition: z3++.h:1462
params(context &c)
Definition: z3++.h:428
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.
void push_back(T const &e)
Definition: z3++.h:1536
expr pble(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:1644
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:68
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_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, Z3_bool v)
Add a Boolean parameter k with value v to the parameter set p.
def is_bv(a)
Definition: z3py.py:3536
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:1422
void push()
Definition: z3++.h:2337
bool is_seq() const
Return true if this sort is a Sequence sort.
Definition: z3++.h:535
bool is_numeral(std::string &s) const
Definition: z3++.h:676
void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 file with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.
bool is_double(unsigned i) const
Definition: z3++.h:1916
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:491
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:2456
context * m_ctx
Definition: z3++.h:369
unsigned size()
Definition: z3++.h:416
void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p)
Set parameters on fixedpoint context.
bool is_finite_domain() const
Return true if this is a Finite-domain expression.
Definition: z3++.h:664
expr operator-(expr const &a)
Definition: z3++.h:1253
func_interp get_func_interp(func_decl f) const
Definition: z3++.h:1865
void pop(unsigned n=1)
Definition: z3++.h:1963
expr smod(expr const &a, expr const &b)
signed modulus operator for bitvectors
Definition: z3++.h:1448
expr to_real(expr const &a)
Definition: z3++.h:2672
handle(unsigned h)
Definition: z3++.h:2300
Z3_ast_vector Z3_API Z3_get_interpolant(Z3_context c, Z3_ast pf, Z3_ast pat, Z3_params p)
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two&#39;s complement addition.
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:2034
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:671
Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a)
Create a unit sequence of a.
Z3_bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t)
Return true if the given expression t is well sorted.
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:584
bool is_seq() const
Return true if this is a sequence expression.
Definition: z3++.h:650
ast(ast const &s)
Definition: z3++.h:456
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:2445
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.
tactic par_or(unsigned n, tactic const *tactics)
Definition: z3++.h:2200
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.
sort(sort const &s)
Definition: z3++.h:486
bool is_finite_domain() const
Return true if this sort is a Finite domain sort.
Definition: z3++.h:543
Z3_bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx)
Return Z3_TRUE if the given statistical data is a double.
void pop()
Definition: z3++.h:2406
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:980
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...
apply_result(context &c, Z3_apply_result s)
Definition: z3++.h:2094
expr nand(expr const &a, expr const &b)
Definition: z3++.h:1361
unsigned Z3_API Z3_apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r)
Return the number of subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort seq)
Create a regular expression sort out of a sequence sort.
Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d)
Retrieve a formula that encodes satisfying answers to the query.
Z3_string Z3_API Z3_fixedpoint_to_string(Z3_context c, Z3_fixedpoint f, unsigned num_queries, Z3_ast queries[])
Print the current rules and background axioms as a string.
Z3_lbool Z3_API Z3_fixedpoint_query_relations(Z3_context c, Z3_fixedpoint d, unsigned num_relations, Z3_func_decl const relations[])
Pose multiple queries against the asserted rules.
expr operator/(expr const &a, expr const &b)
Definition: z3++.h:1234
Function declaration (aka function definition). It is the signature of interpreted and uninterpreted ...
Definition: z3++.h:570
expr set_union(expr const &a, expr const &b)
Definition: z3++.h:2773
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:361
param_descrs get_param_descrs()
Definition: z3++.h:2167
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.
sort int_sort()
Return the integer sort.
Definition: z3++.h:2432
goal(goal const &s)
Definition: z3++.h:2048
expr set_del(expr const &s, expr const &e)
Definition: z3++.h:2769
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:1906
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:576
apply_result & operator=(apply_result const &s)
Definition: z3++.h:2098
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:1668
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.
sort to_sort(context &c, Z3_sort s)
Definition: z3++.h:1397
context()
Definition: z3++.h:161
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:622
void add(expr const &f)
Definition: z3++.h:2058
expr to_re(expr const &s)
Definition: z3++.h:2832
void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)
Check if container contains containee.
unsigned num_funcs() const
Definition: z3++.h:1847
check_result
Definition: z3++.h:126
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:2399
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:2095