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

8 files changed, 35 insertions, 34 deletions

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index f75e74d63..69db89086 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -327,7 +327,7 @@ private:
   /**
    * Transforms the node into CNF recursively.
    * @param node the formula to transform
-   * @param negated wheather the literal is negated
+   * @param negated whether the literal is negated
    * @return the literal representing the root of the formula
    */
   SatLiteral toCNF(TNode node, bool negated = false);
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 102f8051b..c30f18d29 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file sat_module.h
+/*! \file sat_solver.h
  ** \verbatim
  ** Original author: lianah
- ** Major contributors: 
- ** Minor contributors (to current version): 
+ ** Major contributors: dejan
+ ** 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/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index 3b048af47..68f09eb72 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file sat_solver_factory.h
+/*! \file sat_solver_factory.cpp
  ** \verbatim
- ** Original author: lianah
- ** Major contributors:
- ** Minor contributors (to current version):
+ ** Original author: dejan
+ ** Major contributors: taking
+ ** Minor contributors (to current version): lianah
  ** 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/prop/sat_solver_registry.cpp b/src/prop/sat_solver_registry.cpp
index 01434bd80..53753d3e1 100644
--- a/src/prop/sat_solver_registry.cpp
+++ b/src/prop/sat_solver_registry.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file sat_solver_registry.h
+/*! \file sat_solver_registry.cpp
  ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters, dejan
- ** Minor contributors (to current version): barrett, cconway
+ ** 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/prop/sat_solver_registry.h b/src/prop/sat_solver_registry.h
index df1cf86f8..cf829849f 100644
--- a/src/prop/sat_solver_registry.h
+++ b/src/prop/sat_solver_registry.h
@@ -35,7 +35,7 @@ namespace CVC4 {
 namespace prop {
 
 /**
- * Interface for SAT solver constructors. Solvers should declare an instantiatiation of the
+ * Interface for SAT solver constructors. Solvers should declare an instantiation of the
  * SatSolverConstructor interface below.
  */
 class SatSolverConstructorInterface {
@@ -59,7 +59,7 @@ class SatSolverRegistry {
 
   /**
    * Register a SAT solver with the registry. The Constructor type should be a subclass
-   * of the SatSolverConstrutor.
+   * of the SatSolverConstructor.
    */
   template <typename Constructor>
   size_t registerSolver(const char* id) {
diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h
index 9dcc1c4bf..88ddb8107 100644
--- a/src/prop/sat_solver_types.h
+++ b/src/prop/sat_solver_types.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file cnf_stream.h
+/*! \file sat_solver_types.h
  ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters, dejan
- ** Minor contributors (to current version): barrett, cconway, kshitij
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): kshitij
  ** 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/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 15a383d92..668b57b40 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file sat.cpp
+/*! \file theory_proxy.cpp
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: dejan, taking, mdeters
- ** Minor contributors (to current version): kshitij
+ ** Major contributors: lianah, dejan, kshitij, mdeters
+ ** Minor contributors (to current version): barrett, 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
@@ -80,12 +80,13 @@ void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) {
 
 SatLiteral TheoryProxy::getNextDecisionRequest(bool &stopSearch) {
   TNode n = d_theoryEngine->getNextDecisionRequest();
-  if(not n.isNull())
+  if(not n.isNull()) {
     return d_cnfStream->getLiteral(n);
-  
+  }
+
   // If theory doesn't give us a deicsion ask the decision engine. It
-  // may return in undefSatLiteral in which case the sat solver figure
-  // it out something
+  // may return in undefSatLiteral in which case the sat solver uses
+  // whatever default heuristic it has.
   Assert(d_decisionEngine != NULL);
   Assert(stopSearch != true);
   SatLiteral ret = d_decisionEngine->getNext(stopSearch);
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 99aab8286..26357886c 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file sat.h
+/*! \file theory_proxy.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: taking, cconway, dejan
- ** Minor contributors (to current version): barrett, kshitij
+ ** Major contributors: kshitij, lianah, dejan
+ ** Minor contributors (to current version): taking, cconway
  ** 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