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>

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 5321cbd95b213bca9daba86115abe804577b4df0..3ea0fcb017ad628c2c60a923fffa03022f6df457 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1044,16 +1044,16 @@ bool Term::operator==(const Term& t) const { return *d_expr == *t.d_expr; }
 
 bool Term::operator!=(const Term& t) const { return *d_expr != *t.d_expr; }
 
-Kind Term::getKind() const
+uint64_t Term::getId() const
 {
   CVC4_API_CHECK_NOT_NULL;
-  return intToExtKind(d_expr->getKind());
+  return d_expr->getId();
 }
 
-bool Term::isParameterized() const
+Kind Term::getKind() const
 {
   CVC4_API_CHECK_NOT_NULL;
-  return d_expr->isParameterized();
+  return intToExtKind(d_expr->getKind());
 }
 
 Sort Term::getSort() const
@@ -1064,6 +1064,12 @@ Sort Term::getSort() const
 
 bool Term::isNull() const { return d_expr->isNull(); }
 
+bool Term::isParameterized() const
+{
+  CVC4_API_CHECK_NOT_NULL;
+  return d_expr->isParameterized();
+}
+
 Term Term::notTerm() const
 {
   try

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index bb7b48f97d04e3c335442ad431e46e01a839f1f7..49c283b757f012130da3b36b50868173ab769125 100644 (file)
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -575,11 +575,26 @@ class CVC4_PUBLIC Term
    */
   bool operator!=(const Term& t) const;
 
+  /**
+   * @return the id of this term
+   */
+  uint64_t getId() const;
+
   /**
    * @return the kind of this term
    */
   Kind getKind() const;
-  
+
+  /**
+   * @return the sort of this term
+   */
+  Sort getSort() const;
+
+  /**
+   * @return true if this Term is a null term
+   */
+  bool isNull() const;
+
   /**
    * @return true if this expression is parameterized.
    *
@@ -596,16 +611,6 @@ class CVC4_PUBLIC Term
    *   mkTerm(t.getKind(), b1, ..., bn )
    */
   bool isParameterized() const;
-  
-  /**
-   * @return the sort of this term
-   */
-  Sort getSort() const;
-
-  /**
-   * @return true if this Term is a null term
-   */
-  bool isNull() const;
 
   /**
    * Boolean negation.

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 04466a4c6933086d9bc62cf338aaeff0801d4a6f..2338a73200384a15654bd5c7bc8208b828a398b2 100644 (file)
--- 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 d03efdd52574d69d18512bfb27a66cd613ef6a40..2c52e5b7237a1a6cb0d6efe30f0bec36e6b61956 100644 (file)
--- 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 3550acf055b96cb447fb410b3be7f48273de8c86..c651a5f28ecc4ef00d92d71d9a81f99beb2fc016 100644 (file)
--- 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 b8a665f0ce80bdfd07de3fd6cc6405fc1bc65d9c..e0231bef68df3d59e281c29b58bf78b3b886dcd6 100644 (file)
--- 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 024a13941726688ce37348f4cf3ca59d35e3153a..0174bdd15d1e5d02035fd7f9d970631314b38d6b 100644 (file)
--- 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);
   }
 

diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index e8128ef7e17a4f2cb30e043c56f508b6a00441a7..945944467ba496bc9a73c536e9e25db98906a524 100644 (file)
--- a/test/unit/api/term_black.h
+++ b/test/unit/api/term_black.h
@@ -25,9 +25,11 @@ class TermBlack : public CxxTest::TestSuite
   void tearDown() override {}
 
   void testEq();
+  void testGetId();
   void testGetKind();
   void testGetSort();
   void testIsNull();
+  void testIsParameterized();
   void testNotTerm();
   void testAndTerm();
   void testOrTerm();
@@ -57,6 +59,19 @@ void TermBlack::testEq()
   TS_ASSERT(x != z);
 }
 
+void TermBlack::testGetId()
+{
+  Term n;
+  TS_ASSERT_THROWS(n.getId(), CVC4ApiException&);
+  Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x");
+  TS_ASSERT_THROWS_NOTHING(x.getId());
+  Term y = x;
+  TS_ASSERT_EQUALS(x.getId(), y.getId());
+
+  Term z = d_solver.mkVar(d_solver.getIntegerSort(), "z");
+  TS_ASSERT_DIFFERS(x.getId(), z.getId());
+}
+
 void TermBlack::testGetKind()
 {
   Sort uSort = d_solver.mkUninterpretedSort("u");
@@ -173,6 +188,14 @@ void TermBlack::testNotTerm()
   TS_ASSERT_THROWS_NOTHING(p_f_x.notTerm());
 }
 
+void TermBlack::testIsParameterized()
+{
+  Term n;
+  TS_ASSERT_THROWS(n.isParameterized(), CVC4ApiException&);
+  Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x");
+  TS_ASSERT_THROWS_NOTHING(x.isParameterized());
+}
+
 void TermBlack::testAndTerm()
 {
   Sort bvSort = d_solver.mkBitVectorSort(8);