From 1640e695e405f800547bb1e34cb043e9afa8d10e Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 1 Feb 2010 07:54:35 +0000 Subject: [PATCH] On the last goal at maxdepth we stop at the first solution. --- helm/software/components/ng_tactics/nnAuto.ml | 54 +++++++++++++------ 1 file changed, 37 insertions(+), 17 deletions(-) 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; -- 2.39.2