mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-30 21:57:46 +00:00
Code Activity

simplify contains check

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-01-15 12:01:44 -08:00
parent f5fc7eb173
commit aa6fddf944
1 changed files with 1 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/util/search_tree.h
View file

@ -209,10 +209,7 @@ namespace search_tree {
// If the node is closed AND has a stronger or equal core, we are done. // If the node is closed AND has a stronger or equal core, we are done.
// Otherwise, closed nodes may still accept a different (stronger) core to enable pruning/resolution higher in the tree. // Otherwise, closed nodes may still accept a different (stronger) core to enable pruning/resolution higher in the tree.
auto subseteq = [](vector<literal> const& A, vector<literal> const& B) { auto subseteq = [](vector<literal> const& A, vector<literal> const& B) {
for (auto const& a : A) return all_of(A, [&](auto const &a) { return B.contains(a); });
if (!B.contains(a))
return false;
return true;
}; };
if (n->get_status() == status::closed && subseteq(n->get_core(), C)) if (n->get_status() == status::closed && subseteq(n->get_core(), C))
return; return;