* Numerous documentation fixes (fix doxygen warnings, add missing documentation, etc.).

* Remove sat_module.cpp, which was no longer used (was previously refactored?)

35 files changed, 98 insertions, 564 deletions

diff --git a/README b/README
index ed8edd53a..37c285639 100644
--- a/README
+++ b/README
@@ -5,7 +5,7 @@ This is a prerelease version of CVC4.
 To build, you'll need reasonably new automake, autoconf, and libtool
 installed (see below). Execute,
 
-    ./autogen.sh 
+    ./autogen.sh
     ./configure
     make
 
@@ -80,10 +80,10 @@ includes a diff of all changes made to cudd makefiles.
 *** Build dependencies
 
 The following tools and libraries are required to build CVC4 from
-scratch. 
+scratch.
 
 Automake v1.11
-Autoconf v2.61 
+Autoconf v2.61
 Libtool v2.2
 ANTLR3 v3.2
 
diff --git a/config/doxygen.cfg b/config/doxygen.cfg
index 71d434959..f4713b616 100644
--- a/config/doxygen.cfg
+++ b/config/doxygen.cfg
@@ -568,7 +568,12 @@ WARN_LOGFILE           =
 # directories like "/usr/src/myproject". Separate the files or directories
 # with spaces.
 
-INPUT                  = $(CVC4_DOXYGEN_INPUT)
+INPUT                  = $(SRCDIR)/AUTHORS \
+                         $(SRCDIR)/COPYING \
+                         $(SRCDIR)/NEWS \
+                         $(SRCDIR)/README \
+                         $(SRCDIR)/ChangeLog \
+                         $(CVC4_DOXYGEN_INPUT)
 
 # This tag can be used to specify the character encoding of the source files
 # that doxygen parses. Internally doxygen uses the UTF-8 encoding, which is
@@ -1242,7 +1247,7 @@ SEARCH_INCLUDES        = YES
 # contain include files that are not input files but should be processed by
 # the preprocessor.
 
-INCLUDE_PATH           = .
+INCLUDE_PATH           = . include $(SRCDIR)/src $(SRCDIR)/src/include
 
 # You can use the INCLUDE_FILE_PATTERNS tag to specify one or more wildcard
 # patterns (like *.h and *.hpp) to filter out the header-files in the
diff --git a/src/bindings/compat/c/c_interface.h b/src/bindings/compat/c/c_interface.h
index 14fea7478..379097c27 100644
--- a/src/bindings/compat/c/c_interface.h
+++ b/src/bindings/compat/c/c_interface.h
@@ -12,7 +12,7 @@
  * License to use, copy, modify, sell and/or distribute this software
  * and its documentation for any purpose is hereby granted without
  * royalty, subject to the terms and conditions defined in the \ref
- * LICENSE file provided with this distribution.
+ * COPYING file provided with this distribution.
  *
  * <hr>
  *
@@ -66,6 +66,8 @@ Type vc_subRangeType(VC vc, int lowerEnd, int upperEnd);
 
 //! Creates a subtype defined by the given predicate
 /*!
+ * \param vc the validity checker
+ *
  * \param pred is a predicate taking one argument of type T and returning
  * Boolean.  The resulting type is a subtype of T whose elements x are those
  * satisfying the predicate pred(x).
@@ -298,6 +300,7 @@ Expr vc_ratExprFromStr(VC vc, char* n, char* d, int base);
 
 //! Create a rational from a single string.
 /*!
+  \param vc the validity checker
   \param n can be a string containing an integer, a pair of integers
   "nnn/ddd", or a number in the fixed or floating point format.
   \param base is the base in which to interpret the string.
@@ -442,7 +445,8 @@ Expr vc_datatypeTestExpr(VC vc, char* constructor, Expr arg);
 // Quantifiers
 
 //! Create a bound variable.
-/*! \param name
+/*! \param vc the validity checker
+ * \param name
  * \param uid is a fresh unique string to distinguish this variable
  * from other bound variables with the same name
  * \param type
diff --git a/src/bindings/compat/c/c_interface_defs.h b/src/bindings/compat/c/c_interface_defs.h
index ee6c09e13..f30e9b797 100644
--- a/src/bindings/compat/c/c_interface_defs.h
+++ b/src/bindings/compat/c/c_interface_defs.h
@@ -1,9 +1,9 @@
 /*****************************************************************************/
 /*!
  * \file c_interface_defs.h
- * 
+ *
  * Author: Clark Barrett
- * 
+ *
  * Created: Thu Jun  5 13:16:26 2003
  *
  * <hr>
@@ -11,10 +11,10 @@
  * License to use, copy, modify, sell and/or distribute this software
  * and its documentation for any purpose is hereby granted without
  * royalty, subject to the terms and conditions defined in the \ref
- * LICENSE file provided with this distribution.
- * 
+ * COPYING file provided with this distribution.
+ *
  * <hr>
- * 
+ *
  */
 /*****************************************************************************/
 
