From 43d2a1f5b15bb9c2d7c9db288756e48827330935 Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Mon, 25 Aug 2025 10:15:56 -0700 Subject: [PATCH] rename variables --- src/params/smt_parallel_params.pyg | 4 ++-- src/smt/smt_parallel.cpp | 28 ++++++++++++++-------------- src/smt/smt_parallel.h | 6 +++--- 3 files changed, 19 insertions(+), 19 deletions(-) diff --git a/src/params/smt_parallel_params.pyg b/src/params/smt_parallel_params.pyg index dde9efd4d..191d3b2ef 100644 --- a/src/params/smt_parallel_params.pyg +++ b/src/params/smt_parallel_params.pyg @@ -10,8 +10,8 @@ def_module_params('smt_parallel', ('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'), - ('max_cube_size', UINT, 20, 'maximum size of a cube to share'), + ('max_cube_depth', UINT, 20, 'maximum depth (size) of a cube to share'), ('max_greedy_cubes', UINT, 1000, 'maximum number of cube to greedily share before switching to frugal'), ('num_split_lits', UINT, 2, 'how many literals, k, we split on to create 2^k cubes'), - ('frugal_deepest_cube_only', BOOL, False, 'only apply frugal cube strategy, and only on a deepest (biggest) cube from the batch manager'), + ('frugal_depth_splitting_only', BOOL, False, 'only apply frugal cube strategy, and only on deepest (biggest) cubes from the batch manager'), )) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 650464c68..a3476fe41 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -281,7 +281,7 @@ namespace smt { } for (unsigned i = 0; i < std::min(m_max_batch_size / p.num_threads, (unsigned)m_cubes.size()) && !m_cubes.empty(); ++i) { - if (m_config.m_frugal_deepest_cube_only) { + if (m_config.m_frugal_depth_splitting_only) { // get the deepest set of cubes auto& deepest_cubes = m_cubes_depth_sets.rbegin()->second; unsigned idx = rand() % deepest_cubes.size(); @@ -360,7 +360,7 @@ namespace smt { return l_undef; // the main context was cancelled, so we return undef. switch (m_state) { case state::is_running: // batch manager is still running, but all threads have processed their cubes, which means all cubes were unsat - if (!m_cubes.empty() || (m_config.m_frugal_deepest_cube_only && !m_cubes_depth_sets.empty())) + if (!m_cubes.empty() || (m_config.m_frugal_depth_splitting_only && !m_cubes_depth_sets.empty())) throw default_exception("inconsistent end state"); if (!p.m_assumptions_used.empty()) { // collect unsat core from assumptions used, if any --> case when all cubes were unsat, but depend on nonempty asms, so we need to add these asms to final unsat core @@ -448,12 +448,12 @@ 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) + if (cube.size() >= m_config.m_max_cube_depth) continue; m_cubes.push_back(cube); m_cubes.back().push_back(m.mk_not(atom)); m_cubes[i].push_back(atom); - m_stats.m_max_cube_size = std::max(m_stats.m_max_cube_size, m_cubes.back().size()); + m_stats.m_max_cube_depth = std::max(m_stats.m_max_cube_depth, m_cubes.back().size()); m_stats.m_num_cubes += 2; } }; @@ -464,7 +464,7 @@ namespace smt { expr_ref_vector g_cube(l2g.to()); for (auto& atom : c) g_cube.push_back(l2g(atom)); - if (g_cube.size() >= m_config.m_max_cube_size) // we already added this before!! we just need to add the splits now + if (g_cube.size() >= m_config.m_max_cube_depth) // we already added this before!! we just need to add the splits now continue; // add depth set d+1 if it doesn't exist yet @@ -481,13 +481,13 @@ namespace smt { m_cubes_depth_sets[d + 1].push_back(g_cube); m_stats.m_num_cubes += 2; - m_stats.m_max_cube_size = std::max(m_stats.m_max_cube_size, d + 1); + m_stats.m_max_cube_depth = std::max(m_stats.m_max_cube_depth, d + 1); } }; std::scoped_lock lock(mux); unsigned max_greedy_cubes = 1000; - bool greedy_mode = (m_cubes.size() <= max_greedy_cubes) && !m_config.m_frugal_cube_only && !m_config.m_frugal_deepest_cube_only; + bool greedy_mode = (m_cubes.size() <= max_greedy_cubes) && !m_config.m_frugal_cube_only && !m_config.m_frugal_depth_splitting_only; unsigned a_worker_start_idx = 0; // @@ -518,14 +518,14 @@ namespace smt { g_cube.push_back(l2g(atom)); unsigned start = m_cubes.size(); // update start after adding each cube so we only process the current cube being added - if (m_config.m_frugal_deepest_cube_only) { + if (m_config.m_frugal_depth_splitting_only) { // need to add the depth set if it doesn't exist yet if (m_cubes_depth_sets.find(g_cube.size()) == m_cubes_depth_sets.end()) { m_cubes_depth_sets[g_cube.size()] = vector(); } m_cubes_depth_sets[g_cube.size()].push_back(g_cube); m_stats.m_num_cubes += 1; - m_stats.m_max_cube_size = std::max(m_stats.m_max_cube_size, g_cube.size()); + m_stats.m_max_cube_depth = std::max(m_stats.m_max_cube_depth, g_cube.size()); } else { m_cubes.push_back(g_cube); } @@ -550,7 +550,7 @@ namespace smt { expr_ref g_atom(l2g(A_worker[i]), l2g.to()); if (!m_split_atoms.contains(g_atom)) m_split_atoms.push_back(g_atom); - if (m_config.m_frugal_deepest_cube_only) { + if (m_config.m_frugal_depth_splitting_only) { add_split_atom_deepest_cubes(g_atom); } else { add_split_atom(g_atom, initial_m_cubes_size); @@ -609,22 +609,22 @@ namespace smt { m_cubes.reset(); m_cubes.push_back(expr_ref_vector(m)); // push empty cube - if (m_config.m_frugal_deepest_cube_only) { + if (m_config.m_frugal_depth_splitting_only) { m_cubes_depth_sets.clear(); } m_split_atoms.reset(); smt_parallel_params sp(p.ctx.m_params); - m_config.m_max_cube_size = sp.max_cube_size(); + m_config.m_max_cube_depth = sp.max_cube_depth(); m_config.m_frugal_cube_only = sp.frugal_cube_only(); m_config.m_never_cube = sp.never_cube(); - m_config.m_frugal_deepest_cube_only = sp.frugal_deepest_cube_only(); + m_config.m_frugal_depth_splitting_only = sp.frugal_depth_splitting_only(); } void parallel::batch_manager::collect_statistics(::statistics& st) const { //ctx->collect_statistics(st); st.update("parallel-num_cubes", m_stats.m_num_cubes); - st.update("parallel-max-cube-size", m_stats.m_max_cube_size); + st.update("parallel-max-cube-size", m_stats.m_max_cube_depth); } lbool parallel::operator()(expr_ref_vector const& asms) { diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index ae084a65e..99d5633f6 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -47,13 +47,13 @@ namespace smt { is_exception_code }; struct config { - unsigned m_max_cube_size = 20; + unsigned m_max_cube_depth = 20; bool m_frugal_cube_only = false; bool m_never_cube = false; - bool m_frugal_deepest_cube_only = false; + bool m_frugal_depth_splitting_only = false; }; struct stats { - unsigned m_max_cube_size = 0; + unsigned m_max_cube_depth = 0; unsigned m_num_cubes = 0; };