ppAsert -> ppAssert

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 1c01c35ab9ce25e04eda00d96c1696e0be44ee31..b10fc964dc03627092fc474f611855846a947379 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -167,7 +167,7 @@ Node TheoryArith::ppRewrite(TNode atom) {
   return a;
 }
 
-Theory::PPAssertStatus TheoryArith::ppAsert(TNode in, SubstitutionMap& outSubstitutions) {
+Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
   TimerStat::CodeTimer codeTimer(d_statistics.d_simplifyTimer);
   Debug("simplify") << "TheoryArith::solve(" << in << ")" << endl;
 

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 9e6a725bfd605c9a7af1700dc9ff00053be2419f..c19a20eadff43ce9064f13b6c4a68ec0f2063be0 100644 (file)
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -268,7 +268,7 @@ public:
 
   void presolve();
   void notifyRestart();
-  PPAssertStatus ppAsert(TNode in, SubstitutionMap& outSubstitutions);
+  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
   Node ppRewrite(TNode atom);
   void ppStaticLearn(TNode in, NodeBuilder<>& learned);
 

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 9ef81cc967f92136f2fa127330196c7fe366ae28..fd88c751a23ad27d2442888b61898dc2d2aa92ca 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -187,7 +187,7 @@ Node TheoryArrays::getValue(TNode n) {
   }
 }
 
-Theory::PPAssertStatus TheoryArrays::ppAsert(TNode in, SubstitutionMap& outSubstitutions) {
+Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
   switch(in.getKind()) {
     case kind::EQUAL:
     {

diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 3e12c3499565d67ccaa7b4285a9d53018c1ace15..d699617e216c61985ff5f4444e292a75b993b9a4 100644 (file)
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -479,7 +479,7 @@ public:
   Node explain(TNode n);
 
   Node getValue(TNode n);
-  PPAssertStatus ppAsert(TNode in, SubstitutionMap& outSubstitutions);
+  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
   Node ppRewrite(TNode atom);
   void shutdown() { }
   std::string identify() const { return std::string("TheoryArrays"); }

diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 3b3cde33d8dd20ee35dc1b4dd36cace09af3526b..520adc228c79ca8e5865f4c4893aadb2eeb4c421 100644 (file)
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -134,7 +134,7 @@ Node TheoryBool::getValue(TNode n) {
   }
 }
 
-Theory::PPAssertStatus TheoryBool::ppAsert(TNode in, SubstitutionMap& outSubstitutions) {
+Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
 
   if (in.getKind() == kind::CONST_BOOLEAN && !in.getConst<bool>()) {
     // If we get a false literal, we're in conflict

diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index dd15436d8281fa2ffa37ddf5c477e0ed7d3175b2..fedc47aeb8f270c4254a6829fba08551fa671f80 100644 (file)
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -36,7 +36,7 @@ public:
 
   Node getValue(TNode n);
 
-  PPAssertStatus ppAsert(TNode in, SubstitutionMap& outSubstitutions);
+  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
 
   std::string identify() const { return std::string("TheoryBool"); }
 };/* class TheoryBool */

diff --git a/src/theory/theory.h b/src/theory/theory.h
index a67d3b7afe941ba421847a1391ed76a4f1a10760..b0f5e4e539cc80fb066d2b7d178430d29b515869 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -478,7 +478,7 @@ public:
    * Given a literal, add the solved substitutions to the map, if any.
    * The method should return true if the literal can be safely removed.
    */
-  virtual PPAssertStatus ppAsert(TNode in, SubstitutionMap& outSubstitutions) {
+  virtual PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
     if (in.getKind() == kind::EQUAL) {
       if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) {
         outSubstitutions.addSubstitution(in[0], in[1]);

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 578f68d54e46edac295747de49e8a905319d8f1e..0019b7b43c27829d81a7c9a7a1c581aed58a8521 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -481,7 +481,7 @@ void TheoryEngine::shutdown() {
 theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) {
   TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
   Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl;
-  Theory::PPAssertStatus solveStatus = theoryOf(atom)->ppAsert(literal, substitutionOut);
+  Theory::PPAssertStatus solveStatus = theoryOf(atom)->ppAssert(literal, substitutionOut);
   Trace("theory::solve") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << endl;
   return solveStatus;
 }