This is a merge from the "theoryfixes+cdattrhash" branch. The changes

are somewhat disparate but belonged on the same branch because they were
held back from trunk all for the same reason (to keep the trunk stable
for furious bitvector development).  Dejan has now given me the go-ahead
for a merge.

=========================================
THIS COMMIT CHANGES THE THEORY INTERFACE!
=========================================

Theory constructors are expected to take an additional "Valuation*"
parameter that each Theory should send along to the base class
constructor.  The base class Theory keeps the Valuation* in a
d_valuation field for use by it and by its derived classes.
Theory::getValue() no longer takes a Valuation* (it is expected
to use d_valuation instead).  This allows other theory functions
to take advantage of getValue() for debugging or heuristic
purposes.

TODO BEFORE MERGE TO TRUNK:
****implement BitIterator find() in CDAttrHash<bool>.

Specifically:

* Added QF_BV support for SMT-LIB v2.
* Two adjustments to the theory interface as requested by Tim King:
  1. As described above.
  2. Theories now have const access to the fact queue through base
     class functions facts_begin() and facts_end(); useful for
     debugging.
* Added an "Asserted" attribute so that theories can check if something
  has been asserted or not (and therefore not propagate it).  However, this
  has been disabled for now, pending more data on the overhead of it, and
  pending discussion at the 3/25/2011 meeting.
* Do not define NDEBUG in MiniSat in assertion-enabled builds (so
  that MiniSat asserts are evaluated).
* As a result of the new MiniSat assertions, some --incremental
  regressions had to be disabled; also, some bitvectors ?!!
* Bug 71 is resolved by adding a specialization for CDAttrHash<> in the
  attribute package.
* Fixes for some warnings flagged by clang.
* System tests have arrived!  So far mainly infrastructure for having
  system tests, but there is a system test aimed at improving code
  coverage of the printer package.
* Minor other adjustments to documentation and coding to be more
  conformant to CVC4 policy.

Tests have been performed to demonstrate that these changes have no or
negligible effect on performance.  In particular, changing the
CDAttrHash<> doesn't have any real effect on performance or memory right
now, since there is only one context-dependent boolean flag (as soon
as another is added, the effect is noticeable but probably still slight).

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: