From ae33f11d0f4156b4d21b9e77f6df59ec0f9e8184 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 22 May 2020 08:01:59 -0500 Subject: [PATCH] (proof-new) Proof node to SExpr utility. (#4512) This is required for dag-ifying ProofNode output. --- src/expr/CMakeLists.txt | 2 + src/expr/proof_node_to_sexpr.cpp | 139 +++++++++++++++++++++++++++++++ src/expr/proof_node_to_sexpr.h | 65 +++++++++++++++ 3 files changed, 206 insertions(+) create mode 100644 src/expr/proof_node_to_sexpr.cpp create mode 100644 src/expr/proof_node_to_sexpr.h diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 36675a148..55b2c9baa 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -39,6 +39,8 @@ libcvc4_add_sources( proof_checker.h proof_node.cpp proof_node.h + proof_node_to_sexpr.cpp + proof_node_to_sexpr.h proof_node_manager.cpp proof_node_manager.h proof_rule.cpp diff --git a/src/expr/proof_node_to_sexpr.cpp b/src/expr/proof_node_to_sexpr.cpp new file mode 100644 index 000000000..cf58daa3a --- /dev/null +++ b/src/expr/proof_node_to_sexpr.cpp @@ -0,0 +1,139 @@ +/********************* */ +/*! \file proof_node_to_sexpr.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 Implementation of proof node to s-expression + **/ + +#include "expr/proof_node_to_sexpr.h" + +#include + +using namespace CVC4::kind; + +namespace CVC4 { + +ProofNodeToSExpr::ProofNodeToSExpr() +{ + NodeManager* nm = NodeManager::currentNM(); + std::vector types; + d_argsMarker = nm->mkBoundVar(":args", nm->mkSExprType(types)); +} + +Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn) +{ + NodeManager* nm = NodeManager::currentNM(); + std::map::iterator it; + std::vector visit; + std::vector constructing; + const ProofNode* cur; + visit.push_back(pn); + do + { + cur = visit.back(); + visit.pop_back(); + it = d_pnMap.find(cur); + + if (it == d_pnMap.end()) + { + d_pnMap[cur] = Node::null(); + constructing.push_back(cur); + visit.push_back(cur); + const std::vector>& pc = cur->getChildren(); + for (const std::shared_ptr& cp : pc) + { + if (std::find(constructing.begin(), constructing.end(), cp.get()) + != constructing.end()) + { + AlwaysAssert(false) + << "ProofNodeToSExpr::convertToSExpr: cyclic proof!" << std::endl; + return Node::null(); + } + visit.push_back(cp.get()); + } + } + else if (it->second.isNull()) + { + Assert(!constructing.empty()); + constructing.pop_back(); + std::vector children; + // add proof rule + children.push_back(getOrMkPfRuleVariable(cur->getRule())); + const std::vector>& pc = cur->getChildren(); + for (const std::shared_ptr& cp : pc) + { + it = d_pnMap.find(cp.get()); + Assert(it != d_pnMap.end()); + Assert(!it->second.isNull()); + children.push_back(it->second); + } + // add arguments + const std::vector& args = cur->getArguments(); + if (!args.empty()) + { + children.push_back(d_argsMarker); + // needed to ensure builtin operators are not treated as operators + // this can be the case for CONG where d_args may contain a builtin + // operator + std::vector argsSafe; + for (const Node& a : args) + { + Node av = a; + if (a.getNumChildren() == 0 + && NodeManager::operatorToKind(a) != UNDEFINED_KIND) + { + av = getOrMkNodeVariable(a); + } + argsSafe.push_back(av); + } + Node argsC = nm->mkNode(SEXPR, argsSafe); + children.push_back(argsC); + } + d_pnMap[cur] = nm->mkNode(SEXPR, children); + } + } while (!visit.empty()); + Assert(d_pnMap.find(pn) != d_pnMap.end()); + Assert(!d_pnMap.find(pn)->second.isNull()); + return d_pnMap[pn]; +} + +Node ProofNodeToSExpr::getOrMkPfRuleVariable(PfRule r) +{ + std::map::iterator it = d_pfrMap.find(r); + if (it != d_pfrMap.end()) + { + return it->second; + } + std::stringstream ss; + ss << r; + NodeManager* nm = NodeManager::currentNM(); + std::vector types; + Node var = nm->mkBoundVar(ss.str(), nm->mkSExprType(types)); + d_pfrMap[r] = var; + return var; +} + +Node ProofNodeToSExpr::getOrMkNodeVariable(Node n) +{ + std::map::iterator it = d_nodeMap.find(n); + if (it != d_nodeMap.end()) + { + return it->second; + } + std::stringstream ss; + ss << n; + NodeManager* nm = NodeManager::currentNM(); + std::vector types; + Node var = nm->mkBoundVar(ss.str(), nm->mkSExprType(types)); + d_nodeMap[n] = var; + return var; +} + +} // namespace CVC4 diff --git a/src/expr/proof_node_to_sexpr.h b/src/expr/proof_node_to_sexpr.h new file mode 100644 index 000000000..3a5cd566a --- /dev/null +++ b/src/expr/proof_node_to_sexpr.h @@ -0,0 +1,65 @@ +/********************* */ +/*! \file proof_to_sexpr.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 Conversion from ProofNode to s-expressions + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__PROOF_NODE_TO_SEXPR_H +#define CVC4__EXPR__PROOF_NODE_TO_SEXPR_H + +#include + +#include "expr/node.h" +#include "expr/proof_node.h" + +namespace CVC4 { + +/** A class to convert ProofNode objects to s-expressions */ +class ProofNodeToSExpr +{ + public: + ProofNodeToSExpr(); + ~ProofNodeToSExpr() {} + /** Convert the given proof node to an s-expression + * + * This is useful for operations where it is useful to view a ProofNode as + * a Node. Printing is one such example, where a ProofNode can be printed + * as a dag after this conversion. + * + * The s-expression for a ProofNode has the form: + * (SEXPR (VAR "") S1 ... Sn (VAR ":args") (SEXPR )) + * where S1, ..., Sn are the s-expressions for its . + */ + Node convertToSExpr(const ProofNode* pn); + + private: + /** map proof rules to a variable */ + std::map d_pfrMap; + /** Dummy ":args" marker */ + Node d_argsMarker; + /** map proof nodes to their s-expression */ + std::map d_pnMap; + /** + * map nodes to a bound variable, used for nodes that have special AST status + * like builtin operators + */ + std::map d_nodeMap; + /** get or make pf rule variable */ + Node getOrMkPfRuleVariable(PfRule r); + /** get or make node variable */ + Node getOrMkNodeVariable(Node n); +}; + +} // namespace CVC4 + +#endif /* CVC4__EXPR__PROOF_RULE_H */ -- 2.30.2