Fix errors and reduce warnings on clang (merge from mdeters/clang)

22 files changed, 40 insertions, 285 deletions

diff --git a/contrib/get-antlr-3.4 b/contrib/get-antlr-3.4
index 6c8e5de46..49b0b54a7 100755
--- a/contrib/get-antlr-3.4
+++ b/contrib/get-antlr-3.4
@@ -49,10 +49,10 @@ cd libantlr3c-3.4
 
 if [ ${MACHINE_TYPE} == 'x86_64' ]; then
   # 64-bit stuff here
-  ./configure --enable-64bit --disable-antlrdebug --prefix=`pwd`/../.. $ANTLR_CONFIGURE_ARGS
+  ./configure --enable-64bit --disable-shared --disable-antlrdebug --prefix=`pwd`/../.. $ANTLR_CONFIGURE_ARGS
 else
   # 32-bit stuff here
-  ./configure --disable-antlrdebug --prefix=`pwd`/../.. $ANTLR_CONFIGURE_ARGS
+  ./configure --disable-shared --disable-antlrdebug --prefix=`pwd`/../.. $ANTLR_CONFIGURE_ARGS
 fi
 
 cp Makefile Makefile.orig
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index a085161bc..9a14caec5 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -752,7 +752,7 @@ public:
                      table_value_type table_value_type;
     typedef attr::AttributeTraits<table_value_type, context_dep> traits;
     uint64_t id = attr::LastAttributeId<table_value_type, context_dep>::s_id++;
-    Assert(traits::cleanup.size() == id);// sanity check
+    //Assert(traits::cleanup.size() == id);// sanity check
     traits::cleanup.push_back(attr::getCleanupStrategy<value_t,
                                                        CleanupStrategy>::fn);
     return id;
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index b9cae9431..09018cbfd 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -43,7 +43,7 @@ class SmtEngine;
 class NodeManager;
 class Options;
 class IntStat;
-class ExprManagerMapCollection;
+struct ExprManagerMapCollection;
 class StatisticsRegistry;
 
 namespace expr {
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 442d29ac9..b353ec5dc 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -67,7 +67,7 @@ namespace prop {
   class TheoryProxy;
 }/* CVC4::prop namespace */
 
-class ExprManagerMapCollection;
+struct ExprManagerMapCollection;
 
 struct ExprHashFunction;
 
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 47504b0e4..0cab4e628 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -27,7 +27,7 @@
 namespace CVC4 {
 namespace kind {
 
-enum Kind_t {
+enum CVC4_PUBLIC Kind_t {
   UNDEFINED_KIND = -1, /**< undefined */
   NULL_EXPR, /**< Null kind */
 ${kind_decls}
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index cc52b11b9..4e95c0fe2 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -204,111 +204,48 @@ bool Type::isBoolean() const {
   return d_typeNode->isBoolean();
 }
 
-/** Cast to a Boolean type */
-Type::operator BooleanType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isBoolean(), this);
-  return BooleanType(*this);
-}
-
 /** Is this the integer type? */
 bool Type::isInteger() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isInteger();
 }
 
-/** Cast to a integer type */
-Type::operator IntegerType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isInteger(), this);
-  return IntegerType(*this);
-}
-
 /** Is this the real type? */
 bool Type::isReal() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isReal();
 }
 
-/** Cast to a real type */
-Type::operator RealType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isReal(), this);
-  return RealType(*this);
-}
-
 /** Is this the string type? */
 bool Type::isString() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isString();
 }
 
-/** Cast to a string type */
-Type::operator StringType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isString(), this);
-  return StringType(*this);
-}
-
 /** Is this the bit-vector type? */
 bool Type::isBitVector() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isBitVector();
 }
 
-/** Cast to a bit-vector type */
-Type::operator BitVectorType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isBitVector(), this);
-  return BitVectorType(*this);
-}
-
-/** Cast to a Constructor type */
-Type::operator DatatypeType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isDatatype(), this);
-  return DatatypeType(*this);
-}
-
 /** Is this a datatype type? */
 bool Type::isDatatype() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isDatatype() || d_typeNode->isParametricDatatype();
 }
 
-/** Cast to a Constructor type */
-Type::operator ConstructorType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isConstructor(), this);
-  return ConstructorType(*this);
-}
-
 /** Is this the Constructor type? */
 bool Type::isConstructor() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isConstructor();
 }
 
