diff options
Diffstat (limited to 'src/theory/arith')
22 files changed, 107 insertions, 57 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 |