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/util/resource_manager.cpp | |
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/util/resource_manager.cpp')
-rw-r--r-- | src/util/resource_manager.cpp | 11 |
1 files changed, 6 insertions, 5 deletions
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 */ |