Fixed nasty bug in superposition and freshing of clauses

[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 4a688620590f94506e4ae07c7ec47bb5fe281269..8bbf6e1606162c47eca6f15a8490e1ba2f7fa3f3 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -12,7 +12,7 @@
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
 let debug s = prerr_endline (Lazy.force s) ;;
-(* let debug _ = ();; *)
+let debug _ = ();;
 
 let monster = 100;;
     
@@ -66,14 +66,16 @@ module Paramod (B : Orderings.Blob) = struct
 
   let add_passive_clause ?(bonus_weight=0) (passives_w,passives_a) cl =
     let (w,cl) = Clauses.mk_passive_clause cl in
-    let cl = (w+bonus_weight,cl) in
-    WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a
+    (* let cl = (w+bonus_weight,cl) in *)
+    let cl = if bonus_weight = 0 then (w,cl) else (0,cl) in
+   WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a
   ;;
 
   let add_passive_goal ?(bonus_weight=0) (passives_w,passives_a) g =
     let (w,g) = Clauses.mk_passive_goal g in
-    let g = (w+bonus_weight,g) in
-    WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a
+    (* let g = (w+bonus_weight,g) in *)
+    let g = if bonus_weight = 0 then (w,g) else (0,g) in
+   WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a
   ;;
 
   let remove_passive_clause (passives_w,passives_a) cl =