type i = int type t = Dis of i * i | Top | Bot | Ign of i let size = (ref (1000+7)) let hsh_form_to_int = Hashtbl.create (!size*100) let int_to_form = ref (Array.make (!size) Bot) let _ = (!int_to_form).(1) <- Top let cur_form = ref 1 let none = 0 let all = 1 let notsol = -1 let get_type n = (!int_to_form).(n) let resize nsize = int_to_form := Array.init nsize (fun i -> if i < !size then get_type i else Bot) ; size:=nsize (* ; print_string "Growing!" ; print_newline () *) let stat () = (!cur_form,!size) let add_type f = try Hashtbl.find hsh_form_to_int f with | Not_found -> incr cur_form ; if !cur_form = !size then resize (!size * 2 + 7) ; (!int_to_form).(!cur_form) <- f ; Hashtbl.add hsh_form_to_int f (!cur_form) ; (!cur_form) let add_type_ign i = if i <= 1 then i else add_type (Ign i) let add_type_dis (a,b) = if a = b then add_type_ign a else add_type (Dis (a,b)) let hsh_get_form = Hashtbl.create (!size) let get form = let rec foo form min_var i = if min_var > 0 && min_var < i then add_type_ign (foo form min_var (i+1)) else begin (* try Hashtbl.find hsh_get_form (i,form) with | Not_found -> *) let res = match form with | Bf.Top -> all | Bf.Bot -> none | _ -> let f1 = Bf.simplify (Bf.replace i Bf.Bot form) and f2 = Bf.simplify (Bf.replace i Bf.Top form) in if f1 = f2 then add_type_ign (foo f1 (Bf.get_min_var f1) (i+1)) else add_type_dis (foo f1 (Bf.get_min_var f1) (i+1), foo f2 (Bf.get_min_var f2) (i+1)) in (* Hashtbl.add hsh_get_form (i,form) res ;*) res end in foo (Bf.simplify form) (Bf.get_min_var form) 0 (* TODO : Memoize *) let hsh_inter = Hashtbl.create (!size) let rec inter a b = let foo () = match (get_type a,get_type b) with | Top,f -> b | f,Top -> a | Bot,_ | _,Bot -> none | Dis(a,b),Dis(c,d) -> add_type_dis (inter a c, inter b d) | Dis(a,b),Ign(c) | Ign(c),Dis(a,b) -> add_type_dis (inter a c, inter b c) | Ign(a), Ign(b) -> add_type_ign (inter a b) in if a<=1 || b<=1 then foo () else if a>b then inter b a else try Hashtbl.find hsh_inter (a,b) with | Not_found -> let res = foo () in Hashtbl.add hsh_inter (a,b) res ; res let cut side f = match get_type f with | Top -> all | Bot -> none | Ign(c) -> c | Dis(a,b) -> if side then b else a let print l = let rec iter p f = match get_type f with | Bot -> () | Top -> print_string p ; print_newline () | Dis(a,b) -> iter (p^"0") a ; iter (p^"1") b | Ign(c) -> iter (p^"*") c in iter "Sol : " l let mem a s = let rec foo i f = match get_type f with | Top -> true | Bot -> false | Ign(c) -> foo (i+1) c | Dis(f1,f2) -> if a.(i) then foo (i+1) f2 else foo (i+1) f1 in foo 0 s let add a s = let rec foo i l = if i = Array.length a then all else match get_type l with | Top -> all | Bot -> let f = foo (i+1) none in if a.(i) then add_type (Dis(none,f)) else add_type (Dis (f,none)) | Dis(f1,f2) -> let f1,f2 = if a.(i) then (f1,foo (i+1) f2) else (foo (i+1) f1, f2) in add_type_dis (f1,f2) | Ign(c) -> if a.(i) then add_type_dis (c,foo (i+1) c) else add_type_dis (foo (i+1) c,c) in foo 0 s let rec get_size c = match get_type c with | Bot -> 0 | Top -> 1 | Dis(a,b) -> get_size a + get_size b | Ign(c) -> 2*get_size c let prints = print_int