- begin
- prerr_endline("Last chance: "^string_of_float (Unix.gettimeofday()));
- given_clause ~noinfer:true bag maxvar iterno max_steps None
- actives passives g_actives g_passives
- (*raise (Failure ("Timeout !",bag,maxvar,iterno))*)
- end
- else
+ if noinfer then
+ begin
+ debug
+ ("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 (Failure (("Last chance: failed over " ^
+ string_of_int maxgoals^ " goal " ^
+ string_of_float (Unix.gettimeofday())),bag,maxvar,0));
+ end
+ else if false then (* activates last chance strategy *)
+ begin
+ debug("Last chance: "^string_of_float (Unix.gettimeofday()));
+ given_clause ~noinfer:true bag maxvar iterno max_steps
+ (Some (Unix.gettimeofday () +. 20.))
+ actives passives g_actives g_passives;
+ raise (Failure ("Timeout !",bag,maxvar,iterno))
+ end
+ else raise (Failure ("Timeout !",bag,maxvar,iterno));