mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix #4826
This commit is contained in:
parent
f58618aa04
commit
1619311ff7
|
@ -480,10 +480,12 @@ expr * arith_rewriter::reduce_power(expr * arg, bool is_eq) {
|
|||
if (m_util.is_power(arg, arg0, arg1) && m_util.is_numeral(arg1, k) && k.is_int() &&
|
||||
((is_eq && k > rational(1)) || (!is_eq && k > rational(2)))) {
|
||||
if (is_eq || !k.is_even()) {
|
||||
if (m_util.is_int(arg0))
|
||||
arg0 = m_util.mk_to_real(arg0);
|
||||
new_args.push_back(arg0);
|
||||
}
|
||||
else {
|
||||
new_args.push_back(mk_power(arg0, rational(2)));
|
||||
new_args.push_back(m_util.mk_power(arg0, m_util.mk_real(2)));
|
||||
}
|
||||
}
|
||||
else {
|
||||
|
@ -1245,11 +1247,19 @@ br_status arith_rewriter::mk_rem_core(expr * arg1, expr * arg2, expr_ref & resul
|
|||
return BR_FAILED;
|
||||
}
|
||||
|
||||
app* arith_rewriter_core::mk_power(expr* x, rational const& r) {
|
||||
expr* arith_rewriter_core::coerce(expr* x, sort* s) {
|
||||
if (m_util.is_int(x) && m_util.is_real(s))
|
||||
return m_util.mk_to_real(x);
|
||||
if (m_util.is_real(x) && m_util.is_int(s))
|
||||
return m_util.mk_to_int(x);
|
||||
return x;
|
||||
}
|
||||
|
||||
app* arith_rewriter_core::mk_power(expr* x, rational const& r, sort* s) {
|
||||
SASSERT(r.is_unsigned() && r.is_pos());
|
||||
bool is_int = m_util.is_int(x);
|
||||
app* y = m_util.mk_power(x, m_util.mk_numeral(r, is_int));
|
||||
if (is_int)
|
||||
if (m_util.is_int(s))
|
||||
y = m_util.mk_to_int(y);
|
||||
return y;
|
||||
}
|
||||
|
|
|
@ -44,7 +44,8 @@ protected:
|
|||
decl_kind mul_decl_kind() const { return OP_MUL; }
|
||||
bool use_power() const { return m_mul2power && !m_expand_power; }
|
||||
decl_kind power_decl_kind() const { return OP_POWER; }
|
||||
app* mk_power(expr* x, rational const& r);
|
||||
app* mk_power(expr* x, rational const& r, sort* s);
|
||||
expr* coerce(expr* x, sort* s);
|
||||
public:
|
||||
arith_rewriter_core(ast_manager & m):m_util(m) {}
|
||||
bool is_zero(expr * n) const { return m_util.is_zero(n); }
|
||||
|
|
|
@ -39,7 +39,8 @@ protected:
|
|||
decl_kind add_decl_kind() const { return OP_BADD; }
|
||||
decl_kind mul_decl_kind() const { return OP_BMUL; }
|
||||
bool use_power() const { return false; }
|
||||
app* mk_power(expr* x, rational const& r) { UNREACHABLE(); return nullptr; }
|
||||
app* mk_power(expr* x, rational const& r, sort* s) { UNREACHABLE(); return nullptr; }
|
||||
expr* coerce(expr* x, sort* s) { UNREACHABLE(); return nullptr; }
|
||||
decl_kind power_decl_kind() const { UNREACHABLE(); return static_cast<decl_kind>(UINT_MAX); }
|
||||
|
||||
public:
|
||||
|
|
|
@ -85,15 +85,16 @@ expr * poly_rewriter<Config>::mk_mul_app(unsigned num_args, expr * const * args)
|
|||
return args[0];
|
||||
default:
|
||||
if (use_power()) {
|
||||
sort* s = m().get_sort(args[0]);
|
||||
rational k_prev;
|
||||
expr * prev = get_power_body(args[0], k_prev);
|
||||
rational k;
|
||||
ptr_buffer<expr> new_args;
|
||||
auto push_power = [&]() {
|
||||
if (k_prev.is_one())
|
||||
new_args.push_back(prev);
|
||||
new_args.push_back(this->coerce(prev, s));
|
||||
else
|
||||
new_args.push_back(this->mk_power(prev, k_prev));
|
||||
new_args.push_back(this->mk_power(prev, k_prev, s));
|
||||
};
|
||||
|
||||
for (unsigned i = 1; i < num_args; i++) {
|
||||
|
|
Loading…
Reference in a new issue