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