(* * * Otto & Mezzo / ml * LRI - Equipe Architecture * Universite de Paris Sud - Orsay * Olivier MICHEL & Jean-Louis GIAVITTO * File: $RCSfile: bdd.ml,v $ * Path: %P% * Description: * Created: * Author: Olivier Michel & Jean-Louis Giavitto * Modified: $Date: 1997/04/21 11:23:36 $ at * Version: $Revision: 15.37 $ * Status: * * ------------------------------------------------------------------------------- * Ce module contient toutes les fonctions de manipulation des bdd (bientot robdd) * * L'operateur ite -> IfThenElse f g h * L'operateur de reduction d'un bdd en robdd ' * L'operateur de restriction d'une variable dans une fonction -> F| (F ou x=k) * |x <- k * Les operations de quantifications existentielle/universelle. * * Note: _ nous avons definis un 'a bdd_tree. On utilise la fonction arg.cmp pour comparer * les 'a, i. e. les labels (fct get_true et get_false). * * Il serait necessaire d'utiliser la fonction de comparaison de _arg_ pour * tester l'egalitee des labels, mais aussi les egalites de 'a bdd_tree qui * doivent se faire sur la structure (alors/sinon) **ET** sur les labels. * * _ *Attention* : on utilise une egalite physique ("=="), ce qui est correct. * Si on utilise l'egalite structurelle de ml, on risque de boucler dans * le cas ou le 'a est une structure circulaire car le "=" peut boucler. * ------------------------------------------------------------------------------- *) (* exception eBddError;; *) (* On ne cherche le label que sur un cnode, et on est sur d'avoir * un cnode (on est appelle par min_3_bdd qui elimine les terminaux * avant d'appeler get_cnode). *) let rec get_cnode_lbl = function cNode c -> c.label | cTerm _ -> raise (eBddError "cTerm in get_cnode_lbl") and get_true arg = fun x v -> (match x with cTerm b -> x | cNode {label=l; alors=a} -> if (0 == (arg.cmp l v)) then a else x) and get_false arg = fun x v -> (match x with cTerm b -> x | cNode {label=l; sinon=s} -> if (0 == (arg.cmp l v)) then s else x) and get_slot = function cNode node -> node.slot | _ -> raise (eBddError "get : Not a bdd node.") and set_slot val = function cNode node -> node.slot <- val | _ -> raise (eBddError "set : Not a bdd node.") and raz_slot arg = hashtbl__do_table (fun x (cNode node) -> node.slot <- (arg.init ()) | _ _ -> ()) arg.utbl (* Ajout dans une table de hash code d'un element s'il n'y est pas deja. * retourne cet element. *) and find_or_add = fun tbl expr -> try (hashtbl__find tbl expr) with Not_found -> (hashtbl__add tbl expr expr; expr) (* On match les cas terminaux qui sont resolus immediatement. 1,f,g ou 0,f,g ou f,1,0. *) and is_terminal_case = fun f g h -> (match f with cTerm val -> true (* On match (1,f,g) et (0,f,g) *) | _ -> (match g with cTerm true -> (match h with cTerm false -> true (* On match (f,1,0) *) | _ -> false) | _ -> false)) and is_cnode = function cNode _ -> true | _ -> false and is_cterm = function x -> not (is_cnode x) (* On _EST_ dans un cas terminal, on retourne le bon bdd. *) and term_val = fun f g h -> (match f with cTerm val -> if (val) then g else h (* C'est le cas (1,f,g) et (0,g,f) *) | _ -> f) (* C'est le cas (f,1,0) *) (* Retourne le plus petit de deux bdds *) and min_2_bdd arg = fun x y -> if (is_cterm x) then (get_cnode_lbl y) (* Si x est un terminal, alors le plus petit est y *) else if (is_cterm y) then (get_cnode_lbl x) (* Si y est un terminal, alors le plus petit est x *) else min_elt arg (get_cnode_lbl x) (get_cnode_lbl y) (* Sinon c'est le plus petit des deux *) (* Retourne : Le plus petit des 3 'a bdd en fonction de leur label. * Il est obligatoire que les bdd aient au moins un label, car sinon nous sommes dans un cas terminal * immediatement reduit et detecte dans is_terminal_case. On cherche ce cas terminal parmis les 3 que nous * avons en argument, en eliminant du choix tous les termes _terminaux_ (les puits TRUE ou FALSE). *) and min_3_bdd arg = fun x y z -> if (is_cterm x) then min_2_bdd arg y z (* elimine x qui est un terminal *) else if (is_cterm y) then min_2_bdd arg x z (* elimine y qui est un terminal *) else if (is_cterm z) then min_2_bdd arg x y (* elimine z qui est un terminal *) else min_elt arg (min_elt arg (get_cnode_lbl x) (get_cnode_lbl y)) (get_cnode_lbl z) (* On peut faire le min, car on 3 labels *) (* Retournent resp : Predicat vrai si le premier element est plus petit que le second, * Le plus petit de 2 elements. *) and inf arg x y = (arg.cmp x y) < 0 and min_elt arg = fun x y -> if (inf arg x y) then x else y and ite arg = fun f g h -> robdd arg (ite_r arg f g h) (* Pas necessaire de le faire car les bdds sont construits a partit d'elements en NF. let bef = ref (ite_r arg f g h) in let aft = ref (robdd arg !bef) in while (!bef <> !aft) do bef := !aft; aft := (robdd arg !bef) done; !aft *) (* Operateur tryadique If Then Else de Bryant. * on calcule le bdd resultanst de f g h. On elimines les cas terminaux le plus tot possible, * et on descends recursivements dans les bdd jusqu'a arriver a un cas terminal (True/False). * On gere deux tables de hash_code: _ la table des bdds pour le partage des sous graphes de bdd. * _ la table des bdds calcules qui correspond a un couple f g h * pour ne pas calculer deux fois une meme operation. * On retourne le bdd resultant de l'operation. *) and ite_r arg = fun f g h -> if (is_terminal_case f g h) then term_val f g h (* Si c'est un cas terminal -> on le reduit *) else begin try hashtbl__find arg.ctbl (f, g, h) (* Sinon, cela as-t-il deja ete calcule ? *) with Not_found -> begin let v = min_3_bdd arg f g h (* non -> trouver le label le + petit *) in (* trouver le bdd de la branche si *) let t = ite_r arg (get_true arg f v) (get_true arg g v) (get_true arg h v) (* trouver le bdd de la branche alors *) and e = ite_r arg (get_false arg f v) (get_false arg g v) (get_false arg h v) in begin if (compare_bdd arg t e) (** au lieu de t == e **) then t (* s'ils sont egaux -> on en elimine un *) else (let r = find_or_add arg.utbl (cNode {label=v; alors=t; sinon=e; slot = (arg.init ())}) in (hashtbl__add arg.ctbl (f, g, h) r; (* on ajoute le bdd calcule dans la table de hash code. *) r)) end end end (** Comparaison structurelle des bdd: ** 2 bdd sont structurellement egaux s'ils sont physiquement egaux ou bien ** si ils sont "structurellement" egaux. Le test d'egalite physique est redondant ** mais permet de ne pas explorer toute la structure dans le cas ou un bdd est ** partage (ce qui est souvent le cas avec les bdd). **) and compare_bdd arg a b = (a == b) or (compare_bdd_structure arg a b) and compare_bdd_structure arg = fun (cTerm x) (cTerm y) -> x = y | (cTerm _) (cNode _) -> false | (cNode _) (cTerm _) -> false | (cNode {label = l1; alors = a1; sinon = s1}) (cNode {label = l2; alors = a2; sinon = s2}) -> (0 == (arg.cmp l1 l2)) & (compare_bdd arg a1 a2) & (compare_bdd arg s1 s2) (* Implementation des operations unaires et binaires a l'aide * de l'operateur ite. *) and bdd_t = cTerm true and bdd_f = cTerm false and bdd_and arg = fun f g -> ite arg f g bdd_f and bdd_gt arg = fun f g -> ite arg f (bdd_not arg g) bdd_f and bdd_lt arg = fun f g -> ite arg f bdd_f g and bdd_xor arg = fun f g -> ite arg f (bdd_not arg g) g and bdd_or arg = fun f g -> ite arg f bdd_t g and bdd_nor arg = fun f g -> ite arg f bdd_f (bdd_not arg g) and bdd_xnor arg = fun f g -> ite arg f g (bdd_not arg g) (* _ *) and bdd_not arg = fun g -> ite arg g bdd_f bdd_t (* Note -> b :-> b _xor_ 1 *) and bdd_ge arg = fun f g -> ite arg f bdd_t (bdd_not arg g) and bdd_le arg = fun f g -> ite arg f g bdd_t and bdd_nand arg = fun f g -> ite arg f (bdd_not arg g) bdd_t and bdd_id = fun (f : ('a, 'b) bdd_tree) -> f and f_bdd_t = function x -> bdd_t (* Necessaire, en effet, on ne peut exporter bdd_t qui est ('a, 'b) bdd_t car 'b est un mutable, qui ne peut *) and f_bdd_f = function x -> bdd_f (* donc etre polymorphe (les mutables doivent etres des types concrets.) *) (* * Transformation d'un OBDD en ROBDD * par reduction/eradication des parties communes. * * Je ne suis pas sur que utiliser l'egalite structurelle soit necessaire, car comme on cherche * les bdd dns la table de hash-code, ils doivent etre unique (i.e. a ce niveau, egalite * structurelle = egalite physique). *) and robdd arg = fun f -> (match f with cTerm x -> find_or_add arg.utbl f (* Partage des terminaux *) | cNode {label = l; alors = a; sinon = s} -> if (compare_bdd arg a s) (** au lieu de: a==s **) then find_or_add arg.utbl (robdd arg s) (* Partage des non terminaux *) else find_or_add arg.utbl ( let nfa = find_or_add arg.utbl (robdd arg a) and nfs = find_or_add arg.utbl (robdd arg s) in ( (* Eradication des non terminaux avec fils identiques *) if (compare_bdd arg nfa nfs) (** au lieu de: nfa==nfs **) then (robdd arg nfs) else cNode {label = l; alors = nfa; sinon = nfs; slot = (arg.init ())} ) )) (* * Operation de restriction d'un ROBDD avec une variable (lbl) ayant pour valeur (val) * a.b+b.d avec a=true -> b+b.d (une variable est affectee, et le nouveaux bdd reduit). *) and restrict arg = fun bdd lbl val -> (let rec res_r = fun f lbl val -> (match f with cTerm x -> find_or_add arg.utbl f | cNode {label = l; alors = a; sinon = s} -> if (l=lbl) then find_or_add arg.utbl (res_r (if val then a else s) lbl val) else find_or_add arg.utbl (cNode{label = l; alors = res_r a lbl val; sinon = res_r s lbl val; slot = (arg.init ())})) in (match val with cTerm x -> robdd arg (res_r bdd lbl x) | _ -> raise (eBddError "restrict"))) (* * Operations de composition de deux bdd, de quantification universelle et existentielle, * d'implication. *) (* Operation de composition de la page 301 *) and compose arg = fun f x g -> bdd_or arg (bdd_and arg (bdd_not arg g) (restrict arg f x bdd_f)) (bdd_and arg g (restrict arg f x bdd_t)) (* Operation de quantification de variable de la page 301 *) and smooth arg = fun f x -> bdd_or arg (restrict arg f x bdd_f) (restrict arg f x bdd_t) (* Note -> Avec le bug corrige *) and consensus arg = fun f x -> bdd_and arg (restrict arg f x bdd_f) (restrict arg f x bdd_t) (* P => Q ie ((not P) + Q) tautologie *) and imply arg = fun p q -> ((bdd_or arg (bdd_not arg p) q) = bdd_t) (* P <=> Q ie P => Q et Q => P *) and equivalent arg = fun p q -> (imply arg p q) & (imply arg q p) (* Rends la liste de *tous* les 'a d'un bdd_tree. Il n'est pas necessaire d'utiliser un stamp pour l'anti-bouclage. En effet, * le graphe des bdd_trees est un dag qui vas toujours vers un puit. On enleve les doubles. *) and collect_r = function cTerm _ -> [] | cNode {label = l; alors = a; sinon = s} -> l::((bdd_collect a)@(bdd_collect s)) and bdd_collect f = global_fun__without_double (collect_r f) (******************************************************************************************************************) (******************************************************************************************************************) and generic_walk g comb = function cNode {label=l; alors=a; sinon=s} -> comb l a s | cTerm t -> g t and walk f g comb = function cNode {label=l; alors=a; sinon=s} -> comb (f l) (walk f g comb a) (walk f g comb s) | cTerm t -> g t and walk2 arg f g comb = function cNode {label=l; alors=a; sinon=s} -> comb arg (f arg l) (walk2 arg f g comb a) (walk2 arg f g comb s) | cTerm t -> g arg t and walk3 g comb = function cNode {label=l; alors=a; sinon=s; slot=arg} -> comb arg l a s | cTerm t -> g t and walk4 g comb = function cNode n -> comb n | cTerm t -> g t and walk5 g comb = function (cNode n) as cn -> comb n cn | cTerm t -> g t and print_bdd arg = function cTerm x -> if (x) then print_string "1" else print_string "0" | cNode {label=l; alors=a; sinon=s} -> print_string "("; arg.printer l; print_string ", "; print_bdd arg a; print_string ", "; print_bdd arg s; print_string ")" and print_log arg = function cTerm x -> print_string (if (x) then "1" else "0") (* l *) | cNode {label=l; alors=cTerm true; sinon=cTerm false } -> arg.printer l (* !l *) | cNode {label=l; alors=cTerm false; sinon=cTerm true } -> print_string "!"; arg.printer l (* !l.(...) *) | cNode {label=l; alors=cTerm false; sinon=s } -> print_string "!"; arg.printer l; print_string " . "; print_log arg s (* l+(!l.s) == (l+s) *) | cNode {label=l; alors=cTerm true; sinon=s } -> print_string "("; arg.printer l; print_string " + "; print_log arg s; print_string ")" (* l.a *) | cNode {label=l; alors=a; sinon=cTerm false } -> print_string "("; arg.printer l; print_string " . "; print_log arg a; print_string ")" (* !l+(l.a) == (!l+a) *) | cNode {label=l; alors=a; sinon=cTerm true } -> print_string "(!"; arg.printer l; print_string " + "; print_log arg a; print_string ")" (* (l.a + !l.s) *) | cNode {label=l; alors=a; sinon=s} -> print_string "("; arg.printer l; print_string "."; print_log arg a; print_string " + "; print_string "!"; arg.printer l; print_string "."; print_log arg s; print_string ")" (* Cree un ensemble de tous les elements d'une table de hash_code. * Enleve les elements se trouvant plus d'une fois. *) (* and cl arg = fun tbl -> let liste = ref arg.empty in hashtbl__do_table (fun x y -> liste := !liste @ [y]) tbl; global_fun__without_double !liste and print_uutbl arg = fun () -> do_list (function x -> arg.printer x; print_string "\n") (cl arg arg.utbl) *) ;; (* --- End ------------------------------------------------------- *)