fix drat for units learned from binary clause resolution

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

src/sat/sat_clause.cpp

@@ -94,6 +94,11 @@ namespace sat {
             mark_strengthened(); 
         } 
     }
+    
+    void clause::restore(unsigned num_lits) {
+        SASSERT(num_lits <= m_capacity);
+        m_size = num_lits;
+    }
 
     bool clause::satisfied_by(model const & m) const {
         for (literal l : *this) {

src/sat/sat_clause.h

@@ -68,6 +68,7 @@ namespace sat {
         bool is_learned() const { return m_learned; }
         void set_learned(bool l) { SASSERT(is_learned() != l); m_learned = l; }
         void shrink(unsigned num_lits);
+        void restore(unsigned num_lits);
         bool strengthened() const { return m_strengthened; }
         void mark_strengthened() { m_strengthened = true; update_approx(); }
         void unmark_strengthened() { m_strengthened = false; }

src/sat/sat_cleaner.cpp

@@ -135,7 +135,7 @@ namespace sat {
                     break;
                 default:
                     SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
-                    if (s.m_config.m_drat && new_sz < i) {
+                    if (s.m_config.m_drat && new_sz < sz) {
                         tmp.set(c.size(), c.begin(), c.is_learned());
                     }
                     c.shrink(new_sz);
@@ -144,7 +144,7 @@ namespace sat {
                     if (!c.frozen()) {                            
                         s.attach_clause(c);
                     }
-                    if (s.m_config.m_drat && new_sz < i) {
+                    if (s.m_config.m_drat && new_sz < sz) {
                         // for optimization, could also report deletion 
                         // of previous version of clause.
                         s.m_drat.add(c, true);

src/sat/sat_drat.cpp

@@ -68,7 +68,7 @@ namespace sat {
         case status::asserted: return;
         case status::external: return; // requires extension to drat format.
         case status::learned: break;
-        case status::deleted: (*m_out) << "d "; break;
+        case status::deleted: return; (*m_out) << "d "; break;
         }
         for (unsigned i = 0; i < n; ++i) (*m_out) << c[i] << " ";
         (*m_out) << "0\n";
@@ -215,18 +215,12 @@ namespace sat {
         if (!m_inconsistent) {
             DEBUG_CODE(validate_propagation(););
         }
-        for (unsigned i = 0; i < m_units.size(); ++i) {
+        DEBUG_CODE(
-            SASSERT(m_assignment[m_units[i].var()] != l_undef);
+            for (literal u : m_units) {
-        }
+                SASSERT(m_assignment[u.var()] != l_undef);
+            });
 
-        for (unsigned i = num_units; i < m_units.size(); ++i) {
+        if (!m_inconsistent) {
-            m_assignment[m_units[i].var()] = l_undef;
-        }
-        m_units.resize(num_units);
-        bool ok = m_inconsistent;
-        m_inconsistent = false;
-
-        if (!ok) {
             literal_vector lits(n, c);
             IF_VERBOSE(0, verbose_stream() << "not drup " << lits << "\n");
             for (unsigned v = 0; v < m_assignment.size(); ++v) {
@@ -274,6 +268,13 @@ namespace sat {
             IF_VERBOSE(0, s.display(verbose_stream()));
             exit(0);
         }
+        for (unsigned i = num_units; i < m_units.size(); ++i) {
+            m_assignment[m_units[i].var()] = l_undef;
+        }
+        m_units.resize(num_units);
+        bool ok = m_inconsistent;
+        m_inconsistent = false;
+
         return ok;
     }
 
@@ -344,6 +345,7 @@ namespace sat {
     }
 
     bool drat::contains(unsigned n, literal const* lits) {
+        if (!m_check) return true;
         for (unsigned i = m_proof.size(); i-- > 0; ) {
             clause& c = *m_proof[i];
             status st = m_status[i];

src/sat/sat_simplifier.cpp

@@ -125,8 +125,9 @@ namespace sat {
     }
 
     inline void simplifier::remove_clause_core(clause & c) {
-        for (literal l : c) 
+        for (literal l : c) {
             insert_elim_todo(l.var());
+        }
         m_sub_todo.erase(c);
         c.set_removed(true);
         TRACE("resolution_bug", tout << "del_clause: " << c << "\n";);
@@ -330,35 +331,40 @@ namespace sat {
                 }
             }
 
+            unsigned sz0 = c.size();
             if (cleanup_clause(c, in_use_lists)) {
                 s.del_clause(c);
                 continue;
             }
             unsigned sz = c.size();
-            if (sz == 0) {
+            switch(sz) {
+            case 0:
                 s.set_conflict(justification());
                 for (; it != end; ++it, ++it2) {
                     *it2 = *it;                  
                 }
-                break;
+                cs.set_end(it2);
-            }
+                return;                
-            if (sz == 1) {
+            case 1:
                 s.assign(c[0], justification());
+                c.restore(sz0);
                 s.del_clause(c);
-                continue;
+                break;
-            }
+            case 2:
-            if (sz == 2) {
                 s.mk_bin_clause(c[0], c[1], c.is_learned());
-                s.del_clause(c, false);
+                c.restore(sz0);
-                continue;
+                s.del_clause(c, true);
-            }
+                break;
-            *it2 = *it;
+            default:
-            it2++;
+                *it2 = *it;
-            if (!c.frozen()) {
+                it2++;
-                s.attach_clause(c);
+                if (!c.frozen()) {
-                if (s.m_config.m_drat) {
+                    s.attach_clause(c);
-                    s.m_drat.add(c, true);
+                    if (sz != sz0 && s.m_config.m_drat) {
+                        s.m_drat.add(c, true);
+                    }
                 }
+                break;
             }
         }
         cs.set_end(it2);
@@ -679,9 +685,15 @@ namespace sat {
         m_need_cleanup = true;
         m_num_elim_lits++;
         insert_elim_todo(l.var());
-        c.elim(l);
+        if (s.m_config.m_drat && c.contains(l)) {
-        if (s.m_config.m_drat) s.m_drat.add(c, true); 
+            m_dummy.set(c.size(), c.begin(), c.is_learned());
-        // if (s.m_config.m_drat) s.m_drat.del(c0); // can delete previous version 
+            c.elim(l);
+            s.m_drat.add(c, true); 
+            s.m_drat.del(*m_dummy.get());
+        }
+        else {
+            c.elim(l);
+        }
         clause_use_list & occurs = m_use_list.get(l);
         occurs.erase_not_removed(c);
         m_sub_counter -= occurs.size()/2;
@@ -695,23 +707,23 @@ namespace sat {
         case 0:
             TRACE("elim_lit", tout << "clause is empty\n";);
             s.set_conflict(justification());
-            return;
+            break;
         case 1:
             TRACE("elim_lit", tout << "clause became unit: " << c[0] << "\n";);
             propagate_unit(c[0]);
             // propagate_unit will delete c.
             // remove_clause(c);
-            return;
+            break;
         case 2:
             TRACE("elim_lit", tout << "clause became binary: " << c[0] << " " << c[1] << "\n";);
             s.mk_bin_clause(c[0], c[1], c.is_learned());
             m_sub_bin_todo.push_back(bin_clause(c[0], c[1], c.is_learned()));
             remove_clause(c);
-            return;
+            break;
         default:
             TRACE("elim_lit", tout << "result: " << c << "\n";);
             m_sub_todo.insert(c);
-            return;
+            break;
         }
     }
 
@@ -876,27 +888,30 @@ namespace sat {
             m_sub_counter--;
             TRACE("subsumption", tout << "next: " << c << "\n";);
             if (s.m_trail.size() > m_last_sub_trail_sz) {
+                unsigned sz0 = c.size();
                 if (cleanup_clause(c, true /* clause is in the use_lists */)) {
                     remove_clause(c);
                     continue;
                 }
                 unsigned sz = c.size();
-                if (sz == 0) {
+                switch (sz) {
+                case 0:
                     s.set_conflict(justification());
                     return;
-                }
+                case 1:
-                if (sz == 1) {
                     propagate_unit(c[0]);
                     // propagate_unit will delete c.
                     // remove_clause(c);
                     continue;
-                }
+                case 2:
-                if (sz == 2) {
                     TRACE("subsumption", tout << "clause became binary: " << c << "\n";);
                     s.mk_bin_clause(c[0], c[1], c.is_learned());
                     m_sub_bin_todo.push_back(bin_clause(c[0], c[1], c.is_learned()));
+                    c.restore(sz0);
                     remove_clause(c);
                     continue;
+                default:
+                    break;
                 }
             }
             TRACE("subsumption", tout << "using: " << c << "\n";);

src/sat/sat_solver.cpp

@@ -344,11 +344,11 @@ namespace sat {
 
     void solver::mk_bin_clause(literal l1, literal l2, bool learned) {
         if (find_binary_watch(get_wlist(~l1), ~l2)) {
-            assign(l1, justification());
+            assign_core(l1, 0, justification(l2));
             return;
         }
         if (find_binary_watch(get_wlist(~l2), ~l1)) {
-            assign(l2, justification());
+            assign_core(l2, 0, justification(l1));
             return;
         }
         watched* w0 = find_binary_watch(get_wlist(~l1), l2);
@@ -759,17 +759,20 @@ namespace sat {
         m_not_l    = not_l;
     }
 
-    void solver::assign_core(literal l, unsigned lvl, justification j) {
+    void solver::assign_core(literal l, unsigned _lvl, justification j) {
         SASSERT(value(l) == l_undef);
         TRACE("sat_assign_core", tout << l << " " << j << " level: " << lvl << "\n";);
+        if (_lvl == 0 && m_config.m_drat) {
+            m_drat.add(l, !j.is_none());
+        }
+
         if (at_base_lvl()) {
-            if (m_config.m_drat) m_drat.add(l, !j.is_none());
             j = justification(); // erase justification for level 0
         }
         m_assignment[l.index()]    = l_true;
         m_assignment[(~l).index()] = l_false;
         bool_var v = l.var();
-        m_level[v]                 = lvl;
+        m_level[v]                 = scope_lvl();
         m_justification[v]         = j;
         m_phase[v]                 = static_cast<phase>(l.sign());
         m_assigned_since_gc[v]     = true;
@@ -2263,6 +2266,7 @@ namespace sat {
 
     bool solver::resolve_conflict_core() {
 
+
         m_conflicts_since_init++;
         m_conflicts_since_restart++;
         m_conflicts_since_gc++;
@@ -2378,6 +2382,7 @@ namespace sat {
         while (num_marks > 0);
 
         m_lemma[0] = ~consequent;
+        m_drat.verify(m_lemma.size(), m_lemma.c_ptr());
         learn_lemma_and_backjump();
         return true;
     }
@@ -2409,7 +2414,6 @@ namespace sat {
         unsigned glue = num_diff_levels(m_lemma.size(), m_lemma.c_ptr());
         m_fast_glue_avg.update(glue);
         m_slow_glue_avg.update(glue);
-
         pop_reinit(m_scope_lvl - new_scope_lvl);
         TRACE("sat_conflict_detail", tout << new_scope_lvl << "\n"; display(tout););
         // unsound: m_asymm_branch.minimize(m_scc, m_lemma);
@@ -2879,20 +2883,16 @@ namespace sat {
     void solver::minimize_lemma() {
         SASSERT(!m_lemma.empty());
         SASSERT(m_unmark.empty());
-        //m_unmark.reset();
         updt_lemma_lvl_set();
 
         unsigned sz   = m_lemma.size();
         unsigned i    = 1; // the first literal is the FUIP
         unsigned j    = 1;
-        //bool drop = false;
-        //unsigned bound = sz/5+10;
         for (; i < sz; i++) {
             literal l = m_lemma[i];
             if (implied_by_marked(l)) {
                 TRACE("sat", tout << "drop: " << l << "\n";);
                 m_unmark.push_back(l.var());
-                //drop = true;
             }
             else {
                 if (j != i) {
@@ -2900,12 +2900,6 @@ namespace sat {
                 }
                 j++;
             }
-#if 0
-            if (!drop && i >= bound) {
-                j = sz;
-                break;
-            }
-#endif
         }
 
         reset_unmark(0);