Merge pull request #6905 from Z3Prover/unit_prop_on_monomials

src/math/lp/bound_analyzer_on_row.h

@@ -26,6 +26,8 @@ Revision History:
 #include "math/lp/test_bound_analyzer.h"
 
 namespace lp {
+
+
 template <typename C, typename B> // C plays a role of a container, B - lp_bound_propagator
 class bound_analyzer_on_row {
     const C&                           m_row;
@@ -91,39 +93,17 @@ public :
     }
 
     bool bound_is_available(unsigned j, bool lower_bound) {
-        return (lower_bound && lower_bound_is_available(j)) ||
-            (!lower_bound && upper_bound_is_available(j));
-    }
-
-    bool upper_bound_is_available(unsigned j) const {
-        switch (m_bp.get_column_type(j)) {
-        case column_type::fixed:
-        case column_type::boxed:
-        case column_type::upper_bound:
-            return true;
-        default:
-            return false;
-        }
-    }
-
-    bool lower_bound_is_available(unsigned j) const {
-        switch (m_bp.get_column_type(j)) {
-        case column_type::fixed:
-        case column_type::boxed:
-        case column_type::lower_bound:
-            return true;
-        default:
-            return false;
-        }
+        return (lower_bound && m_bp.lower_bound_is_available(j)) ||
+            (!lower_bound && m_bp.upper_bound_is_available(j));
     }
 
     const impq & ub(unsigned j) const {
-        lp_assert(upper_bound_is_available(j));
+        lp_assert(m_bp.upper_bound_is_available(j));
         return m_bp.get_upper_bound(j);
     }
 
     const impq & lb(unsigned j) const {
-        lp_assert(lower_bound_is_available(j));
+        lp_assert(m_bp.lower_bound_is_available(j));
         return m_bp.get_lower_bound(j);
     }
 
@@ -301,10 +281,32 @@ public :
     //     */
     // }
 
-    void limit_j(unsigned j, const mpq& u, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict){
-        m_bp.try_add_bound(u, j, is_lower_bound, coeff_before_j_is_pos, m_row_index, strict);
+    void limit_j(unsigned bound_j, const mpq& u, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict)
+    {
+        unsigned row_index = this->m_row_index;
+        auto* lar = &m_bp.lp();
+        auto explain = [bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index, lar]() {
+            TRACE("bound_analyzer", tout << "explain_bound_on_var_on_coeff, bound_j = " << bound_j << ", coeff_before_j_is_pos = " << coeff_before_j_is_pos << ", is_lower_bound = " << is_lower_bound << ", strict = " << strict << ", row_index = " << row_index << "\n";);
+            int bound_sign = (is_lower_bound ? 1 : -1);
+            int j_sign = (coeff_before_j_is_pos ? 1 : -1) * bound_sign;
+
+            SASSERT(!tv::is_term(bound_j));
+            u_dependency* ret = nullptr;
+            for (auto const& r : lar->get_row(row_index)) {
+                unsigned j = r.var();
+                if (j == bound_j)
+                    continue;
+                mpq const& a = r.coeff();
+                int a_sign = is_pos(a) ? 1 : -1;
+                int sign = j_sign * a_sign;
+                u_dependency* witness = sign > 0 ? lar->get_column_upper_bound_witness(j) : lar->get_column_lower_bound_witness(j);
+                ret = lar->join_deps(ret, witness);
+            }
+            return ret;
+        };
+        m_bp.add_bound(u, bound_j, is_lower_bound, strict, explain);
     }
-    
+
     void advance_u(unsigned j) {
         m_column_of_u = (m_column_of_u == -1) ? j : -2;
     }
@@ -335,6 +337,9 @@ public :
             break;
         }
     }   
+
 };
+
+
 }
 

src/math/lp/core_solver_pretty_printer_def.h

@@ -279,10 +279,12 @@ template <typename T, typename X> void core_solver_pretty_printer<T, X>::print()
         print_row(i);
     }
     m_out << std::endl;
