Previous  Up  Next

Module Cudd.Custom


module Custom: sig .. end

Custom Operations on VDDs
type pid 
type mlvalue

type common = {
   pid : pid;
   arity : int;
   memo : Cudd.Memo.t;
}
Common information

type ('a, 'b) op1 = {
   common1 : common;
   closure1 : 'a -> 'b;
}
Unary operation

type ('a, 'b, 'c) op2 = {
   common2 : common;
   closure2 : 'a -> 'b -> 'c;
   ospecial2 : ('a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t option) option;
   commutative : bool;
   idempotent : bool;
}
Binary operation

type ('a, 'b) test2 = {
   common2t : common;
   closure2t : 'a -> 'b -> bool;
   ospecial2t : ('a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> bool option) option;
   symetric : bool;
   reflexive : bool;
}
Binary test

type ('a, 'b, 'c, 'd) op3 = {
   common3 : common;
   closure3 : 'a -> 'b -> 'c -> 'd;
   ospecial3 : ('a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t -> 'd Cudd.Vdd.t option)
option;
}
Ternary operation

type ('a, 'b) opN = {
   commonN : common;
   arityNbdd : int;
   closureN : Cudd.Bdd.vt array -> 'a Cudd.Vdd.t array -> 'b Cudd.Vdd.t option;
}
N-ary operation

type ('a, 'b) opG = {
   commonG : common;
   arityGbdd : int;
   closureG : Cudd.Bdd.vt array -> 'a Cudd.Vdd.t array -> 'b Cudd.Vdd.t option;
   oclosureBeforeRec : (int * bool ->
Cudd.Bdd.vt array ->
'a Cudd.Vdd.t array -> Cudd.Bdd.vt array * 'a Cudd.Vdd.t array)
option;
   oclosureIte : (int -> 'b Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'b Cudd.Vdd.t) option;
}
N-ary general operation

type 'a exist = {
   commonexist : common;
   combineexist : ('a, 'a, 'a) op2;
}
Existential quantification

type 'a existand = {
   commonexistand : common;
   combineexistand : ('a, 'a, 'a) op2;
   bottomexistand : 'a;
}
Existential quantification combined with intersection

type ('a, 'b) existop1 = {
   commonexistop1 : common;
   combineexistop1 : ('b, 'b, 'b) op2;
   existop1 : ('a, 'b) op1;
}
Existop1ential quantification

type ('a, 'b) existandop1 = {
   commonexistandop1 : common;
   combineexistandop1 : ('b, 'b, 'b) op2;
   existandop1 : ('a, 'b) op1;
   bottomexistandop1 : 'b;
}
Existential quantification combined with intersection
val newpid : unit -> pid
val apply_op1 : ('a, 'b) op1 -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t
val apply_op2 : ('a, 'b, 'c) op2 ->
       'a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t
val apply_test2 : ('a, 'b) test2 -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> bool
val apply_op3 : ('a, 'b, 'c, 'd) op3 ->
       'a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t -> 'd Cudd.Vdd.t
val apply_opN : ('a, 'b) opN ->
       Cudd.Bdd.vt array -> 'a Cudd.Vdd.t array -> 'b Cudd.Vdd.t
val apply_opG : ('a, 'b) opG ->
       Cudd.Bdd.vt array -> 'a Cudd.Vdd.t array -> 'b Cudd.Vdd.t
val _apply_exist : 'a exist -> Cudd.Bdd.vt -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t
val _apply_existand : 'a existand ->
       Cudd.Bdd.vt -> Cudd.Bdd.vt -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t
val _apply_existop1 : ('a, 'b) existop1 ->
       Cudd.Bdd.vt -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t
val _apply_existandop1 : ('a, 'b) existandop1 ->
       Cudd.Bdd.vt -> Cudd.Bdd.vt -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t