diff options
Diffstat (limited to 'src/theory/shared_data.h')
| -rw-r--r-- | src/theory/shared_data.h | 214 |
1 files changed, 0 insertions, 214 deletions
diff --git a/src/theory/shared_data.h b/src/theory/shared_data.h deleted file mode 100644 index 7d6a9ebd2..000000000 --- a/src/theory/shared_data.h +++ /dev/null @@ -1,214 +0,0 @@ -/********************* */ -/*! \file shared_data.h - ** \verbatim - ** Original author: barrett - ** Major contributors: mdeters - ** 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 Context-dependent data class for shared terms - ** - ** Context-dependent data class for shared terms. - ** Used by SharedTermManager. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__SHARED_DATA_H -#define __CVC4__THEORY__SHARED_DATA_H - -#include "expr/node.h" -#include "context/context.h" -#include "context/cdo.h" -#include "context/context_mm.h" - -namespace CVC4 { - -namespace theory { - class Theory; -} - -/** - * SharedData is the data for shared terms and is context dependent. - * - * SharedData maintains: - * - list of theories sharing this term (as a bit-vector) - * - size of the equivalence class (valid only if it is a find-representative) - * - find pointer - * - proof tree pointer (for explanations) - * - equality associated with proof tree pointer - * - theory associated with proof tree pointer - * - the node associated with this data - * - * See also SharedAttr() in shared_term_manager.h - */ - -class SharedData : public context::ContextObj { -private: - /** - * Bit-vector representation of list of theories needing to be - * notified if this shared term is no longer the representative - */ - uint64_t d_theories; - - /** - * Size of this equivalence class - */ - unsigned d_size; - - /** - * Find pointer (standard union/find algorithm) - */ - SharedData* d_find; - - /** - * Pointer to next node (towards root) in proof forest - */ - SharedData* d_proofNext; - - /** - * In order to precisely reconstruct the equality that justifies - * this node being equal to the node at d_proofNext, we need to know - * whether this edge has been switched. Value is meaningless at the - * proof root. - */ - bool d_edgeReversed; - - /** - * The theory that can explain the equality of this node and the - * node at d_proofNext. Not valid if this is proof root. - */ - theory::Theory* d_explainingTheory; - - /** - * This is a pointer back to the node associated with this - * SharedData object. - * - * The following invariant should be maintained: - * - * (n.getAttribute(SharedAttr()))->d_rep == n - * - * i.e. rep is equal to the node that maps to the SharedData using - * SharedAttr. - */ - TNode d_rep; - - /** Context-dependent operation: save this SharedData */ - context::ContextObj* save(context::ContextMemoryManager* pCMM); - - /** Context-dependent operation: restore this SharedData */ - void restore(context::ContextObj* pContextObj); - -public: - /** - * Creates a SharedData object with the representative n - */ - SharedData(context::Context* context, TNode n, uint64_t theories); - - /** Destructor for SharedDatas */ - ~SharedData() { - destroy(); - } - - /** - * Get list of theories for this shared term - */ - uint64_t getTheories() const { return d_theories; } - - /** - * Set list of theories for this shared term - */ - void setTheories(uint64_t t) { makeCurrent(); d_theories = t; } - - /** - * Get size of equivalence class (valid if getFind() == this) - */ - unsigned getSize() const { return d_size; } - - /** - * Set size of equivalence class - */ - - void setSize(unsigned size) { makeCurrent(); d_size = size; } - - /** - * Returns the find pointer of the SharedData. If this is the - * representative of the equivalence class, then getFind() == this - */ - SharedData* getFind() const { return d_find; } - - /** - * Sets the find pointer - */ - void setFind(SharedData * pData) { makeCurrent(); d_find = pData; } - - /** - * Return true iff this is the root of the proof tree - */ - bool isProofRoot() const { return d_proofNext == this; } - - /** - * Get the next link in the proof tree - */ - SharedData* getProofNext() const { return d_proofNext; } - - /** - * Set the next link in the proof tree - */ - void setProofNext(SharedData* pData) { makeCurrent(); d_proofNext = pData; } - - /** - * Get the edge reversed property of this node - */ - bool getEdgeReversed() const { return d_edgeReversed; } - - /** - * Set the edge reversed flag to value - */ - void setEdgeReversed(bool value) { makeCurrent(); d_edgeReversed = value; } - - /** - * Get the original equality that created the link from this node to - * the next proof node. - */ - Node getEquality() const { - return d_edgeReversed - ? NodeManager::currentNM()->mkNode(kind::EQUAL, - d_proofNext->getRep(), d_rep) - : NodeManager::currentNM()->mkNode(kind::EQUAL, - d_rep, d_proofNext->getRep()); - } - - /** - * Get the explaining theory - */ - theory::Theory* getExplainingTheory() const { return d_explainingTheory; } - - /** - * Set the explaining theory - */ - void setExplainingTheory(theory::Theory* t) { - makeCurrent(); - d_explainingTheory = t; - } - - /** - * Get the shared term associated with this data - */ - Node getRep() const { return d_rep; } - - /** - * Reverse the edges in the proof tree from here to the root. - */ - void reverseEdges(); - -};/* class SharedData */ - -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__SHARED_DATA_H */ |