From dd5b7e474d70a87846f977f887d045f77342ae62 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 19 Jun 2006 13:03:33 +0000 Subject: [PATCH] added (but not yet used) remove_local_context weight of non oriented equations decreased --- components/tactics/paramodulation/utils.ml | 9 ++++++++- components/tactics/paramodulation/utils.mli | 2 ++ 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml index 8b67ddb05..a25ba8e2d 100644 --- a/components/tactics/paramodulation/utils.ml +++ b/components/tactics/paramodulation/utils.ml @@ -103,6 +103,13 @@ let metas_of_term term = aux term ;; +let rec remove_local_context = + function + | Cic.Meta (i,_) -> Cic.Meta (i,[]) + | Cic.Appl l -> + Cic.Appl(List.map remove_local_context l) + | t -> t + (************************* rpo ********************************) let number = [ @@ -311,7 +318,7 @@ let compute_equality_weight (ty,left,right,o) = ~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)) + (max w1 w2)+(max (factor * (List.length m1)) (factor * (List.length m2))) ;; (* old diff --git a/components/tactics/paramodulation/utils.mli b/components/tactics/paramodulation/utils.mli index 5e3f61e1a..c64eacfd6 100644 --- a/components/tactics/paramodulation/utils.mli +++ b/components/tactics/paramodulation/utils.mli @@ -88,3 +88,5 @@ val compute_equality_weight: Cic.term * Cic.term * Cic.term * comparison -> int val debug_print: string Lazy.t -> unit val metas_of_term: Cic.term -> int list + +val remove_local_context: Cic.term -> Cic.term -- 2.39.2