diff options
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/equality_engine.cpp | 8 | ||||
| -rw-r--r-- | src/theory/uf/equality_engine.h | 16 | ||||
| -rw-r--r-- | src/theory/uf/equality_engine_types.h | 4 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf_candidate_generator.h | 6 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 4 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf_strong_solver.h | 4 |
6 files changed, 21 insertions, 21 deletions
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 */ |