X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;fp=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=8bbf6e1606162c47eca6f15a8490e1ba2f7fa3f3;hb=f2039f5c9e68dc69c86c77758bc521acd30e973f;hp=4a688620590f94506e4ae07c7ec47bb5fe281269;hpb=0842258ce37ce992a0d52c813a9a5cb4c3f2bb52;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 4a6886205..8bbf6e160 100644
--- 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 =