From ce0e796ad92f040fb75435bd7880bc28a60b0374 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 19 Feb 2010 20:29:58 +0000
Subject: * Attribute infrastructure -- static design.  Documentation is
 coming.   See test/unit/expr/node_white.h for use examples, including how to 
  define new attribute kinds.

Also:

* fixes to test infrastructure
* minor changes to code formatting throughout
* attribute tests in test/unit/expr/node_white.h
* fixes to NodeManagerScope ordering
* use NodeValue::getKind() to properly deal with UNDEFINED_KIND
  (removing compiler warning)
* ExprManager: add proper NodeManagerScope to public-facing member
  functions
* store variable names and types in attributes
* SoftNode is a placeholder, not a real implementation
---
 src/expr/node_value.h | 18 +++++++++++++++---
 1 file changed, 15 insertions(+), 3 deletions(-)

(limited to 'src/expr/node_value.h')

diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index d86822b8d..2d84967c6 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -51,6 +51,12 @@ class NodeValue {
    *  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;
+
+  /** A mask for d_kind */
+  static const unsigned kindMask = (1u << KINDBITS) - 1;
+
   // this header fits into one 64-bit word
 
   /** The ID (0 is reserved for the null value) */
@@ -60,7 +66,7 @@ class NodeValue {
   unsigned d_rc        :  8;
 
   /** Kind of the expression */
-  unsigned d_kind      :  8;
+  unsigned d_kind      : KINDBITS;
 
   /** Number of children */
   unsigned d_nchildren : 16;
@@ -178,13 +184,19 @@ public:
     }
   };
 
-
   unsigned getId() const { return d_id; }
-  Kind getKind() const { return (Kind) d_kind; }
+  Kind getKind() const { return dKindToKind(d_kind); }
   unsigned getNumChildren() const { return d_nchildren; }
 
   std::string toString() const;
   void toStream(std::ostream& out) const;
+
+  static inline unsigned kindToDKind(Kind k) {
+    return ((unsigned) k) & kindMask;
+  }
+  static inline Kind dKindToKind(unsigned d) {
+    return (d == kindMask) ? UNDEFINED_KIND : Kind(d);
+  }
 };
 
 }/* CVC4::expr namespace */
-- 
cgit v1.2.3