From 9661f752463ae767572961e0580448f811f977ce Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 13 Dec 2019 20:43:22 -1000 Subject: [PATCH] add an assert test_find_b_c() Signed-off-by: Lev Nachmanson --- src/math/lp/nla_grobner.cpp | 24 ++++++++++++++++++++---- src/math/lp/nla_grobner.h | 8 +++++--- 2 files changed, 25 insertions(+), 7 deletions(-) diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 44b956d1f..fe6bc0e5c 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -429,7 +429,9 @@ bool grobner::simplify_source_target(equation * source, equation * target) { TRACE("grobner_d", tout << "no simplification\n";); return false; } - + + + void grobner::process_simplified_target(equation* target, ptr_buffer& to_remove) { if (is_trivial(target)) { to_remove.push_back(target); @@ -597,6 +599,7 @@ bool grobner::find_b_c(const nex* ab, const nex* ac, nex_mul*& b, nex_mul*& c) { nex_mul *a = divide_ignore_coeffs_perform(m_nex_creator.clone(ab), b); SASSERT(ab->get_degree() == a->get_degree() + b->get_degree()); SASSERT(ac->get_degree() == a->get_degree() + c->get_degree()); + SASSERT(test_find_b_c(ab, ac, b, c)); return true; } @@ -700,11 +703,9 @@ bool grobner::compute_basis_loop(){ while (!done()) { if (compute_basis_step()) { TRACE("grobner", tout << "progress in compute_basis_step\n";); - TRACE("grobner_stats", print_stats(tout);); return true; } TRACE("grobner", tout << "continue compute_basis_loop\n";); - TRACE("grobner_stats", print_stats(tout);); } TRACE("grobner", tout << "return false from compute_basis_loop\n";); TRACE("grobner_stats", print_stats(tout);); @@ -816,4 +817,19 @@ std::ostream& grobner::display_dependency(std::ostream& out, ci_dependency* dep) } return out; } - +#ifdef Z3DEBUG +bool grobner::test_find_b(const nex* ab, const nex_mul* b) { + nex_mul& ab_clone = m_nex_creator.clone(ab)->to_mul(); + nex_mul * a= divide_ignore_coeffs_perform(&ab_clone, b); + ab_clone.coeff() = rational(1); + SASSERT(b->coeff().is_one()); + nex * m = m_nex_creator.mk_mul(a, m_nex_creator.clone(b)); + m = m_nex_creator.simplify(m); + return m_nex_creator.equal(m, &ab_clone); +} + +bool grobner::test_find_b_c(const nex* ab, const nex* ac, const nex_mul* b, const nex_mul* c) { + return test_find_b(ab, b) && test_find_b(ac, c); +} + +#endif diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index 749e2f471..575cb5be0 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -160,8 +160,10 @@ private: std::unordered_set get_vars_of_expr_with_opening_terms(const nex *e ); unsigned num_of_equations() const { return m_to_simplify.size() + m_to_superpose.size(); } std::ostream& print_stats(std::ostream&) const; - template - std::ostream& print_stats_eqs(T&, std::ostream&) const; - void update_stats_max_degree_and_size(const equation *e); + void update_stats_max_degree_and_size(const equation*); +#ifdef Z3DEBUG + bool test_find_b_c(const nex* ab, const nex* ac, const nex_mul* b, const nex_mul* c); + bool test_find_b(const nex* ab, const nex_mul* b); +#endif }; // end of grobner }