Commit d1a25cde by Kim Nguyễn

### Implement some semantic simplification of BDDs. This fixes the exponential...

`Implement some semantic simplification of BDDs. This fixes the exponential beahviour during the typing of the application of flatten.`
parent a8f46774
 ... ... @@ -98,8 +98,8 @@ struct | _ -> () let rec dump ppf = function | True -> Format.fprintf ppf "⊤" | False -> Format.fprintf ppf "⊥" | True -> Format.fprintf ppf "⊤" | Split (_,x, p,i,n) -> Format.fprintf ppf "@[@[%a@][@[%a,@\n%a,@\n%a@]]@]" X.dump x dump p dump i dump n ... ...
 ... ... @@ -2,11 +2,12 @@ let flatten_all (l : X where X = [ ( 'a \ [Any*] | X)* ]) : [ ( 'a \ [Any*] )* match l with [] -> [] | (e \[Any*], ll) -> (e, flatten_all ll) | (ll1, ll2) -> (flatten_all ll1) @ (flatten_all ll2) | (ll1, ll2) -> flatten_all (ll1 @ ll2) ;; let v = flatten_all [ [ [ `A ] ] ] ;; let v = flatten_all [ `A [ `B `C [`D]] [[[[[[[[[[[[[[[[[[[[[[[[[[1]]]]]]]]]]]]]]]]]]]]]]]]] ]] \ No newline at end of file ]]
 ... ... @@ -19,6 +19,7 @@ module type S = sig val pp_print : Format.formatter -> t -> unit val print : ?f:(Format.formatter -> elem -> unit) -> t -> (Format.formatter -> unit) list val extract : t -> [ `Empty | `Full | `Split of (elem * t * t * t) ] end ... ... @@ -119,8 +120,8 @@ module Make (T : Bool.S) : S with module Atom = T and type elem = T.t Var.var_or | _ -> () let rec dump ppf = function | True -> Format.fprintf ppf "⫧" | False -> Format.fprintf ppf "⫨" | False -> Format.fprintf ppf "⊥" | True -> Format.fprintf ppf "⊤" | Split (_,x, p,i,n) -> let fmt = format_of_string ( match x with ... ... @@ -382,4 +383,10 @@ module Make (T : Bool.S) : S with module Atom = T and type elem = T.t Var.var_or let cap = ( ** ) let diff = ( // ) let extract = function | False -> `Empty | True -> `Full | Split (_,x,p,i,n) -> `Split (x,p,i,n) end
 ... ... @@ -16,6 +16,7 @@ module type S = sig val print : ?f:(Format.formatter -> elem -> unit) -> t -> (Format.formatter -> unit) list val extract : t -> [ `Empty | `Full | `Split of (elem * t * t * t) ] end module Make : functor (T : Bool.S) -> S with module Atom = T and type elem = T.t Var.var_or_atom
 ... ... @@ -141,23 +141,6 @@ module BoolAbstracts = BoolVar.Make(Abstracts) module rec Descr : sig (* each kind is represented as a union of itersection of types * the type is a union of all kinds * * we add a new field that contains only variables. * Inv : * if the bdd of ANY kind is composed only of variables, the we move it in vars: * From a bdd we move all variables to vars: that belong to * to a path in the bdd that contains only variables and end in * true * A bdd never contains a path that ends in 1 and contains only variables * * (t1 v a ) ^ ( t2 v b ) * we need to distribute variables for the intersection * (t1 ^ t2) v (t1 ^ b) v (t2 ^ a) v (a ^ b) * before we were doing only t1 ^ t2 *) type s = { atoms : BoolAtoms.t; ints : BoolIntervals.t; ... ... @@ -167,9 +150,6 @@ sig arrow : BoolPair.t; record: BoolRec.t; abstract: BoolAbstracts.t; (* this is used in record to flag the fact that the type of a label is * absent . It is used for optional arguments in functions as ?Int * is the union of Int ^ undef where undef is a type with absent : true *) absent: bool; } include Custom.T with type t = s ... ... @@ -224,10 +204,6 @@ struct absent = false; } (* * Two representations possible. Either all fields (except vars) are full, OR * the field vars is full. *) let any = { times = BoolPair.full; xml = BoolPair.full; ... ... @@ -1590,6 +1566,112 @@ module Iter = (BoolRec.compute ~empty ~full:any_record ~cup ~cap ~diff ~atom:(var_or record_bdd) t.record);] let simplify t = let aux (type bdd) (type atom) inj (module BV : BoolVar.S with type t = bdd and type Atom.t = atom ) b = let clean b = if is_empty (inj b) then BV.empty else b in let rec loop b = match BV.extract b with `Split(`Var v, p, i , n) -> let p = loop p in let i = loop i in let n = loop n in let tp = inj p and tn = inj n in if disjoint tp tn then b else let v' = clean (BV.var v) in let p' = clean BV.(cap v' (diff p n)) in let n' = clean BV.(diff (diff n p) v') in let i' = clean (BV.cap n p) in let i'' = clean (BV.cup i i') in BV.(cup i'' (cup p' n')) | _ -> b in loop b in { t with atoms = aux (fun i -> { empty with atoms = i }) (module BoolAtoms) t.atoms; chars = aux (fun i -> { empty with chars = i }) (module BoolChars) t.chars; ints = aux (fun i -> { empty with ints = i }) (module BoolIntervals) t.ints; abstract = aux (fun i -> { empty with abstract = i }) (module BoolAbstracts) t.abstract; times = aux (fun i -> { empty with times = i }) (module BoolPair) t.times; xml = aux (fun i -> { empty with xml = i }) (module BoolPair) t.xml; arrow = aux (fun i -> { empty with arrow = i }) (module BoolPair) t.arrow; record = aux (fun i -> { empty with record = i }) (module BoolRec) t.record; } let compute_bdd ~typ ~cup ~cap ~neg ~var ~atoms ~ints ~chars ~times ~xml ~arrow ~record ~abstract ~absent t = let t = simplify t in let any_node2 = any_node, any_node in let any_atoms = atoms Atoms.full in let any_ints = ints Intervals.full in let any_chars = chars Chars.full in let any_abstract = abstract Abstracts.full in let any_times = times any_node2 in let any_xml = xml any_node2 in let any_record = record (true,LabelMap.empty) in let any_arrow = typ Arrow.any (*neg (cup ([ any_atoms; any_ints; any_chars; any_abstract; any_times; any_xml; any_record ])) *) in let var_or do_atom = function `Var v -> var v | `Atm atm -> do_atom atm in let simple_bdd (type bdd) (type atom) any do_atom (module B : Bool.S with type t = bdd and type elem = atom) acc bv = List.fold_left (fun acc (ipos, ineg) -> match List.map do_atom ipos, List.map do_atom ineg with | [] , [] -> any :: acc | [ e ] , [] -> e :: acc | [], l -> cap (any :: List.map neg l) :: acc | l1, l2 -> cap (l1 @ List.map neg l2) :: acc ) acc (B.get bv) in let cplx_bdd (type bdd) (type atom) (type atom2) any do_atom (module BV : BoolVar.S with type t = bdd and type Atom.t = atom and type Atom.elem = atom2) acc bdd = simple_bdd (cap[]) (var_or (fun t -> cup (simple_bdd (any) do_atom (module BV.Atom) [] t))) (module BV) acc bdd in let acc = absent t.absent in let acc = simple_bdd any_ints (var_or ints) (module BoolIntervals) acc t.ints in let acc = simple_bdd any_atoms (var_or atoms) (module BoolAtoms) acc t.atoms in let acc = simple_bdd any_chars (var_or chars) (module BoolChars) acc t.chars in let acc = simple_bdd any_abstract (var_or abstract) (module BoolAbstracts) acc t.abstract in let acc = cplx_bdd any_times times (module BoolPair) acc t.times in let acc = cplx_bdd any_xml xml (module BoolPair) acc t.xml in let acc = cplx_bdd any_arrow arrow (module BoolPair) acc t.arrow in let acc = cplx_bdd any_record record (module BoolRec) acc t.record in match acc with [ e ] -> e | _ -> cup acc end module Variable = ... ... @@ -1664,13 +1746,100 @@ module Variable = in loop t let collect_vars2 t = let memo = DescrHash.create 17 in let empty3 = Var.Set.(empty,empty,empty) in let merge l = List.fold_left (fun (a1, a2, a3) (s1, s2, s3) -> Var.Set.(cup a1 s1, cup a2 s2, cup a3 s3)) empty3 l in let cst_empty3 _ = empty3 in let rec loop t = try DescrHash.find memo t with Not_found -> DescrHash.add memo t empty3; let res = Iter.compute_bdd ~typ:cst_empty3 ~cup:merge ~cap:merge ~neg:(fun (a, b, c) -> (a , c , b)) ~var:(fun v -> let e = Var.Set.singleton v in e,e,Var.Set.empty) ~ints:cst_empty3 ~chars:cst_empty3 ~atoms:cst_empty3 ~abstract:cst_empty3 ~xml:prod ~times:prod ~arrow:arrow ~record:record ~absent:(fun _ -> []) t in DescrHash.replace memo t res; res and prod (t1, t2) = let _,y1,z1 = loop (descr t1) and _,y2,z2 = loop (descr t2) in Var.Set.(empty, cup y1 y2, cup z1 z2) and arrow (t1, t2) = let _,y1,z1 = loop (descr t1) and _,y2,z2 = loop (descr t2) in Var.Set.(empty, cup z1 y2, cup y1 z2) and record (b, lm) = let _, y, z = merge (List.map (fun (_,t) -> (loop (descr t))) (LabelMap.get lm)) in Var.Set.empty, y, z in loop t let no_var t = let memo = DescrHash.create 17 in let rec loop t = try DescrHash.find memo t with Not_found -> DescrHash.add memo t (); Iter.compute_bdd ~typ:ignore ~cup:ignore ~cap:ignore ~neg:ignore ~var:(fun _ -> raise Not_found) ~ints:ignore ~chars:ignore ~atoms:ignore ~abstract:ignore ~xml:prod ~times:prod ~arrow:prod ~record:record ~absent:(fun _ -> []) t and prod (t1, t2) = loop (descr t1); loop (descr t2) and record (b, lm) = List.iter (fun (_,t) -> (loop (descr t))) (LabelMap.get lm) in try loop t; true with Not_found -> false let collect_vars t = let extract = function Some e -> e | None -> Var.Set.empty in let _extract = function Some e -> e | None -> Var.Set.empty in try DescrHash.find var_cache t with Not_found -> let tlv, pos, neg = collect_vars t in let tlv, pos, neg = extract tlv, extract pos, extract neg in let tlv, pos, neg = collect_vars2 t in (* let tlv, pos, neg = extract tlv, extract pos, extract neg in *) let res = tlv, pos, neg, Var.Set.cup pos neg in DescrHash.add var_cache t res; res ... ... @@ -1679,7 +1848,16 @@ module Variable = let _, _, _, all = collect_vars t in all let is_ground t = Var.Set.is_empty (all_vars t) let is_ground = let h = DescrHash.create 17 in fun t -> try DescrHash.find h t with Not_found -> let b = no_var t in DescrHash.add h t b; b (* let is_ground t = Var.Set.is_empty (all_vars t) *) let no_var = is_ground let is_closed delta t = ... ... @@ -1721,6 +1899,7 @@ module Variable = | _ -> raise (Invalid_argument "Variable.extract") let extract_variable = extract end let is_var = Variable.is_var ... ... @@ -1940,6 +2119,7 @@ module Print = struct VarTable.replace table key (set old_t new_a)) (BV.get (get t)) in let h = VarTable.create 17 in let d = Iter.simplify d in fill_line (module BoolIntervals) h (fun t -> t.ints) (fun t u -> {t with ints = u }) d; fill_line (module BoolChars) h (fun t -> t.chars) (fun t u -> {t with chars = u }) d; fill_line (module BoolAtoms) h (fun t -> t.atoms) (fun t u -> {t with atoms = u }) d; ... ... @@ -1973,6 +2153,7 @@ module Print = struct ) h; h' with Not_found -> h in (* let tt, rm_keys = (* Simplify types of the form 'a & T | T \'a *) VarTable.fold (fun (v1, v2) tt1 ((acc_empty, acc_keys) as acc) -> ... ... @@ -1992,7 +2173,8 @@ module Print = struct in if non_empty tt then VarTable.replace h Key.empty tt; List.iter (fun (v1, v2) -> VarTable.remove h (v1, v2); VarTable.remove h (v2, v1)) rm_keys; VarTable.remove h (v2, v1)) rm_keys; *) let found_any, all_descrs = try let res = ... ... @@ -2042,6 +2224,8 @@ module Print = struct merge_columns ((factv, remv,t)::acc) nll in let all_descrs = merge_columns [] all_descrs in let inter_d l = match l with [] -> Neg (alloc []) ... ... @@ -2972,6 +3156,48 @@ module Positive = struct ~opt:(function true -> ty Record.absent | _ -> empty) t in loop t let decompose2 ?(stop=(fun _ -> None)) t = let memo = DescrHash.create 17 in let rec loop t = let res = try DescrHash.find memo t with Not_found -> let node_t = forward () in let () = DescrHash.add memo t node_t in let rhs = match stop t with | Some s -> s | None -> loop_struct t in node_t.def <- (rhs).def; node_t.descr <- Some t; node_t in res.descr <- Some t; res and loop_struct t = Iter.compute_bdd ~typ:ty ~cup ~cap ~neg ~var ~ints:interval ~chars:char ~atoms:atom ~abstract:abstract ~xml:(fun (t1, t2) -> xml (loop (descr t1)) (loop (descr t2))) ~times:(fun (t1, t2) -> times (loop (descr t1)) (loop (descr t2))) ~arrow:(fun (t1, t2) -> arrow (loop (descr t1)) (loop (descr t2))) ~record:(fun (b, lm) -> record b (List.map (fun (l,t) -> let t = descr t in t.absent, l, loop t) (LabelMap.get lm))) ~absent:(function true -> [ty Record.absent] | _ -> []) t in loop t end module Substitution = ... ... @@ -3005,7 +3231,7 @@ struct let decompose t = let open Positive in let res = decompose let res = decompose2 ~stop:(fun x -> if Variable.no_var x then Some (ty x) else if Variable.is_var t then let v, p = extract_variable t in ... ... @@ -3138,7 +3364,7 @@ struct let clean_type delta t = let res = clean_type delta t in DEBUG clean_type (Format.eprintf "@[ Calling clean_type(%a, %a) = %a@]@\n%!" DEBUG clean_type (Format.eprintf "@[ Calling clean_type(%a,@, %a) = %a@]@\n%!" Var.Set.pp delta Print.pp_type t Print.pp_type res); res ... ... @@ -3470,88 +3696,96 @@ module Tallying = struct module NormMemoHash = Hashtbl.Make(Custom.Pair(Descr)(Var.Set)) let memo_norm = NormMemoHash.create 17 let () = Format.pp_set_margin Format.err_formatter 100 let rec norm (t,delta,mem) = DEBUG normrec ( Format.eprintf " @[Entering norm rec(%a):@\n" Print.pp_type t); DEBUG normrec ( Format.eprintf " @[Entering norm rec(%a):@\n" Print.pp_type t); let res = try (* If we find it in the global hashtable, we are finished *) let res = NormMemoHash.find memo_norm (t, delta) in DEBUG normrec (Format.eprintf "@[ - Result found in global table @]@\n"); res with Not_found -> try let finished, cst = NormMemoHash.find mem (t, delta) in DEBUG normrec (Format.eprintf "@[ - Result found in local table, finished = %b @]@\n" finished); if finished then cst else CS.sat with Not_found -> begin let res = (* base cases *) if is_empty t then begin DEBUG normrec (Format.eprintf "@[ - Empty type case @]@\n"); CS.sat end else if no_var t then begin DEBUG normrec (Format.eprintf "@[ - No var case @]@\n"); CS.unsat end else if is_var t then begin let (v,p) = extract_variable t in if Var.Set.mem delta v then begin DEBUG normrec (Format.eprintf "@[ - Monomorphic var case @]@\n"); CS.unsat (* if it is monomorphic, unsat *) end else begin DEBUG normrec (Format.eprintf "@[ - Polymorphic var case @]@\n"); (* otherwise, create a single constraint according to its polarity *) let s = if p then (Pos (v,empty)) else (Neg (any,v)) in CS.singleton s try (* If we find it in the global hashtable, we are finished *) let res = NormMemoHash.find memo_norm (t, delta) in DEBUG normrec (Format.eprintf "@[ - Result found in global table @]@\n"); res with Not_found -> try let finished, cst = NormMemoHash.find mem (t, delta) in DEBUG normrec (Format.eprintf "@[ - Result found in local table, finished = %b @]@\n" finished); if finished then cst else CS.sat with Not_found -> begin let res = (* base cases *) if is_empty t then begin DEBUG normrec (Format.eprintf "@[ - Empty type case @]@\n"); CS.sat end else if no_var t then begin DEBUG normrec (Format.eprintf "@[ - No var case @]@\n"); CS.unsat end else if is_var t then begin let (v,p) = extract_variable t in if Var.Set.mem delta v then begin DEBUG normrec (Format.eprintf "@[ - Monomorphic var case @]@\n"); CS.unsat (* if it is monomorphic, unsat *) end else begin DEBUG normrec (Format.eprintf "@[ - Polymorphic var case @]@\n"); (* otherwise, create a single constraint according to its polarity *) let s = if p then (Pos (v,empty)) else (Neg (any,v)) in CS.singleton s end end else begin (* type is not empty and is not a variable *) DEBUG normrec (Format.eprintf "@[ - Inductive case:@\n"); let mem = NormMemoHash.add mem (t,delta) (false, CS.sat); mem in let t = Iter.simplify t in let aux single norm_aux acc l = big_prod delta (toplevel delta single norm_aux mem) acc l in let acc = aux single_atoms normatoms CS.sat (BoolAtoms.get t.atoms) in DEBUG normrec (Format.eprintf "@[ - After Atoms constraints: %a @]@\n" CS.pp_s acc); let acc = aux single_chars normchars acc (BoolChars.get t.chars) in DEBUG normrec (Format.eprintf "@[ - After Chars constraints: %a @]@\n" CS.pp_s acc); let acc = aux single_ints normints acc (BoolIntervals.get t.ints) in DEBUG normrec (Format.eprintf "@[ - After Ints constraints: %a @]@\n" CS.pp_s acc); let acc = aux single_times normpair acc (BoolPair.get t.times) in DEBUG normrec (Format.eprintf "@[ - After Times constraints: %a @]@\n" CS.pp_s acc); let acc = aux single_xml normpair acc (BoolPair.get t.xml) in DEBUG normrec (Format.eprintf "@[ - After Xml constraints: %a @]@\n" CS.pp_s acc); let acc = aux single_arrow normarrow acc (BoolPair.get t.arrow) in DEBUG normrec (Format.eprintf "@[ - After Arrow constraints: %a @]@\n" CS.pp_s acc); let acc = aux single_abstract normabstract acc (BoolAbstracts.get t.abstract) in DEBUG normrec (Format.eprintf "@[ - After Abstract constraints: %a @]@\n" CS.pp_s acc); (* XXX normrec is not tested at all !!! *) let acc = aux single_record normrec acc (BoolRec.get t.record) in DEBUG normrec (Format.eprintf "@[ - After Record constraints: %a @]@\n" CS.pp_s acc); let acc = (* Simplify the constraints on that type *) CS.S.filter (fun m -> CS.M.for_all (fun v (s, t) -> if Var.Set.mem delta v then (* constraint on a monomorphic variables must be trivial *) let x = var v in subtype s x && subtype x t else true (* subtype s t || (non_empty (cap s t)) *) ) m) acc in DEBUG normrec (Format.eprintf "@[ - After Filtering constraints: %a @]@\n" CS.pp_s acc); DEBUG normrec (Format.eprintf "@]@\n"); acc end end else begin (* type is not empty and is not a variable *) DEBUG normrec (Format.eprintf "@[ - Inductive case:@\n"); let mem = NormMemoHash.add mem (t,delta) (false, CS.sat); mem in let aux single norm_aux acc l = big_prod delta (toplevel delta single norm_aux mem) acc l in let acc = aux single_atoms normatoms CS.sat (BoolAtoms.get t.atoms) in DEBUG normrec (Format.eprintf "@[ - After Atoms constraints: %a @]@\n" CS.pp_s acc); let acc = aux single_chars normchars acc (BoolChars.get t.chars) in DEBUG normrec (Format.eprintf "@[ - After Chars constraints: %a @]@\n" CS.pp_s acc); let acc = aux single_ints normints acc (BoolIntervals.get t.ints) in DEBUG normrec (Format.eprintf "@[ - After Ints constraints: %a @]@\n" CS.pp_s acc); let acc = aux single_times normpair acc (BoolPair.get t.times) in DEBUG normrec (Format.eprintf "@[ - After Times constraints: %a @]@\n" CS.pp_s acc); let acc = aux single_xml normpair acc (BoolPair.get t.xml) in DEBUG normrec (Format.eprintf "@[ - After Xml constraints: %a @]@\n" CS.pp_s acc); let acc = aux single_arrow normarrow acc (BoolPair.get t.arrow) in DEBUG normrec (Format.eprintf "@[ - After Arrow constraints: %a @]@\n" CS.pp_s acc); let acc = aux single_abstract normabstract acc (BoolAbstracts.get t.abstract) in DEBUG normrec (Format.eprintf "@[ - After Abstract constraints: %a @]@\n" CS.pp_s acc); (* XXX normrec is not tested at all !!! *) let acc = aux single_record normrec acc (BoolRec.get t.record) in DEBUG normrec (Format.eprintf "@[ - After Record constraints: %a @]@\n" CS.pp_s acc);