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

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>

scripts/update_api.py

@@ -1086,6 +1086,9 @@ def def_API(name, result, params):
             elif ty == INT64:
                 log_c.write("  I(0);\n")
                 exe_c.write("in.get_int64_addr(%s)" % i)
+            elif ty == BOOL:
+                log_c.write("  I(0);\n")
+                exe_c.write("in.get_bool_addr(%s)" % i)
             elif ty == VOID_PTR:
                 log_c.write("  P(0);\n")
                 exe_c.write("in.get_obj_addr(%s)" % i)

src/api/api_fpa.cpp

@@ -896,7 +896,7 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
-    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) {
         Z3_TRY;
         LOG_Z3_fpa_get_numeral_sign(c, t, sgn);
         RESET_ERROR_CODE();

src/api/z3_fpa.h

@@ -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.

src/api/z3_replayer.cpp

@@ -662,6 +662,11 @@ struct z3_replayer::imp {
         return v.data();
     }
 
+    bool * get_bool_addr(unsigned pos) {
+        check_arg(pos, INT64);
+        return reinterpret_cast<bool*>(&(m_args[pos].m_int));
+    }
+
     int * get_int_addr(unsigned pos) {
         check_arg(pos, INT64);
         return reinterpret_cast<int*>(&(m_args[pos].m_int));
@@ -790,6 +795,10 @@ void ** z3_replayer::get_obj_array(unsigned pos) const {
     return m_imp->get_obj_array(pos);
 }
 
+bool * z3_replayer::get_bool_addr(unsigned pos) {
+    return m_imp->get_bool_addr(pos);
+}
+
 int * z3_replayer::get_int_addr(unsigned pos) {
     return m_imp->get_int_addr(pos);
 }

src/api/z3_replayer.h

@@ -53,6 +53,7 @@ public:
     Z3_symbol * get_symbol_array(unsigned pos) const;
     void ** get_obj_array(unsigned pos) const;
 
+    bool * get_bool_addr(unsigned pos);
     int * get_int_addr(unsigned pos);
     int64_t * get_int64_addr(unsigned pos);
     unsigned * get_uint_addr(unsigned pos);