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/smt/term_formula_removal.cpp | |
parent | c4a2d444a601ab8131d2088065bbc8bd24ed7696 (diff) |
RemoveTermFormulas: Remove ContainsTermITEVisitor (#1782)
Diffstat (limited to 'src/smt/term_formula_removal.cpp')
-rw-r--r-- | src/smt/term_formula_removal.cpp | 18 |
1 files changed, 1 insertions, 17 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 |