Commit to fix bug 241 (improper "using namespace std" in a header). This caused a number of latent errors in sources and headers to come up. Those are now fixed (by adding "using" or "std::" depending on the context). Took the opportunity to bring many rewriter sources in line with coding conventions.

19 files changed, 264 insertions, 110 deletions

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 75216dac6..cc80e2dd8 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -2,10 +2,10 @@
 /*! \file arith_rewriter.cpp
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
+ ** Major contributors: dejan
  ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -17,7 +17,6 @@
  ** \todo document this file
  **/
 
-
 #include "theory/theory.h"
 #include "theory/arith/normal_form.h"
 #include "theory/arith/arith_rewriter.h"
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index e161bd8d6..3a8fc191a 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -2,10 +2,10 @@
 /*! \file arith_rewriter.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: mdeters
+ ** Major contributors: mdeters, dejan
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -17,6 +17,11 @@
  ** \todo document this file
  **/
 
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__ARITH_REWRITER_H
+#define __CVC4__THEORY__ARITH__ARITH_REWRITER_H
+
 #include "theory/theory.h"
 #include "theory/arith/arith_constants.h"
 #include "theory/arith/arith_utilities.h"
@@ -24,9 +29,6 @@
 
 #include "theory/rewriter.h"
 
-#ifndef __CVC4__THEORY__ARITH__REWRITER_H
-#define __CVC4__THEORY__ARITH__REWRITER_H
-
 namespace CVC4 {
 namespace theory {
 namespace arith {
@@ -88,11 +90,10 @@ private:
     return !isAtom(n);
   }
 
-};
-
+};/* class ArithRewriter */
 
-}; /* namesapce rewrite */
-}; /* namespace theory */
-}; /* namespace CVC4 */
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__ARITH__REWRITER_H */
+#endif /* __CVC4__THEORY__ARITH__ARITH_REWRITER_H */
diff --git a/src/theory/arith/row_vector.cpp b/src/theory/arith/row_vector.cpp
index 2463adf47..0dc483126 100644
--- a/src/theory/arith/row_vector.cpp
+++ b/src/theory/arith/row_vector.cpp
@@ -3,7 +3,9 @@
 
 using namespace CVC4;
 using namespace CVC4::theory;
-using namespace CVC4::theory::arith ;
+using namespace CVC4::theory::arith;
+
+using namespace std;
 
 bool RowVector::isSorted(const VarCoeffArray& arr, bool strictlySorted) {
   if(arr.size() >= 2){
diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h
index 29b79ddd5..bed33349d 100644
--- a/src/theory/arith/row_vector.h
+++ b/src/theory/arith/row_vector.h
@@ -85,7 +85,7 @@ protected:
   std::vector<ArithVarSet>& d_columnMatrix;
 
   NonZeroIterator lower_bound(ArithVar x_j) const{
-    return std::lower_bound(d_entries.begin(), d_entries.end(), make_pair(x_j,0), cmp);
+    return std::lower_bound(d_entries.begin(), d_entries.end(), std::make_pair(x_j,0), cmp);
   }
 
   typedef VarCoeffArray::iterator iterator;
@@ -120,7 +120,7 @@ public:
 private:
   /** Debugging code. */
   bool hasInEntries(ArithVar x_j) const {
-    return std::binary_search(d_entries.begin(), d_entries.end(), make_pair(x_j,0), cmp);
+    return std::binary_search(d_entries.begin(), d_entries.end(), std::make_pair(x_j,0), cmp);
   }
 public:
 
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index ebf7dbee8..a85765303 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -24,6 +24,8 @@ using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::arith;
 
+using namespace std;
+
 Tableau::~Tableau(){
   while(!d_basicVariables.empty()){
     ArithVar curr = *(d_basicVariables.begin());
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 103707601..33a6233bc 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -1,12 +1,26 @@
-/*
- * theory_arrays_rewriter.h
- *
- *  Created on: Dec 21, 2010
- *      Author: dejan
- */
-
-#pragma once
-
+/*********************                                                        */
+/*! \file theory_arrays_rewriter.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
+#define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
 
 #include "theory/rewriter.h"
 
@@ -29,9 +43,10 @@ public:
   static inline void init() {}
   static inline void shutdown() {}
 
-};
+};/* class TheoryArraysRewriter */
 
-}
-}
-}
+}/* CVC4::theory::arrays namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
+#endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H */
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index a62bc6fa0..c1be3b906 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file theory_bool_rewriter.cpp
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
 #include <algorithm>
 #include "theory/booleans/theory_bool_rewriter.h"
 
