debugging cuts

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Sep 22, 2020 · 1e6d2fb · 1e6d2fb
1 parent b7ec448
commit 1e6d2fb
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 27 deletions.
diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
@@ -388,45 +388,20 @@ int gomory::find_basic_var() {
     int result = -1;
     unsigned n = 0;
     unsigned min_row_size = UINT_MAX;
-#if 0
-    bool boxed = false;
-    mpq min_range;
-#endif
-
 
     // Prefer smaller row size
     // Prefer boxed to non-boxed
     // Prefer smaller ranges
 
+
     for (unsigned j : lra.r_basis()) {
         if (!lia.column_is_int_inf(j))
             continue;
         const row_strip<mpq>& row = lra.get_row(lia.row_of_basic_column(j));
         if (!is_gomory_cut_target(row)) 
             continue;
 
-#if 0
-        if (is_boxed(j) && (min_row_size == UINT_MAX || 4*row.size() < 5*min_row_size)) {
-            lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
-            auto new_range = lclia.m_r_upper_bounds()[j].x - lclia.m_r_lower_bounds()[j].x;
-            if (!boxed) {
-                result = j;
-                n = 1;
-                min_row_size = row.size();
-                boxed = true;
-                min_range = new_range;
-                continue;
-            }
-            if (min_range > 2*new_range || ((5*min_range > 4*new_range && (random() % (++n)) == 0))) { 
-                result = j;
-                n = 1;
-                min_row_size = row.size();
-                min_range = std::min(min_range, new_range);
-                continue;
-            }
-        }
-#endif
-
+        IF_VERBOSE(20, lia.display_row_info(verbose_stream(), lia.row_of_basic_column(j)));
         if (min_row_size == UINT_MAX || 
             2*row.size() < min_row_size || 
             (4*row.size() < 5*min_row_size && lia.random() % (++n) == 0)) {

diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
@@ -486,6 +486,19 @@ std::ostream& int_solver::display_row_info(std::ostream & out, unsigned row_inde
     auto & rslv = lrac.m_r_solver;
     bool first = true;
     for (const auto &c: rslv.m_A.m_rows[row_index]) {
+        if (is_fixed(c.var())) {
+            if (!get_value(c.var()).is_zero()) {
+                impq val = get_value(c.var())*c.coeff();
+                if (!first && val.is_pos())
+                    out << "+";
+                if (val.y.is_zero())
+                    out << val.x << " ";
+                else 
+                    out << val << " ";
+            }
+            first = false;
+            continue;
+        }
         if (c.coeff().is_one()) {
             if (!first)
                 out << "+";
@@ -508,6 +521,8 @@ std::ostream& int_solver::display_row_info(std::ostream & out, unsigned row_inde
     }
     out << "\n";
     for (const auto& c: rslv.m_A.m_rows[row_index]) {
+        if (is_fixed(c.var()))
+            continue;
         rslv.print_column_info(c.var(), out);
         if (is_base(c.var())) out << "j" << c.var() << " base\n";
     }