From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 4 Jun 2009 09:52:15 +0000 (+0000)
Subject: better type for comparison and implementation of KBO orderings
X-Git-Tag: make_still_working~3924
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b60b04a930b208dc0bf8876305c4fa5ea2aeb619;p=helm.git

better type for comparison and implementation of KBO orderings
---

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index dde09e81f..3da8477a9 100644
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -11,6 +11,8 @@
 
 (* $Id$ *)
 
+type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE
+
 module Orderings (B : Terms.Blob) = struct
 
   type weight = int * (int * int) list;;
@@ -47,27 +49,24 @@ module Orderings (B : Terms.Blob) = struct
     (w, List.sort compare l) (* from the biggest meta to the smallest (0) *)
   ;;
   
-  let compute_clause_weight = assert false (*
-    let factor = 2 in
-    match o with
-      | Terms.Lt -> 
-  	let w, m = (weight_of_term 
-  	       ~consider_metas:true ~count_metas_occurrences:false right) in
-  	  w + (factor * (List.length m)) ;
-      | Terms.Le -> assert false
-      | Terms.Gt -> 
-  	let w, m = (weight_of_term 
-  	       ~consider_metas:true ~count_metas_occurrences:false left) in
-  	  w + (factor * (List.length m)) ;
-    | Terms.Ge -> assert false
-    | Terms.Eq 
-    | Terms.Incomparable -> 
-        let w1, m1 = (weight_of_term 
-  	       ~consider_metas:true ~count_metas_occurrences:false right) in
-        let w2, m2 = (weight_of_term 
-  	       ~consider_metas:true ~count_metas_occurrences:false left) in
-        w1 + w2 + (factor * (List.length m1)) + (factor * (List.length m2))
-  *)
+  let compute_unit_clause_weight = 
+    let weight_of_polynomial w m =
+      let factor = 2 in      
+      w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
+    in
+    function
+    | 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.Gt) ->
+        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) ->
+        let wl, ml = weight_of_term l in 
+        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
@@ -118,7 +117,7 @@ module Orderings (B : Terms.Blob) = struct
   ;;
   
   (* Riazanov: 3.1.5 pag 38 *)
-  (* TODO: optimize early detection of Terms.Incomparable case *)
+  (* TODO: optimize early detection of XINCOMPARABLE case *)
   let compare_weights (h1, w1) (h2, w2) =
     let res, diffs =
       try
@@ -138,107 +137,113 @@ module Orderings (B : Terms.Blob) = struct
     let hdiff = h1 - h2 in 
     match res with
     | (0, _, 0) ->
-        if hdiff < 0 then Terms.Lt
-        else if hdiff > 0 then Terms.Gt
-        else Terms.Eq 
+        if hdiff < 0 then XLT
+        else if hdiff > 0 then XGT
+        else XEQ 
     | (m, _, 0) ->
-        if hdiff <= 0 then Terms.Lt
-        else if (- diffs) >= hdiff then Terms.Le else Terms.Incomparable
+        if hdiff <= 0 then XLT
+        else if (- diffs) >= hdiff then XLE else XINCOMPARABLE
     | (0, _, m) ->
-        if hdiff >= 0 then Terms.Gt
-        else if diffs >= (- hdiff) then Terms.Ge else Terms.Incomparable
-    | (m, _, n) when m > 0 && n > 0 -> Terms.Incomparable
+        if hdiff >= 0 then XGT
+        else if diffs >= (- hdiff) then XGE else XINCOMPARABLE
+    | (m, _, n) when m > 0 && n > 0 -> XINCOMPARABLE
     | _ -> assert false 
   ;;
   
