diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 74aa43d1c..aa33e73e4 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -412,17 +412,7 @@ namespace smt { 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_search_tree.is_closed()) - throw default_exception("inconsistent end state"); - - // case when all cubes were unsat, but depend on nonempty asms, so we need to add these asms to final unsat core - // these asms are stored in the cube tree, at the root node - if (p.ctx.m_unsat_core.empty()) { - SASSERT(root && root->is_closed()); - for (auto a : m_search_tree.get_core_from_root()) - p.ctx.m_unsat_core.push_back(a); - } - return l_false; + throw default_exception("inconsistent end state"); case state::is_unsat: return l_false; case state::is_sat: diff --git a/src/util/search_tree.h b/src/util/search_tree.h index 2f0d29bec..2b9a41b59 100644 --- a/src/util/search_tree.h +++ b/src/util/search_tree.h @@ -14,7 +14,7 @@ Abstract: - Closed nodes are fully explored (both children are closed). - Active nodes have no children and are currently being explored. - Open nodes either have children that are open or are leaves. - + A node can be split if it is active. After splitting, it becomes open and has two open children. Backtracking on a conflict closes all nodes below the last node whose atom is in the conflict set. @@ -35,26 +35,33 @@ namespace search_tree { enum class status { open, closed, active }; - template - class node { + template class node { typedef typename Config::literal literal; literal m_literal; - node* m_left = nullptr, * m_right = nullptr, * m_parent = nullptr; + node *m_left = nullptr, *m_right = nullptr, *m_parent = nullptr; status m_status; vector m_core; + public: - node(literal const& l, node* parent) : - m_literal(l), m_parent(parent), m_status(status::open) {} + node(literal const &l, node *parent) : m_literal(l), m_parent(parent), m_status(status::open) {} ~node() { dealloc(m_left); dealloc(m_right); } - status get_status() const { return m_status; } - void set_status(status s) { m_status = s; } - literal const& get_literal() const { return m_literal; } - bool literal_is_null() const { return Config::is_null(m_literal); } - void split(literal const& a, literal const& b) { + status get_status() const { + return m_status; + } + void set_status(status s) { + m_status = s; + } + literal const &get_literal() const { + return m_literal; + } + bool literal_is_null() const { + return Config::is_null(m_literal); + } + void split(literal const &a, literal const &b) { SASSERT(!Config::literal_is_null(a)); SASSERT(!Config::literal_is_null(b)); if (m_status != status::active) @@ -66,16 +73,22 @@ namespace search_tree { m_status = status::open; } - node* left() const { return m_left; } - node* right() const { return m_right; } - node* parent() const { return m_parent; } + node *left() const { + return m_left; + } + node *right() const { + return m_right; + } + node *parent() const { + return m_parent; + } - node* find_active_node() { + node *find_active_node() { if (m_status == status::active) return this; if (m_status != status::open) return nullptr; - node* nodes[2] = { m_left, m_right }; + node *nodes[2] = {m_left, m_right}; for (unsigned i = 0; i < 2; ++i) { auto res = nodes[i] ? nodes[i]->find_active_node() : nullptr; if (res) @@ -86,7 +99,7 @@ namespace search_tree { return nullptr; } - void display(std::ostream& out, unsigned indent) const { + void display(std::ostream &out, unsigned indent) const { for (unsigned i = 0; i < indent; ++i) out << " "; Config::display_literal(out, m_literal); @@ -98,16 +111,18 @@ namespace search_tree { m_right->display(out, indent + 2); } - bool has_core() const { return !m_core.empty(); } - void set_core(vector const &core) { + void set_core(vector const &core) { m_core = core; } - vector const & get_core() const { return m_core; } - void clear_core() { m_core.clear(); } + vector const &get_core() const { + return m_core; + } + void clear_core() { + m_core.clear(); + } }; - template - class tree { + template class tree { typedef typename Config::literal literal; scoped_ptr> m_root = nullptr; literal m_null_literal; @@ -115,7 +130,7 @@ namespace search_tree { // return an active node in the subtree rooted at n, or nullptr if there is none // close nodes that are fully explored (whose children are all closed) - node* activate_from_root(node* n) { + node *activate_from_root(node *n) { if (!n) return nullptr; if (n->get_status() != status::open) @@ -126,7 +141,7 @@ namespace search_tree { n->set_status(status::active); return n; } - node* nodes[2] = { left, right }; + node *nodes[2] = {left, right}; unsigned index = m_rand(2); auto child = activate_from_root(nodes[index]); if (child) @@ -134,145 +149,75 @@ namespace search_tree { child = activate_from_root(nodes[1 - index]); if (child) return child; - if (left && right && left->get_status() == status::closed && right->get_status() == status::closed) - n->set_status(status::closed); + if (left && right && left->get_status() == status::closed && right->get_status() == status::closed) + n->set_status(status::closed); return nullptr; } - // Invariants: - // Cores labeling nodes are subsets of the literals on the path to the node and the (external) assumption literals. - // If a parent is open, then the one of the children is open. - void close_with_core(node* n, vector const &C, bool allow_resolve = true) { - if (!n || n->get_status() == status::closed) - return; + void close(node *n) { + if (!n || n->get_status() == status::closed) + return; + n->set_status(status::closed); + close(n->left()); + close(n->right()); + } - n->set_core(C); - n->set_status(status::closed); + // Invariants: + // Cores labeling nodes are subsets of the literals on the path to the node and the (external) assumption + // literals. If a parent is open, then the one of the children is open. + void close_with_core(node *n, vector const &C) { + if (!n || n->get_status() == status::closed) + return; + node *p = n->parent(); + if (p && all_of(C, [n](auto const &l) { return l != n->get_literal(); })) { + close_with_core(p, C); + return; + } + close(n->left()); + close(n->right()); + n->set_core(C); + n->set_status(status::closed); - close_with_core(n->left(), C, false); - close_with_core(n->right(), C, false); + if (!p) + return; + auto left = p->left(); + auto right = p->right(); + if (!left || !right) + return; - // stop at root - if (!n->parent()) return; + // only attempt when both children are closed and each has a core + if (left->get_status() != status::closed || right->get_status() != status::closed) + return; - node* p = n->parent(); - if (!p) return; // root reached + auto resolvent = compute_sibling_resolvent(left, right); + close_with_core(p, resolvent); + } - auto is_literal_in_core = [](literal const& l, vector const& C) { - for (unsigned i = 0; i < C.size(); ++i) - if (C[i] == l) return true; - return false; - }; + // Given complementary sibling nodes for literals x and ¬x, sibling resolvent = (core_left ∪ core_right) \ {x, + // ¬x} + vector compute_sibling_resolvent(node *left, node *right) { + vector res; - // case 1: current splitting literal not in the conflict core - if (!is_literal_in_core(n->get_literal(), C)) { - close_with_core(p, C); - // case 2: both siblings closed -> resolve - } else if (allow_resolve && p->left()->get_status() == status::closed && p->right()->get_status() == status::closed) { - try_resolve_upwards(p); - } - } + auto &core_l = left->get_core(); + auto &core_r = right->get_core(); - // Given complementary sibling nodes for literals x and ¬x, sibling resolvent = (core_left ∪ core_right) \ {x, ¬x} - vector compute_sibling_resolvent(node* left, node* right) { - vector res; + if (core_l.empty() || core_r.empty() || left->parent() != right->parent()) + return res; - if (!left->has_core() || !right->has_core()) return res; + auto lit_l = left->get_literal(); + auto lit_r = right->get_literal(); - bool are_sibling_complements = left->parent() == right->parent(); - if (!are_sibling_complements) - return res; - - auto &core_l = left->get_core(); - auto &core_r = right->get_core(); - - auto contains = [](vector const &v, literal const &l) { - for (unsigned i = 0; i < v.size(); ++i) - if (v[i] == l) return true; - return false; - }; - - auto lit_l = left->get_literal(); - auto lit_r = right->get_literal(); - - // Add literals from left core, skipping lit_l - for (unsigned i = 0; i < core_l.size(); ++i) { - if (core_l[i] != lit_l && !contains(res, core_l[i])) - res.push_back(core_l[i]); - } - - // Add literals from right core, skipping lit_r - for (unsigned i = 0; i < core_r.size(); ++i) { - if (core_r[i] != lit_r && !contains(res, core_r[i])) - res.push_back(core_r[i]); - } - - return res; - } - - void try_resolve_upwards(node* p) { - while (p) { - auto left = p->left(); - auto right = p->right(); - if (!left || !right) return; - - // only attempt when both children are closed and each has a core - if (left->get_status() != status::closed || right->get_status() != status::closed) return; - if (!left->has_core() || !right->has_core()) return; - - auto resolvent = compute_sibling_resolvent(left, right); - - // empty resolvent of sibling complement (i.e. tautology) -> global UNSAT - if (resolvent.empty()) { - close_with_core(m_root.get(), resolvent, false); - return; - } - - // if p already has the same core, nothing more to do - if (p->has_core() && resolvent == p->get_core()) - return; - - // Bubble to the highest ancestor where ALL literals in the resolvent - // are present somewhere on the path from that ancestor to root - node* candidate = p; - node* attach_here = p; // fallback - - while (candidate) { - bool all_found = true; - - for (auto const& r : resolvent) { - bool found = false; - for (node* q = candidate; q; q = q->parent()) { - if (q->get_literal() == r) { - found = true; - break; - } - } - if (!found) { - all_found = false; - break; - } - } - - if (all_found) { - attach_here = candidate; // bubble up to this node - } - - candidate = candidate->parent(); - } - - // attach the resolvent and close the subtree at attach_here - if (!attach_here->has_core() || attach_here->get_core() != resolvent) { - close_with_core(attach_here, resolvent, false); - } - - // continue upward from parent of attach_here - p = attach_here->parent(); - } - } + for (auto const &lit : core_l) + if (lit != lit_l && !res.contains(lit)) + res.push_back(lit); + for (auto const &lit : core_r) + if (lit != lit_l && !res.contains(lit)) + res.push_back(lit); + return res; + } public: - tree(literal const& null_literal) : m_null_literal(null_literal) { + tree(literal const &null_literal) : m_null_literal(null_literal) { reset(); } @@ -284,38 +229,37 @@ namespace search_tree { m_root = alloc(node, m_null_literal, nullptr); m_root->set_status(status::active); } - + // Split current node if it is active. // After the call, n is open and has two children. - void split(node* n, literal const& a, literal const& b) { + void split(node *n, literal const &a, literal const &b) { n->split(a, b); } // conflict is given by a set of literals. // they are subsets of the literals on the path from root to n AND the external assumption literals - void backtrack(node* n, vector const& conflict) { + void backtrack(node *n, vector const &conflict) { if (conflict.empty()) { close_with_core(m_root.get(), conflict); return; - } + } SASSERT(n != m_root.get()); // all literals in conflict are on the path from root to n // remove assumptions from conflict to ensure this. - DEBUG_CODE( - auto on_path = [&](literal const& a) { - node* p = n; - while (p) { - if (p->get_literal() == a) - return true; - p = p->parent(); - } - return false; - }; - SASSERT(all_of(conflict, [&](auto const& a) { return on_path(a); })); - ); + DEBUG_CODE(auto on_path = + [&](literal const &a) { + node *p = n; + while (p) { + if (p->get_literal() == a) + return true; + p = p->parent(); + } + return false; + }; + SASSERT(all_of(conflict, [&](auto const &a) { return on_path(a); }));); while (n) { - if (any_of(conflict, [&](auto const& a) { return a == n->get_literal(); })) { + if (any_of(conflict, [&](auto const &a) { return a == n->get_literal(); })) { // close the subtree under n (preserves core attached to n), and attempt to resolve upwards close_with_core(n, conflict); return; @@ -327,9 +271,9 @@ namespace search_tree { } // return an active node in the tree, or nullptr if there is none - // first check if there is a node to activate under n, + // first check if there is a node to activate under n, // if not, go up the tree and try to activate a sibling subtree - node* activate_node(node* n) { + node *activate_node(node *n) { if (!n) { if (m_root->get_status() == status::active) return m_root.get(); @@ -341,10 +285,10 @@ namespace search_tree { auto p = n->parent(); while (p) { - if (p->left() && p->left()->get_status() == status::closed && - p->right() && p->right()->get_status() == status::closed) { + if (p->left() && p->left()->get_status() == status::closed && p->right() && + p->right()->get_status() == status::closed) { p->set_status(status::closed); - n = p; + n = p; p = n->parent(); continue; } @@ -358,18 +302,18 @@ namespace search_tree { res = activate_from_root(p->left()); if (res) return res; - } + } n = p; p = n->parent(); } return nullptr; } - node* find_active_node() { + node *find_active_node() { return m_root->find_active_node(); } - vector const& get_core_from_root() const { + vector const &get_core_from_root() const { return m_root->get_core(); } @@ -377,10 +321,9 @@ namespace search_tree { return m_root->get_status() == status::closed; } - std::ostream& display(std::ostream& out) const { + std::ostream &display(std::ostream &out) const { m_root->display(out, 0); return out; } - }; -} \ No newline at end of file +} // namespace search_tree