Implemented orphan murdering technique

[helm.git] / helm / software / components / ng_paramodulation / paramod.ml

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 32eff6826f468e9d652f4e5797916deccaba9666..a92bf5dcccb7d9a86c9300c7001b9134810ded82 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -224,12 +224,29 @@ module Paramod (B : Terms.Blob) = struct
                   g_actives g_passives g_current
        else
          (* debug ("Selected fact : " ^ Pp.pp_unit_clause current); *)
+         (*let is_orphan = Sup.orphan_murder bag (fst actives) current in*)
           match 
             if noinfer then bag, Some (current,actives)
-           else Sup.keep_simplified current actives bag maxvar with
-       (*  match Sup.one_pass_simplification current actives bag maxvar with*)
+           else if Sup.orphan_murder bag (fst actives) current then
+             let (id,_,_,_) = current in
+             let bag = Terms.M.add id (current,true) bag in
+               bag, None
+           else Sup.keep_simplified current actives bag maxvar
+         with
+       (*match Sup.one_pass_simplification current actives bag maxvar with*)
              | bag,None -> aux_select bag passives g_passives
              | bag,Some (current,actives) ->
+(*                 if is_orphan then prerr_endline
+                     ("WRONG discarded: " ^ (Pp.pp_unit_clause current));
+                 List.iter (fun x ->
+                              prerr_endline (Pp.pp_unit_clause x))
+                   (fst actives);*)
+
+(*               List.iter (fun (id,_,_,_) -> let (cl,d) =
+                            Terms.M.find id bag in 
+                            if d then prerr_endline
+                              ("WRONG discarded: " ^ (Pp.pp_unit_clause cl)))
+                   (current::fst actives);*)
                  if noinfer then
                    let actives = 
                      current::fst actives,
@@ -241,8 +258,8 @@ module Paramod (B : Terms.Blob) = struct
                      g_actives g_passives current
     in
     
-    (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag);
-      prerr_endline "Active table :"; 
+
+      (*prerr_endline "Active table :"; 
        (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x))
          (fst actives)); *)
 
@@ -297,6 +314,9 @@ module Paramod (B : Terms.Blob) = struct
           let gsteps,esteps = traverse true ([],[]) i in
             (List.rev esteps)@gsteps
         in
+(*       List.iter (fun id -> let (cl,d) =
+                      Terms.M.find id bag in 
+                   if d then prerr_endline (Pp.pp_unit_clause cl)) l;*)
         prerr_endline 
           (Printf.sprintf "Found proof, %fs" 
             (Unix.gettimeofday() -. initial_timestamp));