From 9dbb56fdfcc5a997e2a6dc8b703be5e7a43e163e Mon Sep 17 00:00:00 2001
From: Lev <levnach@hotmail.com>
Date: Mon, 12 Nov 2018 10:45:24 -0800
Subject: [PATCH] toward order_lemma

Signed-off-by: Lev <levnach@hotmail.com>
---
 src/util/lp/nla_solver.cpp     | 41 +++++++++++++++++++++++-----------
 src/util/lp/vars_equivalence.h | 30 +++++++++++++++++++++++++
 2 files changed, 58 insertions(+), 13 deletions(-)

diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index 6165f0bfa..9ceff28fa 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -30,15 +30,7 @@ struct solver::imp {
 
     typedef lp::lar_base_constraint lpcon;
     
-    struct index_with_sign {
-        unsigned m_i; // the monomial index
-        rational m_sign; // the monomial sign: -1 or 1
-        index_with_sign(unsigned i, rational sign) : m_i(i), m_sign(sign) {}
-        index_with_sign() {}
-        bool operator==(const index_with_sign& b) {
-            return m_i == b.m_i && m_sign == b.m_sign;
-        }
-    };
+   
 
     //fields    
     vars_equivalence                                       m_vars_equivalence;
@@ -839,8 +831,30 @@ struct solver::imp {
         m_expl->clear();
         m_lemma->clear();
     }
+    bool order_lemma_on_factor_equiv_and_other_mon(unsigned o_i_mon, unsigned e_j, unsigned i_mon, const factorization& f, unsigned k, const rational& sign) {
+        NOT_IMPLEMENTED_YET();
+        return false;
+    }
+    // here e_j is equivalent to f[k],
+    // f is a factorization of m_monomials[i_mon]
+    bool order_lemma_on_factor_and_equiv(unsigned e_j, unsigned i_mon, const factorization& f, unsigned k, const rational& sign) {
+        lpvar j = f[k];
+        for (unsigned i : m_monomials_containing_var[j]) {
+            if (order_lemma_on_factor_equiv_and_other_mon(i, e_j, i_mon, f, k, sign)) {
+                return true;
+            }
+        }
+        return false;
+    }
 
-    bool order_lemma_on_factor(const factorization& f, unsigned k, int sign) {
+    
+    bool order_lemma_on_factor(unsigned i_mon, const factorization& f, unsigned k, int sign) {
+        lpvar j = f[k];
+        for (const index_with_sign& p : m_vars_equivalence.get_equivalent_vars(j)) {
+            if (order_lemma_on_factor_and_equiv(p.m_i, i_mon, f, k, sign * p.m_sign)) {
+                return true;
+            }
+        }
         return false;
     }
 
@@ -852,12 +866,13 @@ struct solver::imp {
 
             int sign = ((v.is_pos() && f.sign().is_pos()) || (v.is_neg() && f.sign().is_neg()))? 1 : -1;
             
-            if (order_lemma_on_factor(f, k, sign)) { 
+            if (order_lemma_on_factor(i_mon, f, k, sign)) { 
                 return true;
             }
         }
         return false;
     }
+
     bool order_lemma_on_monomial(unsigned i_mon) {
         for (auto factorization : factorization_factory_imp(i_mon, *this)) {
             if (factorization.is_empty())
@@ -910,8 +925,8 @@ struct solver::imp {
         m_expl =   &exp;
         m_lemma =  &l;
        
-        if (m_lar_solver.get_status() != lp::lp_status::OPTIMAL) {
-            TRACE("nla_solver", tout << "unknown\n";);
+        if (!(m_lar_solver.get_status() == lp::lp_status::OPTIMAL || m_lar_solver.get_status() == lp::lp_status::FEASIBLE )) {
+            TRACE("nla_solver", tout << "unknown because of the m_lar_solver.m_status = " << lp_status_to_string(m_lar_solver.get_status()) << "\n";);
             return l_undef;
         }
 
diff --git a/src/util/lp/vars_equivalence.h b/src/util/lp/vars_equivalence.h
index ec0819e21..cf8408f68 100644
--- a/src/util/lp/vars_equivalence.h
+++ b/src/util/lp/vars_equivalence.h
@@ -28,6 +28,15 @@ struct hash_svector {
     }
 };
 
+struct index_with_sign {
+    unsigned m_i; // the index
+    rational m_sign; // the sign: -1 or 1
+    index_with_sign(unsigned i, rational sign) : m_i(i), m_sign(sign) {}
+    index_with_sign() {}
+    bool operator==(const index_with_sign& b) {
+        return m_i == b.m_i && m_sign == b.m_sign;
+    }
+};
 
 struct rat_hash {
     typedef rational data;
@@ -60,6 +69,8 @@ struct vars_equivalence {
         }
     };
 
+   
+    
     // The map from the variables to m_equivs indices
     // m_tree is a spanning tree of the graph of equivs represented by m_equivs
     std::unordered_map<unsigned, unsigned> m_tree;  
@@ -70,6 +81,25 @@ struct vars_equivalence {
         m_equivs.clear();
         m_tree.clear();
     }
+    // it also returns (j, 1)
+    vector<index_with_sign> get_equivalent_vars(lpvar j) const {
+        // it is just a place holder, see if we need something more substantial
+        vector<index_with_sign> ret;
+        ret.push_back(index_with_sign(j, rational(1)));
+        return ret; 
+        /*
+        vector<index_with_sign> ret;
+        std::unordered_set<unsigned> returned;
+        std::unordered_set<unsigned> processed;
+        ret.push_back(std::make_pair(j, 1));
+        returned.insert(j);
+        processed.insert(j);
+        std::queue<unsigned> q;
+        q.enqueue(j);
+        
+        */
+        
+    } 
 
     unsigned size() const { return static_cast<unsigned>(m_tree.size()); }