Add SLS tactic as a separate worker thread (#8263)

* setting up sls tactic thread

* finish the new threading setup, need to add the tactic

* add sls thread, it compiles but crashes

* it runs but there is some infinite recursion issue with the SLS thread

* debug code

* fix SLS

* update SLS to notify batch manager

* clean up imports

* add sls param, fix collect sls statistics, clean up other params

* clean up code

* handle the case when the SLS thread is canceled by another worker but the tactic is still running internally (don't throw an error in this case)

* let SLS worker take a stab at all LIA problems, even those with unsupported DISTINCT terms, but don't error on unsupported problems, just return

* fix bug when sls is false

---------

Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.lan1>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>

src/params/smt_parallel_params.pyg

@@ -2,5 +2,6 @@ def_module_params('smt_parallel',
                   export=True,
                   description='Experimental parameters for parallel solving',
                   params=(
-                        ('inprocessing', BOOL, True, 'integrate in-processing as a heuristic simplification'),
+                        ('inprocessing', BOOL, False, 'integrate in-processing as a heuristic simplification'),
+                        ('sls', BOOL, False, 'add sls-tactic as a separate worker thread outside the search tree parallelism'),
               ))

src/smt/smt_parallel.cpp

@@ -64,6 +64,50 @@ namespace smt {
 
 namespace smt {
 
+    void parallel::sls_worker::run() {
+        ptr_vector<expr> assertions;
+        p.ctx.get_assertions(assertions);
+        for (expr* e : assertions)
+            m_sls->assert_expr(m_g2l(e));
+
+        lbool res = l_undef;
+        try {
+            if (!m.inc())
+                return;
+            res = m_sls->check();
+        } catch (z3_exception& ex) {
+            // Cancellation is normal in portfolio mode
+            if (m.limit().is_canceled()) {
+                IF_VERBOSE(1, verbose_stream() << "SLS worker canceled\n");
+                return;
+            }
+
+            if (strstr(ex.what(), "unsupported for sls") != nullptr) {
+                IF_VERBOSE(1, verbose_stream() << "SLS opted out: " << ex.what() << "\n");
+                return;
+            }
+
+            // Anything else is a real error
+            IF_VERBOSE(1, verbose_stream() << "SLS threw exception: " << ex.what() << "\n");
+            b.set_exception(ex.what());
+            return;
+        }
+
+        if (res == l_true) {            
+            model_ref mdl = m_sls->get_model();
+            b.set_sat(m_l2g, *mdl);
+        }
+    }
+
+    void parallel::sls_worker::cancel() {
+        IF_VERBOSE(1, verbose_stream() << " SLS WORKER cancelling\n");
+        m.limit().cancel();
+    }
+
+    void parallel::sls_worker::collect_statistics(::statistics &st) const {
+        m_sls->collect_statistics(st);
+    }
+
     void parallel::worker::run() {
         search_tree::node<cube_config> *node = nullptr;
         expr_ref_vector cube(m);
@@ -151,6 +195,13 @@ namespace smt {
         m_config.m_inprocessing = pp.inprocessing();
     }
 
+    parallel::sls_worker::sls_worker(parallel& p)
+        : p(p), b(p.m_batch_manager), m(), m_g2l(p.ctx.m, m), m_l2g(m, p.ctx.m) {
+        IF_VERBOSE(1, verbose_stream() << "Initialized SLS portfolio thread\n");
+        m_params.append(p.ctx.m_params);
+        m_sls = alloc(sls::smt_solver, m, m_params);
+    }
+
     void parallel::worker::share_units() {
         // Collect new units learned locally by this worker and send to batch manager
         
@@ -281,7 +332,7 @@ namespace smt {
             SASSERT(p.ctx.m_unsat_core.empty());
             for (auto e : m_search_tree.get_core_from_root())
                p.ctx.m_unsat_core.push_back(e);
-            cancel_workers();
+            cancel_background_threads();
         }
     }
 
@@ -389,7 +440,7 @@ namespace smt {
             return;
         m_state = state::is_sat;
         p.ctx.set_model(m.translate(l2g));
-        cancel_workers();
+        cancel_background_threads();
     }
 
     void parallel::batch_manager::set_unsat(ast_translation &l2g, expr_ref_vector const &unsat_core) {
@@ -403,7 +454,7 @@ namespace smt {
         SASSERT(p.ctx.m_unsat_core.empty());
         for (expr *e : unsat_core)
             p.ctx.m_unsat_core.push_back(l2g(e));
-        cancel_workers();
+        cancel_background_threads();
     }
 
     void parallel::batch_manager::set_exception(unsigned error_code) {
@@ -413,7 +464,7 @@ namespace smt {
             return;
         m_state = state::is_exception_code;
         m_exception_code = error_code;
-        cancel_workers();
+        cancel_background_threads();
     }
 
     void parallel::batch_manager::set_exception(std::string const &msg) {
@@ -423,7 +474,7 @@ namespace smt {
             return;
         m_state = state::is_exception_msg;
         m_exception_msg = msg;
-        cancel_workers();
+        cancel_background_threads();
     }
 
     lbool parallel::batch_manager::get_result() const {
@@ -487,6 +538,7 @@ namespace smt {
     }
 
     lbool parallel::operator()(expr_ref_vector const &asms) {
+        IF_VERBOSE(1, verbose_stream() << "Parallel SMT with " << num_threads << " threads\n";);
         ast_manager &m = ctx.m;
 
         if (m.has_trace_stream())
@@ -497,26 +549,38 @@ namespace smt {
             scoped_clear(parallel &p) : p(p) {}
             ~scoped_clear() {
                 p.m_workers.reset();
+                p.m_sls_worker = nullptr;
             }
         };
         scoped_clear clear(*this);
 
         m_batch_manager.initialize();
         m_workers.reset();
+
+        smt_parallel_params pp(ctx.m_params);
+        m_should_run_sls = pp.sls();
+        
         scoped_limits sl(m.limit());
         flet<unsigned> _nt(ctx.m_fparams.m_threads, 1);
         SASSERT(num_threads > 1);
         for (unsigned i = 0; i < num_threads; ++i)
             m_workers.push_back(alloc(worker, i, *this, asms));
-
         for (auto w : m_workers)
             sl.push_child(&(w->limit()));
+        if (m_should_run_sls) {
+            m_sls_worker = alloc(sls_worker, *this);
+            sl.push_child(&(m_sls_worker->limit()));
+        }
 
         // Launch threads
-        vector<std::thread> threads(num_threads);
+        vector<std::thread> threads;
-        for (unsigned i = 0; i < num_threads; ++i) {
+        threads.resize(m_should_run_sls ? num_threads + 1 : num_threads); // +1 for sls worker
+        for (unsigned i = 0; i < num_threads; ++i)
             threads[i] = std::thread([&, i]() { m_workers[i]->run(); });
-        }
+        
+        // the final thread runs the sls worker
+        if (m_should_run_sls)
+            threads[num_threads] = std::thread([&]() { m_sls_worker->run(); });
 
         // Wait for all threads to finish
         for (auto &th : threads)
@@ -525,6 +589,8 @@ namespace smt {
         for (auto w : m_workers)
             w->collect_statistics(ctx.m_aux_stats);
         m_batch_manager.collect_statistics(ctx.m_aux_stats);
+        if (m_should_run_sls)
+            m_sls_worker->collect_statistics(ctx.m_aux_stats);
 
         return m_batch_manager.get_result();
     }

src/smt/smt_parallel.h

@@ -20,6 +20,7 @@ Revision History:
 
 #include "smt/smt_context.h"
 #include "util/search_tree.h"
+#include "ast/sls/sls_smt_solver.h"
 #include <thread>
 #include <mutex>
 
@@ -35,6 +36,7 @@ namespace smt {
     class parallel {
         context& ctx;
         unsigned num_threads;
+        bool m_should_run_sls = false;
 
         struct shared_clause {
             unsigned source_worker_id;
@@ -77,6 +79,16 @@ namespace smt {
                     w->cancel();
             }
 
+            void cancel_sls_worker() {
+                IF_VERBOSE(1, verbose_stream() << "Canceling SLS worker\n");
+                p.m_sls_worker->cancel();
+            }
+
+            void cancel_background_threads() {
+                cancel_workers();
+                if (p.m_should_run_sls) cancel_sls_worker();    
+            }
+
             void init_parameters_state();
 
         public:
@@ -108,8 +120,8 @@ namespace smt {
                 bool m_share_units_relevant_only = true;
                 bool m_share_units_initial_only = true;
                 double m_max_conflict_mul = 1.5;
-                bool m_cube_initial_only = true;
+                bool m_inprocessing = false;
-                bool m_inprocessing = true;
+                bool m_sls = false;
                 unsigned m_inprocessing_delay = 1;
                 unsigned m_max_cube_depth = 20;
                 unsigned m_max_conflicts = UINT_MAX;
@@ -158,8 +170,28 @@ namespace smt {
 
         };
 
+        class sls_worker {
+            parallel &p;
+            batch_manager &b;
+            ast_manager m;
+            ast_translation m_g2l, m_l2g;
+            scoped_ptr<sls::smt_solver> m_sls;
+            params_ref m_params;
+
+            public:
+                sls_worker(parallel &p);
+                void cancel();
+                void run();
+                void collect_statistics(::statistics& st) const;
+
+                reslimit &limit() {
+                    return m.limit();
+                }
+        };
+
         batch_manager m_batch_manager;
         scoped_ptr_vector<worker> m_workers;
+        scoped_ptr<sls_worker> m_sls_worker;
 
     public:
         parallel(context& ctx) :