diff --git a/src/bindings/compat/java/formula_value.h b/src/bindings/compat/java/formula_value.h
index 79f31f404..efcd32eea 100644
--- a/src/bindings/compat/java/formula_value.h
+++ b/src/bindings/compat/java/formula_value.h
@@ -1,6 +1,6 @@
 /*****************************************************************************/
 /*!
- *\file formulavalue.h
+ *\file formula_value.h
  *\brief enumerated type for value of formulas
  *
  * Author: Alexander Fuchs
@@ -13,7 +13,7 @@
  * and its documentation for any purpose is hereby granted without
  * royalty, subject to the terms and conditions defined in the \ref
  * LICENSE file provided with this distribution.
- * 
+ *
  * <hr>
  */
 /*****************************************************************************/
@@ -31,7 +31,7 @@ namespace CVC3 {
 typedef enum FormulaValue {
   TRUE_VAL,
   FALSE_VAL,
-  UNKNOWN_VAL 
+  UNKNOWN_VAL
 } FormulaValue;
 
 }
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 67000b1ba..77f4cd56c 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -21,8 +21,8 @@
  **/
 /*****************************************************************************/
 /*!
- *\file search_sat.cpp
- *\brief Implementation of Search engine with generic external sat solver
+ * file search_sat.cpp
+ * brief Implementation of Search engine with generic external sat solver
  *
  * Author: Clark Barrett
  *
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 5e7aebbec..804d3af9a 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file expr_manager_template.cpp
+/*! \file expr_manager.cpp
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: cconway, mdeters
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 158f17c14..8e0f23c6a 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file expr_manager_template.h
+/*! \file expr_manager.h
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: mdeters
@@ -210,7 +210,7 @@ public:
    *
    * @param kind the kind of expression to build
    * @param child1 the first subexpression
-   * @param children the remaining subexpressions
+   * @param otherChildren the remaining subexpressions
    * @return the n-ary expression
    */
   Expr mkExpr(Kind kind, Expr child1, const std::vector<Expr>& otherChildren);
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 365dc050f..a6f9f2cf6 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file expr_template.cpp
+/*! \file expr.cpp
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: mdeters
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 395bdff3a..c50e85ac2 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file expr_template.h
+/*! \file expr.h
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: mdeters
@@ -403,6 +403,7 @@ public:
    * @param types set to true to ascribe types to the output
    * expressions (might break language compliance, but good for
    * debugging expressions)
+   * @param dag the dagification threshold to use (0 == off)
    * @param language the language in which to output
    */
   void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
@@ -960,7 +961,7 @@ public:
 
 ${getConst_instantiations}
 
