Package io.github.cvc5

Class OptionInfo

java.lang.Object
io.github.cvc5.OptionInfo
public class OptionInfo extends Object
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. The valueInfo member holds any of the following alternatives:
  • OptionInfo.VoidInfo if the option holds no value (or the value has no native type)
  • OptionInfo.ValueInfo if the option is of type boolean or String, holds the current value and the default value.
  • OptionInfo.NumberInfo if the option is of type BigInteger or double, holds the current and default value, as well as the minimum and maximum.
  • OptionInfo.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 booleanValue(), stringValue(), intValue(), and doubleValue(). They assert that the option has the respective type and return the current value.

  • Field Details

    • pointer

      protected long pointer
      The raw native pointer value.

  • Method Details

    • toString

      public String toString()
      Return a string representation of the pointer.
      Returns:
      a string representation of the pointer

    • toString

      protected String toString(long pointer)
      Return a string representation of the specified native pointer.

      Subclasses must implement this method to convert the native pointer into a meaningful string.

      Parameters:
      pointer - the native pointer
      Returns:
      A string representation of this OptionInfo.

    • getName

      public String getName()
      Get the name of the option.
      Returns:
      The option name.

    • getAliases

      public String[] getAliases()
      Get the option name aliases.
      Returns:
      An array of alias strings associated with the option.

    • getSetByUser

      public boolean getSetByUser()
      Determine if the option was set by the user.
      Returns:
      True if the option was set by the user.

    • getBaseInfo

      public OptionInfo.BaseInfo getBaseInfo()
      Get base info.
      Returns:
      The base info.

    • booleanValue

      public boolean booleanValue()
      Obtain the current value as a Boolean. Asserts that valueInfo holds a Boolean.
      Returns:
      The Boolean value.

    • stringValue

      public String stringValue()
      Obtain the current value as a string. Asserts that valueInfo holds a string.
      Returns:
      The string value.

    • intValue

      public BigInteger intValue()
      Obtain the current value as as int. Asserts that valueInfo holds an int.
      Returns:
      The integer value.

    • doubleValue

      public double doubleValue()
      Obtain the current value as a double. Asserts that valueInfo holds a double.
      Returns:
      The double value.

    • getCategory

      public OptionCategory getCategory()
      Get the category of the option.
      Returns:
      The option category.

    • getPointer

      public long getPointer()
      Return the raw native pointer.

      Every native call obtains the pointers of the objects it uses through this method, so that using an object after its native resource has been released raises an exception instead of crashing the JVM.

      Returns:
      the pointer value
      Throws:
      IllegalStateException - if the native resource of this object has been released, e.g., via deletePointer()

    • deletePointer

      public void deletePointer()
      Free the native resource associated with this pointer.

      Native resources are freed automatically once the Java object is no longer reachable. This method frees the native resource immediately instead; afterwards, using the object raises an IllegalStateException. It must be called from the thread that is using the associated term manager. Calling it more than once has no further effect.