diff options
Diffstat (limited to 'src/theory/quantifiers/single_inv_partition.cpp')
| -rw-r--r-- | src/theory/quantifiers/single_inv_partition.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp index cc11d884c..05492b5b7 100644 --- a/src/theory/quantifiers/single_inv_partition.cpp +++ b/src/theory/quantifiers/single_inv_partition.cpp @@ -285,7 +285,7 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs, Trace("si-prt-debug") << "...normalized invocations to " << cr << std::endl; // now must check if it has other bound variables - std::unordered_set<Node, NodeHashFunction> fvs; + std::unordered_set<Node> fvs; expr::getFreeVariables(cr, fvs); // bound variables must be contained in the single invocation variables for (const Node& bv : fvs) @@ -316,7 +316,7 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs, Trace("si-prt") << "...not single invocation." << std::endl; singleInvocation = false; // rename bound variables with maximal overlap with si_vars - std::unordered_set<Node, NodeHashFunction> fvs; + std::unordered_set<Node> fvs; expr::getFreeVariables(cr, fvs); std::vector<Node> termsNs; std::vector<Node> subsNs; @@ -349,7 +349,7 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs, Trace("si-prt") << ".....got si=" << singleInvocation << ", result : " << cr << std::endl; d_conjuncts[2].push_back(cr); - std::unordered_set<Node, NodeHashFunction> fvs; + std::unordered_set<Node> fvs; expr::getFreeVariables(cr, fvs); d_all_vars.insert(fvs.begin(), fvs.end()); if (singleInvocation) |