Refactor sep-pre-skolem-emp preprocessing pass

6 files changed, 175 insertions, 66 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index d0621bf5b..afc967df9 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -86,6 +86,8 @@ libcvc4_la_SOURCES = \
 	preprocessing/passes/real_to_int.h \
 	preprocessing/passes/rewrite.cpp \
 	preprocessing/passes/rewrite.h \
+	preprocessing/passes/sep_skolem_emp.cpp \
+	preprocessing/passes/sep_skolem_emp.h \
 	preprocessing/passes/static_learning.cpp \
 	preprocessing/passes/static_learning.h \
 	preprocessing/passes/symmetry_breaker.cpp \
diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp
new file mode 100644
index 000000000..d79ec8b93
--- /dev/null
+++ b/src/preprocessing/passes/sep_skolem_emp.cpp
@@ -0,0 +1,124 @@
+/**********************/
+/*! \file sep_skolem_emp.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Mathias Preiner, Yoni Zohar
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The sep-pre-skolem-emp preprocessing pass
+ **
+ **/
+
+#include "preprocessing/passes/sep_skolem_emp.h"
+
+#include <string>
+#include <unordered_map>
+#include <vector>
+
+#include "expr/node.h"
+#include "theory/quantifiers/quant_util.h"
+#include "theory/rewriter.h"
+#include "theory/theory.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using namespace CVC4::theory;
+
+namespace {
+
+Node 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;
+  }
+}
+
+}  // namespace
+
+SepSkolemEmp::SepSkolemEmp(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "sep-skolem-emp"){};
+
+PreprocessingPassResult SepSkolemEmp::applyInternal(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  std::map<bool, std::map<Node, Node>> visited;
+  for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
+  {
+    Node prev = (*assertionsToPreprocess)[i];
+    bool pol = true;
+    Node next = preSkolemEmp(prev, pol, visited);
+    if (next != prev)
+    {
+      assertionsToPreprocess->replace(i, Rewriter::rewrite(next));
+      Trace("sep-preprocess") << "*** Preprocess sep " << prev << endl;
+      Trace("sep-preprocess") << "   ...got " << (*assertionsToPreprocess)[i]
+                              << endl;
+    }
+    visited.clear();
+  }
+  return PreprocessingPassResult::NO_CONFLICT;
+}
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/preprocessing/passes/sep_skolem_emp.h b/src/preprocessing/passes/sep_skolem_emp.h
new file mode 100644
index 000000000..4a3dba6b8
--- /dev/null
+++ b/src/preprocessing/passes/sep_skolem_emp.h
@@ -0,0 +1,42 @@
+/*********************                                                        */
+/*! \file sep_skolem_emp.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Mathias Preiner, Yoni Zohar
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The sep-pre-skolem-emp eprocessing pass
+ **
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H
+#define __CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class SepSkolemEmp : public PreprocessingPass
+{
+ public:
+  SepSkolemEmp(PreprocessingPassContext* preprocContext);
+
+ protected:
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+};
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 69c0dab9c..958fec175 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -79,6 +79,7 @@
 #include "preprocessing/passes/pseudo_boolean_processor.h"
 #include "preprocessing/passes/real_to_int.h"
 #include "preprocessing/passes/rewrite.h"
+#include "preprocessing/passes/sep_skolem_emp.h"
 #include "preprocessing/passes/static_learning.h"
 #include "preprocessing/passes/symmetry_breaker.h"
 #include "preprocessing/passes/symmetry_detect.h"
@@ -2725,7 +2726,9 @@ void SmtEnginePrivate::finishInit()
       new SymBreakerPass(d_preprocessingPassContext.get()));
   std::unique_ptr<SynthRewRulesPass> srrProc(
       new SynthRewRulesPass(d_preprocessingPassContext.get()));
-  d_preprocessingPassRegistry.registerPass("apply-substs",
+ std::unique_ptr<SepSkolemEmp> sepSkolemEmp(
+      new SepSkolemEmp(d_preprocessingPassContext.get()));
+   d_preprocessingPassRegistry.registerPass("apply-substs",
                                            std::move(applySubsts));
   d_preprocessingPassRegistry.registerPass("bool-to-bv", std::move(boolToBv));
   d_preprocessingPassRegistry.registerPass("bv-abstraction",
@@ -2741,6 +2744,8 @@ void SmtEnginePrivate::finishInit()
                                            std::move(pbProc));
   d_preprocessingPassRegistry.registerPass("real-to-int", std::move(realToInt));
   d_preprocessingPassRegistry.registerPass("rewrite", std::move(rewrite));
+  d_preprocessingPassRegistry.registerPass("sep-skolem-emp",
+                                           std::move(sepSkolemEmp));
   d_preprocessingPassRegistry.registerPass("static-learning", 
                                            std::move(staticLearning));
   d_preprocessingPassRegistry.registerPass("sym-break", std::move(sbProc));
@@ -4224,15 +4229,7 @@ void SmtEnginePrivate::processAssertions() {
     Trace("smt") << "POST boolToBv" << endl;
   }
   if(options::sepPreSkolemEmp()) {
-    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
-      Node prev = d_assertions[i];
-      Node next = sep::TheorySepRewriter::preprocess( prev );
-      if( next!=prev ){
-        d_assertions.replace( i, Rewriter::rewrite( next ) );
-        Trace("sep-preprocess") << "*** Preprocess sep " << prev << endl;
-        Trace("sep-preprocess") << "   ...got " << d_assertions[i] << endl;
-      }
-    }
+    d_preprocessingPassRegistry.getPass("sep-skolem-emp")->apply(&d_assertions);
   }
 
   if( d_smt.d_logic.isQuantified() ){
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 */