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/theory_engine.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/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 35 |
1 files changed, 29 insertions, 6 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index f467d0d8f..bb9131023 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -26,6 +26,7 @@ #include "theory/theoryof_table.h" #include "prop/prop_engine.h" +#include "theory/shared_term_manager.h" #include "theory/builtin/theory_builtin.h" #include "theory/booleans/theory_bool.h" #include "theory/uf/theory_uf.h" @@ -122,6 +123,9 @@ class TheoryEngine { EngineOutputChannel d_theoryOut; + /** Pointer to Shared Term Manager */ + SharedTermManager* d_sharedTermManager; + theory::builtin::TheoryBuiltin d_builtin; theory::booleans::TheoryBool d_bool; theory::uf::TheoryUF d_uf; @@ -192,14 +196,23 @@ public: TheoryEngine(context::Context* ctxt) : d_propEngine(NULL), d_theoryOut(this, ctxt), - d_builtin(ctxt, d_theoryOut), - d_bool(ctxt, d_theoryOut), - d_uf(ctxt, d_theoryOut), - d_arith(ctxt, d_theoryOut), - d_arrays(ctxt, d_theoryOut), - d_bv(ctxt, d_theoryOut), + d_builtin(0, ctxt, d_theoryOut), + d_bool(1, ctxt, d_theoryOut), + d_uf(2, ctxt, d_theoryOut), + d_arith(3, ctxt, d_theoryOut), + d_arrays(4, ctxt, d_theoryOut), + d_bv(5, ctxt, d_theoryOut), d_statistics() { + d_sharedTermManager = new SharedTermManager(this, ctxt); + + d_sharedTermManager->registerTheory(&d_builtin); + d_sharedTermManager->registerTheory(&d_bool); + d_sharedTermManager->registerTheory(&d_uf); + d_sharedTermManager->registerTheory(&d_arith); + d_sharedTermManager->registerTheory(&d_arrays); + d_sharedTermManager->registerTheory(&d_bv); + d_theoryOfTable.registerTheory(&d_builtin); d_theoryOfTable.registerTheory(&d_bool); d_theoryOfTable.registerTheory(&d_uf); @@ -208,6 +221,10 @@ public: d_theoryOfTable.registerTheory(&d_bv); } + SharedTermManager* getSharedTermManager() { + return d_sharedTermManager; + } + void setPropEngine(prop::PropEngine* propEngine) { Assert(d_propEngine == NULL); @@ -226,6 +243,7 @@ public: d_arith.shutdown(); d_arrays.shutdown(); d_bv.shutdown(); + delete d_sharedTermManager; } /** @@ -314,6 +332,11 @@ public: //d_bv.propagate(theory::Theory::FULL_EFFORT); } + inline Node getExplanation(TNode node, theory::Theory* theory) { + theory->explain(node); + return d_theoryOut.d_explanationNode; + } + inline Node getExplanation(TNode node){ d_theoryOut.d_explanationNode = Node::null(); theory::Theory* theory = |