From 130995a3db793cefb402d85431fa66b0fa8165ab Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 20 Jun 2019 12:57:48 -0700 Subject: [PATCH] print terms as monomials Signed-off-by: Lev Nachmanson --- src/math/lp/emonomials.cpp | 2 +- src/math/lp/gomory.cpp | 2 +- src/math/lp/lar_solver.cpp | 2 +- src/math/lp/lp_utils.h | 81 +++++++++++++++---------------- src/math/lp/nla_basics_lemmas.cpp | 22 ++++----- src/math/lp/nla_core.cpp | 38 +++++++++++---- src/math/lp/nla_core.h | 14 ++++-- src/math/lp/nla_order_lemmas.cpp | 14 +++--- src/math/lp/nla_solver.cpp | 5 -- src/math/lp/nla_solver.h | 1 - 10 files changed, 99 insertions(+), 82 deletions(-) diff --git a/src/math/lp/emonomials.cpp b/src/math/lp/emonomials.cpp index 3f93a7309..d7b464ce9 100644 --- a/src/math/lp/emonomials.cpp +++ b/src/math/lp/emonomials.cpp @@ -397,7 +397,7 @@ std::ostream& emonomials::display(const core& cr, std::ostream& out) const { out << "monomials\n"; unsigned idx = 0; for (auto const& m : m_monomials) { - out << "m" << (idx++) << ": " << pp_rmon(cr, m) << "\n"; + out << "m" << (idx++) << ": " << pp_mon_with_vars(cr, m) << "\n"; } return display_use(out); } diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index aa12e3efd..ea7914b5a 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -310,7 +310,7 @@ public: lp_assert(m_int_solver.current_solution_is_inf_on_cut()); TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout);); m_int_solver.m_lar_solver->subs_term_columns(m_t); - TRACE("gomory_cut", print_linear_combination_of_column_indices_only(m_t, tout << "gomory cut:"); tout << " <= " << m_k << std::endl;); + TRACE("gomory_cut", print_linear_combination_of_column_indices_only(m_t.coeffs_as_vector(), tout << "gomory cut:"); tout << " <= " << m_k << std::endl;); return lia_move::cut; } diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index a7ce4ebb5..3ebfab0a7 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1418,7 +1418,7 @@ std::ostream& lar_solver::print_term(lar_term const& term, std::ostream & out) c } std::ostream& lar_solver::print_term_as_indices(lar_term const& term, std::ostream & out) const { - print_linear_combination_of_column_indices_only(term, out); + print_linear_combination_of_column_indices_only(term.coeffs_as_vector(), out); return out; } diff --git a/src/math/lp/lp_utils.h b/src/math/lp/lp_utils.h index 900ab47f8..f0e9fe5af 100644 --- a/src/math/lp/lp_utils.h +++ b/src/math/lp/lp_utils.h @@ -77,52 +77,51 @@ bool is_non_decreasing(const K& v) { return true; } +template +std::ostream& print_linear_combination_customized(const vector> & coeffs, std::function var_str, std::ostream & out) { + bool first = true; + for (const auto & it : coeffs) { + T val = it.first; + if (first) { + first = false; + if (val.is_neg()) { + out << "- "; + val = -val; + } + } else { + if (val.is_pos()) { + out << " + "; + } else { + out << " - "; + val = -val; + } + } + if (val == 1) + out << " "; + else { + out << T_to_string(val); + } + out << var_str(it.second); + } + return out; +} + template -void print_linear_combination_of_column_indices_only(const T & coeffs, std::ostream & out) { - bool first = true; - for (const auto & it : coeffs) { - auto val = it.coeff(); - if (first) { - first = false; - } else { - if (val.is_pos()) { - out << " + "; - } else { - out << " - "; - val = -val; - } - } - if (val == 1) - out << " "; - else - out << T_to_string(val); - - out << "v" << it.var(); - } +std::ostream& print_linear_combination_of_column_indices_only(const vector> & coeffs, std::ostream & out) { + return print_linear_combination_customized( + coeffs, + [](unsigned j) {std::stringstream ss; ss << "v" << j; return ss.str();}, + out); } -template -void print_linear_combination_of_column_indices_only(const vector> & coeffs, std::ostream & out) { - bool first = true; +template +std::ostream& print_linear_combination_indices_only(const T & coeffs, std::ostream & out) { + vector> cfs; + for (const auto & it : coeffs) { - auto val = it.first; - if (first) { - first = false; - } else { - if (val.is_pos()) { - out << " + "; - } else { - out << " - "; - val = -val; - } - } - if (val == 1) - out << " "; - else - out << T_to_string(val); - - out << "v" << it.second; + cfs.push_back(std::make_pair(it.coeff(), it.var())); } + return print_linear_combination_of_column_indices_only(cfs, out); } inline void throw_exception(std::string && str) { diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp index d1497644e..bbb5bce12 100644 --- a/src/math/lp/nla_basics_lemmas.cpp +++ b/src/math/lp/nla_basics_lemmas.cpp @@ -121,16 +121,16 @@ bool basics::basic_sign_lemma_on_mon(lpvar v, std::unordered_set & exp if (!try_insert(v, explored)) { return false; } - const monomial& m_v = c().m_emons[v]; - TRACE("nla_solver", tout << "m_v = " << pp_rmon(c(), m_v);); - CTRACE("nla_solver", !c().m_emons.is_canonized(m_v), - c().m_emons.display(c(), tout); + const monomial& m_v = c().emons()[v]; + TRACE("nla_solver", tout << "m_v = " << pp_mon_with_vars(c(), m_v);); + CTRACE("nla_solver", !c().emons().is_canonized(m_v), + c().emons().display(c(), tout); c().m_evars.display(tout); ); - SASSERT(c().m_emons.is_canonized(m_v)); + SASSERT(c().emons().is_canonized(m_v)); - for (auto const& m : c().m_emons.enum_sign_equiv_monomials(v)) { - TRACE("nla_solver_details", tout << "m = " << pp_rmon(c(), m);); + for (auto const& m : c().emons().enum_sign_equiv_monomials(v)) { + TRACE("nla_solver_details", tout << "m = " << pp_mon_with_vars(c(), m);); SASSERT(m.rvars() == m_v.rvars()); if (m_v.var() != m.var() && basic_sign_lemma_on_two_monomials(m_v, m) && done()) return true; @@ -160,8 +160,8 @@ bool basics::basic_sign_lemma(bool derived) { void basics::generate_sign_lemma(const monomial& m, const monomial& n, const rational& sign) { add_empty_lemma(); TRACE("nla_solver", - tout << "m = " << pp_rmon(_(), m); - tout << "n = " << pp_rmon(_(), n); + tout << "m = " << pp_mon_with_vars(_(), m); + tout << "n = " << pp_mon_with_vars(_(), n); ); c().mk_ineq(m.var(), -sign, n.var(), llc::EQ); explain(m); @@ -704,7 +704,7 @@ void basics::basic_lemma_for_mon_neutral_model_based(const monomial& rm, const f bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const monomial& m, const factorization& f) { rational sign = sign_to_rat(m.rsign()); SASSERT(m.rsign() == canonize_sign(f)); - TRACE("nla_solver_bl", tout << pp_rmon(_(), m) <<"\nf = "; c().print_factorization(f, tout); tout << "sign = " << sign << '\n'; ); + TRACE("nla_solver_bl", tout << pp_mon_with_vars(_(), m) <<"\nf = "; c().print_factorization(f, tout); tout << "sign = " << sign << '\n'; ); lpvar not_one = -1; for (auto j : f){ TRACE("nla_solver_bl", tout << "j = "; c().print_factor_with_vars(j, tout);); @@ -760,7 +760,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(co explain(f); TRACE("nla_solver", c().print_lemma(tout); - tout << "m = " << pp_rmon(c(), m); + tout << "m = " << pp_mon_with_vars(c(), m); ); return true; } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 4ab91779d..9512ccb26 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -189,6 +189,19 @@ std::ostream& core::print_product(const T & m, std::ostream& out) const { } return out; } +template +std::string core::product_indices_str(const T & m) const { + std::stringstream out; + bool first = true; + for (lpvar v : m) { + if (!first) + out << "*"; + else + first = false; + out << "v" << v;; + } + return out.str(); +} std::ostream & core::print_factor(const factor& f, std::ostream& out) const { if (f.sign()) @@ -209,7 +222,7 @@ std::ostream & core::print_factor_with_vars(const factor& f, std::ostream& out) print_var(f.var(), out); } else { - out << " MON = " << pp_rmon(*this, m_emons[f.var()]); + out << " MON = " << pp_mon_with_vars(*this, m_emons[f.var()]); } return out; } @@ -1184,7 +1197,7 @@ bool core::find_bfc_to_refine_on_monomial(const monomial& m, factorization & bf) if (val(m) != val(a) * val(b)) { bf = f; TRACE("nla_solver", tout << "found bf"; - tout << ":m:" << pp_rmon(*this, m) << "\n"; + tout << ":m:" << pp_mon_with_vars(*this, m) << "\n"; tout << "bf:"; print_bfc(bf, tout);); return true; @@ -1254,6 +1267,7 @@ bool core:: done() const { } lbool core:: inner_check(bool derived) { + TRACE("nla_cn", print_terms(tout);); for (int search_level = 0; search_level < 3 && !done(); search_level++) { TRACE("nla_solver", tout << "derived = " << derived << ", search_level = " << search_level << "\n";); if (search_level == 0) { @@ -1342,11 +1356,17 @@ lbool core::test_check( return check(l); } -} // end of nla - - -#if 0 -rational core::mon_value_by_vars(unsigned i) const { - return product_value(m_monomials[i]); +std::ostream& core::print_terms(std::ostream& out) const { + for (auto t: m_lar_solver.m_terms) + print_term(*t, out) << "\n"; + return out; } -#endif +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()) : (std::string("v") + lp::T_to_string(j)); + }, + out); +} +} // end of nla diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index d90c0808a..cd8e2ed30 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -162,7 +162,9 @@ public: std::ostream & print_ineqs(const lemma& l, std::ostream & out) const; std::ostream & print_factorization(const factorization& f, std::ostream& out) const; template - std::ostream& print_product(const T & m, std::ostream& out) const; + std::ostream& print_product(const T & m, std::ostream& out) const; + template + std::string product_indices_str(const T & m) 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; @@ -341,6 +343,8 @@ public: lbool test_check(vector& l); lpvar map_to_root(lpvar) const; + std::ostream& print_terms(std::ostream&) const; + std::ostream& print_term( const lp::lar_term&, std::ostream&) const; }; // end of core struct pp_mon { @@ -349,14 +353,14 @@ struct pp_mon { pp_mon(core const& c, monomial const& m): c(c), m(m) {} pp_mon(core const& c, lpvar v): c(c), m(c.m_emons[v]) {} }; -struct pp_rmon { +struct pp_mon_with_vars { core const& c; monomial const& m; - pp_rmon(core const& c, monomial const& m): c(c), m(m) {} - pp_rmon(core const& c, lpvar v): c(c), m(c.m_emons[v]) {} + pp_mon_with_vars(core const& c, monomial const& m): c(c), m(m) {} + pp_mon_with_vars(core const& c, lpvar v): c(c), m(c.emons()[v]) {} }; inline std::ostream& operator<<(std::ostream& out, pp_mon const& p) { return p.c.print_monomial(p.m, out); } -inline std::ostream& operator<<(std::ostream& out, pp_rmon const& p) { return p.c.print_monomial_with_vars(p.m, out); } +inline std::ostream& operator<<(std::ostream& out, pp_mon_with_vars const& p) { return p.c.print_monomial_with_vars(p.m, out); } struct pp_fac { core const& c; diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index 059d5de22..74e98fb3a 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -66,7 +66,7 @@ void order::order_lemma_on_monomial(const monomial& m) { // a > b && c > 0 => ac > bc, // with either variable of ac playing the role of c void order::order_lemma_on_binomial(const monomial& ac) { - TRACE("nla_solver", tout << pp_rmon(c(), ac);); + TRACE("nla_solver", tout << pp_mon_with_vars(c(), ac);); SASSERT(!check_monomial(ac) && ac.size() == 2); const rational mult_val = val(ac.vars()[0]) * val(ac.vars()[1]); const rational acv = val(ac); @@ -101,13 +101,13 @@ void order::order_lemma_on_binomial_sign(const monomial& xy, lpvar x, lpvar y, i // We look for monomials e = m.rvars()[k]*d and see if we can create an order lemma for m and e void order::order_lemma_on_factor_binomial_explore(const monomial& ac, bool k) { - TRACE("nla_solver", tout << "ac = " << pp_rmon(c(), ac);); + TRACE("nla_solver", tout << "ac = " << pp_mon_with_vars(c(), ac);); SASSERT(ac.size() == 2); lpvar c = ac.vars()[k]; for (monomial const& bd : _().m_emons.get_products_of(c)) { if (bd.var() == ac.var()) continue; - TRACE("nla_solver", tout << "bd = " << pp_rmon(_(), bd);); + TRACE("nla_solver", tout << "bd = " << pp_mon_with_vars(_(), bd);); order_lemma_on_factor_binomial_rm(ac, k, bd); if (done()) { break; @@ -119,9 +119,9 @@ void order::order_lemma_on_factor_binomial_explore(const monomial& ac, bool k) { // create order lemma on monomials bd where d is equivalent to ac[k] void order::order_lemma_on_factor_binomial_rm(const monomial& ac, bool k, const monomial& bd) { TRACE("nla_solver", - tout << "ac=" << pp_rmon(_(), ac) << "\n"; + tout << "ac=" << pp_mon_with_vars(_(), ac) << "\n"; tout << "k=" << k << "\n"; - tout << "bd=" << pp_rmon(_(), bd) << "\n"; + tout << "bd=" << pp_mon_with_vars(_(), bd) << "\n"; ); factor d(_().m_evars.find(ac.vars()[k]).var(), factor_type::VAR); factor b(false); @@ -204,8 +204,8 @@ bool order::order_lemma_on_ac_and_bc(const monomial& rm_ac, bool k, const monomial& rm_bd) { TRACE("nla_solver", - tout << "rm_ac = " << pp_rmon(_(), rm_ac) << "\n"; - tout << "rm_bd = " << pp_rmon(_(), rm_bd) << "\n"; + tout << "rm_ac = " << pp_mon_with_vars(_(), rm_ac) << "\n"; + tout << "rm_bd = " << pp_mon_with_vars(_(), rm_bd) << "\n"; tout << "ac_f[k] = "; c().print_factor_with_vars(ac_f[k], tout);); factor b(false); diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index 848631af9..3a7ab7c51 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -47,11 +47,6 @@ void solver::push(){ void solver::pop(unsigned n) { m_core->pop(n); } - - std::ostream& solver::display(std::ostream& out) { - return m_core->print_monomials(out); - } - solver::solver(lp::lar_solver& s): m_core(alloc(core, s, m_res_limit)) { } diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index 0f9c88ac0..1c3705533 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -43,7 +43,6 @@ public: void pop(unsigned scopes); bool need_check(); lbool check(vector&); - std::ostream& display(std::ostream& out); bool is_monomial_var(lpvar) const; }; }