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.

We register the operation:
let op = make_op1 ~memo:(Cache (Cache.create 1)) (fun b -> not b);;
Later we apply it on bdd1 and bdd2 with
let res1 = apply_op1 op bdd1 and res2 = apply_op1 op bdd2;;
The local cache is reused between the two calls to apply_op1, which is nice if bdd1 and bdd2 share common nodes. The cache is automatically garbage collected when needed. But even if diagrams in the caches entries may be garbage collected, the cache itself takes memory. You can clear it with Cache.clear or Memo.clear.
If ~memo::(Cache (Cache.create 1)) is replaced by ~memo::(Hash (Hash.create 1)), then diagrams in the table are referenced and cannot be gabage collected. You should clear them explicitly with Hash.clear or Memo.clear.
The third option is to use the CUDD global regular cache, which is automatically garbage collected when needed:
If the operation is applied only once to one diagram, it is simpler to write let res1 = map_op1 (fun b -> not b) bdd1;;

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

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