mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 20:31:21 +00:00
Code Activity

fix #6676 get rid of rem0 declare it to be mod0 semantics to simplify code paths

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-04-11 16:46:30 -07:00
parent 58a2a9c79c
commit 0b5c38dea5
5 changed files with 7 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/arith_decl_plugin.cpp
View file

@ -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_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_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_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_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: case OP_POWER0:
if (is_real) { if (is_real) {
@ -612,7 +611,6 @@ void arith_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
op_names.push_back(builtin_name("euler", OP_E)); op_names.push_back(builtin_name("euler", OP_E));
op_names.push_back(builtin_name("/0",OP_DIV0)); op_names.push_back(builtin_name("/0",OP_DIV0));
op_names.push_back(builtin_name("div0",OP_IDIV0)); 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)); 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()) { 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() }; 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; 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()) { 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() { func_decl* arith_util::mk_rem0() {
sort* rs[2] = { mk_int(), mk_int() }; 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() { func_decl* arith_util::mk_mod0() {
@ -942,7 +940,6 @@ bool arith_util::is_underspecified(expr* e) const {
case OP_MOD: case OP_MOD:
case OP_DIV0: case OP_DIV0:
case OP_IDIV0: case OP_IDIV0:
case OP_REM0:
case OP_MOD0: case OP_MOD0:
return true; return true;
default: default:

10
src/ast/arith_decl_plugin.h
View file

@ -50,7 +50,6 @@ enum arith_op_kind {
OP_IDIVIDES, OP_IDIVIDES,
OP_REM, OP_REM,
OP_MOD, OP_MOD,
OP_REM0,
OP_MOD0, OP_MOD0,
OP_TO_REAL, OP_TO_REAL,
OP_TO_INT, OP_TO_INT,
@ -216,7 +215,6 @@ public:
case OP_U_ACOS: case OP_U_ACOS:
case OP_DIV0: case OP_DIV0:
case OP_IDIV0: case OP_IDIV0:
case OP_REM0:
case OP_MOD0: case OP_MOD0:
case OP_POWER0: case OP_POWER0:
return true; return true;
@ -270,7 +268,7 @@ public:
bool is_div0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_DIV0); } 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_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_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_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); } bool is_power(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_POWER); }
@ -296,7 +294,7 @@ public:
bool is_mod(expr const * n) const { return is_app_of(n, arith_family_id, OP_MOD); } 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_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_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_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_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); } bool is_is_int(expr const * n) const { return is_app_of(n, arith_family_id, OP_IS_INT); }
@ -355,7 +353,7 @@ public:
MATCH_BINARY(is_div); MATCH_BINARY(is_div);
MATCH_BINARY(is_idiv); MATCH_BINARY(is_idiv);
MATCH_BINARY(is_mod0); MATCH_BINARY(is_mod0);
MATCH_BINARY(is_rem0); // MATCH_BINARY(is_rem0);
MATCH_BINARY(is_div0); MATCH_BINARY(is_div0);
MATCH_BINARY(is_idiv0); MATCH_BINARY(is_idiv0);
MATCH_BINARY(is_power); MATCH_BINARY(is_power);
@ -465,7 +463,7 @@ public:
app * mk_mod(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_MOD, arg1, arg2); } 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_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_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_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_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); } app * mk_to_int(expr * arg1) { return m_manager.mk_app(arith_family_id, OP_TO_INT, arg1); }

1
src/math/subpaving/tactic/expr2subpaving.cpp
View file

@ -311,7 +311,6 @@ struct expr2subpaving::imp {
case OP_REM: case OP_REM:
case OP_IRRATIONAL_ALGEBRAIC_NUM: case OP_IRRATIONAL_ALGEBRAIC_NUM:
case OP_DIV0: case OP_DIV0:
case OP_REM0:
case OP_MOD0: case OP_MOD0:
case OP_IDIV0: case OP_IDIV0:
throw default_exception("you must apply arithmetic purifier before internalizing expressions into the subpaving module."); throw default_exception("you must apply arithmetic purifier before internalizing expressions into the subpaving module.");

1
src/smt/theory_arith_core.h
View file

@ -154,7 +154,6 @@ namespace smt {
case OP_MOD: case OP_MOD:
case OP_DIV0: case OP_DIV0:
case OP_IDIV0: case OP_IDIV0:
case OP_REM0:
case OP_MOD0: case OP_MOD0:
return true; return true;
default: default:

2
src/smt/theory_lra.cpp
View file

@ -469,7 +469,7 @@ class theory_lra::imp {
st.to_ensure_var().push_back(n1); st.to_ensure_var().push_back(n1);
st.to_ensure_var().push_back(n2); 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(n1);
st.to_ensure_var().push_back(n2); st.to_ensure_var().push_back(n2);
} }