10 files changed, 259 insertions, 41 deletions

diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index 295244473..85c0fe528 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -37,8 +37,7 @@ void AttributeManager::deleteAllAttributes(NodeValue* nv) {
   deleteFromTable(d_strings, nv);
   deleteFromTable(d_ptrs, nv);
 
-  // FIXME CD-bools in optimized table
-  deleteFromTable(d_cdbools, nv);
+  d_cdbools.erase(nv);
   deleteFromTable(d_cdints, nv);
   deleteFromTable(d_cdtnodes, nv);
   deleteFromTable(d_cdnodes, nv);
@@ -55,7 +54,6 @@ void AttributeManager::deleteAllAttributes() {
   deleteAllFromTable(d_strings);
   deleteAllFromTable(d_ptrs);
 
-  // FIXME CD-bools in optimized table
   d_cdbools.clear();
   d_cdints.clear();
   d_cdtnodes.clear();
@@ -64,7 +62,6 @@ void AttributeManager::deleteAllAttributes() {
   d_cdptrs.clear();
 }
 
-
 }/* CVC4::expr::attr namespace */
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index a77d09c4d..3bbab17a4 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -153,11 +153,11 @@ namespace attr {
  * to value_type using our specialized hash function for these pairs.
  */
 template <class value_type>
-struct AttrHash :
+class AttrHash :
     public __gnu_cxx::hash_map<std::pair<uint64_t, NodeValue*>,
                                value_type,
                                AttrHashStrategy> {
-};
+};/* class AttrHash<> */
 
 /**
  * In the case of Boolean-valued attributes we have a special
@@ -205,7 +205,7 @@ class AttrHash<bool> :
     operator bool() const {
       return (d_word & (1 << d_bit)) ? true : false;
     }
-  };
+  };/* class AttrHash<bool>::BitAccessor */
 
   /**
    * A (somewhat degenerate) iterator over boolean-valued attributes.
@@ -239,7 +239,7 @@ class AttrHash<bool> :
     bool operator==(const BitIterator& b) {
       return d_entry == b.d_entry && d_bit == b.d_bit;
     }
-  };
+  };/* class AttrHash<bool>::BitIterator */
 
   /**
    * A (somewhat degenerate) const_iterator over boolean-valued
@@ -274,7 +274,7 @@ class AttrHash<bool> :
     bool operator==(const ConstBitIterator& b) {
       return d_entry == b.d_entry && d_bit == b.d_bit;
     }
-  };
+  };/* class AttrHash<bool>::ConstBitIterator */
 
 public:
 
@@ -374,7 +374,226 @@ public:
                    value_type,
                    AttrHashStrategy>(ctxt) {
   }
-};
+};/* class CDAttrHash<> */
+
+/**
+ * In the case of Boolean-valued attributes we have a special
+ * "CDAttrHash<bool>" to pack bits together in words.
+ */
+template <>
+class CDAttrHash<bool> :
+    protected context::CDMap<NodeValue*,
+                             uint64_t,
+                             AttrHashBoolStrategy> {
+
+  /** A "super" type, like in Java, for easy reference below. */
+  typedef context::CDMap<NodeValue*, uint64_t, AttrHashBoolStrategy> super;
+
+  /**
+   * BitAccessor allows us to return a bit "by reference."  Of course,
+   * we don't require bit-addressibility supported by the system, we
+   * do it with a complex type.
+   */
+  class BitAccessor {
+
+    super& d_map;
+
+    NodeValue* d_key;
+
+    uint64_t d_word;
+
+    unsigned d_bit;
+
+  public:
+
+    BitAccessor(super& map, NodeValue* key, uint64_t word, unsigned bit) :
+      d_map(map),
+      d_key(key),
+      d_word(word),
+      d_bit(bit) {
+      Debug.printf("cdboolattr", "CDAttrHash<bool>::BitAccessor(%p, %p, %lx, %u)\n", &map, key, word, bit);
+    }
+
+    BitAccessor& operator=(bool b) {
+      if(b) {
+        // set the bit
+        d_word |= (1 << d_bit);
+        d_map.insert(d_key, d_word);
+        Debug.printf("cdboolattr", "CDAttrHash<bool>::BitAccessor::set(%p, %p, %lx, %u)\n", &d_map, d_key, d_word, d_bit);
+      } else {
+        // clear the bit
+        d_word &= ~(1 << d_bit);
+        d_map.insert(d_key, d_word);
+        Debug.printf("cdboolattr", "CDAttrHash<bool>::BitAccessor::clr(%p, %p, %lx, %u)\n", &d_map, d_key, d_word, d_bit);
+      }
+
+      return *this;
+    }
+
+    operator bool() const {
+      Debug.printf("cdboolattr", "CDAttrHash<bool>::BitAccessor::toBool(%p, %p, %lx, %u)\n", &d_map, d_key, d_word, d_bit);
+      return (d_word & (1 << d_bit)) ? true : false;
+    }
+  };/* class CDAttrHash<bool>::BitAccessor */
+
+  /**
+   * A (somewhat degenerate) iterator over boolean-valued attributes.
+   * This iterator doesn't support anything except comparison and
+   * dereference.  It's intended just for the result of find() on the
+   * table.
+   */
+  class BitIterator {
+
+    super* d_map;
+
+    std::pair<NodeValue* const, uint64_t>* d_entry;
+
+    unsigned d_bit;
+
+  public:
+
+    BitIterator() :
+      d_map(NULL),
+      d_entry(NULL),
+      d_bit(0) {
+    }
+
+    BitIterator(super& map, std::pair<NodeValue* const, uint64_t>& entry, unsigned bit) :
+      d_map(&map),
+      d_entry(&entry),
+      d_bit(bit) {
+    }
+
+    std::pair<NodeValue* const, BitAccessor> operator*() {
+      return std::make_pair(d_entry->first,
+                            BitAccessor(*d_map, d_entry->first, d_entry->second, d_bit));
+    }
+
+    bool operator==(const BitIterator& b) {
+      return d_entry == b.d_entry && d_bit == b.d_bit;
+    }
+  };/* class CDAttrHash<bool>::BitIterator */
+
+  /**
+   * A (somewhat degenerate) const_iterator over boolean-valued
+   * attributes.  This const_iterator doesn't support anything except
+   * comparison and dereference.  It's intended just for the result of
+   * find() on the table.
+   */
+  class ConstBitIterator {
+
+    const std::pair<NodeValue* const, uint64_t> d_entry;
+
+    unsigned d_bit;
+
+  public:
+
+    ConstBitIterator() :
+      d_entry(),
+      d_bit(0) {
+    }
+
+    ConstBitIterator(const std::pair<NodeValue* const, uint64_t>& entry,
+                     unsigned bit) :
+      d_entry(entry),
+      d_bit(bit) {
+    }
+
+    std::pair<NodeValue* const, bool> operator*() {
+      return std::make_pair(d_entry.first,
+                            (d_entry.second & (1 << d_bit)) ? true : false);
+    }
+
+    bool operator==(const ConstBitIterator& b) {
+      return d_entry == b.d_entry && d_bit == b.d_bit;
+    }
+  };/* class CDAttrHash<bool>::ConstBitIterator */
+
+  /* remove non-permitted operations */
+  CDAttrHash(const CDAttrHash<bool>&) CVC4_UNDEFINED;
+  CDAttrHash<bool>& operator=(const CDAttrHash<bool>&) CVC4_UNDEFINED;
+
+public:
+
+  CDAttrHash(context::Context* context) : super(context) { }
+
+  typedef std::pair<uint64_t, NodeValue*> key_type;
+  typedef bool data_type;
+  typedef std::pair<const key_type, data_type> value_type;
+
+  /** an iterator type; see above for limitations */
+  typedef BitIterator iterator;
+  /** a const_iterator type; see above for limitations */
+  typedef ConstBitIterator const_iterator;
+
+  /**
+   * Find the boolean value in the hash table.  Returns something ==
+   * end() if not found.
+   */
+  /*BitIterator find(const std::pair<uint64_t, NodeValue*>& k) {
+    super::iterator i = super::find(k.second);
+    if(i == super::end()) {
+      return BitIterator();
+    }
+    Debug.printf("cdboolattr",
+                 "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);
+  }*/
+
+  /** The "off the end" iterator */
+  BitIterator end() {
+    return BitIterator();
+  }
+
+  /**
+   * Find the boolean value in the hash table.  Returns something ==
+   * end() if not found.
+   */
+  ConstBitIterator find(const std::pair<uint64_t, NodeValue*>& k) const {
+    super::const_iterator i = super::find(k.second);
+    if(i == super::end()) {
+      return ConstBitIterator();
+    }
+    Debug.printf("cdboolattr",
+                 "underlying word at address looks like 0x%016llx, bit is %u\n",
+                 (unsigned long long)((*i).second),
+                 unsigned(k.first));
+    return ConstBitIterator(*i, k.first);
+  }
+
+  /** The "off the end" const_iterator */
+  ConstBitIterator end() const {
+    return ConstBitIterator();
+  }
+
+  /**
+   * Access the hash table using the underlying operator[].  Inserts
+   * the key into the table (associated to default value) if it's not
+   * already there.
+   */
+  BitAccessor operator[](const std::pair<uint64_t, NodeValue*>& k) {
+    uint64_t word = super::operator[](k.second);
+    return BitAccessor(*this, k.second, word, k.first);
+  }
+
+  /**
+   * Delete all flags from the given node.
+   */
+  void erase(NodeValue* nv) {
+    super::obliterate(nv);
+  }
+
+  /**
+   * Clear the hash table.
+   */
+  void clear() {
+    super::clear();
+  }
+
+};/* class CDAttrHash<bool> */
 
 }/* CVC4::expr::attr namespace */
 
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index b17e98b38..7c08293be 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -345,9 +345,9 @@ void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->setInfo(":status", status);
     //d_result = "success";
