fix uses of getMetaKind() from outside the expr package. (they now use isConst() and isVar() as appropriate)

also some base infrastructure for the new ::isConst().

8 files changed, 88 insertions, 13 deletions

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index c70fed889..f88914fd2 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -114,9 +114,9 @@ namespace expr {
 static Node exportConstant(TNode n, NodeManager* to);
 
 Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap) {
-  if(n.getMetaKind() == kind::metakind::CONSTANT) {
+  if(n.isConst()) {
     return exportConstant(n, NodeManager::fromExprManager(to));
-  } else if(n.getMetaKind() == kind::metakind::VARIABLE) {
+  } else if(n.isVar()) {
     Expr from_e(from, new Node(n));
     Expr& to_e = vmap.d_typeMap[from_e];
     if(! to_e.isNull()) {
@@ -522,7 +522,7 @@ ${getConst_implementations}
 namespace expr {
 
 static Node exportConstant(TNode n, NodeManager* to) {
-  Assert(n.getMetaKind() == kind::metakind::CONSTANT);
+  Assert(n.isConst());
   switch(n.getKind()) {
 ${exportConstant_cases}
 
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 8b21814dc..28a47d84d 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -62,6 +62,9 @@ mkConst_instantiations=
 mkConst_implementations=
 exportConstant_cases=
 
+typerules=
+construles=
+
 seen_theory=false
 seen_theory_builtin=false
 
@@ -139,6 +142,16 @@ function typerule {
 "
 }
 
+function construle {
+  # isconst OPERATOR isconst-checking-class
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+  construles="${construles}
+  case kind::$1:
+    return $2::computeIsConst(nodeManager, n);
+"
+}
+
 function sort {
   # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"]
   lineno=${BASH_LINENO[0]}
@@ -262,6 +275,7 @@ for var in \
     exportConstant_cases \
     typechecker_includes \
     typerules \
+    construles \
     ; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
 done
diff --git a/src/expr/mkkind b/src/expr/mkkind
index 89e77754f..88c28d4b9 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -142,6 +142,12 @@ function typerule {
   check_theory_seen
 }
 
+function construle {
+  # construle OPERATOR isconst-checking-class
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
 function rewriter {
   # properties prop*
   lineno=${BASH_LINENO[0]}
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 654a1f94f..5608d2972 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -117,6 +117,12 @@ function typerule {
   check_theory_seen
 }
 
+function construle {
+  # construle OPERATOR isconst-checking-class
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
 function rewriter {
   # rewriter class header
   lineno=${BASH_LINENO[0]}
diff --git a/src/expr/node.h b/src/expr/node.h
index b0fda3354..cada443a1 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -442,10 +442,7 @@ public:
    * Returns true if this node represents a constant
    * @return true if const
    */
-  inline bool isConst() const {
-    assertTNodeNotExpired();
-    return getMetaKind() == kind::metakind::CONSTANT;
-  }
+  inline bool isConst() const;
 
   /**
    * Returns true if this node represents a constant
@@ -917,6 +914,7 @@ inline std::ostream& operator<<(std::ostream& out,
 
 #include "expr/attribute.h"
 #include "expr/node_manager.h"
+#include "expr/type_checker.h"
 
 namespace CVC4 {
 
@@ -1263,6 +1261,36 @@ TypeNode NodeTemplate<ref_count>::getType(bool check) const
   return NodeManager::currentNM()->getType(*this, check);
 }
 
+/** 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>
+inline bool
+NodeTemplate<ref_count>::isConst() const {
+  assertTNodeNotExpired();
+  if(isNull()) {
+    return false;
+  }
+  switch(getMetaKind()) {
+  case kind::metakind::CONSTANT:
+    return true;
+  case kind::metakind::VARIABLE:
+    return false;
+  default:
+    if(getAttribute(IsConstComputedAttr())) {
+      return getAttribute(IsConstAttr());
+    } else {
+      bool bval = expr::TypeChecker::computeIsConst(NodeManager::currentNM(), *this);
+      const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstAttr(), bval);
+      const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstComputedAttr(), true);
+      return bval;
+    }
+  }
+}
+
 template <bool ref_count>
 inline Node
 NodeTemplate<ref_count>::substitute(TNode node, TNode replacement) const {
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 501a0f4fd..ce6a91483 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -54,8 +54,8 @@ class TypeChecker;
 // Definition of an attribute for the variable name.
 // TODO: hide this attribute behind a NodeManager interface.
 namespace attr {
-  struct VarNameTag {};
-  struct SortArityTag {};
+  struct VarNameTag { };
+  struct SortArityTag { };
 }/* CVC4::expr::attr namespace */
 
 typedef Attribute<attr::VarNameTag, std::string> VarNameAttr;
@@ -230,8 +230,8 @@ class NodeManager {
   };/* struct NodeManager::NVStorage<N> */
 
   // attribute tags
-  struct TypeTag {};
-  struct TypeCheckedTag;
+  struct TypeTag { };
+  struct TypeCheckedTag { };
 
   // NodeManager's attributes.  These aren't exposed outside of this
   // class; use the getters.
diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h
index 0c8093469..f198e33ca 100644
--- a/src/expr/type_checker.h
+++ b/src/expr/type_checker.h
@@ -18,11 +18,12 @@
 
 #include "cvc4_private.h"
 
+// ordering dependence
+#include "expr/node.h"
+
 #ifndef __CVC4__EXPR__TYPE_CHECKER_H
 #define __CVC4__EXPR__TYPE_CHECKER_H
 
-#include "expr/node.h"
-
 namespace CVC4 {
 namespace expr {
 
@@ -32,6 +33,9 @@ public:
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check = false)
     throw (TypeCheckingExceptionPrivate, AssertionException);
 
+  static bool computeIsConst(NodeManager* nodeManager, TNode n)
+    throw (AssertionException);
+
 };/* class TypeChecker */
 
 }/* CVC4::expr namespace */
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index 2791376b5..9359a6ab8 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -62,5 +62,22 @@ ${typerules}
 
 }/* TypeChecker::computeType */
 
+bool TypeChecker::computeIsConst(NodeManager* nodeManager, TNode n)
+  throw (AssertionException) {
+
+  Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED);
+
+  switch(n.getKind()) {
+${construles}
+
+#line 74 "${template}"
+
+  default:;
+  }
+
+  return false;
+
+}/* TypeChecker::computeIsConst */
+
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */