From: Andrew Reynolds Date: Thu, 7 Oct 2021 17:45:50 +0000 (-0500) Subject: Finish the LFSC printer (#7285) X-Git-Tag: cvc5-1.0.0~1105 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cb20e47bc69a6bdf00ab255ed23b3cfd9c26c10b;p=cvc5.git Finish the LFSC printer (#7285) This adds the remaining implementation of the LFSC printer. It also corrects a bug introduced during merging the last PR. The printer will be connected to the proof manager in a follow up PR. It will also be extended with support for DSL proof rule printing when the infrastructure is added. --- diff --git a/src/proof/lfsc/lfsc_printer.cpp b/src/proof/lfsc/lfsc_printer.cpp index 743c5fab2..3772e2386 100644 --- a/src/proof/lfsc/lfsc_printer.cpp +++ b/src/proof/lfsc/lfsc_printer.cpp @@ -44,7 +44,222 @@ void LfscPrinter::print(std::ostream& out, const std::vector& assertions, const ProofNode* pn) { - // to be added + Trace("lfsc-print-debug") << "; ORIGINAL PROOF: " << *pn << std::endl; + Assert (!pn->getChildren().empty()); + // closing parentheses + std::stringstream cparen; + const ProofNode* pnBody = pn->getChildren()[0].get(); + + // clear the rules we have warned about + d_trustWarned.clear(); + + Trace("lfsc-print-debug") << "; print declarations" << std::endl; + // [1] compute and print the declarations + std::unordered_set syms; + std::unordered_set visited; + std::vector iasserts; + std::map passumeMap; + std::unordered_set types; + std::unordered_set typeVisited; + for (size_t i = 0, nasserts = assertions.size(); i < nasserts; i++) + { + Node a = assertions[i]; + expr::getSymbols(a, syms, visited); + expr::getTypes(a, types, typeVisited); + iasserts.push_back(d_tproc.convert(a)); + // remember the assumption name + passumeMap[a] = i; + } + d_assumpCounter = assertions.size(); + Trace("lfsc-print-debug") << "; print sorts" << std::endl; + // [1a] user declared sorts + std::stringstream preamble; + std::unordered_set sts; + std::unordered_set tupleArity; + for (const TypeNode& st : types) + { + // note that we must get all "component types" of a type, so that + // e.g. U is printed as a sort declaration when we have type (Array U Int). + std::unordered_set ctypes; + expr::getComponentTypes(st, ctypes); + for (const TypeNode& stc : ctypes) + { + if (sts.find(stc) != sts.end()) + { + continue; + } + sts.insert(stc); + if (stc.isSort()) + { + preamble << "(declare "; + printType(preamble, stc); + preamble << " sort)" << std::endl; + } + else if (stc.isDatatype()) + { + const DType& dt = stc.getDType(); + if (stc.getKind() == PARAMETRIC_DATATYPE) + { + // skip the instance of a parametric datatype + continue; + } + preamble << "; DATATYPE " << dt.getName() << std::endl; + if (dt.isTuple()) + { + const DTypeConstructor& cons = dt[0]; + size_t arity = cons.getNumArgs(); + if (tupleArity.find(arity) == tupleArity.end()) + { + tupleArity.insert(arity); + preamble << "(declare Tuple_" << arity << " "; + std::stringstream tcparen; + for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++) + { + preamble << "(! s" << j << " sort "; + tcparen << ")"; + } + preamble << "sort" << tcparen.str() << ")"; + } + preamble << std::endl; + } + else + { + preamble << "(declare "; + printType(preamble, stc); + std::stringstream cdttparens; + if (dt.isParametric()) + { + std::vector params = dt.getParameters(); + for (const TypeNode& tn : params) + { + preamble << " (! " << tn << " sort"; + cdttparens << ")"; + } + } + preamble << " sort)" << cdttparens.str() << std::endl; + } + for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) + { + const DTypeConstructor& cons = dt[i]; + std::stringstream sscons; + sscons << d_tproc.convert(cons.getConstructor()); + std::string cname = + LfscNodeConverter::getNameForUserName(sscons.str()); + // print construct/tester + preamble << "(declare " << cname << " term)" << std::endl; + for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++) + { + const DTypeSelector& arg = cons[j]; + // print selector + Node si = d_tproc.convert(arg.getSelector()); + std::stringstream sns; + sns << si; + std::string sname = + LfscNodeConverter::getNameForUserName(sns.str()); + preamble << "(declare " << sname << " term)" << std::endl; + } + } + // testers and updaters are instances of parametric symbols + // shared selectors are instance of parametric symbol "sel" + preamble << "; END DATATYPE " << std::endl; + } + // all other sorts are builtin into the LFSC signature + } + } + Trace("lfsc-print-debug") << "; print user symbols" << std::endl; + // [1b] user declare function symbols + for (const Node& s : syms) + { + TypeNode st = s.getType(); + if (st.isConstructor() || st.isSelector() || st.isTester() + || st.isUpdater()) + { + // constructors, selector, testers, updaters are defined by the datatype + continue; + } + Node si = d_tproc.convert(s); + preamble << "(define " << si << " (var " + << d_tproc.getOrAssignIndexForVar(s) << " "; + printType(preamble, st); + preamble << "))" << std::endl; + } + + Trace("lfsc-print-debug") << "; compute proof letification" << std::endl; + // [2] compute the proof letification + std::vector pletList; + std::map pletMap; + computeProofLetification(pnBody, pletList, pletMap); + + Trace("lfsc-print-debug") << "; compute term lets" << std::endl; + // compute the term lets + LetBinding lbind; + for (const Node& ia : iasserts) + { + lbind.process(ia); + } + // We do a "dry-run" of proof printing here, using the LetBinding print + // channel. This pass traverses the proof but does not print it, but instead + // updates the let binding data structure for all nodes that appear anywhere + // in the proof. + LfscPrintChannelPre lpcp(lbind); + LetBinding emptyLetBind; + std::map::iterator itp; + for (const ProofNode* p : pletList) + { + itp = pletMap.find(p); + Assert(itp != pletMap.end()); + size_t pid = itp->second; + pletMap.erase(p); + printProofInternal(&lpcp, p, emptyLetBind, pletMap, passumeMap); + pletMap[p] = pid; + } + // Print the body of the outermost scope + printProofInternal(&lpcp, pnBody, emptyLetBind, pletMap, passumeMap); + + // [3] print warnings + for (PfRule r : d_trustWarned) + { + out << "; WARNING: adding trust step for " << r << std::endl; + } + + // [4] print the DSL rewrite rule declarations + // TODO cvc5-projects #285. + + // [5] print the check command and term lets + out << preamble.str(); + out << "(check" << std::endl; + cparen << ")"; + // print the term let list + printLetList(out, cparen, lbind); + + Trace("lfsc-print-debug") << "; print asserts" << std::endl; + // [6] print the assertions, with letification + // the assumption identifier mapping + for (size_t i = 0, nasserts = iasserts.size(); i < nasserts; i++) + { + Node ia = iasserts[i]; + out << "(% "; + LfscPrintChannelOut::printAssumeId(out, i); + out << " (holds "; + printInternal(out, ia, lbind); + out << ")" << std::endl; + cparen << ")"; + } + + Trace("lfsc-print-debug") << "; print annotation" << std::endl; + // [7] print the annotation + out << "(: (holds false)" << std::endl; + cparen << ")"; + + Trace("lfsc-print-debug") << "; print proof body" << std::endl; + // [8] print the proof body + Assert(pn->getRule() == PfRule::SCOPE); + // the outermost scope can be ignored (it is the scope of the assertions, + // which are already printed above). + LfscPrintChannelOut lout(out); + printProofLetify(&lout, pnBody, lbind, pletList, pletMap, passumeMap); + + out << cparen.str() << std::endl; } void LfscPrinter::printProofLetify( @@ -140,14 +355,14 @@ void LfscPrinter::printProofInternal( LfscRule lr = getLfscRule(cur->getArguments()[0]); isLambda = (lr == LfscRule::LAMBDA); } - else if (r == PfRule::ASSUME) + 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) + else if (isLambda) { Assert(cur->getArguments().size() == 3); // lambdas are handled specially. We print in a self contained way