From 96c91e470f670018df67c9cbff62fa06e3b57c5e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 10 Jun 2009 16:43:48 +0000 Subject: [PATCH] 1) added simplification of actives w.r.t. selected 2) added simple main loop (look at the comment for a possible optimization) --- .../components/ng_paramodulation/paramod.ml | 86 +++++++++++++++++++ .../components/ng_paramodulation/pp.ml | 6 +- .../ng_paramodulation/superposition.ml | 52 ++++++++--- .../ng_paramodulation/superposition.mli | 31 ++++++- .../components/ng_paramodulation/terms.ml | 2 +- .../components/ng_paramodulation/terms.mli | 2 +- helm/software/matita/tests/paratest.ma | 6 +- 7 files changed, 165 insertions(+), 20 deletions(-) diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index f30a9fcb6..9b5b13157 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -57,3 +57,89 @@ let nparamod metasenv subst context t table = prerr_endline (Pp.pp_bag bag); prerr_endline "========================================"; ;; + +let select = function + | [] -> None + | x::tl -> Some (x, tl) +;; + +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 rec given_clause bag maxvar actives passives g_actives g_passives = + + (* keep goals demodulated w.r.t. actives and check if solved *) + (* we may move this at the end of infer_right and simplify with + * just new_clauses *) + let bag, g_actives = + List.fold_left + (fun (bag,acc) c -> + let bag, c = Sup.backward_simplify maxvar (snd actives) bag c in + bag, c::acc) + (bag,[]) g_actives + in + + (* backward step *) + let bag, maxvar, g_actives, g_passives = + match select g_passives with + | None -> bag, maxvar, g_actives, g_passives + | Some (g_current, g_passives) -> + let bag, g_current = + Sup.backward_simplify maxvar (snd actives) bag g_current + in + let bag, maxvar, new_goals = + Sup.infer_left bag maxvar g_current actives + in + bag, maxvar, g_current::g_actives, g_passives @ new_goals + in + + (* forward step *) + let bag, maxvar, actives, passives = + match select passives with + | None -> bag, maxvar, actives, passives + | Some (current, passives) -> + match Sup.forward_simplify (snd actives) bag current with + | None -> bag, maxvar, actives, passives + | Some (bag, current) -> + let bag, maxvar, actives, new_clauses = + Sup.infer_right bag maxvar current actives + in + bag, maxvar, actives, passives @ new_clauses + in + + given_clause bag maxvar actives passives g_actives g_passives + in + + let mk_clause bag maxvar ty = + let ty = B.embed ty in + let proof = B.embed (NCic.Rel ~-1) in + let c, maxvar = Utils.mk_unit_clause maxvar ty proof in + let bag, c = Utils.add_to_bag bag c in + bag, maxvar, c + in + let bag, maxvar, goal = mk_clause Terms.M.empty 0 t in + let g_actives = [] in + let g_passives = [goal] in + let passives, bag, maxvar = + List.fold_left + (fun (cl, bag, maxvar) t -> + let bag, maxvar, c = mk_clause bag maxvar t in + c::cl, bag, maxvar) + ([], bag, maxvar) table + in + let actives = [], IDX.DT.empty in + try given_clause bag maxvar actives passives g_actives g_passives + with Sup.Success _ -> prerr_endline "YES!" +;; diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml index a125101bc..b90c08d38 100644 --- a/helm/software/components/ng_paramodulation/pp.ml +++ b/helm/software/components/ng_paramodulation/pp.ml @@ -36,9 +36,8 @@ let pp_foterm ~formatter:f t = ;; let string_of_rule = function - | Terms.SuperpositionRight -> "SupR" - | Terms.SuperpositionLeft -> "SupL" - | Terms.Demodulation -> "Demod" + | Terms.Superposition -> "Super" + | Terms.Demodulation -> "Demod" ;; let string_of_direction = function @@ -107,7 +106,6 @@ let pp_unit_clause ~formatter:f c = (string_of_rule rule) id1 id2 (String.concat "," (List.map string_of_int p))) - ;; let pp_bag ~formatter:f bag = diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 1729919af..4015d4b6d 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -19,6 +19,8 @@ module Superposition (B : Terms.Blob) = module Order = Orderings.Orderings(B) module Utils = FoUtils.Utils(B) module Pp = Pp.Pp(B) + + exception Success of B.t Terms.bag * int * B.t Terms.unit_clause let rec list_first f = function | [] -> None @@ -181,9 +183,17 @@ module Superposition (B : Terms.Blob) = else Some (bag, clause) ;; + (* this is like forward_simplify but raises Success *) + let backward_simplify maxvar table bag clause = + let bag, clause = demodulate bag clause table in + if is_identity_clause clause then raise (Success (bag, maxvar, clause)) + else bag, clause + ;; + (* =================== inference ===================== *) - let superposition_right table varlist subterm pos context = + (* this is OK for both the sup_left and sup_right inference steps *) + let superposition table varlist subterm pos context = let cands = IDX.DT.retrieve_unifiables table subterm in HExtlib.filter_map (fun (dir, (id,lit,vl,_ (*as uc*))) -> @@ -232,33 +242,33 @@ module Superposition (B : Terms.Blob) = bag, maxvar, res ;; - let superposition_right_with_table bag maxvar (id,selected,vl,_) table = + let superposition_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 Terms.SuperpositionRight + fold_build_new_clause bag maxvar id Terms.Superposition (fun _ -> true) (all_positions [3] (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) - r (superposition_right table vl)) + r (superposition table vl)) | Terms.Equation (l,r,ty,Terms.Gt) -> - fold_build_new_clause bag maxvar id Terms.SuperpositionRight + fold_build_new_clause bag maxvar id Terms.Superposition (fun _ -> true) (all_positions [2] (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) - l (superposition_right table vl)) + l (superposition table vl)) | Terms.Equation (l,r,ty,Terms.Incomparable) -> - fold_build_new_clause bag maxvar id Terms.SuperpositionRight + fold_build_new_clause bag maxvar id Terms.Superposition (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 | _ -> assert false) ((all_positions [3] (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) - r (superposition_right table vl)) @ + r (superposition table vl)) @ (all_positions [2] (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) - l (superposition_right table vl))) + l (superposition table vl))) | _ -> assert false ;; @@ -266,11 +276,17 @@ module Superposition (B : Terms.Blob) = * (and is not the identity) *) let infer_right bag maxvar current (alist,atable) = let ctable = IDX.index_unit_clause IDX.DT.empty current in + let bag, (alist, atable) = + let bag, alist = + HExtlib.filter_map_acc (forward_simplify ctable) bag alist + in + bag, (alist, List.fold_left IDX.index_unit_clause IDX.DT.empty alist) + 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 + superposition_with_table bag maxvar active ctable in bag, maxvar, newc @ acc) (bag, maxvar, []) alist @@ -280,7 +296,7 @@ module Superposition (B : Terms.Blob) = 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 + superposition_with_table bag maxvar fresh_current atable in let new_clauses = new_clauses @ additional_new_clauses in let bag, new_clauses = @@ -289,6 +305,20 @@ module Superposition (B : Terms.Blob) = bag, maxvar, (alist, atable), new_clauses ;; + let infer_left bag maxvar goal (_alist, atable) = + let bag, maxvar, new_goals = + superposition_with_table bag maxvar goal atable + in + let bag, new_goals = + List.fold_left + (fun (bag, acc) g -> + let bag, g = demodulate bag g atable in + bag, g :: acc) + (bag, []) new_goals + in + bag, maxvar, List.rev new_goals + ;; + end diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli index adfaf68e2..5878918c2 100644 --- a/helm/software/components/ng_paramodulation/superposition.mli +++ b/helm/software/components/ng_paramodulation/superposition.mli @@ -11,18 +11,45 @@ (* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *) - module Superposition (B : Terms.Blob) : sig + exception Success of B.t Terms.bag * int * B.t Terms.unit_clause + (* The returned active set is the input one + the selected clause *) val infer_right : B.t Terms.bag -> int -> (* maxvar *) - B.t Terms.unit_clause -> (* selected *) + B.t Terms.unit_clause -> (* selected passive *) Index.Index(B).active_set -> B.t Terms.bag * int * Index.Index(B).active_set * B.t Terms.unit_clause list + val infer_left : + B.t Terms.bag -> + int -> (* maxvar *) + B.t Terms.unit_clause -> (* selected goal *) + Index.Index(B).active_set -> + B.t Terms.bag * int * B.t Terms.unit_clause list + + val demodulate : + B.t Terms.bag -> + B.t Terms.unit_clause -> + Index.Index(B).DT.t -> B.t Terms.bag * B.t Terms.unit_clause + + val forward_simplify : + Index.Index(B).DT.t -> + B.t Terms.bag -> + B.t Terms.unit_clause -> + (B.t Terms.bag * B.t Terms.unit_clause) option + + (* may raise success *) + val backward_simplify : + int -> + Index.Index(B).DT.t -> + B.t Terms.bag -> + B.t Terms.unit_clause -> + B.t Terms.bag * B.t Terms.unit_clause + end diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml index 0e7bed7fb..bcc3bcf7b 100644 --- a/helm/software/components/ng_paramodulation/terms.ml +++ b/helm/software/components/ng_paramodulation/terms.ml @@ -20,7 +20,7 @@ type 'a substitution = (int * 'a foterm) list type comparison = Lt | Eq | Gt | Incomparable -type rule = SuperpositionRight | SuperpositionLeft | Demodulation +type rule = Superposition | Demodulation type direction = Left2Right | Right2Left | Nodir type position = int list diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli index d7f4b74e3..7b3cb1750 100644 --- a/helm/software/components/ng_paramodulation/terms.mli +++ b/helm/software/components/ng_paramodulation/terms.mli @@ -20,7 +20,7 @@ type 'a substitution = (int * 'a foterm) list type comparison = Lt | Eq | Gt | Incomparable -type rule = SuperpositionRight | SuperpositionLeft | Demodulation +type rule = Superposition | Demodulation (* A Discrimination tree is a map: foterm |-> (dir, clause) *) type direction = Left2Right | Right2Left | Nodir diff --git a/helm/software/matita/tests/paratest.ma b/helm/software/matita/tests/paratest.ma index de4c42048..68fe4cdde 100644 --- a/helm/software/matita/tests/paratest.ma +++ b/helm/software/matita/tests/paratest.ma @@ -14,9 +14,13 @@ include "nat/plus.ma". +ntheorem boo: + ((λx.x = x) ?) → 0 = 0. +##[ #H; nwhd in H ⊢ %; nauto by H. + ntheorem foo: ((λx.x + 0 = x) ?) → ((λx,y.x + S y = S (x + y)) ? ?) → ((λx,y.y + x = x + y) ? ?) → ∀x. ((λz. x + x = z + S z) ?). -##[ #H; #H1; #H2; #x; nnormalize in H H1 H2 ⊢ %; nauto by H, H1, H2. \ No newline at end of file +##[ #H; #H1; #H2; #x; nwhd in H H1 H2 ⊢ %; nauto by H, H1, H2. \ No newline at end of file -- 2.39.2