# Module type `Theory.Minimal`

The Minimal theory.

`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`.