1 files changed, 39 insertions, 0 deletions
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 30f7ce8b9..b1614f31b 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -15,6 +15,7 @@
  **/
 
 #include "expr/node.h"
+#include "expr/attribute.h"
 #include "util/output.h"
 
 #include <iostream>
@@ -51,4 +52,42 @@ UnknownTypeException::UnknownTypeException(TNode n) throw() :
                                " its type cannot be computed until it is substituted away") {
 }
 
+/** Is this node constant? (and has that been computed yet?) */
+struct IsConstTag { };
+struct IsConstComputedTag { };
+typedef expr::Attribute<IsConstTag, bool> IsConstAttr;
+typedef expr::Attribute<IsConstComputedTag, bool> IsConstComputedAttr;
+
+template <bool ref_count>
+bool NodeTemplate<ref_count>::isConst() const {
+  assertTNodeNotExpired();
+  Debug("isConst") << "Node::isConst() for: " << *this << std::endl;
+  if(isNull()) {
+    return false;
+  }
+  switch(getMetaKind()) {
+  case kind::metakind::CONSTANT:
+    Debug("isConst") << "Node::isConst() returning true, it's a CONSTANT" << std::endl;
+    return true;
+  case kind::metakind::VARIABLE:
+    Debug("isConst") << "Node::isConst() returning false, it's a VARIABLE" << std::endl;
+    return false;
+  default:
+    if(getAttribute(IsConstComputedAttr())) {
+      bool bval = getAttribute(IsConstAttr());
+      Debug("isConst") << "Node::isConst() returning cached value " << (bval ? "true" : "false") << " for: " << *this << std::endl;
+      return bval;
+    } else {
+      bool bval = expr::TypeChecker::computeIsConst(NodeManager::currentNM(), *this);
+      Debug("isConst") << "Node::isConst() computed value " << (bval ? "true" : "false") << " for: " << *this << std::endl;
+      const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstAttr(), bval);
+      const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstComputedAttr(), true);
+      return bval;
+    }
+  }
+}
+
+template bool NodeTemplate<true>::isConst() const;
+template bool NodeTemplate<false>::isConst() const;
+
 }/* CVC4 namespace */