Various fixes to documentation---typos, some incomplete documentation fixed, \file tags corrected, copyright added to files that had it missing, etc.

I ensured that I didn't change any code with this commit, and even tested on the cluster to be doubly sure:

  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4655&reference_id=4646&p=0

59 files changed, 278 insertions, 186 deletions

diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h
index d1fac1e58..43cf54d37 100644
--- a/src/theory/arith/arith_priority_queue.h
+++ b/src/theory/arith/arith_priority_queue.h
@@ -50,7 +50,7 @@ namespace arith {
  *   to determine which to dequeue first.
  *
  * - Variable Order Queue
- *   This mode uses the variable order to determine which ArithVar is deuqued first.
+ *   This mode uses the variable order to determine which ArithVar is dequeued first.
  *
  * The transitions between the modes of operation are:
  *  Collection => Difference Queue
@@ -119,7 +119,7 @@ private:
   /**
    * Priority Queue of the basic variables that may be inconsistent.
    * Variables are ordered according to which violates its bound the most.
-   * This is a heuristic and makes no guarentees to terminate!
+   * This is a heuristic and makes no guarantees to terminate!
    * This heuristic comes from Alberto Griggio's thesis.
    */
   DifferenceArray d_diffQueue;
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 5ce27eb46..a478f3cfb 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -417,6 +417,6 @@ void ArithStaticLearner::addBound(TNode n) {
   }
 }
 
-}; /* namesapce arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
index d877339b3..66eb4d311 100644
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -84,7 +84,7 @@ private:
   void miplibTrick(TNode var, std::set<Rational>& values, NodeBuilder<>& learned);
 
 
-  /** These fields are designed to be accessable to ArithStaticLearner methods. */
+  /** These fields are designed to be accessible to ArithStaticLearner methods. */
   class Statistics {
   public:
     IntStat d_iteMinMaxApplications;
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index fb669cce4..6ac2338f3 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -259,10 +259,8 @@ inline Node flattenAnd(Node n){
   return NodeManager::currentNM()->mkNode(kind::AND, out);
 }
 
-}; /* namesapce arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
-
-
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
 #endif /* __CVC4__THEORY__ARITH__ARITH_UTILITIES_H */
diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h
index 924e91bf5..80190b065 100644
--- a/src/theory/arith/arithvar.h
+++ b/src/theory/arith/arithvar.h
@@ -62,8 +62,8 @@ public:
   virtual void operator()(Node n) = 0;
 };
 
-}; /* namesapce arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
 #endif /* __CVC4__THEORY__ARITH__ARITHVAR_H */
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 52f4c7014..b167acf40 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file congruence_manager.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  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/arith/congruence_manager.h"
 
 #include "theory/arith/constraint.h"
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index fd8eef1f1..83a5e7fb4 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -1,4 +1,21 @@
-
+/*********************                                                        */
+/*! \file congruence_manager.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  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"
 
@@ -179,7 +196,7 @@ private:
    */
   //void assertLiteral(bool eq, ArithVar s, TNode reason);
 
-  /** This sends a shared term to the uninterpretted equality engine. */
+  /** This sends a shared term to the uninterpreted equality engine. */
   //void addAssertionToEqualityEngine(bool eq, ArithVar s, TNode reason);
   void assertionToEqualityEngine(bool eq, ArithVar s, TNode reason);
 
@@ -241,10 +258,8 @@ private:
     ~Statistics();
   } d_statistics;
 
-};/* class CongruenceManager */
+};/* class ArithCongruenceManager */
 
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
-
-
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index ce338b5f3..0d8a0a8f4 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -1,3 +1,21 @@
+/*********************                                                        */
+/*! \file constraint.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  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"
 #include "theory/arith/constraint.h"
@@ -1369,6 +1387,6 @@ void ConstraintDatabase::unatePropEquality(Constraint curr, Constraint prevLB, C
   }
 }
 
-}/* arith namespace */
-}/* theory namespace */
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index be4197a26..56fa5dcdf 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -243,7 +243,7 @@ private:
    *
    * This is not context dependent, but may be set once.
    *
-   * This must be set if the constraint canbePropgated().
+   * This must be set if the constraint canBePropagated().
    * This must be set if the constraint assertedToTheTheory().
    * Otherwise, this may be null().
    */
