From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Fri, 15 Mar 2019 22:01:42 +0000 (-0500)
Subject: Adding capture avoiding substitution (#2867)
X-Git-Tag: cvc5-1.0.0~4239
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e8f23236b7f797fd3cd8900df0422d44f1a6a7e0;p=cvc5.git

Adding capture avoiding substitution (#2867)
---

diff --git a/src/expr/node.h b/src/expr/node.h
index 50add7b17..003863c8e 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -459,7 +459,7 @@ public:
     assertTNodeNotExpired();
     return getMetaKind() == kind::metakind::VARIABLE;
   }
-  
+
   /**
    * Returns true if this node represents a nullary operator
    */
@@ -467,12 +467,11 @@ public:
     assertTNodeNotExpired();
     return getMetaKind() == kind::metakind::NULLARY_OPERATOR;
   }
-  
+
   inline bool isClosure() const {
     assertTNodeNotExpired();
     return getKind() == kind::LAMBDA || getKind() == kind::FORALL
-           || getKind() == kind::EXISTS || getKind() == kind::REWRITE_RULE
-           || getKind() == kind::CHOICE;
+           || getKind() == kind::EXISTS || getKind() == kind::CHOICE;
   }
 
   /**
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 6923efec2..dcf78fb37 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -273,5 +273,117 @@ void getSymbols(TNode n,
   } while (!visit.empty());
 }
 
+Node substituteCaptureAvoiding(TNode n, Node src, Node dest)
+{
+  if (n == src)
+  {
+    return dest;
+  }
+  if (src == dest)
+  {
+    return n;
+  }
+  std::vector<Node> srcs;
+  std::vector<Node> dests;
+  srcs.push_back(src);
+  dests.push_back(dest);
+  return substituteCaptureAvoiding(n, srcs, dests);
+}
+
+Node substituteCaptureAvoiding(TNode n,
+                               std::vector<Node>& src,
+                               std::vector<Node>& dest)
+{
+  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+  std::vector<TNode> visit;
+  TNode curr;
+  visit.push_back(n);
+  Assert(src.size() == dest.size(),
+         "Substitution domain and range must be equal size");
+  do
+  {
+    curr = visit.back();
+    visit.pop_back();
+    it = visited.find(curr);
+
+    if (it == visited.end())
+    {
+      auto itt = std::find(src.rbegin(), src.rend(), curr);
+      if (itt != src.rend())
+      {
+        Assert(
+            (std::distance(src.begin(), itt.base()) - 1) >= 0
+            && static_cast<unsigned>(std::distance(src.begin(), itt.base()) - 1)
+                   < dest.size());
+        Node n = dest[std::distance(src.begin(), itt.base()) - 1];
+        visited[curr] = n;
+        continue;
+      }
+      if (curr.getNumChildren() == 0)
+      {
+        visited[curr] = curr;
+        continue;
+      }
+
+      visited[curr] = Node::null();
+      // if binder, rename variables to avoid capture
+      if (curr.isClosure())
+      {
+        NodeManager* nm = NodeManager::currentNM();
+        // have new vars -> renames subs in the end of current sub
+        for (const Node& v : curr[0])
+        {
+          src.push_back(v);
+          dest.push_back(nm->mkBoundVar(v.getType()));
+        }
+      }
+      // save for post-visit
+      visit.push_back(curr);
+      // visit children
+      if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
+      {
+        // push the operator
+        visit.push_back(curr.getOperator());
+      }
+      for (unsigned i = 0, size = curr.getNumChildren(); i < size; ++i)
+      {
+        visit.push_back(curr[i]);
+      }
+    }
+    else if (it->second.isNull())
+    {
+      // build node
+      NodeBuilder<> nb(curr.getKind());
+      if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
+      {
+        // push the operator
+        Assert(visited.find(curr.getOperator()) != visited.end());
+        nb << visited[curr.getOperator()];
+      }
+      // collect substituted children
+      for (unsigned i = 0, size = curr.getNumChildren(); i < size; ++i)
+      {
+        Assert(visited.find(curr[i]) != visited.end());
+        nb << visited[curr[i]];
+      }
+      Node n = nb;
+      visited[curr] = n;
+
+      // remove renaming
+      if (curr.isClosure())
+      {
+        // remove beginning of sub which correspond to renaming of variables in
+        // this binder
+        unsigned nchildren = curr[0].getNumChildren();
+        src.resize(src.size() - nchildren);
+        dest.resize(dest.size() - nchildren);
+      }
+    }
+  } while (!visit.empty());
+  Assert(visited.find(n) != visited.end());
+  return visited[n];
+}
+
 }  // namespace expr
 }  // namespace CVC4
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index bf2cb5877..7cc12b664 100644
--- a/src/expr/node_algorithm.h
+++ b/src/expr/node_algorithm.h
@@ -83,6 +83,19 @@ void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms);
 void getSymbols(TNode n,
                 std::unordered_set<Node, NodeHashFunction>& syms,
                 std::unordered_set<TNode, TNodeHashFunction>& visited);
+/**
+ * Substitution of Nodes in a capture avoiding way.
+ */
+Node substituteCaptureAvoiding(TNode n, Node src, Node dest);
+
+/**
+ * Simultaneous substitution of Nodes in a capture avoiding way.  Elements in
+ * source will be replaced by their corresponding element in dest.  Both
+ * vectors should have the same size.
+ */
+Node substituteCaptureAvoiding(TNode n,
+                               std::vector<Node>& src,
+                               std::vector<Node>& dest);
 
 }  // namespace expr
 }  // namespace CVC4