summaryrefslogtreecommitdiff
path: root/src/main
diff options
context:
space:
mode:
Diffstat (limited to 'src/main')
-rw-r--r--src/main/command_executor.cpp43
-rw-r--r--src/main/driver_unified.cpp72
-rw-r--r--src/main/interactive_shell.cpp17
-rw-r--r--src/main/main.cpp16
-rw-r--r--src/main/time_limit.cpp4
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();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback