summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/Makefile.am10
-rw-r--r--src/expr/attr_type.h34
-rw-r--r--src/expr/expr.cpp104
-rw-r--r--src/expr/expr_attribute.h98
-rw-r--r--src/expr/expr_builder.cpp152
-rw-r--r--src/expr/expr_builder.h153
-rw-r--r--src/expr/expr_manager.cpp52
-rw-r--r--src/expr/expr_manager.h58
-rw-r--r--src/expr/expr_value.cpp79
-rw-r--r--src/expr/expr_value.h75
-rw-r--r--src/expr/kind.h38
11 files changed, 853 insertions, 0 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
new file mode 100644
index 000000000..d26a7483d
--- /dev/null
+++ b/src/expr/Makefile.am
@@ -0,0 +1,10 @@
+INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CXXFLAGS = -Wall
+
+noinst_LIBRARIES = libcore.a
+
+libcore_a_SOURCES = \
+ expr.cpp \
+ expr_builder.cpp \
+ expr_manager.cpp \
+ expr_value.cpp
diff --git a/src/expr/attr_type.h b/src/expr/attr_type.h
new file mode 100644
index 000000000..d76bd742d
--- /dev/null
+++ b/src/expr/attr_type.h
@@ -0,0 +1,34 @@
+/********************* -*- C++ -*- */
+/** attr_type.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.
+ **
+ **/
+
+#ifndef __CVC4_ATTR_TYPE_H
+#define __CVC4_ATTR_TYPE_H
+
+#include "core/expr_attribute.h"
+
+namespace CVC4 {
+
+class Type;
+
+// an "attribute type" for types
+// this is essentially a traits structure
+class Type_attr {
+public:
+ enum { hash_value = 11 }; // could use typeid but then different on different machines/compiles
+ typedef Type value_type;//Expr?
+ static const Type_attr marker;
+};
+
+extern AttrTable<Type_attr> type_table;
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4_ATTR_TYPE_H */
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
new file mode 100644
index 000000000..5e422f349
--- /dev/null
+++ b/src/expr/expr.cpp
@@ -0,0 +1,104 @@
+/********************* -*- C++ -*- */
+/** expr.cpp
+ ** 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.
+ **
+ ** Reference-counted encapsulation of a pointer to an expression.
+ **/
+
+#include "cvc4_expr.h"
+#include "core/expr_value.h"
+#include "core/expr_builder.h"
+
+namespace CVC4 {
+
+Expr Expr::s_null(0);
+
+Expr::Expr(ExprValue* ev)
+ : d_ev(ev) {
+ // FIXME: thread-safety
+ ++d_ev->d_rc;
+}
+
+Expr::Expr(const Expr& e) {
+ // FIXME: thread-safety
+ if((d_ev = e.d_ev))
+ ++d_ev->d_rc;
+}
+
+Expr::~Expr() {
+ // FIXME: thread-safety
+ --d_ev->d_rc;
+}
+
+Expr& Expr::operator=(const Expr& e) {
+ // FIXME: thread-safety
+ if(d_ev)
+ --d_ev->d_rc;
+ if((d_ev = e.d_ev))
+ ++d_ev->d_rc;
+ return *this;
+}
+
+ExprValue* Expr::operator->() {
+ return d_ev;
+}
+
+const ExprValue* Expr::operator->() const {
+ return d_ev;
+}
+
+uint64_t Expr::hash() const {
+ return d_ev->hash();
+}
+
+Expr Expr::eqExpr(const Expr& right) const {
+ return ExprBuilder(*this).eqExpr(right);
+}
+
+Expr Expr::notExpr() const {
+ return ExprBuilder(*this).notExpr();
+}
+
+Expr Expr::negate() const { // avoid double-negatives
+ return ExprBuilder(*this).negate();
+}
+
+Expr Expr::andExpr(const Expr& right) const {
+ return ExprBuilder(*this).andExpr(right);
+}
+
+Expr Expr::orExpr(const Expr& right) const {
+ return ExprBuilder(*this).orExpr(right);
+}
+
+Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const {
+ return ExprBuilder(*this).iteExpr(thenpart, elsepart);
+}
+
+Expr Expr::iffExpr(const Expr& right) const {
+ return ExprBuilder(*this).iffExpr(right);
+}
+
+Expr Expr::impExpr(const Expr& right) const {
+ return ExprBuilder(*this).impExpr(right);
+}
+
+Expr Expr::xorExpr(const Expr& right) const {
+ return ExprBuilder(*this).xorExpr(right);
+}
+
+Expr Expr::skolemExpr(int i) const {
+ return ExprBuilder(*this).skolemExpr(i);
+}
+
+Expr Expr::substExpr(const std::vector<Expr>& oldTerms,
+ const std::vector<Expr>& newTerms) const {
+ return ExprBuilder(*this).substExpr(oldTerms, newTerms);
+}
+
+} /* CVC4 namespace */
diff --git a/src/expr/expr_attribute.h b/src/expr/expr_attribute.h
new file mode 100644
index 000000000..b00882478
--- /dev/null
+++ b/src/expr/expr_attribute.h
@@ -0,0 +1,98 @@
+/********************* -*- C++ -*- */
+/** expr_attribute.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.
+ **
+ **/
+
+#ifndef __CVC4_EXPR_ATTRIBUTE_H
+#define __CVC4_EXPR_ATTRIBUTE_H
+
+// TODO WARNING this file needs work !
+
+#include <stdint.h>
+#include "core/config.h"
+#include "core/context.h"
+#include "core/cvc4_expr.h"
+
+namespace CVC4 {
+
+template <class value_type>
+class AttrTables;
+
+// global (or TSS)
+extern CDMap<uint64_t> g_hash_bool;
+extern CDMap<uint64_t> g_hash_int;
+extern CDMap<Expr> g_hash_expr;
+extern CDMap<void*> g_hash_ptr;
+
+template <class T>
+class AttrTable;
+
+template <>
+class AttrTable<bool> {
+public:
+ class BitAccessor {
+ uint64_t& d_word;
+ unsigned d_bit;
+ public:
+ BitAccessor& operator=(bool b);
+ // continue...
+ };
+
+ // bool specialization
+ static CDMap<uint64_t> *s_hash;
+
+ template <class Attr>
+ BitAccessor& find(Expr e, const Attr&);
+
+ template <class Attr>
+ bool find(Expr e, const Attr&) const;
+};
+
+template <>
+class AttrTable<uint64_t> {
+public:
+ // int(egral) specialization
+ static CDMap<uint64_t> *s_hash;
+ uint64_t& find(Expr);
+ uint64_t& find(Expr) const;
+};
+
+template <class T>
+class AttrTable<T*> {
+ // pointer specialization
+ static CDMap<void*> *s_hash;
+public:
+};
+
+template <>
+class AttrTable<Expr> {
+public:
+ // Expr specialization
+ static CDMap<Expr> *s_hash;
+ Expr find(Expr);
+};
+
+CDMap<uint64_t>* AttrTable<bool>::s_hash = &g_hash_bool;
+CDMap<uint64_t>* AttrTable<uint64_t>::s_hash = &g_hash_int;
+CDMap<Expr>* AttrTable<Expr>::s_hash = &g_hash_expr;
+
+template <class T>
+CDMap<void*>* AttrTable<T*>::s_hash = &g_hash_ptr;
+
+template <class Attr>
+class AttributeTable {
+ typedef typename Attr::value_type value_type;
+
+ AttrTable<value_type>& d_table;
+
+};
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4_EXPR_ATTRIBUTE_H */
diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp
new file mode 100644
index 000000000..6491b7d44
--- /dev/null
+++ b/src/expr/expr_builder.cpp
@@ -0,0 +1,152 @@
+/********************* -*- C++ -*- */
+/** expr_builder.cpp
+ ** 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.
+ **
+ **/
+
+#include "core/expr_builder.h"
+#include "core/expr_manager.h"
+#include "core/expr_value.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+ExprBuilder::ExprBuilder() : d_em(ExprManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(0) {}
+
+ExprBuilder::ExprBuilder(Kind k) : d_em(ExprManager::currentEM()), d_kind(k), d_used(false), d_nchildren(0) {}
+
+ExprBuilder::ExprBuilder(const Expr& e) : d_em(ExprManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) {
+ ExprValue *v = e->inc();
+ d_children.u_arr[0] = v;
+}
+
+ExprBuilder::ExprBuilder(const ExprBuilder& eb) : d_em(eb.d_em), d_kind(eb.d_kind), d_used(eb.d_used), d_nchildren(eb.d_nchildren) {
+ cvc4assert(!d_used);
+
+ if(d_nchildren > nchild_thresh) {
+ d_children.u_vec = new vector<Expr>();
+ d_children.u_vec->reserve(d_nchildren + 5);
+ copy(eb.d_children.u_vec->begin(), eb.d_children.u_vec->end(), back_inserter(*d_children.u_vec));
+ } else {
+ iterator j = d_children.u_arr;
+ for(iterator i = eb.d_children.u_arr; i != eb.d_children.u_arr + eb.d_nchildren; ++i, ++j)
+ *j = i->inc();
+ }
+}
+
+ExprBuilder::ExprBuilder(ExprManager* em) : d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(0) {
+}
+
+ExprBuilder::ExprBuilder(ExprManager* em, Kind k) : d_em(em), d_kind(k), d_used(false), d_nchildren(0) {
+}
+
+ExprBuilder::ExprBuilder(ExprManager* em, const Expr&) : d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) {
+ ExprValue *v = e->inc();
+ d_children.u_arr[0] = v;
+}
+
+ExprBuilder::~ExprBuilder() {
+ if(d_nchildren > nchild_thresh) {
+ delete d_children.u_vec;
+ } else {
+ for(iterator i = d_children.u_arr; i != d_children.u_arr + d_nchildren; ++i) {
+ *i
+ }
+ }
+}
+
+// Compound expression constructors
+ExprBuilder& ExprBuilder::eqExpr(const Expr& right) {
+ if(d_kind != UNDEFINED_KIND && d_kind != EQUAL)
+ collapse();
+ d_kind = EQUAL;
+ return *this;
+}
+
+ExprBuilder& ExprBuilder::notExpr() {
+}
+
+// avoid double-negatives
+ExprBuilder& ExprBuilder::negate() {
+}
+
+ExprBuilder& ExprBuilder::andExpr(const Expr& right) {
+}
+
+ExprBuilder& ExprBuilder::orExpr(const Expr& right) {
+}
+
+ExprBuilder& ExprBuilder::iteExpr(const Expr& thenpart, const Expr& elsepart) {
+}
+
+ExprBuilder& ExprBuilder::iffExpr(const Expr& right) {
+}
+
+ExprBuilder& ExprBuilder::impExpr(const Expr& right) {
+}
+
+ExprBuilder& ExprBuilder::xorExpr(const Expr& right) {
+}
+
+ExprBuilder& ExprBuilder::skolemExpr(int i) {
+}
+
+ExprBuilder& ExprBuilder::substExpr(const std::vector<Expr>& oldTerms,
+ const std::vector<Expr>& newTerms) {
+}
+
+// "Stream" expression constructor syntax
+ExprBuilder& ExprBuilder::operator<<(const Kind& op) {
+}
+
+ExprBuilder& ExprBuilder::operator<<(const Expr& child) {
+}
+
+template <class Iterator>
+ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) {
+}
+
+void ExprBuilder::addChild(const Expr& e) {
+ if(d_nchildren == nchild_thresh) {
+ vector<Expr>* v = new vector<Expr>();
+ v->reserve(nchild_thresh + 5);
+
+ }
+ return *this;
+}
+
+void ExprBuilder::collapse() {
+ if(d_nchildren == nchild_thresh) {
+ vector<Expr>* v = new vector<Expr>();
+ v->reserve(nchild_thresh + 5);
+
+ }
+ return *this;
+}
+
+// not const
+ExprBuilder::operator Expr() {
+}
+
+AndExprBuilder ExprBuilder::operator&&(Expr) {
+}
+
+OrExprBuilder ExprBuilder::operator||(Expr) {
+}
+
+PlusExprBuilder ExprBuilder::operator+ (Expr) {
+}
+
+PlusExprBuilder ExprBuilder::operator- (Expr) {
+}
+
+MultExprBuilder ExprBuilder::operator* (Expr) {
+}
+
+} /* CVC4 namespace */
diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h
new file mode 100644
index 000000000..fa08a3149
--- /dev/null
+++ b/src/expr/expr_builder.h
@@ -0,0 +1,153 @@
+/********************* -*- C++ -*- */
+/** expr_builder.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.
+ **
+ **/
+
+#ifndef __CVC4_EXPR_BUILDER_H
+#define __CVC4_EXPR_BUILDER_H
+
+#include <vector>
+#include "core/expr_manager.h"
+#include "core/kind.h"
+
+namespace CVC4 {
+
+class AndExprBuilder;
+class OrExprBuilder;
+class PlusExprBuilder;
+class MinusExprBuilder;
+class MultExprBuilder;
+
+class ExprBuilder {
+ ExprManager* d_em;
+
+ Kind d_kind;
+
+ // initially false, when you extract the Expr this is set and you can't
+ // extract another
+ bool d_used;
+
+ static const unsigned nchild_thresh = 10;
+
+ unsigned d_nchildren;
+ union {
+ ExprValue* u_arr[nchild_thresh];
+ std::vector<Expr>* u_vec;
+ } d_children;
+
+ void addChild();
+ void collapse();
+
+public:
+
+ ExprBuilder();
+ ExprBuilder(Kind k);
+ ExprBuilder(const Expr&);
+ ExprBuilder(const ExprBuilder&);
+
+ ExprBuilder(ExprManager*);
+ ExprBuilder(ExprManager*, Kind k);
+ ExprBuilder(ExprManager*, const Expr&);
+ ExprBuilder(ExprManager*, const ExprBuilder&);
+
+ ~ExprBuilder();
+
+ // Compound expression constructors
+ ExprBuilder& eqExpr(const Expr& right);
+ ExprBuilder& notExpr();
+ ExprBuilder& negate(); // avoid double-negatives
+ ExprBuilder& andExpr(const Expr& right);
+ ExprBuilder& orExpr(const Expr& right);
+ ExprBuilder& iteExpr(const Expr& thenpart, const Expr& elsepart);
+ ExprBuilder& iffExpr(const Expr& right);
+ ExprBuilder& impExpr(const Expr& right);
+ ExprBuilder& xorExpr(const Expr& right);
+ ExprBuilder& skolemExpr(int i);
+ ExprBuilder& substExpr(const std::vector<Expr>& oldTerms,
+ const std::vector<Expr>& newTerms);
+ /*
+ ExprBuilder& substExpr(const ExprHashMap<Expr>& oldToNew);
+ */
+
+ /* TODO design: these modify ExprBuilder */
+ ExprBuilder& operator!() { return notExpr(); }
+ ExprBuilder& operator&&(const Expr& right) { return andExpr(right); }
+ ExprBuilder& operator||(const Expr& right) { return orExpr(right); }
+
+ // "Stream" expression constructor syntax
+ ExprBuilder& operator<<(const Kind& op);
+ ExprBuilder& operator<<(const Expr& child);
+
+ // For pushing sequences of children
+ ExprBuilder& append(const std::vector<Expr>& children) { return append(children.begin(), children.end()); }
+ template <class Iterator> ExprBuilder& append(const Iterator& begin, const Iterator& end);
+
+ operator Expr();// not const
+
+ AndExprBuilder operator&&(Expr);
+ OrExprBuilder operator||(Expr);
+ PlusExprBuilder operator+ (Expr);
+ PlusExprBuilder operator- (Expr);
+ MultExprBuilder operator* (Expr);
+
+};/* class ExprBuilder */
+
+class AndExprBuilder {
+ ExprManager* d_em;
+
+public:
+
+ AndExprBuilder& operator&&(Expr);
+ OrExprBuilder operator||(Expr);
+
+ operator ExprBuilder();
+
+};/* class AndExprBuilder */
+
+class OrExprBuilder {
+ ExprManager* d_em;
+
+public:
+
+ AndExprBuilder operator&&(Expr);
+ OrExprBuilder& operator||(Expr);
+
+ operator ExprBuilder();
+
+};/* class OrExprBuilder */
+
+class PlusExprBuilder {
+ ExprManager* d_em;
+
+public:
+
+ PlusExprBuilder& operator+(Expr);
+ PlusExprBuilder& operator-(Expr);
+ MultExprBuilder operator*(Expr);
+
+ operator ExprBuilder();
+
+};/* class PlusExprBuilder */
+
+class MultExprBuilder {
+ ExprManager* d_em;
+
+public:
+
+ PlusExprBuilder operator+(Expr);
+ PlusExprBuilder operator-(Expr);
+ MultExprBuilder& operator*(Expr);
+
+ operator ExprBuilder();
+
+};/* class MultExprBuilder */
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4_EXPR_BUILDER_H */
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
new file mode 100644
index 000000000..90f10d8f7
--- /dev/null
+++ b/src/expr/expr_manager.cpp
@@ -0,0 +1,52 @@
+/********************* -*- C++ -*- */
+/** expr_manager.cpp
+ ** 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.
+ **
+ ** Expression manager implementation.
+ **/
+
+#include "core/expr_builder.h"
+#include "core/expr_manager.h"
+#include "core/cvc4_expr.h"
+
+namespace CVC4 {
+
+__thread ExprManager* ExprManager::s_current = 0;
+
+// general expression-builders
+
+Expr ExprManager::mkExpr(Kind kind) {
+ return ExprBuilder(this, kind);
+}
+
+Expr ExprManager::mkExpr(Kind kind, Expr child1) {
+ return ExprBuilder(this, kind) << child1;
+}
+
+Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) {
+ return ExprBuilder(this, kind) << child1 << child2;
+}
+
+Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3) {
+ return ExprBuilder(this, kind) << child1 << child2 << child3;
+}
+
+Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4) {
+ return ExprBuilder(this, kind) << child1 << child2 << child3 << child4;
+}
+
+Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5) {
+ return ExprBuilder(this, kind) << child1 << child2 << child3 << child4 << child5;
+}
+
+// N-ary version
+Expr ExprManager::mkExpr(Kind kind, std::vector<Expr> children) {
+ return ExprBuilder(this, kind).append(children);
+}
+
+} /* CVC4 namespace */
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
new file mode 100644
index 000000000..048250485
--- /dev/null
+++ b/src/expr/expr_manager.h
@@ -0,0 +1,58 @@
+/********************* -*- C++ -*- */
+/** expr_manager.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.
+ **
+ **/
+
+#ifndef __CVC4_EXPR_MANAGER_H
+#define __CVC4_EXPR_MANAGER_H
+
+#include <vector>
+#include "cvc4_expr.h"
+#include "core/kind.h"
+
+namespace CVC4 {
+
+class ExprManager {
+ static __thread ExprManager* s_current;
+
+public:
+ static ExprManager* currentEM() { return s_current; }
+
+ // general expression-builders
+ Expr mkExpr(Kind kind);
+ Expr mkExpr(Kind kind, Expr child1);
+ Expr mkExpr(Kind kind, Expr child1, Expr child2);
+ Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3);
+ Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
+ Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5);
+ // N-ary version
+ Expr mkExpr(Kind kind, std::vector<Expr> children);
+
+ // TODO: these use the current EM (but must be renamed)
+ /*
+ static Expr mkExpr(Kind kind)
+ { currentEM()->mkExpr(kind); }
+ static Expr mkExpr(Kind kind, Expr child1);
+ { currentEM()->mkExpr(kind, child1); }
+ static Expr mkExpr(Kind kind, Expr child1, Expr child2);
+ { currentEM()->mkExpr(kind, child1, child2); }
+ static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3);
+ { currentEM()->mkExpr(kind, child1, child2, child3); }
+ static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
+ { currentEM()->mkExpr(kind, child1, child2, child3, child4); }
+ static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5);
+ { currentEM()->mkExpr(kind, child1, child2, child3, child4, child5); }
+ */
+
+ // do we want a varargs one? perhaps not..
+};
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4_EXPR_MANAGER_H */
diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp
new file mode 100644
index 000000000..ce4177a09
--- /dev/null
+++ b/src/expr/expr_value.cpp
@@ -0,0 +1,79 @@
+/********************* -*- C++ -*- */
+/** expr_value.cpp
+ ** 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
+ **/
+
+#include "core/expr_value.h"
+
+namespace CVC4 {
+
+uint64_t ExprValue::hash() const {
+ uint64_t hash = d_kind;
+
+ for(const_iterator i = begin(); i != end(); ++i)
+ hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ i->hash();
+
+ return hash;
+}
+
+ExprValue* ExprValue::inc() {
+ // FIXME multithreading
+ if(d_rc < MAX_RC)
+ ++d_rc;
+ return this;
+}
+
+ExprValue* ExprValue::dec() {
+ // FIXME multithreading
+ if(d_rc < MAX_RC)
+ if(--d_rc == 0) {
+ // FIXME gc
+ return 0;
+ }
+ return this;
+}
+
+ExprValue::iterator ExprValue::begin() {
+ return d_children;
+}
+
+ExprValue::iterator ExprValue::end() {
+ return d_children + d_nchildren;
+}
+
+ExprValue::iterator ExprValue::rbegin() {
+ return d_children + d_nchildren - 1;
+}
+
+ExprValue::iterator ExprValue::rend() {
+ return d_children - 1;
+}
+
+ExprValue::const_iterator ExprValue::begin() const {
+ return d_children;
+}
+
+ExprValue::const_iterator ExprValue::end() const {
+ return d_children + d_nchildren;
+}
+
+ExprValue::const_iterator ExprValue::rbegin() const {
+ return d_children + d_nchildren - 1;
+}
+
+ExprValue::const_iterator ExprValue::rend() const {
+ return d_children - 1;
+}
+
+} /* CVC4 namespace */
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 */
diff --git a/src/expr/kind.h b/src/expr/kind.h
new file mode 100644
index 000000000..9c4e4d5ab
--- /dev/null
+++ b/src/expr/kind.h
@@ -0,0 +1,38 @@
+/********************* -*- C++ -*- */
+/** kind.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.
+ **
+ **/
+
+#ifndef __CVC4_KIND_H
+#define __CVC4_KIND_H
+
+namespace CVC4 {
+
+// TODO: create this file (?) from theory solver headers so that we
+// have a collection of kinds from all. This file is mainly a
+// placeholder for design & development work.
+
+enum Kind {
+ UNDEFINED_KIND = -1,
+ EQUAL,
+ AND,
+ OR,
+ XOR,
+ NOT,
+ PLUS,
+ MINUS,
+ ITE,
+ IFF,
+ SKOLEM,
+ SUBST
+};/* enum Kind */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_KIND_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback