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.

diff --git a/examples/api/smtlib/extract.smt2 b/examples/api/smtlib/extract.smt2
index 8bbabb77ad150fec618d453c428261daca877c8a..1e6bd8ab98662fcfee6da5c22b9c1f6d383630bf 100644 (file)
--- a/examples/api/smtlib/extract.smt2
+++ b/examples/api/smtlib/extract.smt2
@@ -11,4 +11,4 @@
 (assert (= a_31_1 a_30_0))
 
 (echo "Check unsatisfiability assuming a_31_31 != a_0_0")
-(check-sat (not (= a_31_31 a_0_0)))
\ No newline at end of file
+(check-sat-assuming ((not (= a_31_31 a_0_0))))

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 623b0aedd0156f50fbf3b60a7871bba879bb415e..68499ad0d96cd69783582763bcff0ad668554482 100644 (file)
--- 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 7c1661e5e698c84fbb182e5924c715e09790ca9c..e8bdab039037048777a0cb91d5fb872c15d80db0 100644 (file)
--- 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 fd5742c603f0d2c894990d8df4dab9890e525069..cf4b532adf2ff10f3b96c37523ebd31d97e8028c 100644 (file)
--- 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 a29d2eb4df01bc1f3e639c939894b71b48ec84d3..ec0fdeda1c06ece731a8e023d6d05969f4297235 100644 (file)
--- 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 2a7cf1f4dd6a497f0adcb039c074b95441172add..8c8118aa933b5e24ce2b332d205d1e8898bb8007 100644 (file)
--- 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 cf3f683080b8f7ff4f10921129af5a0e257d6704..e6aff1ace22ca06d11acdfe5f225ec21cb04355e 100644 (file)
--- 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 f12fa6b050d5cf26cd3e53119a75229771ada9b4..06404170cfd42cc2d09485ea0a97f9fd110b33c7 100644 (file)
--- 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 1573ce16bcd8db0df79c73864a7b5add74ac5d66..427b79c67d6ff60c7507657786a61c4978663f7d 100644 (file)
--- 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 0756714b6c6673e742c7a1b745167af15f293259..5df891ead869dcc357514babf91768d96062095d 100644 (file)
--- 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 f447773ad75f2a623a815da83ca9322bb0fcdbc2..99410593c1c5aa3bbb1305dbd489b7a4e17a8abf 100644 (file)
--- 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 7fd786801bf1c962fcc71a8112f8c68d48cf5ea6..6fbac94e5da1fe582d483fd7c4a45f28a50b295e 100644 (file)
--- 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

diff --git a/test/regress/regress0/cores/issue4925.smt2 b/test/regress/regress0/cores/issue4925.smt2
index 951f7e0088fc0e787d5965a17a9317f0e024dfb8..62428b5651c0a6214425bb312799272e54a38671 100644 (file)
--- a/test/regress/regress0/cores/issue4925.smt2
+++ b/test/regress/regress0/cores/issue4925.smt2
@@ -12,5 +12,5 @@
 (assert (or (< a 1) (> c 1)))
 (check-sat)
 (assert (= b (- 1)))
-(check-sat true)
-(check-sat)
\ No newline at end of file
+(check-sat-assuming (true))
+(check-sat)

diff --git a/test/regress/regress0/cores/issue5238.smt2 b/test/regress/regress0/cores/issue5238.smt2
index ae3bed2e251322e78232f7b21e11130f97deb47e..faf72f0e1d0684bf3f9e18e434608228b76b25bb 100644 (file)
--- a/test/regress/regress0/cores/issue5238.smt2
+++ b/test/regress/regress0/cores/issue5238.smt2
@@ -10,5 +10,5 @@
 (assert (= (/ 0 a) 1))
 (check-sat)
 (assert (= (+ a b) 0))
-(check-sat (> b 1))
-(check-sat)
\ No newline at end of file
+(check-sat-assuming ((> b 1)))
+(check-sat)

diff --git a/test/regress/regress0/cores/issue5902.smt2 b/test/regress/regress0/cores/issue5902.smt2
index 809873003cd63d3a0d7dee35f54e43200b83f70d..3c930b26bfdf6ee73f69f6615a806d32dfdd50bc 100644 (file)
--- a/test/regress/regress0/cores/issue5902.smt2
+++ b/test/regress/regress0/cores/issue5902.smt2
@@ -1,3 +1,3 @@
 ; COMMAND-LINE: -q
 ; EXPECT: unsat
-(check-sat false)
+(check-sat-assuming (false))