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); }); };