some optimizations...

[helm.git] / helm / ocaml / paramodulation / path_indexing.ml

diff --git a/helm/ocaml/paramodulation/path_indexing.ml b/helm/ocaml/paramodulation/path_indexing.ml
index 87e917fff79b5c176401225a1cc757f20f64967c..bc9bc01f1608fa42d36c369a57808496364a6b08 100644 (file)
--- a/helm/ocaml/paramodulation/path_indexing.ml
+++ b/helm/ocaml/paramodulation/path_indexing.ml
@@ -160,6 +160,22 @@ let remove_index trie equality =
 ;;
 
 
+let in_index trie equality =
+  let _, (_, l, r, ordering), _, _ = equality in
+  let psl = path_strings_of_term 0 l
+  and psr = path_strings_of_term 0 r in
+  let meta_convertibility = Inference.meta_convertibility_eq equality in
+  let ok ps =
+    try
+      let set = PSTrie.find ps trie in
+      PosEqSet.exists (fun (p, e) -> meta_convertibility e) set
+    with Not_found ->
+      false
+  in
+  (List.exists ok psl) || (List.exists ok psr)
+;;
+
+
 let head_of_term = function
   | Cic.Appl (hd::tl) -> hd
   | term -> term