From: Andrew Reynolds Date: Wed, 8 Sep 2021 21:42:30 +0000 (-0500) Subject: Add Lfsc print channel utilities (#7123) X-Git-Tag: cvc5-1.0.0~1252 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b9dcd4d141cef256b4371aa103af4ee1aa7c61bd;p=cvc5.git Add Lfsc print channel utilities (#7123) These are utilities used for two-pass printing of LFSC proofs. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5c898b654..4484f9447 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -182,6 +182,8 @@ libcvc5_add_sources( proof/lfsc/lfsc_list_sc_node_converter.h proof/lfsc/lfsc_node_converter.cpp proof/lfsc/lfsc_node_converter.h + proof/lfsc/lfsc_print_channel.cpp + proof/lfsc/lfsc_print_channel.h proof/lfsc/lfsc_util.cpp proof/lfsc/lfsc_util.h proof/method_id.cpp diff --git a/src/proof/lfsc/lfsc_print_channel.cpp b/src/proof/lfsc/lfsc_print_channel.cpp new file mode 100644 index 000000000..36fd8831b --- /dev/null +++ b/src/proof/lfsc/lfsc_print_channel.cpp @@ -0,0 +1,161 @@ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Print channels for LFSC proofs. + */ + +#include "proof/lfsc/lfsc_print_channel.h" + +#include + +#include "proof/lfsc/lfsc_util.h" + +namespace cvc5 { +namespace proof { + +LfscPrintChannelOut::LfscPrintChannelOut(std::ostream& out) : d_out(out) {} +void LfscPrintChannelOut::printNode(TNode n) +{ + d_out << " "; + printNodeInternal(d_out, n); +} + +void LfscPrintChannelOut::printTypeNode(TypeNode tn) +{ + d_out << " "; + printTypeNodeInternal(d_out, tn); +} + +void LfscPrintChannelOut::printHole() { d_out << " _ "; } +void LfscPrintChannelOut::printTrust(TNode res, PfRule src) +{ + d_out << std::endl << "(trust "; + printNodeInternal(d_out, res); + d_out << ") ; from " << src << std::endl; +} + +void LfscPrintChannelOut::printOpenRule(const ProofNode* pn) +{ + d_out << std::endl << "("; + printRule(d_out, pn); +} + +void LfscPrintChannelOut::printOpenLfscRule(LfscRule lr) +{ + d_out << std::endl << "(" << lr; +} + +void LfscPrintChannelOut::printCloseRule(size_t nparen) +{ + for (size_t i = 0; i < nparen; i++) + { + d_out << ")"; + } +} + +void LfscPrintChannelOut::printProofId(size_t id) +{ + d_out << " "; + printProofId(d_out, id); +} +void LfscPrintChannelOut::printAssumeId(size_t id) +{ + d_out << " "; + printAssumeId(d_out, id); +} + +void LfscPrintChannelOut::printEndLine() { d_out << std::endl; } + +void LfscPrintChannelOut::printNodeInternal(std::ostream& out, Node n) +{ + // due to use of special names in the node converter, we must clean symbols + std::stringstream ss; + n.toStream(ss, -1, 0, Language::LANG_SMTLIB_V2_6); + std::string s = ss.str(); + cleanSymbols(s); + out << s; +} + +void LfscPrintChannelOut::printTypeNodeInternal(std::ostream& out, TypeNode tn) +{ + // due to use of special names in the node converter, we must clean symbols + std::stringstream ss; + tn.toStream(ss, Language::LANG_SMTLIB_V2_6); + std::string s = ss.str(); + cleanSymbols(s); + out << s; +} + +void LfscPrintChannelOut::printRule(std::ostream& out, const ProofNode* pn) +{ + if (pn->getRule() == PfRule::LFSC_RULE) + { + const std::vector& args = pn->getArguments(); + out << getLfscRule(args[0]); + return; + } + // Otherwise, convert to lower case + std::stringstream ss; + ss << pn->getRule(); + std::string rname = ss.str(); + std::transform( + rname.begin(), rname.end(), rname.begin(), [](unsigned char c) { + return std::tolower(c); + }); + out << rname; +} + +void LfscPrintChannelOut::printId(std::ostream& out, size_t id) +{ + out << "__t" << id; +} + +void LfscPrintChannelOut::printProofId(std::ostream& out, size_t id) +{ + out << "__p" << id; +} + +void LfscPrintChannelOut::printAssumeId(std::ostream& out, size_t id) +{ + out << "__a" << id; +} + +void LfscPrintChannelOut::cleanSymbols(std::string& s) +{ + size_t start_pos = 0; + while ((start_pos = s.find("(_ ", start_pos)) != std::string::npos) + { + s.replace(start_pos, 3, "("); + start_pos += 1; + } + start_pos = 0; + while ((start_pos = s.find("__LFSC_TMP", start_pos)) != std::string::npos) + { + s.replace(start_pos, 10, ""); + } +} + +LfscPrintChannelPre::LfscPrintChannelPre(LetBinding& lbind) : d_lbind(lbind) {} + +void LfscPrintChannelPre::printNode(TNode n) { d_lbind.process(n); } +void LfscPrintChannelPre::printTrust(TNode res, PfRule src) +{ + d_lbind.process(res); +} + +void LfscPrintChannelPre::printOpenRule(const ProofNode* pn) +{ + +} + +} // namespace proof +} // namespace cvc5 diff --git a/src/proof/lfsc/lfsc_print_channel.h b/src/proof/lfsc/lfsc_print_channel.h new file mode 100644 index 000000000..655fa192c --- /dev/null +++ b/src/proof/lfsc/lfsc_print_channel.h @@ -0,0 +1,128 @@ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Print channels for LFSC proofs. + */ + +#include "cvc5_private.h" + +#ifndef CVC4__PROOF__LFSC__LFSC_PRINT_CHANNEL_H +#define CVC4__PROOF__LFSC__LFSC_PRINT_CHANNEL_H + +#include +#include + +#include "expr/node.h" +#include "printer/let_binding.h" +#include "proof/lfsc/lfsc_util.h" +#include "proof/proof_node.h" + +namespace cvc5 { +namespace proof { + +/** + * LFSC proofs are printed in two phases: the first phase computes the + * letification of terms in the proof as well as other information that is + * required for printing the preamble of the proof. The second phase prints the + * proof to an output stream. This is the base class for these two phases. + */ +class LfscPrintChannel +{ + public: + LfscPrintChannel() {} + virtual ~LfscPrintChannel() {} + /** Print node n */ + virtual void printNode(TNode n) {} + /** Print type node n */ + virtual void printTypeNode(TypeNode tn) {} + /** Print a hole */ + virtual void printHole() {} + /** + * Print an application of the trusting the result res, whose source is the + * given proof rule. + */ + virtual void printTrust(TNode res, PfRule src) {} + /** Print the opening of the rule of proof rule pn, e.g. "(and_elim ". */ + virtual void printOpenRule(const ProofNode* pn) {} + /** Print the opening of LFSC rule lr, e.g. "(cong " */ + virtual void printOpenLfscRule(LfscRule lr) {} + /** Print the closing of # nparen proof rules */ + virtual void printCloseRule(size_t nparen = 1) {} + /** Print a letified proof with the given identifier */ + virtual void printProofId(size_t id) {} + /** Print a proof assumption with the given identifier */ + virtual void printAssumeId(size_t id) {} + /** Print an end line */ + virtual void printEndLine() {} +}; + +/** Prints the proof to output stream d_out */ +class LfscPrintChannelOut : public LfscPrintChannel +{ + public: + LfscPrintChannelOut(std::ostream& out); + void printNode(TNode n) override; + void printTypeNode(TypeNode tn) override; + void printHole() override; + void printTrust(TNode res, PfRule src) override; + void printOpenRule(const ProofNode* pn) override; + void printOpenLfscRule(LfscRule lr) override; + void printCloseRule(size_t nparen = 1) override; + void printProofId(size_t id) override; + void printAssumeId(size_t id) override; + void printEndLine() override; + //------------------- helper methods + /** + * Print node to stream in the expected format of LFSC. + */ + static void printNodeInternal(std::ostream& out, Node n); + /** + * Print type node to stream in the expected format of LFSC. + */ + static void printTypeNodeInternal(std::ostream& out, TypeNode tn); + static void printRule(std::ostream& out, const ProofNode* pn); + static void printId(std::ostream& out, size_t id); + static void printProofId(std::ostream& out, size_t id); + static void printAssumeId(std::ostream& out, size_t id); + //------------------- end helper methods + private: + /** + * Replaces "(_ " with "(" to eliminate indexed symbols + * Replaces "__LFSC_TMP" with "" + */ + static void cleanSymbols(std::string& s); + /** The output stream */ + std::ostream& d_out; +}; + +/** + * Run on the proof before it is printed, and does two preparation steps: + * - Computes the letification of nodes that appear in the proof. + * - Computes the set of DSL rules that appear in the proof. + */ +class LfscPrintChannelPre : public LfscPrintChannel +{ + public: + LfscPrintChannelPre(LetBinding& lbind); + void printNode(TNode n) override; + void printTrust(TNode res, PfRule src) override; + void printOpenRule(const ProofNode* pn) override; + + private: + /** The let binding */ + LetBinding& d_lbind; +}; + +} // namespace proof +} // namespace cvc5 + +#endif