From: denes <??>
Date: Mon, 6 Jul 2009 10:28:04 +0000 (+0000)
Subject: Tried to implement lpo in a more efficient way
X-Git-Tag: make_still_working~3748
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=047a0464181070aa816c189c7a6dd5ebeb68bc45;p=helm.git

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 85a1497a7..2e1d3c4f6 100644
--- 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