From 5e2f7f7177bf7f4d5f5b66cd7bd5db0f4e07ffab Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 21 Jun 2017 20:22:31 -0700
Subject: [PATCH] fixes top lookahead simplification

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_lookahead.cpp  | 29 ++++++++++++++++++++---------
 src/sat/sat_simplifier.cpp | 10 ----------
 src/sat/sat_solver.cpp     |  2 ++
 src/util/uint_set.h        |  1 +
 4 files changed, 23 insertions(+), 19 deletions(-)

diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index 763126398..955b3766c 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -841,6 +841,7 @@ namespace sat {
         unsigned sz = m_s.m_watches.size();
         for (unsigned l_idx = 0; l_idx < sz; ++l_idx) {
             literal l = ~to_literal(l_idx);
+            if (m_s.was_eliminated(l.var())) continue;
             watch_list const & wlist = m_s.m_watches[l_idx];
             watch_list::const_iterator it  = wlist.begin();
             watch_list::const_iterator end = wlist.end();
@@ -848,9 +849,7 @@ namespace sat {
                 if (!it->is_binary_non_learned_clause())
                     continue;
                 literal l2 = it->get_literal();                    
-                SASSERT(!m_s.was_eliminated(l.var()));
-                SASSERT(!m_s.was_eliminated(l2.var()));
-                if (l.index() < l2.index()) 
+                if (l.index() < l2.index() && !m_s.was_eliminated(l2.var()))
                     add_binary(l, l2);
             }
         }
@@ -895,6 +894,12 @@ namespace sat {
                 m_config.m_use_ternary_reward = false;
             }
 #endif
+            bool was_eliminated = false;
+            for (unsigned i = 0; !was_eliminated && i < c.size(); ++i) {
+                was_eliminated = m_s.was_eliminated(c[i].var());
+            }
+            if (was_eliminated) continue;
+
             clause* c1 = m_cls_allocator.mk_clause(c.size(), c.begin(), false);
             m_clauses.push_back(c1);
             attach_clause(*c1);
@@ -1519,7 +1524,9 @@ namespace sat {
             if (m_search_mode == lookahead_mode::searching) {
                 m_stats.m_propagations++;
                 TRACE("sat", tout << "removing free var v" << l.var() << "\n";);
-                m_freevars.remove(l.var());
+                if (l.var() > m_freevars.max_var()) std::cout << "bigger than max-var: " << l << " " << " " << m_freevars.max_var() << "\n";
+                if (!m_freevars.contains(l.var())) std::cout << "does not contain: " << l << " eliminated: " << m_s.was_eliminated(l.var()) << "\n";
+                if (m_freevars.contains(l.var())) { m_freevars.remove(l.var()); }
                 validate_assign(l);
             }
         }
@@ -1722,16 +1729,20 @@ namespace sat {
         if (inconsistent()) return;
         SASSERT(m_trail_lim.empty());
         unsigned num_units = 0;
-        for (unsigned i = 0; i < m_trail.size(); ++i) {
+        
+        for (unsigned i = 0; i < m_trail.size() && !m_s.inconsistent(); ++i) {
             literal lit = m_trail[i];
             if (m_s.value(lit) == l_undef && !m_s.was_eliminated(lit.var())) {
-                m_s.m_simplifier.propagate_unit(lit);                    
+                m_s.assign(lit, justification());
                 ++num_units;
             }
-        }
+        }        
         IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :units " << num_units << ")\n";);
-            
-        m_s.m_simplifier.subsume();
+         
+        if (num_units > 0 && !m_s.inconsistent()) {
+            m_s.propagate_core(false);
+            m_s.m_simplifier(false);
+        }
         m_lookahead.reset();
     }
 
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index afeed35be..366e994ae 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -166,10 +166,7 @@ namespace sat {
         CASSERT("sat_solver", s.check_invariant());
         TRACE("before_simplifier", s.display(tout););
 
-        m_sub_todo.reset();
-        m_sub_bin_todo.reset();
         s.m_cleaner(true);
-        m_last_sub_trail_sz = s.m_trail.size();
         TRACE("after_cleanup", s.display(tout););
         CASSERT("sat_solver", s.check_invariant());
         m_need_cleanup = false;
@@ -223,13 +220,6 @@ namespace sat {
             }
         }
 
-        if (!learned && s.m_config.m_lookahead_simplify) {
-            // perform lookahead simplification
-            lookahead lh(s);
-            lh.simplify();
-            lh.collect_statistics(s.m_aux_stats);
-        }
-
         CASSERT("sat_solver", s.check_invariant());
         TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout););
 
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 0341b9269..078acfb6e 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1355,6 +1355,7 @@ namespace sat {
         m_luby_idx                = 1;
         m_gc_threshold            = m_config.m_gc_initial;
         m_restarts                = 0;
+        m_conflicts               = 0;
         m_min_d_tk                = 1.0;
         m_search_lvl              = 0;
         m_stopwatch.reset();
@@ -1399,6 +1400,7 @@ namespace sat {
 
         if (m_config.m_lookahead_simplify) {
             lookahead lh(*this);
+            lh.simplify();
             lh.scc();
             lh.collect_statistics(m_aux_stats);
         }
diff --git a/src/util/uint_set.h b/src/util/uint_set.h
index f0990492b..c345f1092 100644
--- a/src/util/uint_set.h
+++ b/src/util/uint_set.h
@@ -369,6 +369,7 @@ public:
     void reset() { m_size = 0; }
     bool empty() const { return m_size == 0; }    
     unsigned size() const { return m_size; }
+    unsigned max_var() const { return m_index.size(); }
     typedef  unsigned_vector::const_iterator iterator;
     iterator begin() const { return m_elems.begin(); }
     iterator end() const { return m_elems.begin() + m_size; }