# Module `Theory.Empty`

The empty theory.

`include Basic`
`include Minimal`
`include Init`
`val var : 'a var -> 'a pure`

`var v` is the value of the variable `v`.

`val unk : 'a Value.sort -> 'a pure`

`unk s` an unknown value of sort `s`.

This term explicitly denotes a term with undefined or unknown value.

`val let_ : 'a var -> 'a pure -> 'b pure -> 'b pure`

`let_ v exp body` bind the value of `exp` to `v` `body`.

`val ite : bool -> 'a pure -> 'a pure -> 'a pure`

`ite c x y` is `x` if `c` evaluates to `b1` else `y`.

`include Bool`
`val b0 : bool`

`b0` is `false` aka `0` bit

`val b1 : bool`

`b1` is `true` aka `1` bit

`val inv : bool -> bool`

`inv x` inverts `x`.

`val and_ : bool -> bool -> bool`

`and_ x y` is a conjunction of `x` and `y`.

`val or_ : bool -> bool -> bool`

`or_ x y` is a disjunction of `x` and `y`.

`include Bitv`
`val int : 's Bitv.t Value.sort -> word -> 's bitv`

`int s x` is a bitvector constant `x` of sort `s`.

`val msb : 's bitv -> bool`

`msb x` is the most significant bit of `x`.

`val lsb : 's bitv -> bool`

`lsb x` is the least significant bit of `x`.

`val neg : 's bitv -> 's bitv`

`neg x` is two-complement unary minus

`val not : 's bitv -> 's bitv`

`not x` is one-complement negation.

`val add : 's bitv -> 's bitv -> 's bitv`

`add x y` addition modulo `2^'s`

`val sub : 's bitv -> 's bitv -> 's bitv`

`sub x y` subtraction modulo `2^'s`

`val mul : 's bitv -> 's bitv -> 's bitv`

`mul x y` multiplication modulo `2^'s`

`val div : 's bitv -> 's bitv -> 's bitv`

`div x y` unsigned division modulo `2^'s` truncating towards 0.

The division by zero is defined to be a vector of all ones of size `'s`.

`val sdiv : 's bitv -> 's bitv -> 's bitv`

`sdiv x y` is signed division of `x` by `y` modulo `2^'s`,

The signed division operator is defined in terms of the `div` operator as follows:

```                             /
| div x y : if not mx /\ not my
| neg (div (neg x) y) if mx /\ not my
x sdiv y = <
| neg (div x (neg y)) if not mx /\ my
| div (neg x) (neg y) if mx /\ my
\

where mx = msb x, and my = msb y.```
`val modulo : 's bitv -> 's bitv -> 's bitv`

`modulo x y` is the remainder of `div x y` modulo `2^'s`.

`val smodulo : 's bitv -> 's bitv -> 's bitv`

`smodulo x y` is the signed remainder of `div x y` modulo `2^'s`.

This version of the signed remainder where the sign follows the dividend, and is defined via the `% = modulo` operation as follows

```                           /
| x % y : if not mx /\ not my
| neg (neg x % y) if mx /\ not my
x smodulo y = <
| neg (x % (neg y)) if not mx /\ my
| neg (neg x % neg y) mod m if mx /\ my
\

where mx = msb x  and my = msb y.```
`val logand : 's bitv -> 's bitv -> 's bitv`

`logand x y` is a bitwise logical and of `x` and `y`.

`val logor : 's bitv -> 's bitv -> 's bitv`

`logor x y` is a bitwise logical or of `x` and `y`.

`val logxor : 's bitv -> 's bitv -> 's bitv`

`logxor x y` is a bitwise logical xor of `x` and `y`.

`val shiftr : bool -> 's bitv -> 'b bitv -> 's bitv`

`shiftr s x m` shifts `x` right by `m` bits filling with `s`.

`val shiftl : bool -> 's bitv -> 'b bitv -> 's bitv`

`shiftl s x m` shifts `x` left by `m` bits filling with `s`.

