Remove unused `DeclarationSequence` command (#8892)

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index eca052ee79f5483ac08b965153d7a4d889d57738..b89a4a9b655ba0447fc15c42ff4d833762bab038 100644 (file)
--- 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<cvc5::Command*>& 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<cvc5::Command*>& sequence) const
 {

diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h
index f349b1a4b9f346c7f2a8f0bc64889e24e1dff7a0..577b38587aef1f49003e64c6e21ae0ebc2d603b6 100644 (file)
--- 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<cvc5::Command*>& sequence) const override;
 
-  /** Print declaration sequence command */
-  void toStreamCmdDeclarationSequence(
-      std::ostream& out,
-      const std::vector<cvc5::Command*>& sequence) const override;
-
  private:
   void toStream(std::ostream& out,
                 TNode n,

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index ea38b2012ddfc0909c26c62b429be26ddece15a7..70811aea9fd31e71cad5f2dbbcb1b412c24f9c41 100644 (file)
--- 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<cvc5::Command*>& sequence) const
-{
-  printUnknownCommand(out, "sequence");
-}
-
 }  // namespace cvc5::internal

diff --git a/src/printer/printer.h b/src/printer/printer.h
index 3bdfd29f0afc78b74344c2166082f5d342775c7c..7262c2a39d781aa6096b39134d30f889acef63da 100644 (file)
--- 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<cvc5::Command*>& sequence) const;
 
-  /** Print declaration sequence command */
-  virtual void toStreamCmdDeclarationSequence(
-      std::ostream& out, const std::vector<cvc5::Command*>& 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 c49bd202f765b1e2f24fd4742a2f5a74d3e420ce..6cf212d22e503586dc0e1d4c9b861c642d3189a9 100644 (file)
--- 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<cvc5::Command*>& 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 0e7712254250b038d38c5468746279d27af15bb8..bfaa64b6172764c31a1fbcb1f5638caacbe8beac 100644 (file)
--- 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<cvc5::Command*>& sequence) const override;
 
-  /** Print declaration sequence command */
-  void toStreamCmdDeclarationSequence(
-      std::ostream& out,
-      const std::vector<cvc5::Command*>& 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 52d1f56e40ff34852f7e2a5cac97edb13e5cfabc..174c47e36d6f1f76c0fed111db0d882d93b81e92 100644 (file)
--- 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 6c0cf28e3de8f39b60d6ca5658722630810a7b33..beffab0d632b656f03e434035e8f4c5812c2a284 100644 (file)
--- 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 */