mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

FPA API bugfixes

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-01-24 17:33:26 +00:00
parent 5f527fa562
commit 9cb50c9f28
1 changed files with 216 additions and 168 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

286
src/api/api_fpa.cpp
View file

@ -29,19 +29,20 @@ extern "C" {
LOG_Z3_mk_fpa_rounding_mode_sort(c); LOG_Z3_mk_fpa_rounding_mode_sort(c);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_sort r = of_sort(ctx->fpautil().mk_rm_sort()); sort * s = ctx->fpautil().mk_rm_sort();
RETURN_Z3(r); mk_c(c)->save_ast_trail(s);
RETURN_Z3(of_sort(s));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(Z3_context c) Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(Z3_context c) {
{
Z3_TRY; Z3_TRY;
LOG_Z3_mk_fpa_round_nearest_ties_to_even(c); LOG_Z3_mk_fpa_round_nearest_ties_to_even(c);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_even()); expr * a = ctx->fpautil().mk_round_nearest_ties_to_even();
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -50,19 +51,20 @@ extern "C" {
LOG_Z3_mk_fpa_rne(c); LOG_Z3_mk_fpa_rne(c);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_even()); expr * a = ctx->fpautil().mk_round_nearest_ties_to_even();
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(Z3_context c) Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(Z3_context c) {
{
Z3_TRY; Z3_TRY;
LOG_Z3_mk_fpa_round_nearest_ties_to_away(c); LOG_Z3_mk_fpa_round_nearest_ties_to_away(c);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_away()); expr * a = ctx->fpautil().mk_round_nearest_ties_to_away();
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -71,19 +73,20 @@ extern "C" {
LOG_Z3_mk_fpa_rna(c); LOG_Z3_mk_fpa_rna(c);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_away()); expr * a = ctx->fpautil().mk_round_nearest_ties_to_away();
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(Z3_context c) Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(Z3_context c) {
{
Z3_TRY; Z3_TRY;
LOG_Z3_mk_fpa_round_toward_positive(c); LOG_Z3_mk_fpa_round_toward_positive(c);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_positive()); expr * a = ctx->fpautil().mk_round_toward_positive();
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -92,19 +95,20 @@ extern "C" {
LOG_Z3_mk_fpa_rtp(c); LOG_Z3_mk_fpa_rtp(c);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_positive()); expr * a = ctx->fpautil().mk_round_toward_positive();
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(Z3_context c) Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(Z3_context c) {
{
Z3_TRY; Z3_TRY;
LOG_Z3_mk_fpa_round_toward_negative(c); LOG_Z3_mk_fpa_round_toward_negative(c);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_negative()); expr * a = ctx->fpautil().mk_round_toward_negative();
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -113,19 +117,20 @@ extern "C" {
LOG_Z3_mk_fpa_rtn(c); LOG_Z3_mk_fpa_rtn(c);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_negative()); expr * a = ctx->fpautil().mk_round_toward_negative();
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(Z3_context c) Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(Z3_context c) {
{
Z3_TRY; Z3_TRY;
LOG_Z3_mk_fpa_round_toward_zero(c); LOG_Z3_mk_fpa_round_toward_zero(c);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_zero()); expr * a = ctx->fpautil().mk_round_toward_zero();
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -134,8 +139,9 @@ extern "C" {
LOG_Z3_mk_fpa_rtz(c); LOG_Z3_mk_fpa_rtz(c);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_zero()); expr * a = ctx->fpautil().mk_round_toward_zero();
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -148,8 +154,9 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
} }
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_sort r = of_sort(ctx->fpautil().mk_float_sort(ebits, sbits)); sort * s = ctx->fpautil().mk_float_sort(ebits, sbits);
RETURN_Z3(r); ctx->save_ast_trail(s);
RETURN_Z3(of_sort(s));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -190,8 +197,9 @@ extern "C" {
LOG_Z3_mk_fpa_nan(c, s); LOG_Z3_mk_fpa_nan(c, s);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_nan(to_sort(s))); expr * a = ctx->fpautil().mk_nan(to_sort(s));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -200,9 +208,10 @@ extern "C" {
LOG_Z3_mk_fpa_inf(c, s, negative); LOG_Z3_mk_fpa_inf(c, s, negative);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(negative != 0 ? ctx->fpautil().mk_ninf(to_sort(s)) : expr * a = negative != 0 ? ctx->fpautil().mk_ninf(to_sort(s)) :
ctx->fpautil().mk_pinf(to_sort(s))); ctx->fpautil().mk_pinf(to_sort(s));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -211,9 +220,10 @@ extern "C" {
LOG_Z3_mk_fpa_inf(c, s, negative); LOG_Z3_mk_fpa_inf(c, s, negative);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(negative != 0 ? ctx->fpautil().mk_nzero(to_sort(s)) : expr * a = negative != 0 ? ctx->fpautil().mk_nzero(to_sort(s)) :
ctx->fpautil().mk_pzero(to_sort(s))); ctx->fpautil().mk_pzero(to_sort(s));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -222,8 +232,9 @@ extern "C" {
LOG_Z3_mk_fpa_fp(c, sgn, sig, exp); LOG_Z3_mk_fpa_fp(c, sgn, sig, exp);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_fp(to_expr(sgn), to_expr(sig), to_expr(exp))); expr * a = ctx->fpautil().mk_fp(to_expr(sgn), to_expr(sig), to_expr(exp));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -237,8 +248,9 @@ extern "C" {
ctx->fpautil().get_ebits(to_sort(ty)), ctx->fpautil().get_ebits(to_sort(ty)),
ctx->fpautil().get_sbits(to_sort(ty)), ctx->fpautil().get_sbits(to_sort(ty)),
v); v);
Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp)); expr * a = ctx->fpautil().mk_value(tmp);
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -249,8 +261,9 @@ extern "C" {
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
scoped_mpf tmp(ctx->fpautil().fm()); scoped_mpf tmp(ctx->fpautil().fm());
ctx->fpautil().fm().set(tmp, ctx->fpautil().get_ebits(to_sort(ty)), ctx->fpautil().get_sbits(to_sort(ty)), v); ctx->fpautil().fm().set(tmp, ctx->fpautil().get_ebits(to_sort(ty)), ctx->fpautil().get_sbits(to_sort(ty)), v);
Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp)); expr * a = ctx->fpautil().mk_value(tmp);
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -264,8 +277,9 @@ extern "C" {
ctx->fpautil().get_ebits(to_sort(ty)), ctx->fpautil().get_ebits(to_sort(ty)),
ctx->fpautil().get_sbits(to_sort(ty)), ctx->fpautil().get_sbits(to_sort(ty)),
v); v);
Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp)); expr * a = ctx->fpautil().mk_value(tmp);
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -279,8 +293,9 @@ extern "C" {
ctx->fpautil().get_ebits(to_sort(ty)), ctx->fpautil().get_ebits(to_sort(ty)),
ctx->fpautil().get_sbits(to_sort(ty)), ctx->fpautil().get_sbits(to_sort(ty)),
sgn != 0, sig, exp); sgn != 0, sig, exp);
Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp)); expr * a = ctx->fpautil().mk_value(tmp);
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -294,8 +309,9 @@ extern "C" {
ctx->fpautil().get_ebits(to_sort(ty)), ctx->fpautil().get_ebits(to_sort(ty)),
ctx->fpautil().get_sbits(to_sort(ty)), ctx->fpautil().get_sbits(to_sort(ty)),
sgn != 0, sig, exp); sgn != 0, sig, exp);
Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp)); expr * a = ctx->fpautil().mk_value(tmp);
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -304,8 +320,9 @@ extern "C" {
LOG_Z3_mk_fpa_abs(c, t); LOG_Z3_mk_fpa_abs(c, t);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_abs(to_expr(t))); expr * a = ctx->fpautil().mk_abs(to_expr(t));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -314,8 +331,9 @@ extern "C" {
LOG_Z3_mk_fpa_neg(c, t); LOG_Z3_mk_fpa_neg(c, t);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_neg(to_expr(t))); expr * a = ctx->fpautil().mk_neg(to_expr(t));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -324,8 +342,9 @@ extern "C" {
LOG_Z3_mk_fpa_add(c, rm, t1, t2); LOG_Z3_mk_fpa_add(c, rm, t1, t2);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_add(to_expr(rm), to_expr(t1), to_expr(t2))); expr * a = ctx->fpautil().mk_add(to_expr(rm), to_expr(t1), to_expr(t2));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -334,8 +353,9 @@ extern "C" {
LOG_Z3_mk_fpa_add(c, rm, t1, t2); LOG_Z3_mk_fpa_add(c, rm, t1, t2);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_sub(to_expr(rm), to_expr(t1), to_expr(t2))); expr * a = ctx->fpautil().mk_sub(to_expr(rm), to_expr(t1), to_expr(t2));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -344,8 +364,9 @@ extern "C" {
LOG_Z3_mk_fpa_add(c, rm, t1, t2); LOG_Z3_mk_fpa_add(c, rm, t1, t2);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_mul(to_expr(rm), to_expr(t1), to_expr(t2))); expr * a = ctx->fpautil().mk_mul(to_expr(rm), to_expr(t1), to_expr(t2));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -354,8 +375,9 @@ extern "C" {
LOG_Z3_mk_fpa_add(c, rm, t1, t2); LOG_Z3_mk_fpa_add(c, rm, t1, t2);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_div(to_expr(rm), to_expr(t1), to_expr(t2))); expr * a = ctx->fpautil().mk_div(to_expr(rm), to_expr(t1), to_expr(t2));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -364,8 +386,9 @@ extern "C" {
LOG_Z3_mk_fpa_fma(c, rm, t1, t2, t3); LOG_Z3_mk_fpa_fma(c, rm, t1, t2, t3);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_fma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3))); expr * a = ctx->fpautil().mk_fma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -374,8 +397,9 @@ extern "C" {
LOG_Z3_mk_fpa_sqrt(c, rm, t); LOG_Z3_mk_fpa_sqrt(c, rm, t);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_sqrt(to_expr(rm), to_expr(t))); expr * a = ctx->fpautil().mk_sqrt(to_expr(rm), to_expr(t));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -384,8 +408,9 @@ extern "C" {
LOG_Z3_mk_fpa_rem(c, t1, t2); LOG_Z3_mk_fpa_rem(c, t1, t2);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_rem(to_expr(t1), to_expr(t2))); expr * a = ctx->fpautil().mk_rem(to_expr(t1), to_expr(t2));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -394,8 +419,9 @@ extern "C" {
LOG_Z3_mk_fpa_round_to_integral(c, rm, t); LOG_Z3_mk_fpa_round_to_integral(c, rm, t);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_round_to_integral(to_expr(rm), to_expr(t))); expr * a = ctx->fpautil().mk_round_to_integral(to_expr(rm), to_expr(t));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -404,8 +430,9 @@ extern "C" {
LOG_Z3_mk_fpa_min(c, t1, t2); LOG_Z3_mk_fpa_min(c, t1, t2);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_min(to_expr(t1), to_expr(t2))); expr * a = ctx->fpautil().mk_min(to_expr(t1), to_expr(t2));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -424,8 +451,9 @@ extern "C" {
LOG_Z3_mk_fpa_leq(c, t1, t2); LOG_Z3_mk_fpa_leq(c, t1, t2);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_le(to_expr(t1), to_expr(t2))); expr * a = ctx->fpautil().mk_le(to_expr(t1), to_expr(t2));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -434,8 +462,9 @@ extern "C" {
LOG_Z3_mk_fpa_lt(c, t1, t2); LOG_Z3_mk_fpa_lt(c, t1, t2);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_lt(to_expr(t1), to_expr(t2))); expr * a = ctx->fpautil().mk_lt(to_expr(t1), to_expr(t2));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -444,8 +473,9 @@ extern "C" {
LOG_Z3_mk_fpa_geq(c, t1, t2); LOG_Z3_mk_fpa_geq(c, t1, t2);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_ge(to_expr(t1), to_expr(t2))); expr * a = ctx->fpautil().mk_ge(to_expr(t1), to_expr(t2));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -454,8 +484,9 @@ extern "C" {
LOG_Z3_mk_fpa_gt(c, t1, t2); LOG_Z3_mk_fpa_gt(c, t1, t2);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_gt(to_expr(t1), to_expr(t2))); expr * a = ctx->fpautil().mk_gt(to_expr(t1), to_expr(t2));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -464,8 +495,9 @@ extern "C" {
LOG_Z3_mk_fpa_eq(c, t1, t2); LOG_Z3_mk_fpa_eq(c, t1, t2);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_float_eq(to_expr(t1), to_expr(t2))); expr * a = ctx->fpautil().mk_float_eq(to_expr(t1), to_expr(t2));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -474,8 +506,9 @@ extern "C" {
LOG_Z3_mk_fpa_is_normal(c, t); LOG_Z3_mk_fpa_is_normal(c, t);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_is_normal(to_expr(t))); expr * a = ctx->fpautil().mk_is_normal(to_expr(t));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -484,8 +517,9 @@ extern "C" {
LOG_Z3_mk_fpa_is_subnormal(c, t); LOG_Z3_mk_fpa_is_subnormal(c, t);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_is_subnormal(to_expr(t))); expr * a = ctx->fpautil().mk_is_subnormal(to_expr(t));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -494,8 +528,9 @@ extern "C" {
LOG_Z3_mk_fpa_is_zero(c, t); LOG_Z3_mk_fpa_is_zero(c, t);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_is_zero(to_expr(t))); expr * a = ctx->fpautil().mk_is_zero(to_expr(t));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -504,8 +539,9 @@ extern "C" {
LOG_Z3_mk_fpa_is_infinite(c, t); LOG_Z3_mk_fpa_is_infinite(c, t);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_is_inf(to_expr(t))); expr * a = ctx->fpautil().mk_is_inf(to_expr(t));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -514,8 +550,9 @@ extern "C" {
LOG_Z3_mk_fpa_is_nan(c, t); LOG_Z3_mk_fpa_is_nan(c, t);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_is_nan(to_expr(t))); expr * a = ctx->fpautil().mk_is_nan(to_expr(t));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -524,8 +561,9 @@ extern "C" {
LOG_Z3_mk_fpa_is_negative(c, t); LOG_Z3_mk_fpa_is_negative(c, t);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_is_negative(to_expr(t))); expr * a = ctx->fpautil().mk_is_negative(to_expr(t));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -534,8 +572,9 @@ extern "C" {
LOG_Z3_mk_fpa_is_positive(c, t); LOG_Z3_mk_fpa_is_positive(c, t);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_is_positive(to_expr(t))); expr * a = ctx->fpautil().mk_is_positive(to_expr(t));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -551,8 +590,9 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return 0; return 0;
} }
Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(bv))); expr * a = fu.mk_to_fp(to_sort(s), to_expr(bv));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -568,8 +608,9 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return 0; return 0;
} }
Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t))); expr * a = fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -585,8 +626,9 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return 0; return 0;
} }
Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t))); expr * a = fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -602,8 +644,9 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return 0; return 0;
} }
Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t))); expr * a = fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -619,8 +662,9 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return 0; return 0;
} }
Z3_ast r = of_ast(fu.mk_to_fp_unsigned(to_sort(s), to_expr(rm), to_expr(t))); expr * a = fu.mk_to_fp_unsigned(to_sort(s), to_expr(rm), to_expr(t));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -629,8 +673,9 @@ extern "C" {
LOG_Z3_mk_fpa_to_ubv(c, rm, t, sz); LOG_Z3_mk_fpa_to_ubv(c, rm, t, sz);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_to_ubv(to_expr(rm), to_expr(t), sz)); expr * a = ctx->fpautil().mk_to_ubv(to_expr(rm), to_expr(t), sz);
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -639,8 +684,9 @@ extern "C" {
LOG_Z3_mk_fpa_to_sbv(c, rm, t, sz); LOG_Z3_mk_fpa_to_sbv(c, rm, t, sz);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_to_sbv(to_expr(rm), to_expr(t), sz)); expr * a = ctx->fpautil().mk_to_sbv(to_expr(rm), to_expr(t), sz);
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -649,8 +695,9 @@ extern "C" {
LOG_Z3_mk_fpa_to_real(c, t); LOG_Z3_mk_fpa_to_real(c, t);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->fpautil().mk_to_real(to_expr(t))); expr * a = ctx->fpautil().mk_to_real(to_expr(t));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -775,7 +822,7 @@ extern "C" {
Z3_ast Z3_API Z3_mk_fpa_to_fp_int_real(Z3_context c, Z3_ast rm, Z3_ast exp, Z3_ast sig, Z3_sort s) { Z3_ast Z3_API Z3_mk_fpa_to_fp_int_real(Z3_context c, Z3_ast rm, Z3_ast exp, Z3_ast sig, Z3_sort s) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_fpa_to_fp_int_real(c, rm, exp, sig, s); LOG_Z3_mk_fpa_to_fp_int_real(c, rm, sig, exp, s);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
fpa_util & fu = ctx->fpautil(); fpa_util & fu = ctx->fpautil();
@ -786,8 +833,9 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return 0; return 0;
} }
Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(sig), to_expr(exp))); expr * a = fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(sig), to_expr(exp));
RETURN_Z3(r); ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }