mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
renamed function to avoid compilation issues
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
034e4f469e
commit
0c2e2d78dd
|
@ -118,7 +118,7 @@ namespace api {
|
|||
arith_util & autil() { return m_arith_util; }
|
||||
bv_util & bvutil() { return m_bv_util; }
|
||||
datalog::dl_decl_util & datalog_util() { return m_datalog_util; }
|
||||
fpa_util & fpa_util() { return m_fpa_util; }
|
||||
fpa_util & fpautil() { return m_fpa_util; }
|
||||
family_id get_basic_fid() const { return m_basic_fid; }
|
||||
family_id get_array_fid() const { return m_array_fid; }
|
||||
family_id get_arith_fid() const { return m_arith_fid; }
|
||||
|
|
|
@ -29,7 +29,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_rounding_mode_sort(c);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_sort r = of_sort(ctx->fpa_util().mk_rm_sort());
|
||||
Z3_sort r = of_sort(ctx->fpautil().mk_rm_sort());
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -40,7 +40,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_round_nearest_ties_to_even(c);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_round_nearest_ties_to_even());
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_even());
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -50,7 +50,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_rne(c);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_round_nearest_ties_to_even());
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_even());
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -61,7 +61,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_round_nearest_ties_to_away(c);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_round_nearest_ties_to_away());
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_away());
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -71,7 +71,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_rna(c);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_round_nearest_ties_to_away());
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_away());
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -82,7 +82,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_round_toward_positive(c);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_round_toward_positive());
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_positive());
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -92,7 +92,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_rtp(c);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_round_toward_positive());
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_positive());
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -103,7 +103,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_round_toward_negative(c);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_round_toward_negative());
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_negative());
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -113,7 +113,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_rtn(c);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_round_toward_negative());
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_negative());
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -124,7 +124,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_round_toward_zero(c);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_round_toward_zero());
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_zero());
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -134,7 +134,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_rtz(c);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_round_toward_zero());
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_zero());
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -148,7 +148,7 @@ extern "C" {
|
|||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
}
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_sort r = of_sort(ctx->fpa_util().mk_float_sort(ebits, sbits));
|
||||
Z3_sort r = of_sort(ctx->fpautil().mk_float_sort(ebits, sbits));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -190,7 +190,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_nan(c, s);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_nan(to_sort(s)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_nan(to_sort(s)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -200,8 +200,8 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_inf(c, s, negative);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(negative != 0 ? ctx->fpa_util().mk_ninf(to_sort(s)) :
|
||||
ctx->fpa_util().mk_pinf(to_sort(s)));
|
||||
Z3_ast r = of_ast(negative != 0 ? ctx->fpautil().mk_ninf(to_sort(s)) :
|
||||
ctx->fpautil().mk_pinf(to_sort(s)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -211,8 +211,8 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_inf(c, s, negative);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(negative != 0 ? ctx->fpa_util().mk_nzero(to_sort(s)) :
|
||||
ctx->fpa_util().mk_pzero(to_sort(s)));
|
||||
Z3_ast r = of_ast(negative != 0 ? ctx->fpautil().mk_nzero(to_sort(s)) :
|
||||
ctx->fpautil().mk_pzero(to_sort(s)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -222,7 +222,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_fp(c, sgn, sig, exp);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_fp(to_expr(sgn), to_expr(sig), to_expr(exp)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_fp(to_expr(sgn), to_expr(sig), to_expr(exp)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -232,12 +232,12 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_numeral_float(c, v, ty);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
scoped_mpf tmp(ctx->fpa_util().fm());
|
||||
ctx->fpa_util().fm().set(tmp,
|
||||
ctx->fpa_util().get_ebits(to_sort(ty)),
|
||||
ctx->fpa_util().get_sbits(to_sort(ty)),
|
||||
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);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_value(tmp));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -247,9 +247,9 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_numeral_double(c, v, ty);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
scoped_mpf tmp(ctx->fpa_util().fm());
|
||||
ctx->fpa_util().fm().set(tmp, ctx->fpa_util().get_ebits(to_sort(ty)), ctx->fpa_util().get_sbits(to_sort(ty)), v);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_value(tmp));
|
||||
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);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -259,12 +259,12 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_numeral_int(c, v, ty);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
scoped_mpf tmp(ctx->fpa_util().fm());
|
||||
ctx->fpa_util().fm().set(tmp,
|
||||
ctx->fpa_util().get_ebits(to_sort(ty)),
|
||||
ctx->fpa_util().get_sbits(to_sort(ty)),
|
||||
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);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_value(tmp));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -274,12 +274,12 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_numeral_uint64_int64(c, sgn, sig, exp, ty);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
scoped_mpf tmp(ctx->fpa_util().fm());
|
||||
ctx->fpa_util().fm().set(tmp,
|
||||
ctx->fpa_util().get_ebits(to_sort(ty)),
|
||||
ctx->fpa_util().get_sbits(to_sort(ty)),
|
||||
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)),
|
||||
sgn != 0, sig, exp);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_value(tmp));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -289,12 +289,12 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_numeral_uint64_int64(c, sgn, sig, exp, ty);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
scoped_mpf tmp(ctx->fpa_util().fm());
|
||||
ctx->fpa_util().fm().set(tmp,
|
||||
ctx->fpa_util().get_ebits(to_sort(ty)),
|
||||
ctx->fpa_util().get_sbits(to_sort(ty)),
|
||||
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)),
|
||||
sgn != 0, sig, exp);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_value(tmp));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -304,7 +304,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_abs(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_abs(to_expr(t)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_abs(to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -314,7 +314,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_neg(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_neg(to_expr(t)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_neg(to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -324,7 +324,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_add(c, rm, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_add(to_expr(rm), to_expr(t1), to_expr(t2)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_add(to_expr(rm), to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -334,7 +334,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_add(c, rm, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_sub(to_expr(rm), to_expr(t1), to_expr(t2)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_sub(to_expr(rm), to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -344,7 +344,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_add(c, rm, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_mul(to_expr(rm), to_expr(t1), to_expr(t2)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_mul(to_expr(rm), to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -354,7 +354,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_add(c, rm, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_div(to_expr(rm), to_expr(t1), to_expr(t2)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_div(to_expr(rm), to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -364,7 +364,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_fma(c, rm, t1, t2, t3);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_fma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_fma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -374,7 +374,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_sqrt(c, rm, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_sqrt(to_expr(rm), to_expr(t)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_sqrt(to_expr(rm), to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -384,7 +384,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_rem(c, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_rem(to_expr(t1), to_expr(t2)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_rem(to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -394,7 +394,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_round_to_integral(c, rm, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_round_to_integral(to_expr(rm), to_expr(t)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_round_to_integral(to_expr(rm), to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -404,7 +404,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_min(c, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_min(to_expr(t1), to_expr(t2)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_min(to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -414,7 +414,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_max(c, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_max(to_expr(t1), to_expr(t2)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_max(to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -424,7 +424,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_leq(c, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_le(to_expr(t1), to_expr(t2)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_le(to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -434,7 +434,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_lt(c, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_lt(to_expr(t1), to_expr(t2)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_lt(to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -444,7 +444,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_geq(c, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_ge(to_expr(t1), to_expr(t2)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_ge(to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -454,7 +454,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_gt(c, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_gt(to_expr(t1), to_expr(t2)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_gt(to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -464,7 +464,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_eq(c, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_float_eq(to_expr(t1), to_expr(t2)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_float_eq(to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -474,7 +474,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_is_normal(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_is_normal(to_expr(t)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_is_normal(to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -484,7 +484,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_is_subnormal(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_is_subnormal(to_expr(t)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_is_subnormal(to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -494,7 +494,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_is_zero(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_is_zero(to_expr(t)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_is_zero(to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -504,7 +504,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_is_infinite(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_is_inf(to_expr(t)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_is_inf(to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -514,7 +514,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_is_nan(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_is_nan(to_expr(t)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_is_nan(to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -524,7 +524,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_is_negative(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_is_negative(to_expr(t)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_is_negative(to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -534,7 +534,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_is_positive(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_is_positive(to_expr(t)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_is_positive(to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -545,7 +545,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_to_fp_bv(c, bv, s);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
fpa_util & fu = ctx->fpa_util();
|
||||
fpa_util & fu = ctx->fpautil();
|
||||
if (!ctx->bvutil().is_bv(to_expr(bv)) ||
|
||||
!fu.is_float(to_sort(s))) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
|
@ -561,7 +561,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_to_fp_float(c, rm, t, s);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
fpa_util & fu = ctx->fpa_util();
|
||||
fpa_util & fu = ctx->fpautil();
|
||||
if (!fu.is_rm(to_expr(rm)) ||
|
||||
!fu.is_float(to_expr(t)) ||
|
||||
!fu.is_float(to_sort(s))) {
|
||||
|
@ -578,7 +578,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_to_fp_real(c, rm, t, s);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
fpa_util & fu = ctx->fpa_util();
|
||||
fpa_util & fu = ctx->fpautil();
|
||||
if (!fu.is_rm(to_expr(rm)) ||
|
||||
!ctx->autil().is_real(to_expr(t)) ||
|
||||
!fu.is_float(to_sort(s))) {
|
||||
|
@ -595,7 +595,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_to_fp_signed(c, rm, t, s);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
fpa_util & fu = ctx->fpa_util();
|
||||
fpa_util & fu = ctx->fpautil();
|
||||
if (!fu.is_rm(to_expr(rm)) ||
|
||||
!ctx->bvutil().is_bv(to_expr(t)) ||
|
||||
!fu.is_float(to_sort(s))) {
|
||||
|
@ -612,7 +612,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_to_fp_unsigned(c, rm, t, s);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
fpa_util & fu = ctx->fpa_util();
|
||||
fpa_util & fu = ctx->fpautil();
|
||||
if (!fu.is_rm(to_expr(rm)) ||
|
||||
!ctx->bvutil().is_bv(to_expr(t)) ||
|
||||
!fu.is_float(to_sort(s))) {
|
||||
|
@ -629,7 +629,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_to_ubv(c, rm, t, sz);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_to_ubv(to_expr(rm), to_expr(t), sz));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_to_ubv(to_expr(rm), to_expr(t), sz));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -639,7 +639,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_to_sbv(c, rm, t, sz);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_to_sbv(to_expr(rm), to_expr(t), sz));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_to_sbv(to_expr(rm), to_expr(t), sz));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -649,7 +649,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_to_real(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_to_real(to_expr(t)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_to_real(to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -659,7 +659,7 @@ extern "C" {
|
|||
LOG_Z3_fpa_get_ebits(c, s);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_NON_NULL(s, 0);
|
||||
return mk_c(c)->fpa_util().get_ebits(to_sort(s));
|
||||
return mk_c(c)->fpautil().get_ebits(to_sort(s));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -668,7 +668,7 @@ extern "C" {
|
|||
LOG_Z3_fpa_get_ebits(c, s);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_NON_NULL(s, 0);
|
||||
return mk_c(c)->fpa_util().get_sbits(to_sort(s));
|
||||
return mk_c(c)->fpautil().get_sbits(to_sort(s));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -677,7 +677,7 @@ extern "C" {
|
|||
LOG_Z3_fpa_get_numeral_sign(c, t, sgn);
|
||||
RESET_ERROR_CODE();
|
||||
ast_manager & m = mk_c(c)->m();
|
||||
mpf_manager & mpfm = mk_c(c)->fpa_util().fm();
|
||||
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
|
||||
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
|
||||
scoped_mpf val(mpfm);
|
||||
bool r = plugin->is_numeral(to_expr(t), val);
|
||||
|
@ -695,7 +695,7 @@ extern "C" {
|
|||
LOG_Z3_fpa_get_numeral_significand_string(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
ast_manager & m = mk_c(c)->m();
|
||||
mpf_manager & mpfm = mk_c(c)->fpa_util().fm();
|
||||
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
|
||||
unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
|
||||
unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
|
||||
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
|
||||
|
@ -726,7 +726,7 @@ extern "C" {
|
|||
LOG_Z3_fpa_get_numeral_exponent_string(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
ast_manager & m = mk_c(c)->m();
|
||||
mpf_manager & mpfm = mk_c(c)->fpa_util().fm();
|
||||
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
|
||||
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
|
||||
scoped_mpf val(mpfm);
|
||||
bool r = plugin->is_numeral(to_expr(t), val);
|
||||
|
@ -750,7 +750,7 @@ extern "C" {
|
|||
LOG_Z3_fpa_get_numeral_exponent_string(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
ast_manager & m = mk_c(c)->m();
|
||||
mpf_manager & mpfm = mk_c(c)->fpa_util().fm();
|
||||
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
|
||||
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
|
||||
scoped_mpf val(mpfm);
|
||||
bool r = plugin->is_numeral(to_expr(t), val);
|
||||
|
@ -768,7 +768,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_to_ieee_bv(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpa_util().mk_float_to_ieee_bv(to_expr(t)));
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_float_to_ieee_bv(to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -778,7 +778,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_to_fp_real_int(c, rm, sig, exp, s);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
fpa_util & fu = ctx->fpa_util();
|
||||
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)) ||
|
||||
|
|
|
@ -59,7 +59,7 @@ extern "C" {
|
|||
RETURN_Z3(0);
|
||||
}
|
||||
sort * _ty = to_sort(ty);
|
||||
bool is_float = mk_c(c)->fpa_util().is_float(_ty);
|
||||
bool is_float = mk_c(c)->fpautil().is_float(_ty);
|
||||
std::string fixed_num;
|
||||
char const* m = n;
|
||||
while (*m) {
|
||||
|
@ -78,7 +78,7 @@ extern "C" {
|
|||
ast * a = 0;
|
||||
if (_ty->get_family_id() == mk_c(c)->get_fpa_fid()) {
|
||||
// avoid expanding floats into huge rationals.
|
||||
fpa_util & fu = mk_c(c)->fpa_util();
|
||||
fpa_util & fu = mk_c(c)->fpautil();
|
||||
scoped_mpf t(fu.fm());
|
||||
fu.fm().set(t, fu.get_ebits(_ty), fu.get_sbits(_ty), MPF_ROUND_TOWARD_ZERO, n);
|
||||
a = fu.mk_value(t);
|
||||
|
@ -148,8 +148,8 @@ extern "C" {
|
|||
return
|
||||
mk_c(c)->autil().is_numeral(e) ||
|
||||
mk_c(c)->bvutil().is_numeral(e) ||
|
||||
mk_c(c)->fpa_util().is_numeral(e) ||
|
||||
mk_c(c)->fpa_util().is_rm_numeral(e);
|
||||
mk_c(c)->fpautil().is_numeral(e) ||
|
||||
mk_c(c)->fpautil().is_rm_numeral(e);
|
||||
Z3_CATCH_RETURN(Z3_FALSE);
|
||||
}
|
||||
|
||||
|
@ -191,10 +191,10 @@ extern "C" {
|
|||
}
|
||||
else {
|
||||
// floats are separated from all others to avoid huge rationals.
|
||||
fpa_util & fu = mk_c(c)->fpa_util();
|
||||
fpa_util & fu = mk_c(c)->fpautil();
|
||||
scoped_mpf tmp(fu.fm());
|
||||
mpf_rounding_mode rm;
|
||||
if (mk_c(c)->fpa_util().is_rm_numeral(to_expr(a), rm)) {
|
||||
if (mk_c(c)->fpautil().is_rm_numeral(to_expr(a), rm)) {
|
||||
switch (rm) {
|
||||
case OP_FPA_RM_NEAREST_TIES_TO_EVEN:
|
||||
return mk_c(c)->mk_external_string("roundNearestTiesToEven");
|
||||
|
@ -214,7 +214,7 @@ extern "C" {
|
|||
break;
|
||||
}
|
||||
}
|
||||
else if (mk_c(c)->fpa_util().is_numeral(to_expr(a), tmp)) {
|
||||
else if (mk_c(c)->fpautil().is_numeral(to_expr(a), tmp)) {
|
||||
return mk_c(c)->mk_external_string(fu.fm().to_string(tmp));
|
||||
}
|
||||
else {
|
||||
|
|
Loading…
Reference in a new issue