Module Bddint

module Bddint: sig .. end
Integer type for interpreted automaton

This module is intended to encode operations based on bounded integers (or more generally, enumerated types), using BDDs. It represents a layer on top of Bddarith, which provides with arrays resizing and signs.

Let us give an example: suppose we have a variable i: int[0..7]; this variable will be encoded by 3 Boolean variables i0,i1,i2, starting from the least significant bit. Now, how to translate the expression i<=5 ? Here the result will be i2 and not i1 or not i2

This module requires the mlcuddidl library and the Bddarith module.

The basic types are signed or unsigned n-bits integers. Integers are defined by a an array of BDDs, each BDD corresponding to a bit. The order in this array is going from the LSB (Least Significant Bit) to the MSB (Most Significant Bit).

type t = {
   signed : bool;
   reg : Bdd.t array;

type of an enumerated variable
exception Typing of string
Raised when operands are of incompatible type (sign and size)

All the functions are basically wrapper around functions of Bddarith. Resizing and conversion from unsigned to signed are automatic. For instance, When adding or substracting integers, the smallest one is resized to the size of the larger one, possibly with one more bit if they are not of the same type (signed or unsigned).

Conversion of integers

val extend : Manager.t -> int -> t -> t

Operations on integers

val neg : t -> t
val succ : t -> t
val pred : t -> t
val add : t -> t -> t
val sub : t -> t -> t
val shift_left : int -> t -> t
val shift_right : int -> t -> t
val scale : int -> t -> t
val ite : Bdd.t -> t -> t -> t

Predicates on integers

val is_cst : t -> bool
val zero : Manager.t -> t -> Bdd.t
val equal : Manager.t -> t -> t -> Bdd.t
val greatereq : Manager.t -> t -> t -> Bdd.t
val greater : Manager.t -> t -> t -> Bdd.t

Predicates involving constant integers

val of_int : Manager.t -> bool -> int -> int -> t
val to_int : t -> int
val equal_int : Manager.t -> t -> int -> Bdd.t
val greatereq_int : Manager.t -> t -> int -> Bdd.t

Decomposition in guarded form

module Minterm: sig .. end
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 -> 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 : (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.