diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp index 52768bff2..325928932 100644 --- a/src/math/lp/nex_creator.cpp +++ b/src/math/lp/nex_creator.cpp @@ -624,16 +624,11 @@ bool nex_creator::register_in_join_map(std::map& map, ne return false; } else { map_it->second += r; - TRACE("nla_cn_details", tout << "adding" << r << std::endl;); + TRACE("nla_cn_details", tout << "adding " << r << " , got " << map_it->second << std::endl;); return true; } } -// returns true if a simplificatian happens -bool nex_creator::process_mul_in_simplify_sum(nex_mul* em, std::map &map) { - return register_in_join_map(map, em, em->coeff()); -} - bool nex_creator::fill_join_map_for_sum(ptr_vector & children, std::map& map, std::unordered_set& existing_nex, @@ -653,7 +648,8 @@ bool nex_creator::fill_join_map_for_sum(ptr_vector & children, } existing_nex.insert(e); if (e->is_mul()) { - simplified |= process_mul_in_simplify_sum(to_mul(e), map); + nex_mul * m = to_mul(e); + simplified |= register_in_join_map(map, m, m->coeff()); } else { SASSERT(e->is_var()); simplified |= register_in_join_map(map, e, rational(1)); @@ -666,14 +662,14 @@ void nex_creator::sort_join_sum(ptr_vector & children) { TRACE("nla_cn_details", print_vector_of_ptrs(children, tout);); std::map map([this](const nex *a , const nex *b) { return lt_for_sort_join_sum(a, b); }); - std::unordered_set existing_nex; // handling (nex*) as numbers + std::unordered_set allocated_nexs; // handling (nex*) as numbers nex_scalar * common_scalar; - fill_join_map_for_sum(children, map, existing_nex, common_scalar); + fill_join_map_for_sum(children, map, allocated_nexs, common_scalar); TRACE("nla_cn_details", for (auto & p : map ) { tout << "(" << *p.first << ", " << p.second << ") ";}); children.clear(); for (auto& p : map) { - process_map_pair(p.first, p.second, children, existing_nex); + process_map_pair(p.first, p.second, children, allocated_nexs); } if (common_scalar) { children.push_back(common_scalar); @@ -828,29 +824,21 @@ nex* nex_creator::simplify(nex* e) { return es; } -void nex_creator::process_map_pair(nex *e, const rational& coeff, ptr_vector & children, std::unordered_set& existing_nex) { - // todo : break on shorter functions +void nex_creator::process_map_pair(nex *e, const rational& coeff, ptr_vector & children, std::unordered_set& allocated_nexs) { if (coeff.is_zero()) return; - bool e_is_old = existing_nex.find(e) != existing_nex.end(); - if (e_is_old) { + bool e_is_old = allocated_nexs.find(e) != allocated_nexs.end(); + if (!e_is_old) { + m_allocated.push_back(e); + } + if (e->is_mul()) { + to_mul(e)->coeff() = coeff; + } else { + SASSERT(e->is_var()); if (coeff.is_one()) { children.push_back(e); } else { - if (e->is_var()) { - children.push_back(mk_mul(mk_scalar(coeff), e)); - } else { - to_mul(e)->coeff() = coeff; - e = simplify(e); - children.push_back(e); - } - } - } else { // e is new - if (coeff.is_one()) { - m_allocated.push_back(e); - children.push_back(e); - } else { - children.push_back(simplify(mk_mul(mk_scalar(coeff), e))); + children.push_back(mk_mul(mk_scalar(coeff), e)); } } } diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h index c158fd15f..8192b613f 100644 --- a/src/math/lp/nex_creator.h +++ b/src/math/lp/nex_creator.h @@ -227,7 +227,6 @@ public: bool is_sorted(const nex_mul * e) const; nex* simplify_sum(nex_sum *e); - bool process_mul_in_simplify_sum(nex_mul* e, std::map &); bool is_simplified(const nex *e) const; bool sum_is_simplified(const nex_sum* e) const; diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index e303b0014..d49a4a239 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -304,6 +304,7 @@ bool nla_grobner::simplify_target_monomials_sum(equation * source, unsigned j = find_divisible(targ_sum, high_mon); if (j + 1 == 0) return false; + m_changed_leading_term = (j == 0); unsigned targ_orig_size = targ_sum->size(); for (; j < targ_orig_size; j++) { simplify_target_monomials_sum_j(source, target, targ_sum, high_mon, j); @@ -407,12 +408,14 @@ nex_mul * nla_grobner::divide_ignore_coeffs_perform(nex* e, const nex* h) { // then targ_sum->children()[j] = - (c/b) * e*p void nla_grobner::simplify_target_monomials_sum_j(equation * source, equation *target, nex_sum* targ_sum, const nex* high_mon, unsigned j) { - nex * ej = (*targ_sum)[j]; + TRACE("grobner", tout << "high_mon = " << *high_mon << ", ej = " << *ej << "\n";); nex_mul * ej_over_high_mon = divide_ignore_coeffs(ej, high_mon); if (ej_over_high_mon == nullptr) { + TRACE("grobner", tout << "no div\n";); return; } + TRACE("grobner", tout << "ej_over_high_mon = " << *ej_over_high_mon << "\n";); rational c = ej->is_mul()? to_mul(ej)->coeff() : rational(1); nex_sum * ej_sum = m_nex_creator.mk_sum(); (*targ_sum)[j] = ej_sum; @@ -484,7 +487,7 @@ bool nla_grobner::simplify_to_superpose_with_eq(equation* eq) { ptr_buffer to_delete; equation_set::iterator it = m_to_superpose.begin(); equation_set::iterator end = m_to_superpose.end(); - for (; it != end && !canceled(); ++it) { + for (; it != end && !canceled() && !done(); ++it) { equation * target = *it; m_changed_leading_term = false; // if the leading term is simplified, then the equation has to be moved to m_to_simplify @@ -715,7 +718,7 @@ bool nla_grobner::done() const { || canceled() || - m_reported > 10 + m_reported > 0 // 10 || m_conflict) { TRACE("grobner", tout << "done()\n";);