restore m_crossed* and create lemmas

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

src/math/lp/lar_solver.cpp

@@ -2361,8 +2361,6 @@ namespace lp {
     // dep is the reason for the new bound
 
     void lar_solver::set_infeasible_column_and_witness(unsigned j, bool lower_bound, u_dependency* dep) {
-        bool was_feas = column_is_feasible(j);
-        bool in_heap = m_mpq_lar_core_solver.m_r_solver.inf_heap().contains(j);
         SASSERT(m_crossed_bounds_deps == nullptr && m_crossed_bounds_deps == nullptr);
         set_status(lp_status::INFEASIBLE);
         m_crossed_bounds_column = j;

src/math/lp/lar_solver.h

@@ -79,7 +79,7 @@ class lar_solver : public column_namer {
     stacked_value<simplex_strategy_enum> m_simplex_strategy;
     // such can be found at the initialization step: u < l
     lpvar m_crossed_bounds_column;
-    u_dependency* m_crossed_bounds_deps;   
+    u_dependency* m_crossed_bounds_deps;
     lar_core_solver m_mpq_lar_core_solver;
     int_solver* m_int_solver = nullptr;
     bool m_need_register_terms = false;
@@ -142,6 +142,13 @@ class lar_solver : public column_namer {
     inline void clear_columns_with_changed_bounds() { m_columns_with_changed_bounds.reset(); }
  public:   
     void insert_to_columns_with_changed_bounds(unsigned j);
+    const u_dependency* crossed_bounds_deps() const { return m_crossed_bounds_deps;}
+    u_dependency*& crossed_bounds_deps() { return m_crossed_bounds_deps;}
+
+    lpvar crossed_bounds_column() const { return m_crossed_bounds_column; }
+    lpvar& crossed_bounds_column() { return m_crossed_bounds_column; } 
+        
+
  private:   
     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);

src/math/lp/monomial_bounds.cpp

@@ -258,32 +258,30 @@ namespace nla {
         }
     }
 
-    bool monomial_bounds::unit_propagate() {  
-        unsigned sz = 0;
-        vector<lpvar> monics_vars;
-        for (auto const& m : c().m_emons) {
-            monics_vars.push_back(m.var());
-            sz++;
-        }
-        unsigned l = this->random();
-        for (unsigned i = 0; i < sz; ++i) {
-            lpvar v = monics_vars[(i + l) % sz];
-            if (!unit_propagate(c().m_emons[v])) {
-                return false;
-            }
-        }
-
-        return true;    
+    void monomial_bounds::unit_propagate() {  
+        for (auto const& m : c().m_emons)
+            unit_propagate(m);
     }
 
-// returns false if and only if there is a conflict
-    bool monomial_bounds::unit_propagate(monic const& m) {
+    void monomial_bounds::check_for_conflict() {
+        if (c().lra.crossed_bounds_deps() != nullptr) {
+            new_lemma lemma(c(), "fixed-values");
+            lp::explanation ex;
+            c().lra.fill_explanation_from_crossed_bounds_column(ex);
+            lemma &= ex;
+            c().lra.crossed_bounds_deps() = nullptr;
+            c().lra.crossed_bounds_column() = null_lpvar;     
+            c().lra.set_status(lp::lp_status::OPTIMAL);           
+        }
+    }
+
+    void monomial_bounds::unit_propagate(monic const& m) {
         m_propagated.reserve(m.var() + 1, false);
         if (m_propagated[m.var()])
-            return true;
+            return;
 
         if (!is_linear(m))
-            return true;
+            return;
         
         c().trail().push(set_bitvector_trail(m_propagated, m.var()));
         lpvar zero_fixed = null_lpvar, non_fixed = null_lpvar;
@@ -303,8 +301,7 @@ namespace nla {
         if (zero_fixed != null_lpvar) {
             // the m.var() has to have a zero value
             u_dependency* d = this->dep.mk_join(c().lra.get_column_lower_bound_witness(zero_fixed),
-                                                c().lra.get_column_upper_bound_witness(zero_fixed));
-
+                                                c().lra.get_column_upper_bound_witness(zero_fixed));            
             c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, mpq(0), d);
         } else if (non_fixed != null_lpvar) {
             u_dependency* d = nullptr;
@@ -330,7 +327,6 @@ namespace nla {
                     bool strict = b.y.is_pos();
                     c().lra.update_column_type_and_bound(m.var(), strict ? lp::lconstraint_kind::GT : lp::lconstraint_kind::GE, k * b.x, d);
                 }
-
             } else {
                 d = c().lra.get_column_upper_bound_witness(non_fixed);
                 if (d) {
@@ -358,12 +354,9 @@ namespace nla {
             SASSERT(k.is_pos() || k.is_neg());
             // we have m = k: m.var() getting the bounds witnesses of all fixed variables
             c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, d);
-        }        
-        if (c().lra.get_status() == lp::lp_status::INFEASIBLE) {
-            TRACE("nla_solver", tout << "conflict in unit_propagate\n";);
-            return false;
         }
-        return true;
+        check_for_conflict();
+        SASSERT (c().lra.get_status() != lp::lp_status::INFEASIBLE);
     }
     bool monomial_bounds::is_linear(monic const& m) {
         unsigned non_fixed = 0;

src/math/lp/monomial_bounds.h

@@ -32,12 +32,13 @@ namespace nla {
 
         // monomial propagation
         bool_vector m_propagated;
-        bool unit_propagate(monic const& m);
+        void unit_propagate(monic const& m);
         bool is_linear(monic const& m);
         rational fixed_var_product(monic const& m);
     public:
         monomial_bounds(core* core);
         void propagate();
-        bool unit_propagate();
+        void unit_propagate();
+        void check_for_conflict();
     }; 
 }