Theory interface changes:

solve -> ppAsert
staticLearning -> ppStaticLearn
preprocess -> ppRewrite
SolveStatus -> PPAssertStatus (SOLVE_* -> PP_ASSERT_*)

via Eclipse refactoring magic.

2 files changed, 3 insertions, 3 deletions

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 2344adc70..7f5e11a64 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -282,7 +282,7 @@ void TheoryUF::presolve() {
   Debug("uf") << "uf: end presolve()" << endl;
 }
 
-void TheoryUF::staticLearning(TNode n, NodeBuilder<>& learned) {
+void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
   //TimerStat::CodeTimer codeTimer(d_staticLearningTimer);
 
   vector<TNode> workList;
@@ -393,7 +393,7 @@ void TheoryUF::staticLearning(TNode n, NodeBuilder<>& learned) {
   if(Options::current()->ufSymmetryBreaker) {
     d_symb.assertFormula(n);
   }
-}/* TheoryUF::staticLearning() */
+}/* TheoryUF::ppStaticLearn() */
 
 EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) {
   if (d_equalityEngine.areEqual(a, b)) {
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 2a02208dc..ab391e242 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -109,7 +109,7 @@ public:
   void preRegisterTerm(TNode term);
   Node explain(TNode n);
 
-  void staticLearning(TNode in, NodeBuilder<>& learned);
+  void ppStaticLearn(TNode in, NodeBuilder<>& learned);
   void presolve();
 
   void addSharedTerm(TNode n);