add changes in lp with validate_bound and maximize_term

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/math/lp/lar_core_solver.h

@@ -122,7 +122,7 @@ class lar_core_solver  {
         m_r_solver.m_d.resize(m_r_A.column_count());
 
         m_stacked_simplex_strategy.pop(k);
-        m_r_solver.m_settings.set_simplex_strategy(m_stacked_simplex_strategy);
+        m_r_solver.m_settings.simplex_strategy() = m_stacked_simplex_strategy;
         m_infeasible_linear_combination.reset();
         lp_assert(m_r_solver.basis_heading_is_correct());
     }

src/math/lp/lar_solver.h

@@ -155,12 +155,20 @@ class lar_solver : public column_namer {
     lpvar& crossed_bounds_column() { return m_crossed_bounds_column; } 
 
 
- private:   
+ private:
+    bool validate_bound(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);   
+    void add_dep_constraints_to_solver(lar_solver& ls, u_dependency* dep);
+    void add_bound_negation_to_solver(lar_solver& ls, lpvar j, lconstraint_kind kind, const mpq& right_side);
+    void add_constraint_to_validate(lar_solver& ls, constraint_index ci);
+    bool m_validate_blocker = false;
     void update_column_type_and_bound_check_on_equal(unsigned j, const mpq& right_side, constraint_index ci, unsigned&);
     void update_column_type_and_bound(unsigned j, const mpq& right_side, constraint_index ci);
  public:   
-    void update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
- private:   
+    bool validate_blocker() const { return m_validate_blocker; }
+    bool & validate_blocker() { return m_validate_blocker; }   
+	void update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
+ private:
+    void require_nbasis_sort() { m_mpq_lar_core_solver.m_r_solver.m_nbasis_sort_counter = 0; }   
     void update_column_type_and_bound_with_ub(var_index j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
     void update_column_type_and_bound_with_no_ub(var_index j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
     void update_bound_with_ub_lb(var_index j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
@@ -203,7 +211,9 @@ class lar_solver : public column_namer {
     bool reduced_costs_are_zeroes_for_r_solver() const;
     void set_costs_to_zero(const lar_term& term);
     void prepare_costs_for_r_solver(const lar_term& term);
-    bool maximize_term_on_corrected_r_solver(lar_term& term, impq& term_max);
+    bool maximize_term_on_feasible_r_solver(lar_term& term, impq& term_max, vector<std::pair<mpq,lpvar>>* max_coeffs);
+    u_dependency* get_dependencies_of_maximum(const vector<std::pair<mpq,lpvar>>& max_coeffs);
+
     void pop_core_solver_params();
     void pop_core_solver_params(unsigned k);
     void set_upper_bound_witness(var_index j, u_dependency* ci);
@@ -263,7 +273,12 @@ class lar_solver : public column_namer {
     mutable std::unordered_set<mpq> m_set_of_different_singles;
     mutable mpq m_delta;
 
-   public:
+ public:
+    u_dependency* find_improved_bound(lpvar j, bool is_lower, mpq& bound);
+
+    std::ostream& print_explanation(
+        std::ostream& out, const explanation& exp, 
+        std::function<std::string(lpvar)> var_str = [](lpvar j) { return std::string("j") + T_to_string(j); }) const;
     // this function just looks at the status
     bool is_feasible() const;
 
@@ -302,8 +317,6 @@ class lar_solver : public column_namer {
 
     lp_status maximize_term(unsigned j_or_term, impq& term_max);
 
-    bool improve_bound(lpvar j, bool is_lower);
-
     inline core_solver_pretty_printer<lp::mpq, lp::impq> pp(std::ostream& out) const {
         return core_solver_pretty_printer<lp::mpq, lp::impq>(m_mpq_lar_core_solver.m_r_solver, out);
     }

src/math/lp/lp_core_solver_base.cpp

@@ -23,10 +23,8 @@ Revision History:
 #include "util/vector.h"
 #include <functional>
 #include "math/lp/lp_core_solver_base_def.h"
-template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::print_statistics_with_iterations_and_nonzeroes_and_cost_and_check_that_the_time_is_over(char const*, std::ostream &);
 template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::basis_heading_is_correct() const ;
 template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::column_is_dual_feasible(unsigned int) const;
-template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::print_statistics_with_iterations_and_nonzeroes_and_cost_and_check_that_the_time_is_over(char const*, std::ostream &);
 template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::add_delta_to_entering(unsigned int, const lp::mpq&);
 template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::init();
 template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::init_basis_heading_and_non_basic_columns_vector();
@@ -35,7 +33,6 @@ template lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::lp_core_s
     vector<unsigned int >&, vector<unsigned> &, vector<int> &, vector<lp::numeric_pair<lp::mpq> >&, vector<lp::mpq>&, lp::lp_settings&, const column_namer&, const vector<lp::column_type >&,
                                                                                                    const vector<lp::numeric_pair<lp::mpq> >&,
                                                                                                    const vector<lp::numeric_pair<lp::mpq> >&);
-template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::print_statistics_with_cost_and_check_that_the_time_is_over(lp::numeric_pair<lp::mpq>, std::ostream&);
 
 template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::add_delta_to_entering(unsigned int, const lp::numeric_pair<lp::mpq>&);
 template lp::lp_core_solver_base<lp::mpq, lp::mpq>::lp_core_solver_base(
@@ -50,7 +47,6 @@ template lp::lp_core_solver_base<lp::mpq, lp::mpq>::lp_core_solver_base(
                                                                               const vector<lp::column_type >&,
                                                                               const vector<lp::mpq>&,
                                                                               const vector<lp::mpq>&);
-template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::print_statistics_with_iterations_and_check_that_the_time_is_over(std::ostream &);
 template std::string lp::lp_core_solver_base<lp::mpq, lp::mpq>::column_name(unsigned int) const;
 template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::pretty_print(std::ostream & out);
 template std::string lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::column_name(unsigned int) const;

src/math/lp/lp_core_solver_base.h

@@ -19,6 +19,7 @@ Revision History:
 --*/
 #pragma once
 #include <set>
+#include <list>
 #include "util/vector.h"
 #include <string>
 #include "math/lp/lp_utils.h"
@@ -88,7 +89,7 @@ class lp_core_solver_base {
     const vector<column_type> & m_column_types;
     const vector<X> &     m_lower_bounds;
     const vector<X> &     m_upper_bounds; 
-    unsigned              m_basis_sort_counter;
+    unsigned              m_nbasis_sort_counter;
     vector<unsigned>      m_trace_of_basis_change_vector; // the even positions are entering, the odd positions are leaving
     bool                  m_tracing_basis_changes;
     // these rows are changed by adding to them a multiple of the pivot row
@@ -165,10 +166,6 @@ class lp_core_solver_base {
 
     void print_statistics(char const* str, X cost, std::ostream & message_stream);
 
-    bool print_statistics_with_iterations_and_check_that_the_time_is_over(std::ostream & message_stream);
-
-    bool print_statistics_with_iterations_and_nonzeroes_and_cost_and_check_that_the_time_is_over(char const* str, std::ostream & message_stream);
-
     bool print_statistics_with_cost_and_check_that_the_time_is_over(X cost, std::ostream & message_stream);
 
     unsigned total_iterations() const { return m_total_iterations; }
@@ -277,7 +274,7 @@ class lp_core_solver_base {
     bool non_basis_has_no_doubles() const;
 
     bool basis_is_correctly_represented_in_heading() const ;
-    bool non_basis_is_correctly_represented_in_heading() const ;
+    bool non_basis_is_correctly_represented_in_heading(std::list<unsigned>*) const ;
 
     bool basis_heading_is_correct() const;
 
@@ -416,6 +413,7 @@ class lp_core_solver_base {
                 TRACE("lp_core", tout << "inf col "; print_column_info(j, tout) << "\n";);
                 return false;
             }
+
         return true;
     }
 

src/math/lp/lp_core_solver_base_def.h

@@ -56,7 +56,7 @@ lp_core_solver_base(static_matrix<T, X> & A,
     m_column_types(column_types),
     m_lower_bounds(lower_bound_values),
     m_upper_bounds(upper_bound_values),
-    m_basis_sort_counter(0),
+    m_nbasis_sort_counter(0),
     m_tracing_basis_changes(false),
     m_touched_rows(nullptr),
     m_look_for_feasible_solution_only(false) {
@@ -133,37 +133,6 @@ print_statistics(char const* str, X cost, std::ostream & out) {
         << ", nonzeros = " <<  m_A.number_of_non_zeroes() << std::endl;
 }
 
-template <typename T, typename X> bool lp_core_solver_base<T, X>::
-print_statistics_with_iterations_and_check_that_the_time_is_over(std::ostream & str) {
-    unsigned total_iterations = inc_total_iterations();
-    if (m_settings.report_frequency != 0)  {
-        if (m_settings.print_statistics && (total_iterations % m_settings.report_frequency == 0)) {
-            print_statistics("", X(), str);
-        }
-    }
-    return time_is_over();
-}
-
-template <typename T, typename X> bool lp_core_solver_base<T, X>::
-print_statistics_with_iterations_and_nonzeroes_and_cost_and_check_that_the_time_is_over(char const* str, std::ostream & out) {
-    unsigned total_iterations = inc_total_iterations();
-    if (m_settings.report_frequency != 0)
-        if (m_settings.print_statistics && (total_iterations % m_settings.report_frequency == 0)) {
-            print_statistics(str, get_cost(), out);
-        }
-    return time_is_over();
-}
-
-template <typename T, typename X> bool lp_core_solver_base<T, X>::
-print_statistics_with_cost_and_check_that_the_time_is_over(X cost, std::ostream & out) {
-    unsigned total_iterations = inc_total_iterations();
-    if (m_settings.report_frequency != 0)
-        if (m_settings.print_statistics && (total_iterations % m_settings.report_frequency == 0)) {
-            print_statistics("", cost, out);
-        }
-    return time_is_over();
-}
-
 template <typename T, typename X> bool lp_core_solver_base<T, X>::
 column_is_dual_feasible(unsigned j) const {
     switch (m_column_types[j]) {
@@ -194,18 +163,6 @@ d_is_not_positive(unsigned j) const {
     return m_d[j] <= numeric_traits<T>::zero();    
 }
 
-
-template <typename T, typename X> bool lp_core_solver_base<T, X>::
-time_is_over() {
-    if (m_settings.get_cancel_flag()) {
-        m_status = lp_status::TIME_EXHAUSTED;
-        return true;
-    }
-    else {
-        return false;
-    }
-}
-
 template <typename T, typename X> void lp_core_solver_base<T, X>::
 rs_minus_Anx(vector<X> & rs) {
     unsigned row = m_m();
@@ -360,15 +317,42 @@ basis_is_correctly_represented_in_heading() const {
     return true;
 }
 template <typename T, typename X> bool lp_core_solver_base<T, X>::
-non_basis_is_correctly_represented_in_heading() const {
+non_basis_is_correctly_represented_in_heading(std::list<unsigned>* non_basis_list) const {
     for (unsigned i = 0; i < m_nbasis.size(); i++) 
         if (m_basis_heading[m_nbasis[i]] !=  - static_cast<int>(i) - 1)
             return false;
 
     for (unsigned j = 0; j < m_A.column_count(); j++) 
         if (m_basis_heading[j] >= 0)
             lp_assert(static_cast<unsigned>(m_basis_heading[j]) < m_A.row_count() && m_basis[m_basis_heading[j]] == j);
-
+
+    if (non_basis_list == nullptr) return true;
+
+    std::unordered_set<unsigned> nbasis_set(this->m_nbasis.size());
+    for (unsigned j : this->m_nbasis) 
+        nbasis_set.insert(j);
+
+    if (non_basis_list->size() != nbasis_set.size()) {
+        TRACE("lp_core", tout << "non_basis_list.size() = " << non_basis_list->size() << ", nbasis_set.size() = " << nbasis_set.size() << "\n";);
+        return false;
+    }
+    for (auto it = non_basis_list->begin(); it != non_basis_list->end(); it++) {
+        if (nbasis_set.find(*it) == nbasis_set.end()) {
+            TRACE("lp_core", tout << "column " << *it << " is in m_non_basis_list but not in m_nbasis\n";);
+            return false;
+        }
+    }
+
+    // check for duplicates in m_non_basis_list
+    nbasis_set.clear();
+    for (auto it = non_basis_list->begin(); it != non_basis_list->end(); it++) {
+        if (nbasis_set.find(*it) != nbasis_set.end()) {
+            TRACE("lp_core", tout << "column " << *it << " is in m_non_basis_list twice\n";);
+            return false;
+        }
+        nbasis_set.insert(*it);
+    }
+
     return true;
 }
 
@@ -390,7 +374,7 @@ template <typename T, typename X> bool lp_core_solver_base<T, X>::
     if (!basis_is_correctly_represented_in_heading()) 
         return false;    
 
-    if (!non_basis_is_correctly_represented_in_heading()) 
+    if (!non_basis_is_correctly_represented_in_heading(nullptr)) 
         return false;
 
     return true;

src/math/lp/lp_primal_core_solver.h

@@ -592,7 +592,7 @@ namespace lp {
             theta = zero_of_type<X>();
         }
     }
-
+    bool correctly_moved_to_bounds(lpvar) const;
     bool column_is_benefitial_for_entering_basis(unsigned j) const;
     void init_infeasibility_costs();
     void print_column(unsigned j, std::ostream &out);

src/math/lp/lp_primal_core_solver_def.h

@@ -40,49 +40,57 @@ void lp_primal_core_solver<T, X>::sort_non_basis() {
                 if (ca != 0 && cb == 0) return true;
                 return ca < cb;
             });
-     
-    m_non_basis_list.clear();
-    // reinit m_basis_heading
-    for (unsigned j = 0; j < this->m_nbasis.size(); j++) {
-        unsigned col = this->m_nbasis[j];
-        this->m_basis_heading[col] = - static_cast<int>(j) - 1;
-        m_non_basis_list.push_back(col);
+    m_non_basis_list.resize(this->m_nbasis.size());
+    // initialize m_non_basis_list from m_nbasis by using an iterator on m_non_basis_list
+    auto it = m_non_basis_list.begin();
+    unsigned j = 0;
+    for (; j < this->m_nbasis.size(); j++, ++it) {
+        unsigned col = *it = this->m_nbasis[j];
+        this->m_basis_heading[col] = -static_cast<int>(j) - 1;
     }
 }
 
+template <typename T, typename X>
+bool lp_primal_core_solver<T, X>::correctly_moved_to_bounds(unsigned j) const {
+    switch (this->m_column_types[j]) {
+    case column_type::fixed:
+        return this->m_x[j] == this->m_lower_bounds[j];
+    case column_type::boxed:
+        return this->m_x[j] == this->m_lower_bounds[j] || this->m_x[j] == this->m_upper_bounds[j];
+    case column_type::lower_bound:
+        return this->m_x[j] == this->m_lower_bounds[j];
+    case column_type::upper_bound:
+        return this->m_x[j] == this->m_upper_bounds[j];
+    case column_type::free_column:
+        return true;
+    default:
+        UNREACHABLE();
+        return false;
+    }
+}
 
 
 template <typename T, typename X>
 bool lp_primal_core_solver<T, X>::column_is_benefitial_for_entering_basis(unsigned j) const {
     const T& dj = this->m_d[j];
-    TRACE("lar_solver", tout << "dj=" << dj << "\n";); 
+    if (dj.is_zero()) return false;
+    TRACE("lar_solver", tout << "d[" << j <<"] = " << dj << "\n";); 
+    SASSERT(correctly_moved_to_bounds(j));
     switch (this->m_column_types[j]) {
     case column_type::fixed:  break;
     case column_type::free_column:
-        if (!is_zero(dj))
-            return true;
-        break;
+        return true;
     case column_type::lower_bound:
         if (dj > zero_of_type<T>()) return true;
-        if (dj < 0 && this->m_x[j] > this->m_lower_bounds[j]){
-            return true;
-        }
         break;
     case column_type::upper_bound:
         if (dj < zero_of_type<T>()) return true;
-        if (dj > 0 && this->m_x[j] < this->m_upper_bounds[j]) {
-            return true;
-        }
         break;
     case column_type::boxed:
-        if (dj > zero_of_type<T>()) {
-            if (this->m_x[j] < this->m_upper_bounds[j])
-                return true;
-            break;
-        } else if (dj < zero_of_type<T>()) {
-            if (this->m_x[j] > this->m_lower_bounds[j])
-                return true;
-        }
+        if (dj > zero_of_type<T>() && this->m_x[j] == this->m_lower_bounds[j])
+            return true;
+        if (dj < zero_of_type<T>() && this->m_x[j] == this->m_upper_bounds[j])
+            return true;
         break;
     default:
         UNREACHABLE();

src/math/lp/lp_primal_core_solver_tableau_def.h

@@ -44,19 +44,22 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::advance_on_e
     advance_on_entering_and_leaving_tableau(entering, leaving, t);
 }
 
+
  template <typename T, typename X> int lp_primal_core_solver<T, X>::choose_entering_column_tableau() {
     //this moment m_y = cB * B(-1)
-    unsigned number_of_benefitial_columns_to_go_over =  get_number_of_non_basic_column_to_try_for_enter();
-
-    if (number_of_benefitial_columns_to_go_over == 0)
-        return -1;
-    if (this->m_basis_sort_counter == 0) {
+    if (this->m_nbasis_sort_counter == 0) {
         sort_non_basis();
-        this->m_basis_sort_counter = 20;
+        this->m_nbasis_sort_counter = 20;
     }
     else {
-        this->m_basis_sort_counter--;
+        this->m_nbasis_sort_counter--;
+        SASSERT(non_basis_is_correctly_represented_in_heading(&m_non_basis_list));
     }
+    unsigned number_of_benefitial_columns_to_go_over =  get_number_of_non_basic_column_to_try_for_enter();
+
+    if (number_of_benefitial_columns_to_go_over == 0)
+        return -1;
+
     unsigned j_nz = this->m_m() + 1; // this number is greater than the max column size
     std::list<unsigned>::iterator entering_iter = m_non_basis_list.end();
     unsigned n = 0;
@@ -98,7 +101,8 @@ unsigned lp_primal_core_solver<T, X>::solve() {
     }
 
     do {
-        if (this->print_statistics_with_iterations_and_nonzeroes_and_cost_and_check_that_the_time_is_over( "feas t", * this->m_settings.get_message_ostream())) {
+        if (this->m_settings.get_cancel_flag()) {
+            this->set_status(lp_status::CANCELLED);
             return this->total_iterations();
         }
         if (this->m_settings.use_tableau_rows()) {
@@ -256,8 +260,6 @@ template <typename T, typename X> int lp_primal_core_solver<T, X>::find_leaving_
 }
 template <typename T, typename X> void lp_primal_core_solver<T, X>::init_run_tableau() {
         lp_assert(basis_columns_are_set_correctly());
-        this->m_basis_sort_counter = 0; // to initiate the sort of the basis
-        //  this->set_total_iterations(0);
         this->iters_with_no_cost_growing() = 0;
 		lp_assert(this->inf_heap_is_correct());
         if (this->current_x_is_feasible() && this->m_look_for_feasible_solution_only)