diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/metakind_template.h | 9 | ||||
-rw-r--r-- | src/expr/node_manager.h | 4 | ||||
-rw-r--r-- | src/expr/node_value.h | 12 |
3 files changed, 15 insertions, 10 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 { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 0b3830f4b..aaffeb322 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -96,7 +96,7 @@ class NodeManager { expr::NodeValuePoolEq> NodeValuePool; typedef __gnu_cxx::hash_set<expr::NodeValue*, expr::NodeValueIDHashFunction, - expr::NodeValueEq> ZombieSet; + expr::NodeValueIDEquality> ZombieSet; static CVC4_THREADLOCAL(NodeManager*) s_current; @@ -268,7 +268,7 @@ class NodeManager { Debug("gc") << (d_inReclaimZombies ? " [CURRENTLY-RECLAIMING]" : "") << std::endl; } - d_zombies.insert(nv);// FIXME multithreading + d_zombies.insert(nv); // FIXME multithreading if(safeToReclaimZombies()) { if(d_zombies.size() > 5000) { diff --git a/src/expr/node_value.h b/src/expr/node_value.h index fbf3ff76e..b403d0c86 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -372,6 +372,18 @@ struct NodeValueIDHashFunction { } };/* struct NodeValueIDHashFunction */ + +/** + * An equality predicate that is applicable between pointers to fully + * constructed NodeValues. + */ +struct NodeValueIDEquality { + inline bool operator()(const NodeValue* a, const NodeValue* b) const { + return a->getId() == b->getId(); + } +}; + + inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv); }/* CVC4::expr namespace */ |