X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=8bbf6e1606162c47eca6f15a8490e1ba2f7fa3f3;hb=d35aca0e979a9c7edbc60c44040360d52be8ca82;hp=48811239bf08a30caaca026a3c97929be3e4e590;hpb=4693f3b9de6d867921b51f61e9a7dc36c3da1b77;p=helm.git diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 48811239b..8bbf6e160 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -19,27 +19,22 @@ 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,36 +43,39 @@ 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 - WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a + 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 *) + let cl = if bonus_weight = 0 then (w,cl) else (0,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 - WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a + 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 *) + let g = if bonus_weight = 0 then (w,g) else (0,g) in + WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a ;; let remove_passive_clause (passives_w,passives_a) cl = @@ -86,20 +84,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 +123,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 @@ -347,16 +335,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