-#line 964 "${template}"
+#line 965 "${template}"
 
 namespace expr {
 
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 1acbed978..fc7d838a1 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file kind_template.h
+/*! \file kind.h
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: dejan
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index a954a7f70..dbaba664c 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file metakind_template.h
+/*! \file metakind.h
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h
index ee04b17fd..3f24d10f8 100644
--- a/src/expr/symbol_table.h
+++ b/src/expr/symbol_table.h
@@ -118,6 +118,8 @@ public:
    * @param name an identifier
    * @param params the parameters to the type
    * @param t the type to bind to <code>name</code>
+   * @param levelZero true to bind it globally (default is to bind it
+   * locally within the current scope)
    */
   void bindType(const std::string& name,
                 const std::vector<Type>& params,
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index 9359a6ab8..d559477f1 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file type_checker_template.cpp
+/*! \file type_checker.cpp
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h
index 1e983e86c..ee7a93144 100644
--- a/src/expr/type_properties_template.h
+++ b/src/expr/type_properties_template.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file type_properties_template.h
+/*! \file type_properties.h
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
diff --git a/src/options/base_options_template.cpp b/src/options/base_options_template.cpp
index 97d747652..e3d62936b 100644
--- a/src/options/base_options_template.cpp
+++ b/src/options/base_options_template.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file base_options_template.cpp
+/*! \file base_options.cpp
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
diff --git a/src/options/base_options_template.h b/src/options/base_options_template.h
index 211cb866a..97c19930e 100644
--- a/src/options/base_options_template.h
+++ b/src/options/base_options_template.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file base_options_template.h
+/*! \file base_options.h
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
diff --git a/src/options/options_holder_template.h b/src/options/options_holder_template.h
index 5b2c9a35d..2d37475f0 100644
--- a/src/options/options_holder_template.h
+++ b/src/options/options_holder_template.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file options_holder_template.h
+/*! \file options_holder.h
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 97a588414..560efdfe3 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file options_template.cpp
+/*! \file options.cpp
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
diff --git a/src/parser/input.h b/src/parser/input.h
index 1b8c97713..d47ca4d12 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -68,7 +68,7 @@ protected:
 public:
 
   /** Destructor. */
-  virtual ~InputStream() { 
+  virtual ~InputStream() {
     if( d_fileIsTemporary ) {
       remove(d_name.c_str());
     }
@@ -108,8 +108,8 @@ public:
     * @param filename the input filename
     * @param useMmap true if the parser should use memory-mapped I/O (default: false)
     */
-  static Input* newFileInput(InputLanguage lang, 
-                             const std::string& filename, 
+  static Input* newFileInput(InputLanguage lang,
+                             const std::string& filename,
                              bool useMmap = false)
     throw (InputStreamException, AssertionException);
 
@@ -118,9 +118,12 @@ public:
    * @param lang the input language
    * @param input the input stream
    * @param name the name of the stream, for use in error messages
+   * @param lineBuffered whether this Input should be line-buffered
+   * (false, the default, means that the entire Input might be read
+   * before being lexed and parsed)
    */
-  static Input* newStreamInput(InputLanguage lang, 
-                               std::istream& input, 
+  static Input* newStreamInput(InputLanguage lang,
+                               std::istream& input,
                                const std::string& name,
                                bool lineBuffered = false)
     throw (InputStreamException, AssertionException);
@@ -131,8 +134,8 @@ public:
    * @param input the input string
    * @param name the name of the stream, for use in error messages
    */
-  static Input* newStringInput(InputLanguage lang, 
-                               const std::string& input, 
+  static Input* newStringInput(InputLanguage lang,
+                               const std::string& input,
                                const std::string& name)
     throw (InputStreamException, AssertionException);
 
diff --git a/src/prop/sat_module.cpp b/src/prop/sat_module.cpp
deleted file mode 100644
index ca41eac2f..000000000
--- a/src/prop/sat_module.cpp
+++ /dev/null
@@ -1,478 +0,0 @@
-/*********************                                                        */
-/*! \file sat.cpp
- ** \verbatim
- ** Original author: cconway
- ** Major contributors: dejan, taking, mdeters, lianah
- ** 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 "prop/prop_engine.h"
-#include "prop/sat_module.h"
-#include "context/context.h"
-#include "theory/theory_engine.h"
-#include "expr/expr_stream.h"
-#include "prop/sat.h"
-
-// DPLLT Minisat
-#include "prop/minisat/simp/SimpSolver.h"
-
-// BV Minisat
-#include "prop/bvminisat/simp/SimpSolver.h"
-
-
-using namespace std; 
-
-namespace CVC4 {
-namespace prop {
-
-string SatLiteral::toString() {
-  ostringstream os;
-  os << (isNegated()? "~" : "") << getSatVariable() << " ";
-  return os.str(); 
-}
-
-MinisatSatSolver::MinisatSatSolver() :
-  d_minisat(new BVMinisat::SimpSolver())
-{
-  d_statistics.init(d_minisat); 
-}
-
-MinisatSatSolver::~MinisatSatSolver() {
-  delete d_minisat; 
-}
-
-void MinisatSatSolver::addClause(SatClause& clause, bool removable) {
-  Debug("sat::minisat") << "Add clause " << clause <<"\n"; 
-  BVMinisat::vec<BVMinisat::Lit> minisat_clause;
-  toMinisatClause(clause, minisat_clause);
-  // for(unsigned i = 0; i < minisat_clause.size(); ++i) {
-  //   d_minisat->setFrozen(BVMinisat::var(minisat_clause[i]), true); 
-  // }
-  d_minisat->addClause(minisat_clause);
-}
-
-SatVariable MinisatSatSolver::newVar(bool freeze){
-  return d_minisat->newVar(true, true, freeze);
-}
-
-void MinisatSatSolver::markUnremovable(SatLiteral lit){
-  d_minisat->setFrozen(BVMinisat::var(toMinisatLit(lit)), true);
-}
- 
-void MinisatSatSolver::interrupt(){
-  d_minisat->interrupt(); 
-}
-
-SatLiteralValue MinisatSatSolver::solve(){
-  return toSatLiteralValue(d_minisat->solve()); 
-}
-
-SatLiteralValue MinisatSatSolver::solve(long unsigned int& resource){
-  Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
-  if(resource == 0) {
-    d_minisat->budgetOff();
-  } else {
-    d_minisat->setConfBudget(resource);
-  }
-  BVMinisat::vec<BVMinisat::Lit> empty;
-  unsigned long conflictsBefore = d_minisat->conflicts;
-  SatLiteralValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
-  d_minisat->clearInterrupt();
-  resource = d_minisat->conflicts - conflictsBefore;
-  Trace("limit") << "<MinisatSatSolver::solve(): it took " << resource << " conflicts" << std::endl;
-  return result;
-}
-
-SatLiteralValue MinisatSatSolver::solve(const context::CDList<SatLiteral> & assumptions){
-  Debug("sat::minisat") << "Solve with assumptions ";
-  context::CDList<SatLiteral>::const_iterator it = assumptions.begin();
-  BVMinisat::vec<BVMinisat::Lit> assump; 
-  for(; it!= assumptions.end(); ++it) {
-    SatLiteral lit = *it;
-    Debug("sat::minisat") << lit <<" "; 
-    assump.push(toMinisatLit(lit)); 
-  }
-  Debug("sat::minisat") <<"\n";
-  
- SatLiteralValue result = toSatLiteralValue(d_minisat->solve(assump));
- return result;
-}
-
-
-void MinisatSatSolver::getUnsatCore(SatClause& unsatCore) {
-  // TODO add assertion to check the call was after an unsat call
-  for (int i = 0; i < d_minisat->conflict.size(); ++i) {
-    unsatCore.push_back(toSatLiteral(d_minisat->conflict[i])); 
-  }
-}
-
-SatLiteralValue MinisatSatSolver::value(SatLiteral l){
-    Unimplemented();
-    return SatValUnknown; 
-}
-
-SatLiteralValue MinisatSatSolver::modelValue(SatLiteral l){
-    Unimplemented();
-    return SatValUnknown; 
-}
-
-void MinisatSatSolver::unregisterVar(SatLiteral lit) {
-  // this should only be called when user context is implemented
-  // in the BVSatSolver 
-  Unreachable();
-}
-
-void MinisatSatSolver::renewVar(SatLiteral lit, int level) {
-  // this should only be called when user context is implemented
-  // in the BVSatSolver 
-
-  Unreachable(); 
-}
-
-int MinisatSatSolver::getAssertionLevel() const {
-  // we have no user context implemented so far
-  return 0;
-}
-
-// converting from internal Minisat representation
-
-SatVariable MinisatSatSolver::toSatVariable(BVMinisat::Var var) {
-  if (var == var_Undef) {
-    return undefSatVariable; 
-  }
-  return SatVariable(var);
-}
-
-BVMinisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) {
-  if (lit == undefSatLiteral) {
-    return BVMinisat::lit_Undef;
-  }
-  return BVMinisat::mkLit(lit.getSatVariable(), lit.isNegated()); 
-}
-
-SatLiteral MinisatSatSolver::toSatLiteral(BVMinisat::Lit lit) {
-  if (lit == BVMinisat::lit_Undef) {
-    return undefSatLiteral; 
-  }
-  
-  return SatLiteral(SatVariable(BVMinisat::var(lit)),
-                    BVMinisat::sign(lit)); 
-}
-
-SatLiteralValue MinisatSatSolver::toSatLiteralValue(bool res) {
-  if(res) return SatValTrue;
-  else return SatValFalse; 
-}
-
-SatLiteralValue MinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) {
-  if(res == (BVMinisat::lbool((uint8_t)0))) return SatValTrue;
-  if(res == (BVMinisat::lbool((uint8_t)2))) return SatValUnknown;
-  Assert(res == (BVMinisat::lbool((uint8_t)1)));
-  return SatValFalse; 
-}
-
-void MinisatSatSolver::toMinisatClause(SatClause& clause,
-                                           BVMinisat::vec<BVMinisat::Lit>& minisat_clause) {
-  for (unsigned i = 0; i < clause.size(); ++i) {
-    minisat_clause.push(toMinisatLit(clause[i])); 
-  }
-  Assert(clause.size() == (unsigned)minisat_clause.size()); 
-}
-
-void MinisatSatSolver::toSatClause(BVMinisat::vec<BVMinisat::Lit>& clause,
-                                       SatClause& sat_clause) {
-  for (int i = 0; i < clause.size(); ++i) {
-    sat_clause.push_back(toSatLiteral(clause[i])); 
-  }
-  Assert((unsigned)clause.size() == sat_clause.size()); 
-}
-
-
-// Satistics for MinisatSatSolver
-
-MinisatSatSolver::Statistics::Statistics() :
-  d_statStarts("theory::bv::bvminisat::starts"),
-  d_statDecisions("theory::bv::bvminisat::decisions"),
-  d_statRndDecisions("theory::bv::bvminisat::rnd_decisions"),
-  d_statPropagations("theory::bv::bvminisat::propagations"),
-  d_statConflicts("theory::bv::bvminisat::conflicts"),
-  d_statClausesLiterals("theory::bv::bvminisat::clauses_literals"),
-  d_statLearntsLiterals("theory::bv::bvminisat::learnts_literals"),
-  d_statMaxLiterals("theory::bv::bvminisat::max_literals"),
-  d_statTotLiterals("theory::bv::bvminisat::tot_literals"),
-  d_statEliminatedVars("theory::bv::bvminisat::eliminated_vars")
-{
-  StatisticsRegistry::registerStat(&d_statStarts);
-  StatisticsRegistry::registerStat(&d_statDecisions);
-  StatisticsRegistry::registerStat(&d_statRndDecisions);
-  StatisticsRegistry::registerStat(&d_statPropagations);
-  StatisticsRegistry::registerStat(&d_statConflicts);
-  StatisticsRegistry::registerStat(&d_statClausesLiterals);
-  StatisticsRegistry::registerStat(&d_statLearntsLiterals);
-  StatisticsRegistry::registerStat(&d_statMaxLiterals);
-  StatisticsRegistry::registerStat(&d_statTotLiterals);
-  StatisticsRegistry::registerStat(&d_statEliminatedVars);
-}
-
-MinisatSatSolver::Statistics::~Statistics() {
-  StatisticsRegistry::unregisterStat(&d_statStarts);
-  StatisticsRegistry::unregisterStat(&d_statDecisions);
-  StatisticsRegistry::unregisterStat(&d_statRndDecisions);
-  StatisticsRegistry::unregisterStat(&d_statPropagations);
-  StatisticsRegistry::unregisterStat(&d_statConflicts);
-  StatisticsRegistry::unregisterStat(&d_statClausesLiterals);
-  StatisticsRegistry::unregisterStat(&d_statLearntsLiterals);
-  StatisticsRegistry::unregisterStat(&d_statMaxLiterals);
-  StatisticsRegistry::unregisterStat(&d_statTotLiterals);
-  StatisticsRegistry::unregisterStat(&d_statEliminatedVars);
-}
-    
-void MinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){
-  d_statStarts.setData(minisat->starts);
-  d_statDecisions.setData(minisat->decisions);
-  d_statRndDecisions.setData(minisat->rnd_decisions);
-  d_statPropagations.setData(minisat->propagations);
-  d_statConflicts.setData(minisat->conflicts);
-  d_statClausesLiterals.setData(minisat->clauses_literals);
-  d_statLearntsLiterals.setData(minisat->learnts_literals);
-  d_statMaxLiterals.setData(minisat->max_literals);
-  d_statTotLiterals.setData(minisat->tot_literals);
-  d_statEliminatedVars.setData(minisat->eliminated_vars);
-}
-
-
-
-//// DPllMinisatSatSolver
-
-DPLLMinisatSatSolver::DPLLMinisatSatSolver() :
-  d_minisat(NULL), 
-  d_theoryProxy(NULL),
-  d_context(NULL)
-{}
-
-DPLLMinisatSatSolver::~DPLLMinisatSatSolver() {
-  delete d_minisat; 
-}
-
-SatVariable DPLLMinisatSatSolver::toSatVariable(Minisat::Var var) {
-  if (var == var_Undef) {
-    return undefSatVariable; 
-  }
-  return SatVariable(var);
-}
-
-Minisat::Lit DPLLMinisatSatSolver::toMinisatLit(SatLiteral lit) {
-  if (lit == undefSatLiteral) {
-    return Minisat::lit_Undef;
-  }
-  return Minisat::mkLit(lit.getSatVariable(), lit.isNegated()); 
-}
-
-SatLiteral DPLLMinisatSatSolver::toSatLiteral(Minisat::Lit lit) {
-  if (lit == Minisat::lit_Undef) {
-    return undefSatLiteral; 
-  }
-  
-  return SatLiteral(SatVariable(Minisat::var(lit)),
-                    Minisat::sign(lit)); 
-}
-
-SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(bool res) {
-  if(res) return SatValTrue;
-  else return SatValFalse; 
-}
-
-SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(Minisat::lbool res) {
-  if(res == (Minisat::lbool((uint8_t)0))) return SatValTrue;
-  if(res == (Minisat::lbool((uint8_t)2))) return SatValUnknown;
-  Assert(res == (Minisat::lbool((uint8_t)1)));
-  return SatValFalse; 
-}
-
-
-void DPLLMinisatSatSolver::toMinisatClause(SatClause& clause,
-                                           Minisat::vec<Minisat::Lit>& minisat_clause) {
-  for (unsigned i = 0; i < clause.size(); ++i) {
-    minisat_clause.push(toMinisatLit(clause[i])); 
-  }
-  Assert(clause.size() == (unsigned)minisat_clause.size()); 
-}
-
-void DPLLMinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause,
-                                       SatClause& sat_clause) {
-  for (int i = 0; i < clause.size(); ++i) {
-    sat_clause.push_back(toSatLiteral(clause[i])); 
-  }
-  Assert((unsigned)clause.size() == sat_clause.size()); 
-}
-
-
-void DPLLMinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy)
-{
-
-  d_context = context;
-  
-  // Create the solver
-  d_minisat = new Minisat::SimpSolver(theoryProxy, d_context,
-                                      options::incrementalSolving());
-  // Setup the verbosity
-  d_minisat->verbosity = (options::verbosity() > 0) ? 1 : -1;
-
-  // Setup the random decision parameters
-  d_minisat->random_var_freq = options::satRandomFreq();
-  d_minisat->random_seed = options::satRandomSeed();
-  // Give access to all possible options in the sat solver
-  d_minisat->var_decay = options::satVarDecay();
-  d_minisat->clause_decay = options::satClauseDecay();
-  d_minisat->restart_first = options::satRestartFirst();
-  d_minisat->restart_inc = options::satRestartInc();
-
-  d_statistics.init(d_minisat);
-}
-
-void DPLLMinisatSatSolver::addClause(SatClause& clause, bool removable) {
-  Minisat::vec<Minisat::Lit> minisat_clause;
-  toMinisatClause(clause, minisat_clause); 
-  d_minisat->addClause(minisat_clause, removable);
-}
-
-SatVariable DPLLMinisatSatSolver::newVar(bool theoryAtom) {
-  return d_minisat->newVar(true, true, theoryAtom);
-}
-
-  
-SatLiteralValue DPLLMinisatSatSolver::solve(unsigned long& resource) {
-  Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
-  if(resource == 0) {
-    d_minisat->budgetOff();
-  } else {
-    d_minisat->setConfBudget(resource);
-  }
-  Minisat::vec<Minisat::Lit> empty;
-  unsigned long conflictsBefore = d_minisat->conflicts;
-  SatLiteralValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
-  d_minisat->clearInterrupt();
-  resource = d_minisat->conflicts - conflictsBefore;
-  Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl;
-  return result;
-}
-
-SatLiteralValue DPLLMinisatSatSolver::solve() {
-  d_minisat->budgetOff();
-  return toSatLiteralValue(d_minisat->solve()); 
-}
-
-
-void DPLLMinisatSatSolver::interrupt() {
-  d_minisat->interrupt();
-}
-
-SatLiteralValue DPLLMinisatSatSolver::value(SatLiteral l) {
-  return toSatLiteralValue(d_minisat->value(toMinisatLit(l)));
-}
-
-SatLiteralValue DPLLMinisatSatSolver::modelValue(SatLiteral l){
-  return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
-}
-
-bool DPLLMinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const {
-  return true;
-}
-
-/** Incremental interface */ 
-  
-int DPLLMinisatSatSolver::getAssertionLevel() const {
-  return d_minisat->getAssertionLevel(); 
-}
-  
-void DPLLMinisatSatSolver::push() {
-  d_minisat->push();
-}
-
-void DPLLMinisatSatSolver::pop(){
-  d_minisat->pop();
-}
-
-void DPLLMinisatSatSolver::unregisterVar(SatLiteral lit) {
-  d_minisat->unregisterVar(toMinisatLit(lit));
-}
-
-void DPLLMinisatSatSolver::renewVar(SatLiteral lit, int level) {
-  d_minisat->renewVar(toMinisatLit(lit), level);
-}
-
-/// Statistics for DPLLMinisatSatSolver
-
-DPLLMinisatSatSolver::Statistics::Statistics() :
-  d_statStarts("sat::starts"),
-  d_statDecisions("sat::decisions"),
-  d_statRndDecisions("sat::rnd_decisions"),
-  d_statPropagations("sat::propagations"),
-  d_statConflicts("sat::conflicts"),
-  d_statClausesLiterals("sat::clauses_literals"),
-  d_statLearntsLiterals("sat::learnts_literals"),
-  d_statMaxLiterals("sat::max_literals"),
-  d_statTotLiterals("sat::tot_literals")
-{
-  StatisticsRegistry::registerStat(&d_statStarts);
-  StatisticsRegistry::registerStat(&d_statDecisions);
-  StatisticsRegistry::registerStat(&d_statRndDecisions);
-  StatisticsRegistry::registerStat(&d_statPropagations);
-  StatisticsRegistry::registerStat(&d_statConflicts);
-  StatisticsRegistry::registerStat(&d_statClausesLiterals);
-  StatisticsRegistry::registerStat(&d_statLearntsLiterals);
-  StatisticsRegistry::registerStat(&d_statMaxLiterals);
-  StatisticsRegistry::registerStat(&d_statTotLiterals);
-}
-DPLLMinisatSatSolver::Statistics::~Statistics() {
-  StatisticsRegistry::unregisterStat(&d_statStarts);
-  StatisticsRegistry::unregisterStat(&d_statDecisions);
-  StatisticsRegistry::unregisterStat(&d_statRndDecisions);
-  StatisticsRegistry::unregisterStat(&d_statPropagations);
-  StatisticsRegistry::unregisterStat(&d_statConflicts);
-  StatisticsRegistry::unregisterStat(&d_statClausesLiterals);
-  StatisticsRegistry::unregisterStat(&d_statLearntsLiterals);
-  StatisticsRegistry::unregisterStat(&d_statMaxLiterals);
-  StatisticsRegistry::unregisterStat(&d_statTotLiterals);
-}
-void DPLLMinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){
-  d_statStarts.setData(d_minisat->starts);
-  d_statDecisions.setData(d_minisat->decisions);
-  d_statRndDecisions.setData(d_minisat->rnd_decisions);
-  d_statPropagations.setData(d_minisat->propagations);
-  d_statConflicts.setData(d_minisat->conflicts);
-  d_statClausesLiterals.setData(d_minisat->clauses_literals);
-  d_statLearntsLiterals.setData(d_minisat->learnts_literals);
-  d_statMaxLiterals.setData(d_minisat->max_literals);
-  d_statTotLiterals.setData(d_minisat->tot_literals);
-}
-
-
-/*
-  
-  SatSolverFactory
-  
- */
-
-MinisatSatSolver* SatSolverFactory::createMinisat() {
-  return new MinisatSatSolver(); 
-}
-
-DPLLMinisatSatSolver* SatSolverFactory::createDPLLMinisat(){
-  return new DPLLMinisatSatSolver(); 
-} 
-
-
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index d2e967393..567f897a1 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -18,8 +18,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROP__SAT_MODULE_H
-#define __CVC4__PROP__SAT_MODULE_H
+#ifndef __CVC4__PROP__SAT_SOLVER_H
+#define __CVC4__PROP__SAT_SOLVER_H
 
 #include <string>
 #include <stdint.h>
@@ -30,21 +30,21 @@
 namespace CVC4 {
 namespace prop {
 
-class TheoryProxy; 
+class TheoryProxy;
 
 class SatSolver {
 
-public:  
+public:
 
   /** Virtual destructor */
   virtual ~SatSolver() { }
-  
+
   /** Assert a clause in the solver. */
   virtual void addClause(SatClause& clause, bool removable) = 0;
 
   /** Create a new boolean variable in the solver. */
   virtual SatVariable newVar(bool theoryAtom = false) = 0;
- 
+
   /** Create a new (or return an existing) boolean variable representing the constant true */
   virtual SatVariable trueVar() = 0;
 
@@ -56,7 +56,7 @@ public:
 
   /** Check the satisfiability of the added clauses */
   virtual SatValue solve(long unsigned int&) = 0;
-  
+
   /** Interrupt the solver */
   virtual void interrupt() = 0;
 
@@ -67,12 +67,12 @@ public:
   virtual SatValue modelValue(SatLiteral l) = 0;
 
   virtual void unregisterVar(SatLiteral lit) = 0;
-  
+
   virtual void renewVar(SatLiteral lit, int level = -1) = 0;
 
   virtual unsigned getAssertionLevel() const = 0;
 
-};
+};/* class SatSolver */
 
 
 class BVSatSolverInterface: public SatSolver {
@@ -94,30 +94,31 @@ public:
      * Notify about a learnt clause.
      */
     virtual void notify(SatClause& clause) = 0;
-  };
+  };/* class BVSatSolverInterface::Notify */
+
+  virtual void setNotify(Notify* notify) = 0;
 
-  virtual void setNotify(Notify* notify) = 0; 
-  
   virtual void markUnremovable(SatLiteral lit) = 0;
 
-  virtual void getUnsatCore(SatClause& unsatCore) = 0; 
+  virtual void getUnsatCore(SatClause& unsatCore) = 0;
 
-  virtual void addMarkerLiteral(SatLiteral lit) = 0; 
+  virtual void addMarkerLiteral(SatLiteral lit) = 0;
 
   virtual SatValue propagate() = 0;
 
   virtual void explain(SatLiteral lit, std::vector<SatLiteral>& explanation) = 0;
 
-  virtual SatValue assertAssumption(SatLiteral lit, bool propagate = false) = 0; 
+  virtual SatValue assertAssumption(SatLiteral lit, bool propagate = false) = 0;
 
   virtual void popAssumption() = 0;
-}; 
+
+};/* class BVSatSolverInterface */
 
 
 class DPLLSatSolverInterface: public SatSolver {
 public:
-  virtual void initialize(context::Context* context, prop::TheoryProxy* theoryProxy) = 0; 
-  
+  virtual void initialize(context::Context* context, prop::TheoryProxy* theoryProxy) = 0;
+
   virtual void push() = 0;
 
   virtual void pop() = 0;
@@ -130,9 +131,9 @@ public:
 
   virtual bool isDecision(SatVariable decn) const = 0;
 
-}; 
+};/* class DPLLSatSolverInterface */
 
-}/* prop namespace */
+}/* CVC4::prop namespace */
 
 inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
   out << lit.toString();
diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp
index 1af029f17..deec881e4 100644
--- a/src/smt/smt_options_template.cpp
+++ b/src/smt/smt_options_template.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file smt_options_template.cpp
+/*! \file smt_options.cpp
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index 8cfdab5af..80b689b8c 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -100,7 +100,7 @@ void inline makeZero(Bits& bits, unsigned width) {
  * 
  * @param a first term to be added
  * @param b second term to be added
- * @param sum the sum 
+ * @param res the result
  * @param carry the carry-in bit 
  * 
  * @return the carry-out
diff --git a/src/theory/bv/bitblast_strategies.h b/src/theory/bv/bitblast_strategies.h
index 826b61d4f..5b53678dd 100644
--- a/src/theory/bv/bitblast_strategies.h
+++ b/src/theory/bv/bitblast_strategies.h
@@ -41,7 +41,6 @@ typedef std::vector<Node>    Bits;
  * Default Atom Bitblasting strategies: 
  * 
  * @param node the atom to be bitblasted
- * @param markerLit the marker literal corresponding to the atom
  * @param bb the bitblaster
  */
 
@@ -68,9 +67,8 @@ Node SleBB(TNode node, Bitblaster* bb);
  * Default Term Bitblasting strategies
  * 
  * @param node the term to be bitblasted
+ * @param bits [output parameter] bits representing the new term 
  * @param bb the bitblaster in which the clauses are added
- * 
- * @return the bits representing the new term 
  */
 
 void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb); 
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index c86f14398..eb5f3e155 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -170,7 +170,7 @@ void Bitblaster::explain(TNode atom, std::vector<TNode>& explanation) {
 /** 
  * Asserts the clauses corresponding to the atom to the Sat Solver
  * by turning on the marker literal (i.e. setting it to false)
- * @param node the atom to be aserted
+ * @param node the atom to be asserted
  * 
  */
  
diff --git a/src/theory/instantiator_tables_template.cpp b/src/theory/instantiator_tables_template.cpp
index 7a78c3aae..7234993fa 100644
--- a/src/theory/instantiator_tables_template.cpp
+++ b/src/theory/instantiator_tables_template.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file instantiator_tables_template.cpp
+/*! \file instantiator_tables.cpp
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h
index 9ab98168e..6533e9335 100644
--- a/src/theory/rewriter_tables_template.h
+++ b/src/theory/rewriter_tables_template.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file rewriter_tables_template.h
+/*! \file rewriter_tables.h
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: mdeters
diff --git a/src/theory/theory_traits_template.h b/src/theory/theory_traits_template.h
index bbf13b425..4522af568 100644
--- a/src/theory/theory_traits_template.h
+++ b/src/theory/theory_traits_template.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file theory_traits_template.h
+/*! \file theory_traits.h
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: mdeters
@@ -27,7 +27,6 @@
 ${theory_includes}
 
 namespace CVC4 {
-
 namespace theory {
 
 template <TheoryId theoryId>
@@ -37,5 +36,5 @@ ${theory_traits}
 
 ${theory_for_each_macro}
 
-}/* theory namespace */
+}/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/type_enumerator_template.cpp b/src/theory/type_enumerator_template.cpp
index 426bf52a0..0619a900f 100644
--- a/src/theory/type_enumerator_template.cpp
+++ b/src/theory/type_enumerator_template.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file type_enumerator_template.cpp
+/*! \file type_enumerator.cpp
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
@@ -58,4 +58,3 @@ ${mk_type_enumerator_cases}
 
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
-
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 7f216d634..1e3b276a4 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -58,7 +58,7 @@ public:
   /**
    * Notifies about a trigger equality that became true or false.
    *
-   * @param eq the equality that became true or false
+   * @param equality the equality that became true or false
    * @param value the value of the equality
    */
   virtual bool eqNotifyTriggerEquality(TNode equality, bool value) = 0;
