From f99889b0c1260fccf28daac995e58312912bae9f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 17 Jul 2020 13:38:50 -0500 Subject: [PATCH] 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/. --- src/base/listener.cpp | 70 ----------- src/base/listener.h | 123 +------------------ src/options/base_options.toml | 1 - src/options/expr_options.toml | 3 - src/options/options.h | 137 --------------------- src/options/options_handler.cpp | 49 -------- src/options/options_handler.h | 9 -- src/options/options_template.cpp | 101 +-------------- src/options/smt_options.toml | 16 --- src/smt/managed_ostreams.h | 14 --- src/smt/options_manager.cpp | 24 ++++ src/smt/options_manager.h | 7 ++ src/smt/set_defaults.h | 2 +- src/smt/smt_engine.cpp | 204 ++++--------------------------- src/smt/smt_engine.h | 15 ++- src/util/resource_manager.cpp | 11 +- src/util/resource_manager.h | 10 +- test/unit/util/CMakeLists.txt | 1 - test/unit/util/listener_black.h | 153 ----------------------- 19 files changed, 75 insertions(+), 875 deletions(-) delete mode 100644 test/unit/util/listener_black.h diff --git a/src/base/listener.cpp b/src/base/listener.cpp index 63617f978..0800e4b43 100644 --- a/src/base/listener.cpp +++ b/src/base/listener.cpp @@ -25,75 +25,5 @@ namespace CVC4 { Listener::Listener(){} Listener::~Listener(){} -ListenerCollection::ListenerCollection() : d_listeners() {} -ListenerCollection::~ListenerCollection() { Assert(empty()); } - -ListenerCollection::iterator ListenerCollection::addListener(Listener* listener) -{ - return d_listeners.insert(d_listeners.end(), listener); -} - -void ListenerCollection::removeListener(iterator position) { - d_listeners.erase(position); -} - -void ListenerCollection::notify() { - for(iterator i = d_listeners.begin(), iend = d_listeners.end(); i != iend; - ++i) - { - Listener* listener = *i; - listener->notify(); - } -} - -bool ListenerCollection::empty() const { return d_listeners.empty(); } - - -ListenerCollection::Registration::Registration( - ListenerCollection* collection, Listener* listener) - : d_listener(listener) - , d_position() - , d_collection(collection) -{ - d_position = d_collection->addListener(d_listener); -} - -ListenerCollection::Registration::~Registration() { - d_collection->removeListener(d_position); - delete d_listener; -} - - ListenerCollection::Registration* ListenerCollection::registerListener( - Listener* listener) -{ - return new Registration(this, listener); -} - - -ListenerRegistrationList::ListenerRegistrationList() - : d_registrations() -{} - -ListenerRegistrationList::~ListenerRegistrationList() { - clear(); -} - -void ListenerRegistrationList::add( - ListenerCollection::Registration* registration) -{ - d_registrations.push_back(registration); -} - -void ListenerRegistrationList::clear(){ - typedef std::list::iterator iterator; - for(iterator i = d_registrations.begin(), iend = d_registrations.end(); - i != iend; ++i) - { - ListenerCollection::Registration* current = *i; - delete current; - } - d_registrations.clear(); -} - }/* CVC4 namespace */ diff --git a/src/base/listener.h b/src/base/listener.h index e131d0420..2e682b7ba 100644 --- a/src/base/listener.h +++ b/src/base/listener.h @@ -12,10 +12,7 @@ ** \brief Utility classes for listeners and collections of listeners. ** ** Utilities for the development of a Listener interface class. This class - ** provides a single notification that must be overwritten. This file also - ** provides a utility class for a collection of listeners and an RAII style - ** Registration class for managing the relationship between Listeners - ** and the collection. + ** provides a single notification that must be overwritten. **/ #include "cvc4_public.h" @@ -41,124 +38,6 @@ public: virtual void notify() = 0; }; -/** - * ListenerCollection is a list of Listener instances. - * One can add and remove Listeners. - * - * ListenerCollection does not own the memory of the Listeners. - * As a sanity check, it asserted that all of its listeners - * have been removed. - */ -class CVC4_PUBLIC ListenerCollection { -public: - typedef std::list ListenerList; - typedef ListenerList::iterator iterator; - - /** Creates an empty listener collection. */ - ListenerCollection(); - - /** - * Destroys an iterator collection. - * If assertions are on, this throws an AssertionException if the collection - * is not empty(). - */ - ~ListenerCollection(); - - /** - * This adds a listener to the current collection and returns - * an iterator to the listener in the collection. - * The user of the collection must call removeListener() using - * this iterator. - * The collection does not take over the memory for the listener. - */ - iterator addListener(Listener* listener); - - /** - * Remove an listener using the iterator distributed when adding the - * listener. - */ - void removeListener(iterator position); - - /** Calls notify() on all listeners in the collection. */ - void notify(); - - /** Returns true if the collection contains no listeners. */ - bool empty() const; - - /** - * Registration is an RAII utility function for using Listener - * with ListenerCollection. - * - * On construction, the Registration takes a ListenerCollection, - * collection, - * and a Listener*, listener. It takes over the memory for listener. It then - * adds listener to collection. On destruction it removes listener and calls - * delete on listener. - * - * Because of this usage, a Registration must be destroyed before the - * ListenerCollection it is attached to. - */ - class CVC4_PUBLIC Registration { - public: - Registration(ListenerCollection* collection, Listener* listener); - ~Registration(); - - private: - Listener* d_listener; - ListenerCollection::iterator d_position; - ListenerCollection* d_collection; - };/* class CVC4::ListenerCollection::Registration */ - - - /** - * Returns a new Registration given a Listener that is attached to this - * ListenerCollection. Management of the memory is handed to the user of - * this function. To remove the listener, call the destructor for the - * Registration. - */ - Registration* registerListener(Listener* listener); - -private: - - /** - * Disabling the copy-constructor. - * The user of the class must be know to remove listeners on the collection. - * Allowing copies will only cause confusion. - */ - ListenerCollection(const ListenerCollection& copy) = delete; - - /** - * Disabling the assignment operator. - * The user of the class must be know to remove listeners on the collection. - * Allowing copies will only cause confusion. - */ - ListenerCollection& operator=(const ListenerCollection& copy) = delete; - - /** A list of the listeners in the collection.*/ - ListenerList d_listeners; -};/* class CVC4::ListenerCollection */ - -/** - * A list of ListenerCollection::Registration* pointers. - * - * This list assumes it has control over all of the memory of the registrations. - */ -class ListenerRegistrationList { - public: - ListenerRegistrationList(); - ~ListenerRegistrationList(); - - void add(ListenerCollection::Registration* registration); - void clear(); - - private: - /** Disallow copying.*/ - ListenerRegistrationList(const ListenerRegistrationList&) = delete; - /** Disallow assignment.*/ - ListenerRegistrationList operator=(const ListenerRegistrationList&) = delete; - std::list d_registrations; -};/* class CVC4::ListenerRegistrationList */ - }/* CVC4 namespace */ #endif /* CVC4__LISTENER_H */ 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 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 Options::parseOptions(Options* options, } options->d_holder->binary_name = std::string(progName); - std::vector 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" diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h index 577ef3226..c53def1f8 100644 --- a/src/smt/managed_ostreams.h +++ b/src/smt/managed_ostreams.h @@ -74,20 +74,6 @@ class ManagedOstream { std::ostream* d_managed; }; /* class ManagedOstream */ -class SetToDefaultSourceListener : public Listener { - public: - SetToDefaultSourceListener(ManagedOstream* managedOstream) - : d_managedOstream(managedOstream){} - - void notify() override - { - d_managedOstream->set(d_managedOstream->defaultSource()); - } - - private: - ManagedOstream* d_managedOstream; -}; - /** * This controls the memory associated with --dump-to. * This is is assumed to recieve a set whenever diagnosticChannelName diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp index 5b976bc31..ce5652650 100644 --- a/src/smt/options_manager.cpp +++ b/src/smt/options_manager.cpp @@ -51,6 +51,18 @@ OptionsManager::OptionsManager(Options* opts, ResourceManager* rm) { notifySetOption(options::printSuccess.getName()); } + if (opts->wasSetByUser(options::diagnosticChannelName)) + { + notifySetOption(options::diagnosticChannelName.getName()); + } + if (opts->wasSetByUser(options::regularChannelName)) + { + notifySetOption(options::regularChannelName.getName()); + } + if (opts->wasSetByUser(options::dumpToFileName)) + { + notifySetOption(options::dumpToFileName.getName()); + } // set this as a listener to be notified of options changes from now on opts->setListener(this); } @@ -110,6 +122,18 @@ void OptionsManager::notifySetOption(const std::string& key) Warning.getStream() << Command::printsuccess(value); *options::out() << Command::printsuccess(value); } + else if (key == options::regularChannelName.getName()) + { + d_managedRegularChannel.set(options::regularChannelName()); + } + else if (key == options::diagnosticChannelName.getName()) + { + d_managedDiagnosticChannel.set(options::diagnosticChannelName()); + } + else if (key == options::dumpToFileName.getName()) + { + d_managedDumpChannel.set(options::dumpToFileName()); + } // otherwise, no action is necessary } diff --git a/src/smt/options_manager.h b/src/smt/options_manager.h index bc58f17ba..ad5fe9fa2 100644 --- a/src/smt/options_manager.h +++ b/src/smt/options_manager.h @@ -17,6 +17,7 @@ #include "options/options.h" #include "options/options_listener.h" +#include "smt/managed_ostreams.h" namespace CVC4 { @@ -65,6 +66,12 @@ class OptionsManager : public OptionsListener Options* d_options; /** Pointer to the resource manager */ ResourceManager* d_resourceManager; + /** Manager for the memory of regular-output-channel. */ + ManagedRegularOutputChannel d_managedRegularChannel; + /** Manager for the memory of diagnostic-output-channel. */ + ManagedDiagnosticOutputChannel d_managedDiagnosticChannel; + /** Manager for the memory of --dump-to. */ + ManagedDumpOStream d_managedDumpChannel; }; } // namespace smt diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h index 606921b7c..972d828bd 100644 --- a/src/smt/set_defaults.h +++ b/src/smt/set_defaults.h @@ -28,7 +28,7 @@ namespace smt { * updated by this method based on the current options and the logic itself. * @param isInternalSubsolver Whether we are setting the options for an * internal subsolver (see SmtEngine::isInternalSubsolver). - * + * * NOTE: we currently modify the current options in scope. This method * can be further refactored to modify an options object provided as an * explicit argument. diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 16e4e916a..c8896b621 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -81,17 +81,16 @@ #include "proof/theory_proof.h" #include "proof/unsat_core.h" #include "prop/prop_engine.h" -#include "smt/abstract_values.h" #include "smt/abduction_solver.h" +#include "smt/abstract_values.h" #include "smt/command.h" #include "smt/command_list.h" #include "smt/defined_function.h" #include "smt/logic_request.h" -#include "smt/managed_ostreams.h" #include "smt/model_blocker.h" #include "smt/model_core_builder.h" +#include "smt/options_manager.h" #include "smt/process_assertions.h" -#include "smt/set_defaults.h" #include "smt/smt_engine_scope.h" #include "smt/smt_engine_stats.h" #include "smt/term_formula_removal.h" @@ -161,86 +160,6 @@ class ResourceOutListener : public Listener { SmtEngine* d_smt; }; /* class ResourceOutListener */ -class BeforeSearchListener : public Listener { - public: - BeforeSearchListener(SmtEngine& smt) : d_smt(&smt) {} - void notify() override { d_smt->beforeSearch(); } - - private: - SmtEngine* d_smt; -}; /* class BeforeSearchListener */ - -class SetDefaultExprDepthListener : public Listener { - public: - void notify() override - { - int depth = options::defaultExprDepth(); - Debug.getStream() << expr::ExprSetDepth(depth); - Trace.getStream() << expr::ExprSetDepth(depth); - Notice.getStream() << expr::ExprSetDepth(depth); - Chat.getStream() << expr::ExprSetDepth(depth); - Message.getStream() << expr::ExprSetDepth(depth); - Warning.getStream() << expr::ExprSetDepth(depth); - // intentionally exclude Dump stream from this list - } -}; - -class SetDefaultExprDagListener : public Listener { - public: - void notify() override - { - int dag = options::defaultDagThresh(); - Debug.getStream() << expr::ExprDag(dag); - Trace.getStream() << expr::ExprDag(dag); - Notice.getStream() << expr::ExprDag(dag); - Chat.getStream() << expr::ExprDag(dag); - Message.getStream() << expr::ExprDag(dag); - Warning.getStream() << expr::ExprDag(dag); - Dump.getStream() << expr::ExprDag(dag); - } -}; - -class SetPrintExprTypesListener : public Listener { - public: - void notify() override - { - bool value = options::printExprTypes(); - Debug.getStream() << expr::ExprPrintTypes(value); - Trace.getStream() << expr::ExprPrintTypes(value); - Notice.getStream() << expr::ExprPrintTypes(value); - Chat.getStream() << expr::ExprPrintTypes(value); - Message.getStream() << expr::ExprPrintTypes(value); - Warning.getStream() << expr::ExprPrintTypes(value); - // intentionally exclude Dump stream from this list - } -}; - -class DumpModeListener : public Listener { - public: - void notify() override - { - const std::string& value = options::dumpModeString(); - Dump.setDumpFromString(value); - } -}; - -class PrintSuccessListener : public Listener { - public: - void notify() override - { - bool value = options::printSuccess(); - Debug.getStream() << Command::printsuccess(value); - Trace.getStream() << Command::printsuccess(value); - Notice.getStream() << Command::printsuccess(value); - Chat.getStream() << Command::printsuccess(value); - Message.getStream() << Command::printsuccess(value); - Warning.getStream() << Command::printsuccess(value); - *options::out() << Command::printsuccess(value); - } -}; - - - /** * This is an inelegant solution, but for the present, it will work. * The point of this is to separate the public and private portions of @@ -261,25 +180,13 @@ class SmtEnginePrivate : public NodeManagerListener { typedef unordered_map NodeToNodeHashMap; typedef unordered_map NodeToBoolHashMap; - /** Manager for the memory of regular-output-channel. */ - ManagedRegularOutputChannel d_managedRegularChannel; - - /** Manager for the memory of diagnostic-output-channel. */ - ManagedDiagnosticOutputChannel d_managedDiagnosticChannel; - - /** Manager for the memory of --dump-to. */ - ManagedDumpOStream d_managedDumpChannel; - /** - * This list contains: - * softResourceOut - * hardResourceOut - * beforeSearchListener - * - * This needs to be deleted before both NodeManager's Options, - * SmtEngine, d_resourceManager, and TheoryEngine. + * Manager for limiting time and abstract resource usage. */ - ListenerRegistrationList* d_listenerRegistrations; + ResourceManager* d_resourceManager; + + /** Resource out listener */ + std::unique_ptr d_routListener; /** A circuit propagator for non-clausal propositional deduction */ booleans::CircuitPropagator d_propagator; @@ -333,15 +240,11 @@ class SmtEnginePrivate : public NodeManagerListener { public: SmtEnginePrivate(SmtEngine& smt) : d_smt(smt), - d_managedRegularChannel(), - d_managedDiagnosticChannel(), - d_managedDumpChannel(), - d_listenerRegistrations(new ListenerRegistrationList()), + d_routListener(new ResourceOutListener(d_smt)), d_propagator(true, true), d_assertions(), d_assertionsProcessed(smt.getUserContext(), false), d_processor(smt, *smt.getResourceManager()), - // d_needsExpandDefs(true), //TODO? d_exprNames(smt.getUserContext()), d_iteRemover(smt.getUserContext()), d_sygusConjectureStale(smt.getUserContext(), true) @@ -349,62 +252,11 @@ class SmtEnginePrivate : public NodeManagerListener { d_smt.d_nodeManager->subscribeEvents(this); d_true = NodeManager::currentNM()->mkConst(true); ResourceManager* rm = d_smt.getResourceManager(); - - d_listenerRegistrations->add( - rm->registerListener(new ResourceOutListener(d_smt))); - - try - { - Options& opts = d_smt.getOptions(); - // Multiple options reuse BeforeSearchListener so registration requires an - // extra bit of care. - // We can safely not call notify on this before search listener at - // registration time. This d_smt cannot be beforeSearch at construction - // time. Therefore the BeforeSearchListener is a no-op. Therefore it does - // not have to be called. - d_listenerRegistrations->add( - opts.registerBeforeSearchListener(new BeforeSearchListener(d_smt))); - - // These do need registration calls. - d_listenerRegistrations->add(opts.registerSetDefaultExprDepthListener( - new SetDefaultExprDepthListener(), true)); - d_listenerRegistrations->add(opts.registerSetDefaultExprDagListener( - new SetDefaultExprDagListener(), true)); - d_listenerRegistrations->add(opts.registerSetPrintExprTypesListener( - new SetPrintExprTypesListener(), true)); - d_listenerRegistrations->add( - opts.registerSetDumpModeListener(new DumpModeListener(), true)); - d_listenerRegistrations->add(opts.registerSetPrintSuccessListener( - new PrintSuccessListener(), true)); - d_listenerRegistrations->add(opts.registerSetRegularOutputChannelListener( - new SetToDefaultSourceListener(&d_managedRegularChannel), true)); - d_listenerRegistrations->add( - opts.registerSetDiagnosticOutputChannelListener( - new SetToDefaultSourceListener(&d_managedDiagnosticChannel), - true)); - d_listenerRegistrations->add(opts.registerDumpToFileNameListener( - new SetToDefaultSourceListener(&d_managedDumpChannel), true)); - } - catch (OptionException& e) - { - // Registering the option listeners can lead to OptionExceptions, e.g. - // when the user chooses a dump tag that does not exist. In that case, we - // have to make sure that we delete existing listener registrations and - // that we unsubscribe from NodeManager events. Otherwise we will have - // errors in the deconstructors of the NodeManager (because the - // NodeManager tries to notify an SmtEnginePrivate that does not exist) - // and the ListenerCollection (because not all registrations have been - // removed before calling the deconstructor). - delete d_listenerRegistrations; - d_smt.d_nodeManager->unsubscribeEvents(this); - throw OptionException(e.getRawMessage()); - } + rm->registerListener(d_routListener.get()); } ~SmtEnginePrivate() { - delete d_listenerRegistrations; - if(d_propagator.getNeedsFinish()) { d_propagator.finish(); d_propagator.setNeedsFinish(false); @@ -620,6 +472,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_statisticsRegistry.reset(new StatisticsRegistry()); d_resourceManager.reset( new ResourceManager(*d_statisticsRegistry.get(), d_options)); + d_optm.reset(new smt::OptionsManager(&d_options, d_resourceManager.get())); d_private.reset(new smt::SmtEnginePrivate(*this)); d_stats.reset(new SmtEngineStatistics()); @@ -645,27 +498,14 @@ void SmtEngine::finishInit() // parsing smt2, this occurs at the moment we enter "Assert mode", page 52 // of SMT-LIB 2.6 standard. - // Inialize the resource manager based on the options. - if (options::perCallResourceLimit() != 0) - { - d_resourceManager->setResourceLimit(options::perCallResourceLimit(), false); - } - if (options::cumulativeResourceLimit() != 0) - { - d_resourceManager->setResourceLimit(options::cumulativeResourceLimit(), - true); - } - if (options::perCallMillisecondLimit() != 0) - { - d_resourceManager->setTimeLimit(options::perCallMillisecondLimit()); - } - // set the random seed Random::getRandom().setSeed(options::seed()); - // ensure that our heuristics are properly set up - setDefaults(d_logic, d_isInternalSubsolver); - + // Call finish init on the options manager. This inializes the resource + // manager based on the options, and sets up the best default options + // based on our heuristics. + d_optm->finishInit(d_logic, d_isInternalSubsolver); + Trace("smt-debug") << "SmtEngine::finishInit" << std::endl; // We have mutual dependency here, so we add the prop engine to the theory // engine later (it is non-essential there) @@ -850,6 +690,7 @@ SmtEngine::~SmtEngine() d_stats.reset(nullptr); d_private.reset(nullptr); + d_optm.reset(nullptr); // d_resourceManager must be destroyed before d_statisticsRegistry d_resourceManager.reset(nullptr); d_statisticsRegistry.reset(nullptr); @@ -3425,17 +3266,14 @@ void SmtEngine::setPrintFuncInModel(Expr f, bool p) { } } -void SmtEngine::beforeSearch() +void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) { + // Always check whether the SmtEngine has been initialized (which is done + // upon entering Assert mode the first time). No option can be set after + // initialized. if(d_fullyInited) { - throw ModalException( - "SmtEngine::beforeSearch called after initialization."); + throw ModalException("SmtEngine::setOption called after initialization."); } -} - - -void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) -{ NodeManagerScope nms(d_nodeManager); Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 591b69424..b38ec2d7a 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -93,6 +93,7 @@ namespace prop { namespace smt { /** Utilities */ class AbstractValues; +class OptionsManager; /** Subsolvers */ class AbductionSolver; /** @@ -855,14 +856,6 @@ class CVC4_PUBLIC SmtEngine /** Set print function in model. */ void setPrintFuncInModel(Expr f, bool p); - /** - * Check and throw a ModalException if the SmtEngine has been fully - * initialized. - * - * throw@ ModalException - */ - void beforeSearch(); - /** * Get expression name. * @@ -1298,6 +1291,12 @@ class CVC4_PUBLIC SmtEngine * Manager for limiting time and abstract resource usage. */ std::unique_ptr d_resourceManager; + /** + * The options manager, which is responsible for implementing core options + * such as those related to time outs and printing. It is also responsible + * for set default options based on the logic. + */ + std::unique_ptr d_optm; /** * The global scope object. Upon creation of this SmtEngine, it becomes the * SmtEngine in scope. It says the SmtEngine in scope until it is destructed, diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index ac1d57324..07b135b58 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -158,7 +158,6 @@ ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options) d_thisCallResourceUsed(0), d_thisCallResourceBudget(0), d_on(false), - d_listeners(), d_statistics(new ResourceManager::Statistics(stats)), d_options(options) @@ -227,7 +226,10 @@ void ResourceManager::spendResource(unsigned amount) << d_perCallTimer.elapsed() << std::endl; } - d_listeners.notify(); + for (Listener* l : d_listeners) + { + l->notify(); + } } } @@ -369,10 +371,9 @@ void ResourceManager::enable(bool on) d_on = on; } -ListenerCollection::Registration* ResourceManager::registerListener( - Listener* listener) +void ResourceManager::registerListener(Listener* listener) { - return d_listeners.registerListener(listener); + return d_listeners.push_back(listener); } } /* namespace CVC4 */ diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index 57a227d7b..6a9b3e2bf 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -162,12 +162,10 @@ class CVC4_PUBLIC ResourceManager static uint64_t getFrequencyCount() { return s_resourceCount; } /** - * Registers a listener that is notified on a resource out. - * - * This Registration must be destroyed by the user before this - * ResourceManager. + * Registers a listener that is notified on a resource out or (per-call) + * timeout. */ - ListenerCollection::Registration* registerListener(Listener* listener); + void registerListener(Listener* listener); private: /** The per-call wall clock timer. */ @@ -201,7 +199,7 @@ class CVC4_PUBLIC ResourceManager static const uint64_t s_resourceCount; /** Receives a notification on reaching a limit. */ - ListenerCollection d_listeners; + std::vector d_listeners; void spendResource(unsigned amount); diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt index af2ca0dfa..c28869dbd 100644 --- a/test/unit/util/CMakeLists.txt +++ b/test/unit/util/CMakeLists.txt @@ -13,7 +13,6 @@ cvc4_add_unit_test_black(datatype_black util) cvc4_add_unit_test_black(exception_black util) cvc4_add_unit_test_black(integer_black util) cvc4_add_unit_test_white(integer_white util) -cvc4_add_unit_test_black(listener_black util) cvc4_add_unit_test_black(output_black util) cvc4_add_unit_test_black(rational_black util) cvc4_add_unit_test_white(rational_white util) diff --git a/test/unit/util/listener_black.h b/test/unit/util/listener_black.h deleted file mode 100644 index 2b34e8dbb..000000000 --- a/test/unit/util/listener_black.h +++ /dev/null @@ -1,153 +0,0 @@ -/********************* */ -/*! \file listener_black.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Andres Noetzli, Paul Meng - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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.\endverbatim - ** - ** \brief Black box testing of CVC4 output classes. - ** - ** Black box testing of CVC4 output classes. - **/ - -#include -#include - -#include "base/listener.h" - -using namespace CVC4; -using namespace std; - -class ListenerBlack : public CxxTest::TestSuite { - - std::multiset d_events; - - class EventListener : public Listener { - public: - EventListener(std::multiset& events, std::string name) - : d_events(events), d_name(name) {} - ~EventListener() override {} - - void notify() override { d_events.insert(d_name); } - - private: - std::multiset& d_events; - std::string d_name; - }; - -public: - - static std::multiset mkMultiset(std::string arr[], int len){ - return std::multiset(arr, arr + len); - } - - void setUp() override { d_events.clear(); } - - void tearDown() override { d_events.clear(); } - - void testEmptyCollection() { - // Makes an new collection and tests that it is empty. - ListenerCollection* collection = new ListenerCollection; - TS_ASSERT(collection->empty()); - TS_ASSERT_THROWS_NOTHING( delete collection ); - } - - void testSingletonCollection() { - ListenerCollection collection; - std::string expected[1] = {"a"}; - { - ListenerCollection::Registration a(&collection, new EventListener(d_events, "a")); - collection.notify(); - TS_ASSERT(not collection.empty()); - } - TS_ASSERT(collection.empty()); - TS_ASSERT_EQUALS(d_events, mkMultiset(expected, 1)); - } - - void testSingleRegisterTearDown() { - // Tests that collection succeeds at destruction after - // registering a single event. - ListenerCollection* collection = new ListenerCollection; - { - ListenerCollection::Registration a(collection, new EventListener(d_events, "a")); - TS_ASSERT(not collection->empty()); - // The destructor for a now runs. - } - TS_ASSERT(collection->empty()); - TS_ASSERT_THROWS_NOTHING( delete collection ); - } - - void testMultipleCollection() { - ListenerCollection* collection = new ListenerCollection; - { - ListenerCollection::Registration c(collection, new EventListener(d_events, "c")); - collection->notify(); - // d_events == {"c"} - ListenerCollection::Registration b(collection, new EventListener(d_events, "b")); - ListenerCollection::Registration a(collection, new EventListener(d_events, "a")); - collection->notify(); - // d_events == {"a", "b", "c", "c"} - TS_ASSERT(not collection->empty()); - } - TS_ASSERT(collection->empty()); - std::string expected[4] = {"a", "b", "c", "c"}; - TS_ASSERT_EQUALS(d_events, mkMultiset(expected, 4)); - TS_ASSERT_THROWS_NOTHING( delete collection ); - } - - void testRegisterMiddleTearDown() { - // Tests that collection succeeds at destruction after - // registering several events. - ListenerCollection* collection = new ListenerCollection; - { - ListenerCollection::Registration a(collection, new EventListener(d_events, "a")); - ListenerCollection::Registration* b = - new ListenerCollection::Registration(collection, new EventListener(d_events, "b")); - ListenerCollection::Registration c(collection, new EventListener(d_events, "c")); - - collection->notify(); - delete b; - collection->notify(); - // The destructor for a and c now run. - TS_ASSERT(not collection->empty()); - } - TS_ASSERT(collection->empty()); - TS_ASSERT_THROWS_NOTHING( delete collection ); - } - - - - void testRegisterMultiple() { - // This tests adds and notify multiple times. - ListenerCollection collection; - - std::vector listeners; - for(int i = 0; i < 4 ; ++i){ - stringstream ss; ss << i; - Listener* listener = new EventListener(d_events, ss.str()); - listeners.push_back(new ListenerCollection::Registration(&collection, listener)); - collection.notify(); - } - - TS_ASSERT(not collection.empty()); - for(unsigned i=0; i < listeners.size(); ++i){ - ListenerCollection::Registration* at_i = listeners[i]; - delete at_i; - } - listeners.clear(); - TS_ASSERT(collection.empty()); - - std::string expected[10] = - {"0", "0", "0", "0", "1", "1", "1", "2", "2", "3"}; - TS_ASSERT_EQUALS(d_events, mkMultiset(expected, 10)); - - // No more events occur. - collection.notify(); - TS_ASSERT_EQUALS(d_events, mkMultiset(expected, 10)); - } - -}; -- 2.30.2