working on completing ATE/ALA for acce and abce

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

src/sat/ba_solver.cpp

@@ -3282,21 +3282,26 @@ namespace sat {
     extension* ba_solver::copy(solver* s) {
         ba_solver* result = alloc(ba_solver);
         result->set_solver(s);
-        copy_core(result);
+        copy_core(result, false);
         return result;
     }
 
-    extension* ba_solver::copy(lookahead* s) {
+    extension* ba_solver::copy(lookahead* s, bool learned) {
         ba_solver* result = alloc(ba_solver);
         result->set_lookahead(s);
-        copy_core(result);
+        copy_core(result, learned);
         return result;
     }
 
-    void ba_solver::copy_core(ba_solver* result) {
+    void ba_solver::copy_core(ba_solver* result, bool learned) {
+        copy_constraints(result, m_constraints);
+        if (learned) copy_constraints(result, m_learned);
+    }
+
+    void ba_solver::copy_constraints(ba_solver* result, ptr_vector<constraint> const& constraints) {
         literal_vector lits;
         svector<wliteral> wlits;
-        for (constraint* cp : m_constraints) {
+        for (constraint* cp : constraints) {
             switch (cp->tag()) {
             case card_t: {
                 card const& c = cp->to_card();

src/sat/ba_solver.h

@@ -462,7 +462,8 @@ namespace sat {
         constraint* add_pb_ge(literal l, svector<wliteral> const& wlits, unsigned k, bool learned);
         constraint* add_xor(literal_vector const& lits, bool learned);
 
-        void copy_core(ba_solver* result);
+        void copy_core(ba_solver* result, bool learned);
+        void copy_constraints(ba_solver* result, ptr_vector<constraint> const& constraints);
     public:
         ba_solver();
         virtual ~ba_solver();
@@ -489,7 +490,7 @@ namespace sat {
         virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const;
         virtual void collect_statistics(statistics& st) const;
         virtual extension* copy(solver* s);
-        virtual extension* copy(lookahead* s);
+        virtual extension* copy(lookahead* s, bool learned);
         virtual void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes);
         virtual void pop_reinit();
         virtual void gc(); 

src/sat/sat_asymm_branch.cpp

@@ -67,22 +67,28 @@ namespace sat {
         }
     };
 
-    bool asymm_branch::process(big* big) {
+    void asymm_branch::process_bin(big& big) {
+        unsigned elim = big.reduce_tr(s);
+        m_hidden_tautologies += elim;
+    }
+
+    bool asymm_branch::process(big& big, bool learned) {
         unsigned elim0 = m_elim_literals;
         unsigned eliml0 = m_elim_learned_literals;
         for (unsigned i = 0; i < m_asymm_branch_rounds; ++i) {
-            unsigned elim = m_elim_literals;
+            unsigned elim = m_elim_literals + m_hidden_tautologies;
-            if (big) big->init_big(s, true);
+            big.init(s, learned);
-            process(big, s.m_clauses);
+            process(&big, s.m_clauses);
-            if (big) process(big, s.m_learned);
+            process(&big, s.m_learned);
+            process_bin(big);
             s.propagate(false); 
             if (s.m_inconsistent)
                 break;
-            unsigned num_elim = m_elim_literals - elim;
+            unsigned num_elim = m_elim_literals + m_hidden_tautologies - elim;
             IF_VERBOSE(1, verbose_stream() << "(sat-asymm-branch-step :elim " << num_elim << ")\n";);
             if (num_elim == 0)
                 break;
-            if (num_elim > 1000) 
+            if (num_elim > 100) 
                 i = 0;
         }        
         IF_VERBOSE(1, if (m_elim_learned_literals > eliml0) 
@@ -90,6 +96,16 @@ namespace sat {
         return m_elim_literals > elim0;
     }
 
+    bool asymm_branch::process(bool learned) {
+        unsigned eliml0 = m_elim_learned_literals;
+        unsigned elim = m_elim_literals;
+        process(nullptr, s.m_clauses);
+        s.propagate(false); 
+        IF_VERBOSE(1, if (m_elim_learned_literals > eliml0) 
+                          verbose_stream() << "(sat-asymm-branch :elim " << m_elim_learned_literals - eliml0 << ")\n";);
+        return m_elim_literals > elim;
+    }
+
 
     void asymm_branch::process(big* big, clause_vector& clauses) {
         int64 limit = -m_asymm_branch_limit;
@@ -138,10 +154,22 @@ namespace sat {
         s.propagate(false); 
         if (s.m_inconsistent)
             return;
-        report rpt(*this);
+        report rpt(*this);        
-        svector<char> saved_phase(s.m_phase);
+        
-        process(&big);
+        for (unsigned i = 0; i < m_asymm_branch_rounds; ++i) {
-        s.m_phase = saved_phase;
+            unsigned elim = m_elim_literals;
+            big.reinit();
+            process(&big, s.m_clauses);
+            process(&big, s.m_learned);
+            process_bin(big);
+            unsigned num_elim = m_elim_literals - elim;
+            IF_VERBOSE(1, verbose_stream() << "(sat-asymm-branch-step :elim " << num_elim << ")\n";);
+            if (num_elim == 0)
+                break;
+            if (num_elim > 1000)
+                i = 0;
+        }
+        s.propagate(false);       
     }
     
     void asymm_branch::operator()(bool force) {
@@ -168,12 +196,16 @@ namespace sat {
             ++counter;
             change = false;
             if (m_asymm_branch_sampled) {
-                big big;
+                big big(s.m_rand, true);
-                if (process(&big)) change = true;
+                if (process(big, true)) change = true;
+            }
+            if (m_asymm_branch_sampled) {
+                big big(s.m_rand, false);
+                if (process(big, false)) change = true;
             }
             if (m_asymm_branch) {
                 m_counter  = 0; 
-                if (process(nullptr)) change = true;
+                if (process(true)) change = true;
                 m_counter = -m_counter;
             }
         }
@@ -399,7 +431,7 @@ namespace sat {
     bool asymm_branch::process_sampled(big& big, clause & c) {
         scoped_detach scoped_d(s, c);
         sort(big, c);
-        if (c.is_learned() && uhte(big, c)) {
+        if ((c.is_learned() || !big.learned()) && uhte(big, c)) {
             ++m_hidden_tautologies;
             scoped_d.del_clause();
             return false;
@@ -408,7 +440,6 @@ namespace sat {
     }
 
     bool asymm_branch::process(clause & c) {
-        if (c.is_blocked()) return true;
         TRACE("asymm_branch_detail", tout << "processing: " << c << "\n";);
         SASSERT(s.scope_lvl() == 0);
         SASSERT(s.m_qhead == s.m_trail.size());

src/sat/sat_asymm_branch.h

@@ -66,7 +66,9 @@ namespace sat {
 
         bool re_attach(scoped_detach& scoped_d, clause& c, unsigned new_sz);
 
-        bool process(big* big);
+        bool process(bool learned);
+
+        bool process(big& big, bool learned);
 
         bool process(clause & c);
 
@@ -75,6 +77,8 @@ namespace sat {
         void process(big* big, clause_vector & c);
         
         bool process_all(clause & c);
+
+        void process_bin(big& big);
         
         bool flip_literal_at(clause const& c, unsigned flip_index, unsigned& new_sz);
         
@@ -85,7 +89,7 @@ namespace sat {
     public:
         asymm_branch(solver & s, params_ref const & p);
 
-        void operator()(bool force = false);
+        void operator()(bool force);
 
         void operator()(big& big);
 

src/sat/sat_asymm_branch_params.pyg

@@ -4,6 +4,6 @@ def_module_params(module_name='sat',
                   params=(('asymm_branch', BOOL, True, 'asymmetric branching'),
                           ('asymm_branch.rounds', UINT, 10, 'maximal number of rounds to run asymmetric branch simplifications if progress is made'),
                           ('asymm_branch.delay', UINT, 1, 'number of simplification rounds to wait until invoking asymmetric branch simplification'),
-                          ('asymm_branch.sampled', BOOL, False, 'use sampling based asymmetric branching based on binary implication graph'),
+                          ('asymm_branch.sampled', BOOL, True, 'use sampling based asymmetric branching based on binary implication graph'),
                           ('asymm_branch.limit', UINT, 100000000, 'approx. maximum number of literals visited during asymmetric branching'),
                           ('asymm_branch.all', BOOL, False, 'asymmetric branching on all literals per clause')))

src/sat/sat_big.cpp

@@ -21,10 +21,13 @@ Revision History:
 
 namespace sat {
 
-    big::big() {}
+    big::big(random_gen& rand, bool binary): 
+        m_rand(rand) {
+        m_binary = binary;
+    }
 
-    void big::init_big(solver& s, bool learned) {
+    void big::init(solver& s, bool learned) {
-        init_adding_edges(s.num_vars());
+        init_adding_edges(s.num_vars(), learned);
         unsigned num_lits = m_num_vars * 2;
         literal_vector lits;
         SASSERT(num_lits == m_dag.size() && num_lits == m_roots.size());
@@ -44,7 +47,12 @@ namespace sat {
         done_adding_edges();
     }
 
-    void big::init_adding_edges(unsigned num_vars) {
+    void big::reinit() {
+        done_adding_edges();
+    }
+
+    void big::init_adding_edges(unsigned num_vars, bool learned) {
+        m_learned = learned;
         m_num_vars = num_vars;
         unsigned num_lits = m_num_vars * 2;
         m_dag.reset();
@@ -129,9 +137,36 @@ namespace sat {
                 m_right[i] = ++dfs_num;
             }
         }
-        for (unsigned i = 0; i < num_lits; ++i) {
+        DEBUG_CODE(for (unsigned i = 0; i < num_lits; ++i) { VERIFY(m_left[i] < m_right[i]);});
-            VERIFY(m_left[i] < m_right[i]);
+    }
+
+    unsigned big::reduce_tr(solver& s) {
+        if (!m_binary && learned()) return 0;
+        unsigned num_lits = s.num_vars() * 2;
+        unsigned idx = 0;
+        unsigned elim = 0;
+        for (watch_list & wlist : s.m_watches) {
+            literal u = to_literal(idx++);
+            watch_list::iterator it     = wlist.begin();
+            watch_list::iterator itprev = it;
+            watch_list::iterator end    = wlist.end();
+            for (; it != end; ++it) {
+                watched& w = *it;
+                if (learned() ? w.is_binary_learned_clause() : w.is_binary_clause()) {
+                    literal v = w.get_literal();
+                    if (reaches(u, v) && u != get_parent(v)) {
+                        ++elim;
+                        // could turn non-learned non-binary tautology into learned binary.
+                        s.get_wlist(~v).erase(watched(~u, w.is_learned()));
+                        continue;
+                    }
+                }
+                *itprev = *it;
+                itprev++;
+            }
+            wlist.set_end(itprev);
         }
+        return elim;
     }
 
     void big::display(std::ostream& out) const {

src/sat/sat_big.h

@@ -27,32 +27,41 @@ namespace sat {
     class solver;
 
     class big {
-        random_gen             m_rand;
+        random_gen&            m_rand;
         unsigned               m_num_vars;
         vector<literal_vector> m_dag;
         svector<bool>          m_roots;
         svector<int>           m_left, m_right;
         literal_vector         m_root, m_parent;
+        bool                   m_learned;
+        bool                   m_binary;   // is the BIG produced from binary clauses or hyper-binary resolution?
 
         void init_dfs_num();
         struct pframe;
 
     public:
 
-        big();
+        big(random_gen& rand, bool binary);
         /**
            \brief initialize a BIG from a solver.
          */
-        void init_big(solver& s, bool learned);
+        void init(solver& s, bool learned);
+
+        void reinit();
 
         /**
            \brief initialize a BIG externally by adding implications.
         */
-        void init_adding_edges(unsigned num_vars);
+        void init_adding_edges(unsigned num_vars, bool learned);
         void add_edge(literal u, literal v);
         void done_adding_edges();
 
-        void ensure_big(solver& s, bool learned) { if (m_left.empty()) init_big(s, learned); }
+        void ensure_big(solver& s, bool learned) { if (m_left.empty()) init(s, learned); }
+
+        unsigned reduce_tr(solver& s);
+
+        // does it include learned binaries?
+        bool learned() const { return m_learned; }
         int get_left(literal l) const { return m_left[l.index()]; }
         int get_right(literal l) const { return m_right[l.index()]; }
         literal get_parent(literal l) const { return m_parent[l.index()]; }

src/sat/sat_clause.cpp

@@ -29,7 +29,6 @@ namespace sat {
         m_capacity(sz),
         m_removed(false),
         m_learned(learned),
-        m_blocked(false),
         m_used(false),
         m_frozen(false),
         m_reinit_stack(false),
@@ -165,7 +164,6 @@ namespace sat {
         if (c.was_removed()) out << "x";
         if (c.strengthened()) out << "+";
         if (c.is_learned()) out << "*";
-        if (c.is_blocked()) out << "b";
         return out;
     }
 

src/sat/sat_clause.h

@@ -50,7 +50,6 @@ 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
@@ -66,6 +65,7 @@ namespace sat {
         literal & operator[](unsigned idx) { SASSERT(idx < m_size); return m_lits[idx]; }
         literal const & operator[](unsigned idx) const { SASSERT(idx < m_size); return m_lits[idx]; }
         bool is_learned() const { return m_learned; }
+        void set_learned() { SASSERT(!is_learned()); m_learned = true; }
         void unset_learned() { SASSERT(is_learned()); m_learned = false; }
         void shrink(unsigned num_lits) { SASSERT(num_lits <= m_size); if (num_lits < m_size) { m_size = num_lits; mark_strengthened(); } }
         bool strengthened() const { return m_strengthened; }
@@ -92,9 +92,6 @@ 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; }
@@ -161,6 +158,16 @@ namespace sat {
     public:
         clause_wrapper(literal l1, literal l2):m_l1_idx(l1.to_uint()), m_l2_idx(l2.to_uint()) {}
         clause_wrapper(clause & c):m_cls(&c), m_l2_idx(null_literal.to_uint()) {}
+        clause_wrapper& operator=(clause_wrapper const& other) {
+            if (other.is_binary()) {
+                m_l1_idx = other.m_l1_idx;
+            }
+            else {
+                m_cls = other.m_cls;
+            }
+            m_l2_idx = other.m_l2_idx;
+            return *this;
+        }
 
         bool is_binary() const { return m_l2_idx != null_literal.to_uint(); }
         unsigned size() const { return is_binary() ? 2 : m_cls->size(); }

src/sat/sat_clause_use_list.cpp

@@ -27,11 +27,11 @@ namespace sat {
             if (!c->was_removed())
                 sz++;
         SASSERT(sz == m_size);
-        unsigned blocked = 0;
+        unsigned redundant = 0;
         for (clause* c : m_clauses) 
-            if (c->is_blocked())
+            if (c->is_learned())
-                blocked++;
+                redundant++;
-        SASSERT(blocked == m_num_blocked);
+        SASSERT(redundant == m_num_redundant);
 
         return true;
     }

src/sat/sat_clause_use_list.h

@@ -30,24 +30,24 @@ namespace sat {
     class clause_use_list {
         clause_vector   m_clauses;
         unsigned        m_size;
-        unsigned        m_num_blocked;
+        unsigned        m_num_redundant;
     public:
         clause_use_list() {
             STRACE("clause_use_list_bug", tout << "[cul_created] " << this << "\n";);
             m_size = 0; 
-            m_num_blocked = 0;
+            m_num_redundant = 0;
         }
         
         unsigned size() const { 
             return m_size; 
         }
 
-        unsigned num_blocked() const {
+        unsigned num_redundant() const {
-            return m_num_blocked;
+            return m_num_redundant;
         }
-
+        
-        unsigned non_blocked_size() const {
+        unsigned num_irredundant() const {
-            return m_size - m_num_blocked;
+            return m_size - m_num_redundant;
         }
 
         bool empty() const { return size() == 0; }
@@ -58,7 +58,7 @@ namespace sat {
             SASSERT(!c.was_removed()); 
             m_clauses.push_back(&c); 
             m_size++; 
-            if (c.is_blocked()) ++m_num_blocked;
+            if (c.is_learned()) ++m_num_redundant;
         }
 
         void erase_not_removed(clause & c) { 
@@ -67,7 +67,7 @@ namespace sat {
             SASSERT(!c.was_removed()); 
             m_clauses.erase(&c); 
             m_size--; 
-            if (c.is_blocked()) --m_num_blocked;
+            if (c.is_learned()) --m_num_redundant;
         }
 
         void erase(clause & c) { 
@@ -75,25 +75,25 @@ namespace sat {
             SASSERT(m_clauses.contains(&c)); 
             SASSERT(c.was_removed()); 
             m_size--; 
-            if (c.is_blocked()) --m_num_blocked;
+            if (c.is_learned()) --m_num_redundant;
         }
 
         void block(clause const& c) {
-            SASSERT(c.is_blocked());
+            SASSERT(c.is_learned());
-            ++m_num_blocked;
+            ++m_num_redundant;
             SASSERT(check_invariant());
         }
 
         void unblock(clause const& c) {
-            SASSERT(!c.is_blocked());
+            SASSERT(!c.is_learned());
-            --m_num_blocked;
+            --m_num_redundant;
             SASSERT(check_invariant());
         }
         
         void reset() { 
             m_clauses.finalize(); 
             m_size = 0; 
-            m_num_blocked = 0;
+            m_num_redundant = 0;
         }
         
         bool check_invariant() const;

src/sat/sat_cleaner.cpp

@@ -137,8 +137,7 @@ namespace sat {
                     SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
                     if (new_sz == 2) {
                         TRACE("cleanup_bug", tout << "clause became binary: " << c[0] << " " << c[1] << "\n";);
-                        if (!c.is_blocked()) 
+                        s.mk_bin_clause(c[0], c[1], c.is_learned());
-                            s.mk_bin_clause(c[0], c[1], c.is_learned());
                         s.del_clause(c);
                     }
                     else {

src/sat/sat_config.cpp

@@ -111,8 +111,8 @@ namespace sat {
         m_lookahead_global_autarky = p.lookahead_global_autarky();
 
         // These parameters are not exposed
-        m_simplify_mult1  = _p.get_uint("simplify_mult1", 300);
+        m_simplify_mult1  = _p.get_uint("simplify_mult1", 100);
-        m_simplify_mult2  = _p.get_double("simplify_mult2", 1.5);
+        m_simplify_mult2  = _p.get_double("simplify_mult2", 1.2);
         m_simplify_max    = _p.get_uint("simplify_max", 500000);
         // --------------------------------
 

src/sat/sat_elim_vars.cpp

@@ -43,7 +43,7 @@ namespace sat{
         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.non_blocked_size() + neg_occs.non_blocked_size();
+        unsigned clause_size = num_bin_pos + num_bin_neg + pos_occs.num_irredundant() + neg_occs.num_irredundant();
         if (clause_size == 0) {
             return false;
         }
@@ -307,13 +307,11 @@ namespace sat{
         bdd result = m.mk_true();       
         for (auto it = occs.mk_iterator(); !it.at_end(); it.next()) {
             clause const& c = it.curr();
-            if (!c.is_blocked()) {
+            bdd cl = m.mk_false();
-                bdd cl = m.mk_false();
+            for (literal l : c) {
-                for (literal l : c) {
+                cl |= mk_literal(l);
-                    cl |= mk_literal(l);
+            }           
-                }           
+            result &= cl;            
-                result &= cl;
-            }
         }
         return result;
     }

src/sat/sat_extension.h

@@ -72,7 +72,7 @@ namespace sat {
         virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const = 0;
         virtual void collect_statistics(statistics& st) const = 0;
         virtual extension* copy(solver* s) = 0;       
-        virtual extension* copy(lookahead* s) = 0;       
+        virtual extension* copy(lookahead* s, bool learned) = 0;       
         virtual void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) = 0;
         virtual void gc() = 0;
         virtual void pop_reinit() = 0;

src/sat/sat_iff3_finder.cpp

@@ -73,7 +73,7 @@ namespace sat {
        It assumes wlist have been sorted using iff3_lt
     */
     static bool contains(watch_list const & wlist, literal l1, literal l2) {
-        watched k(l1, l2);
+        watched k(l1, l2, false);
         if (wlist.size() < SMALL_WLIST)
             return wlist.contains(k);
         iff3_lt lt;

src/sat/sat_integrity_checker.cpp

@@ -28,8 +28,8 @@ namespace sat {
     }
 
     // for ternary clauses 
-    static bool contains_watched(watch_list const & wlist, literal l1, literal l2) {
+    static bool contains_watched(watch_list const & wlist, literal l1, literal l2, bool learned) {
-        return wlist.contains(watched(l1, l2));
+        return wlist.contains(watched(l1, l2, learned));
     }
     
     // for nary clauses
@@ -64,13 +64,13 @@ namespace sat {
             return true;
 
         if (c.size() == 3) {
-            CTRACE("sat_ter_watch_bug", !contains_watched(s.get_wlist(~c[0]), c[1], c[2]), tout << c << "\n";
+            CTRACE("sat_ter_watch_bug", !contains_watched(s.get_wlist(~c[0]), c[1], c[2], c.learned()), tout << c << "\n";
                    tout << "watch_list:\n";
                    sat::display_watch_list(tout, s.m_cls_allocator, s.get_wlist(~c[0]));
                    tout << "\n";);
-            VERIFY(contains_watched(s.get_wlist(~c[0]), c[1], c[2]));
+            VERIFY(contains_watched(s.get_wlist(~c[0]), c[1], c[2], c.is_learned()));
-            VERIFY(contains_watched(s.get_wlist(~c[1]), c[0], c[2]));
+            VERIFY(contains_watched(s.get_wlist(~c[1]), c[0], c[2], c.is_learned()));
-            VERIFY(contains_watched(s.get_wlist(~c[2]), c[0], c[1]));
+            VERIFY(contains_watched(s.get_wlist(~c[2]), c[0], c[1], c.is_learned()));
         }
         else {
             if (s.value(c[0]) == l_false || s.value(c[1]) == l_false) {

src/sat/sat_lookahead.cpp

@@ -989,7 +989,7 @@ namespace sat {
             m_freevars.insert(v);
     }
 
-    void lookahead::init() {
+    void lookahead::init(bool learned) {
         m_delta_trigger = 0.0;
         m_delta_decrease = 0.0;
         m_config.m_dl_success = 0.8;
@@ -1010,6 +1010,8 @@ namespace sat {
             for (auto& w : wlist) {
                 if (!w.is_binary_clause())
                     continue;
+                if (!learned && w.is_learned())
+                    continue;
                 literal l2 = w.get_literal();                    
                 if (l.index() < l2.index() && !m_s.was_eliminated(l2.var()))
                     add_binary(l, l2);
@@ -1017,7 +1019,7 @@ namespace sat {
         }
 
         copy_clauses(m_s.m_clauses, false);
-        copy_clauses(m_s.m_learned, true);
+        if (learned) copy_clauses(m_s.m_learned, true);
 
         // copy units
         unsigned trail_sz = m_s.init_trail_size();
@@ -1030,7 +1032,7 @@ namespace sat {
         }
         
         if (m_s.m_ext) {
-            m_ext = m_s.m_ext->copy(this);
+            m_ext = m_s.m_ext->copy(this, learned);
         }
         propagate();
         m_qhead = m_trail.size();
@@ -2223,7 +2225,7 @@ namespace sat {
     void lookahead::init_search() {
         m_search_mode = lookahead_mode::searching;
         scoped_level _sl(*this, c_fixed_truth);
-        init();            
+        init(true);            
     }
 
     void lookahead::checkpoint() {
@@ -2255,13 +2257,13 @@ namespace sat {
     /**
        \brief simplify set of clauses by extracting units from a lookahead at base level.
     */
-    void lookahead::simplify() {
+    void lookahead::simplify(bool learned) {
         scoped_ext _scoped_ext(*this);
         SASSERT(m_prefix == 0);
         SASSERT(m_watches.empty());
         m_search_mode = lookahead_mode::searching;
         scoped_level _sl(*this, c_fixed_truth);
-        init();                
+        init(learned);                
         if (inconsistent()) return;
         inc_istamp();            
         literal l = choose();        
@@ -2311,12 +2313,11 @@ namespace sat {
                 elim(roots, to_elim);
 
                 if (get_config().m_lookahead_simplify_asymm_branch) {
-                    big_asymm_branch();
+                    big_asymm_branch(learned);
                 }
-                if (get_config().m_lookahead_simplify_bca) {
+                if (learned && get_config().m_lookahead_simplify_bca) {
                     add_hyper_binary();
-                }
+                }                
-                
             }
         }   
         m_lookahead.reset();        
@@ -2327,11 +2328,11 @@ namespace sat {
        for strengthening clauses.
      */
 
-    void lookahead::big_asymm_branch() {
+    void lookahead::big_asymm_branch(bool learned) {
         unsigned num_lits = m_s.num_vars() * 2;
         unsigned idx = 0;
-        big big;
+        big big(m_s.m_rand, false);
-        big.init_adding_edges(m_s.num_vars());
+        big.init_adding_edges(m_s.num_vars(), learned);
         for (auto const& lits : m_binary) {
             literal u = get_parent(to_literal(idx++));
             if (u == null_literal) continue;
@@ -2370,8 +2371,8 @@ namespace sat {
             }
         }
 
-        big big;
+        big big(m_s.m_rand, false);
-        big.init_big(m_s, true);
+        big.init(m_s, true);
         svector<std::pair<literal, literal>> candidates;
 
         unsigned_vector bin_size(num_lits);
@@ -2395,7 +2396,7 @@ namespace sat {
         }
 
         for (unsigned count = 0; count < 5; ++count) {
-            big.init_big(m_s, true);
+            big.init(m_s, true);
             unsigned k = 0;
             union_find_default_ctx ufctx;
             union_find<union_find_default_ctx> uf(ufctx);
@@ -2418,7 +2419,7 @@ namespace sat {
                     }
                 }
             }
-            std::cout << candidates.size() << " -> " << k << "\n";
+            // std::cout << candidates.size() << " -> " << k << "\n";
             if (k == candidates.size()) break;
             candidates.shrink(k);
             if (k == 0) break;

src/sat/sat_lookahead.h

@@ -488,7 +488,7 @@ namespace sat {
         // initialization
         
         void init_var(bool_var v);
-        void init();
+        void init(bool learned);
         void copy_clauses(clause_vector const& clauses, bool learned);
         nary * copy_clause(clause const& c);
 
@@ -555,7 +555,7 @@ namespace sat {
 
         void add_hyper_binary();
 
-        void big_asymm_branch();
+        void big_asymm_branch(bool learned);
 
         double psat_heur();
 
@@ -600,7 +600,7 @@ namespace sat {
         /**
            \brief simplify set of clauses by extracting units from a lookahead at base level.
          */
-        void simplify();
+        void simplify(bool learned);
 
         std::ostream& display(std::ostream& out) const;
         std::ostream& display_summary(std::ostream& out) const;

src/sat/sat_params.pyg

@@ -50,8 +50,8 @@ def_module_params('sat',
                           ('lookahead_search', BOOL, False, 'use lookahead solver'),
                           ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'),
                           ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'),
-                          ('lookahead_simplify.bca', BOOL, False, 'add learned binary clauses as part of lookahead simplification'),
+                          ('lookahead_simplify.bca', BOOL, True, 'add learned binary clauses as part of lookahead simplification'),
-                          ('lookahead_simplify.asymm_branch', BOOL, False, 'apply asymmetric branch simplification with lookahead simplifier'),
+                          ('lookahead_simplify.asymm_branch', BOOL, True, 'apply asymmetric branch simplification with lookahead simplifier'),
                           ('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'),
                           ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu')))
 

src/sat/sat_scc.cpp

@@ -26,7 +26,8 @@ Revision History:
 namespace sat {
 
     scc::scc(solver & s, params_ref const & p):
-        m_solver(s) {
+        m_solver(s),
+        m_big(s.m_rand, true) {
         reset_statistics();
         updt_params(p);
     }
@@ -237,41 +238,16 @@ namespace sat {
     unsigned scc::reduce_tr(bool learned) {        
         unsigned num_lits = m_solver.num_vars() * 2;
         init_big(learned);
-        
+        unsigned num_elim = m_big.reduce_tr(m_solver);
-        unsigned idx = 0;
+        m_num_elim_bin += num_elim;
-        unsigned elim = m_num_elim_bin;
+        return num_elim;
-        for (watch_list & wlist : m_solver.m_watches) {
-            literal u = to_literal(idx++);
-            watch_list::iterator it     = wlist.begin();
-            watch_list::iterator itprev = it;
-            watch_list::iterator end    = wlist.end();
-            for (; it != end; ++it) {
-                watched& w = *it;
-                if (learned ? w.is_binary_learned_clause() : w.is_binary_clause()) {
-                    literal v = w.get_literal();
-                    if (reaches(u, v) && u != get_parent(v)) {
-                        ++m_num_elim_bin;
-                        m_solver.get_wlist(~v).erase(watched(~u, w.is_learned()));
-                    }
-                    else {
-                        *itprev = *it;
-                        itprev++;
-                    }
-                }
-                else {
-                    *itprev = *it;
-                    itprev++;
-                }
-            }
-            wlist.set_end(itprev);
-        }
-        return m_num_elim_bin - elim;
     }
 
     void scc::reduce_tr() {
         unsigned quota = 0, num_reduced = 0;
         while ((num_reduced = reduce_tr(false)) > quota) { quota = std::max(100u, num_reduced / 2); }
-        while ((num_reduced = reduce_tr(true)) > quota) { quota = std::max(100u, num_reduced / 2); }
+        quota = 0;
+        while ((num_reduced = reduce_tr(true))  > quota) { quota = std::max(100u, num_reduced / 2); }
     }
 
     void scc::collect_statistics(statistics & st) const {

src/sat/sat_scc.h

@@ -56,16 +56,12 @@ namespace sat {
         /*
           \brief create binary implication graph and associated data-structures to check transitivity.
          */
-        void init_big(bool learned) { m_big.init_big(m_solver, learned); }
+        void init_big(bool learned) { m_big.init(m_solver, learned); }
         void ensure_big(bool learned) { m_big.ensure_big(m_solver, learned); }
         int get_left(literal l) const { return m_big.get_left(l); }
         int get_right(literal l) const { return m_big.get_right(l); }
-        literal get_parent(literal l) const { return m_big.get_parent(l); }
         literal get_root(literal l) const { return m_big.get_root(l); }
-        bool reaches(literal u, literal v) const { return m_big.reaches(u, v); }        
+        bool connected(literal u, literal v) const { return m_big.connected(u, v); }
-        bool connected(literal u, literal v) const {
-            return m_big.connected(u, v); 
-        }
     };
 };
 

src/sat/sat_scc_params.pyg

@@ -2,5 +2,5 @@ def_module_params(module_name='sat',
                   class_name='sat_scc_params',
                   export=True,
                   params=(('scc', BOOL, True, 'eliminate Boolean variables by computing strongly connected components'),
-                          ('scc.tr', BOOL, False, 'apply transitive reduction, eliminate redundant binary clauses'), ))
+                          ('scc.tr', BOOL, True, 'apply transitive reduction, eliminate redundant binary clauses'), ))
 

src/sat/sat_simplifier.cpp

@@ -150,7 +150,8 @@ namespace sat {
 
     inline void simplifier::block_clause(clause & c) {
         if (m_retain_blocked_clauses) {
-            c.block();
+            m_need_cleanup = true;
+            c.set_learned();
             m_use_list.block(c);
         }
         else {
@@ -160,7 +161,7 @@ namespace sat {
     }
 
     inline void simplifier::unblock_clause(clause & c) {
-        c.unblock();
+        c.unset_learned();
         m_use_list.unblock(c);
     }
 
@@ -231,7 +232,6 @@ namespace sat {
         if (bce_enabled() || abce_enabled() || bca_enabled()) {
             elim_blocked_clauses();
         }
-        if (!m_need_cleanup) si.check_watches();
 
         if (!learned) {
             m_num_calls++;
@@ -265,6 +265,8 @@ namespace sat {
         if (m_need_cleanup || vars_eliminated) {
             TRACE("after_simplifier", tout << "cleanning watches...\n";);
             cleanup_watches();
+            move_clauses(s.m_learned, true);
+            move_clauses(s.m_clauses, false);
             cleanup_clauses(s.m_learned, true, vars_eliminated,  m_learned_in_use_lists);
             cleanup_clauses(s.m_clauses, false, vars_eliminated, true);
         }
@@ -302,6 +304,26 @@ namespace sat {
         }
     }
 
+    void simplifier::move_clauses(clause_vector& cs, bool learned) {
+        clause_vector::iterator it  = cs.begin();
+        clause_vector::iterator it2 = it;
+        clause_vector::iterator end = cs.end();
+        for (; it != end; ++it) {
+            clause & c = *(*it);
+            if (learned && !c.is_learned()) {
+                s.m_clauses.push_back(&c);
+            }
+            else if (!learned && c.is_learned()) {
+                s.m_learned.push_back(&c);
+            }
+            else {
+                *it2 = *it;
+                ++it2;
+            }
+        }
+        cs.set_end(it2);
+    }
+
     void simplifier::cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists) {
         TRACE("sat", tout << "cleanup_clauses\n";);
         clause_vector::iterator it  = cs.begin();
@@ -309,6 +331,7 @@ namespace sat {
         clause_vector::iterator end = cs.end();
         for (; it != end; ++it) {
             clause & c = *(*it);
+            VERIFY(learned == c.is_learned());
             if (c.was_removed()) {
                 s.del_clause(c);
                 continue;
@@ -350,10 +373,10 @@ namespace sat {
                 s.del_clause(c);
                 continue;
             }
-            // clause became a problem clause
+            // clause became a learned clause
-            if (learned && !c.is_learned()) {
+            if (!learned && c.is_learned()) {
                 SASSERT(!c.frozen());
-                s.m_clauses.push_back(&c);
+                s.m_learned.push_back(&c);
                 continue;
             }
             *it2 = *it;
@@ -433,7 +456,6 @@ 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);
         for (auto it = cs.mk_iterator(); !it.at_end(); it.next()) {
             clause & c2 = it.curr();
@@ -474,17 +496,15 @@ namespace sat {
         literal_vector::iterator l_it = m_bs_ls.begin();
         for (; it != end; ++it, ++l_it) {
             clause & c2 = *(*it);
-            if (!c2.was_removed() && !c1.is_blocked() && *l_it == null_literal) {
+            if (!c2.was_removed() && *l_it == null_literal) {
                 // 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() && !c1.is_blocked()) {
+            else if (!c2.was_removed()) {
                 // subsumption resolution
                 TRACE("subsumption_resolution", tout << c1 << " sub-ref(" << *l_it << ") " << c2 << "\n";);
                 elim_lit(c2, *l_it);
@@ -544,7 +564,6 @@ 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();
         for (; !it.at_end(); it.next()) {
@@ -955,16 +974,19 @@ namespace sat {
         literal_vector m_covered_clause;
         literal_vector m_intersection;
         literal_vector m_new_intersection;
+        literal_vector m_blocked_binary;
         svector<bool>  m_in_intersection;
         sat::model_converter::elim_stackv m_elim_stack;
         unsigned       m_ala_qhead;
+        clause_wrapper m_clause;
 
         blocked_clause_elim(simplifier & _s, unsigned limit, model_converter & _mc, use_list & l,
                             vector<watch_list> & wlist):
             s(_s),
             m_counter(limit),
             mc(_mc),
-            m_queue(l, wlist) {
+            m_queue(l, wlist),
+            m_clause(null_literal, null_literal) {
             m_in_intersection.resize(s.s.num_vars() * 2, false);
         }
 
@@ -977,25 +999,34 @@ namespace sat {
             return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v);
         }
 
+        enum elim_type {
+            cce_t,
+            acce_t,
+            abce_t
+        };
+
+        enum verdict_type {
+            at_t,    // asymmetric tautology
+            bc_t,    // blocked clause
+            no_t     // neither
+        };
+
         void operator()() {
-            integrity_checker si(s.s);
-            //si.check_watches();
             if (s.bce_enabled()) {
                 block_clauses();
             }
-            //si.check_watches();
             if (s.abce_enabled()) {
-                cce<false>();
+                cce<abce_t>();
             }
-            //si.check_watches();
             if (s.cce_enabled()) {
-                cce<true>();
+                cce<cce_t>();
+            }
+            if (s.acce_enabled()) {
+                cce<acce_t>();
             }
-            //si.check_watches();
             if (s.bca_enabled()) {
                 bca();
             }
-            //si.check_watches();
         }
 
         void block_clauses() {
@@ -1022,13 +1053,12 @@ namespace sat {
                 return;
             }
             integrity_checker si(s.s);
-            //si.check_watches();
             process_clauses(l);
             process_binary(l);
-            //si.check_watches();
+        }        
-        }
 
         void process_binary(literal l) {
+            m_blocked_binary.reset();
             model_converter::entry* new_entry = 0;
             watch_list & wlist = s.get_wlist(~l);
             m_counter -= wlist.size();
@@ -1046,6 +1076,7 @@ namespace sat {
                 if (all_tautology(l)) {
                     block_binary(it, l, new_entry);
                     s.m_num_blocked_clauses++;
+                    m_blocked_binary.push_back(l2);
                 }
                 else {
                     *it2 = *it; it2++;
@@ -1053,6 +1084,12 @@ namespace sat {
                 s.unmark_visited(l2);
             }
             wlist.set_end(it2);
+            if (s.m_retain_blocked_clauses && !m_blocked_binary.empty()) {
+                IF_VERBOSE(0, verbose_stream() << "retaining " << m_blocked_binary.size() << " binary clauses\n";);
+                for (literal lit2 : m_blocked_binary) {
+                    s.s.mk_bin_clause(l, lit2, true);
+                }
+            }
         }
 
         void process_clauses(literal l) {
@@ -1062,7 +1099,7 @@ namespace sat {
             clause_use_list::iterator it = occs.mk_iterator();
             for (; !it.at_end(); it.next()) {
                 clause & c = it.curr();
-                if (c.is_blocked()) continue;
+                if (c.is_learned()) continue;
                 m_counter -= c.size();
                 SASSERT(c.contains(l));
                 s.mark_all_but(c, l);
@@ -1118,7 +1155,7 @@ namespace sat {
             for (auto it = neg_occs.mk_iterator(); !it.at_end(); it.next()) {
                 bool tautology = false;
                 clause & c = it.curr();
-                if (c.is_blocked() && !adding) continue;
+                if (c.is_learned() && !adding) continue;
                 for (literal lit : c) {
                     if (s.is_marked(~lit) && lit != ~l) {
                         tautology = true;
@@ -1159,7 +1196,7 @@ namespace sat {
             clause_use_list & neg_occs = s.m_use_list.get(~l);
             for (auto it = neg_occs.mk_iterator(); !it.at_end(); it.next()) {
                 clause & c = it.curr();
-                if (c.is_blocked()) continue;
+                if (c.is_learned()) continue;
                 bool tautology = false;
                 for (literal lit : c) {
                     if (s.is_marked(~lit) && lit != ~l) {
@@ -1172,24 +1209,107 @@ namespace sat {
             return true;
         }
 
+        bool revisit_binary(literal l1, literal l2) const {
+            return m_clause.is_binary() && 
+                ((m_clause[0] == l1 && m_clause[1] == l2) ||
+                 (m_clause[0] == l2 && m_clause[1] == l1));
+        }
+
+        bool revisit_ternary(literal l1, literal l2, literal l3) const {
+            return m_clause.size() == 3 && 
+                ((m_clause[0] == l1 && m_clause[1] == l2 && m_clause[2] == l3) ||
+                 (m_clause[0] == l2 && m_clause[1] == l1 && m_clause[2] == l3) ||
+                 (m_clause[0] == l2 && m_clause[1] == l3 && m_clause[2] == l1) ||
+                 (m_clause[0] == l1 && m_clause[1] == l3 && m_clause[2] == l2) ||
+                 (m_clause[0] == l3 && m_clause[1] == l1 && m_clause[2] == l2) ||
+                 (m_clause[0] == l3 && m_clause[1] == l2 && m_clause[2] == l1));
+        }
+
+        bool revisit_clause(clause const& c) const {
+            return !m_clause.is_binary() && (m_clause.get_clause() == &c);
+        }
+
         /*
          * C \/ l     l \/ lit
          * -------------------
          *    C \/ l \/ ~lit
+         *
+         * C \/ lit \/ l   l \/ lit
+         * ------------------------
+         *        l \/ lit              C \/ lit \/ l can be removed
+         *
+         * C \/ l1 \/ ... \/ lk     l1 \/ ... \/ lk \/ lit
+         * -----------------------------------------------
+         *      C \/ l1 \/ ... \/ lk \/ ~lit
+         * unless C contains lit, and it is a tautology.
          */
-        void add_ala() {
+        bool add_ala() {
             for (; m_ala_qhead < m_covered_clause.size(); ++m_ala_qhead) {
                 literal l = m_covered_clause[m_ala_qhead];
                 for (watched & w : s.get_wlist(~l)) {
                     if (w.is_binary_non_learned_clause()) {
                         literal lit = w.get_literal();
-                        if (!s.is_marked(lit) && !s.is_marked(~lit)) {
+                        if (revisit_binary(l, lit)) continue;
+                        if (s.is_marked(lit)) {
+                            IF_VERBOSE(0, verbose_stream() << "ATE: " << m_covered_clause << " binary: " << l << " " << lit << "\n";);
+                            return true;
+                        }
+                        if (!s.is_marked(~lit)) {
+                            IF_VERBOSE(0, verbose_stream() << "ALA: " << m_covered_clause << " binary " << l << " " << lit << " " << (~lit) << "\n";);
                             m_covered_clause.push_back(~lit);
                             s.mark_visited(~lit);
                         }
                     }
+                    else if (w.is_ternary_clause() && !w.is_learned()) {
+                        literal lit1 = w.get_literal1();
+                        literal lit2 = w.get_literal2();
+                        if (revisit_ternary(l, lit1, lit2)) continue;
+                        if (s.is_marked(lit1) && s.is_marked(lit2)) {
+                            IF_VERBOSE(0, verbose_stream() << "ATE: " << m_covered_clause << " ternary: " << l << " " << lit1 << " " << lit2 << "\n";);
+                            return true;
+                        }
+                        if (s.is_marked(lit1) && !s.is_marked(~lit2)) {
+                            IF_VERBOSE(0, verbose_stream() << "ALA: " << m_covered_clause << " ternary " << l << " " << lit1 << " " << lit2 << " " << (~lit2) << "\n";);
+                            m_covered_clause.push_back(~lit2);
+                            s.mark_visited(~lit2);
+                            continue;
+                        }
+                        if (s.is_marked(lit2) && !s.is_marked(~lit1)) {
+                            IF_VERBOSE(0, verbose_stream() << "ALA: " << m_covered_clause << " ternay " << l << " " << lit1 << " " << lit2 << " " << (~lit1) << "\n";);
+                            m_covered_clause.push_back(~lit1);
+                            s.mark_visited(~lit1);
+                            continue;
+                        }
+                    }
+                    else if (w.is_clause()) {
+                        clause & c = s.s.get_clause(w.get_clause_offset());
+                        if (c.is_learned()) continue;
+                        if (revisit_clause(c)) continue;
+                        literal lit1 = null_literal;
+                        bool ok = true;
+                        for (literal lit : c) {
+                            if (lit == l) continue;
+                            if (s.is_marked(lit)) continue;
+                            if (!s.is_marked(~lit) && lit1 == null_literal) {
+                                lit1 = lit;
+                            }
+                            else {
+                                ok = false;
+                                break;
+                            }
+                        }
+                        if (!ok) continue;
+                        if (lit1 == null_literal) {
+                            IF_VERBOSE(0, verbose_stream() << "ATE: " << m_covered_clause << " clause " << c << "\n";);
+                            return true;
+                        }
+                        IF_VERBOSE(0, verbose_stream() << "ALA: " << m_covered_clause << " clause " << c << " " << (~lit1) << "\n";);
+                        m_covered_clause.push_back(~lit1);
+                        s.mark_visited(~lit1);
+                    }
                 }
             }
+            return false;
         }
 
 
@@ -1220,11 +1340,12 @@ namespace sat {
         }
 
         bool above_threshold(unsigned sz0) const {
-            return sz0 * 10 < m_covered_clause.size();
+            if (sz0 * 400 < m_covered_clause.size()) IF_VERBOSE(0, verbose_stream() << "above threshold " << sz0 << " " << m_covered_clause.size() << "\n";);
+            return sz0 * 400 < m_covered_clause.size();
         }
 
-        template<bool use_ri>
+        template<elim_type et>
-        bool cla(literal& blocked, model_converter::kind& k) {
+        verdict_type cla(literal& blocked, model_converter::kind& k) {
             bool is_tautology = false;
             for (literal l : m_covered_clause) s.mark_visited(l);
             unsigned num_iterations = 0, sz;
@@ -1240,9 +1361,9 @@ namespace sat {
              * So we record sz0, the original set of literals in the clause, mark additional literals, 
              * and then check if any of the first sz0 literals are blocked.
              */
-            if (s.abce_enabled() && !use_ri) {
+            if (et == abce_t) {
-                add_ala();               
+                if (add_ala()) return at_t;               
-                for (unsigned i = 0; i < sz0; ++i) {
+                for (unsigned i = 0; !is_tautology && i < sz0; ++i) {
                     if (check_abce_tautology(m_covered_clause[i])) {
                         blocked = m_covered_clause[i];
                         is_tautology = true;
@@ -1252,7 +1373,7 @@ namespace sat {
                 k = model_converter::BLOCK_LIT; // actually ABCE
                 for (literal l : m_covered_clause) s.unmark_visited(l);
                 m_covered_clause.shrink(sz0);
-                return is_tautology;
+                return is_tautology ? bc_t : no_t;
             }
 
             /*
@@ -1268,53 +1389,56 @@ namespace sat {
                 }
                 while (m_covered_clause.size() > sz && !is_tautology);
                 if (above_threshold(sz0)) break;
-                if (s.acce_enabled() && !is_tautology) {
+                if (et == acce_t && !is_tautology) {
                     sz = m_covered_clause.size();
-                    add_ala();
+                    if (add_ala()) return at_t;
                     k = model_converter::ACCE;
                 }
             }
             while (m_covered_clause.size() > sz && !is_tautology);
             // if (is_tautology) std::cout << num_iterations << " " << m_covered_clause.size() << " " << sz0 << " " << is_tautology << " " << m_elim_stack.size() << "\n";
             for (literal l : m_covered_clause) s.unmark_visited(l);
-            return is_tautology && !above_threshold(sz0);
+            return (is_tautology && !above_threshold(sz0)) ? bc_t : no_t;
         }
 
         // perform covered clause elimination.
         // first extract the covered literal addition (CLA).
         // then check whether the CLA is blocked.
-        template<bool use_ri>
+        template<elim_type et>
-        bool cce(clause& c, literal& blocked, model_converter::kind& k) {
+        verdict_type cce(clause& c, literal& blocked, model_converter::kind& k) {
+            m_clause = clause_wrapper(c);
             m_covered_clause.reset();
             for (literal l : c) m_covered_clause.push_back(l);
-            return cla<use_ri>(blocked, k);
+            return cla<et>(blocked, k);
         }
 
-        template<bool use_ri>
+        template<elim_type et>
-        bool cce(literal l1, literal l2, literal& blocked, model_converter::kind& k) {
+        verdict_type cce(literal l1, literal l2, literal& blocked, model_converter::kind& k) {
+            m_clause = clause_wrapper(l1, l2);
             m_covered_clause.reset();
             m_covered_clause.push_back(l1);
             m_covered_clause.push_back(l2);
-            return cla<use_ri>(blocked, k);            
+            return cla<et>(blocked, k);            
         }
         
-        template<bool use_ri>
+        template<elim_type et>
         void cce() {
             insert_queue();
-            cce_clauses<use_ri>();
+            cce_clauses<et>();
-            cce_binary<use_ri>();
+            cce_binary<et>();
         }
 
-        template<bool use_ri>
+        template<elim_type et>
         void cce_binary() {
             while (!m_queue.empty() && m_counter >= 0) {
                 s.checkpoint();
-                process_cce_binary<use_ri>(m_queue.next());
+                process_cce_binary<et>(m_queue.next());
             }
         }
 
-        template<bool use_ri>
+        template<elim_type et>
         void process_cce_binary(literal l) {
+            m_blocked_binary.reset();
             literal blocked = null_literal;
             watch_list & wlist = s.get_wlist(~l);
             m_counter -= wlist.size();
@@ -1329,29 +1453,51 @@ namespace sat {
                     continue;
                 }
                 literal l2 = it->get_literal();
-                if (cce<use_ri>(l, l2, blocked, k)) {
+                switch (cce<et>(l, l2, blocked, k)) {
+                case bc_t:
                     block_covered_binary(it, l, blocked, k);
                     s.m_num_covered_clauses++;
-                }
+                    m_blocked_binary.push_back(l2);
-                else {
+                    break;
+                case at_t:
+                    s.m_num_ate++;
+                    m_blocked_binary.push_back(l2);
+                    break;
+                case no_t:
                     *it2 = *it; 
                     it2++;
+                    break;
                 }
             }
             wlist.set_end(it2);
+            if (s.m_retain_blocked_clauses && !m_blocked_binary.empty()) {
+                IF_VERBOSE(0, verbose_stream() << "retaining " << m_blocked_binary.size() << " binary clauses\n";);
+                for (literal lit2 : m_blocked_binary) {
+                    s.s.mk_bin_clause(l, lit2, true);
+                }
+            }
         }
 
 
-        template<bool use_ri>
+        template<elim_type et>
         void cce_clauses() {
             m_to_remove.reset();
             literal blocked;
             model_converter::kind k;
             for (clause* cp : s.s.m_clauses) {
                 clause& c = *cp;
-                if (!c.was_removed() && !c.is_blocked() && cce<use_ri>(c, blocked, k)) {
+                if (!c.was_removed() && !c.is_learned()) {
-                    block_covered_clause(c, blocked, k);
+                    switch (cce<et>(c, blocked, k)) {
-                    s.m_num_covered_clauses++;                    
+                    case bc_t:
+                        block_covered_clause(c, blocked, k);
+                        s.m_num_covered_clauses++;          
+                        break;
+                    case at_t:
+                        m_to_remove.push_back(&c);
+                        break;
+                    case no_t:
+                        break;
+                    }
                 }
             }
             for (clause* c : m_to_remove) {
@@ -1456,7 +1602,7 @@ namespace sat {
             clause_use_list::iterator it = neg_occs.mk_iterator();
             for (; !it.at_end(); it.next()) {
                 clause & c = it.curr();
-                if (c.is_blocked()) continue;
+                if (c.is_learned()) continue;
                 m_counter -= c.size();
                 unsigned sz = c.size();
                 unsigned i;
@@ -1485,11 +1631,13 @@ namespace sat {
         stopwatch    m_watch;
         unsigned     m_num_blocked_clauses;
         unsigned     m_num_covered_clauses;
+        unsigned     m_num_ate;
         unsigned     m_num_added_clauses;
         blocked_cls_report(simplifier & s):
             m_simplifier(s),
             m_num_blocked_clauses(s.m_num_blocked_clauses),
             m_num_covered_clauses(s.m_num_covered_clauses),
+            m_num_ate(s.m_num_ate),
             m_num_added_clauses(s.m_num_bca) {
             m_watch.start();
         }
@@ -1503,6 +1651,8 @@ namespace sat {
                        << (m_simplifier.m_num_covered_clauses - m_num_covered_clauses)
                        << " :added-clauses "
                        << (m_simplifier.m_num_bca - m_num_added_clauses)
+                       << " :ate "
+                       << (m_simplifier.m_num_ate - m_num_ate) 
                        << mem_stat()
                        << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
         }
@@ -1571,7 +1721,7 @@ namespace sat {
     void simplifier::collect_clauses(literal l, clause_wrapper_vector & r) {
         clause_use_list const & cs = m_use_list.get(l);
         for (auto it = cs.mk_iterator(); !it.at_end(); it.next()) {
-            if (!it.curr().is_blocked()) {
+            if (!it.curr().is_learned()) {
                 r.push_back(clause_wrapper(it.curr()));
                 SASSERT(r.back().size() == it.curr().size());
             }
@@ -1715,8 +1865,8 @@ namespace sat {
         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.non_blocked_size() + num_bin_pos;
+        unsigned num_pos = pos_occs.num_irredundant() + num_bin_pos;
-        unsigned num_neg = neg_occs.non_blocked_size() + num_bin_neg;
+        unsigned num_neg = neg_occs.num_irredundant() + num_bin_neg;
 
         TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << "\n";);
 
@@ -1726,12 +1876,12 @@ namespace sat {
         unsigned before_lits = num_bin_pos*2 + num_bin_neg*2;
 
         for (auto it = pos_occs.mk_iterator(); !it.at_end(); it.next()) {
-            if (!it.curr().is_blocked())
+            if (!it.curr().is_learned())
                 before_lits += it.curr().size();
         }
 
         for (auto it = neg_occs.mk_iterator(); !it.at_end(); it.next()) {
-            if (!it.curr().is_blocked())
+            if (!it.curr().is_learned())
                 before_lits += it.curr().size();
         }
 
@@ -1847,7 +1997,7 @@ namespace sat {
         ~elim_var_report() {
             m_watch.stop();
             IF_VERBOSE(SAT_VB_LVL,
-                       verbose_stream() << " (sat-resolution :elim-bool-vars "
+                       verbose_stream() << " (sat-resolution :elim-vars "
                        << (m_simplifier.m_num_elim_vars - m_num_elim_vars)
                        << " :threshold " << m_simplifier.m_elim_counter
                        << mem_stat()
@@ -1921,6 +2071,7 @@ namespace sat {
         st.update("elim blocked clauses", m_num_blocked_clauses);
         st.update("elim covered clauses", m_num_covered_clauses);
         st.update("blocked clauses added", m_num_bca);
+        st.update("asymmetric tautologies eliminated", m_num_ate);
     }
 
     void simplifier::reset_statistics() {
@@ -1931,5 +2082,6 @@ namespace sat {
         m_num_elim_lits = 0;
         m_num_elim_vars = 0;
         m_num_bca = 0;
+        m_num_ate = 0;
     }
 };

src/sat/sat_simplifier.h

@@ -107,6 +107,7 @@ namespace sat {
         unsigned               m_num_sub_res;
         unsigned               m_num_elim_lits;
         unsigned               m_num_bca;
+        unsigned               m_num_ate;
 
         bool                   m_learned_in_use_lists;
         unsigned               m_old_num_elim_vars;
@@ -159,6 +160,7 @@ namespace sat {
         void mark_as_not_learned(literal l1, literal l2);
 
         void cleanup_watches();
+        void move_clauses(clause_vector & cs, bool learned);
         void cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists);
 
         bool is_external(bool_var v) const;

src/sat/sat_simplifier_params.pyg

@@ -8,7 +8,7 @@ def_module_params(module_name='sat',
                           ('elim_blocked_clauses_at', UINT, 2, 'eliminate blocked clauses only once at the given simplification round'),
                           ('bca', BOOL, False, 'blocked clause addition - add blocked binary clauses'),
 	                  ('bce_delay', UINT, 0, 'delay eliminate blocked clauses until simplification round'),
-                          ('retain_blocked_clauses', BOOL, False, 'retain blocked clauses for propagation, hide them from variable elimination'),
+                          ('retain_blocked_clauses', BOOL, True, 'retain blocked clauses as lemmas'),
                           ('blocked_clause_limit', UINT, 100000000, 'maximum number of literals visited during blocked clause elimination'),
                           ('override_incremental', BOOL, False, 'override incemental safety gaps. Enable elimination of blocked clauses and variables even if solver is reused'),
                           ('resolution.limit', UINT, 500000000, 'approx. maximum number of literals visited during variable elimination'),

src/sat/sat_solver.cpp

@@ -173,11 +173,9 @@ namespace sat {
             for (clause* c : src.m_clauses) {
                 buffer.reset();
                 for (literal l : *c) buffer.push_back(l);
-                clause* c1 = mk_clause_core(buffer);
+                mk_clause_core(buffer);
-                if (c1 && c->is_blocked()) {
-                    c1->block();
-                }
             }
+
             // copy high quality lemmas
             unsigned num_learned = 0;
             for (clause* c : src.m_learned) {
@@ -398,9 +396,9 @@ namespace sat {
 
     bool solver::attach_ter_clause(clause & c) {
         bool reinit = false;
-        m_watches[(~c[0]).index()].push_back(watched(c[1], c[2]));
+        m_watches[(~c[0]).index()].push_back(watched(c[1], c[2], c.is_learned()));
-        m_watches[(~c[1]).index()].push_back(watched(c[0], c[2]));
+        m_watches[(~c[1]).index()].push_back(watched(c[0], c[2], c.is_learned()));
-        m_watches[(~c[2]).index()].push_back(watched(c[0], c[1]));
+        m_watches[(~c[2]).index()].push_back(watched(c[0], c[1], c.is_learned()));
         if (!at_base_lvl()) {
             if (value(c[1]) == l_false && value(c[2]) == l_false) {
                 m_stats.m_ter_propagate++;
@@ -1508,6 +1506,7 @@ namespace sat {
         CASSERT("sat_simplify_bug", check_invariant());
         si.check_watches();
         
+
         m_simplifier(false);
         CASSERT("sat_simplify_bug", check_invariant());
         CASSERT("sat_missed_prop", check_missed_propagation());
@@ -1517,11 +1516,6 @@ namespace sat {
             CASSERT("sat_missed_prop", check_missed_propagation());
             CASSERT("sat_simplify_bug", check_invariant());
         }
-        if (m_config.m_lookahead_simplify) {
-            lookahead lh(*this);
-            lh.simplify();
-            lh.collect_statistics(m_aux_stats);
-        }
         sort_watch_lits();
         CASSERT("sat_simplify_bug", check_invariant());
 
@@ -1529,7 +1523,7 @@ namespace sat {
         CASSERT("sat_missed_prop", check_missed_propagation());
         CASSERT("sat_simplify_bug", check_invariant());
 
-        m_asymm_branch();
+        m_asymm_branch(false);
         CASSERT("sat_missed_prop", check_missed_propagation());
         CASSERT("sat_simplify_bug", check_invariant());
 
@@ -1538,6 +1532,17 @@ namespace sat {
             m_ext->simplify();
         }
 
+        if (m_config.m_lookahead_simplify) {
+            lookahead lh(*this);
+            lh.simplify(true);
+            lh.collect_statistics(m_aux_stats);
+        }
+        if (false && m_config.m_lookahead_simplify) {
+            lookahead lh(*this);
+            lh.simplify(false);
+            lh.collect_statistics(m_aux_stats);
+        }
+
         TRACE("sat", display(tout << "consistent: " << (!inconsistent()) << "\n"););
 
         reinit_assumptions();
@@ -1639,7 +1644,7 @@ namespace sat {
         bool ok = true;
         for (clause const* cp : m_clauses) {
             clause const & c = *cp;
-            if (!c.satisfied_by(m) && !c.is_blocked()) {
+            if (!c.satisfied_by(m)) {
                 IF_VERBOSE(0, verbose_stream() << "failed clause " << c.id() << ": " << c << "\n";);
                 TRACE("sat", tout << "failed: " << c << "\n";
                       tout << "assumptions: " << m_assumptions << "\n";
@@ -3282,6 +3287,19 @@ namespace sat {
         return num_cls + m_clauses.size() + m_learned.size();
     }
 
+    void solver::num_binary(unsigned& given, unsigned& learned) const {
+        given = learned = 0;
+        unsigned l_idx = 0;
+        for (auto const& wl : m_watches) {
+            literal l = ~to_literal(l_idx++);
+            for (auto const& w : wl) {
+                if (w.is_binary_clause() && l.index() < w.get_literal().index()) {
+                    if (w.is_learned()) ++learned; else ++given;
+                }
+            }
+        }
+    }
+
     void solver::display_dimacs(std::ostream & out) const {
         out << "p cnf " << num_vars() << " " << num_clauses() << "\n";
         for (literal lit : m_trail) {
@@ -4054,10 +4072,12 @@ namespace sat {
     }
 
     void mk_stat::display(std::ostream & out) const {
+        unsigned given, learned;
+        m_solver.num_binary(given, learned);
         if (!m_solver.m_clauses.empty())
-            out << " :clauses " << m_solver.m_clauses.size();
+            out << " :clauses " << m_solver.m_clauses.size() + given << "/" << given;
         if (!m_solver.m_learned.empty()) {
-            out << " :learned " << (m_solver.m_learned.size() - m_solver.m_num_frozen);
+            out << " :learned " << (m_solver.m_learned.size() + learned - m_solver.m_num_frozen) << "/" << learned;
             if (m_solver.m_num_frozen > 0)
                 out << " :frozen " << m_solver.m_num_frozen;
         }

src/sat/sat_solver.h

@@ -263,6 +263,7 @@ namespace sat {
         bool inconsistent() const { return m_inconsistent; }
         unsigned num_vars() const { return m_level.size(); }
         unsigned num_clauses() const;
+        void num_binary(unsigned& given, unsigned& learned) const;
         unsigned num_restarts() const { return m_restarts; }
         bool is_external(bool_var v) const { return m_external[v] != 0; }
         bool is_external(literal l) const { return is_external(l.var()); }

src/sat/sat_watched.h

@@ -53,15 +53,16 @@ namespace sat {
             SASSERT(learned || is_binary_non_learned_clause());
         }
 
-        watched(literal l1, literal l2) {
+        watched(literal l1, literal l2, bool learned) {
             SASSERT(l1 != l2);
             if (l1.index() > l2.index())
                 std::swap(l1, l2);
             m_val1 = l1.to_uint();
-            m_val2 = static_cast<unsigned>(TERNARY) + (l2.to_uint() << 2);
+            m_val2 = static_cast<unsigned>(TERNARY) + (static_cast<unsigned>(learned) << 2) + (l2.to_uint() << 3);
             SASSERT(is_ternary_clause());
             SASSERT(get_literal1() == l1);
             SASSERT(get_literal2() == l2);
+            SASSERT(is_learned() == learned);
         }
 
         unsigned val2() const { return m_val2; }
@@ -91,12 +92,12 @@ namespace sat {
         bool is_binary_learned_clause() const { return is_binary_clause() && is_learned(); }
         bool is_binary_non_learned_clause() const { return is_binary_clause() && !is_learned(); }
 
-        void set_not_learned() { SASSERT(is_learned()); m_val2 = static_cast<unsigned>(BINARY); SASSERT(!is_learned()); }
+        void set_not_learned() { SASSERT(is_learned()); m_val2 &= 0x3; SASSERT(!is_learned()); }
-        void set_learned() { SASSERT(!is_learned()); m_val2 = static_cast<unsigned>(BINARY) + (1u << 2); SASSERT(is_learned()); }
+        void set_learned() { SASSERT(!is_learned()); m_val2 |= 0x4; SASSERT(is_learned()); }
                 
         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)); }
-        literal get_literal2() const { SASSERT(is_ternary_clause()); return to_literal(m_val2 >> 2); }
+        literal get_literal2() const { SASSERT(is_ternary_clause()); return to_literal(m_val2 >> 3); }
 
         bool is_clause() const { return get_kind() == CLAUSE; }
         clause_offset get_clause_offset() const { SASSERT(is_clause()); return static_cast<clause_offset>(m_val1); }
@@ -135,7 +136,7 @@ namespace sat {
     watched* find_binary_watch(watch_list & wlist, literal l);
     watched const* find_binary_watch(watch_list const & wlist, literal l);
     bool erase_clause_watch(watch_list & wlist, clause_offset c);
-    inline void erase_ternary_watch(watch_list & wlist, literal l1, literal l2) { wlist.erase(watched(l1, l2)); }
+    inline void erase_ternary_watch(watch_list & wlist, literal l1, literal l2) { wlist.erase(watched(l1, l2, true)); wlist.erase(watched(l1, l2, false)); }
 
     class clause_allocator;
     std::ostream& display_watch_list(std::ostream & out, clause_allocator const & ca, watch_list const & wlist);