@@ -66,7 +85,6 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
   return RewriteResponse(REWRITE_DONE, n);
 }
 
-}
-}
-}
-
+}/* CVC4::theory::booleans namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h
index 62eed9e2b..4a23249d4 100644
--- a/src/theory/booleans/theory_bool_rewriter.h
+++ b/src/theory/booleans/theory_bool_rewriter.h
@@ -1,11 +1,26 @@
-/*
- * theory_bool_rewriter.h
- *
- *  Created on: Dec 21, 2010
- *      Author: dejan
- */
-
-#pragma once
+/*********************                                                        */
+/*! \file theory_bool_rewriter.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H
+#define __CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H
 
 #include "theory/rewriter.h"
 
@@ -25,8 +40,10 @@ public:
   static void init() {}
   static void shutdown() {}
 
-};
+};/* class TheoryBoolRewriter */
+
+}/* CVC4::theory::booleans namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
-}
-}
-}
+#endif /* __CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H */
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index 05f7891d6..b71d66c03 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -1,5 +1,26 @@
+/*********************                                                        */
+/*! \file theory_builtin_rewriter.cpp
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
 #include "theory/builtin/theory_builtin_rewriter.h"
 
+using namespace std;
+
 namespace CVC4 {
 namespace theory {
 namespace builtin {
@@ -30,6 +51,6 @@ Node TheoryBuiltinRewriter::blastDistinct(TNode in) {
   return out;
 }
 
-}
-}
-}
+}/* CVC4::theory::builtin namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h
index 7da4289b1..d50397598 100644
--- a/src/theory/builtin/theory_builtin_rewriter.h
+++ b/src/theory/builtin/theory_builtin_rewriter.h
@@ -1,11 +1,26 @@
-/*
- * theory_builtin_rewriter.h
- *
- *  Created on: Dec 21, 2010
- *      Author: dejan
- */
+/*********************                                                        */
+/*! \file theory_builtin_rewriter.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
 
-#pragma once
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
+#define __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
 
 #include "theory/rewriter.h"
 #include "theory/theory.h"
@@ -41,8 +56,10 @@ public:
   static inline void init() {}
   static inline void shutdown() {}
 
-};
+};/* class TheoryBuiltinRewriter */
+
+}/* CVC4::theory::builtin namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
-}
-}
-}
+#endif /* __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H */
diff --git a/src/theory/bv/cd_set_collection.h b/src/theory/bv/cd_set_collection.h
index bd26a3595..33648660b 100644
--- a/src/theory/bv/cd_set_collection.h
+++ b/src/theory/bv/cd_set_collection.h
@@ -306,7 +306,7 @@ public:
    * String representation of a set.
    */
   std::string toString(reference_type set) {
-    stringstream out;
+    std::stringstream out;
     print(out, set);
     return out.str();
   }
