+ 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
+ in
+ debug
+ (Printf.sprintf "Number of active goals : %d"
+ (List.length g_actives));
+ debug
+ (Printf.sprintf "Number of passive goals : %d"
+ (passive_set_cardinal g_passives));
+ debug
+ (Printf.sprintf "Number of actives : %d" (List.length (fst actives)));
+ debug
+ (Printf.sprintf "Number of passives : %d"
+ (passive_set_cardinal passives));
+ given_clause ~noinfer
+ bag maxvar iterno max_steps timeout
+ actives passives g_actives g_passives
+ ;;
+
+ let paramod ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
+ let initial_timestamp = Unix.gettimeofday () in
+ let passives =
+ add_passive_clauses ~no_weight:true passive_empty_set passives
+ in
+ let g_passives =
+ add_passive_clauses ~no_weight:true passive_empty_set g_passives
+ in
+ let g_actives = [] in
+ let actives = [], IDX.DT.empty in
+ try
+ given_clause ~noinfer:false
+ bag maxvar 0 max_steps timeout actives passives g_actives g_passives
+ with
+ | Sup.Success (bag, _, (i,_,_,_)) ->
+ let l =
+ let rec traverse ongoal (accg,acce) i =
+ match Terms.M.find i bag with
+ | (id,_,_,Terms.Exact _),_ ->
+ if ongoal then [i],acce else
+ if (List.mem i acce) then accg,acce else accg,acce@[i]
+ | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),_ ->
+ if (not ongoal) && (List.mem i acce) then accg,acce
+ else
+ let accg,acce =
+ traverse false (traverse ongoal (accg,acce) i1) i2
+ in
+ if ongoal then i::accg,acce else accg,i::acce
+ in
+ let gsteps,esteps = traverse true ([],[]) i in
+ (List.rev esteps)@gsteps
+ in
+(* List.iter (fun id -> let (cl,d) =
+ Terms.M.find id bag in
+ if d then prerr_endline (Pp.pp_unit_clause cl)) l;*)
+ prerr_endline
+ (Printf.sprintf "Found proof, %fs"
+ (Unix.gettimeofday() -. initial_timestamp));
+ (*
+ prerr_endline "Proof:";
+ List.iter (fun x ->
+ prerr_endline (Pp.pp_unit_clause (fst(Terms.M.find x bag)))) l;
+ *)
+ [ bag, i, l ]
+ | Failure (msg,_bag,_maxvar,iterno) ->
+ prerr_endline msg;
+ prerr_endline (Printf.sprintf "FAILURE in %d iterations" iterno);
+ []
+ ;;
+
+end