ord -package:foundation -package:BNFC-meta package:sbv

The ord of a character.

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