io.github.cvc5

Class OptionInfo.NumberInfo<T>

java.lang.Object

io.github.cvc5.OptionInfo.BaseInfo

io.github.cvc5.OptionInfo.ValueInfo<T>

io.github.cvc5.OptionInfo.NumberInfo<T>

Enclosing class:

OptionInfo

public class OptionInfo.NumberInfo<T>
extends OptionInfo.ValueInfo<T>

Default value, current value, minimum and maximum of a numeric value

Constructor Summary

Constructors

Constructor and Description
NumberInfo(T defaultValue, T currentValue, T minimum, T maximum)

Method Summary

Modifier and Type	Method and Description
T	getMaximum()
T	getMinimum()

Methods inherited from class io.github.cvc5.OptionInfo.ValueInfo

getCurrentValue, getDefaultValue

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

NumberInfo

public NumberInfo(T defaultValue,
                  T currentValue,
                  T minimum,
                  T maximum)

Method Detail

getMinimum

public T getMinimum()

getMaximum

public T getMaximum()