diff options
98 files changed, 540 insertions, 300 deletions
diff --git a/contrib/extract-strings-and-comments b/contrib/extract-strings-and-comments new file mode 100755 index 000000000..a6670c1e9 --- /dev/null +++ b/contrib/extract-strings-and-comments @@ -0,0 +1,52 @@ +#!/usr/bin/perl -0777 + +my $debug = 0; + +$_ = <>; +my $comments = ""; +my $code = ""; + +# ignore strings and comments appearing in preprocessor directives +s/^#.*//mg; + +for(;;) { + s,^([^"/]+),,; + $code .= "$1\n"; + + if(m,^([^"]*)"",) { + s,^([^"]*)"",,s; + $code .= "$1\n"; + next; + } + if(m,^([^"]*)"([^"]*)",) { + s,^([^"]*)"(([^\\"]*?([^\\"]|(\\.)))+)",,s; + print STDERR "quote: $2\n" if $debug; + $code .= "$1\n"; + $comments .= "$2\n"; + next; + } + if(m,/\*.*?\*/,) { + s,/\*(.*?)\*/,,s; + print STDERR "c-style comment: $1\n" if $debug; + $comments .= "$1\n"; + print STDERR "REMAINDER:\n===========================\n$_\n=========================\n" if $debug; + next; + } + if(m,//,) { + s,//([^\n]*),,s; + print STDERR "c++-style comment: $1\n" if $debug; + $comments .= "$1\n"; + print STDERR "REMAINDER:\n===========================\n$_\n=========================\n" if $debug; + next; + } + last; +} + +$code .= "$_\n"; +$code =~ s,\W+,\n,g; +$code =~ s,^,@,gm; +print "$code\n"; + +$comments =~ s,^,^,gm; +print "$comments\n"; + diff --git a/contrib/spellcheck b/contrib/spellcheck new file mode 100755 index 000000000..4aa210a50 --- /dev/null +++ b/contrib/spellcheck @@ -0,0 +1,22 @@ +#!/bin/bash + +dir="$(dirname "$0")" + +find src \( -name '*.cpp' -o -name '*.h' \) \! -path 'src/prop/minisat/*' \! -path 'src/prop/bvminisat/*' \! -path 'src/prop/cryptominisat/*' \! -path 'src/parser/*/generated/*' | + while read f; do + misspelled_words=` + $dir/extract-strings-and-comments $f | + ispell -a -W 3 2>/dev/null | + tail -n +2 | + while read s; do + case "$s" in + \**|\+*|-*) ;; + \&*|\#*|\?*) echo "$s" | awk '{print$2}';; +# *) test -n "$s" && echo "UNKNOWN : $s";; + esac + done | sort -fu | sed 's,^, ,'` + if [ -n "$misspelled_words" ]; then + echo "$f" + echo "$misspelled_words" + fi + done diff --git a/contrib/theoryskel/theory_DIR.h b/contrib/theoryskel/theory_DIR.h index ed36193f7..f8151ae42 100644 --- a/contrib/theoryskel/theory_DIR.h +++ b/contrib/theoryskel/theory_DIR.h @@ -12,7 +12,7 @@ namespace $dir { class Theory$camel : public Theory { public: - /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ + /** Constructs a new instance of Theory$camel w.r.t. the provided context.*/ Theory$camel(context::Context* c, context::UserContext* u, OutputChannel& out, diff --git a/src/context/cdhashmap_forward.h b/src/context/cdhashmap_forward.h index f1031fec4..593807f5c 100644 --- a/src/context/cdhashmap_forward.h +++ b/src/context/cdhashmap_forward.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file cdmap_forward.h +/*! \file cdhashmap_forward.h ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 @@ -20,7 +20,7 @@ ** public header context. ** ** For CDMap<> in particular, it's difficult to forward-declare it - ** yourself, becase it has a default template argument. + ** yourself, because it has a default template argument. **/ #include "cvc4_public.h" diff --git a/src/context/cdhashset.h b/src/context/cdhashset.h index bf1f7d097..7e15cf9eb 100644 --- a/src/context/cdhashset.h +++ b/src/context/cdhashset.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file cdset.h +/*! \file cdhashset.h ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/context/cdhashset_forward.h b/src/context/cdhashset_forward.h index dc7da22d2..01482ed34 100644 --- a/src/context/cdhashset_forward.h +++ b/src/context/cdhashset_forward.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file cdset_forward.h +/*! \file cdhashset_forward.h ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 @@ -20,7 +20,7 @@ ** public header context. ** ** For CDSet<> in particular, it's difficult to forward-declare it - ** yourself, becase it has a default template argument. + ** yourself, because it has a default template argument. **/ #include "cvc4_public.h" diff --git a/src/context/cdlist.h b/src/context/cdlist.h index 1630fa586..a63bd2d21 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -442,8 +442,8 @@ class CDList <T, CleanUp, ContextMemoryAllocator<T> > : public ContextObj { * * Explanation: * If ContextMemoryAllocator is used and d_list grows at a deeper context level - * the reallocated will be reallocated in a context memory regaion that can be - * detroyed on pop. To support this, a full copy of d_list would have to be made. + * the reallocated will be reallocated in a context memory region that can be + * destroyed on pop. To support this, a full copy of d_list would have to be made. * As this is unacceptable for performance in other situations, we do not do * this. */ diff --git a/src/context/cdmaybe.h b/src/context/cdmaybe.h index 3c95ab126..676025d03 100644 --- a/src/context/cdmaybe.h +++ b/src/context/cdmaybe.h @@ -1,8 +1,23 @@ -/** - * This implements a CDMaybe. - * This has either been set in the context or it has not. - * T must have a default constructor and support assignment. - */ +/********************* */ +/*! \file cdmaybe.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 A context-dependent "maybe" template type + ** + ** This implements a CDMaybe. + ** This has either been set in the context or it has not. + ** Template parameter T must have a default constructor and support + ** assignment. + **/ #include "cvc4_private.h" @@ -33,7 +48,7 @@ public: d_flag.set(true); } -}; /* class CDRaised */ +};/* class CDRaised */ template <class T> class CDMaybe { @@ -58,7 +73,7 @@ public: Assert(isSet()); return d_data.get().second; } -}; /* class CDMaybe<T> */ +};/* class CDMaybe<T> */ }/* CVC4::context namespace */ }/* CVC4 namespace */ diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 065d40a9a..c7051d570 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file justification_heuristic.h +/*! \file justification_heuristic.cpp ** \verbatim ** Original author: kshitij ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2012 The Analysis of Computer Systems Group (ACSys) + ** 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 @@ -165,7 +165,7 @@ bool JustificationHeuristic::findSplitterRec(TNode node, /* Good luck, hope you can get what you want */ Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN, - "invariant voilated"); + "invariant violated"); /* What type of node is this */ Kind k = node.getKind(); diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 1dc7a85d7..f0ae9fe78 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -37,7 +37,7 @@ namespace decision { class GiveUpException : public Exception { public: GiveUpException() : - Exception("justification hueristic: giving up") { + Exception("justification heuristic: giving up") { } };/* class GiveUpException */ @@ -196,7 +196,7 @@ private: } /** - * Do all the hardwork. + * Do all the hard work. * @param findFirst returns */ bool findSplitterRec(TNode node, SatValue value, SatLiteral* litDecision); diff --git a/src/decision/relevancy.cpp b/src/decision/relevancy.cpp index f73337c8f..d0d44f606 100644 --- a/src/decision/relevancy.cpp +++ b/src/decision/relevancy.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file relevancy.h +/*! \file relevancy.cpp ** \verbatim ** Original author: kshitij ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2012 The Analysis of Computer Systems Group (ACSys) + ** 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 @@ -143,7 +143,7 @@ bool Relevancy::findSplitterRec(TNode node, /* Good luck, hope you can get what you want */ Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN, - "invariant voilated"); + "invariant violated"); /* What type of node is this */ Kind k = node.getKind(); diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index cf2616011..1db534dc4 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -51,7 +51,7 @@ ${includes} if (d_exprStatisticsVars[type] == NULL) { \ stringstream statName; \ if (type == LAST_TYPE) { \ - statName << "expr::ExprManager::VARIABLE:Parametrized type"; \ + statName << "expr::ExprManager::VARIABLE:Parameterized type"; \ } else { \ statName << "expr::ExprManager::VARIABLE:" << type; \ } \ diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index c5d41816e..fcb503d37 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -569,7 +569,7 @@ public: Assert(getKind() == kind::UNDEFINED_KIND || d_nv->d_id == 0, "can't redefine the Kind of a NodeBuilder"); Assert(d_nv->d_id == 0, - "interal inconsistency with NodeBuilder: d_id != 0"); + "internal inconsistency with NodeBuilder: d_id != 0"); AssertArgument(k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR && k < kind::LAST_KIND, diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index b900a6994..6ce96e70a 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -661,10 +661,10 @@ public: /** Make a new (anonymous) sort of arity 0. */ inline TypeNode mkSort(); - /** Make a new sort with the given name and arity. */ + /** Make a new sort with the given name of arity 0. */ inline TypeNode mkSort(const std::string& name); - /** Make a new sort with the given name and arity. */ + /** Make a new sort by parameterizing the given sort constructor. */ inline TypeNode mkSort(TypeNode constructor, const std::vector<TypeNode>& children); diff --git a/src/expr/pickler.h b/src/expr/pickler.h index 6e79d6997..a6427ad47 100644 --- a/src/expr/pickler.h +++ b/src/expr/pickler.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file pickle.h +/*! \file pickler.h ** \verbatim - ** Original author: kshitij - ** Major contributors: taking, mdeters + ** Original author: mdeters + ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/main/driver.cpp b/src/main/driver.cpp index 44457841d..958175030 100644 --- a/src/main/driver.cpp +++ b/src/main/driver.cpp @@ -11,9 +11,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Driver for (sequential) CVC4 executable + ** \brief Driver for (sequential) CVC4 executable (cvc4) ** - ** Driver for (sequential) CVC4 executable. + ** Driver for (sequential) CVC4 executable (cvc4). **/ #include <cstdlib> diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp index a8da88173..486e0e0d3 100644 --- a/src/main/driver_portfolio.cpp +++ b/src/main/driver_portfolio.cpp @@ -1,3 +1,21 @@ +/********************* */ +/*! \file driver_portfolio.cpp + ** \verbatim + ** Original author: kshitij + ** Major contributors: taking, mdeters + ** 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 Driver for portfolio CVC4 executable (pcvc4) + ** + ** Driver for portfolio CVC4 executable (pcvc4). + **/ + #include <cstdio> #include <cstdlib> #include <iostream> @@ -786,10 +804,10 @@ void sharingManager(int numThreads, } } /* end of infinite while */ - Trace("interrupt") << "sharing thread interuppted, interrupting all smtEngines" << std::endl; + Trace("interrupt") << "sharing thread interrupted, interrupting all smtEngines" << std::endl; for(int t = 0; t < numThreads; ++t) { - Trace("interrupt") << "Interuppting thread #" << t << std::endl; + Trace("interrupt") << "Interrupting thread #" << t << std::endl; try{ smts[t]->interrupt(); }catch(ModalException &e){ @@ -798,5 +816,5 @@ void sharingManager(int numThreads, } } - Trace("sharing") << "sharing: Interuppted, exiting." << std::endl; + Trace("sharing") << "sharing: Interrupted, exiting." << std::endl; } diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp index 581ee6d96..0bf033a22 100644 --- a/src/proof/sat_proof.cpp +++ b/src/proof/sat_proof.cpp @@ -111,7 +111,7 @@ bool resolve(const Lit v, LitSet& clause1, LitSet& clause2, bool s) { } else { // literal appears negative in the first clause if( !clause1.count(~var) || !clause2.count(var)) { - Debug("proof:sat") << "proof:resolve: Mising literal "; + Debug("proof:sat") << "proof:resolve: Missing literal "; printLit(var); Debug("proof:sat") << endl; return false; diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index f75e74d63..69db89086 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -327,7 +327,7 @@ private: /** * Transforms the node into CNF recursively. * @param node the formula to transform - * @param negated wheather the literal is negated + * @param negated whether the literal is negated * @return the literal representing the root of the formula */ SatLiteral toCNF(TNode node, bool negated = false); diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 102f8051b..c30f18d29 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file sat_module.h +/*! \file sat_solver.h ** \verbatim ** Original author: lianah - ** Major contributors: - ** Minor contributors (to current version): + ** Major contributors: dejan + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index 3b048af47..68f09eb72 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file sat_solver_factory.h +/*! \file sat_solver_factory.cpp ** \verbatim - ** Original author: lianah - ** Major contributors: - ** Minor contributors (to current version): + ** Original author: dejan + ** Major contributors: taking + ** Minor contributors (to current version): lianah ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/prop/sat_solver_registry.cpp b/src/prop/sat_solver_registry.cpp index 01434bd80..53753d3e1 100644 --- a/src/prop/sat_solver_registry.cpp +++ b/src/prop/sat_solver_registry.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file sat_solver_registry.h +/*! \file sat_solver_registry.cpp ** \verbatim - ** Original author: taking - ** Major contributors: mdeters, dejan - ** Minor contributors (to current version): barrett, cconway + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/prop/sat_solver_registry.h b/src/prop/sat_solver_registry.h index df1cf86f8..cf829849f 100644 --- a/src/prop/sat_solver_registry.h +++ b/src/prop/sat_solver_registry.h @@ -35,7 +35,7 @@ namespace CVC4 { namespace prop { /** - * Interface for SAT solver constructors. Solvers should declare an instantiatiation of the + * Interface for SAT solver constructors. Solvers should declare an instantiation of the * SatSolverConstructor interface below. */ class SatSolverConstructorInterface { @@ -59,7 +59,7 @@ class SatSolverRegistry { /** * Register a SAT solver with the registry. The Constructor type should be a subclass - * of the SatSolverConstrutor. + * of the SatSolverConstructor. */ template <typename Constructor> size_t registerSolver(const char* id) { diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h index 9dcc1c4bf..88ddb8107 100644 --- a/src/prop/sat_solver_types.h +++ b/src/prop/sat_solver_types.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file cnf_stream.h +/*! \file sat_solver_types.h ** \verbatim - ** Original author: taking - ** Major contributors: mdeters, dejan - ** Minor contributors (to current version): barrett, cconway, kshitij + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): kshitij ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 15a383d92..668b57b40 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file sat.cpp +/*! \file theory_proxy.cpp ** \verbatim ** Original author: cconway - ** Major contributors: dejan, taking, mdeters - ** Minor contributors (to current version): kshitij + ** Major contributors: lianah, dejan, kshitij, mdeters + ** Minor contributors (to current version): barrett, taking ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 @@ -80,12 +80,13 @@ void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) { SatLiteral TheoryProxy::getNextDecisionRequest(bool &stopSearch) { TNode n = d_theoryEngine->getNextDecisionRequest(); - if(not n.isNull()) + if(not n.isNull()) { return d_cnfStream->getLiteral(n); - + } + // If theory doesn't give us a deicsion ask the decision engine. It - // may return in undefSatLiteral in which case the sat solver figure - // it out something + // may return in undefSatLiteral in which case the sat solver uses + // whatever default heuristic it has. Assert(d_decisionEngine != NULL); Assert(stopSearch != true); SatLiteral ret = d_decisionEngine->getNext(stopSearch); diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 99aab8286..26357886c 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file sat.h +/*! \file theory_proxy.h ** \verbatim ** Original author: mdeters - ** Major contributors: taking, cconway, dejan - ** Minor contributors (to current version): barrett, kshitij + ** Major contributors: kshitij, lianah, dejan + ** Minor contributors (to current version): taking, cconway ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h index d1fac1e58..43cf54d37 100644 --- a/src/theory/arith/arith_priority_queue.h +++ b/src/theory/arith/arith_priority_queue.h @@ -50,7 +50,7 @@ namespace arith { * to determine which to dequeue first. * * - Variable Order Queue - * This mode uses the variable order to determine which ArithVar is deuqued first. + * This mode uses the variable order to determine which ArithVar is dequeued first. * * The transitions between the modes of operation are: * Collection => Difference Queue @@ -119,7 +119,7 @@ private: /** * Priority Queue of the basic variables that may be inconsistent. * Variables are ordered according to which violates its bound the most. - * This is a heuristic and makes no guarentees to terminate! + * This is a heuristic and makes no guarantees to terminate! * This heuristic comes from Alberto Griggio's thesis. */ DifferenceArray d_diffQueue; diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index 5ce27eb46..a478f3cfb 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -417,6 +417,6 @@ void ArithStaticLearner::addBound(TNode n) { } } -}; /* namesapce arith */ -}; /* namespace theory */ -}; /* namespace CVC4 */ +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index d877339b3..66eb4d311 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -84,7 +84,7 @@ private: void miplibTrick(TNode var, std::set<Rational>& values, NodeBuilder<>& learned); - /** These fields are designed to be accessable to ArithStaticLearner methods. */ + /** These fields are designed to be accessible to ArithStaticLearner methods. */ class Statistics { public: IntStat d_iteMinMaxApplications; diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index fb669cce4..6ac2338f3 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -259,10 +259,8 @@ inline Node flattenAnd(Node n){ return NodeManager::currentNM()->mkNode(kind::AND, out); } -}; /* namesapce arith */ -}; /* namespace theory */ -}; /* namespace CVC4 */ - - +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ #endif /* __CVC4__THEORY__ARITH__ARITH_UTILITIES_H */ diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h index 924e91bf5..80190b065 100644 --- a/src/theory/arith/arithvar.h +++ b/src/theory/arith/arithvar.h @@ -62,8 +62,8 @@ public: virtual void operator()(Node n) = 0; }; -}; /* namesapce arith */ -}; /* namespace theory */ -}; /* namespace CVC4 */ +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ #endif /* __CVC4__THEORY__ARITH__ARITHVAR_H */ diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 52f4c7014..b167acf40 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file congruence_manager.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): dejan + ** 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 "theory/arith/congruence_manager.h" #include "theory/arith/constraint.h" diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index fd8eef1f1..83a5e7fb4 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -1,4 +1,21 @@ - +/********************* */ +/*! \file congruence_manager.h + ** \verbatim + ** Original author: taking + ** Major contributors: dejan + ** 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" @@ -179,7 +196,7 @@ private: */ //void assertLiteral(bool eq, ArithVar s, TNode reason); - /** This sends a shared term to the uninterpretted equality engine. */ + /** This sends a shared term to the uninterpreted equality engine. */ //void addAssertionToEqualityEngine(bool eq, ArithVar s, TNode reason); void assertionToEqualityEngine(bool eq, ArithVar s, TNode reason); @@ -241,10 +258,8 @@ private: ~Statistics(); } d_statistics; -};/* class CongruenceManager */ +};/* class ArithCongruenceManager */ }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ - - diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index ce338b5f3..0d8a0a8f4 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -1,3 +1,21 @@ +/********************* */ +/*! \file constraint.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): dejan + ** 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" #include "theory/arith/constraint.h" @@ -1369,6 +1387,6 @@ void ConstraintDatabase::unatePropEquality(Constraint curr, Constraint prevLB, C } } -}/* arith namespace */ -}/* theory namespace */ +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index be4197a26..56fa5dcdf 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -243,7 +243,7 @@ private: * * This is not context dependent, but may be set once. * - * This must be set if the constraint canbePropgated(). + * This must be set if the constraint canBePropagated(). * This must be set if the constraint assertedToTheTheory(). * Otherwise, this may be null(). */ @@ -290,7 +290,7 @@ private: /** * True if the equality has been split. - * Only meaningful if ContraintType == Equality. + * Only meaningful if ConstraintType == Equality. * * User Context Dependent. * This is initially false. @@ -490,7 +490,7 @@ public: /** * Returns a explanation of the constraint that is appropriate for conflicts. * - * This is not appropraite for propagation! + * This is not appropriate for propagation! * * This is the minimum fringe of the implication tree s.t. * every constraint is assertedToTheTheory() or hasEqualityEngineProof(). @@ -507,7 +507,7 @@ public: * This is the minimum fringe of the implication tree s.t. * every constraint is assertedToTheTheory() or hasEqualityEngineProof(). * - * This is not appropraite for propagation! + * This is not appropriate for propagation! * Use explainForPropagation() instead. */ void explainForConflict(NodeBuilder<>& nb) const{ @@ -587,7 +587,7 @@ public: void propagate(const std::vector<Constraint>& b); /** * The only restriction is that this is not known be true. - * This propgates if there is a node. + * This propagates if there is a node. */ void impliedBy(Constraint a); void impliedBy(Constraint a, Constraint b); @@ -829,7 +829,7 @@ public: * If no such constraint exists, NullConstraint is returned. * * t must be either UpperBound or LowerBound. - * The returned value v is dominatated: + * The returned value v is dominated: * If t is UpperBound, r <= v * If t is LowerBound, r >= v */ diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 38cff88ff..e3eae88b3 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -279,7 +279,7 @@ void DioSolver::enqueueInputConstraints(){ /*TODO Currently linear in the size of the Queue *It is not clear if am O(log n) strategy would be better. - *Right before this in the algorithm is a substition which could potentially + *Right before this in the algorithm is a substitution which could potentially *effect the key values of everything in the queue. */ void DioSolver::moveMinimumByAbsToQueueFront(){ @@ -508,7 +508,7 @@ SumPair DioSolver::processEquationsForCut(){ SumPair DioSolver::purifyIndex(TrailIndex i){ - // TODO: "This uses the substition trail to reverse the substitions from the sum term. Using the proof term should be more efficient." + // TODO: "This uses the substitution trail to reverse the substitutions from the sum term. Using the proof term should be more efficient." SumPair curr = d_trail[i].d_eq; diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index b92aced4e..b6c9e3afb 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -383,7 +383,7 @@ private: void debugPrintTrail(TrailIndex i) const; public: - /** These fields are designed to be accessable to TheoryArith methods. */ + /** These fields are designed to be accessible to TheoryArith methods. */ class Statistics { public: diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index 7efe349e5..95f8138d2 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file simplex.cpp +/*! \file linear_equality.cpp ** \verbatim ** Original author: taking ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index 7cac4c871..2553bedd0 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -63,7 +63,7 @@ private: public: /** - * Initailizes a LinearEqualityModule with a partial model, a tableau, + * Initializes a LinearEqualityModule with a partial model, a tableau, * and a callback function for when basic variables update their values. */ LinearEqualityModule(ArithPartialModel& pm, Tableau& t, ArithVarCallBack& f): @@ -145,7 +145,7 @@ public: private: - /** These fields are designed to be accessable to TheoryArith methods. */ + /** These fields are designed to be accessible to TheoryArith methods. */ class Statistics { public: IntStat d_statPivots, d_statUpdates; diff --git a/src/theory/arith/matrix.cpp b/src/theory/arith/matrix.cpp index 6320f87ce..a691d61da 100644 --- a/src/theory/arith/matrix.cpp +++ b/src/theory/arith/matrix.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file tableau.cpp +/*! \file matrix.cpp ** \verbatim ** Original author: taking ** Major contributors: none ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h index f0e17f8a4..5ed1b9ab2 100644 --- a/src/theory/arith/matrix.h +++ b/src/theory/arith/matrix.h @@ -336,7 +336,7 @@ public: typedef typename SuperT::const_iterator const_iterator; RowVector(MatrixEntryVector<T>* mev) : SuperT(mev){} -}; +};/* class RowVector<T> */ template <class T> class ColumnVector : public MatrixVector<T, false> @@ -347,7 +347,7 @@ public: typedef typename SuperT::const_iterator const_iterator; ColumnVector(MatrixEntryVector<T>* mev) : SuperT(mev){} -}; +};/* class ColumnVector<T> */ template <class T> class Matrix { @@ -919,7 +919,7 @@ private: /* Changes the basic variable on the row for basicOld to basicNew. */ void rowPivot(ArithVar basicOld, ArithVar basicNew); -}; +};/* class Tableau */ }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index f42b6d398..b054f9804 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -977,7 +977,7 @@ public: */ static Node computeQR(const Polynomial& p, const Integer& z); - /** Returns the coefficient assiociated with the VarList in the polynomial. */ + /** Returns the coefficient associated with the VarList in the polynomial. */ Constant getCoefficient(const VarList& vl) const; uint32_t maxLength() const{ @@ -1041,7 +1041,7 @@ public: * is known to implicitly be equal to 0. * * SumPairs do not have unique representations due to the potential for p = 0. - * This makes them inappropraite for normal forms. + * This makes them inappropriate for normal forms. */ class SumPair : public NodeWrapper { private: diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index 0fabe1a0f..99a6e4878 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -304,6 +304,6 @@ void ArithPartialModel::computeDelta(){ d_deltaIsSafe = true; } -}; /* namesapce arith */ -}; /* namespace theory */ -}; /* namespace CVC4 */ +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 9ba44b102..33c6537de 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -271,7 +271,7 @@ private: - /** These fields are designed to be accessable to TheoryArith methods. */ + /** These fields are designed to be accessible to TheoryArith methods. */ class Statistics { public: IntStat d_statUpdateConflicts; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 6174e9500..188f73c78 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -2284,6 +2284,6 @@ void TheoryArith::propagateCandidates(){ } } -}; /* namesapce arith */ -}; /* namespace theory */ -}; /* namespace CVC4 */ +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 0431f543c..fd2925bf6 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -372,7 +372,7 @@ private: /** * Splits the disequalities in d_diseq that are violated using lemmas on demand. * returns true if any lemmas were issued. - * returns false if all disequalities are satisified in the current model. + * returns false if all disequalities are satisfied in the current model. */ bool splitDisequalities(); @@ -433,7 +433,7 @@ private: /** Tracks the bounds that were updated in the current round. */ DenseSet d_updatedBounds; - /** Tracks the basic variables where propagatation might be possible. */ + /** Tracks the basic variables where propagation might be possible. */ DenseSet d_candidateBasics; bool hasAnyUpdates() { return !d_updatedBounds.empty(); } @@ -466,7 +466,7 @@ private: bool assertionCases(Constraint c); /** - * Returns the basic variable with the shorted row containg a non-basic variable. + * Returns the basic variable with the shorted row containing a non-basic variable. * If no such row exists, return ARITHVAR_SENTINEL. */ ArithVar findShortestBasicRow(ArithVar variable); @@ -493,7 +493,7 @@ private: /** Debugging only routine. Prints the model. */ void debugPrintModel(); - /** These fields are designed to be accessable to TheoryArith methods. */ + /** These fields are designed to be accessible to TheoryArith methods. */ class Statistics { public: IntStat d_statAssertUpperConflicts, d_statAssertLowerConflicts; diff --git a/src/theory/arith/theory_arith_instantiator.cpp b/src/theory/arith/theory_arith_instantiator.cpp index 48c8a30ee..f1b870c52 100644 --- a/src/theory/arith/theory_arith_instantiator.cpp +++ b/src/theory/arith/theory_arith_instantiator.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file instantiator_arith_instantiator.cpp +/*! \file theory_arith_instantiator.cpp ** \verbatim ** Original author: ajreynol ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/theory/arith/theory_arith_instantiator.h b/src/theory/arith/theory_arith_instantiator.h index 524d16859..3880a49a7 100644 --- a/src/theory/arith/theory_arith_instantiator.h +++ b/src/theory/arith/theory_arith_instantiator.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file instantiator_arith_instantiator.h +/*! \file theory_arith_instantiator.h ** \verbatim ** Original author: ajreynol ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 796bc9e21..04934b1fa 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -264,7 +264,7 @@ public: /** * Propagate through the asserted circuit propagator. New information discovered by the propagator - * are put in the subsitutions vector used in construction. + * are put in the substitutions vector used in construction. * * @return true iff conflict found */ diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index c063245a5..bb6dfe40b 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -516,7 +516,7 @@ void DefaultMultBB (TNode node, Bits& res, Bitblaster* bb) { } void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefaulPlusBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefaultPlusBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_PLUS && res.size() == 0); @@ -537,7 +537,7 @@ void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) { void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefautSubBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefaultSubBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_SUB && node.getNumChildren() == 2 && bits.size() == 0); @@ -555,7 +555,7 @@ void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) { } void DefaultNegBB (TNode node, Bits& bits, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefautNegBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefaultNegBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_NEG); Bits a; @@ -633,7 +633,7 @@ void uDivModRec(const Bits& a, const Bits& b, Bits& q, Bits& r, unsigned rec_wid } void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefautUdivBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_UDIV && q.size() == 0); Bits a, b; @@ -649,7 +649,7 @@ void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) { } void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefautUremBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_UREM && rem.size() == 0); Bits a, b; diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index a5a9b9a7e..24d6b300b 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file bv_subtheory_eq_bitblast.cpp +/*! \file bv_subtheory_bitblast.cpp ** \verbatim - ** Original author: lianah - ** Major contributors: dejan + ** Original author: dejan + ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 0a8f046b7..324921f9a 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file bv_subtheory_eq_bitblast.h +/*! \file bv_subtheory_bitblast.h ** \verbatim - ** Original author: lianah - ** Major contributors: dejan + ** Original author: dejan + ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h index 8cbf99ae9..005be88a8 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h +++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file theory_bv_rewrite_rules_core.h +/*! \file theory_bv_rewrite_rules_constant_evaluation.h ** \verbatim ** Original author: lianah - ** Major contributors: none - ** Minor contributors (to current version): + ** Major contributors: barrett + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index 506570ed2..48df9492d 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file theory_bv_rewrite_rules_core.h +/*! \file theory_bv_rewrite_rules_operator_elimination.h ** \verbatim ** Original author: lianah - ** Major contributors: none - ** Minor contributors (to current version): + ** Major contributors: barrett + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 @@ -65,7 +65,7 @@ bool RewriteRule<SgtEliminate>::applies(TNode node) { template<> Node RewriteRule<SgtEliminate>::apply(TNode node) { - BVDebug("bv-rewrite") << "RgewriteRule<UgtEliminate>(" << node << ")" << std::endl; + BVDebug("bv-rewrite") << "RewriteRule<SgtEliminate>(" << node << ")" << std::endl; TNode a = node[0]; TNode b = node[1]; Node result = utils::mkNode(kind::BITVECTOR_SLT, b, a); diff --git a/src/theory/datatypes/theory_datatypes_instantiator.h b/src/theory/datatypes/theory_datatypes_instantiator.h index 5c52f7f48..ab5703757 100644 --- a/src/theory/datatypes/theory_datatypes_instantiator.h +++ b/src/theory/datatypes/theory_datatypes_instantiator.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file instantiator_datatypes_instantiator.h +/*! \file theory_datatypes_instantiator.h ** \verbatim ** Original author: ajreynol ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/theory/inst_match.h b/src/theory/inst_match.h index 73a99bcc5..dcb9190a1 100644 --- a/src/theory/inst_match.h +++ b/src/theory/inst_match.h @@ -277,7 +277,7 @@ public: virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0; /** get the next match. must call reset( eqc ) before this function. */ virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0; - /** return true if whatever Node is subsituted for the variables the + /** return true if whatever Node is substituted for the variables the given Node can't match the pattern */ virtual bool nonunifiable( TNode t, const std::vector<Node> & vars) = 0; /** add instantiations directly */ @@ -323,7 +323,7 @@ private: bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe ); public: /** get the match against ground term or formula t. - d_match_mattern and t should have the same shape. + d_match_pattern and t should have the same shape. only valid for use where !d_match_pattern.isNull(). */ bool getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ); @@ -346,7 +346,7 @@ public: void reset( Node eqc, QuantifiersEngine* qe ); /** get the next match. must call reset( eqc ) before this function. */ bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ); - /** return true if whatever Node is subsituted for the variables the + /** return true if whatever Node is substituted for the variables the given Node can't match the pattern */ bool nonunifiable( TNode t, const std::vector<Node> & vars); /** add instantiations */ @@ -371,9 +371,9 @@ private: std::vector< IndexedTrie >& unique_var_tries, int uvtIndex, InstMatchTrie* tr = NULL, int trieIndex = 0 ); private: - /** var contains (variable indicies) for each pattern node */ + /** var contains (variable indices) for each pattern node */ std::map< Node, std::vector< int > > d_var_contains; - /** variable indicies contained to pattern nodes */ + /** variable indices contained to pattern nodes */ std::map< int, std::vector< Node > > d_var_to_node; /** quantifier to use */ Node d_f; @@ -396,7 +396,7 @@ public: void reset( Node eqc, QuantifiersEngine* qe ); /** get the next match. must call reset( eqc ) before this function. (not implemented) */ bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; } - /** return true if whatever Node is subsituted for the variables the + /** return true if whatever Node is substituted for the variables the given Node can't match the pattern */ bool nonunifiable( TNode t, const std::vector<Node> & vars) { return true; } /** add instantiations */ @@ -428,7 +428,7 @@ public: void reset( Node eqc, QuantifiersEngine* qe ) {} /** get the next match. must call reset( eqc ) before this function. (not implemented) */ bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; } - /** return true if whatever Node is subsituted for the variables the + /** return true if whatever Node is substituted for the variables the given Node can't match the pattern */ bool nonunifiable( TNode t, const std::vector<Node> & vars) { return true; } /** add instantiations */ diff --git a/src/theory/inst_match_impl.h b/src/theory/inst_match_impl.h index b38bcb6f5..8ac5fd34f 100644 --- a/src/theory/inst_match_impl.h +++ b/src/theory/inst_match_impl.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file inst_match.h +/*! \file inst_match_impl.h ** \verbatim - ** Original author: ajreynol + ** Original author: bobot ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): taking, mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/theory/instantiator_default.h b/src/theory/instantiator_default.h index 351d0c4a3..8e0e47231 100644 --- a/src/theory/instantiator_default.h +++ b/src/theory/instantiator_default.h @@ -40,7 +40,7 @@ public: void assertNode( Node assertion ); /** identify */ std::string identify() const { return std::string("InstantiatorDefault"); } -};/* class Instantiatior */ +};/* class InstantiatorDefault */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 4031efdf9..cf6691918 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file instantiation_engine.h +/*! \file model_engine.h ** \verbatim ** Original author: ajreynol - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 0fba9d59e..4850d999b 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file theory_quantifiers_rewriter.cpp +/*! \file quantifiers_rewriter.cpp ** \verbatim ** Original author: ajreynol - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/theory/quantifiers/theory_quantifiers_instantiator.h b/src/theory/quantifiers/theory_quantifiers_instantiator.h index dda3bfeaa..39e34c319 100644 --- a/src/theory/quantifiers/theory_quantifiers_instantiator.h +++ b/src/theory/quantifiers/theory_quantifiers_instantiator.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file instantiator_quantifiers_instantiator.h +/*! \file theory_quantifiers_instantiator.h ** \verbatim ** Original author: ajreynol ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index 4169cb9fe..afca18b76 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -85,7 +85,7 @@ class Rewriter { static RewriteResponse callPostRewrite(theory::TheoryId theoryId, TNode node); /** - * Calls the equality-rewruter for the given theory. + * Calls the equality-rewriter for the given theory. */ static Node callRewriteEquality(theory::TheoryId theoryId, TNode equality); diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp index 0072a36e9..0d7f5005a 100644 --- a/src/theory/rewriterules/theory_rewriterules.cpp +++ b/src/theory/rewriterules/theory_rewriterules.cpp @@ -1,12 +1,11 @@ -/********************* */ -/*! \file rewrite_engine.cpp +/********************* */ +/*! \file theory_rewriterules.cpp ** \verbatim - ** Original author: ajreynolds + ** Original author: ajreynol ** Major contributors: bobot - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 - ** The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h index 499535687..e47fd2fd4 100644 --- a/src/theory/rewriterules/theory_rewriterules.h +++ b/src/theory/rewriterules/theory_rewriterules.h @@ -1,12 +1,11 @@ -/********************* */ -/*! \file rewrite_engine.h +/********************* */ +/*! \file theory_rewriterules.h ** \verbatim ** Original author: ajreynol ** Major contributors: bobot - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 - ** The Analysis of Computer Systems Group (ACSys) + ** 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 @@ -230,7 +229,7 @@ private: */ void propagateRule(const RuleInst * r, TCache cache); - /** Auxillary functions */ + /** Auxiliary functions */ private: /** A guard is verify, notify the Guarded */ void notification(GList * const lpropa, bool b); diff --git a/src/theory/rewriterules/theory_rewriterules_params.h b/src/theory/rewriterules/theory_rewriterules_params.h index ecb5385f9..9ab2ae3e7 100644 --- a/src/theory/rewriterules/theory_rewriterules_params.h +++ b/src/theory/rewriterules/theory_rewriterules_params.h @@ -1,12 +1,11 @@ -/********************* */ -/*! \file rewrite_engine.cpp +/********************* */ +/*! \file theory_rewriterules_params.h ** \verbatim ** Original author: bobot ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 - ** The Analysis of Computer Systems Group (ACSys) + ** 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 @@ -67,7 +66,7 @@ static const size_t checkSlowdown = 10; static const bool useCurrentModel = false; /** - Simulate rewritting by tagging rewritten terms. + Simulate rewriting by tagging rewritten terms. */ static const bool simulateRewritting = false; diff --git a/src/theory/rewriterules/theory_rewriterules_preprocess.h b/src/theory/rewriterules/theory_rewriterules_preprocess.h index 5d9cebfec..c90edcf27 100644 --- a/src/theory/rewriterules/theory_rewriterules_preprocess.h +++ b/src/theory/rewriterules/theory_rewriterules_preprocess.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file rewriterules.h +/*! \file theory_rewriterules_preprocess.h ** \verbatim ** Original author: bobot ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/theory/rewriterules/theory_rewriterules_rewriter.h b/src/theory/rewriterules/theory_rewriterules_rewriter.h index 3d01dc2a5..8638c49b4 100644 --- a/src/theory/rewriterules/theory_rewriterules_rewriter.h +++ b/src/theory/rewriterules/theory_rewriterules_rewriter.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file theory_rewriterules_rewriter.h + ** \verbatim + ** Original author: bobot + ** 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" #ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_REWRITER_H diff --git a/src/theory/rewriterules/theory_rewriterules_rules.cpp b/src/theory/rewriterules/theory_rewriterules_rules.cpp index 9847f1727..d66fc78cb 100644 --- a/src/theory/rewriterules/theory_rewriterules_rules.cpp +++ b/src/theory/rewriterules/theory_rewriterules_rules.cpp @@ -1,12 +1,11 @@ -/********************* */ -/*! \file rewrite_engine.cpp +/********************* */ +/*! \file theory_rewriterules_rules.cpp ** \verbatim - ** Original author: ajreynolds - ** Major contributors: bobot - ** Minor contributors (to current version): none + ** Original author: bobot + ** Major contributors: none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 - ** The Analysis of Computer Systems Group (ACSys) + ** 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 @@ -153,7 +152,7 @@ void TheoryRewriteRules::addRewriteRule(const Node r) }; break; default: - Unreachable("RewriteRules can be of only threee kinds"); + Unreachable("RewriteRules can be of only three kinds"); }; /* Add the other guards */ TNode g = r[1]; diff --git a/src/theory/rewriterules/theory_rewriterules_rules.h b/src/theory/rewriterules/theory_rewriterules_rules.h index a8e70f3e6..8610dffca 100644 --- a/src/theory/rewriterules/theory_rewriterules_rules.h +++ b/src/theory/rewriterules/theory_rewriterules_rules.h @@ -1,12 +1,11 @@ -/********************* */ -/*! \file rewrite_engine.h +/********************* */ +/*! \file theory_rewriterules_rules.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: bobot + ** Original author: bobot + ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 - ** The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/theory/rewriterules/theory_rewriterules_type_rules.h b/src/theory/rewriterules/theory_rewriterules_type_rules.h index 5a0e8c5e0..8bc4522a1 100644 --- a/src/theory/rewriterules/theory_rewriterules_type_rules.h +++ b/src/theory/rewriterules/theory_rewriterules_type_rules.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file theory_rewriterules_type_rules.h + ** \verbatim + ** Original author: bobot + ** 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" #ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_TYPE_RULES_H diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 4a6cac969..fb972b73f 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -1,15 +1,18 @@ /********************* */ -/*! \file node_visitor.h +/*! \file shared_terms_database.h ** \verbatim ** Original author: dejan - ** Major contributors: - ** Minor contributors (to current version): + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 + ** + ** [[ Add lengthier description here ]] + ** \todo document this file **/ #pragma once diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index b0b712356..ab6b27dff 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -1,15 +1,18 @@ /********************* */ -/*! \file term_registration_visitor.h +/*! \file term_registration_visitor.cpp ** \verbatim ** Original author: dejan - ** Major contributors: none - ** Minor contributors (to current version): none + ** Major contributors: mdeters + ** Minor contributors (to current version): taking, barrett ** 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 + ** + ** [[ Add lengthier description here ]] + ** \todo document this file **/ #include "theory/term_registration_visitor.h" diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h index ac3494193..c9c033bdd 100644 --- a/src/theory/term_registration_visitor.h +++ b/src/theory/term_registration_visitor.h @@ -1,15 +1,18 @@ /********************* */ -/*! \file node_visitor.h +/*! \file term_registration_visitor.h ** \verbatim ** Original author: dejan - ** Major contributors: - ** Minor contributors (to current version): + ** Major contributors: none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 + ** + ** [[ Add lengthier description here ]] + ** \todo document this file **/ #include "cvc4_private.h" @@ -109,7 +112,7 @@ class SharedTermsVisitor { SharedTermsDatabase& d_sharedTerms; /** - * Cache from proprocessing of atoms. + * Cache from preprocessing of atoms. */ typedef std::hash_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap; TNodeVisitedMap d_visited; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 0e7d7d51c..4ab2c779c 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1062,7 +1062,7 @@ static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) { Node TheoryEngine::getExplanation(TNode node) { - Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current proagation index = " << d_propagationMapTimestamp << std::endl; + Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current propagation index = " << d_propagationMapTimestamp << std::endl; bool polarity = node.getKind() != kind::NOT; TNode atom = polarity ? node : node[0]; @@ -1237,7 +1237,7 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector explanation = theoryOf(toExplain.theory)->explain(toExplain.node); } Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.theory << std::endl; - Assert(explanation != toExplain.node, "wansn't sent to you, so why are you explaining it trivially"); + Assert(explanation != toExplain.node, "wasn't sent to you, so why are you explaining it trivially"); // Mark the explanation NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp); explanationVector.push_back(newExplain); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 0452d13aa..3d70ffa6b 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -503,7 +503,7 @@ public: void preprocessStart(); /** - * Runs theory specific preprocesssing on the non-Boolean parts of + * Runs theory specific preprocessing on the non-Boolean parts of * the formula. This is only called on input assertions, after ITEs * have been removed. */ diff --git a/src/theory/theory_registrar.h b/src/theory/theory_registrar.h index 810ef1f67..372172e99 100644 --- a/src/theory/theory_registrar.h +++ b/src/theory/theory_registrar.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file registrar.h +/*! \file theory_registrar.h ** \verbatim - ** Original author: taking - ** Major contributors: mdeters + ** Original author: lianah + ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index 44f009bc0..f827b9ee7 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -19,7 +19,7 @@ #include "cvc4_public.h" #ifndef __CVC4__THEORY__THEORY_TEST_UTILS_H -#define __CVC4__THEORY__ITHEORY_TEST_UTILS_H +#define __CVC4__THEORY__THEORY_TEST_UTILS_H #include "util/Assert.h" #include "expr/node.h" diff --git a/src/theory/theoryof_mode.h b/src/theory/theoryof_mode.h index 533704a39..0ce72449d 100644 --- a/src/theory/theoryof_mode.h +++ b/src/theory/theoryof_mode.h @@ -1,19 +1,19 @@ /********************* */ -/*! \file theory.h +/*! \file theoryof_mode.h ** \verbatim ** Original author: mdeters ** Major contributors: dejan ** Minor contributors (to current version): taking, barrett ** 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 Base of the theory interface. + ** \brief Option selection for theoryOf() operation ** - ** Base of the theory interface. + ** Option selection for theoryOf() operation. **/ #pragma once @@ -29,8 +29,8 @@ enum TheoryOfMode { THEORY_OF_TYPE_BASED, /** Variables are uninterpreted, constants are with the type, equalities prefer parametric */ THEORY_OF_TERM_BASED -}; +};/* enum TheoryOfMode */ -} -} +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 54fe8e508..fe75b5f59 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file equality_engine_impl.h +/*! \file equality_engine.cpp ** \verbatim ** Original author: dejan ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): taking, mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 @@ -1701,7 +1701,7 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger // This is the class trigger set const TriggerTermSet& triggerSet = getTriggerTermSet(triggerSetRef); - // Go throught the disequalities and notify + // Go through the disequalities and notify TaggedEqualitiesSet::const_iterator it = disequalitiesToNotify.begin(); TaggedEqualitiesSet::const_iterator it_end = disequalitiesToNotify.end(); for (; !d_done && it != it_end; ++ it) { diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 5a5b62105..9228e29d4 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -142,7 +142,7 @@ public: /** - * Class for keeping an incremental congurence closure over a set of terms. It provides + * Class for keeping an incremental congruence closure over a set of terms. It provides * notifications via an EqualityEngineNotify object. */ class EqualityEngine : public context::ContextNotifyObj { @@ -226,7 +226,7 @@ private: /** Number of application lookups, for backtracking. */ context::CDO<DefaultSizeType> d_applicationLookupsCount; - /** Map from ids to the nodes (these need to be nodes as we pick-up the opreators) */ + /** Map from ids to the nodes (these need to be nodes as we pick up the operators) */ std::vector<Node> d_nodes; /** A context-dependents count of nodes */ @@ -301,7 +301,7 @@ private: /** * All the equality edges (twice as many as the number of asserted equalities. If an equality - * t1 = t2 is asserted, the edges added are -> t2, -> t1 (in this order). Hance, having the index + * t1 = t2 is asserted, the edges added are -> t2, -> t1 (in this order). Hence, having the index * of one of the edges you can reconstruct the original equality. */ std::vector<EqualityEdge> d_equalityEdges; @@ -384,7 +384,7 @@ private: std::vector<TriggerId> d_nodeTriggers; /** - * Map from ids to wheather they are constants (constants are always + * Map from ids to whether they are constants (constants are always * representatives of their class. */ std::vector<bool> d_isConstant; @@ -397,7 +397,7 @@ private: } /** - * Map from ids to wheather they are Boolean. + * Map from ids to whether they are Boolean. */ std::vector<bool> d_isBoolean; @@ -587,7 +587,7 @@ private: bool hasPropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId) const; /** - * Stores a propagated disequality for explanation purpooses and remembers the reasons. The + * Stores a propagated disequality for explanation purposes and remembers the reasons. The * reasons should be pushed on the reasons vector. */ void storePropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId); @@ -680,7 +680,7 @@ public: /** * Adds a predicate p with given polarity. The predicate asserted - * should be in the coungruence closure kinds (otherwise it's + * should be in the congruence closure kinds (otherwise it's * useless. * * @param p the (non-negated) predicate @@ -781,7 +781,7 @@ public: size_t getSize(TNode t); /** - * Returns true if the engine is in a consistents state. + * Returns true if the engine is in a consistent state. */ bool consistent() const { return !d_done; } diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h index 591b15bf4..054a6f153 100644 --- a/src/theory/uf/equality_engine_types.h +++ b/src/theory/uf/equality_engine_types.h @@ -115,7 +115,7 @@ struct DisequalityReasonRef { }; /** - * We mantaint uselist where a node appears in, and this is the node + * We maintain uselist where a node appears in, and this is the node * of such a list. */ class UseListNode { @@ -155,7 +155,7 @@ public: * Main class for representing nodes in the equivalence class. The * nodes are a circular list, with the representative carrying the * size. Each individual node carries with itself the uselist of - * functino applications it appears in and the list of asserted + * function applications it appears in and the list of asserted * disequalities it belongs to. In order to get these lists one must * traverse the entire class and pick up all the individual lists. */ diff --git a/src/theory/uf/theory_uf_candidate_generator.h b/src/theory/uf/theory_uf_candidate_generator.h index 948573439..668d619db 100644 --- a/src/theory/uf/theory_uf_candidate_generator.h +++ b/src/theory/uf/theory_uf_candidate_generator.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file theory_uf_candidate generator.h +/*! \file theory_uf_candidate_generator.h ** \verbatim ** Original author: ajreynol ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index a793b6a57..9d9be60e3 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -752,8 +752,8 @@ bool StrongSolverTheoryUf::ConflictFind::disambiguateTerms( OutputChannel* out ) } Assert( children.size()>1 ); Node lem = NodeManager::currentNM()->mkNode( OR, children ); - Debug( "uf-ss-lemma" ) << "*** Diambiguate lemma : " << lem << std::endl; - //Notice() << "*** Diambiguate lemma : " << lem << std::endl; + Debug( "uf-ss-lemma" ) << "*** Disambiguate lemma : " << lem << std::endl; + //Notice() << "*** Disambiguate lemma : " << lem << std::endl; out->lemma( lem ); d_term_amb[ eq ] = false; lemmaAdded = true; diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index e36441f6d..dde24394a 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -309,9 +309,9 @@ public: /** statistics class */ Statistics d_statistics; - /** is relavant type */ + /** is relevant type */ static bool isRelevantType( TypeNode t ); - /** involves relavant type */ + /** involves relevant type */ static bool involvesRelevantType( Node n ); };/* class StrongSolverTheoryUf */ diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp index d925a3366..58254df33 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/theory/unconstrained_simplifier.cpp @@ -523,7 +523,7 @@ void UnconstrainedSimplifier::processUnconstrained() } break; - // Array store - if both store and value are uncosntrained, so is resulting store + // Array store - if both store and value are unconstrained, so is resulting store case kind::STORE: if (((parent[0] == current && d_unconstrained.find(parent[2]) != d_unconstrained.end()) || 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); diff --git a/test/system/cvc3_george.cpp b/test/system/cvc3_george.cpp index b39477625..34ac8c2c2 100644 --- a/test/system/cvc3_george.cpp +++ b/test/system/cvc3_george.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file cvc3_main.cpp +/*! \file cvc3_george.cpp ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/test/system/cvc3_george.h b/test/system/cvc3_george.h index c904fd0c6..6f04f7bbf 100644 --- a/test/system/cvc3_george.h +++ b/test/system/cvc3_george.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file cvc3_main.cpp +/*! \file cvc3_george.h ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/test/unit/context/context_mm_black.h b/test/unit/context/context_mm_black.h index 0e5de3198..2ef74e46f 100644 --- a/test/unit/context/context_mm_black.h +++ b/test/unit/context/context_mm_black.h @@ -88,7 +88,7 @@ public: d_cmm->pop(); } - // Try poping out of scope + // Try popping out of scope d_cmm->pop(); } |