From 9f9ae4427de529643b9f18d2c0e77040a02c01fb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 15 Oct 2017 15:13:43 -0700
Subject: [PATCH] add cce

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_bdd.cpp             |  35 ++++--
 src/sat/sat_bdd.h               | 108 ++++++++++---------
 src/sat/sat_elim_vars.cpp       |  44 ++------
 src/sat/sat_elim_vars.h         |   1 -
 src/sat/sat_model_converter.cpp |   9 +-
 src/sat/sat_simplifier.cpp      | 186 ++++++++++++++++++++++++++------
 src/sat/sat_simplifier.h        |   1 +
 src/sat/sat_solver.cpp          |   2 +
 src/sat/sat_solver.h            |   2 +
 src/test/bdd.cpp                |  10 +-
 10 files changed, 259 insertions(+), 139 deletions(-)

diff --git a/src/sat/sat_bdd.cpp b/src/sat/sat_bdd.cpp
index 36900760e..edc8ad2a8 100644
--- a/src/sat/sat_bdd.cpp
+++ b/src/sat/sat_bdd.cpp
@@ -21,7 +21,7 @@ Revision History:
 
 namespace sat {
 
-    bdd_manager::bdd_manager(unsigned num_vars, unsigned cache_size) {
+    bdd_manager::bdd_manager(unsigned num_vars) {
         for (BDD a = 0; a < 2; ++a) {
             for (BDD b = 0; b < 2; ++b) {
                 for (unsigned op = bdd_and_op; op < bdd_not_op; ++op) {                
@@ -84,7 +84,7 @@ namespace sat {
             try {
                 return apply_rec(arg1, arg2, op);
             }
-            catch (bdd_exception) {
+            catch (mem_out) {
                 try_reorder();
                 if (!first) throw;
                 first = false;
@@ -92,6 +92,16 @@ namespace sat {
         }
     }
 
+
+    bdd bdd_manager::mk_true() { return bdd(true_bdd, this); }
+    bdd bdd_manager::mk_false() { return bdd(false_bdd, this); }
+    bdd bdd_manager::mk_and(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_and_op), this); }
+    bdd bdd_manager::mk_or(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_or_op), this); }
+    bdd bdd_manager::mk_iff(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_iff_op), this); }
+    bdd bdd_manager::mk_exists(unsigned v, bdd const& b) { return mk_exists(1, &v, b); }
+    bdd bdd_manager::mk_forall(unsigned v, bdd const& b) { return mk_forall(1, &v, b); }
+
+
     bool bdd_manager::check_result(op_entry*& e1, op_entry const* e2, BDD a, BDD b, BDD c) {
         if (e1 != e2) {
             push_entry(e1);
@@ -203,14 +213,15 @@ namespace sat {
             return e->get_data().m_index;
         }
         e->get_data().m_refcount = 0;
-        if (m_free_nodes.empty()) {
+        bool do_gc = m_free_nodes.empty();
+        if (do_gc) {
             gc();
             e = m_node_table.insert_if_not_there2(n);
             e->get_data().m_refcount = 0;
         }
-        if (m_free_nodes.empty()) {
+        if (do_gc && m_free_nodes.size()*3 < m_nodes.size()) {
             if (m_nodes.size() > m_max_num_bdd_nodes) {
-                throw bdd_exception();
+                throw mem_out();
             }
             e->get_data().m_index = m_nodes.size();
             m_nodes.push_back(e->get_data());
@@ -228,6 +239,11 @@ namespace sat {
         // TBD
     }
 
+    void bdd_manager::sift_up(unsigned level) {
+        // exchange level and level + 1.
+        
+    }
+
     bdd bdd_manager::mk_var(unsigned i) {
         return bdd(m_var2bdd[2*i], this);        
     }
@@ -242,7 +258,7 @@ namespace sat {
             try {
                 return bdd(mk_not_rec(b.root), this);
             }
-            catch (bdd_exception) {
+            catch (mem_out) {
                 try_reorder();
                 if (!first) throw;
                 first = false;
@@ -271,7 +287,7 @@ namespace sat {
             try {
                 return bdd(mk_ite_rec(c.root, t.root, e.root), this); 
             }
-            catch (bdd_exception) {
+            catch (mem_out) {
                 try_reorder();
                 if (!first) throw;
                 first = false;
@@ -409,7 +425,7 @@ namespace sat {
     }
 
     void bdd_manager::gc() {
-        IF_VERBOSE(1, verbose_stream() << "(bdd :gc " << m_nodes.size() << ")\n";);
+        IF_VERBOSE(3, verbose_stream() << "(bdd :gc " << m_nodes.size() << ")\n";);
         SASSERT(m_free_nodes.empty());
         svector<bool> reachable(m_nodes.size(), false);
         for (unsigned i = m_bdd_stack.size(); i-- > 0; ) {
@@ -502,6 +518,7 @@ namespace sat {
 
     bdd::bdd(unsigned root, bdd_manager* m): root(root), m(m) { m->inc_ref(root); }
     bdd::bdd(bdd & other): root(other.root), m(other.m) { m->inc_ref(root); }
+    bdd::bdd(bdd && other): root(0), m(other.m) { std::swap(root, other.root); }
     bdd::~bdd() { m->dec_ref(root); }
     bdd bdd::lo() const { return bdd(m->lo(root), m); }
     bdd bdd::hi() const { return bdd(m->hi(root), m); }
@@ -514,5 +531,7 @@ namespace sat {
     bdd& bdd::operator=(bdd const& other) { unsigned r1 = root; root = other.root; m->inc_ref(root); m->dec_ref(r1); return *this; }
     std::ostream& bdd::display(std::ostream& out) const { return m->display(out, *this); }
     std::ostream& operator<<(std::ostream& out, bdd const& b) { return b.display(out); }
+    double bdd::cnf_size() const { return m->cnf_size(*this); }
+    double bdd::dnf_size() const { return m->dnf_size(*this); }
 
 }
diff --git a/src/sat/sat_bdd.h b/src/sat/sat_bdd.h
index 29d91446e..c0f1fc9b2 100644
--- a/src/sat/sat_bdd.h
+++ b/src/sat/sat_bdd.h
@@ -25,34 +25,7 @@ Revision History:
 
 namespace sat {
 
-    class bdd_manager;
-
-    class bdd {
-        friend class bdd_manager;
-        unsigned     root;
-        bdd_manager* m;
-        bdd(unsigned root, bdd_manager* m);
-    public:
-        bdd(bdd & other);
-        bdd& operator=(bdd const& other);
-        ~bdd();        
-        bdd lo() const;
-        bdd hi() const;
-        unsigned var() const;
-        bool is_true() const;
-        bool is_false() const;
-        
-        bdd operator!();
-        bdd operator&&(bdd const& other);
-        bdd operator||(bdd const& other);
-        bdd operator|=(bdd const& other) { return *this = *this || other; }
-        bdd operator&=(bdd const& other) { return *this = *this && other; }
-        std::ostream& display(std::ostream& out) const;
-        bool operator==(bdd const& other) const { return root == other.root; }
-        bool operator!=(bdd const& other) const { return root != other.root; }
-    };
-
-    std::ostream& operator<<(std::ostream& out, bdd const& b);
+    class bdd;
 
     class bdd_manager {
         friend bdd;
@@ -169,6 +142,7 @@ namespace sat {
         bool is_marked(unsigned i) { return m_mark[i] == m_mark_level; }
 
         void try_reorder();
+        void sift_up(unsigned level);
 
         static const BDD false_bdd = 0;
         static const BDD true_bdd = 1;
@@ -185,32 +159,70 @@ namespace sat {
         inline void dec_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount--; }
         inline BDD level2bdd(unsigned l) const { return m_var2bdd[m_level2var[l]]; }
 
-        struct bdd_exception {};
-    public:
-        bdd_manager(unsigned nodes, unsigned cache_size);
-        ~bdd_manager();
-        
-        bdd mk_var(unsigned i);
-        bdd mk_nvar(unsigned i);
-
-        bdd mk_true() { return bdd(true_bdd, this); }
-        bdd mk_false() { return bdd(false_bdd, this); }
-        bdd mk_not(bdd b);
-        bdd mk_exists(unsigned n, unsigned const* vars, bdd const & b);
-        bdd mk_forall(unsigned n, unsigned const* vars, bdd const & b);
-        bdd mk_exists(unsigned v, bdd const& b) { return mk_exists(1, &v, b); }
-        bdd mk_forall(unsigned v, bdd const& b) { return mk_forall(1, &v, b); }
-        bdd mk_and(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_and_op), this); }
-        bdd mk_or(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_or_op), this); }
-        bdd mk_iff(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_iff_op), this); }
-        bdd mk_ite(bdd const& c, bdd const& t, bdd const& e);
-
         double dnf_size(bdd const& b) { return count(b, 0); }
         double cnf_size(bdd const& b) { return count(b, 1); }
 
+        bdd mk_not(bdd b);
+        bdd mk_and(bdd const& a, bdd const& b);
+        bdd mk_or(bdd const& a, bdd const& b);
+
         std::ostream& display(std::ostream& out, bdd const& b);
+
+    public:
+        struct mem_out {};
+
+        bdd_manager(unsigned nodes);
+        ~bdd_manager();
+
+        void set_max_num_nodes(unsigned n) { m_max_num_bdd_nodes = n; }
+
+        bdd mk_var(unsigned i);
+        bdd mk_nvar(unsigned i);
+
+        bdd mk_true();
+        bdd mk_false();
+
+        bdd mk_exists(unsigned n, unsigned const* vars, bdd const & b);
+        bdd mk_forall(unsigned n, unsigned const* vars, bdd const & b);
+        bdd mk_exists(unsigned v, bdd const& b);
+        bdd mk_forall(unsigned v, bdd const& b);
+        bdd mk_iff(bdd const& a, bdd const& b);
+        bdd mk_ite(bdd const& c, bdd const& t, bdd const& e);
+
         std::ostream& display(std::ostream& out);
     };
+
+    class bdd {
+        friend class bdd_manager;
+        unsigned     root;
+        bdd_manager* m;
+        bdd(unsigned root, bdd_manager* m);
+    public:
+        bdd(bdd & other);
+        bdd(bdd && other);
+        bdd& operator=(bdd const& other);
+        ~bdd();        
+        bdd lo() const;
+        bdd hi() const;
+        unsigned var() const;
+        bool is_true() const;
+        bool is_false() const;
+        
+        bdd operator!();
+        bdd operator&&(bdd const& other);
+        bdd operator||(bdd const& other);
+        bdd operator|=(bdd const& other) { return *this = *this || other; }
+        bdd operator&=(bdd const& other) { return *this = *this && other; }
+        std::ostream& display(std::ostream& out) const;
+        bool operator==(bdd const& other) const { return root == other.root; }
+        bool operator!=(bdd const& other) const { return root != other.root; }
+        double cnf_size() const;
+        double dnf_size() const;
+    };
+
+    std::ostream& operator<<(std::ostream& out, bdd const& b);
+
 }
 
+
 #endif
diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp
index 764c193b3..a5ca80a32 100644
--- a/src/sat/sat_elim_vars.cpp
+++ b/src/sat/sat_elim_vars.cpp
@@ -23,9 +23,9 @@ Revision History:
 
 namespace sat{
 
-    elim_vars::elim_vars(simplifier& s) : simp(s), s(s.s), m(20,10000) {
+    elim_vars::elim_vars(simplifier& s) : simp(s), s(s.s), m(20) {
         m_mark_lim = 0;
-        m_max_literals = 13; // p.resolution_occ_cutoff();
+        m_max_literals = 11; 
     }
 
     bool elim_vars::operator()(bool_var v) {
@@ -54,7 +54,7 @@ namespace sat{
         // associate index with each variable.
         sort_marked();
         bdd b1 = elim_var(v);
-        double sz1 = m.cnf_size(b1);
+        double sz1 = b1.cnf_size();
         if (sz1 > 2*clause_size) {
             return false;
         }
@@ -63,13 +63,13 @@ namespace sat{
         }
         m_vars.reverse();
         bdd b2 = elim_var(v);
-        double sz2 = m.cnf_size(b2);
+        double sz2 = b2.cnf_size();
         if (sz2 <= clause_size) {
             return elim_var(v, b2);
         }
         shuffle_vars();
         bdd b3 = elim_var(v);
-        double sz3 = m.cnf_size(b3);
+        double sz3 = b3.cnf_size();
         if (sz3 <= clause_size) {
             return elim_var(v, b3);
         }
@@ -91,6 +91,7 @@ namespace sat{
         simp.save_clauses(mc_entry, simp.m_pos_cls);
         simp.save_clauses(mc_entry, simp.m_neg_cls);
         s.m_eliminated[v] = true;
+        ++s.m_stats.m_elim_var_bdd;
         simp.remove_bin_clauses(pos_l);
         simp.remove_bin_clauses(neg_l);
         simp.remove_clauses(pos_occs, pos_l);
@@ -152,33 +153,6 @@ namespace sat{
               tout << m.cnf_size(b) << "\n";
               );
 
-#if 0
-        TRACE("elim_vars",
-              clause_vector clauses;
-              literal_vector units;
-              get_clauses(b0, lits, clauses, units);
-              for (clause* c : clauses) 
-                  tout << *c << "\n";
-              for (literal l : units) 
-                  tout << l << "\n";              
-              for (clause* c : clauses) 
-                  s.m_cls_allocator.del_clause(c);
-              SASSERT(lits.empty());
-              clauses.reset();
-              units.reset();
-              tout << "after elim:\n";
-              get_clauses(b, lits, clauses, units);
-              for (clause* c : clauses) 
-                  tout << *c << "\n";
-              for (literal l : units) 
-                  tout << l << "\n";              
-              for (clause* c : clauses) 
-                  s.m_cls_allocator.del_clause(c);
-              SASSERT(lits.empty());
-              clauses.reset();
-              );
-#endif
-
         return b;
     }
 
@@ -194,15 +168,15 @@ namespace sat{
             
             switch (c.size()) {
             case 0:
-                UNREACHABLE();
+                s.set_conflict(justification());
                 break;
             case 1: 
                 simp.propagate_unit(c[0]);
                 break;
             case 2:
                 s.m_stats.m_mk_bin_clause++;
-                simp.add_non_learned_binary_clause(c[0],c[1]);
-                simp.back_subsumption1(c[0],c[1], false);
+                simp.add_non_learned_binary_clause(c[0], c[1]);
+                simp.back_subsumption1(c[0], c[1], false);
                 break;
             default: {
                 if (c.size() == 3)
diff --git a/src/sat/sat_elim_vars.h b/src/sat/sat_elim_vars.h
index 8f7ec1bb4..8893bbc40 100644
--- a/src/sat/sat_elim_vars.h
+++ b/src/sat/sat_elim_vars.h
@@ -27,7 +27,6 @@ namespace sat {
     class simplifier;
 
     class elim_vars {
-        friend class simplifier;
         class compare_occ;
 
         simplifier& simp;
diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp
index e9d047086..d4a994d0f 100644
--- a/src/sat/sat_model_converter.cpp
+++ b/src/sat/sat_model_converter.cpp
@@ -226,13 +226,8 @@ namespace sat {
 
     unsigned model_converter::max_var(unsigned min) const {
         unsigned result = min;
-        vector<entry>::const_iterator it = m_entries.begin();
-        vector<entry>::const_iterator end = m_entries.end();
-        for (; it != end; ++it) {
-            literal_vector::const_iterator lvit = it->m_clauses.begin();
-            literal_vector::const_iterator lvend = it->m_clauses.end();
-            for (; lvit != lvend; ++lvit) {
-                literal l = *lvit;
+        for (entry const& e : m_entries) {
+            for (literal l : e.m_clauses) {
                 if (l != null_literal) {
                     if (l.var() > result)
                         result = l.var();
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 688510153..6ad88a31b 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -330,19 +330,15 @@ namespace sat {
         cs.set_end(it2);
     }
 
-    void simplifier::mark_all_but(clause const & c, literal l) {
-        unsigned sz = c.size();
-        for (unsigned i = 0; i < sz; i++) {
-            if (c[i] == l)
-                continue;
-            mark_visited(c[i]);
-        }
+    void simplifier::mark_all_but(clause const & c, literal l1) {
+        for (literal l2 : c) 
+            if (l2 != l1)
+                mark_visited(l2);
     }
 
     void simplifier::unmark_all(clause const & c) {
-        unsigned sz = c.size();
-        for (unsigned i = 0; i < sz; i++)
-            unmark_visited(c[i]);
+        for (literal l : c)
+            unmark_visited(l);
     }
 
     /**
@@ -952,7 +948,7 @@ namespace sat {
         }
 
         bool process_var(bool_var v) {
-            return !s.s.is_assumption(v) &&  !s.was_eliminated(v);
+            return !s.s.is_assumption(v) &&  !s.was_eliminated(v) && !s.is_external(v);
         }
 
         void operator()(unsigned num_vars) {
@@ -971,6 +967,108 @@ namespace sat {
             }
         }
 
+        //
+        // Resolve intersection
+        // Find literals that are in the intersection of all resolvents with l.
+        //
+        void ri(literal l, literal_vector& inter) {
+            if (!process_var(l.var())) return;
+            bool first = true;
+            for (watched & w : s.get_wlist(~l)) {
+                if (w.is_binary_non_learned_clause()) {
+                    literal lit = w.get_literal();
+                    if (s.is_marked(~lit)) continue;
+                    if (!first) {
+                        inter.reset();
+                        return;
+                    }
+                    first = false;
+                    inter.push_back(lit);
+                }
+            }
+            clause_use_list & neg_occs = s.m_use_list.get(~l);
+            clause_use_list::iterator it = neg_occs.mk_iterator();
+            while (!it.at_end()) {
+                bool tautology = false;
+                clause & c = it.curr();
+                for (literal lit : c) {
+                    if (s.is_marked(~lit)) {
+                        tautology = true;
+                        break;
+                    }
+                }
+                if (!tautology) {
+                    if (first) {
+                        for (literal lit : c) {
+                            if (lit != ~l) inter.push_back(lit);
+                        }
+                        first = false;
+                    }
+                    else {
+                        unsigned j = 0;
+                        unsigned sz = inter.size();
+                        for (unsigned i = 0; i < sz; ++i) {
+                            literal lit1 = inter[i];
+                            for (literal lit2 : c) {
+                                if (lit1 == lit2) {
+                                    inter[j++] = lit1;
+                                    break;
+                                }
+                            }
+                        }
+                        inter.shrink(j);
+                        if (j == 0) return;
+                    }
+                }
+                it.next();
+            }
+        }
+
+        // perform covered clause elimination.
+        // first extract the covered literal addition (CLA).
+        // then check whether the CLA is blocked.
+        bool cce(clause& c, literal lit) {
+            for (literal l : c) s.mark_visited(l);
+            literal_vector added, lits;
+            for (literal l : c) added.push_back(l);
+            for (unsigned i = 0; i < added.size(); ++i) {
+                ri(added[i], lits);
+                for (literal l : lits) {
+                    if (!s.is_marked(l)) {
+                        s.mark_visited(l);
+                        added.push_back(l);
+                    }
+                }
+                lits.reset();
+            }
+            s.unmark_visited(lit);
+            bool is_tautology = (added.size() > c.size()) && all_tautology(lit);
+            for (literal l : added) s.unmark_visited(l);
+            return is_tautology;
+        }
+
+        bool cce(literal lit, literal l2) {
+            literal_vector added, lits;
+            s.mark_visited(lit);
+            s.mark_visited(l2);
+            added.push_back(lit);
+            added.push_back(l2);
+            for (unsigned i = 0; i < added.size(); ++i) {
+                ri(added[i], lits);
+                for (literal l : lits) {
+                    if (!s.is_marked(l)) {
+                        s.mark_visited(l);
+                        added.push_back(l);
+                    }
+                }
+                lits.reset();
+            }
+            s.unmark_visited(lit);
+            bool is_tautology = added.size() > 2 && all_tautology(lit);
+            for (literal l : added) s.unmark_visited(l);
+            return is_tautology;
+        }
+
         void process(literal l) {
             TRACE("blocked_clause", tout << "processing: " << l << "\n";);
             model_converter::entry * new_entry = 0;
@@ -988,21 +1086,14 @@ namespace sat {
                     SASSERT(c.contains(l));
                     s.mark_all_but(c, l);
                     if (all_tautology(l)) {
-                        TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";);
-                        if (new_entry == 0)
-                            new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var()));
-                        m_to_remove.push_back(&c);
+                        block_clause(c, l, new_entry);
                         s.m_num_blocked_clauses++;
-                        mc.insert(*new_entry, c);
-                        unsigned sz = c.size();
-                        for (unsigned i = 0; i < sz; i++) {
-                            literal lit = c[i];
-                            if (lit != l && process_var(lit.var())) {
-                                m_queue.decreased(~lit);
-                            }
-                        }
+                        s.unmark_all(c);
+                    }
+                    else if (cce(c, l)) {
+                        block_clause(c, l, new_entry);
+                        s.m_num_covered_clauses++;                        
                     }
-                    s.unmark_all(c);
                     it.next();
                 }
             }
@@ -1024,13 +1115,12 @@ namespace sat {
                     literal l2 = it->get_literal();
                     s.mark_visited(l2);
                     if (all_tautology(l)) {
-                        if (new_entry == 0)
-                            new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var()));
-                        TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l << "\n";);
-                        s.remove_bin_clause_half(l2, l, it->is_learned());
+                        block_binary(it, l, new_entry);
                         s.m_num_blocked_clauses++;
-                        m_queue.decreased(~l2);
-                        mc.insert(*new_entry, l, l2);
+                    }
+                    else if (cce(l, l2)) {
+                        block_binary(it, l, new_entry);
+                        s.m_num_covered_clauses++;
                     }
                     else {
                         *it2 = *it;
@@ -1042,6 +1132,29 @@ namespace sat {
             }
         }
 
+        void block_clause(clause& c, literal l, model_converter::entry *& new_entry) {
+            TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";);
+            if (new_entry == 0)
+                new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var()));
+            m_to_remove.push_back(&c);
+            mc.insert(*new_entry, c);
+            for (literal lit : c) {
+                if (lit != l && process_var(lit.var())) {
+                    m_queue.decreased(~lit);
+                }
+            }
+        }
+
+        void block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) {
+            if (new_entry == 0)
+                new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var()));
+            TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l << "\n";);
+            literal l2 = it->get_literal();
+            s.remove_bin_clause_half(l2, l, it->is_learned());
+            m_queue.decreased(~l2);
+            mc.insert(*new_entry, l, l2);
+        }
+
         bool all_tautology(literal l) {
             watch_list & wlist = s.get_wlist(l);
             m_counter -= wlist.size();
@@ -1083,9 +1196,11 @@ namespace sat {
         simplifier & m_simplifier;
         stopwatch    m_watch;
         unsigned     m_num_blocked_clauses;
+        unsigned     m_num_covered_clauses;
         blocked_cls_report(simplifier & s):
             m_simplifier(s),
-            m_num_blocked_clauses(s.m_num_blocked_clauses) {
+            m_num_blocked_clauses(s.m_num_blocked_clauses),
+            m_num_covered_clauses(s.m_num_covered_clauses) {
             m_watch.start();
         }
 
@@ -1094,6 +1209,8 @@ namespace sat {
             IF_VERBOSE(SAT_VB_LVL,
                        verbose_stream() << " (sat-blocked-clauses :elim-blocked-clauses "
                        << (m_simplifier.m_num_blocked_clauses - m_num_blocked_clauses)
+                       << " :elim-covered-clauses " 
+                       << (m_simplifier.m_num_covered_clauses - m_num_covered_clauses)
                        << mem_stat()
                        << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
         }
@@ -1379,6 +1496,7 @@ namespace sat {
         m_elim_counter -= num_pos * num_neg + before_lits;
 
         // eliminate variable
+        ++s.m_stats.m_elim_var_res;
         model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
         save_clauses(mc_entry, m_pos_cls);
         save_clauses(mc_entry, m_neg_cls);
@@ -1463,7 +1581,6 @@ namespace sat {
         order_vars_for_elim(vars);
         sat::elim_vars elim_bdd(*this);
 
-        std::cout << "vars to elim: " << vars.size() << "\n";
         for (bool_var v : vars) {
             checkpoint();
             if (m_elim_counter < 0) 
@@ -1471,11 +1588,9 @@ namespace sat {
             if (try_eliminate(v)) {
                 m_num_elim_vars++;
             }
-#if 1
             else if (elim_bdd(v)) {
                 m_num_elim_vars++;
             }
-#endif
         }
 
         m_pos_cls.finalize();
@@ -1512,12 +1627,13 @@ namespace sat {
         st.update("subsumed", m_num_subsumed);
         st.update("subsumption resolution", m_num_sub_res);
         st.update("elim literals", m_num_elim_lits);
-        st.update("elim bool vars", m_num_elim_vars);
         st.update("elim blocked clauses", m_num_blocked_clauses);
+        st.update("elim covered clauses", m_num_covered_clauses);
     }
 
     void simplifier::reset_statistics() {
         m_num_blocked_clauses = 0;
+        m_num_covered_clauses = 0;
         m_num_subsumed = 0;
         m_num_sub_res = 0;
         m_num_elim_lits = 0;
diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h
index 6ef0f8f18..fdfabb513 100644
--- a/src/sat/sat_simplifier.h
+++ b/src/sat/sat_simplifier.h
@@ -90,6 +90,7 @@ namespace sat {
 
         // stats
         unsigned               m_num_blocked_clauses;
+        unsigned               m_num_covered_clauses;
         unsigned               m_num_subsumed;
         unsigned               m_num_elim_vars;
         unsigned               m_num_sub_res;
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 8004c9635..ca1fc7801 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -4038,6 +4038,8 @@ namespace sat {
         st.update("dyn subsumption resolution", m_dyn_sub_res);
         st.update("blocked correction sets", m_blocked_corr_sets);
         st.update("units", m_units);
+        st.update("elim bool vars", m_elim_var_res);
+        st.update("elim bool vars bdd", m_elim_var_bdd);
     }
 
     void stats::reset() {
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 56071182b..58d2824c7 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -67,6 +67,8 @@ namespace sat {
         unsigned m_dyn_sub_res;
         unsigned m_non_learned_generation;
         unsigned m_blocked_corr_sets;
+        unsigned m_elim_var_res;
+        unsigned m_elim_var_bdd;
         unsigned m_units;
         stats() { reset(); }
         void reset();
diff --git a/src/test/bdd.cpp b/src/test/bdd.cpp
index f3f6e6b8d..6826df35e 100644
--- a/src/test/bdd.cpp
+++ b/src/test/bdd.cpp
@@ -2,7 +2,7 @@
 
 namespace sat {
     static void test1() {
-        bdd_manager m(20, 1000);
+        bdd_manager m(20);
         bdd v0 = m.mk_var(0);
         bdd v1 = m.mk_var(1);
         bdd v2 = m.mk_var(2);
@@ -10,17 +10,17 @@ namespace sat {
         bdd c2 = v2 && v0 && v1;
         std::cout << c1 << "\n";
         SASSERT(c1 == c2);
-        std::cout << "cnf size: " << m.cnf_size(c1) << "\n";
+        std::cout << "cnf size: " << c1.cnf_size() << "\n";
 
         c1 = v0 || v1 || v2;
         c2 = v2 || v1 || v0;
         std::cout << c1 << "\n";
         SASSERT(c1 == c2);
-        std::cout << "cnf size: " << m.cnf_size(c1) << "\n";
+        std::cout << "cnf size: " << c1.cnf_size() << "\n";
     }
 
     static void test2() {
-        bdd_manager m(20, 1000);
+        bdd_manager m(20);
         bdd v0 = m.mk_var(0);
         bdd v1 = m.mk_var(1);
         bdd v2 = m.mk_var(2);
@@ -35,7 +35,7 @@ namespace sat {
     }
 
     static void test3() {
-        bdd_manager m(20, 1000);
+        bdd_manager m(20);
         bdd v0 = m.mk_var(0);
         bdd v1 = m.mk_var(1);
         bdd v2 = m.mk_var(2);