From d34e563fe48c42aa06eea44191a21dcf29772339 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 14 Sep 2021 15:43:47 -0500 Subject: [PATCH] Utilities in preparation for print benchmark utility (#7190) This adds a few utilities in preparation for the print benchmark utility, which will replace our own dumping infrastructure. --- src/expr/dtype.cpp | 13 +++++++++++ src/expr/dtype.h | 6 +++++ src/printer/printer.cpp | 52 +++++++++++++++++++++++++++++++++++++++++ src/printer/printer.h | 8 +++++++ src/smt/command.cpp | 4 ++-- 5 files changed, 81 insertions(+), 2 deletions(-) diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index 31a22b44a..fdb397d39 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -895,6 +895,19 @@ const std::vector >& DType::getConstructors() return d_constructors; } +std::unordered_set DType::getSubfieldTypes() const +{ + std::unordered_set subFieldTypes; + for (std::shared_ptr ctor : d_constructors) + { + for (size_t i = 0, nargs = ctor->getNumArgs(); i < nargs; i++) + { + subFieldTypes.insert(ctor->getArgType(i)); + } + } + return subFieldTypes; +} + std::ostream& operator<<(std::ostream& os, const DType& dt) { // can only output datatypes in the cvc5 native language diff --git a/src/expr/dtype.h b/src/expr/dtype.h index a608b9adb..4f54f0af7 100644 --- a/src/expr/dtype.h +++ b/src/expr/dtype.h @@ -425,6 +425,12 @@ class DType const std::vector >& getConstructors() const; + /** + * Return the subfield types of this datatype. This is the set of all types T + * for which there exists an argument to a constructor of type T. + */ + std::unordered_set getSubfieldTypes() const; + /** prints this datatype to stream */ void toStream(std::ostream& out) const; diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index e038952c4..9bd68e697 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -204,6 +204,13 @@ void Printer::toStreamCmdDeclareFunction(std::ostream& out, printUnknownCommand(out, "declare-fun"); } +void Printer::toStreamCmdDeclareFunction(std::ostream& out, const Node& v) const +{ + std::stringstream vs; + vs << v; + toStreamCmdDeclareFunction(out, vs.str(), v.getType()); +} + void Printer::toStreamCmdDeclarePool(std::ostream& out, const std::string& id, TypeNode type, @@ -235,6 +242,25 @@ void Printer::toStreamCmdDefineFunction(std::ostream& out, printUnknownCommand(out, "define-fun"); } +void Printer::toStreamCmdDefineFunction(std::ostream& out, + Node v, + Node lambda) const +{ + std::stringstream vs; + vs << v; + std::vector formals; + Node body = lambda; + TypeNode rangeType = v.getType(); + if (body.getKind() == kind::LAMBDA) + { + formals.insert(formals.end(), lambda[0].begin(), lambda[0].end()); + body = lambda[1]; + Assert(rangeType.isFunction()); + rangeType = rangeType.getRangeType(); + } + toStreamCmdDefineFunction(out, vs.str(), formals, rangeType, body); +} + void Printer::toStreamCmdDefineFunctionRec( std::ostream& out, const std::vector& funcs, @@ -244,6 +270,32 @@ void Printer::toStreamCmdDefineFunctionRec( printUnknownCommand(out, "define-fun-rec"); } +void Printer::toStreamCmdDefineFunctionRec( + std::ostream& out, + const std::vector& funcs, + const std::vector& lambdas) const +{ + std::vector> formals; + std::vector formulas; + for (const Node& l : lambdas) + { + std::vector formalsVec; + Node formula; + if (l.getKind() == kind::LAMBDA) + { + formalsVec.insert(formalsVec.end(), l[0].begin(), l[0].end()); + formula = l[1]; + } + else + { + formula = l; + } + formals.emplace_back(formalsVec); + formulas.emplace_back(formula); + } + toStreamCmdDefineFunctionRec(out, funcs, formals, formulas); +} + void Printer::toStreamCmdSetUserAttribute(std::ostream& out, const std::string& attr, Node n) const diff --git a/src/printer/printer.h b/src/printer/printer.h index 5e141fe8f..5ffe07f77 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -87,6 +87,8 @@ class Printer virtual void toStreamCmdDeclareFunction(std::ostream& out, const std::string& id, TypeNode type) const; + /** Variant of above for a pre-existing variable */ + void toStreamCmdDeclareFunction(std::ostream& out, const Node& v) const; /** Print declare-pool command */ virtual void toStreamCmdDeclarePool(std::ostream& out, const std::string& id, @@ -109,6 +111,8 @@ class Printer const std::vector& formals, TypeNode range, Node formula) const; + /** Variant of above that takes the definition */ + void toStreamCmdDefineFunction(std::ostream& out, Node v, Node lambda) const; /** Print define-fun-rec command */ virtual void toStreamCmdDefineFunctionRec( @@ -116,6 +120,10 @@ class Printer const std::vector& funcs, const std::vector>& formals, const std::vector& formulas) const; + /** Variant of above that takes the definition */ + void toStreamCmdDefineFunctionRec(std::ostream& out, + const std::vector& funcs, + const std::vector& lambdas) const; /** Print set-user-attribute command */ void toStreamCmdSetUserAttribute(std::ostream& out, diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 522c38040..adfd2f71d 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1186,8 +1186,8 @@ void DeclareFunctionCommand::toStream(std::ostream& out, size_t dag, Language language) const { - Printer::getPrinter(language)->toStreamCmdDeclareFunction( - out, d_func.toString(), sortToTypeNode(d_sort)); + Printer::getPrinter(language)->toStreamCmdDeclareFunction(out, + termToNode(d_func)); } /* -------------------------------------------------------------------------- */ -- 2.30.2