From f49a2aa0634549cc4fb44067225514ba7de46fec Mon Sep 17 00:00:00 2001 From: denes Date: Mon, 29 Jun 2009 10:41:50 +0000 Subject: [PATCH] Implemented orphan murdering technique --- .../ng_paramodulation/nCicParamod.ml | 4 +-- .../components/ng_paramodulation/paramod.ml | 28 ++++++++++++++++--- .../components/ng_paramodulation/pp.ml | 4 ++- .../ng_paramodulation/superposition.ml | 16 +++++++---- .../ng_paramodulation/superposition.mli | 6 ++++ 5 files changed, 46 insertions(+), 12 deletions(-) diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml index 89660143d..6c1aa695e 100644 --- a/helm/software/components/ng_paramodulation/nCicParamod.ml +++ b/helm/software/components/ng_paramodulation/nCicParamod.ml @@ -38,9 +38,9 @@ let nparamod rdb metasenv subst context t table = in List.map (fun (bag,i,l) -> - List.iter (fun x -> + (* List.iter (fun x -> print_endline (Pp.pp_unit_clause ~margin:max_int - (fst(Terms.M.find x bag)))) l; + (fst(Terms.M.find x bag)))) l; *) let stamp = Unix.gettimeofday () in let proofterm = NCicProof.mk_proof bag i l in prerr_endline (Printf.sprintf "Got proof term in %fs" diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 32eff6826..a92bf5dcc 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -224,12 +224,29 @@ module Paramod (B : Terms.Blob) = struct g_actives g_passives g_current else (* debug ("Selected fact : " ^ Pp.pp_unit_clause current); *) + (*let is_orphan = Sup.orphan_murder bag (fst actives) current in*) 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*) + else if Sup.orphan_murder bag (fst actives) current then + let (id,_,_,_) = current in + let bag = Terms.M.add id (current,true) bag in + bag, None + 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) -> +(* if is_orphan then prerr_endline + ("WRONG discarded: " ^ (Pp.pp_unit_clause current)); + List.iter (fun x -> + prerr_endline (Pp.pp_unit_clause x)) + (fst actives);*) + +(* List.iter (fun (id,_,_,_) -> let (cl,d) = + Terms.M.find id bag in + if d then prerr_endline + ("WRONG discarded: " ^ (Pp.pp_unit_clause cl))) + (current::fst actives);*) if noinfer then let actives = current::fst actives, @@ -241,8 +258,8 @@ module Paramod (B : Terms.Blob) = struct g_actives g_passives current in - (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag); - prerr_endline "Active table :"; + + (*prerr_endline "Active table :"; (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x)) (fst actives)); *) @@ -297,6 +314,9 @@ module Paramod (B : Terms.Blob) = struct let gsteps,esteps = traverse true ([],[]) i in (List.rev esteps)@gsteps in +(* List.iter (fun id -> let (cl,d) = + Terms.M.find id bag in + if d then prerr_endline (Pp.pp_unit_clause cl)) l;*) prerr_endline (Printf.sprintf "Found proof, %fs" (Unix.gettimeofday() -. initial_timestamp)); diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml index e8035da65..cb971ea74 100644 --- a/helm/software/components/ng_paramodulation/pp.ml +++ b/helm/software/components/ng_paramodulation/pp.ml @@ -123,7 +123,9 @@ let pp_unit_clause ~formatter:f c = let pp_bag ~formatter:f bag = Format.fprintf f "@["; Terms.M.iter - (fun _ (c,_) -> pp_unit_clause ~formatter:f c;Format.fprintf f "@;") bag; + (fun _ (c,d) -> pp_unit_clause ~formatter:f c; + if d then Format.fprintf f " (discarded)@;" + else Format.fprintf f "@;") bag; Format.fprintf f "@]" ;; diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 9ccd934e1..8070b4b5d 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -22,7 +22,7 @@ module Superposition (B : Terms.Blob) = exception Success of B.t Terms.bag * int * B.t Terms.unit_clause -(* let debug s = prerr_endline s;;*) + let debug s = prerr_endline s;; let debug _ = ();; let rec list_first f = function @@ -315,16 +315,17 @@ module Superposition (B : Terms.Blob) = if res then res,acc else res,i::acc ;; - let orphan_murder bag cl = + let orphan_murder bag actives cl = let (id,_,_,_) = cl in - let (res,_) = orphan_murder bag [] id in + let actives = List.map (fun (i,_,_,_) -> i) actives in + let (res,_) = orphan_murder bag actives id in if res then debug "Orphan murdered"; res ;; (* demodulate and check for subsumption *) let simplify table maxvar bag clause = if is_identity_clause ~unify:false clause then bag,None - (* else if orphan_murder bag clause then bag,None *) + (* else if orphan_murder bag actives clause then bag,None *) else let bag, clause = demodulate bag clause table in if is_identity_clause ~unify:false clause then bag,None else @@ -338,6 +339,10 @@ 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 (id,_,_,_) = clause in + if orphan_murder bag clause then + Terms.M.add id (clause,true) bag, Some clause + else bag, Some clause*) ;; let one_pass_simplification new_clause (alist,atable) bag maxvar = @@ -366,7 +371,8 @@ module Superposition (B : Terms.Blob) = (* Simplification of new_clause with : * * - actives and cl if new_clause is not cl * * - only actives otherwise *) - match simplify atable1 maxvar bag new_clause with + match + simplify atable1 maxvar bag new_clause with | bag,None -> bag,(Some cl, None) (* new_clause has been discarded *) | bag,Some clause -> (* Simplification of each active clause with clause * diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli index 52011c3e8..149bbb048 100644 --- a/helm/software/components/ng_paramodulation/superposition.mli +++ b/helm/software/components/ng_paramodulation/superposition.mli @@ -69,5 +69,11 @@ module Superposition (B : Terms.Blob) : int -> B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option + val orphan_murder: + B.t Terms.bag -> + B.t Terms.unit_clause list -> + B.t Terms.unit_clause -> + bool + end -- 2.39.2