From ad4b678b155e33fc9bf7264a18f7d60a9fc62ec0 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 22 Mar 2006 13:47:39 +0000 Subject: [PATCH] : This line, and those below, will be ignored-- M tactics/paramodulation/utils.ml --- components/tactics/paramodulation/utils.ml | 25 +++++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml index babf684bf..8fb1d42bc 100644 --- a/components/tactics/paramodulation/utils.ml +++ b/components/tactics/paramodulation/utils.ml @@ -292,6 +292,29 @@ end module IntSet = Set.Make(OrderedInt) +let compute_equality_weight (ty,left,right,o) = + let factor = 1 in + match o with + | Lt -> + let w, m = (weight_of_term + ~consider_metas:true ~count_metas_occurrences:false right) in + w + (factor * (List.length m)) ; + | Le -> assert false + | Gt -> + let w, m = (weight_of_term + ~consider_metas:true ~count_metas_occurrences:false left) in + w + (factor * (List.length m)) ; + | Ge -> assert false + | Eq + | Incomparable -> + let w1, m1 = (weight_of_term + ~consider_metas:true ~count_metas_occurrences:false right) in + let w2, m2 = (weight_of_term + ~consider_metas:true ~count_metas_occurrences:false left) in + w1 + w2 + (factor * (List.length m1)) + (factor * (List.length m2)) +;; + +(* old let compute_equality_weight (ty,left,right,o) = let metasw = ref 0 in let weight_of t = @@ -306,7 +329,7 @@ let compute_equality_weight (ty,left,right,o) = (* let w = weight_of (Cic.Appl [ty;left;right]) in *) w + !metasw ;; - +*) (* returns a "normalized" version of the polynomial weight wl (with type * weight list), i.e. a list sorted ascending by meta number, -- 2.39.2