fix flipper

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/opt/maxres.cpp

@@ -179,7 +179,7 @@ public:
     lbool mus_mss_solver() {
         init();
         init_local();
-        //enable_sls(m_asms);
+        enable_sls(m_asms);
         ptr_vector<expr> mcs;
         vector<ptr_vector<expr> > cores;
         while (m_lower < m_upper) {            

src/sat/sat_mus.cpp

@@ -24,7 +24,7 @@ Notes:
 
 namespace sat {
 
-    mus::mus(solver& s):s(s) {}
+    mus::mus(solver& s):s(s), m_is_active(false) {}
 
     mus::~mus() {}
    
@@ -42,6 +42,7 @@ namespace sat {
     lbool mus::operator()() {
         flet<bool> _disable_min(s.m_config.m_minimize_core, false);
         flet<bool> _disable_opt(s.m_config.m_optimize_model, false);
+        flet<bool> _is_active(m_is_active, true);
         TRACE("sat", tout << "old core: " << s.get_core() << "\n";);
         IF_VERBOSE(2, verbose_stream() << "(sat.mus " << s.get_core() << ")\n";);
         reset();

src/sat/sat_mus.h

@@ -23,12 +23,14 @@ namespace sat {
     class mus {
         literal_vector m_core;
         literal_vector m_mus;
+        bool           m_is_active;
 
         solver& s;
     public:
         mus(solver& s);
         ~mus();        
         lbool operator()();
+        bool is_active() const { return m_is_active; }
     private:
         lbool mus2();
         void mr();

src/sat/sat_probing.cpp

@@ -196,6 +196,7 @@ namespace sat {
         s.propagate(false); // make sure propagation queue is empty
         if (s.inconsistent())
             return true;
+        SASSERT(s.m_qhead == s.m_trail.size());
         CASSERT("probing", s.check_invariant());
         if (!force && m_counter > 0)
             return true;

src/sat/sat_sls.cpp

@@ -363,6 +363,7 @@ namespace sat {
         m_clause_weights.resize(m_clauses.size(), 1);
         m_sscore.resize(s.num_vars(), 0.0);
         m_hscore.resize(s.num_vars(), 0);
+        m_marked.resize(s.num_vars(), false);
         unsigned num_violated = 0;
         for (unsigned i = 0; i < m_soft.size(); ++i) {
             literal lit = m_soft[i];
@@ -453,7 +454,7 @@ namespace sat {
                 else {
                     lit = m_min_vars[m_rand(m_min_vars.size())];
                 }
-                TRACE("sat", tout << "flip soft(" << m_min_vars.size() << ") " << lit << "\n";);
+                TRACE("sat", tout << "flip soft(" << m_min_vars.size() << ", " << m_sscore[lit.var()] << ") " << lit << "\n";);
 
             }
             SASSERT(value_at(lit, m_model) == l_false);
@@ -464,9 +465,10 @@ namespace sat {
     void wsls::wflip(literal lit) {
         flip(lit);
         unsigned v = lit.var();
-        m_hscore[v] = compute_hscore(v);
         m_sscore[v] = -m_sscore[v];
+        m_hscore[v] = compute_hscore(v);
         refresh_scores(v);
+        recompute_hscores(v);
     }
 
     void wsls::update_hard_weights() {
@@ -517,7 +519,7 @@ namespace sat {
         return result;
     }
 
-    int wsls::compute_hscore(unsigned v) {
+    int wsls::compute_hscore(bool_var v) {
         literal lit(v, false);
         if (value_at(lit, m_model) == l_false) {
             lit.neg();
@@ -548,15 +550,65 @@ namespace sat {
         return hs;
     }
 
-    void wsls::refresh_scores(unsigned v) {
+    void wsls::recompute_hscores(bool_var v) {
-        if (m_hscore[v] > 0) {
+        literal lit(v, false);
+        if (value_at(lit, m_model) == l_false) {
+            lit.neg();
+        }
+        m_marked[v] = true;
+        unsigned_vector const& use1 = get_use(~lit);
+        unsigned sz = use1.size();
+        unsigned csz;
+        for (unsigned i = 0; i < sz; ++i) {
+            unsigned cl = use1[i]; 
+            if (m_num_true[cl] > 2) continue;
+            clause const& c = *m_clauses[cl];
+            csz = c.size();
+            for (unsigned j = 0; j < csz; ++j) {
+                add_refresh(c[j].var());
+            }
+        }
+        unsigned_vector const& use2 = get_use(lit);
+        sz = use2.size();
+        for (unsigned i = 0; i < sz; ++i) {
+            unsigned cl = use2[i]; 
+            if (m_num_true[cl] > 2) continue;
+            clause const& c = *m_clauses[cl];
+            csz = c.size();
+            for (unsigned j = 0; j < csz; ++j) {
+                add_refresh(c[j].var());
+            }
+        }
+        m_marked[v] = false;
+        for (unsigned i = 0; i < m_to_refresh.size(); ++i) {
+            v = m_to_refresh[i];
+            int hs = compute_hscore(v);
+            if (hs != m_hscore[v]) {
+                TRACE("sat_verbose", tout << "refresh: " << v << " from " << m_hscore[v] << " to " << hs << "\n";);
+                m_hscore[v] = hs;
+                refresh_scores(v);
+            }
+            m_marked[v] = false;
+        }
+        m_to_refresh.reset();
+    }
+
+    void wsls::add_refresh(bool_var v) {
+        if (!m_marked[v]) {
+            m_to_refresh.push_back(v);
+            m_marked[v] = true;
+        }
+    }
+
+    void wsls::refresh_scores(bool_var v) {
+        if (m_hscore[v] > 0 && !m_tabu[v] && m_sscore[v] == 0) {
             m_H.insert(v);
         }
         else {
             m_H.remove(v);
         }
         if (m_sscore[v] > 0) {
-            if (m_hscore[v] == 0) {
+            if (m_hscore[v] == 0 && !m_tabu[v]) {
                 m_S.insert(v);
             }
             else {
@@ -575,6 +627,7 @@ namespace sat {
         //           - Sum weight(c) for num_true(c) = 1 and (v in c, M(v) or !v in c and !M(v)) 
         for (unsigned v = 0; v < s.num_vars(); ++v) {
             int hs = compute_hscore(v);
+            CTRACE("sat", hs != m_hscore[v], display(tout << v << " - computed: " << hs << " - assigned: " << m_hscore[v] << "\n"););
             SASSERT(m_hscore[v] == hs);
         }
 
@@ -585,14 +638,14 @@ namespace sat {
             SASSERT(m_sscore[v] == ss);
         }
 
-        // m_H are values such that m_hscore >= 0.
+        // m_H are values such that m_hscore > 0 and sscore = 0.
         for (bool_var v = 0; v < m_hscore.size(); ++v) {
-            SASSERT(m_hscore[v] > 0 == m_H.contains(v));
+            SASSERT((m_hscore[v] > 0 && !m_tabu[v] && m_sscore[v] == 0) == m_H.contains(v));
         }
         
         // m_S are values such that hscore = 0, sscore > 0
         for (bool_var v = 0; v < m_sscore.size(); ++v) {
-            SASSERT((m_hscore[v] == 0 && m_sscore[v] > 0) == m_S.contains(v));
+            SASSERT((m_hscore[v] == 0 && m_sscore[v] > 0 && !m_tabu[v]) == m_S.contains(v));
         }
     }
 

src/sat/sat_sls.h

@@ -91,6 +91,8 @@ namespace sat {
         model           m_best_model;
         index_set       m_H, m_S;
         unsigned        m_smoothing_probability;
+        svector<bool>   m_marked;
+        unsigned_vector m_to_refresh;
     public:
         wsls(solver& s);
         virtual ~wsls();        
@@ -106,8 +108,10 @@ namespace sat {
         bool pick_wflip(literal & lit);
         double evaluate_model();
         virtual void check_invariant();
-        void refresh_scores(unsigned v);
+        void refresh_scores(bool_var v);
-        int compute_hscore(unsigned v);
+        int compute_hscore(bool_var v);
+        void recompute_hscores(bool_var v);
+        void add_refresh(bool_var v);
     };
 
 };

src/sat/sat_solver.cpp

@@ -692,6 +692,7 @@ namespace sat {
             }
             wlist.set_end(it2);
         }
+        SASSERT(m_qhead == m_trail.size());
         SASSERT(!m_inconsistent);
         return true;
     }
@@ -952,10 +953,15 @@ namespace sat {
 
     /**
        \brief Apply all simplifications.
+
     */
     void solver::simplify_problem() {
-        pop(scope_lvl());
+
-        m_trail.reset();
+        // Disable simplification during MUS computation.        
+        // if (m_mus.is_active()) return;
+        TRACE("sat", tout << "simplify\n";);
+
+        pop(scope_lvl());        
 
         SASSERT(scope_lvl() == 0);
 
@@ -990,6 +996,9 @@ namespace sat {
             m_ext->clauses_modifed();
             m_ext->simplify();
         }
+
+        TRACE("sat", display(tout << "consistent: " << (!inconsistent()) << "\n"););
+
         reinit_assumptions();
     }
 
@@ -2144,7 +2153,7 @@ namespace sat {
     // -----------------------
     void solver::push() {
         SASSERT(!inconsistent());
-        TRACE("sat", tout << "q:" << m_qhead << " trail: " << m_trail.size() << "\n";);
+        TRACE("sat_verbose", tout << "q:" << m_qhead << " trail: " << m_trail.size() << "\n";);
         SASSERT(m_qhead == m_trail.size());
         m_scopes.push_back(scope());
         scope & s = m_scopes.back();