X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Forderings.ml;h=28fbe15073ae2fc32abf0dbfeda32e0e15726e2b;hb=2f77bd6071bd316ed0a91448f4c04e638f853442;hp=85a1497a753361141d922fd4c31eb15f5fe4f67d;hpb=c900512d028a10f1caf89677c9a7dd61c7a64856;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 85a1497a7..28fbe1507 100644
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -18,6 +18,15 @@ module Orderings (B : Terms.Blob) = struct
   module Pp = Pp.Pp(B)
 
   type weight = int * (int * int) list;;
+
+let rec eq_foterm x y =
+    x == y ||
+    match x, y with
+    | Terms.Leaf t1, Terms.Leaf t2 -> B.eq t1 t2
+    | Terms.Var i, Terms.Var j -> i = j
+    | Terms.Node l1, Terms.Node l2 -> List.for_all2 eq_foterm l1 l2
+    | _ -> false
+  ;;
   
   let string_of_weight (cw, mw) =
     let s =
@@ -83,9 +92,9 @@ let compute_goal_weight (_,l, _, _) =
     | Terms.Equation (l,r,_,_) ->
         let wl, ml = weight_of_term l in 
         let wr, mr = weight_of_term r in 
-	let wl = weight_of_polynomial wl ml in
-	let wr = weight_of_polynomial wr mr in
-	  - (abs (wl-wr))
+        let wl = weight_of_polynomial wl ml in
+        let wr = weight_of_polynomial wr mr in
+          - (abs (wl-wr))
   ;;
   
   (* Riazanov: 3.1.5 pag 38 *)
@@ -97,36 +106,36 @@ let compute_goal_weight (_,l, _, _) =
   let compare_weights (h1, w1) (h2, w2) =
     let rec aux hdiff (lt, gt) diffs w1 w2 =
       match w1, w2 with
-	| ((var1, w1)::tl1) as l1, (((var2, w2)::tl2) as l2) ->
-	    if var1 = var2 then
-	      let diffs = (w1 - w2) + diffs in
-	      let r = compare w1 w2 in
-	      let lt = lt or (r < 0) in
-	      let gt = gt or (r > 0) in
-		if lt && gt then XINCOMPARABLE else
-		  aux hdiff (lt, gt) diffs tl1 tl2
-	    else if var1 < var2 then
-	      if lt then XINCOMPARABLE else
-		aux hdiff (false,true) (diffs+w1) tl1 l2	
-	    else
-	      if gt then XINCOMPARABLE else
-		aux hdiff (true,false) (diffs-w2) l1 tl2
-	| [], (_,w2)::tl2 ->
-	    if gt then XINCOMPARABLE else
-	      aux hdiff (true,false) (diffs-w2) [] tl2
-	| (_,w1)::tl1, [] ->
-	    if lt then XINCOMPARABLE else
-	      aux hdiff (false,true) (diffs+w1) tl1 []
-	| [], [] ->
-	    if lt then
-	      if hdiff <= 0 then XLT
+        | ((var1, w1)::tl1) as l1, (((var2, w2)::tl2) as l2) ->
+            if var1 = var2 then
+              let diffs = (w1 - w2) + diffs in
+              let r = compare w1 w2 in
+              let lt = lt or (r < 0) in
+              let gt = gt or (r > 0) in
+                if lt && gt then XINCOMPARABLE else
+                  aux hdiff (lt, gt) diffs tl1 tl2
+            else if var1 < var2 then
+              if lt then XINCOMPARABLE else
+                aux hdiff (false,true) (diffs+w1) tl1 l2        
+            else
+              if gt then XINCOMPARABLE else
+                aux hdiff (true,false) (diffs-w2) l1 tl2
+        | [], (_,w2)::tl2 ->
+            if gt then XINCOMPARABLE else
+              aux hdiff (true,false) (diffs-w2) [] tl2
+        | (_,w1)::tl1, [] ->
+            if lt then XINCOMPARABLE else
+              aux hdiff (false,true) (diffs+w1) tl1 []
+        | [], [] ->
+            if lt then
+              if hdiff <= 0 then XLT
               else if (- diffs) >= hdiff then XLE else XINCOMPARABLE
-	    else if gt then
-	      if hdiff >= 0 then XGT
+            else if gt then
+              if hdiff >= 0 then XGT
               else if diffs >= (- hdiff) then XGE else XINCOMPARABLE
-	    else
-	      if hdiff < 0 then XLT
-	      else if hdiff > 0 then XGT
+            else
+              if hdiff < 0 then XLT
+              else if hdiff > 0 then XGT
               else XEQ
     in
       aux (h1-h2) (false,false) 0 w1 w2
@@ -140,7 +149,7 @@ let compute_goal_weight (_,l, _, _) =
      * If we give back XEQ, no inference rule    *
      * will be applied on this equality          *)
     | Terms.Var i, Terms.Var j when i = j ->
-	XEQ
+        XEQ
     (* 1. *)
     | Terms.Var _, _
     | _, Terms.Var _ -> XINCOMPARABLE
@@ -224,116 +233,76 @@ let compute_goal_weight (_,l, _, _) =
 
   let rec lpo s t =
     match s,t with
-      | s, t when s = t ->
-	  XEQ
+      | s, t when eq_foterm s t ->
+          XEQ
       | Terms.Var _, Terms.Var _ ->
-	  XINCOMPARABLE
+          XINCOMPARABLE
       | _, Terms.Var i ->
-	  if (List.mem i (Terms.vars_of_term s)) then XGT
-	  else XINCOMPARABLE
+          if (List.mem i (Terms.vars_of_term s)) then XGT
+          else XINCOMPARABLE
       | Terms.Var i,_ ->
-	  if (List.mem i (Terms.vars_of_term t)) then XLT
-	  else XINCOMPARABLE
+          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
-		 (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
+          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 lpo x y with
-	| XINCOMPARABLE -> Terms.Incomparable
-	| XGT -> Terms.Gt
-	| XLT -> Terms.Lt
-	| XEQ -> Terms.Eq
-	| _ -> assert false
-  ;; 
+      match nonrec_kbo x y with
+        | XINCOMPARABLE -> Terms.Incomparable
+        | XGT -> Terms.Gt
+        | XLT -> Terms.Lt
+        | XEQ -> Terms.Eq
+        | _ -> assert false
+  ;;
+
+  let profiler = HExtlib.profile ~enable:true "compare_terms";;
+  let compare_terms x y =
+    profiler.HExtlib.profile (compare_terms x) y
+  ;;
 
 end