prepare for local version of Gomory cuts

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Oct 30, 2023 · 938a89e · 938a89e
1 parent 160971d
commit 938a89e
Show file tree

Hide file tree

Showing 3 changed files with 39 additions and 1 deletion.
diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
@@ -194,7 +194,11 @@ namespace lp {
         if (r == lia_move::undef && m_patcher.should_apply()) r = m_patcher();
         if (r == lia_move::undef && should_find_cube()) r = int_cube(*this)();
         if (r == lia_move::undef && should_hnf_cut()) r = hnf_cut();
+#if 1
         if (r == lia_move::undef && should_gomory_cut()) r = gomory(*this)();
+#else
+        if (r == lia_move::undef && should_gomory_cut()) r = local_gomory();
+#endif
         if (r == lia_move::undef) r = int_branch(*this)();
         return r;
     }
@@ -914,5 +918,35 @@ namespace lp {
 #endif
     }
 
+    lia_move int_solver::local_gomory() {
+        for (unsigned i = 0; i < 4; ++i) {
+
+            m_ex->clear();
+            m_t.clear();
+            m_k.reset();
+            auto r = gomory(*this)();
+            IF_VERBOSE(3, verbose_stream() << i << " " << r << "\n");
+            if (r != lia_move::cut) 
+                return r;
+            u_dependency* dep = nullptr;
+            for (auto c : *m_ex) 
+                dep = lra.join_deps(lra.dep_manager().mk_leaf(c.ci()), dep);
+            lp::lpvar term_index = lra.add_term(get_term().coeffs_as_vector(), UINT_MAX);
+            term_index = lra.map_term_index_to_column_index(term_index);
+            lra.update_column_type_and_bound(term_index, is_upper() ? lp::lconstraint_kind::LE : lp::lconstraint_kind::GE, get_offset(), dep);
+            lra.find_feasible_solution();
+            if (!lra.is_feasible()) {
+                lra.get_infeasibility_explanation(*m_ex);
+                return lia_move::conflict;
+            }
+        }
+        m_ex->clear();
+        m_t.clear();
+        m_k.reset();
+
+        return lia_move::undef;
+    }
+
+
 
 }
diff --git a/src/math/lp/int_solver.h b/src/math/lp/int_solver.h
@@ -110,6 +110,7 @@ class int_solver {
     bool has_upper(unsigned j) const;
     unsigned row_of_basic_column(unsigned j) const;
     bool cut_indices_are_columns() const;
+    lia_move local_gomory();
 
 public:
     std::ostream& display_column(std::ostream & out, unsigned j) const;
@@ -128,7 +129,6 @@ class int_solver {
     bool is_term(unsigned j) const;
     unsigned column_count() const;
     bool all_columns_are_bounded() const;
-    void find_feasible_solution();
     lia_move hnf_cut();
 
     int select_int_infeasible_var();

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
@@ -2416,6 +2416,10 @@ class theory_lra::imp {
             return false;
         theory_var uv = lp().local_to_external(u); // variables that are returned should have external representations
         theory_var vv = lp().local_to_external(v); // so maybe better to have them already transformed to external form
+        if (uv == null_theory_var)
+            return false;
+        if (vv == null_theory_var)
+            return false;
         enode* n1 = get_enode(uv);
         enode* n2 = get_enode(vv);