`val sle : 'a bitv -> 'a bitv -> bool`

`sle x y` binary predicate for singed less than or equal

`val ule : 'a bitv -> 'a bitv -> bool`

`ule x y` binary predicate for unsigned less than or equal

`val cast : 'a Bitv.t Value.sort -> bool -> 'b bitv -> 'a bitv`

`cast s b x` casts `x` to sort `s` filling with `b`.

If `m = size s - size (sort b) > 0` then `m` bits `b` are prepended to the most significant part of the vector.

Otherwise, if `m <= 0`, i.e., it is a narrowing cast, then the value of `b` doesn't affect the result of evaluation.

`val concat : 'a Bitv.t Value.sort -> 'b bitv list -> 'a bitv`

`concat s xs` concatenates a list of vectors `xs`.

All vectors are concatenated from left to right (so that the most significant bits of the resulting vector are defined by the first element of the list and so on).

The result of concatenation are then casted to sort `s` with all extra bits (if any) set to `zero`.

`val append : 'a Bitv.t Value.sort -> 'b bitv -> 'c bitv -> 'a bitv`

`append s x y` appends `x` and `y` and casts to `s`.

Appends `x` and `y` so that in the resulting vector the vector `x` occupies the most significant part and `y` the least significant part. The resulting vector is then casted to the sort `s` with extra bits (if any) set to zero.

`include Memory`
`val load : ('a, 'b) mem -> 'a bitv -> 'b bitv`

`load m k` is the value associated with the key `k` in the memory `m`.

`val store : ('a, 'b) mem -> 'a bitv -> 'b bitv -> ('a, 'b) mem`

`store m k x` a memory `m` in which the key `k` is associated with the word `x`.

`include Effect`
`val perform : 'a Effect.sort -> 'a eff`

`perform s` performs a generic effect of sort `s`.

`val set : 'a var -> 'a pure -> data eff`

`set v x` changes the value stored in `v` to the value of `x`.

`val jmp : _ bitv -> ctrl eff`

`jmp dst` passes the control to a program located at `dst`.

`val goto : label -> ctrl eff`

`goto lbl` passes the control to a program labeled with `lbl`.

`val seq : 'a eff -> 'a eff -> 'a eff`

`seq x y` performs effect `x`, after that perform effect `y`.

`val blk : label -> data eff -> ctrl eff -> unit eff`

`blk lbl data ctrl` an optionally labeled sequence of effects.

If `lbl` is `Label.null` then the block is unlabeled. If it is not `Label.null` then the denotations will preserve the label and assume that this `blk` is referenced from some other blocks.

• since 2.4.0 the [blk] operator accepts (and welcomes)

`Label.null` as the label in cases when the block is not really expected to be called from anywhere else.

`val repeat : bool -> data eff -> data eff`

`repeat c data` repeats data effects until the condition `c` holds.

`val branch : bool -> 'a eff -> 'a eff -> 'a eff`

`branch c lhs rhs` if `c` holds then performs `lhs` else `rhs`.

`val zero : 'a Bitv.t Value.sort -> 'a bitv`

`zero s` creates a bitvector of all zeros of sort `s`.

`val is_zero : 'a bitv -> bool`

`is_zero x` holds if `x` is a bitvector of all zeros

`val non_zero : 'a bitv -> bool`

`non_zero x` holds if `x` is not a zero bitvector.

`val succ : 'a bitv -> 'a bitv`

`succ x` is the successor of `x`.

`val pred : 'a bitv -> 'a bitv`

`pred x` is the predecessor of `x`.

`val nsucc : 'a bitv -> int -> 'a bitv`

`nsucc x n` is the `n`th successor of `x`.

`val npred : 'a bitv -> int -> 'a bitv`

`npred x` is the `n`th predecessor of `x`.

`val high : 'a Bitv.t Value.sort -> 'b bitv -> 'a bitv`

`high s x` is the high cast of `x` to sort `s`.

