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 =
given_clause bag maxvar actives passives g_actives g_passives
in
- let mk_clause bag maxvar (t,ty) =
+ let mk_clause ?(no_weight=false) bag maxvar (t,ty) =
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 bag, maxvar, goal = mk_clause Terms.M.empty 0 t in
let g_actives = [] in
let g_passives =
- passive_singleton (Utils.mk_passive_clause goal)
+ passive_singleton (0,goal)
in
let passives, bag, maxvar =
List.fold_left