@@ -290,7 +290,7 @@ private:
 
   /**
    * True if the equality has been split.
-   * Only meaningful if ContraintType == Equality.
+   * Only meaningful if ConstraintType == Equality.
    *
    * User Context Dependent.
    * This is initially false.
@@ -490,7 +490,7 @@ public:
   /**
    * Returns a explanation of the constraint that is appropriate for conflicts.
    *
-   * This is not appropraite for propagation!
+   * This is not appropriate for propagation!
    *
    * This is the minimum fringe of the implication tree s.t.
    * every constraint is assertedToTheTheory() or hasEqualityEngineProof().
@@ -507,7 +507,7 @@ public:
    * This is the minimum fringe of the implication tree s.t.
    * every constraint is assertedToTheTheory() or hasEqualityEngineProof().
    *
-   * This is not appropraite for propagation!
+   * This is not appropriate for propagation!
    * Use explainForPropagation() instead.
    */
   void explainForConflict(NodeBuilder<>& nb) const{
@@ -587,7 +587,7 @@ public:
   void propagate(const std::vector<Constraint>& b);
   /**
    * The only restriction is that this is not known be true.
-   * This propgates if there is a node.
+   * This propagates if there is a node.
    */
   void impliedBy(Constraint a);
   void impliedBy(Constraint a, Constraint b);
@@ -829,7 +829,7 @@ public:
    * If no such constraint exists, NullConstraint is returned.
    *
    * t must be either UpperBound or LowerBound.
-   * The returned value v is dominatated:
+   * The returned value v is dominated:
    *  If t is UpperBound, r <= v
    *  If t is LowerBound, r >= v
    */
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 38cff88ff..e3eae88b3 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -279,7 +279,7 @@ void DioSolver::enqueueInputConstraints(){
 
 /*TODO Currently linear in the size of the Queue
  *It is not clear if am O(log n) strategy would be better.
- *Right before this in the algorithm is a substition which could potentially
+ *Right before this in the algorithm is a substitution which could potentially
  *effect the key values of everything in the queue.
  */
 void DioSolver::moveMinimumByAbsToQueueFront(){
@@ -508,7 +508,7 @@ SumPair DioSolver::processEquationsForCut(){
 
 
 SumPair DioSolver::purifyIndex(TrailIndex i){
-  // TODO: "This uses the substition trail to reverse the substitions from the sum term. Using the proof term should be more efficient."
+  // TODO: "This uses the substitution trail to reverse the substitutions from the sum term. Using the proof term should be more efficient."
 
   SumPair curr = d_trail[i].d_eq;
 
diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
index b92aced4e..b6c9e3afb 100644
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -383,7 +383,7 @@ private:
   void debugPrintTrail(TrailIndex i) const;
 
 public:
-  /** These fields are designed to be accessable to TheoryArith methods. */
+  /** These fields are designed to be accessible to TheoryArith methods. */
   class Statistics {
   public:
 
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index 7efe349e5..95f8138d2 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file simplex.cpp
+/*! \file linear_equality.cpp
  ** \verbatim
  ** Original author: taking
  ** 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)
+ ** Copyright (c) 2009-2012  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
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index 7cac4c871..2553bedd0 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -63,7 +63,7 @@ private:
 public:
 
   /**
-   * Initailizes a LinearEqualityModule with a partial model, a tableau,
+   * Initializes a LinearEqualityModule with a partial model, a tableau,
    * and a callback function for when basic variables update their values.
    */
   LinearEqualityModule(ArithPartialModel& pm, Tableau& t, ArithVarCallBack& f):
@@ -145,7 +145,7 @@ public:
 
 
 private:
-  /** These fields are designed to be accessable to TheoryArith methods. */
+  /** These fields are designed to be accessible to TheoryArith methods. */
   class Statistics {
   public:
     IntStat d_statPivots, d_statUpdates;
diff --git a/src/theory/arith/matrix.cpp b/src/theory/arith/matrix.cpp
index 6320f87ce..a691d61da 100644
--- a/src/theory/arith/matrix.cpp
+++ b/src/theory/arith/matrix.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file tableau.cpp
+/*! \file matrix.cpp
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
  ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  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
diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h
index f0e17f8a4..5ed1b9ab2 100644
--- a/src/theory/arith/matrix.h
+++ b/src/theory/arith/matrix.h
@@ -336,7 +336,7 @@ public:
   typedef typename SuperT::const_iterator const_iterator;
 
   RowVector(MatrixEntryVector<T>* mev) : SuperT(mev){}
-};
+};/* class RowVector<T> */
 
 template <class T>
   class ColumnVector : public MatrixVector<T, false>
@@ -347,7 +347,7 @@ public:
   typedef typename SuperT::const_iterator const_iterator;
 
   ColumnVector(MatrixEntryVector<T>* mev) : SuperT(mev){}
-};
+};/* class ColumnVector<T> */
 
 template <class T>
 class Matrix {
@@ -919,7 +919,7 @@ private:
   /* Changes the basic variable on the row for basicOld to basicNew. */
   void rowPivot(ArithVar basicOld, ArithVar basicNew);
 
-};
+};/* class Tableau */
 
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index f42b6d398..b054f9804 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -977,7 +977,7 @@ public:
    */
   static Node computeQR(const Polynomial& p, const Integer& z);
 
-  /** Returns the coefficient assiociated with the VarList in the polynomial. */
+  /** Returns the coefficient associated with the VarList in the polynomial. */
   Constant getCoefficient(const VarList& vl) const;
 
   uint32_t maxLength() const{
@@ -1041,7 +1041,7 @@ public:
  * is known to implicitly be equal to 0.
  *
  * SumPairs do not have unique representations due to the potential for p = 0.
- * This makes them inappropraite for normal forms.
+ * This makes them inappropriate for normal forms.
  */
 class SumPair : public NodeWrapper {
 private:
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index 0fabe1a0f..99a6e4878 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -304,6 +304,6 @@ void ArithPartialModel::computeDelta(){
   d_deltaIsSafe = true;
 }
 
-}; /* namesapce arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 9ba44b102..33c6537de 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -271,7 +271,7 @@ private:
 
 
 
-  /** These fields are designed to be accessable to TheoryArith methods. */
+  /** These fields are designed to be accessible to TheoryArith methods. */
   class Statistics {
   public:
     IntStat d_statUpdateConflicts;
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 6174e9500..188f73c78 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -2284,6 +2284,6 @@ void TheoryArith::propagateCandidates(){
   }
 }
 
-}; /* namesapce arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 0431f543c..fd2925bf6 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -372,7 +372,7 @@ private:
   /**
    * Splits the disequalities in d_diseq that are violated using lemmas on demand.
    * returns true if any lemmas were issued.
-   * returns false if all disequalities are satisified in the current model.
+   * returns false if all disequalities are satisfied in the current model.
    */
   bool splitDisequalities();
 
@@ -433,7 +433,7 @@ private:
   /** Tracks the bounds that were updated in the current round. */
   DenseSet d_updatedBounds;
 
-  /** Tracks the basic variables where propagatation might be possible. */
+  /** Tracks the basic variables where propagation might be possible. */
   DenseSet d_candidateBasics;
 
   bool hasAnyUpdates() { return !d_updatedBounds.empty(); }
@@ -466,7 +466,7 @@ private:
   bool assertionCases(Constraint c);
 
   /**
-   * Returns the basic variable with the shorted row containg a non-basic variable.
+   * Returns the basic variable with the shorted row containing a non-basic variable.
    * If no such row exists, return ARITHVAR_SENTINEL.
    */
   ArithVar findShortestBasicRow(ArithVar variable);
@@ -493,7 +493,7 @@ private:
   /** Debugging only routine. Prints the model. */
   void debugPrintModel();
 
-  /** These fields are designed to be accessable to TheoryArith methods. */
+  /** These fields are designed to be accessible to TheoryArith methods. */
   class Statistics {
   public:
     IntStat d_statAssertUpperConflicts, d_statAssertLowerConflicts;
diff --git a/src/theory/arith/theory_arith_instantiator.cpp b/src/theory/arith/theory_arith_instantiator.cpp
index 48c8a30ee..f1b870c52 100644
--- a/src/theory/arith/theory_arith_instantiator.cpp
+++ b/src/theory/arith/theory_arith_instantiator.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file instantiator_arith_instantiator.cpp
+/*! \file theory_arith_instantiator.cpp
  ** \verbatim
  ** Original author: ajreynol
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  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
diff --git a/src/theory/arith/theory_arith_instantiator.h b/src/theory/arith/theory_arith_instantiator.h
index 524d16859..3880a49a7 100644
--- a/src/theory/arith/theory_arith_instantiator.h
+++ b/src/theory/arith/theory_arith_instantiator.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file instantiator_arith_instantiator.h
+/*! \file theory_arith_instantiator.h
  ** \verbatim
  ** Original author: ajreynol
  ** 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)
+ ** Copyright (c) 2009-2012  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
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index 796bc9e21..04934b1fa 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -264,7 +264,7 @@ public:
 
   /**
    * Propagate through the asserted circuit propagator. New information discovered by the propagator
-   * are put in the subsitutions vector used in construction.
+   * are put in the substitutions vector used in construction.
    *
    * @return true iff conflict found
    */
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index c063245a5..bb6dfe40b 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -516,7 +516,7 @@ void DefaultMultBB (TNode node, Bits& res, Bitblaster* bb) {
 }
 
 void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaulPlusBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultPlusBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_PLUS &&
          res.size() == 0);
 
@@ -537,7 +537,7 @@ void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) {
 
 
 void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefautSubBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultSubBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_SUB &&
          node.getNumChildren() == 2 &&
          bits.size() == 0);
@@ -555,7 +555,7 @@ void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) {
 }
 
 void DefaultNegBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefautNegBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultNegBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_NEG);
   
   Bits a;
@@ -633,7 +633,7 @@ void uDivModRec(const Bits& a, const Bits& b, Bits& q, Bits& r, unsigned rec_wid
 }
 
 void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefautUdivBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_UDIV &&  q.size() == 0);
 
   Bits a, b;
