Remove support for extended `(check-sat <term>)` command. (#7270)

This commit removes support for the extended `(check-sat <term>)` command which overlaps in functionality with the standard `(check-sat-assuming (<prop_literal>*))` command.

6 files changed, 8 insertions, 33 deletions

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 7c1661e5e..e8bdab039 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -182,17 +182,9 @@ void AstPrinter::toStreamCmdPop(std::ostream& out) const {
   out << "Pop()" << std::endl;
 }
 
-void AstPrinter::toStreamCmdCheckSat(std::ostream& out, Node n) const
+void AstPrinter::toStreamCmdCheckSat(std::ostream& out) const
 {
-  if (n.isNull())
-  {
-    out << "CheckSat()";
-  }
-  else
-  {
-    out << "CheckSat(" << n << ')';
-  }
-  out << std::endl;
+  out << "CheckSat()" << std::endl;
 }
 
 void AstPrinter::toStreamCmdCheckSatAssuming(
diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h
index fd5742c60..cf4b532ad 100644
--- a/src/printer/ast/ast_printer.h
+++ b/src/printer/ast/ast_printer.h
@@ -80,8 +80,7 @@ class AstPrinter : public cvc5::Printer
                                  Node formula) const override;
 
   /** Print check-sat command */
-  void toStreamCmdCheckSat(std::ostream& out,
-                           Node n = Node::null()) const override;
+  void toStreamCmdCheckSat(std::ostream& out) const override;
 
   /** Print check-sat-assuming command */
   void toStreamCmdCheckSatAssuming(
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index a29d2eb4d..ec0fdeda1 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -299,7 +299,7 @@ void Printer::toStreamCmdSetUserAttribute(std::ostream& out,
   printUnknownCommand(out, "set-user-attribute");
 }
 
-void Printer::toStreamCmdCheckSat(std::ostream& out, Node n) const
+void Printer::toStreamCmdCheckSat(std::ostream& out) const
 {
   printUnknownCommand(out, "check-sat");
 }
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 2a7cf1f4d..8c8118aa9 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -131,8 +131,7 @@ class Printer
                                    Node n) const;
 
   /** Print check-sat command */
-  virtual void toStreamCmdCheckSat(std::ostream& out,
-                                   Node n = Node::null()) const;
+  virtual void toStreamCmdCheckSat(std::ostream& out) const;
 
   /** Print check-sat-assuming command */
   virtual void toStreamCmdCheckSatAssuming(
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index cf3f68308..e6aff1ace 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1363,23 +1363,9 @@ void Smt2Printer::toStreamCmdPop(std::ostream& out) const
   out << "(pop 1)" << std::endl;
 }
 
-void Smt2Printer::toStreamCmdCheckSat(std::ostream& out, Node n) const
+void Smt2Printer::toStreamCmdCheckSat(std::ostream& out) const
 {
-  if (!n.isNull())
-  {
-    toStreamCmdPush(out);
-    out << std::endl;
-    toStreamCmdAssert(out, n);
-    out << std::endl;
-    toStreamCmdCheckSat(out);
-    out << std::endl;
-    toStreamCmdPop(out);
-  }
-  else
-  {
-    out << "(check-sat)";
-  }
-  out << std::endl;
+  out << "(check-sat)" << std::endl;
 }
 
 void Smt2Printer::toStreamCmdCheckSatAssuming(
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index f12fa6b05..06404170c 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -99,8 +99,7 @@ class Smt2Printer : public cvc5::Printer
       const std::vector<Node>& formulas) const override;
 
   /** Print check-sat command */
-  void toStreamCmdCheckSat(std::ostream& out,
-                           Node n = Node::null()) const override;
+  void toStreamCmdCheckSat(std::ostream& out) const override;
 
   /** Print check-sat-assuming command */
   void toStreamCmdCheckSatAssuming(