diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-20 18:16:26 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-01 16:11:24 -0400 |
commit | b6ad34343d0a09de37dc4e5ff57cd8625dca3fc4 (patch) | |
tree | d4aa8da10c6ad99c46d7f8c1fd824f2d7566ef4e /src | |
parent | cba10a096d97e82bd112b4d99a6ebe399d1369d6 (diff) |
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
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/type_checker_template.cpp | 4 | ||||
-rw-r--r-- | src/main/command_executor_portfolio.h | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 32 | ||||
-rw-r--r-- | src/theory/bv/bv_inequality_graph.cpp | 4 | ||||
-rw-r--r-- | src/theory/output_channel.h | 13 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_util.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 2 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 4 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.h | 2 | ||||
-rw-r--r-- | src/theory/uf/equality_engine_types.h | 2 | ||||
-rw-r--r-- | src/util/integer_gmp_imp.h | 4 |
11 files changed, 34 insertions, 37 deletions
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp index 4d9cbc60d..b436bad7c 100644 --- a/src/expr/type_checker_template.cpp +++ b/src/expr/type_checker_template.cpp @@ -45,7 +45,7 @@ TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check) ${typerules} -#line 46 "${template}" +#line 49 "${template}" default: Debug("getType") << "FAILURE" << std::endl; @@ -68,7 +68,7 @@ bool TypeChecker::computeIsConst(NodeManager* nodeManager, TNode n) switch(n.getKind()) { ${construles} -#line 69 "${template}" +#line 72 "${template}" default:; } diff --git a/src/main/command_executor_portfolio.h b/src/main/command_executor_portfolio.h index 0527b7f1a..bb26feef3 100644 --- a/src/main/command_executor_portfolio.h +++ b/src/main/command_executor_portfolio.h @@ -34,7 +34,7 @@ namespace main { class CommandExecutorPortfolio : public CommandExecutor { - // These shall be created/deleted during initalization + // These shall be created/deleted during initialization std::vector<ExprManager*> d_exprMgrs; const unsigned d_numThreads; // Currently const, but designed so it is // not too hard to support this changing diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2b909a9a9..d4448787f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -254,7 +254,7 @@ class SmtEnginePrivate : public NodeManagerListener { * A map of AbsractValues to their actual constants. Only used if * options::abstractValues() is on. */ - theory::SubstitutionMap d_abstractValueMap; + SubstitutionMap d_abstractValueMap; /** * A mapping of all abstract values (actual value |-> abstract) that @@ -489,7 +489,7 @@ public: /** * Return the uinterpreted function symbol corresponding to division-by-zero - * for this particular bit-wdith + * for this particular bit-width * @param k should be UREM or UDIV * @param width * @@ -695,7 +695,7 @@ void SmtEngine::finalOptionsAreSet() { setLogicInternal(); } - // finish initalization, creat the prop engine, etc. + // finish initialization, create the prop engine, etc. finishInit(); AlwaysAssert( d_propEngine->getAssertionLevel() == 0, @@ -815,11 +815,11 @@ void SmtEngine::setLogicInternal() throw() { d_logic.lock(); // may need to force uninterpreted functions to be on for non-linear - if(((d_logic.isTheoryEnabled(theory::THEORY_ARITH) && !d_logic.isLinear()) || - d_logic.isTheoryEnabled(theory::THEORY_BV)) && - !d_logic.isTheoryEnabled(theory::THEORY_UF)){ + if(((d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()) || + d_logic.isTheoryEnabled(THEORY_BV)) && + !d_logic.isTheoryEnabled(THEORY_UF)){ d_logic = d_logic.getUnlockedCopy(); - d_logic.enableTheory(theory::THEORY_UF); + d_logic.enableTheory(THEORY_UF); d_logic.lock(); } @@ -1030,7 +1030,7 @@ void SmtEngine::setLogicInternal() throw() { } // Non-linear arithmetic does not support models - if (d_logic.isTheoryEnabled(theory::THEORY_ARITH) && + if (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()) { if (options::produceModels()) { Warning() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << endl; @@ -1042,8 +1042,8 @@ void SmtEngine::setLogicInternal() throw() { } } - //datatypes theory should assign values to all datatypes terms if logic is quantified - if (d_logic.isQuantified() && d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) { + // datatypes theory should assign values to all datatypes terms if logic is quantified + if (d_logic.isQuantified() && d_logic.isTheoryEnabled(THEORY_DATATYPES)) { if( !options::dtForceAssignment.wasSetByUser() ){ options::dtForceAssignment.set(true); } @@ -1800,7 +1800,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { for( SubstitutionMap::iterator pos = d_topLevelSubstitutions.begin(); pos != d_topLevelSubstitutions.end(); ++pos) { Node n = (*pos).first; Node v = (*pos).second; - Trace("model") << "Add substitution : " << n << " " << v << std::endl; + Trace("model") << "Add substitution : " << n << " " << v << endl; m->addSubstitution( n, v ); } } @@ -2395,7 +2395,7 @@ bool SmtEnginePrivate::simplifyAssertions() // miplib rewrites aren't safe in incremental mode ! options::incrementalSolving() && // only useful in arith - d_smt.d_logic.isTheoryEnabled(theory::THEORY_ARITH) && + d_smt.d_logic.isTheoryEnabled(THEORY_ARITH) && // we add new assertions and need this (in practice, this // restriction only disables miplib processing during // re-simplification, which we don't expect to be useful anyway) @@ -2654,16 +2654,16 @@ void SmtEnginePrivate::processAssertions() { switch(booleans::BooleanTermConversionMode mode = options::booleanTermConversionMode()) { case booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS: case booleans::BOOLEAN_TERM_CONVERT_NATIVE: - if(!d_smt.d_logic.isTheoryEnabled(theory::THEORY_BV)) { + if(!d_smt.d_logic.isTheoryEnabled(THEORY_BV)) { d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); - d_smt.d_logic.enableTheory(theory::THEORY_BV); + d_smt.d_logic.enableTheory(THEORY_BV); d_smt.d_logic.lock(); } break; case booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES: - if(!d_smt.d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) { + if(!d_smt.d_logic.isTheoryEnabled(THEORY_DATATYPES)) { d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); - d_smt.d_logic.enableTheory(theory::THEORY_DATATYPES); + d_smt.d_logic.enableTheory(THEORY_DATATYPES); d_smt.d_logic.lock(); } break; 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 */ diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index 85d49f921..9a7878066 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -174,10 +174,6 @@ public: /** * Returns the Integer obtained by setting the ith bit of the * current Integer to 1. - * - * @param bit - * - * @return */ Integer setBit(uint32_t i) const { mpz_class res = d_value; |