if `m = size (sort x) - size s > 0` then `high s x` evaluates to `m` most significant bits of `x`; else if `m = 0` then `high s x` evaluates to the value of `x`; else `m` zeros are prepended to the most significant part of `x`.

`val low : 'a Bitv.t Value.sort -> 'b bitv -> 'a bitv`

`low s x = cast s b0 x` is the low cast of `x` to sort `s`.

if `m = size (sort x) - size s < 0` then `low s x` evaluates to `size s` least significant bits of `x`; else if `m = 0` then `high s x` evaluates to the value of `x`; else `m` zeros are prepended to the most significant part of `x`.

`val signed : 'a Bitv.t Value.sort -> 'b bitv -> 'a bitv`

`signed s x = cast s (msb x) x` is the signed cast of `x` to sort `s`.

if `m = size s - (size (sort x)) > 0` then extends `x` on its most significant side with `m` bits equal to `msb x`; else if `m = 0` then `signed s x` evaluates to `x` else it evaluates to `size s` least significant bits of `x`.

`val unsigned : 'a Bitv.t Value.sort -> 'b bitv -> 'a bitv`

`unsigned s x = cast s b0 x` is the unsigned cast of `x` to sort `s`.

if `m = size s - (size (sort x)) > 0` then extends `x` on its most significant side with `m` zeros; else if `m = 0` then `unsigned s x` evaluates to `x` else it evaluates to `size s` least significant bits of `x`.

`val extract : 'a Bitv.t Value.sort -> 'b bitv -> 'b bitv -> _ bitv -> 'a bitv`

`extract s hi lo x` extracts bits of `x` between `hi` and `lo`.

Extracts `hi-lo+1` consecutive bits of `x` from `hi` to `lo`, and casts them to sort `s` with any excessive bits set to zero.

Note that `hi-lo+1` is taken modulo `2^'b`, so this operation is defined even if `lo` is greater or equal to `hi`.

`val loadw : 'c Bitv.t Value.sort -> bool -> ('a, _) mem -> 'a bitv -> 'c bitv`

`loadw s e m k` loads a word from the memory `m`.

if `e` evaluates to `b1` (big endian case), then the term evaluates to `low s (m[k] @ m[k+1] @ ... @ m[k+n] )`, else the term evaluates to `low s (m[k+n] @ m[k+n-1] @ ... @ m[k] )` where `x @ y` is `append (vals m) x y`, and `n` is the smallest natural number such that `n * size (vals (sort m)) >= size s`, an `m[i]` is the `i`'th value of memory `m`. .

This is a generic function that loads words using specified endianess (`e` could be read as `is_big_endian`) with arbitrary byte size.

`val storew : bool -> ('a, 'b) mem -> 'a bitv -> 'c bitv -> ('a, 'b) mem`

`storew e m k x` stores a word in the memory `m`.

Splits the word `x` into chunks of size equal to the size of memory elements and lays them out in the big endian order, if `e` evaluates to `b1`, or little endian order otherwise.

`val arshift : 'a bitv -> 'b bitv -> 'a bitv`

`arshift x m = shiftr (msb x) m` arithmetically shifts `x` right by `m` bits.

`val rshift : 'a bitv -> 'b bitv -> 'a bitv`

`rshift x m = shiftr b0 x m` shifts `x` right by `m` bits

`val lshift : 'a bitv -> 'b bitv -> 'a bitv`

`lshift x y = shiftl b0 x m` shifts `x` left by `m` bits.

`val eq : 'a bitv -> 'a bitv -> bool`

`eq x y` holds if `x` and `y` are bitwise equal.

`val neq : 'a bitv -> 'a bitv -> bool`

`eq x y` holds if `x` and `y` are not bitwise equal.

`val slt : 'a bitv -> 'a bitv -> bool`

`slt x y` signed strict less than.

`val ult : 'a bitv -> 'a bitv -> bool`

`ult x y` unsigned strict less than.

`val sgt : 'a bitv -> 'a bitv -> bool`

