remove instantiator framework

(this commit was certified error- and warning-free by the test-and-commit script.)

1 files changed, 0 insertions, 9 deletions

diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index c32d6ff75..b41089b80 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -102,9 +102,6 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) {
     d_visited[current] = visitedTheories;
     Theory* th = d_engine->theoryOf(currentTheoryId);
     th->preRegisterTerm(current);
-    if(th->getInstantiator() != NULL) {
-      th->getInstantiator()->preRegisterTerm(current);
-    }
     Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl;
   }
   if (!Theory::setContains(parentTheoryId, visitedTheories)) {
@@ -112,9 +109,6 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) {
     d_visited[current] = visitedTheories;
     Theory* th = d_engine->theoryOf(parentTheoryId);
     th->preRegisterTerm(current);
-    if(th->getInstantiator() != NULL) {
-      th->getInstantiator()->preRegisterTerm(current);
-    }
     Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
   }
   if (useType) {
@@ -124,9 +118,6 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) {
       d_visited[current] = visitedTheories;
       Theory* th = d_engine->theoryOf(typeTheoryId);
       th->preRegisterTerm(current);
-      if(th->getInstantiator() != NULL) {
-        th->getInstantiator()->preRegisterTerm(current);
-      }
       Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
     }
   }