1 files changed, 0 insertions, 43 deletions
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index 810cd1d39..489c97e67 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -26,49 +26,6 @@ namespace CVC4 {
 namespace theory {
 namespace builtin {
 
-Node TheoryBuiltin::blastDistinct(TNode in) {
-  Debug("theory-rewrite") << "TheoryBuiltin::blastDistinct: "
-                          << in << std::endl;
-  Assert(in.getKind() == kind::DISTINCT);
-  if(in.getNumChildren() == 2) {
-    // if this is the case exactly 1 != pair will be generated so the
-    // AND is not required
-    Node eq = NodeManager::currentNM()->mkNode(in[0].getType().isBoolean() ?
-                                               kind::IFF : kind::EQUAL,
-                                               in[0], in[1]);
-    Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq);
-    return neq;
-  }
-  // assume that in.getNumChildren() > 2 => diseqs.size() > 1
-  vector<Node> diseqs;
-  for(TNode::iterator i = in.begin(); i != in.end(); ++i) {
-    TNode::iterator j = i;
-    while(++j != in.end()) {
-      Node eq = NodeManager::currentNM()->mkNode((*i).getType().isBoolean() ?
-                                                 kind::IFF : kind::EQUAL,
-                                                 *i, *j);
-      Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq);
-      diseqs.push_back(neq);
-    }
-  }
-  Node out = NodeManager::currentNM()->mkNode(kind::AND, diseqs);
-  return out;
-}
-
-RewriteResponse TheoryBuiltin::preRewrite(TNode in, bool topLevel) {
-  switch(in.getKind()) {
-  case kind::DISTINCT:
-    return RewriteComplete(blastDistinct(in));
-
-  case kind::EQUAL:
-    // EQUAL is a special case that should never end up here
-    Unreachable("TheoryBuiltin can't rewrite EQUAL !");
-
-  default:
-    return RewriteComplete(in);
-  }
-}
-
 Node TheoryBuiltin::getValue(TNode n, TheoryEngine* engine) {
   switch(n.getKind()) {