From: Gereon Kremer Date: Sun, 6 Jun 2021 11:09:40 +0000 (+0200) Subject: Support public option modules (#6691) X-Git-Tag: cvc5-1.0.0~1637 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f27d633c82442f2106f747195834c2cb5ba6dd81;p=cvc5.git Support public option modules (#6691) This PR adds the possibility to make option modules public. As shown on the example of the main driver options, this allows to get rid of the wrappers from options_public.h. We plan to make only very few option modules public (i.e. main and parser). --- diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 4f82ac1ae..caa0340bd 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -35,6 +35,7 @@ #include "main/time_limit.h" #include "options/options.h" #include "options/options_public.h" +#include "options/main_options.h" #include "options/set_language.h" #include "parser/parser.h" #include "parser/parser_builder.h" @@ -112,7 +113,7 @@ int runCvc5(int argc, char* argv[], Options& opts) string progNameStr = options::getBinaryName(opts); progName = &progNameStr; - if (options::getHelp(opts)) + if (opts.driver.help) { printUsage(opts, true); exit(1); @@ -122,13 +123,13 @@ int runCvc5(int argc, char* argv[], Options& opts) Options::printLanguageHelp(*(options::getOut(opts))); exit(1); } - else if (options::getVersion(opts)) + else if (opts.driver.version) { *(options::getOut(opts)) << Configuration::about().c_str() << flush; exit(0); } - segvSpin = options::getSegvSpin(opts); + segvSpin = opts.driver.segvSpin; // If in competition mode, set output stream option to flush immediately #ifdef CVC5_COMPETITION_MODE @@ -146,7 +147,7 @@ int runCvc5(int argc, char* argv[], Options& opts) // if we're reading from stdin on a TTY, default to interactive mode if (!options::wasSetByUserInteractive(opts)) { - options::setInteractive(inputFromStdin && isatty(fileno(stdin)), opts); + opts.driver.interactive = inputFromStdin && isatty(fileno(stdin)); } // Auto-detect input language by filename extension @@ -212,9 +213,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 (options::getInteractive(opts) && inputFromStdin) + if (opts.driver.interactive && inputFromStdin) { - if (options::getTearDownIncremental(opts) > 0) + if (opts.driver.tearDownIncremental > 0) { throw Exception( "--tear-down-incremental doesn't work in interactive mode"); @@ -227,7 +228,7 @@ int runCvc5(int argc, char* argv[], Options& opts) } InteractiveShell shell(pExecutor->getSolver(), pExecutor->getSymbolManager()); - if (options::getInteractivePrompt(opts)) + if (opts.driver.interactivePrompt) { CVC5Message() << Configuration::getPackageName() << " " << Configuration::getVersionString(); @@ -257,10 +258,10 @@ int runCvc5(int argc, char* argv[], Options& opts) } } } - else if (options::getTearDownIncremental(opts) > 0) + else if (opts.driver.tearDownIncremental > 0) { if (!options::getIncrementalSolving(opts) - && options::getTearDownIncremental(opts) > 1) + && opts.driver.tearDownIncremental > 1) { // For tear-down-incremental values greater than 1, need incremental // on too. @@ -313,7 +314,7 @@ int runCvc5(int argc, char* argv[], Options& opts) } if(dynamic_cast(cmd.get()) != nullptr) { - if (needReset >= options::getTearDownIncremental(opts)) + if (needReset >= opts.driver.tearDownIncremental) { pExecutor->reset(); for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) { @@ -342,7 +343,7 @@ int runCvc5(int argc, char* argv[], Options& opts) } } else if(dynamic_cast(cmd.get()) != nullptr) { allCommands.pop_back(); // fixme leaks cmds here - if (needReset >= options::getTearDownIncremental(opts)) + if (needReset >= opts.driver.tearDownIncremental) { pExecutor->reset(); for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) { @@ -371,7 +372,7 @@ int runCvc5(int argc, char* argv[], Options& opts) } } else if(dynamic_cast(cmd.get()) != nullptr || dynamic_cast(cmd.get()) != nullptr) { - if (needReset >= options::getTearDownIncremental(opts)) + if (needReset >= opts.driver.tearDownIncremental) { pExecutor->reset(); for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) { @@ -511,12 +512,12 @@ int runCvc5(int argc, char* argv[], Options& opts) pExecutor->flushOutputStreams(); #ifdef CVC5_DEBUG - if (options::getEarlyExit(opts) && options::wasSetByUserEarlyExit(opts)) + if (opts.driver.earlyExit && options::wasSetByUserEarlyExit(opts)) { _exit(returnValue); } #else /* CVC5_DEBUG */ - if (options::getEarlyExit(opts)) + if (opts.driver.earlyExit) { _exit(returnValue); } diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 9a0539490..048c101f0 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -41,6 +41,7 @@ #include "base/output.h" #include "expr/symbol_manager.h" #include "options/language.h" +#include "options/main_options.h" #include "options/options.h" #include "options/options_public.h" #include "parser/input.h" @@ -198,7 +199,7 @@ restart: if (d_usingEditline) { #if HAVE_LIBEDITLINE - lineBuf = ::readline(options::getInteractivePrompt(d_options) + lineBuf = ::readline(d_options.driver.interactivePrompt ? (line == "" ? "cvc5> " : "... > ") : ""); if(lineBuf != NULL && lineBuf[0] != '\0') { @@ -210,7 +211,7 @@ restart: } else { - if (options::getInteractivePrompt(d_options)) + if (d_options.driver.interactivePrompt) { if(line == "") { d_out << "cvc5> " << flush; @@ -284,7 +285,7 @@ restart: if (d_usingEditline) { #if HAVE_LIBEDITLINE - lineBuf = ::readline(options::getInteractivePrompt(d_options) ? "... > " + lineBuf = ::readline(d_options.driver.interactivePrompt ? "... > " : ""); if(lineBuf != NULL && lineBuf[0] != '\0') { ::add_history(lineBuf); @@ -295,7 +296,7 @@ restart: } else { - if (options::getInteractivePrompt(d_options)) + if (d_options.driver.interactivePrompt) { d_out << "... > " << flush; } diff --git a/src/options/main_options.toml b/src/options/main_options.toml index ccbf2e6ae..0f5dfdcd7 100644 --- a/src/options/main_options.toml +++ b/src/options/main_options.toml @@ -1,5 +1,6 @@ id = "DRIVER" name = "Driver" +public = true [[option]] name = "version" diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index df0ef1a38..73de9209b 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -49,7 +49,7 @@ import toml ### Allowed attributes for module/option MODULE_ATTR_REQ = ['id', 'name'] -MODULE_ATTR_ALL = MODULE_ATTR_REQ + ['option'] +MODULE_ATTR_ALL = MODULE_ATTR_REQ + ['option', 'public'] OPTION_ATTR_REQ = ['category', 'type'] OPTION_ATTR_ALL = OPTION_ATTR_REQ + [ @@ -615,10 +615,14 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): help=help_mode_format(option), long=option.long.split('=')[0])) + if module.public: + visibility_include = '#include "cvc5_public.h"' + else: + visibility_include = '#include "cvc5_private.h"' + filename = os.path.splitext(os.path.split(module.header)[1])[0] write_file(dst_dir, '{}.h'.format(filename), tpl_module_h.format( - filename=filename, - header=module.header, + visibility_include=visibility_include, id_cap=module.id_cap, id=module.id, includes='\n'.join(sorted(list(includes))), diff --git a/src/options/module_template.h b/src/options/module_template.h index 722490948..a74d3c49d 100644 --- a/src/options/module_template.h +++ b/src/options/module_template.h @@ -16,7 +16,7 @@ * expands this template and generates a _options.h file. */ -#include "cvc5_private.h" +${visibility_include}$ #ifndef CVC5__OPTIONS__${id_cap}$_H #define CVC5__OPTIONS__${id_cap}$_H diff --git a/src/options/options_public.cpp b/src/options/options_public.cpp index 778056553..f590ba083 100644 --- a/src/options/options_public.cpp +++ b/src/options/options_public.cpp @@ -61,7 +61,6 @@ 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; @@ -70,21 +69,14 @@ 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; @@ -98,15 +90,10 @@ 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; @@ -125,10 +112,6 @@ 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) { diff --git a/src/options/options_public.h b/src/options/options_public.h index a6d93cae7..9b549601f 100644 --- a/src/options/options_public.h +++ b/src/options/options_public.h @@ -37,25 +37,18 @@ 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; @@ -65,7 +58,6 @@ 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;