From 18beb4339a683c5b6243673b91da878a208b36e3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 13 Jul 2009 13:48:35 +0000 Subject: [PATCH] statistics are used, when possible, to sort constants --- .../binaries/matitaprover/matitaprover.ml | 85 +++++++++++++------ .../components/ng_paramodulation/stats.ml | 24 +++++- .../components/ng_paramodulation/stats.mli | 2 +- 3 files changed, 82 insertions(+), 29 deletions(-) diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml index cfa82da98..b1a71034f 100644 --- a/helm/software/components/binaries/matitaprover/matitaprover.ml +++ b/helm/software/components/binaries/matitaprover/matitaprover.ml @@ -99,7 +99,7 @@ let success_msg bag l (pp : ?margin:int -> leaf Terms.unit_clause -> string) ord (times.Unix.tms_utime +. times.Unix.tms_stime) ^ " using " ^ ord); ;; -let start_msg passives g_passives (pp : leaf Terms.unit_clause -> string) oname = +let start_msg stats passives g_passives (pp : ?margin:int -> leaf Terms.unit_clause -> string) oname = let prefix = string_of_int (Unix.getpid ()) in let prerr_endline s = prerr_endline (prefix ^ ": " ^ s) in prerr_endline "Facts:"; @@ -108,13 +108,26 @@ let start_msg passives g_passives (pp : leaf Terms.unit_clause -> string) oname prerr_endline (" " ^ pp g_passives); prerr_endline "Order:"; prerr_endline (" " ^ oname); + prerr_endline "Leaf order:"; + List.iter (fun ((_,name), (a,b,c,gp,l)) -> + prerr_endline (name ^ " " ^ string_of_int a ^ " " ^ + string_of_int b ^ " " ^ + string_of_int c ^ " " ^ + String.concat "," (List.map string_of_int gp) ^ + String.concat "," (List.map snd l))) stats; ;; let report_error s = prerr_endline (string_of_int (Unix.getpid())^": "^s);; module Main(P : Paramod.Paramod with type t = leaf) = struct - let run bag g_passives passives pp_unit_clause name = + let run stats goal hypotheses pp_unit_clause name = + let bag = Terms.empty_bag, 0 in + let bag, g_passives = P.mk_goal bag goal in + let bag, passives = + HExtlib.list_mapi_acc (fun x _ b -> P.mk_passive b x) bag hypotheses + in + start_msg stats passives g_passives pp_unit_clause name; match P.paramod ~max_steps:max_int bag ~g_passives:[g_passives] ~passives @@ -129,13 +142,13 @@ module Main(P : Paramod.Paramod with type t = leaf) = struct ;; end -let worker order goal hypotheses = + let compute_stats goal hypotheses = let module C = struct type t = leaf let cmp (a,_) (b,_) = Pervasives.compare a b end in let module B = MakeBlob(C) in let module Pp = Pp.Pp(B) in - let module O = Orderings.NRKBO(B) in (* just for processing the clauses *) + let module O = Orderings.NRKBO(B) in let module P = Paramod.Paramod(O) in let module Stats = Stats.Stats(O) in let bag = Terms.empty_bag, 0 in @@ -143,40 +156,56 @@ let worker order goal hypotheses = let bag, passives = HExtlib.list_mapi_acc (fun x _ b -> P.mk_passive b x) bag hypotheses in - (* TODO: do stats analysys there and generate a new - * C and then B - * TODO: rebuild clauses, since the ordering has to - * change after the stats are computed *) - let symb_list = Stats.parse_symbols passives g_passives in - prerr_endline "Hypotheses statistics :"; - List.iter (fun (t,occ,ar,g_occ) -> prerr_endline - (Printf.sprintf "%s %d %d %d %s" - (B.pp t) ar occ g_occ - (String.concat "," - (List.map B.pp (Stats.dependencies t passives)))); - if List.exists - (fun (u,occ2,ar2,g_occ2) -> not (B.eq t u) && occ = occ2 - && ar = ar2 && g_occ = g_occ2) symb_list - then prerr_endline ((B.pp t) ^ " clashes") - ) symb_list; - let module C = C in + let data = Stats.parse_symbols passives g_passives in + let data = + List.map + (fun (name, n_occ, arity, n_gocc, g_pos) -> + name, (n_occ, arity, n_gocc, g_pos, Stats.dependencies name passives)) + data + in + List.sort Pervasives.compare data + ;; + +let worker order goal hypotheses = + let stats = compute_stats goal hypotheses in + let module C = + struct + let cmp = + let raw = List.map snd stats in + let rec pos x = function + | ((y,_)::tl) when y = x -> 0 + | _::tl -> 1 + pos x tl + | [] -> assert false + in + if List.length raw = + List.length (HExtlib.list_uniq raw) + then + (prerr_endline "NO CLASH, using fixed ground order"; + fun a b -> + Pervasives.compare + (pos a stats) + (pos b stats)) + else + (prerr_endline "CLASH, statistics insufficient"; + fun (a,_) (b,_) -> Pervasives.compare a b) + ;; + end + in let module B = MakeBlob(C) in + let module Pp = Pp.Pp(B) in match order with | `NRKBO -> let module O = Orderings.NRKBO(B) in let module Main = Main(Paramod.Paramod(O)) in - start_msg passives g_passives Pp.pp_unit_clause O.name; - Main.run bag g_passives passives Pp.pp_unit_clause O.name + Main.run stats goal hypotheses Pp.pp_unit_clause O.name | `KBO -> let module O = Orderings.KBO(B) in let module Main = Main(Paramod.Paramod(O)) in - start_msg passives g_passives Pp.pp_unit_clause O.name; - Main.run bag g_passives passives Pp.pp_unit_clause O.name + Main.run stats goal hypotheses Pp.pp_unit_clause O.name | `LPO -> let module O = Orderings.LPO(B) in let module Main = Main(Paramod.Paramod(O)) in - start_msg passives g_passives Pp.pp_unit_clause O.name; - Main.run bag g_passives passives Pp.pp_unit_clause O.name + Main.run stats goal hypotheses Pp.pp_unit_clause O.name ;; let print_status p = @@ -243,9 +272,11 @@ usage: matitaprover [options] problemfile"; [ (fun () -> worker `NRKBO goal hypotheses) ; +(* (fun () -> worker `KBO goal hypotheses) ; (fun () -> worker `LPO goal hypotheses) +*) ]; let rec aux () = if List.length !childs = 0 then diff --git a/helm/software/components/ng_paramodulation/stats.ml b/helm/software/components/ng_paramodulation/stats.ml index 90d6ccf0b..a281ddc86 100644 --- a/helm/software/components/ng_paramodulation/stats.ml +++ b/helm/software/components/ng_paramodulation/stats.ml @@ -55,10 +55,32 @@ module Stats (B : Terms.Blob) = | Terms.Predicate _ -> assert false; ;; + let goal_pos t goal = + let rec aux path = function + | Terms.Var _ -> [] + | Terms.Leaf x -> + if B.eq t x then path else [] + | Terms.Node l -> + match + HExtlib.list_findopt + (fun x i -> + let p = aux (i::path) x in + if p = [] then None else Some p) + l + with + | None -> [] + | Some p -> p + in + aux [] + (match goal with + | _,Terms.Equation (l,r,ty,_),_,_ -> Terms.Node [ Terms.Leaf B.eqP; ty; l; r ] + | _,Terms.Predicate p,_,_ -> p) + ;; + let parse_symbols l goal = let res = parse_symbols (parse_symbols SymbMap.empty [goal]) l in SymbMap.fold (fun t (occ,ar) acc -> - (t,occ,ar,goal_occ_nbr t goal)::acc) res [] + (t,occ,ar,goal_occ_nbr t goal,goal_pos t goal)::acc) res [] ;; let rec dependencies op clauses acc = diff --git a/helm/software/components/ng_paramodulation/stats.mli b/helm/software/components/ng_paramodulation/stats.mli index b9be72907..271fd2bcf 100644 --- a/helm/software/components/ng_paramodulation/stats.mli +++ b/helm/software/components/ng_paramodulation/stats.mli @@ -18,7 +18,7 @@ module Stats (B : Orderings.Blob) : val parse_symbols : B.t Terms.unit_clause list -> (* hypotheses *) B.t Terms.unit_clause -> (* goal *) - (B.t * int * int * int) list + (B.t * int * int * int * int list) list val dependencies : B.t -> B.t Terms.unit_clause list -> B.t list -- 2.39.2