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.
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
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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
projects / cvc5.git / commitdiff