-  } catch(ModalException& m) {
+  } catch(ModalException&) {
     d_result = "error";
-  } catch(BadOptionException& bo) {
+  } catch(BadOptionException&) {
     // should not happen
     d_result = "error";
   }
@@ -367,7 +367,7 @@ void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->setLogic(d_logic);
     //d_result = "success";
-  } catch(ModalException& m) {
+  } catch(ModalException&) {
     d_result = "error";
   }
 }
@@ -387,9 +387,9 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->setInfo(d_flag, d_sexpr);
     //d_result = "success";
-  } catch(ModalException& m) {
+  } catch(ModalException&) {
     d_result = "error";
-  } catch(BadOptionException& bo) {
+  } catch(BadOptionException&) {
     d_result = "unsupported";
   }
 }
@@ -419,7 +419,7 @@ void GetInfoCommand::invoke(SmtEngine* smtEngine) {
     stringstream ss;
     ss << smtEngine->getInfo(d_flag);
     d_result = ss.str();
-  } catch(BadOptionException& bo) {
+  } catch(BadOptionException&) {
     d_result = "unsupported";
   }
 }
@@ -449,9 +449,9 @@ void SetOptionCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->setOption(d_flag, d_sexpr);
     //d_result = "success";
-  } catch(ModalException& m) {
+  } catch(ModalException&) {
     d_result = "error";
-  } catch(BadOptionException& bo) {
+  } catch(BadOptionException&) {
     d_result = "unsupported";
   }
 }
