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.



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

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 .