Module Cudd.User

module User: sig .. end


Important note: The OCaml closure defining the custom operation should not use free variables that may be modified and so impact its result: they would act as hidden parameters that are not taken into account in the memoization table.

If such hidden parameters are modified, the cache should be cleared with Memo.clear, if it is local, otherwise the global cache should be cleared with Cudd.Man.flush.

Types and values



Type of registered operations


type pid = Cudd.Custom.pid 
Identifiers of closures used in shared memoization tables
type common = Cudd.Custom.common = {
   pid :pid; (*Identifiers for shared memoization tables*)
   arity :int; (*Arity of the operations*)
   memo :Cudd.Memo.t; (*Memoization table*)
}
Common information to all operations
val newpid : unit -> Cudd.Custom.pid
val make_common : ?memo:Cudd.Memo.t -> int -> common

Unary operations


type ('a, 'b) op1 = private ('a, 'b) Cudd.Custom.op1 = private {
   common1 :common;
   closure1 :'a -> 'b; (*Operation on leaves*)
}
val make_op1 : ?memo:Cudd.Memo.t -> ('a -> 'b) -> ('a, 'b) op1
Makes a binary operation, with the given memoization policy.
val apply_op1 : ('a, 'b) op1 -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t

Example:

Assuming type t = bool Vdd.t, and corresponding diagrams bdd:t and bdd2:t (with type bool, it is safe to use directly VDDs, and it simplifies the examples).

We want to negate every leaf of bdd1 and bdd2.



Binary operations


