Promote InstStrategyCbqi to quantifier module. Cleanup unused code.

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 */