diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-12-16 04:25:45 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-12-16 04:25:45 +0000 |
commit | 79df573326e6911d3a97fcc2528105acd1c2c525 (patch) | |
tree | 70930bcdb620cdf8ff9e3e9c495f67ed8317aa2e /src/expr/node_builder.h | |
parent | 8cb3a7b556e8b4b85745bffbd1f0246e6af29588 (diff) |
Fixes to the build system:
Makefile.am files - remove obsolete INCLUDES, incorporate into AM_CPPFLAGS
Makefile files in src/ - support "make" under src/ (current build profile)
configure.ac - updates to fix warnings
config/antlr.m4 - updates to fix warnings
autogen.sh - updates to generate warnings from autotools; also support Macs
src/include/cvc4_config.h - guard with #ifdef
total reimplementation of NodeBuilder
ExprValue => NodeValue
context_mm.{h,cpp} - fixed numerous compile errors
Diffstat (limited to 'src/expr/node_builder.h')
-rw-r--r-- | src/expr/node_builder.h | 513 |
1 files changed, 359 insertions, 154 deletions
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 */ |