X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnAuto.ml;h=25f4e0fc70ff52c85f4e49f7630605fcae456bcc;hb=3ca99dabf7d136ebd58fa61e7a2d7134c8dc365c;hp=640128616719fdbeb76aa7eead5beed334e15e40;hpb=8e1b4eb6c9c8544f754b525d6cf2ba5ab0bf5396;p=helm.git

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index 640128616..25f4e0fc7 100644
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -13,7 +13,7 @@
 
 open Printf
 
-let debug = ref false
+let debug = ref true
 let debug_print ?(depth=0) s = 
   if !debug then prerr_endline (String.make depth '\t'^Lazy.force s) else ()
 let debug_do f = if !debug then f () else ()
@@ -1499,7 +1499,7 @@ let auto_main flags signature (pos : 'a and_pos) cache =
                  status pos cache 
 
   and attack pos cache and_item =
-    show pos; (* uncomment to show the tree *)
+    (* show pos; uncomment to show the tree *)
     match and_item with
     | _, S _ -> assert false (* next would close the proof or give a D *) 
     | _, L _ -> assert false (* L is a final solution *)
@@ -1618,6 +1618,40 @@ let auto_tac ~params:(_univ,flags) status =
     up_to depth depth
 ;;
 
+let rec rm_assoc n = function
+  | [] -> assert false
+  | (x,i)::tl when n=x -> i,tl
+  | p::tl -> let i,tl = rm_assoc n tl in i,p::tl
+;;
+
+let merge canonicals elements n m =
+  let cn,canonicals = rm_assoc n canonicals in
+  let cm,canonicals = rm_assoc m canonicals in
+  let ln,elements = rm_assoc cn elements in
+  let lm,elements = rm_assoc cm elements in
+  let canonicals = 
+    (n,cm)::(m,cm)::List.map 
+      (fun (x,xc) as p  -> 
+	 if xc = cn then (x,cm) else p) canonicals
+  in 
+  let elements = (cn,ln@lm)::elements 
+  in
+    canonicals,elements
+;;
+
+let clusters f l =
+  let canonicals = List.map (fun x -> (x,x)) l in
+  let elements = List.map (fun x -> (x,[x])) l in
+   List.fold_left 
+     (fun (canonicals,elements) x ->
+       let dep = f x in
+	 List.fold_left 
+	   (fun (canonicals,elements) d ->
+	      merge canonicals elements d x) 
+	   (canonicals,elements) dep)
+     (canonicals,elements) l
+;;
+
 let group_by_tac ~eq_predicate ~action:tactic status = 
  let goals = head_goals status#stack in
  if List.length goals < 2 then tactic status 
@@ -1674,7 +1708,11 @@ let auto_tac ~params =
 (* ========================= dispatching of auto/auto_paramod ============ *)
 let auto_tac ~params:(_,flags as params) =
   if List.mem_assoc "paramodulation" flags then 
-    auto_paramod_tac ~params  
+    auto_paramod_tac ~params 
+  else if List.mem_assoc "fast_paramod" flags then 
+    NnAuto.fast_eq_check_tac ~params  
+  else if List.mem_assoc "slir" flags then 
+    NnAuto.auto_tac ~params  
   else 
     auto_tac ~params
 ;;