Minor code cleanup.

16 files changed, 25 insertions, 32 deletions

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 78de1a74e..54d2dee97 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -106,7 +106,7 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNextThresh(bool &stopSearch, D
 
     if(litDecision != undefSatLiteral) {
       setPrvsIndex(i);
-      Trace("decision") << "jh: spliting on " << litDecision << std::endl;
+      Trace("decision") << "jh: splitting on " << litDecision << std::endl;
       return litDecision;
     }
   }
diff --git a/src/decision/options_handlers.h b/src/decision/options_handlers.h
index f538ba947..a8931aecb 100644
--- a/src/decision/options_handlers.h
+++ b/src/decision/options_handlers.h
@@ -29,7 +29,7 @@ static const std::string decisionModeHelp = "\
 Decision modes currently supported by the --decision option:\n\
 \n\
 internal (default)\n\
-+ Use the internal decision hueristics of the SAT solver\n\
++ Use the internal decision heuristics of the SAT solver\n\
 \n\
 justification\n\
 + An ATGP-inspired justification heuristic\n\
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index 86768500b..cde261463 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -128,7 +128,7 @@ void AttributeManager::deleteAttributes(const AttrIdVec& atids){
     case AttrTableCDNode:
     case AttrTableCDString:
     case AttrTableCDPointer:
-      Unimplemented("CDAttributes cannot be deleted. Contact Tim/Morgan if this behaviour is desired.");
+      Unimplemented("CDAttributes cannot be deleted. Contact Tim/Morgan if this behavior is desired.");
       break;
     case LastAttrTable:
     default:
diff --git a/src/expr/attribute_unique_id.h b/src/expr/attribute_unique_id.h
index 08b31a4c0..3a52d7a89 100644
--- a/src/expr/attribute_unique_id.h
+++ b/src/expr/attribute_unique_id.h
@@ -46,7 +46,7 @@ enum AttrTableId {
 };
 
 /**
- * This uniquely indentifies attributes across tables.
+ * This uniquely identifies attributes across tables.
  */
 class AttributeUniqueId {
   AttrTableId d_tableId;
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 0b664ceb4..9341c9828 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -467,7 +467,7 @@ Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapColle
     Command* cmd_to_export = *i;
     Command* cmd = cmd_to_export->exportTo(exprManager, variableMap);
     seq->addCommand(cmd);
-    Debug("export") << "[export] so far coverted: " << seq << endl;
+    Debug("export") << "[export] so far converted: " << seq << endl;
   }
   seq->d_index = d_index;
   return seq;
diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp
index 56a05795a..21c1b60a3 100644
--- a/src/main/portfolio.cpp
+++ b/src/main/portfolio.cpp
@@ -38,7 +38,7 @@ int global_winner;
 template<typename S>
 void runThread(int thread_id, boost::function<S()> threadFn, S& returnValue)
 {
-  /* Uncommment line to delay first thread, useful to unearth errors/debug */
+  /* Uncomment line to delay first thread, useful to unearth errors/debug */
   // if(thread_id == 0) { sleep(1); }
   returnValue = threadFn();
 
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);
diff --git a/src/util/backtrackable.h b/src/util/backtrackable.h
index c5844c6c4..57ed94771 100644
--- a/src/util/backtrackable.h
+++ b/src/util/backtrackable.h
@@ -170,7 +170,7 @@ void List<T>::concat (List<T>* other) {
 template <class T>
 void List<T>::unconcat(List<T>* other) {
   // we do not need to check consistency since this is only called by the
-  //Backtracker when we are inconsistent
+  // Backtracker when we are inconsistent
   Assert(other->ptr_to_head != NULL);
   other->ptr_to_head->next = NULL;
   tail = other->ptr_to_head;
diff --git a/src/util/bool.h b/src/util/bool.h
index 8e3c8849c..373b4fdec 100644
--- a/src/util/bool.h
+++ b/src/util/bool.h
@@ -9,15 +9,9 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief A multi-precision rational constant.
+ ** \brief A hash function for Boolean
  **
- ** A multi-precision rational constant.
- ** This stores the rational as a pair of multi-precision integers,
- ** one for the numerator and one for the denominator.
- ** The number is always stored so that the gcd of the numerator and denominator
- ** is 1.  (This is referred to as referred to as canonical form in GMP's
- ** literature.) A consequence is that that the numerator and denominator may be
- ** different than the values used to construct the Rational.
+ ** A hash function for Boolean.
  **/
 
 #include "cvc4_public.h"