+
+ (* e = select P *
+ * e' = demod A e *
+ * A' = demod [e'] A *
+ * A'' = A' + e' *
+ * e'' = fresh e' *
+ * new = supright e'' A'' *
+ * new'= demod A'' new *
+ * P' = P + new' *)
+ debug (lazy "Forward infer step...");
+ debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives)))));
+ let bag, maxvar, actives, new_clauses =
+ Sup.infer_right bag maxvar current actives
+ in
+ debug (lazy "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 ->
+ match
+ Sup.simplify_goal ~no_demod:false maxvar (snd actives) bag acc c
+ with
+ | None -> bag, acc
+ | Some (bag,c1) -> bag,if c==c1 then c::acc else c::c1::acc)
+ (bag,[]) g_actives
+ in
+ let ctable = IDX.index_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 m g ([current],ctable) in
+ bag,m,ng@acc)
+ (bag,maxvar,[]) g_actives
+ in
+ let bag = Terms.replace_in_bag (current,false,iterno) bag in
+ bag, maxvar, actives,
+ add_passive_clauses passives new_clauses, g_actives,
+ add_passive_goals g_passives new_goals
+ ;;
+
+ let rec given_clause ~useage ~noinfer
+ bag maxvar iterno weight_picks max_steps timeout
+ actives passives g_actives g_passives
+ =
+ let iterno = iterno + 1 in
+ if iterno = max_steps then raise (Stop (Timeout (maxvar,bag)));
+ (* timeout check: gettimeofday called only if timeout set *)
+ if timeout <> None &&
+ (match timeout with
+ | None -> assert false
+ | Some timeout -> Unix.gettimeofday () > timeout) then
+ if noinfer then
+ begin
+ debug
+ (lazy("Last chance: all is indexed " ^ string_of_float
+ (Unix.gettimeofday())));
+ let maxgoals = 100 in
+ ignore(List.fold_left
+ (fun (acc,i) x ->
+ if i < maxgoals then
+ ignore(Sup.simplify_goal ~no_demod:true
+ maxvar (snd actives) bag acc x)
+ else
+ ();
+ x::acc,i+1)
+ ([],0) g_actives);
+ raise (Stop (Timeout (maxvar,bag)))
+ end
+ else if false then (* activates last chance strategy *)
+ begin
+ debug (lazy("Last chance: "^string_of_float (Unix.gettimeofday())));
+ given_clause ~useage ~noinfer:true bag maxvar iterno weight_picks max_steps
+ (Some (Unix.gettimeofday () +. 20.))
+ actives passives g_actives g_passives;
+ raise (Stop (Timeout (maxvar,bag)));
+ end
+ else raise (Stop (Timeout (maxvar,bag)));
+
+ let use_age = useage && (weight_picks = (iterno / 6 + 1)) in
+ let weight_picks = if use_age then 0 else weight_picks+1
+ in
+
+ let rec aux_select bag passives g_passives =
+ let backward,(weight,current),passives,g_passives =
+ select ~use_age passives g_passives
+ in
+ if use_age && weight > monster then
+ let bag,cl = Terms.add_to_bag current bag in
+ if backward then
+ aux_select bag passives (add_passive_clause g_passives cl)
+ else
+ aux_select bag (add_passive_clause passives cl) g_passives
+ else
+ let bag = Terms.replace_in_bag (current,false,iterno) bag in
+ if backward then
+ let _ = debug (lazy("Selected goal : " ^ Pp.pp_clause current)) in
+ 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 iterno
+ else
+ let _ = debug (lazy("Selected fact : " ^ Pp.pp_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 _ = 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