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.

2 files changed, 36 insertions, 19 deletions

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