From: Claudio Sacerdoti Coen Date: Thu, 12 Mar 2009 00:08:54 +0000 (+0000) Subject: New algorithm based on in-place modification of the graph. X-Git-Tag: make_still_working~4153 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cb99a2022db2d4731679912db78fba002c1acb5c;p=helm.git New algorithm based on in-place modification of the graph. Conjecture solved in the negative: (CMM?)+ | (MM?C)+ cCw = Cw -Cw = MCw cMw = CMw -MMw = -w -MCw = MMCw iw = w --- diff --git a/helm/software/matita/contribs/formal_topology/bin/Makefile b/helm/software/matita/contribs/formal_topology/bin/Makefile index a9298a921..4b532e262 100644 --- a/helm/software/matita/contribs/formal_topology/bin/Makefile +++ b/helm/software/matita/contribs/formal_topology/bin/Makefile @@ -1,2 +1,2 @@ comb: comb.ml - ocamlfind ocamlc -g -linkpkg -package ocamlgraph,unix -o comb comb.ml + ocamlfind ocamlopt -g -linkpkg -package ocamlgraph,unix -o comb comb.ml diff --git a/helm/software/matita/contribs/formal_topology/bin/comb.ml b/helm/software/matita/contribs/formal_topology/bin/comb.ml index e89deaeeb..5734c618d 100755 --- a/helm/software/matita/contribs/formal_topology/bin/comb.ml +++ b/helm/software/matita/contribs/formal_topology/bin/comb.ml @@ -1,12 +1,21 @@ -(* 0: 7 4 - 1: 29 6 - 2: 120 10 - 3: > 327 >9 - 4: > 657 >9 - 5: > 526 >8 +(* 0: 7 4 0.312 3 5 7 + 1: 29 6 0.549 3 8 16 24 29 + 2: 120 10 25.525 3 8 19 39 66 95 113 119 120 + 3: > 327 >9 3 8 19 39 75 134 208 274 + 4: > 657 >9 3 8 19 39 75 139 245 + 5: > 526 >8 3 8 19 39 75 139 245 6: > 529 >8 7: > 529 >8 8: > 529 >8 + +(CMM?)+ | (MM?C)+ + +cCw = Cw +-Cw = MCw +cMw = CMw +-MMw = -w +-MCw = MMCw +iw = w *) type t = M | I | C @@ -40,25 +49,22 @@ let rules = ;; let inject = + let cache = Hashtbl.create 5393 in function w -> - let rec aux acc = - function - [] -> acc - | he::tl -> aux (4 * acc + (match he with I -> 1 | C -> 2 | M -> 3)) tl - in - 0, aux 0 w, w + try + Hashtbl.find cache w + with + Not_found -> + let rec aux acc = + function + [] -> acc + | he::tl -> aux (4 * acc + (match he with I -> 1 | C -> 2 | M -> 3)) tl + in + let res = 0, aux 0 w, w in + Hashtbl.add cache w res; + res ;; -module V = - struct - type t = int * int * w - let compare (h1,l1,_) (h2,l2,_) = compare (h1,l1) (h2,l2) - let hash (_,l,_) = l - let equal ((h1 : int),(l1 : int),_) (h2,l2,_) = l1=l2 && h1=h2 - end - -module G = Graph.Imperative.Digraph.Concrete(V);; - module VL = struct type t = eqclass @@ -150,7 +156,7 @@ let step (l : w list) = (List.map (function w -> List.map (fun x -> x@w) - (if List.length (List.filter (fun w -> w = M) w) >= 1 then + (if List.length (List.filter (fun w -> w = M) w) >= 5 then [[I];[C]] else [[I];[C];[M]]) @@ -190,19 +196,28 @@ let iteri f l = print_newline (); ;; -let normalize (l : w list) = +let normalize canonical (l : w list) = print_endline (string_of_int (List.length l) ^ " nodes to be normalized"); - let rels = - List.flatten - (mapi (fun x -> apply_rules (x,Le) @ apply_rules (x,Ge)) l) in - let arcs = - mapi - (function (x,rel,y) -> - let x = inject x in - let y = inject y in - match rel with Le -> x,y | Ge -> y,x) rels + let rec aux all l = + let rels = + List.flatten + (mapi (fun x -> apply_rules (x,Le) @ apply_rules (x,Ge)) l) in + let arcs = + mapi + (function (x,rel,y) -> + let x = canonical x(*(inject x)*) in + let y = canonical y(*(inject y)*) in + match rel with Le -> x,y | Ge -> y,x) rels in + let res = uniq arcs in + let nodes = uniq (l @ List.map (fun (_,_,n) -> n) rels) in + let new_nodes = List.filter (fun n -> not (List.mem n all)) nodes in + let new_nodes = List.filter (function n -> [n] = canonical n) new_nodes in + if new_nodes = [] then + res + else + uniq (res @ aux nodes new_nodes) in - uniq arcs + aux l l ;; let visualize graph = @@ -231,70 +246,63 @@ let w_compare s1 s2 = if c = 0 then compare s1 s2 else c ;; -let normalize_and_describe norm = - let cache = Hashtbl.create 5393 in - let canonicals = Hashtbl.create 5393 in - let descriptions = Hashtbl.create 5393 in - (function v -> - let normalized = norm v in - let _,_,dsc = G.V.label v in - if not (List.mem dsc (Hashtbl.find_all cache normalized)) then - Hashtbl.add cache normalized dsc; - normalized), - (function () -> - let vertexes = uniq (Hashtbl.fold (fun k _ l -> k::l) cache []) in - let xx = - mapi - (fun v -> v, List.sort w_compare (Hashtbl.find_all cache v)) vertexes in - iteri (function (_,w::_) -> Hashtbl.add canonicals w () | _ -> ()) xx; - let is_not_redundant = - function - [] | [_] -> true - | _::w -> - try Hashtbl.find canonicals w; true with Not_found -> false - in - iteri - (function (v,x) -> - Hashtbl.add descriptions v ((List.filter is_not_redundant x) : eqclass)) xx), - Hashtbl.find descriptions -;; - -let classify arcs = - print_endline (string_of_int (List.length arcs) ^ " arcs to be classified"); - let graph = G.create () in - iteri (fun (x,y) -> G.add_edge graph x y) arcs; - print_endline (""); - let classes,norm = - let module SCC = Graph.Components.Make(G) in SCC.scc graph in - print_endline (string_of_int classes ^ " classes"); - print_endline ("-----"); - norm,arcs -;; - -let analyze (norm,arcs) = - print_endline ("building class graph (" ^ string_of_int (List.length arcs) ^ ")"); - let normalize,finish,describe = normalize_and_describe norm in - let arcs = uniq (mapi (fun (x,y) -> normalize x,normalize y) arcs) in - print_endline "finish"; - finish (); - print_endline ("collapse " ^ string_of_int (List.length arcs) ^ " arcs"); - let arcs = uniq (mapi (function (x,y) -> describe x,describe y) arcs) in - print_endline ("build (" ^ string_of_int (List.length arcs) ^ " arcs)"); - let cgraph = GL.create () in - iteri (function (x,y) -> if x <> y then GL.add_edge cgraph x y) arcs; - print_endline "visualize"; - visualize cgraph; - print_endline ("/////"); -;; +exception Found of GL.V.t;; -let rec iter n nodes old_arcs = +let rec iter n cgraph (canonical: w -> GL.V.t) = print_endline ("STEP " ^ string_of_int n); - let arcs = old_arcs @ normalize nodes in - let pkg = classify arcs in - if n > 0 then - iter (n - 1) (step nodes) arcs - else - analyze pkg + let nodes = GL.fold_vertex (fun n l -> n::l) cgraph [] in + let nodes = step (List.map List.hd nodes) in +(*let nodes = [[C;M];[C;M;C;M];[C;M;C;M;C;M];[C;M;C;M;C;M;C;M];[C;M;C;M;C;M;C;M;C;M]] in*) +(*let nodes = [[C;I;C;I;C;I]] in*) + (*let nodes = step (List.concat nodes) in*) +(*List.iter (fun x -> prerr_endline ("#@ " ^ string_of_w x)) nodes;*) + let arcs = normalize canonical nodes in + iteri (fun (x,y) -> if x <> y then GL.add_edge cgraph x y) arcs; +(*List.iter (fun (x,y) -> prerr_endline (string_of_eqclass x ^ " -> " ^ string_of_eqclass y)) arcs;*) + + print_endline (""); + let classes,norm = + let module SCC = Graph.Components.Make(GL) in SCC.scc cgraph in + let xxx = + let module SCC = Graph.Components.Make(GL) in SCC.scc_array cgraph in + print_endline (""); + let get_canonical n = + try List.sort w_compare (List.concat (xxx.(norm n))) + with Not_found -> n + in + let nodes = GL.fold_vertex (fun n l -> n::l) cgraph [] in + print_endline "get_canonical"; + let nodes = mapi (fun n -> n,get_canonical n) nodes in + print_endline "/get_canonical"; + print_endline ("collapse " ^ string_of_int (List.length nodes)); + iteri + (function (n,n') -> + let succ = GL.succ cgraph n in + let pred = GL.pred cgraph n in + GL.remove_vertex cgraph n; + let add_edge s t = if s <> t then GL.add_edge cgraph s t in + List.iter (fun s -> add_edge n' (get_canonical s)) succ; + List.iter (fun p -> add_edge (get_canonical p) n') pred) + nodes; + print_endline (string_of_int classes ^ " classes"); + print_endline ("-----"); + print_endline "visualize"; + visualize cgraph; + print_endline ("/////"); + GL.iter_vertex (fun l -> print_endline ("?" ^ string_of_eqclass l)) cgraph; + let canonical = + function (*_,_,*)w -> + try + GL.iter_vertex (fun l -> if List.mem w l then raise (Found l)) cgraph; + [w] + with + Found l -> l in + if n > 0 then + iter (n - 1) cgraph canonical + else + () in - iter 7 [[]] [] + let cgraph = GL.create () in + GL.add_vertex cgraph [[]]; + iter 9 cgraph (fun w(*(_,_,w)*) -> [w]) ;;