Go to the documentation of this file.
89 char const *
msg()
const {
return m_msg.c_str(); }
90 char const *
what()
const throw() {
return m_msg.c_str(); }
95 #if !defined(Z3_THROW)
96 #if __cpp_exceptions || _CPPUNWIND || __EXCEPTIONS
97 #define Z3_THROW(x) throw x
99 #define Z3_THROW(x) {}
101 #endif // !defined(Z3_THROW)
113 operator Z3_config()
const {
return m_cfg; }
125 void set(
char const * param,
int value) {
126 auto str = std::to_string(value);
157 bool m_enable_exceptions;
163 void set_context(Z3_context ctx) {
165 m_enable_exceptions =
true;
166 m_rounding_mode =
RNA;
176 context(Z3_context c) { set_context(c); }
177 void detach() { m_ctx =
nullptr; }
182 operator Z3_context()
const {
return m_ctx; }
220 void set(
char const * param,
int value) {
221 auto str = std::to_string(value);
284 template<
size_t precision>
338 expr fpa_const(
char const * name,
unsigned ebits,
unsigned sbits);
340 template<
size_t precision>
400 array(
unsigned sz):m_size(sz) { m_array =
new T[sz]; }
401 template<
typename T2>
404 void resize(
unsigned sz) {
delete[] m_array; m_size = sz; m_array =
new T[sz]; }
405 unsigned size()
const {
return m_size; }
406 T &
operator[](
int i) { assert(0 <= i); assert(
static_cast<unsigned>(i) < m_size);
return m_array[i]; }
407 T
const &
operator[](
int i)
const { assert(0 <= i); assert(
static_cast<unsigned>(i) < m_size);
return m_array[i]; }
408 T
const *
ptr()
const {
return m_array; }
409 T *
ptr() {
return m_array; }
420 friend void check_context(
object const & a,
object const & b);
430 operator Z3_symbol()
const {
return m_sym; }
439 out <<
"k!" << s.
to_int();
447 Z3_param_descrs m_descrs;
454 m_descrs = o.m_descrs;
476 operator Z3_params()
const {
return m_params; }
481 m_params = s.m_params;
504 operator Z3_ast()
const {
return m_ast; }
505 operator bool()
const {
return m_ast != 0; }
509 friend std::ostream &
operator<<(std::ostream & out,
ast const & n);
516 friend bool eq(
ast const & a,
ast const & b);
526 Z3_ast_vector m_vector;
535 operator Z3_ast_vector()
const {
return m_vector; }
547 m_vector = s.m_vector;
571 return other.m_index == m_index;
574 return other.m_index != m_index;
587 iterator
begin()
const {
return iterator(
this, 0); }
588 iterator
end()
const {
return iterator(
this,
size()); }
602 operator Z3_sort()
const {
return reinterpret_cast<Z3_sort
>(
m_ast); }
703 operator Z3_func_decl()
const {
return reinterpret_cast<Z3_func_decl
>(
m_ast); }
739 expr
select(expr
const & a, expr
const& i);
934 assert(
ctx().enable_exceptions());
935 if (!
ctx().enable_exceptions())
return 0;
954 assert(
ctx().enable_exceptions());
955 if (!
ctx().enable_exceptions())
return 0;
971 assert(
ctx().enable_exceptions());
972 if (!
ctx().enable_exceptions())
return 0;
988 assert(
ctx().enable_exceptions());
989 if (!
ctx().enable_exceptions())
return 0;
1030 return std::string(s);
1038 return std::string(s, n);
1041 operator Z3_app()
const { assert(
is_app());
return reinterpret_cast<Z3_app
>(
m_ast); }
1350 return select(*
this, index);
1356 return select(*
this, index);
1380 #define _Z3_MK_BIN_(a, b, binop) \
1381 check_context(a, b); \
1382 Z3_ast r = binop(a.ctx(), a, b); \
1384 return expr(a.ctx(), r); \
1427 #define _Z3_MK_UN_(a, mkun) \
1428 Z3_ast r = mkun(a.ctx(), a); \
1430 return expr(a.ctx(), r); \
1442 Z3_ast args[2] = { a, b };
1454 Z3_ast args[2] = { a, b };
1475 Z3_ast args[2] = { a, b };
1487 Z3_ast args[2] = { a, b };
1497 Z3_ast _args[2] = { a, b };
1517 Z3_ast args[2] = { a, b };
1581 else if (a.
is_bv()) {
1599 Z3_ast args[2] = { a, b };
1708 else if (a.
is_bv()) {
1723 else if (a.
is_bv()) {
1968 return sort(c,
reinterpret_cast<Z3_sort
>(a));
1976 return func_decl(c,
reinterpret_cast<Z3_func_decl
>(a));
1980 template<
typename T>
1981 template<
typename T2>
1983 m_array =
new T[v.
size()];
1985 for (
unsigned i = 0; i < m_size; i++) {
1994 Z3_app vars[] = {(Z3_app) x};
1999 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2004 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2009 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2018 Z3_app vars[] = {(Z3_app) x};
2023 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2028 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2033 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2042 Z3_app vars[] = {(Z3_app) x};
2047 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2052 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2057 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2066 assert(es.
size() > 0);
2071 return expr(ctx, r);
2074 assert(es.
size() > 0);
2079 return expr(ctx, r);
2082 assert(es.
size() > 0);
2087 return expr(ctx, r);
2090 assert(es.
size() > 0);
2095 return expr(ctx, r);
2098 assert(es.
size() > 0);
2103 return expr(ctx, r);
2106 assert(args.
size() > 0);
2111 return expr(ctx, r);
2115 assert(args.
size() > 0);
2120 return expr(ctx, r);
2127 Z3_ast _args[2] = { a, b };
2131 Z3_ast _args[2] = { a, b };
2143 assert(args.
size() > 0);
2144 if (args.
size() == 1) {
2156 r = _args[args.
size()-1];
2157 for (
unsigned i = args.
size()-1; i > 0; ) {
2164 return expr(ctx, r);
2171 return expr(args.ctx(), r);
2177 return expr(args.ctx(), r);
2182 Z3_func_entry m_entry;
2183 void init(Z3_func_entry e) {
2191 operator Z3_func_entry()
const {
return m_entry; }
2196 m_entry = s.m_entry;
2205 Z3_func_interp m_interp;
2206 void init(Z3_func_interp e) {
2214 operator Z3_func_interp()
const {
return m_interp; }
2219 m_interp = s.m_interp;
2237 void init(Z3_model m) {
2248 operator Z3_model()
const {
return m_model; }
2253 m_model = s.m_model;
2262 if (status ==
false &&
ctx().enable_exceptions())
2311 friend std::ostream &
operator<<(std::ostream & out,
model const & m);
2319 void init(Z3_stats e) {
2328 operator Z3_stats()
const {
return m_stats; }
2333 m_stats = s.m_stats;
2342 friend std::ostream &
operator<<(std::ostream & out,
stats const & s);
2348 if (r ==
unsat) out <<
"unsat";
2349 else if (r ==
sat) out <<
"sat";
2350 else out <<
"unknown";
2357 void init(Z3_solver s) {
2371 operator Z3_solver()
const {
return m_solver; }
2376 m_solver = s.m_solver;
2395 add(e,
ctx().bool_const(p));
2399 for (
unsigned i = 0; i < v.
size(); ++i)
2418 for (
unsigned i = 0; i < n; i++) {
2420 _assumptions[i] = assumptions[i];
2427 unsigned n = assumptions.
size();
2429 for (
unsigned i = 0; i < n; i++) {
2431 _assumptions[i] = assumptions[i];
2454 unsigned sz = result.
size();
2463 std::string
to_smt2(
char const* status =
"unknown") {
2465 Z3_ast
const* fmls = es.
ptr();
2467 unsigned sz = es.
size();
2503 assert(!m_end && !m_empty);
2504 m_cube = m_solver.
cube(m_vars, m_cutoff);
2505 m_cutoff = 0xFFFFFFFF;
2506 if (m_cube.
size() == 1 && m_cube[0].is_false()) {
2510 else if (m_cube.
empty()) {
2542 return other.m_end == m_end;
2545 return other.m_end != m_end;
2558 m_cutoff(0xFFFFFFFF),
2559 m_default_vars(s.
ctx()),
2560 m_vars(m_default_vars)
2565 m_cutoff(0xFFFFFFFF),
2566 m_default_vars(s.
ctx()),
2583 void init(Z3_goal s) {
2592 operator Z3_goal()
const {
return m_goal; }
2623 unsigned n =
size();
2630 for (
unsigned i = 0; i < n; i++)
2631 args[i] =
operator[](i);
2636 friend std::ostream &
operator<<(std::ostream & out,
goal const & g);
2641 Z3_apply_result m_apply_result;
2642 void init(Z3_apply_result s) {
2650 operator Z3_apply_result()
const {
return m_apply_result; }
2655 m_apply_result = s.m_apply_result;
2666 void init(Z3_tactic s) {
2675 operator Z3_tactic()
const {
return m_tactic; }
2680 m_tactic = s.m_tactic;
2736 Z3_THROW(
exception(
"a non-zero number of tactics need to be passed to par_or"));
2739 for (
unsigned i = 0; i < n; ++i) buffer[i] =
tactics[i];
2752 void init(Z3_probe s) {
2762 operator Z3_probe()
const {
return m_probe; }
2767 m_probe = s.m_probe;
2835 unsigned h()
const {
return m_h; }
2847 for (expr_vector::iterator it = v.
begin(); it != v.
end(); ++it)
minimize(*it);
2857 operator Z3_optimize()
const {
return m_opt; }
2863 for (expr_vector::iterator it = es.
begin(); it != es.
end(); ++it)
add(*it);
2871 add(e,
ctx().bool_const(p));
2875 auto str = std::to_string(weight);
2899 unsigned n = asms.
size();
2901 for (
unsigned i = 0; i < n; i++) {
2937 operator Z3_fixedpoint()
const {
return m_fp; }
3017 switch (m_rounding_mode) {
3023 default:
return sort(*
this);
3036 for (
unsigned i = 0; i < n; i++) { _enum_names[i] =
Z3_mk_string_symbol(*
this, enum_names[i]); }
3048 for (
unsigned i = 0; i < n; i++) { _names[i] =
Z3_mk_string_symbol(*
this, names[i]); _sorts[i] = sorts[i]; }
3068 for (
unsigned i = 0; i < arity; i++) {
3070 args[i] = domain[i];
3083 for (
unsigned i = 0; i < domain.
size(); i++) {
3085 args[i] = domain[i];
3099 Z3_sort args[1] = { domain };
3107 Z3_sort args[2] = { d1, d2 };
3115 Z3_sort args[3] = { d1, d2, d3 };
3123 Z3_sort args[4] = { d1, d2, d3, d4 };
3131 Z3_sort args[5] = { d1, d2, d3, d4, d5 };
3139 for (
unsigned i = 0; i < arity; i++) {
3141 args[i] = domain[i];
3158 sort dom[2] = { d1, d2 };
3171 return expr(*
this, r);
3180 template<
size_t precision>
3205 for (
unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
3220 for (
unsigned i = 0; i < n; i++) {
3231 for (
unsigned i = 0; i < args.
size(); i++) {
3246 Z3_ast args[1] = { a };
3259 Z3_ast args[2] = { a1, a2 };
3280 Z3_ast args[3] = { a1, a2, a3 };
3287 Z3_ast args[4] = { a1, a2, a3, a4 };
3294 Z3_ast args[5] = { a1, a2, a3, a4, a5 };
3386 #define MK_EXPR1(_fn, _arg) \
3387 Z3_ast r = _fn(_arg.ctx(), _arg); \
3388 _arg.check_error(); \
3389 return expr(_arg.ctx(), r);
3391 #define MK_EXPR2(_fn, _arg1, _arg2) \
3392 check_context(_arg1, _arg2); \
3393 Z3_ast r = _fn(_arg1.ctx(), _arg1, _arg2); \
3394 _arg1.check_error(); \
3395 return expr(_arg1.ctx(), r);
3419 Z3_ast es[2] = { a, b };
3427 Z3_ast es[2] = { a, b };
3508 assert(args.
size() > 0);
3513 return expr(ctx, r);
3546 for (
unsigned i = 0; i < sorts.
size(); ++i) {
3547 sort_names[i] = sorts[i].name();
3549 for (
unsigned i = 0; i < decls.
size(); ++i) {
3550 decl_names[i] = decls[i].name();
3563 for (
unsigned i = 0; i < sorts.
size(); ++i) {
3564 sort_names[i] = sorts[i].name();
3566 for (
unsigned i = 0; i < decls.
size(); ++i) {
3567 decl_names[i] = decls[i].name();
3579 for (
unsigned i = 0; i < src.
size(); ++i) {
3590 for (
unsigned i = 0; i < dst.
size(); ++i) {
3605 final_eh_t m_final_eh;
3607 fixed_eh_t m_fixed_eh;
3610 Z3_solver_callback cb {
nullptr };
3613 return c ? c : (Z3_context)s->
ctx();
3626 static void push_eh(
void* p) {
3630 static void pop_eh(
void* p,
unsigned num_scopes) {
3634 static void* fresh_eh(
void* p, Z3_context ctx) {
3638 static void fixed_eh(
void* _p, Z3_solver_callback cb,
unsigned id, Z3_ast _value) {
3640 scoped_cb _cb(p, cb);
3642 expr value(ctx(), _value);
3646 static void eq_eh(
void* p, Z3_solver_callback cb,
unsigned x,
unsigned y) {
3647 scoped_cb _cb(p, cb);
3651 static void final_eh(
void* p, Z3_solver_callback cb) {
3652 scoped_cb _cb(p, cb);
3662 virtual void pop(
unsigned num_scopes) = 0;
3700 void final(final_eh_t& f) {
3728 expr conseq = _ctx().bool_val(
false);
3734 assert(conseq.
ctx() == ctx());
3739 unsigned num_eqs,
unsigned const* lhs,
unsigned const * rhs,
3740 expr const& conseq) {
3742 assert(conseq.
ctx() == ctx());
Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re)
Create the regular language re+.
expr operator!=(expr const &a, expr const &b)
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...
Z3_bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast *v)
Evaluate the AST node t in the given model. Return true if succeeded, and store the result in v.
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...
handle add_soft(expr const &e, char const *weight)
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
expr plus(expr const &re)
expr xnor(expr const &a, expr const &b)
double double_value(unsigned i) const
void add(expr_vector const &v)
ast(context &c, Z3_ast n)
expr suffixof(expr const &a, expr const &b)
tactic fail_if(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.
void from_string(char const *constraints)
Z3_ast Z3_API Z3_solver_get_implied_lower(Z3_context c, Z3_solver s, Z3_ast e)
retrieve implied lower bound value for arithmetic expression. If a lower bound is implied at search l...
expr pw(expr const &a, expr const &b)
void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m)
Decrement the reference counter of the given model.
Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context dst)
translate model from context c to context dst.
expr at(expr const &index) const
friend expr operator&(expr const &a, expr const &b)
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.
expr set_difference(expr const &a, expr const &b)
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
expr as_array(func_decl &f)
expr get_cover_delta(int level, func_decl &p)
void interrupt()
Interrupt the current procedure being executed by any object managed by this context....
friend expr max(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.
Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re)
Create the regular language [re].
expr bv2int(expr const &a, bool is_signed)
bit-vector and integer conversions.
bool as_binary(std::string &s) const
Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t)
Create a new solver that is implemented using the given tactic. The solver supports the commands Z3_s...
Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)
Shift left.
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.
bool operator!=(cube_iterator const &other)
A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort ...
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.
solver(context &c, char const *logic)
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 Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a)
Test if there exists an interpretation (i.e., assignment) for a in the model m.
Z3_sort_kind sort_kind() const
Return the internal sort kind.
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.
bool is_fpa() const
Return true if this sort is a Floating point sort.
double operator()(goal const &g) const
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.
func_decl get_const_decl(unsigned i) const
expr set_member(expr const &s, expr const &e)
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.
Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s)
Integer to string conversion.
void Z3_API Z3_params_set_uint(Z3_context c, Z3_params p, Z3_symbol k, unsigned v)
Add a unsigned parameter k with value v to the parameter set p.
Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re)
Create the complement of the regular language re.
void Z3_API Z3_params_set_double(Z3_context c, Z3_params p, Z3_symbol k, double v)
Add a double parameter k with value v to the parameter set p.
Z3_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.
friend expr operator>(expr const &a, expr const &b)
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
expr_vector assertions() const
param_descrs(context &c, Z3_param_descrs d)
solver & operator=(solver const &s)
void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t)
Increment the reference counter of the given tactic.
bool is_relation() const
Return true if this sort is a Relation sort.
void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz, unsigned levels[])
retrieve the decision depth of Boolean literals (variables or their negations). Assumes a check-sat c...
Z3_ast Z3_API Z3_mk_fpa_rtn(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
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.
ast_vector_tpl< sort > sort_vector
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.
sort string_sort()
Return the sort for ASCII strings.
sort array_sort(sort d, sort r)
Return an array sort for arrays from d to r.
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.
friend expr operator==(expr const &a, expr const &b)
friend std::ostream & operator<<(std::ostream &out, stats const &s)
symbol name() const
Return name of sort.
expr set_complement(expr const &a)
iterator operator=(iterator const &other)
expr bvadd_no_overflow(expr const &a, expr const &b, bool is_signed)
bit-vector overflow/underflow checks
expr ult(expr const &a, expr const &b)
unsigned less than operator for bitvectors.
expr to_re(expr const &s)
Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2)
Minimum of floating-point numbers.
iterator(iterator const &other)
expr operator^(expr const &a, expr const &b)
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
bool is_const() const
Return true if this expression is a constant (i.e., an application with 0 arguments).
tactic par_and_then(tactic const &t1, tactic const &t2)
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
void add_const_interp(func_decl &f, expr &value)
Z3_ast Z3_API Z3_mk_true(Z3_context c)
Create an AST node representing true.
std::string reason_unknown() const
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.
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.
friend expr fma(expr const &a, expr const &b, expr const &c, expr const &rm)
FloatingPoint fused multiply-add.
void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a)
Decrement the reference counter of the given AST. The context c should have been created using Z3_mk_...
Z3_ast_vector Z3_API Z3_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.
void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value)
Set a value of a context parameter.
Z3_ast Z3_API Z3_mk_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 operator%(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.
scoped_context(Z3_context c)
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_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.
friend tactic try_for(tactic const &t, unsigned ms)
void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)
Decrement the reference counter of the given probe.
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point remainder.
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_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err)
Return a string describing the given error code.
sort int_sort()
Return the integer sort.
#define _Z3_MK_BIN_(a, b, binop)
std::string key(unsigned i) const
Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.
probe(context &c, Z3_probe s)
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)
Decrement the reference counter of the given optimize context.
Z3_probe Z3_API Z3_probe_and(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when p1 and p2 evaluates to true.
bool is_numeral_i(int &i) const
Z3_ast Z3_API Z3_mk_zero_ext(Z3_context c, unsigned i, Z3_ast t1)
Extend the given bit-vector with zeros to the (unsigned) equivalent bit-vector of size m+i,...
expr replace(expr const &src, expr const &dst) const
Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c, Z3_fixedpoint d, Z3_ast query)
Pose a query against the asserted rules.
bool is_re() const
Return true if this sort is a regular expression sort.
static param_descrs simplify_param_descrs(context &c)
friend expr bvsdiv_no_overflow(expr const &a, expr const &b)
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
friend expr operator&&(expr const &a, expr const &b)
Return an expression representing a and b.
friend std::ostream & operator<<(std::ostream &out, ast_vector_tpl const &v)
Z3_config Z3_API Z3_mk_config(void)
Create a configuration object for the Z3 context object.
cube_iterator(solver &s, expr_vector &vars, unsigned &cutoff, bool end)
ast_vector_tpl(ast_vector_tpl const &s)
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[](int i) const
Z3_ast Z3_API Z3_mk_fpa_rtz(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
expr_vector rules() const
bool is_forall() const
Return true if this expression is a universal quantifier.
func_decl operator()(context &c, Z3_ast a)
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_...
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
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.
void add(expr const &e, expr const &p)
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
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...
friend tactic with(tactic const &t, params const &p)
Z3_symbol_kind Z3_API Z3_get_symbol_kind(Z3_context c, Z3_symbol s)
Return Z3_INT_SYMBOL if the symbol was constructed using Z3_mk_int_symbol, and Z3_STRING_SYMBOL if th...
void from_file(char const *s)
unsigned algebraic_i() const
Return i of an algebraic number (root-obj p i)
Z3_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.
Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s)
Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.
Z3_ast_vector Z3_API Z3_fixedpoint_from_string(Z3_context c, Z3_fixedpoint f, Z3_string s)
Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context....
Z3_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...
model(context &c, Z3_model m)
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.
expr bvsub_no_underflow(expr const &a, expr const &b, bool is_signed)
std::string to_string() const
sort & operator=(sort const &s)
Return true if this sort and s are equal.
expr range(expr const &lo, expr const &hi)
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...
friend expr nand(expr const &a, expr const &b)
bool is_numeral(std::string &s, unsigned precision) const
void set(params const &p)
expr lower(handle const &h)
unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a)
Return the number of argument of an application. If t is an constant, then the number of arguments is...
Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re)
Create an universal regular expression of sort re.
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.
bool is_relation() const
Return true if this is a Relation expression.
expr upper(handle const &h)
Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)
Return the declaration of a constant or function application.
Z3_param_kind
The different kinds of parameters that can be associated with parameter sets. (see Z3_mk_params).
unsigned Z3_API Z3_get_ast_hash(Z3_context c, Z3_ast a)
Return a hash code for the given AST. The hash code is structural. You can use Z3_get_ast_id intercha...
Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast t1, bool is_signed)
Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is t...
Z3_char_ptr Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned *length)
Retrieve the unescaped string constant stored in s.
func_decl operator[](int i) const
optimize & operator=(optimize const &o)
func_decl get_func_decl(unsigned i) const
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.
user_propagator_base(solver *s)
expr is_int(expr const &e)
expr lambda(expr const &x, expr const &b)
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_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].
friend probe operator||(probe const &p1, probe const &p2)
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point square root.
std::string dimacs(bool include_names=true) const
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.
Exception used to sign API usage errors.
bool is_numeral_u(unsigned &i) const
expr bvmul_no_underflow(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...
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.
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_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
unsigned id() const
retrieve unique identifier for expression.
goal operator[](int i) const
void set(char const *k, char const *v)
ast operator()(context &c, Z3_ast a)
void set(params const &p)
check_result check(expr_vector const &asms)
sort domain(unsigned i) const
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...
void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p)
Set parameters on fixedpoint context.
void Z3_API Z3_interrupt(Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers,...
sort re_sort(sort &seq_sort)
Return a regular expression sort over sequences seq_sort.
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....
friend expr pbeq(expr_vector const &es, int const *coeffs, int bound)
friend expr operator<(expr const &a, expr const &b)
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
friend expr bvsub_no_overflow(expr const &a, expr const &b)
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...
sort seq_sort(sort &s)
Return a sequence sort over base sort s.
tactic & operator=(tactic const &s)
unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g)
Return the number of formulas in the given goal.
expr select(expr const &a, expr const &i)
forward declarations
Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem)
Remove an element to a set.
friend expr rem(expr const &a, expr const &b)
friend std::ostream & operator<<(std::ostream &out, optimize const &s)
void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value)
Set a configuration parameter.
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.
void set(char const *param, int value)
Update global parameter param with Integer value.
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 Z3_API Z3_mk_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s)
Check if suffix is a suffix of s.
bool is_array() const
Return true if this sort is a Array sort.
check_result check(unsigned n, expr *const assumptions)
Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 xor t2.
expr option(expr const &re)
model(model &src, context &dst, translate)
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...
func_interp & operator=(func_interp const &s)
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.
expr loop(unsigned lo, unsigned hi)
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.
expr udiv(expr const &a, expr const &b)
unsigned division operator for bitvectors.
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
void add(expr_vector const &es)
unsigned fpa_ebits() const
cube_iterator operator++(int)
Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[])
Check whether the assertions in the given solver and optional assumptions are consistent or not.
Z3_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_full_set(Z3_context c, Z3_sort domain)
Create the full set.
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.
expr sext(expr const &a, unsigned i)
Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i,...
expr upper(expr const &e)
optimize(context &c, optimize &src)
bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
Compare terms.
friend expr pble(expr_vector const &es, int const *coeffs, int bound)
unsigned Z3_API Z3_get_sort_id(Z3_context c, Z3_sort s)
Return a unique identifier for s.
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...
void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d)
Increment the reference counter of the given fixedpoint context.
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_smt2(char const *status="unknown")
unsigned Z3_API Z3_algebraic_get_i(Z3_context c, Z3_ast a)
Return which root of the polynomial the algebraic number represents.
friend std::ostream & operator<<(std::ostream &out, ast const &n)
expr ashr(expr const &a, expr const &b)
arithmetic shift right operator for bitvectors
friend expr operator~(expr const &a)
friend expr pbge(expr_vector const &es, int const *coeffs, int bound)
expr int_const(char const *name)
Z3_ast Z3_API Z3_mk_set_union(Z3_context c, unsigned num_args, Z3_ast const args[])
Take the union of a list of sets.
void set(char const *k, symbol const &s)
expr simplify() const
Return a simplified version of this expression.
apply_result apply(goal const &g) const
expr bv_const(char const *name, unsigned sz)
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_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f)
Return a string describing all fixedpoint available parameters.
user_propagator_base(Z3_context c)
void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g)
Erase all formulas from the given goal.
expr algebraic_lower(unsigned precision) const
void add(expr const &e, char const *p)
unsigned Z3_API Z3_goal_num_exprs(Z3_context c, Z3_goal g)
Return the number of formulas, subformulas and terms in the given goal.
friend expr abs(expr const &a)
void Z3_API Z3_ast_vector_push(Z3_context c, Z3_ast_vector v, Z3_ast a)
Add the AST a in the end of the AST vector v. The size of v is increased by one.
Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f)
Return the 'else' value of the given function interpretation.
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 set(char const *k, unsigned n)
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
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....
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
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.
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.
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)
Create the empty set.
friend expr ite(expr const &c, expr const &t, expr const &e)
Create the if-then-else expression ite(c, t, e)
sort operator()(context &c, Z3_ast a)
Z3_ast Z3_API Z3_goal_formula(Z3_context c, Z3_goal g, unsigned idx)
Return a formula from the given goal.
expr bvmul_no_overflow(expr const &a, expr const &b, bool is_signed)
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_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nor.
friend expr nor(expr const &a, expr const &b)
goal & operator=(goal const &s)
void Z3_API Z3_solver_propagate_eq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh)
register a callback on expression equalities.
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.
const char * Z3_string
Z3 string type. It is just an alias for const char *.
expr lshr(expr const &a, expr const &b)
logic shift right operator for bitvectors
check_result query(func_decl_vector &relations)
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.
unsigned Z3_API Z3_ast_vector_size(Z3_context c, Z3_ast_vector v)
Return the size of the given AST vector.
unsigned num_args() const
Return the number of arguments in this application. This method assumes the expression is an applicat...
Z3_model Z3_API Z3_mk_model(Z3_context c)
Create a fresh model object. It has reference count 0.
Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi)
Create a regular expression loop. The supplied regular expression r is repeated between lo and hi tim...
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than or equal.
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 add(expr const &e, expr const &t)
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a maximization constraint.
bool is_decided_unsat() const
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.
apply_result operator()(goal const &g) const
friend expr bvneg_no_overflow(expr const &a)
expr exists(expr const &x, expr const &b)
Z3_lbool
Lifted Boolean type: false, undefined, true.
friend expr sum(expr_vector const &args)
Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d)
Retrieve a formula that encodes satisfying answers to the query.
int get_numeral_int() const
Return int value of numeral, throw if result cannot fit in machine int.
expr_vector assertions() const
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.
friend expr operator!(expr const &a)
Return an expression representing not(a).
bool is_bv() const
Return true if this sort is a Bit-vector sort.
solver(context &c, Z3_solver s)
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 Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g)
Decrement the reference counter of the given tactic.
bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)
Determine if an ast is a universal quantifier.
bool Z3_API Z3_is_string(Z3_context c, Z3_ast s)
Determine if s is a string constant.
expr uge(expr const &a, expr const &b)
unsigned greater than or equal to operator for bitvectors.
tactic try_for(tactic const &t, unsigned ms)
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
T const & operator[](int i) const
expr operator||(expr const &a, expr const &b)
expr constant(symbol const &name, sort const &s)
expr rotate_left(unsigned i)
Z3 global configuration object.
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.
void Z3_API Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode)
Select mode for the format used for pretty-printing AST nodes.
Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than.
bool is_var() const
Return true if this expression is a variable.
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_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s)
Check if prefix is a prefix of s.
void Z3_API Z3_param_descrs_dec_ref(Z3_context c, Z3_param_descrs p)
Decrement the reference counter of the given parameter description set.
friend expr sqrt(expr const &a, expr const &rm)
Z3_ast Z3_API Z3_mk_fpa_rna(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
void push_back(T const &e)
friend std::ostream & operator<<(std::ostream &out, goal const &g)
Z3_ast Z3_API Z3_get_algebraic_number_upper(Z3_context c, Z3_ast a, unsigned precision)
Return a upper bound for the given real algebraic number. The interval isolating the number is smalle...
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
bool operator==(cube_iterator const &other)
expr operator!(expr const &a)
bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t)
Return true if the given expression t is well sorted.
ast & operator=(ast const &s)
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
void Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback, unsigned num_fixed, unsigned const *fixed_ids, unsigned num_eqs, unsigned const *eq_lhs, unsigned const *eq_rhs, Z3_ast conseq)
propagate a consequence based on fixed values. This is a callback a client may invoke during the fixe...
friend std::ostream & operator<<(std::ostream &out, params const &p)
uint64_t get_numeral_uint64() const
Return uint64_t value of numeral, throw if result cannot fit in uint64_t.
void from_string(char const *s)
Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 rem arg2.
Z3_ast_vector Z3_API Z3_algebraic_get_poly(Z3_context c, Z3_ast a)
Return the coefficients of the defining polynomial.
exception(char const *msg)
Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a)
Create a unit sequence of a.
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 fpa_const(char const *name, unsigned ebits, unsigned sbits)
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_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.
bool is_numeral(std::string &s) const
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.
#define _Z3_MK_UN_(a, mkun)
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 urem(expr const &a, expr const &b)
unsigned reminder operator for bitvectors
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.
void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d)
Decrement the reference counter of the given fixedpoint context.
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_ast Z3_API Z3_mk_fpa_rne(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
expr_vector objectives() const
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.
ast_vector_tpl(context &c)
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.
std::string to_string() const
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits)
Create a FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_rtp(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.
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.
sort(context &c, Z3_ast a)
bool is_quantifier() const
Return true if this expression is a quantifier.
Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s)
Return the length of the sequence s.
expr_vector cube(expr_vector &vars, unsigned cutoff)
expr value(expr const &e)
Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re)
Create the regular language re*.
probe(context &c, char const *name)
expr last_indexof(expr const &s, expr const &substr)
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...
void recdef(func_decl, expr_vector const &args, expr const &body)
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c)
Return the parameter description set for the simplify procedure.
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.
bool is_seq() const
Return true if this is a sequence expression.
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.
param_descrs get_param_descrs()
bool enable_exceptions() const
Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than.
expr sqrt(expr const &a, expr const &rm)
Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s)
Retrieve the string constant stored in s.
expr operator<(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.
unsigned id() const
retrieve unique identifier for func_decl.
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.
friend probe operator!(probe const &p)
sort fpa_sort()
Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128).
Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg)
Take the complement of a set.
void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p)
Decrement the reference counter of the given parameter set.
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point subtraction.
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a)
Return the denominator (as a numeral AST) of a numeral AST of sort Real.
Z3_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.
solver(context &c, simple)
Z3_ast Z3_API Z3_mk_exists_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Similar to Z3_mk_forall_const.
Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than or equal to.
expr shl(expr const &a, expr const &b)
shift left operator for bitvectors
std::string get_escaped_string() const
for a string value expression return an escaped or unescaped string value.
ast_vector_tpl(context &c, ast_vector_tpl const &src)
Z3_ast Z3_API Z3_mk_seq_last_index(Z3_context c, Z3_ast, Z3_ast substr)
Return the last occurrence of substr in s. If s does not contain substr, then the value is -1,...
virtual user_propagator_base * fresh(Z3_context ctx)=0
user_propagators created using fresh() are created during search and their lifetimes are restricted t...
void register_relation(func_decl &p)
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.
bool is_int() const
Return true if this is an integer expression.
bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a)
Determine if ast is an existential quantifier.
Z3_string Z3_API Z3_ast_vector_to_string(Z3_context c, Z3_ast_vector v)
Convert AST vector into a string.
void add_rule(expr &rule, symbol const &name)
void set_param(char const *param, char const *value)
void from_file(char const *file)
void Z3_API Z3_ast_vector_dec_ref(Z3_context c, Z3_ast_vector v)
Decrement the reference counter of the given AST vector.
Z3_decl_kind decl_kind() const
expr string_val(char const *s)
expr operator[](expr_vector const &index) const
expr set_del(expr const &s, expr const &e)
expr empty_set(sort const &s)
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.
handle maximize(expr const &e)
friend tactic operator&(tactic const &t1, tactic const &t2)
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.
bool is_finite_domain() const
Return true if this is a Finite-domain expression.
param_descrs get_param_descrs()
ast_vector_tpl< ast > ast_vector
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.
expr pble(expr_vector const &es, int const *coeffs, int bound)
expr ugt(expr const &a, expr const &b)
unsigned greater than operator for bitvectors.
Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s)
Convert string to integer.
void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g)
Decrement the reference counter of the given goal.
friend std::ostream & operator<<(std::ostream &out, exception const &e)
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.
symbol & operator=(symbol const &s)
friend probe operator>=(probe const &p1, probe const &p2)
bool is_datatype() const
Return true if this sort is a Datatype sort.
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.
func_decl(func_decl const &s)
Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1)
Repeat the given bit-vector up length i.
cube_iterator & operator++()
expr nor(expr const &a, expr const &b)
A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort.
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.
unsigned fpa_sbits() const
expr operator&&(expr const &a, expr const &b)
expr_vector algebraic_poly() const
Return coefficients for p of an algebraic number (root-obj p i)
friend expr mk_or(expr_vector const &args)
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.
func_entry(context &c, Z3_func_entry e)
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....
sort to_sort(context &c, Z3_sort s)
void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p)
Increment the reference counter of the given probe.
expr operator>(expr const &a, expr const &b)
void set(char const *param, char const *value)
Update global parameter param with string value.
bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g)
Return true if the goal contains false, and it is precise or the product of an over approximation.
Z3_ast_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...
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_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi)
Create the range regular expression over two sequences of length 1.
expr lower(expr const &e)
expr min(expr const &a, expr const &b)
bool operator==(iterator const &other) const
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
Z3_ast Z3_API Z3_mk_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,...
goal(context &c, bool models=true, bool unsat_cores=false, bool proofs=false)
friend expr implies(expr const &a, expr const &b)
void from_file(char const *filename)
void Z3_API Z3_ast_vector_inc_ref(Z3_context c, Z3_ast_vector v)
Increment the reference counter of the given AST vector.
bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a)
Return true if the given AST is a real algebraic number.
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
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....
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 mod(expr const &a, expr const &b)
ast_vector_tpl< func_decl > func_decl_vector
Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Take the set difference between two sets.
void add_entry(expr_vector const &args, expr &value)
Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than or equal to.
void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f)
Increment the reference counter of the given Z3_func_interp object.
sort bv_sort(unsigned sz)
Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz.
expr empty(sort const &s)
Z3_goal_prec precision() const
param_descrs(param_descrs const &o)
expr operator()(context &c, Z3_ast a)
friend tactic repeat(tactic const &t, unsigned max)
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,...
friend tactic par_or(unsigned n, tactic const *tactics)
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
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.
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
bool inconsistent() const
apply_result(apply_result const &s)
void add_fact(func_decl &f, unsigned *args)
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...
std::ostream & operator<<(std::ostream &out, exception const &e)
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.
friend expr xnor(expr const &a, expr const &b)
expr_vector unsat_core() const
expr fma(expr const &a, expr const &b, expr const &c, expr const &rm)
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...
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.
expr bvsub_no_overflow(expr const &a, expr const &b)
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...
func_decl & operator=(func_decl const &s)
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.
unsigned get_num_levels(func_decl &p)
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.
cube_generator(solver &s)
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point division.
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.
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.
void add(expr const &e, char const *p)
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_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g)
Convert a goal into a string.
void Z3_API Z3_fixedpoint_register_relation(Z3_context c, Z3_fixedpoint d, Z3_func_decl f)
Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics...
void set(char const *param, bool value)
Set global parameter param with Boolean value.
Function declaration (aka function definition). It is the signature of interpreted and uninterpreted ...
friend probe operator>(probe const &p1, probe const &p2)
expr operator<=(expr const &a, expr const &b)
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_goal_inc_ref(Z3_context c, Z3_goal g)
Increment the reference counter of the given goal.
friend std::ostream & operator<<(std::ostream &out, solver const &s)
void set(char const *k, char const *s)
friend expr operator>=(expr const &a, expr const &b)
Z3_symbol_kind kind() const
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_vector non_units() const
model convert_model(model const &m) const
friend expr bvmul_no_overflow(expr const &a, expr const &b, bool is_signed)
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.
expr real_val(int n, int d)
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)
Return the number of parameters associated with a declaration.
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....
check_result check(expr_vector const &assumptions)
func_decl transitive_closure(func_decl const &)
expr mk_and(expr_vector const &args)
friend expr range(expr const &lo, expr const &hi)
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
expr extract(expr const &offset, expr const &length) const
sequence and regular expression operations.
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_stats_dec_ref(Z3_context c, Z3_stats s)
Decrement the reference counter of the given statistics object.
goal(context &c, Z3_goal s)
expr contains(expr const &s)
unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m)
Return the number of function interpretations in the given model.
friend expr bvsub_no_underflow(expr const &a, expr const &b, bool is_signed)
expr bvsdiv_no_overflow(expr const &a, expr const &b)
expr set_add(expr const &s, expr const &e)
unsigned num_args() const
model & operator=(model const &s)
Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)
Create a bit-vector type of the given size.
expr arg(unsigned i) const
friend tactic operator|(tactic const &t1, tactic const &t2)
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)
Create a new fixedpoint context.
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a string.
Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq)
Create a regular expression that accepts the sequence seq.
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
Z3_probe Z3_API Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than or equal to the...
Z3_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.
unsigned num_entries() const
expr ule(expr const &a, expr const &b)
unsigned less than or equal to operator for bitvectors.
friend expr operator|(expr const &a, expr const &b)
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...
void set(char const *param, bool value)
Update global parameter param with Boolean value.
void check_parser_error() const
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_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned remainder.
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...
void add(expr_vector const &v)
expr pbeq(expr_vector const &es, int const *coeffs, int bound)
void set(char const *k, symbol const &v)
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...
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.
Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s)
Return the set of units modulo model conversion.
bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned int....
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows divisor).
void set(char const *k, bool 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 ...
expr operator~(expr const &a)
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.
void set_rounding_mode(rounding_mode rm)
Sets RoundingMode of FloatingPoints.
friend expr atmost(expr_vector const &es, unsigned bound)
expr sle(expr const &a, expr const &b)
signed less than or equal to operator for bitvectors.
friend expr bv2int(expr const &a, bool is_signed)
bit-vector and integer conversions.
friend expr operator+(expr const &a, expr const &b)
unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d)
Alias for Z3_get_domain_size.
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....
friend expr pw(expr const &a, expr const &b)
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)
Check if container contains containee.
friend std::ostream & operator<<(std::ostream &out, model const &m)
unsigned get_numeral_uint() const
Return uint value of numeral, throw if result cannot fit in machine uint.
unsigned bv_size() const
Return the size of this Bit-vector sort.
apply_result & operator=(apply_result const &s)
bool is_finite_domain() const
Return true if this sort is a Finite domain sort.
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....
bool is_algebraic() const
Return true if expression is an algebraic number.
sort(context &c, Z3_sort s)
expr mk_or(expr_vector const &args)
expr_vector units() const
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
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....
bool is_int() const
Return true if this sort is the Integer sort.
Z3_ast Z3_API Z3_ast_vector_get(Z3_context c, Z3_ast_vector v, unsigned i)
Return the AST at position i in the AST vector v.
Z3_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...
expr re_empty(sort const &s)
Z3_ast_vector Z3_API Z3_mk_ast_vector(Z3_context c)
Return an empty AST vector.
bool is_datatype() const
Return true if this is a Datatype expression.
expr int2bv(unsigned n, expr const &a)
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_param_descrs Z3_API Z3_tactic_get_param_descrs(Z3_context c, Z3_tactic t)
Return the parameter description set for the given tactic object.
Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.
void Z3_API Z3_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...
void set(char const *k, unsigned v)
expr operator*(expr const &a, expr const &b)
Z3_probe Z3_API Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned...
sort real_sort()
Return the Real sort.
Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq)
Create an empty sequence of the sequence sort seq.
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.
void Z3_API Z3_ast_vector_resize(Z3_context c, Z3_ast_vector v, unsigned n)
Resize the AST vector v.
Z3_ast Z3_API Z3_solver_get_implied_value(Z3_context c, Z3_solver s, Z3_ast e)
retrieve implied value for expression, if any is implied by solver at search level....
friend probe operator<=(probe const &p1, probe const &p2)
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...
void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p)
Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p.
Z3_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 ...
ast_vector_tpl< expr > expr_vector
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.
handle add(expr const &e, unsigned weight)
expr operator/(expr const &a, expr const &b)
void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p)
Increment the reference counter of the given parameter set.
Z3_sort Z3_API Z3_mk_string_sort(Z3_context c)
Create a sort for 8 bit strings.
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.
expr sum(expr_vector const &args)
bool is_seq() const
Return true if this sort is a Sequence sort.
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.
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.
expr bvneg_no_overflow(expr const &a)
func_decl linear_order(sort const &a, unsigned index)
friend expr concat(expr const &a, expr const &b)
Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(Z3_context c, Z3_fixedpoint f)
Retrieve set of background assertions from fixedpoint context.
void Z3_API Z3_del_config(Z3_config c)
Delete the given configuration object.
void conflict(unsigned num_fixed, unsigned const *fixed)
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.
bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a)
Determine if ast is a lambda expression.
bool is_real() const
Return true if this is a real expression.
Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)
Create an array type.
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_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1)
Create an n bit bit-vector from the integer argument t1.
void Z3_API Z3_solver_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...
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.
bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
unsigned Z3_API Z3_get_bv_sort_size(Z3_context c, Z3_sort t)
Return the size of the given bit-vector sort.
expr_vector parse_file(char const *file)
friend expr bvadd_no_underflow(expr const &a, expr const &b)
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_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_false(Z3_context c)
Create an AST node representing false.
expr smod(expr const &a, expr const &b)
signed modulus operator for bitvectors
bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int....
Z3_sort Z3_API Z3_get_array_sort_range(Z3_context c, Z3_sort t)
Return the range of the given array sort.
void set(char const *k, double n)
expr operator|(expr const &a, expr const &b)
expr max(expr const &a, expr const &b)
sort fpa_rounding_mode()
Return a RoundingMode sort.
void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m)
Increment the reference counter of the given model.
friend expr operator!=(expr const &a, expr const &b)
symbol(context &c, Z3_symbol s)
Z3_ast_vector Z3_API Z3_parse_smtlib2_string(Z3_context c, Z3_string str, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Parse the given string using the SMT-LIB2 parser.
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.
Z3_ast_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_arith() const
Return true if this sort is the Integer or Real sort.
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
expr rotate_right(unsigned i)
expr real_const(char const *name)
sort uninterpreted_sort(char const *name)
create an uninterpreted sort with the name given by the string or symbol.
Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, uint64_t v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d)
Return the range of the given declaration.
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...
expr forall(expr const &x, expr const &b)
std::string get_decimal_string(int precision) const
Return string representation of numeral or algebraic number This method assumes the expression is num...
Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i)
Return the i-th argument of the given application.
expr rem(expr const &a, expr const &b)
friend expr bvadd_no_overflow(expr const &a, expr const &b, bool is_signed)
bit-vector overflow/underflow checks
std::string get_string() const
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)
Create a new optimize context.
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_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m)
Convert the given model into a string.
ast_vector_tpl(context &c, Z3_ast_vector v)
Z3_symbol_kind
The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See Z3_...
expr distinct(expr_vector const &args)
solver(context &c, solver const &src, translate)
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set)
Check for set membership.
bool is_numeral(double &d) const
expr prefixof(expr const &a, expr const &b)
friend expr operator/(expr const &a, expr const &b)
expr extract(unsigned hi, unsigned lo) const
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.
expr operator-(expr const &a)
tactic when(probe const &p, tactic const &t)
func_decl(context &c, Z3_func_decl n)
Z3_tactic Z3_API Z3_tactic_par_or(Z3_context c, unsigned num, Z3_tactic const ts[])
Return a tactic that applies the given tactics in parallel.
Z3_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.
func_interp(func_interp const &s)
void propagate(unsigned num_fixed, unsigned const *fixed, unsigned num_eqs, unsigned const *lhs, unsigned const *rhs, expr const &conseq)
void check_context(object const &a, object const &b)
Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than.
expr bvadd_no_underflow(expr const &a, expr const &b)
void set_cutoff(unsigned c)
friend void check_context(object const &a, object const &b)
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.
friend probe operator<(probe const &p1, probe const &p2)
Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than.
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
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.
friend expr operator^(expr const &a, expr const &b)
expr concat(expr const &a, expr const &b)
friend expr mk_and(expr_vector const &args)
@ Z3_PRINT_SMTLIB2_COMPLIANT
std::string documentation(symbol const &s)
func_interp(context &c, Z3_func_interp e)
friend probe operator&&(probe const &p1, probe const &p2)
friend expr mod(expr const &a, expr const &b)
func_decl tree_order(sort const &a, unsigned index)
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.
void update_rule(expr &rule, symbol const &name)
expr atmost(expr_vector const &es, unsigned bound)
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.
expr_vector trail() const
void set(char const *k, bool v)
Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[])
Create the union of the regular languages.
Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned division.
ast_vector_tpl & operator=(ast_vector_tpl const &s)
bool is_re() const
Return true if this is a regular expression.
std::string to_string(expr_vector const &queries)
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)
Create a backtracking point.
bool is_bv() const
Return true if this is a Bit-vector expression.
Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort seq)
Create a regular expression sort out of a sequence sort.
char const * what() const
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
expr(context &c, Z3_ast n)
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...
void set(params const &p)
sort fpa_rounding_mode()
Return a RoundingMode sort.
bool is_double(unsigned i) const
bool eq(ast const &a, ast const &b)
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,...
bool is_exists() const
Return true if this expression is an existential quantifier.
Z3_func_decl Z3_API Z3_mk_tree_order(Z3_context c, Z3_sort a, unsigned id)
create a tree ordering relation over signature a identified using index id.
Z3_error_code Z3_API Z3_get_error_code(Z3_context c)
Return the error code for the last API call.
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.
check_result query(expr &q)
unsigned Z3_API Z3_solver_propagate_register(Z3_context c, Z3_solver s, Z3_ast e)
register an expression to propagate on with the solver. Only expressions of type Bool and type Bit-Ve...
bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx)
Return true if the given statistical data is a double.
unsigned add(expr const &e)
tracks e by a unique identifier that is returned by the call.
bool is_array() const
Return true if this is a Array expression.
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_vector assertions() const
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
Z3_ast Z3_API Z3_solver_get_implied_upper(Z3_context c, Z3_solver s, Z3_ast e)
retrieve implied upper bound value for arithmetic expression. If an upper bound is implied at search ...
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 ...
unsigned Z3_API Z3_fpa_get_ebits(Z3_context c, Z3_sort s)
Retrieves the number of bits reserved for the exponent in a FloatingPoint sort.
Z3_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.
friend expr operator||(expr const &a, expr const &b)
Return an expression representing a or b.
friend std::ostream & operator<<(std::ostream &out, apply_result const &r)
expr implies(expr const &a, expr const &b)
friend expr int2bv(unsigned n, expr const &a)
Z3_ast Z3_API Z3_substitute(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const from[], Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs....
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)
Create a new incremental solver.
Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.
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 is_real() const
Return true if this sort is the Real sort.
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...
void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h)
Register a Z3 error handler.
expr nth(expr const &index) const
bool operator!=(iterator const &other) const
Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
Z3_ast Z3_API Z3_mk_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_max(Z3_context c, Z3_ast t1, Z3_ast t2)
Maximum of floating-point numbers.
expr nand(expr const &a, expr const &b)
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,...
expr store(expr const &a, expr const &i, expr const &v)
func_decl function(std::string const &name, sort_vector const &domain, sort const &range)
Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v)
Array update.
func_entry(func_entry const &s)
Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort d)
Return the sort name as a symbol.
void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s)
Increment the reference counter of the given statistics object.
double apply(goal const &g) const
bool is_bool() const
Return true if this sort is the Boolean sort.
void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a file.
unsigned num_consts() const
expr algebraic_upper(unsigned precision) const
friend probe operator==(probe const &p1, probe const &p2)
expr eval(expr const &n, bool model_completion=false) const
A Context manages all other Z3 objects, global configuration options, etc.
func_interp add_func_interp(func_decl &f, expr &else_val)
expr atleast(expr_vector const &es, unsigned bound)
unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m)
Return the number of constants assigned by the given model.
ast_vector_tpl & set(unsigned idx, ast &a)
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...
check_result to_check_result(Z3_lbool l)
T operator[](int i) const
expr & operator=(expr const &n)
void set(char const *param, char const *value)
Set global parameter param with string value.
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.
int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s)
Return the symbol int value.
func_decl partial_order(sort const &a, unsigned index)
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
expr operator[](expr const &index) const
tactic with(tactic const &t, params const &p)
Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point multiplication.
#define MK_EXPR2(_fn, _arg1, _arg2)
unsigned id() const
retrieve unique identifier for func_decl.
expr to_real(expr const &a)
expr num_val(int n, sort const &s)
Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d)
Return the constant declaration name as a symbol.
sort array_range() const
Return the range of this Array sort.
stats & operator=(stats const &s)
friend tactic par_and_then(tactic const &t1, tactic const &t2)
void add_cover(int level, func_decl &p, expr &property)
Z3_ast Z3_API Z3_mk_real(Z3_context c, int num, int den)
Create a real from a fraction.
expr_vector const & operator*() const
Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem)
Add an element to a set.
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_param_kind kind(symbol const &s)
expr operator&(expr const &a, expr const &b)
expr substitute(expr_vector const &src, expr_vector const &dst)
Apply substitution. Replace src expressions by dst.
Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset)
Return index of first occurrence of substr in s starting from offset offset. If s does not contain su...
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)
Create the constant array.
Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d)
Return declaration kind corresponding to declaration.
std::string reason_unknown()
void Z3_API Z3_params_set_symbol(Z3_context c, Z3_params p, Z3_symbol k, Z3_symbol v)
Add a symbol parameter k with value v to the parameter set p.
Z3_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const to[])
Substitute the free variables in a with the expressions in to. For every i smaller than num_exprs,...
bool has_interp(func_decl f) const
func_decl to_func_decl(context &c, Z3_func_decl f)
Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1)
Coerce an integer to a real.
void Z3_API Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r)
Increment the reference counter of the given Z3_apply_result object.
Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[])
Create the intersection of the regular languages.
bool is_lambda() const
Return true if this expression is a lambda expression.
Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point addition.
tactic cond(probe const &p, tactic const &t1, tactic const &t2)
bool is_numeral_i64(int64_t &i) const
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
expr set_intersect(expr const &a, expr const &b)
virtual void pop(unsigned num_scopes)=0
expr bool_const(char const *name)
cube_generator cubes(expr_vector &vars)
expr_vector trail(array< unsigned > &levels) const
bool is_uint(unsigned i) const
void propagate(unsigned num_fixed, unsigned const *fixed, expr const &conseq)
friend expr operator-(expr const &a)
expr const_array(sort const &d, expr const &v)
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.
func_interp get_func_interp(func_decl f) const
#define MK_EXPR1(_fn, _arg)
friend expr distinct(expr_vector const &args)
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_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.
tactic(context &c, Z3_tactic s)
unsigned Z3_API Z3_get_func_decl_id(Z3_context c, Z3_func_decl f)
Return a unique identifier for f.
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
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.
stats(context &c, Z3_stats e)
expr operator>=(expr const &a, expr const &b)
friend expr operator*(expr const &a, expr const &b)
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.
friend expr bvmul_no_underflow(expr const &a, expr const &b)
param_descrs get_param_descrs()
friend expr operator<=(expr const &a, expr const &b)
iterator(ast_vector_tpl const *v, unsigned i)
Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
void set_else(expr &value)
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.
double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a)
Return numeral as a double.
expr_vector const * operator->() const
friend expr min(expr const &a, expr const &b)
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.
sort bool_sort()
Return the Boolean sort.
handle minimize(expr const &e)
tactic par_or(unsigned n, tactic const *tactics)
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,...
params & operator=(params const &s)
friend std::ostream & operator<<(std::ostream &out, symbol const &s)
sort array_domain() const
Return the domain of this Array sort.
expr indexof(expr const &s, expr const &substr, expr const &offset)
bool is_well_sorted() const
Return true if this expression is well sorted (aka type correct).
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.
Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index)
Retrieve from s the unit sequence positioned at position index. The sequence is empty if the index is...
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
void set(char const *param, int value)
Set global parameter param with integer value.
Z3_ast Z3_API Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows dividend).
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.
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
tactic(context &c, char const *name)
expr star(expr const &re)
expr full_set(sort const &s)
unsigned uint_value(unsigned i) const
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_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 Z3_API Z3_fixedpoint_add_cover(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property)
Add property about the predicate pred. Add a property of predicate pred at level. It gets pushed forw...
Z3_error_code check_error() const
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 ...
expr set_union(expr const &a, expr const &b)
check_result consequences(expr_vector &assumptions, expr_vector &vars, expr_vector &conseq)
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)
Retrieve the model for the last Z3_optimize_check.
tactic repeat(tactic const &t, unsigned max=UINT_MAX)
Z3_ast Z3_API Z3_mk_lambda_const(Z3_context c, unsigned num_bound, Z3_app const bound[], Z3_ast body)
Create a lambda expression using a list of constants that form the set of bound variables.
Z3_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_error_code check_error() const
Auxiliary method used to check for API usage errors.
void from_string(char const *s)
Z3_tactic Z3_API Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1.
Z3_decl_kind
The different kinds of interpreted function kinds.
bool is_fpa() const
Return true if this is a FloatingPoint expression. .
friend bool eq(ast const &a, ast const &b)
Return true if the ASTs are structurally identical.
expr set_subset(expr const &a, expr const &b)
Z3_error_code
Z3 error codes (See Z3_get_error_code).
void set(char const *k, double v)
unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e)
Return the number of arguments in a Z3_func_entry object.
expr re_complement(expr const &a)
expr re_full(sort const &s)
handle add_soft(expr const &e, unsigned weight)
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_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Check for subsetness of sets.
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.
func_decl piecewise_linear_order(sort const &a, unsigned index)
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
apply_result(context &c, Z3_apply_result s)
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than.
Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2)
Logical shift right.
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_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].
unsigned num_funcs() const
Z3_sort Z3_API Z3_mk_real_sort(Z3_context c)
Create the real type.
Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s)
Return the symbol name.
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.
bool is_bool() const
Return true if this is a Boolean expression.
expr re_intersect(expr_vector const &args)
Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re)
Create an empty regular expression of sort re.
expr_vector unsat_core() const
std::string to_string() const
expr body() const
Return the 'body' of this quantifier.
void fixed(fixed_eh_t &f)
register callbacks. Callbacks can only be registered with user_propagators that were created using a ...
func_entry entry(unsigned i) const
Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e)
Return the value of this point.
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f)
Retrieve set of rules from fixedpoint context.
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...
friend expr atleast(expr_vector const &es, unsigned bound)
expr pbge(expr_vector const &es, int const *coeffs, int bound)
probe(context &c, double val)
expr_vector parse_string(char const *s)
parsing
Z3_lbool bool_value() const
unsigned num_exprs() const
func_entry & operator=(func_entry const &s)
bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g)
Return true if the given goal contains the formula false.
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_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...
expr loop(unsigned lo)
create a looping regular expression.
expr operator==(expr const &a, expr const &b)
expr bv_val(int n, unsigned sz)
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
std::string dimacs(bool include_names=true) const
expr in_re(expr const &s, expr const &re)
expr srem(expr const &a, expr const &b)
signed remainder operator for bitvectors
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_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].
expr get_const_interp(func_decl c) const
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.
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a minimization constraint.
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.
expr operator+(expr const &a, expr const &b)
Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred)
bool is_app() const
Return true if this expression is an application.
expr ite(expr const &c, expr const &t, expr const &e)
Create the if-then-else expression ite(c, t, e)
cube_generator(solver &s, expr_vector &vars)
Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c, Z3_func_decl f)
create transitive closure of binary relation.
param_descrs & operator=(param_descrs const &o)
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.
bool is_arith() const
Return true if this is an integer or real expression.
bool is_string_value() const
Return true if this expression is a string literal. The string can be accessed using get_string() and...
bool is_numeral_u64(uint64_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:
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.
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.
sort get_sort() const
Return the sort of this expression.
int64_t get_numeral_int64() const
Return int64_t value of numeral, throw if result cannot fit in int64_t.
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
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.
symbol int_symbol(int n)
Create a Z3 symbol based on the given integer.
expr slt(expr const &a, expr const &b)
signed less than operator for bitvectors.
bool is_decided_sat() const
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.
probe & operator=(probe const &s)