* directory for licensing information.
* ****************************************************************************
*
- * Driver for cvc5 executable (cvc4).
+ * Driver for cvc5 executable (cvc5).
*/
#include <stdio.h>
#include "api/cpp/cvc5.h"
#include "base/configuration.h"
+#include "base/cvc5config.h"
#include "base/output.h"
-#include "cvc4autoconfig.h"
#include "main/command_executor.h"
#include "main/interactive_shell.h"
#include "main/main.h"
+#include "main/options.h"
#include "main/signal_handlers.h"
#include "main/time_limit.h"
+#include "options/base_options.h"
+#include "options/main_options.h"
+#include "options/option_exception.h"
#include "options/options.h"
+#include "options/options_public.h"
+#include "options/parser_options.h"
#include "options/set_language.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
namespace cvc5 {
namespace main {
-/** Global options variable */
-thread_local Options* pOptions;
/** Full argv[0] */
const char* progPath;
/** Just the basename component of argv[0] */
-const std::string* progName;
+std::string progName;
/** A pointer to the CommandExecutor (the signal handlers need it) */
std::unique_ptr<cvc5::main::CommandExecutor> pExecutor;
} // namespace main
} // namespace cvc5
-void printUsage(Options& opts, bool full) {
- stringstream ss;
- ss << "usage: " << opts.getBinaryName() << " [options] [input-file]" << endl
- << endl
- << "Without an input file, or with `-', cvc5 reads from standard input."
- << endl
- << endl
- << "cvc5 options:" << endl;
- if(full) {
- Options::printUsage( ss.str(), *(opts.getOut()) );
- } else {
- Options::printShortUsage( ss.str(), *(opts.getOut()) );
- }
-}
+ void printUsage(const api::DriverOptions& dopts, bool full)
+ {
+ std::stringstream ss;
+ ss << "usage: " << progName << " [options] [input-file]" << std::endl
+ << std::endl
+ << "Without an input file, or with `-', cvc5 reads from standard "
+ "input."
+ << std::endl
+ << std::endl
+ << "cvc5 options:" << std::endl;
+ if (full)
+ {
+ main::printUsage(ss.str(), dopts.out());
+ }
+ else
+ {
+ main::printShortUsage(ss.str(), dopts.out());
+ }
+ }
-int runCvc4(int argc, char* argv[], Options& opts) {
+int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
+{
main::totalTime = std::make_unique<TotalTimer>();
- // For the signal handlers' benefit
- pOptions = &opts;
// Initialize the signal handlers
signal_handlers::install();
progPath = argv[0];
- // Parse the options
- vector<string> filenames = Options::parseOptions(&opts, argc, argv);
+ // Create the command executor to execute the parsed commands
+ pExecutor = std::make_unique<CommandExecutor>(solver);
+ api::DriverOptions dopts = solver->getDriverOptions();
+ Options* opts = &pExecutor->getOptions();
- auto limit = install_time_limit(opts);
+ // Parse the options
+ std::vector<string> filenames = main::parse(*solver, argc, argv, progName);
- string progNameStr = opts.getBinaryName();
- progName = &progNameStr;
+ auto limit = install_time_limit(*opts);
- if( opts.getHelp() ) {
- printUsage(opts, true);
+ if (opts->driver.help)
+ {
+ printUsage(dopts, true);
exit(1);
- } else if( opts.getLanguageHelp() ) {
- Options::printLanguageHelp(*(opts.getOut()));
+ }
+ else if (opts->base.languageHelp)
+ {
+ main::printLanguageHelp(dopts.out());
exit(1);
- } else if( opts.getVersion() ) {
- *(opts.getOut()) << Configuration::about().c_str() << flush;
+ }
+ else if (opts->driver.version)
+ {
+ dopts.out() << Configuration::about().c_str() << flush;
exit(0);
}
- segvSpin = opts.getSegvSpin();
+ segvSpin = opts->driver.segvSpin;
// If in competition mode, set output stream option to flush immediately
#ifdef CVC5_COMPETITION_MODE
- *(opts.getOut()) << unitbuf;
+ dopts.out() << unitbuf;
#endif /* CVC5_COMPETITION_MODE */
// We only accept one input file
const bool inputFromStdin = filenames.empty() || filenames[0] == "-";
// if we're reading from stdin on a TTY, default to interactive mode
- if(!opts.wasSetByUserInteractive()) {
- opts.setInteractive(inputFromStdin && isatty(fileno(stdin)));
+ if (!opts->driver.interactiveWasSetByUser)
+ {
+ opts->driver.interactive = inputFromStdin && isatty(fileno(stdin));
}
// Auto-detect input language by filename extension
std::string filenameStr("<stdin>");
if (!inputFromStdin) {
- // Use swap to avoid copying the string
- // TODO: use std::move() when switching to c++11
- filenameStr.swap(filenames[0]);
+ filenameStr = std::move(filenames[0]);
}
const char* filename = filenameStr.c_str();
- if(opts.getInputLanguage() == language::input::LANG_AUTO) {
+ if (solver->getOption("input-language") == "LANG_AUTO")
+ {
if( inputFromStdin ) {
// We can't do any fancy detection on stdin
- opts.setInputLanguage(language::input::LANG_CVC);
+ solver->setOption("input-language", "cvc");
} else {
- unsigned len = filenameStr.size();
+ size_t len = filenameStr.size();
if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
- opts.setInputLanguage(language::input::LANG_SMTLIB_V2_6);
+ solver->setOption("input-language", "smt2");
} else if((len >= 2 && !strcmp(".p", filename + len - 2))
|| (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
- opts.setInputLanguage(language::input::LANG_TPTP);
+ solver->setOption("input-language", "tptp");
} else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
|| ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
- opts.setInputLanguage(language::input::LANG_CVC);
+ solver->setOption("input-language", "cvc");
} else if((len >= 3 && !strcmp(".sy", filename + len - 3))
|| (len >= 3 && !strcmp(".sl", filename + len - 3))) {
// version 2 sygus is the default
- opts.setInputLanguage(language::input::LANG_SYGUS_V2);
+ solver->setOption("input-language", "sygus2");
}
}
}
- if(opts.getOutputLanguage() == language::output::LANG_AUTO) {
- opts.setOutputLanguage(language::toOutputLanguage(opts.getInputLanguage()));
+ if (solver->getOption("output-language") == "LANG_AUTO")
+ {
+ solver->setOption("output-language", solver->getOption("input-language"));
}
+ pExecutor->storeOptionsAsOriginal();
// Determine which messages to show based on smtcomp_mode and verbosity
if(Configuration::isMuzzledBuild()) {
WarningChannel.setStream(&cvc5::null_os);
}
- // important even for muzzled builds (to get result output right)
- (*(opts.getOut())) << language::SetLanguage(opts.getOutputLanguage());
-
- // Create the command executor to execute the parsed commands
- pExecutor = std::make_unique<CommandExecutor>(opts);
-
int returnValue = 0;
{
// notify SmtEngine that we are starting to parse
// Parse and execute commands until we are done
std::unique_ptr<Command> cmd;
bool status = true;
- if(opts.getInteractive() && inputFromStdin) {
- if(opts.getTearDownIncremental() > 0) {
- throw Exception(
- "--tear-down-incremental doesn't work in interactive mode");
- }
- if(!opts.wasSetByUserIncrementalSolving()) {
+ if (opts->driver.interactive && inputFromStdin)
+ {
+ if (!opts->base.incrementalSolvingWasSetByUser)
+ {
cmd.reset(new SetOptionCommand("incremental", "true"));
cmd->setMuted(true);
pExecutor->doCommand(cmd);
}
InteractiveShell shell(pExecutor->getSolver(),
pExecutor->getSymbolManager());
- if(opts.getInteractivePrompt()) {
- CVC5Message() << Configuration::getPackageName() << " "
- << Configuration::getVersionString();
- if(Configuration::isGitBuild()) {
- CVC5Message() << " [" << Configuration::getGitId() << "]";
- }
- CVC5Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
- << " assertions:"
- << (Configuration::isAssertionBuild() ? "on" : "off")
- << endl
- << endl;
- CVC5Message() << Configuration::copyright() << endl;
+
+ CVC5Message() << Configuration::getPackageName() << " "
+ << Configuration::getVersionString();
+ if (Configuration::isGitBuild())
+ {
+ CVC5Message() << " [" << Configuration::getGitId() << "]";
}
+ CVC5Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
+ << " assertions:"
+ << (Configuration::isAssertionBuild() ? "on" : "off")
+ << endl
+ << endl;
+ CVC5Message() << Configuration::copyright() << endl;
while(true) {
try {
cmd.reset(shell.readCommand());
} catch(UnsafeInterruptException& e) {
- (*opts.getOut()) << CommandInterrupted();
+ dopts.out() << CommandInterrupted();
break;
}
if (cmd == nullptr)
break;
status = pExecutor->doCommand(cmd) && status;
+ opts = &pExecutor->getOptions();
if (cmd->interrupted()) {
break;
}
}
- } else if( opts.getTearDownIncremental() > 0) {
- if(!opts.getIncrementalSolving() && opts.getTearDownIncremental() > 1) {
- // For tear-down-incremental values greater than 1, need incremental
- // on too.
- cmd.reset(new SetOptionCommand("incremental", "true"));
- cmd->setMuted(true);
- pExecutor->doCommand(cmd);
- // if(opts.wasSetByUserIncrementalSolving()) {
- // throw OptionException(
- // "--tear-down-incremental incompatible with --incremental");
- // }
-
- // cmd.reset(new SetOptionCommand("incremental", "false"));
- // cmd->setMuted(true);
- // pExecutor->doCommand(cmd);
- }
-
- ParserBuilder parserBuilder(pExecutor->getSolver(),
- pExecutor->getSymbolManager(),
- filename,
- opts);
-
- if( inputFromStdin ) {
-#if defined(CVC5_COMPETITION_MODE) && !defined(CVC5_SMTCOMP_APPLICATION_TRACK)
- parserBuilder.withStreamInput(cin);
-#else /* CVC5_COMPETITION_MODE && !CVC5_SMTCOMP_APPLICATION_TRACK */
- parserBuilder.withLineBufferedStreamInput(cin);
-#endif /* CVC5_COMPETITION_MODE && !CVC5_SMTCOMP_APPLICATION_TRACK */
- }
-
- vector< vector<Command*> > allCommands;
- allCommands.push_back(vector<Command*>());
- std::unique_ptr<Parser> parser(parserBuilder.build());
- int needReset = 0;
- // true if one of the commands was interrupted
- bool interrupted = false;
- while (status)
+ }
+ else
+ {
+ if (!opts->base.incrementalSolvingWasSetByUser)
{
- if (interrupted) {
- (*opts.getOut()) << CommandInterrupted();
- break;
- }
-
- try {
- cmd.reset(parser->nextCommand());
- if (cmd == nullptr) break;
- } catch (UnsafeInterruptException& e) {
- interrupted = true;
- continue;
- }
-
- if(dynamic_cast<PushCommand*>(cmd.get()) != nullptr) {
- if(needReset >= opts.getTearDownIncremental()) {
- pExecutor->reset();
- for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
- if (interrupted) break;
- for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
- {
- Command* ccmd = allCommands[i][j]->clone();
- ccmd->setMuted(true);
- pExecutor->doCommand(ccmd);
- if (ccmd->interrupted())
- {
- interrupted = true;
- }
- delete ccmd;
- }
- }
- needReset = 0;
- }
- allCommands.push_back(vector<Command*>());
- Command* copy = cmd->clone();
- allCommands.back().push_back(copy);
- status = pExecutor->doCommand(cmd);
- if(cmd->interrupted()) {
- interrupted = true;
- continue;
- }
- } else if(dynamic_cast<PopCommand*>(cmd.get()) != nullptr) {
- allCommands.pop_back(); // fixme leaks cmds here
- if (needReset >= opts.getTearDownIncremental()) {
- pExecutor->reset();
- for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
- for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
- {
- std::unique_ptr<Command> ccmd(allCommands[i][j]->clone());
- ccmd->setMuted(true);
- pExecutor->doCommand(ccmd);
- if (ccmd->interrupted())
- {
- interrupted = true;
- }
- }
- }
- if (interrupted) continue;
- (*opts.getOut()) << CommandSuccess();
- needReset = 0;
- } else {
- status = pExecutor->doCommand(cmd);
- if(cmd->interrupted()) {
- interrupted = true;
- continue;
- }
- }
- } else if(dynamic_cast<CheckSatCommand*>(cmd.get()) != nullptr ||
- dynamic_cast<QueryCommand*>(cmd.get()) != nullptr) {
- if(needReset >= opts.getTearDownIncremental()) {
- pExecutor->reset();
- for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
- for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
- {
- Command* ccmd = allCommands[i][j]->clone();
- ccmd->setMuted(true);
- pExecutor->doCommand(ccmd);
- if (ccmd->interrupted())
- {
- interrupted = true;
- }
- delete ccmd;
- }
- }
- needReset = 0;
- } else {
- ++needReset;
- }
- if (interrupted) {
- continue;
- }
-
- status = pExecutor->doCommand(cmd);
- if(cmd->interrupted()) {
- interrupted = true;
- continue;
- }
- } else if(dynamic_cast<ResetCommand*>(cmd.get()) != nullptr) {
- pExecutor->doCommand(cmd);
- allCommands.clear();
- allCommands.push_back(vector<Command*>());
- } else {
- // We shouldn't copy certain commands, because they can cause
- // an error on replay since there's no associated sat/unsat check
- // preceding them.
- if(dynamic_cast<GetUnsatCoreCommand*>(cmd.get()) == nullptr &&
- dynamic_cast<GetProofCommand*>(cmd.get()) == nullptr &&
- dynamic_cast<GetValueCommand*>(cmd.get()) == nullptr &&
- dynamic_cast<GetModelCommand*>(cmd.get()) == nullptr &&
- dynamic_cast<GetAssignmentCommand*>(cmd.get()) == nullptr &&
- dynamic_cast<GetInstantiationsCommand*>(cmd.get()) == nullptr &&
- dynamic_cast<GetAssertionsCommand*>(cmd.get()) == nullptr &&
- dynamic_cast<GetInfoCommand*>(cmd.get()) == nullptr &&
- dynamic_cast<GetOptionCommand*>(cmd.get()) == nullptr &&
- dynamic_cast<EchoCommand*>(cmd.get()) == nullptr) {
- Command* copy = cmd->clone();
- allCommands.back().push_back(copy);
- }
- status = pExecutor->doCommand(cmd);
- if(cmd->interrupted()) {
- interrupted = true;
- continue;
- }
-
- if(dynamic_cast<QuitCommand*>(cmd.get()) != nullptr) {
- break;
- }
- }
- }
- } else {
- if(!opts.wasSetByUserIncrementalSolving()) {
cmd.reset(new SetOptionCommand("incremental", "false"));
cmd->setMuted(true);
pExecutor->doCommand(cmd);
}
- ParserBuilder parserBuilder(pExecutor->getSolver(),
- pExecutor->getSymbolManager(),
- filename,
- opts);
-
+ ParserBuilder parserBuilder(
+ pExecutor->getSolver(), pExecutor->getSymbolManager(), true);
+ std::unique_ptr<Parser> parser(parserBuilder.build());
if( inputFromStdin ) {
-#if defined(CVC5_COMPETITION_MODE) && !defined(CVC5_SMTCOMP_APPLICATION_TRACK)
- parserBuilder.withStreamInput(cin);
-#else /* CVC5_COMPETITION_MODE && !CVC5_SMTCOMP_APPLICATION_TRACK */
- parserBuilder.withLineBufferedStreamInput(cin);
-#endif /* CVC5_COMPETITION_MODE && !CVC5_SMTCOMP_APPLICATION_TRACK */
+ parser->setInput(Input::newStreamInput(
+ solver->getOption("input-language"), cin, filename));
+ }
+ else
+ {
+ parser->setInput(
+ Input::newFileInput(solver->getOption("input-language"),
+ filename,
+ solver->getOption("mmap") == "true"));
}
- std::unique_ptr<Parser> parser(parserBuilder.build());
bool interrupted = false;
while (status)
{
if (interrupted) {
- (*opts.getOut()) << CommandInterrupted();
+ dopts.out() << CommandInterrupted();
pExecutor->reset();
+ opts = &pExecutor->getOptions();
break;
}
try {
}
status = pExecutor->doCommand(cmd);
+ opts = &pExecutor->getOptions();
if (cmd->interrupted() && status == 0) {
interrupted = true;
break;
}
#ifdef CVC5_COMPETITION_MODE
- opts.flushOut();
+ dopts.out() << std::flush;
// exit, don't return (don't want destructors to run)
// _exit() from unistd.h doesn't run global destructors
// or other on_exit/atexit stuff.
pExecutor->flushOutputStreams();
#ifdef CVC5_DEBUG
- if(opts.getEarlyExit() && opts.wasSetByUserEarlyExit()) {
+ if (opts->driver.earlyExit && opts->driver.earlyExitWasSetByUser)
+ {
_exit(returnValue);
}
#else /* CVC5_DEBUG */
- if(opts.getEarlyExit()) {
+ if (opts->driver.earlyExit)
+ {
_exit(returnValue);
}
#endif /* CVC5_DEBUG */
projects / cvc5.git / blobdiff