1 /********************* */
4 ** Original author: mdeters
5 ** Major contributors: none
6 ** Minor contributors (to current version): dejan, cconway
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2012 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Global (command-line, set-option, ...) parameters for SMT.
14 ** Global (command-line, set-option, ...) parameters for SMT.
17 #include "cvc4_public.h"
19 #ifndef __CVC4__OPTIONS__OPTIONS_H
20 #define __CVC4__OPTIONS__OPTIONS_H
27 #include "options/option_exception.h"
28 #include "util/language.h"
35 }/* CVC4::options namespace */
39 class NodeManagerScope
;
42 class CVC4_PUBLIC Options
{
43 /** The struct that holds all option values. */
44 options::OptionsHolder
* d_holder
;
46 /** The current Options in effect */
47 static CVC4_THREADLOCAL(Options
*) s_current
;
49 /** Low-level assignment function for options */
51 void assign(T
, std::string option
, std::string value
, SmtEngine
* smt
);
52 /** Low-level assignment function for bool-valued options */
54 void assignBool(T
, std::string option
, bool value
, SmtEngine
* smt
);
56 friend class NodeManager
;
57 friend class NodeManagerScope
;
58 friend class SmtEngine
;
62 /** Get the current Options in effect */
63 static inline Options
& current() {
68 Options(const Options
& options
);
72 * Set the value of the given option. Use of this default
73 * implementation causes a compile-time error; write-able
74 * options specialize this template with a real implementation.
77 void set(T
, const typename
T::type
&) {
78 // Flag a compile-time error. Write-able options specialize
79 // this template to provide an implementation.
80 T::you_are_trying_to_assign_to_a_read_only_option
;
83 /** Get the value of the given option. Const access only. */
85 const typename
T::type
& operator[](T
) const;
88 * Returns true iff the value of the given option was set
89 * by the user via a command-line option or SmtEngine::setOption().
90 * (Options::set() is low-level and doesn't count.) Returns false
94 bool wasSetByUser(T
) const;
97 * Get a description of the command-line flags accepted by
98 * parseOptions. The returned string will be escaped so that it is
99 * suitable as an argument to printf. */
100 std::string
getDescription() const;
103 * Print overall command-line option usage message, prefixed by
104 * "msg"---which could be an error message causing the usage
105 * output in the first place, e.g. "no such option --foo"
107 static void printUsage(const std::string msg
, std::ostream
& out
);
110 * Print command-line option usage message for only the most-commonly
111 * used options. The message is prefixed by "msg"---which could be
112 * an error message causing the usage output in the first place, e.g.
113 * "no such option --foo"
115 static void printShortUsage(const std::string msg
, std::ostream
& out
);
117 /** Print help for the --lang command line option */
118 static void printLanguageHelp(std::ostream
& out
);
121 * Initialize the options based on the given command-line arguments.
122 * The return value is what's left of the command line (that is, the
123 * non-option arguments).
125 std::vector
<std::string
> parseOptions(int argc
, char* argv
[]) throw(OptionException
);
127 };/* class Options */
129 }/* CVC4 namespace */
131 #include "options/base_options.h"
133 #endif /* __CVC4__OPTIONS__OPTIONS_H */