diff --git a/src/params/smt_parallel_params.pyg b/src/params/smt_parallel_params.pyg index df7b1b189..53892b066 100644 --- a/src/params/smt_parallel_params.pyg +++ b/src/params/smt_parallel_params.pyg @@ -9,5 +9,6 @@ def_module_params('smt_parallel', ('relevant_units_only', BOOL, True, 'only share relvant units'), ('max_conflict_mul', DOUBLE, 1.5, 'increment multiplier for max-conflicts'), ('share_units_initial_only', BOOL, False, 'share only initial Boolean atoms as units'), - ('cube_initial_only', BOOL, False, 'cube only on initial Boolean atoms') + ('cube_initial_only', BOOL, False, 'cube only on initial Boolean atoms'), + ('max_cube_size', UINT, 20, 'maximum size of a cube to share'), )) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index cb46725a0..77733e10d 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -420,6 +420,8 @@ namespace smt { for (unsigned i = start; i < stop; ++i) { // copy the last cube so that expanding m_cubes doesn't invalidate reference. auto cube = m_cubes[i]; + if (cube.size() >= m_config.m_max_cube_size) + continue; m_cubes.push_back(cube); m_cubes.back().push_back(m.mk_not(atom)); m_cubes[i].push_back(atom); @@ -522,6 +524,7 @@ namespace smt { m_cubes.reset(); m_cubes.push_back(expr_ref_vector(m)); // push empty cube m_split_atoms.reset(); + m_config.m_max_cube_size = smt_parallel_params(p.ctx.m_params).max_cube_size(); } lbool parallel::operator()(expr_ref_vector const& asms) { diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index 24e920f57..5309ffa42 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -45,11 +45,15 @@ namespace smt { is_exception_msg, is_exception_code }; + struct config { + unsigned m_max_cube_size = 20; + }; ast_manager& m; parallel& p; std::mutex mux; state m_state = state::is_running; + config m_config; expr_ref_vector m_split_atoms; // atoms to split on vector m_cubes; unsigned m_max_batch_size = 10;