From b6ad34343d0a09de37dc4e5ff57cd8625dca3fc4 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 20 Mar 2013 18:16:26 -0400 Subject: Merging some cleanup work: * Comment cleanup * Spelling fixes * Fix warnings * Documentation updates * References in docs to cryptominisat removed * Unneeded scope resolutions removed * Old, unused regression removed --- src/theory/bv/bv_inequality_graph.cpp | 4 ++-- src/theory/output_channel.h | 13 +++++++------ src/theory/quantifiers/quant_util.h | 2 +- src/theory/quantifiers/term_database.h | 2 +- src/theory/uf/equality_engine.cpp | 4 ++-- src/theory/uf/equality_engine.h | 2 +- src/theory/uf/equality_engine_types.h | 2 +- 7 files changed, 15 insertions(+), 14 deletions(-) (limited to 'src/theory') diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp index 499d362a9..ec4b223cf 100644 --- a/src/theory/bv/bv_inequality_graph.cpp +++ b/src/theory/bv/bv_inequality_graph.cpp @@ -30,7 +30,7 @@ const ReasonId CVC4::theory::bv::AxiomReasonId = -2; bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason) { - Debug("bv-inequality") << "InequlityGraph::addInequality " << a << " " << b << " strict: " << strict << "\n"; + Debug("bv-inequality") << "InequalityGraph::addInequality " << a << " " << b << " strict: " << strict << "\n"; TermId id_a = registerTerm(a); TermId id_b = registerTerm(b); @@ -121,7 +121,7 @@ bool InequalityGraph::processQueue(BFSQueue& queue, TermId start) { while (!queue.empty()) { TermId current = queue.top(); queue.pop(); - Debug("bv-inequality-internal") << "InequalityGraph::processQueue proceessing " << getTermNode(current) << "\n"; + Debug("bv-inequality-internal") << "InequalityGraph::processQueue processing " << getTermNode(current) << "\n"; BitVector current_value = getValue(current); diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 2ea92635e..ca22f29b6 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -208,12 +208,13 @@ public: */ virtual void spendResource() throw() {} - /** Handle user attribute - * Associates theory t with the attribute attr. Theory t will be - * notifed whenever an attribute of name attr is set on a node. - * This can happen through, for example, the SMT LIB v2 language. - */ - virtual void handleUserAttribute( const char* attr, Theory* t ){} + /** + * Handle user attribute. + * Associates theory t with the attribute attr. Theory t will be + * notified whenever an attribute of name attr is set on a node. + * This can happen through, for example, the SMT-LIBv2 language. + */ + virtual void handleUserAttribute(const char* attr, Theory* t) {} };/* class OutputChannel */ diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 0b4f2654b..187587227 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -31,7 +31,7 @@ namespace theory { class QuantRelevance { private: - /** for computing relavance */ + /** for computing relevance */ bool d_computeRel; /** map from quantifiers to symbols they contain */ std::map< Node, std::vector< Node > > d_syms; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 6bfea5c44..e232a382e 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -212,7 +212,7 @@ private: std::map< TNode, std::vector< TNode > > d_var_contains; /** triggers for each operator */ std::map< Node, std::vector< inst::Trigger* > > d_op_triggers; - /** helper for is intance of */ + /** helper for is instance of */ bool isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs ); public: /** compute var contains */ diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 45f161143..016abb2ac 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -291,7 +291,7 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) { d_subtermsToEvaluate[result] = t.getNumChildren(); for (unsigned i = 0; i < t.getNumChildren(); ++ i) { if (isConstant(getNodeId(t[i]))) { - Debug("equality::evaluation") << d_name << "::eq::addTermInternal(" << t << "): evaluatates " << t[i] << std::endl; + Debug("equality::evaluation") << d_name << "::eq::addTermInternal(" << t << "): evaluates " << t[i] << std::endl; subtermEvaluates(result); } } @@ -390,7 +390,7 @@ void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason) { } void EqualityEngine::mergePredicates(TNode p, TNode q, TNode reason) { - Debug("equality") << d_name << "::eq::mergePredicats(" << p << "," << q << ")" << std::endl; + Debug("equality") << d_name << "::eq::mergePredicates(" << p << "," << q << ")" << std::endl; assertEqualityInternal(p, q, reason); propagate(); } diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 2373c7f9a..34cb2443f 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -727,7 +727,7 @@ public: } /** - * Returns true if this kind is used for congruencce closure + evaluation of constants. + * Returns true if this kind is used for congruence closure + evaluation of constants. */ bool isInterpretedFunctionKind(Kind fun) const { return d_congruenceKindsInterpreted.tst(fun); diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h index f993b941b..9caa8b1f1 100644 --- a/src/theory/uf/equality_engine_types.h +++ b/src/theory/uf/equality_engine_types.h @@ -282,7 +282,7 @@ enum FunctionApplicationType { struct FunctionApplication { /** Type of application */ FunctionApplicationType type; - /** The actuall application elements */ + /** The actual application elements */ EqualityNodeId a, b; /** Construct an application */ -- cgit v1.2.3