@@ -649,7 +649,7 @@ void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) {
 }
 
 void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefautUremBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_UREM &&  rem.size() == 0);
 
   Bits a, b;
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index a5a9b9a7e..24d6b300b 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file bv_subtheory_eq_bitblast.cpp
+/*! \file bv_subtheory_bitblast.cpp
  ** \verbatim
- ** Original author: lianah
- ** Major contributors: dejan
+ ** 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)
+ ** Copyright (c) 2009-2012  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
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 0a8f046b7..324921f9a 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file bv_subtheory_eq_bitblast.h
+/*! \file bv_subtheory_bitblast.h
  ** \verbatim
- ** Original author: lianah
- ** Major contributors: dejan
+ ** 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)
+ ** Copyright (c) 2009-2012  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
diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
index 8cbf99ae9..005be88a8 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file theory_bv_rewrite_rules_core.h
+/*! \file theory_bv_rewrite_rules_constant_evaluation.h
  ** \verbatim
  ** Original author: lianah
- ** Major contributors: none
- ** Minor contributors (to current version): 
+ ** Major contributors: barrett
+ ** 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)
+ ** Copyright (c) 2009-2012  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
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index 506570ed2..48df9492d 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file theory_bv_rewrite_rules_core.h
+/*! \file theory_bv_rewrite_rules_operator_elimination.h
  ** \verbatim
  ** Original author: lianah
- ** Major contributors: none
- ** Minor contributors (to current version): 
+ ** Major contributors: barrett
+ ** 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)
+ ** Copyright (c) 2009-2012  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
@@ -65,7 +65,7 @@ bool RewriteRule<SgtEliminate>::applies(TNode node) {
 
 template<>
 Node RewriteRule<SgtEliminate>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RgewriteRule<UgtEliminate>(" << node << ")" << std::endl;
+  BVDebug("bv-rewrite") << "RewriteRule<SgtEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   TNode b = node[1];
   Node result = utils::mkNode(kind::BITVECTOR_SLT, b, a);
diff --git a/src/theory/datatypes/theory_datatypes_instantiator.h b/src/theory/datatypes/theory_datatypes_instantiator.h
index 5c52f7f48..ab5703757 100644
--- a/src/theory/datatypes/theory_datatypes_instantiator.h
+++ b/src/theory/datatypes/theory_datatypes_instantiator.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file instantiator_datatypes_instantiator.h
+/*! \file theory_datatypes_instantiator.h
  ** \verbatim
  ** Original author: ajreynol
  ** 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)
+ ** Copyright (c) 2009-2012  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
diff --git a/src/theory/inst_match.h b/src/theory/inst_match.h
index 73a99bcc5..dcb9190a1 100644
--- a/src/theory/inst_match.h
+++ b/src/theory/inst_match.h
@@ -277,7 +277,7 @@ public:
   virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0;
   /** get the next match.  must call reset( eqc ) before this function. */
   virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0;
