mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
parent
f29b033253
commit
292e72ce0c
|
@ -86,7 +86,7 @@ br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
|
|||
case OP_TANH: SASSERT(num_args == 1); st = mk_tanh_core(args[0], result); break;
|
||||
default: st = BR_FAILED; break;
|
||||
}
|
||||
CTRACE("arith_rewriter", st != BR_FAILED, tout << mk_pp(f, m());
|
||||
CTRACE("arith_rewriter", st != BR_FAILED, tout << st << ": " << mk_pp(f, m());
|
||||
for (unsigned i = 0; i < num_args; ++i) tout << mk_pp(args[i], m()) << " ";
|
||||
tout << "\n==>\n" << mk_pp(result.get(), m()) << "\n";);
|
||||
return st;
|
||||
|
|
|
@ -289,6 +289,18 @@ br_status poly_rewriter<Config>::mk_nflat_mul_core(unsigned num_args, expr * con
|
|||
}
|
||||
}
|
||||
|
||||
if (num_coeffs > 1 || (num_coeffs == 1 && !is_numeral(args[0]))) {
|
||||
ptr_buffer<expr> m_args;
|
||||
for (unsigned i = 0; i < num_args; i ++) {
|
||||
if (!is_numeral(args[i])) {
|
||||
m_args.push_back(args[i]);
|
||||
}
|
||||
}
|
||||
result = mk_mul_app(c, mk_mul_app(m_args.size(), m_args.c_ptr()));
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
|
||||
|
||||
SASSERT(num_coeffs <= num_args - 2);
|
||||
|
||||
if (!m_som || num_add == 0) {
|
||||
|
@ -363,7 +375,7 @@ br_status poly_rewriter<Config>::mk_nflat_mul_core(unsigned num_args, expr * con
|
|||
for (unsigned i = 0; i < num_args; i++) {
|
||||
expr * const * v = sums[i];
|
||||
expr * arg = v[it[i]];
|
||||
m_args.push_back(arg);
|
||||
m_args.push_back(arg);
|
||||
}
|
||||
sum.push_back(mk_mul_app(m_args.size(), m_args.c_ptr()));
|
||||
}
|
||||
|
|
|
@ -1217,10 +1217,8 @@ namespace smt {
|
|||
m_var2num_occs.insert(VAR, occs); \
|
||||
}
|
||||
|
||||
typename sbuffer<coeff_expr>::const_iterator it = p.begin();
|
||||
typename sbuffer<coeff_expr>::const_iterator end = p.end();
|
||||
for (; it != end; ++it) {
|
||||
expr * m = it->second;
|
||||
for (coeff_expr const& kv : p) {
|
||||
expr * m = kv.second;
|
||||
if (is_pure_monomial(m)) {
|
||||
unsigned num_vars = get_num_vars_in_monomial(m);
|
||||
for (unsigned i = 0; i < num_vars; i++) {
|
||||
|
@ -1237,6 +1235,7 @@ namespace smt {
|
|||
else {
|
||||
TRACE("non_linear", tout << mk_pp(m, get_manager()) << "\n";);
|
||||
UNREACHABLE();
|
||||
return;
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -1253,7 +1252,6 @@ namespace smt {
|
|||
template<typename Ext>
|
||||
expr * theory_arith<Ext>::p2expr(sbuffer<coeff_expr> & p) {
|
||||
SASSERT(!p.empty());
|
||||
TRACE("p2expr_bug", display_coeff_exprs(tout, p););
|
||||
ptr_buffer<expr> args;
|
||||
for (coeff_expr const& ce : p) {
|
||||
rational const & c = ce.first;
|
||||
|
@ -1275,6 +1273,7 @@ namespace smt {
|
|||
SASSERT(!args.empty());
|
||||
expr * r = mk_nary_add(args.size(), args.c_ptr());
|
||||
m_nl_new_exprs.push_back(r);
|
||||
TRACE("p2expr_bug", display_coeff_exprs(tout, p); tout << mk_pp(r, get_manager()) << "\n";);
|
||||
return r;
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue