diff options
| author | Tim King <taking@google.com> | 2016-11-06 16:05:29 -0800 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2016-11-06 16:06:53 -0800 |
| commit | 8be2d02f510e329d88e38889720334c277bf268c (patch) | |
| tree | 60ffaa576d6a63beafc8ac8c5ea3d66f59f67b0b /src/expr/metakind_template.h | |
| parent | 4961abfa9bec88a2e15fc3078e2bd8a5bb258f93 (diff) | |
This switches the ZombieSet in the NodeManager to use NodeValue's id for equality comparison. The previously used function NodeValueEq incorrectly identified VARIABLE nodes as being equal. This meant that on hash collisions these nodes could leak memory.
Diffstat (limited to 'src/expr/metakind_template.h')
| -rw-r--r-- | src/expr/metakind_template.h | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 9025aa02a..75521e901 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -150,13 +150,6 @@ static const unsigned MAX_CHILDREN = namespace expr { // Comparison predicate -struct NodeValueEq { - inline bool operator()(const NodeValue* nv1, const NodeValue* nv2) const { - return ::CVC4::kind::metakind::NodeValueCompare::compare<false>(nv1, nv2); - } -}; - -// Comparison predicate struct NodeValuePoolEq { inline bool operator()(const NodeValue* nv1, const NodeValue* nv2) const { return ::CVC4::kind::metakind::NodeValueCompare::compare<true>(nv1, nv2); @@ -345,7 +338,7 @@ ${metakind_operatorKinds} }/* CVC4::kind namespace */ -#line 349 "${template}" +#line 341 "${template}" namespace theory { |