-  /** return true if whatever Node is subsituted for the variables the
+  /** return true if whatever Node is substituted for the variables the
       given Node can't match the pattern */
   virtual bool nonunifiable( TNode t, const std::vector<Node> & vars) = 0;
   /** add instantiations directly */
@@ -323,7 +323,7 @@ private:
   bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe );
 public:
   /** get the match against ground term or formula t.
-      d_match_mattern and t should have the same shape.
+      d_match_pattern and t should have the same shape.
       only valid for use where !d_match_pattern.isNull().
   */
   bool getMatch( Node t, InstMatch& m, QuantifiersEngine* qe );
@@ -346,7 +346,7 @@ public:
   void reset( Node eqc, QuantifiersEngine* qe );
   /** get the next match.  must call reset( eqc ) before this function. */
   bool getNextMatch( InstMatch& m, QuantifiersEngine* qe );
-  /** return true if whatever Node is subsituted for the variables the
+  /** return true if whatever Node is substituted for the variables the
       given Node can't match the pattern */
   bool nonunifiable( TNode t, const std::vector<Node> & vars);
   /** add instantiations */
@@ -371,9 +371,9 @@ private:
                                std::vector< IndexedTrie >& unique_var_tries,
                                int uvtIndex, InstMatchTrie* tr = NULL, int trieIndex = 0 );
 private:
-  /** var contains (variable indicies) for each pattern node */
+  /** var contains (variable indices) for each pattern node */
   std::map< Node, std::vector< int > > d_var_contains;
-  /** variable indicies contained to pattern nodes */
+  /** variable indices contained to pattern nodes */
   std::map< int, std::vector< Node > > d_var_to_node;
   /** quantifier to use */
   Node d_f;
@@ -396,7 +396,7 @@ public:
   void reset( Node eqc, QuantifiersEngine* qe );
   /** get the next match.  must call reset( eqc ) before this function. (not implemented) */
   bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }
