From 46eabc0138c57d5c329e33f1bca111d8a2be9621 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 8 Apr 2022 16:37:09 -0500 Subject: [PATCH] Minor refactoring of smt2 printer (#8588) --- src/printer/smt2/smt2_printer.cpp | 105 +++++++++++++----------------- src/printer/smt2/smt2_printer.h | 12 +++- 2 files changed, 56 insertions(+), 61 deletions(-) diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index c9199c64d..91a3f2186 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1319,6 +1319,24 @@ std::string Smt2Printer::smtKindStringOf(const Node& n, Variant v) return smtKindString(k, v); } +void Smt2Printer::toStreamDeclareType(std::ostream& out, TypeNode tn) const +{ + out << "("; + if (tn.isFunction()) + { + const vector argTypes = tn.getArgTypes(); + if (argTypes.size() > 0) + { + copy(argTypes.begin(), + argTypes.end() - 1, + ostream_iterator(out, " ")); + out << argTypes.back(); + } + tn = tn.getRangeType(); + } + out << ") " << tn; +} + void Smt2Printer::toStreamType(std::ostream& out, TypeNode tn) const { // we currently must call TypeNode::toStream here. @@ -1539,21 +1557,9 @@ void Smt2Printer::toStreamCmdDeclareFunction(std::ostream& out, const std::string& id, TypeNode type) const { - out << "(declare-fun " << cvc5::internal::quoteSymbol(id) << " ("; - if (type.isFunction()) - { - const vector argTypes = type.getArgTypes(); - if (argTypes.size() > 0) - { - copy(argTypes.begin(), - argTypes.end() - 1, - ostream_iterator(out, " ")); - out << argTypes.back(); - } - type = type.getRangeType(); - } - - out << ") " << type << ')' << std::endl; + out << "(declare-fun " << cvc5::internal::quoteSymbol(id) << " "; + toStreamDeclareType(out, type); + out << ')' << std::endl; } void Smt2Printer::toStreamCmdDeclarePool( @@ -1579,25 +1585,9 @@ void Smt2Printer::toStreamCmdDefineFunction(std::ostream& out, TypeNode range, Node formula) const { - out << "(define-fun " << cvc5::internal::quoteSymbol(id) << " ("; - if (!formals.empty()) - { - vector::const_iterator i = formals.cbegin(); - for (;;) - { - out << "(" << (*i) << " " << (*i).getType() << ")"; - ++i; - if (i != formals.cend()) - { - out << " "; - } - else - { - break; - } - } - } - out << ") " << range << ' ' << formula << ')' << std::endl; + out << "(define-fun " << cvc5::internal::quoteSymbol(id) << " "; + toStreamSortedVarList(out, formals); + out << " " << range << ' ' << formula << ')' << std::endl; } void Smt2Printer::toStreamCmdDefineFunctionRec( @@ -1626,24 +1616,15 @@ void Smt2Printer::toStreamCmdDefineFunctionRec( } out << "("; } - out << funcs[i] << " ("; + out << funcs[i] << " "; // print its type signature - vector::const_iterator itf = formals[i].cbegin(); - while (itf != formals[i].cend()) - { - out << "(" << (*itf) << " " << (*itf).getType() << ")"; - ++itf; - if (itf != formals[i].cend()) - { - out << " "; - } - } + toStreamSortedVarList(out, formals[i]); TypeNode type = funcs[i].getType(); if (type.isFunction()) { type = type.getRangeType(); } - out << ") " << type; + out << " " << type; if (funcs.size() > 1) { out << ")"; @@ -1672,6 +1653,21 @@ void Smt2Printer::toStreamCmdDefineFunctionRec( out << ")" << std::endl; } +void Smt2Printer::toStreamSortedVarList(std::ostream& out, + const std::vector& vars) const +{ + out << "("; + for (size_t i = 0, nvars = vars.size(); i < nvars; i++) + { + out << "(" << vars[i] << " " << vars[i].getType() << ")"; + if (i + 1 < nvars) + { + out << " "; + } + } + out << ")"; +} + void Smt2Printer::toStreamCmdDeclareType(std::ostream& out, TypeNode type) const { @@ -1972,20 +1968,9 @@ void Smt2Printer::toStreamCmdSynthFun(std::ostream& out, bool isInv, TypeNode sygusType) const { - out << '(' << (isInv ? "synth-inv " : "synth-fun ") << f << ' ' << '('; - if (!vars.empty()) - { - // print variable list - std::vector::const_iterator i = vars.cbegin(), i_end = vars.cend(); - out << '(' << *i << ' ' << i->getType() << ')'; - ++i; - while (i != i_end) - { - out << " (" << *i << ' ' << i->getType() << ')'; - ++i; - } - } - out << ')'; + out << '(' << (isInv ? "synth-inv " : "synth-fun ") << f << ' '; + // print variable list + toStreamSortedVarList(out, vars); // if not invariant-to-synthesize, print return type if (!isInv) { diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 038aa703e..ad417b256 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -73,7 +73,6 @@ class Smt2Printer : public cvc5::internal::Printer void toStreamCmdDeclareFunction(std::ostream& out, const std::string& id, TypeNode type) const override; - /** Print declare-pool command */ void toStreamCmdDeclarePool(std::ostream& out, const std::string& id, @@ -280,6 +279,17 @@ class Smt2Printer : public cvc5::internal::Printer TNode n, int toDepth, LetBinding* lbind = nullptr) const; + /** + * Prints the vector as a sorted variable list + */ + void toStreamSortedVarList(std::ostream& out, + const std::vector& vars) const; + /** + * Prints a type as part of e.g. a declare-fun command. This prints either + * `() T` if the type T is not a function, or `(T1 ... Tn) Tr` if T is + * a function type with argument types T1 ... Tn and return Tr. + */ + void toStreamDeclareType(std::ostream& out, TypeNode tn) const; /** To stream type node, which ensures tn is printed in smt2 format */ void toStreamType(std::ostream& out, TypeNode tn) const; /** -- 2.30.2