Implemented orphan murdering technique

diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml
index 89660143de5e426b53f9cdc291442237aed5dc57..6c1aa695ee231f91692a89d46ca9accefb1e09e8 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicParamod.ml
+++ b/helm/software/components/ng_paramodulation/nCicParamod.ml
@@ -38,9 +38,9 @@ let nparamod rdb metasenv subst context t table =
   in
   List.map 
     (fun (bag,i,l) ->
-      List.iter (fun x ->
+      (* List.iter (fun x ->
         print_endline (Pp.pp_unit_clause ~margin:max_int
-          (fst(Terms.M.find x bag)))) l;
+          (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/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));

diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml
index e8035da65c5d510e44495cb5e71a6310f8e4cbda..cb971ea74b4e4bddf8a23a61754b9508721cd81a 100644 (file)
--- a/helm/software/components/ng_paramodulation/pp.ml
+++ b/helm/software/components/ng_paramodulation/pp.ml
@@ -123,7 +123,9 @@ let pp_unit_clause ~formatter:f c =
 let pp_bag ~formatter:f bag = 
   Format.fprintf f "@[<v>";
   Terms.M.iter 
-  (fun _ (c,_) -> pp_unit_clause ~formatter:f c;Format.fprintf f "@;") bag;
+  (fun _ (c,d) -> pp_unit_clause ~formatter:f c;
+     if d then Format.fprintf f " (discarded)@;"
+     else Format.fprintf f "@;") bag;
   Format.fprintf f "@]"
 ;;
 

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 9ccd934e1a8213dd2ab0f15bae92e091b48a3d68..8070b4b5db69a2334ccc1e536009ae38895136ea 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -22,7 +22,7 @@ module Superposition (B : Terms.Blob) =
     
     exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
 
-(*    let debug s = prerr_endline s;;*)
+    let debug s = prerr_endline s;;
     let debug _ = ();;
 
     let rec list_first f = function
@@ -315,16 +315,17 @@ module Superposition (B : Terms.Blob) =
                  if res then res,acc else res,i::acc
     ;;
 
-    let orphan_murder bag cl =
+    let orphan_murder bag actives cl =
       let (id,_,_,_) = cl in
-      let (res,_) = orphan_murder bag [] id in
+      let actives = List.map (fun (i,_,_,_) -> i) actives in
+      let (res,_) = orphan_murder bag actives id in
        if res then debug "Orphan murdered"; res
     ;;
 
     (* demodulate and check for subsumption *)
     let simplify table maxvar bag clause = 
       if is_identity_clause ~unify:false clause then bag,None
-      (* else if orphan_murder bag clause then bag,None *)
+      (* else if orphan_murder bag actives clause then bag,None *)
       else let bag, clause = demodulate bag clause table in
       if is_identity_clause ~unify:false clause then bag,None
       else
@@ -338,6 +339,10 @@ module Superposition (B : Terms.Blob) =
        | bag, None -> let (id,_,_,_) = clause in
            Terms.M.add id (clause,true) bag, None
        | bag, Some clause -> bag, Some clause
+    (*let (id,_,_,_) = clause in
+           if orphan_murder bag clause then
+             Terms.M.add id (clause,true) bag, Some clause
+           else bag, Some clause*)
     ;;
 
     let one_pass_simplification new_clause (alist,atable) bag maxvar =
@@ -366,7 +371,8 @@ module Superposition (B : Terms.Blob) =
        (* Simplification of new_clause with :      *
         * - actives and cl if new_clause is not cl *
         * - only actives otherwise                 *)
-       match simplify atable1 maxvar bag new_clause with
+       match
+         simplify atable1 maxvar bag new_clause with
          | bag,None -> bag,(Some cl, None) (* new_clause has been discarded *)
          | bag,Some clause ->
              (* Simplification of each active clause with clause *

diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli
index 52011c3e806893d3ca2a8854ce135454ea8586a3..149bbb0486f76726169f207cf3d4d13ae8455b46 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -69,5 +69,11 @@ module Superposition (B : Terms.Blob) :
       int ->
       B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option
 
+    val  orphan_murder:
+      B.t Terms.bag ->
+      B.t Terms.unit_clause list ->
+      B.t Terms.unit_clause ->
+      bool
+
 
   end