- let rec given_clause bag maxvar actives passives g_actives g_passives =
- (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag);
- prerr_endline "Active table :";
- (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x))
- (fst actives)); *)
- incr nb_iter; if !nb_iter = max_nb_iter then
- raise (Failure "No iterations left !");
- if Unix.gettimeofday () > timeout then
- raise (Failure "Timeout !");
-
-
- let rec aux_select passives g_passives =
- let backward,current,passives,g_passives = select passives g_passives in
- if backward then
- match Sup.simplify_goal maxvar (snd actives) bag g_actives current with
- | None -> aux_select passives g_passives
- | Some x -> let bag,g_current = x in
- backward_infer_step bag maxvar actives passives
- g_actives g_passives g_current
+ 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
+
+ let rec given_clause ~useage
+ bag maxvar iterno weight_picks max_steps timeout
+ actives passives g_actives g_passives
+ =
+ let iterno = iterno + 1 in
+ if iterno = max_steps || check_timeout timeout then
+ last_chance (bag,maxvar,actives,passives,g_actives,g_passives)
+ else
+ 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:IDX.DT.t * WeightPassiveSet.t * AgePassiveSet.t)
+ 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_goal g_passives cl)
+ else
+ aux_select bag (add_passive_clause passives cl) g_passives