Minor code cleanup.

8 files changed, 16 insertions, 17 deletions

diff --git a/src/theory/arith/options_handlers.h b/src/theory/arith/options_handlers.h
index a72ced0bc..f81f1b227 100644
--- a/src/theory/arith/options_handlers.h
+++ b/src/theory/arith/options_handlers.h
@@ -52,7 +52,7 @@ This decides on kind of propagation arithmetic attempts to do during the search.
 ";
 
 static const std::string errorSelectionRulesHelp = "\
-This decides on the rule used by simplex during hueristic rounds\n\
+This decides on the rule used by simplex during heuristic rounds\n\
 for deciding the next basic variable to select.\n\
 Heuristic pivot rules available:\n\
 +min\n\
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 5140bd498..f35fc2896 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -25,7 +25,6 @@
 #include "expr/node_manager.h"
 #include "theory/decision_attributes.h"
 
-
 namespace CVC4 {
 namespace theory {
 namespace bv {
diff --git a/src/theory/idl/idl_assertion_db.h b/src/theory/idl/idl_assertion_db.h
index 205102b0f..358a5386e 100644
--- a/src/theory/idl/idl_assertion_db.h
+++ b/src/theory/idl/idl_assertion_db.h
@@ -35,7 +35,7 @@ class IDLAssertionDB {
   struct IDLAssertionListElement {
     /** The assertion itself */
     IDLAssertion d_assertion;
-    /** The inndex of the previous element (-1 for null) */
+    /** The index of the previous element (-1 for null) */
     unsigned d_previous;
 
     IDLAssertionListElement(const IDLAssertion& assertion, unsigned previous)
diff --git a/src/theory/idl/idl_model.h b/src/theory/idl/idl_model.h
index 22e05c469..c69a0c38f 100644
--- a/src/theory/idl/idl_model.h
+++ b/src/theory/idl/idl_model.h
@@ -33,7 +33,7 @@ namespace idl {
 struct IDLReason {
   /** The variable of the reason */
   TNode x;
-  /** The constraint of the reaason */
+  /** The constraint of the reason */
   TNode constraint;
 
   IDLReason(TNode x, TNode constraint)
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index a47f7bd77..9ed4be0c3 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -9,9 +9,9 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Regular Expresion Operations

+ ** \brief Regular Expression Operations

  **

- ** Regular Expresion Operations

+ ** Regular Expression Operations

  **/

 

 #include "cvc4_private.h"

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 9f4d84765..62e71327e 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -218,7 +218,7 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
 	std::map< Node, Node > processed;
 	std::vector< std::vector< Node > > col;
 	std::vector< Node > lts;
-	seperateByLength( nodes, col, lts );
+	separateByLength( nodes, col, lts );
 	//step 1 : get all values for known lengths
 	std::vector< Node > lts_values;
 	std::map< unsigned, bool > values_used;
@@ -1667,7 +1667,7 @@ bool TheoryStrings::checkNormalForms() {
 	  getEquivalenceClasses( eqcs );
 	  std::vector< std::vector< Node > > cols;
 	  std::vector< Node > lts;
-	  seperateByLength( eqcs, cols, lts );
+	  separateByLength( eqcs, cols, lts );
 	  for( unsigned i=0; i<cols.size(); i++ ){
 	    if( cols[i].size()>1 && d_lemma_cache.empty() ){
 			Trace("strings-solve") << "- Verify disequalities are processed for ";
@@ -1745,7 +1745,7 @@ bool TheoryStrings::checkCardinality() {
 
   std::vector< std::vector< Node > > cols;
   std::vector< Node > lts;
-  seperateByLength( eqcs, cols, lts );
+  separateByLength( eqcs, cols, lts );
 
   for( unsigned i = 0; i<cols.size(); ++i ){
     Node lr = lts[i];
@@ -1862,7 +1862,7 @@ void TheoryStrings::getFinalNormalForm( Node n, std::vector< Node >& nf, std::ve
 	}
 }
 
-void TheoryStrings::seperateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& cols,
+void TheoryStrings::separateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& cols,
 											 std::vector< Node >& lts ) {
   unsigned leqc_counter = 0;
   std::map< Node, unsigned > eqc_to_leqc;
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 4d2a192cf..875f407c5 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -188,7 +188,7 @@ private:
 	/** map from representatives to information necessary for equivalence classes */
 	std::map< Node, EqcInfo* > d_eqc_info;
 	EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true );
-	//maintain which concat terms have the length lemma instantiatied
+	//maintain which concat terms have the length lemma instantiated
 	std::map< Node, bool > d_length_inst;
 private:
     bool getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
@@ -223,11 +223,11 @@ public:
 
 	/** Conflict when merging two constants */
 	void conflict(TNode a, TNode b);
-	/** called when a new equivalance class is created */
+	/** called when a new equivalence class is created */
 	void eqNotifyNewClass(TNode t);
-	/** called when two equivalance classes will merge */
+	/** called when two equivalence classes will merge */
 	void eqNotifyPreMerge(TNode t1, TNode t2);
-	/** called when two equivalance classes have merged */
+	/** called when two equivalence classes have merged */
 	void eqNotifyPostMerge(TNode t1, TNode t2);
 	/** called when two equivalence classes are made disequal */
 	void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
@@ -255,8 +255,8 @@ protected:
 	//get final normal form
 	void getFinalNormalForm( Node n, std::vector< Node >& nf, std::vector< Node >& exp );
 
-	//seperate into collections with equal length
-	void seperateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& col, std::vector< Node >& lts );
+	//separate into collections with equal length
+	void separateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& col, std::vector< Node >& lts );
 	void printConcat( std::vector< Node >& n, const char * c );
 
 	// Measurement
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index ffc36e59b..92469aa31 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -749,7 +749,7 @@ public:
   theory::EqualityStatus getEqualityStatus(TNode a, TNode b);
 
   /**
-   * Retruns the value that a theory that owns the type of var currently
+   * Returns the value that a theory that owns the type of var currently
    * has (or null if none);
    */
   Node getModelValue(TNode var);