Documentation fixes, some code typo fixes, file perms, other minor things.

29 files changed, 182 insertions, 27 deletions

diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h
index 175e56f8e..a34c8981d 100644
--- a/src/theory/arith/approx_simplex.h
+++ b/src/theory/arith/approx_simplex.h
@@ -24,7 +24,7 @@ public:
 
   /**
    * If glpk is enabled, return a subclass that can do something.
-   * If glpk is disabled, return a sublass that does nothing.
+   * If glpk is disabled, return a subclass that does nothing.
    */
   static ApproximateSimplex* mkApproximateSimplexSolver(const ArithVariables& vars);
   ApproximateSimplex();
@@ -52,7 +52,7 @@ public:
   virtual ApproxResult solveMIP() = 0;
   virtual Solution extractMIP() const = 0;
 
-  /** UTILIES FOR DEALING WITH ESTIMATES */
+  /** UTILITIES FOR DEALING WITH ESTIMATES */
 
   static const double SMALL_FIXED_DELTA;
   static const double TOLERENCE;
diff --git a/src/theory/arith/bound_counts.h b/src/theory/arith/bound_counts.h
index 1ee6ada06..49c1a94ce 100644
--- a/src/theory/arith/bound_counts.h
+++ b/src/theory/arith/bound_counts.h
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file bound_counts.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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"
 #pragma once
 
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index 1ebbe49e0..7cd202e53 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -22,7 +22,7 @@
 using namespace std;
 
 namespace CVC4 {
-namespace theory{
+namespace theory {
 namespace arith {
 
 bool Variable::isDivMember(Node n){
diff --git a/src/theory/arith/options b/src/theory/arith/options
index 57ef3d1b9..43b582bc8 100644
--- a/src/theory/arith/options
+++ b/src/theory/arith/options
@@ -56,7 +56,7 @@ option arithMLTrick miplib-trick --enable-miplib-trick/--disable-miplib-trick bo
  turns on the preprocessing step of attempting to infer bounds on miplib problems
 /turns off the preprocessing step of attempting to infer bounds on miplib problems
 
-option arithMLTrickSubstitutions miplib-trick-subs --miplib-trick-subs unsigned :default 1
+option arithMLTrickSubstitutions miplib-trick-subs --miplib-trick-subs=N unsigned :default 1
  do substitution for miplib 'tmp' vars if defined in <= N eliminated vars
 
 option doCutAllBounded --cut-all-bounded bool :default false :read-write
@@ -67,11 +67,11 @@ option maxCutsInContext --maxCutsInContext unsigned :default 65535
  maximum cuts in a given context before signalling a restart
 
 option revertArithModels --revert-arith-models-on-unsat bool :default false
- Revert the arithmetic model to a known safe model on unsat if one is cached
+ revert the arithmetic model to a known safe model on unsat if one is cached
 
 option havePenalties --fc-penalties bool :default false :read-write
  turns on degenerate pivot penalties
-/ turns off degenerate pivot penalties
+/turns off degenerate pivot penalties
 
 option useFC --use-fcsimplex bool :default false :read-write
  use focusing and converging simplex (FMCAD 2013 submission)
@@ -80,25 +80,25 @@ option useSOI --use-soi bool :default false :read-write
  use sum of infeasibility simplex (FMCAD 2013 submission)
 
 option restrictedPivots --restrict-pivots bool :default true :read-write
- have a pivot cap for simplex at effort levels below fullEffort.
+ have a pivot cap for simplex at effort levels below fullEffort
 
 option collectPivots --collect-pivot-stats bool :default false :read-write
  collect the pivot history
 
 option fancyFinal --fancy-final bool :default false :read-write
- Tuning how final check works for really hard problems.
+ tuning how final check works for really hard problems
 
 option exportDioDecompositions --dio-decomps bool :default false :read-write
- Let skolem variables for integer divisibility constraints leak from the dio solver.
+ let skolem variables for integer divisibility constraints leak from the dio solver
 
 option newProp --new-prop bool :default false :read-write
- Use the new row propagation system
+ use the new row propagation system
 
 option arithPropAsLemmaLength --arith-prop-clauses uint16_t :default 8 :read-write
- Rows shorter than this are propagated as clauses
+ rows shorter than this are propagated as clauses
 
 option soiQuickExplain --soi-qe bool :default false :read-write
- Use quick explain to minimize the sum of infeasibility conflicts.
+ use quick explain to minimize the sum of infeasibility conflicts
 
 option rewriteDivk rewrite-divk --rewrite-divk bool :default false
  rewrite division and mod when by a constant into linear terms
diff --git a/src/theory/arith/simplex_update.h b/src/theory/arith/simplex_update.h
index 516586568..64aa193dd 100644
--- a/src/theory/arith/simplex_update.h
+++ b/src/theory/arith/simplex_update.h
@@ -318,7 +318,7 @@ private:
   }
 
   /**
-   * Determines the appropraite WitnessImprovement for the update.
+   * Determines the appropriate WitnessImprovement for the update.
    * useBlands breaks ties for degenerate pivots.
    *
    * This is safe if:
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 5847bac3e..ab6a615a2 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -357,7 +357,7 @@ inline Node flattenAnd(std::vector<TNode>& queue) {
 }
 
 
-// neeed a better name, this is not technically a ground term 
+// need a better name, this is not technically a ground term 
 inline bool isBVGroundTerm(TNode node) {
   if (node.getNumChildren() == 0) {
     return node.isConst(); 
diff --git a/src/theory/idl/idl_assertion.cpp b/src/theory/idl/idl_assertion.cpp
index 861dd0a46..1e725932b 100644
--- a/src/theory/idl/idl_assertion.cpp
+++ b/src/theory/idl/idl_assertion.cpp
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file idl_assertion.cpp
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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/idl/idl_assertion.h"
 
 using namespace CVC4;
diff --git a/src/theory/idl/idl_assertion.h b/src/theory/idl/idl_assertion.h
index 2ed5a6bef..8ce0e93b2 100644
--- a/src/theory/idl/idl_assertion.h
+++ b/src/theory/idl/idl_assertion.h
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file idl_assertion.h
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
 #pragma once
 
 #include "theory/idl/idl_model.h"
diff --git a/src/theory/idl/idl_assertion_db.cpp b/src/theory/idl/idl_assertion_db.cpp
index 7c27e9d0d..697c70c02 100644
--- a/src/theory/idl/idl_assertion_db.cpp
+++ b/src/theory/idl/idl_assertion_db.cpp
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file idl_assertion_db.cpp
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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/idl/idl_assertion_db.h"
 
 using namespace CVC4;
diff --git a/src/theory/idl/idl_assertion_db.h b/src/theory/idl/idl_assertion_db.h
index 3972819da..0501bc6bf 100644
--- a/src/theory/idl/idl_assertion_db.h
+++ b/src/theory/idl/idl_assertion_db.h
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file idl_assertion_db.h
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
 #pragma once
 
 #include "theory/idl/idl_assertion.h"
diff --git a/src/theory/idl/idl_model.cpp b/src/theory/idl/idl_model.cpp
index 2feabd700..75f4834ea 100644
--- a/src/theory/idl/idl_model.cpp
+++ b/src/theory/idl/idl_model.cpp
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file idl_model.cpp
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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/idl/idl_model.h"
 
 using namespace CVC4;
diff --git a/src/theory/idl/idl_model.h b/src/theory/idl/idl_model.h
index a1840a35a..64407684b 100644
--- a/src/theory/idl/idl_model.h
+++ b/src/theory/idl/idl_model.h
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file idl_model.h
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
 #pragma once
 
 #include "expr/node.h"
diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp
index bf2297d3d..e5100fc71 100644
--- a/src/theory/idl/theory_idl.cpp
+++ b/src/theory/idl/theory_idl.cpp
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file theory_idl.cpp
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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/idl/theory_idl.h"
 #include "theory/idl/options.h"
 #include "theory/rewriter.h"
diff --git a/src/theory/idl/theory_idl.h b/src/theory/idl/theory_idl.h
index 25b992981..c629ad2b0 100644
--- a/src/theory/idl/theory_idl.h
+++ b/src/theory/idl/theory_idl.h
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file theory_idl.h
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
 #pragma once
 
 #include "cvc4_private.h"
diff --git a/src/theory/ite_simplifier.cpp b/src/theory/ite_simplifier.cpp
index ec9eb27d4..463a9c41a 100644
--- a/src/theory/ite_simplifier.cpp
+++ b/src/theory/ite_simplifier.cpp
@@ -33,7 +33,7 @@ bool ITESimplifier::containsTermITE(TNode e)
   }
 
   hash_map<Node, bool, NodeHashFunction>::iterator it;
-  it = d_containsTermITECache.find(e); 
+  it = d_containsTermITECache.find(e);
   if (it != d_containsTermITECache.end()) {
     return (*it).second;
   }
@@ -60,7 +60,7 @@ bool ITESimplifier::leavesAreConst(TNode e, TheoryId tid)
   }
 
   hash_map<Node, bool, NodeHashFunction>::iterator it;
-  it = d_leavesConstCache.find(e); 
+  it = d_leavesConstCache.find(e);
   if (it != d_leavesConstCache.end()) {
     return (*it).second;
   }
diff --git a/src/theory/ite_simplifier.h b/src/theory/ite_simplifier.h
index 0f648f91d..2329cd970 100644
--- a/src/theory/ite_simplifier.h
+++ b/src/theory/ite_simplifier.h
@@ -43,6 +43,7 @@
 #include "util/ite_removal.h"
 
 namespace CVC4 {
+namespace theory {
 
 class ITESimplifier {
   Node d_true;
@@ -160,6 +161,7 @@ public:
 
 };
 
-}
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
 #endif
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 524c9606d..44b89e8cb 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -222,7 +222,7 @@ public:
 
   /** Demands that the search restart from sat search level 0.
    * Using this leads to non-termination issues.
-   * It is appropraite for prototyping for theories.
+   * It is appropriate for prototyping for theories.
    */
   virtual void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException) {}
 
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 13e075265..13e075265 100755..100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index 27d5b7569..27d5b7569 100755..100644
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
diff --git a/src/theory/quantifiers/first_order_reasoning.cpp b/src/theory/quantifiers/first_order_reasoning.cpp
index ebfb55f08..ebfb55f08 100755..100644
--- a/src/theory/quantifiers/first_order_reasoning.cpp
+++ b/src/theory/quantifiers/first_order_reasoning.cpp
diff --git a/src/theory/quantifiers/first_order_reasoning.h b/src/theory/quantifiers/first_order_reasoning.h
index 5f217050c..5f217050c 100755..100644
--- a/src/theory/quantifiers/first_order_reasoning.h
+++ b/src/theory/quantifiers/first_order_reasoning.h
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index a0b195a9c..a0b195a9c 100755..100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 6bb375c34..6bb375c34 100755..100644
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index 686a2cc13..1c2c38c51 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -56,7 +56,7 @@ public:
   //get relevant domain
   RelevantDomain * getRelevantDomain() { return d_rel_dom; }
   //get the builder
-  QModelBuilder * getModelBuilder() { return d_builder; }
+  QModelBuilder* getModelBuilder() { return d_builder; }
 public:
   void check( Theory::Effort e );
   void registerQuantifier( Node f );
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 9ed20cc99..3e30645e8 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -72,7 +72,7 @@ TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) {
     // Variables
     if (node.isVar()) {
       if (theoryOf(node.getType()) != theory::THEORY_BOOL) {
-        // We treat the varibables as uninterpreted
+        // We treat the variables as uninterpreted
         return s_uninterpretedSortOwner;
       } else {
         // Except for the Boolean ones, which we just ignore anyhow
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 23fd67b23..6b1974bb8 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -516,7 +516,7 @@ public:
   virtual EqualityStatus getEqualityStatus(TNode a, TNode b) { return EQUALITY_UNKNOWN; }
 
   /**
-   * Return the model value of the give shared term (or null if not avalilable.
+   * Return the model value of the give shared term (or null if not available).
    */
   virtual Node getModelValue(TNode var) { return Node::null(); }
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f6616920a..448e3a8fa 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -212,7 +212,7 @@ void TheoryEngine::preRegister(TNode preprocessed) {
         }
       }
       if (multipleTheories) {
-        // Collect the shared terms if there are multipe theories
+        // Collect the shared terms if there are multiple theories
         NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed);
       }
     }
@@ -1317,7 +1317,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable
   d_iteRemover.run(additionalLemmas, iteSkolemMap);
   additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]);
 
