From 1490b7a15fc7a292d7774ce99c7874322e4f36f9 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 19 Jul 2017 22:14:05 -0700 Subject: [PATCH] a cleaner version of subs_term_columns Signed-off-by: Lev Nachmanson --- src/util/lp/int_solver.cpp | 2 +- src/util/lp/lar_solver.h | 8 +++++--- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp index 349393cc3..793663bf1 100644 --- a/src/util/lp/int_solver.cpp +++ b/src/util/lp/int_solver.cpp @@ -281,7 +281,7 @@ lia_move int_solver::report_gomory_cut(lar_term& t, mpq& k, mpq &lcm_den, unsign gomory_cut_adjust_t_and_k_for_size_1(pol, t, k); else gomory_cut_adjust_t_and_k_for_size_gt_1(pol, t, k, num_ints, lcm_den); - m_lar_solver->subs_terms_for_debugging(t); // todo: remove later + m_lar_solver->subs_term_columns(t); return lia_move::cut; } diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index d6f55c612..3a48c4d79 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -461,14 +461,16 @@ public: return m_columns_to_ul_pairs()[j].low_bound_witness(); } - void subs_terms_for_debugging(lar_term& t) { - vector> pol; + void subs_term_columns(lar_term& t) { + vector > pol; for (const auto & m : t.m_coeffs) { pol.push_back(std::make_pair(m.second, adjust_column_index_to_term_index(m.first))); } + + mpq v = t.m_v; - vector> pol_after_subs; + // todo : remove the call to substitute_terms_in_linear_expression substitute_terms_in_linear_expression(pol, pol_after_subs, v); t.clear(); t = lar_term(pol_after_subs, v);