From 217710627bd440cb28524d014afb5f10058302fd Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 7 Oct 2019 18:37:48 -0700 Subject: New C++ API: Add Term::getId(). (#3360) + use explicit types in NodeValue + add unit test for Term::isParameterized() Co-Authored-By: makaimann --- src/api/cvc4cpp.cpp | 14 ++++++++++---- src/api/cvc4cpp.h | 27 ++++++++++++++++----------- src/expr/expr_template.cpp | 3 ++- src/expr/expr_template.h | 2 +- src/expr/metakind_template.h | 4 ++-- src/expr/node.h | 3 ++- src/expr/node_value.h | 42 ++++++++++++++++++++++++------------------ test/unit/api/term_black.h | 23 +++++++++++++++++++++++ 8 files changed, 80 insertions(+), 38 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 5321cbd95..3ea0fcb01 100644 --- 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 bb7b48f97..49c283b75 100644 --- 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 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); } diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h index e8128ef7e..945944467 100644 --- 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); -- cgit v1.2.3