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

convert m_r_upper and m_r_lower bounds to plain vectors

Browse source 
manage backtracking state together with backtracking of column data.
This commit is contained in:
Nikolaj Bjorner 2025-04-23 16:33:38 -07:00
parent fae60946bf
commit e41acd7b50
6 changed files with 46 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/int_branch.cpp
View file

@ -75,7 +75,7 @@ int int_branch::find_inf_int_base_column() {
if (!lia.column_is_int_inf(j)) if (!lia.column_is_int_inf(j))
continue; continue;
usage = lra.usage_in_terms(j); usage = lra.usage_in_terms(j);
if (lia.is_boxed(j) && (range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage)) <= small_value) { if (lia.is_boxed(j) && (range = lcs.m_r_upper_bounds[j].x - lcs.m_r_lower_bounds[j].x - rational(2*usage)) <= small_value) {
result = j; result = j;
k++; k++;
n = 1; n = 1;
@ -98,7 +98,7 @@ int int_branch::find_inf_int_base_column() {
continue; continue;
SASSERT(!lia.is_fixed(j)); SASSERT(!lia.is_fixed(j));
usage = lra.usage_in_terms(j); usage = lra.usage_in_terms(j);
new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage); new_range = lcs.m_r_upper_bounds[j].x - lcs.m_r_lower_bounds[j].x - rational(2*usage);
if (new_range < range) { if (new_range < range) {
n = 1; n = 1;
result = j; result = j;

8
src/math/lp/lar_core_solver.h
View file

@ -29,8 +29,8 @@ public:
stacked_vector<column_type> m_column_types; stacked_vector<column_type> m_column_types;
// r - solver fields, for rational numbers // r - solver fields, for rational numbers
stacked_vector<numeric_pair<mpq>> m_r_lower_bounds; vector<numeric_pair<mpq>> m_r_lower_bounds;
stacked_vector<numeric_pair<mpq>> m_r_upper_bounds; vector<numeric_pair<mpq>> m_r_upper_bounds;
static_matrix<mpq, numeric_pair<mpq>> m_r_A; static_matrix<mpq, numeric_pair<mpq>> m_r_A;
stacked_vector<unsigned> m_r_pushed_basis; stacked_vector<unsigned> m_r_pushed_basis;
vector<unsigned> m_r_basis; vector<unsigned> m_r_basis;
@ -122,14 +122,10 @@ public:
m_stacked_simplex_strategy.push(); m_stacked_simplex_strategy.push();
m_column_types.push(); m_column_types.push();
// rational // rational
m_r_lower_bounds.push();
m_r_upper_bounds.push();
} }
void pop(unsigned k) { void pop(unsigned k) {
// rationals // rationals
m_r_lower_bounds.pop(k);
m_r_upper_bounds.pop(k);
m_column_types.pop(k); m_column_types.pop(k);
m_r_x.resize(m_r_A.column_count()); m_r_x.resize(m_r_A.column_count());

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

@ -27,8 +27,8 @@ lar_core_solver::lar_core_solver(
m_r_heading, m_r_heading,
m_costs_dummy, m_costs_dummy,
m_column_types(), m_column_types(),
m_r_lower_bounds(), m_r_lower_bounds,
m_r_upper_bounds(), m_r_upper_bounds,
settings, settings,
column_names) { column_names) {
} }

40
src/math/lp/lar_solver.cpp
View file

@ -421,14 +421,14 @@ namespace lp {
auto& val = lcs.r_x(j); auto& val = lcs.r_x(j);
switch (lcs.m_column_types()[j]) { switch (lcs.m_column_types()[j]) {
case column_type::boxed: { case column_type::boxed: {
const auto& l = lcs.m_r_lower_bounds()[j]; const auto& l = lcs.m_r_lower_bounds[j];
if (val == l || val == lcs.m_r_upper_bounds()[j]) return false; if (val == l || val == lcs.m_r_upper_bounds[j]) return false;
set_value_for_nbasic_column(j, l); set_value_for_nbasic_column(j, l);
return true; return true;
} }
case column_type::lower_bound: { case column_type::lower_bound: {
const auto& l = lcs.m_r_lower_bounds()[j]; const auto& l = lcs.m_r_lower_bounds[j];
if (val != l) { if (val != l) {
set_value_for_nbasic_column(j, l); set_value_for_nbasic_column(j, l);
return true; return true;
@ -437,7 +437,7 @@ namespace lp {
} }
case column_type::fixed: case column_type::fixed:
case column_type::upper_bound: { case column_type::upper_bound: {
const auto & u = lcs.m_r_upper_bounds()[j]; const auto & u = lcs.m_r_upper_bounds[j];
if (val != u) { if (val != u) {
set_value_for_nbasic_column(j, u); set_value_for_nbasic_column(j, u);
return true; return true;
@ -574,15 +574,31 @@ namespace lp {
A_r().pop(k); A_r().pop(k);
} }
struct lar_solver::column_update_trail : public trail {
lar_solver& s;
column_update_trail(lar_solver& s) : s(s) {}
void undo() override {
auto& [is_upper, j, bound, column] = s.m_column_updates.back();
if (is_upper)
s.m_mpq_lar_core_solver.m_r_upper_bounds[j] = bound;
else
s.m_mpq_lar_core_solver.m_r_lower_bounds[j] = bound;
s.m_columns[j] = column;
s.m_column_updates.pop_back();
}
};
void lar_solver::set_upper_bound_witness(lpvar j, u_dependency* dep, impq const& high) { void lar_solver::set_upper_bound_witness(lpvar j, u_dependency* dep, impq const& high) {
m_trail.push(vector_value_trail(m_columns, j)); m_column_updates.push_back({true, j, get_upper_bound(j), m_columns[j]});
m_trail.push(column_update_trail(*this));
m_columns[j].set_upper_bound_witness(dep); m_columns[j].set_upper_bound_witness(dep);
m_mpq_lar_core_solver.m_r_upper_bounds[j] = high; m_mpq_lar_core_solver.m_r_upper_bounds[j] = high;
insert_to_columns_with_changed_bounds(j); insert_to_columns_with_changed_bounds(j);
} }
void lar_solver::set_lower_bound_witness(lpvar j, u_dependency* dep, impq const& low) { void lar_solver::set_lower_bound_witness(lpvar j, u_dependency* dep, impq const& low) {
m_trail.push(vector_value_trail(m_columns, j)); m_column_updates.push_back({false, j, get_lower_bound(j), m_columns[j]});
m_trail.push(column_update_trail(*this));
m_columns[j].set_lower_bound_witness(dep); m_columns[j].set_lower_bound_witness(dep);
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low; m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
insert_to_columns_with_changed_bounds(j); insert_to_columns_with_changed_bounds(j);
@ -1084,7 +1100,7 @@ namespace lp {
const column& ul = m_columns[var]; const column& ul = m_columns[var];
dep = ul.lower_bound_witness(); dep = ul.lower_bound_witness();
if (dep != nullptr) { if (dep != nullptr) {
auto& p = m_mpq_lar_core_solver.m_r_lower_bounds()[var]; auto& p = m_mpq_lar_core_solver.m_r_lower_bounds[var];
value = p.x; value = p.x;
is_strict = p.y.is_pos(); is_strict = p.y.is_pos();
return true; return true;
@ -1103,7 +1119,7 @@ namespace lp {
const column& ul = m_columns[var]; const column& ul = m_columns[var];
dep = ul.upper_bound_witness(); dep = ul.upper_bound_witness();
if (dep != nullptr) { if (dep != nullptr) {
auto& p = m_mpq_lar_core_solver.m_r_upper_bounds()[var]; auto& p = m_mpq_lar_core_solver.m_r_upper_bounds[var];
value = p.x; value = p.x;
is_strict = p.y.is_neg(); is_strict = p.y.is_neg();
return true; return true;
@ -1625,8 +1641,8 @@ namespace lp {
// SASSERT(m_mpq_lar_core_solver.m_r_lower_bounds.size() == j && m_mpq_lar_core_solver.m_r_upper_bounds.size() == j); // restore later // SASSERT(m_mpq_lar_core_solver.m_r_lower_bounds.size() == j && m_mpq_lar_core_solver.m_r_upper_bounds.size() == j); // restore later
m_mpq_lar_core_solver.resize_x(j + 1); m_mpq_lar_core_solver.resize_x(j + 1);
auto& rslv = m_mpq_lar_core_solver.m_r_solver; auto& rslv = m_mpq_lar_core_solver.m_r_solver;
m_mpq_lar_core_solver.m_r_lower_bounds.increase_size_by_one(); m_mpq_lar_core_solver.m_r_lower_bounds.reserve(j + 1);
m_mpq_lar_core_solver.m_r_upper_bounds.increase_size_by_one(); m_mpq_lar_core_solver.m_r_upper_bounds.reserve(j + 1);
rslv.inf_heap_increase_size_by_one(); rslv.inf_heap_increase_size_by_one();
rslv.m_costs.resize(j + 1); rslv.m_costs.resize(j + 1);
rslv.m_d.resize(j + 1); rslv.m_d.resize(j + 1);
@ -2264,9 +2280,9 @@ namespace lp {
impq ivalue(value); impq ivalue(value);
auto& lcs = m_mpq_lar_core_solver; auto& lcs = m_mpq_lar_core_solver;
if (column_has_upper_bound(j) && lcs.m_r_upper_bounds()[j] < ivalue) if (column_has_upper_bound(j) && lcs.m_r_upper_bounds[j] < ivalue)
return false; return false;
if (column_has_lower_bound(j) && lcs.m_r_lower_bounds()[j] > ivalue) if (column_has_lower_bound(j) && lcs.m_r_lower_bounds[j] > ivalue)
return false; return false;
set_value_for_nbasic_column(j, ivalue); set_value_for_nbasic_column(j, ivalue);

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

@ -73,6 +73,14 @@ class lar_solver : public column_namer {
} }
}; };
struct column_update {
bool is_upper;
unsigned j;
impq bound;
column column;
};
struct column_update_trail;
//////////////////// fields ////////////////////////// //////////////////// fields //////////////////////////
trail_stack m_trail; trail_stack m_trail;
lp_settings m_settings; lp_settings m_settings;
@ -86,6 +94,8 @@ class lar_solver : public column_namer {
bool m_need_register_terms = false; bool m_need_register_terms = false;
var_register m_var_register; var_register m_var_register;
svector<column> m_columns; svector<column> m_columns;
vector<column_update> m_column_updates;
constraint_set m_constraints; constraint_set m_constraints;
// the set of column indices j such that bounds have changed for j // the set of column indices j such that bounds have changed for j
indexed_uint_set m_columns_with_changed_bounds; indexed_uint_set m_columns_with_changed_bounds;

2
src/math/lp/lp_core_solver_base.h
View file

@ -437,7 +437,7 @@ public:
} }
std::ostream& print_column_info(unsigned j, std::ostream & out, bool print_nl = false, const std::string& var_prefix = "j") const { std::ostream& print_column_info(unsigned j, std::ostream & out, bool print_nl = false, const std::string& var_prefix = "j") const {
if (j >= m_lower_bounds.size()) { if (j >= m_column_types.size()) {
out << "[" << j << "] is not present\n"; out << "[" << j << "] is not present\n";
return out; return out;
} }