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

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 7c8a80995..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) =
@@ -49,12 +51,12 @@ module Orderings (B : Terms.Blob) = struct
     (w, List.sort compare l) (* from the smallest meta to the bigest *)
   ;;
   
-  let compute_unit_clause_weight = 
+  let compute_unit_clause_weight (_,l, _, _) = 
     let weight_of_polynomial w m =
       let factor = 2 in      
       w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
     in
-    function
+    match l with
     | Terms.Predicate t -> 
         let w, m = weight_of_term t in 
         weight_of_polynomial w m
@@ -68,6 +70,23 @@ module Orderings (B : Terms.Blob) = struct
         let wr, mr = weight_of_term r in 
         weight_of_polynomial (wl+wr) (ml@mr)
   ;;
+
+let compute_goal_weight (_,l, _, _) = 
+    let weight_of_polynomial w m =
+      let factor = 2 in      
+      w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
+    in
+    match l with
+    | Terms.Predicate t -> 
+        let w, m = weight_of_term t in 
+        weight_of_polynomial w m
+    | 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))
+  ;;
   
   (* Riazanov: 3.1.5 pag 38 *)
 (* Compare weights normalized in a new way :
@@ -117,6 +136,11 @@ module Orderings (B : Terms.Blob) = struct
    * if head_only=true then it is not >>> but helps case 2 of 3.14 p 39 *)
   let rec aux_ordering ?(head_only=false) t1 t2 =
     match t1, t2 with
+    (* We want to discard any identity equality. *
+     * If we give back XEQ, no inference rule    *
+     * will be applied on this equality          *)
+    | Terms.Var i, Terms.Var j when i = j ->
+	XEQ
     (* 1. *)
     | Terms.Var _, _
     | _, Terms.Var _ -> XINCOMPARABLE
@@ -197,14 +221,119 @@ module Orderings (B : Terms.Blob) = struct
         ) else r 
     | res -> res
   ;;
-            
+
+  let rec lpo s t =
+    match s,t with
+      | s, t when s = t ->
+	  XEQ
+      | Terms.Var _, Terms.Var _ ->
+	  XINCOMPARABLE
+      | _, Terms.Var i ->
+	  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
+      | 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
+      | _,_ -> 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 nonrec_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