X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=801e56b2623ed802a8f0eb71ce93c733d72f59a8;hb=076439def28e649ec384fae038ed021dadd5f75c;hp=42cf063b64f08b3e352693d7a30bebff78025e95;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git diff --git a/matita/components/ng_paramodulation/superposition.ml b/matita/components/ng_paramodulation/superposition.ml index 42cf063b6..801e56b26 100644 --- a/matita/components/ng_paramodulation/superposition.ml +++ b/matita/components/ng_paramodulation/superposition.ml @@ -109,9 +109,9 @@ module Superposition (B : Orderings.Blob) = let visit bag pos ctx id t f = let rec aux bag pos ctx id subst = function | Terms.Leaf _ as t -> - let bag,subst,t,id = f bag t pos ctx id - in assert (subst=[]); bag,t,id - | Terms.Var i as t -> + let bag,subst,t,id = f bag t pos ctx id in + assert (subst=[]); bag,t,id + | Terms.Var _ as t -> let t= Subst.apply_subst subst t in bag,t,id | Terms.Node (hd::l) -> @@ -142,7 +142,18 @@ module Superposition (B : Orderings.Blob) = 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) + (* CSC: to avoid equations of the form ? -> T that + can always be applied and that lead to type-checking errors *) + (match l,r,o with +(* + (Terms.Var _ | Terms.Node (Terms.Var _ ::_)),_,Terms.Gt + | _,(Terms.Var _ | Terms.Node (Terms.Var _ ::_)),Terms.Lt -> assert false +*) + | (Terms.Var _ | Terms.Node (Terms.Var _ ::_)),_,(Terms.Incomparable | Terms.Invertible) -> + Terms.Equation (l, r, ty, Terms.Lt) + | _, (Terms.Var _ | Terms.Node (Terms.Var _ ::_)),(Terms.Incomparable | Terms.Invertible) -> + Terms.Equation (l, r, ty, Terms.Gt) + | _ -> Terms.Equation (l, r, ty, o)) | t -> Terms.Predicate t in let bag, uc = @@ -170,7 +181,7 @@ module Superposition (B : Orderings.Blob) = (IDX.DT.retrieve_generalizations table) subterm in list_first - (fun (dir, (id,lit,vl,_)) -> + (fun (dir, (id,lit,_vl,_)) -> match lit with | Terms.Predicate _ -> assert false | Terms.Equation (l,r,_,o) -> @@ -216,7 +227,7 @@ module Superposition (B : Orderings.Blob) = (IDX.DT.retrieve_generalizations table) subterm in list_first - (fun (dir, ((id,lit,vl,_) as c)) -> + (fun (dir, ((id,lit,_vl,_) as c)) -> debug (lazy("candidate: " ^ Pp.pp_unit_clause c)); match lit with @@ -269,7 +280,7 @@ module Superposition (B : Orderings.Blob) = (bag,subst,newside,id) ;; - let rec demodulate bag (id, literal, vl, pr) table = + let demodulate bag (id, literal, vl, _pr) table = debug (lazy ("demodulate " ^ (string_of_int id))); match literal with | Terms.Predicate t -> (* assert false *) @@ -330,7 +341,7 @@ module Superposition (B : Orderings.Blob) = let is_identity_goal = function | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> Some [] - | _, Terms.Equation (l,r,_,_), vl, proof -> + | _, Terms.Equation (l,r,_,_), _vl, _proof -> (try Some (Unif.unification (* vl *) [] l r) with FoUnif.UnificationFailure _ -> None) | _, Terms.Predicate _, _, _ -> assert false @@ -365,15 +376,20 @@ module Superposition (B : Orderings.Blob) = bag, maxvar, res ;; - let rewrite_eq ~unify l r ty vl table = + (* rewrite_eq check if in table there an equation matching l=r; + used in subsumption and deep_eq. In deep_eq, we need to match + several times times w.r.t. the same table, hence we should refresh + the retrieved clauses, to avoid clashes of variables *) + + let rewrite_eq ~refresh ~unify maxvar l r ty vl table = 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 f b c = let id, dir, l, r, vl = match c with - | (d, (id,Terms.Equation (l,r,ty,_),vl,_))-> id, d, l, r, vl + | (d, (id,Terms.Equation (l,r,_ty,_),vl,_))-> id, d, l, r, vl |_ -> assert false in let reverse = (dir = Terms.Left2Right) = b in @@ -389,8 +405,12 @@ module Superposition (B : Orderings.Blob) = | [] -> None | (id2,dir,c,vl1)::tl -> try + let c,maxvar = if refresh then + let maxvar,_,r = Utils.relocate maxvar vl1 [] in + Subst.apply_subst r c,maxvar + else c,maxvar in let subst = Unif.unification (* (vl@vl1) *) locked_vars c t in - Some (id2, dir, subst) + Some (id2, dir, subst, maxvar) with FoUnif.UnificationFailure _ -> aux tl in aux (cands1 @ cands2) @@ -400,9 +420,9 @@ module Superposition (B : Orderings.Blob) = match lit with | Terms.Predicate _ -> assert false | Terms.Equation (l,r,ty,_) -> - match rewrite_eq ~unify l r ty vl table with + match rewrite_eq ~refresh:false ~unify maxvar l r ty vl table with | None -> None - | Some (id2, dir, subst) -> + | Some (id2, dir, subst, maxvar) -> let id_t = Terms.Node [ Terms.Leaf B.eqP; ty; r; r ] in build_new_clause bag maxvar (fun _ -> true) Terms.Superposition id_t subst id id2 [2] dir @@ -414,38 +434,46 @@ module Superposition (B : Orderings.Blob) = (* id refers to a clause proving contextl l = contextr r *) let rec deep_eq ~unify l r ty pos contextl contextr table acc = + (* let _ = prerr_endline ("pos = " ^ String.concat "," + (List.map string_of_int pos)) in *) match acc with | None -> None | Some(bag,maxvar,(id,lit,vl,p),subst) -> (* prerr_endline ("input subst = "^Pp.pp_substitution subst); *) + (* prerr_endline ("l prima =" ^ Pp.pp_foterm l); *) + (* prerr_endline ("r prima =" ^ Pp.pp_foterm r); *) let l = Subst.apply_subst subst l in let r = Subst.apply_subst subst r in + (* prerr_endline ("l dopo =" ^ Pp.pp_foterm l); *) + (* prerr_endline ("r dopo =" ^ Pp.pp_foterm r); *) try let subst1 = Unif.unification (* vl *) [] l r in let lit = match lit with Terms.Predicate _ -> assert false | Terms.Equation (l,r,ty,o) -> - Terms.Equation (FoSubst.apply_subst subst1 l, - FoSubst.apply_subst subst1 r, ty, o) + let l = Subst.apply_subst subst1 l in + let r = Subst.apply_subst subst1 r in + Terms.Equation (l, r, ty, o) in Some(bag,maxvar,(id,lit,vl,p),Subst.concat subst1 subst) with FoUnif.UnificationFailure _ -> - match rewrite_eq ~unify l r ty vl table with - | Some (id2, dir, subst1) -> + match rewrite_eq ~refresh:true ~unify maxvar l r ty vl table with + | Some (id2, dir, subst1, maxvar) -> (* prerr_endline ("subst1 = "^Pp.pp_substitution subst1); - prerr_endline ("old subst = "^Pp.pp_substitution subst);*) + prerr_endline ("old subst = "^Pp.pp_substitution subst); *) let newsubst = Subst.concat subst1 subst in let id_t = FoSubst.apply_subst newsubst (Terms.Node[Terms.Leaf B.eqP;ty;contextl r;contextr r]) in - (match + (match build_new_clause_reloc bag maxvar (fun _ -> true) Terms.Superposition id_t - subst1 id id2 (pos@[2]) dir - with + subst1 id id2 (pos@[2]) dir + with | Some ((bag, maxvar), c), r -> - (* prerr_endline ("r = "^Pp.pp_substitution r); *) + (* prerr_endline ("creo "^ Pp.pp_unit_clause c); *) + (* prerr_endline ("r = "^Pp.pp_substitution r); *) let newsubst = Subst.flat (Subst.concat r subst) in Some(bag,maxvar,c,newsubst) @@ -480,7 +508,7 @@ module Superposition (B : Orderings.Blob) = let rec orphan_murder bag acc i = match Terms.get_from_bag i bag with | (_,_,_,Terms.Exact _),discarded,_ -> (discarded,acc) - | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),true,_ -> (true,acc) + | (_,_,_,Terms.Step (_,_i1,_i2,_,_,_)),true,_ -> (true,acc) | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),false,_ -> if (List.mem i acc) then (false,acc) else match orphan_murder bag acc i1 with @@ -542,7 +570,7 @@ module Superposition (B : Orderings.Blob) = match simplify ctable maxvar bag c with |bag,None -> (bag,alist,atable) (* an active clause as been discarded *) - |bag,Some c1 -> + |bag,Some _c1 -> bag, c :: alist, IDX.index_unit_clause atable c) (bag,[],IDX.DT.empty) alist in @@ -636,14 +664,14 @@ module Superposition (B : Orderings.Blob) = let bag, clause = if no_demod then bag, clause else demodulate bag clause table in - let _ = debug (lazy ("demodulated goal : " + let _ = debug(lazy ("demodulated goal : " ^ Pp.pp_unit_clause clause)) in if List.exists (are_alpha_eq clause) g_actives then None else match (is_identity_goal clause) with | Some subst -> raise (Success (bag,maxvar,clause,subst)) | None -> - let (id,lit,vl,_) = clause in + let (_id,lit,vl,_) = clause in (* this optimization makes sense only if we demodulated, since in that case the clause should have been turned into an identity *) if (vl = [] && not(no_demod)) @@ -659,12 +687,13 @@ module Superposition (B : Orderings.Blob) = | None -> Some (bag,clause) | Some (bag,maxvar,cl,subst) -> debug (lazy "Goal subsumed"); + debug (lazy ("subst in superpos: " ^ Pp.pp_substitution subst)); raise (Success (bag,maxvar,cl,subst)) (* match is_subsumed ~unify:true bag maxvar clause table with | None -> Some (bag, clause) | Some ((bag,maxvar),c) -> - prerr_endline "Goal subsumed"; + debug (lazy "Goal subsumed"); raise (Success (bag,maxvar,c)) *) ;; @@ -677,10 +706,10 @@ module Superposition (B : Orderings.Blob) = (* =================== inference ===================== *) (* this is OK for both the sup_left and sup_right inference steps *) - let superposition table varlist subterm pos context = + 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*))) -> + (fun (dir, (id,lit,_vl,_ (*as uc*))) -> match lit with | Terms.Predicate _ -> assert false | Terms.Equation (l,r,_,o) ->