From a7a7011cb7cf84e46d63651fa3a016f97533463b Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 21 Mar 2006 15:11:34 +0000 Subject: [PATCH] Changed the type of compute-equality_weight that now takes also in input the ordering --- components/tactics/paramodulation/indexing.ml | 20 +++++++++------ .../tactics/paramodulation/inference.ml | 25 +++++++++++-------- .../tactics/paramodulation/saturation.ml | 10 ++++---- components/tactics/paramodulation/utils.ml | 7 +++--- components/tactics/paramodulation/utils.mli | 2 +- 5 files changed, 37 insertions(+), 27 deletions(-) diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml index 83dc1b180..bbc605620 100644 --- a/components/tactics/paramodulation/indexing.ml +++ b/components/tactics/paramodulation/indexing.ml @@ -589,9 +589,10 @@ let rec demodulation_equality ?from newmeta env table sign target = (* first, we simplify *) let right = U.guarded_simpl context right in let left = U.guarded_simpl context left in - let w = Utils.compute_equality_weight eq_ty left right in let order = !Utils.compare_terms left right in - let target = w, proof, (eq_ty, left, right, order), metas, args in + let stat = (eq_ty, left, right, order) in + let w = Utils.compute_equality_weight stat in + let target = w, proof, stat, metas, args in if Utils.debug_metas then ignore(check_target context target "demod equalities input"); let metasenv' = (* metasenv @ *) metas in @@ -691,11 +692,12 @@ let rec demodulation_equality ?from newmeta env table sign target = in let left, right = if is_left then newterm, right else left, newterm in let ordering = !Utils.compare_terms left right in + let stat = (eq_ty, left, right, ordering) in let time2 = Unix.gettimeofday () in build_newtarget_time := !build_newtarget_time +. (time2 -. time1); let res = - let w = Utils.compute_equality_weight eq_ty left right in - (w, newproof, (eq_ty, left, right, ordering),newmenv,args) in + let w = Utils.compute_equality_weight stat in + (w, newproof, stat,newmenv,args) in if Utils.debug_metas then ignore(check_target context res "buildnew_target output"); !maxmeta, res @@ -945,12 +947,13 @@ let superposition_left newmeta (metasenv, context, ugraph) table target = let left, right = if ordering = U.Gt then newgoal, right else left, newgoal in let neworder = !Utils.compare_terms left right in + let stat = (eq_ty, left, right, neworder) in let newmenv = (* Inference.filter s *) menv in let time2 = Unix.gettimeofday () in build_newtarget_time := !build_newtarget_time +. (time2 -. time1); - let w = Utils.compute_equality_weight eq_ty left right in - (w, newproof, (eq_ty, left, right, neworder), newmenv, []) + let w = Utils.compute_equality_weight stat in + (w, newproof, stat, newmenv, []) in !maxmeta, List.map build_new expansions @@ -1028,9 +1031,10 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = let neworder = !Utils.compare_terms left right in let newmenv = (* Inference.filter s *) m in let newargs = args @ args' in + let stat = (eq_ty, left, right, neworder) in let eq' = - let w = Utils.compute_equality_weight eq_ty left right in - (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs) in + let w = Utils.compute_equality_weight stat in + (w, newproof, stat, newmenv, newargs) in if Utils.debug_metas then ignore (check_target context eq' "buildnew3"); let newm, eq' = Inference.fix_metas !maxmeta eq' in diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml index fdaf68018..07d95ef86 100644 --- a/components/tactics/paramodulation/inference.ml +++ b/components/tactics/paramodulation/inference.ml @@ -698,9 +698,10 @@ let find_equalities context proof = (lazy (Printf.sprintf "OK: %s" (CicPp.ppterm term))); let o = !Utils.compare_terms t1 t2 in - let w = compute_equality_weight ty t1 t2 in + let stat = (ty,t1,t2,o) in + let w = compute_equality_weight stat in let proof = BasicProof p in - let e = (w, proof, (ty, t1, t2, o), newmetas, args) in + let e = (w, proof, stat, newmetas, args) in Some e, (newmeta+1) | _ -> None, newmeta ) @@ -710,8 +711,9 @@ let find_equalities context proof = let t1 = S.lift index t1 in let t2 = S.lift index t2 in let o = !Utils.compare_terms t1 t2 in - let w = compute_equality_weight ty t1 t2 in - let e = (w, BasicProof (C.Rel index), (ty, t1, t2, o), [], []) in + let stat = (ty,t1,t2,o) in + let w = compute_equality_weight stat in + let e = (w, BasicProof (C.Rel index), stat, [], []) in Some e, (newmeta+1) | _ -> None, newmeta in ( @@ -846,17 +848,19 @@ let find_library_equalities dbd context status maxmeta = (lazy (Printf.sprintf "OK: %s" (CicPp.ppterm term))); let o = !Utils.compare_terms t1 t2 in - let w = compute_equality_weight ty t1 t2 in + let stat = (ty,t1,t2,o) in + let w = compute_equality_weight stat in let proof = BasicProof p in - let e = (w, proof, (ty, t1, t2, o), newmetas, args) in + let e = (w, proof, stat, newmetas, args) in Some e, (newmeta+1) | _ -> None, newmeta ) | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when iseq uri && not (has_vars termty) -> let o = !Utils.compare_terms t1 t2 in - let w = compute_equality_weight ty t1 t2 in - let e = (w, BasicProof term, (ty, t1, t2, o), [], []) in + let stat = (ty,t1,t2,o) in + let w = compute_equality_weight stat in + let e = (w, BasicProof term, stat, [], []) in Some e, (newmeta+1) | _ -> None, newmeta in @@ -1115,8 +1119,9 @@ let equality_of_term proof term = match term with | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri -> let o = !Utils.compare_terms t1 t2 in - let w = compute_equality_weight ty t1 t2 in - let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in + let stat = (ty,t1,t2,o) in + let w = compute_equality_weight stat in + let e = (w, BasicProof proof, stat, [], []) in e | _ -> raise TermIsNotAnEquality diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index 9bc9d2464..654195c06 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -70,7 +70,7 @@ let maximal_retained_equality = ref None;; (* equality-selection related globals *) let use_fullred = ref true;; -let weight_age_ratio = ref 4 (* 5 *);; (* settable by the user *) +let weight_age_ratio = ref 5 (* 5 *);; (* settable by the user *) let weight_age_counter = ref !weight_age_ratio ;; let symbols_ratio = ref 0 (* 3 *);; let symbols_counter = ref 0;; @@ -260,10 +260,10 @@ let rec select env goals passive (active, _) = ) | _ -> symbols_counter := !symbols_ratio; - (* let set_selection set = EqualitySet.min_elt set in *) - let set_selection l = min_elt (fun (w,_,_,_,_) -> w) l in + let set_selection set = EqualitySet.min_elt set in + (* let set_selection l = min_elt (fun (w,_,_,_,_) -> w) l in *) if EqualitySet.is_empty neg_set then - let current = set_selection pos_list in + let current = set_selection pos_set in let passive = (neg_list, neg_set), (remove current pos_list, EqualitySet.remove current pos_set), @@ -271,7 +271,7 @@ let rec select env goals passive (active, _) = in (Positive, current), passive else - let current = set_selection neg_list in + let current = set_selection neg_set in let passive = (remove current neg_list, EqualitySet.remove current neg_set), (pos_list, pos_set), diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml index 84de8800e..babf684bf 100644 --- a/components/tactics/paramodulation/utils.ml +++ b/components/tactics/paramodulation/utils.ml @@ -292,17 +292,18 @@ end module IntSet = Set.Make(OrderedInt) -let compute_equality_weight ty left right = +let compute_equality_weight (ty,left,right,o) = let metasw = ref 0 in let weight_of t = let w, m = (weight_of_term ~consider_metas:true ~count_metas_occurrences:false t) in - metasw := !metasw + (2 * (List.length m)) ; + metasw := !metasw + (1 * (List.length m)) ; w in (* Warning: the following let cannot be expanded since it forces the right evaluation order!!!! *) - let w = (weight_of ty) + (weight_of left) + (weight_of right) in + let w = (weight_of ty) + (weight_of left) + (weight_of right) in + (* let w = weight_of (Cic.Appl [ty;left;right]) in *) w + !metasw ;; diff --git a/components/tactics/paramodulation/utils.mli b/components/tactics/paramodulation/utils.mli index 9dc6501d7..bef03b141 100644 --- a/components/tactics/paramodulation/utils.mli +++ b/components/tactics/paramodulation/utils.mli @@ -81,7 +81,7 @@ type pos = Left | Right val string_of_pos: pos -> string -val compute_equality_weight: Cic.term -> Cic.term -> Cic.term -> int +val compute_equality_weight: Cic.term * Cic.term * Cic.term * comparison -> int val debug_print: string Lazy.t -> unit -- 2.39.2