Tried to implement lpo in a more efficient way

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 85a1497a753361141d922fd4c31eb15f5fe4f67d..2e1d3c4f6c9753295ef7e952e36842d363078a6f 100644 (file)
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -235,21 +235,38 @@ let compute_goal_weight (_,l, _, _) =
          if (List.mem i (Terms.vars_of_term t)) then XLT
          else XINCOMPARABLE
       | Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) ->
-         if List.exists (fun x -> let o = lpo x t in o=XGT || o=XEQ) tl1
-         then XGT
-         else if List.exists (fun x -> let o=lpo s x in o=XLT || o=XEQ) tl2
-         then XLT
-         else begin
-           match aux_ordering 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 x t = XLT) tl1 then XLT
-               else XINCOMPARABLE
-             | XEQ -> 
-              let lex = List.fold_left2
-                (fun acc si ti -> if acc = XEQ then lpo si ti else acc)
-                XEQ tl1 tl2
-              in
+         let rec ge_subterm t ol = function
+           | [] -> (false, ol)
+           | x::tl ->
+               let res = lpo x t in
+               match res with
+                 | XGT | XEQ -> (true,res::ol)
+                 | o -> ge_subterm t (o::ol) tl
+         in
+         let (res, l_ol) = ge_subterm t [] tl1 in
+           if res then XGT
+           else let (res, r_ol) = ge_subterm s [] tl2 in
+             if res then XLT
+             else begin
+               let rec check_subterms t = function
+                 | _,[] -> true
+                 | o::ol,_::tl ->
+                     if o = XLT then check_subterms t (ol,tl)
+                     else false
+                 | [], x::tl ->
+                     if lpo x t = XLT then check_subterms t ([],tl)
+                     else false
+               in
+               match aux_ordering hd1 hd2 with
+                 | XGT -> if check_subterms s (r_ol,tl2) then XGT
+                   else XINCOMPARABLE
+                 | XLT -> if check_subterms t (l_ol,tl1) then XLT
+                   else XINCOMPARABLE
+                 | XEQ -> 
+                     let lex = List.fold_left2
+                       (fun acc si ti -> if acc = XEQ then lpo si ti else acc)
+                       XEQ tl1 tl2
+                     in
                 (match lex with
                    | XGT ->
                        if List.for_all (fun x -> lpo s x = XGT) tl2 then XGT