mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-27 07:49:49 +00:00
Code Activity

Make rcf is_rational and is_rational_function operations handle zero (#8025)

Browse source 
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>
This commit is contained in:
Josh Berdine 2025-11-16 00:36:32 +00:00 • committed by GitHub
parent 28b31cfe91
commit 5690be8cfc
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/realclosure/realclosure.cpp
View file

@ -1021,7 +1021,7 @@ namespace realclosure {
}
static bool is_rational_function(numeral const & a) {
return is_rational_function(a.m_value);
return !is_zero(a) && is_rational_function(a.m_value);
}
static rational_function_value * to_rational_function(numeral const & a) {
@ -2521,7 +2521,7 @@ namespace realclosure {
\brief Return true if a is a rational.
*/
bool is_rational(numeral const & a) {
return a.m_value->is_rational();
return is_zero(a) || a.m_value->is_rational();
}