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