module Bddreg:Arithmetic with BDDs`sig`

..`end`

This module encode the classical arithmetic and logical operations on arrays of bits, each bit being defined by a BDD. It doesn't need any initialization, and there is no in-place modification.

The type handled by the module is an array of BDDs, which represent a processor-like register with the Least Significant Bit in first position.

This module requires the mlcuddidl library.

type`t =`

`Bdd.t array`

type of arrays of bits

`val lnot : ``t -> t`

Logical negation (for all bits).

`val shift_left : ``Manager.t -> int -> t -> t * Bdd.t`

`shift_left man t n`

shifts the register to the left by `n`

bits. Returns the resulting register and the carry, which
contains the last bit shifted out of the register. Assume, as
for the following functions, that `n`

is between `1`

and
the size of the register.`val shift_right : ``Manager.t -> int -> t -> t * Bdd.t`

`shift_right t n`

shifts the register to the right by `n`

bits. This an `val shift_right_logical : ``Manager.t -> int -> t -> t * Bdd.t`

Same as *logical* shift: a zero
is always inserted.

`shift_right`

, but here `val extend : ``Manager.t -> signed:bool -> int -> t -> t`

register extension or truncation.

`extend ~signed:b n x`

extends the register x by adding `n`

most
significant bits, if `n>0`

, or truncate the `-n`

most significant bits if
`n<0`

. `b`

indicates whether the register is considered as a signed one or
not.`val succ : ``Manager.t -> t -> t * Bdd.t`

Successor operation; returns the new register and the carry.

`val pred : ``Manager.t -> t -> t * Bdd.t`

Predecessor operation; returns the new register and the carry.

`val add : ``Manager.t -> t -> t -> t * Bdd.t * Bdd.t`

Addition; returns the new registerm, the carry, and the
overflow (for signed integers).

`val sub : ``Manager.t -> t -> t -> t * Bdd.t * Bdd.t`

Substraction; returns the new register, the carry, and the
overflow (for signed integers).

`val neg : ``t -> t`

Unary negation; be cautious, if the size of integer is

`n`

,
the negation of `-2^(n-1)`

is itself.`val scale : ``int -> t -> t`

Multiplication by a positive constant.

`val ite : ``Bdd.t -> t -> t -> t`

if-then-else operation. Zero-size possible.

`val is_cst : ``t -> bool`

Tests whether it contains a constant value. Zero-size possible.

`val zero : ``Manager.t -> t -> Bdd.t`

Tests the register to zero.

`val equal : ``Manager.t -> t -> t -> Bdd.t`

Equality test.

`val greatereq : ``Manager.t -> t -> t -> Bdd.t`

Signed greater-or-equal test.

`val greater : ``Manager.t -> t -> t -> Bdd.t`

Signed strictly-greater-than test.

`val highereq : ``Manager.t -> t -> t -> Bdd.t`

Unsigned greater-or-equal test.

`val higher : ``Manager.t -> t -> t -> Bdd.t`

Unsigned strictly-greater-than test.

`val min_size : ``int -> int`

`min_size cst`

computes the minimum number of bits required
to represent the given constant. We have for example ```
min_size
0=0
```

, `min_size 1 = 2`

, `min_size 3 = 2`

, `min_size (-8) = 4`

.`val of_int : ``Manager.t -> int -> int -> t`

`of_int size cst`

puts the constant integer `cst`

in a constant register
of size `size`

. The fact that `size`

is big enough is checked using the
previous function, and a `Failure "..."`

exception is raised in case of
problem.`val to_int : ``signed:bool -> t -> int`

`to_int sign x`

converts a constant register to an integer. `sign`

indicates whether the register is to be interpreted as a signed or
unsigned.`val equal_int : ``Manager.t -> t -> int -> Bdd.t`

`val greatereq_int : ``Manager.t -> t -> int -> Bdd.t`

`val greater_int : ``Manager.t -> t -> int -> Bdd.t`

`val highereq_int : ``Manager.t -> t -> int -> Bdd.t`

`val higher_int : ``Manager.t -> t -> int -> Bdd.t`

Tests w.r.t. a constant register, the size of which is
defined by the first given register.

module Minterm:`sig`

..`end`

`val guard_of_minterm : ``Manager.t -> t -> Minterm.t -> Bdd.t`

Return the guard of the deterministic minterm in the BDD register.

`val guard_of_int : ``Manager.t -> t -> int -> Bdd.t`

Return the guard of the integer value in the BDD register.

`val guardints : ``Manager.t -> signed:bool -> t -> (Bdd.t * int) list`

Return the list

`g -> n`

represented by the BDD register.`val print : ``(int -> string) -> Format.formatter -> t -> unit`

`print f fmt t`

prints the register `t`

using the formatter
`fmt`

and the function `f`

to convert BDDs indices to
names.`val print_minterm : ``signed:bool ->`

(Format.formatter -> Bdd.t -> unit) -> Format.formatter -> t -> unit

`print_minterm f fmt t`

prints the register `t`

using the formatter
`fmt`

and the function `f`

to convert BDDs indices to
names.