(* $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;;
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 =