New version of compare_weights.

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index 70a77c8e8c8c1292af5ce3b745be47846a7299aa..0a2cd4502a02cea18d16865ddaf2719f62971265 100644 (file)
--- a/helm/ocaml/paramodulation/utils.ml
+++ b/helm/ocaml/paramodulation/utils.ml
@@ -23,8 +23,6 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(* $Id$ *)
-
 let debug = true;;
 
 let debug_print s = if debug then prerr_endline (Lazy.force s);;
@@ -107,7 +105,7 @@ let weight_of_term ?(consider_metas=true) term =
   let compare w1 w2 = 
     match w1, w2 with
     | (m1, _), (m2, _) -> m2 - m1 
-  in
+  in 
   (w, List.sort compare l) (* from the biggest meta to the smallest (0) *)
 ;;
 
@@ -235,17 +233,23 @@ let compare_weights ?(normalize=false)
       else if hdiff > 0 then Gt
       else Eq (* Incomparable *)
   | (m, _, 0) ->
+      if diffs < (- hdiff) then Lt
+      else if diffs = (- hdiff) then Le else Incomparable
+(*
       if hdiff <= 0 then 
         if m > 0 || hdiff < 0 then Lt
         else if diffs >= (- hdiff) then Le else Incomparable
       else 
-        if diffs >= (- hdiff) then Le else Incomparable
+        if diffs >= (- hdiff) then Le else Incomparable *)
   | (0, _, m) ->
+      if (- hdiff) < diffs then Gt
+      else if (- hdiff) = diffs then Ge else Incomparable
+(*
       if hdiff >= 0 then 
         if m > 0 || hdiff > 0 then Gt
         else if (- diffs) >= hdiff then Ge else Incomparable
       else
-        if (- diffs) >= hdiff then Ge else Incomparable
+        if (- diffs) >= hdiff then Ge else Incomparable *)
   | (m, _, n) when m > 0 && n > 0 ->
       Incomparable
   | _ -> assert false
@@ -321,6 +325,10 @@ let nonrec_kbo_w (t1, w1) (t2, w2) =
 let nonrec_kbo t1 t2 =
   let w1 = weight_of_term t1 in
   let w2 = weight_of_term t2 in
+  (* 
+  prerr_endline ("weight1 :"^(string_of_weight w1));
+  prerr_endline ("weight2 :"^(string_of_weight w2)); 
+  *)
   match compare_weights ~normalize:true w1 w2 with
   | Le -> if aux_ordering t1 t2 = Lt then Lt else Incomparable
   | Ge -> if aux_ordering t1 t2 = Gt then Gt else Incomparable
@@ -549,8 +557,8 @@ let rec lpo t1 t2 =
 
 
 (* settable by the user... *)
-(* let compare_terms = ref nonrec_kbo;; *)
-let compare_terms = ref ao;;
+let compare_terms = ref nonrec_kbo;; 
+(* let compare_terms = ref ao;; *)
 
 let guarded_simpl context t =
   let t' = ProofEngineReduction.simpl context t in