From d3258e7084a17539baf523866cc6271333727c02 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 1 Sep 2023 11:18:03 -0700
Subject: [PATCH] propagate lineal monomial

---
 src/math/lp/monomial_bounds.cpp |  6 +++---
 src/math/lp/nla_core.cpp        | 11 +++++++++++
 src/math/lp/nla_types.h         |  1 +
 3 files changed, 15 insertions(+), 3 deletions(-)

diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp
index 28d287477..e21891ee4 100644
--- a/src/math/lp/monomial_bounds.cpp
+++ b/src/math/lp/monomial_bounds.cpp
@@ -283,7 +283,7 @@ namespace nla {
                     break;
                 }
             }
-            lemma |= ineq(m.var(), lp::lconstraint_kind::NE, 0);
+            lemma += ineq(m.var(), lp::lconstraint_kind::EQ, 0);
         }
         else {
             for (auto v : m) 
@@ -295,9 +295,9 @@ namespace nla {
                 lp::lar_term term;
                 term.add_var(m.var());
                 term.add_monomial(-k, w);
-                lemma |= ineq(term, lp::lconstraint_kind::NE, 0);
+                lemma += ineq(term, lp::lconstraint_kind::EQ, 0);
             } else {
-                lemma |= ineq(m.var(), lp::lconstraint_kind::NE, k);
+                lemma += ineq(m.var(), lp::lconstraint_kind::EQ, k);
             }
         }
         
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 0e87f8a1d..622475cf4 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1056,6 +1056,17 @@ new_lemma& new_lemma::operator|=(ineq const& ineq) {
     }
     return *this;
 }
+
+// Contrary to new_lemma::operator|=, this method does not assert that the model does not satisfy the ineq.
+// If ineq holds then it is a nop.
+new_lemma& new_lemma::operator+=(ineq const& ineq) {
+    if (c.ineq_holds(ineq)) return *this;
+    
+    if (!c.explain_ineq(*this, ineq.term(), ineq.cmp(), ineq.rs())) {
+        current().push_back(ineq);
+    }
+    return *this;
+}
     
 
 new_lemma::~new_lemma() {
diff --git a/src/math/lp/nla_types.h b/src/math/lp/nla_types.h
index 8169266cc..186c2e902 100644
--- a/src/math/lp/nla_types.h
+++ b/src/math/lp/nla_types.h
@@ -83,6 +83,7 @@ namespace nla {
         new_lemma& operator&=(const factorization& f);
         new_lemma& operator&=(lpvar j);
         new_lemma& operator|=(ineq const& i);
+        new_lemma& operator+=(ineq const& i);
         new_lemma& explain_fixed(lpvar j);
         new_lemma& explain_equiv(lpvar u, lpvar v);
         new_lemma& explain_var_separated_from_zero(lpvar j);