1 files changed, 2 insertions, 33 deletions

diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 557dcc413..38c99f551 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -18,7 +18,6 @@
 
 #include "context/context.h"
 #include "decision/decision_engine.h"
-#include "expr/expr_stream.h"
 #include "options/decision_options.h"
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
@@ -37,24 +36,17 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine,
                          TheoryEngine* theoryEngine,
                          DecisionEngine* decisionEngine,
                          context::Context* context,
-                         CnfStream* cnfStream,
-                         std::ostream* replayLog,
-                         ExprStream* replayStream)
+                         CnfStream* cnfStream)
     : d_propEngine(propEngine),
       d_cnfStream(cnfStream),
       d_decisionEngine(decisionEngine),
       d_theoryEngine(theoryEngine),
-      d_replayLog(replayLog),
-      d_replayStream(replayStream),
-      d_queue(context),
-      d_replayedDecisions("prop::theoryproxy::replayedDecisions", 0)
+      d_queue(context)
 {
-  smtStatisticsRegistry()->registerStat(&d_replayedDecisions);
 }
 
 TheoryProxy::~TheoryProxy() {
   /* nothing to do for now */
-  smtStatisticsRegistry()->unregisterStat(&d_replayedDecisions);
 }
 
 void TheoryProxy::variableNotify(SatVariable var) {
@@ -150,29 +142,6 @@ void TheoryProxy::notifyRestart() {
   d_theoryEngine->notifyRestart();
 }
 
-SatLiteral TheoryProxy::getNextReplayDecision() {
-#ifdef CVC4_REPLAY
-  if(d_replayStream != NULL) {
-    Expr e = d_replayStream->nextExpr();
-    if(!e.isNull()) { // we get null node when out of decisions to replay
-      // convert & return
-      ++d_replayedDecisions;
-      return d_cnfStream->getLiteral(e);
-    }
-  }
-#endif /* CVC4_REPLAY */
-  return undefSatLiteral;
-}
-
-void TheoryProxy::logDecision(SatLiteral lit) {
-#ifdef CVC4_REPLAY
-  if(d_replayLog != NULL) {
-    Assert(lit != undefSatLiteral) << "logging an `undef' decision ?!";
-    (*d_replayLog) << d_cnfStream->getNode(lit) << std::endl;
-  }
-#endif /* CVC4_REPLAY */
-}
-
 void TheoryProxy::spendResource(ResourceManager::Resource r)
 {
   d_theoryEngine->spendResource(r);