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 some description about a particular 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

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.

Public Members

std::string name: The option name

std::vector<std::string> aliases: The option name aliases

bool setByUser: Whether the option was explicitly set by the user

bool isExpert: Whether this is an expert option

bool isRegular: Whether this is a regular 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 std::ostream.