* 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.

1 files changed, 31 insertions, 23 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;