Implemented LPO

[helm.git] / helm / software / components / ng_paramodulation / orderings.ml

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 5c42090c4508d03308809a78d125d65590d73b6c..f2e0273c84a5b4976d7baf3187e97dafb35d5250 100644 (file)
--- 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