Skip to content

Commit c81eb74

Browse files
levnachlevnach
committed
apply the slack idea in a loop
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
1 parent e041fe9 commit c81eb74

2 files changed

Lines changed: 70 additions & 39 deletions

File tree

‎src/math/lp/lar_solver.cpp‎

Lines changed: 65 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,46 @@
88

99

1010
namespace lp {
11+
struct column_update {
12+
bool m_is_upper;
13+
unsigned m_j;
14+
impq m_bound;
15+
column m_column;
16+
};
17+
18+
struct imp {
19+
lar_solver &lra;
20+
vector<column_update> m_column_updates;
21+
22+
void set_r_upper_bound(unsigned j, const impq& b) {
23+
lra.m_mpq_lar_core_solver.m_r_upper_bounds[j] = b;
24+
}
25+
void set_r_lower_bound(unsigned j, const impq& b) {
26+
lra.m_mpq_lar_core_solver.m_r_lower_bounds[j] = b;
27+
}
28+
29+
imp(lar_solver& s) : lra(s) {}
30+
31+
void set_column(unsigned j, const column& c) {
32+
lra.m_columns[j] = c;
33+
}
34+
35+
struct column_update_trail : public trail {
36+
imp& m_imp;
37+
column_update_trail(imp & i) : m_imp(i) {}
38+
void undo() override {
39+
auto& [is_upper, j, bound, column] = m_imp.m_column_updates.back();
40+
if (is_upper)
41+
m_imp.set_r_upper_bound(j, bound);
42+
else
43+
m_imp.set_r_lower_bound(j, bound);
44+
m_imp.set_column(j, column);
45+
m_imp.m_column_updates.pop_back();
46+
}
47+
};
48+
};
1149

50+
imp* m_imp;
1251
lp_settings& lar_solver::settings() { return m_settings; }
1352

1453
lp_settings const& lar_solver::settings() const { return m_settings; }
@@ -25,7 +64,8 @@ namespace lp {
2564
lar_solver::lar_solver() :
2665
m_mpq_lar_core_solver(m_settings, *this),
2766
m_var_register(),
28-
m_constraints(m_dependencies, *this) {}
67+
m_constraints(m_dependencies, *this), m_imp(alloc(imp, *this)) {
68+
}
2969

3070
// start or ends tracking the rows that were changed by solve()
3171
void lar_solver::track_touched_rows(bool v) {
@@ -574,38 +614,25 @@ namespace lp {
574614
A_r().pop(k);
575615
}
576616

577-
struct lar_solver::column_update_trail : public trail {
578-
lar_solver& s;
579-
column_update_trail(lar_solver& s) : s(s) {}
580-
void undo() override {
581-
auto& [is_upper, j, bound, column] = s.m_column_updates.back();
582-
if (is_upper)
583-
s.m_mpq_lar_core_solver.m_r_upper_bounds[j] = bound;
584-
else
585-
s.m_mpq_lar_core_solver.m_r_lower_bounds[j] = bound;
586-
s.m_columns[j] = column;
587-
s.m_column_updates.pop_back();
588-
}
589-
};
590-
617+
591618
void lar_solver::set_upper_bound_witness(lpvar j, u_dependency* dep, impq const& high) {
592619
bool has_upper = m_columns[j].upper_bound_witness() != nullptr;
593-
m_column_updates.push_back({true, j, get_upper_bound(j), m_columns[j]});
594-
m_trail.push(column_update_trail(*this));
620+
m_imp->m_column_updates.push_back({true, j, get_upper_bound(j), m_columns[j]});
621+
m_trail.push(imp::column_update_trail(*this->m_imp));
595622
m_columns[j].set_upper_bound_witness(dep);
596623
if (has_upper)
597-
m_columns[j].set_previous_upper(m_column_updates.size() - 1);
624+
m_columns[j].set_previous_upper(m_imp->m_column_updates.size() - 1);
598625
m_mpq_lar_core_solver.m_r_upper_bounds[j] = high;
599626
insert_to_columns_with_changed_bounds(j);
600627
}
601628

602629
void lar_solver::set_lower_bound_witness(lpvar j, u_dependency* dep, impq const& low) {
603630
bool has_lower = m_columns[j].lower_bound_witness() != nullptr;
604-
m_column_updates.push_back({false, j, get_lower_bound(j), m_columns[j]});
605-
m_trail.push(column_update_trail(*this));
631+
m_imp->m_column_updates.push_back({false, j, get_lower_bound(j), m_columns[j]});
632+
m_trail.push(imp::column_update_trail(*this->m_imp));
606633
m_columns[j].set_lower_bound_witness(dep);
607634
if (has_lower)
608-
m_columns[j].set_previous_lower(m_column_updates.size() - 1);
635+
m_columns[j].set_previous_lower(m_imp->m_column_updates.size() - 1);
609636
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
610637
insert_to_columns_with_changed_bounds(j);
611638
}
@@ -1196,26 +1223,34 @@ namespace lp {
11961223

11971224
#if 1
11981225
if(is_upper) {
1199-
if (ul.previous_upper() != UINT_MAX) {
1200-
auto const& [_is_upper, _j, _bound, _column] = m_column_updates[ul.previous_upper()];
1226+
unsigned current_update_index = ul.previous_upper();
1227+
while (current_update_index != UINT_MAX) {
1228+
auto const& [_is_upper, _j, _bound, _column] = m_imp->m_column_updates[current_update_index];
12011229
auto new_slack = slack + coeff * (_bound - get_upper_bound(j));
12021230
if (sign == get_sign(new_slack)) {
1203-
// verbose_stream() << "can weaken j" << j << " " << coeff << " " << get_upper_bound(j) << " " << _bound << "\n";
1231+
//verbose_stream() << "can weaken upper j" << j << " " << coeff << " " << get_upper_bound(j) << " " << _bound << "\n";
12041232
slack = new_slack;
12051233
bound_constr_i = _column.upper_bound_witness();
1206-
}
1234+
current_update_index = _column.previous_upper(); // Move to the next previous bound in the list
1235+
} else
1236+
break; // Stop if weakening is not possible with this previous bound
1237+
12071238
}
1208-
}
1239+
}
12091240
else {
1210-
if (ul.previous_lower() != UINT_MAX) {
1211-
auto const& [_is_upper, _j, _bound, _column] = m_column_updates[ul.previous_lower()];
1241+
unsigned prev_l = ul.previous_lower();
1242+
while (prev_l != UINT_MAX) {
1243+
auto const& [_is_upper, _j, _bound, _column] = m_imp->m_column_updates[prev_l];
12121244
auto new_slack = slack + coeff * (_bound - get_lower_bound(j));
12131245
if (sign == get_sign(new_slack)) {
1214-
// verbose_stream() << "can weaken j" << j << " " << coeff << " " << get_lower_bound(j) << " " << _bound << "\n";
1246+
//verbose_stream() << "can weaken lower j" << j << " " << coeff << " " << get_lower_bound(j) << " " << _bound << "\n";
12151247
slack = new_slack;
12161248
bound_constr_i = _column.lower_bound_witness();
1249+
prev_l = _column.previous_lower();
12171250
}
1218-
}
1251+
else
1252+
break;
1253+
}
12191254
}
12201255
#endif
12211256

‎src/math/lp/lar_solver.h‎

Lines changed: 5 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ namespace lp {
4747

4848
class int_branch;
4949
class int_solver;
50-
50+
struct imp;
5151

5252
class lar_solver : public column_namer {
5353
struct term_hasher {
@@ -73,13 +73,7 @@ class lar_solver : public column_namer {
7373
}
7474
};
7575

76-
struct column_update {
77-
bool m_is_upper;
78-
unsigned m_j;
79-
impq m_bound;
80-
column m_column;
81-
};
82-
struct column_update_trail;
76+
8377

8478
//////////////////// fields //////////////////////////
8579
trail_stack m_trail;
@@ -94,7 +88,6 @@ class lar_solver : public column_namer {
9488
bool m_need_register_terms = false;
9589
var_register m_var_register;
9690
svector<column> m_columns;
97-
vector<column_update> m_column_updates;
9891

9992
constraint_set m_constraints;
10093
// the set of column indices j such that bounds have changed for j
@@ -123,6 +116,7 @@ class lar_solver : public column_namer {
123116
map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>> m_fixed_var_table_real;
124117
// the set of fixed variables which are also base variables
125118
indexed_uint_set m_fixed_base_var_set;
119+
imp* m_imp;
126120
// end of fields
127121

128122
////////////////// nested structs /////////////////////////
@@ -742,5 +736,7 @@ class lar_solver : public column_namer {
742736
std::function<void (const indexed_uint_set& columns_with_changed_bound)> m_find_monics_with_changed_bounds_func = nullptr;
743737
friend int_solver;
744738
friend int_branch;
739+
friend imp;
740+
745741
};
746742
} // namespace lp

0 commit comments

Comments
 (0)