From 353bccac179f9673583c3ce559c720751ae3fa96 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 16 Apr 2018 09:42:34 -0700
Subject: RemoveTermFormulas: Remove ContainsTermITEVisitor (#1782)

---
 src/smt/term_formula_removal.cpp | 18 +-----------------
 src/smt/term_formula_removal.h   | 11 -----------
 2 files changed, 1 insertion(+), 28 deletions(-)

(limited to 'src/smt')

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index fc10d2b4b..ad01848cc 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -19,7 +19,6 @@
 
 #include "options/proof_options.h"
 #include "proof/proof_manager.h"
-#include "theory/ite_utilities.h"
 
 using namespace std;
 
@@ -28,20 +27,9 @@ namespace CVC4 {
 RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u)
     : d_tfCache(u), d_skolem_cache(u)
 {
-  d_containsVisitor = new theory::ContainsTermITEVisitor();
 }
 
-RemoveTermFormulas::~RemoveTermFormulas(){
-  delete d_containsVisitor;
-}
-
-void RemoveTermFormulas::garbageCollect(){
-  d_containsVisitor->garbageCollect();
-}
-
-theory::ContainsTermITEVisitor* RemoveTermFormulas::getContainsVisitor() {
-  return d_containsVisitor;
-}
+RemoveTermFormulas::~RemoveTermFormulas() {}
 
 void RemoveTermFormulas::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps)
 {
@@ -65,10 +53,6 @@ void RemoveTermFormulas::run(std::vector<Node>& output, IteSkolemMap& iteSkolemM
   }
 }
 
-bool RemoveTermFormulas::containsTermITE(TNode e) const {
-  return d_containsVisitor->containsTermITE(e);
-}
-
 Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
                     IteSkolemMap& iteSkolemMap, bool inQuant, bool inTerm) {
   // Current node
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index 63a74a332..49f2e815f 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -30,10 +30,6 @@
 
 namespace CVC4 {
 
-namespace theory {
-  class ContainsTermITEVisitor;
-}/* CVC4::theory namespace */
-
 typedef std::unordered_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
 
 class RemoveTermFormulas {
@@ -151,13 +147,6 @@ public:
 
   /** Garbage collects non-context dependent data-structures. */
   void garbageCollect();
-
-  /** Return the RemoveTermFormulas's containsVisitor. */
-  theory::ContainsTermITEVisitor* getContainsVisitor();
-
-private:
-  theory::ContainsTermITEVisitor* d_containsVisitor;
-
 };/* class RemoveTTE */
 
 }/* CVC4 namespace */
-- 
cgit v1.2.3