84 char const *
msg()
const {
return m_msg.c_str(); }
112 void set(
char const * param,
int value) {
113 std::ostringstream oss;
158 void set(
char const * param,
int value) {
159 std::ostringstream oss;
205 sort enumeration_sort(
char const * name,
unsigned n,
char const *
const * enum_names, func_decl_vector & cs, func_decl_vector & ts);
208 func_decl function(
char const * name,
unsigned arity,
sort const * domain,
sort const & range);
210 func_decl function(
char const * name, sort_vector
const& domain,
sort const& range);
255 array(
unsigned sz):m_size(sz) { m_array =
new T[sz]; }
256 template<
typename T2>
259 unsigned size()
const {
return m_size; }
260 T &
operator[](
int i) { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size);
return m_array[i]; }
261 T
const &
operator[](
int i)
const { assert(0 <= i); assert(static_cast<unsigned>(i) < m_size);
return m_array[i]; }
262 T
const *
ptr()
const {
return m_array; }
263 T *
ptr() {
return m_array; }
271 object(
object const & s):m_ctx(s.m_ctx) {}
274 friend void check_context(
object const & a,
object const & b);
284 operator Z3_symbol()
const {
return m_sym; }
290 out <<
"k!" << s.
to_int();
292 out << s.
str().c_str();
309 m_params = s.m_params;
330 operator bool()
const {
return m_ast != 0; }
341 friend bool eq(
ast const & a,
ast const & b);
594 Z3_ast args[2] = { a, b };
625 Z3_ast args[2] = { a, b };
670 Z3_ast args[2] = { a, b };
682 Z3_ast args[2] = { a, b };
702 Z3_ast args[2] = { a, b };
749 else if (a.
is_bv()) {
764 Z3_ast args[2] = { a, b };
999 return sort(c, reinterpret_cast<Z3_sort>(a));
1007 return func_decl(c, reinterpret_cast<Z3_func_decl>(a));
1011 template<
typename T>
1012 class ast_vector_tpl :
public object {
1032 m_vector = s.m_vector;
1038 template<
typename T>
1039 template<
typename T2>
1041 m_array =
new T[v.size()];
1043 for (
unsigned i = 0; i < m_size; i++) {
1101 assert(args.
size() > 0);
1106 return expr(ctx, r);
1124 m_entry = s.m_entry;
1147 m_interp = s.m_interp;
1170 m_model = s.m_model;
1180 throw exception(
"failed to evaluate expression");
1226 m_stats = s.m_stats;
1243 if (r ==
unsat) out <<
"unsat";
1244 else if (r ==
sat) out <<
"sat";
1245 else out <<
"unknown";
1272 m_solver = s.m_solver;
1286 add(e,
ctx().bool_const(p));
1291 for (
unsigned i = 0; i < n; i++) {
1293 _assumptions[i] = assumptions[i];
1300 unsigned n = assumptions.
size();
1302 for (
unsigned i = 0; i < n; i++) {
1304 _assumptions[i] = assumptions[i];
1349 unsigned n =
size();
1356 for (
unsigned i = 0; i < n; i++)
1357 args[i] =
operator[](i);
1379 m_apply_result = s.m_apply_result;
1409 m_tactic = s.m_tactic;
1475 m_probe = s.m_probe;
1531 return tactic(t1.ctx(), r);
1544 for (
unsigned i = 0; i < n; i++) { _enum_names[i] =
Z3_mk_string_symbol(*
this, enum_names[i]); }
1556 for (
unsigned i = 0; i < arity; i++) {
1558 args[i] = domain[i];
1566 return function(range.
ctx().
str_symbol(name), arity, domain, range);
1571 for (
unsigned i = 0; i < domain.
size(); i++) {
1573 args[i] = domain[i];
1581 return function(range.
ctx().
str_symbol(name), domain, range);
1603 Z3_sort args[3] = { d1, d2, d3 };
1611 Z3_sort args[4] = { d1, d2, d3, d4 };
1619 Z3_sort args[5] = { d1, d2, d3, d4, d5 };
1628 return expr(*
this, r);
1661 for (
unsigned i = 0; i < n; i++) {
1672 for (
unsigned i = 0; i < args.
size(); i++) {
1700 Z3_ast args[2] = { a1, a2 };
1721 Z3_ast args[3] = { a1, a2, a3 };
1728 Z3_ast args[4] = { a1, a2, a3, a4 };
1735 Z3_ast args[5] = { a1, a2, a3, a4, a5 };
1744 return range.
ctx().
function(name, arity, domain, range);
1746 inline func_decl function(
char const * name,
unsigned arity,
sort const * domain,
sort const & range) {
1747 return range.
ctx().
function(name, arity, domain, range);
1756 return range.
ctx().
function(name, d1, d2, d3, range);
1759 return range.
ctx().
function(name, d1, d2, d3, d4, range);
1762 return range.
ctx().
function(name, d1, d2, d3, d4, d5, range);
1794 for (
unsigned i = 0; i < src.
size(); ++i) {
1805 for (
unsigned i = 0; i < dst.
size(); ++i) {
ast_vector_tpl(context &c)
expr distinct(expr_vector const &args)
Z3_ast Z3_API Z3_mk_const(__in Z3_context c, __in Z3_symbol s, __in Z3_sort ty)
Declare and create a constant.
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Z3_ast Z3_API Z3_mk_power(__in Z3_context c, __in Z3_ast arg1, __in Z3_ast arg2)
Create an AST node representing arg1^arg2.
friend expr operator|(expr const &a, expr const &b)
std::string reason_unknown() const
Z3_ast Z3_API Z3_mk_forall_const(__in Z3_context c, unsigned weight, unsigned num_bound, __in_ecount(num_bound) Z3_app const bound[], unsigned num_patterns, __in_ecount(num_patterns) Z3_pattern const patterns[], __in Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables...
Z3_bool Z3_API Z3_is_well_sorted(__in Z3_context c, __in Z3_ast t)
Return true if the given expression t is well sorted.
sort bool_sort()
Return the Boolean sort.
friend expr operator+(expr const &a, expr const &b)
void Z3_API Z3_solver_assert_and_track(__in Z3_context c, __in Z3_solver s, __in Z3_ast a, __in Z3_ast p)
Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p...
friend expr pw(expr const &a, expr const &b)
Power operator.
Z3_ast Z3_API Z3_mk_bvule(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Unsigned less than or equal to.
Z3_context Z3_API Z3_mk_context_rc(__in Z3_config c)
Create a context using the given configuration. This function is similar to Z3_mk_context. However, in the context returned by this function, the user is responsible for managing Z3_ast reference counters. Managing reference counters is a burden and error-prone, but allows the user to use the memory more efficiently. The user must invoke Z3_inc_ref for any Z3_ast returned by Z3, and Z3_dec_ref whenever the Z3_ast is not needed anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD.
Z3_ast Z3_API Z3_mk_mul(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].The array args must have num_args el...
Z3_sort Z3_API Z3_mk_bool_sort(__in Z3_context c)
Create the Boolean type.
friend expr operator>=(expr const &a, int b)
Z3_string Z3_API Z3_solver_to_string(__in Z3_context c, __in Z3_solver s)
Convert a solver into a string.
Z3_lbool Z3_API Z3_solver_check(__in Z3_context c, __in Z3_solver s)
Check whether the assertions in a given solver are consistent or not.
void Z3_API Z3_inc_ref(__in Z3_context c, __in Z3_ast a)
Increment the reference counter of the given AST. The context c should have been created using Z3_mk_...
bool is_int() const
Return true if this sort is the Integer sort.
tactic & operator=(tactic const &s)
probe(context &c, Z3_probe s)
Z3_ast Z3_API Z3_mk_bvadd(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Standard two's complement addition.
probe & operator=(probe const &s)
func_decl get_const_decl(unsigned i) const
void Z3_API Z3_params_dec_ref(__in Z3_context c, __in Z3_params p)
Decrement the reference counter of the given parameter set.
void Z3_API Z3_apply_result_inc_ref(__in Z3_context c, __in Z3_apply_result r)
Increment the reference counter of the given Z3_apply_result object.
friend expr operator>=(expr const &a, expr const &b)
bool is_array() const
Return true if this is a Array expression.
Z3_tactic Z3_API Z3_mk_tactic(__in Z3_context c, __in Z3_string name)
Return a tactic associated with the given name. The complete list of tactics may be obtained using th...
friend probe operator<(probe const &p1, double p2)
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
Z3_string Z3_API Z3_tactic_get_help(__in Z3_context c, __in Z3_tactic t)
Return a string containing a description of parameters accepted by the given tactic.
Z3_sort Z3_API Z3_get_array_sort_range(__in Z3_context c, __in Z3_sort t)
Return the range of the given array sort.
void set(char const *k, symbol const &s)
std::ostream & operator<<(std::ostream &out, check_result r)
friend expr operator<=(expr const &a, int b)
Z3_sort Z3_API Z3_mk_bv_sort(__in Z3_context c, __in unsigned sz)
Create a bit-vector type of the given size.
friend bool eq(ast const &a, ast const &b)
Return true if the ASTs are structurally identical.
Z3_symbol Z3_API Z3_get_decl_name(__in Z3_context c, __in Z3_func_decl d)
Return the constant declaration name as a symbol.
tactic cond(probe const &p, tactic const &t1, tactic const &t2)
expr bv_val(int n, unsigned sz)
Z3_probe Z3_API Z3_probe_eq(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned ...
void Z3_API Z3_model_inc_ref(__in Z3_context c, __in Z3_model m)
Increment the reference counter of the given model.
bool is_real() const
Return true if this is a real expression.
func_interp & operator=(func_interp const &s)
friend expr operator!=(expr const &a, expr const &b)
Z3_ast Z3_API Z3_mk_numeral(__in Z3_context c, __in Z3_string numeral, __in Z3_sort ty)
Create a numeral of a given sort.
Z3_ast Z3_API Z3_substitute_vars(__in Z3_context c, __in Z3_ast a, __in unsigned num_exprs, __in_ecount(num_exprs) Z3_ast const to[])
Substitute the free variables in a with the expressions in to. For every i smaller than num_exprs...
Z3_tactic Z3_API Z3_tactic_fail_if(__in Z3_context c, __in Z3_probe p)
Return a tactic that fails if the probe p evaluates to false.
unsigned Z3_API Z3_get_app_num_args(__in Z3_context c, __in Z3_app a)
Return the number of argument of an application. If t is an constant, then the number of arguments is...
probe(context &c, double val)
void Z3_API Z3_func_entry_dec_ref(__in Z3_context c, __in Z3_func_entry e)
Decrement the reference counter of the given Z3_func_entry object.
expr select(expr const &a, expr const &i)
Z3_ast Z3_API Z3_mk_bvor(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Bitwise or.
func_entry & operator=(func_entry const &s)
void set(char const *param, char const *value)
Set global parameter param with string value.
Z3_sort Z3_API Z3_mk_enumeration_sort(__in Z3_context c, __in Z3_symbol name, __in unsigned n, __in_ecount(n) Z3_symbol const enum_names[], __out_ecount(n) Z3_func_decl enum_consts[], __out_ecount(n) Z3_func_decl enum_testers[])
Create a enumeration sort.
Z3_ast Z3_API Z3_model_get_const_interp(__in Z3_context c, __in Z3_model m, __in Z3_func_decl a)
Return the interpretation (i.e., assignment) of constant a in the model m. Return NULL...
tactic when(probe const &p, tactic const &t)
friend std::ostream & operator<<(std::ostream &out, params const &p)
void set(char const *k, double n)
Z3_func_decl Z3_API Z3_model_get_func_decl(__in Z3_context c, __in Z3_model m, __in unsigned i)
Return the declaration of the i-th function in the given model.
void Z3_API Z3_solver_dec_ref(__in Z3_context c, __in Z3_solver s)
Decrement the reference counter of the given solver.
void Z3_API Z3_goal_inc_ref(__in Z3_context c, __in Z3_goal g)
Increment the reference counter of the given goal.
friend expr operator/(expr const &a, expr const &b)
void set(char const *param, char const *value)
Update global parameter param with string value.
A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort.
expr simplify() const
Return a simplified version of this expression.
unsigned bv_size() const
Return the size of this Bit-vector sort.
Z3_apply_result Z3_API Z3_tactic_apply(__in Z3_context c, __in Z3_tactic t, __in Z3_goal g)
Apply tactic t to the goal g.
bool is_bv() const
Return true if this sort is a Bit-vector sort.
Z3_ast Z3_API Z3_func_entry_get_value(__in Z3_context c, __in Z3_func_entry e)
Return the value of this point.
friend expr operator^(expr const &a, expr const &b)
Z3_goal_prec Z3_API Z3_goal_precision(__in Z3_context c, __in Z3_goal g)
Return the "precision" of the given goal. Goals can be transformed using over and under approximation...
Z3_model Z3_API Z3_apply_result_convert_model(__in Z3_context c, __in Z3_apply_result r, __in unsigned i, __in Z3_model m)
Convert a model for the subgoal Z3_apply_result_get_subgoal(c, r, i) into a model for the original go...
friend std::ostream & operator<<(std::ostream &out, ast const &n)
sort bv_sort(unsigned sz)
Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz.
void interrupt()
Interrupt the current procedure being executed by any object managed by this context. This is a soft interruption: there is no guarantee the object will actualy stop.
bool is_double(unsigned i) const
expr udiv(expr const &a, expr const &b)
unsigned division operator for bitvectors.
apply_result operator()(goal const &g) const
void Z3_API Z3_params_inc_ref(__in Z3_context c, __in Z3_params p)
Increment the reference counter of the given parameter set.
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Z3_symbol Z3_API Z3_mk_string_symbol(__in Z3_context c, __in Z3_string s)
Create a Z3 symbol using a C string.
Z3_error_code
Z3 error codes (See Z3_get_error_code).
goal(context &c, Z3_goal s)
Z3_sort Z3_API Z3_mk_real_sort(__in Z3_context c)
Create the real type.
expr eval(expr const &n, bool model_completion=false) const
model(context &c, Z3_model m)
sort array_sort(sort d, sort r)
Return an array sort for arrays from d to r.
expr constant(symbol const &name, sort const &s)
friend probe operator>(double p1, probe const &p2)
int Z3_bool
Z3 Boolean type. It is just an alias for int.
Z3_bool Z3_API Z3_goal_inconsistent(__in Z3_context c, __in Z3_goal g)
Return true if the given goal contains the formula false.
Z3_sort Z3_API Z3_get_range(__in Z3_context c, __in Z3_func_decl d)
Return the range of the given declaration.
func_decl operator[](int i) const
System.IntPtr Z3_func_entry
friend probe operator>=(probe const &p1, double p2)
friend expr operator/(expr const &a, int b)
friend expr operator||(bool a, expr const &b)
Return an expression representing a or b. The C++ Boolean value a is automatically converted into a Z...
Z3_ast Z3_API Z3_mk_unsigned_int(__in Z3_context c, __in unsigned v, __in Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
friend expr operator||(expr const &a, expr const &b)
Return an expression representing a or b.
Z3_probe Z3_API Z3_probe_gt(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than the value retur...
bool is_datatype() const
Return true if this is a Datatype expression.
Z3_ast Z3_API Z3_goal_formula(__in Z3_context c, __in Z3_goal g, __in unsigned idx)
Return a formula from the given goal.
sort operator()(context &c, Z3_ast a)
void Z3_API Z3_stats_inc_ref(__in Z3_context c, __in Z3_stats s)
Increment the reference counter of the given statistics object.
Z3_ast Z3_API Z3_mk_sub(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing args[0] - ... - args[num_args - 1].The array args must have num_args ...
friend probe operator||(probe const &p1, probe const &p2)
friend expr operator*(int a, expr const &b)
Z3_ast Z3_API Z3_substitute(__in Z3_context c, __in Z3_ast a, __in unsigned num_exprs, __in_ecount(num_exprs) Z3_ast const from[], __in_ecount(num_exprs) Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs. The result is the new AST. The arrays from and to must have size num_exprs. For every i smaller than num_exprs, we must have that sort of from[i] must be equal to sort of to[i].
Z3_sort Z3_API Z3_mk_array_sort(__in Z3_context c, __in Z3_sort domain, __in Z3_sort range)
Create an array type.
Exception used to sign API usage errors.
unsigned uint_value(unsigned i) const
Z3_bool Z3_API Z3_is_eq_ast(__in Z3_context c, __in Z3_ast t1, Z3_ast t2)
compare terms.
void Z3_API Z3_params_set_symbol(__in Z3_context c, __in Z3_params p, __in Z3_symbol k, __in Z3_symbol v)
Add a symbol parameter k with value v to the parameter set p.
ast_vector_tpl(context &c, Z3_ast_vector v)
A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort ...
expr & operator=(expr const &n)
void Z3_API Z3_model_dec_ref(__in Z3_context c, __in Z3_model m)
Decrement the reference counter of the given model.
unsigned num_exprs() const
Z3_ast Z3_API Z3_mk_gt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create greater than.
bool is_uint(unsigned i) const
expr ule(expr const &a, expr const &b)
unsigned less than or equal to operator for bitvectors.
Z3_ast Z3_API Z3_mk_bvsdiv(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed division.
expr_vector unsat_core() const
void Z3_API Z3_global_param_set(__in Z3_string param_id, __in Z3_string param_value)
Set a global (or module) parameter. This setting is shared by all Z3 contexts.
Z3_func_interp Z3_API Z3_model_get_func_interp(__in Z3_context c, __in Z3_model m, __in Z3_func_decl f)
Return the interpretation of the function f in the model m. Return NULL, if the model does not assign...
Z3_ast Z3_API Z3_mk_bvslt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed less than.
Z3_model Z3_API Z3_solver_get_model(__in Z3_context c, __in Z3_solver s)
Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.
void Z3_API Z3_set_ast_print_mode(__in Z3_context c, __in Z3_ast_print_mode mode)
Select mode for the format used for pretty-printing AST nodes.
void set(char const *param, int value)
Update global parameter param with Integer value.
Z3_string Z3_API Z3_stats_to_string(__in Z3_context c, __in Z3_stats s)
Convert a statistics into a string.
unsigned num_entries() const
Z3_string Z3_API Z3_apply_result_to_string(__in Z3_context c, __in Z3_apply_result r)
Convert the Z3_apply_result object returned by Z3_tactic_apply into a string.
void Z3_API Z3_goal_reset(__in Z3_context c, __in Z3_goal g)
Erase all formulas from the given goal.
Z3_ast Z3_API Z3_mk_true(__in Z3_context c)
Create an AST node representing true.
bool is_finite_domain() const
Return true if this sort is a Finite domain sort.
friend probe operator>(probe const &p1, double p2)
void Z3_API Z3_apply_result_dec_ref(__in Z3_context c, __in Z3_apply_result r)
Decrement the reference counter of the given Z3_apply_result object.
func_decl operator()(context &c, Z3_ast a)
ast_vector_tpl< func_decl > func_decl_vector
Z3_tactic Z3_API Z3_tactic_repeat(__in Z3_context c, __in Z3_tactic t, unsigned max)
Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of...
Z3_ast_kind Z3_API Z3_get_ast_kind(__in Z3_context c, __in Z3_ast a)
Return the kind of the given AST.
void Z3_API Z3_goal_assert(__in Z3_context c, __in Z3_goal g, __in Z3_ast a)
Add a new formula a to the given goal.
expr pw(expr const &a, expr const &b)
friend std::ostream & operator<<(std::ostream &out, goal const &g)
friend probe operator>=(probe const &p1, probe const &p2)
expr(context &c, Z3_ast n)
friend expr operator^(expr const &a, int b)
expr operator[](int i) const
friend expr operator-(expr const &a, expr const &b)
Z3_bool Z3_API Z3_stats_is_double(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return Z3_TRUE if the given statistical data is a double.
friend expr operator-(expr const &a)
friend expr distinct(expr_vector const &args)
check_result check(unsigned n, expr *const assumptions)
Z3_goal Z3_API Z3_apply_result_get_subgoal(__in Z3_context c, __in Z3_apply_result r, __in unsigned i)
Return one of the subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
check_result check(expr_vector assumptions)
friend expr operator*(expr const &a, int b)
friend expr operator&(expr const &a, int b)
friend expr operator*(expr const &a, expr const &b)
probe(context &c, char const *name)
friend std::ostream & operator<<(std::ostream &out, solver const &s)
Z3_decl_kind Z3_API Z3_get_decl_kind(__in Z3_context c, __in Z3_func_decl d)
Return declaration kind corresponding to declaration.
Z3_tactic Z3_API Z3_tactic_try_for(__in Z3_context c, __in Z3_tactic t, __in unsigned ms)
Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms mil...
friend expr operator<=(expr const &a, expr const &b)
Z3_ast Z3_API Z3_get_quantifier_body(__in Z3_context c, __in Z3_ast a)
Return body of quantifier.
expr get_const_interp(func_decl c) const
void Z3_API Z3_solver_inc_ref(__in Z3_context c, __in Z3_solver s)
Increment the reference counter of the given solver.
A Context manages all other Z3 objects, global configuration options, etc.
Z3_tactic Z3_API Z3_tactic_using_params(__in Z3_context c, __in Z3_tactic t, __in Z3_params p)
Return a tactic that applies t using the given set of parameters.
Z3_ast Z3_API Z3_mk_ge(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create greater than or equal to.
friend tactic operator|(tactic const &t1, tactic const &t2)
void Z3_API Z3_dec_ref(__in Z3_context c, __in Z3_ast a)
Decrement the reference counter of the given AST. The context c should have been created using Z3_mk_...
Z3_ast Z3_API Z3_mk_int(__in Z3_context c, __in int v, __in Z3_sort ty)
Create a numeral of an int, bit-vector, or finite-domain sort.
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...
friend expr operator&(int a, expr const &b)
Z3_tactic Z3_API Z3_tactic_and_then(__in Z3_context c, __in Z3_tactic t1, __in Z3_tactic t2)
Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1...
Z3_ast Z3_API Z3_mk_bvult(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Unsigned less than.
solver(context &c, Z3_solver s)
Z3 global configuration object.
solver & operator=(solver const &s)
void set(char const *param, int value)
Set global parameter param with integer value.
Z3_ast Z3_API Z3_simplify(__in Z3_context c, __in Z3_ast a)
Interface to simplifier.
expr substitute(expr_vector const &src, expr_vector const &dst)
Apply substitution. Replace src expressions by dst.
ast(context &c, Z3_ast n)
ast_vector_tpl & operator=(ast_vector_tpl const &s)
void Z3_API Z3_params_set_uint(__in Z3_context c, __in Z3_params p, __in Z3_symbol k, __in unsigned v)
Add a unsigned parameter k with value v to the parameter set p.
friend std::ostream & operator<<(std::ostream &out, apply_result const &r)
Z3_ast_vector Z3_API Z3_solver_get_unsat_core(__in Z3_context c, __in Z3_solver s)
Retrieve the unsat core for the last Z3_solver_check_assumptions The unsat core is a subset of the as...
bool is_finite_domain() const
Return true if this is a Finite-domain expression.
expr bv_const(char const *name, unsigned sz)
Z3_func_entry Z3_API Z3_func_interp_get_entry(__in Z3_context c, __in Z3_func_interp f, unsigned i)
Return a "point" of the given function intepretation. It represents the value of f in a particular po...
tactic(context &c, char const *name)
Z3_solver Z3_API Z3_mk_solver_for_logic(__in Z3_context c, __in Z3_symbol logic)
Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unkn...
Z3_bool Z3_API Z3_model_eval(__in Z3_context c, __in Z3_model m, __in Z3_ast t, __in Z3_bool model_completion, __out Z3_ast *v)
Evaluate the AST node t in the given model. Return Z3_TRUE if succeeded, and store the result in v...
void Z3_API Z3_probe_inc_ref(__in Z3_context c, __in Z3_probe p)
Increment the reference counter of the given probe.
Z3_ast Z3_API Z3_mk_bvmul(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Standard two's complement multiplication.
tactic with(tactic const &t, params const &p)
System.IntPtr Z3_func_decl
friend expr operator<=(int a, expr const &b)
Z3_probe Z3_API Z3_probe_not(__in Z3_context x, __in Z3_probe p)
Return a probe that evaluates to "true" when p does not evaluate to true.
unsigned Z3_API Z3_stats_size(__in Z3_context c, __in Z3_stats s)
Return the number of statistical data in s.
void Z3_API Z3_solver_assert(__in Z3_context c, __in Z3_solver s, __in Z3_ast a)
Assert a constraint into the solver.
Z3_symbol_kind Z3_API Z3_get_symbol_kind(__in Z3_context c, __in Z3_symbol s)
Return Z3_INT_SYMBOL if the symbol was constructed using Z3_mk_int_symbol, and Z3_STRING_SYMBOL if th...
unsigned Z3_API Z3_func_interp_get_num_entries(__in Z3_context c, __in Z3_func_interp f)
Return the number of entries in the given function interpretation.
sort array_domain() const
Return the domain of this Array sort.
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
BEGIN_MLAPI_EXCLUDE Z3_string Z3_API Z3_get_error_msg_ex(__in Z3_context c, __in Z3_error_code err)
Return a string describing the given error code.
func_entry(context &c, Z3_func_entry e)
Z3_string Z3_API Z3_goal_to_string(__in Z3_context c, __in Z3_goal g)
Convert a goal into a string.
bool is_var() const
Return true if this expression is a variable.
void add(expr const &e, char const *p)
func_decl to_func_decl(context &c, Z3_func_decl f)
Z3_ast Z3_API Z3_mk_bvnot(__in Z3_context c, __in Z3_ast t1)
Bitwise negation.
sort array_range() const
Return the range of this Array sort.
double Z3_API Z3_stats_get_double_value(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return the double value of the given statistical data.
Z3_ast Z3_API Z3_mk_false(__in Z3_context c)
Create an AST node representing false.
Z3_string Z3_API Z3_params_to_string(__in Z3_context c, __in 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_ast_vector_push(__in Z3_context c, __in Z3_ast_vector v, __in Z3_ast a)
Add the AST a in the end of the AST vector v. The size of v is increased by one.
void Z3_API Z3_solver_push(__in Z3_context c, __in Z3_solver s)
Create a backtracking point.
unsigned Z3_API Z3_goal_num_exprs(__in Z3_context c, __in Z3_goal g)
Return the number of formulas, subformulas and terms in the given goal.
Z3_ast Z3_API Z3_mk_ite(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2, __in Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
Z3_sort Z3_API Z3_get_array_sort_domain(__in Z3_context c, __in Z3_sort t)
Return the domain of the given array sort.
void Z3_API Z3_goal_dec_ref(__in Z3_context c, __in Z3_goal g)
Decrement the reference counter of the given goal.
func_decl get_func_decl(unsigned i) const
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
expr operator()(context &c, Z3_ast a)
friend probe operator!(probe const &p)
bool is_numeral() const
Return true if this expression is a numeral.
Z3_tactic Z3_API Z3_tactic_cond(__in Z3_context c, __in Z3_probe p, __in Z3_tactic t1, __in 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...
unsigned Z3_API Z3_model_get_num_funcs(__in Z3_context c, __in Z3_model m)
Return the number of function interpretations in the given model.
exception(char const *msg)
Z3_ast Z3_API Z3_mk_implies(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create an AST node representing t1 implies t2.
Z3_lbool
Lifted Boolean type: false, undefined, true.
friend expr operator!=(expr const &a, int b)
Z3_ast Z3_API Z3_mk_bvugt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Unsigned greater than.
Z3_string Z3_API Z3_stats_get_key(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return the key (a string) for a particular statistical data.
void Z3_API Z3_func_interp_inc_ref(__in Z3_context c, __in Z3_func_interp f)
Increment the reference counter of the given Z3_func_interp object.
expr real_val(int n, int d)
ast_vector_tpl< sort > sort_vector
Z3_ast Z3_API Z3_mk_and(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].The array args must have num_arg...
unsigned Z3_API Z3_get_arity(__in Z3_context c, __in Z3_func_decl d)
Alias for Z3_get_domain_size.
int Z3_API Z3_get_symbol_int(__in Z3_context c, __in Z3_symbol s)
Return the symbol int value.
Z3_ast Z3_API Z3_mk_select(__in Z3_context c, __in Z3_ast a, __in Z3_ast i)
Array read. The argument a is the array and i is the index of the array that gets read...
Z3_ast Z3_API Z3_mk_bvsle(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed less than or equal to.
func_interp(func_interp const &s)
Z3_decl_kind decl_kind() const
model & operator=(model const &s)
friend expr operator-(int a, expr const &b)
Z3_ast Z3_API Z3_mk_lt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create less than.
Z3_func_decl Z3_API Z3_model_get_const_decl(__in Z3_context c, __in Z3_model m, __in unsigned i)
Return the i-th constant in the given model.
unsigned Z3_API Z3_get_ast_hash(__in Z3_context c, __in Z3_ast a)
Return a hash code for the given AST.
friend expr operator==(expr const &a, expr const &b)
void set(char const *param, bool value)
Set global parameter param with Boolean value.
func_entry entry(unsigned i) const
bool is_relation() const
Return true if this is a Relation expression.
bool is_bool() const
Return true if this sort is the Boolean sort.
expr ugt(expr const &a, expr const &b)
unsigned greater than operator for bitvectors.
goal & operator=(goal const &s)
Z3_ast Z3_API Z3_mk_bvsub(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Standard two's complement subtraction.
expr const_array(sort const &d, expr const &v)
void Z3_API Z3_params_set_double(__in Z3_context c, __in Z3_params p, __in Z3_symbol k, __in double v)
Add a double parameter k with value v to the parameter set p.
Z3_ast Z3_API Z3_mk_int2real(__in Z3_context c, __in Z3_ast t1)
Coerce an integer to a real.
Z3_string Z3_API Z3_ast_to_string(__in Z3_context c, __in Z3_ast a)
Convert the given AST node into a string.
friend std::ostream & operator<<(std::ostream &out, model const &m)
Z3_ast Z3_API Z3_solver_get_proof(__in Z3_context c, __in Z3_solver s)
Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.
goal operator[](int i) const
Z3_probe Z3_API Z3_probe_const(__in Z3_context x, __in double val)
Return a probe that always evaluates to val.
friend expr operator<(expr const &a, int b)
friend probe operator==(probe const &p1, double p2)
Z3_sort Z3_API Z3_mk_int_sort(__in Z3_context c)
Create the integer type.
friend expr operator<(int a, expr const &b)
Z3_ast Z3_API Z3_mk_bvand(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Bitwise and.
void set_param(char const *param, char const *value)
friend void check_context(object const &a, object const &b)
void Z3_API Z3_del_context(__in Z3_context c)
Delete the given logical context.
void Z3_API Z3_set_error_handler(__in Z3_context c, __in Z3_error_handler h)
Register a Z3 error handler.
Z3_bool Z3_API Z3_goal_is_decided_sat(__in Z3_context c, __in Z3_goal g)
Return true if the goal is empty, and it is precise or the product of a under approximation.
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Z3_ast Z3_API Z3_mk_bvuge(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Unsigned greater than or equal to.
friend probe operator<=(probe const &p1, probe const &p2)
friend expr operator&&(expr const &a, expr const &b)
Return an expression representing a and b.
expr int_const(char const *name)
friend expr operator&(expr const &a, expr const &b)
friend std::ostream & operator<<(std::ostream &out, exception const &e)
expr arg(unsigned i) const
void Z3_API Z3_solver_set_params(__in Z3_context c, __in Z3_solver s, __in Z3_params p)
Set the given solver using the given parameters.
Z3_stats Z3_API Z3_solver_get_statistics(__in Z3_context c, __in Z3_solver s)
Return statistics for the given solver.
unsigned num_args() const
Return the number of arguments in this application. This method assumes the expression is an applicat...
Z3_symbol_kind
The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See Z3_...
friend expr operator&&(expr const &a, bool b)
Return an expression representing a and b. The C++ Boolean value b is automatically converted into a ...
Z3_probe Z3_API Z3_probe_ge(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than or equal to the...
unsigned Z3_API Z3_model_get_num_consts(__in Z3_context c, __in Z3_model m)
Return the number of constants assigned by the given model.
Z3_ast Z3_API Z3_mk_not(__in Z3_context c, __in Z3_ast a)
Create an AST node representing not(a).
Z3_ast Z3_API Z3_mk_bvsge(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed greater than or equal to.
goal(context &c, bool models=true, bool unsat_cores=false, bool proofs=false)
void Z3_API Z3_del_config(__in Z3_config c)
Delete the given configuration object.
System.IntPtr Z3_apply_result
bool is_app() const
Return true if this expression is an application.
friend tactic operator&(tactic const &t1, tactic const &t2)
friend expr operator>(expr const &a, expr const &b)
Z3_bool Z3_API Z3_stats_is_uint(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return Z3_TRUE if the given statistical data is a unsigned integer.
Z3_ast Z3_API Z3_mk_div(__in Z3_context c, __in Z3_ast arg1, __in Z3_ast arg2)
Create an AST node representing arg1 div arg2.The arguments must either both have int type or both ha...
Z3_symbol_kind kind() const
Z3_ast Z3_API Z3_mk_bvneg(__in Z3_context c, __in Z3_ast t1)
Standard two's complement unary minus.
Z3_ast Z3_API Z3_mk_unary_minus(__in Z3_context c, __in Z3_ast arg)
Create an AST node representing -arg.The arguments must have int or real type.
Z3_sort Z3_API Z3_get_sort(__in Z3_context c, __in Z3_ast a)
Return the sort of an AST node.
friend tactic with(tactic const &t, params const &p)
Z3_ast Z3_API Z3_func_entry_get_arg(__in Z3_context c, __in Z3_func_entry e, __in unsigned i)
Return an argument of a Z3_func_entry object.
friend expr operator!=(int a, expr const &b)
Z3_string Z3_API Z3_model_to_string(__in Z3_context c, __in Z3_model m)
Convert the given model into a string.
expr real_const(char const *name)
friend probe operator<=(double p1, probe const &p2)
friend expr operator/(int a, expr const &b)
friend expr operator>(int a, expr const &b)
func_interp get_func_interp(func_decl f) const
void Z3_API Z3_func_entry_inc_ref(__in Z3_context c, __in Z3_func_entry e)
Increment the reference counter of the given Z3_func_entry object.
friend probe operator==(probe const &p1, probe const &p2)
Z3_func_decl Z3_API Z3_get_app_decl(__in Z3_context c, __in Z3_app a)
Return the declaration of a constant or function application.
friend probe operator>=(double p1, probe const &p2)
void Z3_API Z3_solver_reset(__in Z3_context c, __in Z3_solver s)
Remove all assertions from the solver.
Z3_solver Z3_API Z3_mk_solver(__in Z3_context c)
Create a new (incremental) solver. This solver also uses a set of builtin tactics for handling the fi...
Z3_sort_kind sort_kind() const
Return the internal sort kind.
bool is_arith() const
Return true if this sort is the Integer or Real sort.
unsigned Z3_API Z3_goal_size(__in Z3_context c, __in Z3_goal g)
Return the number of formulas in the given goal.
Z3_ast Z3_API Z3_func_interp_get_else(__in Z3_context c, __in Z3_func_interp f)
Return the 'else' value of the given function interpretation.
Z3_probe Z3_API Z3_probe_or(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when p1 or p2 evaluates to true.
Z3_ast Z3_API Z3_mk_bvsgt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed greater than.
model convert_model(model const &m, unsigned i=0) const
bool is_well_sorted() const
Return true if this expression is well sorted (aka type correct).
unsigned Z3_API Z3_ast_vector_size(__in Z3_context c, __in Z3_ast_vector v)
Return the size of the given AST vector.
Z3_sort Z3_API Z3_get_domain(__in Z3_context c, __in Z3_func_decl d, __in unsigned i)
Return the sort of the i-th parameter of the given function declaration.
Z3_config Z3_API Z3_mk_config(void)
Create a configuration object for the Z3 context object.
void Z3_API Z3_tactic_dec_ref(__in Z3_context c, __in Z3_tactic g)
Decrement the reference counter of the given tactic.
Z3_bool Z3_API Z3_goal_is_decided_unsat(__in Z3_context c, __in Z3_goal g)
Return true if the goal contains false, and it is precise or the product of an over approximation...
symbol & operator=(symbol const &s)
sort real_sort()
Return the Real sort.
friend std::ostream & operator<<(std::ostream &out, ast_vector_tpl const &v)
bool inconsistent() const
bool is_const() const
Return true if this expression is a constant (i.e., an application with 0 arguments).
expr arg(unsigned i) const
Return the i-th argument of this application. This method assumes the expression is an application...
ast_vector_tpl(ast_vector_tpl const &s)
Z3_ast Z3_API Z3_mk_distinct(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).The distinct construct is us...
expr num_val(int n, sort const &s)
Z3_ast Z3_API Z3_mk_bvudiv(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Unsigned division.
Z3_ast Z3_API Z3_mk_or(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].The array args must have num_args ...
bool eq(ast const &a, ast const &b)
unsigned num_consts() const
symbol int_symbol(int n)
Create a Z3 symbol based on the given integer.
Z3_ast Z3_API Z3_mk_exists_const(__in Z3_context c, unsigned weight, unsigned num_bound, __in_ecount(num_bound) Z3_app const bound[], unsigned num_patterns, __in_ecount(num_patterns) Z3_pattern const patterns[], __in Z3_ast body)
Similar to Z3_mk_forall_const.
void Z3_API Z3_ast_vector_inc_ref(__in Z3_context c, __in Z3_ast_vector v)
Increment the reference counter of the given AST vector.
friend probe operator>(probe const &p1, probe const &p2)
void Z3_API Z3_interrupt(__in Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers...
friend probe operator<(double p1, probe const &p2)
unsigned num_funcs() const
unsigned Z3_API Z3_func_entry_get_num_args(__in Z3_context c, __in Z3_func_entry e)
Return the number of arguments in a Z3_func_entry object.
friend probe operator==(double p1, probe const &p2)
check_result to_check_result(Z3_lbool l)
friend expr operator~(expr const &a)
Z3_tactic Z3_API Z3_tactic_when(__in Z3_context c, __in Z3_probe p, __in 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...
friend tactic repeat(tactic const &t, unsigned max)
T operator[](int i) const
Z3_ast Z3_API Z3_ast_vector_get(__in Z3_context c, __in Z3_ast_vector v, __in unsigned i)
Return the AST at position i in the AST vector v.
tactic(context &c, Z3_tactic s)
void check_context(object const &a, object const &b)
Z3_probe Z3_API Z3_probe_le(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the va...
expr bool_const(char const *name)
double apply(goal const &g) const
void Z3_API Z3_func_interp_dec_ref(__in Z3_context c, __in Z3_func_interp f)
Decrement the reference counter of the given Z3_func_interp object.
Z3_solver Z3_API Z3_mk_solver_from_tactic(__in Z3_context c, __in Z3_tactic t)
Create a new solver that is implemented using the given tactic. The solver supports the commands Z3_s...
friend expr ite(expr const &c, expr const &t, expr const &e)
Create the if-then-else expression ite(c, t, e)
params & operator=(params const &s)
Z3_ast Z3_API Z3_mk_bvxor(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Bitwise exclusive-or.
Z3_string Z3_API Z3_ast_vector_to_string(__in Z3_context c, __in Z3_ast_vector v)
Convert AST vector into a string.
friend std::ostream & operator<<(std::ostream &out, symbol const &s)
Z3_ast_vector Z3_API Z3_solver_get_assertions(__in Z3_context c, __in Z3_solver s)
Return the set of asserted formulas as a goal object.
friend expr operator>(expr const &a, int b)
friend expr operator<(expr const &a, expr const &b)
friend expr operator!(expr const &a)
Return an expression representing not(a).
Z3_goal_prec precision() const
Z3_probe Z3_API Z3_probe_lt(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned...
func_decl(context &c, Z3_func_decl n)
ast_vector_tpl< ast > ast_vector
bool is_decided_unsat() const
friend probe operator<(probe const &p1, probe const &p2)
friend expr operator==(expr const &a, int b)
expr_vector assertions() const
unsigned Z3_API Z3_goal_depth(__in Z3_context c, __in Z3_goal g)
Return the depth of the given goal. It tracks how many transformations were applied to it...
sort get_sort() const
Return the sort of this expression.
Z3_ast Z3_API Z3_mk_int64(__in Z3_context c, __in __int64 v, __in Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
friend probe operator&&(probe const &p1, probe const &p2)
void add(expr const &e, expr const &p)
expr store(expr const &a, expr const &i, expr const &v)
void Z3_API Z3_params_set_bool(__in Z3_context c, __in Z3_params p, __in Z3_symbol k, __in Z3_bool v)
Add a Boolean parameter k with value v to the parameter set p.
void set(char const *k, unsigned n)
void check_error() const
Auxiliary method used to check for API usage errors.
Z3_string Z3_API Z3_get_symbol_string(__in Z3_context c, __in Z3_symbol s)
Return the symbol name.
std::string key(unsigned i) const
void Z3_API Z3_probe_dec_ref(__in Z3_context c, __in Z3_probe p)
Decrement the reference counter of the given probe.
bool is_relation() const
Return true if this sort is a Relation sort.
Z3_ast Z3_API Z3_mk_eq(__in Z3_context c, __in Z3_ast l, __in Z3_ast r)
Create an AST node representing l = r.
void set(char const *k, bool b)
tactic repeat(tactic const &t, unsigned max=UINT_MAX)
Z3_ast Z3_API Z3_mk_unsigned_int64(__in Z3_context c, __in unsigned __int64 v, __in Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
expr ult(expr const &a, expr const &b)
unsigned less than operator for bitvectors.
friend expr operator&&(bool a, expr const &b)
Return an expression representing a and b. The C++ Boolean value a is automatically converted into a ...
Z3_ast Z3_API Z3_mk_store(__in Z3_context c, __in Z3_ast a, __in Z3_ast i, __in Z3_ast v)
Array update.
unsigned Z3_API Z3_get_bv_sort_size(__in Z3_context c, __in Z3_sort t)
Return the size of the given bit-vector sort.
bool is_int() const
Return true if this is an integer expression.
apply_result apply(goal const &g) const
bool is_arith() const
Return true if this is an integer or real expression.
void Z3_API Z3_global_param_reset_all(void)
Restore the value of all global (and module) parameters. This command will not affect already created...
func_decl(func_decl const &s)
friend expr operator||(expr const &a, bool b)
Return an expression representing a or b. The C++ Boolean value b is automatically converted into a Z...
Z3_sort_kind Z3_API Z3_get_sort_kind(__in Z3_context c, __in Z3_sort t)
Return the sort kind (e.g., array, tuple, int, bool, etc).
tactic fail_if(probe const &p)
stats(context &c, Z3_stats e)
expr exists(expr const &x, expr const &b)
ast operator()(context &c, Z3_ast a)
void Z3_API Z3_ast_vector_dec_ref(__in Z3_context c, __in Z3_ast_vector v)
Decrement the reference counter of the given AST vector.
bool is_array() const
Return true if this sort is a Array sort.
Z3_ast Z3_API Z3_mk_app(__in Z3_context c, __in Z3_func_decl d, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create a constant or function application.
friend expr operator-(expr const &a, int b)
Z3_func_decl Z3_API Z3_mk_func_decl(__in Z3_context c, __in Z3_symbol s, __in unsigned domain_size, __in_ecount(domain_size) Z3_sort const domain[], __in Z3_sort range)
Declare a constant or function.
expr ite(expr const &c, expr const &t, expr const &e)
Create the if-then-else expression ite(c, t, e)
T const & operator[](int i) const
func_entry(func_entry const &s)
double double_value(unsigned i) const
expr body() const
Return the 'body' of this quantifier.
#define Z3_FALSE
False value. It is just an alias for 0.
ast & operator=(ast const &s)
void Z3_API Z3_stats_dec_ref(__in Z3_context c, __in Z3_stats s)
Decrement the reference counter of the given statistics object.
void Z3_API Z3_update_param_value(__in Z3_context c, __in Z3_string param_id, __in Z3_string param_value)
Set a value of a context parameter.
bool is_bv() const
Return true if this is a Bit-vector expression.
expr forall(expr const &x, expr const &b)
sort domain(unsigned i) const
bool is_bool() const
Return true if this is a Boolean expression.
sort(context &c, Z3_sort s)
double operator()(goal const &g) const
bool is_datatype() const
Return true if this sort is a Datatype sort.
void Z3_API Z3_solver_pop(__in Z3_context c, __in Z3_solver s, unsigned n)
Backtrack n backtracking points.
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...
friend expr operator+(int a, expr const &b)
symbol(context &c, Z3_symbol s)
solver(context &c, char const *logic)
tactic try_for(tactic const &t, unsigned ms)
func_interp(context &c, Z3_func_interp e)
Z3_params Z3_API Z3_mk_params(__in Z3_context c)
Create a Z3 (empty) parameter set. Starting at Z3 4.0, parameter sets are used to configure many comp...
friend tactic try_for(tactic const &t, unsigned ms)
void push_back(T const &e)
System.IntPtr Z3_ast_vector
Z3_tactic Z3_API Z3_tactic_or_else(__in Z3_context c, __in Z3_tactic t1, __in Z3_tactic t2)
Return a tactic that first applies t1 to a given goal, if it fails then returns the result of t2 appl...
ast_vector_tpl< expr > expr_vector
Z3_error_code Z3_API Z3_get_error_code(__in Z3_context c)
Return the error code for the last API call.
expr uge(expr const &a, expr const &b)
unsigned greater than or equal to operator for bitvectors.
expr implies(expr const &a, bool b)
void set(char const *param, bool value)
Update global parameter param with Boolean value.
void set(params const &p)
friend expr operator+(expr const &a, int b)
Z3_symbol Z3_API Z3_mk_int_symbol(__in Z3_context c, __in int i)
Create a Z3 symbol using an integer.
sort & operator=(sort const &s)
Return true if this sort and s are equal.
bool is_quantifier() const
Return true if this expression is a quantifier.
friend probe operator<=(probe const &p1, double p2)
Z3_lbool Z3_API Z3_solver_check_assumptions(__in Z3_context c, __in Z3_solver s, __in unsigned num_assumptions, __in_ecount(num_assumptions) Z3_ast const assumptions[])
Check whether the assertions in the given solver and optional assumptions are consistent or not...
friend expr operator|(expr const &a, int b)
Z3_ast Z3_API Z3_mk_add(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].The array args must have num_args el...
Z3_ast Z3_API Z3_get_app_arg(__in Z3_context c, __in Z3_app a, __in unsigned i)
Return the i-th argument of the given application.
friend std::ostream & operator<<(std::ostream &out, stats const &s)
void Z3_API Z3_set_param_value(__in Z3_config c, __in Z3_string param_id, __in Z3_string param_value)
Set a configuration parameter.
expr to_real(expr const &a)
Z3_probe Z3_API Z3_mk_probe(__in Z3_context c, __in Z3_string name)
Return a probe associated with the given name. The complete list of probes may be obtained using the ...
friend expr operator>=(int a, expr const &b)
friend expr implies(expr const &a, expr const &b)
Z3_probe Z3_API Z3_probe_and(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when p1 and p2 evaluates to true.
void Z3_API Z3_tactic_inc_ref(__in Z3_context c, __in Z3_tactic t)
Increment the reference counter of the given tactic.
Z3_ast Z3_API Z3_mk_const_array(__in Z3_context c, __in Z3_sort domain, __in Z3_ast v)
Create the constant array.
Z3_ast Z3_API Z3_mk_le(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create less than or equal to.
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...
friend expr operator==(int a, expr const &b)
friend expr operator|(int a, expr const &b)
Z3_decl_kind
The different kinds of interpreted function kinds.
apply_result(context &c, Z3_apply_result s)
double Z3_API Z3_probe_apply(__in Z3_context c, __in Z3_probe p, __in Z3_goal g)
Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0...
Z3_ast Z3_API Z3_simplify_ex(__in Z3_context c, __in Z3_ast a, __in Z3_params p)
Interface to simplifier.
friend expr operator^(int a, expr const &b)
Function declaration (aka function definition). It is the signature of interpreted and uninterpreted ...
unsigned Z3_API Z3_apply_result_get_num_subgoals(__in Z3_context c, __in Z3_apply_result r)
Return the number of subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
sort int_sort()
Return the integer sort.
stats & operator=(stats const &s)
unsigned num_args() const
func_decl & operator=(func_decl const &s)
apply_result & operator=(apply_result const &s)
unsigned Z3_API Z3_stats_get_uint_value(__in Z3_context c, __in Z3_stats s, __in unsigned idx)
Return the unsigned value of the given statistical data.
System.IntPtr Z3_func_interp
void Z3_API Z3_ast_vector_resize(__in Z3_context c, __in Z3_ast_vector v, __in unsigned n)
Resize the AST vector v.
Z3_ast_vector Z3_API Z3_mk_ast_vector(__in Z3_context c)
Return an empty AST vector.
bool is_real() const
Return true if this sort is the Real sort.
sort to_sort(context &c, Z3_sort s)
Z3_goal Z3_API Z3_mk_goal(__in Z3_context c, __in Z3_bool models, __in Z3_bool unsat_cores, __in Z3_bool proofs)
Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or trans...
bool is_decided_sat() const
Z3_ast Z3_API Z3_mk_real(__in Z3_context c, __in int num, __in int den)
Create a real from a fraction.
Z3_string Z3_API Z3_solver_get_reason_unknown(__in Z3_context c, __in Z3_solver s)
Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the commands Z3_solver_ch...
const char * Z3_string
Z3 string type. It is just an alias for const char *.
apply_result(apply_result const &s)