From: Andrew Reynolds Date: Fri, 1 Oct 2021 14:07:34 +0000 (-0500) Subject: Add the LFSC printer (#7158) X-Git-Tag: cvc5-1.0.0~1140 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e2675f8a1eb18be5697493d89ac97347e598c57d;p=cvc5.git Add the LFSC printer (#7158) This adds the LFSC printer for proof nodes. This PR has been split to not include support for DSL rewrite rules yet, or its main print method which will be added in a followup PR. Further PRs will connect this printer as a possible output format for cvc5. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index fe9267bed..f78e951d3 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -180,12 +180,16 @@ libcvc5_add_sources( proof/lfsc/lfsc_node_converter.h proof/lfsc/lfsc_post_processor.cpp proof/lfsc/lfsc_post_processor.h + proof/lfsc/lfsc_printer.cpp + proof/lfsc/lfsc_printer.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 proof/method_id.h + proof/print_expr.cpp + proof/print_expr.h proof/proof.cpp proof/proof.h proof/proof_checker.cpp diff --git a/src/proof/lfsc/lfsc_printer.cpp b/src/proof/lfsc/lfsc_printer.cpp new file mode 100644 index 000000000..743c5fab2 --- /dev/null +++ b/src/proof/lfsc/lfsc_printer.cpp @@ -0,0 +1,517 @@ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * The printer for LFSC proofs + */ + +#include "proof/lfsc/lfsc_printer.h" + +#include + +#include "expr/dtype.h" +#include "expr/dtype_cons.h" +#include "expr/dtype_selector.h" +#include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" +#include "proof/lfsc/lfsc_list_sc_node_converter.h" +#include "proof/lfsc/lfsc_print_channel.h" + +using namespace cvc5::kind; + +namespace cvc5 { +namespace proof { + +LfscPrinter::LfscPrinter(LfscNodeConverter& ltp) + : d_tproc(ltp), d_assumpCounter(0) +{ + NodeManager* nm = NodeManager::currentNM(); + d_boolType = nm->booleanType(); + // used for the `flag` type in LFSC + d_tt = d_tproc.mkInternalSymbol("tt", d_boolType); + d_ff = d_tproc.mkInternalSymbol("ff", d_boolType); +} + +void LfscPrinter::print(std::ostream& out, + const std::vector& assertions, + const ProofNode* pn) +{ + // to be added +} + +void LfscPrinter::printProofLetify( + LfscPrintChannel* out, + const ProofNode* pn, + const LetBinding& lbind, + const std::vector& pletList, + std::map& pletMap, + std::map& passumeMap) +{ + // closing parentheses + size_t cparen = 0; + + // define the let proofs + if (!pletList.empty()) + { + std::map::iterator itp; + for (const ProofNode* p : pletList) + { + itp = pletMap.find(p); + Assert(itp != pletMap.end()); + size_t pid = itp->second; + // print (plet _ _ + out->printOpenLfscRule(LfscRule::PLET); + cparen++; + out->printHole(); + out->printHole(); + out->printEndLine(); + // print the letified proof + pletMap.erase(p); + printProofInternal(out, p, lbind, pletMap, passumeMap); + pletMap[p] = pid; + // print the lambda (\ __pX + out->printOpenLfscRule(LfscRule::LAMBDA); + cparen++; + out->printProofId(pid); + out->printEndLine(); + } + out->printEndLine(); + } + + // [2] print the proof body + printProofInternal(out, pn, lbind, pletMap, passumeMap); + + // print the closing parenthesis + out->printCloseRule(cparen); +} + +void LfscPrinter::printProofInternal( + LfscPrintChannel* out, + const ProofNode* pn, + const LetBinding& lbind, + const std::map& pletMap, + std::map& passumeMap) +{ + // the stack + std::vector visit; + // whether we have to process children + std::unordered_set processingChildren; + // helper iterators + std::unordered_set::iterator pit; + std::map::const_iterator pletIt; + std::map::iterator passumeIt; + Node curn; + TypeNode curtn; + const ProofNode* cur; + visit.push_back(PExpr(pn)); + do + { + curn = visit.back().d_node; + curtn = visit.back().d_typeNode; + cur = visit.back().d_pnode; + visit.pop_back(); + // case 1: printing a proof + if (cur != nullptr) + { + PfRule r = cur->getRule(); + // maybe it is letified + pletIt = pletMap.find(cur); + if (pletIt != pletMap.end()) + { + // a letified proof + out->printProofId(pletIt->second); + continue; + } + pit = processingChildren.find(cur); + if (pit == processingChildren.end()) + { + bool isLambda = false; + if (r == PfRule::LFSC_RULE) + { + Assert(!cur->getArguments().empty()); + LfscRule lr = getLfscRule(cur->getArguments()[0]); + isLambda = (lr == LfscRule::LAMBDA); + } + else if (r == PfRule::ASSUME) + { + // an assumption, must have a name + passumeIt = passumeMap.find(cur->getResult()); + Assert(passumeIt != passumeMap.end()); + out->printAssumeId(passumeIt->second); + } + if (isLambda) + { + Assert(cur->getArguments().size() == 3); + // lambdas are handled specially. We print in a self contained way + // here. + // allocate an assumption, if necessary + size_t pid; + Node assumption = cur->getArguments()[2]; + passumeIt = passumeMap.find(assumption); + if (passumeIt == passumeMap.end()) + { + pid = d_assumpCounter; + d_assumpCounter++; + passumeMap[assumption] = pid; + } + else + { + pid = passumeIt->second; + } + // make the node whose name is the assumption id, where notice that + // the type of this node does not matter + std::stringstream pidNodeName; + LfscPrintChannelOut::printAssumeId(pidNodeName, pid); + // must be an internal symbol so that it is not turned into (bvar ...) + Node pidNode = + d_tproc.mkInternalSymbol(pidNodeName.str(), d_boolType); + // print "(\ " + out->printOpenRule(cur); + // print the identifier + out->printNode(pidNode); + // Print the body of the proof with a fresh proof letification. We can + // keep the assumption map and the let binding (for terms). + std::vector pletListNested; + std::map pletMapNested; + const ProofNode* curBody = cur->getChildren()[0].get(); + computeProofLetification(curBody, pletListNested, pletMapNested); + printProofLetify( + out, curBody, lbind, pletListNested, pletMapNested, passumeMap); + // print ")" + out->printCloseRule(); + } + else + { + // assert that we should traverse cur when letifying + Assert(d_lpltc.shouldTraverse(cur)); + // a normal rule application, compute the proof arguments, which + // notice in the case of PI also may modify our passumeMap. + std::vector args; + if (computeProofArgs(cur, args)) + { + processingChildren.insert(cur); + // will revisit this proof node to close parentheses + visit.push_back(PExpr(cur)); + std::reverse(args.begin(), args.end()); + visit.insert(visit.end(), args.begin(), args.end()); + // print the rule name + out->printOpenRule(cur); + } + else + { + // could not print the rule, trust for now + Node res = d_tproc.convert(cur->getResult()); + res = lbind.convert(res, "__t", true); + out->printTrust(res, r); + if (d_trustWarned.find(r) == d_trustWarned.end()) + { + d_trustWarned.insert(r); + } + } + } + } + else + { + processingChildren.erase(cur); + out->printCloseRule(); + } + } + // case 2: printing a node + else if (!curn.isNull()) + { + // it has already been converted to internal form, we letify it here + Node curni = lbind.convert(curn, "__t", true); + out->printNode(curni); + } + // case 3: printing a type node + else if (!curtn.isNull()) + { + out->printTypeNode(curtn); + } + // case 4: a hole + else + { + out->printHole(); + } + } while (!visit.empty()); +} + +bool LfscPrinter::computeProofArgs(const ProofNode* pn, + std::vector& pargs) +{ + const std::vector>& children = pn->getChildren(); + std::vector cs; + for (const std::shared_ptr& c : children) + { + cs.push_back(c.get()); + } + PfRule r = pn->getRule(); + const std::vector& args = pn->getArguments(); + std::vector as; + for (const Node& a : args) + { + Node ac = d_tproc.convert(a); + Assert(!ac.isNull()); + as.push_back(ac); + } + // The proof expression stream, which packs the next expressions (proofs, + // terms, sorts, LFSC datatypes) into a print-expression vector pargs. This + // stream can be used via "pf << e" which appends an expression to the + // vector maintained by this stream. + PExprStream pf(pargs, d_tt, d_ff); + // hole + PExpr h; + Trace("lfsc-print-debug2") + << "Compute proof args " << r << " #children= " << cs.size() + << " #args=" << as.size() << std::endl; + switch (r) + { + // SAT + case PfRule::RESOLUTION: + pf << h << h << h << cs[0] << cs[1] << args[0].getConst() << as[1]; + break; + case PfRule::REORDERING: pf << h << as[0] << cs[0]; break; + case PfRule::FACTORING: pf << h << h << cs[0]; break; + // Boolean + case PfRule::SPLIT: pf << as[0]; break; + case PfRule::NOT_NOT_ELIM: pf << h << cs[0]; break; + case PfRule::CONTRA: pf << h << cs[0] << cs[1]; break; + case PfRule::MODUS_PONENS: + case PfRule::EQ_RESOLVE: pf << h << h << cs[0] << cs[1]; break; + case PfRule::NOT_AND: pf << h << h << cs[0]; break; + case PfRule::NOT_OR_ELIM: + case PfRule::AND_ELIM: pf << h << h << args[0] << cs[0]; break; + case PfRule::IMPLIES_ELIM: + case PfRule::NOT_IMPLIES_ELIM1: + case PfRule::NOT_IMPLIES_ELIM2: + case PfRule::EQUIV_ELIM1: + case PfRule::EQUIV_ELIM2: + case PfRule::NOT_EQUIV_ELIM1: + case PfRule::NOT_EQUIV_ELIM2: + case PfRule::XOR_ELIM1: + case PfRule::XOR_ELIM2: + case PfRule::NOT_XOR_ELIM1: + case PfRule::NOT_XOR_ELIM2: pf << h << h << cs[0]; break; + case PfRule::ITE_ELIM1: + case PfRule::ITE_ELIM2: + case PfRule::NOT_ITE_ELIM1: + case PfRule::NOT_ITE_ELIM2: pf << h << h << h << cs[0]; break; + // CNF + case PfRule::CNF_AND_POS: + case PfRule::CNF_OR_NEG: + // print second argument as a raw integer (mpz) + pf << h << as[0] << args[1]; + break; + case PfRule::CNF_AND_NEG: pf << h << as[0]; break; + case PfRule::CNF_OR_POS: + pf << as[0]; + break; + break; + case PfRule::CNF_IMPLIES_POS: + case PfRule::CNF_IMPLIES_NEG1: + case PfRule::CNF_IMPLIES_NEG2: + case PfRule::CNF_EQUIV_POS1: + case PfRule::CNF_EQUIV_POS2: + case PfRule::CNF_EQUIV_NEG1: + case PfRule::CNF_EQUIV_NEG2: + case PfRule::CNF_XOR_POS1: + case PfRule::CNF_XOR_POS2: + case PfRule::CNF_XOR_NEG1: + case PfRule::CNF_XOR_NEG2: pf << as[0][0] << as[0][1]; break; + case PfRule::CNF_ITE_POS1: + case PfRule::CNF_ITE_POS2: + case PfRule::CNF_ITE_POS3: + case PfRule::CNF_ITE_NEG1: + case PfRule::CNF_ITE_NEG2: + case PfRule::CNF_ITE_NEG3: pf << as[0][0] << as[0][1] << as[0][2]; break; + // equality + case PfRule::REFL: pf << as[0]; break; + case PfRule::SYMM: pf << h << h << cs[0]; break; + case PfRule::TRANS: pf << h << h << h << cs[0] << cs[1]; break; + case PfRule::TRUE_INTRO: + case PfRule::FALSE_INTRO: + case PfRule::TRUE_ELIM: + case PfRule::FALSE_ELIM: pf << h << cs[0]; break; + // arithmetic + case PfRule::ARITH_MULT_POS: + case PfRule::ARITH_MULT_NEG: + { + pf << h << as[0] << as[1]; + } + break; + case PfRule::ARITH_TRICHOTOMY: + { + // should be robust to different orderings + pf << h << h << h << cs[0] << cs[1]; + } + break; + // strings + case PfRule::STRING_LENGTH_POS: pf << as[0]; break; + case PfRule::STRING_LENGTH_NON_EMPTY: pf << h << cs[0]; break; + case PfRule::RE_INTER: pf << h << h << h << cs[0] << cs[1]; break; + case PfRule::CONCAT_EQ: + pf << h << h << h << args[0].getConst() << cs[0]; + break; + case PfRule::CONCAT_UNIFY: + pf << h << h << h << h << args[0].getConst() << cs[0] << cs[1]; + break; + case PfRule::CONCAT_CSPLIT: + pf << h << h << h << h << args[0].getConst() << cs[0] << cs[1]; + break; + break; + case PfRule::RE_UNFOLD_POS: + if (children[0]->getResult()[1].getKind() != REGEXP_CONCAT) + { + return false; + } + pf << h << h << h << cs[0]; + break; + case PfRule::STRING_EAGER_REDUCTION: + { + Kind k = as[0].getKind(); + if (k == STRING_TO_CODE || k == STRING_CONTAINS || k == STRING_INDEXOF) + { + pf << h << as[0] << as[0][0].getType(); + } + else + { + // not yet defined for other kinds + return false; + } + } + break; + case PfRule::STRING_REDUCTION: + { + Kind k = as[0].getKind(); + if (k == STRING_SUBSTR || k == STRING_INDEXOF) + { + pf << h << as[0] << as[0][0].getType(); + } + else + { + // not yet defined for other kinds + return false; + } + } + break; + // quantifiers + case PfRule::SKOLEM_INTRO: + { + pf << h << d_tproc.convert(SkolemManager::getOriginalForm(args[0])); + } + break; + // ---------- arguments of non-translated rules go here + case PfRule::LFSC_RULE: + { + LfscRule lr = getLfscRule(args[0]); + // lambda should be processed elsewhere + Assert(lr != LfscRule::LAMBDA); + // Note that `args` has 2 builtin arguments, thus the first real argument + // begins at index 2 + switch (lr) + { + case LfscRule::SCOPE: pf << h << as[2] << cs[0]; break; + case LfscRule::NEG_SYMM: pf << h << h << cs[0]; break; + case LfscRule::CONG: pf << h << h << h << h << cs[0] << cs[1]; break; + case LfscRule::AND_INTRO1: pf << h << cs[0]; break; + case LfscRule::NOT_AND_REV: pf << h << h << cs[0]; break; + case LfscRule::PROCESS_SCOPE: pf << h << h << as[2] << cs[0]; break; + case LfscRule::AND_INTRO2: pf << h << h << cs[0] << cs[1]; break; + case LfscRule::ARITH_SUM_UB: pf << h << h << h << cs[0] << cs[1]; break; + default: return false; break; + } + } + break; + default: + { + return false; + break; + } + } + return true; +} + +void LfscPrinter::computeProofLetification( + const ProofNode* pn, + std::vector& pletList, + std::map& pletMap) +{ + // use callback to specify to stop at LAMBDA + ProofLetify::computeProofLet(pn, pletList, pletMap, 2, &d_lpltc); +} + +void LfscPrinter::print(std::ostream& out, Node n) +{ + Node ni = d_tproc.convert(n); + printLetify(out, ni); +} + +void LfscPrinter::printLetify(std::ostream& out, Node n) +{ + // closing parentheses + std::stringstream cparen; + + LetBinding lbind; + lbind.process(n); + + // [1] print the letification + printLetList(out, cparen, lbind); + + // [2] print the body + printInternal(out, n, lbind); + + out << cparen.str(); +} + +void LfscPrinter::printLetList(std::ostream& out, + std::ostream& cparen, + LetBinding& lbind) +{ + std::vector letList; + lbind.letify(letList); + std::map::const_iterator it; + for (size_t i = 0, nlets = letList.size(); i < nlets; i++) + { + Node nl = letList[i]; + out << "(@ "; + size_t id = lbind.getId(nl); + Assert(id != 0); + LfscPrintChannelOut::printId(out, id); + out << " "; + // remove, print, insert again + printInternal(out, nl, lbind, false); + out << std::endl; + cparen << ")"; + } +} + +void LfscPrinter::printInternal(std::ostream& out, Node n) +{ + LetBinding lbind; + printInternal(out, n, lbind); +} +void LfscPrinter::printInternal(std::ostream& out, + Node n, + LetBinding& lbind, + bool letTop) +{ + Node nc = lbind.convert(n, "__t", letTop); + LfscPrintChannelOut::printNodeInternal(out, nc); +} + +void LfscPrinter::printType(std::ostream& out, TypeNode tn) +{ + TypeNode tni = d_tproc.convertType(tn); + LfscPrintChannelOut::printTypeNodeInternal(out, tni); +} + +} // namespace proof +} // namespace cvc5 diff --git a/src/proof/lfsc/lfsc_printer.h b/src/proof/lfsc/lfsc_printer.h new file mode 100644 index 000000000..fb5890394 --- /dev/null +++ b/src/proof/lfsc/lfsc_printer.h @@ -0,0 +1,147 @@ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * The printer for LFSC proofs + */ + +#include "cvc5_private.h" + +#ifndef CVC4__PROOF__LFSC__LFSC_PRINTER_H +#define CVC4__PROOF__LFSC__LFSC_PRINTER_H + +#include +#include + +#include "expr/node.h" +#include "printer/let_binding.h" +#include "proof/lfsc/lfsc_node_converter.h" +#include "proof/lfsc/lfsc_util.h" +#include "proof/print_expr.h" +#include "proof/proof_node.h" + +namespace cvc5 { +namespace proof { + +class LfscPrintChannel; + +/** + * The LFSC printer, which prints proof nodes in a proof that is checkable + * by LFSC using the signature, currently located at: + * https://github.com/CVC4/signatures/tree/master/lfsc/new. + * + * It expects to print proof nodes that have been processed by the LFSC + * proof post processor. + */ +class LfscPrinter +{ + public: + LfscPrinter(LfscNodeConverter& ltp); + ~LfscPrinter() {} + + /** + * Print the full proof of assertions => false by pn on output stream out. + */ + void print(std::ostream& out, + const std::vector& assertions, + const ProofNode* pn); + + /** + * Print node to stream in the expected format of LFSC. + */ + void print(std::ostream& out, Node n); + /** + * Print type node to stream in the expected format of LFSC. + */ + void printType(std::ostream& out, TypeNode n); + + private: + /** + * Print node to stream in the expected format of LFSC. + */ + void printLetify(std::ostream& out, Node n); + /** + * Print node to stream in the expected format of LFSC, where n has been + * processed by the LFSC node converter. + */ + void printInternal(std::ostream& out, Node n); + /** + * Print node n to stream in the expected format of LFSC, with let binding, + * where n has been processed by the LFSC node converter. + * + * @param out The output stream + * @param n The node to print + * @param lbind The let binding to consider + * @param letTop Whether we should consider the top-most application in n + * for the let binding (see LetBinding::convert). + */ + void printInternal(std::ostream& out, + Node n, + LetBinding& lbind, + bool letTop = true); + /** + * print let list, prints definitions of lbind on out in order, and closing + * parentheses on cparen. + */ + void printLetList(std::ostream& out, std::ostream& cparen, LetBinding& lbind); + + //------------------------------ printing proofs + /** + * Print proof internal, after term lets and proofs for assumptions have + * been computed. + */ + void printProofLetify(LfscPrintChannel* out, + const ProofNode* pn, + const LetBinding& lbind, + const std::vector& pletList, + std::map& pletMap, + std::map& passumeMap); + /** + * Print proof internal, after all mappings have been computed. + */ + void printProofInternal(LfscPrintChannel* out, + const ProofNode* pn, + const LetBinding& lbind, + const std::map& pletMap, + std::map& passumeMap); + /** + * Get the arguments for the proof node application. This adds the arguments + * of the given proof to the vector pargs. + * + * @return false if the proof cannot be printed in LFSC format. + */ + bool computeProofArgs(const ProofNode* pn, std::vector& pargs); + /** + * Compute proof letification for proof node pn. + */ + void computeProofLetification(const ProofNode* pn, + std::vector& pletList, + std::map& pletMap); + //------------------------------ end printing proofs + /** The term processor */ + LfscNodeConverter& d_tproc; + /** The proof traversal callback */ + LfscProofLetifyTraverseCallback d_lpltc; + /** true and false nodes */ + Node d_tt; + Node d_ff; + /** Boolean type */ + TypeNode d_boolType; + /** assumption counter */ + size_t d_assumpCounter; + /** for debugging the open rules, the set of PfRule we have warned about */ + std::unordered_set d_trustWarned; +}; + +} // namespace proof +} // namespace cvc5 + +#endif