summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/api/cvc4cpp.cpp14
-rw-r--r--src/api/cvc4cpp.h27
-rw-r--r--src/expr/expr_template.cpp3
-rw-r--r--src/expr/expr_template.h2
-rw-r--r--src/expr/metakind_template.h4
-rw-r--r--src/expr/node.h3
-rw-r--r--src/expr/node_value.h42
-rw-r--r--test/unit/api/term_black.h23
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
@@ -576,10 +576,25 @@ 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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback