mirror of
https://github.com/Z3Prover/z3
synced 2025-10-31 03:32:28 +00:00
New FPA C-API example
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger
parent
6e849d7f73
commit
b46d76cddb
1 changed files with 73 additions and 76 deletions
|
|
@ -2595,16 +2595,20 @@ void substitute_vars_example() {
|
|||
Z3_del_context(ctx);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Demonstrates some basic features of the FloatingPoint theory.
|
||||
*/
|
||||
|
||||
void fpa_example() {
|
||||
Z3_config cfg;
|
||||
Z3_context ctx;
|
||||
Z3_sort double_sort, rm_sort;
|
||||
Z3_symbol symbol_rm, symbol_x, symbol_y, symbol_q;
|
||||
Z3_ast rm, x, y, n, q, c1, c2, c3, c4, c5, c6;
|
||||
Z3_symbol s_rm, s_x, s_y, s_x_plus_y;
|
||||
Z3_ast rm, x, y, n, x_plus_y, c1, c2, c3, c4, c5, c6;
|
||||
|
||||
printf("\nFPA-example\n");
|
||||
LOG_MSG("FPA-example");
|
||||
|
||||
printf("\nfpa_example\n");
|
||||
LOG_MSG("fpa_example");
|
||||
|
||||
cfg = Z3_mk_config();
|
||||
ctx = Z3_mk_context(cfg);
|
||||
Z3_del_config(cfg);
|
||||
|
|
@ -2612,83 +2616,76 @@ void fpa_example() {
|
|||
double_sort = Z3_mk_fpa_sort(ctx, 11, 53);
|
||||
rm_sort = Z3_mk_fpa_rounding_mode_sort(ctx);
|
||||
|
||||
symbol_rm = Z3_mk_string_symbol(ctx, "rm");
|
||||
rm = Z3_mk_const(ctx, symbol_rm, rm_sort);
|
||||
symbol_x = Z3_mk_string_symbol(ctx, "x");
|
||||
symbol_y = Z3_mk_string_symbol(ctx, "y");
|
||||
x = Z3_mk_const(ctx, symbol_x, double_sort);
|
||||
y = Z3_mk_const(ctx, symbol_y, double_sort);
|
||||
n = Z3_mk_fpa_numeral_double(ctx, 42.0, double_sort);
|
||||
{
|
||||
// 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");
|
||||
s_y = Z3_mk_string_symbol(ctx, "y");
|
||||
x = Z3_mk_const(ctx, s_x, double_sort);
|
||||
y = Z3_mk_const(ctx, s_y, double_sort);
|
||||
n = Z3_mk_fpa_numeral_double(ctx, 42.0, double_sort);
|
||||
|
||||
symbol_q = Z3_mk_string_symbol(ctx, "q");
|
||||
q = Z3_mk_const(ctx, symbol_q, double_sort);
|
||||
c1 = Z3_mk_eq(ctx, q, Z3_mk_fpa_add(ctx, rm, x, y));
|
||||
s_x_plus_y = Z3_mk_string_symbol(ctx, "x_plus_y");
|
||||
x_plus_y = Z3_mk_const(ctx, s_x_plus_y, double_sort);
|
||||
c1 = Z3_mk_eq(ctx, x_plus_y, Z3_mk_fpa_add(ctx, rm, x, y));
|
||||
|
||||
Z3_ast args[2] = { c1, Z3_mk_eq(ctx, q, n) };
|
||||
c2 = Z3_mk_and(ctx, 2, (Z3_ast*)&args);
|
||||
Z3_ast args[2] = { c1, Z3_mk_eq(ctx, x_plus_y, n) };
|
||||
c2 = Z3_mk_and(ctx, 2, (Z3_ast*)&args);
|
||||
|
||||
Z3_ast args2[2] = { c2, Z3_mk_not(ctx, Z3_mk_eq(ctx, rm, Z3_mk_fpa_round_nearest_ties_to_away(ctx))) };
|
||||
c3 = Z3_mk_and(ctx, 2, (Z3_ast*)&args2);
|
||||
Z3_ast args2[2] = { c2, Z3_mk_not(ctx, Z3_mk_eq(ctx, rm, Z3_mk_fpa_rtz(ctx))) };
|
||||
c3 = Z3_mk_and(ctx, 2, (Z3_ast*)&args2);
|
||||
|
||||
Z3_ast and_args[3] = {
|
||||
Z3_mk_not(ctx, Z3_mk_fpa_is_zero(ctx, y)),
|
||||
Z3_mk_not(ctx, Z3_mk_fpa_is_nan(ctx, y)),
|
||||
Z3_mk_not(ctx, Z3_mk_fpa_is_inf(ctx, y)) };
|
||||
Z3_ast args3[2] = { c3, Z3_mk_and(ctx, 3, and_args) };
|
||||
c4 = Z3_mk_and(ctx, 2, (Z3_ast*)&args3);
|
||||
|
||||
|
||||
Z3_assert_cnstr(ctx, c4);
|
||||
Z3_push(ctx);
|
||||
|
||||
// c5 := (IEEEBV(x) == 7.0).
|
||||
c5 = Z3_mk_eq(ctx, Z3_mk_fpa_to_ieee_bv(ctx, x),
|
||||
Z3_mk_numeral(ctx, "4619567317775286272", Z3_mk_bv_sort(ctx, 64)));
|
||||
|
||||
Z3_assert_cnstr(ctx, c5);
|
||||
|
||||
Z3_model m = 0;
|
||||
Z3_lbool result = Z3_check_and_get_model(ctx, &m);
|
||||
switch (result) {
|
||||
case Z3_L_FALSE:
|
||||
printf("unsat\n");
|
||||
break;
|
||||
case Z3_L_UNDEF:
|
||||
printf("unknown\n");
|
||||
printf("potential model:\n%s\n", Z3_model_to_string(ctx, m));
|
||||
break;
|
||||
case Z3_L_TRUE:
|
||||
printf("sat\n%s\n", Z3_model_to_string(ctx, m));
|
||||
Z3_del_model(ctx, m);
|
||||
break;
|
||||
}
|
||||
|
||||
Z3_pop(ctx, 1);
|
||||
|
||||
// c6 := (IEEEBV(x) == 28.0).
|
||||
c6 = Z3_mk_eq(ctx, Z3_mk_fpa_to_ieee_bv(ctx, x),
|
||||
Z3_mk_numeral(ctx, "4628574517030027264", Z3_mk_bv_sort(ctx, 64)));
|
||||
|
||||
Z3_assert_cnstr(ctx, c6);
|
||||
Z3_push(ctx);
|
||||
|
||||
m = 0;
|
||||
result = Z3_check_and_get_model(ctx, &m);
|
||||
switch (result) {
|
||||
case Z3_L_FALSE:
|
||||
printf("unsat\n");
|
||||
break;
|
||||
case Z3_L_UNDEF:
|
||||
printf("unknown\n");
|
||||
printf("potential model:\n%s\n", Z3_model_to_string(ctx, m));
|
||||
break;
|
||||
case Z3_L_TRUE:
|
||||
printf("sat\n%s\n", Z3_model_to_string(ctx, m));
|
||||
Z3_del_model(ctx, m);
|
||||
break;
|
||||
Z3_ast and_args[3] = {
|
||||
Z3_mk_not(ctx, Z3_mk_fpa_is_zero(ctx, y)),
|
||||
Z3_mk_not(ctx, Z3_mk_fpa_is_nan(ctx, y)),
|
||||
Z3_mk_not(ctx, Z3_mk_fpa_is_infinite(ctx, y)) };
|
||||
Z3_ast args3[2] = { c3, 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_push(ctx);
|
||||
Z3_assert_cnstr(ctx, c4);
|
||||
check(ctx, Z3_L_TRUE);
|
||||
Z3_pop(ctx, 1);
|
||||
}
|
||||
|
||||
Z3_pop(ctx, 1);
|
||||
|
||||
{
|
||||
// Show that the following are equal:
|
||||
// (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_ast args3[3];
|
||||
|
||||
Z3_push(ctx);
|
||||
c1 = Z3_mk_fpa_fp(ctx,
|
||||
Z3_mk_numeral(ctx, "0", Z3_mk_bv_sort(ctx, 1)),
|
||||
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_real_int(ctx,
|
||||
Z3_mk_fpa_rtz(ctx),
|
||||
Z3_mk_numeral(ctx, "1.75", Z3_mk_real_sort(ctx)),
|
||||
Z3_mk_numeral(ctx, "2", Z3_mk_int_sort(ctx)),
|
||||
Z3_mk_fpa_sort(ctx, 11, 53));
|
||||
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));
|
||||
args3[0] = Z3_mk_eq(ctx, c1, c2);
|
||||
args3[1] = Z3_mk_eq(ctx, c1, c3);
|
||||
args3[2] = Z3_mk_eq(ctx, c1, c4);
|
||||
c5 = Z3_mk_and(ctx, 3, args3);
|
||||
|
||||
printf("c5: %s\n", Z3_ast_to_string(ctx, c5));
|
||||
Z3_assert_cnstr(ctx, c5);
|
||||
check(ctx, Z3_L_TRUE);
|
||||
Z3_pop(ctx, 1);
|
||||
}
|
||||
|
||||
Z3_del_context(ctx);
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue