bool CommandExecutor::doCommand(Command* cmd)
{
- CommandSequence *seq = dynamic_cast<CommandSequence*>(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()
#include <iostream>
#include <memory>
#include <new>
+#include <optional>
#include "api/cpp/cvc5.h"
#include "base/configuration.h"
solver->setInfo("filename", filenameStr);
// Parse and execute commands until we are done
- std::unique_ptr<cvc5::Command> cmd;
bool status = true;
if (solver->getOptionInfo("interactive").boolValue() && inputFromStdin)
{
<< 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<InteractiveShell::CmdSeq> cmds = shell.readCommand();
+ if (!cmds)
+ {
break;
}
+ for (std::unique_ptr<cvc5::Command>& cmd : *cmds)
+ {
+ status = pExecutor->doCommand(cmd) && status;
+ if (cmd->interrupted())
+ {
+ quit = true;
+ break;
+ }
+ }
}
}
else
*/
#include "main/interactive_shell.h"
-#include <cstring>
#include <unistd.h>
#include <algorithm>
#include <cstdlib>
+#include <cstring>
#include <iostream>
+#include <optional>
#include <set>
#include <string>
#include <utility>
#endif /* HAVE_LIBEDITLINE */
}
-Command* InteractiveShell::readCommand()
+std::optional<InteractiveShell::CmdSeq> InteractiveShell::readCommand()
{
char* lineBuf = NULL;
string line = "";
* 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. */
if(input.empty()) {
/* Nothing left to parse. */
d_out << endl;
- return NULL;
+ return {};
}
/* Some input left to parse, but nothing left to read.
/* There may be more than one command in the input. Build up a
sequence. */
- CommandSequence *cmd_seq = new CommandSequence();
+ std::vector<std::unique_ptr<cvc5::Command>> cmdSeq;
Command *cmd;
try
{
while ((cmd = d_parser->nextCommand()))
{
- cmd_seq->addCommand(cmd);
+ cmdSeq.emplace_back(cmd);
if (dynamic_cast<QuitCommand*>(cmd) != NULL)
{
d_quit = true;
// cmd_seq = new CommandSequence();
}
- return cmd_seq;
+ return std::optional<CmdSeq>(std::move(cmdSeq));
}/* InteractiveShell::readCommand() */
#if HAVE_LIBEDITLINE
#include <iosfwd>
#include <memory>
+#include <optional>
#include <string>
+#include <vector>
namespace cvc5 {
class InteractiveShell
{
public:
+ using CmdSeq = std::vector<std::unique_ptr<cvc5::Command>>;
+
InteractiveShell(Solver* solver,
SymbolManager* sm,
std::istream& in,
~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<CmdSeq> readCommand();
/**
* Return the internal parser being used.
std::vector<cvc5::Term> funcs;
std::vector<cvc5::Term> func_defs;
cvc5::Term aexpr;
- std::unique_ptr<cvc5::CommandSequence> seq;
std::vector<cvc5::Sort> sorts;
std::vector<cvc5::Term> flattenVars;
}
std::vector<cvc5::Term> terms;
std::vector<cvc5::Sort> sorts;
std::vector<std::pair<std::string, cvc5::Sort> > sortedVarNames;
- std::unique_ptr<cvc5::CommandSequence> seq;
cvc5::Grammar* g = nullptr;
}
/* Extended SMT-LIB set of commands syntax, not permitted in
}
| 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();
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;
}
;
out << "Quit()" << std::endl;
}
-void AstPrinter::toStreamCmdCommandSequence(
- std::ostream& out, const std::vector<cvc5::Command*>& 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
/** Print quit command */
void toStreamCmdQuit(std::ostream& out) const override;
- /** Print command sequence command */
- void toStreamCmdCommandSequence(
- std::ostream& out,
- const std::vector<cvc5::Command*>& sequence) const override;
-
private:
void toStream(std::ostream& out,
TNode n,
printUnknownCommand(out, "declare-heap");
}
-void Printer::toStreamCmdCommandSequence(
- std::ostream& out, const std::vector<cvc5::Command*>& sequence) const
-{
- printUnknownCommand(out, "sequence");
-}
-
} // namespace cvc5::internal
TypeNode locType,
TypeNode dataType) const;
- /** Print command sequence command */
- virtual void toStreamCmdCommandSequence(
- std::ostream& out, const std::vector<cvc5::Command*>& sequence) const;
-
protected:
/** Derived classes can construct, but no one else. */
Printer() {}
out << "(exit)" << std::endl;
}
-void Smt2Printer::toStreamCmdCommandSequence(
- std::ostream& out, const std::vector<cvc5::Command*>& sequence) const
-{
- for (cvc5::Command* i : sequence)
- {
- out << *i;
- }
-}
-
void Smt2Printer::toStreamCmdDeclareFunction(std::ostream& out,
const std::string& id,
TypeNode type) const
TypeNode locType,
TypeNode dataType) const override;
- /** Print command sequence command */
- void toStreamCmdCommandSequence(
- std::ostream& out,
- const std::vector<cvc5::Command*>& 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).
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 */
/* -------------------------------------------------------------------------- */
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<Command*> 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<Command*>::iterator iterator;
- typedef std::vector<Command*>::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 */
* Black box testing of cvc5::InteractiveShell.
*/
+#include <memory>
#include <sstream>
#include <vector>
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<InteractiveShell::CmdSeq> cmds = shell.readCommand();
+ if (!cmds)
+ {
+ break;
+ }
+ n += cmds->size();
}
ASSERT_LE(n, maxCommands);
ASSERT_GE(n, minCommands);
{
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)
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)
projects / cvc5.git / commitdiff