Changed the type of compute-equality_weight that now takes also

[helm.git] / helm / software / components / tactics / paramodulation / saturation.ml

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 9bc9d2464421e136230468ea7cc09b23addc3916..654195c06360bd16ee0d274a3d5425bc1723774b 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/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),