@@ -479,7 +479,7 @@ GetOptionCommand::GetOptionCommand(std::string flag) :
 void GetOptionCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->getOption(d_flag).getValue();
-  } catch(BadOptionException& bo) {
+  } catch(BadOptionException&) {
     d_result = "unsupported";
   }
 }
diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h
index 65574b6c9..9acc46b5f 100644
--- a/src/expr/declaration_scope.h
+++ b/src/expr/declaration_scope.h
@@ -16,8 +16,10 @@
  ** Convenience class for scoping variable and type declarations.
  **/
 
-#ifndef DECLARATION_SCOPE_H
-#define DECLARATION_SCOPE_H
+#include "cvc4_public.h"
+
+#ifndef __CVC4__DECLARATION_SCOPE_H
+#define __CVC4__DECLARATION_SCOPE_H
 
 #include <vector>
 #include <utility>
@@ -182,4 +184,4 @@ public:
 
 }/* CVC4 namespace */
 
-#endif /* DECLARATION_SCOPE_H */
+#endif /* __CVC4__DECLARATION_SCOPE_H */
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index eadbb73a2..9b8511de9 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -115,22 +115,22 @@ ExprManager::~ExprManager() {
 
 BooleanType ExprManager::booleanType() const {
   NodeManagerScope nms(d_nodeManager);
-  return Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType()));
+  return BooleanType(Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType())));
 }
 
 KindType ExprManager::kindType() const {
   NodeManagerScope nms(d_nodeManager);
-  return Type(d_nodeManager, new TypeNode(d_nodeManager->kindType()));
+  return KindType(Type(d_nodeManager, new TypeNode(d_nodeManager->kindType())));
 }
 
 RealType ExprManager::realType() const {
   NodeManagerScope nms(d_nodeManager);
-  return Type(d_nodeManager, new TypeNode(d_nodeManager->realType()));
+  return RealType(Type(d_nodeManager, new TypeNode(d_nodeManager->realType())));
 }
 
 IntegerType ExprManager::integerType() const {
   NodeManagerScope nms(d_nodeManager);
-  return Type(d_nodeManager, new TypeNode(d_nodeManager->integerType()));
+  return IntegerType(Type(d_nodeManager, new TypeNode(d_nodeManager->integerType())));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
@@ -285,7 +285,7 @@ Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) {
 /** Make a function type from domain to range. */
 FunctionType ExprManager::mkFunctionType(const Type& domain, const Type& range) {
   NodeManagerScope nms(d_nodeManager);
-  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(*domain.d_typeNode, *range.d_typeNode)));
+  return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(*domain.d_typeNode, *range.d_typeNode))));
 }
 
 /** Make a function type with input types from argTypes. */
