mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

do not pass row index to bound_analyzer_on_row

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-02-21 14:31:44 -08:00
parent 10c2af85c1
commit b985838112
3 changed files with 14 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -32,7 +32,6 @@ template <typename C, typename B> // C plays a role of a container, B - lp_bound
class bound_analyzer_on_row {
const C& m_row;
B & m_bp;
unsigned m_row_index;
int m_column_of_u; // index of an unlimited from above monoid
// -1 means that such a value is not found, -2 means that at least two of such monoids were found
int m_column_of_l; // index of an unlimited from below monoid
@ -43,12 +42,10 @@ public :
bound_analyzer_on_row(
const C & it,
const numeric_pair<mpq>& rs,
unsigned row_or_term_index,
B & bp)
:
m_row(it),
m_bp(bp),
m_row_index(row_or_term_index),
m_column_of_u(-1),
m_column_of_l(-1),
m_rs(rs)
@ -57,9 +54,8 @@ public :
static unsigned analyze_row(const C & row,
const numeric_pair<mpq>& rs,
unsigned row_or_term_index,
B & bp) {
bound_analyzer_on_row a(row, rs, row_or_term_index, bp);
bound_analyzer_on_row a(row, rs, bp);
return a.analyze();
}
@ -281,16 +277,16 @@ private:
void limit_j(unsigned bound_j, const mpq& u, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict)
{
unsigned row_index = this->m_row_index;
auto* lar = &m_bp.lp();
auto explain = [bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index, lar]() {
const auto& row = this->m_row;
auto explain = [row, bound_j, coeff_before_j_is_pos, is_lower_bound, strict, lar]() {
(void) strict;
TRACE("bound_analyzer", tout << "explain_bound_on_var_on_coeff, bound_j = " << bound_j << ", coeff_before_j_is_pos = " << coeff_before_j_is_pos << ", is_lower_bound = " << is_lower_bound << ", strict = " << strict << ", row_index = " << row_index << "\n";);
TRACE("bound_analyzer", tout << "explain_bound_on_var_on_coeff, bound_j = " << bound_j << ", coeff_before_j_is_pos = " << coeff_before_j_is_pos << ", is_lower_bound = " << is_lower_bound << ", strict = " << strict << "\n";);
int bound_sign = (is_lower_bound ? 1 : -1);
int j_sign = (coeff_before_j_is_pos ? 1 : -1) * bound_sign;
u_dependency* ret = nullptr;
for (auto const& r : lar->get_row(row_index)) {
for (auto const& r : row) {
unsigned j = r.var();
if (j == bound_j)
continue;

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

@ -485,6 +485,7 @@ namespace lp {
indexed_uint_set m_changed_rows;
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)
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;
@ -1361,6 +1362,7 @@ namespace lp {
// Copy changed terms to another vector for sorting
std_vector<unsigned> sorted_changed_terms;
std_vector<unsigned> cleanup;
m_tightened_columns.reset();
for (unsigned j : m_changed_terms) {
if (
j >= lra.column_count() ||
@ -1620,8 +1622,11 @@ namespace lp {
}
}
lia_move propagate_bounds_on_tightened_columns() {
return lia_move::undef;
}
// m_espace contains the coefficients of the term
// m_c contains the constant term
// m_c contains the fixed part of the term
// m_tmp_l is the linear combination of the equations that removes the
// substituted variables.
// returns true iff the conflict is found
@ -1642,6 +1647,7 @@ namespace lp {
return lia_move::conflict;
}
}
std::cout << "new tbs:" << m_tightened_columns.size() << "\n";
return lia_move::undef;
}
@ -1649,7 +1655,7 @@ namespace lp {
bool tighten_bound_kind(const mpq& g, unsigned j, const mpq& ub, bool upper,
u_dependency* prev_dep) {
// ub = (upper_bound(j) - m_c)/g.
// we have x[j] = t = g*t_+ m_c <= upper_bound(j), then
// we have xj = t = g*t_+ m_c <= upper_bound(j), then
// t_ <= floor((upper_bound(j) - m_c)/g) = floor(ub)
//
// so xj = g*t_+m_c <= g*floor(ub) + m_c is new upper bound
@ -1679,6 +1685,7 @@ namespace lp {
lra.update_column_type_and_bound(j, kind, bound, dep);
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;

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

@ -185,7 +185,6 @@ class lar_solver : public column_namer {
return bound_analyzer_on_row<row_strip<mpq>, lp_bound_propagator<T>>::analyze_row(
A_r().m_rows[row_index],
zero_of_type<numeric_pair<mpq>>(),
row_index,
bp);
}