From f7746e22848ea318a8a094e30a002e022aef1d85 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 23 Jan 2019 16:58:00 -0800
Subject: [PATCH] address perf #2098

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_big.cpp | 22 +++-------------------
 src/sat/sat_big.h   |  2 +-
 2 files changed, 4 insertions(+), 20 deletions(-)

diff --git a/src/sat/sat_big.cpp b/src/sat/sat_big.cpp
index c1eeecd27..1aa923f1f 100644
--- a/src/sat/sat_big.cpp
+++ b/src/sat/sat_big.cpp
@@ -164,22 +164,22 @@ namespace sat {
         DEBUG_CODE(for (unsigned i = 0; i < num_lits; ++i) { VERIFY(m_left[i] < m_right[i]);});
     }
 
-    // svector<std::pair<literal, literal>> big::s_del_bin;
 
     bool big::in_del(literal u, literal v) const {
         if (u.index() > v.index()) std::swap(u, v);
-        return m_del_bin.contains(std::make_pair(u, v));
+        return m_del_bin[u.index()].contains(v);
     }
 
     void big::add_del(literal u, literal v) {
         if (u.index() > v.index()) std::swap(u, v);
-        m_del_bin.push_back(std::make_pair(u, v));
+        m_del_bin[u.index()].push_back(v);
     }
 
     unsigned big::reduce_tr(solver& s) {
         unsigned idx = 0;
         unsigned elim = 0;
         m_del_bin.reset();
+        m_del_bin.reserve(s.m_watches.size());
         for (watch_list & wlist : s.m_watches) {
             if (s.inconsistent()) break;
             literal u = to_literal(idx++);
@@ -211,22 +211,6 @@ namespace sat {
             wlist.set_end(itprev);
         }        
 
-#if 0
-        s_del_bin.append(m_del_bin);
-        IF_VERBOSE(1, 
-                   display(verbose_stream() << "Learned: " << learned() << ":");
-                   verbose_stream() << "del-bin\n";
-                   for (auto p : m_del_bin) {
-                       verbose_stream() << p.first << " " << p.second << "\n";
-                       if (safe_reach(~p.first, p.second)) {
-                           display_path(verbose_stream(), ~p.first, p.second) << " " << "\n";
-                       }
-                       else {
-                           display_path(verbose_stream(), ~p.second, p.first) << " " << "\n";
-                       }                       
-                   }
-                   );
-#endif
         s.propagate(false);
         return elim;
     }
diff --git a/src/sat/sat_big.h b/src/sat/sat_big.h
index 25093fd60..e682f9dfc 100644
--- a/src/sat/sat_big.h
+++ b/src/sat/sat_big.h
@@ -36,7 +36,7 @@ namespace sat {
         bool                   m_learned;
         bool                   m_include_cardinality;
 
-        svector<std::pair<literal, literal>> m_del_bin;
+        vector<svector<literal> > m_del_bin;
         
 
         void init_dfs_num();