Commit for the theory engine and rewriter changes. Changes are substantial and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later.

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()) {