(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
-let debug s = prerr_endline s ;;
-let debug _ = ();;
+let debug s = prerr_endline (Lazy.force s) ;;
+let debug _ = ();;
let monster = 100;;
let backward_infer_step bag maxvar actives passives
g_actives g_passives g_current iterno =
(* superposition left, simplifications on goals *)
- debug "infer_left step...";
+ debug (lazy "infer_left step...");
let bag, maxvar, new_goals =
Sup.infer_left bag maxvar g_current actives
in
- debug "Performed infer_left step";
+ debug (lazy "Performed infer_left step");
let bag = Terms.replace_in_bag (g_current,false,iterno) bag in
bag, maxvar, actives, passives, g_current::g_actives,
(add_passive_goals g_passives new_goals)
* new = supright e'' A'' *
* new'= demod A'' new *
* P' = P + new' *)
- debug "Forward infer step...";
+ debug (lazy "Forward infer step...");
+ debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives)))));
let bag, maxvar, actives, new_clauses =
Sup.infer_right bag maxvar current actives
in
- debug "Demodulating goals with actives...";
+ debug (lazy "Demodulating goals with actives...");
(* keep goals demodulated w.r.t. actives and check if solved *)
let bag, g_actives =
List.fold_left
(bag,maxvar,[]) g_actives
in
let bag = Terms.replace_in_bag (current,false,iterno) bag in
+ (* prerr_endline (Pp.pp_bag bag); *)
bag, maxvar, actives,
add_passive_clauses passives new_clauses, g_actives,
add_passive_goals g_passives new_goals
if noinfer then
begin
debug
- ("Last chance: all is indexed " ^ string_of_float
- (Unix.gettimeofday()));
+ (lazy("Last chance: all is indexed " ^ string_of_float
+ (Unix.gettimeofday())));
let maxgoals = 100 in
ignore(List.fold_left
(fun (acc,i) x ->
end
else if false then (* activates last chance strategy *)
begin
- debug("Last chance: "^string_of_float (Unix.gettimeofday()));
+ 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;
else
let bag = Terms.replace_in_bag (current,false,iterno) bag in
if backward then
- let _ = debug ("Selected goal : " ^ Pp.pp_unit_clause current) in
+ let _ = debug (lazy("Selected goal : " ^ Pp.pp_unit_clause current)) in
match
if noinfer then
if weight > monster then None else Some (bag,current)
backward_infer_step bag maxvar actives passives
g_actives g_passives g_current iterno
else
- let _ = debug ("Selected fact : " ^ Pp.pp_unit_clause current) in
+ let _ = debug (lazy("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 _ = debug "Orphan murdered" in
+ 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
aux_select bag passives g_passives
in
debug
- (Printf.sprintf "Number of active goals : %d"
- (List.length g_actives));
+ (lazy(Printf.sprintf "Number of active goals : %d"
+ (List.length g_actives)));
debug
- (Printf.sprintf "Number of passive goals : %d"
- (passive_set_cardinal g_passives));
+ (lazy(Printf.sprintf "Number of passive goals : %d"
+ (passive_set_cardinal g_passives)));
debug
- (Printf.sprintf "Number of actives : %d" (List.length (fst actives)));
+ (lazy(Printf.sprintf "Number of actives : %d" (List.length (fst actives))));
debug
- (Printf.sprintf "Number of passives : %d"
- (passive_set_cardinal passives));
+ (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 ?timeout (bag,maxvar) ~g_passives ~passives =
- let initial_timestamp = Unix.gettimeofday () in
+ let _initial_timestamp = Unix.gettimeofday () in
let passives =
add_passive_clauses ~no_weight:true passive_empty_set passives
in
(Printf.sprintf "Id : %d, selected at %d, weight %d by %s"
id it (Order.compute_unit_clause_weight cl)
(Pp.pp_proof_step proof))) l;*)
- prerr_endline
- (Printf.sprintf "Found proof, %fs"
- (Unix.gettimeofday() -. initial_timestamp));
(*
prerr_endline "Proof:";
List.iter (fun x ->