X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=90cc852474da915ce94c7645783a39a7d1d8a5a2;hb=59d4332991ab14755fa631d729edb5b5d3c6714c;hp=c40b4a9ac238de328366c0c49fa9ec6e067dc23b;hpb=9de2bb1a68109ae9e15b78ed4225e4846d2e2b0a;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index c40b4a9ac..90cc85247 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) -let _profiler = <:profiler<_profiler>>;; +(* let _profiler = <:profiler<_profiler>>;; *) (* $Id$ *) @@ -174,9 +174,11 @@ let rec select env g passive = if w < 30 then hd, (tl, EqualitySet.remove hd pos_set) else +(* (prerr_endline ("+++ skipping giant of size "^string_of_int w^" +++"); - select env g (tl@[hd],pos_set)) +*) + select env g (tl@[hd],pos_set) | _ -> assert false in skip_giant pos_list pos_set) @@ -265,8 +267,10 @@ let filter_dependent passive id = (eq::list, set), no) pos_list (([],pos_set),0) in +(* if no_pruned > 0 then prerr_endline ("+++ pruning "^ string_of_int no_pruned ^" passives +++"); +*) passive ;; @@ -355,11 +359,11 @@ let infer eq_uri env current (active_list, active_table) = let maxm, copy_of_current = Equality.fix_metas !maxmeta current in maxmeta := maxm; let active_table = Indexing.index active_table copy_of_current in - let _ = <:start> in +(* let _ = <:start> in *) let maxm, res = Indexing.superposition_right eq_uri !maxmeta env active_table current in - let _ = <:stop> in +(* let _ = <:stop> in *) if Utils.debug_metas then ignore(List.map (function current -> @@ -386,9 +390,9 @@ let infer eq_uri env current (active_list, active_table) = maxmeta := maxm; *) let curr_table = Indexing.index Indexing.empty current in - let _ = <:start> in +(* let _ = <:start> in *) let pos = infer_positive curr_table ((*copy_of_current::*)active_list) in - let _ = <:stop> in +(* let _ = <:stop> in *) if Utils.debug_metas then ignore(List.map (function current -> @@ -814,11 +818,13 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) = (* match Indexing.subsumption env table goal_equation with*) match Indexing.unification env table goal_equation with | Some (subst, equality, swapped ) -> +(* prerr_endline - ("GOAL SUBSUMED IS: " ^ Equality.string_of_equality goal_equation ~env); + ("GOAL SUBSUMED IS: "^Equality.string_of_equality goal_equation ~env); prerr_endline - ("GOAL IS SUBSUMED BY: " ^ Equality.string_of_equality equality ~env); - prerr_endline ("SUBST:" ^ Subst.ppsubst ~names subst); + ("GOAL IS SUBSUMED BY: "^Equality.string_of_equality equality ~env); + prerr_endline ("SUBST:"^Subst.ppsubst ~names subst); +*) let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in let p = @@ -899,8 +905,10 @@ let infer_goal_set env active 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 let already_in = List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1) @@ -967,6 +975,13 @@ let pp_goals label goals context = (snd goals); ;; +let print_status iterno goals active passive = + prerr_endline + (Printf.sprintf "\n%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)" + iterno (size_of_active active) (size_of_passive passive) + (size_of_goal_set_a goals) (size_of_goal_set_p goals)) +;; + (** given-clause algorithm with full reduction strategy: NEW implementation *) (* here goals is a set of goals in OR *) let given_clause @@ -989,17 +1004,9 @@ 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)) +(* print_status iterno goals active passive *) + Printf.printf ".%!"; in (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *) let passive = @@ -1019,7 +1026,7 @@ let given_clause match check_if_goals_set_is_solved env active goals with | Some p -> prerr_endline - (Printf.sprintf "Found a proof in: %f\n" + (Printf.sprintf "\nFound a proof in: %f\n" (Unix.gettimeofday() -. initial_time)); ParamodulationSuccess p | None -> @@ -1035,6 +1042,7 @@ let given_clause (* COLLECTION OF GARBAGED EQUALITIES *) if iterno mod 40 = 0 then begin + print_status iterno goals active passive; let active = List.map Equality.id_of (fst active) in let passive = List.map Equality.id_of (fst passive) in let goal = ids_of_goal_set goals in @@ -1042,24 +1050,21 @@ let given_clause end; let current, passive = select env goals passive in (* SIMPLIFICATION OF CURRENT *) +(* prerr_endline ("Selected : " ^ Equality.string_of_equality ~env current); +*) let res = forward_simplify eq_uri env current active in match res with | None -> step goals theorems passive active (iterno+1) | Some current -> -(* - prerr_endline - ("Selected simpl: " ^ - Equality.string_of_equality ~env current); -*) (* GENERATION OF NEW EQUATIONS *) - prerr_endline "infer"; +(* prerr_endline "infer"; *) let new' = infer eq_uri env current active in - prerr_endline "infer goal"; +(* prerr_endline "infer goal"; *) (* match check_if_goals_set_is_solved env active goals with | Some p -> @@ -1077,7 +1082,7 @@ let given_clause infer_goal_set_with_current env current goals active in (* FORWARD AND BACKWARD SIMPLIFICATION *) - prerr_endline "fwd/back simpl"; +(* prerr_endline "fwd/back simpl"; *) let rec simplify new' active passive head = let new' = forward_simplify_new eq_uri env new' active @@ -1098,12 +1103,12 @@ let given_clause let active, passive, new', head = simplify new' active passive [] in - prerr_endline "simpl goal with new"; +(* prerr_endline "simpl goal with new"; *) let goals = let a,b,_ = build_table new' in - let _ = <:start> in +(* let _ = <:start> in *) let rc = simplify_goal_set env goals (a,b) in - let _ = <:stop> in +(* let _ = <:stop> in *) rc in let passive = add_to_passive passive new' head in @@ -1206,7 +1211,8 @@ let eq_and_ty_of_goal = function let saturate caso_strano - dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = + dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) + ?(timeout=600.) status = let module C = Cic in reset_refs (); Indexing.init_index (); @@ -1277,7 +1283,7 @@ let saturate *) let goals = make_goal_set goal in let max_iterations = 10000 in - let max_time = Unix.gettimeofday () +. 600. (* minutes *) in + let max_time = Unix.gettimeofday () +. timeout (* minutes *) in given_clause eq_uri env goals theorems passive active max_iterations max_time in @@ -1289,13 +1295,15 @@ let saturate raise (ProofEngineTypes.Fail (lazy ("NO proof found: " ^ s))) | ParamodulationSuccess (goalproof,newproof,subsumption_id,subsumption_subst, proof_menv) -> - prerr_endline "OK, found a proof!"; + prerr_endline "Proof:"; prerr_endline (Equality.pp_proof names goalproof newproof subsumption_subst subsumption_id type_of_goal); - prerr_endline "ENDOFPROOFS___"; +(* prerr_endline "ENDOFPROOFS"; *) +(* prerr_endline ("max weight: " ^ (string_of_int (Equality.max_weight goalproof newproof))); +*) (* generation of the CIC proof *) let side_effects = List.filter (fun i -> i <> goalno) @@ -1308,7 +1316,7 @@ let saturate eq_uri goalproof initial type_of_goal side_effects context proof_menv in - prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); +(* prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *) let goal_proof = Subst.apply_subst subsumption_subst goal_proof in let metas_still_open_in_proof = Utils.metas_of_term goal_proof in (*prerr_endline (CicPp.pp goal_proof names);*) @@ -1318,7 +1326,7 @@ let saturate List.map (Subst.apply_subst subsumption_subst) side_effects_t in (* replacing fake mets with real ones *) - prerr_endline "replacing metas..."; +(* prerr_endline "replacing metas..."; *) let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in let goal_proof_menv, what, with_what,free_meta = List.fold_left @@ -1351,7 +1359,8 @@ let saturate (ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv:goal_proof_menv) in -prerr_endline ("freemetas: " ^ String.concat "," (List.map string_of_int free_metas) ); +(* prerr_endline ("freemetas: " ^ String.concat "," (List.map string_of_int + * free_metas) ); *) (* check/refine/... build the new proof *) let replaced_goal = ProofEngineReduction.replace @@ -1376,7 +1385,7 @@ prerr_endline ("freemetas: " ^ String.concat "," (List.map string_of_int free_me let final_subst = (goalno,(context,goal_proof,type_of_goal))::subst_side_effects in -prerr_endline ("MENVreal_menv: " ^ CicMetaSubst.ppmetasenv [] real_menv); +(* prerr_endline ("MENVreal_menv: " ^ CicMetaSubst.ppmetasenv [] real_menv); *) let _ = try CicTypeChecker.type_of_aux' real_menv context goal_proof @@ -1398,11 +1407,13 @@ prerr_endline ("MENVreal_menv: " ^ CicMetaSubst.ppmetasenv [] real_menv); let open_goals = match free_meta with Some(Cic.Meta(m,_)) when m<>goalno ->[m] | _ ->[] in +(* Printf.eprintf "GOALS APERTI: %s\nMETASENV PRIMA:\n%s\nMETASENV DOPO:\n%s\n" (String.concat ", " (List.map string_of_int open_goals)) (CicMetaSubst.ppmetasenv [] metasenv) (CicMetaSubst.ppmetasenv [] real_metasenv); +*) prerr_endline (Printf.sprintf "\nTIME NEEDED: %8.2f" time); proof, open_goals ;; @@ -1533,8 +1544,8 @@ let main_demod_equalities dbd term metasenv ugraph = (String.concat "\n" (List.map (Equality.string_of_equality ~env) equalities)); - print_endline "--------------------------------------------------"; - print_endline "GO!"; + prerr_endline "--------------------------------------------------"; + prerr_endline "GO!"; start_time := Unix.gettimeofday (); if !time_limit < 1. then time_limit := 60.; let ra, rp = @@ -1736,8 +1747,10 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status = proof,[goalno] ;; -let get_stats () = +let get_stats () = "" +(* <:show> ^ Indexing.get_stats () ^ Inference.get_stats () ^ Equality.get_stats () ;; +*)