-    if (m_core_solver.inf_heap().size()) {
-        m_out << "inf columns: ";
+    if (!m_core_solver.inf_heap().empty()) {
+        m_out << "inf columns: size() = " << m_core_solver.inf_heap().size() << std::endl;
         print_vector(m_core_solver.inf_heap(), m_out);
         m_out << std::endl;
+    } else {
+        m_out << "inf columns: none\n";
     }
 }
 

src/math/lp/gomory.cpp

@@ -417,7 +417,7 @@ int gomory::find_basic_var() {
 }
 
 lia_move gomory::operator()() {
-    lra.move_non_basic_columns_to_bounds(true);
+    lra.move_non_basic_columns_to_bounds();
     int j = find_basic_var();
     if (j == -1)
         return lia_move::undef;

src/math/lp/implied_bound.h

@@ -21,37 +21,40 @@ Revision History:
 #include "math/lp/lp_settings.h"
 #include "math/lp/lar_constraints.h"
 namespace lp {
-struct implied_bound {
+class implied_bound {
+    public:
     mpq m_bound;
-    unsigned m_j; // the column for which the bound has been found
+    // It is either the column for which the bound has been found, or,
+    // in the case the column was created as
+    // the slack variable to a term, it is the term index.
+    // It is the same index that was returned by lar_solver::add_var(), or
+    // by lar_solver::add_term()
+    unsigned m_j; 
     bool m_is_lower_bound;
-    bool m_coeff_before_j_is_pos;
-    unsigned m_row_or_term_index;
     bool m_strict;
+    private:
+    std::function<u_dependency*()> m_explain_bound = nullptr;
+    public:
+    // s is expected to be the pointer to lp_bound_propagator.
+    u_dependency* explain_implied() const { return m_explain_bound(); }
+    void set_explain(std::function<u_dependency*()> f) { m_explain_bound = f; }
     lconstraint_kind kind() const {
         lconstraint_kind k = m_is_lower_bound? GE : LE;
         if (m_strict)
             k = static_cast<lconstraint_kind>(k / 2);
         return k;
     }
-    bool operator==(const implied_bound & o) const {
-        return m_j == o.m_j && m_is_lower_bound == o.m_is_lower_bound && m_bound == o.m_bound &&
-            m_coeff_before_j_is_pos == o.m_coeff_before_j_is_pos &&
-            m_row_or_term_index == o.m_row_or_term_index && m_strict == o.m_strict;
-    }
     implied_bound(){}
     implied_bound(const mpq & a,
                   unsigned j,
-                  bool lower_bound,
-                  bool coeff_before_j_is_pos,
-                  unsigned row_or_term_index,
-                  bool strict):
+                  bool is_lower_bound,
+                  bool is_strict,
+                  std::function<u_dependency*()> get_dep):
         m_bound(a),
         m_j(j),
-        m_is_lower_bound(lower_bound),
-        m_coeff_before_j_is_pos(coeff_before_j_is_pos),
-        m_row_or_term_index(row_or_term_index),
-        m_strict(strict) {
+        m_is_lower_bound(is_lower_bound),
+        m_strict(is_strict),
+        m_explain_bound(get_dep) {
     }
 };
 }

src/math/lp/int_branch.cpp

@@ -24,7 +24,7 @@ namespace lp {
 int_branch::int_branch(int_solver& lia):lia(lia), lra(lia.lra) {}
 
 lia_move int_branch::operator()() {
-    lra.move_non_basic_columns_to_bounds(true);
+    lra.move_non_basic_columns_to_bounds();
     int j = find_inf_int_base_column();
     return j == -1? lia_move::sat : create_branch_on_column(j);        
 }

src/math/lp/int_cube.cpp

@@ -43,7 +43,7 @@ namespace lp {
         if (st != lp_status::FEASIBLE && st != lp_status::OPTIMAL) {
             TRACE("cube", tout << "cannot find a feasible solution";);
             lra.pop();
-            lra.move_non_basic_columns_to_bounds(false);
+            lra.move_non_basic_columns_to_bounds();
             // it can happen that we found an integer solution here
             return !lra.r_basis_has_inf_int()? lia_move::sat: lia_move::undef;
         }