summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus_sampler.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/sygus_sampler.cpp')
-rw-r--r--src/theory/quantifiers/sygus_sampler.cpp12
1 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index d4720ea7c..36602d3ae 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -323,8 +323,8 @@ bool SygusSampler::isContiguous(Node n)
void SygusSampler::computeFreeVariables(Node n, std::vector<Node>& fvs)
{
- std::unordered_set<TNode, TNodeHashFunction> visited;
- std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+ std::unordered_set<TNode> visited;
+ std::unordered_set<TNode>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
@@ -359,8 +359,8 @@ bool SygusSampler::checkVariables(Node n, bool checkOrder, bool checkLinear)
// compute free variables in n for each type
std::map<unsigned, std::vector<Node> > fvs;
- std::unordered_set<TNode, TNodeHashFunction> visited;
- std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+ std::unordered_set<TNode> visited;
+ std::unordered_set<TNode>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
@@ -411,8 +411,8 @@ bool SygusSampler::containsFreeVariables(Node a, Node b, bool strict)
computeFreeVariables(a, fvs);
std::vector<Node> fv_found;
- std::unordered_set<TNode, TNodeHashFunction> visited;
- std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+ std::unordered_set<TNode> visited;
+ std::unordered_set<TNode>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(b);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback