From b5dec96e8e65591e7686c460a30a5c62d5becdcf Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 23 Jun 2022 13:51:05 -0700 Subject: [PATCH] Remove `CommandSequence` command (#8904) The CommandSequence command was not widely used and was essentially just replicating the functionality of a vector of commands. This is work towards a streamlined parser API. --- src/main/command_executor.cpp | 25 ++----- src/main/driver_unified.cpp | 23 ++++-- src/main/interactive_shell.cpp | 15 ++-- src/main/interactive_shell.h | 10 ++- src/parser/smt2/Smt2.g | 2 - src/parser/tptp/Tptp.g | 12 ++-- src/printer/ast/ast_printer.cpp | 13 ---- src/printer/ast/ast_printer.h | 5 -- src/printer/printer.cpp | 6 -- src/printer/printer.h | 4 -- src/printer/smt2/smt2_printer.cpp | 9 --- src/printer/smt2/smt2_printer.h | 5 -- src/smt/command.cpp | 84 ---------------------- src/smt/command.h | 33 --------- test/unit/main/interactive_shell_black.cpp | 19 ++--- 15 files changed, 51 insertions(+), 214 deletions(-) diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 96b771ac2..6e2104053 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -84,27 +84,12 @@ void CommandExecutor::printStatisticsSafe(int fd) const bool CommandExecutor::doCommand(Command* cmd) { - CommandSequence *seq = dynamic_cast(cmd); - if(seq != nullptr) { - // assume no error - bool status = true; - - for (CommandSequence::iterator subcmd = seq->begin(); - status && subcmd != seq->end(); - ++subcmd) - { - status = doCommand(*subcmd); - } - - return status; - } else { - if (d_solver->getOptionInfo("verbosity").intValue() > 2) - { - d_solver->getDriverOptions().out() << "Invoking: " << *cmd << std::endl; - } - - return doCommandSingleton(cmd); + if (d_solver->getOptionInfo("verbosity").intValue() > 2) + { + d_solver->getDriverOptions().out() << "Invoking: " << *cmd << std::endl; } + + return doCommandSingleton(cmd); } void CommandExecutor::reset() diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 859941cc5..7887ed08a 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -22,6 +22,7 @@ #include #include #include +#include #include "api/cpp/cvc5.h" #include "base/configuration.h" @@ -162,7 +163,6 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) solver->setInfo("filename", filenameStr); // Parse and execute commands until we are done - std::unique_ptr cmd; bool status = true; if (solver->getOptionInfo("interactive").boolValue() && inputFromStdin) { @@ -187,14 +187,23 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) << std::endl << Configuration::copyright() << std::endl; - while(true) { - cmd.reset(shell.readCommand()); - if (cmd == nullptr) - break; - status = pExecutor->doCommand(cmd) && status; - if (cmd->interrupted()) { + bool quit = false; + while (!quit) + { + std::optional cmds = shell.readCommand(); + if (!cmds) + { break; } + for (std::unique_ptr& cmd : *cmds) + { + status = pExecutor->doCommand(cmd) && status; + if (cmd->interrupted()) + { + quit = true; + break; + } + } } } else diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index d9f6ece6d..cd1f11881 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -17,12 +17,13 @@ */ #include "main/interactive_shell.h" -#include #include #include #include +#include #include +#include #include #include #include @@ -170,7 +171,7 @@ InteractiveShell::~InteractiveShell() { #endif /* HAVE_LIBEDITLINE */ } -Command* InteractiveShell::readCommand() +std::optional InteractiveShell::readCommand() { char* lineBuf = NULL; string line = ""; @@ -181,7 +182,7 @@ restart: * QuitCommand. */ if(d_in.eof() || d_quit) { d_out << endl; - return NULL; + return {}; } /* If something's wrong with the input, there's nothing we can do. */ @@ -248,7 +249,7 @@ restart: if(input.empty()) { /* Nothing left to parse. */ d_out << endl; - return NULL; + return {}; } /* Some input left to parse, but nothing left to read. @@ -306,14 +307,14 @@ restart: /* There may be more than one command in the input. Build up a sequence. */ - CommandSequence *cmd_seq = new CommandSequence(); + std::vector> cmdSeq; Command *cmd; try { while ((cmd = d_parser->nextCommand())) { - cmd_seq->addCommand(cmd); + cmdSeq.emplace_back(cmd); if (dynamic_cast(cmd) != NULL) { d_quit = true; @@ -376,7 +377,7 @@ restart: // cmd_seq = new CommandSequence(); } - return cmd_seq; + return std::optional(std::move(cmdSeq)); }/* InteractiveShell::readCommand() */ #if HAVE_LIBEDITLINE diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index 32b283d38..1943d7d16 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -18,7 +18,9 @@ #include #include +#include #include +#include namespace cvc5 { @@ -37,6 +39,8 @@ namespace parser { class InteractiveShell { public: + using CmdSeq = std::vector>; + InteractiveShell(Solver* solver, SymbolManager* sm, std::istream& in, @@ -48,10 +52,10 @@ namespace parser { ~InteractiveShell(); /** - * Read a command from the interactive shell. This will read as - * many lines as necessary to parse a well-formed command. + * Read a list of commands from the interactive shell. This will read as + * many lines as necessary to parse at least one well-formed command. */ - Command* readCommand(); + std::optional readCommand(); /** * Return the internal parser being used. diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index ee0738b11..bc5ee3147 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -725,7 +725,6 @@ smt25Command[std::unique_ptr* cmd] std::vector funcs; std::vector func_defs; cvc5::Term aexpr; - std::unique_ptr seq; std::vector sorts; std::vector flattenVars; } @@ -863,7 +862,6 @@ extendedCommand[std::unique_ptr* cmd] std::vector terms; std::vector sorts; std::vector > sortedVarNames; - std::unique_ptr seq; cvc5::Grammar* g = nullptr; } /* Extended SMT-LIB set of commands syntax, not permitted in diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 0db135c83..c238f324c 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -238,12 +238,11 @@ parseCommand returns [cvc5::Command* cmd = NULL] } | EOF { - CommandSequence* seq = new CommandSequence(); // assert that all distinct constants are distinct cvc5::Term aexpr = PARSER_STATE->getAssertionDistinctConstants(); if( !aexpr.isNull() ) { - seq->addCommand(new AssertCommand(aexpr)); + PARSER_STATE->preemptCommand(new AssertCommand(aexpr)); } std::string filename = PARSER_STATE->getInput()->getInputStreamName(); @@ -254,15 +253,14 @@ parseCommand returns [cvc5::Command* cmd = NULL] if(filename.substr(filename.length() - 2) == ".p") { filename = filename.substr(0, filename.length() - 2); } - seq->addCommand(new SetInfoCommand("filename", filename)); + PARSER_STATE->preemptCommand(new SetInfoCommand("filename", filename)); if(PARSER_STATE->hasConjecture()) { // note this does not impact how the TPTP status is reported currently - seq->addCommand(new CheckSatAssumingCommand(SOLVER->mkTrue())); + PARSER_STATE->preemptCommand(new CheckSatAssumingCommand(SOLVER->mkTrue())); } else { - seq->addCommand(new CheckSatCommand()); + PARSER_STATE->preemptCommand(new CheckSatCommand()); } - PARSER_STATE->preemptCommand(seq); - cmd = NULL; + cmd = nullptr; } ; diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index f91bf5d0d..c785be581 100644 --- 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::toStreamCmdCommandSequence( - std::ostream& out, const std::vector& sequence) const -{ - out << "cvc5::CommandSequence[" << endl; - for (cvc5::CommandSequence::const_iterator i = sequence.cbegin(); - i != sequence.cend(); - ++i) - { - out << *i << endl; - } - out << "]" << std::endl; -} - void AstPrinter::toStreamCmdDeclareFunction(std::ostream& out, const std::string& id, TypeNode type) const diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h index 577b38587..8cf8bec47 100644 --- a/src/printer/ast/ast_printer.h +++ b/src/printer/ast/ast_printer.h @@ -143,11 +143,6 @@ class AstPrinter : public cvc5::internal::Printer /** Print quit command */ void toStreamCmdQuit(std::ostream& out) const override; - /** Print command sequence command */ - void toStreamCmdCommandSequence( - std::ostream& out, - const std::vector& sequence) const override; - private: void toStream(std::ostream& out, TNode n, diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 70811aea9..7f7ad5c74 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -508,10 +508,4 @@ void Printer::toStreamCmdDeclareHeap(std::ostream& out, printUnknownCommand(out, "declare-heap"); } -void Printer::toStreamCmdCommandSequence( - std::ostream& out, const std::vector& sequence) const -{ - printUnknownCommand(out, "sequence"); -} - } // namespace cvc5::internal diff --git a/src/printer/printer.h b/src/printer/printer.h index 7262c2a39..ac71cb04b 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -283,10 +283,6 @@ class Printer TypeNode locType, TypeNode dataType) const; - /** Print command sequence command */ - virtual void toStreamCmdCommandSequence( - std::ostream& out, const std::vector& 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 c495f5618..58cdd7739 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1555,15 +1555,6 @@ void Smt2Printer::toStreamCmdQuit(std::ostream& out) const out << "(exit)" << std::endl; } -void Smt2Printer::toStreamCmdCommandSequence( - std::ostream& out, const std::vector& sequence) const -{ - for (cvc5::Command* i : sequence) - { - out << *i; - } -} - 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 bfaa64b61..1e19edf74 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -251,11 +251,6 @@ class Smt2Printer : public cvc5::internal::Printer TypeNode locType, TypeNode dataType) const override; - /** Print command sequence command */ - void toStreamCmdCommandSequence( - std::ostream& out, - const std::vector& 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 b2d7ccb8f..5599eab39 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -799,90 +799,6 @@ void QuitCommand::toStream(std::ostream& out) const Printer::getPrinter(out)->toStreamCmdQuit(out); } -/* -------------------------------------------------------------------------- */ -/* class CommandSequence */ -/* -------------------------------------------------------------------------- */ - -CommandSequence::CommandSequence() : d_index(0) {} -CommandSequence::~CommandSequence() -{ - for (unsigned i = d_index; i < d_commandSequence.size(); ++i) - { - delete d_commandSequence[i]; - } -} - -void CommandSequence::addCommand(Command* cmd) -{ - d_commandSequence.push_back(cmd); -} - -void CommandSequence::clear() { d_commandSequence.clear(); } -void CommandSequence::invoke(cvc5::Solver* solver, SymbolManager* sm) -{ - for (; d_index < d_commandSequence.size(); ++d_index) - { - d_commandSequence[d_index]->invoke(solver, sm); - if (!d_commandSequence[d_index]->ok()) - { - // abort execution - d_commandStatus = d_commandSequence[d_index]->getCommandStatus(); - return; - } - delete d_commandSequence[d_index]; - } - - AlwaysAssert(d_commandStatus == NULL); - d_commandStatus = CommandSuccess::instance(); -} - -void CommandSequence::invoke(cvc5::Solver* solver, - SymbolManager* sm, - std::ostream& out) -{ - for (; d_index < d_commandSequence.size(); ++d_index) - { - d_commandSequence[d_index]->invoke(solver, sm, out); - if (!d_commandSequence[d_index]->ok()) - { - // abort execution - d_commandStatus = d_commandSequence[d_index]->getCommandStatus(); - return; - } - delete d_commandSequence[d_index]; - } - - AlwaysAssert(d_commandStatus == NULL); - d_commandStatus = CommandSuccess::instance(); -} - -CommandSequence::const_iterator CommandSequence::begin() const -{ - return d_commandSequence.begin(); -} - -CommandSequence::const_iterator CommandSequence::end() const -{ - return d_commandSequence.end(); -} - -CommandSequence::iterator CommandSequence::begin() -{ - return d_commandSequence.begin(); -} - -CommandSequence::iterator CommandSequence::end() -{ - return d_commandSequence.end(); -} - -std::string CommandSequence::getCommandName() const { return "sequence"; } - -void CommandSequence::toStream(std::ostream& out) const -{ - Printer::getPrinter(out)->toStreamCmdCommandSequence(out, d_commandSequence); -} - /* -------------------------------------------------------------------------- */ /* class DeclarationDefinitionCommand */ /* -------------------------------------------------------------------------- */ diff --git a/src/smt/command.h b/src/smt/command.h index ba6e30f1b..534208205 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1216,39 +1216,6 @@ class CVC5_EXPORT QuitCommand : public Command void toStream(std::ostream& out) const override; }; /* class QuitCommand */ -class CVC5_EXPORT CommandSequence : public Command -{ - protected: - /** All the commands to be executed (in sequence) */ - std::vector d_commandSequence; - /** Next command to be executed */ - unsigned int d_index; - - public: - CommandSequence(); - ~CommandSequence(); - - void addCommand(Command* cmd); - void clear(); - - void invoke(cvc5::Solver* solver, SymbolManager* sm) override; - void invoke(cvc5::Solver* solver, - SymbolManager* sm, - std::ostream& out) override; - - typedef std::vector::iterator iterator; - typedef std::vector::const_iterator const_iterator; - - const_iterator begin() const; - const_iterator end() const; - - iterator begin(); - iterator end(); - - std::string getCommandName() const override; - void toStream(std::ostream& out) const override; -}; /* class CommandSequence */ - } // namespace cvc5 #endif /* CVC5__COMMAND_H */ diff --git a/test/unit/main/interactive_shell_black.cpp b/test/unit/main/interactive_shell_black.cpp index 134c5fcdf..d96a02a77 100644 --- a/test/unit/main/interactive_shell_black.cpp +++ b/test/unit/main/interactive_shell_black.cpp @@ -13,6 +13,7 @@ * Black box testing of cvc5::InteractiveShell. */ +#include #include #include @@ -65,12 +66,15 @@ class TestMainBlackInteractiveShell : public TestInternal uint32_t minCommands, uint32_t maxCommands) { - Command* cmd; uint32_t n = 0; - while (n <= maxCommands && (cmd = shell.readCommand()) != NULL) + while (n <= maxCommands) { - ++n; - delete cmd; + std::optional cmds = shell.readCommand(); + if (!cmds) + { + break; + } + n += cmds->size(); } ASSERT_LE(n, maxCommands); ASSERT_GE(n, minCommands); @@ -100,9 +104,7 @@ TEST_F(TestMainBlackInteractiveShell, def_use1) { InteractiveShell shell(d_solver.get(), d_symman.get(), *d_sin, *d_sout); *d_sin << "(declare-const x Real) (assert (> x 0))\n" << std::flush; - /* readCommand may return a sequence, so we can't say for sure - whether it will return 1 or 2... */ - countCommands(shell, 1, 2); + countCommands(shell, 2, 2); } TEST_F(TestMainBlackInteractiveShell, def_use2) @@ -110,10 +112,9 @@ TEST_F(TestMainBlackInteractiveShell, def_use2) InteractiveShell shell(d_solver.get(), d_symman.get(), *d_sin, *d_sout); /* readCommand may return a sequence, see above. */ *d_sin << "(declare-const x Real)\n" << std::flush; - Command* tmp = shell.readCommand(); + shell.readCommand(); *d_sin << "(assert (> x 0))\n" << std::flush; countCommands(shell, 1, 1); - delete tmp; } TEST_F(TestMainBlackInteractiveShell, empty_line) -- 2.30.2