mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

a cleaner version of subs_term_columns

Browse source 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
Lev Nachmanson 2017-07-19 22:14:05 -07:00
parent 4d1b0d8026
commit 1490b7a15f
2 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/util/lp/int_solver.cpp
View file

@ -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); gomory_cut_adjust_t_and_k_for_size_1(pol, t, k);
else else
gomory_cut_adjust_t_and_k_for_size_gt_1(pol, t, k, num_ints, lcm_den); 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; return lia_move::cut;
} }

8
src/util/lp/lar_solver.h
View file

@ -461,14 +461,16 @@ public:
return m_columns_to_ul_pairs()[j].low_bound_witness(); return m_columns_to_ul_pairs()[j].low_bound_witness();
} }
void subs_terms_for_debugging(lar_term& t) { void subs_term_columns(lar_term& t) {
vector<std::pair<mpq, unsigned>> pol; vector<std::pair<mpq, unsigned> > pol;
for (const auto & m : t.m_coeffs) { for (const auto & m : t.m_coeffs) {
pol.push_back(std::make_pair(m.second, adjust_column_index_to_term_index(m.first))); pol.push_back(std::make_pair(m.second, adjust_column_index_to_term_index(m.first)));
} }
mpq v = t.m_v; mpq v = t.m_v;
vector<std::pair<mpq, unsigned>> pol_after_subs; vector<std::pair<mpq, unsigned>> pol_after_subs;
// todo : remove the call to substitute_terms_in_linear_expression
substitute_terms_in_linear_expression(pol, pol_after_subs, v); substitute_terms_in_linear_expression(pol, pol_after_subs, v);
t.clear(); t.clear();
t = lar_term(pol_after_subs, v); t = lar_term(pol_after_subs, v);