-  /** return true if whatever Node is subsituted for the variables the
+  /** return true if whatever Node is substituted for the variables the
       given Node can't match the pattern */
   bool nonunifiable( TNode t, const std::vector<Node> & vars) { return true; }
   /** add instantiations */
@@ -428,7 +428,7 @@ public:
   void reset( Node eqc, QuantifiersEngine* qe ) {}
   /** get the next match.  must call reset( eqc ) before this function. (not implemented) */
   bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }
-  /** return true if whatever Node is subsituted for the variables the
+  /** return true if whatever Node is substituted for the variables the
       given Node can't match the pattern */
   bool nonunifiable( TNode t, const std::vector<Node> & vars) { return true; }
   /** add instantiations */
diff --git a/src/theory/inst_match_impl.h b/src/theory/inst_match_impl.h
index b38bcb6f5..8ac5fd34f 100644
--- a/src/theory/inst_match_impl.h
+++ b/src/theory/inst_match_impl.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file inst_match.h
+/*! \file inst_match_impl.h
  ** \verbatim
- ** Original author: ajreynol
+ ** Original author: bobot
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): taking, mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  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
diff --git a/src/theory/instantiator_default.h b/src/theory/instantiator_default.h
index 351d0c4a3..8e0e47231 100644
--- a/src/theory/instantiator_default.h
+++ b/src/theory/instantiator_default.h
@@ -40,7 +40,7 @@ public:
   void assertNode( Node assertion );
   /** identify */
   std::string identify() const { return std::string("InstantiatorDefault"); }
-};/* class Instantiatior */
+};/* class InstantiatorDefault */
 
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index 4031efdf9..cf6691918 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file instantiation_engine.h
+/*! \file model_engine.h
  ** \verbatim
  ** Original author: ajreynol
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** 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)
+ ** Copyright (c) 2009-2012  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
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 0fba9d59e..4850d999b 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file theory_quantifiers_rewriter.cpp
+/*! \file quantifiers_rewriter.cpp
  ** \verbatim
  ** Original author: ajreynol
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** 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)
+ ** Copyright (c) 2009-2012  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
diff --git a/src/theory/quantifiers/theory_quantifiers_instantiator.h b/src/theory/quantifiers/theory_quantifiers_instantiator.h
index dda3bfeaa..39e34c319 100644
--- a/src/theory/quantifiers/theory_quantifiers_instantiator.h
+++ b/src/theory/quantifiers/theory_quantifiers_instantiator.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file instantiator_quantifiers_instantiator.h
+/*! \file theory_quantifiers_instantiator.h
  ** \verbatim
  ** Original author: ajreynol
  ** 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)
+ ** Copyright (c) 2009-2012  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
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index 4169cb9fe..afca18b76 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -85,7 +85,7 @@ class Rewriter {
   static RewriteResponse callPostRewrite(theory::TheoryId theoryId, TNode node);
 
   /**
-   * Calls the equality-rewruter for the given theory.
+   * Calls the equality-rewriter for the given theory.
    */
   static Node callRewriteEquality(theory::TheoryId theoryId, TNode equality);
 
diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp
index 0072a36e9..0d7f5005a 100644
--- a/src/theory/rewriterules/theory_rewriterules.cpp
+++ b/src/theory/rewriterules/theory_rewriterules.cpp
@@ -1,12 +1,11 @@
-/*********************                                                       */
-/*! \file rewrite_engine.cpp
+/*********************                                                        */
+/*! \file theory_rewriterules.cpp
  ** \verbatim
- ** Original author: ajreynolds
+ ** Original author: ajreynol
  ** Major contributors: bobot
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011
- ** The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  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
diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h
index 499535687..e47fd2fd4 100644
--- a/src/theory/rewriterules/theory_rewriterules.h
+++ b/src/theory/rewriterules/theory_rewriterules.h
@@ -1,12 +1,11 @@
-/*********************                                                       */
-/*! \file rewrite_engine.h
+/*********************                                                        */
+/*! \file theory_rewriterules.h
  ** \verbatim
  ** Original author: ajreynol
  ** Major contributors: bobot
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011
- ** The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  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
@@ -230,7 +229,7 @@ private:
    */
   void propagateRule(const RuleInst * r, TCache cache);
 
-  /** Auxillary functions */
+  /** Auxiliary functions */
 private:
   /** A guard is verify, notify the Guarded */
   void notification(GList * const lpropa, bool b);
diff --git a/src/theory/rewriterules/theory_rewriterules_params.h b/src/theory/rewriterules/theory_rewriterules_params.h
index ecb5385f9..9ab2ae3e7 100644
--- a/src/theory/rewriterules/theory_rewriterules_params.h
+++ b/src/theory/rewriterules/theory_rewriterules_params.h
@@ -1,12 +1,11 @@
-/*********************                                                       */
-/*! \file rewrite_engine.cpp
+/*********************                                                        */
+/*! \file theory_rewriterules_params.h
  ** \verbatim
  ** Original author: bobot
  ** 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)
+ ** Copyright (c) 2009-2012  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
@@ -67,7 +66,7 @@ static const size_t checkSlowdown = 10;
 static const bool useCurrentModel = false;
 
 /**
-   Simulate rewritting by tagging rewritten terms.
+   Simulate rewriting by tagging rewritten terms.
  */
 static const bool simulateRewritting = false;
 
