Implemented orphan murder test (clauses are not discarded for now)

[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 d85c5627a4e4b4e97d1a9e667253dac41cd7aecb..51bd67286f0dc498886df771a0ae18cd2f91a8a8 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -11,7 +11,7 @@
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
-let debug s = prerr_endline s ;;
+(* let debug s = prerr_endline s ;;*)
 let debug _ = ();;
     
 module Paramod (B : Terms.Blob) = struct
@@ -49,8 +49,10 @@ module Paramod (B : Terms.Blob) = struct
       passives_w,passives_a
   ;;
 
-  let add_passive_clauses (passives_w,passives_a) new_clauses =
-    let new_clauses_w,new_clauses_a = List.fold_left add_passive_clause
+  let add_passive_clauses ?(no_weight=false)
+      (passives_w,passives_a) new_clauses =
+    let new_clauses_w,new_clauses_a =
+      List.fold_left (add_passive_clause ~no_weight)
       (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
     in
       (WeightPassiveSet.union new_clauses_w passives_w,
@@ -172,22 +174,22 @@ module Paramod (B : Terms.Blob) = struct
 
     let use_age = iterno mod 10 = 0 in
 
-    let rec aux_select passives g_passives =
+    let rec aux_select bag passives g_passives =
       let backward,current,passives,g_passives =
        select ~use_age:false passives g_passives
       in
        if backward then
         match Sup.simplify_goal maxvar (snd actives) bag g_actives current with
-           | None -> aux_select passives g_passives
-           | Some x -> let bag,g_current = x in
+           | None -> aux_select bag passives g_passives
+           | Some (bag,g_current) ->
                backward_infer_step bag maxvar actives passives
                  g_actives g_passives g_current
        else
          (* debug ("Selected fact : " ^ Pp.pp_unit_clause current); *)
           match Sup.keep_simplified current actives bag maxvar with
        (*  match Sup.one_pass_simplification current actives bag maxvar with*)
-             | None -> aux_select passives g_passives
-             | Some x -> let (current, bag, actives) = x in
+             | bag,None -> aux_select bag passives g_passives
+             | bag,Some (current,actives) ->
                  forward_infer_step bag maxvar actives passives
                                     g_actives g_passives current
     in
@@ -198,7 +200,7 @@ module Paramod (B : Terms.Blob) = struct
          (fst actives)); *)
 
     let bag,maxvar,actives,passives,g_actives,g_passives =      
-      aux_select passives g_passives
+      aux_select bag passives g_passives
     in
       debug
        (Printf.sprintf "Number of active goals : %d"
@@ -218,8 +220,12 @@ module Paramod (B : Terms.Blob) = struct
 
   let paramod ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
     let initial_timestamp = Unix.gettimeofday () in
-    let passives = add_passive_clauses passive_empty_set passives in
-    let g_passives = add_passive_clauses passive_empty_set g_passives in
+    let passives =
+      add_passive_clauses ~no_weight:true passive_empty_set passives
+    in
+    let g_passives =
+      add_passive_clauses ~no_weight:true passive_empty_set g_passives
+    in
     let g_actives = [] in
     let actives = [], IDX.DT.empty in
     try