diff options
Diffstat (limited to 'src')
36 files changed, 567 insertions, 567 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 0f2d5ad1b..668fc9382 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -4743,7 +4743,7 @@ Solver::Solver(Options* opts) } d_smtEngine.reset(new SmtEngine(d_nodeMgr.get(), d_originalOptions.get())); d_smtEngine->setSolver(this); - d_rng.reset(new Random(d_smtEngine->getOptions()[options::seed])); + d_rng.reset(new Random(d_smtEngine->getOptions().driver.seed)); resetStatistics(); } @@ -6452,7 +6452,7 @@ Result Solver::checkEntailed(const Term& term) const NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions()[options::incrementalSolving]) + || d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERM(term); @@ -6468,7 +6468,7 @@ Result Solver::checkEntailed(const std::vector<Term>& terms) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions()[options::incrementalSolving]) + || d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERMS(terms); @@ -6497,7 +6497,7 @@ Result Solver::checkSat(void) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions()[options::incrementalSolving]) + || d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; //////// all checks before this line @@ -6512,7 +6512,7 @@ Result Solver::checkSatAssuming(const Term& assumption) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions()[options::incrementalSolving]) + || d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(assumption, getBooleanSort()); @@ -6528,7 +6528,7 @@ Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() || assumptions.size() == 0 - || d_smtEngine->getOptions()[options::incrementalSolving]) + || d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERMS_WITH_SORT(assumptions, getBooleanSort()); @@ -6863,10 +6863,10 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const { CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); - CVC5_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot get unsat assumptions unless incremental solving is enabled " "(try --incremental)"; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::unsatAssumptions]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.unsatAssumptions) << "Cannot get unsat assumptions unless explicitly enabled " "(try --produce-unsat-assumptions)"; CVC5_API_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT) @@ -6891,7 +6891,7 @@ std::vector<Term> Solver::getUnsatCore(void) const { CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); - CVC5_API_CHECK(d_smtEngine->getOptions()[options::unsatCores]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.unsatCores) << "Cannot get unsat core unless explicitly enabled " "(try --produce-unsat-cores)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT) @@ -6925,7 +6925,7 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const { CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); - CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions()[options::produceModels]) + CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) @@ -6992,7 +6992,7 @@ Term Solver::getSeparationHeap() const d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) << "Cannot obtain separation logic expressions if not using the " "separation logic theory."; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get separation heap term unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) @@ -7011,7 +7011,7 @@ Term Solver::getSeparationNilTerm() const d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) << "Cannot obtain separation logic expressions if not using the " "separation logic theory."; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get separation nil term unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) @@ -7044,7 +7044,7 @@ void Solver::pop(uint32_t nscopes) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot pop when not solving incrementally (use --incremental)"; CVC5_API_CHECK(nscopes <= d_smtEngine->getNumUserLevels()) << "Cannot pop beyond first pushed context"; @@ -7133,7 +7133,7 @@ void Solver::blockModel() const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) @@ -7148,7 +7148,7 @@ void Solver::blockModelValues(const std::vector<Term>& terms) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) @@ -7176,7 +7176,7 @@ void Solver::push(uint32_t nscopes) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot push when not solving incrementally (use --incremental)"; //////// all checks before this line for (uint32_t n = 0; n < nscopes; ++n) diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index c8e977f1f..5759ec856 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -26,6 +26,7 @@ #include <vector> #include "main/main.h" +#include "options/options_public.h" #include "smt/command.h" #include "smt/smt_engine.h" @@ -64,7 +65,7 @@ CommandExecutor::~CommandExecutor() void CommandExecutor::printStatistics(std::ostream& out) const { - if (d_options.getStatistics()) + if (options::getStatistics(d_options)) { getSmtEngine()->printStatistics(out); } @@ -72,7 +73,7 @@ void CommandExecutor::printStatistics(std::ostream& out) const void CommandExecutor::printStatisticsSafe(int fd) const { - if (d_options.getStatistics()) + if (options::getStatistics(d_options)) { getSmtEngine()->printStatisticsSafe(fd); } @@ -80,7 +81,8 @@ void CommandExecutor::printStatisticsSafe(int fd) const bool CommandExecutor::doCommand(Command* cmd) { - if( d_options.getParseOnly() ) { + if (options::getParseOnly(d_options)) + { return true; } @@ -98,8 +100,9 @@ bool CommandExecutor::doCommand(Command* cmd) 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); @@ -108,7 +111,7 @@ bool CommandExecutor::doCommand(Command* 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 @@ -121,10 +124,13 @@ void CommandExecutor::reset() 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); } @@ -144,8 +150,9 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) 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(); @@ -153,20 +160,21 @@ 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 (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() @@ -176,14 +184,15 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) 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) { @@ -222,11 +231,18 @@ bool solverInvoke(api::Solver* solver, } 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 diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index a26ee3b73..79c98924a 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -34,6 +34,7 @@ #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" @@ -78,16 +79,17 @@ TotalTimer::~TotalTimer() 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))); } } @@ -107,25 +109,30 @@ int runCvc5(int argc, char* argv[], Options& 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 @@ -137,8 +144,9 @@ 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(!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 @@ -150,30 +158,33 @@ int runCvc5(int argc, char* argv[], Options& opts) } 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 @@ -187,7 +198,8 @@ int runCvc5(int argc, char* argv[], Options& opts) } // 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); @@ -200,19 +212,23 @@ int runCvc5(int argc, char* argv[], Options& 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()) { @@ -230,7 +246,7 @@ int runCvc5(int argc, char* argv[], Options& opts) try { cmd.reset(shell.readCommand()); } catch(UnsafeInterruptException& e) { - (*opts.getOut()) << CommandInterrupted(); + (*options::getOut(opts)) << CommandInterrupted(); break; } if (cmd == nullptr) @@ -240,14 +256,18 @@ int runCvc5(int argc, char* argv[], Options& opts) 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"); // } @@ -262,13 +282,14 @@ int runCvc5(int argc, char* argv[], Options& opts) 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; @@ -279,7 +300,7 @@ int runCvc5(int argc, char* argv[], Options& opts) while (status) { if (interrupted) { - (*opts.getOut()) << CommandInterrupted(); + (*options::getOut(opts)) << CommandInterrupted(); break; } @@ -292,7 +313,8 @@ int runCvc5(int argc, char* argv[], Options& opts) } 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; @@ -320,7 +342,8 @@ int runCvc5(int argc, char* argv[], Options& opts) } } 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) @@ -335,9 +358,11 @@ int runCvc5(int argc, char* argv[], Options& opts) } } if (interrupted) continue; - (*opts.getOut()) << CommandSuccess(); + (*options::getOut(opts)) << CommandSuccess(); needReset = 0; - } else { + } + else + { status = pExecutor->doCommand(cmd); if(cmd->interrupted()) { interrupted = true; @@ -346,7 +371,8 @@ int runCvc5(int argc, char* argv[], Options& opts) } } 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) @@ -362,7 +388,9 @@ int runCvc5(int argc, char* argv[], Options& opts) } } needReset = 0; - } else { + } + else + { ++needReset; } if (interrupted) { @@ -406,8 +434,11 @@ int runCvc5(int argc, char* argv[], Options& opts) } } } - } else { - if(!opts.wasSetByUserIncrementalSolving()) { + } + else + { + if (!options::wasSetByUserIncrementalSolving(opts)) + { cmd.reset(new SetOptionCommand("incremental", "false")); cmd->setMuted(true); pExecutor->doCommand(cmd); @@ -418,20 +449,21 @@ int runCvc5(int argc, char* argv[], Options& opts) 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; } @@ -465,7 +497,10 @@ int runCvc5(int argc, char* argv[], Options& opts) } #ifdef CVC5_COMPETITION_MODE - opts.flushOut(); + if (cvc5::options::getOut(opts) != nullptr) + { + cvc5::options::getOut(opts) << 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. @@ -476,11 +511,13 @@ int runCvc5(int argc, char* argv[], Options& opts) 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 */ diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 8ca10799f..9a0539490 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -42,6 +42,7 @@ #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" @@ -87,15 +88,16 @@ static set<string> s_declarations; 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()); } @@ -109,7 +111,8 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm) #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"; @@ -195,7 +198,7 @@ restart: 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') { @@ -207,7 +210,8 @@ restart: } else { - if(d_options.getInteractivePrompt()) { + if (options::getInteractivePrompt(d_options)) + { if(line == "") { d_out << "cvc5> " << flush; } else { @@ -280,7 +284,8 @@ restart: 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); } @@ -290,7 +295,8 @@ restart: } else { - if(d_options.getInteractivePrompt()) { + if (options::getInteractivePrompt(d_options)) + { d_out << "... > " << flush; } @@ -306,8 +312,8 @@ restart: } } - 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. */ @@ -358,7 +364,7 @@ restart: } catch (ParserException& pe) { - if (language::isOutputLang_smt2(d_options.getOutputLanguage())) + if (language::isOutputLang_smt2(options::getOutputLanguage(d_options))) { d_out << "(error \"" << pe << "\")" << endl; } diff --git a/src/main/main.cpp b/src/main/main.cpp index b96598b0b..2b25e6c93 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -14,12 +14,13 @@ */ #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" @@ -28,6 +29,7 @@ #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" @@ -51,25 +53,25 @@ int main(int argc, char* argv[]) { 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); diff --git a/src/main/time_limit.cpp b/src/main/time_limit.cpp index 0f0a824f6..c0fc6846a 100644 --- a/src/main/time_limit.cpp +++ b/src/main/time_limit.cpp @@ -56,6 +56,7 @@ #include <cstring> #include "base/exception.h" +#include "options/options_public.h" #include "signal_handlers.h" namespace cvc5 { @@ -79,7 +80,7 @@ TimeLimit::~TimeLimit() 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(); diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index 2107865c0..978c32888 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -30,7 +30,8 @@ libcvc5_add_sources( 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 diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index fc52dfe0d..c355ff436 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -80,35 +80,25 @@ g_getopt_long_start = 256 ### Source code templates -TPL_IMPL_ASSIGN = \ -"""template <> void Options::assign( - options::{name}__option_t, - std::string option, - std::string optionarg) -{{ - auto parsedval = {handler}; +TPL_ASSIGN = ''' +void assign_{module}_{name}(Options& opts, const std::string& option, const std::string& optionarg) {{ + auto value = {handler}; {predicates} - {module}.{name} = parsedval; - {module}.{name}__setByUser = true; - Trace("options") << "user assigned option {name}" << std::endl; -}}""" + opts.{module}.{name} = value; + opts.{module}.{name}__setByUser = true; + Trace("options") << "user assigned option {name} = " << value << std::endl; +}}''' -TPL_IMPL_ASSIGN_BOOL = \ -"""template <> void Options::assignBool( - options::{name}__option_t, - std::string option, - bool value) -{{ +TPL_ASSIGN_BOOL = ''' +void assign_{module}_{name}(Options& opts, const std::string& option, bool value) {{ {predicates} - {module}.{name} = value; - {module}.{name}__setByUser = true; - Trace("options") << "user assigned option {name}" << std::endl; -}}""" - -TPL_CALL_ASSIGN_BOOL = \ - ' assignBool(options::{name}, {option}, {value});' + opts.{module}.{name} = value; + opts.{module}.{name}__setByUser = true; + Trace("options") << "user assigned option {name} = " << value << std::endl; +}}''' -TPL_CALL_ASSIGN = ' assign(options::{name}, {option}, optionarg);' +TPL_CALL_ASSIGN_BOOL = ' assign_{module}_{name}(opts, {option}, {value});' +TPL_CALL_ASSIGN = ' assign_{module}_{name}(opts, {option}, optionarg);' TPL_CALL_SET_OPTION = 'setOption(std::string("{smtname}"), ("{value}"));' @@ -139,16 +129,6 @@ TPL_OPTION_STRUCT_RW = \ type operator()() const; }} thread_local {name};""" -TPL_DECL_OP_BRACKET = \ -"""template <> const options::{name}__option_t::type& Options::operator[]( - options::{name}__option_t) const;""" - -TPL_IMPL_OP_BRACKET = TPL_DECL_OP_BRACKET[:-1] + \ -""" -{{ - return {module}.{name}; -}}""" - TPL_DECL_WAS_SET_BY_USER = \ """template <> bool Options::wasSetByUser(options::{name}__option_t) const;""" @@ -161,10 +141,8 @@ TPL_IMPL_WAS_SET_BY_USER = TPL_DECL_WAS_SET_BY_USER[:-1] + \ # Option specific methods TPL_IMPL_OP_PAR = \ -"""inline {name}__option_t::type {name}__option_t::operator()() const -{{ - return Options::current()[*this]; -}}""" +"""inline {type} {name}__option_t::operator()() const +{{ return Options::current().{module}.{name}; }}""" # Mode templates TPL_DECL_MODE_ENUM = \ @@ -601,7 +579,6 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): # Generate module specialization default_decl.append(TPL_DECL_SET_DEFAULT.format(module=module.id, name=option.name, funcname=capoptionname, type=option.type)) - specs.append(TPL_DECL_OP_BRACKET.format(name=option.name)) specs.append(TPL_DECL_WAS_SET_BY_USER.format(name=option.name)) if option.long and option.type not in ['bool', 'void'] and \ @@ -616,14 +593,13 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): module.id, option.long, option.type)) # Generate module inlines - inls.append(TPL_IMPL_OP_PAR.format(name=option.name)) + inls.append(TPL_IMPL_OP_PAR.format(module=module.id, name=option.name, type=option.type)) ### Generate code for {module.name}_options.cpp # Accessors default_impl.append(TPL_IMPL_SET_DEFAULT.format(module=module.id, name=option.name, funcname=capoptionname, type=option.type)) - accs.append(TPL_IMPL_OP_BRACKET.format(module=module.id, name=option.name)) accs.append(TPL_IMPL_WAS_SET_BY_USER.format(module=module.id, name=option.name)) # Global definitions @@ -770,10 +746,10 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ handler = None if option.handler: if option.type == 'void': - handler = 'd_handler->{}(option)'.format(option.handler) + handler = 'opts.handler().{}(option)'.format(option.handler) else: handler = \ - 'd_handler->{}(option, optionarg)'.format(option.handler) + 'opts.handler().{}(option, optionarg)'.format(option.handler) elif option.mode: handler = 'stringTo{}(optionarg)'.format(option.type) elif option.type != 'bool': @@ -785,12 +761,12 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ if option.predicates: if option.type == 'bool': predicates = \ - ['d_handler->{}(option, value);'.format(x) \ + ['opts.handler().{}(option, value);'.format(x) \ for x in option.predicates] else: assert option.type != 'void' predicates = \ - ['d_handler->{}(option, parsedval);'.format(x) \ + ['opts.handler().{}(option, value);'.format(x) \ for x in option.predicates] # Generate options_handler and getopt_long @@ -820,12 +796,14 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ if option.type == 'bool' and option.name: cases.append( TPL_CALL_ASSIGN_BOOL.format( + module=module.id, name=option.name, option='option', value='true')) elif option.type != 'void' and option.name: cases.append( TPL_CALL_ASSIGN.format( + module=module.id, name=option.name, option='option', value='optionarg')) @@ -854,12 +832,14 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ if option.type == 'bool': setoption_handlers.append( TPL_CALL_ASSIGN_BOOL.format( + module=module.id, name=option.name, option='key', value='optionarg == "true"')) elif argument_req and option.name: setoption_handlers.append( TPL_CALL_ASSIGN.format( + module=module.id, name=option.name, option='key')) elif option.handler: @@ -878,17 +858,17 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ 'if ({}) {{'.format(cond)) if option.type == 'bool': getoption_handlers.append( - 'return (*this)[options::{}] ? "true" : "false";'.format(option.name)) + 'return options.{}.{} ? "true" : "false";'.format(module.id, option.name)) elif option.type == 'std::string': getoption_handlers.append( - 'return (*this)[options::{}];'.format(option.name)) + 'return options.{}.{};'.format(module.id, option.name)) elif is_numeric_cpp_type(option.type): getoption_handlers.append( - 'return std::to_string((*this)[options::{}]);'.format(option.name)) + 'return std::to_string(options.{}.{});'.format(module.id, option.name)) else: getoption_handlers.append('std::stringstream ss;') getoption_handlers.append( - 'ss << (*this)[options::{}];'.format(option.name)) + 'ss << options.{}.{};'.format(module.id, option.name)) getoption_handlers.append('return ss.str();') getoption_handlers.append('}') @@ -914,9 +894,9 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ cases.append( TPL_CALL_ASSIGN_BOOL.format( + module=module.id, name=option.name, option='option', value='false')) cases.append(' break;') - options_handler.extend(cases) optname = option.long @@ -943,13 +923,15 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ # Define handler assign/assignBool - tpl = None if option.type == 'bool': - tpl = TPL_IMPL_ASSIGN_BOOL + custom_handlers.append(TPL_ASSIGN_BOOL.format( + module=module.id, + name=option.name, + handler=handler, + predicates='\n'.join(predicates) + )) elif option.short or option.long: - tpl = TPL_IMPL_ASSIGN - if tpl: - custom_handlers.append(tpl.format( + custom_handlers.append(TPL_ASSIGN.format( module=module.id, name=option.name, handler=handler, diff --git a/src/options/options_public.cpp b/src/options/options_public.cpp new file mode 100644 index 000000000..778056553 --- /dev/null +++ b/src/options/options_public.cpp @@ -0,0 +1,155 @@ +/****************************************************************************** + * 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 diff --git a/src/options/options_public.h b/src/options/options_public.h new file mode 100644 index 000000000..a6d93cae7 --- /dev/null +++ b/src/options/options_public.h @@ -0,0 +1,79 @@ +/****************************************************************************** + * 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 diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp deleted file mode 100644 index 2789b2d68..000000000 --- a/src/options/options_public_functions.cpp +++ /dev/null @@ -1,234 +0,0 @@ -/****************************************************************************** - * 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 diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 091acfd7a..0d6b7f01b 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -416,7 +416,7 @@ void Options::parseOptionsRecursive(int argc, char* argv[], std::vector<std::string>* nonoptions) { - + Options& opts = *this; if(Debug.isOn("options")) { Debug("options") << "starting a new parseOptionsRecursive with " << argc << " arguments" << std::endl; @@ -553,6 +553,7 @@ void Options::setOptionInternal(const std::string& key, const std::string& optionarg) { options::OptionsHandler* handler = d_handler; + Options& opts = *this; ${setoption_handlers}$ throw UnrecognizedOptionException(key); } @@ -562,6 +563,7 @@ void Options::setOptionInternal(const std::string& key, std::string Options::getOption(const std::string& key) const { Trace("options") << "Options::getOption(" << key << ")" << std::endl; + const Options& options = *this; ${getoption_handlers}$ throw UnrecognizedOptionException(key); diff --git a/src/options/options_template.h b/src/options/options_template.h index 502dfb833..6ce77d7a1 100644 --- a/src/options/options_template.h +++ b/src/options/options_template.h @@ -63,13 +63,6 @@ ${holder_ref_decls}$ /** The current Options in effect */ static thread_local Options* s_current; - /** Low-level assignment function for options */ - template <class T> - void assign(T, std::string option, std::string value); - /** Low-level assignment function for bool-valued options */ - template <class T> - void assignBool(T, std::string option, bool value); - friend class options::OptionsHandler; /** @@ -113,6 +106,9 @@ public: Options(OptionsListener* ol = nullptr); ~Options(); + options::OptionsHandler& handler() const { + return *d_handler; + } /** * Copies the value of the options stored in OptionsHolder into the current @@ -128,10 +124,6 @@ public: */ void setOption(const std::string& key, const std::string& optionarg); - /** Get the value of the given option. Const access only. */ - template <class T> - const typename T::type& operator[](T) const; - /** * Gets the value of the given option by key and returns value as a string. * @@ -140,53 +132,6 @@ public: */ 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(); diff --git a/src/options/printer_modes.cpp b/src/options/printer_modes.cpp index fc765db01..b2d8ec79a 100644 --- a/src/options/printer_modes.cpp +++ b/src/options/printer_modes.cpp @@ -18,9 +18,9 @@ #include "options/printer_modes.h" -namespace cvc5 { +namespace cvc5::options { -std::ostream& operator<<(std::ostream& out, options::InstFormatMode mode) +std::ostream& operator<<(std::ostream& out, InstFormatMode mode) { out << "InstFormatMode::"; switch (mode) diff --git a/src/options/printer_modes.h b/src/options/printer_modes.h index e27cb133f..093bff7d9 100644 --- a/src/options/printer_modes.h +++ b/src/options/printer_modes.h @@ -36,9 +36,9 @@ enum class InstFormatMode SZS, }; -} // namespace options +std::ostream& operator<<(std::ostream& out, InstFormatMode mode); -std::ostream& operator<<(std::ostream& out, options::InstFormatMode mode); +} // namespace options } // namespace cvc5 diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index eb952f8db..f6592a931 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -27,6 +27,7 @@ #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" @@ -898,7 +899,8 @@ std::wstring Parser::processAdHocStringEsc(const std::string& s) 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); } diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 26a867f95..e4f46326f 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -22,6 +22,7 @@ #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" @@ -116,16 +117,17 @@ ParserBuilder& ParserBuilder::withParseOnly(bool flag) { 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; diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 992ca408a..aed3b06f1 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -109,7 +109,7 @@ class CVC5_EXPORT ParserBuilder 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? diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index d32f149bf..4f5440944 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -18,6 +18,7 @@ #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" @@ -316,7 +317,7 @@ bool Smt2::isTheoryEnabled(theory::TheoryId theory) const bool Smt2::isHoEnabled() const { - return getLogic().isHigherOrder() && d_solver->getOptions().getUfHo(); + return getLogic().isHigherOrder() && options::getUfHo(d_solver->getOptions()); } bool Smt2::logicIsSet() { @@ -842,7 +843,7 @@ api::Term Smt2::mkAbstractValue(const std::string& name) InputLanguage Smt2::getLanguage() const { - return d_solver->getOptions().getInputLanguage(); + return options::getInputLanguage(d_solver->getOptions()); } void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type) @@ -1094,7 +1095,8 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) } 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(); @@ -1146,7 +1148,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) 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."); } diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 156f2e1e6..764e83361 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -22,6 +22,7 @@ #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" @@ -315,7 +316,8 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args) // 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(); @@ -362,7 +364,7 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args) 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."); } diff --git a/src/smt/env.cpp b/src/smt/env.cpp index 647981ab3..1381ef87c 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -104,9 +104,9 @@ ResourceManager* Env::getResourceManager() const const Printer& Env::getPrinter() { - return *Printer::getPrinter(d_options[options::outputLanguage]); + return *Printer::getPrinter(d_options.base.outputLanguage); } -std::ostream& Env::getDumpOut() { return *d_options.getOut(); } +std::ostream& Env::getDumpOut() { return *d_options.base.out; } } // namespace cvc5 diff --git a/src/smt/env.h b/src/smt/env.h index 667497683..29a360209 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -91,12 +91,6 @@ class Env /** Get a pointer to the underlying dump manager. */ smt::DumpManager* getDumpManager(); - template <typename Opt> - const auto& getOption(Opt opt) const - { - return d_options[opt]; - } - /** Get the options object (const version only) owned by this Env. */ const Options& getOptions() const; diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp index 3fc58ff05..37541751e 100644 --- a/src/smt/options_manager.cpp +++ b/src/smt/options_manager.cpp @@ -71,7 +71,7 @@ void OptionsManager::notifySetOption(const std::string& key) << std::endl; if (key == options::expr::defaultExprDepth__name) { - int depth = (*d_options)[options::defaultExprDepth]; + int depth = d_options->expr.defaultExprDepth; Debug.getStream() << expr::ExprSetDepth(depth); Trace.getStream() << expr::ExprSetDepth(depth); Notice.getStream() << expr::ExprSetDepth(depth); @@ -82,7 +82,7 @@ void OptionsManager::notifySetOption(const std::string& key) } else if (key == options::expr::defaultDagThresh__name) { - int dag = (*d_options)[options::defaultDagThresh]; + int dag = d_options->expr.defaultDagThresh; Debug.getStream() << expr::ExprDag(dag); Trace.getStream() << expr::ExprDag(dag); Notice.getStream() << expr::ExprDag(dag); @@ -93,12 +93,12 @@ void OptionsManager::notifySetOption(const std::string& key) } else if (key == options::smt::dumpModeString__name) { - const std::string& value = (*d_options)[options::dumpModeString]; + const std::string& value = d_options->smt.dumpModeString; Dump.setDumpFromString(value); } else if (key == options::base::printSuccess__name) { - bool value = (*d_options)[options::printSuccess]; + bool value = d_options->base.printSuccess; Debug.getStream() << Command::printsuccess(value); Trace.getStream() << Command::printsuccess(value); Notice.getStream() << Command::printsuccess(value); diff --git a/src/smt/output_manager.cpp b/src/smt/output_manager.cpp index 6395a4c2c..aa91bb184 100644 --- a/src/smt/output_manager.cpp +++ b/src/smt/output_manager.cpp @@ -15,6 +15,7 @@ #include "smt/output_manager.h" +#include "options/base_options.h" #include "smt/smt_engine.h" namespace cvc5 { @@ -25,7 +26,7 @@ const Printer& OutputManager::getPrinter() const { return d_smt->getPrinter(); } std::ostream& OutputManager::getDumpOut() const { - return *d_smt->getOptions().getOut(); + return *d_smt->getOptions().base.out; } } // namespace cvc5 diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index ad1e40c77..55cfc1f15 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -130,9 +130,8 @@ void PfManager::setFinalProof(std::shared_ptr<ProofNode> pfn, Assertions& as) Trace("smt-proof") << "SmtEngine::setFinalProof(): make scope...\n"; // Now make the final scope, which ensures that the only open leaves of the - // proof are the assertions, unless we are doing proofs to generate unsat - // cores, in which case we do not care. - d_finalProof = d_pnm->mkScope(pfn, assertions, !options::unsatCores()); + // proof are the assertions. + d_finalProof = d_pnm->mkScope(pfn, assertions); Trace("smt-proof") << "SmtEngine::setFinalProof(): finished.\n"; } diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 135fabf5f..96081e97b 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -1523,12 +1523,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (opts.wasSetByUser(options::nlCad)) { std::stringstream ss; - ss << "Cannot use " << options::nlCad.name << " without configuring with --poly."; + ss << "Cannot use " << options::arith::nlCad__name << " without configuring with --poly."; throw OptionException(ss.str()); } else { - Notice() << "Cannot use --" << options::nlCad.name + Notice() << "Cannot use --" << options::arith::nlCad__name << " without configuring with --poly." << std::endl; opts.arith.nlCad = false; opts.arith.nlExt = options::NlExtMode::FULL; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7abeac44f..c84a29055 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -193,7 +193,7 @@ void SmtEngine::finishInit() } // set the random seed - Random::getRandom().setSeed(d_env->getOption(options::seed)); + Random::getRandom().setSeed(d_env->getOptions().driver.seed); // Call finish init on the options manager. This inializes the resource // manager based on the options, and sets up the best default options @@ -201,7 +201,7 @@ void SmtEngine::finishInit() d_optm->finishInit(d_env->d_logic, d_isInternalSubsolver); ProofNodeManager* pnm = nullptr; - if (d_env->getOption(options::produceProofs)) + if (d_env->getOptions().smt.produceProofs) { // ensure bound variable uses canonical bound variables getNodeManager()->getBoundVarManager()->enableKeepCacheValues(); @@ -262,11 +262,11 @@ void SmtEngine::finishInit() getDumpManager()->finishInit(); // subsolvers - if (d_env->getOption(options::produceAbducts)) + if (d_env->getOptions().smt.produceAbducts) { d_abductSolver.reset(new AbductionSolver(this)); } - if (d_env->getOption(options::produceInterpols) + if (d_env->getOptions().smt.produceInterpols != options::ProduceInterpols::NONE) { d_interpolSolver.reset(new InterpolationSolver(this)); @@ -459,10 +459,10 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value) if (!Options::current().wasSetByUser(options::outputLanguage)) { language::output::Language olang = language::toOutputLanguage(ilang); - if (d_env->getOption(options::outputLanguage) != olang) + if (d_env->getOptions().base.outputLanguage != olang) { getOptions().base.outputLanguage = olang; - *d_env->getOption(options::out) << language::SetLanguage(olang); + *d_env->getOptions().base.out << language::SetLanguage(olang); } } } @@ -575,7 +575,7 @@ void SmtEngine::debugCheckFunctionBody(Node formula, Node func) { TypeNode formulaType = - formula.getType(d_env->getOption(options::typeChecking)); + formula.getType(d_env->getOptions().expr.typeChecking); TypeNode funcType = func.getType(); // We distinguish here between definitions of constants and functions, // because the type checking for them is subtly different. Perhaps we @@ -741,7 +741,7 @@ Result SmtEngine::quickCheck() { Model* SmtEngine::getAvailableModel(const char* c) const { - if (!d_env->getOption(options::assignFunctionValues)) + if (!d_env->getOptions().theory.assignFunctionValues) { std::stringstream ss; ss << "Cannot " << c << " when --assign-function-values is false."; @@ -758,7 +758,7 @@ Model* SmtEngine::getAvailableModel(const char* c) const throw RecoverableModalException(ss.str().c_str()); } - if (!d_env->getOption(options::produceModels)) + if (!d_env->getOptions().smt.produceModels) { std::stringstream ss; ss << "Cannot " << c << " when produce-models options is off."; @@ -902,7 +902,7 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions, << "(" << assumptions << ") => " << r << endl; // Check that SAT results generate a model correctly. - if (d_env->getOption(options::checkModels)) + if (d_env->getOptions().smt.checkModels) { if (r.asSatisfiabilityResult().isSat() == Result::SAT) { @@ -910,14 +910,14 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions, } } // Check that UNSAT results generate a proof correctly. - if (d_env->getOption(options::checkProofs) - || d_env->getOption(options::proofEagerChecking)) + if (d_env->getOptions().smt.checkProofs + || d_env->getOptions().proof.proofEagerChecking) { if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) { - if ((d_env->getOption(options::checkProofs) - || d_env->getOption(options::proofEagerChecking)) - && !d_env->getOption(options::produceProofs)) + if ((d_env->getOptions().smt.checkProofs + || d_env->getOptions().proof.proofEagerChecking) + && !d_env->getOptions().smt.produceProofs) { throw ModalException( "Cannot check-proofs because proofs were disabled."); @@ -926,7 +926,7 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions, } } // Check that UNSAT results generate an unsat core correctly. - if (d_env->getOption(options::checkUnsatCores)) + if (d_env->getOptions().smt.checkUnsatCores) { if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) { @@ -955,7 +955,7 @@ std::vector<Node> SmtEngine::getUnsatAssumptions(void) { Trace("smt") << "SMT getUnsatAssumptions()" << endl; SmtScope smts(this); - if (!d_env->getOption(options::unsatAssumptions)) + if (!d_env->getOptions().smt.unsatAssumptions) { throw ModalException( "Cannot get unsat assumptions when produce-unsat-assumptions option " @@ -1166,7 +1166,7 @@ Node SmtEngine::getValue(const Node& ex) const Assert(m->hasApproximations() || resultNode.getKind() == kind::LAMBDA || resultNode.isConst()); - if (d_env->getOption(options::abstractValues) + if (d_env->getOptions().smt.abstractValues && resultNode.getType().isArray()) { resultNode = d_absValues->mkAbstractValue(resultNode); @@ -1207,7 +1207,7 @@ Model* SmtEngine::getModel() { Assert(te != nullptr); te->setEagerModelBuilding(); - if (d_env->getOption(options::modelCoresMode) + if (d_env->getOptions().smt.modelCoresMode != options::ModelCoresMode::NONE) { // If we enabled model cores, we compute a model core for m based on our @@ -1215,7 +1215,7 @@ Model* SmtEngine::getModel() { std::vector<Node> eassertsProc = getExpandedAssertions(); ModelCoreBuilder::setModelCore(eassertsProc, m->getTheoryModel(), - d_env->getOption(options::modelCoresMode)); + d_env->getOptions().smt.modelCoresMode); } // set the information on the SMT-level model Assert(m != nullptr); @@ -1238,7 +1238,7 @@ Result SmtEngine::blockModel() Model* m = getAvailableModel("block model"); - if (d_env->getOption(options::blockModelsMode) + if (d_env->getOptions().smt.blockModelsMode == options::BlockModelsMode::NONE) { std::stringstream ss; @@ -1251,7 +1251,7 @@ Result SmtEngine::blockModel() Node eblocker = ModelBlocker::getModelBlocker(eassertsProc, m->getTheoryModel(), - d_env->getOption(options::blockModelsMode)); + d_env->getOptions().smt.blockModelsMode); Trace("smt") << "Block formula: " << eblocker << std::endl; return assertFormula(eblocker); } @@ -1349,17 +1349,17 @@ Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; } void SmtEngine::checkProof() { - Assert(d_env->getOption(options::produceProofs)); + Assert(d_env->getOptions().smt.produceProofs); // internal check the proof PropEngine* pe = getPropEngine(); Assert(pe != nullptr); - if (d_env->getOption(options::proofEagerChecking)) + if (d_env->getOptions().proof.proofEagerChecking) { pe->checkProof(d_asserts->getAssertionList()); } Assert(pe->getProof() != nullptr); std::shared_ptr<ProofNode> pePfn = pe->getProof(); - if (d_env->getOption(options::checkProofs)) + if (d_env->getOptions().smt.checkProofs) { d_pfManager->checkProof(pePfn, *d_asserts); } @@ -1372,7 +1372,7 @@ StatisticsRegistry& SmtEngine::getStatisticsRegistry() UnsatCore SmtEngine::getUnsatCoreInternal() { - if (!d_env->getOption(options::unsatCores)) + if (!d_env->getOptions().smt.unsatCores) { throw ModalException( "Cannot get an unsat core when produce-unsat-cores or produce-proofs " @@ -1405,7 +1405,7 @@ UnsatCore SmtEngine::getUnsatCoreInternal() } void SmtEngine::checkUnsatCore() { - Assert(d_env->getOption(options::unsatCores)) + Assert(d_env->getOptions().smt.unsatCores) << "cannot check unsat core if unsat cores are turned off"; Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl; @@ -1514,7 +1514,7 @@ std::string SmtEngine::getProof() { getPrinter().toStreamCmdGetProof(getOutputManager().getDumpOut()); } - if (!d_env->getOption(options::produceProofs)) + if (!d_env->getOptions().smt.produceProofs) { throw ModalException("Cannot get a proof when proof option is off."); } @@ -1537,7 +1537,7 @@ std::string SmtEngine::getProof() void SmtEngine::printInstantiations( std::ostream& out ) { SmtScope smts(this); finishInit(); - if (d_env->getOption(options::instFormatMode) == options::InstFormatMode::SZS) + if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS) { out << "% SZS output start Proof for " << d_state->getFilename() << std::endl; @@ -1546,9 +1546,9 @@ void SmtEngine::printInstantiations( std::ostream& out ) { // First, extract and print the skolemizations bool printed = false; - bool reqNames = !d_env->getOption(options::printInstFull); + bool reqNames = !d_env->getOptions().printer.printInstFull; // only print when in list mode - if (d_env->getOption(options::printInstMode) == options::PrintInstMode::LIST) + if (d_env->getOptions().printer.printInstMode == options::PrintInstMode::LIST) { std::map<Node, std::vector<Node>> sks; qe->getSkolemTermVectors(sks); @@ -1583,14 +1583,14 @@ void SmtEngine::printInstantiations( std::ostream& out ) { continue; } // must have a name - if (d_env->getOption(options::printInstMode) == options::PrintInstMode::NUM) + if (d_env->getOptions().printer.printInstMode == options::PrintInstMode::NUM) { out << "(num-instantiations " << name << " " << i.second.size() << ")" << std::endl; } else { - Assert(d_env->getOption(options::printInstMode) + Assert(d_env->getOptions().printer.printInstMode == options::PrintInstMode::LIST); InstantiationList ilist(name, i.second); out << ilist; @@ -1602,7 +1602,7 @@ void SmtEngine::printInstantiations( std::ostream& out ) { { out << "No instantiations" << std::endl; } - if (d_env->getOption(options::instFormatMode) == options::InstFormatMode::SZS) + if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS) { out << "% SZS output end Proof for " << d_state->getFilename() << std::endl; } @@ -1613,9 +1613,9 @@ void SmtEngine::getInstantiationTermVectors( { SmtScope smts(this); finishInit(); - if (d_env->getOption(options::produceProofs) - && (!d_env->getOption(options::unsatCores) - || d_env->getOption(options::unsatCoresMode) == options::UnsatCoresMode::FULL_PROOF) + if (d_env->getOptions().smt.produceProofs + && (!d_env->getOptions().smt.unsatCores + || d_env->getOptions().smt.unsatCoresMode == options::UnsatCoresMode::FULL_PROOF) && getSmtMode() == SmtMode::UNSAT) { // minimize instantiations based on proof manager @@ -1716,7 +1716,7 @@ std::vector<Node> SmtEngine::getAssertions() getPrinter().toStreamCmdGetAssertions(getOutputManager().getDumpOut()); } Trace("smt") << "SMT getAssertions()" << endl; - if (!d_env->getOption(options::produceAssertions)) + if (!d_env->getOptions().smt.produceAssertions) { const char* msg = "Cannot query the current assertion list when not in produce-assertions mode."; diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 7f97c4122..1bb558d1b 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -27,6 +27,7 @@ #include "theory/ext_theory.h" #include "theory/rewriter.h" #include "theory/theory_model.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp index 6c4e0f96b..ed4f81cb3 100644 --- a/src/theory/booleans/proof_circuit_propagator.cpp +++ b/src/theory/booleans/proof_circuit_propagator.cpp @@ -169,11 +169,11 @@ std::shared_ptr<ProofNode> ProofCircuitPropagator::neqXFromY(bool y, { return nullptr; } - return mkResolution( + return mkNot(mkResolution( mkProof(y ? PfRule::NOT_EQUIV_ELIM2 : PfRule::NOT_EQUIV_ELIM1, {assume(parent.notNode())}), parent[1], - !y); + !y)); } std::shared_ptr<ProofNode> ProofCircuitPropagator::neqYFromX(bool x, @@ -183,11 +183,11 @@ std::shared_ptr<ProofNode> ProofCircuitPropagator::neqYFromX(bool x, { return nullptr; } - return mkResolution( + return mkNot(mkResolution( mkProof(x ? PfRule::NOT_EQUIV_ELIM2 : PfRule::NOT_EQUIV_ELIM1, {assume(parent.notNode())}), parent[0], - !x); + !x)); } std::shared_ptr<ProofNode> ProofCircuitPropagator::xorXFromY(bool negated, diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 582d67b31..6069745e0 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -76,7 +76,7 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker, Node query) { Assert (!query.isNull()); - if (Options::current().wasSetByUser(options::sygusExprMinerCheckTimeout)) + if (Options::current().quantifiers.sygusExprMinerCheckTimeout__setByUser) { initializeSubsolver(checker, true, options::sygusExprMinerCheckTimeout()); } diff --git a/src/theory/quantifiers/solution_filter.cpp b/src/theory/quantifiers/solution_filter.cpp index 5a4c2d142..ccc0763b7 100644 --- a/src/theory/quantifiers/solution_filter.cpp +++ b/src/theory/quantifiers/solution_filter.cpp @@ -16,6 +16,8 @@ #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" @@ -90,7 +92,7 @@ bool SolutionFilterStrength::addTerm(Node n, std::ostream& out) 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; } diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index e4ec40325..62c61fe1e 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -444,7 +444,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) 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; } } @@ -529,7 +529,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) 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++) @@ -995,7 +995,7 @@ void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums, // 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); } diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index 36602d3ae..48dce7cf3 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -828,7 +828,7 @@ void SygusSampler::checkEquivalent(Node bv, Node bvr) } // 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; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 40f5b901f..4f20fae22 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -15,6 +15,7 @@ #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" @@ -461,7 +462,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ 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); } } diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 8b5e35023..fc8fb15b0 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -547,7 +547,9 @@ void ExtfSolver::checkExtfInference(Node n, if (d_state.areEqual(conc, d_false)) { // we are in conflict - d_im.sendInference(in.d_exp, conc, InferenceId::STRINGS_CTN_DECOMPOSE); + d_im.addToExplanation(conc, d_false, in.d_exp); + d_im.sendInference( + in.d_exp, d_false, InferenceId::STRINGS_CTN_DECOMPOSE); Assert(d_state.isInConflict()); return; } diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index de9a32248..f0cc78789 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -164,7 +164,7 @@ ResourceManager::ResourceManager(StatisticsRegistry& stats, d_infidWeights.fill(1); d_resourceWeights.fill(1); - for (const auto& opt : d_options[options::resourceWeightHolder]) + for (const auto& opt : d_options.resman.resourceWeightHolder) { std::string name; uint64_t weight; @@ -189,9 +189,9 @@ uint64_t ResourceManager::getTimeUsage() const { return d_cumulativeTimeUsed; } uint64_t ResourceManager::getResourceRemaining() const { - if (d_options[options::cumulativeResourceLimit] <= d_cumulativeResourceUsed) + if (d_options.resman.cumulativeResourceLimit <= d_cumulativeResourceUsed) return 0; - return d_options[options::cumulativeResourceLimit] - d_cumulativeResourceUsed; + return d_options.resman.cumulativeResourceLimit - d_cumulativeResourceUsed; } void ResourceManager::spendResource(uint64_t amount) @@ -237,21 +237,21 @@ void ResourceManager::spendResource(theory::InferenceId iid) void ResourceManager::beginCall() { - d_perCallTimer.set(d_options[options::perCallMillisecondLimit]); + d_perCallTimer.set(d_options.resman.perCallMillisecondLimit); d_thisCallResourceUsed = 0; - if (d_options[options::cumulativeResourceLimit] > 0) + if (d_options.resman.cumulativeResourceLimit > 0) { // Compute remaining cumulative resource budget d_thisCallResourceBudget = - d_options[options::cumulativeResourceLimit] - d_cumulativeResourceUsed; + d_options.resman.cumulativeResourceLimit - d_cumulativeResourceUsed; } - if (d_options[options::perCallResourceLimit] > 0) + if (d_options.resman.perCallResourceLimit > 0) { // Check if per-call resource budget is even smaller - if (d_options[options::perCallResourceLimit] < d_thisCallResourceBudget) + if (d_options.resman.perCallResourceLimit < d_thisCallResourceBudget) { - d_thisCallResourceBudget = d_options[options::perCallResourceLimit]; + d_thisCallResourceBudget = d_options.resman.perCallResourceLimit; } } } @@ -265,25 +265,25 @@ void ResourceManager::endCall() bool ResourceManager::limitOn() const { - return (d_options[options::cumulativeResourceLimit] > 0) - || (d_options[options::perCallMillisecondLimit] > 0) - || (d_options[options::perCallResourceLimit] > 0); + return (d_options.resman.cumulativeResourceLimit > 0) + || (d_options.resman.perCallMillisecondLimit > 0) + || (d_options.resman.perCallResourceLimit > 0); } bool ResourceManager::outOfResources() const { - if (d_options[options::perCallResourceLimit] > 0) + if (d_options.resman.perCallResourceLimit > 0) { // Check if per-call resources are exhausted - if (d_thisCallResourceUsed >= d_options[options::perCallResourceLimit]) + if (d_thisCallResourceUsed >= d_options.resman.perCallResourceLimit) { return true; } } - if (d_options[options::cumulativeResourceLimit] > 0) + if (d_options.resman.cumulativeResourceLimit > 0) { // Check if cumulative resources are exhausted - if (d_cumulativeResourceUsed >= d_options[options::cumulativeResourceLimit]) + if (d_cumulativeResourceUsed >= d_options.resman.cumulativeResourceLimit) { return true; } @@ -293,7 +293,7 @@ bool ResourceManager::outOfResources() const bool ResourceManager::outOfTime() const { - if (d_options[options::perCallMillisecondLimit] == 0) return false; + if (d_options.resman.perCallMillisecondLimit == 0) return false; return d_perCallTimer.expired(); } |