Implemented LPO

[helm.git] / helm / software / components / ng_paramodulation / orderings.ml

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 7c8a80995d697479fa9d15540fa84fc39433d5aa..f2e0273c84a5b4976d7baf3187e97dafb35d5250 100644 (file)
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -49,12 +49,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 +68,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 +134,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,9 +219,41 @@ module Orderings (B : Terms.Blob) = struct
         ) else r 
     | res -> res
   ;;
-            
+
+  let rec lpo s t =
+    match s,t with
+      | Terms.Var i, Terms.Var j when i = j ->
+         XEQ
+      | Terms.Var _, Terms.Var _ ->
+         XINCOMPARABLE
+      | Terms.Var _, _ ->
+         (match lpo t s with
+           | XGT -> XLT
+           | XLT -> XGT
+           | o -> o)
+      | _, Terms.Var i ->
+         if (List.mem i (Terms.vars_of_term s)) then XGT
+         else XINCOMPARABLE
+      | Terms.Leaf a1, Terms.Leaf a2 -> 
+          let cmp = B.compare a1 a2 in
+            if cmp = 0 then XEQ else if cmp < 0 then XLT else XGT
+      | Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) ->
+         (match lpo 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 s x = XLT) tl2 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)
+      | _ -> assert false
+           
+  ;;
+
   let compare_terms x y = 
-    match nonrec_kbo x y with
+    match kbo x y with
     | XINCOMPARABLE -> Terms.Incomparable
     | XGT -> Terms.Gt
     | XLT -> Terms.Lt