1 files changed, 15 insertions, 15 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index fade1e3c7..a67d3b7af 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -463,39 +463,39 @@ public:
    * *never* clear it.  It is a conjunction to add to the formula at
    * the top-level and may contain other theories' contributions.
    */
-  virtual void staticLearning(TNode in, NodeBuilder<>& learned) { }
+  virtual void ppStaticLearn(TNode in, NodeBuilder<>& learned) { }
 
-  enum SolveStatus {
+  enum PPAssertStatus {
     /** Atom has been solved  */
-    SOLVE_STATUS_SOLVED,
+    PP_ASSERT_STATUS_SOLVED,
     /** Atom has not been solved */
-    SOLVE_STATUS_UNSOLVED,
+    PP_ASSERT_STATUS_UNSOLVED,
     /** Atom is inconsistent */
-    SOLVE_STATUS_CONFLICT
+    PP_ASSERT_STATUS_CONFLICT
   };
 
   /**
    * 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 SolveStatus solve(TNode in, SubstitutionMap& outSubstitutions) {
+  virtual PPAssertStatus ppAsert(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]);
-        return SOLVE_STATUS_SOLVED;
+        return PP_ASSERT_STATUS_SOLVED;
       }
       if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) {
         outSubstitutions.addSubstitution(in[1], in[0]);
-        return SOLVE_STATUS_SOLVED;
+        return PP_ASSERT_STATUS_SOLVED;
       }
       if (in[0].getMetaKind() == kind::metakind::CONSTANT && in[1].getMetaKind() == kind::metakind::CONSTANT) {
         if (in[0] != in[1]) {
-          return SOLVE_STATUS_CONFLICT;
+          return PP_ASSERT_STATUS_CONFLICT;
         }
       }
     }
 
-    return SOLVE_STATUS_UNSOLVED;
+    return PP_ASSERT_STATUS_UNSOLVED;
   }
 
   /**
@@ -504,7 +504,7 @@ public:
    * the atom into an equivalent form.  This is only called just
    * before an input atom to the engine.
    */
-  virtual Node preprocess(TNode atom) { return atom; }
+  virtual Node ppRewrite(TNode atom) { return atom; }
 
   /**
    * A Theory is called with presolve exactly one time per user
@@ -639,13 +639,13 @@ inline std::ostream& operator<<(std::ostream& out,
   return out << theory.identify();
 }
 
-inline std::ostream& operator << (std::ostream& out, theory::Theory::SolveStatus status) {
+inline std::ostream& operator << (std::ostream& out, theory::Theory::PPAssertStatus status) {
   switch (status) {
-  case theory::Theory::SOLVE_STATUS_SOLVED:
+  case theory::Theory::PP_ASSERT_STATUS_SOLVED:
     out << "SOLVE_STATUS_SOLVED"; break;
-  case theory::Theory::SOLVE_STATUS_UNSOLVED:
+  case theory::Theory::PP_ASSERT_STATUS_UNSOLVED:
     out << "SOLVE_STATUS_UNSOLVED"; break;
-  case theory::Theory::SOLVE_STATUS_CONFLICT:
+  case theory::Theory::PP_ASSERT_STATUS_CONFLICT:
     out << "SOLVE_STATUS_CONFLICT"; break;
   default:
     Unhandled();