Refactor sep-pre-skolem-emp preprocessing pass

2 files changed, 0 insertions, 56 deletions

diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp
index 4d0885dc2..614d4f7c4 100644
--- a/src/theory/sep/theory_sep_rewriter.cpp
+++ b/src/theory/sep/theory_sep_rewriter.cpp
@@ -161,58 +161,6 @@ RewriteResponse TheorySepRewriter::postRewrite(TNode node) {
   return RewriteResponse(node==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode);
 }
 
-Node TheorySepRewriter::preSkolemEmp( Node n, bool pol, std::map< bool, std::map< Node, Node > >& visited ) {
-  std::map< Node, Node >::iterator it = visited[pol].find( n );
-  if( it==visited[pol].end() ){
-    Trace("sep-preprocess") << "Pre-skolem emp " << n << " with pol " << pol << std::endl;
-    Node ret = n;
-    if( n.getKind()==kind::SEP_EMP ){
-      if( !pol ){
-        TypeNode tnx = n[0].getType();
-        TypeNode tny = n[1].getType();
-        Node x = NodeManager::currentNM()->mkSkolem( "ex", tnx, "skolem location for negated emp" );
-        Node y = NodeManager::currentNM()->mkSkolem( "ey", tny, "skolem data for negated emp" );
-        return NodeManager::currentNM()->mkNode( kind::SEP_STAR, 
-                 NodeManager::currentNM()->mkNode( kind::SEP_PTO, x, y ),
-                 NodeManager::currentNM()->mkConst( true ) ).negate();
-      }
-    }else if( n.getKind()!=kind::FORALL && n.getNumChildren()>0 ){
-      std::vector< Node > children;
-      bool childChanged = false;
-      if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-        children.push_back( n.getOperator() );
-      }
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        bool newPol, newHasPol;
-        QuantPhaseReq::getPolarity( n, i, true, pol, newHasPol, newPol );
-        Node nc = n[i];
-        if( newHasPol ){
-          nc = preSkolemEmp( n[i], newPol, visited );
-          childChanged = childChanged || nc!=n[i];
-        }
-        children.push_back( nc );
-      }
-      if( childChanged ){
-        return NodeManager::currentNM()->mkNode( n.getKind(), children );
-      }
-    }
-    visited[pol][n] = ret;
-    return n;
-  }else{
-    return it->second;
-  }
-}
-
-Node TheorySepRewriter::preprocess( Node n ) {
-  if( options::sepPreSkolemEmp() ){
-    bool pol = true;
-    std::map< bool, std::map< Node, Node > > visited;
-    n = preSkolemEmp( n, pol, visited );
-  }
-  return n;
-}
-
-
 }/* CVC4::theory::sep namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/sep/theory_sep_rewriter.h b/src/theory/sep/theory_sep_rewriter.h
index e867bc0e9..8ed8c3de2 100644
--- a/src/theory/sep/theory_sep_rewriter.h
+++ b/src/theory/sep/theory_sep_rewriter.h
@@ -43,10 +43,6 @@ public:
 
   static inline void init() {}
   static inline void shutdown() {}
-private:
-  static Node preSkolemEmp( Node n, bool pol, std::map< bool, std::map< Node, Node > >& visited );
-public:
-  static Node preprocess( Node n );
 };/* class TheorySepRewriter */
 
 }/* CVC4::theory::sep namespace */