+
+ let debug_status (_,_,actives,passives,g_actives,g_passives) =
+ lazy
+ ((Printf.sprintf "Number of active goals : %d\n"
+ (List.length g_actives)) ^
+ (Printf.sprintf "Number of passive goals : %d\n"
+ (g_passive_set_cardinal g_passives)) ^
+ (Printf.sprintf "Number of actives : %d\n"
+ (List.length (fst actives))) ^
+ (Printf.sprintf "Number of passives : %d\n"
+ (passive_set_cardinal passives)))
+ ;;
+
+
+ (* we just check if any of the active goals is subsumed by a
+ passive clause, or if any of the passive goal is subsumed
+ by an active or passive clause *)
+ let last_chance (bag,maxvar,actives,passives,g_actives,g_passives) =
+ debug (lazy("Last chance " ^ string_of_float
+ (Unix.gettimeofday())));
+ let active_t = snd actives in
+ let passive_t,wset,_ = passives in
+ let _ = debug
+ (lazy
+ ("Passive set :" ^ (String.concat ";\n"
+ (List.map (fun _,cl -> Pp.pp_unit_clause cl)
+ (WeightPassiveSet.elements wset))))) in
+ let wset = IDX.elems passive_t in
+ let _ = debug
+ (lazy
+ ("Passive table :" ^(String.concat ";\n"
+ (List.map (fun _,cl -> Pp.pp_unit_clause cl)
+ (IDX.ClauseSet.elements wset))))) in
+ let g_passives =
+ WeightPassiveSet.fold
+ (fun (_,x) acc ->
+ if List.exists (Sup.are_alpha_eq x) g_actives then acc
+ else x::acc)
+ (fst g_passives) []
+ in
+ ignore
+ (List.iter
+ (fun x ->
+ ignore
+ (Sup.simplify_goal ~no_demod:true maxvar active_t bag [] x))
+ g_passives);
+ ignore
+ (List.iter
+ (fun x ->
+ ignore
+ (Sup.simplify_goal ~no_demod:true maxvar passive_t bag [] x))
+ (g_actives@g_passives));
+ raise (Stop (Timeout (maxvar,bag)))
+
+ let check_timeout = function
+ | None -> false
+ | Some timeout -> Unix.gettimeofday () > timeout