removed calls to settings.random_next() from assert statements

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

src/util/lp/emonomials.cpp

@@ -21,6 +21,7 @@
 
 #include "util/lp/emonomials.h"
 #include "util/lp/nla_defs.h"
+#include "util/lp/nla_core.h"
 
 namespace nla {
 
@@ -339,11 +340,11 @@ namespace nla {
         }        
     }
 
-   std::ostream& emonomials::display(std::ostream& out) const {
+std::ostream& emonomials::display(const core& cr, std::ostream& out) const {
        out << "monomials\n";
        unsigned idx = 0;
        for (auto const& m : m_monomials) {
-           out << (idx++) << ": " << m << "\n";
+           out << (idx++) << ": " << pp_mon(cr, m) << "\n";
        }
        out << "use lists\n";
        idx = 0;

src/util/lp/emonomials.h

@@ -27,6 +27,8 @@
 
 namespace nla {
 
+class core;
+
 class emonomials : public var_eqs_merge_handler {
     mutable svector<lpvar> m_find_key;
     /**
@@ -275,7 +277,7 @@ public:
     /**
        \brief display state of emonomials
     */
-    std::ostream& display(std::ostream& out) const;
+    std::ostream& display(const core&, std::ostream& out) const;
 
     /**
        \brief
@@ -291,6 +293,15 @@ public:
     bool is_monomial_var(lpvar v) const { return m_var2index.get(v, UINT_MAX) != UINT_MAX; }
 };
 
-inline std::ostream& operator<<(std::ostream& out, emonomials const& m) { return m.display(out); }
+struct pp_emons {
+    const core&       m_c;
+    const emonomials& m_em;
+    pp_emons(const core& c, const emonomials& e): m_c(c), m_em(e) {}
+    inline std::ostream& display(std::ostream& out) const {
+        return m_em.display(m_c, out);
+    }
+};
+
+inline std::ostream& operator<<(std::ostream& out, pp_emons const& p) { return p.display(out); }
 
 }

src/util/lp/lar_core_solver_def.h

@@ -300,10 +300,9 @@ void lar_core_solver::solve() {
             if (snapped)
                 m_r_solver.solve_Ax_eq_b();
         }
-        if (m_r_solver.m_look_for_feasible_solution_only)
+        if (m_r_solver.m_look_for_feasible_solution_only) //todo : should it be set?
             m_r_solver.find_feasible_solution();
         else {
-            TRACE("lar_solver", tout << "solve\n";);
             m_r_solver.solve();
         }
         lp_assert(!settings().use_tableau() || r_basis_is_OK());

src/util/lp/lp_core_solver_base.h

@@ -575,6 +575,10 @@ public:
     }
 
     std::ostream& print_column_info(unsigned j, std::ostream & out) const {
+        if (j >= m_lower_bounds.size()) {
+            out << "[" << j << "] is not present\n";
+            return out;
+        }
         out << "[" << j << "],\tname = "<< column_name(j) << "\t";
         switch (m_column_types[j]) {
         case column_type::fixed:

src/util/lp/monomial.h

@@ -68,19 +68,8 @@ public:
     void sort_rvars() {
         std::sort(m_rvars.begin(), m_rvars.end());
     }
-    std::ostream& display(std::ostream& out) const {
-        // out << "v" << var() << " := ";
-        // if (sign()) out << "- ";
-        // for (lpvar v : vars()) out << "v" << v << " ";
-        SASSERT(false);
-        return out;
-    }
 };
 
-inline std::ostream& operator<<(std::ostream& out, monomial const& m) {
-    SASSERT(false);
-    return m.display(out);
-}
 
 typedef std::unordered_map<lpvar, rational> variable_map_type;
 template <typename T>

src/util/lp/nla_basics_lemmas.cpp

@@ -30,7 +30,7 @@ bool basics::basic_sign_lemma_on_two_monomials(const monomial& m, const monomial
     const rational& sign = m.rsign() * n.rsign();
      if (val(m) == val(n) * sign)
         return false;
-    TRACE("nla_solver", tout << "sign contradiction:\nm = " << m << "n= " << n << "sign: " << sign << "\n";);
+     TRACE("nla_solver", tout << "sign contradiction:\nm = " << pp_mon(c(), m) << "n= " << pp_mon(c(), n) << "sign: " << sign << "\n";);
     generate_sign_lemma(m, n, sign);
     return true;
 }

src/util/lp/nla_core.cpp

@@ -1277,11 +1277,8 @@ void core::add_equivalence_maybe(const lp::lar_term *t, lpci c0, lpci c1) {
 
 // x is equivalent to y if x = +- y
 void core::init_vars_equivalence() {
-    /*       SASSERT(m_evars.empty());*/
     collect_equivs();
-    /*        TRACE("nla_solver_details", tout << "number of equivs = " << m_evars.size(););*/
+    //    SASSERT(tables_are_ok());
-        
-    SASSERT((settings().random_next() % 100) || tables_are_ok());
 }
     
 bool core:: tables_are_ok() const {
@@ -1339,6 +1336,7 @@ void core::init_search() {
 }
 
 void core::init_to_refine() {
+    TRACE("nla_solver", tout << "emons:" << pp_emons(*this, m_emons););
     m_to_refine.clear();
     for (auto const & m : m_emons) 
         if (!check_monomial(m)) 

src/util/lp/static_matrix.h

@@ -48,7 +48,10 @@ struct row_cell {
     unsigned & offset() { return m_offset;}
             
 };
-
+template <typename T>
+std::ostream& operator<<(std::ostream& out, const row_cell<T>& rc) {
+    return out << "(m_j=" << rc.m_j << ", m_offset= " << rc.m_offset << ", m_value=" << rc.m_value << ")";   
+}
 struct empty_struct {};
 typedef row_cell<empty_struct> column_cell;