X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=98bfdde6566deff12d40c57653e3c316935f03c6;hb=2e11e475e62e4f3d6872554fb504d77bf2327b7d;hp=73e9809d3ae2d0569761aaac9b00d90bffcdeeae;hpb=e34ae96116185c15fc3fdc62065122e5dd1dd338;p=helm.git diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 73e9809d3..98bfdde65 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -1,7 +1,5 @@ -(* LOOPING : COL057-1.ma *) - let debug s = - () (* prerr_endline s *) + () (*prerr_endline s*) ;; let nparamod rdb metasenv subst context t table = @@ -21,55 +19,89 @@ let nparamod rdb metasenv subst context t table = let module Sup = Superposition.Superposition(B) in let module Utils = FoUtils.Utils(B) in - let module OrderedPassives = + let module WeightOrderedPassives = + struct + type t = B.t Terms.passive_clause + + let compare = Utils.compare_passive_clauses_weight + end + in + let module AgeOrderedPassives = struct type t = B.t Terms.passive_clause - let compare = Utils.compare_passive_clauses + let compare = Utils.compare_passive_clauses_age end in - let module PassiveSet = Set.Make(OrderedPassives) + let module WeightPassiveSet = Set.Make(WeightOrderedPassives) in + let module AgePassiveSet = Set.Make(AgeOrderedPassives) in + 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 + in + let remove_passive_clause (passives_w,passives_a) cl = + let passives_w = WeightPassiveSet.remove cl passives_w in + let passives_a = AgePassiveSet.remove cl passives_a in + passives_w,passives_a + in + let add_passive_clauses (passives_w,passives_a) new_clauses = + let new_clauses_w,new_clauses_a = List.fold_left add_passive_clause + (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses + in + (WeightPassiveSet.union new_clauses_w passives_w, + AgePassiveSet.union new_clauses_a passives_a) + in + let is_passive_set_empty (passives_w,passives_a) = + if (WeightPassiveSet.is_empty passives_w) then begin + assert (AgePassiveSet.is_empty passives_a); true + end else begin + assert (not (AgePassiveSet.is_empty passives_a)); false + end + in + let passive_set_cardinal (passives_w,_) = + WeightPassiveSet.cardinal passives_w in - let add_passive_clause passives cl = - PassiveSet.add (Utils.mk_passive_clause cl) passives + let passive_singleton cl = + (WeightPassiveSet.singleton cl,AgePassiveSet.singleton cl) + in + let passive_empty_set = + (WeightPassiveSet.empty,AgePassiveSet.empty) + in + 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 in let timeout = Unix.gettimeofday () +. amount_of_time in - (* TODO : fairness condition *) + (* TODO : global age over facts and goals (without comparing weights) *) let select passives g_passives = - if PassiveSet.is_empty passives then begin - assert (not (PassiveSet.is_empty g_passives)); - let g_cl = PassiveSet.min_elt g_passives in - (true,snd g_cl,passives,PassiveSet.remove g_cl 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 + (true,snd g_cl,passives,remove_passive_clause g_passives g_cl) end - else let cl = PassiveSet.min_elt passives in - if PassiveSet.is_empty g_passives then - (false,snd cl,PassiveSet.remove cl passives,g_passives) + else let cl = pick_min_passive false passives in + if is_passive_set_empty g_passives then + (false,snd cl,remove_passive_clause passives cl,g_passives) else - let g_cl = PassiveSet.min_elt g_passives in + let g_cl = pick_min_passive false g_passives in if (fst cl <= fst g_cl) then - (false,snd cl,PassiveSet.remove cl passives,g_passives) + (false,snd cl,remove_passive_clause passives cl,g_passives) else - (true,snd g_cl,passives,PassiveSet.remove g_cl g_passives) + (true,snd g_cl,passives,remove_passive_clause g_passives g_cl) in - let backward_infer_step bag maxvar actives passives g_actives g_passives g_current = + let backward_infer_step bag maxvar actives passives + g_actives g_passives g_current = (* superposition left, simplifications on goals *) debug "infer_left step..."; - debug ("Selected goal : " ^ Pp.pp_unit_clause g_current); - let bag, g_current = - Sup.simplify_goal maxvar (snd actives) bag g_current - in - debug "Simplified goal"; let bag, maxvar, new_goals = Sup.infer_left bag maxvar g_current actives in debug "Performed infer_left step"; - let new_goals = List.fold_left add_passive_clause - PassiveSet.empty new_goals - in - bag, maxvar, actives, passives, g_current::g_actives, - (PassiveSet.union new_goals g_passives) + bag, maxvar, actives, passives, g_current::g_actives, + (add_passive_clauses g_passives new_goals) in let forward_infer_step bag maxvar actives passives g_actives @@ -92,18 +124,15 @@ let nparamod rdb metasenv subst context t table = Sup.infer_right bag maxvar current actives in debug "Demodulating goals with actives..."; - debug ("Current : " ^ (Pp.pp_unit_clause current)); - debug ("Active goal : " ^ (Pp.pp_unit_clause (List.hd g_actives))); (* keep goals demodulated w.r.t. actives and check if solved *) let bag, g_actives = List.fold_left (fun (bag,acc) c -> - let bag, c = Sup.simplify_goal maxvar (snd actives) bag c in - bag, c::acc) + match Sup.simplify_goal maxvar (snd actives) bag acc c with + | None -> bag, acc + | Some (bag,c) -> bag,c::acc) (bag,[]) g_actives in - debug (Pp.pp_unit_clause current); - debug (Pp.pp_unit_clause (List.hd g_actives)); let ctable = IDX.index_unit_clause IDX.DT.empty current in let bag, maxvar, new_goals = List.fold_left @@ -113,15 +142,9 @@ let nparamod rdb metasenv subst context t table = bag,m,ng@acc) (bag,maxvar,[]) g_actives in - let new_clauses = List.fold_left add_passive_clause - PassiveSet.empty new_clauses in - let new_goals = List.fold_left add_passive_clause - PassiveSet.empty new_goals in - debug (string_of_int (PassiveSet.cardinal new_goals)); - debug (string_of_int (PassiveSet.cardinal g_passives)); bag, maxvar, actives, - PassiveSet.union new_clauses passives, g_actives, - PassiveSet.union new_goals g_passives + add_passive_clauses passives new_clauses, g_actives, + add_passive_clauses g_passives new_goals in let rec given_clause bag maxvar actives passives g_actives g_passives = @@ -138,8 +161,11 @@ let nparamod rdb metasenv subst context t table = let rec aux_select passives g_passives = let backward,current,passives,g_passives = select passives g_passives in if backward then - backward_infer_step bag maxvar actives passives - g_actives g_passives current + 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 else (* debug ("Selected fact : " ^ Pp.pp_unit_clause current); *) match Sup.keep_simplified current actives bag maxvar with @@ -153,22 +179,21 @@ let nparamod rdb metasenv subst context t table = let bag,maxvar,actives,passives,g_actives,g_passives = aux_select passives g_passives in - assert (PassiveSet.cardinal g_passives < 2); debug (Printf.sprintf "Number of active goals : %d" (List.length g_actives)); debug (Printf.sprintf "Number of passive goals : %d" - (PassiveSet.cardinal g_passives)); + (passive_set_cardinal g_passives)); debug (Printf.sprintf "Number of actives : %d" (List.length (fst actives))); debug (Printf.sprintf "Number of passives : %d" - (PassiveSet.cardinal passives)); + (passive_set_cardinal passives)); given_clause bag maxvar actives passives g_actives g_passives in - let mk_clause bag maxvar (t,ty) = + let mk_clause ?(no_weight=false) bag maxvar (t,ty) = let (proof,ty) = B.saturate t ty in let c, maxvar = Utils.mk_unit_clause maxvar ty proof in let bag, c = Utils.add_to_bag bag c in @@ -176,13 +201,15 @@ let nparamod rdb metasenv subst context t table = in let bag, maxvar, goal = mk_clause Terms.M.empty 0 t in let g_actives = [] in - let g_passives = PassiveSet.singleton (Utils.mk_passive_clause goal) in + let g_passives = + passive_singleton (0,goal) + in let passives, bag, maxvar = List.fold_left (fun (cl, bag, maxvar) t -> let bag, maxvar, c = mk_clause bag maxvar t in (add_passive_clause cl c), bag, maxvar) - (PassiveSet.empty, bag, maxvar) table + (passive_empty_set, bag, maxvar) table in let actives = [], IDX.DT.empty in try given_clause bag maxvar actives passives g_actives g_passives @@ -221,7 +248,7 @@ let nparamod rdb metasenv subst context t table = let metasenv,i,_,_=NCicMetaSubst.mk_meta metasenv context `Term in metasenv, NCic.Meta (i,(k,NCic.Irl (List.length context))) | t -> NCicUntrusted.map_term_fold_a - (fun _ k -> k+1) k aux metasenv t + (fun _ k -> k+1) k aux metasenv t in aux 0 metasenv proofterm in @@ -231,6 +258,8 @@ let nparamod rdb metasenv subst context t table = metasenv subst context proofterm None in proofterm, metasenv, subst - | Failure _ -> prerr_endline + | Failure s -> + prerr_endline s; + prerr_endline (Printf.sprintf "FAILURE in %d iterations" !nb_iter); assert false ;;