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.h | |
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.h')
-rw-r--r-- | src/util/resource_manager.h | 10 |
1 files changed, 4 insertions, 6 deletions
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<Listener*> d_listeners; void spendResource(unsigned amount); |