From 20ea4afc703668c1c643aaf81d62aeae51be36a1 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 19 Dec 2005 16:03:29 +0000 Subject: [PATCH] moved term indexing (in both discrimination and path tree forms) from paramodulation/ to cic/ --- helm/ocaml/cic/.depend | 3 + helm/ocaml/cic/Makefile | 3 +- helm/ocaml/cic/discrimination_tree.ml | 3 +- helm/ocaml/cic/discrimination_tree.mli | 10 +- .../{paramodulation => cic}/path_indexing.ml | 156 ++++++------------ helm/ocaml/cic/path_indexing.mli | 42 +++++ helm/ocaml/paramodulation/.depend | 9 +- helm/ocaml/paramodulation/Makefile | 4 +- .../ocaml/paramodulation/equality_indexing.ml | 129 +++++++++++++++ .../paramodulation/equality_indexing.mli | 43 +++++ helm/ocaml/paramodulation/indexing.ml | 123 ++------------ helm/ocaml/paramodulation/saturation.ml | 23 ++- 12 files changed, 300 insertions(+), 248 deletions(-) rename helm/ocaml/{paramodulation => cic}/path_indexing.ml (58%) create mode 100644 helm/ocaml/cic/path_indexing.mli create mode 100644 helm/ocaml/paramodulation/equality_indexing.ml create mode 100644 helm/ocaml/paramodulation/equality_indexing.mli diff --git a/helm/ocaml/cic/.depend b/helm/ocaml/cic/.depend index 58a8c3bed..a35156331 100644 --- a/helm/ocaml/cic/.depend +++ b/helm/ocaml/cic/.depend @@ -4,6 +4,7 @@ cicParser.cmi: cic.cmo cicUtil.cmi: cic.cmo helmLibraryObjects.cmi: cic.cmo discrimination_tree.cmi: cic.cmo +path_indexing.cmi: cic.cmo cic.cmo: cicUniv.cmi cic.cmx: cicUniv.cmx unshare.cmo: cic.cmo unshare.cmi @@ -22,3 +23,5 @@ libraryObjects.cmo: helmLibraryObjects.cmi libraryObjects.cmi libraryObjects.cmx: helmLibraryObjects.cmx libraryObjects.cmi discrimination_tree.cmo: cic.cmo discrimination_tree.cmi discrimination_tree.cmx: cic.cmx discrimination_tree.cmi +path_indexing.cmo: cic.cmo path_indexing.cmi +path_indexing.cmx: cic.cmx path_indexing.cmi diff --git a/helm/ocaml/cic/Makefile b/helm/ocaml/cic/Makefile index a0cfe0daa..4e36af019 100644 --- a/helm/ocaml/cic/Makefile +++ b/helm/ocaml/cic/Makefile @@ -9,7 +9,8 @@ INTERFACE_FILES = \ cicUtil.mli \ helmLibraryObjects.mli \ libraryObjects.mli \ - discrimination_tree.mli + discrimination_tree.mli \ + path_indexing.mli IMPLEMENTATION_FILES = \ cic.ml $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = cic.ml cic.cmi diff --git a/helm/ocaml/cic/discrimination_tree.ml b/helm/ocaml/cic/discrimination_tree.ml index fd234df98..6e2529016 100644 --- a/helm/ocaml/cic/discrimination_tree.ml +++ b/helm/ocaml/cic/discrimination_tree.ml @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) -module DiscriminationTreeIndexing = +module DiscriminationTreeIndexing = functor (A:Set.S) -> struct @@ -59,7 +59,6 @@ module DiscriminationTreeIndexing = module DiscriminationTree = Trie.Make(PSMap);; type t = A.t DiscriminationTree.t - type elt = A.elt let empty = DiscriminationTree.empty (* diff --git a/helm/ocaml/cic/discrimination_tree.mli b/helm/ocaml/cic/discrimination_tree.mli index 5c5e6f05d..61631f478 100644 --- a/helm/ocaml/cic/discrimination_tree.mli +++ b/helm/ocaml/cic/discrimination_tree.mli @@ -26,20 +26,16 @@ module DiscriminationTreeIndexing : functor (A : Set.S) -> sig - type path_string_elem = Cic.term - type path_string = path_string_elem list val arities : (Cic.term, int) Hashtbl.t - val path_string_of_term : Cic.term -> Cic.term list type key = Cic.term type t - type elt = A.elt val empty : t - val index : t -> Cic.term -> A.elt -> t - val remove_index : t -> Cic.term -> A.elt -> t - val in_index : t -> Cic.term -> (A.elt -> bool) -> bool + val index : t -> key -> A.elt -> t + val remove_index : t -> key -> A.elt -> t + val in_index : t -> key -> (A.elt -> bool) -> bool val retrieve_generalizations : t -> key -> A.t val retrieve_unifiables : t -> key -> A.t end diff --git a/helm/ocaml/paramodulation/path_indexing.ml b/helm/ocaml/cic/path_indexing.ml similarity index 58% rename from helm/ocaml/paramodulation/path_indexing.ml rename to helm/ocaml/cic/path_indexing.ml index 06da404ab..81c3583e1 100644 --- a/helm/ocaml/paramodulation/path_indexing.ml +++ b/helm/ocaml/cic/path_indexing.ml @@ -26,6 +26,11 @@ (* path indexing implementation *) (* position of the subterm, subterm (Appl are not stored...) *) + +module PathIndexing = + functor(A:Set.S) -> + struct + type path_string_elem = Index of int | Term of Cic.term;; type path_string = path_string_elem list;; @@ -46,7 +51,7 @@ let rec path_strings_of_term index = | term -> [ [Index index; Term term] ] ;; - +(* let string_of_path_string ps = String.concat "." (List.map @@ -59,7 +64,7 @@ let string_of_path_string ps = "(" ^ s ^ ")") ps) ;; - +*) module OrderedPathStringElement = struct type t = path_string_elem @@ -74,72 +79,44 @@ end module PSMap = Map.Make(OrderedPathStringElement);; -module OrderedPosEquality = struct - type t = Utils.pos * Inference.equality - - let compare = Pervasives.compare -end - -module PosEqSet = Set.Make(OrderedPosEquality);; - - module PSTrie = Trie.Make(PSMap);; - -let 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 index pos trie ps = - let ps_set = try PSTrie.find ps trie with Not_found -> PosEqSet.empty in - let trie = PSTrie.add ps (PosEqSet.add (pos, equality) ps_set) trie in - trie - in - match ordering with - | Utils.Gt -> List.fold_left (index Utils.Left) trie psl - | Utils.Lt -> List.fold_left (index Utils.Right) trie psr - | _ -> - let trie = List.fold_left (index Utils.Left) trie psl in - List.fold_left (index Utils.Right) trie psr -;; - - -let remove_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 remove_index pos trie ps = - try - let ps_set = PosEqSet.remove (pos, equality) (PSTrie.find ps trie) in - if PosEqSet.is_empty ps_set then - PSTrie.remove ps trie - else - PSTrie.add ps ps_set trie - with Not_found -> - trie - in - match ordering with - | Utils.Gt -> List.fold_left (remove_index Utils.Left) trie psl - | Utils.Lt -> List.fold_left (remove_index Utils.Right) trie psr - | _ -> - let trie = List.fold_left (remove_index Utils.Left) trie psl in - List.fold_left (remove_index Utils.Right) trie psr +type t = A.t PSTrie.t +type key = Cic.term +let empty = PSTrie.empty +let arities = Hashtbl.create 0 + +let index trie term info = + let ps = path_strings_of_term 0 term in + List.fold_left + (fun trie ps -> + let ps_set = try PSTrie.find ps trie with Not_found -> A.empty in + let trie = PSTrie.add ps (A.add info ps_set) trie in + trie) trie ps + +let remove_index trie term info= + let ps = path_strings_of_term 0 term in + List.fold_left + (fun trie ps -> + try + let ps_set = A.remove info (PSTrie.find ps trie) in + if A.is_empty ps_set then + PSTrie.remove ps trie + else + PSTrie.add ps ps_set trie + with Not_found -> trie) trie ps ;; - -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 in_index trie term test = + let ps = path_strings_of_term 0 term in let ok ps = try let set = PSTrie.find ps trie in - PosEqSet.exists (fun (p, e) -> meta_convertibility e) set + A.exists test set with Not_found -> false in - (List.exists ok psl) || (List.exists ok psr) + List.exists ok ps ;; @@ -165,7 +142,7 @@ let rec retrieve_generalizations trie term = | PSTrie.Node (value, map) -> let res = match term with - | Cic.Meta _ -> PosEqSet.empty + | Cic.Meta _ -> A.empty | term -> let hd_term = head_of_term term in try @@ -186,15 +163,15 @@ let rec retrieve_generalizations trie term = in match l with | hd::tl -> - List.fold_left (fun r s -> PosEqSet.inter r s) hd tl - | _ -> PosEqSet.empty + List.fold_left (fun r s -> A.inter r s) hd tl + | _ -> A.empty with Not_found -> - PosEqSet.empty + A.empty in try let n = PSMap.find (Term (Cic.Implicit None)) map in match n with - | PSTrie.Node (Some s, _) -> PosEqSet.union res s + | PSTrie.Node (Some s, _) -> A.union res s | _ -> res with Not_found -> res @@ -208,9 +185,9 @@ let rec retrieve_unifiables trie term = match term with | Cic.Meta _ -> PSTrie.fold - (fun ps v res -> PosEqSet.union res v) + (fun ps v res -> A.union res v) (PSTrie.Node (None, map)) - PosEqSet.empty + A.empty | _ -> let hd_term = head_of_term term in try @@ -231,57 +208,18 @@ let rec retrieve_unifiables trie term = in match l with | hd::tl -> - List.fold_left (fun r s -> PosEqSet.inter r s) hd tl - | _ -> PosEqSet.empty + List.fold_left (fun r s -> A.inter r s) hd tl + | _ -> A.empty with Not_found -> - PosEqSet.empty + A.empty in try let n = PSMap.find (Term (Cic.Implicit None)) map in match n with - | PSTrie.Node (Some s, _) -> PosEqSet.union res s + | PSTrie.Node (Some s, _) -> A.union res s | _ -> res with Not_found -> res ;; - -let retrieve_all trie term = - PSTrie.fold - (fun k v s -> PosEqSet.union v s) trie PosEqSet.empty -;; - - -let string_of_pstrie trie = - let rec to_string level = function - | PSTrie.Node (v, map) -> - let s = - match v with - | Some v -> - (String.make (2 * level) ' ') ^ - "{" ^ (String.concat "; " - (List.map - (fun (p, e) -> - "(" ^ (Utils.string_of_pos p) ^ ", " ^ - (Inference.string_of_equality e) ^ ")") - (PosEqSet.elements v))) ^ "}" - | None -> "" - in - let rest = - String.concat "\n" - (PSMap.fold - (fun k v s -> - let ks = - match k with - | Index i -> "Index " ^ (string_of_int i) - | Term t -> "Term " ^ (CicPp.ppterm t) - in - let rs = to_string (level+1) v in - ((String.make (2 * level) ' ') ^ ks ^ "\n" ^ rs)::s) - map []) - in - s ^ rest - in - to_string 0 trie -;; - +end diff --git a/helm/ocaml/cic/path_indexing.mli b/helm/ocaml/cic/path_indexing.mli new file mode 100644 index 000000000..899901618 --- /dev/null +++ b/helm/ocaml/cic/path_indexing.mli @@ -0,0 +1,42 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +module PathIndexing : + functor (A : Set.S) -> + sig + val arities : (Cic.term, int) Hashtbl.t + + type key = Cic.term + type t + + val empty : t + val index : t -> key -> A.elt -> t + val remove_index : t -> key -> A.elt -> t + val in_index : t -> key -> (A.elt -> bool) -> bool + val retrieve_generalizations : t -> key -> A.t + val retrieve_unifiables : t -> key -> A.t + end + + diff --git a/helm/ocaml/paramodulation/.depend b/helm/ocaml/paramodulation/.depend index ec3ba7d6c..7c6673bad 100644 --- a/helm/ocaml/paramodulation/.depend +++ b/helm/ocaml/paramodulation/.depend @@ -1,11 +1,12 @@ inference.cmi: utils.cmi +equality_indexing.cmi: utils.cmi inference.cmi utils.cmo: utils.cmi utils.cmx: utils.cmi inference.cmo: utils.cmi inference.cmi inference.cmx: utils.cmx inference.cmi -path_indexing.cmo: utils.cmi inference.cmi -path_indexing.cmx: utils.cmx inference.cmx -indexing.cmo: utils.cmi inference.cmi -indexing.cmx: utils.cmx inference.cmx +equality_indexing.cmo: utils.cmi inference.cmi equality_indexing.cmi +equality_indexing.cmx: utils.cmx inference.cmx equality_indexing.cmi +indexing.cmo: utils.cmi inference.cmi equality_indexing.cmi +indexing.cmx: utils.cmx inference.cmx equality_indexing.cmx saturation.cmo: utils.cmi inference.cmi indexing.cmo saturation.cmx: utils.cmx inference.cmx indexing.cmx diff --git a/helm/ocaml/paramodulation/Makefile b/helm/ocaml/paramodulation/Makefile index 683bac671..854621090 100644 --- a/helm/ocaml/paramodulation/Makefile +++ b/helm/ocaml/paramodulation/Makefile @@ -2,10 +2,10 @@ PACKAGE = paramodulation INTERFACE_FILES = \ utils.mli \ - inference.mli + inference.mli\ + equality_indexing.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) \ - path_indexing.ml \ indexing.ml \ saturation.ml diff --git a/helm/ocaml/paramodulation/equality_indexing.ml b/helm/ocaml/paramodulation/equality_indexing.ml new file mode 100644 index 000000000..fd3fa5c32 --- /dev/null +++ b/helm/ocaml/paramodulation/equality_indexing.ml @@ -0,0 +1,129 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +module type EqualityIndex = + sig + module PosEqSet : Set.S with type elt = Utils.pos * Inference.equality + val arities : (Cic.term, int) Hashtbl.t + type key = Cic.term + type t = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet).t + val empty : t + val retrieve_generalizations : t -> key -> PosEqSet.t + val retrieve_unifiables : t -> key -> PosEqSet.t + val init_index : unit -> unit + val remove_index : t -> Inference.equality -> t + val index : t -> Inference.equality -> t + val in_index : t -> Inference.equality -> bool + end + +module DT = +struct + module OrderedPosEquality = struct + type t = Utils.pos * Inference.equality + let compare = Pervasives.compare + end + + module PosEqSet = Set.Make(OrderedPosEquality);; + + include Discrimination_tree.DiscriminationTreeIndexing(PosEqSet) + + + (* DISCRIMINATION TREES *) + let init_index () = + Hashtbl.clear arities; + ;; + + let remove_index tree equality = + let _, _, (_, l, r, ordering), _, _ = equality in + match ordering with + | Utils.Gt -> remove_index tree l (Utils.Left, equality) + | Utils.Lt -> remove_index tree r (Utils.Right, equality) + | _ -> + let tree = remove_index tree r (Utils.Right, equality) in + remove_index tree l (Utils.Left, equality) + + let index tree equality = + let _, _, (_, l, r, ordering), _, _ = equality in + match ordering with + | Utils.Gt -> index tree l (Utils.Left, equality) + | Utils.Lt -> index tree r (Utils.Right, equality) + | _ -> + let tree = index tree r (Utils.Right, equality) in + 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 + in_index tree l meta_convertibility || in_index tree r meta_convertibility + + end + +module PT = + struct + module OrderedPosEquality = struct + type t = Utils.pos * Inference.equality + let compare = Pervasives.compare + end + + module PosEqSet = Set.Make(OrderedPosEquality);; + + include Discrimination_tree.DiscriminationTreeIndexing(PosEqSet) + + + (* DISCRIMINATION TREES *) + let init_index () = + Hashtbl.clear arities; + ;; + + let remove_index tree equality = + let _, _, (_, l, r, ordering), _, _ = equality in + match ordering with + | Utils.Gt -> remove_index tree l (Utils.Left, equality) + | Utils.Lt -> remove_index tree r (Utils.Right, equality) + | _ -> + let tree = remove_index tree r (Utils.Right, equality) in + remove_index tree l (Utils.Left, equality) + + let index tree equality = + let _, _, (_, l, r, ordering), _, _ = equality in + match ordering with + | Utils.Gt -> index tree l (Utils.Left, equality) + | Utils.Lt -> index tree r (Utils.Right, equality) + | _ -> + let tree = index tree r (Utils.Right, equality) in + 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 + in_index tree l meta_convertibility || in_index tree r meta_convertibility +end + diff --git a/helm/ocaml/paramodulation/equality_indexing.mli b/helm/ocaml/paramodulation/equality_indexing.mli new file mode 100644 index 000000000..d7c3bec5e --- /dev/null +++ b/helm/ocaml/paramodulation/equality_indexing.mli @@ -0,0 +1,43 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +module type EqualityIndex = + sig + module PosEqSet : Set.S with type elt = Utils.pos * Inference.equality + val arities : (Cic.term, int) Hashtbl.t + type key = Cic.term + type t = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet).t + val empty : t + val retrieve_generalizations : t -> key -> PosEqSet.t + val retrieve_unifiables : t -> key -> PosEqSet.t + val init_index : unit -> unit + val remove_index : t -> Inference.equality -> t + val index : t -> Inference.equality -> t + val in_index : t -> Inference.equality -> bool + end + +module DT : EqualityIndex +module PT : EqualityIndex + diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index 8c4137556..523cff882 100644 --- 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); *) diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 2e7f1f21a..bef39f7b2 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -221,8 +221,7 @@ let make_passive neg pos = List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities in let table = - List.fold_left (fun tbl e -> Indexing.index tbl e) - (Indexing.empty_table ()) pos + List.fold_left (fun tbl e -> Indexing.index tbl e) Indexing.empty pos in (neg, set_of neg), (pos, set_of pos), @@ -231,7 +230,7 @@ let make_passive neg pos = let make_active () = - [], Indexing.empty_table () + [], Indexing.empty ;; @@ -364,7 +363,7 @@ let prune_passive howmany (active, _) passive = maximal_retained_equality := Some (EqualitySet.max_elt ps); let tbl = EqualitySet.fold - (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) + (fun e tbl -> Indexing.index tbl e) ps Indexing.empty in (nl, ns), (pl, ps), tbl ;; @@ -398,7 +397,7 @@ let infer env sign current (active_list, active_table) = let neg, pos = infer_positive table tl in neg, res @ pos in - let curr_table = Indexing.index (Indexing.empty_table ()) current in + let curr_table = Indexing.index Indexing.empty current in let neg, pos = infer_positive curr_table active_list in neg, res @ pos in @@ -655,7 +654,7 @@ let backward_simplify_active env new_pos new_table min_weight active = ) else (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq) - active_list ([], Indexing.empty_table ()), + active_list ([], Indexing.empty), List.fold_right (fun (s, eq) (n, p) -> if (s <> Negative) && (is_identity env eq) then ( @@ -692,7 +691,7 @@ let backward_simplify_passive env new_pos new_table min_weight passive = and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in let passive_table = List.fold_left - (fun tbl e -> Indexing.index tbl e) (Indexing.empty_table ()) pl + (fun tbl e -> Indexing.index tbl e) Indexing.empty pl in match newn, newp with | [], [] -> ((nl, ns), (pl, ps), passive_table), None @@ -706,7 +705,7 @@ let backward_simplify env new' ?passive active = (fun (l, t, w) e -> let ew, _, _, _, _ = e in (Positive, e)::l, Indexing.index t e, min ew w) - ([], Indexing.empty_table (), 1000000) (snd new') + ([], Indexing.empty, 1000000) (snd new') in let active, newa = backward_simplify_active env new_pos new_table min_weight active in @@ -1843,7 +1842,7 @@ let main dbd full term metasenv ugraph = let tbl = List.fold_left (fun t (_, e) -> Indexing.index t e) - (Indexing.empty_table ()) active + Indexing.empty active in let res = forward_simplify env e (active, tbl) in match others with @@ -2020,7 +2019,7 @@ let saturate let tbl = List.fold_left (fun t (_, e) -> Indexing.index t e) - (Indexing.empty_table ()) active + Indexing.empty active in let res = forward_simplify env e (active, tbl) in match others with @@ -2215,7 +2214,7 @@ let retrieve_and_print dbd term metasenv ugraph = let tbl = List.fold_left (fun t (_, e) -> Indexing.index t e) - (Indexing.empty_table ()) active + Indexing.empty active in let res = forward_simplify env (Positive, e) (active, tbl) in match others with @@ -2301,7 +2300,7 @@ let main_demod_equalities dbd term metasenv ugraph = let tbl = List.fold_left (fun t (_, e) -> Indexing.index t e) - (Indexing.empty_table ()) active + Indexing.empty active in let res = forward_simplify env e (active, tbl) in match others with -- 2.39.2