From: Alberto Griggio Date: Wed, 22 Jun 2005 09:07:45 +0000 (+0000) Subject: use of discrimination trees instead of path indexes, for a little X-Git-Tag: INDEXING_NO_PROOFS~106 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=969fb8763a6d4afb88aef1eaa4a4d1ce7d626264;p=helm.git use of discrimination trees instead of path indexes, for a little performance gain --- diff --git a/helm/ocaml/paramodulation/Makefile b/helm/ocaml/paramodulation/Makefile index f16094a17..9d30e7020 100644 --- a/helm/ocaml/paramodulation/Makefile +++ b/helm/ocaml/paramodulation/Makefile @@ -27,22 +27,25 @@ opt: saturation.opt INTERFACE_FILES = \ utils.mli \ - inference.mli + inference.mli DEPOBJS = \ $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) \ + trie.ml \ path_indexing.ml \ - indexing.ml \ - saturation.ml \ discrimination_tree.ml \ - test_indexing.ml + test_indexing.ml \ + indexing.ml \ + saturation.ml TOPLEVELOBJS = $(INTERFACE_FILES:%.mli=%.cmo) \ + trie.cmo \ path_indexing.cmo \ discrimination_tree.cmo \ indexing.cmo \ saturation.cmo TESTOBJS = $(INTERFACE_FILES:%.mli=%.cmo) \ + trie.cmo \ path_indexing.cmo \ discrimination_tree.cmo \ test_indexing.cmo diff --git a/helm/ocaml/paramodulation/discrimination_tree.ml b/helm/ocaml/paramodulation/discrimination_tree.ml index 8753782d4..9470e1bde 100644 --- a/helm/ocaml/paramodulation/discrimination_tree.ml +++ b/helm/ocaml/paramodulation/discrimination_tree.ml @@ -16,6 +16,11 @@ let rec path_string_of_term = function ;; +let string_of_path_string ps = + String.concat "." (List.map CicPp.ppterm ps) +;; + + module OrderedPathStringElement = struct type t = path_string_elem @@ -25,9 +30,22 @@ 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 DiscriminationTree = Trie.Make(PSMap);; + + +(* module DiscriminationTree = struct type key = path_string - type t = Node of (Utils.pos * Inference.equality) option * (t PSMap.t) + type t = Node of PosEqSet.t option * (t PSMap.t) let empty = Node (None, PSMap.empty) @@ -56,10 +74,11 @@ module DiscriminationTree = struct let rec remove l t = match (l, t) with | [], Node (_, m) -> Node (None, m) - | x::r, Node (v, m) -> + | x::r, Node (v, m) -> try let t' = remove r (PSMap.find x m) in - Node (v, if t' = empty then PSMap.remove x m else PSMap.add x t' m) + let m' = if t' = empty then PSMap.remove x m else PSMap.add x t' m in + Node (v, m') with Not_found -> t @@ -73,18 +92,55 @@ module DiscriminationTree = struct traverse [] t acc end +*) + +let string_of_discrimination_tree tree = + let rec to_string level = function + | DiscriminationTree.Node (value, map) -> + let s = + match value 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 = CicPp.ppterm k 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 tree +;; let index tree equality = let _, (_, l, r, ordering), _, _ = equality in let psl = path_string_of_term l and psr = path_string_of_term r in + let index pos tree ps = + let ps_set = + try DiscriminationTree.find ps tree with Not_found -> PosEqSet.empty in + let tree = + DiscriminationTree.add ps (PosEqSet.add (pos, equality) ps_set) tree in + tree + in match ordering with - | Utils.Gt -> DiscriminationTree.add psl (Utils.Left, equality) tree - | Utils.Lt -> DiscriminationTree.add psr (Utils.Right, equality) tree + | Utils.Gt -> index Utils.Left tree psl + | Utils.Lt -> index Utils.Right tree psr | _ -> - let tree = DiscriminationTree.add psl (Utils.Left, equality) tree in - DiscriminationTree.add psr (Utils.Right, equality) tree + let tree = index Utils.Left tree psl in + index Utils.Right tree psr ;; @@ -92,12 +148,23 @@ let remove_index tree equality = let _, (_, l, r, ordering), _, _ = equality in let psl = path_string_of_term l and psr = path_string_of_term r in + let remove_index pos tree ps = + try + let ps_set = + PosEqSet.remove (pos, equality) (DiscriminationTree.find ps tree) in + if PosEqSet.is_empty ps_set then + DiscriminationTree.remove ps tree + else + DiscriminationTree.add ps ps_set tree + with Not_found -> + tree + in match ordering with - | Utils.Gt -> DiscriminationTree.remove psl tree - | Utils.Lt -> DiscriminationTree.remove psr tree + | Utils.Gt -> remove_index Utils.Left tree psl + | Utils.Lt -> remove_index Utils.Right tree psr | _ -> - let tree = DiscriminationTree.remove psl tree in - DiscriminationTree.remove psr tree + let tree = remove_index Utils.Left tree psl in + remove_index Utils.Right tree psr ;; @@ -107,8 +174,11 @@ let in_index tree equality = and psr = path_string_of_term r in let meta_convertibility = Inference.meta_convertibility_eq equality in let ok ps = - try let _, eq = DiscriminationTree.find ps tree in meta_convertibility eq - with Not_found -> false + try + let set = DiscriminationTree.find ps tree in + PosEqSet.exists (fun (p, e) -> meta_convertibility e) set + with Not_found -> + false in (ok psl) || (ok psr) ;; @@ -116,6 +186,7 @@ let in_index tree equality = let head_of_term = function | Cic.Appl (hd::tl) -> hd +(* | Cic.Meta _ -> Cic.Implicit None *) | term -> term ;; @@ -131,18 +202,6 @@ let rec subterm_at_pos pos term = ;; -let next_t pos term = - let t = subterm_at_pos pos term in - try - let t2 = subterm_at_pos [1] t in - pos @ [1] - with Not_found -> - match pos with - | [] -> [1] - | pos -> List.fold_right (fun i r -> if r = [] then [i+1] else i::r) pos [] -;; - - let rec after_t pos term = let pos' = match pos with @@ -160,24 +219,44 @@ let rec after_t pos term = ;; +let next_t pos term = + let t = subterm_at_pos pos term in + try + let _ = subterm_at_pos [1] t in + pos @ [1] + with Not_found -> + match pos with + | [] -> [1] + | pos -> after_t pos term +;; + + let retrieve_generalizations tree term = - let rec retrieve tree term pos = + let rec retrieve tree term pos = match tree with - | DiscriminationTree.Node (value, map) -> + | DiscriminationTree.Node (Some s, _) when pos = [] -> s + | DiscriminationTree.Node (_, map) -> let res = try let hd_term = head_of_term (subterm_at_pos pos term) in let n = PSMap.find hd_term map in match n with - | DiscriminationTree.Node (Some s, _) -> [s] + | DiscriminationTree.Node (Some s, _) -> s | DiscriminationTree.Node (None, _) -> - retrieve n term (next_t pos term) + let newpos = try next_t pos term with Not_found -> [] in + retrieve n term newpos with Not_found -> - [] + PosEqSet.empty in try let n = PSMap.find (Cic.Implicit None) map in - res @ (retrieve n term (after_t pos term)) + let newpos = try after_t pos term with _ -> [-1] in + if newpos = [-1] then + match n with + | DiscriminationTree.Node (Some s, _) -> PosEqSet.union s res + | _ -> res + else + PosEqSet.union res (retrieve n term newpos) with Not_found -> res in @@ -209,30 +288,43 @@ let jump_list = function let retrieve_unifiables tree term = let rec retrieve tree term pos = match tree with - | DiscriminationTree.Node (value, map) -> - let res = - try - match subterm_at_pos pos term with - | Cic.Meta _ -> - List.concat - (List.map - (fun t -> retrieve t term (next_t pos term)) - (jump_list tree)) - | subterm -> + | DiscriminationTree.Node (Some s, _) when pos = [] -> s + | DiscriminationTree.Node (_, map) -> + let subterm = + try Some (subterm_at_pos pos term) with Not_found -> None + in + match subterm with + | None -> PosEqSet.empty + | Some (Cic.Meta _) -> + let newpos = try next_t pos term with Not_found -> [] in + let jl = jump_list tree in + List.fold_left + (fun r s -> PosEqSet.union r s) + PosEqSet.empty + (List.map (fun t -> retrieve t term newpos) jl) + | Some subterm -> + let res = + try let hd_term = head_of_term subterm in let n = PSMap.find hd_term map in match n with - | DiscriminationTree.Node (Some s, _) -> [s] + | DiscriminationTree.Node (Some s, _) -> s | DiscriminationTree.Node (None, _) -> retrieve n term (next_t pos term) - with Not_found -> - [] - in - try - let n = PSMap.find (Cic.Implicit None) map in - res @ (retrieve n term (after_t pos term)) - with Not_found -> - res + with Not_found -> + PosEqSet.empty + in + try + let n = PSMap.find (Cic.Implicit None) map in + let newpos = try after_t pos term with _ -> [-1] in + if newpos = [-1] then + match n with + | DiscriminationTree.Node (Some s, _) -> PosEqSet.union s res + | _ -> res + else + PosEqSet.union res (retrieve n term newpos) + with Not_found -> + res in retrieve tree term [] ;; diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index 5607ca3db..ddec5f9d4 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -2,6 +2,29 @@ type retrieval_mode = Matching | Unification;; +let print_candidates mode term res = +(* match res with *) +(* | [] -> () *) +(* | _ -> *) + let _ = + match mode with + | Matching -> + Printf.printf "| candidates Matching %s\n" (CicPp.ppterm term) + | Unification -> + Printf.printf "| candidates Unification %s\n" (CicPp.ppterm term) + in + print_endline + (String.concat "\n" + (List.map + (fun (p, e) -> + Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p) + (Inference.string_of_equality e)) + res)); + print_endline "|"; +;; + + +(* let empty_table () = Path_indexing.PSTrie.empty ;; @@ -11,16 +34,20 @@ and remove_index = Path_indexing.remove_index and in_index = Path_indexing.in_index;; let get_candidates mode trie term = - let s = - match mode with - | Matching -> Path_indexing.retrieve_generalizations trie term - | Unification -> Path_indexing.retrieve_unifiables trie term + let res = + let s = + match mode with + | Matching -> Path_indexing.retrieve_generalizations trie term + | Unification -> Path_indexing.retrieve_unifiables trie term + in + Path_indexing.PosEqSet.elements s in - Path_indexing.PosEqSet.elements s + print_candidates mode term res; + res ;; +*) -(* let empty_table () = Discrimination_tree.DiscriminationTree.empty ;; @@ -30,11 +57,17 @@ and remove_index = Discrimination_tree.remove_index and in_index = Discrimination_tree.in_index;; let get_candidates mode tree term = - match mode with - | Matching -> Discrimination_tree.retrieve_generalizations tree term - | Unification -> Discrimination_tree.retrieve_unifiables tree term + let res = + let s = + match mode with + | Matching -> Discrimination_tree.retrieve_generalizations tree term + | Unification -> Discrimination_tree.retrieve_unifiables tree term + in + Discrimination_tree.PosEqSet.elements s + in +(* print_candidates mode term res; *) + res ;; -*) let rec find_matches metasenv context ugraph lift_amount term = @@ -195,10 +228,10 @@ let rec demodulate_term metasenv context ugraph table lift_amount term = let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in - let candidates = get_candidates Matching table term in match term with | C.Meta _ -> None | term -> + let candidates = get_candidates Matching table term in let res = find_matches metasenv context ugraph lift_amount term candidates in @@ -328,7 +361,6 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term = let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in - let candidates = get_candidates Unification table term in let res, lifted_term = match term with | C.Meta (i, l) -> @@ -415,6 +447,7 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term = match term with | C.Meta _ -> res, lifted_term | term -> + let candidates = get_candidates Unification table term in let r = find_all_matches metasenv context ugraph lift_amount term candidates in diff --git a/helm/ocaml/paramodulation/path_indexing.ml b/helm/ocaml/paramodulation/path_indexing.ml index bc9bc01f1..95d6de9f5 100644 --- a/helm/ocaml/paramodulation/path_indexing.ml +++ b/helm/ocaml/paramodulation/path_indexing.ml @@ -49,8 +49,6 @@ end module PSMap = Map.Make(OrderedPathStringElement);; -(* module PSTrie = Trie.Make(PathStringElementMap);; *) - module OrderedPosEquality = struct type t = Utils.pos * Inference.equality @@ -59,6 +57,9 @@ end module PosEqSet = Set.Make(OrderedPosEquality);; +module PSTrie = Trie.Make(PSMap);; + +(* (* * Trie: maps over lists. * Copyright (C) 2000 Jean-Christophe FILLIATRE @@ -111,6 +112,7 @@ module PSTrie = struct traverse [] t acc end +*) let index trie equality = diff --git a/helm/ocaml/paramodulation/test_indexing.ml b/helm/ocaml/paramodulation/test_indexing.ml index a54e0aef3..2ef07a17c 100644 --- a/helm/ocaml/paramodulation/test_indexing.ml +++ b/helm/ocaml/paramodulation/test_indexing.ml @@ -14,7 +14,7 @@ let build_equality term = b = Rel 4 c = Rel 5 *) -let main_test () = +let path_indexing_test () = let module C = Cic in let terms = [ C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Meta (1, [])]; C.Rel 5]; @@ -89,7 +89,59 @@ let next_after () = ;; +let discrimination_tree_test () = + let module C = Cic in + let terms = [ + C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Meta (1, [])]; C.Rel 5]; + C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 4]; C.Meta (1, [])]; + C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Rel 4]; C.Rel 5]; + C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 5]; C.Rel 4]; + C.Appl [C.Rel 10; C.Meta (5, []); C.Rel 11] + ] in + let path_strings = + List.map Discrimination_tree.path_string_of_term terms in + let table = + List.fold_left + Discrimination_tree.index + Discrimination_tree.DiscriminationTree.empty + (List.map build_equality terms) + in +(* let query = *) +(* C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 4]; C.Rel 5] in *) + let query = C.Appl [C.Rel 10; C.Meta (14, []); C.Meta (13, [])] in + let matches = Discrimination_tree.retrieve_generalizations table query in + let unifications = Discrimination_tree.retrieve_unifiables table query in + let eq1 = build_equality (C.Appl [C.Rel 1; C.Meta (1, []); C.Meta (1, [])]) + and eq2 = build_equality (C.Appl [C.Rel 1; C.Meta (1, []); C.Meta (2, [])]) in + let res1 = Discrimination_tree.in_index table eq1 + and res2 = Discrimination_tree.in_index table eq2 in + let print_results res = + String.concat "\n" + (Discrimination_tree.PosEqSet.fold + (fun (p, e) l -> + let s = + "(" ^ (Utils.string_of_pos p) ^ ", " ^ + (Inference.string_of_equality e) ^ ")" + in + s::l) + res []) + in + Printf.printf "path_strings:\n%s\n\n" + (String.concat "\n" + (List.map Discrimination_tree.string_of_path_string path_strings)); + Printf.printf "table:\n%s\n\n" + (Discrimination_tree.string_of_discrimination_tree table); + Printf.printf "matches:\n%s\n\n" (print_results matches); + Printf.printf "unifications:\n%s\n\n" (print_results unifications); + Printf.printf "in_index %s: %s\n" + (Inference.string_of_equality eq1) (string_of_bool res1); + Printf.printf "in_index %s: %s\n" + (Inference.string_of_equality eq2) (string_of_bool res2); +;; + + (* differing ();; *) -(* main_test ();; *) -next_after ();; +(* next_after ();; *) +discrimination_tree_test ();; +(* path_indexing_test ();; *)