X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=32eff6826f468e9d652f4e5797916deccaba9666;hb=e7d2bbd23d9cc06232afd4c9b50d09b95abfbefa;hp=b898d353babce559769c77239d630d1bae9b404b;hpb=d268de514258947484a22a106c220b102c611cc3;p=helm.git diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index b898d353b..32eff6826 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -12,11 +12,8 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) let debug s = prerr_endline s ;; -(* let debug _ = ();; *) +let debug _ = ();; -let max_nb_iter = 999999999 ;; -let amount_of_time = 300.0 ;; - module Paramod (B : Terms.Blob) = struct exception Failure of string * B.t Terms.bag * int * int type bag = B.t Terms.bag * int @@ -52,8 +49,10 @@ module Paramod (B : Terms.Blob) = struct passives_w,passives_a ;; - let add_passive_clauses (passives_w,passives_a) new_clauses = - let new_clauses_w,new_clauses_a = List.fold_left add_passive_clause + let add_passive_clauses ?(no_weight=false) + (passives_w,passives_a) new_clauses = + let new_clauses_w,new_clauses_a = + List.fold_left (add_passive_clause ~no_weight) (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses in (WeightPassiveSet.union new_clauses_w passives_w, @@ -74,7 +73,7 @@ module Paramod (B : Terms.Blob) = struct (WeightPassiveSet.empty,AgePassiveSet.empty) ;; - let pick_min_passive use_age (passives_w,passives_a) = + let pick_min_passive ~use_age (passives_w,passives_a) = if use_age then AgePassiveSet.min_elt passives_a else WeightPassiveSet.min_elt passives_w ;; @@ -90,17 +89,17 @@ module Paramod (B : Terms.Blob) = struct let mk_goal (bag,maxvar) = mk_clause bag maxvar;; (* TODO : global age over facts and goals (without comparing weights) *) - let select passives g_passives = + let select ~use_age passives g_passives = if is_passive_set_empty passives then begin assert (not (is_passive_set_empty g_passives)); - let g_cl = pick_min_passive false g_passives in + let g_cl = pick_min_passive ~use_age:use_age g_passives in (true,snd g_cl,passives,remove_passive_clause g_passives g_cl) end - else let cl = pick_min_passive false passives in + else let cl = pick_min_passive ~use_age:use_age passives in if is_passive_set_empty g_passives then (false,snd cl,remove_passive_clause passives cl,g_passives) else - let g_cl = pick_min_passive false g_passives in + let g_cl = pick_min_passive ~use_age:use_age g_passives in if (fst cl <= fst g_cl) then (false,snd cl,remove_passive_clause passives cl,g_passives) else @@ -132,9 +131,6 @@ module Paramod (B : Terms.Blob) = struct * new'= demod A'' new * * P' = P + new' *) debug "Forward infer step..."; - debug "Selected and simplified"; - (* debug ("Fact after simplification :" - ^ Pp.pp_unit_clause current); *) let bag, maxvar, actives, new_clauses = Sup.infer_right bag maxvar current actives in @@ -143,7 +139,9 @@ module Paramod (B : Terms.Blob) = struct let bag, g_actives = List.fold_left (fun (bag,acc) c -> - match Sup.simplify_goal maxvar (snd actives) bag acc c with + match + Sup.simplify_goal ~no_demod:false maxvar (snd actives) bag acc c + with | None -> bag, acc | Some (bag,c) -> bag,c::acc) (bag,[]) g_actives @@ -162,37 +160,94 @@ module Paramod (B : Terms.Blob) = struct add_passive_clauses g_passives new_goals ;; - let rec given_clause bag maxvar nb_iter timeout actives passives g_actives g_passives = - (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag); - prerr_endline "Active table :"; - (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x)) - (fst actives)); *) - let nb_iter = nb_iter + 1 in - if nb_iter = max_nb_iter then - raise (Failure ("No iterations left !",bag,maxvar,nb_iter)); - if Unix.gettimeofday () > timeout then - raise (Failure ("Timeout !",bag,maxvar,nb_iter)); - - let rec aux_select passives g_passives = - let backward,current,passives,g_passives = select passives g_passives in + let rec given_clause ~noinfer + bag maxvar iterno max_steps timeout + actives passives g_actives g_passives + = + let iterno = iterno + 1 in + if iterno = max_steps then + raise (Failure ("No iterations left !",bag,maxvar,iterno)); + (* timeout check: gettimeofday called only if timeout set *) + if timeout <> None && + (match timeout with + | None -> assert false + | Some timeout -> Unix.gettimeofday () > timeout) then + begin + prerr_endline("Last chance: "^string_of_float (Unix.gettimeofday())); + given_clause ~noinfer:true bag maxvar iterno max_steps None + actives passives g_actives g_passives + (*raise (Failure ("Timeout !",bag,maxvar,iterno))*) + end + else + + let use_age = iterno mod 10 = 0 in + + let rec aux_select bag passives g_passives = + if noinfer && + is_passive_set_empty passives && + is_passive_set_empty g_passives then + begin + prerr_endline + ("Last chance: all is indexed " ^ string_of_float + (Unix.gettimeofday())); + let maxgoals = 100 in + List.fold_left + (fun (acc,i) x -> + if i < maxgoals then + ignore(Sup.simplify_goal ~no_demod:true + maxvar (snd actives) bag acc x) + else + (); + x::acc,i+1) + ([],0) g_actives; + raise (Failure (("Last chance: failed over " ^ + string_of_int maxgoals^ " goal " ^ + string_of_float (Unix.gettimeofday())),bag,maxvar,0)); + end; + let backward,current,passives,g_passives = + select ~use_age:false passives g_passives + in if backward then - match Sup.simplify_goal maxvar (snd actives) bag g_actives current with - | None -> aux_select passives g_passives - | Some x -> let bag,g_current = x in - backward_infer_step bag maxvar actives passives - g_actives g_passives g_current + match + if noinfer then Some (bag,current) + else + Sup.simplify_goal + ~no_demod:false maxvar (snd actives) bag g_actives current + with + | None -> aux_select bag passives g_passives + | Some (bag,g_current) -> + if noinfer then + let g_actives = g_current :: g_actives in + bag,maxvar,actives,passives,g_actives,g_passives + else + backward_infer_step bag maxvar actives passives + g_actives g_passives g_current else (* debug ("Selected fact : " ^ Pp.pp_unit_clause current); *) - match Sup.keep_simplified current actives bag maxvar with + match + if noinfer then bag, Some (current,actives) + else Sup.keep_simplified current actives bag maxvar with (* match Sup.one_pass_simplification current actives bag maxvar with*) - | None -> aux_select passives g_passives - | Some x -> let (current, bag, actives) = x in - forward_infer_step bag maxvar actives passives - g_actives g_passives current + | bag,None -> aux_select bag passives g_passives + | bag,Some (current,actives) -> + if noinfer then + let actives = + current::fst actives, + IDX.index_unit_clause (snd actives) current + in + bag,maxvar,actives,passives,g_actives,g_passives + else + forward_infer_step bag maxvar actives passives + g_actives g_passives current in + + (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag); + 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 passives g_passives + aux_select bag passives g_passives in debug (Printf.sprintf "Number of active goals : %d" @@ -205,28 +260,33 @@ module Paramod (B : Terms.Blob) = struct debug (Printf.sprintf "Number of passives : %d" (passive_set_cardinal passives)); - given_clause - bag maxvar nb_iter timeout actives passives g_actives g_passives + given_clause ~noinfer + bag maxvar iterno max_steps timeout + actives passives g_actives g_passives ;; - let paramod (bag,maxvar) ~g_passives ~passives = - let timeout = Unix.gettimeofday () +. amount_of_time in - let passives = add_passive_clauses passive_empty_set passives in - let g_passives = add_passive_clauses passive_empty_set g_passives in + let paramod ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives = + let initial_timestamp = Unix.gettimeofday () in + let passives = + add_passive_clauses ~no_weight:true passive_empty_set passives + in + let g_passives = + add_passive_clauses ~no_weight:true passive_empty_set g_passives + in let g_actives = [] in let actives = [], IDX.DT.empty in try - given_clause - bag maxvar 0 timeout actives passives g_actives g_passives + given_clause ~noinfer:false + bag maxvar 0 max_steps timeout actives passives g_actives g_passives with | Sup.Success (bag, _, (i,_,_,_)) -> let l = let rec traverse ongoal (accg,acce) i = match Terms.M.find i bag with - | (id,_,_,Terms.Exact _) -> + | (id,_,_,Terms.Exact _),_ -> if ongoal then [i],acce else if (List.mem i acce) then accg,acce else accg,acce@[i] - | (_,_,_,Terms.Step (_,i1,i2,_,_,_)) -> + | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),_ -> if (not ongoal) && (List.mem i acce) then accg,acce else let accg,acce = @@ -239,14 +299,16 @@ module Paramod (B : Terms.Blob) = struct in prerr_endline (Printf.sprintf "Found proof, %fs" - (Unix.gettimeofday() -. timeout +. amount_of_time)); + (Unix.gettimeofday() -. initial_timestamp)); + (* prerr_endline "Proof:"; - List.iter (fun x -> prerr_endline (string_of_int x); - prerr_endline (Pp.pp_unit_clause (Terms.M.find x bag))) l; + List.iter (fun x -> + prerr_endline (Pp.pp_unit_clause (fst(Terms.M.find x bag)))) l; + *) [ bag, i, l ] - | Failure (msg,_bag,_maxvar,nb_iter) -> + | Failure (msg,_bag,_maxvar,iterno) -> prerr_endline msg; - prerr_endline (Printf.sprintf "FAILURE in %d iterations" nb_iter); + prerr_endline (Printf.sprintf "FAILURE in %d iterations" iterno); [] ;;