mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

fix #4811

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-11-22 16:05:44 -08:00
parent 65464f5944
commit 193ca57444
4 changed files with 23 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/ast/rewriter/arith_rewriter.cpp
View file

@ -483,7 +483,7 @@ expr * arith_rewriter::reduce_power(expr * arg, bool is_eq) {
new_args.push_back(arg0);
}
else {
new_args.push_back(m_util.mk_power(arg0, m_util.mk_numeral(rational(2), m_util.is_int(arg))));
new_args.push_back(mk_power(arg0, rational(2)));
}
}
else {
@ -1042,7 +1042,6 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
}
return BR_FAILED;
}
//
// implement div ab ac = floor( ab / ac) = floor (b / c) = div b c
@ -1246,6 +1245,15 @@ 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) {
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)
y = m_util.mk_to_int(y);
return y;
}
br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & result) {
numeral x, y;
bool is_num_x = m_util.is_numeral(arg1, x);
@ -1446,6 +1454,9 @@ br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) {
real_args.push_back(c);
}
}
if (real_args.empty() && m_util.is_power(arg))
return BR_FAILED;
if (real_args.empty()) {
result = m().mk_app(get_fid(), to_app(arg)->get_decl()->get_decl_kind(), int_args.size(), int_args.c_ptr());
return BR_REWRITE1;

1
src/ast/rewriter/arith_rewriter.h
View file

@ -44,6 +44,7 @@ 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);
public:
arith_rewriter_core(ast_manager & m):m_util(m) {}
bool is_zero(expr * n) const { return m_util.is_zero(n); }

1
src/ast/rewriter/bv_rewriter.h
View file

@ -39,6 +39,7 @@ 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; }
decl_kind power_decl_kind() const { UNREACHABLE(); return static_cast<decl_kind>(UINT_MAX); }
public:

19
src/ast/rewriter/poly_rewriter_def.h
View file

@ -89,15 +89,12 @@ expr * poly_rewriter<Config>::mk_mul_app(unsigned num_args, expr * const * args)
expr * prev = get_power_body(args[0], k_prev);
rational k;
ptr_buffer<expr> new_args;
#define PUSH_POWER() { \
if (k_prev.is_one()) { \
new_args.push_back(prev); \
} \
else { \
expr * pargs[2] = { prev, mk_numeral(k_prev) }; \
new_args.push_back(m().mk_app(get_fid(), power_decl_kind(), 2, pargs)); \
} \
}
auto push_power = [&]() {
if (k_prev.is_one())
new_args.push_back(prev);
else
new_args.push_back(mk_power(prev, k_prev));
};
for (unsigned i = 1; i < num_args; i++) {
expr * arg = get_power_body(args[i], k);
@ -105,12 +102,12 @@ expr * poly_rewriter<Config>::mk_mul_app(unsigned num_args, expr * const * args)
k_prev += k;
}
else {
PUSH_POWER();
push_power();
prev = arg;
k_prev = k;
}
}
PUSH_POWER();
push_power();
SASSERT(new_args.size() > 0);
if (new_args.size() == 1) {
return new_args[0];