Module type Theory.Bitv

The theory of bitvectors.

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.