diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-07-07 21:01:33 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-07-07 21:01:33 +0000 |
commit | 8b01efc32d61391d8d3cd2aaac0de49cd8e88ecc (patch) | |
tree | 9e61b253a66fc91ca86b11bc1cabae9e1a7394da /src/util | |
parent | 8166b6cef258b198d0ffc97d125da3c85acf9708 (diff) |
Various fixes to documentation---typos, some incomplete documentation fixed, \file tags corrected, copyright added to files that had it missing, etc.
I ensured that I didn't change any code with this commit, and even tested on the cluster to be doubly sure:
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4655&reference_id=4646&p=0
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/backtrackable.h | 2 | ||||
-rw-r--r-- | src/util/bool.h | 8 | ||||
-rw-r--r-- | src/util/dense_map.h | 2 | ||||
-rw-r--r-- | src/util/index.h | 25 | ||||
-rw-r--r-- | src/util/integer_gmp_imp.h | 2 | ||||
-rw-r--r-- | src/util/lemma_input_channel.h | 19 | ||||
-rw-r--r-- | src/util/node_visitor.h | 21 | ||||
-rw-r--r-- | src/util/options.cpp | 16 | ||||
-rw-r--r-- | src/util/options.h | 4 | ||||
-rw-r--r-- | src/util/stats.cpp | 3 |
10 files changed, 71 insertions, 31 deletions
diff --git a/src/util/backtrackable.h b/src/util/backtrackable.h index c5c6b1399..5c948841b 100644 --- a/src/util/backtrackable.h +++ b/src/util/backtrackable.h @@ -145,7 +145,7 @@ void List<T>::append (const T& d) { new(head)ListNode<T> (d, head->next); //head->data = d; head->empty = false; - //Assert(tail == head); FIXME: do I need this because this list might be empty but appende to another one + //Assert(tail == head); FIXME: do I need this because this list might be empty but append to another one uninitialized = false; } else { diff --git a/src/util/bool.h b/src/util/bool.h index 15d46b5d1..a4d33ca61 100644 --- a/src/util/bool.h +++ b/src/util/bool.h @@ -11,14 +11,14 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief A multiprecision rational constant. + ** \brief A multi-precision rational constant. ** - ** A multiprecision rational constant. - ** This stores the rational as a pair of multiprecision integers, + ** 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 consquence is that that the numerator and denominator may be + ** literature.) A consequence is that that the numerator and denominator may be ** different than the values used to construct the Rational. **/ diff --git a/src/util/dense_map.h b/src/util/dense_map.h index a687985f9..6e590ae6b 100644 --- a/src/util/dense_map.h +++ b/src/util/dense_map.h @@ -16,7 +16,7 @@ ** This is an abstraction of a Map from an unsigned integer to elements of type T. ** This class is designed to provide constant time insertion, deletion, element_of, ** and fast iteration. This is done by storing backing vectors of size greater than - ** the maximum key. This datastructure is appropraite for heavy use datastructures + ** the maximum key. This datastructure is appropriate for heavy use datastructures ** where the Keys are a dense set of integers. ** ** T must support T(), and operator=(). diff --git a/src/util/index.h b/src/util/index.h index 0c8b0a307..41afa12f2 100644 --- a/src/util/index.h +++ b/src/util/index.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file index.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 @@ -19,11 +38,11 @@ BOOST_STATIC_ASSERT(!std::numeric_limits<Index>::is_signed); /* Discussion: Why is Index a uint32_t instead of size_t (or uint_fast32_t)? * - * size_t is a more appropraite choice than uint32_t as the choice is dictated by + * size_t is a more appropriate choice than uint32_t as the choice is dictated by * uniqueness in arrays and vectors. These correspond to size_t. - * However, the using size_t with a sizeof == 8 on 64 bit platforms is noticably + * However, the using size_t with a sizeof == 8 on 64 bit platforms is noticeably * slower. (Limited testing suggests a ~1/16 of running time.) * (Interestingly, uint_fast32_t also has a sizeof == 8 on x86_64. Filthy Liars!) */ -}; /* namespace CVC4 */ +}/* CVC4 namespace */ diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index f5254a3d2..dfd6c0599 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -378,7 +378,7 @@ public: */ unsigned isPow2() const { if (d_value <= 0) return 0; - // check that the number of ones in the binary represenation is 1 + // check that the number of ones in the binary representation is 1 if (mpz_popcount(d_value.get_mpz_t()) == 1) { // return the index of the first one plus 1 return mpz_scan1(d_value.get_mpz_t(), 0) + 1; diff --git a/src/util/lemma_input_channel.h b/src/util/lemma_input_channel.h index 1627711ee..d56dc6090 100644 --- a/src/util/lemma_input_channel.h +++ b/src/util/lemma_input_channel.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file lemma_input_channel.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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_public.h" #ifndef __CVC4__LEMMA_INPUT_CHANNEL_H diff --git a/src/util/node_visitor.h b/src/util/node_visitor.h index 3714fcccc..4bd4f43b7 100644 --- a/src/util/node_visitor.h +++ b/src/util/node_visitor.h @@ -5,15 +5,15 @@ ** Major contributors: dejan ** Minor contributors (to current version): ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011, 2012 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief A simple visitor for nodes. + ** \brief A simple visitor for nodes ** - ** The theory engine. + ** A simple visitor for nodes. **/ #pragma once @@ -26,7 +26,8 @@ namespace CVC4 { /** - * Traverses the nodes topologically and call the visitor when all the children have been visited. + * Traverses the nodes reverse-topologically (children before parents), + * calling the visitor in order. */ template<typename Visitor> class NodeVisitor { @@ -34,6 +35,9 @@ class NodeVisitor { /** For re-entry checking */ static CVC4_THREADLOCAL(bool) s_inRun; + /** + * Guard against NodeVisitor<> being re-entrant. + */ class GuardReentry { bool& d_guard; public: @@ -46,7 +50,7 @@ class NodeVisitor { Assert(d_guard); d_guard = false; } - }; + };/* class NodeVisitor<>::GuardReentry */ public: @@ -74,7 +78,7 @@ public: // Notify of a start visitor.start(node); - // Do a topological sort of the subexpressions + // Do a reverse-topological sort of the subexpressions std::vector<stack_element> toVisit; toVisit.push_back(stack_element(node, node)); while (!toVisit.empty()) { @@ -108,10 +112,9 @@ public: return visitor.done(node); } -}; +};/* class NodeVisitor<> */ template <typename Visitor> CVC4_THREADLOCAL(bool) NodeVisitor<Visitor>::s_inRun = false; -} - +}/* CVC4 namespace */ diff --git a/src/util/options.cpp b/src/util/options.cpp index c02482e7e..a10aae83d 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -218,8 +218,8 @@ Additional CVC4 options:\n\ --print-winner enable printing the winning thread (pcvc4 only)\n\ --trace | -t trace something (e.g. -t pushpop), can repeat\n\ --debug | -d debug something (e.g. -d arith), can repeat\n\ - --show-debug-tags show all avalable tags for debugging\n\ - --show-trace-tags show all avalable tags for tracing\n\ + --show-debug-tags show all available tags for debugging\n\ + --show-trace-tags show all available tags for tracing\n\ --show-sat-solvers show all available SAT solvers\n\ --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\ --default-dag-thresh=N dagify common subexprs appearing > N times\n\ @@ -228,7 +228,7 @@ Additional CVC4 options:\n\ --lazy-definition-expansion expand define-funs/LAMBDAs lazily\n\ --simplification=MODE choose simplification mode, see --simplification=help\n\ --decision=MODE choose decision mode, see --decision=help\n\ - --decision-budget=N impose a budget for relevancy hueristic which increases linearly with\n\ + --decision-budget=N impose a budget for relevancy heuristic which increases linearly with\n\ each decision. N between 0 and 1000. (default: 1000, no budget)\n\ --no-static-learning turn off static learning (e.g. diamond-breaking)\n\ --ite-simp turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\ @@ -299,7 +299,7 @@ Additional CVC4 options:\n\ --threadN=string configures thread N (0..#threads-1)\n\ --filter-lemma-length=N don't share lemmas strictly longer than N\n\ --bitblast-eager eagerly bitblast the bitvectors to the main SAT solver\n\ - --bitblast-share-lemmas share lemmas from the bitblsting solver with the main solver\n\ + --bitblast-share-lemmas share lemmas from the bitblasting solver with the main solver\n\ --bitblast-eager-fullcheck check the bitblasting eagerly\n\ --refine-conflicts refine theory conflict clauses\n\ "; @@ -353,7 +353,7 @@ static const string decisionHelp = "\ 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\ @@ -430,7 +430,7 @@ t-explanations [non-stateful]\n\ + Output correctness queries for all theory explanations\n\ \n\ Dump modes can be combined with multiple uses of --dump. Generally you want\n\ -one from the assertions category (either asertions, learned, or clauses), and\n\ +one from the assertions category (either assertions, learned, or clauses), and\n\ perhaps one or more stateful or non-stateful modes for checking correctness\n\ and completeness of decision procedure implementations. Stateful modes dump\n\ the contextual assertions made by the core solver (all decisions and\n\ @@ -471,7 +471,7 @@ This decides on kind of propagation arithmetic attempts to do during the search. "; static const string pivotRulesHelp = "\ -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\ Pivot rules available:\n\ +min\n\ @@ -1067,7 +1067,7 @@ throw(OptionException) { optarg + "'. Must be between 0 and 1000."); } if(i == 0) { - Warning() << "Decision budget is 0. Consider using internal decision hueristic and " + Warning() << "Decision budget is 0. Consider using internal decision heuristic and " << std::endl << " removing this option." << std::endl; } diff --git a/src/util/options.h b/src/util/options.h index ac95c99ca..f3ae3b64e 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -269,7 +269,7 @@ struct CVC4_PUBLIC Options { ArithPropagationMode arithPropagationMode; /** - * The maximum number of difference pivots to do per invokation of simplex. + * The maximum number of difference pivots to do per invocation of simplex. * If this is negative, the number of pivots done is the number of variables. * If this is not set by the user, different logics are free to chose different * defaults. @@ -278,7 +278,7 @@ struct CVC4_PUBLIC Options { bool arithHeuristicPivotsSetByUser; /** - * The maximum number of variable order pivots to do per invokation of simplex. + * The maximum number of variable order pivots to do per invocation of simplex. * If this is negative, the number of pivots done is unlimited. * If this is not set by the user, different logics are free to chose different * defaults. diff --git a/src/util/stats.cpp b/src/util/stats.cpp index 709f80b04..b030495c5 100644 --- a/src/util/stats.cpp +++ b/src/util/stats.cpp @@ -46,8 +46,7 @@ void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) { #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::registerStat() */ -void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException) -{ +void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException) { #ifdef CVC4_STATISTICS_ON AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end()); d_registeredStats.insert(s); |