From 9ac8cbdc2bfaa8f43b19216e0d2cce06f27fb00a Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 21 Jun 2022 13:23:54 -0700 Subject: [PATCH] Remove unused `DeclarationSequence` command (#8892) --- src/printer/ast/ast_printer.cpp | 13 ------------- src/printer/ast/ast_printer.h | 5 ----- src/printer/printer.cpp | 6 ------ src/printer/printer.h | 4 ---- src/printer/smt2/smt2_printer.cpp | 6 ------ src/printer/smt2/smt2_printer.h | 5 ----- src/smt/command.cpp | 10 ---------- src/smt/command.h | 5 ----- 8 files changed, 54 deletions(-) diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index eca052ee7..b89a4a9b6 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -230,19 +230,6 @@ void AstPrinter::toStreamCmdQuit(std::ostream& out) const out << "Quit()" << std::endl; } -void AstPrinter::toStreamCmdDeclarationSequence( - std::ostream& out, const std::vector& sequence) const -{ - out << "DeclarationSequence[" << endl; - for (cvc5::CommandSequence::const_iterator i = sequence.cbegin(); - i != sequence.cend(); - ++i) - { - out << *i << endl; - } - out << "]" << std::endl; -} - void AstPrinter::toStreamCmdCommandSequence( std::ostream& out, const std::vector& sequence) const { diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h index f349b1a4b..577b38587 100644 --- a/src/printer/ast/ast_printer.h +++ b/src/printer/ast/ast_printer.h @@ -148,11 +148,6 @@ class AstPrinter : public cvc5::internal::Printer std::ostream& out, const std::vector& sequence) const override; - /** Print declaration sequence command */ - void toStreamCmdDeclarationSequence( - std::ostream& out, - const std::vector& sequence) const override; - private: void toStream(std::ostream& out, TNode n, diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index ea38b2012..70811aea9 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -514,10 +514,4 @@ void Printer::toStreamCmdCommandSequence( printUnknownCommand(out, "sequence"); } -void Printer::toStreamCmdDeclarationSequence( - std::ostream& out, const std::vector& sequence) const -{ - printUnknownCommand(out, "sequence"); -} - } // namespace cvc5::internal diff --git a/src/printer/printer.h b/src/printer/printer.h index 3bdfd29f0..7262c2a39 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -287,10 +287,6 @@ class Printer virtual void toStreamCmdCommandSequence( std::ostream& out, const std::vector& sequence) const; - /** Print declaration sequence command */ - virtual void toStreamCmdDeclarationSequence( - std::ostream& out, const std::vector& sequence) const; - protected: /** Derived classes can construct, but no one else. */ Printer() {} diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index c49bd202f..6cf212d22 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1563,12 +1563,6 @@ void Smt2Printer::toStreamCmdCommandSequence( } } -void Smt2Printer::toStreamCmdDeclarationSequence( - std::ostream& out, const std::vector& sequence) const -{ - toStreamCmdCommandSequence(out, sequence); -} - void Smt2Printer::toStreamCmdDeclareFunction(std::ostream& out, const std::string& id, TypeNode type) const diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 0e7712254..bfaa64b61 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -256,11 +256,6 @@ class Smt2Printer : public cvc5::internal::Printer std::ostream& out, const std::vector& sequence) const override; - /** Print declaration sequence command */ - void toStreamCmdDeclarationSequence( - std::ostream& out, - const std::vector& sequence) const override; - /** * Get the string for a kind k, which returns how the kind k is printed in * the SMT-LIB format (with variant v). diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 52d1f56e4..174c47e36 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -960,16 +960,6 @@ void CommandSequence::toStream(std::ostream& out) const Printer::getPrinter(out)->toStreamCmdCommandSequence(out, d_commandSequence); } -/* -------------------------------------------------------------------------- */ -/* class DeclarationSequence */ -/* -------------------------------------------------------------------------- */ - -void DeclarationSequence::toStream(std::ostream& out) const -{ - Printer::getPrinter(out)->toStreamCmdDeclarationSequence(out, - d_commandSequence); -} - /* -------------------------------------------------------------------------- */ /* class DeclarationDefinitionCommand */ /* -------------------------------------------------------------------------- */ diff --git a/src/smt/command.h b/src/smt/command.h index 6c0cf28e3..beffab0d6 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1320,11 +1320,6 @@ class CVC5_EXPORT CommandSequence : public Command void toStream(std::ostream& out) const override; }; /* class CommandSequence */ -class CVC5_EXPORT DeclarationSequence : public CommandSequence -{ - void toStream(std::ostream& out) const override; -}; - } // namespace cvc5 #endif /* CVC5__COMMAND_H */ -- 2.30.2