Minor code cleanup.

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 78de1a74e5ae68bfb4d2ba9a79cd4c2b31dd0d9a..54d2dee97af1c5b8f58a5b6d75897a6f48faf1ab 100644 (file)
--- 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 f538ba94772af7ed33eba785217b66e0725de0b9..a8931aecb2d6cf1b70ab75cb84ff64837b8e0dbd 100644 (file)
--- 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 86768500b09b87f2a177f8e65d7e739d32a889e0..cde2614633142a8608840c31e29090f52fa637e2 100644 (file)
--- 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 08b31a4c0492dcd24c04267df4488aa83199073e..3a52d7a89628f3971a7561bde76bc97d9b202e51 100644 (file)
--- 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 0b664ceb4a0031a562aa95f61002ea882dfe07a9..9341c9828e175684f9406671a044324bac5287fc 100644 (file)
--- 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 56a05795a65b91b0370ba151f703d0423adb15ee..21c1b60a3b22331a06fb364fdfe6475d30c36b57 100644 (file)
--- 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 a72ced0bc94248e0cbb30f6dfa8735b27028f2fb..f81f1b2272e6352ded4bfb7920e632e5047b874f 100644 (file)
--- 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 5140bd498d60893153bbce3bef1d4de6ec39bb09..f35fc28966acb4f22a8aafc6375504c2269328cc 100644 (file)
--- 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 205102b0f7c63f65624ac6543df9dd639be6c196..358a5386e2e936e9fe2eaf56220c48f2abd20c5c 100644 (file)
--- 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 22e05c469ca4a1bc004f3d03bda70d70556a696e..c69a0c38f3add095cd20655c4f52ef8e6df27b8e 100644 (file)
--- 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 a47f7bd776f49549d0b3b1db5293b5656686b921..9ed4be0c3c2e78b6fed0775c7ed5cdb2f4089050 100644 (file)
--- 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\r
+ ** \brief Regular Expression Operations\r
  **\r
- ** Regular Expresion Operations\r
+ ** Regular Expression Operations\r
  **/\r
 \r
 #include "cvc4_private.h"\r

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 9f4d84765bbd449a16a281c7393b36510a9baebd..62e71327e5e5ccaae69bb14ca3d0964244a92cd4 100644 (file)
--- 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 4d2a192cf265f5066ffe86b0f94602d0386d1b0a..875f407c51260d3cf6f49d77a62cb3cb0d9bdcb2 100644 (file)
--- 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 ffc36e59b7fa5e47fa06be5629746703e6850f92..92469aa3174f4e3c328d0e75b635deec0f348e96 100644 (file)
--- 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 c5844c6c47640661e6324716554d8ba812375806..57ed9477101b27d69e4ef4266f26055d2032be74 100644 (file)
--- 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 8e3c8849ca7d8a89391a51562f3ed754ca6b7d51..373b4fdec5fb0e868d1aa36adb4df91d9375e958 100644 (file)
--- 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"