From f10a5a5ab423ee3b59667e8fda415eff85cf69e3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 18 Nov 2020 14:30:07 -0600 Subject: [PATCH] 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. --- src/CMakeLists.txt | 2 + src/printer/let_binding.cpp | 210 ++++++++++++++++++++++++++++++++++++ src/printer/let_binding.h | 150 ++++++++++++++++++++++++++ 3 files changed, 362 insertions(+) create mode 100644 src/printer/let_binding.cpp create mode 100644 src/printer/let_binding.h 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& letList) +{ + Assert(!n.isNull()); + // first, push the context + pushScope(); + // process the node + process(n); + // now, letify + letify(letList); +} + +void LetBinding::letify(std::vector& 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 visited; + std::unordered_map::iterator it; + std::vector 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 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 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 +#include + +#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 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 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 letList1; + * lbind.letify(n1, letList1); + * std::vector 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; + using NodeIdMap = context::CDHashMap; + + 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& letList); + /** + * Same as above, without a node to letify. + */ + void letify(std::vector& 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 -- 2.30.2