From ff436ecb104c3521586796ac0462468c4289683d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 19 Feb 2020 09:52:09 -0800
Subject: [PATCH] fix #3038 again

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/qe/nlqsat.cpp        |  4 +++-
 src/sat/sat_aig_cuts.cpp | 24 ++++++++++++++++--------
 src/sat/sat_aig_cuts.h   |  1 +
 3 files changed, 20 insertions(+), 9 deletions(-)

diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp
index b40c11c58..714323c67 100644
--- a/src/qe/nlqsat.cpp
+++ b/src/qe/nlqsat.cpp
@@ -433,8 +433,10 @@ namespace qe {
             s.m_solver.vars(l, vs);
             TRACE("qe", s.m_solver.display(tout << vs << " ", l) << "\n";);
             for (unsigned v : vs) {
-                level.merge(s.m_rvar2level.get(v, max_level()));                
+                level.merge(s.m_rvar2level.get(v, max_level()));
             }
+            if (level == max_level()) 
+                throw default_exception("level not in NRA");
             set_level(l.var(), level);
             return level;
         }
diff --git a/src/sat/sat_aig_cuts.cpp b/src/sat/sat_aig_cuts.cpp
index fe31aa50a..75d1f6a17 100644
--- a/src/sat/sat_aig_cuts.cpp
+++ b/src/sat/sat_aig_cuts.cpp
@@ -372,7 +372,7 @@ namespace sat {
             literal  r = m_roots[i].second;
             literal rr = to_root[r.var()];
             to_root[v] = r.sign() ? ~rr : rr;
-            if (rr != r) std::cout << v << " -> " << to_root[v] << "\n";
+            // if (rr != r) std::cout << v << " -> " << to_root[v] << "\n";
         }
         for (unsigned i = 0; i < m_aig.size(); ++i) {
             // invalidate nodes that have been rooted
@@ -439,23 +439,31 @@ namespace sat {
     bool aig_cuts::eq(node const& a, node const& b) {
         if (a.is_valid() != b.is_valid()) return false;
         if (!a.is_valid()) return true;
-        if (a.op() != b.op() || a.sign() != b.sign() || a.size() != b.size()) return false;
-        for (unsigned i = 0; i < a.size(); ++i) {
-            if (m_literals[a.offset() + i] != m_literals[b.offset() + i]) return false;
+        if (a.op() != b.op() || a.sign() != b.sign() || a.size() != b.size()) 
+            return false;
+        for (unsigned i = a.size(); i-- > 0; ) {
+            if (m_literals[a.offset() + i] != m_literals[b.offset() + i]) 
+                return false;
         }
         return true;
     }
 
+    bool aig_cuts::similar(node const& a, node const& b) {
+        bool sim = true;
+        sim = a.is_lut() && !b.is_lut() && a.size() == b.size();
+        for (unsigned i = a.size(); sim && i-- > 0; ) {
+            sim = m_literals[a.offset() + i].var() == m_literals[b.offset() + i].var();
+        }
+        return sim;
+    }
+
     bool aig_cuts::insert_aux(unsigned v, node const& n) {
         if (!m_config.m_full) return false;
         unsigned num_gt = 0, num_eq = 0;
         for (node const& n2 : m_aig[v]) {
-            if (eq(n, n2)) return false;
+            if (eq(n, n2) || similar(n, n2)) return false;
             else if (n.size() < n2.size()) num_gt++;
             else if (n.size() == n2.size()) num_eq++;
-            // avoid inserting LUTs that are likely to collide
-            if (n.is_lut() && !n2.is_lut() && n.size() == n2.size()) 
-                return false;
         }
         if (m_aig[v].size() < m_config.m_max_aux) {
             on_node_add(v, n);
diff --git a/src/sat/sat_aig_cuts.h b/src/sat/sat_aig_cuts.h
index 9496b1264..62e6c42e7 100644
--- a/src/sat/sat_aig_cuts.h
+++ b/src/sat/sat_aig_cuts.h
@@ -124,6 +124,7 @@ namespace sat {
         void init_cut_set(unsigned id);
 
         bool eq(node const& a, node const& b);
+        bool similar(node const& a, node const& b);
 
         unsigned_vector filter_valid_nodes() const;
         void augment(unsigned_vector const& ids);