- let (current, bag, actives),passives = aux_simplify passives
- in
- debug ("Fact after simplification :"
- ^ Pp.pp_unit_clause current);
- let bag, maxvar, actives, new_clauses =
- Sup.infer_right bag maxvar current actives
- in
- debug "Demodulating goals with actives...";
- (* keep goals demodulated w.r.t. actives and check if solved *)
- let bag, g_actives =
- List.fold_left
- (fun (bag,acc) c ->
- let bag, c = Sup.simplify_goal maxvar (snd actives) bag c in
- bag, c::acc)
- (bag,[]) g_actives
- in
- let ctable = IDX.index_unit_clause IDX.DT.empty current in
- let bag, maxvar, new_goals =
- List.fold_left
- (fun (bag,m,acc) g ->
- let bag, m, ng = Sup.infer_left bag maxvar g
- ([current],ctable) in
- bag,m,ng@acc)
- (bag,maxvar,[]) g_actives
- in
- let new_clauses = List.fold_left add_passive_clause
- PassiveSet.empty new_clauses in
- let new_goals = List.fold_left add_passive_clause
- PassiveSet.empty new_goals in
- bag, maxvar, actives,
- PassiveSet.union new_clauses passives,
- PassiveSet.union new_goals g_passives
+ if backward then
+ match
+ if noinfer then
+ if weight > monster then None else Some (bag,current)
+ else
+ Sup.simplify_goal
+ ~no_demod:false maxvar (snd actives) bag g_actives current
+ with
+ | None -> aux_select bag passives g_passives
+ | Some (bag,g_current) ->
+ if noinfer then
+ let g_actives = g_current :: g_actives in
+ bag,maxvar,actives,passives,g_actives,g_passives
+ else
+ backward_infer_step bag maxvar actives passives
+ g_actives g_passives g_current
+ else
+ let _ = debug ("Selected fact : " ^ Pp.pp_unit_clause current) in
+ (*let is_orphan = Sup.orphan_murder bag (fst actives) current in*)
+ match
+ 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 (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);*)
+
+(* 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_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
+ in
+
+
+ (*prerr_endline "Active table :";
+ (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x))
+ (fst actives)); *)
+
+ let bag,maxvar,actives,passives,g_actives,g_passives =
+ aux_select bag passives g_passives