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.

3 files changed, 86 insertions, 33 deletions

diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 12de9eb5f..1d2705240 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -56,7 +56,7 @@ namespace expr {
 
 struct AttrHashFcn {
   enum { LARGE_PRIME = 1 };
-  std::size_t operator()(const std::pair<unsigned, SoftNode>& p) const {
+  std::size_t operator()(const std::pair<uint64_t, SoftNode>& p) const {
     return p.first * LARGE_PRIME + p.second.hash();
   }
 };
@@ -122,7 +122,7 @@ struct KindTableMapping {
 
 // use a TAG to indicate which table it should be in
 template <class value_type>
-struct AttrHash : public __gnu_cxx::hash_map<std::pair<unsigned, SoftNode>, value_type, AttrHashFcn> {};
+struct AttrHash : public __gnu_cxx::hash_map<std::pair<uint64_t, SoftNode>, value_type, AttrHashFcn> {};
 
 template <>
 class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHashBoolFcn> {
@@ -215,19 +215,23 @@ class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHas
 
 public:
 
-  typedef std::pair<unsigned, SoftNode> key_type;
+  typedef std::pair<uint64_t, SoftNode> key_type;
   typedef bool data_type;
   typedef std::pair<const key_type, data_type> value_type;
 
   typedef BitIterator iterator;
   typedef ConstBitIterator const_iterator;
 
-  BitIterator find(const std::pair<unsigned, SoftNode>& k) {
+  BitIterator find(const std::pair<uint64_t, SoftNode>& k) {
     super::iterator i = super::find(k.second);
     if(i == super::end()) {
       return BitIterator();
     }
-    Debug.printf("boolattr", "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", &(*i).second, (*i).second, k.first);
+    Debug.printf("boolattr",
+                 "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
+                 &(*i).second,
+                 (unsigned long long)((*i).second),
+                 unsigned(k.first));
     return BitIterator(*i, k.first);
   }
 
@@ -235,12 +239,16 @@ public:
     return BitIterator();
   }
 
-  ConstBitIterator find(const std::pair<unsigned, SoftNode>& k) const {
+  ConstBitIterator find(const std::pair<uint64_t, SoftNode>& k) const {
     super::const_iterator i = super::find(k.second);
     if(i == super::end()) {
       return ConstBitIterator();
     }
-    Debug.printf("boolattr", "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", &(*i).second, (*i).second, k.first);
+    Debug.printf("boolattr",
+                 "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
+                 &(*i).second,
+                 (unsigned long long)((*i).second),
+                 unsigned(k.first));
     return ConstBitIterator(*i, k.first);
   }
 
@@ -248,7 +256,7 @@ public:
     return ConstBitIterator();
   }
 
-  BitAccessor operator[](const std::pair<unsigned, SoftNode>& k) {
+  BitAccessor operator[](const std::pair<uint64_t, SoftNode>& k) {
     uint64_t& word = super::operator[](k.second);
     return BitAccessor(word, k.first);
   }
@@ -268,18 +276,18 @@ struct Attribute {
   /** cleanup routine when the Node goes away */
   static inline void cleanup(const value_t&) {}
 
-  static inline unsigned getId() { return s_id; }
-  static inline unsigned getHashValue() { return s_hashValue; }
+  static inline uint64_t getId() { return s_id; }
+  static inline uint64_t getHashValue() { return s_hashValue; }
 
   static const bool has_default_value = false;
 
 private:
 
   /** an id */
-  static const unsigned s_id;
+  static const uint64_t s_id;
 
   /** an extra hash value (to avoid same-value-type collisions) */
-  static const unsigned s_hashValue;
+  static const uint64_t s_hashValue;
 };
 
 /**
@@ -294,13 +302,13 @@ struct Attribute<T, bool> {
   /** cleanup routine when the Node goes away */
   static inline void cleanup(const bool&) {}
 
-  static inline unsigned getId() { return s_id; }
-  static inline unsigned getHashValue() { return s_hashValue; }
+  static inline uint64_t getId() { return s_id; }
+  static inline uint64_t getHashValue() { return s_hashValue; }
 
   static const bool has_default_value = true;
   static const bool default_value = false;
 
-  static inline unsigned checkID(unsigned id) {
+  static inline uint64_t checkID(uint64_t id) {
     AlwaysAssert(id <= 63,
                  "Too many boolean node attributes registered during initialization !");
     return id;
@@ -309,10 +317,10 @@ struct Attribute<T, bool> {
 private:
 
   /** a bit assignment */
-  static const unsigned s_id;
+  static const uint64_t s_id;
 
   /** an extra hash value (to avoid same-value-type collisions) */
-  static const unsigned s_hashValue;
+  static const uint64_t s_hashValue;
 };
 
 // SPECIFIC, GLOBAL ATTRIBUTE DEFINITIONS ======================================
@@ -323,11 +331,11 @@ namespace attr {
 
   template <class T>
   struct LastAttributeId {
-    static unsigned s_id;
+    static uint64_t s_id;
   };
 
   template <class T>
-  unsigned LastAttributeId<T>::s_id = 0;
+  uint64_t LastAttributeId<T>::s_id = 0;
 }/* CVC4::expr::attr namespace */
 
 typedef Attribute<attr::VarName, std::string> VarNameAttr;
@@ -336,16 +344,16 @@ typedef Attribute<attr::Type, const CVC4::Type*> TypeAttr;
 // ATTRIBUTE IDENTIFIER ASSIGNMENT =============================================
 
 template <class T, class value_t>
-const unsigned Attribute<T, value_t>::s_id =
+const uint64_t Attribute<T, value_t>::s_id =
   attr::LastAttributeId<typename KindValueToTableValueMapping<value_t>::table_value_type>::s_id++;
 template <class T, class value_t>
-const unsigned Attribute<T, value_t>::s_hashValue = Attribute<T, value_t>::s_id;
+const uint64_t Attribute<T, value_t>::s_hashValue = Attribute<T, value_t>::s_id;
 
 template <class T>
-const unsigned Attribute<T, bool>::s_id =
+const uint64_t Attribute<T, bool>::s_id =
   Attribute<T, bool>::checkID(attr::LastAttributeId<bool>::s_id++);
 template <class T>
-const unsigned Attribute<T, bool>::s_hashValue = Attribute<T, bool>::s_id;
+const uint64_t Attribute<T, bool>::s_hashValue = Attribute<T, bool>::s_id;
 
 class AttributeManager;
 
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);
     }
diff --git a/src/expr/node.h b/src/expr/node.h
index 463ff8144..a39dc5b7e 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -48,7 +48,6 @@ using CVC4::expr::NodeValue;
 class Node {
 
   friend class NodeValue;
-  friend class SoftNode;
 
   /** A convenient null-valued encapsulated pointer */
   static Node s_null;
@@ -106,7 +105,7 @@ public:
   bool operator!=(const Node& e) const { return d_ev != e.d_ev; }
 
   Node operator[](int i) const {
-    Assert(i >= 0 && i < d_ev->d_nchildren);
+    Assert(i >= 0 && unsigned(i) < d_ev->d_nchildren);
     return Node(d_ev->d_children[i]);
   }
 
@@ -130,9 +129,11 @@ public:
   Node impExpr(const Node& right) const;
   Node xorExpr(const Node& right) const;
 
+  /*
   Node plusExpr(const Node& right) const;
   Node uMinusExpr() const;
   Node multExpr(const Node& right) const;
+  */
 
   inline Kind getKind() const;
 
@@ -171,9 +172,9 @@ public:
    * @param indent number of spaces to indent the formula by.
    */
   void printAst(std::ostream & o, int indent = 0) const;
-  
+
 private:
-  
+
   /**
    * Pretty printer for use within gdb
    * This is not intended to be used outside of gdb.
@@ -262,18 +263,30 @@ inline size_t Node::getNumChildren() const {
 
 template <class AttrKind>
 inline typename AttrKind::value_type Node::getAttribute(const AttrKind&) {
+  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()->getAttribute(*this, AttrKind());
 }
 
 template <class AttrKind>
 inline bool Node::hasAttribute(const AttrKind&,
                                typename AttrKind::value_type* ret) {
+  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()->hasAttribute(*this, AttrKind(), ret);
 }
 
 template <class AttrKind>
 inline void Node::setAttribute(const AttrKind&,
                                const typename AttrKind::value_type& value) {
+  Assert( NodeManager::currentNM() != NULL,
+          "There is no current CVC4::NodeManager associated to this thread.\n"
+          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
   NodeManager::currentNM()->setAttribute(*this, AttrKind(), value);
 }