1 files changed, 0 insertions, 200 deletions
diff --git a/src/util/nary_builder.cpp b/src/util/nary_builder.cpp
deleted file mode 100644
index d89121fd7..000000000
--- a/src/util/nary_builder.cpp
+++ /dev/null
@@ -1,200 +0,0 @@
-/*********************                                                        */
-/*! \file nary_builder.cpp
- ** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-
-#include "util/nary_builder.h"
-#include "expr/metakind.h"
-using namespace std;
-
-namespace CVC4 {
-namespace util {
-
-Node NaryBuilder::mkAssoc(Kind kind, const std::vector<Node>& children){
-  if(children.size() == 0){
-    return zeroArity(kind);
-  }else if(children.size() == 1){
-    return children[0];
-  }else{
-    const unsigned int max = kind::metakind::getUpperBoundForKind(kind);
-    const unsigned int min = kind::metakind::getLowerBoundForKind(kind);
-
-    Assert(min <= children.size());
-
-    unsigned int numChildren = children.size();
-    NodeManager* nm = NodeManager::currentNM();
-    if( numChildren <= max ) {
-      return nm->mkNode(kind,children);
-    }
-
-    typedef std::vector<Node>::const_iterator const_iterator;
-    const_iterator it = children.begin() ;
-    const_iterator end = children.end() ;
-
-    /* The new top-level children and the children of each sub node */
-    std::vector<Node> newChildren;
-    std::vector<Node> subChildren;
-
-    while( it != end && numChildren > max ) {
-      /* Grab the next max children and make a node for them. */
-      for(const_iterator next = it + max; it != next; ++it, --numChildren ) {
-        subChildren.push_back(*it);
-      }
-      Node subNode = nm->mkNode(kind,subChildren);
-      newChildren.push_back(subNode);
-      subChildren.clear();
-    }
-
-    /* If there's children left, "top off" the Expr. */
-    if(numChildren > 0) {
-      /* If the leftovers are too few, just copy them into newChildren;
-       * otherwise make a new sub-node  */
-      if(numChildren < min) {
-        for(; it != end; ++it) {
-          newChildren.push_back(*it);
-        }
-      } else {
-        for(; it != end; ++it) {
-          subChildren.push_back(*it);
-        }
-        Node subNode = nm->mkNode(kind, subChildren);
-        newChildren.push_back(subNode);
-      }
-    }
-
-    /* It's inconceivable we could have enough children for this to fail
-     * (more than 2^32, in most cases?). */
-    AlwaysAssert( newChildren.size() <= max,
-                  "Too many new children in mkAssociative" );
-
-    /* It would be really weird if this happened (it would require
-     * min > 2, for one thing), but let's make sure. */
-    AlwaysAssert( newChildren.size() >= min,
-                  "Too few new children in mkAssociative" );
-
-    return nm->mkNode(kind,newChildren);
-  }
-}
-
-Node NaryBuilder::zeroArity(Kind k){
-  using namespace kind;
-  NodeManager* nm = NodeManager::currentNM();
-  switch(k){
-  case AND:
-    return nm->mkConst(true);
-  case OR:
-    return nm->mkConst(false);
-  case PLUS:
-    return nm->mkConst(Rational(0));
-  case MULT:
-    return nm->mkConst(Rational(1));
-  default:
-    return Node::null();
-  }
-}
-
-
-RePairAssocCommutativeOperators::RePairAssocCommutativeOperators()
-  : d_cache()
-{}
-RePairAssocCommutativeOperators::~RePairAssocCommutativeOperators(){}
-size_t RePairAssocCommutativeOperators::size() const{ return d_cache.size(); }
-void RePairAssocCommutativeOperators::clear(){ d_cache.clear(); }
-
-bool RePairAssocCommutativeOperators::isAssociateCommutative(Kind k){
-  using namespace kind;
-  switch(k){
-  case BITVECTOR_CONCAT:
-  case BITVECTOR_AND:
-  case BITVECTOR_OR:
-  case BITVECTOR_XOR:
-  case BITVECTOR_MULT:
-  case BITVECTOR_PLUS:
-  case DISTINCT:
-  case PLUS:
-  case MULT:
-  case AND:
-  case OR:
-    return true;
-  default:
-    return false;
-  }
-}
-
-Node RePairAssocCommutativeOperators::rePairAssocCommutativeOperators(TNode n){
-  if(d_cache.find(n) != d_cache.end()){
-    return d_cache[n];
-  }
-  Node result =
-    isAssociateCommutative(n.getKind()) ?
-    case_assoccomm(n) : case_other(n);
-
-  d_cache[n] = result;
-  return result;
-}
-
-Node RePairAssocCommutativeOperators::case_assoccomm(TNode n){
-  Kind k = n.getKind();
-  Assert(isAssociateCommutative(k));
-  Assert(n.getMetaKind() != kind::metakind::PARAMETERIZED);
-  unsigned N = n.getNumChildren();
-  Assert(N >= 2);
-
-
-  Node last = rePairAssocCommutativeOperators( n[N-1]);
-  Node nextToLast = rePairAssocCommutativeOperators(n[N-2]);
-
-  NodeManager* nm = NodeManager::currentNM();
-  Node last2 = nm->mkNode(k, nextToLast, last);
-
-  if(N <= 2){
-    return last2;
-  } else{
-    Assert(N > 2);
-    Node prevRound = last2;
-    for(unsigned prevPos = N-2; prevPos > 0; --prevPos){
-      unsigned currPos = prevPos-1;
-      Node curr = rePairAssocCommutativeOperators(n[currPos]);
-      Node round = nm->mkNode(k, curr, prevRound);
-      prevRound = round;
-    }
-    return prevRound;
-  }
-}
-
-Node RePairAssocCommutativeOperators::case_other(TNode n){
-  if(n.isConst() || n.isVar()){
-    return n;
-  }
-
-  NodeBuilder<> nb(n.getKind());
-
-  if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
-    nb << n.getOperator();
-  }
-
-  // Remove the ITEs from the children
-  for(TNode::const_iterator i = n.begin(), end = n.end(); i != end; ++i) {
-    Node newChild = rePairAssocCommutativeOperators(*i);
-    nb << newChild;
-  }
-
-  Node result = (Node)nb;
-  return result;
-}
-
-}/* util namespace */
-}/* CVC4 namespace */