moved term indexing (in both discrimination and path tree forms) from paramodulation...

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

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 8c41375565652266966189d1d068d7b3bba437c2..523cff88233def6f9d30ef2ca304458300386bb0 100644 (file)
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -23,21 +23,16 @@
  * http://cs.unibo.it/helm/.
  *)
 
-module OrderedPosEquality = struct
-       type t = Utils.pos * Inference.equality
-       let compare = Pervasives.compare
-      end
-
-module PosEqSet = Set.Make(OrderedPosEquality);;
-
-module DT = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet);;
+module Index = Equality_indexing.DT (* discrimination tree based indexing *)
+(*
+module Index = Equality_indexing.DT (* path tree based indexing *)
+*)
 
 let debug_print = Utils.debug_print;;
 
 
 type retrieval_mode = Matching | Unification;;
 
-
 let print_candidates mode term res =
   let _ =
     match mode with
@@ -62,105 +57,11 @@ let indexing_retrieval_time = ref 0.;;
 
 let apply_subst = CicMetaSubst.apply_subst
 
-(*
-(* NO INDEXING *)
-let init_index () = ()
-  
-let empty_table () = []
-
-let index table equality =
-  let _, _, (_, l, r, ordering), _, _ = equality in
-  match ordering with
-  | Utils.Gt -> (Utils.Left, equality)::table
-  | Utils.Lt -> (Utils.Right, equality)::table
-  | _ -> (Utils.Left, equality)::(Utils.Right, equality)::table
-;;
-
-let remove_index table equality =
-  List.filter (fun (p, e) -> e != equality) table
-;;
-
-let in_index table equality =
-  List.exists (fun (p, e) -> e == equality) table
-;;
-
-let get_candidates mode table term = table
-*)
-
-
-(*
-(* PATH INDEXING *)
-let init_index () = ()
-
-let empty_table () =
-  Path_indexing.PSTrie.empty
-;;
-
-let index = Path_indexing.index
-let remove_index tree equality = 
-  let _, _, (_, l, r, ordering), _, _ = equality in
-  match ordering with
-  | Utils.Gt -> DT.remove_index tree l equality
-  | Utils.Lt -> DT.remove_index tree r equality
-  | _ -> 
-    DT.remove_index (DT.remove_index tree r equality) l equality
-  
-
-let in_index = Path_indexing.in_index;;
-  
-let get_candidates mode trie term =
-  let t1 = Unix.gettimeofday () in
-  let res = 
-    let s = 
-      match mode with
-      | Matching -> Path_indexing.retrieve_generalizations trie term
-      | Unification -> Path_indexing.retrieve_unifiables trie term
-(*       Path_indexing.retrieve_all trie term *)
-    in
-    Path_indexing.PosEqSet.elements s
-  in
-(*   print_candidates mode term res; *)
-  let t2 = Unix.gettimeofday () in
-  indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
-  res
-;;
-*)
-
-(* DISCRIMINATION TREES *)
-let init_index () =
-  Hashtbl.clear DT.arities;
-;;
-
-let empty_table () =
-  DT.empty
-;;
-
-let remove_index tree equality = 
-  let _, _, (_, l, r, ordering), _, _ = equality in
-  match ordering with
-  | Utils.Gt -> DT.remove_index tree l (Utils.Left, equality)
-  | Utils.Lt -> DT.remove_index tree r (Utils.Right, equality)
-  | _ -> 
-    let tree = DT.remove_index tree r (Utils.Right, equality) in
-    DT.remove_index tree l (Utils.Left, equality)
-
-let index tree equality = 
-  let _, _, (_, l, r, ordering), _, _ = equality in
-  match ordering with
-  | Utils.Gt -> DT.index tree l (Utils.Left, equality)
-  | Utils.Lt -> DT.index tree r (Utils.Right, equality)
-  | _ -> 
-    let tree = DT.index tree r (Utils.Right, equality) in
-    DT.index tree l (Utils.Left, equality)
-  
-
-let in_index tree equality = 
-  let _, _, (_, l, r, ordering), _, _ = equality in
-  let meta_convertibility (pos,equality') = 
-    Inference.meta_convertibility_eq equality equality' 
-  in
-  DT.in_index tree l meta_convertibility || DT.in_index tree r meta_convertibility
-
+let index = Index.index
+let remove_index = Index.remove_index
+let in_index = Index.in_index
+let empty = Index.empty 
+let init_index = Index.init_index
 
 (* returns a list of all the equalities in the tree that are in relation
    "mode" with the given term, where mode can be either Matching or
@@ -180,10 +81,10 @@ let get_candidates mode tree term =
   let res =
     let s = 
       match mode with
-      | Matching -> DT.retrieve_generalizations tree term
-      | Unification -> DT.retrieve_unifiables tree term
+      | Matching -> Index.retrieve_generalizations tree term
+      | Unification -> Index.retrieve_unifiables tree term
     in
-    PosEqSet.elements s
+    Index.PosEqSet.elements s
   in
   (*   print_candidates mode term res; *)
 (*   print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)