bug fixes, prepare for retaining blocked clauses

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

src/sat/ba_solver.cpp

@@ -2761,8 +2761,8 @@ namespace sat {
         }
     }
 
-    unsigned ba_solver::get_num_non_learned_bin(literal l) {
+    unsigned ba_solver::get_num_unblocked_bin(literal l) {
-        return s().m_simplifier.get_num_non_learned_bin(l);
+        return s().m_simplifier.get_num_unblocked_bin(l);
     }
 
     /*
@@ -2831,8 +2831,8 @@ namespace sat {
                     value(lit) == l_undef && 
                     use_count(lit) == 1 &&
                     use_count(~lit) == 1 &&
-                    get_num_non_learned_bin(lit) == 0 && 
+                    get_num_unblocked_bin(lit) == 0 && 
-                    get_num_non_learned_bin(~lit) == 0) {
+                    get_num_unblocked_bin(~lit) == 0) {
                     remove_constraint(c, "unused def");
                 }
                 break;
@@ -2876,7 +2876,7 @@ namespace sat {
 
     bool ba_solver::elim_pure(literal lit) {
         if (value(lit) == l_undef && !m_cnstr_use_list[lit.index()].empty() && 
-            use_count(~lit) == 0 && get_num_non_learned_bin(~lit) == 0) {
+            use_count(~lit) == 0 && get_num_unblocked_bin(~lit) == 0) {
             IF_VERBOSE(10, verbose_stream() << "pure literal: " << lit << "\n";);
             s().assign(lit, justification());
             return true;
@@ -3163,9 +3163,12 @@ namespace sat {
             if (w.is_binary_clause() && is_marked(w.get_literal())) {
                 ++m_stats.m_num_bin_subsumes;
                 // IF_VERBOSE(10, verbose_stream() << c1 << " subsumes (" << lit << " " << w.get_literal() << ")\n";);
-                if (!w.is_binary_non_learned_clause()) {
+                if (w.is_learned()) {
                     c1.set_learned(false);
                 }
+                else if (w.is_blocked()) {
+                    w.set_unblocked();
+                }
             }
             else {
                 if (it != it2) {

src/sat/ba_solver.h

@@ -262,7 +262,7 @@ namespace sat {
         void mark_visited(literal l) { m_visited[l.index()] = true; }
         void unmark_visited(literal l) { m_visited[l.index()] = false; }
         bool is_marked(literal l) const { return m_visited[l.index()] != 0; }
-        unsigned get_num_non_learned_bin(literal l);
+        unsigned get_num_unblocked_bin(literal l);
         literal get_min_occurrence_literal(card const& c);
         void init_use_lists();
         void remove_unused_defs();

src/sat/sat_clause.cpp

@@ -29,6 +29,7 @@ namespace sat {
         m_capacity(sz),
         m_removed(false),
         m_learned(learned),
+        m_blocked(false),
         m_used(false),
         m_frozen(false),
         m_reinit_stack(false),

src/sat/sat_clause.h

@@ -46,6 +46,7 @@ namespace sat {
         unsigned           m_used:1;
         unsigned           m_frozen:1;
         unsigned           m_reinit_stack:1;
+        unsigned           m_blocked;
         unsigned           m_inact_rounds:8;
         unsigned           m_glue:8;
         unsigned           m_psm:8;  // transient field used during gc
@@ -86,6 +87,9 @@ namespace sat {
         unsigned inact_rounds() const { return m_inact_rounds; }
         bool frozen() const { return m_frozen; }
         void freeze() { SASSERT(is_learned()); SASSERT(!frozen()); m_frozen = true; }
+        bool is_blocked() const { return m_blocked; }
+        void block() { SASSERT(!m_blocked); SASSERT(!is_learned()); m_blocked = true; }
+        void unblock() { SASSERT(m_blocked); SASSERT(!is_learned()); m_blocked = false; }
         void unfreeze() { SASSERT(is_learned()); SASSERT(frozen()); m_frozen = false; }
         static var_approx_set approx(unsigned num, literal const * lits);
         void set_glue(unsigned glue) { m_glue = glue > 255 ? 255 : glue; }

src/sat/sat_clause_use_list.cpp

@@ -22,17 +22,20 @@ Revision History:
 namespace sat {
 
     bool clause_use_list::check_invariant() const {
-#ifdef LAZY_USE_LIST
         unsigned sz = 0;
-        for (unsigned i = 0; i < m_clauses.size(); i++) 
+        for (clause* c : m_clauses) 
-            if (!m_clauses[i]->was_removed())
+            if (!c->was_removed())
                 sz++;
         SASSERT(sz == m_size);
-#endif
+        unsigned blocked = 0;
+        for (clause* c : m_clauses) 
+            if (c->is_blocked())
+                blocked++;
+        SASSERT(blocked == m_num_blocked);
+
         return true;
     }
 
-#ifdef LAZY_USE_LIST
     void clause_use_list::iterator::consume() {
         while (true) {
             if (m_i == m_size)
@@ -44,14 +47,11 @@ namespace sat {
             m_i++;
         }
     }
-#endif
 
     clause_use_list::iterator::~iterator() {
-#ifdef LAZY_USE_LIST
         while (m_i < m_size)
             next();
         m_clauses.shrink(m_j);
-#endif
     }
 
 };

src/sat/sat_clause_use_list.h

@@ -24,30 +24,30 @@ Revision History:
 
 namespace sat {
 
-#define LAZY_USE_LIST
-
     /**
        \brief Clause use list with delayed deletion.
     */
     class clause_use_list {
         clause_vector   m_clauses;
-#ifdef LAZY_USE_LIST
         unsigned        m_size;
-#endif
+        unsigned        m_num_blocked;
     public:
         clause_use_list() {
             STRACE("clause_use_list_bug", tout << "[cul_created] " << this << "\n";);
-#ifdef LAZY_USE_LIST
             m_size = 0; 
-#endif
+            m_num_blocked = 0;
         }
         
         unsigned size() const { 
-#ifdef LAZY_USE_LIST
             return m_size; 
-#else
+        }
-            return m_clauses.size();
+
-#endif
+        unsigned num_blocked() const {
+            return m_num_blocked;
+        }
+
+        unsigned non_blocked_size() const {
+            return m_size - m_num_blocked;
         }
 
         bool empty() const { return size() == 0; }
@@ -57,58 +57,59 @@ namespace sat {
             SASSERT(!m_clauses.contains(&c)); 
             SASSERT(!c.was_removed()); 
             m_clauses.push_back(&c); 
-#ifdef LAZY_USE_LIST
             m_size++; 
-#endif
+            if (c.is_blocked()) ++m_num_blocked;
         }
 
         void erase_not_removed(clause & c) { 
             STRACE("clause_use_list_bug", tout << "[cul_erase_not_removed] " << this << " " << &c << "\n";);
-#ifdef LAZY_USE_LIST
             SASSERT(m_clauses.contains(&c)); 
             SASSERT(!c.was_removed()); 
             m_clauses.erase(&c); 
             m_size--; 
-#else
+            if (c.is_blocked()) --m_num_blocked;
-            m_clauses.erase(&c);
-#endif
         }
 
         void erase(clause & c) { 
             STRACE("clause_use_list_bug", tout << "[cul_erase] " << this << " " << &c << "\n";);
-#ifdef LAZY_USE_LIST
             SASSERT(m_clauses.contains(&c)); 
             SASSERT(c.was_removed()); 
             m_size--; 
-#else
+            if (c.is_blocked()) --m_num_blocked;
-            m_clauses.erase(&c);
+        }
-#endif
+
+        void block(clause const& c) {
+            SASSERT(c.is_blocked());
+            ++m_num_blocked;
+            SASSERT(check_invariant());
+        }
+
+        void unblock(clause const& c) {
+            SASSERT(!c.is_blocked());
+            --m_num_blocked;
+            SASSERT(check_invariant());
         }
         
         void reset() { 
             m_clauses.finalize(); 
-#ifdef LAZY_USE_LIST
             m_size = 0; 
-#endif
+            m_num_blocked = 0;
         }
         
         bool check_invariant() const;
 
         // iterate & compress
-        class iterator {
+        class iterator {            
             clause_vector & m_clauses;
             unsigned        m_size;
             unsigned        m_i;
-#ifdef LAZY_USE_LIST
             unsigned        m_j;
             void consume();
-#endif
+
         public:
             iterator(clause_vector & v):m_clauses(v), m_size(v.size()), m_i(0) {
-#ifdef LAZY_USE_LIST
                 m_j = 0;
                 consume(); 
-#endif
             }
             ~iterator();
             bool at_end() const { return m_i == m_size; }
@@ -117,10 +118,8 @@ namespace sat {
                 SASSERT(!at_end()); 
                 SASSERT(!m_clauses[m_i]->was_removed()); 
                 m_i++; 
-#ifdef LAZY_USE_LIST
                 m_j++; 
                 consume(); 
-#endif
             }
         };
         

src/sat/sat_elim_vars.cpp

@@ -37,13 +37,13 @@ namespace sat{
 
         literal pos_l(v, false);
         literal neg_l(v, true);
-        unsigned num_bin_pos = simp.get_num_non_learned_bin(pos_l);
+        unsigned num_bin_pos = simp.get_num_unblocked_bin(pos_l);
         if (num_bin_pos > m_max_literals) return false;
-        unsigned num_bin_neg = simp.get_num_non_learned_bin(neg_l);
+        unsigned num_bin_neg = simp.get_num_unblocked_bin(neg_l);
         if (num_bin_neg > m_max_literals) return false;
         clause_use_list & pos_occs = simp.m_use_list.get(pos_l);
         clause_use_list & neg_occs = simp.m_use_list.get(neg_l);
-        unsigned clause_size = num_bin_pos + num_bin_neg + pos_occs.size() + neg_occs.size();
+        unsigned clause_size = num_bin_pos + num_bin_neg + pos_occs.non_blocked_size() + neg_occs.non_blocked_size();
         if (clause_size == 0) {
             return false;
         }
@@ -85,8 +85,8 @@ namespace sat{
         // eliminate variable
         simp.m_pos_cls.reset();
         simp.m_neg_cls.reset();
-        simp.collect_clauses(pos_l, simp.m_pos_cls);
+        simp.collect_clauses(pos_l, simp.m_pos_cls, false);
-        simp.collect_clauses(neg_l, simp.m_neg_cls);
+        simp.collect_clauses(neg_l, simp.m_neg_cls, false);
         model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
         simp.save_clauses(mc_entry, simp.m_pos_cls);
         simp.save_clauses(mc_entry, simp.m_neg_cls);
@@ -122,13 +122,13 @@ namespace sat{
         TRACE("elim_vars",
               tout << "eliminate " << v << "\n";
               for (watched const& w : simp.get_wlist(~pos_l)) {
-                  if (w.is_binary_non_learned_clause()) {
+                  if (w.is_binary_unblocked_clause()) {
                       tout << pos_l << " " << w.get_literal() << "\n";
                   }
               }
               m.display(tout, b1);
               for (watched const& w : simp.get_wlist(~neg_l)) {
-                  if (w.is_binary_non_learned_clause()) {
+                  if (w.is_binary_unblocked_clause()) {
                       tout << neg_l << " " << w.get_literal() << "\n";
                   }
               }
@@ -294,7 +294,7 @@ namespace sat{
     bool elim_vars::mark_literals(literal lit) {
         watch_list& wl = simp.get_wlist(lit);
         for (watched const& w : wl) {
-            if (w.is_binary_non_learned_clause()) {
+            if (w.is_binary_unblocked_clause()) {
                 mark_var(w.get_literal().var());
             }
         }
@@ -306,6 +306,7 @@ namespace sat{
         clause_use_list::iterator it = occs.mk_iterator();
         while (!it.at_end()) {
             clause const& c = it.curr();
+            if (c.is_blocked()) continue;
             bdd cl = m.mk_false();
             for (literal l : c) {
                 cl |= mk_literal(l);
@@ -320,7 +321,7 @@ namespace sat{
         bdd result = m.mk_true();
         watch_list& wl = simp.get_wlist(~lit);
         for (watched const& w : wl) {
-            if (w.is_binary_non_learned_clause()) {
+            if (w.is_binary_unblocked_clause()) {
                 result &= (mk_literal(lit) || mk_literal(w.get_literal()));
             }
         }        

src/sat/sat_local_search.cpp

@@ -304,7 +304,7 @@ namespace sat {
                 watch_list::const_iterator it  = wlist.begin();
                 watch_list::const_iterator end = wlist.end();
                 for (; it != end; ++it) {
-                    if (!it->is_binary_non_learned_clause())
+                    if (!it->is_binary_unblocked_clause())
                         continue;
                     literal l2 = it->get_literal();
                     if (l1.index() > l2.index()) 

src/sat/sat_lookahead.cpp

@@ -965,7 +965,7 @@ namespace sat {
             if (m_s.was_eliminated(l.var())) continue;
             watch_list const & wlist = m_s.m_watches[l_idx];
             for (auto& w : wlist) {
-                if (!w.is_binary_non_learned_clause())
+                if (!w.is_binary_clause())
                     continue;
                 literal l2 = w.get_literal();                    
                 if (l.index() < l2.index() && !m_s.was_eliminated(l2.var()))

src/sat/sat_simplifier.cpp

@@ -34,26 +34,29 @@ namespace sat {
     }
 
     void use_list::insert(clause & c) {
-        unsigned sz = c.size();
+        for (literal l : c) 
-        for (unsigned i = 0; i < sz; i++) {
+            m_use_list[l.index()].insert(c);
-            m_use_list[c[i].index()].insert(c);
-        }
     }
 
     void use_list::erase(clause & c) {
-        unsigned sz = c.size();
+        for (literal l : c) 
-        for (unsigned i = 0; i < sz; i++) {
+            m_use_list[l.index()].erase(c);
-            m_use_list[c[i].index()].erase(c);
-        }
     }
 
     void use_list::erase(clause & c, literal l) {
-        unsigned sz = c.size();
+        for (literal l2 : c) 
-        for (unsigned i = 0; i < sz; i++) {
-            literal l2 = c[i];
             if (l2 != l)
                 m_use_list[l2.index()].erase(c);
-        }
+    }
+
+    void use_list::block(clause& c) {
+        for (literal l : c) 
+            m_use_list[l.index()].block(c);
+    }
+
+    void use_list::unblock(clause& c) {
+        for (literal l : c) 
+            m_use_list[l.index()].unblock(c);
     }
 
     simplifier::simplifier(solver & _s, params_ref const & p):
@@ -99,9 +102,8 @@ namespace sat {
     }
 
     inline void simplifier::remove_clause_core(clause & c) {
-        unsigned sz = c.size();
+        for (literal l : c) 
-        for (unsigned i = 0; i < sz; i++)
+            insert_elim_todo(l.var());
-            insert_elim_todo(c[i].var());
         m_sub_todo.erase(c);
         c.set_removed(true);
         TRACE("resolution_bug", tout << "del_clause: " << c << "\n";);
@@ -118,6 +120,20 @@ namespace sat {
         m_use_list.erase(c, l);
     }
 
+    inline void simplifier::block_clause(clause & c) {
+#if 1
+        remove_clause(c);
+#else
+        c.block();
+        m_use_list.block(c);
+#endif
+    }
+
+    inline void simplifier::unblock_clause(clause & c) {
+        c.unblock();
+        m_use_list.unblock(c);
+    }
+
     inline void simplifier::remove_bin_clause_half(literal l1, literal l2, bool learned) {
         SASSERT(s.get_wlist(~l1).contains(watched(l2, learned)));
         s.get_wlist(~l1).erase(watched(l2, learned));
@@ -238,10 +254,7 @@ namespace sat {
        \brief Eliminate all ternary and clause watches.
     */
     void simplifier::cleanup_watches() {
-        vector<watch_list>::iterator it  = s.m_watches.begin();
+        for (watch_list& wlist : s.m_watches) {
-        vector<watch_list>::iterator end = s.m_watches.end();
-        for (; it != end; ++it) {
-            watch_list & wlist = *it;
             watch_list::iterator it2    = wlist.begin();
             watch_list::iterator itprev = it2;
             watch_list::iterator end2   = wlist.end();
@@ -345,11 +358,9 @@ namespace sat {
        \brief Return the variable in c with the minimal number positive+negative occurrences.
     */
     bool_var simplifier::get_min_occ_var(clause const & c) const {
-        literal l_best = c[0];
+        literal l_best = null_literal;
-        unsigned best  = m_use_list.get(l_best).size() + m_use_list.get(~l_best).size();
+        unsigned best = UINT_MAX;
-        unsigned sz = c.size();
+        for (literal l : c) {
-        for (unsigned i = 1; i < sz; i++) {
-            literal l = c[i];
             unsigned num = m_use_list.get(l).size() + m_use_list.get(~l).size();
             if (num < best) {
                 l_best = l;
@@ -394,6 +405,7 @@ namespace sat {
     */
     void simplifier::collect_subsumed1_core(clause const & c1, clause_vector & out, literal_vector & out_lits,
                                             literal target) {
+        if (c1.is_blocked()) return;
         clause_use_list const & cs = m_use_list.get(target);
         clause_use_list::iterator it = cs.mk_iterator();
         while (!it.at_end()) {
@@ -424,7 +436,7 @@ namespace sat {
     }
 
     /**
-       \brief Perform backward subsumption and self-subsumption resolution using c.
+       \brief Perform backward subsumption and self-subsumption resolution using c1.
     */
     void simplifier::back_subsumption1(clause & c1) {
         m_bs_cs.reset();
@@ -440,11 +452,13 @@ namespace sat {
                 // c2 was subsumed
                 if (c1.is_learned() && !c2.is_learned())
                     c1.unset_learned();
+                else if (c1.is_blocked() && !c2.is_learned() && !c2.is_blocked()) 
+                    unblock_clause(c1);
                 TRACE("subsumption", tout << c1 << " subsumed " << c2 << "\n";);
                 remove_clause(c2);
                 m_num_subsumed++;
             }
-            else if (!c2.was_removed()) {
+            else if (!c2.was_removed() && !c1.is_blocked()) {
                 // subsumption resolution
                 TRACE("subsumption_resolution", tout << c1 << " sub-ref(" << *l_it << ") " << c2 << "\n";);
                 elim_lit(c2, *l_it);
@@ -466,11 +480,9 @@ namespace sat {
        \brief Return the literal in c with the minimal number of occurrences.
     */
     literal simplifier::get_min_occ_var0(clause const & c) const {
-        literal l_best = c[0];
+        literal l_best = null_literal;
-        unsigned best  = m_use_list.get(l_best).size();
+        unsigned best = UINT_MAX;
-        unsigned sz = c.size();
+        for (literal l : c) {
-        for (unsigned i = 1; i < sz; i++) {
-            literal l = c[i];
             unsigned num = m_use_list.get(l).size();
             if (num < best) {
                 l_best = l;
@@ -485,21 +497,19 @@ namespace sat {
        Otherwise return false
     */
     bool simplifier::subsumes0(clause const & c1, clause const & c2) {
-        unsigned sz2 = c2.size();
+        for (literal l : c2) 
-        for (unsigned i = 0; i < sz2; i++)
+            mark_visited(l);
-            mark_visited(c2[i]);
 
         bool r = true;
-        unsigned sz1 = c1.size();
+        for (literal l : c1) {
-        for (unsigned i = 0; i < sz1; i++) {
+            if (!is_marked(l)) {
-            if (!is_marked(c1[i])) {
                 r = false;
                 break;
             }
         }
 
-        for (unsigned i = 0; i < sz2; i++)
+        for (literal l : c2)
-            unmark_visited(c2[i]);
+            unmark_visited(l);
 
         return r;
     }
@@ -508,6 +518,7 @@ namespace sat {
        \brief Collect the clauses subsumed by c1 (using the occurrence list of target).
     */
     void simplifier::collect_subsumed0_core(clause const & c1, clause_vector & out, literal target) {
+        if (c1.is_blocked()) return;
         clause_use_list const & cs = m_use_list.get(target);
         clause_use_list::iterator it = cs.mk_iterator();
         while (!it.at_end()) {
@@ -540,10 +551,8 @@ namespace sat {
     void simplifier::back_subsumption0(clause & c1) {
         m_bs_cs.reset();
         collect_subsumed0(c1, m_bs_cs);
-        clause_vector::iterator it    = m_bs_cs.begin();
+        for (clause* cp : m_bs_cs) {
-        clause_vector::iterator end   = m_bs_cs.end();
+            clause & c2 = *cp;
-        for (; it != end; ++it) {
-            clause & c2 = *(*it);
             // c2 was subsumed
             if (c1.is_learned() && !c2.is_learned())
                 c1.unset_learned();
@@ -951,13 +960,17 @@ namespace sat {
             return !s.s.is_assumption(v) &&  !s.was_eliminated(v) && !s.is_external(v);
         }
 
-        void operator()(unsigned num_vars) {
+        void insert_queue(unsigned num_vars) {
             for (bool_var v = 0; v < num_vars; v++) {
                 if (process_var(v)) {
                     insert(literal(v, false));
                     insert(literal(v, true));
                 }
             }
+        }
+
+        void block_clauses(unsigned num_vars) {
+            insert_queue(num_vars);
             while (!m_queue.empty()) {
                 s.checkpoint();
                 if (m_counter < 0)
@@ -965,7 +978,73 @@ namespace sat {
                 literal l = m_queue.next();
                 process(l);
             }
-            cce();
+        }
+
+        void operator()(unsigned num_vars) {
+            block_clauses(num_vars);
+            if (s.m_elim_covered_clauses) 
+                cce();
+        }
+
+        void process(literal l) {
+            TRACE("blocked_clause", tout << "processing: " << l << "\n";);
+            model_converter::entry * new_entry = 0;
+            if (!process_var(l.var())) {
+                return;
+            }
+
+            literal blocked = null_literal;
+            m_to_remove.reset();
+            {
+                clause_use_list & occs = s.m_use_list.get(l);
+                clause_use_list::iterator it = occs.mk_iterator();
+                while (!it.at_end()) {
+                    clause & c = it.curr();
+                    if (c.is_blocked()) continue;
+                    m_counter -= c.size();
+                    SASSERT(c.contains(l));
+                    s.mark_all_but(c, l);
+                    if (all_tautology(l)) {
+                        block_clause(c, l, new_entry);
+                        s.m_num_blocked_clauses++;
+                    }
+                    s.unmark_all(c);
+                    it.next();
+                }
+            }
+            for (clause* c : m_to_remove) 
+                s.block_clause(*c);
+
+            {
+                watch_list & wlist = s.get_wlist(~l);
+                m_counter -= wlist.size();
+                watch_list::iterator it  = wlist.begin();
+                watch_list::iterator it2 = it;
+                watch_list::iterator end = wlist.end();
+                for (; it != end; ++it) {
+                    if (!it->is_binary_clause() || it->is_blocked()) {
+                        *it2 = *it;
+                        it2++;
+                        continue;
+                    }
+                    literal l2 = it->get_literal();
+                    s.mark_visited(l2);
+                    if (all_tautology(l)) {
+                        block_binary(it, l, new_entry);
+                        s.m_num_blocked_clauses++;
+                    }
+                    else if (s.m_elim_covered_clauses && cce(l, l2, blocked)) {
+                        block_covered_binary(it, l, blocked);
+                        s.m_num_covered_clauses++;
+                    }
+                    else {
+                        *it2 = *it;
+                        it2++;
+                    }
+                    s.unmark_visited(l2);
+                }
+                wlist.set_end(it2);
+            }
         }
 
         //
@@ -976,7 +1055,7 @@ namespace sat {
             if (!process_var(l.var())) return false;
             bool first = true;
             for (watched & w : s.get_wlist(l)) {
-                if (w.is_binary_non_learned_clause()) {
+                if (w.is_binary_unblocked_clause()) {
                     literal lit = w.get_literal();
                     if (s.is_marked(~lit) && lit != ~l) continue;
                     if (!first) {
@@ -992,6 +1071,7 @@ namespace sat {
             while (!it.at_end()) {
                 bool tautology = false;
                 clause & c = it.curr();
+                if (c.is_blocked()) continue;
                 for (literal lit : c) {
                     if (s.is_marked(~lit) && lit != ~l) {
                         tautology = true;
@@ -1007,16 +1087,9 @@ namespace sat {
                     }
                     else {
                         unsigned j = 0;
-                        unsigned sz = inter.size();
+                        for (literal lit : inter) 
-                        for (unsigned i = 0; i < sz; ++i) {
+                            if (c.contains(lit)) 
-                            literal lit1 = inter[i];
+                                inter[j++] = lit;
-                            for (literal lit2 : c) {
-                                if (lit1 == lit2) {
-                                    inter[j++] = lit1;
-                                    break;
-                                }
-                            }
-                        }
                         inter.shrink(j);
                         if (j == 0) return false;
                     }
@@ -1052,6 +1125,14 @@ namespace sat {
             }
         }
 
+
+        /*
+         *  C \/ l    ~l \/ lit \/ D_i   for i = 1...N all the clauses that have ~l
+         *  -------------------------
+         *      C \/ l \/ lit
+         *
+         *
+         */
         bool add_cla(literal& blocked) {
             for (unsigned i = 0; i < m_covered_clause.size(); ++i) {
                 m_intersection.reset();
@@ -1059,15 +1140,15 @@ namespace sat {
                     blocked = m_covered_clause[i];
                     return true;
                 }
+                if (!m_intersection.empty()) {
+                    m_elim_stack.push_back(std::make_pair(m_covered_clause.size(), m_covered_clause[i]));
+                }
                 for (literal l : m_intersection) {
                     if (!s.is_marked(l)) {
                         s.mark_visited(l);
                         m_covered_clause.push_back(l);
                     }
                 }
-                if (!m_intersection.empty()) {
-                    m_elim_stack.push_back(std::make_pair(m_covered_clause.size(), m_covered_clause[i]));
-                }
             }
             return false;
         }
@@ -1085,14 +1166,18 @@ namespace sat {
                     is_tautology = add_cla(blocked);
                 }
                 while (m_covered_clause.size() > sz && !is_tautology);
+#if 1
                 break;
-                //if (is_tautology) break;
+#else
-                //sz = m_covered_clause.size();
+                // check for soundness?
-                // unsound? add_ala();
+                if (is_tautology) break;
+                sz = m_covered_clause.size();
+                add_ala();
+#endif
             }
             while (m_covered_clause.size() > sz);
             for (literal l : m_covered_clause) s.unmark_visited(l);
-            // if (is_tautology) std::cout << "taut: " << num_iterations << " " << m_covered_clause.size() << " " << m_elim_stack.size() << "\n";
+            if (is_tautology) std::cout << "taut: " << num_iterations << " " << m_covered_clause.size() << " " << m_elim_stack.size() << "\n";
             return is_tautology;
         }
 
@@ -1105,9 +1190,9 @@ namespace sat {
             return cla(blocked);
         }
 
-        bool cce(literal lit, literal l2, literal& blocked) {
+        bool cce(literal l1, literal l2, literal& blocked) {
             m_covered_clause.reset();
-            m_covered_clause.push_back(lit);
+            m_covered_clause.push_back(l1);
             m_covered_clause.push_back(l2);
             return cla(blocked);            
         }
@@ -1117,79 +1202,17 @@ namespace sat {
             literal blocked;
             for (clause* cp : s.s.m_clauses) {
                 clause& c = *cp;
-                if (c.was_removed()) continue;
+                if (!c.was_removed() && !c.is_blocked() && cce(c, blocked)) {
-                if (cce(c, blocked)) {
+                    block_covered_clause(c, blocked);
-                    model_converter::entry * new_entry = 0;
-                    block_covered_clause(c, blocked, new_entry);
                     s.m_num_covered_clauses++;                    
                 }
             }
             for (clause* c : m_to_remove) {
-                s.remove_clause(*c);
+                s.block_clause(*c);
             }
             m_to_remove.reset();
         }
 
-        void process(literal l) {
-            TRACE("blocked_clause", tout << "processing: " << l << "\n";);
-            model_converter::entry * new_entry = 0;
-            if (!process_var(l.var())) {
-                return;
-            }
-
-            literal blocked = null_literal;
-            m_to_remove.reset();
-            {
-                clause_use_list & occs = s.m_use_list.get(l);
-                clause_use_list::iterator it = occs.mk_iterator();
-                while (!it.at_end()) {
-                    clause & c = it.curr();
-                    m_counter -= c.size();
-                    SASSERT(c.contains(l));
-                    s.mark_all_but(c, l);
-                    if (all_tautology(l)) {
-                        block_clause(c, l, new_entry);
-                        s.m_num_blocked_clauses++;
-                    }
-                    s.unmark_all(c);
-                    it.next();
-                }
-            }
-            for (clause* c : m_to_remove) {
-                s.remove_clause(*c);
-            }
-            {
-                watch_list & wlist = s.get_wlist(~l);
-                m_counter -= wlist.size();
-                watch_list::iterator it  = wlist.begin();
-                watch_list::iterator it2 = it;
-                watch_list::iterator end = wlist.end();
-                for (; it != end; ++it) {
-                    if (!it->is_binary_clause()) {
-                        *it2 = *it;
-                        it2++;
-                        continue;
-                    }
-                    literal l2 = it->get_literal();
-                    s.mark_visited(l2);
-                    if (all_tautology(l)) {
-                        block_binary(it, l, new_entry);
-                        s.m_num_blocked_clauses++;
-                    }
-                    else if (cce(l, l2, blocked)) {
-                        model_converter::entry * blocked_entry = 0;
-                        block_covered_binary(it, l, blocked, blocked_entry);
-                        s.m_num_covered_clauses++;
-                    }
-                    else {
-                        *it2 = *it;
-                        it2++;
-                    }
-                    s.unmark_visited(l2);
-                }
-                wlist.set_end(it2);
-            }
-        }
 
         void prepare_block_clause(clause& c, literal l, model_converter::entry*& new_entry) {
             TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";);
@@ -1208,7 +1231,8 @@ namespace sat {
             mc.insert(*new_entry, c);
         }
 
-        void block_covered_clause(clause& c, literal l, model_converter::entry *& new_entry) {
+        void block_covered_clause(clause& c, literal l) {
+            model_converter::entry * new_entry = 0;
             prepare_block_clause(c, l, new_entry);
             mc.insert(*new_entry, m_covered_clause, m_elim_stack);
         }
@@ -1227,7 +1251,8 @@ namespace sat {
             mc.insert(*new_entry, l, it->get_literal());
         }
 
-        void block_covered_binary(watch_list::iterator it, literal l, literal blocked, model_converter::entry *& new_entry) {
+        void block_covered_binary(watch_list::iterator it, literal l, literal blocked) {
+            model_converter::entry * new_entry = 0;
             prepare_block_binary(it, l, blocked, new_entry);
             mc.insert(*new_entry, m_covered_clause, m_elim_stack);
         }
@@ -1236,7 +1261,7 @@ namespace sat {
             watch_list & wlist = s.get_wlist(l);
             m_counter -= wlist.size();
             for (auto const& w : wlist) {
-                if (w.is_binary_non_learned_clause() && 
+                if (w.is_binary_unblocked_clause() && 
                     !s.is_marked(~w.get_literal()))
                     return false;
             }
@@ -1245,6 +1270,7 @@ namespace sat {
             clause_use_list::iterator it = neg_occs.mk_iterator();
             while (!it.at_end()) {
                 clause & c = it.curr();
+                if (c.is_blocked()) continue;
                 m_counter -= c.size();
                 unsigned sz = c.size();
                 unsigned i;
@@ -1300,11 +1326,11 @@ namespace sat {
         elim(s.num_vars());
     }
 
-    unsigned simplifier::get_num_non_learned_bin(literal l) const {
+    unsigned simplifier::get_num_unblocked_bin(literal l) const {
         unsigned r = 0;
         watch_list const & wlist = get_wlist(~l);
         for (auto & w : wlist) {
-            if (w.is_binary_non_learned_clause())
+            if (w.is_binary_unblocked_clause())
                 r++;
         }
         return r;
@@ -1315,8 +1341,8 @@ namespace sat {
         literal neg_l(v, true);
         unsigned num_pos = m_use_list.get(pos_l).size();
         unsigned num_neg = m_use_list.get(neg_l).size();
-        unsigned num_bin_pos = get_num_non_learned_bin(pos_l);
+        unsigned num_bin_pos = get_num_unblocked_bin(pos_l);
-        unsigned num_bin_neg = get_num_non_learned_bin(neg_l);
+        unsigned num_bin_neg = get_num_unblocked_bin(neg_l);
         unsigned cost = 2 * num_pos * num_neg + num_pos * num_bin_neg + num_neg * num_bin_pos;
         CTRACE("elim_vars_detail", cost == 0, tout << v << " num_pos: " << num_pos << " num_neg: " << num_neg << " num_bin_pos: " << num_bin_pos
                << " num_bin_neg: " << num_bin_neg << " cost: " << cost << "\n";);
@@ -1353,20 +1379,32 @@ namespace sat {
     /**
        \brief Collect clauses and binary clauses containing l.
     */
-    void simplifier::collect_clauses(literal l, clause_wrapper_vector & r) {
+    void simplifier::collect_clauses(literal l, clause_wrapper_vector & r, bool include_blocked) {
         clause_use_list const & cs = m_use_list.get(l);
         clause_use_list::iterator it = cs.mk_iterator();
         while (!it.at_end()) {
-            r.push_back(clause_wrapper(it.curr()));
+            if (!it.curr().is_blocked() || include_blocked) {
-            SASSERT(r.back().size() == it.curr().size());
+                r.push_back(clause_wrapper(it.curr()));
+                SASSERT(r.back().size() == it.curr().size());
+            }
             it.next();
         }
 
         watch_list & wlist = get_wlist(~l);
-        for (auto & w : wlist) {
+        if (include_blocked) {
-            if (w.is_binary_non_learned_clause()) {
+            for (auto & w : wlist) {
-                r.push_back(clause_wrapper(l, w.get_literal()));
+                if (w.is_binary_non_learned_clause2()) {
-                SASSERT(r.back().size() == 2);
+                    r.push_back(clause_wrapper(l, w.get_literal()));
+                    SASSERT(r.back().size() == 2);
+                }
+            }
+        }
+        else {
+            for (auto & w : wlist) {
+                if (w.is_binary_unblocked_clause()) {
+                    r.push_back(clause_wrapper(l, w.get_literal()));
+                    SASSERT(r.back().size() == 2);
+                }
             }
         }
     }
@@ -1503,12 +1541,12 @@ namespace sat {
 
         literal pos_l(v, false);
         literal neg_l(v, true);
-        unsigned num_bin_pos = get_num_non_learned_bin(pos_l);
+        unsigned num_bin_pos = get_num_unblocked_bin(pos_l);
-        unsigned num_bin_neg = get_num_non_learned_bin(neg_l);
+        unsigned num_bin_neg = get_num_unblocked_bin(neg_l);
         clause_use_list & pos_occs = m_use_list.get(pos_l);
         clause_use_list & neg_occs = m_use_list.get(neg_l);
-        unsigned num_pos = pos_occs.size() + num_bin_pos;
+        unsigned num_pos = pos_occs.non_blocked_size() + num_bin_pos;
-        unsigned num_neg = neg_occs.size() + num_bin_neg;
+        unsigned num_neg = neg_occs.non_blocked_size() + num_bin_neg;
 
         TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << "\n";);
 
@@ -1520,7 +1558,8 @@ namespace sat {
         {
             clause_use_list::iterator it = pos_occs.mk_iterator();
             while (!it.at_end()) {
-                before_lits += it.curr().size();
+                if (!it.curr().is_blocked())
+                    before_lits += it.curr().size();
                 it.next();
             }
         }
@@ -1528,7 +1567,8 @@ namespace sat {
         {
             clause_use_list::iterator it2 = neg_occs.mk_iterator();
             while (!it2.at_end()) {
-                before_lits += it2.curr().size();
+                if (!it2.curr().is_blocked())
+                    before_lits += it2.curr().size();
                 it2.next();
             }
         }
@@ -1546,8 +1586,8 @@ namespace sat {
 
         m_pos_cls.reset();
         m_neg_cls.reset();
-        collect_clauses(pos_l, m_pos_cls);
+        collect_clauses(pos_l, m_pos_cls, false);
-        collect_clauses(neg_l, m_neg_cls);
+        collect_clauses(neg_l, m_neg_cls, false);
 
 
         TRACE("resolution_detail", tout << "collecting number of after_clauses\n";);
@@ -1676,6 +1716,7 @@ namespace sat {
 
     void simplifier::updt_params(params_ref const & _p) {
         sat_simplifier_params p(_p);
+        m_elim_covered_clauses    = p.elim_covered_clauses();
         m_elim_blocked_clauses    = p.elim_blocked_clauses();
         m_elim_blocked_clauses_at = p.elim_blocked_clauses_at();
         m_blocked_clause_limit    = p.blocked_clause_limit();
@@ -1693,6 +1734,7 @@ namespace sat {
         m_subsumption             = p.subsumption();
         m_subsumption_limit       = p.subsumption_limit();
         m_elim_vars               = p.elim_vars();
+        m_elim_vars_bdd           = p.elim_vars_bdd();
     }
 
     void simplifier::collect_param_descrs(param_descrs & r) {

src/sat/sat_simplifier.h

@@ -40,6 +40,8 @@ namespace sat {
     public:
         void init(unsigned num_vars);
         void insert(clause & c);
+        void block(clause & c);
+        void unblock(clause & c);
         void erase(clause & c);
         void erase(clause & c, literal l);
         clause_use_list & get(literal l) { return m_use_list[l.index()]; }
@@ -69,6 +71,7 @@ namespace sat {
         int                    m_elim_counter;
 
         // config
+        bool                   m_elim_covered_clauses;
         bool                   m_elim_blocked_clauses;
         unsigned               m_elim_blocked_clauses_at;
         unsigned               m_blocked_clause_limit;
@@ -87,6 +90,7 @@ namespace sat {
         bool                   m_subsumption;
         unsigned               m_subsumption_limit;
         bool                   m_elim_vars;
+        bool                   m_elim_vars_bdd;
 
         // stats
         unsigned               m_num_blocked_clauses;
@@ -119,6 +123,8 @@ namespace sat {
         void remove_clause_core(clause & c);
         void remove_clause(clause & c);
         void remove_clause(clause & c, literal l);
+        void block_clause(clause & c);
+        void unblock_clause(clause & c);
         void remove_bin_clause_half(literal l1, literal l2, bool learned);
 
         bool_var get_min_occ_var(clause const & c) const;
@@ -157,10 +163,10 @@ namespace sat {
         struct blocked_clause_elim;
         void elim_blocked_clauses();
 
-        unsigned get_num_non_learned_bin(literal l) const;
+        unsigned get_num_unblocked_bin(literal l) const;
         unsigned get_to_elim_cost(bool_var v) const;
         void order_vars_for_elim(bool_var_vector & r);
-        void collect_clauses(literal l, clause_wrapper_vector & r);
+        void collect_clauses(literal l, clause_wrapper_vector & r, bool include_blocked);
         clause_wrapper_vector m_pos_cls;
         clause_wrapper_vector m_neg_cls;
         literal_vector m_new_cls;

src/sat/sat_simplifier_params.pyg

@@ -2,6 +2,7 @@ def_module_params(module_name='sat',
                   class_name='sat_simplifier_params',
                   export=True,
                   params=(('elim_blocked_clauses', BOOL, False, 'eliminate blocked clauses'),
+                          ('elim_covered_clauses', BOOL, False, 'eliminate covered clauses'),
                           ('elim_blocked_clauses_at', UINT, 2, 'eliminate blocked clauses only once at the given simplification round'),
                           ('blocked_clause_limit', UINT, 100000000, 'maximum number of literals visited during blocked clause elimination'),
                           ('resolution', BOOL, True, 'eliminate boolean variables using resolution'),
@@ -16,5 +17,6 @@ def_module_params(module_name='sat',
                           ('resolution.cls_cutoff1', UINT, 100000000, 'limit1 - total number of problems clauses for the second cutoff of Boolean variable elimination'),
                           ('resolution.cls_cutoff2', UINT, 700000000, 'limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination'),
                           ('elim_vars', BOOL, True, 'enable variable elimination during simplification'),
+                          ('elim_vars_bdd', BOOL, True, 'enable variable elimination using BDD recompilation during simplification'),
                           ('subsumption', BOOL, True, 'eliminate subsumed clauses'),
                           ('subsumption.limit', UINT, 100000000, 'approx. maximum number of literals visited during subsumption (and subsumption resolution)')))

src/sat/sat_solver.cpp

@@ -117,7 +117,7 @@ namespace sat {
             assign(src.m_trail[i], justification());
         }
 
-        // copy binary clauses
+        // copy binary clauses that are unblocked.
         {
             unsigned sz = src.m_watches.size();
             for (unsigned l_idx = 0; l_idx < sz; ++l_idx) {
@@ -125,7 +125,7 @@ namespace sat {
                 if (src.was_eliminated(l.var())) continue;
                 watch_list const & wlist = src.m_watches[l_idx];
                 for (auto & wi : wlist) {
-                    if (!wi.is_binary_non_learned_clause())
+                    if (!wi.is_binary_unblocked_clause())
                         continue;
                     literal l2 = wi.get_literal();
                     if (l.index() > l2.index() ||
@@ -142,7 +142,10 @@ namespace sat {
             for (clause* c : src.m_clauses) {
                 buffer.reset();
                 for (literal l : *c) buffer.push_back(l);
-                mk_clause_core(buffer);
+                clause* c1 = mk_clause_core(buffer);
+                if (c1 && c->is_blocked()) {
+                    c1->block();
+                }
             }
             // copy high quality lemmas
             for (clause* c : src.m_learned) {
@@ -1558,8 +1561,8 @@ namespace sat {
         m_mc(m_model);
         TRACE("sat", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";);
 
-#ifndef _EXTERNAL_RELEASE
+// #ifndef _EXTERNAL_RELEASE
-        IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"checking model\"\n";);
+        IF_VERBOSE(1, verbose_stream() << "\"checking model\"\n";);
         if (!check_model(m_model))
             throw solver_exception("check model failed");
 
@@ -1568,7 +1571,7 @@ namespace sat {
             if (!m_clone->check_model(m_model))
                 throw solver_exception("check model failed (for cloned solver)");
         }
-#endif
+// #endif
     }
 
     bool solver::check_model(model const & m) const {
@@ -3124,17 +3127,14 @@ namespace sat {
         for (unsigned l_idx = 0; l_idx < sz; l_idx++) {
             literal l = to_literal(l_idx);
             l.neg();
-            watch_list const & wlist = m_watches[l_idx];
+            for (watched const& w : m_watches[l_idx]) {
-            watch_list::const_iterator it  = wlist.begin();
+                if (!w.is_binary_clause())
-            watch_list::const_iterator end = wlist.end();
-            for (; it != end; ++it) {
-                if (!it->is_binary_clause())
                     continue;
-                if (!learned && it->is_learned())
+                if (!learned && w.is_learned())
                     continue;
-                else if (learned && learned_only && !it->is_learned()) 
+                else if (learned && learned_only && !w.is_learned()) 
                     continue;
-                literal l2 = it->get_literal();
+                literal l2 = w.get_literal();
                 if (l.index() > l2.index())
                     continue;
                 TRACE("cleanup_bug", tout << "collected: " << l << " " << l2 << "\n";);
@@ -3168,13 +3168,10 @@ namespace sat {
         for (unsigned l_idx = 0; l_idx < sz; l_idx++) {
             literal l = to_literal(l_idx);
             l.neg();
-            watch_list const & wlist = m_watches[l_idx];
+            for (watched const& w : m_watches[l_idx]) {
-            watch_list::const_iterator it  = wlist.begin();
+                if (!w.is_binary_clause())
-            watch_list::const_iterator end = wlist.end();
-            for (; it != end; ++it) {
-                if (!it->is_binary_clause())
                     continue;
-                literal l2 = it->get_literal();
+                literal l2 = w.get_literal();
                 if (l.index() > l2.index())
                     continue;
                 out << "(" << l << " " << l2 << ")\n";

src/sat/sat_solver.h

@@ -220,8 +220,8 @@ namespace sat {
     protected:
         void del_clause(clause & c);
         clause * mk_clause_core(unsigned num_lits, literal * lits, bool learned);
-        void mk_clause_core(literal_vector const& lits) { mk_clause_core(lits.size(), lits.c_ptr()); }
+        clause * mk_clause_core(literal_vector const& lits) { return mk_clause_core(lits.size(), lits.c_ptr()); }
-        void mk_clause_core(unsigned num_lits, literal * lits) { mk_clause_core(num_lits, lits, false); }
+        clause * mk_clause_core(unsigned num_lits, literal * lits) { return mk_clause_core(num_lits, lits, false); }
         void mk_clause_core(literal l1, literal l2) { literal lits[2] = { l1, l2 }; mk_clause_core(2, lits); }
         void mk_bin_clause(literal l1, literal l2, bool learned);
         bool propagate_bin_clause(literal l1, literal l2);

src/sat/sat_watched.h

@@ -50,7 +50,7 @@ namespace sat {
             SASSERT(is_binary_clause());
             SASSERT(get_literal() == l);
             SASSERT(is_learned() == learned);
-            SASSERT(learned || is_binary_non_learned_clause());
+            SASSERT(learned || is_binary_unblocked_clause());
         }
 
         watched(literal l1, literal l2) {
@@ -85,8 +85,15 @@ namespace sat {
         literal get_literal() const { SASSERT(is_binary_clause()); return to_literal(static_cast<unsigned>(m_val1)); }
         void set_literal(literal l) { SASSERT(is_binary_clause()); m_val1 = l.to_uint(); }
         bool is_learned() const { SASSERT(is_binary_clause()); return (m_val2 >> 2) == 1; }
-        bool is_binary_non_learned_clause() const { return m_val2 == 0; }
+
+        bool is_binary_unblocked_clause() const { return m_val2 == 0; }
+        bool is_binary_learned_clause() const { return is_binary_clause() && is_learned(); }
+        bool is_binary_non_learned_clause2() const { return is_binary_clause() && !is_learned(); }
+
         void mark_not_learned() { SASSERT(is_learned()); m_val2 = static_cast<unsigned>(BINARY); SASSERT(!is_learned()); }
+        void set_blocked() { SASSERT(is_binary_clause()); SASSERT(!is_learned()); m_val2 |= (1 << 3); }
+        bool is_blocked() const { SASSERT(is_binary_clause()); return 0 != (m_val2 & (1 << 3)); }
+        void set_unblocked() { SASSERT(is_binary_clause()); SASSERT(is_blocked()); m_val2 &= ~(1u << 3u); }
         
         bool is_ternary_clause() const { return get_kind() == TERNARY; }
         literal get_literal1() const { SASSERT(is_ternary_clause()); return to_literal(static_cast<unsigned>(m_val1)); }

src/shell/dimacs_frontend.cpp

@@ -21,9 +21,9 @@ Revision History:
 #include<signal.h>
 #include "util/timeout.h"
 #include "util/rlimit.h"
+#include "util/gparams.h"
 #include "sat/dimacs.h"
 #include "sat/sat_solver.h"
-#include "util/gparams.h"
 
 extern bool          g_display_statistics;
 static sat::solver * g_solver = 0;
@@ -126,6 +126,42 @@ static void track_clauses(sat::solver const& src,
     }
 }
 
+void verify_solution(char const * file_name) {
+    params_ref p = gparams::get_module("sat");
+    p.set_bool("produce_models", true);
+    reslimit limit;
+    sat::solver solver(p, limit);
+    std::ifstream in(file_name);
+    if (in.bad() || in.fail()) {
+        std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl;
+        exit(ERR_OPEN_FILE);
+    }
+    parse_dimacs(in, solver);
+    
+    sat::model const & m = g_solver->get_model();
+    for (unsigned i = 1; i < m.size(); i++) {
+        sat::literal lit(i, false);
+        switch (m[i]) {
+        case l_false: lit.neg(); break;
+        case l_undef: break;
+        case l_true: break;
+        }
+        solver.mk_clause(1, &lit);
+    }
+    lbool r = solver.check();
+    switch (r) {
+    case l_false: 
+        std::cout << "model checking failed\n";
+        break;
+    case l_true:
+        std::cout << "model validated\n";
+        break;
+    default:
+        std::cout << "inconclusive model\n";
+        break;
+    }
+}
+
 unsigned read_dimacs(char const * file_name) {
     g_start_time = clock();
     register_on_timeout_proc(on_timeout);
@@ -164,6 +200,7 @@ unsigned read_dimacs(char const * file_name) {
     switch (r) {
     case l_true: 
         std::cout << "sat\n"; 
+        if (file_name) verify_solution(file_name);
         display_model(*g_solver);
         break;
     case l_undef: