From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 26 Feb 2011 22:19:47 +0000 (+0000)
Subject: Commit to fix bug 241 (improper "using namespace std" in a header).  This caused... 
X-Git-Tag: cvc5-1.0.0~8686
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3548c7e5f6afed4e07bf9a70f0403952c9262519;p=cvc5.git

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.
---

diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl
index 5cf543459..db3ac47da 100755
--- a/contrib/update-copyright.pl
+++ b/contrib/update-copyright.pl
@@ -2,7 +2,7 @@
 #
 # update-copyright.pl
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2009, 2010  The CVC4 Project
+# Copyright (c) 2009, 2010, 2011  The CVC4 Project
 #
 # usage: update-copyright [ files/directories... ]
 #
@@ -34,7 +34,7 @@ my $excluded_paths = '^src/parser/antlr_input_imports.cpp$';
 
 # Years of copyright for the template.  E.g., the string
 # "1985, 1987, 1992, 1997, 2008" or "2006-2009" or whatever.
-my $years = '2009, 2010';
+my $years = '2009, 2010, 2011';
 
 my $standard_template = <<EOF;
  ** This file is part of the CVC4 prototype.
@@ -91,7 +91,110 @@ EOF
 
 print "Updating sources...\n";
 
-recurse(shift @searchdirs) while $#searchdirs >= 0;
+while($#searchdirs >= 0) {
+  my $dir = shift @searchdirs;
+  my $mode = (stat($dir))[2] || warn "file or directory \`$dir' does not exist!";
+  my $is_directory = S_ISDIR($mode);
+  if($is_directory) {
+    recurse($dir);
+  } else {
+    if($dir =~ m,^(.*)\/([^/]*)$,) {
+      my($dir, $file) = ($1, $2);
+      if($dir eq "") {
+        $dir = "/";
+      }
+      handleFile($dir, $file);
+    } else {
+      handleFile(".", $dir);
+    }
+  }
+}
+
+sub handleFile {
+  my ($srcdir, $file) = @_;
+  next if !($file =~ /\.(c|cc|cpp|C|h|hh|hpp|H|y|yy|ypp|Y|l|ll|lpp|L|g)$/);
+  next if ($srcdir.'/'.$file) =~ /$excluded_paths/;
+  print "$srcdir/$file...";
+  my $infile = $srcdir.'/'.$file;
+  my $outfile = $srcdir.'/#'.$file.'.tmp';
+  open(my $IN, $infile) || die "error opening $infile for reading";
+  open(my $OUT, '>', $outfile) || die "error opening $outfile for writing";
+  open(my $AUTHOR, "$dir/get-authors " . $infile . '|');
+  my $author = <$AUTHOR>; chomp $author;
+  my $major_contributors = <$AUTHOR>; chomp $major_contributors;
+  my $minor_contributors = <$AUTHOR>; chomp $minor_contributors;
+  close $AUTHOR;
+  $_ = <$IN>;
+  if(m,^(%{)?/\*(\*| )\*\*\*,) {
+    print "updating\n";
+    if($file =~ /\.(y|yy|ypp|Y)$/) {
+      print $OUT "%{/*******************                                                        */\n";
+      print $OUT "/** $file\n";
+    } elsif($file =~ /\.g$/) {
+      # avoid javadoc-style comment here; antlr complains
+      print $OUT "/* *******************                                                        */\n";
+      print $OUT "/*! \\file $file\n";
+    } else {
+      print $OUT "/*********************                                                        */\n";
+      print $OUT "/*! \\file $file\n";
+    }
+    print $OUT " ** \\verbatim\n";
+    print $OUT " ** Original author: $author\n";
+    print $OUT " ** Major contributors: $major_contributors\n";
+    print $OUT " ** Minor contributors (to current version): $minor_contributors\n";
+    print $OUT $standard_template;
+    print $OUT " **\n";
+    while(my $line = <$IN>) {
+      last if $line =~ /^ \*\*\s*$/;
+    }
+  } else {
+    my $line = $_;
+    print "adding\n";
+    if($file =~ /\.(y|yy|ypp|Y)$/) {
+      print $OUT "%{/*******************                                                        */\n";
+      print $OUT "/*! \\file $file\n";
+    } elsif($file =~ /\.g$/) {
+      # avoid javadoc-style comment here; antlr complains
+      print $OUT "/* *******************                                                        */\n";
+      print $OUT "/*! \\file $file\n";
+    } else {
+      print $OUT "/*********************                                                        */\n";
+      print $OUT "/*! \\file $file\n";
+    }
+    print $OUT " ** \\verbatim\n";
+    print $OUT " ** Original author: $author\n";
+    print $OUT " ** Major contributors: $major_contributors\n";
+    print $OUT " ** Minor contributors (to current version): $minor_contributors\n";
+    print $OUT $standard_template;
+    print $OUT " **\n";
+    print $OUT " ** \\brief [[ Add one-line brief description here ]]\n";
+    print $OUT " **\n";
+    print $OUT " ** [[ Add lengthier description here ]]\n";
+    print $OUT " ** \\todo document this file\n";
+    print $OUT " **/\n\n";
+    print $OUT $line;
+    if($file =~ /\.(y|yy|ypp|Y)$/) {
+      while(my $line = <$IN>) {
+        chomp $line;
+        if($line =~ '\s*%{(.*)') {
+          print $OUT "$1\n";
+          last;
+        }
+        # just in case something's weird with the file ?
+        if(!($line =~ '\s*')) {
+          print $OUT "$line\n";
+          last;
+        }
+      }
+    }
+  }
+  while(my $line = <$IN>) {
+    print $OUT $line;
+  }
+  close $IN;
+  close $OUT;
+  rename($outfile, $infile) || die "can't rename working file \`$outfile' to \`$infile'";
+}
 
 sub recurse {
   my ($srcdir) = @_;
@@ -106,88 +209,7 @@ sub recurse {
       next if $file =~ /$excluded_directories/;
       recurse($srcdir.'/'.$file);
     } else {
-      next if !($file =~ /\.(c|cc|cpp|C|h|hh|hpp|H|y|yy|ypp|Y|l|ll|lpp|L|g)$/);
-      next if ($srcdir.'/'.$file) =~ /$excluded_paths/;
-      print "$srcdir/$file...";
-      my $infile = $srcdir.'/'.$file;
-      my $outfile = $srcdir.'/#'.$file.'.tmp';
-      open(my $IN, $infile) || die "error opening $infile for reading";
-      open(my $OUT, '>', $outfile) || die "error opening $outfile for writing";
-      open(my $AUTHOR, "$dir/get-authors " . $infile . '|');
-      my $author = <$AUTHOR>; chomp $author;
-      my $major_contributors = <$AUTHOR>; chomp $major_contributors;
-      my $minor_contributors = <$AUTHOR>; chomp $minor_contributors;
-      close $AUTHOR;
-      $_ = <$IN>;
-      if(m,^(%{)?/\*(\*| )\*\*\*,) {
-        print "updating\n";
-        if($file =~ /\.(y|yy|ypp|Y)$/) {
-          print $OUT "%{/*******************                                                        */\n";
-          print $OUT "/** $file\n";
-        } elsif($file =~ /\.g$/) {
-          # avoid javadoc-style comment here; antlr complains
-          print $OUT "/* *******************                                                        */\n";
-          print $OUT "/*! \\file $file\n";
-        } else {
-          print $OUT "/*********************                                                        */\n";
-          print $OUT "/*! \\file $file\n";
-        }
-        print $OUT " ** \\verbatim\n";
-        print $OUT " ** Original author: $author\n";
-        print $OUT " ** Major contributors: $major_contributors\n";
-        print $OUT " ** Minor contributors (to current version): $minor_contributors\n";
-        print $OUT $standard_template;
-        print $OUT " **\n";
-        while(my $line = <$IN>) {
-          last if $line =~ /^ \*\*\s*$/;
-        }
-      } else {
-        my $line = $_;
-        print "adding\n";
-        if($file =~ /\.(y|yy|ypp|Y)$/) {
-          print $OUT "%{/*******************                                                        */\n";
-          print $OUT "/*! \\file $file\n";
-        } elsif($file =~ /\.g$/) {
-          # avoid javadoc-style comment here; antlr complains
-          print $OUT "/* *******************                                                        */\n";
-          print $OUT "/*! \\file $file\n";
-        } else {
-          print $OUT "/*********************                                                        */\n";
-          print $OUT "/*! \\file $file\n";
-        }
-        print $OUT " ** \\verbatim\n";
-        print $OUT " ** Original author: $author\n";
-        print $OUT " ** Major contributors: $major_contributors\n";
-        print $OUT " ** Minor contributors (to current version): $minor_contributors\n";
-        print $OUT $standard_template;
-        print $OUT " **\n";
-        print $OUT " ** \\brief [[ Add one-line brief description here ]]\n";
-        print $OUT " **\n";
-        print $OUT " ** [[ Add lengthier description here ]]\n";
-        print $OUT " ** \\todo document this file\n";
-        print $OUT " **/\n\n";
-        print $OUT $line;
-        if($file =~ /\.(y|yy|ypp|Y)$/) {
-          while(my $line = <$IN>) {
-            chomp $line;
-            if($line =~ '\s*%{(.*)') {
-              print $OUT "$1\n";
-              last;
-            }
-            # just in case something's weird with the file ?
-            if(!($line =~ '\s*')) {
-              print $OUT "$line\n";
-              last;
-            }
-          }
-        }
-      }
-      while(my $line = <$IN>) {
-        print $OUT $line;
-      }
-      close $IN;
-      close $OUT;
-      rename($outfile, $infile) || die "can't rename working file \`$outfile' to \`$infile'";
+      handleFile($srcdir, $file);
     }
   }
   closedir $DIR;
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 18ed9b5da..28a90d741 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -197,13 +197,13 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type)
     } else {
         // Lemma
         vec<Lit> assigned_lits;
-        Debug("minisat::lemmas") << "Asserting lemma with " << ps.size() << " literals." << endl;
+        Debug("minisat::lemmas") << "Asserting lemma with " << ps.size() << " literals." << std::endl;
         bool lemmaSatisfied = false;
         for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
           if (ps[i] == ~p) {
             // We don't add clauses that represent splits directly, they are decision literals
             // so they will get decided upon and sent to the theory
-            Debug("minisat::lemmas") << "Lemma is a tautology." << endl;
+            Debug("minisat::lemmas") << "Lemma is a tautology." << std::endl;
             return true;
           }
           if (value(ps[i]) == l_Undef) {
@@ -216,7 +216,7 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type)
             p = ps[i];
             if (value(p) == l_True) lemmaSatisfied = true;
             assigned_lits.push(p);
-            Debug("minisat::lemmas") << proxy->getNode(p) << " has value " << value(p) << endl;
+            Debug("minisat::lemmas") << proxy->getNode(p) << " has value " << value(p) << std::endl;
           }
         }
         Assert(j >= 1 || lemmaSatisfied, "You are asserting a falsified lemma, produce a conflict instead!");
@@ -232,7 +232,7 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type)
           }
         }
         if (value(ps[1]) != l_Undef && max_level != -1) {
-          swap(ps[1], ps[max_level_j]);
+          std::swap(ps[1], ps[max_level_j]);
         }
         ps.shrink(i - j);
     }
@@ -249,7 +249,7 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type)
         clauses.push(cr);
 	attachClause(cr);
         if (propagate_first_literal) {
-          Debug("minisat::lemmas") << "Lemma propagating: " << (theory[var(ps[0])] ? proxy->getNode(ps[0]).toString() : "bool") << endl;
+          Debug("minisat::lemmas") << "Lemma propagating: " << (theory[var(ps[0])] ? proxy->getNode(ps[0]).toString() : "bool") << std::endl;
           lemma_propagated_literals.push(ps[0]);
           lemma_propagated_reasons.push(cr);
           propagating_lemmas.push(cr);
@@ -915,11 +915,11 @@ lbool Solver::search(int nof_conflicts)
         // If we have more assertions from lemmas, we continue
         if (problem_extended) {
 
-          Debug("minisat::lemmas") << "Problem extended with lemmas, adding propagations." << endl;
+          Debug("minisat::lemmas") << "Problem extended with lemmas, adding propagations." << std::endl;
 
           for (int i = 0, i_end = lemma_propagated_literals.size(); i < i_end; ++ i) {
             if (value(var(lemma_propagated_literals[i])) == l_Undef) {
-              Debug("minisat::lemmas") << "Lemma propagating: " << proxy->getNode(lemma_propagated_literals[i]) << endl;
+              Debug("minisat::lemmas") << "Lemma propagating: " << proxy->getNode(lemma_propagated_literals[i]) << std::endl;
               uncheckedEnqueue(lemma_propagated_literals[i], lemma_propagated_reasons[i]);
             }
           }
@@ -1080,7 +1080,7 @@ static double luby(double y, int x){
 // NOTE: assumptions passed in member-variable 'assumptions'.
 lbool Solver::solve_()
 {
-    Debug("minisat") << "nvars = " << nVars() << endl;
+    Debug("minisat") << "nvars = " << nVars() << std::endl;
 
     in_solve = true;
 
@@ -1123,7 +1123,7 @@ lbool Solver::solve_()
         model.growTo(nVars());
         for (int i = 0; i < nVars(); i++) {
           model[i] = value(i);
-          Debug("minisat") << i << " = " << model[i] << endl;
+          Debug("minisat") << i << " = " << model[i] << std::endl;
         }
     }else if (status == l_False && conflict.size() == 0)
         ok = false;
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 */
diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index 27b019378..56423e7d5 100644
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -20,8 +20,6 @@
 #ifndef __CVC4__CONFIGURATION_PRIVATE_H
 #define __CVC4__CONFIGURATION_PRIVATE_H
 
-using namespace std;
-
 namespace CVC4 {
 
 #ifdef CVC4_DEBUG