From 231eaa4afb7f65d14e75170ef74c75a6d1def7bc Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 3 Mar 2022 16:54:27 -0600 Subject: [PATCH] Fix datatype declaration printing in LFSC printer (#8222) --- src/proof/lfsc/lfsc_printer.cpp | 208 +++++++++++++++++++------------- src/proof/lfsc/lfsc_printer.h | 29 +++++ 2 files changed, 151 insertions(+), 86 deletions(-) diff --git a/src/proof/lfsc/lfsc_printer.cpp b/src/proof/lfsc/lfsc_printer.cpp index 3018d3b6b..329b9106f 100644 --- a/src/proof/lfsc/lfsc_printer.cpp +++ b/src/proof/lfsc/lfsc_printer.cpp @@ -80,91 +80,43 @@ void LfscPrinter::print(std::ostream& out, { // 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) + ensureTypeDefinitionPrinted(preamble, st, sts, tupleArity); + } + // print datatype definitions for the above sorts + for (const TypeNode& stc : sts) + { + if (!stc.isDatatype() || stc.getKind() == PARAMETRIC_DATATYPE) { - if (sts.find(stc) != sts.end()) - { - continue; - } - sts.insert(stc); - if (stc.isSort()) + // skip the instance of a parametric datatype + continue; + } + const DType& dt = stc.getDType(); + preamble << "; DATATYPE " << dt.getName() << std::endl; + NodeManager* nm = NodeManager::currentNM(); + for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) + { + const DTypeConstructor& cons = dt[i]; + std::string cname = d_tproc.getNameForUserNameOf(cons.getConstructor()); + // for now, must print as node to ensure same policy for printing + // variable names. For instance, this means that cvc.X is printed as + // LFSC identifier |cvc.X| if X contains symbols legal in LFSC but not + // SMT-LIB. (cvc5-projects/issues/466) We should disable printing quote + // escapes in the smt2 printing of LFSC converted terms. + Node cc = nm->mkBoundVar(cname, stc); + // print constructor/tester + preamble << "(declare " << cc << " term)" << std::endl; + for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++) { - preamble << "(declare "; - printType(preamble, stc); - preamble << " sort)" << std::endl; + const DTypeSelector& arg = cons[j]; + // print selector + std::string sname = d_tproc.getNameForUserNameOf(arg.getSelector()); + Node sc = nm->mkBoundVar(sname, stc); + preamble << "(declare " << sc << " term)" << 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 } + // testers and updaters are instances of parametric symbols + // shared selectors are instance of parametric symbol "sel" + preamble << "; END DATATYPE " << std::endl; } Trace("lfsc-print-debug") << "; print user symbols" << std::endl; // [1b] user declare function symbols @@ -262,6 +214,92 @@ void LfscPrinter::print(std::ostream& out, out << cparen.str() << std::endl; } +void LfscPrinter::ensureTypeDefinitionPrinted( + std::ostream& os, + TypeNode tn, + std::unordered_set& processed, + std::unordered_set& tupleArityProcessed) +{ + // 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(tn, ctypes); + + for (const TypeNode& stc : ctypes) + { + printTypeDefinition(os, stc, processed, tupleArityProcessed); + } +} + +void LfscPrinter::printTypeDefinition( + std::ostream& os, + TypeNode tn, + std::unordered_set& processed, + std::unordered_set& tupleArityProcessed) +{ + if (processed.find(tn) != processed.end()) + { + return; + } + processed.insert(tn); + if (tn.isSort()) + { + os << "(declare "; + printType(os, tn); + os << " sort)" << std::endl; + } + else if (tn.isDatatype()) + { + const DType& dt = tn.getDType(); + if (tn.getKind() == PARAMETRIC_DATATYPE) + { + // skip the instance of a parametric datatype + return; + } + if (dt.isTuple()) + { + const DTypeConstructor& cons = dt[0]; + size_t arity = cons.getNumArgs(); + if (tupleArityProcessed.find(arity) == tupleArityProcessed.end()) + { + tupleArityProcessed.insert(arity); + os << "(declare Tuple_" << arity << " "; + std::stringstream tcparen; + for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++) + { + os << "(! s" << j << " sort "; + tcparen << ")"; + } + os << "sort" << tcparen.str() << ")"; + } + os << std::endl; + } + else + { + os << "(declare "; + printType(os, tn); + std::stringstream cdttparens; + if (dt.isParametric()) + { + std::vector params = dt.getParameters(); + for (const TypeNode& p : params) + { + os << " (! " << p << " sort"; + cdttparens << ")"; + } + } + os << " sort)" << cdttparens.str() << std::endl; + } + // must also ensure the subfield types of the datatype are printed + std::unordered_set sftypes = dt.getSubfieldTypes(); + for (const TypeNode& sft : sftypes) + { + ensureTypeDefinitionPrinted(os, sft, processed, tupleArityProcessed); + } + } + // all other sorts are builtin into the LFSC signature +} + void LfscPrinter::printProofLetify( LfscPrintChannel* out, const ProofNode* pn, @@ -426,10 +464,7 @@ void LfscPrinter::printProofInternal( 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); - } + d_trustWarned.insert(r); } } } @@ -576,8 +611,9 @@ bool LfscPrinter::computeProofArgs(const ProofNode* pn, Assert(res[1].getKind() == CONST_RATIONAL); pf << h << h << d_tproc.convert(res[1]) << cs[0]; } + break; // strings - break;case PfRule::STRING_LENGTH_POS: + case PfRule::STRING_LENGTH_POS: pf << as[0] << d_tproc.convertType(as[0].getType()) << h; break; case PfRule::STRING_LENGTH_NON_EMPTY: pf << h << h << cs[0]; break; diff --git a/src/proof/lfsc/lfsc_printer.h b/src/proof/lfsc/lfsc_printer.h index fb5890394..3a6e36764 100644 --- a/src/proof/lfsc/lfsc_printer.h +++ b/src/proof/lfsc/lfsc_printer.h @@ -64,6 +64,35 @@ class LfscPrinter void printType(std::ostream& out, TypeNode n); private: + /** + * This ensures that the type definition of type tn has been + * printed, which ensures that all of its component types, and the + * user-defined subfields of datatype types among those are declared. This + * furthermore includes running to a fixed point in the case that tn contains + * subfield types that are themselves datatypes. + * Notice that type definitions do not include printing the symbols of the + * datatype. + * + * @param os The stream to print to + * @param tn The type to ensure the definition(s) are printed for + * @param processed The types whose definitions we have already printed + * @param tupleArityProcessed The arity of tuples that we have declared. + * Note this is only required until we have a more robust treatment of + * tuples in the LFSC signature + */ + void ensureTypeDefinitionPrinted( + std::ostream& os, + TypeNode tn, + std::unordered_set& processed, + std::unordered_set& tupleArityProcessed); + /** + * print type definition, which is the same as above, but does not process + * component types. + */ + void printTypeDefinition(std::ostream& os, + TypeNode tn, + std::unordered_set& processed, + std::unordered_set& tupleArityProcessed); /** * Print node to stream in the expected format of LFSC. */ -- 2.30.2