X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Forderings.ml;h=6880f6d18c177d3849fd284e8bab30e9165c7723;hb=7f9e313fe5ae4200f080f481a6b8b795a0618093;hp=3da8477a961d8cb93d84d5889fb2c98f276daf2d;hpb=b60b04a930b208dc0bf8876305c4fa5ea2aeb619;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 3da8477a9..6880f6d18 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) =
@@ -44,21 +46,21 @@ module Orderings (B : Terms.Blob) = struct
     in
     let compare w1 w2 = 
       match w1, w2 with
-      | (m1, _), (m2, _) -> m2 - m1 
+      | (m1, _), (m2, _) -> m1 - m2
     in 
-    (w, List.sort compare l) (* from the biggest meta to the smallest (0) *)
+    (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
-    | Terms.Equation (_,x,_,Terms.Lt)
+    | Terms.Equation (_,x,_,Terms.Lt) 
     | Terms.Equation (x,_,_,Terms.Gt) ->
         let w, m = weight_of_term x in 
         weight_of_polynomial w m
@@ -68,92 +70,77 @@ module Orderings (B : Terms.Blob) = struct
         let wr, mr = weight_of_term r in 
         weight_of_polynomial (wl+wr) (ml@mr)
   ;;
-  
-  (* returns a "normalized" version of the polynomial weight wl (with type
-   * weight list), i.e. a list sorted ascending by meta number,
-   * from 0 to maxmeta. wl must be sorted descending by meta number. Example:
-   * normalize_weight 5 (3, [(3, 2); (1, 1)]) ->
-   *      (3, [(1, 1); (2, 0); (3, 2); (4, 0); (5, 0)]) *)
-  let normalize_weight maxmeta (cw, wl) =
-    let rec aux = function
-      | 0 -> []
-      | m -> (m, 0)::(aux (m-1))
-    in
-    let tmpl = aux maxmeta in
-    let wl =
-      List.sort
-        (fun (m, _) (n, _) -> Pervasives.compare m n)
-        (List.fold_left
-           (fun res (m, w) -> (m, w)::(List.remove_assoc m res)) tmpl wl)
-    in
-    (cw, wl)
-  ;;
-  
-  
-  let normalize_weights (cw1, wl1) (cw2, wl2) =
-    let rec aux wl1 wl2 =
-      match wl1, wl2 with
-      | [], [] -> [], []
-      | (m, w)::tl1, (n, w')::tl2 when m = n ->
-          let res1, res2 = aux tl1 tl2 in
-          (m, w)::res1, (n, w')::res2
-      | (m, w)::tl1, ((n, w')::_ as wl2) when m < n ->
-          let res1, res2 = aux tl1 wl2 in
-          (m, w)::res1, (m, 0)::res2
-      | ((m, w)::_ as wl1), (n, w')::tl2 when m > n ->
-          let res1, res2 = aux wl1 tl2 in
-          (n, 0)::res1, (n, w')::res2
-      | [], (n, w)::tl2 ->
-          let res1, res2 = aux [] tl2 in
-          (n, 0)::res1, (n, w)::res2
-      | (m, w)::tl1, [] ->
-          let res1, res2 = aux tl1 [] in
-          (m, w)::res1, (m, 0)::res2
-      | _, _ -> assert false
+
+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
-    let cmp (m, _) (n, _) = compare m n in
-    let wl1, wl2 = aux (List.sort cmp wl1) (List.sort cmp wl2) in
-    (cw1, wl1), (cw2, wl2)
+    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 *)
-  (* TODO: optimize early detection of XINCOMPARABLE case *)
+(* Compare weights normalized in a new way :
+ * Variables should be sorted from the lowest index to the highest
+ * Variables which do not occur in the term should not be present
+ * in the normalized polynomial
+ *)
   let compare_weights (h1, w1) (h2, w2) =
-    let res, diffs =
-      try
-        List.fold_left2
-          (fun ((lt, eq, gt), diffs) w1 w2 ->
-             match w1, w2 with
-             | (meta1, w1), (meta2, w2) when meta1 = meta2 ->
-                 let diffs = (w1 - w2) + diffs in 
-                 let r = compare w1 w2 in
-                 if r < 0 then (lt+1, eq, gt), diffs
-                 else if r = 0 then (lt, eq+1, gt), diffs
-                 else (lt, eq, gt+1), diffs
-             | _ -> assert false)
-          ((0, 0, 0), 0) w1 w2
-      with Invalid_argument _ -> assert false
+    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
+              else if (- diffs) >= hdiff then XLE else XINCOMPARABLE
+            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 XEQ
     in
-    let hdiff = h1 - h2 in 
-    match res with
-    | (0, _, 0) ->
-        if hdiff < 0 then XLT
-        else if hdiff > 0 then XGT
-        else XEQ 
-    | (m, _, 0) ->
-        if hdiff <= 0 then XLT
-        else if (- diffs) >= hdiff then XLE else XINCOMPARABLE
-    | (0, _, m) ->
-        if hdiff >= 0 then XGT
-        else if diffs >= (- hdiff) then XGE else XINCOMPARABLE
-    | (m, _, n) when m > 0 && n > 0 -> XINCOMPARABLE
-    | _ -> assert false 
+      aux (h1-h2) (false,false) 0 w1 w2
   ;;
   
   (* Riazanov: p. 40, relation >>> 
    * 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
@@ -181,7 +168,6 @@ module Orderings (B : Terms.Blob) = struct
   let nonrec_kbo t1 t2 =
     let w1 = weight_of_term t1 in
     let w2 = weight_of_term t2 in
-    let w1, w2 = normalize_weights w1 w2 in
     match compare_weights w1 w2 with
     | XLE ->  (* this is .> *)
         if aux_ordering t1 t2 = XLT then XLT else XINCOMPARABLE
@@ -206,7 +192,6 @@ module Orderings (B : Terms.Blob) = struct
     in
     let w1 = weight_of_term t1 in
     let w2 = weight_of_term t2 in
-    let w1, w2 = normalize_weights w1 w2 in
     let comparison = compare_weights w1 w2 in
     match comparison with
     | XLE ->
@@ -236,14 +221,137 @@ 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) ->
+          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 nonrec_kbo x y with
-    | XINCOMPARABLE -> Terms.Incomparable
-    | XGT -> Terms.Gt
-    | XLT -> Terms.Lt
-    | XEQ -> Terms.Eq
-    | _ -> assert false
+      match nonrec_kbo x y with
+(*       match lpo x y with *)
+        | XINCOMPARABLE -> Terms.Incomparable
+        | XGT -> Terms.Gt
+        | XLT -> Terms.Lt
+        | XEQ -> Terms.Eq
+        | _ -> assert false
   ;; 
 
 end