Module Cudd.Mapleaf

module Mapleaf: sig .. end

This module offers functions to lift operations on leaves to operations on MTBDDs on such leaves. Algorithmically, this is done by decomposing MTBDDs in lists of pairs (guard,leaf).

An alternative, which may be more efficient but a bit less flexible, is to use functions of module Cudd.User.

In order to be usable with both modules Cudd.Mtbdd and Cudd.Mtbddc, the signature of the functions of this modules use the type 'a Vdd.t, but Vdds should not be used directly.

Global option

val restrict : bool Pervasives.ref

If true, simplifies in some functions MTBDDs using Cudd.Mtbdd.restrict or Cudd.Mtbddc.restrict.

Functions of arity 1

In the following documentation, the pair guard,leaf is implicitly iterated on all such pairs contained in the argument MTBDD.

val mapleaf1 : ('a -> 'b) -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t

Return the MTBDD \/ guard -> f leaf

val retractivemapleaf1 : default:'a Cudd.Vdd.t ->
       (Cudd.Bdd.vt -> 'b -> Cudd.Bdd.vt * 'a) -> 'b Cudd.Vdd.t -> 'a Cudd.Vdd.t

Assuming that the new guards delivered by the function f are disjoint, return the MTBDD

default \/ (\/ nguard ->
        nleaf)

with (nguard,nleaf) = f guard leaf.

val expansivemapleaf1 : default:'a Cudd.Vdd.t ->
       merge:('a Cudd.Vdd.t -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t) ->
       (Cudd.Bdd.vt -> 'b -> Cudd.Bdd.vt * 'a) -> 'b Cudd.Vdd.t -> 'a Cudd.Vdd.t

Same as above, but with \/ replaced by merge (supposed to be commutative and associative).

val combineleaf1 : default:'a ->
       combine:('b -> 'a -> 'a) -> (Cudd.Bdd.vt -> 'c -> 'b) -> 'c Cudd.Vdd.t -> 'a

Generic function, instanciated above. The result acc (kind of accumulator) is initialized with default, to which one progressively add combine acc (f guard leaf).

combine should not be sensitive to the order in which one iterates on guards and leaves.

Functions of arity 2

In the following documentation, the pair guard1,leaf1 (resp. guard2,leaf2) is implicitly iterated on all such pairs contained in the first (resp. second) argument MTBDD.

val mapleaf2 : ('a -> 'b -> 'c) -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t

Return the MTBDD \/ guard1 /\ guard2 -> f leaf1 leaf2

val retractivemapleaf2 : default:'a Cudd.Vdd.t ->
       (Cudd.Bdd.vt -> 'b -> 'c -> Cudd.Bdd.vt * 'a) ->
       'b Cudd.Vdd.t -> 'c Cudd.Vdd.t -> 'a Cudd.Vdd.t

Assuming that the new guards delivered by the function f are disjoint, return the MTBDD default \/ (\/ nguard -> nleaf) with (nguard,nleaf) = f (guard1 /\ guard2) leaf1 leaf2.

val expansivemapleaf2 : default:'a Cudd.Vdd.t ->
       merge:('a Cudd.Vdd.t -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t) ->
       (Cudd.Bdd.vt -> 'b -> 'c -> Cudd.Bdd.vt * 'a) ->
       'b Cudd.Vdd.t -> 'c Cudd.Vdd.t -> 'a Cudd.Vdd.t

Same as above, but with \/ replaced by merge (supposed to be commutative and associative).

val combineleaf2 : default:'a ->
       combine:('b -> 'a -> 'a) ->
       (Cudd.Bdd.vt -> 'c -> 'd -> 'b) -> 'c Cudd.Vdd.t -> 'd Cudd.Vdd.t -> 'a

Generic function, instanciated above. The result acc (kind of accumulator) is initialized with default, to which one progressively add

combine acc (f (guard1 /\
        guard2) leaf1 leaf2)

combine should not be sensitive to the order in which one iterates on guards and leaves.

Functions on arrays

In the following documentation, tguard,tleaves denotes resp. the conjunctions of guards (of the array of MTBDD) and the associated array of leaves.

val combineleaf_array : default:'a ->
       combine:('b -> 'a -> 'a) ->
       tabsorbant:('c -> bool) option array ->
       (Cudd.Bdd.vt -> 'c array -> 'b) -> 'c Cudd.Vdd.t array -> 'a

Generic function,. The result acc (kind of accumulator) is initialized with default, to which one progressively add combine acc (f (/\ tguard) tleaves).

The arrays are assumed to be non-empty.

If for some i, tabsorbant.(i)=Some abs and absorbant tleaves.(i)=true, then f (/\ tguard) tleaves is assumed to return default (this allows optimisation).

combine should not be sensitive to the order in which one iterates on guards and leaves.

val combineleaf1_array : default:'a ->
       combine:('b -> 'a -> 'a) ->
       ?absorbant:('c -> bool) ->
       tabsorbant:('d -> bool) option array ->
       (Cudd.Bdd.vt -> 'c -> 'd array -> 'b) ->
       'c Cudd.Vdd.t -> 'd Cudd.Vdd.t array -> 'a

val combineleaf2_array : default:'a ->
       combine:('b -> 'a -> 'a) ->
       ?absorbant1:('c -> bool) ->
       ?absorbant2:('d -> bool) ->
       tabsorbant:('e -> bool) option array ->
       (Cudd.Bdd.vt -> 'c -> 'd -> 'e array -> 'b) ->
       'c Cudd.Vdd.t -> 'd Cudd.Vdd.t -> 'e Cudd.Vdd.t array -> 'a

Functions similar to combineleaf_array, but in which the first (resp. first and second) leaves (and MTBDD) type may be different.

Internal functions

val combineretractive : Cudd.Bdd.vt * 'a -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t

combinetractive (guard,leaf) vdd = Vdd.ite guard leaf vdd. Used in cases where guard and the guard of ``interesting things'' in vdd are disjoint, hence the name.

val combineexpansive : default:'a Cudd.Vdd.t ->
       merge:('a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t) ->
       Cudd.Bdd.vt * 'a -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t

combineexpansive ~default ~merge (guard,leaf) vdd = merge
        (Vdd.ite guard leaf default) vdd

. Implements in some way an ``union'' of (guard,leaf) and vdd.