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#pragma once
22
23#include<cassert>
24#include<iostream>
25#include<string>
26#include<sstream>
27#include<memory>
28#include<z3.h>
29#include<limits.h>
30#include<functional>
31
32#undef min
33#undef max
34
40
45
49namespace z3 {
50
51 class exception;
52 class config;
53 class context;
54 class symbol;
55 class params;
56 class param_descrs;
57 class ast;
58 class sort;
59 class func_decl;
60 class expr;
61 class solver;
62 class goal;
63 class tactic;
64 class probe;
65 class model;
66 class func_interp;
67 class func_entry;
68 class statistics;
69 class apply_result;
70 template<typename T> class cast_ast;
71 template<typename T> class ast_vector_tpl;
76
77 inline void set_param(char const * param, char const * value) { Z3_global_param_set(param, value); }
78 inline void set_param(char const * param, bool value) { Z3_global_param_set(param, value ? "true" : "false"); }
79 inline void set_param(char const * param, int value) { auto str = std::to_string(value); Z3_global_param_set(param, str.c_str()); }
81
85 class exception : public std::exception {
86 std::string m_msg;
87 public:
88 virtual ~exception() throw() {}
89 exception(char const * msg):m_msg(msg) {}
90 char const * msg() const { return m_msg.c_str(); }
91 char const * what() const throw() { return m_msg.c_str(); }
92 friend std::ostream & operator<<(std::ostream & out, exception const & e);
93 };
94 inline std::ostream & operator<<(std::ostream & out, exception const & e) { out << e.msg(); return out; }
95
96#if !defined(Z3_THROW)
97#if __cpp_exceptions || _CPPUNWIND || __EXCEPTIONS
98#define Z3_THROW(x) throw x
99#else
100#define Z3_THROW(x) {}
101#endif
102#endif // !defined(Z3_THROW)
103
107 class config {
108 Z3_config m_cfg;
109 config(config const &) = delete;
110 config & operator=(config const &) = delete;
111 public:
112 config() { m_cfg = Z3_mk_config(); }
113 ~config() { Z3_del_config(m_cfg); }
114 operator Z3_config() const { return m_cfg; }
118 void set(char const * param, char const * value) { Z3_set_param_value(m_cfg, param, value); }
122 void set(char const * param, bool value) { Z3_set_param_value(m_cfg, param, value ? "true" : "false"); }
126 void set(char const * param, int value) {
127 auto str = std::to_string(value);
128 Z3_set_param_value(m_cfg, param, str.c_str());
129 }
130 };
131
134 };
135
141 RTZ
142 };
143
145 if (l == Z3_L_TRUE) return sat;
146 else if (l == Z3_L_FALSE) return unsat;
147 return unknown;
148 }
149
150
156 class context {
157 private:
158 bool m_enable_exceptions;
159 rounding_mode m_rounding_mode;
160 Z3_context m_ctx;
161 void init(config & c) {
162 set_context(Z3_mk_context_rc(c));
163 }
164 void set_context(Z3_context ctx) {
165 m_ctx = ctx;
166 m_enable_exceptions = true;
167 m_rounding_mode = RNE;
168 Z3_set_error_handler(m_ctx, 0);
170 }
171
172
173 context(context const &) = delete;
174 context & operator=(context const &) = delete;
175
176 friend class scoped_context;
177 context(Z3_context c) { set_context(c); }
178 void detach() { m_ctx = nullptr; }
179 public:
180 context() { config c; init(c); }
181 context(config & c) { init(c); }
182 ~context() { if (m_ctx) Z3_del_context(m_ctx); }
183 operator Z3_context() const { return m_ctx; }
184
190 if (e != Z3_OK && enable_exceptions())
192 return e;
193 }
194
195 void check_parser_error() const {
196 check_error();
197 }
198
206 void set_enable_exceptions(bool f) { m_enable_exceptions = f; }
207
208 bool enable_exceptions() const { return m_enable_exceptions; }
209
213 void set(char const * param, char const * value) { Z3_update_param_value(m_ctx, param, value); }
217 void set(char const * param, bool value) { Z3_update_param_value(m_ctx, param, value ? "true" : "false"); }
221 void set(char const * param, int value) {
222 auto str = std::to_string(value);
223 Z3_update_param_value(m_ctx, param, str.c_str());
224 }
225
230 void interrupt() { Z3_interrupt(m_ctx); }
231
235 symbol str_symbol(char const * s);
239 symbol int_symbol(int n);
243 sort bool_sort();
247 sort int_sort();
251 sort real_sort();
255 sort bv_sort(unsigned sz);
263 sort seq_sort(sort& s);
273 sort array_sort(sort d, sort r);
274 sort array_sort(sort_vector const& d, sort r);
281 sort fpa_sort(unsigned ebits, unsigned sbits);
285 template<size_t precision>
300 sort enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts);
301
308 func_decl tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs);
309
313 sort uninterpreted_sort(char const* name);
314 sort uninterpreted_sort(symbol const& name);
315
316 func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range);
317 func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range);
318 func_decl function(symbol const& name, sort_vector const& domain, sort const& range);
319 func_decl function(char const * name, sort_vector const& domain, sort const& range);
320 func_decl function(char const * name, sort const & domain, sort const & range);
321 func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range);
322 func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range);
323 func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range);
324 func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range);
325
326 func_decl recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range);
327 func_decl recfun(char const * name, unsigned arity, sort const * domain, sort const & range);
328 func_decl recfun(char const * name, sort const & domain, sort const & range);
329 func_decl recfun(char const * name, sort const & d1, sort const & d2, sort const & range);
330
331 void recdef(func_decl, expr_vector const& args, expr const& body);
332
333 expr constant(symbol const & name, sort const & s);
334 expr constant(char const * name, sort const & s);
335 expr bool_const(char const * name);
336 expr int_const(char const * name);
337 expr real_const(char const * name);
338 expr string_const(char const * name);
339 expr bv_const(char const * name, unsigned sz);
340 expr fpa_const(char const * name, unsigned ebits, unsigned sbits);
341
342 template<size_t precision>
343 expr fpa_const(char const * name);
344
346
347 expr bool_val(bool b);
348
349 expr int_val(int n);
350 expr int_val(unsigned n);
351 expr int_val(int64_t n);
352 expr int_val(uint64_t n);
353 expr int_val(char const * n);
354
355 expr real_val(int n, int d);
356 expr real_val(int n);
357 expr real_val(unsigned n);
358 expr real_val(int64_t n);
359 expr real_val(uint64_t n);
360 expr real_val(char const * n);
361
362 expr bv_val(int n, unsigned sz);
363 expr bv_val(unsigned n, unsigned sz);
364 expr bv_val(int64_t n, unsigned sz);
365 expr bv_val(uint64_t n, unsigned sz);
366 expr bv_val(char const * n, unsigned sz);
367 expr bv_val(unsigned n, bool const* bits);
368
369 expr fpa_val(double n);
370 expr fpa_val(float n);
371 expr fpa_nan(sort const & s);
372 expr fpa_inf(sort const & s, bool sgn);
373
374 expr string_val(char const* s);
375 expr string_val(char const* s, unsigned n);
376 expr string_val(std::string const& s);
377
378 expr num_val(int n, sort const & s);
379
383 expr_vector parse_string(char const* s);
384 expr_vector parse_file(char const* file);
385
386 expr_vector parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
387 expr_vector parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
388 };
389
390 class scoped_context final {
391 context m_ctx;
392 public:
393 scoped_context(Z3_context c): m_ctx(c) {}
394 ~scoped_context() { m_ctx.detach(); }
395 context& operator()() { return m_ctx; }
396 };
397
398
399 template<typename T>
400 class array {
401 std::unique_ptr<T[]> m_array;
402 unsigned m_size;
403 array(array const &) = delete;
404 array & operator=(array const &) = delete;
405 public:
406 array(unsigned sz):m_array(new T[sz]),m_size(sz) {}
407 template<typename T2>
408 array(ast_vector_tpl<T2> const & v);
409 void resize(unsigned sz) { m_array.reset(new T[sz]); m_size = sz; }
410 unsigned size() const { return m_size; }
411 T & operator[](int i) { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
412 T const & operator[](int i) const { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size); return m_array[i]; }
413 T const * ptr() const { return m_array.get(); }
414 T * ptr() { return m_array.get(); }
415 };
416
417 class object {
418 protected:
420 public:
421 object(context & c):m_ctx(&c) {}
422 context & ctx() const { return *m_ctx; }
424 friend void check_context(object const & a, object const & b);
425 };
426 inline void check_context(object const & a, object const & b) { (void)a; (void)b; assert(a.m_ctx == b.m_ctx); }
427
428 class symbol : public object {
429 Z3_symbol m_sym;
430 public:
431 symbol(context & c, Z3_symbol s):object(c), m_sym(s) {}
432 operator Z3_symbol() const { return m_sym; }
433 Z3_symbol_kind kind() const { return Z3_get_symbol_kind(ctx(), m_sym); }
434 std::string str() const { assert(kind() == Z3_STRING_SYMBOL); return Z3_get_symbol_string(ctx(), m_sym); }
435 int to_int() const { assert(kind() == Z3_INT_SYMBOL); return Z3_get_symbol_int(ctx(), m_sym); }
436 friend std::ostream & operator<<(std::ostream & out, symbol const & s);
437 };
438
439 inline std::ostream & operator<<(std::ostream & out, symbol const & s) {
440 if (s.kind() == Z3_INT_SYMBOL)
441 out << "k!" << s.to_int();
442 else
443 out << s.str();
444 return out;
445 }
446
447
448 class param_descrs : public object {
449 Z3_param_descrs m_descrs;
450 public:
451 param_descrs(context& c, Z3_param_descrs d): object(c), m_descrs(d) { Z3_param_descrs_inc_ref(c, d); }
452 param_descrs(param_descrs const& o): object(o.ctx()), m_descrs(o.m_descrs) { Z3_param_descrs_inc_ref(ctx(), m_descrs); }
454 Z3_param_descrs_inc_ref(o.ctx(), o.m_descrs);
455 Z3_param_descrs_dec_ref(ctx(), m_descrs);
456 m_descrs = o.m_descrs;
457 object::operator=(o);
458 return *this;
459 }
462
463 unsigned size() { return Z3_param_descrs_size(ctx(), m_descrs); }
464 symbol name(unsigned i) { return symbol(ctx(), Z3_param_descrs_get_name(ctx(), m_descrs, i)); }
465 Z3_param_kind kind(symbol const& s) { return Z3_param_descrs_get_kind(ctx(), m_descrs, s); }
466 std::string documentation(symbol const& s) { char const* r = Z3_param_descrs_get_documentation(ctx(), m_descrs, s); check_error(); return r; }
467 std::string to_string() const { return Z3_param_descrs_to_string(ctx(), m_descrs); }
468 };
469
470 inline std::ostream& operator<<(std::ostream & out, param_descrs const & d) { return out << d.to_string(); }
471
472 class params : public object {
473 Z3_params m_params;
474 public:
475 params(context & c):object(c) { m_params = Z3_mk_params(c); Z3_params_inc_ref(ctx(), m_params); }
476 params(params const & s):object(s), m_params(s.m_params) { Z3_params_inc_ref(ctx(), m_params); }
477 ~params() { Z3_params_dec_ref(ctx(), m_params); }
478 operator Z3_params() const { return m_params; }
479 params & operator=(params const & s) {
480 Z3_params_inc_ref(s.ctx(), s.m_params);
481 Z3_params_dec_ref(ctx(), m_params);
482 object::operator=(s);
483 m_params = s.m_params;
484 return *this;
485 }
486 void set(char const * k, bool b) { Z3_params_set_bool(ctx(), m_params, ctx().str_symbol(k), b); }
487 void set(char const * k, unsigned n) { Z3_params_set_uint(ctx(), m_params, ctx().str_symbol(k), n); }
488 void set(char const * k, double n) { Z3_params_set_double(ctx(), m_params, ctx().str_symbol(k), n); }
489 void set(char const * k, symbol const & s) { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), s); }
490 void set(char const * k, char const* s) { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), ctx().str_symbol(s)); }
491 friend std::ostream & operator<<(std::ostream & out, params const & p);
492 };
493
494 inline std::ostream & operator<<(std::ostream & out, params const & p) {
495 out << Z3_params_to_string(p.ctx(), p); return out;
496 }
497
498 class ast : public object {
499 protected:
500 Z3_ast m_ast;
501 public:
502 ast(context & c):object(c), m_ast(0) {}
503 ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
504 ast(ast const & s):object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
505 ast(ast && s) noexcept : object(std::forward<object>(s)), m_ast(s.m_ast) { s.m_ast = nullptr; }
507 operator Z3_ast() const { return m_ast; }
508 operator bool() const { return m_ast != 0; }
509 ast & operator=(ast const & s) {
510 Z3_inc_ref(s.ctx(), s.m_ast);
511 if (m_ast)
512 Z3_dec_ref(ctx(), m_ast);
513 object::operator=(s);
514 m_ast = s.m_ast;
515 return *this;
516 }
517 ast & operator=(ast && s) noexcept {
518 if (this != &s) {
519 object::operator=(std::forward<object>(s));
520 m_ast = s.m_ast;
521 s.m_ast = nullptr;
522 }
523 return *this;
524 }
526 unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }
527 friend std::ostream & operator<<(std::ostream & out, ast const & n);
528 std::string to_string() const { return std::string(Z3_ast_to_string(ctx(), m_ast)); }
529
530
534 friend bool eq(ast const & a, ast const & b);
535 };
536 inline std::ostream & operator<<(std::ostream & out, ast const & n) {
537 out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
538 }
539
540 inline bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b); }
541
542 template<typename T>
543 class ast_vector_tpl : public object {
544 Z3_ast_vector m_vector;
545 void init(Z3_ast_vector v) { Z3_ast_vector_inc_ref(ctx(), v); m_vector = v; }
546 public:
548 ast_vector_tpl(context & c, Z3_ast_vector v):object(c) { init(v); }
549 ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
550 ast_vector_tpl(context& c, ast_vector_tpl const& src): object(c) { init(Z3_ast_vector_translate(src.ctx(), src, c)); }
551
553 operator Z3_ast_vector() const { return m_vector; }
554 unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); }
555 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); }
556 void push_back(T const & e) { Z3_ast_vector_push(ctx(), m_vector, e); check_error(); }
557 void resize(unsigned sz) { Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }
558 T back() const { return operator[](size() - 1); }
559 void pop_back() { assert(size() > 0); resize(size() - 1); }
560 bool empty() const { return size() == 0; }
562 Z3_ast_vector_inc_ref(s.ctx(), s.m_vector);
563 Z3_ast_vector_dec_ref(ctx(), m_vector);
564 object::operator=(s);
565 m_vector = s.m_vector;
566 return *this;
567 }
568 ast_vector_tpl& set(unsigned idx, ast& a) {
569 Z3_ast_vector_set(ctx(), m_vector, idx, a);
570 return *this;
571 }
572 /*
573 Disabled pending C++98 build upgrade
574 bool contains(T const& x) const {
575 for (T y : *this) if (eq(x, y)) return true;
576 return false;
577 }
578 */
579
580 class iterator final {
581 ast_vector_tpl const* m_vector;
582 unsigned m_index;
583 public:
584 iterator(ast_vector_tpl const* v, unsigned i): m_vector(v), m_index(i) {}
585
586 bool operator==(iterator const& other) const noexcept {
587 return other.m_index == m_index;
588 };
589 bool operator!=(iterator const& other) const noexcept {
590 return other.m_index != m_index;
591 };
592 iterator& operator++() noexcept {
593 ++m_index;
594 return *this;
595 }
596 void set(T& arg) {
597 Z3_ast_vector_set(m_vector->ctx(), *m_vector, m_index, arg);
598 }
599 iterator operator++(int) noexcept { iterator tmp = *this; ++m_index; return tmp; }
600 T * operator->() const { return &(operator*()); }
601 T operator*() const { return (*m_vector)[m_index]; }
602 };
603 iterator begin() const noexcept { return iterator(this, 0); }
604 iterator end() const { return iterator(this, size()); }
605 friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
606 };
607
608
612 class sort : public ast {
613 public:
614 sort(context & c):ast(c) {}
615 sort(context & c, Z3_sort s):ast(c, reinterpret_cast<Z3_ast>(s)) {}
616 sort(context & c, Z3_ast a):ast(c, a) {}
617 operator Z3_sort() const { return reinterpret_cast<Z3_sort>(m_ast); }
618
622 unsigned id() const { unsigned r = Z3_get_sort_id(ctx(), *this); check_error(); return r; }
623
627 Z3_sort_kind sort_kind() const { return Z3_get_sort_kind(*m_ctx, *this); }
631 symbol name() const { Z3_symbol s = Z3_get_sort_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
635 bool is_bool() const { return sort_kind() == Z3_BOOL_SORT; }
639 bool is_int() const { return sort_kind() == Z3_INT_SORT; }
643 bool is_real() const { return sort_kind() == Z3_REAL_SORT; }
647 bool is_arith() const { return is_int() || is_real(); }
651 bool is_bv() const { return sort_kind() == Z3_BV_SORT; }
655 bool is_array() const { return sort_kind() == Z3_ARRAY_SORT; }
659 bool is_datatype() const { return sort_kind() == Z3_DATATYPE_SORT; }
663 bool is_relation() const { return sort_kind() == Z3_RELATION_SORT; }
667 bool is_seq() const { return sort_kind() == Z3_SEQ_SORT; }
671 bool is_re() const { return sort_kind() == Z3_RE_SORT; }
679 bool is_fpa() const { return sort_kind() == Z3_FLOATING_POINT_SORT; }
680
686 unsigned bv_size() const { assert(is_bv()); unsigned r = Z3_get_bv_sort_size(ctx(), *this); check_error(); return r; }
687
688 unsigned fpa_ebits() const { assert(is_fpa()); unsigned r = Z3_fpa_get_ebits(ctx(), *this); check_error(); return r; }
689
690 unsigned fpa_sbits() const { assert(is_fpa()); unsigned r = Z3_fpa_get_sbits(ctx(), *this); check_error(); return r; }
696 sort array_domain() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_domain(ctx(), *this); check_error(); return sort(ctx(), s); }
702 sort array_range() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_range(ctx(), *this); check_error(); return sort(ctx(), s); }
703
704 friend std::ostream & operator<<(std::ostream & out, sort const & s) { return out << Z3_sort_to_string(s.ctx(), Z3_sort(s.m_ast)); }
705 };
706
711 class func_decl : public ast {
712 public:
714 func_decl(context & c, Z3_func_decl n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
715 operator Z3_func_decl() const { return reinterpret_cast<Z3_func_decl>(m_ast); }
716
720 unsigned id() const { unsigned r = Z3_get_func_decl_id(ctx(), *this); check_error(); return r; }
721
722 unsigned arity() const { return Z3_get_arity(ctx(), *this); }
723 sort domain(unsigned i) const { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }
724 sort range() const { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }
725 symbol name() const { Z3_symbol s = Z3_get_decl_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
726 Z3_decl_kind decl_kind() const { return Z3_get_decl_kind(ctx(), *this); }
727
729 Z3_func_decl tc = Z3_mk_transitive_closure(ctx(), *this); check_error(); return func_decl(ctx(), tc);
730 }
731
732 bool is_const() const { return arity() == 0; }
733
734 expr operator()() const;
735 expr operator()(unsigned n, expr const * args) const;
736 expr operator()(expr_vector const& v) const;
737 expr operator()(expr const & a) const;
738 expr operator()(int a) const;
739 expr operator()(expr const & a1, expr const & a2) const;
740 expr operator()(expr const & a1, int a2) const;
741 expr operator()(int a1, expr const & a2) const;
742 expr operator()(expr const & a1, expr const & a2, expr const & a3) const;
743 expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const;
744 expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const;
745 };
746
750 expr select(expr const & a, expr const& i);
751 expr select(expr const & a, expr_vector const & i);
752
757 class expr : public ast {
758 public:
759 expr(context & c):ast(c) {}
760 expr(context & c, Z3_ast n):ast(c, reinterpret_cast<Z3_ast>(n)) {}
761
765 sort get_sort() const { Z3_sort s = Z3_get_sort(*m_ctx, m_ast); check_error(); return sort(*m_ctx, s); }
766
770 bool is_bool() const { return get_sort().is_bool(); }
774 bool is_int() const { return get_sort().is_int(); }
778 bool is_real() const { return get_sort().is_real(); }
782 bool is_arith() const { return get_sort().is_arith(); }
786 bool is_bv() const { return get_sort().is_bv(); }
790 bool is_array() const { return get_sort().is_array(); }
794 bool is_datatype() const { return get_sort().is_datatype(); }
798 bool is_relation() const { return get_sort().is_relation(); }
802 bool is_seq() const { return get_sort().is_seq(); }
806 bool is_re() const { return get_sort().is_re(); }
807
816 bool is_finite_domain() const { return get_sort().is_finite_domain(); }
820 bool is_fpa() const { return get_sort().is_fpa(); }
821
827 bool is_numeral() const { return kind() == Z3_NUMERAL_AST; }
828 bool is_numeral_i64(int64_t& i) const { bool r = Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}
829 bool is_numeral_u64(uint64_t& i) const { bool r = Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}
830 bool is_numeral_i(int& i) const { bool r = Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}
831 bool is_numeral_u(unsigned& i) const { bool r = Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
832 bool is_numeral(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; }
833 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; }
834 bool is_numeral(double& d) const { if (!is_numeral()) return false; d = Z3_get_numeral_double(ctx(), m_ast); check_error(); return true; }
835 bool as_binary(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_binary_string(ctx(), m_ast); check_error(); return true; }
836
837 double as_double() const { double d = 0; is_numeral(d); return d; }
838 uint64_t as_uint64() const { uint64_t r = 0; is_numeral_u64(r); return r; }
839 uint64_t as_int64() const { int64_t r = 0; is_numeral_i64(r); return r; }
840
841
845 bool is_app() const { return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
849 bool is_const() const { return is_app() && num_args() == 0; }
853 bool is_quantifier() const { return kind() == Z3_QUANTIFIER_AST; }
854
858 bool is_forall() const { return Z3_is_quantifier_forall(ctx(), m_ast); }
862 bool is_exists() const { return Z3_is_quantifier_exists(ctx(), m_ast); }
866 bool is_lambda() const { return Z3_is_lambda(ctx(), m_ast); }
871 bool is_var() const { return kind() == Z3_VAR_AST; }
875 bool is_algebraic() const { return Z3_is_algebraic_number(ctx(), m_ast); }
876
880 bool is_well_sorted() const { bool r = Z3_is_well_sorted(ctx(), m_ast); check_error(); return r; }
881
885 expr mk_is_inf() const {
886 assert(is_fpa());
887 Z3_ast r = Z3_mk_fpa_is_infinite(ctx(), m_ast);
888 check_error();
889 return expr(ctx(), r);
890 }
891
895 expr mk_is_nan() const {
896 assert(is_fpa());
897 Z3_ast r = Z3_mk_fpa_is_nan(ctx(), m_ast);
898 check_error();
899 return expr(ctx(), r);
900 }
901
906 assert(is_fpa());
907 Z3_ast r = Z3_mk_fpa_is_normal(ctx(), m_ast);
908 check_error();
909 return expr(ctx(), r);
910 }
911
916 assert(is_fpa());
917 Z3_ast r = Z3_mk_fpa_is_subnormal(ctx(), m_ast);
918 check_error();
919 return expr(ctx(), r);
920 }
921
925 expr mk_is_zero() const {
926 assert(is_fpa());
927 Z3_ast r = Z3_mk_fpa_is_zero(ctx(), m_ast);
928 check_error();
929 return expr(ctx(), r);
930 }
931
936 assert(is_fpa());
937 Z3_ast r = Z3_mk_fpa_to_ieee_bv(ctx(), m_ast);
938 check_error();
939 return expr(ctx(), r);
940 }
941
945 expr mk_from_ieee_bv(sort const &s) const {
946 assert(is_bv());
947 Z3_ast r = Z3_mk_fpa_to_fp_bv(ctx(), m_ast, s);
948 check_error();
949 return expr(ctx(), r);
950 }
951
958 std::string get_decimal_string(int precision) const {
959 assert(is_numeral() || is_algebraic());
960 return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
961 }
962
966 expr algebraic_lower(unsigned precision) const {
967 assert(is_algebraic());
968 Z3_ast r = Z3_get_algebraic_number_lower(ctx(), m_ast, precision);
969 check_error();
970 return expr(ctx(), r);
971 }
972
973 expr algebraic_upper(unsigned precision) const {
974 assert(is_algebraic());
975 Z3_ast r = Z3_get_algebraic_number_upper(ctx(), m_ast, precision);
976 check_error();
977 return expr(ctx(), r);
978 }
979
984 assert(is_algebraic());
985 Z3_ast_vector r = Z3_algebraic_get_poly(ctx(), m_ast);
986 check_error();
987 return expr_vector(ctx(), r);
988 }
989
993 unsigned algebraic_i() const {
994 assert(is_algebraic());
995 unsigned i = Z3_algebraic_get_i(ctx(), m_ast);
996 check_error();
997 return i;
998 }
999
1003 unsigned id() const { unsigned r = Z3_get_ast_id(ctx(), m_ast); check_error(); return r; }
1004
1015 int get_numeral_int() const {
1016 int result = 0;
1017 if (!is_numeral_i(result)) {
1018 assert(ctx().enable_exceptions());
1019 if (!ctx().enable_exceptions()) return 0;
1020 Z3_THROW(exception("numeral does not fit in machine int"));
1021 }
1022 return result;
1023 }
1024
1034 unsigned get_numeral_uint() const {
1035 assert(is_numeral());
1036 unsigned result = 0;
1037 if (!is_numeral_u(result)) {
1038 assert(ctx().enable_exceptions());
1039 if (!ctx().enable_exceptions()) return 0;
1040 Z3_THROW(exception("numeral does not fit in machine uint"));
1041 }
1042 return result;
1043 }
1044
1051 int64_t get_numeral_int64() const {
1052 assert(is_numeral());
1053 int64_t result = 0;
1054 if (!is_numeral_i64(result)) {
1055 assert(ctx().enable_exceptions());
1056 if (!ctx().enable_exceptions()) return 0;
1057 Z3_THROW(exception("numeral does not fit in machine int64_t"));
1058 }
1059 return result;
1060 }
1061
1068 uint64_t get_numeral_uint64() const {
1069 assert(is_numeral());
1070 uint64_t result = 0;
1071 if (!is_numeral_u64(result)) {
1072 assert(ctx().enable_exceptions());
1073 if (!ctx().enable_exceptions()) return 0;
1074 Z3_THROW(exception("numeral does not fit in machine uint64_t"));
1075 }
1076 return result;
1077 }
1078
1080 return Z3_get_bool_value(ctx(), m_ast);
1081 }
1082
1083 expr numerator() const {
1084 assert(is_numeral());
1085 Z3_ast r = Z3_get_numerator(ctx(), m_ast);
1086 check_error();
1087 return expr(ctx(),r);
1088 }
1089
1090
1092 assert(is_numeral());
1093 Z3_ast r = Z3_get_denominator(ctx(), m_ast);
1094 check_error();
1095 return expr(ctx(),r);
1096 }
1097
1098
1103 bool is_string_value() const { return Z3_is_string(ctx(), m_ast); }
1104
1110 std::string get_escaped_string() const {
1111 assert(is_string_value());
1112 char const* s = Z3_get_string(ctx(), m_ast);
1113 check_error();
1114 return std::string(s);
1115 }
1116
1117 std::string get_string() const {
1118 assert(is_string_value());
1119 unsigned n;
1120 char const* s = Z3_get_lstring(ctx(), m_ast, &n);
1121 check_error();
1122 return std::string(s, n);
1123 }
1124
1125 operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
1126
1133 func_decl decl() const { Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }
1140 unsigned num_args() const { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
1148 expr arg(unsigned i) const { Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }
1149
1155 expr body() const { assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
1156
1162 friend expr operator!(expr const & a);
1163
1170 friend expr operator&&(expr const & a, expr const & b);
1171
1172
1179 friend expr operator&&(expr const & a, bool b);
1186 friend expr operator&&(bool a, expr const & b);
1187
1194 friend expr operator||(expr const & a, expr const & b);
1201 friend expr operator||(expr const & a, bool b);
1202
1209 friend expr operator||(bool a, expr const & b);
1210
1211 friend expr implies(expr const & a, expr const & b);
1212 friend expr implies(expr const & a, bool b);
1213 friend expr implies(bool a, expr const & b);
1214
1215 friend expr mk_or(expr_vector const& args);
1216 friend expr mk_and(expr_vector const& args);
1217
1218 friend expr ite(expr const & c, expr const & t, expr const & e);
1219
1220 bool is_true() const { return is_app() && Z3_OP_TRUE == decl().decl_kind(); }
1221 bool is_false() const { return is_app() && Z3_OP_FALSE == decl().decl_kind(); }
1222 bool is_not() const { return is_app() && Z3_OP_NOT == decl().decl_kind(); }
1223 bool is_and() const { return is_app() && Z3_OP_AND == decl().decl_kind(); }
1224 bool is_or() const { return is_app() && Z3_OP_OR == decl().decl_kind(); }
1225 bool is_xor() const { return is_app() && Z3_OP_XOR == decl().decl_kind(); }
1226 bool is_implies() const { return is_app() && Z3_OP_IMPLIES == decl().decl_kind(); }
1227 bool is_eq() const { return is_app() && Z3_OP_EQ == decl().decl_kind(); }
1228 bool is_ite() const { return is_app() && Z3_OP_ITE == decl().decl_kind(); }
1229 bool is_distinct() const { return is_app() && Z3_OP_DISTINCT == decl().decl_kind(); }
1230
1231 friend expr distinct(expr_vector const& args);
1232 friend expr concat(expr const& a, expr const& b);
1233 friend expr concat(expr_vector const& args);
1234
1235 friend expr operator==(expr const & a, expr const & b);
1236 friend expr operator==(expr const & a, int b);
1237 friend expr operator==(int a, expr const & b);
1238
1239 friend expr operator!=(expr const & a, expr const & b);
1240 friend expr operator!=(expr const & a, int b);
1241 friend expr operator!=(int a, expr const & b);
1242
1243 friend expr operator+(expr const & a, expr const & b);
1244 friend expr operator+(expr const & a, int b);
1245 friend expr operator+(int a, expr const & b);
1246 friend expr sum(expr_vector const& args);
1247
1248 friend expr operator*(expr const & a, expr const & b);
1249 friend expr operator*(expr const & a, int b);
1250 friend expr operator*(int a, expr const & b);
1251
1252 /* \brief Power operator */
1253 friend expr pw(expr const & a, expr const & b);
1254 friend expr pw(expr const & a, int b);
1255 friend expr pw(int a, expr const & b);
1256
1257 /* \brief mod operator */
1258 friend expr mod(expr const& a, expr const& b);
1259 friend expr mod(expr const& a, int b);
1260 friend expr mod(int a, expr const& b);
1261
1262 /* \brief rem operator */
1263 friend expr rem(expr const& a, expr const& b);
1264 friend expr rem(expr const& a, int b);
1265 friend expr rem(int a, expr const& b);
1266
1267 friend expr is_int(expr const& e);
1268
1269 friend expr operator/(expr const & a, expr const & b);
1270 friend expr operator/(expr const & a, int b);
1271 friend expr operator/(int a, expr const & b);
1272
1273 friend expr operator-(expr const & a);
1274
1275 friend expr operator-(expr const & a, expr const & b);
1276 friend expr operator-(expr const & a, int b);
1277 friend expr operator-(int a, expr const & b);
1278
1279 friend expr operator<=(expr const & a, expr const & b);
1280 friend expr operator<=(expr const & a, int b);
1281 friend expr operator<=(int a, expr const & b);
1282
1283
1284 friend expr operator>=(expr const & a, expr const & b);
1285 friend expr operator>=(expr const & a, int b);
1286 friend expr operator>=(int a, expr const & b);
1287
1288 friend expr operator<(expr const & a, expr const & b);
1289 friend expr operator<(expr const & a, int b);
1290 friend expr operator<(int a, expr const & b);
1291
1292 friend expr operator>(expr const & a, expr const & b);
1293 friend expr operator>(expr const & a, int b);
1294 friend expr operator>(int a, expr const & b);
1295
1296 friend expr pble(expr_vector const& es, int const * coeffs, int bound);
1297 friend expr pbge(expr_vector const& es, int const * coeffs, int bound);
1298 friend expr pbeq(expr_vector const& es, int const * coeffs, int bound);
1299 friend expr atmost(expr_vector const& es, unsigned bound);
1300 friend expr atleast(expr_vector const& es, unsigned bound);
1301
1302 friend expr operator&(expr const & a, expr const & b);
1303 friend expr operator&(expr const & a, int b);
1304 friend expr operator&(int a, expr const & b);
1305
1306 friend expr operator^(expr const & a, expr const & b);
1307 friend expr operator^(expr const & a, int b);
1308 friend expr operator^(int a, expr const & b);
1309
1310 friend expr operator|(expr const & a, expr const & b);
1311 friend expr operator|(expr const & a, int b);
1312 friend expr operator|(int a, expr const & b);
1313 friend expr nand(expr const& a, expr const& b);
1314 friend expr nor(expr const& a, expr const& b);
1315 friend expr xnor(expr const& a, expr const& b);
1316
1317 friend expr min(expr const& a, expr const& b);
1318 friend expr max(expr const& a, expr const& b);
1319
1320 friend expr bv2int(expr const& a, bool is_signed);
1321 friend expr int2bv(unsigned n, expr const& a);
1322 friend expr bvadd_no_overflow(expr const& a, expr const& b, bool is_signed);
1323 friend expr bvadd_no_underflow(expr const& a, expr const& b);
1324 friend expr bvsub_no_overflow(expr const& a, expr const& b);
1325 friend expr bvsub_no_underflow(expr const& a, expr const& b, bool is_signed);
1326 friend expr bvsdiv_no_overflow(expr const& a, expr const& b);
1327 friend expr bvneg_no_overflow(expr const& a);
1328 friend expr bvmul_no_overflow(expr const& a, expr const& b, bool is_signed);
1329 friend expr bvmul_no_underflow(expr const& a, expr const& b);
1330
1331 expr rotate_left(unsigned i) { Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
1332 expr rotate_right(unsigned i) { Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
1333 expr repeat(unsigned i) { Z3_ast r = Z3_mk_repeat(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
1334
1335 friend expr bvredor(expr const & a);
1336 friend expr bvredand(expr const & a);
1337
1338 friend expr abs(expr const & a);
1339 friend expr sqrt(expr const & a, expr const & rm);
1340 friend expr fp_eq(expr const & a, expr const & b);
1341
1342 friend expr operator~(expr const & a);
1343 expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }
1344 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)); }
1345 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)); }
1346
1350 friend expr fma(expr const& a, expr const& b, expr const& c, expr const& rm);
1351
1355 friend expr fpa_fp(expr const& sgn, expr const& exp, expr const& sig);
1356
1360 friend expr fpa_to_sbv(expr const& t, unsigned sz);
1361
1365 friend expr fpa_to_ubv(expr const& t, unsigned sz);
1366
1370 friend expr sbv_to_fpa(expr const& t, sort s);
1371
1375 friend expr ubv_to_fpa(expr const& t, sort s);
1376
1380 friend expr fpa_to_fpa(expr const& t, sort s);
1381
1385 friend expr round_fpa_to_closest_integer(expr const& t);
1386
1392 expr extract(expr const& offset, expr const& length) const {
1393 check_context(*this, offset); check_context(offset, length);
1394 Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
1395 }
1396 expr replace(expr const& src, expr const& dst) const {
1397 check_context(*this, src); check_context(src, dst);
1398 Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
1399 check_error();
1400 return expr(ctx(), r);
1401 }
1402 expr unit() const {
1403 Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
1404 check_error();
1405 return expr(ctx(), r);
1406 }
1407 expr contains(expr const& s) const {
1408 check_context(*this, s);
1409 Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
1410 check_error();
1411 return expr(ctx(), r);
1412 }
1413 expr at(expr const& index) const {
1414 check_context(*this, index);
1415 Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
1416 check_error();
1417 return expr(ctx(), r);
1418 }
1419 expr nth(expr const& index) const {
1420 check_context(*this, index);
1421 Z3_ast r = Z3_mk_seq_nth(ctx(), *this, index);
1422 check_error();
1423 return expr(ctx(), r);
1424 }
1425 expr length() const {
1426 Z3_ast r = Z3_mk_seq_length(ctx(), *this);
1427 check_error();
1428 return expr(ctx(), r);
1429 }
1430 expr stoi() const {
1431 Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
1432 check_error();
1433 return expr(ctx(), r);
1434 }
1435 expr itos() const {
1436 Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
1437 check_error();
1438 return expr(ctx(), r);
1439 }
1440
1441 friend expr range(expr const& lo, expr const& hi);
1445 expr loop(unsigned lo) {
1446 Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0);
1447 check_error();
1448 return expr(ctx(), r);
1449 }
1450 expr loop(unsigned lo, unsigned hi) {
1451 Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi);
1452 check_error();
1453 return expr(ctx(), r);
1454 }
1455
1459 expr operator[](expr const& index) const {
1460 assert(is_array() || is_seq());
1461 if (is_array()) {
1462 return select(*this, index);
1463 }
1464 return nth(index);
1465 }
1466
1467 expr operator[](expr_vector const& index) const {
1468 return select(*this, index);
1469 }
1470
1474 expr simplify() const { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
1478 expr simplify(params const & p) const { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
1479
1483 expr substitute(expr_vector const& src, expr_vector const& dst);
1484
1488 expr substitute(expr_vector const& dst);
1489
1490 };
1491
1492#define _Z3_MK_BIN_(a, b, binop) \
1493 check_context(a, b); \
1494 Z3_ast r = binop(a.ctx(), a, b); \
1495 a.check_error(); \
1496 return expr(a.ctx(), r); \
1497
1498
1499 inline expr implies(expr const & a, expr const & b) {
1500 assert(a.is_bool() && b.is_bool());
1502 }
1503 inline expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); }
1504 inline expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); }
1505
1506
1507 inline expr pw(expr const & a, expr const & b) { _Z3_MK_BIN_(a, b, Z3_mk_power); }
1508 inline expr pw(expr const & a, int b) { return pw(a, a.ctx().num_val(b, a.get_sort())); }
1509 inline expr pw(int a, expr const & b) { return pw(b.ctx().num_val(a, b.get_sort()), b); }
1510
1511 inline expr mod(expr const& a, expr const& b) {
1512 if (a.is_bv()) {
1513 _Z3_MK_BIN_(a, b, Z3_mk_bvsmod);
1514 }
1515 else {
1516 _Z3_MK_BIN_(a, b, Z3_mk_mod);
1517 }
1518 }
1519 inline expr mod(expr const & a, int b) { return mod(a, a.ctx().num_val(b, a.get_sort())); }
1520 inline expr mod(int a, expr const & b) { return mod(b.ctx().num_val(a, b.get_sort()), b); }
1521
1522 inline expr operator%(expr const& a, expr const& b) { return mod(a, b); }
1523 inline expr operator%(expr const& a, int b) { return mod(a, b); }
1524 inline expr operator%(int a, expr const& b) { return mod(a, b); }
1525
1526
1527 inline expr rem(expr const& a, expr const& b) {
1528 if (a.is_fpa() && b.is_fpa()) {
1530 } else {
1531 _Z3_MK_BIN_(a, b, Z3_mk_rem);
1532 }
1533 }
1534 inline expr rem(expr const & a, int b) { return rem(a, a.ctx().num_val(b, a.get_sort())); }
1535 inline expr rem(int a, expr const & b) { return rem(b.ctx().num_val(a, b.get_sort()), b); }
1536
1537#undef _Z3_MK_BIN_
1538
1539#define _Z3_MK_UN_(a, mkun) \
1540 Z3_ast r = mkun(a.ctx(), a); \
1541 a.check_error(); \
1542 return expr(a.ctx(), r); \
1543
1544
1545 inline expr operator!(expr const & a) { assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); }
1546
1547 inline expr is_int(expr const& e) { _Z3_MK_UN_(e, Z3_mk_is_int); }
1548
1549#undef _Z3_MK_UN_
1550
1551 inline expr operator&&(expr const & a, expr const & b) {
1552 check_context(a, b);
1553 assert(a.is_bool() && b.is_bool());
1554 Z3_ast args[2] = { a, b };
1555 Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1556 a.check_error();
1557 return expr(a.ctx(), r);
1558 }
1559
1560 inline expr operator&&(expr const & a, bool b) { return a && a.ctx().bool_val(b); }
1561 inline expr operator&&(bool a, expr const & b) { return b.ctx().bool_val(a) && b; }
1562
1563 inline expr operator||(expr const & a, expr const & b) {
1564 check_context(a, b);
1565 assert(a.is_bool() && b.is_bool());
1566 Z3_ast args[2] = { a, b };
1567 Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1568 a.check_error();
1569 return expr(a.ctx(), r);
1570 }
1571
1572 inline expr operator||(expr const & a, bool b) { return a || a.ctx().bool_val(b); }
1573
1574 inline expr operator||(bool a, expr const & b) { return b.ctx().bool_val(a) || b; }
1575
1576 inline expr operator==(expr const & a, expr const & b) {
1577 check_context(a, b);
1578 Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1579 a.check_error();
1580 return expr(a.ctx(), r);
1581 }
1582 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()); }
1583 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; }
1584 inline expr operator==(expr const & a, double b) { assert(a.is_fpa()); return a == a.ctx().fpa_val(b); }
1585 inline expr operator==(double a, expr const & b) { assert(b.is_fpa()); return b.ctx().fpa_val(a) == b; }
1586
1587 inline expr operator!=(expr const & a, expr const & b) {
1588 check_context(a, b);
1589 Z3_ast args[2] = { a, b };
1590 Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1591 a.check_error();
1592 return expr(a.ctx(), r);
1593 }
1594 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()); }
1595 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; }
1596 inline expr operator!=(expr const & a, double b) { assert(a.is_fpa()); return a != a.ctx().fpa_val(b); }
1597 inline expr operator!=(double a, expr const & b) { assert(b.is_fpa()); return b.ctx().fpa_val(a) != b; }
1598
1599 inline expr operator+(expr const & a, expr const & b) {
1600 check_context(a, b);
1601 Z3_ast r = 0;
1602 if (a.is_arith() && b.is_arith()) {
1603 Z3_ast args[2] = { a, b };
1604 r = Z3_mk_add(a.ctx(), 2, args);
1605 }
1606 else if (a.is_bv() && b.is_bv()) {
1607 r = Z3_mk_bvadd(a.ctx(), a, b);
1608 }
1609 else if (a.is_seq() && b.is_seq()) {
1610 return concat(a, b);
1611 }
1612 else if (a.is_re() && b.is_re()) {
1613 Z3_ast _args[2] = { a, b };
1614 r = Z3_mk_re_union(a.ctx(), 2, _args);
1615 }
1616 else if (a.is_fpa() && b.is_fpa()) {
1617 r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1618 }
1619 else {
1620 // operator is not supported by given arguments.
1621 assert(false);
1622 }
1623 a.check_error();
1624 return expr(a.ctx(), r);
1625 }
1626 inline expr operator+(expr const & a, int b) { return a + a.ctx().num_val(b, a.get_sort()); }
1627 inline expr operator+(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) + b; }
1628
1629 inline expr operator*(expr const & a, expr const & b) {
1630 check_context(a, b);
1631 Z3_ast r = 0;
1632 if (a.is_arith() && b.is_arith()) {
1633 Z3_ast args[2] = { a, b };
1634 r = Z3_mk_mul(a.ctx(), 2, args);
1635 }
1636 else if (a.is_bv() && b.is_bv()) {
1637 r = Z3_mk_bvmul(a.ctx(), a, b);
1638 }
1639 else if (a.is_fpa() && b.is_fpa()) {
1640 r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1641 }
1642 else {
1643 // operator is not supported by given arguments.
1644 assert(false);
1645 }
1646 a.check_error();
1647 return expr(a.ctx(), r);
1648 }
1649 inline expr operator*(expr const & a, int b) { return a * a.ctx().num_val(b, a.get_sort()); }
1650 inline expr operator*(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) * b; }
1651
1652
1653 inline expr operator>=(expr const & a, expr const & b) {
1654 check_context(a, b);
1655 Z3_ast r = 0;
1656 if (a.is_arith() && b.is_arith()) {
1657 r = Z3_mk_ge(a.ctx(), a, b);
1658 }
1659 else if (a.is_bv() && b.is_bv()) {
1660 r = Z3_mk_bvsge(a.ctx(), a, b);
1661 }
1662 else if (a.is_fpa() && b.is_fpa()) {
1663 r = Z3_mk_fpa_geq(a.ctx(), a, b);
1664 }
1665 else {
1666 // operator is not supported by given arguments.
1667 assert(false);
1668 }
1669 a.check_error();
1670 return expr(a.ctx(), r);
1671 }
1672
1673 inline expr operator/(expr const & a, expr const & b) {
1674 check_context(a, b);
1675 Z3_ast r = 0;
1676 if (a.is_arith() && b.is_arith()) {
1677 r = Z3_mk_div(a.ctx(), a, b);
1678 }
1679 else if (a.is_bv() && b.is_bv()) {
1680 r = Z3_mk_bvsdiv(a.ctx(), a, b);
1681 }
1682 else if (a.is_fpa() && b.is_fpa()) {
1683 r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1684 }
1685 else {
1686 // operator is not supported by given arguments.
1687 assert(false);
1688 }
1689 a.check_error();
1690 return expr(a.ctx(), r);
1691 }
1692 inline expr operator/(expr const & a, int b) { return a / a.ctx().num_val(b, a.get_sort()); }
1693 inline expr operator/(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) / b; }
1694
1695 inline expr operator-(expr const & a) {
1696 Z3_ast r = 0;
1697 if (a.is_arith()) {
1698 r = Z3_mk_unary_minus(a.ctx(), a);
1699 }
1700 else if (a.is_bv()) {
1701 r = Z3_mk_bvneg(a.ctx(), a);
1702 }
1703 else if (a.is_fpa()) {
1704 r = Z3_mk_fpa_neg(a.ctx(), a);
1705 }
1706 else {
1707 // operator is not supported by given arguments.
1708 assert(false);
1709 }
1710 a.check_error();
1711 return expr(a.ctx(), r);
1712 }
1713
1714 inline expr operator-(expr const & a, expr const & b) {
1715 check_context(a, b);
1716 Z3_ast r = 0;
1717 if (a.is_arith() && b.is_arith()) {
1718 Z3_ast args[2] = { a, b };
1719 r = Z3_mk_sub(a.ctx(), 2, args);
1720 }
1721 else if (a.is_bv() && b.is_bv()) {
1722 r = Z3_mk_bvsub(a.ctx(), a, b);
1723 }
1724 else if (a.is_fpa() && b.is_fpa()) {
1725 r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1726 }
1727 else {
1728 // operator is not supported by given arguments.
1729 assert(false);
1730 }
1731 a.check_error();
1732 return expr(a.ctx(), r);
1733 }
1734 inline expr operator-(expr const & a, int b) { return a - a.ctx().num_val(b, a.get_sort()); }
1735 inline expr operator-(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) - b; }
1736
1737 inline expr operator<=(expr const & a, expr const & b) {
1738 check_context(a, b);
1739 Z3_ast r = 0;
1740 if (a.is_arith() && b.is_arith()) {
1741 r = Z3_mk_le(a.ctx(), a, b);
1742 }
1743 else if (a.is_bv() && b.is_bv()) {
1744 r = Z3_mk_bvsle(a.ctx(), a, b);
1745 }
1746 else if (a.is_fpa() && b.is_fpa()) {
1747 r = Z3_mk_fpa_leq(a.ctx(), a, b);
1748 }
1749 else {
1750 // operator is not supported by given arguments.
1751 assert(false);
1752 }
1753 a.check_error();
1754 return expr(a.ctx(), r);
1755 }
1756 inline expr operator<=(expr const & a, int b) { return a <= a.ctx().num_val(b, a.get_sort()); }
1757 inline expr operator<=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) <= b; }
1758
1759 inline expr operator>=(expr const & a, int b) { return a >= a.ctx().num_val(b, a.get_sort()); }
1760 inline expr operator>=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) >= b; }
1761
1762 inline expr operator<(expr const & a, expr const & b) {
1763 check_context(a, b);
1764 Z3_ast r = 0;
1765 if (a.is_arith() && b.is_arith()) {
1766 r = Z3_mk_lt(a.ctx(), a, b);
1767 }
1768 else if (a.is_bv() && b.is_bv()) {
1769 r = Z3_mk_bvslt(a.ctx(), a, b);
1770 }
1771 else if (a.is_fpa() && b.is_fpa()) {
1772 r = Z3_mk_fpa_lt(a.ctx(), a, b);
1773 }
1774 else {
1775 // operator is not supported by given arguments.
1776 assert(false);
1777 }
1778 a.check_error();
1779 return expr(a.ctx(), r);
1780 }
1781 inline expr operator<(expr const & a, int b) { return a < a.ctx().num_val(b, a.get_sort()); }
1782 inline expr operator<(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) < b; }
1783
1784 inline expr operator>(expr const & a, expr const & b) {
1785 check_context(a, b);
1786 Z3_ast r = 0;
1787 if (a.is_arith() && b.is_arith()) {
1788 r = Z3_mk_gt(a.ctx(), a, b);
1789 }
1790 else if (a.is_bv() && b.is_bv()) {
1791 r = Z3_mk_bvsgt(a.ctx(), a, b);
1792 }
1793 else if (a.is_fpa() && b.is_fpa()) {
1794 r = Z3_mk_fpa_gt(a.ctx(), a, b);
1795 }
1796 else {
1797 // operator is not supported by given arguments.
1798 assert(false);
1799 }
1800 a.check_error();
1801 return expr(a.ctx(), r);
1802 }
1803 inline expr operator>(expr const & a, int b) { return a > a.ctx().num_val(b, a.get_sort()); }
1804 inline expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > b; }
1805
1806 inline expr operator&(expr const & a, expr const & b) { if (a.is_bool()) return a && b; check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); return expr(a.ctx(), r); }
1807 inline expr operator&(expr const & a, int b) { return a & a.ctx().num_val(b, a.get_sort()); }
1808 inline expr operator&(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) & b; }
1809
1810 inline expr operator^(expr const & a, expr const & b) { check_context(a, b); Z3_ast r = a.is_bool() ? Z3_mk_xor(a.ctx(), a, b) : Z3_mk_bvxor(a.ctx(), a, b); return expr(a.ctx(), r); }
1811 inline expr operator^(expr const & a, int b) { return a ^ a.ctx().num_val(b, a.get_sort()); }
1812 inline expr operator^(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) ^ b; }
1813
1814 inline expr operator|(expr const & a, expr const & b) { if (a.is_bool()) return a || b; check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); return expr(a.ctx(), r); }
1815 inline expr operator|(expr const & a, int b) { return a | a.ctx().num_val(b, a.get_sort()); }
1816 inline expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; }
1817
1818 inline expr nand(expr const& a, expr const& b) { if (a.is_bool()) return !(a && b); check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); return expr(a.ctx(), r); }
1819 inline expr nor(expr const& a, expr const& b) { if (a.is_bool()) return !(a || b); check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); return expr(a.ctx(), r); }
1820 inline expr xnor(expr const& a, expr const& b) { if (a.is_bool()) return !(a ^ b); check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); return expr(a.ctx(), r); }
1821 inline expr min(expr const& a, expr const& b) {
1822 check_context(a, b);
1823 Z3_ast r;
1824 if (a.is_arith()) {
1825 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
1826 }
1827 else if (a.is_bv()) {
1828 r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
1829 }
1830 else {
1831 assert(a.is_fpa());
1832 r = Z3_mk_fpa_min(a.ctx(), a, b);
1833 }
1834 return expr(a.ctx(), r);
1835 }
1836 inline expr max(expr const& a, expr const& b) {
1837 check_context(a, b);
1838 Z3_ast r;
1839 if (a.is_arith()) {
1840 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
1841 }
1842 else if (a.is_bv()) {
1843 r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
1844 }
1845 else {
1846 assert(a.is_fpa());
1847 r = Z3_mk_fpa_max(a.ctx(), a, b);
1848 }
1849 return expr(a.ctx(), r);
1850 }
1851 inline expr bvredor(expr const & a) {
1852 assert(a.is_bv());
1853 Z3_ast r = Z3_mk_bvredor(a.ctx(), a);
1854 a.check_error();
1855 return expr(a.ctx(), r);
1856 }
1857 inline expr bvredand(expr const & a) {
1858 assert(a.is_bv());
1859 Z3_ast r = Z3_mk_bvredor(a.ctx(), a);
1860 a.check_error();
1861 return expr(a.ctx(), r);
1862 }
1863 inline expr abs(expr const & a) {
1864 Z3_ast r;
1865 if (a.is_int()) {
1866 expr zero = a.ctx().int_val(0);
1867 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1868 }
1869 else if (a.is_real()) {
1870 expr zero = a.ctx().real_val(0);
1871 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1872 }
1873 else {
1874 r = Z3_mk_fpa_abs(a.ctx(), a);
1875 }
1876 a.check_error();
1877 return expr(a.ctx(), r);
1878 }
1879 inline expr sqrt(expr const & a, expr const& rm) {
1880 check_context(a, rm);
1881 assert(a.is_fpa());
1882 Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
1883 a.check_error();
1884 return expr(a.ctx(), r);
1885 }
1886 inline expr fp_eq(expr const & a, expr const & b) {
1887 check_context(a, b);
1888 assert(a.is_fpa());
1889 Z3_ast r = Z3_mk_fpa_eq(a.ctx(), a, b);
1890 a.check_error();
1891 return expr(a.ctx(), r);
1892 }
1893 inline expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
1894
1895 inline expr fma(expr const& a, expr const& b, expr const& c, expr const& rm) {
1896 check_context(a, b); check_context(a, c); check_context(a, rm);
1897 assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
1898 Z3_ast r = Z3_mk_fpa_fma(a.ctx(), rm, a, b, c);
1899 a.check_error();
1900 return expr(a.ctx(), r);
1901 }
1902
1903 inline expr fpa_fp(expr const& sgn, expr const& exp, expr const& sig) {
1904 check_context(sgn, exp); check_context(exp, sig);
1905 assert(sgn.is_bv() && exp.is_bv() && sig.is_bv());
1906 Z3_ast r = Z3_mk_fpa_fp(sgn.ctx(), sgn, exp, sig);
1907 sgn.check_error();
1908 return expr(sgn.ctx(), r);
1909 }
1910
1911 inline expr fpa_to_sbv(expr const& t, unsigned sz) {
1912 assert(t.is_fpa());
1913 Z3_ast r = Z3_mk_fpa_to_sbv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
1914 t.check_error();
1915 return expr(t.ctx(), r);
1916 }
1917
1918 inline expr fpa_to_ubv(expr const& t, unsigned sz) {
1919 assert(t.is_fpa());
1920 Z3_ast r = Z3_mk_fpa_to_ubv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
1921 t.check_error();
1922 return expr(t.ctx(), r);
1923 }
1924
1925 inline expr sbv_to_fpa(expr const& t, sort s) {
1926 assert(t.is_bv());
1927 Z3_ast r = Z3_mk_fpa_to_fp_signed(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
1928 t.check_error();
1929 return expr(t.ctx(), r);
1930 }
1931
1932 inline expr ubv_to_fpa(expr const& t, sort s) {
1933 assert(t.is_bv());
1934 Z3_ast r = Z3_mk_fpa_to_fp_unsigned(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
1935 t.check_error();
1936 return expr(t.ctx(), r);
1937 }
1938
1939 inline expr fpa_to_fpa(expr const& t, sort s) {
1940 assert(t.is_fpa());
1941 Z3_ast r = Z3_mk_fpa_to_fp_float(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
1942 t.check_error();
1943 return expr(t.ctx(), r);
1944 }
1945
1947 assert(t.is_fpa());
1948 Z3_ast r = Z3_mk_fpa_round_to_integral(t.ctx(), t.ctx().fpa_rounding_mode(), t);
1949 t.check_error();
1950 return expr(t.ctx(), r);
1951 }
1952
1958 inline expr ite(expr const & c, expr const & t, expr const & e) {
1959 check_context(c, t); check_context(c, e);
1960 assert(c.is_bool());
1961 Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
1962 c.check_error();
1963 return expr(c.ctx(), r);
1964 }
1965
1966
1971 inline expr to_expr(context & c, Z3_ast a) {
1972 c.check_error();
1973 assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
1975 Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
1977 return expr(c, a);
1978 }
1979
1980 inline sort to_sort(context & c, Z3_sort s) {
1981 c.check_error();
1982 return sort(c, s);
1983 }
1984
1985 inline func_decl to_func_decl(context & c, Z3_func_decl f) {
1986 c.check_error();
1987 return func_decl(c, f);
1988 }
1989
1993 inline expr sle(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsle(a.ctx(), a, b)); }
1994 inline expr sle(expr const & a, int b) { return sle(a, a.ctx().num_val(b, a.get_sort())); }
1995 inline expr sle(int a, expr const & b) { return sle(b.ctx().num_val(a, b.get_sort()), b); }
1999 inline expr slt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvslt(a.ctx(), a, b)); }
2000 inline expr slt(expr const & a, int b) { return slt(a, a.ctx().num_val(b, a.get_sort())); }
2001 inline expr slt(int a, expr const & b) { return slt(b.ctx().num_val(a, b.get_sort()), b); }
2005 inline expr sge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsge(a.ctx(), a, b)); }
2006 inline expr sge(expr const & a, int b) { return sge(a, a.ctx().num_val(b, a.get_sort())); }
2007 inline expr sge(int a, expr const & b) { return sge(b.ctx().num_val(a, b.get_sort()), b); }
2011 inline expr sgt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsgt(a.ctx(), a, b)); }
2012 inline expr sgt(expr const & a, int b) { return sgt(a, a.ctx().num_val(b, a.get_sort())); }
2013 inline expr sgt(int a, expr const & b) { return sgt(b.ctx().num_val(a, b.get_sort()), b); }
2014
2015
2019 inline expr ule(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
2020 inline expr ule(expr const & a, int b) { return ule(a, a.ctx().num_val(b, a.get_sort())); }
2021 inline expr ule(int a, expr const & b) { return ule(b.ctx().num_val(a, b.get_sort()), b); }
2025 inline expr ult(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }
2026 inline expr ult(expr const & a, int b) { return ult(a, a.ctx().num_val(b, a.get_sort())); }
2027 inline expr ult(int a, expr const & b) { return ult(b.ctx().num_val(a, b.get_sort()), b); }
2031 inline expr uge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }
2032 inline expr uge(expr const & a, int b) { return uge(a, a.ctx().num_val(b, a.get_sort())); }
2033 inline expr uge(int a, expr const & b) { return uge(b.ctx().num_val(a, b.get_sort()), b); }
2037 inline expr ugt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
2038 inline expr ugt(expr const & a, int b) { return ugt(a, a.ctx().num_val(b, a.get_sort())); }
2039 inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), b); }
2043 inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
2044 inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); }
2045 inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); }
2046
2050 inline expr srem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsrem(a.ctx(), a, b)); }
2051 inline expr srem(expr const & a, int b) { return srem(a, a.ctx().num_val(b, a.get_sort())); }
2052 inline expr srem(int a, expr const & b) { return srem(b.ctx().num_val(a, b.get_sort()), b); }
2053
2057 inline expr smod(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsmod(a.ctx(), a, b)); }
2058 inline expr smod(expr const & a, int b) { return smod(a, a.ctx().num_val(b, a.get_sort())); }
2059 inline expr smod(int a, expr const & b) { return smod(b.ctx().num_val(a, b.get_sort()), b); }
2060
2064 inline expr urem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvurem(a.ctx(), a, b)); }
2065 inline expr urem(expr const & a, int b) { return urem(a, a.ctx().num_val(b, a.get_sort())); }
2066 inline expr urem(int a, expr const & b) { return urem(b.ctx().num_val(a, b.get_sort()), b); }
2067
2071 inline expr shl(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvshl(a.ctx(), a, b)); }
2072 inline expr shl(expr const & a, int b) { return shl(a, a.ctx().num_val(b, a.get_sort())); }
2073 inline expr shl(int a, expr const & b) { return shl(b.ctx().num_val(a, b.get_sort()), b); }
2074
2078 inline expr lshr(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvlshr(a.ctx(), a, b)); }
2079 inline expr lshr(expr const & a, int b) { return lshr(a, a.ctx().num_val(b, a.get_sort())); }
2080 inline expr lshr(int a, expr const & b) { return lshr(b.ctx().num_val(a, b.get_sort()), b); }
2081
2085 inline expr ashr(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvashr(a.ctx(), a, b)); }
2086 inline expr ashr(expr const & a, int b) { return ashr(a, a.ctx().num_val(b, a.get_sort())); }
2087 inline expr ashr(int a, expr const & b) { return ashr(b.ctx().num_val(a, b.get_sort()), b); }
2088
2092 inline expr zext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_zero_ext(a.ctx(), i, a)); }
2093
2097 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); }
2098 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); }
2099
2103 inline expr bvadd_no_overflow(expr const& a, expr const& b, bool is_signed) {
2104 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);
2105 }
2106 inline expr bvadd_no_underflow(expr const& a, expr const& b) {
2107 check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2108 }
2109 inline expr bvsub_no_overflow(expr const& a, expr const& b) {
2110 check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2111 }
2112 inline expr bvsub_no_underflow(expr const& a, expr const& b, bool is_signed) {
2113 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);
2114 }
2115 inline expr bvsdiv_no_overflow(expr const& a, expr const& b) {
2116 check_context(a, b); Z3_ast r = Z3_mk_bvsdiv_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2117 }
2118 inline expr bvneg_no_overflow(expr const& a) {
2119 Z3_ast r = Z3_mk_bvneg_no_overflow(a.ctx(), a); a.check_error(); return expr(a.ctx(), r);
2120 }
2121 inline expr bvmul_no_overflow(expr const& a, expr const& b, bool is_signed) {
2122 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);
2123 }
2124 inline expr bvmul_no_underflow(expr const& a, expr const& b) {
2125 check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2126 }
2127
2128
2132 inline expr sext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_sign_ext(a.ctx(), i, a)); }
2133
2134 inline func_decl linear_order(sort const& a, unsigned index) {
2135 return to_func_decl(a.ctx(), Z3_mk_linear_order(a.ctx(), a, index));
2136 }
2137 inline func_decl partial_order(sort const& a, unsigned index) {
2138 return to_func_decl(a.ctx(), Z3_mk_partial_order(a.ctx(), a, index));
2139 }
2140 inline func_decl piecewise_linear_order(sort const& a, unsigned index) {
2141 return to_func_decl(a.ctx(), Z3_mk_piecewise_linear_order(a.ctx(), a, index));
2142 }
2143 inline func_decl tree_order(sort const& a, unsigned index) {
2144 return to_func_decl(a.ctx(), Z3_mk_tree_order(a.ctx(), a, index));
2145 }
2146
2147 template<> class cast_ast<ast> {
2148 public:
2149 ast operator()(context & c, Z3_ast a) { return ast(c, a); }
2150 };
2151
2152 template<> class cast_ast<expr> {
2153 public:
2154 expr operator()(context & c, Z3_ast a) {
2155 assert(Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
2156 Z3_get_ast_kind(c, a) == Z3_APP_AST ||
2158 Z3_get_ast_kind(c, a) == Z3_VAR_AST);
2159 return expr(c, a);
2160 }
2161 };
2162
2163 template<> class cast_ast<sort> {
2164 public:
2165 sort operator()(context & c, Z3_ast a) {
2166 assert(Z3_get_ast_kind(c, a) == Z3_SORT_AST);
2167 return sort(c, reinterpret_cast<Z3_sort>(a));
2168 }
2169 };
2170
2171 template<> class cast_ast<func_decl> {
2172 public:
2174 assert(Z3_get_ast_kind(c, a) == Z3_FUNC_DECL_AST);
2175 return func_decl(c, reinterpret_cast<Z3_func_decl>(a));
2176 }
2177 };
2178
2179 template<typename T>
2180 template<typename T2>
2181 array<T>::array(ast_vector_tpl<T2> const & v):m_array(new T[v.size()]), m_size(v.size()) {
2182 for (unsigned i = 0; i < m_size; i++) {
2183 m_array[i] = v[i];
2184 }
2185 }
2186
2187 // Basic functions for creating quantified formulas.
2188 // The C API should be used for creating quantifiers with patterns, weights, many variables, etc.
2189 inline expr forall(expr const & x, expr const & b) {
2190 check_context(x, b);
2191 Z3_app vars[] = {(Z3_app) x};
2192 Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2193 }
2194 inline expr forall(expr const & x1, expr const & x2, expr const & b) {
2195 check_context(x1, b); check_context(x2, b);
2196 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2197 Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2198 }
2199 inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
2200 check_context(x1, b); check_context(x2, b); check_context(x3, b);
2201 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2202 Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2203 }
2204 inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
2205 check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2206 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2207 Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2208 }
2209 inline expr forall(expr_vector const & xs, expr const & b) {
2210 array<Z3_app> vars(xs);
2211 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);
2212 }
2213 inline expr exists(expr const & x, expr const & b) {
2214 check_context(x, b);
2215 Z3_app vars[] = {(Z3_app) x};
2216 Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2217 }
2218 inline expr exists(expr const & x1, expr const & x2, expr const & b) {
2219 check_context(x1, b); check_context(x2, b);
2220 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2221 Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2222 }
2223 inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
2224 check_context(x1, b); check_context(x2, b); check_context(x3, b);
2225 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2226 Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2227 }
2228 inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
2229 check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2230 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2231 Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2232 }
2233 inline expr exists(expr_vector const & xs, expr const & b) {
2234 array<Z3_app> vars(xs);
2235 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);
2236 }
2237 inline expr lambda(expr const & x, expr const & b) {
2238 check_context(x, b);
2239 Z3_app vars[] = {(Z3_app) x};
2240 Z3_ast r = Z3_mk_lambda_const(b.ctx(), 1, vars, b); b.check_error(); return expr(b.ctx(), r);
2241 }
2242 inline expr lambda(expr const & x1, expr const & x2, expr const & b) {
2243 check_context(x1, b); check_context(x2, b);
2244 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2245 Z3_ast r = Z3_mk_lambda_const(b.ctx(), 2, vars, b); b.check_error(); return expr(b.ctx(), r);
2246 }
2247 inline expr lambda(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
2248 check_context(x1, b); check_context(x2, b); check_context(x3, b);
2249 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2250 Z3_ast r = Z3_mk_lambda_const(b.ctx(), 3, vars, b); b.check_error(); return expr(b.ctx(), r);
2251 }
2252 inline expr lambda(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
2253 check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2254 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2255 Z3_ast r = Z3_mk_lambda_const(b.ctx(), 4, vars, b); b.check_error(); return expr(b.ctx(), r);
2256 }
2257 inline expr lambda(expr_vector const & xs, expr const & b) {
2258 array<Z3_app> vars(xs);
2259 Z3_ast r = Z3_mk_lambda_const(b.ctx(), vars.size(), vars.ptr(), b); b.check_error(); return expr(b.ctx(), r);
2260 }
2261
2262 inline expr pble(expr_vector const& es, int const* coeffs, int bound) {
2263 assert(es.size() > 0);
2264 context& ctx = es[0].ctx();
2265 array<Z3_ast> _es(es);
2266 Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
2267 ctx.check_error();
2268 return expr(ctx, r);
2269 }
2270 inline expr pbge(expr_vector const& es, int const* coeffs, int bound) {
2271 assert(es.size() > 0);
2272 context& ctx = es[0].ctx();
2273 array<Z3_ast> _es(es);
2274 Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
2275 ctx.check_error();
2276 return expr(ctx, r);
2277 }
2278 inline expr pbeq(expr_vector const& es, int const* coeffs, int bound) {
2279 assert(es.size() > 0);
2280 context& ctx = es[0].ctx();
2281 array<Z3_ast> _es(es);
2282 Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
2283 ctx.check_error();
2284 return expr(ctx, r);
2285 }
2286 inline expr atmost(expr_vector const& es, unsigned bound) {
2287 assert(es.size() > 0);
2288 context& ctx = es[0].ctx();
2289 array<Z3_ast> _es(es);
2290 Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
2291 ctx.check_error();
2292 return expr(ctx, r);
2293 }
2294 inline expr atleast(expr_vector const& es, unsigned bound) {
2295 assert(es.size() > 0);
2296 context& ctx = es[0].ctx();
2297 array<Z3_ast> _es(es);
2298 Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
2299 ctx.check_error();
2300 return expr(ctx, r);
2301 }
2302 inline expr sum(expr_vector const& args) {
2303 assert(args.size() > 0);
2304 context& ctx = args[0].ctx();
2305 array<Z3_ast> _args(args);
2306 Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
2307 ctx.check_error();
2308 return expr(ctx, r);
2309 }
2310
2311 inline expr distinct(expr_vector const& args) {
2312 assert(args.size() > 0);
2313 context& ctx = args[0].ctx();
2314 array<Z3_ast> _args(args);
2315 Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
2316 ctx.check_error();
2317 return expr(ctx, r);
2318 }
2319
2320 inline expr concat(expr const& a, expr const& b) {
2321 check_context(a, b);
2322 Z3_ast r;
2323 if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
2324 Z3_ast _args[2] = { a, b };
2325 r = Z3_mk_seq_concat(a.ctx(), 2, _args);
2326 }
2327 else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
2328 Z3_ast _args[2] = { a, b };
2329 r = Z3_mk_re_concat(a.ctx(), 2, _args);
2330 }
2331 else {
2332 r = Z3_mk_concat(a.ctx(), a, b);
2333 }
2334 a.ctx().check_error();
2335 return expr(a.ctx(), r);
2336 }
2337
2338 inline expr concat(expr_vector const& args) {
2339 Z3_ast r;
2340 assert(args.size() > 0);
2341 if (args.size() == 1) {
2342 return args[0];
2343 }
2344 context& ctx = args[0].ctx();
2345 array<Z3_ast> _args(args);
2346 if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
2347 r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
2348 }
2349 else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
2350 r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
2351 }
2352 else {
2353 r = _args[args.size()-1];
2354 for (unsigned i = args.size()-1; i > 0; ) {
2355 --i;
2356 r = Z3_mk_concat(ctx, _args[i], r);
2357 ctx.check_error();
2358 }
2359 }
2360 ctx.check_error();
2361 return expr(ctx, r);
2362 }
2363
2364 inline expr mk_or(expr_vector const& args) {
2365 array<Z3_ast> _args(args);
2366 Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2367 args.check_error();
2368 return expr(args.ctx(), r);
2369 }
2370 inline expr mk_and(expr_vector const& args) {
2371 array<Z3_ast> _args(args);
2372 Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2373 args.check_error();
2374 return expr(args.ctx(), r);
2375 }
2376
2377
2378 class func_entry : public object {
2379 Z3_func_entry m_entry;
2380 void init(Z3_func_entry e) {
2381 m_entry = e;
2382 Z3_func_entry_inc_ref(ctx(), m_entry);
2383 }
2384 public:
2385 func_entry(context & c, Z3_func_entry e):object(c) { init(e); }
2386 func_entry(func_entry const & s):object(s) { init(s.m_entry); }
2388 operator Z3_func_entry() const { return m_entry; }
2390 Z3_func_entry_inc_ref(s.ctx(), s.m_entry);
2391 Z3_func_entry_dec_ref(ctx(), m_entry);
2392 object::operator=(s);
2393 m_entry = s.m_entry;
2394 return *this;
2395 }
2396 expr value() const { Z3_ast r = Z3_func_entry_get_value(ctx(), m_entry); check_error(); return expr(ctx(), r); }
2397 unsigned num_args() const { unsigned r = Z3_func_entry_get_num_args(ctx(), m_entry); check_error(); return r; }
2398 expr arg(unsigned i) const { Z3_ast r = Z3_func_entry_get_arg(ctx(), m_entry, i); check_error(); return expr(ctx(), r); }
2399 };
2400
2401 class func_interp : public object {
2402 Z3_func_interp m_interp;
2403 void init(Z3_func_interp e) {
2404 m_interp = e;
2405 Z3_func_interp_inc_ref(ctx(), m_interp);
2406 }
2407 public:
2408 func_interp(context & c, Z3_func_interp e):object(c) { init(e); }
2409 func_interp(func_interp const & s):object(s) { init(s.m_interp); }
2411 operator Z3_func_interp() const { return m_interp; }
2413 Z3_func_interp_inc_ref(s.ctx(), s.m_interp);
2414 Z3_func_interp_dec_ref(ctx(), m_interp);
2415 object::operator=(s);
2416 m_interp = s.m_interp;
2417 return *this;
2418 }
2419 expr else_value() const { Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), r); }
2420 unsigned num_entries() const { unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }
2421 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); }
2422 void add_entry(expr_vector const& args, expr& value) {
2423 Z3_func_interp_add_entry(ctx(), m_interp, args, value);
2424 check_error();
2425 }
2426 void set_else(expr& value) {
2427 Z3_func_interp_set_else(ctx(), m_interp, value);
2428 check_error();
2429 }
2430 };
2431
2432 class model : public object {
2433 Z3_model m_model;
2434 void init(Z3_model m) {
2435 m_model = m;
2436 Z3_model_inc_ref(ctx(), m);
2437 }
2438 public:
2439 struct translate {};
2440 model(context & c):object(c) { init(Z3_mk_model(c)); }
2441 model(context & c, Z3_model m):object(c) { init(m); }
2442 model(model const & s):object(s) { init(s.m_model); }
2443 model(model& src, context& dst, translate) : object(dst) { init(Z3_model_translate(src.ctx(), src, dst)); }
2444 ~model() { Z3_model_dec_ref(ctx(), m_model); }
2445 operator Z3_model() const { return m_model; }
2446 model & operator=(model const & s) {
2447 Z3_model_inc_ref(s.ctx(), s.m_model);
2448 Z3_model_dec_ref(ctx(), m_model);
2449 object::operator=(s);
2450 m_model = s.m_model;
2451 return *this;
2452 }
2453
2454 expr eval(expr const & n, bool model_completion=false) const {
2455 check_context(*this, n);
2456 Z3_ast r = 0;
2457 bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
2458 check_error();
2459 if (status == false && ctx().enable_exceptions())
2460 Z3_THROW(exception("failed to evaluate expression"));
2461 return expr(ctx(), r);
2462 }
2463
2464 unsigned num_consts() const { return Z3_model_get_num_consts(ctx(), m_model); }
2465 unsigned num_funcs() const { return Z3_model_get_num_funcs(ctx(), m_model); }
2466 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); }
2467 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); }
2468 unsigned size() const { return num_consts() + num_funcs(); }
2469 func_decl operator[](int i) const {
2470 assert(0 <= i);
2471 return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
2472 }
2473
2474 // returns interpretation of constant declaration c.
2475 // If c is not assigned any value in the model it returns
2476 // an expression with a null ast reference.
2478 check_context(*this, c);
2479 Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);
2480 check_error();
2481 return expr(ctx(), r);
2482 }
2484 check_context(*this, f);
2485 Z3_func_interp r = Z3_model_get_func_interp(ctx(), m_model, f);
2486 check_error();
2487 return func_interp(ctx(), r);
2488 }
2489
2490 // returns true iff the model contains an interpretation
2491 // for function f.
2492 bool has_interp(func_decl f) const {
2493 check_context(*this, f);
2494 return Z3_model_has_interp(ctx(), m_model, f);
2495 }
2496
2498 Z3_func_interp r = Z3_add_func_interp(ctx(), m_model, f, else_val);
2499 check_error();
2500 return func_interp(ctx(), r);
2501 }
2502
2504 Z3_add_const_interp(ctx(), m_model, f, value);
2505 check_error();
2506 }
2507
2508 friend std::ostream & operator<<(std::ostream & out, model const & m);
2509
2510 std::string to_string() const { return std::string(Z3_model_to_string(ctx(), m_model)); }
2511 };
2512 inline std::ostream & operator<<(std::ostream & out, model const & m) { out << Z3_model_to_string(m.ctx(), m); return out; }
2513
2514 class stats : public object {
2515 Z3_stats m_stats;
2516 void init(Z3_stats e) {
2517 m_stats = e;
2518 Z3_stats_inc_ref(ctx(), m_stats);
2519 }
2520 public:
2521 stats(context & c):object(c), m_stats(0) {}
2522 stats(context & c, Z3_stats e):object(c) { init(e); }
2523 stats(stats const & s):object(s) { init(s.m_stats); }
2524 ~stats() { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); }
2525 operator Z3_stats() const { return m_stats; }
2526 stats & operator=(stats const & s) {
2527 Z3_stats_inc_ref(s.ctx(), s.m_stats);
2528 if (m_stats) Z3_stats_dec_ref(ctx(), m_stats);
2529 object::operator=(s);
2530 m_stats = s.m_stats;
2531 return *this;
2532 }
2533 unsigned size() const { return Z3_stats_size(ctx(), m_stats); }
2534 std::string key(unsigned i) const { Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; }
2535 bool is_uint(unsigned i) const { bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r; }
2536 bool is_double(unsigned i) const { bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r; }
2537 unsigned uint_value(unsigned i) const { unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; }
2538 double double_value(unsigned i) const { double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
2539 friend std::ostream & operator<<(std::ostream & out, stats const & s);
2540 };
2541 inline std::ostream & operator<<(std::ostream & out, stats const & s) { out << Z3_stats_to_string(s.ctx(), s); return out; }
2542
2543
2544 inline std::ostream & operator<<(std::ostream & out, check_result r) {
2545 if (r == unsat) out << "unsat";
2546 else if (r == sat) out << "sat";
2547 else out << "unknown";
2548 return out;
2549 }
2550
2551
2552 class solver : public object {
2553 Z3_solver m_solver;
2554 void init(Z3_solver s) {
2555 m_solver = s;
2556 Z3_solver_inc_ref(ctx(), s);
2557 }
2558 public:
2559 struct simple {};
2560 struct translate {};
2561 solver(context & c):object(c) { init(Z3_mk_solver(c)); }
2563 solver(context & c, Z3_solver s):object(c) { init(s); }
2564 solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); }
2565 solver(context & c, solver const& src, translate): object(c) { init(Z3_solver_translate(src.ctx(), src, c)); }
2566 solver(solver const & s):object(s) { init(s.m_solver); }
2567 ~solver() { Z3_solver_dec_ref(ctx(), m_solver); }
2568 operator Z3_solver() const { return m_solver; }
2569 solver & operator=(solver const & s) {
2570 Z3_solver_inc_ref(s.ctx(), s.m_solver);
2571 Z3_solver_dec_ref(ctx(), m_solver);
2572 object::operator=(s);
2573 m_solver = s.m_solver;
2574 return *this;
2575 }
2576 void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
2577 void set(char const * k, bool v) { params p(ctx()); p.set(k, v); set(p); }
2578 void set(char const * k, unsigned v) { params p(ctx()); p.set(k, v); set(p); }
2579 void set(char const * k, double v) { params p(ctx()); p.set(k, v); set(p); }
2580 void set(char const * k, symbol const & v) { params p(ctx()); p.set(k, v); set(p); }
2581 void set(char const * k, char const* v) { params p(ctx()); p.set(k, v); set(p); }
2582 void push() { Z3_solver_push(ctx(), m_solver); check_error(); }
2583 void pop(unsigned n = 1) { Z3_solver_pop(ctx(), m_solver, n); check_error(); }
2584 void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); }
2585 void add(expr const & e) { assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); }
2586 void add(expr const & e, expr const & p) {
2587 assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
2588 Z3_solver_assert_and_track(ctx(), m_solver, e, p);
2589 check_error();
2590 }
2591 void add(expr const & e, char const * p) {
2592 add(e, ctx().bool_const(p));
2593 }
2594 void add(expr_vector const& v) {
2595 check_context(*this, v);
2596 for (unsigned i = 0; i < v.size(); ++i)
2597 add(v[i]);
2598 }
2599 void from_file(char const* file) { Z3_solver_from_file(ctx(), m_solver, file); ctx().check_parser_error(); }
2600 void from_string(char const* s) { Z3_solver_from_string(ctx(), m_solver, s); ctx().check_parser_error(); }
2601
2603 check_result check(unsigned n, expr * const assumptions) {
2604 array<Z3_ast> _assumptions(n);
2605 for (unsigned i = 0; i < n; i++) {
2606 check_context(*this, assumptions[i]);
2607 _assumptions[i] = assumptions[i];
2608 }
2609 Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
2610 check_error();
2611 return to_check_result(r);
2612 }
2613 check_result check(expr_vector const& assumptions) {
2614 unsigned n = assumptions.size();
2615 array<Z3_ast> _assumptions(n);
2616 for (unsigned i = 0; i < n; i++) {
2617 check_context(*this, assumptions[i]);
2618 _assumptions[i] = assumptions[i];
2619 }
2620 Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
2621 check_error();
2622 return to_check_result(r);
2623 }
2624 model get_model() const { Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }
2626 Z3_lbool r = Z3_solver_get_consequences(ctx(), m_solver, assumptions, vars, conseq);
2627 check_error();
2628 return to_check_result(r);
2629 }
2630 std::string reason_unknown() const { Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }
2631 stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }
2632 expr_vector unsat_core() const { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2633 expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2634 expr_vector non_units() const { Z3_ast_vector r = Z3_solver_get_non_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2635 expr_vector units() const { Z3_ast_vector r = Z3_solver_get_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2636 expr_vector trail() const { Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
2638 Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver);
2639 check_error();
2640 expr_vector result(ctx(), r);
2641 unsigned sz = result.size();
2642 levels.resize(sz);
2643 Z3_solver_get_levels(ctx(), m_solver, r, sz, levels.ptr());
2644 check_error();
2645 return result;
2646 }
2647 expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
2648 friend std::ostream & operator<<(std::ostream & out, solver const & s);
2649
2650 std::string to_smt2(char const* status = "unknown") {
2652 Z3_ast const* fmls = es.ptr();
2653 Z3_ast fml = 0;
2654 unsigned sz = es.size();
2655 if (sz > 0) {
2656 --sz;
2657 fml = fmls[sz];
2658 }
2659 else {
2660 fml = ctx().bool_val(true);
2661 }
2662 return std::string(Z3_benchmark_to_smtlib_string(
2663 ctx(),
2664 "", "", status, "",
2665 sz,
2666 fmls,
2667 fml));
2668 }
2669
2670 std::string dimacs(bool include_names = true) const { return std::string(Z3_solver_to_dimacs_string(ctx(), m_solver, include_names)); }
2671
2673
2674
2675 expr_vector cube(expr_vector& vars, unsigned cutoff) {
2676 Z3_ast_vector r = Z3_solver_cube(ctx(), m_solver, vars, cutoff);
2677 check_error();
2678 return expr_vector(ctx(), r);
2679 }
2680
2682 solver& m_solver;
2683 unsigned& m_cutoff;
2684 expr_vector& m_vars;
2685 expr_vector m_cube;
2686 bool m_end;
2687 bool m_empty;
2688
2689 void inc() {
2690 assert(!m_end && !m_empty);
2691 m_cube = m_solver.cube(m_vars, m_cutoff);
2692 m_cutoff = 0xFFFFFFFF;
2693 if (m_cube.size() == 1 && m_cube[0].is_false()) {
2694 m_cube = z3::expr_vector(m_solver.ctx());
2695 m_end = true;
2696 }
2697 else if (m_cube.empty()) {
2698 m_empty = true;
2699 }
2700 }
2701 public:
2702 cube_iterator(solver& s, expr_vector& vars, unsigned& cutoff, bool end):
2703 m_solver(s),
2704 m_cutoff(cutoff),
2705 m_vars(vars),
2706 m_cube(s.ctx()),
2707 m_end(end),
2708 m_empty(false) {
2709 if (!m_end) {
2710 inc();
2711 }
2712 }
2713
2715 assert(!m_end);
2716 if (m_empty) {
2717 m_end = true;
2718 }
2719 else {
2720 inc();
2721 }
2722 return *this;
2723 }
2724 cube_iterator operator++(int) { assert(false); return *this; }
2725 expr_vector const * operator->() const { return &(operator*()); }
2726 expr_vector const& operator*() const noexcept { return m_cube; }
2727
2728 bool operator==(cube_iterator const& other) noexcept {
2729 return other.m_end == m_end;
2730 };
2731 bool operator!=(cube_iterator const& other) noexcept {
2732 return other.m_end != m_end;
2733 };
2734
2735 };
2736
2738 solver& m_solver;
2739 unsigned m_cutoff;
2740 expr_vector m_default_vars;
2741 expr_vector& m_vars;
2742 public:
2744 m_solver(s),
2745 m_cutoff(0xFFFFFFFF),
2746 m_default_vars(s.ctx()),
2747 m_vars(m_default_vars)
2748 {}
2749
2751 m_solver(s),
2752 m_cutoff(0xFFFFFFFF),
2753 m_default_vars(s.ctx()),
2754 m_vars(vars)
2755 {}
2756
2757 cube_iterator begin() { return cube_iterator(m_solver, m_vars, m_cutoff, false); }
2758 cube_iterator end() { return cube_iterator(m_solver, m_vars, m_cutoff, true); }
2759 void set_cutoff(unsigned c) noexcept { m_cutoff = c; }
2760 };
2761
2763 cube_generator cubes(expr_vector& vars) { return cube_generator(*this, vars); }
2764
2765 };
2766 inline std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
2767
2768 class goal : public object {
2769 Z3_goal m_goal;
2770 void init(Z3_goal s) {
2771 m_goal = s;
2772 Z3_goal_inc_ref(ctx(), s);
2773 }
2774 public:
2775 goal(context & c, bool models=true, bool unsat_cores=false, bool proofs=false):object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); }
2776 goal(context & c, Z3_goal s):object(c) { init(s); }
2777 goal(goal const & s):object(s) { init(s.m_goal); }
2778 ~goal() { Z3_goal_dec_ref(ctx(), m_goal); }
2779 operator Z3_goal() const { return m_goal; }
2780 goal & operator=(goal const & s) {
2781 Z3_goal_inc_ref(s.ctx(), s.m_goal);
2782 Z3_goal_dec_ref(ctx(), m_goal);
2783 object::operator=(s);
2784 m_goal = s.m_goal;
2785 return *this;
2786 }
2787 void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
2788 void add(expr_vector const& v) { check_context(*this, v); for (unsigned i = 0; i < v.size(); ++i) add(v[i]); }
2789 unsigned size() const { return Z3_goal_size(ctx(), m_goal); }
2790 expr operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
2791 Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); }
2792 bool inconsistent() const { return Z3_goal_inconsistent(ctx(), m_goal); }
2793 unsigned depth() const { return Z3_goal_depth(ctx(), m_goal); }
2794 void reset() { Z3_goal_reset(ctx(), m_goal); }
2795 unsigned num_exprs() const { return Z3_goal_num_exprs(ctx(), m_goal); }
2796 bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal); }
2797 bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal); }
2798 model convert_model(model const & m) const {
2799 check_context(*this, m);
2800 Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, m);
2801 check_error();
2802 return model(ctx(), new_m);
2803 }
2805 Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, 0);
2806 check_error();
2807 return model(ctx(), new_m);
2808 }
2809 expr as_expr() const {
2810 unsigned n = size();
2811 if (n == 0)
2812 return ctx().bool_val(true);
2813 else if (n == 1)
2814 return operator[](0);
2815 else {
2816 array<Z3_ast> args(n);
2817 for (unsigned i = 0; i < n; i++)
2818 args[i] = operator[](i);
2819 return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
2820 }
2821 }
2822 std::string dimacs(bool include_names = true) const { return std::string(Z3_goal_to_dimacs_string(ctx(), m_goal, include_names)); }
2823 friend std::ostream & operator<<(std::ostream & out, goal const & g);
2824 };
2825 inline std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; }
2826
2827 class apply_result : public object {
2828 Z3_apply_result m_apply_result;
2829 void init(Z3_apply_result s) {
2830 m_apply_result = s;
2832 }
2833 public:
2834 apply_result(context & c, Z3_apply_result s):object(c) { init(s); }
2835 apply_result(apply_result const & s):object(s) { init(s.m_apply_result); }
2837 operator Z3_apply_result() const { return m_apply_result; }
2839 Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result);
2840 Z3_apply_result_dec_ref(ctx(), m_apply_result);
2841 object::operator=(s);
2842 m_apply_result = s.m_apply_result;
2843 return *this;
2844 }
2845 unsigned size() const { return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); }
2846 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); }
2847 friend std::ostream & operator<<(std::ostream & out, apply_result const & r);
2848 };
2849 inline std::ostream & operator<<(std::ostream & out, apply_result const & r) { out << Z3_apply_result_to_string(r.ctx(), r); return out; }
2850
2851 class tactic : public object {
2852 Z3_tactic m_tactic;
2853 void init(Z3_tactic s) {
2854 m_tactic = s;
2855 Z3_tactic_inc_ref(ctx(), s);
2856 }
2857 public:
2858 tactic(context & c, char const * name):object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); }
2859 tactic(context & c, Z3_tactic s):object(c) { init(s); }
2860 tactic(tactic const & s):object(s) { init(s.m_tactic); }
2861 ~tactic() { Z3_tactic_dec_ref(ctx(), m_tactic); }
2862 operator Z3_tactic() const { return m_tactic; }
2863 tactic & operator=(tactic const & s) {
2864 Z3_tactic_inc_ref(s.ctx(), s.m_tactic);
2865 Z3_tactic_dec_ref(ctx(), m_tactic);
2866 object::operator=(s);
2867 m_tactic = s.m_tactic;
2868 return *this;
2869 }
2870 solver mk_solver() const { Z3_solver r = Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error(); return solver(ctx(), r); }
2871 apply_result apply(goal const & g) const {
2872 check_context(*this, g);
2873 Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g);
2874 check_error();
2875 return apply_result(ctx(), r);
2876 }
2877 apply_result operator()(goal const & g) const {
2878 return apply(g);
2879 }
2880 std::string help() const { char const * r = Z3_tactic_get_help(ctx(), m_tactic); check_error(); return r; }
2881 friend tactic operator&(tactic const & t1, tactic const & t2);
2882 friend tactic operator|(tactic const & t1, tactic const & t2);
2883 friend tactic repeat(tactic const & t, unsigned max);
2884 friend tactic with(tactic const & t, params const & p);
2885 friend tactic try_for(tactic const & t, unsigned ms);
2886 friend tactic par_or(unsigned n, tactic const* tactics);
2887 friend tactic par_and_then(tactic const& t1, tactic const& t2);
2889 };
2890
2891 inline tactic operator&(tactic const & t1, tactic const & t2) {
2892 check_context(t1, t2);
2893 Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
2894 t1.check_error();
2895 return tactic(t1.ctx(), r);
2896 }
2897
2898 inline tactic operator|(tactic const & t1, tactic const & t2) {
2899 check_context(t1, t2);
2900 Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
2901 t1.check_error();
2902 return tactic(t1.ctx(), r);
2903 }
2904
2905 inline tactic repeat(tactic const & t, unsigned max=UINT_MAX) {
2906 Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
2907 t.check_error();
2908 return tactic(t.ctx(), r);
2909 }
2910
2911 inline tactic with(tactic const & t, params const & p) {
2912 Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
2913 t.check_error();
2914 return tactic(t.ctx(), r);
2915 }
2916 inline tactic try_for(tactic const & t, unsigned ms) {
2917 Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
2918 t.check_error();
2919 return tactic(t.ctx(), r);
2920 }
2921 inline tactic par_or(unsigned n, tactic const* tactics) {
2922 if (n == 0) {
2923 Z3_THROW(exception("a non-zero number of tactics need to be passed to par_or"));
2924 }
2925 array<Z3_tactic> buffer(n);
2926 for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
2927 return tactic(tactics[0].ctx(), Z3_tactic_par_or(tactics[0].ctx(), n, buffer.ptr()));
2928 }
2929
2930 inline tactic par_and_then(tactic const & t1, tactic const & t2) {
2931 check_context(t1, t2);
2932 Z3_tactic r = Z3_tactic_par_and_then(t1.ctx(), t1, t2);
2933 t1.check_error();
2934 return tactic(t1.ctx(), r);
2935 }
2936
2937 class probe : public object {
2938 Z3_probe m_probe;
2939 void init(Z3_probe s) {
2940 m_probe = s;
2941 Z3_probe_inc_ref(ctx(), s);
2942 }
2943 public:
2944 probe(context & c, char const * name):object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); }
2945 probe(context & c, double val):object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); }
2946 probe(context & c, Z3_probe s):object(c) { init(s); }
2947 probe(probe const & s):object(s) { init(s.m_probe); }
2948 ~probe() { Z3_probe_dec_ref(ctx(), m_probe); }
2949 operator Z3_probe() const { return m_probe; }
2950 probe & operator=(probe const & s) {
2951 Z3_probe_inc_ref(s.ctx(), s.m_probe);
2952 Z3_probe_dec_ref(ctx(), m_probe);
2953 object::operator=(s);
2954 m_probe = s.m_probe;
2955 return *this;
2956 }
2957 double apply(goal const & g) const { double r = Z3_probe_apply(ctx(), m_probe, g); check_error(); return r; }
2958 double operator()(goal const & g) const { return apply(g); }
2959 friend probe operator<=(probe const & p1, probe const & p2);
2960 friend probe operator<=(probe const & p1, double p2);
2961 friend probe operator<=(double p1, probe const & p2);
2962 friend probe operator>=(probe const & p1, probe const & p2);
2963 friend probe operator>=(probe const & p1, double p2);
2964 friend probe operator>=(double p1, probe const & p2);
2965 friend probe operator<(probe const & p1, probe const & p2);
2966 friend probe operator<(probe const & p1, double p2);
2967 friend probe operator<(double p1, probe const & p2);
2968 friend probe operator>(probe const & p1, probe const & p2);
2969 friend probe operator>(probe const & p1, double p2);
2970 friend probe operator>(double p1, probe const & p2);
2971 friend probe operator==(probe const & p1, probe const & p2);
2972 friend probe operator==(probe const & p1, double p2);
2973 friend probe operator==(double p1, probe const & p2);
2974 friend probe operator&&(probe const & p1, probe const & p2);
2975 friend probe operator||(probe const & p1, probe const & p2);
2976 friend probe operator!(probe const & p);
2977 };
2978
2979 inline probe operator<=(probe const & p1, probe const & p2) {
2980 check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2981 }
2982 inline probe operator<=(probe const & p1, double p2) { return p1 <= probe(p1.ctx(), p2); }
2983 inline probe operator<=(double p1, probe const & p2) { return probe(p2.ctx(), p1) <= p2; }
2984 inline probe operator>=(probe const & p1, probe const & p2) {
2985 check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2986 }
2987 inline probe operator>=(probe const & p1, double p2) { return p1 >= probe(p1.ctx(), p2); }
2988 inline probe operator>=(double p1, probe const & p2) { return probe(p2.ctx(), p1) >= p2; }
2989 inline probe operator<(probe const & p1, probe const & p2) {
2990 check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2991 }
2992 inline probe operator<(probe const & p1, double p2) { return p1 < probe(p1.ctx(), p2); }
2993 inline probe operator<(double p1, probe const & p2) { return probe(p2.ctx(), p1) < p2; }
2994 inline probe operator>(probe const & p1, probe const & p2) {
2995 check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2996 }
2997 inline probe operator>(probe const & p1, double p2) { return p1 > probe(p1.ctx(), p2); }
2998 inline probe operator>(double p1, probe const & p2) { return probe(p2.ctx(), p1) > p2; }
2999 inline probe operator==(probe const & p1, probe const & p2) {
3000 check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3001 }
3002 inline probe operator==(probe const & p1, double p2) { return p1 == probe(p1.ctx(), p2); }
3003 inline probe operator==(double p1, probe const & p2) { return probe(p2.ctx(), p1) == p2; }
3004 inline probe operator&&(probe const & p1, probe const & p2) {
3005 check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3006 }
3007 inline probe operator||(probe const & p1, probe const & p2) {
3008 check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3009 }
3010 inline probe operator!(probe const & p) {
3011 Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
3012 }
3013
3014 class optimize : public object {
3015 Z3_optimize m_opt;
3016
3017 public:
3018 class handle final {
3019 unsigned m_h;
3020 public:
3021 handle(unsigned h): m_h(h) {}
3022 unsigned h() const { return m_h; }
3023 };
3025 optimize(optimize const & o):object(o), m_opt(o.m_opt) {
3026 Z3_optimize_inc_ref(o.ctx(), o.m_opt);
3027 }
3029 m_opt = Z3_mk_optimize(c);
3030 Z3_optimize_inc_ref(c, m_opt);
3031 add(expr_vector(c, src.assertions()));
3032 expr_vector v(c, src.objectives());
3033 for (expr_vector::iterator it = v.begin(); it != v.end(); ++it) minimize(*it);
3034 }
3036 Z3_optimize_inc_ref(o.ctx(), o.m_opt);
3037 Z3_optimize_dec_ref(ctx(), m_opt);
3038 m_opt = o.m_opt;
3039 object::operator=(o);
3040 return *this;
3041 }
3043 operator Z3_optimize() const { return m_opt; }
3044 void add(expr const& e) {
3045 assert(e.is_bool());
3046 Z3_optimize_assert(ctx(), m_opt, e);
3047 }
3048 void add(expr_vector const& es) {
3049 for (expr_vector::iterator it = es.begin(); it != es.end(); ++it) add(*it);
3050 }
3051 void add(expr const& e, expr const& t) {
3052 assert(e.is_bool());
3053 Z3_optimize_assert_and_track(ctx(), m_opt, e, t);
3054 }
3055 void add(expr const& e, char const* p) {
3056 assert(e.is_bool());
3057 add(e, ctx().bool_const(p));
3058 }
3059 handle add_soft(expr const& e, unsigned weight) {
3060 assert(e.is_bool());
3061 auto str = std::to_string(weight);
3062 return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, str.c_str(), 0));
3063 }
3064 handle add_soft(expr const& e, char const* weight) {
3065 assert(e.is_bool());
3066 return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0));
3067 }
3068 handle add(expr const& e, unsigned weight) {
3069 return add_soft(e, weight);
3070 }
3072 return handle(Z3_optimize_maximize(ctx(), m_opt, e));
3073 }
3075 return handle(Z3_optimize_minimize(ctx(), m_opt, e));
3076 }
3077 void push() {
3078 Z3_optimize_push(ctx(), m_opt);
3079 }
3080 void pop() {
3081 Z3_optimize_pop(ctx(), m_opt);
3082 }
3085 unsigned n = asms.size();
3086 array<Z3_ast> _asms(n);
3087 for (unsigned i = 0; i < n; i++) {
3088 check_context(*this, asms[i]);
3089 _asms[i] = asms[i];
3090 }
3091 Z3_lbool r = Z3_optimize_check(ctx(), m_opt, n, _asms.ptr());
3092 check_error();
3093 return to_check_result(r);
3094 }
3095 model get_model() const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }
3096 expr_vector unsat_core() const { Z3_ast_vector r = Z3_optimize_get_unsat_core(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
3097 void set(params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }
3098 expr lower(handle const& h) {
3099 Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());
3100 check_error();
3101 return expr(ctx(), r);
3102 }
3103 expr upper(handle const& h) {
3104 Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h());
3105 check_error();
3106 return expr(ctx(), r);
3107 }
3108 expr_vector assertions() const { Z3_ast_vector r = Z3_optimize_get_assertions(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
3109 expr_vector objectives() const { Z3_ast_vector r = Z3_optimize_get_objectives(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
3110 stats statistics() const { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); }
3111 friend std::ostream & operator<<(std::ostream & out, optimize const & s);
3112 void from_file(char const* filename) { Z3_optimize_from_file(ctx(), m_opt, filename); check_error(); }
3113 void from_string(char const* constraints) { Z3_optimize_from_string(ctx(), m_opt, constraints); check_error(); }
3114 std::string help() const { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error(); return r; }
3115 };
3116 inline std::ostream & operator<<(std::ostream & out, optimize const & s) { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }
3117
3118 class fixedpoint : public object {
3119 Z3_fixedpoint m_fp;
3120 public:
3122 fixedpoint(fixedpoint const & o):object(o), m_fp(o.m_fp) { Z3_fixedpoint_inc_ref(ctx(), m_fp); }
3125 Z3_fixedpoint_inc_ref(o.ctx(), o.m_fp);
3126 Z3_fixedpoint_dec_ref(ctx(), m_fp);
3127 m_fp = o.m_fp;
3128 object::operator=(o);
3129 return *this;
3130 }
3131 operator Z3_fixedpoint() const { return m_fp; }
3132 expr_vector from_string(char const* s) {
3133 Z3_ast_vector r = Z3_fixedpoint_from_string(ctx(), m_fp, s);
3134 check_error();
3135 return expr_vector(ctx(), r);
3136 }
3137 expr_vector from_file(char const* s) {
3138 Z3_ast_vector r = Z3_fixedpoint_from_file(ctx(), m_fp, s);
3139 check_error();
3140 return expr_vector(ctx(), r);
3141 }
3142 void add_rule(expr& rule, symbol const& name) { Z3_fixedpoint_add_rule(ctx(), m_fp, rule, name); check_error(); }
3143 void add_fact(func_decl& f, unsigned * args) { Z3_fixedpoint_add_fact(ctx(), m_fp, f, f.arity(), args); check_error(); }
3146 array<Z3_func_decl> rs(relations);
3147 Z3_lbool r = Z3_fixedpoint_query_relations(ctx(), m_fp, rs.size(), rs.ptr());
3148 check_error();
3149 return to_check_result(r);
3150 }
3151 expr get_answer() { Z3_ast r = Z3_fixedpoint_get_answer(ctx(), m_fp); check_error(); return expr(ctx(), r); }
3152 std::string reason_unknown() { return Z3_fixedpoint_get_reason_unknown(ctx(), m_fp); }
3153 void update_rule(expr& rule, symbol const& name) { Z3_fixedpoint_update_rule(ctx(), m_fp, rule, name); check_error(); }
3154 unsigned get_num_levels(func_decl& p) { unsigned r = Z3_fixedpoint_get_num_levels(ctx(), m_fp, p); check_error(); return r; }
3156 Z3_ast r = Z3_fixedpoint_get_cover_delta(ctx(), m_fp, level, p);
3157 check_error();
3158 return expr(ctx(), r);
3159 }
3160 void add_cover(int level, func_decl& p, expr& property) { Z3_fixedpoint_add_cover(ctx(), m_fp, level, p, property); check_error(); }
3161 stats statistics() const { Z3_stats r = Z3_fixedpoint_get_statistics(ctx(), m_fp); check_error(); return stats(ctx(), r); }
3163 expr_vector assertions() const { Z3_ast_vector r = Z3_fixedpoint_get_assertions(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
3164 expr_vector rules() const { Z3_ast_vector r = Z3_fixedpoint_get_rules(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); }
3165 void set(params const & p) { Z3_fixedpoint_set_params(ctx(), m_fp, p); check_error(); }
3166 std::string help() const { return Z3_fixedpoint_get_help(ctx(), m_fp); }
3168 std::string to_string() { return Z3_fixedpoint_to_string(ctx(), m_fp, 0, 0); }
3169 std::string to_string(expr_vector const& queries) {
3170 array<Z3_ast> qs(queries);
3171 return Z3_fixedpoint_to_string(ctx(), m_fp, qs.size(), qs.ptr());
3172 }
3173 };
3174 inline std::ostream & operator<<(std::ostream & out, fixedpoint const & f) { return out << Z3_fixedpoint_to_string(f.ctx(), f, 0, 0); }
3175
3176 inline tactic fail_if(probe const & p) {
3177 Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
3178 p.check_error();
3179 return tactic(p.ctx(), r);
3180 }
3181 inline tactic when(probe const & p, tactic const & t) {
3182 check_context(p, t);
3183 Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
3184 t.check_error();
3185 return tactic(t.ctx(), r);
3186 }
3187 inline tactic cond(probe const & p, tactic const & t1, tactic const & t2) {
3188 check_context(p, t1); check_context(p, t2);
3189 Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
3190 t1.check_error();
3191 return tactic(t1.ctx(), r);
3192 }
3193
3194 inline symbol context::str_symbol(char const * s) { Z3_symbol r = Z3_mk_string_symbol(m_ctx, s); check_error(); return symbol(*this, r); }
3195 inline symbol context::int_symbol(int n) { Z3_symbol r = Z3_mk_int_symbol(m_ctx, n); check_error(); return symbol(*this, r); }
3196
3197 inline sort context::bool_sort() { Z3_sort s = Z3_mk_bool_sort(m_ctx); check_error(); return sort(*this, s); }
3198 inline sort context::int_sort() { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }
3199 inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
3200 inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
3201 inline sort context::string_sort() { Z3_sort s = Z3_mk_string_sort(m_ctx); check_error(); return sort(*this, s); }
3202 inline sort context::seq_sort(sort& s) { Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); }
3203 inline sort context::re_sort(sort& s) { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
3204 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); }
3205
3206 template<>
3207 inline sort context::fpa_sort<16>() { return fpa_sort(5, 11); }
3208
3209 template<>
3210 inline sort context::fpa_sort<32>() { return fpa_sort(8, 24); }
3211
3212 template<>
3213 inline sort context::fpa_sort<64>() { return fpa_sort(11, 53); }
3214
3215 template<>
3216 inline sort context::fpa_sort<128>() { return fpa_sort(15, 113); }
3217
3218 inline sort context::fpa_rounding_mode_sort() { Z3_sort r = Z3_mk_fpa_rounding_mode_sort(m_ctx); check_error(); return sort(*this, r); }
3219
3220 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); }
3222 array<Z3_sort> dom(d);
3223 Z3_sort s = Z3_mk_array_sort_n(m_ctx, dom.size(), dom.ptr(), r); check_error(); return sort(*this, s);
3224 }
3225 inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
3226 array<Z3_symbol> _enum_names(n);
3227 for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
3228 array<Z3_func_decl> _cs(n);
3229 array<Z3_func_decl> _ts(n);
3230 Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3231 sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
3232 check_error();
3233 for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
3234 return s;
3235 }
3236 inline func_decl context::tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs) {
3237 array<Z3_symbol> _names(n);
3238 array<Z3_sort> _sorts(n);
3239 for (unsigned i = 0; i < n; i++) { _names[i] = Z3_mk_string_symbol(*this, names[i]); _sorts[i] = sorts[i]; }
3240 array<Z3_func_decl> _projs(n);
3241 Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3242 Z3_func_decl tuple;
3243 sort _ignore_s = to_sort(*this, Z3_mk_tuple_sort(*this, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));
3244 check_error();
3245 for (unsigned i = 0; i < n; i++) { projs.push_back(func_decl(*this, _projs[i])); }
3246 return func_decl(*this, tuple);
3247 }
3248
3249 inline sort context::uninterpreted_sort(char const* name) {
3250 Z3_symbol _name = Z3_mk_string_symbol(*this, name);
3251 return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
3252 }
3254 return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
3255 }
3256
3257 inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3258 array<Z3_sort> args(arity);
3259 for (unsigned i = 0; i < arity; i++) {
3260 check_context(domain[i], range);
3261 args[i] = domain[i];
3262 }
3263 Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
3264 check_error();
3265 return func_decl(*this, f);
3266 }
3267
3268 inline func_decl context::function(char const * name, unsigned arity, sort const * domain, sort const & range) {
3269 return function(range.ctx().str_symbol(name), arity, domain, range);
3270 }
3271
3272 inline func_decl context::function(symbol const& name, sort_vector const& domain, sort const& range) {
3273 array<Z3_sort> args(domain.size());
3274 for (unsigned i = 0; i < domain.size(); i++) {
3275 check_context(domain[i], range);
3276 args[i] = domain[i];
3277 }
3278 Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
3279 check_error();
3280 return func_decl(*this, f);
3281 }
3282
3283 inline func_decl context::function(char const * name, sort_vector const& domain, sort const& range) {
3284 return function(range.ctx().str_symbol(name), domain, range);
3285 }
3286
3287
3288 inline func_decl context::function(char const * name, sort const & domain, sort const & range) {
3289 check_context(domain, range);
3290 Z3_sort args[1] = { domain };
3291 Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
3292 check_error();
3293 return func_decl(*this, f);
3294 }
3295
3296 inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & range) {
3298 Z3_sort args[2] = { d1, d2 };
3299 Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
3300 check_error();
3301 return func_decl(*this, f);
3302 }
3303
3304 inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
3306 Z3_sort args[3] = { d1, d2, d3 };
3307 Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
3308 check_error();
3309 return func_decl(*this, f);
3310 }
3311
3312 inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
3314 Z3_sort args[4] = { d1, d2, d3, d4 };
3315 Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
3316 check_error();
3317 return func_decl(*this, f);
3318 }
3319
3320 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) {
3322 Z3_sort args[5] = { d1, d2, d3, d4, d5 };
3323 Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
3324 check_error();
3325 return func_decl(*this, f);
3326 }
3327
3328 inline func_decl context::recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3329 array<Z3_sort> args(arity);
3330 for (unsigned i = 0; i < arity; i++) {
3331 check_context(domain[i], range);
3332 args[i] = domain[i];
3333 }
3334 Z3_func_decl f = Z3_mk_rec_func_decl(m_ctx, name, arity, args.ptr(), range);
3335 check_error();
3336 return func_decl(*this, f);
3337
3338 }
3339
3340 inline func_decl context::recfun(char const * name, unsigned arity, sort const * domain, sort const & range) {
3341 return recfun(str_symbol(name), arity, domain, range);
3342 }
3343
3344 inline func_decl context::recfun(char const * name, sort const& d1, sort const & range) {
3345 return recfun(str_symbol(name), 1, &d1, range);
3346 }
3347
3348 inline func_decl context::recfun(char const * name, sort const& d1, sort const& d2, sort const & range) {
3349 sort dom[2] = { d1, d2 };
3350 return recfun(str_symbol(name), 2, dom, range);
3351 }
3352
3353 inline void context::recdef(func_decl f, expr_vector const& args, expr const& body) {
3354 check_context(f, args); check_context(f, body);
3355 array<Z3_ast> vars(args);
3356 Z3_add_rec_def(f.ctx(), f, vars.size(), vars.ptr(), body);
3357 }
3358
3359 inline expr context::constant(symbol const & name, sort const & s) {
3360 Z3_ast r = Z3_mk_const(m_ctx, name, s);
3361 check_error();
3362 return expr(*this, r);
3363 }
3364 inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); }
3365 inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); }
3366 inline expr context::int_const(char const * name) { return constant(name, int_sort()); }
3367 inline expr context::real_const(char const * name) { return constant(name, real_sort()); }
3368 inline expr context::string_const(char const * name) { return constant(name, string_sort()); }
3369 inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); }
3370 inline expr context::fpa_const(char const * name, unsigned ebits, unsigned sbits) { return constant(name, fpa_sort(ebits, sbits)); }
3371
3372 template<size_t precision>
3373 inline expr context::fpa_const(char const * name) { return constant(name, fpa_sort<precision>()); }
3374
3375 inline void context::set_rounding_mode(rounding_mode rm) { m_rounding_mode = rm; }
3376
3378 switch (m_rounding_mode) {
3379 case RNA: return expr(*this, Z3_mk_fpa_rna(m_ctx));
3380 case RNE: return expr(*this, Z3_mk_fpa_rne(m_ctx));
3381 case RTP: return expr(*this, Z3_mk_fpa_rtp(m_ctx));
3382 case RTN: return expr(*this, Z3_mk_fpa_rtn(m_ctx));
3383 case RTZ: return expr(*this, Z3_mk_fpa_rtz(m_ctx));
3384 default: return expr(*this);
3385 }
3386 }
3387
3388 inline expr context::bool_val(bool b) { return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }
3389
3390 inline expr context::int_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
3391 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); }
3392 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); }
3393 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); }
3394 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); }
3395
3396 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); }
3397 inline expr context::real_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
3398 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); }
3399 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); }
3400 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); }
3401 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); }
3402
3403 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); }
3404 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); }
3405 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); }
3406 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); }
3407 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); }
3408 inline expr context::bv_val(unsigned n, bool const* bits) {
3409 array<bool> _bits(n);
3410 for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
3411 Z3_ast r = Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error(); return expr(*this, r);
3412 }
3413
3414 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); }
3415 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); }
3416 inline expr context::fpa_nan(sort const & s) { Z3_ast r = Z3_mk_fpa_nan(m_ctx, s); check_error(); return expr(*this, r); }
3417 inline expr context::fpa_inf(sort const & s, bool sgn) { Z3_ast r = Z3_mk_fpa_inf(m_ctx, s, sgn); check_error(); return expr(*this, r); }
3418
3419 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); }
3420 inline expr context::string_val(char const* s) { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
3421 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); }
3422
3423 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); }
3424
3425 inline expr func_decl::operator()(unsigned n, expr const * args) const {
3426 array<Z3_ast> _args(n);
3427 for (unsigned i = 0; i < n; i++) {
3428 check_context(*this, args[i]);
3429 _args[i] = args[i];
3430 }
3431 Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
3432 check_error();
3433 return expr(ctx(), r);
3434
3435 }
3436 inline expr func_decl::operator()(expr_vector const& args) const {
3437 array<Z3_ast> _args(args.size());
3438 for (unsigned i = 0; i < args.size(); i++) {
3439 check_context(*this, args[i]);
3440 _args[i] = args[i];
3441 }
3442 Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
3443 check_error();
3444 return expr(ctx(), r);
3445 }
3447 Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
3448 ctx().check_error();
3449 return expr(ctx(), r);
3450 }
3451 inline expr func_decl::operator()(expr const & a) const {
3452 check_context(*this, a);
3453 Z3_ast args[1] = { a };
3454 Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3455 ctx().check_error();
3456 return expr(ctx(), r);
3457 }
3458 inline expr func_decl::operator()(int a) const {
3459 Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
3460 Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3461 ctx().check_error();
3462 return expr(ctx(), r);
3463 }
3464 inline expr func_decl::operator()(expr const & a1, expr const & a2) const {
3465 check_context(*this, a1); check_context(*this, a2);
3466 Z3_ast args[2] = { a1, a2 };
3467 Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3468 ctx().check_error();
3469 return expr(ctx(), r);
3470 }
3471 inline expr func_decl::operator()(expr const & a1, int a2) const {
3472 check_context(*this, a1);
3473 Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
3474 Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3475 ctx().check_error();
3476 return expr(ctx(), r);
3477 }
3478 inline expr func_decl::operator()(int a1, expr const & a2) const {
3479 check_context(*this, a2);
3480 Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
3481 Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3482 ctx().check_error();
3483 return expr(ctx(), r);
3484 }
3485 inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3) const {
3486 check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
3487 Z3_ast args[3] = { a1, a2, a3 };
3488 Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
3489 ctx().check_error();
3490 return expr(ctx(), r);
3491 }
3492 inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const {
3493 check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
3494 Z3_ast args[4] = { a1, a2, a3, a4 };
3495 Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
3496 ctx().check_error();
3497 return expr(ctx(), r);
3498 }
3499 inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const {
3500 check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
3501 Z3_ast args[5] = { a1, a2, a3, a4, a5 };
3502 Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
3503 ctx().check_error();
3504 return expr(ctx(), r);
3505 }
3506
3507 inline expr to_real(expr const & a) { Z3_ast r = Z3_mk_int2real(a.ctx(), a); a.check_error(); return expr(a.ctx(), r); }
3508
3509 inline func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3510 return range.ctx().function(name, arity, domain, range);
3511 }
3512 inline func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range) {
3513 return range.ctx().function(name, arity, domain, range);
3514 }
3515 inline func_decl function(char const * name, sort const & domain, sort const & range) {
3516 return range.ctx().function(name, domain, range);
3517 }
3518 inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range) {
3519 return range.ctx().function(name, d1, d2, range);
3520 }
3521 inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
3522 return range.ctx().function(name, d1, d2, d3, range);
3523 }
3524 inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
3525 return range.ctx().function(name, d1, d2, d3, d4, range);
3526 }
3527 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) {
3528 return range.ctx().function(name, d1, d2, d3, d4, d5, range);
3529 }
3530 inline func_decl function(char const* name, sort_vector const& domain, sort const& range) {
3531 return range.ctx().function(name, domain, range);
3532 }
3533 inline func_decl function(std::string const& name, sort_vector const& domain, sort const& range) {
3534 return range.ctx().function(name.c_str(), domain, range);
3535 }
3536
3537 inline func_decl recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3538 return range.ctx().recfun(name, arity, domain, range);
3539 }
3540 inline func_decl recfun(char const * name, unsigned arity, sort const * domain, sort const & range) {
3541 return range.ctx().recfun(name, arity, domain, range);
3542 }
3543 inline func_decl recfun(char const * name, sort const& d1, sort const & range) {
3544 return range.ctx().recfun(name, d1, range);
3545 }
3546 inline func_decl recfun(char const * name, sort const& d1, sort const& d2, sort const & range) {
3547 return range.ctx().recfun(name, d1, d2, range);
3548 }
3549
3550 inline expr select(expr const & a, expr const & i) {
3551 check_context(a, i);
3552 Z3_ast r = Z3_mk_select(a.ctx(), a, i);
3553 a.check_error();
3554 return expr(a.ctx(), r);
3555 }
3556 inline expr select(expr const & a, int i) {
3557 return select(a, a.ctx().num_val(i, a.get_sort().array_domain()));
3558 }
3559 inline expr select(expr const & a, expr_vector const & i) {
3560 check_context(a, i);
3561 array<Z3_ast> idxs(i);
3562 Z3_ast r = Z3_mk_select_n(a.ctx(), a, idxs.size(), idxs.ptr());
3563 a.check_error();
3564 return expr(a.ctx(), r);
3565 }
3566
3567 inline expr store(expr const & a, expr const & i, expr const & v) {
3568 check_context(a, i); check_context(a, v);
3569 Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
3570 a.check_error();
3571 return expr(a.ctx(), r);
3572 }
3573
3574 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); }
3575 inline expr store(expr const & a, expr i, int v) { return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
3576 inline expr store(expr const & a, int i, int v) {
3577 return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
3578 }
3579 inline expr store(expr const & a, expr_vector const & i, expr const & v) {
3580 check_context(a, i); check_context(a, v);
3581 array<Z3_ast> idxs(i);
3582 Z3_ast r = Z3_mk_store_n(a.ctx(), a, idxs.size(), idxs.ptr(), v);
3583 a.check_error();
3584 return expr(a.ctx(), r);
3585 }
3586
3588 Z3_ast r = Z3_mk_as_array(f.ctx(), f);
3589 f.check_error();
3590 return expr(f.ctx(), r);
3591 }
3592
3593#define MK_EXPR1(_fn, _arg) \
3594 Z3_ast r = _fn(_arg.ctx(), _arg); \
3595 _arg.check_error(); \
3596 return expr(_arg.ctx(), r);
3597
3598#define MK_EXPR2(_fn, _arg1, _arg2) \
3599 check_context(_arg1, _arg2); \
3600 Z3_ast r = _fn(_arg1.ctx(), _arg1, _arg2); \
3601 _arg1.check_error(); \
3602 return expr(_arg1.ctx(), r);
3603
3604 inline expr const_array(sort const & d, expr const & v) {
3606 }
3607
3608 inline expr empty_set(sort const& s) {
3610 }
3611
3612 inline expr full_set(sort const& s) {
3614 }
3615
3616 inline expr set_add(expr const& s, expr const& e) {
3617 MK_EXPR2(Z3_mk_set_add, s, e);
3618 }
3619
3620 inline expr set_del(expr const& s, expr const& e) {
3621 MK_EXPR2(Z3_mk_set_del, s, e);
3622 }
3623
3624 inline expr set_union(expr const& a, expr const& b) {
3625 check_context(a, b);
3626 Z3_ast es[2] = { a, b };
3627 Z3_ast r = Z3_mk_set_union(a.ctx(), 2, es);
3628 a.check_error();
3629 return expr(a.ctx(), r);
3630 }
3631
3632 inline expr set_intersect(expr const& a, expr const& b) {
3633 check_context(a, b);
3634 Z3_ast es[2] = { a, b };
3635 Z3_ast r = Z3_mk_set_intersect(a.ctx(), 2, es);
3636 a.check_error();
3637 return expr(a.ctx(), r);
3638 }
3639
3640 inline expr set_difference(expr const& a, expr const& b) {
3642 }
3643
3644 inline expr set_complement(expr const& a) {
3646 }
3647
3648 inline expr set_member(expr const& s, expr const& e) {
3650 }
3651
3652 inline expr set_subset(expr const& a, expr const& b) {
3654 }
3655
3656 // sequence and regular expression operations.
3657 // union is +
3658 // concat is overloaded to handle sequences and regular expressions
3659
3660 inline expr empty(sort const& s) {
3661 Z3_ast r = Z3_mk_seq_empty(s.ctx(), s);
3662 s.check_error();
3663 return expr(s.ctx(), r);
3664 }
3665 inline expr suffixof(expr const& a, expr const& b) {
3666 check_context(a, b);
3667 Z3_ast r = Z3_mk_seq_suffix(a.ctx(), a, b);
3668 a.check_error();
3669 return expr(a.ctx(), r);
3670 }
3671 inline expr prefixof(expr const& a, expr const& b) {
3672 check_context(a, b);
3673 Z3_ast r = Z3_mk_seq_prefix(a.ctx(), a, b);
3674 a.check_error();
3675 return expr(a.ctx(), r);
3676 }
3677 inline expr indexof(expr const& s, expr const& substr, expr const& offset) {
3678 check_context(s, substr); check_context(s, offset);
3679 Z3_ast r = Z3_mk_seq_index(s.ctx(), s, substr, offset);
3680 s.check_error();
3681 return expr(s.ctx(), r);
3682 }
3683 inline expr last_indexof(expr const& s, expr const& substr) {
3684 check_context(s, substr);
3685 Z3_ast r = Z3_mk_seq_last_index(s.ctx(), s, substr);
3686 s.check_error();
3687 return expr(s.ctx(), r);
3688 }
3689 inline expr to_re(expr const& s) {
3691 }
3692 inline expr in_re(expr const& s, expr const& re) {
3693 MK_EXPR2(Z3_mk_seq_in_re, s, re);
3694 }
3695 inline expr plus(expr const& re) {
3697 }
3698 inline expr option(expr const& re) {
3700 }
3701 inline expr star(expr const& re) {
3703 }
3704 inline expr re_empty(sort const& s) {
3705 Z3_ast r = Z3_mk_re_empty(s.ctx(), s);
3706 s.check_error();
3707 return expr(s.ctx(), r);
3708 }
3709 inline expr re_full(sort const& s) {
3710 Z3_ast r = Z3_mk_re_full(s.ctx(), s);
3711 s.check_error();
3712 return expr(s.ctx(), r);
3713 }
3714 inline expr re_intersect(expr_vector const& args) {
3715 assert(args.size() > 0);
3716 context& ctx = args[0].ctx();
3717 array<Z3_ast> _args(args);
3718 Z3_ast r = Z3_mk_re_intersect(ctx, _args.size(), _args.ptr());
3719 ctx.check_error();
3720 return expr(ctx, r);
3721 }
3722 inline expr re_complement(expr const& a) {
3724 }
3725 inline expr range(expr const& lo, expr const& hi) {
3726 check_context(lo, hi);
3727 Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
3728 lo.check_error();
3729 return expr(lo.ctx(), r);
3730 }
3731
3732
3733
3734
3735
3736 inline expr_vector context::parse_string(char const* s) {
3737 Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0);
3738 check_error();
3739 return expr_vector(*this, r);
3740
3741 }
3742 inline expr_vector context::parse_file(char const* s) {
3743 Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0);
3744 check_error();
3745 return expr_vector(*this, r);
3746 }
3747
3748 inline expr_vector context::parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls) {
3749 array<Z3_symbol> sort_names(sorts.size());
3750 array<Z3_symbol> decl_names(decls.size());
3751 array<Z3_sort> sorts1(sorts);
3752 array<Z3_func_decl> decls1(decls);
3753 for (unsigned i = 0; i < sorts.size(); ++i) {
3754 sort_names[i] = sorts[i].name();
3755 }
3756 for (unsigned i = 0; i < decls.size(); ++i) {
3757 decl_names[i] = decls[i].name();
3758 }
3759
3760 Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
3761 check_error();
3762 return expr_vector(*this, r);
3763 }
3764
3765 inline expr_vector context::parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls) {
3766 array<Z3_symbol> sort_names(sorts.size());
3767 array<Z3_symbol> decl_names(decls.size());
3768 array<Z3_sort> sorts1(sorts);
3769 array<Z3_func_decl> decls1(decls);
3770 for (unsigned i = 0; i < sorts.size(); ++i) {
3771 sort_names[i] = sorts[i].name();
3772 }
3773 for (unsigned i = 0; i < decls.size(); ++i) {
3774 decl_names[i] = decls[i].name();
3775 }
3776 Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
3777 check_error();
3778 return expr_vector(*this, r);
3779 }
3780
3781
3782 inline expr expr::substitute(expr_vector const& src, expr_vector const& dst) {
3783 assert(src.size() == dst.size());
3784 array<Z3_ast> _src(src.size());
3785 array<Z3_ast> _dst(dst.size());
3786 for (unsigned i = 0; i < src.size(); ++i) {
3787 _src[i] = src[i];
3788 _dst[i] = dst[i];
3789 }
3790 Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
3791 check_error();
3792 return expr(ctx(), r);
3793 }
3794
3795 inline expr expr::substitute(expr_vector const& dst) {
3796 array<Z3_ast> _dst(dst.size());
3797 for (unsigned i = 0; i < dst.size(); ++i) {
3798 _dst[i] = dst[i];
3799 }
3800 Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
3801 check_error();
3802 return expr(ctx(), r);
3803 }
3804
3805
3807
3808 typedef std::function<void(unsigned, expr const&)> fixed_eh_t;
3809 typedef std::function<void(void)> final_eh_t;
3810 typedef std::function<void(unsigned, unsigned)> eq_eh_t;
3811
3812 final_eh_t m_final_eh;
3813 eq_eh_t m_eq_eh;
3814 fixed_eh_t m_fixed_eh;
3815 solver* s;
3816 Z3_context c;
3817 Z3_solver_callback cb { nullptr };
3818
3819 Z3_context ctx() {
3820 return c ? c : (Z3_context)s->ctx();
3821 }
3822
3823 struct scoped_cb {
3825 scoped_cb(void* _p, Z3_solver_callback cb):p(*static_cast<user_propagator_base*>(_p)) {
3826 p.cb = cb;
3827 }
3828 ~scoped_cb() {
3829 p.cb = nullptr;
3830 }
3831 };
3832
3833 static void push_eh(void* p) {
3834 static_cast<user_propagator_base*>(p)->push();
3835 }
3836
3837 static void pop_eh(void* p, unsigned num_scopes) {
3838 static_cast<user_propagator_base*>(p)->pop(num_scopes);
3839 }
3840
3841 static void* fresh_eh(void* p, Z3_context ctx) {
3842 return static_cast<user_propagator_base*>(p)->fresh(ctx);
3843 }
3844
3845 static void fixed_eh(void* _p, Z3_solver_callback cb, unsigned id, Z3_ast _value) {
3846 user_propagator_base* p = static_cast<user_propagator_base*>(_p);
3847 scoped_cb _cb(p, cb);
3848 scoped_context ctx(p->ctx());
3849 expr value(ctx(), _value);
3850 static_cast<user_propagator_base*>(p)->m_fixed_eh(id, value);
3851 }
3852
3853 static void eq_eh(void* p, Z3_solver_callback cb, unsigned x, unsigned y) {
3854 scoped_cb _cb(p, cb);
3855 static_cast<user_propagator_base*>(p)->m_eq_eh(x, y);
3856 }
3857
3858 static void final_eh(void* p, Z3_solver_callback cb) {
3859 scoped_cb _cb(p, cb);
3860 static_cast<user_propagator_base*>(p)->m_final_eh();
3861 }
3862
3863
3864 public:
3865 user_propagator_base(solver* s): s(s), c(nullptr) {}
3866 user_propagator_base(Z3_context c): s(nullptr), c(c) {}
3867
3868 virtual void push() = 0;
3869 virtual void pop(unsigned num_scopes) = 0;
3870
3879 virtual user_propagator_base* fresh(Z3_context ctx) = 0;
3880
3887 void fixed(fixed_eh_t& f) {
3888 assert(s);
3889 m_fixed_eh = f;
3890 Z3_solver_propagate_fixed(ctx(), *s, fixed_eh);
3891 }
3892
3893 void eq(eq_eh_t& f) {
3894 assert(s);
3895 m_eq_eh = f;
3896 Z3_solver_propagate_eq(ctx(), *s, eq_eh);
3897 }
3898
3907 void register_final(final_eh_t& f) {
3908 assert(s);
3909 m_final_eh = f;
3910 Z3_solver_propagate_final(ctx(), *s, final_eh);
3911 }
3912
3927 unsigned add(expr const& e) {
3928 assert(s);
3929 return Z3_solver_propagate_register(ctx(), *s, e);
3930 }
3931
3932 void conflict(unsigned num_fixed, unsigned const* fixed) {
3933 assert(cb);
3934 scoped_context _ctx(ctx());
3935 expr conseq = _ctx().bool_val(false);
3936 Z3_solver_propagate_consequence(ctx(), cb, num_fixed, fixed, 0, nullptr, nullptr, conseq);
3937 }
3938
3939 void propagate(unsigned num_fixed, unsigned const* fixed, expr const& conseq) {
3940 assert(cb);
3941 assert(conseq.ctx() == ctx());
3942 Z3_solver_propagate_consequence(ctx(), cb, num_fixed, fixed, 0, nullptr, nullptr, conseq);
3943 }
3944
3945 void propagate(unsigned num_fixed, unsigned const* fixed,
3946 unsigned num_eqs, unsigned const* lhs, unsigned const * rhs,
3947 expr const& conseq) {
3948 assert(cb);
3949 assert(conseq.ctx() == ctx());
3950 Z3_solver_propagate_consequence(ctx(), cb, num_fixed, fixed, num_eqs, lhs, rhs, conseq);
3951 }
3952 };
3953
3954
3955
3956
3957}
3958
3961#undef Z3_THROW
3962
unsigned size() const
Definition: z3++.h:2845
apply_result & operator=(apply_result const &s)
Definition: z3++.h:2838
apply_result(context &c, Z3_apply_result s)
Definition: z3++.h:2834
goal operator[](int i) const
Definition: z3++.h:2846
friend std::ostream & operator<<(std::ostream &out, apply_result const &r)
Definition: z3++.h:2849
apply_result(apply_result const &s)
Definition: z3++.h:2835
unsigned size() const
Definition: z3++.h:410
void resize(unsigned sz)
Definition: z3++.h:409
T const & operator[](int i) const
Definition: z3++.h:412
array(unsigned sz)
Definition: z3++.h:406
T const * ptr() const
Definition: z3++.h:413
T * ptr()
Definition: z3++.h:414
T & operator[](int i)
Definition: z3++.h:411
iterator(ast_vector_tpl const *v, unsigned i)
Definition: z3++.h:584
bool operator==(iterator const &other) const noexcept
Definition: z3++.h:586
iterator operator++(int) noexcept
Definition: z3++.h:599
T * operator->() const
Definition: z3++.h:600
bool operator!=(iterator const &other) const noexcept
Definition: z3++.h:589
iterator & operator++() noexcept
Definition: z3++.h:592
void pop_back()
Definition: z3++.h:559
friend std::ostream & operator<<(std::ostream &out, ast_vector_tpl const &v)
Definition: z3++.h:605
unsigned size() const
Definition: z3++.h:554
void resize(unsigned sz)
Definition: z3++.h:557
ast_vector_tpl & operator=(ast_vector_tpl const &s)
Definition: z3++.h:561
ast_vector_tpl(ast_vector_tpl const &s)
Definition: z3++.h:549
bool empty() const
Definition: z3++.h:560
iterator end() const
Definition: z3++.h:604
ast_vector_tpl(context &c, Z3_ast_vector v)
Definition: z3++.h:548
void push_back(T const &e)
Definition: z3++.h:556
T back() const
Definition: z3++.h:558
T operator[](int i) const
Definition: z3++.h:555
ast_vector_tpl & set(unsigned idx, ast &a)
Definition: z3++.h:568
ast_vector_tpl(context &c, ast_vector_tpl const &src)
Definition: z3++.h:550
ast_vector_tpl(context &c)
Definition: z3++.h:547
iterator begin() const noexcept
Definition: z3++.h:603
Definition: z3++.h:498
~ast()
Definition: z3++.h:506
friend std::ostream & operator<<(std::ostream &out, ast const &n)
Definition: z3++.h:536
ast(ast const &s)
Definition: z3++.h:504
ast & operator=(ast const &s)
Definition: z3++.h:509
ast(ast &&s) noexcept
Definition: z3++.h:505
friend bool eq(ast const &a, ast const &b)
Return true if the ASTs are structurally identical.
Definition: z3++.h:540
Z3_ast_kind kind() const
Definition: z3++.h:525
Z3_ast m_ast
Definition: z3++.h:500
ast(context &c)
Definition: z3++.h:502
std::string to_string() const
Definition: z3++.h:528
ast(context &c, Z3_ast n)
Definition: z3++.h:503
ast & operator=(ast &&s) noexcept
Definition: z3++.h:517
unsigned hash() const
Definition: z3++.h:526
ast operator()(context &c, Z3_ast a)
Definition: z3++.h:2149
expr operator()(context &c, Z3_ast a)
Definition: z3++.h:2154
func_decl operator()(context &c, Z3_ast a)
Definition: z3++.h:2173
sort operator()(context &c, Z3_ast a)
Definition: z3++.h:2165
Z3 global configuration object.
Definition: z3++.h:107
~config()
Definition: z3++.h:113
void set(char const *param, int value)
Set global parameter param with integer value.
Definition: z3++.h:126
void set(char const *param, char const *value)
Set global parameter param with string value.
Definition: z3++.h:118
config()
Definition: z3++.h:112
void set(char const *param, bool value)
Set global parameter param with Boolean value.
Definition: z3++.h:122
A Context manages all other Z3 objects, global configuration options, etc.
Definition: z3++.h:156
expr real_val(int n, int d)
Definition: z3++.h:3396
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Definition: z3++.h:3194
expr num_val(int n, sort const &s)
Definition: z3++.h:3423
expr fpa_rounding_mode()
Definition: z3++.h:3377
context()
Definition: z3++.h:180
expr bv_val(int n, unsigned sz)
Definition: z3++.h:3403
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3328
expr bool_val(bool b)
Definition: z3++.h:3388
expr fpa_const(char const *name, unsigned ebits, unsigned sbits)
Definition: z3++.h:3370
expr string_val(char const *s)
Definition: z3++.h:3420
sort real_sort()
Return the Real sort.
Definition: z3++.h:3199
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
expr bv_const(char const *name, unsigned sz)
Definition: z3++.h:3369
expr string_const(char const *name)
Definition: z3++.h:3368
sort array_sort(sort d, sort r)
Return an array sort for arrays from d to r.
Definition: z3++.h:3220
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:206
sort string_sort()
Return the sort for ASCII strings.
Definition: z3++.h:3201
sort re_sort(sort &seq_sort)
Return a regular expression sort over sequences seq_sort.
Definition: z3++.h:3203
sort uninterpreted_sort(char const *name)
create an uninterpreted sort with the name given by the string or symbol.
Definition: z3++.h:3249
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:3225
void set(char const *param, int value)
Update global parameter param with Integer value.
Definition: z3++.h:221
sort bool_sort()
Return the Boolean sort.
Definition: z3++.h:3197
void set(char const *param, char const *value)
Update global parameter param with string value.
Definition: z3++.h:213
~context()
Definition: z3++.h:182
expr bool_const(char const *name)
Definition: z3++.h:3365
void check_parser_error() const
Definition: z3++.h:195
expr_vector parse_string(char const *s)
parsing
Definition: z3++.h:3736
sort fpa_sort()
Definition: z3++.h:3207
symbol int_symbol(int n)
Create a Z3 symbol based on the given integer.
Definition: z3++.h:3195
expr real_const(char const *name)
Definition: z3++.h:3367
expr int_const(char const *name)
Definition: z3++.h:3366
expr fpa_nan(sort const &s)
Definition: z3++.h:3416
expr fpa_val(double n)
Definition: z3++.h:3414
bool enable_exceptions() const
Definition: z3++.h:208
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:3200
expr int_val(int n)
Definition: z3++.h:3390
expr fpa_inf(sort const &s, bool sgn)
Definition: z3++.h:3417
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3257
sort fpa_rounding_mode_sort()
Return a RoundingMode sort.
Definition: z3++.h:3218
expr_vector parse_file(char const *file)
Definition: z3++.h:3742
expr constant(symbol const &name, sort const &s)
Definition: z3++.h:3359
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:3236
void set(char const *param, bool value)
Update global parameter param with Boolean value.
Definition: z3++.h:217
sort int_sort()
Return the integer sort.
Definition: z3++.h:3198
void interrupt()
Interrupt the current procedure being executed by any object managed by this context....
Definition: z3++.h:230
void set_rounding_mode(rounding_mode rm)
Sets RoundingMode of FloatingPoints.
Definition: z3++.h:3375
sort fpa_sort()
Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128).
context(config &c)
Definition: z3++.h:181
void recdef(func_decl, expr_vector const &args, expr const &body)
Definition: z3++.h:3353
sort seq_sort(sort &s)
Return a sequence sort over base sort s.
Definition: z3++.h:3202
Exception used to sign API usage errors.
Definition: z3++.h:85
char const * what() const
Definition: z3++.h:91
friend std::ostream & operator<<(std::ostream &out, exception const &e)
Definition: z3++.h:94
virtual ~exception()
Definition: z3++.h:88
char const * msg() const
Definition: z3++.h:90
exception(char const *msg)
Definition: z3++.h:89
A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort ...
Definition: z3++.h:757
bool is_lambda() const
Return true if this expression is a lambda expression.
Definition: z3++.h:866
expr numerator() const
Definition: z3++.h:1083
friend expr pw(expr const &a, expr const &b)
Definition: z3++.h:1507
friend expr sbv_to_fpa(expr const &t, sort s)
Conversion of a signed bit-vector term into a floating-point.
Definition: z3++.h:1925
friend expr bvneg_no_overflow(expr const &a)
Definition: z3++.h:2118
uint64_t as_int64() const
Definition: z3++.h:839
expr loop(unsigned lo, unsigned hi)
Definition: z3++.h:1450
expr body() const
Return the 'body' of this quantifier.
Definition: z3++.h:1155
friend expr bvadd_no_underflow(expr const &a, expr const &b)
Definition: z3++.h:2106
friend expr sum(expr_vector const &args)
Definition: z3++.h:2302
expr substitute(expr_vector const &src, expr_vector const &dst)
Apply substitution. Replace src expressions by dst.
Definition: z3++.h:3782
bool is_quantifier() const
Return true if this expression is a quantifier.
Definition: z3++.h:853
bool is_exists() const
Return true if this expression is an existential quantifier.
Definition: z3++.h:862
bool is_numeral_u64(uint64_t &i) const
Definition: z3++.h:829
bool is_int() const
Return true if this is an integer expression.
Definition: z3++.h:774
expr rotate_left(unsigned i)
Definition: z3++.h:1331
friend expr operator/(expr const &a, expr const &b)
Definition: z3++.h:1673
friend expr fp_eq(expr const &a, expr const &b)
Definition: z3++.h:1886
friend expr concat(expr const &a, expr const &b)
Definition: z3++.h:2320
friend expr bvmul_no_underflow(expr const &a, expr const &b)
Definition: z3++.h:2124
int64_t get_numeral_int64() const
Return int64_t value of numeral, throw if result cannot fit in int64_t.
Definition: z3++.h:1051
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:845
friend expr fpa_to_fpa(expr const &t, sort s)
Conversion of a floating-point term into another floating-point.
Definition: z3++.h:1939
friend expr operator&&(expr const &a, expr const &b)
Return an expression representing a and b.
Definition: z3++.h:1551
friend expr operator!=(expr const &a, expr const &b)
Definition: z3++.h:1587
friend expr operator+(expr const &a, expr const &b)
Definition: z3++.h:1599
std::string get_string() const
Definition: z3++.h:1117
bool is_numeral(std::string &s) const
Definition: z3++.h:832
bool is_var() const
Return true if this expression is a variable.
Definition: z3++.h:871
bool is_numeral_u(unsigned &i) const
Definition: z3++.h:831
friend expr min(expr const &a, expr const &b)
Definition: z3++.h:1821
expr at(expr const &index) const
Definition: z3++.h:1413
expr denominator() const
Definition: z3++.h:1091
bool is_real() const
Return true if this is a real expression.
Definition: z3++.h:778
bool is_numeral_i(int &i) const
Definition: z3++.h:830
friend expr operator>(expr const &a, expr const &b)
Definition: z3++.h:1784
expr mk_is_nan() const
Return Boolean expression to test for whether an FP expression is a NaN.
Definition: z3++.h:895
int get_numeral_int() const
Return int value of numeral, throw if result cannot fit in machine int.
Definition: z3++.h:1015
friend expr bv2int(expr const &a, bool is_signed)
bit-vector and integer conversions.
Definition: z3++.h:2097
friend expr operator~(expr const &a)
Definition: z3++.h:1893
unsigned num_args() const
Return the number of arguments in this application. This method assumes the expression is an applicat...
Definition: z3++.h:1140
friend expr nor(expr const &a, expr const &b)
Definition: z3++.h:1819
friend expr fpa_fp(expr const &sgn, expr const &exp, expr const &sig)
Create an expression of FloatingPoint sort from three bit-vector expressions.
Definition: z3++.h:1903
expr arg(unsigned i) const
Return the i-th argument of this application. This method assumes the expression is an application.
Definition: z3++.h:1148
expr mk_is_normal() const
Return Boolean expression to test for whether an FP expression is a normal.
Definition: z3++.h:905
friend expr bvsub_no_underflow(expr const &a, expr const &b, bool is_signed)
Definition: z3++.h:2112
bool is_true() const
Definition: z3++.h:1220
expr(context &c)
Definition: z3++.h:759
bool is_numeral(std::string &s, unsigned precision) const
Definition: z3++.h:833
unsigned get_numeral_uint() const
Return uint value of numeral, throw if result cannot fit in machine uint.
Definition: z3++.h:1034
bool is_distinct() const
Definition: z3++.h:1229
bool is_numeral(double &d) const
Definition: z3++.h:834
friend expr operator*(expr const &a, expr const &b)
Definition: z3++.h:1629
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:765
friend expr nand(expr const &a, expr const &b)
Definition: z3++.h:1818
bool is_and() const
Definition: z3++.h:1223
friend expr fpa_to_ubv(expr const &t, unsigned sz)
Conversion of a floating-point term into an unsigned bit-vector.
Definition: z3++.h:1918
friend expr bvredor(expr const &a)
Definition: z3++.h:1851
expr extract(unsigned hi, unsigned lo) const
Definition: z3++.h:1343
friend expr int2bv(unsigned n, expr const &a)
Definition: z3++.h:2098
friend expr max(expr const &a, expr const &b)
Definition: z3++.h:1836
bool is_relation() const
Return true if this is a Relation expression.
Definition: z3++.h:798
friend expr xnor(expr const &a, expr const &b)
Definition: z3++.h:1820
friend expr abs(expr const &a)
Definition: z3++.h:1863
friend expr pbge(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:2270
bool is_well_sorted() const
Return true if this expression is well sorted (aka type correct).
Definition: z3++.h:880
bool is_or() const
Definition: z3++.h:1224
friend expr round_fpa_to_closest_integer(expr const &t)
Round a floating-point term into its closest integer.
Definition: z3++.h:1946
friend expr distinct(expr_vector const &args)
Definition: z3++.h:2311
friend expr bvmul_no_overflow(expr const &a, expr const &b, bool is_signed)
Definition: z3++.h:2121
friend expr bvsub_no_overflow(expr const &a, expr const &b)
Definition: z3++.h:2109
bool is_const() const
Return true if this expression is a constant (i.e., an application with 0 arguments).
Definition: z3++.h:849
expr length() const
Definition: z3++.h:1425
friend expr mod(expr const &a, expr const &b)
Definition: z3++.h:1511
friend expr fma(expr const &a, expr const &b, expr const &c, expr const &rm)
FloatingPoint fused multiply-add.
Definition: z3++.h:1895
bool is_bool() const
Return true if this is a Boolean expression.
Definition: z3++.h:770
friend expr mk_or(expr_vector const &args)
Definition: z3++.h:2364
expr contains(expr const &s) const
Definition: z3++.h:1407
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:1958
expr algebraic_lower(unsigned precision) const
Definition: z3++.h:966
unsigned hi() const
Definition: z3++.h:1345
expr simplify() const
Return a simplified version of this expression.
Definition: z3++.h:1474
bool is_arith() const
Return true if this is an integer or real expression.
Definition: z3++.h:782
expr mk_is_inf() const
Return Boolean expression to test for whether an FP expression is inf.
Definition: z3++.h:885
expr stoi() const
Definition: z3++.h:1430
expr_vector algebraic_poly() const
Return coefficients for p of an algebraic number (root-obj p i)
Definition: z3++.h:983
bool is_ite() const
Definition: z3++.h:1228
bool is_bv() const
Return true if this is a Bit-vector expression.
Definition: z3++.h:786
friend expr pbeq(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:2278
friend expr operator^(expr const &a, expr const &b)
Definition: z3++.h:1810
friend expr operator<=(expr const &a, expr const &b)
Definition: z3++.h:1737
friend expr operator>=(expr const &a, expr const &b)
Definition: z3++.h:1653
friend expr sqrt(expr const &a, expr const &rm)
Definition: z3++.h:1879
friend expr pble(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:2262
friend expr operator==(expr const &a, expr const &b)
Definition: z3++.h:1576
bool is_finite_domain() const
Return true if this is a Finite-domain expression.
Definition: z3++.h:816
expr operator[](expr_vector const &index) const
Definition: z3++.h:1467
bool is_forall() const
Return true if this expression is a universal quantifier.
Definition: z3++.h:858
bool is_implies() const
Definition: z3++.h:1226
uint64_t as_uint64() const
Definition: z3++.h:838
friend expr implies(expr const &a, expr const &b)
Definition: z3++.h:1499
expr mk_is_subnormal() const
Return Boolean expression to test for whether an FP expression is a subnormal.
Definition: z3++.h:915
uint64_t get_numeral_uint64() const
Return uint64_t value of numeral, throw if result cannot fit in uint64_t.
Definition: z3++.h:1068
expr(context &c, Z3_ast n)
Definition: z3++.h:760
friend expr bvadd_no_overflow(expr const &a, expr const &b, bool is_signed)
bit-vector overflow/underflow checks
Definition: z3++.h:2103
bool is_datatype() const
Return true if this is a Datatype expression.
Definition: z3++.h:794
bool is_not() const
Definition: z3++.h:1222
bool is_string_value() const
Return true if this expression is a string literal. The string can be accessed using get_string() and...
Definition: z3++.h:1103
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:1478
expr loop(unsigned lo)
create a looping regular expression.
Definition: z3++.h:1445
expr mk_from_ieee_bv(sort const &s) const
Convert this IEEE BV into a fpa.
Definition: z3++.h:945
friend expr bvredand(expr const &a)
Definition: z3++.h:1857
friend expr operator&(expr const &a, expr const &b)
Definition: z3++.h:1806
friend expr operator-(expr const &a)
Definition: z3++.h:1695
friend expr bvsdiv_no_overflow(expr const &a, expr const &b)
Definition: z3++.h:2115
expr extract(expr const &offset, expr const &length) const
sequence and regular expression operations.
Definition: z3++.h:1392
std::string get_escaped_string() const
for a string value expression return an escaped or unescaped string value.
Definition: z3++.h:1110
bool is_eq() const
Definition: z3++.h:1227
expr rotate_right(unsigned i)
Definition: z3++.h:1332
expr unit() const
Definition: z3++.h:1402
bool is_re() const
Return true if this is a regular expression.
Definition: z3++.h:806
bool is_numeral_i64(int64_t &i) const
Definition: z3++.h:828
bool as_binary(std::string &s) const
Definition: z3++.h:835
unsigned id() const
retrieve unique identifier for expression.
Definition: z3++.h:1003
friend expr rem(expr const &a, expr const &b)
Definition: z3++.h:1527
friend expr operator!(expr const &a)
Return an expression representing not(a).
Definition: z3++.h:1545
bool is_algebraic() const
Return true if expression is an algebraic number.
Definition: z3++.h:875
expr repeat(unsigned i)
Definition: z3++.h:1333
friend expr mk_and(expr_vector const &args)
Definition: z3++.h:2370
expr itos() const
Definition: z3++.h:1435
bool is_false() const
Definition: z3++.h:1221
double as_double() const
Definition: z3++.h:837
expr mk_is_zero() const
Return Boolean expression to test for whether an FP expression is a zero.
Definition: z3++.h:925
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:958
Z3_lbool bool_value() const
Definition: z3++.h:1079
expr replace(expr const &src, expr const &dst) const
Definition: z3++.h:1396
friend expr operator||(expr const &a, expr const &b)
Return an expression representing a or b.
Definition: z3++.h:1563
bool is_array() const
Return true if this is a Array expression.
Definition: z3++.h:790
bool is_xor() const
Definition: z3++.h:1225
unsigned algebraic_i() const
Return i of an algebraic number (root-obj p i)
Definition: z3++.h:993
unsigned lo() const
Definition: z3++.h:1344
friend expr ubv_to_fpa(expr const &t, sort s)
Conversion of an unsigned bit-vector term into a floating-point.
Definition: z3++.h:1932
expr nth(expr const &index) const
Definition: z3++.h:1419
friend expr fpa_to_sbv(expr const &t, unsigned sz)
Conversion of a floating-point term into a signed bit-vector.
Definition: z3++.h:1911
bool is_seq() const
Return true if this is a sequence expression.
Definition: z3++.h:802
friend expr operator|(expr const &a, expr const &b)
Definition: z3++.h:1814
friend expr atmost(expr_vector const &es, unsigned bound)
Definition: z3++.h:2286
friend expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725
friend expr atleast(expr_vector const &es, unsigned bound)
Definition: z3++.h:2294
friend expr operator<(expr const &a, expr const &b)
Definition: z3++.h:1762
expr mk_to_ieee_bv() const
Convert this fpa into an IEEE BV.
Definition: z3++.h:935
expr operator[](expr const &index) const
Definition: z3++.h:1459
expr algebraic_upper(unsigned precision) const
Definition: z3++.h:973
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:827
bool is_fpa() const
Return true if this is a FloatingPoint expression. .
Definition: z3++.h:820
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:1133
std::string to_string(expr_vector const &queries)
Definition: z3++.h:3169
std::string help() const
Definition: z3++.h:3166
fixedpoint & operator=(fixedpoint const &o)
Definition: z3++.h:3124
expr_vector from_string(char const *s)
Definition: z3++.h:3132
void add_fact(func_decl &f, unsigned *args)
Definition: z3++.h:3143
void add_cover(int level, func_decl &p, expr &property)
Definition: z3++.h:3160
expr_vector rules() const
Definition: z3++.h:3164
stats statistics() const
Definition: z3++.h:3161
expr get_answer()
Definition: z3++.h:3151
expr get_cover_delta(int level, func_decl &p)
Definition: z3++.h:3155
fixedpoint(context &c)
Definition: z3++.h:3121
std::string reason_unknown()
Definition: z3++.h:3152
check_result query(func_decl_vector &relations)
Definition: z3++.h:3145
void register_relation(func_decl &p)
Definition: z3++.h:3162
std::string to_string()
Definition: z3++.h:3168
check_result query(expr &q)
Definition: z3++.h:3144
param_descrs get_param_descrs()
Definition: z3++.h:3167
expr_vector from_file(char const *s)
Definition: z3++.h:3137
void update_rule(expr &rule, symbol const &name)
Definition: z3++.h:3153
expr_vector assertions() const
Definition: z3++.h:3163
fixedpoint(fixedpoint const &o)
Definition: z3++.h:3122
unsigned get_num_levels(func_decl &p)
Definition: z3++.h:3154
void add_rule(expr &rule, symbol const &name)
Definition: z3++.h:3142
void set(params const &p)
Definition: z3++.h:3165
Function declaration (aka function definition). It is the signature of interpreted and uninterpreted ...
Definition: z3++.h:711
func_decl transitive_closure(func_decl const &)
Definition: z3++.h:728
func_decl(context &c, Z3_func_decl n)
Definition: z3++.h:714
symbol name() const
Definition: z3++.h:725
expr operator()() const
Definition: z3++.h:3446
bool is_const() const
Definition: z3++.h:732
sort range() const
Definition: z3++.h:724
func_decl(context &c)
Definition: z3++.h:713
Z3_decl_kind decl_kind() const
Definition: z3++.h:726
sort domain(unsigned i) const
Definition: z3++.h:723
unsigned id() const
retrieve unique identifier for func_decl.
Definition: z3++.h:720
unsigned arity() const
Definition: z3++.h:722
Definition: z3++.h:2378
~func_entry()
Definition: z3++.h:2387
unsigned num_args() const
Definition: z3++.h:2397
expr arg(unsigned i) const
Definition: z3++.h:2398
func_entry(context &c, Z3_func_entry e)
Definition: z3++.h:2385
expr value() const
Definition: z3++.h:2396
func_entry & operator=(func_entry const &s)
Definition: z3++.h:2389
func_entry(func_entry const &s)
Definition: z3++.h:2386
expr else_value() const
Definition: z3++.h:2419
void set_else(expr &value)
Definition: z3++.h:2426
func_interp(context &c, Z3_func_interp e)
Definition: z3++.h:2408
func_interp(func_interp const &s)
Definition: z3++.h:2409
func_entry entry(unsigned i) const
Definition: z3++.h:2421
void add_entry(expr_vector const &args, expr &value)
Definition: z3++.h:2422
unsigned num_entries() const
Definition: z3++.h:2420
func_interp & operator=(func_interp const &s)
Definition: z3++.h:2412
void add(expr const &f)
Definition: z3++.h:2787
unsigned size() const
Definition: z3++.h:2789
Z3_goal_prec precision() const
Definition: z3++.h:2791
model convert_model(model const &m) const
Definition: z3++.h:2798
bool is_decided_unsat() const
Definition: z3++.h:2797
goal(goal const &s)
Definition: z3++.h:2777
bool inconsistent() const
Definition: z3++.h:2792
model get_model() const
Definition: z3++.h:2804
std::string dimacs(bool include_names=true) const
Definition: z3++.h:2822
unsigned num_exprs() const
Definition: z3++.h:2795
goal(context &c, Z3_goal s)
Definition: z3++.h:2776
goal(context &c, bool models=true, bool unsat_cores=false, bool proofs=false)
Definition: z3++.h:2775
void add(expr_vector const &v)
Definition: z3++.h:2788
~goal()
Definition: z3++.h:2778
goal & operator=(goal const &s)
Definition: z3++.h:2780
void reset()
Definition: z3++.h:2794
friend std::ostream & operator<<(std::ostream &out, goal const &g)
Definition: z3++.h:2825
unsigned depth() const
Definition: z3++.h:2793
bool is_decided_sat() const
Definition: z3++.h:2796
expr as_expr() const
Definition: z3++.h:2809
expr operator[](int i) const
Definition: z3++.h:2790
expr eval(expr const &n, bool model_completion=false) const
Definition: z3++.h:2454
unsigned size() const
Definition: z3++.h:2468
~model()
Definition: z3++.h:2444
expr get_const_interp(func_decl c) const
Definition: z3++.h:2477
unsigned num_consts() const
Definition: z3++.h:2464
model & operator=(model const &s)
Definition: z3++.h:2446
unsigned num_funcs() const
Definition: z3++.h:2465
func_interp get_func_interp(func_decl f) const
Definition: z3++.h:2483
func_decl get_func_decl(unsigned i) const
Definition: z3++.h:2467
func_interp add_func_interp(func_decl &f, expr &else_val)
Definition: z3++.h:2497
func_decl operator[](int i) const
Definition: z3++.h:2469
friend std::ostream & operator<<(std::ostream &out, model const &m)
Definition: z3++.h:2512
model(model const &s)
Definition: z3++.h:2442
model(context &c)
Definition: z3++.h:2440
void add_const_interp(func_decl &f, expr &value)
Definition: z3++.h:2503
func_decl get_const_decl(unsigned i) const
Definition: z3++.h:2466
bool has_interp(func_decl f) const
Definition: z3++.h:2492
std::string to_string() const
Definition: z3++.h:2510
model(model &src, context &dst, translate)
Definition: z3++.h:2443
model(context &c, Z3_model m)
Definition: z3++.h:2441
context * m_ctx
Definition: z3++.h:419
Z3_error_code check_error() const
Definition: z3++.h:423
context & ctx() const
Definition: z3++.h:422
object(context &c)
Definition: z3++.h:421
friend void check_context(object const &a, object const &b)
Definition: z3++.h:426
handle(unsigned h)
Definition: z3++.h:3021
unsigned h() const
Definition: z3++.h:3022
std::string help() const
Definition: z3++.h:3114
handle add_soft(expr const &e, char const *weight)
Definition: z3++.h:3064
friend std::ostream & operator<<(std::ostream &out, optimize const &s)
Definition: z3++.h:3116
void add(expr const &e, expr const &t)
Definition: z3++.h:3051
expr lower(handle const &h)
Definition: z3++.h:3098
void pop()
Definition: z3++.h:3080
expr_vector objectives() const
Definition: z3++.h:3109
void add(expr_vector const &es)
Definition: z3++.h:3048
void add(expr const &e, char const *p)
Definition: z3++.h:3055
model get_model() const
Definition: z3++.h:3095
handle add(expr const &e, unsigned weight)
Definition: z3++.h:3068
check_result check()
Definition: z3++.h:3083
check_result check(expr_vector const &asms)
Definition: z3++.h:3084
stats statistics() const
Definition: z3++.h:3110
void add(expr const &e)
Definition: z3++.h:3044
void push()
Definition: z3++.h:3077
handle add_soft(expr const &e, unsigned weight)
Definition: z3++.h:3059
handle maximize(expr const &e)
Definition: z3++.h:3071
~optimize()
Definition: z3++.h:3042
optimize(optimize const &o)
Definition: z3++.h:3025
void from_file(char const *filename)
Definition: z3++.h:3112
expr_vector assertions() const
Definition: z3++.h:3108
optimize & operator=(optimize const &o)
Definition: z3++.h:3035
void from_string(char const *constraints)
Definition: z3++.h:3113
expr upper(handle const &h)
Definition: z3++.h:3103
optimize(context &c, optimize &src)
Definition: z3++.h:3028
handle minimize(expr const &e)
Definition: z3++.h:3074
optimize(context &c)
Definition: z3++.h:3024
void set(params const &p)
Definition: z3++.h:3097
expr_vector unsat_core() const
Definition: z3++.h:3096
param_descrs(param_descrs const &o)
Definition: z3++.h:452
param_descrs(context &c, Z3_param_descrs d)
Definition: z3++.h:451
Z3_param_kind kind(symbol const &s)
Definition: z3++.h:465
std::string documentation(symbol const &s)
Definition: z3++.h:466
symbol name(unsigned i)
Definition: z3++.h:464
static param_descrs simplify_param_descrs(context &c)
Definition: z3++.h:461
unsigned size()
Definition: z3++.h:463
std::string to_string() const
Definition: z3++.h:467
param_descrs & operator=(param_descrs const &o)
Definition: z3++.h:453
void set(char const *k, char const *s)
Definition: z3++.h:490
params(context &c)
Definition: z3++.h:475
params(params const &s)
Definition: z3++.h:476
~params()
Definition: z3++.h:477
void set(char const *k, bool b)
Definition: z3++.h:486
void set(char const *k, unsigned n)
Definition: z3++.h:487
void set(char const *k, symbol const &s)
Definition: z3++.h:489
params & operator=(params const &s)
Definition: z3++.h:479
void set(char const *k, double n)
Definition: z3++.h:488
friend std::ostream & operator<<(std::ostream &out, params const &p)
Definition: z3++.h:494
probe & operator=(probe const &s)
Definition: z3++.h:2950
friend probe operator<(probe const &p1, probe const &p2)
Definition: z3++.h:2989
double operator()(goal const &g) const
Definition: z3++.h:2958
friend probe operator==(probe const &p1, probe const &p2)
Definition: z3++.h:2999
friend probe operator<=(probe const &p1, probe const &p2)
Definition: z3++.h:2979
probe(context &c, Z3_probe s)
Definition: z3++.h:2946
probe(context &c, double val)
Definition: z3++.h:2945
probe(context &c, char const *name)
Definition: z3++.h:2944
friend probe operator&&(probe const &p1, probe const &p2)
Definition: z3++.h:3004
probe(probe const &s)
Definition: z3++.h:2947
~probe()
Definition: z3++.h:2948
friend probe operator!(probe const &p)
Definition: z3++.h:3010
double apply(goal const &g) const
Definition: z3++.h:2957
friend probe operator>=(probe const &p1, probe const &p2)
Definition: z3++.h:2984
friend probe operator>(probe const &p1, probe const &p2)
Definition: z3++.h:2994
friend probe operator||(probe const &p1, probe const &p2)
Definition: z3++.h:3007
context & operator()()
Definition: z3++.h:395
scoped_context(Z3_context c)
Definition: z3++.h:393
cube_iterator end()
Definition: z3++.h:2758
cube_generator(solver &s, expr_vector &vars)
Definition: z3++.h:2750
cube_iterator begin()
Definition: z3++.h:2757
cube_generator(solver &s)
Definition: z3++.h:2743
void set_cutoff(unsigned c) noexcept
Definition: z3++.h:2759
expr_vector const * operator->() const
Definition: z3++.h:2725
cube_iterator operator++(int)
Definition: z3++.h:2724
cube_iterator & operator++()
Definition: z3++.h:2714
bool operator!=(cube_iterator const &other) noexcept
Definition: z3++.h:2731
cube_iterator(solver &s, expr_vector &vars, unsigned &cutoff, bool end)
Definition: z3++.h:2702
bool operator==(cube_iterator const &other) noexcept
Definition: z3++.h:2728
expr_vector const & operator*() const noexcept
Definition: z3++.h:2726
void from_string(char const *s)
Definition: z3++.h:2600
expr proof() const
Definition: z3++.h:2647
~solver()
Definition: z3++.h:2567
cube_generator cubes(expr_vector &vars)
Definition: z3++.h:2763
friend std::ostream & operator<<(std::ostream &out, solver const &s)
Definition: z3++.h:2766
solver(context &c, solver const &src, translate)
Definition: z3++.h:2565
expr_vector non_units() const
Definition: z3++.h:2634
solver(context &c, simple)
Definition: z3++.h:2562
solver(context &c, Z3_solver s)
Definition: z3++.h:2563
solver(context &c, char const *logic)
Definition: z3++.h:2564
void set(char const *k, bool v)
Definition: z3++.h:2577
void add(expr const &e, expr const &p)
Definition: z3++.h:2586
void add(expr const &e, char const *p)
Definition: z3++.h:2591
check_result consequences(expr_vector &assumptions, expr_vector &vars, expr_vector &conseq)
Definition: z3++.h:2625
void set(char const *k, char const *v)
Definition: z3++.h:2581
check_result check(unsigned n, expr *const assumptions)
Definition: z3++.h:2603
model get_model() const
Definition: z3++.h:2624
std::string dimacs(bool include_names=true) const
Definition: z3++.h:2670
check_result check()
Definition: z3++.h:2602
stats statistics() const
Definition: z3++.h:2631
expr_vector units() const
Definition: z3++.h:2635
expr_vector trail() const
Definition: z3++.h:2636
void add(expr const &e)
Definition: z3++.h:2585
solver & operator=(solver const &s)
Definition: z3++.h:2569
void set(char const *k, double v)
Definition: z3++.h:2579
void pop(unsigned n=1)
Definition: z3++.h:2583
void push()
Definition: z3++.h:2582
std::string to_smt2(char const *status="unknown")
Definition: z3++.h:2650
solver(context &c)
Definition: z3++.h:2561
param_descrs get_param_descrs()
Definition: z3++.h:2672
void set(char const *k, unsigned v)
Definition: z3++.h:2578
void add(expr_vector const &v)
Definition: z3++.h:2594
expr_vector assertions() const
Definition: z3++.h:2633
void from_file(char const *file)
Definition: z3++.h:2599
expr_vector trail(array< unsigned > &levels) const
Definition: z3++.h:2637
void reset()
Definition: z3++.h:2584
std::string reason_unknown() const
Definition: z3++.h:2630
void set(params const &p)
Definition: z3++.h:2576
expr_vector cube(expr_vector &vars, unsigned cutoff)
Definition: z3++.h:2675
cube_generator cubes()
Definition: z3++.h:2762
expr_vector unsat_core() const
Definition: z3++.h:2632
solver(solver const &s)
Definition: z3++.h:2566
void set(char const *k, symbol const &v)
Definition: z3++.h:2580
check_result check(expr_vector const &assumptions)
Definition: z3++.h:2613
A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort.
Definition: z3++.h:612
sort(context &c, Z3_sort s)
Definition: z3++.h:615
Z3_sort_kind sort_kind() const
Return the internal sort kind.
Definition: z3++.h:627
unsigned bv_size() const
Return the size of this Bit-vector sort.
Definition: z3++.h:686
bool is_int() const
Return true if this sort is the Integer sort.
Definition: z3++.h:639
sort(context &c)
Definition: z3++.h:614
bool is_real() const
Return true if this sort is the Real sort.
Definition: z3++.h:643
sort(context &c, Z3_ast a)
Definition: z3++.h:616
friend std::ostream & operator<<(std::ostream &out, sort const &s)
Definition: z3++.h:704
symbol name() const
Return name of sort.
Definition: z3++.h:631
bool is_relation() const
Return true if this sort is a Relation sort.
Definition: z3++.h:663
unsigned fpa_ebits() const
Definition: z3++.h:688
sort array_range() const
Return the range of this Array sort.
Definition: z3++.h:702
bool is_bool() const
Return true if this sort is the Boolean sort.
Definition: z3++.h:635
bool is_arith() const
Return true if this sort is the Integer or Real sort.
Definition: z3++.h:647
bool is_bv() const
Return true if this sort is a Bit-vector sort.
Definition: z3++.h:651
sort array_domain() const
Return the domain of this Array sort.
Definition: z3++.h:696
bool is_finite_domain() const
Return true if this sort is a Finite domain sort.
Definition: z3++.h:675
bool is_datatype() const
Return true if this sort is a Datatype sort.
Definition: z3++.h:659
bool is_re() const
Return true if this sort is a regular expression sort.
Definition: z3++.h:671
unsigned id() const
retrieve unique identifier for func_decl.
Definition: z3++.h:622
bool is_array() const
Return true if this sort is a Array sort.
Definition: z3++.h:655
bool is_seq() const
Return true if this sort is a Sequence sort.
Definition: z3++.h:667
unsigned fpa_sbits() const
Definition: z3++.h:690
bool is_fpa() const
Return true if this sort is a Floating point sort.
Definition: z3++.h:679
stats & operator=(stats const &s)
Definition: z3++.h:2526
unsigned size() const
Definition: z3++.h:2533
bool is_uint(unsigned i) const
Definition: z3++.h:2535
bool is_double(unsigned i) const
Definition: z3++.h:2536
~stats()
Definition: z3++.h:2524
stats(stats const &s)
Definition: z3++.h:2523
double double_value(unsigned i) const
Definition: z3++.h:2538
unsigned uint_value(unsigned i) const
Definition: z3++.h:2537
stats(context &c, Z3_stats e)
Definition: z3++.h:2522
friend std::ostream & operator<<(std::ostream &out, stats const &s)
Definition: z3++.h:2541
std::string key(unsigned i) const
Definition: z3++.h:2534
stats(context &c)
Definition: z3++.h:2521
Z3_symbol_kind kind() const
Definition: z3++.h:433
symbol(context &c, Z3_symbol s)
Definition: z3++.h:431
int to_int() const
Definition: z3++.h:435
friend std::ostream & operator<<(std::ostream &out, symbol const &s)
Definition: z3++.h:439
std::string str() const
Definition: z3++.h:434
friend tactic par_or(unsigned n, tactic const *tactics)
Definition: z3++.h:2921
friend tactic par_and_then(tactic const &t1, tactic const &t2)
Definition: z3++.h:2930
std::string help() const
Definition: z3++.h:2880
solver mk_solver() const
Definition: z3++.h:2870
tactic(context &c, char const *name)
Definition: z3++.h:2858
tactic(context &c, Z3_tactic s)
Definition: z3++.h:2859
friend tactic repeat(tactic const &t, unsigned max)
Definition: z3++.h:2905
~tactic()
Definition: z3++.h:2861
friend tactic with(tactic const &t, params const &p)
Definition: z3++.h:2911
apply_result apply(goal const &g) const
Definition: z3++.h:2871
friend tactic operator&(tactic const &t1, tactic const &t2)
Definition: z3++.h:2891
friend tactic try_for(tactic const &t, unsigned ms)
Definition: z3++.h:2916
param_descrs get_param_descrs()
Definition: z3++.h:2888
tactic & operator=(tactic const &s)
Definition: z3++.h:2863
apply_result operator()(goal const &g) const
Definition: z3++.h:2877
tactic(tactic const &s)
Definition: z3++.h:2860
friend tactic operator|(tactic const &t1, tactic const &t2)
Definition: z3++.h:2898
void eq(eq_eh_t &f)
Definition: z3++.h:3893
virtual void push()=0
void register_final(final_eh_t &f)
register a callback on final-check. During the final check stage, all propagations have been processe...
Definition: z3++.h:3907
virtual void pop(unsigned num_scopes)=0
void propagate(unsigned num_fixed, unsigned const *fixed, unsigned num_eqs, unsigned const *lhs, unsigned const *rhs, expr const &conseq)
Definition: z3++.h:3945
virtual user_propagator_base * fresh(Z3_context ctx)=0
user_propagators created using fresh() are created during search and their lifetimes are restricted t...
void fixed(fixed_eh_t &f)
register callbacks. Callbacks can only be registered with user_propagators that were created using a ...
Definition: z3++.h:3887
unsigned add(expr const &e)
tracks e by a unique identifier that is returned by the call.
Definition: z3++.h:3927
user_propagator_base(solver *s)
Definition: z3++.h:3865
void conflict(unsigned num_fixed, unsigned const *fixed)
Definition: z3++.h:3932
user_propagator_base(Z3_context c)
Definition: z3++.h:3866
void propagate(unsigned num_fixed, unsigned const *fixed, expr const &conseq)
Definition: z3++.h:3939
Z3 C++ namespace.
Definition: z3++.h:49
expr re_intersect(expr_vector const &args)
Definition: z3++.h:3714
expr indexof(expr const &s, expr const &substr, expr const &offset)
Definition: z3++.h:3677
expr mk_and(expr_vector const &args)
Definition: z3++.h:2370
expr fpa_to_ubv(expr const &t, unsigned sz)
Definition: z3++.h:1918
expr star(expr const &re)
Definition: z3++.h:3701
void check_context(object const &a, object const &b)
Definition: z3++.h:426
expr bvsub_no_overflow(expr const &a, expr const &b)
Definition: z3++.h:2109
expr operator==(expr const &a, expr const &b)
Definition: z3++.h:1576
expr operator>=(expr const &a, expr const &b)
Definition: z3++.h:1653
expr srem(expr const &a, expr const &b)
signed remainder operator for bitvectors
Definition: z3++.h:2050
expr bvadd_no_underflow(expr const &a, expr const &b)
Definition: z3++.h:2106
expr pble(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:2262
expr store(expr const &a, expr const &i, expr const &v)
Definition: z3++.h:3567
expr mod(expr const &a, expr const &b)
Definition: z3++.h:1511
expr fma(expr const &a, expr const &b, expr const &c, expr const &rm)
Definition: z3++.h:1895
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725
expr round_fpa_to_closest_integer(expr const &t)
Definition: z3++.h:1946
expr distinct(expr_vector const &args)
Definition: z3++.h:2311
expr bvmul_no_underflow(expr const &a, expr const &b)
Definition: z3++.h:2124
expr operator|(expr const &a, expr const &b)
Definition: z3++.h:1814
expr pbeq(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:2278
ast_vector_tpl< func_decl > func_decl_vector
Definition: z3++.h:75
expr lshr(expr const &a, expr const &b)
logic shift right operator for bitvectors
Definition: z3++.h:2078
expr bv2int(expr const &a, bool is_signed)
bit-vector and integer conversions.
Definition: z3++.h:2097
expr max(expr const &a, expr const &b)
Definition: z3++.h:1836
expr operator^(expr const &a, expr const &b)
Definition: z3++.h:1810
func_decl linear_order(sort const &a, unsigned index)
Definition: z3++.h:2134
check_result
Definition: z3++.h:132
@ unknown
Definition: z3++.h:133
@ sat
Definition: z3++.h:133
@ unsat
Definition: z3++.h:133
expr operator<(expr const &a, expr const &b)
Definition: z3++.h:1762
expr set_intersect(expr const &a, expr const &b)
Definition: z3++.h:3632
func_decl tree_order(sort const &a, unsigned index)
Definition: z3++.h:2143
expr forall(expr const &x, expr const &b)
Definition: z3++.h:2189
expr bvneg_no_overflow(expr const &a)
Definition: z3++.h:2118
expr set_member(expr const &s, expr const &e)
Definition: z3++.h:3648
expr set_difference(expr const &a, expr const &b)
Definition: z3++.h:3640
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3537
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:2132
expr bvadd_no_overflow(expr const &a, expr const &b, bool is_signed)
bit-vector overflow/underflow checks
Definition: z3++.h:2103
expr slt(expr const &a, expr const &b)
signed less than operator for bitvectors.
Definition: z3++.h:1999
expr bvsdiv_no_overflow(expr const &a, expr const &b)
Definition: z3++.h:2115
expr empty_set(sort const &s)
Definition: z3++.h:3608
expr plus(expr const &re)
Definition: z3++.h:3695
std::ostream & operator<<(std::ostream &out, exception const &e)
Definition: z3++.h:94
expr rem(expr const &a, expr const &b)
Definition: z3++.h:1527
expr operator!(expr const &a)
Definition: z3++.h:1545
expr fpa_fp(expr const &sgn, expr const &exp, expr const &sig)
Definition: z3++.h:1903
void set_param(char const *param, char const *value)
Definition: z3++.h:77
expr full_set(sort const &s)
Definition: z3++.h:3612
ast_vector_tpl< sort > sort_vector
Definition: z3++.h:74
expr as_array(func_decl &f)
Definition: z3++.h:3587
tactic when(probe const &p, tactic const &t)
Definition: z3++.h:3181
expr operator*(expr const &a, expr const &b)
Definition: z3++.h:1629
expr uge(expr const &a, expr const &b)
unsigned greater than or equal to operator for bitvectors.
Definition: z3++.h:2031
expr nand(expr const &a, expr const &b)
Definition: z3++.h:1818
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:2092
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3509
expr is_int(expr const &e)
Definition: z3++.h:1547
expr empty(sort const &s)
Definition: z3++.h:3660
expr operator-(expr const &a)
Definition: z3++.h:1695
expr re_complement(expr const &a)
Definition: z3++.h:3722
expr set_del(expr const &s, expr const &e)
Definition: z3++.h:3620
expr mk_or(expr_vector const &args)
Definition: z3++.h:2364
expr concat(expr const &a, expr const &b)
Definition: z3++.h:2320
tactic with(tactic const &t, params const &p)
Definition: z3++.h:2911
expr operator%(expr const &a, expr const &b)
Definition: z3++.h:1522
expr re_full(sort const &s)
Definition: z3++.h:3709
func_decl partial_order(sort const &a, unsigned index)
Definition: z3++.h:2137
tactic par_and_then(tactic const &t1, tactic const &t2)
Definition: z3++.h:2930
bool eq(ast const &a, ast const &b)
Definition: z3++.h:540
expr operator~(expr const &a)
Definition: z3++.h:1893
expr exists(expr const &x, expr const &b)
Definition: z3++.h:2213
expr ite(expr const &c, expr const &t, expr const &e)
Create the if-then-else expression ite(c, t, e)
Definition: z3++.h:1958
expr bvsub_no_underflow(expr const &a, expr const &b, bool is_signed)
Definition: z3++.h:2112
expr set_add(expr const &s, expr const &e)
Definition: z3++.h:3616
expr sum(expr_vector const &args)
Definition: z3++.h:2302
expr last_indexof(expr const &s, expr const &substr)
Definition: z3++.h:3683
expr pbge(expr_vector const &es, int const *coeffs, int bound)
Definition: z3++.h:2270
expr set_union(expr const &a, expr const &b)
Definition: z3++.h:3624
func_decl to_func_decl(context &c, Z3_func_decl f)
Definition: z3++.h:1985
tactic cond(probe const &p, tactic const &t1, tactic const &t2)
Definition: z3++.h:3187
expr sbv_to_fpa(expr const &t, sort s)
Definition: z3++.h:1925
expr ubv_to_fpa(expr const &t, sort s)
Definition: z3++.h:1932
expr operator||(expr const &a, expr const &b)
Definition: z3++.h:1563
expr const_array(sort const &d, expr const &v)
Definition: z3++.h:3604
tactic par_or(unsigned n, tactic const *tactics)
Definition: z3++.h:2921
func_decl piecewise_linear_order(sort const &a, unsigned index)
Definition: z3++.h:2140
expr operator&&(expr const &a, expr const &b)
Definition: z3++.h:1551
func_decl function(std::string const &name, sort_vector const &domain, sort const &range)
Definition: z3++.h:3533
expr atleast(expr_vector const &es, unsigned bound)
Definition: z3++.h:2294
expr atmost(expr_vector const &es, unsigned bound)
Definition: z3++.h:2286
expr operator>(expr const &a, expr const &b)
Definition: z3++.h:1784
tactic repeat(tactic const &t, unsigned max=UINT_MAX)
Definition: z3++.h:2905
expr re_empty(sort const &s)
Definition: z3++.h:3704
expr select(expr const &a, expr const &i)
forward declarations
Definition: z3++.h:3550
expr urem(expr const &a, expr const &b)
unsigned reminder operator for bitvectors
Definition: z3++.h:2064
expr in_re(expr const &s, expr const &re)
Definition: z3++.h:3692
expr to_re(expr const &s)
Definition: z3++.h:3689
expr operator/(expr const &a, expr const &b)
Definition: z3++.h:1673
expr fp_eq(expr const &a, expr const &b)
Definition: z3++.h:1886
expr bvredor(expr const &a)
Definition: z3++.h:1851
expr nor(expr const &a, expr const &b)
Definition: z3++.h:1819
expr bvmul_no_overflow(expr const &a, expr const &b, bool is_signed)
Definition: z3++.h:2121
expr min(expr const &a, expr const &b)
Definition: z3++.h:1821
expr sle(expr const &a, expr const &b)
signed less than or equal to operator for bitvectors.
Definition: z3++.h:1993
sort to_sort(context &c, Z3_sort s)
Definition: z3++.h:1980
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:144
expr ugt(expr const &a, expr const &b)
unsigned greater than operator for bitvectors.
Definition: z3++.h:2037
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:73
expr sgt(expr const &a, expr const &b)
signed greater than operator for bitvectors.
Definition: z3++.h:2011
expr lambda(expr const &x, expr const &b)
Definition: z3++.h:2237
expr to_real(expr const &a)
Definition: z3++.h:3507
rounding_mode
Definition: z3++.h:136
@ RNE
Definition: z3++.h:138
@ RNA
Definition: z3++.h:137
@ RTZ
Definition: z3++.h:141
@ RTN
Definition: z3++.h:140
@ RTP
Definition: z3++.h:139
expr operator+(expr const &a, expr const &b)
Definition: z3++.h:1599
expr int2bv(unsigned n, expr const &a)
Definition: z3++.h:2098
expr udiv(expr const &a, expr const &b)
unsigned division operator for bitvectors.
Definition: z3++.h:2043
expr prefixof(expr const &a, expr const &b)
Definition: z3++.h:3671
expr suffixof(expr const &a, expr const &b)
Definition: z3++.h:3665
expr set_complement(expr const &a)
Definition: z3++.h:3644
expr abs(expr const &a)
Definition: z3++.h:1863
expr fpa_to_sbv(expr const &t, unsigned sz)
Definition: z3++.h:1911
expr ule(expr const &a, expr const &b)
unsigned less than or equal to operator for bitvectors.
Definition: z3++.h:2019
void reset_params()
Definition: z3++.h:80
expr operator<=(expr const &a, expr const &b)
Definition: z3++.h:1737
expr option(expr const &re)
Definition: z3++.h:3698
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:1971
expr operator!=(expr const &a, expr const &b)
Definition: z3++.h:1587
tactic fail_if(probe const &p)
Definition: z3++.h:3176
ast_vector_tpl< ast > ast_vector
Definition: z3++.h:71
expr sqrt(expr const &a, expr const &rm)
Definition: z3++.h:1879
expr shl(expr const &a, expr const &b)
shift left operator for bitvectors
Definition: z3++.h:2071
expr implies(expr const &a, expr const &b)
Definition: z3++.h:1499
expr operator&(expr const &a, expr const &b)
Definition: z3++.h:1806
expr sge(expr const &a, expr const &b)
signed greater than or equal to operator for bitvectors.
Definition: z3++.h:2005
expr smod(expr const &a, expr const &b)
signed modulus operator for bitvectors
Definition: z3++.h:2057
expr set_subset(expr const &a, expr const &b)
Definition: z3++.h:3652
expr ult(expr const &a, expr const &b)
unsigned less than operator for bitvectors.
Definition: z3++.h:2025
expr pw(expr const &a, expr const &b)
Definition: z3++.h:1507
expr ashr(expr const &a, expr const &b)
arithmetic shift right operator for bitvectors
Definition: z3++.h:2085
expr xnor(expr const &a, expr const &b)
Definition: z3++.h:1820
expr bvredand(expr const &a)
Definition: z3++.h:1857
tactic try_for(tactic const &t, unsigned ms)
Definition: z3++.h:2916
expr fpa_to_fpa(expr const &t, sort s)
Definition: z3++.h:1939
def tactics(ctx=None)
Definition: z3py.py:8323
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1492
#define MK_EXPR1(_fn, _arg)
Definition: z3++.h:3593
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition: z3++.h:3598
#define Z3_THROW(x)
Definition: z3++.h:100
#define _Z3_MK_UN_(a, mkun)
Definition: z3++.h:1539
Z3_ast_vector Z3_API Z3_algebraic_get_poly(Z3_context c, Z3_ast a)
Return the coefficients of the defining polynomial.
unsigned Z3_API Z3_algebraic_get_i(Z3_context c, Z3_ast a)
Return which root of the polynomial the algebraic number represents.
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:1337
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:180
@ Z3_APP_AST
Definition: z3_api.h:182
@ Z3_VAR_AST
Definition: z3_api.h:183
@ Z3_SORT_AST
Definition: z3_api.h:185
@ Z3_NUMERAL_AST
Definition: z3_api.h:181
@ Z3_FUNC_DECL_AST
Definition: z3_api.h:186
@ Z3_QUANTIFIER_AST
Definition: z3_api.h:184
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:1408
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_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.
unsigned Z3_API Z3_solver_propagate_register(Z3_context c, Z3_solver s, Z3_ast e)
register an expression to propagate on with the solver. Only expressions of type Bool and type Bit-Ve...
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:1000
@ Z3_OP_DISTINCT
Definition: z3_api.h:1005
@ Z3_OP_AND
Definition: z3_api.h:1007
@ Z3_OP_FALSE
Definition: z3_api.h:1003
@ Z3_OP_XOR
Definition: z3_api.h:1010
@ Z3_OP_IMPLIES
Definition: z3_api.h:1012
@ Z3_OP_ITE
Definition: z3_api.h:1006
@ Z3_OP_EQ
Definition: z3_api.h:1004
@ Z3_OP_OR
Definition: z3_api.h:1008
@ Z3_OP_NOT
Definition: z3_api.h:1011
@ Z3_OP_TRUE
Definition: z3_api.h:1002
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_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision)
Return a lower bound for the given real algebraic number. The interval isolating the number is smalle...
Z3_char_ptr 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_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:1317
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition: z3_api.h:84
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:150
@ Z3_RELATION_SORT
Definition: z3_api.h:158
@ Z3_BOOL_SORT
Definition: z3_api.h:152
@ Z3_BV_SORT
Definition: z3_api.h:155
@ Z3_DATATYPE_SORT
Definition: z3_api.h:157
@ Z3_INT_SORT
Definition: z3_api.h:153
@ Z3_FINITE_DOMAIN_SORT
Definition: z3_api.h:159
@ Z3_RE_SORT
Definition: z3_api.h:163
@ Z3_FLOATING_POINT_SORT
Definition: z3_api.h:160
@ Z3_ARRAY_SORT
Definition: z3_api.h:156
@ Z3_REAL_SORT
Definition: z3_api.h:154
@ Z3_SEQ_SORT
Definition: z3_api.h:162
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_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:102
@ Z3_L_TRUE
Definition: z3_api.h:105
@ Z3_L_FALSE
Definition: z3_api.h:103
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_string Z3_API Z3_sort_to_string(Z3_context c, Z3_sort s)
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.
void Z3_API Z3_solver_propagate_final(Z3_context c, Z3_solver s, Z3_final_eh final_eh)
register a callback on final check. This provides freedom to the propagator to delay actions or imple...
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_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g, bool include_names)
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_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_get_algebraic_number_upper(Z3_context c, Z3_ast a, unsigned precision)
Return a upper bound for the given real algebraic number. The interval isolating the number is smalle...
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_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:116
@ Z3_STRING_SYMBOL
Definition: z3_api.h:118
@ Z3_INT_SYMBOL
Definition: z3_api.h:117
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...
void Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback, unsigned num_fixed, unsigned const *fixed_ids, unsigned num_eqs, unsigned const *eq_lhs, unsigned const *eq_rhs, Z3_ast conseq)
propagate a consequence based on fixed values. This is a callback a client may invoke during the fixe...
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:1359
@ Z3_OK
Definition: z3_api.h:1360
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.
bool Z3_API Z3_is_string(Z3_context c, Z3_ast s)
Determine if s is a string constant.
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 but two different AST objects can m...
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_xor(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 xor t2.
void Z3_API Z3_solver_propagate_eq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh)
register a callback on expression equalities.
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.
Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s, bool include_names)
Convert a solver into a DIMACS formatted string.
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 decimal string of a numeric constant term.
void Z3_API Z3_solver_propagate_fixed(Z3_context c, Z3_solver s, Z3_fixed_eh fixed_eh)
register a callback for when an expression is bound to a fixed value. The supported expression types ...
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_string Z3_API Z3_get_numeral_binary_string(Z3_context c, Z3_ast a)
Return numeral value, as a binary string of a numeric constant term.
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_bvredor(Z3_context c, Z3_ast t1)
Take disjunction of bits in vector, return vector of length 1.
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_ast_vector Z3_API Z3_ast_vector_translate(Z3_context s, Z3_ast_vector v, Z3_context t)
Translate the AST vector v from context s into an AST vector in context t.
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_is_infinite(Z3_context c, Z3_ast t)
Predicate indicating whether t is a floating-point number representing +oo or -oo.
Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s)
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
Z3_ast Z3_API Z3_mk_fpa_is_subnormal(Z3_context c, Z3_ast t)
Predicate indicating whether t is a subnormal floating-point number.
Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t)
Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)
Conversion of a floating-point term into a signed bit-vector.
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.
Z3_ast Z3_API Z3_mk_fpa_is_normal(Z3_context c, Z3_ast t)
Predicate indicating whether t is a normal floating-point number.
Z3_ast Z3_API Z3_mk_fpa_to_ubv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)
Conversion of a floating-point term into an unsigned bit-vector.
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_inf(Z3_context c, Z3_sort s, bool negative)
Create a floating-point infinity of sort s.
Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s)
Create a floating-point NaN of sort s.
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_is_zero(Z3_context c, Z3_ast t)
Predicate indicating whether t is a floating-point number with zero value, i.e., +zero or -zero.
Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point equality.
Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than or equal.
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_round_to_integral(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point roundToIntegral. Rounds a floating-point number to the closest integer,...
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_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort.
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_is_nan(Z3_context c, Z3_ast t)
Predicate indicating whether t is a NaN.
Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig)
Create an expression of FloatingPoint sort from three bit-vector expressions.
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_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
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_sort Z3_API Z3_mk_fpa_rounding_mode_sort(Z3_context c)
Create the RoundingMode sort.
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.