From f253b20820473735f950ea29e2730b9c38113ec1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 15 May 2017 09:34:11 -0700
Subject: [PATCH] local changes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_elim_eqs.cpp   |  9 +++++++--
 src/sat/sat_lookahead.h    | 14 ++++++++++++--
 src/sat/sat_simplifier.cpp | 11 ++++++-----
 src/sat/sat_solver.cpp     |  1 +
 4 files changed, 26 insertions(+), 9 deletions(-)

diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp
index 0001aaf5c..b9b7dbd85 100644
--- a/src/sat/sat_elim_eqs.cpp
+++ b/src/sat/sat_elim_eqs.cpp
@@ -78,7 +78,7 @@ namespace sat {
         clause_vector::iterator end = cs.end();
         for (; it != end; ++it) {
             clause & c     = *(*it);
-            TRACE("elim_eqs", tout << "processing: " << c << "\n";);
+            TRACE("sats", tout << "processing: " << c << "\n";);
             unsigned sz    = c.size();
             unsigned i;
             for (i = 0; i < sz; i++) {
@@ -101,7 +101,12 @@ namespace sat {
                 c[i] = norm(roots, c[i]);
             }
             std::sort(c.begin(), c.end());
-            TRACE("elim_eqs", tout << "after normalization/sorting: " << c << "\n";);
+            TRACE("sats", tout << "after normalization/sorting: " << c << "\n"; tout.flush(););
+            DEBUG_CODE({
+                for (unsigned i = 0; i < sz; i++) {
+                    CTRACE("sats", c[i] != norm(roots, c[i]), tout << c[i] << " " << norm(roots, c[i]) << "\n"; tout.flush(););
+                    SASSERT(c[i] == norm(roots, c[i]));
+                } });
             // remove duplicates, and check if it is a tautology
             literal l_prev = null_literal;
             unsigned j = 0;
diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h
index 72e64ae1d..f1d0833c4 100644
--- a/src/sat/sat_lookahead.h
+++ b/src/sat/sat_lookahead.h
@@ -723,9 +723,10 @@ namespace sat {
         void set_min(literal v, literal u) { m_dfs[v.index()].m_min = u; }
         void set_rank(literal v, unsigned r) { m_dfs[v.index()].m_rank = r; }
         void set_height(literal v, unsigned h) { m_dfs[v.index()].m_height = h; }
-        void set_parent(literal v, literal p) { TRACE("sat", tout << v << " <- " << p << "\n";); m_dfs[v.index()].m_parent = p; }
+        void set_parent(literal v, literal p) { TRACE("scc", tout << v << " <- " << p << "\n";); m_dfs[v.index()].m_parent = p; }
         void set_vcomp(literal v, literal u) { m_dfs[v.index()].m_vcomp = u; }
         void get_scc(literal v) {
+            TRACE("scc", tout << v << "\n";);
             set_parent(v, null_literal);
             activate_scc(v);
             do {
@@ -1065,7 +1066,9 @@ namespace sat {
                 for (; it != end; ++it) {
                     if (!it->is_binary_non_learned_clause())
                         continue;
-                    literal l2 = it->get_literal();
+                    literal l2 = it->get_literal();                    
+                    SASSERT(!m_s.was_eliminated(l.var()));
+                    SASSERT(!m_s.was_eliminated(l2.var()));
                     if (l.index() < l2.index()) 
                         add_binary(l, l2);
                 }
@@ -1100,6 +1103,7 @@ namespace sat {
                 attach_clause(*c1);
                 for (unsigned i = 0; i < c.size(); ++i) {
                     m_full_watches[(~c[i]).index()].push_back(c1);
+                    SASSERT(!m_s.was_eliminated(c[i].var()));
                 }
                 if (m_s.m_config.m_drat) m_drat.add(c, false);
             }
@@ -1906,6 +1910,12 @@ namespace sat {
                     if (p != null_literal && p.var() != v && !m_s.is_external(v) && !m_s.was_eliminated(v) && !m_s.was_eliminated(p.var())) {
                         to_elim.push_back(v);
                         roots[v] = p;
+                        SASSERT(get_parent(p) == p);
+                        set_parent(~p, ~p);
+                        SASSERT(get_parent(~p) == ~p);
+                        if (v == 5904 || v == 5903) {
+                            std::cout << lit << " " << p << "\n";
+                        }
                     }
                 }
                 IF_VERBOSE(1, verbose_stream() << "eliminate " << to_elim.size() << " variables\n";);
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 2687c59e5..efb9f5498 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -207,11 +207,6 @@ namespace sat {
         }
         while (!m_sub_todo.empty());
 
-        if (!learned) {
-            // perform lookahead simplification
-            lookahead(s).simplify();
-        }
-
         bool vars_eliminated = m_num_elim_vars > m_old_num_elim_vars;
 
         if (m_need_cleanup) {
@@ -230,6 +225,12 @@ namespace sat {
 
         CASSERT("sat_solver", s.check_invariant());
         TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout););
+
+        if (!learned) {
+            // perform lookahead simplification
+            lookahead(s).simplify();
+        }
+
         finalize();
 
     }
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 3df718527..d42f4d41a 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -97,6 +97,7 @@ namespace sat {
                 }
             }
         }
+
         //
         // register the extension before performing assignments.
         // the assignments may call back into the extension.