From 7e8ed0762d29bbfc80716937183772e388802f1c Mon Sep 17 00:00:00 2001
From: TheRealNebus <miguel.a.t.neves@gmail.com>
Date: Thu, 26 Apr 2018 22:39:58 +0100
Subject: [PATCH] Revert "implemented CLD"

This reverts commit 3a7efb91ae073c346716b4213c06d32fc39510a6.
---
 src/opt/mss.cpp        | 12 ++++----
 src/opt/mss_solver.cpp | 62 ++++--------------------------------------
 2 files changed, 12 insertions(+), 62 deletions(-)

diff --git a/src/opt/mss.cpp b/src/opt/mss.cpp
index 47f4b6e02..cc0fa8d7d 100644
--- a/src/opt/mss.cpp
+++ b/src/opt/mss.cpp
@@ -155,10 +155,10 @@ namespace opt {
         lbool is_sat = l_true;
         for (unsigned i = 0; is_sat == l_true && i < m_cores.size(); ++i) {
             bool has_mcs = false;
-            bool not_last = i + 1 < m_cores.size();
+            bool is_last = i + 1 < m_cores.size();
             SASSERT(check_invariant());
             update_core(m_cores[i]); // remove members of mss
-            is_sat = process_core(1, m_cores[i], has_mcs, not_last);
+            is_sat = process_core(1, m_cores[i], has_mcs, is_last); 
         }    
         if (is_sat == l_true) {
             SASSERT(check_invariant());
@@ -183,7 +183,7 @@ namespace opt {
     // at least one literal in core is false in current model.
     // pick literals in core that are not yet in mss.
     //    
-    lbool mss::process_core(unsigned sz, exprs& core, bool& has_mcs, bool not_last) {
+    lbool mss::process_core(unsigned sz, exprs& core, bool& has_mcs, bool is_last) {
         SASSERT(sz > 0);
         if (core.empty()) {
             return l_true;
@@ -191,7 +191,7 @@ namespace opt {
         if (m.canceled()) {
             return l_undef;
         }
-        if (sz == 1 && core.size() == 1 && not_last && !has_mcs) {
+        if (sz == 1 && core.size() == 1 && is_last && !has_mcs) {
             // there has to be at least one false 
             // literal in the core.
             TRACE("opt", tout << "mcs: " << mk_pp(core[0], m) << "\n";);
@@ -214,7 +214,7 @@ namespace opt {
                     SASSERT(m_mss_set.contains(core[i]));
                 });
             update_core(core);
-            return process_core(2*sz, core, has_mcs, not_last);
+            return process_core(2*sz, core, has_mcs, is_last);
         case l_false:
             if (sz == 1) {
                 has_mcs = true;
@@ -232,7 +232,7 @@ namespace opt {
                 }
                 update_core(core);
             }
-            return process_core(1, core, has_mcs, not_last);
+            return process_core(1, core, has_mcs, is_last);
         case l_undef:
             return l_undef;
         }
diff --git a/src/opt/mss_solver.cpp b/src/opt/mss_solver.cpp
index d27b6300c..501b43ee4 100755
--- a/src/opt/mss_solver.cpp
+++ b/src/opt/mss_solver.cpp
@@ -98,61 +98,15 @@ private:
         vector<exprs> dummy;
         push_exprs(mss, m_asms);
         push_exprs(mss, asms);
-        is_sat = cld(mdl.get(), mss, mcs);
-        if (is_sat == l_true) {
-            IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";);
-        }
-        /*is_sat = m_mss(mdl.get(), dummy, mss, mcs);
-        SASSERT(is_sat != l_false);
-        if (is_sat == l_true) {
-            mdl.reset();
-            m_mss.get_model(mdl);
-            update_assignment(mdl.get());
-            IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";);
-        }*/
+        is_sat = m_mss(mdl.get(), dummy, mss, mcs);
+        SASSERT(is_sat == l_true);
+        mdl.reset();
+        m_mss.get_model(mdl);
+        update_assignment(mdl.get());
+        IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";);
         return is_sat;
     }
 
-    lbool cld(model_ref initial_model, exprs& mss, exprs& mcs) {
-        exprs sat, undef;
-        undef.append(mss);
-        update_sat(initial_model, sat, undef);
-        lbool is_sat = l_true;
-        while (is_sat == l_true) {
-            expr_ref asum = relax_and_assert(m.mk_or(undef.size(), undef.c_ptr()));
-            sat.push_back(asum);
-            is_sat = check_sat(sat);
-            sat.pop_back();
-            if (is_sat == l_true) {
-                model_ref mdl;
-                s().get_model(mdl);
-                update_sat(mdl, sat, undef);
-                update_assignment(mdl.get());
-            }
-        }
-        if (is_sat == l_false) {
-            mss.reset();
-            mcs.reset();
-            mss.append(sat);
-            mcs.append(undef);
-            is_sat = l_true;
-        }
-        return is_sat;
-    }
-
-    void update_sat(model_ref mdl, exprs& sat, exprs& undef) {
-        for (unsigned i = 0; i < undef.size();) {
-            if (is_true(mdl.get(), undef[i])) {
-                sat.push_back(undef[i]);
-                undef[i] = undef.back();
-                undef.pop_back();
-            }
-            else {
-                ++i;
-            }
-        }
-    }
-
     void push_exprs(exprs& dst, expr_ref_vector const& src) {
         for (unsigned i = 0; i < src.size(); ++i) {
             dst.push_back(src[i]);
@@ -168,10 +122,6 @@ private:
         return s().check_sat(asms);
     }
 
-    lbool check_sat(exprs const& asms) {
-        return s().check_sat(asms.size(), asms.c_ptr());
-    }
-
     void update_assignment(model* mdl) {
         rational upper(0);
         for (unsigned i = 0; i < m_soft.size(); ++i) {