This PR adds api::Solver::getOptionInfo() that returns information about a single option, including its name, aliases, current and default value and its domain.
run: |
make -j${{ env.num_proc }} install
echo -e "#include <cvc5/cvc5.h>\nint main() { cvc5::api::Solver s; return 0; }" > /tmp/test.cpp
- g++ -std=c++11 /tmp/test.cpp -I install/include -L install/lib -lcvc5
+ g++ -std=c++17 /tmp/test.cpp -I install/include -L install/lib -lcvc5
working-directory: build
- name: Python Install Check
* class :ref:`api/cpp/op:op`
+ * class :ref:`api/cpp/optioninfo:optioninfo`
+
* class :ref:`api/cpp/result:result`
* enum :cpp:enum:`UnknownExplanation <cvc5::api::Result::UnknownExplanation>`
grammar
kind
op
+ optioninfo
result
roundingmode
solver
--- /dev/null
+OptionInfo
+==========
+
+.. doxygenstruct:: cvc5::api::OptionInfo
+ :project: cvc5
+ :members:
project(cvc5-examples)
-set(CMAKE_CXX_STANDARD 11)
+set(CMAKE_CXX_STANDARD 17)
enable_testing()
CVC5_API_TRY_CATCH_END;
}
+// Supports a visitor from a list of lambdas
+// Taken from https://en.cppreference.com/w/cpp/utility/variant/visit
+template<class... Ts> struct overloaded : Ts... { using Ts::operator()...; };
+template<class... Ts> overloaded(Ts...) -> overloaded<Ts...>;
+
+bool OptionInfo::boolValue() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_RECOVERABLE_CHECK(std::holds_alternative<ValueInfo<bool>>(valueInfo))
+ << name << " is not a bool option";
+ //////// all checks before this line
+ return std::get<ValueInfo<bool>>(valueInfo).currentValue;
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+std::string OptionInfo::stringValue() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_RECOVERABLE_CHECK(
+ std::holds_alternative<ValueInfo<std::string>>(valueInfo))
+ << name << " is not a string option";
+ //////// all checks before this line
+ return std::get<ValueInfo<std::string>>(valueInfo).currentValue;
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+int64_t OptionInfo::intValue() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_RECOVERABLE_CHECK(
+ std::holds_alternative<NumberInfo<int64_t>>(valueInfo))
+ << name << " is not an int option";
+ //////// all checks before this line
+ return std::get<NumberInfo<int64_t>>(valueInfo).currentValue;
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+uint64_t OptionInfo::uintValue() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_RECOVERABLE_CHECK(
+ std::holds_alternative<NumberInfo<uint64_t>>(valueInfo))
+ << name << " is not a uint option";
+ //////// all checks before this line
+ return std::get<NumberInfo<uint64_t>>(valueInfo).currentValue;
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+double OptionInfo::doubleValue() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_RECOVERABLE_CHECK(
+ std::holds_alternative<NumberInfo<double>>(valueInfo))
+ << name << " is not a double option";
+ //////// all checks before this line
+ return std::get<NumberInfo<double>>(valueInfo).currentValue;
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
+std::ostream& operator<<(std::ostream& os, const OptionInfo& oi)
+{
+ os << "OptionInfo{ " << oi.name;
+ if (oi.setByUser)
+ {
+ os << " | set by user";
+ }
+ if (!oi.aliases.empty())
+ {
+ container_to_stream(os, oi.aliases, ", ", "", ", ");
+ }
+ auto printNum = [&os](const std::string& type, const auto& vi) {
+ os << " | " << type << " | " << vi.currentValue << " | default "
+ << vi.defaultValue;
+ if (vi.minimum || vi.maximum)
+ {
+ os << " |";
+ if (vi.minimum)
+ {
+ os << " " << *vi.minimum << " <=";
+ }
+ os << " x";
+ if (vi.maximum)
+ {
+ os << " <= " << *vi.maximum;
+ }
+ }
+ };
+ std::visit(overloaded{
+ [&os](const OptionInfo::VoidInfo& vi) { os << " | void"; },
+ [&os](const OptionInfo::ValueInfo<bool>& vi) {
+ os << " | bool | " << vi.currentValue << " | default "
+ << vi.defaultValue;
+ },
+ [&os](const OptionInfo::ValueInfo<std::string>& vi) {
+ os << " | string | " << vi.currentValue << " | default "
+ << vi.defaultValue;
+ },
+ [&printNum](const OptionInfo::NumberInfo<int64_t>& vi) {
+ printNum("int64_t", vi);
+ },
+ [&printNum](const OptionInfo::NumberInfo<uint64_t>& vi) {
+ printNum("uint64_t", vi);
+ },
+ [&printNum](const OptionInfo::NumberInfo<double>& vi) {
+ printNum("double", vi);
+ },
+ [&os](const OptionInfo::ModeInfo& vi) {
+ os << " | mode | " << vi.currentValue << " | default "
+ << vi.defaultValue << " | modes: ";
+ container_to_stream(os, vi.modes, "", "", ", ");
+ },
+ },
+ oi.valueInfo);
+ os << " }";
+ return os;
+}
+
std::vector<std::string> Solver::getOptionNames() const
{
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_TRY_CATCH_END;
}
+OptionInfo Solver::getOptionInfo(const std::string& option) const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ //////// all checks before this line
+ auto info = options::getInfo(d_smtEngine->getOptions(), option);
+ return std::visit(
+ overloaded{
+ [&info](const options::OptionInfo::VoidInfo& vi) {
+ return OptionInfo{info.name,
+ info.aliases,
+ info.setByUser,
+ OptionInfo::VoidInfo{}};
+ },
+ [&info](const options::OptionInfo::ValueInfo<bool>& vi) {
+ return OptionInfo{
+ info.name,
+ info.aliases,
+ info.setByUser,
+ OptionInfo::ValueInfo<bool>{vi.defaultValue, vi.currentValue}};
+ },
+ [&info](const options::OptionInfo::ValueInfo<std::string>& vi) {
+ return OptionInfo{info.name,
+ info.aliases,
+ info.setByUser,
+ OptionInfo::ValueInfo<std::string>{
+ vi.defaultValue, vi.currentValue}};
+ },
+ [&info](const options::OptionInfo::NumberInfo<int64_t>& vi) {
+ return OptionInfo{
+ info.name,
+ info.aliases,
+ info.setByUser,
+ OptionInfo::NumberInfo<int64_t>{
+ vi.defaultValue, vi.currentValue, vi.minimum, vi.maximum}};
+ },
+ [&info](const options::OptionInfo::NumberInfo<uint64_t>& vi) {
+ return OptionInfo{
+ info.name,
+ info.aliases,
+ info.setByUser,
+ OptionInfo::NumberInfo<uint64_t>{
+ vi.defaultValue, vi.currentValue, vi.minimum, vi.maximum}};
+ },
+ [&info](const options::OptionInfo::NumberInfo<double>& vi) {
+ return OptionInfo{
+ info.name,
+ info.aliases,
+ info.setByUser,
+ OptionInfo::NumberInfo<double>{
+ vi.defaultValue, vi.currentValue, vi.minimum, vi.maximum}};
+ },
+ [&info](const options::OptionInfo::ModeInfo& vi) {
+ return OptionInfo{info.name,
+ info.aliases,
+ info.setByUser,
+ OptionInfo::ModeInfo{
+ vi.defaultValue, vi.currentValue, vi.modes}};
+ },
+ },
+ info.valueInfo);
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
DriverOptions Solver::getDriverOptions() const { return DriverOptions(*this); }
std::vector<Term> Solver::getUnsatAssumptions(void) const
#include <map>
#include <memory>
+#include <optional>
#include <set>
#include <sstream>
#include <string>
#include <unordered_map>
#include <unordered_set>
+#include <variant>
#include <vector>
#include "api/cpp/cvc5_kind.h"
const Solver& d_solver;
};
+/**
+ * Holds some description about a particular option, including its name, its
+ * aliases, whether the option was explcitly set by the user, and information
+ * concerning its value. The `valueInfo` member holds any of the following
+ * alternatives:
+ * - VoidInfo if the option holds no value (or the value has no native type)
+ * - ValueInfo<T> if the option is of type bool or std::string, holds the
+ * current value and the default value.
+ * - NumberInfo<T> if the option is of type int64_t, uint64_t or double, holds
+ * the current and default value, as well as the minimum and maximum.
+ * - ModeInfo if the option is a mode option, holds the current and default
+ * values, as well as a list of valid modes.
+ * Additionally, this class provides convenience functions to obtain the
+ * current value of an option in a type-safe manner using boolValue(),
+ * stringValue(), intValue(), uintValue() and doubleValue(). They assert that
+ * the option has the respective type and return the current value.
+ */
+struct CVC5_EXPORT OptionInfo
+{
+ /** Has no value information */
+ struct VoidInfo {};
+ /** Has the current and the default value */
+ template <typename T>
+ struct ValueInfo
+ {
+ T defaultValue;
+ T currentValue;
+ };
+ /** Default value, current value, minimum and maximum of a numeric value */
+ template <typename T>
+ struct NumberInfo
+ {
+ T defaultValue;
+ T currentValue;
+ std::optional<T> minimum;
+ std::optional<T> maximum;
+ };
+ /** Default value, current value and choices of a mode option */
+ struct ModeInfo
+ {
+ std::string defaultValue;
+ std::string currentValue;
+ std::vector<std::string> modes;
+ };
+
+ /** The option name */
+ std::string name;
+ /** The option name aliases */
+ std::vector<std::string> aliases;
+ /** Whether the option was explicitly set by the user */
+ bool setByUser;
+ /** The option value information */
+ std::variant<VoidInfo,
+ ValueInfo<bool>,
+ ValueInfo<std::string>,
+ NumberInfo<int64_t>,
+ NumberInfo<uint64_t>,
+ NumberInfo<double>,
+ ModeInfo>
+ valueInfo;
+ /** Obtain the current value as a bool. Asserts that valueInfo holds a bool.
+ */
+ bool boolValue() const;
+ /** Obtain the current value as a string. Asserts that valueInfo holds a
+ * string. */
+ std::string stringValue() const;
+ /** Obtain the current value as as int. Asserts that valueInfo holds an int.
+ */
+ int64_t intValue() const;
+ /** Obtain the current value as a uint. Asserts that valueInfo holds a uint.
+ */
+ uint64_t uintValue() const;
+ /** Obtain the current value as a double. Asserts that valueInfo holds a
+ * double. */
+ double doubleValue() const;
+};
+
+/**
+ * Print a `OptionInfo` object to an ``std::ostream``.
+ */
+std::ostream& operator<<(std::ostream& os, const OptionInfo& oi) CVC5_EXPORT;
+
/* -------------------------------------------------------------------------- */
/* Statistics */
/* -------------------------------------------------------------------------- */
*/
std::vector<std::string> getOptionNames() const;
+ /**
+ * Get some information about the given option. Check the `OptionInfo` class
+ * for more details on which information is available.
+ * @return information about the given option
+ */
+ OptionInfo getOptionInfo(const std::string& option) const;
+
/**
* Get the driver options, which provide access to options that can not be
* communicated properly via getOption() and getOptionInfo().
short = "o"
long = "output=TAG"
type = "OutputTag"
+ default = "NONE"
handler = "enableOutputTag"
category = "regular"
help = "Enable output tag."
help_mode = "Output tags."
+[[option.mode.NONE]]
+ name = "none"
[[option.mode.INST]]
name = "inst"
help = "print instantiations during solving"
res.append(val.format(opt['help_mode']))
res.append(val.format(''))
for k, v in opt['modes'].items():
+ if v == '':
+ continue
res.append(val.format(':{}: {}'.format(k, v)))
res.append(' ')
for value, attrib in option.mode.items():
assert len(attrib) == 1
attrib = attrib[0]
+ if 'help' not in attrib:
+ continue
if value == option.default and attrib['name'] != "default":
text.append('+ {} (default)'.format(attrib['name']))
else:
text.append('+ {}'.format(attrib['name']))
- if 'help' in attrib:
- text.extend(' {}'.format(x) for x in wrapper.wrap(attrib['help']))
+ text.extend(' {}'.format(x) for x in wrapper.wrap(attrib['help']))
return '\n '.join('"{}\\n"'.format(x) for x in text)
getopt_short = [] # short options for getopt_long
getopt_long = [] # long options for getopt_long
options_getall = [] # options for options::getAll()
- options_getoptions = [] # options for Options::getOptions()
+ options_get_info = [] # code for getOptionInfo()
options_handler = [] # option handler calls
options_names = set() # option names
help_common = [] # help text for all common options
cond = ' || '.join(
['name == "{}"'.format(x) for x in sorted(names)])
+ # Generate code for getOptionInfo
+ if option.name:
+ constr = None
+ fmt = {
+ 'type': option.type,
+ 'value': 'opts.{}.{}'.format(module.id, option.name),
+ 'default': option.default if option.default else '{}()'.format(option.type),
+ 'minimum': option.minimum if option.minimum else '{}',
+ 'maximum': option.maximum if option.maximum else '{}',
+ }
+ if option.type in ['bool', 'std::string']:
+ constr = 'OptionInfo::ValueInfo<{type}>{{{default}, {value}}}'.format(**fmt)
+ elif option.type == 'double' or is_numeric_cpp_type(option.type):
+ constr = 'OptionInfo::NumberInfo<{type}>{{{default}, {value}, {minimum}, {maximum}}}'.format(**fmt)
+ elif option.mode:
+ values = ', '.join(map(lambda s: '"{}"'.format(s), option.mode.keys()))
+ assert(option.default)
+ constr = 'OptionInfo::ModeInfo{{"{default}", {value}, {{ {modes} }}}}'.format(**fmt, modes=values)
+ else:
+ constr = 'OptionInfo::VoidInfo{}'
+ if option.alias:
+ alias = ', '.join(map(lambda s: '"{}"'.format(s), option.alias))
+ else:
+ alias = ''
+ options_get_info.append('if ({}) return OptionInfo{{"{}", {{{alias}}}, opts.{}.{}WasSetByUser, {}}};'.format(cond, long_get_option(option.long), module.id, option.name, constr, alias=alias))
+
if setoption_handlers:
setoption_handlers.append(' }} else if ({}) {{'.format(cond))
else:
'options_short': ''.join(getopt_short),
'options_getall': '\n '.join(options_getall),
'options_all_names': options_all_names,
+ 'options_get_info': '\n '.join(sorted(options_get_info)),
'getoption_handlers': '\n'.join(getoption_handlers),
'setoption_handlers': '\n'.join(setoption_handlers),
}
option = Option(attribs)
if option.mode and not option.help_mode:
perr(filename, 'defines modes but no help_mode', option)
+ if option.mode and not option.default:
+ perr(filename, "mode option has no default", option)
if option.mode and option.default and \
option.default not in option.mode.keys():
perr(filename,
#define CVC5__OPTIONS__OPTIONS_PUBLIC_H
#include <iosfwd>
+#include <optional>
+#include <sstream>
#include <string>
+#include <variant>
#include <vector>
#include "cvc5_export.h"
*/
std::vector<std::string> getNames() CVC5_EXPORT;
+/**
+ * Represents information we can provide about a particular option. It contains
+ * its name and aliases, the current value and the default value as well as
+ * type-specific information like its range (if it is a number) or the choices
+ * (if it is a mode option).
+ */
+struct CVC5_EXPORT OptionInfo
+{
+ std::string name;
+ std::vector<std::string> aliases;
+ bool setByUser;
+
+ /** No information about the options value */
+ struct VoidInfo
+ {
+ };
+ /** Default value and current value */
+ template <typename T>
+ struct ValueInfo
+ {
+ T defaultValue;
+ T currentValue;
+ };
+ /** Default value, current value, minimum and maximum of a numeric value */
+ template <typename T>
+ struct NumberInfo
+ {
+ T defaultValue;
+ T currentValue;
+ std::optional<T> minimum;
+ std::optional<T> maximum;
+ };
+ /** Default value, current value and choices of a mode option */
+ struct ModeInfo
+ {
+ std::string defaultValue;
+ std::string currentValue;
+ std::vector<std::string> modes;
+
+ template <typename T>
+ ModeInfo(const std::string& def, T cur, const std::vector<std::string>& m)
+ : defaultValue(def), modes(m)
+ {
+ std::stringstream ss;
+ ss << cur;
+ currentValue = ss.str();
+ }
+ };
+
+ /** A variant over all possible option value information */
+ std::variant<VoidInfo,
+ ValueInfo<bool>,
+ ValueInfo<std::string>,
+ NumberInfo<int64_t>,
+ NumberInfo<uint64_t>,
+ NumberInfo<double>,
+ ModeInfo>
+ valueInfo;
+};
+
+/**
+ * Retrieves information about an option specified by its name from an options
+ * object. Note that `opts` is only used to retrieve the current value.
+ */
+OptionInfo getInfo(const Options& opts, const std::string& name) CVC5_EXPORT;
+
} // namespace cvc5::options
#endif
std::vector<std::vector<std::string> > getAll(const Options& opts)
{
std::vector<std::vector<std::string>> res;
-
-${options_getall}$
-
+ // clang-format off
+ ${options_getall}$
+ // clang-format on
return res;
}
std::vector<std::string> getNames()
{
return {
-${options_all_names}$
+ // clang-format off
+ ${options_all_names}$
+ // clang-format on
};
}
+#if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE)
+#define DO_SEMANTIC_CHECKS_BY_DEFAULT false
+#else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
+#define DO_SEMANTIC_CHECKS_BY_DEFAULT true
+#endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
+
+OptionInfo getInfo(const Options& opts, const std::string& name)
+{
+ // clang-format off
+ ${options_get_info}$
+ // clang-format on
+ return OptionInfo{name, {}, false, OptionInfo::VoidInfo{}};
+}
+
+#undef DO_SEMANTIC_CHECKS_BY_DEFAULT
+
} // namespace cvc5::options
ASSERT_EQ(std::find(names.begin(), names.end(), "foobar"), names.end());
}
+TEST_F(TestApiBlackSolver, getOptionInfo)
+{
+ {
+ auto info = d_solver.getOptionInfo("verbose");
+ ASSERT_EQ(info.name, "verbose");
+ ASSERT_EQ(info.aliases, std::vector<std::string>{});
+ ASSERT_TRUE(std::holds_alternative<api::OptionInfo::VoidInfo>(info.valueInfo));
+ }
+ {
+ // int64 type with default
+ api::OptionInfo info = d_solver.getOptionInfo("verbosity");
+ EXPECT_EQ("verbosity", info.name);
+ EXPECT_EQ(std::vector<std::string>{}, info.aliases);
+ EXPECT_TRUE(std::holds_alternative<OptionInfo::NumberInfo<int64_t>>(info.valueInfo));
+ auto numInfo = std::get<OptionInfo::NumberInfo<int64_t>>(info.valueInfo);
+ EXPECT_EQ(0, numInfo.defaultValue);
+ EXPECT_EQ(0, numInfo.currentValue);
+ EXPECT_FALSE(numInfo.minimum || numInfo.maximum);
+ ASSERT_EQ(info.intValue(), 0);
+ }
+ {
+ auto info = d_solver.getOptionInfo("random-freq");
+ ASSERT_EQ(info.name, "random-freq");
+ ASSERT_EQ(info.aliases, std::vector<std::string>{"random-frequency"});
+ ASSERT_TRUE(std::holds_alternative<api::OptionInfo::NumberInfo<double>>(info.valueInfo));
+ auto ni = std::get<api::OptionInfo::NumberInfo<double>>(info.valueInfo);
+ ASSERT_EQ(ni.currentValue, 0.0);
+ ASSERT_EQ(ni.defaultValue, 0.0);
+ ASSERT_TRUE(ni.minimum && ni.maximum);
+ ASSERT_EQ(*ni.minimum, 0.0);
+ ASSERT_EQ(*ni.maximum, 1.0);
+ ASSERT_EQ(info.doubleValue(), 0.0);
+ }
+ {
+ // mode option
+ api::OptionInfo info = d_solver.getOptionInfo("output");
+ EXPECT_EQ("output", info.name);
+ EXPECT_EQ(std::vector<std::string>{}, info.aliases);
+ EXPECT_TRUE(std::holds_alternative<OptionInfo::ModeInfo>(info.valueInfo));
+ auto modeInfo = std::get<OptionInfo::ModeInfo>(info.valueInfo);
+ EXPECT_EQ("NONE", modeInfo.defaultValue);
+ EXPECT_EQ("OutputTag::NONE", modeInfo.currentValue);
+ std::vector<std::string> modes{"NONE", "INST", "SYGUS", "TRIGGER"};
+ EXPECT_EQ(modes, modeInfo.modes);
+ }
+}
+
TEST_F(TestApiBlackSolver, getUnsatAssumptions1)
{
d_solver.setOption("incremental", "false");
projects / cvc5.git / commitdiff