From d3df62e637057c77bab90ae644437fe250a64d37 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 20 Aug 2021 14:47:04 -0700 Subject: [PATCH] Make driver use options from the solver (#6930) This PR removes explicit ownership of the options object from the main function and replaces it by an api::Solver object. To achieve this, it does a number of minor changes: - api::Solver not takes a unique_ptr in its constructor - CommandExecutor only holds a reference to (a unique ptr of) the api::Solver - the main functions accesses options via the solver --- src/api/cpp/cvc5.cpp | 10 ++--- src/api/cpp/cvc5.h | 10 ++++- src/api/python/cvc5.pxd | 2 +- src/api/python/cvc5.pxi | 2 +- src/main/command_executor.cpp | 17 +++++--- src/main/command_executor.h | 9 +++- src/main/driver_unified.cpp | 82 +++++++++++++++++++---------------- src/main/main.cpp | 22 +++++----- src/main/main.h | 3 +- src/smt/command.cpp | 2 +- 10 files changed, 92 insertions(+), 67 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 82064b758..f5e2c8f0c 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -4951,20 +4951,18 @@ std::ostream& operator<<(std::ostream& out, const Statistics& stats) /* Solver */ /* -------------------------------------------------------------------------- */ -Solver::Solver(const Options* opts) +Solver::Solver(std::unique_ptr&& original) { d_nodeMgr.reset(new NodeManager()); - d_originalOptions.reset(new Options()); - if (opts != nullptr) - { - d_originalOptions->copyValues(*opts); - } + d_originalOptions = std::move(original); d_smtEngine.reset(new SmtEngine(d_nodeMgr.get(), d_originalOptions.get())); d_smtEngine->setSolver(this); d_rng.reset(new Random(d_smtEngine->getOptions().driver.seed)); resetStatistics(); } +Solver::Solver() : Solver(std::make_unique()) {} + Solver::~Solver() {} /* Helpers and private functions */ diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 62ee9ac32..3226dd4fd 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -2781,6 +2781,13 @@ class CVC5_EXPORT Solver friend class Sort; friend class Term; + private: + /* + * Constructs a solver with the given original options. This should only be + * used internally when the Solver is reset. + */ + Solver(std::unique_ptr&& original); + public: /* .................................................................... */ /* Constructors/Destructors */ @@ -2788,10 +2795,9 @@ class CVC5_EXPORT Solver /** * Constructor. - * @param opts an optional pointer to a solver options object * @return the Solver */ - Solver(const Options* opts = nullptr); + Solver(); /** * Destructor. diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 99e471b0a..ee73187ff 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -155,7 +155,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": cdef cppclass Solver: - Solver(Options*) except + + Solver() except + Sort getBooleanSort() except + Sort getIntegerSort() except + Sort getNullSort() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index d31fdc126..210eb0639 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -487,7 +487,7 @@ cdef class Solver: cdef c_Solver* csolver def __cinit__(self): - self.csolver = new c_Solver(NULL) + self.csolver = new c_Solver() def __dealloc__(self): del self.csolver diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 4e25e984d..f60ed925b 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -29,6 +29,7 @@ #include "options/base_options.h" #include "options/main_options.h" #include "smt/command.h" +#include "smt/smt_engine.h" namespace cvc5 { namespace main { @@ -49,17 +50,23 @@ void setNoLimitCPU() { #endif /* ! __WIN32__ */ } -CommandExecutor::CommandExecutor(const Options& options) - : d_solver(new api::Solver(&options)), +CommandExecutor::CommandExecutor(std::unique_ptr& solver) + : d_solver(solver), d_symman(new SymbolManager(d_solver.get())), d_result() { } CommandExecutor::~CommandExecutor() { - // ensure that symbol manager is destroyed before solver - d_symman.reset(nullptr); - d_solver.reset(nullptr); +} + +Options& CommandExecutor::getOptions() +{ + return d_solver->d_smtEngine->getOptions(); +} +void CommandExecutor::storeOptionsAsOriginal() +{ + d_solver->d_originalOptions->copyValues(getOptions()); } void CommandExecutor::printStatistics(std::ostream& out) const diff --git a/src/main/command_executor.h b/src/main/command_executor.h index ff7b89928..e8c2d25ac 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -40,7 +40,7 @@ class CommandExecutor * The solver object, which is allocated by this class and is used for * executing most commands (e.g. check-sat). */ - std::unique_ptr d_solver; + std::unique_ptr& d_solver; /** * The symbol manager, which is allocated by this class. This manages * all things related to definitions of symbols and their impact on behaviors @@ -56,7 +56,7 @@ class CommandExecutor api::Result d_result; public: - CommandExecutor(const Options& options); + CommandExecutor(std::unique_ptr& solver); virtual ~CommandExecutor(); @@ -83,6 +83,11 @@ 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(); + /** * Prints statistics to an output stream. * Checks whether statistics should be printed according to the options. diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 0f1130234..93d458c32 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -95,7 +95,7 @@ void printUsage(const Options& opts, bool full) { } } -int runCvc5(int argc, char* argv[], Options& opts) +int runCvc5(int argc, char* argv[], std::unique_ptr& solver) { main::totalTime = std::make_unique(); @@ -104,32 +104,36 @@ int runCvc5(int argc, char* argv[], Options& opts) progPath = argv[0]; + // Create the command executor to execute the parsed commands + pExecutor = std::make_unique(solver); + Options* opts = &pExecutor->getOptions(); + // Parse the options - std::vector filenames = options::parse(opts, argc, argv, progName); + std::vector filenames = options::parse(*opts, argc, argv, progName); - auto limit = install_time_limit(opts); + auto limit = install_time_limit(*opts); - if (opts.driver.help) + if (opts->driver.help) { - printUsage(opts, true); + printUsage(*opts, true); exit(1); } - else if (opts.base.languageHelp) + else if (opts->base.languageHelp) { - options::printLanguageHelp(*opts.base.out); + options::printLanguageHelp(*opts->base.out); exit(1); } - else if (opts.driver.version) + else if (opts->driver.version) { - *opts.base.out << Configuration::about().c_str() << flush; + *opts->base.out << Configuration::about().c_str() << flush; exit(0); } - segvSpin = opts.driver.segvSpin; + segvSpin = opts->driver.segvSpin; // If in competition mode, set output stream option to flush immediately #ifdef CVC5_COMPETITION_MODE - *opts.base.out << unitbuf; + *opts->base.out << unitbuf; #endif /* CVC5_COMPETITION_MODE */ // We only accept one input file @@ -141,9 +145,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.driver.interactiveWasSetByUser) + if (!opts->driver.interactiveWasSetByUser) { - opts.driver.interactive = inputFromStdin && isatty(fileno(stdin)); + opts->driver.interactive = inputFromStdin && isatty(fileno(stdin)); } // Auto-detect input language by filename extension @@ -153,33 +157,34 @@ int runCvc5(int argc, char* argv[], Options& opts) } const char* filename = filenameStr.c_str(); - if (opts.base.inputLanguage == language::input::LANG_AUTO) + if (opts->base.inputLanguage == language::input::LANG_AUTO) { if( inputFromStdin ) { // We can't do any fancy detection on stdin - opts.base.inputLanguage = language::input::LANG_CVC; + opts->base.inputLanguage = language::input::LANG_CVC; } else { size_t len = filenameStr.size(); if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { - opts.base.inputLanguage = language::input::LANG_SMTLIB_V2_6; + opts->base.inputLanguage = language::input::LANG_SMTLIB_V2_6; } else if((len >= 2 && !strcmp(".p", filename + len - 2)) || (len >= 5 && !strcmp(".tptp", filename + len - 5))) { - opts.base.inputLanguage = language::input::LANG_TPTP; + opts->base.inputLanguage = language::input::LANG_TPTP; } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { - opts.base.inputLanguage = language::input::LANG_CVC; + opts->base.inputLanguage = language::input::LANG_CVC; } else if((len >= 3 && !strcmp(".sy", filename + len - 3)) || (len >= 3 && !strcmp(".sl", filename + len - 3))) { // version 2 sygus is the default - opts.base.inputLanguage = language::input::LANG_SYGUS_V2; + opts->base.inputLanguage = language::input::LANG_SYGUS_V2; } } } - if (opts.base.outputLanguage == language::output::LANG_AUTO) + if (opts->base.outputLanguage == language::output::LANG_AUTO) { - opts.base.outputLanguage = language::toOutputLanguage(opts.base.inputLanguage); + opts->base.outputLanguage = language::toOutputLanguage(opts->base.inputLanguage); } + pExecutor->storeOptionsAsOriginal(); // Determine which messages to show based on smtcomp_mode and verbosity if(Configuration::isMuzzledBuild()) { @@ -192,11 +197,9 @@ int runCvc5(int argc, char* argv[], Options& opts) } // important even for muzzled builds (to get result output right) - (*opts.base.out) - << language::SetLanguage(opts.base.outputLanguage); + (*opts->base.out) + << language::SetLanguage(opts->base.outputLanguage); - // Create the command executor to execute the parsed commands - pExecutor = std::make_unique(opts); int returnValue = 0; { @@ -206,9 +209,9 @@ int runCvc5(int argc, char* argv[], Options& opts) // Parse and execute commands until we are done std::unique_ptr cmd; bool status = true; - if (opts.driver.interactive && inputFromStdin) + if (opts->driver.interactive && inputFromStdin) { - if (!opts.base.incrementalSolvingWasSetByUser) + if (!opts->base.incrementalSolvingWasSetByUser) { cmd.reset(new SetOptionCommand("incremental", "true")); cmd->setMuted(true); @@ -234,12 +237,13 @@ int runCvc5(int argc, char* argv[], Options& opts) try { cmd.reset(shell.readCommand()); } catch(UnsafeInterruptException& e) { - *opts.base.out << CommandInterrupted(); + *opts->base.out << CommandInterrupted(); break; } if (cmd == nullptr) break; status = pExecutor->doCommand(cmd) && status; + opts = &pExecutor->getOptions(); if (cmd->interrupted()) { break; } @@ -247,7 +251,7 @@ int runCvc5(int argc, char* argv[], Options& opts) } else { - if (!opts.base.incrementalSolvingWasSetByUser) + if (!opts->base.incrementalSolvingWasSetByUser) { cmd.reset(new SetOptionCommand("incremental", "false")); cmd->setMuted(true); @@ -256,25 +260,26 @@ int runCvc5(int argc, char* argv[], Options& opts) ParserBuilder parserBuilder(pExecutor->getSolver(), pExecutor->getSymbolManager(), - opts); + *opts); std::unique_ptr parser(parserBuilder.build()); if( inputFromStdin ) { parser->setInput(Input::newStreamInput( - opts.base.inputLanguage, cin, filename)); + opts->base.inputLanguage, cin, filename)); } else { - parser->setInput(Input::newFileInput(opts.base.inputLanguage, + parser->setInput(Input::newFileInput(opts->base.inputLanguage, filename, - opts.parser.memoryMap)); + opts->parser.memoryMap)); } bool interrupted = false; while (status) { if (interrupted) { - *opts.base.out << CommandInterrupted(); + *opts->base.out << CommandInterrupted(); pExecutor->reset(); + opts = &pExecutor->getOptions(); break; } try { @@ -286,6 +291,7 @@ int runCvc5(int argc, char* argv[], Options& opts) } status = pExecutor->doCommand(cmd); + opts = &pExecutor->getOptions(); if (cmd->interrupted() && status == 0) { interrupted = true; break; @@ -307,9 +313,9 @@ int runCvc5(int argc, char* argv[], Options& opts) } #ifdef CVC5_COMPETITION_MODE - if (opts.base.out != nullptr) + if (opts->base.out != nullptr) { - *opts.base.out << std::flush; + *opts->base.out << std::flush; } // exit, don't return (don't want destructors to run) // _exit() from unistd.h doesn't run global destructors @@ -321,12 +327,12 @@ int runCvc5(int argc, char* argv[], Options& opts) pExecutor->flushOutputStreams(); #ifdef CVC5_DEBUG - if (opts.driver.earlyExit && opts.driver.earlyExitWasSetByUser) + if (opts->driver.earlyExit && opts->driver.earlyExitWasSetByUser) { _exit(returnValue); } #else /* CVC5_DEBUG */ - if (opts.driver.earlyExit) + if (opts->driver.earlyExit) { _exit(returnValue); } diff --git a/src/main/main.cpp b/src/main/main.cpp index 6173cfd69..12a2920b4 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -22,6 +22,7 @@ #include #include +#include "api/cpp/cvc5.h" #include "base/configuration.h" #include "base/output.h" #include "main/command_executor.h" @@ -49,10 +50,11 @@ using namespace cvc5::language; */ int main(int argc, char* argv[]) { - Options opts; + std::unique_ptr solver; try { - return runCvc5(argc, argv, opts); + solver = std::make_unique(); + return runCvc5(argc, argv, solver); } catch (cvc5::api::CVC5ApiOptionException& e) { @@ -63,10 +65,10 @@ int main(int argc, char* argv[]) << endl << "Please use --help to get help on command-line options." << endl; } - catch (cvc5::OptionException& e) + catch (OptionException& e) { #ifdef CVC5_COMPETITION_MODE - *opts.base.out << "unknown" << endl; + *solver->getOptions().base.out << "unknown" << endl; #endif cerr << "(error \"" << e.getMessage() << "\")" << endl << endl @@ -75,20 +77,20 @@ int main(int argc, char* argv[]) catch (Exception& e) { #ifdef CVC5_COMPETITION_MODE - *opts.base.out << "unknown" << endl; + *solver->getOptions().base.out << "unknown" << endl; #endif - if (language::isOutputLang_smt2(opts.base.outputLanguage)) + if (language::isOutputLang_smt2(solver->getOptions().base.outputLanguage)) { - *opts.base.out << "(error \"" << e << "\")" << endl; + *solver->getOptions().base.out << "(error \"" << e << "\")" << endl; } else { - *opts.base.err << "(error \"" << e << "\")" << endl; + *solver->getOptions().base.err << "(error \"" << e << "\")" << endl; } - if (opts.base.statistics && pExecutor != nullptr) + if (solver->getOptions().base.statistics && pExecutor != nullptr) { totalTime.reset(); - pExecutor->printStatistics(*opts.base.err); + pExecutor->printStatistics(*solver->getOptions().base.err); } } exit(1); diff --git a/src/main/main.h b/src/main/main.h index 636df405f..e76836600 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -18,6 +18,7 @@ #include #include +#include "api/cpp/cvc5.h" #include "base/cvc5config.h" #include "base/exception.h" #include "options/options.h" @@ -63,7 +64,7 @@ extern bool segvSpin; } // namespace cvc5 /** Actual cvc5 driver functions **/ -int runCvc5(int argc, char* argv[], cvc5::Options&); +int runCvc5(int argc, char* argv[], std::unique_ptr&); void printUsage(const cvc5::Options&, bool full = false); #endif /* CVC5__MAIN__MAIN_H */ diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 1981f1063..3dafdd7f0 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -249,7 +249,7 @@ void Command::resetSolver(api::Solver* solver) // CommandExecutor such that this reconstruction can be done within the // CommandExecutor, who actually owns the solver. solver->~Solver(); - new (solver) api::Solver(opts.get()); + new (solver) api::Solver(std::move(opts)); } Node Command::termToNode(const api::Term& term) { return term.getNode(); } -- 2.30.2