Re-committing revision 232 properly:

* 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 33), fixed bad configure lines (bug 19), added
  documentation for some things.

* config.h.in: removed; it's auto-generated.

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);
     }