Add let binding utility (#5444)

This utility will replace the dagification visitor for printing lets for Node in the smt2 printer, and will be used further in e.g. LFSC proof printing.

3 files changed, 362 insertions, 0 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index b505871a3..47903ccae 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -124,6 +124,8 @@ libcvc4_add_sources(
   printer/cvc/cvc_printer.h
   printer/dagification_visitor.cpp
   printer/dagification_visitor.h
+  printer/let_binding.cpp
+  printer/let_binding.h
   printer/printer.cpp
   printer/printer.h
   printer/smt2/smt2_printer.cpp
diff --git a/src/printer/let_binding.cpp b/src/printer/let_binding.cpp
new file mode 100644
index 000000000..439037b64
--- /dev/null
+++ b/src/printer/let_binding.cpp
@@ -0,0 +1,210 @@
+/*********************                                                        */
+/*! \file let_binding.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 A let binding utility
+ **/
+
+#include "printer/let_binding.h"
+
+namespace CVC4 {
+
+LetBinding::LetBinding(uint32_t thresh)
+    : d_thresh(thresh),
+      d_context(),
+      d_visitList(&d_context),
+      d_count(&d_context),
+      d_letList(&d_context),
+      d_letMap(&d_context)
+{
+}
+
+uint32_t LetBinding::getThreshold() const { return d_thresh; }
+
+void LetBinding::process(Node n)
+{
+  Assert(!n.isNull());
+  if (d_thresh == 0)
+  {
+    // value of 0 means do not introduce let
+    return;
+  }
+  // update the count of occurrences
+  updateCounts(n);
+}
+
+void LetBinding::letify(Node n, std::vector<Node>& letList)
+{
+  Assert(!n.isNull());
+  // first, push the context
+  pushScope();
+  // process the node
+  process(n);
+  // now, letify
+  letify(letList);
+}
+
+void LetBinding::letify(std::vector<Node>& letList)
+{
+  size_t prevSize = d_letList.size();
+  // populate the d_letList and d_letMap
+  convertCountToLet();
+  // add the new entries to the letList
+letList.insert(letList.end(), d_letList.begin() + prevSize, d_letList.end());
+}
+
+void LetBinding::pushScope() { d_context.push(); }
+
+void LetBinding::popScope() { d_context.pop(); }
+
+uint32_t LetBinding::getId(Node n) const
+{
+  NodeIdMap::const_iterator it = d_letMap.find(n);
+  if (it == d_letMap.end())
+  {
+    return 0;
+  }
+  return (*it).second;
+}
+
+Node LetBinding::convert(Node n, const std::string& prefix, bool letTop) const
+{
+  if (d_letMap.empty())
+  {
+    return n;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = visited.find(cur);
+
+    if (it == visited.end())
+    {
+      uint32_t id = getId(cur);
+      // do not letify id 0, or n itself if letTop is false
+      if (id > 0 && (cur != n || letTop))
+      {
+        // make the let variable
+        std::stringstream ss;
+        ss << prefix << id;
+        visited[cur] = nm->mkBoundVar(ss.str(), cur.getType());
+      }
+      else
+      {
+        visited[cur] = Node::null();
+        visit.push_back(cur);
+        visit.insert(visit.end(), cur.begin(), cur.end());
+      }
+    }
+    else if (it->second.isNull())
+    {
+      Node ret = cur;
+      bool childChanged = false;
+      std::vector<Node> children;
+      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
+      {
+        children.push_back(cur.getOperator());
+      }
+      for (const Node& cn : cur)
+      {
+        it = visited.find(cn);
+        Assert(it != visited.end());
+        Assert(!it->second.isNull());
+        childChanged = childChanged || cn != it->second;
+        children.push_back(it->second);
+      }
+      if (childChanged)
+      {
+        ret = nm->mkNode(cur.getKind(), children);
+      }
+      visited[cur] = ret;
+    }
+  } while (!visit.empty());
+  Assert(visited.find(n) != visited.end());
+  Assert(!visited.find(n)->second.isNull());
+  return visited[n];
+}
+
+void LetBinding::updateCounts(Node n)
+{
+  NodeIdMap::iterator it;
+  std::vector<Node> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    it = d_count.find(cur);
+    if (it == d_count.end())
+    {
+      // do not traverse beneath quantifiers
+      if (cur.getNumChildren() == 0 || cur.isClosure())
+      {
+        d_visitList.push_back(cur);
+        d_count[cur] = 1;
+        visit.pop_back();
+      }
+      else
+      {
+        d_count[cur] = 0;
+        visit.insert(visit.end(), cur.begin(), cur.end());
+      }
+    }
+    else
+    {
+      if ((*it).second == 0)
+      {
+        d_visitList.push_back(cur);
+      }
+      d_count[cur] = (*it).second + 1;
+      visit.pop_back();
+    }
+  } while (!visit.empty());
+}
+
+void LetBinding::convertCountToLet()
+{
+  Assert(d_thresh > 0);
+  // Assign ids for those whose d_count is >= d_thresh, traverse in d_visitList
+  // in order so that deeper nodes are assigned lower identifiers, which
+  // ensures the let list can be printed.
+  NodeIdMap::const_iterator itc;
+  for (const Node& n : d_visitList)
+  {
+    if (n.getNumChildren() == 0)
+    {
+      // do not letify terms with no children
+      continue;
+    }
+    else if (d_letMap.find(n) != d_letMap.end())
+    {
+      // already letified, perhaps at a lower context
+      continue;
+    }
+    itc = d_count.find(n);
+    Assert(itc != d_count.end());
+    if ((*itc).second >= d_thresh)
+    {
+      d_letList.push_back(n);
+      // start with id 1
+      size_t id = d_letMap.size() + 1;
+      d_letMap[n] = id;
+    }
+  }
+}
+
+}  // namespace CVC4
diff --git a/src/printer/let_binding.h b/src/printer/let_binding.h
new file mode 100644
index 000000000..d81274c87
--- /dev/null
+++ b/src/printer/let_binding.h
@@ -0,0 +1,150 @@
+/*********************                                                        */
+/*! \file let_binding.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 A let binding
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__PRINTER__LET_BINDING_H
+#define CVC4__PRINTER__LET_BINDING_H
+
+#include <map>
+#include <vector>
+
+#include "context/cdhashmap.h"
+#include "context/cdlist.h"
+#include "expr/node.h"
+
+namespace CVC4 {
+
+/**
+ * A flexible let binding class. This class provides functionalities for
+ * printing letified terms. A simple use case is the following for Node n
+ * and LetBinding lbind:
+ * ```
+ *   std::vector<Node> letList;
+ *   lbind.letify(n, letList);
+ * ```
+ * Now, letList contains a list of subterms of n that should be letified based
+ * on the threshold value passed to this class where a value n>0 indicates that
+ * terms with n or more occurrences should be letified.
+ *
+ * The above is equivalent to:
+ * ```
+ *   std::vector<Node> letList;
+ *   lbind.pushScope();
+ *   lbind.process(n);
+ *   lbind.letify(letList);
+ * ```
+ * In fact, multiple terms can be passed to calls to process, in which case the
+ * counting is cumulative.
+ *
+ * All quantified formulas are treated as black boxes. This class can be used
+ * to letify terms with quantifiers, where multiple calls to pushScope /
+ * popScope can be used. In particular, consider:
+ * ```
+ *   std::vector<Node> letList1;
+ *   lbind.letify(n1, letList1);
+ *   std::vector<Node> letList2;
+ *   lbind.letify(n2, letList2);
+ *   ...
+ *   lbind.popScope();
+ *   lbind.popScope();
+ * ```
+ * In a typical use case, n2 is the body of a quantified formula that is a
+ * subterm of n1. We have that letList2 is the list of subterms of n2 that
+ * should be letified, assuming that we have already have let definitions
+ * given by letList1.
+ *
+ * Internally, a let binding is a list and a map that can be printed as a let
+ * expression. In particular, the list d_letList is ordered such that
+ * d_letList[i] does not contain subterm d_letList[j] for j>i.
+ * It is intended that d_letList contains only unique nodes. Each node
+ * in d_letList is mapped to a unique identifier in d_letMap.
+ */
+class LetBinding
+{
+  using NodeList = context::CDList<Node>;
+  using NodeIdMap = context::CDHashMap<Node, uint32_t, NodeHashFunction>;
+
+ public:
+  LetBinding(uint32_t thresh = 2);
+  /** Get threshold */
+  uint32_t getThreshold() const;
+  /**
+   * This updates this let binding to consider the counts for node n.
+   */
+  void process(Node n);
+  /**
+   * This pushes a scope, computes the letification for n, adds the (new) terms
+   * that must be letified in this context to letList.
+   *
+   * Notice that this method does not traverse inside of closures.
+   *
+   * @param n The node to letify
+   * @param letList The list of terms that should be letified within n. This
+   * list is ordered in such a way that letList[i] does not contain subterm
+   * letList[j] for j>i.
+   */
+  void letify(Node n, std::vector<Node>& letList);
+  /**
+   * Same as above, without a node to letify.
+   */
+  void letify(std::vector<Node>& letList);
+  /** Push scope */
+  void pushScope();
+  /** Pop scope for n, reverts the state change of the above method */
+  void popScope();
+  /**
+   * @return the identifier for node n, or 0 if it does not have one.
+   */
+  uint32_t getId(Node n) const;
+  /**
+   * Convert n based on the state of the let binding. This replaces all
+   * letified subterms of n with a fresh variable whose name prefix is the
+   * given one.
+   *
+   * @param n The node to convert
+   * @param prefix The prefix of variables to convert
+   * @param letTop Whether we letify n itself
+   * @return the converted node.
+   */
+  Node convert(Node n, const std::string& prefix, bool letTop = true) const;
+
+ private:
+  /**
+   * Compute the count of sub nodes in n, store in d_count. Additionally,
+   * store each node in the domain of d_count in an order in d_visitList
+   * such that d_visitList[i] does not contain sub d_visitList[j] for j>i.
+   */
+  void updateCounts(Node n);
+  /**
+   * Convert a count to a let binding.
+   */
+  void convertCountToLet();
+  /** The dag threshold */
+  uint32_t d_thresh;
+  /** An internal context */
+  context::Context d_context;
+  /** Visit list */
+  NodeList d_visitList;
+  /** Count */
+  NodeIdMap d_count;
+  /** The let list */
+  NodeList d_letList;
+  /** The let map */
+  NodeIdMap d_letMap;
+};
+
+}  // namespace CVC4
+
+#endif