RemoveTermFormulas: Remove ContainsTermITEVisitor (#1782)

5 files changed, 48 insertions, 63 deletions

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 */
diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp
index 6d81dbab0..cf273a88a 100644
--- a/src/theory/ite_utilities.cpp
+++ b/src/theory/ite_utilities.cpp
@@ -79,11 +79,11 @@ struct CTIVStackElement {
 
 } /* CVC4::theory::ite */
 
-ITEUtilities::ITEUtilities(ContainsTermITEVisitor* containsVisitor)
-  : d_containsVisitor(containsVisitor)
-  , d_compressor(NULL)
-  , d_simplifier(NULL)
-  , d_careSimp(NULL)
+ITEUtilities::ITEUtilities()
+    : d_containsVisitor(new ContainsTermITEVisitor()),
+      d_compressor(NULL),
+      d_simplifier(NULL),
+      d_careSimp(NULL)
 {
   Assert(d_containsVisitor != NULL);
 }
@@ -103,7 +103,7 @@ ITEUtilities::~ITEUtilities(){
 
 Node ITEUtilities::simpITE(TNode assertion){
   if(d_simplifier == NULL){
-    d_simplifier = new ITESimplifier(d_containsVisitor);
+    d_simplifier = new ITESimplifier(d_containsVisitor.get());
   }
   return d_simplifier->simpITE(assertion);
 }
@@ -119,7 +119,7 @@ bool ITEUtilities::simpIteDidALotOfWorkHeuristic() const{
 /* returns false if an assertion is discovered to be equal to false. */
 bool ITEUtilities::compress(std::vector<Node>& assertions){
   if(d_compressor == NULL){
-     d_compressor = new ITECompressor(d_containsVisitor);
+    d_compressor = new ITECompressor(d_containsVisitor.get());
   }
   return d_compressor->compress(assertions);
 }
@@ -141,6 +141,7 @@ void ITEUtilities::clear(){
   if(d_careSimp != NULL){
     d_careSimp->clear();
   }
+  d_containsVisitor->garbageCollect();
 }
 
 /*********************                                                        */
diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h
index 096393de2..7fb3eae41 100644
--- a/src/theory/ite_utilities.h
+++ b/src/theory/ite_utilities.h
@@ -32,36 +32,12 @@
 namespace CVC4 {
 namespace theory {
 
-class ContainsTermITEVisitor;
 class IncomingArcCounter;
 class TermITEHeightCounter;
 class ITECompressor;
 class ITESimplifier;
 class ITECareSimplifier;
 
-class ITEUtilities {
-public:
-  ITEUtilities(ContainsTermITEVisitor* containsVisitor);
-  ~ITEUtilities();
-
-  Node simpITE(TNode assertion);
-
-  bool simpIteDidALotOfWorkHeuristic() const;
-
-  /* returns false if an assertion is discovered to be equal to false. */
-  bool compress(std::vector<Node>& assertions);
-
-  Node simplifyWithCare(TNode e);
-
-  void clear();
-
-private:
-  ContainsTermITEVisitor* d_containsVisitor;
-  ITECompressor* d_compressor;
-  ITESimplifier* d_simplifier;
-  ITECareSimplifier* d_careSimp;
-};
-
 /**
  * A caching visitor that computes whether a node contains a term ite.
  */
@@ -84,6 +60,40 @@ private:
   NodeBoolMap d_cache;
 };
 
+class ITEUtilities
+{
+ public:
+  ITEUtilities();
+  ~ITEUtilities();
+
+  Node simpITE(TNode assertion);
+
+  bool simpIteDidALotOfWorkHeuristic() const;
+
+  /* returns false if an assertion is discovered to be equal to false. */
+  bool compress(std::vector<Node>& assertions);
+
+  Node simplifyWithCare(TNode e);
+
+  void clear();
+
+  ContainsTermITEVisitor* getContainsVisitor()
+  {
+    return d_containsVisitor.get();
+  }
+
+  bool containsTermITE(TNode n)
+  {
+    return d_containsVisitor->containsTermITE(n);
+  }
+
+ private:
+  std::unique_ptr<ContainsTermITEVisitor> d_containsVisitor;
+  ITECompressor* d_compressor;
+  ITESimplifier* d_simplifier;
+  ITECareSimplifier* d_careSimp;
+};
+
 class IncomingArcCounter {
 public:
   IncomingArcCounter(bool skipVars = false, bool skipConstants = false);
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 38885db85..850c7ed97 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -334,7 +334,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   ProofManager::currentPM()->initTheoryProofEngine();
 #endif
 
-  d_iteUtilities = new ITEUtilities(d_tform_remover.getContainsVisitor());
+  d_iteUtilities = new ITEUtilities();
 
   smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded);
 }
@@ -2010,7 +2010,8 @@ void TheoryEngine::mkAckermanizationAssertions(std::vector<Node>& assertions) {
 
 Node TheoryEngine::ppSimpITE(TNode assertion)
 {
-  if (!d_tform_remover.containsTermITE(assertion)) {
+  if (!d_iteUtilities->containsTermITE(assertion))
+  {
     return assertion;
   } else {
     Node result = d_iteUtilities->simpITE(assertion);
@@ -2051,7 +2052,6 @@ bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){
         Chat() << "....node manager contains " << nm->poolSize() << " nodes before cleanup" << endl;
         d_iteUtilities->clear();
         Rewriter::clearCaches();
-        d_tform_remover.garbageCollect();
         nm->reclaimZombiesUntil(options::zombieHuntThreshold());
         Chat() << "....node manager contains " << nm->poolSize() << " nodes after cleanup" << endl;
       }
@@ -2062,7 +2062,8 @@ bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){
   if(d_logicInfo.isTheoryEnabled(theory::THEORY_ARITH)
      && !options::incrementalSolving() ){
     if(!simpDidALotOfWork){
-      ContainsTermITEVisitor& contains = *d_tform_remover.getContainsVisitor();
+      ContainsTermITEVisitor& contains =
+          *(d_iteUtilities->getContainsVisitor());
       arith::ArithIteUtils aiteu(contains, d_userContext, getModel());
       bool anyItes = false;
       for(size_t i = 0;  i < assertions.size(); ++i){