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/theory_engine.cpp | |
| parent | c4a2d444a601ab8131d2088065bbc8bd24ed7696 (diff) | |
RemoveTermFormulas: Remove ContainsTermITEVisitor (#1782)
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 9 |
1 files changed, 5 insertions, 4 deletions
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){ |