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 .