From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Sat, 25 Feb 2012 22:35:53 +0000 (+0000)
Subject: ppAsert -> ppAssert
X-Git-Tag: cvc5-1.0.0~8303
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8dae2b1d76de678be272df097259901463bdccbb;p=cvc5.git

ppAsert -> ppAssert
---

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 1c01c35ab..b10fc964d 100644
--- 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 9e6a725bf..c19a20ead 100644
--- 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 9ef81cc96..fd88c751a 100644
--- 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 3e12c3499..d699617e2 100644
--- 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 3b3cde33d..520adc228 100644
--- 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 dd15436d8..fedc47aeb 100644
--- 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 a67d3b7af..b0f5e4e53 100644
--- 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 578f68d54..0019b7b43 100644
--- 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;
 }