From d35aca0e979a9c7edbc60c44040360d52be8ca82 Mon Sep 17 00:00:00 2001 From: denes Date: Fri, 31 Jul 2009 21:37:53 +0000 Subject: [PATCH] Fixed (yet another) nasty bug, in deep_eq this time --- .../ng_paramodulation/superposition.ml | 33 +++++++++---------- 1 file changed, 15 insertions(+), 18 deletions(-) diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 51269d2b3..fd7be3b7e 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -123,6 +123,7 @@ module Superposition (B : Orderings.Blob) = let bag, cl = Terms.add_to_bag cl bag in + debug (lazy (Pp.pp_clause cl)); Some (bag, maxvar, cl, literal) else ((*prerr_endline ("Filtering: " ^ Pp.pp_foterm t);*)None) @@ -228,7 +229,7 @@ module Superposition (B : Orderings.Blob) = | Some ((bag, id, lit),jump) -> demod_lit ~jump_to_right:jump bag id lit clause_ctx in - (*let cmp_bag,cmp_cl = match nlit,plit with + (*match nlit,plit with |[],[lit,_] -> let bag, id, lit = demod_lit ~jump_to_right:false bag id lit (fun l -> nlit, [l,true]) in @@ -239,8 +240,7 @@ module Superposition (B : Orderings.Blob) = in let cl,_,_ = Terms.get_from_bag id bag in bag,cl - |_ -> assert false - in*) + |_ -> assert false*) let nlit,_,bag,id = if nlit = [] then nlit,[],bag,id else List.fold_left (fun (pre,post,bag,id) (lit,sel) -> @@ -354,7 +354,7 @@ module Superposition (B : Orderings.Blob) = let rec deep_eq ~unify l r ty pos contextl contextr table acc = match acc with | None -> None - | Some(bag,maxvar,(id,nlit,plit,vl,p),subst) -> + | Some(bag,maxvar,(id,nlit,plit,vl,p as cl),subst) -> let l = Subst.apply_subst subst l in let r = Subst.apply_subst subst r in try @@ -364,9 +364,9 @@ module Superposition (B : Orderings.Blob) = | [Terms.Equation (l,r,ty,o),_],[] -> Terms.Equation (FoSubst.apply_subst subst1 l, FoSubst.apply_subst subst1 r, ty, o) - | _ -> assert false + | _ -> debug (lazy (Pp.pp_clause cl));assert false in - Some(bag,maxvar,(id,[],[lit,true],vl,p),Subst.concat subst1 subst) + Some(bag,maxvar,(id,[lit,true],[],vl,p),Subst.concat subst1 subst) with FoUnif.UnificationFailure _ -> match rewrite_eq ~unify l r ty vl table with | Some (id2, dir, subst1) -> @@ -378,7 +378,7 @@ module Superposition (B : Orderings.Blob) = (match build_clause ~fresh:true bag maxvar (fun _ -> true) Terms.Superposition id_t - subst1 id id2 (pos@[2]) dir (fun l -> [],[l,true]) + subst1 id id2 (pos@[2]) dir (fun l -> [l,true],[]) with | Some (bag, maxvar, c, _) -> Some(bag,maxvar,c,newsubst) @@ -604,7 +604,7 @@ module Superposition (B : Orderings.Blob) = (* this is OK for both the sup_left and sup_right inference steps *) let superposition table varlist is_pos subterm pos context = let cands = IDX.DT.retrieve_unifiables table subterm in - let res = HExtlib.filter_map + HExtlib.filter_map (fun (dir, is_cand_pos, _, (id,nlit,plit,vl,_ (*as uc*))) -> match nlit,plit with | [],[Terms.Equation (l,r,_,o),_] -> @@ -629,10 +629,6 @@ module Superposition (B : Orderings.Blob) = with FoUnif.UnificationFailure _ -> None) | _ -> assert false) (IDX.ClauseSet.elements cands) - in - debug (lazy (string_of_int (List.length (IDX.ClauseSet.elements cands)) ^ " candidates")); - debug (lazy (string_of_int (List.length res) ^ " results")); - res ;; (* Superposes selected equation with equalities in table *) @@ -732,17 +728,18 @@ module Superposition (B : Orderings.Blob) = * variables clauses refer to are known. *) let bag, (id,nlit,plit,vl,_) = Terms.add_to_bag fresh_current bag in (* We superpose current with active clauses *) - let bag, maxvar, _, _, new_clauses = - if nlit = [] then bag,maxvar,[],[],new_clauses + let bag, maxvar, _, _, additional_new_clauses = + if nlit = [] then bag,maxvar,[],[],[] else List.fold_left - (superpose_literal id vl atable false) (bag,maxvar,[],List.tl nlit,new_clauses) nlit + (superpose_literal id vl atable false) (bag,maxvar,[],List.tl nlit,[]) nlit in - let bag, maxvar, _, _, new_clauses = - if plit = [] then bag,maxvar,[],[],new_clauses + let bag, maxvar, _, _, additional_new_clauses = + if plit = [] then bag,maxvar,[],[],[] else List.fold_left - (superpose_literal id vl atable true) (bag,maxvar,[],List.tl plit,new_clauses) plit + (superpose_literal id vl atable true) (bag,maxvar,[],List.tl plit,additional_new_clauses) plit in debug (lazy "Another superposition"); + let new_clauses = new_clauses@additional_new_clauses in debug (lazy (Printf.sprintf "Demodulating %d clauses" (List.length new_clauses))); let bag, new_clauses = -- 2.39.2