@@ -296,7 +296,7 @@ FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, cons
   for (unsigned i = 0, i_end = argTypes.size(); i < i_end; ++ i) {
     argTypeNodes.push_back(*argTypes[i].d_typeNode);
   }
-  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(argTypeNodes, *range.d_typeNode)));
+  return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(argTypeNodes, *range.d_typeNode))));
 }
 
 FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) {
@@ -306,7 +306,7 @@ FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) {
   for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
      sortNodes.push_back(*sorts[i].d_typeNode);
   }
-  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(sortNodes)));
+  return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(sortNodes))));
 }
 
 FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) {
@@ -316,7 +316,7 @@ FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) {
   for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
      sortNodes.push_back(*sorts[i].d_typeNode);
   }
-  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes)));
+  return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes))));
 }
 
 TupleType ExprManager::mkTupleType(const std::vector<Type>& types) {
@@ -326,29 +326,29 @@ TupleType ExprManager::mkTupleType(const std::vector<Type>& types) {
   for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) {
      typeNodes.push_back(*types[i].d_typeNode);
   }
-  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes)));
+  return TupleType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes))));
 }
 
 BitVectorType ExprManager::mkBitVectorType(unsigned size) const {
   NodeManagerScope nms(d_nodeManager);
-  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkBitVectorType(size)));
+  return BitVectorType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkBitVectorType(size))));
 }
 
 ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const {
   NodeManagerScope nms(d_nodeManager);
-  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode)));
+  return ArrayType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode))));
 }
 
 SortType ExprManager::mkSort(const std::string& name) const {
   NodeManagerScope nms(d_nodeManager);
-  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name)));
+  return SortType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name))));
 }
 
 SortConstructorType ExprManager::mkSortConstructor(const std::string& name,
                                                    size_t arity) const {
   NodeManagerScope nms(d_nodeManager);
-  return Type(d_nodeManager,
-              new TypeNode(d_nodeManager->mkSortConstructor(name, arity)));
+  return SortConstructorType(Type(d_nodeManager,
+              new TypeNode(d_nodeManager->mkSortConstructor(name, arity))));
 }
 
 /**
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index fba1a919c..83d306871 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -40,7 +40,7 @@ namespace CVC4 {
 class Expr;
 class SmtEngine;
 class NodeManager;
-class Options;
+struct Options;
 class IntStat;
 
 namespace context {
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index eb618a8c9..f6d346630 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -74,7 +74,7 @@ TypeCheckingException::~TypeCheckingException() throw () {
 
 std::string TypeCheckingException::toString() const {
   std::stringstream ss;
-  ss << "Error type-checking " << d_expr << ": " << d_msg;
+  ss << "Error type-checking " << d_expr << ": " << d_msg << std::endl << *d_expr;
   return ss.str();
 }
 
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index efcd42999..445d91da8 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -37,7 +37,7 @@ TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () {
 
 string TypeCheckingExceptionPrivate::toString() const {
   stringstream ss;
-  ss << "Error type-checking " << d_node << ": " << d_msg;
+  ss << "Error type-checking " << d_node << ": " << d_msg << std::endl << *d_node;
   return ss.str();
 }
 
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 117497539..d8a690da5 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -42,7 +42,7 @@
 
 namespace CVC4 {
 
-class Options;
+struct Options;
 
 namespace expr {
 
diff --git a/src/expr/type.h b/src/expr/type.h
index d357c869e..cc1248510 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -73,7 +73,7 @@ class CVC4_PUBLIC Type {
   friend class SmtEngine;
   friend class ExprManager;
   friend class TypeNode;
-  friend class TypeHashStrategy;
+  friend struct TypeHashStrategy;
   friend std::ostream& operator<<(std::ostream& out, const Type& t);
 
 protected: