From: Andrea Asperti Date: Mon, 23 Nov 2009 11:21:27 +0000 (+0000) Subject: Removed dead code X-Git-Tag: make_still_working~3200 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=94c7a260ca00f045a3ec1b371f19de757f83003b;p=helm.git Removed dead code --- diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 53d2958d1..538305815 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -261,7 +261,7 @@ module Superposition (B : Orderings.Blob) = (bag,subst,newside,id) ;; - let rec demodulate ~jump_to_right bag (id, literal, vl, pr) table = + let rec demodulate bag (id, literal, vl, pr) table = match literal with | Terms.Predicate t -> assert false | Terms.Equation (l,r,ty,_) -> @@ -279,39 +279,6 @@ module Superposition (B : Orderings.Blob) = bag,cl ;; - - let demodulate_once_old ~jump_to_right bag (id, literal, vl, pr) table = - match literal with - | Terms.Predicate t -> assert false - | Terms.Equation (l,r,ty,_) -> - let left_position = if jump_to_right then None else - first_position [2] - (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) l - (demod table vl) - in - match left_position with - | Some (newt, subst, id2, dir, pos) -> - begin - match build_clause bag (fun _ -> true) Terms.Demodulation - newt subst id id2 pos dir - with - | None -> assert false - | Some x -> Some (x,false) - end - | None -> - match first_position - [3] (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) r - (demod table vl) - with - | None -> None - | Some (newt, subst, id2, dir, pos) -> - match build_clause bag (fun _ -> true) - Terms.Demodulation newt subst id id2 pos dir - with - | None -> assert false - | Some x -> Some (x,true) - ;; - let parallel_demod table vl bag t pos ctx id = match demod table vl t with | None -> (bag,t,id) @@ -324,42 +291,6 @@ module Superposition (B : Orderings.Blob) = (bag,newside,id) ;; - let demodulate_once ~jump_to_right bag (id, literal, vl, pr) table = - match literal with - | Terms.Predicate t -> assert false - | Terms.Equation (l,r,ty,_) -> - let bag,l,id1 = if jump_to_right then (bag,l,id) else - parallel_positions bag [2] - (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) id l - (parallel_demod table vl) - in - let jump_to_right = id1 = id in - let bag,r,id2 = - parallel_positions bag [3] - (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) id1 r - (parallel_demod table vl) - in - if id = id2 then None - else - let cl,_,_ = Terms.get_from_bag id2 bag in - Some ((bag,cl),jump_to_right) - ;; - - let rec demodulate_old ~jump_to_right bag clause table = - match demodulate_once ~jump_to_right bag clause table with - | None -> bag, clause - | Some ((bag, clause),r) -> demodulate ~jump_to_right:r - bag clause table - ;; -(* - let rec demodulate_old ~jump_to_right bag clause table = - match demodulate_once_old ~jump_to_right bag clause table with - | None -> bag, clause - | Some ((bag, clause),r) -> demodulate_old ~jump_to_right:r - bag clause table - ;; -*) - let are_alpha_eq cl1 cl2 = let get_term (_,lit,_,_) = match lit with @@ -371,28 +302,6 @@ module Superposition (B : Orderings.Blob) = with FoUnif.UnificationFailure _ -> false ;; - let demodulate bag clause table = - demodulate ~jump_to_right:false bag clause table -;; -(* - let (bag1,c1), (bag2,c2) = - demodulate ~jump_to_right:false bag clause table, - demodulate_old ~jump_to_right:false bag clause table - in - if are_alpha_eq c1 c2 then bag1,c1 - else - begin - prerr_endline (Pp.pp_unit_clause clause); - prerr_endline (Pp.pp_unit_clause c1); - prerr_endline (Pp.pp_unit_clause c2); - prerr_endline "Bag1 :"; - prerr_endline (Pp.pp_bag bag1); - prerr_endline "Bag2 :"; - prerr_endline (Pp.pp_bag bag2); - assert false - end - ;; *) - let prof_demodulate = HExtlib.profile ~enable "demodulate";; let demodulate bag clause x = prof_demodulate.HExtlib.profile (demodulate bag clause) x