From 20db536832e9f2da6ed06917eedcad4101194ffc Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 14 Jul 2021 23:25:36 -0500 Subject: [PATCH] Add node converter utility (#6878) Adds a utility for converting nodes. This is the first step towards the LFSC proof conversion. --- src/expr/CMakeLists.txt | 2 + src/expr/node_converter.cpp | 251 ++++++++++++++++++++++++++++++++++++ src/expr/node_converter.h | 107 +++++++++++++++ 3 files changed, 360 insertions(+) create mode 100644 src/expr/node_converter.cpp create mode 100644 src/expr/node_converter.h diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 094c7bcbd..ed8a25f17 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -39,6 +39,8 @@ libcvc5_add_sources( node_algorithm.h node_builder.cpp node_builder.h + node_converter.cpp + node_converter.h node_manager.cpp node_manager.h node_manager_attributes.h diff --git a/src/expr/node_converter.cpp b/src/expr/node_converter.cpp new file mode 100644 index 000000000..92b459105 --- /dev/null +++ b/src/expr/node_converter.cpp @@ -0,0 +1,251 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Node converter utility + */ + +#include "expr/node_converter.h" + +#include "expr/attribute.h" + +using namespace cvc5::kind; + +namespace cvc5 { + +NodeConverter::NodeConverter(bool forceIdem) : d_forceIdem(forceIdem) {} + +Node NodeConverter::convert(Node n) +{ + Trace("nconv-debug") << "NodeConverter::convert: " << n << std::endl; + NodeManager* nm = NodeManager::currentNM(); + std::unordered_map::iterator it; + std::vector visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + it = d_cache.find(cur); + Trace("nconv-debug2") << "convert " << cur << std::endl; + if (it == d_cache.end()) + { + d_cache[cur] = Node::null(); + Assert(d_preCache.find(cur) == d_preCache.end()); + Node curp = preConvert(cur); + // If curp = cur, then we did not pre-rewrite. Hence, we should not + // revisit cur, and instead set curp to null. + curp = curp == cur ? Node::null() : curp; + d_preCache[cur] = curp; + if (!curp.isNull()) + { + visit.push_back(cur); + visit.push_back(curp); + } + else + { + if (!shouldTraverse(cur)) + { + addToCache(cur, cur); + } + else + { + visit.push_back(cur); + if (cur.getMetaKind() == metakind::PARAMETERIZED) + { + visit.push_back(cur.getOperator()); + } + visit.insert(visit.end(), cur.begin(), cur.end()); + } + } + } + else if (it->second.isNull()) + { + it = d_preCache.find(cur); + Assert(it != d_preCache.end()); + if (!it->second.isNull()) + { + // it converts to what its prewrite converts to + Assert(d_cache.find(it->second) != d_cache.end()); + Node ret = d_cache[it->second]; + addToCache(cur, ret); + } + else + { + Node ret = cur; + bool childChanged = false; + std::vector children; + if (ret.getMetaKind() == metakind::PARAMETERIZED) + { + it = d_cache.find(ret.getOperator()); + Assert(it != d_cache.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || ret.getOperator() != it->second; + children.push_back(it->second); + } + for (const Node& cn : ret) + { + it = d_cache.find(cn); + Assert(it != d_cache.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cn != it->second; + children.push_back(it->second); + } + if (childChanged) + { + ret = nm->mkNode(ret.getKind(), children); + } + // run the callback for the current application + Node cret = postConvert(ret); + if (!cret.isNull() && ret != cret) + { + AlwaysAssert(cret.getType().isComparableTo(ret.getType())) + << "Converting " << ret << " to " << cret << " changes type"; + ret = cret; + } + addToCache(cur, ret); + } + } + } while (!visit.empty()); + Assert(d_cache.find(n) != d_cache.end()); + Assert(!d_cache.find(n)->second.isNull()); + return d_cache[n]; +} + +TypeNode NodeConverter::convertType(TypeNode tn) +{ + if (tn.isNull()) + { + return tn; + } + Trace("nconv-debug") << "NodeConverter::convertType: " << tn << std::endl; + std::unordered_map::iterator it; + std::vector visit; + TypeNode cur; + visit.push_back(tn); + do + { + cur = visit.back(); + visit.pop_back(); + it = d_tcache.find(cur); + Trace("nconv-debug2") << "convert type " << cur << std::endl; + if (it == d_tcache.end()) + { + d_tcache[cur] = TypeNode::null(); + Assert(d_preTCache.find(cur) == d_preTCache.end()); + TypeNode curp = preConvertType(cur); + // if curp = cur, set null to avoid infinite loop + curp = curp == cur ? TypeNode::null() : curp; + d_preTCache[cur] = curp; + if (!curp.isNull()) + { + visit.push_back(cur); + visit.push_back(curp); + } + else + { + curp = curp.isNull() ? cur : curp; + if (cur.getNumChildren() == 0) + { + TypeNode ret = postConvertType(cur); + addToTypeCache(cur, ret); + } + else + { + visit.push_back(cur); + visit.insert(visit.end(), cur.begin(), cur.end()); + } + } + } + else if (it->second.isNull()) + { + it = d_preTCache.find(cur); + Assert(it != d_preTCache.end()); + if (!it->second.isNull()) + { + // it converts to what its prewrite converts to + Assert(d_tcache.find(it->second) != d_tcache.end()); + TypeNode ret = d_tcache[it->second]; + addToTypeCache(cur, ret); + } + else + { + TypeNode ret = cur; + // reconstruct using a node builder, which seems to be required for + // type nodes. + NodeBuilder nb(ret.getKind()); + if (ret.getMetaKind() == kind::metakind::PARAMETERIZED) + { + // push the operator + nb << ret.getOperator(); + } + for (TypeNode::const_iterator j = ret.begin(), iend = ret.end(); + j != iend; + ++j) + { + it = d_tcache.find(*j); + Assert(it != d_tcache.end()); + Assert(!it->second.isNull()); + nb << it->second; + } + // construct the type node + ret = nb.constructTypeNode(); + Trace("nconv-debug") << cur << " <- " << ret << std::endl; + // run the callback for the current application + TypeNode cret = postConvertType(ret); + if (!cret.isNull()) + { + ret = cret; + } + Trace("nconv-debug") + << cur << " <- " << ret << " (post-convert)" << std::endl; + addToTypeCache(cur, ret); + } + } + } while (!visit.empty()); + Assert(d_tcache.find(tn) != d_tcache.end()); + Assert(!d_tcache.find(tn)->second.isNull()); + Trace("nconv-debug") << "NodeConverter::convertType: returns " << d_tcache[tn] + << std::endl; + return d_tcache[tn]; +} + +void NodeConverter::addToCache(TNode cur, TNode ret) +{ + d_cache[cur] = ret; + // also force idempotency, if specified + if (d_forceIdem) + { + d_cache[ret] = ret; + } +} +void NodeConverter::addToTypeCache(TypeNode cur, TypeNode ret) +{ + d_tcache[cur] = ret; + // also force idempotency, if specified + if (d_forceIdem) + { + d_tcache[ret] = ret; + } +} + +Node NodeConverter::preConvert(Node n) { return Node::null(); } +Node NodeConverter::postConvert(Node n) { return Node::null(); } + +TypeNode NodeConverter::preConvertType(TypeNode tn) { return TypeNode::null(); } +TypeNode NodeConverter::postConvertType(TypeNode tn) +{ + return TypeNode::null(); +} +bool NodeConverter::shouldTraverse(Node n) { return true; } + +} // namespace cvc5 diff --git a/src/expr/node_converter.h b/src/expr/node_converter.h new file mode 100644 index 000000000..6edb2522c --- /dev/null +++ b/src/expr/node_converter.h @@ -0,0 +1,107 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Node converter utility + */ + +#include "cvc5_private.h" + +#ifndef CVC4__EXPR__NODE_CONVERTER_H +#define CVC4__EXPR__NODE_CONVERTER_H + +#include +#include + +#include "expr/node.h" +#include "expr/type_node.h" + +namespace cvc5 { + +/** + * A node converter for terms and types. Implements term/type traversals, + * calling the provided implementations of conversion methods (pre/postConvert + * and pre/postConvertType) at pre-traversal and post-traversal. + * + * This class can be used as a generic method for converting terms/types, which + * is orthogonal to methods for traversing nodes. + */ +class NodeConverter +{ + public: + /** + * @param forceIdem If true, this assumes that terms returned by postConvert + * and postConvertType should not be converted again. + */ + NodeConverter(bool forceIdem = true); + virtual ~NodeConverter() {} + /** + * This converts node n based on the preConvert/postConvert methods that can + * be overriden by instances of this class. + */ + Node convert(Node n); + + /** + * This converts type node n based on the preConvertType/postConvertType + * methods that can be overriden by instances of this class. + */ + TypeNode convertType(TypeNode tn); + + protected: + //------------------------- virtual interface + /** Should we traverse n? */ + virtual bool shouldTraverse(Node n); + /** + * Run the conversion for n during pre-order traversal. + * Returning null is equivalent to saying the node should not be changed. + */ + virtual Node preConvert(Node n); + /** + * Run the conversion for post-order traversal, where notice n is a term + * of the form: + * (f i_1 ... i_m) + * where i_1, ..., i_m are terms that have been returned by previous calls + * to postConvert. + * + * Returning null is equivalent to saying the node should not be changed. + */ + virtual Node postConvert(Node n); + /** + * Run the conversion, same as `preConvert`, but for type nodes, which notice + * can be built from children similar to Node. + */ + virtual TypeNode preConvertType(TypeNode n); + /** + * Run the conversion, same as `postConvert`, but for type nodes, which notice + * can be built from children similar to Node. + */ + virtual TypeNode postConvertType(TypeNode n); + //------------------------- end virtual interface + private: + /** Add to cache */ + void addToCache(TNode cur, TNode ret); + /** Add to type cache */ + void addToTypeCache(TypeNode cur, TypeNode ret); + /** Node cache for preConvert */ + std::unordered_map d_preCache; + /** Node cache for postConvert */ + std::unordered_map d_cache; + /** TypeNode cache for preConvert */ + std::unordered_map d_preTCache; + /** TypeNode cache for postConvert */ + std::unordered_map d_tcache; + /** Whether this node converter is idempotent. */ + bool d_forceIdem; +}; + +} // namespace cvc5 + +#endif -- 2.30.2