diff options
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/command_executor.cpp | 43 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 72 | ||||
-rw-r--r-- | src/main/interactive_shell.cpp | 17 | ||||
-rw-r--r-- | src/main/main.cpp | 16 | ||||
-rw-r--r-- | src/main/time_limit.cpp | 4 |
5 files changed, 77 insertions, 75 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 6bdc1abc9..b6ead1b70 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -26,7 +26,8 @@ #include <vector> #include "main/main.h" -#include "options/options_public.h" +#include "options/base_options.h" +#include "options/main_options.h" #include "smt/command.h" #include "smt/smt_engine.h" @@ -65,7 +66,7 @@ CommandExecutor::~CommandExecutor() void CommandExecutor::printStatistics(std::ostream& out) const { - if (options::getStatistics(d_options)) + if (d_options.base.statistics) { getSmtEngine()->printStatistics(out); } @@ -73,7 +74,7 @@ void CommandExecutor::printStatistics(std::ostream& out) const void CommandExecutor::printStatisticsSafe(int fd) const { - if (options::getStatistics(d_options)) + if (d_options.base.statistics) { getSmtEngine()->printStatisticsSafe(fd); } @@ -81,7 +82,7 @@ void CommandExecutor::printStatisticsSafe(int fd) const bool CommandExecutor::doCommand(Command* cmd) { - if (options::getParseOnly(d_options)) + if (d_options.base.parseOnly) { return true; } @@ -100,9 +101,9 @@ bool CommandExecutor::doCommand(Command* cmd) return status; } else { - if (options::getVerbosity(d_options) > 2) + if (d_options.base.verbosity > 2) { - *options::getOut(d_options) << "Invoking: " << *cmd << std::endl; + *d_options.base.out << "Invoking: " << *cmd << std::endl; } return doCommandSingleton(cmd); @@ -111,7 +112,7 @@ bool CommandExecutor::doCommand(Command* cmd) void CommandExecutor::reset() { - printStatistics(*options::getErr(d_options)); + printStatistics(*d_options.base.err); /* We have to keep options passed via CL on reset. These options are stored * in CommandExecutor::d_options (populated and created in the driver), and * CommandExecutor::d_options only contains *these* options since the @@ -124,10 +125,10 @@ void CommandExecutor::reset() bool CommandExecutor::doCommandSingleton(Command* cmd) { bool status = true; - if (options::getVerbosity(d_options) >= -1) + if (d_options.base.verbosity >= -1) { status = solverInvoke( - d_solver.get(), d_symman.get(), cmd, options::getOut(d_options)); + d_solver.get(), d_symman.get(), cmd, d_options.base.out); } else { @@ -150,9 +151,9 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) d_result = res = q->getResult(); } - if ((cs != nullptr || q != nullptr) && options::getStatsEveryQuery(d_options)) + if ((cs != nullptr || q != nullptr) && d_options.base.statisticsEveryQuery) { - getSmtEngine()->printStatisticsDiff(*options::getErr(d_options)); + getSmtEngine()->printStatisticsDiff(*d_options.base.err); } bool isResultUnsat = res.isUnsat() || res.isEntailed(); @@ -160,32 +161,32 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) // dump the model/proof/unsat core if option is set if (status) { std::vector<std::unique_ptr<Command> > getterCommands; - if (options::getDumpModels(d_options) + if (d_options.driver.dumpModels && (res.isSat() || (res.isSatUnknown() && res.getUnknownExplanation() == api::Result::INCOMPLETE))) { getterCommands.emplace_back(new GetModelCommand()); } - if (options::getDumpProofs(d_options) && isResultUnsat) + if (d_options.driver.dumpProofs && isResultUnsat) { getterCommands.emplace_back(new GetProofCommand()); } - if (options::getDumpInstantiations(d_options) + if (d_options.driver.dumpInstantiations && GetInstantiationsCommand::isEnabled(d_solver.get(), res)) { getterCommands.emplace_back(new GetInstantiationsCommand()); } - if (options::getDumpUnsatCores(d_options) && isResultUnsat) + if ((d_options.driver.dumpUnsatCores || d_options.driver.dumpUnsatCoresFull) && isResultUnsat) { getterCommands.emplace_back(new GetUnsatCoreCommand()); } if (!getterCommands.empty()) { // set no time limit during dumping if applicable - if (options::getForceNoLimitCpuWhileDump(d_options)) + if (d_options.driver.forceNoLimitCpuWhileDump) { setNoLimitCPU(); } @@ -225,17 +226,17 @@ bool solverInvoke(api::Solver* solver, } void CommandExecutor::flushOutputStreams() { - printStatistics(*(options::getErr(d_options))); + printStatistics(*d_options.base.err); // make sure out and err streams are flushed too - if (options::getOut(d_options) != nullptr) + if (d_options.base.out != nullptr) { - *options::getOut(d_options) << std::flush; + *d_options.base.out << std::flush; } - if (options::getErr(d_options) != nullptr) + if (d_options.base.err != nullptr) { - *options::getErr(d_options) << std::flush; + *d_options.base.err << std::flush; } } diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 697501d13..ed1825711 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -33,8 +33,9 @@ #include "main/main.h" #include "main/signal_handlers.h" #include "main/time_limit.h" +#include "options/base_options.h" #include "options/options.h" -#include "options/options_public.h" +#include "options/parser_options.h" #include "options/main_options.h" #include "options/set_language.h" #include "parser/parser.h" @@ -88,9 +89,9 @@ void printUsage(Options& opts, bool full) { << endl << "cvc5 options:" << endl; if(full) { - Options::printUsage(ss.str(), *(options::getOut(opts))); + Options::printUsage(ss.str(), *opts.base.out); } else { - Options::printShortUsage(ss.str(), *(options::getOut(opts))); + Options::printShortUsage(ss.str(), *opts.base.out); } } @@ -116,14 +117,14 @@ int runCvc5(int argc, char* argv[], Options& opts) printUsage(opts, true); exit(1); } - else if (options::getLanguageHelp(opts)) + else if (opts.base.languageHelp) { - Options::printLanguageHelp(*(options::getOut(opts))); + Options::printLanguageHelp(*opts.base.out); exit(1); } else if (opts.driver.version) { - *(options::getOut(opts)) << Configuration::about().c_str() << flush; + *opts.base.out << Configuration::about().c_str() << flush; exit(0); } @@ -131,7 +132,7 @@ int runCvc5(int argc, char* argv[], Options& opts) // If in competition mode, set output stream option to flush immediately #ifdef CVC5_COMPETITION_MODE - *(options::getOut(opts)) << unitbuf; + *opts.base.out << unitbuf; #endif /* CVC5_COMPETITION_MODE */ // We only accept one input file @@ -143,7 +144,7 @@ int runCvc5(int argc, char* argv[], Options& opts) const bool inputFromStdin = filenames.empty() || filenames[0] == "-"; // if we're reading from stdin on a TTY, default to interactive mode - if (!options::wasSetByUserInteractive(opts)) + if (!opts.driver.interactiveWasSetByUser) { opts.driver.interactive = inputFromStdin && isatty(fileno(stdin)); } @@ -157,33 +158,32 @@ int runCvc5(int argc, char* argv[], Options& opts) } const char* filename = filenameStr.c_str(); - if (options::getInputLanguage(opts) == language::input::LANG_AUTO) + if (opts.base.inputLanguage == language::input::LANG_AUTO) { if( inputFromStdin ) { // We can't do any fancy detection on stdin - options::setInputLanguage(language::input::LANG_CVC, opts); + opts.base.inputLanguage = language::input::LANG_CVC; } else { size_t len = filenameStr.size(); if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { - options::setInputLanguage(language::input::LANG_SMTLIB_V2_6, opts); + opts.base.inputLanguage = language::input::LANG_SMTLIB_V2_6; } else if((len >= 2 && !strcmp(".p", filename + len - 2)) || (len >= 5 && !strcmp(".tptp", filename + len - 5))) { - options::setInputLanguage(language::input::LANG_TPTP, opts); + opts.base.inputLanguage = language::input::LANG_TPTP; } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { - options::setInputLanguage(language::input::LANG_CVC, opts); + opts.base.inputLanguage = language::input::LANG_CVC; } else if((len >= 3 && !strcmp(".sy", filename + len - 3)) || (len >= 3 && !strcmp(".sl", filename + len - 3))) { // version 2 sygus is the default - options::setInputLanguage(language::input::LANG_SYGUS_V2, opts); + opts.base.inputLanguage = language::input::LANG_SYGUS_V2; } } } - if (options::getOutputLanguage(opts) == language::output::LANG_AUTO) + if (opts.base.outputLanguage == language::output::LANG_AUTO) { - options::setOutputLanguage( - language::toOutputLanguage(options::getInputLanguage(opts)), opts); + opts.base.outputLanguage = language::toOutputLanguage(opts.base.inputLanguage); } // Determine which messages to show based on smtcomp_mode and verbosity @@ -197,8 +197,8 @@ int runCvc5(int argc, char* argv[], Options& opts) } // important even for muzzled builds (to get result output right) - (*(options::getOut(opts))) - << language::SetLanguage(options::getOutputLanguage(opts)); + (*opts.base.out) + << language::SetLanguage(opts.base.outputLanguage); // Create the command executor to execute the parsed commands pExecutor = std::make_unique<CommandExecutor>(opts); @@ -218,7 +218,7 @@ int runCvc5(int argc, char* argv[], Options& opts) throw Exception( "--tear-down-incremental doesn't work in interactive mode"); } - if (!options::wasSetByUserIncrementalSolving(opts)) + if (!opts.base.incrementalSolvingWasSetByUser) { cmd.reset(new SetOptionCommand("incremental", "true")); cmd->setMuted(true); @@ -245,7 +245,7 @@ int runCvc5(int argc, char* argv[], Options& opts) try { cmd.reset(shell.readCommand()); } catch(UnsafeInterruptException& e) { - (*options::getOut(opts)) << CommandInterrupted(); + *opts.base.out << CommandInterrupted(); break; } if (cmd == nullptr) @@ -258,7 +258,7 @@ int runCvc5(int argc, char* argv[], Options& opts) } else if (opts.driver.tearDownIncremental > 0) { - if (!options::getIncrementalSolving(opts) + if (!opts.base.incrementalSolving && opts.driver.tearDownIncremental > 1) { // For tear-down-incremental values greater than 1, need incremental @@ -266,7 +266,7 @@ int runCvc5(int argc, char* argv[], Options& opts) cmd.reset(new SetOptionCommand("incremental", "true")); cmd->setMuted(true); pExecutor->doCommand(cmd); - // if(options::wasSetByUserIncrementalSolving(opts)) { + // if(opts.base.incrementalWasSetByUser) { // throw OptionException( // "--tear-down-incremental incompatible with --incremental"); // } @@ -282,13 +282,13 @@ int runCvc5(int argc, char* argv[], Options& opts) std::unique_ptr<Parser> parser(parserBuilder.build()); if( inputFromStdin ) { parser->setInput(Input::newStreamInput( - options::getInputLanguage(opts), cin, filename)); + opts.base.inputLanguage, cin, filename)); } else { - parser->setInput(Input::newFileInput(options::getInputLanguage(opts), + parser->setInput(Input::newFileInput(opts.base.inputLanguage, filename, - options::getMemoryMap(opts))); + opts.parser.memoryMap)); } vector< vector<Command*> > allCommands; @@ -299,7 +299,7 @@ int runCvc5(int argc, char* argv[], Options& opts) while (status) { if (interrupted) { - (*options::getOut(opts)) << CommandInterrupted(); + *opts.base.out << CommandInterrupted(); break; } @@ -357,7 +357,7 @@ int runCvc5(int argc, char* argv[], Options& opts) } } if (interrupted) continue; - (*options::getOut(opts)) << CommandSuccess(); + *opts.base.out << CommandSuccess(); needReset = 0; } else @@ -436,7 +436,7 @@ int runCvc5(int argc, char* argv[], Options& opts) } else { - if (!options::wasSetByUserIncrementalSolving(opts)) + if (!opts.base.incrementalSolvingWasSetByUser) { cmd.reset(new SetOptionCommand("incremental", "false")); cmd->setMuted(true); @@ -449,20 +449,20 @@ int runCvc5(int argc, char* argv[], Options& opts) std::unique_ptr<Parser> parser(parserBuilder.build()); if( inputFromStdin ) { parser->setInput(Input::newStreamInput( - options::getInputLanguage(opts), cin, filename)); + opts.base.inputLanguage, cin, filename)); } else { - parser->setInput(Input::newFileInput(options::getInputLanguage(opts), + parser->setInput(Input::newFileInput(opts.base.inputLanguage, filename, - options::getMemoryMap(opts))); + opts.parser.memoryMap)); } bool interrupted = false; while (status) { if (interrupted) { - (*options::getOut(opts)) << CommandInterrupted(); + *opts.base.out << CommandInterrupted(); pExecutor->reset(); break; } @@ -496,9 +496,9 @@ int runCvc5(int argc, char* argv[], Options& opts) } #ifdef CVC5_COMPETITION_MODE - if (cvc5::options::getOut(opts) != nullptr) + if (opts.base.out != nullptr) { - *cvc5::options::getOut(opts) << std::flush; + *opts.base.out << std::flush; } // exit, don't return (don't want destructors to run) // _exit() from unistd.h doesn't run global destructors @@ -510,7 +510,7 @@ int runCvc5(int argc, char* argv[], Options& opts) pExecutor->flushOutputStreams(); #ifdef CVC5_DEBUG - if (opts.driver.earlyExit && options::wasSetByUserEarlyExit(opts)) + if (opts.driver.earlyExit && opts.driver.earlyExitWasSetByUser) { _exit(returnValue); } diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 048c101f0..964b88ea0 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -40,10 +40,11 @@ #include "base/check.h" #include "base/output.h" #include "expr/symbol_manager.h" +#include "options/base_options.h" #include "options/language.h" #include "options/main_options.h" #include "options/options.h" -#include "options/options_public.h" +#include "options/parser_options.h" #include "parser/input.h" #include "parser/parser.h" #include "parser/parser_builder.h" @@ -89,16 +90,16 @@ static set<string> s_declarations; InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm) : d_options(solver->getOptions()), - d_in(*options::getIn(d_options)), - d_out(*options::getOut(d_options)), + d_in(*d_options.base.in), + d_out(*d_options.base.out), d_quit(false) { ParserBuilder parserBuilder(solver, sm, d_options); /* Create parser with bogus input. */ d_parser = parserBuilder.build(); - if (options::wasSetByUserForceLogicString(d_options)) + if (d_options.parser.forceLogicStringWasSetByUser) { - LogicInfo tmp(options::getForceLogicString(d_options)); + LogicInfo tmp(d_options.parser.forceLogicString); d_parser->forceLogic(tmp.getLogicString()); } @@ -113,7 +114,7 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm) ::using_history(); OutputLanguage lang = - toOutputLanguage(options::getInputLanguage(d_options)); + toOutputLanguage(d_options.base.inputLanguage); switch(lang) { case output::LANG_CVC: d_historyFilename = string(getenv("HOME")) + "/.cvc5_history"; @@ -314,7 +315,7 @@ restart: } d_parser->setInput(Input::newStringInput( - options::getInputLanguage(d_options), input, INPUT_FILENAME)); + d_options.base.inputLanguage, input, INPUT_FILENAME)); /* There may be more than one command in the input. Build up a sequence. */ @@ -365,7 +366,7 @@ restart: } catch (ParserException& pe) { - if (language::isOutputLang_smt2(options::getOutputLanguage(d_options))) + if (language::isOutputLang_smt2(d_options.base.outputLanguage)) { d_out << "(error \"" << pe << "\")" << endl; } diff --git a/src/main/main.cpp b/src/main/main.cpp index 2b25e6c93..a00e29b04 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -26,10 +26,10 @@ #include "base/output.h" #include "main/command_executor.h" #include "main/interactive_shell.h" +#include "options/base_options.h" #include "options/language.h" #include "options/option_exception.h" #include "options/options.h" -#include "options/options_public.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "parser/parser_exception.h" @@ -53,25 +53,25 @@ int main(int argc, char* argv[]) { return runCvc5(argc, argv, opts); } catch(OptionException& e) { #ifdef CVC5_COMPETITION_MODE - *options::getOut(opts) << "unknown" << endl; + *opts.base.out << "unknown" << endl; #endif cerr << "(error \"" << e << "\")" << endl << endl << "Please use --help to get help on command-line options." << endl; } catch(Exception& e) { #ifdef CVC5_COMPETITION_MODE - *options::getOut(opts) << "unknown" << endl; + *opts.base.out << "unknown" << endl; #endif - if (language::isOutputLang_smt2(options::getOutputLanguage(opts))) + if (language::isOutputLang_smt2(opts.base.outputLanguage)) { - *options::getOut(opts) << "(error \"" << e << "\")" << endl; + *opts.base.out << "(error \"" << e << "\")" << endl; } else { - *options::getErr(opts) << "(error \"" << e << "\")" << endl; + *opts.base.err << "(error \"" << e << "\")" << endl; } - if (options::getStatistics(opts) && pExecutor != nullptr) + if (opts.base.statistics && pExecutor != nullptr) { totalTime.reset(); - pExecutor->printStatistics(*options::getErr(opts)); + pExecutor->printStatistics(*opts.base.err); } } exit(1); diff --git a/src/main/time_limit.cpp b/src/main/time_limit.cpp index c0fc6846a..28a0087bb 100644 --- a/src/main/time_limit.cpp +++ b/src/main/time_limit.cpp @@ -56,7 +56,7 @@ #include <cstring> #include "base/exception.h" -#include "options/options_public.h" +#include "options/base_options.h" #include "signal_handlers.h" namespace cvc5 { @@ -80,7 +80,7 @@ TimeLimit::~TimeLimit() TimeLimit install_time_limit(const Options& opts) { - unsigned long ms = options::getCumulativeTimeLimit(opts); + uint64_t ms = opts.base.cumulativeMillisecondLimit; // Skip if no time limit shall be set. if (ms == 0) { return TimeLimit(); |