`sgt x y` signed strict greater than.

`val ugt : 'a bitv -> 'a bitv -> bool`

`ugt x y` unsigned strict greater than.

`val sge : 'a bitv -> 'a bitv -> bool`

`sge x y` signed greater or equal than.

`val uge : 'a bitv -> 'a bitv -> bool`

`sge x y` signed greater or equal than.

`include Float`
`include Fbasic`
```val float : ('r, 's) format Float.t Value.sort -> 's bitv -> ('r, 's) format float```

`float s x` interprets `x` as a floating-point number.

`val fbits : ('r, 's) format float -> 's bitv`

`fbits x` is a bitvector representation of the floating-point number `x`.

`val is_finite : 'f float -> bool`

`is_finite x` holds if `x` represents a finite number.

A floating-point number is finite if it represents a number from the set of real numbers `R`.

The predicate always holds for formats in which only finite floating-point numbers are representable.

`val is_nan : 'f float -> bool`

`is_nan x` holds if `x` represents a not-a-number.

A floating-point value is not-a-number if it is neither finite nor infinite number.

The predicated never holds for formats that represent only numbers.

`val is_inf : 'f float -> bool`

`is_inf x` holds if `x` represents an infinite number.

Never holds for formats in which infinite numbers are not representable.

`val is_fzero : 'f float -> bool`

`is_fzero x` holds if `x` represents a zero.

`val is_fpos : 'f float -> bool`

`is_fpos x` holds if `x` represents a positive number.

The denotation is not defined if `x` represents zero.

`val is_fneg : 'f float -> bool`

`is_fneg x` hold if `x` represents a negative number.

The denotation is not defined if `x` represents zero.

#### Rounding modes

Many operations in the Theory of Floating-Point numbers are defined using the rounding mode parameter.

The rounding mode gives a precise meaning to the phrase "the closest floating-point number to `x`", where `x` is a real number. When `x` is not representable by the given format, some other number `x'` is selected based on rules of the rounding mode.

`val rne : rmode`

rounding to nearest, ties to even.

The denotation is the floating-point number nearest to the denoted real number. If the two nearest numbers are equally close, then the one with an even least significant digit shall be selected. The denotation is not defined, if both numbers have an even least significant digit.

`val rna : rmode`

rounding to nearest, ties away.

The denotation is the floating-point number nearest to the denoted real number. If the two nearest numbers are equally close, then the one with larger magnitude shall be selected.

`val rtp : rmode`

rounding towards positive.

The denotation is the floating-point number that is nearest but no less than the denoted real number.

`val rtn : rmode`

rounding towards negative.

The denotation is the floating-point number that is nearest but not greater than the denoted real number.

`val rtz : rmode`

rounding towards zero.

The denotation is the floating-point number that is nearest but not greater in magnitude than the denoted real number.

`val requal : rmode -> rmode -> bool`

`requal x y` holds if rounding modes are equal.

`val cast_float : 'f Float.t Value.sort -> rmode -> 'a bitv -> 'f float`

`cast_float s m x` is the closest to `x` floating number of sort `s`.

The bitvector `x` is interpreted as an unsigned integer in the two-complement form.

`val cast_sfloat : 'f Float.t Value.sort -> rmode -> 'a bitv -> 'f float`

`cast_sfloat s rm x` is the closest to `x` floating-point number of sort `x`.

The bitvector `x` is interpreted as a signed integer in the two-complement form.

`val cast_int : 'a Bitv.t Value.sort -> rmode -> 'f float -> 'a bitv`

`cast_int s rm x` returns an integer closest to `x`.

The resulting bitvector should be interpreted as an unsigned two-complement integer.

`val cast_sint : 'a Bitv.t Value.sort -> rmode -> 'f float -> 'a bitv`

`cast_sint s rm x` returns an integer closest to `x`.

The resulting bitvector should be interpreted as a signed two-complement integer.

`val fneg : 'f float -> 'f float`

`fneg x` is `-x`

`val fabs : 'f float -> 'f float`

`fabs x` the absolute value of `x`.

`val fadd : rmode -> 'f float -> 'f float -> 'f float`

`fadd m x y` is the floating-point number closest to `x+y`.

`val fsub : rmode -> 'f float -> 'f float -> 'f float`

`fsub m x y` is the floating-point number closest to `x-y`.

`val fmul : rmode -> 'f float -> 'f float -> 'f float`

`fmul m x y` is the floating-point number closest to `x*y`.

`val fdiv : rmode -> 'f float -> 'f float -> 'f float`

`fdiv m x y` is the floating-point number closest to `x/y`.

`val fsqrt : rmode -> 'f float -> 'f float`

`fsqrt m x` returns the closest floating-point number to `r`, where `r` is such number that `r*r` is equal to `x`.

If `x` is a negative finite non-zero number, or is `nan`, or is the negative infinity, then `sqrt x` is `nan`. If `x` is the positive infinity then `fsqrt x` is the positive infinity.

`val fmodulo : rmode -> 'f float -> 'f float -> 'f float`

`fdiv m x y` is the floating-point number closest to the remainder of `x/y`.

`val fmad : rmode -> 'f float -> 'f float -> 'f float -> 'f float`

`fmad m x y z` is the floating-point number closest to `x * y + z`.

`val fround : rmode -> 'f float -> 'f float`

`fround m x` is the floating-point number closest to `x` rounded to an integral, using the rounding mode `m`.

`val fconvert : 'f Float.t Value.sort -> rmode -> _ float -> 'f float`

`fconvert f r x` is the closest to `x` floating number in format `f`.

`val fsucc : 'f float -> 'f float`

`fsucc m x` is the least floating-point number representable in (sort x) that is greater than `x`.

`val fpred : 'f float -> 'f float`

`fsucc m x` is the greatest floating-point number representable in (sort x) that is less than `x`.

`val forder : 'f float -> 'f float -> bool`

`forder x y` holds if floating-point number `x` is less than `y`.

The denotation is not defined if either of arguments do not represent a floating-point number.

`val pow : rmode -> 'f float -> 'f float -> 'f float`

`pow m b a` is a floating-point number closest to `b^a`.

Where `b^a` is `b` raised to the power of `a`.

Values, such as `0^0`, as well as `1^infinity` and `infinity^1` in formats that have a representation for infinity, are not defined.

`val compound : rmode -> 'f float -> 'a bitv -> 'f float`

`compound m x n` is the floating-point number closest to `(1+x)^n`.

Where `b^a` is `b` raised to the power of `a`.

The denotation is not defined if `x` is less than `-1`, or if `x` is `n` represent zeros, or if `x` doesn't represent a finite floating-point number.

`val rootn : rmode -> 'f float -> 'a bitv -> 'f float`

`rootn m x n` is the floating-point number closest to `x^(1/n)`.

Where `b^a` is `b` raised to the power of `a`.

The denotation is not defined if:

• `n` is zero;
• `x` is zero and n is less than zero;
• `x` is not a finite floating-point number;
`val pown : rmode -> 'f float -> 'a bitv -> 'f float`

`pown m x n` is the floating-point number closest to `x^n`.

Where `b^a` is `b` raised to the power of `a`.

The denotation is not defined if `x` and `n` both represent zero or if `x` doesn't represent a finite floating-point number.

`val rsqrt : rmode -> 'f float -> 'f float`

`rsqrt m x` is the closest floating-point number to `1 / sqrt x`.

The denotation is not defined if `x` is less than or equal to zero or doesn't represent a finite floating-point number.

`val hypot : rmode -> 'f float -> 'f float -> 'f float`

`hypot m x y` is the closest floating-point number to `sqrt(x^2 + y^2)`.

The denotation is not defined if `x` or `y` do not represent finite floating-point numbers.

`include Trans`
`val exp : rmode -> 'f float -> 'f float`

`exp m x` is the floating-point number closest to `e^x`,

