1 /******************************************************************************
2 * Top contributors (to current version):
3 * Tim King, Gereon Kremer, Andrew Reynolds
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
13 * Global (command-line, set-option, ...) parameters for SMT.
16 #include "options/options_public.h"
19 #include "base/check.h"
20 #include "base/output.h"
21 #include "options/options_handler.h"
22 #include "options/options_listener.h"
23 #include "options/options.h"
24 #include "options/uf_options.h"
32 namespace cvc5::options
{
34 bool getUfHo(const Options
& opts
) { return opts
.uf
.ufHo
; }
36 /** Set a given Options* as "current" just for a particular scope. */
41 OptionsGuard(Options
** field
, Options
* opts
) :
49 };/* class OptionsGuard */
53 * This is a default handler for options of built-in C++ type. This
54 * template is really just a helper for the handleOption() template,
55 * below. Variants of this template handle numeric and non-numeric,
56 * integral and non-integral, signed and unsigned C++ types.
57 * handleOption() makes sure to instantiate the right one.
59 * This implements default behavior when e.g. an option is
60 * unsigned but the user specifies a negative argument; etc.
62 template <class T
, bool is_numeric
, bool is_integer
>
63 struct OptionHandler
{
64 static T
handle(const std::string
& option
, const std::string
& flag
, const std::string
& optionarg
);
65 };/* struct OptionHandler<> */
67 /** Variant for integral C++ types */
69 struct OptionHandler
<T
, true, true> {
70 static bool stringToInt(T
& t
, const std::string
& str
) {
71 std::istringstream
ss(str
);
74 return !(ss
.fail() || ss
.get(tmp
));
77 static bool containsMinus(const std::string
& str
) {
78 return str
.find('-') != std::string::npos
;
81 static T
handle(const std::string
& option
, const std::string
& flag
, const std::string
& optionarg
) {
84 bool success
= stringToInt(i
, optionarg
);
87 throw OptionException(flag
+ ": failed to parse "+ optionarg
+
88 " as an integer of the appropriate type.");
91 // Depending in the platform unsigned numbers with '-' signs may parse.
92 // Reject these by looking for any minus if it is not signed.
93 if( (! std::numeric_limits
<T
>::is_signed
) && containsMinus(optionarg
) ) {
94 // unsigned type but user gave negative argument
95 throw OptionException(flag
+ " requires a nonnegative argument");
96 } else if(i
< std::numeric_limits
<T
>::min()) {
97 // negative overflow for type
99 ss
<< flag
<< " requires an argument >= "
100 << std::numeric_limits
<T
>::min();
101 throw OptionException(ss
.str());
102 } else if(i
> std::numeric_limits
<T
>::max()) {
103 // positive overflow for type
104 std::stringstream ss
;
105 ss
<< flag
<< " requires an argument <= "
106 << std::numeric_limits
<T
>::max();
107 throw OptionException(ss
.str());
112 // if(std::numeric_limits<T>::is_signed) {
113 // return T(i.getLong());
115 // return T(i.getUnsignedLong());
117 } catch(std::invalid_argument
&) {
118 // user gave something other than an integer
119 throw OptionException(flag
+ " requires an integer argument");
122 };/* struct OptionHandler<T, true, true> */
124 /** Variant for numeric but non-integral C++ types */
126 struct OptionHandler
<T
, true, false> {
127 static T
handle(const std::string
& option
, const std::string
& flag
, const std::string
& optionarg
) {
128 std::stringstream
inss(optionarg
);
132 // we didn't consume the whole string (junk at end)
133 throw OptionException(flag
+ " requires a numeric argument");
136 if(! std::numeric_limits
<T
>::is_signed
&& r
< 0.0) {
137 // unsigned type but user gave negative value
138 throw OptionException(flag
+ " requires a nonnegative argument");
139 } else if(r
< -std::numeric_limits
<T
>::max()) {
140 // negative overflow for type
141 std::stringstream ss
;
142 ss
<< flag
<< " requires an argument >= "
143 << -std::numeric_limits
<T
>::max();
144 throw OptionException(ss
.str());
145 } else if(r
> std::numeric_limits
<T
>::max()) {
146 // positive overflow for type
147 std::stringstream ss
;
148 ss
<< flag
<< " requires an argument <= "
149 << std::numeric_limits
<T
>::max();
150 throw OptionException(ss
.str());
155 };/* struct OptionHandler<T, true, false> */
157 /** Variant for non-numeric C++ types */
159 struct OptionHandler
<T
, false, false> {
160 static T
handle(const std::string
& option
, const std::string
& flag
, const std::string
& optionarg
) {
161 T::unsupported_handleOption_call___please_write_me
;
162 // The above line causes a compiler error if this version of the template
163 // is ever instantiated (meaning that a specialization is missing). So
164 // don't worry about the segfault in the next line, the "return" is only
165 // there to keep the compiler from giving additional, distracting errors
169 };/* struct OptionHandler<T, false, false> */
171 /** Specialization for ManagedErr */
173 struct OptionHandler
<ManagedErr
, false, false>
175 static ManagedErr
handle(const std::string
& option
,
176 const std::string
& flag
,
177 const std::string
& optionarg
)
184 /** Specialization for ManagedIn */
186 struct OptionHandler
<ManagedIn
, false, false>
188 static ManagedIn
handle(const std::string
& option
,
189 const std::string
& flag
,
190 const std::string
& optionarg
)
197 /** Specialization for ManagedOut */
199 struct OptionHandler
<ManagedOut
, false, false>
201 static ManagedOut
handle(const std::string
& option
,
202 const std::string
& flag
,
203 const std::string
& optionarg
)
211 /** Handle an option of type T in the default way. */
213 T
handleOption(const std::string
& option
, const std::string
& flag
, const std::string
& optionarg
) {
214 return OptionHandler
<T
, std::numeric_limits
<T
>::is_specialized
, std::numeric_limits
<T
>::is_integer
>::handle(option
, flag
, optionarg
);
217 /** Handle an option of type std::string in the default way. */
219 std::string handleOption
<std::string
>(const std::string
& option
, const std::string
& flag
, const std::string
& optionarg
) {
223 bool handleOption
<bool>(const std::string
& option
, const std::string
& flag
, const std::string
& optionarg
) {
224 Assert(optionarg
== "true" || optionarg
== "false");
225 return optionarg
== "true";
228 std::string
get(const Options
& options
, const std::string
& name
)
230 Trace("options") << "Options::getOption(" << name
<< ")" << std::endl
;
232 $
{getoption_handlers
}$
234 throw OptionException("Unrecognized option key or setting: " + name
);
237 void setInternal(Options
& opts
, const std::string
& name
,
238 const std::string
& optionarg
)
241 $
{setoption_handlers
}$
246 throw OptionException("Unrecognized option key or setting: " + name
);
248 Trace("options") << "user assigned option " << name
<< " = " << optionarg
<< std::endl
;
251 void set(Options
& opts
, const std::string
& name
, const std::string
& optionarg
)
254 Trace("options") << "setOption(" << name
<< ", " << optionarg
<< ")"
256 // first update this object
257 setInternal(opts
, name
, optionarg
);
260 std::vector
<std::string
> getNames()
264 $
{options_all_names
}$
269 #if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE)
270 #define DO_SEMANTIC_CHECKS_BY_DEFAULT false
271 #else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
272 #define DO_SEMANTIC_CHECKS_BY_DEFAULT true
273 #endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
275 OptionInfo
getInfo(const Options
& opts
, const std::string
& name
)
280 return OptionInfo
{name
, {}, false, OptionInfo::VoidInfo
{}};
283 #undef DO_SEMANTIC_CHECKS_BY_DEFAULT
285 } // namespace cvc5::options