diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-07-07 21:01:33 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-07-07 21:01:33 +0000 |
commit | 8b01efc32d61391d8d3cd2aaac0de49cd8e88ecc (patch) | |
tree | 9e61b253a66fc91ca86b11bc1cabae9e1a7394da /src/theory | |
parent | 8166b6cef258b198d0ffc97d125da3c85acf9708 (diff) |
Various fixes to documentation---typos, some incomplete documentation fixed, \file tags corrected, copyright added to files that had it missing, etc.
I ensured that I didn't change any code with this commit, and even tested on the cluster to be doubly sure:
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4655&reference_id=4646&p=0
Diffstat (limited to 'src/theory')
59 files changed, 278 insertions, 186 deletions
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()) || |