From: Enrico Tassi Date: Tue, 27 Jun 2006 16:55:52 +0000 (+0000) Subject: fixed infer_goal, added simplification before inferring with current X-Git-Tag: make_still_working~7139 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=44f4e888646ac95752bbd8c3e7b9b4b48209b1a6;p=helm.git fixed infer_goal, added simplification before inferring with current --- diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index bb1b3a853..81c2a15f1 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -901,6 +901,17 @@ let print_goals goals = Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals)) ;; +let pp_goal_set msg goals names = + let active_goals, passive_goals = goals in + prerr_endline ("////" ^ msg); + prerr_endline ("ACTIVE G: " ^ + (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names) + active_goals))); + prerr_endline ("PASSIVE G: " ^ + (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names) + passive_goals))) +;; + let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) = (* let names = names_of_context ctx in @@ -959,7 +970,7 @@ let rec check goal = function | (Some p) as ok -> ok ;; -let simplify_goal_set env goals passive active = +let simplify_goal_set env goals ?passive active = let active_goals, passive_goals = goals in let find (_,_,g) where = List.exists (fun (_,_,g1) -> Equality.meta_convertibility g g1) where @@ -967,7 +978,7 @@ let simplify_goal_set env goals passive active = let simplified = List.fold_left (fun acc goal -> - match simplify_goal env goal ~passive active with + match simplify_goal env goal ?passive active with | changed, g -> if changed then prerr_endline "???????????????cambiato ancora"; if find g acc then acc else g::acc) @@ -1000,26 +1011,28 @@ let check_if_goals_set_is_solved env active goals = let infer_goal_set env active goals = let active_goals, passive_goals = goals in let rec aux = function - | [] -> goals + | [] -> active_goals, [] | hd::tl -> let changed,selected = simplify_goal env hd active in if changed then prerr_endline ("--------------- goal semplificato"); let (_,_,t1) = selected in - if (List.exists - (fun (_,_,t) -> - Equality.meta_convertibility t t1) - active_goals) then aux tl - else - let passive_goals = tl in - let new_passive_goals = - if Utils.metas_of_term t1 = [] then passive_goals - else - let new' = - Indexing.superposition_left env (snd active) selected in - passive_goals @ new' + let already_in = + List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1) + active_goals in - selected::active_goals, new_passive_goals + if already_in then + aux tl + else + let passive_goals = tl in + let new_passive_goals = + if Utils.metas_of_term t1 = [] then passive_goals + else + let new' = + Indexing.superposition_left env (snd active) selected in + passive_goals @ new' + in + selected::active_goals, new_passive_goals in aux passive_goals ;; @@ -1053,8 +1066,11 @@ let infer_goal_set env active goals = let infer_goal_set_with_current env current goals = let active_goals, passive_goals = goals in - let _,table,_ = build_table [current] in - active_goals, + let l,table,_ = build_table [current] in + let active_goals, _ = + simplify_goal_set env goals (l,table) + in + active_goals, List.fold_left (fun acc g -> let new' = Indexing.superposition_left env table g in @@ -1152,6 +1168,11 @@ let given_clause prerr_endline (Printf.sprintf "Current goal = %s\n" (CicPp.pp g names))) (fst goals); + List.iter + (fun _,_,g -> + prerr_endline (Printf.sprintf "Passive goal = %s\n" + (CicPp.pp g names))) + (snd goals); prerr_endline (Printf.sprintf "Selected = %s\n" (Equality.string_of_equality ~env current)) in @@ -1194,7 +1215,7 @@ let given_clause let goals = let a,b,_ = build_table new' in let _ = <:start> in - let rc = simplify_goal_set env goals passive (a,b) in + let rc = simplify_goal_set env goals ~passive (a,b) in let _ = <:stop> in rc in @@ -1225,6 +1246,8 @@ let rec saturate_equations eq_uri env goal accept_fun passive active = let al, tbl = active in al @ [current], Indexing.index tbl current in + (* alla fine new' contiene anche le attive semplificate! + * quindi le aggiungo alle passive insieme alle new *) let rec simplify new' active passive = let new' = forward_simplify_new eq_uri env new' ~passive active in let active, passive, newa, retained, pruned = @@ -1461,6 +1484,7 @@ let eq_and_ty_of_goal = function ;; let saturate + caso_strano dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = let module C = Cic in reset_refs (); @@ -1481,7 +1505,7 @@ let saturate let res, time = let t1 = Unix.gettimeofday () in let lib_eq_uris, library_equalities, maxm = - find_library_equalities dbd context (proof, goalno) (maxm+2) + find_library_equalities caso_strano dbd context (proof, goalno) (maxm+2) in let library_equalities = List.map snd library_equalities in let t2 = Unix.gettimeofday () in @@ -1675,7 +1699,7 @@ let retrieve_and_print dbd term metasenv ugraph = let env = (metasenv, context, ugraph) in let t1 = Unix.gettimeofday () in let lib_eq_uris, library_equalities, maxm = - find_library_equalities dbd context (proof, goal') (maxm+2) in + find_library_equalities false dbd context (proof, goal') (maxm+2) in let t2 = Unix.gettimeofday () in maxmeta := maxm+2; let equalities = (* equalities @ *) library_equalities in @@ -1753,7 +1777,7 @@ let main_demod_equalities dbd term metasenv ugraph = let eq_uri = eq_of_goal goal in let eq_indexes, equalities, maxm = find_equalities context proof in let lib_eq_uris, library_equalities, maxm = - find_library_equalities dbd context (proof, goal') (maxm+2) + find_library_equalities false dbd context (proof, goal') (maxm+2) in let library_equalities = List.map snd library_equalities in maxmeta := maxm+2; (* TODO ugly!! *) @@ -1832,7 +1856,7 @@ let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) = Inference.find_equalities context proof in let lib_eq_uris, library_equalities, maxm = - Inference.find_library_equalities dbd context (proof, goal) (maxm+2) in + Inference.find_library_equalities false dbd context (proof, goal) (maxm+2) in if library_equalities = [] then prerr_endline "VUOTA!!!"; let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let library_equalities = List.map snd library_equalities in diff --git a/helm/software/components/tactics/paramodulation/saturation.mli b/helm/software/components/tactics/paramodulation/saturation.mli index 9f1ad293d..8a03cd547 100644 --- a/helm/software/components/tactics/paramodulation/saturation.mli +++ b/helm/software/components/tactics/paramodulation/saturation.mli @@ -27,6 +27,7 @@ val saturate : + bool -> HMysql.dbd -> ?full:bool -> ?depth:int ->