From 0782563e0c84d6a3ca21068c0a19ddd5c93fa5b2 Mon Sep 17 00:00:00 2001
From: Ilana Shapiro <ilanashapiro@Mac.localdomain>
Date: Tue, 16 Dec 2025 10:41:06 -0800
Subject: [PATCH] add user params

---
 src/params/CMakeLists.txt          |  1 +
 src/params/smt_parallel_params.pyg | 25 +++++++++++++++++++++++++
 src/smt/smt_parallel.cpp           |  8 +++++++-
 3 files changed, 33 insertions(+), 1 deletion(-)
 create mode 100644 src/params/smt_parallel_params.pyg

diff --git a/src/params/CMakeLists.txt b/src/params/CMakeLists.txt
index 9aea5b918..732430fe3 100644
--- a/src/params/CMakeLists.txt
+++ b/src/params/CMakeLists.txt
@@ -28,6 +28,7 @@ z3_add_component(params
     seq_rewriter_params.pyg
     sls_params.pyg
     smt_params_helper.pyg
+    smt_parallel_params.pyg
     solver_params.pyg
     tactic_params.pyg
   EXTRA_REGISTER_MODULE_HEADERS
diff --git a/src/params/smt_parallel_params.pyg b/src/params/smt_parallel_params.pyg
new file mode 100644
index 000000000..51ca7e2b2
--- /dev/null
+++ b/src/params/smt_parallel_params.pyg
@@ -0,0 +1,25 @@
+def_module_params('smt_parallel', 
+                  export=True,
+                  description='Experimental parameters for parallel solving',
+                  params=(
+                        ('share_units', BOOL, True, 'share units'),
+                        ('share_conflicts', BOOL, True, 'share conflicts'),
+                        ('never_cube', BOOL, False, 'never cube'),
+                        ('frugal_cube_only', BOOL, False, 'only apply frugal cube strategy'),
+                        ('relevant_units_only', BOOL, True, 'only share relvant units'),
+                        ('max_conflict_mul', DOUBLE, 1.5, 'increment multiplier for max-conflicts'),
+                        ('share_units_initial_only', BOOL, True, 'share only initial Boolean atoms as units'),
+                        ('cube_initial_only', BOOL, False, 'cube only on initial Boolean atoms'),
+                        ('max_cube_depth', UINT, 20, 'maximum depth (size) of a cube to share'),
+                        ('max_greedy_cubes', UINT, 1000, 'maximum number of cube to greedily share before switching to frugal'),
+                        ('num_split_lits', UINT, 2, 'how many literals, k, we split on to create 2^k cubes'),
+                        ('depth_splitting_only', BOOL, False, 'only apply frugal cube strategy, and only on deepest (biggest) cubes from the batch manager'),
+                        ('backbone_detection', BOOL, False, 'apply backbone literal heuristic'),
+                        ('iterative_deepening', BOOL, False, 'deepen cubes based on iterative hardness cutoff heuristic'),
+                        ('beam_search', BOOL, False, 'use beam search with PQ to rank cubes given to threads'),
+                        ('explicit_hardness', BOOL, False, 'use explicit hardness metric for cube'),
+                        ('cubetree', BOOL, False, 'use cube tree data structure for storing cubes'),
+                        ('searchtree', BOOL, False, 'use search tree implementation (parallel2)'),
+                        ('inprocessing', BOOL, False, 'integrate in-processing as a heuristic simplification'),
+                        ('inprocessing_delay', UINT, 0, 'number of undef before invoking simplification'),
+              ))
\ No newline at end of file
diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index c4ece1ad7..dc6b7cfb5 100644
--- a/src/smt/smt_parallel.cpp
+++ b/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 "params/smt_parallel_params.hpp"
 
 #include <cmath>
 #include <mutex>
@@ -121,8 +122,10 @@ namespace smt {
                 break;
             }
             }
-            if (m_config.m_share_units)
+            if (m_config.m_share_units) {
+                IF_VERBOSE(1, verbose_stream() << " Sharing units\n");
                 share_units();
+            }
         }
     }
 
@@ -141,6 +144,9 @@ namespace smt {
         m_num_shared_units = ctx->assigned_literals().size();
         m_num_initial_atoms = ctx->get_num_bool_vars();
         ctx->get_fparams().m_preprocess = false;  // avoid preprocessing lemmas that are exchanged
+
+        smt_parallel_params pp(p.ctx.m_params);
+        m_config.m_share_units = pp.share_units();
     }
 
     void parallel::worker::share_units() {