diff options
Diffstat (limited to 'src/include/expr_value.h')
-rw-r--r-- | src/include/expr_value.h | 71 |
1 files changed, 71 insertions, 0 deletions
diff --git a/src/include/expr_value.h b/src/include/expr_value.h new file mode 100644 index 000000000..ca12b8e03 --- /dev/null +++ b/src/include/expr_value.h @@ -0,0 +1,71 @@ +/********************* +/** expr_value.h + ** This file is part of the CVC4 prototype. + ** + ** 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 + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_EXPR_VALUE_H +#define __CVC4_EXPR_VALUE_H + +#include "expr.h" + +namespace CVC4 { + +/** + * This is an ExprValue. + */ +class ExprValue { + // 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]; + +public: + /** Hash this expression. + * @return the hash value of this expression. */ + unsigned hash() const; + + /** Convert to (wrap in) an Expr. + * @return an Expr pointing to this expression. */ + operator Expr(); + + // 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 */ |