From a6cdf2b085aaa9789f47757329a7803053ceb36a Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 31 Aug 2021 18:17:24 -0700 Subject: No longer use direct access to options in driver (#7094) This PR refactors the driver to no longer directly access the Options object, but instead use Solver::getOption() or Solver::getOptionInfo(). --- src/api/cpp/cvc5.cpp | 6 ------ src/api/cpp/cvc5.h | 4 ---- src/base/exception.cpp | 3 +++ src/base/exception.h | 2 +- src/main/command_executor.cpp | 34 ++++++++++++++-------------------- src/main/command_executor.h | 2 -- src/main/driver_unified.cpp | 42 +++++++++++++++++------------------------- src/main/interactive_shell.cpp | 7 +------ src/main/main.cpp | 5 +++-- src/main/time_limit.cpp | 4 +--- src/main/time_limit.h | 2 +- src/options/base_options.toml | 1 + src/parser/parser.cpp | 4 +--- src/parser/parser_builder.cpp | 20 +++++++++----------- src/parser/parser_builder.h | 4 ++-- src/parser/smt2/smt2.cpp | 8 -------- src/parser/smt2/smt2.h | 2 -- 17 files changed, 54 insertions(+), 96 deletions(-) (limited to 'src') diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 6171c147b..d03b8975e 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -7906,12 +7906,6 @@ std::vector Solver::getSynthSolutions( */ SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); } -/* - * !!! This is only temporarily available until the parser is fully migrated to - * the new API. !!! - */ -Options& Solver::getOptions(void) { return d_smtEngine->getOptions(); } - Statistics Solver::getStatistics() const { return Statistics(d_smtEngine->getStatisticsRegistry()); diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 5abcc578e..11b138a50 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -4333,10 +4333,6 @@ class CVC5_EXPORT Solver // to the new API. !!! SmtEngine* getSmtEngine(void) const; - // !!! This is only temporarily available until options are refactored at - // the driver level. !!! - Options& getOptions(void); - /** * Returns a snapshot of the current state of the statistic values of this * solver. The returned object is completely decoupled from the solver and diff --git a/src/base/exception.cpp b/src/base/exception.cpp index b337f819a..da8a56254 100644 --- a/src/base/exception.cpp +++ b/src/base/exception.cpp @@ -19,6 +19,7 @@ #include #include #include +#include #include #include @@ -35,6 +36,8 @@ std::string Exception::toString() const return ss.str(); } +void Exception::toStream(std::ostream& os) const { os << d_msg; } + thread_local LastExceptionBuffer* LastExceptionBuffer::s_currentBuffer = nullptr; LastExceptionBuffer::LastExceptionBuffer() : d_contents(nullptr) {} diff --git a/src/base/exception.h b/src/base/exception.h index 0f053e415..e37b69ec8 100644 --- a/src/base/exception.h +++ b/src/base/exception.h @@ -66,7 +66,7 @@ class CVC5_EXPORT Exception : public std::exception * a derived class, it's recommended that this method print the * type of exception before the actual message. */ - virtual void toStream(std::ostream& os) const { os << d_msg; } + virtual void toStream(std::ostream& os) const; }; /* class Exception */ diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 6501a1b0f..98e93ca5a 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -26,8 +26,6 @@ #include #include "main/main.h" -#include "options/base_options.h" -#include "options/main_options.h" #include "smt/command.h" #include "smt/smt_engine.h" @@ -60,22 +58,18 @@ CommandExecutor::~CommandExecutor() { } -Options& CommandExecutor::getOptions() -{ - return d_solver->d_smtEngine->getOptions(); -} void CommandExecutor::storeOptionsAsOriginal() { - d_solver->d_originalOptions->copyValues(getOptions()); + d_solver->d_originalOptions->copyValues(d_solver->d_smtEngine->getOptions()); } void CommandExecutor::printStatistics(std::ostream& out) const { - const auto& baseopts = d_solver->getOptions().base; - if (baseopts.statistics) + if (d_solver->getOptionInfo("stats").boolValue()) { const auto& stats = d_solver->getStatistics(); - auto it = stats.begin(baseopts.statisticsExpert, baseopts.statisticsAll); + auto it = stats.begin(d_solver->getOptionInfo("stats-expert").boolValue(), + d_solver->getOptionInfo("stats-all").boolValue()); for (; it != stats.end(); ++it) { out << it->first << " = " << it->second << std::endl; @@ -85,7 +79,7 @@ void CommandExecutor::printStatistics(std::ostream& out) const void CommandExecutor::printStatisticsSafe(int fd) const { - if (d_solver->getOptions().base.statistics) + if (d_solver->getOptionInfo("stats").boolValue()) { d_solver->printStatisticsSafe(fd); } @@ -93,7 +87,7 @@ void CommandExecutor::printStatisticsSafe(int fd) const bool CommandExecutor::doCommand(Command* cmd) { - if (d_solver->getOptions().base.parseOnly) + if (d_solver->getOptionInfo("parse-only").boolValue()) { return true; } @@ -112,7 +106,7 @@ bool CommandExecutor::doCommand(Command* cmd) return status; } else { - if (d_solver->getOptions().base.verbosity > 2) + if (d_solver->getOptionInfo("verbosity").intValue() > 2) { d_solver->getDriverOptions().out() << "Invoking: " << *cmd << std::endl; } @@ -154,27 +148,27 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) // dump the model/proof/unsat core if option is set if (status) { std::vector > getterCommands; - if (d_solver->getOptions().driver.dumpModels + if (d_solver->getOptionInfo("dump-models").boolValue() && (isResultSat || (res.isSatUnknown() && res.getUnknownExplanation() == api::Result::INCOMPLETE))) { getterCommands.emplace_back(new GetModelCommand()); } - if (d_solver->getOptions().driver.dumpProofs && isResultUnsat) + if (d_solver->getOptionInfo("dump-proofs").boolValue() && isResultUnsat) { getterCommands.emplace_back(new GetProofCommand()); } - if ((d_solver->getOptions().driver.dumpInstantiations - || d_solver->getOptions().driver.dumpInstantiationsDebug) + if ((d_solver->getOptionInfo("dump-instantiations").boolValue() + || d_solver->getOptionInfo("dump-instantiations-debug").boolValue()) && GetInstantiationsCommand::isEnabled(d_solver.get(), res)) { getterCommands.emplace_back(new GetInstantiationsCommand()); } - if ((d_solver->getOptions().driver.dumpUnsatCores - || d_solver->getOptions().driver.dumpUnsatCoresFull) + if ((d_solver->getOptionInfo("dump-unsat-cores").boolValue() + || d_solver->getOptionInfo("dump-unsat-cores-full").boolValue()) && isResultUnsat) { getterCommands.emplace_back(new GetUnsatCoreCommand()); @@ -182,7 +176,7 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) if (!getterCommands.empty()) { // set no time limit during dumping if applicable - if (d_solver->getOptions().driver.forceNoLimitCpuWhileDump) + if (d_solver->getOptionInfo("force-no-limit-cpu-while-dump").boolValue()) { setNoLimitCPU(); } diff --git a/src/main/command_executor.h b/src/main/command_executor.h index d44986640..0a7a56e5b 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -83,8 +83,6 @@ class CommandExecutor SmtEngine* getSmtEngine() const { return d_solver->getSmtEngine(); } - /** Get the current options from the solver */ - Options& getOptions(); /** Store the current options as the original options */ void storeOptionsAsOriginal(); diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 2c6413503..25726f458 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -34,13 +34,6 @@ #include "main/options.h" #include "main/signal_handlers.h" #include "main/time_limit.h" -#include "options/base_options.h" -#include "options/main_options.h" -#include "options/option_exception.h" -#include "options/options.h" -#include "options/options_public.h" -#include "options/parser_options.h" -#include "options/set_language.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "smt/command.h" @@ -112,30 +105,29 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) // Create the command executor to execute the parsed commands pExecutor = std::make_unique(solver); api::DriverOptions dopts = solver->getDriverOptions(); - Options* opts = &pExecutor->getOptions(); // Parse the options std::vector filenames = main::parse(*solver, argc, argv, progName); - auto limit = install_time_limit(*opts); + auto limit = install_time_limit(solver->getOptionInfo("tlimit").uintValue()); - if (opts->driver.help) + if (solver->getOptionInfo("help").boolValue()) { printUsage(dopts, true); exit(1); } - else if (opts->base.languageHelp) + else if (solver->getOptionInfo("language-help").boolValue()) { main::printLanguageHelp(dopts.out()); exit(1); } - else if (opts->driver.version) + else if (solver->getOptionInfo("version").boolValue()) { dopts.out() << Configuration::about().c_str() << flush; exit(0); } - segvSpin = opts->driver.segvSpin; + segvSpin = solver->getOptionInfo("segv-spin").boolValue(); // If in competition mode, set output stream option to flush immediately #ifdef CVC5_COMPETITION_MODE @@ -151,9 +143,9 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) const bool inputFromStdin = filenames.empty() || filenames[0] == "-"; // if we're reading from stdin on a TTY, default to interactive mode - if (!opts->driver.interactiveWasSetByUser) + if (!solver->getOptionInfo("interactive").setByUser) { - opts->driver.interactive = inputFromStdin && isatty(fileno(stdin)); + solver->setOption("interactive", (inputFromStdin && isatty(fileno(stdin))) ? "true" : "false"); } // Auto-detect input language by filename extension @@ -210,9 +202,9 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) // Parse and execute commands until we are done std::unique_ptr cmd; bool status = true; - if (opts->driver.interactive && inputFromStdin) + if (solver->getOptionInfo("interactive").boolValue() && inputFromStdin) { - if (!opts->base.incrementalSolvingWasSetByUser) + if (!solver->getOptionInfo("incremental").setByUser) { cmd.reset(new SetOptionCommand("incremental", "true")); cmd->setMuted(true); @@ -244,7 +236,6 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) if (cmd == nullptr) break; status = pExecutor->doCommand(cmd) && status; - opts = &pExecutor->getOptions(); if (cmd->interrupted()) { break; } @@ -252,7 +243,7 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) } else { - if (!opts->base.incrementalSolvingWasSetByUser) + if (!solver->getOptionInfo("incremental").setByUser) { cmd.reset(new SetOptionCommand("incremental", "false")); cmd->setMuted(true); @@ -271,7 +262,7 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) parser->setInput( Input::newFileInput(solver->getOption("input-language"), filename, - solver->getOption("mmap") == "true")); + solver->getOptionInfo("mmap").boolValue())); } bool interrupted = false; @@ -280,7 +271,6 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) if (interrupted) { dopts.out() << CommandInterrupted(); pExecutor->reset(); - opts = &pExecutor->getOptions(); break; } try { @@ -292,7 +282,6 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) } status = pExecutor->doCommand(cmd); - opts = &pExecutor->getOptions(); if (cmd->interrupted() && status == 0) { interrupted = true; break; @@ -325,12 +314,15 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) pExecutor->flushOutputStreams(); #ifdef CVC5_DEBUG - if (opts->driver.earlyExit && opts->driver.earlyExitWasSetByUser) { - _exit(returnValue); + auto info = solver->getOptionInfo("early-exit"); + if (info.boolValue() && info.setByUser) + { + _exit(returnValue); + } } #else /* CVC5_DEBUG */ - if (opts->driver.earlyExit) + if (solver->getOptionInfo("early-exit").boolValue()) { _exit(returnValue); } diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index a47b8abb7..ea408012a 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -42,11 +42,6 @@ #include "base/check.h" #include "base/output.h" #include "expr/symbol_manager.h" -#include "options/base_options.h" -#include "options/language.h" -#include "options/main_options.h" -#include "options/options.h" -#include "options/parser_options.h" #include "parser/input.h" #include "parser/parser.h" #include "parser/parser_builder.h" @@ -99,7 +94,7 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm) ParserBuilder parserBuilder(solver, sm, true); /* Create parser with bogus input. */ d_parser = parserBuilder.build(); - if (d_solver->getOptions().parser.forceLogicStringWasSetByUser) + if (d_solver->getOptionInfo("force-logic").setByUser) { LogicInfo tmp(d_solver->getOption("force-logic")); d_parser->forceLogic(tmp.getLogicString()); diff --git a/src/main/main.cpp b/src/main/main.cpp index d17bcaab1..18be1b406 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -79,7 +79,7 @@ int main(int argc, char* argv[]) #ifdef CVC5_COMPETITION_MODE solver->getDriverOptions().out() << "unknown" << std::endl; #endif - if (language::isLangSmt2(solver->getOptions().base.outputLanguage)) + if (solver->getOption("output-language") == "LANG_SMTLIB_V2_6") { solver->getDriverOptions().out() << "(error \"" << e << "\")" << std::endl; @@ -89,7 +89,8 @@ int main(int argc, char* argv[]) solver->getDriverOptions().err() << "(error \"" << e << "\")" << std::endl; } - if (solver->getOptions().base.statistics && pExecutor != nullptr) + if (solver->getOptionInfo("stats").boolValue() + && main::pExecutor != nullptr) { totalTime.reset(); pExecutor->printStatistics(solver->getDriverOptions().err()); diff --git a/src/main/time_limit.cpp b/src/main/time_limit.cpp index 28a0087bb..698d08c6d 100644 --- a/src/main/time_limit.cpp +++ b/src/main/time_limit.cpp @@ -56,7 +56,6 @@ #include #include "base/exception.h" -#include "options/base_options.h" #include "signal_handlers.h" namespace cvc5 { @@ -78,9 +77,8 @@ TimeLimit::~TimeLimit() } #endif -TimeLimit install_time_limit(const Options& opts) +TimeLimit install_time_limit(uint64_t ms) { - uint64_t ms = opts.base.cumulativeMillisecondLimit; // Skip if no time limit shall be set. if (ms == 0) { return TimeLimit(); diff --git a/src/main/time_limit.h b/src/main/time_limit.h index c84e22b4b..de0a28a26 100644 --- a/src/main/time_limit.h +++ b/src/main/time_limit.h @@ -43,7 +43,7 @@ struct TimeLimit * thread needs to communicate back to the timer thread when it wants to * terminate, which is done via the TimeLimit object. */ -TimeLimit install_time_limit(const Options& opts); +TimeLimit install_time_limit(uint64_t ms); } // namespace main } // namespace cvc5 diff --git a/src/options/base_options.toml b/src/options/base_options.toml index 439a1beba..adc2d8456 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -55,6 +55,7 @@ public = true [[option]] name = "languageHelp" + long = "language-help" category = "undocumented" type = "bool" diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index bd0f56b2d..39b38be30 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -26,8 +26,6 @@ #include "base/check.h" #include "base/output.h" #include "expr/kind.h" -#include "options/base_options.h" -#include "options/options.h" #include "parser/input.h" #include "parser/parser_exception.h" #include "smt/command.h" @@ -899,7 +897,7 @@ std::wstring Parser::processAdHocStringEsc(const std::string& s) api::Term Parser::mkStringConstant(const std::string& s) { - if (language::isLangSmt2(d_solver->getOptions().base.inputLanguage)) + if (d_solver->getOption("input-language") == "LANG_SMTLIB_V2_6") { return d_solver->mkString(s, true); } diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 665836402..b1bb9a432 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -21,9 +21,6 @@ #include "api/cpp/cvc5.h" #include "base/check.h" #include "cvc/cvc.h" -#include "options/base_options.h" -#include "options/options.h" -#include "options/parser_options.h" #include "parser/antlr_input.h" #include "parser/input.h" #include "parser/parser.h" @@ -41,7 +38,7 @@ ParserBuilder::ParserBuilder(api::Solver* solver, init(solver, sm); if (useOptions) { - withOptions(solver->getOptions()); + withOptions(); } } @@ -109,17 +106,18 @@ ParserBuilder& ParserBuilder::withParseOnly(bool flag) { return *this; } -ParserBuilder& ParserBuilder::withOptions(const Options& opts) +ParserBuilder& ParserBuilder::withOptions() { ParserBuilder& retval = *this; retval = retval.withInputLanguage(d_solver->getOption("input-language")) - .withChecks(opts.parser.semanticChecks) - .withStrictMode(opts.parser.strictParsing) - .withParseOnly(opts.base.parseOnly) - .withIncludeFile(opts.parser.filesystemAccess); - if (opts.parser.forceLogicStringWasSetByUser) + .withChecks(d_solver->getOptionInfo("semantic-checks").boolValue()) + .withStrictMode(d_solver->getOptionInfo("strict-parsing").boolValue()) + .withParseOnly(d_solver->getOptionInfo("parse-only").boolValue()) + .withIncludeFile(d_solver->getOptionInfo("filesystem-access").boolValue()); + auto info = d_solver->getOptionInfo("force-logic"); + if (info.setByUser) { - LogicInfo tmp(opts.parser.forceLogicString); + LogicInfo tmp(info.stringValue()); retval = retval.withForcedLogic(tmp.getLogicString()); } return retval; diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 23a9daae2..d148a538d 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -104,8 +104,8 @@ class CVC5_EXPORT ParserBuilder */ ParserBuilder& withParseOnly(bool flag = true); - /** Derive settings from the given options. */ - ParserBuilder& withOptions(const Options& opts); + /** Derive settings from the solver's options. */ + ParserBuilder& withOptions(); /** * Should the parser use strict mode? diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 1a0a3d52a..2fd4a5596 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -17,9 +17,6 @@ #include #include "base/check.h" -#include "options/base_options.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" @@ -843,11 +840,6 @@ api::Term Smt2::mkAbstractValue(const std::string& name) return d_solver->mkAbstractValue(name.substr(1)); } -Language Smt2::getLanguage() const -{ - return d_solver->getOptions().base.inputLanguage; -} - void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type) { Debug("parser") << "parseOpApplyTypeAscription : " << p << " " << type diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index c3f93708d..97eb95c00 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -413,8 +413,6 @@ class Smt2 : public Parser void addSepOperators(); - Language getLanguage() const; - /** * Utility function to create a conjunction of expressions. * -- cgit v1.2.3