diff --git a/src/theory/rewriterules/theory_rewriterules_preprocess.h b/src/theory/rewriterules/theory_rewriterules_preprocess.h
index 5d9cebfec..c90edcf27 100644
--- a/src/theory/rewriterules/theory_rewriterules_preprocess.h
+++ b/src/theory/rewriterules/theory_rewriterules_preprocess.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file rewriterules.h
+/*! \file theory_rewriterules_preprocess.h
  ** \verbatim
  ** Original author: bobot
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  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
diff --git a/src/theory/rewriterules/theory_rewriterules_rewriter.h b/src/theory/rewriterules/theory_rewriterules_rewriter.h
index 3d01dc2a5..8638c49b4 100644
--- a/src/theory/rewriterules/theory_rewriterules_rewriter.h
+++ b/src/theory/rewriterules/theory_rewriterules_rewriter.h
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file theory_rewriterules_rewriter.h
+ ** \verbatim
+ ** Original author: bobot
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  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__REWRITERULES__THEORY_REWRITERULES_REWRITER_H
diff --git a/src/theory/rewriterules/theory_rewriterules_rules.cpp b/src/theory/rewriterules/theory_rewriterules_rules.cpp
index 9847f1727..d66fc78cb 100644
--- a/src/theory/rewriterules/theory_rewriterules_rules.cpp
+++ b/src/theory/rewriterules/theory_rewriterules_rules.cpp
@@ -1,12 +1,11 @@
-/*********************                                                       */
-/*! \file rewrite_engine.cpp
+/*********************                                                        */
+/*! \file theory_rewriterules_rules.cpp
  ** \verbatim
- ** Original author: ajreynolds
- ** Major contributors: bobot
- ** Minor contributors (to current version): none
+ ** Original author: bobot
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011
- ** The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  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
@@ -153,7 +152,7 @@ void TheoryRewriteRules::addRewriteRule(const Node r)
     };
     break;
   default:
-    Unreachable("RewriteRules can be of only threee kinds");
+    Unreachable("RewriteRules can be of only three kinds");
   };
   /* Add the other guards */
   TNode g = r[1];
diff --git a/src/theory/rewriterules/theory_rewriterules_rules.h b/src/theory/rewriterules/theory_rewriterules_rules.h
index a8e70f3e6..8610dffca 100644
--- a/src/theory/rewriterules/theory_rewriterules_rules.h
+++ b/src/theory/rewriterules/theory_rewriterules_rules.h
@@ -1,12 +1,11 @@
-/*********************                                                       */
-/*! \file rewrite_engine.h
+/*********************                                                        */
+/*! \file theory_rewriterules_rules.h
  ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: bobot
+ ** Original author: bobot
+ ** 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)
+ ** Copyright (c) 2009-2012  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
diff --git a/src/theory/rewriterules/theory_rewriterules_type_rules.h b/src/theory/rewriterules/theory_rewriterules_type_rules.h
index 5a0e8c5e0..8bc4522a1 100644
--- a/src/theory/rewriterules/theory_rewriterules_type_rules.h
+++ b/src/theory/rewriterules/theory_rewriterules_type_rules.h
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file theory_rewriterules_type_rules.h
+ ** \verbatim
+ ** Original author: bobot
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  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__REWRITERULES__THEORY_REWRITERULES_TYPE_RULES_H
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index 4a6cac969..fb972b73f 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -1,15 +1,18 @@
 /*********************                                                        */
-/*! \file node_visitor.h
+/*! \file shared_terms_database.h
  ** \verbatim
  ** Original author: dejan
- ** Major contributors:
- ** Minor contributors (to current version):
+ ** Major contributors: mdeters
+ ** 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)
+ ** Copyright (c) 2009-2012  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
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
  **/
 
 #pragma once
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index b0b712356..ab6b27dff 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -1,15 +1,18 @@
 /*********************                                                        */
-/*! \file term_registration_visitor.h
+/*! \file term_registration_visitor.cpp
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): taking, barrett
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009-2012  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
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
  **/
 
 #include "theory/term_registration_visitor.h"
diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h
index ac3494193..c9c033bdd 100644
--- a/src/theory/term_registration_visitor.h
+++ b/src/theory/term_registration_visitor.h
@@ -1,15 +1,18 @@
 /*********************                                                        */
-/*! \file node_visitor.h
+/*! \file term_registration_visitor.h
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: 
- ** Minor contributors (to current version):
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  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
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
  **/
 
 #include "cvc4_private.h"
