From 8bb849acb32ab6180be4ea23dbb9fe35d7300ceb Mon Sep 17 00:00:00 2001 From: denes Date: Fri, 12 Jun 2009 16:16:11 +0000 Subject: [PATCH] Implemented keep_simplified. If a candidate for forward inference is discarded, another is selected --- .../components/ng_paramodulation/paramod.ml | 135 ++++++------------ .../ng_paramodulation/superposition.ml | 86 ++++++++--- .../ng_paramodulation/superposition.mli | 8 +- 3 files changed, 111 insertions(+), 118 deletions(-) diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 1f621ce05..b301e8005 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -1,70 +1,9 @@ -(*let nparamod metasenv subst context t table = - prerr_endline "========================================"; - let module C = struct - let metasenv = metasenv - let subst = subst - let context = context - end - in - let module B = NCicBlob.NCicBlob(C) in - let module Pp = Pp.Pp (B) in - let module FU = FoUnif.Founif(B) in - let module IDX = Index.Index(B) in - let module Sup = Superposition.Superposition(B) in - let module Utils = FoUtils.Utils(B) in*) -(* - let test_unification _ = function - | Terms.Node [_; _; lhs; rhs] -> - prerr_endline "Unification test :"; - prerr_endline (Pp.pp_foterm lhs); - prerr_endline (Pp.pp_foterm rhs); - FU.unification [] [] lhs rhs - | _ -> assert false - in - let subst,vars = test_unification [] res in - prerr_endline "Result :"; - prerr_endline (Pp.pp_foterm res); - prerr_endline "Substitution :"; - prerr_endline (Pp.pp_substitution subst) -*) -(* - - let mk_clause maxvar t = - let ty = B.embed t in - let proof = B.embed (NCic.Rel ~-1) in - Utils.mk_unit_clause maxvar ty proof - in - let clause, maxvar = mk_clause 0 t in - prerr_endline "Input clause :"; - prerr_endline (Pp.pp_unit_clause clause); - let bag = Utils.empty_bag in - let active_clauses, maxvar = - List.fold_left - (fun (cl,maxvar) t -> - let c, m = mk_clause maxvar t in - c::cl, m) - ([],maxvar) table - in - let table = - List.fold_left IDX.index_unit_clause IDX.DT.empty active_clauses - in - prerr_endline "Active table:"; - List.iter (fun uc -> prerr_endline (Pp.pp_unit_clause uc)) active_clauses; - let bag, maxvar, _, newclauses = - Sup.infer_right bag maxvar clause (active_clauses, table) - in - prerr_endline "Output clauses :"; - List.iter (fun c -> prerr_endline (Pp.pp_unit_clause c)) newclauses; - (* prerr_endline "Proofs: "; - prerr_endline (Pp.pp_bag bag); *) - prerr_endline "========================================"; -;; -*) -let debug s = - prerr_endline s +let debug s = () +(* prerr_endline s *) ;; let nparamod metasenv subst context t table = + let nb_iter = ref 100 in prerr_endline "========================================"; let module C = struct let metasenv = metasenv @@ -97,8 +36,11 @@ let nparamod metasenv subst context t table = else let cl = PassiveSet.min_elt passives in Some (snd cl,PassiveSet.remove cl passives) in - let rec given_clause bag maxvar actives passives g_actives g_passives = + let rec given_clause bag maxvar actives + passives g_actives g_passives = + decr nb_iter; if !nb_iter = 0 then raise (Failure "Timeout !"); + (* keep goals demodulated w.r.t. actives and check if solved *) (* we may move this at the end of infer_right *) let bag, g_actives = @@ -147,34 +89,38 @@ let nparamod metasenv subst context t table = * P' = P + new' *) debug "Forward infer step..."; let bag, maxvar, actives, passives, g_passives = - match select passives with - | None -> bag, maxvar, actives, passives, g_passives - | Some (current, passives) -> - debug ("Selected fact : " ^ Pp.pp_unit_clause current); - match Sup.simplify (snd actives) bag current with - | None -> debug ("Discarded fact"); - bag, maxvar, actives, passives, g_passives - | Some (bag, current) -> - debug ("Fact after simplification :" ^ Pp.pp_unit_clause current); - let bag, maxvar, actives, new_clauses = - Sup.infer_right bag maxvar current actives - in - let ctable = IDX.index_unit_clause IDX.DT.empty current in - let bag, maxvar, new_goals = - List.fold_left - (fun (bag,m,acc) g -> - let bag, m, ng = Sup.infer_left bag maxvar g - ([current],ctable) in - 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 - bag, maxvar, actives, - PassiveSet.union new_clauses passives, - PassiveSet.union new_goals g_passives + let rec aux_simplify passives = + match select passives with + | None -> assert false + | Some (current, passives) -> + debug ("Selected fact : " ^ Pp.pp_unit_clause current); + match Sup.keep_simplified current actives bag with + | None -> aux_simplify passives + | Some x -> x + in + let (current, bag, actives) = aux_simplify passives + in + debug ("Fact after simplification :" + ^ Pp.pp_unit_clause current); + let bag, maxvar, actives, new_clauses = + Sup.infer_right bag maxvar current actives + in + let ctable = IDX.index_unit_clause IDX.DT.empty current in + let bag, maxvar, new_goals = + List.fold_left + (fun (bag,m,acc) g -> + let bag, m, ng = Sup.infer_left bag maxvar g + ([current],ctable) in + 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 + bag, maxvar, actives, + PassiveSet.union new_clauses passives, + PassiveSet.union new_goals g_passives in prerr_endline (Printf.sprintf "Number of actives : %d" (List.length (fst actives))); @@ -204,6 +150,7 @@ let nparamod metasenv subst context t table = try given_clause bag maxvar actives passives g_actives g_passives with Sup.Success (bag, _, mp) -> prerr_endline "YES!"; - prerr_endline "Meeting point :"; prerr_endline (Pp.pp_unit_clause mp); + prerr_endline "Meeting point :"; prerr_endline (Pp.pp_unit_clause mp) (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag) *) + | Failure _ -> prerr_endline "FAILURE" ;; diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 4142a35b6..046799a77 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -191,27 +191,67 @@ module Superposition (B : Terms.Blob) = else Some (bag, clause) ;; - let rec keep_simplified (alist,atable) bag newc = - match newc with - | [] -> bag, (alist,atable) - | hd::tl -> - (match simplify atable bag hd with - | None -> keep_simplified (alist,atable) bag tl - | Some (bag, 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) c -> - let bag, c1 = demodulate bag c ctable in - if (c1 == c) then - bag, newa, c :: alist, IDX.index_unit_clause atable c - else - bag, c :: newa, alist, atable) - (bag,[],[],IDX.DT.empty) alist - in - keep_simplified (alist, atable) bag newa) + let simplification_step ~new_cl cl (alist,atable) bag new_clause = + let atable1 = + if new_cl then atable else + IDX.index_unit_clause atable cl + in + match simplify atable1 bag new_clause with + | None -> (Some cl, None) + | Some (bag, 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 -> + match simplify ctable bag c with + |None -> acc + |Some (bag, c1) -> + if (c1 == c) then + bag, newa, c :: alist, + IDX.index_unit_clause atable c + else + bag, c1 :: newa, alist, atable) + (bag,[],[],IDX.DT.empty) alist + in + if new_cl then + (Some cl, Some (clause, (alist,atable), newa, bag)) + else + match simplify ctable bag cl with + | None -> + (None, Some (clause, (alist,atable), newa, bag)) + | Some (bag,cl1) -> + (Some cl1, Some (clause, (alist,atable), newa, bag)) ;; + let keep_simplified cl (alist,atable) bag = + 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 cl with + | (None, _) -> assert false + | (Some _, None) -> None + | (Some _, Some (clause, (alist,atable), newa, bag)) -> + keep_simplified_aux ~new_cl:(cl!=clause) clause (alist,atable) + bag (newa@newc) + else + match newc with + | [] -> Some (cl, bag, (alist,atable)) + | hd::tl -> + match simplification_step ~new_cl cl + (alist,atable) bag hd with + | (None,None) -> assert false + | (Some _,None) -> + keep_simplified_aux ~new_cl cl (alist,atable) bag tl + | (None, Some _) -> None + | (Some cl1, Some (clause, (alist,atable), newa, bag)) -> + let alist,atable = + (clause::alist, IDX.index_unit_clause atable clause) + in + keep_simplified_aux ~new_cl:(cl!=cl1) cl1 (alist,atable) + bag (newa@tl) + in + keep_simplified_aux ~new_cl:true cl (alist,atable) bag [] + ;; + (* this is like simplify but raises Success *) let simplify_goal maxvar table bag clause = let bag, clause = demodulate bag clause table in @@ -306,14 +346,16 @@ module Superposition (B : Terms.Blob) = (* the current equation is normal w.r.t. demodulation with atable * (and is not the identity) *) let infer_right bag maxvar current (alist,atable) = - (* We demodulate actives clause with current *) + (* We demodulate actives clause with current until all * + * active clauses are reduced w.r.t each other *) + (* let bag, (alist,atable) = keep_simplified (alist,atable) bag [current] in *) let ctable = IDX.index_unit_clause IDX.DT.empty current in - let bag, (alist, atable) = + (* let bag, (alist, atable) = let bag, alist = HExtlib.filter_map_acc (simplify ctable) bag alist in bag, (alist, List.fold_left IDX.index_unit_clause IDX.DT.empty alist) - in + in*) debug "Simplified active clauses with fact"; (* We superpose active clauses with current *) let bag, maxvar, new_clauses = diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli index 23477be1a..d7efb1b42 100644 --- a/helm/software/components/ng_paramodulation/superposition.mli +++ b/helm/software/components/ng_paramodulation/superposition.mli @@ -51,7 +51,11 @@ module Superposition (B : Terms.Blob) : B.t Terms.unit_clause -> B.t Terms.bag * B.t Terms.unit_clause - end - + val keep_simplified: + B.t Terms.unit_clause -> + Index.Index(B).active_set -> + B.t Terms.bag -> + (B.t Terms.unit_clause * B.t Terms.bag * Index.Index(B).active_set) option + end -- 2.39.2