From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 1 Feb 2010 07:54:35 +0000 (+0000)
Subject: On the last goal at maxdepth we stop at the first solution.
X-Git-Tag: make_still_working~3081
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1640e695e405f800547bb1e34cb043e9afa8d10e;p=helm.git

On the last goal at maxdepth we stop at the first solution.
---

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index fdf2d2ea3..c9f641cb3 100644
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -1371,6 +1371,7 @@ let search_in_th gty th =
 
 type flags = {
         do_types : bool; (* solve goals in Type *)
+        last : bool; (* last goal: take first solution only  *)
         maxwidth : int;
         maxsize  : int;
         maxdepth : int;
@@ -1427,7 +1428,7 @@ let try_candidate ?(smart=0) flags depth status eq_cache t =
 	smart_apply_auto ("",0,t) eq_cache status in 
   let og_no = openg_no status in 
     if (* og_no > flags.maxwidth || *)
-      (depth = flags.maxdepth && og_no <> 0) then
+      ((depth + 1) = flags.maxdepth && og_no <> 0) then
 	(print ~depth (lazy "pruned immediately"); None)
    else
      (incr candidate_no;
@@ -1496,24 +1497,32 @@ let applicative_case depth signature status flags gty (cache:cache) =
 (*
   let sm = 0 in 
   let smart_candidates = [] in *)
-  let sm = if is_eq then 0 else 2 in 
-  let elems = 
+  let sm = if is_eq then 0 else 2 in
+  let only_one = flags.last && (depth + 1 = flags.maxdepth) in 
+  print (lazy ("only_one: " ^ (string_of_bool only_one)));
+  let elems =  
     List.fold_left 
       (fun elems cand ->
-        match try_candidate (~smart:sm) 
-	  flags depth status cache.unit_eq cand with
-        | None -> elems
-        | Some x -> x::elems)
+	 if (only_one && (elems <> [])) then elems 
+	 else
+	   match try_candidate (~smart:sm) 
+	     flags depth status cache.unit_eq cand with
+               | None -> elems
+               | Some x -> x::elems)
       [] candidates
   in
   let more_elems = 
-    List.fold_left 
-      (fun elems cand ->
-        match try_candidate (~smart:1) 
-	  flags depth status cache.unit_eq cand with
-        | None -> elems
-        | Some x -> x::elems)
-      [] smart_candidates
+    if only_one && elems <> [] then elems 
+    else
+      List.fold_left 
+	(fun elems cand ->
+	 if (only_one && (elems <> [])) then elems 
+	 else
+           match try_candidate (~smart:1) 
+	     flags depth status cache.unit_eq cand with
+               | None -> elems
+               | Some x -> x::elems)
+	[] smart_candidates
   in
   elems@more_elems
 ;;
@@ -1729,6 +1738,7 @@ let focus_tac focus status =
 let rec auto_clusters ?(top=false)  
     flags signature cache depth status : unit =
   debug_print ~depth (lazy "entering auto clusters");
+  print (lazy ("auto cluster: " ^ (string_of_bool flags.last)));
   (* ignore(Unix.select [] [] [] 0.01); *)
   let status = clean_up_tac status in
   let goals = head_goals status#stack in
@@ -1737,7 +1747,7 @@ let rec auto_clusters ?(top=false)
   else if List.length goals < 2 then 
     auto_main flags signature cache depth status 
   else
-    debug_print ~depth (lazy ("goals = " ^ 
+    print ~depth (lazy ("goals = " ^ 
       String.concat "," (List.map string_of_int goals)));
     let classes = HExtlib.clusters (deps status) goals in
     let classes = if top then List.rev classes else classes in
@@ -1769,6 +1779,7 @@ and
    of the initial head goals in the stack *)
 
 auto_main flags signature (cache:cache) depth status: unit =
+  print (lazy ("auto enter: " ^ (string_of_bool flags.last)));
   debug_print ~depth (lazy "entering auto main");
   (* ignore(Unix.select [] [] [] 0.01); *)
   let status = sort_tac (clean_up_tac status) in
@@ -1795,8 +1806,10 @@ auto_main flags signature (cache:cache) depth status: unit =
 	  (debug_print (lazy "SUBSUMED");
 	   raise (Gaveup IntSet.add g IntSet.empty))
 	else 
+        let do_flags = 
+	  {flags with last = flags.last && (not branch)} in 
 	let alternatives, cache = 
-          do_something signature flags status g depth gty cache in
+          do_something signature do_flags status g depth gty cache in
 	let loop_cache =
 	  let under_inspection = 
 	    add_to_th closegty cache.under_inspection closegty in
@@ -1812,7 +1825,11 @@ auto_main flags signature (cache:cache) depth status: unit =
                debug_print (~depth:depth') 
 		 (lazy ("Case: " ^ CicNotationPp.pp_term t));
 	       let flags' = 
-		 {flags with maxwidth = flags.maxwidth - ng +1} in 
+		 {flags with maxwidth = flags.maxwidth - ng +1} in
+		 (* sistemare *)
+	       let flags' = 
+		 {flags' with last = flags'.last && (not branch)} in 
+               print (lazy ("auto last: " ^ (string_of_bool flags'.last)));
 	       try auto_clusters flags' signature loop_cache
 		 depth' status; unsat
                with 
@@ -1822,6 +1839,8 @@ auto_main flags signature (cache:cache) depth status: unit =
 		       let status = NTactics.merge_tac status
 		       in
 			 (* old cache, here *)
+		       let flags = 
+			 {flags with maxwidth = flags.maxwidth - 1} in 
 			 try auto_clusters flags signature cache 
 			   depth status; assert false
 			 with Gaveup f ->
@@ -1873,6 +1892,7 @@ let auto_tac ~params:(_univ,flags) status =
   let goals = List.map (fun i -> (i,P)) goals in
   let signature = () in
   let flags = { 
+          last = true;
           maxwidth = width;
           maxsize = size;
           maxdepth = depth;