-/** Cast to a Selector type */
-Type::operator SelectorType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isSelector(), this);
-  return SelectorType(*this);
-}
-
 /** Is this the Selector type? */
 bool Type::isSelector() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isSelector();
 }
 
-/** Cast to a Tester type */
-Type::operator TesterType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isTester(), this);
-  return TesterType(*this);
-}
-
 /** Is this the Tester type? */
 bool Type::isTester() const {
   NodeManagerScope nms(d_nodeManager);
@@ -330,64 +267,30 @@ bool Type::isPredicate() const {
   return d_typeNode->isPredicate();
 }
 
-/** Cast to a function type */
-Type::operator FunctionType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isFunction(), this);
-  return FunctionType(*this);
-}
-
 /** Is this a tuple type? */
 bool Type::isTuple() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isTuple();
 }
 
-/** Cast to a tuple type */
-Type::operator TupleType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isTuple(), this);
-  return TupleType(*this);
-}
-
 /** Is this a record type? */
 bool Type::isRecord() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isRecord();
 }
 
-/** Cast to a record type */
-Type::operator RecordType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isRecord(), this);
-  return RecordType(*this);
-}
-
 /** Is this a symbolic expression type? */
 bool Type::isSExpr() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isSExpr();
 }
 
-/** Cast to a symbolic expression type */
-Type::operator SExprType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isSExpr(), this);
-  return SExprType(*this);
-}
-
 /** Is this an array type? */
 bool Type::isArray() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isArray();
 }
 
-/** Cast to an array type */
-Type::operator ArrayType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  return ArrayType(*this);
-}
-
 /** Is this a sort kind */
 bool Type::isSort() const {
   NodeManagerScope nms(d_nodeManager);
@@ -395,25 +298,11 @@ bool Type::isSort() const {
 }
 
 /** Cast to a sort type */
-Type::operator SortType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isSort(), this);
-  return SortType(*this);
-}
-
-/** Is this a sort constructor kind */
 bool Type::isSortConstructor() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isSortConstructor();
 }
 
-/** Cast to a sort constructor type */
-Type::operator SortConstructorType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isSortConstructor(), this);
-  return SortConstructorType(*this);
-}
-
 /** Is this a predicate subtype */
 /* - not in release 1.0
 bool Type::isPredicateSubtype() const {
@@ -422,28 +311,12 @@ bool Type::isPredicateSubtype() const {
 }
 */
 
-/** Cast to a predicate subtype */
-/* - not in release 1.0
-Type::operator PredicateSubtype() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isPredicateSubtype(), this);
-  return PredicateSubtype(*this);
-}
-*/
-
 /** Is this an integer subrange */
 bool Type::isSubrange() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isSubrange();
 }
 