@@ -109,7 +112,7 @@ class SharedTermsVisitor {
   SharedTermsDatabase& d_sharedTerms;
 
   /**
-   * Cache from proprocessing of atoms.
+   * Cache from preprocessing of atoms.
    */
   typedef std::hash_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap;
   TNodeVisitedMap d_visited;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 0e7d7d51c..4ab2c779c 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1062,7 +1062,7 @@ static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {
 
 
 Node TheoryEngine::getExplanation(TNode node) {
-  Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current proagation index = " << d_propagationMapTimestamp << std::endl;
+  Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current propagation index = " << d_propagationMapTimestamp << std::endl;
 
   bool polarity = node.getKind() != kind::NOT;
   TNode atom = polarity ? node : node[0];
@@ -1237,7 +1237,7 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
       explanation = theoryOf(toExplain.theory)->explain(toExplain.node);
     }
     Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.theory << std::endl;
-    Assert(explanation != toExplain.node, "wansn't sent to you, so why are you explaining it trivially");
+    Assert(explanation != toExplain.node, "wasn't sent to you, so why are you explaining it trivially");
     // Mark the explanation
     NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp);
     explanationVector.push_back(newExplain);
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 0452d13aa..3d70ffa6b 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -503,7 +503,7 @@ public:
   void preprocessStart();
 
   /**
-   * Runs theory specific preprocesssing on the non-Boolean parts of
+   * Runs theory specific preprocessing on the non-Boolean parts of
    * the formula.  This is only called on input assertions, after ITEs
    * have been removed.
    */
diff --git a/src/theory/theory_registrar.h b/src/theory/theory_registrar.h
index 810ef1f67..372172e99 100644
--- a/src/theory/theory_registrar.h
+++ b/src/theory/theory_registrar.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file registrar.h
+/*! \file theory_registrar.h
  ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
+ ** Original author: lianah
+ ** 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)
+ ** Copyright (c) 2009-2012  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
diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index 44f009bc0..f827b9ee7 100644
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -19,7 +19,7 @@
 #include "cvc4_public.h"
 
 #ifndef __CVC4__THEORY__THEORY_TEST_UTILS_H
-#define __CVC4__THEORY__ITHEORY_TEST_UTILS_H
+#define __CVC4__THEORY__THEORY_TEST_UTILS_H
 
 #include "util/Assert.h"
 #include "expr/node.h"
diff --git a/src/theory/theoryof_mode.h b/src/theory/theoryof_mode.h
index 533704a39..0ce72449d 100644
--- a/src/theory/theoryof_mode.h
+++ b/src/theory/theoryof_mode.h
@@ -1,19 +1,19 @@
 /*********************                                                        */
-/*! \file theory.h
+/*! \file theoryof_mode.h
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: dejan
  ** Minor contributors (to current version): taking, barrett
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011, 2012  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 Base of the theory interface.
+ ** \brief Option selection for theoryOf() operation
  **
- ** Base of the theory interface.
+ ** Option selection for theoryOf() operation.
  **/
 
 #pragma once
@@ -29,8 +29,8 @@ enum TheoryOfMode {
   THEORY_OF_TYPE_BASED,
   /** Variables are uninterpreted, constants are with the type, equalities prefer parametric */
   THEORY_OF_TERM_BASED
-};
+};/* enum TheoryOfMode */
 
-}
-}
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 54fe8e508..fe75b5f59 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file equality_engine_impl.h
+/*! \file equality_engine.cpp
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): taking, mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  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
@@ -1701,7 +1701,7 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger
 
   // This is the class trigger set
   const TriggerTermSet& triggerSet = getTriggerTermSet(triggerSetRef); 
-  // Go throught the disequalities and notify
+  // Go through the disequalities and notify
   TaggedEqualitiesSet::const_iterator it = disequalitiesToNotify.begin();
   TaggedEqualitiesSet::const_iterator it_end = disequalitiesToNotify.end();
   for (; !d_done && it != it_end; ++ it) {
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 5a5b62105..9228e29d4 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -142,7 +142,7 @@ public:
 
 
 /**
- * Class for keeping an incremental congurence closure over a set of terms. It provides
+ * Class for keeping an incremental congruence closure over a set of terms. It provides
  * notifications via an EqualityEngineNotify object.
  */
 class EqualityEngine : public context::ContextNotifyObj {
@@ -226,7 +226,7 @@ private:
   /** Number of application lookups, for backtracking.  */
   context::CDO<DefaultSizeType> d_applicationLookupsCount;
 
-  /** Map from ids to the nodes (these need to be nodes as we pick-up the opreators) */
+  /** Map from ids to the nodes (these need to be nodes as we pick up the operators) */
   std::vector<Node> d_nodes;
 
   /** A context-dependents count of nodes */
@@ -301,7 +301,7 @@ private:
 
   /**
    * All the equality edges (twice as many as the number of asserted equalities. If an equality
-   * t1 = t2 is asserted, the edges added are -> t2, -> t1 (in this order). Hance, having the index
+   * t1 = t2 is asserted, the edges added are -> t2, -> t1 (in this order). Hence, having the index
    * of one of the edges you can reconstruct the original equality.
    */
   std::vector<EqualityEdge> d_equalityEdges;
@@ -384,7 +384,7 @@ private:
   std::vector<TriggerId> d_nodeTriggers;
 
   /**
-   * Map from ids to wheather they are constants (constants are always 
+   * Map from ids to whether they are constants (constants are always 
    * representatives of their class.
    */
   std::vector<bool> d_isConstant;
@@ -397,7 +397,7 @@ private:
   }
 
   /**
-   * Map from ids to wheather they are Boolean.
+   * Map from ids to whether they are Boolean.
    */
   std::vector<bool> d_isBoolean;
 
