convert m_r_upper and m_r_lower bounds to plain vectors

manage backtracking state together with backtracking of column data.

Author: NikolajBjorner

src/math/lp/int_branch.cpp

@@ -75,7 +75,7 @@ int int_branch::find_inf_int_base_column() {
         if (!lia.column_is_int_inf(j))
             continue;
         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;
             k++;            
             n = 1;
@@ -98,7 +98,7 @@ int int_branch::find_inf_int_base_column() {
             continue;
         SASSERT(!lia.is_fixed(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) {
             n = 1;
             result = j;

src/math/lp/lar_core_solver.h

@@ -29,8 +29,8 @@ class lar_core_solver  {
     stacked_vector<column_type> m_column_types;
     // r - solver fields, for rational numbers
 
-    stacked_vector<numeric_pair<mpq>> m_r_lower_bounds;
-    stacked_vector<numeric_pair<mpq>> m_r_upper_bounds;
+    vector<numeric_pair<mpq>> m_r_lower_bounds;
+    vector<numeric_pair<mpq>> m_r_upper_bounds;
     static_matrix<mpq, numeric_pair<mpq>> m_r_A;
     stacked_vector<unsigned> m_r_pushed_basis;
     vector<unsigned>         m_r_basis;
@@ -121,15 +121,11 @@ class lar_core_solver  {
         m_stacked_simplex_strategy = settings().simplex_strategy();
         m_stacked_simplex_strategy.push();
         m_column_types.push();
-        // rational
-        m_r_lower_bounds.push();
-        m_r_upper_bounds.push();        
+        // rational     
     }
 
     void pop(unsigned k) {
         // rationals
-        m_r_lower_bounds.pop(k);
-        m_r_upper_bounds.pop(k);
         m_column_types.pop(k);
 
         m_r_x.resize(m_r_A.column_count());

src/math/lp/lar_core_solver_def.h

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

src/math/lp/lar_solver.cpp

@@ -421,14 +421,14 @@ namespace lp {
         auto& val = lcs.r_x(j);
         switch (lcs.m_column_types()[j]) {
         case column_type::boxed: {
-            const auto& l = lcs.m_r_lower_bounds()[j];
-            if (val == l || val == lcs.m_r_upper_bounds()[j]) return false;
+            const auto& l = lcs.m_r_lower_bounds[j];
+            if (val == l || val == lcs.m_r_upper_bounds[j]) return false;
             set_value_for_nbasic_column(j, l);
             return true;
         }
 
         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) {
                 set_value_for_nbasic_column(j, l);
                 return true;
@@ -437,7 +437,7 @@ namespace lp {
         }
         case column_type::fixed:
         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) {
                 set_value_for_nbasic_column(j, u);
                 return true;
@@ -574,15 +574,31 @@ namespace lp {
         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) {
-        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_mpq_lar_core_solver.m_r_upper_bounds[j] = high;
         insert_to_columns_with_changed_bounds(j);
     }
 
     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_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
         insert_to_columns_with_changed_bounds(j);
@@ -1084,7 +1100,7 @@ namespace lp {
         const column& ul = m_columns[var];
         dep = ul.lower_bound_witness();
         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;
             is_strict = p.y.is_pos();
             return true;
@@ -1103,7 +1119,7 @@ namespace lp {
         const column& ul = m_columns[var];
         dep = ul.upper_bound_witness();
         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;
             is_strict = p.y.is_neg();
             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
         m_mpq_lar_core_solver.resize_x(j + 1);
         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_upper_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.reserve(j + 1);
         rslv.inf_heap_increase_size_by_one();
         rslv.m_costs.resize(j + 1);
         rslv.m_d.resize(j + 1);
@@ -2264,9 +2280,9 @@ namespace lp {
         impq ivalue(value);
         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;
-        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;
 
         set_value_for_nbasic_column(j, ivalue);

src/math/lp/lar_solver.h

@@ -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 //////////////////////////
     trail_stack m_trail;
     lp_settings m_settings;
@@ -86,6 +94,8 @@ class lar_solver : public column_namer {
     bool m_need_register_terms = false;
     var_register m_var_register;
     svector<column> m_columns;
+    vector<column_update> m_column_updates;
+    
     constraint_set m_constraints;
     // the set of column indices j such that bounds have changed for j
     indexed_uint_set m_columns_with_changed_bounds;

src/math/lp/lp_core_solver_base.h

@@ -437,7 +437,7 @@ class lp_core_solver_base {
     }
 
     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";
             return out;
         }