-/** Cast to a predicate subtype */
-Type::operator SubrangeType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isSubrange(), this);
-  return SubrangeType(*this);
-}
-
 vector<Type> FunctionType::getArgTypes() const {
   NodeManagerScope nms(d_nodeManager);
   vector<Type> args;
diff --git a/src/expr/type.h b/src/expr/type.h
index 4223d71ab..ce6291cd8 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -30,15 +30,15 @@
 namespace CVC4 {
 
 class NodeManager;
-class ExprManager;
-class Expr;
+class CVC4_PUBLIC ExprManager;
+class CVC4_PUBLIC Expr;
 class TypeNode;
-class ExprManagerMapCollection;
+struct CVC4_PUBLIC ExprManagerMapCollection;
 
-class SmtEngine;
+class CVC4_PUBLIC SmtEngine;
 
-class Datatype;
-class Record;
+class CVC4_PUBLIC Datatype;
+class CVC4_PUBLIC Record;
 
 template <bool ref_count>
 class NodeTemplate;
@@ -240,60 +240,30 @@ public:
   bool isBoolean() const;
 
   /**
-   * Cast this type to a Boolean type
-   * @return the BooleanType
-   */
-  operator BooleanType() const throw(IllegalArgumentException);
-
-  /**
    * Is this the integer type?
    * @return true if the type is a integer type
    */
   bool isInteger() const;
 
   /**
-   * Cast this type to a integer type
-   * @return the IntegerType
-   */
-  operator IntegerType() const throw(IllegalArgumentException);
-
-  /**
    * Is this the real type?
    * @return true if the type is a real type
    */
   bool isReal() const;
 
   /**
-   * Cast this type to a real type
-   * @return the RealType
-   */
-  operator RealType() const throw(IllegalArgumentException);
-
-  /**
    * Is this the string type?
    * @return true if the type is the string type
    */
   bool isString() const;
 
   /**
-   * Cast this type to a string type
-   * @return the StringType
-   */
-  operator StringType() const throw(IllegalArgumentException);
-
-  /**
    * Is this the bit-vector type?
    * @return true if the type is a bit-vector type
    */
   bool isBitVector() const;
 
   /**
-   * Cast this type to a bit-vector type
-   * @return the BitVectorType
-   */
-  operator BitVectorType() const throw(IllegalArgumentException);
-
-  /**
    * Is this a function type?
    * @return true if the type is a function type
    */
@@ -307,132 +277,66 @@ public:
   bool isPredicate() const;
 
   /**
-   * Cast this type to a function type
-   * @return the FunctionType
-   */
-  operator FunctionType() const throw(IllegalArgumentException);
-
-  /**
    * Is this a tuple type?
    * @return true if the type is a tuple type
    */
   bool isTuple() const;
 
   /**
-   * Cast this type to a tuple type
-   * @return the TupleType
-   */
-  operator TupleType() const throw(IllegalArgumentException);
-
-  /**
    * Is this a record type?
    * @return true if the type is a record type
    */
   bool isRecord() const;
 
   /**
-   * Cast this type to a record type
-   * @return the RecordType
-   */
-  operator RecordType() const throw(IllegalArgumentException);
-
-  /**
    * Is this a symbolic expression type?
    * @return true if the type is a symbolic expression type
    */
   bool isSExpr() const;
 
   /**
-   * Cast this type to a symbolic expression type
-   * @return the SExprType
-   */
-  operator SExprType() const throw(IllegalArgumentException);
-
-  /**
    * Is this an array type?
    * @return true if the type is a array type
    */
   bool isArray() const;
 
   /**
-   * Cast this type to an array type
-   * @return the ArrayType
-   */
-  operator ArrayType() const throw(IllegalArgumentException);
-
-  /**
    * Is this a datatype type?
    * @return true if the type is a datatype type
    */
   bool isDatatype() const;
 
   /**
-   * Cast this type to a datatype type
-   * @return the DatatypeType
-   */
-  operator DatatypeType() const throw(IllegalArgumentException);
-
-  /**
    * Is this a constructor type?
    * @return true if the type is a constructor type
    */
   bool isConstructor() const;
 
   /**
-   * Cast this type to a constructor type
-   * @return the ConstructorType
-   */
-  operator ConstructorType() const throw(IllegalArgumentException);
-
-  /**
    * Is this a selector type?
    * @return true if the type is a selector type
    */
   bool isSelector() const;
 
   /**
-   * Cast this type to a selector type
-   * @return the SelectorType
-   */
-  operator SelectorType() const throw(IllegalArgumentException);
-
-  /**
    * Is this a tester type?
    * @return true if the type is a tester type
    */
   bool isTester() const;
 
   /**
-   * Cast this type to a tester type
-   * @return the TesterType
-   */
-  operator TesterType() const throw(IllegalArgumentException);
-
-  /**
    * Is this a sort kind?
    * @return true if this is a sort kind
    */
   bool isSort() const;
 
   /**
-   * Cast this type to a sort type
-   * @return the sort type
-   */
-  operator SortType() const throw(IllegalArgumentException);
-
-  /**
    * Is this a sort constructor kind?
    * @return true if this is a sort constructor kind
    */
   bool isSortConstructor() const;
 
   /**
-   * Cast this type to a sort constructor type
-   * @return the sort constructor type
-   */
-  operator SortConstructorType() const throw(IllegalArgumentException);
-
-  /**
    * Is this a predicate subtype?
    * @return true if this is a predicate subtype
    */
@@ -440,25 +344,12 @@ public:
   //bool isPredicateSubtype() const;
 
   /**
-   * Cast this type to a predicate subtype
-   * @return the predicate subtype
-   */
-  // not in release 1.0
-  //operator PredicateSubtype() const throw(IllegalArgumentException);
-
-  /**
    * Is this an integer subrange type?
    * @return true if this is an integer subrange type
    */
   bool isSubrange() const;
 
   /**
-   * Cast this type to an integer subrange type
-   * @return the integer subrange type
-   */
-  operator SubrangeType() const throw(IllegalArgumentException);
-
-  /**
    * Outputs a string representation of this type to the stream.
    * @param out the stream to output to
    */
diff --git a/src/options/options.h b/src/options/options.h
index 2d49765f3..5f17f5a5c 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -31,7 +31,7 @@
 namespace CVC4 {
 
 namespace options {
-  class OptionsHolder;
+  struct OptionsHolder;
 }/* CVC4::options namespace */
 
 class ExprStream;
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index d05fe24a7..c1351c6a2 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -26,7 +26,7 @@ namespace CVC4 {
 bool          ProofManager::isInitialized = false;
 ProofManager* ProofManager::proofManager = NULL;
 
-ProofManager::ProofManager(ProofFormat format = LFSC):
+ProofManager::ProofManager(ProofFormat format):
   d_satProof(NULL),
   d_cnfProof(NULL),
   d_format(format)
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 3bfff1456..91eb2ed99 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -52,7 +52,7 @@ class ProofManager {
   
   static ProofManager* proofManager; 
   static bool isInitialized; 
-  ProofManager(ProofFormat format);
+  ProofManager(ProofFormat format = LFSC);
 public:
   static ProofManager* currentPM();
 
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 978ac8d7b..68969c78b 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -32,7 +32,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "theory/interrupted.h"
 using namespace BVMinisat;
 
-namespace CVC4 {
+namespace BVMinisat {
 
 #define OUTPUT_TAG "bvminisat: [a=" << assumptions.size() << ",l=" << decisionLevel() << "] "
 
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index e5d876b48..b4807b021 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -130,8 +130,6 @@ public:
 
 };/* class DPLLSatSolverInterface */
 
-}/* CVC4::prop namespace */
-
 inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
   out << lit.toString();
   return out;
@@ -167,6 +165,7 @@ inline std::ostream& operator <<(std::ostream& out, prop::SatValue val) {
   return out;
 }
 
+}/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
 #endif /* __CVC4__PROP__SAT_MODULE_H */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 3edcd6872..cdae68d96 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -47,7 +47,7 @@ namespace CVC4 {
 template <bool ref_count> class NodeTemplate;
 typedef NodeTemplate<true> Node;
 typedef NodeTemplate<false> TNode;
-class NodeHashFunction;
+struct NodeHashFunction;
 
 class Command;
 class GetModelCommand;
@@ -77,7 +77,7 @@ namespace smt {
    */
   class DefinedFunction;
 
-  class SmtEngineStatistics;
+  struct SmtEngineStatistics;
   class SmtEnginePrivate;
   class SmtScope;
   class BooleanTermConverter;
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 9a41d8d23..fdb4a8ffa 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -225,7 +225,7 @@ private:
   bool equalSizes();
 
   bool inMaps(ArithVar x) const{
-    return 0 <= x && x < d_mapSize;
+    return x < d_mapSize;
   }
 
 };/* class ArithPartialModel */
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 23cd8381d..8bcc64414 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -430,10 +430,6 @@ Node RewriteRule<BitwiseNotOr>::apply(TNode node) {
 template<> inline
 bool RewriteRule<XorNot>::applies(TNode node) {
   Unreachable();
-  if (node.getKind() == kind::BITVECTOR_XOR &&
-      node.getNumChildren() == 2 &&
-          node[0].getKind() == kind::BITVECTOR_NOT &&
-          node[1].getKind() == kind::BITVECTOR_NOT); 
 }
 
 template<> inline
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 3d98674a8..8272ce168 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -42,10 +42,6 @@ void FirstOrderModel::reset(){
   TheoryModel::reset();
 }
 
-void FirstOrderModel::addTerm( Node n ){
-  TheoryModel::addTerm( n );
-}
-
 void FirstOrderModel::initialize( bool considerAxioms ){
   //rebuild models
   d_uf_model_tree.clear();
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 3779579fd..50a941968 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -33,8 +33,6 @@ class TermDb;
 class FirstOrderModel : public TheoryModel
 {
 private:
-  //add term function
-  void addTerm( Node n );
   //for initialize model
   void initializeModelForTerm( Node n );
   /** whether an axiom is asserted */
diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp
index c6fd9611c..a82b94f73 100644
--- a/src/theory/rewriterules/theory_rewriterules.cpp
+++ b/src/theory/rewriterules/theory_rewriterules.cpp
@@ -276,7 +276,7 @@ void TheoryRewriteRules::check(Effort level) {
       if(glast.inst == RULEINST_TRUE||glast.inst == RULEINST_FALSE)
         continue;
       // If it has a value it should already has been notified
-      bool value; value = value; // avoiding the warning in non debug mode
+      bool value CVC4_UNUSED;
       Assert(!getValuation().hasSatValue(g,value));
       Debug("rewriterules::check") << "RewriteRules::Check Narrowing on:" << g << std::endl;
       /** Can split on already rewritten instrule... but... */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index e76441f6b..5b2032430 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -50,13 +50,13 @@ namespace theory {
 class QuantifiersEngine;
 class TheoryModel;
 
-namespace rrinst{
-class CandidateGenerator;
-}
+namespace rrinst {
+  class CandidateGenerator;
+}/* CVC4::theory::rrinst namespace */
 
 namespace eq {
-class EqualityEngine;
-}
+  class EqualityEngine;
+}/* CVC4::theory::eq namespace */
 
 /**
  * Information about an assertion for the theories.
@@ -787,14 +787,10 @@ public:
   std::hash_set<TNode, TNodeHashFunction> currentlySharedTerms() const;
 };/* class Theory */
 
-std::ostream& operator<<(std::ostream& os, Theory::Effort level);
-
-namespace eq{
-  class EqualityEngine;
-}
-
+std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level);
+inline std::ostream& operator<<(std::ostream& out, const theory::Assertion& a);
 
-inline Assertion Theory::get() {
+inline theory::Assertion Theory::get() {
   Assert( !done(), "Theory::get() called with assertion queue empty!" );
 
   // Get the assertion
@@ -810,7 +806,9 @@ inline Assertion Theory::get() {
   return fact;
 }
 
-}/* CVC4::theory namespace */
+inline std::ostream& operator<<(std::ostream& out, const theory::Assertion& a) {
+  return out << a.assertion;
+}
 
 inline std::ostream& operator<<(std::ostream& out,
                                 const CVC4::theory::Theory& theory) {
@@ -831,6 +829,7 @@ inline std::ostream& operator << (std::ostream& out, theory::Theory::PPAssertSta
   return out;
 }
 
+}/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
 #endif /* __CVC4__THEORY__THEORY_H */
diff --git a/src/util/node_visitor.h b/src/util/node_visitor.h
index e444ba6e2..4c8e646bd 100644
--- a/src/util/node_visitor.h
+++ b/src/util/node_visitor.h
@@ -36,10 +36,11 @@ class NodeVisitor {
   /**
    * Guard against NodeVisitor<> being re-entrant.
    */
+  template <class T>
   class GuardReentry {
-    bool& d_guard;
+    T& d_guard;
   public:
-    GuardReentry(bool& guard)
+    GuardReentry(T& guard)
     : d_guard(guard) {
       Assert(!d_guard);
       d_guard = true;
@@ -71,7 +72,7 @@ public:
    */
   static typename Visitor::return_type run(Visitor& visitor, TNode node) {
 
-    GuardReentry guard(bool(s_inRun));
+    GuardReentry<CVC4_THREADLOCAL_TYPE(bool)> guard(s_inRun);
 
     // Notify of a start
     visitor.start(node);
diff --git a/src/util/record.h b/src/util/record.h
index 2c15d30e0..27b090e1d 100644
--- a/src/util/record.h
+++ b/src/util/record.h
@@ -29,7 +29,7 @@
 
 namespace CVC4 {
 
-class Record;
+class CVC4_PUBLIC Record;
 
 // operators for record select and update
 
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index 0a5450b8a..9aca3cb5a 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -42,6 +42,8 @@ namespace CVC4 {
 class ExprManager;
 class SmtEngine;
 
+inline std::ostream& operator<<(std::ostream& os, const timespec& t);
+
 /**
  * The base class for all statistics.
  *