X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_paramodulation%2Forderings.ml;h=d24a5742eeed196035d3c97c9f181e6ab0d35054;hb=578ba04e1a0812f538729fbc02ea38d2cfd0ed3e;hp=2613efefd1044fd9fee7a067711346c9201ccd1d;hpb=3d5b3358654105803ee99b99f02d87314741a4fa;p=helm.git

diff --git a/matita/components/ng_paramodulation/orderings.ml b/matita/components/ng_paramodulation/orderings.ml
index 2613efefd..d24a5742e 100644
--- a/matita/components/ng_paramodulation/orderings.ml
+++ b/matita/components/ng_paramodulation/orderings.ml
@@ -363,10 +363,16 @@ module LPO (B : Terms.Blob) = struct
   let compute_unit_clause_weight = compute_unit_clause_weight;;
   let compute_goal_weight = compute_goal_weight;;
 
+  (*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
       | _, Terms.Var _ -> false
       | Terms.Var i,_ ->
@@ -376,6 +382,8 @@ module LPO (B : Terms.Blob) = struct
       | 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) ->
           if List.exists (lpo_le s) tl2 then true
           else
@@ -395,85 +403,23 @@ module LPO (B : Terms.Blob) = struct
                     else false
                 in 
                 compare_args tl1 tl2
+            | _ -> assert false
            end
+   in
+    Hashtbl.add cache (s,t) res; res
   ;;
 
-  let new_lpo s t =
+  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 rec lpo s t =
-    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 i,_ ->
-          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 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
-            
-  ;;
-  
-  let lpo s t = new_lpo s t 
-(* 
-      if res = lpo s t then res
-      else assert false *)
-
   let compare_terms = compare_terms lpo;;
 
   let profiler = HExtlib.profile ~enable:true "compare_terms(lpo)";;