From e7d2bbd23d9cc06232afd4c9b50d09b95abfbefa Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 26 Jun 2009 15:38:56 +0000 Subject: [PATCH] attempt to run a last chance procedure after the timeout --- .../components/ng_paramodulation/paramod.ml | 79 +++++++++++++++---- .../ng_paramodulation/superposition.ml | 29 ++++--- .../ng_paramodulation/superposition.mli | 3 +- 3 files changed, 79 insertions(+), 32 deletions(-) diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 51bd67286..32eff6826 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -11,7 +11,7 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) -(* let debug s = prerr_endline s ;;*) +let debug s = prerr_endline s ;; let debug _ = ();; module Paramod (B : Terms.Blob) = struct @@ -139,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 @@ -158,7 +160,7 @@ module Paramod (B : Terms.Blob) = struct add_passive_clauses g_passives new_goals ;; - let rec given_clause + let rec given_clause ~noinfer bag maxvar iterno max_steps timeout actives passives g_actives g_passives = @@ -166,32 +168,77 @@ module Paramod (B : Terms.Blob) = struct if iterno = max_steps then raise (Failure ("No iterations left !",bag,maxvar,iterno)); (* timeout check: gettimeofday called only if timeout set *) - (match timeout with - | None -> () - | Some timeout -> - if Unix.gettimeofday () > timeout then - raise (Failure ("Timeout !",bag,maxvar,iterno))); + 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 + 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) -> - backward_infer_step bag maxvar actives passives - g_actives g_passives 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*) | bag,None -> aux_select bag passives g_passives | bag,Some (current,actives) -> - forward_infer_step bag maxvar actives passives - g_actives g_passives current + 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); @@ -213,7 +260,7 @@ module Paramod (B : Terms.Blob) = struct debug (Printf.sprintf "Number of passives : %d" (passive_set_cardinal passives)); - given_clause + given_clause ~noinfer bag maxvar iterno max_steps timeout actives passives g_actives g_passives ;; @@ -229,7 +276,7 @@ module Paramod (B : Terms.Blob) = struct let g_actives = [] in let actives = [], IDX.DT.empty in try - given_clause + given_clause ~noinfer:false bag maxvar 0 max_steps timeout actives passives g_actives g_passives with | Sup.Success (bag, _, (i,_,_,_)) -> diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index c1c0612b1..9ccd934e1 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -313,13 +313,13 @@ module Superposition (B : Terms.Blob) = | (false,acc) -> let (res,acc) = orphan_murder bag acc i2 in if res then res,acc else res,i::acc -;; + ;; let orphan_murder bag cl = let (id,_,_,_) = cl in let (res,_) = orphan_murder bag [] id in if res then debug "Orphan murdered"; res -;; + ;; (* demodulate and check for subsumption *) let simplify table maxvar bag clause = @@ -338,7 +338,7 @@ module Superposition (B : Terms.Blob) = | bag, None -> let (id,_,_,_) = clause in Terms.M.add id (clause,true) bag, None | bag, Some clause -> bag, Some clause -;; + ;; let one_pass_simplification new_clause (alist,atable) bag maxvar = match simplify atable maxvar bag new_clause with @@ -439,11 +439,13 @@ module Superposition (B : Terms.Blob) = ;; (* this is like simplify but raises Success *) - let simplify_goal maxvar table bag g_actives clause = - let bag, clause = demodulate bag clause table in + let simplify_goal ~no_demod maxvar table bag g_actives clause = + let bag, clause = + if no_demod then bag, clause else demodulate bag clause table + in + if List.exists (are_alpha_eq clause) g_actives then None else if (is_identity_clause ~unify:true clause) then raise (Success (bag, maxvar, clause)) - else let (id,lit,vl,_) = clause in let l,r,ty = @@ -453,20 +455,17 @@ module Superposition (B : Terms.Blob) = in match deep_eq ~unify:true l r ty [] (fun x -> x) (fun x -> x) table (Some(bag,maxvar,clause,Subst.id_subst)) with - | None -> - if List.exists (are_alpha_eq clause) g_actives then None - else Some (bag, clause) + | None -> Some (bag,clause) | Some (bag,maxvar,cl,subst) -> prerr_endline "Goal subsumed"; raise (Success (bag,maxvar,cl)) - (* +(* else match is_subsumed ~unify:true bag maxvar clause table with - | None -> - if List.exists (are_alpha_eq clause) g_actives then None - else Some (bag, clause) + | None -> Some (bag, clause) | Some ((bag,maxvar),c) -> prerr_endline "Goal subsumed"; - raise (Success (bag,maxvar,c))*) + raise (Success (bag,maxvar,c)) +*) ;; (* =================== inference ===================== *) @@ -593,7 +592,7 @@ module Superposition (B : Terms.Blob) = let bag, new_goals = List.fold_left (fun (bag, acc) g -> - match simplify_goal maxvar atable bag [] g with + match simplify_goal ~no_demod:false maxvar atable bag [] g with | None -> assert false | Some (bag,g) -> bag,g::acc) (bag, []) new_goals diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli index a7badaba4..52011c3e8 100644 --- a/helm/software/components/ng_paramodulation/superposition.mli +++ b/helm/software/components/ng_paramodulation/superposition.mli @@ -45,7 +45,8 @@ module Superposition (B : Terms.Blob) : B.t Terms.bag * (B.t Terms.unit_clause option) (* may raise success *) - val simplify_goal : + val simplify_goal : + no_demod:bool -> int -> Index.Index(B).DT.t -> B.t Terms.bag -> -- 2.39.2