mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

FPA API bug and consistency fixes

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-11-11 12:38:59 +00:00
parent 8d3ef92383
commit 261fe01cea
5 changed files with 95 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

2
examples/c/test_capi.c
View file

@ -2618,7 +2618,7 @@ void fpa_example() {
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_double(ctx, 42.0, 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);

24
src/api/api_fpa.cpp
View file

@ -101,6 +101,22 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_sort Z3_API Z3_mk_fpa_sort_half(__in Z3_context c) {
return Z3_mk_fpa_sort(c, 5, 11);
}
Z3_sort Z3_API Z3_mk_fpa_sort_single(__in Z3_context c) {
return Z3_mk_fpa_sort(c, 8, 24);
}
Z3_sort Z3_API Z3_mk_fpa_sort_double(__in Z3_context c) {
return Z3_mk_fpa_sort(c, 11, 53);
}
Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(__in Z3_context c) {
return Z3_mk_fpa_sort(c, 15, 113);
}
Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s) {
Z3_TRY;
LOG_Z3_mk_fpa_nan(c, s);
@ -131,9 +147,9 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_double(Z3_context c, double v, Z3_sort ty) {
Z3_ast Z3_API Z3_mk_fpa_numeral_double(Z3_context c, double v, Z3_sort ty) {
Z3_TRY;
LOG_Z3_mk_fpa_double(c, v, ty);
LOG_Z3_mk_fpa_numeral_double(c, v, ty);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
scoped_mpf tmp(ctx->float_util().fm());
@ -158,7 +174,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->float_util().mk_uminus(to_expr(t)));
Z3_ast r = of_ast(ctx->float_util().mk_neg(to_expr(t)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@ -208,7 +224,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->float_util().mk_fused_ma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3)));
Z3_ast r = of_ast(ctx->float_util().mk_fma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}

2
src/api/dotnet/Context.cs
View file

@ -3533,7 +3533,7 @@ namespace Microsoft.Z3
public FPNum MkFP(double v, FPSort s)
{
Contract.Ensures(Contract.Result<FPNum>() != null);
return new FPNum(this, Native.Z3_mk_fpa_double(this.nCtx, v, s.NativeObject));
return new FPNum(this, Native.Z3_mk_fpa_numeral_double(this.nCtx, v, s.NativeObject));
}
/// <summary>

92
src/api/z3_fpa.h
View file

@ -23,6 +23,18 @@ Notes:
extern "C" {
#endif // __cplusplus
/**
\defgroup capi C API
*/
/*@{*/
/**
@name Floating-Point API
*/
/*@{*/
/**
\brief Create a rounding mode sort.
@ -92,6 +104,59 @@ extern "C" {
*/
Z3_sort Z3_API Z3_mk_fpa_sort(__in Z3_context c, __in unsigned ebits, __in unsigned sbits);
/**
\brief Create the half-precision (16-bit) floating point sort.
\param c logical context.
\param ebits number of exponent bits
\param sbits number of significand bits
\remark ebits must be larger than 1 and sbits must be larger than 2.
def_API('Z3_mk_fpa_sort_half', SORT, (_in(CONTEXT),))
*/
Z3_sort Z3_API Z3_mk_fpa_sort_half(__in Z3_context c);
/**
\brief Create the single-precision (32-bit) floating point sort.
\param c logical context.
\param ebits number of exponent bits
\param sbits number of significand bits
\remark ebits must be larger than 1 and sbits must be larger than 2.
def_API('Z3_mk_fpa_sort_single', SORT, (_in(CONTEXT),))
*/
Z3_sort Z3_API Z3_mk_fpa_sort_single(__in Z3_context c);
/**
\brief Create the double-precision (64-bit) floating point sort.
\param c logical context.
\param ebits number of exponent bits
\param sbits number of significand bits
\remark ebits must be larger than 1 and sbits must be larger than 2.
def_API('Z3_mk_fpa_sort_double', SORT, (_in(CONTEXT),))
*/
Z3_sort Z3_API Z3_mk_fpa_sort_double(__in Z3_context c);
/**
\brief Create the quadruple-precision (128-bit) floating point sort.
\param c logical context.
\param ebits number of exponent bits
\param sbits number of significand bits
\remark ebits must be larger than 1 and sbits must be larger than 2.
def_API('Z3_mk_fpa_sort_quadruple', SORT, (_in(CONTEXT),))
*/
Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(__in Z3_context c);
/**
\brief Create a NaN of sort s.
@ -129,7 +194,7 @@ extern "C" {
Z3_ast Z3_API Z3_mk_fpa_zero(__in Z3_context c, __in Z3_sort s, __in Z3_bool negative);
/**
\brief Create a numeral of floating point sort.
\brief Create a numeral of floating point sort from a double.
This function can be use to create numerals that fit in a double value.
It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string.
@ -142,27 +207,9 @@ extern "C" {
\sa Z3_mk_numeral
def_API('Z3_mk_fpa_double', AST, (_in(CONTEXT), _in(DOUBLE), _in(SORT)))
def_API('Z3_mk_fpa_numeral_double', AST, (_in(CONTEXT), _in(DOUBLE), _in(SORT)))
*/
Z3_ast Z3_API Z3_mk_fpa_double(__in Z3_context c, __in double v, __in Z3_sort ty);
/**
\brief Create a numeral of floating point sort.
This function can be use to create numerals that fit in a double value.
It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string.
\params c logical context.
\params v value.
\params ty sort.
ty must be a floating point sort
\sa Z3_mk_numeral
def_API('Z3_mk_fpa_double', AST, (_in(CONTEXT), _in(DOUBLE), _in(SORT)))
*/
Z3_ast Z3_API Z3_mk_fpa_double(__in Z3_context c, __in double v, __in Z3_sort ty);
Z3_ast Z3_API Z3_mk_fpa_numeral_double(__in Z3_context c, __in double v, __in Z3_sort ty);
/**
\brief Floating-point absolute value
@ -469,6 +516,9 @@ extern "C" {
*/
Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(__in Z3_context c, __in Z3_ast t);
/*@}*/
/*@}*/
#ifdef __cplusplus
};
#endif // __cplusplus

8
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -1858,14 +1858,6 @@ void fpa2bv_converter::mk_is_positive(func_decl * f, unsigned num, expr * const
result = m.mk_and(m.mk_not(t1), t2);
}
void fpa2bv_converter::mk_is_positive(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 1);
expr_ref t1(m), t2(m);
mk_is_nan(args[0], t1);
mk_is_pos(args[0], t2);
result = m.mk_and(m.mk_not(t1), t2);
}
void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
TRACE("fpa2bv_to_float", for (unsigned i=0; i < num; i++)
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl; );