Up  Next

Module Bddreg


module Bddreg: sig .. end
Arithmetic with BDDs

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

Logical operations


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 arithmetical shift: the sign is inserted as the new most significant bits. Returns the resulting register and the carry, which contains the last bit shifted out of the register.
val shift_right_logical : Manager.t -> int -> t -> t * Bdd.t
Same as shift_right, but here logical shift: a zero is always inserted.
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.

Arithmetic operations


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.

Predicates


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.

Constants: conversion and predicates


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.

Decomposition in guarded form


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.

Printing


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.