From: Enrico Tassi Date: Thu, 18 Jun 2009 16:58:39 +0000 (+0000) Subject: proof patching! X-Git-Tag: make_still_working~3845 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=59eba9406321e2eeb1e4471dc490aa72ebf4ec47;p=helm.git proof patching! --- diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml index 1e5e67979..46710db21 100644 --- a/helm/software/components/ng_paramodulation/nCicBlob.ml +++ b/helm/software/components/ng_paramodulation/nCicBlob.ml @@ -197,7 +197,7 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct let amount = List.length seen in let lit,vl,proof = get_literal id in if not ongoal && id = mp then - ((*prerr_endline ("Reached meeting point, id=" ^ (string_of_int id));*) + ((*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*) assert (vl = []); NCic.LetIn ("clause_" ^ string_of_int id, extract amount vl lit, diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index b32a5b1be..b80bfc500 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -4,6 +4,7 @@ let debug s = let nparamod rdb metasenv subst context t table = let nb_iter = ref 200 in + let amount_of_time = 20.0 in let module C = struct let metasenv = metasenv let subst = subst @@ -29,6 +30,7 @@ let nparamod rdb metasenv subst context t table = let add_passive_clause passives cl = PassiveSet.add (Utils.mk_passive_clause cl) passives in + let timeout = Unix.gettimeofday () +. amount_of_time in (* TODO : fairness condition *) let select passives = if PassiveSet.is_empty passives then None @@ -43,7 +45,9 @@ let nparamod rdb metasenv subst context t table = prerr_endline "Active table :"; (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x)) (fst actives));*) - raise (Failure "Timeout !"); + raise (Failure "No iterations left !"); + if Unix.gettimeofday () > timeout then + raise (Failure "Timeout !"); @@ -90,8 +94,8 @@ let nparamod rdb metasenv subst context t table = | None -> assert false | Some (current, passives) -> debug ("Selected fact : " ^ Pp.pp_unit_clause current); - match Sup.keep_simplified current actives bag maxvar with - (* match Sup.one_pass_simplification current actives bag with *) +(* match Sup.keep_simplified current actives bag maxvar with *) + match Sup.one_pass_simplification current actives bag maxvar with | None -> aux_simplify passives | Some x -> x,passives in @@ -188,19 +192,32 @@ let nparamod rdb metasenv subst context t table = let gsteps = List.rev gsteps in esteps@(i::gsteps) in - debug "YES!"; - debug ("Meeting point : " ^ (string_of_int i)); - debug "Proof:"; - (*List.iter (fun x -> prerr_endline (string_of_int x); - prerr_endline (Pp.pp_unit_clause (Terms.M.find x bag))) l; *) + prerr_endline "YES!"; + prerr_endline ("Meeting point : " ^ (string_of_int i)); + 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; let proofterm = B.mk_proof bag i l in - prerr_endline (NCicPp.ppterm ~metasenv:C.metasenv - ~subst:C.subst ~context:C.context proofterm); + let metasenv, proofterm = + let rec aux k metasenv = function + | NCic.Meta _ as t -> metasenv, t + | NCic.Implicit _ -> + 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 + in + aux 0 metasenv proofterm + in + prerr_endline + ("prova generata: " ^ NCicPp.ppterm + ~metasenv ~subst ~context proofterm); let metasenv, subst, proofterm, _prooftype = NCicRefiner.typeof (rdb#set_coerc_db NCicCoercion.empty_db) - C.metasenv C.subst C.context proofterm None + metasenv subst context proofterm None in + prerr_endline "prova raffinata"; proofterm, metasenv, subst | Failure _ -> prerr_endline "FAILURE"; assert false ;;