summaryrefslogtreecommitdiff
path: root/src/options/options.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/options/options.h')
-rw-r--r--src/options/options.h310
1 files changed, 0 insertions, 310 deletions
diff --git a/src/options/options.h b/src/options/options.h
deleted file mode 100644
index 324850c43..000000000
--- a/src/options/options.h
+++ /dev/null
@@ -1,310 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- * Tim King, Morgan Deters, Paul Meng
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Global (command-line, set-option, ...) parameters for SMT.
- */
-
-#include "cvc5_public.h"
-
-#ifndef CVC5__OPTIONS__OPTIONS_H
-#define CVC5__OPTIONS__OPTIONS_H
-
-#include <iosfwd>
-#include <memory>
-#include <string>
-#include <vector>
-
-#include "base/listener.h"
-#include "cvc5_export.h"
-#include "options/language.h"
-#include "options/printer_modes.h"
-
-namespace cvc5 {
-
-namespace api {
-class Solver;
-}
-namespace options {
- struct OptionsHolder;
- class OptionsHandler;
- } // namespace options
-
-class OptionsListener;
-
-class CVC5_EXPORT Options
-{
- friend api::Solver;
- /** The struct that holds all option values. */
- std::unique_ptr<options::OptionsHolder> d_holder;
-
- /** The handler for the options of the theory. */
- options::OptionsHandler* d_handler;
-
- /** The current Options in effect */
- static thread_local Options* s_current;
-
- /** Low-level assignment function for options */
- template <class T>
- 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);
-
- friend class options::OptionsHandler;
-
- /**
- * Options cannot be copied as they are given an explicit list of
- * Listeners to respond to.
- */
- Options(const Options& options) = delete;
-
- /**
- * Options cannot be assigned as they are given an explicit list of
- * Listeners to respond to.
- */
- Options& operator=(const Options& options) = delete;
-
- static std::string formatThreadOptionException(const std::string& option);
-
-public:
- class OptionsScope
- {
- private:
- Options* d_oldOptions;
- public:
- OptionsScope(Options* newOptions) :
- d_oldOptions(Options::s_current)
- {
- Options::s_current = newOptions;
- }
- ~OptionsScope(){
- Options::s_current = d_oldOptions;
- }
- };
-
- /** Return true if current Options are null */
- static inline bool isCurrentNull() {
- return s_current == NULL;
- }
-
- /** Get the current Options in effect */
- static inline Options& current() {
- return *s_current;
- }
-
- Options(OptionsListener* ol = nullptr);
- ~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. Uses `ref()`, which causes a
- * compile-time error if the given option is read-only.
- */
- template <class T>
- void set(T t, const typename T::type& val) {
- ref(t) = val;
- }
-
- /**
- * Set the default value of the given option. Is equivalent to calling `set()`
- * if `wasSetByUser()` returns false. Uses `ref()`, which causes a compile-time
- * error if the given option is read-only.
- */
- template <class T>
- void setDefault(T t, const typename T::type& val)
- {
- if (!wasSetByUser(t))
- {
- ref(t) = val;
- }
- }
-
- /**
- * Get a non-const reference to the value of the given option. Causes a
- * compile-time error if the given option is read-only. Writeable options
- * specialize this template with a real implementation.
- */
- template <class T>
- typename T::type& ref(T) {
- // Flag a compile-time error.
- T::you_are_trying_to_get_nonconst_access_to_a_read_only_option;
- // Ensure the compiler does not complain about the return value.
- return *static_cast<typename T::type*>(nullptr);
- }
-
- /**
- * Set the value of the given option by key.
- *
- * Throws OptionException or ModalException on failures.
- */
- void setOption(const std::string& key, const std::string& optionarg);
-
- /** 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.
- *
- * Throws OptionException on failures, such as key not being the name of an
- * option.
- */
- std::string getOption(const std::string& key) const;
-
- // Get accessor functions.
- InputLanguage getInputLanguage() const;
- options::InstFormatMode getInstFormatMode() const;
- OutputLanguage getOutputLanguage() const;
- bool getUfHo() const;
- bool getDumpInstantiations() const;
- bool getDumpModels() const;
- bool getDumpProofs() const;
- bool getDumpUnsatCores() const;
- bool getEarlyExit() const;
- bool getFilesystemAccess() const;
- bool getForceNoLimitCpuWhileDump() const;
- bool getHelp() const;
- bool getIncrementalSolving() const;
- bool getInteractive() const;
- bool getInteractivePrompt() const;
- bool getLanguageHelp() const;
- bool getMemoryMap() const;
- bool getParseOnly() const;
- bool getProduceModels() const;
- bool getSegvSpin() const;
- bool getSemanticChecks() const;
- bool getStatistics() const;
- bool getStatsEveryQuery() const;
- bool getStrictParsing() const;
- int getTearDownIncremental() const;
- uint64_t getCumulativeTimeLimit() const;
- bool getVersion() const;
- const std::string& getForceLogicString() 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;
-
- // TODO: Document these.
- void setInputLanguage(InputLanguage);
- void setInteractive(bool);
- void setOut(std::ostream*);
- void setOutputLanguage(OutputLanguage);
-
- bool wasSetByUserEarlyExit() const;
- bool wasSetByUserForceLogicString() const;
- bool wasSetByUserIncrementalSolving() const;
- bool wasSetByUserInteractive() const;
-
- // Static accessor functions.
- // TODO: Document these.
- 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
- * otherwise.
- */
- template <class T>
- bool wasSetByUser(T) const;
-
- /**
- * Get a description of the command-line flags accepted by
- * parseOptions. The returned string will be escaped so that it is
- * suitable as an argument to printf. */
- std::string getDescription() const;
-
- /**
- * Print overall command-line option usage message, prefixed by
- * "msg"---which could be an error message causing the usage
- * output in the first place, e.g. "no such option --foo"
- */
- static void printUsage(const std::string msg, std::ostream& out);
-
- /**
- * Print command-line option usage message for only the most-commonly
- * used options. The message is prefixed by "msg"---which could be
- * an error message causing the usage output in the first place, e.g.
- * "no such option --foo"
- */
- static void printShortUsage(const std::string msg, std::ostream& out);
-
- /** Print help for the --lang command line option */
- static void printLanguageHelp(std::ostream& out);
-
- /**
- * Initialize the Options object options based on the given
- * command-line arguments given in argc and argv. The return value
- * is what's left of the command line (that is, the non-option
- * arguments).
- *
- * This function uses getopt_long() and is not thread safe.
- *
- * Throws OptionException on failures.
- *
- * Preconditions: options and argv must be non-null.
- */
- static std::vector<std::string> parseOptions(Options* options,
- int argc,
- char* argv[]);
-
- /**
- * Get the setting for all options.
- */
- std::vector<std::vector<std::string> > getOptions() const;
-
- /** Set the generic listener associated with this class to ol */
- void setListener(OptionsListener* ol);
-
- /** Sends a std::flush to getErr(). */
- void flushErr();
-
- /** Sends a std::flush to getOut(). */
- void flushOut();
-
- private:
- /** Pointer to the options listener, if one exists */
- OptionsListener* d_olisten;
- /**
- * Helper method for setOption, updates this object for setting the given
- * option.
- */
- void setOptionInternal(const std::string& key, const std::string& optionarg);
- /**
- * Internal procedure for implementing the parseOptions function.
- * Initializes the options object based on the given command-line
- * arguments. The command line arguments are stored in argc/argv.
- * Nonoptions are stored into nonoptions.
- *
- * This is not thread safe.
- *
- * Throws OptionException on failures.
- *
- * Preconditions: options, extender and nonoptions are non-null.
- */
- void parseOptionsRecursive(int argc,
- char* argv[],
- std::vector<std::string>* nonoptions);
-}; /* class Options */
-
-} // namespace cvc5
-
-#endif /* CVC5__OPTIONS__OPTIONS_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback