X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Forderings.ml;h=5eb3c43a5666eb9a052be298fc3cc4ed5ec0160f;hb=b714e87e96f14f332a5157567a4c62a4b28fa8eb;hp=2e1d3c4f6c9753295ef7e952e36842d363078a6f;hpb=047a0464181070aa816c189c7a6dd5ebeb68bc45;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 2e1d3c4f6..5eb3c43a5 100644
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -11,23 +11,46 @@
 
 (* $Id$ *)
 
-type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE
+type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE | XINVERTIBLE
 
-module Orderings (B : Terms.Blob) = struct
+module type Blob =
+  sig 
+    include Terms.Blob 
 
-  module Pp = Pp.Pp(B)
+    (* This order relation should be:
+     * - stable for instantiation
+     * - total on ground terms
+     *
+     *)
+    val compare_terms : 
+          t Terms.foterm -> t Terms.foterm -> Terms.comparison
+
+    val compute_clause_weight : 't Terms.clause -> int
+
+    val name : string
 
-  type weight = int * (int * int) list;;
+  end
   
-  let string_of_weight (cw, mw) =
-    let s =
-      String.concat ", "
-        (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw)
-    in
-    Printf.sprintf "[%d; %s]" cw s
-  ;;
+type weight = int * (int * int) list;;
+  
+let rec eq_foterm f x y =
+    x == y ||
+    match x, y with
+    | Terms.Leaf t1, Terms.Leaf t2 -> f t1 t2
+    | Terms.Var i, Terms.Var j -> i = j
+    | Terms.Node l1, Terms.Node l2 -> List.for_all2 (eq_foterm f) l1 l2
+    | _ -> false
+;;
+  
+let string_of_weight (cw, mw) =
+  let s =
+    String.concat ", "
+      (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw)
+  in
+  Printf.sprintf "[%d; %s]" cw s
+;;
   
-  let weight_of_term term =
+let weight_of_term term =
     let vars_dict = Hashtbl.create 5 in
     let rec aux = function
       | Terms.Var i -> 
@@ -49,9 +72,9 @@ module Orderings (B : Terms.Blob) = struct
       | (m1, _), (m2, _) -> m1 - m2
     in 
     (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
@@ -65,104 +88,126 @@ module Orderings (B : Terms.Blob) = struct
         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 *)
+(* Riazanov: 3.1.5 pag 38 *)
 (* 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 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
-      aux (h1-h2) (false,false) 0 w1 w2
-  ;;
+let compare_weights (h1, w1) (h2, w2) =
+  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 = Pervasives.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
+    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 b_compare ?(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
+  (* 2.a *)
+  | 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.Leaf _, Terms.Node _ -> XLT
+  | Terms.Node _, Terms.Leaf _ -> XGT
+  (* 2.b *)
+  | Terms.Node l1, Terms.Node l2 ->
+      let rec cmp t1 t2 =
+        match t1, t2 with
+        | [], [] -> XEQ
+        | _, [] -> (* XGT *) assert false (* hd symbols were eq *)
+        | [], _ -> (* XLT *) assert false (* hd symbols were eq *)
+        | hd1::tl1, hd2::tl2 ->
+            let o = aux_ordering b_compare ~head_only hd1 hd2 in
+            if o = XEQ && not head_only then cmp tl1 tl2 else o
+      in
+      cmp l1 l2
+;;
   
-  (* 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
-    (* 2.a *)
-    | 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.Leaf _, Terms.Node _ -> XLT
-    | Terms.Node _, Terms.Leaf _ -> XGT
-    (* 2.b *)
-    | Terms.Node l1, Terms.Node l2 ->
-        let rec cmp t1 t2 =
-          match t1, t2 with
-          | [], [] -> XEQ
-          | _, [] -> XGT
-          | [], _ -> XLT
-          | hd1::tl1, hd2::tl2 ->
-              let o = aux_ordering ~head_only hd1 hd2 in
-              if o = XEQ && not head_only then cmp tl1 tl2 else o
-        in
-        cmp l1 l2
-  ;;
+let compare_terms o x y = 
+    match o x y with
+      | XINCOMPARABLE -> Terms.Incomparable
+      | XGT -> Terms.Gt
+      | XLT -> Terms.Lt
+      | XEQ -> Terms.Eq
+      | XINVERTIBLE -> Terms.Invertible
+      | _ -> assert false
+;;
+
+let are_invertible relocate alpha_eq eq_foterm l r =
+    let varlist = (Terms.vars_of_term l)@(Terms.vars_of_term r) in
+    let maxvar = List.fold_left max 0 varlist in
+    let _,_,subst = relocate maxvar varlist FoSubst.id_subst in
+    let newl = FoSubst.apply_subst subst l in
+    let newr = FoSubst.apply_subst subst r in
+      try (let subst = alpha_eq l newr in eq_foterm newl (FoSubst.apply_subst subst r)) with
+	  FoUnif.UnificationFailure _ -> false;;
+
+module NRKBO (B : Terms.Blob) = struct
+  let name = "nrkbo"
+  include B 
+
+  module Pp = Pp.Pp(B)
+  module Unif = FoUnif.FoUnif(B)
+  module Utils = FoUtils.Utils(B)
+
+  let eq_foterm = eq_foterm B.eq;;
+
+  let are_invertible = are_invertible Utils.relocate Unif.alpha_eq eq_foterm;;
+
+  let compute_clause_weight = compute_clause_weight;;
   
   (* Riazanov: p. 40, relation >_n *)
   let nonrec_kbo t1 t2 =
@@ -170,16 +215,42 @@ let compute_goal_weight (_,l, _, _) =
     let w2 = weight_of_term t2 in
     match compare_weights w1 w2 with
     | XLE ->  (* this is .> *)
-        if aux_ordering t1 t2 = XLT then XLT else XINCOMPARABLE
+        if aux_ordering B.compare t1 t2 = XLT then XLT else XINCOMPARABLE
     | XGE -> 
-        if aux_ordering t1 t2 = XGT then XGT else XINCOMPARABLE
-    | XEQ -> aux_ordering t1 t2
+        if aux_ordering B.compare t1 t2 = XGT then XGT else XINCOMPARABLE
+    | XEQ -> let res = aux_ordering B.compare t1 t2 in
+	if res = XINCOMPARABLE && are_invertible t1 t2 then XINVERTIBLE
+	else res
     | res -> res
   ;;
+
+  let compare_terms = compare_terms nonrec_kbo;;
+
+  let profiler = HExtlib.profile ~enable:true "compare_terms(nrkbo)";;
+  let compare_terms x y =
+    profiler.HExtlib.profile (compare_terms x) y
+  ;;
+
+end
   
+module KBO (B : Terms.Blob) = struct
+  let name = "kbo"
+  include B 
+
+  module Pp = Pp.Pp(B)
+  module Unif = FoUnif.FoUnif(B)
+  module Utils = FoUtils.Utils(B)
+
+  let eq_foterm = eq_foterm B.eq;;
+
+  let are_invertible = are_invertible Utils.relocate Unif.alpha_eq eq_foterm;;
+
+  let compute_clause_weight = compute_clause_weight;;
+  let compute_goal_weight = compute_goal_weight;;
+
   (* Riazanov: p. 38, relation > *)
   let rec kbo t1 t2 =
-    let aux = aux_ordering ~head_only:true in
+    let aux = aux_ordering B.compare ~head_only:true in
     let rec cmp t1 t2 =
       match t1, t2 with
       | [], [] -> XEQ
@@ -216,141 +287,103 @@ let compute_goal_weight (_,l, _, _) =
         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 
     | res -> res
   ;;
 
+  let compare_terms = compare_terms kbo;;
+
+  let profiler = HExtlib.profile ~enable:true "compare_terms(kbo)";;
+  let compare_terms x y =
+    profiler.HExtlib.profile (compare_terms x) y
+  ;;
+
+end
+
+module LPO (B : Terms.Blob) = struct
+  let name = "lpo"
+  include B 
+
+  module Pp = Pp.Pp(B)
+  module Unif = FoUnif.FoUnif(B)
+  module Utils = FoUtils.Utils(B)
+
+  let eq_foterm = eq_foterm B.eq;;
+
+  let are_invertible = are_invertible Utils.relocate Unif.alpha_eq eq_foterm;;
+
+  let compute_clause_weight = compute_clause_weight;;
+  let compute_goal_weight = compute_goal_weight;;
+
   let rec lpo s t =
     match s,t with
-      | s, t when s = t ->
-	  XEQ
+      | s, t when eq_foterm s t ->
+          XEQ
       | Terms.Var _, Terms.Var _ ->
-	  XINCOMPARABLE
+          XINCOMPARABLE
       | _, Terms.Var i ->
-	  if (List.mem i (Terms.vars_of_term s)) then XGT
-	  else XINCOMPARABLE
+          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
+          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 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 B.compare 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 B.compare 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 = compare_terms lpo;;
 
-  let compare_terms x y = 
-      match lpo x y with
-	| XINCOMPARABLE -> Terms.Incomparable
-	| XGT -> Terms.Gt
-	| XLT -> Terms.Lt
-	| XEQ -> Terms.Eq
-	| _ -> assert false
-  ;; 
+  let profiler = HExtlib.profile ~enable:true "compare_terms(lpo)";;
+  let compare_terms x y =
+    profiler.HExtlib.profile (compare_terms x) y
+  ;;
 
 end
+