- if noinfer then bag, Some (current,actives)
- else if Sup.orphan_murder bag (fst actives) current then
- let (id,_,_,_) = current in
- let bag = Terms.M.add id (current,true) 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);*)
+ 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 "Orphan murdered" in
+ let bag = Terms.replace_in_bag (current,true) 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);*)