diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c
index 07fc05b21..0c6e2fae4 100644
--- a/examples/c/test_capi.c
+++ b/examples/c/test_capi.c
@@ -19,7 +19,7 @@ Copyright (c) 2015 Microsoft Corporation
#define LOG_MSG(msg) ((void)0)
#endif
-/**
+/**
\defgroup capi_ex C API examples
*/
/*@{*/
@@ -31,7 +31,7 @@ Copyright (c) 2015 Microsoft Corporation
/**
\brief exit gracefully in case of error.
*/
-void exitf(const char* message)
+void exitf(const char* message)
{
fprintf(stderr,"BUG: %s.\n", message);
exit(1);
@@ -40,7 +40,7 @@ void exitf(const char* message)
/**
\brief exit if unreachable code was reached.
*/
-void unreachable()
+void unreachable()
{
exitf("unreachable code was reached");
}
@@ -48,7 +48,7 @@ void unreachable()
/**
\brief Simpler error handler.
*/
-void error_handler(Z3_context c, Z3_error_code e)
+void error_handler(Z3_context c, Z3_error_code e)
{
printf("Error code: %d\n", e);
exitf("incorrect use of Z3");
@@ -56,34 +56,34 @@ void error_handler(Z3_context c, Z3_error_code e)
static jmp_buf g_catch_buffer;
/**
- \brief Low tech exceptions.
-
+ \brief Low tech exceptions.
+
In high-level programming languages, an error handler can throw an exception.
*/
-void throw_z3_error(Z3_context c, Z3_error_code e)
+void throw_z3_error(Z3_context c, Z3_error_code e)
{
longjmp(g_catch_buffer, e);
}
/**
- \brief Create a logical context.
+ \brief Create a logical context.
Enable model construction. Other configuration parameters can be passed in the cfg variable.
Also enable tracing to stderr and register custom error handler.
*/
-Z3_context mk_context_custom(Z3_config cfg, Z3_error_handler err)
+Z3_context mk_context_custom(Z3_config cfg, Z3_error_handler err)
{
Z3_context ctx;
-
+
Z3_set_param_value(cfg, "model", "true");
ctx = Z3_mk_context(cfg);
Z3_set_error_handler(ctx, err);
-
+
return ctx;
}
-Z3_solver mk_solver(Z3_context ctx)
+Z3_solver mk_solver(Z3_context ctx)
{
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
@@ -102,7 +102,7 @@ void del_solver(Z3_context ctx, Z3_solver s)
Also enable tracing to stderr and register standard error handler.
*/
-Z3_context mk_context()
+Z3_context mk_context()
{
Z3_config cfg;
Z3_context ctx;
@@ -132,7 +132,7 @@ Z3_context mk_proof_context() {
/**
\brief Create a variable using the given name and type.
*/
-Z3_ast mk_var(Z3_context ctx, const char * name, Z3_sort ty)
+Z3_ast mk_var(Z3_context ctx, const char * name, Z3_sort ty)
{
Z3_symbol s = Z3_mk_string_symbol(ctx, name);
return Z3_mk_const(ctx, s, ty);
@@ -141,7 +141,7 @@ Z3_ast mk_var(Z3_context ctx, const char * name, Z3_sort ty)
/**
\brief Create a boolean variable using the given name.
*/
-Z3_ast mk_bool_var(Z3_context ctx, const char * name)
+Z3_ast mk_bool_var(Z3_context ctx, const char * name)
{
Z3_sort ty = Z3_mk_bool_sort(ctx);
return mk_var(ctx, name, ty);
@@ -150,16 +150,16 @@ Z3_ast mk_bool_var(Z3_context ctx, const char * name)
/**
\brief Create an integer variable using the given name.
*/
-Z3_ast mk_int_var(Z3_context ctx, const char * name)
+Z3_ast mk_int_var(Z3_context ctx, const char * name)
{
Z3_sort ty = Z3_mk_int_sort(ctx);
return mk_var(ctx, name, ty);
}
/**
- \brief Create a Z3 integer node using a C int.
+ \brief Create a Z3 integer node using a C int.
*/
-Z3_ast mk_int(Z3_context ctx, int v)
+Z3_ast mk_int(Z3_context ctx, int v)
{
Z3_sort ty = Z3_mk_int_sort(ctx);
return Z3_mk_int(ctx, v, ty);
@@ -168,7 +168,7 @@ Z3_ast mk_int(Z3_context ctx, int v)
/**
\brief Create a real variable using the given name.
*/
-Z3_ast mk_real_var(Z3_context ctx, const char * name)
+Z3_ast mk_real_var(Z3_context ctx, const char * name)
{
Z3_sort ty = Z3_mk_real_sort(ctx);
return mk_var(ctx, name, ty);
@@ -177,7 +177,7 @@ Z3_ast mk_real_var(Z3_context ctx, const char * name)
/**
\brief Create the unary function application: (f x).
*/
-Z3_ast mk_unary_app(Z3_context ctx, Z3_func_decl f, Z3_ast x)
+Z3_ast mk_unary_app(Z3_context ctx, Z3_func_decl f, Z3_ast x)
{
Z3_ast args[1] = {x};
return Z3_mk_app(ctx, f, 1, args);
@@ -186,7 +186,7 @@ Z3_ast mk_unary_app(Z3_context ctx, Z3_func_decl f, Z3_ast x)
/**
\brief Create the binary function application: (f x y).
*/
-Z3_ast mk_binary_app(Z3_context ctx, Z3_func_decl f, Z3_ast x, Z3_ast y)
+Z3_ast mk_binary_app(Z3_context ctx, Z3_func_decl f, Z3_ast x, Z3_ast y)
{
Z3_ast args[2] = {x, y};
return Z3_mk_app(ctx, f, 2, args);
@@ -205,7 +205,7 @@ void check(Z3_context ctx, Z3_solver s, Z3_lbool expected_result)
printf("unsat\n");
break;
case Z3_L_UNDEF:
- printf("unknown\n");
+ printf("unknown\n");
m = Z3_solver_get_model(ctx, s);
if (m) Z3_model_inc_ref(ctx, m);
printf("potential model:\n%s\n", Z3_model_to_string(ctx, m));
@@ -226,7 +226,7 @@ void check(Z3_context ctx, Z3_solver s, Z3_lbool expected_result)
\brief Prove that the constraints already asserted into the logical
context implies the given formula. The result of the proof is
displayed.
-
+
Z3 is a satisfiability checker. So, one can prove \c f by showing
that (not f) is unsatisfiable.
@@ -242,7 +242,7 @@ void prove(Z3_context ctx, Z3_solver s, Z3_ast f, Z3_bool is_valid)
not_f = Z3_mk_not(ctx, f);
Z3_solver_assert(ctx, s, not_f);
-
+
switch (Z3_solver_check(ctx, s)) {
case Z3_L_FALSE:
/* proved */
@@ -286,7 +286,7 @@ void prove(Z3_context ctx, Z3_solver s, Z3_ast f, Z3_bool is_valid)
/**
\brief Assert the axiom: function f is injective in the i-th argument.
-
+
The following axiom is asserted into the logical context:
\code
forall (x_0, ..., x_n) finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i
@@ -294,7 +294,7 @@ void prove(Z3_context ctx, Z3_solver s, Z3_ast f, Z3_bool is_valid)
Where, \c finv is a fresh function declaration.
*/
-void assert_inj_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f, unsigned i)
+void assert_inj_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f, unsigned i)
{
unsigned sz, j;
Z3_sort finv_domain, finv_range;
@@ -310,7 +310,7 @@ void assert_inj_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f, unsigned i)
if (i >= sz) {
exitf("failed to create inj axiom");
}
-
+
/* declare the i-th inverse of f: finv */
finv_domain = Z3_get_range(ctx, f);
finv_range = Z3_get_domain(ctx, f, i);
@@ -320,7 +320,7 @@ void assert_inj_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f, unsigned i)
types = (Z3_sort *) malloc(sizeof(Z3_sort) * sz);
names = (Z3_symbol *) malloc(sizeof(Z3_symbol) * sz);
xs = (Z3_ast *) malloc(sizeof(Z3_ast) * sz);
-
+
/* fill types, names and xs */
for (j = 0; j < sz; j++) { types[j] = Z3_get_domain(ctx, f, j); };
for (j = 0; j < sz; j++) { names[j] = Z3_mk_int_symbol(ctx, j); };
@@ -328,7 +328,7 @@ void assert_inj_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f, unsigned i)
x_i = xs[i];
- /* create f(x_0, ..., x_i, ..., x_{n-1}) */
+ /* create f(x_0, ..., x_i, ..., x_{n-1}) */
fxs = Z3_mk_app(ctx, f, sz, xs);
/* create f_inv(f(x_0, ..., x_i, ..., x_{n-1})) */
@@ -343,12 +343,12 @@ void assert_inj_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f, unsigned i)
printf("\n");
/* create & assert quantifier */
- q = Z3_mk_forall(ctx,
+ q = Z3_mk_forall(ctx,
0, /* using default weight */
1, /* number of patterns */
&p, /* address of the "array" of patterns */
sz, /* number of quantified variables */
- types,
+ types,
names,
eq);
printf("assert axiom:\n%s\n", Z3_ast_to_string(ctx, q));
@@ -361,11 +361,11 @@ void assert_inj_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f, unsigned i)
}
/**
- \brief Assert the axiom: function f is commutative.
-
+ \brief Assert the axiom: function f is commutative.
+
This example uses the SMT-LIB parser to simplify the axiom construction.
*/
-void assert_comm_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f)
+void assert_comm_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f)
{
Z3_sort t;
Z3_symbol f_name, t_name;
@@ -377,16 +377,16 @@ void assert_comm_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f)
Z3_get_domain(ctx, f, 0) != t ||
Z3_get_domain(ctx, f, 1) != t) {
exitf("function must be binary, and argument types must be equal to return type");
- }
-
+ }
+
/* Inside the parser, function f will be referenced using the symbol 'f'. */
f_name = Z3_mk_string_symbol(ctx, "f");
-
+
/* Inside the parser, type t will be referenced using the symbol 'T'. */
t_name = Z3_mk_string_symbol(ctx, "T");
-
- Z3_parse_smtlib_string(ctx,
+
+ Z3_parse_smtlib_string(ctx,
"(benchmark comm :formula (forall (x T) (y T) (= (f x y) (f y x))))",
1, &t_name, &t,
1, &f_name, &f);
@@ -396,15 +396,15 @@ void assert_comm_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f)
}
/**
- \brief Z3 does not support explicitly tuple updates. They can be easily implemented
- as macros. The argument \c t must have tuple type.
+ \brief Z3 does not support explicitly tuple updates. They can be easily implemented
+ as macros. The argument \c t must have tuple type.
A tuple update is a new tuple where field \c i has value \c new_val, and all
other fields have the value of the respective field of \c t.
update(t, i, new_val) is equivalent to
- mk_tuple(proj_0(t), ..., new_val, ..., proj_n(t))
+ mk_tuple(proj_0(t), ..., new_val, ..., proj_n(t))
*/
-Z3_ast mk_tuple_update(Z3_context c, Z3_ast t, unsigned i, Z3_ast new_val)
+Z3_ast mk_tuple_update(Z3_context c, Z3_ast t, unsigned i, Z3_ast new_val)
{
Z3_sort ty;
Z3_func_decl mk_tuple_decl;
@@ -419,11 +419,11 @@ Z3_ast mk_tuple_update(Z3_context c, Z3_ast t, unsigned i, Z3_ast new_val)
}
num_fields = Z3_get_tuple_sort_num_fields(c, ty);
-
+
if (i >= num_fields) {
exitf("invalid tuple update, index is too big");
}
-
+
new_fields = (Z3_ast*) malloc(sizeof(Z3_ast) * num_fields);
for (j = 0; j < num_fields; j++) {
if (i == j) {
@@ -445,7 +445,7 @@ Z3_ast mk_tuple_update(Z3_context c, Z3_ast t, unsigned i, Z3_ast new_val)
/**
\brief Display a symbol in the given output stream.
*/
-void display_symbol(Z3_context c, FILE * out, Z3_symbol s)
+void display_symbol(Z3_context c, FILE * out, Z3_symbol s)
{
switch (Z3_get_symbol_kind(c, s)) {
case Z3_INT_SYMBOL:
@@ -462,7 +462,7 @@ void display_symbol(Z3_context c, FILE * out, Z3_symbol s)
/**
\brief Display the given type.
*/
-void display_sort(Z3_context c, FILE * out, Z3_sort ty)
+void display_sort(Z3_context c, FILE * out, Z3_sort ty)
{
switch (Z3_get_sort_kind(c, ty)) {
case Z3_UNINTERPRETED_SORT:
@@ -480,7 +480,7 @@ void display_sort(Z3_context c, FILE * out, Z3_sort ty)
case Z3_BV_SORT:
fprintf(out, "bv%d", Z3_get_bv_sort_size(c, ty));
break;
- case Z3_ARRAY_SORT:
+ case Z3_ARRAY_SORT:
fprintf(out, "[");
display_sort(c, out, Z3_get_array_sort_domain(c, ty));
fprintf(out, "->");
@@ -488,7 +488,7 @@ void display_sort(Z3_context c, FILE * out, Z3_sort ty)
fprintf(out, "]");
break;
case Z3_DATATYPE_SORT:
- if (Z3_get_datatype_sort_num_constructors(c, ty) != 1)
+ if (Z3_get_datatype_sort_num_constructors(c, ty) != 1)
{
fprintf(out, "%s", Z3_sort_to_string(c,ty));
break;
@@ -516,11 +516,11 @@ void display_sort(Z3_context c, FILE * out, Z3_sort ty)
}
/**
- \brief Custom ast pretty printer.
+ \brief Custom ast pretty printer.
This function demonstrates how to use the API to navigate terms.
*/
-void display_ast(Z3_context c, FILE * out, Z3_ast v)
+void display_ast(Z3_context c, FILE * out, Z3_ast v)
{
switch (Z3_get_ast_kind(c, v)) {
case Z3_NUMERAL_AST: {
@@ -551,7 +551,7 @@ void display_ast(Z3_context c, FILE * out, Z3_ast v)
}
case Z3_QUANTIFIER_AST: {
fprintf(out, "quantifier");
- ;
+ ;
}
default:
fprintf(out, "#unknown");
@@ -561,7 +561,7 @@ void display_ast(Z3_context c, FILE * out, Z3_ast v)
/**
\brief Custom function interpretations pretty printer.
*/
-void display_function_interpretations(Z3_context c, FILE * out, Z3_model m)
+void display_function_interpretations(Z3_context c, FILE * out, Z3_model m)
{
unsigned num_functions, i;
@@ -574,14 +574,14 @@ void display_function_interpretations(Z3_context c, FILE * out, Z3_model m)
Z3_ast func_else;
unsigned num_entries = 0, j;
Z3_func_interp_opt finterp;
-
+
fdecl = Z3_model_get_func_decl(c, m, i);
finterp = Z3_model_get_func_interp(c, m, fdecl);
Z3_func_interp_inc_ref(c, finterp);
name = Z3_get_decl_name(c, fdecl);
display_symbol(c, out, name);
fprintf(out, " = {");
- if (finterp)
+ if (finterp)
num_entries = Z3_func_interp_get_num_entries(c, finterp);
for (j = 0; j < num_entries; j++) {
unsigned num_args, k;
@@ -617,7 +617,7 @@ void display_function_interpretations(Z3_context c, FILE * out, Z3_model m)
/**
\brief Custom model pretty printer.
*/
-void display_model(Z3_context c, FILE * out, Z3_model m)
+void display_model(Z3_context c, FILE * out, Z3_model m)
{
unsigned num_constants;
unsigned i;
@@ -677,7 +677,7 @@ void check2(Z3_context ctx, Z3_solver s, Z3_lbool expected_result)
/**
\brief Display Z3 version in the standard output.
*/
-void display_version()
+void display_version()
{
unsigned major, minor, build, revision;
Z3_get_version(&major, &minor, &build, &revision);
@@ -692,12 +692,12 @@ void display_version()
/**
\brief "Hello world" example: create a Z3 logical context, and delete it.
*/
-void simple_example()
+void simple_example()
{
Z3_context ctx;
LOG_MSG("simple_example");
printf("\nsimple_example\n");
-
+
ctx = mk_context();
/* delete logical context */
@@ -708,7 +708,7 @@ void simple_example()
Demonstration of how Z3 can be used to prove validity of
De Morgan's Duality Law: {e not(x and y) <-> (not x) or ( not y) }
*/
-void demorgan()
+void demorgan()
{
Z3_config cfg;
Z3_context ctx;
@@ -720,7 +720,7 @@ void demorgan()
printf("\nDeMorgan\n");
LOG_MSG("DeMorgan");
-
+
cfg = Z3_mk_config();
ctx = Z3_mk_context(cfg);
Z3_del_config(cfg);
@@ -729,7 +729,7 @@ void demorgan()
symbol_y = Z3_mk_int_symbol(ctx, 1);
x = Z3_mk_const(ctx, symbol_x, bool_sort);
y = Z3_mk_const(ctx, symbol_y, bool_sort);
-
+
/* De Morgan - with a negation around */
/* !(!(x && y) <-> (!x || !y)) */
not_x = Z3_mk_not(ctx, x);
@@ -743,8 +743,8 @@ void demorgan()
rs = Z3_mk_or(ctx, 2, args);
conjecture = Z3_mk_iff(ctx, ls, rs);
negated_conjecture = Z3_mk_not(ctx, conjecture);
-
- s = mk_solver(ctx);
+
+ s = mk_solver(ctx);
Z3_solver_assert(ctx, s, negated_conjecture);
switch (Z3_solver_check(ctx, s)) {
case Z3_L_FALSE:
@@ -767,7 +767,7 @@ void demorgan()
/**
\brief Find a model for x xor y.
*/
-void find_model_example1()
+void find_model_example1()
{
Z3_context ctx;
Z3_ast x, y, x_xor_y;
@@ -782,7 +782,7 @@ void find_model_example1()
x = mk_bool_var(ctx, "x");
y = mk_bool_var(ctx, "y");
x_xor_y = Z3_mk_xor(ctx, x, y);
-
+
Z3_solver_assert(ctx, s, x_xor_y);
printf("model for: x xor y\n");
@@ -796,7 +796,7 @@ void find_model_example1()
\brief Find a model for x < y + 1, x > 2.
Then, assert not(x = y), and find another model.
*/
-void find_model_example2()
+void find_model_example2()
{
Z3_context ctx;
Z3_ast x, y, one, two, y_plus_one;
@@ -807,7 +807,7 @@ void find_model_example2()
printf("\nfind_model_example2\n");
LOG_MSG("find_model_example2");
-
+
ctx = mk_context();
s = mk_solver(ctx);
x = mk_int_var(ctx, "x");
@@ -821,7 +821,7 @@ void find_model_example2()
c1 = Z3_mk_lt(ctx, x, y_plus_one);
c2 = Z3_mk_gt(ctx, x, two);
-
+
Z3_solver_assert(ctx, s, c1);
Z3_solver_assert(ctx, s, c2);
@@ -847,7 +847,7 @@ void find_model_example2()
This function demonstrates how to create uninterpreted types and
functions.
*/
-void prove_example1()
+void prove_example1()
{
Z3_context ctx;
Z3_solver s;
@@ -860,14 +860,14 @@ void prove_example1()
printf("\nprove_example1\n");
LOG_MSG("prove_example1");
-
+
ctx = mk_context();
s = mk_solver(ctx);
/* create uninterpreted type. */
U_name = Z3_mk_string_symbol(ctx, "U");
U = Z3_mk_uninterpreted_sort(ctx, U_name);
-
+
/* declare function g */
g_name = Z3_mk_string_symbol(ctx, "g");
g_domain[0] = U;
@@ -881,7 +881,7 @@ void prove_example1()
/* create g(x), g(y) */
gx = mk_unary_app(ctx, g, x);
gy = mk_unary_app(ctx, g, y);
-
+
/* assert x = y */
eq = Z3_mk_eq(ctx, x, y);
Z3_solver_assert(ctx, s, eq);
@@ -893,7 +893,7 @@ void prove_example1()
/* create g(g(x)) */
ggx = mk_unary_app(ctx, g, gx);
-
+
/* disprove g(g(x)) = g(y) */
f = Z3_mk_eq(ctx, ggx, gy);
printf("disprove: x = y implies g(g(x)) = g(y)\n");
@@ -909,7 +909,7 @@ void prove_example1()
This example demonstrates how to combine uninterpreted functions and arithmetic.
*/
-void prove_example2()
+void prove_example2()
{
Z3_context ctx;
Z3_solver s;
@@ -923,7 +923,7 @@ void prove_example2()
printf("\nprove_example2\n");
LOG_MSG("prove_example2");
-
+
ctx = mk_context();
s = mk_solver(ctx);
@@ -932,7 +932,7 @@ void prove_example2()
g_name = Z3_mk_string_symbol(ctx, "g");
g_domain[0] = int_sort;
g = Z3_mk_func_decl(ctx, g_name, 1, g_domain, int_sort);
-
+
/* create x, y, and z */
x = mk_int_var(ctx, "x");
y = mk_int_var(ctx, "y");
@@ -942,7 +942,7 @@ void prove_example2()
gx = mk_unary_app(ctx, g, x);
gy = mk_unary_app(ctx, g, y);
gz = mk_unary_app(ctx, g, z);
-
+
/* create zero */
zero = mk_int(ctx, 0);
@@ -987,7 +987,7 @@ void prove_example2()
This example also demonstrates how big numbers can be created in Z3.
*/
-void push_pop_example1()
+void push_pop_example1()
{
Z3_context ctx;
Z3_solver s;
@@ -1005,7 +1005,7 @@ void push_pop_example1()
/* create a big number */
int_sort = Z3_mk_int_sort(ctx);
big_number = Z3_mk_numeral(ctx, "1000000000000000000000000000000000000000000000000000000", int_sort);
-
+
/* create number 3 */
three = Z3_mk_numeral(ctx, "3", int_sort);
@@ -1044,7 +1044,7 @@ void push_pop_example1()
check2(ctx, s, Z3_L_TRUE);
/* new constraints can be asserted... */
-
+
/* create y */
y_sym = Z3_mk_string_symbol(ctx, "y");
y = Z3_mk_const(ctx, y_sym, int_sort);
@@ -1056,18 +1056,18 @@ void push_pop_example1()
/* the context is still consistent. */
check2(ctx, s, Z3_L_TRUE);
-
+
del_solver(ctx, s);
Z3_del_context(ctx);
}
/**
- \brief Prove that f(x, y) = f(w, v) implies y = v when
+ \brief Prove that f(x, y) = f(w, v) implies y = v when
\c f is injective in the second argument.
\sa assert_inj_axiom.
*/
-void quantifier_example1()
+void quantifier_example1()
{
Z3_config cfg;
Z3_context ctx;
@@ -1102,10 +1102,10 @@ void quantifier_example1()
f_domain[0] = int_sort;
f_domain[1] = int_sort;
f = Z3_mk_func_decl(ctx, f_name, 2, f_domain, int_sort);
-
+
/* assert that f is injective in the second argument. */
assert_inj_axiom(ctx, s, f, 1);
-
+
/* create x, y, v, w, fxy, fwv */
x = mk_int_var(ctx, "x");
y = mk_int_var(ctx, "y");
@@ -1113,7 +1113,7 @@ void quantifier_example1()
w = mk_int_var(ctx, "w");
fxy = mk_binary_app(ctx, f, x, y);
fwv = mk_binary_app(ctx, f, w, v);
-
+
/* assert f(x, y) = f(w, v) */
p1 = Z3_mk_eq(ctx, fxy, fwv);
Z3_solver_assert(ctx, s, p1);
@@ -1135,15 +1135,15 @@ void quantifier_example1()
del_solver(ctx, s);
Z3_del_context(ctx);
/* reset global parameters set by this function */
- Z3_global_param_reset_all();
+ Z3_global_param_reset_all();
}
/**
\brief Prove store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3)).
-
+
This example demonstrates how to use the array theory.
*/
-void array_example1()
+void array_example1()
{
Z3_context ctx = mk_context();
Z3_solver s = mk_solver(ctx);
@@ -1168,10 +1168,10 @@ void array_example1()
i3 = mk_var(ctx, "i3", int_sort);
v1 = mk_var(ctx, "v1", int_sort);
v2 = mk_var(ctx, "v2", int_sort);
-
+
st1 = Z3_mk_store(ctx, a1, i1, v1);
st2 = Z3_mk_store(ctx, a2, i2, v2);
-
+
sel1 = Z3_mk_select(ctx, a1, i3);
sel2 = Z3_mk_select(ctx, a2, i3);
@@ -1201,7 +1201,7 @@ void array_example1()
This example also shows how to use the \c distinct construct.
*/
-void array_example2()
+void array_example2()
{
Z3_context ctx;
Z3_solver s;
@@ -1217,16 +1217,16 @@ void array_example2()
printf("n = %d\n", n);
ctx = mk_context();
s = mk_solver(ctx);
-
+
bool_sort = Z3_mk_bool_sort(ctx);
array_sort = Z3_mk_array_sort(ctx, bool_sort, bool_sort);
-
+
/* create arrays */
for (i = 0; i < n; i++) {
Z3_symbol s = Z3_mk_int_symbol(ctx, i);
a[i] = Z3_mk_const(ctx, s, array_sort);
}
-
+
/* assert distinct(a[0], ..., a[n]) */
d = Z3_mk_distinct(ctx, n, a);
printf("%s\n", Z3_ast_to_string(ctx, d));
@@ -1234,7 +1234,7 @@ void array_example2()
/* context is satisfiable if n < 5 */
check2(ctx, s, n < 5 ? Z3_L_TRUE : Z3_L_FALSE);
-
+
del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -1243,7 +1243,7 @@ void array_example2()
/**
\brief Simple array type construction/deconstruction example.
*/
-void array_example3()
+void array_example3()
{
Z3_context ctx = mk_context();
Z3_solver s = mk_solver(ctx);
@@ -1254,13 +1254,13 @@ void array_example3()
bool_sort = Z3_mk_bool_sort(ctx);
- int_sort = Z3_mk_int_sort(ctx);
+ int_sort = Z3_mk_int_sort(ctx);
array_sort = Z3_mk_array_sort(ctx, int_sort, bool_sort);
if (Z3_get_sort_kind(ctx, array_sort) != Z3_ARRAY_SORT) {
exitf("type must be an array type");
}
-
+
domain = Z3_get_array_sort_domain(ctx, array_sort);
range = Z3_get_array_sort_range(ctx, array_sort);
@@ -1282,21 +1282,21 @@ void array_example3()
/**
\brief Simple tuple type example. It creates a tuple that is a pair of real numbers.
*/
-void tuple_example1()
+void tuple_example1()
{
Z3_context ctx = mk_context();
Z3_solver s = mk_solver(ctx);
Z3_sort real_sort, pair_sort;
Z3_symbol mk_tuple_name;
Z3_func_decl mk_tuple_decl;
- Z3_symbol proj_names[2];
- Z3_sort proj_sorts[2];
+ Z3_symbol proj_names[2];
+ Z3_sort proj_sorts[2];
Z3_func_decl proj_decls[2];
Z3_func_decl get_x_decl, get_y_decl;
printf("\ntuple_example1\n");
LOG_MSG("tuple_example1");
-
+
real_sort = Z3_mk_real_sort(ctx);
@@ -1310,7 +1310,7 @@ void tuple_example1()
pair_sort = Z3_mk_tuple_sort(ctx, mk_tuple_name, 2, proj_names, proj_sorts, &mk_tuple_decl, proj_decls);
get_x_decl = proj_decls[0]; /* function that extracts the first element of a tuple. */
get_y_decl = proj_decls[1]; /* function that extracts the second element of a tuple. */
-
+
printf("tuple_sort: ");
display_sort(ctx, stdout, pair_sort);
printf("\n");
@@ -1319,11 +1319,11 @@ void tuple_example1()
/* prove that get_x(mk_pair(x,y)) == 1 implies x = 1*/
Z3_ast app1, app2, x, y, one;
Z3_ast eq1, eq2, eq3, thm;
-
+
x = mk_real_var(ctx, "x");
y = mk_real_var(ctx, "y");
app1 = mk_binary_app(ctx, mk_tuple_decl, x, y);
- app2 = mk_unary_app(ctx, get_x_decl, app1);
+ app2 = mk_unary_app(ctx, get_x_decl, app1);
one = Z3_mk_numeral(ctx, "1", real_sort);
eq1 = Z3_mk_eq(ctx, app2, one);
eq2 = Z3_mk_eq(ctx, x, one);
@@ -1343,7 +1343,7 @@ void tuple_example1()
Z3_ast p1, p2, x1, x2, y1, y2;
Z3_ast antecedents[2];
Z3_ast antecedent, consequent, thm;
-
+
p1 = mk_var(ctx, "p1", pair_sort);
p2 = mk_var(ctx, "p2", pair_sort);
x1 = mk_unary_app(ctx, get_x_decl, p1);
@@ -1397,7 +1397,7 @@ void tuple_example1()
/**
\brief Simple bit-vector example. This example disproves that x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers
*/
-void bitvector_example1()
+void bitvector_example1()
{
Z3_context ctx = mk_context();
Z3_solver s = mk_solver(ctx);
@@ -1406,10 +1406,10 @@ void bitvector_example1()
printf("\nbitvector_example1\n");
LOG_MSG("bitvector_example1");
-
-
+
+
bv_sort = Z3_mk_bv_sort(ctx, 32);
-
+
x = mk_var(ctx, "x", bv_sort);
zero = Z3_mk_numeral(ctx, "0", bv_sort);
ten = Z3_mk_numeral(ctx, "10", bv_sort);
@@ -1420,7 +1420,7 @@ void bitvector_example1()
thm = Z3_mk_iff(ctx, c1, c2);
printf("disprove: x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers\n");
prove(ctx, s, thm, Z3_FALSE);
-
+
del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -1432,7 +1432,7 @@ void bitvector_example2()
{
Z3_context ctx = mk_context();
Z3_solver s = mk_solver(ctx);
-
+
/* construct x ^ y - 103 == x * y */
Z3_sort bv_sort = Z3_mk_bv_sort(ctx, 32);
Z3_ast x = mk_var(ctx, "x", bv_sort);
@@ -1446,13 +1446,13 @@ void bitvector_example2()
printf("\nbitvector_example2\n");
LOG_MSG("bitvector_example2");
printf("find values of x and y, such that x ^ y - 103 == x * y\n");
-
+
/* add the constraint x ^ y - 103 == x * y<\tt> to the logical context */
Z3_solver_assert(ctx, s, ctr);
-
+
/* find a model (i.e., values for x an y that satisfy the constraint */
check(ctx, s, Z3_L_TRUE);
-
+
del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -1460,7 +1460,7 @@ void bitvector_example2()
/**
\brief Demonstrate how to use #Z3_eval.
*/
-void eval_example1()
+void eval_example1()
{
Z3_context ctx = mk_context();
Z3_solver s = mk_solver(ctx);
@@ -1470,11 +1470,11 @@ void eval_example1()
printf("\neval_example1\n");
LOG_MSG("eval_example1");
-
+
x = mk_int_var(ctx, "x");
y = mk_int_var(ctx, "y");
two = mk_int(ctx, 2);
-
+
/* assert x < y */
c1 = Z3_mk_lt(ctx, x, y);
Z3_solver_assert(ctx, s, c1);
@@ -1514,7 +1514,7 @@ void eval_example1()
/**
\brief Several logical context can be used simultaneously.
*/
-void two_contexts_example1()
+void two_contexts_example1()
{
Z3_context ctx1, ctx2;
Z3_ast x1, x2;
@@ -1525,22 +1525,22 @@ void two_contexts_example1()
/* using the same (default) configuration to initialized both logical contexts. */
ctx1 = mk_context();
ctx2 = mk_context();
-
+
x1 = Z3_mk_const(ctx1, Z3_mk_int_symbol(ctx1,0), Z3_mk_bool_sort(ctx1));
x2 = Z3_mk_const(ctx2, Z3_mk_int_symbol(ctx2,0), Z3_mk_bool_sort(ctx2));
Z3_del_context(ctx1);
-
+
/* ctx2 can still be used. */
printf("%s\n", Z3_ast_to_string(ctx2, x2));
-
+
Z3_del_context(ctx2);
}
/**
\brief Demonstrates how error codes can be read insted of registering an error handler.
*/
-void error_code_example1()
+void error_code_example1()
{
Z3_config cfg;
Z3_context ctx;
@@ -1563,7 +1563,7 @@ void error_code_example1()
x = mk_bool_var(ctx, "x");
x_decl = Z3_get_app_decl(ctx, Z3_to_app(ctx, x));
Z3_solver_assert(ctx, s, x);
-
+
if (Z3_solver_check(ctx, s) != Z3_L_TRUE) {
exitf("unexpected result");
}
@@ -1596,19 +1596,19 @@ void error_code_example2() {
printf("\nerror_code_example2\n");
LOG_MSG("error_code_example2");
-
+
/* low tech try&catch */
r = setjmp(g_catch_buffer);
if (r == 0) {
Z3_ast x, y, app;
-
+
cfg = Z3_mk_config();
ctx = mk_context_custom(cfg, throw_z3_error);
Z3_del_config(cfg);
-
+
x = mk_int_var(ctx, "x");
y = mk_bool_var(ctx, "y");
- printf("before Z3_mk_iff\n");
+ printf("before Z3_mk_iff\n");
/* the next call will produce an error */
app = Z3_mk_iff(ctx, x, y);
unreachable();
@@ -1625,7 +1625,7 @@ void error_code_example2() {
/**
\brief Demonstrates how to use the SMTLIB parser.
*/
-void parser_example1()
+void parser_example1()
{
Z3_context ctx = mk_context();
Z3_solver s = mk_solver(ctx);
@@ -1633,9 +1633,9 @@ void parser_example1()
printf("\nparser_example1\n");
LOG_MSG("parser_example1");
-
-
- Z3_parse_smtlib_string(ctx,
+
+
+ Z3_parse_smtlib_string(ctx,
"(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))",
0, 0, 0,
0, 0, 0);
@@ -1645,7 +1645,7 @@ void parser_example1()
printf("formula %d: %s\n", i, Z3_ast_to_string(ctx, f));
Z3_solver_assert(ctx, s, f);
}
-
+
check(ctx, s, Z3_L_TRUE);
del_solver(ctx, s);
@@ -1655,7 +1655,7 @@ void parser_example1()
/**
\brief Demonstrates how to initialize the parser symbol table.
*/
-void parser_example2()
+void parser_example2()
{
Z3_context ctx = mk_context();
Z3_solver s = mk_solver(ctx);
@@ -1671,16 +1671,16 @@ void parser_example2()
/* Z3_enable_arithmetic doesn't need to be invoked in this example
because it will be implicitly invoked by mk_int_var.
*/
-
+
x = mk_int_var(ctx, "x");
decls[0] = Z3_get_app_decl(ctx, Z3_to_app(ctx, x));
y = mk_int_var(ctx, "y");
decls[1] = Z3_get_app_decl(ctx, Z3_to_app(ctx, y));
-
+
names[0] = Z3_mk_string_symbol(ctx, "a");
names[1] = Z3_mk_string_symbol(ctx, "b");
-
- Z3_parse_smtlib_string(ctx,
+
+ Z3_parse_smtlib_string(ctx,
"(benchmark tst :formula (> a b))",
0, 0, 0,
/* 'x' and 'y' declarations are inserted as 'a' and 'b' into the parser symbol table. */
@@ -1697,7 +1697,7 @@ void parser_example2()
/**
\brief Demonstrates how to initialize the parser symbol table.
*/
-void parser_example3()
+void parser_example3()
{
Z3_config cfg;
Z3_context ctx;
@@ -1724,10 +1724,10 @@ void parser_example3()
g_domain[0] = int_sort;
g_domain[1] = int_sort;
g = Z3_mk_func_decl(ctx, g_name, 2, g_domain, int_sort);
-
+
assert_comm_axiom(ctx, s, g);
- Z3_parse_smtlib_string(ctx,
+ Z3_parse_smtlib_string(ctx,
"(benchmark tst :formula (forall (x Int) (y Int) (implies (= x y) (= (g x 0) (g 0 y)))))",
0, 0, 0,
1, &g_name, &g);
@@ -1742,17 +1742,17 @@ void parser_example3()
/**
\brief Display the declarations, assumptions and formulas in a SMT-LIB string.
*/
-void parser_example4()
+void parser_example4()
{
Z3_context ctx;
unsigned i, num_decls, num_assumptions, num_formulas;
printf("\nparser_example4\n");
LOG_MSG("parser_example4");
-
+
ctx = mk_context();
-
- Z3_parse_smtlib_string(ctx,
+
+ Z3_parse_smtlib_string(ctx,
"(benchmark tst :extrafuns ((x Int) (y Int)) :assumption (= x 20) :formula (> x y) :formula (> x 0))",
0, 0, 0,
0, 0, 0);
@@ -1792,8 +1792,8 @@ void parser_example5() {
ctx = mk_context_custom(cfg, throw_z3_error);
s = mk_solver(ctx);
Z3_del_config(cfg);
-
- Z3_parse_smtlib_string(ctx,
+
+ Z3_parse_smtlib_string(ctx,
/* the following string has a parsing error: missing parenthesis */
"(benchmark tst :extrafuns ((x Int (y Int)) :formula (> x y) :formula (> x 0))",
0, 0, 0,
@@ -1822,7 +1822,7 @@ void numeral_example() {
Z3_sort real_ty;
printf("\nnumeral_example\n");
LOG_MSG("numeral_example");
-
+
ctx = mk_context();
s = mk_solver(ctx);
@@ -1841,25 +1841,25 @@ void numeral_example() {
del_solver(ctx, s);
Z3_del_context(ctx);
}
-
+
/**
\brief Test ite-term (if-then-else terms).
*/
-void ite_example()
+void ite_example()
{
Z3_context ctx;
Z3_ast f, one, zero, ite;
-
+
printf("\nite_example\n");
LOG_MSG("ite_example");
ctx = mk_context();
-
+
f = Z3_mk_false(ctx);
one = mk_int(ctx, 1);
zero = mk_int(ctx, 0);
ite = Z3_mk_ite(ctx, f, one, zero);
-
+
printf("term: %s\n", Z3_ast_to_string(ctx, ite));
/* delete logical context */
@@ -1879,7 +1879,7 @@ void enum_example() {
Z3_func_decl enum_testers[3];
Z3_ast apple, orange, banana, fruity;
Z3_ast ors[3];
-
+
printf("\nenum_example\n");
LOG_MSG("enum_example");
@@ -1888,7 +1888,7 @@ void enum_example() {
enum_names[2] = Z3_mk_string_symbol(ctx,"orange");
fruit = Z3_mk_enumeration_sort(ctx, name, 3, enum_names, enum_consts, enum_testers);
-
+
printf("%s\n", Z3_func_decl_to_string(ctx, enum_consts[0]));
printf("%s\n", Z3_func_decl_to_string(ctx, enum_consts[1]));
printf("%s\n", Z3_func_decl_to_string(ctx, enum_consts[2]));
@@ -1935,7 +1935,7 @@ void list_example() {
Z3_func_decl nil_decl, is_nil_decl, cons_decl, is_cons_decl, head_decl, tail_decl;
Z3_ast nil, l1, l2, x, y, u, v, fml, fml1;
Z3_ast ors[2];
-
+
printf("\nlist_example\n");
LOG_MSG("list_example");
@@ -1944,7 +1944,7 @@ void list_example() {
int_list = Z3_mk_list_sort(ctx, Z3_mk_string_symbol(ctx, "int_list"), int_ty,
&nil_decl, &is_nil_decl, &cons_decl, &is_cons_decl, &head_decl, &tail_decl);
-
+
nil = Z3_mk_app(ctx, nil_decl, 0, 0);
l1 = mk_binary_app(ctx, cons_decl, mk_int(ctx, 1), nil);
l2 = mk_binary_app(ctx, cons_decl, mk_int(ctx, 2), nil);
@@ -1957,14 +1957,14 @@ void list_example() {
/* cons(x,nil) = cons(y, nil) => x = y */
x = mk_var(ctx, "x", int_ty);
- y = mk_var(ctx, "y", int_ty);
+ y = mk_var(ctx, "y", int_ty);
l1 = mk_binary_app(ctx, cons_decl, x, nil);
l2 = mk_binary_app(ctx, cons_decl, y, nil);
prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE);
/* cons(x,u) = cons(x, v) => u = v */
u = mk_var(ctx, "u", int_list);
- v = mk_var(ctx, "v", int_list);
+ v = mk_var(ctx, "v", int_list);
l1 = mk_binary_app(ctx, cons_decl, x, u);
l2 = mk_binary_app(ctx, cons_decl, y, v);
prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), Z3_TRUE);
@@ -1975,7 +1975,7 @@ void list_example() {
ors[1] = Z3_mk_app(ctx, is_cons_decl, 1, &u);
prove(ctx, s, Z3_mk_or(ctx, 2, ors), Z3_TRUE);
- /* occurs check u != cons(x,u) */
+ /* occurs check u != cons(x,u) */
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), Z3_TRUE);
/* destructors: is_cons(u) => u = cons(head(u),tail(u)) */
@@ -1993,7 +1993,7 @@ void list_example() {
/**
\brief Create a binary tree datatype.
-*/
+*/
void tree_example() {
Z3_context ctx = mk_context();
Z3_solver s = mk_solver(ctx);
@@ -2015,7 +2015,7 @@ void tree_example() {
cons_con = Z3_mk_constructor(ctx, Z3_mk_string_symbol(ctx, "cons"), Z3_mk_string_symbol(ctx, "is_cons"), 2, head_tail, sorts, sort_refs);
constructors[0] = nil_con;
constructors[1] = cons_con;
-
+
cell = Z3_mk_datatype(ctx, Z3_mk_string_symbol(ctx, "cell"), 2, constructors);
Z3_query_constructor(ctx, nil_con, 0, &nil_decl, &is_nil_decl, 0);
@@ -2036,9 +2036,9 @@ void tree_example() {
/* cons(x,u) = cons(x, v) => u = v */
u = mk_var(ctx, "u", cell);
- v = mk_var(ctx, "v", cell);
+ v = mk_var(ctx, "v", cell);
x = mk_var(ctx, "x", cell);
- y = mk_var(ctx, "y", cell);
+ y = mk_var(ctx, "y", cell);
l1 = mk_binary_app(ctx, cons_decl, x, u);
l2 = mk_binary_app(ctx, cons_decl, y, v);
prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), Z3_TRUE);
@@ -2049,7 +2049,7 @@ void tree_example() {
ors[1] = Z3_mk_app(ctx, is_cons_decl, 1, &u);
prove(ctx, s, Z3_mk_or(ctx, 2, ors), Z3_TRUE);
- /* occurs check u != cons(x,u) */
+ /* occurs check u != cons(x,u) */
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), Z3_TRUE);
/* destructors: is_cons(u) => u = cons(car(u),cdr(u)) */
@@ -2072,7 +2072,7 @@ void tree_example() {
forest ::= nil | cons(tree, forest)
tree ::= nil | cons(forest, forest)
-*/
+*/
void forest_example() {
Z3_context ctx = mk_context();
@@ -2110,7 +2110,7 @@ void forest_example() {
cons2_con = Z3_mk_constructor(ctx, Z3_mk_string_symbol(ctx, "cons2"), Z3_mk_string_symbol(ctx, "is_cons2"),2, head_tail, sorts, sort_refs);
constructors2[0] = nil2_con;
constructors2[1] = cons2_con;
-
+
clist1 = Z3_mk_constructor_list(ctx, 2, constructors1);
clist2 = Z3_mk_constructor_list(ctx, 2, constructors2);
@@ -2130,7 +2130,7 @@ void forest_example() {
Z3_query_constructor(ctx, cons2_con, 2, &cons2_decl, &is_cons2_decl, cons_accessors);
car2_decl = cons_accessors[0];
cdr2_decl = cons_accessors[1];
-
+
Z3_del_constructor_list(ctx, clist1);
Z3_del_constructor_list(ctx, clist2);
Z3_del_constructor(ctx,nil1_con);
@@ -2156,7 +2156,7 @@ void forest_example() {
/* cons(x,u) = cons(x, v) => u = v */
u = mk_var(ctx, "u", forest);
- v = mk_var(ctx, "v", forest);
+ v = mk_var(ctx, "v", forest);
x = mk_var(ctx, "x", tree);
y = mk_var(ctx, "y", tree);
l1 = mk_binary_app(ctx, cons1_decl, x, u);
@@ -2169,7 +2169,7 @@ void forest_example() {
ors[1] = Z3_mk_app(ctx, is_cons1_decl, 1, &u);
prove(ctx, s, Z3_mk_or(ctx, 2, ors), Z3_TRUE);
- /* occurs check u != cons(x,u) */
+ /* occurs check u != cons(x,u) */
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), Z3_TRUE);
/* delete logical context */
@@ -2181,14 +2181,14 @@ void forest_example() {
/**
\brief Create a binary tree datatype of the form
- BinTree ::= nil
+ BinTree ::= nil
| node(value : Int, left : BinTree, right : BinTree)
-*/
+*/
void binary_tree_example() {
Z3_context ctx = mk_context();
Z3_solver s = mk_solver(ctx);
Z3_sort cell;
- Z3_func_decl
+ Z3_func_decl
nil_decl, /* nil : BinTree (constructor) */
is_nil_decl, /* is_nil : BinTree -> Bool (tester, return true if the given BinTree is a nil) */
node_decl, /* node : Int, BinTree, BinTree -> BinTree (constructor) */
@@ -2208,15 +2208,15 @@ void binary_tree_example() {
/* nil_con and node_con are auxiliary datastructures used to create the new recursive datatype BinTree */
nil_con = Z3_mk_constructor(ctx, Z3_mk_string_symbol(ctx, "nil"), Z3_mk_string_symbol(ctx, "is-nil"), 0, 0, 0, 0);
- node_con = Z3_mk_constructor(ctx, Z3_mk_string_symbol(ctx, "node"), Z3_mk_string_symbol(ctx, "is-cons"),
+ node_con = Z3_mk_constructor(ctx, Z3_mk_string_symbol(ctx, "node"), Z3_mk_string_symbol(ctx, "is-cons"),
3, node_accessor_names, node_accessor_sorts, node_accessor_sort_refs);
constructors[0] = nil_con;
constructors[1] = node_con;
-
+
/* create the new recursive datatype */
cell = Z3_mk_datatype(ctx, Z3_mk_string_symbol(ctx, "BinTree"), 2, constructors);
- /* retrieve the new declarations: constructors (nil_decl, node_decl), testers (is_nil_decl, is_cons_del), and
+ /* retrieve the new declarations: constructors (nil_decl, node_decl), testers (is_nil_decl, is_cons_del), and
accessors (value_decl, left_decl, right_decl */
Z3_query_constructor(ctx, nil_con, 0, &nil_decl, &is_nil_decl, 0);
Z3_query_constructor(ctx, node_con, 3, &node_decl, &is_node_decl, node_accessors);
@@ -2267,7 +2267,7 @@ void binary_tree_example() {
\brief Prove a theorem and extract, and print the proof.
This example illustrates the use of #Z3_check_assumptions.
-*/
+*/
void unsat_core_and_proof_example() {
Z3_context ctx = mk_proof_context();
Z3_solver s = mk_solver(ctx);
@@ -2290,7 +2290,7 @@ void unsat_core_and_proof_example() {
Z3_ast g1[2] = { f1, p1 };
Z3_ast g2[2] = { f2, p2 };
Z3_ast g3[2] = { f3, p3 };
- Z3_ast g4[2] = { f4, p4 };
+ Z3_ast g4[2] = { f4, p4 };
Z3_lbool result;
Z3_ast proof;
Z3_model m = 0;
@@ -2299,7 +2299,7 @@ void unsat_core_and_proof_example() {
printf("\nunsat_core_and_proof_example\n");
LOG_MSG("unsat_core_and_proof_example");
-
+
Z3_solver_assert(ctx, s, Z3_mk_or(ctx, 2, g1));
Z3_solver_assert(ctx, s, Z3_mk_or(ctx, 2, g2));
Z3_solver_assert(ctx, s, Z3_mk_or(ctx, 2, g3));
@@ -2381,7 +2381,7 @@ void del_ext_context(Z3_ext_context ctx) {
/**
\brief Create a retractable constraint.
-
+
\return An id that can be used to retract/reassert the constraint.
*/
unsigned assert_retractable_cnstr(Z3_ext_context ctx, Z3_ast c) {
@@ -2488,7 +2488,7 @@ void incremental_example1() {
z = mk_int_var(ctx, "z");
two = mk_int(ctx, 2);
one = mk_int(ctx, 1);
-
+
/* assert x < y */
c1 = assert_retractable_cnstr(ext_ctx, Z3_mk_lt(ctx, x, y));
/* assert x = z */
@@ -2497,8 +2497,8 @@ void incremental_example1() {
c3 = assert_retractable_cnstr(ext_ctx, Z3_mk_gt(ctx, x, two));
/* assert y < 1 */
c4 = assert_retractable_cnstr(ext_ctx, Z3_mk_lt(ctx, y, one));
-
- result = ext_check(ext_ctx);
+
+ result = ext_check(ext_ctx);
if (result != Z3_L_FALSE)
exitf("bug in Z3");
printf("unsat\n");
@@ -2550,7 +2550,7 @@ void reference_counter_example() {
// Create a Z3 context where the user is reponsible for managing
// Z3_ast reference counters.
ctx = Z3_mk_context_rc(cfg);
- Z3_del_config(cfg);
+ Z3_del_config(cfg);
s = mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
@@ -2564,16 +2564,16 @@ void reference_counter_example() {
y = Z3_mk_const(ctx, sy, ty);
Z3_inc_ref(ctx, y);
// ty is not needed anymore.
- Z3_dec_ref(ctx, Z3_sort_to_ast(ctx, ty));
+ Z3_dec_ref(ctx, Z3_sort_to_ast(ctx, ty));
x_xor_y = Z3_mk_xor(ctx, x, y);
Z3_inc_ref(ctx, x_xor_y);
// x and y are not needed anymore.
- Z3_dec_ref(ctx, x);
+ Z3_dec_ref(ctx, x);
Z3_dec_ref(ctx, y);
Z3_solver_assert(ctx, s, x_xor_y);
// x_or_y is not needed anymore.
- Z3_dec_ref(ctx, x_xor_y);
-
+ Z3_dec_ref(ctx, x_xor_y);
+
printf("model for: x xor y\n");
check(ctx, s, Z3_L_TRUE);
@@ -2619,12 +2619,12 @@ void substitute_example() {
int_ty = Z3_mk_int_sort(ctx);
a = mk_int_var(ctx,"a");
b = mk_int_var(ctx,"b");
- {
+ {
Z3_sort f_domain[2] = { int_ty, int_ty };
f = Z3_mk_func_decl(ctx, Z3_mk_string_symbol(ctx, "f"), 2, f_domain, int_ty);
}
g = Z3_mk_func_decl(ctx, Z3_mk_string_symbol(ctx, "g"), 1, &int_ty, int_ty);
- {
+ {
Z3_ast args[2] = { a, b };
fab = Z3_mk_app(ctx, f, 2, args);
}
@@ -2665,12 +2665,12 @@ void substitute_vars_example() {
int_ty = Z3_mk_int_sort(ctx);
x0 = Z3_mk_bound(ctx, 0, int_ty);
x1 = Z3_mk_bound(ctx, 1, int_ty);
- {
+ {
Z3_sort f_domain[2] = { int_ty, int_ty };
f = Z3_mk_func_decl(ctx, Z3_mk_string_symbol(ctx, "f"), 2, f_domain, int_ty);
}
g = Z3_mk_func_decl(ctx, Z3_mk_string_symbol(ctx, "g"), 1, &int_ty, int_ty);
- {
+ {
Z3_ast args[2] = { x0, x1 };
f01 = Z3_mk_app(ctx, f, 2, args);
}
@@ -2706,7 +2706,7 @@ void fpa_example() {
printf("\nFPA-example\n");
LOG_MSG("FPA-example");
-
+
cfg = Z3_mk_config();
ctx = Z3_mk_context(cfg);
s = mk_solver(ctx);
@@ -2715,7 +2715,7 @@ void fpa_example() {
double_sort = Z3_mk_fpa_sort(ctx, 11, 53);
rm_sort = Z3_mk_fpa_rounding_mode_sort(ctx);
- // Show that there are x, y s.t. (x + y) = 42.0 (with rounding mode).
+ // Show that there are x, y s.t. (x + y) = 42.0 (with rounding mode).
s_rm = Z3_mk_string_symbol(ctx, "rm");
rm = Z3_mk_const(ctx, s_rm, rm_sort);
s_x = Z3_mk_string_symbol(ctx, "x");
@@ -2742,33 +2742,33 @@ void fpa_example() {
args3[0] = c3;
args3[1] = Z3_mk_and(ctx, 3, and_args);
c4 = Z3_mk_and(ctx, 2, (Z3_ast*)&args3);
-
+
printf("c4: %s\n", Z3_ast_to_string(ctx, c4));
- Z3_solver_push(ctx, s);
+ Z3_solver_push(ctx, s);
Z3_solver_assert(ctx, s, c4);
check(ctx, s, Z3_L_TRUE);
Z3_solver_pop(ctx, s, 1);
// Show that the following are equal:
- // (fp #b0 #b10000000001 #xc000000000000)
+ // (fp #b0 #b10000000001 #xc000000000000)
// ((_ to_fp 11 53) #x401c000000000000))
// ((_ to_fp 11 53) RTZ 1.75 2)))
// ((_ to_fp 11 53) RTZ 7.0)))
-
+
Z3_solver_push(ctx, s);
- c1 = Z3_mk_fpa_fp(ctx,
+ c1 = Z3_mk_fpa_fp(ctx,
Z3_mk_numeral(ctx, "0", Z3_mk_bv_sort(ctx, 1)),
- Z3_mk_numeral(ctx, "3377699720527872", Z3_mk_bv_sort(ctx, 52)),
- Z3_mk_numeral(ctx, "1025", Z3_mk_bv_sort(ctx, 11)));
+ Z3_mk_numeral(ctx, "1025", Z3_mk_bv_sort(ctx, 11)),
+ Z3_mk_numeral(ctx, "3377699720527872", Z3_mk_bv_sort(ctx, 52)));
c2 = Z3_mk_fpa_to_fp_bv(ctx,
Z3_mk_numeral(ctx, "4619567317775286272", Z3_mk_bv_sort(ctx, 64)),
Z3_mk_fpa_sort(ctx, 11, 53));
- c3 = Z3_mk_fpa_to_fp_int_real(ctx,
+ c3 = Z3_mk_fpa_to_fp_int_real(ctx,
Z3_mk_fpa_rtz(ctx),
- Z3_mk_numeral(ctx, "2", Z3_mk_int_sort(ctx)),
- Z3_mk_numeral(ctx, "1.75", Z3_mk_real_sort(ctx)),
+ Z3_mk_numeral(ctx, "2", Z3_mk_int_sort(ctx)), /* exponent */
+ Z3_mk_numeral(ctx, "1.75", Z3_mk_real_sort(ctx)), /* significand */
Z3_mk_fpa_sort(ctx, 11, 53));
- c4 = Z3_mk_fpa_to_fp_real(ctx,
+ c4 = Z3_mk_fpa_to_fp_real(ctx,
Z3_mk_fpa_rtz(ctx),
Z3_mk_numeral(ctx, "7.0", Z3_mk_real_sort(ctx)),
Z3_mk_fpa_sort(ctx, 11, 53));
diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp
index c910b3f99..90b818b4b 100644
--- a/src/api/api_fpa.cpp
+++ b/src/api/api_fpa.cpp
@@ -1077,8 +1077,8 @@ extern "C" {
api::context * ctx = mk_c(c);
fpa_util & fu = ctx->fpautil();
if (!fu.is_rm(to_expr(rm)) ||
- !ctx->autil().is_real(to_expr(sig)) ||
!ctx->autil().is_int(to_expr(exp)) ||
+ !ctx->autil().is_real(to_expr(sig)) ||
!fu.is_float(to_sort(s))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 2cce08697..863d1d8db 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -2490,12 +2490,12 @@ void fpa2bv_converter::mk_to_fp_real_int(func_decl * f, unsigned num, expr * con
SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
expr * bv_rm = to_app(args[0])->get_arg(0);
- rational q;
- if (!m_arith_util.is_numeral(args[1], q))
+ rational e;
+ if (!m_arith_util.is_numeral(args[1], e))
UNREACHABLE();
- rational e;
- if (!m_arith_util.is_numeral(args[2], e))
+ rational q;
+ if (!m_arith_util.is_numeral(args[2], q))
UNREACHABLE();
SASSERT(e.is_int64());
diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp
index 7833ae7d1..317112cae 100644
--- a/src/ast/fpa_decl_plugin.cpp
+++ b/src/ast/fpa_decl_plugin.cpp
@@ -490,11 +490,24 @@ func_decl * fpa_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, para
return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
}
else if (arity == 3 &&
- is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) &&
- is_sort_of(domain[1], m_arith_fid, REAL_SORT) &&
- is_sort_of(domain[2], m_arith_fid, INT_SORT))
+ is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) &&
+ is_sort_of(domain[1], m_arith_fid, REAL_SORT) &&
+ is_sort_of(domain[2], m_arith_fid, INT_SORT))
{
- // Rounding + 1 Real + 1 Int -> 1 FP
+ // Rounding + 1 Real + 1 Int -> 1 FP
+ if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int()))
+ m_manager->raise_exception("expecting two integer parameters to to_fp");
+
+ sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
+ symbol name("to_fp");
+ return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
+ }
+ else if (arity == 3 &&
+ is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) &&
+ is_sort_of(domain[1], m_arith_fid, INT_SORT) &&
+ is_sort_of(domain[2], m_arith_fid, REAL_SORT))
+ {
+ // Rounding + 1 Int + 1 Real -> 1 FP
if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int()))
m_manager->raise_exception("expecting two integer parameters to to_fp");
@@ -545,6 +558,7 @@ func_decl * fpa_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, para
"(Real), "
"(RoundingMode (_ BitVec (eb+sb))), "
"(RoundingMode (_ FloatingPoint eb' sb')), "
+ "(RoundingMode Int Real), "
"(RoundingMode Real Int), "
"(RoundingMode Int), and "
"(RoundingMode Real)."
diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h
index 90e50d8c3..a667bc6f8 100644
--- a/src/ast/fpa_decl_plugin.h
+++ b/src/ast/fpa_decl_plugin.h
@@ -286,9 +286,9 @@ public:
expr * args[] = { rm, t };
return m().mk_app(m_fid, OP_FPA_TO_FP, 2, s->get_parameters(), 2, args);
}
- app * mk_to_fp(sort * s, expr * rm, expr * sig, expr * exp) {
+ app * mk_to_fp(sort * s, expr * rm, expr * exp, expr * sig) {
SASSERT(is_float(s) && s->get_num_parameters() == 2);
- expr * args[] = { rm, sig, exp };
+ expr * args[] = { rm, exp, sig};
return m().mk_app(m_fid, OP_FPA_TO_FP, 2, s->get_parameters(), 3, args);
}
app * mk_to_fp_unsigned(sort * s, expr * rm, expr * t) {
diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp
index cd096d6a5..bc3f8c25e 100644
--- a/src/ast/rewriter/fpa_rewriter.cpp
+++ b/src/ast/rewriter/fpa_rewriter.cpp
@@ -271,6 +271,20 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
result = m_util.mk_value(v);
return BR_DONE;
}
+ else if (m_util.is_rm_numeral(args[0], rmv) &&
+ m_util.au().is_int(args[1]) &&
+ m_util.au().is_real(args[2])) {
+ // rm + int + real -> float
+ if (!m_util.is_rm_numeral(args[0], rmv) ||
+ !m_util.au().is_numeral(args[1], r1) ||
+ !m_util.au().is_numeral(args[2], r2))
+ return BR_FAILED;
+
+ TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";);
+ m_fm.set(v, ebits, sbits, rmv, r1.to_mpq().numerator(), r2.to_mpq());
+ result = m_util.mk_value(v);
+ return BR_DONE;
+ }
else if (bu.is_numeral(args[0], r1, bvs1) &&
bu.is_numeral(args[1], r2, bvs2) &&
bu.is_numeral(args[2], r3, bvs3)) {