From 4abb82936fbb1a297d0d5eb69f8dbdb4599a67f2 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 24 Dec 2013 12:45:13 -0500 Subject: [PATCH] Minor code cleanup. --- src/decision/justification_heuristic.cpp | 2 +- src/decision/options_handlers.h | 2 +- src/expr/attribute.cpp | 2 +- src/expr/attribute_unique_id.h | 2 +- src/expr/command.cpp | 2 +- src/main/portfolio.cpp | 2 +- src/theory/arith/options_handlers.h | 2 +- src/theory/bv/theory_bv_utils.h | 1 - src/theory/idl/idl_assertion_db.h | 2 +- src/theory/idl/idl_model.h | 2 +- src/theory/strings/regexp_operation.h | 4 ++-- src/theory/strings/theory_strings.cpp | 8 ++++---- src/theory/strings/theory_strings.h | 12 ++++++------ src/theory/theory_engine.h | 2 +- src/util/backtrackable.h | 2 +- src/util/bool.h | 10 ++-------- 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 void runThread(int thread_id, boost::function 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; i1 && 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& 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::concat (List* other) { template void List::unconcat(List* 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" -- 2.30.2