mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

FPA API: reintroduced to_ieee_bv

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-12-11 12:05:52 +00:00
parent 72dbb2a513
commit d6ac98a494
6 changed files with 74 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/api/api_fpa.cpp
View file

@ -398,4 +398,15 @@ extern "C" {
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(__in Z3_context c, __in Z3_ast t) {
Z3_TRY;
LOG_Z3_mk_fpa_to_ieee_bv(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->float_util().mk_float_to_ieee_bv(to_expr(t)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
};

13
src/api/z3_fpa.h
View file

@ -555,6 +555,19 @@ extern "C" {
*/
Z3_ast Z3_API Z3_mk_fpa_convert(__in Z3_context c, __in Z3_sort s, __in Z3_ast rm, __in Z3_ast t);
/**
\brief Conversion of a floating point term to a bit-vector term in IEEE754 format.
\param c logical context.
\param t floating-point term.
t must have floating point sort. The size of the resulting bit-vector is automatically determined.
def_API('Z3_mk_fpa_to_ieee_bv', AST, (_in(CONTEXT),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(__in Z3_context c, __in Z3_ast t);
/*@}*/
/*@}*/