@@ -680,13 +680,13 @@ public:
 
   /**
    * Adds a predicate p with given polarity. The predicate asserted
-   * should be in the congruence closure kinds (otherwise it's 
+   * should be in the congruence closure kinds (otherwise it's
    * useless.
    *
    * @param p the (non-negated) predicate
-   * @param polarity true if asserting the predicate, false if 
+   * @param polarity true if asserting the predicate, false if
    *                 asserting the negated predicate
-   * @param the reason to keep for building explanations
+   * @param reason the reason to keep for building explanations
    */
   void assertPredicate(TNode p, bool polarity, TNode reason);
 
@@ -694,9 +694,9 @@ public:
    * Adds an equality eq with the given polarity to the database.
    *
    * @param eq the (non-negated) equality
-   * @param polarity true if asserting the equality, false if 
+   * @param polarity true if asserting the equality, false if
    *                 asserting the negated equality
-   * @param the reason to keep for building explanations
+   * @param reason the reason to keep for building explanations
    */
   void assertEquality(TNode eq, bool polarity, TNode reason);
 
@@ -706,20 +706,20 @@ public:
   TNode getRepresentative(TNode t) const;
 
   /**
-   * Add all the terms where the given term appears as a first child 
+   * Add all the terms where the given term appears as a first child
    * (directly or implicitly).
    */
   void getUseListTerms(TNode t, std::set<TNode>& output);
 
   /**
-   * Get an explanation of the equality t1 = t2 begin true of false. 
+   * Get an explanation of the equality t1 = t2 begin true of false.
    * Returns the reasons (added when asserting) that imply it
    * in the assertions vector.
    */
   void explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& assertions) const;
 
   /**
-   * Get an explanation of the predicate being true or false. 
+   * Get an explanation of the predicate being true or false.
    * Returns the reasons (added when asserting) that imply imply it
    * in the assertions vector.
    */
