summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/backtrackable.h2
-rw-r--r--src/util/bool.h8
-rw-r--r--src/util/dense_map.h2
-rw-r--r--src/util/index.h25
-rw-r--r--src/util/integer_gmp_imp.h2
-rw-r--r--src/util/lemma_input_channel.h19
-rw-r--r--src/util/node_visitor.h21
-rw-r--r--src/util/options.cpp16
-rw-r--r--src/util/options.h4
-rw-r--r--src/util/stats.cpp3
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback