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