type ('a, 'b, 'c) op2 = private ('a, 'b, 'c) Cudd.Custom.op2 = private {
   common2 :common;
   closure2 :'a -> 'b -> 'c; (*Operation on leaves*)
   ospecial2 :('a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t option) option; (*Special case operation*)
   commutative :bool; (*Is the operation commutative ?*)
   idempotent :bool; (*Is the operation idempotent (op x x = x) ?*)
}
val make_op2 : ?memo:Cudd.Memo.t ->
?commutative:bool ->
?idempotent:bool ->
?special:('a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t option) ->
('a -> 'b -> 'c) -> ('a, 'b, 'c) op2
Makes a binary operation, with the given memoization policy.

commutative (default: false), when true, allows to optimize the cache usage (hence the speed) when the operation is commutative.

idempotent (default: false) allows similarly some optimization when op is idempotent: op x x = x. This makes sense only if 'a='b='c (the case will never happens otherwise).

?special (default: None), if equal to Some specialcase, modifies op as follows: it is applied to every pair of node during the recursive descend, and if specialcase vdda vddb = (Some vddc), then vddc is assumed to be the result of map_op2 op vdda vddb. This allows not to perform a full recursive descend when a special case is encountered. See the example below.

val apply_op2 : ('a, 'b, 'c) op2 -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t

Example:

Assuming as for unary operation example type t = bool Vdd.t and corresponding diagrams bdd1:t and bdd2:t.

We can compute their conjunction with

let res = map_op2
    ~commutative:true ~idempotent:true
    ~special:(fun bdd1 bdd2 ->
      if Vdd.is_cst bdd1 && Vdd.dval bdd1 = false then Some(bdd1)
      else if Vdd.is_cst bdd2 && Vdd.dval bdd2 = false then Some(bdd2)
      else None
    (fun b1 b2 -> b1 && b2) bdd1 bdd2;;


Ternary operations


type ('a, 'b, 'c, 'd) op3 = private ('a, 'b, 'c, 'd) Cudd.Custom.op3 = private {
   common3 :common;
   closure3 :'a -> 'b -> 'c -> 'd; (*Operation on leaves*)
   ospecial3 :('a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t -> 'd Cudd.Vdd.t option)
option
;
(*Special cases*)
}
val make_op3 : ?memo:Cudd.Memo.t ->
?special:('a Cudd.Vdd.t ->
'b Cudd.Vdd.t -> 'c Cudd.Vdd.t -> 'd Cudd.Vdd.t option) ->
('a -> 'b -> 'c -> 'd) -> ('a, 'b, 'c, 'd) op3
val apply_op3 : ('a, 'b, 'c, 'd) op3 ->
'a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t -> 'd Cudd.Vdd.t
Combine the two previous operations. if ?memo=None, then a hash table is used, and cleared at the end.

Example:

Still assuming type t = bool Vdd.t and corresponding diagrams bdd1:t, bdd2:t, bdd3:t.

We can define if-then-else with let res = map_op3
    ~special:(fun bdd1 bdd2 bdd3 ->
      if Vdd.is_cst bdd1
      then Some(if Vdd.dval bdd1 (* = true *) then bdd2 else bdd3)
      else None
    )
    (fun b1 b2 b3 -> if b1 then b2 else b3) bdd1 bdd2 bdd3


Nary operations


type ('a, 'b) opN = private ('a, 'b) Cudd.Custom.opN = private {
   commonN :common;
   arityNbdd :int;
   closureN :Cudd.Bdd.vt array -> 'a Cudd.Vdd.t array -> 'b Cudd.Vdd.t option; (*Operation on leaves*)
}
N-ary operation
val make_opN : ?memo:Cudd.Memo.t ->
int ->
int ->
(Cudd.Bdd.vt array -> 'a Cudd.Vdd.t array -> 'b Cudd.Vdd.t option) ->
('a, 'b) opN
val apply_opN : ('a, 'b) opN ->
Cudd.Bdd.vt array -> 'a Cudd.Vdd.t array -> 'b Cudd.Vdd.t
type ('a, 'b) opG = private ('a, 'b) Cudd.Custom.opG = private {
   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
val make_opG : ?memo:Cudd.Memo.t ->
?beforeRec:(int * bool ->
Cudd.Bdd.vt array ->
'a Cudd.Vdd.t array -> Cudd.Bdd.vt array * 'a Cudd.Vdd.t array) ->
?ite:(int -> 'b Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'b Cudd.Vdd.t) ->
int ->
int ->
(Cudd.Bdd.vt array -> 'a Cudd.Vdd.t array -> 'b Cudd.Vdd.t option) ->
('a, 'b) opG
val apply_opG : ('a, 'b) opG ->
Cudd.Bdd.vt array -> 'a Cudd.Vdd.t array -> 'b Cudd.Vdd.t

Binary tests


type ('a, 'b) test2 = private ('a, 'b) Cudd.Custom.test2 = private {
   common2t :common;
   closure2t :'a -> 'b -> bool; (*Test on leaves*)
   ospecial2t :('a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> bool option) option; (*Special cases*)
   symetric :bool; (*Is the relation symetric ?*)
   reflexive :bool; (*Is the relation reflexive ? (test x x = true) ?*)
}
val make_test2 : ?memo:Cudd.Memo.t ->
?symetric:bool ->
?reflexive:bool ->
?special:('a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> bool option) ->
('a -> 'b -> bool) -> ('a, 'b) test2
Register a binary test, with the given memoization policy,

symetric (default: false), when true, allows to optimize the cache usage (hence the speed) when the relation is symetric.

reflexive (default: false) allows similarly some optimization when the relation is reflexive: test x x = true. This makes sense only if 'a='b (the case will never happen otherwise).

?special (default: None) has the same semantics as for binary operation above.

val apply_test2 : ('a, 'b) test2 -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> bool

Quantification


type 'a exist = private 'a Cudd.Custom.exist = private {
   commonexist :common;
   combineexist :('a, 'a, 'a) op2; (*Combining operation when a decision is eliminated*)
}
val make_exist : ?memo:Cudd.Memo.t -> ('a, 'a, 'a) op2 -> 'a exist
Make an existential quantification operation, with the given memoization policy, and the given underlying binary operation, assumed to be commutative and idempotent, that combines the two branch of the diagram when a decision is quantified out.
val apply_exist : 'a exist -> supp:Cudd.Bdd.vt -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t

Example:

Still assuming type t = bool Vdd.t and corresponding diagrams bdd:t

We define ordinary existential quantification with

let dor = make_op2 ~commutative:true ~idempotent:true ( || );;
  let exist = make_exist dor;;
  let res = apply_exist exist ~supp bdd;;
  

We can define ordinary universal quantification by replacing || with &&.

Quantification combined with intersection


type 'a existand = private 'a Cudd.Custom.existand = private {
   commonexistand :common;
   combineexistand :('a, 'a, 'a) op2; (*Combining operation when a decision is eliminated*)
   bottomexistand :'a; (*Value returned when intersecting with Bdd.dfalse*)
}
val make_existand : ?memo:Cudd.Memo.t ->
bottom:'a -> ('a, 'a, 'a) op2 -> 'a existand
val apply_existand : 'a existand ->
supp:Cudd.Bdd.vt -> Cudd.Bdd.vt -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t

existand ~bottom op2 supp bdd f is equivalent to exist op2 supp (ite bdd f bottom).

The leaf operation op2:'a -> 'a -> 'a is assumed to be commutative, idempotent, and also op2 f bottom = f.

Quantification combined with unary operation


type ('a, 'b) existop1 = private ('a, 'b) Cudd.Custom.existop1 = private {
   commonexistop1 :common;
   combineexistop1 :('b, 'b, 'b) op2; (*Combining operation when a decision is eliminated*)
   existop1 :('a, 'b) op1; (*Unary operations applied before elimination*)
}
val make_existop1 : ?memo:Cudd.Memo.t ->
op1:('a, 'b) op1 ->
('b, 'b, 'b) op2 -> ('a, 'b) existop1
val apply_existop1 : ('a, 'b) existop1 ->
supp:Cudd.Bdd.vt -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t

Type of unary operation, conjunction and quantification

existop1 op1 op2 supp f is equivalent to exist op2 supp (op1 f).

The leaf operation op2:'b -> 'b -> 'b is assumed to be commutative and idempotent.

Quantification combined with intersection and unary operation


type ('a, 'b) existandop1 = private ('a, 'b) Cudd.Custom.existandop1 = private {
   commonexistandop1 :common;
   combineexistandop1 :('b, 'b, 'b) op2; (*Combining operation when a decision is eliminated*)
   existandop1 :('a, 'b) op1; (*Unary operations applied before elimination*)
   bottomexistandop1 :'b; (*Value returned when intersecting with Bdd.dfalse*)
}
val make_existandop1 : ?memo:Cudd.Memo.t ->
op1:('a, 'b) op1 ->
bottom:'b -> ('b, 'b, 'b) op2 -> ('a, 'b) existandop1
val apply_existandop1 : ('a, 'b) existandop1 ->
supp:Cudd.Bdd.vt -> Cudd.Bdd.vt -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t

existandop1 ~bottom op op1 supp bdd f is equivalent to exist op2 supp (ite bdd (op1 f) bottom)).

The leaf operation op2:'b -> 'b -> 'b is assumed to be commutative, idempotent, and also op2 f bottom = f.

Clearing memoization tables


val clear_common : common -> unit
val clear_op1 : ('a, 'b) op1 -> unit
val clear_op2 : ('a, 'b, 'c) op2 -> unit
val clear_op3 : ('a, 'b, 'c, 'd) op3 -> unit
val clear_opN : ('a, 'b) opN -> unit
val clear_opG : ('a, 'b) opG -> unit
val clear_test2 : ('a, 'b) test2 -> unit
val clear_exist : 'a exist -> unit
val clear_existand : 'a existand -> unit
val clear_existop1 : ('a, 'b) existop1 -> unit
val clear_existandop1 : ('a, 'b) existandop1 -> unit

Map operations



These operations combine make_opXXX and apply_opXXX operations.

if ?memo=None, then a hash table is used, and cleared at the end.

val map_op1 : ?memo:Cudd.Memo.t -> ('a -> 'b) -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t
val map_op2 : ?memo:Cudd.Memo.t ->
?commutative:bool ->
?idempotent:bool ->
?special:('a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t option) ->
('a -> 'b -> 'c) -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t
val map_op3 : ?memo:Cudd.Memo.t ->
?special:('a Cudd.Vdd.t ->
'b Cudd.Vdd.t -> 'c Cudd.Vdd.t -> 'd Cudd.Vdd.t option) ->
('a -> 'b -> 'c -> 'd) ->
'a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t -> 'd Cudd.Vdd.t
val map_opN : ?memo:Cudd.Memo.t ->
(Cudd.Bdd.vt array -> 'a Cudd.Vdd.t array -> 'b Cudd.Vdd.t option) ->
Cudd.Bdd.vt array -> 'a Cudd.Vdd.t array -> 'b Cudd.Vdd.t
val map_test2 : ?memo:Cudd.Memo.t ->
?symetric:bool ->
?reflexive:bool ->
?special:('a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> bool option) ->
('a -> 'b -> bool) -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> bool