mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-05 09:55:15 +00:00
Code Activity

Return sign from Z3_fpa_get_numeral_sign as bool instead of int (#8047)

Browse source 
The underlying `mpf_manager::sgn` function returns a `bool`, and functions
such as `Z3_mk_fpa_numeral_int_uint` take the sign as a `bool`.

Signed-off-by: Josh Berdine <josh@berdine.net>
This commit is contained in:
Josh Berdine 2025-11-26 02:10:38 +00:00 • committed by Nikolaj Bjorner
parent 2b1583a7f0
commit d8ac364bf7
5 changed files with 17 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/api/z3_fpa.h
View file

@ -1236,12 +1236,12 @@ extern "C" {
\param sgn the retrieved sign
\returns true if \c t corresponds to a floating point numeral, otherwise invokes exception handler or returns false
Remarks: sets \c sgn to 0 if `t' is positive and to 1 otherwise, except for
Remarks: sets \c sgn to \c false if `t' is positive and to \c true otherwise, except for
NaN, which is an invalid argument.
def_API('Z3_fpa_get_numeral_sign', BOOL, (_in(CONTEXT), _in(AST), _out(INT)))
def_API('Z3_fpa_get_numeral_sign', BOOL, (_in(CONTEXT), _in(AST), _out(BOOL)))
*/
bool Z3_API Z3_fpa_get_numeral_sign(Z3_context c, Z3_ast t, int * sgn);
bool Z3_API Z3_fpa_get_numeral_sign(Z3_context c, Z3_ast t, bool * sgn);
/**
\brief Return the significand value of a floating-point numeral as a string.