From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Wed, 29 Sep 2021 21:32:31 +0000 (-0500) Subject: Remove support for extended `(check-sat )` command. (#7270) X-Git-Tag: cvc5-1.0.0~1157 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bed236463f34019a802c8f0ee66f386b77ac4446;p=cvc5.git Remove support for extended `(check-sat )` command. (#7270) This commit removes support for the extended `(check-sat )` command which overlaps in functionality with the standard `(check-sat-assuming (*))` command. --- diff --git a/examples/api/smtlib/extract.smt2 b/examples/api/smtlib/extract.smt2 index 8bbabb77a..1e6bd8ab9 100644 --- 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 623b0aedd..68499ad0d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -370,20 +370,11 @@ command [std::unique_ptr* 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& 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 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 diff --git a/test/regress/regress0/cores/issue4925.smt2 b/test/regress/regress0/cores/issue4925.smt2 index 951f7e008..62428b565 100644 --- 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 ae3bed2e2..faf72f0e1 100644 --- 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 809873003..3c930b26b 100644 --- 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))