where `b^a` is `b` raised to the power of `a` and `e` is the base of natural logarithm.

`val expm1 : rmode -> 'f float -> 'f float`

`expm1 m x` is the floating-point number closest to `e^x - 1`,

where `b^a` is `b` raised to the power of `a` and `e` is the base of natural logarithm.

`val exp2 : rmode -> 'f float -> 'f float`

`exp2 m x` is the floating-point number closest to `2^x`,

where `b^a` is `b` raised to the power of `a`.

`val exp2m1 : rmode -> 'f float -> 'f float`

`exp2 m x` is the floating-point number closest to `2^x - 1`,

where `b^a` is `b` raised to the power of `a`.

`val exp10 : rmode -> 'f float -> 'f float`

`exp10 m x` is the floating-point number closest to `10^x`,

where `b^a` is `b` raised to the power of `a`.

`val exp10m1 : rmode -> 'f float -> 'f float`

`exp10m1 m x` is the floating-point number closest to `10^x - 1`,

where `b^a` is `b` raised to the power of `a`.

`val log : rmode -> 'f float -> 'f float`

`log m x` is the floating-point number closest to `log x`.

`val log2 : rmode -> 'f float -> 'f float`

`log2 m x` is the floating-point number closest to `log x / log 2`.

`val log10 : rmode -> 'f float -> 'f float`

`log10 m x` is the floating-point number closest to `log x / log 10`.

`val logp1 : rmode -> 'f float -> 'f float`

`logp1 m x` is the floating-point number closest to `log (1+x)`.

`val log2p1 : rmode -> 'f float -> 'f float`

`logp1 m x` is the floating-point number closest to `log (1+x) / log 2`.

`val log10p1 : rmode -> 'f float -> 'f float`

`logp1 m x` is the floating-point number closest to `log (1+x) / log 10`.

`val sin : rmode -> 'f float -> 'f float`

`sin m x` is the floating-point number closest to `sin x`.

`val cos : rmode -> 'f float -> 'f float`

`cos m x` is the floating-point number closest to `cos x`.

`val tan : rmode -> 'f float -> 'f float`

`tan m x` is the floating-point number closest to `tan x`.

`val sinpi : rmode -> 'f float -> 'f float`

`sinpi m x` is the floating-point number closest to `sin (pi*x)`.

`val cospi : rmode -> 'f float -> 'f float`

`cospi m x` is the floating-point number closest to `cos (pi*x)`.

`val atanpi : rmode -> 'f float -> 'f float`

`atanpi m y x` is the floating-point number closest to `atan(y/x) / pi`.

`val atan2pi : rmode -> 'f float -> 'f float -> 'f float`

`atanpi m y x` is the floating-point number closest to `atan(y/x) / (2*pi)`.

`val asin : rmode -> 'f float -> 'f float`

`asin m x` is the floating-point number closest to `asin x`.

`val acos : rmode -> 'f float -> 'f float`

`acos m x` is the floating-point number closest to `acos x`.

`val atan : rmode -> 'f float -> 'f float`

`atan m x` is the floating-point number closest to `atan x`.

`val atan2 : rmode -> 'f float -> 'f float -> 'f float`

`atan2 m y x` is the floating-point number closest to `atan (y/x)`.

`val sinh : rmode -> 'f float -> 'f float`

`sinh m x` is the floating-point number closest to `sinh x`.

`val cosh : rmode -> 'f float -> 'f float`

`cosh m x` is the floating-point number closest to `cosh x`.

`val tanh : rmode -> 'f float -> 'f float`

`tanh m x` is the floating-point number closest to `tanh x`.

`val asinh : rmode -> 'f float -> 'f float`

`asinh m x` is the floating-point number closest to `asinh x`.

`val acosh : rmode -> 'f float -> 'f float`

`acosh m x` is the floating-point number closest to `acosh x`.

`val atanh : rmode -> 'f float -> 'f float`

`atanh m x` is the floating-point number closest to `atanh x`.