93 char const *
msg()
const {
return m_msg.c_str(); }
94 char const *
what()
const throw() {
return m_msg.c_str(); }
99 #if !defined(Z3_THROW)
100 #if __cpp_exceptions || _CPPUNWIND || __EXCEPTIONS
101 #define Z3_THROW(x) throw x
103 #define Z3_THROW(x) {}
105 #endif // !defined(Z3_THROW)
117 operator Z3_config()
const {
return m_cfg; }
129 void set(
char const * param,
int value) {
130 auto str = std::to_string(value);
163 bool m_enable_exceptions =
true;
165 Z3_context m_ctx =
nullptr;
169 void set_context(Z3_context ctx) {
171 m_enable_exceptions =
true;
172 m_rounding_mode =
RNE;
181 context(Z3_context c) { set_context(c); }
182 void detach() { m_ctx =
nullptr; }
187 operator Z3_context()
const {
return m_ctx; }
225 void set(
char const * param,
int value) {
226 auto str = std::to_string(value);
294 template<
size_t precision>
309 sort enumeration_sort(
char const * name,
unsigned n,
char const *
const * enum_names, func_decl_vector & cs, func_decl_vector & ts);
317 func_decl tuple_sort(
char const * name,
unsigned n,
char const *
const * names,
sort const* sorts, func_decl_vector & projs);
392 expr fpa_const(
char const * name,
unsigned ebits,
unsigned sbits);
394 template<
size_t precision>
445 expr_vector
parse_string(
char const* s, sort_vector
const& sorts, func_decl_vector
const& decls);
446 expr_vector
parse_file(
char const* s, sort_vector
const& sorts, func_decl_vector
const& decls);
452 std::unique_ptr<T[]> m_array;
457 array(
unsigned sz):m_array(new T[sz]),m_size(sz) {}
458 template<
typename T2>
460 void resize(
unsigned sz) { m_array.reset(
new T[sz]); m_size = sz; }
461 unsigned size()
const {
return m_size; }
462 T &
operator[](
int i) { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size);
return m_array[i]; }
463 T
const &
operator[](
int i)
const { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size);
return m_array[i]; }
464 T
const *
ptr()
const {
return m_array.get(); }
465 T *
ptr() {
return m_array.get(); }
475 friend void check_context(
object const & a,
object const & b);
483 operator Z3_symbol()
const {
return m_sym; }
492 out <<
"k!" << s.
to_int();
500 Z3_param_descrs m_descrs;
507 m_descrs = o.m_descrs;
508 object::operator=(o);
530 operator Z3_params()
const {
return m_params; }
534 object::operator=(s);
535 m_params = s.m_params;
558 operator Z3_ast()
const {
return m_ast; }
559 operator bool()
const {
return m_ast != 0; }
564 object::operator=(s);
570 friend std::ostream &
operator<<(std::ostream & out,
ast const & n);
577 friend bool eq(
ast const & a,
ast const & b);
586 class ast_vector_tpl :
public object {
587 Z3_ast_vector m_vector;
596 operator Z3_ast_vector()
const {
return m_vector; }
607 object::operator=(s);
608 m_vector = s.m_vector;
630 return other.m_index == m_index;
633 return other.m_index != m_index;
646 iterator
begin() const noexcept {
return iterator(
this, 0); }
647 iterator
end()
const {
return iterator(
this,
size()); }
661 operator Z3_sort()
const {
return reinterpret_cast<Z3_sort
>(
m_ast); }
763 operator Z3_func_decl()
const {
return reinterpret_cast<Z3_func_decl
>(
m_ast); }
803 expr
select(expr
const & a, expr
const& i);
804 expr
select(expr
const & a, expr_vector
const & i);
1071 assert(
ctx().enable_exceptions());
1072 if (!
ctx().enable_exceptions())
return 0;
1089 unsigned result = 0;
1091 assert(
ctx().enable_exceptions());
1092 if (!
ctx().enable_exceptions())
return 0;
1108 assert(
ctx().enable_exceptions());
1109 if (!
ctx().enable_exceptions())
return 0;
1123 uint64_t result = 0;
1125 assert(
ctx().enable_exceptions());
1126 if (!
ctx().enable_exceptions())
return 0;
1167 return std::string(s);
1184 operator Z3_app()
const { assert(
is_app());
return reinterpret_cast<Z3_app
>(
m_ast); }
1215 expr_vector vec(
ctx());
1217 for (
unsigned i = 0; i < argCnt; i++)
1369 friend expr pble(expr_vector
const& es,
int const * coeffs,
int bound);
1370 friend expr pbge(expr_vector
const& es,
int const * coeffs,
int bound);
1371 friend expr pbeq(expr_vector
const& es,
int const * coeffs,
int bound);
1372 friend expr atmost(expr_vector
const& es,
unsigned bound);
1373 friend expr atleast(expr_vector
const& es,
unsigned bound);
1566 return select(*
this, index);
1572 return select(*
this, index);
1597 expr substitute(func_decl_vector
const& funs, expr_vector
const& bodies);
1606 return i == other.i;
1609 return i != other.i;
1621 #define _Z3_MK_BIN_(a, b, binop) \
1622 check_context(a, b); \
1623 Z3_ast r = binop(a.ctx(), a, b); \
1625 return expr(a.ctx(), r); \
1668 #define _Z3_MK_UN_(a, mkun) \
1669 Z3_ast r = mkun(a.ctx(), a); \
1671 return expr(a.ctx(), r); \
1683 Z3_ast args[2] = { a, b };
1695 Z3_ast args[2] = { a, b };
1718 Z3_ast args[2] = { a, b };
1732 Z3_ast args[2] = { a, b };
1742 Z3_ast _args[2] = { a, b };
1762 Z3_ast args[2] = { a, b };
1829 else if (a.
is_bv()) {
1847 Z3_ast args[2] = { a, b };
1956 else if (a.
is_bv()) {
1972 else if (a.
is_bv()) {
1998 expr ge = a >= zero;
2004 expr ge = a >= zero;
2035 return expr(a.ctx(), r);
2302 return sort(c, reinterpret_cast<Z3_sort>(a));
2310 return func_decl(c, reinterpret_cast<Z3_func_decl>(a));
2314 template<
typename T>
2315 template<
typename T2>
2317 for (
unsigned i = 0; i < m_size; i++) {
2326 Z3_app vars[] = {(Z3_app) x};
2331 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2336 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2341 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2350 Z3_app vars[] = {(Z3_app) x};
2355 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2360 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2365 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2374 Z3_app vars[] = {(Z3_app) x};
2379 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2384 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2389 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2397 inline expr pble(expr_vector
const& es,
int const* coeffs,
int bound) {
2398 assert(es.
size() > 0);
2403 return expr(ctx, r);
2405 inline expr pbge(expr_vector
const& es,
int const* coeffs,
int bound) {
2406 assert(es.
size() > 0);
2411 return expr(ctx, r);
2413 inline expr pbeq(expr_vector
const& es,
int const* coeffs,
int bound) {
2414 assert(es.
size() > 0);
2419 return expr(ctx, r);
2422 assert(es.
size() > 0);
2427 return expr(ctx, r);
2430 assert(es.
size() > 0);
2435 return expr(ctx, r);
2438 assert(args.
size() > 0);
2443 return expr(ctx, r);
2447 assert(args.
size() > 0);
2452 return expr(ctx, r);
2459 Z3_ast _args[2] = { a, b };
2463 Z3_ast _args[2] = { a, b };
2475 assert(args.
size() > 0);
2476 if (args.
size() == 1) {
2488 r = _args[args.
size()-1];
2489 for (
unsigned i = args.
size()-1; i > 0; ) {
2496 return expr(ctx, r);
2515 for (
unsigned i = 1; i < args.
size(); ++i)
2522 Z3_func_entry m_entry;
2523 void init(Z3_func_entry e) {
2531 operator Z3_func_entry()
const {
return m_entry; }
2535 object::operator=(s);
2536 m_entry = s.m_entry;
2545 Z3_func_interp m_interp;
2546 void init(Z3_func_interp e) {
2554 operator Z3_func_interp()
const {
return m_interp; }
2558 object::operator=(s);
2559 m_interp = s.m_interp;
2577 void init(Z3_model m) {
2588 operator Z3_model()
const {
return m_model; }
2592 object::operator=(s);
2593 m_model = s.m_model;
2602 if (status ==
false &&
ctx().enable_exceptions())
2651 friend std::ostream &
operator<<(std::ostream & out,
model const & m);
2659 void init(Z3_stats e) {
2668 operator Z3_stats()
const {
return m_stats; }
2672 object::operator=(s);
2673 m_stats = s.m_stats;
2682 friend std::ostream &
operator<<(std::ostream & out,
stats const & s);
2688 if (r ==
unsat) out <<
"unsat";
2689 else if (r ==
sat) out <<
"sat";
2690 else out <<
"unknown";
2708 context& ctx()
const {
return m_decl.
ctx(); }
2734 void init(Z3_solver s) {
2750 operator Z3_solver()
const {
return m_solver; }
2754 object::operator=(s);
2755 m_solver = s.m_solver;
2784 add(e,
ctx().bool_const(p));
2786 void add(expr_vector
const& v) {
2788 for (
unsigned i = 0; i < v.
size(); ++i)
2797 for (
unsigned i = 0; i < n; i++) {
2799 _assumptions[i] = assumptions[i];
2806 unsigned n = assumptions.
size();
2808 for (
unsigned i = 0; i < n; i++) {
2810 _assumptions[i] = assumptions[i];
2832 expr_vector result(
ctx(), r);
2833 unsigned sz = result.
size();
2842 std::string
to_smt2(
char const* status =
"unknown") {
2844 Z3_ast
const* fmls = es.
ptr();
2846 unsigned sz = es.
size();
2867 expr_vector
cube(expr_vector& vars,
unsigned cutoff) {
2876 expr_vector& m_vars;
2882 assert(!m_end && !m_empty);
2883 m_cube = m_solver.
cube(m_vars, m_cutoff);
2884 m_cutoff = 0xFFFFFFFF;
2885 if (m_cube.
size() == 1 && m_cube[0u].is_false()) {
2889 else if (m_cube.
empty()) {
2918 expr_vector
const&
operator*() const noexcept {
return m_cube; }
2921 return other.m_end == m_end;
2924 return other.m_end != m_end;
2932 expr_vector m_default_vars;
2933 expr_vector& m_vars;
2937 m_cutoff(0xFFFFFFFF),
2938 m_default_vars(s.
ctx()),
2939 m_vars(m_default_vars)
2944 m_cutoff(0xFFFFFFFF),
2945 m_default_vars(s.
ctx()),
2962 void init(Z3_goal s) {
2971 operator Z3_goal()
const {
return m_goal; }
2975 object::operator=(s);
3002 unsigned n =
size();
3009 for (
unsigned i = 0; i < n; i++)
3010 args[i] =
operator[](i);
3015 friend std::ostream &
operator<<(std::ostream & out,
goal const & g);
3020 Z3_apply_result m_apply_result;
3021 void init(Z3_apply_result s) {
3029 operator Z3_apply_result()
const {
return m_apply_result; }
3033 object::operator=(s);
3034 m_apply_result = s.m_apply_result;
3045 void init(Z3_tactic s) {
3054 operator Z3_tactic()
const {
return m_tactic; }
3058 object::operator=(s);
3059 m_tactic = s.m_tactic;
3115 Z3_THROW(
exception(
"a non-zero number of tactics need to be passed to par_or"));
3118 for (
unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
3130 Z3_simplifier m_simplifier;
3131 void init(Z3_simplifier s) {
3140 operator Z3_simplifier()
const {
return m_simplifier; }
3144 object::operator=(s);
3145 m_simplifier = s.m_simplifier;
3172 void init(Z3_probe s) {
3182 operator Z3_probe()
const {
return m_probe; }
3186 object::operator=(s);
3187 m_probe = s.m_probe;
3255 unsigned h()
const {
return m_h; }
3266 for (expr_vector::iterator it = v.begin(); it != v.end(); ++it)
minimize(*it);
3272 object::operator=(o);
3276 operator Z3_optimize()
const {
return m_opt; }
3281 void add(expr_vector
const& es) {
3282 for (expr_vector::iterator it = es.
begin(); it != es.
end(); ++it)
add(*it);
3290 add(e,
ctx().bool_const(p));
3294 auto str = std::to_string(weight);
3318 unsigned n = asms.
size();
3320 for (
unsigned i = 0; i < n; i++) {
3361 object::operator=(o);
3364 operator Z3_fixedpoint()
const {
return m_fp; }
3424 return tactic(t1.ctx(), r);
3461 for (
unsigned i = 0; i < n; i++) { _enum_names[i] =
Z3_mk_string_symbol(*
this, enum_names[i]); }
3473 for (
unsigned i = 0; i < n; i++) { _names[i] =
Z3_mk_string_symbol(*
this, names[i]); _sorts[i] = sorts[i]; }
3485 Z3_constructor_list clist;
3489 operator Z3_constructor_list()
const {
return clist; }
3495 std::vector<Z3_constructor> cons;
3496 std::vector<unsigned> num_fields;
3501 for (
auto con : cons)
3509 for (
unsigned i = 0; i < n; ++i) sorts[i] = fields[i], _names[i] = names[i];
3511 num_fields.push_back(n);
3516 unsigned size()
const {
return (
unsigned)cons.size(); }
3519 Z3_func_decl _constructor;
3529 constructor =
func_decl(ctx, _constructor);
3532 for (
unsigned j = 0; j < num_fields[i]; ++j)
3539 for (
unsigned i = 0; i < cs.
size(); ++i)
3546 for (
unsigned i = 0; i < cs.
size(); ++i) _cs[i] = cs[i];
3549 return sort(*
this, s);
3553 unsigned n,
symbol const* names,
3555 sort_vector result(*
this);
3559 for (
unsigned i = 0; i < n; ++i)
3560 _names[i] = names[i], _cons[i] = *cons[i];
3562 for (
unsigned i = 0; i < n; ++i)
3571 return sort(*
this, s);
3585 for (
unsigned i = 0; i < arity; i++) {
3587 args[i] = domain[i];
3600 for (
unsigned i = 0; i < domain.
size(); i++) {
3602 args[i] = domain[i];
3616 Z3_sort args[1] = { domain };
3624 Z3_sort args[2] = { d1, d2 };
3632 Z3_sort args[3] = { d1, d2, d3 };
3640 Z3_sort args[4] = { d1, d2, d3, d4 };
3648 Z3_sort args[5] = { d1, d2, d3, d4, d5 };
3656 for (
unsigned i = 0; i < arity; i++) {
3658 args[i] = domain[i];
3688 sort dom[2] = { d1, d2 };
3709 return expr(*
this, r);
3715 return expr(*
this, r);
3724 template<
size_t precision>
3730 switch (m_rounding_mode) {
3736 default:
return expr(*
this);
3762 for (
unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
3780 for (
unsigned i = 0; i < n; i++) {
3791 for (
unsigned i = 0; i < args.
size(); i++) {
3806 Z3_ast args[1] = { a };
3819 Z3_ast args[2] = { a1, a2 };
3840 Z3_ast args[3] = { a1, a2, a3 };
3847 Z3_ast args[4] = { a1, a2, a3, a4 };
3854 Z3_ast args[5] = { a1, a2, a3, a4, a5 };
3863 return range.
ctx().
function(name, arity, domain, range);
3866 return range.
ctx().
function(name, arity, domain, range);
3875 return range.
ctx().
function(name, d1, d2, d3, range);
3878 return range.
ctx().
function(name, d1, d2, d3, d4, range);
3881 return range.
ctx().
function(name, d1, d2, d3, d4, d5, range);
3891 return range.
ctx().
recfun(name, arity, domain, range);
3894 return range.
ctx().
recfun(name, arity, domain, range);
3897 return range.
ctx().
recfun(name, d1, range);
3900 return range.
ctx().
recfun(name, d1, d2, range);
3946 #define MK_EXPR1(_fn, _arg) \
3947 Z3_ast r = _fn(_arg.ctx(), _arg); \
3948 _arg.check_error(); \
3949 return expr(_arg.ctx(), r);
3951 #define MK_EXPR2(_fn, _arg1, _arg2) \
3952 check_context(_arg1, _arg2); \
3953 Z3_ast r = _fn(_arg1.ctx(), _arg1, _arg2); \
3954 _arg1.check_error(); \
3955 return expr(_arg1.ctx(), r);
3979 Z3_ast es[2] = { a, b };
3987 Z3_ast es[2] = { a, b };
4068 assert(args.
size() > 0);
4073 return expr(ctx, r);
4080 return expr(ctx, r);
4113 for (
unsigned i = 0; i < sorts.
size(); ++i) {
4114 sort_names[i] = sorts[i].name();
4116 for (
unsigned i = 0; i < decls.
size(); ++i) {
4117 decl_names[i] = decls[i].name();
4125 inline expr_vector
context::parse_file(
char const* s, sort_vector
const& sorts, func_decl_vector
const& decls) {
4130 for (
unsigned i = 0; i < sorts.
size(); ++i) {
4131 sort_names[i] = sorts[i].name();
4133 for (
unsigned i = 0; i < decls.
size(); ++i) {
4134 decl_names[i] = decls[i].name();
4143 func_decl_vector cs(
ctx());
4145 for (
unsigned i = 0; i < n; ++i)
4152 func_decl_vector rs(
ctx());
4154 for (
unsigned i = 0; i < n; ++i)
4164 for (; idx < n; ++idx) {
4171 func_decl_vector as(
ctx());
4172 for (
unsigned i = 0; i < n; ++i)
4182 for (
unsigned i = 0; i < src.
size(); ++i) {
4193 for (
unsigned i = 0; i < dst.
size(); ++i) {
4208 for (
unsigned i = 0; i < dst.
size(); ++i) {
4217 typedef std::function<void(expr const& proof, std::vector<unsigned>
const& deps, expr_vector
const& clause)>
on_clause_eh_t;
4223 static void _on_clause_eh(
void* _ctx, Z3_ast _proof,
unsigned n,
unsigned const* dep, Z3_ast_vector _literals) {
4225 expr_vector lits(ctx->c, _literals);
4226 expr proof(ctx->c, _proof);
4227 std::vector<unsigned> deps;
4228 for (
unsigned i = 0; i < n; ++i)
4229 deps.push_back(dep[i]);
4230 ctx->m_on_clause(proof, deps, lits);
4242 typedef std::function<void(expr const&, expr const&)> fixed_eh_t;
4243 typedef std::function<void(void)> final_eh_t;
4244 typedef std::function<void(expr const&, expr const&)> eq_eh_t;
4245 typedef std::function<void(expr const&)> created_eh_t;
4246 typedef std::function<void(expr, unsigned, bool)> decide_eh_t;
4248 final_eh_t m_final_eh;
4250 fixed_eh_t m_fixed_eh;
4251 created_eh_t m_created_eh;
4252 decide_eh_t m_decide_eh;
4255 std::vector<z3::context*> subcontexts;
4257 Z3_solver_callback cb {
nullptr };
4261 scoped_cb(
void* _p, Z3_solver_callback cb):p(*static_cast<user_propagator_base*>(_p)) {
4269 static void push_eh(
void* _p, Z3_solver_callback cb) {
4271 scoped_cb _cb(p, cb);
4275 static void pop_eh(
void* _p, Z3_solver_callback cb,
unsigned num_scopes) {
4277 scoped_cb _cb(p, cb);
4281 static void* fresh_eh(
void* _p, Z3_context
ctx) {
4284 p->subcontexts.push_back(c);
4285 return p->
fresh(*c);
4288 static void fixed_eh(
void* _p, Z3_solver_callback cb, Z3_ast _var, Z3_ast _value) {
4290 scoped_cb _cb(p, cb);
4293 p->m_fixed_eh(var, value);
4296 static void eq_eh(
void* _p, Z3_solver_callback cb, Z3_ast _x, Z3_ast _y) {
4298 scoped_cb _cb(p, cb);
4303 static void final_eh(
void* p, Z3_solver_callback cb) {
4304 scoped_cb _cb(p, cb);
4308 static void created_eh(
void* _p, Z3_solver_callback cb, Z3_ast _e) {
4310 scoped_cb _cb(p, cb);
4315 static void decide_eh(
void* _p, Z3_solver_callback cb, Z3_ast _val,
unsigned bit,
bool is_pos) {
4317 scoped_cb _cb(p, cb);
4319 p->m_decide_eh(val, bit, is_pos);
4329 virtual void push() = 0;
4330 virtual void pop(
unsigned num_scopes) = 0;
4333 for (
auto& subcontext : subcontexts) {
4334 subcontext->detach();
4340 return c ? *c : s->
ctx();
4367 m_fixed_eh = [
this](
expr const &id,
expr const &e) {
4383 m_eq_eh = [
this](
expr const& x,
expr const& y) {
4407 m_final_eh = [
this]() {
4423 m_created_eh = [
this](
expr const& e) {
4439 m_decide_eh = [
this](
expr val,
unsigned bit,
bool is_pos) {
4440 decide(val, bit, is_pos);
4451 virtual void final() { }
4492 void conflict(expr_vector
const&
fixed, expr_vector
const& lhs, expr_vector
const& rhs) {
4504 assert((Z3_context)conseq.
ctx() == (Z3_context)
ctx());
4510 expr_vector
const& lhs, expr_vector
const& rhs,
4511 expr const& conseq) {
4513 assert((Z3_context)conseq.
ctx() == (Z3_context)
ctx());
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.
cube_generator cubes(expr_vector &vars)
ast_vector_tpl(context &c)
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
expr distinct(expr_vector const &args)
expr mod(expr const &a, expr const &b)
friend expr mk_or(expr_vector const &args)
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.
expr bvadd_no_overflow(expr const &a, expr const &b, bool is_signed)
bit-vector overflow/underflow checks
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_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...
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...
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.
void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s)
Increment the reference counter of the given statistics object.
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 ...
Z3_ast Z3_API Z3_mk_true(Z3_context c)
Create an AST node representing true.
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)
Create a new fixedpoint context.
user_propagator_base(solver *s)
Z3_probe Z3_API Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the va...
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
bool is_numeral_u(unsigned &i) const
Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)
Create a bit-vector type of the given size.
friend expr operator|(expr const &a, expr const &b)
Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nor.
void register_final(final_eh_t &f)
register a callback on final-check. During the final check stage, all propagations have been processe...
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.
std::string reason_unknown() const
sort bool_sort()
Return the Boolean sort.
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.
friend expr atmost(expr_vector const &es, unsigned bound)
void check_parser_error() const
handle add_soft(expr const &e, char const *weight)
friend expr operator+(expr const &a, expr const &b)
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.
expr variable(unsigned index, sort const &s)
create a de-Bruijn variable.
void add_const_interp(func_decl &f, expr &value)
expr mk_and(expr_vector const &args)
Z3_string Z3_API Z3_get_decl_rational_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the rational value, as a string, associated with a rational parameter.
friend expr pw(expr const &a, expr const &b)
bool is_numeral_i64(int64_t &i) const
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: ...
unsigned Z3_API Z3_get_string_length(Z3_context c, Z3_ast s)
Retrieve the length of the unescaped string constant stored in s.
bool as_binary(std::string &s) const
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_ast Z3_API Z3_mk_fpa_rtz(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
void set(char const *k, bool v)
Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1)
Take conjunction of bits in vector, return vector of length 1.
friend expr bv2int(expr const &a, bool is_signed)
bit-vector and integer conversions.
bool is_int() const
Return true if this sort is the Integer sort.
Z3_ast Z3_API Z3_mk_false(Z3_context c)
Create an AST node representing false.
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas on the solver.
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
Z3_probe Z3_API Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than or equal to the...
tactic & operator=(tactic const &s)
expr operator[](expr const &index) const
sort re_sort(sort &seq_sort)
Return a regular expression sort over sequences seq_sort.
void Z3_API Z3_del_constructor(Z3_context c, Z3_constructor constr)
Reclaim memory allocated to constructor.
expr sle(expr const &a, expr const &b)
signed less than or equal to operator for bitvectors.
expr bvredand(expr const &a)
void add_fact(func_decl &f, unsigned *args)
Z3_param_descrs Z3_API Z3_tactic_get_param_descrs(Z3_context c, Z3_tactic t)
Return the parameter description set for the given tactic object.
probe(context &c, Z3_probe s)
void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g)
Erase all formulas from the given goal.
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.
expr pbeq(expr_vector const &es, int const *coeffs, int bound)
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.
friend expr xnor(expr const &a, expr const &b)
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.
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor_accessor(Z3_context c, Z3_sort t, unsigned idx_c, unsigned idx_a)
Return idx_a'th accessor for the idx_c'th constructor.
probe & operator=(probe const &s)
Z3_tactic Z3_API Z3_tactic_when(Z3_context c, Z3_probe p, Z3_tactic t)
Return a tactic that applies t to a given goal is the probe p evaluates to true. If p evaluates to fa...
func_decl get_const_decl(unsigned i) const
Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty)
Create a variable.
void register_fixed(fixed_eh_t &f)
register callbacks. Callbacks can only be registered with user_propagators that were created using a ...
Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err)
Return a string describing the given error code.
unsigned get_num_levels(func_decl &p)
std::string documentation(symbol const &s)
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.
Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c, Z3_func_decl f)
create transitive closure of binary relation.
void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t)
Increment the reference counter of the given tactic.
virtual void eq(expr const &, expr const &)
friend expr operator>=(expr const &a, expr const &b)
void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh)
register a callback when a new expression with a registered function is used by the solver The regist...
iterator & operator++() noexcept
bool is_array() const
Return true if this is a Array expression.
unsigned id() const
retrieve unique identifier for expression.
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d)
Return the constant declaration name as a symbol.
Z3_string Z3_API Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s)
Retrieve documentation string corresponding to parameter name s.
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits)
Create a FloatingPoint sort.
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...
void Z3_API Z3_simplifier_dec_ref(Z3_context c, Z3_simplifier g)
Decrement the reference counter of the given simplifier.
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.
Z3_ast Z3_API Z3_mk_char_is_digit(Z3_context c, Z3_ast ch)
Create a check if the character is a digit.
void set(char const *k, symbol const &s)
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...
friend std::ostream & operator<<(std::ostream &out, sort const &s)
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...
Z3_tactic Z3_API Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1...
friend bool eq(ast const &a, ast const &b)
Return true if the ASTs are structurally identical.
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...
func_decl piecewise_linear_order(sort const &a, unsigned index)
void Z3_API Z3_ast_vector_inc_ref(Z3_context c, Z3_ast_vector v)
Increment the reference counter of the given AST vector.
void push()
Create a backtracking point.
friend expr bvmul_no_overflow(expr const &a, expr const &b, bool is_signed)
expr bvsub_no_underflow(expr const &a, expr const &b, bool is_signed)
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_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_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
friend expr bvadd_no_underflow(expr const &a, expr const &b)
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.
friend expr fp_eq(expr const &a, expr const &b)
void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a)
Add a constant interpretation.
expr range(expr const &lo, expr const &hi)
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_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_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
friend expr bvsub_no_underflow(expr const &a, expr const &b, bool is_signed)
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, again represented as a floating-point number.
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...
bool is_real() const
Return true if this is a real expression.
func_interp & operator=(func_interp const &s)
friend expr operator!=(expr const &a, expr const &b)
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...
func_decl_vector recognizers()
friend expr bvredor(expr const &a)
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_xor(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 xor t2.
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...
probe(context &c, double val)
bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a)
Return true if the given AST is a real algebraic number.
uint64_t as_uint64() const
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.
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 set(char const *param, char const *value)
Set global parameter param with string value.
expr_vector units() const
Z3_simplifier Z3_API Z3_simplifier_and_then(Z3_context c, Z3_simplifier t1, Z3_simplifier t2)
Return a simplifier that applies t1 to a given goal and t2 to every subgoal produced by t1...
constructor_list(constructors const &cs)
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 set(char const *k, char const *v)
simplifier(simplifier const &s)
expr fma(expr const &a, expr const &b, expr const &c, expr const &rm)
tactic when(probe const &p, tactic const &t)
Z3_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.
void set_else(expr &value)
friend expr round_fpa_to_closest_integer(expr const &t)
Round a floating-point term into its closest integer.
friend std::ostream & operator<<(std::ostream &out, params const &p)
void set(char const *k, double n)
void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s)
Decrement the reference counter of the given statistics object.
Z3_sort Z3_API Z3_get_array_sort_range(Z3_context c, Z3_sort t)
Return the range of the given array sort.
expr lower(handle const &h)
bool is_numeral_u64(uint64_t &i) const
friend expr operator/(expr const &a, expr const &b)
Z3_probe Z3_API Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned ...
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
void set(char const *param, char const *value)
Update global parameter param with string value.
handle add_soft(expr const &e, unsigned weight)
expr mk_is_inf() const
Return Boolean expression to test for whether an FP expression is inf.
std::ostream & operator<<(std::ostream &out, exception const &e)
void Z3_API Z3_get_string_contents(Z3_context c, Z3_ast s, unsigned length, unsigned contents[])
Retrieve the unescaped string constant stored in 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 ...
A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort.
optimize(context &c, optimize &src)
Z3_param_descrs Z3_API Z3_simplifier_get_param_descrs(Z3_context c, Z3_simplifier t)
Return the parameter description set for the given simplifier object.
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].
expr simplify() const
Return a simplified version of this expression.
unsigned bv_size() const
Return the size of this Bit-vector sort.
bool is_bv() const
Return true if this sort is a Bit-vector sort.
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_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than.
Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)
Create a new optimize context.
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.
friend expr operator^(expr const &a, expr const &b)
expr full_set(sort const &s)
def on_clause_eh(ctx, p, n, dep, clause)
model(model &src, context &dst, translate)
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.
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 Z3_API Z3_mk_datatype(Z3_context c, Z3_symbol name, unsigned num_constructors, Z3_constructor constructors[])
Create datatype, such as lists, trees, records, enumerations or unions of records. The datatype may be recursive. Return the datatype sort.
friend expr fpa_to_ubv(expr const &t, unsigned sz)
Conversion of a floating-point term into an unsigned bit-vector.
Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s)
Convert string to integer.
friend std::ostream & operator<<(std::ostream &out, ast const &n)
Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem)
Remove an element to a set.
Z3_ast Z3_API Z3_mk_int64(Z3_context c, int64_t v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
Z3_ast Z3_API Z3_mk_set_union(Z3_context c, unsigned num_args, Z3_ast const args[])
Take the union of a list of sets.
Z3_func_decl Z3_API Z3_model_get_const_decl(Z3_context c, Z3_model m, unsigned i)
Return the i-th constant in the given model.
sort bv_sort(unsigned sz)
Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz.
void interrupt()
Interrupt the current procedure being executed by any object managed by this context. This is a soft interruption: there is no guarantee the object will actually stop.
bool is_double(unsigned i) const
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.
void add(expr const &e)
tracks e by a unique identifier that is returned by the call.
apply_result operator()(goal const &g) const
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
friend expr concat(expr const &a, expr const &b)
friend expr mod(expr const &a, expr const &b)
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_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...
expr upper(handle const &h)
Z3_goal_prec
Z3 custom error handler (See Z3_set_error_handler).
Z3_error_code
Z3 error codes (See Z3_get_error_code).
goal(context &c, Z3_goal s)
optimize(optimize const &o)
optimize & operator=(optimize const &o)
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 eval(expr const &n, bool model_completion=false) const
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)
create an uninterpreted constant.
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.
friend simplifier operator&(simplifier const &t1, simplifier const &t2)
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)
Return the number of parameters associated with a declaration.
func_decl operator[](int i) const
bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
Compare terms.
check_result query(expr &q)
unsigned fpa_sbits() const
Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than or equal to.
sort char_sort()
Return the sort for Unicode characters.
constructors(context &ctx)
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_string Z3_API Z3_ast_vector_to_string(Z3_context c, Z3_ast_vector v)
Convert AST vector into a string.
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...
double get_double() const
friend expr operator||(expr const &a, expr const &b)
Return an expression representing a or b.
void set_enable_exceptions(bool f)
The C++ API uses by defaults exceptions on errors. For applications that don't work well with excepti...
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...
bool is_datatype() const
Return true if this is a Datatype expression.
void add(expr const &e, expr const &t)
Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d)
Return declaration kind corresponding to declaration.
bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a)
Determine if ast is an existential quantifier.
sort operator()(context &c, Z3_ast a)
expr ubv_to_fpa(expr const &t, sort s)
simplifier(context &c, Z3_simplifier s)
Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[])
Create the intersection of the regular languages.
expr rotate_left(unsigned i) const
friend probe operator||(probe const &p1, probe const &p2)
expr is_int(expr const &e)
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.
expr fpa_to_fpa(expr const &t, sort s)
expr contains(expr const &s) const
friend expr bvadd_no_overflow(expr const &a, expr const &b, bool is_signed)
bit-vector overflow/underflow checks
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.
iterator operator++(int) noexcept
Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[])
Check whether the assertions in the given solver and optional assumptions are consistent or not...
expr operator^(expr const &a, expr const &b)
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.
friend std::ostream & operator<<(std::ostream &out, optimize const &s)
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)
Create the constant array.
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)
void add(expr const &e, char const *p)
Exception used to sign API usage errors.
expr operator*(expr const &a, expr const &b)
Z3_stats Z3_API Z3_fixedpoint_get_statistics(Z3_context c, Z3_fixedpoint d)
Retrieve statistics information from the last call to Z3_fixedpoint_query.
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
unsigned uint_value(unsigned i) const
unsigned Z3_API Z3_get_sort_id(Z3_context c, Z3_sort s)
Return a unique identifier for s.
Z3_context Z3_API Z3_mk_context_rc(Z3_config c)
Create a context using the given configuration. This function is similar to Z3_mk_context. However, in the context returned by this function, the user is responsible for managing Z3_ast reference counters. Managing reference counters is a burden and error-prone, but allows the user to use the memory more efficiently. The user must invoke Z3_inc_ref for any Z3_ast returned by Z3, and Z3_dec_ref whenever the Z3_ast is not needed anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD.
Z3_string Z3_API Z3_simplifier_get_help(Z3_context c, Z3_simplifier t)
Return a string containing a description of parameters accepted by the given simplifier.
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.
expr nth(expr const &index) const
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...
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.
Z3_string Z3_API Z3_sort_to_string(Z3_context c, Z3_sort s)
expr operator!(expr const &a)
ast_vector_tpl & set(unsigned idx, ast &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.
void add(expr_vector const &es)
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.
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
unsigned num_exprs() const
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_fpa_is_subnormal(Z3_context c, Z3_ast t)
Predicate indicating whether t is a subnormal floating-point number.
bool is_uint(unsigned i) const
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)
expr re_diff(expr const &a, expr const &b)
void Z3_API Z3_ast_vector_resize(Z3_context c, Z3_ast_vector v, unsigned n)
Resize the AST vector v.
expr_vector unsat_core() const
bool is_lambda() const
Return true if this expression is a lambda expression.
Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s)
Return the length of the sequence s.
bool is_fpa() const
Return true if this is a FloatingPoint expression. .
Z3_parameter_kind Z3_API Z3_get_decl_parameter_kind(Z3_context c, Z3_func_decl d, unsigned idx)
Return the parameter type associated with a declaration.
sort datatype_sort(symbol const &name)
a reference to a recursively defined datatype. Expect that it gets defined as a datatype.
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_error_code check_error() const
Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s)
Return the set of units modulo model conversion.
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.
void set(char const *param, int value)
Update global parameter param with Integer value.
static param_descrs simplify_param_descrs(context &c)
friend expr mk_and(expr_vector const &args)
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.
unsigned num_entries() const
Z3_ast Z3_API Z3_mk_fpa_rne(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode...
Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th recognizer.
Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re)
Create the complement of the regular language re.
sort_vector datatypes(unsigned n, symbol const *names, constructor_list *const *cons)
Create a set of mutually recursive datatypes. n - number of recursive datatypes names - array of name...
void update_rule(expr &rule, symbol const &name)
bool enable_exceptions() const
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...
bool is_finite_domain() const
Return true if this sort is a Finite domain sort.
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...
func_decl operator()(context &c, Z3_ast a)
std::string to_string(expr_vector const &queries)
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
expr algebraic_upper(unsigned precision) const
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.
void Z3_API Z3_ast_vector_dec_ref(Z3_context c, Z3_ast_vector v)
Decrement the reference counter of the given AST vector.
expr operator>=(expr const &a, expr const &b)
std::string reason_unknown()
#define MK_EXPR2(_fn, _arg1, _arg2)
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...
expr replace(expr const &src, expr const &dst) const
void add_entry(expr_vector const &args, expr &value)
Z3_symbol Z3_API Z3_get_decl_symbol_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the double value associated with an double parameter.
Z3_ast Z3_API Z3_mk_set_intersect(Z3_context c, unsigned num_args, Z3_ast const args[])
Take the intersection of a list of sets.
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
expr pw(expr const &a, expr const &b)
Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)
Return the declaration of a constant or function application.
friend std::ostream & operator<<(std::ostream &out, goal const &g)
friend expr fpa_fp(expr const &sgn, expr const &exp, expr const &sig)
Create an expression of FloatingPoint sort from three bit-vector expressions.
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...
friend probe operator>=(probe const &p1, probe const &p2)
expr(context &c, Z3_ast n)
Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast default_value)
Create a fresh func_interp object, add it to a model for a specified function. It has reference count...
expr set_difference(expr const &a, expr const &b)
symbol name() const
Return name of sort.
unsigned Z3_API Z3_ast_vector_size(Z3_context c, Z3_ast_vector v)
Return the size of the given AST vector.
Z3_ast Z3_API Z3_mk_real_int64(Z3_context c, int64_t num, int64_t den)
Create a real from a fraction of int64.
unsigned id() const
retrieve unique identifier for func_decl.
expr operator~(expr const &a)
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.
expr operator[](int i) const
bool propagate(expr_vector const &fixed, expr const &conseq)
Z3_ast Z3_API Z3_mk_fpa_rtn(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode...
expr_vector assertions() const
friend expr int2bv(unsigned n, expr const &a)
expr_vector assertions() const
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.
expr_vector unsat_core() const
friend expr operator-(expr const &a)
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a string.
Z3_error_code Z3_API Z3_get_error_code(Z3_context c)
Return the error code for the last API call.
friend expr distinct(expr_vector const &args)
check_result check(unsigned n, expr *const assumptions)
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.
expr bvredor(expr const &a)
expr rem(expr const &a, expr const &b)
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.
friend expr operator*(expr const &a, expr const &b)
probe(context &c, char const *name)
friend std::ostream & operator<<(std::ostream &out, solver const &s)
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
#define MK_EXPR1(_fn, _arg)
Z3_sort Z3_API Z3_mk_string_sort(Z3_context c)
Create a sort for unicode strings.
bool is_forall() const
Return true if this expression is a universal quantifier.
friend expr min(expr const &a, expr const &b)
sort seq_sort(sort &s)
Return a sequence sort over base sort s.
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.
friend expr bvmul_no_underflow(expr const &a, expr const &b)
bool next_split(expr const &e, unsigned idx, Z3_lbool phase)
Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2)
Maximum of floating-point numbers.
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
friend expr operator<=(expr const &a, expr const &b)
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_ast Z3_API Z3_mk_char_to_bv(Z3_context c, Z3_ast ch)
Create a bit-vector (code point) from character.
Z3_ast Z3_API Z3_mk_bit2bool(Z3_context c, unsigned i, Z3_ast t1)
Extracts the bit at position i of a bit-vector and yields a boolean.
expr bvmul_no_underflow(expr const &a, expr const &b)
friend expr bvredand(expr const &a)
expr get_const_interp(func_decl c) const
Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s)
Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.
Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve upper bound value or approximation for the i'th optimization objective.
void Z3_API Z3_del_constructor_list(Z3_context c, Z3_constructor_list clist)
Reclaim memory allocated for constructor list.
Z3_constructor Z3_API Z3_mk_constructor(Z3_context c, Z3_symbol name, Z3_symbol recognizer, unsigned num_fields, Z3_symbol const field_names[], Z3_sort_opt const sorts[], unsigned sort_refs[])
Create a constructor.
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_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.
expr set_add(expr const &s, expr const &e)
expr ashr(expr const &a, expr const &b)
arithmetic shift right operator for bitvectors
expr re_empty(sort const &s)
void Z3_API Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode)
Select mode for the format used for pretty-printing AST nodes.
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.
Z3_ast Z3_API Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows dividend).
sort fpa_sort()
Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128).
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.
friend tactic operator|(tactic const &t1, tactic const &t2)
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
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...
expr nor(expr const &a, expr const &b)
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_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_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c)
Return the parameter description set for the simplify procedure.
std::string get_rational() const
fixedpoint(fixedpoint const &o)
void Z3_API Z3_solver_propagate_register_cb(Z3_context c, Z3_solver_callback cb, Z3_ast e)
register an expression to propagate on with the solver. Only expressions of type Bool and type Bit-Ve...
solver(context &c, Z3_solver s)
func_decl_vector accessors()
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.
solver & operator=(solver const &s)
Z3_ast Z3_API Z3_mk_char_from_bv(Z3_context c, Z3_ast bv)
Create a character from a bit-vector (code point).
Z3_ast Z3_API Z3_mk_fpa_rtp(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode...
void set(char const *param, int value)
Set global parameter param with integer value.
void add_cover(int level, func_decl &p, expr &property)
expr substitute(expr_vector const &src, expr_vector const &dst)
Apply substitution. Replace src expressions by dst.
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.
ast(context &c, Z3_ast n)
ast_vector_tpl & operator=(ast_vector_tpl const &s)
expr_vector cube(expr_vector &vars, unsigned cutoff)
friend expr fpa_to_sbv(expr const &t, unsigned sz)
Conversion of a floating-point term into a signed bit-vector.
expr operator<=(expr const &a, expr const &b)
friend std::ostream & operator<<(std::ostream &out, apply_result const &r)
bool is_finite_domain() const
Return true if this is a Finite-domain expression.
void set(char const *k, char const *s)
expr bv_const(char const *name, unsigned sz)
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.
user_propagator_base(context &c)
expr string_val(char const *s)
uint64_t get_numeral_uint64() const
Return uint64_t value of numeral, throw if result cannot fit in uint64_t.
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.
void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d)
Increment the reference counter of the given fixedpoint context.
void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p)
Increment the reference counter of the given probe.
sort string_sort()
Return the sort for Unicode strings.
void conflict(expr_vector const &fixed, expr_vector const &lhs, expr_vector const &rhs)
tactic with(tactic const &t, params const &p)
expr empty_set(sort const &s)
Z3_ast Z3_API Z3_mk_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s)
Check if suffix is a suffix of s.
Z3_ast_vector Z3_API Z3_mk_ast_vector(Z3_context c)
Return an empty AST vector.
expr as_array(func_decl &f)
expr plus(expr const &re)
func_decl partial_order(sort const &a, unsigned index)
expr xnor(expr const &a, expr const &b)
Z3_func_decl Z3_API Z3_get_decl_func_decl_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the expression value associated with an expression parameter.
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_int2real(Z3_context c, Z3_ast t1)
Coerce an integer to a real.
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...
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_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)
Shift left.
std::string get_decimal_string(int precision) const
Return string representation of numeral or algebraic number This method assumes the expression is num...
void from_string(char const *s)
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
sort array_domain() const
Return the domain of this Array sort.
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst)
Replace the first occurrence of src with dst in s.
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
unsigned Z3_API Z3_goal_depth(Z3_context c, Z3_goal g)
Return the depth of the given goal. It tracks how many transformations were applied to it...
void Z3_API Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r)
Increment the reference counter of the given Z3_apply_result object.
expr_vector args() const
Return a vector of all the arguments of this application. This method assumes the expression is an ap...
friend expr atleast(expr_vector const &es, unsigned bound)
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.
expr fpa_fp(expr const &sgn, expr const &exp, expr const &sig)
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 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...
func_entry(context &c, Z3_func_entry e)
void Z3_API Z3_del_config(Z3_config c)
Delete the given configuration object.
bool is_var() const
Return true if this expression is a variable.
Z3_simplifier Z3_API Z3_simplifier_using_params(Z3_context c, Z3_simplifier t, Z3_params p)
Return a simplifier that applies t using the given set of parameters.
expr extract(unsigned hi, unsigned lo) const
Z3_ast_vector Z3_API Z3_algebraic_get_poly(Z3_context c, Z3_ast a)
Return the coefficients of the defining polynomial.
expr operator[](expr_vector const &index) const
void add(expr const &e, char const *p)
func_decl to_func_decl(context &c, Z3_func_decl f)
friend simplifier with(simplifier const &t, params const &p)
expr min(expr const &a, expr const &b)
sort array_range() const
Return the range of this Array sort.
cube_iterator(solver &s, expr_vector &vars, unsigned &cutoff, bool end)
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...
param_descrs(param_descrs const &o)
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)
Create a backtracking point.
void set_cutoff(unsigned c) noexcept
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re)
Create the regular language [re].
friend expr fpa_to_fpa(expr const &t, sort s)
Conversion of a floating-point term into another floating-point.
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 variables in a with the expressions in to. For every i smaller than num_exprs...
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
unsigned Z3_API Z3_get_bv_sort_size(Z3_context c, Z3_sort t)
Return the size of the given bit-vector sort.
Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve lower bound value or approximation for the i'th optimization objective.
Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)
Create an array type.
sort fpa_rounding_mode_sort()
Return a RoundingMode sort.
bool is_string_value() const
Return true if this expression is a string literal. The string can be accessed using get_string() and...
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.
Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Check for subsetness of sets.
std::string to_smt2(char const *status="unknown")
unsigned get_numeral_uint() const
Return uint value of numeral, throw if result cannot fit in machine uint.
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...
func_decl get_func_decl(unsigned i) const
expr operator+(expr const &a, expr const &b)
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.
double Z3_API Z3_get_decl_double_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the double value associated with an double parameter.
friend probe operator!(probe const &p)
Z3_ast Z3_API Z3_mk_store_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const *idxs, Z3_ast v)
n-ary Array update.
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
expr bvadd_no_underflow(expr const &a, expr const &b)
Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg)
Take the complement of a set.
expr int2bv(unsigned n, expr const &a)
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...
expr bvneg_no_overflow(expr const &a)
func_decl tree_order(sort const &a, unsigned index)
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 re_complement(expr const &a)
model convert_model(model const &m) const
expr srem(expr const &a, expr const &b)
signed remainder 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.
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.
expr operator&(expr const &a, expr const &b)
expr set_intersect(expr const &a, expr const &b)
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.
exception(char const *msg)
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_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const *domain, Z3_sort range)
Create an array type with N arguments.
Z3_lbool
Lifted Boolean type: false, undefined, true.
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_sort Z3_API Z3_mk_fpa_rounding_mode_sort(Z3_context c)
Create the RoundingMode 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...
friend expr max(expr const &a, expr const &b)
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...
bool operator!=(iterator const &other) noexcept
expr fpa_const(char const *name, unsigned ebits, unsigned sbits)
virtual void pop(unsigned num_scopes)=0
void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g)
Decrement the reference counter of the given goal.
Z3_string Z3_API Z3_fixedpoint_get_reason_unknown(Z3_context c, Z3_fixedpoint d)
Retrieve a string that describes the last status returned by Z3_fixedpoint_query. ...
expr select(expr const &a, expr const &i)
forward declarations
expr re_intersect(expr_vector const &args)
friend expr ubv_to_fpa(expr const &t, sort s)
Conversion of an unsigned bit-vector term into a floating-point.
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.
void Z3_API Z3_solver_propagate_decide(Z3_context c, Z3_solver s, Z3_decide_eh decide_eh)
register a callback when the solver decides to split on a registered expression. The callback may cha...
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 The string may contain escape encoding f...
ast_vector_tpl< sort > sort_vector
std::function< void(expr const &proof, std::vector< unsigned > const &deps, expr_vector const &clause)> on_clause_eh_t
void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a file.
expr mk_xor(expr_vector const &args)
Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a)
Return the numerator (as a numeral AST) of a numeral AST of sort Real.
expr prefixof(expr const &a, expr const &b)
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_ubv_to_str(Z3_context c, Z3_ast s)
Unsigned bit-vector to string conversion.
Z3_parameter_kind kind() const
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_decl_kind decl_kind() const
sort datatype(symbol const &name, constructors const &cs)
Create a recursive datatype over a single sort. name is the name of the recursive datatype n - the nu...
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.
Z3_ast Z3_API Z3_mk_u32string(Z3_context c, unsigned len, unsigned const chars[])
Create a string constant out of the string that is passed in It takes the length of the string as wel...
expr operator%(expr const &a, expr const &b)
expr_vector parse_file(char const *file)
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.
Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s)
Retrieve the string constant stored in s. Characters outside the basic printable ASCII range are esca...
Z3_ast Z3_API Z3_mk_rotate_right(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the right i times.
tactic par_and_then(tactic const &t1, tactic const &t2)
unsigned Z3_API Z3_param_descrs_size(Z3_context c, Z3_param_descrs p)
Return the number of parameters in the given parameter description set.
friend expr operator==(expr const &a, expr const &b)
void set(char const *param, bool value)
Set global parameter param with Boolean value.
unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m)
Return the number of constants assigned by the given model.
expr loop(unsigned lo)
create a looping regular expression.
func_entry entry(unsigned i) const
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_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d)
Decrement the reference counter of the given fixedpoint context.
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.
bool is_relation() const
Return true if this is a Relation expression.
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_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point multiplication.
unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g)
Return the number of formulas in the given goal.
bool is_bool() const
Return true if this sort is the Boolean sort.
expr ugt(expr const &a, expr const &b)
unsigned greater than operator for bitvectors.
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_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.
goal & operator=(goal const &s)
expr option(expr const &re)
Z3_sort Z3_API Z3_get_array_sort_domain(Z3_context c, Z3_sort t)
Return the domain of the given array sort. In the case of a multi-dimensional array, this function returns the sort of the first dimension.
expr const_array(sort const &d, expr const &v)
cube_iterator operator++(int)
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f)
Retrieve set of rules from fixedpoint context.
void 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...
expr set_member(expr const &s, expr const &e)
Z3_model Z3_API Z3_mk_model(Z3_context c)
Create a fresh model object. It has reference count 0.
unsigned id() const
retrieve unique identifier for func_decl.
Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name)
create a forward reference to a recursive datatype being declared. The forward reference can be used ...
friend std::ostream & operator<<(std::ostream &out, model const &m)
Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target)
Copy a solver s from the context source to the context target.
int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s)
Return the symbol int value.
void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p)
Decrement the reference counter of the given parameter set.
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)
Decrement the reference counter of the given optimize context.
sort uninterpreted_sort(char const *name)
create an uninterpreted sort with the name given by the string or symbol.
double Z3_API Z3_probe_apply(Z3_context c, Z3_probe p, Z3_goal g)
Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0...
Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s)
Retrieve the unsat core for the last Z3_solver_check_assumptions The unsat core is a subset of the as...
goal operator[](int i) const
check_result check(expr_vector const &assumptions)
unsigned fpa_ebits() const
expr_vector trail() const
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows divisor).
bool is_numeral(double &d) const
Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e)
Return the value of this point.
expr_vector algebraic_poly() const
Return coefficients for p of an algebraic number (root-obj p i)
unsigned Z3_API Z3_stats_get_uint_value(Z3_context c, Z3_stats s, unsigned idx)
Return the unsigned value of the given statistical data.
void set_param(char const *param, char const *value)
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.
Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than.
expr bv2int(expr const &a, bool is_signed)
bit-vector and integer conversions.
friend void check_context(object const &a, object const &b)
Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g)
Convert a goal into a string.
parameter(expr const &e, unsigned idx)
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_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.
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
bool is_seq() const
Return true if this is a sequence expression.
std::u32string get_u32string() const
for a string value expression return an unespaced string value.
Z3_param_kind
The different kinds of parameters that can be associated with parameter sets. (see Z3_mk_params)...
friend expr bvsdiv_no_overflow(expr const &a, expr const &b)
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...
friend probe operator<=(probe const &p1, probe const &p2)
friend expr operator&&(expr const &a, expr const &b)
Return an expression representing a and b.
expr get_cover_delta(int level, func_decl &p)
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.
bool Z3_API Z3_is_string(Z3_context c, Z3_ast s)
Determine if s is a string constant.
expr int_const(char const *name)
Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 rem arg2.
friend expr operator&(expr const &a, expr const &b)
friend std::ostream & operator<<(std::ostream &out, exception const &e)
expr arg(unsigned i) const
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.
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.
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...
unsigned num_args() const
Return the number of arguments in this application. This method assumes the expression is an applicat...
virtual void decide(expr const &, unsigned, bool)
void register_decide(decide_eh_t &c)
Z3_symbol_kind
The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See Z3_...
expr sum(expr_vector const &args)
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_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re)
Create the regular language re+.
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_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
expr_vector from_string(char const *s)
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)
Retrieve the model for the last Z3_optimize_check.
virtual void created(expr const &)
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.
goal(context &c, bool models=true, bool unsat_cores=false, bool proofs=false)
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...
expr_vector const * operator->() const
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.
check_result consequences(expr_vector &assumptions, expr_vector &vars, expr_vector &conseq)
unsigned algebraic_i() const
Return i of an algebraic number (root-obj p i)
bool is_app() const
Return true if this expression is an application.
std::string to_string() const
friend tactic operator&(tactic const &t1, tactic const &t2)
expr operator<(expr const &a, expr const &b)
friend expr operator>(expr const &a, expr const &b)
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.
handle add(expr const &e, unsigned weight)
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.
fixedpoint & operator=(fixedpoint const &o)
Z3_symbol_kind kind() const
param_descrs get_param_descrs()
friend expr nand(expr const &a, expr const &b)
void set(params const &p)
expr fp_eq(expr const &a, expr const &b)
expr atleast(expr_vector const &es, unsigned bound)
friend tactic with(tactic const &t, params const &p)
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_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
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...
bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
expr real_const(char const *name)
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_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.
sort(context &c, Z3_ast a)
friend expr sbv_to_fpa(expr const &t, sort s)
Conversion of a signed bit-vector term into a floating-point.
func_interp get_func_interp(func_decl f) const
friend probe operator==(probe const &p1, probe const &p2)
bool operator!=(cube_iterator const &other) noexcept
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...
bool is_numeral(std::string &s, unsigned precision) const
Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1)
Repeat the given bit-vector up length i.
void conflict(expr_vector const &fixed)
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_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the expression value associated with an expression parameter.
bool operator!=(iterator const &other) const noexcept
expr algebraic_lower(unsigned precision) const
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.
double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a)
Return numeral as a double.
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_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.
Z3_sort_kind sort_kind() const
Return the internal sort kind.
bool is_numeral(std::string &s) const
bool is_arith() const
Return true if this sort is the Integer or Real sort.
Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re)
Create the regular language re*.
std::string dimacs(bool include_names=true) 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.
friend expr fma(expr const &a, expr const &b, expr const &c, expr const &rm)
FloatingPoint fused multiply-add.
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.
expr mk_is_zero() const
Return Boolean expression to test for whether an FP expression is a zero.
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_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context dst)
translate model from context c to context dst.
void from_file(char const *file)
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_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.
void Z3_API Z3_fixedpoint_add_cover(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property)
Add property about the predicate pred. Add a property of predicate pred at level. It gets pushed forw...
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.
Z3_sort Z3_API Z3_mk_real_sort(Z3_context c)
Create the real type.
friend expr pbeq(expr_vector const &es, int const *coeffs, int bound)
expr at(expr const &index) const
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. Thus, two ast nodes created by the same context and having the same children and same function symbols have the same identifiers. Ast nodes created in the same context, but having different children or different functions have different identifiers. Variables and quantifiers are also assigned different identifiers according to their structure.
bool operator==(iterator const &other) const noexcept
void add(expr_vector const &v)
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.
expr_vector trail(array< unsigned > &levels) const
Z3_ast Z3_API Z3_mk_fpa_rna(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode...
expr empty(sort const &s)
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.
bool is_well_sorted() const
Return true if this expression is well sorted (aka type correct).
Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length)
Extract subsequence starting at offset of length.
Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset)
Return index of the first occurrence of substr in s starting from offset offset. If s does not contai...
Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point addition.
Z3_config Z3_API Z3_mk_config(void)
Create a configuration object for the Z3 context object.
Z3_ast Z3_API Z3_mk_char_to_int(Z3_context c, Z3_ast ch)
Create an integer (code point) from character.
cube_generator(solver &s, expr_vector &vars)
friend tactic par_and_then(tactic const &t1, tactic const &t2)
char const * what() const
sort real_sort()
Return the Real sort.
void set(char const *k, unsigned v)
Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi)
Create the range regular expression over two sequences of length 1.
unsigned Z3_API Z3_goal_num_exprs(Z3_context c, Z3_goal g)
Return the number of formulas, subformulas and terms in the given goal.
virtual ~user_propagator_base()
friend std::ostream & operator<<(std::ostream &out, ast_vector_tpl const &v)
expr re_full(sort const &s)
Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d)
Return the range of the given declaration.
bool inconsistent() const
bool is_const() const
Return true if this expression is a constant (i.e., an application with 0 arguments).
expr arg(unsigned i) const
Return the i-th argument of this application. This method assumes the expression is an application...
Z3_ast Z3_API Z3_mk_seq_last_index(Z3_context c, Z3_ast s, Z3_ast substr)
Return index of the last occurrence of substr in s. If s does not contain substr, then the value is -...
ast_vector_tpl(ast_vector_tpl const &s)
friend expr rem(expr const &a, expr const &b)
expr num_val(int n, sort const &s)
void Z3_API Z3_fixedpoint_update_rule(Z3_context c, Z3_fixedpoint d, Z3_ast a, Z3_symbol name)
Update a named rule. A rule with the same name must have been previously created. ...
bool eq(ast const &a, ast const &b)
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.
unsigned num_consts() const
symbol int_symbol(int n)
Create a Z3 symbol based on the given integer.
Z3_tactic Z3_API Z3_tactic_repeat(Z3_context c, Z3_tactic t, unsigned max)
Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of...
expr loop(unsigned lo, unsigned hi)
void add(expr_vector const &v)
func_decl transitive_closure(func_decl const &)
void Z3_API Z3_mk_datatypes(Z3_context c, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort sorts[], Z3_constructor_list constructor_lists[])
Create mutually recursive datatypes.
expr bvmul_no_overflow(expr const &a, expr const &b, bool is_signed)
Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d)
Retrieve statistics information from the last call to Z3_optimize_check.
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
friend probe operator>(probe const &p1, probe const &p2)
expr indexof(expr const &s, expr const &substr, expr const &offset)
void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p)
Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p...
expr set_complement(expr const &a)
unsigned num_funcs() const
bool is_algebraic() const
Return true if expression is an algebraic number.
Z3_constructor operator[](unsigned i) const
expr_vector non_units() const
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
iterator(expr &e, unsigned i)
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_tactic Z3_API Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal if the probe p evaluates to true, and t2 if p evaluat...
param_descrs & operator=(param_descrs const &o)
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].
check_result to_check_result(Z3_lbool l)
expr star(expr const &re)
Z3_tactic Z3_API Z3_tactic_par_or(Z3_context c, unsigned num, Z3_tactic const ts[])
Return a tactic that applies the given tactics in parallel.
friend expr operator~(expr const &a)
Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
expr operator==(expr const &a, expr const &b)
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)
Create a new incremental solver.
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
Z3_tactic Z3_API Z3_tactic_try_for(Z3_context c, Z3_tactic t, unsigned ms)
Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms mil...
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.
friend tactic repeat(tactic const &t, unsigned max)
expr operator|(expr const &a, expr const &b)
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_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point division.
friend tactic par_or(unsigned n, tactic const *tactics)
expr pbge(expr_vector const &es, int const *coeffs, int bound)
Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re)
Create an empty regular expression of sort re.
friend expr abs(expr const &a)
tactic(context &c, Z3_tactic s)
void check_context(object const &a, object const &b)
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 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.
expr mk_from_ieee_bv(sort const &s) const
Convert this IEEE BV into a fpa.
virtual user_propagator_base * fresh(context &ctx)=0
user_propagators created using fresh() are created during search and their lifetimes are restricted t...
Z3_probe Z3_API Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned...
Z3_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f)
Return a string describing all fixedpoint available parameters.
expr bool_const(char const *name)
create uninterpreted constants of a given sort.
expr urem(expr const &a, expr const &b)
unsigned reminder operator for bitvectors
void Z3_API Z3_simplifier_inc_ref(Z3_context c, Z3_simplifier t)
Increment the reference counter of the given simplifier.
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.
expr sbv_to_fpa(expr const &t, sort s)
void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a)
Add a new formula a to the given goal. The formula is split according to the following procedure that...
Z3_tactic Z3_API Z3_tactic_fail_if(Z3_context c, Z3_probe p)
Return a tactic that fails if the probe p evaluates to false.
expr operator&&(expr const &a, expr const &b)
double apply(goal const &g) const
expr extract(expr const &offset, expr const &length) const
sequence and regular expression operations.
Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize t)
Return a string containing a description of parameters accepted by optimize.
Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s)
Return the symbol name.
unsigned Z3_API Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t)
Return number of constructors for datatype.
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...
symbol get_symbol() const
#define _Z3_MK_BIN_(a, b, binop)
void set_rounding_mode(rounding_mode rm)
Sets RoundingMode of FloatingPoints.
friend expr ite(expr const &c, expr const &t, expr const &e)
Create the if-then-else expression ite(c, t, e)
Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c, Z3_solver s, Z3_ast_vector assumptions, Z3_ast_vector variables, Z3_ast_vector consequences)
retrieve consequences from solver that determine values of the supplied function symbols.
Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i)
Return one of the subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
std::string dimacs(bool include_names=true) const
expr_vector rules() const
friend expr nor(expr const &a, expr const &b)
params & operator=(params const &s)
friend std::ostream & operator<<(std::ostream &out, symbol const &s)
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_param_descrs Z3_API Z3_get_global_param_descrs(Z3_context c)
Retrieve description of global parameters.
check_result query(func_decl_vector &relations)
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.
bool operator==(iterator const &other) noexcept
Z3_param_kind Z3_API Z3_param_descrs_get_kind(Z3_context c, Z3_param_descrs p, Z3_symbol n)
Return the kind associated with the given parameter name n.
iterator(ast_vector_tpl const *v, unsigned i)
friend expr operator<(expr const &a, expr const &b)
friend expr operator!(expr const &a)
Return an expression representing not(a).
class for auxiliary parameters associated with func_decl The class is initialized with a func_decl or...
Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1)
Take disjunction of bits in vector, return vector of length 1.
virtual ~exception()=default
friend expr bvsub_no_overflow(expr const &a, expr const &b)
solver(context &c, solver const &src, translate)
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_goal_prec precision() const
unsigned Z3_API Z3_get_func_decl_id(Z3_context c, Z3_func_decl f)
Return a unique identifier for f.
void Z3_API Z3_apply_result_dec_ref(Z3_context c, Z3_apply_result r)
Decrement the reference counter of the given Z3_apply_result object.
Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re)
Create an universal regular expression of sort re.
void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value)
add a function entry to a function interpretation.
friend expr sum(expr_vector const &args)
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...
expr lambda(expr const &x, expr const &b)
parameter(func_decl const &d, unsigned idx)
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)
Determine if an ast is a universal quantifier.
func_decl get_decl() const
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.
Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(Z3_context c, Z3_fixedpoint f)
Retrieve set of background assertions from fixedpoint context.
ast_vector_tpl< ast > ast_vector
bool is_decided_unsat() const
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.
handle minimize(expr const &e)
expr mk_is_subnormal() const
Return Boolean expression to test for whether an FP expression is a subnormal.
friend probe operator<(probe const &p1, probe const &p2)
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
expr_vector assertions() const
cube_iterator & operator++()
void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g)
Increment the reference counter of the given goal.
Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred)
bool operator==(cube_iterator const &other) noexcept
sort get_sort() const
Return the sort of this expression.
friend probe operator&&(probe const &p1, probe const &p2)
void set(char const *k, double v)
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)
Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than or equal.
bool is_exists() const
Return true if this expression is an existential quantifier.
Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c, Z3_fixedpoint d, Z3_ast query)
Pose a query against the asserted rules.
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
void set(char const *k, unsigned n)
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...
iterator begin() const noexcept
expr_vector const & operator*() const noexcept
friend expr pble(expr_vector const &es, int const *coeffs, int bound)
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point subtraction.
std::string key(unsigned i) const
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.
bool is_relation() const
Return true if this sort is a Relation sort.
Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned division.
void set(char const *k, bool b)
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.
void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p)
Increment the reference counter of the given parameter set.
Z3_solver Z3_API Z3_solver_add_simplifier(Z3_context c, Z3_solver solver, Z3_simplifier simplifier)
Attach simplifier to a solver. The solver will use the simplifier for incremental pre-processing...
unsigned num_parameters() const
Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables...
Z3_string Z3_API Z3_tactic_get_help(Z3_context c, Z3_tactic t)
Return a string containing a description of parameters accepted by the given tactic.
void Z3_API Z3_params_set_symbol(Z3_context c, Z3_params p, Z3_symbol k, Z3_symbol v)
Add a symbol parameter k with value v to the parameter set p.
bool is_int() const
Return true if this is an integer expression.
friend expr pbge(expr_vector const &es, int const *coeffs, int bound)
apply_result apply(goal const &g) const
bool is_arith() const
Return true if this is an integer or real expression.
void Z3_API Z3_global_param_reset_all(void)
Restore the value of all global (and module) parameters. This command will not affect already created...
void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m)
Increment the reference counter of the given model.
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a minimization constraint.
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_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re)
Check if seq is in the language generated by the regular expression re.
expr mk_or(expr_vector const &args)
tactic fail_if(probe const &p)
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_param_kind kind(symbol const &s)
stats(context &c, Z3_stats e)
expr exists(expr const &x, expr const &b)
expr round_fpa_to_closest_integer(expr const &t)
expr sge(expr const &a, expr const &b)
signed greater than or equal to operator for bitvectors.
ast operator()(context &c, Z3_ast a)
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
expr rotate_right(unsigned i) const
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.
expr_vector parse_string(char const *s)
parsing
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.
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.
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
func_decl user_propagate_function(symbol const &name, sort_vector const &domain, sort const &range)
void recdef(func_decl decl, expr_vector const &args, expr const &body)
add function definition body to declaration decl. decl needs to be declared using context::recfun...
bool is_array() const
Return true if this sort is a Array sort.
Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s)
Return the parameter description set for the given solver object.
unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f)
Return the number of entries in the given function interpretation.
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...
expr_vector from_file(char const *s)
void set(char const *k, symbol const &v)
expr ite(expr const &c, expr const &t, expr const &e)
Create the if-then-else expression ite(c, t, e)
T const & operator[](int i) const
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.
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...
double double_value(unsigned i) const
expr bit2bool(unsigned i) const
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
void register_eq(eq_eh_t &f)
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_seq_empty(Z3_context c, Z3_sort seq)
Create an empty sequence of the sequence sort seq.
expr body() const
Return the 'body' of this quantifier.
std::string get_string() const
for a string value expression return an escaped string value.
expr char_from_bv() const
friend expr bvneg_no_overflow(expr const &a)
Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq)
Create a regular expression that accepts the sequence seq.
double Z3_API Z3_stats_get_double_value(Z3_context c, Z3_stats s, unsigned idx)
Return the double value of the given statistical data.
cube_generator(solver &s)
void Z3_API Z3_fixedpoint_add_fact(Z3_context c, Z3_fixedpoint d, Z3_func_decl r, unsigned num_args, unsigned args[])
Add a Database fact.
ast & operator=(ast const &s)
bool is_seq() const
Return true if this sort is a Sequence sort.
func_interp add_func_interp(func_decl &f, expr &else_val)
expr repeat(unsigned i) const
bool is_bv() const
Return true if this is a Bit-vector expression.
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)
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.
sort domain(unsigned i) const
bool is_bool() const
Return true if this is a Boolean expression.
int64_t get_numeral_int64() const
Return int64_t value of numeral, throw if result cannot fit in int64_t.
sort(context &c, Z3_sort s)
double operator()(goal const &g) const
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
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_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
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_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).
bool is_datatype() const
Return true if this sort is a Datatype sort.
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.
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...
std::string to_string() const
expr implies(expr const &a, expr const &b)
void Z3_API Z3_solver_propagate_init(Z3_context c, Z3_solver s, void *user_context, Z3_push_eh push_eh, Z3_pop_eh pop_eh, Z3_fresh_eh fresh_eh)
register a user-propagator with the solver.
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...
friend expr sqrt(expr const &a, expr const &rm)
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...
bool has_interp(func_decl f) const
Z3_sort Z3_API Z3_mk_char_sort(Z3_context c)
Create a sort for unicode characters.
expr mk_is_normal() const
Return Boolean expression to test for whether an FP expression is a normal.
expr concat(expr const &a, expr const &b)
symbol(context &c, Z3_symbol s)
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.
solver(context &c, char const *logic)
tactic try_for(tactic const &t, unsigned ms)
func_interp(context &c, Z3_func_interp e)
Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, bool negative)
Create a floating-point infinity of sort s.
void register_relation(func_decl &p)
unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d)
Alias for Z3_get_domain_size.
expr fpa_nan(sort const &s)
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.
void add_rule(expr &rule, symbol const &name)
expr shl(expr const &a, expr const &b)
shift left operator for bitvectors
expr bvsdiv_no_overflow(expr const &a, expr const &b)
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.
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.
Z3_ast Z3_API Z3_mk_re_diff(Z3_context c, Z3_ast re1, Z3_ast re2)
Create the difference of regular expressions.
friend tactic try_for(tactic const &t, unsigned ms)
void push_back(T const &e)
expr pble(expr_vector const &es, int const *coeffs, int bound)
expr max(expr const &a, expr const &b)
expr sqrt(expr const &a, expr const &rm)
expr mk_to_ieee_bv() const
Convert this fpa into an IEEE BV.
ast_vector_tpl< expr > expr_vector
bool is_re() const
Return true if this is a regular expression.
Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[])
Create the union of the regular languages.
void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)
Decrement the reference counter of the given probe.
expr mk_is_nan() const
Return Boolean expression to test for whether an FP expression is a NaN.
expr uge(expr const &a, expr const &b)
unsigned greater than or equal to operator for bitvectors.
expr last_indexof(expr const &s, expr const &substr)
expr slt(expr const &a, expr const &b)
signed less than operator for bitvectors.
void set(char const *param, bool value)
Update global parameter param with Boolean value.
Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c, unsigned num_constructors, Z3_constructor const constructors[])
Create list of constructors.
void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 file with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.
void set(params const &p)
bool is_re() const
Return true if this sort is a regular expression sort.
func_decl_vector constructors()
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_get_sort_name(Z3_context c, Z3_sort d)
Return the sort name as a symbol.
bool is_quantifier() const
Return true if this expression is a quantifier.
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...
bool propagate(expr_vector const &fixed, expr_vector const &lhs, expr_vector const &rhs, expr const &conseq)
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_mk_fpa_nan(Z3_context c, Z3_sort s)
Create a floating-point NaN of sort s.
void Z3_API Z3_query_constructor(Z3_context c, Z3_constructor constr, unsigned num_fields, Z3_func_decl *constructor, Z3_func_decl *tester, Z3_func_decl accessors[])
Query constructor for declared functions.
expr fpa_inf(sort const &s, bool sgn)
bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.
expr operator-(expr const &a)
friend std::ostream & operator<<(std::ostream &out, stats const &s)
expr smod(expr const &a, expr const &b)
signed modulus operator for bitvectors
bool Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback cb, unsigned num_fixed, Z3_ast const *fixed, unsigned num_eqs, Z3_ast const *eq_lhs, Z3_ast const *eq_rhs, Z3_ast conseq)
propagate a consequence based on fixed values and equalities. A client may invoke it during the propa...
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.
expr to_real(expr const &a)
void register_created(created_eh_t &c)
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
friend expr implies(expr const &a, expr const &b)
void Z3_API Z3_fixedpoint_register_relation(Z3_context c, Z3_fixedpoint d, Z3_func_decl f)
Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics...
param_descrs get_param_descrs()
void add(symbol const &name, symbol const &rec, unsigned n, symbol const *names, sort const *fields)
Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a)
Create a unit sequence of a.
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.
void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a)
Increment the reference counter of the given AST. The context c should have been created using Z3_mk_...
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...
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.
Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2)
Minimum of floating-point numbers.
tactic par_or(unsigned n, tactic const *tactics)
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.
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_decl_kind
The different kinds of interpreted function kinds.
T operator[](unsigned i) const
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a maximization constraint.
expr sgt(expr const &a, expr const &b)
signed greater than operator for bitvectors.
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_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than or equal.
apply_result(context &c, Z3_apply_result s)
expr nand(expr const &a, expr const &b)
unsigned Z3_API Z3_apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r)
Return the number of subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort seq)
Create a regular expression sort out of a sequence sort.
Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d)
Retrieve a formula that encodes satisfying answers to the query.
Z3_string Z3_API Z3_fixedpoint_to_string(Z3_context c, Z3_fixedpoint f, unsigned num_queries, Z3_ast queries[])
Print the current rules and background axioms as a string.
Z3_lbool Z3_API Z3_fixedpoint_query_relations(Z3_context c, Z3_fixedpoint d, unsigned num_relations, Z3_func_decl const relations[])
Pose multiple queries against the asserted rules.
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.
expr fpa_to_ubv(expr const &t, unsigned sz)
static param_descrs global_param_descrs(context &c)
expr operator/(expr const &a, expr const &b)
void Z3_API Z3_solver_register_on_clause(Z3_context c, Z3_solver s, void *user_context, Z3_on_clause_eh on_clause_eh)
register a callback to that retrieves assumed, inferred and deleted clauses during search...
Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than.
void query(unsigned i, func_decl &constructor, func_decl &test, func_decl_vector &accs)
Function declaration (aka function definition). It is the signature of interpreted and uninterpreted ...
expr set_union(expr const &a, expr const &b)
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.
expr_vector objectives() const
bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t)
Return true if the given expression t is well sorted.
int get_numeral_int() const
Return int value of numeral, throw if result cannot fit in machine int.
param_descrs get_param_descrs()
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...
virtual void fixed(expr const &, expr const &)
Z3_probe Z3_API Z3_probe_or(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when p1 or p2 evaluates to true.
sort int_sort()
Return the integer sort.
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...
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th constructor.
ast_vector_tpl(context &c, ast_vector_tpl const &src)
expr set_del(expr const &s, expr const &e)
void set(params const &p)
check_result check(expr_vector const &asms)
#define _Z3_MK_UN_(a, mkun)
void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g)
Decrement the reference counter of the given tactic.
simplifier & operator=(simplifier const &s)
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.
simplifier(context &c, char const *name)
unsigned num_args() const
expr bvsub_no_overflow(expr const &a, expr const &b)
Z3_ast Z3_API Z3_mk_sbv_to_str(Z3_context c, Z3_ast s)
Signed bit-vector to string conversion.
Z3_lbool bool_value() const
expr fpa_to_sbv(expr const &t, unsigned sz)
bool Z3_API Z3_solver_next_split(Z3_context c, Z3_solver_callback cb, Z3_ast t, unsigned idx, Z3_lbool phase)
apply_result & operator=(apply_result const &s)
Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s)
Integer to string conversion.
Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_symbol name, unsigned n, Z3_sort *domain, Z3_sort range)
expr atmost(expr_vector const &es, unsigned bound)
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_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.
bool is_real() const
Return true if this sort is the Real sort.
Z3_ast Z3_API Z3_substitute_funs(Z3_context c, Z3_ast a, unsigned num_funs, Z3_func_decl const from[], Z3_ast const to[])
Substitute functions in from with new expressions in to.
bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a)
Determine if ast is a lambda expression.
sort to_sort(context &c, Z3_sort s)
expr string_const(char const *name)
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_simplifier Z3_API Z3_mk_simplifier(Z3_context c, Z3_string name)
Return a simplifier associated with the given name. The complete list of simplifiers may be obtained ...
Z3_sort Z3_API Z3_get_decl_sort_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the sort value associated with a sort parameter.
void Z3_API Z3_solver_propagate_eq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh)
register a callback on expression equalities.
bool is_decided_sat() const
on_clause(solver &s, on_clause_eh_t &on_clause_eh)
friend expr mk_xor(expr_vector const &args)
Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than.
friend expr range(expr const &lo, expr const &hi)
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...
expr to_re(expr const &s)
func_decl linear_order(sort const &a, unsigned index)
void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)
Check if container contains containee.
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.
std::string to_string() const
bool is_numeral_i(int &i) const
param_descrs get_param_descrs()
const char * Z3_string
Z3 string type. It is just an alias for const char *.
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_select_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const *idxs)
n-ary Array read. The argument a is the array and idxs are the indices of the array that gets read...
apply_result(apply_result const &s)
bool is_fpa() const
Return true if this sort is a Floating point sort.