Added shared term manager. Basic mechanism for identifying shared terms is

working.  Still need to implement theory-specific shared term propagation.

1 files changed, 90 insertions, 0 deletions

diff --git a/src/theory/shared_data.cpp b/src/theory/shared_data.cpp
new file mode 100644
index 000000000..678595f5f
--- /dev/null
+++ b/src/theory/shared_data.cpp
@@ -0,0 +1,90 @@
+/*********************                                                        */
+/*! \file shared_data.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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 equivalence class data for UF theory.
+ **
+ ** Implementation of equivalence class data for UF theory.  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_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_equality = data->d_equality;
+  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;
+  Node equality = d_equality;
+  Theory* explainingTheory = d_explainingTheory;
+
+  makeCurrent();
+  d_proofNext = this;
+  
+  Node tmpNode;
+  Theory* tmpTheory;
+  SharedData* tmpData;
+
+  while (!current->isProofRoot()) {
+    tmpNode = current->getEquality();
+    current->setEquality(equality);
+    equality = tmpNode;
+
+    tmpTheory = current->getExplainingTheory();
+    current->setExplainingTheory(explainingTheory);
+    explainingTheory = tmpTheory;
+
+    tmpData = current->getProofNext();
+    current->setProofNext(parent);
+    parent = current;
+    current = tmpData;
+  }
+  current->setEquality(equality);
+  current->setExplainingTheory(explainingTheory);
+  current->setProofNext(parent);
+}