- (* 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 "Forward infer step...";
- let bag, maxvar, actives, passives, g_passives =
- match select passives with
- | None -> bag, maxvar, actives, passives, g_passives
- | Some (current, passives) ->
- debug ("Selected fact : " ^ Pp.pp_unit_clause current);
- match Sup.forward_simplify (snd actives) bag current with
- | None -> debug ("Discarded fact");
- bag, maxvar, actives, passives, g_passives
- | Some (bag, current) ->
- debug ("Fact after simplification :" ^ Pp.pp_unit_clause current);
- let bag, maxvar, actives, new_clauses =
- Sup.infer_right bag maxvar current actives
- in
- let ctable = IDX.index_unit_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 maxvar g
- ([current],ctable) in
- bag,m,ng@acc)
- (bag,maxvar,[]) g_actives
- in
- let new_clauses = List.fold_left add_passive_clause
- PassiveSet.empty new_clauses in
- let new_goals = List.fold_left add_passive_clause
- PassiveSet.empty new_goals in
- bag, maxvar, actives,
- PassiveSet.union new_clauses passives,
- PassiveSet.union new_goals g_passives
+ 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
+ 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
+ (lazy(Printf.sprintf "Number of active goals : %d"
+ (List.length g_actives)));
+ debug
+ (lazy(Printf.sprintf "Number of passive goals : %d"
+ (passive_set_cardinal g_passives)));
+ debug
+ (lazy(Printf.sprintf "Number of actives : %d" (List.length (fst actives))));
+ debug
+ (lazy(Printf.sprintf "Number of passives : %d"
+ (passive_set_cardinal passives)));
+ given_clause ~useage ~noinfer
+ bag maxvar iterno weight_picks max_steps timeout
+ actives passives g_actives g_passives
+ ;;
+
+ let paramod ~useage ~max_steps ~print_problem ?timeout goal hypotheses =
+ let initial_timestamp = Unix.gettimeofday () in
+ let bag = Terms.empty_bag in
+ let maxvar = 0 in
+ let build_clause (bag,maxvar,l) (t,(nlit,plit)) =
+ let c,maxvar = Utils.mk_clause maxvar nlit plit t in
+ let bag,c = Terms.add_to_bag c bag in
+ (bag,maxvar,c::l)
+ in
+ let bag,maxvar,hypotheses = List.fold_left build_clause (bag,maxvar,[]) hypotheses in
+ let bag,maxvar,goals = build_clause (bag,maxvar,[]) goal in
+ let goal = match goals with | [g] -> g | _ -> assert false in
+ let passives =
+ add_passive_clauses ~no_weight:true passive_empty_set hypotheses
+ in
+ let g_passives =
+ add_passive_goal ~no_weight:true passive_empty_set goal