84 char const *
msg()
const {
return m_msg.c_str(); }
101 operator Z3_config()
const {
return m_cfg; }
109 void set(
char const * param,
bool value) {
Z3_set_param_value(m_cfg, param, value ?
"true" :
"false"); }
113 void set(
char const * param,
int value) {
114 std::ostringstream oss;
143 void init_interp(
config & c) {
157 operator Z3_context()
const {
return m_ctx; }
179 void set(
char const * param,
int value) {
180 std::ostringstream oss;
194 symbol str_symbol(
char const * s);
214 sort bv_sort(
unsigned sz);
238 sort enumeration_sort(
char const * name,
unsigned n,
char const *
const * enum_names, func_decl_vector & cs, func_decl_vector & ts);
242 sort uninterpreted_sort(
char const* name);
246 func_decl function(
char const * name,
unsigned arity,
sort const * domain,
sort const & range);
248 func_decl function(
char const * name, sort_vector
const& domain,
sort const& range);
256 expr constant(
char const * name,
sort const & s);
257 expr bool_const(
char const * name);
258 expr int_const(
char const * name);
259 expr real_const(
char const * name);
260 expr bv_const(
char const * name,
unsigned sz);
262 expr bool_val(
bool b);
265 expr int_val(
unsigned n);
268 expr int_val(
char const * n);
270 expr real_val(
int n,
int d);
271 expr real_val(
int n);
272 expr real_val(
unsigned n);
275 expr real_val(
char const * n);
277 expr bv_val(
int n,
unsigned sz);
278 expr bv_val(
unsigned n,
unsigned sz);
281 expr bv_val(
char const * n,
unsigned sz);
283 expr string_val(
char const* s);
284 expr string_val(std::string
const& s);
286 expr num_val(
int n,
sort const & s);
291 expr parse_string(
char const* s);
292 expr parse_file(
char const* file);
294 expr parse_string(
char const* s, sort_vector
const& sorts, func_decl_vector
const& decls);
295 expr parse_file(
char const* s, sort_vector
const& sorts, func_decl_vector
const& decls);
301 expr_vector get_interpolant(
expr const& proof,
expr const& pat,
params const& p);
315 array(
unsigned sz):m_size(sz) { m_array =
new T[sz]; }
316 template<
typename T2>
319 unsigned size()
const {
return m_size; }
320 T &
operator[](
int i) { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size);
return m_array[i]; }
321 T
const &
operator[](
int i)
const { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size);
return m_array[i]; }
322 T
const *
ptr()
const {
return m_array; }
323 T *
ptr() {
return m_array; }
331 object(
object const & s):m_ctx(s.m_ctx) {}
334 friend void check_context(
object const & a,
object const & b);
344 operator Z3_symbol()
const {
return m_sym; }
346 std::string
str()
const { assert(kind() ==
Z3_STRING_SYMBOL);
return Z3_get_symbol_string(ctx(), m_sym); }
353 out <<
"k!" << s.
to_int();
355 out << s.
str().c_str();
361 Z3_param_descrs m_descrs;
368 m_descrs = o.m_descrs;
390 operator Z3_params()
const {
return m_params; }
395 m_params = s.m_params;
399 void set(
char const * k,
unsigned n) {
Z3_params_set_uint(ctx(), m_params, ctx().str_symbol(k), n); }
417 operator Z3_ast()
const {
return m_ast; }
418 operator bool()
const {
return m_ast != 0; }
421 unsigned hash()
const {
unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error();
return r; }
422 friend std::ostream &
operator<<(std::ostream & out,
ast const & n);
427 friend bool eq(
ast const & a,
ast const & b);
433 inline bool eq(
ast const & a,
ast const & b) {
return Z3_is_eq_ast(a.
ctx(), a, b) != 0; }
444 operator Z3_sort()
const {
return reinterpret_cast<Z3_sort
>(m_ast); }
456 symbol name()
const { Z3_symbol s = Z3_get_sort_name(ctx(), *
this); check_error();
return symbol(ctx(), s); }
507 unsigned bv_size()
const { assert(
is_bv());
unsigned r = Z3_get_bv_sort_size(ctx(), *
this); check_error();
return r; }
532 operator Z3_func_decl()
const {
return reinterpret_cast<Z3_func_decl
>(m_ast); }
535 unsigned arity()
const {
return Z3_get_arity(ctx(), *
this); }
536 sort domain(
unsigned i)
const { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *
this, i); check_error();
return sort(ctx(), r); }
537 sort range()
const { Z3_sort r = Z3_get_range(ctx(), *
this); check_error();
return sort(ctx(), r); }
538 symbol name()
const { Z3_symbol s = Z3_get_decl_name(ctx(), *
this); check_error();
return symbol(ctx(), s); }
543 expr operator()()
const;
544 expr operator()(
unsigned n,
expr const * args)
const;
545 expr operator()(expr_vector
const& v)
const;
546 expr operator()(
expr const & a)
const;
547 expr operator()(
int a)
const;
548 expr operator()(
expr const & a1,
expr const & a2)
const;
549 expr operator()(
expr const & a1,
int a2)
const;
550 expr operator()(
int a1,
expr const & a2)
const;
570 sort get_sort()
const { Z3_sort s = Z3_get_sort(*m_ctx, m_ast); check_error();
return sort(*m_ctx, s); }
575 bool is_bool()
const {
return get_sort().is_bool(); }
579 bool is_int()
const {
return get_sort().is_int(); }
583 bool is_real()
const {
return get_sort().is_real(); }
587 bool is_arith()
const {
return get_sort().is_arith(); }
591 bool is_bv()
const {
return get_sort().is_bv(); }
595 bool is_array()
const {
return get_sort().is_array(); }
607 bool is_seq()
const {
return get_sort().is_seq(); }
611 bool is_re()
const {
return get_sort().is_re(); }
654 bool is_algebraic()
const {
return 0 != Z3_is_algebraic_number(ctx(), m_ast); }
659 bool is_well_sorted()
const {
bool r = Z3_is_well_sorted(ctx(), m_ast) != 0; check_error();
return r; }
668 assert(is_numeral() || is_algebraic());
680 if (!is_numeral_i(result)) {
681 throw exception(
"numeral does not fit in machine int");
693 assert(is_numeral());
695 if (!is_numeral_u(result)) {
696 throw exception(
"numeral does not fit in machine uint");
708 assert(is_numeral());
710 if (!is_numeral_i64(result)) {
711 throw exception(
"numeral does not fit in machine __int64");
723 assert(is_numeral());
725 if (!is_numeral_u64(result)) {
726 throw exception(
"numeral does not fit in machine __uint64");
732 operator Z3_app()
const { assert(
is_app());
return reinterpret_cast<Z3_app
>(m_ast); }
747 unsigned num_args()
const {
unsigned r = Z3_get_app_num_args(ctx(), *
this); check_error();
return r; }
755 expr arg(
unsigned i)
const { Z3_ast r = Z3_get_app_arg(ctx(), *
this, i); check_error();
return expr(ctx(), r); }
823 friend expr mk_or(expr_vector
const& args);
871 friend expr wasoperator(
expr const & a,
expr const & b);
897 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)); }
898 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)); }
907 Z3_ast r = Z3_mk_seq_extract(ctx(), *
this, offset, length); check_error();
return expr(ctx(), r);
911 Z3_ast r = Z3_mk_seq_replace(ctx(), *
this, src, dst);
913 return expr(ctx(), r);
916 Z3_ast r = Z3_mk_seq_unit(ctx(), *
this);
918 return expr(ctx(), r);
922 Z3_ast r = Z3_mk_seq_contains(ctx(), *
this, s);
924 return expr(ctx(), r);
928 Z3_ast r = Z3_mk_seq_at(ctx(), *
this, index);
930 return expr(ctx(), r);
933 Z3_ast r = Z3_mk_seq_length(ctx(), *
this);
935 return expr(ctx(), r);
993 Z3_ast args[2] = { a, b };
1005 Z3_ast args[2] = { a, b };
1026 Z3_ast args[2] = { a, b };
1038 Z3_ast args[2] = { a, b };
1048 Z3_ast _args[2] = { a, b };
1049 r = Z3_mk_re_union(a.
ctx(), 2, _args);
1065 Z3_ast args[2] = { a, b };
1123 else if (a.
is_bv()) {
1138 Z3_ast args[2] = { a, b };
1252 assert(Z3_get_ast_kind(c, a) ==
Z3_APP_AST ||
1367 return sort(c, reinterpret_cast<Z3_sort>(a));
1375 return func_decl(c, reinterpret_cast<Z3_func_decl>(a));
1379 template<
typename T>
1381 Z3_ast_vector m_vector;
1382 void init(Z3_ast_vector v) { Z3_ast_vector_inc_ref(ctx(), v); m_vector = v; }
1388 operator Z3_ast_vector()
const {
return m_vector; }
1389 unsigned size()
const {
return Z3_ast_vector_size(ctx(), m_vector); }
1390 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); }
1391 void push_back(T
const & e) { Z3_ast_vector_push(ctx(), m_vector, e); check_error(); }
1392 void resize(
unsigned sz) { Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }
1393 T
back()
const {
return operator[](size() - 1); }
1394 void pop_back() { assert(size() > 0); resize(size() - 1); }
1395 bool empty()
const {
return size() == 0; }
1397 Z3_ast_vector_inc_ref(s.
ctx(), s.m_vector);
1398 Z3_ast_vector_dec_ref(ctx(), m_vector);
1400 m_vector = s.m_vector;
1407 template<
typename T>
1408 template<
typename T2>
1410 m_array =
new T[v.
size()];
1412 for (
unsigned i = 0; i < m_size; i++) {
1421 Z3_app vars[] = {(Z3_app) x};
1422 Z3_ast r = Z3_mk_forall_const(b.
ctx(), 0, 1, vars, 0, 0, b); b.
check_error();
return expr(b.
ctx(), r);
1426 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1427 Z3_ast r = Z3_mk_forall_const(b.
ctx(), 0, 2, vars, 0, 0, b); b.
check_error();
return expr(b.
ctx(), r);
1431 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1432 Z3_ast r = Z3_mk_forall_const(b.
ctx(), 0, 3, vars, 0, 0, b); b.
check_error();
return expr(b.
ctx(), r);
1436 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1437 Z3_ast r = Z3_mk_forall_const(b.
ctx(), 0, 4, vars, 0, 0, b); b.
check_error();
return expr(b.
ctx(), r);
1445 Z3_app vars[] = {(Z3_app) x};
1446 Z3_ast r = Z3_mk_exists_const(b.
ctx(), 0, 1, vars, 0, 0, b); b.
check_error();
return expr(b.
ctx(), r);
1450 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1451 Z3_ast r = Z3_mk_exists_const(b.
ctx(), 0, 2, vars, 0, 0, b); b.
check_error();
return expr(b.
ctx(), r);
1455 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1456 Z3_ast r = Z3_mk_exists_const(b.
ctx(), 0, 3, vars, 0, 0, b); b.
check_error();
return expr(b.
ctx(), r);
1460 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1461 Z3_ast r = Z3_mk_exists_const(b.
ctx(), 0, 4, vars, 0, 0, b); b.
check_error();
return expr(b.
ctx(), r);
1470 assert(args.
size() > 0);
1475 return expr(ctx, r);
1482 Z3_ast _args[2] = { a, b };
1483 r = Z3_mk_seq_concat(a.
ctx(), 2, _args);
1486 Z3_ast _args[2] = { a, b };
1487 r = Z3_mk_re_concat(a.
ctx(), 2, _args);
1498 assert(args.
size() > 0);
1499 if (args.
size() == 1) {
1504 if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
1505 r = Z3_mk_seq_concat(ctx, _args.
size(), _args.
ptr());
1507 else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
1508 r = Z3_mk_re_concat(ctx, _args.
size(), _args.
ptr());
1511 r = _args[args.
size()-1];
1512 for (
unsigned i = args.
size()-1; i > 0; ) {
1519 return expr(ctx, r);
1537 Z3_func_entry m_entry;
1538 void init(Z3_func_entry e) {
1546 operator Z3_func_entry()
const {
return m_entry; }
1551 m_entry = s.m_entry;
1560 Z3_func_interp m_interp;
1561 void init(Z3_func_interp e) {
1569 operator Z3_func_interp()
const {
return m_interp; }
1574 m_interp = s.m_interp;
1584 void init(Z3_model m) {
1592 operator Z3_model()
const {
return m_model; }
1597 m_model = s.m_model;
1607 throw exception(
"failed to evaluate expression");
1608 return expr(ctx(), r);
1615 unsigned size()
const {
return num_consts() + num_funcs(); }
1618 return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
1628 return expr(ctx(), r);
1644 friend std::ostream &
operator<<(std::ostream & out,
model const & m);
1650 void init(Z3_stats e) {
1659 operator Z3_stats()
const {
return m_stats; }
1664 m_stats = s.m_stats;
1673 friend std::ostream &
operator<<(std::ostream & out,
stats const & s);
1679 if (r ==
unsat) out <<
"unsat";
1680 else if (r ==
sat) out <<
"sat";
1681 else out <<
"unknown";
1688 void init(Z3_solver s) {
1702 operator Z3_solver()
const {
return m_solver; }
1707 m_solver = s.m_solver;
1721 add(e, ctx().bool_const(p));
1726 for (
unsigned i = 0; i < n; i++) {
1728 _assumptions[i] = assumptions[i];
1735 unsigned n = assumptions.
size();
1737 for (
unsigned i = 0; i < n; i++) {
1739 _assumptions[i] = assumptions[i];
1758 std::string
to_smt2(
char const* status =
"unknown") {
1760 Z3_ast
const* fmls = es.
ptr();
1762 unsigned sz = es.
size();
1768 fml = ctx().bool_val(
true);
1784 void init(Z3_goal s) {
1793 operator Z3_goal()
const {
return m_goal; }
1812 unsigned n = size();
1814 return ctx().bool_val(
true);
1816 return operator[](0);
1819 for (
unsigned i = 0; i < n; i++)
1820 args[i] =
operator[](i);
1824 friend std::ostream &
operator<<(std::ostream & out,
goal const & g);
1829 Z3_apply_result m_apply_result;
1830 void init(Z3_apply_result s) {
1838 operator Z3_apply_result()
const {
return m_apply_result; }
1843 m_apply_result = s.m_apply_result;
1852 return model(ctx(), new_m);
1860 void init(Z3_tactic s) {
1869 operator Z3_tactic()
const {
return m_tactic; }
1874 m_tactic = s.m_tactic;
1930 void init(Z3_probe s) {
1940 operator Z3_probe()
const {
return m_probe; }
1945 m_probe = s.m_probe;
2012 unsigned h()
const {
return m_h; }
2016 operator Z3_optimize()
const {
return m_opt; }
2019 Z3_optimize_assert(ctx(), m_opt, e);
2023 std::stringstream strm;
2025 return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, strm.str().c_str(), 0));
2029 return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0));
2032 return handle(Z3_optimize_maximize(ctx(), m_opt, e));
2035 return handle(Z3_optimize_minimize(ctx(), m_opt, e));
2038 Z3_optimize_push(ctx(), m_opt);
2041 Z3_optimize_pop(ctx(), m_opt);
2044 model get_model()
const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error();
return model(ctx(), m); }
2045 void set(
params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }
2047 Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.
h());
2049 return expr(ctx(), r);
2052 Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.
h());
2054 return expr(ctx(), r);
2056 expr_vector
assertions()
const { Z3_ast_vector r = Z3_optimize_get_assertions(ctx(), m_opt); check_error();
return expr_vector(ctx(), r); }
2057 expr_vector
objectives()
const { Z3_ast_vector r = Z3_optimize_get_objectives(ctx(), m_opt); check_error();
return expr_vector(ctx(), r); }
2058 stats statistics()
const { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error();
return stats(ctx(), r); }
2060 void from_file(
char const* filename) { Z3_optimize_from_file(ctx(), m_opt, filename); check_error(); }
2061 void from_string(
char const* constraints) { Z3_optimize_from_string(ctx(), m_opt, constraints); check_error(); }
2062 std::string
help()
const {
char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error();
return r; }
2064 inline std::ostream &
operator<<(std::ostream & out,
optimize const & s) { out << Z3_optimize_to_string(s.
ctx(), s.m_opt);
return out; }
2081 return tactic(t1.ctx(), r);
2098 for (
unsigned i = 0; i < n; i++) { _enum_names[i] =
Z3_mk_string_symbol(*
this, enum_names[i]); }
2117 for (
unsigned i = 0; i < arity; i++) {
2119 args[i] = domain[i];
2127 return function(range.
ctx().
str_symbol(name), arity, domain, range);
2132 for (
unsigned i = 0; i < domain.
size(); i++) {
2134 args[i] = domain[i];
2142 return function(range.
ctx().
str_symbol(name), domain, range);
2148 Z3_sort args[1] = { domain };
2149 Z3_func_decl f =
Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
2156 Z3_sort args[2] = { d1, d2 };
2157 Z3_func_decl f =
Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
2164 Z3_sort args[3] = { d1, d2, d3 };
2165 Z3_func_decl f =
Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
2172 Z3_sort args[4] = { d1, d2, d3, d4 };
2173 Z3_func_decl f =
Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
2180 Z3_sort args[5] = { d1, d2, d3, d4, d5 };
2181 Z3_func_decl f =
Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
2189 return expr(*
this, r);
2200 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); }
2212 inline expr context::bv_val(
int n,
unsigned sz) { Z3_ast r = Z3_mk_int(m_ctx, n, bv_sort(sz)); check_error();
return expr(*
this, r); }
2213 inline expr context::bv_val(
unsigned n,
unsigned sz) { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, bv_sort(sz)); check_error();
return expr(*
this, r); }
2216 inline expr context::bv_val(
char const * n,
unsigned sz) { Z3_ast r = Z3_mk_numeral(m_ctx, n, bv_sort(sz)); check_error();
return expr(*
this, r); }
2225 for (
unsigned i = 0; i < n; i++) {
2231 return expr(ctx(), r);
2236 for (
unsigned i = 0; i < args.
size(); i++) {
2240 Z3_ast r =
Z3_mk_app(ctx(), *
this, args.
size(), _args.ptr());
2242 return expr(ctx(), r);
2245 Z3_ast r =
Z3_mk_app(ctx(), *
this, 0, 0);
2246 ctx().check_error();
2247 return expr(ctx(), r);
2251 Z3_ast args[1] = { a };
2252 Z3_ast r =
Z3_mk_app(ctx(), *
this, 1, args);
2253 ctx().check_error();
2254 return expr(ctx(), r);
2257 Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
2258 Z3_ast r =
Z3_mk_app(ctx(), *
this, 1, args);
2259 ctx().check_error();
2260 return expr(ctx(), r);
2264 Z3_ast args[2] = { a1, a2 };
2265 Z3_ast r =
Z3_mk_app(ctx(), *
this, 2, args);
2266 ctx().check_error();
2267 return expr(ctx(), r);
2271 Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
2272 Z3_ast r =
Z3_mk_app(ctx(), *
this, 2, args);
2273 ctx().check_error();
2274 return expr(ctx(), r);
2278 Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
2279 Z3_ast r =
Z3_mk_app(ctx(), *
this, 2, args);
2280 ctx().check_error();
2281 return expr(ctx(), r);
2285 Z3_ast args[3] = { a1, a2, a3 };
2286 Z3_ast r =
Z3_mk_app(ctx(), *
this, 3, args);
2287 ctx().check_error();
2288 return expr(ctx(), r);
2292 Z3_ast args[4] = { a1, a2, a3, a4 };
2293 Z3_ast r =
Z3_mk_app(ctx(), *
this, 4, args);
2294 ctx().check_error();
2295 return expr(ctx(), r);
2299 Z3_ast args[5] = { a1, a2, a3, a4, a5 };
2300 Z3_ast r =
Z3_mk_app(ctx(), *
this, 5, args);
2301 ctx().check_error();
2302 return expr(ctx(), r);
2308 return range.
ctx().
function(name, arity, domain, range);
2310 inline func_decl function(
char const * name,
unsigned arity,
sort const * domain,
sort const & range) {
2311 return range.
ctx().
function(name, arity, domain, range);
2320 return range.
ctx().
function(name, d1, d2, d3, range);
2323 return range.
ctx().
function(name, d1, d2, d3, d4, range);
2326 return range.
ctx().
function(name, d1, d2, d3, d4, d5, range);
2348 #define MK_EXPR1(_fn, _arg) \ 2349 Z3_ast r = _fn(_arg.ctx(), _arg); \ 2350 _arg.check_error(); \ 2351 return expr(_arg.ctx(), r); 2353 #define MK_EXPR2(_fn, _arg1, _arg2) \ 2354 check_context(_arg1, _arg2); \ 2355 Z3_ast r = _fn(_arg1.ctx(), _arg1, _arg2); \ 2356 _arg1.check_error(); \ 2357 return expr(_arg1.ctx(), r); 2381 Z3_ast es[2] = { a, b };
2389 Z3_ast es[2] = { a, b };
2416 Z3_ast r = Z3_mk_seq_empty(s.
ctx(), s);
2422 Z3_ast r = Z3_mk_seq_suffix(a.
ctx(), a, b);
2428 Z3_ast r = Z3_mk_seq_prefix(a.
ctx(), a, b);
2434 Z3_ast r = Z3_mk_seq_index(s.
ctx(), s, substr, offset);
2439 Z3_ast r = Z3_mk_seq_to_re(s.
ctx(), s);
2445 Z3_ast r = Z3_mk_seq_in_re(s.
ctx(), s, re);
2450 Z3_ast r = Z3_mk_re_plus(re.
ctx(), re);
2455 Z3_ast r = Z3_mk_re_option(re.
ctx(), re);
2460 Z3_ast r = Z3_mk_re_star(re.
ctx(), re);
2472 return expr(*
this, r);
2478 return expr(*
this, r);
2486 for (
unsigned i = 0; i < sorts.
size(); ++i) {
2487 sort_names[i] = sorts[i].name();
2489 for (
unsigned i = 0; i < decls.
size(); ++i) {
2490 decl_names[i] = decls[i].name();
2494 return expr(*
this, r);
2502 for (
unsigned i = 0; i < sorts.
size(); ++i) {
2503 sort_names[i] = sorts[i].name();
2505 for (
unsigned i = 0; i < decls.
size(); ++i) {
2506 decl_names[i] = decls[i].name();
2510 return expr(*
this, r);
2515 Z3_ast_vector interp = 0;
2523 m =
model(*
this, mdl);
2539 for (
unsigned i = 0; i < src.
size(); ++i) {
2545 return expr(ctx(), r);
2550 for (
unsigned i = 0; i < dst.
size(); ++i) {
2555 return expr(ctx(), r);
ast_vector_tpl(context &c)
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_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...
expr distinct(expr_vector const &args)
bool is_uint(unsigned i) const
Z3_ast Z3_API Z3_mk_true(Z3_context c)
Create an AST node representing true.
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).
Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s)
Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.
Z3_sort_kind
The different kinds of Z3 types (See #Z3_get_sort_kind).
expr parse_string(char const *s)
parsing
Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)
Create a bit-vector type of the given size.
void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value)
Set a global (or module) parameter. This setting is shared by all Z3 contexts.
sort bool_sort()
Return the Boolean sort.
void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)
Decrement the reference counter of the given probe.
expr get_const_interp(func_decl c) const
expr mk_and(expr_vector const &args)
bool is_decided_unsat() const
Z3_ast Z3_API Z3_mk_false(Z3_context c)
Create an AST node representing false.
tactic & operator=(tactic const &s)
bool is_bool() const
Return true if this sort is the Boolean sort.
sort re_sort(sort &seq_sort)
Return a regular expression sort over sequences seq_sort.
bool is_datatype() const
Return true if this is a Datatype expression.
probe(context &c, Z3_probe s)
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
unsigned uint_value(unsigned i) const
probe & operator=(probe const &s)
func_entry entry(unsigned i) const
Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err)
Return a string describing the given error code.
Z3_ast Z3_API Z3_mk_interpolant(Z3_context c, Z3_ast a)
Create an AST node marking a formula position for interpolation.
double double_value(unsigned i) const
std::string documentation(symbol const &s)
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_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.
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f)
Increment the reference counter of the given Z3_func_interp object.
expr zext(expr const &a, unsigned i)
Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i...
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.
void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t)
Increment the reference counter of the given tactic.
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.
void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g)
Erase all formulas from the given goal.
Z3_params Z3_API Z3_mk_params(Z3_context c)
Create a Z3 (empty) parameter set. Starting at Z3 4.0, parameter sets are used to configure many comp...
expr operator[](int i) const
expr contains(expr const &s)
func_decl get_const_decl(unsigned i) const
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
tactic cond(probe const &p, tactic const &t1, tactic const &t2)
Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s)
Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
expr extract(expr const &offset, expr const &length) const
sequence and regular expression operations.
solver(context &c, simple)
void Z3_API Z3_params_set_uint(Z3_context c, Z3_params p, Z3_symbol k, unsigned v)
Add a unsigned parameter k with value v to the parameter set p.
expr bv_val(int n, unsigned sz)
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than.
expr operator!=(expr const &a, expr const &b)
Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2)
Logical shift right.
Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i)
Return the declaration of the i-th function in the given model.
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
func_interp & operator=(func_interp const &s)
Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2)
Arithmetic shift right.
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...
func_decl get_func_decl(unsigned i) const
probe(context &c, double val)
expr select(expr const &a, expr const &i)
expr operator &(expr const &a, expr const &b)
Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v)
Array update.
func_entry & operator=(func_entry const &s)
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
void check_error() const
Auxiliary method used to check for API usage errors.
Z3_ast Z3_API Z3_goal_formula(Z3_context c, Z3_goal g, unsigned idx)
Return a formula from the given goal.
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.
tactic when(probe const &p, tactic const &t)
bool is_algebraic() const
Return true if expression is an algebraic number.
unsigned get_numeral_uint() const
Return uint value of numeral, throw if result cannot fit in machine uint.
expr lower(handle const &h)
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_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
expr extract(unsigned hi, unsigned lo) const
A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort.
Z3_ast Z3_API Z3_substitute(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const from[], Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs. The result is the new AST. The arrays from and to must have size num_exprs. For every i smaller than num_exprs, we must have that sort of from[i] must be equal to sort of to[i].
sort array_domain() const
Return the domain of this Array sort.
T operator[](int i) const
Z3_bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx)
Return Z3_TRUE if the given statistical data is a double.
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
__uint64 get_numeral_uint64() const
Return __uint64 value of numeral, throw if result cannot fit in __uint64.
Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than.
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...
expr full_set(sort const &s)
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.
unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g)
Return the number of formulas in the given goal.
sort array_range() const
Return the range of this Array sort.
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem)
Remove an element to a set.
T const & operator[](int i) const
Z3_ast Z3_API Z3_mk_set_union(Z3_context c, unsigned num_args, Z3_ast const args[])
Take the union of a list of sets.
sort bv_sort(unsigned sz)
Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz.
Z3_func_decl Z3_API Z3_model_get_const_decl(Z3_context c, Z3_model m, unsigned i)
Return the i-th constant in the given model.
void interrupt()
Interrupt the current procedure being executed by any object managed by this context. This is a soft interruption: there is no guarantee the object will actualy stop.
expr lshr(expr const &a, expr const &b)
logic shift right operator for bitvectors
expr udiv(expr const &a, expr const &b)
unsigned division operator for bitvectors.
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
Z3_symbol Z3_API Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, unsigned i)
Return the number of parameters in the given parameter description set.
bool is_bv() const
Return true if this is a Bit-vector expression.
expr upper(handle const &h)
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Z3_error_code
Z3 error codes (See Z3_get_error_code).
goal(context &c, Z3_goal s)
Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].
std::string to_string() const
expr_vector assertions() const
Z3_ast Z3_API Z3_parse_smtlib2_file(Z3_context c, Z3_string file_name, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Similar to Z3_parse_smtlib2_string, but reads the benchmark from a file.
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.
model(context &c, Z3_model m)
sort array_sort(sort d, sort r)
Return an array sort for arrays from d to r.
expr constant(symbol const &name, sort const &s)
Z3_bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g)
Return true if the goal contains false, and it is precise or the product of an over approximation...
Z3_ast Z3_API Z3_func_entry_get_arg(Z3_context c, Z3_func_entry e, unsigned i)
Return an argument of a Z3_func_entry object.
int Z3_bool
Z3 Boolean type. It is just an alias for int.
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.
double operator()(goal const &g) const
bool is_real() const
Return true if this is a real expression.
Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than or equal to.
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
bool is_datatype() const
Return true if this sort is a Datatype sort.
func_decl operator[](int i) const
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.
bool is_array() const
Return true if this is a Array expression.
sort operator()(context &c, Z3_ast a)
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.
expr operator^(expr const &a, expr const &b)
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)
Create the constant array.
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.
std::string get_decimal_string(int precision) const
Return string representation of numeral or algebraic number This method assumes the expression is num...
Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].
void from_string(char const *constraints)
Z3_bool Z3_API Z3_goal_is_decided_sat(Z3_context c, Z3_goal g)
Return true if the goal is empty, and it is precise or the product of a under approximation.
Exception used to sign API usage errors.
expr operator*(expr const &a, expr const &b)
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
Z3_ast Z3_API Z3_parse_smtlib2_string(Z3_context c, Z3_string str, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Parse the given string using the SMT-LIB2 parser.
Z3_context Z3_API Z3_mk_context_rc(Z3_config c)
Create a context using the given configuration. This function is similar to Z3_mk_context. However, in the context returned by this function, the user is responsible for managing Z3_ast reference counters. Managing reference counters is a burden and error-prone, but allows the user to use the memory more efficiently. The user must invoke Z3_inc_ref for any Z3_ast returned by Z3, and Z3_dec_ref whenever the Z3_ast is not needed anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD.
ast_vector_tpl(context &c, Z3_ast_vector v)
A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort ...
void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value)
Set a value of a context parameter.
bool is_int() const
Return true if this sort is the Integer sort.
expr operator!(expr const &a)
expr set_subset(expr const &a, expr const &b)
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)
Create the empty set.
#define MK_EXPR2(_fn, _arg1, _arg2)
expr & operator=(expr const &n)
expr ule(expr const &a, expr const &b)
unsigned less than or equal to operator for bitvectors.
expr in_re(expr const &s, expr const &re)
std::string key(unsigned i) const
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...
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
static param_descrs simplify_param_descrs(context &c)
sort domain(unsigned i) const
expr parse_file(char const *file)
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_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...
func_decl operator()(context &c, Z3_ast a)
void Z3_API Z3_func_interp_dec_ref(Z3_context c, Z3_func_interp f)
Decrement the reference counter of the given Z3_func_interp object.
ast_vector_tpl< func_decl > func_decl_vector
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.
expr operator>=(expr const &a, expr const &b)
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.
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.
bool is_re() const
Return true if this is a regular expression.
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...
expr pw(expr const &a, expr const &b)
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.
Z3_string Z3_API Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p)
Convert a parameter description set into a string. This function is mainly used for printing the cont...
context(config &c, interpolation)
expr(context &c, Z3_ast n)
expr set_difference(expr const &a, expr const &b)
Z3_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.
expr operator~(expr const &a)
unsigned num_entries() const
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.
Z3_error_code Z3_API Z3_get_error_code(Z3_context c)
Return the error code for the last API call.
check_result check(unsigned n, expr *const assumptions)
check_result check(expr_vector assumptions)
probe(context &c, char const *name)
Z3_symbol_kind kind() const
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
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...
sort seq_sort(sort &s)
Return a sequence sort over base sort s.
A Context manages all other Z3 objects, global configuration options, etc.
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_bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, unsigned __int64 *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned __int6...
expr set_add(expr const &s, expr const &e)
expr ashr(expr const &a, expr const &b)
arithmetic shift right operator for bitvectors
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_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows dividend).
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c)
Return the parameter description set for the simplify procedure.
solver(context &c, Z3_solver s)
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
Z3 global configuration object.
Z3_decl_kind decl_kind() const
bool is_re() const
Return true if this sort is a regular expression sort.
solver & operator=(solver const &s)
expr operator &&(expr const &a, expr const &b)
expr substitute(expr_vector const &src, expr_vector const &dst)
Apply substitution. Replace src expressions by dst.
ast(context &c, Z3_ast n)
ast_vector_tpl & operator=(ast_vector_tpl const &s)
expr operator<=(expr const &a, expr const &b)
handle add(expr const &e, char const *weight)
Z3_goal_prec precision() const
expr bv_const(char const *name, unsigned sz)
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_param_descrs_inc_ref(Z3_context c, Z3_param_descrs p)
Increment the reference counter of the given parameter description set.
Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f)
Return the 'else' value of the given function interpretation.
Z3_sort_kind sort_kind() const
Return the internal sort kind.
expr string_val(char const *s)
tactic(context &c, char const *name)
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.
sort string_sort()
Return the sort for ASCII strings.
tactic with(tactic const &t, params const &p)
expr empty_set(sort const &s)
expr plus(expr const &re)
__int64 get_numeral_int64() const
Return __int64 value of numeral, throw if result cannot fit in __int64.
Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1)
Coerce an integer to a real.
Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)
Shift left.
bool is_arith() const
Return true if this sort is the Integer or Real sort.
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
bool is_relation() const
Return true if this sort is a Relation sort.
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...
void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p)
Increment the reference counter of the given probe.
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
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_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
bool is_real() const
Return true if this sort is the Real sort.
void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e)
Increment the reference counter of the given Z3_func_entry object.
void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a)
Decrement the reference counter of the given AST. The context c should have been created using Z3_mk_...
func_entry(context &c, Z3_func_entry e)
void Z3_API Z3_del_config(Z3_config c)
Delete the given configuration object.
Z3_bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned int...
expr body() const
Return the 'body' of this quantifier.
void add(expr const &e, char const *p)
func_decl to_func_decl(context &c, Z3_func_decl f)
goal operator[](int i) const
Z3_lbool Z3_API Z3_compute_interpolant(Z3_context c, Z3_ast pat, Z3_params p, Z3_ast_vector *interp, Z3_model *model)
param_descrs(param_descrs const &o)
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
bool is_app() const
Return true if this expression is an application.
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].
Z3_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const to[])
Substitute the free variables in a with the expressions in to. For every i smaller than num_exprs...
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)
Create an array type.
expr_vector objectives() const
Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Check for subsetness of sets.
std::string to_smt2(char const *status="unknown")
expr operator+(expr const &a, expr const &b)
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...
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
expr operator()(context &c, Z3_ast a)
Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than or equal to.
Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem)
Add an element to a set.
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.
bool is_arith() const
Return true if this is an integer or real expression.
bool is_well_sorted() const
Return true if this expression is well sorted (aka type correct).
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_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg)
Take the complement of a set.
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...
expr srem(expr const &a, expr const &b)
signed reminder operator for bitvectors
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.
expr set_intersect(expr const &a, expr const &b)
Z3_goal Z3_API Z3_mk_goal(Z3_context c, Z3_bool models, Z3_bool unsat_cores, Z3_bool proofs)
Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or trans...
bool inconsistent() const
exception(char const *msg)
void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g)
Decrement the reference counter of the given tactic.
Z3_lbool
Lifted Boolean type: false, undefined, true.
void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a)
Add a new formula a to the given goal.
Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g)
Convert a goal into a string.
expr at(expr const &index) const
expr real_val(int n, int d)
ast_vector_tpl< sort > sort_vector
bool is_bool() const
Return true if this is a Boolean expression.
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.
expr prefixof(expr const &a, expr const &b)
void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h)
Register a Z3 error handler.
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas on the solver.
Z3_ast Z3_API Z3_mk_sign_ext(Z3_context c, unsigned i, Z3_ast t1)
Sign-extend of the given bit-vector to the (signed) equivalent bit-vector of size m+i...
func_interp(func_interp const &s)
Z3_func_interp Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f)
Return the interpretation of the function f in the model m. Return NULL, if the model does not assign...
model & operator=(model const &s)
void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m)
Decrement the reference counter of the given model.
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.
void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g)
Decrement the reference counter of the given goal.
unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m)
Return the number of constants assigned by the given model.
expr interpolant(expr const &a)
Z3_ast Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a)
Return the interpretation (i.e., assignment) of constant a in the model m. Return NULL...
void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s)
Decrement the reference counter of the given statistics object.
expr ugt(expr const &a, expr const &b)
unsigned greater than operator for bitvectors.
goal & operator=(goal const &s)
expr option(expr const &re)
expr const_array(sort const &d, expr const &v)
expr set_member(expr const &s, expr const &e)
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.
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.
void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p)
Decrement the reference counter of the given parameter set.
bool is_numeral_i64(__int64 &i) const
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...
sort get_sort() const
Return the sort of this expression.
sort uninterpreted_sort(char const *name)
create an uninterpreted sort with the name given by the string or symbol.
Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e)
Return the value of this point.
void set_param(char const *param, char const *value)
check_result compute_interpolant(expr const &pat, params const &p, expr_vector &interp, model &m)
Interpolation support.
Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than.
bool is_array() const
Return true if this sort is a Array sort.
handle maximize(expr const &e)
unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m)
Return the number of function interpretations in the given model.
Z3_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_param_kind
The different kinds of parameters that can be associated with parameter sets. (see Z3_mk_params)...
Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a string of a numeric constant term.
expr int_const(char const *name)
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.
friend std::ostream & operator<<(std::ostream &out, exception const &e)
expr replace(expr const &src, expr const &dst) const
Z3_bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, Z3_bool model_completion, Z3_ast *v)
Evaluate the AST node t in the given model. Return Z3_TRUE if succeeded, and store the result in v...
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_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_symbol_kind
The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See #Z3...
Z3_bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a)
Test if there exists an interpretation (i.e., assignment) for a in the model m.
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.
goal(context &c, bool models=true, bool unsat_cores=false, bool proofs=false)
Z3_bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx)
Return Z3_TRUE if the given statistical data is a unsigned integer.
expr suffixof(expr const &a, expr const &b)
void from_file(char const *filename)
void Z3_API Z3_interrupt(Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers...
check_result consequences(expr_vector &assumptions, expr_vector &vars, expr_vector &conseq)
expr operator<(expr const &a, expr const &b)
unsigned num_exprs() const
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)
Create a new (incremental) solver.
handle add(expr const &e, unsigned weight)
bool is_numeral(std::string &s, unsigned precision) const
expr arg(unsigned i) const
Return the i-th argument of this application. This method assumes the expression is an application...
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_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
expr real_const(char const *name)
bool is_relation() const
Return true if this is a Relation expression.
bool is_const() const
Return true if this expression is a constant (i.e., an application with 0 arguments).
bool is_decided_sat() const
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.
model convert_model(model const &m, unsigned i=0) const
expr sext(expr const &a, unsigned i)
Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector.
Z3_sort Z3_API Z3_mk_real_sort(Z3_context c)
Create the real type.
Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision)
Return numeral as a string in decimal notation. The result has at most precision decimal places...
Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set)
Check for set membership.
bool is_numeral_i(int &i) const
expr empty(sort const &s)
Z3_config Z3_API Z3_mk_config(void)
Create a configuration object for the Z3 context object.
symbol & operator=(symbol const &s)
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...
sort real_sort()
Return the Real sort.
friend std::ostream & operator<<(std::ostream &out, ast_vector_tpl const &v)
Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target)
Copy a solver s from the context source to a the context target.
void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g)
Increment the reference counter of the given goal.
ast_vector_tpl(ast_vector_tpl const &s)
expr num_val(int n, sort const &s)
bool eq(ast const &a, ast const &b)
bool is_bv() const
Return true if this sort is a Bit-vector sort.
symbol int_symbol(int n)
Create a Z3 symbol based on the given integer.
Z3_bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int...
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
expr indexof(expr const &s, expr const &substr, expr const &offset)
expr set_complement(expr const &a)
param_descrs & operator=(param_descrs const &o)
expr operator>(expr const &a, expr const &b)
Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] - ... - args[num_args - 1].
expr simplify() const
Return a simplified version of this expression.
check_result to_check_result(Z3_lbool l)
expr star(expr const &re)
expr operator==(expr const &a, expr const &b)
symbol name() const
Return name of sort.
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
#define MK_EXPR1(_fn, _arg)
param_descrs(context &c, Z3_param_descrs d)
void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value)
Set a configuration parameter.
Z3_tactic Z3_API Z3_tactic_repeat(Z3_context c, Z3_tactic t, unsigned max)
Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of...
expr operator|(expr const &a, expr const &b)
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
unsigned num_args() const
tactic(context &c, Z3_tactic s)
void check_context(object const &a, object const &b)
expr arg(unsigned i) const
expr bool_const(char const *name)
expr urem(expr const &a, expr const &b)
unsigned reminder operator for bitvectors
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.
std::string reason_unknown() const
unsigned num_consts() const
params & operator=(params const &s)
bool is_numeral_u(unsigned &i) const
bool is_numeral_u64(__uint64 &i) const
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.
solver(context &c, solver const &src, translate)
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_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
func_decl(context &c, Z3_func_decl n)
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
ast_vector_tpl< ast > ast_vector
handle minimize(expr const &e)
apply_result apply(goal const &g) const
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
void add(expr const &e, expr const &p)
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.
expr store(expr const &a, expr const &i, expr const &v)
bool has_interp(func_decl f) const
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
apply_result operator()(goal const &g) const
Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned division.
tactic repeat(tactic const &t, unsigned max=UINT_MAX)
expr operator||(expr const &a, expr const &b)
expr ult(expr const &a, expr const &b)
unsigned less than operator for bitvectors.
bool is_var() const
Return true if this expression is a variable.
Z3_context Z3_API Z3_mk_interpolation_context(Z3_config cfg)
This function generates a Z3 context suitable for generation of interpolants. Formulas can be generat...
void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p)
Increment the reference counter of the given parameter set.
expr_vector get_interpolant(expr const &proof, expr const &pat, params const &p)
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...
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.
void Z3_API Z3_global_param_reset_all(void)
Restore the value of all global (and module) parameters. This command will not affect already created...
void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m)
Increment the reference counter of the given model.
func_decl(func_decl const &s)
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
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_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.
expr mk_or(expr_vector const &args)
tactic fail_if(probe const &p)
Z3_param_kind kind(symbol const &s)
stats(context &c, Z3_stats e)
expr exists(expr const &x, expr const &b)
ast operator()(context &c, Z3_ast a)
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
Z3_solver Z3_API Z3_mk_solver(Z3_context c)
Create a new (incremental) solver. This solver also uses a set of builtin tactics for handling the fi...
bool is_quantifier() const
Return true if this expression is a quantifier.
unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f)
Return the number of entries in the given function interpretation.
expr ite(expr const &c, expr const &t, expr const &e)
Create the if-then-else expression ite(c, t, e)
double apply(goal const &g) const
func_entry(func_entry const &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...
expr eval(expr const &n, bool model_completion=false) const
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.
#define Z3_FALSE
False value. It is just an alias for 0.
expr_vector unsat_core() const
int get_numeral_int() const
Return int value of numeral, throw if result cannot fit in machine int.
ast & operator=(ast const &s)
expr_vector assertions() const
unsigned num_args() const
Return the number of arguments in this application. This method assumes the expression is an applicat...
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.
unsigned bv_size() const
Return the size of this Bit-vector sort.
Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned remainder.
expr forall(expr const &x, expr const &b)
sort(context &c, Z3_sort s)
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
expr implies(expr const &a, expr const &b)
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...
Z3_func_entry Z3_API Z3_func_interp_get_entry(Z3_context c, Z3_func_interp f, unsigned i)
Return a "point" of the given function intepretation. It represents the value of f in a particular po...
Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c, Z3_string name, Z3_string logic, Z3_string status, Z3_string attributes, unsigned num_assumptions, Z3_ast const assumptions[], Z3_ast formula)
Convert the given benchmark into SMT-LIB formatted string.
expr to_expr(context &c, Z3_ast a)
Wraps a Z3_ast as an expr object. It also checks for errors. This function allows the user to use the...
expr concat(expr const &a, expr const &b)
symbol(context &c, Z3_symbol s)
solver(context &c, char const *logic)
tactic try_for(tactic const &t, unsigned ms)
func_interp(context &c, Z3_func_interp e)
expr shl(expr const &a, expr const &b)
shift left operator for bitvectors
void push_back(T const &e)
ast_vector_tpl< expr > expr_vector
void Z3_API Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, Z3_bool v)
Add a Boolean parameter k with value v to the parameter set p.
expr uge(expr const &a, expr const &b)
unsigned greater than or equal to operator for bitvectors.
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...
bool is_seq() const
Return true if this sort is a Sequence sort.
bool is_numeral(std::string &s) const
void Z3_API Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r)
Increment the reference counter of the given Z3_apply_result object.
bool is_double(unsigned i) const
sort & operator=(sort const &s)
Return true if this sort and s are equal.
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_bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g)
Return true if the given goal contains the formula false.
bool is_finite_domain() const
Return true if this is a Finite-domain expression.
expr operator-(expr const &a)
func_interp get_func_interp(func_decl f) const
expr to_real(expr const &a)
Z3_ast_vector Z3_API Z3_get_interpolant(Z3_context c, Z3_ast pf, Z3_ast pat, Z3_params p)
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
param_descrs get_param_descrs()
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a)
Increment the reference counter of the given AST. The context c should have been created using Z3_mk_...
Z3_bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, __int64 *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine __int64 int...
bool is_seq() const
Return true if this is a sequence expression.
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...
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.
bool is_finite_domain() const
Return true if this sort is a Finite domain sort.
void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s)
Increment the reference counter of the given statistics object.
Z3_decl_kind
The different kinds of interpreted function kinds.
Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i)
Array read. The argument a is the array and i is the index of the array that gets read...
apply_result(context &c, Z3_apply_result s)
expr operator/(expr const &a, expr const &b)
Function declaration (aka function definition). It is the signature of interpreted and uninterpreted ...
expr set_union(expr const &a, expr const &b)
param_descrs get_param_descrs()
sort int_sort()
Return the integer sort.
expr set_del(expr const &s, expr const &e)
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.
stats & operator=(stats const &s)
Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c, Z3_symbol name, unsigned n, Z3_symbol const enum_names[], Z3_func_decl enum_consts[], Z3_func_decl enum_testers[])
Create a enumeration sort.
func_decl & operator=(func_decl const &s)
apply_result & operator=(apply_result const &s)
sort to_sort(context &c, Z3_sort s)
void Z3_API Z3_param_descrs_dec_ref(Z3_context c, Z3_param_descrs p)
Decrement the reference counter of the given parameter description set.
bool is_int() const
Return true if this is an integer expression.
Z3_model Z3_API Z3_apply_result_convert_model(Z3_context c, Z3_apply_result r, unsigned i, Z3_model m)
Convert a model for the subgoal Z3_apply_result_get_subgoal(c, r, i) into a model for the original go...
expr to_re(expr const &s)
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...
unsigned num_funcs() const
Z3_ast Z3_API Z3_mk_zero_ext(Z3_context c, unsigned i, Z3_ast t1)
Extend the given bit-vector with zeros to the (unsigned) equivalent bit-vector of size m+i...
Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m)
Convert the given model into a string.
const char * Z3_string
Z3 string type. It is just an alias for const char *.
apply_result(apply_result const &s)