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

5 files changed, 30 insertions, 13 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: