diff options
Diffstat (limited to 'src/theory/uf/theory_uf.h')
| -rw-r--r-- | src/theory/uf/theory_uf.h | 23 |
1 files changed, 0 insertions, 23 deletions
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 11830f0e2..82597e286 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -103,13 +103,6 @@ public: };/* class TheoryUF::NotifyClass */ - /** A callback class for ppRewrite(). See registerPpRewrite(), below. */ - class PpRewrite { - public: - virtual Node ppRewrite(TNode node) = 0; - virtual ~PpRewrite() {} - };/* class TheoryUF::PpRewrite */ - private: /** The notify class */ @@ -165,12 +158,6 @@ private: /** called when two equivalence classes are made disequal */ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); - /** a registry type for keeping Node-specific callbacks for ppRewrite() */ - typedef std::hash_map<Node, PpRewrite*, NodeHashFunction> RegisterPpRewrites; - - /** a collection of callbacks to issue while doing a ppRewrite() */ - RegisterPpRewrites d_registeredPpRewrites; - public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ @@ -209,16 +196,6 @@ public: StrongSolverTheoryUF* getStrongSolver() { return d_thss; } - - Node ppRewrite(TNode node); - - /** - * Register a ppRewrite() callback on "op." TheoryUF owns - * the callback, and will delete it when it is destructed. - */ - void registerPpRewrite(TNode op, PpRewrite* callback) { - d_registeredPpRewrites.insert(std::make_pair(op, callback)); - } };/* class TheoryUF */ }/* CVC4::theory::uf namespace */ |