From 2701c980f48541dd5e8317b5a5661b439ced8b29 Mon Sep 17 00:00:00 2001 From: denes Date: Fri, 26 Jun 2009 09:46:23 +0000 Subject: [PATCH] Implemented orphan murder test (clauses are not discarded for now) Re-enabled zero weight trick --- .../components/ng_paramodulation/paramod.ml | 28 ++++--- .../ng_paramodulation/superposition.ml | 73 +++++++++++++------ .../ng_paramodulation/superposition.mli | 4 +- 3 files changed, 70 insertions(+), 35 deletions(-) diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index d85c5627a..51bd67286 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 @@ -49,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, @@ -172,22 +174,22 @@ module Paramod (B : Terms.Blob) = struct let use_age = iterno mod 10 = 0 in - let rec aux_select passives g_passives = + let rec aux_select bag passives g_passives = 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 + | None -> aux_select bag passives g_passives + | Some (bag,g_current) -> 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 Sup.one_pass_simplification current actives bag maxvar with*) - | None -> aux_select passives g_passives - | Some x -> let (current, bag, actives) = x in + | bag,None -> aux_select bag passives g_passives + | bag,Some (current,actives) -> forward_infer_step bag maxvar actives passives g_actives g_passives current in @@ -198,7 +200,7 @@ module Paramod (B : Terms.Blob) = struct (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" @@ -218,8 +220,12 @@ module Paramod (B : Terms.Blob) = struct let paramod ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives = let initial_timestamp = Unix.gettimeofday () in - let passives = add_passive_clauses passive_empty_set passives in - let g_passives = add_passive_clauses passive_empty_set g_passives 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 diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 3957e925e..d058be253 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -22,9 +22,8 @@ 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 | [] -> None @@ -296,9 +295,30 @@ module Superposition (B : Terms.Blob) = | _,_ -> None ;; + let rec orphan_murder bag acc i = + match Terms.M.find i bag with + | (_,_,_,Terms.Exact _),discarded -> (discarded,acc) + | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),true -> (true,acc) + | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),false -> + if (List.mem i acc) then (false,acc) + else match orphan_murder bag acc i1 with + | (true,acc) -> (true,acc) + | (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 = - let bag, clause = demodulate bag clause table in + if is_identity_clause ~unify:false clause then bag,None + (* else if orphan_murder bag clause then bag,None *) + else let bag, clause = demodulate bag clause table in if is_identity_clause ~unify:false clause then bag,None else match is_subsumed ~unify:false bag maxvar clause table with @@ -306,21 +326,29 @@ module Superposition (B : Terms.Blob) = | Some _ -> bag, None ;; + let simplify table maxvar bag clause = + match simplify table maxvar bag clause with + | 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 - | bag,None -> None (* new_clause has been discarded *) + | bag,None -> bag,None (* new_clause has been discarded *) | bag,(Some clause) -> let ctable = IDX.index_unit_clause IDX.DT.empty clause in let bag, alist, atable = List.fold_left - (fun (bag, alist, atable as acc) c -> + (fun (bag, alist, atable) c -> match simplify ctable maxvar bag c with - |bag,None -> acc (* an active clause as been discarded *) + |bag,None -> (bag,alist,atable) + (* an active clause as been discarded *) |bag,Some c1 -> bag, c :: alist, IDX.index_unit_clause atable c) (bag,[],IDX.DT.empty) alist in - Some (clause, bag, (alist,atable)) + bag, Some (clause, (alist,atable)) ;; let simplification_step ~new_cl cl (alist,atable) bag maxvar new_clause = @@ -332,16 +360,17 @@ module Superposition (B : Terms.Blob) = * - actives and cl if new_clause is not cl * * - only actives otherwise *) match simplify atable1 maxvar bag new_clause with - | bag,None -> (Some cl, None) (* new_clause has been discarded *) + | bag,None -> bag,(Some cl, None) (* new_clause has been discarded *) | bag,Some clause -> (* Simplification of each active clause with clause * * which is the simplified form of new_clause *) let ctable = IDX.index_unit_clause IDX.DT.empty clause in let bag, newa, alist, atable = List.fold_left - (fun (bag, newa, alist, atable as acc) c -> + (fun (bag, newa, alist, atable) c -> match simplify ctable maxvar bag c with - |bag,None -> acc (* an active clause as been discarded *) + |bag,None -> (bag, newa, alist, atable) + (* an active clause as been discarded *) |bag,Some c1 -> if (c1 == c) then bag, newa, c :: alist, @@ -351,37 +380,37 @@ module Superposition (B : Terms.Blob) = (bag,[],[],IDX.DT.empty) alist in if new_cl then - (Some cl, Some (clause, (alist,atable), newa, bag)) + bag, (Some cl, Some (clause, (alist,atable), newa)) else (* if new_clause is not cl, we simplify cl with clause *) match simplify ctable maxvar bag cl with | bag,None -> (* cl has been discarded *) - (None, Some (clause, (alist,atable), newa, bag)) + bag,(None, Some (clause, (alist,atable), newa)) | bag,Some cl1 -> - (Some cl1, Some (clause, (alist,atable), newa, bag)) + bag,(Some cl1, Some (clause, (alist,atable), newa)) ;; let keep_simplified cl (alist,atable) bag maxvar = let rec keep_simplified_aux ~new_cl cl (alist,atable) bag newc = if new_cl then match simplification_step ~new_cl cl (alist,atable) bag maxvar cl with - | (None, _) -> assert false - | (Some _, None) -> None - | (Some _, Some (clause, (alist,atable), newa, bag)) -> + | _,(None, _) -> assert false + | bag,(Some _, None) -> bag,None + | bag,(Some _, Some (clause, (alist,atable), newa)) -> keep_simplified_aux ~new_cl:(cl!=clause) clause (alist,atable) bag (newa@newc) else match newc with - | [] -> Some (cl, bag, (alist,atable)) + | [] -> bag, Some (cl, (alist,atable)) | hd::tl -> match simplification_step ~new_cl cl (alist,atable) bag maxvar hd with - | (None,None) -> assert false - | (Some _,None) -> + | _,(None,None) -> assert false + | bag,(Some _,None) -> keep_simplified_aux ~new_cl cl (alist,atable) bag tl - | (None, Some _) -> None - | (Some cl1, Some (clause, (alist,atable), newa, bag)) -> + | bag,(None, Some _) -> bag,None + | bag,(Some cl1, Some (clause, (alist,atable), newa)) -> let alist,atable = (clause::alist, IDX.index_unit_clause atable clause) in diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli index e3e2f8b9f..a7badaba4 100644 --- a/helm/software/components/ng_paramodulation/superposition.mli +++ b/helm/software/components/ng_paramodulation/superposition.mli @@ -58,7 +58,7 @@ module Superposition (B : Terms.Blob) : Index.Index(B).active_set -> B.t Terms.bag -> int -> - (B.t Terms.unit_clause * B.t Terms.bag * Index.Index(B).active_set) option + B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option val keep_simplified: @@ -66,7 +66,7 @@ module Superposition (B : Terms.Blob) : Index.Index(B).active_set -> B.t Terms.bag -> int -> - (B.t Terms.unit_clause * B.t Terms.bag * Index.Index(B).active_set) option + B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option end -- 2.39.2