1 files changed, 0 insertions, 73 deletions
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index ac07e13fb..ae560c5e5 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -210,79 +210,6 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a,
   }
 }
 
-void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ) {
-  //make sure internal representatives currently exist
-  for( std::map< TypeNode, std::vector< Node > >::iterator it = reps.begin(); it != reps.end(); ++it ){
-    if( it->first.isSort() ){
-      for( unsigned i=0; i<it->second.size(); i++ ){
-        Node r = getInternalRepresentative( it->second[i], Node::null(), 0 );
-      }
-    }
-  }
-  Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl;
-  for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
-    for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
-      Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl;
-    }
-  }
-  //store representatives for newly created terms
-  std::map< Node, Node > temp_rep_map;
-
-  bool success;
-  do {
-    success = false;
-    for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
-      for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
-        if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){
-          Node ni = it->second;
-          std::vector< Node > cc;
-          cc.push_back( it->second.getOperator() );
-          bool changed = false;
-          for( unsigned j=0; j<ni.getNumChildren(); j++ ){
-            if( ni[j].getType().isSort() ){
-              Node r = getRepresentative( ni[j] );
-              if( itt->second.find( r )==itt->second.end() ){
-                Assert( temp_rep_map.find( r )!=temp_rep_map.end() );
-                r = temp_rep_map[r];
-              }
-              if( r==ni ){
-                //found sub-term as instance
-                Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl;
-                itt->second[it->first] = ni[j];
-                changed = false;
-                success = true;
-                break;
-              }else{
-                Node ir = itt->second[r];
-                cc.push_back( ir );
-                if( ni[j]!=ir ){
-                  changed = true;
-                }
-              }
-            }else{
-              changed = false;
-              break;
-            }
-          }
-          if( changed ){
-            Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc );
-            Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl;
-            success = true;
-            itt->second[it->first] = n;
-            temp_rep_map[n] = it->first;
-          }
-        }
-      }
-    }
-  }while( success );
-  Trace("internal-rep-flatten") << "---After flattening : " << std::endl;
-  for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
-    for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
-      Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl;
-    }
-  }
-}
-
 eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){
   return d_qe->getActiveEqualityEngine();
 }