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);
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);
273  sort uninterpreted_sort(char const* name);
274  sort uninterpreted_sort(symbol const& name);
275 
276  func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range);
277  func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range);
278  func_decl function(symbol const& name, sort_vector const& domain, sort const& range);
279  func_decl function(char const * name, sort_vector const& domain, sort const& range);
280  func_decl function(char const * name, sort const & domain, sort const & range);
281  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range);
282  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range);
283  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range);
284  func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range);
285 
286  expr constant(symbol const & name, sort const & s);
287  expr constant(char const * name, sort const & s);
288  expr bool_const(char const * name);
289  expr int_const(char const * name);
290  expr real_const(char const * name);
291  expr bv_const(char const * name, unsigned sz);
292 
293  expr bool_val(bool b);
294 
295  expr int_val(int n);
296  expr int_val(unsigned n);
297  expr int_val(__int64 n);
298  expr int_val(__uint64 n);
299  expr int_val(char const * n);
300 
301  expr real_val(int n, int d);
302  expr real_val(int n);
303  expr real_val(unsigned n);
304  expr real_val(__int64 n);
306  expr real_val(char const * n);
307 
308  expr bv_val(int n, unsigned sz);
309  expr bv_val(unsigned n, unsigned sz);
310  expr bv_val(__int64 n, unsigned sz);
311  expr bv_val(__uint64 n, unsigned sz);
312  expr bv_val(char const * n, unsigned sz);
313  expr bv_val(unsigned n, bool const* bits);
314 
315  expr string_val(char const* s);
316  expr string_val(std::string const& s);
317 
318  expr num_val(int n, sort const & s);
319 
323  expr parse_string(char const* s);
324  expr parse_file(char const* file);
325 
326  expr parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
327  expr parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
328 
332  check_result compute_interpolant(expr const& pat, params const& p, expr_vector& interp, model& m);
333  expr_vector get_interpolant(expr const& proof, expr const& pat, params const& p);
334 
335  };
336 
337 
338 
339 
340  template<typename T>
341  class array {
342  T * m_array;
343  unsigned m_size;
344  array(array const & s);
345  array & operator=(array const & s);
346  public:
347  array(unsigned sz):m_size(sz) { m_array = new T[sz]; }
348  template<typename T2>
349  array(ast_vector_tpl<T2> const & v);
350  ~array() { delete[] m_array; }
351  unsigned size() const { return m_size; }
352  T & operator[](int i) { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
353  T const & operator[](int i) const { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
354  T const * ptr() const { return m_array; }
355  T * ptr() { return m_array; }
356  };
357 
358  class object {
359  protected:
361  public:
362  object(context & c):m_ctx(&c) {}
363  object(object const & s):m_ctx(s.m_ctx) {}
364  context & ctx() const { return *m_ctx; }
366  friend void check_context(object const & a, object const & b);
367  };
368  inline void check_context(object const & a, object const & b) { (void)a; (void)b; assert(a.m_ctx == b.m_ctx); }
369 
370  class symbol : public object {
371  Z3_symbol m_sym;
372  public:
373  symbol(context & c, Z3_symbol s):object(c), m_sym(s) {}
374  symbol(symbol const & s):object(s), m_sym(s.m_sym) {}
375  symbol & operator=(symbol const & s) { m_ctx = s.m_ctx; m_sym = s.m_sym; return *this; }
376  operator Z3_symbol() const { return m_sym; }
377  Z3_symbol_kind kind() const { return Z3_get_symbol_kind(ctx(), m_sym); }
378  std::string str() const { assert(kind() == Z3_STRING_SYMBOL); return Z3_get_symbol_string(ctx(), m_sym); }
379  int to_int() const { assert(kind() == Z3_INT_SYMBOL); return Z3_get_symbol_int(ctx(), m_sym); }
380  friend std::ostream & operator<<(std::ostream & out, symbol const & s);
381  };
382 
383  inline std::ostream & operator<<(std::ostream & out, symbol const & s) {
384  if (s.kind() == Z3_INT_SYMBOL)
385  out << "k!" << s.to_int();
386  else
387  out << s.str().c_str();
388  return out;
389  }
390 
391 
392  class param_descrs : public object {
393  Z3_param_descrs m_descrs;
394  public:
395  param_descrs(context& c, Z3_param_descrs d): object(c), m_descrs(d) { Z3_param_descrs_inc_ref(c, d); }
396  param_descrs(param_descrs const& o): object(o.ctx()), m_descrs(o.m_descrs) { Z3_param_descrs_inc_ref(ctx(), m_descrs); }
398  Z3_param_descrs_inc_ref(o.ctx(), o.m_descrs);
399  Z3_param_descrs_dec_ref(ctx(), m_descrs);
400  m_descrs = o.m_descrs;
401  m_ctx = o.m_ctx;
402  return *this;
403  }
406 
407  unsigned size() { return Z3_param_descrs_size(ctx(), m_descrs); }
408  symbol name(unsigned i) { return symbol(ctx(), Z3_param_descrs_get_name(ctx(), m_descrs, i)); }
409  Z3_param_kind kind(symbol const& s) { return Z3_param_descrs_get_kind(ctx(), m_descrs, s); }
410  std::string documentation(symbol const& s) { char const* r = Z3_param_descrs_get_documentation(ctx(), m_descrs, s); check_error(); return r; }
411  std::string to_string() const { return Z3_param_descrs_to_string(ctx(), m_descrs); }
412  };
413 
414  inline std::ostream& operator<<(std::ostream & out, param_descrs const & d) { return out << d.to_string(); }
415 
416  class params : public object {
417  Z3_params m_params;
418  public:
419  params(context & c):object(c) { m_params = Z3_mk_params(c); Z3_params_inc_ref(ctx(), m_params); }
420  params(params const & s):object(s), m_params(s.m_params) { Z3_params_inc_ref(ctx(), m_params); }
421  ~params() { Z3_params_dec_ref(ctx(), m_params); }
422  operator Z3_params() const { return m_params; }
423  params & operator=(params const & s) {
424  Z3_params_inc_ref(s.ctx(), s.m_params);
425  Z3_params_dec_ref(ctx(), m_params);
426  m_ctx = s.m_ctx;
427  m_params = s.m_params;
428  return *this;
429  }
430  void set(char const * k, bool b) { Z3_params_set_bool(ctx(), m_params, ctx().str_symbol(k), b); }
431  void set(char const * k, unsigned n) { Z3_params_set_uint(ctx(), m_params, ctx().str_symbol(k), n); }
432  void set(char const * k, double n) { Z3_params_set_double(ctx(), m_params, ctx().str_symbol(k), n); }
433  void set(char const * k, symbol const & s) { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), s); }
434  friend std::ostream & operator<<(std::ostream & out, params const & p);
435  };
436 
437  inline std::ostream & operator<<(std::ostream & out, params const & p) {
438  out << Z3_params_to_string(p.ctx(), p); return out;
439  }
440 
441  class ast : public object {
442  protected:
443  Z3_ast m_ast;
444  public:
445  ast(context & c):object(c), m_ast(0) {}
446  ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
447  ast(ast const & s):object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
448  ~ast() { if (m_ast) Z3_dec_ref(*m_ctx, m_ast); }
449  operator Z3_ast() const { return m_ast; }
450  operator bool() const { return m_ast != 0; }
451  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; }
452  Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }
453  unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }
454  friend std::ostream & operator<<(std::ostream & out, ast const & n);
455  std::string to_string() const { return std::string(Z3_ast_to_string(ctx(), m_ast)); }
456 
457 
461  friend bool eq(ast const & a, ast const & b);
462  };
463  inline std::ostream & operator<<(std::ostream & out, ast const & n) {
464  out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
465  }
466 
467  inline bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b) != 0; }
468 
469 
473  class sort : public ast {
474  public:
475  sort(context & c):ast(c) {}
476  sort(context & c, Z3_sort s):ast(c, reinterpret_cast<Z3_ast>(s)) {}
477  sort(sort const & s):ast(s) {}
478  operator Z3_sort() const { return reinterpret_cast<Z3_sort>(m_ast); }
482  sort & operator=(sort const & s) { return static_cast<sort&>(ast::operator=(s)); }
486  Z3_sort_kind sort_kind() const { return Z3_get_sort_kind(*m_ctx, *this); }
490  symbol name() const { Z3_symbol s = Z3_get_sort_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
494  bool is_bool() const { return sort_kind() == Z3_BOOL_SORT; }
498  bool is_int() const { return sort_kind() == Z3_INT_SORT; }
502  bool is_real() const { return sort_kind() == Z3_REAL_SORT; }
506  bool is_arith() const { return is_int() || is_real(); }
510  bool is_bv() const { return sort_kind() == Z3_BV_SORT; }
514  bool is_array() const { return sort_kind() == Z3_ARRAY_SORT; }
518  bool is_datatype() const { return sort_kind() == Z3_DATATYPE_SORT; }
522  bool is_relation() const { return sort_kind() == Z3_RELATION_SORT; }
526  bool is_seq() const { return sort_kind() == Z3_SEQ_SORT; }
530  bool is_re() const { return sort_kind() == Z3_RE_SORT; }
534  bool is_finite_domain() const { return sort_kind() == Z3_FINITE_DOMAIN_SORT; }
535 
541  unsigned bv_size() const { assert(is_bv()); unsigned r = Z3_get_bv_sort_size(ctx(), *this); check_error(); return r; }
542 
548  sort array_domain() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_domain(ctx(), *this); check_error(); return sort(ctx(), s); }
554  sort array_range() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_range(ctx(), *this); check_error(); return sort(ctx(), s); }
555  };
556 
561  class func_decl : public ast {
562  public:
563  func_decl(context & c):ast(c) {}
564  func_decl(context & c, Z3_func_decl n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
565  func_decl(func_decl const & s):ast(s) {}
566  operator Z3_func_decl() const { return reinterpret_cast<Z3_func_decl>(m_ast); }
567  func_decl & operator=(func_decl const & s) { return static_cast<func_decl&>(ast::operator=(s)); }
568 
569  unsigned arity() const { return Z3_get_arity(ctx(), *this); }
570  sort domain(unsigned i) const { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }
571  sort range() const { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }
572  symbol name() const { Z3_symbol s = Z3_get_decl_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
573  Z3_decl_kind decl_kind() const { return Z3_get_decl_kind(ctx(), *this); }
574 
575  bool is_const() const { return arity() == 0; }
576 
577  expr operator()() const;
578  expr operator()(unsigned n, expr const * args) const;
579  expr operator()(expr_vector const& v) const;
580  expr operator()(expr const & a) const;
581  expr operator()(int a) const;
582  expr operator()(expr const & a1, expr const & a2) const;
583  expr operator()(expr const & a1, int a2) const;
584  expr operator()(int a1, expr const & a2) const;
585  expr operator()(expr const & a1, expr const & a2, expr const & a3) const;
586  expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const;
587  expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const;
588  };
589 
594  class expr : public ast {
595  public:
596  expr(context & c):ast(c) {}
597  expr(context & c, Z3_ast n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
598  expr(expr const & n):ast(n) {}
599  expr & operator=(expr const & n) { return static_cast<expr&>(ast::operator=(n)); }
600 
604  sort get_sort() const { Z3_sort s = Z3_get_sort(*m_ctx, m_ast); check_error(); return sort(*m_ctx, s); }
605 
609  bool is_bool() const { return get_sort().is_bool(); }
613  bool is_int() const { return get_sort().is_int(); }
617  bool is_real() const { return get_sort().is_real(); }
621  bool is_arith() const { return get_sort().is_arith(); }
625  bool is_bv() const { return get_sort().is_bv(); }
629  bool is_array() const { return get_sort().is_array(); }
633  bool is_datatype() const { return get_sort().is_datatype(); }
637  bool is_relation() const { return get_sort().is_relation(); }
641  bool is_seq() const { return get_sort().is_seq(); }
645  bool is_re() const { return get_sort().is_re(); }
646 
655  bool is_finite_domain() const { return get_sort().is_finite_domain(); }
656 
662  bool is_numeral() const { return kind() == Z3_NUMERAL_AST; }
663  bool is_numeral_i64(__int64& i) const { bool r = 0 != Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}
664  bool is_numeral_u64(__uint64& i) const { bool r = 0 != Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}
665  bool is_numeral_i(int& i) const { bool r = 0 != Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}
666  bool is_numeral_u(unsigned& i) const { bool r = 0 != Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
667  bool is_numeral(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; }
668  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; }
672  bool is_app() const { return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
676  bool is_const() const { return is_app() && num_args() == 0; }
680  bool is_quantifier() const { return kind() == Z3_QUANTIFIER_AST; }
684  bool is_var() const { return kind() == Z3_VAR_AST; }
688  bool is_algebraic() const { return 0 != Z3_is_algebraic_number(ctx(), m_ast); }
689 
693  bool is_well_sorted() const { bool r = Z3_is_well_sorted(ctx(), m_ast) != 0; check_error(); return r; }
694 
701  std::string get_decimal_string(int precision) const {
702  assert(is_numeral() || is_algebraic());
703  return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
704  }
705 
716  int get_numeral_int() const {
717  int result = 0;
718  if (!is_numeral_i(result)) {
719  assert(ctx().enable_exceptions());
720  if (!ctx().enable_exceptions()) return 0;
721  Z3_THROW(exception("numeral does not fit in machine int"));
722  }
723  return result;
724  }
725 
735  unsigned get_numeral_uint() const {
736  assert(is_numeral());
737  unsigned result = 0;
738  if (!is_numeral_u(result)) {
739  assert(ctx().enable_exceptions());
740  if (!ctx().enable_exceptions()) return 0;
741  Z3_THROW(exception("numeral does not fit in machine uint"));
742  }
743  return result;
744  }
745 
753  assert(is_numeral());
754  __int64 result = 0;
755  if (!is_numeral_i64(result)) {
756  assert(ctx().enable_exceptions());
757  if (!ctx().enable_exceptions()) return 0;
758  Z3_THROW(exception("numeral does not fit in machine __int64"));
759  }
760  return result;
761  }
762 
770  assert(is_numeral());
771  __uint64 result = 0;
772  if (!is_numeral_u64(result)) {
773  assert(ctx().enable_exceptions());
774  if (!ctx().enable_exceptions()) return 0;
775  Z3_THROW(exception("numeral does not fit in machine __uint64"));
776  }
777  return result;
778  }
779 
781  return Z3_get_bool_value(ctx(), m_ast);
782  }
783 
784  expr numerator() const {
785  assert(is_numeral());
786  Z3_ast r = Z3_get_numerator(ctx(), m_ast);
787  check_error();
788  return expr(ctx(),r);
789  }
790 
791 
792  expr denominator() const {
793  assert(is_numeral());
794  Z3_ast r = Z3_get_denominator(ctx(), m_ast);
795  check_error();
796  return expr(ctx(),r);
797  }
798 
799  operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
800 
807  func_decl decl() const { Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }
814  unsigned num_args() const { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
822  expr arg(unsigned i) const { Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }
823 
829  expr body() const { assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
830 
836  friend expr operator!(expr const & a);
837 
838 
845  friend expr operator&&(expr const & a, expr const & b);
846 
847 
854  friend expr operator&&(expr const & a, bool b);
861  friend expr operator&&(bool a, expr const & b);
862 
869  friend expr operator||(expr const & a, expr const & b);
876  friend expr operator||(expr const & a, bool b);
877 
884  friend expr operator||(bool a, expr const & b);
885 
886  friend expr implies(expr const & a, expr const & b);
887  friend expr implies(expr const & a, bool b);
888  friend expr implies(bool a, expr const & b);
889 
890  friend expr mk_or(expr_vector const& args);
891  friend expr mk_and(expr_vector const& args);
892 
893  friend expr ite(expr const & c, expr const & t, expr const & e);
894 
895  friend expr distinct(expr_vector const& args);
896  friend expr concat(expr const& a, expr const& b);
897  friend expr concat(expr_vector const& args);
898 
899  friend expr operator==(expr const & a, expr const & b);
900  friend expr operator==(expr const & a, int b);
901  friend expr operator==(int a, expr const & b);
902 
903  friend expr operator!=(expr const & a, expr const & b);
904  friend expr operator!=(expr const & a, int b);
905  friend expr operator!=(int a, expr const & b);
906 
907  friend expr operator+(expr const & a, expr const & b);
908  friend expr operator+(expr const & a, int b);
909  friend expr operator+(int a, expr const & b);
910  friend expr sum(expr_vector const& args);
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  /* \brief Power operator */
917  friend expr pw(expr const & a, expr const & b);
918  friend expr pw(expr const & a, int b);
919  friend expr pw(int a, expr const & b);
920 
921  /* \brief mod operator */
922  friend expr mod(expr const& a, expr const& b);
923  friend expr mod(expr const& a, int b);
924  friend expr mod(int a, expr const& b);
925 
926  /* \brief rem operator */
927  friend expr rem(expr const& a, expr const& b);
928  friend expr rem(expr const& a, int b);
929  friend expr rem(int a, expr const& b);
930 
931  friend expr is_int(expr const& e);
932 
933  friend expr operator/(expr const & a, expr const & b);
934  friend expr operator/(expr const & a, int b);
935  friend expr operator/(int a, expr const & b);
936 
937  friend expr operator-(expr const & a);
938 
939  friend expr operator-(expr const & a, expr const & b);
940  friend expr operator-(expr const & a, int b);
941  friend expr operator-(int a, expr const & b);
942 
943  friend expr operator<=(expr const & a, expr const & b);
944  friend expr operator<=(expr const & a, int b);
945  friend expr operator<=(int a, expr const & b);
946 
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  friend expr operator>(expr const & a, expr const & b);
957  friend expr operator>(expr const & a, int b);
958  friend expr operator>(int a, expr const & b);
959 
960  friend expr pble(expr_vector const& es, int const * coeffs, int bound);
961  friend expr pbge(expr_vector const& es, int const * coeffs, int bound);
962  friend expr pbeq(expr_vector const& es, int const * coeffs, int bound);
963  friend expr atmost(expr_vector const& es, unsigned bound);
964  friend expr atleast(expr_vector const& es, unsigned bound);
965 
966  friend expr operator&(expr const & a, expr const & b);
967  friend expr operator&(expr const & a, int b);
968  friend expr operator&(int a, expr const & b);
969 
970  friend expr operator^(expr const & a, expr const & b);
971  friend expr operator^(expr const & a, int b);
972  friend expr operator^(int a, expr const & b);
973 
974  friend expr operator|(expr const & a, expr const & b);
975  friend expr operator|(expr const & a, int b);
976  friend expr operator|(int a, expr const & b);
977  friend expr nand(expr const& a, expr const& b);
978  friend expr nor(expr const& a, expr const& b);
979  friend expr xnor(expr const& a, expr const& b);
980 
981  expr rotate_left(unsigned i) { Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
982  expr rotate_right(unsigned i) { Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
983  expr repeat(unsigned i) { Z3_ast r = Z3_mk_repeat(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
984 
985  friend expr operator~(expr const & a);
986  expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }
987  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)); }
988  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)); }
989 
995  expr extract(expr const& offset, expr const& length) const {
996  check_context(*this, offset); check_context(offset, length);
997  Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
998  }
999  expr replace(expr const& src, expr const& dst) const {
1000  check_context(*this, src); check_context(src, dst);
1001  Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
1002  check_error();
1003  return expr(ctx(), r);
1004  }
1005  expr unit() const {
1006  Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
1007  check_error();
1008  return expr(ctx(), r);
1009  }
1010  expr contains(expr const& s) {
1011  check_context(*this, s);
1012  Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
1013  check_error();
1014  return expr(ctx(), r);
1015  }
1016  expr at(expr const& index) const {
1017  check_context(*this, index);
1018  Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
1019  check_error();
1020  return expr(ctx(), r);
1021  }
1022  expr length() const {
1023  Z3_ast r = Z3_mk_seq_length(ctx(), *this);
1024  check_error();
1025  return expr(ctx(), r);
1026  }
1027  expr stoi() const {
1028  Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
1029  check_error();
1030  return expr(ctx(), r);
1031  }
1032  expr itos() const {
1033  Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
1034  check_error();
1035  return expr(ctx(), r);
1036  }
1037 
1038  friend expr range(expr const& lo, expr const& hi);
1042  expr loop(unsigned lo) {
1043  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0);
1044  check_error();
1045  return expr(ctx(), r);
1046  }
1047  expr loop(unsigned lo, unsigned hi) {
1048  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi);
1049  check_error();
1050  return expr(ctx(), r);
1051  }
1052 
1053 
1057  expr simplify() const { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
1061  expr simplify(params const & p) const { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
1062 
1066  expr substitute(expr_vector const& src, expr_vector const& dst);
1067 
1071  expr substitute(expr_vector const& dst);
1072 
1073  };
1074 
1075 #define _Z3_MK_BIN_(a, b, binop) \
1076  check_context(a, b); \
1077  Z3_ast r = binop(a.ctx(), a, b); \
1078  a.check_error(); \
1079  return expr(a.ctx(), r); \
1080 
1081 
1082  inline expr implies(expr const & a, expr const & b) {
1083  assert(a.is_bool() && b.is_bool());
1084  _Z3_MK_BIN_(a, b, Z3_mk_implies);
1085  }
1086  inline expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); }
1087  inline expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); }
1088 
1089 
1090  inline expr pw(expr const & a, expr const & b) { _Z3_MK_BIN_(a, b, Z3_mk_power); }
1091  inline expr pw(expr const & a, int b) { return pw(a, a.ctx().num_val(b, a.get_sort())); }
1092  inline expr pw(int a, expr const & b) { return pw(b.ctx().num_val(a, b.get_sort()), b); }
1093 
1094  inline expr mod(expr const& a, expr const& b) { _Z3_MK_BIN_(a, b, Z3_mk_mod); }
1095  inline expr mod(expr const & a, int b) { return mod(a, a.ctx().num_val(b, a.get_sort())); }
1096  inline expr mod(int a, expr const & b) { return mod(b.ctx().num_val(a, b.get_sort()), b); }
1097 
1098  inline expr rem(expr const& a, expr const& b) { _Z3_MK_BIN_(a, b, Z3_mk_rem); }
1099  inline expr rem(expr const & a, int b) { return rem(a, a.ctx().num_val(b, a.get_sort())); }
1100  inline expr rem(int a, expr const & b) { return rem(b.ctx().num_val(a, b.get_sort()), b); }
1101 
1102 #undef _Z3_MK_BIN_
1103 
1104 #define _Z3_MK_UN_(a, mkun) \
1105  Z3_ast r = mkun(a.ctx(), a); \
1106  a.check_error(); \
1107  return expr(a.ctx(), r); \
1108 
1109 
1110  inline expr operator!(expr const & a) { assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); }
1111 
1112  inline expr is_int(expr const& e) { _Z3_MK_UN_(e, Z3_mk_is_int); }
1113 
1114 #undef _Z3_MK_UN_
1115 
1116  inline expr operator&&(expr const & a, expr const & b) {
1117  check_context(a, b);
1118  assert(a.is_bool() && b.is_bool());
1119  Z3_ast args[2] = { a, b };
1120  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1121  a.check_error();
1122  return expr(a.ctx(), r);
1123  }
1124 
1125  inline expr operator&&(expr const & a, bool b) { return a && a.ctx().bool_val(b); }
1126  inline expr operator&&(bool a, expr const & b) { return b.ctx().bool_val(a) && b; }
1127 
1128  inline expr operator||(expr const & a, expr const & b) {
1129  check_context(a, b);
1130  assert(a.is_bool() && b.is_bool());
1131  Z3_ast args[2] = { a, b };
1132  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1133  a.check_error();
1134  return expr(a.ctx(), r);
1135  }
1136 
1137  inline expr operator||(expr const & a, bool b) { return a || a.ctx().bool_val(b); }
1138 
1139  inline expr operator||(bool a, expr const & b) { return b.ctx().bool_val(a) || b; }
1140 
1141  inline expr operator==(expr const & a, expr const & b) {
1142  check_context(a, b);
1143  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1144  a.check_error();
1145  return expr(a.ctx(), r);
1146  }
1147  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()); }
1148  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; }
1149 
1150  inline expr operator!=(expr const & a, expr const & b) {
1151  check_context(a, b);
1152  Z3_ast args[2] = { a, b };
1153  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1154  a.check_error();
1155  return expr(a.ctx(), r);
1156  }
1157  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()); }
1158  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; }
1159 
1160  inline expr operator+(expr const & a, expr const & b) {
1161  check_context(a, b);
1162  Z3_ast r = 0;
1163  if (a.is_arith() && b.is_arith()) {
1164  Z3_ast args[2] = { a, b };
1165  r = Z3_mk_add(a.ctx(), 2, args);
1166  }
1167  else if (a.is_bv() && b.is_bv()) {
1168  r = Z3_mk_bvadd(a.ctx(), a, b);
1169  }
1170  else if (a.is_seq() && b.is_seq()) {
1171  return concat(a, b);
1172  }
1173  else if (a.is_re() && b.is_re()) {
1174  Z3_ast _args[2] = { a, b };
1175  r = Z3_mk_re_union(a.ctx(), 2, _args);
1176  }
1177  else {
1178  // operator is not supported by given arguments.
1179  assert(false);
1180  }
1181  a.check_error();
1182  return expr(a.ctx(), r);
1183  }
1184  inline expr operator+(expr const & a, int b) { return a + a.ctx().num_val(b, a.get_sort()); }
1185  inline expr operator+(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) + b; }
1186 
1187  inline expr operator*(expr const & a, expr const & b) {
1188  check_context(a, b);
1189  Z3_ast r = 0;
1190  if (a.is_arith() && b.is_arith()) {
1191  Z3_ast args[2] = { a, b };
1192  r = Z3_mk_mul(a.ctx(), 2, args);
1193  }
1194  else if (a.is_bv() && b.is_bv()) {
1195  r = Z3_mk_bvmul(a.ctx(), a, b);
1196  }
1197  else {
1198  // operator is not supported by given arguments.
1199  assert(false);
1200  }
1201  a.check_error();
1202  return expr(a.ctx(), r);
1203  }
1204  inline expr operator*(expr const & a, int b) { return a * a.ctx().num_val(b, a.get_sort()); }
1205  inline expr operator*(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) * b; }
1206 
1207 
1208  inline expr operator>=(expr const & a, expr const & b) {
1209  check_context(a, b);
1210  Z3_ast r = 0;
1211  if (a.is_arith() && b.is_arith()) {
1212  r = Z3_mk_ge(a.ctx(), a, b);
1213  }
1214  else if (a.is_bv() && b.is_bv()) {
1215  r = Z3_mk_bvsge(a.ctx(), a, b);
1216  }
1217  else {
1218  // operator is not supported by given arguments.
1219  assert(false);
1220  }
1221  a.check_error();
1222  return expr(a.ctx(), r);
1223  }
1224 
1225  inline expr operator/(expr const & a, expr const & b) {
1226  check_context(a, b);
1227  Z3_ast r = 0;
1228  if (a.is_arith() && b.is_arith()) {
1229  r = Z3_mk_div(a.ctx(), a, b);
1230  }
1231  else if (a.is_bv() && b.is_bv()) {
1232  r = Z3_mk_bvsdiv(a.ctx(), a, b);
1233  }
1234  else {
1235  // operator is not supported by given arguments.
1236  assert(false);
1237  }
1238  a.check_error();
1239  return expr(a.ctx(), r);
1240  }
1241  inline expr operator/(expr const & a, int b) { return a / a.ctx().num_val(b, a.get_sort()); }
1242  inline expr operator/(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) / b; }
1243 
1244  inline expr operator-(expr const & a) {
1245  Z3_ast r = 0;
1246  if (a.is_arith()) {
1247  r = Z3_mk_unary_minus(a.ctx(), a);
1248  }
1249  else if (a.is_bv()) {
1250  r = Z3_mk_bvneg(a.ctx(), a);
1251  }
1252  else {
1253  // operator is not supported by given arguments.
1254  assert(false);
1255  }
1256  a.check_error();
1257  return expr(a.ctx(), r);
1258  }
1259 
1260  inline expr operator-(expr const & a, expr const & b) {
1261  check_context(a, b);
1262  Z3_ast r = 0;
1263  if (a.is_arith() && b.is_arith()) {
1264  Z3_ast args[2] = { a, b };
1265  r = Z3_mk_sub(a.ctx(), 2, args);
1266  }
1267  else if (a.is_bv() && b.is_bv()) {
1268  r = Z3_mk_bvsub(a.ctx(), a, b);
1269  }
1270  else {
1271  // operator is not supported by given arguments.
1272  assert(false);
1273  }
1274  a.check_error();
1275  return expr(a.ctx(), r);
1276  }
1277  inline expr operator-(expr const & a, int b) { return a - a.ctx().num_val(b, a.get_sort()); }
1278  inline expr operator-(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) - b; }
1279 
1280  inline expr operator<=(expr const & a, expr const & b) {
1281  check_context(a, b);
1282  Z3_ast r = 0;
1283  if (a.is_arith() && b.is_arith()) {
1284  r = Z3_mk_le(a.ctx(), a, b);
1285  }
1286  else if (a.is_bv() && b.is_bv()) {
1287  r = Z3_mk_bvsle(a.ctx(), a, b);
1288  }
1289  else {
1290  // operator is not supported by given arguments.
1291  assert(false);
1292  }
1293  a.check_error();
1294  return expr(a.ctx(), r);
1295  }
1296  inline expr operator<=(expr const & a, int b) { return a <= a.ctx().num_val(b, a.get_sort()); }
1297  inline expr operator<=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) <= b; }
1298 
1299  inline expr operator>=(expr const & a, int b) { return a >= a.ctx().num_val(b, a.get_sort()); }
1300  inline expr operator>=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) >= b; }
1301 
1302  inline expr operator<(expr const & a, expr const & b) {
1303  check_context(a, b);
1304  Z3_ast r = 0;
1305  if (a.is_arith() && b.is_arith()) {
1306  r = Z3_mk_lt(a.ctx(), a, b);
1307  }
1308  else if (a.is_bv() && b.is_bv()) {
1309  r = Z3_mk_bvslt(a.ctx(), a, b);
1310  }
1311  else {
1312  // operator is not supported by given arguments.
1313  assert(false);
1314  }
1315  a.check_error();
1316  return expr(a.ctx(), r);
1317  }
1318  inline expr operator<(expr const & a, int b) { return a < a.ctx().num_val(b, a.get_sort()); }
1319  inline expr operator<(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) < b; }
1320 
1321  inline expr operator>(expr const & a, expr const & b) {
1322  check_context(a, b);
1323  Z3_ast r = 0;
1324  if (a.is_arith() && b.is_arith()) {
1325  r = Z3_mk_gt(a.ctx(), a, b);
1326  }
1327  else if (a.is_bv() && b.is_bv()) {
1328  r = Z3_mk_bvsgt(a.ctx(), a, b);
1329  }
1330  else {
1331  // operator is not supported by given arguments.
1332  assert(false);
1333  }
1334  a.check_error();
1335  return expr(a.ctx(), r);
1336  }
1337  inline expr operator>(expr const & a, int b) { return a > a.ctx().num_val(b, a.get_sort()); }
1338  inline expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > b; }
1339 
1340  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); }
1341  inline expr operator&(expr const & a, int b) { return a & a.ctx().num_val(b, a.get_sort()); }
1342  inline expr operator&(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) & b; }
1343 
1344  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); }
1345  inline expr operator^(expr const & a, int b) { return a ^ a.ctx().num_val(b, a.get_sort()); }
1346  inline expr operator^(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) ^ b; }
1347 
1348  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); }
1349  inline expr operator|(expr const & a, int b) { return a | a.ctx().num_val(b, a.get_sort()); }
1350  inline expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; }
1351 
1352  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); }
1353  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); }
1354  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); }
1355 
1356  inline expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
1357 
1358 
1359 
1366  inline expr ite(expr const & c, expr const & t, expr const & e) {
1367  check_context(c, t); check_context(c, e);
1368  assert(c.is_bool());
1369  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
1370  c.check_error();
1371  return expr(c.ctx(), r);
1372  }
1373 
1374 
1379  inline expr to_expr(context & c, Z3_ast a) {
1380  c.check_error();
1381  assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
1382  Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
1383  Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
1385  return expr(c, a);
1386  }
1387 
1388  inline sort to_sort(context & c, Z3_sort s) {
1389  c.check_error();
1390  return sort(c, s);
1391  }
1392 
1393  inline func_decl to_func_decl(context & c, Z3_func_decl f) {
1394  c.check_error();
1395  return func_decl(c, f);
1396  }
1397 
1401  inline expr ule(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
1402  inline expr ule(expr const & a, int b) { return ule(a, a.ctx().num_val(b, a.get_sort())); }
1403  inline expr ule(int a, expr const & b) { return ule(b.ctx().num_val(a, b.get_sort()), b); }
1407  inline expr ult(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }
1408  inline expr ult(expr const & a, int b) { return ult(a, a.ctx().num_val(b, a.get_sort())); }
1409  inline expr ult(int a, expr const & b) { return ult(b.ctx().num_val(a, b.get_sort()), b); }
1413  inline expr uge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }
1414  inline expr uge(expr const & a, int b) { return uge(a, a.ctx().num_val(b, a.get_sort())); }
1415  inline expr uge(int a, expr const & b) { return uge(b.ctx().num_val(a, b.get_sort()), b); }
1419  inline expr ugt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
1420  inline expr ugt(expr const & a, int b) { return ugt(a, a.ctx().num_val(b, a.get_sort())); }
1421  inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), b); }
1425  inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
1426  inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); }
1427  inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); }
1428 
1432  inline expr srem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsrem(a.ctx(), a, b)); }
1433  inline expr srem(expr const & a, int b) { return srem(a, a.ctx().num_val(b, a.get_sort())); }
1434  inline expr srem(int a, expr const & b) { return srem(b.ctx().num_val(a, b.get_sort()), b); }
1435 
1439  inline expr smod(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsmod(a.ctx(), a, b)); }
1440  inline expr smod(expr const & a, int b) { return smod(a, a.ctx().num_val(b, a.get_sort())); }
1441  inline expr smod(int a, expr const & b) { return smod(b.ctx().num_val(a, b.get_sort()), b); }
1442 
1446  inline expr urem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvurem(a.ctx(), a, b)); }
1447  inline expr urem(expr const & a, int b) { return urem(a, a.ctx().num_val(b, a.get_sort())); }
1448  inline expr urem(int a, expr const & b) { return urem(b.ctx().num_val(a, b.get_sort()), b); }
1449 
1453  inline expr shl(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvshl(a.ctx(), a, b)); }
1454  inline expr shl(expr const & a, int b) { return shl(a, a.ctx().num_val(b, a.get_sort())); }
1455  inline expr shl(int a, expr const & b) { return shl(b.ctx().num_val(a, b.get_sort()), b); }
1456 
1460  inline expr lshr(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvlshr(a.ctx(), a, b)); }
1461  inline expr lshr(expr const & a, int b) { return lshr(a, a.ctx().num_val(b, a.get_sort())); }
1462  inline expr lshr(int a, expr const & b) { return lshr(b.ctx().num_val(a, b.get_sort()), b); }
1463 
1467  inline expr ashr(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvashr(a.ctx(), a, b)); }
1468  inline expr ashr(expr const & a, int b) { return ashr(a, a.ctx().num_val(b, a.get_sort())); }
1469  inline expr ashr(int a, expr const & b) { return ashr(b.ctx().num_val(a, b.get_sort()), b); }
1470 
1474  inline expr zext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_zero_ext(a.ctx(), i, a)); }
1475 
1479  inline expr sext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_sign_ext(a.ctx(), i, a)); }
1480 
1481  template<typename T> class cast_ast;
1482 
1483  template<> class cast_ast<ast> {
1484  public:
1485  ast operator()(context & c, Z3_ast a) { return ast(c, a); }
1486  };
1487 
1488  template<> class cast_ast<expr> {
1489  public:
1490  expr operator()(context & c, Z3_ast a) {
1491  assert(Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
1492  Z3_get_ast_kind(c, a) == Z3_APP_AST ||
1494  Z3_get_ast_kind(c, a) == Z3_VAR_AST);
1495  return expr(c, a);
1496  }
1497  };
1498 
1499  template<> class cast_ast<sort> {
1500  public:
1501  sort operator()(context & c, Z3_ast a) {
1502  assert(Z3_get_ast_kind(c, a) == Z3_SORT_AST);
1503  return sort(c, reinterpret_cast<Z3_sort>(a));
1504  }
1505  };
1506 
1507  template<> class cast_ast<func_decl> {
1508  public:
1509  func_decl operator()(context & c, Z3_ast a) {
1510  assert(Z3_get_ast_kind(c, a) == Z3_FUNC_DECL_AST);
1511  return func_decl(c, reinterpret_cast<Z3_func_decl>(a));
1512  }
1513  };
1514 
1515  template<typename T>
1516  class ast_vector_tpl : public object {
1517  Z3_ast_vector m_vector;
1518  void init(Z3_ast_vector v) { Z3_ast_vector_inc_ref(ctx(), v); m_vector = v; }
1519  public:
1521  ast_vector_tpl(context & c, Z3_ast_vector v):object(c) { init(v); }
1522  ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
1524  operator Z3_ast_vector() const { return m_vector; }
1525  unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); }
1526  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); }
1527  void push_back(T const & e) { Z3_ast_vector_push(ctx(), m_vector, e); check_error(); }
1528  void resize(unsigned sz) { Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }
1529  T back() const { return operator[](size() - 1); }
1530  void pop_back() { assert(size() > 0); resize(size() - 1); }
1531  bool empty() const { return size() == 0; }
1533  Z3_ast_vector_inc_ref(s.ctx(), s.m_vector);
1534  Z3_ast_vector_dec_ref(ctx(), m_vector);
1535  m_ctx = s.m_ctx;
1536  m_vector = s.m_vector;
1537  return *this;
1538  }
1539  /*
1540  Disabled pending C++98 build upgrade
1541  bool contains(T const& x) const {
1542  for (T y : *this) if (eq(x, y)) return true;
1543  return false;
1544  }
1545  */
1546 
1547  class iterator {
1548  ast_vector_tpl const* m_vector;
1549  unsigned m_index;
1550  public:
1551  iterator(ast_vector_tpl const* v, unsigned i): m_vector(v), m_index(i) {}
1552  iterator(iterator& other): m_vector(other.m_vector), m_index(other.m_index) {}
1553  iterator operator=(iterator const& other) { m_vector = other.m_vector; m_index = other.m_index; return *this; }
1554 
1555  bool operator==(iterator const& other) {
1556  return other.m_index == m_index;
1557  };
1558  bool operator!=(iterator const& other) {
1559  return other.m_index != m_index;
1560  };
1562  ++m_index;
1563  return *this;
1564  }
1565  iterator operator++(int) { iterator tmp = *this; ++m_index; return tmp; }
1566  T * operator->() const { return &(operator*()); }
1567  T operator*() const { return (*m_vector)[m_index]; }
1568  };
1569  iterator begin() const { return iterator(this, 0); }
1570  iterator end() const { return iterator(this, size()); }
1571  friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
1572  };
1573 
1574 
1575  template<typename T>
1576  template<typename T2>
1578  m_array = new T[v.size()];
1579  m_size = v.size();
1580  for (unsigned i = 0; i < m_size; i++) {
1581  m_array[i] = v[i];
1582  }
1583  }
1584 
1585  // Basic functions for creating quantified formulas.
1586  // The C API should be used for creating quantifiers with patterns, weights, many variables, etc.
1587  inline expr forall(expr const & x, expr const & b) {
1588  check_context(x, b);
1589  Z3_app vars[] = {(Z3_app) x};
1590  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1591  }
1592  inline expr forall(expr const & x1, expr const & x2, expr const & b) {
1593  check_context(x1, b); check_context(x2, b);
1594  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1595  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1596  }
1597  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
1598  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1599  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1600  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1601  }
1602  inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
1603  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1604  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1605  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1606  }
1607  inline expr forall(expr_vector const & xs, expr const & b) {
1608  array<Z3_app> vars(xs);
1609  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);
1610  }
1611  inline expr exists(expr const & x, expr const & b) {
1612  check_context(x, b);
1613  Z3_app vars[] = {(Z3_app) x};
1614  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1615  }
1616  inline expr exists(expr const & x1, expr const & x2, expr const & b) {
1617  check_context(x1, b); check_context(x2, b);
1618  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1619  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1620  }
1621  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
1622  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1623  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1624  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1625  }
1626  inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
1627  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1628  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1629  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1630  }
1631  inline expr exists(expr_vector const & xs, expr const & b) {
1632  array<Z3_app> vars(xs);
1633  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);
1634  }
1635  inline expr pble(expr_vector const& es, int const* coeffs, int bound) {
1636  assert(es.size() > 0);
1637  context& ctx = es[0].ctx();
1638  array<Z3_ast> _es(es);
1639  Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
1640  ctx.check_error();
1641  return expr(ctx, r);
1642  }
1643  inline expr pbge(expr_vector const& es, int const* coeffs, int bound) {
1644  assert(es.size() > 0);
1645  context& ctx = es[0].ctx();
1646  array<Z3_ast> _es(es);
1647  Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
1648  ctx.check_error();
1649  return expr(ctx, r);
1650  }
1651  inline expr pbeq(expr_vector const& es, int const* coeffs, int bound) {
1652  assert(es.size() > 0);
1653  context& ctx = es[0].ctx();
1654  array<Z3_ast> _es(es);
1655  Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
1656  ctx.check_error();
1657  return expr(ctx, r);
1658  }
1659  inline expr atmost(expr_vector const& es, unsigned bound) {
1660  assert(es.size() > 0);
1661  context& ctx = es[0].ctx();
1662  array<Z3_ast> _es(es);
1663  Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
1664  ctx.check_error();
1665  return expr(ctx, r);
1666  }
1667  inline expr atleast(expr_vector const& es, unsigned bound) {
1668  assert(es.size() > 0);
1669  context& ctx = es[0].ctx();
1670  array<Z3_ast> _es(es);
1671  Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
1672  ctx.check_error();
1673  return expr(ctx, r);
1674  }
1675  inline expr sum(expr_vector const& args) {
1676  assert(args.size() > 0);
1677  context& ctx = args[0].ctx();
1678  array<Z3_ast> _args(args);
1679  Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
1680  ctx.check_error();
1681  return expr(ctx, r);
1682  }
1683 
1684  inline expr distinct(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_distinct(ctx, _args.size(), _args.ptr());
1689  ctx.check_error();
1690  return expr(ctx, r);
1691  }
1692 
1693  inline expr concat(expr const& a, expr const& b) {
1694  check_context(a, b);
1695  Z3_ast r;
1696  if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
1697  Z3_ast _args[2] = { a, b };
1698  r = Z3_mk_seq_concat(a.ctx(), 2, _args);
1699  }
1700  else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
1701  Z3_ast _args[2] = { a, b };
1702  r = Z3_mk_re_concat(a.ctx(), 2, _args);
1703  }
1704  else {
1705  r = Z3_mk_concat(a.ctx(), a, b);
1706  }
1707  a.ctx().check_error();
1708  return expr(a.ctx(), r);
1709  }
1710 
1711  inline expr concat(expr_vector const& args) {
1712  Z3_ast r;
1713  assert(args.size() > 0);
1714  if (args.size() == 1) {
1715  return args[0];
1716  }
1717  context& ctx = args[0].ctx();
1718  array<Z3_ast> _args(args);
1719  if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
1720  r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
1721  }
1722  else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
1723  r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
1724  }
1725  else {
1726  r = _args[args.size()-1];
1727  for (unsigned i = args.size()-1; i > 0; ) {
1728  --i;
1729  r = Z3_mk_concat(ctx, _args[i], r);
1730  ctx.check_error();
1731  }
1732  }
1733  ctx.check_error();
1734  return expr(ctx, r);
1735  }
1736 
1737  inline expr mk_or(expr_vector const& args) {
1738  array<Z3_ast> _args(args);
1739  Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
1740  args.check_error();
1741  return expr(args.ctx(), r);
1742  }
1743  inline expr mk_and(expr_vector const& args) {
1744  array<Z3_ast> _args(args);
1745  Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
1746  args.check_error();
1747  return expr(args.ctx(), r);
1748  }
1749 
1750 
1751  class func_entry : public object {
1752  Z3_func_entry m_entry;
1753  void init(Z3_func_entry e) {
1754  m_entry = e;
1755  Z3_func_entry_inc_ref(ctx(), m_entry);
1756  }
1757  public:
1758  func_entry(context & c, Z3_func_entry e):object(c) { init(e); }
1759  func_entry(func_entry const & s):object(s) { init(s.m_entry); }
1761  operator Z3_func_entry() const { return m_entry; }
1763  Z3_func_entry_inc_ref(s.ctx(), s.m_entry);
1764  Z3_func_entry_dec_ref(ctx(), m_entry);
1765  m_ctx = s.m_ctx;
1766  m_entry = s.m_entry;
1767  return *this;
1768  }
1769  expr value() const { Z3_ast r = Z3_func_entry_get_value(ctx(), m_entry); check_error(); return expr(ctx(), r); }
1770  unsigned num_args() const { unsigned r = Z3_func_entry_get_num_args(ctx(), m_entry); check_error(); return r; }
1771  expr arg(unsigned i) const { Z3_ast r = Z3_func_entry_get_arg(ctx(), m_entry, i); check_error(); return expr(ctx(), r); }
1772  };
1773 
1774  class func_interp : public object {
1775  Z3_func_interp m_interp;
1776  void init(Z3_func_interp e) {
1777  m_interp = e;
1778  Z3_func_interp_inc_ref(ctx(), m_interp);
1779  }
1780  public:
1781  func_interp(context & c, Z3_func_interp e):object(c) { init(e); }
1782  func_interp(func_interp const & s):object(s) { init(s.m_interp); }
1784  operator Z3_func_interp() const { return m_interp; }
1786  Z3_func_interp_inc_ref(s.ctx(), s.m_interp);
1787  Z3_func_interp_dec_ref(ctx(), m_interp);
1788  m_ctx = s.m_ctx;
1789  m_interp = s.m_interp;
1790  return *this;
1791  }
1792  expr else_value() const { Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), r); }
1793  unsigned num_entries() const { unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }
1794  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); }
1795  void add_entry(expr_vector const& args, expr& value) {
1796  Z3_func_interp_add_entry(ctx(), m_interp, args, value);
1797  check_error();
1798  }
1799  void set_else(expr& value) {
1800  Z3_func_interp_set_else(ctx(), m_interp, value);
1801  check_error();
1802  }
1803  };
1804 
1805  class model : public object {
1806  Z3_model m_model;
1807  void init(Z3_model m) {
1808  m_model = m;
1809  Z3_model_inc_ref(ctx(), m);
1810  }
1811  public:
1812  model(context & c):object(c) { init(Z3_mk_model(c)); }
1813  model(context & c, Z3_model m):object(c) { init(m); }
1814  model(model const & s):object(s) { init(s.m_model); }
1815  ~model() { Z3_model_dec_ref(ctx(), m_model); }
1816  operator Z3_model() const { return m_model; }
1817  model & operator=(model const & s) {
1818  Z3_model_inc_ref(s.ctx(), s.m_model);
1819  Z3_model_dec_ref(ctx(), m_model);
1820  m_ctx = s.m_ctx;
1821  m_model = s.m_model;
1822  return *this;
1823  }
1824 
1825  expr eval(expr const & n, bool model_completion=false) const {
1826  check_context(*this, n);
1827  Z3_ast r = 0;
1828  Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
1829  check_error();
1830  if (status == Z3_FALSE && ctx().enable_exceptions())
1831  Z3_THROW(exception("failed to evaluate expression"));
1832  return expr(ctx(), r);
1833  }
1834 
1835  unsigned num_consts() const { return Z3_model_get_num_consts(ctx(), m_model); }
1836  unsigned num_funcs() const { return Z3_model_get_num_funcs(ctx(), m_model); }
1837  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); }
1838  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); }
1839  unsigned size() const { return num_consts() + num_funcs(); }
1840  func_decl operator[](int i) const {
1841  assert(0 <= i);
1842  return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
1843  }
1844 
1845  // returns interpretation of constant declaration c.
1846  // If c is not assigned any value in the model it returns
1847  // an expression with a null ast reference.
1849  check_context(*this, c);
1850  Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);
1851  check_error();
1852  return expr(ctx(), r);
1853  }
1855  check_context(*this, f);
1856  Z3_func_interp r = Z3_model_get_func_interp(ctx(), m_model, f);
1857  check_error();
1858  return func_interp(ctx(), r);
1859  }
1860 
1861  // returns true iff the model contains an interpretation
1862  // for function f.
1863  bool has_interp(func_decl f) const {
1864  check_context(*this, f);
1865  return 0 != Z3_model_has_interp(ctx(), m_model, f);
1866  }
1867 
1869  Z3_func_interp r = Z3_add_func_interp(ctx(), m_model, f, else_val);
1870  check_error();
1871  return func_interp(ctx(), r);
1872  }
1873 
1874  void add_const_interp(func_decl& f, expr& value) {
1875  Z3_add_const_interp(ctx(), m_model, f, value);
1876  check_error();
1877  }
1878 
1879  friend std::ostream & operator<<(std::ostream & out, model const & m);
1880  };
1881  inline std::ostream & operator<<(std::ostream & out, model const & m) { out << Z3_model_to_string(m.ctx(), m); return out; }
1882 
1883  class stats : public object {
1884  Z3_stats m_stats;
1885  void init(Z3_stats e) {
1886  m_stats = e;
1887  Z3_stats_inc_ref(ctx(), m_stats);
1888  }
1889  public:
1890  stats(context & c):object(c), m_stats(0) {}
1891  stats(context & c, Z3_stats e):object(c) { init(e); }
1892  stats(stats const & s):object(s) { init(s.m_stats); }
1893  ~stats() { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); }
1894  operator Z3_stats() const { return m_stats; }
1895  stats & operator=(stats const & s) {
1896  Z3_stats_inc_ref(s.ctx(), s.m_stats);
1897  if (m_stats) Z3_stats_dec_ref(ctx(), m_stats);
1898  m_ctx = s.m_ctx;
1899  m_stats = s.m_stats;
1900  return *this;
1901  }
1902  unsigned size() const { return Z3_stats_size(ctx(), m_stats); }
1903  std::string key(unsigned i) const { Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; }
1904  bool is_uint(unsigned i) const { Z3_bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r != 0; }
1905  bool is_double(unsigned i) const { Z3_bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r != 0; }
1906  unsigned uint_value(unsigned i) const { unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; }
1907  double double_value(unsigned i) const { double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
1908  friend std::ostream & operator<<(std::ostream & out, stats const & s);
1909  };
1910  inline std::ostream & operator<<(std::ostream & out, stats const & s) { out << Z3_stats_to_string(s.ctx(), s); return out; }
1911 
1912 
1913  inline std::ostream & operator<<(std::ostream & out, check_result r) {
1914  if (r == unsat) out << "unsat";
1915  else if (r == sat) out << "sat";
1916  else out << "unknown";
1917  return out;
1918  }
1919 
1920 
1921  class solver : public object {
1922  Z3_solver m_solver;
1923  void init(Z3_solver s) {
1924  m_solver = s;
1925  Z3_solver_inc_ref(ctx(), s);
1926  }
1927  public:
1928  struct simple {};
1929  struct translate {};
1930  solver(context & c):object(c) { init(Z3_mk_solver(c)); }
1932  solver(context & c, Z3_solver s):object(c) { init(s); }
1933  solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); }
1934  solver(context & c, solver const& src, translate): object(c) { init(Z3_solver_translate(src.ctx(), src, c)); }
1935  solver(solver const & s):object(s) { init(s.m_solver); }
1936  ~solver() { Z3_solver_dec_ref(ctx(), m_solver); }
1937  operator Z3_solver() const { return m_solver; }
1938  solver & operator=(solver const & s) {
1939  Z3_solver_inc_ref(s.ctx(), s.m_solver);
1940  Z3_solver_dec_ref(ctx(), m_solver);
1941  m_ctx = s.m_ctx;
1942  m_solver = s.m_solver;
1943  return *this;
1944  }
1945  void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
1946  void set(char const * k, bool v) { params p(ctx()); p.set(k, v); set(p); }
1947  void set(char const * k, unsigned v) { params p(ctx()); p.set(k, v); set(p); }
1948  void set(char const * k, double v) { params p(ctx()); p.set(k, v); set(p); }
1949  void set(char const * k, symbol const & v) { params p(ctx()); p.set(k, v); set(p); }
1950  void set(char const * k, char const* v) { params p(ctx()); p.set(k, v); set(p); }
1951  void push() { Z3_solver_push(ctx(), m_solver); check_error(); }
1952  void pop(unsigned n = 1) { Z3_solver_pop(ctx(), m_solver, n); check_error(); }
1953  void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); }
1954  void add(expr const & e) { assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); }
1955  void add(expr const & e, expr const & p) {
1956  assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
1957  Z3_solver_assert_and_track(ctx(), m_solver, e, p);
1958  check_error();
1959  }
1960  void add(expr const & e, char const * p) {
1961  add(e, ctx().bool_const(p));
1962  }
1963  // fails for some compilers:
1964  // void add(expr_vector const& v) { check_context(*this, v); for (expr e : v) add(e); }
1965  void from_file(char const* file) { Z3_solver_from_file(ctx(), m_solver, file); ctx().check_parser_error(); }
1966  void from_string(char const* s) { Z3_solver_from_string(ctx(), m_solver, s); ctx().check_parser_error(); }
1967 
1969  check_result check(unsigned n, expr * const assumptions) {
1970  array<Z3_ast> _assumptions(n);
1971  for (unsigned i = 0; i < n; i++) {
1972  check_context(*this, assumptions[i]);
1973  _assumptions[i] = assumptions[i];
1974  }
1975  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
1976  check_error();
1977  return to_check_result(r);
1978  }
1980  unsigned n = assumptions.size();
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  model get_model() const { Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }
1992  Z3_lbool r = Z3_solver_get_consequences(ctx(), m_solver, assumptions, vars, conseq);
1993  check_error();
1994  return to_check_result(r);
1995  }
1996  std::string reason_unknown() const { Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }
1997  stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }
1998  expr_vector unsat_core() const { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
1999  expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2000  expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
2001  friend std::ostream & operator<<(std::ostream & out, solver const & s);
2002 
2003  std::string to_smt2(char const* status = "unknown") {
2004  array<Z3_ast> es(assertions());
2005  Z3_ast const* fmls = es.ptr();
2006  Z3_ast fml = 0;
2007  unsigned sz = es.size();
2008  if (sz > 0) {
2009  --sz;
2010  fml = fmls[sz];
2011  }
2012  else {
2013  fml = ctx().bool_val(true);
2014  }
2015  return std::string(Z3_benchmark_to_smtlib_string(
2016  ctx(),
2017  "", "", status, "",
2018  sz,
2019  fmls,
2020  fml));
2021  }
2022 
2024 
2025  };
2026  inline std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
2027 
2028  class goal : public object {
2029  Z3_goal m_goal;
2030  void init(Z3_goal s) {
2031  m_goal = s;
2032  Z3_goal_inc_ref(ctx(), s);
2033  }
2034  public:
2035  goal(context & c, bool models=true, bool unsat_cores=false, bool proofs=false):object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); }
2036  goal(context & c, Z3_goal s):object(c) { init(s); }
2037  goal(goal const & s):object(s) { init(s.m_goal); }
2038  ~goal() { Z3_goal_dec_ref(ctx(), m_goal); }
2039  operator Z3_goal() const { return m_goal; }
2040  goal & operator=(goal const & s) {
2041  Z3_goal_inc_ref(s.ctx(), s.m_goal);
2042  Z3_goal_dec_ref(ctx(), m_goal);
2043  m_ctx = s.m_ctx;
2044  m_goal = s.m_goal;
2045  return *this;
2046  }
2047  void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
2048  // fails for some compilers:
2049  // void add(expr_vector const& v) { check_context(*this, v); for (expr e : v) add(e); }
2050  unsigned size() const { return Z3_goal_size(ctx(), m_goal); }
2051  expr operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
2052  Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); }
2053  bool inconsistent() const { return Z3_goal_inconsistent(ctx(), m_goal) != 0; }
2054  unsigned depth() const { return Z3_goal_depth(ctx(), m_goal); }
2055  void reset() { Z3_goal_reset(ctx(), m_goal); }
2056  unsigned num_exprs() const { return Z3_goal_num_exprs(ctx(), m_goal); }
2057  bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal) != 0; }
2058  bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal) != 0; }
2059  expr as_expr() const {
2060  unsigned n = size();
2061  if (n == 0)
2062  return ctx().bool_val(true);
2063  else if (n == 1)
2064  return operator[](0);
2065  else {
2066  array<Z3_ast> args(n);
2067  for (unsigned i = 0; i < n; i++)
2068  args[i] = operator[](i);
2069  return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
2070  }
2071  }
2072  friend std::ostream & operator<<(std::ostream & out, goal const & g);
2073  };
2074  inline std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; }
2075 
2076  class apply_result : public object {
2077  Z3_apply_result m_apply_result;
2078  void init(Z3_apply_result s) {
2079  m_apply_result = s;
2081  }
2082  public:
2083  apply_result(context & c, Z3_apply_result s):object(c) { init(s); }
2084  apply_result(apply_result const & s):object(s) { init(s.m_apply_result); }
2085  ~apply_result() { Z3_apply_result_dec_ref(ctx(), m_apply_result); }
2086  operator Z3_apply_result() const { return m_apply_result; }
2088  Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result);
2089  Z3_apply_result_dec_ref(ctx(), m_apply_result);
2090  m_ctx = s.m_ctx;
2091  m_apply_result = s.m_apply_result;
2092  return *this;
2093  }
2094  unsigned size() const { return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }
2095  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); }
2096  model convert_model(model const & m, unsigned i = 0) const {
2097  check_context(*this, m);
2098  Z3_model new_m = Z3_apply_result_convert_model(ctx(), m_apply_result, i, m);
2099  check_error();
2100  return model(ctx(), new_m);
2101  }
2102  friend std::ostream & operator<<(std::ostream & out, apply_result const & r);
2103  };
2104  inline std::ostream & operator<<(std::ostream & out, apply_result const & r) { out << Z3_apply_result_to_string(r.ctx(), r); return out; }
2105 
2106  class tactic : public object {
2107  Z3_tactic m_tactic;
2108  void init(Z3_tactic s) {
2109  m_tactic = s;
2110  Z3_tactic_inc_ref(ctx(), s);
2111  }
2112  public:
2113  tactic(context & c, char const * name):object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); }
2114  tactic(context & c, Z3_tactic s):object(c) { init(s); }
2115  tactic(tactic const & s):object(s) { init(s.m_tactic); }
2116  ~tactic() { Z3_tactic_dec_ref(ctx(), m_tactic); }
2117  operator Z3_tactic() const { return m_tactic; }
2118  tactic & operator=(tactic const & s) {
2119  Z3_tactic_inc_ref(s.ctx(), s.m_tactic);
2120  Z3_tactic_dec_ref(ctx(), m_tactic);
2121  m_ctx = s.m_ctx;
2122  m_tactic = s.m_tactic;
2123  return *this;
2124  }
2125  solver mk_solver() const { Z3_solver r = Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error(); return solver(ctx(), r); }
2126  apply_result apply(goal const & g) const {
2127  check_context(*this, g);
2128  Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g);
2129  check_error();
2130  return apply_result(ctx(), r);
2131  }
2132  apply_result operator()(goal const & g) const {
2133  return apply(g);
2134  }
2135  std::string help() const { char const * r = Z3_tactic_get_help(ctx(), m_tactic); check_error(); return r; }
2136  friend tactic operator&(tactic const & t1, tactic const & t2);
2137  friend tactic operator|(tactic const & t1, tactic const & t2);
2138  friend tactic repeat(tactic const & t, unsigned max);
2139  friend tactic with(tactic const & t, params const & p);
2140  friend tactic try_for(tactic const & t, unsigned ms);
2141  friend tactic par_or(unsigned n, tactic const* tactics);
2142  friend tactic par_and_then(tactic const& t1, tactic const& t2);
2144  };
2145 
2146  inline tactic operator&(tactic const & t1, tactic const & t2) {
2147  check_context(t1, t2);
2148  Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
2149  t1.check_error();
2150  return tactic(t1.ctx(), r);
2151  }
2152 
2153  inline tactic operator|(tactic const & t1, tactic const & t2) {
2154  check_context(t1, t2);
2155  Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
2156  t1.check_error();
2157  return tactic(t1.ctx(), r);
2158  }
2159 
2160  inline tactic repeat(tactic const & t, unsigned max=UINT_MAX) {
2161  Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
2162  t.check_error();
2163  return tactic(t.ctx(), r);
2164  }
2165 
2166  inline tactic with(tactic const & t, params const & p) {
2167  Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
2168  t.check_error();
2169  return tactic(t.ctx(), r);
2170  }
2171  inline tactic try_for(tactic const & t, unsigned ms) {
2172  Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
2173  t.check_error();
2174  return tactic(t.ctx(), r);
2175  }
2176  inline tactic par_or(unsigned n, tactic const* tactics) {
2177  if (n == 0) {
2178  Z3_THROW(exception("a non-zero number of tactics need to be passed to par_or"));
2179  }
2180  array<Z3_tactic> buffer(n);
2181  for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
2182  return tactic(tactics[0].ctx(), Z3_tactic_par_or(tactics[0].ctx(), n, buffer.ptr()));
2183  }
2184 
2185  inline tactic par_and_then(tactic const & t1, tactic const & t2) {
2186  check_context(t1, t2);
2187  Z3_tactic r = Z3_tactic_par_and_then(t1.ctx(), t1, t2);
2188  t1.check_error();
2189  return tactic(t1.ctx(), r);
2190  }
2191 
2192  class probe : public object {
2193  Z3_probe m_probe;
2194  void init(Z3_probe s) {
2195  m_probe = s;
2196  Z3_probe_inc_ref(ctx(), s);
2197  }
2198  public:
2199  probe(context & c, char const * name):object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); }
2200  probe(context & c, double val):object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); }
2201  probe(context & c, Z3_probe s):object(c) { init(s); }
2202  probe(probe const & s):object(s) { init(s.m_probe); }
2203  ~probe() { Z3_probe_dec_ref(ctx(), m_probe); }
2204  operator Z3_probe() const { return m_probe; }
2205  probe & operator=(probe const & s) {
2206  Z3_probe_inc_ref(s.ctx(), s.m_probe);
2207  Z3_probe_dec_ref(ctx(), m_probe);
2208  m_ctx = s.m_ctx;
2209  m_probe = s.m_probe;
2210  return *this;
2211  }
2212  double apply(goal const & g) const { double r = Z3_probe_apply(ctx(), m_probe, g); check_error(); return r; }
2213  double operator()(goal const & g) const { return apply(g); }
2214  friend probe operator<=(probe const & p1, probe const & p2);
2215  friend probe operator<=(probe const & p1, double p2);
2216  friend probe operator<=(double p1, probe const & p2);
2217  friend probe operator>=(probe const & p1, probe const & p2);
2218  friend probe operator>=(probe const & p1, double p2);
2219  friend probe operator>=(double p1, probe const & p2);
2220  friend probe operator<(probe const & p1, probe const & p2);
2221  friend probe operator<(probe const & p1, double p2);
2222  friend probe operator<(double p1, probe const & p2);
2223  friend probe operator>(probe const & p1, probe const & p2);
2224  friend probe operator>(probe const & p1, double p2);
2225  friend probe operator>(double p1, probe const & p2);
2226  friend probe operator==(probe const & p1, probe const & p2);
2227  friend probe operator==(probe const & p1, double p2);
2228  friend probe operator==(double p1, probe const & p2);
2229  friend probe operator&&(probe const & p1, probe const & p2);
2230  friend probe operator||(probe const & p1, probe const & p2);
2231  friend probe operator!(probe const & p);
2232  };
2233 
2234  inline probe operator<=(probe const & p1, probe const & p2) {
2235  check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2236  }
2237  inline probe operator<=(probe const & p1, double p2) { return p1 <= probe(p1.ctx(), p2); }
2238  inline probe operator<=(double p1, probe const & p2) { return probe(p2.ctx(), p1) <= p2; }
2239  inline probe operator>=(probe const & p1, probe const & p2) {
2240  check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2241  }
2242  inline probe operator>=(probe const & p1, double p2) { return p1 >= probe(p1.ctx(), p2); }
2243  inline probe operator>=(double p1, probe const & p2) { return probe(p2.ctx(), p1) >= p2; }
2244  inline probe operator<(probe const & p1, probe const & p2) {
2245  check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2246  }
2247  inline probe operator<(probe const & p1, double p2) { return p1 < probe(p1.ctx(), p2); }
2248  inline probe operator<(double p1, probe const & p2) { return probe(p2.ctx(), p1) < p2; }
2249  inline probe operator>(probe const & p1, probe const & p2) {
2250  check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2251  }
2252  inline probe operator>(probe const & p1, double p2) { return p1 > probe(p1.ctx(), p2); }
2253  inline probe operator>(double p1, probe const & p2) { return probe(p2.ctx(), p1) > p2; }
2254  inline probe operator==(probe const & p1, probe const & p2) {
2255  check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2256  }
2257  inline probe operator==(probe const & p1, double p2) { return p1 == probe(p1.ctx(), p2); }
2258  inline probe operator==(double p1, probe const & p2) { return probe(p2.ctx(), p1) == p2; }
2259  inline probe operator&&(probe const & p1, probe const & p2) {
2260  check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2261  }
2262  inline probe operator||(probe const & p1, probe const & p2) {
2263  check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2264  }
2265  inline probe operator!(probe const & p) {
2266  Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
2267  }
2268 
2269  class optimize : public object {
2270  Z3_optimize m_opt;
2271  public:
2272  class handle {
2273  unsigned m_h;
2274  public:
2275  handle(unsigned h): m_h(h) {}
2276  unsigned h() const { return m_h; }
2277  };
2278  optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }
2280  operator Z3_optimize() const { return m_opt; }
2281  void add(expr const& e) {
2282  assert(e.is_bool());
2283  Z3_optimize_assert(ctx(), m_opt, e);
2284  }
2285  handle add(expr const& e, unsigned weight) {
2286  assert(e.is_bool());
2287  std::stringstream strm;
2288  strm << weight;
2289  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, strm.str().c_str(), 0));
2290  }
2291  handle add(expr const& e, char const* weight) {
2292  assert(e.is_bool());
2293  return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0));
2294  }
2295  handle maximize(expr const& e) {
2296  return handle(Z3_optimize_maximize(ctx(), m_opt, e));
2297  }
2298  handle minimize(expr const& e) {
2299  return handle(Z3_optimize_minimize(ctx(), m_opt, e));
2300  }
2301  void push() {
2302  Z3_optimize_push(ctx(), m_opt);
2303  }
2304  void pop() {
2305  Z3_optimize_pop(ctx(), m_opt);
2306  }
2308  model get_model() const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }
2309  void set(params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }
2310  expr lower(handle const& h) {
2311  Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());
2312  check_error();
2313  return expr(ctx(), r);
2314  }
2315  expr upper(handle const& h) {
2316  Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h());
2317  check_error();
2318  return expr(ctx(), r);
2319  }
2320  expr_vector assertions() const { Z3_ast_vector r = Z3_optimize_get_assertions(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
2321  expr_vector objectives() const { Z3_ast_vector r = Z3_optimize_get_objectives(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
2322  stats statistics() const { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); }
2323  friend std::ostream & operator<<(std::ostream & out, optimize const & s);
2324  void from_file(char const* filename) { Z3_optimize_from_file(ctx(), m_opt, filename); check_error(); }
2325  void from_string(char const* constraints) { Z3_optimize_from_string(ctx(), m_opt, constraints); check_error(); }
2326  std::string help() const { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error(); return r; }
2327  };
2328  inline std::ostream & operator<<(std::ostream & out, optimize const & s) { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }
2329 
2330  class fixedpoint : public object {
2331  Z3_fixedpoint m_fp;
2332  public:
2335  operator Z3_fixedpoint() const { return m_fp; }
2336  void from_string(char const* s) { Z3_fixedpoint_from_string(ctx(), m_fp, s); check_error(); }
2337  void from_file(char const* s) { Z3_fixedpoint_from_file(ctx(), m_fp, s); check_error(); }
2338  void add_rule(expr& rule, symbol const& name) { Z3_fixedpoint_add_rule(ctx(), m_fp, rule, name); check_error(); }
2339  void add_fact(func_decl& f, unsigned * args) { Z3_fixedpoint_add_fact(ctx(), m_fp, f, f.arity(), args); check_error(); }
2342  array<Z3_func_decl> rs(relations);
2343  Z3_lbool r = Z3_fixedpoint_query_relations(ctx(), m_fp, rs.size(), rs.ptr());
2344  check_error();
2345  return to_check_result(r);
2346  }
2347  expr get_answer() { Z3_ast r = Z3_fixedpoint_get_answer(ctx(), m_fp); check_error(); return expr(ctx(), r); }
2348  std::string reason_unknown() { return Z3_fixedpoint_get_reason_unknown(ctx(), m_fp); }
2349  void update_rule(expr& rule, symbol const& name) { Z3_fixedpoint_update_rule(ctx(), m_fp, rule, name); check_error(); }
2350  unsigned get_num_levels(func_decl& p) { unsigned r = Z3_fixedpoint_get_num_levels(ctx(), m_fp, p); check_error(); return r; }
2351  expr get_cover_delta(int level, func_decl& p) {
2352  Z3_ast r = Z3_fixedpoint_get_cover_delta(ctx(), m_fp, level, p);
2353  check_error();
2354  return expr(ctx(), r);
2355  }
2356  void add_cover(int level, func_decl& p, expr& property) { Z3_fixedpoint_add_cover(ctx(), m_fp, level, p, property); check_error(); }
2357  stats statistics() const { Z3_stats r = Z3_fixedpoint_get_statistics(ctx(), m_fp); check_error(); return stats(ctx(), r); }
2359  expr_vector assertions() const { Z3_ast_vector r = Z3_fixedpoint_get_assertions(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
2360  expr_vector rules() const { Z3_ast_vector r = Z3_fixedpoint_get_rules(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
2361  void set(params const & p) { Z3_fixedpoint_set_params(ctx(), m_fp, p); check_error(); }
2362  std::string help() const { return Z3_fixedpoint_get_help(ctx(), m_fp); }
2364  std::string to_string() { return Z3_fixedpoint_to_string(ctx(), m_fp, 0, 0); }
2365  std::string to_string(expr_vector const& queries) {
2366  array<Z3_ast> qs(queries);
2367  return Z3_fixedpoint_to_string(ctx(), m_fp, qs.size(), qs.ptr());
2368  }
2369  void push() { Z3_fixedpoint_push(ctx(), m_fp); check_error(); }
2370  void pop() { Z3_fixedpoint_pop(ctx(), m_fp); check_error(); }
2371  };
2372  inline std::ostream & operator<<(std::ostream & out, fixedpoint const & f) { return out << Z3_fixedpoint_to_string(f.ctx(), f, 0, 0); }
2373 
2374  inline tactic fail_if(probe const & p) {
2375  Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
2376  p.check_error();
2377  return tactic(p.ctx(), r);
2378  }
2379  inline tactic when(probe const & p, tactic const & t) {
2380  check_context(p, t);
2381  Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
2382  t.check_error();
2383  return tactic(t.ctx(), r);
2384  }
2385  inline tactic cond(probe const & p, tactic const & t1, tactic const & t2) {
2386  check_context(p, t1); check_context(p, t2);
2387  Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
2388  t1.check_error();
2389  return tactic(t1.ctx(), r);
2390  }
2391 
2392  inline symbol context::str_symbol(char const * s) { Z3_symbol r = Z3_mk_string_symbol(m_ctx, s); check_error(); return symbol(*this, r); }
2393  inline symbol context::int_symbol(int n) { Z3_symbol r = Z3_mk_int_symbol(m_ctx, n); check_error(); return symbol(*this, r); }
2394 
2395  inline sort context::bool_sort() { Z3_sort s = Z3_mk_bool_sort(m_ctx); check_error(); return sort(*this, s); }
2396  inline sort context::int_sort() { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }
2397  inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
2398  inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
2399  inline sort context::string_sort() { Z3_sort s = Z3_mk_string_sort(m_ctx); check_error(); return sort(*this, s); }
2400  inline sort context::seq_sort(sort& s) { Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); }
2401  inline sort context::re_sort(sort& s) { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
2402 
2403  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); }
2405  array<Z3_sort> dom(d);
2406  Z3_sort s = Z3_mk_array_sort_n(m_ctx, dom.size(), dom.ptr(), r); check_error(); return sort(*this, s);
2407  }
2408 
2409  inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
2410  array<Z3_symbol> _enum_names(n);
2411  for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
2412  array<Z3_func_decl> _cs(n);
2413  array<Z3_func_decl> _ts(n);
2414  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2415  sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
2416  check_error();
2417  for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
2418  return s;
2419  }
2420  inline sort context::uninterpreted_sort(char const* name) {
2421  Z3_symbol _name = Z3_mk_string_symbol(*this, name);
2422  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
2423  }
2425  return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
2426  }
2427 
2428  inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
2429  array<Z3_sort> args(arity);
2430  for (unsigned i = 0; i < arity; i++) {
2431  check_context(domain[i], range);
2432  args[i] = domain[i];
2433  }
2434  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
2435  check_error();
2436  return func_decl(*this, f);
2437  }
2438 
2439  inline func_decl context::function(char const * name, unsigned arity, sort const * domain, sort const & range) {
2440  return function(range.ctx().str_symbol(name), arity, domain, range);
2441  }
2442 
2443  inline func_decl context::function(symbol const& name, sort_vector const& domain, sort const& range) {
2444  array<Z3_sort> args(domain.size());
2445  for (unsigned i = 0; i < domain.size(); i++) {
2446  check_context(domain[i], range);
2447  args[i] = domain[i];
2448  }
2449  Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
2450  check_error();
2451  return func_decl(*this, f);
2452  }
2453 
2454  inline func_decl context::function(char const * name, sort_vector const& domain, sort const& range) {
2455  return function(range.ctx().str_symbol(name), domain, range);
2456  }
2457 
2458 
2459  inline func_decl context::function(char const * name, sort const & domain, sort const & range) {
2460  check_context(domain, range);
2461  Z3_sort args[1] = { domain };
2462  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
2463  check_error();
2464  return func_decl(*this, f);
2465  }
2466 
2467  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & range) {
2469  Z3_sort args[2] = { d1, d2 };
2470  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
2471  check_error();
2472  return func_decl(*this, f);
2473  }
2474 
2475  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
2477  Z3_sort args[3] = { d1, d2, d3 };
2478  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
2479  check_error();
2480  return func_decl(*this, f);
2481  }
2482 
2483  inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
2485  Z3_sort args[4] = { d1, d2, d3, d4 };
2486  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
2487  check_error();
2488  return func_decl(*this, f);
2489  }
2490 
2491  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) {
2493  Z3_sort args[5] = { d1, d2, d3, d4, d5 };
2494  Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
2495  check_error();
2496  return func_decl(*this, f);
2497  }
2498 
2499  inline expr context::constant(symbol const & name, sort const & s) {
2500  Z3_ast r = Z3_mk_const(m_ctx, name, s);
2501  check_error();
2502  return expr(*this, r);
2503  }
2504  inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); }
2505  inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); }
2506  inline expr context::int_const(char const * name) { return constant(name, int_sort()); }
2507  inline expr context::real_const(char const * name) { return constant(name, real_sort()); }
2508  inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); }
2509 
2510  inline expr context::bool_val(bool b) { return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }
2511 
2512  inline expr context::int_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
2513  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); }
2514  inline expr context::int_val(__int64 n) { Z3_ast r = Z3_mk_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
2515  inline expr context::int_val(__uint64 n) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
2516  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); }
2517 
2518  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); }
2519  inline expr context::real_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
2520  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); }
2521  inline expr context::real_val(__int64 n) { Z3_ast r = Z3_mk_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
2522  inline expr context::real_val(__uint64 n) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
2523  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); }
2524 
2525  inline expr context::bv_val(int n, unsigned sz) { Z3_ast r = Z3_mk_int(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
2526  inline expr context::bv_val(unsigned n, unsigned sz) { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
2527  inline expr context::bv_val(__int64 n, unsigned sz) { Z3_ast r = Z3_mk_int64(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
2528  inline expr context::bv_val(__uint64 n, unsigned sz) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
2529  inline expr context::bv_val(char const * n, unsigned sz) { Z3_ast r = Z3_mk_numeral(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
2530  inline expr context::bv_val(unsigned n, bool const* bits) {
2531  array<Z3_bool> _bits(n);
2532  for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
2533  Z3_ast r = Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error(); return expr(*this, r);
2534  }
2535 
2536  inline expr context::string_val(char const* s) { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
2537  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); }
2538 
2539  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); }
2540 
2541  inline expr func_decl::operator()(unsigned n, expr const * args) const {
2542  array<Z3_ast> _args(n);
2543  for (unsigned i = 0; i < n; i++) {
2544  check_context(*this, args[i]);
2545  _args[i] = args[i];
2546  }
2547  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
2548  check_error();
2549  return expr(ctx(), r);
2550 
2551  }
2552  inline expr func_decl::operator()(expr_vector const& args) const {
2553  array<Z3_ast> _args(args.size());
2554  for (unsigned i = 0; i < args.size(); i++) {
2555  check_context(*this, args[i]);
2556  _args[i] = args[i];
2557  }
2558  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
2559  check_error();
2560  return expr(ctx(), r);
2561  }
2562  inline expr func_decl::operator()() const {
2563  Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
2564  ctx().check_error();
2565  return expr(ctx(), r);
2566  }
2567  inline expr func_decl::operator()(expr const & a) const {
2568  check_context(*this, a);
2569  Z3_ast args[1] = { a };
2570  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
2571  ctx().check_error();
2572  return expr(ctx(), r);
2573  }
2574  inline expr func_decl::operator()(int a) const {
2575  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
2576  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
2577  ctx().check_error();
2578  return expr(ctx(), r);
2579  }
2580  inline expr func_decl::operator()(expr const & a1, expr const & a2) const {
2581  check_context(*this, a1); check_context(*this, a2);
2582  Z3_ast args[2] = { a1, a2 };
2583  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
2584  ctx().check_error();
2585  return expr(ctx(), r);
2586  }
2587  inline expr func_decl::operator()(expr const & a1, int a2) const {
2588  check_context(*this, a1);
2589  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
2590  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
2591  ctx().check_error();
2592  return expr(ctx(), r);
2593  }
2594  inline expr func_decl::operator()(int a1, expr const & a2) const {
2595  check_context(*this, a2);
2596  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
2597  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
2598  ctx().check_error();
2599  return expr(ctx(), r);
2600  }
2601  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3) const {
2602  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
2603  Z3_ast args[3] = { a1, a2, a3 };
2604  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
2605  ctx().check_error();
2606  return expr(ctx(), r);
2607  }
2608  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const {
2609  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
2610  Z3_ast args[4] = { a1, a2, a3, a4 };
2611  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
2612  ctx().check_error();
2613  return expr(ctx(), r);
2614  }
2615  inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const {
2616  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
2617  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
2618  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
2619  ctx().check_error();
2620  return expr(ctx(), r);
2621  }
2622 
2623  inline expr to_real(expr const & a) { Z3_ast r = Z3_mk_int2real(a.ctx(), a); a.check_error(); return expr(a.ctx(), r); }
2624 
2625  inline func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
2626  return range.ctx().function(name, arity, domain, range);
2627  }
2628  inline func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range) {
2629  return range.ctx().function(name, arity, domain, range);
2630  }
2631  inline func_decl function(char const * name, sort const & domain, sort const & range) {
2632  return range.ctx().function(name, domain, range);
2633  }
2634  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range) {
2635  return range.ctx().function(name, d1, d2, range);
2636  }
2637  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
2638  return range.ctx().function(name, d1, d2, d3, range);
2639  }
2640  inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
2641  return range.ctx().function(name, d1, d2, d3, d4, range);
2642  }
2643  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) {
2644  return range.ctx().function(name, d1, d2, d3, d4, d5, range);
2645  }
2646 
2647  inline expr select(expr const & a, expr const & i) {
2648  check_context(a, i);
2649  Z3_ast r = Z3_mk_select(a.ctx(), a, i);
2650  a.check_error();
2651  return expr(a.ctx(), r);
2652  }
2653  inline expr select(expr const & a, int i) { return select(a, a.ctx().num_val(i, a.get_sort().array_domain())); }
2654  inline expr store(expr const & a, expr const & i, expr const & v) {
2655  check_context(a, i); check_context(a, v);
2656  Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
2657  a.check_error();
2658  return expr(a.ctx(), r);
2659  }
2660  inline expr select(expr const & a, expr_vector const & i) {
2661  check_context(a, i);
2662  array<Z3_ast> idxs(i);
2663  Z3_ast r = Z3_mk_select_n(a.ctx(), a, idxs.size(), idxs.ptr());
2664  a.check_error();
2665  return expr(a.ctx(), r);
2666  }
2667 
2668  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); }
2669  inline expr store(expr const & a, expr i, int v) { return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
2670  inline expr store(expr const & a, int i, int v) {
2671  return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
2672  }
2673  inline expr store(expr const & a, expr_vector const & i, expr const & v) {
2674  check_context(a, i); check_context(a, v);
2675  array<Z3_ast> idxs(i);
2676  Z3_ast r = Z3_mk_store_n(a.ctx(), a, idxs.size(), idxs.ptr(), v);
2677  a.check_error();
2678  return expr(a.ctx(), r);
2679  }
2680 
2681  inline expr as_array(func_decl & f) {
2682  Z3_ast r = Z3_mk_as_array(f.ctx(), f);
2683  f.check_error();
2684  return expr(f.ctx(), r);
2685  }
2686 
2687 #define MK_EXPR1(_fn, _arg) \
2688  Z3_ast r = _fn(_arg.ctx(), _arg); \
2689  _arg.check_error(); \
2690  return expr(_arg.ctx(), r);
2691 
2692 #define MK_EXPR2(_fn, _arg1, _arg2) \
2693  check_context(_arg1, _arg2); \
2694  Z3_ast r = _fn(_arg1.ctx(), _arg1, _arg2); \
2695  _arg1.check_error(); \
2696  return expr(_arg1.ctx(), r);
2697 
2698  inline expr const_array(sort const & d, expr const & v) {
2699  MK_EXPR2(Z3_mk_const_array, d, v);
2700  }
2701 
2702  inline expr empty_set(sort const& s) {
2704  }
2705 
2706  inline expr full_set(sort const& s) {
2708  }
2709 
2710  inline expr set_add(expr const& s, expr const& e) {
2711  MK_EXPR2(Z3_mk_set_add, s, e);
2712  }
2713 
2714  inline expr set_del(expr const& s, expr const& e) {
2715  MK_EXPR2(Z3_mk_set_del, s, e);
2716  }
2717 
2718  inline expr set_union(expr const& a, expr const& b) {
2719  check_context(a, b);
2720  Z3_ast es[2] = { a, b };
2721  Z3_ast r = Z3_mk_set_union(a.ctx(), 2, es);
2722  a.check_error();
2723  return expr(a.ctx(), r);
2724  }
2725 
2726  inline expr set_intersect(expr const& a, expr const& b) {
2727  check_context(a, b);
2728  Z3_ast es[2] = { a, b };
2729  Z3_ast r = Z3_mk_set_intersect(a.ctx(), 2, es);
2730  a.check_error();
2731  return expr(a.ctx(), r);
2732  }
2733 
2734  inline expr set_difference(expr const& a, expr const& b) {
2736  }
2737 
2738  inline expr set_complement(expr const& a) {
2740  }
2741 
2742  inline expr set_member(expr const& s, expr const& e) {
2743  MK_EXPR2(Z3_mk_set_member, s, e);
2744  }
2745 
2746  inline expr set_subset(expr const& a, expr const& b) {
2747  MK_EXPR2(Z3_mk_set_subset, a, b);
2748  }
2749 
2750  // sequence and regular expression operations.
2751  // union is +
2752  // concat is overloaded to handle sequences and regular expressions
2753 
2754  inline expr empty(sort const& s) {
2755  Z3_ast r = Z3_mk_seq_empty(s.ctx(), s);
2756  s.check_error();
2757  return expr(s.ctx(), r);
2758  }
2759  inline expr suffixof(expr const& a, expr const& b) {
2760  check_context(a, b);
2761  Z3_ast r = Z3_mk_seq_suffix(a.ctx(), a, b);
2762  a.check_error();
2763  return expr(a.ctx(), r);
2764  }
2765  inline expr prefixof(expr const& a, expr const& b) {
2766  check_context(a, b);
2767  Z3_ast r = Z3_mk_seq_prefix(a.ctx(), a, b);
2768  a.check_error();
2769  return expr(a.ctx(), r);
2770  }
2771  inline expr indexof(expr const& s, expr const& substr, expr const& offset) {
2772  check_context(s, substr); check_context(s, offset);
2773  Z3_ast r = Z3_mk_seq_index(s.ctx(), s, substr, offset);
2774  s.check_error();
2775  return expr(s.ctx(), r);
2776  }
2777  inline expr to_re(expr const& s) {
2779  }
2780  inline expr in_re(expr const& s, expr const& re) {
2781  MK_EXPR2(Z3_mk_seq_in_re, s, re);
2782  }
2783  inline expr plus(expr const& re) {
2784  MK_EXPR1(Z3_mk_re_plus, re);
2785  }
2786  inline expr option(expr const& re) {
2788  }
2789  inline expr star(expr const& re) {
2790  MK_EXPR1(Z3_mk_re_star, re);
2791  }
2792  inline expr re_empty(sort const& s) {
2793  Z3_ast r = Z3_mk_re_empty(s.ctx(), s);
2794  s.check_error();
2795  return expr(s.ctx(), r);
2796  }
2797  inline expr re_full(sort const& s) {
2798  Z3_ast r = Z3_mk_re_full(s.ctx(), s);
2799  s.check_error();
2800  return expr(s.ctx(), r);
2801  }
2802  inline expr re_intersect(expr_vector const& args) {
2803  assert(args.size() > 0);
2804  context& ctx = args[0].ctx();
2805  array<Z3_ast> _args(args);
2806  Z3_ast r = Z3_mk_re_intersect(ctx, _args.size(), _args.ptr());
2807  ctx.check_error();
2808  return expr(ctx, r);
2809  }
2810  inline expr re_complement(expr const& a) {
2812  }
2813  inline expr range(expr const& lo, expr const& hi) {
2814  check_context(lo, hi);
2815  Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
2816  lo.check_error();
2817  return expr(lo.ctx(), r);
2818  }
2819 
2820 
2821 
2822 
2823 
2824  inline expr interpolant(expr const& a) {
2825  return expr(a.ctx(), Z3_mk_interpolant(a.ctx(), a));
2826  }
2827 
2828  inline expr context::parse_string(char const* s) {
2829  Z3_ast r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0);
2831  return expr(*this, r);
2832  }
2833  inline expr context::parse_file(char const* s) {
2834  Z3_ast r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0);
2836  return expr(*this, r);
2837  }
2838 
2839  inline expr context::parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls) {
2840  array<Z3_symbol> sort_names(sorts.size());
2841  array<Z3_symbol> decl_names(decls.size());
2842  array<Z3_sort> sorts1(sorts);
2843  array<Z3_func_decl> decls1(decls);
2844  for (unsigned i = 0; i < sorts.size(); ++i) {
2845  sort_names[i] = sorts[i].name();
2846  }
2847  for (unsigned i = 0; i < decls.size(); ++i) {
2848  decl_names[i] = decls[i].name();
2849  }
2850  Z3_ast r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
2852  return expr(*this, r);
2853  }
2854 
2855  inline expr context::parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls) {
2856  array<Z3_symbol> sort_names(sorts.size());
2857  array<Z3_symbol> decl_names(decls.size());
2858  array<Z3_sort> sorts1(sorts);
2859  array<Z3_func_decl> decls1(decls);
2860  for (unsigned i = 0; i < sorts.size(); ++i) {
2861  sort_names[i] = sorts[i].name();
2862  }
2863  for (unsigned i = 0; i < decls.size(); ++i) {
2864  decl_names[i] = decls[i].name();
2865  }
2866  Z3_ast r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
2868  return expr(*this, r);
2869  }
2870 
2871 
2873  Z3_ast_vector interp = 0;
2874  Z3_model mdl = 0;
2875  Z3_lbool r = Z3_compute_interpolant(*this, pat, p, &interp, &mdl);
2876  switch (r) {
2877  case Z3_L_FALSE:
2878  i = expr_vector(*this, interp);
2879  break;
2880  case Z3_L_TRUE:
2881  m = model(*this, mdl);
2882  break;
2883  case Z3_L_UNDEF:
2884  break;
2885  }
2886  return to_check_result(r);
2887  }
2888 
2889  inline expr_vector context::get_interpolant(expr const& proof, expr const& pat, params const& p) {
2890  return expr_vector(*this, Z3_get_interpolant(*this, proof, pat, p));
2891  }
2892 
2893  inline expr expr::substitute(expr_vector const& src, expr_vector const& dst) {
2894  assert(src.size() == dst.size());
2895  array<Z3_ast> _src(src.size());
2896  array<Z3_ast> _dst(dst.size());
2897  for (unsigned i = 0; i < src.size(); ++i) {
2898  _src[i] = src[i];
2899  _dst[i] = dst[i];
2900  }
2901  Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
2902  check_error();
2903  return expr(ctx(), r);
2904  }
2905 
2906  inline expr expr::substitute(expr_vector const& dst) {
2907  array<Z3_ast> _dst(dst.size());
2908  for (unsigned i = 0; i < dst.size(); ++i) {
2909  _dst[i] = dst[i];
2910  }
2911  Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
2912  check_error();
2913  return expr(ctx(), r);
2914  }
2915 
2916 
2917 
2918 }
2919 
2922 #undef Z3_THROW
2923 #endif
2924 
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:1520
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:1684
bool is_uint(unsigned i) const
Definition: z3++.h:1904
expr mod(expr const &a, expr const &b)
Definition: z3++.h:1094
friend expr mk_or(expr_vector const &args)
Definition: z3++.h:1737
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:2322
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 repated between lo and hi time...
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:154
expr parse_string(char const *s)
parsing
Definition: z3++.h:2828
Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)
Create a bit-vector type of the given size.
friend expr operator|(expr const &a, expr const &b)
Definition: z3++.h:1348
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:2395
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.
friend expr atmost(expr_vector const &es, unsigned bound)
Definition: z3++.h:1659
expr get_const_interp(func_decl c) const
Definition: z3++.h:1848
friend expr operator+(expr const &a, expr const &b)
Definition: z3++.h:1160
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:1874
expr mk_and(expr_vector const &args)
Definition: z3++.h:1743
friend expr pw(expr const &a, expr const &b)
Definition: z3++.h:1090
bool is_decided_unsat() const
Definition: z3++.h:2058
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:1812
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:1565
tactic & operator=(tactic const &s)
Definition: z3++.h:2118
bool is_bool() const
Return true if this sort is the Boolean sort.
Definition: z3++.h:494
sort re_sort(sort &seq_sort)
Return a regular expression sort over sequences seq_sort.
Definition: z3++.h:2401
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:633
void add_fact(func_decl &f, unsigned *args)
Definition: z3++.h:2339
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:2201
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:807
expr pbeq(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:1651
friend expr xnor(expr const &a, expr const &b)
Definition: z3++.h:1354
unsigned uint_value(unsigned i) const
Definition: z3++.h:1906
probe & operator=(probe const &s)
Definition: z3++.h:2205
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:1794
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:2350
double double_value(unsigned i) const
Definition: z3++.h:1907
std::string documentation(symbol const &s)
Definition: z3++.h:410
stats statistics() const
Definition: z3++.h:1997
Z3_error_code check_error() const
Definition: z3++.h:365
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:2326
void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t)
Increment the reference counter of the given tactic.
friend expr operator>=(expr const &a, expr const &b)
Definition: z3++.h:1208
#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:2308
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:2392
unsigned size() const
Definition: z3++.h:2050
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:1474
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.
friend probe operator &&(probe const &p1, probe const &p2)
Definition: z3++.h:2259
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:2051
Z3_tactic Z3_API Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1...
friend bool eq(ast const &a, ast const &b)
Return true if the ASTs are structurally identical.
Definition: z3++.h:467
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:1951
expr contains(expr const &s)
Definition: z3++.h:1010
func_decl get_const_decl(unsigned i) const
Definition: z3++.h:1837
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:2385
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:995
solver(context &c, simple)
Definition: z3++.h:1931
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:596
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:2813
expr bv_val(int n, unsigned sz)
Definition: z3++.h:2525
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:1150
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:1345
func_interp & operator=(func_interp const &s)
Definition: z3++.h:1785
friend expr operator!=(expr const &a, expr const &b)
Definition: z3++.h:1150
iterator & operator++()
Definition: z3++.h:1561
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:1838
probe(context &c, double val)
Definition: z3++.h:2200
expr select(expr const &a, expr const &i)
Definition: z3++.h:2647
Definition: z3++.h:127
expr operator &(expr const &a, expr const &b)
Definition: z3++.h:1340
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:1762
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:2379
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:1799
config()
Definition: z3++.h:105
friend std::ostream & operator<<(std::ostream &out, params const &p)
Definition: z3++.h:437
bool is_algebraic() const
Return true if expression is an algebraic number.
Definition: z3++.h:688
unsigned get_numeral_uint() const
Return uint value of numeral, throw if result cannot fit in machine uint.
Definition: z3++.h:735
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:2310
friend expr operator/(expr const &a, expr const &b)
Definition: z3++.h:1225
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.
Z3_ast Z3_API Z3_mk_int64(Z3_context c, __int64 v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
array(unsigned sz)
Definition: z3++.h:347
std::ostream & operator<<(std::ostream &out, exception const &e)
Definition: z3++.h:87
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:986
A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort.
Definition: z3++.h:473
~solver()
Definition: z3++.h:1936
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:548
char const * msg() const
Definition: z3++.h:84
T operator[](int i) const
Definition: z3++.h:1526
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
__uint64 get_numeral_uint64() const
Return __uint64 value of numeral, throw if result cannot fit in __uint64.
Definition: z3++.h:769
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:563
void push()
Definition: z3++.h:2369
friend expr operator^(expr const &a, expr const &b)
Definition: z3++.h:1344
~array()
Definition: z3++.h:350
void pop_back()
Definition: z3++.h:1530
expr full_set(sort const &s)
Definition: z3++.h:2706
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:554
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s)
Convert string to integer.
friend std::ostream & operator<<(std::ostream &out, ast const &n)
Definition: z3++.h:463
Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem)
Remove an element to a set.
T const & operator[](int i) const
Definition: z3++.h:353
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.
Z3_func_decl Z3_API Z3_model_get_const_decl(Z3_context c, Z3_model m, unsigned i)
Return the i-th constant in the given model.
sort bv_sort(unsigned sz)
Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz.
Definition: z3++.h:2398
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 actualy stop.
Definition: z3++.h:218
expr lshr(expr const &a, expr const &b)
logic shift right operator for bitvectors
Definition: z3++.h:1460
expr as_expr() const
Definition: z3++.h:2059
expr udiv(expr const &a, expr const &b)
unsigned division operator for bitvectors.
Definition: z3++.h:1425
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
friend expr concat(expr const &a, expr const &b)
Definition: z3++.h:1693
friend expr mod(expr const &a, expr const &b)
Definition: z3++.h:1094
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:2135
bool is_bv() const
Return true if this is a Bit-vector expression.
Definition: z3++.h:625
expr upper(handle const &h)
Definition: z3++.h:2315
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1380
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1343
goal(context &c, Z3_goal s)
Definition: z3++.h:2036
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:411
expr_vector assertions() const
Definition: z3++.h:2320
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:1813
sort array_sort(sort d, sort r)
Return an array sort for arrays from d to r.
Definition: z3++.h:2403
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:2499
void pop()
Definition: z3++.h:2304
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.
int Z3_bool
Z3 Boolean type. It is just an alias for int.
Definition: z3_api.h:85
double operator()(goal const &g) const
Definition: z3++.h:2213
bool is_real() const
Return true if this is a real expression.
Definition: z3++.h:617
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:2340
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:1104
fixedpoint(context &c)
Definition: z3++.h:2333
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:518
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:2115
friend expr operator||(expr const &a, expr const &b)
Return an expression representing a or b.
Definition: z3++.h:1128
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:2203
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:379
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:1840
expr rotate_right(unsigned i)
Definition: z3++.h:982
~tactic()
Definition: z3++.h:2116
bool is_array() const
Return true if this is a Array expression.
Definition: z3++.h:629
sort operator()(context &c, Z3_ast a)
Definition: z3++.h:1501
check_result check()
Definition: z3++.h:2307
Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[])
Create the intersection of the regular languages.
friend probe operator||(probe const &p1, probe const &p2)
Definition: z3++.h:2262
expr is_int(expr const &e)
Definition: z3++.h:1112
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:1344
friend std::ostream & operator<<(std::ostream &out, optimize const &s)
Definition: z3++.h:2328
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:701
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:2325
Exception used to sign API usage errors.
Definition: z3++.h:80
expr operator*(expr const &a, expr const &b)
Definition: z3++.h:1187
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:1032
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:1521
A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort ...
Definition: z3++.h:594
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:498
expr operator!(expr const &a)
Definition: z3++.h:1110
bool operator==(iterator const &other)
Definition: z3++.h:1555
expr set_subset(expr const &a, expr const &b)
Definition: z3++.h:2746
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:2692
#define __uint64
Definition: z3_api.h:44
expr & operator=(expr const &n)
Definition: z3++.h:599
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:1401
expr in_re(expr const &s, expr const &re)
Definition: z3++.h:2780
symbol name(unsigned i)
Definition: z3++.h:408
std::string key(unsigned i) const
Definition: z3++.h:1903
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:1061
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:405
friend expr mk_and(expr_vector const &args)
Definition: z3++.h:1743
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:570
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:2349
expr parse_file(char const *file)
Definition: z3++.h:2833
func_decl operator()(context &c, Z3_ast a)
Definition: z3++.h:1509
std::string to_string(expr_vector const &queries)
Definition: z3++.h:2365
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:1890
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:1208
std::string reason_unknown()
Definition: z3++.h:2348
void add_entry(expr_vector const &args, expr &value)
Definition: z3++.h:1795
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:645
expr pw(expr const &a, expr const &b)
Definition: z3++.h:1090
bool empty() const
Definition: z3++.h:1531
Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)
Return the declaration of a constant or function application.
friend std::ostream & operator<<(std::ostream &out, goal const &g)
Definition: z3++.h:2074
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...
context(config &c, interpolation)
Definition: z3++.h:163
friend probe operator>=(probe const &p1, probe const &p2)
Definition: z3++.h:2239
expr(context &c, Z3_ast n)
Definition: z3++.h:597
~goal()
Definition: z3++.h:2038
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:2734
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:2359
expr operator~(expr const &a)
Definition: z3++.h:1356
unsigned num_entries() const
Definition: z3++.h:1793
void Z3_API Z3_fixedpoint_pop(Z3_context c, Z3_fixedpoint d)
Backtrack one backtracking point.
def tactics(ctx=None)
Definition: z3py.py:7417
friend expr operator-(expr const &a)
Definition: z3++.h:1244
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a string.
Z3_error_code Z3_API Z3_get_error_code(Z3_context c)
Return the error code for the last API call.
friend expr distinct(expr_vector const &args)
Definition: z3++.h:1684
check_result check(unsigned n, expr *const assumptions)
Definition: z3++.h:1969
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:1979
expr rem(expr const &a, expr const &b)
Definition: z3++.h:1098
friend expr operator*(expr const &a, expr const &b)
Definition: z3++.h:1187
probe(context &c, char const *name)
Definition: z3++.h:2199
friend std::ostream & operator<<(std::ostream &out, solver const &s)
Definition: z3++.h:2026
Z3_symbol_kind kind() const
Definition: z3++.h:377
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:2347
Z3_sort Z3_API Z3_mk_string_sort(Z3_context c)
Create a sort for 8 bit strings.
~stats()
Definition: z3++.h:1893
Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, __uint64 v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
sort seq_sort(sort &s)
Return a sequence sort over base sort s.
Definition: z3++.h:2400
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.
friend expr operator<=(expr const &a, expr const &b)
Definition: z3++.h:1280
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:1022
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:441
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:792
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:571
expr set_add(expr const &s, expr const &e)
Definition: z3++.h:2710
expr ashr(expr const &a, expr const &b)
arithmetic shift right operator for bitvectors
Definition: z3++.h:1467
expr re_empty(sort const &s)
Definition: z3++.h:2792
unsigned size() const
Definition: z3++.h:1902
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).
friend tactic operator|(tactic const &t1, tactic const &t2)
Definition: z3++.h:2153
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed division.
expr nor(expr const &a, expr const &b)
Definition: z3++.h:1353
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:1932
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:573
bool is_re() const
Return true if this sort is a regular expression sort.
Definition: z3++.h:530
solver & operator=(solver const &s)
Definition: z3++.h:1938
expr operator &&(expr const &a, expr const &b)
Definition: z3++.h:1116
void add_cover(int level, func_decl &p, expr &property)
Definition: z3++.h:2356
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:2893
iterator begin() const
Definition: z3++.h:1569
ast(context &c, Z3_ast n)
Definition: z3++.h:446
ast_vector_tpl & operator=(ast_vector_tpl const &s)
Definition: z3++.h:1532
expr operator<=(expr const &a, expr const &b)
Definition: z3++.h:1280
handle add(expr const &e, char const *weight)
Definition: z3++.h:2291
friend std::ostream & operator<<(std::ostream &out, apply_result const &r)
Definition: z3++.h:2104
Z3_goal_prec precision() const
Definition: z3++.h:2052
expr bv_const(char const *name, unsigned sz)
Definition: z3++.h:2508
context & ctx() const
Definition: z3++.h:364
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:486
T back() const
Definition: z3++.h:1529
expr string_val(char const *s)
Definition: z3++.h:2536
tactic(context &c, char const *name)
Definition: z3++.h:2113
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:2399
tactic with(tactic const &t, params const &p)
Definition: z3++.h:2166
expr empty_set(sort const &s)
Definition: z3++.h:2702
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:2681
expr plus(expr const &re)
Definition: z3++.h:2783
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:1354
__int64 get_numeral_int64() const
Return __int64 value of numeral, throw if result cannot fit in __int64.
Definition: z3++.h:752
void reset()
Definition: z3++.h:1953
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:1570
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:506
void from_string(char const *s)
Definition: z3++.h:1966
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:522
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:184
unsigned Z3_API Z3_goal_depth(Z3_context c, Z3_goal g)
Return the depth of the given goal. It tracks how many transformations were applied to it...
void Z3_API Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r)
Increment the reference counter of the given Z3_apply_result object.
friend expr atleast(expr_vector const &es, unsigned bound)
Definition: z3++.h:1667
bool is_real() const
Return true if this sort is the Real sort.
Definition: z3++.h:502
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:1552
func_entry(context &c, Z3_func_entry e)
Definition: z3++.h:1758
void resize(unsigned sz)
Definition: z3++.h:1528
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:829
expr operator()() const
Definition: z3++.h:2562
void add(expr const &e, char const *p)
Definition: z3++.h:1960
func_decl to_func_decl(context &c, Z3_func_decl f)
Definition: z3++.h:1393
unsigned hash() const
Definition: z3++.h:453
optimize(context &c)
Definition: z3++.h:2278
goal operator[](int i) const
Definition: z3++.h:2095
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:396
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:672
expr(expr const &n)
Definition: z3++.h:598
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:1751
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:1968
expr_vector objectives() const
Definition: z3++.h:2321
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:2003
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:1160
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2428
expr operator()(context &c, Z3_ast a)
Definition: z3++.h:1490
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:2362
friend probe operator!(probe const &p)
Definition: z3++.h:2265
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:621
bool is_well_sorted() const
Return true if this expression is well sorted (aka type correct).
Definition: z3++.h:693
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...
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:378
expr re_complement(expr const &a)
Definition: z3++.h:2810
expr srem(expr const &a, expr const &b)
signed remainder operator for bitvectors
Definition: z3++.h:1432
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:2726
void from_string(char const *s)
Definition: z3++.h:2336
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:2053
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:1935
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:106
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:2279
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:1016
#define __int64
Definition: z3_api.h:40
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:2802
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:2518
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:609
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:2281
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:2765
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:1782
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:1817
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:780
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:2185
unsigned Z3_API Z3_param_descrs_size(Z3_context c, Z3_param_descrs p)
Return the number of parameters in the given parameter description set.
friend expr operator==(expr const &a, expr const &b)
Definition: z3++.h:1141
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:1042
expr interpolant(expr const &a)
Definition: z3++.h:2824
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:1954
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:983
expr ugt(expr const &a, expr const &b)
unsigned greater than operator for bitvectors.
Definition: z3++.h:1419
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:2040
expr option(expr const &re)
Definition: z3++.h:2786
~params()
Definition: z3++.h:421
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:2698
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:1892
std::string to_string() const
Definition: z3++.h:455
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:2742
Z3_model Z3_API Z3_mk_model(Z3_context c)
Create a fresh model object. It has reference count 0.
friend std::ostream & operator<<(std::ostream &out, model const &m)
Definition: z3++.h:1881
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 a 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.
bool is_numeral_i64(__int64 &i) const
Definition: z3++.h:663
~func_entry()
Definition: z3++.h:1760
friend expr operator &(expr const &a, expr const &b)
Definition: z3++.h:1340
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:604
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)
Decrement the reference counter of the given optimize context.
sort uninterpreted_sort(char const *name)
create an uninterpreted sort with the name given by the string or symbol.
Definition: z3++.h:2420
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:1027
Z3_bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, __uint64 *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine __uint64 int...
void reset()
Definition: z3++.h:2055
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:355
params(params const &s)
Definition: z3++.h:420
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:2872
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:987
friend void check_context(object const &a, object const &b)
Definition: z3++.h:368
bool is_array() const
Return true if this sort is a Array sort.
Definition: z3++.h:514
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:2295
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:1302
friend probe operator<=(probe const &p1, probe const &p2)
Definition: z3++.h:2234
expr get_cover_delta(int level, func_decl &p)
Definition: z3++.h:2351
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:2506
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:999
symbol(symbol const &s)
Definition: z3++.h:374
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:1769
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:120
expr sum(expr_vector const &args)
Definition: z3++.h:1675
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:475
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:569
goal(context &c, bool models=true, bool unsat_cores=false, bool proofs=false)
Definition: z3++.h:2035
expr suffixof(expr const &a, expr const &b)
Definition: z3++.h:2759
void from_file(char const *filename)
Definition: z3++.h:2324
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:1991
expr operator<(expr const &a, expr const &b)
Definition: z3++.h:1302
unsigned num_exprs() const
Definition: z3++.h:2056
object(context &c)
Definition: z3++.h:362
friend expr operator>(expr const &a, expr const &b)
Definition: z3++.h:1321
handle add(expr const &e, unsigned weight)
Definition: z3++.h:2285
bool is_numeral(std::string &s, unsigned precision) const
Definition: z3++.h:668
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:445
object(object const &s)
Definition: z3++.h:363
friend expr nand(expr const &a, expr const &b)
Definition: z3++.h:1352
expr arg(unsigned i) const
Return the i-th argument of this application. This method assumes the expression is an application...
Definition: z3++.h:822
expr atleast(expr_vector const &es, unsigned bound)
Definition: z3++.h:1667
friend tactic with(tactic const &t, params const &p)
Definition: z3++.h:2166
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:2507
bool is_relation() const
Return true if this is a Relation expression.
Definition: z3++.h:637
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:676
friend probe operator==(probe const &p1, probe const &p2)
Definition: z3++.h:2254
unsigned h() const
Definition: z3++.h:2276
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:2094
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:2057
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:2096
Z3_bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a)
Return true if the give 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:1479
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.
void from_file(char const *file)
Definition: z3++.h:1965
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.
friend expr pbeq(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:1651
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:665
expr empty(sort const &s)
Definition: z3++.h:2754
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:375
~model()
Definition: z3++.h:1815
friend tactic par_and_then(tactic const &t1, tactic const &t2)
Definition: z3++.h:2185
expr_vector rules() const
Definition: z3++.h:2360
sort real_sort()
Return the Real sort.
Definition: z3++.h:2397
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:1571
expr re_full(sort const &s)
Definition: z3++.h:2797
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:1522
friend expr rem(expr const &a, expr const &b)
Definition: z3++.h:1098
expr num_val(int n, sort const &s)
Definition: z3++.h:2539
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:467
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:510
symbol int_symbol(int n)
Create a Z3 symbol based on the given integer.
Definition: z3++.h:2393
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:1047
expr else_value() const
Definition: z3++.h:1792
Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d)
Retrieve statistics information from the last call to Z3_optimize_check.
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
friend probe operator>(probe const &p1, probe const &p2)
Definition: z3++.h:2249
expr numerator() const
Definition: z3++.h:784
expr indexof(expr const &s, expr const &substr, expr const &offset)
Definition: z3++.h:2771
void from_file(char const *s)
Definition: z3++.h:2337
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:2738
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:397
expr unit() const
Definition: z3++.h:1005
expr operator>(expr const &a, expr const &b)
Definition: z3++.h:1321
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:1057
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:130
expr star(expr const &re)
Definition: z3++.h:2789
Z3_tactic Z3_API Z3_tactic_par_or(Z3_context c, unsigned num, Z3_tactic const ts[])
Return a tactic that applies the given tactics in parallel.
friend expr operator~(expr const &a)
Definition: z3++.h:1356
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:1141
symbol name() const
Return name of sort.
Definition: z3++.h:490
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:2687
param_descrs(context &c, Z3_param_descrs d)
Definition: z3++.h:395
void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value)
Set a configuration parameter.
friend tactic repeat(tactic const &t, unsigned max)
Definition: z3++.h:2160
expr operator|(expr const &a, expr const &b)
Definition: z3++.h:1348
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:988
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
unsigned num_args() const
Definition: z3++.h:1770
friend tactic par_or(unsigned n, tactic const *tactics)
Definition: z3++.h:2176
expr pbge(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:1643
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:2114
void check_context(object const &a, object const &b)
Definition: z3++.h:368
expr arg(unsigned i) const
Definition: z3++.h:1771
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:2505
expr urem(expr const &a, expr const &b)
unsigned reminder operator for bitvectors
Definition: z3++.h:1446
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:2125
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:1996
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:1990
bool operator!=(iterator const &other)
Definition: z3++.h:1558
friend expr ite(expr const &c, expr const &t, expr const &e)
Create the if-then-else expression ite(c, t, e)
Definition: z3++.h:1366
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:1835
friend expr nor(expr const &a, expr const &b)
Definition: z3++.h:1353
params & operator=(params const &s)
Definition: z3++.h:423
friend std::ostream & operator<<(std::ostream &out, symbol const &s)
Definition: z3++.h:383
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:1814
expr proof() const
Definition: z3++.h:2000
bool is_numeral_u(unsigned &i) const
Definition: z3++.h:666
check_result query(func_decl_vector &relations)
Definition: z3++.h:2341
bool is_numeral_u64(__uint64 &i) const
Definition: z3++.h:664
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:2202
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:1551
symbol name() const
Definition: z3++.h:572
friend expr operator<(expr const &a, expr const &b)
Definition: z3++.h:1302
friend expr operator!(expr const &a)
Return an expression representing not(a).
Definition: z3++.h:1110
solver(context &c, solver const &src, translate)
Definition: z3++.h:1934
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:1930
void Z3_API Z3_apply_result_dec_ref(Z3_context c, Z3_apply_result r)
Decrement the reference counter of the given Z3_apply_result object.
Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re)
Create an universal regular expression of sort re.
void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value)
add a function entry to a function interpretation.
friend expr sum(expr_vector const &args)
Definition: z3++.h:1675
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:564
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:354
handle minimize(expr const &e)
Definition: z3++.h:2298
apply_result apply(goal const &g) const
Definition: z3++.h:2126
friend probe operator<(probe const &p1, probe const &p2)
Definition: z3++.h:2244
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:1955
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:2654
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:1863
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
unsigned size() const
Definition: z3++.h:1839
apply_result operator()(goal const &g) const
Definition: z3++.h:2132
friend expr pble(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:1635
Z3_ast m_ast
Definition: z3++.h:443
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:430
unsigned size() const
Definition: z3++.h:1525
unsigned size() const
Definition: z3++.h:351
tactic repeat(tactic const &t, unsigned max=UINT_MAX)
Definition: z3++.h:2160
expr bool_val(bool b)
Definition: z3++.h:2510
~context()
Definition: z3++.h:164
expr operator||(expr const &a, expr const &b)
Definition: z3++.h:1128
expr ult(expr const &a, expr const &b)
unsigned less than operator for bitvectors.
Definition: z3++.h:1407
bool is_var() const
Return true if this expression is a variable.
Definition: z3++.h:684
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:1566
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:2889
unsigned depth() const
Definition: z3++.h:2054
Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables...
Z3_string Z3_API Z3_tactic_get_help(Z3_context c, Z3_tactic t)
Return a string containing a description of parameters accepted by the given tactic.
void Z3_API Z3_params_set_symbol(Z3_context c, Z3_params p, Z3_symbol k, Z3_symbol v)
Add a symbol parameter k with value v to the parameter set p.
friend expr pbge(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:1643
expr int_val(int n)
Definition: z3++.h:2512
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...
friend expr operator &&(expr const &a, expr const &b)
Return an expression representing a and b.
Definition: z3++.h:1116
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:565
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:1553
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:1737
tactic fail_if(probe const &p)
Definition: z3++.h:2374
Z3_param_kind kind(symbol const &s)
Definition: z3++.h:409
stats(context &c, Z3_stats e)
Definition: z3++.h:1891
expr exists(expr const &x, expr const &b)
Definition: z3++.h:1611
std::string to_string()
Definition: z3++.h:2364
ast operator()(context &c, Z3_ast a)
Definition: z3++.h:1485
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:680
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:1366
double apply(goal const &g) const
Definition: z3++.h:2212
func_entry(func_entry const &s)
Definition: z3++.h:1759
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:1825
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:448
#define Z3_FALSE
False value. It is just an alias for 0.
Definition: z3_api.h:101
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:1998
int get_numeral_int() const
Return int value of numeral, throw if result cannot fit in machine int.
Definition: z3++.h:716
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:451
func_interp add_func_interp(func_decl &f, expr &else_val)
Definition: z3++.h:1868
expr_vector assertions() const
Definition: z3++.h:1999
unsigned num_args() const
Return the number of arguments in this application. This method assumes the expression is an applicat...
Definition: z3++.h:814
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:541
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:452
expr forall(expr const &x, expr const &b)
Definition: z3++.h:1587
sort(context &c, Z3_sort s)
Definition: z3++.h:476
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:1082
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 intepretation. It represents the value of f in a particular po...
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1075
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:1379
expr rotate_left(unsigned i)
Definition: z3++.h:981
expr concat(expr const &a, expr const &b)
Definition: z3++.h:1693
symbol(context &c, Z3_symbol s)
Definition: z3++.h:373
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:2357
solver(context &c, char const *logic)
Definition: z3++.h:1933
tactic try_for(tactic const &t, unsigned ms)
Definition: z3++.h:2171
func_interp(context &c, Z3_func_interp e)
Definition: z3++.h:1781
void register_relation(func_decl &p)
Definition: z3++.h:2358
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:2338
expr shl(expr const &a, expr const &b)
shift left operator for bitvectors
Definition: z3++.h:1453
params(context &c)
Definition: z3++.h:419
Z3_ast Z3_API Z3_mk_rotate_left(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the left i times.
friend tactic try_for(tactic const &t, unsigned ms)
Definition: z3++.h:2171
void push_back(T const &e)
Definition: z3++.h:1527
expr pble(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:1635
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.
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:1413
void push()
Definition: z3++.h:2301
bool is_seq() const
Return true if this sort is a Sequence sort.
Definition: z3++.h:526
bool is_numeral(std::string &s) const
Definition: z3++.h:667
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:1905
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:482
Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort d)
Return the sort name as a symbol.
context * m_ctx
Definition: z3++.h:360
unsigned size()
Definition: z3++.h:407
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:655
expr operator-(expr const &a)
Definition: z3++.h:1244
func_interp get_func_interp(func_decl f) const
Definition: z3++.h:1854
void pop(unsigned n=1)
Definition: z3++.h:1952
friend std::ostream & operator<<(std::ostream &out, stats const &s)
Definition: z3++.h:1910
expr smod(expr const &a, expr const &b)
signed modulus operator for bitvectors
Definition: z3++.h:1439
expr to_real(expr const &a)
Definition: z3++.h:2623
handle(unsigned h)
Definition: z3++.h:2275
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.
friend expr implies(expr const &a, expr const &b)
Definition: z3++.h:1082
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:2023
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:662
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_...
Z3_bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, __int64 *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine __int64 int...
bool is_const() const
Definition: z3++.h:575
bool is_seq() const
Return true if this is a sequence expression.
Definition: z3++.h:641
ast(ast const &s)
Definition: z3++.h:447
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:2409
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:2176
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:477
bool is_finite_domain() const
Return true if this sort is a Finite domain sort.
Definition: z3++.h:534
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:2370
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:1002
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:2083
friend tactic operator &(tactic const &t1, tactic const &t2)
Definition: z3++.h:2146
expr nand(expr const &a, expr const &b)
Definition: z3++.h:1352
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:1225
Function declaration (aka function definition). It is the signature of interpreted and uninterpreted ...
Definition: z3++.h:561
expr set_union(expr const &a, expr const &b)
Definition: z3++.h:2718
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:352
param_descrs get_param_descrs()
Definition: z3++.h:2143
Z3_probe Z3_API Z3_probe_or(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when p1 or p2 evaluates to true.
goal(goal const &s)
Definition: z3++.h:2037
sort int_sort()
Return the integer sort.
Definition: z3++.h:2396
expr set_del(expr const &s, expr const &e)
Definition: z3++.h:2714
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:1895
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:567
apply_result & operator=(apply_result const &s)
Definition: z3++.h:2087
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:1659
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:1388
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:613
void add(expr const &f)
Definition: z3++.h:2047
friend expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
expr to_re(expr const &s)
Definition: z3++.h:2777
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:1836
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:2363
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition: z3_api.h:90
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:2084