From cbaa16df57ce3861d84cbb5f3d614385c5b38748 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 11 May 2022 09:03:57 -0700
Subject: [PATCH] lcm normalization

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/simplex/model_based_opt.cpp | 19 +++++++++++++++++--
 src/math/simplex/model_based_opt.h   |  1 +
 2 files changed, 18 insertions(+), 2 deletions(-)

diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp
index e63e71be6..62d1f4c55 100644
--- a/src/math/simplex/model_based_opt.cpp
+++ b/src/math/simplex/model_based_opt.cpp
@@ -485,6 +485,21 @@ namespace opt {
         }
     }
 
+    model_based_opt::row& model_based_opt::row::normalize() {
+        if (m_type == t_mod)
+            return *this;
+        rational D(abs(m_coeff));
+        for (auto const& [id, coeff] : m_vars)
+            D = lcm(D, coeff);
+        if (D == 1)
+            return *this;
+        SASSERT(D > 0);
+        for (auto & [id, coeff] : m_vars)
+            coeff *= D;
+        m_coeff *= D;
+        return *this;
+    }
+
     // 
     // Let
     //   row1: t1 + a1*x <= 0
@@ -923,9 +938,9 @@ namespace opt {
     }
 
     void model_based_opt::get_live_rows(vector<row>& rows) {
-        for (row const& r : m_rows) {
+        for (row & r : m_rows) {
             if (r.m_alive) {
-                rows.push_back(r);
+                rows.push_back(r.normalize());
             }
         }
     }
diff --git a/src/math/simplex/model_based_opt.h b/src/math/simplex/model_based_opt.h
index bb6f8f91c..cb8c18542 100644
--- a/src/math/simplex/model_based_opt.h
+++ b/src/math/simplex/model_based_opt.h
@@ -59,6 +59,7 @@ namespace opt {
             bool        m_alive;        // rows can be marked dead if they have been processed.
             void reset() { m_vars.reset(); m_coeff.reset(); m_value.reset(); }
 
+            row& normalize();
             void neg() { for (var & v : m_vars) v.m_coeff.neg(); m_coeff.neg(); m_value.neg(); }
             rational get_coefficient(unsigned x) const;
         };