From 82bf62f5fadacc4c5d897096591baa267e3e86b8 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 27 Apr 2019 17:21:53 -0700 Subject: [PATCH] removed calls to settings.random_next() from assert statements Signed-off-by: Lev Nachmanson --- src/util/lp/emonomials.cpp | 5 +++-- src/util/lp/emonomials.h | 15 +++++++++++++-- src/util/lp/lar_core_solver_def.h | 3 +-- src/util/lp/lp_core_solver_base.h | 4 ++++ src/util/lp/monomial.h | 11 ----------- src/util/lp/nla_basics_lemmas.cpp | 2 +- src/util/lp/nla_core.cpp | 6 ++---- src/util/lp/static_matrix.h | 5 ++++- 8 files changed, 28 insertions(+), 23 deletions(-) diff --git a/src/util/lp/emonomials.cpp b/src/util/lp/emonomials.cpp index 5434ef6b0..78c1f8909 100644 --- a/src/util/lp/emonomials.cpp +++ b/src/util/lp/emonomials.cpp @@ -21,6 +21,7 @@ #include "util/lp/emonomials.h" #include "util/lp/nla_defs.h" +#include "util/lp/nla_core.h" namespace nla { @@ -339,11 +340,11 @@ namespace nla { } } - std::ostream& emonomials::display(std::ostream& out) const { +std::ostream& emonomials::display(const core& cr, std::ostream& out) const { out << "monomials\n"; unsigned idx = 0; for (auto const& m : m_monomials) { - out << (idx++) << ": " << m << "\n"; + out << (idx++) << ": " << pp_mon(cr, m) << "\n"; } out << "use lists\n"; idx = 0; diff --git a/src/util/lp/emonomials.h b/src/util/lp/emonomials.h index 915699141..64528e1b5 100644 --- a/src/util/lp/emonomials.h +++ b/src/util/lp/emonomials.h @@ -27,6 +27,8 @@ namespace nla { +class core; + class emonomials : public var_eqs_merge_handler { mutable svector m_find_key; /** @@ -275,7 +277,7 @@ public: /** \brief display state of emonomials */ - std::ostream& display(std::ostream& out) const; + std::ostream& display(const core&, std::ostream& out) const; /** \brief @@ -291,6 +293,15 @@ public: bool is_monomial_var(lpvar v) const { return m_var2index.get(v, UINT_MAX) != UINT_MAX; } }; -inline std::ostream& operator<<(std::ostream& out, emonomials const& m) { return m.display(out); } +struct pp_emons { + const core& m_c; + const emonomials& m_em; + pp_emons(const core& c, const emonomials& e): m_c(c), m_em(e) {} + inline std::ostream& display(std::ostream& out) const { + return m_em.display(m_c, out); + } +}; + +inline std::ostream& operator<<(std::ostream& out, pp_emons const& p) { return p.display(out); } } diff --git a/src/util/lp/lar_core_solver_def.h b/src/util/lp/lar_core_solver_def.h index 476e11698..7c54a3b6b 100644 --- a/src/util/lp/lar_core_solver_def.h +++ b/src/util/lp/lar_core_solver_def.h @@ -300,10 +300,9 @@ void lar_core_solver::solve() { if (snapped) m_r_solver.solve_Ax_eq_b(); } - if (m_r_solver.m_look_for_feasible_solution_only) + if (m_r_solver.m_look_for_feasible_solution_only) //todo : should it be set? m_r_solver.find_feasible_solution(); else { - TRACE("lar_solver", tout << "solve\n";); m_r_solver.solve(); } lp_assert(!settings().use_tableau() || r_basis_is_OK()); diff --git a/src/util/lp/lp_core_solver_base.h b/src/util/lp/lp_core_solver_base.h index 425013eb0..081b7124a 100644 --- a/src/util/lp/lp_core_solver_base.h +++ b/src/util/lp/lp_core_solver_base.h @@ -575,6 +575,10 @@ public: } std::ostream& print_column_info(unsigned j, std::ostream & out) const { + if (j >= m_lower_bounds.size()) { + out << "[" << j << "] is not present\n"; + return out; + } out << "[" << j << "],\tname = "<< column_name(j) << "\t"; switch (m_column_types[j]) { case column_type::fixed: diff --git a/src/util/lp/monomial.h b/src/util/lp/monomial.h index 15cdf9499..206028fb3 100644 --- a/src/util/lp/monomial.h +++ b/src/util/lp/monomial.h @@ -68,19 +68,8 @@ public: void sort_rvars() { std::sort(m_rvars.begin(), m_rvars.end()); } - std::ostream& display(std::ostream& out) const { - // out << "v" << var() << " := "; - // if (sign()) out << "- "; - // for (lpvar v : vars()) out << "v" << v << " "; - SASSERT(false); - return out; - } }; -inline std::ostream& operator<<(std::ostream& out, monomial const& m) { - SASSERT(false); - return m.display(out); -} typedef std::unordered_map variable_map_type; template diff --git a/src/util/lp/nla_basics_lemmas.cpp b/src/util/lp/nla_basics_lemmas.cpp index 393852d58..3adde59f9 100644 --- a/src/util/lp/nla_basics_lemmas.cpp +++ b/src/util/lp/nla_basics_lemmas.cpp @@ -30,7 +30,7 @@ bool basics::basic_sign_lemma_on_two_monomials(const monomial& m, const monomial const rational& sign = m.rsign() * n.rsign(); if (val(m) == val(n) * sign) return false; - TRACE("nla_solver", tout << "sign contradiction:\nm = " << m << "n= " << n << "sign: " << sign << "\n";); + TRACE("nla_solver", tout << "sign contradiction:\nm = " << pp_mon(c(), m) << "n= " << pp_mon(c(), n) << "sign: " << sign << "\n";); generate_sign_lemma(m, n, sign); return true; } diff --git a/src/util/lp/nla_core.cpp b/src/util/lp/nla_core.cpp index 79451ed2b..0a587dcd3 100644 --- a/src/util/lp/nla_core.cpp +++ b/src/util/lp/nla_core.cpp @@ -1277,11 +1277,8 @@ void core::add_equivalence_maybe(const lp::lar_term *t, lpci c0, lpci c1) { // x is equivalent to y if x = +- y void core::init_vars_equivalence() { - /* SASSERT(m_evars.empty());*/ collect_equivs(); - /* TRACE("nla_solver_details", tout << "number of equivs = " << m_evars.size(););*/ - - SASSERT((settings().random_next() % 100) || tables_are_ok()); + // SASSERT(tables_are_ok()); } bool core:: tables_are_ok() const { @@ -1339,6 +1336,7 @@ void core::init_search() { } void core::init_to_refine() { + TRACE("nla_solver", tout << "emons:" << pp_emons(*this, m_emons);); m_to_refine.clear(); for (auto const & m : m_emons) if (!check_monomial(m)) diff --git a/src/util/lp/static_matrix.h b/src/util/lp/static_matrix.h index 1a0ee1bdc..1bf0c4afb 100644 --- a/src/util/lp/static_matrix.h +++ b/src/util/lp/static_matrix.h @@ -48,7 +48,10 @@ struct row_cell { unsigned & offset() { return m_offset;} }; - +template +std::ostream& operator<<(std::ostream& out, const row_cell& rc) { + return out << "(m_j=" << rc.m_j << ", m_offset= " << rc.m_offset << ", m_value=" << rc.m_value << ")"; +} struct empty_struct {}; typedef row_cell column_cell;