diff options
Diffstat (limited to 'src/theory/quantifiers/cegqi/nested_qe.cpp')
| -rw-r--r-- | src/theory/quantifiers/cegqi/nested_qe.cpp | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/theory/quantifiers/cegqi/nested_qe.cpp b/src/theory/quantifiers/cegqi/nested_qe.cpp index 6ae5cf546..a20c37043 100644 --- a/src/theory/quantifiers/cegqi/nested_qe.cpp +++ b/src/theory/quantifiers/cegqi/nested_qe.cpp @@ -55,8 +55,7 @@ bool NestedQe::hasProcessed(Node q) const return d_qnqe.find(q) != d_qnqe.end(); } -bool NestedQe::getNestedQuantification( - Node q, std::unordered_set<Node, NodeHashFunction>& nqs) +bool NestedQe::getNestedQuantification(Node q, std::unordered_set<Node>& nqs) { expr::getKindSubterms(q[1], kind::FORALL, true, nqs); return !nqs.empty(); @@ -64,7 +63,7 @@ bool NestedQe::getNestedQuantification( bool NestedQe::hasNestedQuantification(Node q) { - std::unordered_set<Node, NodeHashFunction> nqs; + std::unordered_set<Node> nqs; return getNestedQuantification(q, nqs); } @@ -79,7 +78,7 @@ Node NestedQe::doNestedQe(Node q, bool keepTopLevel) inputExists = true; } Assert(q.getKind() == kind::FORALL); - std::unordered_set<Node, NodeHashFunction> nqs; + std::unordered_set<Node> nqs; if (!getNestedQuantification(q, nqs)) { Trace("cegqi-nested-qe-debug") |