diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-04-16 09:42:34 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-16 11:42:34 -0500 |
commit | 353bccac179f9673583c3ce559c720751ae3fa96 (patch) | |
tree | 794745ad20270cbec9235ea9885805fffdeebac1 /src/theory | |
parent | c4a2d444a601ab8131d2088065bbc8bd24ed7696 (diff) |
RemoveTermFormulas: Remove ContainsTermITEVisitor (#1782)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/ite_utilities.cpp | 15 | ||||
-rw-r--r-- | src/theory/ite_utilities.h | 58 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 9 |
3 files changed, 47 insertions, 35 deletions
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){ |