-  
-  let rec aux_ordering t1 t2 =
+  (* 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
+    (* 1. *)
     | Terms.Var _, _
-    | _, Terms.Var _ -> Terms.Incomparable
-  
+    | _, Terms.Var _ -> XINCOMPARABLE
+    (* 2.a *)
     | Terms.Leaf a1, Terms.Leaf a2 -> 
-        let cmp = Pervasives.compare a1 a2 in
-        if cmp = 0 then Terms.Eq else if cmp < 0 then Terms.Lt else Terms.Gt
-  
-    | Terms.Leaf _, Terms.Node _ -> Terms.Lt
-    | Terms.Node _, Terms.Leaf _ -> Terms.Gt
-  
+        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
-          | [], [] -> Terms.Eq
-          | _, [] -> Terms.Gt
-          | [], _ -> Terms.Lt
+          | [], [] -> XEQ
+          | _, [] -> XGT
+          | [], _ -> XLT
           | hd1::tl1, hd2::tl2 ->
-              let o = aux_ordering hd1 hd2 in
-              if o = Terms.Eq then cmp tl1 tl2
-              else o
+              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
   ;;
   
+  (* Riazanov: p. 40, relation >_n *)
   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
-    | Terms.Le -> if aux_ordering t1 t2 = Terms.Lt then Terms.Lt else Terms.Incomparable
-    | Terms.Ge -> if aux_ordering t1 t2 = Terms.Gt then Terms.Gt else Terms.Incomparable
-    | Terms.Eq -> aux_ordering t1 t2
+    | XLE ->  (* this is .> *)
+        if aux_ordering t1 t2 = XLT then XLT else XINCOMPARABLE
+    | XGE -> 
+        if aux_ordering t1 t2 = XGT then XGT else XINCOMPARABLE
+    | XEQ -> aux_ordering t1 t2
     | res -> res
   ;;
   
-  (*
+  (* Riazanov: p. 38, relation > *)
   let rec kbo t1 t2 =
-    let aux = aux_ordering ~recursion:false in
-    let w1 = weight_of_term t1
-    and w2 = weight_of_term t2 in
+    let aux = aux_ordering ~head_only:true in
     let rec cmp t1 t2 =
       match t1, t2 with
-      | [], [] -> Terms.Eq
-      | _, [] -> Terms.Gt
-      | [], _ -> Terms.Lt
+      | [], [] -> XEQ
+      | _, [] -> XGT
+      | [], _ -> XLT
       | hd1::tl1, hd2::tl2 ->
-          let o =
-            kbo hd1 hd2
-          in
-          if o = Terms.Eq then cmp tl1 tl2
+          let o = kbo hd1 hd2 in
+          if o = XEQ then cmp tl1 tl2
           else o
     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
-    | Terms.Le ->
+    | XLE ->
         let r = aux t1 t2 in
-        if r = Terms.Lt then Terms.Lt
-        else if r = Terms.Eq then (
+        if r = XLT then XLT
+        else if r = XEQ then (
           match t1, t2 with
-          | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
-              if cmp tl1 tl2 = Terms.Lt then Terms.Lt else Terms.Incomparable
-          | _, _ ->  Terms.Incomparable
-        ) else Terms.Incomparable
-    | Terms.Ge ->
+          | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
+              if cmp tl1 tl2 = XLT then XLT else XINCOMPARABLE
+          | _, _ -> assert false
+        ) else XINCOMPARABLE
+    | XGE ->
         let r = aux t1 t2 in
-        if r = Terms.Gt then Terms.Gt
-        else if r = Terms.Eq then (
+        if r = XGT then XGT
+        else if r = XEQ then (
           match t1, t2 with
-          | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
-              if cmp tl1 tl2 = Terms.Gt then Terms.Gt else Terms.Incomparable
-          | _, _ ->  Terms.Incomparable
-        ) else Terms.Incomparable
-    | Terms.Eq ->
+          | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
+              if cmp tl1 tl2 = XGT then XGT else XINCOMPARABLE
+          | _, _ ->  assert false
+        ) else XINCOMPARABLE
+    | XEQ ->
         let r = aux t1 t2 in
-        if r = Terms.Eq then (
+        if r = XEQ then (
           match t1, t2 with
-          | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
-              cmp tl1 tl2
-          | _, _ ->  Terms.Incomparable
+          | Terms.Node (_::tl1), Terms.Node (_::tl2) -> cmp tl1 tl2
+          | _, _ ->  XINCOMPARABLE
         ) else r 
     | res -> res
   ;;
-  *)
             
-  let compare_terms = nonrec_kbo;; 
+  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
+  ;; 
 
 end
diff --git a/helm/software/components/ng_paramodulation/orderings.mli b/helm/software/components/ng_paramodulation/orderings.mli
index 74989c3eb..c7f67aa09 100644
--- a/helm/software/components/ng_paramodulation/orderings.mli
+++ b/helm/software/components/ng_paramodulation/orderings.mli
@@ -17,6 +17,8 @@ module Orderings (B : Terms.Blob) :
     (* This order relation should be:
      * - stable for instantiation
      * - total on ground terms
+     *
+     * The output can range only on Eq, Lt, Gt, Incomparable
      *)
     val compare_terms : 
           B.t Terms.foterm -> B.t Terms.foterm -> Terms.comparison
diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml
index 8fad7187b..72e32987a 100644
--- a/helm/software/components/ng_paramodulation/terms.ml
+++ b/helm/software/components/ng_paramodulation/terms.ml
@@ -18,7 +18,7 @@ type 'a foterm =
 
 type 'a substitution = (int * 'a foterm) list
 
-type comparison = Lt | Le | Eq | Ge | Gt | Incomparable
+type comparison = Lt | Eq | Gt | Incomparable
 
 type rule = SuperpositionRight | SuperpositionLeft | Demodulation
 type direction = Left2Right | Right2Left | Nodir
diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli
index f5aaa619f..02e3a8b66 100644
--- a/helm/software/components/ng_paramodulation/terms.mli
+++ b/helm/software/components/ng_paramodulation/terms.mli
@@ -18,7 +18,7 @@ type 'a foterm =
 
 type 'a substitution = (int * 'a foterm) list
 
-type comparison = Lt | Le | Eq | Ge | Gt | Incomparable
+type comparison = Lt | Eq | Gt | Incomparable
 
 type rule = SuperpositionRight | SuperpositionLeft | Demodulation
 type direction = Left2Right | Right2Left | Nodir