New C++ API: Add Term::getId(). (#3360)

+ use explicit types in NodeValue
+ add unit test for Term::isParameterized()

Co-Authored-By: makaimann <makaim@stanford.edu>

5 files changed, 31 insertions, 23 deletions

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 04466a4c6..2338a7320 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -371,7 +371,8 @@ bool Expr::operator>(const Expr& e) const {
   return *d_node > *e.d_node;
 }
 
-unsigned long Expr::getId() const {
+uint64_t Expr::getId() const
+{
   ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
   return d_node->getId();
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index d03efdd52..2c52e5b72 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -326,7 +326,7 @@ public:
    * @return an identifier uniquely identifying the value this
    * expression holds.
    */
-  unsigned long getId() const;
+  uint64_t getId() const;
 
   /**
    * Returns the kind of the expression (AND, PLUS ...).
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 3550acf05..c651a5f28 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -123,8 +123,8 @@ namespace metakind {
 #define CVC4__EXPR__NODE_VALUE__NBITS__ID 40
 #define CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN 26
 
-static const unsigned MAX_CHILDREN =
-  (1u << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1;
+static const uint32_t MAX_CHILDREN =
+    (((uint32_t)1) << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1;
 
 }/* CVC4::kind::metakind namespace */
 }/* CVC4::kind namespace */
diff --git a/src/expr/node.h b/src/expr/node.h
index b8a665f0c..e0231bef6 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -476,7 +476,8 @@ public:
    * Returns the unique id of this node
    * @return the ud
    */
-  unsigned long getId() const {
+  uint64_t getId() const
+  {
     assertTNodeNotExpired();
     return d_nv->getId();
   }
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 024a13941..0174bdd15 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -70,18 +70,19 @@ namespace expr {
  * This is a NodeValue.
  */
 class NodeValue {
-
-  static const unsigned NBITS_REFCOUNT = CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT;
-  static const unsigned NBITS_KIND = CVC4__EXPR__NODE_VALUE__NBITS__KIND;
-  static const unsigned NBITS_ID = CVC4__EXPR__NODE_VALUE__NBITS__ID;
-  static const unsigned NBITS_NCHILDREN = CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN;
+  static const uint32_t NBITS_REFCOUNT =
+      CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT;
+  static const uint32_t NBITS_KIND = CVC4__EXPR__NODE_VALUE__NBITS__KIND;
+  static const uint32_t NBITS_ID = CVC4__EXPR__NODE_VALUE__NBITS__ID;
+  static const uint32_t NBITS_NCHILDREN =
+      CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN;
 
   /** Maximum reference count possible.  Used for sticky
    *  reference-counting.  Should be (1 << num_bits(d_rc)) - 1 */
-  static const unsigned MAX_RC = (1u << NBITS_REFCOUNT) - 1;
+  static const uint32_t MAX_RC = (((uint32_t)1) << NBITS_REFCOUNT) - 1;
 
   /** A mask for d_kind */
-  static const unsigned kindMask = (1u << NBITS_KIND) - 1;
+  static const uint32_t kindMask = (((uint32_t)1) << NBITS_KIND) - 1;
 
   // This header fits into 96 bits
 
@@ -89,13 +90,13 @@ class NodeValue {
   uint64_t d_id        : NBITS_ID;
 
   /** The expression's reference count.  @see cvc4::Node. */
-  uint64_t d_rc        : NBITS_REFCOUNT;
+  uint32_t d_rc : NBITS_REFCOUNT;
 
   /** Kind of the expression */
-  uint64_t d_kind      : NBITS_KIND;
+  uint32_t d_kind : NBITS_KIND;
 
   /** Number of children */
-  uint64_t d_nchildren : NBITS_NCHILDREN;
+  uint32_t d_nchildren : NBITS_NCHILDREN;
 
   /** Variable number of child nodes */
   NodeValue* d_children[0];
@@ -252,13 +253,16 @@ public:
     return hash;
   }
 
-  unsigned long getId() const { return d_id; }
+  uint64_t getId() const { return d_id; }
+
   Kind getKind() const { return dKindToKind(d_kind); }
+
   kind::MetaKind getMetaKind() const { return kind::metaKindOf(getKind()); }
-  unsigned getNumChildren() const {
-    return (getMetaKind() == kind::metakind::PARAMETERIZED)
-      ? d_nchildren - 1
-      : d_nchildren;
+
+  uint32_t getNumChildren() const
+  {
+    return (getMetaKind() == kind::metakind::PARAMETERIZED) ? d_nchildren - 1
+                                                            : d_nchildren;
   }
 
   unsigned getRefCount() const { return d_rc; }
@@ -267,11 +271,13 @@ public:
   void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
                 OutputLanguage = language::output::LANG_AUTO) const;
 
-  static inline unsigned kindToDKind(Kind k) {
-    return ((unsigned) k) & kindMask;
+  static inline uint32_t kindToDKind(Kind k)
+  {
+    return ((uint32_t)k) & kindMask;
   }
 
-  static inline Kind dKindToKind(unsigned d) {
+  static inline Kind dKindToKind(uint32_t d)
+  {
     return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d);
   }