Theory interface changes:

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

via Eclipse refactoring magic.

2 files changed, 6 insertions, 6 deletions

diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 229a40532..3b3cde33d 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -134,11 +134,11 @@ Node TheoryBool::getValue(TNode n) {
   }
 }
 
-Theory::SolveStatus TheoryBool::solve(TNode in, SubstitutionMap& outSubstitutions) {
+Theory::PPAssertStatus TheoryBool::ppAsert(TNode in, SubstitutionMap& outSubstitutions) {
 
   if (in.getKind() == kind::CONST_BOOLEAN && !in.getConst<bool>()) {
     // If we get a false literal, we're in conflict
-    return SOLVE_STATUS_CONFLICT;
+    return PP_ASSERT_STATUS_CONFLICT;
   }
 
   // Add the substitution from the variable to it's value
@@ -146,17 +146,17 @@ Theory::SolveStatus TheoryBool::solve(TNode in, SubstitutionMap& outSubstitution
     if (in[0].getKind() == kind::VARIABLE) {
       outSubstitutions.addSubstitution(in[0], NodeManager::currentNM()->mkConst<bool>(false));
     } else {
-      return SOLVE_STATUS_UNSOLVED;
+      return PP_ASSERT_STATUS_UNSOLVED;
     }
   } else {
     if (in.getKind() == kind::VARIABLE) {
       outSubstitutions.addSubstitution(in, NodeManager::currentNM()->mkConst<bool>(true));
     } else {
-      return SOLVE_STATUS_UNSOLVED;
+      return PP_ASSERT_STATUS_UNSOLVED;
     }
   }
 
-  return SOLVE_STATUS_SOLVED;
+  return PP_ASSERT_STATUS_SOLVED;
 }
 
 
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index bd4c8d565..dd15436d8 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -36,7 +36,7 @@ public:
 
   Node getValue(TNode n);
 
-  SolveStatus solve(TNode in, SubstitutionMap& outSubstitutions);
+  PPAssertStatus ppAsert(TNode in, SubstitutionMap& outSubstitutions);
 
   std::string identify() const { return std::string("TheoryBool"); }
 };/* class TheoryBool */