Removed dead code

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 53d2958d1c2d1788fc2ff36ac843a9d2b864aafe..538305815261256e03d076b28742e12949963cb5 100644 (file)
--- 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