From be463eab6d67a122a0abd268d146f32b46f8ccc4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Aug 2025 13:51:50 -0700 Subject: [PATCH] add experimental parameters Signed-off-by: Nikolaj Bjorner --- src/params/CMakeLists.txt | 1 + src/params/smt_parallel_params.pyg | 7 +++++++ src/smt/smt_parallel.cpp | 7 +++++-- 3 files changed, 13 insertions(+), 2 deletions(-) create mode 100644 src/params/smt_parallel_params.pyg diff --git a/src/params/CMakeLists.txt b/src/params/CMakeLists.txt index 9aea5b918..f2c9ee7b4 100644 --- a/src/params/CMakeLists.txt +++ b/src/params/CMakeLists.txt @@ -21,6 +21,7 @@ z3_add_component(params bv_rewriter_params.pyg fpa_rewriter_params.pyg fpa2bv_rewriter_params.pyg + smt_parallel_params.pyg pattern_inference_params_helper.pyg poly_rewriter_params.pyg rewriter_params.pyg diff --git a/src/params/smt_parallel_params.pyg b/src/params/smt_parallel_params.pyg new file mode 100644 index 000000000..ab9cffd7c --- /dev/null +++ b/src/params/smt_parallel_params.pyg @@ -0,0 +1,7 @@ +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'), + )) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 4d9f84c02..f730173ef 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -23,6 +23,7 @@ Author: #include "ast/ast_translation.h" #include "smt/smt_parallel.h" #include "smt/smt_lookahead.h" +#include "params/smt_parallel_params.hpp" #ifdef SINGLE_THREAD @@ -99,12 +100,14 @@ namespace smt { b.report_assumption_used(l2g, e); // report assumptions used in unsat core, so they can be used in final core IF_VERBOSE(1, verbose_stream() << "Worker " << id << " found unsat cube\n"); - b.collect_clause(l2g, id, mk_not(mk_and(unsat_core))); + if (smt_parallel_params(p.ctx.m_params).share_conflicts()) + b.collect_clause(l2g, id, mk_not(mk_and(unsat_core))); break; } } } - share_units(l2g); + if (smt_parallel_params(p.ctx.m_params).share_units()) + share_units(l2g); } }