3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-20 15:34:41 +00:00
z3/src/math/realclosure
Josh Berdine 2a785bf291 Make rcf is_rational and is_rational_function operations handle zero (#8025)
The representation of the zero rcf numeral is nullptr, and the is_rational
and is_rational_function operations are not expecting to be called with
nullptr. But there isn't a way to test for that in the API, other than
checking if Z3_rcf_num_to_string returns "0".

This patch adds a couple conditions so that is_rational and
is_rational_function operations handle zero. Maybe this isn't the desired
change. For instance, the is_zero operation could instead be exposed in the
API and preconditions added to the relevant operations.

Signed-off-by: Josh Berdine <josh@berdine.net>
2026-02-18 20:55:56 -08:00
..
CMakeLists.txt [CMake] Move CMake files into their intended location so the 2017-06-12 11:59:00 +01:00
mpz_matrix.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
mpz_matrix.h remove default destructors 2024-10-02 22:20:12 +01:00
rcf_params.pyg Fix some spelling errors (mostly in comments). 2018-10-20 17:07:41 +02:00
realclosure.cpp Make rcf is_rational and is_rational_function operations handle zero (#8025) 2026-02-18 20:55:56 -08:00
realclosure.h Use noexcept more. (#7058) 2023-12-16 12:14:53 +00:00