diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2010-07-07 02:18:42 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2010-07-07 02:18:42 +0000 |
commit | daf3b024547deaf1cf53b66ed046fbb15584b9d3 (patch) | |
tree | 91a2b7ebfe804041ad531ae897a037bdde61a4a7 /src/theory/shared_term_manager.h | |
parent | 34ef50c2fcfa4d6aa8337c3096defa56d7dc0093 (diff) |
Added shared term manager. Basic mechanism for identifying shared terms is
working. Still need to implement theory-specific shared term propagation.
Diffstat (limited to 'src/theory/shared_term_manager.h')
-rw-r--r-- | src/theory/shared_term_manager.h | 86 |
1 files changed, 86 insertions, 0 deletions
diff --git a/src/theory/shared_term_manager.h b/src/theory/shared_term_manager.h new file mode 100644 index 000000000..e6a58cdc9 --- /dev/null +++ b/src/theory/shared_term_manager.h @@ -0,0 +1,86 @@ +/********************* */ +/*! \file shared_term_manager.h + ** \verbatim + ** Original author: barrett + ** Major contributors: + ** Minor contributors (to current version): + ** 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 Manager for shared terms + ** + ** Manager for shared terms. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__SHARED_TERM_MANAGER_H +#define __CVC4__SHARED_TERM_MANAGER_H + +#include "expr/node.h" +#include "theory/shared_data.h" + +namespace CVC4 { + +namespace context { + class Context; +} + +namespace theory { + class Theory; +} + +/** + * Manages shared terms + */ +class SharedTermManager { + + TheoryEngine* d_engine; + + context::Context* d_context; + + std::vector<theory::Theory*> d_theories; + + SharedData* find(SharedData* pData); + +public: + SharedTermManager(TheoryEngine* engine, context::Context* context); + + void registerTheory(theory::Theory* th); + + void addTerm(TNode n, theory::Theory* parent, + theory::Theory* child); + + void addEq(theory::Theory* thReason, TNode eq); + + Node explain(TNode eq); + +};/* class SharedTermManager */ + +/** + * Cleanup function for SharedData. This will be called whenever + * a SharedAttr is being destructed. + */ +struct SharedDataCleanupStrategy { + static void cleanup(SharedData* sd) { + sd->deleteSelf(); + } +};/* struct SharedDataCleanupStrategy */ + +/** Unique name to use for constructing ECAttr. */ +struct SharedAttrTag {}; + +/** + * SharedAttr is the attribute that maps a node to its SharedData. + */ +typedef expr::Attribute<SharedAttrTag, SharedData*, + SharedDataCleanupStrategy> SharedAttr; + + +}/* CVC4 namespace */ + +#endif /* __CVC4__SHARED_TERM_MANAGER_H */ |