experiment with tighten_bound

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

src/math/lp/dioph_eq.cpp

@@ -1156,6 +1156,12 @@ namespace lp {
             return lra.print_expl(out, ex);
         }
 
+        bool var_is_fresh(unsigned j) const {
+            bool ret = m_fresh_k2xt_terms.has_second_key(j);
+            SASSERT(!ret || m_var_register.local_to_external(j) == UINT_MAX);
+            return ret;
+        }
+
         bool has_fresh_var(unsigned row_index) const {
             for (const auto& p : m_e_matrix.m_rows[row_index]) {
                 if (var_is_fresh(p.var()))
@@ -1363,7 +1369,7 @@ namespace lp {
             return weight;
         }
 
-        bool term_has_int_inv_vars(unsigned j) const {
+        bool term_has_int_inf_vars(unsigned j) const {
             for (const auto & p: lra.get_term(j)) {
                 if (lia.column_is_int_inf(p.var()))
                     return true;
@@ -1381,7 +1387,7 @@ namespace lp {
                     !lra.column_has_term(j) ||
                     lra.column_is_free(j) ||
                     !lia.column_is_int(j) ||
-                    !term_has_int_inv_vars(j)) {
+                    !term_has_int_inf_vars(j)) {
                     cleanup.push_back(j);
                     continue;
                 }
@@ -1396,8 +1402,7 @@ namespace lp {
             lia_move r = lia_move::undef;
             // Process sorted terms
             TRACE("dio", 
-                  tout << "changed terms:";
+                  tout << "changed terms:"; for (auto j : sorted_changed_terms) tout << j << " "; tout << std::endl;
-                  for (auto j : sorted_changed_terms) lra.print_term(lra.get_term(j), tout) << " - x" <<j << " = 0" << std::endl;
                   print_S(tout);
                   print_bounds(tout);
             );
@@ -1409,14 +1414,6 @@ namespace lp {
                     break;
                 }                
             }
-            // Process sorted terms
-            TRACE("dio", 
-                  tout << "after tighten_terms_with_S():\n";
-                  print_S(tout);
-                  for (auto j : sorted_changed_terms) tout << j << " "; tout << std::endl;
-                  print_bounds(tout);
-            );
-            
             for (unsigned j : cleanup) {
                 m_changed_terms.remove(j);
             }
@@ -1495,7 +1492,7 @@ namespace lp {
                 term_to_lar_solver(remove_fresh_vars(create_term_from_subst_space())));
 
             mpq g = gcd_of_coeffs(m_espace.m_data, true);
-            TRACE("dio", tout << "after process_q_with_S\nt:";  print_term_o(create_term_from_subst_space(), tout) << std::endl; tout << "g:" << g << std::endl;);
+            TRACE("dioph_eq", tout << "after process_q_with_S\nt:";  print_term_o(create_term_from_subst_space(), tout) << std::endl; tout << "g:" << g << std::endl;);
 
             if (g.is_one())
                 return lia_move::undef;
@@ -1590,8 +1587,7 @@ namespace lp {
             lia.offset() = floor(rs);
             lia.is_upper() = true;
             m_report_branch = true;
-            enable_trace("dio");
+            TRACE("dioph_eq", tout << "prepare branch, t:";
-            TRACE("dio", tout << "prepare branch, t:";
                   print_lar_term_L(t, tout)
                   << " <= " << lia.offset()
                   << std::endl;
@@ -1641,52 +1637,9 @@ namespace lp {
             }
         }
 
-        struct prop_bound {
-            mpq m_bound;
-            unsigned m_j;
-            bool m_is_low;
-            bool m_strict;
-            u_dependency* m_dep;
-            prop_bound(const mpq& b, unsigned j, bool is_low, bool strict, u_dependency* dep): m_bound(b), m_j(j), m_is_low(is_low), m_strict(strict), m_dep(dep) {}
-        };
-        std_vector<prop_bound> m_prop_bounds;
         lia_move propagate_bounds_on_tightened_columns() {
-            for (unsigned j : m_tightened_columns) {
-                m_prop_bounds.clear();
-                auto t = lra.get_term(j);
-                t.add_monomial(mpq(-1), j);
-                bound_analyzer_on_row<lar_term, dioph_eq::imp>::analyze_row(t, impq(0), *this);
-                for (const auto & pb: m_prop_bounds) {                
-                    lconstraint_kind kind = get_bound_kind(!pb.m_is_low, pb.m_strict);            
-                    lra.update_column_type_and_bound(pb.m_j, kind, pb.m_bound, pb.m_dep);
-                }
-                lp_status st = lra.find_feasible_solution();
-                if ((int)st >= (int)lp::lp_status::FEASIBLE) {
-                    continue;
-                }
-                if (st == lp_status::CANCELLED) {
-                    return lia_move::undef;
-                }
-                SASSERT(st == lp_status::INFEASIBLE);
-                lra.get_infeasibility_explanation(m_infeas_explanation);
-                return lia_move::conflict;
-            }
             return lia_move::undef;
         }
-
-        lconstraint_kind get_bound_kind(bool upper, bool is_strict) {
-            if (upper) {
-                return is_strict ? lp::LT : lp::LE; 
-            }
-            else {
-                return is_strict ? lp::GT : lp::GE;
-            }
-        }
-        
-        void add_bound(mpq const& bound, unsigned j, bool is_low, bool strict, std::function<u_dependency* ()> explain_bound) {
-            m_prop_bounds.push_back({bound, j, is_low, strict, explain_bound()});
-
-        }
         // m_espace contains the coefficients of the term
         // m_c contains the fixed part of the term
         // m_tmp_l is the linear combination of the equations that removes the
@@ -1811,14 +1764,6 @@ namespace lp {
                 lra.stats().m_dio_tighten_conflicts++;
                 return lia_move::conflict;
             }
-            if (lra.settings().get_cancel_flag())
-                return lia_move::undef;
-
-            if (ret == lia_move::undef) {    
-                ret = propagate_bounds_on_tightened_columns();
-                if (ret == lia_move::conflict)
-                    lra.stats().m_dio_bound_propagation_conflicts++;
-            }
             return ret;
         }
 
@@ -2589,7 +2534,7 @@ namespace lp {
             if (h == UINT_MAX) return false;
             SASSERT(h == f_vector[ih]);
             if (min_ahk.is_one()) {
-                TRACE("dio", tout << "push to S:\n"; print_entry(h, tout););
+                TRACE("dioph_eq", tout << "push to S:\n"; print_entry(h, tout););
                 move_entry_from_f_to_s(kh, h);
                 eliminate_var_in_f(h, kh, kh_sign);
                 if (ih != f_vector.size() - 1) {
@@ -2602,12 +2547,6 @@ namespace lp {
             return true;
         }
 
-        bool var_is_fresh(unsigned j) const {
-            bool ret = m_fresh_k2xt_terms.has_second_key(j);
-            SASSERT(!ret || m_var_register.local_to_external(j) == UINT_MAX);
-            return ret;
-        }
-
     public:
         void explain(explanation& ex) {
             if (m_conflict_index == UINT_MAX) {

src/math/lp/int_solver.cpp

@@ -215,8 +215,14 @@ namespace lp {
         // Tighten bounds
         // expose at level of lar_solver so it can be invoked by theory_lra after back-jumping 
         // consider multi-round bound tightnening as well and deal with divergence issues.
+
+        unsigned m_bounds_refine_depth = 0;
+
         lia_move tighten_bounds() {
 
+            if (m_bounds_refine_depth > 10)
+                return lia_move::undef;
+
             struct bound_consumer {
                 imp& i;
                 bound_consumer(imp& i) : i(i) {}
@@ -227,11 +233,8 @@ namespace lp {
             bound_consumer bc(*this);
             std_vector<implied_bound> ibounds;
             lp_bound_propagator<bound_consumer> bp(bc, ibounds);
-            bp.init();
 
-            unsigned num_refined_bounds = 0;
+            auto set_conflict = [&](u_dependency * d1, u_dependency * d2) {
-
-            auto set_conflict = [&](unsigned j, u_dependency * d1, u_dependency * d2) {
                 ++settings().stats().m_bounds_tightening_conflicts;
                 for (auto e : lra.flatten(d1))
                     m_ex->push_back(e);
@@ -239,6 +242,7 @@ namespace lp {
                     m_ex->push_back(e);
             };
 
+            bool bounds_refined = false;
             auto refine_bound = [&](implied_bound const& ib) {
                 unsigned j = ib.m_j;
                 rational bound = ib.m_bound;
@@ -249,43 +253,46 @@ namespace lp {
                         return l_undef;
                     auto d = ib.explain_implied();
                     if (lra.column_has_upper_bound(j) && lra.column_upper_bound(j) < bound) {
-                        set_conflict(j, d, lra.get_column_upper_bound_witness(j));
+                        set_conflict(d, lra.get_column_upper_bound_witness(j));
                         return l_false;
                     }
-
+                    lra.update_column_type_and_bound(j, ib.m_strict ? lconstraint_kind::GT : lconstraint_kind::GE, bound, d);                    
-                    lra.update_column_type_and_bound(j, ib.m_strict ? lconstraint_kind::GT : lconstraint_kind::GE, bound, d);
+                } 
-                    ++num_refined_bounds;
+                else {
-                } else {
                     if (lra.column_is_int(j))
                         bound = floor(bound);
                     if (lra.column_has_upper_bound(j) && lra.column_upper_bound(j) <= bound)
                         return l_undef;
                     auto d = ib.explain_implied();
                     if (lra.column_has_lower_bound(j) && lra.column_lower_bound(j) > bound) {                        
-                        set_conflict(j, d, lra.get_column_lower_bound_witness(j));
+                        set_conflict(d, lra.get_column_lower_bound_witness(j));
                         return l_false;
                     }
-
                     lra.update_column_type_and_bound(j, ib.m_strict ? lconstraint_kind::LT : lconstraint_kind::LE, bound, d);
-                    ++num_refined_bounds;
                 }
+                ++settings().stats().m_bounds_tightenings;
+                bounds_refined = true;
                 return l_true;
             };
 
             for (unsigned row_index = 0; row_index < lra.row_count(); ++row_index) {
+                bp.init();
                 bound_analyzer_on_row<row_strip<mpq>, lp_bound_propagator<bound_consumer>>::analyze_row(
                     lra.A_r().m_rows[row_index],
                     zero_of_type<numeric_pair<mpq>>(),                    
                     bp);
 
-                settings().stats().m_bounds_tightenings += static_cast<unsigned>(ibounds.size());
                 for (auto const& ib : ibounds)
                     if (l_false == refine_bound(ib))
                         return lia_move::conflict;
-                ibounds.clear();
+            }
+            
+            if (bounds_refined) {
+                lra.trail().push(value_trail(m_bounds_refine_depth));
+                ++m_bounds_refine_depth;
             }
 
-            return num_refined_bounds > 0 ? lia_move::continue_with_check : lia_move::undef;
+            return bounds_refined  ? lia_move::continue_with_check : lia_move::undef;
         }
 
         
@@ -318,7 +325,6 @@ namespace lp {
             if (r == lia_move::undef && should_hnf_cut()) r = hnf_cut();
             if (r == lia_move::undef && should_gomory_cut()) r = gomory(lia).get_gomory_cuts(2);
             if (r == lia_move::undef && should_solve_dioph_eq()) r = solve_dioph_eq();
-            if (r == lia_move::undef) lra.remove_fixed_vars_from_base();
             if (r == lia_move::undef) r = int_branch(lia)();
             if (settings().get_cancel_flag()) r = lia_move::undef;        
             return r;

src/math/lp/lar_solver.h

@@ -160,7 +160,7 @@ class lar_solver : public column_namer {
  public:   
     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);
+	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(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);

src/math/lp/lp_settings.h

@@ -138,7 +138,6 @@ struct statistics {
     unsigned m_dio_rewrite_conflicts = 0;
     unsigned m_dio_branching_sats = 0;
     unsigned m_dio_branching_conflicts = 0;
-    unsigned m_dio_bound_propagation_conflicts = 0;
     unsigned m_bounds_tightening_conflicts = 0;
     unsigned m_bounds_tightenings = 0;
     ::statistics m_st = {};
@@ -186,7 +185,6 @@ struct statistics {
         st.update("arith-dio-branching-conflicts", m_dio_branching_conflicts);
         st.update("arith-bounds-tightening-conflicts", m_bounds_tightening_conflicts);
         st.update("arith-bounds-tightenings", m_bounds_tightenings);
-        st.update("arith-dio-propagation-conflicts", m_dio_bound_propagation_conflicts);
         st.copy(m_st);
     }
 };
@@ -260,7 +258,7 @@ private:
     bool             m_dio_enable_gomory_cuts = false;
     bool             m_dio_enable_hnf_cuts = true;
     unsigned         m_dio_branching_period = 100; //  do branching rarely
-    unsigned         m_dio_report_branch_with_term_tigthening_period = 10000000;
+    unsigned         m_dio_report_branch_with_term_tigthening_period = 10000000; // period of reporting the branch with term tigthening
 
 public:
     bool print_external_var_name() const { return m_print_external_var_name; }