From 08d891891eeffd6737cb45401f4828c4fa346b58 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 22 Aug 2018 11:03:32 +0800
Subject: [PATCH] handle unsorted monomials

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/smt/theory_lra.cpp      |  2 +-
 src/util/lp/lp_utils.h      |  8 ++++++++
 src/util/lp/mon_eq.h        |  2 ++
 src/util/lp/niil_solver.cpp | 29 ++++++++++++++++++++---------
 src/util/lp/niil_solver.h   |  3 +--
 5 files changed, 32 insertions(+), 12 deletions(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index c056358a8..d0f566447 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -430,7 +430,7 @@ class theory_lra::imp {
     }
     void ensure_niil() {
         if (!m_niil) {
-            m_niil = alloc(niil::solver, *m_solver.get(), m.limit(), ctx().get_params());
+            m_niil = alloc(niil::solver, *m_solver.get(), m.limit(), ctx().get_params(), false);
             m_switcher.m_niil = &m_niil;
             for (auto const& _s : m_scopes) {
                 (void)_s;
diff --git a/src/util/lp/lp_utils.h b/src/util/lp/lp_utils.h
index 069bf9abf..cfac7a08d 100644
--- a/src/util/lp/lp_utils.h
+++ b/src/util/lp/lp_utils.h
@@ -29,6 +29,14 @@ void print_vector(const C & t, std::ostream & out) {
     out << std::endl;
 }
 
+template <typename C>
+void print_vector(const C * t, unsigned size, std::ostream & out) {
+    for (unsigned i = 0; i < size; i++ )
+        out << t[i] << " ";
+    out << std::endl;
+}
+
+
 template <typename A, typename B>
 bool try_get_value(const std::unordered_map<A,B> & map, const A& key, B & val) {
     const auto it = map.find(key);
diff --git a/src/util/lp/mon_eq.h b/src/util/lp/mon_eq.h
index 5401e9d45..73858d394 100644
--- a/src/util/lp/mon_eq.h
+++ b/src/util/lp/mon_eq.h
@@ -9,6 +9,8 @@ namespace nra {
     struct mon_eq {
         mon_eq(lp::var_index v, unsigned sz, lp::var_index const* vs):
             m_v(v), m_vs(sz, vs) {}
+        mon_eq(lp::var_index v, const svector<lp::var_index> &vs):
+            m_v(v), m_vs(vs) {}
         lp::var_index          m_v;
         svector<lp::var_index> m_vs;
         unsigned var() const { return m_v; }
diff --git a/src/util/lp/niil_solver.cpp b/src/util/lp/niil_solver.cpp
index 7fea30e5a..7c21aee0e 100644
--- a/src/util/lp/niil_solver.cpp
+++ b/src/util/lp/niil_solver.cpp
@@ -33,9 +33,8 @@ struct solver::imp {
             lpvar                m_i;
             lpvar                m_j;
             int                  m_sign;
-            lpci m_c0;
-            lpci m_c1;
-            
+            lpci                 m_c0;
+            lpci                 m_c1;
             equiv(lpvar i, lpvar j, int sign, lpci c0, lpci c1) :
                 m_i(i),
                 m_j(j),
@@ -196,17 +195,29 @@ struct solver::imp {
     std::unordered_map<lpvar, var_lists>                   m_var_lists;
     lp::explanation *                                      m_expl;
     lemma *                                                m_lemma;
-    imp(lp::lar_solver& s, reslimit& lim, params_ref const& p)
-        : m_lar_solver(s)
+    bool                                                   m_monomials_are_presorted;
+    imp(lp::lar_solver& s, reslimit& lim, params_ref const& p, bool monomials_are_presorted)
+        : m_lar_solver(s), m_monomials_are_presorted(monomials_are_presorted)
           // m_limit(lim),
           // m_params(p)
     {
     }
 
     void add(lpvar v, unsigned sz, lpvar const* vs) {
-        m_monomials.push_back(mon_eq(v, sz, vs));
+        if (m_monomials_are_presorted) {
+            m_monomials.push_back(mon_eq(v, sz, vs));
+        }
+        else {
+            svector<lpvar> sorted_vs;
+            for (unsigned i = 0; i < sz; i++)
+                sorted_vs.push_back(vs[i]);
+            std::sort(sorted_vs.begin(), sorted_vs.end());
+            std::cout << "sorted_vs = ";
+            print_vector(sorted_vs, std::cout);
+            m_monomials.push_back(mon_eq(v, sorted_vs));
+        }
     }
-
+    
     void push() {
         m_monomials_lim.push_back(m_monomials.size());
     }
@@ -640,8 +651,8 @@ void solver::pop(unsigned n) {
 }
 
 
-solver::solver(lp::lar_solver& s, reslimit& lim, params_ref const& p) {
-    m_imp = alloc(imp, s, lim, p);
+solver::solver(lp::lar_solver& s, reslimit& lim, params_ref const& p, bool monomials_are_sorted) {
+    m_imp = alloc(imp, s, lim, p, monomials_are_sorted);
 }
 
 
diff --git a/src/util/lp/niil_solver.h b/src/util/lp/niil_solver.h
index cbc1283c3..8b4fa4729 100644
--- a/src/util/lp/niil_solver.h
+++ b/src/util/lp/niil_solver.h
@@ -40,8 +40,7 @@ public:
     struct imp;
     imp* m_imp;
     void add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs);
-    solver(lp::lar_solver& s, reslimit& lim, params_ref const& p);
-
+    solver(lp::lar_solver& s, reslimit& lim, params_ref const& p, bool monomials_are_presorted);
     imp* get_imp();
     void push();
     void pop(unsigned scopes);