allow gomory cut for a row with free non-basic vars

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

src/smt/theory_lra.cpp

@@ -2042,7 +2042,7 @@ public:
             m_eqs.reset();
             m_core.reset();
             m_params.reset();
-            for (auto const& ev : ex) {
+            for (auto const& ev : ex.m_explanation) {
                 if (!ev.first.is_zero()) { 
                     set_evidence(ev.second);
                 }
@@ -2096,39 +2096,40 @@ public:
         return r;
     }
 
-    niil::lemma m_lemma;
+    void process_lemma(const niil::lemma& lemma) {
- 
+        literal_vector core;
-    lbool check_aftermath_niil(lbool r) {
+        for (auto const& ineq : lemma) {
-        switch (r) {
+            bool is_lower = true, pos = true, is_eq = false;
-        case l_false: {            
-            literal_vector core;
-            for (auto const& ineq : m_lemma) {
-                bool is_lower = true, pos = true, is_eq = false;
                 
-                switch (ineq.m_cmp) {
+            switch (ineq.m_cmp) {
-                case lp::LE: is_lower = false; pos = false;  break;
+            case lp::LE: is_lower = false; pos = false;  break;
-                case lp::LT: is_lower = true;  pos = true; break;
+            case lp::LT: is_lower = true;  pos = true; break;
-                case lp::GE: is_lower = true;  pos = false;  break;
+            case lp::GE: is_lower = true;  pos = false;  break;
-                case lp::GT: is_lower = false; pos = true; break;
+            case lp::GT: is_lower = false; pos = true; break;
-                case lp::EQ: is_eq = true; pos = true; break;
+            case lp::EQ: is_eq = true; pos = true; break;
-                case lp::NE: is_eq = true; pos = false; break;
+            case lp::NE: is_eq = true; pos = false; break;
-                default: UNREACHABLE();
+            default: UNREACHABLE();
-                }
-                TRACE("arith", tout << "is_lower: " << is_lower << " pos " << pos << "\n";);
-                app_ref atom(m);
-                if (is_eq) {
-                    atom = mk_eq(ineq.m_term);
-                }
-                else {
-                    // create term >= 0 (or term <= 0)
-                    atom = mk_bound(ineq.m_term, rational::zero(), is_lower);
-                }
-                literal lit(ctx().get_bool_var(atom), pos);
-                core.push_back(~lit);
             }
-            set_conflict_or_lemma(core, false);
+            TRACE("arith", tout << "is_lower: " << is_lower << " pos " << pos << "\n";);
-            break;
+            app_ref atom(m);
+            if (is_eq) {
+                atom = mk_eq(ineq.m_term);
+            }
+            else {
+                // create term >= 0 (or term <= 0)
+                atom = mk_bound(ineq.m_term, rational::zero(), is_lower);
+            }
+            literal lit(ctx().get_bool_var(atom), pos);
+            core.push_back(~lit);
         }
+        set_conflict_or_lemma(core, false);
+    }
+ 
+    lbool check_aftermath_niil(lbool r, const niil::lemma & lemma) {
+        switch (r) {
+        case l_false:
+            process_lemma(lemma);
+            break;
         case l_true:
             if (assume_eqs()) {
                 return l_false;
@@ -2149,9 +2150,9 @@ public:
         if (!m_nra && !m_niil) return l_true;
         if (!m_switcher.need_check()) return l_true;
         m_a1 = nullptr; m_a2 = nullptr;
-        
+        niil::lemma lemma;
-        lbool r = m_nra? m_nra->check(m_explanation): m_niil->check(m_explanation, m_lemma);
+        lbool r = m_nra? m_nra->check(m_explanation): m_niil->check(m_explanation, lemma);
-        return m_nra? check_aftermath_nra(r) : check_aftermath_niil(r);
+        return m_nra? check_aftermath_nra(r) : check_aftermath_niil(r, lemma);
     }
 
     /**

src/util/lp/int_solver.cpp

@@ -104,11 +104,10 @@ bool int_solver::is_gomory_cut_target(const row_strip<mpq>& row) {
         j = p.var();
         if (!is_base(j) && (!at_bound(j) || !is_zero(get_value(j).y))) {
             TRACE("gomory_cut", tout << "row is not gomory cut target:\n";
-                  display_column(tout, j);
+                  display_column(tout, j););
-                  tout << "infinitesimal: " << !is_zero(get_value(j).y) << "\n";);
             return false;
         }
-    }
+	}
     return true;
 }
 
@@ -122,7 +121,6 @@ constraint_index int_solver::column_lower_bound_constraint(unsigned j) const {
     return m_lar_solver->get_column_lower_bound_witness(j);
 }
 
-
 bool int_solver::current_solution_is_inf_on_cut() const {
     const auto & x = m_lar_solver->m_mpq_lar_core_solver.m_r_x;
     impq v = m_t.apply(x);
@@ -150,6 +148,7 @@ lia_move int_solver::proceed_with_gomory_cut(unsigned j) {
         return create_branch_on_column(j);
 
     m_upper = true;
+
     return mk_gomory_cut(j, row);
 }
 
@@ -377,10 +376,17 @@ lia_move int_solver::make_hnf_cut() {
 #endif
     lia_move r =  m_hnf_cutter.create_cut(m_t, m_k, m_ex, m_upper, x0);
 
-    if (r == lia_move::cut) {      
+    m_lemma->clear();
+    m_lemma->push_back(ineq());
+    ineq & f_in = first_in();
+    mpq k;
+    bool upper;
+    lia_move r =  m_hnf_cutter.create_cut(f_in.m_term, k, *m_ex, upper, x0);
+    if (r == lia_move::cut) {
+        f_in.m_term.m_v = -k;
+        f_in.m_cmp = upper? lconstraint_kind::LE : GE;
         TRACE("hnf_cut",
-              m_lar_solver->print_term(m_t, tout << "cut:"); 
+              print_ineq(f_in, tout << "cut:"); 
-              tout << " <= " << m_k << std::endl;
               for (unsigned i : m_hnf_cutter.constraints_for_explanation()) {
                   m_lar_solver->print_constraint(i, tout);
               }              
@@ -861,7 +867,7 @@ bool int_solver::at_bound(unsigned j) const {
     case column_type::upper_bound:
         return  mpq_solver.m_upper_bounds[j] == get_value(j);
     default:
-        return false;
+        return true; // a free var is always at a bound
     }
 }
 
@@ -999,7 +1005,7 @@ lia_move int_solver::create_branch_on_column(int j) {
     TRACE("check_main_int", tout << "branching" << std::endl;);
     lp_assert(m_t.is_empty());
     lp_assert(j != -1);
-    m_t->add_coeff_var(mpq(1), m_lar_solver->adjust_column_index_to_term_index(j));
+    first_in().add_coeff_var(mpq(1), m_lar_solver->adjust_column_index_to_term_index(j));
     if (is_free(j)) {
         m_upper = true;
         m_k = mpq(0);

src/util/lp/int_solver.h

@@ -33,6 +33,31 @@ class lar_solver;
 template <typename T, typename X>
 struct lp_constraint;
 
+struct ineq {
+    lp::lconstraint_kind m_cmp;
+    lp::lar_term         m_term;
+    ineq(lp::lconstraint_kind cmp, const lp::lar_term& term) : m_cmp(cmp), m_term(term) {}
+    ineq() {} // empty constructor
+    void add_coeff_var(const mpq& c, unsigned j) {
+        m_term.add_coeff_var(c, j);
+    }
+    bool holds(const vector<impq> & x) const {
+        auto v = m_term.apply(x);
+        switch(m_cmp) {
+        case lconstraint_kind::LE: return v <= zero_of_type<impq>();
+        case lconstraint_kind::LT: return v <  zero_of_type<impq>();
+        case lconstraint_kind::GE: return v >= zero_of_type<impq>();
+        case lconstraint_kind::GT: return v >  zero_of_type<impq>();
+        case lconstraint_kind::EQ: return v == zero_of_type<impq>();
+        default:
+            lp_assert(false);
+            return false;
+        }
+    }
+    bool is_empty() const { return m_term.is_empty(); }
+};
+
+typedef vector<ineq> lemma;
 
 class int_solver {
 public:
@@ -54,7 +79,6 @@ public:
     mpq const& get_offset() const { return m_k; }
     explanation const& get_explanation() const { return m_ex; }
     bool is_upper() const { return m_upper; }
-
     bool is_base(unsigned j) const;
     bool is_real(unsigned j) const;
     const impq & lower_bound(unsigned j) const;
@@ -116,6 +140,7 @@ private:
     unsigned row_of_basic_column(unsigned j) const;
 
 public:
+    std::ostream & print_ineq(const ineq & in, std::ostream & out) const;
     void display_column(std::ostream & out, unsigned j) const;
     constraint_index column_upper_bound_constraint(unsigned j) const;
     constraint_index column_lower_bound_constraint(unsigned j) const;
@@ -140,6 +165,7 @@ public:
     int find_inf_int_nbasis_column() const;
     lia_move run_gcd_test();
     lia_move gomory_cut();
+    void add_free_vars_ineqs_to_lemma();
     lia_move hnf_cut();
     lia_move make_hnf_cut();
     bool init_terms_for_hnf_cut();

src/util/lp/niil_solver.cpp

@@ -26,7 +26,7 @@ typedef lp::constraint_index     lpci;
 typedef std::unordered_set<lpci> expl_set;
 typedef nra::mon_eq              mon_eq;
 typedef lp::var_index            lpvar;
-
+typedef lp::ineq                 ineq;
 struct hash_svector {
     size_t operator()(const unsigned_vector & v) const {
         return svector_hash<unsigned_hash>()(v);
@@ -513,7 +513,7 @@ struct solver::imp {
         return true;
     }
     
-    std::ostream & print_ineq(ineq & in, std::ostream & out) const {
+    std::ostream & print_ineq(const ineq & in, std::ostream & out) const {
         m_lar_solver.print_term(in.m_term, out);
         out << " " << lp::lconstraint_kind_string(in.m_cmp) << " 0";
         return out;

src/util/lp/niil_solver.h

@@ -24,15 +24,9 @@ Revision History:
 #include "util/params.h"
 #include "nlsat/nlsat_solver.h"
 #include "util/lp/lar_solver.h"
+#include "util/lp/int_solver.h"
 namespace niil {
-struct ineq {
+typedef lp::lemma lemma;
-    lp::lconstraint_kind m_cmp;
-    lp::lar_term         m_term;
-    ineq(lp::lconstraint_kind cmp, const lp::lar_term& term) : m_cmp(cmp), m_term(term) {} 
-};
-
-typedef vector<ineq> lemma;
-
 // nonlinear integer incremental linear solver
 class solver {
     struct imp;