@@ -733,12 +733,12 @@ public:
    * it's own notification.
    *
    * @param t the trigger term
-   * @param tag tag for this trigger (do NOT use THEORY_LAST)
+   * @param theoryTag tag for this trigger (do NOT use THEORY_LAST)
    */
   void addTriggerTerm(TNode t, TheoryId theoryTag);
 
   /**
-   * Returns true if t is a trigger term or in the same equivalence 
+   * Returns true if t is a trigger term or in the same equivalence
    * class as some other trigger term.
    */
   bool isTriggerTerm(TNode t, TheoryId theoryTag) const;
diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index 30bdea78d..81a291006 100644
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -165,7 +165,7 @@ public:
   /**
    * Returns true iff this cardinality is finite and large (i.e.,
    * at the ceiling of representable finite cardinalities).
- . */
+   */
   bool isLargeFinite() const throw() {
     return d_card >= s_largeFiniteCard;
   }
diff --git a/src/util/integer.h.in b/src/util/integer.h.in
index b2973081d..1fdaf0215 100644
--- a/src/util/integer.h.in
+++ b/src/util/integer.h.in
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file integer.h.in
+/*! \file integer.h
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
diff --git a/src/util/rational.h.in b/src/util/rational.h.in
index 17c1e31fc..f97559377 100644
--- a/src/util/rational.h.in
+++ b/src/util/rational.h.in
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file rational.h.in
+/*! \file rational.h
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
diff --git a/src/util/tls.h.in b/src/util/tls.h.in
index df53cae36..cd89be9d0 100644
--- a/src/util/tls.h.in
+++ b/src/util/tls.h.in
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file tls.h.in
+/*! \file tls.h
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none