X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=bb1b3a853515d22c49fecc0e9b43e944e0b55d17;hb=a507a21ca97552dec5077667cf8433f24d7a45ae;hp=67a328275b2d68b543ef16d2c079a566a5f8043b;hpb=a41f941ef133b7b8dcdf306d63f43f7bfb8d5275;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index 67a328275..bb1b3a853 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -1062,7 +1062,16 @@ let infer_goal_set_with_current env current goals = passive_goals active_goals ;; +let ids_of_goal g = + let p,_,_ = g in + let ids = List.map (fun _,_,i,_,_ -> i) p in + ids +;; +let ids_of_goal_set (ga,gp) = + List.flatten (List.map ids_of_goal ga) @ + List.flatten (List.map ids_of_goal gp) +;; let size_of_goal_set_a (l,_) = List.length l;; let size_of_goal_set_p (_,l) = List.length l;; @@ -1090,53 +1099,62 @@ let given_clause else if Unix.gettimeofday () > max_time then (ParamodulationFailure "No more time to spend") else - (* +(* let _ = prerr_endline "simpl goal with active" in let _ = <:start> in let goals = simplify_goal_set env goals passive active in let _ = <:stop> in - *) +*) + let _ = + prerr_endline + (Printf.sprintf "%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)\n" + iterno (size_of_active active) (size_of_passive passive) + (size_of_goal_set_a goals) (size_of_goal_set_p goals)) + in + (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *) + let passive = + let selection_estimate = iterations_left iterno in + let kept = size_of_passive passive in + if kept > selection_estimate then + begin + (*Printf.eprintf "Too many passive equalities: pruning..."; + prune_passive selection_estimate active*) passive + end + else + passive + in + kept_clauses := (size_of_passive passive) + (size_of_active active); + let goals = infer_goal_set env active goals in match check_if_goals_set_is_solved env active goals with | Some p -> prerr_endline (Printf.sprintf "Found a proof in: %f\n" (Unix.gettimeofday() -. initial_time)); -(* assert false;*) ParamodulationSuccess p | None -> - prerr_endline - (Printf.sprintf "%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)\n" - iterno (size_of_active active) (size_of_passive passive) - (size_of_goal_set_a goals) (size_of_goal_set_p goals)); - (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *) - (* - let passive = - let selection_estimate = iterations_left iterno in - let kept = size_of_passive passive in - if kept > selection_estimate then - begin - (*Printf.eprintf "Too many passive equalities: pruning..."; - prune_passive selection_estimate active*) passive - end - else - passive - in - kept_clauses := (size_of_passive passive) + (size_of_active active); - *) (* SELECTION *) if passive_is_empty passive then ParamodulationFailure "No more passive"(*maybe this is a success! *) else begin - let goals = infer_goal_set env active goals in + (* COLLECTION OF GARBAGED EQUALITIES *) + if iterno mod 40 = 0 then + begin + let active = List.map Equality.id_of (fst active) in + let passive = List.map Equality.id_of (fst (fst passive)) in + let goal = ids_of_goal_set goals in + Equality.collect active passive goal + end; let current, passive = select env goals passive in - let _,_,goaltype = List.hd (fst goals) in - List.iter + let _ = + List.iter (fun _,_,g -> - prerr_endline (Printf.sprintf "Current goal = %s\n" - (CicPp.pp g names))) (fst goals); - prerr_endline (Printf.sprintf "Selected = %s\n" - (Equality.string_of_equality ~env current)); + prerr_endline (Printf.sprintf "Current goal = %s\n" + (CicPp.pp g names))) + (fst goals); + prerr_endline (Printf.sprintf "Selected = %s\n" + (Equality.string_of_equality ~env current)) + in (* SIMPLIFICATION OF CURRENT *) let res = forward_simplify eq_uri env (Positive, current) active @@ -1146,7 +1164,6 @@ let given_clause | Some current -> (* GENERATION OF NEW EQUATIONS *) prerr_endline "infer"; - let _,_,_,_,id = Equality.open_equality current in let new' = infer eq_uri env current active in prerr_endline "infer goal"; let goals = infer_goal_set_with_current env current goals in @@ -1437,6 +1454,12 @@ let eq_of_goal = function | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality "))) ;; +let eq_and_ty_of_goal = function + | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri -> + uri,t + | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality "))) +;; + let saturate dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = let module C = Cic in @@ -1802,7 +1825,6 @@ let main_demod_equalities dbd term metasenv ugraph = ;; let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) = - let module I = Inference in let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let eq_uri = eq_of_goal ty in @@ -1810,7 +1832,7 @@ let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) = Inference.find_equalities context proof in let lib_eq_uris, library_equalities, maxm = - I.find_library_equalities dbd context (proof, goal) (maxm+2) in + Inference.find_library_equalities 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 @@ -1854,6 +1876,110 @@ let demodulate_tac ~dbd ~pattern = ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern) ;; +let rec find_in_ctx i name = function + | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name))) + | Some (Cic.Name name', _)::tl when name = name' -> i + | _::tl -> find_in_ctx (i+1) name tl +;; + +let rec position_of i x = function + | [] -> assert false + | j::tl when j <> x -> position_of (i+1) x tl + | _ -> i +;; + +(* Syntax: + * auto superposition target = NAME + * [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only] + * + * - if table is omitted no superposition will be performed + * - if demod_table is omitted no demodulation will be prformed + * - subterms_only is passed to Indexing.superposition_right + * + * lists are coded using _ (example: H_H1_H2) + *) +let superposition_tac ~target ~table ~subterms_only ~demod_table status = + reset_refs(); + Indexing.init_index (); + let proof,goalno = status in + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = CicUtil.lookup_meta goalno metasenv in + let eq_uri,tty = eq_and_ty_of_goal ty in + let env = (metasenv, context, CicUniv.empty_ugraph) in + let names = names_of_context context in + let eq_index, equalities, maxm = find_equalities context proof in + let eq_what = + let what = find_in_ctx 1 target context in + List.nth equalities (position_of 0 what eq_index) + in + let eq_other = + if table <> "" then + let other = + let others = Str.split (Str.regexp "_") table in + List.map (fun other -> find_in_ctx 1 other context) others + in + List.map + (fun other -> List.nth equalities (position_of 0 other eq_index)) + other + else + [] + in + let index = List.fold_left Indexing.index Indexing.empty eq_other in + let maxm, eql = + if table = "" then maxm,[eq_what] else + Indexing.superposition_right + ~subterms_only eq_uri maxm env index eq_what + in + prerr_endline ("Superposition right:"); + prerr_endline ("\n eq: " ^ Equality.string_of_equality eq_what ~env); + prerr_endline ("\n table: "); + List.iter (fun e -> prerr_endline (" " ^ Equality.string_of_equality e ~env)) eq_other; + prerr_endline ("\n result: "); + List.iter (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql; + prerr_endline ("\n result (cut&paste): "); + List.iter + (fun e -> + let t = Equality.term_of_equality eq_uri e in + prerr_endline (CicPp.pp t names)) + eql; + if demod_table <> "" then + begin + let demod = + let demod = Str.split (Str.regexp "_") demod_table in + List.map (fun other -> find_in_ctx 1 other context) demod + in + let eq_demod = + List.map + (fun demod -> List.nth equalities (position_of 0 demod eq_index)) + demod + in + let table = List.fold_left Indexing.index Indexing.empty eq_demod in + let maxm,eql = + List.fold_left + (fun (maxm,acc) e -> + let maxm,eq = + Indexing.demodulation_equality + eq_uri maxm env table Utils.Positive e + in + maxm,eq::acc) + (maxm,[]) eql + in + let eql = List.rev eql in + prerr_endline ("\n result [demod]: "); + List.iter + (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql; + prerr_endline ("\n result [demod] (cut&paste): "); + List.iter + (fun e -> + let t = Equality.term_of_equality eq_uri e in + prerr_endline (CicPp.pp t names)) + eql; + end; + proof,[goalno] +;; + let get_stats () = - <:show> ^ Indexing.get_stats () ^ Inference.get_stats ();; + <:show> ^ Indexing.get_stats () ^ Inference.get_stats () ^ + Equality.get_stats () +;;