summaryrefslogtreecommitdiff
path: root/src/expr/node_value.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/node_value.h')
-rw-r--r--src/expr/node_value.h162
1 files changed, 100 insertions, 62 deletions
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 995a63180..7dd90913f 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -19,12 +19,15 @@
#include "cvc4_private.h"
+// circular dependency
+#include "expr/metakind.h"
+
#ifndef __CVC4__EXPR__NODE_VALUE_H
#define __CVC4__EXPR__NODE_VALUE_H
#include "cvc4_config.h"
-#include <stdint.h>
#include "expr/kind.h"
+#include <stdint.h>
#include <string>
#include <iterator>
@@ -40,8 +43,25 @@ class PlusNodeBuilder;
class MultNodeBuilder;
class NodeManager;
+namespace kind {
+ namespace metakind {
+ template < ::CVC4::Kind k, bool pool >
+ struct NodeValueConstCompare;
+
+ struct NodeValueCompare;
+ struct NodeValueConstPrinter;
+ }/* CVC4::kind::metakind namespace */
+}/* CVC4::kind namespace */
+
namespace expr {
+#if __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT + \
+ __CVC4__EXPR__NODE_VALUE__NBITS__KIND + \
+ __CVC4__EXPR__NODE_VALUE__NBITS__ID + \
+ __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN != 64
+# error NodeValue header bit assignment does not sum to 64 !
+#endif /* sum != 64 */
+
/**
* This is an NodeValue.
*/
@@ -50,39 +70,47 @@ class NodeValue {
/** A convenient null-valued expression value */
static NodeValue s_null;
+ 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;
+
/** Maximum reference count possible. Used for sticky
* reference-counting. Should be (1 << num_bits(d_rc)) - 1 */
- static const unsigned MAX_RC = 255;
-
- /** Number of bits assigned to the kind in the NodeValue header */
- static const unsigned KINDBITS = 8;
+ static const unsigned MAX_RC = (1u << NBITS_REFCOUNT) - 1;
/** A mask for d_kind */
- static const unsigned kindMask = (1u << KINDBITS) - 1;
+ static const unsigned kindMask = (1u << NBITS_KIND) - 1;
// this header fits into one 64-bit word
/** The ID (0 is reserved for the null value) */
- unsigned d_id : 32;
+ unsigned d_id : NBITS_ID;
/** The expression's reference count. @see cvc4::Node. */
- unsigned d_rc : 8;
+ unsigned d_rc : NBITS_REFCOUNT;
/** Kind of the expression */
- unsigned d_kind : KINDBITS;
+ unsigned d_kind : NBITS_KIND;
/** Number of children */
- unsigned d_nchildren : 16;
+ unsigned d_nchildren : NBITS_NCHILDREN;
/** Variable number of child nodes */
NodeValue* d_children[0];
// todo add exprMgr ref in debug case
- template <bool> friend class CVC4::NodeTemplate;
- template <class Builder> friend class CVC4::NodeBuilderBase;
- template <unsigned nchild_thresh> friend class CVC4::NodeBuilder;
- friend class CVC4::NodeManager;
+ template <bool> friend class ::CVC4::NodeTemplate;
+ template <class Builder> friend class ::CVC4::NodeBuilderBase;
+ template <unsigned nchild_thresh> friend class ::CVC4::NodeBuilder;
+ friend class ::CVC4::NodeManager;
+
+ template <Kind k, bool pool>
+ friend struct ::CVC4::kind::metakind::NodeValueConstCompare;
+
+ friend struct ::CVC4::kind::metakind::NodeValueCompare;
+ friend struct ::CVC4::kind::metakind::NodeValueConstPrinter;
void inc();
void dec();
@@ -146,14 +174,10 @@ private:
public:
template <bool ref_count>
- iterator<ref_count> begin() const {
- return iterator<ref_count>(d_children);
- }
+ inline iterator<ref_count> begin() const;
template <bool ref_count>
- iterator<ref_count> end() const {
- return iterator<ref_count>(d_children + d_nchildren);
- }
+ inline iterator<ref_count> end() const;
/**
* Hash this NodeValue. For hash_maps, hash_sets, etc.. but this is
@@ -162,7 +186,11 @@ public:
* collisions for all VARIABLEs.
* @return the hash value of this expression.
*/
- size_t internalHash() const {
+ size_t poolHash() const {
+ if(getMetaKind() == kind::metakind::CONSTANT) {
+ return kind::metakind::NodeValueCompare::constHash(this);
+ }
+
size_t hash = d_kind;
const_nv_iterator i = nv_begin();
const_nv_iterator i_end = nv_end();
@@ -173,43 +201,17 @@ public:
return hash;
}
- inline bool compareTo(const NodeValue* nv) const {
- if(d_kind != nv->d_kind) {
- return false;
- }
-
- if(d_nchildren != nv->d_nchildren) {
- return false;
- }
-
- const_nv_iterator i = nv_begin();
- const_nv_iterator j = nv->nv_begin();
- const_nv_iterator i_end = nv_end();
-
- while(i != i_end) {
- if((*i) != (*j)) {
- return false;
- }
- ++i;
- ++j;
- }
-
- return true;
- }
-
- // Comparison predicate
- struct NodeValueEq {
- bool operator()(const NodeValue* nv1, const NodeValue* nv2) const {
- return nv1->compareTo(nv2);
- }
- };
-
unsigned getId() const { return d_id; }
Kind getKind() const { return dKindToKind(d_kind); }
- unsigned getNumChildren() const { return d_nchildren; }
+ kind::MetaKind getMetaKind() const { return kind::metaKindOf(getKind()); }
+ unsigned getNumChildren() const {
+ return (getMetaKind() == kind::metakind::PARAMETERIZED)
+ ? d_nchildren - 1
+ : d_nchildren;
+ }
std::string toString() const;
- void toStream(std::ostream& out) const;
+ void toStream(std::ostream& out, int toDepth = -1) const;
static inline unsigned kindToDKind(Kind k) {
return ((unsigned) k) & kindMask;
@@ -223,19 +225,27 @@ public:
return s_null;
}
+ /**
+ * If this is a CONST_* Node, extract the constant from it.
+ */
+ template <class T>
+ inline const T& getConst() const;
+
+ NodeValue* getChild(int i) const;
+
};/* class NodeValue */
/**
* For hash_maps, hash_sets, etc.. but this is for expr package
* internal use only at present! This is likely to be POORLY
- * PERFORMING for other uses! NodeValue::internalHash() will lead to
+ * PERFORMING for other uses! NodeValue::poolHash() will lead to
* collisions for all VARIABLEs.
*/
-struct NodeValueInternalHashFunction {
+struct NodeValuePoolHashFcn {
inline size_t operator()(const NodeValue* nv) const {
- return (size_t) nv->internalHash();
+ return (size_t) nv->poolHash();
}
-};/* struct NodeValueInternalHashFunction */
+};/* struct NodeValuePoolHashFcn */
/**
* For hash_maps, hash_sets, etc.
@@ -244,12 +254,14 @@ struct NodeValueIDHashFunction {
inline size_t operator()(const NodeValue* nv) const {
return (size_t) nv->getId();
}
-};/* struct NodeValueHashFcn */
+};/* struct NodeValueIDHashFcn */
+
+inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv);
}/* CVC4::expr namespace */
}/* CVC4 namespace */
-#include "node_manager.h"
+#include "expr/node_manager.h"
namespace CVC4 {
namespace expr {
@@ -306,13 +318,34 @@ inline NodeValue::const_nv_iterator NodeValue::nv_end() const {
return d_children + d_nchildren;
}
+template <bool ref_count>
+inline NodeValue::iterator<ref_count> NodeValue::begin() const {
+ NodeValue* const* firstChild = d_children;
+ if(getMetaKind() == kind::metakind::PARAMETERIZED) {
+ ++firstChild;
+ }
+ return iterator<ref_count>(firstChild);
+}
+
+template <bool ref_count>
+inline NodeValue::iterator<ref_count> NodeValue::end() const {
+ return iterator<ref_count>(d_children + d_nchildren);
+}
-inline bool NodeValue::isBeingDeleted() const
-{
+inline bool NodeValue::isBeingDeleted() const {
return NodeManager::currentNM() != NULL &&
NodeManager::currentNM()->isCurrentlyDeleting(this);
}
+inline NodeValue* NodeValue::getChild(int i) const {
+ if(getMetaKind() == kind::metakind::PARAMETERIZED) {
+ ++i;
+ }
+
+ Assert(i >= 0 && unsigned(i) < d_nchildren);
+ return d_children[i];
+}
+
}/* CVC4::expr namespace */
}/* CVC4 namespace */
@@ -326,6 +359,11 @@ inline CVC4::NodeTemplate<ref_count> NodeValue::iterator<ref_count>::operator*()
return NodeTemplate<ref_count>(*d_i);
}
+inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) {
+ nv.toStream(out, Node::setdepth::getDepth(out));
+ return out;
+}
+
}/* CVC4::expr namespace */
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback