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.

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 : (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.