From 72501467bfb39358faeef6a6230c3e9b198cd190 Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Fri, 15 Aug 2025 12:09:24 -0700 Subject: [PATCH] add more params --- src/params/smt_parallel_params.pyg | 2 ++ src/smt/smt_parallel.cpp | 3 +++ 2 files changed, 5 insertions(+) diff --git a/src/params/smt_parallel_params.pyg b/src/params/smt_parallel_params.pyg index ab9cffd7c..89891deb1 100644 --- a/src/params/smt_parallel_params.pyg +++ b/src/params/smt_parallel_params.pyg @@ -4,4 +4,6 @@ def_module_params('smt_parallel', params=( ('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'), )) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index f730173ef..9bbf704d2 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -344,6 +344,9 @@ namespace smt { // currenly, the code just implements the greedy strategy void parallel::batch_manager::return_cubes(ast_translation& l2g, vectorconst& C_worker, expr_ref_vector const& A_worker) { + if (smt_parallel_params(p.ctx.m_params).never_cube()) + return; // portfolio only + auto atom_in_cube = [&](expr_ref_vector const& cube, expr* atom) { return any_of(cube, [&](expr* e) { return e == atom || (m.is_not(e, e) && e == atom); }); };