Theory interface changes:

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

via Eclipse refactoring magic.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 12288e40aaf8f8d01b877db369b6194d2d5ee56f..5a7209c409b4c73286375c3ee015c29376f098b6 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -622,7 +622,7 @@ void SmtEnginePrivate::staticLearning() {
 
     NodeBuilder<> learned(kind::AND);
     learned << d_assertionsToCheck[i];
-    d_smt.d_theoryEngine->staticLearning(d_assertionsToCheck[i], learned);
+    d_smt.d_theoryEngine->ppStaticLearn(d_assertionsToCheck[i], learned);
     if(learned.getNumChildren() == 1) {
       learned.clear();
     } else {
@@ -689,10 +689,10 @@ void SmtEnginePrivate::nonClausalSimplify() {
       // Solve it with the corresponding theory
       Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                         << "solving " << learnedLiteral << endl;
-      Theory::SolveStatus solveStatus =
+      Theory::PPAssertStatus solveStatus =
         d_smt.d_theoryEngine->solve(learnedLiteral, d_topLevelSubstitutions);
       switch (solveStatus) {
-      case Theory::SOLVE_STATUS_CONFLICT:
+      case Theory::PP_ASSERT_STATUS_CONFLICT:
         // If in conflict, we return false
         Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                           << "conflict while solving "
@@ -700,7 +700,7 @@ void SmtEnginePrivate::nonClausalSimplify() {
         d_assertionsToPreprocess.clear();
         d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
         return;
-      case Theory::SOLVE_STATUS_SOLVED:
+      case Theory::PP_ASSERT_STATUS_SOLVED:
         // The literal should rewrite to true
         Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                           << "solved " << learnedLiteral << endl;

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index ec5752d3a6bf0575fda6c5c71deb9f4eb5be4a82..1c01c35ab9ce25e04eda00d96c1696e0be44ee31 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -141,7 +141,7 @@ void TheoryArith::addSharedTerm(TNode n){
   d_differenceManager.addSharedTerm(n);
 }
 
-Node TheoryArith::preprocess(TNode atom) {
+Node TheoryArith::ppRewrite(TNode atom) {
   Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
 
   Node a = d_pbSubstitutions.apply(atom);
@@ -167,7 +167,7 @@ Node TheoryArith::preprocess(TNode atom) {
   return a;
 }
 
-Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutions) {
+Theory::PPAssertStatus TheoryArith::ppAsert(TNode in, SubstitutionMap& outSubstitutions) {
   TimerStat::CodeTimer codeTimer(d_statistics.d_simplifyTimer);
   Debug("simplify") << "TheoryArith::solve(" << in << ")" << endl;
 
@@ -220,7 +220,7 @@ Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutio
           // substitution is integral
           Debug("simplify") << "TheoryArith::solve(): substitution " << minVar << " |-> " << elim << endl;
           outSubstitutions.addSubstitution(minVar, elim);
-          return SOLVE_STATUS_SOLVED;
+          return PP_ASSERT_STATUS_SOLVED;
         } else {
           Debug("simplify") << "TheoryArith::solve(): can't substitute b/c it's integer: " << minVar << ":" << minVar.getType() << " |-> " << elim << ":" << elim.getType() << endl;
         }
@@ -243,10 +243,10 @@ Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutio
     break;
   }
 
-  return SOLVE_STATUS_UNSOLVED;
+  return PP_ASSERT_STATUS_UNSOLVED;
 }
 
-void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) {
+void TheoryArith::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
   TimerStat::CodeTimer codeTimer(d_statistics.d_staticLearningTimer);
 
   d_learner.staticLearning(n, learned);

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 256a197cdd5e8bbc3f1320bd3e6e89aea439fdc9..9e6a725bfd605c9a7af1700dc9ff00053be2419f 100644 (file)
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -268,9 +268,9 @@ public:
 
   void presolve();
   void notifyRestart();
-  SolveStatus solve(TNode in, SubstitutionMap& outSubstitutions);
-  Node preprocess(TNode atom);
-  void staticLearning(TNode in, NodeBuilder<>& learned);
+  PPAssertStatus ppAsert(TNode in, SubstitutionMap& outSubstitutions);
+  Node ppRewrite(TNode atom);
+  void ppStaticLearn(TNode in, NodeBuilder<>& learned);
 
   std::string identify() const { return std::string("TheoryArith"); }
 

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 601805343748a5d42832865ca7c8d61ef25cc51a..9ef81cc967f92136f2fa127330196c7fe366ae28 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -187,18 +187,18 @@ Node TheoryArrays::getValue(TNode n) {
   }
 }
 
-Theory::SolveStatus TheoryArrays::solve(TNode in, SubstitutionMap& outSubstitutions) {
+Theory::PPAssertStatus TheoryArrays::ppAsert(TNode in, SubstitutionMap& outSubstitutions) {
   switch(in.getKind()) {
     case kind::EQUAL:
     {
       d_staticFactManager.addEq(in);
       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;
       }
       break;
     }
@@ -214,7 +214,7 @@ Theory::SolveStatus TheoryArrays::solve(TNode in, SubstitutionMap& outSubstituti
     default:
       break;
   }
-  return SOLVE_STATUS_UNSOLVED;
+  return PP_ASSERT_STATUS_UNSOLVED;
 }
 
 Node TheoryArrays::preprocessTerm(TNode term) {
@@ -382,7 +382,7 @@ Node TheoryArrays::recursivePreprocessTerm(TNode term) {
   return newTerm;
 }
 
-Node TheoryArrays::preprocess(TNode atom) {
+Node TheoryArrays::ppRewrite(TNode atom) {
   if (d_donePreregister) return atom;
   Assert(atom.getKind() == kind::EQUAL, "expected EQUAL, got %s", atom.toString().c_str());
   return recursivePreprocessTerm(atom);

diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 366c2d3f703120d5e70700ada92545bcadef6da9..3e12c3499565d67ccaa7b4285a9d53018c1ace15 100644 (file)
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -479,8 +479,8 @@ public:
   Node explain(TNode n);
 
   Node getValue(TNode n);
-  SolveStatus solve(TNode in, SubstitutionMap& outSubstitutions);
-  Node preprocess(TNode atom);
+  PPAssertStatus ppAsert(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 229a40532b0104dc2ef70c96a3dac31e6c6c6160..3b3cde33d8dd20ee35dc1b4dd36cace09af3526b 100644 (file)
--- 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 bd4c8d56574f038b56695713f362bc5b2113b815..dd15436d8281fa2ffa37ddf5c477e0ed7d3175b2 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);
 
-  SolveStatus solve(TNode in, SubstitutionMap& outSubstitutions);
+  PPAssertStatus ppAsert(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 fade1e3c777677026d976655d89c2ca3044a34aa..a67d3b7afe941ba421847a1391ed76a4f1a10760 100644 (file)
--- 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();

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 3486d9075fee0fa71745fd74825770a3cd8946c9..578f68d54e46edac295747de49e8a905319d8f1e 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -442,7 +442,7 @@ void TheoryEngine::notifyRestart() {
   CVC4_FOR_EACH_THEORY;
 }
 
-void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) {
+void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
   // NOTE that we don't look at d_theoryIsActive[] here.  First of
   // all, we haven't done any pre-registration yet, so we don't know
   // which theories are active.  Second, let's give each theory a shot
@@ -455,7 +455,7 @@ void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) {
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
   if (theory::TheoryTraits<THEORY>::hasStaticLearning) { \
-    reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->staticLearning(in, learned); \
+    reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->ppStaticLearn(in, learned); \
   }
 
   // static learning for each theory using the statement above
@@ -478,10 +478,10 @@ void TheoryEngine::shutdown() {
   theory::Rewriter::shutdown();
 }
 
-theory::Theory::SolveStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) {
+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::SolveStatus solveStatus = theoryOf(atom)->solve(literal, substitutionOut);
+  Theory::PPAssertStatus solveStatus = theoryOf(atom)->ppAsert(literal, substitutionOut);
   Trace("theory::solve") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << endl;
   return solveStatus;
 }
@@ -519,7 +519,7 @@ Node TheoryEngine::preprocess(TNode assertion) {
 
     // If this is an atom, we preprocess it with the theory
     if (Theory::theoryOf(current) != THEORY_BOOL) {
-      d_atomPreprocessingCache[current] = theoryOf(current)->preprocess(current);
+      d_atomPreprocessingCache[current] = theoryOf(current)->ppRewrite(current);
       continue;
     }
 

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 2c1c9a436788c818b0558e0276257fbef9e45c6e..ceefa88e8f662e31db155a14f9317565b22d1faf 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -507,7 +507,7 @@ public:
   /**
    * Solve the given literal with a theory that owns it.
    */
-  theory::Theory::SolveStatus solve(TNode literal,
+  theory::Theory::PPAssertStatus solve(TNode literal,
                                     theory::SubstitutionMap& substitutionOut);
 
   /**
@@ -543,10 +543,10 @@ public:
   void combineTheories();
 
   /**
-   * Calls staticLearning() on all theories, accumulating their
+   * Calls ppStaticLearn() on all theories, accumulating their
    * combined contributions in the "learned" builder.
    */
-  void staticLearning(TNode in, NodeBuilder<>& learned);
+  void ppStaticLearn(TNode in, NodeBuilder<>& learned);
 
   /**
    * Calls presolve() on all theories and returns true

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 2344adc703f9d0ade9b0c100a19e8060a926a0eb..7f5e11a642098e65f17a9b49942a27b72df9df09 100644 (file)
--- 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 2a02208dc6d6c1f449dc319d85dfc7f2917cfb8b..ab391e242c5c422703faff4b8ee8c40c7f18ce1b 100644 (file)
--- 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);