From 37ec66710218bbda44d0fad7ad541950947b52c4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 8 Jun 2023 14:37:42 -0700
Subject: [PATCH] new (and fixed) patcher

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/int_solver.cpp | 35 ++++++++++++++++++++---------------
 src/math/lp/int_solver.h   |  4 ++--
 src/smt/smt_context_pp.cpp |  3 ---
 3 files changed, 22 insertions(+), 20 deletions(-)

diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index ff698fa10..837ba66db 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -103,37 +103,42 @@ namespace lp {
         mpq r = fractional_part(lra.get_value(v));
         SASSERT(0 < a && a < 1);
         SASSERT(0 < r && r < 1);
-        if (!divides(denominator(a), denominator(r)))
+        if (!divides(denominator(r), denominator(a)))
             return false;
         // stronger filter for now:
-        if (denominator(a) != denominator(r))
+        // if a = r = 1/2 then both patch directions are attempted.
+
+        if (a == r || a == 1 - r) {            
+            if (try_patch_column(v, c.var(), mpq(1)))
+                return true;
+            if (try_patch_column(v, c.var(), mpq(-1)))
+                return true;
             return false;
-        if (a == r) {
-            if (try_patch_column(c.var(), mpq(a.is_pos() ? 1 : -1)))
-                return true;
-        }
-        if (a == 1 - r) {
-            if (try_patch_column(c.var(), mpq(a.is_pos() ? -1 : 1)))
-                return true;
         }
         rational x, y;
         rational g = gcd(numerator(a), denominator(a), x, y);
+        rational scale = denominator(a)/denominator(r);
+        VERIFY(scale.is_int() && scale > 0);
         // g = numerator(a)*x + denominator(a)*y
-        x = abs(x);
+        VERIFY(g == numerator(a)*x + denominator(a)*y);
         if (divides(g, numerator(r))) {
-            auto xs = a.is_pos() ? x : -x;
-            if (try_patch_column(c.var(), xs*(numerator(r)/g)))
+            if (try_patch_column(v, c.var(), scale*x*(numerator(r)/g)))
                 return true;
+            if (try_patch_column(v, c.var(), -scale*x*(numerator(r)/g)))
+                return true;
+            return false;
         }
         if (divides(g, numerator(1 - r))) {
-            auto xs = a.is_pos() ? -x : x;
-            if (try_patch_column(c.var(), xs*(numerator(r)/g)))
+            if (try_patch_column(v, c.var(), scale*x*(numerator(1 - r)/g)))
                 return true;
+            if (try_patch_column(v, c.var(), -scale*x*(numerator(1 - r)/g)))
+                return true;
+            return false;
         }
         return false;
     }
 
-    bool int_solver::patcher::try_patch_column(unsigned j, mpq const& delta) {
+    bool int_solver::patcher::try_patch_column(unsigned v, unsigned j, mpq const& delta) {
         const auto & A = lra.A_r();
         unsigned make_count = 0, break_count = 0;
         if (delta < 0) {
diff --git a/src/math/lp/int_solver.h b/src/math/lp/int_solver.h
index e128871f5..b194b076c 100644
--- a/src/math/lp/int_solver.h
+++ b/src/math/lp/int_solver.h
@@ -51,11 +51,11 @@ class int_solver {
     public:
         patcher(int_solver& lia);
         bool should_apply() const { return true; }
-        lia_move operator()() { return patch_nbasic_columns(); }
+        lia_move operator()() { return patch_basic_columns(); }
         void patch_nbasic_column(unsigned j);
         bool patch_basic_column(unsigned v, row_cell<mpq> const& c);
         void patch_basic_column(unsigned j);
-        bool try_patch_column(unsigned j, mpq const& delta);
+        bool try_patch_column(unsigned v, unsigned j, mpq const& delta);
         unsigned count_non_int();
     private:
         void remove_fixed_vars_from_base();
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index 490a5a90e..c1d903631 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -510,9 +510,6 @@ namespace smt {
 #else
         strm << "lemma_" << (++m_lemma_id) << ".smt2";
 #endif
-        if (m_lemma_id == 1303) {
-            verbose_stream() << "lemma\n";
-        }
         return strm.str();
     }