mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

remove an unused field

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-03-18 10:08:02 -07:00 • committed by Lev Nachmanson
parent fc1c8c4cc4
commit 307af0fd97
1 changed files with 0 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/lp/dioph_eq.cpp
View file

@ -501,7 +501,6 @@ namespace lp {
indexed_uint_set m_changed_columns;
indexed_uint_set m_changed_terms; // represented by term columns
indexed_uint_set m_terms_to_tighten; // represented by term columns
indexed_uint_set m_tightened_columns; // the column that got tightened by the tigthening phase,
// m_column_to_terms[j] is the set of all k such lra.get_term(k) depends on j
std::unordered_map<unsigned, std::unordered_set<unsigned>> m_columns_to_terms;
@ -1399,7 +1398,6 @@ namespace lp {
// Copy changed terms to another vector for sorting
std_vector<unsigned> sorted_changed_terms;
std_vector<unsigned> processed_terms;
m_tightened_columns.reset();
for (unsigned j: m_terms_to_tighten) {
if (j >= lra.column_count() ||
!lra.column_has_term(j) ||
@ -1733,7 +1731,6 @@ namespace lp {
lp_status st = lra.find_feasible_solution();
if ((int)st >= (int)lp::lp_status::FEASIBLE) {
m_tightened_columns.insert(j);
return false;
}
if (st == lp_status::CANCELLED) return false;