From c2e7dd337839d6b75b4ddd93d73c1d45a20c8354 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 16 Mar 2020 11:24:25 -0700 Subject: [PATCH] catch the possible infeasible column when adding an equality Signed-off-by: Lev Nachmanson --- src/math/lp/lar_solver.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 7cf314708..e7aa0ff20 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1693,9 +1693,9 @@ bool lar_solver::all_vars_are_registered(const vector> return true; } -// do not register this term if ext_i == UINT_MAX +// do not register in m_var_register this term if ext_i == UINT_MAX var_index lar_solver::add_term(const vector> & coeffs, unsigned ext_i) { - TRACE("lar_solver_terms", print_linear_combination_of_column_indices_only(coeffs, tout) << ", ext_i =" << ext_i << "\n";); + TRACE("lar_solver_terms", print_linear_combination_of_column_indices_only(coeffs, tout) << ", ext_i =" << ext_i << "\n";); m_term_register.add_var(ext_i, term_is_int(coeffs)); lp_assert(all_vars_are_registered(coeffs)); if (strategy_is_undecided()) @@ -2362,6 +2362,9 @@ std::pair lar_solver::add_equality(lpvar j, coeffs.push_back(std::make_pair(mpq(1),j)); coeffs.push_back(std::make_pair(mpq(-1),k)); unsigned term_index = add_term(coeffs, UINT_MAX); // UINT_MAX is the external null var + if (get_column_value(j) != get_column_value(k)) { + set_infeasible_column(map_term_index_to_column_index(term_index)); + } return std::pair( add_var_bound(term_index, lconstraint_kind::LE, mpq(0)), add_var_bound(term_index, lconstraint_kind::GE, mpq(0)));