diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-17 13:38:50 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-17 13:38:50 -0500 |
commit | f99889b0c1260fccf28daac995e58312912bae9f (patch) | |
tree | c9bba127e62aedef587ee7da83950281a4c131f4 /src/options | |
parent | e8df6f67cc2654f50d49995377a4b411668235e1 (diff) |
Replace options listener infrastructure (#4764)
This replaces the old options listener infrastructure with the OptionsManager introduced in cb8d041.
It eliminates a "beforeSearchListener", which was a custom way of some options throwing a modal exception if they were set after initialization. Now all options are consistent: no option can be set after initialization.
It also moves managed ostream objects to the OptionsManager.
@mpreiner The next step will be to remove the "notifies" field from the Options build system and then proceed with cleaning src/options/.
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/base_options.toml | 1 | ||||
-rw-r--r-- | src/options/expr_options.toml | 3 | ||||
-rw-r--r-- | src/options/options.h | 137 | ||||
-rw-r--r-- | src/options/options_handler.cpp | 49 | ||||
-rw-r--r-- | src/options/options_handler.h | 9 | ||||
-rw-r--r-- | src/options/options_template.cpp | 101 | ||||
-rw-r--r-- | src/options/smt_options.toml | 16 |
7 files changed, 4 insertions, 312 deletions
diff --git a/src/options/base_options.toml b/src/options/base_options.toml index 65eeda3ae..cab4332b8 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -151,6 +151,5 @@ header = "options/base_options.h" category = "regular" long = "print-success" type = "bool" - notifies = ["notifyPrintSuccess"] read_only = true help = "print the \"success\" output required of SMT-LIBv2" diff --git a/src/options/expr_options.toml b/src/options/expr_options.toml index 5f70aee43..037d46169 100644 --- a/src/options/expr_options.toml +++ b/src/options/expr_options.toml @@ -9,7 +9,6 @@ header = "options/expr_options.h" type = "int" default = "0" predicates = ["setDefaultExprDepthPredicate"] - notifies = ["notifySetDefaultExprDepth"] read_only = true help = "print exprs to depth N (0 == default, -1 == no limit)" @@ -21,7 +20,6 @@ header = "options/expr_options.h" type = "int" default = "1" predicates = ["setDefaultDagThreshPredicate"] - notifies = ["notifySetDefaultDagThresh"] read_only = true help = "dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)" @@ -31,7 +29,6 @@ header = "options/expr_options.h" long = "print-expr-types" type = "bool" default = "false" - notifies = ["notifySetPrintExprTypes"] read_only = true help = "print types with variables when printing exprs" diff --git a/src/options/options.h b/src/options/options.h index 2ea72ca92..44f4be7b4 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -53,36 +53,6 @@ class CVC4_PUBLIC Options { /** The current Options in effect */ static thread_local Options* s_current; - /** Listeners for notifyBeforeSearch. */ - ListenerCollection d_beforeSearchListeners; - - /** Listeners for options::defaultExprDepth. */ - ListenerCollection d_setDefaultExprDepthListeners; - - /** Listeners for options::defaultDagThresh. */ - ListenerCollection d_setDefaultDagThreshListeners; - - /** Listeners for options::printExprTypes. */ - ListenerCollection d_setPrintExprTypesListeners; - - /** Listeners for options::dumpModeString. */ - ListenerCollection d_setDumpModeListeners; - - /** Listeners for options::printSuccess. */ - ListenerCollection d_setPrintSuccessListeners; - - /** Listeners for options::dumpToFileName. */ - ListenerCollection d_dumpToFileListeners; - - /** Listeners for options::regularChannelName. */ - ListenerCollection d_setRegularChannelListeners; - - /** Listeners for options::diagnosticChannelName. */ - ListenerCollection d_setDiagnosticChannelListeners; - - static ListenerCollection::Registration* registerAndNotify( - ListenerCollection& collection, Listener* listener, bool notify); - /** Low-level assignment function for options */ template <class T> void assign(T, std::string option, std::string value); @@ -304,113 +274,6 @@ public: /** Set the generic listener associated with this class to ol */ void setListener(OptionsListener* ol); - /** - * Registers a listener for the notification, notifyBeforeSearch. - * - * The memory for the Registration is controlled by the user and must - * be destroyed before the Options object is. - * - * This has multiple usages so having a notifyIfSet flag does not add - * clarity. Users should check the relevant flags before registering this. - */ - ListenerCollection::Registration* registerBeforeSearchListener( - Listener* listener); - - /** - * Registers a listener for options::defaultExprDepth being set. - * - * If notifyIfSet is true, this calls notify on the listener - * if the option was set by the user. - * - * The memory for the Registration is controlled by the user and must - * be destroyed before the Options object is. - */ - ListenerCollection::Registration* registerSetDefaultExprDepthListener( - Listener* listener, bool notifyIfSet); - - /** - * Registers a listener for options::defaultDagThresh being set. - * - * If notifyIfSet is true, this calls notify on the listener - * if the option was set by the user. - * - * The memory for the Registration is controlled by the user and must - * be destroyed before the Options object is. - */ - ListenerCollection::Registration* registerSetDefaultExprDagListener( - Listener* listener, bool notifyIfSet); - - /** - * Registers a listener for options::printExprTypes being set. - * - * If notifyIfSet is true, this calls notify on the listener - * if the option was set by the user. - * - * The memory for the Registration is controlled by the user and must - * be destroyed before the Options object is. - */ - ListenerCollection::Registration* registerSetPrintExprTypesListener( - Listener* listener, bool notifyIfSet); - - /** - * Registers a listener for options::dumpModeString being set. - * - * If notifyIfSet is true, this calls notify on the listener - * if the option was set by the user. - * - * The memory for the Registration is controlled by the user and must - * be destroyed before the Options object is. - */ - ListenerCollection::Registration* registerSetDumpModeListener( - Listener* listener, bool notifyIfSet); - - /** - * Registers a listener for options::printSuccess being set. - * - * If notifyIfSet is true, this calls notify on the listener - * if the option was set by the user. - * - * The memory for the Registration is controlled by the user and must - * be destroyed before the Options object is. - */ - ListenerCollection::Registration* registerSetPrintSuccessListener( - Listener* listener, bool notifyIfSet); - - /** - * Registers a listener for options::dumpToFileName being set. - * - * If notifyIfSet is true, this calls notify on the listener - * if the option was set by the user. - * - * The memory for the Registration is controlled by the user and must - * be destroyed before the Options object is. - */ - ListenerCollection::Registration* registerDumpToFileNameListener( - Listener* listener, bool notifyIfSet); - - /** - * Registers a listener for options::regularChannelName being set. - * - * If notifyIfSet is true, this calls notify on the listener - * if the option was set by the user. - * - * The memory for the Registration is controlled by the user and must - * be destroyed before the Options object is. - */ - ListenerCollection::Registration* registerSetRegularOutputChannelListener( - Listener* listener, bool notifyIfSet); - - /** - * Registers a listener for options::diagnosticChannelName being set. - * - * If notifyIfSet is true, this calls notify on the listener - * if the option was set by the user. - * - * The memory for the Registration is controlled by the user and must - * be destroyed before the Options object is. - */ - ListenerCollection::Registration* registerSetDiagnosticOutputChannelListener( - Listener* listener, bool notifyIfSet); /** Sends a std::flush to getErr(). */ void flushErr(); diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 40f9b898e..b752bfdda 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -69,17 +69,6 @@ void throwLazyBBUnsupported(options::SatSolverMode m) OptionsHandler::OptionsHandler(Options* options) : d_options(options) { } -void OptionsHandler::notifyBeforeSearch(const std::string& option) -{ - try{ - d_options->d_beforeSearchListeners.notify(); - } catch (ModalException&){ - std::stringstream ss; - ss << "cannot change option `" << option << "' after final initialization"; - throw ModalException(ss.str()); - } -} - unsigned long OptionsHandler::limitHandler(std::string option, std::string optarg) { @@ -92,12 +81,6 @@ unsigned long OptionsHandler::limitHandler(std::string option, } return ms; } - -/* options/base_options_handlers.h */ -void OptionsHandler::notifyPrintSuccess(std::string option) { - d_options->d_setPrintSuccessListeners.notify(); -} - // theory/quantifiers/options_handlers.h void OptionsHandler::checkInstWhenMode(std::string option, InstWhenMode mode) @@ -310,19 +293,6 @@ void OptionsHandler::LFSCEnabledBuild(std::string option, bool value) { #endif /* CVC4_USE_LFSC */ } -void OptionsHandler::notifyDumpToFile(std::string option) { - d_options->d_dumpToFileListeners.notify(); -} - - -void OptionsHandler::notifySetRegularOutputChannel(std::string option) { - d_options->d_setRegularChannelListeners.notify(); -} - -void OptionsHandler::notifySetDiagnosticOutputChannel(std::string option) { - d_options->d_setDiagnosticChannelListeners.notify(); -} - void OptionsHandler::statsEnabledBuild(std::string option, bool value) { #ifndef CVC4_STATISTICS_ON @@ -338,12 +308,6 @@ void OptionsHandler::threadN(std::string option) { throw OptionException(option + " is not a real option by itself. Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\""); } -void OptionsHandler::notifyDumpMode(std::string option) -{ - d_options->d_setDumpModeListeners.notify(); -} - - // expr/options_handlers.h void OptionsHandler::setDefaultExprDepthPredicate(std::string option, int depth) { if(depth < -1) { @@ -357,19 +321,6 @@ void OptionsHandler::setDefaultDagThreshPredicate(std::string option, int dag) { } } -void OptionsHandler::notifySetDefaultExprDepth(std::string option) { - d_options->d_setDefaultExprDepthListeners.notify(); -} - -void OptionsHandler::notifySetDefaultDagThresh(std::string option) { - d_options->d_setDefaultDagThreshListeners.notify(); -} - -void OptionsHandler::notifySetPrintExprTypes(std::string option) { - d_options->d_setPrintExprTypesListeners.notify(); -} - - // main/options_handlers.h static void print_config (const char * str, std::string config) { diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 876edfad7..221e6179f 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -84,14 +84,9 @@ public: * Throws a ModalException if this option is being set after final * initialization. */ - void notifyBeforeSearch(const std::string& option); - void notifyDumpMode(std::string option); void setProduceAssertions(std::string option, bool value); void proofEnabledBuild(std::string option, bool value); void LFSCEnabledBuild(std::string option, bool value); - void notifyDumpToFile(std::string option); - void notifySetRegularOutputChannel(std::string option); - void notifySetDiagnosticOutputChannel(std::string option); void statsEnabledBuild(std::string option, bool value); @@ -100,9 +95,6 @@ public: /* expr/options_handlers.h */ void setDefaultExprDepthPredicate(std::string option, int depth); void setDefaultDagThreshPredicate(std::string option, int dag); - void notifySetDefaultExprDepth(std::string option); - void notifySetDefaultDagThresh(std::string option); - void notifySetPrintExprTypes(std::string option); /* main/options_handlers.h */ void copyright(std::string option); @@ -119,7 +111,6 @@ public: InputLanguage stringToInputLanguage(std::string option, std::string optarg); void enableTraceTag(std::string option, std::string optarg); void enableDebugTag(std::string option, std::string optarg); - void notifyPrintSuccess(std::string option); private: diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index b4aa3dae0..5afa9173e 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -224,12 +224,10 @@ void runBoolPredicates(T, std::string option, bool b, options::OptionsHandler* h // that can throw exceptions. } - Options::Options(OptionsListener* ol) - : d_holder(new options::OptionsHolder()) - , d_handler(new options::OptionsHandler(this)) - , d_beforeSearchListeners(), - d_olisten(ol) + : d_holder(new options::OptionsHolder()), + d_handler(new options::OptionsHandler(this)), + d_olisten(ol) {} Options::~Options() { @@ -254,94 +252,6 @@ std::string Options::formatThreadOptionException(const std::string& option) { void Options::setListener(OptionsListener* ol) { d_olisten = ol; } -ListenerCollection::Registration* Options::registerAndNotify( - ListenerCollection& collection, Listener* listener, bool notify) -{ - ListenerCollection::Registration* registration = - collection.registerListener(listener); - if(notify) { - try - { - listener->notify(); - } - catch (OptionException& e) - { - // It can happen that listener->notify() throws an OptionException. In - // that case, we have to make sure that we delete the registration of our - // listener before rethrowing the exception. Otherwise the - // ListenerCollection deconstructor will complain that not all - // registrations have been removed before invoking the deconstructor. - delete registration; - throw OptionException(e.getRawMessage()); - } - } - return registration; -} - -ListenerCollection::Registration* Options::registerBeforeSearchListener( - Listener* listener) -{ - return d_beforeSearchListeners.registerListener(listener); -} - -ListenerCollection::Registration* Options::registerSetDefaultExprDepthListener( - Listener* listener, bool notifyIfSet) -{ - bool notify = notifyIfSet && wasSetByUser(options::defaultExprDepth); - return registerAndNotify(d_setDefaultExprDepthListeners, listener, notify); -} - -ListenerCollection::Registration* Options::registerSetDefaultExprDagListener( - Listener* listener, bool notifyIfSet) -{ - bool notify = notifyIfSet && wasSetByUser(options::defaultDagThresh); - return registerAndNotify(d_setDefaultDagThreshListeners, listener, notify); -} - -ListenerCollection::Registration* Options::registerSetPrintExprTypesListener( - Listener* listener, bool notifyIfSet) -{ - bool notify = notifyIfSet && wasSetByUser(options::printExprTypes); - return registerAndNotify(d_setPrintExprTypesListeners, listener, notify); -} - -ListenerCollection::Registration* Options::registerSetDumpModeListener( - Listener* listener, bool notifyIfSet) -{ - bool notify = notifyIfSet && wasSetByUser(options::dumpModeString); - return registerAndNotify(d_setDumpModeListeners, listener, notify); -} - -ListenerCollection::Registration* Options::registerSetPrintSuccessListener( - Listener* listener, bool notifyIfSet) -{ - bool notify = notifyIfSet && wasSetByUser(options::printSuccess); - return registerAndNotify(d_setPrintSuccessListeners, listener, notify); -} - -ListenerCollection::Registration* Options::registerDumpToFileNameListener( - Listener* listener, bool notifyIfSet) -{ - bool notify = notifyIfSet && wasSetByUser(options::dumpToFileName); - return registerAndNotify(d_dumpToFileListeners, listener, notify); -} - -ListenerCollection::Registration* -Options::registerSetRegularOutputChannelListener( - Listener* listener, bool notifyIfSet) -{ - bool notify = notifyIfSet && wasSetByUser(options::regularChannelName); - return registerAndNotify(d_setRegularChannelListeners, listener, notify); -} - -ListenerCollection::Registration* -Options::registerSetDiagnosticOutputChannelListener( - Listener* listener, bool notifyIfSet) -{ - bool notify = notifyIfSet && wasSetByUser(options::diagnosticChannelName); - return registerAndNotify(d_setDiagnosticChannelListeners, listener, notify); -} - ${custom_handlers}$ #if defined(CVC4_MUZZLED) || defined(CVC4_COMPETITION_MODE) @@ -497,7 +407,6 @@ std::vector<std::string> Options::parseOptions(Options* options, } options->d_holder->binary_name = std::string(progName); - std::vector<std::string> nonoptions; parseOptionsRecursive(options, argc, argv, &nonoptions); if(Debug.isOn("options")){ @@ -688,11 +597,9 @@ void Options::setOptionInternal(const std::string& key, std::string Options::getOption(const std::string& key) const { - Trace("options") << "SMT getOption(" << key << ")" << std::endl; - + Trace("options") << "Options::getOption(" << key << ")" << std::endl; ${getoption_handlers}$ - throw UnrecognizedOptionException(key); } diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 18a99ad3c..3fecab5c9 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -8,7 +8,6 @@ header = "options/smt_options.h" category = "common" long = "dump=MODE" type = "std::string" - notifies = ["notifyDumpMode"] read_only = true help = "dump preprocessed assertions, etc., see --dump=help" @@ -18,7 +17,6 @@ header = "options/smt_options.h" category = "common" long = "dump-to=FILE" type = "std::string" - notifies = ["notifyDumpToFile"] read_only = true help = "all dumping goes to FILE (instead of stdout)" @@ -71,7 +69,6 @@ header = "options/smt_options.h" long = "produce-models" type = "bool" default = "false" - notifies = ["notifyBeforeSearch"] help = "support the get-value and get-model commands" [[option]] @@ -79,7 +76,6 @@ header = "options/smt_options.h" category = "regular" long = "check-models" type = "bool" - notifies = ["notifyBeforeSearch"] help = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions" [[option]] @@ -87,7 +83,6 @@ header = "options/smt_options.h" category = "regular" long = "debug-check-models" type = "bool" - notifies = ["notifyBeforeSearch"] help = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user and internal assertions" [[option]] @@ -143,7 +138,6 @@ header = "options/smt_options.h" type = "bool" default = "false" predicates = ["proofEnabledBuild"] - notifies = ["notifyBeforeSearch"] help = "turn on proof generation" [[option]] @@ -152,7 +146,6 @@ header = "options/smt_options.h" long = "check-proofs" type = "bool" predicates = ["LFSCEnabledBuild"] - notifies = ["notifyBeforeSearch"] help = "after UNSAT/VALID, machine-check the generated proof" [[option]] @@ -234,7 +227,6 @@ header = "options/smt_options.h" long = "produce-unsat-cores" type = "bool" predicates = ["proofEnabledBuild"] - notifies = ["notifyBeforeSearch"] help = "turn on unsat core generation" [[option]] @@ -250,7 +242,6 @@ header = "options/smt_options.h" long = "dump-unsat-cores" type = "bool" default = "false" - notifies = ["notifyBeforeSearch"] help = "output unsat cores after every UNSAT/VALID response" [[option]] @@ -259,7 +250,6 @@ header = "options/smt_options.h" long = "dump-unsat-cores-full" type = "bool" default = "false" - notifies = ["notifyBeforeSearch"] read_only = true help = "dump the full unsat core, including unlabeled assertions" @@ -270,7 +260,6 @@ header = "options/smt_options.h" type = "bool" default = "false" predicates = ["proofEnabledBuild"] - notifies = ["notifyBeforeSearch"] read_only = true help = "turn on unsat assumptions generation" @@ -288,7 +277,6 @@ header = "options/smt_options.h" long = "produce-assignments" type = "bool" default = "false" - notifies = ["notifyBeforeSearch"] help = "support the get-assignment command" [[option]] @@ -297,7 +285,6 @@ header = "options/smt_options.h" category = "undocumented" type = "bool" predicates = ["setProduceAssertions"] - notifies = ["notifyBeforeSearch"] help = "deprecated name for produce-assertions" [[option]] @@ -306,7 +293,6 @@ header = "options/smt_options.h" long = "produce-assertions" type = "bool" predicates = ["setProduceAssertions"] - notifies = ["notifyBeforeSearch"] help = "keep an assertions list (enables get-assertions command)" [[option]] @@ -429,7 +415,6 @@ header = "options/smt_options.h" smt_name = "regular-output-channel" category = "regular" type = "std::string" - notifies = ["notifySetRegularOutputChannel"] read_only = true help = "set the regular output channel of the solver" @@ -438,7 +423,6 @@ header = "options/smt_options.h" smt_name = "diagnostic-output-channel" category = "regular" type = "std::string" - notifies = ["notifySetDiagnosticOutputChannel"] read_only = true help = "set the diagnostic output channel of the solver" |