@@ -587,7 +587,7 @@ private:
   bool hasPropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId) const;
 
   /**
-   * Stores a propagated disequality for explanation purpooses and remembers the reasons. The
+   * Stores a propagated disequality for explanation purposes and remembers the reasons. The
    * reasons should be pushed on the reasons vector.
    */
   void storePropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId);
@@ -680,7 +680,7 @@ public:
 
   /**
    * Adds a predicate p with given polarity. The predicate asserted
-   * should be in the coungruence closure kinds (otherwise it's 
+   * should be in the congruence closure kinds (otherwise it's 
    * useless.
    *
    * @param p the (non-negated) predicate
@@ -781,7 +781,7 @@ public:
   size_t getSize(TNode t);
 
   /**
-   * Returns true if the engine is in a consistents state.
+   * Returns true if the engine is in a consistent state.
    */
   bool consistent() const { return !d_done; }
 
diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h
index 591b15bf4..054a6f153 100644
--- a/src/theory/uf/equality_engine_types.h
+++ b/src/theory/uf/equality_engine_types.h
@@ -115,7 +115,7 @@ struct DisequalityReasonRef {
 };
 
 /** 
- * We mantaint uselist where a node appears in, and this is the node
+ * We maintain uselist where a node appears in, and this is the node
  * of such a list. 
  */
 class UseListNode {
@@ -155,7 +155,7 @@ public:
  * Main class for representing nodes in the equivalence class. The 
  * nodes are a circular list, with the representative carrying the
  * size. Each individual node carries with itself the uselist of
- * functino applications it appears in and the list of asserted 
+ * function applications it appears in and the list of asserted 
  * disequalities it belongs to. In order to get these lists one must
  * traverse the entire class and pick up all the individual lists. 
  */
diff --git a/src/theory/uf/theory_uf_candidate_generator.h b/src/theory/uf/theory_uf_candidate_generator.h
index 948573439..668d619db 100644
--- a/src/theory/uf/theory_uf_candidate_generator.h
+++ b/src/theory/uf/theory_uf_candidate_generator.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file theory_uf_candidate generator.h
+/*! \file theory_uf_candidate_generator.h
  ** \verbatim
  ** Original author: ajreynol
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  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
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index a793b6a57..9d9be60e3 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -752,8 +752,8 @@ bool StrongSolverTheoryUf::ConflictFind::disambiguateTerms( OutputChannel* out )
                 }
                 Assert( children.size()>1 );
                 Node lem = NodeManager::currentNM()->mkNode( OR, children );
-                Debug( "uf-ss-lemma" ) << "*** Diambiguate lemma : " << lem << std::endl;
-                //Notice() << "*** Diambiguate lemma : " << lem << std::endl;
+                Debug( "uf-ss-lemma" ) << "*** Disambiguate lemma : " << lem << std::endl;
+                //Notice() << "*** Disambiguate lemma : " << lem << std::endl;
                 out->lemma( lem );
                 d_term_amb[ eq ] = false;
                 lemmaAdded = true;
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index e36441f6d..dde24394a 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -309,9 +309,9 @@ public:
   /** statistics class */
   Statistics d_statistics;
 
-  /** is relavant type */
+  /** is relevant type */
   static bool isRelevantType( TypeNode t );
-  /** involves relavant type */
+  /** involves relevant type */
   static bool involvesRelevantType( Node n );
 };/* class StrongSolverTheoryUf */
 
diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index d925a3366..58254df33 100644
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -523,7 +523,7 @@ void UnconstrainedSimplifier::processUnconstrained()
           }
           break;
 
-        // Array store - if both store and value are uncosntrained, so is resulting store
+        // Array store - if both store and value are unconstrained, so is resulting store
         case kind::STORE:
           if (((parent[0] == current &&
                 d_unconstrained.find(parent[2]) != d_unconstrained.end()) ||