From 4ae7d510a430a2a6929f973d36b993d528772d64 Mon Sep 17 00:00:00 2001 From: denes Date: Thu, 11 Jun 2009 22:52:38 +0000 Subject: [PATCH] Active goals are now demodulated after selecting a positive clause. Implemented OrderedSet for passive clauses. Selection is now based on weight (fairness condition to be added). --- .../components/ng_paramodulation/foUtils.ml | 9 ++ .../components/ng_paramodulation/foUtils.mli | 6 + .../components/ng_paramodulation/orderings.ml | 4 +- .../ng_paramodulation/orderings.mli | 3 + .../components/ng_paramodulation/paramod.ml | 125 +++++++++++++----- .../components/ng_paramodulation/paramod.mli | 2 +- .../ng_paramodulation/superposition.ml | 49 +++++-- .../ng_paramodulation/superposition.mli | 1 + .../components/ng_tactics/nTactics.ml | 5 +- helm/software/matita/tests/paratest.ma | 17 ++- 10 files changed, 169 insertions(+), 52 deletions(-) diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml index 76e9735be..ec76511d9 100644 --- a/helm/software/components/ng_paramodulation/foUtils.ml +++ b/helm/software/components/ng_paramodulation/foUtils.ml @@ -136,4 +136,13 @@ module Utils (B : Terms.Blob) = struct let empty_bag = Terms.M.empty ;; + let mk_passive_clause cl = + (Order.compute_unit_clause_weight cl, cl) + ;; + + let compare_passive_clauses (w1,(id1,_,_,_)) (w2,(id2,_,_,_)) = + if w1 = w2 then id1 - id2 + else w1 - w2 + ;; + end diff --git a/helm/software/components/ng_paramodulation/foUtils.mli b/helm/software/components/ng_paramodulation/foUtils.mli index 3bf04342b..d0fb30367 100644 --- a/helm/software/components/ng_paramodulation/foUtils.mli +++ b/helm/software/components/ng_paramodulation/foUtils.mli @@ -26,6 +26,9 @@ module Utils (B : Terms.Blob) : int -> B.t Terms.foterm -> B.t Terms.foterm -> B.t Terms.unit_clause * int + val mk_passive_clause : + B.t Terms.unit_clause -> B.t Terms.passive_clause + 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 @@ -43,4 +46,7 @@ module Utils (B : Terms.Blob) : val empty_bag : B.t Terms.bag + val compare_passive_clauses : + B.t Terms.passive_clause -> B.t Terms.passive_clause -> int + end diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml index 8f0575a67..51b48a4c3 100644 --- a/helm/software/components/ng_paramodulation/orderings.ml +++ b/helm/software/components/ng_paramodulation/orderings.ml @@ -49,12 +49,12 @@ module Orderings (B : Terms.Blob) = struct (w, List.sort compare l) (* from the smallest meta to the bigest *) ;; - let compute_unit_clause_weight = + let compute_unit_clause_weight (_,l, _, _) = let weight_of_polynomial w m = let factor = 2 in w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m in - function + match l with | Terms.Predicate t -> let w, m = weight_of_term t in weight_of_polynomial w m diff --git a/helm/software/components/ng_paramodulation/orderings.mli b/helm/software/components/ng_paramodulation/orderings.mli index ccd6bf286..7586d41ac 100644 --- a/helm/software/components/ng_paramodulation/orderings.mli +++ b/helm/software/components/ng_paramodulation/orderings.mli @@ -22,4 +22,7 @@ module Orderings (B : Terms.Blob) : val compare_terms : B.t Terms.foterm -> B.t Terms.foterm -> Terms.comparison + val compute_unit_clause_weight : + B.t Terms.unit_clause -> int + end diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 9b5b13157..a33f1121d 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -1,4 +1,4 @@ -let nparamod metasenv subst context t table = +(*let nparamod metasenv subst context t table = prerr_endline "========================================"; let module C = struct let metasenv = metasenv @@ -11,7 +11,7 @@ let nparamod metasenv subst context t table = 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 module Utils = FoUtils.Utils(B) in*) (* let test_unification _ = function | Terms.Node [_; _; lhs; rhs] -> @@ -27,6 +27,8 @@ let nparamod metasenv subst context t table = 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 @@ -53,14 +55,13 @@ let nparamod metasenv subst context t 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 "Proofs: "; + prerr_endline (Pp.pp_bag bag); *) prerr_endline "========================================"; ;; - -let select = function - | [] -> None - | x::tl -> Some (x, tl) +*) +let debug s = + prerr_endline s ;; let nparamod metasenv subst context t table = @@ -77,69 +78,133 @@ let nparamod metasenv subst context t table = let module IDX = Index.Index(B) in let module Sup = Superposition.Superposition(B) in let module Utils = FoUtils.Utils(B) in - + + let module OrderedPassives = + struct + type t = B.t Terms.passive_clause + + let compare = Utils.compare_passive_clauses + end + in + let module PassiveSet = Set.Make(OrderedPassives) + in + let add_passive_clause passives cl = + PassiveSet.add (Utils.mk_passive_clause cl) passives + in + (* TODO : fairness condition *) + let select passives = + if PassiveSet.is_empty passives then None + 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 = - + (* 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) + 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 + + (* backward step : superposition left, simplifications on goals *) + debug "Backward infer 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) -> + debug ("Selected goal : " ^ Pp.pp_unit_clause g_current); 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 + let new_goals = List.fold_left add_passive_clause + PassiveSet.empty new_goals + in + bag, maxvar, g_current::g_actives, + (PassiveSet.union new_goals g_passives) in + prerr_endline + (Printf.sprintf "Number of active goals : %d" + (List.length g_actives)); + prerr_endline + (Printf.sprintf "Number of passive goals : %d" + (PassiveSet.cardinal g_passives)); - (* forward step *) - let bag, maxvar, actives, passives = + (* forward step *) + + (* e = select P * + * e' = demod A e * + * A' = demod [e'] A * + * A'' = A' + e' * + * e'' = fresh e' * + * new = supright e'' A'' * + * new'= demod A'' new * + * P' = P + new' *) + debug "Forward infer step..."; + let bag, maxvar, actives, passives, g_passives = match select passives with - | None -> bag, maxvar, actives, passives + | None -> bag, maxvar, actives, passives, g_passives | Some (current, passives) -> + debug ("Selected fact : " ^ Pp.pp_unit_clause current); match Sup.forward_simplify (snd actives) bag current with - | None -> bag, maxvar, actives, passives + | 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 - bag, maxvar, actives, passives @ new_clauses + 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))); + prerr_endline + (Printf.sprintf "Number of passives : %d" + (PassiveSet.cardinal passives)); 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 mk_clause bag maxvar (t,ty) = + let (proof,ty) = B.saturate t ty 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 g_passives = PassiveSet.singleton (Utils.mk_passive_clause 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 + (add_passive_clause cl c), bag, maxvar) + (PassiveSet.empty, 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!" + with Sup.Success (bag, _, mp) -> + prerr_endline "YES!"; + prerr_endline "Meeting point :"; prerr_endline (Pp.pp_unit_clause mp); + (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag) *) ;; diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli index 78bea9934..5ba90f943 100644 --- a/helm/software/components/ng_paramodulation/paramod.mli +++ b/helm/software/components/ng_paramodulation/paramod.mli @@ -1,4 +1,4 @@ val nparamod : NCic.metasenv -> NCic.substitution -> NCic.context -> - NCic.term -> NCic.term list -> + (NCic.term * NCic.term) -> (NCic.term * NCic.term) list -> unit diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 4015d4b6d..5b88f90cd 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -22,6 +22,10 @@ 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 rec list_first f = function | [] -> None | x::tl -> match f x with Some _ as x -> x | _ -> list_first f tl @@ -106,7 +110,7 @@ module Superposition (B : Terms.Blob) = 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 + let o = Order.compare_terms newside side in (* Riazanov, pp. 45 (ii) *) if o = Terms.Lt then Some (context newside, subst, varlist, id, pos, dir) @@ -123,7 +127,8 @@ module Superposition (B : Terms.Blob) = (* 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 demodulate_once bag (id, literal, vl, pr) table = + debug ("Demodulating : " ^ (Pp.pp_unit_clause (id, literal, vl, pr))); let t = match literal with | Terms.Predicate t -> t @@ -149,12 +154,14 @@ module Superposition (B : Terms.Blob) = | _ -> false ;; - let is_subsumed (id, lit, vl, _) table = + let is_subsumed ~unify (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 retrieve = if unify then IDX.DT.retrieve_unifiables + else IDX.DT.retrieve_generalizations in + let lcands = retrieve table l in + let rcands = retrieve table r in let f b c = let dir, l, r, vl = match c with @@ -167,11 +174,12 @@ module Superposition (B : Terms.Blob) = 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) + let locked_vars = if unify then [] else vl in + List.exists + (fun (c, vl1) -> + try ignore(Unif.unification (vl@vl1) locked_vars c t); true + with FoUnif.UnificationFailure _ -> false) + (cands1 @ cands2) ;; (* demodulate and check for subsumption *) @@ -179,14 +187,15 @@ module Superposition (B : Terms.Blob) = let bag, clause = demodulate bag clause table in if is_identity_clause clause then None else - if is_subsumed clause table then None + if is_subsumed ~unify:false clause table then None 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)) + if (is_identity_clause clause) || (is_subsumed ~unify:true clause table) + then raise (Success (bag, maxvar, clause)) else bag, clause ;; @@ -242,6 +251,7 @@ module Superposition (B : Terms.Blob) = bag, maxvar, res ;; + (* Superposes selected equation with equalities in table *) let superposition_with_table bag maxvar (id,selected,vl,_) table = match selected with | Terms.Predicate _ -> assert false @@ -275,6 +285,7 @@ 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 *) let ctable = IDX.index_unit_clause IDX.DT.empty current in let bag, (alist, atable) = let bag, alist = @@ -282,6 +293,8 @@ module Superposition (B : Terms.Blob) = in bag, (alist, List.fold_left IDX.index_unit_clause IDX.DT.empty alist) in + debug "Simplified active clauses with fact"; + (* We superpose active clauses with current *) let bag, maxvar, new_clauses = List.fold_left (fun (bag, maxvar, acc) active -> @@ -291,24 +304,36 @@ module Superposition (B : Terms.Blob) = bag, maxvar, newc @ acc) (bag, maxvar, []) alist in + debug "First superpositions"; + (* We add current to active clauses so that it can be * + * superposed with itself *) let alist, atable = current :: alist, IDX.index_unit_clause atable current in + debug "Indexed"; let fresh_current, maxvar = Utils.fresh_unit_clause maxvar current in + (* We need to put fresh_current into the bag so that all * + * variables clauses refer to are known. *) + let bag, fresh_current = Utils.add_to_bag bag fresh_current in + (* We superpose current with active clauses *) let bag, maxvar, additional_new_clauses = superposition_with_table bag maxvar fresh_current atable in + debug "Another superposition"; let new_clauses = new_clauses @ additional_new_clauses in let bag, new_clauses = HExtlib.filter_map_acc (forward_simplify atable) bag new_clauses in + debug "Demodulated new clauses"; bag, maxvar, (alist, atable), new_clauses ;; let infer_left bag maxvar goal (_alist, atable) = + (* We superpose the goal with active clauses *) let bag, maxvar, new_goals = superposition_with_table bag maxvar goal atable in + (* We demodulate the goal with active clauses *) let bag, new_goals = List.fold_left (fun (bag, acc) g -> diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli index 5878918c2..cce81944b 100644 --- a/helm/software/components/ng_paramodulation/superposition.mli +++ b/helm/software/components/ng_paramodulation/superposition.mli @@ -14,6 +14,7 @@ module Superposition (B : Terms.Blob) : sig + (* bag, maxvar, meeting point *) exception Success of B.t Terms.bag * int * B.t Terms.unit_clause (* The returned active set is the input one + the selected clause *) diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index fd383f7c1..147df78f8 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -563,11 +563,12 @@ let auto ~params:(l,_) status goal = (fun (status, l) t -> let status, t = disambiguate status t None (ctx_of gty) in let status, ty = typeof status (ctx_of t) t in + let status, t = term_of_cic_term status t (ctx_of gty) in let status, ty = term_of_cic_term status ty (ctx_of ty) in - (status, ty :: l)) + (status, (t,ty) :: l)) (status,[]) l in - Paramod.nparamod metasenv subst (ctx_of gty) t l; + Paramod.nparamod metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l; status ;; diff --git a/helm/software/matita/tests/paratest.ma b/helm/software/matita/tests/paratest.ma index 68fe4cdde..93970a1d4 100644 --- a/helm/software/matita/tests/paratest.ma +++ b/helm/software/matita/tests/paratest.ma @@ -14,13 +14,20 @@ include "nat/plus.ma". -ntheorem boo: - ((λx.x = x) ?) → 0 = 0. -##[ #H; nwhd in H ⊢ %; nauto by H. +(*ntheorem boo: + (∀x. x = x) → 0 = 0. +##[ #H; nwhd in H ⊢ %; nauto by H.*) + +ntheorem bboo: + (∀x. x + 0 = x) -> + (∀x, y. x + S y = S (x + y)) → + (∀x, y. x + y = y + x) → + 3 + 2 = 5. +#H; #H1; #H2; nauto by H, H1. H2. 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) ?). + ((λx,y.x y = x y) ? ?) → + ∀x. ((λz. x + x = z + z) ?). ##[ #H; #H1; #H2; #x; nwhd in H H1 H2 ⊢ %; nauto by H, H1, H2. \ No newline at end of file -- 2.39.2