type 'codomain mtbdd = Value of 'codomain | Undefined | Node of 'codomain mtbdd * 'codomain mtbdd exception Duplicate_def exception Multiple_def let empty = Undefined let create_node compare st_true st_false = match (st_true,st_false) with (Value val_true), (Value val_false) when (compare val_true val_false) -> Value val_true | _ -> Node(st_true, st_false) let rec add (compare : 'codomain->'codomain->bool) (key : bool list) (value : 'codomain) (mtbdd : 'codomain mtbdd) = match key with [] -> begin match mtbdd with Undefined -> Value value | _ -> raise Duplicate_def end | head::tail -> begin match mtbdd with Undefined -> let subtree = add compare tail value Undefined in if head then Node(subtree, Undefined) else Node(Undefined, subtree) | Node(st_true, st_false) -> if head then create_node compare (add compare tail value st_true) st_false else create_node compare st_true (add compare tail value st_false) | Value _ -> raise Duplicate_def end let rec find (key : bool list) = function Value value -> value | Undefined -> raise Not_found | Node(st_true, st_false) -> begin match key with [] -> raise Multiple_def | head::tail -> find tail (if head then st_true else st_false) end let create_node_compactify compare st_true st_false = match (st_true,st_false) with (Value val_true), (Value val_false) when (compare val_true val_false) -> Value val_true | Undefined, ((Value _) as result) -> result | ((Value _) as result), Undefined -> result | _ -> Node(st_true, st_false) let rec compactify compare = function Node(st_true, st_false) -> create_node_compactify compare (compactify compare st_true) (compactify compare st_false) | x -> x let rec fprint prefix separator codomain_fprint channel = function Value value -> Printf.fprintf channel "%s -> %a%s" prefix codomain_fprint value separator | Node(st_true, st_false) -> fprint (prefix ^ "1") separator codomain_fprint channel st_true; fprint (prefix ^ "0") separator codomain_fprint channel st_false | Undefined -> () let compare (x : int) (y : int) = (x = y) let bdd = List.fold_left (fun bdd (key, value) -> add compare key value bdd) empty [ [false; false; false], 0; [true ; false; false], 1; [false; false; true ], 0; [true ; false ; true], 2 ];; let print = fprint "" "\n" (fun channel x -> Printf.fprintf channel "%d" x) stdout;; print bdd;; print (compactify compare bdd);;