From 59eec251021ca82334e1fbedeedfbbb9d3cc97f8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 16 Nov 2025 10:08:21 -0800 Subject: [PATCH] fix #8024 Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.cpp | 10 ++++++++-- src/ast/arith_decl_plugin.h | 12 +++++++----- src/ast/rewriter/arith_rewriter.cpp | 12 ++++++++++-- 3 files changed, 25 insertions(+), 9 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index db927e431..3d2bbec17 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -188,8 +188,12 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) { m_to_real_decl = m->mk_func_decl(symbol("to_real"), i, r, func_decl_info(id, OP_TO_REAL)); m->inc_ref(m_to_real_decl); + m_r_to_real_decl = m->mk_func_decl(symbol("to_real"), r, r, func_decl_info(id, OP_TO_REAL)); + m->inc_ref(m_r_to_real_decl); m_to_int_decl = m->mk_func_decl(symbol("to_int"), r, i, func_decl_info(id, OP_TO_INT)); m->inc_ref(m_to_int_decl); + m_i_to_int_decl = m->mk_func_decl(symbol("to_int"), i, i, func_decl_info(id, OP_TO_INT)); + m->inc_ref(m_i_to_int_decl); m_is_int_decl = m->mk_func_decl(symbol("is_int"), r, m->mk_bool_sort(), func_decl_info(id, OP_IS_INT)); m->inc_ref(m_is_int_decl); @@ -311,6 +315,8 @@ void arith_decl_plugin::finalize() { DEC_REF(m_i_rem_decl); DEC_REF(m_to_real_decl); DEC_REF(m_to_int_decl); + DEC_REF(m_r_to_real_decl); + DEC_REF(m_i_to_int_decl); DEC_REF(m_is_int_decl); DEC_REF(m_i_power_decl); DEC_REF(m_r_power_decl); @@ -368,8 +374,8 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) { return m_manager->mk_func_decl(symbol("^0"), m_real_decl, m_real_decl, m_real_decl, func_decl_info(m_family_id, OP_POWER0)); } return m_manager->mk_func_decl(symbol("^0"), m_int_decl, m_int_decl, m_real_decl, func_decl_info(m_family_id, OP_POWER0)); - case OP_TO_REAL: return m_to_real_decl; - case OP_TO_INT: return m_to_int_decl; + case OP_TO_REAL: return is_real ? m_r_to_real_decl : m_to_real_decl; + case OP_TO_INT: return is_real ? m_to_int_decl : m_i_to_int_decl; case OP_IS_INT: return m_is_int_decl; case OP_POWER: return is_real ? m_r_power_decl : m_i_power_decl; case OP_ABS: return is_real ? m_r_abs_decl : m_i_abs_decl; diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 275d39cf1..9dbaeeccd 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -120,11 +120,13 @@ protected: func_decl * m_i_mod_decl; func_decl * m_i_rem_decl; - func_decl * m_to_real_decl; - func_decl * m_to_int_decl; - func_decl * m_is_int_decl; - func_decl * m_r_power_decl; - func_decl * m_i_power_decl; + func_decl * m_to_real_decl = nullptr; + func_decl * m_to_int_decl = nullptr; + func_decl * m_r_to_real_decl = nullptr; + func_decl * m_i_to_int_decl = nullptr; + func_decl * m_is_int_decl = nullptr; + func_decl * m_r_power_decl = nullptr; + func_decl * m_i_power_decl = nullptr; func_decl * m_r_abs_decl; func_decl * m_i_abs_decl; diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index d5ad70a1f..ab9ac1597 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -1829,6 +1829,10 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) { numeral a; expr* x = nullptr; + if (m_util.is_int(arg)) { + result = arg; + return BR_DONE; + } if (m_util.convert_int_numerals_to_real()) return BR_FAILED; @@ -1837,7 +1841,7 @@ br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) { return BR_DONE; } - if (m_util.is_to_real(arg, x)) { + if (m_util.is_to_real(arg, x) && m_util.is_int(x)) { result = x; return BR_DONE; } @@ -1885,6 +1889,10 @@ br_status arith_rewriter::mk_to_real_core(expr * arg, expr_ref & result) { result = m_util.mk_numeral(a, false); return BR_DONE; } + if (m_util.is_real(arg)) { + result = arg; + return BR_DONE; + } // push to_real over OP_ADD, OP_MUL if (m_push_to_real) { if (m_util.is_add(arg) || m_util.is_mul(arg)) { @@ -1909,7 +1917,7 @@ br_status arith_rewriter::mk_is_int(expr * arg, expr_ref & result) { return BR_DONE; } - if (m_util.is_to_real(arg)) { + if (m_util.is_to_real(arg) && m_util.is_int(to_app(arg)->get_arg(0))) { result = m.mk_true(); return BR_DONE; }