diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-17 17:11:35 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-17 17:11:35 +0000 |
commit | 73d8c7a4f4896455fef39c44c80bf3df30a52d89 (patch) | |
tree | 9a515d8f3290f2842ab8ec4ae66433bbfb5c529e /src/expr/expr_value.h | |
parent | 105503064be6a198dd864d1e95d6d79e1af51d25 (diff) |
from meeting
Diffstat (limited to 'src/expr/expr_value.h')
-rw-r--r-- | src/expr/expr_value.h | 75 |
1 files changed, 75 insertions, 0 deletions
diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h new file mode 100644 index 000000000..5f90533ed --- /dev/null +++ b/src/expr/expr_value.h @@ -0,0 +1,75 @@ +/********************* -*- C++ -*- */ +/** expr_value.h + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** An expression node. + ** + ** Instances of this class are generally referenced through + ** cvc4::Expr rather than by pointer; cvc4::Expr maintains the + ** reference count on ExprValue instances and + **/ + +#ifndef __CVC4_EXPR_VALUE_H +#define __CVC4_EXPR_VALUE_H + +#include <stdint.h> +#include "cvc4_expr.h" + +namespace CVC4 { + +/** + * This is an ExprValue. + */ +class ExprValue { + /** Maximum reference count possible. Used for sticky + * reference-counting. Should be (1 << num_bits(d_rc)) - 1 */ + static const unsigned MAX_RC = 255; + + // this header fits into one 64-bit word + + /** The ID */ + unsigned d_id : 32; + + /** The expression's reference count. @see cvc4::Expr. */ + unsigned d_rc : 8; + + /** Kind of the expression */ + unsigned d_kind : 8; + + /** Number of children */ + unsigned d_nchildren : 16; + + /** Variable number of child nodes */ + Expr d_children[0]; + + friend class Expr; + +public: + /** Hash this expression. + * @return the hash value of this expression. */ + uint64_t hash() const; + + // Iterator support + + typedef Expr* iterator; + typedef Expr const* const_iterator; + + iterator begin(); + iterator end(); + iterator rbegin(); + iterator rend(); + + const_iterator begin() const; + const_iterator end() const; + const_iterator rbegin() const; + const_iterator rend() const; +}; + +} /* CVC4 namespace */ + +#endif /* __CVC4_EXPR_VALUE_H */ |