X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Forderings.ml;h=f2e0273c84a5b4976d7baf3187e97dafb35d5250;hb=016f069da6221053873b4d505716ef1bd80f08b6;hp=5c42090c4508d03308809a78d125d65590d73b6c;hpb=b69275324ae2d436f2f4dbb70e0ddcbdf3886636;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 5c42090c4..f2e0273c8 100644
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -219,9 +219,41 @@ let compute_goal_weight (_,l, _, _) =
         ) else r 
     | res -> res
   ;;
-            
+
+  let rec lpo s t =
+    match s,t with
+      | Terms.Var i, Terms.Var j when i = j ->
+	  XEQ
+      | Terms.Var _, Terms.Var _ ->
+	  XINCOMPARABLE
+      | Terms.Var _, _ ->
+	  (match lpo t s with
+	    | XGT -> XLT
+	    | XLT -> XGT
+	    | o -> o)
+      | _, Terms.Var i ->
+	  if (List.mem i (Terms.vars_of_term s)) then XGT
+	  else XINCOMPARABLE
+      | Terms.Leaf a1, Terms.Leaf a2 -> 
+          let cmp = B.compare a1 a2 in
+            if cmp = 0 then XEQ else if cmp < 0 then XLT else XGT
+      | Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) ->
+	  (match lpo hd1 hd2 with
+	    | XGT -> if List.for_all (fun x -> lpo s x = XGT) tl2 then XGT
+	      else XINCOMPARABLE
+	    | XLT -> if List.for_all (fun x -> lpo s x = XLT) tl2 then XLT
+	      else XINCOMPARABLE
+	    | XEQ -> List.fold_left2
+		(fun acc si ti -> if acc = XEQ then lpo si ti else acc)
+		  XEQ tl1 tl2
+	    | XINCOMPARABLE -> XINCOMPARABLE
+	    | _ -> assert false)
+      | _ -> assert false
+	    
+  ;;
+
   let compare_terms x y = 
-    match nonrec_kbo x y with
+    match kbo x y with
     | XINCOMPARABLE -> Terms.Incomparable
     | XGT -> Terms.Gt
     | XLT -> Terms.Lt