diff --git a/src/smt/CubeTree.h b/src/smt/CubeTree.h index c82957d3e..79dbfd6f9 100644 --- a/src/smt/CubeTree.h +++ b/src/smt/CubeTree.h @@ -106,8 +106,7 @@ public: // get closest cube to current by getting a random sibling of current (if current was UNSAT and we removed it from the tree) // or by descending randomly to a leaf (if we split the current node) to get the newest cube split fromthe current // we descend randomly to a leaf instead of just taking a random child because it's possible another thread made more descendants - CubeNode* get_next_cube(CubeNode* current) { - + CubeNode* get_next_cube(CubeNode* current, std::vector& frontier_roots) { IF_VERBOSE(1, verbose_stream() << "CubeTree: current cube is null: " << (current == nullptr) << "\n"); if (!current) return nullptr; @@ -115,44 +114,66 @@ public: // lambda to find any active leaf in the subtree (explore all branches) std::function find_active_leaf = [&](CubeNode* node) -> CubeNode* { - if (!node || !node->active) return nullptr; - if (node->is_leaf()) return node; + if (!node) return nullptr; + if (node->is_leaf() && node->active) return node; for (CubeNode* child : node->children) { - CubeNode* leaf = find_active_leaf(child); - if (leaf) return leaf; + CubeNode* active_leaf = find_active_leaf(child); + if (active_leaf) return active_leaf; } return nullptr; }; CubeNode* node = current; + std::vector remaining_frontier_roots = frontier_roots; + bool is_unexplored_frontier = frontier_roots.size() > 0 && current->cube.size() < frontier_roots[0]->cube.size(); // i.e. current is above the frontier (which always happens when we start with the empty cube!!) + IF_VERBOSE(1, verbose_stream() << "CubeTree: current cube is " << (is_unexplored_frontier ? "above" : "within") << " the frontier\n"); + + // if current is above the frontier, start searching from the first frontier root + if (is_unexplored_frontier && !frontier_roots.empty()) { + IF_VERBOSE(1, verbose_stream() << "CubeTree: starting search from first frontier root\n"); + node = frontier_roots[0]; + } while (node) { - // 1. check if current node itself is active leaf - if (node->active && node->is_leaf()) return node; - - // 2. check active leaf descendants + // check active leaf descendants CubeNode* leaf_descendant = nullptr; - for (CubeNode* child : node->children) { - leaf_descendant = find_active_leaf(child); - if (leaf_descendant) return leaf_descendant; - } + leaf_descendant = find_active_leaf(node); + if (leaf_descendant) return leaf_descendant; - // 3 & 4. check siblings and their active leaf descendants - if (node->parent) { - CubeNode* parent = node->parent; - for (CubeNode* sibling : parent->children) { - if (sibling == node) continue; + // DO NOT NEED to check siblings and their active leaf descendants + // since this is handled by the recusion up the tree!! + // and checking siblings here is unsafe if we adhere to thread frontier optimizations - // check if sibling itself is an active leaf - if (sibling->active && sibling->is_leaf()) return sibling; + // see if we're at a boundary of the frontier (i.e. we hit one of the frontier roots) + auto it = std::find(remaining_frontier_roots.begin(), remaining_frontier_roots.end(), node); + // get the index of the node in remaining_frontier_roots + unsigned curr_root_idx = std::distance(remaining_frontier_roots.begin(), it); + if (it != remaining_frontier_roots.end()) { // i.e. the node is in the list of remaining_frontier_roots + IF_VERBOSE(1, verbose_stream() << "CubeTree: hit frontier root " << node << "\n"); - // check for active leaf descendants of sibling - CubeNode* leaf_in_sibling = find_active_leaf(sibling); - if (leaf_in_sibling) return leaf_in_sibling; + if (!remaining_frontier_roots.empty()) { + IF_VERBOSE(1, verbose_stream() << "CubeTree: picking next frontier root to search from.\n"); + // pick the next frontier root (wrap around if at end) + // we do this so we either move onto the next split atom in the frontier (if we just processed neg(atom)) + // or we get the negation of the atom we just processed (if we just processed pos(atom)) + // since the other the splits are added is [pos, neg, ...] for each split atom + node = remaining_frontier_roots[curr_root_idx + 1 < remaining_frontier_roots.size() ? curr_root_idx + 1 : 0]; + + // Remove exhausted frontier root + remaining_frontier_roots.erase(it); + } else { + IF_VERBOSE(1, verbose_stream() << "CubeTree: resetting frontier after exhausting\n"); + // Frontier exhausted: reset frontier_roots for next iteration + frontier_roots.clear(); + + // Start "global" search from current node + node = node->parent; } + + continue; } - // 5. climb up to parent + // Move up in the current frontier node = node->parent; } diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 4e2dbd811..10f42ed6b 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -104,8 +104,12 @@ namespace smt { LOG_WORKER(1, " Curr cube node is null: " << (m_curr_cube_node == nullptr) << "\n"); if (m_config.m_cubetree) { // use std::tie so we don't overshadow cube_node!!! - std::tie(cube_node, cube) = b.get_cube_from_tree(m_g2l, m_curr_cube_node); // cube node is the reference to the node in the tree, tells us how to get the next cube. "cube" is the translated cube we need for the solver + std::tie(cube_node, cube) = b.get_cube_from_tree(m_g2l, frontier_roots, m_curr_cube_node); // cube node is the reference to the node in the tree, tells us how to get the next cube. "cube" is the translated cube we need for the solver LOG_WORKER(1, " Got cube node from CubeTree. Is null: " << (cube_node == nullptr) << "\n"); + if (!cube_node) { // i.e. no more cubes + LOG_WORKER(1, " No more cubes from CubeTree, exiting\n"); + return; + } m_curr_cube_node = cube_node; // store the current cube so we know how to get the next closest cube from the tree IF_VERBOSE(1, verbose_stream() << " Worker " << id << " got cube of size " << cube.size() << " from CubeTree\n"); } else { @@ -159,8 +163,7 @@ namespace smt { b.return_cubes(m_l2g, cube, split_atoms, should_split, cube_hardness); } else if (m_config.m_cubetree) { IF_VERBOSE(1, verbose_stream() << " returning undef cube to CubeTree. Cube node is null: " << (cube_node == nullptr) << "\n"); - - b.return_cubes_tree(m_l2g, cube_node, split_atoms); + b.return_cubes_tree(m_l2g, cube_node, split_atoms, frontier_roots); } else { b.return_cubes(m_l2g, cube, split_atoms); } @@ -382,7 +385,7 @@ namespace smt { return r; } - std::pair parallel::batch_manager::get_cube_from_tree(ast_translation& g2l, CubeNode* prev_cube) { + std::pair parallel::batch_manager::get_cube_from_tree(ast_translation& g2l, std::vector& frontier_roots, CubeNode* prev_cube) { std::scoped_lock lock(mux); expr_ref_vector l_cube(g2l.to()); SASSERT(m_config.m_cubetree); @@ -402,10 +405,15 @@ namespace smt { // get a cube from the CubeTree SASSERT(!m_cubes_tree.empty()); - CubeNode* next_cube_node = m_cubes_tree.get_next_cube(prev_cube); // get the next cube in the tree closest to the prev cube (i.e. longest common prefix) + CubeNode* next_cube_node = m_cubes_tree.get_next_cube(prev_cube, frontier_roots); // get the next cube in the tree closest to the prev cube (i.e. longest common prefix) IF_VERBOSE(1, verbose_stream() << "Batch manager giving out cube from CubeTree. Is null: " << (next_cube_node==nullptr) << "\n"); + if (!next_cube_node) { // i.e. no more cubes + IF_VERBOSE(1, verbose_stream() << " No more cubes from CubeTree, exiting\n"); + return {nullptr, l_cube}; // return nullptr and empty cube + } + for (auto& e : next_cube_node->cube) { l_cube.push_back(g2l(e)); } @@ -781,12 +789,14 @@ namespace smt { } } - void parallel::batch_manager::return_cubes_tree(ast_translation& l2g, CubeNode* cube_node, expr_ref_vector const& A_worker) { - + void parallel::batch_manager::return_cubes_tree(ast_translation& l2g, CubeNode* cube_node, expr_ref_vector const& A_worker, std::vector& frontier_roots) { IF_VERBOSE(1, verbose_stream() << " Returning cube to batch manager's cube tree.\n"); - expr_ref_vector const& c = cube_node->cube; + expr_ref_vector const& l_cube = cube_node->cube; IF_VERBOSE(1, verbose_stream() << " Cube node null: " << (cube_node == nullptr) << "\n"); - IF_VERBOSE(1, verbose_stream() << " PROCESSING CUBE of size: " << c.size() << "\n"); + IF_VERBOSE(1, verbose_stream() << " PROCESSING CUBE of size: " << l_cube.size() << "\n"); + + bool is_new_frontier = frontier_roots.empty(); // need to save this as a bool here, bc otherwise the frontier stops being populated after a single split atom + IF_VERBOSE(1, verbose_stream() << " Is new frontier: " << is_new_frontier << "\n"); 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); }); @@ -797,19 +807,29 @@ namespace smt { auto add_split_atom_tree = [&](expr* atom) { IF_VERBOSE(1, verbose_stream() << " Adding split atom to tree: " << mk_bounded_pp(atom, m, 3) << "\n"); expr_ref_vector g_cube(l2g.to()); - for (auto& atom : c) + for (auto& atom : l_cube) g_cube.push_back(l2g(atom)); // Positive atom branch - expr_ref_vector cube_pos = g_cube; - cube_pos.push_back(atom); + expr_ref_vector g_cube_pos = g_cube; + g_cube_pos.push_back(atom); // Negative atom branch - expr_ref_vector cube_neg = g_cube; - cube_neg.push_back(m.mk_not(atom)); + expr_ref_vector g_cube_neg = g_cube; + g_cube_neg.push_back(m.mk_not(atom)); + m_cubes_tree.add_children(cube_node, g_cube_pos, g_cube_neg); // default is active + if (is_new_frontier) { // note: calling frontier_roots.empty() here would always return false after adding the first split atom + // add cube_pos and cube_neg to frontier roots + CubeNode* cube_node_pos = new CubeNode(*cube_node); // deep copy of the node + CubeNode* cube_node_neg = new CubeNode(*cube_node); // deep copy of the node + cube_node_pos->cube.push_back(atom); // modify cube + cube_node_neg->cube.push_back(m.mk_not(atom)); // modify cube - m_cubes_tree.add_children(cube_node, cube_pos, cube_neg); // default is active + frontier_roots.push_back(cube_node_pos); + frontier_roots.push_back(cube_node_neg); + IF_VERBOSE(1, verbose_stream() << " Added split to frontier roots. Size now: " << frontier_roots.size() << "\n"); + } m_stats.m_num_cubes += 2; m_stats.m_max_cube_depth = std::max(m_stats.m_max_cube_depth, g_cube.size() + 1); @@ -817,8 +837,7 @@ namespace smt { std::scoped_lock lock(mux); - - if (c.size() >= m_config.m_max_cube_depth) { + if (l_cube.size() >= m_config.m_max_cube_depth) { IF_VERBOSE(1, verbose_stream() << " Skipping split of cube at max depth " << m_config.m_max_cube_depth << "\n";); cube_node->active = true; // mark the cube as active again since we didn't split it return; @@ -832,7 +851,7 @@ namespace smt { if (!m_split_atoms.contains(g_atom)) m_split_atoms.push_back(g_atom); - IF_VERBOSE(1, verbose_stream() << " splitting worker cubes on new atom for PQ " << mk_bounded_pp(g_atom, m, 3) << "\n"); + IF_VERBOSE(1, verbose_stream() << " splitting worker cube on new atom " << mk_bounded_pp(g_atom, m, 3) << "\n"); add_split_atom_tree(g_atom); } } diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index a35332b69..68393deec 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -132,13 +132,13 @@ namespace smt { // The batch manager returns the next cube to // expr_ref_vector get_cube(ast_translation& g2l); // FOR ALL NON-TREE VERSIONS - std::pair get_cube_from_tree(ast_translation& g2l, CubeNode* prev_cube = nullptr); + std::pair get_cube_from_tree(ast_translation& g2l, std::vector& frontier_roots, CubeNode* prev_cube = nullptr); // // worker threads return unprocessed cubes to the batch manager together with split literal candidates. // the batch manager re-enqueues unprocessed cubes and optionally splits them using the split_atoms returned by this and workers. // - void return_cubes_tree(ast_translation& l2g, CubeNode* cube, expr_ref_vector const& split_atoms); + void return_cubes_tree(ast_translation& l2g, CubeNode* cube, expr_ref_vector const& split_atoms, std::vector& frontier_roots); // FOR ALL NON-TREE VERSIONS void return_cubes(ast_translation& l2g, expr_ref_vector const& cube, expr_ref_vector const& split_atoms, const bool should_split=true, const double hardness=1.0); void report_assumption_used(ast_translation& l2g, expr* assumption); @@ -198,6 +198,8 @@ namespace smt { scoped_ptr ctx; ast_translation m_g2l, m_l2g; CubeNode* m_curr_cube_node = nullptr; + std::vector frontier_roots; + unsigned m_num_shared_units = 0; unsigned m_num_initial_atoms = 0; unsigned m_shared_clause_limit = 0; // remembers the index into shared_clause_trail marking the boundary between "old" and "new" clauses to share