From 14f5eda52d26967d1704605e6548fd9140450913 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 17 May 2012 11:26:24 +0000
Subject: [PATCH] The lpo cache is now implemented as an hastbl for more
 performance improvement. Probably it would be better with an ad-hoc
 hash-function.

---
 matita/components/ng_paramodulation/orderings.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/matita/components/ng_paramodulation/orderings.ml b/matita/components/ng_paramodulation/orderings.ml
index bf033ec66..d24a5742e 100644
--- a/matita/components/ng_paramodulation/orderings.ml
+++ b/matita/components/ng_paramodulation/orderings.ml
@@ -364,13 +364,13 @@ module LPO (B : Terms.Blob) = struct
   let compute_goal_weight = compute_goal_weight;;
 
   (*CSC: beware! Imperative cache! *)
-  let cache = ref [];;
+  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 List.assoc (s,t) !cache
+    try Hashtbl.find cache (s,t)
     with
     Not_found -> let res =
     match s,t with
@@ -406,7 +406,7 @@ module LPO (B : Terms.Blob) = struct
             | _ -> assert false
            end
    in
-    cache := ((s,t),res)::!cache; res
+    Hashtbl.add cache (s,t) res; res
   ;;
 
   let lpo s t =
@@ -416,7 +416,7 @@ module LPO (B : Terms.Blob) = struct
     else if lpo_lt t s then XGT
     else XINCOMPARABLE
     in
-     cache := []; res
+     Hashtbl.clear cache; res
   ;;
     
 
-- 
2.39.2