From 04fcadbd9e194847138d97a0a9892a475bc21c88 Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Wed, 22 Jun 2005 17:57:55 +0000 Subject: [PATCH] reverted to previous version, as it worked better... --- .../paramodulation/discrimination_tree.ml | 5 +- helm/ocaml/paramodulation/indexing.ml | 55 ++++++++----------- helm/ocaml/paramodulation/path_indexing.ml | 6 +- helm/ocaml/paramodulation/saturation.ml | 3 +- 4 files changed, 30 insertions(+), 39 deletions(-) diff --git a/helm/ocaml/paramodulation/discrimination_tree.ml b/helm/ocaml/paramodulation/discrimination_tree.ml index 9470e1bde..b5a2d7274 100644 --- a/helm/ocaml/paramodulation/discrimination_tree.ml +++ b/helm/ocaml/paramodulation/discrimination_tree.ml @@ -39,10 +39,9 @@ end module PosEqSet = Set.Make(OrderedPosEquality);; -module DiscriminationTree = Trie.Make(PSMap);; +(* module DiscriminationTree = Trie.Make(PSMap);; *) -(* module DiscriminationTree = struct type key = path_string type t = Node of PosEqSet.t option * (t PSMap.t) @@ -92,8 +91,8 @@ module DiscriminationTree = struct traverse [] t acc end -*) + let string_of_discrimination_tree tree = let rec to_string level = function | DiscriminationTree.Node (value, map) -> diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index ddec5f9d4..bbd3c4844 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -3,28 +3,24 @@ 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 _ = + 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 ;; @@ -34,20 +30,16 @@ and remove_index = Path_indexing.remove_index and in_index = Path_indexing.in_index;; let get_candidates mode 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 + let s = + match mode with + | Matching -> Path_indexing.retrieve_generalizations trie term + | Unification -> Path_indexing.retrieve_unifiables trie term in - print_candidates mode term res; - res + Path_indexing.PosEqSet.elements s ;; -*) +(* let empty_table () = Discrimination_tree.DiscriminationTree.empty ;; @@ -68,6 +60,7 @@ let get_candidates mode tree term = (* print_candidates mode term res; *) res ;; +*) let rec find_matches metasenv context ugraph lift_amount term = @@ -228,10 +221,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 @@ -361,6 +354,7 @@ 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) -> @@ -447,7 +441,6 @@ 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 95d6de9f5..bc9bc01f1 100644 --- a/helm/ocaml/paramodulation/path_indexing.ml +++ b/helm/ocaml/paramodulation/path_indexing.ml @@ -49,6 +49,8 @@ end module PSMap = Map.Make(OrderedPathStringElement);; +(* module PSTrie = Trie.Make(PathStringElementMap);; *) + module OrderedPosEquality = struct type t = Utils.pos * Inference.equality @@ -57,9 +59,6 @@ end module PosEqSet = Set.Make(OrderedPosEquality);; -module PSTrie = Trie.Make(PSMap);; - -(* (* * Trie: maps over lists. * Copyright (C) 2000 Jean-Christophe FILLIATRE @@ -112,7 +111,6 @@ module PSTrie = struct traverse [] t acc end -*) let index trie equality = diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 634df11ff..b77fe955f 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -324,7 +324,7 @@ let prune_passive howmany (active, _) passive = let w, s, l = picka w s tl in w, s, hd::l else - 0, s, [] + 0, s, l in let in_age, ns, nl = picka in_age ns nl in let _, ps, pl = picka in_age ps pl in @@ -662,6 +662,7 @@ let backward_simplify env new' ?passive active = let get_selection_estimate () = elapsed_time := (Unix.gettimeofday ()) -. !start_time; +(* !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *) int_of_float ( ceil ((float_of_int !processed_clauses) *. (!time_limit /. !elapsed_time -. 1.))) -- 2.39.2