set clean shutdown for local search and re-enable local search when i…

…t parallelizes with PB solver

Signed-off-by: Nikolaj Bjorner <[email protected]>

src/sat/sat_local_search.cpp

@@ -362,7 +362,7 @@ namespace sat {
             set_phase(i, phase[i]);
     }
 
-    void local_search::import(solver const& s, bool _init) {        
+    void local_search::import(solver const& s, bool _init) {
         flet<bool> linit(m_initializing, true);
         m_is_pb = false;
         m_vars.reset();
@@ -412,9 +412,10 @@ namespace sat {
             [&](unsigned sz, literal const* c, unsigned k) { add_cardinality(sz, c, k); };
         std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)> pb = 
             [&](unsigned sz, literal const* c, unsigned const* coeffs, unsigned k) { add_pb(sz, c, coeffs, k); };
-        if (ext && (!ext->is_pb() || !ext->extract_pb(card, pb)))
+        if (ext && (!ext->is_pb() || !ext->extract_pb(card, pb))) {
+            IF_VERBOSE(0, verbose_stream() << (ext) << " is-pb " << (!ext && ext->is_pb()) << "\n");
             throw default_exception("local search is incomplete with extensions beyond PB");
-
+        }
         if (_init) 
             init();        
     }

src/sat/sat_parallel.cpp

@@ -87,9 +87,15 @@ namespace sat {
     parallel::parallel(solver& s): m_num_clauses(0), m_consumer_ready(false), m_scoped_rlimit(s.rlimit()) {}
 
     parallel::~parallel() {
+        reset();
+    }
+
+    void parallel::reset() {
         m_limits.reset();
+        m_scoped_rlimit.reset();
         for (auto* s : m_solvers)
             dealloc(s);
+        m_solvers.reset();
     }
 
     void parallel::init_solvers(solver& s, unsigned num_extra_solvers) {

src/sat/sat_parallel.h

@@ -78,6 +78,8 @@ namespace sat {
 
         ~parallel();
 
+        void reset();
+
         void init_solvers(solver& s, unsigned num_extra_solvers);
 
         void push_child(reslimit& rl);

src/sat/sat_solver.cpp

@@ -1243,8 +1243,11 @@ namespace sat {
             m_cleaner(true);
             return do_local_search(num_lits, lits);
         }
-        if ((m_config.m_num_threads > 1 || m_config.m_local_search_threads > 0 || 
-             m_config.m_ddfw_threads > 0) && !m_par && !m_ext) {
+        if ((m_config.m_num_threads > 1 || m_config.m_ddfw_threads > 0) && !m_par && !m_ext) {
+            SASSERT(scope_lvl() == 0);
+            return check_par(num_lits, lits);
+        }
+        if (m_config.m_local_search_threads > 0 && !m_par && (!m_ext || m_ext->is_pb())) {
             SASSERT(scope_lvl() == 0);
             return check_par(num_lits, lits);
         }
@@ -1460,15 +1463,17 @@ namespace sat {
         if (!rlimit().inc()) {
             return l_undef;
         }
-        if (m_ext)
+        if (m_ext && !m_ext->is_pb())
             return l_undef;
 
-        scoped_ptr_vector<i_local_search> ls;
-        scoped_ptr_vector<solver> uw;
+
         int num_extra_solvers = m_config.m_num_threads - 1;
         int num_local_search  = static_cast<int>(m_config.m_local_search_threads);
         int num_ddfw      = m_ext ? 0 : static_cast<int>(m_config.m_ddfw_threads);
         int num_threads = num_extra_solvers + 1 + num_local_search + num_ddfw;        
+        vector<reslimit> lims(num_ddfw);
+        scoped_ptr_vector<i_local_search> ls;
+        scoped_ptr_vector<solver> uw;
         for (int i = 0; i < num_local_search; ++i) {
             local_search* l = alloc(local_search);
             l->updt_params(m_params);
@@ -1477,7 +1482,7 @@ namespace sat {
             ls.push_back(l);
         }
 
-        vector<reslimit> lims(num_ddfw);            
+
         // set up ddfw search
         for (int i = 0; i < num_ddfw; ++i) {
             ddfw* d = alloc(ddfw);
@@ -1593,6 +1598,7 @@ namespace sat {
         if (!canceled) {
             rlimit().reset_cancel();
         }
+        par.reset();
         set_par(nullptr, 0);
         ls.reset();
         uw.reset();