From c900512d028a10f1caf89677c9a7dd61c7a64856 Mon Sep 17 00:00:00 2001
From: denes <??>
Date: Mon, 6 Jul 2009 10:01:54 +0000
Subject: [PATCH] Fixed typo in lpo (from old implementation)

---
 .../components/ng_paramodulation/orderings.ml | 64 +++++--------------
 1 file changed, 16 insertions(+), 48 deletions(-)

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index b95593df2..85a1497a7 100644
--- 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) =
@@ -221,58 +223,24 @@ let compute_goal_weight (_,l, _, _) =
   ;;
 
   let rec lpo s t =
-    let cmp a1 a2 =
-      let res = B.compare a1 a2 in
-	if res = 0 then XEQ else if res < 0 then XLT else XGT
-    in
     match s,t with
       | s, t when s = t ->
 	  XEQ
       | Terms.Var _, Terms.Var _ ->
 	  XINCOMPARABLE
-      | Terms.Leaf a1, Terms.Leaf a2 ->
-	  cmp a1 a2
       | _, Terms.Var i ->
 	  if (List.mem i (Terms.vars_of_term s)) then XGT
 	  else XINCOMPARABLE
-      | Terms.Var _, _ ->
-      (*| Terms.Leaf _, Terms.Node _ -> *)
-	  (match lpo t s with
-	    | XGT -> XLT
-	    | XLT -> XGT
-	    | o -> o)
-      (*| Terms.Node (Terms.Leaf a1::tl), Terms.Leaf a2 ->
-	  (match cmp a1 a2 with
-	    | XGT -> XGT
-	    | _ -> 
-		if List.exists (fun x -> let o = lpo x t in o=XGT || o=XEQ) tl
-		then XGT
-		else XINCOMPARABLE)*)
+      | Terms.Var i,_ ->
+	  if (List.mem i (Terms.vars_of_term t)) then XLT
+	  else XINCOMPARABLE
       | Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) ->
-(*	  let lo = List.map (lpo s) tl2 in
-	  let ro = List.map (lpo t) tl1 in
-	    if List.exists (fun x -> x=XGT || x=XEQ) lo
-	    then XGT
-	    else if List.exists (fun x -> x=XGT || x=XEQ) ro
-	    then XLT
-	    else begin
-	      match lpo hd1 hd2 with
-		| XGT -> if List.for_all (fun x -> x=XGT) lo then XGT
-		  else XINCOMPARABLE
-		| XLT -> if List.for_all (fun x -> x=XGT) ro 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
-	    end*)
 	  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 lpo hd1 hd2 with
+	    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
@@ -329,11 +297,11 @@ let rec lpo_old t1 t2 =
         in
         match aux_ordering hd1 hd2 with
         | XGT ->
-            let res = List.fold_left (f t1) false tl2 in
+            let res = List.fold_left (f t1) true tl2 in
             if res then XGT
             else XINCOMPARABLE
         | XLT ->
-            let res = List.fold_left (f t2) false tl1 in
+            let res = List.fold_left (f t2) true tl1 in
             if res then XLT
             else XINCOMPARABLE
         | XEQ -> (
@@ -347,10 +315,10 @@ let rec lpo_old t1 t2 =
             in
             match lex_res with
             | XGT ->
-                if List.fold_left (f t1) false tl2 then XGT
+                if List.fold_left (f t1) true tl2 then XGT
                 else XINCOMPARABLE
             | XLT ->
-                if List.fold_left (f t2) false tl1 then XLT
+                if List.fold_left (f t2) true tl1 then XLT
                 else XINCOMPARABLE
             | _ -> XINCOMPARABLE
           )
@@ -360,12 +328,12 @@ let rec lpo_old t1 t2 =
 ;;
 
   let compare_terms x y = 
-    match lpo_old 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
-- 
2.39.2