diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-03-25 20:20:29 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-03-25 20:20:29 +0000 |
| commit | 56837b30117fda75298138cdd052e0c5ba201b86 (patch) | |
| tree | b96d684f9926ea49c2b39e6193a8925f95d0287d /src/theory/uf | |
| parent | e3e0b625862ba23ba97eb72fcdd3811448ad855a (diff) | |
Adding comments to NodeManager
Minor name changes for cleanup and hash function templates
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 2 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf.h | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index ee3cb4734..cd477a910 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -54,7 +54,7 @@ void TheoryUF::registerTerm(TNode n){ ECData* ecN; - if(n.hasAttribute(ECAttr(), ecN)){ + if(n.getAttribute(ECAttr(), ecN)){ /* registerTerm(n) is only called when a node has not been seen in the * current context. ECAttr() is not a context-dependent attribute. * When n.hasAttribute(ECAttr(),...) is true on a registerTerm(n) call, diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index ccbfa327a..9e57311b5 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -182,7 +182,7 @@ private: * Cleanup function for ECData. This will be used for called whenever * a ECAttr is being destructed. */ -struct ECCleanupFcn{ +struct ECCleanupStrategy{ static void cleanup(ECData* ec){ Debug("ufgc") << "cleaning up ECData " << ec << "\n"; ec->deleteSelf(); @@ -195,7 +195,7 @@ struct EquivClass; /** * ECAttr is the attribute that maps a node to an equivalence class. */ -typedef expr::Attribute<EquivClass, ECData*, ECCleanupFcn > ECAttr; +typedef expr::Attribute<EquivClass, ECData*, ECCleanupStrategy > ECAttr; } /* CVC4::theory::uf namespace */ } /* CVC4::theory namespace */ |