Shared term manager tested and working

It is currently tracking all asserted equalities for simplicity.
Might want to check if this is a performance hit

1 files changed, 8 insertions, 0 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index d16d80090..4fae94254 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -46,6 +46,14 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
   if (fact.getKind() == kind::NOT) {
     // No need to register negations - only atoms
     fact = fact[0];
+// FIXME: In future, might want to track disequalities in shared term manager
+//     if (fact.getKind() == kind::EQUAL) {
+//       d_engine->getSharedTermManager()->addDiseq(fact);
+//     }
+  }
+  else if (fact.getKind() == kind::EQUAL) {
+    // Automatically track all asserted equalities in the shared term manager
+    d_engine->getSharedTermManager()->addEq(fact);
   }
   if(! fact.getAttribute(RegisteredAttr())) {
     std::list<TNode> toReg;