1 files changed, 0 insertions, 94 deletions
diff --git a/src/theory/shared_data.cpp b/src/theory/shared_data.cpp
deleted file mode 100644
index 3e89dec7e..000000000
--- a/src/theory/shared_data.cpp
+++ /dev/null
@@ -1,94 +0,0 @@
-/*********************                                                        */
-/*! \file shared_data.cpp
- ** \verbatim
- ** Original author: barrett
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of shared data for shared term manager.
- **
- ** Implementation of shared data used by the shared term manager.  This is a
- ** context-dependent object.
- **/
-
-
-#include "theory/shared_data.h"
-#include "theory/theory.h"
-
-
-using namespace CVC4;
-using namespace context;
-using namespace theory;
-
-
-SharedData::SharedData(Context * context, TNode n, uint64_t theories) :
-  ContextObj(context),
-  d_theories(theories),
-  d_size(1),
-  d_find(this),
-  d_proofNext(this),
-  d_edgeReversed(false),
-  d_explainingTheory(NULL),
-  d_rep(n) {
-}
-
-
-ContextObj* SharedData::save(ContextMemoryManager* pCMM) {
-  return new(pCMM) SharedData(*this);
-}
-
-
-void SharedData::restore(ContextObj* pContextObj) {
-  SharedData* data = (SharedData*)pContextObj;
-  d_theories = data->d_theories;
-  d_size = data->d_size;
-  d_find = data->d_find;
-  d_proofNext = data->d_proofNext;
-  d_edgeReversed = data->d_edgeReversed;
-  d_explainingTheory = data->d_explainingTheory;
-  d_rep = data->d_rep;
-}
-
-
-void SharedData::reverseEdges() {
-  Assert(!isProofRoot(), "reverseEdges called on proof root");
-
-  SharedData* parent = this;
-  SharedData* current = d_proofNext;
-  bool reversed = d_edgeReversed;
-  Theory* explainingTheory = d_explainingTheory;
-
-  makeCurrent();
-
-  // Make this the proof root
-  d_proofNext = this;
-  
-  // Reverse the edges from here to the former root
-  bool tmpReversed;
-  Theory* tmpTheory;
-  SharedData* tmpData;
-
-  while (!current->isProofRoot()) {
-    tmpReversed = current->getEdgeReversed();
-    current->setEdgeReversed(!reversed);
-    reversed = tmpReversed;
-
-    tmpTheory = current->getExplainingTheory();
-    current->setExplainingTheory(explainingTheory);
-    explainingTheory = tmpTheory;
-
-    tmpData = current->getProofNext();
-    current->setProofNext(parent);
-    parent = current;
-    current = tmpData;
-  }
-  current->setEdgeReversed(!reversed);
-  current->setExplainingTheory(explainingTheory);
-  current->setProofNext(parent);
-}