mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

Renamed Z3_mk_double to Z3_mk_fpa_double for consistency

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-06-11 13:27:21 +01:00
parent c3263e4731
commit c2a2d2d0df
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/api/api_fpa.cpp
View file

@ -121,9 +121,9 @@ extern "C" {
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
Z3_ast Z3_API Z3_mk_double(Z3_context c, double v, Z3_sort ty) { Z3_ast Z3_API Z3_mk_fpa_double(Z3_context c, double v, Z3_sort ty) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_double(c, v, ty); LOG_Z3_mk_fpa_double(c, v, ty);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
scoped_mpf tmp(ctx->float_util().fm()); scoped_mpf tmp(ctx->float_util().fm());

2
src/api/z3_fpa.h
View file

@ -131,7 +131,7 @@ extern "C" {
def_API('Z3_mk_double', AST, (_in(CONTEXT), _in(DOUBLE), _in(SORT))) def_API('Z3_mk_double', AST, (_in(CONTEXT), _in(DOUBLE), _in(SORT)))
*/ */
Z3_ast Z3_API Z3_mk_double(__in Z3_context c, __in double v, __in Z3_sort ty); Z3_ast Z3_API Z3_mk_fpa_double(__in Z3_context c, __in double v, __in Z3_sort ty);
/** /**
\brief Floating-point absolute value \brief Floating-point absolute value