From 353bccac179f9673583c3ce559c720751ae3fa96 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 16 Apr 2018 09:42:34 -0700 Subject: [PATCH] RemoveTermFormulas: Remove ContainsTermITEVisitor (#1782) --- src/smt/term_formula_removal.cpp | 18 +--------- src/smt/term_formula_removal.h | 11 ------ src/theory/ite_utilities.cpp | 15 +++++---- src/theory/ite_utilities.h | 58 +++++++++++++++++++------------- src/theory/theory_engine.cpp | 9 ++--- 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& output, IteSkolemMap& iteSkolemMap, bool reportDeps) { @@ -65,10 +53,6 @@ void RemoveTermFormulas::run(std::vector& output, IteSkolemMap& iteSkolemM } } -bool RemoveTermFormulas::containsTermITE(TNode e) const { - return d_containsVisitor->containsTermITE(e); -} - Node RemoveTermFormulas::run(TNode node, std::vector& 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 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& 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& 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& 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 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& 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& 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& 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){ -- 2.30.2