From: Enrico Tassi Date: Tue, 9 Jun 2009 16:22:41 +0000 (+0000) Subject: almost complete superposition right step X-Git-Tag: make_still_working~3893 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=40ce8d1c14808ea7608ee2988bd9aba77ddf8200;p=helm.git almost complete superposition right step --- diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend index 0a7503d12..cf6dcda02 100644 --- a/helm/software/components/ng_paramodulation/.depend +++ b/helm/software/components/ng_paramodulation/.depend @@ -17,18 +17,18 @@ foSubst.cmo: terms.cmi foSubst.cmi foSubst.cmx: terms.cmx foSubst.cmi orderings.cmo: terms.cmi orderings.cmi orderings.cmx: terms.cmx orderings.cmi -foUtils.cmo: terms.cmi orderings.cmi index.cmi foSubst.cmi foUtils.cmi -foUtils.cmx: terms.cmx orderings.cmx index.cmx foSubst.cmx foUtils.cmi +foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi +foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi index.cmo: terms.cmi foUtils.cmi index.cmi index.cmx: terms.cmx foUtils.cmx index.cmi foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi -superposition.cmo: terms.cmi orderings.cmi index.cmi foUtils.cmi foUnif.cmi \ - foSubst.cmi superposition.cmi -superposition.cmx: terms.cmx orderings.cmx index.cmx foUtils.cmx foUnif.cmx \ - foSubst.cmx superposition.cmi -nCicBlob.cmo: terms.cmi nCicBlob.cmi -nCicBlob.cmx: terms.cmx nCicBlob.cmi +superposition.cmo: terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \ + foUnif.cmi foSubst.cmi superposition.cmi +superposition.cmx: terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \ + foUnif.cmx foSubst.cmx superposition.cmi +nCicBlob.cmo: terms.cmi foUtils.cmi nCicBlob.cmi +nCicBlob.cmx: terms.cmx foUtils.cmx nCicBlob.cmi cicBlob.cmo: terms.cmi cicBlob.cmi cicBlob.cmx: terms.cmx cicBlob.cmi paramod.cmo: superposition.cmi pp.cmi nCicBlob.cmi index.cmi foUtils.cmi \ diff --git a/helm/software/components/ng_paramodulation/.depend.opt b/helm/software/components/ng_paramodulation/.depend.opt index 1dbf27b11..cf6dcda02 100644 --- a/helm/software/components/ng_paramodulation/.depend.opt +++ b/helm/software/components/ng_paramodulation/.depend.opt @@ -2,9 +2,9 @@ terms.cmi: pp.cmi: terms.cmi foSubst.cmi: terms.cmi orderings.cmi: terms.cmi -foUtils.cmi: terms.cmi index.cmi -foUnif.cmi: terms.cmi +foUtils.cmi: terms.cmi index.cmi: terms.cmi +foUnif.cmi: terms.cmi superposition.cmi: terms.cmi index.cmi nCicBlob.cmi: terms.cmi cicBlob.cmi: terms.cmi @@ -17,18 +17,18 @@ foSubst.cmo: terms.cmi foSubst.cmi foSubst.cmx: terms.cmx foSubst.cmi orderings.cmo: terms.cmi orderings.cmi orderings.cmx: terms.cmx orderings.cmi -foUtils.cmo: terms.cmi orderings.cmi index.cmi foSubst.cmi foUtils.cmi -foUtils.cmx: terms.cmx orderings.cmx index.cmx foSubst.cmx foUtils.cmi -foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi -foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi +foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi +foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi index.cmo: terms.cmi foUtils.cmi index.cmi index.cmx: terms.cmx foUtils.cmx index.cmi -superposition.cmo: terms.cmi orderings.cmi index.cmi foUtils.cmi foUnif.cmi \ - foSubst.cmi superposition.cmi -superposition.cmx: terms.cmx orderings.cmx index.cmx foUtils.cmx foUnif.cmx \ - foSubst.cmx superposition.cmi -nCicBlob.cmo: terms.cmi nCicBlob.cmi -nCicBlob.cmx: terms.cmx nCicBlob.cmi +foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi +foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi +superposition.cmo: terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \ + foUnif.cmi foSubst.cmi superposition.cmi +superposition.cmx: terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \ + foUnif.cmx foSubst.cmx superposition.cmi +nCicBlob.cmo: terms.cmi foUtils.cmi nCicBlob.cmi +nCicBlob.cmx: terms.cmx foUtils.cmx nCicBlob.cmi cicBlob.cmo: terms.cmi cicBlob.cmi cicBlob.cmx: terms.cmx cicBlob.cmi paramod.cmo: superposition.cmi pp.cmi nCicBlob.cmi index.cmi foUtils.cmi \ diff --git a/helm/software/components/ng_paramodulation/foUtils.mli b/helm/software/components/ng_paramodulation/foUtils.mli index d78ce32f2..3bf04342b 100644 --- a/helm/software/components/ng_paramodulation/foUtils.mli +++ b/helm/software/components/ng_paramodulation/foUtils.mli @@ -29,10 +29,9 @@ module Utils (B : Terms.Blob) : val eq_unit_clause : B.t Terms.unit_clause -> B.t Terms.unit_clause -> bool val compare_unit_clause : B.t Terms.unit_clause -> B.t Terms.unit_clause -> int -(* + val fresh_unit_clause : int -> B.t Terms.unit_clause -> B.t Terms.unit_clause * int -*) (* relocate [maxvar] [varlist] -> [newmaxvar] * [varlist] * [relocsubst] *) val relocate : int -> int list -> int * int list * B.t Terms.substitution diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml index 6c26e7b86..3c203d3a7 100644 --- a/helm/software/components/ng_paramodulation/index.ml +++ b/helm/software/components/ng_paramodulation/index.ml @@ -93,4 +93,6 @@ module Index(B : Terms.Blob) = struct DT.index t p (Terms.Nodir, c) ;; + type active_set = B.t Terms.unit_clause list * DT.t + end diff --git a/helm/software/components/ng_paramodulation/index.mli b/helm/software/components/ng_paramodulation/index.mli index 5581f7cfa..5d496d936 100644 --- a/helm/software/components/ng_paramodulation/index.mli +++ b/helm/software/components/ng_paramodulation/index.mli @@ -29,4 +29,6 @@ module Index (B : Terms.Blob) : val index_unit_clause : DT.t -> B.t Terms.unit_clause -> DT.t + type active_set = B.t Terms.unit_clause list * DT.t + end diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index fb93ec7f8..13b1d7270 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -48,8 +48,8 @@ let nparamod metasenv subst context t table = in prerr_endline "Active table:"; List.iter (fun uc -> prerr_endline (Pp.pp_unit_clause uc)) active_clauses; - let bag, maxvar, newclauses = - Sup.superposition_right_with_table bag maxvar clause table + let bag, maxvar, _, newclauses = + Sup.superposition_right bag maxvar clause (active_clauses, table) in prerr_endline "Output clauses :"; List.iter (fun c -> prerr_endline (Pp.pp_unit_clause c)) newclauses; diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml index 609ca47a7..e7353cee8 100644 --- a/helm/software/components/ng_paramodulation/pp.ml +++ b/helm/software/components/ng_paramodulation/pp.ml @@ -86,7 +86,7 @@ let string_of_comparison = function | Terms.Incomparable -> "I" let pp_unit_clause ~formatter:f c = - let (id, l, vars, _) = c in + let (id, l, vars, proof) = c in Format.fprintf f "Id : %d, " id ; match l with | Terms.Predicate t -> @@ -98,8 +98,15 @@ let pp_unit_clause ~formatter:f c = pp_foterm f lhs; Format.fprintf f " =(%s) " (string_of_comparison comp); pp_foterm f rhs; - Format.fprintf f " [%s]" - (String.concat ", " (List.map string_of_int vars)) + 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) + ;; (* String buffer implementation *) diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index fe4b578b6..6b98ed5be 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -130,6 +130,29 @@ module Superposition (B : Terms.Blob) = l (superposition_right table vl))) | _ -> assert false ;; + + (* 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 ctable = IDX.index_unit_clause IDX.DT.empty current in + let bag, maxvar, new_clauses = + List.fold_left + (fun (bag, maxvar, acc) active -> + let bag, maxvar, newc = + superposition_right_with_table bag maxvar active ctable + in + bag, maxvar, newc @ acc) + (bag, maxvar, []) alist + in + let alist, atable = + current :: alist, IDX.index_unit_clause atable current + in + let fresh_current, maxvar = Utils.fresh_unit_clause maxvar current in + 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 + ;; end diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli index b67233563..54b5ae50f 100644 --- a/helm/software/components/ng_paramodulation/superposition.mli +++ b/helm/software/components/ng_paramodulation/superposition.mli @@ -15,12 +15,13 @@ module Superposition (B : Terms.Blob) : sig - val superposition_right_with_table : + (* The returned active set is the input one + the selected clause *) + val superposition_right : B.t Terms.bag -> int -> (* maxvar *) - B.t Terms.unit_clause -> - Index.Index(B).DT.t -> - B.t Terms.bag * int * B.t Terms.unit_clause list + 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