merge

Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@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_config.cpp

@@ -38,8 +38,6 @@ namespace sat {
         m_glue_psm("glue_psm"),
         m_psm_glue("psm_glue") {
         m_num_threads = 1;
-        m_local_search = 0;
-        m_lookahead_search = false;
         m_lookahead_simplify = false;
         m_lookahead_simplify_bca = false;
         m_elim_vars = false;
@@ -92,7 +90,6 @@ namespace sat {
         m_local_search_threads = p.local_search_threads();
         m_lookahead_simplify = p.lookahead_simplify();
         m_lookahead_simplify_bca = p.lookahead_simplify_bca();
-        m_lookahead_search = p.lookahead_search();
         if (p.lookahead_reward() == symbol("heule_schur")) {
             m_lookahead_reward = heule_schur_reward;
         }
@@ -214,7 +211,6 @@ namespace sat {
         else {
             throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting");
         }
-        m_dimacs_inprocess_display  = p.dimacs_inprocess_display();
 
         sat_simplifier_params sp(_p);
         m_elim_vars = sp.elim_vars();

src/sat/sat_config.h

@@ -89,7 +89,6 @@ namespace sat {
         unsigned           m_num_threads;
         unsigned           m_local_search_threads;
         bool               m_local_search;
-        bool               m_lookahead_search;
         bool               m_lookahead_simplify;
         bool               m_lookahead_simplify_bca;
         cutoff_t           m_lookahead_cube_cutoff;
@@ -124,8 +123,6 @@ namespace sat {
         bool               m_drat_check_unsat;
         bool               m_drat_check_sat;
 
-        bool               m_dimacs_inprocess_display;
-
         symbol             m_always_true;
         symbol             m_always_false;
         symbol             m_caching;

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

@@ -2408,6 +2408,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_params.pyg

@@ -35,8 +35,8 @@ def_module_params('sat',
                           ('pb.solver', SYMBOL, 'circuit', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), solver (use SMT solver)'),
                           ('xor.solver', BOOL, False, 'use xor solver'),
                           ('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'),
-                          ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
                           ('local_search', BOOL, False, 'use local search instead of CDCL'),
+                          ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
                           ('lookahead.cube.cutoff', SYMBOL, 'adaptive', 'cutoff type used to create lookahead cubes: adaptive, fixed_depth, fixed_freevars, psat'),
                           ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive'),
                           ('lookahead.cube.depth', UINT, 10, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is fixed_depth.'),
@@ -49,6 +49,5 @@ def_module_params('sat',
                           ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'),
                           ('lookahead_simplify.bca', BOOL, False, 'add learned binary clauses as part of lookahead simplification'),
                           ('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'),
+                          ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu')))
-                          ('dimacs.inprocess.display', BOOL, False, 'display SAT instance in DIMACS format if unsolved after inprocess.max inprocessing passes')))
 

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);
@@ -950,12 +950,6 @@ namespace sat {
                 if (m_config.m_inprocess_max <= m_simplifications) {
                     m_reason_unknown = "sat.max.inprocess";
                     IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-inprocess\")\n";);
-                    if (m_config.m_dimacs_inprocess_display) {
-                        display_dimacs(std::cout);
-                        for (unsigned i = 0; i < num_lits; ++lits) {
-                            std::cout << dimacs_lit(lits[i]) << " 0\n";
-                        }
-                    }
                     return l_undef;
                 }
 
@@ -984,21 +978,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);
 
         // -----------------------