From: Enrico Tassi Date: Wed, 10 Jun 2009 13:38:08 +0000 (+0000) Subject: right inference step completed X-Git-Tag: make_still_working~3887 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a99b3bf44964a6a3d56d752efbdc2c962ce24d08;p=helm.git right inference step completed --- diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml index 624b6c99c..76e9735be 100644 --- a/helm/software/components/ng_paramodulation/foUtils.ml +++ b/helm/software/components/ng_paramodulation/foUtils.ml @@ -20,6 +20,11 @@ let rec lexicograph f l1 l2 = | [],_ -> ~-1 | _,[] -> 1 ;; + +let mk_id = + let id = ref 0 in + fun () -> incr id; !id +;; module Utils (B : Terms.Blob) = struct module Subst = FoSubst.Subst(B) ;; @@ -102,11 +107,6 @@ module Utils (B : Terms.Blob) = struct ;; (* may be moved inside the bag *) - let mk_id = - let id = ref 0 in - fun () -> incr id; !id - ;; - let mk_unit_clause maxvar ty proofterm = let varlist = let rec aux acc = function diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 13b1d7270..f30a9fcb6 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -49,9 +49,11 @@ let nparamod metasenv subst context t table = prerr_endline "Active table:"; List.iter (fun uc -> prerr_endline (Pp.pp_unit_clause uc)) active_clauses; let bag, maxvar, _, newclauses = - Sup.superposition_right bag maxvar clause (active_clauses, table) + 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 "========================================"; ;; diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml index e7353cee8..a125101bc 100644 --- a/helm/software/components/ng_paramodulation/pp.ml +++ b/helm/software/components/ng_paramodulation/pp.ml @@ -80,10 +80,10 @@ let pp_proof bag ~formatter:f p = ;; let string_of_comparison = function - | Terms.Lt -> "<" - | Terms.Gt -> ">" - | Terms.Eq -> "=" - | Terms.Incomparable -> "I" + | Terms.Lt -> "=<=" + | Terms.Gt -> "=>=" + | Terms.Eq -> "===" + | Terms.Incomparable -> "=?=" let pp_unit_clause ~formatter:f c = let (id, l, vars, proof) = c in @@ -96,19 +96,27 @@ let pp_unit_clause ~formatter:f c = pp_foterm f ty; Format.fprintf f "}: "; pp_foterm f lhs; - Format.fprintf f " =(%s) " (string_of_comparison comp); + Format.fprintf f " %s " (string_of_comparison comp); pp_foterm f rhs; Format.fprintf f " [%s] by %s" (String.concat ", " (List.map string_of_int vars)) (match proof with | Terms.Exact _ -> "axiom" - | Terms.Step (Terms.SuperpositionRight, id1, id2, _, p, _) -> - Printf.sprintf "supR %d with %d at %s" id1 id2 (String.concat - "," (List.map string_of_int p)) - | _ -> assert false) + | Terms.Step (rule, id1, id2, _, p, _) -> + Printf.sprintf "%s %d with %d at %s" + (string_of_rule rule) + id1 id2 (String.concat + "," (List.map string_of_int p))) ;; +let pp_bag ~formatter:f bag = + Format.fprintf f "@["; + Terms.M.iter + (fun _ c -> pp_unit_clause ~formatter:f c;Format.fprintf f "@;") bag; + Format.fprintf f "@]" +;; + (* String buffer implementation *) let on_buffer f t = let buff = Buffer.create 100 in @@ -118,6 +126,10 @@ let on_buffer f t = Buffer.contents buff ;; +let pp_bag = + on_buffer pp_bag +;; + let pp_foterm = on_buffer pp_foterm ;; diff --git a/helm/software/components/ng_paramodulation/pp.mli b/helm/software/components/ng_paramodulation/pp.mli index dbfca2073..9cdc7a7c1 100644 --- a/helm/software/components/ng_paramodulation/pp.mli +++ b/helm/software/components/ng_paramodulation/pp.mli @@ -18,5 +18,6 @@ module Pp (B : Terms.Blob) : val pp_proof: B.t Terms.bag -> B.t Terms.proof -> string val pp_substitution: B.t Terms.substitution -> string val pp_unit_clause: B.t Terms.unit_clause -> string + val pp_bag: B.t Terms.bag -> string end diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 6b98ed5be..1729919af 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -20,6 +20,34 @@ module Superposition (B : Terms.Blob) = module Utils = FoUtils.Utils(B) module Pp = Pp.Pp(B) + let rec list_first f = function + | [] -> None + | x::tl -> match f x with Some _ as x -> x | _ -> list_first f tl + ;; + + let first_position pos ctx t f = + let rec aux pos ctx = function + | Terms.Leaf _ as t -> f t pos ctx + | Terms.Var _ -> None + | Terms.Node l as t-> + match f t pos ctx with + | Some _ as x -> x + | None -> + let rec first pre post = function + | [] -> None + | t :: tl -> + let newctx = fun x -> ctx (Terms.Node (pre@[x]@post)) in + match aux (List.length pre :: pos) newctx t with + | Some _ as x -> x + | None -> + if post = [] then None (* tl is also empty *) + else first (pre @ [t]) (List.tl post) tl + in + first [] (List.tl l) l + in + aux pos ctx t + ;; + let all_positions pos ctx t f = let rec aux pos ctx = function | Terms.Leaf _ as t -> f t pos ctx @@ -38,6 +66,122 @@ module Superposition (B : Terms.Blob) = in aux pos ctx t ;; + + let build_clause bag filter rule t subst vl id id2 pos dir = + let proof = Terms.Step(rule,id,id2,dir,pos,subst) in + let t = Subst.apply_subst subst t in + if filter t then + let literal = + match t with + | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq -> + let o = Order.compare_terms l r in + Terms.Equation (l, r, ty, o) + | t -> Terms.Predicate t + in + let bag, uc = + Utils.add_to_bag bag (0, literal, vl, proof) + in + Some (bag, uc) + else + ((*prerr_endline ("Filtering: " ^ Pp.pp_foterm t);*)None) + ;; + + + (* ============ simplification ================= *) + + let demod table varlist subterm pos context = + let cands = IDX.DT.retrieve_generalizations table subterm in + list_first + (fun (dir, (id,lit,vl,_)) -> + match lit with + | Terms.Predicate _ -> assert false + | Terms.Equation (l,r,_,o) -> + let side, newside = if dir=Terms.Left2Right then l,r else r,l in + try + let subst, varlist = + Unif.unification (varlist@vl) varlist subterm side + in + if o = Terms.Incomparable then + let side = Subst.apply_subst subst side in + let newside = Subst.apply_subst subst newside in + let o = Order.compare_terms side newside in + (* Riazanov, pp. 45 (ii) *) + if o = Terms.Lt then + Some (context newside, subst, varlist, id, pos, dir) + else + ((*prerr_endline ("Filtering: " ^ + Pp.pp_foterm side ^ " =(< || =)" ^ + Pp.pp_foterm newside ^ " coming from " ^ + Pp.pp_unit_clause uc );*)None) + else + Some (context newside, subst, varlist, id, pos, dir) + with FoUnif.UnificationFailure _ -> None) + (IDX.ClauseSet.elements cands) + ;; + + (* XXX: possible optimization, if the literal has a "side" already + * in normal form we should not traverse it again *) + let demodulate_once bag (id, literal, vl, _) table = + let t = + match literal with + | Terms.Predicate t -> t + | Terms.Equation (l,r,ty,_) -> Terms.Node [ Terms.Leaf B.eqP; ty; l; r ] + in + match first_position [] (fun x -> x) t (demod table vl) with + | None -> None + | Some (newt, subst, varlist, id2, pos, dir) -> + build_clause bag (fun _ -> true) Terms.Demodulation + newt subst varlist id id2 pos dir + ;; + + let rec demodulate bag clause table = + match demodulate_once bag clause table with + | None -> bag, clause + | Some (bag, clause) -> demodulate bag clause table + ;; + + (* move away *) + let is_identity_clause = function + | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true + | _, Terms.Predicate _, _, _ -> assert false + | _ -> false + ;; + + let is_subsumed (id, lit, vl, _) table = + match lit with + | Terms.Predicate _ -> assert false + | Terms.Equation (l,r,ty,_) -> + let lcands = IDX.DT.retrieve_generalizations table l in + let rcands = IDX.DT.retrieve_generalizations table l in + let f b c = + let dir, l, r, vl = + match c with + | (d, (_,Terms.Equation (l,r,ty,_),vl,_))-> d, l, r, vl + |_ -> assert false + in + let l, r = if (dir = Terms.Left2Right) = b then l,r else r,l in + Terms.Node [ Terms.Leaf B.eqP; ty; l; r ], vl + in + let cands1 = List.map (f true) (IDX.ClauseSet.elements lcands) in + let cands2 = List.map (f false) (IDX.ClauseSet.elements rcands) in + let t = Terms.Node [ Terms.Leaf B.eqP; ty; l; r ] in + List.exists + (fun (c, vl1) -> + try ignore(Unif.unification (vl@vl1) vl c t); true + with FoUnif.UnificationFailure _ -> false) + (cands1 @ cands2) + ;; + + (* demodulate and check for subsumption *) + let forward_simplify table bag clause = + let bag, clause = demodulate bag clause table in + if is_identity_clause clause then None + else + if is_subsumed clause table then None + else Some (bag, clause) + ;; + + (* =================== inference ===================== *) let superposition_right table varlist subterm pos context = let cands = IDX.DT.retrieve_unifiables table subterm in @@ -46,7 +190,6 @@ module Superposition (B : Terms.Blob) = match lit with | Terms.Predicate _ -> assert false | Terms.Equation (l,r,_,o) -> - assert(o <> Terms.Eq); let side, newside = if dir=Terms.Left2Right then l,r else r,l in try let subst, varlist = @@ -70,54 +213,42 @@ module Superposition (B : Terms.Blob) = (IDX.ClauseSet.elements cands) ;; - let build_new_clause bag maxvar filter t subst vl id id2 pos dir = + let build_new_clause bag maxvar filter rule t subst vl id id2 pos dir = let maxvar, vl, relocsubst = Utils.relocate maxvar vl in let subst = Subst.concat relocsubst subst in - let proof = Terms.Step(Terms.SuperpositionRight,id,id2,dir,pos,subst) in - let t = Subst.apply_subst subst t in - if filter t then - let literal = - match t with - | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq -> - let o = Order.compare_terms l r in - Terms.Equation (l, r, ty, o) - | t -> Terms.Predicate t - in - let bag, uc = - Utils.add_to_bag bag (0, literal, vl, proof) - in - Some (bag, maxvar, uc) - else - ((*prerr_endline ("Filtering: " ^ Pp.pp_foterm t);*)None) + match build_clause bag filter rule t subst vl id id2 pos dir with + | Some (bag, c) -> Some ((bag, maxvar), c) + | None -> None ;; - let fold_build_new_clause bag maxvar id filter res = - let maxvar, bag, new_clauses = - List.fold_left - (fun (maxvar, bag, acc) (t,subst,vl,id2,pos,dir) -> - match build_new_clause bag maxvar filter t subst vl id id2 pos dir - with Some (bag, maxvar, uc) -> maxvar, bag, uc::acc - | None -> maxvar, bag, acc) - (maxvar, bag, []) res + + let fold_build_new_clause bag maxvar id rule filter res = + let (bag, maxvar), res = + HExtlib.filter_map_acc + (fun (bag, maxvar) (t,subst,vl,id2,pos,dir) -> + build_new_clause bag maxvar filter rule t subst vl id id2 pos dir) + (bag, maxvar) res in - bag, maxvar, new_clauses + bag, maxvar, res ;; let superposition_right_with_table bag maxvar (id,selected,vl,_) table = match selected with | Terms.Predicate _ -> assert false | Terms.Equation (l,r,ty,Terms.Lt) -> - fold_build_new_clause bag maxvar id (fun _ -> true) + fold_build_new_clause bag maxvar id Terms.SuperpositionRight + (fun _ -> true) (all_positions [3] (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) r (superposition_right table vl)) | Terms.Equation (l,r,ty,Terms.Gt) -> - fold_build_new_clause bag maxvar id (fun _ -> true) + fold_build_new_clause bag maxvar id Terms.SuperpositionRight + (fun _ -> true) (all_positions [2] (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) l (superposition_right table vl)) | Terms.Equation (l,r,ty,Terms.Incomparable) -> - fold_build_new_clause bag maxvar id + fold_build_new_clause bag maxvar id Terms.SuperpositionRight (function (* Riazanov: p.33 condition (iv) *) | Terms.Node [Terms.Leaf eq; ty; l; r ] when B.eq B.eqP eq -> Order.compare_terms l r <> Terms.Eq @@ -133,7 +264,7 @@ module Superposition (B : Terms.Blob) = (* the current equation is normal w.r.t. demodulation with atable * (and is not the identity) *) - let superposition_right bag maxvar current (alist,atable) = + let infer_right bag maxvar current (alist,atable) = let ctable = IDX.index_unit_clause IDX.DT.empty current in let bag, maxvar, new_clauses = List.fold_left @@ -151,9 +282,13 @@ module Superposition (B : Terms.Blob) = let bag, maxvar, additional_new_clauses = superposition_right_with_table bag maxvar fresh_current atable in - bag, maxvar, (alist, atable), new_clauses @ additional_new_clauses + let new_clauses = new_clauses @ additional_new_clauses in + let bag, new_clauses = + HExtlib.filter_map_acc (forward_simplify atable) bag new_clauses + in + bag, maxvar, (alist, atable), new_clauses ;; - + end diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli index 54b5ae50f..adfaf68e2 100644 --- a/helm/software/components/ng_paramodulation/superposition.mli +++ b/helm/software/components/ng_paramodulation/superposition.mli @@ -16,13 +16,13 @@ module Superposition (B : Terms.Blob) : sig (* The returned active set is the input one + the selected clause *) - val superposition_right : + val infer_right : B.t Terms.bag -> int -> (* maxvar *) B.t Terms.unit_clause -> (* selected *) Index.Index(B).active_set -> B.t Terms.bag * int * Index.Index(B).active_set * B.t Terms.unit_clause list - + end