Tried to implement lpo in a more efficient way

[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 f2e0273c84a5b4976d7baf3187e97dafb35d5250..2e1d3c4f6c9753295ef7e952e36842d363078a6f 100644 (file)
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -15,6 +15,8 @@ type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE
 
 module Orderings (B : Terms.Blob) = struct
 
+  module Pp = Pp.Pp(B)
+
   type weight = int * (int * int) list;;
   
   let string_of_weight (cw, mw) =
@@ -222,43 +224,133 @@ let compute_goal_weight (_,l, _, _) =
 
   let rec lpo s t =
     match s,t with
-      | Terms.Var i, Terms.Var j when i = j ->
+      | s, t when s = t ->
          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.Var i,_ ->
+         if (List.mem i (Terms.vars_of_term t)) then XLT
+         else XINCOMPARABLE
       | 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 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
+                     else XINCOMPARABLE
+                   | XLT ->
+                       if List.for_all (fun x -> lpo x t = XLT) tl1 then XLT
+                     else XINCOMPARABLE
+                   | o -> o)   
+             | XINCOMPARABLE -> XINCOMPARABLE
+             | _ -> assert false
+         end
+      | _,_ -> aux_ordering s t
            
   ;;
 
+let rec lpo_old t1 t2 =
+  match t1, t2 with
+  | t1, t2 when t1 = t2 -> XEQ
+  | t1, (Terms.Var m) ->
+      if List.mem m (Terms.vars_of_term t1) then XGT else XINCOMPARABLE
+  | (Terms.Var m), t2 ->
+      if List.mem m (Terms.vars_of_term t2) then XLT else XINCOMPARABLE
+  | Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) -> (
+      let res =
+        let f o r t =
+          if r then true else
+            match lpo_old t o with
+            | XGT | XEQ -> true
+            | _ -> false
+        in
+        let res1 = List.fold_left (f t2) false tl1 in
+        if res1 then XGT
+        else let res2 = List.fold_left (f t1) false tl2 in
+        if res2 then XLT
+        else XINCOMPARABLE
+      in
+      if res <> XINCOMPARABLE then
+        res
+      else
+        let f o r t =
+          if not r then false else
+            match lpo_old o t with
+            | XGT -> true
+            | _ -> false
+        in
+        match aux_ordering hd1 hd2 with
+        | XGT ->
+            let res = List.fold_left (f t1) true tl2 in
+            if res then XGT
+            else XINCOMPARABLE
+        | XLT ->
+            let res = List.fold_left (f t2) true tl1 in
+            if res then XLT
+            else XINCOMPARABLE
+        | XEQ -> (
+            let lex_res =
+              try
+                List.fold_left2
+                  (fun r t1 t2 -> if r <> XEQ then r else lpo_old t1 t2)
+                  XEQ tl1 tl2
+              with Invalid_argument _ ->
+                XINCOMPARABLE
+            in
+            match lex_res with
+            | XGT ->
+                if List.fold_left (f t1) true tl2 then XGT
+                else XINCOMPARABLE
+            | XLT ->
+                if List.fold_left (f t2) true tl1 then XLT
+                else XINCOMPARABLE
+            | _ -> XINCOMPARABLE
+          )
+        | _ -> XINCOMPARABLE
+    )
+  | t1, t2 -> aux_ordering t1 t2
+;;
+
   let compare_terms x y = 
-    match kbo x y with
-    | XINCOMPARABLE -> Terms.Incomparable
-    | XGT -> Terms.Gt
-    | XLT -> Terms.Lt
-    | XEQ -> Terms.Eq
-    | _ -> assert false
+      match lpo x y with
+       | XINCOMPARABLE -> Terms.Incomparable
+       | XGT -> Terms.Gt
+       | XLT -> Terms.Lt
+       | XEQ -> Terms.Eq
+       | _ -> assert false
   ;; 
 
 end