diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/Makefile | 5 | ||||
-rw-r--r-- | src/expr/Makefile.am | 9 | ||||
-rw-r--r-- | src/expr/Makefile.in | 15 | ||||
-rw-r--r-- | src/expr/expr_value.cpp | 103 | ||||
-rw-r--r-- | src/expr/kind.h | 1 | ||||
-rw-r--r-- | src/expr/node.cpp | 41 | ||||
-rw-r--r-- | src/expr/node.h | 66 | ||||
-rw-r--r-- | src/expr/node_builder.cpp | 211 | ||||
-rw-r--r-- | src/expr/node_builder.h | 513 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 76 | ||||
-rw-r--r-- | src/expr/node_manager.h | 26 | ||||
-rw-r--r-- | src/expr/node_value.cpp | 147 | ||||
-rw-r--r-- | src/expr/node_value.h (renamed from src/expr/expr_value.h) | 109 |
13 files changed, 756 insertions, 566 deletions
diff --git a/src/expr/Makefile b/src/expr/Makefile new file mode 100644 index 000000000..b661835a5 --- /dev/null +++ b/src/expr/Makefile @@ -0,0 +1,5 @@ +topdir = ../.. +srcdir = src/expr +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index b8606e051..046281702 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -1,6 +1,7 @@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libexpr.la @@ -10,7 +11,7 @@ libexpr_la_SOURCES = \ node.h \ node_builder.h \ expr.h \ - expr_value.h \ + node_value.h \ node_manager.h \ expr_manager.h \ node_attribute.h \ @@ -19,6 +20,6 @@ libexpr_la_SOURCES = \ node_builder.cpp \ node_manager.cpp \ expr_manager.cpp \ - expr_value.cpp \ + node_value.cpp \ expr.cpp diff --git a/src/expr/Makefile.in b/src/expr/Makefile.in index 6b1555e6c..c7d99dc84 100644 --- a/src/expr/Makefile.in +++ b/src/expr/Makefile.in @@ -53,7 +53,7 @@ CONFIG_CLEAN_VPATH_FILES = LTLIBRARIES = $(noinst_LTLIBRARIES) libexpr_la_LIBADD = am_libexpr_la_OBJECTS = node.lo node_builder.lo node_manager.lo \ - expr_manager.lo expr_value.lo expr.lo + expr_manager.lo node_value.lo expr.lo libexpr_la_OBJECTS = $(am_libexpr_la_OBJECTS) DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir) depcomp = $(SHELL) $(top_srcdir)/config/depcomp @@ -105,6 +105,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -216,9 +217,11 @@ target_vendor = @target_vendor@ top_build_prefix = @top_build_prefix@ top_builddir = @top_builddir@ top_srcdir = @top_srcdir@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../include -I@srcdir@/.. + AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libexpr.la libexpr_la_SOURCES = \ attr_type.h \ @@ -226,7 +229,7 @@ libexpr_la_SOURCES = \ node.h \ node_builder.h \ expr.h \ - expr_value.h \ + node_value.h \ node_manager.h \ expr_manager.h \ node_attribute.h \ @@ -235,7 +238,7 @@ libexpr_la_SOURCES = \ node_builder.cpp \ node_manager.cpp \ expr_manager.cpp \ - expr_value.cpp \ + node_value.cpp \ expr.cpp all: all-am @@ -292,10 +295,10 @@ distclean-compile: @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr.Plo@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr_manager.Plo@am__quote@ -@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr_value.Plo@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node.Plo@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node_builder.Plo@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node_manager.Plo@am__quote@ +@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node_value.Plo@am__quote@ .cpp.o: @am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $< diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp deleted file mode 100644 index af064f43d..000000000 --- a/src/expr/expr_value.cpp +++ /dev/null @@ -1,103 +0,0 @@ -/********************* -*- 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::Node rather than by pointer; cvc4::Node maintains the - ** reference count on ExprValue instances and - **/ - -#include "expr_value.h" -#include <sstream> - -using namespace std; - -namespace CVC4 { - -size_t ExprValue::next_id = 1; - -ExprValue::ExprValue() : - d_id(0), d_rc(MAX_RC), d_kind(NULL_EXPR), d_nchildren(0) { -} - -uint64_t ExprValue::hash() const { - return computeHash<const_iterator>(d_kind, begin(), end()); -} - -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; -} - -string ExprValue::toString() const { - stringstream ss; - toStream(ss); - return ss.str(); -} - -void ExprValue::toStream(std::ostream& out) const { - out << "(" << Kind(d_kind); - if(d_kind == VARIABLE) { - out << ":" << this; - } else { - for(const_iterator i = begin(); i != end(); ++i) { - if(i != end()) - out << " "; - out << *i; - } - } - out << ")"; -} - -}/* CVC4 namespace */ diff --git a/src/expr/kind.h b/src/expr/kind.h index 5ac02ca7c..624ab7337 100644 --- a/src/expr/kind.h +++ b/src/expr/kind.h @@ -12,6 +12,7 @@ #ifndef __CVC4__KIND_H #define __CVC4__KIND_H +#include "cvc4_config.h" #include <iostream> namespace CVC4 { diff --git a/src/expr/node.cpp b/src/expr/node.cpp index be9ac995c..1a549973f 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -1,5 +1,5 @@ /********************* -*- C++ -*- */ -/** expr.cpp +/** node.cpp ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -11,7 +11,7 @@ **/ #include "expr/node.h" -#include "expr/expr_value.h" +#include "expr/node_value.h" #include "expr/node_builder.h" #include "util/Assert.h" @@ -22,26 +22,29 @@ using namespace std; namespace CVC4 { -ExprValue ExprValue::s_null; +NodeValue NodeValue::s_null; -Node Node::s_null(&ExprValue::s_null); +Node Node::s_null(&NodeValue::s_null); Node Node::null() { return s_null; } - bool Node::isNull() const { - return d_ev == &ExprValue::s_null; + return d_ev == &NodeValue::s_null; } Node::Node() : - d_ev(&ExprValue::s_null) { + d_ev(&NodeValue::s_null) { // No refcount needed } -Node::Node(ExprValue* ev) - : d_ev(ev) { +// FIXME: escape from type system convenient but is there a better +// way? Nodes conceptually don't change their expr values but of +// course they do modify the refcount. But it's nice to be able to +// support node_iterators over const NodeValue*. So.... hm. +Node::Node(const NodeValue* ev) + : d_ev(const_cast<NodeValue*>(ev)) { Assert(d_ev != NULL, "Expecting a non-NULL expression value!"); d_ev->inc(); } @@ -57,7 +60,7 @@ Node::~Node() { d_ev->dec(); } -void Node::assignExprValue(ExprValue* ev) { +void Node::assignNodeValue(NodeValue* ev) { d_ev = ev; d_ev->inc(); } @@ -72,7 +75,7 @@ Node& Node::operator=(const Node& e) { return *this; } -ExprValue const* Node::operator->() const { +NodeValue const* Node::operator->() const { Assert(d_ev != NULL, "Expecting a non-NULL expression value!"); return d_ev; } @@ -83,35 +86,35 @@ uint64_t Node::hash() const { } Node Node::eqExpr(const Node& right) const { - return NodeManager::currentEM()->mkExpr(EQUAL, *this, right); + return NodeManager::currentNM()->mkExpr(EQUAL, *this, right); } Node Node::notExpr() const { - return NodeManager::currentEM()->mkExpr(NOT, *this); + return NodeManager::currentNM()->mkExpr(NOT, *this); } Node Node::andExpr(const Node& right) const { - return NodeManager::currentEM()->mkExpr(AND, *this, right); + return NodeManager::currentNM()->mkExpr(AND, *this, right); } Node Node::orExpr(const Node& right) const { - return NodeManager::currentEM()->mkExpr(OR, *this, right); + return NodeManager::currentNM()->mkExpr(OR, *this, right); } Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const { - return NodeManager::currentEM()->mkExpr(ITE, *this, thenpart, elsepart); + return NodeManager::currentNM()->mkExpr(ITE, *this, thenpart, elsepart); } Node Node::iffExpr(const Node& right) const { - return NodeManager::currentEM()->mkExpr(IFF, *this, right); + return NodeManager::currentNM()->mkExpr(IFF, *this, right); } Node Node::impExpr(const Node& right) const { - return NodeManager::currentEM()->mkExpr(IMPLIES, *this, right); + return NodeManager::currentNM()->mkExpr(IMPLIES, *this, right); } Node Node::xorExpr(const Node& right) const { - return NodeManager::currentEM()->mkExpr(XOR, *this, right); + return NodeManager::currentNM()->mkExpr(XOR, *this, right); } }/* CVC4 namespace */ diff --git a/src/expr/node.h b/src/expr/node.h index 17d1c0111..5415a5b3c 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -10,6 +10,8 @@ ** Reference-counted encapsulation of a pointer to an expression. **/ +#include "expr/node_value.h" + #ifndef __CVC4__NODE_H #define __CVC4__NODE_H @@ -32,38 +34,44 @@ inline std::ostream& operator<<(std::ostream&, const Node&); class NodeManager; namespace expr { - class ExprValue; + class NodeValue; }/* CVC4::expr namespace */ -using CVC4::expr::ExprValue; +using CVC4::expr::NodeValue; /** - * Encapsulation of an ExprValue pointer. The reference count is - * maintained in the ExprValue. + * Encapsulation of an NodeValue pointer. The reference count is + * maintained in the NodeValue. */ class Node { - friend class ExprValue; + friend class NodeValue; /** A convenient null-valued encapsulated pointer */ static Node s_null; - /** The referenced ExprValue */ - ExprValue* d_ev; + /** The referenced NodeValue */ + NodeValue* d_ev; /** This constructor is reserved for use by the Node package; one * must construct an Node using one of the build mechanisms of the * Node package. * - * Increments the reference count. */ - explicit Node(ExprValue*); - - friend class NodeBuilder; + * Increments the reference count. + * + * FIXME: there's a type-system escape here to cast away the const, + * since the refcount needs to be updated. But conceptually Nodes + * don't change their arguments, and it's nice to have + * const_iterators over them. See notes in .cpp file for + * details. */ + explicit Node(const NodeValue*); + + template <unsigned> friend class NodeBuilder; friend class NodeManager; /** Access to the encapsulated expression. * @return the encapsulated expression. */ - ExprValue const* operator->() const; + NodeValue const* operator->() const; /** * Assigns the expression value and does reference counting. No assumptions are @@ -72,7 +80,15 @@ class Node { * * @param ev the expression value to assign */ - void assignExprValue(ExprValue* ev); + void assignNodeValue(NodeValue* ev); + + typedef NodeValue::iterator ev_iterator; + typedef NodeValue::const_iterator const_ev_iterator; + + inline ev_iterator ev_begin(); + inline ev_iterator ev_end(); + inline const_ev_iterator ev_begin() const; + inline const_ev_iterator ev_end() const; public: @@ -82,7 +98,7 @@ public: Node(const Node&); /** Destructor. Decrements the reference count and, if zero, - * collects the ExprValue. */ + * collects the NodeValue. */ ~Node(); bool operator==(const Node& e) const { return d_ev == e.d_ev; } @@ -117,8 +133,8 @@ public: static Node null(); - typedef Node* iterator; - typedef Node const* const_iterator; + typedef NodeValue::node_iterator iterator; + typedef NodeValue::node_iterator const_iterator; inline iterator begin(); inline iterator end(); @@ -134,7 +150,7 @@ public: }/* CVC4 namespace */ -#include "expr/expr_value.h" +#include "expr/node_value.h" namespace CVC4 { @@ -159,6 +175,22 @@ inline void Node::toStream(std::ostream& out) const { d_ev->toStream(out); } +inline Node::ev_iterator Node::ev_begin() { + return d_ev->ev_begin(); +} + +inline Node::ev_iterator Node::ev_end() { + return d_ev->ev_end(); +} + +inline Node::const_ev_iterator Node::ev_begin() const { + return d_ev->ev_begin(); +} + +inline Node::const_ev_iterator Node::ev_end() const { + return d_ev->ev_end(); +} + inline Node::iterator Node::begin() { return d_ev->begin(); } diff --git a/src/expr/node_builder.cpp b/src/expr/node_builder.cpp index 7d30ff4e3..0a36421f2 100644 --- a/src/expr/node_builder.cpp +++ b/src/expr/node_builder.cpp @@ -1,5 +1,5 @@ /********************* -*- C++ -*- */ -/** expr_builder.cpp +/** node_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 @@ -11,214 +11,7 @@ #include "expr/node_builder.h" #include "expr/node_manager.h" -#include "expr/expr_value.h" +#include "expr/node_value.h" #include "util/output.h" using namespace std; - -namespace CVC4 { - -NodeBuilder::NodeBuilder() : - d_em(NodeManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), - d_nchildren(0) { -} - -NodeBuilder::NodeBuilder(Kind k) : - d_em(NodeManager::currentEM()), d_kind(k), d_used(false), d_nchildren(0) { -} - -NodeBuilder::NodeBuilder(const Node& e) : - d_em(NodeManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) { - d_children.u_arr[0] = e.d_ev->inc();; -} - -NodeBuilder& NodeBuilder::reset(const ExprValue* ev) { - this->~NodeBuilder(); - d_kind = Kind(ev->d_kind); - d_used = false; - d_nchildren = ev->d_nchildren; - for(Node::const_iterator i = ev->begin(); i != ev->end(); ++i) - addChild(i->d_ev); - return *this; -} - -NodeBuilder::NodeBuilder(const NodeBuilder& eb) : - d_em(eb.d_em), d_kind(eb.d_kind), d_used(eb.d_used), - d_nchildren(eb.d_nchildren) { - Assert( !d_used ); - - if(d_nchildren > nchild_thresh) { - d_children.u_vec = new vector<Node> (); - 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 { - ev_iterator j = d_children.u_arr; - ExprValue* const * i = eb.d_children.u_arr; - ExprValue* const * i_end = i + eb.d_nchildren; - for(; i != i_end; ++i, ++j) - *j = (*i)->inc(); - } -} - -NodeBuilder::NodeBuilder(NodeManager* em) : - d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(0) { -} - -NodeBuilder::NodeBuilder(NodeManager* em, Kind k) : - d_em(em), d_kind(k), d_used(false), d_nchildren(0) { -} - -NodeBuilder::NodeBuilder(NodeManager* em, const Node& e) : - d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) { - d_children.u_arr[0] = e.d_ev->inc(); -} - -NodeBuilder::~NodeBuilder() { - if(d_nchildren > nchild_thresh) { - delete d_children.u_vec; - } else { - ev_iterator i = d_children.u_arr; - ev_iterator i_end = d_children.u_arr + d_nchildren; - for(; i != i_end ; ++i) { - (*i)->dec(); - } - } -} - -// Compound expression constructors -NodeBuilder& NodeBuilder::eqExpr(const Node& right) { - Assert( d_kind != UNDEFINED_KIND ); - if(EXPECT_TRUE( d_kind != EQUAL )) { - collapse(); - d_kind = EQUAL; - } - addChild(right); - return *this; -} - -NodeBuilder& NodeBuilder::notExpr() { - Assert( d_kind != UNDEFINED_KIND ); - collapse(); - d_kind = NOT; - return *this; -} - -NodeBuilder& NodeBuilder::andExpr(const Node& right) { - Assert( d_kind != UNDEFINED_KIND ); - if(d_kind != AND) { - collapse(); - d_kind = AND; - } - addChild(right); - return *this; -} - -NodeBuilder& NodeBuilder::orExpr(const Node& right) { - Assert( d_kind != UNDEFINED_KIND ); - if(EXPECT_TRUE( d_kind != OR )) { - collapse(); - d_kind = OR; - } - addChild(right); - return *this; -} - -NodeBuilder& NodeBuilder::iteExpr(const Node& thenpart, const Node& elsepart) { - Assert( d_kind != UNDEFINED_KIND ); - collapse(); - d_kind = ITE; - addChild(thenpart); - addChild(elsepart); - return *this; -} - -NodeBuilder& NodeBuilder::iffExpr(const Node& right) { - Assert( d_kind != UNDEFINED_KIND ); - if(EXPECT_TRUE( d_kind != IFF )) { - collapse(); - d_kind = IFF; - } - addChild(right); - return *this; -} - -NodeBuilder& NodeBuilder::impExpr(const Node& right) { - Assert( d_kind != UNDEFINED_KIND ); - collapse(); - d_kind = IMPLIES; - addChild(right); - return *this; -} - -NodeBuilder& NodeBuilder::xorExpr(const Node& right) { - Assert( d_kind != UNDEFINED_KIND ); - if(EXPECT_TRUE( d_kind != XOR )) { - collapse(); - d_kind = XOR; - } - addChild(right); - return *this; -} - -// "Stream" expression constructor syntax -NodeBuilder& NodeBuilder::operator<<(const Kind& op) { - d_kind = op; - return *this; -} - -NodeBuilder& NodeBuilder::operator<<(const Node& child) { - addChild(child); - return *this; -} - -/** - * We keep the children either: - * (a) In the array of expression values if the number of children is less than - * nchild_thresh. Hence (last else) we increase the reference count. - * (b) If the number of children reaches the nchild_thresh, we allocate a vector - * for the children. Children are now expressions, so we also decrement the - * reference count for each child. - * (c) Otherwise we just add to the end of the vector. - */ -void NodeBuilder::addChild(ExprValue* ev) { - Assert(d_nchildren <= nchild_thresh || - d_nchildren == d_children.u_vec->size(), - "children count doesn't reflect the size of the vector!"); - Debug("expr") << "adding child ev " << ev << endl; - if(d_nchildren == nchild_thresh) { - Debug("expr") << "reached thresh " << nchild_thresh << ", copying" << endl; - vector<Node>* v = new vector<Node> (); - v->reserve(nchild_thresh + 5); - ExprValue** i = d_children.u_arr; - ExprValue** i_end = i + nchild_thresh; - for(;i != i_end; ++ i) { - v->push_back(Node(*i)); - (*i)->dec(); - } - v->push_back(Node(ev)); - d_children.u_vec = v; - ++d_nchildren; - } else if(d_nchildren > nchild_thresh) { - Debug("expr") << "over thresh " << d_nchildren - << " > " << nchild_thresh << endl; - d_children.u_vec->push_back(Node(ev)); - // ++d_nchildren; no need for this - } else { - Debug("expr") << "under thresh " << d_nchildren - << " < " << nchild_thresh << endl; - d_children.u_arr[d_nchildren ++] = ev->inc(); - } -} - -NodeBuilder& NodeBuilder::collapse() { - if(d_nchildren == nchild_thresh) { - vector<Node>* v = new vector<Node> (); - v->reserve(nchild_thresh + 5); - // - Unreachable();// unimplemented - } - return *this; -} - -}/* CVC4 namespace */ diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 5be3c284d..63048c1ac 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -1,5 +1,5 @@ /********************* -*- C++ -*- */ -/** expr_builder.h +/** node_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 @@ -14,68 +14,90 @@ #include <vector> #include <cstdlib> +#include <stdint.h> + +namespace CVC4 { + static const unsigned default_nchild_thresh = 10; + + template <unsigned nchild_thresh = default_nchild_thresh> + class NodeBuilder; + + class NodeManager; +}/* CVC4 namespace */ -#include "expr/node_manager.h" #include "expr/kind.h" #include "util/Assert.h" +#include "expr/node_value.h" namespace CVC4 { -class AndExprBuilder; -class OrExprBuilder; -class PlusExprBuilder; -class MinusExprBuilder; -class MultExprBuilder; +class AndNodeBuilder; +class OrNodeBuilder; +class PlusNodeBuilder; +class MinusNodeBuilder; +class MultNodeBuilder; +template <unsigned nchild_thresh> class NodeBuilder { - NodeManager* d_em; + unsigned d_size; - Kind d_kind; + uint64_t d_hash; + + NodeManager* d_nm; // initially false, when you extract the Node 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<Node>* u_vec; - } d_children; - - void addChild(const Node& e) { addChild(e.d_ev); } - void addChild(ExprValue*); - NodeBuilder& collapse(); + NodeValue *d_ev; + NodeValue d_inlineEv; + NodeValue *d_childrenStorage[nchild_thresh]; - typedef ExprValue** ev_iterator; - typedef ExprValue const** const_ev_iterator; + bool evIsAllocated() { + return d_ev->d_nchildren > nchild_thresh; + } - ev_iterator ev_begin() { - return d_children.u_arr; + template <unsigned N> + bool evIsAllocated(const NodeBuilder<N>& nb) { + return nb.d_ev->d_nchildren > N; } - ev_iterator ev_end() { - return d_children.u_arr + d_nchildren; + bool evNeedsToBeAllocated() { + return d_ev->d_nchildren == d_size; } - NodeBuilder& reset(const ExprValue*); + // realloc in the default way + void realloc(); + + // realloc to a specific size + void realloc(size_t toSize, bool copy = true); + + void allocateEvIfNecessaryForAppend() { + if(EXPECT_FALSE( evNeedsToBeAllocated() )) { + realloc(); + } + } public: - NodeBuilder(); - NodeBuilder(Kind k); - NodeBuilder(const Node&); - NodeBuilder(const NodeBuilder&); + inline NodeBuilder(); + inline NodeBuilder(Kind k); + inline NodeBuilder(const NodeBuilder<nchild_thresh>& nb); + template <unsigned N> inline NodeBuilder(const NodeBuilder<N>& nb); + inline NodeBuilder(NodeManager* nm); + inline NodeBuilder(NodeManager* nm, Kind k); + inline ~NodeBuilder(); - NodeBuilder(NodeManager*); - NodeBuilder(NodeManager*, Kind k); - NodeBuilder(NodeManager*, const Node&); - NodeBuilder(NodeManager*, const NodeBuilder&); + typedef NodeValue::ev_iterator iterator; + typedef NodeValue::const_ev_iterator const_iterator; - ~NodeBuilder(); + iterator begin() { return d_ev->ev_begin(); } + iterator end() { return d_ev->ev_end(); } + const_iterator begin() const { return d_ev->ev_begin(); } + const_iterator end() const { return d_ev->ev_end(); } // Compound expression constructors + /* NodeBuilder& eqExpr(const Node& right); NodeBuilder& notExpr(); NodeBuilder& andExpr(const Node& right); @@ -84,230 +106,413 @@ public: NodeBuilder& iffExpr(const Node& right); NodeBuilder& impExpr(const Node& right); NodeBuilder& xorExpr(const Node& right); + */ - /* TODO design: these modify NodeBuilder */ + /* TODO design: these modify NodeBuilder ?? */ + /* NodeBuilder& operator!() { return notExpr(); } NodeBuilder& operator&&(const Node& right) { return andExpr(right); } NodeBuilder& operator||(const Node& right) { return orExpr(right); } + */ + + /* + NodeBuilder& operator&&=(const Node& right) { return andExpr(right); } + NodeBuilder& operator||=(const Node& right) { return orExpr(right); } + */ // "Stream" expression constructor syntax - NodeBuilder& operator<<(const Kind& op); - NodeBuilder& operator<<(const Node& child); + + NodeBuilder& operator<<(const Kind& k) { + Assert(d_ev->d_kind == UNDEFINED_KIND); + d_ev->d_kind = k; + return *this; + } + + NodeBuilder& operator<<(const Node& n) { + return append(n); + } // For pushing sequences of children - NodeBuilder& append(const std::vector<Node>& children) { return append(children.begin(), children.end()); } - NodeBuilder& append(Node child) { return append(&child, (&child) + 1); } - template <class Iterator> NodeBuilder& append(const Iterator& begin, const Iterator& end); - - operator Node();// not const - - AndExprBuilder operator&&(Node); - OrExprBuilder operator||(Node); - PlusExprBuilder operator+ (Node); - PlusExprBuilder operator- (Node); - MultExprBuilder operator* (Node); - - friend class AndExprBuilder; - friend class OrExprBuilder; - friend class PlusExprBuilder; - friend class MultExprBuilder; + NodeBuilder& append(const std::vector<Node>& children) { + return append(children.begin(), children.end()); + } + + NodeBuilder& append(const Node& n) { + allocateEvIfNecessaryForAppend(); + NodeValue* ev = n.d_ev; + d_hash = NodeValue::computeHash(d_hash, ev); + ev->inc(); + d_ev->d_children[d_ev->d_nchildren++] = ev; + return *this; + } + + template <class Iterator> + NodeBuilder& append(const Iterator& begin, const Iterator& end) { + for(Iterator i = begin; i != end; ++i) { + append(*i); + } + return *this; + } + + void crop() { + if(EXPECT_FALSE( evIsAllocated() ) && d_size > d_ev->d_nchildren) { + d_ev = (NodeValue*) + std::realloc(d_ev, sizeof(NodeValue) + + ( sizeof(NodeValue*) * (d_size = d_ev->d_nchildren) )); + } + } + + // not const + operator Node(); + + /* + AndNodeBuilder operator&&(Node); + OrNodeBuilder operator||(Node); + PlusNodeBuilder operator+ (Node); + PlusNodeBuilder operator- (Node); + MultNodeBuilder operator* (Node); + + friend class AndNodeBuilder; + friend class OrNodeBuilder; + friend class PlusNodeBuilder; + friend class MultNodeBuilder; + */ };/* class NodeBuilder */ -class AndExprBuilder { +#if 0 +class AndNodeBuilder { NodeBuilder d_eb; public: - AndExprBuilder(const NodeBuilder& eb) : d_eb(eb) { + AndNodeBuilder(const NodeBuilder& eb) : d_eb(eb) { if(d_eb.d_kind != AND) { d_eb.collapse(); d_eb.d_kind = AND; } } - AndExprBuilder& operator&&(Node); - OrExprBuilder operator||(Node); + AndNodeBuilder& operator&&(Node); + OrNodeBuilder operator||(Node); operator NodeBuilder() { return d_eb; } -};/* class AndExprBuilder */ +};/* class AndNodeBuilder */ -class OrExprBuilder { +class OrNodeBuilder { NodeBuilder d_eb; public: - OrExprBuilder(const NodeBuilder& eb) : d_eb(eb) { + OrNodeBuilder(const NodeBuilder& eb) : d_eb(eb) { if(d_eb.d_kind != OR) { d_eb.collapse(); d_eb.d_kind = OR; } } - AndExprBuilder operator&&(Node); - OrExprBuilder& operator||(Node); + AndNodeBuilder operator&&(Node); + OrNodeBuilder& operator||(Node); operator NodeBuilder() { return d_eb; } -};/* class OrExprBuilder */ +};/* class OrNodeBuilder */ -class PlusExprBuilder { +class PlusNodeBuilder { NodeBuilder d_eb; public: - PlusExprBuilder(const NodeBuilder& eb) : d_eb(eb) { + PlusNodeBuilder(const NodeBuilder& eb) : d_eb(eb) { if(d_eb.d_kind != PLUS) { d_eb.collapse(); d_eb.d_kind = PLUS; } } - PlusExprBuilder& operator+(Node); - PlusExprBuilder& operator-(Node); - MultExprBuilder operator*(Node); + PlusNodeBuilder& operator+(Node); + PlusNodeBuilder& operator-(Node); + MultNodeBuilder operator*(Node); operator NodeBuilder() { return d_eb; } -};/* class PlusExprBuilder */ +};/* class PlusNodeBuilder */ -class MultExprBuilder { +class MultNodeBuilder { NodeBuilder d_eb; public: - MultExprBuilder(const NodeBuilder& eb) : d_eb(eb) { + MultNodeBuilder(const NodeBuilder& eb) : d_eb(eb) { if(d_eb.d_kind != MULT) { d_eb.collapse(); d_eb.d_kind = MULT; } } - PlusExprBuilder operator+(Node); - PlusExprBuilder operator-(Node); - MultExprBuilder& operator*(Node); + PlusNodeBuilder operator+(Node); + PlusNodeBuilder operator-(Node); + MultNodeBuilder& operator*(Node); operator NodeBuilder() { return d_eb; } -};/* class MultExprBuilder */ - -template <class Iterator> -inline NodeBuilder& NodeBuilder::append(const Iterator& begin, const Iterator& end) { - for(Iterator i = begin; i != end; ++i) - addChild(*i); - return *this; -} - -// not const -inline NodeBuilder::operator Node() { - ExprValue *ev; - uint64_t hash; - - Assert(d_kind != UNDEFINED_KIND, "Can't make an expression of an undefined kind!"); +};/* class MultNodeBuilder */ - // variables are permitted to be duplicates (from POV of the expression manager) - if(d_kind == VARIABLE) { - ev = new ExprValue; - ev->d_kind = d_kind; - ev->d_id = ExprValue::next_id++;// FIXME multithreading - return Node(ev); - } else { - if(d_nchildren <= nchild_thresh) { - hash = ExprValue::computeHash<ev_iterator>(d_kind, ev_begin(), ev_end()); - void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Node)); - ev = new (space) ExprValue; - size_t nc = 0; - ev_iterator i = ev_begin(); - ev_iterator i_end = ev_end(); - for(; i != i_end; ++i) { - // The expressions in the allocated children are all 0, so we must - // construct it without using an assignment operator - ev->d_children[nc++].assignExprValue(*i); - } - } else { - hash = ExprValue::computeHash<std::vector<Node>::const_iterator>(d_kind, d_children.u_vec->begin(), d_children.u_vec->end()); - void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Node)); - ev = new (space) ExprValue; - size_t nc = 0; - for(std::vector<Node>::iterator i = d_children.u_vec->begin(); i != d_children.u_vec->end(); ++i) - ev->d_children[nc++] = Node(*i); - } - } - - ev->d_nchildren = d_nchildren; - ev->d_kind = d_kind; - ev->d_id = ExprValue::next_id++;// FIXME multithreading - ev->d_rc = 0; - Node e(ev); - - return d_em->lookup(hash, e); -} - -inline AndExprBuilder NodeBuilder::operator&&(Node e) { - return AndExprBuilder(*this) && e; +inline AndNodeBuilder NodeBuilder::operator&&(Node e) { + return AndNodeBuilder(*this) && e; } -inline OrExprBuilder NodeBuilder::operator||(Node e) { - return OrExprBuilder(*this) || e; +inline OrNodeBuilder NodeBuilder::operator||(Node e) { + return OrNodeBuilder(*this) || e; } -inline PlusExprBuilder NodeBuilder::operator+ (Node e) { - return PlusExprBuilder(*this) + e; +inline PlusNodeBuilder NodeBuilder::operator+ (Node e) { + return PlusNodeBuilder(*this) + e; } -inline PlusExprBuilder NodeBuilder::operator- (Node e) { - return PlusExprBuilder(*this) - e; +inline PlusNodeBuilder NodeBuilder::operator- (Node e) { + return PlusNodeBuilder(*this) - e; } -inline MultExprBuilder NodeBuilder::operator* (Node e) { - return MultExprBuilder(*this) * e; +inline MultNodeBuilder NodeBuilder::operator* (Node e) { + return MultNodeBuilder(*this) * e; } -inline AndExprBuilder& AndExprBuilder::operator&&(Node e) { +inline AndNodeBuilder& AndNodeBuilder::operator&&(Node e) { d_eb.append(e); return *this; } -inline OrExprBuilder AndExprBuilder::operator||(Node e) { - return OrExprBuilder(d_eb.collapse()) || e; +inline OrNodeBuilder AndNodeBuilder::operator||(Node e) { + return OrNodeBuilder(d_eb.collapse()) || e; } -inline AndExprBuilder OrExprBuilder::operator&&(Node e) { - return AndExprBuilder(d_eb.collapse()) && e; +inline AndNodeBuilder OrNodeBuilder::operator&&(Node e) { + return AndNodeBuilder(d_eb.collapse()) && e; } -inline OrExprBuilder& OrExprBuilder::operator||(Node e) { +inline OrNodeBuilder& OrNodeBuilder::operator||(Node e) { d_eb.append(e); return *this; } -inline PlusExprBuilder& PlusExprBuilder::operator+(Node e) { +inline PlusNodeBuilder& PlusNodeBuilder::operator+(Node e) { d_eb.append(e); return *this; } -inline PlusExprBuilder& PlusExprBuilder::operator-(Node e) { +inline PlusNodeBuilder& PlusNodeBuilder::operator-(Node e) { d_eb.append(e.uMinusExpr()); return *this; } -inline MultExprBuilder PlusExprBuilder::operator*(Node e) { - return MultExprBuilder(d_eb.collapse()) * e; +inline MultNodeBuilder PlusNodeBuilder::operator*(Node e) { + return MultNodeBuilder(d_eb.collapse()) * e; } -inline PlusExprBuilder MultExprBuilder::operator+(Node e) { - return MultExprBuilder(d_eb.collapse()) + e; +inline PlusNodeBuilder MultNodeBuilder::operator+(Node e) { + return MultNodeBuilder(d_eb.collapse()) + e; } -inline PlusExprBuilder MultExprBuilder::operator-(Node e) { - return MultExprBuilder(d_eb.collapse()) - e; +inline PlusNodeBuilder MultNodeBuilder::operator-(Node e) { + return MultNodeBuilder(d_eb.collapse()) - e; } -inline MultExprBuilder& MultExprBuilder::operator*(Node e) { +inline MultNodeBuilder& MultNodeBuilder::operator*(Node e) { d_eb.append(e); return *this; } +#endif /* 0 */ + +}/* CVC4 namespace */ + +#include "expr/node.h" +#include "expr/node_manager.h" + +// template implementations + +namespace CVC4 { + +template <unsigned nchild_thresh> +inline NodeBuilder<nchild_thresh>::NodeBuilder() : + d_size(nchild_thresh), + d_nm(NodeManager::currentNM()), + d_used(false), + d_ev(&d_inlineEv), + d_inlineEv(0), + d_childrenStorage(0) {} + +template <unsigned nchild_thresh> +inline NodeBuilder<nchild_thresh>::NodeBuilder(Kind k) : + d_size(nchild_thresh), + d_nm(NodeManager::currentNM()), + d_used(false), + d_ev(&d_inlineEv), + d_inlineEv(0), + d_childrenStorage(0) { + + d_inlineEv.d_kind = k; +} + +template <unsigned nchild_thresh> +inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<nchild_thresh>& nb) : + d_size(nchild_thresh), + d_nm(nb.d_nm), + d_used(nb.d_used), + d_ev(&d_inlineEv), + d_inlineEv(0), + d_childrenStorage(0) { + + if(evIsAllocated(nb)) { + realloc(nb->d_size, false); + std::copy(d_ev->begin(), nb.d_ev->begin(), nb.d_ev->end()); + } else { + std::copy(d_inlineEv.begin(), nb.d_ev->begin(), nb.d_ev->end()); + } +} + +template <unsigned nchild_thresh> +template <unsigned N> +inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<N>& nb) : + d_size(nchild_thresh), + d_nm(NodeManager::currentNM()), + d_used(nb.d_used), + d_ev(&d_inlineEv), + d_inlineEv(0), + d_childrenStorage(0) { + + if(nb.d_ev->d_nchildren > nchild_thresh) { + realloc(nb.d_size, false); + std::copy(d_ev->begin(), nb.d_ev->begin(), nb.d_ev->end()); + } else { + std::copy(d_inlineEv.begin(), nb.d_ev->begin(), nb.d_ev->end()); + } +} + +template <unsigned nchild_thresh> +inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm) : + d_size(nchild_thresh), + d_nm(nm), + d_used(false), + d_ev(&d_inlineEv), + d_inlineEv(0), + d_childrenStorage(0) {} + +template <unsigned nchild_thresh> +inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm, Kind k) : + d_size(nchild_thresh), + d_nm(nm), + d_used(false), + d_ev(&d_inlineEv), + d_inlineEv(0), + d_childrenStorage() { + + d_inlineEv.d_kind = k; +} + +template <unsigned nchild_thresh> +inline NodeBuilder<nchild_thresh>::~NodeBuilder() { + for(iterator i = begin(); + i != end(); + ++i) { + (*i)->dec(); + } + if(evIsAllocated()) { + free(d_ev); + } +} + +template <unsigned nchild_thresh> +void NodeBuilder<nchild_thresh>::realloc() { + if(EXPECT_FALSE( evIsAllocated() )) { + d_ev = (NodeValue*) + std::realloc(d_ev, + sizeof(NodeValue) + ( sizeof(NodeValue*) * (d_size *= 2) )); + } else { + d_ev = (NodeValue*) + std::malloc(sizeof(NodeValue) + ( sizeof(NodeValue*) * (d_size *= 2) )); + d_ev->d_id = 0; + d_ev->d_rc = 0; + d_ev->d_kind = d_inlineEv.d_kind; + d_ev->d_nchildren = nchild_thresh; + std::copy(d_ev->d_children, + d_inlineEv.d_children, + d_inlineEv.d_children + nchild_thresh); + } +} + +template <unsigned nchild_thresh> +void NodeBuilder<nchild_thresh>::realloc(size_t toSize, bool copy) { + Assert( d_size < toSize ); + + if(EXPECT_FALSE( evIsAllocated() )) { + d_ev = (NodeValue*) + std::realloc(d_ev, sizeof(NodeValue) + + ( sizeof(NodeValue*) * (d_size = toSize) )); + } else { + d_ev = (NodeValue*) + std::malloc(sizeof(NodeValue) + + ( sizeof(NodeValue*) * (d_size = toSize) )); + d_ev->d_id = 0; + d_ev->d_rc = 0; + d_ev->d_kind = d_inlineEv.d_kind; + d_ev->d_nchildren = nchild_thresh; + if(copy) { + std::copy(d_ev->d_children, + d_inlineEv.d_children, + d_inlineEv.d_children + nchild_thresh); + } + } +} + +template <unsigned nchild_thresh> +NodeBuilder<nchild_thresh>::operator Node() {// not const + Assert(d_ev->d_kind != UNDEFINED_KIND, + "Can't make an expression of an undefined kind!"); + Assert(! d_used, "This NodeBuilder has already been used!"); + + // implementation differs depending on whether the expression value + // was malloc'ed or not + + if(EXPECT_FALSE( evIsAllocated() )) { + NodeValue *ev = d_nm->lookupNoInsert(d_hash, d_ev); + if(ev != d_ev) { + // expression already exists in node manager + return Node(ev); + } + + // otherwise create the canonical expression value for this node + crop(); + d_used = true; + ev = d_ev; + d_ev = NULL; + // this inserts into the NodeManager; + // return the result of lookup() in case another thread beat us to it + return d_nm->lookup(d_hash, ev); + } + + NodeValue *ev = d_nm->lookupNoInsert(d_hash, &d_inlineEv); + if(ev != &d_inlineEv) { + // expression already exists in node manager + return Node(ev); + } + + // otherwise create the canonical expression value for this node + ev = (NodeValue*) + std::malloc(sizeof(NodeValue) + + ( sizeof(NodeValue*) * d_inlineEv.d_nchildren) ); + ev->d_nchildren = d_ev->d_nchildren; + ev->d_kind = d_ev->d_kind; + ev->d_id = NodeValue::next_id++;// FIXME multithreading + ev->d_rc = 0; + d_used = true; + d_ev = NULL; + + // this inserts into the NodeManager; + // return the result of lookup() in case another thread beat us to it + return d_nm->lookup(d_hash, ev); +} }/* CVC4 namespace */ diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 8da87c9eb..ab52b9f40 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -1,5 +1,5 @@ /********************* -*- C++ -*- */ -/** expr_manager.cpp +/** node_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 @@ -18,76 +18,116 @@ namespace CVC4 { __thread NodeManager* NodeManager::s_current = 0; -Node NodeManager::lookup(uint64_t hash, const Node& e) { - Assert(this != NULL, "Woops, we have a bad expression manager!"); +Node NodeManager::lookup(uint64_t hash, NodeValue* ev) { + Assert(this != NULL, "Whoops, we have a bad expression manager!"); hash_t::iterator i = d_hash.find(hash); if(i == d_hash.end()) { // insert std::vector<Node> v; + Node e(ev); v.push_back(e); d_hash.insert(std::make_pair(hash, v)); return e; } else { for(std::vector<Node>::iterator j = i->second.begin(); j != i->second.end(); ++j) { - if(e.getKind() != j->getKind()) + if(ev->getKind() != j->getKind()) { continue; + } - if(e.numChildren() != j->numChildren()) + if(ev->numChildren() != j->numChildren()) { continue; + } - Node::const_iterator c1 = e.begin(); - Node::iterator c2 = j->begin(); - for(; c1 != e.end() && c2 != j->end(); ++c1, ++c2) { - if(c1->d_ev != c2->d_ev) + NodeValue::const_iterator c1 = ev->ev_begin(); + NodeValue::iterator c2 = j->d_ev->ev_begin(); + for(; c1 != ev->ev_end() && c2 != j->d_ev->ev_end(); ++c1, ++c2) { + if((*c1).d_ev != (*c2).d_ev) { break; + } } - if(c1 != e.end() || c2 != j->end()) + if(c1 != ev->ev_end() || c2 != j->end()) { continue; + } return *j; } // didn't find it, insert std::vector<Node> v; + Node e(ev); v.push_back(e); d_hash.insert(std::make_pair(hash, v)); return e; } } +NodeValue* NodeManager::lookupNoInsert(uint64_t hash, NodeValue* ev) { + Assert(this != NULL, "Whoops, we have a bad expression manager!"); + hash_t::iterator i = d_hash.find(hash); + if(i == d_hash.end()) { + return NULL; + } else { + for(std::vector<Node>::iterator j = i->second.begin(); j != i->second.end(); ++j) { + if(ev->getKind() != j->getKind()) { + continue; + } + + if(ev->numChildren() != j->numChildren()) { + continue; + } + + NodeValue::const_iterator c1 = ev->ev_begin(); + NodeValue::iterator c2 = j->d_ev->ev_begin(); + for(; c1 != ev->ev_end() && c2 != j->d_ev->ev_end(); ++c1, ++c2) { + if((*c1).d_ev != (*c2).d_ev) { + break; + } + } + + if(c1 != ev->ev_end() || c2 != j->end()) { + continue; + } + + return j->d_ev; + } + // didn't find it + return 0; + } +} + // general expression-builders Node NodeManager::mkExpr(Kind kind) { - return NodeBuilder(this, kind); + return NodeBuilder<>(this, kind); } Node NodeManager::mkExpr(Kind kind, const Node& child1) { - return NodeBuilder(this, kind) << child1; + return NodeBuilder<>(this, kind) << child1; } Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2) { - return NodeBuilder(this, kind) << child1 << child2; + return NodeBuilder<>(this, kind) << child1 << child2; } Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3) { - return NodeBuilder(this, kind) << child1 << child2 << child3; + return NodeBuilder<>(this, kind) << child1 << child2 << child3; } Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4) { - return NodeBuilder(this, kind) << child1 << child2 << child3 << child4; + return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4; } Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5) { - return NodeBuilder(this, kind) << child1 << child2 << child3 << child4 << child5; + return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4 << child5; } // N-ary version Node NodeManager::mkExpr(Kind kind, const std::vector<Node>& children) { - return NodeBuilder(this, kind).append(children); + return NodeBuilder<>(this, kind).append(children); } Node NodeManager::mkVar() { - return NodeBuilder(this, VARIABLE); + return NodeBuilder<>(this, VARIABLE); } }/* CVC4 namespace */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 6c20b29e8..3a28a22ff 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -20,22 +20,20 @@ namespace CVC4 { -namespace expr { - class ExprBuilder; -}/* CVC4::expr namespace */ - class NodeManager { static __thread NodeManager* s_current; - friend class CVC4::NodeBuilder; + template <unsigned> friend class CVC4::NodeBuilder; typedef std::map<uint64_t, std::vector<Node> > hash_t; hash_t d_hash; - Node lookup(uint64_t hash, const Node& e); + Node lookup(uint64_t hash, const Node& e) { return lookup(hash, e.d_ev); } + Node lookup(uint64_t hash, NodeValue* e); + NodeValue* lookupNoInsert(uint64_t hash, NodeValue* e); public: - static NodeManager* currentEM() { return s_current; } + static NodeManager* currentNM() { return s_current; } // general expression-builders Node mkExpr(Kind kind); @@ -50,20 +48,20 @@ public: // variables are special, because duplicates are permitted Node mkVar(); - // TODO: these use the current EM (but must be renamed) + // TODO: these use the current NM (but must be renamed) /* static Node mkExpr(Kind kind) - { currentEM()->mkExpr(kind); } + { currentNM()->mkExpr(kind); } static Node mkExpr(Kind kind, Node child1); - { currentEM()->mkExpr(kind, child1); } + { currentNM()->mkExpr(kind, child1); } static Node mkExpr(Kind kind, Node child1, Node child2); - { currentEM()->mkExpr(kind, child1, child2); } + { currentNM()->mkExpr(kind, child1, child2); } static Node mkExpr(Kind kind, Node child1, Node child2, Node child3); - { currentEM()->mkExpr(kind, child1, child2, child3); } + { currentNM()->mkExpr(kind, child1, child2, child3); } static Node mkExpr(Kind kind, Node child1, Node child2, Node child3, Node child4); - { currentEM()->mkExpr(kind, child1, child2, child3, child4); } + { currentNM()->mkExpr(kind, child1, child2, child3, child4); } static Node mkExpr(Kind kind, Node child1, Node child2, Node child3, Node child4, Node child5); - { currentEM()->mkExpr(kind, child1, child2, child3, child4, child5); } + { currentNM()->mkExpr(kind, child1, child2, child3, child4, child5); } */ // do we want a varargs one? perhaps not.. diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp new file mode 100644 index 000000000..7af2cd2b5 --- /dev/null +++ b/src/expr/node_value.cpp @@ -0,0 +1,147 @@ +/********************* -*- C++ -*- */ +/** node_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::Node rather than by pointer; cvc4::Node maintains the + ** reference count on NodeValue instances and + **/ + +#include "node_value.h" +#include <sstream> + +using namespace std; + +namespace CVC4 { + +size_t NodeValue::next_id = 1; + +NodeValue::NodeValue() : + d_id(0), d_rc(MAX_RC), d_kind(NULL_EXPR), d_nchildren(0) { +} + +NodeValue::NodeValue(int) : + d_id(0), d_rc(0), d_kind(unsigned(UNDEFINED_KIND)), d_nchildren(0) { +} + +NodeValue::~NodeValue() { + for(ev_iterator i = ev_begin(); i != ev_end(); ++i) { + (*i)->dec(); + } +} + +uint64_t NodeValue::hash() const { + return computeHash(d_kind, ev_begin(), ev_end()); +} + +NodeValue* NodeValue::inc() { + // FIXME multithreading + if(d_rc < MAX_RC) + ++d_rc; + return this; +} + +NodeValue* NodeValue::dec() { + // FIXME multithreading + if(d_rc < MAX_RC) { + if(--d_rc == 0) { + // FIXME gc + return 0; + } + } + return this; +} + +NodeValue::iterator NodeValue::begin() { + return node_iterator(d_children); +} + +NodeValue::iterator NodeValue::end() { + return node_iterator(d_children + d_nchildren); +} + +NodeValue::iterator NodeValue::rbegin() { + return node_iterator(d_children + d_nchildren - 1); +} + +NodeValue::iterator NodeValue::rend() { + return node_iterator(d_children - 1); +} + +NodeValue::const_iterator NodeValue::begin() const { + return const_node_iterator(d_children); +} + +NodeValue::const_iterator NodeValue::end() const { + return const_node_iterator(d_children + d_nchildren); +} + +NodeValue::const_iterator NodeValue::rbegin() const { + return const_node_iterator(d_children + d_nchildren - 1); +} + +NodeValue::const_iterator NodeValue::rend() const { + return const_node_iterator(d_children - 1); +} + +NodeValue::ev_iterator NodeValue::ev_begin() { + return d_children; +} + +NodeValue::ev_iterator NodeValue::ev_end() { + return d_children + d_nchildren; +} + +NodeValue::ev_iterator NodeValue::ev_rbegin() { + return d_children + d_nchildren - 1; +} + +NodeValue::ev_iterator NodeValue::ev_rend() { + return d_children - 1; +} + +NodeValue::const_ev_iterator NodeValue::ev_begin() const { + return d_children; +} + +NodeValue::const_ev_iterator NodeValue::ev_end() const { + return d_children + d_nchildren; +} + +NodeValue::const_ev_iterator NodeValue::ev_rbegin() const { + return d_children + d_nchildren - 1; +} + +NodeValue::const_ev_iterator NodeValue::ev_rend() const { + return d_children - 1; +} + +string NodeValue::toString() const { + stringstream ss; + toStream(ss); + return ss.str(); +} + +void NodeValue::toStream(std::ostream& out) const { + out << "(" << Kind(d_kind); + if(d_kind == VARIABLE) { + out << ":" << this; + } else { + for(const_iterator i = begin(); i != end(); ++i) { + if(i != end()) { + out << " "; + } + out << *i; + } + } + out << ")"; +} + +}/* CVC4 namespace */ diff --git a/src/expr/expr_value.h b/src/expr/node_value.h index 25fada4af..9bdbb7f8c 100644 --- a/src/expr/expr_value.h +++ b/src/expr/node_value.h @@ -1,5 +1,5 @@ /********************* -*- C++ -*- */ -/** expr_value.h +/** node_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 @@ -11,15 +11,15 @@ ** ** Instances of this class are generally referenced through ** cvc4::Node rather than by pointer; cvc4::Node maintains the - ** reference count on ExprValue instances and + ** reference count on NodeValue instances and **/ -/* this must be above the check for __CVC4__EXPR__EXPR_VALUE_H */ +/* this must be above the check for __CVC4__EXPR__NODE_VALUE_H */ /* to resolve a circular dependency */ -#include "expr/node.h" +//#include "expr/node.h" -#ifndef __CVC4__EXPR__EXPR_VALUE_H -#define __CVC4__EXPR__EXPR_VALUE_H +#ifndef __CVC4__EXPR__NODE_VALUE_H +#define __CVC4__EXPR__NODE_VALUE_H #include "cvc4_config.h" #include <stdint.h> @@ -30,17 +30,18 @@ namespace CVC4 { class Node; -class NodeBuilder; +template <unsigned> class NodeBuilder; +class NodeManager; namespace expr { /** - * This is an ExprValue. + * This is an NodeValue. */ -class ExprValue { +class NodeValue { /** A convenient null-valued expression value */ - static ExprValue s_null; + static NodeValue s_null; /** Maximum reference count possible. Used for sticky * reference-counting. Should be (1 << num_bits(d_rc)) - 1 */ @@ -61,25 +62,32 @@ class ExprValue { unsigned d_nchildren : 16; /** Variable number of child nodes */ - Node d_children[0]; + NodeValue *d_children[0]; // todo add exprMgr ref in debug case friend class CVC4::Node; - friend class CVC4::NodeBuilder; + template <unsigned> friend class CVC4::NodeBuilder; + friend class CVC4::NodeManager; - ExprValue* inc(); - ExprValue* dec(); + NodeValue* inc(); + NodeValue* dec(); static size_t next_id; /** Private default constructor for the null value. */ - ExprValue(); + NodeValue(); + + /** Private default constructor for the NodeBuilder. */ + NodeValue(int); + + /** Destructor decrements the ref counts of its children */ + ~NodeValue(); /** * Computes the hash over the given iterator span of children, and the * root hash. The iterator should be either over a range of Node or pointers - * to ExprValue. + * to NodeValue. * @param hash the initial value for the hash * @param begin the begining of the range * @param end the end of the range @@ -87,11 +95,55 @@ class ExprValue { */ template<typename const_iterator_type> static uint64_t computeHash(uint64_t hash, const_iterator_type begin, const_iterator_type end) { - for(const_iterator_type i = begin; i != end; ++i) - hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ (*i)->getId(); + for(const_iterator_type i = begin; i != end; ++i) { + hash = computeHash(hash, *i); + } return hash; } + static uint64_t computeHash(uint64_t hash, const NodeValue* ev) { + return ( (hash << 3) | ((hash & 0xE000000000000000ull) >> 61) ) ^ ev->getId(); + } + + typedef NodeValue** ev_iterator; + typedef NodeValue const* const* const_ev_iterator; + + ev_iterator ev_begin(); + ev_iterator ev_end(); + ev_iterator ev_rbegin(); + ev_iterator ev_rend(); + + const_ev_iterator ev_begin() const; + const_ev_iterator ev_end() const; + const_ev_iterator ev_rbegin() const; + const_ev_iterator ev_rend() const; + + class node_iterator { + const_ev_iterator d_i; + public: + node_iterator(const_ev_iterator i) : d_i(i) {} + + inline Node operator*(); + + bool operator==(const node_iterator& i) { + return d_i == i.d_i; + } + + bool operator!=(const node_iterator& i) { + return d_i != i.d_i; + } + + node_iterator& operator++() { + ++d_i; + return *this; + } + + node_iterator operator++(int) { + return node_iterator(d_i++); + } + }; + typedef node_iterator const_node_iterator; + public: /** Hash this expression. * @return the hash value of this expression. */ @@ -99,8 +151,8 @@ public: // Iterator support - typedef Node* iterator; - typedef Node const* const_iterator; + typedef node_iterator iterator; + typedef node_iterator const_iterator; iterator begin(); iterator end(); @@ -113,7 +165,8 @@ public: const_iterator rend() const; unsigned getId() const { return d_id; } - unsigned getKind() const { return (Kind) d_kind; } + Kind getKind() const { return (Kind) d_kind; } + unsigned numChildren() const { return d_nchildren; } std::string toString() const; void toStream(std::ostream& out) const; }; @@ -121,4 +174,16 @@ public: }/* CVC4::expr namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__EXPR__EXPR_VALUE_H */ +#include "expr/node.h" + +namespace CVC4 { +namespace expr { + +inline Node NodeValue::node_iterator::operator*() { + return Node(*d_i); +} + +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__EXPR__NODE_VALUE_H */ |