OptionInfo

This class encapsulates all the information associated with a configuration option. It can be retrieved via cvc5::Solver::getOptionInfo() and allows to query any configuration information associated with an option.

• class cvc5::OptionInfo

• std::ostream& cvc5::operator<< (std::ostream& out, const OptionInfo& info)

struct OptionInfo

Holds information about a specific option, including its name, its aliases, whether the option was explicitly set by the user, and information concerning its value. It can be obtained via Solver::getOptionInfo() and allows for a more detailed inspection of options than Solver::getOption(). The valueInfo member holds any of the following alternatives:

• VoidInfo if the option holds no value (or the value has no native type)

• ValueInfo if the option is of type bool or std::string, holds the current value and the default value.

• NumberInfo 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.

If the option has a special type that is not covered by the above alternatives, the valueInfo holds a VoidInfo. Some options, that are expected to be used by frontends (e.g., input and output streams) can also be accessed using Solver::getDriverOptions().

Public Types

using OptionInfoVariant = std::variant<VoidInfo, ValueInfo<bool>, ValueInfo<std::string>, NumberInfo<int64_t>, NumberInfo<uint64_t>, NumberInfo<double>, ModeInfo>

Possible types for valueInfo.

Public Functions

OptionInfo &operator=(OptionInfo &&info)

Move assignment operator.

bool boolValue() const

Get the current value as a bool.

Note

Asserts that valueInfo holds a bool.

Returns:

The current value as a bool.

std::string stringValue() const

Get the current value as a std::string.

Note

Asserts that valueInfo holds a std::string.

Returns:

The current value as a std::string.

int64_t intValue() const

Get the current value as an int64_t.

Note

Asserts that valueInfo holds an int64_t.

Returns:

The current value as a int64_t.

uint64_t uintValue() const

Get the current value as a uint64_t.

Note

Asserts that valueInfo holds a uint64_t.

Returns:

The current value as a uint64_t.

double doubleValue() const

Obtain the current value as a double.

Note

Asserts that valueInfo holds a double.

Returns:

The current value as a double.

std::string toString() const

Get a string representation of an option info.

Returns:

The string representation.

Public Members

std::string name

The option name

std::vector<std::string> aliases

The option name aliases

std::vector<std::string> noSupports

The features not supported with this

bool setByUser

Whether the option was explicitly set by the user

bool isExpert

True if the option is an expert option

Warning

This field is deprecated and replaced by category. It will be removed in a future release.

bool isRegular

True if the option is a regular option

Warning

This field is deprecated and replaced by category. It will be removed in a future release.

modes::OptionCategory category

The category of this option.

OptionInfoVariant valueInfo

The option value information

struct ModeInfo

Information for mode option values.

Public Members

std::string defaultValue

The default value.

std::string currentValue

The current value.

std::vector<std::string> modes

The possible modes.

template<typename T>
struct NumberInfo

Information for numeric values. T can be int64_t, uint64_t or double.

Public Members

T defaultValue

The default value.

T currentValue

The current value.

std::optional<T> minimum

The optional minimum value.

std::optional<T> maximum

The optional maximum value.

template<typename T>
struct ValueInfo

Basic information for option values. T can be bool or std::string.

Public Members

T defaultValue

The default value.

T currentValue

The current value.

struct VoidInfo

Has no value information.

std::ostream &cvc5::operator<<(std::ostream &os, const OptionInfo &oi)

Print an OptionInfo object to an output stream.

Parameters:

• os – The output stream.

• oi – The option info.

Returns:

The output stream.