Fixes

[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 ba6969aeb143ddaa1df97d72ea3ff61b4c2bcaab..47f6b4512cb33c452653221d258690d9b08b9087 100644 (file)
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -11,7 +11,7 @@
 
 (* $Id$ *)
 
-type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE
+type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE | XINVERTIBLE
 
 module type Blob =
   sig 
@@ -25,9 +25,7 @@ module type Blob =
     val compare_terms : 
           t Terms.foterm -> t Terms.foterm -> Terms.comparison
 
-    val compute_unit_clause_weight : 't Terms.unit_clause -> int
-
-    val compute_goal_weight : 't Terms.unit_clause -> int
+    val compute_clause_weight : 't Terms.clause -> int
 
     val name : string
 
@@ -76,7 +74,7 @@ let weight_of_term term =
     (w, List.sort compare l) (* from the smallest meta to the bigest *)
 ;;
   
-let compute_unit_clause_weight (_,l, _, _) = 
+let compute_literal_weight l =
     let weight_of_polynomial w m =
       let factor = 2 in      
       w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
@@ -90,28 +88,17 @@ let compute_unit_clause_weight (_,l, _, _) =
         let w, m = weight_of_term x in 
         weight_of_polynomial w m
     | Terms.Equation (l,r,_,Terms.Eq) 
-    | Terms.Equation (l,r,_,Terms.Incomparable) ->
+    | Terms.Equation (l,r,_,Terms.Incomparable) 
+    | Terms.Equation (l,r,_,Terms.Invertible) ->
         let wl, ml = weight_of_term l in 
         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))
-  ;;
+let compute_clause_weight (_,nl,pl,_,_) =
+  List.fold_left (fun acc (lit,_) -> compute_literal_weight lit + acc) 0 (nl@pl)
+
+let compute_goal_weight = compute_clause_weight;;
   
 (* Riazanov: 3.1.5 pag 38 *)
 (* Compare weights normalized in a new way :
@@ -195,6 +182,7 @@ let compare_terms o x y =
       | XGT -> Terms.Gt
       | XLT -> Terms.Lt
       | XEQ -> Terms.Eq
+      | XINVERTIBLE -> Terms.Invertible
       | _ -> assert false
 ;;
 
@@ -206,8 +194,52 @@ module NRKBO (B : Terms.Blob) = struct
 
   let eq_foterm = eq_foterm B.eq;;
 
-  let compute_unit_clause_weight = compute_unit_clause_weight;;
-  let compute_goal_weight = compute_goal_weight;;
+exception UnificationFailure of string Lazy.t;;
+
+
+(* DUPLICATE CODE FOR TESTS (see FoUnif)  *)
+  let alpha_eq s t =
+    let rec equiv subst s t =
+      let s = match s with Terms.Var i -> FoSubst.lookup i subst | _ -> s
+      and t = match t with Terms.Var i -> FoSubst.lookup i subst | _ -> t
+        
+      in
+      match s, t with
+        | s, t when eq_foterm s t -> subst
+        | Terms.Var i, Terms.Var j
+            when (not (List.exists (fun (_,k) -> k=t) subst)) ->
+            let subst = FoSubst.build_subst i t subst in
+              subst
+        | Terms.Node l1, Terms.Node l2 -> (
+            try
+              List.fold_left2
+                (fun subst' s t -> equiv subst' s t)
+                subst l1 l2
+            with Invalid_argument _ ->
+              raise (UnificationFailure (lazy "Inference.unification.unif"))
+          )
+        | _, _ ->
+            raise (UnificationFailure (lazy "Inference.unification.unif"))
+    in
+      equiv FoSubst.id_subst s t
+;;
+
+let relocate maxvar varlist subst =
+    List.fold_right
+      (fun i (maxvar, varlist, s) -> 
+         maxvar+1, maxvar::varlist, FoSubst.build_subst i (Terms.Var maxvar) s)
+      varlist (maxvar+1, [], subst)
+  ;;
+
+  let are_invertible l r =
+    let varlist = Terms.vars_of_term l in
+    let maxvar = List.fold_left max 0 varlist in
+    let _,_,subst = relocate maxvar varlist FoSubst.id_subst in
+    let l = FoSubst.apply_subst subst l in
+      try (ignore(alpha_eq l r);true) with
+         UnificationFailure _ -> false
+
+  let compute_clause_weight = compute_clause_weight;;
   
   (* Riazanov: p. 40, relation >_n *)
   let nonrec_kbo t1 t2 =
@@ -218,7 +250,9 @@ module NRKBO (B : Terms.Blob) = struct
         if aux_ordering B.compare t1 t2 = XLT then XLT else XINCOMPARABLE
     | XGE -> 
         if aux_ordering B.compare t1 t2 = XGT then XGT else XINCOMPARABLE
-    | XEQ -> aux_ordering B.compare t1 t2
+    | XEQ -> let res = aux_ordering B.compare t1 t2 in
+       if res = XINCOMPARABLE && are_invertible t1 t2 then XINVERTIBLE
+       else res
     | res -> res
   ;;
 
@@ -239,7 +273,7 @@ module KBO (B : Terms.Blob) = struct
 
   let eq_foterm = eq_foterm B.eq;;
 
-  let compute_unit_clause_weight = compute_unit_clause_weight;;
+  let compute_clause_weight = compute_clause_weight;;
   let compute_goal_weight = compute_goal_weight;;
 
   (* Riazanov: p. 38, relation > *)
@@ -281,6 +315,7 @@ module KBO (B : Terms.Blob) = struct
         let r = aux t1 t2 in
         if r = XEQ then (
           match t1, t2 with
+         | Terms.Var i, Terms.Var j when i=j -> XEQ
           | Terms.Node (_::tl1), Terms.Node (_::tl2) -> cmp tl1 tl2
           | _, _ ->  XINCOMPARABLE
         ) else r 
@@ -304,7 +339,7 @@ module LPO (B : Terms.Blob) = struct
 
   let eq_foterm = eq_foterm B.eq;;
 
-  let compute_unit_clause_weight = compute_unit_clause_weight;;
+  let compute_clause_weight = compute_clause_weight;;
   let compute_goal_weight = compute_goal_weight;;
 
   let rec lpo s t =