from .._utils import final, flatten
from . import ast, dsl, ir
from typing import overload, TYPE_CHECKING
-if TYPE_CHECKING:
+if TYPE_CHECKING: # :nobr:
# make typechecker check final
- from typing import final
+ from typing import final # :nocov:
__all__ = [
- # FIXME
+ 'RNA',
+ 'RNE',
+ 'ROUND_DEFAULT',
+ 'ROUND_NEAREST_TIES_TO_AWAY',
+ 'ROUND_NEAREST_TIES_TO_EVEN',
+ 'ROUND_TOWARD_NEGATIVE',
+ 'ROUND_TOWARD_POSITIVE',
+ 'ROUND_TOWARD_ZERO',
+ 'RTN',
+ 'RTP',
+ 'RTZ',
+ 'RoundingModeEnum',
+ 'SmtBitVec',
+ 'SmtBitVecAdd',
+ 'SmtBitVecAnd',
+ 'SmtBitVecConcat',
+ 'SmtBitVecConst',
+ 'SmtBitVecDiv',
+ 'SmtBitVecExtract',
+ 'SmtBitVecITE',
+ 'SmtBitVecInput',
+ 'SmtBitVecLShift',
+ 'SmtBitVecLt',
+ 'SmtBitVecMul',
+ 'SmtBitVecNeg',
+ 'SmtBitVecNot',
+ 'SmtBitVecOr',
+ 'SmtBitVecRShift',
+ 'SmtBitVecRem',
+ 'SmtBitVecToNat',
+ 'SmtBitVecToSignal',
+ 'SmtBitVecXor',
+ 'SmtBool',
+ 'SmtBoolAnd',
+ 'SmtBoolConst',
+ 'SmtBoolITE',
+ 'SmtBoolImplies',
+ 'SmtBoolNot',
+ 'SmtBoolOr',
+ 'SmtBoolXor',
+ 'SmtDistinct',
+ 'SmtFloatingPoint',
+ 'SmtFloatingPointAbs',
+ 'SmtFloatingPointAdd',
+ 'SmtFloatingPointDiv',
+ 'SmtFloatingPointEq',
+ 'SmtFloatingPointFma',
+ 'SmtFloatingPointFromBits',
+ 'SmtFloatingPointFromFP',
+ 'SmtFloatingPointFromParts',
+ 'SmtFloatingPointFromReal',
+ 'SmtFloatingPointFromSignedBV',
+ 'SmtFloatingPointFromUnsignedBV',
+ 'SmtFloatingPointGE',
+ 'SmtFloatingPointGt',
+ 'SmtFloatingPointITE',
+ 'SmtFloatingPointIsInfinite',
+ 'SmtFloatingPointIsNaN',
+ 'SmtFloatingPointIsNegative',
+ 'SmtFloatingPointIsNormal',
+ 'SmtFloatingPointIsPositive',
+ 'SmtFloatingPointIsSubnormal',
+ 'SmtFloatingPointIsZero',
+ 'SmtFloatingPointLE',
+ 'SmtFloatingPointLt',
+ 'SmtFloatingPointMax',
+ 'SmtFloatingPointMin',
+ 'SmtFloatingPointMul',
+ 'SmtFloatingPointNaN',
+ 'SmtFloatingPointNeg',
+ 'SmtFloatingPointNegInfinity',
+ 'SmtFloatingPointNegZero',
+ 'SmtFloatingPointPosInfinity',
+ 'SmtFloatingPointPosZero',
+ 'SmtFloatingPointRem',
+ 'SmtFloatingPointRoundToIntegral',
+ 'SmtFloatingPointSqrt',
+ 'SmtFloatingPointSub',
+ 'SmtFloatingPointToReal',
+ 'SmtFloatingPointToSignedBV',
+ 'SmtFloatingPointToUnsignedBV',
+ 'SmtITE',
+ 'SmtInt',
+ 'SmtIntAbs',
+ 'SmtIntAdd',
+ 'SmtIntConst',
+ 'SmtIntEuclidDiv',
+ 'SmtIntEuclidRem',
+ 'SmtIntGE',
+ 'SmtIntGt',
+ 'SmtIntITE',
+ 'SmtIntLE',
+ 'SmtIntLt',
+ 'SmtIntMul',
+ 'SmtIntNeg',
+ 'SmtIntSub',
+ 'SmtIntToReal',
+ 'SmtNatToBitVec',
+ 'SmtReal',
+ 'SmtRealAdd',
+ 'SmtRealConst',
+ 'SmtRealDiv',
+ 'SmtRealGE',
+ 'SmtRealGt',
+ 'SmtRealITE',
+ 'SmtRealIsInt',
+ 'SmtRealLE',
+ 'SmtRealLt',
+ 'SmtRealMul',
+ 'SmtRealNeg',
+ 'SmtRealSub',
+ 'SmtRealToInt',
+ 'SmtRoundingMode',
+ 'SmtRoundingModeConst',
+ 'SmtRoundingModeITE',
+ 'SmtSame',
+ 'SmtSort',
+ 'SmtSortBitVec',
+ 'SmtSortBool',
+ 'SmtSortFloat128',
+ 'SmtSortFloat16',
+ 'SmtSortFloat32',
+ 'SmtSortFloat64',
+ 'SmtSortFloatingPoint',
+ 'SmtSortInt',
+ 'SmtSortReal',
+ 'SmtSortRoundingMode',
+ 'SmtValue',
]
@dataclass(frozen=True, unsafe_hash=True, eq=True)
-class SmtSort(meta=ABCMeta):
+class SmtSort(metaclass=ABCMeta):
@abstractmethod
def _smtlib2_expr(self, expr_state):
- return str(...)
+ return str(...) # :nocov:
@abstractmethod
- @staticmethod
- def _ite_class():
- return SmtITE
+ def _ite_class(self):
+ return SmtITE # :nocov:
@final
@dataclass(frozen=True, unsafe_hash=False, eq=False)
-class SmtValue(ast.DUID, meta=ABCMeta):
+class SmtValue(ast.DUID, metaclass=ABCMeta):
@abstractmethod
- @staticmethod
- def sort():
- return SmtSort()
+ def sort(self):
+ return SmtSort() # type: ignore :nocov:
@abstractmethod
def _smtlib2_expr(self, expr_state):
- return str(...)
+ return str(...) # :nocov:
def same(self, other, *rest):
return SmtSame(self, other, *rest)
def sort():
return SmtSortBool()
- def __new__(cls, value=None):
- if cls is not SmtBool:
- assert value is None
- return super().__new__(cls)
- assert isinstance(value, bool)
- return SmtBoolConst(value)
+ @staticmethod
+ def make(value):
+ value = ast.Value.cast(value)
+ if isinstance(value, ast.Const):
+ return SmtBoolConst(bool(value.value))
+ return SmtBitVecInput(value).bool()
# type deduction:
@overload
- def ite(self, then_v: "SmtBool", else_v: "SmtBool") -> "SmtBoolITE": ...
+ def ite(self, then_v: "SmtBool",
+ else_v: "SmtBool") -> "SmtBoolITE": ... # :nocov:
+
@overload
- def ite(self, then_v: "SmtInt", else_v: "SmtInt") -> "SmtIntITE": ...
+ def ite(self, then_v: "SmtInt",
+ else_v: "SmtInt") -> "SmtIntITE": ... # :nocov:
+
@overload
- def ite(self, then_v: "SmtReal", else_v: "SmtReal") -> "SmtRealITE": ...
+ def ite(self, then_v: "SmtReal",
+ else_v: "SmtReal") -> "SmtRealITE": ... # :nocov:
@overload
def ite(self, then_v: "SmtBitVec", else_v: "SmtBitVec") -> "SmtBitVecITE":
- ...
+ ... # :nocov:
@overload
def ite(self, then_v: "SmtRoundingMode",
- else_v: "SmtRoundingMode") -> "SmtRoundingModeITE": ...
+ else_v: "SmtRoundingMode") -> "SmtRoundingModeITE": ... # :nocov:
@overload
- def ite(self, then_v: "SmtFloatingPoint",
- else_v: "SmtFloatingPoint") -> "SmtFloatingPointITE": ...
+ def ite(self, then_v: "SmtFloatingPoint", else_v: "SmtFloatingPoint"
+ ) -> "SmtFloatingPointITE": ... # :nocov:
- def ite(self, then_v, else_v):
- return SmtITE(self, then_v, else_v)
+ def ite(self, then_v, else_v): # type: ignore
+ return SmtITE.make(self, then_v, else_v)
def __invert__(self):
return SmtBoolNot(self)
return SmtBoolImplies(self, *rest)
def to_bit_vec(self):
- return self.ite(SmtBitVec(1, width=1),
- SmtBitVec(0, width=1))
+ return self.ite(SmtBitVecConst(1, width=1),
+ SmtBitVecConst(0, width=1))
def to_signal(self):
return self.to_bit_vec().to_signal()
then_v: SmtValue
else_v: SmtValue
- def __new__(cls, cond, then_v, else_v):
+ # type deduction:
+ @overload
+ @staticmethod
+ def make(cond: "SmtBool", then_v: "SmtBool",
+ else_v: "SmtBool") -> "SmtBoolITE": ... # :nocov:
+
+ @overload
+ @staticmethod
+ def make(cond: "SmtBool", then_v: "SmtInt",
+ else_v: "SmtInt") -> "SmtIntITE": ... # :nocov:
+
+ @overload
+ @staticmethod
+ def make(cond: "SmtBool", then_v: "SmtReal",
+ else_v: "SmtReal") -> "SmtRealITE": ... # :nocov:
+
+ @overload
+ @staticmethod
+ def make(cond: "SmtBool", then_v: "SmtBitVec",
+ else_v: "SmtBitVec") -> "SmtBitVecITE": ... # :nocov:
+
+ @overload
+ @staticmethod
+ def make(cond: "SmtBool", then_v: "SmtRoundingMode",
+ else_v: "SmtRoundingMode") -> "SmtRoundingModeITE": ... # :nocov:
+
+ @overload
+ @staticmethod
+ def make(cond: "SmtBool", then_v: "SmtFloatingPoint",
+ else_v: "SmtFloatingPoint") -> "SmtFloatingPointITE":
+ ... # :nocov:
+
+ @staticmethod
+ def make(cond, then_v, else_v):
+ assert isinstance(cond, SmtBool)
+ assert isinstance(then_v, SmtValue)
+ assert isinstance(else_v, SmtValue)
+ sort = then_v.sort()
+ assert sort == else_v.sort()
+ return sort._ite_class()(cond, then_v, else_v) # type: ignore
+
+ def __init__(self, cond, then_v, else_v):
assert isinstance(cond, SmtBool)
assert isinstance(then_v, SmtValue)
assert isinstance(else_v, SmtValue)
sort = then_v.sort()
assert sort == else_v.sort()
- if cls is SmtITE:
- return sort._ite_class()(cond, then_v, else_v)
- return super().__new__(cls)
+ assert isinstance(self, sort._ite_class())
+ object.__setattr__(self, "cond", cond)
+ object.__setattr__(self, "then_v", then_v)
+ object.__setattr__(self, "else_v", else_v)
def _smtlib2_expr(self, expr_state):
assert isinstance(expr_state, _ExprState)
@dataclass(frozen=True, unsafe_hash=False, eq=False)
-class _SmtNArySameSort(SmtValue):
+class _SmtNAry(SmtValue):
inputs: "tuple[SmtValue, ...]"
@abstractmethod
def _smtlib2_expr_op(self, expr_state):
- assert isinstance(expr_state, _ExprState)
- return str(...)
+ assert isinstance(expr_state, _ExprState) # :nocov:
+ return str(...) # :nocov:
def _expected_input_class(self):
return SmtValue
for i in inputs:
assert isinstance(i, self._expected_input_class())
- assert i.sort == self.input_sort, "all input sorts must match"
+ assert i.sort() == self.input_sort, "all input sorts must match"
@property
def input_sort(self):
- return self.inputs[0].sort
+ return self.inputs[0].sort()
def _smtlib2_expr(self, expr_state):
assert isinstance(expr_state, _ExprState)
@abstractmethod
def _smtlib2_expr_op(self, expr_state):
- assert isinstance(expr_state, _ExprState)
- return str(...)
+ assert isinstance(expr_state, _ExprState) # :nocov:
+ return str(...) # :nocov:
def _expected_input_class(self):
return SmtValue
@abstractmethod
def _smtlib2_expr_op(self, expr_state):
- assert isinstance(expr_state, _ExprState)
- return str(...)
+ assert isinstance(expr_state, _ExprState) # :nocov:
+ return str(...) # :nocov:
def _expected_input_class(self):
return SmtValue
- def _expected_input_lhs_class(self):
- return self._expected_input_class()
-
- def _expected_input_rhs_class(self):
- return self._expected_input_class()
+ @property
+ def input_sort(self):
+ return self.lhs.sort()
def __init__(self, lhs, rhs):
object.__setattr__(self, "lhs", lhs)
object.__setattr__(self, "rhs", rhs)
- assert isinstance(lhs, self._expected_input_lhs_class())
- assert isinstance(rhs, self._expected_input_rhs_class())
+ assert isinstance(lhs, self._expected_input_class())
+ assert isinstance(rhs, self._expected_input_class())
+ assert lhs.sort() == rhs.sort()
def _smtlib2_expr(self, expr_state):
assert isinstance(expr_state, _ExprState)
@final
@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
-class SmtSame(_SmtNArySameSort, SmtBool):
+class SmtSame(_SmtNAry, SmtBool):
def _smtlib2_expr_op(self, expr_state):
assert isinstance(expr_state, _ExprState)
return "="
@final
@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
-class SmtDistinct(_SmtNArySameSort, SmtBool):
+class SmtDistinct(_SmtNAry, SmtBool):
def _smtlib2_expr_op(self, expr_state):
assert isinstance(expr_state, _ExprState)
return "distinct"
@dataclass(frozen=True, unsafe_hash=False, eq=False)
-class _SmtBoolNAryMinBinary(_SmtNArySameSort, SmtBool):
+class _SmtBoolNAryMinBinary(_SmtNAry, SmtBool):
inputs: "tuple[SmtBool, ...]"
def _expected_input_class(self):
return SmtBool
- def __new__(cls, *inputs):
- return super().__new__(cls)
-
def __init__(self, *inputs):
super().__init__(*inputs)
assert len(self.inputs) >= 2, "not enough inputs"
then_v: SmtBool
else_v: SmtBool
- def __new__(cls, cond, then_v, else_v):
+ def __init__(self, cond, then_v, else_v):
assert isinstance(cond, SmtBool)
assert isinstance(then_v, SmtBool)
assert isinstance(else_v, SmtBool)
- return SmtITE.__new__(cls, cond, then_v, else_v)
+ super().__init__(cond, then_v, else_v)
@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
def sort():
return SmtSortReal()
- def __new__(cls, value=None):
- if cls is not SmtReal:
- assert value is None
- return super().__new__(cls)
+ @staticmethod
+ def make(value):
if isinstance(value, SmtInt):
return SmtIntToReal(value)
assert isinstance(value, Rational), ("value must be a rational "
"floats aren't yet supported.")
return SmtRealConst(value)
- def __init__(self, value=None):
- # __init__ for IDE type checker
- # value != None already handled by __new__
- assert value is None, "invalid argument"
- return super().__init__()
-
def __neg__(self):
return SmtRealNeg(self)
return SmtRealGE(self, other)
def __abs__(self):
- return self.__lt__(SmtReal(0)).ite(-self, self)
+ return self.__lt__(SmtRealConst(0)).ite(-self, self)
def __floor__(self):
return SmtRealToInt(self)
def __trunc__(self):
- return self.__lt__(SmtReal(0)).ite(-(-self).__floor__(),
- self.__floor__())
+ return self.__lt__(SmtRealConst(0)).ite(-(-self).__floor__(),
+ self.__floor__())
def __ceil__(self):
return -(-self).__floor__()
@dataclass(frozen=True, unsafe_hash=False, eq=False)
-class _SmtRealNAryMinBinary(_SmtNArySameSort, SmtReal):
+class _SmtRealNAryMinBinary(_SmtNAry, SmtReal):
inputs: "tuple[SmtReal, ...]"
def _expected_input_class(self):
return SmtReal
- def __new__(cls, *inputs):
- return _SmtNArySameSort.__new__(cls)
-
def __init__(self, *inputs):
super().__init__(*inputs)
assert len(self.inputs) >= 2, "not enough inputs"
@dataclass(frozen=True, unsafe_hash=False, eq=False)
-class _SmtRealCompareOp(_SmtNArySameSort, SmtBool):
+class _SmtRealCompareOp(_SmtNAry, SmtBool):
inputs: "tuple[SmtReal, ...]"
def _expected_input_class(self):
return SmtReal
- def __new__(cls, *inputs):
- return _SmtNArySameSort.__new__(cls)
-
def __init__(self, *inputs):
super().__init__(*inputs)
assert len(self.inputs) >= 2, "not enough inputs"
then_v: SmtReal
else_v: SmtReal
- def __new__(cls, cond, then_v, else_v):
+ def __init__(self, cond, then_v, else_v):
assert isinstance(cond, SmtBool)
assert isinstance(then_v, SmtReal)
assert isinstance(else_v, SmtReal)
- return SmtITE.__new__(cls, cond, then_v, else_v)
+ super().__init__(cond, then_v, else_v)
@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
def sort():
return SmtSortInt()
- def __new__(cls, value=None):
- if cls is not SmtInt:
- assert value is None
- return super().__new__(cls)
+ @staticmethod
+ def make(value):
assert isinstance(value, int), "value must be an integer"
return SmtIntConst(value)
- def __init__(self, value=None):
- # __init__ for IDE type checker
- # value != None already handled by __new__
- assert value is None, "invalid argument"
- return super().__init__()
-
def __neg__(self):
return SmtIntNeg(self)
@dataclass(frozen=True, unsafe_hash=False, eq=False)
-class _SmtIntNAryMinBinary(_SmtNArySameSort, SmtInt):
+class _SmtIntNAryMinBinary(_SmtNAry, SmtInt):
inputs: "tuple[SmtInt, ...]"
def _expected_input_class(self):
return SmtInt
- def __new__(cls, *inputs):
- return _SmtNArySameSort.__new__(cls)
-
def __init__(self, *inputs):
super().__init__(*inputs)
assert len(self.inputs) >= 2, "not enough inputs"
@dataclass(frozen=True, unsafe_hash=False, eq=False)
-class _SmtIntCompareOp(_SmtNArySameSort, SmtBool):
+class _SmtIntCompareOp(_SmtNAry, SmtBool):
inputs: "tuple[SmtInt, ...]"
def _expected_input_class(self):
return SmtInt
- def __new__(cls, *inputs):
- return _SmtNArySameSort.__new__(cls)
-
def __init__(self, *inputs):
super().__init__(*inputs)
assert len(self.inputs) >= 2, "not enough inputs"
then_v: SmtInt
else_v: SmtInt
- def __new__(cls, cond, then_v, else_v):
+ def __init__(self, cond, then_v, else_v):
assert isinstance(cond, SmtBool)
assert isinstance(then_v, SmtInt)
assert isinstance(else_v, SmtInt)
- return SmtITE.__new__(cls, cond, then_v, else_v)
+ super().__init__(cond, then_v, else_v)
@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
return SmtSortBitVec(self.width)
@staticmethod
- def __make_bitvec(value=None, *, width=None):
+ def make(value=None, *, width=None):
if isinstance(value, int):
assert width is not None, "missing width"
assert isinstance(width, int) and width > 0, "invalid width"
assert width is None, "can't give both width and nMigen Value"
return SmtBitVecInput(value)
- def __new__(cls, *args, **kwargs):
- if cls is not SmtInt:
- return super().__new__(cls)
- return SmtBitVec.__make_bitvec(*args, **kwargs)
-
- def __init__(self, value=None, *, width=None):
- # __init__ for IDE type checker
- # value != None already handled by __new__
- assert value is None, "invalid argument"
+ def __init__(self, *, width=None):
assert isinstance(width, int) and width > 0, "invalid width"
object.__setattr__(self, "width", width)
super().__init__()
return SmtBoolNot(SmtBitVecLt(self, other))
def __abs__(self):
- return self.__lt__(SmtBitVec(0, width=self.width)).ite(-self, self)
+ lt = self.__lt__(SmtBitVecConst(0, width=self.width))
+ return lt.ite(-self, self)
def __and__(self, other):
return SmtBitVecAnd(self, other)
return SmtBitVecConcat(self[i] for i in r)
return SmtBitVecExtract(self, r)
+ def bool(self):
+ return self != SmtBitVecConst(0, width=self.width)
+
def to_signal(self):
return SmtBitVecToSignal(self)
def __init_subclass__(cls):
try:
_ = SmtBitVecConst
- except AttributeError:
+ except NameError:
# only possible when we're defining SmtBitVecConst
return
raise TypeError("subclassing SmtBitVecInput isn't supported")
- def __new__(cls, value):
+ @staticmethod
+ def make(value):
value = ast.Value.cast(value)
assert isinstance(value, ast.Value)
if isinstance(value, ast.Const):
- if cls is not SmtBitVecConst:
- return SmtBitVecConst(value)
- retval = super().__new__(cls)
- object.__setattr__(retval, "value", value)
- return retval
+ return SmtBitVecConst(value)
+ return SmtBitVecInput(value)
def __init__(self, value):
- # self.value assigned in __new__
+ value = ast.Value.cast(value)
+ assert isinstance(value, ast.Value)
+ object.__setattr__(self, "value", value)
super().__init__(width=self.value.shape().width) # type: ignore
def _smtlib2_expr(self, expr_state):
class SmtBitVecConst(SmtBitVecInput):
value: ast.Const
- def __new__(cls, value, *, width=None):
+ def __init__(self, value, *, width=None):
if isinstance(value, ast.Const):
assert width is None
# decompose -- needed since we switch to unsigned
assert isinstance(value, int), "value must be an integer"
assert isinstance(width, int) and width > 0, "invalid width"
value = ast.Const(value, ast.unsigned(width))
- return super().__new__(cls, value)
-
- def __init__(self, value, *, width=None):
- # rest of logic already handled by __new__
- super().__init__(self.value)
+ super().__init__(value)
def _smtlib2_expr(self, expr_state):
assert isinstance(expr_state, _ExprState)
@dataclass(frozen=True, unsafe_hash=False, eq=False)
-class _SmtBitVecNAryMinBinary(_SmtNArySameSort, SmtBitVec):
+class _SmtBitVecNAryMinBinary(_SmtNAry, SmtBitVec):
inputs: "tuple[SmtBitVec, ...]"
def _expected_input_class(self):
return SmtBitVec
- def __new__(cls, *inputs):
- return _SmtNArySameSort.__new__(cls)
-
def __init__(self, *inputs):
- _SmtNArySameSort.__init__(self, *inputs)
+ _SmtNAry.__init__(self, *inputs)
assert len(self.inputs) >= 2, "not enough inputs"
SmtBitVec.__init__(self, width=self.inputs[0].width)
@dataclass(frozen=True, unsafe_hash=False, eq=False)
-class _SmtBitVecCompareOp(_SmtNArySameSort, SmtBool):
- inputs: "tuple[SmtBitVec, ...]"
+class _SmtBitVecCompareOp(_SmtBinary, SmtBool):
+ lhs: SmtBitVec
+ rhs: SmtBitVec
+
+ def __init__(self, lhs, rhs):
+ _SmtBinary.__init__(self, lhs, rhs)
+ SmtBool.__init__(self)
def _expected_input_class(self):
return SmtBitVec
- def __new__(cls, *inputs):
- return _SmtNArySameSort.__new__(cls)
-
- def __init__(self, *inputs):
- super().__init__(*inputs)
- assert len(self.inputs) >= 2, "not enough inputs"
-
@final
@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
then_v: SmtBitVec
else_v: SmtBitVec
- def __new__(cls, cond, then_v, else_v):
+ def __init__(self, cond, then_v, else_v):
assert isinstance(cond, SmtBool)
assert isinstance(then_v, SmtBitVec)
assert isinstance(else_v, SmtBitVec)
- return SmtITE.__new__(cls, cond, then_v, else_v)
-
- def __init__(self, cond, then_v, else_v):
SmtITE.__init__(self, cond, then_v, else_v)
SmtBitVec.__init__(self, width=self.then_v.width)
@dataclass(frozen=True, unsafe_hash=False, eq=False)
class SmtRoundingMode(SmtValue):
- def __new__(cls, value=None):
- if cls is SmtRoundingMode:
- return SmtRoundingModeConst(value)
- return super().__new__(cls)
-
- def __init__(self, value=None):
- # __init__ for IDE type checker
- # value != None already handled by __new__
- assert value is None, "invalid argument"
- super().__init__()
+ @staticmethod
+ def make(value):
+ return SmtRoundingModeConst(value)
@staticmethod
def sort():
@final
@dataclass(frozen=True, unsafe_hash=False, eq=False)
-class SmtRoundingModeConst(SmtValue):
+class SmtRoundingModeConst(SmtRoundingMode):
value: RoundingModeEnum
- def __new__(cls, value):
- value = RoundingModeEnum(value)
+ def __new__(cls, *args, **kwargs):
+ value = RoundingModeEnum(*args, **kwargs)
try:
if value is RoundingModeEnum.RNE:
return RNE
else:
assert value is RoundingModeEnum.RTZ
return RTZ
- except AttributeError:
+ except NameError:
# instance not created yet
return super().__new__(cls)
+ def __init__(self, value):
+ assert isinstance(value, RoundingModeEnum)
+ object.__setattr__(self, "value", value)
+
def _smtlib2_expr(self, expr_state):
assert isinstance(expr_state, _ExprState)
return self.value._smtlib2_expr
then_v: SmtRoundingMode
else_v: SmtRoundingMode
- def __new__(cls, cond, then_v, else_v):
+ def __init__(self, cond, then_v, else_v):
assert isinstance(cond, SmtBool)
assert isinstance(then_v, SmtRoundingMode)
assert isinstance(else_v, SmtRoundingMode)
- return SmtITE.__new__(cls, cond, then_v, else_v)
+ super().__init__(cond, then_v, else_v)
@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
@staticmethod
def zero(*, sign=None, eb=None, sb=None, sort=None):
- return SmtFloatingPointZero(sign=sign, eb=eb, sb=sb, sort=sort)
+ if sign is None:
+ return SmtFloatingPointPosZero(eb=eb, sb=sb, sort=sort)
+ if isinstance(sign, SmtBitVec):
+ assert sign.width == 1, "invalid sign width"
+ sign = sign.bool()
+ assert isinstance(sign, SmtBool)
+ return sign.ite(SmtFloatingPointNegZero(eb=eb, sb=sb, sort=sort),
+ SmtFloatingPointPosZero(eb=eb, sb=sb, sort=sort))
+
+ @staticmethod
+ def neg_zero(*, eb=None, sb=None, sort=None):
+ return SmtFloatingPointNegZero(eb=eb, sb=sb, sort=sort)
@staticmethod
- def inf(*, sign=None, eb=None, sb=None, sort=None):
- return SmtFloatingPointInf(sign=sign, eb=eb, sb=sb, sort=sort)
+ def infinity(*, sign=None, eb=None, sb=None, sort=None):
+ if sign is None:
+ return SmtFloatingPointPosInfinity(eb=eb, sb=sb, sort=sort)
+ if isinstance(sign, SmtBitVec):
+ assert sign.width == 1, "invalid sign width"
+ sign = sign.bool()
+ assert isinstance(sign, SmtBool)
+ return sign.ite(SmtFloatingPointNegInfinity(eb=eb, sb=sb, sort=sort),
+ SmtFloatingPointPosInfinity(eb=eb, sb=sb, sort=sort))
+
+ @staticmethod
+ def neg_infinity(*, eb=None, sb=None, sort=None):
+ return SmtFloatingPointNegInfinity(eb=eb, sb=sb, sort=sort)
@staticmethod
def from_parts(*, sign, exponent, mantissa):
def sqrt(self, *, rm):
return SmtFloatingPointSqrt(self, rm=rm)
- def rem(self, other, *, rm):
- return SmtFloatingPointRem(self, other, rm=rm)
+ def rem(self, other):
+ return SmtFloatingPointRem(self, other)
def round_to_integral(self, *, rm):
return SmtFloatingPointRoundToIntegral(self, rm=rm)
return ~SmtFloatingPointEq(self, other)
def __lt__(self, other):
- return ~SmtFloatingPointLt(self, other)
+ return SmtFloatingPointLt(self, other)
def __le__(self, other):
- return ~SmtFloatingPointLE(self, other)
+ return SmtFloatingPointLE(self, other)
def __gt__(self, other):
- return ~SmtFloatingPointGt(self, other)
+ return SmtFloatingPointGt(self, other)
def __ge__(self, other):
- return ~SmtFloatingPointGE(self, other)
+ return SmtFloatingPointGE(self, other)
def is_normal(self):
return SmtFloatingPointIsNormal(self)
then_v: SmtFloatingPoint
else_v: SmtFloatingPoint
- def __new__(cls, cond, then_v, else_v):
+ def __init__(self, cond, then_v, else_v):
assert isinstance(cond, SmtBool)
assert isinstance(then_v, SmtFloatingPoint)
assert isinstance(else_v, SmtFloatingPoint)
- return SmtITE.__new__(cls, cond, then_v, else_v)
-
- def __init__(self, cond, then_v, else_v):
SmtITE.__init__(self, cond, then_v, else_v)
SmtFloatingPoint.__init__(self, sort=self.then_v.sort())
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointNaN(SmtFloatingPoint):
+ def _smtlib2_expr(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return f"(_ NaN {self.eb} {self.sb})"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointPosZero(SmtFloatingPoint):
+ def _smtlib2_expr(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return f"(_ +zero {self.eb} {self.sb})"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointNegZero(SmtFloatingPoint):
+ def _smtlib2_expr(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return f"(_ -zero {self.eb} {self.sb})"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointPosInfinity(SmtFloatingPoint):
+ def _smtlib2_expr(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return f"(_ +oo {self.eb} {self.sb})"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointNegInfinity(SmtFloatingPoint):
+ def _smtlib2_expr(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return f"(_ -oo {self.eb} {self.sb})"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False)
+class SmtFloatingPointFromParts(SmtFloatingPoint):
+ sign: SmtBitVec
+ exponent: SmtBitVec
+ mantissa: SmtBitVec
+
+ def __init__(self, sign, exponent, mantissa):
+ if isinstance(sign, SmtBool):
+ sign = sign.to_bit_vec()
+ assert isinstance(sign, SmtBitVec) and sign.width == 1
+ assert isinstance(exponent, SmtBitVec)
+ assert isinstance(mantissa, SmtBitVec)
+ super().__init__(eb=exponent.width, sb=mantissa.width + 1)
+
+ def _smtlib2_expr(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ sign = self.sign._smtlib2_expr(expr_state)
+ exponent = self.exponent._smtlib2_expr(expr_state)
+ mantissa = self.mantissa._smtlib2_expr(expr_state)
+ return f"(fp {sign} {exponent} {mantissa})"
+
+
+@dataclass(frozen=True, unsafe_hash=False, eq=False)
+class _SmtFloatingPointUnary(_SmtUnary, SmtFloatingPoint):
+ inp: SmtFloatingPoint
+
+ def __init__(self, inp):
+ assert isinstance(inp, SmtFloatingPoint)
+ _SmtUnary.__init__(self, inp)
+ SmtFloatingPoint.__init__(self, eb=inp.eb, sb=inp.sb)
+
+ def _expected_input_class(self):
+ return SmtFloatingPoint
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointAbs(_SmtFloatingPointUnary):
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.abs"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointNeg(_SmtFloatingPointUnary):
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.neg"
+
+
+@dataclass(frozen=True, unsafe_hash=False, eq=False)
+class _SmtFloatingPointBinaryRounded(_SmtBinary, SmtFloatingPoint):
+ lhs: SmtFloatingPoint
+ rhs: SmtFloatingPoint
+ rm: SmtRoundingMode
+
+ def __init__(self, lhs, rhs, *, rm):
+ assert isinstance(rm, SmtRoundingMode)
+ _SmtBinary.__init__(self, lhs, rhs)
+ object.__setattr__(self, "rm", rm)
+ SmtFloatingPoint.__init__(self, eb=self.lhs.eb, sb=self.rhs.sb)
+
+ def _expected_input_class(self):
+ return SmtFloatingPoint
+
+ def _smtlib2_expr(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ op = self._smtlib2_expr_op(expr_state)
+ rm = self.rm._smtlib2_expr(expr_state)
+ lhs = self.lhs._smtlib2_expr(expr_state)
+ rhs = self.rhs._smtlib2_expr(expr_state)
+ return f"({op} {rm} {lhs} {rhs})"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointAdd(_SmtFloatingPointBinaryRounded):
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.add"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointSub(_SmtFloatingPointBinaryRounded):
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.sub"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointMul(_SmtFloatingPointBinaryRounded):
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.mul"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointDiv(_SmtFloatingPointBinaryRounded):
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.div"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointFma(SmtFloatingPoint):
+ """returns `self.factor1 * self.factor2 + self.term`"""
+ factor1: SmtFloatingPoint
+ factor2: SmtFloatingPoint
+ term: SmtFloatingPoint
+ rm: SmtRoundingMode
+
+ def __init__(self, factor1, factor2, term, *, rm):
+ assert isinstance(factor1, SmtFloatingPoint)
+ assert isinstance(factor2, SmtFloatingPoint)
+ assert isinstance(term, SmtFloatingPoint)
+ assert factor1.sort() == factor2.sort() == term.sort(), "sort mismatch"
+ assert isinstance(rm, SmtRoundingMode)
+ object.__setattr__(self, "factor1", factor1)
+ object.__setattr__(self, "factor2", factor2)
+ object.__setattr__(self, "term", term)
+ object.__setattr__(self, "rm", rm)
+ super().__init__(eb=factor1.eb, sb=factor1.sb)
+
+ def _smtlib2_expr(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ rm = self.rm._smtlib2_expr(expr_state)
+ factor1 = self.factor1._smtlib2_expr(expr_state)
+ factor2 = self.factor2._smtlib2_expr(expr_state)
+ term = self.term._smtlib2_expr(expr_state)
+ return f"(fp {rm} {factor1} {factor2} {term})"
+
+
+@dataclass(frozen=True, unsafe_hash=False, eq=False)
+class _SmtFloatingPointUnaryRounded(_SmtUnary, SmtFloatingPoint):
+ inp: SmtFloatingPoint
+ rm: SmtRoundingMode
+
+ def __init__(self, inp, *, rm):
+ assert isinstance(rm, SmtRoundingMode)
+ _SmtUnary.__init__(self, inp)
+ object.__setattr__(self, "rm", rm)
+ SmtFloatingPoint.__init__(self, eb=inp.eb, sb=inp.sb)
+
+ def _expected_input_class(self):
+ return SmtFloatingPoint
+
+ def _smtlib2_expr(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ op = self._smtlib2_expr_op(expr_state)
+ rm = self.rm._smtlib2_expr(expr_state)
+ inp = self.inp._smtlib2_expr(expr_state)
+ return f"({op} {rm} {inp})"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointSqrt(_SmtFloatingPointUnaryRounded):
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.sqrt"
+
+
+@dataclass(frozen=True, unsafe_hash=False, eq=False)
+class _SmtFloatingPointBinary(_SmtBinary, SmtFloatingPoint):
+ lhs: SmtFloatingPoint
+ rhs: SmtFloatingPoint
+
+ def __init__(self, lhs, rhs):
+ _SmtBinary.__init__(self, lhs, rhs)
+ SmtFloatingPoint.__init__(self, eb=self.lhs.eb, sb=self.rhs.sb)
+
+ def _expected_input_class(self):
+ return SmtFloatingPoint
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointRem(_SmtFloatingPointBinary):
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.rem"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointRoundToIntegral(_SmtFloatingPointUnaryRounded):
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.roundToIntegral"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointMin(_SmtFloatingPointBinary):
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.min"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointMax(_SmtFloatingPointBinary):
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.max"
+
+
+@dataclass(frozen=True, unsafe_hash=False, eq=False)
+class _SmtFloatingPointCompareOp(_SmtNAry, SmtBool):
+ inputs: "tuple[SmtFloatingPoint, ...]"
+
+ def _expected_input_class(self):
+ return SmtFloatingPoint
+
+ def __init__(self, *inputs):
+ super().__init__(*inputs)
+ assert len(self.inputs) >= 2, "not enough inputs"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointEq(_SmtFloatingPointCompareOp):
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.eq"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointLt(_SmtFloatingPointCompareOp):
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.lt"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointLE(_SmtFloatingPointCompareOp):
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.leq"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointGt(_SmtFloatingPointCompareOp):
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.gt"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointGE(_SmtFloatingPointCompareOp):
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.geq"
+
+
+@dataclass(frozen=True, unsafe_hash=False, eq=False)
+class _SmtFloatingPointToBoolUnary(_SmtUnary, SmtBool):
+ inp: SmtFloatingPoint
+
+ def _expected_input_class(self):
+ return SmtFloatingPoint
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False)
+class SmtFloatingPointIsNormal(_SmtFloatingPointToBoolUnary):
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.isNormal"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False)
+class SmtFloatingPointIsSubnormal(_SmtFloatingPointToBoolUnary):
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.isSubnormal"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False)
+class SmtFloatingPointIsZero(_SmtFloatingPointToBoolUnary):
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.isZero"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False)
+class SmtFloatingPointIsInfinite(_SmtFloatingPointToBoolUnary):
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.isInfinite"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False)
+class SmtFloatingPointIsNaN(_SmtFloatingPointToBoolUnary):
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.isNaN"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False)
+class SmtFloatingPointIsNegative(_SmtFloatingPointToBoolUnary):
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.isNegative"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False)
+class SmtFloatingPointIsPositive(_SmtFloatingPointToBoolUnary):
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.isPositive"
+
+
+@dataclass(frozen=True, unsafe_hash=False, eq=False)
+class _SmtFloatingPointRoundFrom(_SmtUnary, SmtFloatingPoint):
+ rm: SmtRoundingMode
+
+ def __init__(self, inp, *, rm, eb=None, sb=None, sort=None):
+ assert isinstance(rm, SmtRoundingMode)
+ _SmtUnary.__init__(self, inp)
+ object.__setattr__(self, "rm", rm)
+ SmtFloatingPoint.__init__(self, eb=eb, sb=sb, sort=sort)
+
+ def _smtlib2_expr(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ op = self._smtlib2_expr_op(expr_state)
+ rm = self.rm._smtlib2_expr(expr_state)
+ inp = self.inp._smtlib2_expr(expr_state)
+ return f"({op} {rm} {inp})"
+
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return f"(_ to_fp {self.eb} {self.sb})"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointFromSignedBV(_SmtFloatingPointRoundFrom):
+ inp: SmtBitVec
+
+ def _expected_input_class(self):
+ return SmtBitVec
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointFromUnsignedBV(_SmtFloatingPointRoundFrom):
+ inp: SmtBitVec
+
+ def _expected_input_class(self):
+ return SmtBitVec
+
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return f"(_ to_fp_unsigned {self.eb} {self.sb})"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointFromReal(_SmtFloatingPointRoundFrom):
+ inp: SmtReal
+
+ def _expected_input_class(self):
+ return SmtReal
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False, init=False)
+class SmtFloatingPointFromFP(_SmtFloatingPointRoundFrom):
+ inp: SmtFloatingPoint
+
+ def _expected_input_class(self):
+ return SmtFloatingPoint
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False)
+class SmtFloatingPointFromBits(_SmtUnary, SmtFloatingPoint):
+ inp: SmtBitVec
+
+ def __init__(self, inp, *, eb=None, sb=None, sort=None):
+ assert isinstance(inp, SmtBitVec)
+ _SmtUnary.__init__(self, inp)
+ SmtFloatingPoint.__init__(self, eb=eb, sb=sb, sort=sort)
+ mantissa_field_width = sb - 1
+ sign_field_width = 1
+ expected_width = sign_field_width + eb + mantissa_field_width
+ assert inp.width == expected_width, \
+ f"input BitVec is the wrong width, expected {expected_width}"
+
+ def _expected_input_class(self):
+ return SmtBitVec
+
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return f"(_ to_fp {self.eb} {self.sb})"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False)
+class SmtFloatingPointToReal(_SmtUnary, SmtReal):
+ inp: SmtFloatingPoint
+
+ def _expected_input_class(self):
+ return SmtFloatingPoint
+
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.to_real"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False)
+class SmtFloatingPointToUnsignedBV(_SmtUnary, SmtBitVec):
+ inp: SmtFloatingPoint
+
+ def __init__(self, inp, *, width):
+ _SmtUnary.__init__(self, inp)
+ SmtBitVec.__init__(self, width=width)
+
+ def _expected_input_class(self):
+ return SmtFloatingPoint
+
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.to_ubv"
+
+
+@final
+@dataclass(frozen=True, unsafe_hash=False, eq=False)
+class SmtFloatingPointToSignedBV(_SmtUnary, SmtBitVec):
+ inp: SmtFloatingPoint
+
+ def __init__(self, inp, *, width):
+ _SmtUnary.__init__(self, inp)
+ SmtBitVec.__init__(self, width=width)
+
+ def _expected_input_class(self):
+ return SmtFloatingPoint
+
+ def _smtlib2_expr_op(self, expr_state):
+ assert isinstance(expr_state, _ExprState)
+ return "fp.to_sbv"
projects / nmigen.git / commitdiff