diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-26 16:11:00 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-26 16:11:00 +0100 |
commit | af86e5a8dc7a64fb5f7b4ca7bd3b2bedf5e8fe32 (patch) | |
tree | d86858d67279e940a225e7ca693172685532d6d7 /src/theory/uf | |
parent | aaf1bbbdc6e42910e07db64441885ee3476d86df (diff) |
Promote InstStrategyCbqi to quantifier module. Cleanup unused code.
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 27 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 23 |
2 files changed, 0 insertions, 50 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 95671d6ec..6679b5dc2 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -47,12 +47,6 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& } TheoryUF::~TheoryUF() { - // destruct all ppRewrite() callbacks - for(RegisterPpRewrites::iterator i = d_registeredPpRewrites.begin(); - i != d_registeredPpRewrites.end(); - ++i) { - delete i->second; - } delete d_thss; } @@ -544,24 +538,3 @@ void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { d_thss->assertDisequal(t1, t2, reason); } } - -Node TheoryUF::ppRewrite(TNode node) { - - if (node.getKind() != kind::APPLY_UF) { - return node; - } - - // perform the callbacks requested by TheoryUF::registerPpRewrite() - RegisterPpRewrites::iterator c = d_registeredPpRewrites.find(node.getOperator()); - if (c == d_registeredPpRewrites.end()) { - return node; - } else { - Node res = c->second->ppRewrite(node); - if (res != node) { - return ppRewrite(res); - } else { - return res; - } - } -} - 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 */ |