From 1618c970dfcea7001df22a94e2a0bec06d973de5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Dec 2021 13:17:48 -0800 Subject: [PATCH] adding checks Signed-off-by: Nikolaj Bjorner --- src/math/lp/int_solver.cpp | 2 +- src/math/lp/lar_solver.h | 4 ++++ src/math/lp/random_updater_def.h | 14 ++++++-------- 3 files changed, 11 insertions(+), 9 deletions(-) diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index ac9937f2e..39ef072b0 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -536,7 +536,7 @@ for (const auto &c : row) } std::ostream& int_solver::display_row_info(std::ostream & out, unsigned row_index) const { auto & rslv = lrac.m_r_solver; - auto row = rslv.m_A.m_rows[row_index]; + auto const& row = rslv.m_A.m_rows[row_index]; return display_row(out, row); } diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index b4c69d783..9dd180395 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -555,6 +555,10 @@ public: return m_mpq_lar_core_solver.column_is_bounded(j); } + bool check_feasible() const { + return m_mpq_lar_core_solver.m_r_solver.calc_current_x_is_feasible_include_non_basis(); + } + std::pair add_equality(lpvar j, lpvar k); inline void get_bound_constraint_witnesses_for_column(unsigned j, constraint_index & lc, constraint_index & uc) const { diff --git a/src/math/lp/random_updater_def.h b/src/math/lp/random_updater_def.h index aca4e1d65..25ef6f82f 100644 --- a/src/math/lp/random_updater_def.h +++ b/src/math/lp/random_updater_def.h @@ -51,25 +51,23 @@ bool random_updater::shift_var(unsigned j) { void random_updater::update() { + // VERIFY(m_lar_solver.check_feasible()); auto columns = m_var_set.index(); // m_var_set is going to change during the loop for (auto j : columns) { if (!m_var_set.contains(j)) { TRACE("lar_solver_rand", tout << "skipped " << j << "\n";); continue; } - if (!m_lar_solver.is_base(j)) { + if (!m_lar_solver.is_base(j)) shift_var(j); - } else { + else { unsigned row_index = m_lar_solver.r_heading()[j]; for (auto & row_c : m_lar_solver.get_row(row_index)) { unsigned cj = row_c.var(); if (!m_lar_solver.is_base(cj) && - !m_lar_solver.column_is_fixed(cj) - && - shift_var(cj) - ) { - break; // done with the basic var j - } + !m_lar_solver.column_is_fixed(cj) && + shift_var(cj)) + break; // done with the basic var j } } }