some things I had laying around in a directory but never got committed; minor fix-ups to documentation and some node stuff

1 files changed, 6 insertions, 0 deletions

diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index f2da42731..2c11b58d5 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -290,6 +290,7 @@ public:
   template <class T>
   inline const T& getConst() const;
 
+  NodeValue* getOperator() const;
   NodeValue* getChild(int i) const;
 
   void printAst(std::ostream& out, int indent = 0) const;
@@ -432,6 +433,11 @@ inline bool NodeValue::isBeingDeleted() const {
     NodeManager::currentNM()->isCurrentlyDeleting(this);
 }
 
+inline NodeValue* NodeValue::getOperator() const {
+  Assert(getMetaKind() == kind::metakind::PARAMETERIZED);
+  return d_children[0];
+}
+
 inline NodeValue* NodeValue::getChild(int i) const {
   if(getMetaKind() == kind::metakind::PARAMETERIZED) {
     ++i;