diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-19 20:29:58 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-19 20:29:58 +0000 |
commit | ce0e796ad92f040fb75435bd7880bc28a60b0374 (patch) | |
tree | 00a390f0347a30978b482cbbb6e074c6dc5a99d2 /src/expr/node_value.h | |
parent | 34b455b1d74fdc06dd2f874fa2bc8d73127fbedf (diff) |
* 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
Diffstat (limited to 'src/expr/node_value.h')
-rw-r--r-- | src/expr/node_value.h | 18 |
1 files changed, 15 insertions, 3 deletions
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 */ |