ord -package:foundation -package:mixed-types-num -package:github package:sbv
Symbolic Comparisons. Similar to
Eq, we cannot implement
Haskell's
Ord class since there is no way to return an
Ordering value from a symbolic comparison. Furthermore,
OrdSymbolic requires
Mergeable to implement
if-then-else, for the benefit of implementing symbolic versions of
max and
min functions.
A symbolic unsigned bit-vector carrying its size info
16-bit unsigned symbolic value
32-bit unsigned symbolic value
64-bit unsigned symbolic value
8-bit unsigned symbolic value
An unsigned bit-vector carrying its size info
Check if a relation is a linear order. The string argument must
uniquely identify this order.
Check if a relation is a partial order. The string argument must
uniquely identify this order.
Check if a relation is a piece-wise linear order. The string argument
must uniquely identify this order.
Check if a relation is a tree order. The string argument must uniquely
identify this order.
Convert an
SDouble to an
SWord64, preserving the
bit-correspondence. Note that since the representation for
NaNs are not unique, this function will return a symbolic
value when given a concrete
NaN.
See the implementation note for
sFloatAsSWord32, as it applies
here as well.
Convert an
SFloat to an
SWord32, preserving the
bit-correspondence. Note that since the representation for
NaNs are not unique, this function will return a symbolic
value when given a concrete
NaN.
Implementation note: Since there's no corresponding function in SMTLib
for conversion to bit-representation due to partiality, we use a
translation trick by allocating a new word variable, converting it to
float, and requiring it to be equivalent to the input. In
code-generation mode, we simply map it to a simple conversion.
Convert a float to the word containing the corresponding bit pattern
Declare a named
SWord
NB. For a version which generalizes over the underlying monad, see
sWord
Declare a named
SWord16
NB. For a version which generalizes over the underlying monad, see
sWord16
Declare an unnamed
SWord16
NB. For a version which generalizes over the underlying monad, see
sWord16_
Declare a list of
SWord16s
NB. For a version which generalizes over the underlying monad, see
sWord16s
Declare a named
SWord32
NB. For a version which generalizes over the underlying monad, see
sWord32
Reinterpret the bits in a 32-bit word as a single-precision floating
point number
Declare an unnamed
SWord32
NB. For a version which generalizes over the underlying monad, see
sWord32_
Declare a list of
SWord32s
NB. For a version which generalizes over the underlying monad, see
sWord32s
Declare a named
SWord64
NB. For a version which generalizes over the underlying monad, see
sWord64
Reinterpret the bits in a 32-bit word as a single-precision floating
point number