diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-09-15 06:53:33 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-09-15 06:53:33 +0000 |
commit | 72f552ead344b13d90832222157b970ae3dec8ff (patch) | |
tree | b02854356d5c5f98b3873f858f38b6762135bdc1 /src/theory/shared_data.cpp | |
parent | 62a50760346e130345b24e8a14ad0dac0dca5d38 (diff) |
additional stuff for sharing,
Diffstat (limited to 'src/theory/shared_data.cpp')
-rw-r--r-- | src/theory/shared_data.cpp | 94 |
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); -} |