From: Andrea Asperti Date: Fri, 26 Jun 2009 11:02:11 +0000 (+0000) Subject: deep subsumption activated X-Git-Tag: make_still_working~3786 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=895efaa0e4375de535226002fcb1ed14d1fa8301;p=helm.git deep subsumption activated --- diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml index 2536f6443..89660143d 100644 --- a/helm/software/components/ng_paramodulation/nCicParamod.ml +++ b/helm/software/components/ng_paramodulation/nCicParamod.ml @@ -24,6 +24,7 @@ let nparamod rdb metasenv subst context t table = = NCicBlob.NCicBlob(C) in let module P = Paramod.Paramod(B) in + let module Pp = Pp.Pp(B) in let bag, maxvar = Terms.M.empty, 0 in let (bag,maxvar), passives = HExtlib.list_mapi_acc (fun x _ a -> P.mk_passive a x) (bag,maxvar) table @@ -37,6 +38,9 @@ let nparamod rdb metasenv subst context t table = in List.map (fun (bag,i,l) -> + List.iter (fun x -> + print_endline (Pp.pp_unit_clause ~margin:max_int + (fst(Terms.M.find x bag)))) l; let stamp = Unix.gettimeofday () in let proofterm = NCicProof.mk_proof bag i l in prerr_endline (Printf.sprintf "Got proof term in %fs" diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml index 1e50999e9..37abd6edf 100644 --- a/helm/software/components/ng_paramodulation/nCicProof.ml +++ b/helm/software/components/ng_paramodulation/nCicProof.ml @@ -71,9 +71,16 @@ match t with | Terms.Leaf _ | Terms.Var _ -> -(* prerr_endline ("term: " ^ ppfot ft); *) + let module Pp = + Pp.Pp(NCicBlob.NCicBlob( + struct + let metasenv = [] let subst = [] let context = [] + end)) + in + prerr_endline ("term: " ^ Pp.pp_foterm ft); prerr_endline ("path: " ^ String.concat "," (List.map string_of_int p1)); + prerr_endline ("leading to: " ^ Pp.pp_foterm t); assert false | Terms.Node l -> let l = @@ -150,7 +157,7 @@ if ongoal then id1,id,get_literal id1 else id,id1,(lit,vl,proof) in - let vl = if ongoal then Subst.filter subst vl else vl in + let vl = if ongoal then [](*Subst.filter subst vl*) else vl in let proof_of_id id = let vars = List.rev (vars_of id seen) in let args = List.map (Subst.apply_subst subst) vars in diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index d058be253..6a4cc0d79 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -252,24 +252,33 @@ module Superposition (B : Terms.Blob) = let rec deep_eq ~unify l r ty pos contextl contextr table acc = match acc with | None -> None - | Some(bag,maxvar,[],subst) -> assert false - | Some(bag,maxvar,(id,_,vl,_)::clauses,subst) -> + | Some(bag,maxvar,(id,lit,vl,p),subst) -> let l = Subst.apply_subst subst l in let r = Subst.apply_subst subst r in try let subst1,vl1 = Unif.unification vl [] l r in - Some(bag,maxvar,clauses,Subst.concat subst1 subst) + 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) + in + Some(bag,maxvar,(id,lit,vl1,p),Subst.concat subst1 subst) with FoUnif.UnificationFailure _ -> match rewrite_eq ~unify l r ty vl table with | Some (id2, dir, subst1) -> + let newsubst = Subst.concat subst1 subst in let id_t = - Terms.Node[Terms.Leaf B.eqP;ty;contextl r;contextr r] in + FoSubst.apply_subst newsubst + (Terms.Node[Terms.Leaf B.eqP;ty;contextl r;contextr r]) + in (match build_new_clause bag maxvar (fun _ -> true) - Terms.Superposition id_t subst1 [] id id2 (2::pos) dir + Terms.Superposition id_t + subst1 [] id id2 (pos@[2]) dir with | Some ((bag, maxvar), c) -> - Some(bag,maxvar,c::clauses,Subst.concat subst1 subst) + Some(bag,maxvar,c,newsubst) | None -> assert false) | None -> match l,r with @@ -436,7 +445,7 @@ module Superposition (B : Terms.Blob) = let bag, clause = demodulate bag clause table in if (is_identity_clause ~unify:true clause) then raise (Success (bag, maxvar, clause)) -(* + else let (id,lit,vl,_) = clause in let l,r,ty = @@ -445,21 +454,21 @@ module Superposition (B : Terms.Blob) = | _ -> assert false in match deep_eq ~unify:true l r ty [] (fun x -> x) (fun x -> x) - table (Some(bag,maxvar,[clause],Subst.id_subst)) with + table (Some(bag,maxvar,clause,Subst.id_subst)) with | None -> if List.exists (are_alpha_eq clause) g_actives then None else Some (bag, clause) | Some (bag,maxvar,cl,subst) -> - debug "Goal subsumed"; - raise (Success (bag,maxvar,List.hd cl)) -*) + prerr_endline "Goal subsumed"; + raise (Success (bag,maxvar,cl)) + (* else match is_subsumed ~unify:true bag maxvar clause table with | None -> if List.exists (are_alpha_eq clause) g_actives then None else Some (bag, clause) | Some ((bag,maxvar),c) -> - debug "Goal subsumed"; - raise (Success (bag,maxvar,c)) + prerr_endline "Goal subsumed"; + raise (Success (bag,maxvar,c))*) ;; (* =================== inference ===================== *)