diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-03-05 08:26:37 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-03-05 08:26:37 +0000 |
commit | 88b52c971b43248e6ceacf1c8140a06427d0418d (patch) | |
tree | 4ee443c898a858fcdd658f3f043e4180eddd8784 /src/expr/node_builder.h | |
parent | 29cc307cdf2c42bebf4f5615874a864783f47fd0 (diff) |
* public/private code untangled (smt/smt_engine.h no longer #includes
expr/node.h). This removes the warnings we had during compilation,
and heads off a number of potential linking errors due to improper
inlining of private (library-only) stuff in client (out-of-library)
code.
* "configure" now takes some options as part of a "bare-option" build
type (e.g., "./configure debug-coverage" or "./configure production-muzzle").
* split cdo.h, cdlist.h, cdmap.h, and cdset.h from context.h
* split cdlist_black unit test from context_black
* implement CDMap<>.
* give ExprManagers ownership of the context (and have SmtEngine share
that one)
* fix main driver to properly report file-not-found
* fix MemoryMappedInputBuffer class to report reasons for
"errno"-returned system errors
* src/expr/attribute.h: context-dependent attribute kinds now
supported
* test/unit/expr/node_white.h: context-dependent attribute tests
* src/prop/cnf_conversion.h and associated parts of src/util/options.h
and src/main/getopt.cpp: obsolete command-line option, removed.
* src/util/Assert.h: assertions are now somewhat more useful (in debug
builds, anyway) during stack unwinding.
* test/unit/theory/theory_black.h: test context-dependent behavior of
registerTerm() attribute for theories
* src/expr/node_builder.h: formatting, fixes for arithmetic
convenience node builders, check memory allocations
* test/unit/expr/node_builder_black.h: add tessts for addition,
subtraction, unary minus, and multiplication convenience node
builders
* src/expr/attribute.h: more comments
* (various) code formatting, comment cleanup, added throws specifier
to some destructors
* contrib/code-checker: prototype perl script to test (some) code policy
* contrib/indent-settings: command line for GNU indent to indent using
CVC4 style (sort of; this is a work in progress)
* COPYING: legal stuff
* DESIGN_QUESTIONS: obsolete, removed
Diffstat (limited to 'src/expr/node_builder.h')
-rw-r--r-- | src/expr/node_builder.h | 145 |
1 files changed, 114 insertions, 31 deletions
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 4dc3c06d0..42ca9db2b 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -47,7 +47,6 @@ inline std::ostream& operator<<(std::ostream&, const NodeBuilder<nchild_thresh>& class AndNodeBuilder; class OrNodeBuilder; class PlusNodeBuilder; -class MinusNodeBuilder; class MultNodeBuilder; template <unsigned nchild_thresh> @@ -63,7 +62,7 @@ class NodeBuilder { // extract another bool d_used; - expr::NodeValue *d_nv; + expr::NodeValue* d_nv; expr::NodeValue d_inlineNv; expr::NodeValue *d_childrenStorage[nchild_thresh]; @@ -93,7 +92,7 @@ class NodeBuilder { } // dealloc: only call this with d_used == false and nvIsAllocated() - inline void dealloc() throw(); + inline void dealloc(); void crop() { Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); @@ -101,6 +100,9 @@ class NodeBuilder { d_nv = (expr::NodeValue*) std::realloc(d_nv, sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * (d_size = d_nv->d_nchildren) )); + if(d_nv == NULL) { + throw std::bad_alloc(); + } } } @@ -126,7 +128,7 @@ public: template <unsigned N> inline NodeBuilder(const NodeBuilder<N>& nb); inline NodeBuilder(NodeManager* nm); inline NodeBuilder(NodeManager* nm, Kind k); - inline ~NodeBuilder() throw(); + inline ~NodeBuilder(); typedef expr::NodeValue::iterator<true> iterator; typedef expr::NodeValue::iterator<true> const_iterator; @@ -223,9 +225,10 @@ public: friend class PlusNodeBuilder; friend class MultNodeBuilder; - //Yet 1 more example of how terrifying C++ is as a language - //This is needed for copy constructors of different sizes to access private fields - template <unsigned N> friend class NodeBuilder; + // Yet 1 more example of how terrifying C++ is as a language + // This is needed for copy constructors of different sizes to access private fields + template <unsigned N> + friend class NodeBuilder; };/* class NodeBuilder */ @@ -423,14 +426,24 @@ inline MultNodeBuilder PlusNodeBuilder::operator*(const NodeTemplate<rc>& n) { return MultNodeBuilder(Node(d_eb), n); } -/* -inline PlusNodeBuilder& PlusNodeBuilder::operator+(PlusNodeBuilder& b) { return *this + Node(d_eb); } -inline PlusNodeBuilder& PlusNodeBuilder::operator+(MultNodeBuilder& b) { return *this + Node(d_eb); } -inline PlusNodeBuilder& PlusNodeBuilder::operator-(PlusNodeBuilder& b) { return *this - Node(d_eb); } -inline PlusNodeBuilder& PlusNodeBuilder::operator-(MultNodeBuilder& b) { return *this - Node(d_eb); } -inline MultNodeBuilder PlusNodeBuilder::operator*(PlusNodeBuilder& b) { return *this * Node(d_eb); } -inline MultNodeBuilder PlusNodeBuilder::operator*(MultNodeBuilder& b) { return *this * Node(d_eb); } -*/ +inline PlusNodeBuilder& operator+(PlusNodeBuilder& a, const PlusNodeBuilder& b) { + return a + Node(b.d_eb); +} +inline PlusNodeBuilder& operator+(PlusNodeBuilder& a, const MultNodeBuilder& b) { + return a + Node(b.d_eb); +} +inline PlusNodeBuilder& operator-(PlusNodeBuilder&a, const PlusNodeBuilder& b) { + return a - Node(b.d_eb); +} +inline PlusNodeBuilder& operator-(PlusNodeBuilder& a, const MultNodeBuilder& b) { + return a - Node(b.d_eb); +} +inline MultNodeBuilder operator*(PlusNodeBuilder& a, const PlusNodeBuilder& b) { + return a * Node(b.d_eb); +} +inline MultNodeBuilder operator*(PlusNodeBuilder& a, const MultNodeBuilder& b) { + return a * Node(b.d_eb); +} template <bool rc> inline PlusNodeBuilder MultNodeBuilder::operator+(const NodeTemplate<rc>& n) { @@ -439,7 +452,7 @@ inline PlusNodeBuilder MultNodeBuilder::operator+(const NodeTemplate<rc>& n) { template <bool rc> inline PlusNodeBuilder MultNodeBuilder::operator-(const NodeTemplate<rc>& n) { - return PlusNodeBuilder(Node(d_eb), n); + return PlusNodeBuilder(Node(d_eb), NodeManager::currentNM()->mkNode(kind::UMINUS, n)); } template <bool rc> @@ -448,14 +461,24 @@ inline MultNodeBuilder& MultNodeBuilder::operator*(const NodeTemplate<rc>& n) { return *this; } -/* -inline PlusNodeBuilder MultNodeBuilder::operator+(const PlusNodeBuilder& b) { return *this + Node(d_eb); } -inline PlusNodeBuilder MultNodeBuilder::operator+(const MultNodeBuilder& b) { return *this + Node(d_eb); } -inline PlusNodeBuilder MultNodeBuilder::operator-(const PlusNodeBuilder& b) { return *this - Node(d_eb); } -inline PlusNodeBuilder MultNodeBuilder::operator-(const MultNodeBuilder& b) { return *this - Node(d_eb); } -inline MultNodeBuilder& MultNodeBuilder::operator*(const PlusNodeBuilder& b) { return *this * Node(d_eb); } -inline MultNodeBuilder& MultNodeBuilder::operator*(const MultNodeBuilder& b) { return *this * Node(d_eb); } -*/ +inline PlusNodeBuilder operator+(MultNodeBuilder& a, const PlusNodeBuilder& b) { + return a + Node(b.d_eb); +} +inline PlusNodeBuilder operator+(MultNodeBuilder& a, const MultNodeBuilder& b) { + return a + Node(b.d_eb); +} +inline PlusNodeBuilder operator-(MultNodeBuilder& a, const PlusNodeBuilder& b) { + return a - Node(b.d_eb); +} +inline PlusNodeBuilder operator-(MultNodeBuilder& a, const MultNodeBuilder& b) { + return a - Node(b.d_eb); +} +inline MultNodeBuilder& operator*(MultNodeBuilder& a, const PlusNodeBuilder& b) { + return a * Node(b.d_eb); +} +inline MultNodeBuilder& operator*(MultNodeBuilder& a, const MultNodeBuilder& b) { + return a * Node(b.d_eb); +} template <bool rc1, bool rc2> inline AndNodeBuilder operator&&(const NodeTemplate<rc1>& a, const NodeTemplate<rc2>& b) { @@ -502,6 +525,41 @@ inline OrNodeBuilder operator||(const NodeTemplate<rc>& a, const OrNodeBuilder& return a || Node(b.d_eb); } +template <bool rc> +inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a, const PlusNodeBuilder& b) { + return a + Node(b.d_eb); +} + +template <bool rc> +inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a, const MultNodeBuilder& b) { + return a + Node(b.d_eb); +} + +template <bool rc> +inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a, const PlusNodeBuilder& b) { + return a - Node(b.d_eb); +} + +template <bool rc> +inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a, const MultNodeBuilder& b) { + return a - Node(b.d_eb); +} + +template <bool rc> +inline MultNodeBuilder operator*(const NodeTemplate<rc>& a, const PlusNodeBuilder& b) { + return a * Node(b.d_eb); +} + +template <bool rc> +inline MultNodeBuilder operator*(const NodeTemplate<rc>& a, const MultNodeBuilder& b) { + return a * Node(b.d_eb); +} + +template <bool rc> +inline NodeTemplate<true> operator-(const NodeTemplate<rc>& a) { + return NodeManager::currentNM()->mkNode(kind::UMINUS, a); +} + }/* CVC4 namespace */ #include "expr/node.h" @@ -611,7 +669,7 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm, Kind k) : } template <unsigned nchild_thresh> -inline NodeBuilder<nchild_thresh>::~NodeBuilder() throw() { +inline NodeBuilder<nchild_thresh>::~NodeBuilder() { if(!d_used) { // Warning("NodeBuilder unused at destruction\n"); // Commented above, as it happens a lot, for example with exceptions @@ -642,9 +700,15 @@ void NodeBuilder<nchild_thresh>::realloc() { d_nv = (expr::NodeValue*) std::realloc(d_nv, sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * (d_size *= 2) )); + if(d_nv == NULL) { + throw std::bad_alloc(); + } } else { d_nv = (expr::NodeValue*) std::malloc(sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * (d_size *= 2) )); + if(d_nv == NULL) { + throw std::bad_alloc(); + } d_nv->d_id = 0; d_nv->d_rc = 0; d_nv->d_kind = d_inlineNv.d_kind; @@ -663,10 +727,16 @@ void NodeBuilder<nchild_thresh>::realloc(size_t toSize, bool copy) { d_nv = (expr::NodeValue*) std::realloc(d_nv, sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * (d_size = toSize) )); + if(d_nv == NULL) { + throw std::bad_alloc(); + } } else { d_nv = (expr::NodeValue*) std::malloc(sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * (d_size = toSize) )); + if(d_nv == NULL) { + throw std::bad_alloc(); + } d_nv->d_id = 0; d_nv->d_rc = 0; d_nv->d_kind = d_inlineNv.d_kind; @@ -682,12 +752,11 @@ void NodeBuilder<nchild_thresh>::realloc(size_t toSize, bool copy) { } template <unsigned nchild_thresh> -inline void NodeBuilder<nchild_thresh>::dealloc() throw() { +inline void NodeBuilder<nchild_thresh>::dealloc() { /* Prefer asserts to if() because usually these conditions have been * checked already, so we don't want to do a double-check in * production; these are just sanity checks for debug builds */ - DtorAssert(!d_used, - "Internal error: NodeBuilder: dealloc() called with d_used"); + Assert(!d_used, "Internal error: NodeBuilder: dealloc() called with d_used"); for(expr::NodeValue::nv_iterator i = d_nv->nv_begin(); i != d_nv->nv_end(); @@ -707,9 +776,12 @@ NodeBuilder<nchild_thresh>::operator Node() const {// const version if(d_nv->d_kind == kind::VARIABLE) { Assert(d_nv->d_nchildren == 0); - expr::NodeValue *nv = (expr::NodeValue*) + expr::NodeValue* nv = (expr::NodeValue*) std::malloc(sizeof(expr::NodeValue) + (sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));// FIXME :: WTF?? + if(nv == NULL) { + throw std::bad_alloc(); + } nv->d_nchildren = 0; nv->d_kind = kind::VARIABLE; nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading @@ -736,6 +808,9 @@ NodeBuilder<nchild_thresh>::operator Node() const {// const version nv = (expr::NodeValue*) std::malloc(sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * d_nv->d_nchildren )); + if(nv == NULL) { + throw std::bad_alloc(); + } nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading nv->d_rc = 0; nv->d_kind = d_nv->d_kind; @@ -767,6 +842,9 @@ NodeBuilder<nchild_thresh>::operator Node() const {// const version ev = (expr::NodeValue*) std::malloc(sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren )); + if(ev == NULL) { + throw std::bad_alloc(); + } ev->d_nchildren = d_inlineNv.d_nchildren; ev->d_kind = d_inlineNv.d_kind; ev->d_id = expr::NodeValue::next_id++;// FIXME multithreading @@ -797,9 +875,12 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const if(d_nv->d_kind == kind::VARIABLE) { Assert(d_nv->d_nchildren == 0); - expr::NodeValue *nv = (expr::NodeValue*) + expr::NodeValue* nv = (expr::NodeValue*) std::malloc(sizeof(expr::NodeValue) + (sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));// FIXME :: WTF?? + if(nv == NULL) { + throw std::bad_alloc(); + } nv->d_nchildren = 0; nv->d_kind = kind::VARIABLE; nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading @@ -847,6 +928,9 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const ev = (expr::NodeValue*) std::malloc(sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren )); + if(ev == NULL) { + throw std::bad_alloc(); + } ev->d_nchildren = d_inlineNv.d_nchildren; ev->d_kind = d_inlineNv.d_kind; ev->d_id = expr::NodeValue::next_id++;// FIXME multithreading @@ -866,7 +950,6 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const template <unsigned nchild_thresh> inline std::ostream& operator<<(std::ostream& out, const NodeBuilder<nchild_thresh>& b) { - b.toStream(out); return out; } |