From 7d13bcb18e5443bbd33f1857612bb50d1149a6ca Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 8 Oct 2019 17:36:27 -0700 Subject: [PATCH] work on Grobner Signed-off-by: Lev Nachmanson --- src/math/lp/nex.h | 13 ++-- src/math/lp/nla_grobner.cpp | 132 +++++++++++++++++++++++++++++++----- src/math/lp/nla_grobner.h | 26 +++---- src/math/lp/var_eqs.h | 4 +- 4 files changed, 135 insertions(+), 40 deletions(-) diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h index e09a1eeff..a0eb2b621 100644 --- a/src/math/lp/nex.h +++ b/src/math/lp/nex.h @@ -55,6 +55,8 @@ class nex_scalar; // This is the class of non-linear expressions class nex { public: + // the scalar and the variable have size 1 + virtual unsigned size() const { return 1; } virtual expr_type type() const = 0; virtual std::ostream& print(std::ostream&) const = 0; nex() {} @@ -160,9 +162,6 @@ public: friend std::ostream& operator<<(std::ostream& out, const nex_pow & p) { out << p.to_string(); return out; } }; -bool less_than_nex(const nex* a, const nex* b, const lt_on_vars& lt); - - class nex_mul : public nex { vector m_children; @@ -395,10 +394,10 @@ inline std::ostream& operator<<(std::ostream& out, const nex& e ) { return e.print(out); } -inline bool less_than_nex_standard(const nex* a, const nex* b) { - lt_on_vars lt = [](lpvar j, lpvar k) { return j < k; }; - return less_than_nex(a, b, lt); -} +// inline bool less_than_nex_standard(const nex* a, const nex* b) { +// lt_on_vars lt = [](lpvar j, lpvar k) { return j < k; }; +// return less_than_nex(a, b, lt); +// } inline std::unordered_set get_vars_of_expr(const nex *e ) { std::unordered_set r; diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index c8b098caf..7c75ed0b8 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -189,22 +189,17 @@ void nla_grobner::init() { } bool nla_grobner::is_trivial(equation* eq) const { - return eq->m_monomials.empty(); + return eq->m_exp->size() == 0; } -bool nla_grobner:: is_better_choice(equation * eq1, equation * eq2) { +bool nla_grobner::is_better_choice(equation * eq1, equation * eq2) { if (!eq2) return true; if (is_trivial(eq1)) return true; if (is_trivial(eq2)) return false; - if (eq1->m_monomials[0]->get_degree() < eq2->m_monomials[0]->get_degree()) - return true; - if (eq1->m_monomials[0]->get_degree() > eq2->m_monomials[0]->get_degree()) - return false; - return eq1->m_monomials.size() < eq2->m_monomials.size(); - + return m_nex_creator.lt(eq1->m_exp, eq2->m_exp); } void nla_grobner::del_equation(equation * eq) { @@ -214,7 +209,7 @@ void nla_grobner::del_equation(equation * eq) { m_to_process.erase(eq); SASSERT(m_equations_to_delete[eq->m_bidx] == eq); m_equations_to_delete[eq->m_bidx] = 0; - del_monomials(eq->m_monomials); + del_monomials(eq->m_exp); dealloc(eq); */ } @@ -237,8 +232,27 @@ nla_grobner::equation* nla_grobner::pick_next() { } nla_grobner::equation* nla_grobner::simplify_using_processed(equation* eq) { - NOT_IMPLEMENTED_YET(); - return nullptr; + bool result = false; + bool simplified; + TRACE("grobner", tout << "simplifying: "; display_equation(tout, *eq); tout << "using already processed equalities\n";); + do { + simplified = false; + for (equation const* p : m_processed) { + equation * new_eq = simplify(p, eq); + if (new_eq) { + result = true; + simplified = true; + eq = new_eq; + } + if (canceled()) { + return nullptr; + } + } + } + while (simplified); + TRACE("grobner", tout << "simplification result: "; display_equation(tout, *eq);); + return result ? eq : nullptr; + } nla_grobner::equation* nla_grobner::simplify_processed(equation* eq) { @@ -395,8 +409,75 @@ void nla_grobner:: del_equations(unsigned old_size) { void nla_grobner::display_equations(std::ostream & out, equation_set const & v, char const * header) const { NOT_IMPLEMENTED_YET(); } -void nla_grobner::display_equation(std::ostream & out, equation const & eq) const { + + +// void nla_grobner::simplify(ptr_vector & monomials) { +// NOT_IMPLEMENTED_YET(); +// // std::stable_sort(monomials.begin(), monomials.end(), m_monomial_lt); +// // merge_monomials(monomials); +// // normalize_coeff(monomials); +// } + +nla_grobner::equation * nla_grobner::simplify(equation const * source, equation * target) { NOT_IMPLEMENTED_YET(); + /* + TRACE("grobner", tout << "simplifying: "; display_equation(tout, *target); tout << "using: "; display_equation(tout, *source);); + if (source->get_num_monomials() == 0) + return nullptr; + m_stats.m_simplify++; + bool result = false; + bool simplified; + do { + simplified = false; + unsigned i = 0; + unsigned j = 0; + unsigned sz = target->m_monomials.size(); + monomial const * LT = source->get_monomial(0); + ptr_vector & new_monomials = m_tmp_monomials; + new_monomials.reset(); + ptr_vector & rest = m_tmp_vars1; + for (; i < sz; i++) { + monomial * curr = target->m_monomials[i]; + rest.reset(); + if (is_subset(LT, curr, rest)) { + if (i == 0) + m_changed_leading_term = true; + if (!result) { + // first time that source is being applied. + target->m_dep = m_dep_manager.mk_join(target->m_dep, source->m_dep); + } + simplified = true; + result = true; + rational coeff = curr->m_coeff; + coeff /= LT->m_coeff; + coeff.neg(); + if (!rest.empty()) + target->m_lc = false; + mul_append(1, source, coeff, rest, new_monomials); + del_monomial(curr); + target->m_monomials[i] = 0; + } + else { + target->m_monomials[j] = curr; + j++; + } + } + if (simplified) { + target->m_monomials.shrink(j); + target->m_monomials.append(new_monomials.size(), new_monomials.c_ptr()); + simplify(target); + } + } + while (simplified && !m_manager.canceled()); + TRACE("grobner", tout << "result: "; display_equation(tout, *target);); + return result ? target : nullptr;*/ + return nullptr; +} + +std::ostream& nla_grobner::display_equation(std::ostream & out, equation & eq) { + tout << "m_exp = " << *eq.m_exp << "\n"; + tout << "dep = "; display_dependency(tout, eq.m_dep) << "\n"; + return tout; } void nla_grobner::display_monomial(std::ostream & out, monomial const & m) const { @@ -408,22 +489,37 @@ void nla_grobner::display(std::ostream & out) const { } void nla_grobner::assert_eq_0(const nex* e, ci_dependency * dep) { + TRACE("nla_grobner", tout << "e = " << *e << "\n";); if (e == nullptr) return; equation * eq = new equation(); - init_equation(eq, dep); + init_equation(eq, e, dep); m_to_process.insert(eq); } -void nla_grobner::init_equation(equation* e, ci_dependency * dep) { - NOT_IMPLEMENTED_YET(); - /* eq->m_scope_lvl = get_scope_level(); +void nla_grobner::init_equation(equation* eq, const nex*e, ci_dependency * dep) { unsigned bidx = m_equations_to_delete.size(); eq->m_bidx = bidx; - eq->m_dep = d; + eq->m_dep = dep; eq->m_lc = true; + eq->m_exp = e; m_equations_to_delete.push_back(eq); - SASSERT(m_equations_to_delete[eq->m_bidx] == eq);*/ + SASSERT(m_equations_to_delete[eq->m_bidx] == eq); } +std::ostream& nla_grobner::display_dependency(std::ostream& out, ci_dependency* dep) { + svector expl; + m_dep_manager.linearize(dep, expl); + { + lp::explanation e(expl); + if (!expl.empty()) { + out << "upper constraints\n"; + m_core->print_explanation(e, out); + }else { + out << "no constraints\n"; + } + } + return out; +} + } // end of nla namespace diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index a98042661..6ffcea020 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -22,7 +22,7 @@ #include "math/lp/nla_common.h" #include "math/lp/nex.h" #include "math/lp/nex_creator.h" -#include "util/dependency.h" +//#include "util/dependency.h" namespace nla { class core; @@ -55,18 +55,17 @@ class nla_grobner : common { }; class equation { - unsigned m_scope_lvl; //!< scope level when this equation was created. - unsigned m_bidx:31; //!< position at m_equations_to_delete - unsigned m_lc:1; //!< true if equation if a linear combination of the input equations. - ptr_vector m_monomials; //!< sorted monomials - v_dependency * m_dep; //!< justification for the equality + unsigned m_bidx:31; //!< position at m_equations_to_delete + unsigned m_lc:1; //!< true if equation if a linear combination of the input equations. + const nex * m_exp; //!< sorted monomials + ci_dependency * m_dep; //!< justification for the equality friend class nla_grobner; equation() {} public: - unsigned get_num_monomials() const { return m_monomials.size(); } - monomial const * get_monomial(unsigned idx) const { return m_monomials[idx]; } - monomial * const * get_monomials() const { return m_monomials.c_ptr(); } - v_dependency * get_dependency() const { return m_dep; } + unsigned get_num_monomials() const { return m_exp->size(); } + nex_mul* const * get_monomial(unsigned idx) const { NOT_IMPLEMENTED_YET(); + return nullptr; } + ci_dependency * get_dependency() const { return m_dep; } unsigned hash() const { return m_bidx; } bool is_linear_combination() const { return m_lc; } }; @@ -122,7 +121,7 @@ private: void del_equations(unsigned old_size); void del_equation(equation * eq); void display_equations(std::ostream & out, equation_set const & v, char const * header) const; - void display_equation(std::ostream & out, equation const & eq) const; + std::ostream& display_equation(std::ostream & out, equation & eq); void display_monomial(std::ostream & out, monomial const & m) const; @@ -142,8 +141,8 @@ private: return rational(1); } - void init_equation(equation* eq, ci_dependency* d); - + void init_equation(equation* eq, const nex*, ci_dependency* d); + equation * simplify(equation const * source, equation * target); // bool less_than_on_vars(lpvar a, lpvar b) const { // const auto &aw = m_nex_creatorm_active_vars_weights[a]; // const auto &ab = m_active_vars_weights[b]; @@ -160,6 +159,7 @@ private: // return less_than_nex(a, b, lt); // } + std::ostream& display_dependency(std::ostream& out, ci_dependency*); }; // end of grobner } diff --git a/src/math/lp/var_eqs.h b/src/math/lp/var_eqs.h index 880f085ca..58f5e3f09 100644 --- a/src/math/lp/var_eqs.h +++ b/src/math/lp/var_eqs.h @@ -345,7 +345,7 @@ public: } }; // end of var_eqs -template -std::ostream& operator<<(var_eqs const& ve, std::ostream& out) { return ve.display(out); } +// template +// std::ostream& operator<<(var_eqs const& ve, std::ostream& out) { return ve.display(out); } }