normalize parallel params

src/smt/smt_parallel.cpp

@@ -25,6 +25,7 @@ Author:
 #include "smt/smt_parallel.h"
 #include "smt/smt_lookahead.h"
 #include "solver/solver_preprocess.h"
+#include "solver/parallel_params.hpp"
 
 #include <cmath>
 #include <mutex>
@@ -865,11 +866,12 @@ namespace smt {
         m_num_initial_atoms = ctx->get_num_bool_vars();
         ctx->get_fparams().m_preprocess = false;  // avoid preprocessing lemmas that are exchanged
 
+        parallel_params pp(p.ctx.get_params());
         m_config.m_inprocessing = false;
-        m_config.m_global_backbones = true;
+        m_config.m_global_backbones = pp.num_bb_threads() > 0;
         m_config.m_local_backbones = false;
-        m_config.m_core_minimize = true;
+        m_config.m_core_minimize = pp.core_minimize();
-        m_config.m_ablate_backtracking = false;
+        m_config.m_ablate_backtracking = pp.ablate_backtracking();
         
         // When ablating backtracking, disable core minimization since we're using the full cube path
         if (m_config.m_ablate_backtracking) {
@@ -1793,7 +1795,8 @@ namespace smt {
         m_worker_leases.reset();
         m_worker_leases.resize(p.m_workers.size());
         
-        m_ablate_backtracking = false;
+        parallel_params pp(p.ctx.get_params());
+        m_ablate_backtracking = pp.ablate_backtracking();
     }
 
     void parallel::batch_manager::collect_statistics(::statistics &st) const {
@@ -1807,10 +1810,17 @@ namespace smt {
     }
 
     lbool parallel::operator()(expr_ref_vector const &asms) {
-        unsigned num_global_bb_batch_threads = 2;
+        params_ref const& params = ctx.get_params();
+        parallel_params pp(params);
+        unsigned num_global_bb_batch_threads = pp.num_bb_threads();
+        if (num_global_bb_batch_threads > 2)
+            throw default_exception("parallel.num_bb_threads must be 0, 1, or 2");
         unsigned num_workers = std::min((unsigned)std::thread::hardware_concurrency(), ctx.get_fparams().m_threads);
         unsigned num_sls_threads = 0;
-        unsigned num_core_min_threads = 1;
+        bool core_minimize = pp.core_minimize();
+        if (pp.ablate_backtracking())
+            core_minimize = false;
+        unsigned num_core_min_threads = (core_minimize ? 1 : 0);
         unsigned num_global_bb_fl_threads = 0;
         unsigned num_global_bb_threads = num_global_bb_fl_threads > 0 ? num_global_bb_fl_threads : num_global_bb_batch_threads;
         unsigned total_threads = num_workers + num_sls_threads + num_core_min_threads + num_global_bb_threads;

src/solver/parallel_params.pyg

@@ -8,6 +8,7 @@ def_module_params('parallel',
                           ('threads.max', UINT, 10000, 'caps maximal number of threads below the number of processors'),
                           ('num_bb_threads', UINT, 2, 'run Janota-style chunking backbone worker threads; default is 2 (negative and positive mode), supported values are 0 (off), 1 (negative mode only) or 2 (negative and positive mode)'),
                           ('core_minimize', BOOL, True, 'minimize unsat cores used for parallel cube backtracking'),
+                          ('ablate_backtracking', BOOL, False, 'ablation: pass entire cube as core instead of unsat core during backtracking'),
                           ('cube.lookahead', BOOL, False, 'use lookahead cubing in the parallel solver; when false, use VSIDS activity to select one split literal'),
                           ('conquer.batch_size', UINT, 100, 'number of cubes to batch together for fast conquer'),
                           ('conquer.restart.max', UINT, 5, 'maximal number of restarts during conquer phase'),

src/solver/parallel_tactical2.cpp

@@ -953,6 +953,7 @@ class parallel_solver {
                 bool     m_share_units_initial_only = true;
                 bool     m_core_minimize         = false;
                 bool     m_global_backbones      = false;
+                bool     m_ablate_backtracking   = false;
                 unsigned m_max_cube_depth        = 20;
         };
 
@@ -1117,7 +1118,10 @@ class parallel_solver {
             : id(id), b(p.m_batch_manager), asms(m), m_g2l(src.get_manager(), m), m_l2g(m, src.get_manager()) {
             parallel_params pp(params);
             m_config.m_core_minimize = pp.core_minimize();
+            m_config.m_ablate_backtracking = pp.ablate_backtracking();
             m_config.m_global_backbones = pp.num_bb_threads() > 0;
+            if (m_config.m_ablate_backtracking)
+                m_config.m_core_minimize = false;
 
             s = src.translate(m, params);
             // don't share initial units
@@ -1211,7 +1215,8 @@ class parallel_solver {
 
                     LOG_WORKER(1, " found unsat cube\n");
                     auto* source = lease.leased_node;
-                    b.backtrack(m_l2g, id, unsat_core, lease);
+                    expr_ref_vector const& core_to_use = m_config.m_ablate_backtracking ? cube : unsat_core;
+                    b.backtrack(m_l2g, id, core_to_use, lease);
 
                     if (m_config.m_core_minimize)
                         b.enqueue_core_minimization(m_l2g, source, unsat_core);
@@ -1869,6 +1874,8 @@ public:
             static_cast<unsigned>(std::thread::hardware_concurrency()),
             pp.threads_max());
         bool core_minimize = pp.core_minimize();
+        if (pp.ablate_backtracking())
+            core_minimize = false;
         unsigned num_bb_threads = pp.num_bb_threads();
         if (num_bb_threads > 2)
             throw default_exception("parallel.num_bb_threads must be 0, 1, or 2");