X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=4a688620590f94506e4ae07c7ec47bb5fe281269;hb=b714e87e96f14f332a5157567a4c62a4b28fa8eb;hp=d65fce1b2fa4e1fb877b1c3f0b8475d81ee14788;hpb=bebc917ebff72c2e235cb3062a4c94f10a9aab27;p=helm.git diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index d65fce1b2..4a6886205 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -11,35 +11,30 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) -let debug s = prerr_endline s ;; -let debug _ = ();; +let debug s = prerr_endline (Lazy.force s) ;; +(* let debug _ = ();; *) let monster = 100;; module type Paramod = sig type t - type input type szsontology = | Unsatisfiable of (t Terms.bag * int * int list) list | GaveUp | Error of string | Timeout of int * t Terms.bag - type bag = t Terms.bag * int - val mk_passive : bag -> input * input -> bag * t Terms.clause - val mk_goal : bag -> input * input -> bag * t Terms.clause val paramod : useage:bool -> max_steps:int -> + print_problem:bool -> ?timeout:float -> - bag -> - g_passives:t Terms.clause list -> - passives:t Terms.clause list -> szsontology + t Terms.foterm * (t Terms.foterm list * t Terms.foterm list) -> + (t Terms.foterm * (t Terms.foterm list * t Terms.foterm list)) list -> szsontology end module Paramod (B : Orderings.Blob) = struct type t = B.t - type input = B.input type szsontology = | Unsatisfiable of (B.t Terms.bag * int * int list) list | GaveUp @@ -48,35 +43,36 @@ module Paramod (B : Orderings.Blob) = struct exception Stop of szsontology type bag = B.t Terms.bag * int module Pp = Pp.Pp (B) - module FU = FoUnif.Founif(B) + module FU = FoUnif.FoUnif(B) module IDX = Index.Index(B) module Sup = Superposition.Superposition(B) module Utils = FoUtils.Utils(B) module Order = B + module Clauses = Clauses.Clauses(B) module WeightOrderedPassives = struct type t = B.t Terms.passive_clause - let compare = Utils.compare_passive_clauses_weight + let compare = Clauses.compare_passive_clauses_weight end module AgeOrderedPassives = struct type t = B.t Terms.passive_clause - let compare = Utils.compare_passive_clauses_age + let compare = Clauses.compare_passive_clauses_age end module WeightPassiveSet = Set.Make(WeightOrderedPassives) module AgePassiveSet = Set.Make(AgeOrderedPassives) - let add_passive_clause ?(no_weight=false) (passives_w,passives_a) cl = - let cl = if no_weight then (0,cl) - else Utils.mk_passive_clause cl in + let add_passive_clause ?(bonus_weight=0) (passives_w,passives_a) cl = + let (w,cl) = Clauses.mk_passive_clause cl in + let cl = (w+bonus_weight,cl) in WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a ;; - let add_passive_goal ?(no_weight=false) (passives_w,passives_a) g = - let g = if no_weight then (0,g) - else Utils.mk_passive_goal g in + let add_passive_goal ?(bonus_weight=0) (passives_w,passives_a) g = + let (w,g) = Clauses.mk_passive_goal g in + let g = (w+bonus_weight,g) in WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a ;; @@ -86,20 +82,20 @@ module Paramod (B : Orderings.Blob) = struct passives_w,passives_a ;; - let add_passive_clauses ?(no_weight=false) + let add_passive_clauses ?(bonus_weight=0) (passives_w,passives_a) new_clauses = let new_clauses_w,new_clauses_a = - List.fold_left (add_passive_clause ~no_weight) + List.fold_left (add_passive_clause ~bonus_weight) (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses in (WeightPassiveSet.union new_clauses_w passives_w, AgePassiveSet.union new_clauses_a passives_a) ;; - let add_passive_goals ?(no_weight=false) + let add_passive_goals ?(bonus_weight=0) (passives_w,passives_a) new_clauses = let new_clauses_w,new_clauses_a = - List.fold_left (add_passive_goal ~no_weight) + List.fold_left (add_passive_goal ~bonus_weight) (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses in (WeightPassiveSet.union new_clauses_w passives_w, @@ -125,16 +121,6 @@ module Paramod (B : Orderings.Blob) = struct else WeightPassiveSet.min_elt passives_w ;; - let mk_clause bag maxvar (t,ty) = - let (proof,ty) = B.saturate t ty in - let c, maxvar = Utils.mk_clause maxvar [] [ty] proof in - let bag, c = Terms.add_to_bag c bag in - (bag, maxvar), c - ;; - - let mk_passive (bag,maxvar) = mk_clause bag maxvar;; - let mk_goal (bag,maxvar) = mk_clause bag maxvar;; - (* TODO : global age over facts and goals (without comparing weights) *) let select ~use_age passives g_passives = if is_passive_set_empty passives then begin @@ -162,11 +148,11 @@ module Paramod (B : Orderings.Blob) = struct let backward_infer_step bag maxvar actives passives g_actives g_passives g_current iterno = (* superposition left, simplifications on goals *) - debug "infer_left step..."; + debug (lazy "infer_left step..."); let bag, maxvar, new_goals = Sup.infer_left bag maxvar g_current actives in - debug "Performed infer_left step"; + debug (lazy "Performed infer_left step"); let bag = Terms.replace_in_bag (g_current,false,iterno) bag in bag, maxvar, actives, passives, g_current::g_actives, (add_passive_goals g_passives new_goals) @@ -184,12 +170,12 @@ module Paramod (B : Orderings.Blob) = struct * new = supright e'' A'' * * new'= demod A'' new * * P' = P + new' *) - debug "Forward infer step..."; + debug (lazy "Forward infer step..."); debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives))))); let bag, maxvar, actives, new_clauses = Sup.infer_right bag maxvar current actives in - debug "Demodulating goals with actives..."; + debug (lazy "Demodulating goals with actives..."); (* keep goals demodulated w.r.t. actives and check if solved *) let bag, g_actives = List.fold_left @@ -294,7 +280,7 @@ module Paramod (B : Orderings.Blob) = struct if weight > monster then bag,None else bag, Some (current,actives) else if Sup.orphan_murder bag (fst actives) current then - let _ = debug "Orphan murdered" in + let _ = debug (lazy "Orphan murdered") in let bag = Terms.replace_in_bag (current,true,iterno) bag in bag, None else Sup.keep_simplified current actives bag maxvar @@ -328,7 +314,6 @@ module Paramod (B : Orderings.Blob) = struct (*prerr_endline "Active table :"; (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x)) (fst actives)); *) - let bag,maxvar,actives,passives,g_actives,g_passives = aux_select bag passives g_passives in @@ -348,16 +333,32 @@ module Paramod (B : Orderings.Blob) = struct actives passives g_actives g_passives ;; - let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives = + let paramod ~useage ~max_steps ~print_problem ?timeout goal hypotheses = let initial_timestamp = Unix.gettimeofday () in + let bag = Terms.empty_bag in + let maxvar = 0 in + let build_clause (bag,maxvar,l) (t,(nlit,plit)) = + let c,maxvar = Clauses.mk_clause maxvar nlit plit t in + let bag,c = Terms.add_to_bag c bag in + (bag,maxvar,c::l) + in + let bag,maxvar,goals = build_clause (bag,maxvar,[]) goal in + let bag,maxvar,hypotheses = List.fold_left build_clause (bag,maxvar,[]) hypotheses in + let goal = match goals with | [g] -> g | _ -> assert false in let passives = - add_passive_clauses ~no_weight:true passive_empty_set passives + add_passive_clauses ~bonus_weight:(-1000) passive_empty_set hypotheses in let g_passives = - add_passive_goals ~no_weight:true passive_empty_set g_passives + add_passive_goal ~bonus_weight:(-1000) passive_empty_set goal in let g_actives = [] in let actives = [], IDX.DT.empty in + if print_problem then begin + prerr_endline "Facts:"; + List.iter (fun x -> prerr_endline (" " ^ Pp.pp_clause x)) hypotheses; + prerr_endline "Goal:"; + prerr_endline (" " ^ Pp.pp_clause goal); + end; try given_clause ~useage ~noinfer:false bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives