From: Alberto Griggio Date: Mon, 20 Jun 2005 18:04:09 +0000 (+0000) Subject: some optimizations... X-Git-Tag: INDEXING_NO_PROOFS~108 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bdc855b1b6c9552a49a01769cb906a438ca60cc4;p=helm.git some optimizations... --- diff --git a/helm/ocaml/paramodulation/Makefile b/helm/ocaml/paramodulation/Makefile index be59fc135..f16094a17 100644 --- a/helm/ocaml/paramodulation/Makefile +++ b/helm/ocaml/paramodulation/Makefile @@ -34,15 +34,18 @@ DEPOBJS = \ path_indexing.ml \ indexing.ml \ saturation.ml \ - test_path_indexing.ml + discrimination_tree.ml \ + test_indexing.ml TOPLEVELOBJS = $(INTERFACE_FILES:%.mli=%.cmo) \ path_indexing.cmo \ + discrimination_tree.cmo \ indexing.cmo \ saturation.cmo TESTOBJS = $(INTERFACE_FILES:%.mli=%.cmo) \ path_indexing.cmo \ - test_path_indexing.cmo + discrimination_tree.cmo \ + test_indexing.cmo # REGTESTOBJS = $(TESTOBJS) regtest.cmo # TESTLIBOBJS = $(TESTOBJS) testlibrary.cmo @@ -57,7 +60,7 @@ saturation: $(TOPLEVELOBJS) $(LIBRARIES) saturation.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT) $(OCAMLOPT) -thread -linkpkg -o $@ $(TOPLEVELOBJS:.cmo=.cmx) -test_path_indexing: $(TESTOBJS) $(TEST_LIBRARIES) +test_indexing: $(TESTOBJS) $(TEST_LIBRARIES) $(OCAMLC) -linkpkg -o $@ $(TESTOBJS) .SUFFIXES: .ml .mli .cmo .cmi .cmx diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index 84559b222..5607ca3db 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -1,61 +1,41 @@ -let head_of_term = function - | Cic.Appl (hd::tl) -> hd - | t -> t -;; +type retrieval_mode = Matching | Unification;; -(* let empty_table () = - Hashtbl.create 10 + Path_indexing.PSTrie.empty ;; - -let index table eq = - let _, (_, l, r, ordering), _, _ = eq in - let hl = head_of_term l in - let hr = head_of_term r in - let index x pos = - let x_entry = try Hashtbl.find table x with Not_found -> [] in - Hashtbl.replace table x ((pos, eq)::x_entry) - in - let _ = - match ordering with - | Utils.Gt -> - index hl Utils.Left - | Utils.Lt -> - index hr Utils.Right - | _ -> index hl Utils.Left; index hr Utils.Right +let index = Path_indexing.index +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 in -(* index hl Utils.Left; *) -(* index hr Utils.Right; *) - table + Path_indexing.PosEqSet.elements s ;; -let remove_index table eq = - let _, (_, l, r, ordering), _, _ = eq in - let hl = head_of_term l - and hr = head_of_term r in - let remove_index x pos = - let x_entry = try Hashtbl.find table x with Not_found -> [] in - let newentry = List.filter (fun e -> e <> (pos, eq)) x_entry in - Hashtbl.replace table x newentry - in - remove_index hl Utils.Left; - remove_index hr Utils.Right; - table +(* +let empty_table () = + Discrimination_tree.DiscriminationTree.empty ;; -*) +let index = Discrimination_tree.index +and remove_index = Discrimination_tree.remove_index +and in_index = Discrimination_tree.in_index;; -let empty_table () = - Path_indexing.PSTrie.empty +let get_candidates mode tree term = + match mode with + | Matching -> Discrimination_tree.retrieve_generalizations tree term + | Unification -> Discrimination_tree.retrieve_unifiables tree term ;; +*) -let index = Path_indexing.index -and remove_index = Path_indexing.remove_index;; - let rec find_matches metasenv context ugraph lift_amount term = let module C = Cic in @@ -157,27 +137,6 @@ let rec find_all_matches ?(unif_fun=CicUnification.fo_unif) ;; -type retrieval_mode = Matching | Unification;; - -(* -let get_candidates mode table term = - try Hashtbl.find table (head_of_term term) with Not_found -> [] -;; -*) - - -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 - in - Path_indexing.PosEqSet.elements s -;; - - let subsumption env table target = let _, (ty, tl, tr, _), tmetas, _ = target in let metasenv, context, ugraph = env in diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 00e543c2e..e79d78e84 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -1214,3 +1214,25 @@ let subsumption env target source = ); res ;; + + +let extract_differing_subterms t1 t2 = + let module C = Cic in + let rec aux t1 t2 = + match t1, t2 with + | C.Appl l1, C.Appl l2 when (List.length l1) <> (List.length l2) -> + [(t1, t2)] + | C.Appl (h1::tl1), C.Appl (h2::tl2) -> + let res = List.concat (List.map2 aux tl1 tl2) in + if h1 <> h2 then + if res = [] then [(h1, h2)] else [(t1, t2)] + else + if List.length res > 1 then [(t1, t2)] else res + | t1, t2 -> + if t1 <> t2 then [(t1, t2)] else [] + in + let res = aux t1 t2 in + match res with + | hd::[] -> Some hd + | _ -> None +;; diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli index 0cc0fcb70..5ced528bb 100644 --- a/helm/ocaml/paramodulation/inference.mli +++ b/helm/ocaml/paramodulation/inference.mli @@ -79,3 +79,6 @@ val subsumption: environment -> equality -> equality -> bool val metas_of_term: Cic.term -> int list val fix_metas: int -> equality -> int * equality + +val extract_differing_subterms: + Cic.term -> Cic.term -> (Cic.term * Cic.term) option diff --git a/helm/ocaml/paramodulation/path_indexing.ml b/helm/ocaml/paramodulation/path_indexing.ml index 87e917fff..bc9bc01f1 100644 --- a/helm/ocaml/paramodulation/path_indexing.ml +++ b/helm/ocaml/paramodulation/path_indexing.ml @@ -160,6 +160,22 @@ let remove_index trie equality = ;; +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 ok ps = + try + let set = PSTrie.find ps trie in + PosEqSet.exists (fun (p, e) -> meta_convertibility e) set + with Not_found -> + false + in + (List.exists ok psl) || (List.exists ok psr) +;; + + let head_of_term = function | Cic.Appl (hd::tl) -> hd | term -> term diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index c45124338..634df11ff 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -1,6 +1,7 @@ open Inference;; open Utils;; + (* profiling statistics... *) let infer_time = ref 0.;; let forward_simpl_time = ref 0.;; @@ -14,6 +15,7 @@ let elapsed_time = ref 0.;; let maximal_retained_equality = ref None;; (* equality-selection related globals *) +let use_fullred = ref false;; let weight_age_ratio = ref 0;; (* settable by the user from the command line *) let weight_age_counter = ref !weight_age_ratio;; let symbols_ratio = ref 0;; @@ -93,7 +95,11 @@ let select env passive (active, _) = (Negative, hd), ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table) | [], hd::tl -> - let passive_table = Indexing.remove_index passive_table hd in + let passive_table = + Indexing.remove_index passive_table hd +(* if !use_fullred then Indexing.remove_index passive_table hd *) +(* else passive_table *) + in (Positive, hd), (([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table) | _, _ -> assert false @@ -134,17 +140,26 @@ let select env passive (active, _) = let _, current = EqualitySet.fold f pos_set initial in (* Printf.printf "\nsymbols-based selection: %s\n\n" *) (* (string_of_equality ~env current); *) - let passive_table = Indexing.remove_index passive_table current in + let passive_table = + Indexing.remove_index passive_table current +(* if !use_fullred then Indexing.remove_index passive_table current *) +(* else passive_table *) + in (Positive, current), (([], neg_set), (remove current pos_list, EqualitySet.remove current pos_set), passive_table) | _ -> let current = EqualitySet.min_elt pos_set in + let passive_table = + Indexing.remove_index passive_table current +(* if !use_fullred then Indexing.remove_index passive_table current *) +(* else passive_table *) + in let passive = (neg_list, neg_set), (remove current pos_list, EqualitySet.remove current pos_set), - Indexing.remove_index passive_table current + passive_table in (Positive, current), passive ) @@ -157,6 +172,8 @@ let select env passive (active, _) = (neg_list, neg_set), (remove current pos_list, EqualitySet.remove current pos_set), Indexing.remove_index passive_table current +(* if !use_fullred then Indexing.remove_index passive_table current *) +(* else passive_table *) in (Positive, current), passive else @@ -174,10 +191,18 @@ let make_passive neg pos = let set_of equalities = List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities in - let table = Indexing.empty_table () in + let table = + List.fold_left (fun tbl e -> Indexing.index tbl e) + (Indexing.empty_table ()) pos +(* if !use_fullred then *) +(* List.fold_left (fun tbl e -> Indexing.index tbl e) *) +(* (Indexing.empty_table ()) pos *) +(* else *) +(* Indexing.empty_table () *) + in (neg, set_of neg), (pos, set_of pos), - List.fold_left (fun tbl e -> Indexing.index tbl e) table pos + table ;; @@ -191,12 +216,19 @@ let add_to_passive passive (new_neg, new_pos) = let ok set equality = not (EqualitySet.mem equality set) in let neg = List.filter (ok neg_set) new_neg and pos = List.filter (ok pos_set) new_pos in + let table = + List.fold_left (fun tbl e -> Indexing.index tbl e) table pos +(* if !use_fullred then *) +(* List.fold_left (fun tbl e -> Indexing.index tbl e) table pos *) +(* else *) +(* table *) + in let add set equalities = List.fold_left (fun s e -> EqualitySet.add e s) set equalities in (neg @ neg_list, add neg_set neg), (pos_list @ pos, add pos_set pos), - List.fold_left (fun tbl e -> Indexing.index tbl e) table pos + table ;; @@ -218,17 +250,6 @@ let prune_passive howmany (active, _) passive = let in_weight = int_of_float (howmany *. ratio /. (ratio +. 1.)) and in_age = int_of_float (howmany /. (ratio +. 1.)) in Printf.printf "in_weight: %d, in_age: %d\n" in_weight in_age; -(* let rec pickw w s = *) -(* if w > 0 then *) -(* try *) -(* let e = EqualitySet.min_elt s in *) -(* let w, s' = pickw (w-1) (EqualitySet.remove e s) in *) -(* w, EqualitySet.add e s' *) -(* with Not_found -> *) -(* w, s *) -(* else *) -(* 0, EqualitySet.empty *) -(* in *) let symbols, card = match active with | (Negative, e)::_ -> @@ -311,7 +332,13 @@ 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 ()) in + (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) +(* if !use_fullred then *) +(* EqualitySet.fold *) +(* (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) *) +(* else *) +(* tbl *) + in (nl, ns), (pl, ps), tbl ;; @@ -375,14 +402,15 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = and pp = List.map (fun e -> (Positive, e)) pp in pn @ pp, Some pt in - let all = active_list @ pl in - let rec find_duplicate sign current = function - | [] -> false - | (s, eq)::tl when s = sign -> - if meta_convertibility_eq current eq then true - else find_duplicate sign current tl - | _::tl -> find_duplicate sign current tl - in + let all = if pl = [] then active_list else active_list @ pl in + +(* let rec find_duplicate sign current = function *) +(* | [] -> false *) +(* | (s, eq)::tl when s = sign -> *) +(* if meta_convertibility_eq current eq then true *) +(* else find_duplicate sign current tl *) +(* | _::tl -> find_duplicate sign current tl *) +(* in *) let demodulate table current = let newmeta, newcurrent = Indexing.demodulation !maxmeta env table current in @@ -403,11 +431,24 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = in match res with | None -> None - | Some (s, c) -> - if find_duplicate s c all then + | Some (Negative, c) -> + let ok = not ( + List.exists + (fun (s, eq) -> s = Negative && meta_convertibility_eq eq c) + all) + in + if ok then res else None + | Some (Positive, c) -> + if Indexing.in_index active_table c then None else - res + match passive_table with + | None -> res + | Some passive_table -> + if Indexing.in_index passive_table c then None else res + +(* | Some (s, c) -> if find_duplicate s c all then None else res *) + (* if s = Utils.Negative then *) (* res *) (* else *) @@ -490,14 +531,14 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = in let new_pos = EqualitySet.elements new_pos_set in - let subs = - match passive_table with - | None -> - (fun e -> not (Indexing.subsumption env active_table e)) - | Some passive_table -> - (fun e -> not ((Indexing.subsumption env active_table e) || - (Indexing.subsumption env passive_table e))) - in +(* let subs = *) +(* match passive_table with *) +(* | None -> *) +(* (fun e -> not (Indexing.subsumption env active_table e)) *) +(* | Some passive_table -> *) +(* (fun e -> not ((Indexing.subsumption env active_table e) || *) +(* (Indexing.subsumption env passive_table e))) *) +(* in *) let t1 = Unix.gettimeofday () in @@ -514,7 +555,17 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = let t2 = Unix.gettimeofday () in fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1); - new_neg, new_pos + let is_duplicate = + match passive_table with + | None -> (fun e -> not (Indexing.in_index active_table e)) + | Some passive_table -> + (fun e -> not ((Indexing.in_index active_table e) || + (Indexing.in_index passive_table e))) + in + new_neg, List.filter is_duplicate new_pos + +(* new_neg, new_pos *) + (* let res = *) (* (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *) (* List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *) @@ -611,7 +662,9 @@ 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.))) ;; @@ -663,7 +716,7 @@ let rec given_clause env passive active = Success (proof, env) else let t1 = Unix.gettimeofday () in - let new' = forward_simplify_new env new' active in + let new' = forward_simplify_new env new' (* ~passive *) active in let t2 = Unix.gettimeofday () in let _ = forward_simpl_time := !forward_simpl_time +. (t2 -. t1) @@ -900,7 +953,10 @@ let main () = let start = Unix.gettimeofday () in print_endline "GO!"; start_time := Unix.gettimeofday (); - let res = !given_clause_ref env passive active in + let res = + (if !use_fullred then given_clause_fullred else given_clause) + env passive active + in let finish = Unix.gettimeofday () in match res with | Failure -> @@ -932,7 +988,7 @@ let _ = and set_conf f = configuration_file := f and set_lpo () = Utils.compare_terms := lpo and set_kbo () = Utils.compare_terms := nonrec_kbo - and set_fullred () = given_clause_ref := given_clause_fullred + and set_fullred () = use_fullred := true and set_time_limit v = time_limit := float_of_int v in Arg.parse [