(* $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;;
type bag = t Terms.bag * int
val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
- val paramod :
+ val paramod :
+ useage:bool ->
max_steps:int ->
?timeout:float ->
bag ->
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
| Some (bag,c1) -> bag,if c==c1 then c::acc else c::c1::acc)
(bag,[]) g_actives
in
- let ctable = IDX.index_unit_clause IDX.DT.empty current in
+ let ctable = IDX.index_unit_clause maxvar IDX.DT.empty current in
let bag, maxvar, new_goals =
List.fold_left
(fun (bag,m,acc) g ->
(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
;;
- let rec given_clause ~noinfer
+ let rec given_clause ~useage ~noinfer
bag maxvar iterno weight_picks max_steps timeout
actives passives g_actives g_passives
=
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()));
- given_clause ~noinfer:true bag maxvar iterno weight_picks max_steps
+ 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 = weight_picks = (iterno / 6 + 1) in
+ let use_age = useage && (weight_picks = (iterno / 6 + 1)) in
let weight_picks = if use_age then 0 else weight_picks+1
in
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
if noinfer then
let actives =
current::fst actives,
- IDX.index_unit_clause (snd actives) current
+ IDX.index_unit_clause maxvar (snd actives) current
in
bag,maxvar,actives,passives,g_actives,g_passives
else
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));
- given_clause ~noinfer
+ (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 ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
- let initial_timestamp = Unix.gettimeofday () in
+ let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
+ let _initial_timestamp = Unix.gettimeofday () in
let passives =
add_passive_clauses ~no_weight:true passive_empty_set passives
in
let g_actives = [] in
let actives = [], IDX.DT.empty in
try
- given_clause ~noinfer:false
+ given_clause ~useage ~noinfer:false
bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives
with
| Sup.Success (bag, _, (i,_,_,_)) ->
(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 ->
projects / helm.git / blobdiff