From fc277f5648766981bfe66f51ab0cf13d7899e72b Mon Sep 17 00:00:00 2001
From: Lev <levnach@hotmail.com>
Date: Mon, 3 Dec 2018 19:52:06 -0800
Subject: [PATCH] order lemma

Signed-off-by: Lev <levnach@hotmail.com>
---
 src/util/lp/factorization.h | 10 ++++++++++
 src/util/lp/nla_solver.cpp  | 33 ++++++++++++++++++++++++---------
 2 files changed, 34 insertions(+), 9 deletions(-)

diff --git a/src/util/lp/factorization.h b/src/util/lp/factorization.h
index bb4858582..24f5e42ea 100644
--- a/src/util/lp/factorization.h
+++ b/src/util/lp/factorization.h
@@ -18,6 +18,7 @@
 
 
   --*/
+#pragma once
 #include "util/rational.h"
 #include "util/lp/monomial.h"
 
@@ -41,6 +42,15 @@ public:
     bool is_var() const { return m_type == factor_type::VAR; }
 };
 
+inline bool operator==(const factor& a, const factor& b) {
+    return a.index() == b.index() && a.type() == b.type(); 
+}
+
+inline bool operator!=(const factor& a, const factor& b) {
+    return ! (a == b); 
+}
+
+
 class factorization {
     vector<factor>         m_vars;
 public:
diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index 5750eb672..bd54707fc 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -1034,16 +1034,31 @@ struct solver::imp {
         return true;
     }
 
-    void generate_ol() {
-        NOT_IMPLEMENTED_YET();
+    void generate_ol(const rooted_mon& ac,
+                     const factor& a,
+                     const factor& c,
+                     const rooted_mon& bd,
+                     const factor& b,
+                     const factor& d) {
+        if (c != d) {
+            lpvar i = var(c);
+            lpvar j = var(d);
+            auto iv = vvr(i), jv = vvr(j);
+            SASSERT(abs(iv) == abs(jv));
+            if (iv == jv) {
+                mk_ineq(i, -rational(1), j, lp::lconstraint_kind::NE);
+            } else { // iv == -jv
+                mk_ineq(i, j, lp::lconstraint_kind::NE);                
+            }
+        }
     }
 
     bool order_lemma_on_ac_and_bd_and_factors(const rooted_mon& ac,
-                                                   const factor& a,
-                                                   const factor& c,
-                                                   const rooted_mon& bd,
-                                                   const factor& b,
-                                                   const factor& d) {
+                                              const factor& a,
+                                              const factor& c,
+                                              const rooted_mon& bd,
+                                              const factor& b,
+                                              const factor& d) {
         
         auto ac_m = vvr(a) * vvr(c);
         auto bd_m = vvr(b) * vvr(d);
@@ -1052,11 +1067,11 @@ struct solver::imp {
         auto bd_v = vvr(bd);
 
         if (ac_m < bd_m && !(ac_v < bd_v)) {
-            generate_ol();
+            generate_ol(ac, a, c, bd, b, d);
             return true;
         }
         else if (ac_m > bd_m && !(ac_v > bd_v)) {
-            generate_ol();
+            generate_ol(ac, a, c, bd, b, d);
             return true;
         }