From ba6b024ac4d1d54574b5e92450dea4f29598a004 Mon Sep 17 00:00:00 2001
From: Miguel Neves <t-mineve@microsoft.com>
Date: Thu, 19 Oct 2017 19:52:56 -0700
Subject: [PATCH] Reverted to March_CU like lookahead

---
 src/sat/sat_lookahead.cpp | 45 ++++++++++++++++++++++-----------------
 src/sat/sat_lookahead.h   |  5 ++---
 2 files changed, 27 insertions(+), 23 deletions(-)

diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index bdc856fb3..7e9e2d230 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -340,6 +340,13 @@ namespace sat {
     }
 
     bool lookahead::is_unsat() const {
+        for (unsigned idx = 0; idx < m_binary.size(); ++idx) {
+            literal l = to_literal(idx);
+            for (literal lit : m_binary[idx]) {
+                if (is_true(l) && is_false(lit))
+                    return true;
+            }
+        }
         // check if there is a clause whose literals are false.
         // every clause is terminated by a null-literal.
         for (nary* n : m_nary_clauses) {
@@ -432,8 +439,21 @@ namespace sat {
 
     bool lookahead::missed_conflict() const {
         if (inconsistent()) return false;
+        for (literal l1 : m_trail) {
+            for (literal l2 : m_binary[l1.index()]) {
+                if (is_false(l2))
+                    return true;
+            }
+            unsigned sz = m_ternary_count[(~l1).index()];
+            for (binary b : m_ternary[(~l1).index()]) {
+                if (sz-- == 0) break;
+                if ((is_false(b.m_u) && is_false(b.m_v)))
+                    return true;
+            }
+        }
         for (nary * n : m_nary_clauses) {
-            if (n->size() == 0) return true;
+            if (n->size() == 0)
+                return true;
         }
         return false;
     }
@@ -1144,18 +1164,6 @@ namespace sat {
         SASSERT(m_trail_lim.empty() || m_trail.size() >= m_trail_lim.back());
     }
 
-    void lookahead::promote(unsigned base) {
-        if (m_trail.empty()) return;
-        unsigned last_lvl = get_level(m_trail.back());
-        base -= last_lvl;
-        for (unsigned i = m_trail.size(); i > 0; ) {
-            literal lit = m_trail[--i];
-            if (is_fixed_at(lit, c_fixed_truth)) break;
-            SASSERT(is_fixed_at(lit, last_lvl));
-            m_stamp[lit.var()] += base;
-        }
-    }
-
     // 
     // The current version is modeled after CDCL SAT solving data-structures.
     // It borrows from the watch list data-structure. The cost tradeoffs are somewhat
@@ -1496,7 +1504,7 @@ namespace sat {
         sz = m_nary_count[l.index()];
         for (nary* n : m_nary[l.index()]) {
             if (sz-- == 0) break;
-            if (m_stamp[l.var()] > m_stamp[n->get_head().var()]) {
+            if (get_level(l) > get_level(n->get_head())) {
                 n->set_head(l);
             }
         }
@@ -1692,7 +1700,6 @@ namespace sat {
                     num_units += do_double(lit, dl_lvl);
                     if (dl_lvl > level) {
                         base = dl_lvl;
-                        promote(base + m_lookahead[i].m_offset);
                         SASSERT(get_level(m_trail.back()) == base + m_lookahead[i].m_offset);
                     }
                     unsat = inconsistent();
@@ -1881,15 +1888,13 @@ namespace sat {
         SASSERT(dl_no_overflow(base));
         base += m_lookahead.size();
         unsigned dl_truth = base + m_lookahead.size() * m_config.m_dl_max_iterations;
-        promote(dl_truth);
         scoped_level _sl(*this, dl_truth);
         SASSERT(get_level(m_trail.back()) == dl_truth);
         SASSERT(is_fixed(l));
         IF_VERBOSE(2, verbose_stream() << "double: " << l << " depth: " << m_trail_lim.size() << "\n";);
-        //lookahead_backtrack();
-        //assign(l);
-        //propagate();
-        //SASSERT(!inconsistent());
+        lookahead_backtrack();
+        assign(l);
+        propagate();
         unsigned old_sz = m_trail.size();
         bool change = true;
         literal last_changed = null_literal;
diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h
index 8420ae1f5..e84213cfe 100644
--- a/src/sat/sat_lookahead.h
+++ b/src/sat/sat_lookahead.h
@@ -90,7 +90,7 @@ namespace sat {
                 m_min_cutoff = 30;
                 m_preselect = false;
                 m_level_cand = 600;
-                m_delta_rho = (double)0.85;
+                m_delta_rho = (double)0.7;
                 m_dl_max_iterations = 2;
                 m_tc1_limit = 10000000;
                 m_reward_type = ternary_reward;
@@ -246,7 +246,7 @@ namespace sat {
         inline bool is_true(literal l) const { return is_true_at(l, m_level); }
         inline void set_true(literal l) { m_stamp[l.var()] = m_level + l.sign(); }
         inline void set_undef(literal l) { m_stamp[l.var()] = 0; }
-        inline unsigned get_level(literal l) { return m_stamp[l.var()] & UINT_MAX - 1; }
+        inline unsigned get_level(literal l) const { return m_stamp[l.var()] & UINT_MAX - 1; }
         void set_level(literal d, literal s) { m_stamp[d.var()] = (m_stamp[s.var()] & ~0x1) + d.sign(); }
         lbool value(literal l) const { return is_undef(l) ? l_undef : is_true(l) ? l_true : l_false; }
         
@@ -480,7 +480,6 @@ namespace sat {
         unsigned push_lookahead1(literal lit, unsigned level);
         void pop_lookahead1(literal lit, unsigned num_units);
         void lookahead_backtrack();
-        void promote(unsigned base);
         double mix_diff(double l, double r) const;
         clause const& get_clause(watch_list::iterator it) const;
         bool is_nary_propagation(clause const& c, literal l) const;