in
let module WeightPassiveSet = Set.Make(WeightOrderedPassives) in
let module AgePassiveSet = Set.Make(AgeOrderedPassives) in
in
let module WeightPassiveSet = Set.Make(WeightOrderedPassives) in
let module AgePassiveSet = Set.Make(AgeOrderedPassives) in
- let add_passive_clause (passives_w,passives_a) cl =
- let cl = Utils.mk_passive_clause cl in
+ let add_passive_clause ?(no_weight=true) (passives_w,passives_a) cl =
+ let cl = if no_weight then (0,cl)
+ else Utils.mk_passive_clause cl in
WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a
in
let remove_passive_clause (passives_w,passives_a) cl =
WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a
in
let remove_passive_clause (passives_w,passives_a) cl =
let (proof,ty) = B.saturate t ty in
let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
let bag, c = Utils.add_to_bag bag c in
let (proof,ty) = B.saturate t ty in
let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
let bag, c = Utils.add_to_bag bag c in