module Mapleaf:sig
..end
(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
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
\/ 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
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
\/
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
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.
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
\/ 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
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
\/
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
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.
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
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
combineleaf_array
, but in which the
first (resp. first and second) leaves (and MTBDD) type may be
different.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
.