fixes to inprocessing code

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

src/sat/sat_asymm_branch.cpp

@@ -59,7 +59,7 @@ namespace sat {
         }
     };
 
-    void asymm_branch::process(scc& scc, clause_vector& clauses) {
+    void asymm_branch::process(scc* scc, clause_vector& clauses) {
         int64 limit = -m_asymm_branch_limit;
         std::stable_sort(clauses.begin(), clauses.end(), clause_size_lt());
         m_counter -= clauses.size();
@@ -83,7 +83,7 @@ namespace sat {
                 }
                 s.checkpoint();
                 clause & c = *(*it);
-                if (m_asymm_branch_sampled ? !process_sampled(scc, c) : !process(c)) {
+                if (scc ? !process_sampled(*scc, c) : !process(c)) {
                     continue; // clause was removed
                 }
                 *it2 = *it;
@@ -106,7 +106,7 @@ namespace sat {
         ++m_calls;
         if (m_calls <= m_asymm_branch_delay)
             return;
-        if (!m_asymm_branch && !m_asymm_branch_all)
+        if (!m_asymm_branch && !m_asymm_branch_all && !m_asymm_branch_sampled)
             return;
         s.propagate(false); // must propagate, since it uses s.push()
         if (s.m_inconsistent)
@@ -119,13 +119,18 @@ namespace sat {
         TRACE("asymm_branch_detail", s.display(tout););
         report rpt(*this);
         svector<char> saved_phase(s.m_phase);
+        if (m_asymm_branch) {
+            m_counter  = 0; 
+            process(nullptr, s.m_clauses);
+            m_counter = -m_counter;
+        }
         if (m_asymm_branch_sampled) {
             scc scc(s, m_params);
             while (true) {
                 unsigned elim = m_elim_literals;
                 scc.init_big(true);
-                process(scc, s.m_clauses);
+                process(&scc, s.m_clauses);
-                process(scc, s.m_learned);
+                process(&scc, s.m_learned);
                 s.propagate(false); 
                 if (s.m_inconsistent)
                     break;
@@ -134,12 +139,6 @@ namespace sat {
                     break;
             }
         }
-        else {
-            scc scc(s, m_params);
-            m_counter  = 0; 
-            process(scc, s.m_clauses);
-            m_counter = -m_counter;
-        }
         s.m_phase = saved_phase;
         m_asymm_branch_limit *= 2;
         if (m_asymm_branch_limit > UINT_MAX)

src/sat/sat_asymm_branch.h

@@ -41,6 +41,7 @@ namespace sat {
         bool       m_asymm_branch;
         unsigned   m_asymm_branch_delay;
         bool       m_asymm_branch_sampled;
+        bool       m_asymm_branch_propagate;
         bool       m_asymm_branch_all;
         int64      m_asymm_branch_limit;
 
@@ -64,7 +65,7 @@ namespace sat {
 
         bool process_sampled(scc& scc, clause & c);
 
-        void process(scc& scc, clause_vector & c);
+        void process(scc* scc, clause_vector & c);
         
         bool process_all(clause & c);
         

src/sat/sat_elim_eqs.cpp

@@ -94,10 +94,11 @@ namespace sat {
             if (!c.frozen())
                 m_solver.detach_clause(c);
             // apply substitution
-            for (i = 0; i < sz; i++) {                
+            for (i = 0; i < sz; i++) {   
-                c[i] = norm(roots, c[i]);
+				literal lit = c[i];
+                c[i] = norm(roots, lit);
                 VERIFY(c[i] == norm(roots, c[i]));
-                VERIFY(!m_solver.was_eliminated(c[i].var()));
+				VERIFY(!m_solver.was_eliminated(c[i].var()) || lit == c[i]);
             }
             std::sort(c.begin(), c.end());
             for (literal l : c) VERIFY(l == norm(roots, l));

src/sat/sat_lookahead.cpp

@@ -2081,6 +2081,7 @@ namespace sat {
             if (inconsistent()) {
                 TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";);
                 m_cube_state.m_freevars_threshold = prev_nfreevars;
+                m_cube_state.inc_conflict();
                 if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false;
                 continue;
             }
@@ -2375,6 +2376,8 @@ namespace sat {
                         ++disconnected1;
                         uf.merge(u.index(), v.index());
                         uf.merge((~u).index(), (~v).index());
+                        VERIFY(!m_s.was_eliminated(u.var()));
+                        VERIFY(!m_s.was_eliminated(v.var()));
                         m_s.mk_clause(~u, v, true);
                     }
                     else {

src/sat/sat_scc.cpp

@@ -303,16 +303,16 @@ namespace sat {
             else {
                 SASSERT(m_left[u.index()] == 0);
                 m_left[u.index()] = ++dfs_num;
-                for (literal v : m_dag[u.index()]) {
-                    if (m_left[v.index()] == 0) {
-                        todo.push_back(pframe(u, v));
-                    }
-                }
                 literal p = todo.back().parent();
                 if (p != null_literal) {
                     m_root[u.index()] = m_root[p.index()];
                     m_parent[u.index()] = p;
                 }
+                for (literal v : m_dag[u.index()]) {
+                    if (m_left[v.index()] == 0) {
+                        todo.push_back(pframe(u, v));
+                    }
+                }
             }
         }
         for (unsigned i = 0; i < num_lits; ++i) {
@@ -339,7 +339,7 @@ namespace sat {
             watch_list::iterator end    = wlist.end();
             for (; it != end; ++it) {
                 watched& w = *it;
-                if (learned ? w.is_binary_learned_clause() : w.is_binary_unblocked_clause()) {
+                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;

src/sat/sat_solver.cpp

@@ -159,17 +159,20 @@ namespace sat {
                 }
             }
             // copy high quality lemmas
+            unsigned num_learned = 0;
             for (clause* c : src.m_learned) {
                 if (c->glue() <= 2 || (c->size() <= 40 && c->glue() <= 8)) {
                     buffer.reset();
                     for (literal l : *c) buffer.push_back(l);
                     clause* c1 = mk_clause_core(buffer.size(), buffer.c_ptr(), true);
                     if (c1) {
+                        ++num_learned;
                         c1->set_glue(c->glue());
                         c1->set_psm(c->psm());
                     }
                 }
             }
+            IF_VERBOSE(1, verbose_stream() << "(sat.copy :learned " << num_learned << ")\n";);
         }
 
         m_user_scope_literals.reset();
@@ -879,9 +882,6 @@ namespace sat {
         m_stats.m_units = init_trail_size();
         IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";);
         SASSERT(at_base_lvl());
-        if (m_config.m_lookahead_search && num_lits == 0) {
-            return lookahead_search();
-        }
 
         if (m_config.m_local_search) {
             return do_local_search(num_lits, lits);
@@ -984,21 +984,6 @@ namespace sat {
         return r;
     }
 
-    lbool solver::lookahead_search() {
-        lookahead lh(*this);
-        lbool r = l_undef;
-        try {
-            r = lh.check();
-            m_model = lh.get_model();
-        }
-        catch (z3_exception&) {
-            lh.collect_statistics(m_aux_stats);
-            throw;
-        }
-        lh.collect_statistics(m_aux_stats);
-        return r;
-    }
-
     lbool solver::check_par(unsigned num_lits, literal const* lits) {
         scoped_ptr_vector<local_search> ls;
         int num_threads = static_cast<int>(m_config.m_num_threads + m_config.m_local_search_threads);

src/sat/sat_solver.h

@@ -394,7 +394,6 @@ namespace sat {
         void sort_watch_lits();
         void exchange_par();
         lbool check_par(unsigned num_lits, literal const* lits);
-        lbool lookahead_search();
         lbool do_local_search(unsigned num_lits, literal const* lits);
 
         // -----------------------