X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnAuto.ml;h=53c87673bd165861c97ffb4e2564773ef4930725;hb=12f96bd48b460d06f9858a334ee7c52d6831712f;hp=fe45320dd6a333387f93ef7c090bbc73a8e4dec8;hpb=86b61210ee7354743c8015322a68a99f70550f46;p=helm.git

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index fe45320dd..53c87673b 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 ()
@@ -41,7 +41,7 @@ let auto_paramod ~params:(l,_) status goal =
     NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l 
   with
   | [] -> raise (Error (lazy "no proof found",None))
-  | (pt, metasenv, subst)::_ -> 
+  | (pt, _, metasenv, subst)::_ -> 
       let status = status#set_obj (n,h,metasenv,subst,o) in
       instantiate status goal (mk_cic_term (ctx_of gty) pt)
 ;;
@@ -1028,11 +1028,13 @@ type 'a op =
    * step *)
   | S of goal * (#tac_status as 'a)
          (* * cic_term * candidate (* int was minsize *) *)
+  | L of goal * (#tac_status as 'a)
 
 let pp_goal (g,_) = string_of_int g
 let pp_item = function
   | D g -> "D" ^ pp_goal g
   | S (g,_) -> "S" ^ pp_goal g 
+  | L (g,_) -> "L" ^ pp_goal g 
 
 type flags = {
         do_types : bool; (* solve goals in Type *)
@@ -1068,7 +1070,7 @@ let only _ _ _ = true;;
 let candidate_no = ref 0;;
 
 let sort_new_elems l = 
-  List.sort (fun (_,_,_,l1) (_,_,_,l2) -> List.length l1 - List.length l2) l
+  List.sort (fun (_,_,_,_,l1) (_,_,_,_,l2) -> List.length l1 - List.length l2) l
 ;;
 
 let try_candidate flags depth status t g =
@@ -1125,6 +1127,10 @@ let applicative_case depth signature status flags g gty cache =
   in
   elems
 ;;
+let calculate_goal_ty (goalno,_) status = 
+  try Some (get_goalty status goalno)
+  with Error _ -> None
+;;
 
 let equational_and_applicative_case
   signature flags status g depth gty cache 
@@ -1153,21 +1159,28 @@ let equational_and_applicative_case
       elems
  in
  let elems = 
-    (* XXX calculate the sort *)
-   List.map (fun c,s,gl -> c,1,s,List.map (fun i -> i,P) gl) elems 
+   List.map (fun c,s,gl -> 
+       c,1,1,s,List.map (fun i -> 
+                      let sort = 
+                       match calculate_goal_ty (i,()) s with
+                       | None -> assert false
+                       | Some gty ->
+                           let _, sort = typeof s (ctx_of gty) gty in
+                           match term_of_cic_term s sort (ctx_of sort) with
+                           | _, NCic.Sort NCic.Prop -> P
+                           | _ -> (*T*)P
+                      in
+               i,sort) gl) elems 
  in
  let elems = sort_new_elems elems in
  elems, cache
 ;;
 
-let calculate_goal_ty (goalno,_) status = 
-  try Some (get_goalty status goalno)
-  with Error _ -> None
-;;
+
 let d_goals l =
   let rec aux acc = function
     | (D g)::tl -> aux (acc@[g]) tl
-    | (S _)::tl -> aux acc tl
+    | (S _|L _)::tl -> aux acc tl
     | [] -> acc
   in
     aux [] l
@@ -1196,7 +1209,7 @@ let intro_case status gno gty depth cache name =
    debug_print ~depth (lazy ("intro: "^ string_of_int open_goal));
    incr candidate_no;
     (* XXX calculate the sort *)
-   [(!candidate_no,Ast.Implicit `JustOne),0,status,[open_goal,P]],
+   [(!candidate_no,Ast.Implicit `JustOne),0,0,status,[open_goal,P]],
    cache
 ;;
                       
@@ -1211,68 +1224,152 @@ let do_something signature flags s gno depth gty cache =
 module T = ZipTree
 module Z = AndOrTree
 
+let img_counter = ref 0 ;;
 let show pos =
-    debug_print (lazy("generating a.dot"));
+    incr img_counter;
+    let file = ("/tmp/a"^string_of_int !img_counter^".dot") in
+    debug_print (lazy("generating " ^ file));
     debug_do (fun () ->
-    let oc = open_out "/tmp/a.dot" in
+    let oc = open_out file in
     let fmt = Format.formatter_of_out_channel oc in
     GraphvizPp.Dot.header fmt;
     Z.dump pp_item pos fmt;
     GraphvizPp.Dot.trailer fmt;
     Format.fprintf fmt "@?";
     close_out oc;
-    ignore(Sys.command ("dot -Tpng /tmp/a.dot > /tmp/a.png")); 
-    ignore(Sys.command ("eog /tmp/a.png")))
+    ignore(Sys.command ("dot -Tpng "^file^" > "^file^".png")); 
+    (*ignore(Sys.command ("eog "^file^".png"))*))
 ;;
 
-let rightmost_bro pred =
- let rec fst pos = 
+let rightmost_bro pred pos =
+ let rec last acc pos = 
+   let acc = if pred pos then Some pos else acc in
    match Z.right pos with
-   | None ->  None
-   | Some pos -> 
-       if pred pos then Some pos else fst pos
+   | None -> acc
+   | Some pos -> last acc pos
  in
-   fst 
+   last None pos
 ;;
 
-let is_not_S pos = 
+let leftmost_bro pred pos =
+ let rec fst pos = 
+   if pred pos then Some pos else 
+     match Z.right pos with
+     | None ->  None
+     | Some pos -> fst pos
+ in
+   fst pos
+;;
+
+let rec first_left_mark_L_as_D pred pos =
+  if pred pos then 
+      Some pos
+  else 
+    let pos = 
+      match Z.getA pos with
+      | s,L (g,_) -> 
+           Z.inject T.Nil (Z.setA s (D g) pos)
+      | _ -> pos
+    in
+    match Z.left pos with 
+    | None -> None 
+    | Some pos -> 
+        first_left_mark_L_as_D pred pos
+;;
+
+let is_oS pos = 
  match Z.getO pos with
- | S _ -> false
- | D _ -> true
+ | S _ -> true
+ | D _ | L _ -> false
 ;;
 
-let rec next_choice_point (pos : 'a and_pos) : 'a or_pos option =
-  let rec giveup_right_giveup_up_backtrack_left (pos : 'a and_pos) =
-    match Z.upA pos with
-    | None -> None
-    | Some alts -> 
-        match rightmost_bro is_not_S alts with
-        | None -> 
-          let upalts = Z.upO alts in
-          let upalts = Z.inject T.Nil upalts in
-           backtrack_left_giveup_right_giveup_up upalts
-        | Some _ as x -> x
-  and backtrack_left_giveup_right_giveup_up (pos : 'a and_pos) =
-    let pos = Z.inject T.Nil pos in
-    let pos = match Z.getA pos with s,D g | s, S (g,_) -> Z.setA s (D g) pos in
-    match Z.left pos with
-    | None -> giveup_right_giveup_up_backtrack_left pos
-    | Some (pos as left_bro) ->
-        match Z.downA pos with
-        | Z.Unexplored -> assert false (* we explore left2right *)
-        | Z.Alternatives alts ->  
-            match rightmost_bro is_not_S alts with
-            | None -> backtrack_left_giveup_right_giveup_up left_bro
-            | Some _ as x -> x
-  in
-    backtrack_left_giveup_right_giveup_up pos
+
+let is_aS pos = 
+ match Z.getA pos with
+ | _,S _ -> true
+ | _,D _ | _,L _ -> false
+;;
+
+let is_not_oS x = not (is_oS x);;
+let is_not_aS x = not (is_aS x);;
+
+let is_oL pos = match Z.getO pos with L _ -> true | _ -> false ;;
+let is_aL pos = match Z.getA pos with _,L _ -> true | _ -> false ;;
+
+let is_not_oL x = not (is_oL x) ;;
+let is_not_aL x = not (is_aL x) ;;
+
+let rec forall_left pred pos = 
+  match Z.left pos with
+  | None -> true
+  | Some pos -> if pred pos then forall_left pred pos else false
+;;
+
+  
+let rec product = function
+  | [] -> []
+  | ((g,s) :: tl) as l -> (s,List.map fst l) :: product tl
+;;
+
+let has_no_alternatives (pos : 'a and_pos) = 
+  match Z.getA pos with
+  | _, L _ -> true
+  | _ -> false
+;;
+
+let rec collect_left_up (pos : 'a and_pos) =
+  match Z.left pos with
+  | Some pos -> 
+     (match Z.getA pos with
+     | _, L (g,s) -> (g,s) :: collect_left_up pos
+     | _ -> [])
+  | None -> 
+      match Z.upA pos with
+      | None -> [] (* root *)
+      | Some pos -> collect_left_up (Z.upO pos)
+;;
+
+let compute_failed_goals (pos : 'a and_pos) =
+  let curr = match Z.getA pos with (s,_,_),D g -> (g,s) | _ -> assert false in
+  product (List.rev (curr :: collect_left_up pos) )
+;;
+
+let pp_failures l =
+  debug_print (lazy("CACHE FAILURES/UNDERINSPECTION"));
+  List.iter (fun (s,gl) -> 
+    debug_print (lazy("FAIL: " ^
+    String.concat " , " (List.map (fun g ->
+    match calculate_goal_ty g s with
+    | None -> 
+        (try 
+          let (i,_) = g in 
+          let _,_,_,subst,_ = s#obj in
+          let _,cc,_,ty = NCicUtils.lookup_subst i subst in
+          let ty = mk_cic_term cc ty in
+          string_of_int i^":"^ppterm s ty
+        with NCicUtils.Subst_not_found _ -> "XXXX")
+    | Some gty ->
+       let s, gty = apply_subst s (ctx_of gty) gty in
+       string_of_int (fst g)^":"^ppterm s gty) gl)))) 
+    l
+;;
+
+let is_closed pos = 
+  match Z.getA pos with
+  | (s,_,_),S (g,_) 
+  | (s,_,_),D g ->
+      (match calculate_goal_ty g s with
+      | None -> true
+      | Some gty -> metas_of_term s gty = [])
+  | _, L _ -> assert false
 ;;
 
 let auto_main flags signature (pos : 'a and_pos) cache =
-  let solved g depth size s pos =
+  let solved g depth size s (pos : 'a and_pos) =
     Z.inject (T.Node(`Or,[D g,T.Node(`And(s,depth,size),[])])) pos
   in
-  let failed pos =
+  let failed (pos : 'a and_pos) =
+    pp_failures (compute_failed_goals pos);
     Z.inject (T.Node(`Or,[])) pos
   in
 
@@ -1284,32 +1381,111 @@ let auto_main flags signature (pos : 'a and_pos) cache =
 
   and nextO ~unfocus (pos : 'a or_pos) cache =
     match Z.getO pos with
-    | S _ -> assert false (* XXX set to Nil when backtrack *)
+    | S _ | L _ -> assert false (* XXX set to Nil when backtrack *)
     | D g -> 
         match Z.downO pos with
-        | Z.Solution (s,_,_) -> move_solution_up ~unfocus s pos cache 
+        | Z.Solution (s,_,_) -> move_solution_up ~unfocus true s pos cache 
         | Z.Todo pos -> next ~unfocus:true pos cache 
 
+  and next_choice_point (pos : 'a and_pos) cache  =
+
+    let rec global_choice_point (pos : 'a and_pos) : 'a auto_result =
+(*             prerr_endline "global"; show pos; *)
+      match Z.upA pos with
+      | None -> Gaveup
+      | Some alts -> 
+          let alts = Z.inject T.Nil alts in
+          let alts = 
+            match Z.getO alts with
+            | S (s,g) -> Z.setO (L (s,g)) alts 
+            | D (g) -> Z.setO (L (g,Obj.magic g)) alts 
+                       (* L (and other marks) for OR should have no arguments *)
+            | L _ -> assert false
+          in
+          match Z.right alts with
+          | None -> 
+             let upalts = Z.upO alts in
+             let upalts = Z.inject T.Nil upalts in
+             let upalts = 
+               match Z.getA upalts with
+               | s,S (a,b) -> Z.setA s (L (a,b)) upalts 
+               | _,L _ -> assert false
+               | s,D (a) -> Z.setA s (L (a,Obj.magic a)) upalts 
+             in
+             backtrack upalts
+          | Some pos -> 
+              match Z.downO pos with
+              | Z.Solution (s,_,_) -> 
+                    move_solution_up ~unfocus:false true s pos cache
+              | Z.Todo pos -> next ~unfocus:true pos cache 
+
+    and backtrack (pos : 'a and_pos) : 'a auto_result =
+(*             prerr_endline "backtrack"; show pos; *)
+      let pos = Z.inject T.Nil pos in
+      let pos = 
+        match Z.getA pos with 
+        | s,D g | s, S (g,_) | s,L(g,_) -> Z.setA s (D g) pos 
+      in
+      match first_left_mark_L_as_D is_aS pos with 
+      | None -> global_choice_point pos
+      | Some pos ->
+         let rec local_choice_point pos =
+(*             prerr_endline "local"; show pos; *)
+           match Z.downA pos with
+           | Z.Unexplored -> attack pos cache (Z.getA pos)
+           | Z.Alternatives alts ->  
+               match leftmost_bro is_not_oL alts with
+               | None -> assert false (* is not L, thus has alternatives *)
+               | Some pos ->
+                   let is_D = is_not_oS pos in
+                   match if is_D then Z.downO pos else Z.downOr pos with
+                   | Z.Solution (s,_,_) -> assert(is_D);
+                        move_solution_up ~unfocus:false true s pos cache
+                   | Z.Todo pos when is_D -> attack pos cache (Z.getA pos)
+                   | Z.Todo pos ->
+                        match first_left_mark_L_as_D is_aS pos with
+                        | Some pos -> local_choice_point pos
+                        | None -> assert false
+         in
+           local_choice_point pos
+    in
+      backtrack pos
+
   and next_choice (pos : 'a and_pos) cache = 
-    match next_choice_point pos with
-    | None -> Gaveup
-    | Some pos -> nextO ~unfocus:true pos cache 
+    next_choice_point pos cache
 
   and move_solution_up 
-      ~unfocus (status : #tac_status as 'a) (pos : 'a or_pos) cache 
+      ~unfocus are_sons_L
+      (status : #tac_status as 'a) (pos : 'a or_pos) cache 
   =
     let pos = (* mark as solved *)
       match Z.getO pos with
-      | S _ -> assert false (* XXX  *) 
-      | D g -> Z.setO (S (g,status)) pos 
+      | L _ -> assert false (* XXX  *) 
+      | S (g,_) 
+      | D g -> 
+          if are_sons_L then 
+             Z.inject T.Nil (Z.setO (L (g,status)) pos)
+          else 
+             Z.setO (S (g,status)) pos 
     in
+    let has_alternative_or = match Z.right pos with None -> false | _ -> true in
     let pos = Z.upO pos in
+    let are_all_lbro_L = forall_left is_aL pos in
+    let has_no_alternative = 
+      ((not has_alternative_or) && are_sons_L) ||
+      is_closed pos
+    in
     match Z.getA pos with
+    | _, L _ -> assert false
     | (_, size, depth), S (g,_) 
        (* S if already solved and then solved again because of a backtrack *)
     | (_, size, depth), D g -> 
-        let newg = S (g,status) in (* TODO: cache success g *)
-        let status = if unfocus then NTactics.unfocus_tac status else status in
+        let newg = 
+          if has_no_alternative then (L (g,status)) else (S (g,status))in
+        (* TODO: cache success g *)
+        let pos = if has_no_alternative then Z.inject T.Nil pos else pos in
+         let status = if unfocus then NTactics.unfocus_tac status else status
+         in
         let news = status,size,depth in
         let pos = Z.setA news newg pos in
         match Z.right pos with
@@ -1317,72 +1493,76 @@ let auto_main flags signature (pos : 'a and_pos) cache =
         | None -> 
             match Z.upA pos with
             | None -> Proved (status, Some (pos,cache))
-            | Some pos -> move_solution_up ~unfocus:true status pos cache 
+            | Some pos -> 
+               move_solution_up 
+                 ~unfocus:true (has_no_alternative && are_all_lbro_L)
+                 status pos cache 
 
   and attack pos cache and_item =
-     (* show pos; *) (* uncomment to show the tree *)
-     match and_item with
-       | _, S _ -> assert false (* next would close the proof or give a D *) 
-       | (_, depth, _),_ when Unix.gettimeofday () > flags.timeout ->
-           debug_print ~depth (lazy ("fail timeout"));
-           Gaveup 
-       | (s, depth, width), D (_, T as g) when not flags.do_types -> 
-           debug_print ~depth (lazy "skip goal in Type");
-           next ~unfocus:true (solved g depth width s pos) cache
-       | (_,depth,_), D _ when depth > flags.maxdepth -> 
-           debug_print ~depth (lazy "fail depth");
-           next_choice (failed pos) cache
-       | (_,depth,size), D _ when size > flags.maxsize -> 
-           debug_print ~depth (lazy "fail size");
-           next_choice (failed pos) cache
-       | (s,depth,size), D (gno,_ as g) -> 
-           assert (Z.eject pos = T.Nil); (*subtree must be unexplored *)
-           match calculate_goal_ty g s with
-           | None -> 
-              debug_print 
-                ~depth (lazy ("success side effect: " ^ string_of_int gno));
-              next ~unfocus:false (solved g depth size s pos) cache
-           | Some gty ->
-              let s, gty = apply_subst s (ctx_of gty) gty in
-              debug_print ~depth (lazy ("EXAMINE: "^ ppterm s gty));
-              match cache_examine cache gty with
-              | `Failed_in d when d <= depth -> 
-                 debug_print ~depth(lazy("fail depth (c): "^string_of_int gno));
-                  next_choice (failed pos) cache
-              | `UnderInspection -> 
-                  debug_print ~depth (lazy("fail loop: "^string_of_int gno));
-                  next_choice (failed pos) cache
-              | `Succeded t -> 
-                  debug_print ~depth (lazy("success (c): "^string_of_int gno));
-                  let s = put_in_subst s g t gty in
-                  next ~unfocus:true (solved g depth size s pos) cache
-              | `Notfound 
-              | `Failed_in _ -> 
-                  (* more depth than before or first time we see the goal *)
-                  if prunable s gty () then
-                    (debug_print ~depth (lazy( "fail one father is equal"));
-                    next_choice (failed pos) cache)
-                  else
-                  let cache = cache_add_underinspection cache gty depth in
-                  debug_print ~depth (lazy ("INSPECTING: " ^ 
-                    string_of_int gno ^ "("^ string_of_int size ^ ") "));
-                  let subgoals, cache = 
-                    do_something signature flags s gno depth gty cache
-                  in
-                  if subgoals = [] then (* this goal has failed *)
-                    next_choice (failed pos) cache
-                  else
-                    let size_gl l = List.length (prop_only l) in
-                    let subtrees = 
-                      List.map
-                        (fun (_cand,depth_incr,s,gl) ->
-                          D(gno,P), 
-                          T.Node (`And (s,depth+depth_incr,size+size_gl gl), 
-                                  List.map (fun g -> D g,T.Nil) gl))
-                        subgoals
-                    in
-                     next ~unfocus:true 
-                       (Z.inject (T.Node (`Or,subtrees)) pos) cache
+    (* 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 *)
+    | (_, depth, _),_ when Unix.gettimeofday () > flags.timeout ->
+        debug_print ~depth (lazy ("fail timeout"));
+        Gaveup 
+    | (s, depth, width), D (_, T as g) when not flags.do_types -> 
+        debug_print ~depth (lazy "skip goal in Type");
+        next ~unfocus:false (solved g depth width s pos) cache
+    | (_,depth,_), D _ when depth > flags.maxdepth -> 
+        debug_print ~depth (lazy "fail depth");
+        next_choice (failed pos) cache
+    | (_,depth,size), D _ when size > flags.maxsize -> 
+        debug_print ~depth (lazy "fail size");
+        next_choice (failed pos) cache
+    | (s,depth,size), D (gno,_ as g) -> 
+        assert (Z.eject pos = T.Nil); (*subtree must be unexplored *)
+        match calculate_goal_ty g s with
+        | None -> 
+           debug_print ~depth (lazy("success side effect: "^string_of_int gno));
+           next ~unfocus:false (solved g depth size s pos) cache
+        | Some gty ->
+           let s, gty = apply_subst s (ctx_of gty) gty in
+           debug_print ~depth (lazy ("EXAMINE: "^ ppterm s gty));
+           match cache_examine cache gty with
+           | `Failed_in d when d <= depth -> 
+               debug_print ~depth(lazy("fail depth (c): "^string_of_int gno));
+               next_choice (failed pos) cache
+           | `UnderInspection -> 
+               debug_print ~depth (lazy("fail loop: "^string_of_int gno));
+               next_choice (failed pos) cache
+           | `Succeded t -> 
+               debug_print ~depth (lazy("success (c): "^string_of_int gno));
+               let s = put_in_subst s g t gty in
+               next ~unfocus:true (solved g depth size s pos) cache
+           | `Notfound 
+           | `Failed_in _ -> 
+               (* more depth than before or first time we see the goal *)
+               if prunable s gty () then
+                 (debug_print ~depth (lazy( "fail one father is equal"));
+                  next_choice (failed pos) cache)
+               else
+               let cache = cache_add_underinspection cache gty depth in
+               debug_print ~depth (lazy ("INSPECTING: " ^ 
+                 string_of_int gno ^ "("^ string_of_int size ^ ") "));
+               let subgoals, cache = 
+                 do_something signature flags s gno depth gty cache
+               in
+               if subgoals = [] then (* this goal has failed *)
+                 next_choice (failed pos) cache
+               else
+                 let size_gl l = List.length (prop_only l) in
+                 let subtrees = 
+                   List.map
+                     (fun (_cand,depth_incr,size_mult,s,gl) ->
+                       D(gno,P), 
+                       T.Node (`And 
+                          (s,depth+depth_incr,size+size_mult*(size_gl gl)), 
+                               List.map (fun g -> D g,T.Nil) gl))
+                     subgoals
+                 in
+                  next ~unfocus:true 
+                    (Z.inject (T.Node (`Or,subtrees)) pos) cache
   in
     (next ~unfocus:true pos cache : 'a auto_result)
 ;;
@@ -1435,7 +1615,41 @@ let auto_tac ~params:(_univ,flags) status =
           in
           s#set_stack stack
   in
-    up_to 2 depth
+    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 = 
@@ -1461,7 +1675,7 @@ let group_by_tac ~eq_predicate ~action:tactic status =
     let l2 = HExtlib.list_mapi (fun x i -> x,i+1) l2 in
     List.map (fun x -> List.assoc x l2) l1
   in
-  NTactics.block_tac ([ NTactics.branch_tac ]
+  NTactics.block_tac ([ NTactics.branch_tac ~force:false]
     @
     HExtlib.list_concat ~sep:[NTactics.shift_tac]
       (List.map (fun gl-> [NTactics.pos_tac (pos_of gl goals); tactic]) classes)
@@ -1494,7 +1708,13 @@ 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 "paramod" flags then 
+    NnAuto.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
 ;;