From 87cc5c8d96c379eaa7f954e2eb62a4241fbd1396 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 5 Jul 2019 14:35:40 -0700 Subject: [PATCH] fix a bug in nla_expr Signed-off-by: Lev Nachmanson --- src/math/lp/explanation.h | 4 ++++ src/math/lp/lar_solver.cpp | 16 ++++++++++++++++ src/math/lp/lar_solver.h | 4 ++++ src/math/lp/nla_core.cpp | 15 ++++++++++----- src/math/lp/nla_core.h | 4 +++- src/math/lp/nla_intervals.cpp | 26 +++++++++++--------------- 6 files changed, 48 insertions(+), 21 deletions(-) diff --git a/src/math/lp/explanation.h b/src/math/lp/explanation.h index 62b21aa0d..1ed7a5947 100644 --- a/src/math/lp/explanation.h +++ b/src/math/lp/explanation.h @@ -25,6 +25,10 @@ class explanation { vector> m_explanation; std::unordered_set m_set_of_ci; public: + explanation() {} + template + explanation(const T& t) { for ( unsigned c : t) add(c); } + void clear() { m_explanation.clear(); m_set_of_ci.clear(); } vector>::const_iterator begin() const { return m_explanation.begin(); } vector>::const_iterator end() const { return m_explanation.end(); } diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 3ebfab0a7..a40cc7852 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1361,6 +1361,16 @@ std::ostream& lar_solver::print_constraint_indices_only(constraint_index ci, std return print_constraint_indices_only(m_constraints[ci], out); } +std::ostream& lar_solver::print_constraint_indices_only_customized(constraint_index ci, std::function var_str, std::ostream & out) const { + if (ci >= m_constraints.size()) { + out << "constraint " << T_to_string(ci) << " is not found"; + out << std::endl; + return out; + } + + return print_constraint_indices_only_customized(m_constraints[ci], var_str, out); +} + std::ostream& lar_solver::print_constraints(std::ostream& out) const { out << "number of constraints = " << m_constraints.size() << std::endl; for (auto c : m_constraints) { @@ -1443,6 +1453,12 @@ std::ostream& lar_solver::print_constraint_indices_only(const lar_base_constrain return out << " " << lconstraint_kind_string(c->m_kind) << " " << c->m_right_side << std::endl; } +std::ostream& lar_solver::print_constraint_indices_only_customized(const lar_base_constraint * c, + std::function var_str, std::ostream & out) const { + print_linear_combination_customized(c->coeffs(), var_str, out); + return out << " " << lconstraint_kind_string(c->m_kind) << " " << c->m_right_side << std::endl; +} + void lar_solver::fill_var_set_for_random_update(unsigned sz, var_index const * vars, vector& column_list) { for (unsigned i = 0; i < sz; i++) { var_index var = vars[i]; diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 17f1d48ea..b06bb33a2 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -505,6 +505,10 @@ public: std::ostream& print_constraint_indices_only(constraint_index ci, std::ostream & out) const; + std::ostream& print_constraint_indices_only_customized(constraint_index ci, std::function var_str, std::ostream & out) const; + + std::ostream& print_constraint_indices_only_customized(const lar_base_constraint * c, std::function var_str, std::ostream & out) const; + std::ostream& print_terms(std::ostream& out) const; std::ostream& print_left_side_of_constraint(const lar_base_constraint * c, std::ostream & out) const; diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 9f96a2e76..46ecda77f 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -277,7 +277,9 @@ std::ostream& core::print_explanation(const lp::explanation& exp, std::ostream& out << "expl: "; for (auto &p : exp) { out << "(" << p.second << ")"; - m_lar_solver.print_constraint_indices_only(p.second, out); + m_lar_solver.print_constraint_indices_only_customized(p.second, + [this](lpvar j) { return var_str(j);}, + out); out << " "; } out << "\n"; @@ -1397,13 +1399,16 @@ std::ostream& core::print_terms(std::ostream& out) const { } return out; } + +std::string core::var_str(lpvar j) const { + return is_monomial_var(j)? + (product_indices_str(m_emons[j].vars()) + (check_monomial(m_emons[j])? "": "_")) : (std::string("v") + lp::T_to_string(j)); +} + std::ostream& core::print_term( const lp::lar_term& t, std::ostream& out) const { return lp::print_linear_combination_customized( t.coeffs_as_vector(), - [this](lpvar j) { - return is_monomial_var(j)? - (product_indices_str(m_emons[j].vars()) + (check_monomial(m_emons[j])? "": "_")) : (std::string("v") + lp::T_to_string(j)); - }, + [this](lpvar j) { return var_str(j); }, out); } } // end of nla diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 04a1b7f91..3d9eba088 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -172,6 +172,8 @@ public: std::ostream& print_product(const T & m, std::ostream& out) const; template std::string product_indices_str(const T & m) const; + std::string var_str(lpvar) const; + std::ostream & print_factor(const factor& f, std::ostream& out) const; std::ostream & print_factor_with_vars(const factor& f, std::ostream& out) const; std::ostream& print_monomial(const monomial& m, std::ostream& out) const; @@ -187,7 +189,7 @@ public: void print_monomial_stats(const monomial& m, std::ostream& out); void print_stats(std::ostream& out); std::ostream& print_lemma(std::ostream& out) const; - + void print_specific_lemma(const lemma& l, std::ostream& out) const; diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index ed3abdced..b0fb6a51e 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -126,17 +126,19 @@ std::ostream& intervals::display(std::ostream& out, const interval& i) const { } svector expl; m_dep_manager.linearize(i.m_lower_dep, expl); - out << "\nlower constraints (\n"; - for (lp::constraint_index c: expl) - m_core->m_lar_solver.print_constraint_indices_only(c, out); - out << ")\n"; - expl.clear(); + { + lp::explanation e(expl); + out << "\nlower constraints\n"; + m_core->print_explanation(e, out); + expl.clear(); + } m_dep_manager.linearize(i.m_upper_dep, expl); - out << "upper constraints (\n"; - for (lp::constraint_index c: expl) - m_core->m_lar_solver.print_constraint_indices_only(c, out); + { + lp::explanation e(expl); + out << "\n)\nupper constraints (\n"; + m_core->print_explanation(e, out); + } out << ")\n"; - return out; } @@ -144,12 +146,6 @@ lp::lar_solver& intervals::ls() { return m_core->m_lar_solver; } const lp::lar_solver& intervals::ls() const { return m_core->m_lar_solver; } -std::ostream& intervals::print_explanations(const svector &expl , std::ostream& out) const { - out << "interv expl:\n "; - for (auto ci : expl) - m_core->m_lar_solver.print_constraint_indices_only(ci, out); - return out; -} } // end of nla namespace