summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arith/constraint.cpp20
-rw-r--r--src/theory/arith/constraint.h8
-rw-r--r--src/theory/arith/delta_rational.h2
-rw-r--r--src/theory/arith/options3
-rw-r--r--src/theory/arith/options_handlers.h2
-rw-r--r--src/theory/arrays/theory_arrays_model.cpp2
-rwxr-xr-xsrc/theory/mkrewriter7
-rwxr-xr-xsrc/theory/mktheorytraits7
-rw-r--r--src/theory/model.h2
-rw-r--r--src/theory/quantifiers/inst_gen.h10
-rw-r--r--src/theory/quantifiers/macros.cpp2
-rw-r--r--src/theory/quantifiers/term_database.h2
-rw-r--r--src/theory/rep_set.h14
-rw-r--r--src/theory/rewriterules/rr_candidate_generator.h4
-rw-r--r--src/theory/rewriterules/rr_inst_match.h6
-rw-r--r--src/theory/theory_engine.cpp2
-rw-r--r--src/theory/theory_engine.h25
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();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback