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.

11 files changed, 19 insertions, 62 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 623b0aedd..68499ad0d 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -370,20 +370,11 @@ command [std::unique_ptr<cvc5::Command>* cmd]
     }
   | /* check-sat */
     CHECK_SAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { if( PARSER_STATE->sygus() ){
+    { if (PARSER_STATE->sygus()) {
         PARSER_STATE->parseError("Sygus does not support check-sat command.");
       }
+      cmd->reset(new CheckSatCommand());
     }
-    ( term[expr, expr2]
-      { if(PARSER_STATE->strictModeEnabled()) {
-          PARSER_STATE->parseError(
-              "Extended commands (such as check-sat with an argument) are not "
-              "permitted while operating in strict compliance mode.");
-        }
-      }
-    | { expr = api::Term(); }
-    )
-    { cmd->reset(new CheckSatCommand(expr)); }
   | /* check-sat-assuming */
     CHECK_SAT_ASSUMING_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     ( LPAREN_TOK termList[terms,expr] RPAREN_TOK
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(
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 1573ce16b..427b79c67 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -30,8 +30,8 @@
 #include "expr/node.h"
 #include "expr/symbol_manager.h"
 #include "expr/type_node.h"
-#include "options/options.h"
 #include "options/main_options.h"
+#include "options/options.h"
 #include "options/printer_options.h"
 #include "options/smt_options.h"
 #include "printer/printer.h"
@@ -275,7 +275,6 @@ TypeNode Command::grammarToTypeNode(api::Grammar* grammar)
                             : sortToTypeNode(grammar->resolve());
 }
 
-
 /* -------------------------------------------------------------------------- */
 /* class EmptyCommand                                                         */
 /* -------------------------------------------------------------------------- */
@@ -450,20 +449,15 @@ void PopCommand::toStream(std::ostream& out,
 /* class CheckSatCommand                                                      */
 /* -------------------------------------------------------------------------- */
 
-CheckSatCommand::CheckSatCommand() : d_term() {}
+CheckSatCommand::CheckSatCommand() {}
 
-CheckSatCommand::CheckSatCommand(const api::Term& term) : d_term(term) {}
-
-api::Term CheckSatCommand::getTerm() const { return d_term; }
 void CheckSatCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   Trace("dtview::command") << "* ~COMMAND: " << getCommandName() << "~"
                            << std::endl;
   try
   {
-    d_result =
-        d_term.isNull() ? solver->checkSat() : solver->checkSatAssuming(d_term);
-
+    d_result = solver->checkSat();
     d_commandStatus = CommandSuccess::instance();
   }
   catch (exception& e)
@@ -473,6 +467,7 @@ void CheckSatCommand::invoke(api::Solver* solver, SymbolManager* sm)
 }
 
 api::Result CheckSatCommand::getResult() const { return d_result; }
+
 void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const
 {
   if (!ok())
@@ -488,7 +483,7 @@ void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const
 
 Command* CheckSatCommand::clone() const
 {
-  CheckSatCommand* c = new CheckSatCommand(d_term);
+  CheckSatCommand* c = new CheckSatCommand();
   c->d_result = d_result;
   return c;
 }
@@ -500,7 +495,7 @@ void CheckSatCommand::toStream(std::ostream& out,
                                size_t dag,
                                Language language) const
 {
-  Printer::getPrinter(language)->toStreamCmdCheckSat(out, termToNode(d_term));
+  Printer::getPrinter(language)->toStreamCmdCheckSat(out);
 }
 
 /* -------------------------------------------------------------------------- */
diff --git a/src/smt/command.h b/src/smt/command.h
index 0756714b6..5df891ead 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -607,9 +607,6 @@ class CVC5_EXPORT CheckSatCommand : public Command
 {
  public:
   CheckSatCommand();
-  CheckSatCommand(const api::Term& term);
-
-  api::Term getTerm() const;
   api::Result getResult() const;
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
@@ -621,7 +618,6 @@ class CVC5_EXPORT CheckSatCommand : public Command
                 Language language = Language::LANG_AUTO) const override;
 
  private:
-  api::Term d_term;
   api::Result d_result;
 }; /* class CheckSatCommand */
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f447773ad..99410593c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -782,7 +782,7 @@ Result SmtEngine::checkSat(const Node& assumption)
 {
   if (Dump.isOn("benchmark"))
   {
-    getPrinter().toStreamCmdCheckSat(d_env->getDumpOut(), assumption);
+    getPrinter().toStreamCmdCheckSatAssuming(d_env->getDumpOut(), {assumption});
   }
   std::vector<Node> assump;
   if (!assumption.isNull())
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 7fd786801..6fbac94e5 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1366,7 +1366,7 @@ void TheoryEngine::lemma(TrustNode tlemma,
     const Printer& printer = d_env.getPrinter();
     std::ostream& out = d_env.getDumpOut();
     printer.toStreamCmdSetInfo(out, "notes", "theory lemma: expect valid");
-    printer.toStreamCmdCheckSat(out, n);
+    printer.toStreamCmdCheckSatAssuming(out, {n});
   }
 
   // assert the lemma
@@ -1425,7 +1425,7 @@ void TheoryEngine::conflict(TrustNode tconflict, TheoryId theoryId)
     const Printer& printer = d_env.getPrinter();
     std::ostream& out = d_env.getDumpOut();
     printer.toStreamCmdSetInfo(out, "notes", "theory conflict: expect unsat");
-    printer.toStreamCmdCheckSat(out, conflict);
+    printer.toStreamCmdCheckSatAssuming(out, {conflict});
   }
 
   // In the multiple-theories case, we need to reconstruct the conflict