- if noinfer then bag, Some (current,actives)
- else Sup.keep_simplified current actives bag maxvar with
- (* match Sup.one_pass_simplification current actives bag maxvar with*)
- | bag,None -> aux_select bag passives g_passives
- | bag,Some (current,actives) ->
- if noinfer then
- let actives =
- current::fst actives,
- IDX.index_unit_clause (snd actives) current
- in
- bag,maxvar,actives,passives,g_actives,g_passives
- else
- forward_infer_step bag maxvar actives passives
- g_actives g_passives current
+ if noinfer then
+ if weight > monster then bag,None
+ else bag, Some (current,actives)
+ else if Sup.orphan_murder bag (fst actives) current then
+ let _ = debug (lazy "Orphan murdered") in
+ let bag = Terms.replace_in_bag (current,true,iterno) bag in
+ bag, None
+ else Sup.keep_simplified current actives bag maxvar
+ with
+ (*match Sup.one_pass_simplification current actives bag maxvar with*)
+ | bag,None -> aux_select bag passives g_passives
+ | bag,Some (current,actives) ->
+(* if is_orphan then prerr_endline
+ ("WRONG discarded: " ^ (Pp.pp_unit_clause current));
+ List.iter (fun x ->
+ prerr_endline (Pp.pp_unit_clause x))
+ (fst actives);*)
+
+(* List.iter (fun (id,_,_,_) -> let (cl,d) =
+ Terms.M.find id bag in
+ if d then prerr_endline
+ ("WRONG discarded: " ^ (Pp.pp_unit_clause cl)))
+ (current::fst actives);*)
+ if noinfer then
+ let actives =
+ current::fst actives,
+ IDX.index_clause (snd actives) current
+ in
+ bag,maxvar,actives,passives,g_actives,g_passives
+ else
+ forward_infer_step bag maxvar actives passives
+ g_actives g_passives current iterno