diff --git a/src/theory/bv/slice_manager.h b/src/theory/bv/slice_manager.h
index 436ebaec0..8fc1e0b9d 100644
--- a/src/theory/bv/slice_manager.h
+++ b/src/theory/bv/slice_manager.h
@@ -328,7 +328,7 @@ bool SliceManager<TheoryBitvector>::isSliced(TNode node) const {
 template <class TheoryBitvector>
 inline void SliceManager<TheoryBitvector>::slice(TNode node, std::vector<Node>& sliced) {
 
-  Debug("slicing") << "SliceManager::slice(" << node << ")" << endl;
+  Debug("slicing") << "SliceManager::slice(" << node << ")" << std::endl;
 
   Assert(!isSliced(node));
 
@@ -343,7 +343,7 @@ inline void SliceManager<TheoryBitvector>::slice(TNode node, std::vector<Node>&
 
   // Get the base term slice set
   set_collection::reference_type nodeSliceSet = d_nodeSlicing[nodeBase];
-  Debug("slicing") << "SliceManager::slice(" << node << "): current: " << d_setCollection.toString(nodeSliceSet) << endl;
+  Debug("slicing") << "SliceManager::slice(" << node << "): current: " << d_setCollection.toString(nodeSliceSet) << std::endl;
   std::vector<size_t> slicePoints;
   d_setCollection.getElements(nodeSliceSet, low + 1, high - 1, slicePoints);
 
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index b600bc8f1..e183a592c 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -27,6 +27,8 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
 using namespace CVC4::theory::bv::utils;
 
+using namespace std;
+
 void TheoryBV::preRegisterTerm(TNode node) {
 
   Debug("bitvector") << "TheoryBV::preRegister(" << node << ")" << std::endl;
diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h
index e75f53711..7cfb46835 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_core.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_core.h
@@ -34,7 +34,7 @@ bool RewriteRule<ConcatFlatten>::applies(Node node) {
 template<>
 Node RewriteRule<ConcatFlatten>::apply(Node node) {
   NodeBuilder<> result(kind::BITVECTOR_CONCAT);
-  vector<Node> processing_stack;
+  std::vector<Node> processing_stack;
   processing_stack.push_back(node);
   while (!processing_stack.empty()) {
     Node current = processing_stack.back();
@@ -57,7 +57,7 @@ bool RewriteRule<ConcatExtractMerge>::applies(Node node) {
 
 template<>
 Node RewriteRule<ConcatExtractMerge>::apply(Node node) {
-  vector<Node> mergedExtracts;
+  std::vector<Node> mergedExtracts;
 
   Node current = node[0];
   bool mergeStarted = false;
@@ -115,7 +115,7 @@ bool RewriteRule<ConcatConstantMerge>::applies(Node node) {
 
 template<>
 Node RewriteRule<ConcatConstantMerge>::apply(Node node) {
-  vector<Node> mergedConstants;
+  std::vector<Node> mergedConstants;
   for (unsigned i = 0, end = node.getNumChildren(); i < end;) {
     if (node[i].getKind() != kind::CONST_BITVECTOR) {
       // If not a constant, just add it
@@ -187,7 +187,7 @@ Node RewriteRule<ExtractConcat>::apply(Node node) {
   int extract_high = utils::getExtractHigh(node);
   int extract_low = utils::getExtractLow(node);
 
-  vector<Node> resultChildren;
+  std::vector<Node> resultChildren;
 
   Node concat = node[0];
   for (int i = concat.getNumChildren() - 1; i >= 0 && extract_high >= 0; i--) {
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 08245afcb..9b545d25a 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -1,9 +1,21 @@
-/*
- * theory_bv_rewriter.cpp
- *
- *  Created on: Dec 21, 2010
- *      Author: dejan
- */
+/*********************                                                        */
+/*! \file theory_bv_rewriter.cpp
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
 
 #include "theory/theory.h"
 #include "theory/bv/theory_bv_rewriter.h"
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index 437ac49d3..bdf1c8d51 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -1,11 +1,26 @@
-/*
- * theory_bv_rewriter.h
- *
- *  Created on: Dec 21, 2010
- *      Author: dejan
- */
-
-#pragma once
+/*********************                                                        */
+/*! \file theory_bv_rewriter.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BV__THEORY_BV_REWRITER_H
+#define __CVC4__THEORY__BV__THEORY_BV_REWRITER_H
 
 #include "theory/rewriter.h"
 
@@ -29,8 +44,10 @@ public:
 
   static void init();
   static void shutdown();
-};
+};/* class TheoryBVRewriter */
+
+}/* CVC4::theory::bv namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
-}
-}
-}
+#endif /* __CVC4__THEORY__BV__THEORY_BV_REWRITER_H */
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index fe7ad7a9a..e896f9058 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -1,14 +1,28 @@
-/*
- * rewriter.cpp
- *
- *  Created on: Dec 13, 2010
- *      Author: dejan
- */
+/*********************                                                        */
+/*! \file rewriter.cpp
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
 
 #include "theory/theory.h"
 #include "theory/rewriter.h"
 #include "theory/rewriter_tables.h"
 
+using namespace std;
+
 namespace CVC4 {
 namespace theory {
 
diff --git a/src/theory/uf/morgan/union_find.h b/src/theory/uf/morgan/union_find.h
index c378e5a8b..794d7452c 100644
--- a/src/theory/uf/morgan/union_find.h
+++ b/src/theory/uf/morgan/union_find.h
@@ -105,23 +105,23 @@ inline TNode UnionFind<NodeType, NodeHash>::debugFind(TNode n) const {
 
 template <class NodeType, class NodeHash>
 inline TNode UnionFind<NodeType, NodeHash>::find(TNode n) {
-  Trace("ufuf") << "UFUF find of " << n << endl;
+  Trace("ufuf") << "UFUF find of " << n << std::endl;
   typename MapType::iterator i = d_map.find(n);
   if(i == d_map.end()) {
-    Trace("ufuf") << "UFUF   it is rep" << endl;
+    Trace("ufuf") << "UFUF   it is rep" << std::endl;
     return n;
   } else {
-    Trace("ufuf") << "UFUF   not rep: par is " << (*i).second << endl;
-    pair<TNode, TNode> pr = *i;
+    Trace("ufuf") << "UFUF   not rep: par is " << (*i).second << std::endl;
+    std::pair<TNode, TNode> pr = *i;
     // our iterator is invalidated by the recursive call to find(),
     // since it mutates the map
     TNode p = find(pr.second);
     if(p == pr.second) {
       return p;
     }
-    d_trace.push_back(make_pair(n, pr.second));
+    d_trace.push_back(std::make_pair(n, pr.second));
     d_offset = d_trace.size();
-    Trace("ufuf") << "UFUF   setting canon of " << n << " : " << p << " @ " << d_trace.size() << endl;
+    Trace("ufuf") << "UFUF   setting canon of " << n << " : " << p << " @ " << d_trace.size() << std::endl;
     pr.second = p;
     d_map.insert(pr);
     return p;
@@ -133,9 +133,9 @@ inline void UnionFind<NodeType, NodeHash>::setCanon(TNode n, TNode newParent) {
   Assert(d_map.find(n) == d_map.end());
   Assert(d_map.find(newParent) == d_map.end());
   if(n != newParent) {
-    Trace("ufuf") << "UFUF setting canon of " << n << " : " << newParent << " @ " << d_trace.size() << endl;
+    Trace("ufuf") << "UFUF setting canon of " << n << " : " << newParent << " @ " << d_trace.size() << std::endl;
     d_map[n] = newParent;
-    d_trace.push_back(make_pair(n, TNode::null()));
+    d_trace.push_back(std::make_pair(n, TNode::null()));
     d_offset = d_trace.size();
   }
 }
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index e71f74fea..744a3d966 100644
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -1,11 +1,26 @@
-/*
- * theory_uf_rewriter.h
- *
- *  Created on: Dec 21, 2010
- *      Author: dejan
- */
+/*********************                                                        */
+/*! \file theory_uf_rewriter.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
 
-#pragma once
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__UF__THEORY_UF_REWRITER_H
+#define __CVC4__THEORY__UF__THEORY_UF_REWRITER_H
 
 #include "theory/rewriter.h"
 
@@ -42,8 +57,10 @@ public:
   static inline void init() {}
   static inline void shutdown() {}
 
-};
+};/* class TheoryUfRewriter */
+
+}/* CVC4::theory::uf namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
-}
-}
-}
+#endif /* __CVC4__THEORY__UF__THEORY_UF_REWRITER_H */