X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_paramodulation%2Forderings.ml;h=d5f35a3a321c16929177d4af525239dfcac334dc;hb=74c6905907b0bca229366d52450e2a6982b5b8be;hp=f7062b3abebbe2b4d95956ec6f024fd4b46dcb07;hpb=2e6a92bad35a8f8883c498c6a2f36ea3208d4ddd;p=helm.git

diff --git a/matita/components/ng_paramodulation/orderings.ml b/matita/components/ng_paramodulation/orderings.ml
index f7062b3ab..d5f35a3a3 100644
--- a/matita/components/ng_paramodulation/orderings.ml
+++ b/matita/components/ng_paramodulation/orderings.ml
@@ -131,8 +131,8 @@ let compare_weights (h1, w1) (h2, w2) =
           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
+            let lt = lt || (r < 0) in
+            let gt = gt || (r > 0) in
               if lt && gt then XINCOMPARABLE else
                 aux hdiff (lt, gt) diffs tl1 tl2
           else if var1 < var2 then
@@ -208,7 +208,7 @@ module NRKBO (B : Terms.Blob) = struct
   let name = "nrkbo"
   include B 
 
-  module Pp = Pp.Pp(B)
+  (*module Pp = Pp.Pp(B)*)
 
   let eq_foterm = eq_foterm B.eq;;
 
@@ -224,7 +224,7 @@ exception UnificationFailure of string Lazy.t;;
       in
       match s, t with
         | s, t when eq_foterm s t -> subst
-        | Terms.Var i, Terms.Var j
+        | 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
@@ -290,7 +290,7 @@ module KBO (B : Terms.Blob) = struct
   let name = "kbo"
   include B 
 
-  module Pp = Pp.Pp(B)
+  (*module Pp = Pp.Pp(B)*)
 
   let eq_foterm = eq_foterm B.eq;;
 
@@ -356,75 +356,69 @@ module LPO (B : Terms.Blob) = struct
   let name = "lpo"
   include B 
 
-  module Pp = Pp.Pp(B)
+  (*module Pp = Pp.Pp(B)*)
 
   let eq_foterm = eq_foterm B.eq;;
 
   let compute_unit_clause_weight = compute_unit_clause_weight;;
   let compute_goal_weight = compute_goal_weight;;
 
-  let rec lpo s t =
+  (*CSC: beware! Imperative cache! *)
+  let cache = Hashtbl.create 101
+
+  let rec lpo_le s t = 
+    eq_foterm s t || lpo_lt s t 
+  
+  and lpo_lt s t =
+    try Hashtbl.find cache (s,t)
+    with
+    Not_found -> let res =
     match s,t with
-      | s, t when eq_foterm 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 _ -> false
       | 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 true
+          else false
+      | Terms.Leaf a, Terms.Leaf b -> B.compare a b < 0
+      | Terms.Leaf _, Terms.Node _  -> true (* we assume unary constants 
+                            are smaller than constants with higher arity *)
+      | Terms.Node _, Terms.Leaf _ -> false
+      | Terms.Node [],_
+      | _,Terms.Node [] -> assert false
       | 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 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 -> 
-                     (try
-                      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)   
-                      with Invalid_argument _ -> (* assert false *)
-                              XINCOMPARABLE)
-              | XINCOMPARABLE -> XINCOMPARABLE
-              | _ -> assert false
-          end
-      | _,_ -> aux_ordering B.compare s t
-            
+          if List.exists (lpo_le s) tl2 then true
+          else
+          begin 
+            match aux_ordering B.compare hd1 hd2 with
+            | XINCOMPARABLE 
+            | XGT -> false
+            | XLT -> List.for_all (fun x -> lpo_lt x t) tl1
+            | XEQ -> 
+                let rec compare_args l1 l2 =
+                match l1,l2 with
+                | [],_ 
+                | _,[] -> false
+                | a1::tl1,a2::tl2 -> 
+                    if eq_foterm a1 a2 then compare_args tl1 tl2
+                    else if lpo_lt a1 a2 then List.for_all (fun x -> lpo_lt x t) tl1
+                    else false
+                in 
+                compare_args tl1 tl2
+            | _ -> assert false
+           end
+   in
+    Hashtbl.add cache (s,t) res; res
+  ;;
+
+  let lpo s t =
+    let res =
+    if eq_foterm s t then XEQ
+    else if lpo_lt s t then XLT
+    else if lpo_lt t s then XGT
+    else XINCOMPARABLE
+    in
+     Hashtbl.clear cache; res
   ;;
+    
 
   let compare_terms = compare_terms lpo;;