From f5d32970e5601ce0b4246cef5bca0636425fdc34 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 26 Jul 2021 20:31:21 -0500 Subject: [PATCH] Add proof letify utility (#6881) Towards support for external proof conversions. --- src/CMakeLists.txt | 2 + src/proof/proof_letify.cpp | 124 +++++++++++++++++++++++++++++++++++++ src/proof/proof_letify.h | 98 +++++++++++++++++++++++++++++ 3 files changed, 224 insertions(+) create mode 100644 src/proof/proof_letify.cpp create mode 100644 src/proof/proof_letify.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 445d38896..9f208ac46 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -169,6 +169,8 @@ libcvc5_add_sources( proof/proof_ensure_closed.h proof/proof_generator.cpp proof/proof_generator.h + proof/proof_letify.cpp + proof/proof_letify.h proof/proof_node.cpp proof/proof_node.h proof/proof_node_algorithm.cpp diff --git a/src/proof/proof_letify.cpp b/src/proof/proof_letify.cpp new file mode 100644 index 000000000..c6269631c --- /dev/null +++ b/src/proof/proof_letify.cpp @@ -0,0 +1,124 @@ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Utilities for computing letification of proofs. + */ + +#include "proof/proof_letify.h" + +namespace cvc5 { +namespace proof { + +bool ProofLetifyTraverseCallback::shouldTraverse(const ProofNode* pn) +{ + return pn->getRule() != PfRule::SCOPE; +} + +void ProofLetify::computeProofLet(const ProofNode* pn, + std::vector& pletList, + std::map& pletMap, + size_t thresh, + ProofLetifyTraverseCallback* pltc) +{ + Assert(pletList.empty() && pletMap.empty()); + if (thresh == 0) + { + // value of 0 means do not introduce let + return; + } + std::vector visitList; + std::map pcount; + if (pltc == nullptr) + { + // use default callback + ProofLetifyTraverseCallback defaultPltc; + computeProofCounts(pn, visitList, pcount, &defaultPltc); + } + else + { + computeProofCounts(pn, visitList, pcount, pltc); + } + // Now populate the pletList and pletMap + convertProofCountToLet(visitList, pcount, pletList, pletMap, thresh); +} + +void ProofLetify::computeProofCounts(const ProofNode* pn, + std::vector& visitList, + std::map& pcount, + ProofLetifyTraverseCallback* pltc) +{ + std::map::iterator it; + std::vector visit; + const ProofNode* cur; + visit.push_back(pn); + do + { + cur = visit.back(); + it = pcount.find(cur); + if (it == pcount.end()) + { + pcount[cur] = 0; + if (!pltc->shouldTraverse(cur)) + { + // callback indicated we should not traverse + continue; + } + const std::vector>& pc = cur->getChildren(); + for (const std::shared_ptr& cp : pc) + { + visit.push_back(cp.get()); + } + } + else + { + if (it->second == 0) + { + visitList.push_back(cur); + } + pcount[cur]++; + visit.pop_back(); + } + } while (!visit.empty()); +} + +void ProofLetify::convertProofCountToLet( + const std::vector& visitList, + const std::map& pcount, + std::vector& pletList, + std::map& pletMap, + size_t thresh) +{ + Assert(pletList.empty() && pletMap.empty()); + if (thresh == 0) + { + // value of 0 means do not introduce let + return; + } + // Assign ids for those whose count is > 1, traverse in reverse order + // so that deeper proofs are assigned lower identifiers + std::map::const_iterator itc; + for (const ProofNode* pn : visitList) + { + itc = pcount.find(pn); + Assert(itc != pcount.end()); + if (itc->second >= thresh && pn->getRule() != PfRule::ASSUME) + { + pletList.push_back(pn); + // start with id 1 + size_t id = pletMap.size() + 1; + pletMap[pn] = id; + } + } +} + +} // namespace proof +} // namespace cvc5 diff --git a/src/proof/proof_letify.h b/src/proof/proof_letify.h new file mode 100644 index 000000000..cfe1259e5 --- /dev/null +++ b/src/proof/proof_letify.h @@ -0,0 +1,98 @@ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Utilities for computing letification of proofs. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__PROOF_LETIFY_H +#define CVC5__PROOF__PROOF_LETIFY_H + +#include +#include + +#include "expr/node.h" +#include "proof/proof_node.h" + +namespace cvc5 { +namespace proof { + +/** + * A callback which asks whether a proof node should be traversed for + * proof letification. For example, this may make it so that SCOPE is not + * traversed. + */ +class ProofLetifyTraverseCallback +{ + public: + virtual ~ProofLetifyTraverseCallback() {} + /** + * Should we traverse proof node pn for letification? If this returns false, + * then pn is being treated as a black box for letification. + */ + virtual bool shouldTraverse(const ProofNode* pn); +}; + +/** + * Utilities for letification. + */ +class ProofLetify +{ + public: + /** + * Stores proofs in map that require letification, mapping them to a unique + * identifier. For each proof node in the domain of pletMap in the list + * pletList such that pletList[i] does not contain subproof pletList[j] for + * j>i. + * + * @param pn The proof node to letify + * @param pletList The list of proofs occurring in pn that should be letified + * @param pletMap Mapping from proofs in pletList to an identifier + * @param thresh The number of times a proof node has to occur to be added + * to pletList + * @param pltc A callback indicating whether to traverse a proof node during + * this call. + */ + static void computeProofLet(const ProofNode* pn, + std::vector& pletList, + std::map& pletMap, + size_t thresh = 2, + ProofLetifyTraverseCallback* pltc = nullptr); + + private: + /** + * Convert a map from proof nodes to # occurrences (pcount) to a list + * pletList / pletMap as described in the method above, where thresh + * is the minimum number of occurrences to be added to the list. + */ + static void convertProofCountToLet( + const std::vector& visitList, + const std::map& pcount, + std::vector& pletList, + std::map& pletMap, + size_t thresh = 2); + /** + * Compute the count of sub proof nodes in pn, store in pcount. Additionally, + * store each proof node in the domain of pcount in an order in visitList + * such that visitList[i] does not contain sub proof visitList[j] for j>i. + */ + static void computeProofCounts(const ProofNode* pn, + std::vector& visitList, + std::map& pcount, + ProofLetifyTraverseCallback* pltc); +}; + +} // namespace proof +} // namespace cvc5 + +#endif -- 2.30.2