From 5a2ce93ed7b56deb1ffddb0484baf995d9991b34 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 22 Oct 2019 11:48:32 -0700 Subject: [PATCH] port Grobner Signed-off-by: Lev Nachmanson --- src/math/lp/nex.h | 4 +++ src/math/lp/nla_grobner.cpp | 67 ++++++++++++++++++++++++++++++++----- src/math/lp/nla_grobner.h | 8 +++-- 3 files changed, 68 insertions(+), 11 deletions(-) diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h index f08a3d03b..4f576a3a7 100644 --- a/src/math/lp/nex.h +++ b/src/math/lp/nex.h @@ -224,6 +224,10 @@ public: add_child_in_power(e, 1); } + void add_child_in_power(nex_pow& p) { + add_child_in_power(p.e(), p.pow()); + } + const nex_pow& operator[](unsigned j) const { return m_children[j]; } nex_pow& operator[](unsigned j) { return m_children[j]; } diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 8164553cc..06a64bb7f 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -253,7 +253,7 @@ nla_grobner::equation* nla_grobner::simplify_using_processed(equation* eq) { TRACE("grobner", tout << "simplifying: "; display_equation(tout, *eq); tout << "using already processed equalities of size " << m_to_superpose.size() << "\n";); do { simplified = false; - for (equation const* p : m_to_superpose) { + for (equation * p : m_to_superpose) { equation * new_eq = simplify_source_target(p, eq); if (new_eq) { result = true; @@ -271,7 +271,7 @@ nla_grobner::equation* nla_grobner::simplify_using_processed(equation* eq) { } -const nex_mul* nla_grobner::get_highest_monomial(const nex* e) const { +nex_mul* nla_grobner::get_highest_monomial(nex* e) const { switch (e->type()) { case expr_type::MUL: return to_mul(e); @@ -284,7 +284,7 @@ const nex_mul* nla_grobner::get_highest_monomial(const nex* e) const { // source 3f + k + l = 0, so f = (-k - l)/3 // target 2fg + 3fp + e = 0 // target is replaced by 2(-k/3 - l/3)g + 3(-k/3 - l/3)p + e = -2/3kg -2/3lg - kp -lp + e -bool nla_grobner::simplify_target_monomials(equation const * source, equation * target) { +bool nla_grobner::simplify_target_monomials(equation * source, equation * target) { const nex_mul * high_mon = get_highest_monomial(source->exp()); if (high_mon == nullptr) return false; @@ -398,7 +398,7 @@ bool nla_grobner::simplify_target_monomials_sum_j(equation const * source, equat } -nla_grobner::equation * nla_grobner::simplify_source_target(equation const * source, equation * target) { +nla_grobner::equation * nla_grobner::simplify_source_target(equation * source, equation * target) { TRACE("grobner", tout << "simplifying: "; display_equation(tout, *target); tout << "using: "; display_equation(tout, *source);); if (source->get_num_monomials() == 0) return nullptr; @@ -492,13 +492,64 @@ void nla_grobner::simplify_to_process(equation* eq) { // let eq1: ab+q=0, and eq2: ac+e=0, then qc - eb = 0 void nla_grobner::superpose(equation * eq1, equation * eq2) { TRACE("grobner", tout << "eq1="; display_equation(tout, *eq1) << "eq2="; display_equation(tout, *eq2);); - const nex_mul * ab = get_highest_monomial(eq1->exp()); - const nex_mul * ac = get_highest_monomial(eq2->exp()); + nex_mul * ab = get_highest_monomial(eq1->exp()); + nex_mul * ac = get_highest_monomial(eq2->exp()); + nex_mul *b, *c; TRACE("grobner", tout << "ab=" << *ab << " , " << " ac = " << *ac << "\n";); - - NOT_IMPLEMENTED_YET(); + if (!find_b_c(ab, ac, b, c)) { + return; + } + } +bool nla_grobner::find_b_c(nex_mul*ab, nex_mul* ac, nex_mul*& b, nex_mul*& c) { + if (!find_b_c_check(ab, ac)) + return false; + unsigned i = 0, j = 0; // i points to ab, j points to ac + b = m_nex_creator.mk_mul(); c = m_nex_creator.mk_mul(); + nex_pow* bp = ab->begin(); + nex_pow* cp = ac->begin(); + for (;;) { + if (m_nex_creator.lt(bp->e(), cp->e())) { + b->add_child_in_power(*bp); + if (++bp == ab->end()) + break; + } else if (m_nex_creator.lt(cp->e(), bp->e())) { + c->add_child_in_power(*cp); + if (++cp == ac->end()) + break; + } else { + NOT_IMPLEMENTED_YET(); + } + + } + NOT_IMPLEMENTED_YET(); + return true; +} + +bool nla_grobner::find_b_c_check(const nex_mul*ab, const nex_mul* ac) const { + SASSERT(m_nex_creator.is_simplified(ab) && m_nex_creator.is_simplified(ab)); + unsigned i = 0, j = 0; // i points to ab, j points to ac + for (;;) { + if (m_nex_creator.lt((*ab)[i].e(), (*ac)[j].e())) { + i++; + if (i == ab->size()) + return false; + } else if (m_nex_creator.lt((*ac)[j].e(), (*ab)[i].e())) { + j++; + if (j == ac->size()) + return false; + } else { + TRACE("grobner", tout << "found common " << *(*ac)[j].e() << " in " << *ab << " and " << *ac << "\n";); + return true; + } + } + + TRACE("grobner", tout << "not found common " << " in " << *ab << " and " << *ac << "\n";); + return false; +} + + void nla_grobner::superpose(equation * eq) { for (equation * target : m_to_superpose) { superpose(eq, target); diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index 1dd774d2b..ed74155bf 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -113,9 +113,9 @@ private: void compute_basis_init(); bool compute_basis_loop(); bool compute_basis_step(); - equation * simplify_source_target(equation const * source, equation * target); + equation * simplify_source_target(equation * source, equation * target); equation* simplify_using_processed(equation*); - bool simplify_target_monomials(equation const * source, equation * target); + bool simplify_target_monomials(equation * source, equation * target); void process_simplified_target(ptr_buffer& to_insert, equation* new_target, equation*& target, ptr_buffer& to_remove); bool simplify_processed_with_eq(equation*); void simplify_to_process(equation*); @@ -124,6 +124,8 @@ bool simplify_processed_with_eq(equation*); bool canceled() { return false; } // todo, implement void superpose(equation * eq1, equation * eq2); void superpose(equation * eq); + bool find_b_c(nex_mul*ab, nex_mul* ac, nex_mul*& b, nex_mul*& c); + bool find_b_c_check(const nex_mul*ab, const nex_mul* ac) const; bool is_trivial(equation* ) const; bool is_better_choice(equation * eq1, equation * eq2); void del_equations(unsigned old_size); @@ -148,7 +150,7 @@ bool simplify_processed_with_eq(equation*); void insert_to_process(equation *eq) { m_to_simplify.insert(eq); } void insert_processed(equation *eq) { m_to_superpose.insert(eq); } void simplify_equations_to_process(); - const nex_mul * get_highest_monomial(const nex * e) const; + nex_mul * get_highest_monomial(nex * e) const; ci_dependency* dep_from_vector( svector & fixed_vars_constraints); bool simplify_target_monomials_sum(equation const *, equation *, nex_sum*, const nex_mul*); bool simplify_target_monomials_sum_j(equation const *, equation *, nex_sum*, const nex_mul*, unsigned);