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

use m_chandedNterms to tighten terms

Browse source
This commit is contained in:
Lev Nachmanson 2025-02-03 07:02:54 -10:00 • committed by Lev Nachmanson
parent 65bdd58d3e
commit 3b3d8cee03
1 changed files with 19 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -438,6 +438,7 @@ namespace lp {
indexed_uint_set m_changed_rows; indexed_uint_set m_changed_rows;
indexed_uint_set m_changed_columns; indexed_uint_set m_changed_columns;
indexed_uint_set m_changed_terms; // a term is defined by its column j, as in lar_solver.get_term(j)
// m_column_to_terms[j] is the set of all k such lra.get_term(k) depends on j // 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; std::unordered_map<unsigned, std::unordered_set<unsigned>> m_columns_to_terms;
@ -886,12 +887,12 @@ namespace lp {
SASSERT(entry_invariant(ei)); SASSERT(entry_invariant(ei));
} }
void find_changed_terms_and_more_changed_rows(std::unordered_set<unsigned> & changed_terms) { void find_changed_terms_and_more_changed_rows() {
for (unsigned j : m_changed_columns) { for (unsigned j : m_changed_columns) {
const auto it = m_columns_to_terms.find(j); const auto it = m_columns_to_terms.find(j);
if (it != m_columns_to_terms.end()) if (it != m_columns_to_terms.end())
for (unsigned k : it->second) { for (unsigned k : it->second) {
changed_terms.insert(k); m_changed_terms.insert(k);
} }
if (!m_var_register.external_is_used(j)) if (!m_var_register.external_is_used(j))
continue; continue;
@ -923,9 +924,8 @@ namespace lp {
delete_column(j); delete_column(j);
} }
} }
std::unordered_set<unsigned> changed_terms; // a term is signified by the term column, like j in lra.get_term(j) find_changed_terms_and_more_changed_rows();
find_changed_terms_and_more_changed_rows(changed_terms); for (unsigned j : m_changed_terms) {
for (unsigned j : changed_terms) {
for (const auto & cs: m_l_matrix.column(j)) { for (const auto & cs: m_l_matrix.column(j)) {
m_changed_rows.insert(cs.var()); m_changed_rows.insert(cs.var());
} }
@ -1324,16 +1324,24 @@ namespace lp {
} }
lia_move tighten_terms_with_S() { lia_move tighten_terms_with_S() {
for (unsigned j = 0; j < lra.column_count(); j++) { std_vector<unsigned> cleanup;
lia_move ret = lia_move::undef;
for (unsigned j : m_changed_terms) {
cleanup.push_back(j);
if (!lra.column_has_term(j) || lra.column_is_free(j) || if (!lra.column_has_term(j) || lra.column_is_free(j) ||
is_fixed(j) || !lia.column_is_int(j)) is_fixed(j) || !lia.column_is_int(j)) {
continue; continue;
if (tighten_bounds_for_term_column(j))
return lia_move::conflict;
} }
return lia_move::undef; if (tighten_bounds_for_term_column(j)) {
ret = lia_move::conflict;
break;
}
}
for (unsigned j: cleanup) {
m_changed_terms.remove(j);
}
return ret;
} }
std::ostream& print_queue(std::queue<unsigned> q, std::ostream& out) { std::ostream& print_queue(std::queue<unsigned> q, std::ostream& out) {