-  if(Trace.isOn("lemma-ites")) {
+  if(Debug.isOn("lemma-ites")) {
     Debug("lemma-ites") << "removed ITEs from lemma: " << node << endl;
     Debug("lemma-ites") << " + now have the following "
                         << additionalLemmas.size() << " lemma(s):" << endl;
@@ -1417,7 +1417,7 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
 
     Debug("theory::explain") << "TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl;
 
-    // If a treu constant or a negation of a false constant we can ignore it
+    // If a true constant or a negation of a false constant we can ignore it
     if (toExplain.node.isConst() && toExplain.node.getConst<bool>()) {
       ++ i;
       continue;
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 97b018214..fcbec2a41 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -773,7 +773,7 @@ private:
   void dumpAssertions(const char* tag);
 
   /** For preprocessing pass simplifying ITEs */
-  ITESimplifier d_iteSimplifier;
+  theory::ITESimplifier d_iteSimplifier;
 
   /** For preprocessing pass simplifying unconstrained expressions */
   UnconstrainedSimplifier d_unconstrainedSimp;
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 6962f0c69..8d1b6f1d9 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -741,7 +741,7 @@ public:
   /**
    * Adds a predicate p with given polarity. The predicate asserted
    * should be in the congruence closure kinds (otherwise it's
-   * useless.
+   * useless).
    *
    * @param p the (non-negated) predicate
    * @param polarity true if asserting the predicate, false if
@@ -777,7 +777,7 @@ public:
   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 being true or false.
    * Returns the reasons (added when asserting) that imply it
    * in the assertions vector.
    */