From 9de2bb1a68109ae9e15b78ed4225e4846d2e2b0a Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 14 Jul 2006 15:41:26 +0000 Subject: [PATCH] Added the computation of max_weight for equations in proofs. --- helm/software/components/tactics/.depend | 6 ++- .../tactics/paramodulation/equality.ml | 26 ++++++++++++ .../tactics/paramodulation/equality.mli | 2 + .../tactics/paramodulation/inference.ml | 4 +- .../tactics/paramodulation/saturation.ml | 42 +++++++++++++++---- 5 files changed, 69 insertions(+), 11 deletions(-) diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend index 43ed94aa9..2ed8b5147 100644 --- a/helm/software/components/tactics/.depend +++ b/helm/software/components/tactics/.depend @@ -190,5 +190,7 @@ tactics.cmx: variousTactics.cmx tacticals.cmx paramodulation/saturation.cmx \ introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \ equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \ autoTactic.cmx tactics.cmi -declarative.cmo: tactics.cmi tacticals.cmi declarative.cmi -declarative.cmx: tactics.cmx tacticals.cmx declarative.cmi +declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \ + declarative.cmi +declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \ + declarative.cmi diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml index 4414d2f43..ac5cb1a0c 100644 --- a/helm/software/components/tactics/paramodulation/equality.ml +++ b/helm/software/components/tactics/paramodulation/equality.ml @@ -67,6 +67,7 @@ let mk_equality (weight,p,(ty,l,r,o),m) = let id = freshid () in let eq = (uncomparable,weight,p,(ty,l,r,o),m,id) in Hashtbl.add id_to_eq id eq; + eq ;; @@ -108,6 +109,31 @@ let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) = Pervasives.compare s1 s2 ;; +let rec max_weight_in_proof current = + function + | Exact _ -> current + | Step (_, (_,id1,(_,id2),_)) -> + let eq1 = Hashtbl.find id_to_eq id1 in + let eq2 = Hashtbl.find id_to_eq id2 in + let (w1,p1,(_,_,_,_),_,_) = open_equality eq1 in + let (w2,p2,(_,_,_,_),_,_) = open_equality eq2 in + let current = max current w1 in + let current = max_weight_in_proof current p1 in + let current = max current w2 in + max_weight_in_proof current p2 + +let max_weight_in_goal_proof = + List.fold_left + (fun current (_,_,id,_,_) -> + let eq = Hashtbl.find id_to_eq id in + let (w,p,(_,_,_,_),_,_) = open_equality eq in + let current = max current w in + max_weight_in_proof current p) + +let max_weight goal_proof proof = + let current = max_weight_in_proof 0 proof in + max_weight_in_goal_proof current goal_proof + let proof_of_id id = try let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in diff --git a/helm/software/components/tactics/paramodulation/equality.mli b/helm/software/components/tactics/paramodulation/equality.mli index 1a62ee2ff..019578ccc 100644 --- a/helm/software/components/tactics/paramodulation/equality.mli +++ b/helm/software/components/tactics/paramodulation/equality.mli @@ -58,6 +58,8 @@ val open_equality : Cic.metasenv * int val depend : equality -> int -> bool val compare : equality -> equality -> int +val max_weight_in_proof : int-> proof -> int +val max_weight : goal_proof -> proof -> int val string_of_equality : ?env:Utils.environment -> equality -> string val string_of_proof : ?names:(Cic.name option)list -> proof -> goal_proof -> string diff --git a/helm/software/components/tactics/paramodulation/inference.ml b/helm/software/components/tactics/paramodulation/inference.ml index 8f031a4a7..408a7cdb8 100644 --- a/helm/software/components/tactics/paramodulation/inference.ml +++ b/helm/software/components/tactics/paramodulation/inference.ml @@ -243,8 +243,8 @@ let find_equalities context proof = (Printf.sprintf "OK: %s" (CicPp.ppterm term))); let o = !Utils.compare_terms t1 t2 in let stat = (ty,t1,t2,o) in -(* let w = compute_equality_weight stat in *) - let w = 0 in + (* let w = compute_equality_weight stat in *) + let w = 0 in let proof = Equality.Exact p in let e = Equality.mk_equality (w, proof, stat, newmetas) in Some e, (newmeta+1) diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index d4ccf8f42..c40b4a9ac 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -153,11 +153,13 @@ let age_factor = 0.01;; of weight, age and goal-similarity *) -let rec select env (goals,_) passive = +let rec select env g passive = processed_clauses := !processed_clauses + 1; +(* let goal = match (List.rev goals) with goal::_ -> goal | _ -> assert false in +*) let pos_list, pos_set = passive in let remove eq l = List.filter (fun e -> Equality.compare e eq <> 0) l in if !weight_age_ratio > 0 then @@ -165,20 +167,38 @@ let rec select env (goals,_) passive = match !weight_age_counter with | 0 -> ( weight_age_counter := !weight_age_ratio; + let skip_giant pos_list pos_set = + match pos_list with + | (hd:EqualitySet.elt)::tl -> + let w,_,_,_,_ = Equality.open_equality hd in + 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)) + | _ -> assert false + in + skip_giant pos_list pos_set) + +(* let rec skip_giant pos_list pos_set = match pos_list with | (hd:EqualitySet.elt)::tl -> let w,_,_,_,_ = Equality.open_equality hd in let pos_set = EqualitySet.remove hd pos_set in - if w < 500 then + if w < 30 then hd, (tl, pos_set) else (prerr_endline ("+++ skipping giant of size "^string_of_int w^" +++"); skip_giant tl pos_set) | _ -> assert false - in - skip_giant pos_list pos_set) + in + skip_giant pos_list pos_set) + +*) +(* | _ when (!symbols_counter > 0) -> (symbols_counter := !symbols_counter - 1; let cardinality map = @@ -216,6 +236,7 @@ let rec select env (goals,_) passive = let _, current = EqualitySet.fold f pos_set initial in current, (remove current pos_list, EqualitySet.remove current pos_set)) +*) | _ -> symbols_counter := !symbols_ratio; let my_min e1 e2 = @@ -843,6 +864,10 @@ let simplify_goal_set env goals active = let find (_,_,g) where = List.exists (fun (_,_,g1) -> Equality.meta_convertibility g g1) where in + (* prova:tengo le passive semplificate + let passive_goals = + List.map (fun g -> snd (simplify_goal env g active)) passive_goals + in *) List.fold_left (fun (acc_a,acc_p) goal -> match simplify_goal env goal active with @@ -864,6 +889,7 @@ let check_if_goals_set_is_solved env active goals = check goal [ check_if_goal_is_identity env; check_if_goal_is_subsumed env (snd active)]) +(* provare active and passive?*) None active_goals ;; @@ -958,7 +984,6 @@ let given_clause int_of_float iterations_left in let rec step goals theorems passive active iterno = - pp_goals "xxx" goals context; if iterno > max_iterations then (ParamodulationFailure "No more iterations to spend") else if Unix.gettimeofday () > max_time then @@ -989,7 +1014,8 @@ let given_clause passive in kept_clauses := (size_of_passive passive) + (size_of_active active); - let goals = infer_goal_set env active goals in + let goals = infer_goal_set env active goals + in match check_if_goals_set_is_solved env active goals with | Some p -> prerr_endline @@ -1267,7 +1293,9 @@ let saturate 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) -- 2.39.2