]> matita.cs.unibo.it Git - helm.git/commitdiff
New algorithm based on in-place modification of the graph.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 12 Mar 2009 00:08:54 +0000 (00:08 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 12 Mar 2009 00:08:54 +0000 (00:08 +0000)
Conjecture solved in the negative:

(CMM?)+ | (MM?C)+

cCw = Cw
-Cw = MCw
cMw = CMw
-MMw = -w
-MCw = MMCw
iw = w

helm/software/matita/contribs/formal_topology/bin/Makefile
helm/software/matita/contribs/formal_topology/bin/comb.ml

index a9298a9212fc5e8c24befa438f0ad2f08052aedb..4b532e262ba8625792b350ea57f3db83bc1b48ed 100644 (file)
@@ -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
index e89deaeebae75fb61c75e796e9df42f138df6c3f..5734c618d9b4126f92af9ec6cb62f6f8e3b737f5 100755 (executable)
@@ -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 ("<scc>");
- 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 ("<scc>");
+  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 ("</scc>");
+  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])
 ;;