diff options
Diffstat (limited to 'src/options/options.h')
-rw-r--r-- | src/options/options.h | 150 |
1 files changed, 150 insertions, 0 deletions
diff --git a/src/options/options.h b/src/options/options.h new file mode 100644 index 000000000..a3abdd54b --- /dev/null +++ b/src/options/options.h @@ -0,0 +1,150 @@ +/********************* */ +/*! \file options.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: taking, cconway + ** Minor contributors (to current version): dejan + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Global (command-line, set-option, ...) parameters for SMT. + ** + ** Global (command-line, set-option, ...) parameters for SMT. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__OPTIONS__OPTIONS_H +#define __CVC4__OPTIONS__OPTIONS_H + +#include <iostream> +#include <fstream> +#include <string> + +#include "util/exception.h" +#include "util/language.h" +#include "util/tls.h" + +namespace CVC4 { + +namespace options { + class OptionsHolder; +}/* CVC4::options namespace */ + +class ExprStream; +class NodeManager; +class NodeManagerScope; +class SmtEngine; + +/** Class representing an option-parsing exception. */ +class CVC4_PUBLIC OptionException : public CVC4::Exception { +public: + OptionException(const std::string& s) throw() : + CVC4::Exception("Error in option parsing: " + s) { + } +};/* class OptionException */ + +class CVC4_PUBLIC Options { + /** The struct that holds all option values. */ + options::OptionsHolder* d_holder; + + /** The current Options in effect */ + static CVC4_THREADLOCAL(Options*) s_current; + + /** Low-level assignment function for options */ + template <class T> + void assign(T, std::string option, std::string value, SmtEngine* smt); + /** Low-level assignment function for bool-valued options */ + template <class T> + void assignBool(T, std::string option, bool value, SmtEngine* smt); + + friend class NodeManager; + friend class NodeManagerScope; + friend class SmtEngine; + +public: + + /** Get the current Options in effect */ + static inline Options& current() { + return *s_current; + } + + Options(); + Options(const Options& options); + ~Options(); + + /** + * Set the value of the given option. Use of this default + * implementation causes a compile-time error; write-able + * options specialize this template with a real implementation. + */ + template <class T> + void set(T, const typename T::type&) { + // Flag a compile-time error. Write-able options specialize + // this template to provide an implementation. + T::you_are_trying_to_assign_to_a_read_only_option; + } + + /** Get the value of the given option. Const access only. */ + template <class T> + const typename T::type& operator[](T) const; + + /** + * 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 based on the given command-line arguments. + */ + int parseOptions(int argc, char* argv[]) throw(OptionException); + + /** + * Set the output language based on the given string. + */ + void setOutputLanguage(const char* str) throw(OptionException); + + /** + * Set the input language based on the given string. + */ + void setInputLanguage(const char* str) throw(OptionException); + +};/* class Options */ + +}/* CVC4 namespace */ + +#include "options/base_options.h" + +#endif /* __CVC4__OPTIONS__OPTIONS_H */ |