diff --git a/scripts/update_api.py b/scripts/update_api.py index 5c28bcd3e..90164e108 100755 --- a/scripts/update_api.py +++ b/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) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 9f0bc564f..c0cfcd079 100644 --- a/src/api/api_fpa.cpp +++ b/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(); diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index 525b59814..6bdbdae0e 100644 --- a/src/api/z3_fpa.h +++ b/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. diff --git a/src/api/z3_replayer.cpp b/src/api/z3_replayer.cpp index 9272ca0fc..79488f6d1 100644 --- a/src/api/z3_replayer.cpp +++ b/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(&(m_args[pos].m_int)); + } + int * get_int_addr(unsigned pos) { check_arg(pos, INT64); return reinterpret_cast(&(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); } diff --git a/src/api/z3_replayer.h b/src/api/z3_replayer.h index 8c77f0e0a..11b761a4d 100644 --- a/src/api/z3_replayer.h +++ b/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);