mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

adding checks

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-12-03 13:17:48 -08:00
parent 970347e797
commit 1618c970df
3 changed files with 11 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -536,7 +536,7 @@ for (const auto &c : row)
} }
std::ostream& int_solver::display_row_info(std::ostream & out, unsigned row_index) const { std::ostream& int_solver::display_row_info(std::ostream & out, unsigned row_index) const {
auto & rslv = lrac.m_r_solver; 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); return display_row(out, row);
} }

4
src/math/lp/lar_solver.h
View file

@ -555,6 +555,10 @@ public:
return m_mpq_lar_core_solver.column_is_bounded(j); 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<constraint_index, constraint_index> add_equality(lpvar j, lpvar k); std::pair<constraint_index, constraint_index> add_equality(lpvar j, lpvar k);
inline void get_bound_constraint_witnesses_for_column(unsigned j, constraint_index & lc, constraint_index & uc) const { inline void get_bound_constraint_witnesses_for_column(unsigned j, constraint_index & lc, constraint_index & uc) const {

14
src/math/lp/random_updater_def.h
View file

@ -51,25 +51,23 @@ bool random_updater::shift_var(unsigned j) {
void random_updater::update() { 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 auto columns = m_var_set.index(); // m_var_set is going to change during the loop
for (auto j : columns) { for (auto j : columns) {
if (!m_var_set.contains(j)) { if (!m_var_set.contains(j)) {
TRACE("lar_solver_rand", tout << "skipped " << j << "\n";); TRACE("lar_solver_rand", tout << "skipped " << j << "\n";);
continue; continue;
} }
if (!m_lar_solver.is_base(j)) { if (!m_lar_solver.is_base(j))
shift_var(j); shift_var(j);
} else { else {
unsigned row_index = m_lar_solver.r_heading()[j]; unsigned row_index = m_lar_solver.r_heading()[j];
for (auto & row_c : m_lar_solver.get_row(row_index)) { for (auto & row_c : m_lar_solver.get_row(row_index)) {
unsigned cj = row_c.var(); unsigned cj = row_c.var();
if (!m_lar_solver.is_base(cj) && if (!m_lar_solver.is_base(cj) &&
!m_lar_solver.column_is_fixed(cj) !m_lar_solver.column_is_fixed(cj) &&
&& shift_var(cj))
shift_var(cj) break; // done with the basic var j
) {
break; // done with the basic var j
}
} }
} }
} }