From f6f87ce0a27b1cc005ce288909679476e1872fb7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Aug 2025 14:40:17 -0700 Subject: [PATCH] add setting for frugal-only strategy Signed-off-by: Nikolaj Bjorner --- src/params/smt_parallel_params.pyg | 2 +- src/smt/smt_parallel.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/params/smt_parallel_params.pyg b/src/params/smt_parallel_params.pyg index 89891deb1..cfb5f276f 100644 --- a/src/params/smt_parallel_params.pyg +++ b/src/params/smt_parallel_params.pyg @@ -5,5 +5,5 @@ def_module_params('smt_parallel', ('share_units', BOOL, True, 'share units'), ('share_conflicts', BOOL, True, 'share conflicts'), ('never_cube', BOOL, False, 'never cube'), - ('only_eager_cube', BOOL, False, 'only eager cube'), + ('frugal_cube_only', BOOL, False, 'only apply frugal cube strategy'), )) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 9bbf704d2..86f9d5a21 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -362,7 +362,7 @@ namespace smt { std::scoped_lock lock(mux); unsigned max_cubes = 1000; - bool greedy_mode = (m_cubes.size() <= max_cubes); + bool greedy_mode = (m_cubes.size() <= max_cubes) && !smt_parallel_params(p.ctx.m_params).frugal_cube_only(); unsigned a_worker_start_idx = 0; //