-(*
-(* 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
-