From 0b5c38dea555a11a70f0ffe6a67ac8f8b5fee9a7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 11 Apr 2023 16:46:30 -0700 Subject: [PATCH] fix #6676 get rid of rem0 declare it to be mod0 semantics to simplify code paths --- src/ast/arith_decl_plugin.cpp | 7 ++----- src/ast/arith_decl_plugin.h | 10 ++++------ src/math/subpaving/tactic/expr2subpaving.cpp | 1 - src/smt/theory_arith_core.h | 1 - src/smt/theory_lra.cpp | 2 +- 5 files changed, 7 insertions(+), 14 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index a67464a928f..4778caf8933 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -365,7 +365,6 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) { case OP_MOD: return m_i_mod_decl; case OP_DIV0: return m_manager->mk_func_decl(symbol("/0"), m_real_decl, m_real_decl, m_real_decl, func_decl_info(m_family_id, OP_DIV0)); case OP_IDIV0: return m_manager->mk_func_decl(symbol("div0"), m_int_decl, m_int_decl, m_int_decl, func_decl_info(m_family_id, OP_IDIV0)); - case OP_REM0: return m_manager->mk_func_decl(symbol("rem0"), m_int_decl, m_int_decl, m_int_decl, func_decl_info(m_family_id, OP_REM0)); case OP_MOD0: return m_manager->mk_func_decl(symbol("mod0"), m_int_decl, m_int_decl, m_int_decl, func_decl_info(m_family_id, OP_MOD0)); case OP_POWER0: if (is_real) { @@ -612,7 +611,6 @@ void arith_decl_plugin::get_op_names(svector& op_names, symbol con op_names.push_back(builtin_name("euler", OP_E)); op_names.push_back(builtin_name("/0",OP_DIV0)); op_names.push_back(builtin_name("div0",OP_IDIV0)); - op_names.push_back(builtin_name("rem0",OP_REM0)); op_names.push_back(builtin_name("mod0",OP_MOD0)); } } @@ -821,7 +819,7 @@ bool arith_util::is_considered_uninterpreted(func_decl* f, unsigned n, expr* con } if (is_decl_of(f, arith_family_id, OP_REM) && n == 2 && is_numeral(args[1], r) && r.is_zero()) { sort* rs[2] = { mk_int(), mk_int() }; - f_out = m_manager.mk_func_decl(arith_family_id, OP_REM0, 0, nullptr, 2, rs, mk_int()); + f_out = m_manager.mk_func_decl(arith_family_id, OP_MOD0, 0, nullptr, 2, rs, mk_int()); return true; } if (is_decl_of(f, arith_family_id, OP_POWER) && n == 2 && is_numeral(args[1], r) && r.is_zero() && is_numeral(args[0], r) && r.is_zero()) { @@ -857,7 +855,7 @@ func_decl* arith_util::mk_idiv0() { func_decl* arith_util::mk_rem0() { sort* rs[2] = { mk_int(), mk_int() }; - return m_manager.mk_func_decl(arith_family_id, OP_REM0, 0, nullptr, 2, rs, mk_int()); + return m_manager.mk_func_decl(arith_family_id, OP_MOD0, 0, nullptr, 2, rs, mk_int()); } func_decl* arith_util::mk_mod0() { @@ -942,7 +940,6 @@ bool arith_util::is_underspecified(expr* e) const { case OP_MOD: case OP_DIV0: case OP_IDIV0: - case OP_REM0: case OP_MOD0: return true; default: diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 93d0edf2ff6..5dbf3e8cfc8 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -50,7 +50,6 @@ enum arith_op_kind { OP_IDIVIDES, OP_REM, OP_MOD, - OP_REM0, OP_MOD0, OP_TO_REAL, OP_TO_INT, @@ -216,7 +215,6 @@ class arith_decl_plugin : public decl_plugin { case OP_U_ACOS: case OP_DIV0: case OP_IDIV0: - case OP_REM0: case OP_MOD0: case OP_POWER0: return true; @@ -270,7 +268,7 @@ class arith_recognizers { bool is_div0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_DIV0); } bool is_idiv0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_IDIV0); } - bool is_rem0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_REM0); } + bool is_rem0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_MOD0); } bool is_mod0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_MOD0); } bool is_power0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_POWER0); } bool is_power(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_POWER); } @@ -296,7 +294,7 @@ class arith_recognizers { bool is_mod(expr const * n) const { return is_app_of(n, arith_family_id, OP_MOD); } bool is_rem(expr const * n) const { return is_app_of(n, arith_family_id, OP_REM); } bool is_mod0(expr const * n) const { return is_app_of(n, arith_family_id, OP_MOD0); } - bool is_rem0(expr const * n) const { return is_app_of(n, arith_family_id, OP_REM0); } + bool is_rem0(expr const * n) const { return is_app_of(n, arith_family_id, OP_MOD0); } bool is_to_real(expr const * n) const { return is_app_of(n, arith_family_id, OP_TO_REAL); } bool is_to_int(expr const * n) const { return is_app_of(n, arith_family_id, OP_TO_INT); } bool is_is_int(expr const * n) const { return is_app_of(n, arith_family_id, OP_IS_INT); } @@ -355,7 +353,7 @@ class arith_recognizers { MATCH_BINARY(is_div); MATCH_BINARY(is_idiv); MATCH_BINARY(is_mod0); - MATCH_BINARY(is_rem0); + // MATCH_BINARY(is_rem0); MATCH_BINARY(is_div0); MATCH_BINARY(is_idiv0); MATCH_BINARY(is_power); @@ -465,7 +463,7 @@ class arith_util : public arith_recognizers { app * mk_mod(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_MOD, arg1, arg2); } app * mk_div0(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_DIV0, arg1, arg2); } app * mk_idiv0(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_IDIV0, arg1, arg2); } - app * mk_rem0(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_REM0, arg1, arg2); } + app * mk_rem0(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_MOD0, arg1, arg2); } app * mk_mod0(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_MOD0, arg1, arg2); } app * mk_to_real(expr * arg1) { return m_manager.mk_app(arith_family_id, OP_TO_REAL, arg1); } app * mk_to_int(expr * arg1) { return m_manager.mk_app(arith_family_id, OP_TO_INT, arg1); } diff --git a/src/math/subpaving/tactic/expr2subpaving.cpp b/src/math/subpaving/tactic/expr2subpaving.cpp index 3afbc1ecb38..e2c43d12b2d 100644 --- a/src/math/subpaving/tactic/expr2subpaving.cpp +++ b/src/math/subpaving/tactic/expr2subpaving.cpp @@ -311,7 +311,6 @@ struct expr2subpaving::imp { case OP_REM: case OP_IRRATIONAL_ALGEBRAIC_NUM: case OP_DIV0: - case OP_REM0: case OP_MOD0: case OP_IDIV0: throw default_exception("you must apply arithmetic purifier before internalizing expressions into the subpaving module."); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 3a5c86207c2..690775d0835 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -154,7 +154,6 @@ namespace smt { case OP_MOD: case OP_DIV0: case OP_IDIV0: - case OP_REM0: case OP_MOD0: return true; default: diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index d73930a8b46..3b3e3dd79f4 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -469,7 +469,7 @@ class theory_lra::imp { st.to_ensure_var().push_back(n1); st.to_ensure_var().push_back(n2); } - else if (a.is_idiv0(n, n1, n2) || a.is_mod0(n, n1, n2) || a.is_rem0(n, n1, n2)) { + else if (a.is_idiv0(n, n1, n2) || a.is_mod0(n, n1, n2)) { st.to_ensure_var().push_back(n1); st.to_ensure_var().push_back(n2); }