diff options
Diffstat (limited to 'src/options/options.h')
| -rw-r--r-- | src/options/options.h | 383 |
1 files changed, 377 insertions, 6 deletions
diff --git a/src/options/options.h b/src/options/options.h index 8e1ca2b65..8fb52146f 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -19,12 +19,16 @@ #ifndef __CVC4__OPTIONS__OPTIONS_H #define __CVC4__OPTIONS__OPTIONS_H -#include <iostream> #include <fstream> +#include <ostream> #include <string> #include <vector> +#include "base/listener.h" +#include "base/modal_exception.h" #include "base/tls.h" +#include "options/language.h" +#include "options/printer_modes.h" #include "options/option_exception.h" namespace CVC4 { @@ -38,18 +42,90 @@ class CVC4_PUBLIC Options { /** The struct that holds all option values. */ options::OptionsHolder* d_holder; + /** The handler for the options of the theory. */ + options::OptionsHandler* d_handler; + /** The current Options in effect */ static CVC4_THREADLOCAL(Options*) s_current; + /** Listeners for options::forceLogicString being set. */ + ListenerCollection d_forceLogicListeners; + + /** Listeners for notifyBeforeSearch. */ + ListenerCollection d_beforeSearchListeners; + + /** Listeners for options::tlimit. */ + ListenerCollection d_tlimitListeners; + + /** Listeners for options::tlimit-per. */ + ListenerCollection d_tlimitPerListeners; + + /** Listeners for options::rlimit. */ + ListenerCollection d_rlimitListeners; + + /** Listeners for options::tlimit-per. */ + ListenerCollection d_rlimitPerListeners; + + /** Listeners for options::useTheoryList. */ + ListenerCollection d_useTheoryListListeners; + + /** 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; + + /** Listeners for options::replayFilename. */ + ListenerCollection d_setReplayFilenameListeners; + + + 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, options::OptionsHandler* handler); + void assign(T, std::string option, std::string value); /** Low-level assignment function for bool-valued options */ template <class T> - void assignBool(T, std::string option, bool value, options::OptionsHandler* handler); + void assignBool(T, std::string option, bool value); friend class options::OptionsHandler; + /** + * Options cannot be copied as they are given an explicit list of + * Listeners to respond to. + */ + Options(const Options& options) CVC4_UNDEFINED; + + /** + * Options cannot be assigned as they are given an explicit list of + * Listeners to respond to. + */ + Options& operator=(const Options& options) CVC4_UNDEFINED; + + static std::string formatThreadOptionException(const std::string& option); + + static const size_t s_maxoptlen = 128; + static const unsigned s_preemptAdditional = 6; + public: class CVC4_PUBLIC OptionsScope { private: @@ -76,10 +152,14 @@ public: } Options(); - Options(const Options& options); ~Options(); - Options& operator=(const Options& options); + /** + * Copies the value of the options stored in OptionsHolder into the current + * Options object. + * This does not copy the listeners in the Options object. + */ + void copyValues(const Options& options); /** * Set the value of the given option. Use of this default @@ -93,11 +173,99 @@ public: T::you_are_trying_to_assign_to_a_read_only_option; } + /** + * Set the value of the given option by key. + */ + void setOption(const std::string& key, const std::string& optionarg) + throw(OptionException, ModalException); + + /** Get the value of the given option. Const access only. */ template <class T> const typename T::type& operator[](T) const; /** + * Gets the value of the given option by key and returns value as a string. + */ + std::string getOption(const std::string& key) const + throw(OptionException); + + // Get accessor functions. + InputLanguage getInputLanguage() const; + InstFormatMode getInstFormatMode() const; + OutputLanguage getOutputLanguage() const; + bool getCheckProofs() const; + bool getContinuedExecution() const; + bool getDumpInstantiations() const; + bool getDumpModels() const; + bool getDumpProofs() const; + bool getDumpSynth() const; + bool getDumpUnsatCores() const; + bool getEarlyExit() const; + bool getFallbackSequential() const; + bool getFilesystemAccess() const; + bool getForceNoLimitCpuWhileDump() const; + bool getHelp() const; + bool getIncrementalParallel() const; + bool getIncrementalSolving() const; + bool getInteractive() const; + bool getInteractivePrompt() const; + bool getLanguageHelp() const; + bool getMemoryMap() const; + bool getParseOnly() const; + bool getProduceModels() const; + bool getProof() const; + bool getSegvSpin() const; + bool getSemanticChecks() const; + bool getStatistics() const; + bool getStatsEveryQuery() const; + bool getStatsHideZeros() const; + bool getStrictParsing() const; + bool getTearDownIncremental() const; + bool getVersion() const; + bool getWaitToJoin() const; + const std::string& getForceLogicString() const; + const std::vector<std::string>& getThreadArgv() const; + int getSharingFilterByLength() const; + int getThreadId() const; + int getVerbosity() const; + std::istream* getIn() const; + std::ostream* getErr(); + std::ostream* getOut(); + std::ostream* getOutConst() const; // TODO: Remove this. + std::string getBinaryName() const; + std::string getReplayInputFilename() const; + unsigned getParseStep() const; + unsigned getThreadStackSize() const; + unsigned getThreads() const; + + + // TODO: Document these. + void setCeGuidedInst(bool); + void setDumpSynth(bool); + void setInputLanguage(InputLanguage); + void setInteractive(bool); + void setOut(std::ostream*); + void setOutputLanguage(OutputLanguage); + void setSharingFilterByLength(int length); + void setThreadId(int); + + bool wasSetByUserCeGuidedInst() const; + bool wasSetByUserDumpSynth() const; + bool wasSetByUserEarlyExit() const; + bool wasSetByUserForceLogicString() const; + bool wasSetByUserIncrementalSolving() const; + bool wasSetByUserInteractive() const; + bool wasSetByUserThreadStackSize() const; + bool wasSetByUserThreads() const; + + // Static accessor functions. + // TODO: Document these. + static int currentGetSharingFilterByLength(); + static int currentGetThreadId(); + static std::ostream* currentGetOut(); + + /** * Returns true iff the value of the given option was set * by the user via a command-line option or SmtEngine::setOption(). * (Options::set() is low-level and doesn't count.) Returns false @@ -150,13 +318,216 @@ public: * The return value is what's left of the command line (that is, the * non-option arguments). */ - std::vector<std::string> parseOptions(int argc, char* argv[], options::OptionsHandler* handler) throw(OptionException); + std::vector<std::string> parseOptions(int argc, char* argv[]) + throw(OptionException); /** * Get the setting for all options. */ std::vector< std::vector<std::string> > getOptions() const throw(); + + /** + * 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::forceLogic 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* registerForceLogicListener( + Listener* listener, bool notifyIfSet); + + /** + * Registers a listener for options::tlimit 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* registerTlimitListener( + Listener* listener, bool notifyIfSet); + + /** + * Registers a listener for options::tlimit-per 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* registerTlimitPerListener( + Listener* listener, bool notifyIfSet); + + + /** + * Registers a listener for options::rlimit 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* registerRlimitListener( + Listener* listener, bool notifyIfSet); + + /** + * Registers a listener for options::rlimit-per 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* registerRlimitPerListener( + Listener* listener, bool notifyIfSet); + + /** + * Registers a listener for options::useTheoryList 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* registerUseTheoryListListener( + Listener* listener, bool notifyIfSet); + + + /** + * 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); + + /** + * Registers a listener for options::replayLogFilename 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* registerSetReplayLogFilename( + Listener* listener, bool notifyIfSet); + + /** Sends a std::flush to getErr(). */ + void flushErr(); + + /** Sends a std::flush to getOut(). */ + void flushOut(); + };/* class Options */ }/* CVC4 namespace */ |