diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-15 11:19:08 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-16 15:23:00 -0500 |
commit | f06ae104dc3caf9b4ff01a0b2d49b09ace88faad (patch) | |
tree | 488669992e6d375450e18a2c92659be3f93f7a88 /src/theory | |
parent | 5e29fdffd2f72212d699316f9b27e1bf9d6c715c (diff) |
Some cleanup and copyright updating
* update some copyrights for 2013
* cleaned up some comments/ifdefs, indentation
* some spelling corrections
* add some missing makefiles
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/constraint.cpp | 20 | ||||
-rw-r--r-- | src/theory/arith/constraint.h | 8 | ||||
-rw-r--r-- | src/theory/arith/delta_rational.h | 2 | ||||
-rw-r--r-- | src/theory/arith/options | 3 | ||||
-rw-r--r-- | src/theory/arith/options_handlers.h | 2 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_model.cpp | 2 | ||||
-rwxr-xr-x | src/theory/mkrewriter | 7 | ||||
-rwxr-xr-x | src/theory/mktheorytraits | 7 | ||||
-rw-r--r-- | src/theory/model.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_gen.h | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/macros.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 2 | ||||
-rw-r--r-- | src/theory/rep_set.h | 14 | ||||
-rw-r--r-- | src/theory/rewriterules/rr_candidate_generator.h | 4 | ||||
-rw-r--r-- | src/theory/rewriterules/rr_inst_match.h | 6 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 25 |
17 files changed, 61 insertions, 57 deletions
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index cf3aeafee..4655ea34e 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -371,8 +371,8 @@ void ConstraintValue::setAssertedToTheTheory(TNode witness) { d_database->pushAssertionOrderWatch(this, witness); } -// bool ConstraintValue::isPsuedoConstraint() const { -// return d_proof == d_database->d_psuedoConstraintProof; +// bool ConstraintValue::isPseudoConstraint() const { +// return d_proof == d_database->d_pseudoConstraintProof; // } bool ConstraintValue::isSelfExplaining() const { @@ -486,7 +486,7 @@ ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Co d_equalityEngineProof = d_proofs.size(); d_proofs.push_back(NullConstraint); - // d_psuedoConstraintProof = d_proofs.size(); + // d_pseudoConstraintProof = d_proofs.size(); // d_proofs.push_back(NullConstraint); } @@ -833,11 +833,11 @@ void ConstraintValue::impliedBy(const std::vector<Constraint>& b){ } } -// void ConstraintValue::setPsuedoConstraint(){ +// void ConstraintValue::setPseudoConstraint(){ // Assert(truthIsUnknown()); // Assert(!hasLiteral()); -// d_database->pushProofWatch(this, d_database->d_psuedoConstraintProof); +// d_database->pushProofWatch(this, d_database->d_pseudoConstraintProof); // } void ConstraintValue::setEqualityEngineProof(){ @@ -856,7 +856,7 @@ void ConstraintValue::markAsTrue(){ void ConstraintValue::markAsTrue(Constraint imp){ Assert(truthIsUnknown()); Assert(imp->hasProof()); - //Assert(!imp->isPsuedoConstraint()); + //Assert(!imp->isPseudoConstraint()); d_database->d_proofs.push_back(NullConstraint); d_database->d_proofs.push_back(imp); @@ -868,8 +868,8 @@ void ConstraintValue::markAsTrue(Constraint impA, Constraint impB){ Assert(truthIsUnknown()); Assert(impA->hasProof()); Assert(impB->hasProof()); - //Assert(!impA->isPsuedoConstraint()); - //Assert(!impB->isPsuedoConstraint()); + //Assert(!impA->isPseudoConstraint()); + //Assert(!impB->isPseudoConstraint()); d_database->d_proofs.push_back(NullConstraint); d_database->d_proofs.push_back(impA); @@ -886,7 +886,7 @@ void ConstraintValue::markAsTrue(const vector<Constraint>& a){ for(vector<Constraint>::const_iterator i = a.begin(), end = a.end(); i != end; ++i){ Constraint c_i = *i; Assert(c_i->hasProof()); - //Assert(!c_i->isPsuedoConstraint()); + //Assert(!c_i->isPseudoConstraint()); d_database->d_proofs.push_back(c_i); } @@ -903,7 +903,7 @@ SortedConstraintMap& ConstraintValue::constraintSet() const{ bool ConstraintValue::proofIsEmpty() const{ Assert(hasProof()); bool result = d_database->d_proofs[d_proof] == NullConstraint; - //Assert((!result) || isSelfExplaining() || hasEqualityEngineProof() || isPsuedoConstraint()); + //Assert((!result) || isSelfExplaining() || hasEqualityEngineProof() || isPseudoConstraint()); Assert((!result) || isSelfExplaining() || hasEqualityEngineProof()); return result; } diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 52aa5a5ce..82023a48b 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -273,7 +273,7 @@ private: */ AssertionOrder _d_assertionOrder; /** - * This is guarenteed to be on the fact queue. + * This is guaranteed to be on the fact queue. * For example if x + y = x + 1 is on the fact queue, then use this */ TNode d_witness; @@ -491,8 +491,8 @@ public: * The explanation is the constant true. * explainInto() does nothing. */ - //void setPsuedoConstraint(); - //bool isPsuedoConstraint() const; + //void setPseudoConstraint(); + //bool isPseudoConstraint() const; /** * Returns a explanation of the constraint that is appropriate for conflicts. @@ -709,7 +709,7 @@ private: * * This is a special proof that is always a member of the list. */ - //ProofId d_psuedoConstraintProof; + //ProofId d_pseudoConstraintProof; typedef context::CDList<Constraint, ConstraintValue::ProofCleanup> ProofCleanupList; typedef context::CDList<Constraint, ConstraintValue::CanBePropagatedCleanup> CBPList; diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index 19a16d558..51c1e5138 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -249,7 +249,7 @@ public: } /** - * Computes a sufficient upperbound to seperate two DeltaRationals. + * Computes a sufficient upperbound to separate two DeltaRationals. * This value is stored in res. * For any rational d such that * 0 < d < res diff --git a/src/theory/arith/options b/src/theory/arith/options index 9e758a0ef..efe594766 100644 --- a/src/theory/arith/options +++ b/src/theory/arith/options @@ -60,7 +60,6 @@ option arithMLTrickSubstitutions miplib-trick-subs --miplib-trick-subs unsigned option doCutAllBounded --enable-cut-all-bounded/--disable-cut-all-bounded bool :default false :read-write turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds -/ turns off the integer solving step of periodically cutting all integer variables that have both upper and lower bounds - +/turns off the integer solving step of periodically cutting all integer variables that have both upper and lower bounds endmodule diff --git a/src/theory/arith/options_handlers.h b/src/theory/arith/options_handlers.h index 52e7cbf2a..f8f851964 100644 --- a/src/theory/arith/options_handlers.h +++ b/src/theory/arith/options_handlers.h @@ -52,7 +52,7 @@ This decides on kind of propagation arithmetic attempts to do during the search. "; static const std::string heuristicPivotRulesHelp = "\ -This decides on the rule used by simplex during hueristic rounds\n\ +This decides on the rule used by simplex during heuristic rounds\n\ for deciding the next basic variable to select.\n\ Heuristic pivot rules available:\n\ +min\n\ diff --git a/src/theory/arrays/theory_arrays_model.cpp b/src/theory/arrays/theory_arrays_model.cpp index 86bdad53f..4f7584ac1 100644 --- a/src/theory/arrays/theory_arrays_model.cpp +++ b/src/theory/arrays/theory_arrays_model.cpp @@ -41,7 +41,7 @@ Node ArrayModel::getValue( TheoryModel* m, Node i ){ return it->second; }else{ return NodeManager::currentNM()->mkNode( SELECT, getArrayValue(), i ); - //return d_default_value; //TODO: guarentee I can return this here + //return d_default_value; //TODO: guarantee I can return this here } } diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter index 88ac5b9fb..2d8012bfb 100755 --- a/src/theory/mkrewriter +++ b/src/theory/mkrewriter @@ -2,7 +2,7 @@ # # mkrewriter # Morgan Deters <mdeters@cs.nyu.edu> for CVC4 -# Copyright (c) 2010-2012 The CVC4 Project +# Copyright (c) 2010-2013 The CVC4 Project # # The purpose of this script is to create rewriter_tables.h from a template # and a list of theory kinds. @@ -14,13 +14,14 @@ # Output is to standard out. # -copyright=2010-2012 +copyright=2010-2013 cat <<EOF /********************* */ /** rewriter_tables.h ** - ** Copyright $copyright The AcSys Group, New York University, and as below. + ** Copyright $copyright New York University and The University of Iowa, + ** and as below. ** ** This header file automatically generated by: ** diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index a44d8e9c3..3edc7c140 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -2,7 +2,7 @@ # # mktheorytraits # Morgan Deters <mdeters@cs.nyu.edu> for CVC4 -# Copyright (c) 2010-2012 The CVC4 Project +# Copyright (c) 2010-2013 The CVC4 Project # # The purpose of this script is to create theory_traits.h from a template # and a list of theory kinds. @@ -14,7 +14,7 @@ # Output is to standard out. # -copyright=2010-2012 +copyright=2010-2013 filename=`basename "$1" | sed 's,_template,,'` @@ -22,7 +22,8 @@ cat <<EOF /********************* */ /** $filename ** - ** Copyright $copyright The AcSys Group, New York University, and as below. + ** Copyright $copyright New York University and The University of Iowa, + ** and as below. ** ** This header file automatically generated by: ** diff --git a/src/theory/model.h b/src/theory/model.h index e283ee183..98eeda97a 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -87,7 +87,7 @@ public: void addSubstitution(TNode x, TNode t, bool invalidateCache = true); /** add term function * addTerm( n ) will do any model-specific processing necessary for n, - * such as contraining the interpretation of uninterpretted functions, + * such as constraining the interpretation of uninterpreted functions, * and adding n to the equality engine of this model */ virtual void addTerm(TNode n); diff --git a/src/theory/quantifiers/inst_gen.h b/src/theory/quantifiers/inst_gen.h index 94922df18..930133954 100644 --- a/src/theory/quantifiers/inst_gen.h +++ b/src/theory/quantifiers/inst_gen.h @@ -50,10 +50,10 @@ public: int getNumMatches() { return d_matches.size(); } bool getMatch( EqualityQuery* q, int i, InstMatch& m ); Node getMatchValue( int i ) { return d_match_values[i]; } -}; +};/* class InstGenProcess */ -} -} -} +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ -#endif +#endif /* __CVC4__THEORY__QUANTIFIERS__INST_GEN_H */ diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index 9f08764a9..bf67bdd25 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -358,7 +358,7 @@ Node QuantifierMacros::simplify( Node n ){ if( n.getKind()==APPLY_UF ){ Node op = n.getOperator(); if( d_macro_defs.find( op )!=d_macro_defs.end() && !d_macro_defs[op].isNull() ){ - //do subsitutition + //do substitution Node ret = d_macro_defs[op]; ret = ret.substitute( d_macro_basis[op].begin(), d_macro_basis[op].end(), children.begin(), children.end() ); return ret; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 9ac431107..6bfea5c44 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -167,7 +167,7 @@ public: /** get counterexample literal (for cbqi) */ Node getCounterexampleLiteral( Node f ); /** returns node n with bound vars of f replaced by instantiation constants of f - node n : is the futur pattern + node n : is the future pattern node f : is the quantifier containing which bind the variable return a pattern where the variable are replaced by variable for instantiation. diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index dc31f2d5f..019f69ec2 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__REP_SET_H -#define __CVC4__REP_SET_H +#ifndef __CVC4__THEORY__REP_SET_H +#define __CVC4__THEORY__REP_SET_H #include "expr/node.h" #include <map> @@ -45,7 +45,7 @@ public: void complete( TypeNode t ); /** debug print */ void toStream(std::ostream& out); -}; +};/* class RepSet */ //representative domain typedef std::vector< int > RepDomain; @@ -104,9 +104,9 @@ public: /** debug print */ void debugPrint( const char* c ); void debugPrintSmall( const char* c ); -}; +};/* class RepSetIterator */ -} -} +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ -#endif
\ No newline at end of file +#endif /* __CVC4__THEORY__REP_SET_H */ diff --git a/src/theory/rewriterules/rr_candidate_generator.h b/src/theory/rewriterules/rr_candidate_generator.h index 97c710219..d12c67f6a 100644 --- a/src/theory/rewriterules/rr_candidate_generator.h +++ b/src/theory/rewriterules/rr_candidate_generator.h @@ -32,7 +32,7 @@ typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator; //New CandidateGenerator. They have a simpler semantic than the old one -// Just iterate amoung the equivalence classes +// Just iterate among the equivalence classes // node::Null() must be given to reset class CandidateGeneratorTheoryEeClasses : public CandidateGenerator{ private: @@ -54,7 +54,7 @@ public: }; }; -// Just iterate amoung the equivalence class of the given node +// Just iterate among the equivalence class of the given node // node::Null() *can't* be given to reset class CandidateGeneratorTheoryEeClass : public CandidateGenerator{ private: diff --git a/src/theory/rewriterules/rr_inst_match.h b/src/theory/rewriterules/rr_inst_match.h index 63728a95b..636a4dbc1 100644 --- a/src/theory/rewriterules/rr_inst_match.h +++ b/src/theory/rewriterules/rr_inst_match.h @@ -180,7 +180,7 @@ public: /** If reset, or getNextMatch return false they remove from the InstMatch the binding that they have previously created */ - /** virtual Matcher in order to have definned behavior */ + /** virtual Matcher in order to have defined behavior */ virtual ~Matcher(){}; }; @@ -195,7 +195,7 @@ private: std::vector< triple< Matcher*, size_t, EqualityQuery* > > d_childrens; /** the variable that have been set by this matcher (during its own reset) */ std::vector< TNode > d_binded; /* TNode because the variable are already in d_pattern */ - /** the representant of the argument of the term given by the last reset */ + /** the representative of the argument of the term given by the last reset */ std::vector< Node > d_reps; public: /** The pattern we are producing matches for */ @@ -250,7 +250,7 @@ public: PatsMatcher* mkPatterns( std::vector< Node > pat, QuantifiersEngine* qe ); PatsMatcher* mkPatternsEfficient( std::vector< Node > pat, 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, TNode pat, const std::vector<Node> & vars); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index f85a5f3cd..f7f689850 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -809,7 +809,7 @@ Node TheoryEngine::preprocess(TNode assertion) { stringstream ss; ss << "The logic was specified as " << d_logicInfo.getLogicString() << ", which doesn't include " << Theory::theoryOf(current) - << ", but got a preprocesing-time fact for that theory." << endl + << ", but got a preprocessing-time fact for that theory." << endl << "The fact:" << endl << current; throw LogicException(ss.str()); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 388c0edf0..a3779f0e8 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -269,7 +269,7 @@ class TheoryEngine { void safePoint() throw(theory::Interrupted, AssertionException) { if (d_engine->d_interrupted) throw theory::Interrupted(); - } + } void conflict(TNode conflictNode) throw(AssertionException) { Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl; @@ -741,20 +741,23 @@ private: std::map< std::string, std::vector< theory::Theory* > > d_attr_handle; public: - /** Set user attribute - * This function is called when an attribute is set by a user. In SMT-LIBv2 this is done - * via the syntax (! n :attr) - */ + /** + * Set user attribute. + * This function is called when an attribute is set by a user. In SMT-LIBv2 this is done + * via the syntax (! n :attr) + */ void setUserAttribute(const std::string& attr, Node n); - /** Handle user attribute - * Associates theory t with the attribute attr. Theory t will be - * notifed whenever an attribute of name attr is set. - */ + /** + * Handle user attribute. + * Associates theory t with the attribute attr. Theory t will be + * notified whenever an attribute of name attr is set. + */ void handleUserAttribute(const char* attr, theory::Theory* t); - /** Check that the theory assertions are satisfied in the model - * This function is called from the smt engine's checkModel routine + /** + * Check that the theory assertions are satisfied in the model. + * This function is called from the smt engine's checkModel routine. */ void checkTheoryAssertionsWithModel(); |