From 0eb0406444c7cda1c92311e4511c7e241405773c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 20 Sep 2025 20:32:44 +0300 Subject: [PATCH] configuration parameter renaming Signed-off-by: Nikolaj Bjorner --- src/smt/smt_parallel.cpp | 2 +- src/smt/smt_parallel.h | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 11371b29a..cbae4a3ef 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -155,7 +155,7 @@ namespace smt { unsigned sz = ctx->assigned_literals().size(); for (unsigned j = m_num_shared_units; j < sz; ++j) { // iterate only over new literals since last sync literal lit = ctx->assigned_literals()[j]; - if (!ctx->is_relevant(lit.var()) && m_config.m_relevant_units_only) + if (!ctx->is_relevant(lit.var()) && m_config.m_share_units_relevant_only) continue; if (m_config.m_share_units_initial_only && lit.var() >= m_num_initial_atoms) { diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index f7dfd4456..25d8f576b 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -108,16 +108,16 @@ namespace smt { class worker { struct config { unsigned m_threads_max_conflicts = 1000; - unsigned m_max_conflicts = 10000000; - bool m_relevant_units_only = true; - bool m_share_conflicts = true; + bool m_share_conflicts = false; bool m_share_units = true; - double m_max_conflict_mul = 1.5; + 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 = true; unsigned m_inprocessing_delay = 1; unsigned m_max_cube_depth = 20; + unsigned m_max_conflicts = UINT_MAX; }; using node = search_tree::node;