From 687f30a2ce346a5156fabf58438d38477a35c822 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 2 Dec 2019 09:14:22 -0800 Subject: [PATCH] debug grobner and improve printing Signed-off-by: Lev Nachmanson --- src/math/grobner/grobner.cpp | 1 + src/math/lp/lar_solver.cpp | 9 +++-- src/math/lp/lp_core_solver_base.h | 6 ++-- src/math/lp/nla_core.cpp | 7 +++- src/math/lp/nla_grobner.cpp | 59 +++++++++++++++++++++++++------ src/math/lp/nla_grobner.h | 3 ++ 6 files changed, 67 insertions(+), 18 deletions(-) diff --git a/src/math/grobner/grobner.cpp b/src/math/grobner/grobner.cpp index 95e30abeb..6ac88b719 100644 --- a/src/math/grobner/grobner.cpp +++ b/src/math/grobner/grobner.cpp @@ -847,6 +847,7 @@ void grobner::superpose(equation * eq1, equation * eq2) { if (new_monomials.empty()) return; m_num_new_equations++; + TRACE("grobner", tout << "success superposing\n";); equation * new_eq = alloc(equation); new_eq->m_monomials.swap(new_monomials); init_equation(new_eq, m_dep_manager.mk_join(eq1->m_dep, eq2->m_dep)); diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 2db4d920c..b0606a898 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1341,8 +1341,13 @@ std::string lar_solver::get_variable_name(var_index j) const { if (!s.empty()) { return s; } - - return std::string("v") + T_to_string(m_var_register.local_to_external(j)); + if (m_settings.m_print_external_var_name) { + return std::string("v") + T_to_string(m_var_register.local_to_external(j)); + } + else { + std::string s = column_corresponds_to_term(j)? "t":"v"; + return s + T_to_string(j); + } } // ********** print region start diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h index 09531f820..6b1f75e54 100644 --- a/src/math/lp/lp_core_solver_base.h +++ b/src/math/lp/lp_core_solver_base.h @@ -579,10 +579,8 @@ public: out << "[" << j << "] is not present\n"; return out; } - if (m_settings.m_print_external_var_name) - out << "[" << j << "],\tname = "<< column_name(j) << "\t"; - else - out << "v" << j << "= \t"; + + out << "[" << j << "]\t"; switch (m_column_types[j]) { case column_type::fixed: diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 1888c71e4..07aecf3e8 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -655,7 +655,12 @@ std::ostream & core::print_var(lpvar j, std::ostream & out) const { m_lar_solver.print_column_info(j, out); signed_var jr = m_evars.find(j); - out << "root=" << (jr.sign()? "-v":"v") << jr.var() << "\n"; + out << "root="; + if (jr.sign()) { + out << "-"; + } + + out << m_lar_solver.get_variable_name(jr.var()) << "\n"; return out; } diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index f3df0270b..3ec540496 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -469,6 +469,9 @@ void nla_grobner::process_simplified_target(ptr_buffer& to_insert, equ to_remove.push_back(target); } } +} + +void nla_grobner::check_eq(equation* target) { if(m_intervals->check_cross_nested_expr(target->exp(), target->dep())) { TRACE("grobner", tout << "created a lemma for "; display_equation(tout, *target) << "\n"; tout << "vars = \n"; @@ -581,9 +584,6 @@ void nla_grobner::superpose(equation * eq1, equation * eq2) { } equation* eq = alloc(equation); init_equation(eq, expr_superpose( eq1->exp(), eq2->exp(), ab, ac, b, c), m_dep_manager.mk_join(eq1->dep(), eq2->dep())); - if(m_intervals->check_cross_nested_expr(eq->exp(), eq->dep())) { - register_report(); - } insert_to_simplify(eq); } @@ -678,8 +678,10 @@ void nla_grobner::superpose(equation * eq) { bool nla_grobner::compute_basis_step() { equation * eq = pick_next(); - if (!eq) + if (!eq) { + TRACE("grobner", tout << "cannot pick an equation\n";); return true; + } m_stats.m_num_processed++; equation * new_eq = simplify_using_processed(eq); if (new_eq != nullptr && eq != new_eq) { @@ -701,6 +703,14 @@ void nla_grobner::compute_basis(){ compute_basis_init(); if (!compute_basis_loop()) { set_gb_exhausted(); + } else { + TRACE("grobner", tout << "m_to_simplify.size() = " << m_to_simplify.size() << " , m_to_superpose.size() == " << m_to_superpose.size() << "\n";); + for (equation* e : m_to_simplify) { + check_eq(e); + } + for (equation* e : m_to_superpose) { + check_eq(e); + } } } void nla_grobner::compute_basis_init(){ @@ -731,9 +741,13 @@ bool nla_grobner::done() const { bool nla_grobner::compute_basis_loop(){ while (!done()) { - if (compute_basis_step()) + if (compute_basis_step()) { + TRACE("grobner", tout << "progress in compute_basis_step\n";); return true; + } + TRACE("grobner", tout << "continue compute_basis_loop\n";); } + TRACE("grobner", tout << "return false from compute_basis_loop\n";); return false; } @@ -799,20 +813,43 @@ void nla_grobner::display_equations(std::ostream & out, equation_set const & v, } std::ostream& nla_grobner::display_equation(std::ostream & out, const equation & eq) const { - out << "m_exp = " << *eq.exp() << "\n"; - out << "dep = "; display_dependency(out, eq.dep()) << "\n"; + out << "expr = " << *eq.exp() << "\n"; + out << "deps = "; display_dependency(out, eq.dep()) << "\n"; return out; } +std::unordered_set nla_grobner::get_vars_of_expr_with_opening_terms(const nex *e ) { + auto ret = get_vars_of_expr(e); + auto & ls = c().m_lar_solver; + do { + svector added; + for (lpvar j : ret) { + if (ls.column_corresponds_to_term(j)) { + const auto & t = c().m_lar_solver.get_term(ls.local_to_external(j)); + for (auto p : t) { + if (ret.find(p.var()) == ret.end()) + added.push_back(p.var()); + } + } + } + if (added.size() == 0) + return ret; + for (lpvar j: added) + ret.insert(j); + added.clear(); + } while (true); +} void nla_grobner::assert_eq_0(nex* e, ci_dependency * dep) { if (e == nullptr || is_zero_scalar(e)) return; equation * eq = alloc(equation); init_equation(eq, e, dep); - TRACE("grobner", display_equation(tout, *eq); - for (unsigned j : get_vars_of_expr(e)) { - c().print_var(j, tout) << "\n"; - }); + TRACE("grobner", + display_equation(tout, *eq); + for (unsigned j : get_vars_of_expr_with_opening_terms(e)) { + tout << "("; + c().print_var(j, tout) << ")\n"; + }); insert_to_simplify(eq); } diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index ca73becbb..29e72510c 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -145,6 +145,7 @@ private: std::ostream& display_dependency(std::ostream& out, ci_dependency*) const; void insert_to_simplify(equation *eq) { + TRACE("nla_grobner", display_equation(tout, *eq);); SASSERT(!eq->exp()->is_scalar() || to_scalar(eq->exp())->value().is_zero()); m_to_simplify.insert(eq); } @@ -167,6 +168,8 @@ private: nex * expr_superpose(nex* e1, nex* e2, const nex* ab, const nex* ac, nex_mul* b, nex_mul* c); void add_mul_skip_first(nex_sum* r, const rational& beta, nex *e, nex_mul* c); bool done() const; + void check_eq(equation*); void register_report(); + std::unordered_set get_vars_of_expr_with_opening_terms(const nex *e ); }; // end of grobner }