This PR moves options wrapper functions out of the Options class. These wrapper functions are meant to be called by "external" code that should not access the options modules. This PR thereby significantly reduces the interface of the Options class.
#include <vector>
#include "main/main.h"
+#include "options/options_public.h"
#include "smt/command.h"
#include "smt/smt_engine.h"
void CommandExecutor::printStatistics(std::ostream& out) const
{
- if (d_options.getStatistics())
+ if (options::getStatistics(d_options))
{
getSmtEngine()->printStatistics(out);
}
void CommandExecutor::printStatisticsSafe(int fd) const
{
- if (d_options.getStatistics())
+ if (options::getStatistics(d_options))
{
getSmtEngine()->printStatisticsSafe(fd);
}
bool CommandExecutor::doCommand(Command* cmd)
{
- if( d_options.getParseOnly() ) {
+ if (options::getParseOnly(d_options))
+ {
return true;
}
return status;
} else {
- if(d_options.getVerbosity() > 2) {
- *d_options.getOut() << "Invoking: " << *cmd << std::endl;
+ if (options::getVerbosity(d_options) > 2)
+ {
+ *options::getOut(d_options) << "Invoking: " << *cmd << std::endl;
}
return doCommandSingleton(cmd);
void CommandExecutor::reset()
{
- printStatistics(*d_options.getErr());
+ printStatistics(*options::getErr(d_options));
/* 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
bool CommandExecutor::doCommandSingleton(Command* cmd)
{
bool status = true;
- if(d_options.getVerbosity() >= -1) {
- status =
- solverInvoke(d_solver.get(), d_symman.get(), cmd, d_options.getOut());
- } else {
+ if (options::getVerbosity(d_options) >= -1)
+ {
+ status = solverInvoke(
+ d_solver.get(), d_symman.get(), cmd, options::getOut(d_options));
+ }
+ else
+ {
status = solverInvoke(d_solver.get(), d_symman.get(), cmd, nullptr);
}
d_result = res = q->getResult();
}
- if((cs != nullptr || q != nullptr) && d_options.getStatsEveryQuery()) {
- getSmtEngine()->printStatisticsDiff(*d_options.getErr());
+ if ((cs != nullptr || q != nullptr) && options::getStatsEveryQuery(d_options))
+ {
+ getSmtEngine()->printStatisticsDiff(*options::getErr(d_options));
}
bool isResultUnsat = res.isUnsat() || res.isEntailed();
// dump the model/proof/unsat core if option is set
if (status) {
std::vector<std::unique_ptr<Command> > getterCommands;
- if (d_options.getDumpModels()
+ if (options::getDumpModels(d_options)
&& (res.isSat()
|| (res.isSatUnknown()
&& res.getUnknownExplanation() == api::Result::INCOMPLETE)))
{
getterCommands.emplace_back(new GetModelCommand());
}
- if (d_options.getDumpProofs() && isResultUnsat)
+ if (options::getDumpProofs(d_options) && isResultUnsat)
{
getterCommands.emplace_back(new GetProofCommand());
}
- if (d_options.getDumpInstantiations()
- && ((d_options.getInstFormatMode() != options::InstFormatMode::SZS
+ if (options::getDumpInstantiations(d_options)
+ && ((options::getInstFormatMode(d_options)
+ != options::InstFormatMode::SZS
&& (res.isSat()
|| (res.isSatUnknown()
&& res.getUnknownExplanation()
getterCommands.emplace_back(new GetInstantiationsCommand());
}
- if (d_options.getDumpUnsatCores() && isResultUnsat)
+ if (options::getDumpUnsatCores(d_options) && isResultUnsat)
{
getterCommands.emplace_back(new GetUnsatCoreCommand());
}
if (!getterCommands.empty()) {
// set no time limit during dumping if applicable
- if (d_options.getForceNoLimitCpuWhileDump()) {
+ if (options::getForceNoLimitCpuWhileDump(d_options))
+ {
setNoLimitCPU();
}
for (const auto& getterCommand : getterCommands) {
}
void CommandExecutor::flushOutputStreams() {
- printStatistics(*(d_options.getErr()));
+ printStatistics(*(options::getErr(d_options)));
// make sure out and err streams are flushed too
- d_options.flushOut();
- d_options.flushErr();
+
+ if (options::getOut(d_options) != nullptr)
+ {
+ *options::getOut(d_options) << std::flush;
+ }
+ if (options::getErr(d_options) != nullptr)
+ {
+ *options::getErr(d_options) << std::flush;
+ }
}
} // namespace main
#include "main/signal_handlers.h"
#include "main/time_limit.h"
#include "options/options.h"
+#include "options/options_public.h"
#include "options/set_language.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
void printUsage(Options& opts, bool full) {
stringstream ss;
- ss << "usage: " << opts.getBinaryName() << " [options] [input-file]" << endl
+ ss << "usage: " << options::getBinaryName(opts) << " [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()) );
+ Options::printUsage(ss.str(), *(options::getOut(opts)));
} else {
- Options::printShortUsage( ss.str(), *(opts.getOut()) );
+ Options::printShortUsage(ss.str(), *(options::getOut(opts)));
}
}
auto limit = install_time_limit(opts);
- string progNameStr = opts.getBinaryName();
+ string progNameStr = options::getBinaryName(opts);
progName = &progNameStr;
- if( opts.getHelp() ) {
+ if (options::getHelp(opts))
+ {
printUsage(opts, true);
exit(1);
- } else if( opts.getLanguageHelp() ) {
- Options::printLanguageHelp(*(opts.getOut()));
+ }
+ else if (options::getLanguageHelp(opts))
+ {
+ Options::printLanguageHelp(*(options::getOut(opts)));
exit(1);
- } else if( opts.getVersion() ) {
- *(opts.getOut()) << Configuration::about().c_str() << flush;
+ }
+ else if (options::getVersion(opts))
+ {
+ *(options::getOut(opts)) << Configuration::about().c_str() << flush;
exit(0);
}
- segvSpin = opts.getSegvSpin();
+ segvSpin = options::getSegvSpin(opts);
// If in competition mode, set output stream option to flush immediately
#ifdef CVC5_COMPETITION_MODE
- *(opts.getOut()) << unitbuf;
+ *(options::getOut(opts)) << 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 (!options::wasSetByUserInteractive(opts))
+ {
+ options::setInteractive(inputFromStdin && isatty(fileno(stdin)), opts);
}
// Auto-detect input language by filename extension
}
const char* filename = filenameStr.c_str();
- if(opts.getInputLanguage() == language::input::LANG_AUTO) {
+ if (options::getInputLanguage(opts) == language::input::LANG_AUTO)
+ {
if( inputFromStdin ) {
// We can't do any fancy detection on stdin
- opts.setInputLanguage(language::input::LANG_CVC);
+ options::setInputLanguage(language::input::LANG_CVC, opts);
} 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);
+ options::setInputLanguage(language::input::LANG_SMTLIB_V2_6, opts);
} else if((len >= 2 && !strcmp(".p", filename + len - 2))
|| (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
- opts.setInputLanguage(language::input::LANG_TPTP);
+ options::setInputLanguage(language::input::LANG_TPTP, opts);
} else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
|| ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
- opts.setInputLanguage(language::input::LANG_CVC);
+ options::setInputLanguage(language::input::LANG_CVC, opts);
} 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);
+ options::setInputLanguage(language::input::LANG_SYGUS_V2, opts);
}
}
}
- if(opts.getOutputLanguage() == language::output::LANG_AUTO) {
- opts.setOutputLanguage(language::toOutputLanguage(opts.getInputLanguage()));
+ if (options::getOutputLanguage(opts) == language::output::LANG_AUTO)
+ {
+ options::setOutputLanguage(
+ language::toOutputLanguage(options::getInputLanguage(opts)), opts);
}
// Determine which messages to show based on smtcomp_mode and verbosity
}
// important even for muzzled builds (to get result output right)
- (*(opts.getOut())) << language::SetLanguage(opts.getOutputLanguage());
+ (*(options::getOut(opts)))
+ << language::SetLanguage(options::getOutputLanguage(opts));
// Create the command executor to execute the parsed commands
pExecutor = std::make_unique<CommandExecutor>(opts);
// Parse and execute commands until we are done
std::unique_ptr<Command> cmd;
bool status = true;
- if(opts.getInteractive() && inputFromStdin) {
- if(opts.getTearDownIncremental() > 0) {
+ if (options::getInteractive(opts) && inputFromStdin)
+ {
+ if (options::getTearDownIncremental(opts) > 0)
+ {
throw Exception(
"--tear-down-incremental doesn't work in interactive mode");
}
- if(!opts.wasSetByUserIncrementalSolving()) {
+ if (!options::wasSetByUserIncrementalSolving(opts))
+ {
cmd.reset(new SetOptionCommand("incremental", "true"));
cmd->setMuted(true);
pExecutor->doCommand(cmd);
}
InteractiveShell shell(pExecutor->getSolver(),
pExecutor->getSymbolManager());
- if(opts.getInteractivePrompt()) {
+ if (options::getInteractivePrompt(opts))
+ {
CVC5Message() << Configuration::getPackageName() << " "
<< Configuration::getVersionString();
if(Configuration::isGitBuild()) {
try {
cmd.reset(shell.readCommand());
} catch(UnsafeInterruptException& e) {
- (*opts.getOut()) << CommandInterrupted();
+ (*options::getOut(opts)) << CommandInterrupted();
break;
}
if (cmd == nullptr)
break;
}
}
- } else if( opts.getTearDownIncremental() > 0) {
- if(!opts.getIncrementalSolving() && opts.getTearDownIncremental() > 1) {
+ }
+ else if (options::getTearDownIncremental(opts) > 0)
+ {
+ if (!options::getIncrementalSolving(opts)
+ && options::getTearDownIncremental(opts) > 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()) {
+ // if(options::wasSetByUserIncrementalSolving(opts)) {
// throw OptionException(
// "--tear-down-incremental incompatible with --incremental");
// }
opts);
std::unique_ptr<Parser> parser(parserBuilder.build());
if( inputFromStdin ) {
- parser->setInput(
- Input::newStreamInput(opts.getInputLanguage(), cin, filename));
+ parser->setInput(Input::newStreamInput(
+ options::getInputLanguage(opts), cin, filename));
}
else
{
- parser->setInput(Input::newFileInput(
- opts.getInputLanguage(), filename, opts.getMemoryMap()));
+ parser->setInput(Input::newFileInput(options::getInputLanguage(opts),
+ filename,
+ options::getMemoryMap(opts)));
}
vector< vector<Command*> > allCommands;
while (status)
{
if (interrupted) {
- (*opts.getOut()) << CommandInterrupted();
+ (*options::getOut(opts)) << CommandInterrupted();
break;
}
}
if(dynamic_cast<PushCommand*>(cmd.get()) != nullptr) {
- if(needReset >= opts.getTearDownIncremental()) {
+ if (needReset >= options::getTearDownIncremental(opts))
+ {
pExecutor->reset();
for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
if (interrupted) break;
}
} else if(dynamic_cast<PopCommand*>(cmd.get()) != nullptr) {
allCommands.pop_back(); // fixme leaks cmds here
- if (needReset >= opts.getTearDownIncremental()) {
+ if (needReset >= options::getTearDownIncremental(opts))
+ {
pExecutor->reset();
for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
}
}
if (interrupted) continue;
- (*opts.getOut()) << CommandSuccess();
+ (*options::getOut(opts)) << CommandSuccess();
needReset = 0;
- } else {
+ }
+ else
+ {
status = pExecutor->doCommand(cmd);
if(cmd->interrupted()) {
interrupted = true;
}
} else if(dynamic_cast<CheckSatCommand*>(cmd.get()) != nullptr ||
dynamic_cast<QueryCommand*>(cmd.get()) != nullptr) {
- if(needReset >= opts.getTearDownIncremental()) {
+ if (needReset >= options::getTearDownIncremental(opts))
+ {
pExecutor->reset();
for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
}
}
needReset = 0;
- } else {
+ }
+ else
+ {
++needReset;
}
if (interrupted) {
}
}
}
- } else {
- if(!opts.wasSetByUserIncrementalSolving()) {
+ }
+ else
+ {
+ if (!options::wasSetByUserIncrementalSolving(opts))
+ {
cmd.reset(new SetOptionCommand("incremental", "false"));
cmd->setMuted(true);
pExecutor->doCommand(cmd);
opts);
std::unique_ptr<Parser> parser(parserBuilder.build());
if( inputFromStdin ) {
- parser->setInput(
- Input::newStreamInput(opts.getInputLanguage(), cin, filename));
+ parser->setInput(Input::newStreamInput(
+ options::getInputLanguage(opts), cin, filename));
}
else
{
- parser->setInput(Input::newFileInput(
- opts.getInputLanguage(), filename, opts.getMemoryMap()));
+ parser->setInput(Input::newFileInput(options::getInputLanguage(opts),
+ filename,
+ options::getMemoryMap(opts)));
}
bool interrupted = false;
while (status)
{
if (interrupted) {
- (*opts.getOut()) << CommandInterrupted();
+ (*options::getOut(opts)) << CommandInterrupted();
pExecutor->reset();
break;
}
}
#ifdef CVC5_COMPETITION_MODE
- opts.flushOut();
+ if (cvc5::options::getOut(options) != nullptr)
+ {
+ cvc5::options::getOut(options) << 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 (options::getEarlyExit(opts) && options::wasSetByUserEarlyExit(opts))
+ {
_exit(returnValue);
}
#else /* CVC5_DEBUG */
- if(opts.getEarlyExit()) {
+ if (options::getEarlyExit(opts))
+ {
_exit(returnValue);
}
#endif /* CVC5_DEBUG */
#include "expr/symbol_manager.h"
#include "options/language.h"
#include "options/options.h"
+#include "options/options_public.h"
#include "parser/input.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm)
: d_options(solver->getOptions()),
- d_in(*d_options.getIn()),
- d_out(*d_options.getOutConst()),
+ d_in(*options::getIn(d_options)),
+ d_out(*options::getOut(d_options)),
d_quit(false)
{
ParserBuilder parserBuilder(solver, sm, d_options);
/* Create parser with bogus input. */
d_parser = parserBuilder.build();
- if(d_options.wasSetByUserForceLogicString()) {
- LogicInfo tmp(d_options.getForceLogicString());
+ if (options::wasSetByUserForceLogicString(d_options))
+ {
+ LogicInfo tmp(options::getForceLogicString(d_options));
d_parser->forceLogic(tmp.getLogicString());
}
#endif /* EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP */
::using_history();
- OutputLanguage lang = toOutputLanguage(d_options.getInputLanguage());
+ OutputLanguage lang =
+ toOutputLanguage(options::getInputLanguage(d_options));
switch(lang) {
case output::LANG_CVC:
d_historyFilename = string(getenv("HOME")) + "/.cvc5_history";
if (d_usingEditline)
{
#if HAVE_LIBEDITLINE
- lineBuf = ::readline(d_options.getInteractivePrompt()
+ lineBuf = ::readline(options::getInteractivePrompt(d_options)
? (line == "" ? "cvc5> " : "... > ")
: "");
if(lineBuf != NULL && lineBuf[0] != '\0') {
}
else
{
- if(d_options.getInteractivePrompt()) {
+ if (options::getInteractivePrompt(d_options))
+ {
if(line == "") {
d_out << "cvc5> " << flush;
} else {
if (d_usingEditline)
{
#if HAVE_LIBEDITLINE
- lineBuf = ::readline(d_options.getInteractivePrompt() ? "... > " : "");
+ lineBuf = ::readline(options::getInteractivePrompt(d_options) ? "... > "
+ : "");
if(lineBuf != NULL && lineBuf[0] != '\0') {
::add_history(lineBuf);
}
}
else
{
- if(d_options.getInteractivePrompt()) {
+ if (options::getInteractivePrompt(d_options))
+ {
d_out << "... > " << flush;
}
}
}
- d_parser->setInput(Input::newStringInput(d_options.getInputLanguage(),
- input, INPUT_FILENAME));
+ d_parser->setInput(Input::newStringInput(
+ options::getInputLanguage(d_options), input, INPUT_FILENAME));
/* There may be more than one command in the input. Build up a
sequence. */
}
catch (ParserException& pe)
{
- if (language::isOutputLang_smt2(d_options.getOutputLanguage()))
+ if (language::isOutputLang_smt2(options::getOutputLanguage(d_options)))
{
d_out << "(error \"" << pe << "\")" << endl;
}
*/
#include "main/main.h"
+#include <stdio.h>
+#include <unistd.h>
+
#include <cstdlib>
#include <cstring>
#include <fstream>
#include <iostream>
-#include <stdio.h>
-#include <unistd.h>
#include "base/configuration.h"
#include "base/output.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"
return runCvc5(argc, argv, opts);
} catch(OptionException& e) {
#ifdef CVC5_COMPETITION_MODE
- *opts.getOut() << "unknown" << endl;
+ *options::getOut(opts) << "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
- *opts.getOut() << "unknown" << endl;
+ *options::getOut(opts) << "unknown" << endl;
#endif
- if (language::isOutputLang_smt2(opts.getOutputLanguage()))
+ if (language::isOutputLang_smt2(options::getOutputLanguage(opts)))
{
- *opts.getOut() << "(error \"" << e << "\")" << endl;
+ *options::getOut(opts) << "(error \"" << e << "\")" << endl;
} else {
- *opts.getErr() << "(error \"" << e << "\")" << endl;
+ *options::getErr(opts) << "(error \"" << e << "\")" << endl;
}
- if (opts.getStatistics() && pExecutor != nullptr)
+ if (options::getStatistics(opts) && pExecutor != nullptr)
{
totalTime.reset();
- pExecutor->printStatistics(*opts.getErr());
+ pExecutor->printStatistics(*options::getErr(opts));
}
}
exit(1);
#include <cstring>
#include "base/exception.h"
+#include "options/options_public.h"
#include "signal_handlers.h"
namespace cvc5 {
TimeLimit install_time_limit(const Options& opts)
{
- unsigned long ms = opts.getCumulativeTimeLimit();
+ unsigned long ms = options::getCumulativeTimeLimit(opts);
// Skip if no time limit shall be set.
if (ms == 0) {
return TimeLimit();
options_handler.cpp
options_handler.h
options_listener.h
- options_public_functions.cpp
+ options_public.cpp
+ options_public.h
printer_modes.cpp
printer_modes.h
set_language.cpp
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Tim King, Gereon Kremer, Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Definitions of public facing interface functions for Options.
+ *
+ * These are all one line wrappers for accessing the internal option data.
+ */
+
+#include "options_public.h"
+
+#include <fstream>
+#include <ostream>
+#include <string>
+#include <vector>
+
+#include "base/listener.h"
+#include "base/modal_exception.h"
+#include "options/base_options.h"
+#include "options/language.h"
+#include "options/main_options.h"
+#include "options/option_exception.h"
+#include "options/options.h"
+#include "options/parser_options.h"
+#include "options/printer_modes.h"
+#include "options/printer_options.h"
+#include "options/resource_manager_options.h"
+#include "options/smt_options.h"
+#include "options/uf_options.h"
+
+namespace cvc5::options {
+
+InputLanguage getInputLanguage(const Options& opts)
+{
+ return opts.base.inputLanguage;
+}
+InstFormatMode getInstFormatMode(const Options& opts)
+{
+ return opts.printer.instFormatMode;
+}
+OutputLanguage getOutputLanguage(const Options& opts)
+{
+ return opts.base.outputLanguage;
+}
+bool getUfHo(const Options& opts) { return opts.uf.ufHo; }
+bool getDumpInstantiations(const Options& opts)
+{
+ return opts.smt.dumpInstantiations;
+}
+bool getDumpModels(const Options& opts) { return opts.smt.dumpModels; }
+bool getDumpProofs(const Options& opts) { return opts.smt.dumpProofs; }
+bool getDumpUnsatCores(const Options& opts)
+{
+ return opts.smt.dumpUnsatCores || opts.smt.dumpUnsatCoresFull;
+}
+bool getEarlyExit(const Options& opts) { return opts.driver.earlyExit; }
+bool getFilesystemAccess(const Options& opts)
+{
+ return opts.parser.filesystemAccess;
+}
+bool getForceNoLimitCpuWhileDump(const Options& opts)
+{
+ return opts.smt.forceNoLimitCpuWhileDump;
+}
+bool getHelp(const Options& opts) { return opts.driver.help; }
+bool getIncrementalSolving(const Options& opts)
+{
+ return opts.smt.incrementalSolving;
+}
+bool getInteractive(const Options& opts) { return opts.driver.interactive; }
+bool getInteractivePrompt(const Options& opts)
+{
+ return opts.driver.interactivePrompt;
+}
+bool getLanguageHelp(const Options& opts) { return opts.base.languageHelp; }
+bool getMemoryMap(const Options& opts) { return opts.parser.memoryMap; }
+bool getParseOnly(const Options& opts) { return opts.base.parseOnly; }
+bool getProduceModels(const Options& opts) { return opts.smt.produceModels; }
+bool getSegvSpin(const Options& opts) { return opts.driver.segvSpin; }
+bool getSemanticChecks(const Options& opts)
+{
+ return opts.parser.semanticChecks;
+}
+bool getStatistics(const Options& opts) { return opts.base.statistics; }
+bool getStatsEveryQuery(const Options& opts)
+{
+ return opts.base.statisticsEveryQuery;
+}
+bool getStrictParsing(const Options& opts)
+{
+ return opts.parser.strictParsing;
+}
+int32_t getTearDownIncremental(const Options& opts)
+{
+ return opts.driver.tearDownIncremental;
+}
+uint64_t getCumulativeTimeLimit(const Options& opts)
+{
+ return opts.resman.cumulativeMillisecondLimit;
+}
+bool getVersion(const Options& opts) { return opts.driver.version; }
+const std::string& getForceLogicString(const Options& opts)
+{
+ return opts.parser.forceLogicString;
+}
+int32_t getVerbosity(const Options& opts) { return opts.base.verbosity; }
+
+std::istream* getIn(const Options& opts) { return opts.base.in; }
+std::ostream* getErr(const Options& opts) { return opts.base.err; }
+std::ostream* getOut(const Options& opts) { return opts.base.out; }
+const std::string& getBinaryName(const Options& opts)
+{
+ return opts.base.binary_name;
+}
+
+void setInputLanguage(InputLanguage val, Options& opts)
+{
+ opts.base.inputLanguage = val;
+}
+void setInteractive(bool val, Options& opts)
+{
+ opts.driver.interactive = val;
+}
+void setOut(std::ostream* val, Options& opts) { opts.base.out = val; }
+void setOutputLanguage(OutputLanguage val, Options& opts)
+{
+ opts.base.outputLanguage = val;
+}
+
+bool wasSetByUserEarlyExit(const Options& opts)
+{
+ return opts.driver.earlyExit__setByUser;
+}
+bool wasSetByUserForceLogicString(const Options& opts)
+{
+ return opts.parser.forceLogicString__setByUser;
+}
+bool wasSetByUserIncrementalSolving(const Options& opts)
+{
+ return opts.smt.incrementalSolving__setByUser;
+}
+bool wasSetByUserInteractive(const Options& opts)
+{
+ return opts.driver.interactive__setByUser;
+}
+
+} // namespace cvc5::options
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Gereon Kremer
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Public facing functions for options that need to be accessed from the
+ * outside.
+ *
+ * These are all one line wrappers for accessing the internal option data so
+ * that external code (including parser/ and main/) does not need to include
+ * the option modules (*_options.h).
+ */
+
+#include "cvc5_public.h"
+
+#ifndef CVC5__OPTIONS__OPTIONS_PUBLIC_H
+#define CVC5__OPTIONS__OPTIONS_PUBLIC_H
+
+#include "options/language.h"
+#include "options/options.h"
+#include "options/printer_modes.h"
+
+namespace cvc5::options {
+
+InputLanguage getInputLanguage(const Options& opts) CVC5_EXPORT;
+InstFormatMode getInstFormatMode(const Options& opts) CVC5_EXPORT;
+OutputLanguage getOutputLanguage(const Options& opts) CVC5_EXPORT;
+bool getUfHo(const Options& opts) CVC5_EXPORT;
+bool getDumpInstantiations(const Options& opts) CVC5_EXPORT;
+bool getDumpModels(const Options& opts) CVC5_EXPORT;
+bool getDumpProofs(const Options& opts) CVC5_EXPORT;
+bool getDumpUnsatCores(const Options& opts) CVC5_EXPORT;
+bool getEarlyExit(const Options& opts) CVC5_EXPORT;
+bool getFilesystemAccess(const Options& opts) CVC5_EXPORT;
+bool getForceNoLimitCpuWhileDump(const Options& opts) CVC5_EXPORT;
+bool getHelp(const Options& opts) CVC5_EXPORT;
+bool getIncrementalSolving(const Options& opts) CVC5_EXPORT;
+bool getInteractive(const Options& opts) CVC5_EXPORT;
+bool getInteractivePrompt(const Options& opts) CVC5_EXPORT;
+bool getLanguageHelp(const Options& opts) CVC5_EXPORT;
+bool getMemoryMap(const Options& opts) CVC5_EXPORT;
+bool getParseOnly(const Options& opts) CVC5_EXPORT;
+bool getProduceModels(const Options& opts) CVC5_EXPORT;
+bool getSegvSpin(const Options& opts) CVC5_EXPORT;
+bool getSemanticChecks(const Options& opts) CVC5_EXPORT;
+bool getStatistics(const Options& opts) CVC5_EXPORT;
+bool getStatsEveryQuery(const Options& opts) CVC5_EXPORT;
+bool getStrictParsing(const Options& opts) CVC5_EXPORT;
+int32_t getTearDownIncremental(const Options& opts) CVC5_EXPORT;
+uint64_t getCumulativeTimeLimit(const Options& opts) CVC5_EXPORT;
+bool getVersion(const Options& opts) CVC5_EXPORT;
+const std::string& getForceLogicString(const Options& opts) CVC5_EXPORT;
+int32_t getVerbosity(const Options& opts) CVC5_EXPORT;
+
+std::istream* getIn(const Options& opts) CVC5_EXPORT;
+std::ostream* getErr(const Options& opts) CVC5_EXPORT;
+std::ostream* getOut(const Options& opts) CVC5_EXPORT;
+const std::string& getBinaryName(const Options& opts) CVC5_EXPORT;
+
+void setInputLanguage(InputLanguage val, Options& opts) CVC5_EXPORT;
+void setInteractive(bool val, Options& opts) CVC5_EXPORT;
+void setOut(std::ostream* val, Options& opts) CVC5_EXPORT;
+void setOutputLanguage(OutputLanguage val, Options& opts) CVC5_EXPORT;
+
+bool wasSetByUserEarlyExit(const Options& opts) CVC5_EXPORT;
+bool wasSetByUserForceLogicString(const Options& opts) CVC5_EXPORT;
+bool wasSetByUserIncrementalSolving(const Options& opts) CVC5_EXPORT;
+bool wasSetByUserInteractive(const Options& opts) CVC5_EXPORT;
+
+} // namespace cvc5::options
+
+#endif
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Tim King, Gereon Kremer, Andrew Reynolds
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Definitions of public facing interface functions for Options.
- *
- * These are all 1 line wrappers for Options::get<T>, Options::set<T>, and
- * Options::wasSetByUser<T> for different option types T.
- */
-
-#include <fstream>
-#include <ostream>
-#include <string>
-#include <vector>
-
-#include "base/listener.h"
-#include "base/modal_exception.h"
-#include "options/options.h"
-#include "options/base_options.h"
-#include "options/language.h"
-#include "options/main_options.h"
-#include "options/option_exception.h"
-#include "options/parser_options.h"
-#include "options/printer_modes.h"
-#include "options/printer_options.h"
-#include "options/quantifiers_options.h"
-#include "options/resource_manager_options.h"
-#include "options/smt_options.h"
-#include "options/uf_options.h"
-
-namespace cvc5 {
-
-// Get accessor functions.
-InputLanguage Options::getInputLanguage() const {
- return (*this)[options::inputLanguage];
-}
-
-options::InstFormatMode Options::getInstFormatMode() const
-{
- return (*this)[options::instFormatMode];
-}
-
-OutputLanguage Options::getOutputLanguage() const {
- return (*this)[options::outputLanguage];
-}
-
-bool Options::getUfHo() const { return (*this)[options::ufHo]; }
-
-bool Options::getDumpInstantiations() const{
- return (*this)[options::dumpInstantiations];
-}
-
-bool Options::getDumpModels() const{
- return (*this)[options::dumpModels];
-}
-
-bool Options::getDumpProofs() const{
- return (*this)[options::dumpProofs];
-}
-
-bool Options::getDumpUnsatCores() const{
- // dump unsat cores full enables dumpUnsatCores
- return (*this)[options::dumpUnsatCores]
- || (*this)[options::dumpUnsatCoresFull];
-}
-
-bool Options::getEarlyExit() const{
- return (*this)[options::earlyExit];
-}
-
-bool Options::getFilesystemAccess() const{
- return (*this)[options::filesystemAccess];
-}
-
-bool Options::getForceNoLimitCpuWhileDump() const{
- return (*this)[options::forceNoLimitCpuWhileDump];
-}
-
-bool Options::getHelp() const{
- return (*this)[options::help];
-}
-
-bool Options::getIncrementalSolving() const{
- return (*this)[options::incrementalSolving];
-}
-
-bool Options::getInteractive() const{
- return (*this)[options::interactive];
-}
-
-bool Options::getInteractivePrompt() const{
- return (*this)[options::interactivePrompt];
-}
-
-bool Options::getLanguageHelp() const{
- return (*this)[options::languageHelp];
-}
-
-bool Options::getMemoryMap() const{
- return (*this)[options::memoryMap];
-}
-
-bool Options::getParseOnly() const{
- return (*this)[options::parseOnly];
-}
-
-bool Options::getProduceModels() const{
- return (*this)[options::produceModels];
-}
-
-bool Options::getSegvSpin() const{
- return (*this)[options::segvSpin];
-}
-
-bool Options::getSemanticChecks() const{
- return (*this)[options::semanticChecks];
-}
-
-bool Options::getStatistics() const{
- // statsEveryQuery enables stats
- return (*this)[options::statistics] || (*this)[options::statisticsEveryQuery];
-}
-
-bool Options::getStatsEveryQuery() const{
- return (*this)[options::statisticsEveryQuery];
-}
-
-bool Options::getStrictParsing() const{
- return (*this)[options::strictParsing];
-}
-
-int Options::getTearDownIncremental() const{
- return (*this)[options::tearDownIncremental];
-}
-
-uint64_t Options::getCumulativeTimeLimit() const
-{
- return (*this)[options::cumulativeMillisecondLimit];
-}
-
-bool Options::getVersion() const{
- return (*this)[options::version];
-}
-
-const std::string& Options::getForceLogicString() const{
- return (*this)[options::forceLogicString];
-}
-
-int Options::getVerbosity() const{
- return (*this)[options::verbosity];
-}
-
-std::istream* Options::getIn() const{
- return (*this)[options::in];
-}
-
-std::ostream* Options::getErr(){
- return (*this)[options::err];
-}
-
-std::ostream* Options::getOut(){
- return (*this)[options::out];
-}
-
-std::ostream* Options::getOutConst() const{
- // #warning "Remove Options::getOutConst"
- return (*this)[options::out];
-}
-
-std::string Options::getBinaryName() const{
- return (*this)[options::binary_name];
-}
-
-std::ostream* Options::currentGetOut() {
- return current().getOut();
-}
-
-
-// TODO: Document these.
-
-void Options::setInputLanguage(InputLanguage value) {
- base.inputLanguage = value;
-}
-
-void Options::setInteractive(bool value) {
- driver.interactive = value;
-}
-
-void Options::setOut(std::ostream* value) {
- base.out = value;
-}
-
-void Options::setOutputLanguage(OutputLanguage value) {
- base.outputLanguage = value;
-}
-
-bool Options::wasSetByUserEarlyExit() const {
- return wasSetByUser(options::earlyExit);
-}
-
-bool Options::wasSetByUserForceLogicString() const {
- return wasSetByUser(options::forceLogicString);
-}
-
-bool Options::wasSetByUserIncrementalSolving() const {
- return wasSetByUser(options::incrementalSolving);
-}
-
-bool Options::wasSetByUserInteractive() const {
- return wasSetByUser(options::interactive);
-}
-
-
-void Options::flushErr() {
- if(getErr() != NULL) {
- *(getErr()) << std::flush;
- }
-}
-
-void Options::flushOut() {
- if(getOut() != NULL) {
- *(getOut()) << std::flush;
- }
-}
-
-} // namespace cvc5
*/
std::string getOption(const std::string& key) const;
- // Get accessor functions.
- InputLanguage getInputLanguage() const;
- options::InstFormatMode getInstFormatMode() const;
- OutputLanguage getOutputLanguage() const;
- bool getUfHo() const;
- bool getDumpInstantiations() const;
- bool getDumpModels() const;
- bool getDumpProofs() const;
- bool getDumpUnsatCores() const;
- bool getEarlyExit() const;
- bool getFilesystemAccess() const;
- bool getForceNoLimitCpuWhileDump() const;
- bool getHelp() const;
- bool getIncrementalSolving() const;
- bool getInteractive() const;
- bool getInteractivePrompt() const;
- bool getLanguageHelp() const;
- bool getMemoryMap() const;
- bool getParseOnly() const;
- bool getProduceModels() const;
- bool getSegvSpin() const;
- bool getSemanticChecks() const;
- bool getStatistics() const;
- bool getStatsEveryQuery() const;
- bool getStrictParsing() const;
- int getTearDownIncremental() const;
- uint64_t getCumulativeTimeLimit() const;
- bool getVersion() const;
- const std::string& getForceLogicString() const;
- int getVerbosity() const;
- std::istream* getIn() const;
- std::ostream* getErr();
- std::ostream* getOut();
- std::ostream* getOutConst() const; // TODO: Remove this.
- std::string getBinaryName() const;
-
- // TODO: Document these.
- void setInputLanguage(InputLanguage);
- void setInteractive(bool);
- void setOut(std::ostream*);
- void setOutputLanguage(OutputLanguage);
-
- bool wasSetByUserEarlyExit() const;
- bool wasSetByUserForceLogicString() const;
- bool wasSetByUserIncrementalSolving() const;
- bool wasSetByUserInteractive() const;
-
// Static accessor functions.
// TODO: Document these.
static std::ostream* currentGetOut();
#include "base/output.h"
#include "expr/kind.h"
#include "options/options.h"
+#include "options/options_public.h"
#include "parser/input.h"
#include "parser/parser_exception.h"
#include "smt/command.h"
api::Term Parser::mkStringConstant(const std::string& s)
{
- if (language::isInputLang_smt2_6(d_solver->getOptions().getInputLanguage()))
+ if (language::isInputLang_smt2_6(
+ options::getInputLanguage(d_solver->getOptions())))
{
return d_solver->mkString(s, true);
}
#include "base/check.h"
#include "cvc/cvc.h"
#include "options/options.h"
+#include "options/options_public.h"
#include "parser/antlr_input.h"
#include "parser/input.h"
#include "parser/parser.h"
return *this;
}
-ParserBuilder& ParserBuilder::withOptions(const Options& options) {
+ParserBuilder& ParserBuilder::withOptions(const Options& opts)
+{
ParserBuilder& retval = *this;
- retval =
- retval.withInputLanguage(options.getInputLanguage())
- .withChecks(options.getSemanticChecks())
- .withStrictMode(options.getStrictParsing())
- .withParseOnly(options.getParseOnly())
- .withIncludeFile(options.getFilesystemAccess());
- if(options.wasSetByUserForceLogicString()) {
- LogicInfo tmp(options.getForceLogicString());
+ retval = retval.withInputLanguage(options::getInputLanguage(opts))
+ .withChecks(options::getSemanticChecks(opts))
+ .withStrictMode(options::getStrictParsing(opts))
+ .withParseOnly(options::getParseOnly(opts))
+ .withIncludeFile(options::getFilesystemAccess(opts));
+ if (options::wasSetByUserForceLogicString(opts))
+ {
+ LogicInfo tmp(options::getForceLogicString(opts));
retval = retval.withForcedLogic(tmp.getLogicString());
}
return retval;
ParserBuilder& withParseOnly(bool flag = true);
/** Derive settings from the given options. */
- ParserBuilder& withOptions(const Options& options);
+ ParserBuilder& withOptions(const Options& opts);
/**
* Should the parser use strict mode?
#include "base/check.h"
#include "options/options.h"
+#include "options/options_public.h"
#include "parser/antlr_input.h"
#include "parser/parser.h"
#include "parser/smt2/smt2_input.h"
bool Smt2::isHoEnabled() const
{
- return getLogic().isHigherOrder() && d_solver->getOptions().getUfHo();
+ return getLogic().isHigherOrder() && options::getUfHo(d_solver->getOptions());
}
bool Smt2::logicIsSet() {
InputLanguage Smt2::getLanguage() const
{
- return d_solver->getOptions().getInputLanguage();
+ return options::getInputLanguage(d_solver->getOptions());
}
void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type)
}
else if (isBuiltinOperator)
{
- if (!opts.getUfHo() && (kind == api::EQUAL || kind == api::DISTINCT))
+ if (!options::getUfHo(opts)
+ && (kind == api::EQUAL || kind == api::DISTINCT))
{
// need --uf-ho if these operators are applied over function args
for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
unsigned arity = argt.getFunctionArity();
if (args.size() - 1 < arity)
{
- if (!opts.getUfHo())
+ if (!options::getUfHo(opts))
{
parseError("Cannot partially apply functions unless --uf-ho is set.");
}
#include "api/cpp/cvc5.h"
#include "base/check.h"
#include "options/options.h"
+#include "options/options_public.h"
#include "parser/parser.h"
#include "smt/command.h"
// Second phase: apply parse op to the arguments
if (isBuiltinKind)
{
- if (!opts.getUfHo() && (kind == api::EQUAL || kind == api::DISTINCT))
+ if (!options::getUfHo(opts)
+ && (kind == api::EQUAL || kind == api::DISTINCT))
{
// need --uf-ho if these operators are applied over function args
for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
unsigned arity = argt.getFunctionArity();
if (args.size() - 1 < arity)
{
- if (!opts.getUfHo())
+ if (!options::getUfHo(opts))
{
parseError("Cannot partially apply functions unless --uf-ho is set.");
}
return *Printer::getPrinter(d_options[options::outputLanguage]);
}
-std::ostream& Env::getDumpOut() { return *d_options.getOut(); }
+std::ostream& Env::getDumpOut() { return *d_options.base.out; }
} // namespace cvc5
#include "smt/output_manager.h"
+#include "options/base_options.h"
#include "smt/smt_engine.h"
namespace cvc5 {
std::ostream& OutputManager::getDumpOut() const
{
- return *d_smt->getOptions().getOut();
+ return *d_smt->getOptions().base.out;
}
} // namespace cvc5
Node query)
{
Assert (!query.isNull());
- if (Options::current().wasSetByUser(options::sygusExprMinerCheckTimeout))
+ if (Options::current().quantifiers.sygusExprMinerCheckTimeout__setByUser)
{
initializeSubsolver(checker, true, options::sygusExprMinerCheckTimeout());
}
#include "theory/quantifiers/solution_filter.h"
#include <fstream>
+
+#include "options/base_options.h"
#include "options/quantifiers_options.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
else
{
Options& opts = smt::currentSmtEngine()->getOptions();
- std::ostream* smtOut = opts.getOut();
+ std::ostream* smtOut = opts.base.out;
(*smtOut) << "; (filtered " << (d_isStrong ? s : s.negate()) << ")"
<< std::endl;
}
if (printDebug)
{
Options& sopts = smt::currentSmtEngine()->getOptions();
- std::ostream& out = *sopts.getOut();
+ std::ostream& out = *sopts.base.out;
out << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl;
}
}
if (printDebug)
{
Options& sopts = smt::currentSmtEngine()->getOptions();
- std::ostream& out = *sopts.getOut();
+ std::ostream& out = *sopts.base.out;
out << "(sygus-candidate ";
Assert(d_quant[0].getNumChildren() == candidate_values.size());
for (unsigned i = 0, ncands = candidate_values.size(); i < ncands; i++)
// we have generated a solution, print it
// get the current output stream
Options& sopts = smt::currentSmtEngine()->getOptions();
- printSynthSolutionInternal(*sopts.getOut());
+ printSynthSolutionInternal(*sopts.base.out);
excludeCurrentSolution(enums, values);
}
}
// we have detected unsoundness in the rewriter
Options& sopts = smt::currentSmtEngine()->getOptions();
- std::ostream* out = sopts.getOut();
+ std::ostream* out = sopts.base.out;
(*out) << "(unsound-rewrite " << bv << " " << bvr << ")" << std::endl;
// debugging information
(*out) << "Terms are not equivalent for : " << std::endl;
#include "theory/quantifiers_engine.h"
+#include "options/base_options.h"
#include "options/printer_options.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
if (options::debugInst() || debugInstTrace)
{
Options& sopts = smt::currentSmtEngine()->getOptions();
- std::ostream& out = *sopts.getOut();
+ std::ostream& out = *sopts.base.out;
d_qim.getInstantiate()->debugPrint(out);
}
}
#include "api/cpp/cvc5.h"
#include "options/options.h"
+#include "options/options_public.h"
#include "options/set_language.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
int main()
{
Options opts;
- opts.setInputLanguage(language::input::LANG_SMTLIB_V2);
- opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
+ options::setInputLanguage(language::input::LANG_SMTLIB_V2, opts);
+ options::setOutputLanguage(language::output::LANG_SMTLIB_V2, opts);
cout << language::SetLanguage(language::output::LANG_SMTLIB_V2);
projects / cvc5.git / commitdiff