diff options
author | Cesare Tinelli <cesare-tinelli@uiowa.edu> | 2010-02-22 18:59:37 +0000 |
---|---|---|
committer | Cesare Tinelli <cesare-tinelli@uiowa.edu> | 2010-02-22 18:59:37 +0000 |
commit | 9ae657c4568114eb888d9c0b8c27c09586556ff3 (patch) | |
tree | 1abb476b99c20c3c8906d8893159923eb0ccce3a /src/expr/node.cpp | |
parent | 533ed01ce6fdd3b93130b7ba0dbeedcd807a7a1f (diff) |
* Add virtual destructors to CnfStream, Theory, OutputChannel, and
ExplainOutputChannel. Safer and stops a compiler warning.
* node attributes: fix compiler warnings on 64-bit.
* Node: add asserts to make sure the current NodeManager is non-NULL
when it's needed. This can happen when public-facing functions
don't properly set the node manager, and it can look like a bug in
another part of the library. Also some code format cleanup.
* configure.ac, config/cvc4.m4: added --enable-static-binary (see
discussion on bug 32), fixed bad configure lines (bug 19), added
documentation for some things.
* config.h.in: removed; it's auto-generated.
Diffstat (limited to 'src/expr/node.cpp')
-rw-r--r-- | src/expr/node.cpp | 44 |
1 files changed, 38 insertions, 6 deletions
diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 644570b24..79490d58e 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -97,51 +97,83 @@ Node& Node::operator=(const Node& e) { } Node Node::eqExpr(const Node& right) const { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->mkNode(EQUAL, *this, right); } Node Node::notExpr() const { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->mkNode(NOT, *this); } Node Node::andExpr(const Node& right) const { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->mkNode(AND, *this, right); } Node Node::orExpr(const Node& right) const { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->mkNode(OR, *this, right); } Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart); } Node Node::iffExpr(const Node& right) const { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->mkNode(IFF, *this, right); } Node Node::impExpr(const Node& right) const { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->mkNode(IMPLIES, *this, right); } Node Node::xorExpr(const Node& right) const { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->mkNode(XOR, *this, right); } -static void indent(ostream & o, int indent){ - for(int i=0; i < indent; i++) +static void indent(ostream & o, int indent) { + for(int i=0; i < indent; i++) { o << ' '; + } } void Node::printAst(ostream & o, int ind) const { indent(o, ind); o << '('; o << getKind(); - if(getKind() == VARIABLE){ + if(getKind() == VARIABLE) { o << ' ' << getId(); - - }else if(getNumChildren() >= 1){ - for(Node::iterator child = begin(); child != end(); ++child){ + } else if(getNumChildren() >= 1) { + for(Node::iterator child = begin(); child != end(); ++child) { o << endl; (*child).printAst(o, ind + 1); } |