mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

give up on addition subterms in monomial decomposition caused by disabling rewriter.flat seems to be corner case exercised in #4532.

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-07-07 22:38:21 -07:00
parent 69afd9f6bd
commit e1a0a2e536
1 changed files with 13 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/smt/theory_arith_nl.h
View file

@ -1122,27 +1122,29 @@ bool theory_arith<Ext>::get_polynomial_info(buffer<coeff_expr> const & p, sbuffe
varinfo.reset();
m_var2num_occs.reset();
#define ADD_OCC(VAR) if (has_var(VAR) && !is_fixed(expr2var(VAR))) { \
TRACE("nl_info", tout << "adding occ: " << mk_bounded_pp(VAR, get_manager()) << "\n";); \
unsigned occs = 0; \
m_var2num_occs.find(VAR, occs); \
occs++; \
m_var2num_occs.insert(VAR, occs); \
}
auto add_occ = [&](expr* v) {
if (has_var(v) && !is_fixed(expr2var(v))) {
TRACE("nl_info", tout << "adding occ: " << mk_bounded_pp(v, get_manager()) << "\n";);
unsigned occs = 0;
m_var2num_occs.find(v, occs);
m_var2num_occs.insert(v, 1 + occs);
}
};
for (auto const& ce : p) {
expr * m = ce.second;
if (m_util.is_numeral(m)) {
continue;
}
else if (ctx.e_internalized(m) && !is_pure_monomial(m)) {
ADD_OCC(m);
}
else if (m_util.is_add(m))
return false;
else if (ctx.e_internalized(m) && !is_pure_monomial(m))
add_occ(m);
else {
buffer<var_power_pair> vp;
decompose_monomial(m, vp);
for (auto const& p : vp) {
ADD_OCC(p.first);
add_occ(p.first);
}
}
}